---

Step * 1 1 1 1 1 2 3 2 1 3 2 1 1 1 1 3 1 1 of Lemma comp-op-to-comp-fun-inverse

.....set predicate..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u)
4. ∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:Gamma(I+i). ∀phi:𝔽(I).
   ∀u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}. ∀a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
     ((cA I i rho phi u a0 (i1)(rho) g)
     = (cA J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
     ∈ A(g((i1)(rho))))
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I} 
7. rho : Gamma(I+i)
8. phi : 𝔽(I)
9. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
10. x : A((i0)(rho))
11. ∀J:fset(ℕ). ∀f:I,phi(J).  ((x (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
12. <new-name(I)> ∈ 𝕀(s(1))
13. ∀xx:Top. ((cube+(I;i) xx (s(1);<new-name(I)>)) = 1,i=new-name(I) ∈ I+new-name(I) ⟶ I+i)
14. (<rho> o cube+(I;i))(s(1);<new-name(I)>) = 1,i=new-name(I)(rho) ∈ Gamma(I+new-name(I))
15. ((u)cube+(I;i))<(s(1);<new-name(I)>)> o iota
= (u)subset-trans(I+i;I+new-name(I);1,i=new-name(I);s(phi))
∈ {I+new-name(I),s((phi)<1>) ⊢ _:(A)<(<rho> o cube+(I;i))(s(1);<new-name(I)>)> o iota}
16. J : fset(ℕ)
17. ∀f:I,phi(J). ((x (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
18. f : J ⟶ I
19. ((phi)<1> f) = 1
20. (x (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho)))
⊢ (s((phi)<1>) (new-name(I)0) ⋅ f) = 1
BY
{ (RWO  "name-morph-satisfies-comp<" 0 THEN Auto THEN NthHypEqGen (-2) THEN EqCDA) }

1
.....subterm..... T:t
3:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u)
4. ∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:Gamma(I+i). ∀phi:𝔽(I).
   ∀u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}. ∀a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
     ((cA I i rho phi u a0 (i1)(rho) g)
     = (cA J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
     ∈ A(g((i1)(rho))))
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I} 
7. rho : Gamma(I+i)
8. phi : 𝔽(I)
9. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
10. x : A((i0)(rho))
11. ∀J:fset(ℕ). ∀f:I,phi(J).  ((x (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
12. <new-name(I)> ∈ 𝕀(s(1))
13. ∀xx:Top. ((cube+(I;i) xx (s(1);<new-name(I)>)) = 1,i=new-name(I) ∈ I+new-name(I) ⟶ I+i)
14. (<rho> o cube+(I;i))(s(1);<new-name(I)>) = 1,i=new-name(I)(rho) ∈ Gamma(I+new-name(I))
15. ((u)cube+(I;i))<(s(1);<new-name(I)>)> o iota
= (u)subset-trans(I+i;I+new-name(I);1,i=new-name(I);s(phi))
∈ {I+new-name(I),s((phi)<1>) ⊢ _:(A)<(<rho> o cube+(I;i))(s(1);<new-name(I)>)> o iota}
16. J : fset(ℕ)
17. ∀f:I,phi(J). ((x (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho))))
18. f : J ⟶ I
19. ((phi)<1> f) = 1
20. (x (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho)))
⊢ (new-name(I)0)(s((phi)<1>)) = (phi)<1> ∈ Point(face_lattice(I))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  cA  :  I:fset(\mBbbN{})
{}\mrightarrow{}  i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
{}\mrightarrow{}  rho:Gamma(I+i)
{}\mrightarrow{}  phi:\mBbbF{}(I)
{}\mrightarrow{}  u:\{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}
{}\mrightarrow{}  cubical-path-0(Gamma;A;I;i;rho;phi;u)
{}\mrightarrow{}  cubical-path-1(Gamma;A;I;i;rho;phi;u)
4.  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  .  \mforall{}j:\{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\}  .  \mforall{}g:J  {}\mrightarrow{}  I.  \mforall{}rho:Gamma(I+i).  \mforall{}phi:\mBbbF{}(I).
      \mforall{}u:\{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}.  \mforall{}a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
          ((cA  I  i  rho  phi  u  a0  (i1)(rho)  g)
          =  (cA  J  j  g,i=j(rho)  g(phi)  (u)subset-trans(I+i;J+j;g,i=j;s(phi))  (a0  (i0)(rho)  g)))
5.  I  :  fset(\mBbbN{})
6.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
7.  rho  :  Gamma(I+i)
8.  phi  :  \mBbbF{}(I)
9.  u  :  \{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}
10.  x  :  A((i0)(rho))
11.  \mforall{}J:fset(\mBbbN{}).  \mforall{}f:I,phi(J).    ((x  (i0)(rho)  f)  =  u((i0)  \mcdot{}  f))
12.  <new-name(I)>  \mmember{}  \mBbbI{}(s(1))
13.  \mforall{}xx:Top.  ((cube+(I;i)  xx  (s(1);<new-name(I)>))  =  1,i=new-name(I))
14.  (<rho>  o  cube+(I;i))(s(1);<new-name(I)>)  =  1,i=new-name(I)(rho)
15.  ((u)cube+(I;i))<(s(1);<new-name(I)>)>  o  iota
=  (u)subset-trans(I+i;I+new-name(I);1,i=new-name(I);s(phi))
16.  J  :  fset(\mBbbN{})
17.  \mforall{}f:I,phi(J).  ((x  (i0)(rho)  f)  =  u((i0)  \mcdot{}  f))
18.  f  :  J  {}\mrightarrow{}  I
19.  ((phi)ə>  f)  =  1
20.  (x  (i0)(rho)  f)  =  u((i0)  \mcdot{}  f)
\mvdash{}  (s((phi)ə>)  (new-name(I)0)  \mcdot{}  f)  =  1


By

---

Latex:
(RWO    "name-morph-satisfies-comp<"  0  THEN  Auto  THEN  NthHypEqGen  (-2)  THEN  EqCDA)

---

Home Index