some clarification

forked-from-1kasper · Oct 23, 2023 · ed1747b · ed1747b
1 parent f8f56ba
commit ed1747b
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/library/data/equiv.anders b/library/data/equiv.anders
@@ -63,6 +63,7 @@ section
   hcomp (Glue A φ [(φ = 1) → e 1=1]) ψ (λ (i : I), [(ψ = 1) → u i 1=1]) (ouc u₀)
 end
 
+-- This is what first projection of “transp (<i> equiv A (p @ i)) 0 (idEquiv A)” computes into.
 def transportε (A B : U) (p : PathP (<_> U) A B) : A → B :=
 λ (x : A), transp p 0 (transp (<_> A) 0 x)