Zulip Chat Archive

Stream: new members

Topic: Type ?M_1


view this post on Zulip Calle Sönne (Nov 26 2019 at 17:39):

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?

view this post on Zulip Kenny Lau (Nov 26 2019 at 17:41):

well supposedly it has the same type as U

view this post on Zulip Kenny Lau (Nov 26 2019 at 17:41):

which is a meta variable

view this post on Zulip Reid Barton (Nov 26 2019 at 17:46):

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

view this post on Zulip Kevin Buzzard (Nov 26 2019 at 17:59):

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


Last updated: May 06 2021 at 21:09 UTC