title: About the image of the succ function
body: <p>I defined the natural numbers as usually:</p>
  
  <pre><code>data Nat : Set where
    zero : Nat
    succ : Nat → Nat
  </code></pre>
  
  <p>and i.e the number one should be</p>
  
  <pre><code>one : Nat 
  one = succ zero
  </code></pre>
  
  <p>Later on, we can define the image datatype,</p>
  
  <pre><code>data Image_∋_ {A B : Set} (f : A → B) : B -&gt; Set where
    im : (x : A) → Image f ∋ (f x)
  </code></pre>
  
  <p>And to prove something like "the one is in the Image of the successor function" I wrote:</p>
  
  <pre><code>one-succ : Image succ ∋ one
  one-succ  = im zero
  </code></pre>
  
  <p>I would like to have the following.</p>
  
  <ul>
  <li>Define the predecessor function that not allowed zero as an input just its successors. So the next is not valid.</li>
  </ul>
  
  <blockquote>
  <pre><code>pred : Nat → Nat
  pred zero  = zero
  pred (succ n) = n
  </code></pre>
  </blockquote>
  
  <ul>
  <li>I would like to have a variable called Z⁺ representing the positive numbers but using in its definition the image of successor function (Image_∋_ data type defined above).</li>
  </ul>