---

Step * of Lemma pi-comp-nu-uniformity

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[cA:Gamma ⊢ CompOp(A)]. ∀[I:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[rho:Gamma(I+i)].
∀[J,K:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[g:K ⟶ J]. ∀[u:A(f((i1)(rho)))]. ∀[j:{j:ℕ| ¬j ∈ J} ]. ∀[k:{k:ℕ| ¬k ∈ K} ].
  ((pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j) f,i=j(rho) g,j=k)
  = pi-comp-nu(Gamma;A;cA;I;i;rho;K;f ⋅ g;(u f((i1)(rho)) g);k)
  ∈ A(f ⋅ g,i=k(rho)))
BY
{ (Auto
   THEN (RepUR ``pi-comp-nu`` 0 THEN (GenConclTerm ⌜fill_from_comp(Gamma;A;cA)⌝⋅ THENA Auto))
   THEN Thin (-1)
   THEN RenameVar `fill' (-1)
   THEN D -1
   THEN RepUR ``let`` 0
   THEN (Assert u ∈ cubical-path-0(Gamma;A;J;j;f,i=1-j(rho);0;()) BY
               (BLemma `member-cubical-path-0-0` THEN Auto))
   THEN (Assert fill J j f,i=1-j(rho) 0 () u ∈ A(f,i=1-j(rho)) BY
               (DoSubsume
                THEN Auto
                THEN InstLemma `section-iota_wf` [⌜Gamma⌝;⌜A⌝;⌜J+j⌝;⌜f,i=1-j(rho)⌝;⌜a⌝;⌜s(0)⌝]⋅
                THEN Auto))
   THEN Unfold `filling-uniformity` -3
   THEN (InstHyp [⌜J⌝;⌜K⌝;⌜j⌝;⌜k⌝;⌜g⌝;⌜f,i=1-j(rho)⌝;⌜0⌝;⌜()⌝;⌜u⌝] (-3)⋅ THENA Auto)
   THEN DVar `i'
   THEN DVar `j'
   THEN DVar `k') }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : ℕ
6. ¬i ∈ I
7. rho : Gamma(I+i)
8. J : fset(ℕ)
9. K : fset(ℕ)
10. f : J ⟶ I
11. g : K ⟶ J
12. u : A(f((i1)(rho)))
13. j : ℕ
14. ¬j ∈ J
15. k : ℕ
16. ¬k ∈ K
17. fill : I:fset(ℕ)
⟶ i:{i:ℕ| ¬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)
⟶ {a:A(rho)| 
    (section-iota(Gamma;A;I+i;rho;a) = u ∈ {I+i,s(phi) ⊢ _:(A)<rho> o iota}) ∧ ((a rho (i0)) = a0 ∈ A((i0)(rho)))} 
18. ∀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).
      ((fill I i rho phi u a0 rho g,i=j)
      = (fill 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,i=j(rho)))
19. u ∈ cubical-path-0(Gamma;A;J;j;f,i=1-j(rho);0;())
20. fill J j f,i=1-j(rho) 0 () u ∈ A(f,i=1-j(rho))
21. (fill J j f,i=1-j(rho) 0 () u f,i=1-j(rho) g,j=k)
= (fill K k g,j=k(f,i=1-j(rho)) g(0) (())subset-trans(J+j;K+k;g,j=k;s(0)) (u (j0)(f,i=1-j(rho)) g))
∈ A(g,j=k(f,i=1-j(rho)))
⊢ ((fill J j f,i=1-j(rho) 0 () u f,i=1-j(rho) r_j) f,i=j(rho) g,j=k)
= (fill K k f ⋅ g,i=1-k(rho) 0 () (u f((i1)(rho)) g) f ⋅ g,i=1-k(rho) r_k)
∈ A(f ⋅ g,i=k(rho))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  CompOp(A)].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  ].
\mforall{}[rho:Gamma(I+i)].  \mforall{}[J,K:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].  \mforall{}[g:K  {}\mrightarrow{}  J].  \mforall{}[u:A(f((i1)(rho)))].
\mforall{}[j:\{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\}  ].  \mforall{}[k:\{k:\mBbbN{}|  \mneg{}k  \mmember{}  K\}  ].
    ((pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u;j)  f,i=j(rho)  g,j=k)
    =  pi-comp-nu(Gamma;A;cA;I;i;rho;K;f  \mcdot{}  g;(u  f((i1)(rho))  g);k))


By

---

Latex:
(Auto
  THEN  (RepUR  ``pi-comp-nu``  0  THEN  (GenConclTerm  \mkleeneopen{}fill\_from\_comp(Gamma;A;cA)\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  Thin  (-1)
  THEN  RenameVar  `fill'  (-1)
  THEN  D  -1
  THEN  RepUR  ``let``  0
  THEN  (Assert  u  \mmember{}  cubical-path-0(Gamma;A;J;j;f,i=1-j(rho);0;())  BY
                          (BLemma  `member-cubical-path-0-0`  THEN  Auto))
  THEN  (Assert  fill  J  j  f,i=1-j(rho)  0  ()  u  \mmember{}  A(f,i=1-j(rho))  BY
                          (DoSubsume
                            THEN  Auto
                            THEN  InstLemma  `section-iota\_wf`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}J+j\mkleeneclose{};\mkleeneopen{}f,i=1-j(rho)\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}s(0)\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  THEN  Unfold  `filling-uniformity`  -3
  THEN  (InstHyp  [\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}f,i=1-j(rho)\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}()\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  DVar  `i'
  THEN  DVar  `j'
  THEN  DVar  `k')

---

Home Index