Agda unit dioid

Unit.agda

module Algebra.Dioid.Unit where

open import Algebra.Dioid using (Dioid; zero; one; _+_; _*_)
import Algebra.Dioid

data Unit : Set where
  unit : Unit

data _≡_ : (x y : Unit) -> Set where
  reflexivity  : ∀ {x     : Unit} ->                   x ≡ x
  symmetry     : ∀ {x y   : Unit} -> x ≡ y ->          y ≡ x
  transitivity : ∀ {x y z : Unit} -> x ≡ y -> y ≡ z -> x ≡ z

unit-dioid : Dioid -> Unit
unit-dioid zero = unit
unit-dioid one  = unit
unit-dioid (r + s) = unit
unit-dioid (r * s) = unit

unit-dioid-lawful : ∀ {r s : Dioid} -> r Algebra.Dioid.≡ s -> unit-dioid r ≡ unit-dioid s
unit-dioid-lawful {r} {.r} Algebra.Dioid.reflexivity = reflexivity
unit-dioid-lawful {r} {s} (Algebra.Dioid.symmetry eq) = symmetry (unit-dioid-lawful eq)
unit-dioid-lawful {r} {s} (Algebra.Dioid.transitivity eq eq₁) = transitivity (unit-dioid-lawful eq) (unit-dioid-lawful eq₁)
unit-dioid-lawful {.(_ + _)} {.(_ + _)} (Algebra.Dioid.+left-congruence eq) = reflexivity
unit-dioid-lawful {.(_ + _)} {.(_ + _)} (Algebra.Dioid.+right-congruence eq) = reflexivity
unit-dioid-lawful {.(_ * _)} {.(_ * _)} (Algebra.Dioid.*left-congruence eq) = reflexivity
unit-dioid-lawful {.(_ * _)} {.(_ * _)} (Algebra.Dioid.*right-congruence eq) = reflexivity
unit-dioid-lawful {.(s + s)} {s} Algebra.Dioid.+idempotence with unit-dioid s
... | unit = reflexivity
unit-dioid-lawful {.(_ + _)} {.(_ + _)} Algebra.Dioid.+commutativity = reflexivity
unit-dioid-lawful {.(_ + (_ + _))} {.(_ + _ + _)} Algebra.Dioid.+associativity = reflexivity
unit-dioid-lawful {.(s + zero)} {s} Algebra.Dioid.+zero-identity with unit-dioid s
... | unit = reflexivity
unit-dioid-lawful {.(_ * (_ * _))} {.(_ * _ * _)} Algebra.Dioid.*associativity = reflexivity
unit-dioid-lawful {.(zero * _)} {.zero} Algebra.Dioid.*left-zero = reflexivity
unit-dioid-lawful {.(_ * zero)} {.zero} Algebra.Dioid.*right-zero = reflexivity
unit-dioid-lawful {.(one * s)} {s} Algebra.Dioid.*left-identity with unit-dioid s
... | unit = reflexivity
unit-dioid-lawful {.(s * one)} {s} Algebra.Dioid.*right-identity with unit-dioid s
... | unit = reflexivity
unit-dioid-lawful {.(_ * (_ + _))} {.(_ * _ + _ * _)} Algebra.Dioid.left-distributivity = reflexivity
unit-dioid-lawful {.((_ + _) * _)} {.(_ * _ + _ * _)} Algebra.Dioid.right-distributivity = reflexivity