Mercurial > hg > Members > kono > Proof > category
diff src/CCCMonoidal.agda @ 1110:45de2b31bf02
add original library and fix for safe mode
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 07 Oct 2023 19:43:31 +0900 |
parents | 9914aa88b8f5 |
children |
line wrap: on
line diff
--- a/src/CCCMonoidal.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/CCCMonoidal.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,10 +1,12 @@ +-- {-# OPTIONS --cubical-compatible --safe #-} + open import Level open import Category open import CCC module CCCMonoidal {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( c : CCC A ) where open import HomReasoning -open import cat-utility +open import Definitions open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> ) open import Category.Constructions.Product open import Relation.Binary.PropositionalEquality as ER hiding ( [_] )