# Library Morphism

Require Import Setoid Utf8 Ensembles ProofIrrelevance Ensembles.
Require Export Notations.

Set Implicit Arguments.

Delimit Scope function_scope with function.

# Functions

Section morphism.
Local Open Scope function_scope.

Definition compose X Y Z (f : YZ) (g : XY) := λ x, f (g x).

Arguments compose [X Y Z] f g x / .

Infix "○" := (@compose _ _ _).

Definition is_injective X Y (f : XY) := x y, f x = f yx = y.

Definition sum_function X X' Y Y' (f : XY) (f' : X'Y')
: X X'Y Y'
:= fun xmatch x with
| inl xinl (f x)
| inr x'inr (f' x')
end.

Section inverse.
Variables X Y : Type.

Definition inverse_map (f : XY) : YEnsemble X :=
fun y ⇒ (fun xy = f x).

Definition image (f : XY) : Ensemble XEnsemble Y :=
fun Px y x, x Px f x = y.

Definition inverse_image (f : XY) : Ensemble YEnsemble X :=
fun Uy x(f x) Uy.

Definition restrict_domain (f : XY) (P : Ensemble X) : { x | P x }Y
:= fun xf (proj1_sig x).

Definition restrict (f : XY) (P : Ensemble X) (Q : Ensemble Y) (H : x, x P(f x) Q)
: { x | P x }{ y | Q y }
:= fun xexist _ (f (proj1_sig x)) (H (proj1_sig x) (proj2_sig x)).

Definition restrict_range (f : XY) (P : Ensemble Y) : sig (inverse_image f P) → sig P
:= fun xexist _ (f (proj1_sig x)) (proj2_sig x).
End inverse.

Notation "p ⁻¹" := (inverse_image p) (at level 10) : function_scope.

Section inverse_compose.
Variables X Y Z : Type.
Variable f : XY.
Variable g : YZ.

Definition inverse_compose_commutes : f -1 g -1 = (g f) -1.
reflexivity.
Defined.
End inverse_compose.

Add Parametric Morphism T : (@Ensembles.In T)
with signature (@Included T) ==> (@eq T) ==> Basics.impl
as Included_In_mor.
repeat intro.
firstorder.
Qed.

Add Parametric Morphism T : (@Ensembles.In T)
with signature (Basics.flip (@Included T)) ==> (@eq T) ==> (Basics.flip Basics.impl)
as Included_In_mor'.
repeat intro.
firstorder.
Qed.
End morphism.

Arguments compose [X Y Z] f g x / .

Infix "○" := (@compose _ _ _).

Notation "p ⁻¹" := (inverse_image p) (at level 10) : function_scope.

Infix "⊔" := (@sum_function _ _ _ _).