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 _ _ _ _).