Definition Annihilator (C:category) (zero:ZeroMaps C) {c d:C} (f:c --> d) : C^op ⟶ SET. Proof. unshelve refine (_,,_). { unshelve refine (_,,_). { intro b. exists (∑ g:Hom C b c, f ∘ g = pr1 zero b d). abstract (apply isaset_total2; [ apply setproperty | intro g; apply isasetaprop; apply homset_property ]) using _L_. } { intros a b p ge; simpl. exists (pr1 ge ∘ opp_mor p). { abstract ( unshelve refine (! assoc _ _ _ @ _); rewrite (pr2 ge); apply (pr2 (pr2 zero) _ _ _ _)) using _M_. } } } { abstract (split; [ intros x; apply funextsec; intros [r rf0]; apply subtypePath; [ intro; apply homset_property | simpl; unfold opp_mor; apply id_left ] | intros w x y t u; apply funextsec; intros [r rf0]; apply subtypePath; [ intro; apply homset_property | simpl; unfold opp_mor; apply pathsinv0, assoc ] ]) using _N_. } Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import Require Import Require Import UniMath.MoreFoundations.Tactics.