Library UniMath.CategoryTheory.OppositeCategory.LimitsAsColimits
Require Import UniMath.Foundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.OppositeCategory.Core.
Require Import UniMath.CategoryTheory.limits.cones.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.Chains.Chains.
Require Import UniMath.CategoryTheory.Chains.Cochains.
Section ColimitsAsLimits.
Definition graph_op (g : graph)
: graph.
Show proof.
Definition edge_op {g : graph} {v w : pr1 g} (e : pr2 g v w)
: pr2 (graph_op g) w v := e.
Definition diagram_op
{C : category}
{g : graph} (d : diagram g C)
: diagram (graph_op g) (opp_cat C).
Show proof.
Definition cone_op
{C : category}
{g : graph} {d : diagram g C}
{c : C} (cc : cone d c)
: cocone (diagram_op d) c.
Show proof.
Definition cocone_op
{C : category}
{g : graph} {d : diagram g C}
{c : C} (cc : cocone d c)
: cone (diagram_op d) c.
Show proof.
Definition iscolimcocone_op
{C : category} {g : graph} {d : diagram g C}
{c : C} {cc : cocone d c} (cc_lim : isColimCocone d c cc)
: isLimCone (diagram_op d) c (cocone_op cc).
Show proof.
Definition islimcone_op
{C : category} {g : graph} {d : diagram g C}
{c : C} {cc : cone d c} (cc_lim : isLimCone d c cc)
: isColimCocone (diagram_op d) c (cone_op cc).
Show proof.
Definition LimCone_op
{C : category} {g : graph} {d : diagram g C}
(cc : LimCone d)
: ColimCocone (diagram_op d).
Show proof.
Definition chain_op {C : category} (ch : chain C)
: cochain (opp_cat C).
Show proof.
Definition cochain_op {C : category} (ch : cochain C)
: chain (opp_cat C).
Show proof.
Definition islimcone_chain_op
{C : category} {g : chain C}
{c : C} {cc : cone g c} (cc_lim : isLimCone g c cc)
: isColimCocone (chain_op g) c (cone_op cc).
Show proof.
Definition islimcone_cochain_op
{C : category} {g : cochain C}
{c : C} {cc : cone g c} (cc_lim : isLimCone g c cc)
: isColimCocone (cochain_op g) c (cone_op cc).
Show proof.
Definition iscolimcocone_chain_op
{C : category} {g : chain C}
{c : C} {cc : cocone g c} (cc_lim : isColimCocone g c cc)
: isLimCone (chain_op g) c (cocone_op cc).
Show proof.
Definition is_omega_cont_op
{C D : category} {F : functor C D}
(oc : is_omega_cont F)
: is_omega_cocont (functor_op F).
Show proof.
Definition is_omega_cocont_op
{C D : category} {F : functor C D}
(oc : is_omega_cocont F)
: is_omega_cont (functor_op F).
Show proof.
Definition is_cont_op
{C D : category} {F : functor C D}
(oc : is_cont F)
: is_cocont (functor_op F).
Show proof.
Definition is_cocont_op
{C D : category} {F : functor C D}
(oc : is_cocont F)
: is_cont (functor_op F).
Show proof.
End ColimitsAsLimits.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.OppositeCategory.Core.
Require Import UniMath.CategoryTheory.limits.cones.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.Chains.Chains.
Require Import UniMath.CategoryTheory.Chains.Cochains.
Section ColimitsAsLimits.
Definition graph_op (g : graph)
: graph.
Show proof.
Definition edge_op {g : graph} {v w : pr1 g} (e : pr2 g v w)
: pr2 (graph_op g) w v := e.
Definition diagram_op
{C : category}
{g : graph} (d : diagram g C)
: diagram (graph_op g) (opp_cat C).
Show proof.
Definition cone_op
{C : category}
{g : graph} {d : diagram g C}
{c : C} (cc : cone d c)
: cocone (diagram_op d) c.
Show proof.
Definition cocone_op
{C : category}
{g : graph} {d : diagram g C}
{c : C} (cc : cocone d c)
: cone (diagram_op d) c.
Show proof.
Definition iscolimcocone_op
{C : category} {g : graph} {d : diagram g C}
{c : C} {cc : cocone d c} (cc_lim : isColimCocone d c cc)
: isLimCone (diagram_op d) c (cocone_op cc).
Show proof.
Definition islimcone_op
{C : category} {g : graph} {d : diagram g C}
{c : C} {cc : cone d c} (cc_lim : isLimCone d c cc)
: isColimCocone (diagram_op d) c (cone_op cc).
Show proof.
Definition LimCone_op
{C : category} {g : graph} {d : diagram g C}
(cc : LimCone d)
: ColimCocone (diagram_op d).
Show proof.
Definition chain_op {C : category} (ch : chain C)
: cochain (opp_cat C).
Show proof.
Definition cochain_op {C : category} (ch : cochain C)
: chain (opp_cat C).
Show proof.
Definition islimcone_chain_op
{C : category} {g : chain C}
{c : C} {cc : cone g c} (cc_lim : isLimCone g c cc)
: isColimCocone (chain_op g) c (cone_op cc).
Show proof.
Definition islimcone_cochain_op
{C : category} {g : cochain C}
{c : C} {cc : cone g c} (cc_lim : isLimCone g c cc)
: isColimCocone (cochain_op g) c (cone_op cc).
Show proof.
Definition iscolimcocone_chain_op
{C : category} {g : chain C}
{c : C} {cc : cocone g c} (cc_lim : isColimCocone g c cc)
: isLimCone (chain_op g) c (cocone_op cc).
Show proof.
Definition is_omega_cont_op
{C D : category} {F : functor C D}
(oc : is_omega_cont F)
: is_omega_cocont (functor_op F).
Show proof.
intros ch c cc.
set (t := oc (chain_op ch) c (cocone_op cc)).
intro col.
set (tt := iscolimcocone_chain_op col).
intros c0 cc0.
apply (t tt c0 (cocone_op cc0)).
set (t := oc (chain_op ch) c (cocone_op cc)).
intro col.
set (tt := iscolimcocone_chain_op col).
intros c0 cc0.
apply (t tt c0 (cocone_op cc0)).
Definition is_omega_cocont_op
{C D : category} {F : functor C D}
(oc : is_omega_cocont F)
: is_omega_cont (functor_op F).
Show proof.
intros ch c cc.
set (t := oc (cochain_op ch) c (cone_op cc)).
intro lm.
set (tt := islimcone_cochain_op lm).
intros c0 cc0.
apply (t tt c0 (cone_op cc0)).
set (t := oc (cochain_op ch) c (cone_op cc)).
intro lm.
set (tt := islimcone_cochain_op lm).
intros c0 cc0.
apply (t tt c0 (cone_op cc0)).
Definition is_cont_op
{C D : category} {F : functor C D}
(oc : is_cont F)
: is_cocont (functor_op F).
Show proof.
intros g d c cc.
set (t := oc _ _ c (cocone_op cc)).
intro lm.
set (tt := iscolimcocone_op lm).
intros c0 cc0.
apply (t tt c0 (cocone_op cc0)).
set (t := oc _ _ c (cocone_op cc)).
intro lm.
set (tt := iscolimcocone_op lm).
intros c0 cc0.
apply (t tt c0 (cocone_op cc0)).
Definition is_cocont_op
{C D : category} {F : functor C D}
(oc : is_cocont F)
: is_cont (functor_op F).
Show proof.
intros g d c cc.
set (t := oc _ _ c (cone_op cc)).
intro lm.
set (tt := islimcone_op lm).
intros c0 cc0.
apply (t tt c0 (cone_op cc0)).
set (t := oc _ _ c (cone_op cc)).
intro lm.
set (tt := islimcone_op lm).
intros c0 cc0.
apply (t tt c0 (cone_op cc0)).
End ColimitsAsLimits.