Last active
April 11, 2020 20:34
-
-
Save ayberkt/3c8c5e3d4555f7723bbccd7a24702997 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS --cubical --safe #-} | |
| module Problem where | |
| open import Cubical.Core.Everything using ( _≡_ | |
| ; Type | |
| ; Σ | |
| ; Σ-syntax | |
| ; _,_ ) | |
| open import Cubical.Data.Prod using ( _,_; proj₁; proj₂ ) | |
| renaming ( _×_ to _××_ ) | |
| open import Cubical.Data.Sigma.Properties using ( Σ≡ ; ΣProp≡ ) | |
| open import Cubical.Foundations.Prelude using ( J | |
| ; isProp | |
| ; isSet | |
| ; funExt | |
| ; subst | |
| ; cong; refl; sym | |
| ; _≡⟨_⟩_; _∎ | |
| ; transport | |
| ; transportRefl | |
| ; isContr ) | |
| renaming ( isProp→isSet to prop⇒set ) | |
| open import Cubical.Foundations.HLevels using ( hProp | |
| ; isSetHProp | |
| ; isOfHLevelΣ | |
| ; isPropΠ ) | |
| open import Cubical.Data.Sigma using ( sigmaPath→pathSigma | |
| ; pathSigma→sigmaPath ) | |
| open import Cubical.Foundations.Isomorphism using ( isoToPath; iso; section; retract ) | |
| open import Cubical.Foundations.Logic using ( _⇔_; _⇒_; ⇔toPath ) | |
| renaming ( _⊓_ to _∧_ ) | |
| open import Data.Product using ( _×_; uncurry ) | |
| renaming ( proj₁ to π₀ ; proj₂ to π₁ ) | |
| open import Function using (_∘_; id ) | |
| open import Level | |
| variable | |
| ℓ ℓ′ ℓ₀ ℓ₁ ℓ₂ ℓ₃ ℓ₀′ ℓ₁′ ℓ₂′ ℓ₀′′ ℓ₁′′ ℓ₂′′ : Level | |
| variable | |
| A : Type ℓ₀ | |
| B : A → Type ℓ₀ | |
| A₀ : Type ℓ₁ | |
| _is-true : hProp ℓ → Type ℓ | |
| (P , _) is-true = P | |
| infix 5 _is-true | |
| is-true-prop : (P : hProp ℓ) → isProp (P is-true) | |
| is-true-prop (P , P-prop) = P-prop | |
| ∃_ : {A : Type ℓ₀} → (A → hProp ℓ₁) → Type (ℓ₀ ⊔ ℓ₁) | |
| ∃_ {A = A} P = Σ[ x ∈ A ] (P x is-true) | |
| data ∥_∥ (A : Type ℓ) : Type ℓ where | |
| ∣_∣ : A → ∥ A ∥ | |
| squash : (x y : ∥ A ∥) → x ≡ y | |
| ∥∥-prop : (A : Type ℓ) → isProp ∥ A ∥ | |
| ∥∥-prop _ = squash | |
| ∥∥-rec : {X Y : Type ℓ} → isProp Y → (X → Y) → ∥ X ∥ → Y | |
| ∥∥-rec Y-prop f ∣ x ∣ = f x | |
| ∥∥-rec Y-prop f (squash ∣x∣₀ ∣x∣₁ i) = | |
| Y-prop (∥∥-rec Y-prop f ∣x∣₀) (∥∥-rec Y-prop f ∣x∣₁) i | |
| data N₁ {ℓ : Level} : Set ℓ where | |
| tt : N₁ | |
| N₁-prop : {ℓ : Level} → isProp {ℓ = ℓ} N₁ | |
| N₁-prop tt tt = refl | |
| id-∏ : (f g : (x : A) → B x) → ((x : A) → f x ≡ g x) ≡ (f ≡ g) | |
| id-∏ f g = isoToPath (iso F G (λ _ → refl) (λ _ → refl)) | |
| where | |
| F : (∀ x → f x ≡ g x) → f ≡ g | |
| F f~g = λ i x → f~g x i | |
| G : f ≡ g → (∀ x → f x ≡ g x) | |
| G f=g = λ x i → f=g i x | |
| Order : (ℓ₁ : Level) → Type ℓ → Type (ℓ ⊔ suc ℓ₁) | |
| Order {ℓ = ℓ} ℓ₁ A = (A → A → hProp ℓ₁) × isSet A | |
| 𝒫 : Type ℓ → Type (suc ℓ) | |
| 𝒫 {ℓ} A = A → hProp ℓ | |
| Sub : (ℓ₀ : Level) → Set ℓ₁ → Set (suc ℓ₀ ⊔ ℓ₁) | |
| Sub ℓ A = Σ (Set ℓ) (λ I → I → A) | |
| index : Sub ℓ₁ A → Set ℓ₁ | |
| index (I , _) = I | |
| -- Application of a family over X to an index. | |
| _€_ : (ℱ : Sub ℓ₀ A) → index ℱ → A | |
| _€_ (_ , f) = f | |
| infixr 7 _€_ | |
| -- Membership for families. | |
| _ε_ : A → Sub ℓ₁ A → Set _ | |
| x ε S = Σ (index S) (λ i → (S € i) ≡ x) | |
| -- Composition of a family with a function. | |
| _⊚_ : {X : Set ℓ₀} {Y : Set ℓ₁} → (g : X → Y) → (ℱ : Sub ℓ₂ X) → Sub ℓ₂ Y | |
| g ⊚ ℱ = (index ℱ) , g ∘ (_€_ ℱ) | |
| -- Familification of a powerset. | |
| ⟪_⟫ : {A : Type ℓ₀} → (A → hProp ℓ₁) → Sub (ℓ₀ ⊔ ℓ₁) A | |
| ⟪_⟫ {A = A} U = (Σ[ x ∈ A ] (U x is-true)) , π₀ | |
| ∏-set : ((x : A) → isSet (B x)) → isSet ((x : A) → B x) | |
| ∏-set {A = A} B-set f g = NTS | |
| where | |
| rem1 : isProp ((x : A) → f x ≡ g x) | |
| rem1 p q = λ i → λ x → B-set x (f x) (g x) (p x) (q x) i | |
| NTS : isProp (f ≡ g) | |
| NTS p q = subst isProp (id-∏ f g) rem1 p q | |
| 𝒫-set : (A : Type ℓ) → isSet (𝒫 A) | |
| 𝒫-set A = ∏-set λ _ → isSetHProp | |
| variable | |
| U V : 𝒫 A | |
| _⊆⊆_ : {A : Type ℓ} → (A → Type ℓ₀) → (A → Type ℓ₁) → Type (ℓ ⊔ ℓ₀ ⊔ ℓ₁) | |
| _⊆⊆_ {A = A} U V = (x : A) → U x → V x | |
| _⊆_ : {A : Type ℓ} → 𝒫 A → 𝒫 A → hProp ℓ | |
| _⊆_ {A = A} U V = ((λ - → U - is-true) ⊆⊆ (λ - → V - is-true)) , prop | |
| where | |
| prop : isProp ((x : A) → U x is-true → V x is-true) | |
| prop = isPropΠ λ x → isPropΠ λ _ → is-true-prop (V x) | |
| ⊆-antisym : U ⊆ V is-true → V ⊆ U is-true → U ≡ V | |
| ⊆-antisym {U = U} {V} U⊆V V⊆V = funExt (λ x → ⇔toPath (U⊆V x) (V⊆V x)) | |
| _∩_ : 𝒫 A → 𝒫 A → 𝒫 A | |
| _∩_ {A = A} U V = λ x → (U x is-true × V x is-true) , prop x | |
| where | |
| prop : (x : A) → isProp (U x is-true × V x is-true) | |
| prop x = isOfHLevelΣ 1 (is-true-prop (U x)) λ _ → is-true-prop (V x) | |
| module Properties {ℓ ℓ′ : Level} | |
| {X : Set ℓ} | |
| (X-set : isSet X) | |
| (_⊑_ : X → X → hProp ℓ′) where | |
| IsReflexive : hProp (ℓ ⊔ ℓ′) | |
| IsReflexive = ((x : X) → (x ⊑ x) is-true) , isPropΠ λ x → is-true-prop (x ⊑ x) | |
| IsTransitive : hProp (ℓ ⊔ ℓ′) | |
| IsTransitive = φ , φ-prop | |
| where | |
| φ : Set (ℓ ⊔ ℓ′) | |
| φ = ((x y z : X) → (x ⊑ y) is-true → (y ⊑ z) is-true → (x ⊑ z) is-true) | |
| φ-prop : isProp φ | |
| φ-prop = isPropΠ λ x → isPropΠ λ y → isPropΠ λ z | |
| → isPropΠ (λ _ → isPropΠ λ _ → is-true-prop (x ⊑ z)) | |
| IsAntisym : hProp (ℓ ⊔ ℓ′) | |
| IsAntisym = φ , φ-prop | |
| where | |
| φ : Set (ℓ ⊔ ℓ′) | |
| φ = ((x y : X) → (x ⊑ y) is-true → (y ⊑ x) is-true → x ≡ y) | |
| φ-prop : isProp φ | |
| φ-prop = isPropΠ λ x → isPropΠ λ y → | |
| isPropΠ λ p → isPropΠ λ q → X-set x y | |
| PosetAx : (ℓ₁ : Level) (A : Type ℓ₀) → Order ℓ₁ A → hProp (ℓ₀ ⊔ ℓ₁) | |
| PosetAx _ A (_⊑_ , A-set) = IsReflexive ∧ IsTransitive ∧ IsAntisym | |
| where | |
| open Properties A-set _⊑_ | |
| PosetStr : (ℓ₁ : Level) → Type ℓ → Type (ℓ ⊔ suc ℓ₁) | |
| PosetStr ℓ₁ A = Σ (Order ℓ₁ A) (λ RP → PosetAx ℓ₁ A RP is-true) | |
| Poset : (ℓ₀ ℓ₁ : Level) → Type (suc ℓ₀ ⊔ suc ℓ₁) | |
| Poset ℓ₀ ℓ₁ = Σ (Type ℓ₀) (PosetStr ℓ₁) | |
| ∣_∣ₚ : Poset ℓ₀ ℓ₁ → Type ℓ₀ | |
| ∣ X , _ ∣ₚ = X | |
| strₚ : (P : Poset ℓ₀ ℓ₁) → PosetStr ℓ₁ ∣ P ∣ₚ | |
| strₚ (_ , s) = s | |
| rel : (P : Poset ℓ₀ ℓ₁) → ∣ P ∣ₚ → ∣ P ∣ₚ → hProp ℓ₁ | |
| rel (_ , (_⊑_ , _) , _) = _⊑_ | |
| syntax rel P x y = x ⊑[ P ] y | |
| ⊑[_]-refl : (P : Poset ℓ₀ ℓ₁) → (x : ∣ P ∣ₚ) → x ⊑[ P ] x is-true | |
| ⊑[_]-refl (_ , _ , (⊑-refl , _)) = ⊑-refl | |
| ⊑[_]-trans : (P : Poset ℓ₀ ℓ₁) (x y z : ∣ P ∣ₚ) | |
| → x ⊑[ P ] y is-true → y ⊑[ P ] z is-true → x ⊑[ P ] z is-true | |
| ⊑[_]-trans (_ , _ , (_ , ⊑-trans , _)) = ⊑-trans | |
| ⊑[_]-antisym : (P : Poset ℓ₀ ℓ₁) (x y : ∣ P ∣ₚ) | |
| → x ⊑[ P ] y is-true → y ⊑[ P ] x is-true → x ≡ y | |
| ⊑[_]-antisym (_ , _ , (_ , _ , ⊑-antisym)) = ⊑-antisym | |
| carrier-is-set : (P : Poset ℓ₀ ℓ₁) → isSet ∣ P ∣ₚ | |
| carrier-is-set (_ , (_ , is-set) , _) = is-set | |
| module PosetReasoning (P : Poset ℓ₀ ℓ₁) where | |
| _⊑⟨_⟩_ : (x : ∣ P ∣ₚ) {y z : ∣ P ∣ₚ} | |
| → x ⊑[ P ] y is-true → y ⊑[ P ] z is-true → x ⊑[ P ] z is-true | |
| _ ⊑⟨ p ⟩ q = ⊑[ P ]-trans _ _ _ p q | |
| _■ : (x : ∣ P ∣ₚ) → x ⊑[ P ] x is-true | |
| _■ = ⊑[ P ]-refl | |
| infixr 0 _⊑⟨_⟩_ | |
| infix 1 _■ | |
| ≡⇒⊑ : (P : Poset ℓ₀ ℓ₁) → {x y : ∣ P ∣ₚ} → x ≡ y → rel P x y is-true | |
| ≡⇒⊑ P {x = x} p = subst (λ z → x ⊑[ P ] z is-true) p (⊑[ P ]-refl x) | |
| IsMonotonic : (P : Poset ℓ₀ ℓ₁) (Q : Poset ℓ₂ ℓ₃) | |
| → (∣ P ∣ₚ → ∣ Q ∣ₚ) → Type (ℓ₀ ⊔ ℓ₁ ⊔ ℓ₃) | |
| IsMonotonic P Q f = | |
| (x y : ∣ P ∣ₚ) → x ⊑[ P ] y is-true → (f x) ⊑[ Q ] (f y) is-true | |
| IsMonotonic-prop : (P : Poset ℓ₀ ℓ₁) (Q : Poset ℓ₀′ ℓ₁′) (f : ∣ P ∣ₚ → ∣ Q ∣ₚ) | |
| → isProp (IsMonotonic P Q f) | |
| IsMonotonic-prop P Q f = | |
| isPropΠ (λ x → isPropΠ λ y → isPropΠ λ _ → is-true-prop (f x ⊑[ Q ] f y)) | |
| _─m→_ : Poset ℓ₀ ℓ₁ → Poset ℓ₀′ ℓ₁′ → Set (ℓ₀ ⊔ ℓ₁ ⊔ ℓ₀′ ⊔ ℓ₁′) | |
| _─m→_ P Q = Σ (∣ P ∣ₚ → ∣ Q ∣ₚ) (IsMonotonic P Q) | |
| _$ₘ_ = π₀ | |
| _∘m_ : {P : Poset ℓ₀ ℓ₁} {Q : Poset ℓ₀′ ℓ₁′} {R : Poset ℓ₀′′ ℓ₁′′} | |
| → (Q ─m→ R) → (P ─m→ Q) → (P ─m→ R) | |
| (g , pg) ∘m (f , pf) = g ∘ f , λ x y p → pg (f x) (f y) (pf x y p) | |
| 𝟏m : (P : Poset ℓ₀ ℓ₁) → P ─m→ P | |
| 𝟏m P = id , (λ x y x⊑y → x⊑y) | |
| ↓[_]_ : (P : Poset ℓ₀ ℓ₁) → ∣ P ∣ₚ → Type (ℓ₀ ⊔ ℓ₁) | |
| ↓[ P ] a = Σ ∣ P ∣ₚ (λ b → b ⊑[ P ] a is-true) | |
| IsDownwardClosed : (P : Poset ℓ₀ ℓ₁) → (𝒫 ∣ P ∣ₚ) → hProp (ℓ₀ ⊔ ℓ₁) | |
| IsDownwardClosed P@(X , _) D = | |
| ((x y : X) → D x is-true → y ⊑[ P ] x is-true → D y is-true) , prop | |
| where | |
| prop : isProp ((x y : X) → D x is-true → y ⊑[ P ] x is-true → D y is-true) | |
| prop = isPropΠ λ _ → isPropΠ λ x → isPropΠ λ _ → isPropΠ λ _ → | |
| is-true-prop (D x) | |
| DownwardClosedSubset : (P : Poset ℓ₀ ℓ₁) → Set (suc ℓ₀ ⊔ ℓ₁) | |
| DownwardClosedSubset P = Σ (𝒫 ∣ P ∣ₚ) (λ S → IsDownwardClosed P S is-true) | |
| DownwardClosedSubset-set : (P : Poset ℓ₀ ℓ₁) → isSet (DownwardClosedSubset P) | |
| DownwardClosedSubset-set P = | |
| isOfHLevelΣ 2 (𝒫-set ∣ P ∣ₚ) λ x → prop⇒set (is-true-prop (IsDownwardClosed P x)) | |
| -- Formal topology. | |
| InteractionStr : (A : Type ℓ) → Type (suc ℓ) | |
| InteractionStr {ℓ = ℓ} A = | |
| Σ[ B ∈ (A → Type ℓ) ] Σ[ C ∈ ({x : A} → B x → Type ℓ) ]({x : A} → {y : B x} → C y → A) | |
| InteractionSys : (ℓ : Level) → Type (suc ℓ) | |
| InteractionSys ℓ = Σ (Type ℓ) InteractionStr | |
| state : InteractionSys ℓ → Type ℓ | |
| action : (D : InteractionSys ℓ) → state D → Type ℓ | |
| reaction : (D : InteractionSys ℓ) → {x : state D} → action D x → Type ℓ | |
| δ : (D : InteractionSys ℓ) {x : state D} {y : action D x} | |
| → reaction D y → state D | |
| state (A , _ , _ , _) = A | |
| action (_ , B , _ , _) = B | |
| reaction (_ , _ , C , _) = C | |
| δ (_ , _ , _ , d) = d | |
| HasMonotonicity : (P : Poset ℓ₀ ℓ₁) → InteractionStr ∣ P ∣ₚ → Type (ℓ₀ ⊔ ℓ₁) | |
| HasMonotonicity P i = | |
| (a : state IS) (b : action IS a) (c : reaction IS b) → δ IS c ⊑[ P ] a is-true | |
| where | |
| IS : InteractionSys _ | |
| IS = ∣ P ∣ₚ , i | |
| Discipline : (ℓ₀ ℓ₁ : Level) → Type (suc ℓ₀ ⊔ suc ℓ₁) | |
| Discipline ℓ₀ ℓ₁ = | |
| Σ[ P ∈ (Poset ℓ₀ ℓ₁) ] Σ[ IS ∈ (InteractionStr ∣ P ∣ₚ) ] HasMonotonicity P IS | |
| post : (D : Discipline ℓ₀ ℓ₁) → InteractionSys ℓ₀ | |
| post (P , P-disc , _) = ∣ P ∣ₚ , P-disc | |
| module _ (D : Discipline ℓ₀ ℓ₁) where | |
| private | |
| P = π₀ D | |
| str = π₀ (π₁ D) | |
| stage : Type ℓ₀ | |
| stage = state (post D) | |
| exp : stage → Type ℓ₀ | |
| exp = action (post D) | |
| outcome : {x : stage} → exp x → Type ℓ₀ | |
| outcome = reaction (∣ P ∣ₚ , str) | |
| next : {a : stage} → {b : exp a} → outcome b → stage | |
| next = δ (post D) | |
| HasSimulation : Type (ℓ₀ ⊔ ℓ₁) | |
| HasSimulation = | |
| (a₀ a : ∣ P ∣ₚ) → a₀ ⊑[ π₀ D ] a is-true → | |
| (b : exp a) → Σ (exp a₀) (λ b₀ → | |
| (c₀ : outcome b₀) → Σ (outcome b) (λ c → next c₀ ⊑[ π₀ D ] next c is-true)) | |
| FormalTopology : (ℓ₀ ℓ₁ : Level) → Type (suc ℓ₀ ⊔ suc ℓ₁) | |
| FormalTopology ℓ₀ ℓ₁ = Σ[ D ∈ (Discipline ℓ₀ ℓ₁) ] HasSimulation D | |
| RawFrameStr : (ℓ₁ ℓ₂ : Level) → Type ℓ₀ → Type (ℓ₀ ⊔ suc ℓ₁ ⊔ suc ℓ₂) | |
| RawFrameStr ℓ₁ ℓ₂ A = (PosetStr ℓ₁ A) × A × (A → A → A) × (Sub ℓ₂ A → A) | |
| frame-axioms : (A : Type ℓ₀) → RawFrameStr ℓ₁ ℓ₂ A → Set (ℓ₀ ⊔ ℓ₁ ⊔ suc ℓ₂) | |
| frame-axioms {ℓ₀ = ℓ₀} {ℓ₁ = ℓ₁} {ℓ₂ = ℓ₂} O (((_⊑_ , _) , _) , 𝟏 , _⊓_ , ⋃_) = | |
| ((o : O) → o ⊑ 𝟏 is-true) | |
| × ((o p : O) → (o ⊓ p) ⊑ o is-true) | |
| × ((o p : O) → (o ⊓ p) ⊑ p is-true) | |
| × ((o p q : O) → q ⊑ o is-true → q ⊑ p is-true → q ⊑ (o ⊓ p) is-true) | |
| × ((ℱ : Sub ℓ₂ O) → (o : O) → o ε ℱ → o ⊑ (⋃ ℱ) is-true) | |
| × ((ℱ : Sub ℓ₂ O) → (p : O) → ((o : O) → o ε ℱ → o ⊑ p is-true) → (⋃ ℱ) ⊑ p is-true) | |
| × ((o : O) (ℱ : Sub ℓ₂ O) → o ⊓ (⋃ ℱ) ≡ ⋃ (index ℱ , λ i → o ⊓ (ℱ € i))) | |
| FrameStr : (ℓ₁ ℓ₂ : Level) → Type ℓ₀ → Type (ℓ₀ ⊔ suc ℓ₁ ⊔ suc ℓ₂) | |
| FrameStr ℓ₁ ℓ₂ A = Σ (RawFrameStr ℓ₁ ℓ₂ A) (frame-axioms A) | |
| Frame : (ℓ₀ ℓ₁ ℓ₂ : Level) → Type (suc ℓ₀ ⊔ suc ℓ₁ ⊔ suc ℓ₂) | |
| Frame ℓ₀ ℓ₁ ℓ₂ = Σ (Type ℓ₀) (FrameStr ℓ₁ ℓ₂) | |
| -- Projection for the carrier set of a frame | |
| -- i.e., the carrier set of the underlying poset. | |
| ∣_∣F : Frame ℓ₀ ℓ₁ ℓ₂ → Type ℓ₀ | |
| ∣ A , _ ∣F = A | |
| -- The underlying poset of a frame. | |
| pos : Frame ℓ₀ ℓ₁ ℓ₂ → Poset ℓ₀ ℓ₁ | |
| pos (A , (P , _) , _) = A , P | |
| 𝟏[_] : (F : Frame ℓ₀ ℓ₁ ℓ₂) → ∣ F ∣F | |
| 𝟏[ _ , (_ , (𝟏 , _)) , _ ] = 𝟏 | |
| glb-of : (F : Frame ℓ₀ ℓ₁ ℓ₂) → ∣ F ∣F → ∣ F ∣F → ∣ F ∣F | |
| glb-of (_ , (_ , _ , _⊓_ , _) , _) = _⊓_ | |
| syntax glb-of F o p = o ⊓[ F ] p | |
| ⋃[_]_ : (F : Frame ℓ₀ ℓ₁ ℓ₂) → Sub ℓ₂ ∣ F ∣F → ∣ F ∣F | |
| ⋃[ (_ , (_ , (_ , _ , ⋃_)) , _) ] ℱ = ⋃ ℱ | |
| module _ (F : Frame ℓ₀ ℓ₁ ℓ₂) where | |
| private | |
| P = pos F | |
| _⊑_ : ∣ F ∣F → ∣ F ∣F → hProp ℓ₁ | |
| x ⊑ y = x ⊑[ P ] y | |
| 𝟏[_]-top : (o : ∣ F ∣F) → o ⊑[ pos F ] 𝟏[ F ] is-true | |
| 𝟏[_]-top = let (_ , _ , (top , _)) = F in top | |
| ⊓[_]-lower₀ : (o p : ∣ F ∣F) → (o ⊓[ F ] p) ⊑[ pos F ] o is-true | |
| ⊓[_]-lower₀ = let (_ , (_ , _ , (φ , _))) = F in φ | |
| ⊓[_]-lower₁ : (o p : ∣ F ∣F) → (o ⊓[ F ] p) ⊑[ pos F ] p is-true | |
| ⊓[_]-lower₁ = let (_ , (_ , _ , (_ , φ , _))) = F in φ | |
| ⊓[_]-greatest : (o p q : ∣ F ∣F) | |
| → q ⊑[ pos F ] o is-true | |
| → q ⊑[ pos F ] p is-true | |
| → q ⊑[ pos F ] (o ⊓[ F ] p) is-true | |
| ⊓[_]-greatest = let (_ , (_ , _ , (_ , _ , φ , _))) = F in φ | |
| ⋃[_]-upper : (ℱ : Sub ℓ₂ ∣ F ∣F) (o : ∣ F ∣F) → o ε ℱ → o ⊑[ pos F ] (⋃[ F ] ℱ) is-true | |
| ⋃[_]-upper = let (_ , (_ , _ , (_ , _ , _ , φ , _))) = F in φ | |
| ⋃[_]-least : (ℱ : Sub ℓ₂ ∣ F ∣F) (p : ∣ F ∣F) | |
| → ((o : ∣ F ∣F) → o ε ℱ → o ⊑[ pos F ] p is-true) | |
| → (⋃[ F ] ℱ) ⊑[ pos F ] p is-true | |
| ⋃[_]-least = let (_ , (_ , _ , (_ , _ , _ , _ , φ , _))) = F in φ | |
| dist : (o : ∣ F ∣F) (ℱ : Sub ℓ₂ ∣ F ∣F) | |
| → o ⊓[ F ] (⋃[ F ] ℱ) ≡ ⋃[ F ] ((λ - → o ⊓[ F ] -) ⊚ ℱ) | |
| dist = let (_ , (_ , _ , (_ , _ , _ , _ , _ , φ))) = F in φ | |
| ⊓-unique : (x y z : ∣ F ∣F) | |
| → z ⊑[ P ] x is-true | |
| → z ⊑[ P ] y is-true | |
| → ((w : ∣ F ∣F) → w ⊑[ P ] x is-true → w ⊑[ P ] y is-true → w ⊑[ P ] z is-true) | |
| → z ≡ x ⊓[ F ] y | |
| ⊓-unique x y z z⊑x z⊑y greatest = | |
| ⊑[ P ]-antisym z (x ⊓[ F ] y) (⊓[_]-greatest x y z z⊑x z⊑y) NTS | |
| where | |
| NTS : (x ⊓[ F ] y) ⊑[ P ] z is-true | |
| NTS = greatest (x ⊓[ F ] y) (⊓[_]-lower₀ x y) (⊓[_]-lower₁ x y) | |
| ⋃-unique : (ℱ : Sub ℓ₂ ∣ F ∣F) (z : ∣ F ∣F) | |
| → ((o : ∣ F ∣F) → o ε ℱ → o ⊑ z is-true) | |
| → ((w : ∣ F ∣F) → ((o : ∣ F ∣F) → o ε ℱ → o ⊑ w is-true) → z ⊑ w is-true) | |
| → z ≡ ⋃[ F ] ℱ | |
| ⋃-unique ℱ z upper least = | |
| ⊑[ P ]-antisym z (⋃[ F ] ℱ) (least (⋃[ F ] ℱ) (⋃[_]-upper ℱ)) NTS | |
| where | |
| NTS : (⋃[ F ] ℱ) ⊑ z is-true | |
| NTS = ⋃[_]-least ℱ z upper | |
| comm : (x y : ∣ F ∣F) → x ⊓[ F ] y ≡ y ⊓[ F ] x | |
| comm x y = ⊓-unique y x _ (⊓[_]-lower₁ x y) (⊓[_]-lower₀ x y) NTS | |
| where | |
| NTS = λ w w⊑y w⊑x → ⊓[_]-greatest x y w w⊑x w⊑y | |
| family-iff : {ℱ 𝒢 : Sub ℓ₂ ∣ F ∣F} | |
| → ((x : ∣ F ∣F) → (x ε ℱ → x ε 𝒢) × (x ε 𝒢 → x ε ℱ)) | |
| → ⋃[ F ] ℱ ≡ ⋃[ F ] 𝒢 | |
| family-iff {ℱ = ℱ} {𝒢 = 𝒢} h = ⋃-unique _ _ ub least | |
| where | |
| ub : (o : ∣ F ∣F) → o ε 𝒢 → (o ⊑ (⋃[ F ] ℱ)) is-true | |
| ub o (i , p) = subst | |
| (λ - → - ⊑[ pos F ] (⋃[ F ] ℱ) is-true) | |
| p | |
| (⋃[ _ ]-upper _ (π₁ (h (𝒢 € i)) (i , refl))) | |
| least : (w : ∣ F ∣F) | |
| → ((o : ∣ F ∣F) → o ε 𝒢 → o ⊑ w is-true) | |
| → (⋃[ F ] ℱ) ⊑ w is-true | |
| least w f = ⋃[ _ ]-least _ λ o oεℱ → f o (π₀ (h o) oεℱ) | |
| flatten : (I : Type ℓ₂) (J : I → Type ℓ₂) (f : (i : I) → J i → ∣ F ∣F) | |
| → ⋃[ F ] (Σ I J , λ { (x , y) → f x y }) | |
| ≡ ⋃[ F ] (I , λ i → ⋃[ F ] (J i , λ y → f i y)) | |
| flatten I J f = ⊑[ pos F ]-antisym _ _ down up | |
| where | |
| open PosetReasoning (pos F) using (_⊑⟨_⟩_; _■) | |
| LHS = ⋃[ F ] (Σ I J , (λ { (x , y) → f x y })) | |
| RHS = ⋃[ F ] (I , (λ i → ⋃[ F ] (J i , f i))) | |
| down : LHS ⊑[ pos F ] RHS is-true | |
| down = ⋃[_]-least _ _ isUB | |
| where | |
| isUB : (o : ∣ F ∣F) | |
| → o ε (Σ I J , (λ { (x , y) → f x y })) | |
| → o ⊑[ pos F ] RHS is-true | |
| isUB o ((i , j) , eq) = | |
| o ⊑⟨ ≡⇒⊑ (pos F) (sym eq) ⟩ | |
| f i j ⊑⟨ ⋃[_]-upper _ _ (j , refl) ⟩ | |
| ⋃[ F ] (J i , λ - → f i -) ⊑⟨ ⋃[_]-upper _ _ (i , refl) ⟩ | |
| RHS ■ | |
| up : RHS ⊑[ pos F ] LHS is-true | |
| up = ⋃[_]-least _ _ isUB | |
| where | |
| isUB : (o : ∣ F ∣F) | |
| → o ε (I , (λ i → ⋃[ F ] (J i , f i))) | |
| → o ⊑[ pos F ] (⋃[ F ] (Σ I J , (λ { (x , y) → f x y }))) is-true | |
| isUB o (i , eq) = | |
| o ⊑⟨ ≡⇒⊑ (pos F) (sym eq) ⟩ | |
| ⋃[ F ] (J i , λ y → f i y) ⊑⟨ ⋃[_]-least _ _ isUB′ ⟩ | |
| ⋃[ F ] (Σ I J , (λ { (x , y) → f x y })) ■ | |
| where | |
| isUB′ : (z : ∣ F ∣F) → z ε (J i , (λ y → f i y)) → z ⊑[ pos F ] LHS is-true | |
| isUB′ z (j , eq′) = ⋃[_]-upper _ _ ((i , j) , eq′) | |
| -- Frame homomorphisms. | |
| IsFrameHomomorphism : (F G : Frame ℓ₀ ℓ₁ ℓ₂) | |
| → (m : pos F ─m→ pos G) | |
| → Type (ℓ₀ ⊔ suc ℓ₂) | |
| IsFrameHomomorphism {ℓ₀ = ℓ₀} {ℓ₁ = ℓ₁} {ℓ₂ = ℓ₂} F G m = | |
| resp-𝟏 × resp-⊓ × resp-⋃ | |
| where | |
| resp-𝟏 : Type ℓ₀ | |
| resp-𝟏 = m $ₘ 𝟏[ F ] ≡ 𝟏[ G ] | |
| resp-⊓ : Type ℓ₀ | |
| resp-⊓ = (x y : ∣ F ∣F) → m $ₘ (x ⊓[ F ] y) ≡ (m $ₘ x) ⊓[ G ] (m $ₘ y) | |
| resp-⋃ : Type (ℓ₀ ⊔ suc ℓ₂) | |
| resp-⋃ = (ℱ : Sub ℓ₂ ∣ F ∣F) → m $ₘ (⋃[ F ] ℱ) ≡ ⋃[ G ] (π₀ m ⊚ ℱ) | |
| IsFrameHomomorphism-prop : (F G : Frame ℓ₀ ℓ₁ ℓ₂) | |
| → (m : pos F ─m→ pos G) | |
| → isProp (IsFrameHomomorphism F G m) | |
| IsFrameHomomorphism-prop F G m = | |
| isOfHLevelΣ 1 (carrier-is-set (pos G) _ _) λ _ → | |
| isOfHLevelΣ 1 (isPropΠ λ x → isPropΠ λ y → carrier-is-set (pos G) _ _) λ _ → | |
| isPropΠ λ ℱ → carrier-is-set (pos G) _ _ | |
| _─f→_ : Frame ℓ₀ ℓ₁ ℓ₂ → Frame ℓ₀ ℓ₁ ℓ₂ → Type (ℓ₀ ⊔ ℓ₁ ⊔ suc ℓ₂) | |
| _─f→_ {ℓ₀ = ℓ₀} {ℓ₁ = ℓ₁} {ℓ₂ = ℓ₂} F G = Σ (pos F ─m→ pos G) (IsFrameHomomorphism F G) | |
| downward-subset-poset : (P : Poset ℓ₀ ℓ₁) → Poset (suc ℓ₀ ⊔ ℓ₁) ℓ₀ | |
| downward-subset-poset {ℓ₀ = ℓ₀} {ℓ₁ = ℓ₁} (A , P) = | |
| 𝔻 , (_<<_ , DownwardClosedSubset-set (A , P)) , <<-refl , <<-trans , <<-antisym | |
| where | |
| 𝔻 = DownwardClosedSubset (A , P) | |
| _<<_ : 𝔻 → 𝔻 → hProp ℓ₀ | |
| _<<_ (S , _) (T , _) = S ⊆ T | |
| open Properties (DownwardClosedSubset-set (A , P)) _<<_ | |
| renaming ( IsReflexive to <<-IsReflexive | |
| ; IsTransitive to <<-IsTransitive | |
| ; IsAntisym to <<-IsAntisym) | |
| abstract | |
| <<-refl : <<-IsReflexive is-true | |
| <<-refl (U , U-down) x xεU = xεU | |
| <<-trans : <<-IsTransitive is-true | |
| <<-trans _ _ _ S<<T T<<U x xεS = T<<U x (S<<T x xεS) | |
| abstract | |
| <<-antisym : <<-IsAntisym is-true | |
| <<-antisym X Y S⊆T T⊆S = | |
| ΣProp≡ (is-true-prop ∘ IsDownwardClosed (A , P)) (⊆-antisym S⊆T T⊆S) | |
| -- The set of downward-closed subsets of a poset forms a frame. | |
| downward-subset-frame : (P : Poset ℓ₀ ℓ₁) → Frame (suc ℓ₀ ⊔ ℓ₁) ℓ₀ ℓ₀ | |
| downward-subset-frame {ℓ₀ = ℓ₀} {ℓ₁ = ℓ₁} (X , P) = | |
| 𝔻 | |
| , (strₚ 𝔻ₚ , 𝟏 , (_⊓_ , ⊔_)) | |
| , 𝟏-top , ⊓-lower₀ , ⊓-lower₁ , ⊓-greatest , ⊔-upper , ⊔-least , distr | |
| where | |
| 𝔻ₚ = downward-subset-poset (X , P) | |
| 𝔻 = ∣ 𝔻ₚ ∣ₚ | |
| ∣_∣𝔻 : 𝔻 → 𝒫 X | |
| ∣ S , _ ∣𝔻 = S | |
| 𝟏 = (λ _ → N₁ , N₁-prop) , λ _ _ _ _ → tt | |
| ∩-down : (S T : 𝒫 X) | |
| → IsDownwardClosed (X , P) S is-true | |
| → IsDownwardClosed (X , P) T is-true | |
| → IsDownwardClosed (X , P) (S ∩ T) is-true | |
| ∩-down S T S↓ T↓ x y x∈S∩T y⊑x = S↓ x y (π₀ x∈S∩T) y⊑x , T↓ x y (π₁ x∈S∩T) y⊑x | |
| _⊓_ : 𝔻 → 𝔻 → 𝔻 | |
| (S , S-dc) ⊓ (T , T-dc) = (S ∩ T) , ∩-down S T S-dc T-dc | |
| 𝟏-top : (D : 𝔻) → (D ⊑[ 𝔻ₚ ] 𝟏) is-true | |
| 𝟏-top D _ _ = tt | |
| -- Given a family ℱ over 𝔻 and some x : X, `in-some-set ℱ x` holds iff there is some | |
| -- set S among ℱ such that x ∈ S. | |
| in-some-set-of : (ℱ : Sub ℓ₀ 𝔻) → X → Set ℓ₀ | |
| in-some-set-of ℱ x = Σ (index ℱ) (λ i → ∣ ℱ € i ∣𝔻 x is-true) | |
| ⊔_ : Sub ℓ₀ 𝔻 → 𝔻 | |
| ⊔ ℱ = (λ x → ∥ in-some-set-of ℱ x ∥ , ∥∥-prop _) , ⊔ℱ↓ | |
| where | |
| ind : (x y : X) | |
| → y ⊑[ (X , P) ] x is-true → in-some-set-of ℱ x → ∥ in-some-set-of ℱ y ∥ | |
| ind x y y⊑x (i , x∈ℱᵢ) = ∣ i , π₁ (ℱ € i) x y x∈ℱᵢ y⊑x ∣ | |
| ⊔ℱ↓ : IsDownwardClosed (X , P) (λ x → ∥ in-some-set-of ℱ x ∥ , ∥∥-prop _) is-true | |
| ⊔ℱ↓ x y ∣p∣ y⊑x = ∥∥-rec (∥∥-prop _) (ind x y y⊑x) ∣p∣ | |
| ⊔-upper : (ℱ : Sub ℓ₀ 𝔻) (D : 𝔻) → D ε ℱ → D ⊑[ 𝔻ₚ ] (⊔ ℱ) is-true | |
| ⊔-upper ℱ D DεS@(i , p) x x∈D = ∣ i , subst (λ V → ∣ V ∣𝔻 x is-true) (sym p) x∈D ∣ | |
| ⊔-least : (ℱ : Sub ℓ₀ 𝔻) (z : 𝔻) | |
| → ((o : 𝔻) → o ε ℱ → (o ⊑[ 𝔻ₚ ] z) is-true) | |
| → (⊔ ℱ) ⊑[ 𝔻ₚ ] z is-true | |
| ⊔-least ℱ D φ x x∈⊔S = ∥∥-rec (π₁ (∣ D ∣𝔻 x)) ind x∈⊔S | |
| where | |
| ind : in-some-set-of ℱ x → ∣ D ∣𝔻 x is-true | |
| ind (i , x∈ℱᵢ) = φ (ℱ € i) (i , refl) x x∈ℱᵢ | |
| ⊓-lower₀ : (D E : 𝔻) → (D ⊓ E) ⊑[ 𝔻ₚ ] D is-true | |
| ⊓-lower₀ D E x (x∈D , _) = x∈D | |
| ⊓-lower₁ : (D E : 𝔻) → (D ⊓ E) ⊑[ 𝔻ₚ ] E is-true | |
| ⊓-lower₁ D E x (_ , x∈F) = x∈F | |
| ⊓-greatest : (D E F : 𝔻) | |
| → F ⊑[ 𝔻ₚ ] D is-true → F ⊑[ 𝔻ₚ ] E is-true → F ⊑[ 𝔻ₚ ] (D ⊓ E) is-true | |
| ⊓-greatest D E F F<<D F<<E x x∈F = (F<<D x x∈F) , (F<<E x x∈F) | |
| distr : (D : 𝔻) (ℱ : Sub ℓ₀ 𝔻) → D ⊓ (⊔ ℱ) ≡ ⊔ (index ℱ , λ i → D ⊓ (ℱ € i)) | |
| distr D ℱ = ⊑[ 𝔻ₚ ]-antisym (D ⊓ (⊔ ℱ)) (⊔ (index ℱ , λ i → D ⊓ (ℱ € i))) down up | |
| where | |
| 𝒜 = ∣ D ⊓ (⊔ ℱ) ∣𝔻 | |
| ℬ = ∣ ⊔ (index ℱ , (λ i → D ⊓ (ℱ € i))) ∣𝔻 | |
| down : (x : X) → 𝒜 x is-true → ℬ x is-true | |
| down x x∈𝒜@(x∈D , x∈⊔ℱ) = ∥∥-rec (∥∥-prop _) ind x∈⊔ℱ | |
| where | |
| ind : in-some-set-of ℱ x → ∥ in-some-set-of (index ℱ , λ i → D ⊓ (ℱ € i)) x ∥ | |
| ind (i , x∈ℱᵢ) = ∣ i , x∈D , x∈ℱᵢ ∣ | |
| up : (x : X) → ℬ x is-true → 𝒜 x is-true | |
| up x x∈ℬ = | |
| ∥∥-rec (isOfHLevelΣ 1 (is-true-prop (∣ D ∣𝔻 x)) λ _ → | |
| is-true-prop (∣ ⊔ ℱ ∣𝔻 x)) φ x∈ℬ | |
| where | |
| φ : in-some-set-of (index ℱ , λ j → D ⊓ (ℱ € j)) x | |
| → (∣ D ∣𝔻 x is-true) × ∣ ⊔ ℱ ∣𝔻 x is-true | |
| φ (i , x∈D , x∈ℱᵢ) = x∈D , ∣ i , x∈ℱᵢ ∣ | |
| module Test (P : Type ℓ) | |
| (_⊑_ : P → P → Type ℓ′) | |
| (exp : P → Type ℓ) | |
| (out : {a : P} → exp a → Type ℓ) | |
| (rev : {a : P} → {b : exp a} → out b → P) | |
| (mono : (a : P) → (b : exp a) → (c : out b) → rev c ⊑ a) | |
| (sim : (a₀ a : P) | |
| → a₀ ⊑ a | |
| → (b : exp a) | |
| → Σ (exp a₀) | |
| (λ b₀ → (c₀ : out b₀) → | |
| Σ (out b) (λ c → (rev c₀) ⊑ (rev c)))) | |
| where | |
| IsDownwardClosed′ : (P → Type ℓ₀) → Type (ℓ ⊔ ℓ′ ⊔ ℓ₀) | |
| IsDownwardClosed′ U = {a₀ a : P} → U a → a₀ ⊑ a → U a₀ | |
| data _<|_ (a : P) (U : P → Type ℓ) : Type ℓ where | |
| dir : U a → a <| U | |
| branch : (b : exp a) → (f : (c : out b) → rev c <| U) → a <| U | |
| squash : (p₀ p₁ : a <| U) → p₀ ≡ p₁ | |
| <|-prop : (a : P) (U : P → Type ℓ) → isProp (a <| U) | |
| <|-prop a U = squash | |
| private | |
| _∩∩_ : (P → Type ℓ₀) → (P → Type ℓ₁) → P → Type (ℓ₀ ⊔ ℓ₁) | |
| U ∩∩ V = λ x → U x × V x | |
| ∩-comm : (U : P → Type ℓ₀) → (V : P → Type ℓ₁) | |
| → (a : P) → ((V ∩∩ U) a → (U ∩∩ V) a) × ((U ∩∩ V) a → (V ∩∩ U) a) | |
| ∩-comm U V a = V∩U⇒U∩V , U∩V⇒V∩U | |
| where | |
| V∩U⇒U∩V : (V ∩∩ U) a → (U ∩∩ V) a | |
| V∩U⇒U∩V (aεV , aεU) = aεU , aεV | |
| U∩V⇒V∩U : (U ∩∩ V) a → (V ∩∩ U) a | |
| U∩V⇒V∩U (aεU , aεV) = aεV , aεU | |
| <|-∩-comm : {U : P → Type ℓ} {V : P → Type ℓ} | |
| → (a : P) → a <| (V ∩∩ U) → a <| (U ∩∩ V) | |
| <|-∩-comm {U = U} {V} a (dir p) = dir (π₀ (∩-comm U V a) p) | |
| <|-∩-comm {U = U} {V} a (branch b f) = branch b (λ c → <|-∩-comm (rev c) (f c)) | |
| <|-∩-comm {U = U} {V} a (squash p₀ p₁ i) = squash (<|-∩-comm a p₀) (<|-∩-comm a p₁) i | |
| module _ {U : P → Type ℓ} (U-down : IsDownwardClosed′ U) where | |
| lem1 : {a a′ : P} → a′ ⊑ a → a <| U → a′ <| U | |
| lem1 {_} {_} h (squash p₀ p₁ i) = squash (lem1 h p₀) (lem1 h p₁) i | |
| lem1 {_} {_} h (dir q) = dir (U-down q h) | |
| lem1 {a = a} {a′} h (branch b f) = branch b′ g | |
| where | |
| b′ : exp a′ | |
| b′ = π₀ (sim a′ a h b) | |
| g : (c′ : out b′) → rev c′ <| U | |
| g c′ = lem1 (π₁ (π₁ (sim a′ a h b) c′)) (f (π₀ (π₁ (sim a′ a h b) c′))) | |
| lem4 : (a : P) (U : P → Type ℓ) (V : P → Type ℓ) | |
| → a <| U → ((u : P) → U u → u <| V) → a <| V | |
| lem4 a U V (squash p₀ p₁ i) h = squash (lem4 a U V p₀ h) (lem4 a U V p₁ h) i | |
| lem4 a U V (dir p) h = h a p | |
| lem4 a U V (branch b f) h = branch b (λ c → lem4 (rev c) U V (f c) h) | |
| module _ {U : P → Type ℓ} {V : P → Type ℓ} | |
| (U-down : IsDownwardClosed′ U) (V-down : IsDownwardClosed′ V) where | |
| lem2 : {a : P} → a <| U → V a → a <| (U ∩∩ V) | |
| lem2 {a = a} (squash p₀ p₁ i) h = squash (lem2 p₀ h) (lem2 p₁ h) i | |
| lem2 {a = a} (dir q) h = dir (q , h) | |
| lem2 {a = a} (branch b f) h = branch b (λ c → lem2 (f c) (V-down h (mono a b c))) | |
| module _ (U : P → Type ℓ) (V : P → Type ℓ) | |
| (U-down : IsDownwardClosed′ U) (V-down : IsDownwardClosed′ V) where | |
| lem3 : (a a′ : P) → a′ ⊑ a → a′ <| U → a <| V → a′ <| (U ∩∩ V) | |
| lem3 a a′ h (squash p₀ p₁ i) q = squash (lem3 a a′ h p₀ q) (lem3 a a′ h p₁ q) i | |
| lem3 a a′ h (dir p) q = <|-∩-comm a′ (lem2 V-down U-down (lem1 V-down h q) p) | |
| lem3 a a′ h (branch b f) q = branch b g | |
| where | |
| g : (c : out b) → rev c <| (U ∩∩ V) | |
| g c = lem3 a′ (rev c) (mono a′ b c) (f c) (lem1 V-down h q) | |
| -- A predicate expressing whether a function is a nucleus. | |
| IsNuclear : (L : Frame ℓ₀ ℓ₁ ℓ₂) → (∣ L ∣F → ∣ L ∣F) → Set (ℓ₀ ⊔ ℓ₁) | |
| IsNuclear L j = I × II × III | |
| where | |
| I = (a b : ∣ L ∣F) → j (a ⊓[ L ] b) ≡ (j a) ⊓[ L ] (j b) | |
| II = (a : ∣ L ∣F) → a ⊑[ pos L ] (j a) is-true | |
| III = (a : ∣ L ∣F) → j (j a) ⊑[ pos L ] j a is-true | |
| -- The type of nuclei. | |
| Nucleus : Frame ℓ₀ ℓ₁ ℓ₂ → Set (ℓ₀ ⊔ ℓ₁) | |
| Nucleus L = Σ (∣ L ∣F → ∣ L ∣F) (IsNuclear L) | |
| mono : (L : Frame ℓ₀ ℓ₁ ℓ₂) → (N : Nucleus L) | |
| → let j = π₀ N | |
| in (x y : ∣ L ∣F) → x ⊑[ pos L ] y is-true → (j x) ⊑[ pos L ] (j y) is-true | |
| mono L (j , n₀ , n₁ , n₂) x y x⊑y = | |
| j x ⊑⟨ ≡⇒⊑ (pos L) (cong j x≡x⊓y) ⟩ | |
| j (x ⊓[ L ] y) ⊑⟨ ≡⇒⊑ (pos L) (n₀ x y) ⟩ | |
| j x ⊓[ L ] j y ⊑⟨ ⊓[ L ]-lower₁ (j x) (j y) ⟩ | |
| j y ■ | |
| where | |
| open PosetReasoning (pos L) using (_⊑⟨_⟩_; _■) | |
| x⊑x⊓y : x ⊑[ pos L ] (x ⊓[ L ] y) is-true | |
| x⊑x⊓y = ⊓[ L ]-greatest x y x (⊑[ pos L ]-refl x) x⊑y | |
| x≡x⊓y : x ≡ (x ⊓[ L ] y) | |
| x≡x⊓y = ⊑[ pos L ]-antisym x (x ⊓[ L ] y) x⊑x⊓y (⊓[ L ]-lower₀ x y) | |
| -- The set of fixed points for a nucleus `j` forms a poset. | |
| nuclear-fixed-point-poset : (L : Frame ℓ₀ ℓ₁ ℓ₂) → (N : Nucleus L) → Poset ℓ₀ ℓ₁ | |
| nuclear-fixed-point-poset {ℓ₀ = ℓ₀} {ℓ₁} L (j , n₀ , n₁ , n₂) = | |
| 𝔽 , (_≤_ , 𝔽-set) , ≤-refl , ≤-trans , ≤-antisym | |
| where | |
| P = pos L | |
| A-set = carrier-is-set (pos L) | |
| 𝔽 : Set ℓ₀ | |
| 𝔽 = Σ[ a ∈ ∣ L ∣F ] j a ≡ a | |
| 𝔽-set : isSet 𝔽 | |
| 𝔽-set = isOfHLevelΣ 2 A-set (λ a → prop⇒set (A-set (j a) a)) | |
| _≤_ : 𝔽 → 𝔽 → hProp ℓ₁ | |
| (a , _) ≤ (b , _) = a ⊑[ P ] b is-true , is-true-prop (a ⊑[ P ] b) | |
| open Properties 𝔽-set _≤_ | |
| ≤-refl : IsReflexive is-true | |
| ≤-refl (x , _) = ⊑[ P ]-refl x | |
| ≤-trans : IsTransitive is-true | |
| ≤-trans (x , _) (y , _) (z , _) x≤y y≤x = ⊑[ P ]-trans x y z x≤y y≤x | |
| ≤-antisym : IsAntisym is-true | |
| ≤-antisym (x , _) (y , _) x≤y y≤x = | |
| ΣProp≡ (λ z → A-set (j z) z) (⊑[ P ]-antisym x y x≤y y≤x) | |
| -- The set of fixed points of a nucleus `j` forms a frame. | |
| -- The join of this frame is define as ⊔ᵢ ℱᵢ := j (⊔′ᵢ ℱᵢ) where ⊔′ denotes the join of L. | |
| nuclear-fixed-point-frame : (L : Frame ℓ₀ ℓ₁ ℓ₂) → (N : Nucleus L) → Frame ℓ₀ ℓ₁ ℓ₂ | |
| nuclear-fixed-point-frame {ℓ₁ = ℓ₁} {ℓ₂ = ℓ₂} L N@(j , n₀ , n₁ , n₂) = | |
| ∣ nuclear-fixed-point-poset L N ∣ₚ | |
| , (strₚ (nuclear-fixed-point-poset L N) | |
| , (𝟏[ L ] , 𝟏-fixed) | |
| , _⊓_ , ⊔_) | |
| , top , ⊓-lower₀ , ⊓-lower₁ , ⊓-greatest , ⊔-upper , ⊔-least , distr | |
| where | |
| 𝒜 = π₀ (nuclear-fixed-point-poset L N) | |
| P = pos L | |
| _⊑_ : ∣ pos L ∣ₚ → ∣ pos L ∣ₚ → hProp ℓ₁ | |
| _⊑_ = λ x y → x ⊑[ pos L ] y | |
| _⊑N_ : 𝒜 → 𝒜 → hProp ℓ₁ | |
| _⊑N_ = λ x y → x ⊑[ nuclear-fixed-point-poset L N ] y | |
| ⋃L_ : Sub ℓ₂ ∣ L ∣F → ∣ L ∣F | |
| ⋃L x = ⋃[ L ] x | |
| ⊑N-antisym = ⊑[ nuclear-fixed-point-poset L N ]-antisym | |
| A-set = carrier-is-set (nuclear-fixed-point-poset L N) | |
| 𝟏-fixed : j 𝟏[ L ] ≡ 𝟏[ L ] | |
| 𝟏-fixed = ⊑[ pos L ]-antisym (j 𝟏[ L ]) 𝟏[ L ] (𝟏[ L ]-top (j 𝟏[ L ])) (n₁ 𝟏[ L ]) | |
| open PosetReasoning (pos L) using (_⊑⟨_⟩_; _■) | |
| _⊓_ : 𝒜 → 𝒜 → 𝒜 | |
| _⊓_ (x , x-f) (y , y-f) = | |
| x ⊓[ L ] y , ⊑[ P ]-antisym (j (x ⊓[ L ] y)) (x ⊓[ L ] y) φ (n₁ (x ⊓[ L ] y)) | |
| where | |
| ⊑jx : j (x ⊓[ L ] y) ⊑ j x is-true | |
| ⊑jx = j (x ⊓[ L ] y) ⊑⟨ ≡⇒⊑ P (n₀ x y) ⟩ | |
| j x ⊓[ L ] j y ⊑⟨ ⊓[ L ]-lower₀ (j x) (j y) ⟩ | |
| j x ■ | |
| ⊑jy : j (x ⊓[ L ] y) ⊑ j y is-true | |
| ⊑jy = j (x ⊓[ L ] y) ⊑⟨ ≡⇒⊑ P (n₀ x y) ⟩ | |
| j x ⊓[ L ] j y ⊑⟨ ⊓[ L ]-lower₁ (j x) (j y) ⟩ | |
| j y ■ | |
| ⊑x : j (x ⊓[ L ] y) ⊑ x is-true | |
| ⊑x = subst (λ z → j (x ⊓[ L ] y) ⊑ z is-true) x-f ⊑jx | |
| ⊑y : j (x ⊓[ L ] y) ⊑ y is-true | |
| ⊑y = subst (λ z → j (x ⊓[ L ] y) ⊑ z is-true) y-f ⊑jy | |
| φ : j (x ⊓[ L ] y) ⊑ (x ⊓[ L ] y) is-true | |
| φ = ⊓[ L ]-greatest x y (j (x ⊓[ L ] y)) ⊑x ⊑y | |
| ⊔_ : Sub ℓ₂ 𝒜 → 𝒜 | |
| ⊔ (I , F) = j (⋃[ L ] 𝒢) , j⊔L-fixed | |
| where | |
| 𝒢 = I , π₀ ∘ F | |
| j⊔L-fixed : j (j (⋃[ L ] 𝒢)) ≡ j (⋃[ L ] 𝒢) | |
| j⊔L-fixed = ⊑[ P ]-antisym _ _ (n₂ (⋃[ L ] 𝒢)) (n₁ (j (⋃[ L ] 𝒢))) | |
| top : (o : 𝒜) → (o ⊑N (𝟏[ L ] , 𝟏-fixed)) is-true | |
| top = 𝟏[ L ]-top ∘ π₀ | |
| ⊓-lower₀ : (o p : 𝒜) → (o ⊓ p) ⊑N o is-true | |
| ⊓-lower₀ (o , _) (p , _) = ⊓[ L ]-lower₀ o p | |
| ⊓-lower₁ : (o p : 𝒜) → (o ⊓ p) ⊑N p is-true | |
| ⊓-lower₁ (o , _) (p , _) = ⊓[ L ]-lower₁ o p | |
| ⊓-greatest : (o p q : 𝒜) → q ⊑N o is-true → q ⊑N p is-true → q ⊑N (o ⊓ p) is-true | |
| ⊓-greatest (o , _) (p , _) (q , _) q⊑o q⊑p = ⊓[ L ]-greatest o p q q⊑o q⊑p | |
| ⊔-least : (ℱ : Sub ℓ₂ 𝒜) (p : 𝒜) | |
| → ((o : 𝒜) → o ε ℱ → o ⊑N p is-true) → ((⊔ ℱ) ⊑N p) is-true | |
| ⊔-least ℱ p@(p′ , eq) ℱ⊑p = φ | |
| where | |
| 𝒢 : Sub ℓ₂ ∣ P ∣ₚ | |
| 𝒢 = index ℱ , λ i → π₀ (ℱ € i) | |
| ϑ : (o : ∣ P ∣ₚ) → o ε 𝒢 → o ⊑ p′ is-true | |
| ϑ o o∈𝒢@(i , eq′) = o ⊑⟨ ≡⇒⊑ P (sym eq′) ⟩ | |
| 𝒢 € i ⊑⟨ ℱ⊑p (𝒢 € i , π₁ (ℱ € i)) (i , refl) ⟩ | |
| p′ ■ | |
| ψ : j (⋃[ L ] 𝒢) ⊑ (j p′) is-true | |
| ψ = mono L N (⋃[ L ] 𝒢) p′ (⋃[ L ]-least 𝒢 p′ ϑ) | |
| φ : j (⋃[ L ] 𝒢) ⊑ p′ is-true | |
| φ = subst (λ k → (j (⋃[ L ] 𝒢) ⊑ k) is-true) eq ψ | |
| ⊔-upper : (ℱ : Sub ℓ₂ 𝒜) (o : 𝒜) → o ε ℱ → (o ⊑N (⊔ ℱ)) is-true | |
| ⊔-upper ℱ (o , _) o∈ℱ@(i , eq) = | |
| o ⊑⟨ φ ⟩ | |
| ⋃[ L ] (π₀ ⊚ ℱ) ⊑⟨ n₁ (⋃[ L ] (π₀ ⊚ ℱ)) ⟩ | |
| j (⋃[ L ] (π₀ ⊚ ℱ)) ■ | |
| where | |
| φ : o ⊑ (⋃[ L ] (π₀ ⊚ ℱ)) is-true | |
| φ = ⋃[ L ]-upper (π₀ ⊚ ℱ) o (i , λ j → π₀ (eq j)) | |
| distr : (o : 𝒜) (ℱ : Sub ℓ₂ 𝒜) → o ⊓ (⊔ ℱ) ≡ ⊔ (index ℱ , (λ i → o ⊓ (ℱ € i))) | |
| distr o@(o′ , jo′=o′) ℱ@(I , F) = | |
| sigmaPath→pathSigma _ _ (φ , carrier-is-set (pos L) _ _ _ _) | |
| where | |
| 𝒢 : Sub ℓ₂ ∣ P ∣ₚ | |
| 𝒢 = π₀ ⊚ ℱ | |
| o′=jo′ : o′ ≡ j o′ | |
| o′=jo′ = sym jo′=o′ | |
| φ : π₀ (o ⊓ (⊔ ℱ)) ≡ π₀ (⊔ (I , (λ i → o ⊓ (ℱ € i)))) | |
| φ = | |
| o′ ⊓[ L ] j (⋃L 𝒢) ≡⟨ cong (λ - → - ⊓[ L ] j (⋃L 𝒢)) o′=jo′ ⟩ | |
| j o′ ⊓[ L ] (j (⋃L 𝒢)) ≡⟨ sym (n₀ o′ (⋃[ L ] 𝒢)) ⟩ | |
| j (o′ ⊓[ L ] (⋃L 𝒢)) ≡⟨ cong j (dist L o′ 𝒢) ⟩ | |
| π₀ (⊔ (I , λ i → o ⊓ (ℱ € i))) ∎ | |
| module NucleusFrom (F : FormalTopology ℓ₀ ℓ₀) where | |
| private | |
| D = π₀ F | |
| P = π₀ (π₀ F) | |
| 𝔉 = ∣ P ∣ₚ | |
| F↓ = downward-subset-frame P | |
| P↓ = pos F↓ | |
| sim = π₁ F | |
| F-mono = π₁ D | |
| _⊑_ = λ (x y : stage D) → x ⊑[ P ] y is-true | |
| open Test (stage D) _⊑_ (exp D) (outcome D) (next D) (π₁ F-mono) sim public | |
| 𝕛 : ∣ F↓ ∣F → ∣ F↓ ∣F | |
| 𝕛 (U , U-down) = U₀ , λ _ _ → down-closed | |
| where | |
| -- This is not h-propositional unless we force it to be using the HIT definition. | |
| U₀ : stage D → hProp ℓ₀ | |
| U₀ = λ a → a <| (_is-true ∘ U) , <|-prop a (_is-true ∘ U) | |
| down-closed : IsDownwardClosed′ (λ - → - <| (_is-true ∘ U)) | |
| down-closed aεU₁ a₀⊑a = lem1 (U-down _ _) a₀⊑a aεU₁ | |
| _<<_ : ∣ F↓ ∣F → ∣ F↓ ∣F → hProp ℓ₀ | |
| x << y = x ⊑[ pos F↓ ] y | |
| ◀-antisym = ⊑[ pos F↓ ]-antisym | |
| 𝕛-nuclear : IsNuclear F↓ 𝕛 | |
| 𝕛-nuclear = I , II , III | |
| where | |
| -- We reason by antisymmetry and prove in (d) 𝕛 (a₀ ⊓ a₁) ⊑ (𝕛 a₀) ⊓ (𝕛 a₁) and | |
| -- in (u) (𝕛 a₀) ⊓ (𝕛 a₁) ⊑ 𝕛 (a₀ ⊓ a₁). | |
| I : (a₀ a₁ : ∣ F↓ ∣F) → 𝕛 (a₀ ⊓[ F↓ ] a₁) ≡ (𝕛 a₀) ⊓[ F↓ ] (𝕛 a₁) | |
| I 𝕌@(U , U-down) 𝕍@(V , V-down) = | |
| ◀-antisym (𝕛 (𝕌 ⊓[ F↓ ] 𝕍)) (𝕛 𝕌 ⊓[ F↓ ] 𝕛 𝕍) d u | |
| where | |
| U′ = _is-true ∘ U | |
| V′ = _is-true ∘ V | |
| U-down′ : IsDownwardClosed′ (_is-true ∘ U) | |
| U-down′ = U-down _ _ | |
| V-down′ : IsDownwardClosed′ (_is-true ∘ V) | |
| V-down′ = V-down _ _ | |
| d : 𝕛 (𝕌 ⊓[ F↓ ] 𝕍) << (𝕛 𝕌 ⊓[ F↓ ] 𝕛 𝕍) is-true | |
| d a (dir p) = dir (π₀ p) , dir (π₁ p) | |
| d a (branch b f) = branch b (π₀ ∘ IH) , branch b (π₁ ∘ IH) | |
| where | |
| IH : (c : outcome D b) → π₀ (𝕛 𝕌 ⊓[ F↓ ] 𝕛 𝕍) (next D c) is-true | |
| IH c = d (next D c) (f c) | |
| d a (squash p q i) = squash (π₀ IH₀) (π₀ IH₁) i , squash (π₁ IH₀) (π₁ IH₁) i | |
| where | |
| IH₀ = d a p | |
| IH₁ = d a q | |
| u : (𝕛 𝕌 ⊓[ F↓ ] 𝕛 𝕍) << 𝕛 (𝕌 ⊓[ F↓ ] 𝕍) is-true | |
| u a p = lem3 U′ V′ U-down′ V-down′ a a (⊑[ P ]-refl a) (π₀ p) (π₁ p) | |
| II : (𝕌 : ∣ F↓ ∣F) → 𝕌 << (𝕛 𝕌) is-true | |
| II 𝕌@(U , U-down) a₀ p = lem1 (U-down _ _) (⊑[ P ]-refl a₀) (dir p) | |
| III : (a : ∣ F↓ ∣F) → 𝕛 (𝕛 a) << (𝕛 a) is-true | |
| III 𝕌@(U , U-down) a′ p = lem4 a′ (λ a → π₀ (𝕛 𝕌) a is-true) U′ p (λ _ q → q) | |
| where | |
| U′ = _is-true ∘ U | |
| L : Frame (suc ℓ₀) ℓ₀ ℓ₀ | |
| L = nuclear-fixed-point-frame F↓ (𝕛 , 𝕛-nuclear) | |
| ⦅_⦆ : ∣ L ∣F → 𝒫 ∣ P ∣ₚ | |
| ⦅ (U , _) , _ ⦆ = U | |
| ↓-clos : stage D → ∣ F↓ ∣F | |
| ↓-clos x = x↓ , down-DC | |
| where | |
| x↓ = λ y → y ⊑[ P ] x | |
| down-DC : IsDownwardClosed P x↓ is-true | |
| down-DC z y z⊑x y⊑z = ⊑[ P ]-trans y z x y⊑z z⊑x | |
| x◀x↓ : (x : stage D) → x <| (λ - → - ⊑[ P ] x is-true) | |
| x◀x↓ x = dir (⊑[ P ]-refl x) | |
| e : stage D → ∣ F↓ ∣F | |
| e z = (λ a → (a <| (_is-true ∘ (π₀ (↓-clos z)))) , squash) , NTS | |
| where | |
| NTS : IsDownwardClosed P (λ a → (a <| (λ - → - ⊑[ P ] z is-true)) , squash) is-true | |
| NTS x y p q = lem1 (λ p q → ⊑[ P ]-trans _ _ z q p) q p | |
| fixing : (x : stage D) → 𝕛 (e x) ≡ e x | |
| fixing x = ⊑[ P↓ ]-antisym (𝕛 (e x)) (e x) NTS up | |
| where | |
| NTS : ∀ y → π₀ (𝕛 (e x)) y is-true → π₀ (e x) y is-true | |
| NTS y (dir p) = p | |
| NTS y (branch b f) = branch b (λ c → NTS (next D c) (f c)) | |
| NTS y (squash p q i) = squash (NTS y p) (NTS y q) i | |
| up : e x ⊑[ P↓ ] 𝕛 (e x) is-true | |
| up = π₀ (π₁ 𝕛-nuclear) (e x) | |
| η : stage (π₀ F) → ∣ L ∣F | |
| η x = (e x) , (fixing x) | |
| ηm : P ─m→ pos L | |
| ηm = η , η-mono | |
| where | |
| η-mono : IsMonotonic P (pos L) η | |
| η-mono x y x⊑y a (dir p) = dir (⊑[ P ]-trans a x y p x⊑y) | |
| η-mono x y x⊑y a (branch b f) = branch b (λ c → η-mono x y x⊑y (next D c) (f c)) | |
| η-mono x y x⊑y a (squash p q i) = squash (η-mono x y x⊑y a p) (η-mono x y x⊑y a q) i | |
| module UniversalProperty (F : FormalTopology ℓ₀ ℓ₀) where | |
| D = π₀ F | |
| P = π₀ (π₀ F) | |
| 𝔉 = ∣ P ∣ₚ | |
| F↓ = downward-subset-frame P | |
| P↓ = pos F↓ | |
| sim = π₁ F | |
| F-mono = π₁ D | |
| _⊑_ = λ (x y : stage D) → x ⊑[ P ] y | |
| open NucleusFrom F | |
| represents : (R : Frame (suc ℓ₀) ℓ₀ ℓ₀) → (m : P ─m→ pos R) → Type ℓ₀ | |
| represents R (f , _) = | |
| (x : 𝔉) (y : exp D x) → | |
| f x ⊑[ pos R ] (⋃[ R ] (outcome D y , λ u → f (next D u))) is-true | |
| _↓_↓ : 𝔉 → 𝔉 → 𝒫 𝔉 | |
| _↓_↓ a b = λ - → - ⊑[ P ] a ∧ - ⊑[ P ] b | |
| IsFlat : (F : Frame (suc ℓ₀) ℓ₀ ℓ₀) → (m : P ─m→ pos F) → Type (suc ℓ₀) | |
| IsFlat F (f , _) = | |
| 𝟏[ F ] ≡ ⋃[ F ] (𝔉 , f) × ((a b : 𝔉) → f a ⊓[ F ] f b ≡ ⋃[ F ] (f ⊚ ⟪ a ↓ b ↓ ⟫)) | |
| universal-prop : Type (suc (suc ℓ₀)) | |
| universal-prop = | |
| (R : Frame (suc ℓ₀) ℓ₀ ℓ₀) (f : P ─m→ pos R) → IsFlat R f → represents R f → | |
| isContr (Σ[ g ∈ (L ─f→ R) ] (_∘m_ {P = P} {Q = pos L} {R = pos R} (π₀ g) ηm) ≡ f) | |
| cover+ : {x y : 𝔉} ((U , _) : ∣ F↓ ∣F) | |
| → ⦅ η y ⦆ x is-true → U y is-true → x <| (_is-true ∘ U) | |
| cover+ U↓ (dir x⊑y) yεU = lem1 (λ x₁ x₂ → π₁ U↓ _ _ x₁ x₂) x⊑y (dir yεU) | |
| cover+ U↓ (branch b f) yεU = branch b (λ c → cover+ U↓ (f c) yεU) | |
| cover+ U↓ (squash φ ψ i) yεU = squash (cover+ U↓ φ yεU) (cover+ U↓ ψ yεU) i | |
| main-lemma : (𝔘 : ∣ L ∣F) → 𝔘 ≡ ⋃[ L ] (η ⊚ (∃ ⦅ 𝔘 ⦆ , π₀)) | |
| main-lemma 𝔘@((U , U-dc) , U-fix) = ⊑[ pos L ]-antisym _ _ down up | |
| where | |
| down : 𝔘 ⊑[ pos L ] (⋃[ L ] (∃ U , λ { (x , _) → η x })) is-true | |
| down x xεU = dir ∣ (x , xεU) , dir (⊑[ P ]-refl x) ∣ | |
| up : (⋃[ L ] (∃ U , η ∘ π₀)) ⊑[ pos L ] 𝔘 is-true | |
| up x (dir xε⋁) = ∥∥-rec (is-true-prop (U x)) NTS xε⋁ | |
| where | |
| NTS : Σ[ y ∈ _ ] ⦅ η (π₀ y) ⦆ x is-true → U x is-true | |
| NTS ((y , yεU) , x◀y↓) = | |
| subst (λ V → π₀ V x is-true) U-fix (cover+ (U , U-dc) x◀y↓ yεU) | |
| up x (branch b f) = subst (λ V → π₀ V x is-true) U-fix (branch b (dir ∘ IH)) | |
| where | |
| IH : (c : outcome D b) → U (next D c) is-true | |
| IH c = up (next D c) (f c) | |
| up x (squash x◀⋁₀ x◀⋁₁ i) = is-true-prop (U x) (up x x◀⋁₀) (up x x◀⋁₁) i | |
| module MainProof (R : Frame (suc ℓ₀) ℓ₀ ℓ₀) | |
| (fm : P ─m→ pos R) | |
| (f-flat : IsFlat R fm) | |
| (rep : represents R fm) where | |
| f = _$ₘ_ fm | |
| f-mono = π₁ fm | |
| g : ∣ L ∣F → ∣ R ∣F | |
| g 𝔘 = ⋃[ R ] (f ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫) | |
| g-mono : IsMonotonic (pos L) (pos R) g | |
| g-mono ((U , _) , _) ((V , _) , _) U⊆V = | |
| ⋃[ R ]-least _ _ (λ o oεfU → ⋃[ R ]-upper _ _ (NTS o oεfU )) | |
| where | |
| NTS : (x : ∣ R ∣F) → x ε (∃ U , f ∘ π₀) → x ε (∃ V , f ∘ π₀) | |
| NTS x ((x′ , x′εfU) , fUεi=x) = (x′ , U⊆V x′ x′εfU) , fUεi=x | |
| gm : pos L ─m→ pos R | |
| gm = g , g-mono | |
| g-resp-𝟏 : g 𝟏[ L ] ≡ 𝟏[ R ] | |
| g-resp-𝟏 = ⋃[ R ] (f ⊚ (∃ ⦅ 𝟏[ L ] ⦆ , π₀)) ≡⟨ family-iff R NTS ⟩ | |
| ⋃[ R ] (𝔉 , f) ≡⟨ sym (π₀ f-flat) ⟩ | |
| 𝟏[ R ] ∎ | |
| where | |
| NTS : (x : ∣ R ∣F) | |
| → (x ε (f ⊚ (∃ ⦅ 𝟏[ L ] ⦆ , π₀)) → x ε (𝔉 , f)) | |
| × (x ε (𝔉 , f) → x ε (f ⊚ (∃ ⦅ 𝟏[ L ] ⦆ , π₀))) | |
| NTS x = (λ { ((y , _) , eq) → y , eq }) , (λ { (y , eq) → (y , tt) , eq }) | |
| g-resp-⊓ : (𝔘 𝔙 : ∣ L ∣F) → g (𝔘 ⊓[ L ] 𝔙) ≡ g 𝔘 ⊓[ R ] g 𝔙 | |
| g-resp-⊓ 𝔘 𝔙 = | |
| ⋃[ R ] (f ⊚ ⟪ ⦅ 𝔘 ⊓[ L ] 𝔙 ⦆ ⟫) | |
| ≡⟨ cong (λ - → ⋃[ R ] (f ⊚ ⟪ ⦅ - ⦆ ⟫)) (comm L 𝔘 𝔙) ⟩ | |
| ⋃[ R ] (f ⊚ ⟪ ⦅ 𝔙 ⊓[ L ] 𝔘 ⦆ ⟫) | |
| ≡⟨ IV ⟩ | |
| ⋃[ R ] ((∃ ⦅ 𝔙 ⦆ × ∃ ⦅ 𝔘 ⦆) , λ { ((v , _) , (u , _)) → ⋃[ R ] (f ⊚ ⟪ v ↓ u ↓ ⟫) }) | |
| ≡⟨ cong (λ - → ⋃[ R ] ((∃ ⦅ 𝔙 ⦆ × ∃ ⦅ 𝔘 ⦆) , -)) III ⟩ | |
| ⋃[ R ] (((∃ ⦅ 𝔙 ⦆) × (∃ ⦅ 𝔘 ⦆)) , (λ { ((x , _) , (y , _)) → f x ⊓[ R ] f y })) | |
| ≡⟨ flatten R (∃ ⦅ 𝔙 ⦆) (λ _ → ∃ ⦅ 𝔘 ⦆) (λ { (v , _) (u , _) → f v ⊓[ R ] f u }) ⟩ | |
| ⋃[ R ] (_ , (λ { (v , _) → ⋃[ R ] (_ , λ { (u , _) → f v ⊓[ R ] f u }) })) | |
| ≡⟨ cong (λ - → ⋃[ R ] (∃ ⦅ 𝔙 ⦆ , -)) II ⟩ | |
| ⋃[ R ] (_ , λ { (x , _) → f x ⊓[ R ] (⋃[ R ] (_ , λ { (y , _) → f y })) }) | |
| ≡⟨ cong (λ - → ⋃[ R ] (∃ ⦅ 𝔙 ⦆ , -)) I ⟩ | |
| ⋃[ R ] (∃ ⦅ 𝔙 ⦆ , λ { (x , _) → (⋃[ R ] (f ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫)) ⊓[ R ] (f x) }) | |
| ≡⟨ sym (dist R (⋃[ R ] (f ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫)) (f ⊚ ⟪ ⦅ 𝔙 ⦆ ⟫)) ⟩ | |
| g 𝔘 ⊓[ R ] g 𝔙 | |
| ∎ | |
| where | |
| I : (λ v → (f (π₀ v)) ⊓[ R ] (⋃[ R ] ((∃ ⦅ 𝔘 ⦆) , (λ u → f (π₀ u))))) | |
| ≡ (λ v → (⋃[ R ] (∃ ⦅ 𝔘 ⦆ , (λ u → f (π₀ u)))) ⊓[ R ] (f (π₀ v))) | |
| I = funExt λ v → comm R (f (π₀ v)) (⋃[ R ] ((∃ ⦅ 𝔘 ⦆) , λ u → f (π₀ u))) | |
| II : (λ x → ⋃[ R ] ((λ - → f (π₀ x) ⊓[ R ] -) ⊚ (f ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫))) | |
| ≡ (λ v → (f (π₀ v)) ⊓[ R ] (⋃[ R ] (f ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫))) | |
| II = funExt λ v → sym (dist R (f (π₀ v)) (f ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫)) | |
| III : (λ { ((v , _) , u , _) → ⋃[ R ] (f ⊚ ⟪ v ↓ u ↓ ⟫) }) | |
| ≡ (λ { (x , y) → (f (π₀ x)) ⊓[ R ] (f (π₀ y)) }) | |
| III = funExt λ { x → sym (π₁ f-flat (π₀ (π₀ x)) (π₀ (π₁ x))) } | |
| IV : ⋃[ R ] (f ⊚ ⟪ ⦅ 𝔙 ⊓[ L ] 𝔘 ⦆ ⟫) | |
| ≡ ⋃[ R ] (_ , λ { ((v , _) , (u , _)) → ⋃[ R ] (f ⊚ ⟪ v ↓ u ↓ ⟫) }) | |
| IV = ⊑[ pos R ]-antisym _ _ down up | |
| where | |
| down : _ | |
| down = ⋃[ R ]-least _ _ isUB | |
| where | |
| isUB : _ | |
| isUB o ((i , (a , b)) , eq) = | |
| ⋃[ R ]-upper _ _ (((i , a) , (i , b)) , subst (λ o′ → _ ≡ o′) eq φ) | |
| where | |
| down′ : (⋃[ R ] (f ⊚ ⟪ i ↓ i ↓ ⟫)) ⊑[ pos R ] f i is-true | |
| down′ = | |
| ⋃[ R ]-least _ _ λ { z ((_ , (k , _)) , eq′) → | |
| subst (λ - → - ⊑[ pos R ] _ is-true) eq′ (f-mono _ _ k) } | |
| up′ : f i ⊑[ pos R ] (⋃[ R ] (f ⊚ ⟪ i ↓ i ↓ ⟫)) is-true | |
| up′ = ⋃[ R ]-upper _ _ ((i , (⊑[ P ]-refl i , ⊑[ P ]-refl i)) , refl) | |
| φ : ⋃[ R ] (f ⊚ ⟪ i ↓ i ↓ ⟫) ≡ f i | |
| φ = ⊑[ pos R ]-antisym _ _ down′ up′ | |
| up : _ | |
| up = ⋃[ R ]-least _ _ isUB | |
| where | |
| isUB : _ | |
| isUB o (i@((x , xε𝔙) , (y , yε𝔘)) , eq) = | |
| subst (λ o′ → o′ ⊑[ pos R ] _ is-true) eq (⋃[ R ]-least _ _ NTS) | |
| where | |
| NTS : _ | |
| NTS w (j@(z , (z⊑x , z⊑y)) , eq′) = ⋃[ R ]-upper _ _ ((z , φ) , eq′) | |
| where | |
| φ : (⦅ 𝔙 ⦆ ∩ ⦅ 𝔘 ⦆) z is-true | |
| φ = (π₁ (π₀ 𝔙) x z xε𝔙 z⊑x) , (π₁ (π₀ 𝔘) y z yε𝔘 z⊑y) | |
| g-resp-⊔ : (ℱ : Sub ℓ₀ ∣ L ∣F) → g (⋃[ L ] ℱ) ≡ ⋃[ R ] (g ⊚ ℱ) | |
| g-resp-⊔ ℱ@(I , U) = | |
| ⋃[ R ] (f ⊚ ⟪ ⦅ ⋃[ L ] ℱ ⦆ ⟫) | |
| ≡⟨ ⊑[ pos R ]-antisym _ _ down up ⟩ | |
| ⋃[ R ] (Σ I (λ - → ∃ ⦅ U - ⦆) , λ { (x , y) → f (π₀ y) }) | |
| ≡⟨ flatten R I (λ i → ∃ ⦅ U i ⦆) (λ _ j → f (π₀ j)) ⟩ | |
| ⋃[ R ] (g ⊚ ℱ) | |
| ∎ | |
| where | |
| LHS = ⋃[ R ] (f ⊚ ⟪ ⦅ ⋃[ L ] ℱ ⦆ ⟫) | |
| RHS = ⋃[ R ] (Σ I (λ - → ∃ ⦅ U - ⦆) , (λ { (x , y) → f (π₀ y) })) | |
| down : LHS ⊑[ pos R ] RHS is-true | |
| down = ⋃[ R ]-least _ _ ψ | |
| where | |
| ψ : (o : ∣ R ∣F) → o ε (f ⊚ ⟪ ⦅ ⋃[ L ] ℱ ⦆ ⟫) → o ⊑[ pos R ] RHS is-true | |
| ψ o ((x , foo) , eq) = subst (λ - → - ⊑[ pos R ] RHS is-true) eq (ϑ x foo) | |
| where | |
| open PosetReasoning (pos R) using (_⊑⟨_⟩_; _■) | |
| ϑ : (y : 𝔉) → ⦅ ⋃[ L ] ℱ ⦆ y is-true → f y ⊑[ pos R ] RHS is-true | |
| ϑ y (dir mem) = ∥∥-rec | |
| (is-true-prop (f y ⊑[ pos R ] RHS)) | |
| (λ { (j , cov) → | |
| ⋃[ R ]-upper _ _ ((j , y , cov) , refl) }) mem | |
| ϑ y (branch b h) = | |
| f y ⊑⟨ rep y b ⟩ | |
| ⋃[ R ] (outcome D b , f ∘ next D) ⊑⟨ ⋃[ R ]-least _ _ ζ ⟩ | |
| RHS ■ | |
| where | |
| ζ : (r : ∣ R ∣F) | |
| → r ε (outcome D b , f ∘ next D) | |
| → r ⊑[ pos R ] RHS is-true | |
| ζ r (c , eq-r) = | |
| subst (λ - → - ⊑[ pos R ] RHS is-true) eq-r (ϑ (next D c) (h c)) | |
| ϑ y (squash φ ψ i) = is-true-prop (f y ⊑[ pos R ] RHS) (ϑ y φ) (ϑ y ψ) i | |
| up : RHS ⊑[ pos R ] LHS is-true | |
| up = ⋃[ R ]-least _ _ λ { r ((i , (x , xεU)) , eq) → | |
| ⋃[ R ]-upper _ _ ((x , dir ∣ i , xεU ∣) , eq) } | |
| g-frame-homo : IsFrameHomomorphism L R gm | |
| g-frame-homo = g-resp-𝟏 , (g-resp-⊓ , g-resp-⊔) | |
| gm∘ηm = _∘m_ {P = P} {Q = pos L} {R = pos R} gm ηm | |
| gm∘ηm~f : (x : 𝔉) → gm $ₘ (ηm $ₘ x) ≡ fm $ₘ x | |
| gm∘ηm~f x = ⊑[ pos R ]-antisym _ _ down (⋃[ R ]-upper _ _ ((x , x◀x↓ x) , refl)) | |
| where | |
| open PosetReasoning (pos R) using (_⊑⟨_⟩_; _■) | |
| lem : (y : 𝔉) → y <| (_is-true ∘ π₀ (↓-clos x)) → f y ⊑[ pos R ] f x is-true | |
| lem y (squash α β i) = is-true-prop (f y ⊑[ pos R ] f x) (lem y α) (lem y β) i | |
| lem y (dir y⊑x) = f-mono y x y⊑x | |
| lem y (branch b h) = | |
| fm $ₘ y ⊑⟨ rep y b ⟩ | |
| ⋃[ R ] (outcome D b , (λ c → fm $ₘ next D c)) ⊑⟨ ⋃[ R ]-least _ _ isUB ⟩ | |
| fm $ₘ x ■ | |
| where | |
| isUB : (z : ∣ R ∣F) | |
| → z ε (outcome D b , (λ c → fm $ₘ next D c)) | |
| → z ⊑[ pos R ] (fm $ₘ x) is-true | |
| isUB z (c , p) = z ⊑⟨ ≡⇒⊑ (pos R) (sym p) ⟩ | |
| fm $ₘ (next D c) ⊑⟨ lem (next D c) (h c) ⟩ | |
| fm $ₘ x ■ | |
| lem′ : (o : ∣ R ∣F) → o ε (∃ (π₀ (e x)) , f ∘ π₀) → o ⊑[ pos R ] f x is-true | |
| lem′ o ((y , φ) , fy=o) = subst (λ - → - ⊑[ pos R ] f x is-true) fy=o (lem y φ) | |
| down : (⋃[ R ] (∃ (π₀ (e x)) , f ∘ π₀)) ⊑[ pos R ] f x is-true | |
| down = ⋃[ R ]-least _ _ lem′ | |
| g∘η=f : gm∘ηm ≡ fm | |
| g∘η=f = ΣProp≡ (IsMonotonic-prop P (pos R)) (funExt gm∘ηm~f) | |
| g∘η=f′ : g ∘ η ≡ f | |
| g∘η=f′ = subst (λ { (h , _) → h ≡ f }) (sym g∘η=f) refl | |
| g-unique : (y : Σ[ g′ ∈ (L ─f→ R) ] (_∘m_ {P = P} {Q = pos L} {R = pos R} (π₀ g′) ηm ≡ fm)) | |
| → ((gm , g-frame-homo) , g∘η=f) ≡ y | |
| g-unique ((g′m , g′-frame-homo) , φ) = ΣProp≡ I II | |
| where | |
| g′ = _$ₘ_ g′m | |
| f=g′∘η : f ≡ g′ ∘ η | |
| f=g′∘η = subst (λ { (f′ , _) → f′ ≡ g′ ∘ η }) φ refl | |
| NTS₀ : (y : Σ (∣ pos L ∣ₚ → ∣ pos R ∣ₚ) (IsMonotonic (pos L) (pos R))) → isProp ((_∘m_ {P = P} {Q = pos L} {R = pos R} y ηm) ≡ fm) | |
| NTS₀ y = isOfHLevelΣ 2 | |
| (∏-set λ _ → carrier-is-set (pos R)) | |
| (λ h → prop⇒set (IsMonotonic-prop P (pos R) h)) | |
| (_∘m_ {P = P} {Q = pos L} {R = pos R} y ηm) fm | |
| I : (h : L ─f→ R) → isProp (_∘m_ {P = P} {Q = pos L} {R = pos R} (π₀ h) ηm ≡ fm) | |
| I h = isOfHLevelΣ 2 | |
| (∏-set λ _ → carrier-is-set (pos R)) | |
| (λ h → prop⇒set (IsMonotonic-prop P (pos R) h)) | |
| (_∘m_ {P = P} {Q = pos L} {R = pos R} (π₀ h) ηm) fm | |
| g~g′ : (𝔘 : ∣ L ∣F) → g 𝔘 ≡ g′ 𝔘 | |
| g~g′ 𝔘 = | |
| g 𝔘 ≡⟨ cong g (main-lemma 𝔘) ⟩ | |
| g (⋃[ L ] (η ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫)) ≡⟨ π₁ (π₁ g-frame-homo) (η ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫) ⟩ | |
| ⋃[ R ] ((g ∘ η) ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫) ≡⟨ cong (λ - → ⋃[ R ] (- ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫)) g∘η=f′ ⟩ | |
| ⋃[ R ] (f ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫) ≡⟨ eq₀ ⟩ | |
| ⋃[ R ] ((g′ ∘ η) ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫) ≡⟨ eq₁ ⟩ | |
| g′ (⋃[ L ] (η ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫)) ≡⟨ eq₂ ⟩ | |
| g′ 𝔘 ∎ | |
| where | |
| eq₀ : ⋃[ R ] (f ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫) ≡ ⋃[ R ] ((g′ ∘ η) ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫) | |
| eq₀ = cong (λ - → ⋃[ R ] (- ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫)) f=g′∘η | |
| eq₁ : ⋃[ R ] ((g′ ∘ η) ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫) ≡ g′ (⋃[ L ] (η ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫)) | |
| eq₁ = sym (π₁ (π₁ g′-frame-homo) (η ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫)) | |
| eq₂ : g′ (⋃[ L ] ((η ⊚ ⟪ ⦅ 𝔘 ⦆ ⟫))) ≡ g′ 𝔘 | |
| eq₂ = cong g′ (sym (main-lemma 𝔘)) | |
| II : (gm , g-frame-homo) ≡ (g′m , g′-frame-homo) | |
| II = ΣProp≡ | |
| (IsFrameHomomorphism-prop L R) | |
| (ΣProp≡ (IsMonotonic-prop (pos L) (pos R)) (funExt g~g′)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment