{A B : Type} (f : A -> B) {p : MapIn (Tr (-1)) f} : IsInjective f := fun x y pfeq => ap pr1 (@center _ (p (f y) (x; pfeq) (y; idpath))). Section strong_injective. Context {A B} {Aap : Apart A} {Bap : Apart B} (f : A -> B) . Class IsStrongInjective := { strong_injective : forall x y, x ≶ y -> f x ≶ f y ; strong_injective_mor : StrongExtensionality f }. End strong_injective. Section extras. Class CutMinusSpec A (cm : CutMinus A) `{Zero A} `{Plus A} `{Le A} := { cut_minus_le : forall x y, y ≤ x -> x ∸ y + y = x ; cut_minus_0 : forall x y, x ≤ y -> x ∸ y = 0 }. Global ishprop_issemigrouppreserving `{Funext} {A B : Type} `{IsHSet B} `{SgOp A} `{SgOp B} {f : A -> B} : IsHProp (IsSemiGroupPreserving f). Proof. unfold IsSemiGroupPreserving; exact _. Defined.
Require Import Spaces.Nat.Core. Require Import Modalities.ReflectiveSubuniverse.