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