Type ?M_1

Stream: new members

[Calle Sönne]

I have the following code:

import category_theory.opposites
import category_theory.limits.shapes.products
import category_theory.limits.shapes.pullbacks

namespace category_theory
namespace category_theory.limits


universes v u

variables {C : Type (u+1)} [𝒞 : large_category C]
variables {D : Type (u+1)} [Dc : large_category D]
variables [products : limits.has_products.{u} D] [pullbacks : limits.has_pullbacks.{u} C]
include 𝒞 Dc products pullbacks

structure covering (U : C) :=
(ι : Type*)
(obj : ι → C)
(hom : Π i, obj i ⟶ U)

def fan1 (U : C) (CU : covering U) := λ (i : CU.ι) (j : CU.ι), limits.pullback (CU.hom i) (CU.hom j)

#check fan1

The #check fan1 gives:

fan1 : Π (U : ?M_1) (CU : covering U), CU.ι → CU.ι → ?M_1

Why does U have type ?M_1 ? Is this because C is a variable? or have I made some weird error in my definitions?

[Kenny Lau]

well supposedly it has the same type as U

[Kenny Lau]

which is a meta variable

[Reid Barton]

Usually it's better to write, for example, #check @fan1

[Kevin Buzzard]

It's because C is {squiggly} so #check without the @ won't print it.