yellowsquid/idris-setoid.git/src/Data/Setoid/Indexed, branch feature/reindex [no description] http://git.yellowsquid.uk/yellowsquid/idris-setoid.git/atom?h=feature%2Freindex 2022-12-07T12:58:45Z Make more arguments irrelevant. 2022-12-07T12:58:45Z Greg Brown greg.brown01@ed.ac.uk 2022-12-07T12:58:45Z urn:sha1:660a710778a0fc2a9ccc67ec4285bb53ba57b901 Define bundle, index and reindex for morphisms. 2022-12-06T14:10:10Z Greg Brown greg.brown01@ed.ac.uk 2022-12-06T14:10:10Z urn:sha1:6fb52c637c67788e78bdd1e87a80443aa227d5d6 Redefine reindex in terms of bundle and index. 2022-12-06T14:09:45Z Greg Brown greg.brown01@ed.ac.uk 2022-12-06T14:09:45Z urn:sha1:336c0c8c486bf5323cd44f35e06b3aa25f53bb22 Define setoid reindexing. 2022-12-05T13:08:39Z Greg Brown greg.brown01@ed.ac.uk 2022-12-05T13:08:39Z urn:sha1:3c200003925d2fc623c86f19706bcca7411adc76 Remove import alias. 2022-12-05T11:30:56Z Greg Brown greg.brown01@ed.ac.uk 2022-12-05T11:28:33Z urn:sha1:1e404cee8e3f36a5fe657012db8ba94c5666cec2 Define indexed setoids. 2022-12-02T16:15:31Z Greg Brown greg.brown01@ed.ac.uk 2022-12-02T16:15:31Z urn:sha1:aa13e2ec1d82ddb20888b1f60230de9798081bae