{-# OPTIONS --without-K --safe #-}
open import Categories.Category

module Categories.Object.Product.Core {o  e} (𝒞 : Category o  e) where

open import Level
open import Function using (flip; _$_)

open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞

open Category 𝒞
open HomReasoning

private
  variable
    A B C D X Y Z : Obj
    h i j : A  B

-- Borrowed from Dan Doel's definition of products
record Product (A B : Obj) : Set (o    e) where

  infix 10 ⟨_,_⟩

  field
    A×B   : Obj
    π₁    : A×B  A
    π₂    : A×B  B
    ⟨_,_⟩ : C  A  C  B  C  A×B

    project₁ : π₁   h , i   h
    project₂ : π₂   h , i   i
    unique   : π₁  h  i  π₂  h  j   i , j   h

  open Equiv

  g-η :  π₁  h , π₂  h   h
  g-η = unique refl refl

  η :  π₁ , π₂   id
  η = unique identityʳ identityʳ

  ⟨⟩-cong₂ :  {f f′ : C  A} {g g′ : C  B}  f  f′  g  g′   f , g    f′ , g′ 
  ⟨⟩-cong₂ f≡f′ g≡g′ = unique (project₁   f≡f′) (project₂   g≡g′)

  ∘-distribʳ-⟨⟩ :  {f : C  A} {g : C  B} {q : D  C}   f , g   q   f  q , g  q 
  ∘-distribʳ-⟨⟩ =  $ unique (pullˡ project₁) (pullˡ project₂)

  unique′ : π₁  h  π₁  i  π₂  h  π₂  i  h  i
  unique′ eq₁ eq₂ = trans (sym (unique eq₁ eq₂)) g-η

record IsProduct {A B P} (π₁ : P  A) (π₂ : P  B) : Set (o    e) where
  infix 10 ⟨_,_⟩

  field
    ⟨_,_⟩ : C  A  C  B  C  P

    project₁ : π₁   h , i   h
    project₂ : π₂   h , i   i
    unique   : π₁  h  i  π₂  h  j   i , j   h

Product⇒IsProduct : (p : Product A B)  IsProduct (Product.π₁ p) (Product.π₂ p)
Product⇒IsProduct p = record
  { ⟨_,_⟩    = ⟨_,_⟩
  ; project₁ = project₁
  ; project₂ = project₂
  ; unique   = unique
  }
  where open Product p

IsProduct⇒Product :  {P} {π₁ : P  A} {π₂ : P  B}  IsProduct π₁ π₂  Product A B
IsProduct⇒Product p = record
  { ⟨_,_⟩    = ⟨_,_⟩
  ; project₁ = project₁
  ; project₂ = project₂
  ; unique   = unique
  }
  where open IsProduct p

module _ {A B : Obj} where
  open Product {A} {B} renaming (⟨_,_⟩ to _⟨_,_⟩)

  repack : (p₁ p₂ : Product A B)  A×B p₁  A×B p₂
  repack p₁ p₂ = p₂  π₁ p₁ , π₂ p₁ 

  repack∘ : (p₁ p₂ p₃ : Product A B)  repack p₂ p₃  repack p₁ p₂  repack p₁ p₃
  repack∘ p₁ p₂ p₃ =  $ unique p₃
    (glueTrianglesʳ (project₁ p₃) (project₁ p₂))
    (glueTrianglesʳ (project₂ p₃) (project₂ p₂))

  repack≡id : (p : Product A B)  repack p p  id
  repack≡id = η

  repack-cancel : (p₁ p₂ : Product A B)  repack p₁ p₂  repack p₂ p₁  id
  repack-cancel p₁ p₂ = repack∘ p₂ p₁ p₂  repack≡id p₂

up-to-iso :  (p₁ p₂ : Product A B)  Product.A×B p₁  Product.A×B p₂
up-to-iso p₁ p₂ = record
  { from = repack p₁ p₂
  ; to   = repack p₂ p₁
  ; iso  = record
    { isoˡ = repack-cancel p₂ p₁
    ; isoʳ = repack-cancel p₁ p₂
    }
  }

transport-by-iso :  (p : Product A B)   {X}  Product.A×B p  X  Product A B
transport-by-iso p {X} p≅X = record
  { A×B = X
  ; π₁ = π₁  to
  ; π₂ = π₂  to
  ; ⟨_,_⟩ = λ h₁ h₂  from   h₁ , h₂ 
  ; project₁ = cancelInner isoˡ  project₁
  ; project₂ = cancelInner isoˡ  project₂
  ; unique = λ {_ i l r} pf₁ pf₂  begin
    from   l , r                          ≈˘⟨ refl⟩∘⟨ ⟨⟩-cong₂ pf₁ pf₂ 
    from   (π₁  to)  i , (π₂  to)  i  ≈⟨ refl⟩∘⟨ unique sym-assoc sym-assoc 
    from  to  i                            ≈⟨ cancelˡ isoʳ 
    i                                        
  }
  where open Product p
        open _≅_ p≅X

Reversible : (p : Product A B)  Product B A
Reversible p = record
  { A×B       = A×B
  ; π₁        = π₂
  ; π₂        = π₁
  ; ⟨_,_⟩     = flip ⟨_,_⟩
  ; project₁  = project₂
  ; project₂  = project₁
  ; unique = flip unique
  }
  where open Product p

Commutative : (p₁ : Product A B) (p₂ : Product B A)  Product.A×B p₁  Product.A×B p₂
Commutative p₁ p₂ = up-to-iso p₁ (Reversible p₂)

Associable :  (p₁ : Product X Y) (p₂ : Product Y Z) (p₃ : Product X (Product.A×B p₂))  Product (Product.A×B p₁) Z
Associable p₁ p₂ p₃ = record
  { A×B       = A×B p₃
  ; π₁        = p₁  π₁ p₃ , π₁ p₂  π₂ p₃ 
  ; π₂        = π₂ p₂  π₂ p₃
  ; ⟨_,_⟩     = λ f g  p₃  π₁ p₁  f , p₂  π₂ p₁  f , g  
  ; project₁  = λ {_ f g}  begin
    p₁  π₁ p₃ , π₁ p₂  π₂ p₃   p₃  π₁ p₁  f , p₂  π₂ p₁  f , g   ≈⟨ ∘-distribʳ-⟨⟩ p₁ 
    p₁  π₁ p₃  p₃  π₁ p₁  f , p₂  π₂ p₁  f , g  
       , (π₁ p₂  π₂ p₃)  p₃  π₁ p₁  f , p₂  π₂ p₁  f , g          ≈⟨ ⟨⟩-cong₂ p₁ (project₁ p₃) (glueTrianglesˡ (project₁ p₂) (project₂ p₃)) 
    p₁  π₁ p₁  f , π₂ p₁  f                                            ≈⟨ g-η p₁ 
    f                                                                      
  ; project₂  = λ {_ f g}  glueTrianglesˡ (project₂ p₂) (project₂ p₃)
  ; unique = λ {_ i f g} pf₁ pf₂  begin
    p₃  π₁ p₁  f , p₂  π₂ p₁  f , g               ≈⟨ ⟨⟩-cong₂ p₃ (∘-resp-≈ʳ (sym pf₁))
                                                          (⟨⟩-cong₂ p₂ (∘-resp-≈ʳ (sym pf₁)) (sym pf₂)) 
    p₃  π₁ p₁  p₁  π₁ p₃ , π₁ p₂  π₂ p₃   i
       , p₂  π₂ p₁  p₁  π₁ p₃ , π₁ p₂  π₂ p₃   i
            , (π₂ p₂  π₂ p₃)  i                     ≈⟨ ⟨⟩-cong₂ p₃ (pullˡ (project₁ p₁))
                                                          (⟨⟩-cong₂ p₂ (trans (pullˡ (project₂ p₁)) assoc)
                                                                       assoc) 
    p₃  π₁ p₃  i
       , p₂  π₁ p₂  π₂ p₃  i , π₂ p₂  π₂ p₃  i   ≈⟨ ⟨⟩-cong₂ p₃ refl (g-η p₂) 
    p₃  π₁ p₃  i , π₂ p₃  i                         ≈⟨ g-η p₃ 
    i                                                   
  }
  where
  open Product renaming (⟨_,_⟩ to _⟨_,_⟩)
  open Equiv

Associative :  (p₁ : Product X Y) (p₂ : Product Y Z)
                (p₃ : Product X (Product.A×B p₂)) (p₄ : Product (Product.A×B p₁) Z) 
                (Product.A×B p₃)  (Product.A×B p₄)
Associative p₁ p₂ p₃ p₄ = up-to-iso (Associable p₁ p₂ p₃) p₄

Mobile :  {A₁ B₁ A₂ B₂} (p : Product A₁ B₁)  A₁  A₂  B₁  B₂  Product A₂ B₂
Mobile p A₁≅A₂ B₁≅B₂ = record
  { A×B              = A×B
  ; π₁               = from A₁≅A₂  π₁
  ; π₂               = from B₁≅B₂  π₂
  ; ⟨_,_⟩            = λ h k   to A₁≅A₂  h , to B₁≅B₂  k 
  ; project₁         = begin
    (from A₁≅A₂  π₁)   to A₁≅A₂  _ , to B₁≅B₂  _  ≈⟨ pullʳ project₁ 
    from A₁≅A₂  (to A₁≅A₂  _)                         ≈⟨ cancelˡ (isoʳ A₁≅A₂) 
    _                                                   
  ; project₂         = begin
    (from B₁≅B₂  π₂)   to A₁≅A₂  _ , to B₁≅B₂  _  ≈⟨ pullʳ project₂ 
    from B₁≅B₂  (to B₁≅B₂  _)                         ≈⟨ cancelˡ (isoʳ B₁≅B₂) 
    _                                                   
  ; unique        = λ pfˡ pfʳ  unique (switch-fromtoˡ A₁≅A₂ (sym-assoc  pfˡ))
                                       (switch-fromtoˡ B₁≅B₂ (sym-assoc  pfʳ))
  }
  where open Product p
        open _≅_