From 1c816f78c8d80a4fc21be64ddf2c72f529a4599c Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 6 Dec 2023 18:04:54 -0500
Subject: [PATCH] Update src/foundation/copartial-elements.lagda.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/foundation/copartial-elements.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/copartial-elements.lagda.md b/src/foundation/copartial-elements.lagda.md
index f4da7e9f53..aa3d0ebd38 100644
--- a/src/foundation/copartial-elements.lagda.md
+++ b/src/foundation/copartial-elements.lagda.md
@@ -20,7 +20,7 @@ open import orthogonal-factorization-systems.closed-modalities
 
 ## Idea
 
-A {{#concept "copartial element"}} of a type `A` is an element of type
+A {{#concept "copartial element" Agda=copartial-element}} of a type `A` is an element of type
 
 ```text
   Σ (Q : Prop), A * Q