[Agda] Re: Data.Nat.Primality.Prime and irreducibility

[Dr. ERDI Gergo]

On Sat, 7 Mar 2015, N. Raghavendra wrote:

> data Irreducible (n : Carrier) : Set (ℓ ⊔ c) where
>  irreducible : (notUnit : ¬ isUnit n) →
>                (prf : ∀ x y → n ≈ x * y → isUnit x ⊎ isUnit y) →
>                Irreducible n
>
> where isUnit n means that n . m ~ e for some m, where e is the identity
> element of the monoid.

Yeah, I've been struggling with this point as well. I ended up just 
looking up irreducibility in Wikipedia where it is defined for integral 
domains, so I didn't want to push it too far from that.

In more practical terms however, since 0 is not a unit of the 
multiplicative monoid of Nat, so wouldn't your definition allow for 0 
being irreducible?

> Incidentally, why do you want to define Irreducible as a type, rather
> than a function like Prime in Data.Nat.Primality?  I ask because I've
> been wondering when to define a type, and when to define a function, in
> my own proofs.

I like naming things. Let's suppose you're writing Haskell code (just to 
stay in the realm of practicality; also because I am approaching Agda as a 
programmer and not as a mathematician). Would you ever write

type Foo = Either (Int, Bool) (Either (Either () String) Double)

instead of

data Foo = Bar Int Bool
          | Baz (Maybe String)
          | Quux Double

? The first is more of an encoding of the latter than a proper definition 
that people would want to use. And I firmly believe programs are to be 
written first and foremost for other humans.