module Partiality-algebra.Pi where
open import Equality.Propositional
open import Interval using (ext)
open import Logical-equivalence using (_⇔_)
open import Prelude
open import H-level equality-with-J hiding (Type)
open import H-level.Closure equality-with-J
open import Partiality-algebra as PA hiding (id; _∘_)
open Partiality-algebra-with
open Partiality-algebra
at-with :
∀ {a b p q} {A : Set a} {Type : A → Set p} {B : A → Set b}
(P : (x : A) → Partiality-algebra-with (Type x) q (B x)) →
let module P x = Partiality-algebra-with (P x) in
(∃ λ (f : ℕ → (x : A) → Type x) →
∀ n x → P._⊑_ x (f n x) (f (suc n) x)) →
(x : A) → ∃ λ (f : ℕ → Type x) →
∀ n → P._⊑_ x (f n) (f (suc n))
at-with _ s x = Σ-map (λ f n → f n x) (λ f n → f n x) s
at :
∀ {a b p q} {A : Set a} {B : A → Set b}
(P : (x : A) → Partiality-algebra p q (B x)) →
let module P x = Partiality-algebra (P x) in
(∃ λ (f : ℕ → (x : A) → P.Type x) →
∀ n x → P._⊑_ x (f n x) (f (suc n) x)) →
(x : A) → ∃ λ (f : ℕ → P.Type x) →
∀ n → P._⊑_ x (f n) (f (suc n))
at P = at-with (partiality-algebra-with ∘ P)
Π-with : ∀ {a b p q}
(A : Set a) {Type : A → Set p} {B : A → Set b} →
((x : A) → Partiality-algebra-with (Type x) q (B x)) →
Partiality-algebra-with
((x : A) → Type x) (a ⊔ q) ((x : A) → B x)
_⊑_ (Π-with A P) = λ f g → ∀ x → _⊑_ (P x) (f x) (g x)
never (Π-with A P) = λ x → never (P x)
now (Π-with A P) = λ f x → now (P x) (f x)
⨆ (Π-with A P) = λ s x → ⨆ (P x) (at-with P s x)
antisymmetry (Π-with A P) = λ p q → ext λ x →
antisymmetry (P x) (p x) (q x)
Type-UIP-unused (Π-with A P) = _⇔_.to set⇔UIP
(Π-closure ext 2 λ x →
_⇔_.from set⇔UIP
(Type-UIP-unused (P x)))
⊑-refl (Π-with A P) = λ f x → ⊑-refl (P x) (f x)
⊑-trans (Π-with A P) = λ f g x → ⊑-trans (P x) (f x) (g x)
never⊑ (Π-with A P) = λ f x → never⊑ (P x) (f x)
upper-bound (Π-with A P) = λ s n x →
upper-bound (P x) (at-with P s x) n
least-upper-bound (Π-with A P) = λ s ub is-ub x →
least-upper-bound
(P x) (at-with P s x) (ub x)
(λ n → is-ub n x)
⊑-proof-irrelevant (Π-with A P) = _⇔_.to propositional⇔irrelevant
(Π-closure ext 1 λ x →
_⇔_.from propositional⇔irrelevant
(⊑-proof-irrelevant (P x)))
Π : ∀ {a b p q} →
(A : Set a) {B : A → Set b} →
((x : A) → Partiality-algebra p q (B x)) →
Partiality-algebra (a ⊔ p) (a ⊔ q) ((x : A) → B x)
Type (Π A P) = (x : A) → Type (P x)
partiality-algebra-with (Π A P) = Π-with A (partiality-algebra-with ∘ P)