| Age | Commit message (Collapse) | Author |
|---|
|
Since we are working with multiple setoids now, it makes more sense to
qualify their members. Follow the "as P" pattern from the standard
library. Also stop importing those symbols from Relation.Binary.Core as
later agda-stdlib versions will move them away. Rather than EqSetoid or
PropEq, use P.setoid consistently.
|
|
|
|
|
|
We never used the equality property. Thus a simple function is
sufficient here. We always fulfilled the property using ≡-to-Π anyway.
|
|
Turns out, we never use this requirement. The only place where it may
come in relevant is the free theorems. But here non-injectivity turns
out to be reasoning about multiple get functions that are selected by
the additional index each individually satisfying the free theorem and
thus commonly satisfying it as well.
|
|
|
|
Example inspired in VoigtlaenderHMW13. Note that Vec (α × β) (length s)
is not Shaped in this way since its real index is only a number.
|
|
|
|
This is possible using the PartialVecVec implementation.
|
|
|
|
|
|
|
