{-# OPTIONS --cubical-compatible --safe #-}
module Data.Product.Nary.NonDependent where
open import Level as L using (Level; _⊔_; Lift; 0ℓ)
open import Agda.Builtin.Unit
open import Data.Product.Base as Prod
import Data.Product.Properties as Prodₚ
open import Data.Sum.Base using (_⊎_)
open import Data.Nat.Base using (ℕ; zero; suc; pred)
open import Data.Fin.Base using (Fin; zero; suc)
open import Function.Base using (const; _∘′_; _∘_)
open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _×-dec_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
open import Function.Nary.NonDependent.Base
Product⊤ : ∀ n {ls} → Sets n ls → Set (⨆ n ls)
Product⊤ zero as = ⊤
Product⊤ (suc n) (a , as) = a × Product⊤ n as
Product : ∀ n {ls} → Sets n ls → Set (⨆ n ls)
Product 0 _ = ⊤
Product 1 (a , _) = a
Product (suc n) (a , as) = a × Product n as
Allₙ : (∀ {a} {A : Set a} → Rel A a) →
∀ n {ls} {as : Sets n ls} (l r : Product n as) → Sets n ls
Allₙ R 0 l r = _
Allₙ R 1 a b = R a b , _
Allₙ R (suc n@(suc _)) (a , l) (b , r) = R a b , Allₙ R n l r
Equalₙ : ∀ n {ls} {as : Sets n ls} (l r : Product n as) → Sets n ls
Equalₙ = Allₙ _≡_
toProduct : ∀ n {ls} {as : Sets n ls} → Product⊤ n as → Product n as
toProduct 0 _ = _
toProduct 1 (v , _) = v
toProduct (suc n@(suc _)) (v , vs) = v , toProduct n vs
toProduct⊤ : ∀ n {ls} {as : Sets n ls} → Product n as → Product⊤ n as
toProduct⊤ 0 _ = _
toProduct⊤ 1 v = v , _
toProduct⊤ (suc n@(suc _)) (v , vs) = v , toProduct⊤ n vs
curryₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
(Product n as → b) → as ⇉ b
curryₙ 0 f = f _
curryₙ 1 f = f
curryₙ (suc n@(suc _)) f = curryₙ n ∘′ curry f
uncurryₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
as ⇉ b → (Product n as → b)
uncurryₙ 0 f = const f
uncurryₙ 1 f = f
uncurryₙ (suc n@(suc _)) f = uncurry (uncurryₙ n ∘′ f)
curry⊤ₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
(Product⊤ n as → b) → as ⇉ b
curry⊤ₙ zero f = f _
curry⊤ₙ (suc n) f = curry⊤ₙ n ∘′ curry f
uncurry⊤ₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
as ⇉ b → (Product⊤ n as → b)
uncurry⊤ₙ zero f = const f
uncurry⊤ₙ (suc n) f = uncurry (uncurry⊤ₙ n ∘′ f)
Product⊤-dec : ∀ n {ls} {as : Sets n ls} → Product⊤ n (Dec <$> as) → Dec (Product⊤ n as)
Product⊤-dec zero _ = yes _
Product⊤-dec (suc n) (p? , ps?) = p? ×-dec Product⊤-dec n ps?
Product-dec : ∀ n {ls} {as : Sets n ls} → Product n (Dec <$> as) → Dec (Product n as)
Product-dec 0 _ = yes _
Product-dec 1 p? = p?
Product-dec (suc n@(suc _)) (p? , ps?) = p? ×-dec Product-dec n ps?
toEqualₙ : ∀ n {ls} {as : Sets n ls} {l r : Product n as} →
l ≡ r → Product n (Equalₙ n l r)
toEqualₙ 0 eq = _
toEqualₙ 1 eq = eq
toEqualₙ (suc n@(suc _)) eq = Prod.map₂ (toEqualₙ n) (Prodₚ.,-injective eq)
fromEqualₙ : ∀ n {ls} {as : Sets n ls} {l r : Product n as} →
Product n (Equalₙ n l r) → l ≡ r
fromEqualₙ 0 eq = refl
fromEqualₙ 1 eq = eq
fromEqualₙ (suc n@(suc _)) eq = uncurry (cong₂ _,_) (Prod.map₂ (fromEqualₙ n) eq)
Levelₙ : ∀ {n} → Levels n → Fin n → Level
Levelₙ (l , _) zero = l
Levelₙ (_ , ls) (suc k) = Levelₙ ls k
Projₙ : ∀ {n ls} → Sets n ls → ∀ k → Set (Levelₙ ls k)
Projₙ (a , _) zero = a
Projₙ (_ , as) (suc k) = Projₙ as k
projₙ : ∀ n {ls} {as : Sets n ls} k → Product n as → Projₙ as k
projₙ 1 zero v = v
projₙ (suc n@(suc _)) zero (v , _) = v
projₙ (suc n@(suc _)) (suc k) (_ , vs) = projₙ n k vs
projₙ 1 (suc ()) v
zipWith : ∀ n {lsa lsb lsc}
{as : Sets n lsa} {bs : Sets n lsb} {cs : Sets n lsc} →
(∀ k → Projₙ as k → Projₙ bs k → Projₙ cs k) →
Product n as → Product n bs → Product n cs
zipWith 0 f _ _ = _
zipWith 1 f v w = f zero v w
zipWith (suc n@(suc _)) f (v , vs) (w , ws) =
f zero v w , zipWith n (λ k → f (suc k)) vs ws
Levelₙ⁻ : ∀ {n} → Levels n → Fin n → Levels (pred n)
Levelₙ⁻ (_ , ls) zero = ls
Levelₙ⁻ {suc (suc _)} (l , ls) (suc k) = l , Levelₙ⁻ ls k
Levelₙ⁻ {1} _ (suc ())
Removeₙ : ∀ {n ls} → Sets n ls → ∀ k → Sets (pred n) (Levelₙ⁻ ls k)
Removeₙ (_ , as) zero = as
Removeₙ {suc (suc _)} (a , as) (suc k) = a , Removeₙ as k
Removeₙ {1} _ (suc ())
removeₙ : ∀ n {ls} {as : Sets n ls} k →
Product n as → Product (pred n) (Removeₙ as k)
removeₙ (suc zero) zero _ = _
removeₙ (suc (suc _)) zero (_ , vs) = vs
removeₙ (suc (suc zero)) (suc k) (v , _) = v
removeₙ (suc (suc (suc _))) (suc k) (v , vs) = v , removeₙ _ k vs
removeₙ (suc zero) (suc ()) _
Levelₙ⁺ : ∀ {n} → Levels n → Fin (suc n) → Level → Levels (suc n)
Levelₙ⁺ ls zero l⁺ = l⁺ , ls
Levelₙ⁺ {suc _} (l , ls) (suc k) l⁺ = l , Levelₙ⁺ ls k l⁺
Levelₙ⁺ {0} _ (suc ())
Insertₙ : ∀ {n ls l⁺} → Sets n ls → ∀ k (a⁺ : Set l⁺) → Sets (suc n) (Levelₙ⁺ ls k l⁺)
Insertₙ as zero a⁺ = a⁺ , as
Insertₙ {suc _} (a , as) (suc k) a⁺ = a , Insertₙ as k a⁺
Insertₙ {zero} _ (suc ()) _
insertₙ : ∀ n {ls l⁺} {as : Sets n ls} {a⁺ : Set l⁺} k (v⁺ : a⁺) →
Product n as → Product (suc n) (Insertₙ as k a⁺)
insertₙ 0 zero v⁺ vs = v⁺
insertₙ (suc n) zero v⁺ vs = v⁺ , vs
insertₙ 1 (suc k) v⁺ vs = vs , insertₙ 0 k v⁺ _
insertₙ (suc n@(suc _)) (suc k) v⁺ (v , vs) = v , insertₙ n k v⁺ vs
insertₙ 0 (suc ()) _ _
Levelₙᵘ : ∀ {n} → Levels n → Fin n → Level → Levels n
Levelₙᵘ (_ , ls) zero lᵘ = lᵘ , ls
Levelₙᵘ (l , ls) (suc k) lᵘ = l , Levelₙᵘ ls k lᵘ
Updateₙ : ∀ {n ls lᵘ} (as : Sets n ls) k (aᵘ : Set lᵘ) → Sets n (Levelₙᵘ ls k lᵘ)
Updateₙ (_ , as) zero aᵘ = aᵘ , as
Updateₙ (a , as) (suc k) aᵘ = a , Updateₙ as k aᵘ
updateₙ : ∀ n {ls lᵘ} {as : Sets n ls} k {aᵘ : _ → Set lᵘ} (f : ∀ v → aᵘ v)
(vs : Product n as) → Product n (Updateₙ as k (aᵘ (projₙ n k vs)))
updateₙ 1 zero f v = f v
updateₙ (suc (suc _)) zero f (v , vs) = f v , vs
updateₙ (suc n@(suc _)) (suc k) f (v , vs) = v , updateₙ n k f vs
updateₙ 1 (suc ()) _ _
updateₙ′ : ∀ n {ls lᵘ} {as : Sets n ls} k {aᵘ : Set lᵘ} (f : Projₙ as k → aᵘ) →
Product n as → Product n (Updateₙ as k aᵘ)
updateₙ′ n k = updateₙ n k