theory.categories

Require Import
  Relation_Definitions
  abstract_algebra theory.setoids interfaces.functors theory.jections.

Notation "x ⇛ y" := ( a, x a y a) (at level 90, right associativity).

Definition id_nat_trans `{Arrows D} `{!CatId D} `(F: C D): F F := λ _, cat_id.

Section NaturalTransformation.
  Context `{Category C} `{Category D} `{!Functor (F: C D) Fa} `{!Functor (G: C D) Ga}.
  Class NaturalTransformation (η: F G): Prop :=
    natural: `(f: x y), η y fmap F f = fmap G f η x.
End NaturalTransformation.

Section UniversalArrow.
  Context `{Category D} `{Category C} `{!Functor (F: D C) Fa}.
  Class UniversalArrow `(u: c F r) (wit: `(f: c F d), r d): Prop :=
    universal_arrow: (d: D) (f: c F d), is_sole ((f =) (◎ u) fmap F) (wit f).
End UniversalArrow.

Section adjunction.
  Context `{Category C} `{Category D}
    F `{!Functor (F: C D) F'}
    G `{!Functor (G: D C) G'}.

  Class Adjunction (φ: `(F c d), (c G d)) `{ c d, Inverse (@ c d)}: Prop :=
    { _adjunction_left_functor: Functor F _
    ; _adjunction_right_functor: Functor G _
    ; _adjunction_bijective: c d, Bijective (@ c d)
    ; _adjunction_natural_left `(f: F c d) `(k: d d'): (k f) = fmap G k f
    ; _adjunction_natural_right `(f: F c d) `(h: c' c): (f fmap F h) = f h }.

  Class ηAdjunction (η: id G F) (uniwit: `(c G d), F c d): Prop :=
    { η_adjunction_left_functor: Functor F _
    ; η_adjunction_right_functor: Functor G _
    ; η_adjunction_natural: NaturalTransformation η
    ; η_adjunction_universal: c: C, UniversalArrow (η c: c G (F c)) (@uniwit c) }.


  Class ηεAdjunction (η: id G F) (ε: F G id): Prop :=
    { ηε_adjunction_left_functor: Functor F _
    ; ηε_adjunction_right_functor: Functor G _
    ; ηε_adjunction_η_natural: NaturalTransformation η
    ; ηε_adjunction_ε_natural: NaturalTransformation ε
    ; ηε_adjunction_identity_at_G: a, fmap G (ε a) η (G a) = id_nat_trans G a
    ; ηε_adjunction_identity_at_F: a, ε (F a) fmap F (η a) = id_nat_trans F a }.

End adjunction.

Section contents.
  Context `{Category X}.

  Class Mono `(a: x y): Prop :=
    mono: z (f g: z x), a f = a g f = g.

  Section isomorphy.
    Definition iso_arrows {x y: X} (a: x y) (b: y x): Prop
      := a b = cat_id b a = cat_id.
    Global Instance: HeteroSymmetric (@iso_arrows).

    Definition is_iso {x y: X} (a: x y): Prop := ex (iso_arrows a).

    Definition isos_unique (x y: X) (a: x y) (b b': y x): iso_arrows a b iso_arrows a b' b = b'.

    Definition iso: Equiv X := λ x y, ex (uncurry (@iso_arrows x y)).
    Definition isoT: X X Type := λ x y, sig (uncurry (@iso_arrows x y)).

    Program Instance: Reflexive iso := λ x, ex_intro _ (cat_id, cat_id) _.

    Instance: Symmetric iso.

    Instance: Transitive iso.

    Global Instance iso_equivalence: Equivalence iso := {}.
    Global Instance iso_setoid: @Setoid X iso := {}.

    Lemma arrows_between_isomorphic_objects (a b c d: X)
      (ab: a b) (ba: b a) (cd: c d) (dc: d c) (ac: a c) (bd: b d):
       iso_arrows ab ba iso_arrows cd dc
        ac ba = dc bd
        bd ab = cd ac.

    Program Definition refl_arrows (x: X): isoT x x := (cat_id, cat_id).
  End isomorphy.

  Section initiality.
    Class InitialArrow (x: X): Type := initial_arrow: y, x y.

    Class Initial (x: X) `{InitialArrow x}: Prop :=
      initial_arrow_unique: y f', initial_arrow y = f'.

    Definition initial (x: X): Type := y: X, sig (λ a: x y, a': x y, a = a').

    Lemma initials_unique' (x x': X) `{Initial x} `{Initial x'}:
      iso_arrows (initial_arrow x': x x') (initial_arrow x).

    Program Lemma initials_unique (x x': X) (a: initial x) (b: initial x'): iso_arrows (a x') (b x).
  End initiality.

  Section products.
    Context {I: Type} (component: I X).

    Section def.
      Context (product: X).

      Class ElimProduct: Type := tuple_proj: i, product component i.
      Class IntroProduct: Type := make_tuple: x, ( i, x component i) (x product).

      Class Product `{ElimProduct} `{IntroProduct}: Prop :=
        product_factors: c ccomp, is_sole (λ h', i, ccomp i = tuple_proj i h')
          (make_tuple c ccomp).

      Lemma tuple_round_trip `{Product} (x: X) (h: i, x component i) i:
        tuple_proj i make_tuple x h = h i.
    End def.

    Lemma products_unique `{Product c} `{Product c'}:
      iso_arrows
        (make_tuple c c' (tuple_proj c'))
        (make_tuple c' c (tuple_proj c)).
  End products.

  Class Producer: Type := product I: (I X) X.

  Class HasProducts `{Producer}
    `{ I c, ElimProduct c (product I c)}
    `{ I c, IntroProduct c (product I c)}: Prop :=
      makes_products: I (c: I X), Product c (product I c).

End contents.


Implicit Arguments Producer [].
Implicit Arguments HasProducts [[Arrows0] [H] [CatComp0] [H1] [H2] [H3]]. Implicit Arguments product [[X] [Producer] [I]].