From 183ec1009fa9aa510b218009c1b4d88bc63a5beb Mon Sep 17 00:00:00 2001 From: fizruk Date: Wed, 13 Dec 2023 23:25:37 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20rzk-lang?= =?UTF-8?q?/hottbook@463d91e5b4ae7b8922cca1dd592fa5315afb924e=20?= =?UTF-8?q?=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../01-section.rzk/index.html | 66 +- .../02-section.rzk/index.html | 66 +- .../exercises/0.1-solution.rzk/index.html | 66 +- .../exercises/0.2-solution.rzk/index.html | 66 +- .../0-chapter-template/exercises/index.html | 66 +- .../index.html | 66 +- .../05-product-types.rzk/index.html | 66 +- .../06-dependent-pair-types.rzk/index.html | 66 +- .../07-coproduct-types.rzk/index.html | 66 +- .../1-type-theory/08-booleans.rzk/index.html | 66 +- .../09-natural-numbers.rzk/index.html | 66 +- .../index.html | 66 +- .../11-propositions-as-types.rzk/index.html | 66 +- .../12-identity-types.rzk/index.html | 66 +- .../exercises/1.1-solution.rzk/index.html | 66 +- .../exercises/1.10-solution.rzk/index.html | 66 +- .../exercises/1.11-solution.rzk/index.html | 66 +- .../exercises/1.12-solution.rzk/index.html | 66 +- .../exercises/1.13-solution.rzk/index.html | 66 +- .../exercises/1.14-solution.rzk/index.html | 66 +- .../exercises/1.15-solution.rzk/index.html | 66 +- .../exercises/1.16-solution.rzk/index.html | 66 +- .../exercises/1.2-solution.rzk/index.html | 66 +- .../exercises/1.3-solution.rzk/index.html | 66 +- .../exercises/1.4-solution.rzk/index.html | 66 +- .../exercises/1.5-solution.rzk/index.html | 66 +- .../exercises/1.6-solution.rzk/index.html | 66 +- .../exercises/1.7-solution.rzk/index.html | 66 +- .../exercises/1.8-solution.rzk/index.html | 66 +- .../exercises/1.9-solution.rzk/index.html | 66 +- .../1-type-theory/exercises/index.html | 66 +- .../index.html | 108 +- .../02-functions-are-functors.rzk/index.html | 66 +- .../index.html | 72 +- .../index.html | 1998 +++++++++++++++++ .../index.html | 72 +- .../06-cartesian-product-types.rzk/index.html | 167 +- .../07-sigma-types.rzk/index.html | 66 +- .../08-the-unit-type.rzk/index.html | 89 +- .../index.html | 98 +- .../index.html | 66 +- .../11-identity-type.rzk/index.html | 66 +- .../12-coproducts.rzk/index.html | 66 +- .../13-natural-numbers.rzk/index.html | 66 +- .../index.html | 66 +- .../15-universal-properties.rzk/index.html | 66 +- .../exercises/2.1-solution.rzk/index.html | 66 +- .../exercises/2.10-solution.rzk/index.html | 66 +- .../exercises/2.11-solution.rzk/index.html | 66 +- .../exercises/2.12-solution.rzk/index.html | 66 +- .../exercises/2.13-solution.rzk/index.html | 66 +- .../exercises/2.14-solution.rzk/index.html | 66 +- .../exercises/2.15-solution.rzk/index.html | 66 +- .../exercises/2.16-solution.rzk/index.html | 66 +- .../exercises/2.17-solution.rzk/index.html | 66 +- .../exercises/2.18-solution.rzk/index.html | 66 +- .../exercises/2.2-solution.rzk/index.html | 66 +- .../exercises/2.3-solution.rzk/index.html | 66 +- .../exercises/2.4-solution.rzk/index.html | 66 +- .../exercises/2.5-solution.rzk/index.html | 66 +- .../exercises/2.6-solution.rzk/index.html | 66 +- .../exercises/2.7-solution.rzk/index.html | 66 +- .../exercises/2.8-solution.rzk/index.html | 66 +- .../exercises/2.9-solution.rzk/index.html | 66 +- .../exercises/index.html | 84 +- .../01-sets-and-n-types.rzk/index.html | 1359 +++++++++++ .../index.html | 176 +- .../03-mere-propositions.rzk/index.html | 1105 +++++++++ .../11-contractibility.rzk/index.html | 1090 +++++++++ 404.html | 66 +- index.html | 66 +- search/search_index.json | 2 +- sitemap.xml.gz | Bin 127 -> 127 bytes 73 files changed, 10090 insertions(+), 224 deletions(-) create mode 100644 1-foundations/2-homotopy-type-theory/04-homotopies-and-equivalences.rzk/index.html create mode 100644 1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk/index.html rename 1-foundations/{2-homotopy-type-theory/04-homotopies-are-equivalences.rzk => 3-sets-and-logic/02-propositions-as-types.rzk copy}/index.html (86%) create mode 100644 1-foundations/3-sets-and-logic/03-mere-propositions.rzk/index.html create mode 100644 1-foundations/3-sets-and-logic/11-contractibility.rzk/index.html diff --git a/1-foundations/0-chapter-template/01-section.rzk/index.html b/1-foundations/0-chapter-template/01-section.rzk/index.html index 4810698..e5c3ac2 100644 --- a/1-foundations/0-chapter-template/01-section.rzk/index.html +++ b/1-foundations/0-chapter-template/01-section.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/0-chapter-template/02-section.rzk/index.html b/1-foundations/0-chapter-template/02-section.rzk/index.html index d7250a9..2d41b6f 100644 --- a/1-foundations/0-chapter-template/02-section.rzk/index.html +++ b/1-foundations/0-chapter-template/02-section.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/0-chapter-template/exercises/0.1-solution.rzk/index.html b/1-foundations/0-chapter-template/exercises/0.1-solution.rzk/index.html index acd0ecf..5e2e61d 100644 --- a/1-foundations/0-chapter-template/exercises/0.1-solution.rzk/index.html +++ b/1-foundations/0-chapter-template/exercises/0.1-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/0-chapter-template/exercises/0.2-solution.rzk/index.html b/1-foundations/0-chapter-template/exercises/0.2-solution.rzk/index.html index 8aa79ac..72832ba 100644 --- a/1-foundations/0-chapter-template/exercises/0.2-solution.rzk/index.html +++ b/1-foundations/0-chapter-template/exercises/0.2-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/0-chapter-template/exercises/index.html b/1-foundations/0-chapter-template/exercises/index.html index d1584fe..875eba6 100644 --- a/1-foundations/0-chapter-template/exercises/index.html +++ b/1-foundations/0-chapter-template/exercises/index.html @@ -630,11 +630,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -892,6 +892,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/04-dependent-function-types.rzk/index.html b/1-foundations/1-type-theory/04-dependent-function-types.rzk/index.html index f3aedbd..20b9c29 100644 --- a/1-foundations/1-type-theory/04-dependent-function-types.rzk/index.html +++ b/1-foundations/1-type-theory/04-dependent-function-types.rzk/index.html @@ -653,11 +653,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/05-product-types.rzk/index.html b/1-foundations/1-type-theory/05-product-types.rzk/index.html index 117aa62..9b235d7 100644 --- a/1-foundations/1-type-theory/05-product-types.rzk/index.html +++ b/1-foundations/1-type-theory/05-product-types.rzk/index.html @@ -690,11 +690,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -952,6 +952,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/06-dependent-pair-types.rzk/index.html b/1-foundations/1-type-theory/06-dependent-pair-types.rzk/index.html index 9a3bf7c..e57066f 100644 --- a/1-foundations/1-type-theory/06-dependent-pair-types.rzk/index.html +++ b/1-foundations/1-type-theory/06-dependent-pair-types.rzk/index.html @@ -653,11 +653,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/07-coproduct-types.rzk/index.html b/1-foundations/1-type-theory/07-coproduct-types.rzk/index.html index 6dd7a9d..a9ac17a 100644 --- a/1-foundations/1-type-theory/07-coproduct-types.rzk/index.html +++ b/1-foundations/1-type-theory/07-coproduct-types.rzk/index.html @@ -653,11 +653,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/08-booleans.rzk/index.html b/1-foundations/1-type-theory/08-booleans.rzk/index.html index a2d22dc..9a4dc94 100644 --- a/1-foundations/1-type-theory/08-booleans.rzk/index.html +++ b/1-foundations/1-type-theory/08-booleans.rzk/index.html @@ -653,11 +653,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/09-natural-numbers.rzk/index.html b/1-foundations/1-type-theory/09-natural-numbers.rzk/index.html index 1eeae67..3895070 100644 --- a/1-foundations/1-type-theory/09-natural-numbers.rzk/index.html +++ b/1-foundations/1-type-theory/09-natural-numbers.rzk/index.html @@ -653,11 +653,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/10-pattern-matching-and-recursion.rzk/index.html b/1-foundations/1-type-theory/10-pattern-matching-and-recursion.rzk/index.html index fdcb2da..8094538 100644 --- a/1-foundations/1-type-theory/10-pattern-matching-and-recursion.rzk/index.html +++ b/1-foundations/1-type-theory/10-pattern-matching-and-recursion.rzk/index.html @@ -653,11 +653,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/11-propositions-as-types.rzk/index.html b/1-foundations/1-type-theory/11-propositions-as-types.rzk/index.html index 32a532c..b0c08a9 100644 --- a/1-foundations/1-type-theory/11-propositions-as-types.rzk/index.html +++ b/1-foundations/1-type-theory/11-propositions-as-types.rzk/index.html @@ -653,11 +653,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/12-identity-types.rzk/index.html b/1-foundations/1-type-theory/12-identity-types.rzk/index.html index ac68389..d04f9fa 100644 --- a/1-foundations/1-type-theory/12-identity-types.rzk/index.html +++ b/1-foundations/1-type-theory/12-identity-types.rzk/index.html @@ -653,11 +653,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.1-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.1-solution.rzk/index.html index 8dec5f3..0c158c6 100644 --- a/1-foundations/1-type-theory/exercises/1.1-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.1-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.10-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.10-solution.rzk/index.html index 2fbbc3c..a57cf86 100644 --- a/1-foundations/1-type-theory/exercises/1.10-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.10-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.11-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.11-solution.rzk/index.html index 7149c02..aa7a140 100644 --- a/1-foundations/1-type-theory/exercises/1.11-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.11-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.12-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.12-solution.rzk/index.html index 7d35ba5..21b94c0 100644 --- a/1-foundations/1-type-theory/exercises/1.12-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.12-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.13-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.13-solution.rzk/index.html index dfc5a5b..cdb0c03 100644 --- a/1-foundations/1-type-theory/exercises/1.13-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.13-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.14-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.14-solution.rzk/index.html index 9d5754c..032e19e 100644 --- a/1-foundations/1-type-theory/exercises/1.14-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.14-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.15-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.15-solution.rzk/index.html index ba8abb6..794b702 100644 --- a/1-foundations/1-type-theory/exercises/1.15-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.15-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.16-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.16-solution.rzk/index.html index 6bf8691..387c2b9 100644 --- a/1-foundations/1-type-theory/exercises/1.16-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.16-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.2-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.2-solution.rzk/index.html index 6ebf05c..79ae81e 100644 --- a/1-foundations/1-type-theory/exercises/1.2-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.2-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.3-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.3-solution.rzk/index.html index 722fbf0..2b6054e 100644 --- a/1-foundations/1-type-theory/exercises/1.3-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.3-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.4-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.4-solution.rzk/index.html index 4030aa3..5235530 100644 --- a/1-foundations/1-type-theory/exercises/1.4-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.4-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.5-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.5-solution.rzk/index.html index 835be93..8e22b80 100644 --- a/1-foundations/1-type-theory/exercises/1.5-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.5-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.6-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.6-solution.rzk/index.html index 90de8a4..b94ce0e 100644 --- a/1-foundations/1-type-theory/exercises/1.6-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.6-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.7-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.7-solution.rzk/index.html index 1056e98..a826a77 100644 --- a/1-foundations/1-type-theory/exercises/1.7-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.7-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.8-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.8-solution.rzk/index.html index ca21258..d4b31bf 100644 --- a/1-foundations/1-type-theory/exercises/1.8-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.8-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/1.9-solution.rzk/index.html b/1-foundations/1-type-theory/exercises/1.9-solution.rzk/index.html index 099a19b..fe1bc02 100644 --- a/1-foundations/1-type-theory/exercises/1.9-solution.rzk/index.html +++ b/1-foundations/1-type-theory/exercises/1.9-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/1-type-theory/exercises/index.html b/1-foundations/1-type-theory/exercises/index.html index 8a3635c..a5563fe 100644 --- a/1-foundations/1-type-theory/exercises/index.html +++ b/1-foundations/1-type-theory/exercises/index.html @@ -795,11 +795,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -1057,6 +1057,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/01-types-are-higher-groupoids.rzk/index.html b/1-foundations/2-homotopy-type-theory/01-types-are-higher-groupoids.rzk/index.html index c92ea2a..b6d8008 100644 --- a/1-foundations/2-homotopy-type-theory/01-types-are-higher-groupoids.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/01-types-are-higher-groupoids.rzk/index.html @@ -681,6 +681,13 @@ + + +
  • + + Related statements used in further proofs: + +
    • @@ -738,11 +745,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -1000,6 +1007,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + @@ -1086,6 +1155,13 @@ + + +
  • + + Related statements used in further proofs: + +
    • @@ -1243,6 +1319,34 @@

    Associativity of concatenation ( \ x' z' q' w' r' → refl) x y p) z q w r +

    +
    +

    Concatencation of three paths

    +
    +
    #def 3-path-concat
+  ( A : U)
+  ( x y z w : A)
+  : ( x = y) → (y = z) → (z = w) → (x = w)
+  := \ p q r → path-concat A x z w (path-concat A x y z p q) r
+
    +
    +

    Associativity symmetrical to 2.1.4-4

    +
    \[(p \cdot q) \cdot r = p \cdot (q \cdot r)\]
    +
    +
    #def concat-assoc-2
+  ( A : U)
+  ( x y z w : A)
+  ( p : x = y)
+  ( q : y = z)
+  ( r : z = w)
+  : path-concat A x z w (path-concat A x y z p q) r
+    = path-concat A x y w p (path-concat A y z w q r)
+  := path-sym
+      ( x = w)
+      ( path-concat A x y w p (path-concat A y z w q r))
+      ( path-concat A x z w (path-concat A x y z p q) r)
+      ( concat-assoc A x y z w p q r)
+
    diff --git a/1-foundations/2-homotopy-type-theory/02-functions-are-functors.rzk/index.html b/1-foundations/2-homotopy-type-theory/02-functions-are-functors.rzk/index.html index f556cba..0c359ae 100644 --- a/1-foundations/2-homotopy-type-theory/02-functions-are-functors.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/02-functions-are-functors.rzk/index.html @@ -731,11 +731,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -993,6 +993,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/03-type-families-are-fibrations.rzk/index.html b/1-foundations/2-homotopy-type-theory/03-type-families-are-fibrations.rzk/index.html index b4d1022..bf383fa 100644 --- a/1-foundations/2-homotopy-type-theory/03-type-families-are-fibrations.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/03-type-families-are-fibrations.rzk/index.html @@ -12,7 +12,7 @@ - + @@ -704,11 +704,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -966,6 +966,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + @@ -1292,13 +1354,13 @@

    Properties of transport
    + Skip to content + + +
    +
    + +
    + + + + + + +
    + + +
    + +
    + + + + + + +
    +
    + + + +
    +
    +
    + + + + + +
    +
    +
    + + + +
    +
    +
    + + + +
    +
    +
    + + + +
    +
    + + + + + + + + + + + + +

    2.4 Homotopies and equivalences

    +

    This is a literate Rzk file:

    +
    #lang rzk-1
+
    +

    Homotopies between functions

    +
    +

    Definition 2.4.1.

    +

    Let \(f, g : \prod_{(x:A)} P(x)\) be two sections of a type family \(P : A \to U\). +A homotopy from \(f\) to \(g\) is a dependent function of type

    +
    \[(f \sim g) :\equiv \prod_{(x:A)} (f(x) = g(x)).\]
    +
    +
    #def homotopy
+  ( A : U)
+  ( P : A → U)
+  ( f g : (x : A) → P x)
+  : U
+  := (x : A) → f x = g x
+
    +

    Homotopies are equivalence relations

    +
    +

    Lemma 2.4.2.

    +

    Homotopy is an equivalence relation on each dependent function type \(\prod_{(x:A)} P(x)\). +That is, we have elements of the types

    +
    \[\prod_{f : \prod_{(x:A)} P(x)} (f \sim f)\]
    +
    \[\prod_{f, g : \prod_{(x:A)} P(x)} (f \sim g) \to (g \sim f)\]
    +
    \[\prod_{f, g, h : \prod_{(x:A)} P(x)} (f \sim g) \to (g \sim h) \to (f \sim h)\]
    +
    +

    Reflexivity

    +
    #def homotopy-refl
+  ( A : U)
+  ( P : A → U)
+  ( f : (x : A) → P x)
+  : homotopy A P f f
+  := \ x → refl
+
    +

    Symmetry

    +
    #def homotopy-sym
+  ( A : U)
+  ( P : A → U)
+  ( f g : (x : A) → P x)
+  : homotopy A P f g → homotopy A P g f
+  :=
+  \ hom x →
+    path-sym (P x) (f x) (g x) (hom x)
+
    +

    Transitivity

    +
    #def homotopy-trans
+    ( A : U)
+    ( P : A → U)
+    ( f g h : (x : A) → P x)
+  : homotopy A P f g
+  → homotopy A P g h
+  → homotopy A P f h
+  :=
+  \ hom-fg hom-gh x →
+    path-concat (P x) (f x) (g x) (h x) (hom-fg x) (hom-gh x)
+
    +

    Naturality

    +
    +

    Lemma 2.4.3.

    +

    Suppose \(H : f \sim g\) is a homotopy between functions \(f, g: A \to B\) and let \(p : x =_A y\). Then we have

    +
    \[H(x) \cdot g(p) = f(p) \cdot H(y).\]
    +
    +
    +

    Tip

    +

    When dealing with paths, authors write \(f(p)\) to mean \(ap_f(p)\).

    +
    +
    #def hom-naturality
+  ( A B : U)
+  ( f g : A → B)
+  ( H : homotopy A (\ _ → B) f g)
+  : ( x : A)
+  → ( y : A)
+  → ( p : x = y)
+  → path-concat B (f x) (g x) (g y) (H x) (ap A B g x y p)
+  = path-concat B (f x) (f y) (g y) (ap A B f x y p) (H y)
+  :=
+  path-ind A
+  ( \ x' y' p' →
+      path-concat B (f x') (g x') (g y') (H x') (ap A B g x' y' p')
+    = path-concat B (f x') (f y') (g y') (ap A B f x' y' p') (H y'))
+  ( \ x' → path-sym -- H x' ∙ refl = H x'
+            ( f x' = g x')
+            ( H x')
+            ( path-concat B (f x') (g x') (g x') (H x') refl)
+            ( concat-refl B (f x') (g x') (H x')) -- H x' = H x' ∙ refl
+        )
+
    +
    +

    Corollary 2.4.4.

    +

    Let \(H : f \sim id_A\) be a homotopy, with \(f : A \to A\). Then, for any \(x : A\) we have

    +
    \[H(f(x)) = f(H(x)).\]
    +

    Here \(f(x)\) denotes the ordinary application of \(f\) to \(x\), while \(f(H(x))\) denotes \(ap_f(H(x))\).

    +
    +

    Proof homotopy-id-swap is given in the end of the file.

    +

    Quasi-Inverses

    +

    The traditional notion of isomorphism is poorly behaved for proof-relevant mathematics. Thus, it is given the name of quasi-inverse.

    +
    +

    Definition 2.4.6.

    +

    For a function \(f : A → B\), +a quasi-inverse of \(f\) is a triple \((g, \alpha, \beta)\) consisting of +a function \(g : B → A\) +and homotopies \(\alpha : f \circ g \sim id_B\) +and \(\beta : g \circ f \sim id_A\).

    +
    +
    #def qinv
+  ( A B : U)
+  ( f : A → B)
+  : U
+  :=
+  Σ ( g : B → A)
+  , prod
+    ( homotopy B (\ _ → B) (compose B A B f g) (id B))
+    ( homotopy A (\ _ → A) (compose A B A g f) (id A))
+
    +

    Examples

    +
    +

    Example 2.4.7. Identity quasi-inverse

    +

    The identity function \(id_A : A \to A\) has a quasi-inverse given by \(id_A\) itself, +together with homotopies defined by \(\alpha(y) :\equiv \mathsf{refl}_y\) and \(\beta(x) :\equiv \mathsf{refl}_x\).

    +
    +
    #def qinv-id
+  ( A : U)
+  : qinv A A (id A)
+  :=
+  ( id A
+  , ( \ y → refl_{y}
+    , \ x → refl_{x}))
+
    +
    +

    Example 2.4.8. Quasi-inverse for path concatenation

    +

    For any \(p : x =_A y\) and \(z : A\), +the functions \((p \cdot –) : (y =_A z) \to (x =_A z)\) +and \((– \cdot p) : (z =_A x) \to (z =_A y)\) +have quasi-inverses given by \((p^{−1} \cdot –)\) and \((– \cdot p^{−1})\), respectively.

    +
    +

    Quasi-inverse has a quasi-inverse

    +
    #define inverse-from-qinv
+  ( A B : U)
+  ( f : A → B)
+  : qinv A B f → (B → A)
+  := \ (g , _) → g
+
+#define qinv-inverse-from-qinv
+  ( A B : U)
+  ( f : A → B)
+  : ( qinv-f : qinv A B f)
+  → qinv B A (inverse-from-qinv A B f qinv-f)
+  := \ (g , (α , β)) → (f , (β , α))
+
    +

    Quasi-inverse of the concatenation from the right side

    +
    +

    Change of variables in the code

    +

    Note the change of variables: \(p \mapsto q, x \mapsto y, y \mapsto z, z \mapsto x\). That is, the code corrsesponds to the statement that for any \(q : y =_A z\) and \(x : A\), the function \((– \cdot q) : (x =_A y) \to (x =_A z)\) have quasi-inverse given by \((– \cdot q^{−1})\), respectively.

    +
    +
    Definition of right concatenation as a function, and its inverse
    #def right-concat
+  ( A : U)
+  ( x y z : A)
+  ( q : y = z)
+  : ( x = y) → (x = z)
+  := \ p → path-concat A x y z p q
+
+#def right-concat-inv
+  ( A : U)
+  ( x y z : A)
+  ( q : y = z)
+  : ( x = z) → (x = y)
+  := right-concat A x z y (path-sym A y z q)
+
    +
    Proofs that both compositions are homotopical to identity
    #def right-concat-right-inv-remove-refl
+  ( A : U)
+  ( x y z : A)
+  ( p : x = y)
+  : ( q : y = z)
+  → right-concat-inv A x y z q (right-concat A x y z q p) -- (p ∙ q) ∙ q⁻¹
+  = p
+  :=
+  path-ind A
+  ( \ x' y' p' →
+      ( q : y' = z) → right-concat-inv A x' y' z q (right-concat A x' y' z q p') = p')
+  ( \ x' → inverse-r A x' z)
+  ( x)
+  ( y)
+  ( p)
+
+#def right-concat-left-inv-remove-refl
+  ( A : U)
+  ( x y z : A)
+  ( r : x = z)
+  : ( q : y = z)
+  → right-concat A x y z q (right-concat-inv A x y z q r) -- (r ∙ q⁻¹) ∙ q
+  = r
+  :=
+  path-ind A
+  ( \ x' z' r' →
+      ( q : y = z') → right-concat A x' y z' q (right-concat-inv A x' y z' q r') = r')
+  ( \ x' → inverse-l A y x')
+  ( x)
+  ( z)
+  ( r)
+
    +
    Proof for quasi-inverse of right concatenation
    #def right-concat-inv-is-qinv-for-right-concat
+  ( A : U)
+  ( x y z : A)
+  ( q : y = z)
+  : qinv (x = y) (x = z) (right-concat A x y z q)
+  :=
+  ( right-concat-inv A x y z q
+  , ( \ (r : x = z) → right-concat-left-inv-remove-refl  A x y z r q
+    , \ (p : x = y) → right-concat-right-inv-remove-refl A x y z p q))
+
    +

    Equivalences

    +

    An improved notion, isequiv, has the following properties:

    +
      +
    1. For each \(f : A \to B\) there is a function \(\mathsf{qinv}(f) \to \mathsf{isequiv}(f)\)
      2. +
    2. Similarly, for each \(f\) we have \(\mathsf{isequiv}(f) \to \mathsf{qinv}(f)\); thus the two are logically equivalent.
      3. +
    3. For any two inhabitants \(e_1, e_2 : \mathsf{isequiv}(f)\), we have \(e_1 = e_2\).
      4. +
    +

    One of numerous, but equivalent ways to define isequiv:

    +
    +

    Definition 2.4.10.

    +
    \[\mathsf{isequiv}(f) :\equiv \left(\sum_{(g:B \to A)} (f \circ g \sim id_B)\right) \times \left(\sum_{(h:B \to A)} (h \circ f \sim id_A)\right).\]
    +
    +
    #def isequiv
+  ( A B : U)
+  ( f : A → B)
+  : U
+  :=
+  prod
+  ( Σ ( g : B → A) , homotopy B (\ _ → B) (compose B A B f g) (id B))
+  ( Σ ( h : B → A) , homotopy A (\ _ → A) (compose A B A h f) (id A))
+
    +

    Proof of Property 1

    +

    For the \(\mathsf{qinv}(f) \to \mathsf{isequiv}(f)\) direction, \(g\) can play the role of both \(g\) and \(h\), i.e. we take \((g, \alpha, \beta)\) to \((g, \alpha, g, \beta)\).

    +
    #def qinv-to-isequiv
+  ( A B : U)
+  ( f : A → B)
+  : qinv A B f → isequiv A B f
+  := \ (g , (α , β)) → ((g , α) , (g , β))
+
    +

    Proof of Property 2

    +

    For the other direction, we are given \((g, \alpha, h, \beta)\). Notice that \(h \circ f \circ g \sim_{\alpha} h\) and \(h \circ f \circ g \sim_{\beta} g\). Let \(\gamma\) be the composite homotopy

    +
    $$g \sim_{\beta^{-1}} h \circ f \circ g \sim_{\alpha} h,$$
+
+meaning $\gamma(x) :\equiv \beta(g(x))^{-1} \cdot h(\alpha(x))$. Now define $\beta'(x) :\equiv \gamma(f(x)) \cdot \beta(x)$. Then $(g, \alpha, \beta) : \mathsf{qinv}(f)'$.
+
    +
    #def isequiv-to-qinv
+  ( A B : U)
+  ( f : A → B)
+  : isequiv A B f → qinv A B f
+  :=
+  \ ((g , α) , (h , β)) →
+    ( g
+      , ( α
+        , \ x →
+            -- g (f x) = h (f (g (f x))) = h (f x) = x
+            path-concat A -- g (f x) = id x
+            ( compose A B A g f x)
+            ( compose A B A h f x)
+            ( id A x)
+            ( path-concat A -- g (f x) = h (f x)
+              ( g (f x))
+              ( h (f (g (f x))))
+              ( h (f x))
+              ( path-sym A -- g (f x) = (h . f . g) (f x)
+                ( compose A B A h f (g (f x)))
+                ( id A (g (f x)))
+                ( β (g (f x))))
+              ( ap B A h -- (h . f . g) (f x) = h (f x)
+                ( compose B A B f g (f x))
+                ( id B (f x))
+                ( α (f x))))
+            ( β x))) -- h (f x) = id x
+
    +

    Proof of Property 3

    +

    Proof of the third property requires identifying the identity types of cartesian products and dependent pair types, +which are discussed in Sections 2.6 and 2.7.

    +

    Equivalence of types

    +
    +

    Definition 2.4.11.

    +

    An equivalence from type \(A\) to type \(B\) is defined to be a function \(f : A \to B\) together with an inhabitant of \(\mathsf{isequiv}(f)\).

    +
    \[(A \simeq B) :\equiv \sum_{(f:A \to B)} \mathsf{isequiv}(f).\]
    +
    +
    +

    Note

    +

    If we have a function \(f : A \to B\) and we know that \(e : \mathsf{isequiv}(f)\), we may write \(f : A \simeq B\), rather than \((f, e)\).

    +
    +
    #def equivalence
+  ( A B : U)
+  : U
+  := Σ (f : A → B) , isequiv A B f
+
    +

    Type equivalences are equivalence relations

    +
    +

    Lemma 2.4.12.

    +

    Type equivalence is an equivalence relation on \(U\). More specifically:

    +
      +
    1. For any \(A\), the identity function \(id_A\) is an equivalence; hence \(A \simeq A\).
      2. +
    2. For any \(f : A \simeq B\), we have an equivalence \(f^{-1} : B \simeq A\).
      3. +
    3. For any \(f : A \simeq B\) and \(g : B \simeq C\), we have \(g \circ f : A \simeq C\).
      4. +
    +
    +

    Reflexivity

    +
    #def equivalence-refl
+  ( A : U)
+  : equivalence A A
+  :=
+  ( id A
+  , ( ( id A , \ x → refl)
+    , ( id A , \ x → refl)))
+
    +

    Symmetry

    +
    #def inverse-from-isequiv
+  ( A B : U)
+  ( f : A → B)
+  : isequiv A B f → (B → A)
+  :=
+  \ isequiv-f →
+    inverse-from-qinv A B f
+    ( isequiv-to-qinv A B f isequiv-f)
+
+#def inverse-from-equivalence
+  ( A B : U)
+  : equivalence A B → (B → A)
+  :=
+  \ (f , isequiv-f) →
+    inverse-from-isequiv A B f isequiv-f
+
+#def isequiv-inverse-from-equivalence
+  ( A B : U)
+  : ( f : equivalence A B)
+  → isequiv B A (inverse-from-equivalence A B f)
+  :=
+  \ (f , isequiv-f) →
+    qinv-to-isequiv B A
+    ( inverse-from-equivalence A B (f , isequiv-f))
+    ( qinv-inverse-from-qinv A B f (isequiv-to-qinv A B f isequiv-f))
+
+#def equivalence-sym
+  ( A B : U)
+  : equivalence A B → equivalence B A
+  :=
+  \ f →
+    ( inverse-from-equivalence A B f
+    , isequiv-inverse-from-equivalence A B f)
+
    +

    Transitivity

    +
    #define qinv-trans
+  ( A B C : U)
+  ( f : A → B)
+  ( g : B → C)
+  : qinv A B f → qinv B C g → qinv A C (compose A B C g f)
+  :=
+  \ (f⁻¹ , (α-f , β-f)) (g⁻¹ , (α-g , β-g)) →
+    ( compose C B A f⁻¹ g⁻¹
+    , ( \ c →
+          path-concat C
+          ( g (f (f⁻¹ (g⁻¹ c))))
+          ( g (g⁻¹ c))
+          ( c)
+          ( ap B C g
+            ( f (f⁻¹ (g⁻¹ c)))
+            ( g⁻¹ c)
+            ( α-f (g⁻¹ c)))
+          ( α-g c)
+      , \ a →
+          path-concat A
+          ( f⁻¹ (g⁻¹ (g (f a))))
+          ( f⁻¹ (f a))
+          ( a)
+          ( ap B A f⁻¹
+            ( g⁻¹ (g (f a)))
+            ( f a)
+            ( β-g (f a)))
+          ( β-f a)))
+
+#define equivalence-trans
+  ( A B C : U)
+  : equivalence A B
+  → equivalence B C
+  → equivalence A C
+  :=
+  \ (f , isequiv-f) (g , isequiv-g) →
+    ( compose A B C g f
+    , qinv-to-isequiv A C
+      ( compose A B C g f)
+      ( qinv-trans A B C f g
+        ( isequiv-to-qinv A B f isequiv-f)
+        ( isequiv-to-qinv B C g isequiv-g)))
+
    +

    Proof of Corollary 2.4.4

    +
    Proof for corollary 2.4.4. Homotopy with id
    lemma 2.4.3 :  H(x) • g  (p)   = f (p)   • H y
+
+Substitutions:
+x → f x
+y → x
+g → id
+p → H x
+
+Result of application of lemma with the corresponding values:
+H(f x) • id (H x) = f (H x) • H x
+
+
+By right-concatenating (H x)⁻¹ to the both sides, we have
+H(f x) = H(f x) • id (H x) • (H x)⁻¹ = f (H x) • H x • (H x)⁻¹ = f (H x)
+
    +
    #def homotopy-id-swap
+  ( A : U)
+  ( f : A → A)
+  ( H : homotopy A (\ _ → A) f (id A))
+  ( x : A)
+  : H (f x) = ap A A f (f x) (id A x) (H x)
+  :=
+  3-path-concat
+  ( f (f x) = (f x)) -- type of points
+  -- 1st point: H (f x)
+  ( H (f x))
+  -- 2nd point: (H (f x) • (H x)) • (H x)⁻¹
+  ( path-concat A (f (f x)) x (f x)
+    ( path-concat A (f (f x)) (f x) x
+      ( H (f x))
+      ( H x))
+    ( path-sym A (f x) x
+      ( H x)))
+  -- 3rd point:  (f (H x) • (H x)) • (H x)⁻¹
+  ( path-concat A (f (f x)) x (f x)
+    ( path-concat A (f (f x)) (f x) x
+      ( ap A A f (f x) x (H x))
+      ( H x))
+    ( path-sym A (f x) x
+      ( H x)))
+  -- 4th point: f (H x)
+  ( ap A A f (f x) x (H x))
+
+  -- proof that H (f x) = (H (f x) • H x) • (H x)⁻¹
+  ( path-sym
+    ( f (f x) = f x)
+    ( path-concat A (f (f x)) x (f x)
+      ( path-concat A (f (f x)) (f x) x
+        ( H (f x))
+        ( H x))
+      ( path-sym A (f x) x
+        ( H x)))
+    ( H (f x))
+    ( right-concat-right-inv-remove-refl A (f (f x)) (f x) x
+      ( H (f x))
+      ( H x)))
+
+  -- proof that (H (f x) • H x) • (H x)⁻¹ = (f (H x) • (H x)) • (H x)⁻¹
+  ( ap
+    ( f (f x) = x) -- (type of domain)
+    ( f (f x) = f x) -- (type of codomain)
+
+    ( \ p' →
+        path-concat A (f (f x)) x (f x)
+          ( p')
+          ( path-sym A (f x) x
+            ( H x)))
+
+    -- function-to-apply: whiskering by (Hx)⁻¹, a.k.a. cancel out H x
+    ( path-concat A (f (f x)) (f x) x
+      ( H (f x))
+      ( H x)) -- left point in path below
+    ( path-concat A (f (f x)) (f x) x
+      ( ap A A f (f x) x (H x))
+      ( H x)) -- right point in path below
+    ( path-concat
+        ( f (f x) = x)
+        -- (H (f x) • H x)
+        ( path-concat A (f (f x)) (f x) x
+          ( H (f x))
+          ( H x))
+        -- (H (f x) • id (H x))
+        ( path-concat A (f (f x)) (f x) x
+          ( H (f x))
+          ( ap A A (\ z → z) (f x) x (H x)))
+        -- f (H x) • (H x)
+        ( path-concat A (f (f x)) (f x) x
+          ( ap A A f (f x) x (H x))
+          ( H x))
+        -- (H (f x) • H x) = (H (f x) • id (H x))
+        ( ap
+          ( f x = x) -- domain
+          ( ( f (f x)) = x) -- codomain
+          ( \ p' →
+              path-concat A (f (f x)) (f x) x
+                ( H (f x))
+                ( p')) -- action of concatenation
+          ( H x) -- left point in path
+          ( ap A A (\ z → z) (f x) x (H x)) -- right point in path
+          ( path-sym (f x = x)
+            ( ap A A (\ z → z) (f x) x (H x))
+            ( H x)
+            ( ap-id A (f x) x (H x))))
+        -- (H (f x) • id (H x)) = f (H x) • (H x)
+        ( hom-naturality A A f (\ z → z) H (f x) x (H x))))
+
+  -- proof that (f (H x) • (H x)) • (H x)⁻¹ = f (H x)
+  ( right-concat-right-inv-remove-refl A (f (f x)) (f x) x
+    ( ap A A f (f x) (id A x) (H x))
+    ( H x))
+
    + + + + + + +
    +
    + + +
    + +
    + + + +
    +
    +
    +
    + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/1-foundations/2-homotopy-type-theory/05-the-higher-groupoid-structure-of-type-formers.rzk/index.html b/1-foundations/2-homotopy-type-theory/05-the-higher-groupoid-structure-of-type-formers.rzk/index.html index afd9237..a8be6ee 100644 --- a/1-foundations/2-homotopy-type-theory/05-the-higher-groupoid-structure-of-type-formers.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/05-the-higher-groupoid-structure-of-type-formers.rzk/index.html @@ -9,7 +9,7 @@ - + @@ -643,11 +643,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + @@ -988,7 +1050,7 @@

    2.5 The higher groupoi @@ -967,6 +1029,107 @@

    2.6 Cartesian product types
    #lang rzk-1

    +

    For any elements \(x, y : A \times B\) and a path \(p : x =_{A \times B} y\), by functoriality we can extract paths \(\mathsf{pr}_1(p) : \mathsf{pr}_1(x) =_A \mathsf{pr}_1(y)\) and \(\mathsf{pr}_2(p) : \mathsf{pr}_2(x) =_B \mathsf{pr}_2(y)\).

    +
    #def path-in-prod-to-prod-of-paths
+  ( A B : U)
+  ( x y : prod A B)
+  : ( x = y)
+  → prod
+    ( pr₁ A B x = pr₁ A B y)
+    ( pr₂ A B x = pr₂ A B y)
+  :=
+  \ p →
+    ( ap (prod A B) A (pr₁ A B) x y p
+    , ap (prod A B) B (pr₂ A B) x y p)
+
    +
    +

    Theorem 2.6.2. Paths in a product space are pairs of paths

    +

    The function

    +
    \[(x =_{A \times B} y) → (\mathsf{pr}_1(x) =_A \mathsf{pr}_1(y)) \times (\mathsf{pr}_2(x) =_B \mathsf{pr}_2(y)).\]
    +

    is an equivalence

    +
    +
    #def prod-of-paths-to-path-in-prod
+  ( A B : U)
+  ( a₁ a₂ : A)
+  ( b₁ b₂ : B)
+  : prod (a₁ = a₂) (b₁ = b₂)
+  → ( a₁ , b₁) = (a₂ , b₂)
+  :=
+  \ (pa , pb) →
+    path-ind A
+    ( \ x y p → (x , b₁) = (y , b₂))
+    ( \ x →
+        path-ind B
+        ( \ x' y' _p' → (x , x') = (x , y'))
+        ( \ _x' → refl)
+        ( b₁)
+        ( b₂)
+        ( pb))
+    ( a₁)
+    ( a₂)
+    ( pa)
+
    +
    #def prod-path-qinv
+  ( A B : U)
+  ( a₁ a₂ : A)
+  ( b₁ b₂ : B)
+  : qinv
+    ( ( a₁ , b₁) = (a₂ , b₂))
+    ( prod (a₁ = a₂) (b₁ = b₂))
+    ( path-in-prod-to-prod-of-paths A B (a₁ , b₁) (a₂ , b₂))
+  :=
+  ( prod-of-paths-to-path-in-prod A B a₁ a₂ b₁ b₂
+  , ( \ (pa , pb) →
+        path-ind A
+        ( \ x y p →
+          path-in-prod-to-prod-of-paths A B (x , b₁) (y , b₂)
+          ( prod-of-paths-to-path-in-prod A B x y b₁ b₂
+            ( p , pb))
+        = ( p , pb))
+        ( \ x →
+            path-ind B
+            ( \ x' y' p' →
+                path-in-prod-to-prod-of-paths A B (x , x') (x , y')
+                ( prod-of-paths-to-path-in-prod A B x x x' y'
+                  ( refl , p'))
+              = ( refl , p'))
+            ( \ x' → refl)
+            ( b₁)
+            ( b₂)
+            ( pb)
+        )
+        ( a₁)
+        ( a₂)
+        ( pa)
+      , \ pab →
+          path-ind (prod A B)
+          ( \ (a₁' , b₁') (a₂' , b₂') pab' →
+              prod-of-paths-to-path-in-prod A B a₁' a₂' b₁' b₂'
+              ( path-in-prod-to-prod-of-paths A B (a₁' , b₁') (a₂' , b₂')
+                ( pab'))
+            = pab')
+          ( \ x → refl)
+          ( a₁ , b₁)
+          ( a₂ , b₂)
+          ( pab)
+      )
+  )
+
    +
    #def paths-in-prod-equiv-prod-of-paths
+  ( A B : U)
+  ( a₁ a₂ : A)
+  ( b₁ b₂ : B)
+  : equivalence
+    ( ( a₁ , b₁) = (a₂ , b₂))
+    ( prod (a₁ = a₂) (b₁ = b₂))
+  :=
+  ( path-in-prod-to-prod-of-paths A B (a₁ , b₁) (a₂ , b₂)
+  , qinv-to-isequiv
+    ( ( a₁ , b₁) = (a₂ , b₂))
+    ( prod (a₁ = a₂) (b₁ = b₂))
+    ( path-in-prod-to-prod-of-paths A B (a₁ , b₁) (a₂ , b₂))
+    ( prod-path-qinv A B a₁ a₂ b₁ b₂))
+
    diff --git a/1-foundations/2-homotopy-type-theory/07-sigma-types.rzk/index.html b/1-foundations/2-homotopy-type-theory/07-sigma-types.rzk/index.html index cdc6daa..8792416 100644 --- a/1-foundations/2-homotopy-type-theory/07-sigma-types.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/07-sigma-types.rzk/index.html @@ -643,11 +643,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/08-the-unit-type.rzk/index.html b/1-foundations/2-homotopy-type-theory/08-the-unit-type.rzk/index.html index a1801b5..2d98eb2 100644 --- a/1-foundations/2-homotopy-type-theory/08-the-unit-type.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/08-the-unit-type.rzk/index.html @@ -643,11 +643,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + @@ -967,6 +1029,29 @@

    2.8 The unit type
    #lang rzk-1
    +

    For Unit type, uniqueness principle is built-in. That is, for any x, y : Unit, we have refl : x = y

    +
    +

    Theorem 2.8.1.

    +

    For any \(x, y : \mathbb{1}\), we have \((x = y) \simeq \mathbb{1}\).

    +
    +
    #def paths-in-unit-equiv-unit
+    ( x y : Unit)
+  : equivalence (x = y) Unit
+    -- provide a function - a constant map to unit
+  :=
+  ( \ (p : x = y) → unit
+  , ( -- provide right inverse - a constant map to refl_{unit}
+      ( \ (u : Unit) → refl_{unit}
+      , -- prove that composition is homotopical to id_Unit
+        \ (u : Unit) → refl)
+    , -- provide left inverse - a constant map to refl_{unit}
+      ( \ (u : Unit) → refl_{unit}
+      , -- prove that composition is homotopical to id_{x = y}; use path induction on p
+        path-ind Unit
+        ( \ x' y' p' → refl_{unit} = p')
+        ( \ x' → refl)
+        x y)))
+
    diff --git a/1-foundations/2-homotopy-type-theory/09-pi-types-and-function-extensionality.rzk/index.html b/1-foundations/2-homotopy-type-theory/09-pi-types-and-function-extensionality.rzk/index.html index 45a3e4e..09b182a 100644 --- a/1-foundations/2-homotopy-type-theory/09-pi-types-and-function-extensionality.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/09-pi-types-and-function-extensionality.rzk/index.html @@ -643,11 +643,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + @@ -967,6 +1029,38 @@

    2.9 
    #lang rzk-1
    +
    HoTT Book, Definition 2.9.2
    #define happly
+  ( A : U)
+  ( B : A → U)
+  ( f g : (a : A) → B a)
+  : ( f = g) → homotopy A B f g
+  :=
+  path-ind ((a : A) → B a)
+  ( \ f' g' _ → homotopy A B f' g')
+  ( \ f' _ → refl)
+  f g
+
    +
    HoTT Book, Axiom 2.9.3
    #define FunExt
+  : U
+  :=
+    ( A : U)
+  → ( B : A → U)
+  → ( f : (a : A) → B a)
+  → ( g : (a : A) → B a)
+  → isequiv
+    ( f = g)
+    ( homotopy A B f g)
+    ( happly A B f g)
+
    +
    #assume funext : FunExt
+
    +
    #define map-funext uses (funext)
+  ( A : U)
+  ( B : A → U)
+  ( f g : (a : A) → B a)
+  : homotopy A B f g → f = g
+  := first (second (funext A B f g))
+
    diff --git a/1-foundations/2-homotopy-type-theory/10-universes-and-univalence-axiom.rzk/index.html b/1-foundations/2-homotopy-type-theory/10-universes-and-univalence-axiom.rzk/index.html index 0e522d9..464879f 100644 --- a/1-foundations/2-homotopy-type-theory/10-universes-and-univalence-axiom.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/10-universes-and-univalence-axiom.rzk/index.html @@ -643,11 +643,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/11-identity-type.rzk/index.html b/1-foundations/2-homotopy-type-theory/11-identity-type.rzk/index.html index 147a8eb..a9b6ec9 100644 --- a/1-foundations/2-homotopy-type-theory/11-identity-type.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/11-identity-type.rzk/index.html @@ -643,11 +643,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/12-coproducts.rzk/index.html b/1-foundations/2-homotopy-type-theory/12-coproducts.rzk/index.html index 744f916..f52aeef 100644 --- a/1-foundations/2-homotopy-type-theory/12-coproducts.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/12-coproducts.rzk/index.html @@ -643,11 +643,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/13-natural-numbers.rzk/index.html b/1-foundations/2-homotopy-type-theory/13-natural-numbers.rzk/index.html index 018d9a2..7e38b7c 100644 --- a/1-foundations/2-homotopy-type-theory/13-natural-numbers.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/13-natural-numbers.rzk/index.html @@ -643,11 +643,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/14-example-equality-of-structures.rzk/index.html b/1-foundations/2-homotopy-type-theory/14-example-equality-of-structures.rzk/index.html index d370994..aada5ed 100644 --- a/1-foundations/2-homotopy-type-theory/14-example-equality-of-structures.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/14-example-equality-of-structures.rzk/index.html @@ -643,11 +643,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/15-universal-properties.rzk/index.html b/1-foundations/2-homotopy-type-theory/15-universal-properties.rzk/index.html index 91b26e9..eaf2836 100644 --- a/1-foundations/2-homotopy-type-theory/15-universal-properties.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/15-universal-properties.rzk/index.html @@ -643,11 +643,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -915,6 +915,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.1-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.1-solution.rzk/index.html index b3ebbf1..0b37bb3 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.1-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.1-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.10-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.10-solution.rzk/index.html index 93ecece..2f95c74 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.10-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.10-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.11-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.11-solution.rzk/index.html index 7626720..ed03d81 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.11-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.11-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.12-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.12-solution.rzk/index.html index 605c3e2..4eb4a6d 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.12-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.12-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.13-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.13-solution.rzk/index.html index 3757efd..404f290 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.13-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.13-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.14-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.14-solution.rzk/index.html index 7064044..5b773bd 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.14-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.14-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.15-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.15-solution.rzk/index.html index 5b2e53f..d088f08 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.15-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.15-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.16-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.16-solution.rzk/index.html index 86a529c..00dacd6 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.16-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.16-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.17-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.17-solution.rzk/index.html index 8f80214..213db60 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.17-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.17-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.18-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.18-solution.rzk/index.html index 89102c3..5b320c2 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.18-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.18-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.2-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.2-solution.rzk/index.html index cfc79e0..e819c0b 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.2-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.2-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.3-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.3-solution.rzk/index.html index b84deb9..399ca6b 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.3-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.3-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.4-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.4-solution.rzk/index.html index 980cbcd..3101402 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.4-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.4-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.5-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.5-solution.rzk/index.html index 8f74b3b..4dd0b36 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.5-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.5-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.6-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.6-solution.rzk/index.html index 5b3ba74..dca6787 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.6-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.6-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.7-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.7-solution.rzk/index.html index 81b9867..353f23f 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.7-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.7-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.8-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.8-solution.rzk/index.html index fb4deb7..85f5471 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.8-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.8-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/2.9-solution.rzk/index.html b/1-foundations/2-homotopy-type-theory/exercises/2.9-solution.rzk/index.html index 5b20a69..22fb368 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/2.9-solution.rzk/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/2.9-solution.rzk/index.html @@ -635,11 +635,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -897,6 +897,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + diff --git a/1-foundations/2-homotopy-type-theory/exercises/index.html b/1-foundations/2-homotopy-type-theory/exercises/index.html index 0b03a9d..954365f 100644 --- a/1-foundations/2-homotopy-type-theory/exercises/index.html +++ b/1-foundations/2-homotopy-type-theory/exercises/index.html @@ -12,6 +12,8 @@ + + @@ -641,11 +643,11 @@
  • - + - 2.4 Homotopies are equivalences + 2.4 Homotopies and equivalences @@ -1069,6 +1071,68 @@ + + + + + + + + +
  • + + + + + + + + + + + +
    • + + + + @@ -1397,6 +1461,22 @@

    Exercise 2.18 + + + diff --git a/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk/index.html b/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk/index.html new file mode 100644 index 0000000..da3b031 --- /dev/null +++ b/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk/index.html @@ -0,0 +1,1359 @@ + + + + + + + + + + + + + + + + + + + + + 3.1 Sets and n-types - HoTT Book formalisation in Rzk proof assistant + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + + + Skip to content + + +
    +
    + +
    + + + + + + +
    + + +
    + +
    + + + + + + +
    +
    + + + +
    +
    +
    + + + + + +
    +
    +
    + + + +
    +
    +
    + + + +
    +
    +
    + + + +
    +
    + + + + + + + + + + + + +

    3.1 Sets and \(n\)-types

    +

    This is a literate Rzk file:

    +
    #lang rzk-1
+
    +

    This module assumes function extensionality:

    +
    #assume funext : FunExt
+
    +

    In general, types behave like spaces or higher groupoids, but there is a subclass of types that behave more like sets in a traditional sense. +We expect a type to be a set, if there is no higher homotopical information.

    +
    +

    Definition 3.1.1.

    +

    A type \(A\) is a set if for all \(x, y : A\) and all \(p, q : x = y\), we have \(p = q\).

    +
    +
    #def isSet
+  ( A : U)
+  : U
+  :=
+    ( x : A)
+  → ( y : A)
+  → ( p : x = y)
+  → ( q : x = y)
+  → ( p = q)
+
    +

    Some examples

    +

    Many of the proofs below appeal to the injectivity of equivalences:

    +
    #define injective-equivalence
+  ( A B : U)
+  ( ( f , isequiv-f) : equivalence A B)
+  ( x y : A)
+  : ( f x = f y)
+  → ( x = y)
+  :=
+  \ fx-eq-fy →
+    3-path-concat A
+    ( x)
+    ( first (second isequiv-f) (f x))
+    ( first (second isequiv-f) (f y))
+    ( y)
+    ( path-sym A
+      ( first (second isequiv-f) (f x))
+      ( x)
+      ( second (second isequiv-f) x))
+    ( ap B A
+      ( first (second isequiv-f))
+      ( f x)
+      ( f y)
+      fx-eq-fy)
+    ( second (second isequiv-f) y)
+
    +

    Unit type is a set

    +
    +

    Example 3.1.2.

    +

    The type \(\mathbb{1}\) is a set.

    +
    +
    #def isSet-Unit
+  : isSet Unit
+  :=
+  \ x y p q →
+    injective-equivalence
+    ( x = y)
+    ( Unit)
+    ( paths-in-unit-equiv-unit x y)
+    ( p)
+    ( q)
+    ( refl)
+
    +

    Products of sets are sets

    +
    +

    Example 3.1.5.

    +

    If \(A\) and \(B\) are sets, then so is \(A \times B\).

    +
    +
    #def isSet-prod
+  ( A B : U)
+  ( isSet-A : isSet A)
+  ( isSet-B : isSet B)
+  : isSet (prod A B)
+  :=
+  \ (a₁ , b₁) (a₂ , b₂) p q →
+    injective-equivalence
+    ( ( a₁ , b₁) = (a₂ , b₂))
+    ( prod (a₁ = a₂) (b₁ = b₂))
+    ( paths-in-prod-equiv-prod-of-paths A B a₁ a₂ b₁ b₂)
+    ( p)
+    ( q)
+    ( prod-of-paths-to-path-in-prod
+      ( a₁ = a₂)
+      ( b₁ = b₂)
+      ( ap (prod A B) A (pr₁ A B) (a₁ , b₁) (a₂ , b₂) p)
+      ( ap (prod A B) A (pr₁ A B) (a₁ , b₁) (a₂ , b₂) q)
+      ( ap (prod A B) B (pr₂ A B) (a₁ , b₁) (a₂ , b₂) p)
+      ( ap (prod A B) B (pr₂ A B) (a₁ , b₁) (a₂ , b₂) q)
+      ( ( isSet-A a₁ a₂
+          ( ap (prod A B) A (pr₁ A B) (a₁ , b₁) (a₂ , b₂) p)
+          ( ap (prod A B) A (pr₁ A B) (a₁ , b₁) (a₂ , b₂) q)
+        , isSet-B b₁ b₂
+          ( ap (prod A B) B (pr₂ A B) (a₁ , b₁) (a₂ , b₂) p)
+          ( ap (prod A B) B (pr₂ A B) (a₁ , b₁) (a₂ , b₂) q)))
+    )
+
    +

    Function types into sets form sets

    +
    +

    Example 3.1.6

    +

    If \(A\) is any type and \(B : A \to \mathcal{U}\) is such that each \(B(x)\) is a set, then the type \(\prod_{(x:A)} B(x)\) is a set.

    +
    +
    #define weak-isSet-function
+  ( A B : U)
+  ( isSet-B : isSet B)
+  ( f g : A → B)
+  ( p q : homotopy A (\ _ → B) f g)
+  : homotopy A (\ x → f x = g x) p q
+  := \ x → isSet-B (f x) (g x) (p x) (q x)
+
+#define weak-isSet-function₁
+  ( A B : U)
+  ( isSet-B : isSet B)
+  ( f g : A → B)
+  ( p q : f = g)
+  : homotopy A (\ x → f x = g x)
+    ( happly A (\ _ → B) f g p)
+    ( happly A (\ _ → B) f g q)
+  :=
+  weak-isSet-function A B isSet-B f g
+  ( happly A (\ _ → B) f g p)
+  ( happly A (\ _ → B) f g q)
+
+#define weak-isSet-function₂ uses (funext)
+  ( A B : U)
+  ( isSet-B : isSet B)
+  ( f g : A → B)
+  ( p q : f = g)
+  : happly A (\ _ → B) f g p
+  = happly A (\ _ → B) f g q
+  :=
+  map-funext funext A (\ x → f x = g x)
+  ( happly A (\ _ → B) f g p)
+  ( happly A (\ _ → B) f g q)
+  ( weak-isSet-function₁ A B isSet-B f g p q)
+
+#define isSet-function uses (funext)
+  ( A B : U)
+  ( isSet-B : isSet B)
+  : isSet (A → B)
+  :=
+  \ f g p q →
+    injective-equivalence
+    ( f = g)
+    ( homotopy A (\ _ → B) f g)
+    ( happly A (\ _ → B) f g
+    , funext A (\ _ → B) f g)
+    ( p)
+    ( q)
+    ( weak-isSet-function₂ A B isSet-B f g p q)
+
    + + + + + + +
    +
    + + +
    + +
    + + + +
    +
    +
    +
    + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/1-foundations/2-homotopy-type-theory/04-homotopies-are-equivalences.rzk/index.html b/1-foundations/3-sets-and-logic/02-propositions-as-types.rzk copy/index.html similarity index 86% rename from 1-foundations/2-homotopy-type-theory/04-homotopies-are-equivalences.rzk/index.html rename to 1-foundations/3-sets-and-logic/02-propositions-as-types.rzk copy/index.html index 6655b03..79a5925 100644 --- a/1-foundations/2-homotopy-type-theory/04-homotopies-are-equivalences.rzk/index.html +++ b/1-foundations/3-sets-and-logic/02-propositions-as-types.rzk copy/index.html @@ -9,10 +9,6 @@ - - - - @@ -20,7 +16,7 @@ - 2.4 Homotopies are equivalences - HoTT Book formalisation in Rzk proof assistant + Propositions as types? - HoTT Book formalisation in Rzk proof assistant @@ -75,7 +71,7 @@
    - + Skip to content @@ -110,7 +106,7 @@
    - 2.4 Homotopies are equivalences + Propositions as types?
    @@ -265,21 +261,19 @@ - - -
  • +
  • - + -