Use #assume and use for FunExt and ExtExt #28
Conversation
| @@ -152,16 +157,15 @@ in two steps. | |||
| ( \ f -> yon-evid-twice-pointwise ϕ x f) | |||
|
|
|||
| -- By funext again, these are equal as functions of x and f. | |||
| #def yon-evid | |||
| (funext : FunExt) | |||
| #def yon-evid uses (funext) | |||
| (ϕ : (z : A) -> hom A a z -> C z) | |||
| : ((yon A is-segal-A a C is-covariant-C) ((evid A a C) ϕ )) = ϕ | |||
| := eq-htpy funext | |||
There was a problem hiding this comment.
You may notice that some occurrences of funext (and extext) in arguments is not removed. This is because definitions that use them come from different files, so the argument becomes explicit.
I think it makes sense have a (global) version of #assume that will maintain assumption implicit, even in other files. I will try to introduce such a feature in future versions of rzk.
|
I've also refactored definitions to use shape coercion where possible. |
| @@ -176,8 +176,8 @@ This is a literate `rzk` file: | |||
| ( (t : χ) -> X t [ ψ t |-> f t ])) | |||
| := | |||
| ( \ h -> (\ t -> h t , \ t -> h t) , | |||
| ( ( \ fg t -> (second fg) t , \ h -> refl) , | |||
| ( ( \ fg t -> (second fg) t , \ h -> refl)))) | |||
| ( ( \ (_f, g) t -> g t , \ h -> refl) , | |||
There was a problem hiding this comment.
Can you explain the use of the underscore here and elsewhere?
There was a problem hiding this comment.
Single underscore (_) means a wildcard pattern (ignore the argument).
An identifier for an argument that starts with an underscore (e.g. _f or _is-segal-A) serves same purpose, but also helps readability, telling the reader a little bit about what the ignored argument represents.
This is a habit I transfer from programming in Haskell, I will gladly hear about @fredrik-bakke's experience in Agda.
There was a problem hiding this comment.
In Agda, the underscore character has multiple purposes.
- It is used as a placeholder character for mixfix syntax. E.g. if you define a function
_!, you can apply it by writingx !. Similarly, you could define the functionif_then_else_. I think this is one of the big reasons why there are so few reserved characters and why spaces is so important in Agda. - It is used as a placeholder expression to tell Agda to infer a term.
- It is used as a standalone token as a discard similar to how it functions in for instance C#. For example, if you want to define a constant function taking two arguments, you could write
\ _ _ -> x.
I quite like having just _ when discarding arguments as it looks more clean and doesn't clutter the code space with information that is irrelevant anyways. In agda-unimath, if an argument is not "irrelevant", but is not directly used in a definition, we tend to just give it a normal name I think. Other than that, I don't have a strong opinion either way and would be open to having a special naming convention for these. Maybe a suffix would look nicer than a prefix, but perhaps this defeats part of the purpose as it will be less familiar to people coming from Haskell or similar coding languages.
|
I'll be offline for most of the rest of the day, so @fizruk whenever you've resolved the conversations above and feel ready to merge please go ahead. |
|
I will merge, but leave the conversations open in case you (or others) have more to say. |
Closes #26.