[Agda] Fwd: Fwd: Question about transport and cubical

[John Leo]

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

notnot : (b : Bool) → not (not b) ≡ b
notnot true  = refl
notnot false = refl

e : Bool ≡ Bool
e = isoToPath (iso not not notnot notnot)

a = transp (λ i → e i) i0 true
b = transp (λ _ → Bool) i1 true
c = transp (λ i → e i) i1 true

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.

primGlue Bool
(λ .x →
   (λ { (i = i0) → Bool , isoToEquiv (iso not not notnot notnot)
      ; (i = i1) → Bool , idEquiv Bool
      })
   _ .fst)
(λ .x →
   (λ { (i = i0) → Bool , isoToEquiv (iso not not notnot notnot)
      ; (i = i1) → Bool , idEquiv Bool
      })
   _ .snd)
!= Bool of type Type
when checking that the expression transp (λ i → e i) i1 true has
type _28
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200903/f9562889/attachment.html>