-- Copyright 2020 INP Toulouse.
-- Authors : Mathieu Montin.

-- This version of Unary is provided to you free of charge. It is released under the FSF GPL license, http://www.fsf.org/licenses/gpl.html. 
-- As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users  are provided only 
-- with a limited warranty and the software's author, the holder of the economic rights, and the successive licensors have only limited liability. 
-- In this respect, the user's attention is drawn to the risks associated with loading, using, modifying and/or developing or reproducing the 
-- software by the user in light of its specific status of free software, that may mean that it is complicated to manipulate, and that also there-
-- fore means that it is reserved for developers and experienced professionals having in-depth computer knowledge. Users are therefore encouraged 
-- to load and test the software's suitability as regards their requirements in conditions enabling the security of their systems and/or data to 
-- be ensured and, more generally, to use and operate it in the same conditions as regards security.
-- The fact that you are presently reading this means that you have had knowledge of the FSF GPL version 3 license and that you accept its terms.

module Unary where

open import Data.Nat hiding (_⊔_)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Core
open import Function
open import Agda.Primitive

data Even :   Set where
  zpair : Even zero
  spair :  {a}  Even a  Even (suc (suc a))

record  {a b} {A : Set a} (P : A  Set b) : Set (a  b) where
  constructor _,_ ; field
    witness : A
    proof   : P witness

Evenℕ : Set
Evenℕ =  Even

[_/2] : Evenℕ  
[ .zero , zpair /2] = zero
[ .(suc (suc _)) , spair proof /2] = suc [ _ , proof /2]

_≈_ :  {a b} {A : Set a} {P : A  Set b}  Rel ( P) _
_≈_ =  _≡_ on ∃.witness

uniqueEven :  {n} (p₁ p₂ : Even n)  p₁  p₂
uniqueEven zpair      zpair      = refl
uniqueEven (spair p₁) (spair p₂) = cong spair (uniqueEven p₁ p₂)

equality :  {e₁ e₂ :  Even}  e₁  e₂  e₁  e₂
equality {_ , p} {._ , p₁} refl rewrite uniqueEven p p₁ = refl