---

Step * 1 1 of Lemma cubical-pi_wf


1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. a : X(I)
8. w : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:A(f(a)) ⟶ B((f(a);u))
9. ∀J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀u:A(f(a)).
     ((w J f u (f(a);u) g) = (w K (f o g) (u f(a) g)) ∈ B(g((f(a);u))))
10. J@0 : Cname List
11. K : Cname List
12. f@0 : name-morph(J;J@0)
13. g : name-morph(J@0;K)
14. u : A(f@0(f(a)))
⊢ (w J@0 (f o f@0) u (f@0(f(a));u) g) = (w K (f o (f@0 o g)) (u f@0(f(a)) g)) ∈ B(g((f@0(f(a));u)))
BY
{ ((RenameVar `H' (-5) THEN RenameVar `h' (-3))
   THEN (InstHyp [⌜H⌝;⌜K⌝;⌜(f o h)⌝;⌜g⌝;⌜u⌝] (-6)⋅ THENA Auto)
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Try ((EqCD THEN Auto))) }

1
.....antecedent..... 
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. a : X(I)
8. w : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:A(f(a)) ⟶ B((f(a);u))
9. ∀J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀u:A(f(a)).
     ((w J f u (f(a);u) g) = (w K (f o g) (u f(a) g)) ∈ B(g((f(a);u))))
10. H : Cname List
11. K : Cname List
12. h : name-morph(J;H)
13. g : name-morph(H;K)
14. u : A(h(f(a)))
15. (w H (f o h) u ((f o h)(a);u) g) = (w K ((f o h) o g) (u (f o h)(a) g)) ∈ B(g(((f o h)(a);u)))
⊢ True

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  B  :  \{X.A  \mvdash{}  \_\}
4.  I  :  Cname  List
5.  J  :  Cname  List
6.  f  :  name-morph(I;J)
7.  a  :  X(I)
8.  w  :  J:(Cname  List)  {}\mrightarrow{}  f:name-morph(I;J)  {}\mrightarrow{}  u:A(f(a))  {}\mrightarrow{}  B((f(a);u))
9.  \mforall{}J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).  \mforall{}u:A(f(a)).
          ((w  J  f  u  (f(a);u)  g)  =  (w  K  (f  o  g)  (u  f(a)  g)))
10.  J@0  :  Cname  List
11.  K  :  Cname  List
12.  f@0  :  name-morph(J;J@0)
13.  g  :  name-morph(J@0;K)
14.  u  :  A(f@0(f(a)))
\mvdash{}  (w  J@0  (f  o  f@0)  u  (f@0(f(a));u)  g)  =  (w  K  (f  o  (f@0  o  g))  (u  f@0(f(a))  g))


By

---

Latex:
((RenameVar  `H'  (-5)  THEN  RenameVar  `h'  (-3))
  THEN  (InstHyp  [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}(f  o  h)\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]  (-6)\mcdot{}  THENA  Auto)
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Try  ((EqCD  THEN  Auto)))

---

Home Index