{-# OPTIONS --without-K --safe #-}

module Extensive.Core where

-- https://ncatlab.org/nlab/show/extensive+category

open import Level

open import Categories.Category.Core
open import Distributive.Core
open import Categories.Diagram.Pullback
open import Categories.Category.Cocartesian
open import Categories.Category.Cartesian
open import Categories.Category.BinaryProducts
open import Categories.Object.Coproduct
open import Categories.Morphism
open import Function using (_$_)
open import Coproduct


private
    variable
        o ℓ e : Level

record Extensive (𝒞 : Category o ℓ e) : Set (suc (o ⊔ ℓ ⊔ e)) where
  open Category 𝒞
  open Pullback

  field
    cocartesian : Cocartesian 𝒞
  
  module CC = Cocartesian cocartesian
  open CC using (_+_; i₁; i₂; ¡)

  field
    -- top-row is coproduct ⇒ pullback
    cp⇒pullback₁ : {A B C D : Obj} (cp : Coproduct 𝒞 A B) (p₂ : A ⇒ C) (f : Coproduct.A+B cp ⇒ C + D) → IsPullback 𝒞 (Coproduct.i₁ cp) p₂ f i₁
    cp⇒pullback₂ : {A B C D : Obj} (cp : Coproduct 𝒞 A B) (p₂ : B ⇒ D) (f : Coproduct.A+B cp ⇒ C + D) → IsPullback 𝒞 (Coproduct.i₂ cp) p₂ f i₂

    -- pullbacks ⇒ top-row is coproduct
    pullbacks⇒cp : {A B C : Obj} {f : A ⇒ B + C} (P₁ : Pullback 𝒞 f i₁) (P₂ : Pullback 𝒞 f i₂) → IsCoproduct 𝒞 (Pullback.p₁ P₁) (Pullback.p₁ P₂)

Extensive⇒Distributive : ∀ {𝒞 : Category o ℓ e} → (cartesian : Cartesian 𝒞) → (E : Extensive 𝒞) → Distributive 𝒞 cartesian (Extensive.cocartesian E)
Extensive⇒Distributive {𝒞 = 𝒞} cartesian E = record 
  { distributeˡ = λ {A} {B} {C} → ≅-sym 𝒞 $ iso {A} {B} {C} 
  }
  where
    open Category 𝒞
    open Extensive E
    open Cocartesian cocartesian
    open Cartesian cartesian
    open BinaryProducts products
    open HomReasoning
    open Equiv
    open ≅ using () renaming (sym to ≅-sym)
    pb₁ : ∀ {A B C} → Pullback 𝒞 (π₂ {A = A} {B = B + C}) i₁
    pb₁ {A} {B} {C} = record { P = A × B ; p₁ = id ⁂ i₁ ; p₂ = π₂ ; isPullback = record
      { commute = π₂∘⁂
      ; universal = λ {X} {h₁} {h₂} H → ⟨ π₁ ∘ h₁ , h₂ ⟩
      ; unique = λ {X} {h₁} {h₂} {i} {eq} H1 H2 → sym (unique (sym $
          begin 
            π₁ ∘ h₁ ≈⟨ ∘-resp-≈ʳ (sym H1) ⟩ 
            (π₁ ∘ (id ⁂ i₁) ∘ i) ≈⟨ sym-assoc ⟩
            ((π₁ ∘ (id ⁂ i₁)) ∘ i) ≈⟨ ∘-resp-≈ˡ π₁∘⁂ ⟩
            ((id ∘ π₁) ∘ i) ≈⟨ ∘-resp-≈ˡ identityˡ ⟩
            π₁ ∘ i ∎) H2)
      ; p₁∘universal≈h₁ = λ {X} {h₁} {h₂} {eq} → 
          begin 
            (id ⁂ i₁) ∘ ⟨ π₁ ∘ h₁ , h₂ ⟩ ≈⟨ ⁂∘⟨⟩ ⟩
            ⟨ id ∘ π₁ ∘ h₁ , i₁ ∘ h₂ ⟩ ≈⟨ ⟨⟩-congʳ identityˡ ⟩
            ⟨ π₁ ∘ h₁ , i₁ ∘ h₂ ⟩ ≈⟨ ⟨⟩-congˡ (sym eq) ⟩
            ⟨ π₁ ∘ h₁ , π₂ ∘ h₁ ⟩ ≈⟨ g-η ⟩
            h₁ ∎
      ; p₂∘universal≈h₂ = λ {X} {h₁} {h₂} {eq} → project₂
      } }
    pb₂ : ∀ {A B C} → Pullback 𝒞 (π₂ {A = A} {B = B + C}) i₂
    pb₂ {A} {B} {C} = record { P = A × C ; p₁ = id ⁂ i₂ ; p₂ = π₂ ; isPullback = record
      { commute = π₂∘⁂
      ; universal = λ {X} {h₁} {h₂} H → ⟨ π₁ ∘ h₁ , h₂ ⟩
      ; unique = λ {X} {h₁} {h₂} {i} {eq} H1 H2 → sym (unique (sym $
          begin 
            π₁ ∘ h₁ ≈⟨ ∘-resp-≈ʳ (sym H1) ⟩ 
            (π₁ ∘ (id ⁂ i₂) ∘ i) ≈⟨ sym-assoc ⟩
            ((π₁ ∘ (id ⁂ i₂)) ∘ i) ≈⟨ ∘-resp-≈ˡ π₁∘⁂ ⟩
            ((id ∘ π₁) ∘ i) ≈⟨ ∘-resp-≈ˡ identityˡ ⟩
            π₁ ∘ i ∎) H2)
      ; p₁∘universal≈h₁ = λ {X} {h₁} {h₂} {eq} → 
          begin 
            (id ⁂ i₂) ∘ ⟨ π₁ ∘ h₁ , h₂ ⟩ ≈⟨ ⁂∘⟨⟩ ⟩
            ⟨ id ∘ π₁ ∘ h₁ , i₂ ∘ h₂ ⟩ ≈⟨ ⟨⟩-congʳ identityˡ ⟩
            ⟨ π₁ ∘ h₁ , i₂ ∘ h₂ ⟩ ≈⟨ ⟨⟩-congˡ (sym eq) ⟩
            ⟨ π₁ ∘ h₁ , π₂ ∘ h₁ ⟩ ≈⟨ g-η ⟩
            h₁ ∎
      ; p₂∘universal≈h₂ = λ {X} {h₁} {h₂} {eq} → project₂
      } }
    cp₁ : ∀ {A B C : Obj} → IsCoproduct 𝒞 {A+B = A × (B + C)} (id ⁂ i₁) (id ⁂ i₂)
    cp₁ {A} {B} {C} = pullbacks⇒cp pb₁ pb₂
    cp₂ = λ {A B C : Obj} → coproduct {A × B} {A × C}
    iso = λ {A B C : Obj} → Coproduct.up-to-iso 𝒞 (IsCoproduct⇒Coproduct 𝒞 (cp₁ {A} {B} {C})) cp₂