diff --git a/src/Categories/Category/Instance/Thinnings.agda b/src/Categories/Category/Instance/Thinnings.agda new file mode 100644 index 0000000..e37abeb --- /dev/null +++ b/src/Categories/Category/Instance/Thinnings.agda @@ -0,0 +1,25 @@ +{-# OPTIONS --safe --without-K #-} + +module Categories.Category.Instance.Thinnings where + +open import Categories.Category.Core +open import Categories.Category.Helper +open import Data.List.Base using (List) +open import Relation.Binary.PropositionalEquality + +open import Thinning +open import Thinning.Properties + +Thinnings : ∀ {a} (A : Set a) → Category a a a +Thinnings A = categoryHelper record + { Obj = List A + ; _⇒_ = Thinning A + ; _≈_ = _≡_ + ; id = id + ; _∘_ = _∘_ + ; assoc = assoc _ _ _ + ; identityˡ = identityˡ _ + ; identityʳ = identityʳ _ + ; equiv = isEquivalence + ; ∘-resp-≈ = cong₂ _∘_ + }