Require Import Theory.Category.
Require Import Theory.Product.

Program Definition Hom (A B : Type) : Setoid ≔ Setoid.make ⦃ Carrier ≔ A → B

; Equiv

≔ λ f g ∙ ∀ x, f x = g x ⦄.

Show proof.

Local Infix "⇒" ≔ Hom.

Definition id {A} : A ⇒ A ≔ λ x ∙ x.

Program Definition compose {A B C} : [ B ⇒ C ⟶ A ⇒ B ⟶ A ⇒ C ] ≔
  Π₂.make (λ g f x ∙ g (f x)).

Show proof.

Local Infix "∘" ≔ compose.

Lemma left_id A B (f : A ⇒ B) : id ∘ f ≈ f.
Show proof.

Lemma right_id A B (f : A ⇒ B) : f ∘ id ≈ f.
Show proof.

Lemma compose_assoc A B C D (f : A ⇒ B) (g : B ⇒ C) (h : C ⇒ D) : h ∘ g ∘ f ≈ h ∘ (g ∘ f).
Show proof.

Canonical Structure 𝑻𝒚𝒑𝒆 : Category ≔
  mkCategory left_id right_id compose_assoc.

Program Instance 𝑻𝒚𝒑𝒆_BinaryProduct : BinaryProduct 𝑻𝒚𝒑𝒆 ≔

BinaryProduct.make	⦃ Category	≔ 𝑻𝒚𝒑𝒆
	; _×_	≔ _⟨×⟩_
	; ⟨_,_⟩	≔ λ C f g (c : C) ∙ (f c , g c)
	; π₁	≔ fst
	; π₂	≔ snd ⦄.

Show proof.

Show proof.