Expanding on the naming conventions #793

EgbertRijke · 2023-09-21T08:06:36Z

No description provided.

NAMING.md

fredrik-bakke

I would like to review this PR carefully before it is merged, but that will have to wait at the moment.

NAMING.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

VojtechStep

Thank you for putting it all together. I do feel like there are some inconsistencies in the description of some of the examples, could you elaborate a bit on the comments?

NAMING-CONVENTIONS.md

VojtechStep · 2023-09-22T12:52:46Z

NAMING-CONVENTIONS.md

+this happens is in `hom-iso-Group`, which is the construction that returns the
+underlying group homomorphism of an isomorphism of group. The fact that a group
+isomorphism is an isomorphsim is called `is-iso-iso-Group`, which also uses the
+pattern `[type]-[Namespace]`. One could also consider calling it


Isn't this [type]-[hypotheses]-[Namespace]? is-iso being the type and iso being the hypothesis. If not, what's the difference between this and the example is-ideal-ideal-Ring below?

Things that go under [type] are the output types of the specification of an entry. In the case of is-iso-hom-Ring the output type of its specification is UU. We don't put this in the name. Instead is-iso is a descriptor of the specification, falling under [name] in the general pattern.

I don't think I follow. What I'm reading is that

is-iso-iso-Group : (f : iso) -> is-iso f follows [type]-[Namespace], but

is-ideal-ideal-Ring : (I : ideal) -> is-ideal I follows [type]-[hypotheses]-[Namespace]

Is that correct?

NAMING-CONVENTIONS.md

VojtechStep · 2023-09-22T13:02:53Z

NAMING-CONVENTIONS.md

+there is an interchange law for addition over addition, which states that
+`(a + b) + (c + d) ＝ (a + c) + (b + d)`. This law is called
+`interchange-law-add-add-ℤ`. Again, this naming follows the pattern
+`[type]-[Namespace]`, because it states the type of which an element is


Again I'd say this is [type]-[name]-[Namespace]

The type of the output of this entry is interchange-law add-ℤ add-ℤ, so the name here merely describes the type, and the namespace for the integers. In the case is-equiv-succ-ℤ : is-equiv succ-ℤ this would also fall under [type]-[Namespace].

The explanation on left-unit-law-mul-ℤ makes this clear now 👌

VojtechStep · 2023-09-22T13:05:51Z

NAMING-CONVENTIONS.md

+- We prioritize the readability of the code and avoid subtly different
+  variations of the same symbol. An important exception is the use of the
+  [full width equals sign](https://codepoints.net/U+ff1d) for the identity type,
+  as the standard equals sign is a reserved symbol in Agda.


I'd also mention the homotopy composition and whiskering situation

Other examples are the asterisk vs asterisk operator, and big vee vs small vee. Maybe rephrase to "try to avoid subtly different"

NAMING-CONVENTIONS.md

VojtechStep · 2023-09-22T13:56:50Z

NAMING-CONVENTIONS.md

+construction of the underlying set of a group returns for each group a set,
+which is an element of type `Set`. Similarly, we have `type-Group]`,
+`semigroup-Group`, `type-Ring`, `set-Ring`, and so on. Another instance where
+this happens is in `hom-iso-Group`, which is the construction that returns the


hom-iso-Group has the approximate type iso -> hom, shouldn't it then be [type]-[hypotheses]-[Namespace]?

That looks right

NAMING-CONVENTIONS.md

Co-authored-by: Vojtěch Štěpančík <vojtechstepancik@outlook.com>

NAMING-CONVENTIONS.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

NAMING-CONVENTIONS.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

VojtechStep · 2023-09-22T15:08:25Z

NAMING-CONVENTIONS.md

+name adds no extra useful information. This situation is common in instances
+where we omit the `[descriptor]` part of a name. For instance
+`is-category-Category` and `is-ideal-ideal-Ring` follow the patterns
+`[output-type]-[Namespace]` and `[output-type]-[input-types]-[Namespace]`,


On second reading I'm not sure why

is-category-Category : (C : Category) -> is-category C and

is-ideal-ideal-Ring : (I : ideal-Ring) -> is-ideal I

are different? Even the modules where they are defined seem to follow the exact same structure.

fredrik-bakke · 2023-09-22T15:12:00Z

NAMING-CONVENTIONS.md

+  and not `commutative-×`, and the unit of a modality is called `unit-modality`
+  and not `unit-○`.


Although the second example here is also an instance of using a variable in a name, perhaps it still conveys the correct sentiment.

fredrik-bakke · 2023-09-22T15:21:52Z

NAMING-CONVENTIONS.md

+- **[descriptor]:** This part is used to give a custom descriptive name for the
+  entry.


Suggested change

- **[descriptor]:** This part is used to give a custom descriptive name for the

entry.

- **[descriptor]:** This part is used to give a custom descriptive name for the

entry, or refer to the custom descriptive name of another entry.

If I didn't misunderstand, this is how it is used in the below example is-iso-prop-hom-Ring.

fredrik-bakke · 2023-09-22T15:25:25Z

NAMING-CONVENTIONS.md

+`[output-type]-[Namespace]`. The construction of the underlying set of a group
+returns for each group a set, which is an element of type `Set`. Similarly, we
+have `type-Group`, `semigroup-Group`, `type-Ring`, `set-Ring`, and so on.
+Another instance where this happens is in `hom-iso-Group`, which is the


Isn't hom-iso-Group an instance of [output-type]-[input-types]-[Namespace]?

fredrik-bakke · 2023-09-22T15:27:00Z

NAMING-CONVENTIONS.md

+Another instance where this happens is in `hom-iso-Group`, which is the
+construction that returns the underlying group homomorphism of an isomorphism of
+group. The fact that a group isomorphism is an isomorphsim is called
+`is-iso-iso-Group`, which also uses the pattern `[output-type]-[Namespace]`. One


Isn't this also an instance of [output-type]-[input-types]-[Namespace]?

fredrik-bakke · 2023-09-22T15:28:21Z

NAMING-CONVENTIONS.md

+`is-iso-iso-Group`, which also uses the pattern `[output-type]-[Namespace]`. One
+could also consider calling it `is-iso-hom-iso-Group`, to emphasize that the
+underlying group homomorphism of the isomorphism is an isomorphism. However,
+this name does not fit our patterns in any way, and the addition of `hom` to the


It's not clear to me how this does not fit our patterns better than the proposed one. Also, the name would be more consistent with is-iso-hom-inv-iso-Group

NAMING-CONVENTIONS.md

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

scripts/contributors_data.toml

fredrik-bakke · 2023-10-06T18:22:27Z

NAMING-CONVENTIONS.md

+| `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                                                                                                                                                                |


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.

fredrik-bakke · 2023-10-10T12:40:38Z

NAMING-CONVENTIONS.md

+To give a sense of the kind of general descriptors we use, we list some common
+descriptors in the table below.
+
+| Descriptor       | Purpose                                                                                                                                                                                           |


Add statement

fredrik-bakke · 2023-10-10T12:41:03Z

NAMING-CONVENTIONS.md

+To give a sense of the kind of general descriptors we use, we list some common
+descriptors in the table below.
+
+| Descriptor       | Purpose                                                                                                                                                                                           |


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

fredrik-bakke · 2023-10-10T13:29:32Z

NAMING-CONVENTIONS.md

+To give a sense of the kind of general descriptors we use, we list some common
+descriptors in the table below.
+
+| Descriptor       | Purpose                                                                                                                                                                                           |


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

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

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.

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.

fredrik-bakke · 2023-10-10T14:11:40Z

NAMING-CONVENTIONS.md

+| `coh`            | Used for proofs of coherence                                                                                                                                                                      |
+| `coherence`      | Used to assert coherence                                                                                                                                                                          |


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

expanding naming conventions

5d1c20b

EgbertRijke added the guides label Sep 21, 2023

EgbertRijke added 3 commits September 21, 2023 10:14

separate file for naming conventions

18e63c4

separate file for naming conventions

efd8af3

make pre-commit

d8a9cd6

EgbertRijke mentioned this pull request Sep 21, 2023

WIP Functor Categories #787

Closed

fredrik-bakke reviewed Sep 21, 2023

View reviewed changes

NAMING.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed Sep 21, 2023

View reviewed changes

NAMING.md Outdated Show resolved Hide resolved

NAMING.md Outdated Show resolved Hide resolved

NAMING.md Outdated Show resolved Hide resolved

NAMING.md Outdated Show resolved Hide resolved

EgbertRijke and others added 15 commits September 21, 2023 22:27

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

671b890

explaining the naming of underlying objects

0b4e67b

make pre-commit

1f470b1

Update NAMING.md

3d521a8

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

fix broken links

92c28a4

Merge branch 'naming' of github.com:EgbertRijke/agda-unimath into naming

f1e82f9

sectioning

d9ee159

adding gregor

e91cf2e

make pre-commit

0ab40db

further explaining our naming conventions

a44bd45

make pre-commit

2b17fa6

further comments

1d30aa6

revised introduction

c922269

update examples

4ac7ec8

updating the general scheme

cc82fac

VojtechStep reviewed Sep 22, 2023

View reviewed changes

incorporating some of Vojtech's comments

e91085b

VojtechStep reviewed Sep 22, 2023

View reviewed changes

NAMING-CONVENTIONS.md Outdated Show resolved Hide resolved

VojtechStep reviewed Sep 22, 2023

View reviewed changes

NAMING-CONVENTIONS.md Outdated Show resolved Hide resolved

EgbertRijke and others added 2 commits September 22, 2023 16:29

Update NAMING-CONVENTIONS.md

88a9226

Co-authored-by: Vojtěch Štěpančík <vojtechstepancik@outlook.com>

Update NAMING-CONVENTIONS.md

74e0697

Co-authored-by: Vojtěch Štěpančík <vojtechstepancik@outlook.com>

fredrik-bakke reviewed Sep 22, 2023

View reviewed changes

NAMING-CONVENTIONS.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed Sep 22, 2023

View reviewed changes

NAMING-CONVENTIONS.md Outdated Show resolved Hide resolved

EgbertRijke and others added 3 commits September 22, 2023 16:47

Update NAMING-CONVENTIONS.md

a8bfc8f

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

Update NAMING-CONVENTIONS.md

6f88244

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

make pre-commit

fa770b4

fredrik-bakke reviewed Sep 22, 2023

View reviewed changes

NAMING-CONVENTIONS.md Outdated Show resolved Hide resolved

EgbertRijke and others added 2 commits September 22, 2023 17:01

Update NAMING-CONVENTIONS.md

633b471

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

make pre-commit

bd3ed0b

VojtechStep reviewed Sep 22, 2023

View reviewed changes

fredrik-bakke reviewed Sep 22, 2023

View reviewed changes

list of common descriptors

0b27816

fredrik-bakke reviewed Sep 22, 2023

View reviewed changes

NAMING-CONVENTIONS.md Outdated Show resolved Hide resolved

EgbertRijke commented Sep 22, 2023

View reviewed changes

NAMING-CONVENTIONS.md Outdated Show resolved Hide resolved

EgbertRijke and others added 3 commits September 22, 2023 21:05

Update NAMING-CONVENTIONS.md

63a0091

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

make pre-commit

1f95642

equiv and htpy in the table

fdea201

VojtechStep reviewed Sep 23, 2023

View reviewed changes

scripts/contributors_data.toml Outdated Show resolved Hide resolved

EgbertRijke added 5 commits September 23, 2023 14:10

work

693cb0f

merge conflicts

1fbc9b9

explaining the goals

6006e80

predictability

81f66b8

clarify use of

fce34cd

fredrik-bakke mentioned this pull request Oct 6, 2023

Finish draft of the style guide rzk-lang/sHoTT#94

Merged

fredrik-bakke reviewed Oct 6, 2023

View reviewed changes

fredrik-bakke reviewed Oct 10, 2023

View reviewed changes

EgbertRijke marked this pull request as draft November 24, 2023 05:08

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Expanding on the naming conventions #793

Expanding on the naming conventions #793

EgbertRijke commented Sep 21, 2023

fredrik-bakke left a comment

VojtechStep left a comment

VojtechStep Sep 22, 2023

EgbertRijke Sep 22, 2023

VojtechStep Sep 22, 2023

VojtechStep Sep 22, 2023

EgbertRijke Sep 22, 2023 •

edited

Loading

VojtechStep Sep 22, 2023

VojtechStep Sep 22, 2023

fredrik-bakke Sep 22, 2023

VojtechStep Sep 22, 2023

EgbertRijke Sep 22, 2023

VojtechStep Sep 22, 2023 •

edited

Loading

fredrik-bakke Sep 22, 2023

fredrik-bakke Sep 22, 2023

fredrik-bakke Sep 22, 2023

fredrik-bakke Sep 22, 2023

fredrik-bakke Sep 22, 2023

fredrik-bakke Oct 6, 2023

fredrik-bakke Oct 10, 2023

fredrik-bakke Oct 10, 2023

fredrik-bakke Oct 10, 2023

EgbertRijke Oct 10, 2023

fredrik-bakke Oct 10, 2023

EgbertRijke Oct 11, 2023

fredrik-bakke Oct 10, 2023

		and not `commutative-×`, and the unit of a modality is called `unit-modality`
		and not `unit-○`.

		- [descriptor]: This part is used to give a custom descriptive name for the
		entry.

		\| `coh` \| Used for proofs of coherence \|
		\| `coherence` \| Used to assert coherence \|

Expanding on the naming conventions #793

Are you sure you want to change the base?

Expanding on the naming conventions #793

Conversation

EgbertRijke commented Sep 21, 2023

fredrik-bakke left a comment

Choose a reason for hiding this comment

VojtechStep 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

EgbertRijke Sep 22, 2023 • edited Loading

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

VojtechStep Sep 22, 2023 • edited Loading

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

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

EgbertRijke Sep 22, 2023 •

edited

Loading

VojtechStep Sep 22, 2023 •

edited

Loading