Conversation
|
Managed to get preview working again :D http://agda-synthetic-categories.toth.co.uk/preview/185/tot-0001/index.xml |
| \p{This project began as an experiment in formalising simplicial (or triangulated) | ||
| type theory inside the Agda proof assistant, with the goal of creating a library | ||
| for doing synthetic higher category theory.} | ||
|
|
||
| \p{The project was also an experiment in literate formalisation using the | ||
| [[forester]] system, with the goal that mathematics in the informal language of | ||
| HoTT could live side by side with the Agda formalisation, with each bringing | ||
| their own benefits.} |
There was a problem hiding this comment.
| \p{This project began as an experiment in formalising simplicial (or triangulated) | |
| type theory inside the Agda proof assistant, with the goal of creating a library | |
| for doing synthetic higher category theory.} | |
| \p{The project was also an experiment in literate formalisation using the | |
| [[forester]] system, with the goal that mathematics in the informal language of | |
| HoTT could live side by side with the Agda formalisation, with each bringing | |
| their own benefits.} | |
| \p{This project began as an experiment in formalising simplicial (or triangulated) | |
| type theory inside the Agda proof assistant, with the goal of creating a library | |
| for doing synthetic higher category theory. The project was also an experiment | |
| in literate formalisation using the [[forester]] system, with the goal that | |
| mathematics in the informal language of HoTT could live side by side with the | |
| Agda formalisation, with each bringing their own benefits.} |
This doesn't address what the current goals of the library are. Consider commenting that this document is incomplete.
| \p{ | ||
| Names should generally be in kebab-case. | ||
|
|
||
| If a descriptive or common name exists for a theorem, then use that, otherwise | ||
| the name can be informed from the type: Conclusion should go to the left of premises, separated by | ||
| a unicode left arrow ←. This matches the order of function application/composition and makes reading the code easier. | ||
| other defined mixfix operations e.g. ＝, ≃ or ¬ may also be used in place of a '-'. | ||
| If a descriptive or common name exists for a theorem or definition, then that | ||
| should be used, otherwise the name can be informed from the type: Conclusion | ||
| should go to the left of premises, separated by a unicode left arrow ←. This | ||
| matches the order of function application/composition and makes reading the code | ||
| easier. Other defined mixfix operations e.g. ＝, ≃ or ¬ may also be used in place | ||
| of a '-'. Note that some discretion is advised when giving these \em{derived} | ||
| names; premises that are inferable from the context should be omitted, so that | ||
| the names have a balance of brevity and descriptiveness. | ||
| } |
There was a problem hiding this comment.
This paragraph need some prefacing I think. I.e., what are the naming conventions about, why do we need them, how strict are they?
| This means that some types that are proposition-like aren't written in the way | ||
| it is tempting to write them - most notably this includes the data of a | ||
| functions inverse, called a [quasi-inverse](Foundations.QuasiEquivalences). When | ||
| we make this notion [coherent](Foundations.Equivalences), it becomes a | ||
| proposition, and so is written\code{is-equiv}. When referring to things which |
There was a problem hiding this comment.
i'm not entirely convinced about this convention yet. For instance being coherently idempotent is not a proposition, but I am still tempted to use "is", or "are" for it. Maybe more reasons can be given supporting your naming style? E.g. you reserve it for a logical fragment of the library, which only considers propositions. In other words you consider it a logical connective
| \todo{ (Sam): I wonder, we should also rename propositions like \code{FunExt} to | ||
| \code{has-fun-ext}, referring to the proposition that a pair of universes have | ||
| the function extensionality property. |
There was a problem hiding this comment.
Personally I'm very happy with just writing FunExt/fun-ext
| Along a similar vein, maybe we should rename the \code{UP-such-and-such} to | ||
| \code{has-UP-such-and-such}. |
There was a problem hiding this comment.
I'm happy with this suggestion!
| \subtree[tot-NTYP]{ | ||
| \title{Naming non propositional types} | ||
|
|
||
| This means that some types that are proposition-like aren't written in the way it is tempting to write them - most notably this | ||
| includes the data of a functions inverse, called a [quasi-inverse](Foundations.QuasiEquivalences). When we make this notion | ||
| [coherent](Foundations.Equivalences), it becomes a proposition, and so is written \code{is-equiv}. | ||
| \p{Types should be also be named in \code{Kebab-case} but with the first word | ||
| capitalised.} |
There was a problem hiding this comment.
Incoherent subtree.
Do you mean that we can write "Is-coherently-idempotent" even though it is not a propositions?
There was a problem hiding this comment.
The first thought it coherent-idempotent-witness I suppose... but I see the argument that this is ugly. My rationale for the convention of is-... or has-... is that:
A) it's not obvious whether things are propositions are not (there are things that feel like they should be propositions that aren't), so when you see something phrased like a proposition you can be sure it is one, and the you can use all of your intutition for propositions.
B) For things that really aren't propositions there should be a nice way to think about them that makes it clear that they aren't propositions. E.g. I find is-...-witness dissatisfying for this reason, but quasi-inverse feels like a good name.
There was a problem hiding this comment.
Actually according to this scheme it should be Quasi-inverse.... How do you feel about capitalising things?
There was a problem hiding this comment.
Actually according to this scheme it should be
Quasi-inverse.... How do you feel about capitalising things?
hate it
There was a problem hiding this comment.
I suppose this means you want "left/right inverse" over "split-mono/epi witness" then
There was a problem hiding this comment.
Okay, I would be quite happy to remove capitalisation too. I think in my head I thought there would be a clash between instances of a type and the type itself... but it feels like this just doesn't really come up in practice
| \remark{This page is a work in progress and still evolving as we continue to work | ||
| on the library.} |
There was a problem hiding this comment.
This sounds like it is suggesting the introduction can never be finished. Is that true? Maybe a better formulation is
| \remark{This page is a work in progress and still evolving as we continue to work | |
| on the library.} | |
| \remark{ | |
| This page is a work in progress and still evolving as we continue to lay the | |
| groundworks of the library. | |
| } |
| \date{2026-06-06} | ||
| \import{stt-macros} | ||
|
|
||
| \p{Agda uses the concept of [modules]() to organise code bases. } |
| \import{stt-macros} | ||
|
|
||
| \p{Agda uses the concept of [modules]() to organise code bases. } | ||
| \p{Currently we have the following set of top-level modules: |
There was a problem hiding this comment.
In agda-unimath we call these namespaces.
There was a problem hiding this comment.
Although I've heard some people complain that what Agda implements is not namespaces. I.e. where you can extend a namespace with new definitions outside of its original place of definition.
Is the suggestion here to replace top-level modules with namespaces - in which case I think this would be appropriate, since there is no module Foundations or Core
There was a problem hiding this comment.
Oh yes, that's right. you heard it from me for instance 😄
There was a problem hiding this comment.
you can always extend Foundations with a new module...
2 participants
See #94