# What is a simple example of transforming some Objects / Arrows in visual, categorical definition into actual Coq code. An MWE recipe that is

Injective object - Wikipedia

In modern category theory literature, the whole definition of injective object can be written as:

Definition. An object $$Q$$ in a category $$C$$ is injective $$\iff$$:

commutes.

Question.

I'm wondering what is the MWE to write this definition in Coq, given that the user (of some hypothetical diagramming app) specifies the diagram + the lhs text of the $$\iff$$ + "commutes".

Ideally I would like to see a technique that is easily adapted to handle other such single-diagram rules (theorems or definitions).

To read the diagram, anything that isn't dotted is $$\forall$$ prefixed internally (implicitly, so you don't see the $$\forall$$) and a dotted line means $$\exists$$. If an object is needing to be an $$\exists$$ instead of a $$\forall$$ prefixed name, then you'd prefix it explicitly with $$\exists$$. Split tail arrow of course means monomorphism.

• There are a few Coq category theory libraries but none of them seem to have projective or injective objects. I would recommend looking at Agda libraries instead: agda-categories has injective morphisms, which you can use to define injective objects. Commented Jul 28 at 11:31
• You haven't defined what a "direct translation" is. I think it's a pretty direct translation; you can of course inline Lifts and Filler (as a $\Sigma$-type) if you like. Commented Jul 28 at 12:15
• I don't expect it to be difficult in any modern proof assistant. Commented Jul 28 at 21:38
• As a tangent, I remember someone (Freyd?) coming up with a uniform system of symbols representing nested quantifiers with diagrams. Does anyone remember who?
– Trebor
Commented Jul 29 at 8:11
• Lean already has injective objects in its mathlib: leanprover-community.github.io/mathlib4_docs/Mathlib/… Commented Jul 29 at 19:18

Since in the comments you say Lean is ok, here is the definition of CategoryTheory.Injective in Mathlib. (I found it with Moogle.ai.)

variable {C : Type u₁} [Category.{v₁} C]

/--
An object J is injective iff every morphism into J can be obtained by extending a monomorphism.
-/
class Injective (J : C) : Prop where
factors : ∀ {X Y : C} (g : X ⟶ J) (f : X ⟶ Y) [Mono f], ∃ h : Y ⟶ J, f ≫ h = g


Follow the above documentation link to explore the definitions/notations of category (Category), morphism (⟶), monomorphism (Mono), and composition (≫) used in the definition.

It is defined as a type class (in Prop) wrapping the forall-exist property you mention. Notice Category, Mono, and (this definition) Injective are type classes. I’m not sure if you are familiar with type classes in Lean, but they are heavily used in the MathLib category theory library. They let you work with the normal presentations of an object, but apply theorems about, in this case, injective objects as long as Lean’s type class system knows your object is an instance of the Injective type class.