diff --git a/code/agda-issomething/example.agda b/code/agda-issomething/example.agda index 81fd591..78b1172 100644 --- a/code/agda-issomething/example.agda +++ b/code/agda-issomething/example.agda @@ -46,10 +46,10 @@ module SecondAttempt where open IsSemigroup isSemigroup public - record IsContrivedExample {A : Set a} (_∙_ : A → A → A) : Set a where + record IsContrivedExample {A : Set a} (zero : A) (_∙_ : A → A → A) : Set a where field -- first property - monoid : IsMonoid _∙_ + monoid : IsMonoid zero _∙_ -- second property; Semigroup is a stand-in. semigroup : IsSemigroup _∙_ @@ -78,10 +78,10 @@ module ThirdAttempt {A : Set a} (_∙_ : A → A → A) where open IsSemigroup isSemigroup public - record IsContrivedExample : Set a where + record IsContrivedExample (zero : A) : Set a where field -- first property - monoid : IsMonoid _∙_ + monoid : IsMonoid zero -- second property; Semigroup is a stand-in. - semigroup : IsSemigroup _∙_ + semigroup : IsSemigroup