Simple agda tryouts. Contains formalisation of a category.