---

Step * of Lemma pi-comp_wf1

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[B:{Gamma.A ⊢ _}]. ∀[cA:Gamma ⊢ CompOp(A)]. ∀[cB:Gamma.A ⊢ CompOp(B)].
  (pi-comp(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)
   ⟶ J:fset(ℕ)
   ⟶ f:J ⟶ I
   ⟶ u1:A(f((i1)(rho)))
   ⟶ let j = new-name(J) in
       let nu = pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u1;j) in
       cubical-path-1(Gamma.A;B;J;j;(f,i=j(rho);nu);f(phi);pi-comp-app(Gamma;A;I;i;rho;phi;mu;J;f;j;nu)))
BY
{ (Auto
   THEN RepeatFor 9 ((FunExt THENA Auto))
   THEN Unfold `pi-comp` 0
   THEN Reduce 0
   THEN (GenConclTerm ⌜new-name(J)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `j' (-1)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN RepUR ``let`` 0
   THEN DVar `cB'
   THEN Auto) }

---

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)].
    (pi-comp(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{}  \_:(\mPi{}A  B)<rho>  o  iota\}
      {}\mrightarrow{}  lambda:cubical-path-0(Gamma;\mPi{}A  B;I;i;rho;phi;mu)
      {}\mrightarrow{}  J:fset(\mBbbN{})
      {}\mrightarrow{}  f:J  {}\mrightarrow{}  I
      {}\mrightarrow{}  u1:A(f((i1)(rho)))
      {}\mrightarrow{}  let  j  =  new-name(J)  in
              let  nu  =  pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u1;j)  in
              cubical-path-1(Gamma.A;B;J;j;(f,i=j(rho);nu);f(phi);
                                            pi-comp-app(Gamma;A;I;i;rho;phi;mu;J;f;j;nu)))


By

---

Latex:
(Auto
  THEN  RepeatFor  9  ((FunExt  THENA  Auto))
  THEN  Unfold  `pi-comp`  0
  THEN  Reduce  0
  THEN  (GenConclTerm  \mkleeneopen{}new-name(J)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `j'  (-1)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  RepUR  ``let``  0
  THEN  DVar  `cB'
  THEN  Auto)

---

Home Index