Skip to content

Commit

Permalink
Prose, diagrams, disambiguations
Browse files Browse the repository at this point in the history
  • Loading branch information
@VojtechStep
VojtechStep committed Apr 6, 2024
1 parent 1db9be6 commit d56e29c
Show file tree
Hide file tree
Showing 9 changed files with 128 additions and 49 deletions.
6 changes: 3 additions & 3 deletions src/foundation/double-arrows.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,8 @@ open import foundation.universe-levels

## Idea

A {{#concept "double arrow" Agda=double-arrow}} is a
[pair](foundation.dependent-pair-types.md) of types `A`, `B`
A {{#concept "double arrow" Disambiguation="between types" Agda=double-arrow}}
is a [pair](foundation.dependent-pair-types.md) of types `A`, `B`
[equipped](foundation.structure.md) with a pair of
[maps](foundation.function-types.md) `f, g : A → B`.

Expand Down Expand Up @@ -79,4 +79,4 @@ module _
## See also

- Colimits of double arrows are
[coqualizers](synthetic-homotopy-theory.coequalizers.md)
[coequalizers](synthetic-homotopy-theory.coequalizers.md)
26 changes: 14 additions & 12 deletions src/foundation/equivalences-double-arrows.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,20 +22,22 @@ open import foundation.universe-levels

## Idea

An {{#concept "equivalence of double arrows" Agda=equiv-double-arrow}} from a
[double arrow](foundation.double-arrows.md) `f, g : A → B` to a double arrow
`h, k : X → Y` is a pair of [equivalences](foundation-core.equivalences.md)
`i : A ≃ X` and `j : B ≃ Y`, such that the two squares in
An
{{#concept "equivalence of double arrows" Disambiguation="between types" Agda=equiv-double-arrow}}
from a [double arrow](foundation.double-arrows.md) `f, g : A → B` to a double
arrow `h, k : X → Y` is a pair of
[equivalences](foundation-core.equivalences.md) `i : A ≃ X` and `j : B ≃ Y`,
such that the squares

```text
i
A --------> X
| | ≃ | |
f | | g h | | k
| | | |
∨ ∨ ≃ ∨ ∨
B --------> Y
j
i i
A --------> X A --------> X
| ≃ | | ≃ |
f | | h g | | k
| | | |
∨ ≃ ∨ ∨ ≃ ∨
B --------> Y B --------> Y
j j
```

[commute](foundation-core.commuting-squares-of-maps.md). The equivalence `i` is
Expand Down
25 changes: 13 additions & 12 deletions src/foundation/morphisms-double-arrows.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,20 +21,21 @@ open import foundation.universe-levels

## Idea

A {{#concept "morphism of double arrows" Agda=hom-double-arrow}} from a
[double arrow](foundation.double-arrows.md) `f, g : A → B` to a double arrow
`h, k : X → Y` is a pair of maps `i : A → X` and `j : B → Y`, such that the two
squares in
A
{{#concept "morphism of double arrows" Disambiguation="between types" Agda=hom-double-arrow}}
from a [double arrow](foundation.double-arrows.md) `f, g : A → B` to a double
arrow `h, k : X → Y` is a pair of maps `i : A → X` and `j : B → Y`, such that
the squares

```text
i
A --------> X
| | | |
f | | g h | | k
| | | |
∨ ∨ ∨ ∨
B --------> Y
j
i i
A --------> X A --------> X
| | | |
f | | h g | | k
| | | |
∨ ∨ ∨ ∨
B --------> Y B --------> Y
j j
```

[commute](foundation-core.commuting-squares-of-maps.md). The map `i` is referred
Expand Down
6 changes: 4 additions & 2 deletions src/synthetic-homotopy-theory/coequalizers.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,8 +33,10 @@ i.e. a cofork with the

### All double arrows admit a coequalizer

The {{#concept "canonical coequalizer" Agda=canonical-coequalizer}} may be
obtained as a [pushout](synthetic-homotopy-theory.pushouts.md) of the span
The
{{#concept "canonical coequalizer" Disambiguation="of types" Agda=canonical-coequalizer}}
may be obtained as a [pushout](synthetic-homotopy-theory.pushouts.md) of the
span

```text
∇ [f,g]
Expand Down
12 changes: 6 additions & 6 deletions src/synthetic-homotopy-theory/coforks.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ open import synthetic-homotopy-theory.cocones-under-spans

## Idea

A {{#concept "cofork" Agda=cofork}} of a
A {{#concept "cofork" Disambiguation="of types" Agda=cofork}} of a
[double arrow](foundation.double-arrows.md) `f, g : A → B` with vertext `X` is a
map `e : B → X` together with a [homotopy](foundation.homotopies.md)
`H : e ∘ f ~ e ∘ g`. The name comes from the diagram
Expand Down Expand Up @@ -396,13 +396,13 @@ A [morphism of double arrows](foundation.morphisms-double-arrows.md)
induces a [morphism of span diagrams](foundation.morphisms-span-diagrams.md)

```text
∇ [f,g]
∇ [f,g]
A <------- A + A -------> B
| | |
i | | i + i | j
V V V
X <------- X + X -------> Y
∇ [h,k]
∇ [h,k]
```

```agda
Expand Down Expand Up @@ -474,13 +474,13 @@ induces an
[equivalence of span diagrams](foundation.equivalences-span-diagrams.md)

```text
∇ [f,g]
∇ [f,g]
A <------- A + A -------> B
| | |
i | ≃ ≃ | i + i ≃ | j
V V V
∨ ∨ ∨
X <------- X + X -------> Y
∇ [h,k]
∇ [h,k]
```

```agda
Expand Down
5 changes: 3 additions & 2 deletions src/synthetic-homotopy-theory/dependent-coforks.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,9 @@ Given a [double arrow](foundation.double-arrows.md) `f, g : A → B`, a
a type family `P : X → 𝒰` over `X`, we may construct _dependent_ coforks on `P`
over `e`.

A {{#concept "dependent cofork" Agda=dependent-cofork}} on `P` over `e` consists
of a dependent map
A
{{#concept "dependent cofork" Disambiguation="of types" Agda=dependent-cofork}}
on `P` over `e` consists of a dependent map

```text
k : (b : B) → P (e b)
Expand Down
46 changes: 41 additions & 5 deletions src/synthetic-homotopy-theory/equivalences-coforks.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,9 @@ Consider two [double arrows](foundation.double-arrows.md) `f, g : A → B` and
[equivalence of double arrows](foundation.equivalences-double-arrows.md)
`e : (f, g) ≃ (h, k)`.

Then an {{#concept "equivalence of coforks" Agda=equiv-cofork}} over `e` is a
triple `(m, H, K)`, with `m : X ≃ Y` an
Then an
{{#concept "equivalence of coforks" Disambiguation="of types" Agda=equiv-cofork}}
over `e` is a triple `(m, H, K)`, with `m : X ≃ Y` an
[equivalence](foundation-core.equivalences.md) of vertices of the coforks, `H` a
[homotopy](foundation-core.homotopies.md) witnessing that the bottom square in

Expand Down Expand Up @@ -72,9 +73,44 @@ datum filling the inside --- we have two stacks of squares
m m
```

glued along `i` and the bottom square, with the coherences of `c` and `c'`
filling the sides, which give us two homotopies `m ∘ c ∘ f ~ c' ∘ k ∘ i`, and we
need to ensure these are homotopic.
which share the top map `i` and the bottom square, and the coherences of `c` and
`c'` filling the sides; that gives us the homotopies

```text
i i
A A A --------> U A --------> U
| | | |
f | f | | h | k
| | | |
∨ ∨ j ∨ ∨
B ~ B --------> V ~ V ~ V
| | | |
c | | c' | c' | c'
| | | |
∨ ∨ ∨ ∨
X --------> Y Y Y Y
m
```

and

```text
i
A A A A --------> U
| | | |
f | g | g | | k
| | | |
∨ ∨ ∨ j ∨
B ~ B ~ B --------> V ~ V
| | | |
c | c | | c' | c'
| | | |
∨ ∨ ∨ ∨
X --------> Y X --------> Y Y Y ,
m m
```

which we require to be homotopic.

## Definitions

Expand Down
49 changes: 43 additions & 6 deletions src/synthetic-homotopy-theory/morphisms-coforks.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,9 +29,11 @@ Consider two [double arrows](foundation.double-arrows.md) `f, g : A → B` and
[morphism of double arrows](foundation.morphisms-double-arrows.md)
`e : (f, g) → (h, k)`.

Then a {{#concept "morphism of coforks" Agda=hom-cofork}} over `e` is a triple
`(m, H, K)`, with `m : X → Y` a map of vertices of the coforks, `H` a
[homotopy](foundation-core.homotopies.md) witnessing that the bottom square in
Then a
{{#concept "morphism of coforks" Disambiguation="of types" Agda=hom-cofork}}
over `e` is a triple `(m, H, K)`, with `m : X → Y` a map of vertices of the
coforks, `H` a [homotopy](foundation-core.homotopies.md) witnessing that the
bottom square in

```text
i
Expand Down Expand Up @@ -68,9 +70,44 @@ datum filling the inside --- we have two stacks of squares
m m
```

glued along `i` and the bottom square, with the coherences of `c` and `c'`
filling the sides, which give us two homotopies `m ∘ c ∘ f ~ c' ∘ k ∘ i`, and we
need to ensure these are homotopic.
which share the top map `i` and the bottom square, and the coherences of `c` and
`c'` filling the sides; that gives us the homotopies

```text
i i
A A A --------> U A --------> U
| | | |
f | f | | h | k
| | | |
∨ ∨ j ∨ ∨
B ~ B --------> V ~ V ~ V
| | | |
c | | c' | c' | c'
| | | |
∨ ∨ ∨ ∨
X --------> Y Y Y Y
m
```

and

```text
i
A A A A --------> U
| | | |
f | g | g | | k
| | | |
∨ ∨ ∨ j ∨
B ~ B ~ B --------> V ~ V
| | | |
c | c | | c' | c'
| | | |
∨ ∨ ∨ ∨
X --------> Y X --------> Y Y Y ,
m m
```

which we require to be homotopic.

## Definitions

Expand Down
2 changes: 1 addition & 1 deletion src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -158,7 +158,7 @@ module _
( up-coequalizer Y)
```

### In an equivalences of coforks, one cofork is a coequalizer if and only if the other is
### In an equivalence of coforks, one cofork is a coequalizer if and only if the other is

In other words, given two coforks connected vertically with equivalences, as in
the following diagram:
Expand Down

0 comments on commit d56e29c

Please sign in to comment.