Definition ZeroMaps_opp_opp (C:category) (zero:ZeroMaps C) : ZeroMaps_opp C^op (ZeroMaps_opp C zero) = zero. Proof. unshelve refine (total2_paths_f _ _). - reflexivity. - unshelve refine (total2_paths_f _ _); reflexivity. Defined.
Require Import UniMath.MoreFoundations.Tactics.