# Mere spheres

Content created by Egbert Rijke.

Created on 2023-10-17.

module synthetic-homotopy-theory.mere-spheres where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.mere-equivalences
open import foundation.propositions
open import foundation.universe-levels

open import synthetic-homotopy-theory.spheres


## Idea

A mere n-sphere is a type X that is merely equivalent to the n-sphere.

## Definitions

### The predicate of being a mere n-sphere

module _
{l : Level} (n : ℕ) (X : UU l)
where

is-mere-sphere-Prop : Prop l
is-mere-sphere-Prop = mere-equiv-Prop (sphere n) X

is-mere-sphere : UU l
is-mere-sphere = type-Prop is-mere-sphere-Prop

is-prop-is-mere-sphere : is-prop is-mere-sphere
is-prop-is-mere-sphere = is-prop-type-Prop is-mere-sphere-Prop


### Mere spheres

mere-sphere : (l : Level) (n : ℕ) → UU (lsuc l)
mere-sphere l n = Σ (UU l) (is-mere-sphere n)

module _
{l : Level} (n : ℕ) (X : mere-sphere l n)
where

type-mere-sphere : UU l
type-mere-sphere = pr1 X

mere-equiv-mere-sphere : mere-equiv (sphere n) type-mere-sphere
mere-equiv-mere-sphere = pr2 X