+nqed.
+
+(******************* CATEGORIES **********************)
+
+ninductive one : Type[0] ≝ unit : one.
+
+ndefinition force : ∀S:Type[2]. S → ∀T:Type[2]. T → one → Type[2] ≝
+ λS,s,T,t,lock. match lock with [ unit => S ].
+
+ndefinition enrich_as :
+ ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one.force S s T t lock ≝
+ λS,s,T,t,lock. match lock return λlock.match lock with [ unit ⇒ S ]
+ with [ unit ⇒ s ].
+
+ncoercion enrich_as : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock
+ ≝ enrich_as on t: ? to force ? ? ? ? ?.
+
+(* does not work here
+nlemma foo : ∀A,B,C:setoid1.∀f:B ⇒ C.∀g:A ⇒ B. unary_morphism1 A C.
+#A; #B; #C; #f; #g; napply(f \circ g).
+nqed.*)
+
+(* This precise hint does not leave spurious metavariables *)
+unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B;
+ lock ≟ unit
+(* --------------------------------------------------------------- *) ⊢
+ (unary_morphism1 A C)
+ ≡
+ (force (unary_morphism1 A C) (comp1_unary_morphisms A B C f g)
+ (carr1 A → carr1 C) (composition1 A B C f g) lock)
+ .
+
+(* This uniform hint opens spurious metavariables
+unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B, X;
+ lock ≟ unit
+(* --------------------------------------------------------------- *) ⊢
+ (unary_morphism1 A C)
+ ≡
+ (force (unary_morphism1 A C) X (carr1 A → carr1 C) (fun11 … X) lock)
+ .
+*)
+
+nlemma foo : ∀A,B,C:setoid1.∀f:B ⇒ C.∀g:A ⇒ B. unary_morphism1 A C.
+#A; #B; #C; #f; #g; napply(f ∘ g).
+nqed.
+
+(*
+
+ndefinition uffa: ∀A,B. ∀U: unary_morphism1 A B. (A → B) → CProp[0].
+ #A;#B;#_;#_; napply True.
+nqed.
+ndefinition mk_uffa: ∀A,B.∀U: unary_morphism1 A B. ∀f: (A → B). uffa A B U f.
+ #A; #B; #U; #f; napply I.
+nqed.
+
+ndefinition coerc_to_unary_morphism1:
+ ∀A,B. ∀U: unary_morphism1 A B. uffa A B U (fun11 … U) → unary_morphism1 A B.
+ #A; #B; #U; #_; nassumption.
+nqed.
+
+ncheck (λA,B,C,f,g.coerc_to_unary_morphism1 ??? (mk_uffa ??? (composition1 A B C f g))).
+*)
+ndefinition ORelation_composition : ∀P,Q,R.
+ binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
+#P; #Q; #R; @
+[ #F; #G; @
+ [ napply (G ∘ F) (* napply (comp1_unary_morphisms … G F) (*CSC: was (G ∘ F);*) *)
+ | napply (G⎻* ∘ F⎻* ) (* napply (comp1_unary_morphisms … G⎻* F⎻* ) (*CSC: was (G⎻* ∘ F⎻* );*)*)
+ | napply (comp1_unary_morphisms … F* G* ) (*CSC: was (F* ∘ G* );*)
+ | napply (comp1_unary_morphisms … F⎻ G⎻) (*CSC: was (F⎻ ∘ G⎻);*)
+ | #p; #q; nnormalize;
+ napply (.= (or_prop1 … G …)); (*CSC: it used to understand without G *)
+ napply (or_prop1 …)
+ | #p; #q; nnormalize;
+ napply (.= (or_prop2 … F …));
+ napply or_prop2
+ | #p; #q; nnormalize;
+ napply (.= (or_prop3 … G …));
+ napply or_prop3
+ ]
+##| #a;#a';#b;#b';#e;#e1;#x;nnormalize;napply (.= †(e x));napply e1]
+nqed.
+
+(*
+ndefinition OA : category2.
+split;
+[ apply (OAlgebra);
+| intros; apply (ORelation_setoid o o1);
+| intro O; split;
+ [1,2,3,4: apply id2;
+ |5,6,7:intros; apply refl1;]
+| apply ORelation_composition;
+| intros (P Q R S F G H); split;
+ [ change with (H⎻* ∘ G⎻* ∘ F⎻* = H⎻* ∘ (G⎻* ∘ F⎻* ));
+ apply (comp_assoc2 ????? (F⎻* ) (G⎻* ) (H⎻* ));
+ | apply ((comp_assoc2 ????? (H⎻) (G⎻) (F⎻))^-1);
+ | apply ((comp_assoc2 ????? F G H)^-1);
+ | apply ((comp_assoc2 ????? H* G* F* ));]
+| intros; split; unfold ORelation_composition; simplify; apply id_neutral_left2;
+| intros; split; unfold ORelation_composition; simplify; apply id_neutral_right2;]
+qed.
+
+definition OAlgebra_of_objs2_OA: objs2 OA → OAlgebra ≝ λx.x.
+coercion OAlgebra_of_objs2_OA.
+
+definition ORelation_setoid_of_arrows2_OA:
+ ∀P,Q. arrows2 OA P Q → ORelation_setoid P Q ≝ λP,Q,c.c.
+coercion ORelation_setoid_of_arrows2_OA.
+
+prefer coercion Type_OF_objs2.
+*)
+(* alias symbol "eq" = "setoid1 eq". *)