Jason (jcreed) wrote,

Aha, I figured out a super short definition of S∞ and proof of its contractibility during breakfast:

{-# OPTIONS --without-K #-}

open import Base
import Spaces.Suspension

module Spaces.SInf where

data S∞ : Set where
   # : Spaces.Suspension.suspension S∞ → S∞

open Spaces.Suspension S∞

reach-north : (y : S∞) → y ≡ # north
reach-north (# y) = ! (ap # (suspension-rec (λ x → north ≡ x) refl (paths (# north))
                      (λ x → trans-cst≡id (paths x) refl ∘ (ap paths (reach-north x))) y))

S∞-is-contr : is-contr S∞
S∞-is-contr = # north , reach-north


Oh, hm, it has a termination violation, because agda can't tell that things decrease, even though I know they do. Bummer.
Tags: hott, math

  • (no subject)

    Lunch at the goog with wjl, also ran into cgarrod and kelli and tomczak and gopi and agoode. Attended sigbovik, was traditional and glonous and…

  • (no subject)

    The eighth sigbovik sigbovicked successfully. A few really funny talks, some farther on the meh end of the spectrum, as is not uncommon. I really…

  • (no subject)

    Sigbovik happened! It was a good and fine sigbovik. I am mostly impressed that it has simply continued to happen for 7 consecutive years.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded