(X : C) for C : Cat.{u,v}

Stream: Is there code for X?

[Dean Young]

I've noticed I don't get an error if I type X : C instead of X : C.α. Do these mean the same thing?

e.g.

structure example.{u₀,v₀} where
  Obj : Cat.{u₀,v₀}
  Pnt : Obj.α
  CmpObj : Obj.α → Cat.{u₀,v₀}
  CmpHom : (C : Obj.α) →
        (D : Obj.α) →
        (F : C ⭢ D) →
        ((CmpObj C) ⭢ (CmpObj D))

[Eric Wieser]

You can answer this question by comparing variable (X : C) in #check X and variable (X : C.α) in #check X

[Dean Young]

Looks like it checks out.

[Jason Rute]

The reason is explained by @Eric Wieser in your other most recent thread. In this circumstance, there is a coercion from C to its carrier C.α. (And note that otherwise X : C wouldn’t type check since C : Cat is not a type.)

[Dean Young]

@Jason Rute thanks for your help