Contents

1. Agda

2. Type Theory

3. Type Theory 2

4. Logic

5. Abstract Algebras

5.1 Orders

5.2 Groups

5.3 Rings

5.4 Fields

6. Homotopy Type Theory

Extras

α. Applied Type Theory

β. Category Theory

δ. Supergeometry

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 AppliedTypes.introduction
import AppliedTypes.godels_t
import AppliedTypes.system_f
import AppliedTypes.bitcoin
import AppliedTypes.verified_programming

import HoTT.introduction
import HoTT.identity

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

Up