search

HoTT / book

A textbook on informal homotopy type theory
2.04k stars 360 forks source link

Universe problems in exercise 10.11 #724

Open mikeshulman opened 10 years ago

mikeshulman commented 10 years ago

In order to prove that V as defined in Exercise 10.11 admits the constructor (ii) of Definition 10.5.1 (which in the Coq formalization is called setext'), we let R : A -> B -> Prop be fun a b => f a = g b. Note that this lives in the same universe as V itself. However, the usual rules for universe levels of (higher) inductive types would demand that the V of Exercise 10.11 live in a larger universe than that of any R to which its second constructor can be applied.

(The Coq formalization didn't notice this because the size of path-constructors doesn't actually affect the size of a HIT, since they don't appear in its definition as a Private Inductive. That's a separate issue which I'll raise in HoTT/Coq.)

mikeshulman commented 10 years ago

Possibly a solution is to define the bisimulation directly from the induction principle of ex 10.11, and then use that when proving def 10.5.1.