---

Step * 1 1 of Lemma composition-op-nc-e

.....assertion..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I} 
6. j : {j:ℕ| ¬j ∈ I} 
7. ∀g:I ⟶ 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).
     ((comp I i rho phi u a0 (i1)(rho) g)
     = (comp I j g,i=j(rho) g(phi) (u)subset-trans(I+i;I+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
     ∈ A(g((i1)(rho))))
8. rho : Gamma(I+i)
9. phi : 𝔽(I)
10. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
11. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
12. (comp I i rho phi u a0 (i1)(rho) 1)
= (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1))
∈ A(1((i1)(rho)))
13. A((i1)(rho)) = A((j1)(e(i;j)(rho))) ∈ Type
14. comp I i rho phi u a0 ∈ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)} 
⊢ (u)subset-trans(I+i;I+j;e(i;j);s(phi)) ∈ {I+j,s(1(phi)) ⊢ _:(A)<e(i;j)(rho)> o iota}
BY
{ ((InstLemma `cubical-subset-term-trans` [⌜Gamma⌝;⌜A⌝;⌜I⌝;⌜I⌝;⌜i⌝;⌜j⌝;⌜1⌝;⌜rho⌝;⌜phi⌝;⌜u⌝]⋅ THENA Auto)
   THEN (InstLemma `nc-e\'-1` [⌜I⌝;⌜i⌝;⌜j⌝]⋅ THENA Auto)
   ) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I} 
6. j : {j:ℕ| ¬j ∈ I} 
7. ∀g:I ⟶ 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).
     ((comp I i rho phi u a0 (i1)(rho) g)
     = (comp I j g,i=j(rho) g(phi) (u)subset-trans(I+i;I+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
     ∈ A(g((i1)(rho))))
8. rho : Gamma(I+i)
9. phi : 𝔽(I)
10. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
11. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
12. (comp I i rho phi u a0 (i1)(rho) 1)
= (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1))
∈ A(1((i1)(rho)))
13. A((i1)(rho)) = A((j1)(e(i;j)(rho))) ∈ Type
14. comp I i rho phi u a0 ∈ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)} 
15. (u)subset-trans(I+i;I+j;1,i=j;s(phi)) ∈ {I+j,s(1(phi)) ⊢ _:(A)<1,i=j(rho)> o iota}
16. 1,i=j ~ e(i;j)
⊢ (u)subset-trans(I+i;I+j;e(i;j);s(phi)) ∈ {I+j,s(1(phi)) ⊢ _:(A)<e(i;j)(rho)> o iota}

---

Latex:

---

Latex:
.....assertion..... 
1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  comp  :  Gamma  \mvdash{}  CompOp(A)
4.  I  :  fset(\mBbbN{})
5.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
6.  j  :  \{j:\mBbbN{}|  \mneg{}j  \mmember{}  I\} 
7.  \mforall{}g:I  {}\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).
          ((comp  I  i  rho  phi  u  a0  (i1)(rho)  g)
          =  (comp  I  j  g,i=j(rho)  g(phi)  (u)subset-trans(I+i;I+j;g,i=j;s(phi))  (a0  (i0)(rho)  g)))
8.  rho  :  Gamma(I+i)
9.  phi  :  \mBbbF{}(I)
10.  u  :  \{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}
11.  a0  :  cubical-path-0(Gamma;A;I;i;rho;phi;u)
12.  (comp  I  i  rho  phi  u  a0  (i1)(rho)  1)
=  (comp  I  j  e(i;j)(rho)  1(phi)  (u)subset-trans(I+i;I+j;e(i;j);s(phi))  (a0  (i0)(rho)  1))
13.  A((i1)(rho))  =  A((j1)(e(i;j)(rho)))
14.  comp  I  i  rho  phi  u  a0  \mmember{}  \{a1:A((i1)(rho))|  cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)\} 
\mvdash{}  (u)subset-trans(I+i;I+j;e(i;j);s(phi))  \mmember{}  \{I+j,s(1(phi))  \mvdash{}  \_:(A)<e(i;j)(rho)>  o  iota\}


By

---

Latex:
((InstLemma  `cubical-subset-term-trans`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}rho\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  (InstLemma  `nc-e\mbackslash{}'-1`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index