case up.up
B : Type u
inst✝ : Quiver B
a b : B
f g : Discrete (Path a b)
down✝ : f.as = g.as
⊢ PrelaxFunctor.map₂ (preinclusion B) { down := { down := down✝ } } =
    eqToHom (_ : (↑(preinclusion B)).map f = (↑(preinclusion B)).map g)
B : Type u
inst✝ : Quiver B
a b : B
f g : Discrete (Path a b)
η : f ⟶ g
⊢ PrelaxFunctor.map₂ (preinclusion B) η = eqToHom (_ : (↑(preinclusion B)).map f = (↑(preinclusion B)).map g)
rcases η with ⟨⟨⟩⟩
case up.up.refl
B : Type u
inst✝ : Quiver B
a b : B
f : Discrete (Path a b)
down✝ : f.as = f.as
⊢ PrelaxFunctor.map₂ (preinclusion B) { down := { down := down✝ } } =
    eqToHom (_ : (↑(preinclusion B)).map f = (↑(preinclusion B)).map f)
case up.up
B : Type u
inst✝ : Quiver B
a b : B
f g : Discrete (Path a b)
down✝ : f.as = g.as
⊢ PrelaxFunctor.map₂ (preinclusion B) { down := { down := down✝ } } =
    eqToHom (_ : (↑(preinclusion B)).map f = (↑(preinclusion B)).map g)
cases Discrete.ext _ _ (by assumption)
no goals
case up.up.refl
B : Type u
inst✝ : Quiver B
a b : B
f : Discrete (Path a b)
down✝ : f.as = f.as
⊢ PrelaxFunctor.map₂ (preinclusion B) { down := { down := down✝ } } =
    eqToHom (_ : (↑(preinclusion B)).map f = (↑(preinclusion B)).map f)
convert (inclusionPath a b).map_id _
no goals
B : Type u
inst✝ : Quiver B
a b : B
f g : Discrete (Path a b)
down✝ : f.as = g.as
⊢ ?m.4788.as = ?m.4789.as
assumption