proposition: Lemma μ_κ_θ : ∀ x, `1 (μ E x) ≈ κ E (ψ E x) ∘ θ E x.
proof: Proof. intros. pose proof (σ E). destruct X as [_ X]. specialize (X x); simpl in X. unfold equiv_iso, μ, κ, θ, ψ in *. destruct (iso_to_from (lawvere_iso E)), (projG E), (projF E). destruct X; split. - simpl in e2 |- *. rewrite <- e2; cat. - simpl in e3 |- *. rewrite <- e3; 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