{-# OPTIONS --without-K --exact-split --guardedness #-} module everything where open import category-theory open import category-theory.adjunctions-large-precategories open import category-theory.anafunctors open import category-theory.categories open import category-theory.coproducts-precategories open import category-theory.discrete-categories open import category-theory.endomorphisms-of-objects-categories open import category-theory.epimorphisms-large-precategories open import category-theory.equivalences-categories open import category-theory.equivalences-large-precategories open import category-theory.equivalences-precategories open import category-theory.exponential-objects-precategories open import category-theory.functors-categories open import category-theory.functors-large-precategories open import category-theory.functors-precategories open import category-theory.groupoids open import category-theory.homotopies-natural-transformations-large-precategories open import category-theory.initial-objects-precategories open import category-theory.isomorphisms-categories open import category-theory.isomorphisms-large-precategories open import category-theory.isomorphisms-precategories open import category-theory.large-categories open import category-theory.large-precategories open import category-theory.monomorphisms-large-precategories open import category-theory.natural-isomorphisms-categories open import category-theory.natural-isomorphisms-large-precategories open import category-theory.natural-isomorphisms-precategories open import category-theory.natural-numbers-object-precategories open import category-theory.natural-transformations-categories open import category-theory.natural-transformations-large-precategories open import category-theory.natural-transformations-precategories open import category-theory.opposite-precategories open import category-theory.precategories open import category-theory.precategory-of-functors open import category-theory.pregroupoids open import category-theory.products-of-precategories open import category-theory.products-precategories open import category-theory.pullbacks-precategories open import category-theory.sieves-categories open import category-theory.slice-precategories open import category-theory.terminal-objects-precategories open import commutative-algebra open import commutative-algebra.binomial-theorem-commutative-rings open import commutative-algebra.binomial-theorem-commutative-semirings open import commutative-algebra.boolean-rings open import commutative-algebra.commutative-rings open import commutative-algebra.commutative-semirings open import commutative-algebra.dependent-products-commutative-rings open import commutative-algebra.dependent-products-commutative-semirings open import commutative-algebra.discrete-fields open import commutative-algebra.eisenstein-integers open import commutative-algebra.euclidean-domains open import commutative-algebra.function-commutative-rings open import commutative-algebra.function-commutative-semirings open import commutative-algebra.gaussian-integers open import commutative-algebra.homomorphisms-commutative-rings open import commutative-algebra.homomorphisms-commutative-semirings open import commutative-algebra.ideals-commutative-rings open import commutative-algebra.ideals-commutative-semirings open import commutative-algebra.ideals-generated-by-subsets-commutative-rings open import commutative-algebra.integral-domains open import commutative-algebra.invertible-elements-commutative-rings open import commutative-algebra.isomorphisms-commutative-rings open import commutative-algebra.local-commutative-rings open import commutative-algebra.maximal-ideals-commutative-rings open import commutative-algebra.nilradical-commutative-rings open import commutative-algebra.nilradicals-commutative-semirings open import commutative-algebra.powers-of-elements-commutative-rings open import commutative-algebra.powers-of-elements-commutative-semirings open import commutative-algebra.precategory-of-commutative-rings open import commutative-algebra.precategory-of-commutative-semirings open import commutative-algebra.prime-ideals-commutative-rings open import commutative-algebra.radical-ideals-commutative-rings open import commutative-algebra.radicals-of-ideals-commutative-rings open import commutative-algebra.subsets-commutative-rings open import commutative-algebra.subsets-commutative-semirings open import commutative-algebra.sums-commutative-rings open import commutative-algebra.sums-commutative-semirings open import commutative-algebra.trivial-commutative-rings open import commutative-algebra.zariski-topology open import elementary-number-theory open import elementary-number-theory.absolute-value-integers open import elementary-number-theory.ackermann-function open import elementary-number-theory.addition-integer-fractions open import elementary-number-theory.addition-integers open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.addition-rationals open import elementary-number-theory.arithmetic-functions open import elementary-number-theory.based-induction-natural-numbers open import elementary-number-theory.based-strong-induction-natural-numbers open import elementary-number-theory.bezouts-lemma-integers open import elementary-number-theory.bezouts-lemma-natural-numbers open import elementary-number-theory.binomial-coefficients open import elementary-number-theory.binomial-theorem-integers open import elementary-number-theory.binomial-theorem-natural-numbers open import elementary-number-theory.bounded-sums-arithmetic-functions open import elementary-number-theory.catalan-numbers open import elementary-number-theory.cofibonacci open import elementary-number-theory.collatz-bijection open import elementary-number-theory.collatz-conjecture open import elementary-number-theory.commutative-ring-of-integers open import elementary-number-theory.commutative-semiring-of-natural-numbers open import elementary-number-theory.congruence-integers open import elementary-number-theory.congruence-natural-numbers open import elementary-number-theory.decidable-dependent-function-types open import elementary-number-theory.decidable-total-order-natural-numbers open import elementary-number-theory.decidable-types open import elementary-number-theory.difference-integers open import elementary-number-theory.dirichlet-convolution open import elementary-number-theory.distance-integers open import elementary-number-theory.distance-natural-numbers open import elementary-number-theory.divisibility-integers open import elementary-number-theory.divisibility-modular-arithmetic open import elementary-number-theory.divisibility-natural-numbers open import elementary-number-theory.divisibility-standard-finite-types open import elementary-number-theory.equality-integers open import elementary-number-theory.equality-natural-numbers open import elementary-number-theory.euclidean-division-natural-numbers open import elementary-number-theory.eulers-totient-function open import elementary-number-theory.exponentiation-natural-numbers open import elementary-number-theory.factorials open import elementary-number-theory.falling-factorials open import elementary-number-theory.fibonacci-sequence open import elementary-number-theory.finitary-natural-numbers open import elementary-number-theory.finitely-cyclic-maps open import elementary-number-theory.fundamental-theorem-of-arithmetic open import elementary-number-theory.goldbach-conjecture open import elementary-number-theory.greatest-common-divisor-integers open import elementary-number-theory.greatest-common-divisor-natural-numbers open import elementary-number-theory.group-of-integers open import elementary-number-theory.groups-of-modular-arithmetic open import elementary-number-theory.half-integers open import elementary-number-theory.inequality-integer-fractions open import elementary-number-theory.inequality-integers open import elementary-number-theory.inequality-natural-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.inequality-standard-finite-types open import elementary-number-theory.infinitude-of-primes open import elementary-number-theory.initial-segments-natural-numbers open import elementary-number-theory.integer-fractions open import elementary-number-theory.integer-partitions open import elementary-number-theory.integers open import elementary-number-theory.kolakoski-sequence open import elementary-number-theory.lower-bounds-natural-numbers open import elementary-number-theory.maximum-natural-numbers open import elementary-number-theory.maximum-standard-finite-types open import elementary-number-theory.mersenne-primes open import elementary-number-theory.minimum-natural-numbers open import elementary-number-theory.minimum-standard-finite-types open import elementary-number-theory.modular-arithmetic-standard-finite-types open import elementary-number-theory.modular-arithmetic open import elementary-number-theory.monoid-of-natural-numbers-with-addition open import elementary-number-theory.monoid-of-natural-numbers-with-maximum open import elementary-number-theory.multiplication-integers open import elementary-number-theory.multiplication-lists-of-natural-numbers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.multiset-coefficients open import elementary-number-theory.natural-numbers open import elementary-number-theory.nonzero-natural-numbers open import elementary-number-theory.ordinal-induction-natural-numbers open import elementary-number-theory.parity-natural-numbers open import elementary-number-theory.pisano-periods open import elementary-number-theory.powers-integers open import elementary-number-theory.powers-of-two open import elementary-number-theory.prime-numbers open import elementary-number-theory.products-of-natural-numbers open import elementary-number-theory.proper-divisors-natural-numbers open import elementary-number-theory.pythagorean-triples open import elementary-number-theory.rational-numbers open import elementary-number-theory.reduced-integer-fractions open import elementary-number-theory.relatively-prime-integers open import elementary-number-theory.relatively-prime-natural-numbers open import elementary-number-theory.repeating-element-standard-finite-type open import elementary-number-theory.retracts-of-natural-numbers open import elementary-number-theory.sieve-of-eratosthenes open import elementary-number-theory.square-free-natural-numbers open import elementary-number-theory.stirling-numbers-of-the-second-kind open import elementary-number-theory.strict-inequality-natural-numbers open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers open import elementary-number-theory.strong-induction-natural-numbers open import elementary-number-theory.sums-of-natural-numbers open import elementary-number-theory.telephone-numbers open import elementary-number-theory.triangular-numbers open import elementary-number-theory.twin-prime-conjecture open import elementary-number-theory.type-arithmetic-natural-numbers open import elementary-number-theory.unit-elements-standard-finite-types open import elementary-number-theory.unit-similarity-standard-finite-types open import elementary-number-theory.universal-property-natural-numbers open import elementary-number-theory.upper-bounds-natural-numbers open import elementary-number-theory.well-ordering-principle-natural-numbers open import elementary-number-theory.well-ordering-principle-standard-finite-types open import finite-group-theory open import finite-group-theory.abstract-quaternion-group open import finite-group-theory.alternating-concrete-groups open import finite-group-theory.alternating-groups open import finite-group-theory.cartier-delooping-sign-homomorphism open import finite-group-theory.concrete-quaternion-group open import finite-group-theory.delooping-sign-homomorphism open import finite-group-theory.finite-groups open import finite-group-theory.finite-monoids open import finite-group-theory.finite-semigroups open import finite-group-theory.finite-type-groups open import finite-group-theory.groups-of-order-2 open import finite-group-theory.orbits-permutations open import finite-group-theory.permutations-standard-finite-types open import finite-group-theory.permutations open import finite-group-theory.sign-homomorphism open import finite-group-theory.simpson-delooping-sign-homomorphism open import finite-group-theory.subgroups-finite-groups open import finite-group-theory.tetrahedra-in-3-space open import finite-group-theory.transpositions-standard-finite-types open import finite-group-theory.transpositions open import foundation-core open import foundation-core.0-maps open import foundation-core.1-types open import foundation-core.automorphisms open import foundation-core.cartesian-product-types open import foundation-core.coherently-invertible-maps open import foundation-core.commuting-3-simplices-of-homotopies open import foundation-core.commuting-3-simplices-of-maps open import foundation-core.commuting-cubes-of-maps open import foundation-core.commuting-squares-of-maps open import foundation-core.commuting-triangles-of-homotopies open import foundation-core.commuting-triangles-of-maps open import foundation-core.cones-over-cospans open import foundation-core.constant-maps open import foundation-core.contractible-maps open import foundation-core.contractible-types open import foundation-core.coproduct-types open import foundation-core.cospans open import foundation-core.decidable-propositions open import foundation-core.dependent-pair-types open import foundation-core.diagonal-maps-of-types open import foundation-core.discrete-types open import foundation-core.embeddings open import foundation-core.empty-types open import foundation-core.endomorphisms open import foundation-core.equality-cartesian-product-types open import foundation-core.equality-dependent-pair-types open import foundation-core.equality-fibers-of-maps open import foundation-core.equivalence-induction open import foundation-core.equivalence-relations open import foundation-core.equivalences open import foundation-core.faithful-maps open import foundation-core.fibers-of-maps open import foundation-core.function-extensionality open import foundation-core.functions open import foundation-core.functoriality-dependent-function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.functoriality-fibers-of-maps open import foundation-core.functoriality-function-types open import foundation-core.fundamental-theorem-of-identity-types open import foundation-core.homotopies open import foundation-core.identity-systems open import foundation-core.identity-types open import foundation-core.injective-maps open import foundation-core.involutions open import foundation-core.logical-equivalences open import foundation-core.morphisms-cospans open import foundation-core.negation open import foundation-core.path-split-maps open import foundation-core.propositional-maps open import foundation-core.propositions open import foundation-core.pullbacks open import foundation-core.retractions open import foundation-core.sections open import foundation-core.sets open import foundation-core.singleton-induction open import foundation-core.small-types open import foundation-core.subtype-identity-principle open import foundation-core.subtypes open import foundation-core.truncated-maps open import foundation-core.truncated-types open import foundation-core.truncation-levels open import foundation-core.type-arithmetic-cartesian-product-types open import foundation-core.type-arithmetic-dependent-pair-types open import foundation-core.univalence open import foundation-core.universal-property-pullbacks open import foundation-core.universal-property-truncation open import foundation-core.universe-levels open import foundation open import foundation.0-connected-types open import foundation.0-images-of-maps open import foundation.0-maps open import foundation.1-types open import foundation.2-types open import foundation.apartness-relations open import foundation.arithmetic-law-coproduct-and-sigma-decompositions open import foundation.automorphisms open import foundation.axiom-l open import foundation.axiom-of-choice open import foundation.bands open import foundation.binary-embeddings open import foundation.binary-equivalences-unordered-pairs-of-types open import foundation.binary-equivalences open import foundation.binary-functoriality-set-quotients open import foundation.binary-homotopies open import foundation.binary-operations-unordered-pairs-of-types open import foundation.binary-reflecting-maps-equivalence-relations open import foundation.binary-relations open import foundation.binary-transport open import foundation.booleans open import foundation.cantor-schroder-bernstein-escardo open import foundation.cantors-diagonal-argument open import foundation.cartesian-product-types open import foundation.cartesian-products-set-quotients open import foundation.category-of-sets open import foundation.choice-of-representatives-equivalence-relation open import foundation.coherently-invertible-maps open import foundation.commuting-3-simplices-of-homotopies open import foundation.commuting-3-simplices-of-maps open import foundation.commuting-cubes-of-maps open import foundation.commuting-squares-of-identifications open import foundation.commuting-squares-of-maps open import foundation.commuting-triangles-of-homotopies open import foundation.commuting-triangles-of-maps open import foundation.complements-subtypes open import foundation.complements open import foundation.cones-over-cospans open import foundation.conjunction open import foundation.connected-components-universes open import foundation.connected-components open import foundation.connected-maps open import foundation.connected-types open import foundation.constant-maps open import foundation.contractible-maps open import foundation.contractible-types open import foundation.coproduct-decompositions-subuniverse open import foundation.coproduct-decompositions open import foundation.coproduct-types open import foundation.coslice open import foundation.cospans open import foundation.decidable-dependent-function-types open import foundation.decidable-dependent-pair-types open import foundation.decidable-embeddings open import foundation.decidable-equality open import foundation.decidable-equivalence-relations open import foundation.decidable-maps open import foundation.decidable-propositions open import foundation.decidable-relations open import foundation.decidable-subtypes open import foundation.decidable-types open import foundation.dependent-binomial-theorem open import foundation.dependent-pair-types open import foundation.dependent-paths open import foundation.descent-coproduct-types open import foundation.descent-dependent-pair-types open import foundation.descent-empty-types open import foundation.descent-equivalences open import foundation.diagonal-maps-of-types open import foundation.diagonals-of-maps open import foundation.discrete-reflexive-relations open import foundation.discrete-relaxed-sigma-decompositions open import foundation.discrete-sigma-decompositions open import foundation.discrete-types open import foundation.disjunction open import foundation.double-negation open import foundation.double-powersets open import foundation.dubuc-penon-compact-types open import foundation.effective-maps-equivalence-relations open import foundation.embeddings open import foundation.empty-types open import foundation.endomorphisms open import foundation.epimorphisms-with-respect-to-sets open import foundation.epimorphisms-with-respect-to-truncated-types open import foundation.epimorphisms open import foundation.equality-cartesian-product-types open import foundation.equality-coproduct-types open import foundation.equality-dependent-function-types open import foundation.equality-dependent-pair-types open import foundation.equality-fibers-of-maps open import foundation.equivalence-classes open import foundation.equivalence-extensionality open import foundation.equivalence-induction open import foundation.equivalence-relations open import foundation.equivalences-maybe open import foundation.equivalences open import foundation.exclusive-disjunction open import foundation.existential-quantification open import foundation.exponents-set-quotients open import foundation.faithful-maps open import foundation.fiber-inclusions open import foundation.fibered-equivalences open import foundation.fibered-involutions open import foundation.fibered-maps open import foundation.fibers-of-maps open import foundation.full-subtypes open import foundation.function-extensionality open import foundation.functional-correspondences open import foundation.functions open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-coproduct-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.functoriality-fibers-of-maps open import foundation.functoriality-function-types open import foundation.functoriality-propositional-truncation open import foundation.functoriality-set-quotients open import foundation.functoriality-set-truncation open import foundation.functoriality-truncation open import foundation.fundamental-theorem-of-identity-types open import foundation.global-choice open import foundation.hexagons-of-identifications open import foundation.hilberts-epsilon-operators open import foundation.homotopies open import foundation.identity-systems open import foundation.identity-truncated-types open import foundation.identity-types open import foundation.images-subtypes open import foundation.images open import foundation.impredicative-encodings open import foundation.impredicative-universes open import foundation.induction-principle-propositional-truncation open import foundation.inhabited-subtypes open import foundation.inhabited-types open import foundation.injective-maps open import foundation.interchange-law open import foundation.intersections-subtypes open import foundation.involutions open import foundation.isolated-points open import foundation.isomorphisms-of-sets open import foundation.iterated-cartesian-product-types open import foundation.iterating-automorphisms open import foundation.iterating-functions open import foundation.iterating-involutions open import foundation.large-dependent-pair-types open import foundation.large-homotopies open import foundation.large-identity-types open import foundation.large-locale-of-propositions open import foundation.large-locale-of-subtypes open import foundation.law-of-excluded-middle open import foundation.lawveres-fixed-point-theorem open import foundation.lesser-limited-principle-of-omniscience open import foundation.limited-principle-of-omniscience open import foundation.locally-small-types open import foundation.logical-equivalences open import foundation.maybe open import foundation.mere-embeddings open import foundation.mere-equality open import foundation.mere-equivalences open import foundation.monomorphisms open import foundation.morphisms-cospans open import foundation.multisubsets open import foundation.multivariable-correspondences open import foundation.multivariable-decidable-relations open import foundation.multivariable-functoriality-set-quotients open import foundation.multivariable-operations open import foundation.multivariable-relations open import foundation.negation open import foundation.noncontractible-types open import foundation.pairs-of-distinct-elements open import foundation.partial-elements open import foundation.partitions open import foundation.path-algebra open import foundation.path-split-maps open import foundation.perfect-images open import foundation.powersets open import foundation.preidempotent-maps open import foundation.preimages-of-subtypes open import foundation.principle-of-omniscience open import foundation.product-decompositions open import foundation.products-binary-relations open import foundation.products-equivalence-relations open import foundation.products-of-tuples-of-types open import foundation.products-unordered-pairs-of-types open import foundation.products-unordered-tuples-of-types open import foundation.projective-types open import foundation.proper-subtypes open import foundation.propositional-extensionality open import foundation.propositional-maps open import foundation.propositional-resizing open import foundation.propositional-truncations open import foundation.propositions open import foundation.pullback-squares open import foundation.pullbacks open import foundation.raising-universe-levels open import foundation.reflecting-maps-equivalence-relations open import foundation.reflexive-relations open import foundation.relaxed-sigma-decompositions open import foundation.repetitions-of-values open import foundation.repetitions-sequences open import foundation.replacement open import foundation.retractions open import foundation.russells-paradox open import foundation.sections open import foundation.sequences open import foundation.set-presented-types open import foundation.set-quotients open import foundation.set-truncations open import foundation.sets open import foundation.shifting-sequences open import foundation.sigma-decomposition-subuniverse open import foundation.sigma-decompositions open import foundation.singleton-induction open import foundation.singleton-subtypes open import foundation.slice open import foundation.small-maps open import foundation.small-types open import foundation.small-universes open import foundation.split-surjective-maps open import foundation.standard-apartness-relations open import foundation.strongly-extensional-maps open import foundation.structure-identity-principle open import foundation.structure open import foundation.structured-type-duality open import foundation.subterminal-types open import foundation.subtype-duality open import foundation.subtype-identity-principle open import foundation.subtypes open import foundation.subuniverses open import foundation.surjective-maps open import foundation.symmetric-difference open import foundation.symmetric-identity-types open import foundation.symmetric-operations open import foundation.tight-apartness-relations open import foundation.transport open import foundation.trivial-relaxed-sigma-decompositions open import foundation.trivial-sigma-decompositions open import foundation.truncated-equality open import foundation.truncated-maps open import foundation.truncated-types open import foundation.truncation-equivalences open import foundation.truncation-images-of-maps open import foundation.truncation-levels open import foundation.truncations open import foundation.tuples-of-types open import foundation.type-arithmetic-booleans open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-coproduct-types open import foundation.type-arithmetic-dependent-function-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-arithmetic-empty-type open import foundation.type-arithmetic-unit-type open import foundation.type-duality open import foundation.type-theoretic-principle-of-choice open import foundation.unions-subtypes open import foundation.unique-existence open import foundation.uniqueness-image open import foundation.uniqueness-set-quotients open import foundation.uniqueness-set-truncations open import foundation.uniqueness-truncation open import foundation.unit-type open import foundation.unital-binary-operations open import foundation.univalence-action-on-equivalences open import foundation.univalence-implies-function-extensionality open import foundation.univalence open import foundation.univalent-type-families open import foundation.universal-property-booleans open import foundation.universal-property-cartesian-product-types open import foundation.universal-property-coproduct-types open import foundation.universal-property-dependent-pair-types open import foundation.universal-property-empty-type open import foundation.universal-property-fiber-products open import foundation.universal-property-identity-types open import foundation.universal-property-image open import foundation.universal-property-maybe open import foundation.universal-property-propositional-truncation-into-sets open import foundation.universal-property-propositional-truncation open import foundation.universal-property-pullbacks open import foundation.universal-property-set-quotients open import foundation.universal-property-set-truncation open import foundation.universal-property-truncation open import foundation.universal-property-unit-type open import foundation.universe-levels open import foundation.unordered-pairs-of-types open import foundation.unordered-pairs open import foundation.unordered-tuples-of-types open import foundation.unordered-tuples open import foundation.vectors-set-quotients open import foundation.weak-function-extensionality open import foundation.weak-limited-principle-of-omniscience open import foundation.weakly-constant-maps open import graph-theory open import graph-theory.acyclic-undirected-graphs open import graph-theory.circuits-undirected-graphs open import graph-theory.closed-walks-undirected-graphs open import graph-theory.complete-bipartite-graphs open import graph-theory.complete-multipartite-graphs open import graph-theory.complete-undirected-graphs open import graph-theory.connected-undirected-graphs open import graph-theory.cycles-undirected-graphs open import graph-theory.directed-graph-structures-on-standard-finite-sets open import graph-theory.directed-graphs open import graph-theory.edge-coloured-undirected-graphs open import graph-theory.embeddings-directed-graphs open import graph-theory.embeddings-undirected-graphs open import graph-theory.enriched-undirected-graphs open import graph-theory.equivalences-directed-graphs open import graph-theory.equivalences-enriched-undirected-graphs open import graph-theory.equivalences-undirected-graphs open import graph-theory.eulerian-circuits-undirected-graphs open import graph-theory.faithful-morphisms-undirected-graphs open import graph-theory.fibers-directed-graphs open import graph-theory.finite-graphs open import graph-theory.geometric-realizations-undirected-graphs open import graph-theory.hypergraphs open import graph-theory.matchings open import graph-theory.mere-equivalences-undirected-graphs open import graph-theory.morphisms-directed-graphs open import graph-theory.morphisms-undirected-graphs open import graph-theory.neighbors-undirected-graphs open import graph-theory.orientations-undirected-graphs open import graph-theory.paths-undirected-graphs open import graph-theory.polygons open import graph-theory.raising-universe-levels-directed-graphs open import graph-theory.reflecting-maps-undirected-graphs open import graph-theory.reflexive-graphs open import graph-theory.regular-undirected-graphs open import graph-theory.simple-undirected-graphs open import graph-theory.stereoisomerism-enriched-undirected-graphs open import graph-theory.totally-faithful-morphisms-undirected-graphs open import graph-theory.trails-directed-graphs open import graph-theory.trails-undirected-graphs open import graph-theory.undirected-graph-structures-on-standard-finite-sets open import graph-theory.undirected-graphs open import graph-theory.vertex-covers open import graph-theory.voltage-graphs open import graph-theory.walks-directed-graphs open import graph-theory.walks-undirected-graphs open import group-theory open import group-theory.abelian-groups open import group-theory.addition-homomorphisms-abelian-groups open import group-theory.automorphism-groups open import group-theory.cartesian-products-abelian-groups open import group-theory.cartesian-products-concrete-groups open import group-theory.cartesian-products-groups open import group-theory.cartesian-products-monoids open import group-theory.cartesian-products-semigroups open import group-theory.category-of-concrete-groups open import group-theory.category-of-groups open import group-theory.category-of-semigroups open import group-theory.cayleys-theorem open import group-theory.centers-groups open import group-theory.centers-monoids open import group-theory.centers-semigroups open import group-theory.central-elements-groups open import group-theory.central-elements-monoids open import group-theory.central-elements-semigroups open import group-theory.commutative-monoids open import group-theory.commutators-groups open import group-theory.concrete-group-actions open import group-theory.concrete-groups open import group-theory.congruence-relations-abelian-groups open import group-theory.congruence-relations-commutative-monoids open import group-theory.congruence-relations-groups open import group-theory.congruence-relations-monoids open import group-theory.congruence-relations-semigroups open import group-theory.conjugation open import group-theory.contravariant-pushforward-concrete-group-actions open import group-theory.decidable-subgroups open import group-theory.dependent-products-abelian-groups open import group-theory.dependent-products-commutative-monoids open import group-theory.dependent-products-groups open import group-theory.dependent-products-monoids open import group-theory.dependent-products-semigroups open import group-theory.dihedral-group-construction open import group-theory.dihedral-groups open import group-theory.e8-lattice open import group-theory.embeddings-abelian-groups open import group-theory.embeddings-groups open import group-theory.endomorphism-rings-abelian-groups open import group-theory.epimorphisms-groups open import group-theory.equivalences-concrete-group-actions open import group-theory.equivalences-concrete-groups open import group-theory.equivalences-group-actions open import group-theory.equivalences-semigroups open import group-theory.free-concrete-group-actions open import group-theory.free-groups-with-one-generator open import group-theory.full-subgroups open import group-theory.function-abelian-groups open import group-theory.function-commutative-monoids open import group-theory.function-groups open import group-theory.function-monoids open import group-theory.function-semigroups open import group-theory.furstenberg-groups open import group-theory.group-actions open import group-theory.groups open import group-theory.homomorphisms-abelian-groups open import group-theory.homomorphisms-commutative-monoids open import group-theory.homomorphisms-concrete-group-actions open import group-theory.homomorphisms-concrete-groups open import group-theory.homomorphisms-generated-subgroups open import group-theory.homomorphisms-group-actions open import group-theory.homomorphisms-groups open import group-theory.homomorphisms-monoids open import group-theory.homomorphisms-semigroups open import group-theory.inverse-semigroups open import group-theory.invertible-elements-monoids open import group-theory.isomorphisms-abelian-groups open import group-theory.isomorphisms-concrete-groups open import group-theory.isomorphisms-group-actions open import group-theory.isomorphisms-groups open import group-theory.isomorphisms-semigroups open import group-theory.iterated-cartesian-products-concrete-groups open import group-theory.kernels-homomorphisms-concrete-groups open import group-theory.kernels open import group-theory.large-semigroups open import group-theory.loop-groups-sets open import group-theory.mere-equivalences-concrete-group-actions open import group-theory.mere-equivalences-group-actions open import group-theory.monoid-actions open import group-theory.monoids open import group-theory.monomorphisms-concrete-groups open import group-theory.monomorphisms-groups open import group-theory.normal-subgroups-concrete-groups open import group-theory.normal-subgroups open import group-theory.normal-submonoids-commutative-monoids open import group-theory.normal-submonoids open import group-theory.opposite-groups open import group-theory.orbit-stabilizer-theorem-concrete-groups open import group-theory.orbits-concrete-group-actions open import group-theory.orbits-group-actions open import group-theory.orbits-monoid-actions open import group-theory.orders-of-elements-groups open import group-theory.precategory-of-abelian-groups open import group-theory.precategory-of-commutative-monoids open import group-theory.precategory-of-concrete-groups open import group-theory.precategory-of-group-actions open import group-theory.precategory-of-groups open import group-theory.precategory-of-monoids open import group-theory.precategory-of-semigroups open import group-theory.principal-group-actions open import group-theory.principal-torsors-concrete-groups open import group-theory.products-of-elements-monoids open import group-theory.products-of-tuples-of-elements-commutative-monoids open import group-theory.quotient-groups-concrete-groups open import group-theory.quotient-groups open import group-theory.quotients-abelian-groups open import group-theory.representations-monoids open import group-theory.saturated-congruence-relations-commutative-monoids open import group-theory.saturated-congruence-relations-monoids open import group-theory.semigroups open import group-theory.sheargroups open import group-theory.shriek-concrete-group-actions open import group-theory.stabilizer-groups-concrete-group-actions open import group-theory.stabilizer-groups open import group-theory.subgroups-abelian-groups open import group-theory.subgroups-concrete-groups open import group-theory.subgroups-generated-by-subsets-groups open import group-theory.subgroups open import group-theory.submonoids-commutative-monoids open import group-theory.submonoids open import group-theory.subsemigroups open import group-theory.subsets-commutative-monoids open import group-theory.subsets-monoids open import group-theory.substitution-functor-concrete-group-actions open import group-theory.substitution-functor-group-actions open import group-theory.symmetric-concrete-groups open import group-theory.symmetric-groups open import group-theory.torsors open import group-theory.transitive-concrete-group-actions open import group-theory.transitive-group-actions open import group-theory.trivial-subgroups open import group-theory.unordered-tuples-of-elements-commutative-monoids open import higher-group-theory open import higher-group-theory.cartesian-products-higher-groups open import higher-group-theory.equivalences-higher-groups open import higher-group-theory.fixed-points-higher-group-actions open import higher-group-theory.free-higher-group-actions open import higher-group-theory.higher-group-actions open import higher-group-theory.higher-groups open import higher-group-theory.homomorphisms-higher-group-actions open import higher-group-theory.homomorphisms-higher-groups open import higher-group-theory.integers-higher-group open import higher-group-theory.iterated-cartesian-products-higher-groups open import higher-group-theory.orbits-higher-group-actions open import higher-group-theory.subgroups-higher-groups open import higher-group-theory.symmetric-higher-groups open import linear-algebra open import linear-algebra.constant-matrices open import linear-algebra.constant-vectors open import linear-algebra.diagonal-matrices-on-rings open import linear-algebra.functoriality-matrices open import linear-algebra.functoriality-vectors open import linear-algebra.matrices-on-rings open import linear-algebra.matrices open import linear-algebra.multiplication-matrices open import linear-algebra.scalar-multiplication-matrices open import linear-algebra.scalar-multiplication-vectors-on-rings open import linear-algebra.scalar-multiplication-vectors open import linear-algebra.transposition-matrices open import linear-algebra.vectors-on-commutative-rings open import linear-algebra.vectors-on-commutative-semirings open import linear-algebra.vectors-on-euclidean-domains open import linear-algebra.vectors-on-rings open import linear-algebra.vectors-on-semirings open import linear-algebra.vectors open import lists open import lists.arrays open import lists.concatenation-lists open import lists.flattening-lists open import lists.functoriality-lists open import lists.lists-discrete-types open import lists.lists open import lists.permutation-lists open import lists.permutation-vectors open import lists.predicates-on-lists open import lists.quicksort-lists open import lists.reversing-lists open import lists.sort-by-insertion-lists open import lists.sort-by-insertion-vectors open import lists.sorted-lists open import lists.sorted-vectors open import lists.sorting-algorithms-lists open import lists.sorting-algorithms-vectors open import lists.universal-property-lists-wild-monoids open import online-encyclopedia-of-integer-sequences open import online-encyclopedia-of-integer-sequences.oeis open import order-theory open import order-theory.bottom-elements-posets open import order-theory.bottom-elements-preorders open import order-theory.chains-posets open import order-theory.chains-preorders open import order-theory.decidable-posets open import order-theory.decidable-preorders open import order-theory.decidable-subposets open import order-theory.decidable-subpreorders open import order-theory.decidable-total-orders open import order-theory.decidable-total-preorders open import order-theory.dependent-products-large-frames open import order-theory.dependent-products-large-locales open import order-theory.dependent-products-large-meet-semilattices open import order-theory.dependent-products-large-posets open import order-theory.dependent-products-large-preorders open import order-theory.dependent-products-large-suplattices open import order-theory.directed-complete-posets open import order-theory.directed-families open import order-theory.distributive-lattices open import order-theory.finite-posets open import order-theory.finite-preorders open import order-theory.finitely-graded-posets open import order-theory.frames open import order-theory.galois-connections-large-posets open import order-theory.galois-connections open import order-theory.greatest-lower-bounds-large-posets open import order-theory.greatest-lower-bounds-posets open import order-theory.homomorphisms-frames open import order-theory.homomorphisms-large-frames open import order-theory.homomorphisms-large-locales open import order-theory.homomorphisms-large-meet-semilattices open import order-theory.homomorphisms-large-suplattices open import order-theory.homomorphisms-meet-semilattices open import order-theory.homomorphisms-meet-sup-lattices open import order-theory.homomorphisms-sup-lattices open import order-theory.ideals-preorders open import order-theory.interval-subposets open import order-theory.join-semilattices open import order-theory.large-frames open import order-theory.large-locales open import order-theory.large-meet-semilattices open import order-theory.large-meet-subsemilattices open import order-theory.large-posets open import order-theory.large-preorders open import order-theory.large-quotient-locales open import order-theory.large-subframes open import order-theory.large-subposets open import order-theory.large-subpreorders open import order-theory.large-subsuplattices open import order-theory.large-suplattices open import order-theory.lattices open import order-theory.least-upper-bounds-large-posets open import order-theory.least-upper-bounds-posets open import order-theory.locales open import order-theory.locally-finite-posets open import order-theory.lower-bounds-large-posets open import order-theory.lower-bounds-posets open import order-theory.lower-types-preorders open import order-theory.maximal-chains-posets open import order-theory.maximal-chains-preorders open import order-theory.meet-semilattices open import order-theory.meet-suplattices open import order-theory.nuclei-large-locales open import order-theory.order-preserving-maps-large-posets open import order-theory.order-preserving-maps-large-preorders open import order-theory.order-preserving-maps-posets open import order-theory.order-preserving-maps-preorders open import order-theory.posets open import order-theory.powers-of-large-locales open import order-theory.preorders open import order-theory.subposets open import order-theory.subpreorders open import order-theory.suplattices open import order-theory.top-elements-large-posets open import order-theory.top-elements-posets open import order-theory.top-elements-preorders open import order-theory.total-orders open import order-theory.total-preorders open import order-theory.upper-bounds-large-posets open import order-theory.upper-bounds-posets open import organic-chemistry open import organic-chemistry.alcohols open import organic-chemistry.alkanes open import organic-chemistry.alkenes open import organic-chemistry.alkynes open import organic-chemistry.ethane open import organic-chemistry.hydrocarbons open import organic-chemistry.methane open import organic-chemistry.saturated-carbons open import orthogonal-factorization-systems open import orthogonal-factorization-systems.extensions-of-maps open import orthogonal-factorization-systems.factorization-operations-function-classes open import orthogonal-factorization-systems.factorization-operations open import orthogonal-factorization-systems.factorizations-of-maps open import orthogonal-factorization-systems.function-classes open import orthogonal-factorization-systems.higher-modalities open import orthogonal-factorization-systems.lifting-operations open import orthogonal-factorization-systems.lifting-squares open import orthogonal-factorization-systems.lifts-of-maps open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.mere-lifting-properties open import orthogonal-factorization-systems.modal-operators open import orthogonal-factorization-systems.null-types open import orthogonal-factorization-systems.orthogonal-factorization-systems open import orthogonal-factorization-systems.orthogonal-maps open import orthogonal-factorization-systems.pullback-hom open import orthogonal-factorization-systems.reflective-subuniverses open import orthogonal-factorization-systems.sigma-closed-reflective-subuniverses open import orthogonal-factorization-systems.stable-orthogonal-factorization-systems open import orthogonal-factorization-systems.uniquely-eliminating-modalities open import orthogonal-factorization-systems.wide-function-classes open import polytopes open import polytopes.abstract-polytopes open import primitives open import primitives.characters open import primitives.floats open import primitives.machine-integers open import primitives.strings open import real-numbers open import real-numbers.dedekind-real-numbers open import reflection open import reflection.abstractions open import reflection.arguments open import reflection.boolean-reflection open import reflection.definitions open import reflection.fixity open import reflection.group-solver open import reflection.literals open import reflection.metavariables open import reflection.names open import reflection.precategory-solver open import reflection.terms open import reflection.type-checking-monad open import ring-theory open import ring-theory.algebras-rings open import ring-theory.binomial-theorem-rings open import ring-theory.binomial-theorem-semirings open import ring-theory.central-elements-rings open import ring-theory.central-elements-semirings open import ring-theory.congruence-relations-rings open import ring-theory.congruence-relations-semirings open import ring-theory.dependent-products-rings open import ring-theory.dependent-products-semirings open import ring-theory.division-rings open import ring-theory.function-rings open import ring-theory.function-semirings open import ring-theory.homomorphisms-rings open import ring-theory.homomorphisms-semirings open import ring-theory.ideals-generated-by-subsets-rings open import ring-theory.ideals-rings open import ring-theory.ideals-semirings open import ring-theory.idempotent-elements-rings open import ring-theory.invariant-basis-property-rings open import ring-theory.invertible-elements-rings open import ring-theory.isomorphisms-rings open import ring-theory.local-rings open import ring-theory.localizations-rings open import ring-theory.maximal-ideals-rings open import ring-theory.modules-rings open import ring-theory.nil-ideals-rings open import ring-theory.nilpotent-elements-rings open import ring-theory.nilpotent-elements-semirings open import ring-theory.opposite-rings open import ring-theory.powers-of-elements-rings open import ring-theory.powers-of-elements-semirings open import ring-theory.precategory-of-rings open import ring-theory.precategory-of-semirings open import ring-theory.products-rings open import ring-theory.quotient-rings open import ring-theory.radical-ideals-rings open import ring-theory.rings open import ring-theory.semirings open import ring-theory.subsets-rings open import ring-theory.subsets-semirings open import ring-theory.sums-rings open import ring-theory.sums-semirings open import ring-theory.trivial-rings open import set-theory open import set-theory.baire-space open import set-theory.cantor-space open import set-theory.cardinalities open import set-theory.countable-sets open import set-theory.cumulative-hierarchy open import set-theory.infinite-sets open import set-theory.uncountable-sets open import species open import species.cartesian-exponents-species-of-types open import species.cartesian-products-species-of-types open import species.cauchy-composition-species-of-types-in-subuniverses open import species.cauchy-composition-species-of-types open import species.cauchy-exponentials-species-of-types-in-subuniverses open import species.cauchy-exponentials-species-of-types open import species.cauchy-products-species-of-types-in-subuniverses open import species.cauchy-products-species-of-types open import species.cauchy-series-species-of-types-in-subuniverses open import species.cauchy-series-species-of-types open import species.composition-cauchy-series-species-of-types-in-subuniverses open import species.composition-cauchy-series-species-of-types open import species.coproducts-species-of-types-in-subuniverses open import species.coproducts-species-of-types open import species.cycle-index-series-species-of-types open import species.derivatives-species-of-types open import species.dirichlet-products-species-of-types-in-subuniverses open import species.dirichlet-series-species-of-finite-inhabited-types open import species.dirichlet-series-species-of-types-in-subuniverses open import species.equivalences-species-of-types-in-subuniverses open import species.equivalences-species-of-types open import species.exponentials-cauchy-series-of-types-in-subuniverses open import species.exponentials-cauchy-series-of-types open import species.morphisms-finite-species open import species.morphisms-species-of-types open import species.pointing-species-of-types open import species.precategory-of-finite-species open import species.products-cauchy-series-species-of-types-in-subuniverses open import species.products-cauchy-series-species-of-types open import species.products-dirichlet-series-species-of-finite-inhabited-types open import species.products-dirichlet-series-species-of-types-in-subuniverses open import species.small-cauchy-composition-species-of-finite-inhabited-types open import species.small-cauchy-composition-species-of-types-in-subuniverses open import species.species-of-finite-inhabited-types open import species.species-of-finite-types open import species.species-of-inhabited-types open import species.species-of-types-in-subuniverses open import species.species-of-types open import species.unit-cauchy-composition-species-of-types-in-subuniverses open import species.unit-cauchy-composition-species-of-types open import species.unlabeled-structures-species open import structured-types open import structured-types.cartesian-products-types-equipped-with-endomorphisms open import structured-types.central-h-spaces open import structured-types.coherent-h-spaces open import structured-types.commuting-squares-of-pointed-maps open import structured-types.constant-maps-pointed-types open import structured-types.contractible-pointed-types open import structured-types.equivalences-types-equipped-with-endomorphisms open import structured-types.faithful-pointed-maps open import structured-types.fibers-of-pointed-maps open import structured-types.finite-multiplication-magmas open import structured-types.function-magmas open import structured-types.h-spaces open import structured-types.initial-pointed-type-equipped-with-automorphism open import structured-types.involutive-type-of-h-space-structures open import structured-types.involutive-types open import structured-types.iterated-cartesian-products-types-equipped-with-endomorphisms open import structured-types.iterated-pointed-cartesian-product-types open import structured-types.magmas open import structured-types.mere-equivalences-types-equipped-with-endomorphisms open import structured-types.morphisms-coherent-h-spaces open import structured-types.morphisms-magmas open import structured-types.morphisms-types-equipped-with-endomorphisms open import structured-types.pointed-cartesian-product-types open import structured-types.pointed-dependent-functions open import structured-types.pointed-dependent-pair-types open import structured-types.pointed-equivalences open import structured-types.pointed-families-of-types open import structured-types.pointed-homotopies open import structured-types.pointed-maps open import structured-types.pointed-sections open import structured-types.pointed-types-equipped-with-automorphisms open import structured-types.pointed-types open import structured-types.pointed-unit-type open import structured-types.symmetric-elements-involutive-types open import structured-types.symmetric-h-spaces open import structured-types.types-equipped-with-automorphisms open import structured-types.types-equipped-with-endomorphisms open import structured-types.unpointed-maps open import structured-types.wild-groups open import structured-types.wild-loops open import structured-types.wild-monoids open import structured-types.wild-quasigroups open import structured-types.wild-semigroups open import synthetic-homotopy-theory open import synthetic-homotopy-theory.24-pushouts open import synthetic-homotopy-theory.26-descent open import synthetic-homotopy-theory.26-id-pushout open import synthetic-homotopy-theory.27-sequences open import synthetic-homotopy-theory.acyclic-maps open import synthetic-homotopy-theory.acyclic-types open import synthetic-homotopy-theory.cavallos-trick open import synthetic-homotopy-theory.circle open import synthetic-homotopy-theory.cocones-under-spans-of-pointed-types open import synthetic-homotopy-theory.cocones-under-spans open import synthetic-homotopy-theory.cofibers open import synthetic-homotopy-theory.descent-circle open import synthetic-homotopy-theory.double-loop-spaces open import synthetic-homotopy-theory.free-loops open import synthetic-homotopy-theory.functoriality-loop-spaces open import synthetic-homotopy-theory.groups-of-loops-in-1-types open import synthetic-homotopy-theory.hatchers-acyclic-type open import synthetic-homotopy-theory.infinite-complex-projective-space open import synthetic-homotopy-theory.infinite-cyclic-types open import synthetic-homotopy-theory.interval-type open import synthetic-homotopy-theory.iterated-loop-spaces open import synthetic-homotopy-theory.joins-of-types open import synthetic-homotopy-theory.loop-spaces open import synthetic-homotopy-theory.multiplication-circle open import synthetic-homotopy-theory.plus-principle open import synthetic-homotopy-theory.powers-of-loops open import synthetic-homotopy-theory.prespectra open import synthetic-homotopy-theory.pushouts-of-pointed-types open import synthetic-homotopy-theory.pushouts open import synthetic-homotopy-theory.smash-products-of-pointed-types open import synthetic-homotopy-theory.spectra open import synthetic-homotopy-theory.spheres open import synthetic-homotopy-theory.suspensions-of-types open import synthetic-homotopy-theory.triple-loop-spaces open import synthetic-homotopy-theory.universal-cover-circle open import synthetic-homotopy-theory.universal-property-circle open import synthetic-homotopy-theory.universal-property-pushouts open import synthetic-homotopy-theory.wedges-of-pointed-types open import trees open import trees.algebras-polynomial-endofunctors open import trees.bases-directed-trees open import trees.bases-enriched-directed-trees open import trees.coalgebra-of-directed-trees open import trees.coalgebra-of-enriched-directed-trees open import trees.coalgebras-polynomial-endofunctors open import trees.combinator-directed-trees open import trees.combinator-enriched-directed-trees open import trees.directed-trees open import trees.elementhood-relation-coalgebras-polynomial-endofunctors open import trees.elementhood-relation-w-types open import trees.enriched-directed-trees open import trees.equivalences-directed-trees open import trees.equivalences-enriched-directed-trees open import trees.extensional-w-types open import trees.fibers-directed-trees open import trees.fibers-enriched-directed-trees open import trees.functoriality-combinator-directed-trees open import trees.functoriality-fiber-directed-tree open import trees.functoriality-w-types open import trees.indexed-w-types open import trees.induction-w-types open import trees.inequality-w-types open import trees.lower-types-w-types open import trees.morphisms-algebras-polynomial-endofunctors open import trees.morphisms-coalgebras-polynomial-endofunctors open import trees.morphisms-directed-trees open import trees.morphisms-enriched-directed-trees open import trees.multisets open import trees.planar-binary-trees open import trees.polynomial-endofunctors open import trees.raising-universe-levels-directed-trees open import trees.ranks-of-elements-w-types open import trees.rooted-morphisms-directed-trees open import trees.rooted-morphisms-enriched-directed-trees open import trees.rooted-quasitrees open import trees.rooted-undirected-trees open import trees.small-multisets open import trees.submultisets open import trees.transitive-multisets open import trees.underlying-trees-elements-coalgebras-polynomial-endofunctors open import trees.underlying-trees-of-elements-of-w-types open import trees.undirected-trees open import trees.universal-multiset open import trees.w-type-of-natural-numbers open import trees.w-type-of-propositions open import trees.w-types open import type-theories open import type-theories.comprehension-type-theories open import type-theories.dependent-type-theories open import type-theories.fibered-dependent-type-theories open import type-theories.sections-dependent-type-theories open import type-theories.simple-type-theories open import type-theories.unityped-type-theories open import univalent-combinatorics open import univalent-combinatorics.2-element-decidable-subtypes open import univalent-combinatorics.2-element-subtypes open import univalent-combinatorics.2-element-types open import univalent-combinatorics.binomial-types open import univalent-combinatorics.bracelets open import univalent-combinatorics.cartesian-product-types open import univalent-combinatorics.classical-finite-types open import univalent-combinatorics.complements-isolated-points open import univalent-combinatorics.coproduct-types open import univalent-combinatorics.counting-decidable-subtypes open import univalent-combinatorics.counting-dependent-pair-types open import univalent-combinatorics.counting-fibers-of-maps open import univalent-combinatorics.counting-maybe open import univalent-combinatorics.counting open import univalent-combinatorics.cubes open import univalent-combinatorics.cycle-partitions open import univalent-combinatorics.cycle-prime-decomposition-natural-numbers open import univalent-combinatorics.cyclic-types open import univalent-combinatorics.decidable-dependent-function-types open import univalent-combinatorics.decidable-dependent-pair-types open import univalent-combinatorics.decidable-equivalence-relations open import univalent-combinatorics.decidable-propositions open import univalent-combinatorics.decidable-subtypes open import univalent-combinatorics.dedekind-finite-sets open import univalent-combinatorics.dependent-function-types open import univalent-combinatorics.dependent-pair-types open import univalent-combinatorics.discrete-sigma-decompositions open import univalent-combinatorics.distributivity-of-set-truncation-over-finite-products open import univalent-combinatorics.double-counting open import univalent-combinatorics.embeddings-standard-finite-types open import univalent-combinatorics.embeddings open import univalent-combinatorics.equality-finite-types open import univalent-combinatorics.equality-standard-finite-types open import univalent-combinatorics.equivalences-cubes open import univalent-combinatorics.equivalences-standard-finite-types open import univalent-combinatorics.equivalences open import univalent-combinatorics.ferrers-diagrams open import univalent-combinatorics.fibers-of-maps open import univalent-combinatorics.finite-choice open import univalent-combinatorics.finite-connected-components open import univalent-combinatorics.finite-presentations open import univalent-combinatorics.finite-types open import univalent-combinatorics.finitely-presented-types open import univalent-combinatorics.function-types open import univalent-combinatorics.image-of-maps open import univalent-combinatorics.inequality-types-with-counting open import univalent-combinatorics.inhabited-finite-types open import univalent-combinatorics.injective-maps open import univalent-combinatorics.involution-standard-finite-types open import univalent-combinatorics.isotopies-latin-squares open import univalent-combinatorics.kuratowsky-finite-sets open import univalent-combinatorics.latin-squares open import univalent-combinatorics.main-classes-of-latin-hypercubes open import univalent-combinatorics.main-classes-of-latin-squares open import univalent-combinatorics.maybe open import univalent-combinatorics.necklaces open import univalent-combinatorics.orientations-complete-undirected-graph open import univalent-combinatorics.orientations-cubes open import univalent-combinatorics.partitions open import univalent-combinatorics.petri-nets open import univalent-combinatorics.pi-finite-types open import univalent-combinatorics.pigeonhole-principle open import univalent-combinatorics.presented-pi-finite-types open import univalent-combinatorics.quotients-finite-types open import univalent-combinatorics.ramsey-theory open import univalent-combinatorics.repetitions-of-values-sequences open import univalent-combinatorics.repetitions-of-values open import univalent-combinatorics.retracts-of-finite-types open import univalent-combinatorics.sequences-finite-types open import univalent-combinatorics.set-quotients-of-index-two open import univalent-combinatorics.sigma-decompositions open import univalent-combinatorics.skipping-element-standard-finite-types open import univalent-combinatorics.small-types open import univalent-combinatorics.standard-finite-pruned-trees open import univalent-combinatorics.standard-finite-trees open import univalent-combinatorics.standard-finite-types open import univalent-combinatorics.steiner-systems open import univalent-combinatorics.steiner-triple-systems open import univalent-combinatorics.sums-of-natural-numbers open import univalent-combinatorics.surjective-maps open import univalent-combinatorics.symmetric-difference open import univalent-combinatorics.trivial-sigma-decompositions open import univalent-combinatorics.type-duality open import univalent-combinatorics.unions-subtypes open import univalent-combinatorics.universal-property-standard-finite-types open import univalent-combinatorics.unlabeled-partitions open import univalent-combinatorics.unlabeled-rooted-trees open import univalent-combinatorics.unlabeled-trees open import universal-algebra open import universal-algebra.abstract-equations-over-signatures open import universal-algebra.algebraic-theories open import universal-algebra.algebraic-theory-of-groups open import universal-algebra.algebras-of-theories open import universal-algebra.congruences open import universal-algebra.homomorphisms-of-algebras open import universal-algebra.kernels open import universal-algebra.models-of-signatures open import universal-algebra.quotient-algebras open import universal-algebra.signatures open import universal-algebra.terms-over-signatures