hunk ./CAT.v 17
-
+Require Import SetoidClass.
+Require Import Setoid.
hunk ./CAT.v 21
-Program Instance CAT : Category category functor :=
+Typeclasses Transparent Datatypes.id.
+
+Program Instance CAT : Category category functor := {
hunk ./CAT.v 26
-  compose := functor_composition.
+  compose := functor_composition
+}.
hunk ./CAT.v 34
-    split_dep ; refl.
+
+    split_dep; reflex.
hunk ./CAT.v 56
-    split_dep ; refl.
+    split_dep ; reflex.
hunk ./CAT.v 69
-      unfold Basics.id, Basics.compose.
+      unfold Datatypes.id, Basics.compose.
hunk ./CAT.v 72
-      refl.
+      reflex.
hunk ./CAT.v 85
-      unfold Basics.id, Basics.compose.
+      unfold Datatypes.id, Basics.compose.
hunk ./CAT.v 88
-      refl.
+      reflex.
hunk ./CAT.v 106
-      unfold Basics.id, Basics.compose.
+      unfold Datatypes.id, Basics.compose.
hunk ./CAT.v 108
-      refl.
+      reflex.
hunk ./Category.v 33
-Instance (A : Type) (R : relation A) => id_morphism : Morphism (R ++> R) id.
+Instance id_morphism `(A : Type) `(R : relation A) : Morphism (R ++> R) id.
hunk ./Category.v 36
+Hint Resolve id_morphism : category.
+
hunk ./Category.v 46
-Class Category obj (hom : homomorphisms obj) :=
+Class Category obj (hom : homomorphisms obj) := {
hunk ./Category.v 67
-    compose f (compose g h) == compose (compose f g) h.
+    compose f (compose g h) == compose (compose f g) h
+}.
+
+Implicit Arguments Category [].
hunk ./Category.v 76
-Hint Resolve @id_unit_left @id_unit_right @assoc : category.
+Hint Resolve @id_morphisms_morphism @id_unit_left @id_unit_right @assoc : category.
hunk ./Category.v 91
-Program Instance [ Category obj hom ] => opposite_category : Category (opposite obj) (flip hom) :=
+Program Instance opposite_category `(cat :  Category obj hom )  : Category (opposite obj) (flip hom) := {
hunk ./Category.v 94
-  compose a b c := flip (compose (hom:=hom)).
+  compose a b c := flip (compose (hom:=hom))
+}.
hunk ./Category.v 97
-  Solve Obligations using unfold flip in * ; program_simpl.
+  Solve Obligations using unfold flip in * ; program_simpl; auto with category.
hunk ./Category.v 124
-Instance Equivalence category category_equality.
+Instance category_equality_equivalence : Equivalence category_equality.
hunk ./Category.v 140
+Hint Resolve category_equality_equivalence.
+
hunk ./Category.v 144
-Instance (T : Type -> Type) =>
-  type_constructor_morphism : Morphism (eq ++> eq) T.
+Instance type_constructor_morphism (T : Type -> Type) : Morphism (eq ++> eq) T.
hunk ./Category.v 163
-Program Instance category_setoid : Setoid category := 
-  equiv := category_equality.
+Program Instance category_setoid : Setoid category := {
+  equiv := category_equality
+}.
hunk ./Functor.v 19
+
hunk ./Functor.v 22
+Require Import Coq.Program.Tactics.
+Obligation Tactic := program_simpl ; auto with category.
+
hunk ./Functor.v 29
-Class [ C : Category obj hom, D : Category obj' hom'] =>
-  Functor (Fobj : obj -> obj')
-    (Fmor : forall a b, hom a b -> hom' (Fobj a) (Fobj b) ) :=
+Class  Functor `(C : Category obj hom, D : Category obj' hom') 
+  (Fobj : obj -> obj') (Fmor : forall a b, hom a b -> hom' (Fobj a) (Fobj b) ) := {
hunk ./Functor.v 36
-    Fmor a c (compose f g) == Fmor b c g ∘ Fmor a b f.
+    Fmor a c (compose f g) == Fmor b c g ∘ Fmor a b f
+}.
+
+Implicit Arguments Functor [obj hom obj' hom'].
hunk ./Functor.v 41
-Program Instance [ C : Category obj hom ] => 
-  identity_Functor : Functor C C (Basics.id) (fun a b => (Basics.id)).
+Program Instance identity_Functor `(C : Category obj hom) : 
+  Functor C C Datatypes.id (fun a b => Datatypes.id).
hunk ./Functor.v 44
-  Solve Obligations using program_simpl ; unfold Basics.id ; try reflexivity.
+  Solve Obligations using program_simpl ; unfold Datatypes.id ; try reflexivity.
hunk ./Functor.v 48
-Class [ Functor obj hom obj hom Fobj Fmor ] => EndoFunctor.
+Class EndoFunctor `( Functor obj hom obj hom Fobj Fmor).
hunk ./Functor.v 55
-Class [ C : Category obj hom, D : Category obj' hom', 
-  CD : ! Functor C D Fobj F, DC : ! Functor C D Gobj G ] =>
-  NaturalTransformation :=
-
+Class NaturalTransformation 
+  `( C : Category obj hom, D : Category obj' hom', 
+     CD : ! Functor C D Fobj F, DC : ! Functor C D Gobj G)
+:= {
hunk ./Functor.v 60
-
-  eta_law : forall a b (f : hom a b), eta b ∘ F a b f == G a b f ∘ eta a.
+  eta_law : forall a b (f : hom a b), eta b ∘ F a b f == G a b f ∘ eta a
+}.
hunk ./Functor.v 65
-Definition bijective [ Setoid A, Setoid B ] (f : A -> B) : _ := 
+Definition bijective `(Setoid A, Setoid B) (f : A -> B) : _ := 
hunk ./Functor.v 67
+Implicit Arguments bijective [A H B H0].
hunk ./Functor.v 75
-Class [ C : Category obj hom, D : Category obj' hom',
-  F : ! Functor C D Fobj Fm, G : !Functor D C Gobj Gm ] =>
-  Adjunction :=
-  
+Class Adjunction `(C : Category obj hom, D : Category obj' hom',
+                   F : !Functor C D Fobj Fm, G : !Functor D C Gobj Gm) := {
hunk ./Functor.v 80
-  phi_law : forall x y, bijective (@phi x y).
+  phi_law : forall x y, bijective (@phi x y)
+}.
hunk ./Functor.v 84
-
hunk ./Functor.v 93
-Definition identity_functor (c : category) : functor c c := 
-  let 'mkCat obj hom cat := c in
-    (_ & (_ & identity_Functor (C:=cat))).
+Definition identity_functor (c : category) : functor c c :=
+  match c with mkCat obj hom categ =>
+    (Datatypes.id & (fun a b : obj => Datatypes.id & identity_Functor categ))
+  end.
hunk ./Functor.v 98
-Instance (A B C : Type) 
-  [ m : !Morphism (R' ++> R'') (g : B -> C) ]
-  [ n : !Morphism (R ++> R') (f : A -> B) ] =>
-  composition_morphism : Morphism (R ++> R'') (g ∘ f)%prg.
+Instance composition_morphism  (A B C : Type) 
+  `(m : !Morphism (R' ++> R'') (g : B -> C))
+  `(n : !Morphism (R ++> R') (f : A -> B))
+  : Morphism (R ++> R'') (g ∘ f)%prg.
hunk ./Functor.v 105
-  apply (respect (m:=g)).
-  apply respect. 
+  apply (respect (Morphism:=m)).
+  apply (respect (Morphism:=n)).
hunk ./Functor.v 110
+Implicit Arguments composition_morphism [A B C R' R'' g m R f n]. 
+
+
hunk ./Functor.v 119
-Ltac refl := setoid_refl || reflexivity.
+Ltac reflex := setoid_refl || reflexivity.
hunk ./Functor.v 121
-Program Instance 
-  [ C : Category obj₁ hom₁, D : Category obj₂ hom₂, E : Category obj₃ hom₃,
-    F : !Functor C D fobj fmor, G : !Functor D E gobj gmor ] =>
-  composed_Functor : 
-   Functor C E (gobj ∘ fobj)%prg
+Program Instance composed_Functor 
+  `( C : Category obj₁ hom₁, D : Category obj₂ hom₂, E : Category obj₃ hom₃,
+     F : !Functor C D fobj fmor, G : !Functor D E gobj gmor )
+  : Functor C E (gobj ∘ fobj)%prg
hunk ./Functor.v 133
-    rewrite H.
-    refl.
+    apply (respect (Morphism:=m1)).
+    assumption.
hunk ./Functor.v 145
-    refl.
+    reflex.
hunk ./Functor.v 156
-    
+Implicit Arguments composed_Functor [obj₁ hom₁ obj₂ hom₂ obj₃ hom₃ fobj fmor gobj gmor C D E F G].
+
hunk ./Functor.v 169
+Definition subst_hom {obj hom} {C : Category obj hom} {objorig} (f g : objorig -> obj)
+  {a b} (p : f = g) (m : hom (f a) (f b)) : hom (g a) (g b).
+Proof. intros ; subst. exact m. Defined.
+
+
hunk ./Functor.v 175
-  match c, d with
+  match c, d return relation (functor c d) with
hunk ./Functor.v 184
-Definition functor_equivalence (c d : category) : Equivalence (functor c d) functor_equality.
+Definition functor_equivalence (c d : category) : Equivalence (@functor_equality c d).
hunk ./Functor.v 192
-  exists (refl_equal Fobj). refl.
+  exists (refl_equal Fobj). 
+  reflex.
hunk ./Functor.v 197
-  destruct H.
-  subst.
-  split_dep ; intuition.
+  destruct H. exists (sym_eq x). now symmetry.
hunk ./Functor.v 202
-  destruct_conjs.
-  subst ; simpl_JMeq ; subst.
-  split_dep ; refl.
+  destruct_conjs. split_dep. now transitivity Gobj.
+  eapply trans_JMeq; eauto.
hunk ./Functor.v 206
-Program Instance (a b : category) => functor_setoid : Setoid (functor a b) := 
-  equiv := functor_equality.
+(* Definition functor_equality {c d : category} : functor c d -> functor c d -> Prop := *)
+(*   match c, d return relation (functor c d) with *)
+(*     | mkCat obj₁ hom₁ cat₁, *)
+(*       mkCat obj₂ hom₂ cat₂ => *)
+(*       fun f g => *)
+(*         let '(Fobj & (Fmor & F)) := f in *)
+(*         let '(Gobj & (Gmor & G)) := g in *)
+(*           exists H : Gobj = Fobj, *)
+(*             forall a b (m : hom₁ a b), equiv (A:=hom₂ (Fobj a) (Fobj b)) (Fmor _ _ m)  *)
+(*               (subst_hom (C:=cat₂) H (Gmor _ _ m)) *)
+(*   end. *)
+
+(* Definition functor_equivalence (c d : category) : Equivalence (@functor_equality c d). *)
+(* Proof. *)
+(*   intros [obj₁ hom₁ cat₁].  *)
+(*   intros [obj₂ hom₂ cat₂]. *)
+
+(*   simpl. *)
+(*   constructor ; red ; try red ; intros. *)
+(*   destruct x as [Fobj [Fmor F]] ; simpl. *)
+(*   exists (refl_equal Fobj).  *)
+(*   reflex. *)
+
+(*   destruct x as [Fobj [Fmor F]] ; simpl. *)
+(*   destruct y as [Gobj [Gmor G]] ; simpl. *)
+(*   destruct H. exists (sym_eq x). intros. *)
+(*   move x at top. *)
+(*   generalize dependent Fobj. simplify_dep_elim.  *)
+(*   specialize (H a b m). unfold subst_hom in *; simpl in *. *)
+(*   unfold eq_rect_r in *. simpl in *. rewrite H. reflex. *)
+    
+(*   destruct x as [Fobj [Fmor F]] ; simpl. *)
+(*   destruct y as [Gobj [Gmor G]] ; simpl. *)
+(*   destruct z as [Iobj [Imor I]] ; simpl. *)
+(*   destruct_conjs. move H at top; move H0 at top. generalize dependent obj₁.  *)
+(*   simplify_dep_elim. unfold subst_hom, eq_rect_r in *. simpl in *.  *)
+(*   exists (refl_equal Iobj). simpl. intros. rewrite H2, H1. reflex. *)
+(* Qed. *)
+
+Program Instance functor_setoid (a b : category) : Setoid (functor a b) := {
+  equiv := functor_equality
+}.
hunk ./Objects.v 28
-Definition terminal [ cat : Category obj hom ] (x : obj) : Type :=  
+Definition terminal `(cat : Category obj hom) (x : obj) : Type :=  
hunk ./Objects.v 34
-Class [ cat : Category obj hom ] => Terminal (one : obj) :=
+Class Terminal `(cat : Category obj hom )  (one : obj) := {
hunk ./Objects.v 36
-  unique : forall x (f g : hom x one), f == g.
+  unique : forall x (f g : hom x one), f == g
+}.
+Implicit Arguments Terminal [obj hom].
hunk ./Objects.v 42
-Definition isomorphic [ cat : Category obj hom ] a b : _ :=
+Definition isomorphic `(cat : Category obj hom) a b : _ :=
hunk ./Objects.v 45
+Implicit Arguments isomorphic [obj hom cat].
hunk ./Objects.v 50
-Lemma terminal_isomorphic [ C : Category obj hom, ! Terminal C x, ! Terminal C y ] : isomorphic x y.
+Lemma terminal_isomorphic `(C : Category obj hom, ! Terminal C x, ! Terminal C y) : isomorphic x y.
hunk ./Objects.v 54
-  exists (bang x).
+  exists (bang (one:=y) x).
hunk ./Objects.v 58
-  apply (unique (one:=x)).
+  apply unique.
hunk ./Objects.v 64
-Class [ C : Category obj hom ] => Isomorphic (a : obj) (b : obj) :=
+Class Isomorphic `(C : Category obj hom) (a : obj) (b : obj) := {
hunk ./Objects.v 66
-    f ∘ g == id /\ g ∘ f == id } }.
+    f ∘ g == id /\ g ∘ f == id } }
+}.
hunk ./TYPE.v 17
+
hunk ./TYPE.v 27
-Program Instance [ s : Setoid b ] => arrow_setoid : Setoid (a -> b) :=
-  equiv f g := forall x, f x == g x.
-
+Program Instance arrow_setoid `(s : Setoid b) : Setoid (a -> b) := {
+  equiv f g := forall x, f x == g x
+}.
hunk ./TYPE.v 39
+Implicit Arguments arrow_setoid [a b s].
hunk ./TYPE.v 42
-
hunk ./TYPE.v 45
+Next Obligation.
+  apply eq_equivalence.
+Qed.
+
hunk ./TYPE.v 51
-Program Instance TYPE : Category Type arrow :=
+Program Instance TYPE : Category Type arrow := {
hunk ./TYPE.v 54
-  compose a b c f g x := g (f x).
+  compose a b c f g x := g (f x)
+}.
hunk ./TYPE.v 132
-Program Instance [ C : Category obj hom, ! Object C a ] => section_functor : 
+Program Instance section_functor `(C : Category obj hom, ! Object C a ) : 
hunk ./TYPE.v 141
-    refl.
+    reflex.
hunk ./TYPE.v 158
-Class [ C : Category (opposite obj) (flip hom), D : Category obj' hom' ] => 
-  ContravariantFunctor Fobj Fmor := 
-  contravariant_functor :> Functor C D Fobj Fmor.
+Class ContravariantFunctor `(C : Category (opposite obj) (flip hom), D : Category obj' hom' ) Fobj Fmor := {
+  contravariant_functor :> Functor C D Fobj Fmor
+}.
hunk ./TYPE.v 165
-Typeclasses unfold SetoidClass.equiv.
+(* Typeclasses unfold SetoidClass.equiv. *)
hunk ./TYPE.v 169
-Program Instance [  Cop : Category (opposite obj) (flip hom), ! Object Cop b ] => points_functor :
+Program Instance points_functor `(Cop : Category (opposite obj) (flip hom), ! Object Cop b ) :
hunk ./Universe.v 28
-Print arg.
-
hunk ./Universe.v 43
-Inductive μ (I : Set) (C : code I) : I -> Type :=
-  fold : forall i, sem C (μ C) i -> μ C i.
+(* Inductive μ (I : Set) (C : code I) : I -> Type := *)
+(*   fold : forall i (x : I -> Type), μ C = x -> sem C x i -> μ C i. *)