---
title: 泛等结构集合论 (0) 目录
zhihu-tags: Agda, 同伦类型论（HoTT）, 集合论
zhihu-url: https://zhuanlan.zhihu.com/p/646405225
---

# 泛等结构集合论 (0) 目录

> 交流Q群: 893531731  
> 本文源码: [Everything.lagda.md](https://github.com/choukh/USST/blob/main/src/Everything.lagda.md)  
> 高亮渲染: [Everything.html](https://choukh.github.io/USST/Everything.html)  

```agda
{-# OPTIONS --cubical --safe #-}

module Everything where
```

[(1) 泛等基础](https://zhuanlan.zhihu.com/p/643059692)

```agda
import Cubical
```

[(2) 前置知识](https://zhuanlan.zhihu.com/p/649742992)

```agda
import Preliminary
```

[(3) 开胃菜: CH → LEM](https://zhuanlan.zhihu.com/p/643217740)

```agda
import ReverseMath.CH→LEM
```

[(4) 序数的定义及其泛等原理](https://zhuanlan.zhihu.com/p/643453391)

```agda
import Ordinal.Base
```

[(5) 序数的序](https://zhuanlan.zhihu.com/p/644984990)

```agda
import Ordinal.Order
```

[(6) 吃自己: 序数宇宙也是序数](https://zhuanlan.zhihu.com/p/646397707)

```agda
import Ordinal.OrdInOrd
```

[(7) 构造主义阿列夫层级](https://zhuanlan.zhihu.com/p/651332545)

```agda
import Cardinal.Base
```

## 参考文献
1. [The HoTT Book](https://homotopytypetheory.org/book/)
2. [martinescardo/TypeTopology](https://github.com/martinescardo/TypeTopology)
3. [Set-Theoretic and Type-Theoretic Ordinals Coincide](https://arxiv.org/abs/2301.10696)
4. [The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq](https://www.ps.uni-saarland.de/Publications/documents/KirstRech_2021_The-Generalised.pdf)
