summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2022-01-06I: 5: c: show being epic and mono is not sufficient to be isoHEADmasterChloe Brown
2022-01-06I: 5: b: characterise epimorphisms of OfPreorderChloe Brown
2022-01-06I: 5: a: characterise epimorphisms of SetoidsChloe Brown
Note that whilst the decidability argument might look suspicious, it can be provided trivially assuming the law of excluded middle.
2022-01-06misc: move contradiction example to exercisesChloe Brown
2022-01-05I: 4: f: characterise monomorphisms of OfPreorderChloe Brown
2022-01-05misc: define OfPreorder categoryChloe Brown
2022-01-05I: 4: e: show retracts are not unique for SetoidsChloe Brown
2022-01-05I: 4: d: demonstrate injections are exactly monomorphisms in Setoidsi-4-b-2Chloe Brown
2022-01-05I: 4: c: show monomorphisms decomposeChloe Brown
2022-01-05I: 4: b: show monomorphisms composeChloe Brown
2022-01-05I: 4: a: prove retract hierarchyChloe Brown
2022-01-05I: 2: b: show isomorphisms decomposeI-2-cChloe Brown
2022-01-05I: 2: a: show isomorphisms composei-1-cChloe Brown
2022-01-05I: 1: b: show ≡ ≇ ≤ in PreordersChloe Brown
2022-01-05misc: instance: define PreordersChloe Brown
2022-01-05I: 1: a: show 2 ≇ 3 in SetoidsChloe Brown
2022-01-05Initial commit.Chloe Brown
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 22:46:33 +0000