From ce8eb7551504c482d7b32717670fda283fdc2215 Mon Sep 17 00:00:00 2001
From: Andre Videla <andre.videla@gmail.com>
Date: Mon, 3 Feb 2025 17:43:14 +0000
Subject: [PATCH] add a constructor to the Category interface

---
 libs/contrib/Control/Category.idr | 1 +
 1 file changed, 1 insertion(+)

diff --git a/libs/contrib/Control/Category.idr b/libs/contrib/Control/Category.idr
index bf59a96d0d..e92c1089eb 100644
--- a/libs/contrib/Control/Category.idr
+++ b/libs/contrib/Control/Category.idr
@@ -5,6 +5,7 @@ import Data.Morphisms
 
 public export
 interface Category (0 cat : obj -> obj -> Type) | cat where
+  constructor MkCategory
   id  : cat a a
   (.) : cat b c -> cat a b -> cat a c