Define multicategories

anshwad10 · anshwad10 · commit 76170bed7296 · 2025-11-24T13:03:27.000+05:30
The promised sequel to #1212
diff --git a/Cubical/Categories/Multicategories.agda 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
@@ -0,0 +1 @@
+module Cubical.Categories.Multicategories.Base where

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+module Cubical.Categories.Multicategories where`
	`2`	`+`
	`3`	`+open import Cubical.Categories.Multicategories.Base`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1 @@`
	`1`	`+module Cubical.Categories.Multicategories.Base where`