proposition: Lemma lawvere_iso_to {a b} (f : F a ~> b) : φ E ((a, b); f) ≅ ((a, b); φ' E f).
proof: Proof. construct. - exists (from (κ E ((a, b); f))). abstract (unfold φ', lawvere_to; rewrite <- !comp_assoc; pair_comp; rewrite iso_to_from; simpl fst; now rewrite id_right). - exists (to (κ E ((a, b); f))). abstract (unfold φ', lawvere_to; rewrite !comp_assoc; rewrite <- !fmap_comp; pair_comp; rewrite iso_to_from; simpl snd; now rewrite fmap_id, id_left). - abstract (simpl; split; pair_comp; now rewrite iso_from_to). - abstract (simpl; split; pair_comp; now rewrite iso_to_from). Defined.
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