{-# 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 }