{-# OPTIONS --erased-cubical --safe #-}
module Partiality-monad.Inductive.Eliminators where
open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (⊥)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Nat equality-with-J as Nat
open import Partiality-monad.Inductive
Inc-nd : ∀ {a p q}
(A : Type a) (P : Type p)
(Q : P → P → Type q) → Type (p ⊔ q)
Inc-nd A P Q = ∃ λ (p : ℕ → P) → ∀ n → Q (p n) (p (suc n))
record Arguments-nd {a} p q (A : Type a) : Type (a ⊔ lsuc (p ⊔ q)) where
field
P : Type p
Q : P → P → Type q
pe : P
po : (x : A) → P
pl : (s : Increasing-sequence A) (pq : Inc-nd A P Q) → P
pa : (p₁ p₂ : P) (q₁ : Q p₁ p₂) (q₂ : Q p₂ p₁) → p₁ ≡ p₂
ps : Is-set P
qr : (x : A ⊥) (p : P) → Q p p
qt : {x y z : A ⊥} → x ⊑ y → y ⊑ z →
(px py pz : P) → Q px py → Q py pz → Q px pz
qe : (x : A ⊥) (p : P) → Q pe p
qu : (s : Increasing-sequence A) (pq : Inc-nd A P Q) (n : ℕ) →
Q (proj₁ pq n) (pl s pq)
ql : ∀ s (ub : A ⊥) (is-ub : Is-upper-bound s ub) pq (pu : P)
(qu : ∀ n → Q (proj₁ pq n) pu) →
Q (pl s pq) pu
qp : (p₁ p₂ : P) → Is-proposition (Q p₁ p₂)
module _ {a p q} {A : Type a} (args : Arguments-nd p q A) where
open Arguments-nd args
private
args′ : Arguments p q A
args′ = record
{ P = λ _ → P
; Q = λ p-x p-y _ → Q p-x p-y
; pe = pe
; po = po
; pl = pl
; pa = λ x⊑y x⊒y p₁ p₂ q₁ q₂ →
subst (const P) (antisymmetry x⊑y x⊒y) p₁ ≡⟨ subst-const (antisymmetry x⊑y x⊒y) ⟩
p₁ ≡⟨ pa p₁ p₂ q₁ q₂ ⟩∎
p₂ ∎
; pp = ps
; qr = qr
; qt = qt
; qe = qe
; qu = qu
; ql = ql
; qp = λ p-x p-y _ → qp p-x p-y
}
⊥-rec-nd : A ⊥ → P
⊥-rec-nd = ⊥-rec args′
⊑-rec-nd : ∀ {x y} → x ⊑ y → Q (⊥-rec-nd x) (⊥-rec-nd y)
⊑-rec-nd = ⊑-rec args′
inc-rec-nd : Increasing-sequence A → Inc-nd A P Q
inc-rec-nd = inc-rec args′
⊥-rec-nd-never : ⊥-rec-nd never ≡ pe
⊥-rec-nd-never = ⊥-rec-never _
⊥-rec-nd-now : ∀ x → ⊥-rec-nd (now x) ≡ po x
⊥-rec-nd-now = ⊥-rec-now _
⊥-rec-nd-⨆ : ∀ s → ⊥-rec-nd (⨆ s) ≡ pl s (inc-rec-nd s)
⊥-rec-nd-⨆ = ⊥-rec-⨆ _
record Arguments-⊥ {a} p (A : Type a) : Type (a ⊔ lsuc p) where
field
P : A ⊥ → Type p
pe : P never
po : ∀ x → P (now x)
pl : ∀ s (p : ∀ n → P (s [ n ])) → P (⨆ s)
pp : ∀ x → Is-proposition (P x)
module _ {a p} {A : Type a} (args : Arguments-⊥ p A) where
open Arguments-⊥ args
⊥-rec-⊥ : (x : A ⊥) → P x
⊥-rec-⊥ = ⊥-rec (record
{ Q = λ _ _ _ → ⊤
; pe = pe
; po = po
; pl = λ s pq → pl s (proj₁ pq)
; pa = λ _ _ _ _ _ _ → pp _ _ _
; pp = mono₁ 1 (pp _)
; qp = λ _ _ _ _ _ → refl
})
inc-rec-⊥ : (s : ℕ → A ⊥) → ∀ n → P (s n)
inc-rec-⊥ s = ⊥-rec-⊥ ∘ s
⊥-rec-⊥-never : ⊥-rec-⊥ never ≡ pe
⊥-rec-⊥-never = ⊥-rec-never _
⊥-rec-⊥-now : ∀ x → ⊥-rec-⊥ (now x) ≡ po x
⊥-rec-⊥-now = ⊥-rec-now _
⊥-rec-⊥-⨆ : ∀ s → ⊥-rec-⊥ (⨆ s) ≡ pl s (λ n → ⊥-rec-⊥ (s [ n ]))
⊥-rec-⊥-⨆ = ⊥-rec-⨆ _
record Arguments-⊑ {a} q (A : Type a) : Type (a ⊔ lsuc q) where
field
Q : {x y : A ⊥} → x ⊑ y → Type q
qr : ∀ x → Q (⊑-refl x)
qt : ∀ {x y z} (x⊑y : x ⊑ y) (y⊑z : y ⊑ z) →
Q x⊑y → Q y⊑z → Q (⊑-trans x⊑y y⊑z)
qe : ∀ x → Q (never⊑ x)
qu : ∀ s (q : ∀ n → Q (increasing s n)) n →
Q (upper-bound s n)
ql : ∀ s ub is-ub (q : ∀ n → Q (increasing s n))
(qu : ∀ n → Q (is-ub n)) →
Q (least-upper-bound s ub is-ub)
qp : ∀ {x y} (x⊑y : x ⊑ y) →
Is-proposition (Q x⊑y)
module _ {a q} {A : Type a} (args : Arguments-⊑ q A) where
open Arguments-⊑ args
⊑-rec-⊑ : ∀ {x y} (x⊑y : x ⊑ y) → Q x⊑y
⊑-rec-⊑ = ⊑-rec (record
{ P = λ _ → ⊤
; Q = λ _ _ → Q
; pa = λ _ _ _ _ _ _ → refl
; pp = mono (Nat.zero≤ 2) ⊤-contractible
; qr = λ x _ → qr x
; qt = λ x⊑y y⊑z _ _ _ → qt x⊑y y⊑z
; qe = λ x _ → qe x
; qu = λ s pq → qu s (proj₂ pq)
; ql = λ s ub is-ub pq _ → ql s ub is-ub (proj₂ pq)
; qp = λ _ _ → qp
})
inc-rec-⊑ : (s : Increasing-sequence A) → ∀ n → Q (increasing s n)
inc-rec-⊑ (_ , inc) = ⊑-rec-⊑ ∘ inc