interpretation "mk_setoid" 'mk_setoid x = (mk_setoid x ?).
interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y).
+(* single = is for the abstract equality of setoids, == is for concrete
+ equalities (that may be lifted to the setoid level when needed *)
+notation < "hvbox(a break mpadded width -50% (=)= b)" non associative with precedence 45 for @{ 'eq_low $a $b }.
+notation > "a == b" non associative with precedence 45 for @{ 'eq_low $a $b }.
notation > "hvbox(a break =_0 b)" non associative with precedence 45
for @{ eq_rel ? (eq0 ?) $a $b }.
nqed.
unification hint 0 ≔ o1,o2,o3:setoid,f:o2 ⇒_0 o3,g:o1 ⇒_0 o2;
- R ≟ mk_unary_morphism ?? (composition ??? f g)
- (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g))
+ R ≟ mk_unary_morphism o1 o3
+ (composition ??? (fun1 o2 o3 f) (fun1 o1 o2 g))
+ (prop1 o1 o3 (comp_unary_morphisms o1 o2 o3 f g))
(* -------------------------------------------------------------------- *) ⊢
- fun1 ?? R ≡ (composition ??? f g).
+ fun1 o1 o3 R ≡ composition ??? (fun1 o2 o3 f) (fun1 o1 o2 g).
ndefinition comp_binary_morphisms:
∀o1,o2,o3.(o2 ⇒_0 o3) ⇒_0 ((o1 ⇒_0 o2) ⇒_0 (o1 ⇒_0 o3)).