Update src/foundation/copartial-elements.lagda.md

Co-authored-by: Fredrik Bakke <[email protected]>
UniMath · Dec 6, 2023 · 1c816f7 · 1c816f7
1 parent da97d9b
commit 1c816f7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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