Definition fcompose{X Y Z : Type}(f : Y → Z)(g : X → Y)(x : X) : Z :=
  f(g(x)).

Hint Unfold fcompose.

Notation " f ∘ g " := (fcompose f g)
  (at level 40, left associativity) : feq_scope.

Definition function_equal {X Y : Type}(f g : X → Y) :=
  ∀ x : X, f x = g x.

Notation " g ≡ f " := (function_equal g f)
  (at level 70) : feq_scope.

Open Scope feq_scope.

Lemma feq_reflexive : ∀ (X Y : Type)(f : X → Y), f ≡ f.

Lemma feq_transitive :
  ∀ (X Y : Type)(f g h : X → Y), f ≡ g → g ≡ h → f ≡ h.

Lemma feq_symmetric : ∀ (X Y : Type)(f g : X → Y), f ≡ g → g ≡ f.

Lemma feq_eq : ∀(X Y : Type)(f g : X → Y), f = g → f ≡ g.


Lemma feq_rw_r : ∀ (X Y : Type)(f g h : X → Y),
  g ≡ h → f ≡ h → f ≡ g.

Definition id {X : Type} : X → X := fun x ⇒ x.

Lemma feq_id_left : ∀ (X Y : Type)(f : X → Y), (id ∘ f) ≡ f.

Lemma feq_id_right : ∀ (X Y : Type)(f : X → Y), (f ∘ id) ≡ f.

Lemma feq_compose_associative :
  ∀ (U V X Y : Type)(f : X → Y)(g : V → X)(h : U → V),
    (f ∘ (g ∘ h)) ≡ (f ∘ g ∘ h).

Lemma feq_compose_associative_reverse :
  ∀ (U V X Y : Type)(f : X → Y)(g : V → X)(h : U → V),
    (f ∘ g ∘ h) ≡ (f ∘ (g ∘ h)).

Lemma feq_compose_both :
  ∀ (X Y Z : Type)(f1 f2: Y → Z)(g1 g2 : X → Y),
    f1 ≡ f2 → g1 ≡ g2 → (f1 ∘ g1) ≡ (f2 ∘ g2).

Lemma feq_compose_left_both :
  ∀ (X Y Z : Type)(f : Y → Z)(g1 g2 : X → Y),
    g1 ≡ g2 → (f ∘ g1) ≡ (f ∘ g2).

Lemma feq_compose_right_both :
  ∀ (X Y Z : Type)(f1 f2 : Y → Z)(g : X → Y),
    f1 ≡ f2 → (f1 ∘ g) ≡ (f2 ∘ g).

Lemma feq_left_compose_left :
  ∀(X Y Z : Type)(f1 f2 : Y → Z)(g : X → Y)(h : X → Z),
    f1 ≡ f2 → f2 ∘ g ≡ h → f1 ∘ g ≡ h.

Lemma feq_left_compose_right :
  ∀(X Y Z : Type)(f1 f2 : Y → Z)(g : X → Z)(h : X → Y),
    f1 ≡ f2 → g ≡ f2 ∘ h → g ≡ f1 ∘ h.

Lemma feq_right_compose_left :
  ∀(X Y Z : Type)(f : Y → Z)(g1 g2 : X → Y)(h : X → Z),
    g1 ≡ g2 → f ∘ g2 ≡ h → f ∘ g1 ≡ h.

Lemma feq_right_compose_right :
  ∀(X Y Z : Type)(f1 f2 : X → Y)(g : X → Z)(h : Y → Z),
    f1 ≡ f2 → g ≡ h ∘ f2 → g ≡ h ∘ f1.

Definition final_map(X : Type) : X → unit := fun _ ⇒ tt.

Lemma final_map_prop : ∀(X : Type)(f : X → unit),
  f ≡ final_map X.

Definition pair{U X Y : Type}(f : U → X)(g : U → Y) : U → X × Y :=
  fun(u : U) ⇒ (f u, g u).

Lemma pair_proj_left :
  ∀(U X Y : Type)(f : U → X)(g : U → Y),
    (@fst X Y) ∘ (pair f g) = f.

Lemma pair_proj_right :
  ∀(U X Y : Type)(f : U → X)(g : U → Y),
    (@snd X Y) ∘ (pair f g) = g.

Lemma pair_compose_right :
  ∀(U V X Y : Type)(h : U → V)(f : V → X)(g : V → Y),
    (pair f g) ∘ h = pair (f ∘ h) (g ∘ h).

Lemma feq_pair_proj : ∀(U X Y : Type)(f : U → X × Y),
  f ≡ pair ((fst (B := Y)) ∘ f) ((snd (B := Y)) ∘ f).

Lemma feq_pair_both :
  ∀(X Y Z : Type)(f1 f2 : X → Y)(g1 g2 : X → Z),
    f1 ≡ f2 → g1 ≡ g2 → pair f1 g1 ≡ pair f2 g2.

Lemma feq_pair_left :
  ∀(X Y Z : Type)(f1 f2 : X → Y)(g : X → Z),
    f1 ≡ f2 → pair f1 g ≡ pair f2 g.

Lemma feq_pair_right :
  ∀(X Y Z : Type)(f : X → Y)(g1 g2 : X → Z),
    g1 ≡ g2 → pair f g1 ≡ pair f g2.

Definition ftimes{U V X Y : Type}(f : U → X)(g : V → Y) : U × V → X × Y :=
  fun(uv : U × V) ⇒ (f (fst uv), g (snd uv)).

Lemma ftimes_def :
  ∀(U V X Y : Type)(f : U → X)(g : V → Y),
    pair (f ∘ (fst (B := V))) (g ∘ (snd (B := V))) = ftimes f g.

Lemma feq_ftimes_id : ∀(X Y : Type),
  ftimes (@id X) (@id Y) ≡ @id (X × Y).

Lemma feq_ftimes_compose :
  ∀(XL XR YL YR ZL ZR : Type)
        (fl : XL → YL)(fr : XR → YR)(gl : YL → ZL)(gr : YR → ZR),
    (ftimes gl gr) ∘ (ftimes fl fr) ≡ ftimes (gl ∘ fl) (gr ∘ fr).

Lemma feq_ftimes_compose_pair :
  ∀(X YL YR ZL ZR : Type)
        (fl : X → YL)(fr : X → YR)(gl : YL → ZL)(gr : YR → ZR),
    (ftimes gl gr) ∘ (pair fl fr) ≡ pair (gl ∘ fl) (gr ∘ fr).

Lemma feq_ftimes_both :
  ∀(U V X Y : Type)(f1 f2 : U → X)(g1 g2 : V → Y),
    f1 ≡ f2 → g1 ≡ g2 → ftimes f1 g1 ≡ ftimes f2 g2.

Lemma feq_ftimes_left :
  ∀(U V X Y : Type)(f1 f2 : U → X)(g : V → Y),
    f1 ≡ f2 → ftimes f1 g ≡ ftimes f2 g.

Lemma feq_ftimes_right :
  ∀(U V X Y : Type)(f : U → X)(g1 g2 : V → Y),
    g1 ≡ g2 → ftimes f g1 ≡ ftimes f g2.