Hello ! I defined a structure for modeling functors:
HB.mixin Record isFunctor (C D : category) (F : C -> D) := {
actm : forall a b, {hom a, b} -> {hom F a, F b} ;
functor_ext_hom : FunctorLaws.ext actm ;
functor_id_hom : FunctorLaws.id actm ;
functor_comp_hom : FunctorLaws.comp actm
}.
HB.structure Definition Functor C D := {F of isFunctor C D F}.
I'm trying to build an instance and HB is failing for a reason I don't understand. When I write
Check @isFunctor.Build Sets (LModules R)
(@freeLmod R) freeLmod_mor freeLmod_ext freeLmod_id freeLmod_comp.
I get
isFunctor.phant_Build freeLmod_ext freeLmod_id freeLmod_comp
: isFunctor.axioms_ [the category of choiceType] [the category of
lmodType R] (fun T : [the category of choiceType] => { freemod R [T] })
which seem to indicate that everything is ok. But
HB.instance Definition _ :=
@isFunctor.Build Sets (LModules R)
(@freeLmod R) freeLmod_mor freeLmod_ext freeLmod_id freeLmod_comp.
gives the following huge message
Error:
term->gref: input has no global reference: fun `T`
(app
[global (const «Category.sort»),
app
[global (const «TheCanonical.get»),
sort (typ «HB_unnamed_factory_102.u0»),
global (indt «Category.type»), global (indt «Choice.type»),
global (const «Choice_type__canonical__category_Category»),
app
[fun `s` (global (indt «Category.type»)) c0 \
app
[global (indc «TheCanonical.Put»),
sort (typ «HB_unnamed_factory_102.u0»),
global (indt «Category.type»), global (indt «Choice.type»),
app [global (const «Category.sort»), c0], c0],
global (const «Choice_type__canonical__category_Category»)]]]) c0 \
app
[pglobal (const «reverse_coercion»)
«Category.axioms_.u0 freeLmod_mor.u4»,
app
[global (const «Category.sort»),
app
[global (const «TheCanonical.get»),
sort (typ «HB_unnamed_factory_102.u1»),
global (indt «Category.type»),
app [global (indt «GRing.Lmodule.type»), global (const «R»)],
app
[global (const «Lmodule_type__canonical__category_Category»),
global (const «R»)],
app
[fun `s` (global (indt «Category.type»)) c1 \
app
[global (indc «TheCanonical.Put»),
sort (typ «HB_unnamed_factory_102.u1»),
global (indt «Category.type»),
app [global (indt «GRing.Lmodule.type»), global (const «R»)],
app [global (const «Category.sort»), c1], c1],
app
[global (const «Lmodule_type__canonical__category_Category»),
global (const «R»)]]]], sort (typ «freeLmod_mor.u3»),
app
[global (const «msetcompl_freeLmod__canonical__GRing_Lmodule»),
global (const «R»), c0],
app
[global (const «freeLmod»),
app
[global (const «GRing_Ring__to__GRing_Nmodule»), global (const «R»)],
c0]]
Does this makes sense to someone ? Any suggestion ?
Can you printfreeLmod
please?
Sure
freeLmod =
fun (R : nmodType) (T : choiceType) => {fsfun T -> R with 0}
: nmodType -> choiceType -> Type
By the way the code is in https://github.com/hivert/Adjoint
The problem is at the end of https://github.com/hivert/Adjoint/blob/main/theories/examples.v
I expect a eta expansion of freeLmod
is triggered accidentally, and we fail to check this is ok in HB.
NB: you should be able to remove all the [the ...]
I think the eta conversion is triggered because of the typechecking of @freeLmod T
as a choiceType -> choiceType
... Which is unfortunate because that's exacly what we want...
I'll investigate later..
FYI, I manage to solve / workaround the problem with
Definition freeLmod_functor a : lmodType R := {freemod R[a]}.
HB.instance Definition _ :=
@isFunctor.Build Sets (LModules R) freeLmod_functor
freeLmod_mor freeLmod_ext freeLmod_id freeLmod_comp.
That's what I was going to suggest you.
but that's a workaround indeed.
I just got :smiley:
Let F : {functor Sets -> LModules R} := functor_freeLmod R.
Let G : {functor LModules R -> Sets} := forget_LModules_to_Sets R.
Definition adj_FreeLmod_forget : F -| G := AdjointFunctors.mk triL_fm triR_fm.
Last updated: Oct 13 2024 at 01:02 UTC