gistfile1.ml

Require Import
  Relation_Definitions Morphisms.

Global Generalizable All Variables.
Global Set Automatic Introduction.

Class Equiv A := equiv: relation A.

Infix "=" := equiv: type_scope.

Class Arrows (O: Type): Type := xArrow: O → O → Type.
Infix "⟶" := xArrow (at level 90, right associativity).
Class CatComp O `{Arrows O} := comp: ∀ x y z, (y ⟶ z) → (x ⟶ y) → (x ⟶ z).

Implicit Arguments comp [[O] [H] [CatComp]].

Instance: Params (@equiv) 2.

Record Object := object.
Record Arrow (x y: Object): Type := arrow.

Implicit Arguments arrow [[x] [y]].

Hint Extern 4 (Arrows Object) => exact Arrow: typeclass_instances.
  (* Matthieu is adding [Existing Instance (c: T).], which is nicer. *)

Global Instance e (x y:Object) : Equiv (x ⟶ y). admit. Defined.
Global Instance: CatComp Object. admit. Defined.
 
Global Instance: ∀ x y z: Object, Proper (equiv ==> equiv ==> equiv) (comp x y z).