[refactor] instance declaration by gares · Pull Request #376 · math-comp/hierarchy-builder

gares · 2023-08-01T12:44:06Z

@ptorrx I did push here a cleanup which should simplify the main cleanup

TODO:

handle properly the rex.match ..__ELIM in instance.elpi
- it is called by structure.elpi. it is the generic instance saying that that hom of a MEC are a monoid, that is a regular instance, not to be wrapped. see reexport-wrapper-as-instance
handle parameters in instance.elpi
- should we be smart when the mixin instance to be wrapped and the argument expected by the wrapper need some glue? Eg if the mixin instance has an parameter, we could abstract it upfront and wrap under this binder.
  - we should unify and then abstract unresolved variables
eta-expand context if the mixin is wrapped
syntax in HB.structure to generate the wrapper mixin

gares · 2023-10-05T19:56:24Z

rebasing over master, next time don't pull but git reset origin/refactor-instance

gares · 2023-10-05T19:57:03Z

now cat.v works, but we broke #[hnf] somehow.

gares · 2023-10-06T06:57:14Z

it is also broken in master, so we can ignore it here.

gares · 2023-10-09T12:37:25Z

I had to rebase once again, sorry for the noise.

gares · 2023-10-16T16:25:37Z

HB/common/database.elpi

  ].
 find-max-classes [M|_] _ :- coq.error "HB: cannot find a class containing mixin" M.

+pred is-subject-lifter i:term, o:int, o:classname.


This is wrong if the lifter is casted: (hom : T -> T -> Type) hides (let x : T -> T -> Type := hom in x)
and this code should cross/reduce the let

CohenCyril · 2023-10-25T09:00:57Z

theories/encat.v

+HB.mixin Record IsEnQuiver (V: Monoidal.type) C of Quiver C := {
+    hom_object : C -> C -> V 
+  }.


This is still not accurate. Indeed you would have both hom sets and hom objects. You should have only the latter.

Suggested change

HB.mixin Record IsEnQuiver (V: Monoidal.type) C of Quiver C := {

hom_object : C -> C -> V

}.

HB.mixin Record IsEnQuiver (V: Monoidal.type) C := {

hom_object : C -> C -> V

}.

Indeed in V-enriched cats, hom objects are generalizations of hom sets.

Furthermore, you may weaken the dependency in V here:

Suggested change

HB.mixin Record IsEnQuiver (V: Monoidal.type) C of Quiver C := {

hom_object : C -> C -> V

}.

HB.mixin Record IsEnQuiver (V : Type) C := {

hom_object : C -> C -> V

}.

And gradually add what you actually require in subsequent declarations.

CohenCyril · 2023-10-25T09:03:32Z

theories/encat.v

+Notation "a ~^ b" := (hom_object a b)
+   (at level 99, b at level 200, format "a ~^ b") : cat_scope.


I advocate for reusing the same notation in a different scope. E.g.

Suggested change

Notation "a ~^ b" := (hom_object a b)

(at level 99, b at level 200, format "a ~^ b") : cat_scope.

Notation "a ~> b" := (hom_object a b) : encat_scope.

OK for a distinct name scope, but it might be better not to overload ~>, sometimes we need to use both hom and hom_object

CohenCyril · 2023-10-25T09:08:17Z

theories/encat.v

+Unset Universe Checking.
+#[short(type="dcat")]
+HB.structure Definition DCat : Set := { C of Cat C & H2Cat C }.
+Set Universe Checking.


For the record we discussed that this is not the right definition of double categories because the functoriality of the sources and targets functions $s, t : D_1 \to D_0$ is missing. We gave another definition -- closer to nlab -- but I do not see it here.

I see, I still have to push a few commits

CohenCyril · 2023-10-25T15:29:38Z

theories/encat.v

+(* 2-morphisms *)
+Definition hhom (D: DCat.type) := @hom (@D1 D).


Indeed, given the mismatch between the comment and the name we got it wrong.
We should have

Definition hhom (D : DCat.type) (a b : D) := {x : D1 | s10 x = a /\ t10 x = b }

Yes, I actually had already revised the definition (just pushed it), also because we additionally need an identify functor D0 -> D1, and it seems more natural to define it using the record HHomSet. However, there are some problems which have to do with wrapping and I haven't been able to solve yet

You are right, we actually need an identity D0 -> D1 and a composition functor, D1 *_D0 D1 -> D1.
Maybe the HHomSet way is better but I think we'd rather make the transposition a lifter, put a category structure on the transpose and define two-morphisms like this :

two_hom : forall (x y z t : D), (x ~> y) -> (z ~> t) -> (x ~>_(transpose D) z) -> (y ~>_(transpose D) t) -> Type

CohenCyril · 2023-10-25T15:59:10Z

theories/encat.v

+Definition h2hom (D: DCat.type) := @hom (@HHomSet D).
+
+(* dummy def
+Definition transpose (D: DCat.type) : U := D. *)


This def is not dummy, it's the alias which will receive the transposed structure.

But this seems to say that the transpose is the same category as the original one...

It's the same carrier! But then we may put different instances on it as a category.

Ok, it recasts D of DCat to a Type...

I thought the transpose is the result of swapping horizontal and vertical morphisms...

sure it is.... but as a canonical instance.

gares · 2023-10-27T14:04:32Z

theories/encat.v

+Definition hhom (D: DCat.type) := @hom (@D1 D).
+
+Definition transpose (D: DCat.type) : U := D.
+


Definition hhom (D : DCat.type) (a b : D) := {x : D1 | s10 x = a /\ t10 x = b } HB.instance Definition _ (D : DCat.type) : hasHom (transpose D) := hasHom.Build (@hhom D). ...

CohenCyril · 2023-11-03T20:57:16Z

theories/encat.v

+Record GenComp T (h: T -> T -> U) := {
+    comp_first : @Total2 T h ;  
+    comp_second : @Total2 T h ;
+    comp_adjacent : target comp_first = source comp_second
+}.                                            
+
+(* the set of horizontal morphisms. 
+   HB.tag needed to identify HHomSet as lifter *)
+HB.tag Definition HHomSet (C: hquiver) := Total2 (@hhom C).
+
+Definition HComp (C: hquiver) := GenComp (@hhom C).


Suggested change

Record GenComp T (h: T -> T -> U) := {

comp_first : @Total2 T h ;

comp_second : @Total2 T h ;

comp_adjacent : target comp_first = source comp_second

}.

(* the set of horizontal morphisms.

HB.tag needed to identify HHomSet as lifter *)

HB.tag Definition HHomSet (C: hquiver) := Total2 (@hhom C).

Definition HComp (C: hquiver) := GenComp (@hhom C).

Definition D1 {D0} := Total2 (@hhom D0).

Definition Type_PB {A B : Type} (s : cospan A B) : Type := { x : A * B | left2top x.1 = right2top x.2 }.

Definition D1_prod_D0_D1 D0 := Type_PB (Cospan (source : D1 -> D0) (target : D1 -> D0)).

…structure-instance-from-mixins NOTE: synthesis.under-local-canonical-mixins-of.do! is called twice now

… not working

…ples; there's an unsolved compilation glitch (it will compile the 2nd and 3rd examples separately but not together, depending on which we put first)

… cat

…ion from encatD.v

gares force-pushed the refactor-instance branch from 39361f5 to 336ee12 Compare October 5, 2023 19:56

gares force-pushed the refactor-instance branch from e37c1c7 to a738ac2 Compare October 9, 2023 12:36

gares commented Oct 16, 2023

View reviewed changes

CohenCyril reviewed Oct 25, 2023

View reviewed changes

gares commented Oct 27, 2023

View reviewed changes

CohenCyril reviewed Nov 3, 2023

View reviewed changes

gares and others added 16 commits January 22, 2024 11:31

[refactor] separate add-mixin and make-mixin-canonical

567cee2

[instance] declare-instance -> declare-mixins-from-factory + declare-…

64525c7

…structure-instance-from-mixins NOTE: synthesis.under-local-canonical-mixins-of.do! is called twice now

document exported-op

e0f7895

[instance] test for structure op as subject

8c4071c

comment

6128f44

add comment

1f8ca63

wip-wrapping

2ce532b

minor changes

f12d772

minor changes in instance.elpi

d3273a4

introduced derived instance check in instance.elpi (as a hack); still…

894aff0

… not working

fixed bugs in instance.elpi, compiles

1ecb634

minor changes

cb3d53a

added and updated cmon_enriched_cat.v - this file contains three exam…

2fc6662

…ples; there's an unsolved compilation glitch (it will compile the 2nd and 3rd examples separately but not together, depending on which we put first)

fixed bug in cmonoid_enriched_cat.v

c002312

revised tests/cmonoid_enriched_cat.v

46d5932

cleanup

ed74a82

Paolo Torrini and others added 19 commits January 22, 2024 11:35

updated encatI.v

82e72d6

updated encatI.v; complete definition of double cat based on internal…

f1ab058

… cat

updated encatI.v; cleaning up

9ff3448

updated encatI.v; merged in the strict double category direct definit…

d9c6869

…ion from encatD.v

updated comment in encatI.v

41ad7c1

updated comment in encatI.v

40f762b

changes in encatI0.v

c4724d7

encatI.v and encatI0.v now depend on cat.v

6570167

updated encatI.v

deb0352

updated encatI.v

11e40e2

updated encatI.v

4292494

updated encatI.v

b21e282

restructuring

2167b3d

restructuring

a2cc722

updated encatI.v

e84c91f

updated dependencies

3564fd6

updated dependencies

1ce5b11

updated encatI.v

d94c19f

wip

d88dd20

gares force-pushed the refactor-instance branch from 4c52412 to d88dd20 Compare January 29, 2024 13:04

gares added 10 commits January 29, 2024 20:52

wip

b9cb11f

unsafe(univ) option

f2590ab

wip

e8a680c

wip

18ca7ba

wip

59af016

wip

e19ed85

wip

10b3fb0

wip

af2989f

wip

0cf1c4c

wip

e85441c

		Notation "a ~^ b" := (hom_object a b)
		(at level 99, b at level 200, format "a ~^ b") : cat_scope.

	Notation "a ~^ b" := (hom_object a b)
	(at level 99, b at level 200, format "a ~^ b") : cat_scope.
	Notation "a ~> b" := (hom_object a b) : encat_scope.

		(* 2-morphisms *)
		Definition hhom (D: DCat.type) := @hom (@D1 D).

		Definition hhom (D: DCat.type) := @hom (@D1 D).

		Definition transpose (D: DCat.type) : U := D.

Conversation

gares commented Aug 1, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

gares commented Oct 5, 2023

Uh oh!

gares commented Oct 5, 2023

Uh oh!

gares commented Oct 6, 2023

Uh oh!

gares commented Oct 9, 2023

Uh oh!

Choose a reason for hiding this comment

Uh oh!

CohenCyril Oct 25, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

CohenCyril Oct 25, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

CohenCyril Oct 25, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

CohenCyril Oct 25, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

gares Oct 27, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

CohenCyril Nov 3, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

gares commented Aug 1, 2023 •

edited

Loading

CohenCyril Oct 25, 2023 •

edited

Loading

CohenCyril Oct 25, 2023 •

edited

Loading

CohenCyril Oct 25, 2023 •

edited

Loading

CohenCyril Oct 25, 2023 •

edited

Loading

gares Oct 27, 2023 •

edited

Loading

CohenCyril Nov 3, 2023 •

edited

Loading