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