---

Step * 1 1 1 1 1 2 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 : 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)
⊢ (cA I i rho phi u x)
= (cA I new-name(I) (<rho> o cube+(I;i))(s(1);<new-name(I)>) (phi ⋅ 1) ((u)cube+(I;i))<(s(1);<new-name(I)>)> o iota 
   (x (i0)(rho) 1))
∈ A((i1)(rho))
BY
{ ((Assert (<rho> o cube+(I;i))(s(1);<new-name(I)>) = 1,i=new-name(I)(rho) ∈ Gamma(I+new-name(I)) BY
          Auto)
   THEN NthHypEqGen (-3)
   THEN EqCDA) }

1
.....subterm..... T:t
1: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 : 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))
⊢ A((i1)(rho)) = A(1((i1)(rho))) ∈ Type

2
.....subterm..... T:t
2: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 : 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))
⊢ (cA I i rho phi u x) = (cA I i rho phi u x (i1)(rho) 1) ∈ A((i1)(rho))

3
.....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 : 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))
⊢ (cA I new-name(I) (<rho> o cube+(I;i))(s(1);<new-name(I)>) (phi ⋅ 1) ((u)cube+(I;i))<(s(1);<new-name(I)>)> o iota 
   (x (i0)(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((i1)(rho))

---

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  :  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))
\mvdash{}  (cA  I  i  rho  phi  u  x)
=  (cA  I  new-name(I)  (<rho>  o  cube+(I;i))(s(1);<new-name(I)>)  (phi  \mcdot{}  1) 
      ((u)cube+(I;i))<(s(1);<new-name(I)>)>  o  iota 
      (x  (i0)(rho)  1))


By

---

Latex:
((Assert  (<rho>  o  cube+(I;i))(s(1);<new-name(I)>)  =  1,i=new-name(I)(rho)  BY
                Auto)
  THEN  NthHypEqGen  (-3)
  THEN  EqCDA)

---

Home Index