---

Step * 1 of Lemma equal-fiber-discrete


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))}
BY
{ (InstLemma `discrete-pathtype` [⌜B⌝;⌜X⌝;⌜x⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(InstLemma  `discrete-pathtype`  [\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index