⚠ 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.Foundations.Pointed where

open import Cubical.Foundations.Pointed.Base public
open import Cubical.Foundations.Pointed.Properties public
open import Cubical.Foundations.Pointed.FunExt public
open import Cubical.Foundations.Pointed.Homotopy public

open import Cubical.Foundations.Pointed.Homogeneous
Powered by Outcrop
© 2026 Bedrock Institute · content licensed CC BY-NC-SA 4.0 · Source · llms.txt