---

Step * of Lemma case-type-same1

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, phi ⊢ _}]. ∀[psi:{Gamma ⊢ _:𝔽}]. ∀[B:{Gamma, psi ⊢ _}].
  Gamma, phi ⊢ (if phi then A else B) = A
BY
{ (Auto THEN Unfold `same-cubical-type` 0 THEN (Symmetry THEN BLemma `cubical-type-equal`) THEN Try (Trivial)) }

1
.....wf..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma, phi ⊢ _}
4. psi : {Gamma ⊢ _:𝔽}
5. B : {Gamma, psi ⊢ _}
⊢ Gamma, phi j⊢

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

3
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma, phi ⊢ _}
4. psi : {Gamma ⊢ _:𝔽}
5. B : {Gamma, psi ⊢ _}
⊢ A
= (if phi then A else B)
∈ (A:I:fset(ℕ) ⟶ Gamma, phi(I) ⟶ Type × (I:fset(ℕ)
                                          ⟶ J:fset(ℕ)
                                          ⟶ f:J ⟶ I
                                          ⟶ a:Gamma, phi(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,  phi  \mvdash{}  (if  phi  then  A  else  B)  =  A


By

---

Latex:
(Auto
  THEN  Unfold  `same-cubical-type`  0
  THEN  (Symmetry  THEN  BLemma  `cubical-type-equal`)
  THEN  Try  (Trivial))

---

Home Index