(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Certified Haskell Prelude.
 * Author: Matthieu Sozeau
 * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
 *              91405 Orsay, France *)

(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)

Require Export Prelude.Basics.
Require Import Program.

Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.
Require Export Setoid.
Require Import Coq.Classes.Equivalence.

Obligation Tactic := try typeclasses eauto || program_simplify.

Class Functor (F : Setoid -> Setoid) := {

  fmap : Π {A B : Setoid}, (A ---> B) ---> F A ---> F B ;

(*   F_covariant :> Π [ SubSetoid A B ], SubSetoid (F A) (F B) ; *)

  fmap_id : Π {A}, fmap (idS (A:=A)) =∙= idS ;

  fmap_compose : Π {α β δ} (f : β --> δ) (g : α --> β),
    fmap (f ∙ g) =∙= fmap f ∙ fmap g }.

Class Pointed `{F : Functor η} := {
  point : Π {α : Setoid}, α --> η α ; 

  fmap_point : Π {α β : Setoid} (f : α --> β), fmap f ∙ point =∙= point ∙ f }.

Class CoPointed `{F : Functor η} := {
  extract : Π {α}, η α --> α ; 

  extract_fmap : Π {α β} (f : α --> β), extract ∙ fmap f =∙= f ∙ extract }.

Implicit Arguments Pointed [[F]].
Implicit Arguments CoPointed [[F]].