proposition: Theorem hom_counit_fmap_unit {x} : hom_counit (F x) ∘ fmap[F] (hom_unit x) ≈ id.
proof: Proof. spose (@hom_counit_naturality_consequence x (F x) (hom_unit x)) as X. rewrites. unfold hom_unit; simpl. srewrite (iso_from_to hom_adj (x, F x) id); cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Theory.Adjunction Category.Adjunction.Natural.Transformation Category.Construction.Product Category.Construction.Opposite Category.Functor.Hom Category.Functor.Construction.Product Category.Functor.Opposite Category.Instance.Fun Category.Instance.Sets