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

open import Categories.Category
open import Categories.Category.Cartesian
open import Categories.Category.BinaryProducts
open import Categories.Category.Cocartesian
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR

module Distributive.Core {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open Category 𝒞
open M 𝒞

private
    variable
        A B C : Obj

record Distributive (cartesian : Cartesian 𝒞) (cocartesian : Cocartesian 𝒞) : Set (levelOfTerm 𝒞) where
    open Cartesian cartesian
    open BinaryProducts products
    open Cocartesian cocartesian

    field
        distributeˡ : (A × B + A × C) ≅ (A × (B + C))

    distributeʳ : ∀ {A B C : Obj} → (B × A + C × A) ≅ (B + C) × A
    distributeʳ {A} {B} {C} = record 
        { from = (swap ∘ from) ∘ (swap +₁ swap)
        ; to = ((swap +₁ swap) ∘ to) ∘ swap 
        ; iso = record 
            { isoˡ = begin 
                (((swap +₁ swap) ∘ to) ∘ swap) ∘ (swap ∘ from) ∘ (swap +₁ swap) ≈⟨ pullˡ (pullˡ (pullʳ swap∘swap)) ⟩ 
                ((((swap +₁ swap) ∘ to) ∘ id) ∘ from) ∘ (swap +₁ swap)          ≈⟨ identityʳ ⟩∘⟨refl ⟩∘⟨refl ⟩
                (((swap +₁ swap) ∘ to) ∘ from) ∘ (swap +₁ swap)                 ≈⟨ pullʳ isoˡ ⟩∘⟨refl ⟩
                ((swap +₁ swap) ∘ id) ∘ (swap +₁ swap)                          ≈⟨ identityʳ ⟩∘⟨refl ⟩
                (swap +₁ swap) ∘ (swap +₁ swap)                                 ≈⟨ +₁∘+₁ ⟩
                ((swap ∘ swap) +₁ (swap ∘ swap))                                ≈⟨ +₁-cong₂ swap∘swap swap∘swap ⟩
                (id +₁ id)                                                      ≈⟨ +-unique id-comm-sym id-comm-sym ⟩
                id                                                              ∎ 
            ; isoʳ = begin 
                ((swap ∘ from) ∘ (swap +₁ swap)) ∘ ((swap +₁ swap) ∘ to) ∘ swap  ≈⟨ pullˡ (pullˡ (pullʳ +₁∘+₁)) ⟩ 
                (((swap ∘ from) ∘ ((swap ∘ swap) +₁ (swap ∘ swap))) ∘ to) ∘ swap ≈⟨ (((refl⟩∘⟨ +₁-cong₂ swap∘swap swap∘swap) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
                (((swap ∘ from) ∘ (id +₁ id)) ∘ to) ∘ swap                       ≈⟨ (((refl⟩∘⟨ +-unique id-comm-sym id-comm-sym) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
                (((swap ∘ from) ∘ id) ∘ to) ∘ swap                               ≈⟨ ((identityʳ ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
                ((swap ∘ from) ∘ to) ∘ swap                                      ≈⟨ (pullʳ isoʳ ⟩∘⟨refl) ⟩ 
                (swap ∘ id) ∘ swap                                               ≈⟨ (identityʳ ⟩∘⟨refl) ⟩ 
                swap ∘ swap                                                      ≈⟨ swap∘swap ⟩ 
                id                                                               ∎ 
            }
        }
        where 
            open _≅_ (distributeˡ {A} {B} {C})
            open HomReasoning
            open Equiv
            open MR 𝒞