---

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

.....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>}
10. x : cubical-path-0(Gamma;A;I;i;rho;phi;u)
11. <new-name(I)> ∈ 𝕀(s(1))
12. (cA I i rho phi u x (i1)(rho) 1)
= (cA I new-name(I) 1,i=new-name(I)(rho) 1(phi) (u)subset-trans(I+i;I+new-name(I);1,i=new-name(I);s(phi)) 
   (x (i0)(rho) 1))
∈ A(1((i1)(rho)))
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. I1 : fset(ℕ)
16. a : I1 ⟶ I+new-name(I)
17. (s((phi)<1>) a) = 1
18. (cube+(I;i) I1 (s(1);<new-name(I)>)) = 1,i=new-name(I) ∈ I+new-name(I) ⟶ I+i
19. (A)<rho>(1,i=new-name(I) ⋅ a) = (A)<1,i=new-name(I)(rho)>(a) ∈ Type
⊢ s ⋅ 1,i=new-name(I) = 1 ⋅ s ∈ I+new-name(I) ⟶ I
BY
{ (Unfold `names-hom` 0
   THEN (FunExt THENA Auto)
   THEN skip{(RepUR ``cube+ nc-e\'`` 0
              THEN AutoSplit
              THEN skip{(RepUR ``cube-set-restriction formal-cube`` 0 THEN (Assert x1 ∈ names(I) BY Auto))})}) }

1
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>}
10. x : cubical-path-0(Gamma;A;I;i;rho;phi;u)
11. <new-name(I)> ∈ 𝕀(s(1))
12. (cA I i rho phi u x (i1)(rho) 1)
= (cA I new-name(I) 1,i=new-name(I)(rho) 1(phi) (u)subset-trans(I+i;I+new-name(I);1,i=new-name(I);s(phi)) 
   (x (i0)(rho) 1))
∈ A(1((i1)(rho)))
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. I1 : fset(ℕ)
16. a : I1 ⟶ I+new-name(I)
17. (s((phi)<1>) a) = 1
18. (cube+(I;i) I1 (s(1);<new-name(I)>)) = 1,i=new-name(I) ∈ I+new-name(I) ⟶ I+i
19. (A)<rho>(1,i=new-name(I) ⋅ a) = (A)<1,i=new-name(I)(rho)>(a) ∈ Type
20. x1 : names(I)
⊢ (s ⋅ 1,i=new-name(I) x1) = (1 ⋅ s x1) ∈ Point(dM(I+new-name(I)))

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
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>\}
10.  x  :  cubical-path-0(Gamma;A;I;i;rho;phi;u)
11.  <new-name(I)>  \mmember{}  \mBbbI{}(s(1))
12.  (cA  I  i  rho  phi  u  x  (i1)(rho)  1)
=  (cA  I  new-name(I)  1,i=new-name(I)(rho)  1(phi) 
      (u)subset-trans(I+i;I+new-name(I);1,i=new-name(I);s(phi)) 
      (x  (i0)(rho)  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.  I1  :  fset(\mBbbN{})
16.  a  :  I1  {}\mrightarrow{}  I+new-name(I)
17.  (s((phi)ə>)  a)  =  1
18.  (cube+(I;i)  I1  (s(1);<new-name(I)>))  =  1,i=new-name(I)
19.  (A)<rho>(1,i=new-name(I)  \mcdot{}  a)  =  (A)ə,i=new-name(I)(rho)>(a)
\mvdash{}  s  \mcdot{}  1,i=new-name(I)  =  1  \mcdot{}  s


By

---

Latex:
(Unfold  `names-hom`  0
  THEN  (FunExt  THENA  Auto)
  THEN  skip\{(RepUR  ``cube+  nc-e\mbackslash{}'``  0
                        THEN  AutoSplit
                        THEN  skip\{(RepUR  ``cube-set-restriction  formal-cube``  0
                                              THEN  (Assert  x1  \mmember{}  names(I)  BY
                                                                      Auto)
                                              )\})\})

---

Home Index