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

Recent changes