# Condensed Objects #

This file defines the category of condensed objects in a category `C`

, following the work
of Clausen-Scholze and Barwick-Haine.

## Implementation Details #

We use the coherent Grothendieck topology on `CompHaus`

, and define condensed objects in `C`

to
be `C`

-valued sheaves, with respect to this Grothendieck topology.

Note: Our definition more closely resembles "Pyknotic objects" in the sense of Barwick-Haine, as we do not impose cardinality bounds, and manage universes carefully instead.

## References #

- [barwickhaine2019]:
*Pyknotic objects, I. Basic notions*, 2019. - [scholze2019condensed]:
*Lectures on Condensed Mathematics*, 2019.

`Condensed.{u} C`

is the category of condensed objects in a category `C`

, which are
defined as sheaves on `CompHaus.{u}`

with respect to the coherent Grothendieck topology.

## Equations

## Instances For

## Equations

- instCategoryCondensed = let_fun this := inferInstance; this

@[reducible, inline]

Condensed sets (types) with the appropriate universe levels, i.e. `Type (u+1)`

-valued
sheaves on `CompHaus.{u}`

.

## Equations

- CondensedSet = Condensed (Type (u + 1))