⚠ You are viewing the Cubical library. Back to Bedrock
Bedrock
English · 中文 · 日本語
On this page
Menu
Interactive contents
  • Origin
  • Reading routes
  • Dependency graph
  • Glossary
Current route:Common foundations
  • Prelude
  • Impredicativity
  • The classical boundary
  • Choice
  • The object language
  • Structures
  • Semantics
  • The Lévy hierarchy
  • Absoluteness
  • Models of ZF and ZFC
  • Syntax as sets
module Cubical.HITs.SetQuotients where

open import Cubical.HITs.SetQuotients.Base public
open import Cubical.HITs.SetQuotients.Properties public
Powered by Outcrop
© 2026 Bedrock Institute · content licensed CC BY-NC-SA 4.0 · Source · llms.txt