---

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


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)
BY
{ ((Unfold `cubical-type-at` -2 THEN Reduce -2)
   THEN Unfolds ``cubical-type-at cubical-type-ap-morph`` 0
   THEN Reduce 0) }

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 I a
9. f = 1 ∈ name-morph(I;I)
⊢ (A2 I I 1 a u) = u ∈ (A1 I a)

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A1  :  I:(Cname  List)  {}\mrightarrow{}  X(I)  {}\mrightarrow{}  Type
3.  A2  :  I:(Cname  List)  {}\mrightarrow{}  J:(Cname  List)  {}\mrightarrow{}  f:name-morph(I;J)  {}\mrightarrow{}  a:X(I)  {}\mrightarrow{}  (A1  I  a)  {}\mrightarrow{}  (A1  J  f(a))
4.  (\mforall{}I:Cname  List.  \mforall{}a:X(I).  \mforall{}u:A1  I  a.    ((A2  I  I  1  a  u)  =  u))
\mwedge{}  (\mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).  \mforall{}a:X(I).  \mforall{}u:A1  I  a.
          ((A2  I  K  (f  o  g)  a  u)  =  (A2  J  K  g  f(a)  (A2  I  J  f  a  u))))
5.  I  :  Cname  List
6.  f  :  name-morph(I;I)
7.  a  :  X(I)
8.  u  :  <A1,  A2>(a)
9.  f  =  1
\mvdash{}  (u  a  1)  =  u


By

---

Latex:
((Unfold  `cubical-type-at`  -2  THEN  Reduce  -2)
  THEN  Unfolds  ``cubical-type-at  cubical-type-ap-morph``  0
  THEN  Reduce  0)

---

Home Index