# Functors from categories of topological spaces to condensed sets #

This file defines the embedding of the test objects (compact Hausdorff spaces) into condensed sets.

## Main definitions #

`compHausToCondensed : CompHaus.{u} ⥤ CondensedSet.{u}`

is essentially the yoneda presheaf functor. We also define`profiniteToCondensed`

and`stoneanToCondensed`

.

TODO (Dagur):

Define the analogues of

`compHausToCondensed`

for sheaves on`Profinite`

and`Stonean`

and provide the relevant isomorphisms with`profiniteToCondensed`

and`stoneanToCondensed`

.Define the functor

`Type (u+1) ⥤ CondensedSet.{u}`

which takes a set`X`

to the presheaf given by mapping a compact Hausdorff space`S`

to`LocallyConstant S X`

, along with the isomorphism with the functor that goes through`TopCat.{u+1}`

.

Increase the size of the target category of condensed sets.

## Equations

## Instances For

## Equations

## Equations

The functor from `CompHaus`

to `Condensed.{u} (Type u)`

given by the Yoneda sheaf.

## Equations

## Instances For

The yoneda presheaf as an actual condensed set.

## Equations

## Instances For

Dot notation for the value of `compHausToCondensed`

.

## Equations

- S.toCondensed = compHausToCondensed.obj S

## Instances For

The yoneda presheaf as a condensed set, restricted to profinite spaces.

## Equations

## Instances For

Dot notation for the value of `profiniteToCondensed`

.

## Equations

- S.toCondensed = profiniteToCondensed.obj S

## Instances For

The yoneda presheaf as a condensed set, restricted to Stonean spaces.

## Equations

## Instances For

Dot notation for the value of `stoneanToCondensed`

.

## Equations

- S.toCondensed = stoneanToCondensed.obj S