proposition: Lemma lawvere_to_from {a b} (g : a ~> G b) : φ' E (ψ' E g) ≈ g.
proof: Proof. intros. unfold φ', ψ'. pose proof (@lawvere_to_functorial _ _ (`2 (fobj[(lawvere_iso E)⁻¹] ((a, b); g))) a b (fst (to (`1 (projG E) ((a, b); g)))) (snd (`1 (projG E) ((a, b); g))⁻¹)) as X. etransitivity. - now apply X. - clear X. symmetry. etransitivity. + spose (φ_ψ_equiv ((a, b); g)) as X1. symmetry in X1. now apply X1. + apply compose_respects; [|reflexivity]. rewrite <- !comp_assoc. apply compose_respects; [reflexivity|]. spose (surjective_tripleF (ψ E ((a, b); g))) as X2. unfold ψ in *. simpl. rewrite <- X2. solve [ reflexivity | simpl; unfold lawvere_to, θ, κ, ψ; rewrite !comp_assoc; reflexivity ]. 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