Require Import Category.Core Functor.Core Category.Prod Functor.Composition.Core Functor.Prod.Core.
Require Import Functor.Paths.
Require Import Types.Prod HoTT.Tactics Types.Forall Types.Sigma.
Require Import Basics.Tactics.

Set Implicit Arguments.
Generalizable All Variables.

Local Notation fst_type := Basics.Overture.fst.
Local Notation snd_type := Basics.Overture.snd.
Local Notation pair_type := Basics.Overture.pair.
Local Notation prod_type := Basics.Overture.prod.

Local Open Scope morphism_scope.
Local Open Scope functor_scope.

Section universal.
  Context `{Funext}.

  Variables A B C : PreCategory.

  Local Open Scope functor_scope.

  Section universal.
    Variable a : Functor C A.
    Variable b : Functor C B.

    Lemma compose_fst_prod : fst o (a × b) = a.
    Proof.
      path_functor; trivial.
    Defined.

    Lemma compose_snd_prod : snd o (a × b) = b.
    Proof.
      path_functor; trivial.
    Defined.

    Section unique.
      Variable F : Functor C (A × B).
      Hypothesis H1 : fst o F = a.
      Hypothesis H2 : snd o F = b.

      Lemma unique_helper c
      : (a × b) c = F c.
      Proof.
        pose proof (ap (fun F ⇒ object_of F c) H1).
        pose proof (ap (fun F ⇒ object_of F c) H2).
        simpl in ×.
        path_induction.
        apply eta_prod.
      Defined.

      Lemma unique_helper2
      : transport
          (fun GO : C → prod_type A B ⇒
             ∀ s d : C,
               morphism C s d →
               prod_type (morphism A (fst_type (GO s)) (fst_type (GO d)))
                         (morphism B (snd_type (GO s)) (snd_type (GO d))))
          (path_forall (a × b) F unique_helper)
          (fun (s d : C) (m : morphism C s d) ⇒ pair_type (a _1 m) (b _1 m)) =
        morphism_of F.
      Proof.
        repeat (apply path_forall; intro).
        repeat match goal with
                 | _ ⇒ reflexivity
                 | _ ⇒ progress simpl
                 | _ ⇒ rewrite !transport_forall_constant
               end.
        transport_path_forall_hammer.
        unfold unique_helper.
        repeat match goal with
                 | [ H : _ = _ |- _ ] ⇒ case H; simpl; clear H
               end.
        repeat match goal with
                 | [ |- context[@morphism_of ?C ?D ?F ?s ?d ?m] ]
                   ⇒ destruct (@morphism_of C D F s d m); clear m
                 | [ |- context[@object_of ?C ?D ?F ?x] ]
                   ⇒ destruct (@object_of C D F x); clear x
               end.
        reflexivity.
      Qed.

      Lemma unique
      : a × b = F.
      Proof.
        path_functor.
        ∃ (path_forall _ _ unique_helper).
        exact unique_helper2.
      Defined.
    End unique.

    Local Open Scope core_scope.

    #[export] Instance contr_prod_type
           `{IsHSet (Functor C A), IsHSet (Functor C B)}
    : Contr { F : Functor C (A × B)
            | fst o F = a
              ∧ snd o F = b }.
    Proof.
      refine (Build_Contr _ (a × b; (compose_fst_prod, compose_snd_prod)) _).
      intro y.
      apply path_sigma_uncurried.
      simpl.
      ∃ (unique (fst_type y.2) (snd_type y.2)).
      exact (center _).
    Qed.
  End universal.

  Definition path_prod (F G : Functor C (A × B))
             (H1 : fst o F = fst o G)
             (H2 : snd o F = snd o G)
  : F = G.
  Proof.
    etransitivity; [ symmetry | ];
    apply unique; try eassumption; reflexivity.
  Defined.
End universal.