Idris2Doc : Data.CT.Category.Definition

Data.CT.Category.Definition

(source)
Definitions
record Cat : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCat : (0 Obj : Type) -> (0 _ : (Obj -> Obj -> Type)) -> Cat

  Projections:
  
0 .Hom : ({rec:0} : Cat) -> Obj {rec:0} -> Obj {rec:0} -> Type
  
0 .Obj : Cat -> Type
0 .Obj : Cat -> Type
  Totality: total
  Visibility: public export
0 Obj : Cat -> Type
  Totality: total
  Visibility: public export
0 .Hom : ({rec:0} : Cat) -> Obj {rec:0} -> Obj {rec:0} -> Type
  Totality: total
  Visibility: public export
0 Hom : ({rec:0} : Cat) -> Obj {rec:0} -> Obj {rec:0} -> Type
  Totality: total
  Visibility: public export