---

Step * of Lemma pi-comp-uniformity

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[B:{Gamma.A ⊢ _}]. ∀[cA:Gamma ⊢ CompOp(A)]. ∀[cB:Gamma.A ⊢ CompOp(B)].
  composition-uniformity(Gamma;ΠA B;pi-comp(Gamma;A;B;cA;cB))
BY
{ (Intros
   THEN (D 0 THENA Auto)
   THEN Intros
   THEN (Assert (pi-comp(Gamma;A;B;cA;cB) I i rho phi u a0 (i1)(rho) g) ∈ ΠA B(g((i1)(rho))) BY
               Auto)
   THEN RepUR ``cubical-pi cubical-pi-family`` -1
   THEN (MemTypeHD (-1) THENA Auto)
   THEN RepUR ``cubical-pi cubical-pi-family`` 0
   THEN (EqTypeCD THENW Auto)
   THEN Try (Trivial)
   THEN RepeatFor 2 (Thin (-1))
   THEN RenameVar `mu' (-2)
   THEN RenameVar `lambda' (-1)
   THEN (FunExt THENA Auto)
   THEN RenameVar `K' (-1)
   THEN (FunExt THENA Auto)
   THEN Reduce 0
   THEN (FunExt THENA Auto)
   THEN RepUR ``pi-comp`` 0
   THEN (GenConclTerm ⌜new-name(K)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `k' (-1)
   THEN (CallByValueReduce 0 THENA Auto)) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. cA : Gamma ⊢ CompOp(A)
5. cB : Gamma.A ⊢ CompOp(B)
6. I : fset(ℕ)
7. J : fset(ℕ)
8. i : {i:ℕ| ¬i ∈ I} 
9. j : {j:ℕ| ¬j ∈ J} 
10. g : J ⟶ I
11. rho : Gamma(I+i)
12. phi : 𝔽(I)
13. mu : {I+i,s(phi) ⊢ _:(ΠA B)<rho> o iota}
14. lambda : cubical-path-0(Gamma;ΠA B;I;i;rho;phi;mu)
15. K : fset(ℕ)
16. f : K ⟶ J
17. u : A(f(g((i1)(rho))))
18. k : {i:ℕ| ¬i ∈ K} 
⊢ let nu = pi-comp-nu(Gamma;A;cA;I;i;rho;K;g ⋅ f;u;k) in
      cB K k (g ⋅ f,i=k(rho);nu) g ⋅ f(phi) pi-comp-app(Gamma;A;I;i;rho;phi;mu;K;g ⋅ f;k;nu) 
      pi-comp-lambda(Gamma;A;I;i;rho;lambda;K;g ⋅ f;k;nu)
= let nu = pi-comp-nu(Gamma;A;cA;J;j;g,i=j(rho);K;f;u;k) in
      cB K k (f,j=k(g,i=j(rho));nu) f(g(phi)) 
      pi-comp-app(Gamma;A;J;j;g,i=j(rho);g(phi);(mu)subset-trans(I+i;J+j;g,i=j;s(phi));K;f;k;nu) 
      pi-comp-lambda(Gamma;A;J;j;g,i=j(rho);λK,g@0. (lambda K g ⋅ g@0);K;f;k;nu)
∈ B((f(g((i1)(rho)));u))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[B:\{Gamma.A  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  CompOp(A)].
\mforall{}[cB:Gamma.A  \mvdash{}  CompOp(B)].
    composition-uniformity(Gamma;\mPi{}A  B;pi-comp(Gamma;A;B;cA;cB))


By

---

Latex:
(Intros
  THEN  (D  0  THENA  Auto)
  THEN  Intros
  THEN  (Assert  (pi-comp(Gamma;A;B;cA;cB)  I  i  rho  phi  u  a0  (i1)(rho)  g)  \mmember{}  \mPi{}A  B(g((i1)(rho)))  BY
                          Auto)
  THEN  RepUR  ``cubical-pi  cubical-pi-family``  -1
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  RepUR  ``cubical-pi  cubical-pi-family``  0
  THEN  (EqTypeCD  THENW  Auto)
  THEN  Try  (Trivial)
  THEN  RepeatFor  2  (Thin  (-1))
  THEN  RenameVar  `mu'  (-2)
  THEN  RenameVar  `lambda'  (-1)
  THEN  (FunExt  THENA  Auto)
  THEN  RenameVar  `K'  (-1)
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0
  THEN  (FunExt  THENA  Auto)
  THEN  RepUR  ``pi-comp``  0
  THEN  (GenConclTerm  \mkleeneopen{}new-name(K)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `k'  (-1)
  THEN  (CallByValueReduce  0  THENA  Auto))

---

Home Index