Created
March 23, 2011 18:29
-
-
Save tomprince/883648 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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