(Also anyone about to heckle: I am a total baby wrt. dependent type theory, despite 20 years of paper-reading and fiddling; go easy!)
Conversation
Me too, at least on the first bit!
I know about Prop; the similarity is that type-level things, like Prop, are erased ~ proof-irrelevant.
1
The diff is that one's a type, the other, a term... so, I guess, a theorem, vs a proof. But I'm uneasy on the definitiveness of this answer.
2
In CoC at least there's only one term/type language; just depends which universe & side of the colon a term is in/on.
1
Terms in type-positions can all be erased; "irrelevance" is whether you also erase the _values_ (because it's a proof: existence is enough)
1
1
One can try to auto-erase proof-values where they occur (intermixed w/ other values) or separate universes for "propositions" & erase all.
2
Thanks! I know; Twitter is low bandwidth for this kind of thing. Most likely the answer to my original question is "no",
1
but I'm familiar with (most of) the basic concepts (to my knowledge).
1
Ok, sorry for over-elaborating! I'm at that point in learning a thing where it helps me consolidate to regurgitate :)
2
1
I'm leaning some things from your vomit, so thank you! Keep retching! 🤮🤮🤮
1
2
I was wondering about proof erasure on the walk home from work last night, and your stuff about `Prop` helps!