Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Expanding on the naming conventions #793

Draft
wants to merge 36 commits into
base: master
Choose a base branch
from
Draft

Expanding on the naming conventions #793

Changes from 1 commit
Commits
Show all changes
36 commits
Select commit Hold shift click to select a range
5d1c20b
expanding naming conventions
EgbertRijke Sep 21, 2023
18e63c4
separate file for naming conventions
EgbertRijke Sep 21, 2023
efd8af3
separate file for naming conventions
EgbertRijke Sep 21, 2023
d8a9cd6
make pre-commit
EgbertRijke Sep 21, 2023
671b890
Merge branch 'master' of github.com:UniMath/agda-unimath into naming
EgbertRijke Sep 21, 2023
0b4e67b
explaining the naming of underlying objects
EgbertRijke Sep 21, 2023
1f470b1
make pre-commit
EgbertRijke Sep 21, 2023
3d521a8
Update NAMING.md
EgbertRijke Sep 21, 2023
92c28a4
fix broken links
EgbertRijke Sep 21, 2023
f1e82f9
Merge branch 'naming' of github.com:EgbertRijke/agda-unimath into naming
EgbertRijke Sep 21, 2023
d9ee159
sectioning
EgbertRijke Sep 21, 2023
e91cf2e
adding gregor
EgbertRijke Sep 21, 2023
0ab40db
make pre-commit
EgbertRijke Sep 21, 2023
a44bd45
further explaining our naming conventions
EgbertRijke Sep 22, 2023
2b17fa6
make pre-commit
EgbertRijke Sep 22, 2023
1d30aa6
further comments
EgbertRijke Sep 22, 2023
c922269
revised introduction
EgbertRijke Sep 22, 2023
4ac7ec8
update examples
EgbertRijke Sep 22, 2023
cc82fac
updating the general scheme
EgbertRijke Sep 22, 2023
e91085b
incorporating some of Vojtech's comments
EgbertRijke Sep 22, 2023
88a9226
Update NAMING-CONVENTIONS.md
EgbertRijke Sep 22, 2023
74e0697
Update NAMING-CONVENTIONS.md
EgbertRijke Sep 22, 2023
a8bfc8f
Update NAMING-CONVENTIONS.md
EgbertRijke Sep 22, 2023
6f88244
Update NAMING-CONVENTIONS.md
EgbertRijke Sep 22, 2023
fa770b4
make pre-commit
EgbertRijke Sep 22, 2023
633b471
Update NAMING-CONVENTIONS.md
EgbertRijke Sep 22, 2023
bd3ed0b
make pre-commit
EgbertRijke Sep 22, 2023
0b27816
list of common descriptors
EgbertRijke Sep 22, 2023
63a0091
Update NAMING-CONVENTIONS.md
EgbertRijke Sep 22, 2023
1f95642
make pre-commit
EgbertRijke Sep 22, 2023
fdea201
equiv and htpy in the table
EgbertRijke Sep 22, 2023
693cb0f
work
EgbertRijke Sep 23, 2023
1fbc9b9
merge conflicts
EgbertRijke Sep 23, 2023
6006e80
explaining the goals
EgbertRijke Sep 23, 2023
81f66b8
predictability
EgbertRijke Sep 23, 2023
fce34cd
clarify use of
EgbertRijke Sep 23, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
clarify use of
  • Loading branch information
@EgbertRijke
EgbertRijke committed Sep 23, 2023
commit fce34cda3ee6f24bafeb0a461ed25c7dc7030ee8
26 changes: 13 additions & 13 deletions NAMING-CONVENTIONS.md
View file
Open in desktop
EgbertRijke marked this conversation as resolved.
Show resolved Hide resolved
Original file line number Diff line number Diff line change
Expand Up @@ -190,19 190,19 @@ pointwise equal to `tr-Ω` as `compute-tr-Ω`.
To give a sense of the kind of general descriptors we use, we list some common
descriptors in the table below.

| Descriptor | Purpose |
| ---------------- | -------------------------------------------------------------------------------------------------------------- |
| `coh` | Used for proofs of coherence |
| `coherence` | Used to assert coherence |
| `compute` | Used for proofs of computation, which may be an identification or an element of any other identity system |
| `Eq` | Used for identity systems on types of a particular form |
| `eq` | Used as a descriptor for the identity type |
| `equiv` | Used for equivalences, and also for names of identity systems of universe-like types |
| `extensionality` | Used for computations of identity types |
| `htpy` | Used for constructions of homotopies, and also for names of identity systems of function-like types |
| `is-property` | Used when `is-prop` is unavailable |
| `map` | Used in two ways: as the functorial action of a type constructor, but also as the underlying map of a morphism |
| `type` | Used for the underlying type of an object |
| Descriptor | Purpose |
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add statement

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it would be very good to have an example column for this table as well. That's what I did for the sHoTT project

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Another descriptor pair we use a lot is is/has :)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do you think of them as descriptors? That seems grammatically very weird.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

They are modifiers signifying that the type is a property/structure, and then we omit them for the associated total types. It just seems consistent with the scheme.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm willing to come up with our own naming convention, but I'm not willing to come up with a new theory that the verbs to be and to have are modifiers. That idea seems out of this world to me.

| ---------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| `coh` | Used for proofs of coherence |
| `coherence` | Used to assert coherence |
Comment on lines 195 to 196
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems like the need for coh is obsoleted by introducing statement.

| `compute` | Used for proofs of computation, which may be an identification or an element of any other identity system |
| `Eq` | Used for identity systems on types where `htpy` or `equiv` is not an appropriate descriptor of the identity system. `Eq` is commonly used as a descriptor for identity systems on number systems. |
| `eq` | Used as a descriptor for the identity type |
| `equiv` | Used for equivalences, and also for names of identity systems of universe-like types |
| `extensionality` | Used for computations of identity types |
| `htpy` | Used for constructions of homotopies, and also for names of identity systems of function-like types |
| `is-property` | Used when `is-prop` is unavailable |
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't remember if I already mentioned this, but did you know we actually define is-property in foundation-core.subtypes? Although IIRC it is not referred to anywhere.

| `map` | Used in two ways: as the functorial action of a type constructor, but also as the underlying map of a morphism |
| `type` | Used for the underlying type of an object |

## Overview of our naming conventions

Expand Down