---

Step * of Lemma case-type_wf

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, phi ⊢ _}]. ∀[B:{Gamma, psi ⊢ _}].
  Gamma, (phi ∨ psi) ⊢ (if phi then A else B) supposing Gamma, (phi ∧ psi) ⊢ A = B
BY
{ (Auto THEN MemTypeCD THEN Auto) }

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

2
.....set predicate..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. Gamma, (phi ∧ psi) ⊢ A = B
⊢ let A,F = (if phi then A else B) 
  in (∀I:fset(ℕ). ∀a:Gamma, (phi ∨ psi)(I). ∀u:A I a.  ((F I I 1 a u) = u ∈ (A I a)))
     ∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:Gamma, (phi ∨ psi)(I). ∀u:A I a.
          ((F I K f ⋅ g a u) = (F J K g f(a) (F I J f a u)) ∈ (A K f ⋅ g(a))))

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Auto)

---

Home Index