proposition: Lemma lawvere_eqv_counit_fmap_unit {a} : lawvere_eqv_counit ∘ fmap[F] lawvere_eqv_unit ≈ id[F a].
proof: Proof. simpl; intros. unfold lawvere_eqv_counit, lawvere_eqv_unit. rewrite <- id_left. rewrite comp_assoc. rewrite lawvere_from_morph_iso_functorial. simpl (`2 _). rewrite fmap_id, !id_left. now sapply (iso_from_to (@lawvere_morph_iso a (F a))). 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.Adjunction.Natural.Transformation.Universal Category.Construction.Comma Category.Construction.Product Category.Instance.Cat Category.Instance.Fun Category.Instance.Sets