Skip to content

Commit

Permalink
make pre-commit
Browse files Browse the repository at this point in the history
  • Loading branch information
EgbertRijke committed Oct 22, 2023
1 parent 02fc4ae commit b52146d
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,8 @@ open import synthetic-homotopy-theory.powers-of-loops
## Idea

**Hatcher's [acyclic type](synthetic-homotopy-theory.acyclic-types.md)** is a
higher inductive type [equipped](foundation.structure.md) with a base point and two
[loops](synthetic-homotopy-theory.loop-spaces.md) `a` and `b`, and
higher inductive type [equipped](foundation.structure.md) with a base point and
two [loops](synthetic-homotopy-theory.loop-spaces.md) `a` and `b`, and
[identifications](foundation.identity-types.md) witnessing that `a⁵ = b³` and
`b³ = (ab)²`. This type is acyclic, because the structure on Hatcher's acyclic
type on any loop space is [contractible](foundation.contractible-types.md).
Expand Down

0 comments on commit b52146d

Please sign in to comment.