---

Step * of Lemma case-type-1

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}].
  ∀[A:{Gamma ⊢ _}]. ∀[B:Top × Top].  Gamma ⊢ (if phi then A else B) = A supposing phi = 1(𝔽) ∈ {Gamma ⊢ _:𝔽}
BY
{ (InstLemma `case-type-same1` []
   THEN RepeatFor 2 (ParallelLast')
   THEN Intro
   THEN ParallelOp -2
   THEN (InstHyp [⌜0(𝔽)⌝] (-1)⋅ THENA Auto)
   THEN Intro) }

1
1. [Gamma] : CubicalSet{j}
2. [phi] : {Gamma ⊢ _:𝔽}
3. ∀[A:{Gamma, phi ⊢ _}]. ∀[psi:{Gamma ⊢ _:𝔽}]. ∀[B:{Gamma, psi ⊢ _}].  Gamma, phi ⊢ (if phi then A else B) = A
4. [%] : phi = 1(𝔽) ∈ {Gamma ⊢ _:𝔽}
5. [A] : {Gamma ⊢ _}
6. ∀[psi:{Gamma ⊢ _:𝔽}]. ∀[B:{Gamma, psi ⊢ _}].  Gamma, phi ⊢ (if phi then A else B) = A
7. ∀[B:{Gamma, 0(𝔽) ⊢ _}]. Gamma, phi ⊢ (if phi then A else B) = A
8. [B] : Top × Top
⊢ Gamma ⊢ (if phi then A else B) = A

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].
    \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[B:Top  \mtimes{}  Top].    Gamma  \mvdash{}  (if  phi  then  A  else  B)  =  A  supposing  phi  =  1(\mBbbF{})


By

---

Latex:
(InstLemma  `case-type-same1`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Intro
  THEN  ParallelOp  -2
  THEN  (InstHyp  [\mkleeneopen{}0(\mBbbF{})\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Intro)

---

Home Index