ZFC with Grothendieck universes

Stream: Is there code for X?

[Chris Henson]

In Definitional Proof Irrelevance Made Accessible, there is a model interpreting their type theory into ZFC with Grothendieck universes, similar to #leantt. The Rocq formalization includes this, but is done axiomatically.

I'd like to eventually have formalizations of this nature in CSLib. I am working on the type theory side, but does any of the set theory side (universes, accessibility in ZFC, etc.) exist anywhere already?

[Dexin Zhang]

I believe docs#ZFSet is already a model of ZFC. There is no formalization of Grothendieck universes in Mathlib yet, but they are equivalent to $V_\kappa$ when $\kappa$ is an inaccessible cardinal, where you can use docs#ZFSet.vonNeumann and docs#Cardinal.IsInaccessible