wip

README.md

@@ -6,4 +6,4 @@ including my progress into research for my master's degree.
 
 Links:
 
-- [my current focus](https://git.mzhang.io/school/cubical/projects/2)
+- [my current focus](https://git.mzhang.io/michael/type-theory/projects/8)

src/CEKCoinductive.agda

@@ -1,22 +0,0 @@
-{-# OPTIONS --guardedness #-}
-
-module CEKCoinductive where
-
-open import Agda.Primitive
-
-private
-  variable
-    l l1 l2 l3 : Level
-
-    E : Set → Set
-    R : Set
-
-data ITreeF (ITree : Set) : Set where
-  Ret : (r : R) → ITreeF ITree
-  Tau : (t : ITree) → ITreeF ITree
-  Vis : {A : Set l1} → (e : E A) → (k : A → ITreeF E R) → ITreeF E R
-
-record ITree : Set where
-  coinductive
-  field
-    _observe : ITreeF ITree

src/CubicalHott/Exercise4-6.agda

@@ -0,0 +1,26 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Exercise4-6 where
+
+open import Cubical.Core.Glue
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Transport
+
+variable
+  l : Level
+  A B : Type
+
+idtoqinv : A ≡ B → Iso A B
+idtoqinv {A} {B} p = iso (transport p) (transport (sym p)) s r where
+  s : section (transport p) (transport (λ i → p (~ i)))
+  s b = sym (transportComposite (sym p) p b) ∙ cong (λ p → transport p b) (rCancel (sym p)) ∙ transportRefl b
+
+  r : retract (transport p) (transport (λ i → p (~ i)))
+  r a = sym (transportComposite p (sym p) a) ∙ cong (λ p → transport p a) (rCancel p) ∙ transportRefl a
+
+postulate
+  idtoqinv-← : Iso A B → A ≡ B

src/CubicalHott/Theorem7-1-11.agda

@@ -12,14 +12,7 @@ open import Cubical.Data.Nat
 open import Data.Unit
 
 lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n)
-lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , {!   !} where
-  -- G : A ≡ B
-  -- G = ua (isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr))
-
-  -- g : PathP (λ i → G i) a b
-  -- g = {!   !}
-
-  -- contr : Acontr ≡ Bcontr
+lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , contr where
 
   eqv1 : A ≃ B
   eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
@@ -31,7 +24,11 @@ lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , {!   !} where
   g = glue {T = T} {e = e} (λ { (i = i0) → a ; (i = i1) → b }) b
 
   contr : (y : G) → g ≡ y
-  contr y j = {!   !}
+  contr y j =
+    let p = λ where
+      (i = i0) → Acontr (unglue {A = A} (~ i) {T = T} {e = λ { (i = i0) → idEquiv A }} y) j
+      (i = i1) → Bcontr (unglue {A = B} i {T = T} {e = λ { (i = i1) → idEquiv B }} y) j
+    in glue p {!  b !}
 
     -- unglue i {!   !}
     -- (glue (λ { (i = i1) → {!   !} }) {!   !})

src/Log.lagda.md

@@ -1,60 +0,0 @@
-```
-{-# OPTIONS --cubical #-}
-
-module Log where
-
-open import Cubical.Foundations.Prelude
-```
-
-## 2024-09-12
-
-Trying to get hcomp to work
-
-```
-module log-20240912 where
-  private
-    variable
-      l : Level
-      A : Type l
-      x y z w : A
-      p : x ≡ y
-      q : y ≡ z
-      r : z ≡ w
-      s : w ≡ x
-
-  -- Order of the square is
-  --             4
-  --          +----->+
-  --          ^      ^
-  --        1 |      | 2
-  --          |      |
-  --          +----->+
-  --             3
-  -- In this below case, i is the vertical dimension and j is the horizontal dimension
-  test-square : Square refl refl p p
-  test-square {l} {A} {x} {y} {p} i j = p i
-
-  -- Creating the same square with hfill
-  test-square2 : p ∙ refl ≡ p
-  test-square2 {l} {A} {x} {y} {p} i j = hfill (λ k → λ where
-      (j = i0) → x
-      (j = i1) → y
-    )
-    -- A [ ~ j ∨ j ↦ (λ { (j = i0) → x ; (j = i1) → y }) ]
-    -- looking for some expression s.t when φ = i1, will equal the thing in the expression
-    (inS (p j))
-    (~ i)
-
-  -- Trying to port over the 1lab filler
-  -- This fills a square
-  ∙∙-filler : Square s q p (sym s ∙∙ p ∙∙ q)
-  ∙∙-filler {l} {A} {x} {y} {z} {w} {p} {q} {s} i j = hfill (λ k → λ where
-      (j = i0) → {! s (~ i)  !}
-      (j = i1) → {!   !}
-    ) 
-    {!   !} {! i  !}
-```
-
-Question:
-- How many sides do you need for the hcomp to be correct?
-- What direction, semantically, is the last argument to hfill?

src/LogRel.agda

@@ -0,0 +1,200 @@
+module LogRel where
+
+open import Data.Bool
+open import Data.String
+open import Data.Sum
+open import Data.Empty
+open import Data.Nat
+open import Data.Maybe
+open import Data.Product
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary.Negation
+open import Relation.Nullary using (Dec; yes; no)
+
+_∙_ = trans
+
+data type : Set where
+  bool : type
+  _-→_ : type → type → type
+
+data term : Set where
+  `_ : String → term
+  true : term
+  false : term
+  `if_then_else_ : term → term → term → term
+  `λ[_∶_]_ : String → type → term → term
+  _`∙_ : term → term → term
+
+replace : (e : term) → (x : String) → (v : term) → term
+replace (` y) x v = if x == y then v else (` y)
+replace true x v = true
+replace false x v = false
+replace (`if e then e₁ else e₂) x v = `if (replace e x v) then replace e₁ x v else replace e₂ x v
+replace e @ (`λ[ y ∶ t ] e′) x v = if x == y then e else (`λ[ y ∶ t ] replace e′ x v)
+replace (e₁ `∙ e₂) x v = replace e₁ x v `∙ replace e₂ x v
+
+data value : term → Set where
+  true : value true
+  false : value false
+  `λ[_∶_]_ : (x : String) → (t : type) → (e : term) → value (`λ[ x ∶ t ] e)
+
+to-value : (t : term) → Maybe (value t)
+to-value (` x) = nothing
+to-value true = just true
+to-value false = just false
+to-value (`if t then t₁ else t₂) = nothing
+to-value (`λ[ x ∶ t ] e) = just (`λ[ x ∶ t ] e)
+to-value (t `∙ t₁) = nothing
+
+is-value : (t : term) → Set
+is-value t = Is-just (to-value t)
+
+data ectx : Set where
+  [∙] : ectx
+  `if_then_else_ : ectx → term → term → ectx
+  _`∙_ : ectx → term → ectx
+  _∙`_ : {e : term} → value e → ectx → ectx
+
+data ctx : Set where
+  ∅ : ctx
+  _,_∶_ : ctx → String → type → ctx
+
+data sub : Set where
+  ∅ : sub
+  _,_≔_ : sub → String → term → sub
+
+evalsub : sub → term → term
+evalsub ∅ e = e
+evalsub (γ , x ≔ v) e = replace (evalsub γ e) x v
+
+lookup : ctx → String → Maybe type
+lookup ∅ x = nothing
+lookup (Γ , y ∶ t) x = if (x == y) then just t else lookup Γ x
+
+-- Some dumb stuff
+
+lemma1 : ∀ (γ : sub) → evalsub γ true ≡ true
+lemma1 ∅ = refl
+lemma1 (γ , x ≔ v) = cong (λ z → replace z x v) (lemma1 γ)
+
+lemma2 : ∀ (γ : sub) → evalsub γ false ≡ false
+lemma2 ∅ = refl
+lemma2 (γ , x ≔ v) = cong (λ z → replace z x v) (lemma2 γ)
+
+-- Operational semantics
+
+data _↦_ : term → term → Set where
+  rule1 : (e1 e2 : term) → (if true then e1 else e2) ↦ e1
+  rule2 : (e1 e2 : term) → (if false then e1 else e2) ↦ e2
+  rule3 : (x : String) → (t : type) → (e : term) → (v : term)
+    → ((`λ[ x ∶ t ] e) `∙ v) ↦ replace e x v
+
+data iter : ℕ → term → term → Set where
+  iter-zero : ∀ (e : term) → iter zero e e
+  iter-suc : ∀ (n : ℕ) → (e e′ e′′ : term) → iter n e e′ → (e′ ↦ e′′) → iter (suc n) e′ e′′
+
+_↦∙_ : term → term → Set
+e ↦∙ e′ = Σ ℕ λ n → iter n e e′
+
+-- Type judgments
+
+data _⊢_∶_ : ctx → term → type → Set where
+  type1 : (Γ : ctx) → Γ ⊢ true ∶ bool
+  type2 : (Γ : ctx) → Γ ⊢ false ∶ bool
+  type3 : (Γ : ctx) → (x : String) → (tw : Is-just (lookup Γ x)) → Γ ⊢ ` x ∶ to-witness tw
+  type4 : (Γ : ctx) → (x : String) → (e : term) → (t₁ t₂ : type)
+    → ((Γ , x ∶ t₁) ⊢ e ∶ t₂) → Γ ⊢ `λ[ x ∶ t₁ ] e ∶ (t₁ -→ t₂)
+  type5 : (Γ : ctx) → (e₁ e₂ : term) → (t t₂ : type)
+    → (Γ ⊢ e₁ ∶ (t₂ -→ t)) → (Γ ⊢ e₂ ∶ t₂) → Γ ⊢ e₁ `∙ e₂ ∶ t
+  type6 : (Γ : ctx) → (e e₁ e₂ : term) → (t : type)
+    → (Γ ⊢ e ∶ bool) → (Γ ⊢ e₁ ∶ t) → (Γ ⊢ e₂ ∶ t)
+    → Γ ⊢ `if e then e₁ else e₂ ∶ t
+
+-- Type soundness
+
+type-soundness : ∀ {e e′ t} → (∅ ⊢ e ∶ t) → (e ↦∙ e′) → Set
+type-soundness {e = e} {e′ = e′} {t = t} prf eval =
+  (value e) ⊎ Σ term λ e′′ → e′ ↦ e′′
+
+-- Safety
+
+safe : term → Set
+safe e = ∀ (e′ : term) → e ↦∙ e′ → (value e′) ⊎ Σ term (λ e′′ → (e′ ↦ e′′))
+
+-- Logical relations
+
+data V : type → term → Set
+data E : type → term → Set
+  
+data V where
+  bool-true : V bool true
+  bool-false : V bool false
+  →-λ : ∀ (x : String) → (e : term) → (t₁ t₂ : type)
+    → ((v : term) → V t₁ v → E t₂ (replace e x v)) → V (t₁ -→ t₂) (`λ[ x ∶ t₁ ] e)
+
+irred : (e : term) → Set
+irred e = ¬ (Σ term (λ e′ → e ↦ e′))
+
+data E where
+  erel : ∀ (e : term) → (t : type)
+    → ((e′ : term) → ((e ↦∙ e′) × irred e′) → V t e′) → E t e
+
+data G : ctx → sub → Set where
+  nil : G ∅ ∅
+  cons : ∀ (Γ : ctx) → (x : String) → (t : type) → (γ : sub) → (v : term)
+    → (G Γ γ) ⊎ V t v
+    → G (Γ , x ∶ t) (γ , x ≔ v)
+
+-- Semantically well-typed
+
+_⊨_∶_ : (Γ : ctx) → (e : term) → (t : type) → Set 
+Γ ⊨ e ∶ t = ∀ (γ : sub) → G Γ γ → E t (evalsub γ e)
+
+-- Theorem 4.2: fundamental property of logical relations
+
+theorem42 : ∀ (Γ : ctx) → (e : term) → (t : type) → Γ ⊢ e ∶ t → Γ ⊨ e ∶ t
+theorem42 Γ e t (type1 .Γ) γ G[γ] =
+  subst (E bool) (sym (lemma1 γ)) (erel e bool helper) where
+    helper : (e′ : term) → (true ↦∙ e′) × irred e′ → V bool e′
+    helper e′ ((zero , iter-zero .true) , snd) = bool-true
+    helper e′ ((suc n , iter-suc .n e .true .true fst (rule1 .true e2)) , snd) = bool-true
+    helper e′ ((suc n , iter-suc .n e .true .true fst (rule2 e1 .true)) , snd) = bool-true
+theorem42 Γ e t (type2 .Γ) γ G[γ] =
+  subst (E bool) (sym (lemma2 γ)) (erel e bool helper) where
+    helper : (e′ : term) → (false ↦∙ e′) × irred e′ → V bool e′
+    helper e′ ((zero , iter-zero .false) , snd) = bool-false
+    helper e′ ((suc n , iter-suc .n e .false .false fst (rule1 .false e2)) , snd) = bool-false
+    helper e′ ((suc n , iter-suc .n e .false .false fst (rule2 e1 .false)) , snd) = bool-false
+theorem42 Γ e t (type3 .Γ x tw) γ G[γ] = erel {!   !} {!   !} {!   !}
+theorem42 Γ e t (type4 .Γ x e₁ t₁ t₂ sts) ∅ G[γ] = erel (`λ[ x ∶ t₁ ] e₁) t helper where
+  helper : (e′ : term) → ((`λ[ x ∶ t₁ ] e₁) ↦∙ e′) × irred e′ → V (t₁ -→ t₂) e′
+  helper e′ ((zero , iter-zero .(`λ[ x ∶ t₁ ] e₁)) , snd) =
+    →-λ x e₁ t₁ t₂ λ v x₁ → erel {!   !} {!   !} {!   !}
+  helper e′ ((suc n , fst) , snd) = {!   !}
+theorem42 Γ e t (type4 .Γ x e₁ t₁ t₂ sts) (γ , x₁ ≔ x₂) G[γ] =
+  {!   !}
+theorem42 Γ e t (type5 .Γ e₁ e₂ .t t₂ sts sts₁) = {!   !}
+theorem42 Γ e t (type6 .Γ e₁ e₂ e₃ .t sts sts₁ sts₂) ∅ G[γ] =
+  erel (`if e₁ then e₂ else e₃) t helper where
+    helper : (e′ : term) → ((`if e₁ then e₂ else e₃) ↦∙ e′) × irred e′ → V t e′
+    helper e′ ((zero , iter-zero .(`if e₁ then e₂ else e₃)) , snd) =
+      ⊥-elim (snd ((`if e₁ then e₂ else e₃) , rule1 (`if e₁ then e₂ else e₃) e₂)) 
+    helper e′ ((suc n , iter-suc .n e .(`if e₁ then e₂ else e₃) .(`if e₁ then e₂ else e₃) fst (rule1 .(`if e₁ then e₂ else e₃) e2)) , snd) =
+      ⊥-elim (snd ((`if e₁ then e₂ else e₃) , rule1 (`if e₁ then e₂ else e₃) e₂)) 
+    helper e′ ((suc n , iter-suc .n e .(`if e₁ then e₂ else e₃) .(`if e₁ then e₂ else e₃) fst (rule2 e1 .(`if e₁ then e₂ else e₃))) , snd) =
+      ⊥-elim (snd ((`if e₁ then e₂ else e₃) , rule1 (`if e₁ then e₂ else e₃) e₂)) 
+theorem42 Γ e t (type6 .(Γ₁ , x ∶ t₁) e₁ e₂ e₃ .t sts sts₁ sts₂) (γ , x ≔ x₁) (cons Γ₁ .x t₁ .γ .x₁ (inj₁ x₂)) = {!   !}
+theorem42 Γ e t (type6 .(Γ₁ , x ∶ t₁) e₁ e₂ e₃ .t sts sts₁ sts₂) (γ , x ≔ x₁) (cons Γ₁ .x t₁ .γ .x₁ (inj₂ y)) = {!   !}
+
+-- Theorem 4.1: semantic type soundness
+
+theorem41 : ∀ (e : term) → (t : type) → (∅ ⊢ e ∶ t) → safe e
+theorem41 e t ts = goal1 where
+  swt : ∅ ⊨ e ∶ t
+  swt = theorem42 ∅ e t ts
+ 
+  goal2 : E t e
+  goal2 = swt ∅ nil
+
+  goal1 : safe e         
+  goal1 e′ prf = {!   !}