global index

• IntBipart source code documentation Construction of the ring of integer numbers from natural numbers as Grothendieck's ring.
• Ackermann source code documentation Ackermann's function in Coq.
• Equality source code documentation Equality in Intensional Type Theory is a groupoid.
• Init source code documentation Some general definitions.
• ListMonad source code documentation
• TakeDrop source code documentation "take" and "drop" from Haskell.Data.List.
• Stream source code documentation This greatly seconds "TakeDrop" module, but for streams instead of lists.
• FunListArg source code documentation Functions with variable number of arguments.
• Subset source code documentation Subset as an unary predicate. Notations for subset union, intersection etc. Poset, lattice, monad of subsets.
• FunExtEq source code documentation Axiom of extensional equality of functions with dependent types.
• CategoryTheory source code documentation Basics of category theory. Category, monad, functor, natural transformation, adjunction, monad.

all together (no makefiles)