---

Step * of Lemma equal-fiber-discrete

No Annotations
∀[B:Type]. ∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[f:{X ⊢ _:(A ⟶ discr(B))}]. ∀[z:{X ⊢ _:discr(B)}]. ∀[a,b:{X ⊢ _:Fiber(f;z)}].
  (a = b ∈ {X ⊢ _:Fiber(f;z)} ⇐⇒ a.1 = b.1 ∈ {X ⊢ _:A})
BY
{ (Intro
   THEN InstLemma `equal-fiber-when-discrete` []
   THEN ParallelLast'
   THEN (D -1 With ⌜discr(B)⌝  THENA Auto)
   THEN RepeatFor 5 (ParallelLast')
   THEN D -1
   THEN Auto) }

1
1. B : Type
2. X : CubicalSet{j}
3. A : {X ⊢ _}
4. f : {X ⊢ _:(A ⟶ discr(B))}
5. z : {X ⊢ _:discr(B)}
6. a : {X ⊢ _:Fiber(f;z)}
7. b : {X ⊢ _:Fiber(f;z)}
8. x : {X ⊢ _:Path(discr(B))}
⊢ x = refl(x @ 0(𝕀)) ∈ {X ⊢ _:Path(discr(B))}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[B:Type].  \mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[f:\{X  \mvdash{}  \_:(A  {}\mrightarrow{}  discr(B))\}].  \mforall{}[z:\{X  \mvdash{}  \_:discr(B)\}].
\mforall{}[a,b:\{X  \mvdash{}  \_:Fiber(f;z)\}].
    (a  =  b  \mLeftarrow{}{}\mRightarrow{}  a.1  =  b.1)


By

---

Latex:
(Intro
  THEN  InstLemma  `equal-fiber-when-discrete`  []
  THEN  ParallelLast'
  THEN  (D  -1  With  \mkleeneopen{}discr(B)\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  5  (ParallelLast')
  THEN  D  -1
  THEN  Auto)

---

Home Index