Step * 2 of Lemma cubical-sigma_wf


1. CubicalSet
2. {X ⊢ _}
3. {X.A ⊢ _}
4. ∀I:Cname List. ∀a:X(I). ∀u:u:A(a) × B((a;u)).  (<(fst(u) 1), (snd(u) (a;fst(u)) 1)> u ∈ (u:A(a) × B((a;u))))
5. Cname List
6. Cname List
7. Cname List
8. name-morph(I;J)
9. name-morph(J;K)
10. X(I)
11. u:A(a) × B((a;u))
⊢ <(fst(u) (f g)), (snd(u) (a;fst(u)) (f g))>
= <((fst(u) f) f(a) g), ((snd(u) (a;fst(u)) f) (f(a);(fst(u) f)) g)>
∈ (u:A((f g)(a)) × B(((f g)(a);u)))
BY
(((RepeatFor (DVar `B') THEN (Assert X ⊢ BY Auto) THEN RepeatFor (DVar `A'))
    THEN All Reduce
    THEN RepUR ``cubical-type-ap-morph cubical-type-at`` 0 ⋅)
   THEN EqCD
   THEN Auto) }

1
1. 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 a) ⟶ (A1 f(a))
4. ∀I:Cname List. ∀a:X(I). ∀u:A1 a.  ((A2 u) u ∈ (A1 a))
5. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A1 a.
     ((A2 (f g) u) (A2 f(a) (A2 u)) ∈ (A1 (f g)(a)))
6. A@0 I:(Cname List) ⟶ X.<A1, A2>(I) ⟶ Type
7. B1 I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X.<A1, A2>(I) ⟶ (A@0 a) ⟶ (A@0 f(a))
8. ∀I:Cname List. ∀a:X.<A1, A2>(I). ∀u:A@0 a.  ((B1 u) u ∈ (A@0 a))
9. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X.<A1, A2>(I). ∀u:A@0 a.
     ((B1 (f g) u) (B1 f(a) (B1 u)) ∈ (A@0 (f g)(a)))
10. ∀I:Cname List. ∀a:X(I). ∀u:u:<A1, A2>(a) × <A@0, B1>((a;u)).
      (<(fst(u) 1), (snd(u) (a;fst(u)) 1)> u ∈ (u:<A1, A2>(a) × <A@0, B1>((a;u))))
11. Cname List
12. Cname List
13. Cname List
14. name-morph(I;J)
15. name-morph(J;K)
16. X(I)
17. u:<A1, A2>(a) × <A@0, B1>((a;u))
18. X ⊢ <A1, A2>
⊢ (B1 (f g) (a;fst(u)) (snd(u)))
(B1 (f(a);A2 (fst(u))) (B1 (a;fst(u)) (snd(u))))
∈ (A@0 ((f g)(a);A2 (f g) (fst(u))))


Latex:


Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  B  :  \{X.A  \mvdash{}  \_\}
4.  \mforall{}I:Cname  List.  \mforall{}a:X(I).  \mforall{}u:u:A(a)  \mtimes{}  B((a;u)).    (<(fst(u)  a  1),  (snd(u)  (a;fst(u))  1)>  =  u)
5.  I  :  Cname  List
6.  J  :  Cname  List
7.  K  :  Cname  List
8.  f  :  name-morph(I;J)
9.  g  :  name-morph(J;K)
10.  a  :  X(I)
11.  u  :  u:A(a)  \mtimes{}  B((a;u))
\mvdash{}  <(fst(u)  a  (f  o  g)),  (snd(u)  (a;fst(u))  (f  o  g))>
=  <((fst(u)  a  f)  f(a)  g),  ((snd(u)  (a;fst(u))  f)  (f(a);(fst(u)  a  f))  g)>


By


Latex:
(((RepeatFor  2  (DVar  `B')  THEN  (Assert  X  \mvdash{}  A  BY  Auto)  THEN  RepeatFor  2  (DVar  `A'))
    THEN  All  Reduce
    THEN  RepUR  ``cubical-type-ap-morph  cubical-type-at``  0  \mcdot{})
  THEN  EqCD
  THEN  Auto)




Home Index