diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-06 14:09:45 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-06 14:09:45 +0000 |
| commit | 336c0c8c486bf5323cd44f35e06b3aa25f53bb22 (patch) | |
| tree | 727e9b33ba2b81e87232a950e61e923027b475c0 | |
| parent | 3c200003925d2fc623c86f19706bcca7411adc76 (diff) | |
Redefine reindex in terms of bundle and index.
| -rw-r--r-- | src/Data/Setoid/Indexed/Definition.idr | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/src/Data/Setoid/Indexed/Definition.idr b/src/Data/Setoid/Indexed/Definition.idr index cf2bb3d..cf5d9a2 100644 --- a/src/Data/Setoid/Indexed/Definition.idr +++ b/src/Data/Setoid/Indexed/Definition.idr @@ -63,15 +63,7 @@ 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) - } - } +reindex f x = bundle (index x . f) namespace ToSetoid public export |