Investigations on graph-theoretical constructions in Homotopy type theory

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

  -- ∙ Types very often used
  open import foundations.Type public
  open import foundations.BasicTypes public
  open import foundations.HLevelTypes public

  open import foundations.BasicFunctions public
  open import foundations.AlgebraOnPaths public
  open import foundations.Transport public
  open import foundations.TransportLemmas public
  open import foundations.AlgebraOnDependentPaths public

  open import foundations.ProductIdentities public
  open import foundations.CoproductIdentities public

  open import foundations.FibreType public
  open import foundations.EquivalenceType public
  open import foundations.EquivalenceReasoning public
  open import foundations.DependentAlgebra public

  open import foundations.ProductIdentities
  open import foundations.CoproductIdentities

  open import foundations.HomotopyType public
  open import foundations.HomotopyLemmas public

  open import foundations.FunExtAxiom
  open import foundations.FunExtTransport public
  open import foundations.FunExtTransportDependent public

  open import foundations.DecidableEquality public

  open import foundations.HalfAdjointType public

  open import foundations.QuasiinverseType public
  open import foundations.QuasiinverseLemmas public

  open import foundations.TruncationType public

  -- · Extra useful lemmas
  open import foundations.HLevelLemmas public
  open import foundations.HedbergLemmas public

  -- ∙ Equivalences
  open import foundations.BasicEquivalences public
  open import foundations.SigmaEquivalence public
  open import foundations.SigmaPreserves public
  open import foundations.PiPreserves 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