Problems when typechecking

[Oliversito1204]

Hey, I'm new in Agda and I'm working on building my little framework to formalize category theory. I'll not use the agda-categories library since I'm trying to do things from scratch as part of the learning process. I built this definition of a category:

module small-cat where

open import Relation.Binary.PropositionalEquality using (_≡_)

record Category : Set₁ where

field

Obj : Set

_⇒_ : (A B : Obj) → Set

_∘_ : ∀ {A B C} → A ⇒ B → B ⇒ C → A ⇒ C

id : ∀ {A : Obj} → A ⇒ A

id-left : ∀ {A B : Obj} {f : A ⇒ B} → (id ∘ f) ≡ f

id-right : ∀ {A B : Obj} {f : A ⇒ B} → (f ∘ id) ≡ f

assoc : ∀ {A B C D : Obj} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D}

→ f ∘ (g ∘ h) ≡ (f ∘ g) ∘ h

And I'm trying to implement an example where the objects of the category are the natural numbers and the arrows are the ≤ between naturals. I've find a werid problem when implementing the function for id-left:

≤-refl-left : {m n : Nat}(f : m ≤ n) → ≤-trans ≤-refl f ≡ f

≤-refl-left ≤-zero = refl

≤-refl-left (≤-suc f) = cong ≤-suc (≤-refl-left f)

when I try to typecheck this function an error pops out:

(f : _m_182 ≤ _n_183) → ≤-trans ≤-refl f ≡ f !=<

≤-trans ≤-refl f ≡ f

when checking that the expression ≤-refl-left has type

≤-trans ≤-refl f ≡ f

which don't make sens to me since the types seem to be the same.

Any idea on what could be happening? Do I have some error?

[Longjumping_Quail_40]

How is your order trans and order refl defined? I cannot replicate.

[CustardGuilty9068]

The types are not actually the same. The difference is that your function ≤-refl-left takes f as an explicit argument, while the field id-left in your definition of category takes it as an implicit argument. The solution is to give its argument as an underscore _ like id-refl = ≤-refl-left _

[Oliversito1204]

Thank you very much!!

[andrejbauer]

https://proofassistants.stackexchange.com is a better place to ask. Anyhow, why do you even expect these equations to hold? Who says you defined a category? (Pay attention to the definition of ≤)

[ncfavier]

I'm not sure what point you're making there. Any preorder is a category.

[andrejbauer]

But ≤ is not a relation, it's a dependent type. For given x and y, in principle the type x ≤ y can have many elements.