Analysis of proof that for a category which is also a poset, every diagram commutes

Question

A poset may be defined as a set (axioms of ZFC go here to define "set") and a binary relation (which is taken as a primitive notion in first-order logic), which meets these conditions:

$a R a$

$a R b \wedge b R c \implies a R c$

$a R b \wedge bRa \implies a = b $ (where equality was defined as a predicate in first-order logic as well).

It is said that a category may be a poset, if $Ob(C)$ is the set of elements, and $Ar(C)$ is the binary relation (which is defined as a set of pairs). Such a category is called thin.

The common definition of thin is actually that between any two objects, there is at most one arrow in their respective Hom-set.

I will endeavor to show in Coq that a category is thin iff it is a poset, and also, that in a thin category, every diagram commutes.

I may be completely wrong about what I have said above.

I am working with the following example code, which I did not write, but which I want to study to learn Coq better.

Require Import Relations.

(* Definition of a poset *)
Record Poset (A : Type) : Type := {

This defines a new dependent type called Poset. We can imagine the argument A represents what kind of elements the poset contains.

le : A -> A -> Prop;
le_refl : forall x, le x x;
le_trans : forall x y z, le x y -> le y z -> le x z;
le_antisym : forall x y, le x y -> le y x -> x = y
}.

I am slightly confused about this part. I guess, first, it defines the relation "less than or equal to" as a function type (Boolean). It declares the properties of le, which I understand. But I do not understand how Coq will know that le_refl is meant to be a constraint on le. We never declared x and y as variables. Is this code incorrect, or does Coq infer that le_refl refers to a constraint on potential terms of type le? Thanks very much.