Lemma preIt_uniq (t : ∑ h : L μF --> X, # L inF· h = ψ μF h): t = tpair (λ h : L μF --> X, # L inF· h = ψ μF h) preIt preIt_ok. Proof. destruct t as [h h_rec_eq]; simpl. assert (same: h = preIt). 2: { apply subtypePath. + intro. apply homset_property. + simpl. exact same. } apply cancel_φ. unfold preIt. rewrite (φ_adj_after_φ_adj_inv (pr2 is_left_adj_L)). assert(φh_is_alg_mor: inF · φ h = #F(φ h) · φ (ψ (R X) (ε X))). + rewrite <- φ_ψ_μF_eq. rewrite <- (φ_adj_natural_precomp (pr2 is_left_adj_L)). apply maponpaths. exact h_rec_eq. + use (let X : AF ⟦ InitialObject μF_Initial, ⟨ R X, φ (ψ (R X) (ε X)) ⟩ ⟧ := _ in _). * apply (tpair _ (φ h)); assumption. * apply (maponpaths pr1 (InitialArrowUnique _ _ X0)). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.Adjunctions.Core.