Skip to content

Commit

Permalink
remove associativity of standard pullbacks
Browse files Browse the repository at this point in the history
  • Loading branch information
@fredrik-bakke
fredrik-bakke committed Feb 28, 2024
1 parent 07fb076 commit 9e1843b
Showing 1 changed file with 0 additions and 171 deletions.
171 changes: 0 additions & 171 deletions src/foundation/standard-pullbacks.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -271,177 +271,6 @@ triangle-map-commutative-standard-pullback :
triangle-map-commutative-standard-pullback f g c = refl-htpy
```

### Associativity of standard pullbacks

Consider two cospans with a shared vertex

```text
f g h i
A ----> X <---- B ----> Y <---- C,
```

then we can construct their limit using standard pullbacks in two equivalent
ways. We can construct it by first forming the standard pullback of `f` and `g`,
and then forming the standard pullback of the resulting `h ∘ f'` and `i`

```text
(A ×_X B) ×_Y C ---------------------> C
| ⌟ |
| | i
∨ ∨
A ×_X B ---------> B ------------> Y
| ⌟ f' | h
| | g
∨ ∨
A ------------> X,
f
```

or we can first form the pullback of `h` and `i`, and then form the pullback of
`f` and the resulting `g ∘ i'`:

```text
A ×_X (B ×_Y C) --> B ×_Y C ---------> C
| ⌟ | ⌟ |
| | i' | i
| ∨ ∨
| B ------------> Y
| | h
| | g
∨ ∨
A ------------> X.
f
```

We show that both of these constructions are equivalent by giving a definition
of the standard ternary pullback, and show that both are equivalent to it.

**Note:** Associativity with respect to ternary cospans

```text
B
|
| g
∨
A ------> X <------ C
f h
```

is a special case of what we consider here that is recovered by using

```text
f g g h
A ----> X <---- B ----> X <---- C.
```

- See also the following relevant stack exchange question:
[Assocaitivity of pullbacks](https://math.stackexchange.com/questions/2046276/associativity-of-pullbacks).

#### The standard ternary pullback

```agda
module _
{l1 l2 l3 l4 l5 : Level}
{X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
(f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
where

standard-ternary-pullback : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
standard-ternary-pullback =
Σ A (λ a → Σ B (λ b → Σ C (λ c → (f a ＝ g b) × (h b ＝ i c))))
```

#### Computing the left associated iterated standard pullback

```agda
module _
{l1 l2 l3 l4 l5 : Level}
{X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
(f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
where

map-left-associative-standard-pullback :
standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i →
standard-ternary-pullback f g h i
map-left-associative-standard-pullback ((a , b , p) , c , q) =
( a , b , c , p , q)

map-inv-left-associative-standard-pullback :
standard-ternary-pullback f g h i →
standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i
map-inv-left-associative-standard-pullback (a , b , c , p , q) =
( ( a , b , p) , c , q)

is-equiv-map-left-associative-standard-pullback :
is-equiv map-left-associative-standard-pullback
is-equiv-map-left-associative-standard-pullback =
is-equiv-is-invertible
( map-inv-left-associative-standard-pullback)
( refl-htpy)
( refl-htpy)

compute-left-associative-standard-pullback :
standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃
standard-ternary-pullback f g h i
compute-left-associative-standard-pullback =
( map-left-associative-standard-pullback ,
is-equiv-map-left-associative-standard-pullback)
```

#### Computing the right associated iterated dependent pullback

```agda
module _
{l1 l2 l3 l4 l5 : Level}
{X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
(f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
where

map-right-associative-standard-pullback :
standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) →
standard-ternary-pullback f g h i
map-right-associative-standard-pullback (a , (b , c , p) , q) =
( a , b , c , q , p)

map-inv-right-associative-standard-pullback :
standard-ternary-pullback f g h i →
standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
map-inv-right-associative-standard-pullback (a , b , c , p , q) =
( a , (b , c , q) , p)

is-equiv-map-right-associative-standard-pullback :
is-equiv map-right-associative-standard-pullback
is-equiv-map-right-associative-standard-pullback =
is-equiv-is-invertible
( map-inv-right-associative-standard-pullback)
( refl-htpy)
( refl-htpy)

compute-right-associative-standard-pullback :
standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) ≃
standard-ternary-pullback f g h i
compute-right-associative-standard-pullback =
( map-right-associative-standard-pullback ,
is-equiv-map-right-associative-standard-pullback)
```

#### Standard pullbacks are associative

```agda
module _
{l1 l2 l3 l4 l5 : Level}
{X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
(f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
where

associative-standard-pullback :
standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃
standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
associative-standard-pullback =
( inv-equiv (compute-right-associative-standard-pullback f g h i)) ∘e
( compute-left-associative-standard-pullback f g h i)
```

### Pullbacks can be "folded"

Given a standard pullback square
Expand Down

0 comments on commit 9e1843b

Please sign in to comment.