Definition of multicategories

Cubical/Categories/Multicategory/Base.agda

@@ -0,0 +1,34 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Multicategory.Base where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Nat
+open import Cubical.Data.FinData as Fin
+open import Cubical.Data.List as List
+open import Cubical.Data.List.FinData as List
+
+private variable
+  ℓ ℓ' : Level
+
+record Multicategory ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
+  no-eta-equality
+
+  field
+    ob : Type ℓ
+    Hom : List ob → ob → Type ℓ'
+    id : {x : ob} → Hom [ x ] x
+    _⋆_ : {ys : List ob} {z : ob} {xss : FinVec (List ob) (length ys)}
+        → (fs : ∀ k → Hom (xss k) (lookup ys k)) → (g : Hom ys z) → Hom (foldrFinVec _++_ [] xss) z
+
+    ⋆IdR : {xs : List ob} {y : ob} → (f : Hom xs y)
+         → PathP (λ i → Hom (++-unit-r xs i) y) (_⋆_ {xss = λ _ → xs} (λ where zero → f) id) f
+
+    ⋆IdL : {xs : List ob} {y : ob} → (f : Hom xs y)
+         → PathP (λ i → Hom (tabulate'-lookup xs i) y) ((λ _ → id) ⋆ f) f
+
+    ⋆Assoc : {zs : List ob} {w : ob} {yss : FinVec (List ob) (length zs)} {xsss : ∀ k → FinVec (List ob) (length (yss k))}
+           → (h : Hom zs w) (gs : ∀ k → Hom (yss k) (lookup zs k)) (fss : ∀ k l → Hom (xsss k l) (lookup (yss k) l))
+           → PathP (λ i → Hom {!   !} w)
+             ((λ kl → {!   !}) ⋆ (gs ⋆ h))
+             ((λ k → fss k ⋆ gs k) ⋆ h)

Cubical/Data/FinData/Base.agda

@@ -79,8 +79,18 @@ FinVec A n = Fin n → A
 replicateFinVec : (n : ℕ) → A → FinVec A n
 replicateFinVec _ a _ = a
 
-
 _++Fin_ : {n m : ℕ} → FinVec A n → FinVec A m → FinVec A (n + m)
 _++Fin_ {n = zero} _ W i = W i
 _++Fin_ {n = suc n} V _ zero = V zero
 _++Fin_ {n = suc n} V W (suc i) = ((V ∘ suc) ++Fin W) i
+
+foldrFinVec : {n : ℕ} → (A → B → B) → B → FinVec A n → B
+foldrFinVec {n = zero} f x V = x
+foldrFinVec {n = suc n} f x V = f (V zero) (foldrFinVec f x (V ∘ suc))
+
+foldlFinVec : {n : ℕ} → (B → A → B) → B → FinVec A n → B
+foldlFinVec {n = zero} f x V = x
+foldlFinVec {n = suc n} f x V = foldlFinVec f (f x (V zero)) (V ∘ suc)
+
+mapFinVec : {n : ℕ} → (A → B) → FinVec A n → FinVec B n
+mapFinVec f ^a k = f (^a k)

Cubical/Data/List/FinData.agda

@@ -11,7 +11,7 @@ open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Sigma.Properties
 open import Cubical.Data.Nat
 
-variable
+private variable
   ℓ : Level
   A B : Type ℓ
 
@@ -21,8 +21,7 @@ lookup (x ∷ xs) zero    = x
 lookup (x ∷ xs) (suc i) = lookup xs i
 
 tabulate : ∀ n → (Fin n → A) → List A
-tabulate zero ^a = []
-tabulate (suc n) ^a = ^a zero ∷ tabulate n (^a ∘ suc)
+tabulate n = foldrFinVec _∷_ []
 
 length-tabulate : ∀ n → (^a : Fin n → A) → length (tabulate n ^a) ≡ n
 length-tabulate zero ^a = refl
@@ -58,3 +57,32 @@ lookup-map f (x ∷ xs) zero zero p = refl
 lookup-map f (x ∷ xs) zero (suc p1) p = ⊥.rec (znotsP p)
 lookup-map f (x ∷ xs) (suc p0) zero p = ⊥.rec (snotzP p)
 lookup-map f (x ∷ xs) (suc p0) (suc p1) p = lookup-map f xs p0 p1 (injSucFinP p)
+
+tabulate' : ∀ n → (Fin n → A) → List A
+tabulate' n ^a = foldrFinVec _++_ [] (mapFinVec [_] ^a)
+
+tabulate'≡tabulate : ∀ n (^a : Fin n → A) → tabulate' n ^a ≡ tabulate n ^a
+tabulate'≡tabulate zero ^a = refl
+tabulate'≡tabulate (suc n) ^a = congR _∷_ (tabulate'≡tabulate n (^a ∘ suc))
+
+length-tabulate' : ∀ n → (^a : Fin n → A) → length (tabulate' n ^a) ≡ n
+length-tabulate' zero ^a = refl
+length-tabulate' (suc n) ^a = cong suc (length-tabulate' n (^a ∘ suc))
+
+tabulate'-lookup : ∀ (xs : List A) → tabulate' (length xs) (lookup xs) ≡ xs
+tabulate'-lookup [] = refl
+tabulate'-lookup (x ∷ xs) = cong (x ∷_) (tabulate'-lookup xs)
+
+lookup-tabulate' : ∀ n → (^a : Fin n → A)  → PathP (λ i → (Fin (length-tabulate' n ^a i) → A)) (lookup (tabulate' n ^a)) ^a
+lookup-tabulate' (suc n) ^a i zero = ^a zero
+lookup-tabulate' (suc n) ^a i (suc p) = lookup-tabulate' n (^a ∘ suc) i p
+
+lookup-tabulate'-iso : (A : Type ℓ) → Iso (List A) (Σ[ n ∈ ℕ ] (Fin n → A))
+fun (lookup-tabulate'-iso A) xs = (length xs) , lookup xs
+inv (lookup-tabulate'-iso A) (n , f) = tabulate' n f
+leftInv (lookup-tabulate'-iso A) = tabulate'-lookup
+rightInv (lookup-tabulate'-iso A) (n , f) =
+  ΣPathP ((length-tabulate' n f) , lookup-tabulate' n f)
+
+lookup-tabulate'-equiv : (A : Type ℓ) → List A ≃ (Σ[ n ∈ ℕ ] (Fin n → A))
+lookup-tabulate'-equiv A = isoToEquiv (lookup-tabulate'-iso A)