diff options
Diffstat (limited to 'Category/Cartesian')
| -rw-r--r-- | Category/Cartesian/Instance/SymMonCat.agda | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Category/Cartesian/Instance/SymMonCat.agda b/Category/Cartesian/Instance/SymMonCat.agda index 7d91d52..1b4af4a 100644 --- a/Category/Cartesian/Instance/SymMonCat.agda +++ b/Category/Cartesian/Instance/SymMonCat.agda @@ -4,10 +4,12 @@ open import Level using (Level; suc; _⊔_) module Category.Cartesian.Instance.SymMonCat {o ℓ e : Level} where -open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat) +open import Category.Instance.SymMonCat {o} {ℓ} {e} using (module Lax) open import Category.Instance.Properties.SymMonCat {o} {ℓ} {e} using (SymMonCat-Cartesian) open import Categories.Category.Cartesian.Bundle using (CartesianCategory) +open Lax using (SymMonCat) + SymMonCat-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) SymMonCat-CC = record { U = SymMonCat |