Mercurial > hg > Members > kono > Proof > category
view src/category-ex.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 | ac53803b3b2a |
children |
line wrap: on
line source
-- {-# OPTIONS --cubical-compatible --safe #-} module category-ex where open import Level open import Category postulate c₁ c₂ ℓ : Level postulate A : Category c₁ c₂ ℓ postulate a b c : Obj A postulate g : Hom A a b postulate f : Hom A b c open Category.Category h = _o_ A f g i = A [ f o g ]