no goals
C : Type u₁
inst✝ : Category C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
h : HasColimit F₁
⊢ (X : Discrete PEmpty) → F₂.obj X ⟶ ((Functor.const (Discrete PEmpty)).obj (colimit F₁)).obj X
aesop_cat
no goals
C : Type u₁
inst✝ : Category C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
h : HasColimit F₁
⊢ ∀ ⦃X Y : Discrete PEmpty⦄ (f : X ⟶ Y),
    F₂.map f ≫ id (Discrete.casesOn Y fun as => False.elim (_ : False)) =
      id (Discrete.casesOn X fun as => False.elim (_ : False)) ≫
        ((Functor.const (Discrete PEmpty)).obj (colimit F₁)).map f
aesop_cat