wip: pcas

Author: plt-amy

src/Data/Partial/Base.lagda.md

@@ -207,6 +207,9 @@ part-ap f x .elt (pf , px) = f .elt pf (x .elt px)
 
 <!--
 ```agda
+is-always : {A : Type ℓ} (a : ↯ A) (x : ⌞ a ⌟) → a ≡ always (a .elt x)
+is-always a x = part-ext (λ _ → tt) (λ z → x) λ _ _ → ↯-indep a
+
 instance
   ↯-Map : Map (eff ↯)
   ↯-Map .Map.map = part-map
@@ -219,6 +222,18 @@ instance
   ↯-Bind : Bind (eff ↯)
   ↯-Bind .Bind._>>=_      = part-bind
   ↯-Bind .Bind.Idiom-bind = ↯-Idiom
+
+-- This class lets us define syntax sugar for e.g. lifted binary
+-- operators which automatically lifts values from the base type
+record To-part {ℓ'} (X : Type ℓ') (A : Type ℓ) : Type (ℓ ⊔ ℓ') where
+  field to-part : X → ↯ A
+
+instance
+  part-to-part : To-part (↯ A) A
+  part-to-part = record { to-part = λ x → x }
+
+  pure-to-part : To-part A A
+  pure-to-part = record { to-part = always }
 ```
 -->
 

src/Data/Partial/Total.lagda.md

@@ -0,0 +1,95 @@
+<!--
+```agda
+open import 1Lab.Prelude
+
+open import Data.Partial.Base
+open import Data.Nat.Base
+open import Data.Power using (ℙ)
+```
+-->
+
+```agda
+module Data.Partial.Total where
+```
+
+```agda
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B C X Y : Type ℓ
+```
+
+# Total partial elements
+
+```agda
+↯⁺ : Type ℓ → Type ℓ
+↯⁺ A = Σ[ a ∈ ↯ A ] ⌞ a ⌟
+```
+
+<!--
+```agda
+instance
+  fat-to-part : To-part (↯⁺ A) A
+  fat-to-part = record { to-part = fst }
+
+  ↯⁺-Map : Map (eff ↯⁺)
+  ↯⁺-Map .Map.map f (x , hx) = part-map f x , hx
+
+  ↯⁺-Idiom : Idiom (eff ↯⁺)
+  ↯⁺-Idiom .Idiom.Map-idiom = ↯⁺-Map
+  ↯⁺-Idiom .Idiom.pure x    = always x , tt
+  ↯⁺-Idiom .Idiom._<*>_ (f , hf) (x , hx) = part-ap f x , hf , hx
+
+  Extensional-↯⁺ : ⦃ _ : Extensional (↯ A) ℓ ⦄ → Extensional (↯⁺ A) ℓ
+  Extensional-↯⁺ ⦃ e ⦄ = embedding→extensional (fst , Subset-proj-embedding (λ _ → hlevel 1)) e
+
+  abstract
+    H-Level-↯⁺ : ∀ {A : Type ℓ} {n} ⦃ _ : 2 ≤ n ⦄ ⦃ _ : H-Level A n ⦄ → H-Level (↯⁺ A) n
+    H-Level-↯⁺ {n = suc (suc n)} ⦃ s≤s (s≤s p) ⦄ = hlevel-instance $
+      embedding→is-hlevel (1 + n) (Subset-proj-embedding λ _ → hlevel 1) (hlevel (2 + n))
+```
+-->
+
+```agda
+from-total : ↯⁺ A → A
+from-total (a , ha) = a .elt ha
+
+from-total-is-equiv : is-equiv (from-total {A = A})
+from-total-is-equiv = is-iso→is-equiv (iso pure (λ _ → refl) λ (x , a) → Σ-prop-path! (sym (is-always x a)))
+```
+
+```agda
+record ℙ⁺ (A : Type ℓ) : Type ℓ where
+  field
+    mem     : ↯ A → Ω
+    defined : ∀ {a} → ⌞ mem a ⌟ → ⌞ a ⌟
+```
+
+<!--
+```agda
+private unquoteDecl eqv = declare-record-iso eqv (quote ℙ⁺)
+open ℙ⁺ public
+open is-iso
+
+instance
+  Membership-ℙ⁺ : ⦃ _ : To-part X A ⦄ → Membership X (ℙ⁺ A) _
+  Membership-ℙ⁺ = record { _∈_ = λ a p → ⌞ p .mem (to-part a) ⌟ } where open To-part ⦃ ... ⦄
+
+  Extensional-ℙ⁺ : ∀ {ℓr} ⦃ _ : Extensional (↯ A → Ω) ℓr ⦄ → Extensional (ℙ⁺ A) ℓr
+  Extensional-ℙ⁺ ⦃ e ⦄ = injection→extensional! (λ p → Iso.injective eqv (Σ-prop-path! p)) e
+
+  H-Level-ℙ⁺ : ∀ {n} → H-Level (ℙ⁺ A) (2 + n)
+  H-Level-ℙ⁺ = basic-instance 2 (Iso→is-hlevel 2 eqv (hlevel 2))
+```
+-->
+
+```agda
+from-total-predicate : ℙ A → ℙ⁺ A
+from-total-predicate P .mem x = el (Σ[ hx ∈ x ] x .elt hx ∈ P) (hlevel 1)
+from-total-predicate P .defined (hx , _) = hx
+
+from-total-predicate-is-equiv : is-equiv (from-total-predicate {A = A})
+from-total-predicate-is-equiv = is-iso→is-equiv λ where
+  .inv P a → P .mem (always a)
+  .rinv P → ext λ a → Ω-ua (rec! (λ ha → subst (_∈ P) (sym (is-always a ha)))) λ pa → P .defined pa , subst (_∈ P) (is-always a _) pa
+  .linv P → ext λ a → Ω-ua snd (tt ,_)
+```

src/Data/Vec/Base.lagda.md

@@ -4,7 +4,7 @@ open import 1Lab.Path
 open import 1Lab.Type
 
 open import Data.Product.NAry
-open import Data.List.Base hiding (lookup ; tabulate)
+open import Data.List.Base hiding (lookup ; tabulate ; _++_)
 open import Data.Fin.Base
 open import Data.Nat.Base
 ```
@@ -86,6 +86,10 @@ map : (A → B) → Vec A n → Vec B n
 map f [] = []
 map f (x ∷ xs) = f x ∷ map f xs
 
+_++_ : ∀ {n k} → Vec A n → Vec A k → Vec A (n + k)
+[] ++ ys = ys
+(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
+
 zip-with : (A → B → C) → Vec A n → Vec B n → Vec C n
 zip-with f [] [] = []
 zip-with f (x ∷ xs) (y ∷ ys) = f x y ∷ zip-with f xs ys

src/Realisability/Base.lagda.md

@@ -0,0 +1,111 @@
+<!--
+```agda
+open import 1Lab.Prelude
+
+open import Data.Partial.Total
+open import Data.Partial.Base
+open import Data.Vec.Base
+
+open import Realisability.PCA
+
+import Realisability.Data.Pair as pairs
+import Realisability.PCA.Sugar as S
+import Realisability.Data.Sum as sums
+```
+-->
+
+```agda
+module Realisability.Base
+  {ℓ} {𝔸 : Type ℓ} (_%_ : ↯ 𝔸 → ↯ 𝔸 → ↯ 𝔸) (p : is-pca _%_)
+  where
+```
+
+<!--
+```agda
+open pairs p
+open sums p
+open S p
+
+private variable
+  ℓ' ℓ'' : Level
+  X Y Z : Type ℓ'
+  n : Nat
+```
+-->
+
+# Realisability logic
+
+```agda
+record [_]_⊢_ (f : X → Y) (P : X → ℙ⁺ 𝔸) (Q : Y → ℙ⁺ 𝔸) : Type (level-of X ⊔ level-of Y ⊔ ℓ) where
+  field
+    realiser : ↯⁺ 𝔸
+    tracks   : ∀ {x} (a : ↯ 𝔸) (ah : a ∈ P x) → realiser ⋆ a ∈ Q (f x)
+
+  realiser↓ : ∀ {x} (a : ↯ 𝔸) (ah : a ∈ P x) → ⌞ realiser ⋆ a ⌟
+  realiser↓ a ah = Q _ .defined (tracks a ah)
+```
+
+<!--
+```agda
+private unquoteDecl eqv' = declare-record-iso eqv' (quote [_]_⊢_)
+
+open [_]_⊢_
+
+instance
+  tracks-to-term : ∀ {V : Type} {P : X → ℙ⁺ 𝔸} {Q : Y → ℙ⁺ 𝔸} {f : X → Y} → To-term V ([ f ] P ⊢ Q)
+  tracks-to-term = record { to = λ x → const (x .realiser) }
+
+  tracks-to-part : ∀ {P : X → ℙ⁺ 𝔸} {Q : Y → ℙ⁺ 𝔸} {f : X → Y} → To-part ([ f ] P ⊢ Q) 𝔸
+  tracks-to-part = record { to-part = λ x → x .realiser .fst }
+
+private
+  variable P Q R : X → ℙ⁺ 𝔸
+
+  subst-∈ : (P : ℙ⁺ 𝔸) {x y : ↯ 𝔸} → x ∈ P → y ≡ x → y ∈ P
+  subst-∈ P hx p = subst (_∈ P) (sym p) hx
+```
+-->
+
+## Basic structural rules
+
+```agda
+id⊢ : [ id ] P ⊢ P
+id⊢ {P = P} = record
+  { realiser = val ⟨ x ⟩ x
+  ; tracks   = λ {x} a ha → subst-∈ (P x) ha (abs-β _ [] (a , P x .defined ha))
+  }
+
+_∘⊢_ : ∀ {f g} → [ g ] Q ⊢ R → [ f ] P ⊢ Q → [ g ∘ f ] P ⊢ R
+_∘⊢_ {R = R} {P = P} α β = record
+  { realiser = val ⟨ x ⟩ α `· (β `· x)
+  ; tracks   = λ a ha → subst-∈ (R _) (α .tracks (β ⋆ a) (β .tracks a ha)) $
+      (val ⟨ x ⟩ α `· (β `· x)) ⋆ a ≡⟨ abs-β _ [] (a , P _ .defined ha) ⟩
+      α ⋆ (β ⋆ a)                   ∎
+  }
+```
+
+## Conjunction
+
+```agda
+_∧T_ : (P Q : X → ℙ⁺ 𝔸) → X → ℙ⁺ 𝔸
+(P ∧T Q) x = record
+  { mem     = λ a → elΩ (Σ[ u ∈ ↯⁺ 𝔸 ] Σ[ v ∈ ↯⁺ 𝔸 ] (a ≡ `pair ⋆ u ⋆ v × u ∈ P x × v ∈ Q x))
+  ; defined = rec! (λ u hu v hv α _ _ → subst ⌞_⌟ (sym α) (`pair↓₂ hu hv))
+  }
+
+π₁⊢ : [ id ] (P ∧T Q) ⊢ P
+π₁⊢ {P = P} {Q = Q} = record { realiser = `fst ; tracks = tr } where
+  tr : ∀ {x} (a : ↯ 𝔸) (ah : a ∈ (P ∧T Q) x) → `fst ⋆ a ∈ P x
+  tr {x} = elim! λ a p hp q hq α pp qq → subst-∈ (P _) pp $
+    `fst ⋆ a               ≡⟨ ap (`fst ⋆_) α ⟩
+    `fst ⋆ (`pair ⋆ p ⋆ q) ≡⟨ `fst-β hp hq ⟩
+    p                      ∎
+
+π₂⊢ : [ id ] (P ∧T Q) ⊢ Q
+π₂⊢ {P = P} {Q = Q} = record { realiser = `snd ; tracks = tr } where
+  tr : ∀ {x} (a : ↯ 𝔸) (ah : a ∈ (P ∧T Q) x) → `snd ⋆ a ∈ Q x
+  tr {x} = elim! λ a p hp q hq α pp qq → subst-∈ (Q _) qq $
+    `snd ⋆ a               ≡⟨ ap (`snd ⋆_) α ⟩
+    `snd ⋆ (`pair ⋆ p ⋆ q) ≡⟨ `snd-β hp hq ⟩
+    q                      ∎
+```

src/Realisability/Data/Pair.lagda.md

@@ -0,0 +1,71 @@
+<!--
+```agda
+open import 1Lab.Prelude
+
+open import Data.Partial.Total
+open import Data.Partial.Base
+open import Data.Vec.Base
+
+open import Realisability.PCA
+
+import Realisability.PCA.Sugar as S
+```
+-->
+
+```agda
+module Realisability.Data.Pair
+```
+
+<!--
+```agda
+  {ℓ} {A : Type ℓ} {_%_ : ↯ A → ↯ A → ↯ A} (pca : is-pca _%_)
+  (let infixl 8 _%_; _%_ = _%_)
+  where
+
+open S pca
+```
+-->
+
+# Pairs in a PCA
+
+```agda
+`true : ↯⁺ A
+`true = val ⟨ x ⟩ ⟨ y ⟩ x
+
+`false : ↯⁺ A
+`false = val ⟨ x ⟩ ⟨ y ⟩ y
+
+abstract
+  `false-β : {a b : ↯ A} → ⌞ a ⌟ → ⌞ b ⌟ → `false ⋆ a ⋆ b ≡ b
+  `false-β {a} {b} ah bh = abs-βₙ [] ((b , bh) ∷ (a , ah) ∷ [])
+
+  `true-β : {a b : ↯ A} → ⌞ a ⌟ → ⌞ b ⌟ → `true ⋆ a ⋆ b ≡ a
+  `true-β {a} {b} ah bh = abs-βₙ [] ((b , bh) ∷ (a , ah) ∷ [])
+
+`pair : ↯⁺ A
+`pair = val ⟨ a ⟩ ⟨ b ⟩ ⟨ i ⟩ i `· a `· b
+
+abstract
+  `pair↓₂ : ∀ {a b} → ⌞ a ⌟ → ⌞ b ⌟ → ⌞ `pair .fst % a % b ⌟
+  `pair↓₂ {a} {b} ah bh = subst ⌞_⌟ (sym (abs-βₙ [] ((b , bh) ∷ (a , ah) ∷ []))) (abs↓ _ ((b , bh) ∷ (a , ah) ∷ []))
+
+`fst : ↯⁺ A
+`fst = val ⟨ p ⟩ p `· `true
+
+`snd : ↯⁺ A
+`snd = val ⟨ p ⟩ p `· `false
+
+`fst-β : ∀ {a b} → ⌞ a ⌟ → ⌞ b ⌟ → `fst ⋆ (`pair ⋆ a ⋆ b) ≡ a
+`fst-β {a} {b} ah bh =
+  `fst ⋆ (`pair ⋆ a ⋆ b)  ≡⟨ abs-β _ [] (_ , `pair↓₂ ah bh) ⟩
+  `pair ⋆ a ⋆ b ⋆ `true   ≡⟨ abs-βₙ [] (`true ∷ (b , bh) ∷ (a , ah) ∷ []) ⟩
+  `true ⋆ a ⋆ b           ≡⟨ `true-β ah bh ⟩
+  a                       ∎
+
+`snd-β : ∀ {a b} → ⌞ a ⌟ → ⌞ b ⌟ → `snd ⋆ (`pair ⋆ a ⋆ b) ≡ b
+`snd-β {a} {b} ah bh =
+  `snd ⋆ (`pair ⋆ a ⋆ b)  ≡⟨ abs-β _ [] (_ , `pair↓₂ ah bh) ⟩
+  `pair ⋆ a ⋆ b ⋆ `false  ≡⟨ abs-βₙ [] (`false ∷ (b , bh) ∷ (a , ah) ∷ []) ⟩
+  `false ⋆ a ⋆ b          ≡⟨ `false-β ah bh ⟩
+  b                       ∎
+```