---

Step * of Lemma universe-path-type-lemma-1

No Annotations
∀G:j⊢. ∀A,B:{G ⊢ _:c𝕌}. ∀p:{G ⊢ _:(Path_c𝕌 A B)}. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀v:G(I+new-name(I)).
  (universe-type(B;I+new-name(I);v)((new-name(I)1) ⋅ f)
  = fst((p(v) I+new-name(I) 1 <new-name(I)>))((new-name(I)1) ⋅ f)
  ∈ Type)
BY
{ (Intros⋅
   THEN (InstLemma `cubical-term-at_wf` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜(Path_c𝕌 A B)⌝;⌜p⌝;⌜I+new-name(I)⌝;⌜v⌝]⋅ THENA Auto)
   THEN DupHyp (-1)
   THEN (RWO "path-type-at" (-1) THENA Auto)
   THEN ((MemTypeHD (-1) THENA (D -1 THEN Auto)) THEN Fold `member` (-2))
   THEN (MemTypeHD (-2) THENA (D -1 THEN Auto))
   THEN Fold `member` (-3)
   THEN RepUR ``cubical-universe closed-cubical-universe`` -1
   THEN RepUR ``cubical-universe closed-cubical-universe`` -2
   THEN RepUR ``cubical-universe closed-cubical-universe`` -3
   THEN RepUR ``closed-type-to-type csm-fibrant-type`` -1
   THEN RepUR ``closed-type-to-type csm-fibrant-type`` -2
   THEN RepUR ``closed-type-to-type csm-fibrant-type`` -3
   THEN D -1
   THEN Thin (-2)
   ⋅) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. p : {G ⊢ _:(Path_c𝕌 A B)}
5. I : fset(ℕ)
6. J : fset(ℕ)
7. f : J ⟶ I
8. v : G(I+new-name(I))
9. p(v) ∈ (Path_c𝕌 A B)(v)
10. p(v) ∈ J:fset(ℕ) ⟶ f:J ⟶ I+new-name(I) ⟶ u:Point(dM(J)) ⟶ FibrantType(formal-cube(J))
11. ∀J,K:fset(ℕ). ∀f:J ⟶ I+new-name(I). ∀g:K ⟶ J. ∀u:Point(dM(J)).
      (let A,cA = p(v) J f u in <(A)<g>, (cA)<g>> = (p(v) K f ⋅ g (u f(v) g)) ∈ FibrantType(formal-cube(K)))
12. (p(v) I+new-name(I) 1 1) = B(v) ∈ FibrantType(formal-cube(I+new-name(I)))
⊢ universe-type(B;I+new-name(I);v)((new-name(I)1) ⋅ f)
= fst((p(v) I+new-name(I) 1 <new-name(I)>))((new-name(I)1) ⋅ f)
∈ Type

---

Latex:

---

Latex:
No  Annotations
\mforall{}G:j\mvdash{}.  \mforall{}A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}.  \mforall{}p:\{G  \mvdash{}  \_:(Path\_c\mBbbU{}  A  B)\}.  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}v:G(I+new-name(I)).
    (universe-type(B;I+new-name(I);v)((new-name(I)1)  \mcdot{}  f)
    =  fst((p(v)  I+new-name(I)  1  <new-name(I)>))((new-name(I)1)  \mcdot{}  f))


By

---

Latex:
(Intros\mcdot{}
  THEN  (InstLemma  `cubical-term-at\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}(Path\_c\mBbbU{}  A  B)\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}I+new-name(I)\mkleeneclose{};
              \mkleeneopen{}v\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  DupHyp  (-1)
  THEN  (RWO  "path-type-at"  (-1)  THENA  Auto)
  THEN  ((MemTypeHD  (-1)  THENA  (D  -1  THEN  Auto))  THEN  Fold  `member`  (-2))
  THEN  (MemTypeHD  (-2)  THENA  (D  -1  THEN  Auto))
  THEN  Fold  `member`  (-3)
  THEN  RepUR  ``cubical-universe  closed-cubical-universe``  -1
  THEN  RepUR  ``cubical-universe  closed-cubical-universe``  -2
  THEN  RepUR  ``cubical-universe  closed-cubical-universe``  -3
  THEN  RepUR  ``closed-type-to-type  csm-fibrant-type``  -1
  THEN  RepUR  ``closed-type-to-type  csm-fibrant-type``  -2
  THEN  RepUR  ``closed-type-to-type  csm-fibrant-type``  -3
  THEN  D  -1
  THEN  Thin  (-2)
  \mcdot{})

---

Home Index