Library UniMath.CategoryTheory.Monads.Comonads
**********************************************************
Contents:
Written by Ralph Matthes, 2023
- dualization of the contents of Monads.v, but not the part on substitution (that would become redecoration), i.e., Section MonadsUsingCoproducts
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.MoreFoundations.Notations.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.SIP.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.Core.Univalence.
Local Open Scope cat.
Section Comonad_disp_def.
Context {C : category}.
Definition disp_Comonad_data (F : functor C C) : UU :=
(F ⟹ F ∙ F) × (F ⟹ functor_identity C).
Definition disp_δ {F : functor C C} (T : disp_Comonad_data F) : F ⟹ F ∙ F := pr1 T.
Definition disp_ε {F : functor C C} (T : disp_Comonad_data F) : F ⟹ functor_identity C := pr2 T.
the names of the components follow Mac Lane
Definition disp_Comonad_laws {F : functor C C} (T : disp_Comonad_data F) : UU :=
(
(∏ c : C, disp_δ T c · disp_ε T (F c) = identity (F c))
×
(∏ c : C, disp_δ T c · #F (disp_ε T c) = identity (F c)) )
×
(∏ c : C, disp_δ T c · #F (disp_δ T c) = disp_δ T c · disp_δ T (F c)).
Lemma isaprop_disp_Comonad_laws {F : functor C C} (T : disp_Comonad_data F) : isaprop (disp_Comonad_laws T).
Show proof.
Definition disp_Comonad_Mor_laws {F F' : functor C C} (T : disp_Comonad_data F) (T' : disp_Comonad_data F') (α : F ⟹ F') : UU :=
(∏ a : C, α a · disp_δ T' a = disp_δ T a · #F (α a) · α (F' a)) ×
(∏ a : C, α a · disp_ε T' a = disp_ε T a).
Lemma isaprop_disp_Comonad_Mor_laws {F F' : functor C C} (T : disp_Comonad_data F) (T' : disp_Comonad_data F') (α : F ⟹ F')
: isaprop (disp_Comonad_Mor_laws T T' α).
Show proof.
Lemma comonads_category_id_subproof {F : functor C C} (T : disp_Comonad_data F) (Tlaws : disp_Comonad_laws T) :
disp_Comonad_Mor_laws T T (nat_trans_id F).
Show proof.
Lemma comonads_category_comp_subproof {F F' F'' : functor C C}
(T : disp_Comonad_data F) (Tlaws : disp_Comonad_laws T)
(T' : disp_Comonad_data F') (T'laws : disp_Comonad_laws T')
(T'' : disp_Comonad_data F'') (T''laws : disp_Comonad_laws T'')
(α : F ⟹ F') (α' : F' ⟹ F'') :
disp_Comonad_Mor_laws T T' α → disp_Comonad_Mor_laws T' T'' α' → disp_Comonad_Mor_laws T T'' (nat_trans_comp _ _ _ α α').
Show proof.
intros Hα Hα'.
split; intros; simpl.
- rewrite assoc'.
set (H:=pr1 Hα' a); simpl in H.
rewrite H; clear H.
rewrite functor_comp.
set (H:=pr1 Hα a); simpl in H.
do 2 rewrite assoc.
rewrite H; clear H; rewrite <- !assoc.
do 2 apply maponpaths.
now rewrite !assoc, nat_trans_ax.
- rewrite assoc'.
etrans.
{ apply maponpaths, (pr2 Hα'). }
apply (pr2 Hα).
split; intros; simpl.
- rewrite assoc'.
set (H:=pr1 Hα' a); simpl in H.
rewrite H; clear H.
rewrite functor_comp.
set (H:=pr1 Hα a); simpl in H.
do 2 rewrite assoc.
rewrite H; clear H; rewrite <- !assoc.
do 2 apply maponpaths.
now rewrite !assoc, nat_trans_ax.
- rewrite assoc'.
etrans.
{ apply maponpaths, (pr2 Hα'). }
apply (pr2 Hα).
Definition comonads_category_disp : disp_cat [C,C].
Show proof.
use disp_cat_from_SIP_data.
- intro F. exact (∑ T : disp_Comonad_data F, disp_Comonad_laws T).
- intros F F' [T Tlaws] [T' T'laws] α. exact (disp_Comonad_Mor_laws T T' α).
- intros F F' [T Tlaws] [T' T'laws] α. apply isaprop_disp_Comonad_Mor_laws.
- intros F [T Tlaws]. apply (comonads_category_id_subproof _ Tlaws).
- intros F F' F'' [T Tlaws] [T' T'laws] [T'' T''laws] α α'.
apply (comonads_category_comp_subproof _ Tlaws _ T'laws _ T''laws).
- intro F. exact (∑ T : disp_Comonad_data F, disp_Comonad_laws T).
- intros F F' [T Tlaws] [T' T'laws] α. exact (disp_Comonad_Mor_laws T T' α).
- intros F F' [T Tlaws] [T' T'laws] α. apply isaprop_disp_Comonad_Mor_laws.
- intros F [T Tlaws]. apply (comonads_category_id_subproof _ Tlaws).
- intros F F' F'' [T Tlaws] [T' T'laws] [T'' T''laws] α α'.
apply (comonads_category_comp_subproof _ Tlaws _ T'laws _ T''laws).
Definition category_Comonad : category := total_category comonads_category_disp.
Definition Comonad : UU := ob category_Comonad.
Coercion functor_from_Comonad (T : Comonad) : functor C C := pr1 T.
Definition δ (T : Comonad) : T ⟹ T ∙ T := pr112 T.
Definition ε (T : Comonad) : T ⟹ functor_identity C := pr212 T.
Lemma Comonad_law1 {T : Comonad} : ∏ c : C, δ T c · ε T (T c) = identity (T c).
Show proof.
Lemma Comonad_law2 {T : Comonad} : ∏ c : C, δ T c · #T (ε T c) = identity (T c).
Show proof.
Lemma Comonad_law3 {T : Comonad} : ∏ c : C, δ T c · #T (δ T c) = δ T c · δ T (T c).
Show proof.
Lemma comonads_category_disp_eq (F : functor C C) (T T' : comonads_category_disp F) : pr1 T = pr1 T' -> T = T'.
Show proof.
intro H.
induction T as [T Tlaws].
induction T' as [T' T'laws].
use total2_paths_f; [apply H |].
apply isaprop_disp_Comonad_laws.
induction T as [T Tlaws].
induction T' as [T' T'laws].
use total2_paths_f; [apply H |].
apply isaprop_disp_Comonad_laws.
Lemma comonads_category_Pisset (F : functor C C) : isaset (∑ T : disp_Comonad_data F, disp_Comonad_laws T).
Show proof.
change isaset with (isofhlevel 2).
apply isofhleveltotal2.
{ apply isasetdirprod; apply [C,C]. }
intro T.
apply isasetaprop.
apply isaprop_disp_Comonad_laws.
apply isofhleveltotal2.
{ apply isasetdirprod; apply [C,C]. }
intro T.
apply isasetaprop.
apply isaprop_disp_Comonad_laws.
Lemma comonads_category_Hstandard {F : functor C C}
(T : disp_Comonad_data F) (Tlaws : disp_Comonad_laws T)
(T' : disp_Comonad_data F) (T'laws : disp_Comonad_laws T') :
disp_Comonad_Mor_laws T T' (nat_trans_id F) → disp_Comonad_Mor_laws T' T (nat_trans_id F) → T,, Tlaws = T',, T'laws.
Show proof.
intros H H'.
apply subtypeInjectivity.
{ intro T0. apply isaprop_disp_Comonad_laws. }
cbn.
induction T as [δ ε].
induction T' as [δ' ε'].
apply dirprodeq; cbn.
- apply nat_trans_eq; [apply C|]. intro a.
assert (Hinst := pr1 H a).
cbn in Hinst.
rewrite id_right in Hinst.
rewrite id_left in Hinst.
rewrite functor_id in Hinst.
rewrite id_right in Hinst.
exact (!Hinst).
- apply nat_trans_eq; [apply C|]. intro a.
assert (Hinst := pr2 H a).
cbn in Hinst.
rewrite id_left in Hinst.
exact (!Hinst).
apply subtypeInjectivity.
{ intro T0. apply isaprop_disp_Comonad_laws. }
cbn.
induction T as [δ ε].
induction T' as [δ' ε'].
apply dirprodeq; cbn.
- apply nat_trans_eq; [apply C|]. intro a.
assert (Hinst := pr1 H a).
cbn in Hinst.
rewrite id_right in Hinst.
rewrite id_left in Hinst.
rewrite functor_id in Hinst.
rewrite id_right in Hinst.
exact (!Hinst).
- apply nat_trans_eq; [apply C|]. intro a.
assert (Hinst := pr2 H a).
cbn in Hinst.
rewrite id_left in Hinst.
exact (!Hinst).
Definition is_univalent_comonads_category_disp : is_univalent_disp comonads_category_disp.
Show proof.
use is_univalent_disp_from_SIP_data.
- exact comonads_category_Pisset.
- intros F [T Tlaws] [T' T'laws]. apply comonads_category_Hstandard.
- exact comonads_category_Pisset.
- intros F [T Tlaws] [T' T'laws]. apply comonads_category_Hstandard.
End Comonad_disp_def.
Arguments category_Comonad _ : clear implicits.
Arguments Comonad _ : clear implicits.
Definition is_univalent_category_Comonad {C : category} (HC : is_univalent C) :
is_univalent (category_Comonad C).
Show proof.
apply is_univalent_total_category.
- apply is_univalent_functor_category. apply HC.
- apply is_univalent_comonads_category_disp.
- apply is_univalent_functor_category. apply HC.
- apply is_univalent_comonads_category_disp.
Section pointfree.
Context (C : category) (T0: functor C C) (T : disp_Comonad_data T0).
Let EndC := [C, C].
Let ε := disp_ε T.
Let δ := disp_δ T.
Definition Comonad_laws_pointfree : UU :=
(
(nat_trans_comp _ _ _ δ (pre_whisker T0 ε) = identity(C:=EndC) T0)
×
(nat_trans_comp _ _ _ δ (post_whisker ε T0) = identity(C:=EndC) T0) )
×
(nat_trans_comp _ _ _ δ (post_whisker δ T0) = nat_trans_comp _ _ _ δ (pre_whisker T0 δ)).
Lemma pointfree_is_equiv: Comonad_laws_pointfree <-> disp_Comonad_laws T.
Show proof.
split.
- intro H. induction H as [[H1 H2] H3].
split.
+ split.
* intro c. apply (maponpaths pr1) in H1. apply toforallpaths in H1. apply H1.
* intro c. apply (maponpaths pr1) in H2. apply toforallpaths in H2. apply H2.
+ intro c. apply (maponpaths pr1) in H3. apply toforallpaths in H3. apply H3.
- intro H. induction H as [[H1 H2] H3].
split.
+ split.
* apply nat_trans_eq_alt. exact H1.
* apply nat_trans_eq_alt. exact H2.
+ apply nat_trans_eq; try apply homset_property. exact H3.
- intro H. induction H as [[H1 H2] H3].
split.
+ split.
* intro c. apply (maponpaths pr1) in H1. apply toforallpaths in H1. apply H1.
* intro c. apply (maponpaths pr1) in H2. apply toforallpaths in H2. apply H2.
+ intro c. apply (maponpaths pr1) in H3. apply toforallpaths in H3. apply H3.
- intro H. induction H as [[H1 H2] H3].
split.
+ split.
* apply nat_trans_eq_alt. exact H1.
* apply nat_trans_eq_alt. exact H2.
+ apply nat_trans_eq; try apply homset_property. exact H3.
Let T0' := T0 : EndC.
Let ε' := ε: EndC⟦T0', functor_identity C⟧.
Let δ' := δ: EndC⟦T0', functor_compose T0' T0'⟧.
Definition Comonad_laws_pointfree_in_functor_category : UU :=
(
(δ' · #(pre_composition_functor _ _ _ T0') ε' = identity(C:=EndC) T0')
×
(δ' · #(post_composition_functor _ _ _ T0') ε' = identity(C:=EndC) T0') )
×
(δ' · #(post_composition_functor _ _ _ T0') δ' = (δ' · #(pre_composition_functor _ _ _ T0') δ')).
the last variant of the laws is convertible with the one before
Goal
Comonad_laws_pointfree = Comonad_laws_pointfree_in_functor_category.
Show proof.
End pointfree.
Definition Comonad_Mor {C : category} (T T' : Comonad C) : UU
:= category_Comonad C ⟦T, T'⟧.
Coercion nat_trans_from_monad_mor {C : category} (T T' : Comonad C) (s : Comonad_Mor T T')
: T ⟹ T' := pr1 s.
Definition Comonad_Mor_laws {C : category} {T T' : Comonad C} (α : T ⟹ T')
: UU :=
(∏ a : C, α a · δ T' a = δ T a · #T (α a) · α (T' a)) ×
(∏ a : C, α a · ε T' a = ε T a).
Definition Comonad_Mor_ε {C : category} {T T' : Comonad C} (α : Comonad_Mor T T')
: ∏ a : C, α a · ε T' a = ε T a.
Show proof.
Definition Comonad_Mor_δ {C : category} {T T' : Comonad C} (α : Comonad_Mor T T')
: ∏ a : C, α a · δ T' a = δ T a · #T (α a) · α (T' a).
Show proof.
Definition Comonad_Mor_equiv {C : category}
{T T' : Comonad C} (α β : Comonad_Mor T T')
: α = β ≃ (pr1 α = pr1 β).
Show proof.
Lemma isaset_Comonad_Mor {C : category} (T T' : Comonad C) : isaset (Comonad_Mor T T').
Show proof.
Definition Comonad_composition {C : category} {T T' T'' : Comonad C}
(α : Comonad_Mor T T') (α' : Comonad_Mor T' T'')
: Comonad_Mor T T'' := α · α'.
Definition forgetfunctor_Comonad (C : category) : functor (category_Comonad C) [C,C]
:= pr1_category comonads_category_disp.
Lemma forgetComonad_faithful (C : category) : faithful (forgetfunctor_Comonad C).
Show proof.
Comonad_laws_pointfree = Comonad_laws_pointfree_in_functor_category.
Show proof.
End pointfree.
Definition Comonad_Mor {C : category} (T T' : Comonad C) : UU
:= category_Comonad C ⟦T, T'⟧.
Coercion nat_trans_from_monad_mor {C : category} (T T' : Comonad C) (s : Comonad_Mor T T')
: T ⟹ T' := pr1 s.
Definition Comonad_Mor_laws {C : category} {T T' : Comonad C} (α : T ⟹ T')
: UU :=
(∏ a : C, α a · δ T' a = δ T a · #T (α a) · α (T' a)) ×
(∏ a : C, α a · ε T' a = ε T a).
Definition Comonad_Mor_ε {C : category} {T T' : Comonad C} (α : Comonad_Mor T T')
: ∏ a : C, α a · ε T' a = ε T a.
Show proof.
Definition Comonad_Mor_δ {C : category} {T T' : Comonad C} (α : Comonad_Mor T T')
: ∏ a : C, α a · δ T' a = δ T a · #T (α a) · α (T' a).
Show proof.
Definition Comonad_Mor_equiv {C : category}
{T T' : Comonad C} (α β : Comonad_Mor T T')
: α = β ≃ (pr1 α = pr1 β).
Show proof.
Lemma isaset_Comonad_Mor {C : category} (T T' : Comonad C) : isaset (Comonad_Mor T T').
Show proof.
Definition Comonad_composition {C : category} {T T' T'' : Comonad C}
(α : Comonad_Mor T T') (α' : Comonad_Mor T' T'')
: Comonad_Mor T T'' := α · α'.
Definition forgetfunctor_Comonad (C : category) : functor (category_Comonad C) [C,C]
:= pr1_category comonads_category_disp.
Lemma forgetComonad_faithful (C : category) : faithful (forgetfunctor_Comonad C).
Show proof.
Definition of cobind
Context {C : category} {T : Comonad C}.
Definition cobind {a b : C} (f : C⟦T a,b⟧) : C⟦T a,T b⟧ := δ T a · # T f.
Lemma ε_cobind {a b : C} (f : C⟦T a,b⟧) : cobind f · ε T b = f.
Show proof.
unfold cobind.
rewrite assoc'.
etrans.
{ apply maponpaths.
apply (nat_trans_ax (ε T) _ _ f). }
rewrite assoc.
etrans.
{ apply cancel_postcomposition, Comonad_law1. }
apply id_left.
rewrite assoc'.
etrans.
{ apply maponpaths.
apply (nat_trans_ax (ε T) _ _ f). }
rewrite assoc.
etrans.
{ apply cancel_postcomposition, Comonad_law1. }
apply id_left.
Lemma cobind_ε {a : C} : cobind (ε T a) = identity (T a).
Show proof.
Lemma cobind_cobind {a b c : C} (f : C⟦T a,b⟧) (g : C⟦T b,c⟧) :
cobind f · cobind g = cobind (cobind f · g).
Show proof.
unfold cobind; rewrite assoc.
rewrite !functor_comp.
repeat rewrite assoc.
apply cancel_postcomposition.
etrans.
{ rewrite assoc'; apply maponpaths, (nat_trans_ax (δ T) _ _ f). }
rewrite assoc.
apply cancel_postcomposition.
apply (!Comonad_law3 a).
rewrite !functor_comp.
repeat rewrite assoc.
apply cancel_postcomposition.
etrans.
{ rewrite assoc'; apply maponpaths, (nat_trans_ax (δ T) _ _ f). }
rewrite assoc.
apply cancel_postcomposition.
apply (!Comonad_law3 a).
End cobind.
Section Comonad'_def.
Definition raw_Comonad_data (C : category) : UU :=
∑ F : C -> C, (((∏ a b : ob C, a --> b -> F a --> F b) ×
(∏ a : ob C, F a --> F (F a))) ×
(∏ a : ob C, F a --> a)).
Coercion functor_data_from_raw_Comonad_data {C : category} (T : raw_Comonad_data C) :
functor_data C C := make_functor_data (pr1 T) (pr1 (pr1 (pr2 T))).
Definition Comonad'_data_laws {C : category} (T : raw_Comonad_data C) :=
((is_functor T) ×
(is_nat_trans T (functor_composite_data T T) (pr2 (pr1 (pr2 T))))) ×
(is_nat_trans T (functor_identity C) (pr2 (pr2 T))).
Definition Comonad'_data (C : category) := ∑ (T : raw_Comonad_data C), Comonad'_data_laws T.
Definition Comonad'_data_to_Comonad_data {C : category} (T : Comonad'_data C) : disp_Comonad_data (_,, pr1 (pr1 (pr2 T))) :=
((pr2 (pr1 (pr2 (pr1 T))),, (pr2 (pr1 (pr2 T))))),,
(pr2 (pr2 (pr1 T)),, (pr2 (pr2 T))).
Definition Comonad' (C : category) := ∑ (T : Comonad'_data C),
(disp_Comonad_laws (Comonad'_data_to_Comonad_data T)).
End Comonad'_def.
Definition raw_Comonad_data (C : category) : UU :=
∑ F : C -> C, (((∏ a b : ob C, a --> b -> F a --> F b) ×
(∏ a : ob C, F a --> F (F a))) ×
(∏ a : ob C, F a --> a)).
Coercion functor_data_from_raw_Comonad_data {C : category} (T : raw_Comonad_data C) :
functor_data C C := make_functor_data (pr1 T) (pr1 (pr1 (pr2 T))).
Definition Comonad'_data_laws {C : category} (T : raw_Comonad_data C) :=
((is_functor T) ×
(is_nat_trans T (functor_composite_data T T) (pr2 (pr1 (pr2 T))))) ×
(is_nat_trans T (functor_identity C) (pr2 (pr2 T))).
Definition Comonad'_data (C : category) := ∑ (T : raw_Comonad_data C), Comonad'_data_laws T.
Definition Comonad'_data_to_Comonad_data {C : category} (T : Comonad'_data C) : disp_Comonad_data (_,, pr1 (pr1 (pr2 T))) :=
((pr2 (pr1 (pr2 (pr1 T))),, (pr2 (pr1 (pr2 T))))),,
(pr2 (pr2 (pr1 T)),, (pr2 (pr2 T))).
Definition Comonad' (C : category) := ∑ (T : Comonad'_data C),
(disp_Comonad_laws (Comonad'_data_to_Comonad_data T)).
End Comonad'_def.
Section Comonad_Comonad'_equiv.
Definition Comonad'_to_Comonad {C : category} (T : Comonad' C) : Comonad C :=
(_,,(Comonad'_data_to_Comonad_data (pr1 T),, pr2 T)).
Definition Comonad_to_raw_data {C : category} (T : Comonad C) : raw_Comonad_data C.
Show proof.
Definition Comonad_to_Comonad'_data {C : category} (T : Comonad C) : Comonad'_data C :=
(Comonad_to_raw_data T,, ((pr2 (T : functor C C),, (pr2 (δ T))),, pr2 (ε T))).
Definition Comonad_to_Comonad' {C : category} (T : Comonad C) : Comonad' C :=
(Comonad_to_Comonad'_data T,, pr22 T).
Definition Comonad'_to_Comonad_to_Comonad' {C : category} (T : Comonad' C) :
Comonad_to_Comonad' (Comonad'_to_Comonad T) = T := (idpath T).
Definition Comonad_to_Comonad'_to_Comonad {C : category} (T : Comonad C) :
Comonad'_to_Comonad (Comonad_to_Comonad' T) = T := (idpath T).
End Comonad_Comonad'_equiv.
Lemma Comonad'_eq_raw_data (C : category) (T T' : Comonad' C) :
pr1 (pr1 T) = pr1 (pr1 T') -> T = T'.
Show proof.
Lemma Comonad_eq_raw_data (C : category) (T T' : Comonad C) :
Comonad_to_raw_data T = Comonad_to_raw_data T' -> T = T'.
Show proof.
End Comonad_eq_helper.
Section Comonads_from_adjunctions.
Definition Comonad'_to_Comonad {C : category} (T : Comonad' C) : Comonad C :=
(_,,(Comonad'_data_to_Comonad_data (pr1 T),, pr2 T)).
Definition Comonad_to_raw_data {C : category} (T : Comonad C) : raw_Comonad_data C.
Show proof.
use tpair.
- exact (functor_on_objects T).
- use tpair.
+ use tpair.
* exact (@functor_on_morphisms C C T).
* exact (δ T).
+ exact (ε T).
- exact (functor_on_objects T).
- use tpair.
+ use tpair.
* exact (@functor_on_morphisms C C T).
* exact (δ T).
+ exact (ε T).
Definition Comonad_to_Comonad'_data {C : category} (T : Comonad C) : Comonad'_data C :=
(Comonad_to_raw_data T,, ((pr2 (T : functor C C),, (pr2 (δ T))),, pr2 (ε T))).
Definition Comonad_to_Comonad' {C : category} (T : Comonad C) : Comonad' C :=
(Comonad_to_Comonad'_data T,, pr22 T).
Definition Comonad'_to_Comonad_to_Comonad' {C : category} (T : Comonad' C) :
Comonad_to_Comonad' (Comonad'_to_Comonad T) = T := (idpath T).
Definition Comonad_to_Comonad'_to_Comonad {C : category} (T : Comonad C) :
Comonad'_to_Comonad (Comonad_to_Comonad' T) = T := (idpath T).
End Comonad_Comonad'_equiv.
Lemma Comonad'_eq_raw_data (C : category) (T T' : Comonad' C) :
pr1 (pr1 T) = pr1 (pr1 T') -> T = T'.
Show proof.
intro e.
apply subtypePath.
- intro. now apply isaprop_disp_Comonad_laws.
- apply subtypePath.
+ intro. apply isapropdirprod.
* apply isapropdirprod.
-- apply (isaprop_is_functor C C), homset_property.
-- apply (isaprop_is_nat_trans C C), homset_property.
* apply (isaprop_is_nat_trans C C), homset_property.
+ apply e.
apply subtypePath.
- intro. now apply isaprop_disp_Comonad_laws.
- apply subtypePath.
+ intro. apply isapropdirprod.
* apply isapropdirprod.
-- apply (isaprop_is_functor C C), homset_property.
-- apply (isaprop_is_nat_trans C C), homset_property.
* apply (isaprop_is_nat_trans C C), homset_property.
+ apply e.
Lemma Comonad_eq_raw_data (C : category) (T T' : Comonad C) :
Comonad_to_raw_data T = Comonad_to_raw_data T' -> T = T'.
Show proof.
intro e.
apply (invmaponpathsweq (_,, (isweq_iso _ _ (@Comonad_to_Comonad'_to_Comonad C)
(@Comonad'_to_Comonad_to_Comonad' C)))).
now apply (Comonad'_eq_raw_data C).
apply (invmaponpathsweq (_,, (isweq_iso _ _ (@Comonad_to_Comonad'_to_Comonad C)
(@Comonad'_to_Comonad_to_Comonad' C)))).
now apply (Comonad'_eq_raw_data C).
End Comonad_eq_helper.
Section Comonads_from_adjunctions.
This follow a remark of a single line on p.139 in Mac Lane, 2nd edition.
Definition sndfunctor_from_adjunction {C D : category}
{L : functor C D} {R : functor D C} (H : are_adjoints L R) : functor D D := R ∙ L.
Definition Comonad_data_from_adjunction {C D : category} {L : functor C D}
{R : functor D C} (H : are_adjoints L R) : disp_Comonad_data (sndfunctor_from_adjunction H).
Show proof.
Lemma Comonad_laws_from_adjunction {C D : category} {L : functor C D}
{R : functor D C} (H : are_adjoints L R) : disp_Comonad_laws (Comonad_data_from_adjunction H).
Show proof.
cbn.
use make_dirprod.
+ use make_dirprod.
* intro c; cbn.
apply triangle_id_left_ad.
* intro c; cbn.
rewrite <- functor_id.
rewrite <- functor_comp.
apply maponpaths.
apply triangle_id_right_ad.
+ intro c; cbn.
do 2 (rewrite <- functor_comp).
apply maponpaths.
apply pathsinv0.
apply (nat_trans_ax ((unit_from_are_adjoints H))).
use make_dirprod.
+ use make_dirprod.
* intro c; cbn.
apply triangle_id_left_ad.
* intro c; cbn.
rewrite <- functor_id.
rewrite <- functor_comp.
apply maponpaths.
apply triangle_id_right_ad.
+ intro c; cbn.
do 2 (rewrite <- functor_comp).
apply maponpaths.
apply pathsinv0.
apply (nat_trans_ax ((unit_from_are_adjoints H))).
Definition Comonad_from_adjunction {C D : category} {L : functor C D}
{R : functor D C} (H : are_adjoints L R) : Comonad D.
Show proof.
exists (sndfunctor_from_adjunction H).
exact (Comonad_data_from_adjunction H,, Comonad_laws_from_adjunction H).
exact (Comonad_data_from_adjunction H,, Comonad_laws_from_adjunction H).
End Comonads_from_adjunctions.