---

Step * of Lemma same-cubical-type-by-cases

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A,B:{Gamma, (phi ∨ psi) ⊢ _}].
  (Gamma, (phi ∨ psi) ⊢ A = B) supposing (Gamma, phi ⊢ A = B and Gamma, psi ⊢ A = B)
BY
{ (RepeatFor 5 (Intro)
   THEN RepeatFor 2 ((D 0
                      THEN Try ((MemCD'
                                 THEN DoSubsume
                                 THEN (Try ((BLemma `context-subset-subtype-or2` THEN Auto))
                                       THEN Try ((BLemma `context-subset-subtype-or` THEN Auto))
                                       )
                                 THEN Auto))
                      ))
   THEN All (Unfold `same-cubical-type`)
   THEN (BLemma `cubical-type-equal3` THENA Auto)
   THEN Intros
   THEN OnMaybeHyp 9 (\h. (RepUR ``context-subset`` h
                           THEN D h
                           THEN RepUR ``face-or cubical-term-at`` h+1
                           THEN Fold `cubical-term-at` (h+1)
                           THEN (RWO "face_lattice-1-join-irreducible" (h+1) THENA Auto)
                           THEN D h+1))) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, (phi ∨ psi) ⊢ _}
5. B : {Gamma, (phi ∨ psi) ⊢ _}
6. A = B ∈ {Gamma, psi ⊢ _}
7. A = B ∈ {Gamma, phi ⊢ _}
8. I : fset(ℕ)
9. rho : Gamma(I)
10. phi(rho) = 1 ∈ Point(face_lattice(I))
⊢ A(rho) = B(rho) ∈ Type

2
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, (phi ∨ psi) ⊢ _}
5. B : {Gamma, (phi ∨ psi) ⊢ _}
6. A = B ∈ {Gamma, psi ⊢ _}
7. A = B ∈ {Gamma, phi ⊢ _}
8. I : fset(ℕ)
9. rho : Gamma(I)
10. psi(rho) = 1 ∈ Point(face_lattice(I))
⊢ A(rho) = B(rho) ∈ Type

3
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, (phi ∨ psi) ⊢ _}
5. B : {Gamma, (phi ∨ psi) ⊢ _}
6. A = B ∈ {Gamma, psi ⊢ _}
7. A = B ∈ {Gamma, phi ⊢ _}
8. I : fset(ℕ)
9. rho : Gamma(I)
10. phi(rho) = 1 ∈ Point(face_lattice(I))
11. J : fset(ℕ)
12. f : J ⟶ I
13. u : A(rho)
⊢ (u rho f) = (u rho f) ∈ A(f(rho))

4
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, (phi ∨ psi) ⊢ _}
5. B : {Gamma, (phi ∨ psi) ⊢ _}
6. A = B ∈ {Gamma, psi ⊢ _}
7. A = B ∈ {Gamma, phi ⊢ _}
8. I : fset(ℕ)
9. rho : Gamma(I)
10. psi(rho) = 1 ∈ Point(face_lattice(I))
11. J : fset(ℕ)
12. f : J ⟶ I
13. u : A(rho)
⊢ (u rho f) = (u rho f) ∈ A(f(rho))

---

Latex:

---

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


By

---

Latex:
(RepeatFor  5  (Intro)
  THEN  RepeatFor  2  ((D  0
                                        THEN  Try  ((MemCD'
                                                              THEN  DoSubsume
                                                              THEN  (Try  ((BLemma  `context-subset-subtype-or2`  THEN  Auto))
                                                                          THEN  Try  ((BLemma  `context-subset-subtype-or`  THEN  Auto))
                                                                          )
                                                              THEN  Auto))
                                        ))
  THEN  All  (Unfold  `same-cubical-type`)
  THEN  (BLemma  `cubical-type-equal3`  THENA  Auto)
  THEN  Intros
  THEN  OnMaybeHyp  9  (\mbackslash{}h.  (RepUR  ``context-subset``  h
                                                  THEN  D  h
                                                  THEN  RepUR  ``face-or  cubical-term-at``  h+1
                                                  THEN  Fold  `cubical-term-at`  (h+1)
                                                  THEN  (RWO  "face\_lattice-1-join-irreducible"  (h+1)  THENA  Auto)
                                                  THEN  D  h+1)))

---

Home Index