FiniteSets Fintie Sets in Cubical Agda An implementation of the type of finite sets in Cubical Agda based on the Coq formalisation.