Bracelets
Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.
Created on 2022-06-14.
Last modified on 2023-10-09.
module univalent-combinatorics.bracelets where
Imports
open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types open import foundation.universe-levels open import graph-theory.polygons open import univalent-combinatorics.standard-finite-types
Definition
Bracelets
bracelet : ℕ → ℕ → UU (lsuc lzero) bracelet m n = Σ (Polygon m) (λ X → vertex-Polygon m X → Fin n)
See also
Table of files related to cyclic types, groups, and rings
Recent changes
- 2023-10-09. Egbert Rijke. Navigation tables for all files related to cyclic types, groups, and rings (#823).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).