CwFs, indexed families, etc

Stream: Is there code for X?

[Joey Eremondi]

I'm wondering if anyone has done work in Lean with Categories with Families. Even a library of the category Fam (of indexed families of sets) would help, since a CwF is just a Fam-valued presheaf plus some rules about comprehension.
I know you can define Fam as the arrow category of Set (or Type I guess in Lean), so if there's nothing that's probably where I'll start.

[Trebor Huang]

I did some preliminary work using natural models (which is virtually equivalent to CwFs but you get to use more categorical machinery) in a private project. I didn't get very far though.

[Trebor Huang]

Regarding Fam there seems to be some universe level problems. You definitely want it to be universe polymorphic because you want to define standard Set-valued models that interprets functions as set functions etc. But defining it as a family of sets or an arrow gives you inequivalent configurations of universes.