[FOM] foundations meeting/FOMUS/dicussion

[Paul B Levy]

> 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


-- 
Paul Blain Levy
School of Computer Science, University of Birmingham
http://www.cs.bham.ac.uk/~pbl