Hofmann-Streicher universes for graphs and globular types

[EgbertRijke]

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.

[EgbertRijke]

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.

[fredrik-bakke]

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]

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?

[fredrik-bakke]

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.

1. 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.
2. 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.
3. 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).
4. 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.

[EgbertRijke]

This PR now depends on #1222

[EgbertRijke]

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.

1. 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.
2. 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.
3. 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).
4. 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.