---

Step * of Lemma cubical-type-ap-morph-id

∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[f:name-morph(I;I)]. ∀[a:X(I)]. ∀[u:A(a)].
  (u a f) = u ∈ A(a) supposing f = 1 ∈ name-morph(I;I)
BY
{ xxx(Auto THEN (StrongHypSubst  (-1) 0 THENA Auto) THEN RepeatFor 2 (DVar `A') THEN All Reduce)xxx }

1
1. X : CubicalSet
2. A1 : I:(Cname List) ⟶ X(I) ⟶ Type
3. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
4. (∀I:Cname List. ∀a:X(I). ∀u:A1 I a.  ((A2 I I 1 a u) = u ∈ (A1 I a)))
∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A1 I a.
     ((A2 I K (f o g) a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K (f o g)(a))))
5. I : Cname List
6. f : name-morph(I;I)
7. a : X(I)
8. u : <A1, A2>(a)
9. f = 1 ∈ name-morph(I;I)
⊢ (u a 1) = u ∈ <A1, A2>(a)

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[I:Cname  List].  \mforall{}[f:name-morph(I;I)].  \mforall{}[a:X(I)].  \mforall{}[u:A(a)].
    (u  a  f)  =  u  supposing  f  =  1


By

---

Latex:
xxx(Auto  THEN  (StrongHypSubst    (-1)  0  THENA  Auto)  THEN  RepeatFor  2  (DVar  `A')  THEN  All  Reduce)xxx

---

Home Index