-nlemma mk_binary_morphism1:
- ∀A,B,C: setoid1. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') →
- A ⇒_1 (unary_morphism1_setoid1 B C).
- #A; #B; #C; #f; #H; @ [ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph1_eq1; #y]
- /2/.
-nqed.
-
-ndefinition composition1 ≝
- λo1,o2,o3:Type[1].λf:o2 → o3.λg: o1 → o2.λx.f (g x).
-
-interpretation "function composition" 'compose f g = (composition ??? f g).
-interpretation "function composition1" 'compose f g = (composition1 ??? f g).
-
-ndefinition comp1_unary_morphisms:
- ∀o1,o2,o3:setoid1.o2 ⇒_1 o3 → o1 ⇒_1 o2 → o1 ⇒_1 o3.
-#o1; #o2; #o3; #f; #g; @ (f ∘ g);
- #a; #a'; #e; nnormalize; napply (.= †(†e)); napply #.
-nqed.
-
-unification hint 0 ≔ o1,o2,o3:setoid1,f:o2 ⇒_1 o3,g:o1 ⇒_1 o2;
- R ≟ (mk_unary_morphism1 ?? (composition1 ??? (fun11 ?? f) (fun11 ?? g))
- (prop11 ?? (comp1_unary_morphisms o1 o2 o3 f g)))
- (* -------------------------------------------------------------------- *) ⊢
- fun11 o1 o3 R ≡ composition1 ??? (fun11 ?? f) (fun11 ?? g).
-
-ndefinition comp1_binary_morphisms:
- ∀o1,o2,o3. (o2 ⇒_1 o3) ⇒_1 ((o1 ⇒_1 o2) ⇒_1 (o1 ⇒_1 o3)).
-#o1; #o2; #o3; napply mk_binary_morphism1
- [ #f; #g; napply (comp1_unary_morphisms … f g)
- | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ]
-nqed.