(** Basics of category theory. Category, monad, functor, natural transformation, adjunction, monad.
Uses axioms:
- extensional equality of functions;
- proof-irrelevance.
Does not use embedding of Haskell classes into Coq; Coq modules.
Notations. Every structure (e.g. functor) is divided into two parts: [x_set] and [x_prop]. [x_set] contains "data" and [x_prop] contains axioms/laws which data satisfies. We need this splitting when comparing structures using [sig_eq].
- ob = object
- mor = morphism
- id = identity morphism
- comp = composition of morphisms
- fr = functor
- nt = natural transformation
- md = monad
- adj = adjunction *)
Require Import Coq.Logic.ProofIrrelevance.
Require Beroal.Init.
Require Beroal.FunExtEq.
Set Implicit Arguments.
Definition sig_eq := Beroal.Init.sig_eq proof_irrelevance.
Definition fun_ext_eq := Beroal.FunExtEq.ext_eq_dep.
(** * Category *)
(** [category] does not containt a type of objects. Instead a type of objects is a parameter. Then we define functor category as [category], we do not need to duplicate [category] [Record]. *)
Record category (ob : Type) : Type :=
{ hom : ob -> ob -> Type
; id : forall ob1:ob, hom ob1 ob1
; comp : forall ob1 ob2 ob3:ob, hom ob2