[Agda] Q: Equational Reasoning

[Peter Hancock]

Conor McBride wrote:

> I'd like to see a clearer Set/Prop distinction, with
> support for the appropriate style in each. (Of course,
> you need proof irrelevance to get away with it...)

I've probably asked you (100s of times) before, but I've never got the
hang of Props.  I'm particularly interested in
Pi01 props, ie. (all x : N)...x..., where ...x...
is decidable, and presumably a Prop.  Examples are
the consistency of ZF, normalisation theorems,
Goldbach's conjecture, FLT, or (so I'm told) Riemann's
Hypothesis.  From a "behavioural" point of view,
their proofs (should they exist) all look like \x.* .

Are they Props?  In what sense are their proofs irrelevant?

I'm not being rhetorical, I just find something
very paradoxical about Props, and would like to
understand.

Hank