What is the Parigot Mendler encoding? : <p>The following encoding of Nats is used in some Cedille sources:</p>

<pre><code>cNat : ★
cNat = ∀ X : ★ . X ➔ (∀ R : ★ . (R ➔ X) ➔ R ➔ X) ➔ X

cZ : cNat
cZ = Λ X . λ z . λ s . z

cS : ∀ A : ★ . (A ➔ cNat) ➔ A ➔ cNat
cS = Λ A . λ e . λ d . Λ X . λ z . λ s . s · A (λ a . e a · X z s) d
</code></pre>

<p>I wonder if this is a common encoding used in other languages (Agda, Idris, Coq). If so, how can I interpret it, how it works, and how can I construct members of this type?</p>

<p>I've tried applying <code>cS</code> as in:</p>

<pre><code>c0 = cZ
c1 = (cS -CNat (λ p : CNat . p) C0)
c2 = (cS -CNat (λ p : CNat . p) C1)
c3 = (cS -CNat (λ p : CNat . p) C2)
</code></pre>

<p>Which checks, but looks rather weird to me. <code>p</code> could be replaced by any <code>cNat</code> inside lambdas, for example. This doesn't look isomorphic to <code>cNat</code> to me. I guess I don't get this structure.</p>
