---

Step * 2 2 1 3 of Lemma named-path-morph_wf

.....subterm..... T:t
3:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. K : Cname List
7. f : name-morph(I;K)
8. alpha : X(I)
9. z : Cname
10. ¬(z ∈ I)
11. w : A(iota(z)(alpha))
12. (w iota(z)(alpha) (z:=0)) = a(alpha) ∈ A(alpha)
13. (w iota(z)(alpha) (z:=1)) = b(alpha) ∈ A(alpha)
14. x : Cname
15. ¬(x ∈ K)
16. ((w iota(z)(alpha) (z:=1)) alpha f) = b(f(alpha)) ∈ A(f(alpha))
17. ((w iota(z)(alpha) f[z:=x]) f[z:=x](iota(z)(alpha)) (x:=1))
= (w iota(z)(alpha) (f[z:=x] o (x:=1)))
∈ A((f[z:=x] o (x:=1))(iota(z)(alpha)))
⊢ ((w iota(z)(alpha) (z:=1)) alpha f) = (w iota(z)(alpha) (f[z:=x] o (x:=1))) ∈ A(f(alpha))
BY
{ ((InstLemma `cubical-type-ap-morph-comp`  [⌜X⌝;⌜A⌝;⌜[z / I]⌝;⌜I⌝;⌜K⌝;⌜(z:=1)⌝;⌜f⌝;⌜iota(z)(alpha)⌝;⌜w⌝]⋅ THENA Auto)
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
4:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. K : Cname List
7. f : name-morph(I;K)
8. alpha : X(I)
9. z : Cname
10. ¬(z ∈ I)
11. w : A(iota(z)(alpha))
12. (w iota(z)(alpha) (z:=0)) = a(alpha) ∈ A(alpha)
13. (w iota(z)(alpha) (z:=1)) = b(alpha) ∈ A(alpha)
14. x : Cname
15. ¬(x ∈ K)
16. ((w iota(z)(alpha) (z:=1)) alpha f) = b(f(alpha)) ∈ A(f(alpha))
17. ((w iota(z)(alpha) f[z:=x]) f[z:=x](iota(z)(alpha)) (x:=1))
= (w iota(z)(alpha) (f[z:=x] o (x:=1)))
∈ A((f[z:=x] o (x:=1))(iota(z)(alpha)))
18. ((w iota(z)(alpha) (z:=1)) (z:=1)(iota(z)(alpha)) f)
= (w iota(z)(alpha) ((z:=1) o f))
∈ A(((z:=1) o f)(iota(z)(alpha)))
⊢ f = (iota(z) o ((z:=1) o f)) ∈ name-morph(I;K)

2
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. K : Cname List
7. f : name-morph(I;K)
8. alpha : X(I)
9. z : Cname
10. ¬(z ∈ I)
11. w : A(iota(z)(alpha))
12. (w iota(z)(alpha) (z:=0)) = a(alpha) ∈ A(alpha)
13. (w iota(z)(alpha) (z:=1)) = b(alpha) ∈ A(alpha)
14. x : Cname
15. ¬(x ∈ K)
16. ((w iota(z)(alpha) (z:=1)) alpha f) = b(f(alpha)) ∈ A(f(alpha))
17. ((w iota(z)(alpha) f[z:=x]) f[z:=x](iota(z)(alpha)) (x:=1))
= (w iota(z)(alpha) (f[z:=x] o (x:=1)))
∈ A((f[z:=x] o (x:=1))(iota(z)(alpha)))
18. ((w iota(z)(alpha) (z:=1)) (z:=1)(iota(z)(alpha)) f)
= (w iota(z)(alpha) ((z:=1) o f))
∈ A(((z:=1) o f)(iota(z)(alpha)))
⊢ alpha = (iota(z) o (z:=1))(alpha) ∈ X(I)

3
.....subterm..... T:t
3:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. K : Cname List
7. f : name-morph(I;K)
8. alpha : X(I)
9. z : Cname
10. ¬(z ∈ I)
11. w : A(iota(z)(alpha))
12. (w iota(z)(alpha) (z:=0)) = a(alpha) ∈ A(alpha)
13. (w iota(z)(alpha) (z:=1)) = b(alpha) ∈ A(alpha)
14. x : Cname
15. ¬(x ∈ K)
16. ((w iota(z)(alpha) (z:=1)) alpha f) = b(f(alpha)) ∈ A(f(alpha))
17. ((w iota(z)(alpha) f[z:=x]) f[z:=x](iota(z)(alpha)) (x:=1))
= (w iota(z)(alpha) (f[z:=x] o (x:=1)))
∈ A((f[z:=x] o (x:=1))(iota(z)(alpha)))
18. ((w iota(z)(alpha) (z:=1)) (z:=1)(iota(z)(alpha)) f)
= (w iota(z)(alpha) ((z:=1) o f))
∈ A(((z:=1) o f)(iota(z)(alpha)))
⊢ (w iota(z)(alpha) (f[z:=x] o (x:=1))) = (w iota(z)(alpha) ((z:=1) o f)) ∈ A(f(alpha))

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  b  :  \{X  \mvdash{}  \_:A\}
5.  I  :  Cname  List
6.  K  :  Cname  List
7.  f  :  name-morph(I;K)
8.  alpha  :  X(I)
9.  z  :  Cname
10.  \mneg{}(z  \mmember{}  I)
11.  w  :  A(iota(z)(alpha))
12.  (w  iota(z)(alpha)  (z:=0))  =  a(alpha)
13.  (w  iota(z)(alpha)  (z:=1))  =  b(alpha)
14.  x  :  Cname
15.  \mneg{}(x  \mmember{}  K)
16.  ((w  iota(z)(alpha)  (z:=1))  alpha  f)  =  b(f(alpha))
17.  ((w  iota(z)(alpha)  f[z:=x])  f[z:=x](iota(z)(alpha))  (x:=1))
=  (w  iota(z)(alpha)  (f[z:=x]  o  (x:=1)))
\mvdash{}  ((w  iota(z)(alpha)  (z:=1))  alpha  f)  =  (w  iota(z)(alpha)  (f[z:=x]  o  (x:=1)))


By

---

Latex:
((InstLemma  `cubical-type-ap-morph-comp` 
    [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}[z  /  I]\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}(z:=1)\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}iota(z)(alpha)\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto)

---

Home Index