---

Step * 1 of Lemma case-type-comp_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(𝕀)]]}
⊢ (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}
BY
{ (((CubicalTermEqual THENW Auto)
    THENA (Try (((GenConclTerm ⌜case-type-comp(Gamma; phi; psi; A; B; cA; cB) H sigma phi@0 u a0⌝⋅ THENA Auto)
                 THEN D -2
                 THEN Auto))
           THEN Auto
           )
    )
   THEN RenameVar `alpha' (-1)
   THEN PromoteHyp (-2) (-7)
   THEN PromoteHyp (-1) (-6)) }

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. I : fset(ℕ)
15. alpha : K(I)
16. tau : K j⟶ H
17. sigma : H.𝕀 j⟶ Gamma, (phi ∨ psi)
18. phi@0 : {H ⊢ _:𝔽}
19. u : {H, phi@0.𝕀 ⊢ _:((if phi then A else B))sigma}
20. 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 I alpha)
= (case-type-comp(Gamma; phi; psi; A; B; cA; cB) K sigma o tau+ (phi@0)tau (u)tau+ (a0)tau I alpha)
∈ ((((if phi then A else B))sigma)[1(𝕀)])tau(alpha)

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  psi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
4.  A  :  \{Gamma,  phi  \mvdash{}  \_\}
5.  B  :  \{Gamma,  psi  \mvdash{}  \_\}
6.  cA  :  Gamma,  phi  \mvdash{}  Compositon(A)
7.  cB  :  Gamma,  psi  \mvdash{}  Compositon(B)
8.  Gamma,  (phi  \mwedge{}  psi)  \mvdash{}  A  =  B
9.  compatible-composition\{j:l,  i:l\}(Gamma;  phi;  psi;  A;  B;  cA;  cB)
10.  Gamma,  (phi  \mvee{}  psi)  \mvdash{}  (if  phi  then  A  else  B)
11.  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))
12.  H  :  CubicalSet\{j\}
13.  K  :  CubicalSet\{j\}
14.  tau  :  K  j{}\mrightarrow{}  H
15.  sigma  :  H.\mBbbI{}  j{}\mrightarrow{}  Gamma,  (phi  \mvee{}  psi)
16.  phi@0  :  \{H  \mvdash{}  \_:\mBbbF{}\}
17.  u  :  \{H,  phi@0.\mBbbI{}  \mvdash{}  \_:((if  phi  then  A  else  B))sigma\}
18.  a0  :  \{H  \mvdash{}  \_:(((if  phi  then  A  else  B))sigma)[0(\mBbbI{})][phi@0  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}
\mvdash{}  (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)


By

---

Latex:
(((CubicalTermEqual  THENW  Auto)
    THENA  (Try  (((GenConclTerm  \mkleeneopen{}case-type-comp(Gamma;  phi;  psi;  A;  B;  cA;  cB)  H  sigma  phi@0  u  a0\mkleeneclose{}\mcdot{}
                                THENA  Auto
                                )
                              THEN  D  -2
                              THEN  Auto))
                  THEN  Auto
                  )
    )
  THEN  RenameVar  `alpha'  (-1)
  THEN  PromoteHyp  (-2)  (-7)
  THEN  PromoteHyp  (-1)  (-6))

---

Home Index