proposition: Corollary lawvere_from_morph_iso_functorial {a b} (g : a ~{D}~> G b) {a' b'} (i : a' ~> a) (j : b ~> b') : j ∘ from lawvere_morph_iso g ∘ fmap[F] i ≈ from lawvere_morph_iso (fmap[G] j ∘ g ∘ i).
proof: Proof. now apply lawvere_from_functorial. 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