wip

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))

type-theory.agda-lib

@@ -1,2 +1,2 @@
-include: src src/ThesisWork talks
+include: src src/ThesisWork src/AOP talks
 depend: standard-library cubical