---

Step * of Lemma case-type-comp_wf1

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)
   ∈ composition-function{j:l,i:l}(Gamma, (phi ∨ psi);(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 Unhide
   THEN (InstLemma `case-type_wf` [⌜Gamma⌝;⌜phi⌝;⌜psi⌝;⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN RepUR ``case-type-comp composition-function`` 0
   THEN RepeatFor 3 (((FunExt THENA Auto) THEN Reduce 0))
   THEN RenameVar `chi' (-1)
   THEN (Assert H.𝕀 ⊢ ((1(𝔽))sigma ⇒ ((phi)sigma ∨ (psi)sigma)) BY
               ((RWO "csm-face-or<" 0 THENA Auto)
                THEN BLemma `csm-face-term-implies`
                THEN Auto
                THEN RepeatFor 3 ((D 0 THENA Auto))
                THEN RepUR ``context-subset`` -2
                THEN D -2
                THEN Auto))
   THEN (RWW "csm-face-1" (-1) THENA Auto)
   THEN (Assert ⌜(∀ (phi)sigma) ∈ {H ⊢ _:𝔽}⌝ BY
               Auto)
   THEN (Assert ⌜(∀ (psi)sigma) ∈ {H ⊢ _:𝔽}⌝ BY
               Auto)
   THEN (Assert H.𝕀, ((phi)sigma ∧ (psi)sigma) ⊢ (A)sigma = (B)sigma BY
               ((InstLemma `csm-same-cubical-type` [⌜Gamma, (phi ∧ psi)⌝;⌜A⌝;⌜B⌝]⋅ THENA Auto)
                THEN (BHyp -1 THENL [Auto; (RWO "csm-face-and<" 0 THEN Auto)])
                ))
   THEN ((Assert H.𝕀 ⊢ ((if phi then A else B))sigma BY
                (MemCD THEN Auto))
         THEN (Assert H, chi.𝕀 ⊢ ((if phi then A else B))sigma BY
                     (SubsumeC ⌜{H.𝕀 ⊢ _}⌝⋅ THEN Auto))
         )
   THEN RepeatFor 2 (((FunExt THENA Auto) THEN Reduce 0))) }

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. H : CubicalSet{j}
12. sigma : H.𝕀 j⟶ Gamma, (phi ∨ psi)
13. chi : {H ⊢ _:𝔽}
14. H.𝕀 ⊢ (1(𝔽) ⇒ ((phi)sigma ∨ (psi)sigma))
15. (∀ (phi)sigma) ∈ {H ⊢ _:𝔽}
16. (∀ (psi)sigma) ∈ {H ⊢ _:𝔽}
17. H.𝕀, ((phi)sigma ∧ (psi)sigma) ⊢ (A)sigma = (B)sigma
18. H.𝕀 ⊢ ((if phi then A else B))sigma
19. H, chi.𝕀 ⊢ ((if phi then A else B))sigma
20. u : {H, chi.𝕀 ⊢ _:((if phi then A else B))sigma}
21. a0 : {H ⊢ _:(((if phi then A else B))sigma)[0(𝕀)][chi |⟶ (u)[0(𝕀)]]}
⊢ (cA H, (∀ (phi)sigma) sigma chi u a0 ∨ cB H, (∀ (psi)sigma) sigma chi u a0)
  ∈ {H ⊢ _:(((if phi then A else B))sigma)[1(𝕀)][chi |⟶ (u)[1(𝕀)]]}

---

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{}  composition-function\{j:l,i:l\}(Gamma,  (phi  \mvee{}  psi);(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  Unhide
  THEN  (InstLemma  `case-type\_wf`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}psi\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``case-type-comp  composition-function``  0
  THEN  RepeatFor  3  (((FunExt  THENA  Auto)  THEN  Reduce  0))
  THEN  RenameVar  `chi'  (-1)
  THEN  (Assert  H.\mBbbI{}  \mvdash{}  ((1(\mBbbF{}))sigma  {}\mRightarrow{}  ((phi)sigma  \mvee{}  (psi)sigma))  BY
                          ((RWO  "csm-face-or<"  0  THENA  Auto)
                            THEN  BLemma  `csm-face-term-implies`
                            THEN  Auto
                            THEN  RepeatFor  3  ((D  0  THENA  Auto))
                            THEN  RepUR  ``context-subset``  -2
                            THEN  D  -2
                            THEN  Auto))
  THEN  (RWW  "csm-face-1"  (-1)  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(\mforall{}  (phi)sigma)  \mmember{}  \{H  \mvdash{}  \_:\mBbbF{}\}\mkleeneclose{}  BY
                          Auto)
  THEN  (Assert  \mkleeneopen{}(\mforall{}  (psi)sigma)  \mmember{}  \{H  \mvdash{}  \_:\mBbbF{}\}\mkleeneclose{}  BY
                          Auto)
  THEN  (Assert  H.\mBbbI{},  ((phi)sigma  \mwedge{}  (psi)sigma)  \mvdash{}  (A)sigma  =  (B)sigma  BY
                          ((InstLemma  `csm-same-cubical-type`  [\mkleeneopen{}Gamma,  (phi  \mwedge{}  psi)\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (BHyp  -1  THENL  [Auto;  (RWO  "csm-face-and<"  0  THEN  Auto)])
                            ))
  THEN  ((Assert  H.\mBbbI{}  \mvdash{}  ((if  phi  then  A  else  B))sigma  BY
                            (MemCD  THEN  Auto))
              THEN  (Assert  H,  chi.\mBbbI{}  \mvdash{}  ((if  phi  then  A  else  B))sigma  BY
                                      (SubsumeC  \mkleeneopen{}\{H.\mBbbI{}  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto))
              )
  THEN  RepeatFor  2  (((FunExt  THENA  Auto)  THEN  Reduce  0)))

---

Home Index