gmalecha

Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.

Fail Inductive X : Type := BAD : (X -> X) -> X.

Definition natF (T : Type) : Type :=
  T + unit.

(* We define approximation using a fixpoint which computes a Type
 * by repeatedly applying a function. The base case is the empty set.

gmalecha

Set Implicit Arguments.
Set Strict Implicit.

Inductive Even : nat -> Prop :=
| Even_O : Even 0
| Even_SS : forall n, Even n -> Even (S (S n)).

Goal Even 0.
  apply Even_O.
Qed.

gmalecha

Require Import MirrorCore.Iso.

Set Implicit Arguments.
Set Strict Implicit.

Definition Pi (T : Type) (F : T -> Type) : Type :=
  forall x : T, F x.

(** What is the generalization of [Functor] to a dependent function? **)
Class DFunctor (Q : Type -> Type) (F : Pi Q)