Step * of Lemma sigmacomp_wf

No Annotations
[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[B:{Gamma.A ⊢ _}]. ∀[cA:Gamma ⊢ CompOp(A)]. ∀[cB:Gamma.A ⊢ CompOp(B)].
  (sigmacomp(Gamma;A;B;cA;cB) ∈ Gamma ⊢ CompOp(Σ B))
BY
(Intros
   THEN MemTypeCD
   THEN Auto
   THEN 0
   THEN Auto
   THEN Unfold `sigmacomp` 0
   THEN Reduce 0
   THEN (GenConclTerm ⌜fill_from_comp(Gamma;A;cA)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `fillA' (-1)
   THEN DVar `cA'
   THEN DVar  `cB'
   THEN RenameVar `mu' (-3)
   THEN RenameVar `lambda' (-2)) }

1
1. Gamma CubicalSet{j}
2. {Gamma ⊢ _}
3. {Gamma.A ⊢ _}
4. cA I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> iota}
⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u)
5. composition-uniformity(Gamma;A;cA)
6. cB I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:Gamma.A(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(B)<rho> iota}
⟶ cubical-path-0(Gamma.A;B;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma.A;B;I;i;rho;phi;u)
7. composition-uniformity(Gamma.A;B;cB)
8. fset(ℕ)
9. fset(ℕ)
10. {i:ℕ| ¬i ∈ I} 
11. {j:ℕ| ¬j ∈ J} 
12. J ⟶ I
13. rho Gamma(I+i)
14. phi : 𝔽(I)
15. mu {I+i,s(phi) ⊢ _:(Σ B)<rho> iota}
16. lambda cubical-path-0(Gamma;Σ B;I;i;rho;phi;mu)
17. fillA filling-op(Gamma;A)
⊢ (let fillA rho phi mu.1 (fst(lambda)) in
    let cB (rho;v) phi mu.2 (snd(lambda)) in
    <(v rho (i1)), w> (i1)(rho) g)
let fillA g,i=j(rho) g(phi) (mu)subset-trans(I+i;J+j;g,i=j;s(phi)).1 (fst((lambda (i0)(rho) g))) in
   let cB (g,i=j(rho);v) g(phi) (mu)subset-trans(I+i;J+j;g,i=j;s(phi)).2 (snd((lambda (i0)(rho) g))) in
   <(v g,i=j(rho) (j1)), w>
∈ Σ B(g((i1)(rho)))


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)].
    (sigmacomp(Gamma;A;B;cA;cB)  \mmember{}  Gamma  \mvdash{}  CompOp(\mSigma{}  A  B))


By


Latex:
(Intros
  THEN  MemTypeCD
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  Unfold  `sigmacomp`  0
  THEN  Reduce  0
  THEN  (GenConclTerm  \mkleeneopen{}fill\_from\_comp(Gamma;A;cA)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `fillA'  (-1)
  THEN  DVar  `cA'
  THEN  DVar    `cB'
  THEN  RenameVar  `mu'  (-3)
  THEN  RenameVar  `lambda'  (-2))




Home Index