This adds reindexing of displayed categories, the basic definitions of opcartesian fibrations, as well as discrete opfibrations, some nice properties of opcartesian morphisms and the construction of the substitution functor. I stopped short of proving the pseudo-functorial laws of the latter mostly because I didn't care too much.
As opposed to the 1lab which reasons with displayed morphisms using regular paths and transports, I thought we could try having reasoning combinators for the PathP version, so I went with that and added the two abominations that are eq1 ≡[ p ∙ q ]∙ eq2 and eq1 ≡[ p ⋆ q ]⋆ eq2 which are respectively displayed versions of vertical and horizontal compositions of paths. This lets us input mostly "regular" proofs, with the caveat that Agda can't always infer p and q, and when it can it might hinder performance, so I chose to leave them explicit in the syntax. It's a little bit of an experiment but I found that the verbosity of proofs is not too bad considering you don't really need to read p and q. Also, you often end up with equalities over the wrong equality, but because the base category has homsets you can always rectify using ≡[]-rectify.
Hi everyone,
This adds reindexing of displayed categories, the basic definitions of opcartesian fibrations, as well as discrete opfibrations, some nice properties of opcartesian morphisms and the construction of the substitution functor. I stopped short of proving the pseudo-functorial laws of the latter mostly because I didn't care too much.
As opposed to the 1lab which reasons with displayed morphisms using regular paths and transports, I thought we could try having reasoning combinators for the
PathPversion, so I went with that and added the two abominations that areeq1 ≡[ p ∙ q ]∙ eq2andeq1 ≡[ p ⋆ q ]⋆ eq2which are respectively displayed versions of vertical and horizontal compositions of paths. This lets us input mostly "regular" proofs, with the caveat that Agda can't always infer p and q, and when it can it might hinder performance, so I chose to leave them explicit in the syntax. It's a little bit of an experiment but I found that the verbosity of proofs is not too bad considering you don't really need to readpandq. Also, you often end up with equalities over the wrong equality, but because the base category has homsets you can always rectify using≡[]-rectify.WDYT?