(** * Universal properties of product categories *)
Require Import Category.Core Functor.Core Category.Prod Functor.Composition.Core Functor.Prod.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Functor.Paths.
Require Import Types.Prod HoTT.Tactics Types.Forall Types.Sigma.
Require Import Basics.Tactics.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

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.

    (** ** [fst ∘ (a * b) = a] *)
    Lemma compose_fst_prod : fst o (a * b) = a.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
fst o (a * b) = a
    Proof.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
fst o (a * b) = a
      path_functor; trivial.
    Defined.

    (** ** [snd ∘ (a * b) = b] *)
    Lemma compose_snd_prod : snd o (a * b) = b.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
snd o (a * b) = b
    Proof.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
snd o (a * b) = b
      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.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
c: C
((a * b) _0 c)%object = (F _0 c)%object
      Proof.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
c: C
((a * b) _0 c)%object = (F _0 c)%object
        pose proof (ap (fun F => object_of F c) H1).
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
c: C
X: (fun F : Functor C A => (F _0 c)%object) (fst o F) =
(fun F : Functor C A => (F _0 c)%object) a
((a * b) _0 c)%object = (F _0 c)%object
        pose proof (ap (fun F => object_of F c) H2).
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
c: C
X: (fun F : Functor C A => (F _0 c)%object) (fst o F) =
(fun F : Functor C A => (F _0 c)%object) a
X0: (fun F : Functor C B => (F _0 c)%object)
  (snd o F) =
(fun F : Functor C B => (F _0 c)%object) b
((a * b) _0 c)%object = (F _0 c)%object
        simpl in *.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
c: C
X: fst_type (F _0 c)%object = (a _0 c)%object
X0: snd_type (F _0 c)%object = (b _0 c)%object
pair_type (a _0 c)%object (b _0 c)%object =
(F _0 c)%object
        path_induction.
H: Funext
A, B, C: PreCategory
F: Functor C (A * B)
H1: fst o F = fst o F
H2: snd o F = snd o F
c: C
pair_type (fst_type (F _0 c)%object)
  (snd_type (F _0 c)%object) = (F _0 c)%object
        apply eta_prod.
      Defined.

      Lemma unique_helper2
      : transport
          (fun GO : C -> prod_type A B =>
             forall 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.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
transport
  (fun GO : C -> prod_type A B =>
   forall 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.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
transport
  (fun GO : C -> prod_type A B =>
   forall 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
        repeat (apply path_forall; intro).
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
x, x0: C
x1: morphism C x x0
transport
  (fun GO : C -> prod_type A B =>
   forall 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)) x x0 x1 = F _1 x1
        repeat match goal with
                 | _ => reflexivity
                 | _ => progress simpl
                 | _ => rewrite !transport_forall_constant
               end.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
x, x0: C
x1: morphism C x x0
transport
  (fun x1 : C -> prod_type A B =>
   prod_type
     (morphism A (fst_type (x1 x)) (fst_type (x1 x0)))
     (morphism B (snd_type (x1 x)) (snd_type (x1 x0))))
  (path_forall
     (fun c : C =>
      pair_type (a _0 c)%object (b _0 c)%object) F
     unique_helper) (pair_type (a _1 x1) (b _1 x1)) =
F _1 x1
        transport_path_forall_hammer.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
x, x0: C
x1: morphism C x x0
transport
  (fun y : prod_type A B =>
   prod_type
     (morphism A (fst_type (F _0 x)%object)
        (fst_type y))
     (morphism B (snd_type (F _0 x)%object)
        (snd_type y))) (unique_helper x0)
  (transport
     (fun y : prod_type A B =>
      prod_type
        (morphism A (fst_type y)
           (fst_type
              (pair_type (a _0 x0)%object
                 (b _0 x0)%object)))
        (morphism B (snd_type y)
           (snd_type
              (pair_type (a _0 x0)%object
                 (b _0 x0)%object))))
     (unique_helper x) (pair_type (a _1 x1) (b _1 x1))) =
F _1 x1
        unfold unique_helper.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
x, x0: C
x1: morphism C x x0
transport
  (fun y : prod_type A B =>
   prod_type
     (morphism A (fst_type (F _0 x)%object)
        (fst_type y))
     (morphism B (snd_type (F _0 x)%object)
        (snd_type y)))
  (paths_rect B (snd_type (F _0 x0)%object)
     (fun (o : B) (_ : snd_type (F _0 x0)%object = o)
      =>
      pair_type (a _0 x0)%object o = (F _0 x0)%object)
     (paths_rect A (fst_type (F _0 x0)%object)
        (fun (o : A)
           (_ : fst_type (F _0 x0)%object = o) =>
         pair_type o (snd_type (F _0 x0)%object) =
         (F _0 x0)%object)
        (paths_rect (Functor C B) (snd o F)
           (fun (b : Functor C B) (_ : snd o F = b) =>
            snd o F = b ->
            pair_type (fst_type (F _0 x0)%object)
              (snd_type (F _0 x0)%object) =
            (F _0 x0)%object)
           (fun _ : snd o F = snd o F =>
            paths_rect (Functor C A) (fst o F)
              (fun (a : Functor C A) (_ : fst o F = a)
               =>
               fst o F = a ->
               pair_type (fst_type (F _0 x0)%object)
                 (snd_type (F _0 x0)%object) =
               (F _0 x0)%object)
              (fun _ : fst o F = fst o F =>
               eta_prod (F _0 x0)%object) a H1 H1) b
           H2 H2) (a _0 x0)%object
        (ap (fun F : Functor C A => (F _0 x0)%object)
           H1)) (b _0 x0)%object
     (ap (fun F : Functor C B => (F _0 x0)%object) H2))
  (transport
     (fun y : prod_type A B =>
      prod_type
        (morphism A (fst_type y)
           (fst_type
              (pair_type (a _0 x0)%object
                 (b _0 x0)%object)))
        (morphism B (snd_type y)
           (snd_type
              (pair_type (a _0 x0)%object
                 (b _0 x0)%object))))
     (paths_rect B (snd_type (F _0 x)%object)
        (fun (o : B)
           (_ : snd_type (F _0 x)%object = o) =>
         pair_type (a _0 x)%object o = (F _0 x)%object)
        (paths_rect A (fst_type (F _0 x)%object)
           (fun (o : A)
              (_ : fst_type (F _0 x)%object = o) =>
            pair_type o (snd_type (F _0 x)%object) =
            (F _0 x)%object)
           (paths_rect (Functor C B) (snd o F)
              (fun (b : Functor C B) (_ : snd o F = b)
               =>
               snd o F = b ->
               pair_type (fst_type (F _0 x)%object)
                 (snd_type (F _0 x)%object) =
               (F _0 x)%object)
              (fun _ : snd o F = snd o F =>
               paths_rect (Functor C A) (fst o F)
                 (fun (a : Functor C A)
                    (_ : fst o F = a) =>
                  fst o F = a ->
                  pair_type (fst_type (F _0 x)%object)
                    (snd_type (F _0 x)%object) =
                  (F _0 x)%object)
                 (fun _ : fst o F = fst o F =>
                  eta_prod (F _0 x)%object) a H1 H1) b
              H2 H2) (a _0 x)%object
           (ap
              (fun F : Functor C A => (F _0 x)%object)
              H1)) (b _0 x)%object
        (ap (fun F : Functor C B => (F _0 x)%object)
           H2)) (pair_type (a _1 x1) (b _1 x1))) =
F _1 x1
        repeat match goal with
                 | [ H : _ = _ |- _ ] => case H; simpl; clear H
               end.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
x, x0: C
x1: morphism C x x0
pair_type (fst_type (F _1 x1)) (snd_type (F _1 x1)) =
F _1 x1
        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.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
fst0: A
snd0: B
fst1: A
snd1: B
fst: morphism A (fst_type (pair_type fst0 snd0))
  (fst_type (pair_type fst1 snd1))
snd: morphism B (snd_type (pair_type fst0 snd0))
  (snd_type (pair_type fst1 snd1))
pair_type fst snd = pair_type fst snd
        reflexivity.
      Qed.

      Lemma unique
      : a * b = F.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
a * b = F
      Proof.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
a * b = F
        path_functor.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
{HO
: (fun c : C =>
   pair_type (a _0 c)%object (b _0 c)%object) = F &
transport
  (fun GO : C -> prod_type A B =>
   forall 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))))
  HO
  (fun (s d : C) (m : morphism C s d) =>
   pair_type (a _1 m) (b _1 m)) = morphism_of F}
        exists (path_forall _ _ unique_helper).
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
F: Functor C (A * B)
H1: fst o F = a
H2: snd o F = b
transport
  (fun GO : C -> prod_type A B =>
   forall 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
        exact unique_helper2.
      Defined.
    End unique.

    Local Open Scope core_scope.

    (** ** Universal property characterizing unique product of functors *)
    #[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 }.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
IsHSet0: IsHSet (Functor C A)
IsHSet1: IsHSet (Functor C B)
Contr
  {F : Functor C (A * B) &
  prod_type (fst o F = a) (snd o F = b)}
    Proof.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
IsHSet0: IsHSet (Functor C A)
IsHSet1: IsHSet (Functor C B)
Contr
  {F : Functor C (A * B) &
  prod_type (fst o F = a) (snd o F = b)}
      refine (Build_Contr _ (a * b; (compose_fst_prod, compose_snd_prod)) _).
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
IsHSet0: IsHSet (Functor C A)
IsHSet1: IsHSet (Functor C B)
forall
y : {F : Functor C (A * B) &
    prod_type (fst o F = a) (snd o F = b)},
(a * b; pair_type compose_fst_prod compose_snd_prod) =
y
      intro y.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
IsHSet0: IsHSet (Functor C A)
IsHSet1: IsHSet (Functor C B)
y: {F : Functor C (A * B) &
prod_type (fst o F = a) (snd o F = b)}
(a * b; pair_type compose_fst_prod compose_snd_prod) =
y
      apply path_sigma_uncurried.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
IsHSet0: IsHSet (Functor C A)
IsHSet1: IsHSet (Functor C B)
y: {F : Functor C (A * B) &
prod_type (fst o F = a) (snd o F = b)}
{p
: (a * b; pair_type compose_fst_prod compose_snd_prod).1 =
  y.1 &
transport
  (fun F : Functor C (A * B) =>
   prod_type (fst o F = a) (snd o F = b)) p
  (a * b; pair_type compose_fst_prod compose_snd_prod).2 =
y.2}
      simpl.
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
IsHSet0: IsHSet (Functor C A)
IsHSet1: IsHSet (Functor C B)
y: {F : Functor C (A * B) &
prod_type (fst o F = a) (snd o F = b)}
{p : a * b = y.1 &
transport
  (fun F : Functor C (A * B) =>
   prod_type (fst o F = a) (snd o F = b)) p
  (pair_type compose_fst_prod compose_snd_prod) = y.2}
      exists (unique (fst_type y.2) (snd_type y.2)).
H: Funext
A, B, C: PreCategory
a: Functor C A
b: Functor C B
IsHSet0: IsHSet (Functor C A)
IsHSet1: IsHSet (Functor C B)
y: {F : Functor C (A * B) &
prod_type (fst o F = a) (snd o F = b)}
transport
  (fun F : Functor C (A * B) =>
   prod_type (fst o F = a) (snd o F = b))
  (unique (fst_type y.2) (snd_type y.2))
  (pair_type compose_fst_prod compose_snd_prod) = y.2
      exact (center _).
    Qed.
  End universal.

  (** ** Classification of path space of functors to a product precategory *)
  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.
H: Funext
A, B, C: PreCategory
F, G: Functor C (A * B)
H1: fst o F = fst o G
H2: snd o F = snd o G
F = G
  Proof.
H: Funext
A, B, C: PreCategory
F, G: Functor C (A * B)
H1: fst o F = fst o G
H2: snd o F = snd o G
F = G
    etransitivity; [ symmetry | ];
    apply unique; try eassumption; reflexivity.
  Defined.
End universal.