[FOM] foundations meeting/FOMUS/dicussion

Paul B Levy P.B.Levy at cs.bham.ac.uk
Thu Mar 24 14:41:30 EDT 2016

> Date: Wed, 23 Mar 2016 10:08:10 +0000 From: Staffan Angere 
> <staffan.angere at fil.lu.se>

> HoTT gets coherence from its geometric interpretation: every rule of
> the system can be motivated by that.

True.  But there are also rules disallowed in HoTT (at least, the
specific version of HoTT described in the book) that are valid in the
geometric interpretation.  For example: judgemental eta-laws for sum
type and zero type, and equality reflection for the natural number type.
 The reasons that I have heard for disallowing these things have
nothing to do with the geometric interpretation.


Paul Blain Levy
School of Computer Science, University of Birmingham

More information about the FOM mailing list