{-# OPTIONS --erased-cubical --safe #-}
module Partiality-monad.Inductive where
import Equality.Path as P
open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (⊥)
open import Bijection equality-with-J using (_↔_)
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Partiality-algebra as PA hiding (_∘_)
open import Partiality-algebra.Eliminators as PAE hiding (Arguments)
import Partiality-algebra.Properties
private
variable
a ℓ p q : Level
A : Type a
mutual
infix 10 _⊥
infix 4 _⊑_
abstract
data _⊥ (A : Type a) : Type a where
never : A ⊥
now : A → A ⊥
⨆ : Increasing-sequence A → A ⊥
antisymmetry : x ⊑ y → y ⊑ x → x P.≡ y
⊥-is-set-unused : P.Is-set (A ⊥)
Increasing-sequence : Type ℓ → Type ℓ
Increasing-sequence A =
Σ (ℕ → A ⊥) λ f → ∀ n → f n ⊑ f (suc n)
Is-upper-bound :
{A : Type a} → Increasing-sequence A → A ⊥ → Type a
Is-upper-bound s x = ∀ n → (s [ n ]) ⊑ x
infix 30 _[_]
_[_] : Increasing-sequence A → ℕ → A ⊥
_[_] s n = proj₁ {A = _ → _ ⊥} s n
private
variable
x y z : A ⊥
abstract
data _⊑_ {A : Type a} : A ⊥ → A ⊥ → Type a where
⊑-refl : ∀ x → x ⊑ x
⊑-trans : x ⊑ y → y ⊑ z → x ⊑ z
never⊑ : ∀ x → never ⊑ x
upper-bound : ∀ s → Is-upper-bound s (⨆ s)
least-upper-bound : ∀ s ub → Is-upper-bound s ub → ⨆ s ⊑ ub
⊑-propositional : P.Is-proposition (x ⊑ y)
partiality-algebra : ∀ {a} (A : Type a) → Partiality-algebra a a A
partiality-algebra A = record
{ T = A ⊥
; partiality-algebra-with = record
{ _⊑_ = _⊑_
; never = never′
; now = now′
; ⨆ = ⨆′
; antisymmetry = antisymmetry′
; T-is-set-unused = T-is-set-unused′
; ⊑-refl = ⊑-refl′
; ⊑-trans = ⊑-trans′
; never⊑ = never⊑′
; upper-bound = upper-bound′
; least-upper-bound = least-upper-bound′
; ⊑-propositional = ⊑-propositional′
}
}
where
abstract
never′ : A ⊥
never′ = never
now′ : A → A ⊥
now′ = now
⨆′ : Increasing-sequence A → A ⊥
⨆′ = ⨆
antisymmetry′ : x ⊑ y → y ⊑ x → x ≡ y
antisymmetry′ = λ p q → _↔_.from ≡↔≡ (antisymmetry p q)
T-is-set-unused′ : Is-set (A ⊥)
T-is-set-unused′ =
$⟨ (λ {x y} → ⊥-is-set-unused {x = x} {y = y}) ⟩
P.Is-set (A ⊥) ↝⟨ _↔_.from (H-level↔H-level 2) ⟩□
Is-set (A ⊥) □
⊑-refl′ : (x : A ⊥) → x ⊑ x
⊑-refl′ = ⊑-refl
⊑-trans′ : x ⊑ y → y ⊑ z → x ⊑ z
⊑-trans′ = ⊑-trans
never⊑′ : ∀ x → never′ ⊑ x
never⊑′ = never⊑
upper-bound′ : ∀ s → Is-upper-bound s (⨆′ s)
upper-bound′ = upper-bound
least-upper-bound′ : ∀ s ub → Is-upper-bound s ub → ⨆′ s ⊑ ub
least-upper-bound′ = least-upper-bound
⊑-propositional′ : Is-proposition (x ⊑ y)
⊑-propositional′ {x = x} {y = y} =
$⟨ ⊑-propositional ⟩
P.Is-proposition (x ⊑ y) ↝⟨ _↔_.from (H-level↔H-level 1) ⟩□
Is-proposition (x ⊑ y) □
abstract
eliminators : Elimination-principle p q (partiality-algebra A)
eliminators {A = A} args = record
{ ⊥-rec = ⊥-rec
; ⊑-rec = ⊑-rec
; ⊥-rec-never = refl
; ⊥-rec-now = λ _ → refl
; ⊥-rec-⨆ = λ _ → refl
}
where
module A = PAE.Arguments args
mutual
inc-rec : (s : Increasing-sequence A) → A.Inc A.P A.Q s
inc-rec (s , inc) = (λ n → ⊥-rec (s n))
, (λ n → ⊑-rec (inc n))
⊥-rec : (x : A ⊥) → A.P x
⊥-rec never = A.pe
⊥-rec (now x) = A.po x
⊥-rec (⨆ s) = A.pl s (inc-rec s)
⊥-rec (antisymmetry {x = x} {y = y} p q i) = subst≡→[]≡
{B = A.P}
{eq = antisymmetry p q}
(A.pa p q
(⊥-rec x) (⊥-rec y)
(⊑-rec p) (⊑-rec q))
i
⊥-rec (⊥-is-set-unused {x = x} {y = y} p q i j) = lemma i j
where
⊥-is-set-unused′ : P.Is-set (A ⊥)
⊥-is-set-unused′ = ⊥-is-set-unused
lemma :
P.[ (λ i → P.[ (λ j → A.P (⊥-is-set-unused′ p q i j)) ]
⊥-rec x ≡ ⊥-rec y) ]
(λ i → ⊥-rec (p i)) ≡ (λ i → ⊥-rec (q i))
lemma = P.heterogeneous-UIP
(λ x → _↔_.to (H-level↔H-level 2) (A.pp {x = x}))
(⊥-is-set-unused p q)
_ _
⊑-rec : (x⊑y : x ⊑ y) → A.Q (⊥-rec x) (⊥-rec y) x⊑y
⊑-rec (⊑-refl x) = A.qr x (⊥-rec x)
⊑-rec (⊑-trans {x = x} {y = y} {z = z} p q) = A.qt p q
(⊥-rec x) (⊥-rec y) (⊥-rec z)
(⊑-rec p) (⊑-rec q)
⊑-rec (never⊑ x) = A.qe x (⊥-rec x)
⊑-rec (upper-bound s n) = A.qu s (inc-rec s) n
⊑-rec (least-upper-bound s ub is-ub) = A.ql s ub is-ub
(inc-rec s) (⊥-rec ub)
(λ n → ⊑-rec {x = proj₁ s n}
(is-ub n))
⊑-rec (⊑-propositional {x = x} {y = y} p q i) = lemma i
where
⊑-propositional′ : P.Is-proposition (x ⊑ y)
⊑-propositional′ = ⊑-propositional
lemma : P.[ (λ i → A.Q (⊥-rec x) (⊥-rec y)
(⊑-propositional′ p q i)) ]
⊑-rec p ≡ ⊑-rec q
lemma =
P.heterogeneous-irrelevance
(λ p → _↔_.to (H-level↔H-level 1)
(A.qp (⊥-rec x) (⊥-rec y) p))
module _ {A : Type a} where
open Partiality-algebra (partiality-algebra A) public
hiding (T; _⊑_; _[_]; Increasing-sequence; Is-upper-bound)
renaming ( T-is-set to ⊥-is-set
; equality-characterisation-T to
equality-characterisation-⊥
)
open Partiality-algebra.Properties (partiality-algebra A) public
Arguments : ∀ {a} p q (A : Type a) → Type (a ⊔ lsuc (p ⊔ q))
Arguments p q A = PAE.Arguments p q (partiality-algebra A)
module _ (args : Arguments p q A) where
open Eliminators (eliminators args) public
initial : Initial p q (partiality-algebra A)
initial = eliminators→initiality _ eliminators