---

Step * of Lemma face-forall-implies-1

No Annotations
∀[H:j⊢]. ∀[phi:{H.𝕀 ⊢ _:𝔽}]. ∀[X:Top].  H ⊢ ((∀ phi) ⇒ (phi)[1(𝕀)])
BY
{ ((Intros THEN (Subst' [1(𝕀)] ~ [1(𝕀)] 0 THENA (CsmUnfolding THEN Auto)))
   THEN (D 0 THENA Auto)
   THEN Intros
   THEN (InstLemma `nc-1_wf` [⌜I⌝;⌜new-name(I)⌝]⋅ THENA Auto)
   THEN (Assert <new-name(I)> ∈ 𝕀(s(rho)) BY
               ((RWO "interval-type-at" 0 THENA Auto) THEN RepUR ``interval-presheaf`` 0 THEN Auto))
   THEN (Assert ⌜(phi(<s(rho), <new-name(I)>>))<(new-name(I)1)> = phi(<rho, 1>) ∈ Point(face_lattice(I))⌝⋅
         THENA ((InstLemma `cubical-term-at-morph` [⌜H.𝕀⌝;⌜𝔽⌝;⌜phi⌝;⌜I+new-name(I)⌝;⌜(s(rho);<new-name(I)>)⌝;⌜I⌝;
                 ⌜(new-name(I)1)⌝]⋅
                 THENA Auto
                 )
                THEN (RWO "face-type-at" (-1) THENA Auto)
                THEN (RWO "face-type-ap-morph" (-1) THENA Auto)
                THEN RepUR ``cube-context-adjoin cc-adjoin-cube`` -1
                THEN NthHypEq (-1)
                THEN EqCDA
                THEN EqCDA
                THEN RepUR ``cube-context-adjoin`` 0
                THEN EqCDA)
         )) }

1
.....subterm..... T:t
1:n
1. H : CubicalSet{j}
2. phi : {H.𝕀 ⊢ _:𝔽}
3. X : Top
4. I : fset(ℕ)
5. rho : H(I)
6. (∀ phi)(rho) = 1 ∈ Point(face_lattice(I))
7. (new-name(I)1) ∈ I ⟶ I+new-name(I)
8. <new-name(I)> ∈ 𝕀(s(rho))
9. (phi(<s(rho), <new-name(I)>>))<(new-name(I)1)>
= phi(<(new-name(I)1)(s(rho)), (<new-name(I)> s(rho) (new-name(I)1))>)
∈ Point(face_lattice(I))
⊢ rho = (new-name(I)1)(s(rho)) ∈ H(I)

2
.....subterm..... T:t
2:n
1. H : CubicalSet{j}
2. phi : {H.𝕀 ⊢ _:𝔽}
3. X : Top
4. I : fset(ℕ)
5. rho : H(I)
6. (∀ phi)(rho) = 1 ∈ Point(face_lattice(I))
7. (new-name(I)1) ∈ I ⟶ I+new-name(I)
8. <new-name(I)> ∈ 𝕀(s(rho))
9. (phi(<s(rho), <new-name(I)>>))<(new-name(I)1)>
= phi(<(new-name(I)1)(s(rho)), (<new-name(I)> s(rho) (new-name(I)1))>)
∈ Point(face_lattice(I))
⊢ 1 = (<new-name(I)> s(rho) (new-name(I)1)) ∈ 𝕀(rho)

3
1. H : CubicalSet{j}
2. phi : {H.𝕀 ⊢ _:𝔽}
3. X : Top
4. I : fset(ℕ)
5. rho : H(I)
6. (∀ phi)(rho) = 1 ∈ Point(face_lattice(I))
7. (new-name(I)1) ∈ I ⟶ I+new-name(I)
8. <new-name(I)> ∈ 𝕀(s(rho))
9. (phi(<s(rho), <new-name(I)>>))<(new-name(I)1)> = phi(<rho, 1>) ∈ Point(face_lattice(I))
⊢ (phi)[1(𝕀)](rho) = 1 ∈ Point(face_lattice(I))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[phi:\{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[X:Top].    H  \mvdash{}  ((\mforall{}  phi)  {}\mRightarrow{}  (phi)[1(\mBbbI{})])


By

---

Latex:
((Intros  THEN  (Subst'  [1(\mBbbI{})]  \msim{}  [1(\mBbbI{})]  0  THENA  (CsmUnfolding  THEN  Auto)))
  THEN  (D  0  THENA  Auto)
  THEN  Intros
  THEN  (InstLemma  `nc-1\_wf`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}new-name(I)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  <new-name(I)>  \mmember{}  \mBbbI{}(s(rho))  BY
                          ((RWO  "interval-type-at"  0  THENA  Auto)  THEN  RepUR  ``interval-presheaf``  0  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}(phi(<s(rho),  <new-name(I)>>))<(new-name(I)1)>  =  phi(<rho,  1>)\mkleeneclose{}\mcdot{}
              THENA  ((InstLemma  `cubical-term-at-morph`  [\mkleeneopen{}H.\mBbbI{}\mkleeneclose{};\mkleeneopen{}\mBbbF{}\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}I+new-name(I)\mkleeneclose{};
                              \mkleeneopen{}(s(rho);<new-name(I)>)\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}(new-name(I)1)\mkleeneclose{}]\mcdot{}
                              THENA  Auto
                              )
                            THEN  (RWO  "face-type-at"  (-1)  THENA  Auto)
                            THEN  (RWO  "face-type-ap-morph"  (-1)  THENA  Auto)
                            THEN  RepUR  ``cube-context-adjoin  cc-adjoin-cube``  -1
                            THEN  NthHypEq  (-1)
                            THEN  EqCDA
                            THEN  EqCDA
                            THEN  RepUR  ``cube-context-adjoin``  0
                            THEN  EqCDA)
              ))

---

Home Index