CPP2022-paper.md.
Version of Sunday, January 22, 2023, 10:42 PM
Powered by agda version 2.6.2.2-442c76b and pandoc 2.14.0.3
{-# OPTIONS --without-K --exact-split #-}
module CPP2022-paper where
open import foundations.Core
open import foundations.Finite
open import foundations.Cyclic
open import lib.graph-definitions.Graph
open import lib.graph-walks.Walk
open import lib.graph-walks.Walk.isSet
open import lib.graph-walks.Walk.QuasiSimple
open WR
open import lib.graph-walks.Walk.QuasiSimpleFinite
open finiteness-lemmas
open import lib.graph-embeddings.Map
open import lib.graph-embeddings.Map.Face
open import lib.graph-embeddings.Map.Face.Walk.Homotopy
open import lib.graph-embeddings.Map.Face.Walk.Whiskering
open import lib.graph-embeddings.Map.Spherical
open import lib.graph-embeddings.Map.Spherical-is-enough
-- 2. Basics of homotopy type theory Thm-2∙1 = hedberg Def-2∙2 = isFinite Lem-2∙3 = equiv-preserves-finiteness Lem-2∙4 = decidable-→-≡-is-finite Def-2∙5 = CyclicSet -- 3. The type of graphs Def-3∙1 = Graph -- 4. Walks Def-4∙1 = Walk Lem-4∙2 = Walk-is-set Def-4∙3 = _⊰_ Lem-4∙4 = ∑∑walk-wf Thm-4∙5 = ∑∑walk-rec -- 4.3 Quasi-simple walk Def-4∙6 = ∈-walk._∈w_ Lem-4∙7 = _?∈_ Def-4∙8 = quasi-simple-walks.isQuasi Lem-4∙9 = quasi-simple-walks.being-quasi-simple-is-prop Lem-4∙10 = ⊙-quasi-simple-is-quasi-simple Lem-4∙11 = conservation Cor-4∙12a = quasi-simple-walks.one-point-walk-is-quasi-simple Cor-4∙12b = one-edge-is-quasi-simple Lem-4∙13 = ?is-quasi-simple -- 4.4 Finiteness Lem-4∙14 = equiv-fin-sigma-∈ Lem-4∙15 = ∈w-is-finite Def-4∙16 = finite-quasi-simple-walks-type Lem-4∙17 = qswalk-equiv-sigmas Lem-4∙18 = finite-qswalks Lem-4∙19 = sigma-qswalks-forms-finite-set Lem-4∙20 = qswalks-has-bounded-length Lem-4∙21 = quasi-quasi-simple-equiv-qswalk Thm-4∙22 = finite-graph-has-finite-quasi-simple-walks -- 4.5 Walk splitting Def-4∙23 = Prefix Lem-4∙24 = find-suffix Def-4∙25 = SplitAt Lem-4∙26 = split_at_ -- 4.6 Normal forms Def-4∙27-1 = Loop Def-4∙27-2 = Trivial Def-4∙27-3 = NonTrivial Def-4∙27-4 = NoReduce Def-4∙27-5 = NonTrivialLoop Def-4∙28-1 = different-endpoints-is-nontrivial Def-4∙28-2 = ∈-non-trivial Def-4∙28-3 = is-concat Def-4∙29 = _→r_ Def-4∙30 = _→r*_ Def-4∙31-1 = nf-∈ Def-4∙31-2 = length-lem→r Def-4∙32 = Reduce Def-4∙33 = Normal Lem-4∙34 = Normal-is-prop Ex-4∙35 = No-reduce-is-normal Def-4∙36 = Progress Thm-4∙37 = normalize Cor-4∙38-1 = ?reduce Cor-4∙38-2 = ?normal Cor-4∙38-3 = progress -- 5. The notion of walk homotopy Def-5∙1 = Map Rem-4 = Face -- 5.1. Homotopy of walks Def-5∙2 = HomotopyWalks._∼hwalk_ Lem-5∙3-1 = Whiskering.whiskerR Lem-5∙3-2 = Whiskering.whiskerL Lem-5∙3-3 = Whiskering.whisker-h -- 5.2 Homotopy walks in the sphere Def-5∙4 = isSphericalMap Def-5∙5 = isSphericalMap' Lem-5∙6 = hom-normalisation.e⊙∼ Thm-5∙7 = hom-normalisation.hom-normalize Cor-5∙8 = spherical-equiv
(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