Contents

1. Agda

2. Type Theory

3. Type Theory 2

4. Boolean Algebra

5. Abstract Algebras

5.1 Orders

5.2 Groups

5.3 Rings

5.4 Fields

6. Category Theory

7. Homotopy Type Theory

8. Algebraic Topology

Extras

α. Applied Type Theory

Γ. Higher Category Theory

Δ. Topos Theory

ψ. Higher Topos Theory

Go up Gitlab Github

import Lang.setup
import Lang.intro
import Lang.dataStructures
import Lang.functions
import Lang.syntaxQuirks
import Lang.other
import Lang.debugging

import Types.introduction
import Types.universe
import Types.relations
import Types.equality
import Types.operations
import Types.product
import Types.functions
import Types.functions2

import Types.proofsAsData
import Types.variations
import Types.patterns
import Types.equational
import Types.equational2

import Logic.introduction
import Logic.logicBasics
import Logic.equality
import Logic.laws
import Logic.decidability

import Algebra.introduction
import Algebra.sets
import Algebra.order
import Algebra.groups
import Algebra.groups2
import Algebra.groupMorphisms
import Algebra.rings
import Algebra.rings2
import Algebra.ringMorphisms
import Algebra.fields
import Algebra.fields2
import Algebra.fieldMorphisms
import Algebra.numbers

import Category.introduction
import Category.category
import Category.morphisms
import Category.functors
import Category.naturalTransformation
import Category.yoneda
import Category.limits

import HoTT.introduction
import HoTT.homotopy

import AlgTopos.introduction
import AlgTopos.topology

import AppliedTypes.introduction
import AppliedTypes.godels_t
import AppliedTypes.system_f
import AppliedTypes.bitcoin
import AppliedTypes.verified_programming

Up