Code

Define spectra#589

Code

Merged

ecavallo merged 15 commits intoagda:masteragda/cubical:masterfrom felixwellen:define-spectrafelixwellen/cubical:define-spectraCopy head branch name to clipboardOct 22, 2021

+151-17

Commits

Commits on Aug 11, 2021

• Introduce successor structures

  felixwellen

  committed
  f728035

  Copy full SHA for f728035

• Better use records

  felixwellen

  committed
  099ca5f

  Copy full SHA for 099ca5f

• Define prespectrum

  felixwellen

  committed
  79e8831

  Copy full SHA for 79e8831

• Fix: use pointed spaces

  felixwellen

  committed
  69f2629

  Copy full SHA for 69f2629

• Rename and fix definition of prespectrum

  felixwellen

  committed
  ea0a2b7

  Copy full SHA for ea0a2b7

• Unit as a pointed type

  felixwellen

  committed
  e42a770

  Copy full SHA for e42a770

• Refactor

  felixwellen

  committed
  6d681a9

  Copy full SHA for 6d681a9

• Add suspension prespectrum

  felixwellen

  committed
  ba0a5fb

  Copy full SHA for ba0a5fb

• Choose integers as default indices for prespectra

  felixwellen

  committed
  26042fb

  Copy full SHA for 26042fb

• Whitespace

  felixwellen

  committed
  db5aba2

  Copy full SHA for db5aba2

• Define spectrum

  felixwellen

  committed
  e435d8c

  Copy full SHA for e435d8c

• Whitespace

  felixwellen

  committed
  e6cd327

  Copy full SHA for e6cd327

• Move pointed unit type

  felixwellen

  committed
  76b7598

  Copy full SHA for 76b7598

Commits on Oct 22, 2021

• Upstream inclusion into suspension to HITs/Susp/Properties

  felixwellen

  committed
  a9aded5

  Copy full SHA for a9aded5

• Naming conventions

  felixwellen

  committed
  77bc761

  Copy full SHA for 77bc761