C should be explicit in Cubical.Categories.Morphism

[barrettj12]

In Cubical.Categories.Morphism, some things are defined inside an anonymous module:

module _ {C : Precategory ℓ ℓ'} where
  ...
  isMonic : (Hom[ x , y ]) → Type (ℓ-max ℓ ℓ')

so that when you access these definitions from the outside world, C is added as an implicit argument:

isMonic : {C : Precategory ℓ ℓ'} → {x y : ob C} → (Hom[ x , y ]) → Type (ℓ-max ℓ ℓ')

The issue is that when trying to use isMonic, Agda seems unable to work out what C should be. I suspect this is related to the fact that Precategory is a record type, and I'm not sure if this is a bug or a feature. Nonetheless, when referring to isMonic, it seems you always have to give C as an argument:

f : C [ x , y ]
...
mon : isMonic {C = C} f

Clearly, this defeats the purpose of making C implicit in the first place. Hence I propose changing the Cubical.Categories.Morphism file to

module _ (C : Precategory ℓ ℓ') where

and all instances of isMonic (and the other definitions) to

isMonic C f

This is technically a breaking change, but I don't think its impact will be too great, and it's easily fixed.

[mortberg]

You're probably right. I think the problem is that isMonic is currently not used anywhere else in the library, so whoever wrote that code just guessed what the implicit arguments should be. Feel free to change it

[barrettj12]

I've opened the PR #634.

With some testing, I determined that some of the definitions could still infer the category, so I've left those implicit. It also seems that C can usually be inferred inside where blocks, but not outside.