⚠ Cubical ライブラリを閲覧しています。 Bedrock に戻る
Bedrock
English · 中文 · 日本語
このページの内容
メニュー
対話型目次
  • 原点
  • 学習ルート
  • 依存グラフ
  • 用語集
現在のルート:共通の基礎
  • 基礎語彙
  • 非可述性
  • 古典論理との境界
  • 選択原理
  • 対象言語
  • 構造
  • 意味論
  • Lévy 階層
  • 絶対性
  • ZF と ZFC のモデル
  • 集合としての構文
module Cubical.HITs.TypeQuotients where

open import Cubical.HITs.TypeQuotients.Base public
open import Cubical.HITs.TypeQuotients.Properties public
Powered by Outcrop
© 2026 Bedrock Institute · コンテンツは CC BY-NC-SA 4.0 ライセンス · ソース · llms.txt