ncoercion mmmcarr : ∀A,B,Ma,Mb.∀f: magma_morphism A B Ma Mb. pre_magma_morphism A B
≝ mmmcarr
on _f: magma_morphism ???? to pre_magma_morphism ??.
-ndefinition mmcarr_mmmcarr ≝
- λA,B,Ma,Mb.λf: magma_morphism A B Ma Mb. mmcarr ?? (mmmcarr ???? f).
-ncoercion mmcarr_mmmcarr : ∀A,B,Ma,Mb.∀f: magma_morphism A B Ma Mb. A → B ≝ mmcarr_mmmcarr
- on _f: magma_morphism ???? to ∀_.?.
ndefinition mmclosed ≝
λA,B,Ma,Mb.λf: magma_morphism A B Ma Mb.
match f return λf: magma_morphism A B Ma Mb.∀x. x ∈ Ma → f x ∈ Mb with
∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism ?? Ma Mb → magma B.
#A; #B; #Ma; #Mb; #f;
napply (mk_magma ???)
- [ napply (image ?? (mmcarr ?? (mmmcarr ???? f)) (mcarr ? Ma))
+ [ napply (image ?? (mmcarr ?? (mmmcarr ???? f)) Ma) (* NO COMPOSITE! *)
| #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
napply (ex_intro ????)
[ napply (op ? x0 y0)