Skip to content
Find file
Fetching contributors…
Cannot retrieve contributors at this time
12 lines (8 sloc) 225 Bytes
{-# OPTIONS --without-K #-}
module Spaces.Spheres where
open import Base
open import Spaces.Suspension public
-- [Sⁿ n] is the sphere of dimension (n - 1)
Sⁿ : Set
Sⁿ O =
Sⁿ (S n) = suspension (Sⁿ n)
Something went wrong with that request. Please try again.