Monus

src/Quantifiers.lagda

@@ -331,6 +331,11 @@ How do the proofs become more difficult if we replace `m * 2` and `1 + m * 2`
 by `2 * m` and `2 * m + 1`?  Rewrite the proofs of `∃-even` and `∃-odd` when
 restated in this way.
 
+### Exercise (`∃-+-≤`)
+
+Show that `y ≤ z` holds if and only if there exists a `x` such that
+`x + y ≡ z`.
+
 
 ## Existentials, Universals, and Negation
 
@@ -388,5 +393,3 @@ This chapter uses the following unicode.
 
     Π  U+03A0  GREEK CAPITAL LETTER PI (\Pi)
     ∃  U+2203  THERE EXISTS (\ex, \exists)
-
-

src/Relations.lagda

@@ -293,9 +293,11 @@ in this case `m` and `n`.  It is equivalent to the following
 indexed datatype.
 \begin{code}
 data Total′ : ℕ → ℕ → Set where
-  forward : ∀ {m n : ℕ} → m ≤ n → Total′ m n
+  forward′ : ∀ {m n : ℕ} → m ≤ n → Total′ m n
-  flipped : ∀ {m n : ℕ} → n ≤ m → Total′ m n
+  flipped′ : ∀ {m n : ℕ} → n ≤ m → Total′ m n
 \end{code}
+Each parameter of the type translates as an implicit
+parameter of each constructor.
 Unlike an indexed datatype, where the indexes can vary
 (as in `zero ≤ n` and `suc m ≤ suc n`), in a parameterised
 datatype the parameters must always be the same (as in `Total m n`).

src/extra/Monus.agda

@@ -0,0 +1,9 @@
+open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≥_; _≤_; z≤n; s≤s)
+open import Function.Equivalence using (_⇔_)
+open import Relation.Binary.PropositionalEquality using (→-to-⟶)
+
+postulate
+  adjoint : ∀ {x y z} → x + y ≥ z ⇔ x ≥ z ∸ y
+  unit : ∀ {x y} → x ≥ (x + y) ∸ y
+  apply : ∀ {x y} → (x ∸ y) + y ≥ x
+