Trivial (Zero) element

[ysharoda]

A trivial/zero element of an algebraic structure is the structure defined over the unit type. There are different ways for doing this:

1. Extending the definition of monoid with uniqueness axiom.
2. Instantiate the carrier of monoid with the unit type. The approach used here

The problem with the second option is we need to provide proofs if we are to provide the definition of the instance. For example, for the definition of Monoid

record Monoid (A : Set) : Set where 
....... 

will be instantiated as

data Unit : Set where 
   unit : Unit 
unitMonoid : Monoid Unit 
unitMonoid = monoid unit (\ x y -> unit) ? ? ? 

The link above, for the agda definition defines the unitMonoid using record keyword and skips the proofs. Is that correct?

[JacquesCarette]

The agda definition does something clever but invisible: the missing proofs are so trivial that they can be inferred automatically, so they are skipped.

[ysharoda]

But this won't work in Tog, and should not generally be the approach when we abstract over languages. Would all formal systems be able to infer them?

[JacquesCarette]

Right - we need to be explicit. And no, most systems are not set up to infer these automatically, though I'm pretty sure others can too.

[ysharoda]

Then we need to find out a way to deal with proofs, if we choose to define zero monoid as instance of monoid - which I believe is the better option

[JacquesCarette]

I agree. In tog, you should be able to do this, right? Exporting these proofs to other systems will be considerably more challenging.

Hmm, I wonder what Universal Algebra has to say about that. [I'm guessing it is actually quite silent about it]

[ysharoda]

I am not sure how tog works with proofs, and the universal algbera definitions. will check and have better answers

[JacquesCarette]

Looking up the definitions of this again, I see that the categorical definition is the cleanest: a zero object it both initial and terminal. Having a zero object is thus a property of a theory, and should be defined as some sort of predicate (the same way a category being a groupoid is a predicate, implemented via IsGroupoid that asks for extra structure satisfying certain equations).

The simplest statement of it then involves the conjunction of 2 predicates, IsInitial and IsTerminal. These can then be stated in the context of having the theory and its homomorphisms.

What the Zero.agda file uses, implicitly, is the theorem that for singly-sorted theories, such an object is necessarily supported on a singleton (I forget the exact reasons, but it is again category-theoretic) if it exists at all. It won't always exist though. So IsInitial, IsTerminal and IsZero are way more robust because those predicates always make sense. It's just that sometimes IsZero has some simple witnesses, sometimes it doesn't (there is no Zero Field, for example).

You should focus on the universal stuff, and comment on the things that are not. This is the same problem as 'actions' in the paper: it's common but not universal.

[ysharoda]

Make sense. As you said in a previous comment, universal algebra books only mention the singleton constraint and remain silent to any details.