---

Step * of Lemma case-type-same2

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, phi ⊢ _}]. ∀[psi:{Gamma ⊢ _:𝔽}]. ∀[B:{Gamma, psi ⊢ _}].
  Gamma, psi ⊢ (if phi then A else B) = B supposing Gamma, (phi ∧ psi) ⊢ A = B
BY
{ ((Auto
    THEN (Assert Gamma, psi ⊢ (if phi then A else B) BY
                (DoSubsume THENL [Auto; (BLemma `context-subset-subtype-or2` THEN Auto)]))
    )
   THEN Unfold `same-cubical-type` 0
   THEN (BLemma `cubical-type-equal2` THENW Auto)
   THEN Thin (-1)) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma, phi ⊢ _}
4. psi : {Gamma ⊢ _:𝔽}
5. B : {Gamma, psi ⊢ _}
6. Gamma, (phi ∧ psi) ⊢ A = B
⊢ (if phi then A else B)
= B
∈ (A:I:fset(ℕ) ⟶ Gamma, psi(I) ⟶ Type × (I:fset(ℕ)
                                          ⟶ J:fset(ℕ)
                                          ⟶ f:J ⟶ I
                                          ⟶ a:Gamma, psi(I)
                                          ⟶ (A I a)
                                          ⟶ (A J f(a))))

---

Latex:

---

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


By

---

Latex:
((Auto
    THEN  (Assert  Gamma,  psi  \mvdash{}  (if  phi  then  A  else  B)  BY
                            (DoSubsume  THENL  [Auto;  (BLemma  `context-subset-subtype-or2`  THEN  Auto)]))
    )
  THEN  Unfold  `same-cubical-type`  0
  THEN  (BLemma  `cubical-type-equal2`  THENW  Auto)
  THEN  Thin  (-1))

---

Home Index