@include logic.pg

section Category
    variable
        (Obj  : *)
        (Hom  : Obj -> Obj -> *)
        (id   : forall (A     : Obj), Hom A A)
        (comp : forall (A B C : Obj), Hom A B -> Hom B C -> Hom A C);

    hypothesis
        (id_l  : forall (A B     : Obj) (f : Hom A B), eq (Hom A B) (comp A A B (id A) f) f)
        (id_r  : forall (A B     : Obj) (f : Hom B A), eq (Hom A B) (comp B A A f (id A)) f)
        (assoc : forall (A B C D : Obj) (f : Hom A B) (g : Hom B C) (h : Hom C D),
            eq (Hom A D)
                (comp A B D f (comp B C D g h))
                (comp A C D (comp A B C f g) h));

    def initial  (A : Obj) := forall (B : Obj), exists_uniq_t (Hom A B);
    def terminal (A : Obj) := forall (B : Obj), exists_uniq_t (Hom B A);

    def product (A B C : Obj) (piA : Hom C A) (piB : Hom C B) :=
        forall (D : Obj) (f : Hom D A) (g : Hom D B),
            exists_uniq (Hom D C) (fun (fxg : Hom D C) =>
                and (eq (Hom D A) (comp D C A fxg piA) f)
                    (eq (Hom D B) (comp D C B fxg piB) g));

    section Inverses
        variable
            (A B : Obj)
            (f : Hom A B)
            (g : Hom B A);

        def inv_l := eq (Hom A A) (comp A B A f g) (id A);
        def inv_r := eq (Hom B B) (comp B A B g f) (id B);

        def inv := and inv_l inv_r;
    end Inverses

    def isomorphic (A B : Obj) :=
        exists (Hom A B) (fun (f : Hom A B) =>
            exists (Hom B A) (inv A B f));

    def initial_uniq (A B : Obj) (hA : initial A) (hB : initial B) : isomorphic A B :=
        exists_uniq_t_elim (Hom A B) (isomorphic A B) (hA B) (fun (f : Hom A B) (f_uniq : forall (y : Hom A B), eq (Hom A B) f y) =>
        exists_uniq_t_elim (Hom B A) (isomorphic A B) (hB A) (fun (g : Hom B A) (g_uniq : forall (y : Hom B A), eq (Hom B A) g y) =>
        exists_uniq_t_elim (Hom A A) (isomorphic A B) (hA A) (fun (a : Hom A A) (a_uniq : forall (y : Hom A A), eq (Hom A A) a y) =>
        exists_uniq_t_elim (Hom B B) (isomorphic A B) (hB B) (fun (b : Hom B B) (b_uniq : forall (y : Hom B B), eq (Hom B B) b y) =>
            exists_intro (Hom A B) (fun (f : Hom A B) => exists (Hom B A) (inv A B f)) f
                (exists_intro (Hom B A) (inv A B f) g
                    (and_intro (inv_l A B f g) (inv_r A B f g)
                        (eq_trans (Hom A A) (comp A B A f g) a (id A)
                            (eq_sym (Hom A A) a (comp A B A f g) (a_uniq (comp A B A f g)))
                            (a_uniq (id A)))
                        (eq_trans (Hom B B) (comp B A B g f) b (id B)
                            (eq_sym (Hom B B) b (comp B A B g f) (b_uniq (comp B A B g f)))
                            (b_uniq (id B)))))))));

    def terminal_uniq (A B : Obj) (hA : terminal A) (hB : terminal B) : isomorphic A B :=
        exists_uniq_t_elim (Hom A B) (isomorphic A B) (hB A) (fun (f : Hom A B) (f_uniq : forall (y : Hom A B), eq (Hom A B) f y) =>
        exists_uniq_t_elim (Hom B A) (isomorphic A B) (hA B) (fun (g : Hom B A) (g_uniq : forall (y : Hom B A), eq (Hom B A) g y) =>
        exists_uniq_t_elim (Hom A A) (isomorphic A B) (hA A) (fun (a : Hom A A) (a_uniq : forall (y : Hom A A), eq (Hom A A) a y) =>
        exists_uniq_t_elim (Hom B B) (isomorphic A B) (hB B) (fun (b : Hom B B) (b_uniq : forall (y : Hom B B), eq (Hom B B) b y) =>
            exists_intro (Hom A B) (fun (f : Hom A B) => exists (Hom B A) (inv A B f)) f
                (exists_intro (Hom B A) (inv A B f) g
                    (and_intro (inv_l A B f g) (inv_r A B f g)
                        (eq_trans (Hom A A) (comp A B A f g) a (id A)
                            (eq_sym (Hom A A) a (comp A B A f g) (a_uniq (comp A B A f g)))
                            (a_uniq (id A)))
                        (eq_trans (Hom B B) (comp B A B g f) b (id B)
                            (eq_sym (Hom B B) b (comp B A B g f) (b_uniq (comp B A B g f)))
                            (b_uniq (id B)))))))));
end Category