interfaces.sequences

Require Import
  List abstract_algebra theory.categories forget_algebra forget_variety
  theory.rings interfaces.universal_algebra interfaces.functors
  categories.setoids categories.varieties.
Require
  categories.product varieties.monoids categories.algebras
  categories.categories theory.setoids.

Module ua := universal_algebra.

Instance: Arrows Type := λ X Y, X Y.


Class PoshSequence
   (free: setoids.Object monoids.Object) `{!Fmap free}
   (inject: id monoids.forget free)
   (extend: `((x monoids.forget y) (free x y))): Prop :=
   { sequence_adjunction: ηAdjunction _ _ inject extend
   ; extend_morphism: `(Setoid_Morphism (extend x y)) }.


Section practical.

  Class ExtendToSeq (free: Type Type) :=
    extend: {x y} `{!SemiGroupOp y} `{!MonoidUnit y}, (x y) (free x y).

  Class InjectToSeq (free: Type Type) := inject: x, x free x.

  Context
   (free: Type Type) {raw_fmap: Fmap free}
   `{ a, MonoidUnit (free a)}
   `{ a, SemiGroupOp (free a)}
   `{ a, Equiv a Equiv (free a)}
   `{!InjectToSeq free} `{!ExtendToSeq free}.

  Class Sequence :=
    { sequence_makes_monoids:> `{Setoid a}, Monoid (free a)
    ; sequence_inject_morphism:> `{Setoid a}, Setoid_Morphism (inject a)
    ; sequence_map_morphism:> `{Equiv x} `{Equiv y} (f: x y),
        Setoid_Morphism f Monoid_Morphism (raw_fmap _ _ f)
    ; sequence_fmap_proper: `{Equiv x} `{Equiv y} (f g: x y), f = g fmap free f = raw_fmap _ _ g
    ; sequence_fmap_id: `{Equiv x}, raw_fmap _ _ (@id x) = id
    ; sequence_fmap_comp: `{Equiv x} `{Equiv y} `{Equiv z} (f: y z) (g: x y),
        raw_fmap _ _ (f g) = raw_fmap _ _ f raw_fmap _ _ g
    ; sequence_extend_makes_morphisms:> `{Equiv x} `{Monoid y} (f: x y),
        Setoid_Morphism f Monoid_Morphism (extend f)
    ; sequence_inject_natural: `{Setoid A} `{Setoid B} (f: A B), Setoid_Morphism f
        inject B f = raw_fmap _ _ f inject A
    ; sequence_extend_commutes: `{Setoid x} `{Monoid y} (f: x y), Setoid_Morphism f
        extend f inject x = f
    ; sequence_only_extend_commutes: `{Setoid x} `{Monoid y} (f: x y), Setoid_Morphism f
        ( (g: free x y), Monoid_Morphism g g inject x = f g = extend f)
    ; sequence_extend_morphism: `{Setoid x} `{Monoid y} (f g: x y),
        Setoid_Morphism f Setoid_Morphism g
        f = g extend f (free:=free) = extend g (free:=free)
    }.


  Context `{PS: Sequence}.

  Program Definition posh_free (X: setoids.Object): monoids.Object := monoids.object (free X).

  Program Instance posh_fmap: functors.Fmap posh_free :=
    λ _ _ X _, raw_fmap _ _ X.


  Instance: Functor posh_free posh_fmap.

  Program Definition posh_inject: id monoids.forget posh_free := λ a, inject a.


  Typeclasses Transparent compose.

  Program Definition posh_extend (x: setoids.Object) (y: monoids.Object)
    (X: x monoids.forget y): posh_free x y
    := λ u, match u return posh_free x u y u with
      tt => @extend free ExtendToSeq0 x (monoids.forget y) _ _ X end.




  Instance: NaturalTransformation posh_inject.

  Goal @PoshSequence posh_free posh_fmap posh_inject posh_extend.

  Definition fold `{MonoidUnit M} `{SemiGroupOp M}: free M M := extend id.

  Global Instance fold_mor `{Monoid M}: Monoid_Morphism (fold (M:=M)).

End practical.