---

Step * of Lemma csm-fiber-path

No Annotations
∀[X:j⊢]. ∀[T,A:{X ⊢ _}]. ∀[w:{X ⊢ _:(T ⟶ A)}]. ∀[a:{X ⊢ _:A}]. ∀[p:{X ⊢ _:Fiber(w;a)}]. ∀[H:j⊢]. ∀[s:H j⟶ X].
  ((fiber-path(p))s = fiber-path((p)s) ∈ {H ⊢ _:(Path_(A)s (a)s app((w)s; fiber-member((p)s)))})
BY
{ (Intros
   THEN Unhide
   THEN Unfold `cubical-fiber` -3
   THEN Unfold `fiber-path` 0
   THEN (InstLemma `csm-ap-cubical-snd` [⌜X⌝;⌜H⌝;⌜T⌝]⋅ THENA Auto)
   THEN (Assert app((w)p; q) ∈ {X.T ⊢ _:(A)p} BY
               ((Assert q ∈ {X.T ⊢ _:(T)p} BY
                       Auto)
                THEN (Assert (w)p ∈ {X.T ⊢ _:((T ⟶ A))p} BY
                            Auto)
                THEN (InstLemmaIJ `csm-cubical-fun` [⌜X⌝;X.T;⌜T⌝;⌜A⌝;⌜p⌝]⋅ THENA Auto)
                THEN (Assert (w)p ∈ {X.T ⊢ _:((T)p ⟶ (A)p)} BY
                            (InferEqualTypeGen THEN Auto))
                THEN BLemma `cubical-app_wf_fun` 
                THEN Auto))
   THEN Assert ⌜app((w)s; fiber-member((p)s)) ∈ {H ⊢ _:(A)s}⌝⋅) }

1
.....assertion..... 
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. w : {X ⊢ _:(T ⟶ A)}
5. a : {X ⊢ _:A}
6. p : {X ⊢ _:Σ T (Path_(A)p (a)p app((w)p; q))}
7. H : CubicalSet{j}
8. s : H j⟶ X
9. ∀[B:{X.T ⊢ _}]. ∀[p:{X ⊢ _:Σ T B}]. ∀[s:H j⟶ X].  ((p.2)s = (p)s.2 ∈ {H ⊢ _:((B)[p.1])s})
10. app((w)p; q) ∈ {X.T ⊢ _:(A)p}
⊢ app((w)s; fiber-member((p)s)) ∈ {H ⊢ _:(A)s}

2
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. w : {X ⊢ _:(T ⟶ A)}
5. a : {X ⊢ _:A}
6. p : {X ⊢ _:Σ T (Path_(A)p (a)p app((w)p; q))}
7. H : CubicalSet{j}
8. s : H j⟶ X
9. ∀[B:{X.T ⊢ _}]. ∀[p:{X ⊢ _:Σ T B}]. ∀[s:H j⟶ X].  ((p.2)s = (p)s.2 ∈ {H ⊢ _:((B)[p.1])s})
10. app((w)p; q) ∈ {X.T ⊢ _:(A)p}
11. app((w)s; fiber-member((p)s)) ∈ {H ⊢ _:(A)s}
⊢ (p.2)s = (p)s.2 ∈ {H ⊢ _:(Path_(A)s (a)s app((w)s; fiber-member((p)s)))}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T,A:\{X  \mvdash{}  \_\}].  \mforall{}[w:\{X  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}].  \mforall{}[a:\{X  \mvdash{}  \_:A\}].  \mforall{}[p:\{X  \mvdash{}  \_:Fiber(w;a)\}].  \mforall{}[H:j\mvdash{}].
\mforall{}[s:H  j{}\mrightarrow{}  X].
    ((fiber-path(p))s  =  fiber-path((p)s))


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  Unfold  `cubical-fiber`  -3
  THEN  Unfold  `fiber-path`  0
  THEN  (InstLemma  `csm-ap-cubical-snd`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  app((w)p;  q)  \mmember{}  \{X.T  \mvdash{}  \_:(A)p\}  BY
                          ((Assert  q  \mmember{}  \{X.T  \mvdash{}  \_:(T)p\}  BY
                                          Auto)
                            THEN  (Assert  (w)p  \mmember{}  \{X.T  \mvdash{}  \_:((T  {}\mrightarrow{}  A))p\}  BY
                                                    Auto)
                            THEN  (InstLemmaIJ  `csm-cubical-fun`  [\mkleeneopen{}X\mkleeneclose{};X.T;\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (Assert  (w)p  \mmember{}  \{X.T  \mvdash{}  \_:((T)p  {}\mrightarrow{}  (A)p)\}  BY
                                                    (InferEqualTypeGen  THEN  Auto))
                            THEN  BLemma  `cubical-app\_wf\_fun` 
                            THEN  Auto))
  THEN  Assert  \mkleeneopen{}app((w)s;  fiber-member((p)s))  \mmember{}  \{H  \mvdash{}  \_:(A)s\}\mkleeneclose{}\mcdot{})

---

Home Index