Given the recent edits, allow me to ask:

- Has anyone looked into formalizing topological K-theory in homotopy type theory?

We are specifically after twisted equivariant K-theory, for which it would be important to have not any construction of KU, but to have specifically the space of *Fredholm operators* axiomatized as a topological (real-cohesive) 0-type, whose shape would give $KU$.

Does this seem feasible, to formalized spaces of Fredholm operators in (real-)cohesive homotopy type theory, and proceed from there to a discussion of topological K-theory? Has anything in the direction been looked at before (separable Hilbert spaces, bounded linear operators, … in HoTT)?

]]>