pnlph

-- tested with Agda 2.6.0.1
module nat-r where

----------------------------------------------------------------------
-- unary representation
----------------------------------------------------------------------

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

pnlph

module ind-def where

----------------------------------------------------------------------
-- unicode symbols on this file
----------------------------------------------------------------------
-- ℕ  U+2115  DOUBLE-STRUCK CAPITAL N (\bN)
-- →  U+2192  RIGHTWARDS ARROW (\to, \r, \->)
-- ∸  U+2238  DOT MINUS (\.-)
-- ≡  U+2261  IDENTICAL TO (\==)
-- ⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET (\<)

pnlph

{-# OPTIONS --without-K #-}

-- Lemma 1.17 from Jesper Cockx's PhD thesis
-- Dependent Pattern Matching and Proof-Relevant Unification.
-- KU Leuven 2017

module Lemma1-17-h where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

pnlph

{-# OPTIONS --without-K #-}

-- BiInverse definition
-- f : A ≃ B
-- HoTT book
-- 4.3 Bi-invertible maps

module BiInverse where

data _≡_ {A : Set} (x : A) : A → Set where

pnlph

module K-rule where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

-- Enunciation of K-rule
K-rule : Set₁
K-rule = {A : Set}{x : A}(P : x ≡ x → Set)(p : P refl)(e : x ≡ x) → P e

-- Proof of K-rule

pnlph

{-# OPTIONS --without-K #-}

module Theorem where

------------------------------------------------------------------------
-- Definitions needed for Lemma 1.17
-- _≡_; sym; trans; cong; _≃_
------------------------------------------------------------------------

data _≡_ {A : Set} (x : A) : A → Set where

pnlph

module Even where

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

-- Declare _Odd datatype first
-- is to be used by _Even datatype

pnlph

module ReflectionNames where

postulate Name : Set
{-# BUILTIN QNAME Name #-}

data Bool : Set where
  false : Bool
  true : Bool
{-# BUILTIN BOOL Bool #-}
{-# BUILTIN FALSE false #-}

pnlph

module reflection-issue where

open import Data.Nat using (zero)
open import Data.Vec using (_∷_)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Reflection using (con)
open import Data.List using ([])

_ : quoteTerm zero ≡ con (quote zero) []
_ = refl

pnlph

ℕ-induction : (A : ℕ → 𝓤 ̇ ) → A 0 → ((n : ℕ) → A n → A (succ n)) → (n : ℕ) → A n
ℕ-induction A a₀ f = h where h : (n : ℕ) → A n
  h 0        = a₀
  h (succ n) = f n (h n)

ℕ-recursion : (X : 𝓤 ̇ ) → X → (ℕ → X → X) → ℕ → X
ℕ-recursion X = ℕ-induction (λ _ → X)

ℕ-iteration : (X : 𝓤 ̇ ) → X → (X → X) → ℕ → X
ℕ-iteration X x f = ℕ-recursion X x (λ _ x → f x)