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

7. Homotopy Type Theory

6. Algebraic Topology

Extras

α. Applied Type Theory

β. Category 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.order
import Algebra.groups
import Algebra.groups2
import Algebra.morphisms
import Algebra.rings
import Algebra.rings2
import Algebra.fields
import Algebra.fields2
import Algebra.numbers

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