⚠ You are viewing the Cubical library. Back to Bedrock
Bedrock
English · 中文 · 日本語
On this page
Menu
Reading guide
  • Reading routes
  • Dependency map
  • Milestones
  • Glossary
Modules
  • Base
    • Prelude
    • Impredicativity
    • The classical boundary
    • Choice
  • FOL
    • The object language
    • Structures
    • Semantics
    • The Lévy hierarchy
    • Absoluteness
    • Models of ZF and ZFC
    • Manipulation
      • Mapping constants
      • Variable renaming
      • Constant relabelling
      • Relativization
      • Constant bounding
      • Constants by occurrence
      • Parameter abstraction
    • Syntax as sets
  • V
    • The cumulative hierarchy
    • Small truth values in the cumulative hierarchy
    • The cumulative hierarchy models ZF and ZFC
    • Coding inside the cumulative hierarchy
    • Small presentations of sets
    • Cantor–Schröder–Bernstein for small presentations
    • The Mostowski collapse
  • L
    • Definable subsets of a set
    • The constructible hierarchy and universe
    • Ordinal closure and finite ordinals
    • Von Neumann rank
    • Ordinal
      • Ordinals are linearly ordered by membership
      • Locating ordinals in the constructible hierarchy
      • Ordinal indices, the Gödel pair order, and finite indices
    • The index of the least constructible stage
    • Axioms
      • The basic axioms
      • Separation and replacement, bounded
      • Separation and replacement, in full
      • The power set in L
      • The numeral chain
      • The axiom of infinity in L
    • Existential reflection into a constructible stage
    • Reflection for an arbitrary formula
    • From ambient formulas to formulas over L
    • Coding
      • Formulas for singletons and pairs
      • Finite environments as set-coded graphs
      • Coding formulas over the constructible model
      • Formula expressions for coded recursion
      • Subcode-closed domains
      • Rank descent through coded pairs
      • Constructible codes and subformula trees
      • Closure under subformulas
      • The set of fixed-length environments
      • Satisfaction by recursion on formulas
      • Satisfaction and the recursion value
      • Satisfaction tables over subformulas
      • Agreement of environment sets
      • Closing a code slot under its seven constructors
      • Recognizing well-formed constructor keys
      • Recovering formulas from codes
      • Numerals in a successor-closed ordinal stage
      • Quantifying over coded pairs and finite formula families
      • The environment tower
      • The set of all formula codes
      • Describing the closed domain of formula codes
      • Describing the satisfaction table
      • The alphabet of formula codes
      • Reading and validating the satisfaction clauses
      • Pinning recursion on a subcode-closed domain
      • The satisfaction graph formula
      • Uniform satisfaction over all codes
      • A formula for the definable power set
      • A sequence for the constructible hierarchy
      • Coded injections
      • An internal graph of uniform satisfaction
      • Soundness and completeness of the closed code domain
    • Internalizing recursive definitions in L
    • Recursion
      • Graphs of recursive definitions
    • The constructible hierarchy inside L
    • Choice
      • The first stage meeting a set
      • Well-orders on finite stages
      • Canonical names for successor-stage members
      • Well-orders on all stages
      • Formulas for name comparison
      • An internal table of stage orders
      • Adequacy of the stage-order description
      • Adequacy of name comparison
      • The limit-stage order inside L
      • An internal family of earliest-disagreement relations
      • The internal stage-order relation
      • Choice by a transversal
    • WellOrder
      • Strict well-orders and least-element search
    • The constructible universe models ZFC
    • Cardinals and coded injections inside L
    • Turning a definable injection into an internal code
    • Composition and inclusion of coded injections
    • The generalized continuum hypothesis inside L
    • Cantor–Schröder–Bernstein inside L
    • Collapsing a transitive well-founded relation
    • An ordinal L-cardinal above every L-cardinal
    • GCH
      • Assembling GCH from four internal bounds
      • A Δ₀ description of the satisfaction table
      • A Δ₀ description of the definable power set
      • Adequate stages for the GCH argument
      • ω-recursion inside the constructible universe
      • Building and collapsing a Skolem hull
      • A Δ₀ description of the constructible hierarchy
      • Transferring structure through condensation
      • Ordinals below a successor cardinal inject into its base
      • Constructing order types inside L
      • Choosing a cardinal representative for an ordinal
      • The square law for infinite L-cardinals
      • The least-witness map inside a constructible stage
      • Injecting the successor cardinal into the power set
      • Coding finite sequences below an infinite ordinal
      • The counting tools for infinite constructible stages
      • Locating the hull and its collapse inside L
      • Counting a Skolem hull from a counted start
      • Injecting an infinite constructible stage into its index
      • Bounded subsets appear at controlled stages
      • The constructible universe satisfies GCH
module Cubical.Algebra.Semigroup where

open import Cubical.Algebra.Semigroup.Base public
Rendered with a generator adapted from the 1lab (AGPL-3.0).
llms.txt
© 2026 Bedrock Institute · content licensed CC BY-NC-SA 4.0 · Source