pseudo normed abelian groups

Stream: condensed mathematics

[Kevin Buzzard]

Is it going to be a problem that we have defined pseudo normed abelian groups to be abelian groups (i.e. types plus a group structure), whereas on p66 of analytic.pdf after the proof of Prop 9.10 Peter defines them in an arbitrary topos?

[Peter Scholze]

It shouldn't be a problem for the intended application of the notion; Johan has formalized "profinitely filtered pseudo normed abelian groups" which is the relevant kind of internal example (a special kind of pseudo normed abelian groups internally in condensed sets)