---

Step * of Lemma equal-fiber-when-discrete

No Annotations
∀[X:j⊢]. ∀[T,A:{X ⊢ _}]. ∀[f:{X ⊢ _:(A ⟶ T)}]. ∀[z:{X ⊢ _:T}]. ∀[a,b:{X ⊢ _:Fiber(f;z)}].
  a = b ∈ {X ⊢ _:Fiber(f;z)} ⇐⇒ a.1 = b.1 ∈ {X ⊢ _:A} 
  supposing ∀x:{X ⊢ _:Path(T)}. (x = refl(x @ 0(𝕀)) ∈ {X ⊢ _:Path(T)})
BY
{ (Intros
   THEN (Assert app((f)p; q) ∈ {X.A ⊢ _:(T)p} BY
               (Unhide
                THEN (Assert (f)p ∈ {X.A ⊢ _:((A ⟶ T))p} BY
                            Auto)
                THEN (Assert (f)p ∈ {X.A ⊢ _:((A)p ⟶ (T)p)} BY
                            (InferEqualTypeGen THEN Auto THEN EqCDA THEN Auto))
                THEN Auto))
   THEN Auto
   THEN Unfold `cubical-fiber` 0
   THEN BLemma `cubical-sigma-equal`
   THEN Auto) }

1
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. f : {X ⊢ _:(A ⟶ T)}
5. z : {X ⊢ _:T}
6. a : {X ⊢ _:Fiber(f;z)}
7. b : {X ⊢ _:Fiber(f;z)}
8. ∀x:{X ⊢ _:Path(T)}. (x = refl(x @ 0(𝕀)) ∈ {X ⊢ _:Path(T)})
9. app((f)p; q) ∈ {X.A ⊢ _:(T)p}
10. a.1 = b.1 ∈ {X ⊢ _:A}
⊢ a.2 = b.2 ∈ {X ⊢ _:((Path_(T)p (z)p app((f)p; q)))[a.1]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T,A:\{X  \mvdash{}  \_\}].  \mforall{}[f:\{X  \mvdash{}  \_:(A  {}\mrightarrow{}  T)\}].  \mforall{}[z:\{X  \mvdash{}  \_:T\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:Fiber(f;z)\}].
    a  =  b  \mLeftarrow{}{}\mRightarrow{}  a.1  =  b.1  supposing  \mforall{}x:\{X  \mvdash{}  \_:Path(T)\}.  (x  =  refl(x  @  0(\mBbbI{})))


By

---

Latex:
(Intros
  THEN  (Assert  app((f)p;  q)  \mmember{}  \{X.A  \mvdash{}  \_:(T)p\}  BY
                          (Unhide
                            THEN  (Assert  (f)p  \mmember{}  \{X.A  \mvdash{}  \_:((A  {}\mrightarrow{}  T))p\}  BY
                                                    Auto)
                            THEN  (Assert  (f)p  \mmember{}  \{X.A  \mvdash{}  \_:((A)p  {}\mrightarrow{}  (T)p)\}  BY
                                                    (InferEqualTypeGen  THEN  Auto  THEN  EqCDA  THEN  Auto))
                            THEN  Auto))
  THEN  Auto
  THEN  Unfold  `cubical-fiber`  0
  THEN  BLemma  `cubical-sigma-equal`
  THEN  Auto)

---

Home Index