Equivalence injective type families #1009
Conversation
|
On the readthedocs page of the INJECTIVE pragma I find no reasons stated why we should want this pragma in our library. On the contrary, I think injectivity of Agda entries should be explicitly recorded knowledge, with proofs why injectivity holds. Agda-unimath is about recording mathematical knowledge, not about hiding it. This would be an argument for me to not consider this pragma. What are your reasons for wanting to experiment with this? Would you be ok with it if this PR gets rejected? |
|
I completely agree that we dont want to use this pragma, and this PR doesn't introduce its use. I was curious if we could make Agda infer things like the cardinality of a standard finite set with it, but found out that functionality doesn't yet exist. |
|
This PR is compiling and it looks ready for review. I would be happy to give it my approval and merge it after the open conversations are resolved. In particular, there are lots of edits in this PR that would be useful to merge into the library, and if you have further developments of equivalence injective type families in mind they could easily happen in a subsequent pull request. |
Thanks, I am not planning on adding anything else. I was just unsure of the naming and wanted to review the code myself before marking it ready for review, but seems you helped expedite that process 😅 |
|
EDIT: Never mind, I'll just make a new branch. |
I was actually expecting that you would change the notion of equivalence injective type family to transport-split type family. Do you still want to go through with this PR as it is? |
I think equivalence injective type families deserve a spot on equal footing to injective maps. I was thinking to develop the other notions alongside it. |
|
Ah ok, I thought we came to a different conclusions, i.e., that objects should not be called injective in this way even if they happen to be defined as some maps. To me, the notion of injectivity for maps is acceptible because it is a well established notion about maps, but to call an object injective in a way that doesn't refer to the usual notion of injective object in any way sounds wrong and I don't know why it should have equal footing to the well established notion of injective map. |
|
Okay. Then how about |
|
Hm... my apologies I think I went a bit too hard in my previous message. It is totally true that the notion has been used previously, and that it is a useful thing to isolate. Perhaps "equivalence injective type family" is just the best name for it. I think I can live with it:P Apologies for saying that it is wrong. |
|
I checked this PR once more and it looks good now. I'll merge it. Thanks for your good work Fredrik, and thanks for bearing with me. |
|
No worries! Keep posted for the sequel 😁 |
This is the follow-up PR to #1009. ### Summary - Transport-split type families are type families `B` such that `equiv-tr B` admits fiberwise sections - This notion is equivalent to univalent type families by a corollary of the fundamental theorem of identity types - Some infrastructure and basic lemmas for univalent type families - Preunivalent type families are type families `B` such that `equiv-tr B` is a fiberwise embedding - 3-for-2 for preunivalent type families using the preunivalence axiom - Some other infrastructure - `Fin` is preunivalent ### Future work - Closure properties for univalent and preunivalent type families Co-authored-by: Egbert Rijke <[email protected]>
I was checking out Agdas
INJECTIVEpragma. Here are some edits I made while exploring.