Skip to content

Commit 92d51e6

Browse files
fredrik-bakkefredrik-bakke
authored
Refactor extensions of maps (#1695)
pulled from #1677 and #1668.
1 parent ccfcf55 commit 92d51e6

8 files changed

+679
-322
lines changed

‎src/foundation/surjective-maps.lagda.md‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,9 @@ open import foundation-core.torsorial-type-families
5252
open import foundation-core.truncated-maps
5353
open import foundation-core.truncation-levels
5454
55+
open import orthogonal-factorization-systems.equality-extensions-maps
5556
open import orthogonal-factorization-systems.extensions-maps
57+
open import orthogonal-factorization-systems.postcomposition-extensions-maps
5658
```
5759

5860
</details>
@@ -831,8 +833,8 @@ module _
831833
( g ∘ i)
832834
( postcomp-extension f i g (j , N))
833835
( h , L)
834-
( M)
835-
( λ a →
836+
( M ,
837+
λ a →
836838
( ap
837839
( concat' (g (i a)) (M (f a)))
838840
( is-section-map-inv-is-equiv

‎src/orthogonal-factorization-systems.lagda.md‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,8 @@ open import orthogonal-factorization-systems.closed-modalities public
1616
open import orthogonal-factorization-systems.continuation-modalities public
1717
open import orthogonal-factorization-systems.double-lifts-families-of-elements public
1818
open import orthogonal-factorization-systems.double-negation-sheaves public
19+
open import orthogonal-factorization-systems.equality-extensions-maps public
20+
open import orthogonal-factorization-systems.extensions-dependent-maps public
1921
open import orthogonal-factorization-systems.extensions-double-lifts-families-of-elements public
2022
open import orthogonal-factorization-systems.extensions-lifts-families-of-elements public
2123
open import orthogonal-factorization-systems.extensions-maps public
@@ -56,6 +58,7 @@ open import orthogonal-factorization-systems.null-types public
5658
open import orthogonal-factorization-systems.open-modalities public
5759
open import orthogonal-factorization-systems.orthogonal-factorization-systems public
5860
open import orthogonal-factorization-systems.orthogonal-maps public
61+
open import orthogonal-factorization-systems.postcomposition-extensions-maps public
5962
open import orthogonal-factorization-systems.precomposition-lifts-families-of-elements public
6063
open import orthogonal-factorization-systems.pullback-hom public
6164
open import orthogonal-factorization-systems.raise-modalities public

‎src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md‎

Lines changed: 189 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,189 @@
1+
# Equality of extensions of maps
2+
3+
```agda
4+
module orthogonal-factorization-systems.equality-extensions-maps where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import foundation.dependent-pair-types
11+
open import foundation.equivalences
12+
open import foundation.fundamental-theorem-of-identity-types
13+
open import foundation.homotopies
14+
open import foundation.homotopy-induction
15+
open import foundation.identity-types
16+
open import foundation.structure-identity-principle
17+
open import foundation.universe-levels
18+
open import foundation.whiskering-homotopies-composition
19+
20+
open import foundation-core.torsorial-type-families
21+
22+
open import orthogonal-factorization-systems.extensions-dependent-maps
23+
```
24+
25+
</details>
26+
27+
## Idea
28+
29+
We characterize equality of
30+
[extensions](orthogonal-factorization-systems.extensions-maps.md) of
31+
([dependent](orthogonal-factorization-systems.extensions-dependent-maps.md))
32+
maps.
33+
34+
On this page we conflate extensions of dependent maps and extensions of
35+
nondependent maps, as the characterization of equality coincides for the two
36+
notions.
37+
38+
## Definition
39+
40+
### Homotopies of extensions
41+
42+
```agda
43+
module _
44+
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
45+
{P : B → UU l3} (f : (x : A) → P (i x))
46+
where
47+
48+
coherence-htpy-extension :
49+
(e e' : extension-dependent-type i P f) →
50+
map-extension-dependent-type e ~ map-extension-dependent-type e' →
51+
UU (l1 ⊔ l3)
52+
coherence-htpy-extension e e' K =
53+
( is-extension-map-extension-dependent-type e ∙h (K ·r i)) ~
54+
( is-extension-map-extension-dependent-type e')
55+
56+
htpy-extension : (e e' : extension-dependent-type i P f) → UU (l1 ⊔ l2 ⊔ l3)
57+
htpy-extension e e' =
58+
Σ ( map-extension-dependent-type e ~ map-extension-dependent-type e')
59+
( coherence-htpy-extension e e')
60+
61+
refl-htpy-extension :
62+
(e : extension-dependent-type i P f) → htpy-extension e e
63+
pr1 (refl-htpy-extension e) = refl-htpy
64+
pr2 (refl-htpy-extension e) = right-unit-htpy
65+
```
66+
67+
### Homotopies of extensions with homotopies going the other way
68+
69+
```agda
70+
module _
71+
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
72+
{P : B → UU l3} (f : (x : A) → P (i x))
73+
where
74+
75+
coherence-htpy-extension' :
76+
(e e' : extension-dependent-type' i P f) →
77+
map-extension-dependent-type' e ~ map-extension-dependent-type' e' →
78+
UU (l1 ⊔ l3)
79+
coherence-htpy-extension' e e' K =
80+
( is-extension-map-extension-dependent-type' e) ~
81+
( K ·r i ∙h is-extension-map-extension-dependent-type' e')
82+
83+
htpy-extension' :
84+
(e e' : extension-dependent-type' i P f) → UU (l1 ⊔ l2 ⊔ l3)
85+
htpy-extension' e e' =
86+
Σ ( map-extension-dependent-type' e ~ map-extension-dependent-type' e')
87+
( coherence-htpy-extension' e e')
88+
89+
refl-htpy-extension' :
90+
(e : extension-dependent-type' i P f) → htpy-extension' e e
91+
pr1 (refl-htpy-extension' e) = refl-htpy
92+
pr2 (refl-htpy-extension' e) = refl-htpy
93+
```
94+
95+
## Properties
96+
97+
### Homotopies characterize equality
98+
99+
```agda
100+
module _
101+
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
102+
{P : B → UU l3} (f : (x : A) → P (i x))
103+
where
104+
105+
htpy-eq-extension :
106+
(e e' : extension-dependent-type i P f) → e ＝ e' → htpy-extension i f e e'
107+
htpy-eq-extension e .e refl = refl-htpy-extension i f e
108+
109+
abstract
110+
is-torsorial-htpy-extension :
111+
(e : extension-dependent-type i P f) → is-torsorial (htpy-extension i f e)
112+
is-torsorial-htpy-extension e =
113+
is-torsorial-Eq-structure
114+
( is-torsorial-htpy (map-extension-dependent-type e))
115+
( map-extension-dependent-type e , refl-htpy)
116+
( is-torsorial-htpy
117+
( is-extension-map-extension-dependent-type e ∙h
118+
refl-htpy))
119+
120+
abstract
121+
is-equiv-htpy-eq-extension :
122+
(e e' : extension-dependent-type i P f) →
123+
is-equiv (htpy-eq-extension e e')
124+
is-equiv-htpy-eq-extension e =
125+
fundamental-theorem-id
126+
( is-torsorial-htpy-extension e)
127+
( htpy-eq-extension e)
128+
129+
extensionality-extension :
130+
(e e' : extension-dependent-type i P f) →
131+
(e ＝ e') ≃ htpy-extension i f e e'
132+
pr1 (extensionality-extension e e') = htpy-eq-extension e e'
133+
pr2 (extensionality-extension e e') = is-equiv-htpy-eq-extension e e'
134+
135+
eq-htpy-extension :
136+
(e e' : extension-dependent-type i P f) →
137+
htpy-extension i f e e' → e ＝ e'
138+
eq-htpy-extension e e' =
139+
map-inv-equiv (extensionality-extension e e')
140+
```
141+
142+
### Characterizing equality of extensions of dependent maps with homotopies going the other way
143+
144+
```agda
145+
module _
146+
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
147+
{P : B → UU l3} (f : (x : A) → P (i x))
148+
where
149+
150+
htpy-eq-extension' :
151+
(e e' : extension-dependent-type' i P f) →
152+
e ＝ e' → htpy-extension' i f e e'
153+
htpy-eq-extension' e .e refl =
154+
refl-htpy-extension' i f e
155+
156+
abstract
157+
is-torsorial-htpy-extension' :
158+
(e : extension-dependent-type' i P f) →
159+
is-torsorial (htpy-extension' i f e)
160+
is-torsorial-htpy-extension' e =
161+
is-torsorial-Eq-structure
162+
( is-torsorial-htpy (map-extension-dependent-type' e))
163+
( map-extension-dependent-type' e , refl-htpy)
164+
( is-torsorial-htpy
165+
( is-extension-map-extension-dependent-type' e))
166+
167+
abstract
168+
is-equiv-htpy-eq-extension' :
169+
(e e' : extension-dependent-type' i P f) →
170+
is-equiv (htpy-eq-extension' e e')
171+
is-equiv-htpy-eq-extension' e =
172+
fundamental-theorem-id
173+
( is-torsorial-htpy-extension' e)
174+
( htpy-eq-extension' e)
175+
176+
extensionality-extension' :
177+
(e e' : extension-dependent-type' i P f) →
178+
(e ＝ e') ≃ (htpy-extension' i f e e')
179+
pr1 (extensionality-extension' e e') =
180+
htpy-eq-extension' e e'
181+
pr2 (extensionality-extension' e e') =
182+
is-equiv-htpy-eq-extension' e e'
183+
184+
eq-htpy-extension' :
185+
(e e' : extension-dependent-type' i P f) →
186+
htpy-extension' i f e e' → e ＝ e'
187+
eq-htpy-extension' e e' =
188+
map-inv-equiv (extensionality-extension' e e')
189+
```

0 commit comments

Comments
 (0)