(************************************************************************)
(*  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        *)
(************************************************************************)

(* Cat: Category Theory with classes.
 *
 * This module implements the category [UNIV] of codes for polynomial functors
 * and Coq function spaces between their representations.
 * 
 * Author: Matthieu Sozeau <mattam@mattam.org>
 *)

Require Import Cat.Functor.
Require Import Coq.Classes.SetoidTactics.

Set Implicit Arguments.
Unset Strict Implicit.

Inductive code (I : Set) : Type :=
| arg : forall A : Set, (A -> code I) -> code I
| rec : I -> code I -> code I
| out : I -> code I.

Fixpoint sem {I : Set} (c : code I) (X : I -> Type) (j : I) : Type :=
  match c with
    | out i => i = j
    | arg A B => { a : A & sem (B a) X j }
    | rec i C => (X i * sem C X j)%type
  end.

Fixpoint map (I : Set) (X Y : I -> Type) (c : code I) (f : forall i : I, X i -> Y i)
  (i : I) : sem c X i -> sem c Y i :=
  match c return sem c X i -> sem c Y i with
    | out i => fun x => x
    | arg A B => fun x => let (a, b) := x in (a & map f b)
    | rec i C => fun x => let (a, b) := x in (f _ a, map f b)
  end.

(* Inductive μ (I : Set) (C : code I) : I -> Type := *)
(*   fold : forall i (x : I -> Type), μ C = x -> sem C x i -> μ C i. *)