---

Step * 2 of Lemma case-type_wf

.....set predicate..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. Gamma, (phi ∧ psi) ⊢ A = B
⊢ let A,F = (if phi then A else B) 
  in (∀I:fset(ℕ). ∀a:Gamma, (phi ∨ psi)(I). ∀u:A I a.  ((F I I 1 a u) = u ∈ (A I a)))
     ∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:Gamma, (phi ∨ psi)(I). ∀u:A I a.
          ((F I K f ⋅ g a u) = (F J K g f(a) (F I J f a u)) ∈ (A K f ⋅ g(a))))
BY
{ (RepUR ``case-type`` 0
   THEN D 0
   THEN Intros
   THEN RenameVar `rho' (-2)
   THEN (Assert rho ∈ Gamma, (phi ∨ psi)(I) BY
               Auto)
   THEN Guard (-1)
   THEN (RepUR ``context-subset`` -3 THEN D -3)
   THEN RepUR ``face-or cubical-term-at`` -3
   THEN Fold `cubical-term-at` (-3)
   THEN (RWO "face_lattice-1-join-irreducible" (-3) THENA Auto)
   THEN (RepUR ``case-cube`` -2 THEN RepUR ``case-cube`` 0)
   THEN (Assert ⌜𝔽(rho) ⊆r Point(face_lattice(I))⌝⋅ THENA (RWO "face-type-at" 0 THEN Auto))
   THEN Try ((Assert ⌜𝔽(f(rho)) ⊆r Point(face_lattice(J))⌝⋅ THENA (RWO "face-type-at" 0 THEN Auto)))
   THEN (BoolCase ⌜(phi(rho)==1)⌝⋅ THENA Auto)) }

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

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

3
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. Gamma, (phi ∧ psi) ⊢ A = B
7. I : fset(ℕ)
8. J : fset(ℕ)
9. K : fset(ℕ)
10. f : J ⟶ I
11. g : K ⟶ J
12. rho : Gamma(I)
13. (phi(rho) = 1 ∈ Point(face_lattice(I))) ∨ (psi(rho) = 1 ∈ Point(face_lattice(I)))
14. u : if (phi(rho)==1) then A(rho) else B(rho) fi 
15. {rho ∈ Gamma, (phi ∨ psi)(I)}
16. 𝔽(rho) ⊆r Point(face_lattice(I))
17. 𝔽(f(rho)) ⊆r Point(face_lattice(J))
18. phi(rho) = 1 ∈ Point(face_lattice(I))
⊢ (u rho f ⋅ g)
= if (phi(f(rho))==1) then ((u rho f) f(rho) g) else ((u rho f) f(rho) g) fi 
∈ if (phi(f ⋅ g(rho))==1) then A(f ⋅ g(rho)) else B(f ⋅ g(rho)) fi 

4
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. Gamma, (phi ∧ psi) ⊢ A = B
7. I : fset(ℕ)
8. J : fset(ℕ)
9. K : fset(ℕ)
10. f : J ⟶ I
11. g : K ⟶ J
12. rho : Gamma(I)
13. ¬(phi(rho) = 1 ∈ Point(face_lattice(I)))
14. (phi(rho) = 1 ∈ Point(face_lattice(I))) ∨ (psi(rho) = 1 ∈ Point(face_lattice(I)))
15. u : B(rho)
16. {rho ∈ Gamma, (phi ∨ psi)(I)}
17. 𝔽(rho) ⊆r Point(face_lattice(I))
18. 𝔽(f(rho)) ⊆r Point(face_lattice(J))
⊢ (u rho f ⋅ g)
= if (phi(f(rho))==1) then ((u rho f) f(rho) g) else ((u rho f) f(rho) g) fi 
∈ if (phi(f ⋅ g(rho))==1) then A(f ⋅ g(rho)) else B(f ⋅ g(rho)) fi 

---

Latex:

---

Latex:
.....set  predicate..... 
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.  Gamma,  (phi  \mwedge{}  psi)  \mvdash{}  A  =  B
\mvdash{}  let  A,F  =  (if  phi  then  A  else  B) 
    in  (\mforall{}I:fset(\mBbbN{}).  \mforall{}a:Gamma,  (phi  \mvee{}  psi)(I).  \mforall{}u:A  I  a.    ((F  I  I  1  a  u)  =  u))
          \mwedge{}  (\mforall{}I,J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}a:Gamma,  (phi  \mvee{}  psi)(I).  \mforall{}u:A  I  a.
                    ((F  I  K  f  \mcdot{}  g  a  u)  =  (F  J  K  g  f(a)  (F  I  J  f  a  u))))


By

---

Latex:
(RepUR  ``case-type``  0
  THEN  D  0
  THEN  Intros
  THEN  RenameVar  `rho'  (-2)
  THEN  (Assert  rho  \mmember{}  Gamma,  (phi  \mvee{}  psi)(I)  BY
                          Auto)
  THEN  Guard  (-1)
  THEN  (RepUR  ``context-subset``  -3  THEN  D  -3)
  THEN  RepUR  ``face-or  cubical-term-at``  -3
  THEN  Fold  `cubical-term-at`  (-3)
  THEN  (RWO  "face\_lattice-1-join-irreducible"  (-3)  THENA  Auto)
  THEN  (RepUR  ``case-cube``  -2  THEN  RepUR  ``case-cube``  0)
  THEN  (Assert  \mkleeneopen{}\mBbbF{}(rho)  \msubseteq{}r  Point(face\_lattice(I))\mkleeneclose{}\mcdot{}  THENA  (RWO  "face-type-at"  0  THEN  Auto))
  THEN  Try  ((Assert  \mkleeneopen{}\mBbbF{}(f(rho))  \msubseteq{}r  Point(face\_lattice(J))\mkleeneclose{}\mcdot{}  THENA  (RWO  "face-type-at"  0  THEN  Auto)))
  THEN  (BoolCase  \mkleeneopen{}(phi(rho)==1)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index