---

Step * of Lemma case-type-comp-true-false

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}].
  (∀[A:{Gamma ⊢ _}]. ∀[cA:Gamma ⊢ Compositon(A)]. ∀[B:{Gamma, psi ⊢ _}]. ∀[cB:Gamma, psi ⊢ Compositon(B)].
     (case-type-comp(Gamma; phi; psi; A; B; cA; cB) = cA ∈ Gamma ⊢ Compositon(A))) supposing 
     (Gamma ⊢ (1(𝔽) ⇒ phi) and 
     Gamma ⊢ (psi ⇒ 0(𝔽)))
BY
{ (Intros THEN Assert ⌜case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma ⊢ Compositon(A)⌝⋅) }

1
.....assertion..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. Gamma ⊢ (psi ⇒ 0(𝔽))
5. Gamma ⊢ (1(𝔽) ⇒ phi)
6. A : {Gamma ⊢ _}
7. cA : Gamma ⊢ Compositon(A)
8. B : {Gamma, psi ⊢ _}
9. cB : Gamma, psi ⊢ Compositon(B)
⊢ case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma ⊢ Compositon(A)

2
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. Gamma ⊢ (psi ⇒ 0(𝔽))
5. Gamma ⊢ (1(𝔽) ⇒ phi)
6. A : {Gamma ⊢ _}
7. cA : Gamma ⊢ Compositon(A)
8. B : {Gamma, psi ⊢ _}
9. cB : Gamma, psi ⊢ Compositon(B)
10. case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma ⊢ Compositon(A)
⊢ case-type-comp(Gamma; phi; psi; A; B; cA; cB) = cA ∈ Gamma ⊢ Compositon(A)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi,psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].
    (\mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  Compositon(A)].  \mforall{}[B:\{Gamma,  psi  \mvdash{}  \_\}].
      \mforall{}[cB:Gamma,  psi  \mvdash{}  Compositon(B)].
          (case-type-comp(Gamma;  phi;  psi;  A;  B;  cA;  cB)  =  cA))  supposing 
          (Gamma  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  phi)  and 
          Gamma  \mvdash{}  (psi  {}\mRightarrow{}  0(\mBbbF{})))


By

---

Latex:
(Intros  THEN  Assert  \mkleeneopen{}case-type-comp(Gamma;  phi;  psi;  A;  B;  cA;  cB)  \mmember{}  Gamma  \mvdash{}  Compositon(A)\mkleeneclose{}\mcdot{})

---

Home Index