From 7e55ae9b795ceb9fcd3844e70e23c3ded36f023d Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 12 Dec 2024 12:35:04 -0600
Subject: [PATCH] wip

---
 src/AOP/Focus.agda   | 113 +++++++++++++++++++++++++++++++++++++++++++
 type-theory.agda-lib |   2 +-
 2 files changed, 114 insertions(+), 1 deletion(-)
 create mode 100644 src/AOP/Focus.agda

diff --git a/src/AOP/Focus.agda b/src/AOP/Focus.agda
new file mode 100644
index 0000000..2c0327f
--- /dev/null
+++ b/src/AOP/Focus.agda
@@ -0,0 +1,113 @@
+module Focus where
+
+open import Data.Product
+
+-- Forwards lists grow on the left
+-- Mnemonic: > indicates the forward direction
+infixr 5 _:>_
+data List> (A : Set) : Set where
+  [>]  : List> A
+  _:>_ : A → List> A → List> A
+
+-- Backwards lists grow on the right
+-- Mnemonic: < indicates the backward direction
+infixl 5 _:<_
+data List< (A : Set) : Set where
+  [<]  : List< A
+  _:<_ : List< A → A → List< A
+
+variable
+  A : Set
+  x : A
+  xs : List> A
+  sx : List< A -- 'xs' backwards ;)
+
+------------------------------------------------------------------------
+-- Combining lists
+--
+-- There are two ways to combine forwards & backwards lists in an
+-- order-preserving manner depending on the output type.
+
+
+-- 1. Fish
+-- Mnemonic: _<><_ takes a backwards (<) and a forwards (>) list and
+-- returns a backwards one (<)
+
+infixl 5 _<><_
+-- Implement fish
+_<><_ : List< A → List> A → List< A
+b <>< [>] = b
+b <>< (x :> f) = b :< x <>< f
+
+-- 2. Chips
+-- Mnemonic: _<>>_ takes a backwards (<) and a forwards (>) list and
+-- returns a forwards one (>)
+
+infixr 5 _<>>_
+-- Implement chips
+_<>>_ : List< A → List> A → List> A
+[<] <>> f = f
+(b :< x) <>> f = b <>> (x :> f)
+
+module _ where
+  open import Data.Nat
+  open import Relation.Binary.PropositionalEquality
+
+  a : List< ℕ
+  a = [<] :< 1 :< 2 :< 3
+
+  b : List> ℕ
+  b = 4 :> 5 :> 6 :> [>]
+
+  ab : List< ℕ
+  ab = [<] :< 1 :< 2 :< 3 :< 4 :< 5 :< 6
+
+  ab' : List> ℕ
+  ab' = 1 :> 2 :> 3 :> 4 :> 5 :> 6 :> [>]
+
+  _ : a <>< b ≡ ab
+  _ = refl
+  
+  _ : a <>> b ≡ ab'
+  _ = refl
+
+------------------------------------------------------------------------
+-- Locating an element in the middle of a forward list
+
+-- Using these combinators we can explain what it means for an
+-- element to be in focus inside of a forward list: the list
+-- can be decomposed into a backward prefix chipsed onto the
+-- element itself in front of a forward suffix.
+
+infix 1 _∈_
+infix 3 _[_]_
+data _∈_ {A : Set} :  A → List> A → Set where
+  _[_]_ : (sx : List< A) (x : A) (xs : List> A) → x ∈ (sx <>> x :> xs)
+
+------------------------------------------------------------------------
+-- Pointwise lifting a predicate over a forward list
+
+-- Describing what it means for a predicate P to hold of
+-- all the elements in a forwards list.
+-- We overload the list constructors as the structure is
+-- exactly the same:
+--   1. P is trivially true of all the elements in the empty list
+--   2. P is true of all the elements in the list (x :> xs) iff
+--       i. it is true of x
+--       ii. it is true of all the elements in xs
+
+data All> (P : A → Set) : List> A → Set where
+  [>]  : All> P [>]
+  _:>_ : P x → All> P xs → All> P (x :> xs)
+
+------------------------------------------------------------------------
+-- Focusing on all the elements in sight
+
+-- Every element in a list can be focused on
+focus : (xs : List> A) → All> (_∈ xs) xs
+focus list = iter-focus list list ([<] , refl) where
+  open import Relation.Binary.PropositionalEquality using (_≡_; subst; sym; refl)
+  open import Data.Product using (∃)
+  iter-focus : (list : List> A) (remain : List> A) (p : ∃ (λ sx → list ≡ sx <>> remain)) → All> (_∈ list) remain
+  iter-focus list [>] (sx , eq) = [>]
+  iter-focus list (x :> remain) (sx , eq) = subst (λ l → x ∈ l) (sym eq) (sx [ x ] remain) :> (iter-focus list remain ((sx :< x) , eq))
\ No newline at end of file
diff --git a/type-theory.agda-lib b/type-theory.agda-lib
index 50febec..9ad3605 100644
--- a/type-theory.agda-lib
+++ b/type-theory.agda-lib
@@ -1,2 +1,2 @@
-include: src src/ThesisWork talks
+include: src src/ThesisWork src/AOP talks
 depend: standard-library cubical