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_from_to (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