Library UniMath.Bicategories.Monads.Examples.MonadsInBicatOfCats
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.Monads.Monads.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.BicatOfCats.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat.
Import DispBicat.Notations.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax.
Local Open Scope cat.
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.Monads.Monads.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.BicatOfCats.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat.
Import DispBicat.Notations.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax.
Local Open Scope cat.
1. Monads internal to `bicat_of_cats` to monads
Definition mnd_bicat_of_cats_to_Monad
(m : mnd bicat_of_cats)
: Monad (ob_of_mnd m).
Show proof.
(m : mnd bicat_of_cats)
: Monad (ob_of_mnd m).
Show proof.
simple refine (_,,((_ ,, _) ,, _)).
- exact (endo_of_mnd m).
- exact (mult_of_mnd m).
- exact (unit_of_mnd m).
- repeat split.
+ abstract
(intro x ; cbn ;
pose (nat_trans_eq_pointwise (mnd_unit_right m) x) as p ;
cbn in p ;
rewrite id_left in p ;
exact p).
+ abstract
(intro x ; cbn ;
pose (nat_trans_eq_pointwise (mnd_unit_left m) x) as p ;
cbn in p ;
rewrite id_left in p ;
exact p).
+ abstract
(intro x ; cbn ;
pose (nat_trans_eq_pointwise (mnd_mult_assoc m) x) as p ;
cbn in p ;
rewrite id_left in p ;
exact (!p)).
- exact (endo_of_mnd m).
- exact (mult_of_mnd m).
- exact (unit_of_mnd m).
- repeat split.
+ abstract
(intro x ; cbn ;
pose (nat_trans_eq_pointwise (mnd_unit_right m) x) as p ;
cbn in p ;
rewrite id_left in p ;
exact p).
+ abstract
(intro x ; cbn ;
pose (nat_trans_eq_pointwise (mnd_unit_left m) x) as p ;
cbn in p ;
rewrite id_left in p ;
exact p).
+ abstract
(intro x ; cbn ;
pose (nat_trans_eq_pointwise (mnd_mult_assoc m) x) as p ;
cbn in p ;
rewrite id_left in p ;
exact (!p)).
2. The inverse
Definition Monad_to_mnd_bicat_of_cats
{C : category}
(m : Monad C)
: mnd bicat_of_cats.
Show proof.
{C : category}
(m : Monad C)
: mnd bicat_of_cats.
Show proof.
use make_mnd.
- use make_mnd_data.
+ exact C.
+ cbn.
exact m.
+ exact (η m).
+ exact (μ m).
- repeat split.
+ abstract
(use nat_trans_eq ; [ apply homset_property | ] ;
intro x ;
cbn ;
rewrite id_left ;
apply (Monad_law2(T:=m) x)).
+ abstract
(use nat_trans_eq ; [ apply homset_property | ] ;
intro x ;
cbn ;
rewrite id_left ;
apply (Monad_law1(T:=m) x)).
+ abstract
(use nat_trans_eq ; [ apply homset_property | ] ;
intro x ;
cbn ;
rewrite id_left ;
refine (!_) ;
apply (Monad_law3(T:=m) x)).
- use make_mnd_data.
+ exact C.
+ cbn.
exact m.
+ exact (η m).
+ exact (μ m).
- repeat split.
+ abstract
(use nat_trans_eq ; [ apply homset_property | ] ;
intro x ;
cbn ;
rewrite id_left ;
apply (Monad_law2(T:=m) x)).
+ abstract
(use nat_trans_eq ; [ apply homset_property | ] ;
intro x ;
cbn ;
rewrite id_left ;
apply (Monad_law1(T:=m) x)).
+ abstract
(use nat_trans_eq ; [ apply homset_property | ] ;
intro x ;
cbn ;
rewrite id_left ;
refine (!_) ;
apply (Monad_law3(T:=m) x)).
3. The equivalence
Definition mnd_bicat_of_cats_weq_Monad_inv₁
(m : mnd bicat_of_cats)
: Monad_to_mnd_bicat_of_cats (mnd_bicat_of_cats_to_Monad m) = m.
Show proof.
Definition mnd_bicat_of_cats_weq_Monad_inv₂
{C : category}
(m : Monad C)
: mnd_bicat_of_cats_to_Monad (Monad_to_mnd_bicat_of_cats m) = m.
Show proof.
Definition mnd_bicat_of_cats_weq_Monad
: mnd bicat_of_cats ≃ ∑ (C : category), Monad C.
Show proof.
(m : mnd bicat_of_cats)
: Monad_to_mnd_bicat_of_cats (mnd_bicat_of_cats_to_Monad m) = m.
Show proof.
use total2_paths_f.
- apply idpath.
- cbn.
use subtypePath.
{
intro.
apply isaprop_is_mnd.
}
apply idpath.
- apply idpath.
- cbn.
use subtypePath.
{
intro.
apply isaprop_is_mnd.
}
apply idpath.
Definition mnd_bicat_of_cats_weq_Monad_inv₂
{C : category}
(m : Monad C)
: mnd_bicat_of_cats_to_Monad (Monad_to_mnd_bicat_of_cats m) = m.
Show proof.
Definition mnd_bicat_of_cats_weq_Monad
: mnd bicat_of_cats ≃ ∑ (C : category), Monad C.
Show proof.