---

Step * of Lemma case-type-comp_wf

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, phi ⊢ _}]. ∀[B:{Gamma, psi ⊢ _}]. ∀[cA:Gamma, phi ⊢ Compositon(A)].
∀[cB:Gamma, psi ⊢ Compositon(B)].
  (case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then A else B))) supposing 
     (compatible-composition{j:l, i:l}(Gamma; phi; psi; A; B; cA; cB) and 
     Gamma, (phi ∧ psi) ⊢ A = B)
BY
{ (Intros
   THEN (InstLemma `case-type_wf` [⌜Gamma⌝;⌜phi⌝;⌜psi⌝;⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN (Assert case-type-comp(Gamma; phi; psi; A; B; cA; cB)
                ∈ composition-function{j:l,i:l}(Gamma, (phi ∨ psi);(if phi then A else B)) BY
               Auto)
   THEN MemTypeCD
   THEN Auto
   THEN (D 0 THENW Auto)
   THEN Intros
   THEN (EqTypeCD ORELSE (GenConclTerm ⌜((if phi then A else B))sigma⌝⋅ THEN Auto))) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. cA : Gamma, phi ⊢ Compositon(A)
7. cB : Gamma, psi ⊢ Compositon(B)
8. Gamma, (phi ∧ psi) ⊢ A = B
9. compatible-composition{j:l, i:l}(Gamma; phi; psi; A; B; cA; cB)
10. Gamma, (phi ∨ psi) ⊢ (if phi then A else B)
11. case-type-comp(Gamma; phi; psi; A; B; cA; cB)
    ∈ composition-function{j:l,i:l}(Gamma, (phi ∨ psi);(if phi then A else B))
12. H : CubicalSet{j}
13. K : CubicalSet{j}
14. tau : K j⟶ H
15. sigma : H.𝕀 j⟶ Gamma, (phi ∨ psi)
16. phi@0 : {H ⊢ _:𝔽}
17. u : {H, phi@0.𝕀 ⊢ _:((if phi then A else B))sigma}
18. a0 : {H ⊢ _:(((if phi then A else B))sigma)[0(𝕀)][phi@0 |⟶ (u)[0(𝕀)]]}
⊢ (case-type-comp(Gamma; phi; psi; A; B; cA; cB) H sigma phi@0 u a0)tau
= (case-type-comp(Gamma; phi; psi; A; B; cA; cB) K sigma o tau+ (phi@0)tau (u)tau+ (a0)tau)
∈ {K ⊢ _:((((if phi then A else B))sigma)[1(𝕀)])tau}

2
.....set predicate..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. cA : Gamma, phi ⊢ Compositon(A)
7. cB : Gamma, psi ⊢ Compositon(B)
8. Gamma, (phi ∧ psi) ⊢ A = B
9. compatible-composition{j:l, i:l}(Gamma; phi; psi; A; B; cA; cB)
10. Gamma, (phi ∨ psi) ⊢ (if phi then A else B)
11. case-type-comp(Gamma; phi; psi; A; B; cA; cB)
    ∈ composition-function{j:l,i:l}(Gamma, (phi ∨ psi);(if phi then A else B))
12. H : CubicalSet{j}
13. K : CubicalSet{j}
14. tau : K j⟶ H
15. sigma : H.𝕀 j⟶ Gamma, (phi ∨ psi)
16. phi@0 : {H ⊢ _:𝔽}
17. u : {H, phi@0.𝕀 ⊢ _:((if phi then A else B))sigma}
18. a0 : {H ⊢ _:(((if phi then A else B))sigma)[0(𝕀)][phi@0 |⟶ (u)[0(𝕀)]]}
⊢ ((u)[1(𝕀)])tau
= (case-type-comp(Gamma; phi; psi; A; B; cA; cB) H sigma phi@0 u a0)tau
∈ {K, (phi@0)tau ⊢ _:((((if phi then A else B))sigma)[1(𝕀)])tau}

3
.....wf..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. cA : Gamma, phi ⊢ Compositon(A)
7. cB : Gamma, psi ⊢ Compositon(B)
8. Gamma, (phi ∧ psi) ⊢ A = B
9. compatible-composition{j:l, i:l}(Gamma; phi; psi; A; B; cA; cB)
10. Gamma, (phi ∨ psi) ⊢ (if phi then A else B)
11. case-type-comp(Gamma; phi; psi; A; B; cA; cB)
    ∈ composition-function{j:l,i:l}(Gamma, (phi ∨ psi);(if phi then A else B))
12. H : CubicalSet{j}
13. K : CubicalSet{j}
14. tau : K j⟶ H
15. sigma : H.𝕀 j⟶ Gamma, (phi ∨ psi)
16. phi@0 : {H ⊢ _:𝔽}
17. u : {H, phi@0.𝕀 ⊢ _:((if phi then A else B))sigma}
18. a0 : {H ⊢ _:(((if phi then A else B))sigma)[0(𝕀)][phi@0 |⟶ (u)[0(𝕀)]]}
19. a : {K ⊢ _:((((if phi then A else B))sigma)[1(𝕀)])tau}
⊢ istype(((u)[1(𝕀)])tau = a ∈ {K, (phi@0)tau ⊢ _:((((if phi then A else B))sigma)[1(𝕀)])tau})

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi,psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma,  phi  \mvdash{}  \_\}].  \mforall{}[B:\{Gamma,  psi  \mvdash{}  \_\}].
\mforall{}[cA:Gamma,  phi  \mvdash{}  Compositon(A)].  \mforall{}[cB:Gamma,  psi  \mvdash{}  Compositon(B)].
    (case-type-comp(Gamma;  phi;  psi;  A;  B;  cA;  cB)
      \mmember{}  Gamma,  (phi  \mvee{}  psi)  \mvdash{}  Compositon((if  phi  then  A  else  B)))  supposing 
          (compatible-composition\{j:l,  i:l\}(Gamma;  phi;  psi;  A;  B;  cA;  cB)  and 
          Gamma,  (phi  \mwedge{}  psi)  \mvdash{}  A  =  B)


By

---

Latex:
(Intros
  THEN  (InstLemma  `case-type\_wf`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}psi\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  case-type-comp(Gamma;  phi;  psi;  A;  B;  cA;  cB)
                            \mmember{}  composition-function\{j:l,i:l\}(Gamma,  (phi  \mvee{}  psi);(if  phi  then  A  else  B))  BY
                          Auto)
  THEN  MemTypeCD
  THEN  Auto
  THEN  (D  0  THENW  Auto)
  THEN  Intros
  THEN  (EqTypeCD  ORELSE  (GenConclTerm  \mkleeneopen{}((if  phi  then  A  else  B))sigma\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index