Skip to content

Commit

Permalink
pre-commit
Browse files Browse the repository at this point in the history
  • Loading branch information
VojtechStep committed Apr 6, 2024
1 parent b8a5bc6 commit da9c390
Show file tree
Hide file tree
Showing 2 changed files with 12 additions and 8 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,8 @@ open import synthetic-homotopy-theory.sequential-diagrams
A
{{#concept "cocone" Disambiguation="sequential diagram" Agda=cocone-sequential-diagram}}
under a [sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md)
`(A, a)` with codomain `X : 𝒰` consists of a family of maps `iβ‚™ : A n β†’ C` and
a family of [homotopies](foundation.homotopies.md) `Hβ‚™` asserting that the
`(A, a)` with codomain `X : 𝒰` consists of a family of maps `iβ‚™ : A n β†’ C` and a
family of [homotopies](foundation.homotopies.md) `Hβ‚™` asserting that the
triangles

```text
Expand Down
16 changes: 10 additions & 6 deletions src/synthetic-homotopy-theory/shifts-sequential-diagrams.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -66,8 +66,8 @@ alternative would be to shift all data using
numbers.

However, addition computes only on one side, so we have a choice to make: given
a shift `k`, do we define the `n`-th level of the shifted structure to be
the `n+k`-th or `k+n`-th level of the original?
a shift `k`, do we define the `n`-th level of the shifted structure to be the
`n+k`-th or `k+n`-th level of the original?

The former runs into issues already when defining the shifted sequence, since
`aβ‚™β‚Šβ‚– : Aβ‚™β‚Šβ‚– β†’ Aβ‚β‚™β‚Šβ‚β‚Žβ‚Šβ‚–`, but we need a map of type `Aβ‚™β‚Šβ‚– β†’ Aβ‚β‚™β‚Šβ‚–β‚Žβ‚Šβ‚`, which
Expand Down Expand Up @@ -557,13 +557,17 @@ module _
( c)
( unshift-once-cocone-sequential-diagram A
( shift-once-cocone-sequential-diagram c))
pr1 (inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram c) zero-β„• =
pr1 (inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram c)
zero-β„• =
coherence-cocone-sequential-diagram c zero-β„•
pr1 (inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram c) (succ-β„• n) =
pr1 (inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram c)
(succ-β„• n) =
refl-htpy
pr2 (inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram c) zero-β„• =
pr2 (inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram c)
zero-β„• =
refl-htpy
pr2 (inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram c) (succ-β„• n) =
pr2 (inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram c)
(succ-β„• n) =
right-unit-htpy

module _
Expand Down

0 comments on commit da9c390

Please sign in to comment.