-(* this is a projection *)
-ndefinition mmmcarr ≝
- λA,B,Ma,Mb.λf: magma_morphism A B Ma Mb. match f with [ mk_magma_morphism f _ ⇒ f ].
-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 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
- [ mk_magma_morphism _ p ⇒ p ].
-
-ndefinition sub_magma ≝
- λA.λM1,M2: magma A. M1 ⊆ M2.
-
-ndefinition image: ∀A,B. (A → B) → Ω \sup A → Ω \sup B ≝
- λA,B,f,Sa. {y | ∃x. x ∈ Sa ∧ f x = y}.