proposition: Lemma fidentity_axioms : forall a, Category.axioms a -> axioms (fidentity a) = True.
proof: Proof. ir. app iff_eq; ir. uhg; ee. uf fidentity. uf Umorphism.identity. app Umorphism.create_like. fw. fw. ir. fw. rwi source_fidentity H1; am. rwi source_fidentity H1; am. ir; fw; try (rwi source_fidentity H1; cw). ir; fw; try (rwi source_fidentity H1; cw). ir; fw; try (rwi source_fidentity H1; cw). ir; fw; try (rwi source_fidentity H1; cw). ir; fw'; try (rwi source_fidentity H1; cw); try (rwi source_fidentity H2; cw). Qed.
imports: Arith category