Proof that Vec is a monoidal bifunctor from Sets with disjoint union and Natop with addition to Sets with cartesian product

Vec.agda

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

module Categories.Functor.Example.Vec where

open import Categories.Category.Core using (Category)
open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
open import Categories.Category.Instance.Nat
open import Categories.Category.Instance.Sets
open import Categories.Category.Monoidal.Construction.Product using (Product-Monoidal)
open import Categories.Category.Monoidal.Instance.Sets using (module Coproduct; module Product)
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Functor.Monoidal using (IsMonoidalFunctor)
open import Categories.NaturalTransformation using (ntHelper)
open import Data.Fin.Base using (Fin; zero; suc; splitAt; inject+; raise; join)
open import Data.Fin.Properties using (splitAt-inject+; splitAt-raise)
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.Product hiding (map)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
import Data.Sum.Properties as Sum
open import Data.Vec.Base hiding (splitAt)
open import Data.Vec.Properties
open import Function.Base using (id; _∘_; _$_; λ-)
open import Relation.Binary.PropositionalEquality

module _ where
  open import Data.Fin.Base using (Fin)
  open import Data.Nat.Base using (ℕ)
  open import Level using (Level)

  private
    variable
      m n o m′ n′ : ℕ
      a b : Level
      A : Set a
      B : Set b

  -- I'm not sure if arrange is cool enough to go in stdlib
  arrange : (Fin m → Fin n) → Vec A n → Vec A m
  arrange π xs = tabulate (lookup xs ∘ π)

  arrange-id : ∀ (xs : Vec A n) → arrange id xs ≡ xs
  arrange-id = tabulate∘lookup

  arrange-∘ : (π : Fin m → Fin n) (ρ : Fin n → Fin o) (xs : Vec A o) → arrange π (arrange ρ xs) ≡ arrange (ρ ∘ π) xs
  arrange-∘ π ρ xs = tabulate-cong (lookup∘tabulate (lookup xs ∘ ρ) ∘ π)

  arrange-cong : ∀ {π ρ : Fin m → Fin n} → π ≗ ρ → (xs : Vec A n) → arrange π xs ≡ arrange ρ xs
  arrange-cong π≗ρ xs = tabulate-cong (cong (lookup xs) ∘ π≗ρ)

  map-arrange : ∀ (π : Fin m → Fin n) (f : A → B) (xs : Vec A n) → arrange π (map f xs) ≡ map f (arrange π xs)
  map-arrange π f xs = begin
    tabulate (lookup (map f xs) ∘ π) ≡⟨ tabulate-cong (λ i → lookup-map (π i) f xs) ⟩
    tabulate (f ∘ lookup xs ∘ π)     ≡⟨ tabulate-∘ f (lookup xs ∘ π) ⟩
    map f (tabulate (lookup xs ∘ π)) ∎
    where open ≡-Reasoning

  ++-arrange : ∀ (π : Fin m → Fin n) (ρ : Fin m′ → Fin n′) (xs : Vec A n) (ys : Vec A n′) → arrange (join n n′ ∘ Sum.map π ρ ∘ splitAt m) (xs ++ ys) ≡ arrange π xs ++ arrange ρ ys
  ++-arrange {m = zero}  π ρ xs ys = tabulate-cong (λ i → lookup-++ʳ xs ys (ρ i))
  ++-arrange {m = suc m} π ρ xs ys = cong₂ _∷_ (lookup-++ˡ xs ys (π zero)) $ begin
    arrange (join _ _ ∘ Sum.map π ρ ∘ splitAt (suc m) ∘ suc) (xs ++ ys) ≡⟨ arrange-cong (cong (join _ _) ∘ Sum.map-commute ∘ splitAt m) (xs ++ ys) ⟩
    arrange (join _ _ ∘ Sum.map (π ∘ suc) ρ ∘ splitAt m) (xs ++ ys)     ≡⟨ ++-arrange (π ∘ suc) ρ xs ys ⟩
    arrange (π ∘ suc) xs ++ arrange ρ ys                                ∎
    where open ≡-Reasoning

  -- This will be in the next major release of stdlib
  map-++ : ∀ (f : A → B) (xs : Vec A m) (ys : Vec A n) →
           map f (xs ++ ys) ≡ map f xs ++ map f ys
  map-++ f []       ys = refl
  map-++ f (x ∷ xs) ys = cong (f x ∷_) (map-++ f xs ys)

VecBifunctor : ∀ o → Bifunctor (Sets o) Natop (Sets o)
VecBifunctor o = record
  { F₀ = uncurry Vec
  ; F₁ = λ { (f , π) → map f ∘ arrange π }
  ; identity = λ {_} {xs} → trans (map-id (arrange id xs)) (arrange-id xs)
  ; homomorphism = λ {_} {_} {_} → λ
    { {f , π} {g , ρ} {xs} → begin
      map (g ∘ f) (arrange (π ∘ ρ) xs)         ≡˘⟨ cong (map (g ∘ f)) (arrange-∘ ρ π xs) ⟩
      map (g ∘ f) (arrange ρ (arrange π xs))   ≡⟨ map-∘ g f _ ⟩
      map g (map f (arrange ρ (arrange π xs))) ≡˘⟨ cong (map g) (map-arrange ρ f (arrange π xs)) ⟩
      map g (arrange ρ (map f (arrange π xs))) ∎
    }
  ; F-resp-≈ = λ {_} {_} → λ
    { {f , π} {g , ρ} (f≗g , π≗ρ) {xs} → begin
      map f (arrange π xs) ≡⟨ map-cong (λ- f≗g) _ ⟩
      map g (arrange π xs) ≡⟨ cong (map g) (arrange-cong π≗ρ xs) ⟩
      map g (arrange ρ xs) ∎
    }
  }
  where open ≡-Reasoning

-- The VecBifunctor defined above is a monoidal bifunctor
-- From (Sets, ⊎) × (ℕᵒᵖ, +) to (Sets, ×)
VecBifunctorIsMonoidal : ∀ ℓ → IsMonoidalFunctor (record { monoidal = Product-Monoidal Coproduct.Sets-Monoidal (CartesianMonoidal.monoidal (CartesianCategory.cartesian Natop-Cartesian)) }) (record { monoidal = Product.Sets-Monoidal }) (VecBifunctor ℓ)
VecBifunctorIsMonoidal ℓ = record
  { ε = λ _ → []
  ; ⊗-homo = ntHelper record
    { η = λ { ((A , m) , (B , n)) (xs , ys) → map inj₁ xs ++ map inj₂ ys }
    ; commute = λ { ((f , π) , (g , ρ)) {xs , ys} → ⊗-commute f g π ρ xs ys }
    }
  ; associativity = λ { {_} {_} {_} {(xs , ys) , zs} → assoc xs ys zs }
  ; unitaryˡ = λ { {X , n} {_ , xs} → begin
    map Sum.[ _ , id ] (arrange id (map inj₂ xs)) ≡⟨ cong (map Sum.[ _ , id ]) (arrange-id (map inj₂ xs)) ⟩
    map Sum.[ _ , id ] (map inj₂ xs)              ≡˘⟨ map-∘ Sum.[ _ , id ] inj₂ xs ⟩
    map id xs                                     ≡⟨ map-id xs ⟩
    xs                                            ∎
    }
  ; unitaryʳ = λ { {X , n} {xs , _} → begin
    map Sum.[ id , _ ] (arrange (inject+ 0) (map inj₁ xs ++ [])) ≡⟨ cong (map Sum.[ id , _ ]) (tabulate-cong (lookup-++ˡ (map inj₁ xs) [])) ⟩
    map Sum.[ id , _ ] (arrange id (map inj₁ xs))                ≡⟨ cong (map Sum.[ id , _ ]) (arrange-id (map inj₁ xs)) ⟩
    map Sum.[ id , _ ] (map inj₁ xs)                             ≡˘⟨ map-∘ Sum.[ id , _ ] inj₁ xs ⟩
    map id xs                                                    ≡⟨ map-id xs ⟩
    xs ∎
    }
  }
  where
    open ≡-Reasoning
    ⊗-commute : ∀ {A A′ B B′ : Set ℓ} {m m′ n n′ : ℕ} (f : A → A′) (g : B → B′) (π : Fin m′ → Fin m) (ρ : Fin n′ → Fin n) (xs : Vec A m) (ys : Vec B n)
              → map inj₁ (map f (arrange π xs)) ++ map inj₂ (map g (arrange ρ ys))
              ≡ map (Sum.map f g) (arrange (Sum.[ inject+ n ∘ π , raise m ∘ ρ ] ∘ splitAt m′) (map inj₁ xs ++ map inj₂ ys))
    ⊗-commute {m′ = m′} f g π ρ xs ys = begin
      map inj₁ (map f (arrange π xs)) ++ map inj₂ (map g (arrange ρ ys))
        ≡˘⟨ cong₂ _++_ (map-∘ inj₁ f (arrange π xs)) (map-∘ inj₂ g (arrange ρ ys)) ⟩
      map (Sum.map₁ f ∘ inj₁) (arrange π xs) ++ map (Sum.map₂ g ∘ inj₂) (arrange ρ ys)
        ≡⟨ cong₂ _++_ (map-∘ (Sum.map f g) inj₁ (arrange π xs)) (map-∘ (Sum.map f g) inj₂ (arrange ρ ys)) ⟩
      map (Sum.map f g) (map inj₁ (arrange π xs)) ++ map (Sum.map f g) (map inj₂ (arrange ρ ys))
        ≡˘⟨ map-++ (Sum.map f g) (map inj₁ (arrange π xs)) (map inj₂ (arrange ρ ys)) ⟩
      map (Sum.map f g) (map inj₁ (arrange π xs) ++ map inj₂ (arrange ρ ys))
        ≡˘⟨ cong (map (Sum.map f g)) (cong₂ _++_ (map-arrange π inj₁ xs) (map-arrange ρ inj₂ ys)) ⟩
      map (Sum.map f g) (arrange π (map inj₁ xs) ++ arrange ρ (map inj₂ ys))
        ≡˘⟨ cong (map (Sum.map f g)) (++-arrange π ρ (map inj₁ xs) (map inj₂ ys)) ⟩
      map (Sum.map f g) (arrange (join _ _ ∘ Sum.map π ρ ∘ splitAt _) (map inj₁ xs ++ map inj₂ ys))
        ≡⟨ cong (map (Sum.map f g)) (arrange-cong (Sum.[,]-map-commute ∘ splitAt m′) (map inj₁ xs ++ map inj₂ ys)) ⟩
      map (Sum.map f g) (arrange (Sum.[ inject+ _ ∘ π , raise _ ∘ ρ ] ∘ splitAt _) (map inj₁ xs ++ map inj₂ ys))
        ∎

    assoc-lemma₁ : ∀ m n o → splitAt (m + n) ∘ Sum.[ inject+ o ∘ inject+ n , Sum.[ inject+ o ∘ raise m , raise (m + n) ] ∘ splitAt n ] ∘ splitAt m
                              ≗ Sum.[ inj₁ ∘ inject+ n , Sum.map₁ (raise m) ∘ splitAt n ] ∘ splitAt m
    assoc-lemma₁ m n o i = begin
      splitAt (m + n) (Sum.[ inject+ o ∘ inject+ n , Sum.[ inject+ o ∘ raise m , raise (m + n) ] ∘ splitAt n ] (splitAt m i))
        ≡⟨ Sum.[,]-∘-distr (splitAt (m + n)) (splitAt m i) ⟩
      Sum.[ splitAt (m + n) ∘ inject+ o ∘ inject+ n , splitAt (m + n) ∘ Sum.[ inject+ o ∘ raise m , raise (m + n) ] ∘ splitAt n ] (splitAt m i)
        ≡⟨ Sum.[,]-cong (splitAt-inject+ (m + n) o ∘ inject+ n) (Sum.[,]-∘-distr (splitAt (m + n)) ∘ splitAt n) (splitAt m i) ⟩
      Sum.[ inj₁ ∘ inject+ n , Sum.[ splitAt (m + n) ∘ inject+ o ∘ raise m , splitAt (m + n) ∘ raise (m + n) ] ∘ splitAt n ] (splitAt m i)
        ≡⟨ Sum.[,-]-cong (Sum.[,]-cong (splitAt-inject+ (m + n) o ∘ raise m) (splitAt-raise (m + n) o) ∘ splitAt n) (splitAt m i) ⟩
      Sum.[ inj₁ ∘ inject+ n , Sum.map₁ (raise m) ∘ splitAt n ] (splitAt m i)
        ∎

    assoc-lemma₂ : ∀ {A : Set ℓ} {m n o : ℕ} (xs : Vec A m) (ys : Vec A n) (zs : Vec A o)
                 → Sum.[ lookup (xs ++ ys) , lookup zs ] ∘ Sum.map₁ (raise m) ∘ splitAt n
                 ≗ lookup (ys ++ zs)
    assoc-lemma₂ {m = m} {n} {o} xs ys zs i = begin
      Sum.[ lookup (xs ++ ys) , lookup zs ] (Sum.map₁ (raise m) (splitAt n i))
        ≡⟨ Sum.[,]-map-commute (splitAt n i) ⟩
      Sum.[ lookup (xs ++ ys) ∘ raise m , lookup zs ] (splitAt n i)
        ≡⟨ Sum.[-,]-cong (lookup-++ʳ xs ys) (splitAt n i) ⟩
      Sum.[ lookup ys , lookup zs ] (splitAt n i)
        ≡˘⟨ lookup-splitAt n ys zs i ⟩
      lookup (ys ++ zs) i
        ∎
      
    assoc-lemma : ∀ {A : Set ℓ} {m n o : ℕ} (xs : Vec A m) (ys : Vec A n) (zs : Vec A o)
                 → lookup ((xs ++ ys) ++ zs) ∘ Sum.[ inject+ o ∘ inject+ n , Sum.[ inject+ o ∘ raise m , raise (m + n) ] ∘ splitAt n ] ∘ splitAt m
                 ≗ lookup (xs ++ (ys ++ zs))
    assoc-lemma {m = m} {n} {o} xs ys zs i = begin
      lookup ((xs ++ ys) ++ zs) (Sum.[ inject+ o ∘ inject+ n , Sum.[ inject+ o ∘ raise m , raise (m + n) ] ∘ splitAt n ] (splitAt m i))
        ≡⟨ lookup-splitAt (m + n) (xs ++ ys) zs _ ⟩
      Sum.[ lookup (xs ++ ys) , lookup zs ] (splitAt (m + n) (Sum.[ inject+ o ∘ inject+ n , Sum.[ inject+ o ∘ raise m , raise (m + n) ] ∘ splitAt n ] (splitAt m i)))
        ≡⟨ cong Sum.[ lookup (xs ++ ys) , lookup zs ] (assoc-lemma₁ m n o i) ⟩
      Sum.[ lookup (xs ++ ys) , lookup zs ] (Sum.[ inj₁ ∘ inject+ n , Sum.map₁ (raise m) ∘ splitAt n ] (splitAt m i))
        ≡⟨ Sum.[,]-∘-distr Sum.[ lookup (xs ++ ys) , lookup zs ] (splitAt m i) ⟩
      Sum.[ lookup (xs ++ ys) ∘ inject+ n , Sum.[ lookup (xs ++ ys) , lookup zs ] ∘ Sum.map₁ (raise m) ∘ splitAt n ] (splitAt m i)
        ≡⟨ Sum.[,]-cong (lookup-++ˡ xs ys) (assoc-lemma₂ xs ys zs) (splitAt m i) ⟩
      Sum.[ lookup xs , lookup (ys ++ zs) ] (splitAt m i)
        ≡˘⟨ lookup-splitAt m xs (ys ++ zs) i ⟩
      lookup (xs ++ (ys ++ zs)) i
        ∎

    assoc : ∀ {X Y Z : Set ℓ} {m n o : ℕ} (xs : Vec X m) (ys : Vec Y n) (zs : Vec Z o)
          → map Sum.assocʳ (arrange (Sum.[ inject+ o ∘ inject+ n , Sum.[ inject+ o ∘ raise m , raise (m + n) ] ∘ splitAt n ] ∘ splitAt m) (map inj₁ (map inj₁ xs ++ map inj₂ ys) ++ map inj₂ zs))
          ≡ map inj₁ xs ++ map inj₂ (map inj₁ ys ++ map inj₂ zs)
    assoc {m = m} {n} {o} xs ys zs = begin
      map Sum.assocʳ (arrange (Sum.[ inject+ o ∘ inject+ n , Sum.[ inject+ o ∘ raise m , raise (m + n) ] ∘ splitAt n ] ∘ splitAt m) (map inj₁ (map inj₁ xs ++ map inj₂ ys) ++ map inj₂ zs))
        ≡⟨ cong (map Sum.assocʳ) (cong (arrange _) (cong (_++ map inj₂ zs) (map-++ inj₁ (map inj₁ xs) (map inj₂ ys)))) ⟩
      map Sum.assocʳ (arrange (Sum.[ inject+ o ∘ inject+ n , Sum.[ inject+ o ∘ raise m , raise (m + n) ] ∘ splitAt n ] ∘ splitAt m) ((map inj₁ (map inj₁ xs) ++ map inj₁ (map inj₂ ys)) ++ map inj₂ zs))
        ≡⟨ cong (map Sum.assocʳ) (tabulate-cong (assoc-lemma (map inj₁ (map inj₁ xs)) (map inj₁ (map inj₂ ys)) (map inj₂ zs))) ⟩
      map Sum.assocʳ (tabulate (lookup (map inj₁ (map inj₁ xs) ++ (map inj₁ (map inj₂ ys) ++ map inj₂ zs))))
        ≡⟨ cong (map Sum.assocʳ) (tabulate∘lookup (map inj₁ (map inj₁ xs) ++ (map inj₁ (map inj₂ ys) ++ map inj₂ zs))) ⟩
      map Sum.assocʳ (map inj₁ (map inj₁ xs) ++ (map inj₁ (map inj₂ ys) ++ map inj₂ zs))
        ≡˘⟨ cong (map Sum.assocʳ) (cong₂ _++_ (map-∘ inj₁ inj₁ xs) (cong (_++ map inj₂ zs) (map-∘ inj₁ inj₂ ys))) ⟩
      map Sum.assocʳ (map (inj₁ ∘ inj₁) xs ++ (map (inj₁ ∘ inj₂) ys ++ map inj₂ zs))
        ≡⟨ map-++ Sum.assocʳ (map (inj₁ ∘ inj₁) xs) (map (inj₁ ∘ inj₂) ys ++ map inj₂ zs) ⟩
      map Sum.assocʳ (map (inj₁ ∘ inj₁) xs) ++ map Sum.assocʳ (map (inj₁ ∘ inj₂) ys ++ map inj₂ zs)
        ≡⟨ cong (map Sum.assocʳ (map (inj₁ ∘ inj₁) xs) ++_) (map-++ Sum.assocʳ (map (inj₁ ∘ inj₂) ys) (map inj₂ zs)) ⟩
      map Sum.assocʳ (map (inj₁ ∘ inj₁) xs) ++ (map Sum.assocʳ (map (inj₁ ∘ inj₂) ys) ++ map Sum.assocʳ (map inj₂ zs))
        ≡˘⟨ cong₂ _++_ (map-∘ Sum.assocʳ (inj₁ ∘ inj₁) xs) (cong₂ _++_ (map-∘ Sum.assocʳ (inj₁ ∘ inj₂) ys) (map-∘ Sum.assocʳ inj₂ zs)) ⟩
      map inj₁ xs ++ (map (inj₂ ∘ inj₁) ys ++ map (inj₂ ∘ inj₂) zs)
        ≡⟨ cong (map inj₁ xs ++_) (cong₂ _++_ (map-∘ inj₂ inj₁ ys) (map-∘ inj₂ inj₂ zs)) ⟩
      map inj₁ xs ++ (map inj₂ (map inj₁ ys) ++ map inj₂ (map inj₂ zs))
        ≡˘⟨ cong (map inj₁ xs ++_) (map-++ inj₂ (map inj₁ ys) (map inj₂ zs)) ⟩
      map inj₁ xs ++ map inj₂ (map inj₁ ys ++ map inj₂ zs)
        ∎