{-# OPTIONS --without-K --safe #-} module Categories.Category.Dagger.Construction.Discrete where open import Relation.Binary.PropositionalEquality open import Categories.Category.Dagger open import Categories.Category.Construction.StrictDiscrete Discrete-HasDagger : ∀ {a} (A : Set a) → HasDagger (Discrete A) Discrete-HasDagger A = record { _† = sym ; †-identity = refl ; †-homomorphism = λ { {f = refl} {g = refl} → refl } ; †-resp-≈ = cong sym ; †-involutive = λ { refl → refl} } Discrete-DaggerCategory : ∀ {a} (A : Set a) → DaggerCategory a a a Discrete-DaggerCategory A = record { hasDagger = Discrete-HasDagger A }