Skip to content

Instantly share code, notes, and snippets.

@tel
Created November 28, 2012 22:00
Show Gist options
  • Save tel/4164969 to your computer and use it in GitHub Desktop.
Save tel/4164969 to your computer and use it in GitHub Desktop.
(A : O -> O -> Set) :=
{
id : forall (x : O), A x x(* ; *)
(* comp : forall x y z, A x y -> A y z -> A x z; *)
(* id_unit_lt : forall x (a : A x x), comp a (id x) = a; *)
(* id_unit_rt : forall x (a : A x x), comp (id x) a = a *)
}.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment