Define PERs

.gitignore

@@ -1,3 +1,4 @@
 *.agdai
 *.agda~
 *.DS_Store
+*.lagda.md~

src/Realizability/ApplicativeStructure.agda → src/Realizability/ApplicativeStructure.lagda.md

@@ -1,3 +1,15 @@
+---
+title: Applicative Structure
+author: Rahul Chhabra
+---
+# Applicative Structure
+
+In this module we define the notion of an _applicative structure_.
+
+A type $A$ has applicative structure if it has an "application operation" (here represented by `_⨾_`) and is a set.
+
+<details>
+```agda
 open import Cubical.Core.Everything
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
@@ -28,13 +40,21 @@ private module _ {ℓ} {A : Type ℓ} where
   opaque
     chain : ∀ {n} → Vec A (suc n) → (A → A → A) → A
     chain {n} (x ∷vec vec) op = foldl (λ _ → A) (λ acc curr → op acc curr) x vec
+```
+</details>
 
+```agda
 record ApplicativeStructure {ℓ} (A : Type ℓ) : Type ℓ where
   infixl 20 _⨾_
   field
     isSetA : isSet A
     _⨾_ : A → A → A
+```
 
+Since being a set is a property - we will generally not have to think about it too much. Also, since `A` is a set - we can drop the relevance of paths and simply talk about "equality".
+
+We can define the notion of a term over an applicative structure.
+```agda
 module _ {ℓ} {A : Type ℓ} (as : ApplicativeStructure A) where
   open ApplicativeStructure as
   infix 23 `_
@@ -43,7 +63,11 @@ module _ {ℓ} {A : Type ℓ} (as : ApplicativeStructure A) where
     # : Fin n → Term n
     `_ : A → Term n
     _̇_ : Term n → Term n → Term n
+```
+
+These terms can be evaluated into $A$ if we can give the values of the free variables.
 
+```agda
   ⟦_⟧ : ∀ {n} → Term n → Vec A n → A
   ⟦_⟧ (` a) _ = a
   ⟦_⟧ {n} (# k) subs = lookup k subs
@@ -54,22 +78,41 @@ module _ {ℓ} {A : Type ℓ} (as : ApplicativeStructure A) where
 
   apply : ∀ {n} → A → Vec A n → A
   apply {n} a vec = chain (a ∷ vec) (λ x y → x ⨾ y)
-
+```
+
+<details>
+```agda
   private
     opaque
       unfolding reverse
       unfolding foldl
       unfolding chain
       applyWorks : ∀ K a b → apply K (a ∷ b ∷ []) ≡ K ⨾ a ⨾ b
       applyWorks K a b = refl
+```
+</details>
+
+On an applicative structure we can define Feferman structure (or SK structure). We call an applicative structure endowed with Feferman structure a **combinatory algebra**.
 
+```agda
   record Feferman : Type ℓ where
     field
       s : A
       k : A
       kab≡a : ∀ a b → k ⨾ a ⨾ b ≡ a
       sabc≡ac_bc : ∀ a b c → s ⨾ a ⨾ b ⨾ c ≡ (a ⨾ c) ⨾ (b ⨾ c)
-
+```
+
+Feferman structure allows us to construct **combinatorial completeness** structure.
+
+Imagine we have a term `t : Term n` (for some `n : ℕ`). We can ask if `A` has a "copy" of `t` so that application would correspond to subsitution. That is, we may ask if we can find an `a : A` such that
+`a ⨾ < a¹ ⨾ a² ⨾ .... ⨾ aⁿ >` (here the `< ... >` notation represents a chain of applications) would be equal to `t [a¹ / # 0 , a² / # 1 , .... , aⁿ / # (pred n) ]`. If the applicative structure additionally can be endowed with Feferman structure - then the answer is yes. 
+
+To get to such a term, we first need to define a function that takes `Term (suc n)` to `Term n` by "abstracting" the free variable represented by the index `# 0`.
+
+We will call this `λ*abst` and this will turn out to behave very similar to λ abstraction - and we will also show that it validates a kind of β reduction rule.
+
+```agda
   module ComputationRules (feferman : Feferman) where
     open Feferman feferman
 
@@ -79,9 +122,15 @@ module _ {ℓ} {A : Type ℓ} (as : ApplicativeStructure A) where
       λ*abst {n} (# (suc x)) = ` k ̇ # x
       λ*abst {n} (` x) = ` k ̇ ` x
       λ*abst {n} (e ̇ e₁) = ` s ̇ λ*abst e ̇ λ*abst e₁
+```
+
+**Remark** : It is important to note that in general, realizability is developed using **partial combinatory algebras** and **partial applicative structures**. In this case, `λ*abst` is not particularly well-behaved. The β reduction-esque rule we derive also does not behave *completely* like β reduction. See Jonh Longley's PhD thesis "Realizability Toposes and Language Semantics" Theorem 1.1.9.
 
-    -- Some shortcuts
+**Remark** : We declare the definition as `opaque` - this is important. If we let Agda unfold this definition all the way we ocassionally end up with unreadable goals containing a mess of `s` and `k`. 
 
+We define meta-syntactic sugar for some of the more common cases :
+
+```agda
     λ* : Term one → A
     λ* t = ⟦ λ*abst t ⟧ []
 
@@ -93,7 +142,14 @@ module _ {ℓ} {A : Type ℓ} (as : ApplicativeStructure A) where
 
     λ*4 : Term four → A
     λ*4 t = ⟦ λ*abst (λ*abst (λ*abst (λ*abst t))) ⟧ []
+```
+
+We now show that we have a β-reduction-esque operation. We proceed by induction on the structure of the term and the number of free variables.
 
+For the particular combinatory algebra Λ/β (terms of the untyped λ calculus quotiented by β equality) - this β reduction actually coincides with the "actual" β reduction.
+TODO : Prove this.
+
+```agda
     opaque
       unfolding λ*abst
       βreduction : ∀ {n} → (body : Term (suc n)) → (prim : A) → (subs : Vec A n) → ⟦ λ*abst body ̇ ` prim ⟧ subs ≡ ⟦ body ⟧ (prim ∷ subs)
@@ -113,14 +169,22 @@ module _ {ℓ} {A : Type ℓ} (as : ApplicativeStructure A) where
           ≡⟨ cong₂ (λ x y → x ⨾ y) (βreduction rator prim subs) (βreduction rand prim subs) ⟩
         ⟦ rator ⟧ (prim ∷ subs) ⨾ ⟦ rand ⟧ (prim ∷ subs)
           ∎
+```
 
+<details>
+```agda
     λ*chainTerm : ∀ n → Term n → Term zero
     λ*chainTerm zero t = t
     λ*chainTerm (suc n) t = λ*chainTerm n (λ*abst t)
 
     λ*chain : ∀ {n} → Term n → A
     λ*chain {n} t = ⟦ λ*chainTerm n t ⟧ []
+```
+</details>
+
+We provide useful reasoning combinators that are useful and frequent.
 
+```agda
     opaque
       unfolding reverse
       unfolding foldl
@@ -169,3 +233,4 @@ module _ {ℓ} {A : Type ℓ} (as : ApplicativeStructure A) where
           ≡⟨ βreduction t d (c ∷ b ∷ a ∷ []) ⟩
         ⟦ t ⟧ (d ∷ c ∷ b ∷ a ∷ [])
           ∎
+```

src/Realizability/PERs/PER.agda

@@ -0,0 +1,82 @@
+open import Realizability.ApplicativeStructure
+open import Realizability.CombinatoryAlgebra
+open import Realizability.PropResizing
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure using (⟨_⟩; str)
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Equiv
+open import Cubical.Functions.FunExtEquiv
+open import Cubical.Relation.Binary
+open import Cubical.Data.Sigma
+
+module Realizability.PERs.PER
+  {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
+
+isPartialEquivalenceRelation : PropRel A A ℓ → Type _
+isPartialEquivalenceRelation (rel , isPropValuedRel) = BinaryRelation.isSym rel × BinaryRelation.isTrans rel
+
+isPropIsPartialEquivalenceRelation : ∀ r → isProp (isPartialEquivalenceRelation r)
+isPropIsPartialEquivalenceRelation (rel , isPropValuedRel) =
+  isProp×
+    (isPropΠ (λ x → isPropΠ λ y → isProp→ (isPropValuedRel y x)))
+    (isPropΠ λ x → isPropΠ λ y → isPropΠ λ z → isProp→ (isProp→ (isPropValuedRel x z)))
+
+record PER : Type (ℓ-suc ℓ) where
+  no-eta-equality
+  constructor makePER
+  field
+    relation : A → A → Type ℓ
+    isPropValuedRelation : ∀ x y → isProp (relation x y)
+    isPER : isPartialEquivalenceRelation (relation , isPropValuedRelation)
+  isSymmetric = isPER .fst
+  isTransitive = isPER .snd
+
+open PER
+
+PERΣ : Type (ℓ-suc ℓ)
+PERΣ = Σ[ relation ∈ (A → A → hProp ℓ) ] isPartialEquivalenceRelation ((λ a b → ⟨ relation a b ⟩) , λ a b → str (relation a b))
+
+IsoPERΣPER : Iso PERΣ PER
+PER.relation (Iso.fun IsoPERΣPER (relation , isPER)) x y = ⟨ relation x y ⟩
+PER.isPropValuedRelation (Iso.fun IsoPERΣPER (relation , isPER)) x y = str (relation x y)
+PER.isPER (Iso.fun IsoPERΣPER (relation , isPER)) = isPER
+Iso.inv IsoPERΣPER per = (λ x y → per .relation x y , per .isPropValuedRelation x y) , (isSymmetric per) , (isTransitive per)
+-- refl does not work because of no-eta-equality maybe?
+relation (Iso.rightInv IsoPERΣPER per i) = λ a b → per .relation a b
+isPropValuedRelation (Iso.rightInv IsoPERΣPER per i) = λ a b → per .isPropValuedRelation a b
+isPER (Iso.rightInv IsoPERΣPER per i) = (isSymmetric per) , (isTransitive per)
+Iso.leftInv IsoPERΣPER perΣ =
+  Σ≡Prop
+    (λ x → isPropIsPartialEquivalenceRelation ((λ a b → ⟨ x a b ⟩) , (λ a b → str (x a b))))
+    (funExt₂ λ a b → Σ≡Prop (λ x → isPropIsProp) refl)
+
+PERΣ≃PER : PERΣ ≃ PER
+PERΣ≃PER = isoToEquiv IsoPERΣPER
+
+isSetPERΣ : isSet PERΣ
+isSetPERΣ = isSetΣ (isSet→ (isSet→ isSetHProp)) (λ rel → isProp→isSet (isPropIsPartialEquivalenceRelation ((λ a b → ⟨ rel a b ⟩) , (λ a b → str (rel a b)))))
+
+isSetPER : isSet PER
+isSetPER = isOfHLevelRespectEquiv 2 PERΣ≃PER isSetPERΣ
+
+module ResizedPER (resizing : hPropResizing ℓ) where
+  private
+    smallHProp = resizing .fst
+    hProp≃smallHProp = resizing .snd
+    smallHProp≃hProp = invEquiv hProp≃smallHProp
+
+  ResizedPER : Type ℓ
+  ResizedPER = Σ[ relation ∈ (A → A → smallHProp) ] isPartialEquivalenceRelation ((λ a b → ⟨ equivFun (smallHProp≃hProp) (relation a b) ⟩) , λ a b → str (equivFun (smallHProp≃hProp) (relation a b)))
+
+  PERΣ≃ResizedPER : PERΣ ≃ ResizedPER
+  PERΣ≃ResizedPER =
+    Σ-cong-equiv-prop
+      (equiv→ (idEquiv A) (equiv→ (idEquiv A) hProp≃smallHProp))
+      (λ relation → isPropIsPartialEquivalenceRelation ((λ a b → ⟨ relation a b ⟩) , (λ a b → str (relation a b))))
+      (λ resizedRelation → isPropIsPartialEquivalenceRelation ((λ a b → ⟨ equivFun (smallHProp≃hProp) (resizedRelation a b) ⟩) , λ a b → str (equivFun smallHProp≃hProp (resizedRelation a b))))
+      (λ relation isPERRelation → (λ a b aRb → {!!}) , λ a b c aRb bRc → {!!})
+      λ relation isPERRelation → {!!}
+
+  PER≃ResizedPER : PER ≃ ResizedPER
+  PER≃ResizedPER = compEquiv (invEquiv PERΣ≃PER) PERΣ≃ResizedPER

src/Realizability/PERs/SystemF.agda

@@ -0,0 +1,40 @@
+open import Cubical.Foundations.Prelude
+
+module Realizability.PERs.SystemF where
+
+module Syntax where
+  -- Only one kind for now
+  -- System Fω has a simply typed lambda calculus at the type level
+  -- Inspired heavily by
+  -- "System F in Agda for Fun and Profit"
+  data Kind : Type where
+    tp : Kind
+
+  data TypeCtxt : Type where
+    [] : TypeCtxt
+    _,_ : TypeCtxt → Kind → TypeCtxt
+
+  data _∈*_ : Kind → TypeCtxt → Type where
+    here : ∀ {k Γ} → k ∈* (Γ , k)
+    there : ∀ {k Γ k'} → k ∈* Γ → k ∈* (Γ , k')
+
+  data Tp : TypeCtxt → Kind → Type where
+    var : ∀ {Γ k} → k ∈* Γ → Tp Γ k
+    funcTp : ∀ {Γ k} → Tp Γ k → Tp Γ k → Tp Γ k
+    prodTp : ∀ {Γ k} → Tp Γ k → Tp Γ k → Tp Γ k
+    forallTp : ∀ {Γ k} → Tp (Γ , k) tp → Tp Γ tp
+
+  data TermCtxt : TypeCtxt → Type where
+    [] : TermCtxt []
+    _,*_ : ∀ {Γ k} → TermCtxt Γ → k ∈* Γ → TermCtxt (Γ , k)
+    _,_ : ∀ {Γ} → TermCtxt Γ → Tp Γ tp → TermCtxt Γ
+
+  -- This is a better notion of renaming than as an inductive type?
+  Ren* : TypeCtxt → TypeCtxt → Type
+  Ren* Γ Δ = ∀ {K} → K ∈* Γ → K ∈* Δ
+
+  data _∈_ : ∀ {Γ} → Tp Γ tp → TermCtxt Γ → Type where
+    here : ∀ {Γ} {A : Tp Γ tp} {Θ : TermCtxt Γ} → A ∈ (Θ , A)
+    thereType : ∀ {Γ} {A B : Tp Γ tp} {Θ : TermCtxt Γ} → A ∈ Θ → A ∈ (Θ , B)
+
+