diff --git a/Cubical/Categories/Multicategories.agda b/Cubical/Categories/Multicategories.agda new file mode 100644 index 0000000000..9ff777d743 --- /dev/null +++ b/Cubical/Categories/Multicategories.agda @@ -0,0 +1,3 @@ +module Cubical.Categories.Multicategories where + +open import Cubical.Categories.Multicategories.Base diff --git a/Cubical/Categories/Multicategories/Base.agda b/Cubical/Categories/Multicategories/Base.agda new file mode 100644 index 0000000000..c3cda73088 --- /dev/null +++ b/Cubical/Categories/Multicategories/Base.agda @@ -0,0 +1,19 @@ +open import Cubical.Foundations.Prelude + +open import Cubical.WildCat.Functor +open import Cubical.WildCat.Monad +open import Cubical.WildCat.Instances.Types + +module Cubical.Categories.Multicategories.Base ℓ (T : WildMonad (TypeCat ℓ)) where + +open WildFunctor (T .fst) renaming (F-ob to T-ob; F-hom to T-hom; F-id to T-id; F-seq to T-seq) +open IsMonad (T .snd) +open WildNatTrans η renaming (N-ob to η-ob; N-hom to η-hom) +open WildNatTrans μ renaming (N-ob to μ-ob; N-hom to μ-hom) + +record Multicategory ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where + no-eta-equality + field + Ob : Type ℓ + Hom : T-ob Ob → Ob → Type ℓ' + id : ∀ {x} → Hom (η-ob _ x) x