Investigations on graph-theoretical constructions in Homotopy type theory

{-# OPTIONS --without-K --exact-split #-}
module foundations.Type where

This documentation is generated automatically. The sub-folder in the repository of this project contains the Agda sources.

Definitions and theorems are typed with unicode characters. Lemmas and theorems are shown as rule inferences as much as possible. Level universes are explicitly given.

To be consistent with homotopy type theory, we tell Agda to not use for type-checking by using the option on the top of the files.

In addition, without the Axiom K, Agda’s is not a good name for universes in HoTT. So, we rename to . Our type judgments then will include the universe level as one explicit argument. Also, we want to have judgmental equalities for each usage of (=) so we use the following option.

open import Agda.Primitive
  using ( Level ; lsuc; lzero; _⊔_ ) public

Note that is the maximum of two hierarchy levels and and we use this later on to define types in full generality.

Type
  : (ℓ : Level)
  → Set (lsuc ℓ)

Type ℓ = Set ℓ

Type₀
  : Type (lsuc lzero)

Type₀ = Type lzero

Type₁
  : Type (lsuc (lsuc lzero))

Type₁ = Type (lsuc lzero)

The following type is to lift a type to a higher universe.

record
  ↑ {a : Level} ℓ (A : Type a)
    : Type (a ⊔ ℓ)
  where
  constructor Lift
  field
    lower : A

open ↑ public

Latest changes

(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides
(2022-07-06)(d3a4a8cf) minors by jonathan.cubides
(2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides
(2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides
(2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides
(2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides
(2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides
(2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides
(2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides
(2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides
(2021-12-15)(0630ce66) Minor fixes by jonathan.cubides
(2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides
(2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides
(2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides
(2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides