Require Export Map.

Set Implicit Arguments.
Unset Strict Implicit.


Section inj_surj_def.

Variable A B : Setoid.

Definition Inj_law (f : Map A B) := ∀ x y : A, f x =_S f y → x =_S y.

Structure > Inj : Type := {Inj_map :> Map A B; Prf_isInj :> Inj_law Inj_map}.


Definition Surj_law (f : Map A B) (h : B → A) := ∀ b : B, b =_S f (h b).

Structure > Surj : Type :=
  {Surj_map :> Map A B;
   Surj_elt : B → A;
   Prf_isSurj :> Surj_law Surj_map Surj_elt}.

End inj_surj_def.