Well-founded material sets

[fredrik-bakke]

Defines elementhood structures, material sets and well-founded material sets, as introduced in https://arxiv.org/pdf/2312.13024.

[elisabethstenholm]

This can be removed, as it is just a copy of (some of) the code at https://git.app.uib.no/hott/hott-set-theory

[elisabethstenholm]

Hm, or is it nice to have a link to a snapshot of the code in nice clickable html? 🤔

[fredrik-bakke]

Oh, I didn't notice the main version does not have a clickable html page. That is definitely very handy.

[fredrik-bakke]

@elisabethstenholm Does it make sense to call a type with an elementhood structure a "material set" at all? Or is it the elements of such a type that are "material sets"? Or neither?

[elisabethstenholm]

@elisabethstenholm Does it make sense to call a type with an elementhood structure a "material set" at all? Or is it the elements of such a type that are "material sets"? Or neither?

I would say that it is the elements of the type with the associated elementhood relation, that are "material sets".

[fredrik-bakke]

I would say that it is the elements of the type with the associated elementhood relation, that are "material sets".

Hm, then what do you call a type with an elementhood structure? A "type with elementhood"?

[elisabethstenholm]

I would say that it is the elements of the type with the associated elementhood relation, that are "material sets".

Hm, then what do you call a type with an elementhood structure? A "type with elementhood"?

A type together with an extensional elementhood relation, is what we have called an "elementhood structure" in our paper.

https://git.app.uib.no/hott/hott-set-theory/-/blob/master/src/e-structure/core.agda?ref_type=heads#L54-L57

[fredrik-bakke]

Turns out there is considerable overlap with formalizations in trees, and in addition the names in this PR need to be rethought, so I'll mark this as a draft for now.