Step
*
of Lemma
equal-cubical-identity-at
∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[p,q:I-path(X;A;a;b;I;alpha)].
p = q ∈ (Id_A a b)(alpha) supposing path-eq(X;A;I;alpha;p;q)
BY
{ Auto }
Latex:
Latex:
\mforall{}[X:CubicalSet]. \mforall{}[A:\{X \mvdash{} \_\}]. \mforall{}[a,b:\{X \mvdash{} \_:A\}]. \mforall{}[I:Cname List]. \mforall{}[alpha:X(I)].
\mforall{}[p,q:I-path(X;A;a;b;I;alpha)].
p = q supposing path-eq(X;A;I;alpha;p;q)
By
Latex:
Auto
Home
Index