Skip to content

Instantly share code, notes, and snippets.

@tomprince
Created March 23, 2011 18:29
Show Gist options
  • Save tomprince/883648 to your computer and use it in GitHub Desktop.
Save tomprince/883648 to your computer and use it in GitHub Desktop.
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).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment