Definition monad_underlying_is_right_adjoint : is_right_adjoint (underlying_of_hset_struct monad_to_hset_struct). Proof. use right_adjoint_left_from_partial. - exact (λ X, monad_free_alg X). - exact (λ X, η M X). - refine (λ X Y f, _). use iscontraprop1. + exact (monad_to_hset_struct_adj_lift_unique (pr2 Y) f). + simple refine (_ ,, _). * exact (monad_to_hset_struct_adj_lift (pr2 Y) f). * exact (monad_to_hset_struct_adj_lift_eq (pr2 Y) f). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits. Require Import UniMath.CategoryTheory.Monads.Monads.