From 4924c5ff5efcc8a2f3360befe58da886e6831071 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Wed, 11 Oct 2023 16:44:14 +0200 Subject: [PATCH 1/6] fiber products and relative products --- src/hott/11-homotopy-pullbacks.rzk.md | 111 ++++++++++++++++++++++++++ 1 file changed, 111 insertions(+) diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index 972814f4..87cd0b27 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -411,3 +411,114 @@ from composition and cancelling laws for equivalences. #end homotopy-cartesian-horizontal-calculus ``` + +## Fiber products + +Given two type families `B C : A → U`, we can form their fiberwise product. + +```rzk +#def fiberwise-product + ( A : U) + ( B C : A → U) + : A → U + := + \ a → product (B a) (C a) + +#def first-fiberwise-product + ( A : U) + ( B C : A → U) + ( a : A) + : fiberwise-product A B C a → B a + := \ (b,_) → b + +#def second-fiberwise-product + ( A : U) + ( B C : A → U) + ( a : A) + : fiberwise-product A B C a → C a + := \ (_,c) → c +``` + +Given two maps `B → A` and `C → A`, we can form the relative product over `A`. + +```rzk +#section relative-product + +#variable A : U +#variable B : U +#variable β : B → A +#variable C : U +#variable γ : C → A + +#def relative-product + : U + := Σ ( (b, c) : product B C) , β b = γ c + +#def first-relative-product uses (A B β C γ) + : relative-product → B + := \ ((b , _), _) → b + +#def second-relative-product uses (A B β C γ) + : relative-product → C + := \ ((_ , c), _) → c +``` + +This relative product agrees with the fiber product obtained by summing +over the product of all fibers. + +```rzk +#def fiber-product + : U + := total-type A (fiberwise-product A (fib B A β) (fib C A γ)) + +#def fiber-product-unpacked + : fiber-product + = ( Σ (a : A), (product (fib B A β a) (fib C A γ a))) + := refl + +#def relative-fiber-product uses (B C) + ( (a, ((b, p), (c,q))) : fiber-product ) + : relative-product + := ( ( b , c) , zig-zag-concat A (β b) a (γ c) p q) + +#def fiber-relative-product uses ( A B β C) + ( ((b,c), e) : relative-product) + : fiber-product + := ( γ c , ( (b , e) , (c , refl))) + +#def is-id-relative-fiber-relative-product + ( bce : relative-product) + : relative-fiber-product (fiber-relative-product bce) = bce + := refl + +#def is-id-fiber-relative-fiber-product + : ( abpcq : fiber-product) + → ( fiber-relative-product (relative-fiber-product abpcq)) = abpcq + := + \ (a', (bq', cq')) → + ind-fib C A γ + ( \ a cq → + ( ( bq : fib B A β a) + → ( fiber-relative-product (relative-fiber-product (a, (bq, cq))) + = ( a, (bq, cq))))) + ( \ c bq → refl) + ( a') + ( cq') + ( bq') + +#def is-equiv-relative-fiber-product uses (A B β C γ) + : is-equiv fiber-product relative-product relative-fiber-product + := + ( ( fiber-relative-product + , is-id-fiber-relative-fiber-product) + , ( fiber-relative-product + , is-id-relative-fiber-relative-product)) + +#def equiv-relative-product-fiber-product uses (A B β C γ) + : Equiv fiber-product relative-product + := + ( relative-fiber-product + , is-equiv-relative-fiber-product) + +#end relative-product +``` From 3f7bc117a4470deb9bab5091094c2ba46bd137ef Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Wed, 11 Oct 2023 16:54:57 +0200 Subject: [PATCH 2/6] fill region --- src/hott/11-homotopy-pullbacks.rzk.md | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index 87cd0b27..e4a0eb2d 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -35,8 +35,8 @@ We start by fixing the data of a map between two type families := \ (a', c') → (α a', γ a' c') ``` -We say that such a square is homotopy cartesian -just if it induces an equivalence componentwise. +We say that such a square is homotopy cartesian just if it induces an +equivalence componentwise. ```rzk #def is-homotopy-cartesian uses (A) @@ -216,8 +216,8 @@ always do this (whether the square is homotopy-cartesian or not). ### Invariance under pullbacks -We can pullback a homotopy cartesian square over `α : A' → A` -along any map of maps `β → α` and obtain another homotopy cartesian square. +We can pullback a homotopy cartesian square over `α : A' → A` along any map of +maps `β → α` and obtain another homotopy cartesian square. ```rzk #def is-homotopy-cartesian-pullback @@ -246,16 +246,15 @@ along any map of maps `β → α` and obtain another homotopy cartesian square. ## Pasting calculus for homotopy cartesian squares -Currently our notion of squares is not symmetric, -since the vertical maps are given by type families, -i.e. they are _display maps_, -while the horizontal maps are arbitrary. -Therefore we distinquish between the vertical and the horizontal pasting calculus. +Currently our notion of squares is not symmetric, since the vertical maps are +given by type families, i.e. they are _display maps_, while the horizontal maps +are arbitrary. Therefore we distinquish between the vertical and the horizontal +pasting calculus. ### Vertical calculus -The following vertical composition and cancellation laws follow easily from -the corresponding statements about equivalences established above. +The following vertical composition and cancellation laws follow easily from the +corresponding statements about equivalences established above. ```rzk #section homotopy-cartesian-vertical-calculus @@ -463,8 +462,8 @@ Given two maps `B → A` and `C → A`, we can form the relative product over `A := \ ((_ , c), _) → c ``` -This relative product agrees with the fiber product obtained by summing -over the product of all fibers. +This relative product agrees with the fiber product obtained by summing over the +product of all fibers. ```rzk #def fiber-product From dc3476b5ec25ac60c66f4acf1f9ec98f38c0ad46 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Wed, 11 Oct 2023 17:42:38 +0200 Subject: [PATCH 3/6] add projections and homotopy to fiber product --- src/hott/11-homotopy-pullbacks.rzk.md | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index 33edb1b1..6fdbd16c 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -461,6 +461,11 @@ Given two maps `B → A` and `C → A`, we can form the relative product over `A #def second-relative-product uses (A B β C γ) : relative-product → C := \ ((_ , c), _) → c + +#def homotopy-relative-product uses (A B C) + ( (bc, p) : relative-product ) + : β (first-relative-product (bc,p)) = γ (second-relative-product (bc,p)) + := p ``` This relative product agrees with the fiber product obtained by summing over the @@ -476,6 +481,21 @@ product of all fibers. = ( Σ (a : A), (product (fib B A β a) (fib C A γ a))) := refl +#def first-fiber-product uses (A B β C γ) + : fiber-product → B + := \ (_, ((b, _), _ )) → b + +#def second-fiber-product uses (A B β C γ) + : fiber-product → C + := \ (_, (_, (c, _))) → c + +#def homotopy-fiber-product uses (A B C) + : ( abpcq : fiber-product ) + → β (first-fiber-product abpcq) = γ (second-fiber-product abpcq) + := + \ ( a, ((b, p), (c,q))) → + zig-zag-concat A (β b) a (γ c) p q + #def relative-fiber-product uses (B C) ( (a, ((b, p), (c,q))) : fiber-product ) : relative-product From 7261a929d2f3625b830d9da44a997ba289d2e692 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 12 Oct 2023 18:25:21 +0200 Subject: [PATCH 4/6] compute fiber product with unit type --- src/hott/11-homotopy-pullbacks.rzk.md | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index 6fdbd16c..a5514a80 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -542,3 +542,29 @@ product of all fibers. #end relative-product ``` + +### Fiber product with singleton type + +The relative product of `β : B → A` with a map `Unit → A` corresponding to +`a : A` is nothing but the fiber `fib B A β a`. + +```rzk +#def compute-relative-product-singleton + ( A B : U) + ( β : B → A) + ( a : A) + : Equiv-of-maps + ( fib B A β a) (Unit) (\ _ → unit) + ( relative-product A B β Unit (\ unit → a)) + ( Unit) ( second-relative-product A B β Unit (\ unit → a)) + := + ( ( ( ( \ (b , p) → ((b , unit) , p)) + , ( identity Unit)) + , \ _ → refl) + , ( ( ( ( \ ((b , unit) , p) → (b, p)) + , ( \ _ → refl)) + , ( ( \ ((b , unit) , p) → (b, p)) + , ( \ _ → refl))) + , is-equiv-identity Unit)) + +``` From ebc3aa67699063556f0e04649d8a8924f1a6dced Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Fri, 13 Oct 2023 17:04:29 +0200 Subject: [PATCH 5/6] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- src/hott/11-homotopy-pullbacks.rzk.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index a5514a80..bbe6209c 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -414,7 +414,7 @@ from composition and cancelling laws for equivalences. ## Fiber products -Given two type families `B C : A → U`, we can form their fiberwise product. +Given two type families `B C : A → U`, we can form their **fiberwise product**. ```rzk #def fiberwise-product @@ -439,7 +439,7 @@ Given two type families `B C : A → U`, we can form their fiberwise product. := \ (_,c) → c ``` -Given two maps `B → A` and `C → A`, we can form the relative product over `A`. +Given two maps `B → A` and `C → A`, we can form the **relative product** over `A`. ```rzk #section relative-product @@ -452,7 +452,7 @@ Given two maps `B → A` and `C → A`, we can form the relative product over `A #def relative-product : U - := Σ ( (b, c) : product B C) , β b = γ c + := Σ ( (b, c) : product B C) , (β b = γ c) #def first-relative-product uses (A B β C γ) : relative-product → B @@ -476,7 +476,7 @@ product of all fibers. : U := total-type A (fiberwise-product A (fib B A β) (fib C A γ)) -#def fiber-product-unpacked +#def unpack-fiber-product : fiber-product = ( Σ (a : A), (product (fib B A β a) (fib C A γ a))) := refl From e2149822477ee4bb0e901831b7de044e82a856f0 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Fri, 13 Oct 2023 17:07:44 +0200 Subject: [PATCH 6/6] autoformat --- src/hott/11-homotopy-pullbacks.rzk.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index bbe6209c..45aeb770 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -439,7 +439,8 @@ Given two type families `B C : A → U`, we can form their **fiberwise product** := \ (_,c) → c ``` -Given two maps `B → A` and `C → A`, we can form the **relative product** over `A`. +Given two maps `B → A` and `C → A`, we can form the **relative product** over +`A`. ```rzk #section relative-product