---

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


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. cubical-path-condition(Gamma;A;I;i;rho;phi;u;x)
12. <new-name(I)> ∈ 𝕀(s(1))
13. (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)))
14. ∀xx:Top. ((cube+(I;i) xx (s(1);<new-name(I)>)) = 1,i=new-name(I) ∈ I+new-name(I) ⟶ I+i)
15. (<rho> o cube+(I;i))(s(1);<new-name(I)>) = 1,i=new-name(I)(rho) ∈ Gamma(I+new-name(I))
16. ((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}
17. j : names(I+i)
18. j ≠ i
⊢ (dM-lift(I;I;1) ((i0) j))
= (dM-lift(I;I+new-name(I);(new-name(I)0)) (dM-lift(I+new-name(I);I;s) (1 j)))
∈ Point(dM(I))
BY
{ (RepUR ``nc-0 nh-id`` 0 THEN AutoSplit THEN Fold `nc-0` 0) }

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> o iota}
10. x : A((i0)(rho))
11. cubical-path-condition(Gamma;A;I;i;rho;phi;u;x)
12. <new-name(I)> ∈ 𝕀(s(1))
13. (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)))
14. ∀xx:Top. ((cube+(I;i) xx (s(1);<new-name(I)>)) = 1,i=new-name(I) ∈ I+new-name(I) ⟶ I+i)
15. (<rho> o cube+(I;i))(s(1);<new-name(I)>) = 1,i=new-name(I)(rho) ∈ Gamma(I+new-name(I))
16. ((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}
17. j : names(I+i)
18. j ≠ i
19. j ≠ i
⊢ (dM-lift(I;I;λx.<x>) <j>) = (dM-lift(I;I+new-name(I);(new-name(I)0)) (dM-lift(I+new-name(I);I;s) <j>)) ∈ Point(dM(I))

---

Latex:

---

Latex:

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.  cubical-path-condition(Gamma;A;I;i;rho;phi;u;x)
12.  <new-name(I)>  \mmember{}  \mBbbI{}(s(1))
13.  (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))
14.  \mforall{}xx:Top.  ((cube+(I;i)  xx  (s(1);<new-name(I)>))  =  1,i=new-name(I))
15.  (<rho>  o  cube+(I;i))(s(1);<new-name(I)>)  =  1,i=new-name(I)(rho)
16.  ((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))
17.  j  :  names(I+i)
18.  j  \mneq{}  i
\mvdash{}  (dM-lift(I;I;1)  ((i0)  j))
=  (dM-lift(I;I+new-name(I);(new-name(I)0))  (dM-lift(I+new-name(I);I;s)  (1  j)))


By

---

Latex:
(RepUR  ``nc-0  nh-id``  0  THEN  AutoSplit  THEN  Fold  `nc-0`  0)

---

Home Index