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.
    exists (pr1 g).
    exact (λ v1 v2, pr2 g v2 v1).

  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.
    exists (λ v, pr1 d v).
    exact (λ v1 v2 e, pr2 d v2 v1 (edge_op e)).

  Definition cone_op
             {C : category}
             {g : graph} {d : diagram g C}
             {c : C} (cc : cone d c)
    : cocone (diagram_op d) c.
  Show proof.
    exists (λ v, pr1 cc v).
    exact (λ v w e, pr2 cc w v e).

  Definition cocone_op
             {C : category}
             {g : graph} {d : diagram g C}
             {c : C} (cc : cocone d c)
    : cone (diagram_op d) c.
  Show proof.
    exists (λ v, pr1 cc v).
    exact (λ v w e, pr2 cc w v e).

  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.
    intros c0 cc0.
    apply (cc_lim c0 (cone_op cc0)).

  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.
    intros c0 cc0.
    apply (cc_lim c0 (cocone_op cc0)).

  Definition ColimCocone_op
             {C : category} {g : graph} {d : diagram g C}
             (cc : ColimCocone d)
    : LimCone (diagram_op d).
  Show proof.
    use make_LimCone.
    - exact (colim cc).
    - exact (cocone_op (colimCocone cc)).
    - apply (iscolimcocone_op (isColimCocone_from_ColimCocone cc)).

  Definition LimCone_op
             {C : category} {g : graph} {d : diagram g C}
             (cc : LimCone d)
    : ColimCocone (diagram_op d).
  Show proof.
    use make_ColimCocone.
    - exact (lim cc).
    - exact (cone_op (limCone cc)).
    - apply (islimcone_op (isLimCone_from_LimCone cc)).

  Definition Colims_op
    {C : category}
    (H : Colims C)
    : Lims (C^opp)
    := λ g d, ColimCocone_op (H (graph_op g) (diagram_op d)).

  Definition Lims_op
    {C : category}
    (H : Lims C)
    : Colims (C^opp)
    := λ g d, LimCone_op (H (graph_op g) (diagram_op d)).

  Definition chain_op {C : category} (ch : chain C)
    : cochain (opp_cat C).
  Show proof.
    exists (λ v, pr1 ch v).
    exact (λ v w e, pr2 ch w v (edge_op e)).

  Definition cochain_op {C : category} (ch : cochain C)
    : chain (opp_cat C).
  Show proof.
    exists (λ v, pr1 ch v).
    exact (λ v w e, pr2 ch w v (edge_op e)).

  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.
    apply (islimcone_op cc_lim).

  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.
    apply (islimcone_op cc_lim).

  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.
    apply (iscolimcocone_op cc_lim).

  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)).

  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)).

  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)).

  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)).

End ColimitsAsLimits.