---

Step * of Lemma sigmacomp_wf1

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[B:{Gamma.A ⊢ _}]. ∀[cA:Gamma ⊢ CompOp(A)]. ∀[cB:Gamma.A ⊢ CompOp(B)].
  (sigmacomp(Gamma;A;B;cA;cB) ∈ I:fset(ℕ)
   ⟶ i:{i:ℕ| ¬i ∈ I} 
   ⟶ rho:Gamma(I+i)
   ⟶ phi:𝔽(I)
   ⟶ mu:{I+i,s(phi) ⊢ _:(Σ A B)<rho> o iota}
   ⟶ lambda:cubical-path-0(Gamma;Σ A B;I;i;rho;phi;mu)
   ⟶ cubical-path-1(Gamma;Σ A B;I;i;rho;phi;mu))
BY
{ (Intros
   THEN Unfold `sigmacomp` 0
   THEN RepeatFor 6 ((FunExt THENA Auto))
   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') }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. B : {Gamma.A ⊢ _}
4. 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)
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> o 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. I : fset(ℕ)
9. i : {i:ℕ| ¬i ∈ I} 
10. rho : Gamma(I+i)
11. phi : 𝔽(I)
12. mu : {I+i,s(phi) ⊢ _:(Σ A B)<rho> o iota}
13. lambda : cubical-path-0(Gamma;Σ A B;I;i;rho;phi;mu)
14. fillA : filling-op(Gamma;A)
⊢ let v = fillA I i rho phi mu.1 (fst(lambda)) in
   let w = cB I i (rho;v) phi mu.2 (snd(lambda)) in
   <(v rho (i1)), w> ∈ cubical-path-1(Gamma;Σ A B;I;i;rho;phi;mu)

---

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{}  I:fset(\mBbbN{})
      {}\mrightarrow{}  i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
      {}\mrightarrow{}  rho:Gamma(I+i)
      {}\mrightarrow{}  phi:\mBbbF{}(I)
      {}\mrightarrow{}  mu:\{I+i,s(phi)  \mvdash{}  \_:(\mSigma{}  A  B)<rho>  o  iota\}
      {}\mrightarrow{}  lambda:cubical-path-0(Gamma;\mSigma{}  A  B;I;i;rho;phi;mu)
      {}\mrightarrow{}  cubical-path-1(Gamma;\mSigma{}  A  B;I;i;rho;phi;mu))


By

---

Latex:
(Intros
  THEN  Unfold  `sigmacomp`  0
  THEN  RepeatFor  6  ((FunExt  THENA  Auto))
  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')

---

Home Index