module Palmse.Monoid.Laws (A : Set) where import Palmse.Monoid.Exp; open Palmse.Monoid.Exp A infix 2 _∼_ data _∼_ : Exp -> Exp -> Set where ass : {e e' e'' : Exp} -> (e ○ e') ○ e'' ∼ e ○ (e' ○ e'') idl : {e : Exp} -> id ○ e ∼ e idr : {e : Exp} -> e ○ id ∼ e ref : {e : Exp} -> e ∼ e sym : {e e' : Exp} -> e ∼ e' -> e' ∼ e tra : {e e' e'' : Exp} -> e ∼ e' -> e' ∼ e'' -> e ∼ e'' fun : {e e' e'' e''' : Exp} -> e ∼ e' -> e'' ∼ e''' -> e ○ e'' ∼ e' ○ e''' {- e ∼ e' is a family of sets indexed by the expressions e and e', i e an "inductive family". The elements of the set e ∼ e' are "proof objects", think of them as derivation trees built up by the inference rules for ∼. We are using the Curry-Howard isomorphism: an inductive relation is represented by an inductive family of sets. -} open import Relation.Binary ExpSetoid : Set -> Setoid ExpSetoid A = record {carrier = Exp; _≈_ = _∼_; isEquivalence = record {refl = ref; sym = sym; trans = tra } }