Hofmann-Streicher universes for graphs and globular types #1196

EgbertRijke · 2024-10-13T19:52:54Z

This pull request is part of the formalization of higher category theory project with Ivan. Here we construct Hofmann-Streicher universes for:

directed graphs
reflexive directed graphs
globular types
reflexive globular types

Additionally, we add some computations for dependent Pi-types in those toposes, and some infrastructure is streamlined.

…endendent globular types with morphisms into the universal globular type

EgbertRijke · 2024-10-15T16:47:54Z

I have now proven the duality theorem for directed graphs (analogous to type duality), which is the toy-result of what I'm really after for globular types.

src/structured-types/wild-category-of-pointed-types.lagda.md

fredrik-bakke · 2024-10-15T19:02:38Z

I still find it very frustrating that pre-commit produces such a mess on commented code :(

Unfortunately, it is a choice between two evils, unless we want to start playing with making changes to the auto-formatter. Luckily your issue can be avoided by being mindful of how one comments code.

Your best course of action here is to look through the commit history for a point in time where the code wasn't jumbled. Alternatively, you could try something like text replacing -- with \n, but then you will have to manually indent things again after.

fredrik-bakke · 2024-10-18T16:23:13Z

Hiya! It looks like this PR is perhaps growing a bit outside the scope of the original goal. While I don't doubt the changes are relevant to one another, do you think it perhaps would be possible to split it up into some more manageable chunks for the eventual review?

EgbertRijke · 2024-11-15T20:02:46Z

There's a difference in our stylistic approaches when it comes to copattern-matched definitions that I believe we need to resolve before this PR can be merged. Otherwise, we will perpetually undo each other's work. It is my opinion that the λ where syntax is superior to our current prefix style. I have many reasons that I will try to explain to myself and you.

The λ where syntax reduces verbosity in a way that, in my opinion, only improves readability. Especially for long entry names. It is my view that our current style guidelines for line wrapping and indentation are in direct conflict with the prefix copattern matching style when the entry names are long or the record is moderately nested. This entails excessive amounts of line breaks, parenthesis levels and/or indentation levels.
The repetition of the entry name for every field of a record serves to add no information to a definition, and clutters the view to a problematic extent when the entry name is long.
The .XXX pattern can be statically highlighted, making the code easier to read even before it typechecks (or if one doesn't use Agda's highlighting information, which you may not want to do if you're using VS Code, or if you're reading the code on GitHub).
While the λ where syntax is new, I think it should be abundantly clear and intuitive to the reader after only a few exposures to it, and I don't believe it should be a point of continued confusion.

A worked-out comparison

Compare the following two equivalent pieces of Agda formalization

my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory :
 some-type → some-other-type ...
my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory
  x =
  λ where
  .map y z →
    blablablabla x blablablablb z y
  .has-property-map w .stuff →
    blablablabla2
  .has-property-map w .structure →
    blablablabla3

to

my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory :
 some-type → some-other-type ...
map
  ( my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory
      x)
  y z =
  blablablabla x blablablablb z y
stuff
  ( has-property-map
    ( my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory
      x)
    w) =
  blablablabla2
structure
  ( has-property-map
    ( my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory
      x)
    w) =
  blablablabla3

The former is clearly more readable and well-structured than the latter. Of course, you will argue that the latter should be refactored to something like the following:

module _
  (x : some-type)
  where

  map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory :
    some-other-type
  map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory
    y z =
    blablablabla x blablablablb z y

module _
  (x : some-type) (w : ??)
  where

  stuff-has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory :
    .....
  stuff-has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory =
    blablablabla2

  structure-has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory :
    ....
  structure-has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory =
    blablablabla3

  has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory :
    ...
  stuff
    has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory =
    stuff-has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory  
  structure
    has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory =
    structure-has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory  

module _
  (x : some-type)
  where

  my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory :
    some-other-type ...
  map
    my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory =
    map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory
      x
  has-property-map
    my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory =
    has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory
      x

Which is fair, I don't argue against that. And in the process, we extract some definitions that may be useful in their own right. However, my proposed stylistic change does not conflict with this. And, it still reduces verbosity in the last two definitions:

module _
  (x : some-type) (w : ??)
  where
  
  has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory :
    ...
  has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory =
    λ where
    .stuff →
      stuff-has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory  
    .structure →
      structure-has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory  

module _
  (x : some-type)
  where

  my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory :
    some-other-type ...
  my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory =
    λ where
    .map →
      map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory  
        x
    .has-property-map →
      has-property-map-my-very-long-agda-entry-definition-name-that-is-very-long-and-is-in-the-namespace-of-Noncoherent-Large-Wild-Higher-Precategory
        x

I don't understand why we can't adopt a style that affords us the option to not have to refactor every definition into its atoms every time – all while the only downside seems to be that it changes the ordering from prefix to postfix.

I think the issue I'm trying to highlight here is particularly prominent in the formalization of wild category theory and worry that the issue will grow if we do not take action to reduce the verbosity of our formalizations of wild categories.

I appreciate your point but I don't buy into the lamda-where notation as fully as you do. Our guidelines say that we prefer regular pattern matching over lambda-where patterns.

In particular in combination with coinductive types I think the lambda-where notation departs significantly from common mathematical practice, while the standard pattern matching just reads as a judgmental equality that holds when you apply a destructor to a term.

For example, the lambda-where notation permits and encourages weird looking code salads like:

λ where
  .pr1 zero-N → ...

where destructors are mixed with constructors in line of code just looks crazy, to be honest.

It is so much better to read

pr1 long-name-of-a-thing zero-N = ...

where the projection and the arguments are in a sensible order.

I think the current guidelines are sensible in not completely rejecting lambda-where notation while stating a preference for the other pattern-matching approaches. I hope too that we won't be undoing each other's work because of a difference in stylistic preferences.

This PR should be merged before #1196. I have only moved files and adjusted imports and markdown links accordingly, in an attempt to preserve the credits to the content creators.

scripts/preprocessor_git_metadata.py

EgbertRijke · 2024-11-20T12:55:27Z

I believe I've addressed all the review comments, except one where I asked if it is ok to leave it unaddressed.

fredrik-bakke

I can't comment without finishing my review 😩

fredrik-bakke · 2024-11-16T15:28:29Z

src/structured-types/superglobular-types.lagda.md

+  e₂ : {x y : G₀} {s t : H₀ x y} {u v : H₁
+       H₂ (refl G x) (refl G y) u v ≃ G₃ (e₁ u) (e₁ v)


this is misformatted

fredrik-bakke · 2024-11-20T13:17:10Z

src/structured-types/large-lax-reflexive-globular-maps.lagda.md

+
+from the image of the reflexivity cell at `x` in `G` to the reflexivity cell at
+`f₀ x`, such that the [globular map](structured-types.globular-maps.md)
+`f' : G' x y → H' (f₀ x) (f₀ y)` is


Yep, that's fine. I'll have a final read through later tonight 😁👍

fredrik-bakke · 2024-11-20T18:41:11Z

src/globular-types/binary-dependent-globular-types.lagda.md

+record
+  Binary-Dependent-Globular-Type
+    {l1 l2 l3 l4 : Level} (l5 l6 : Level)
+    (G : Globular-Type l1 l2) (H : Globular-Type l3 l4) :


Is there a reason H can't be dependent over G?

fredrik-bakke · 2024-11-20T18:42:11Z

src/globular-types/binary-dependent-reflexive-globular-types.lagda.md

+
+A binary dependent globular type `K` over reflexive globular types `G` and `H`
+is said to be
+{{#concept "reflexive" Disambiguation="binary dependent globular type"}} if it


Add pointer to Agda definition

fredrik-bakke

Crazy stuff! But next time, maybe try and keep the PR a little smaller 😬

src/globular-types/composition-structure-globular-types.lagda.md

fredrik-bakke · 2024-11-20T19:59:37Z

src/globular-types/large-transitive-globular-maps.lagda.md

+    (H : Large-Transitive-Globular-Type α2 β2)
+    (f : large-globular-map-Large-Transitive-Globular-Type γ G H) : UUω
+  where
+  coinductive


This definition doesn't require the coinductive flag since it is not coinductive.

The same is probably true for large ((co)lax) reflexive globular maps as well.

src/globular-types/points-reflexive-globular-types.lagda.md

fredrik-bakke · 2024-11-20T20:24:13Z

src/globular-types/reflexive-globular-equivalences.lagda.md

+    preserves-refl-globular-map G H (globular-map-globular-equiv e)
+```
+
+### Equivalences between globular types


Suggested change

### Equivalences between globular types

### Reflexive equivalences between reflexive globular types

fredrik-bakke · 2024-11-20T20:26:53Z

src/globular-types/reflexive-globular-types.lagda.md

+- [Reflexive globular maps](globular-types.reflexive-globular-maps.md)
+- [Noncoherent wild higher precategories](wild-category-theory.noncoherent-wild-higher-precategories.md)
+  are globular types that are both reflexive and
+  [transitive](globular-types.transitive-globular-types.md).


should noncoherent wild higher precategories rather be reflexive globular types with a composition structure?

I was thinking about this, and since you're suggesting it I would be happy to make that change. I'd call them

Transitive-Reflexive-Globular-Types,

which is a bit shorter than

Noncoherent-Wild-Higher-Precategory

I've also been wondering why you use relational terminology for globular types (eg. the composition structure is called transitivity structure), but don't follow through by calling them Wild-Higher-Preorders. My explanation for this is that we probably want to convey categorical thinking rather than preorder thinking, and perhaps the terminology "preorder" in combination with "higher" would be too "wild".

Please don't make this change in this PR

The reason for the relational terminology is that I consider globular types a higher dimensional variant of graphs, as opposed to a less structured variant of categories

I didn't fully grasp what exactly the difference between a composition structure and transitivity is, though I expect it will be immediately clear if I try and apply the concept, so my question was genuinely "is transitivity the wrong concept?"

Ah, so what the morphism condition buys you is a horizontal composition operation, i.e.,

Given a diagram of 1-cells

f g ------> ------> x ⇓ y ⇓ z ------> ------> f' g'

you have a 2-cell

g ∘ f ----------> x ⇓ z ----------> g'∘ f'

and so on for higher cells. That's neat, I support this change. Similarly, if we assume the globular type is reflexive and the binary map is reflexive, then that gives us whiskering laws, which is also missing in the current definition.

EgbertRijke · 2024-11-20T21:11:57Z

Crazy stuff! But next time, maybe try and keep the PR a little smaller 😬

You're right. Sorry!

Thanks so much for reviewing this beast!

fredrik-bakke · 2024-11-28T22:14:52Z

Sorry to rush you, but could we try to get this PR merged? The outstanding comments are very minor, and I'd like to continue work on wild higher categories.

fredrik-bakke · 2024-11-28T22:15:24Z

I wouldn't mind making the final fixes without credit so we could get this PR merged, for instance.

fredrik-bakke · 2024-11-30T13:26:00Z

Sorry to rush you, but could we try to get this PR merged? The outstanding comments are very minor, and I'd like to continue work on wild higher categories.

Don't sweat it, I'll be working on a branch off of your current version of things in the meantime. I am trying not to have too much overlap in case you make bigger changes, but I'm making additions to composition structures that I can use to define and work with noncoherent wild ω-semiprecatgories. I want to start with semiprecategories because there are some interesting things to say about the nonunital case. From there I propose we define noncoherent wild ω-precategories as noncoherent wild ω-semiprecatgories that are reflexive and whose composition structure is unital.

Egbert Rijke and others added 10 commits September 24, 2024 09:47

work on universal objects

645fdb9

Merge branch 'master' of github.com:UniMath/agda-unimath into globular

c2abb43

adding infrastructure for globular types

3e17ca8

work

9bac61a

Merge branch 'master' of github.com:UniMath/agda-unimath into globular

4f6cead

computation of the universal globular type, and correspondence of dep…

72731cb

…endendent globular types with morphisms into the universal globular type

reflexive globular maps

bb31cac

sections and pi

f56cc6a

typo

70213c1

Merge branch 'master' of github.com:UniMath/agda-unimath into globular

5e0fac9

EgbertRijke added graph-theory structured-types labels Oct 13, 2024

EgbertRijke added 3 commits October 13, 2024 16:04

make pre-commit

90651f3

working towards duality of directed graphs

0285824

duality for directed graphs

d421336

fibers and sections

c98f6e2

EgbertRijke commented Oct 15, 2024

View reviewed changes

src/structured-types/wild-category-of-pointed-types.lagda.md Outdated Show resolved Hide resolved

EgbertRijke added 5 commits October 15, 2024 16:38

wild category of pointed types

cbc1744

mention the categorical laws, which were duplicated

8c3e39f

small edits

9c4ac74

work

7629b7d

refactor reflexive and transitive globular types

45f2d8b

EgbertRijke added the refactoring label Oct 17, 2024

lots of work

f445848

EgbertRijke added the wild-category-theory label Oct 18, 2024

EgbertRijke added 2 commits October 18, 2024 11:04

maps

b9ea44a

colax functors of noncoherent wild higher precategories

cab0051

EgbertRijke added 2 commits November 15, 2024 14:45

partially revert long copattern matchings

5362869

make pre-commit

58b750e

EgbertRijke added 6 commits November 15, 2024 16:07

discrete dependent reflexive graphs

4bb915b

make pre-commit

01fb7d6

discrete dependent reflexive globular types

092b19a

adjust text for discrete binary relations

c36005f

make pre-commit

9cb7cf0

Merge branch 'discrete-graphs' into globular

aae6781

EgbertRijke mentioned this pull request Nov 16, 2024

chore: Moving files about globular types to a new namespace #1223

Merged

moving files to globular types namespace

ea117bb

EgbertRijke added 4 commits November 17, 2024 11:21

fix imports

44edc1e

resolve merge conflicts

bc5b08a

make pre-commit

ef70c90

resolve merge conflicts

3013c3f

EgbertRijke commented Nov 20, 2024

View reviewed changes

scripts/preprocessor_git_metadata.py Outdated Show resolved Hide resolved

EgbertRijke added 2 commits November 20, 2024 07:48

bug

735ea9c

make pre-commit

18b0121

EgbertRijke changed the title ~~Hofmann-Streicher universes for graphs and globular types~~ Towards Hofmann-Streicher universes for graphs and globular types Nov 20, 2024

EgbertRijke changed the title ~~Towards Hofmann-Streicher universes for graphs and globular types~~ Hofmann-Streicher universes for graphs and globular types Nov 20, 2024

fredrik-bakke reviewed Nov 20, 2024

View reviewed changes

fredrik-bakke approved these changes Nov 20, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Hofmann-Streicher universes for graphs and globular types #1196

Hofmann-Streicher universes for graphs and globular types #1196

EgbertRijke commented Oct 13, 2024

EgbertRijke commented Oct 15, 2024

fredrik-bakke commented Oct 15, 2024

fredrik-bakke commented Oct 18, 2024

EgbertRijke commented Nov 15, 2024

A worked-out comparison

EgbertRijke commented Nov 20, 2024

fredrik-bakke left a comment

fredrik-bakke Nov 16, 2024

fredrik-bakke Nov 20, 2024

fredrik-bakke Nov 20, 2024

fredrik-bakke Nov 20, 2024

fredrik-bakke left a comment

fredrik-bakke Nov 20, 2024

fredrik-bakke Nov 20, 2024

fredrik-bakke Nov 20, 2024

fredrik-bakke Nov 20, 2024

EgbertRijke Nov 20, 2024

fredrik-bakke Nov 20, 2024

fredrik-bakke Nov 20, 2024

fredrik-bakke Nov 20, 2024

fredrik-bakke Nov 30, 2024 •

edited

Loading

EgbertRijke commented Nov 20, 2024

fredrik-bakke commented Nov 28, 2024

fredrik-bakke commented Nov 28, 2024

fredrik-bakke commented Nov 30, 2024

		e₂ : {x y : G₀} {s t : H₀ x y} {u v : H₁
		H₂ (refl G x) (refl G y) u v ≃ G₃ (e₁ u) (e₁ v)

	### Equivalences between globular types
	### Reflexive equivalences between reflexive globular types

Hofmann-Streicher universes for graphs and globular types #1196

Are you sure you want to change the base?

Hofmann-Streicher universes for graphs and globular types #1196

Conversation

EgbertRijke commented Oct 13, 2024

EgbertRijke commented Oct 15, 2024

fredrik-bakke commented Oct 15, 2024

fredrik-bakke commented Oct 18, 2024

EgbertRijke commented Nov 15, 2024

A worked-out comparison

EgbertRijke commented Nov 20, 2024

fredrik-bakke left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fredrik-bakke left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fredrik-bakke Nov 30, 2024 • edited Loading

Choose a reason for hiding this comment

EgbertRijke commented Nov 20, 2024

fredrik-bakke commented Nov 28, 2024

fredrik-bakke commented Nov 28, 2024

fredrik-bakke commented Nov 30, 2024

fredrik-bakke Nov 30, 2024 •

edited

Loading