a little category theory in Idris
This is an attempt to formalize some elementary category theory in Idris. Let's see how far we get.
Typechecks (mostly, see below) in Idris Version 0.11
Definitions of a category, a functor, a natural transformation.
Defines type of directed graphs
Construction of the free category on a directed graph.
The discrete category on a type: morphisms are the equalities.
Type is a category with maps as morphisms.
A sceleton of the category of finite sets:
Nat is the type of objects.
Hom m n is Vect m (Fin n) (rather than (Fin m) -> (Fin n)) to have function extensionality.
Attempt to model decidable propositions using interfaces. Overlapping implementation... Not used anywhere...
Defines IsProp and proves Uip in some variants.
Preorders (without Categories). May be unnecessary.
Function extensionality axiom. Needed for FuncCat and CatCat.
Functor category ... incomplete.
Category of categories ... incomplete.
Helper functions to establish the equivalence of dependent functions on Sigma-Types and dependent functions of several variables