Definition make_mnd_univ_cat_with_terminal_obj (C : univalent_category) (M : Monad C) (TC : Terminal C) (MT : preserves_terminal M) : mnd univ_cat_with_terminal_obj. Proof. use make_mnd_total_bicat. - apply disp_2cells_isaprop_subbicat. - use Monad_to_mnd_bicat_of_univ_cats. + exact C. + exact M. - use make_disp_mnd. + exact (TC ,, tt). + exact (tt ,, MT). + exact (tt ,, tt). + exact (tt ,, tt). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Examples.StructuredCategories. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.Examples.EndoMap. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell. Require Import UniMath.Bicategories.Monads.Examples.MonadsInBicatOfUnivCats. Require Import UniMath.Bicategories.Monads.Examples.MonadsInBicatOfCats. Require Import UniMath.Bicategories.Monads.Examples.MonadsInTotalBicat. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Require Import UniMath.Bicategories.MonoidalCategories.BicatOfActegories.