This commit is contained in:
Michael Zhang 2024-09-05 11:29:34 +02:00
parent 8ecbcefe92
commit c1788c20fb
6 changed files with 23 additions and 19 deletions

Binary file not shown.

View file

@ -1,5 +1,5 @@
\RequirePackage{fix-cm}
\def\OPTpagesize{4.8in,7.9in} % Page size
\def\OPTpagesize{6in,9in} % Page size
\documentclass[12pt]{report}
\usepackage[hyphens]{url}
\usepackage[

View file

@ -16,8 +16,8 @@ transportconst : {A : Type l} {x y : A}
→ (B : Type l2)
→ (p : x ≡ y)
→ (b : B)
→ subst ? p ? ≡ ?
transportconst B p b = ?
→ subst (λ _ → B) p b ≡ b
transportconst B p b i = {! !}
```
### Definition 2.4.1
@ -58,7 +58,6 @@ mkIsEquiv : {A B : Type} {f : A → B}
mkIsEquiv {B = B} {f = f} g forward backward = record { equiv-proof = eqv-prf } where
postulate
helper : (y : B) → (z : fiber f y) → (g y , forward y) ≡ z
-- helper y (x , p) = Σ-≡,≡→≡ (ap g (sym p) ∙ backward x , {! !})
eqv-prf : (y : B) → isContr (fiber f y)
eqv-prf y = (g y , forward y) , helper y
@ -67,22 +66,22 @@ mkIsEquiv {B = B} {f = f} g forward backward = record { equiv-proof = eqv-prf }
### Theorem 2.11.3
```
theorem2∙11∙3 : {A B : Type} {f g : A → B} {a a' : A}
→ (p : a ≡ a')
→ (q : f a ≡ g a)
→ subst (λ x → f x ≡ g x) p q ≡ sym (ap f p) ∙ q ∙ ap g p
theorem2∙11∙3 refl q = sym (unitR q)
-- theorem2∙11∙3 : {A B : Type} {f g : A → B} {a a' : A}
-- → (p : a ≡ a')
-- → (q : f a ≡ g a)
-- → subst (λ x → f x ≡ g x) p q ≡ sym (ap f p) ∙ q ∙ ap g p
-- theorem2∙11∙3 refl q = sym (unitR q)
```
### Theorem 2.11.5
```
postulate
theorem2∙11∙5 : {A : Type} {a a' : A}
→ (p : a ≡ a')
→ (q : a ≡ a)
→ (r : a' ≡ a')
→ (transport (λ x → x ≡ x) p q ≡ r) ≃ (q ∙ p ≡ p ∙ r)
-- postulate
-- theorem2∙11∙5 : {A : Type} {a a' : A}
-- → (p : a ≡ a')
-- → (q : a ≡ a)
-- → (r : a' ≡ a')
-- → (transport (λ x → x ≡ x) p q ≡ r) ≃ (q ∙ p ≡ p ∙ r)
-- theorem2∙11∙5 {a = a} refl q r = f , mkIsEquiv g {! !} {! !} where
-- f : (q ≡ r) → (q ∙ refl ≡ r)
-- f refl = unitR q

View file

@ -4,6 +4,9 @@ module CubicalHottBook.Prelude where
open import Cubical.Foundations.Function public
open import Data.Product.Properties public
open import Cubical.Foundations.Prelude public
open import Cubical.Data.Equality public using (id)
open import Cubical.Foundations.Equiv public
module Inductive where
open import Cubical.Data.Equality public
open Inductive public using (id)

View file

@ -480,6 +480,4 @@ module Pushout where
Pushout : {A B C : Set} → (f : C → A) → (g : C → B) → Set
syntax Pushout A B C = A ⊔[ C ] B
```
## asdf
```

View file

@ -0,0 +1,4 @@
{-# OPTIONS --cubical --safe #-}
module VanDoornDissertation.HoTT.LongExactSequence where