{-# OPTIONS --type-in-type #-}

-- Proving induction principles via free theorems from parametricity.
-- The --type-in-type is so that Church-encoded types are still
-- Sets. That may not be necessary, but it avoids things like
-- needing equality and whatnot at multiple levels, and lets one
-- eliminate over the encoded types (which seems handy for the
-- less trivial types).

module ParamInduction where

open import Relation.Binary.PropositionalEquality

const : ∀{A : Set} {B : Set} → (x : A) → B → A
const x _ = x

_⇔_ : Set → Set → Set
A ⇔ B = A → B → Set

infixl 0 _$_
_$_ : ∀{A : Set} {B : A → Set} → ((x : A) → B x) → (x : A) → B x
f $ x = f x

-- Extensionality of functions is something we'll also be needing.
postulate
  ext : {A : Set} {B : A → Set} (f g : (x : A) → B x)
      → (∀ x → f x ≡ g x) → f ≡ g


-- The empty type is the set that entails any other set.
⊥ : Set
⊥ = (R : Set) → R

postulate
  -- ∀ f. f b = b, total functions must be strict
  free-⊥ : {R S : Set} (bot : ⊥) (f : R → S) → f (bot R) ≡ bot S

  pm-⊥ : (A B : Set) (R : A ⇔ B) (b : ⊥) → R (b A) (b B)

-- We don't even need parametricity for the induction principle!
⊥-induction : {P : ⊥ → Set} → (b : ⊥) → P b
⊥-induction {P} b = b (P b)


-- The unit type is the type of the identity function, as it is
-- the only function with that type.
⊤ : Set
⊤ = (R : Set) → R → R

postulate
  pm-⊤ : (A B : Set) (R : A ⇔ B) (u : ⊤) (x : A) (y : B)
       → R x y → R (u A x) (u B y)

-- ∀ f. f ∘ id = id ∘ f
free-⊤ : {R S : Set} (u : ⊤) (f : R → S) → ∀ x → f (u R x) ≡ u S (f x)
free-⊤ {R} {S} u f x = pm-⊤ R S (λ x y → f x ≡ y) u x (f x) refl

id : ⊤
id R x = x

lemma₀ : (u : ⊤) → id ≡ u
lemma₀ u = ext id u λ R → ext (id R) (u R) λ x → free-⊤ u (const x) x

lemma₁ : (u : ⊤) → id ≡ u
lemma₁ u = ext id u λ R → ext (id R) (u R) λ x → 
           pm-⊤ R R (λ _ y → x ≡ y) u x x refl

⊤-induction : {P : ⊤ → Set} → P id → ∀ u → P u
⊤-induction {P} Pid u rewrite lemma₀ u = Pid


-- Standard representation of pairs
_×_ : Set → Set → Set
A × B = (R : Set) → (A → B → R) → R

postulate
  -- Yikes!
  pm-× : ∀{A B} C D 
       → (R₁ : A ⇔ A) (R₂ : B ⇔ B) (R₃ : C ⇔ D) 
       → (p : A × B)
       → (k₀ : A → B → C) (k₁ : A → B → D)
       → (∀ x₀ x₁ y₀ y₁ → R₁ x₀ x₁ → R₂ y₀ y₁ → R₃ (k₀ x₀ y₀) (k₁ x₁ y₁))
       → R₃ (p C k₀) (p D k₁)

-- Bam!
free-× : ∀{A B R S}
       → (f : A → A) (g : B → B)
       → (k₀ : A → B → R) (k₁ : A → B → S)
       → (h : R → S)
       → (p : A × B)
       → (∀ x y → h (k₀ x y) ≡ k₁ (f x) (g y))
       → h (p R k₀) ≡ p S k₁
free-× {A} {B} {R} {S} f g k₀ k₁ h p pf =
  pm-× R S (λ x₀ x₁ → f x₀ ≡ x₁)
           (λ y₀ y₁ → g y₀ ≡ y₁) 
           (λ x y → h x ≡ y)
           p k₀ k₁ λ x₀ x₁ y₀ y₁ fx₀≡x₁ gy₀≡y₁ →
           subst (λ x → h (k₀ x₀ y₀) ≡ k₁ x y₁) fx₀≡x₁
           (subst (λ y → h (k₀ x₀ y₀) ≡ k₁ (f x₀) y) gy₀≡y₁ (pf x₀ y₀))

_,_ : {A B : Set} → A → B → A × B
(x , y) R k = k x y

fst : ∀{A B} → A × B → A
fst {A} pair = pair A (λ x _ → x)

snd : ∀{A B} → A × B → B
snd {B = B} pair = pair B (λ _ y → y)

×-lemma₀ : ∀{A B} → (p : A × B) → p (A × B) _,_ ≡ p
×-lemma₀ {A} {B} p = ext q     p     λ R → 
                     ext (q R) (p R) λ k →
                     free-× (id A) (id B) _,_ k (λ q → q R k) p (λ _ _ → refl)
 where
 q : A × B
 q = p (A × B) _,_

×-lemma₁ : ∀{A B R} → (p : A × B) (k : A → B → R)
         → k (fst p) (snd p) ≡ p R k
×-lemma₁ {A} {B} {R} p k = subst (λ q → k (fst q) (snd q) ≡ p R k) (×-lemma₀ p)
                           (free-× (id A) (id B) _,_ k (λ q → k (fst q) (snd q))
                                 p (λ x y → refl))


×-η : ∀{A B} → (p : A × B) → (fst p , snd p) ≡ p
×-η {A} {B} p = ext (fst p , snd p) p (λ R →
                ext ((fst p , snd p) R) (p R) (λ k →
                ×-lemma₁ p k))


×-induction : ∀{A B} {P : A × B → Set}
            → ((x : A) → (y : B) → P (x , y))
            → (p : A × B) → P p
×-induction {A} {B} {P} f p rewrite sym (×-η p) = f (fst p) (snd p)




Σ : (A : Set) (P : A → Set) → Set
Σ A P = (R : Set) → ((x : A) → P x → R) → R

postulate
  pm-Σ : ∀{A P} C D
       → (R₁ : A ⇔ A) (R₂ : ∀ x₀ x₁ → R₁ x₀ x₁ → P x₀ ⇔ P x₁) (R₃ : C ⇔ D)
       → (p : Σ A P)
       → (k₀ : (x : A) → P x → C) (k₁ : (x : A) → P x → D)
       → (∀ x₀ x₁ → (r : R₁ x₀ x₁) → (w₀ : P x₀) (w₁ : P x₁)
                  → R₂ x₀ x₁ r w₀ w₁ → R₃ (k₀ x₀ w₀) (k₁ x₁ w₁))
       → R₃ (p C k₀) (p D k₁)

_⟩_ : ∀{A P} → (x : A) → P x → Σ A P
(x ⟩ w) R k = k x w

Σ-prelemma : ∀{A P R}
           → (k : (x : A) → P x → R)
           → (x₀ x₁ : A) (eq : x₀ ≡ x₁)
           → (w₀ : P x₀) (w₁ : P x₁)
           → w₀ ≡ subst P (sym eq) w₁
           → k x₀ w₀ ≡ k x₁ w₁
Σ-prelemma k x₀ .x₀ refl .w₁ w₁ refl = refl
           
Σ-lemma₀ : ∀{A P} → (p : Σ A P) → p (Σ A P) _⟩_ ≡ p
Σ-lemma₀ {A} {P} p = ext q     p     λ R →
                     ext (q R) (p R) λ k →
                     pm-Σ (Σ A P) R _≡_
                          (λ x₀ x₁ x₀≡x₁ w₀ w₁ → w₀ ≡ subst P (sym x₀≡x₁) w₁)
                          (λ q e → q R k ≡ e) p _⟩_ k
                          (Σ-prelemma k)
 where
 q : Σ A P
 q = p (Σ A P) _⟩_

module Σ₁ (A : Set) (P : A → Set) where
  Q : Σ A P → Set
  Q q = Σ A λ x → Σ (P x) λ w → q ≡ x ⟩ w

  R₁ : A → A → Set
  R₁ = _≡_

  R₂ : (x₀ x₁ : A) → R₁ x₀ x₁ → P x₀ → P x₁ → Set
  R₂ x₀ x₁ r w₀ w₁ = ⊤

  R₃ : Σ A P → Σ A P → Set
  R₃ _ = Q

Σ-lemma₁ : ∀{A P} → (p : Σ A P) → Σ A λ x → Σ (P x) λ w → p ≡ x ⟩ w
Σ-lemma₁ {A} {P} p = subst Q (Σ-lemma₀ p)
                     (pm-Σ (Σ A P) (Σ A P) R₁ R₂ R₃ p _⟩_ _⟩_
                       (λ x₀ x₁ _ w₀ w₁ _ → x₁ ⟩ (w₁ ⟩ refl)))
 where
 open Σ₁ A P

uncurry : ∀{A : Set} {P : A → Set} {C : Σ A P → Set}
        → (f : (x : A) → (w : P x) → C (x ⟩ w))
        → (p : Σ A P) → C p
uncurry {A} {P} {C} f p = Σ-lemma₁ p (C p) λ x sg →
                          sg (C p) λ w p≡x⟩w →
                          subst C (sym p≡x⟩w) (f x w)

-- If we try to make π₀ use uncurry, then the P (π₀ (x ⟩ w)) result
-- type of the lambda expression in π₁ will be a mess, and we'll need
-- to *prove* that it's equal to P x (substitution with equality
-- postulates is the main culprit, I think). The standard Church-encoding
-- definition normalizes π₀ (x ⟩ w) to x, which is much easier.
π₀ : ∀{A P} → Σ A P → A
π₀ {A} p = p A (λ x _ → x)

π₁ : ∀{A P} → (p : Σ A P) → P (π₀ p)
π₁ {A} {P} p = uncurry {C = λ q → P (π₀ q)} (λ x w → w) p




_⊎_ : Set → Set → Set
A ⊎ B = (R : Set) → (A → R) → (B → R) → R

postulate
  -- Yikes again
  pm-⊎ : ∀{A B} C D
       → (R₁ : A ⇔ A) (R₂ : B ⇔ B) (R₃ : C ⇔ D)
       → (s : A ⊎ B)
       → (l₀ : A → C) (r₀ : B → C)
       → (l₁ : A → D) (r₁ : B → D)
       → (∀ x₀ x₁ → R₁ x₀ x₁ → R₃ (l₀ x₀) (l₁ x₁))
       → (∀ y₀ y₁ → R₂ y₀ y₁ → R₃ (r₀ y₀) (r₁ y₁))
       → R₃ (s C l₀ r₀) (s D l₁ r₁)

free-⊎ : {A B R S : Set}
       → (f : A → A) → (g : B → B)
       → (h : R → S)
       → (l₀ : A → R) → (r₀ : B → R)
       → (l₁ : A → S) → (r₁ : B → S)
       → (s : A ⊎ B)
       → (∀ x → h (l₀ x) ≡ l₁ (f x))
       → (∀ y → h (r₀ y) ≡ r₁ (g y))
       → h (s R l₀ r₀) ≡ s S l₁ r₁
free-⊎ {A} {B} {R} {S} f g h l₀ r₀ l₁ r₁ s pfl pfr =
  pm-⊎ R S (λ x₀ x₁ → f x₀ ≡ x₁)
           (λ y₀ y₁ → g y₀ ≡ y₁)
           (λ x y → h x ≡ y)
           s l₀ r₀ l₁ r₁
           (λ x₀ x₁ fx₀≡x₁ → subst (λ x → h (l₀ x₀) ≡ l₁ x) fx₀≡x₁ (pfl x₀))
           (λ y₀ y₁ gy₀≡y₁ → subst (λ y → h (r₀ y₀) ≡ r₁ y) gy₀≡y₁ (pfr y₀))

inl : ∀{A B} → A → A ⊎ B
inl x R f _ = f x

inr : ∀{A B} → B → A ⊎ B
inr y R _ g = g y


-- A simpler disjunction first
Bool : Set
Bool = (R : Set) → R → R → R

true : Bool
true _ t _ = t

false : Bool
false _ _ f = f

postulate
  pm-B : ∀ A B → (R : A ⇔ B) → (b : Bool) → (x₀ y₀ : A) (x₁ y₁ : B)
               → R x₀ x₁ → R y₀ y₁ → R (b A x₀ y₀) (b B x₁ y₁)

free-B : ∀{R S} → (f : R → S) → (x y : R)
       → (b : Bool) → f (b R x y) ≡ b S (f x) (f y)
free-B {R} {S} f x y b =
  pm-B R S (λ x y → f x ≡ y) b x y (f x) (f y) refl refl

B-lemma₀ : (b : Bool) → b Bool true false ≡ b
B-lemma₀ b = ext c       b       λ R →
             ext (c R)   (b R)   λ t →
             ext (c R t) (b R t) λ f →
             free-B (λ d → d R t f) true false b
 where
 c : Bool
 c = b Bool true false

B-lemma₁ : ∀{A} → (x : A) → (b : Bool) → x ≡ b A x x
B-lemma₁ {A} x b = free-B (const x) x x b

-- This needs the full parametricity theorem, not just the free theorem,
-- as far as I can tell.
B-lemma₂ : ∀{A} → (x y : A) → (b : Bool) → (b A x y ≡ x) ⊎ (b A x y ≡ y)
B-lemma₂ {A} x y b = pm-B A A R b x y x y (inl refl) (inr refl)
 where
 R : A → A → Set
 R _ e = (e ≡ x) ⊎ (e ≡ y)

B-lemma₃ : (b : Bool) → (b ≡ true) ⊎ (b ≡ false)
B-lemma₃ b rewrite sym (B-lemma₀ b) = B-lemma₂ true false b

B-induction : ∀{P : Bool → Set} → P true → P false → ∀ b → P b
B-induction {P} Pt Pf b = B-lemma₃ b (P b)
                          (λ b≡t → subst P (sym b≡t) Pt) 
                          (λ b≡f → subst P (sym b≡f) Pf)







⊎-lemma₀ : ∀{A B} → (s : A ⊎ B) → s (A ⊎ B) inl inr ≡ s
⊎-lemma₀ {A} {B} s = ext t s λ R →
                     ext (t R) (s R) λ l →
                     ext (t R l) (s R l) λ r →
                     free-⊎ (id A) (id B) (λ v → v R l r) inl inr l r s
                            (λ x → refl) (λ y → refl)
 where
 t : A ⊎ B
 t = s (A ⊎ B) inl inr

⊎-lemma₁ : ∀{A B C} → (f : A → C) (g : B → C) → (s : A ⊎ B)
         → (Σ A λ x → s C f g ≡ f x) ⊎ (Σ B λ y → s C f g ≡ g y)
⊎-lemma₁ {A} {B} {C} f g s = pm-⊎ C C _≡_ _≡_ R s f g f g
                             (λ x₀ x₁ x₀≡x₁ → inl (x₁ ⟩ refl))
                             (λ y₀ y₁ y₀≡y₁ → inr (y₁ ⟩ refl)) 
 where
 R : C → C → Set
 R _ e = (Σ A λ x → e ≡ f x) ⊎ (Σ B λ y → e ≡ g y)

⊎-lemma₂ : ∀{A B} → (s : A ⊎ B)
         → (Σ A λ x → s ≡ inl x) ⊎ (Σ B λ y → s ≡ inr y)
⊎-lemma₂ {A} {B} s rewrite sym (⊎-lemma₀ s) = ⊎-lemma₁ inl inr s


⊎-induction : ∀{A B} {P : A ⊎ B → Set} → (∀ x → P (inl x)) → (∀ y → P (inr y))
            → (s : A ⊎ B) → P s
⊎-induction {A} {B} {P} pfl pfr s =
  ⊎-lemma₂ s (P s)
    (λ sg → sg (P s) (λ x s≡inlx → subst P (sym s≡inlx) (pfl x)))
    (λ sg → sg (P s) (λ y s≡inry → subst P (sym s≡inry) (pfr y)))




ℕ : Set
ℕ = (R : Set) → R → (R → R) → R

zero : ℕ
zero R z s = z

suc : ℕ → ℕ
suc n R z s = s (n R z s)

postulate
  pm-ℕ : (A B : Set) (R : A ⇔ B) (s₀ : A → A) (s₁ : B → B) (z₀ : A) (z₁ : B) (n : ℕ)
       → (∀ x₀ x₁ → R x₀ x₁ → R (s₀ x₀) (s₁ x₁))
       → R z₀ z₁ → R (n A z₀ s₀) (n B z₁ s₁)

free-ℕ : {R S : Set} (x : R) (f : R → S) (g : R → R) (h : S → S) (n : ℕ)
       → (∀ x → f (g x) ≡ h (f x))
       → f (n R x g) ≡ n S (f x) h
free-ℕ x f g h n pre = pm-ℕ _ _
                            (λ x y → f x ≡ y) g h x (f x) n 
                            (λ x y pf → subst (λ z → f (g x) ≡ h z) pf (pre x)) refl

ℕ-lemma₀ : (n : ℕ) → n ℕ zero suc ≡ n
ℕ-lemma₀ n = ext (n ℕ zero suc)     n       λ R →
             ext (n ℕ zero suc R)   (n R)   λ z →
             ext (n ℕ zero suc R z) (n R z) λ s →
             free-ℕ zero (λ m → m R z s) suc s n (λ m → refl)

-- I won't argue that things defined this way are handy to work with
data _+_ (A B : Set) : Set where
  inj₁ : A → A + B
  inj₂ : B → A + B

[_^_] : ∀{A B C} → (A → C) → (B → C) → A + B → C
[ f ^ g ] (inj₁ x) = f x
[ f ^ g ] (inj₂ y) = g y

record Sg (A : Set) (T : A → Set) : Set where
  constructor _,,_
  field
    proj₁ : A
    proj₂ : T proj₁
open Sg

ℕ-lemma₁ : ∀{A : Set} z s → (n : ℕ) → (n A z s ≡ z) + (Sg ℕ λ m → n A z s ≡ s (m A z s))
ℕ-lemma₁ {A} z s n = pm-ℕ A A R s s z z n
                       (λ x y → [ (λ y=z → inj₂ (zero ,, cong s y=z))
                                ^ (λ pf → inj₂ (suc (proj₁ pf) ,, cong s (proj₂ pf))) ])
                       (inj₁ refl)
 where
 R : A → A → Set
 R _ e = (e ≡ z) + (Sg ℕ λ m → e ≡ s (m A z s))

{-
induction : {P : ℕ → Set} → P Z → (∀ n → P n → P (S n)) → ∀ n → P n
induction {P} Pz Ps n = {!!}
-}