This repository contains a formalisation of the circle, together with some proofs (about the circle). Namely:
- Formal definition of the circle
- The circle is connected
- The evaluation function is an equivalence
- Formal definition of a set bundle
- Set families lemma
- Equivalences about the circle set bundle