HoTT.Categories.Functor.Prod.Universal.v.alectryon.json

(** * Universal properties of product categories *)
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.

    (** ** [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 F0 : Functor C A => (F0 _0 c)%object) (fst o F) =
(fun F0 : Functor C A => (F0 _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 F0 : Functor C A => (F0 _0 c)%object) (fst o F) =
(fun F0 : Functor C A => (F0 _0 c)%object) a
X0: (fun F0 : Functor C B => (F0 _0 c)%object) (snd o F) =
(fun F0 : Functor C B => (F0 _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 x2 : C -> prod_type A B =>
   prod_type (morphism A (fst_type (x2 x)) (fst_type (x2 x0)))
     (morphism B (snd_type (x2 x)) (snd_type (x2 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 (b0 : Functor C B) (_ : snd o F = b0) =>
            snd o F = b0 ->
            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 (a0 : Functor C A) (_ : fst o F = a0) =>
               fst o F = a0 ->
               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 F0 : Functor C A => (F0 _0 x0)%object) H1))
     (b _0 x0)%object (ap (fun F0 : Functor C B => (F0 _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 (b0 : Functor C B) (_ : snd o F = b0) =>
               snd o F = b0 ->
               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 (a0 : Functor C A) (_ : fst o F = a0) =>
                  fst o F = a0 ->
                  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 F0 : Functor C A => (F0 _0 x)%object) H1))
        (b _0 x)%object (ap (fun F0 : Functor C B => (F0 _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_type (pair_type fst snd)) (snd_type (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.