proposition: Lemma lawvere_from_functorial {a b} (g : a ~{D}~> G b) {a' b'} (i : a' ~> a) (j : b ~> b') : j ∘ ψ' E g ∘ fmap[F] i ≈ ψ' E (fmap[G] j ∘ g ∘ i).
proof: Proof. given (Gj : ((a', b); g ∘ i) ~{ Id[D] ↓ G }~> ((a', b'); fmap[G] j ∘ g ∘ i)). { now refine ((id, j); _); simpl; abstract cat. } spose (`2 (to (lawvere_iso_from (fmap[G] j ∘ g ∘ i)) ∘ fmap[ψ E] Gj ∘ from (lawvere_iso_from (g ∘ i)))) as H. spose (`2 (projG E) ((a', b); g ∘ i) ((a', b'); fmap[G] j ∘ g ∘ i) Gj) as H1. destruct H1 as [H1 H2]. rewrite <- H1 in H; clear H1. rewrite <- H2 in H; clear H2. rewrite fmap_id, id_right in H. rewrite H. clear Gj H. given (Gj : ((a', b); g ∘ i) ~{ Id[D] ↓ G }~> ((G b, b'); fmap[G] j)). { now refine ((g ∘ i, j); _); simpl; abstract cat. } spose (`2 (to (lawvere_iso_from (fmap[G] j)) ∘ fmap[ψ E] Gj ∘ from (lawvere_iso_from (g ∘ i)))) as H. spose (`2 (projG E) ((a', b); g ∘ i) ((G b, b'); fmap[G] j) Gj) as H1. destruct H1 as [H1 H2]. rewrite <- H1 in H; clear H1. rewrite <- H2 in H; clear H2. rewrite <- H. clear Gj H. rewrite fmap_comp. given (Gj : ((a, b); g) ~{ Id[D] ↓ G }~> ((G b, b'); fmap[G] j)). { now refine ((g, j); _); abstract cat. } spose (`2 (to (lawvere_iso_from (fmap[G] j)) ∘ fmap[ψ E] Gj ∘ from (lawvere_iso_from (g)))) as H. spose (`2 (projG E) ((a, b); g) ((G b, b'); fmap[G] j) Gj) as H1. destruct H1 as [H1 H2]. rewrite <- H1 in H; clear H1. rewrite <- H2 in H; clear H2. rewrite <- H. now 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.Adjunction.Natural.Transformation.Universal Category.Construction.Comma Category.Construction.Product Category.Instance.Cat Category.Instance.Fun Category.Instance.Sets