<div dir="ltr">I do have one further point I'd like clarified. Is the check for the r=i1 condition for transp done only when r is not known to be i0 or is it always done? For example is the check run at all when transport p (defined as "transp (λ i → p i) i0") is called? I assume not. For example in the following code<div><br></div><div><font face="monospace">notnot : (b : Bool) → not (not b) ≡ b<br>notnot true  = refl<br>notnot false = refl<br><br>e : Bool ≡ Bool<br>e = isoToPath (iso not not notnot notnot)</font></div><div><font face="monospace"><br>a = transp (λ i → e i) i0 true<br>b = transp (λ _ → Bool) i1 true<br>c = transp (λ i → e i) i1 true<br></font></div><div><br></div><div><div>I get that "a" and "b" typecheck ("a" evaluates to false and "b" to true as expected) but "c" fails to typecheck with the following error, which I assume is due to "e" not being definitionally constant. But perhaps I'm still confused.</div><div><br></div><div><font face="monospace">primGlue Bool<br>(λ .x →<br>   (λ { (i = i0) → Bool , isoToEquiv (iso not not notnot notnot)<br>      ; (i = i1) → Bool , idEquiv Bool<br>      })<br>   _ .fst)<br>(λ .x →<br>   (λ { (i = i0) → Bool , isoToEquiv (iso not not notnot notnot)<br>      ; (i = i1) → Bool , idEquiv Bool<br>      })<br>   _ .snd)<br>!= Bool of type Type<br>when checking that the expression transp (λ i → e i) i1 true has<br>type _28</font><br></div><div><br></div><div><br></div><div><br></div></div></div>