diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 13:08:39 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 13:08:39 +0000 |
| commit | 3c200003925d2fc623c86f19706bcca7411adc76 (patch) | |
| tree | e09c7a4800b6cd886a6c1f75d881e521f2560bb5 | |
| parent | 1e404cee8e3f36a5fe657012db8ba94c5666cec2 (diff) | |
Define setoid reindexing.
| -rw-r--r-- | src/Data/Setoid/Indexed/Definition.idr | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Data/Setoid/Indexed/Definition.idr b/src/Data/Setoid/Indexed/Definition.idr index d50af06..cf2bb3d 100644 --- a/src/Data/Setoid/Indexed/Definition.idr +++ b/src/Data/Setoid/Indexed/Definition.idr @@ -61,6 +61,18 @@ index x i = MkSetoid } } +public export +reindex : (a -> b) -> IndexedSetoid b -> IndexedSetoid a +reindex f x = MkIndexedSetoid + { U = x.U . f + , equivalence = MkIndexedEquivalence + { relation = \i => x.equivalence.relation (f i) + , reflexive = \i => x.equivalence.reflexive (f i) + , symmetric = \i => x.equivalence.symmetric (f i) + , transitive = \i => x.equivalence.transitive (f i) + } + } + namespace ToSetoid public export irrelevantCast : (0 b : a -> Type) -> IndexedSetoid a |