One.agda

{-# OPTIONS --allow-unsolved-metas #-}
module Exercise.One where

open import Lib.Basics
open import Lib.Nat

------------------------------------------------------------------------------
-- ORDER-PRESERVING EMBEDDINGS (or "thinnings" for short)
------------------------------------------------------------------------------

-- The type xs <: ys represents the possible order-preserving
-- embeddings from xs to ys. That means ys is generated by
-- inserting more stuff anywhere in xs, i.e. "thinning" xs.

data _<:_ {X : Set} : List X -> List X -> Set where
  o' : forall {x ys zs} -> ys <: zs ->       ys  <:  x ,- zs  -- insert new
  os : forall {x ys zs} -> ys <: zs ->  x ,- ys  <:  x ,- zs  -- keep old
  oz :                                    []     <:    []     -- done!

infix 50 _<:_

-- You can also think of xs <: ys as the ways of selecting
-- elements xs from ys, with
--   o' meaning "drop the head",
--   os meaning "take the head",
--   oz meaning "end of list".

-- You can also see a thinning in xs <: ys as a vector of bits
-- telling whether each element position in ys is connected
-- from an element position in xs.

--              2 ,-      4 ,- []
--    o'  (o'  (os  (o'  (os   oz))))
--    0 ,- 1 ,- 2 ,- 3 ,- 4 ,- []


------------------------------------------------------------------------------
-- Exploration (for comprehension rather than credit)
------------------------------------------------------------------------------

-- Lists of elements of One are a lot like numbers

num : Nat -> List One
num zero    = []
num (suc n) = <> ,- num n

-- Using C-c C-a with -l and -s options, generate exhaustive lists of
-- thinnings with the following types.

pick0from4 : List (num 0 <: num 4)
pick0from4 = {!!}

pick1from4 : List (num 1 <: num 4)
pick1from4 = {!!}

pick2from4 : List (num 2 <: num 4)
pick2from4 = {!!}

pick3from4 : List (num 3 <: num 4)
pick3from4 = {!!}
          
pick4from4 : List (num 4 <: num 4)
pick4from4 = {!!}

-- But with more interesting elements, we have fewer options, sometimes.

thinOdds : List (1 ,- 3 ,- 5 ,- [] <: 0 ,- 1 ,- 2 ,- 3 ,- 4 ,- 5 ,- 6 ,- [])
thinOdds = {!!}


------------------------------------------------------------------------------
-- 1.1 Categorical Structure
------------------------------------------------------------------------------

-- Construct the identity thinning from any list to itself.

oi : forall {X}{xs : List X} -> xs <: xs
oi = {!!}

-- Give composition for thinnings. Minimize the number of cases.

_-<-_ : forall {X}{xs ys zs : List X} -> xs <: ys -> ys <: zs -> xs <: zs
th -<- ph = {!!}

infixl 40 _-<-_

-- Prove the following laws. Minimize the number of cases (which will
-- depend on your definition of _-<-_).

oi-<- : forall {X}{xs ys : List X}(ph : xs <: ys) -> oi -<- ph == ph
oi-<- ph = {!!}

_-<-oi : forall {X}{xs ys : List X}(th : xs <: ys) -> th -<- oi == th
th -<-oi = {!!}

assoc-<- : forall {X}{ws xs ys zs : List X}
             (th0 : ws <: xs)(th1 : xs <: ys)(th2 : ys <: zs) ->
             (th0 -<- th1) -<- th2 == th0 -<- (th1 -<- th2)
assoc-<- th0 th1 th2 = {!!}


------------------------------------------------------------------------------
-- 1.2 Emptiness
------------------------------------------------------------------------------

-- Show that the empty list embeds into all lists in a unique way.

oe : forall {X}{xs : List X} -> [] <: xs
oe = {!!}

oe-unique : forall {X}{xs : List X}(th : [] <: xs) -> th == oe
oe-unique th = {!!}


------------------------------------------------------------------------------
-- 1.3 Antisymmetry
------------------------------------------------------------------------------

-- Show that if two lists are mutually embeddable, they are equal
-- and the embeddings are the identity.

antisym : forall {X}{xs ys : List X}
             (th : xs <: ys)(ph : ys <: xs) ->
             Sg (xs == ys) \
             { refl -> th == oi * ph == oi }
antisym th ph = {!!}

-- Deduce that oi is unique.

oi-unique : forall {X}{xs : List X}(th : xs <: xs) -> th == oi
oi-unique th = {!!}


------------------------------------------------------------------------------
-- 1.4 Thinnings as selections
------------------------------------------------------------------------------

-- We can use the "selection" interpretation of thinnings to act
-- on data indexed by lists.
-- The type All P ys has elements of type P y for each y in ys.
-- If xs <: ys, show that we can get P x for each x in xs.

select : forall {X}{xs ys : List X}{P : X -> Set} ->
         xs <: ys -> All P ys -> All P xs
select th pys = {!!}

-- Now prove the following laws relating to selecting by the
-- identity and composition.

select-oi : forall {X}{xs : List X}{P : X -> Set} -> (pxs : All P xs) ->
            select oi pxs == pxs
select-oi pxs = {!!}

select-<- : forall {X}{xs ys zs : List X}{P : X -> Set} ->
            (th : xs <: ys)(ph : ys <: zs) -> (pzs : All P zs) ->
            select (th -<- ph) pzs == select th (select ph pzs)
select-<- th ph pzs = {!!}


------------------------------------------------------------------------------
-- 1.5 Splittings
------------------------------------------------------------------------------

-- If we have two thinnings,
--   th : xs <: zs
--   ph : ys <: zs
-- we can say what it means for th and ph to *split* zs:
-- every element position in zs is connected from either
-- a position in xs or from a position in ys, but *not both*.

data Splitting {X : Set} : {xs ys zs : List X}
                           (th : xs <: zs)(ph : ys <: zs) 
                           -> Set where
  split's : forall {w xs ys zs}{th : xs <: zs}{ph : ys <: zs} ->
             Splitting th ph ->
             Splitting {zs = w ,- _} (o' th) (os ph)
  splits' : forall {w xs ys zs}{th : xs <: zs}{ph : ys <: zs} ->
             Splitting th ph ->
             Splitting {zs = w ,- _} (os th) (o' ph)
  splitzz : Splitting oz oz

-- Show that if we know how xs <: zs, we can find a splitting of zs by
-- computing...

thinSplit : {X : Set}{xs zs : List X}(th : xs <: zs) ->
            Sg (List X) \ ys ->    -- ...what wasn't from xs...
            Sg (ys <: zs) \ ph ->  -- ...but was in zs...
            Splitting th ph        -- ...hence forms a splitting.
thinSplit th = {!!}

-- Given a splitting, show that we can "riffle" together a bunch
-- of "All P"-s for each selection to get an "All P" for the whole.

riffle : forall {X : Set}{xs ys zs : List X}
                {th : xs <: zs}{ph : ys <: zs}
                {P : X -> Set} ->
                All P xs -> Splitting th ph -> All P ys ->
                All P zs
riffle pxs s pys = {!!}

-- Moreover, we can use a splitting to invert "riffle", dealing
-- out an "All P" for the whole list into the parts for each
-- selection in the splitting, and making sure that the parts
-- riffle back together to make the whole.

data Deal {X : Set}{xs ys zs : List X}
          {th : xs <: zs}{ph : ys <: zs}(s : Splitting th ph)
          {P : X -> Set} :
            All P zs -> Set where
  dealt : (pxs : All P xs)(pys : All P ys) -> Deal s (riffle pxs s pys)

deal : {X : Set}{xs ys zs : List X}
       {th : xs <: zs}{ph : ys <: zs}(s : Splitting th ph)
       {P : X -> Set}(pzs : All P zs) -> Deal s pzs
deal s pzs = {!!}


------------------------------------------------------------------------------
-- 1.6 Composability as a relation
------------------------------------------------------------------------------

-- We have the composition *operator*, but it is sometimes more
-- convenient to work with the *call graph* of the composition operator,
-- giving the explanations for why an output comes from some input.

-- For example, the call graph of our boolean <= operator from Lecture.One
--   _<=_ : Nat -> Nat -> Two
--   zero <= y = tt
--   suc x <= zero = ff
--   suc x <= suc y = x <= y

-- would be
--   data Graph<= : Nat -> Nat -> Two -> Set where
--     le-z-y : forall {y} -> Graph<= zero    y    tt
--     le-s-z : forall {x} -> Graph<= (suc x) zero ff
--     le-s-s : forall {x y b} -> Graph<= x y b -> Graph<= (suc x) (suc y) b

-- so that we can always show
--   graph<= : (x y : Nat) -> Graph<= x y (x <= y)

-- Define the inductive composability relation on three thinnings.
-- This should correspond to your composition function, with one
-- constructor per line of your function, and one recursive substructure
-- per recursive call. We've written the type declaration, but you need
-- to add the constructors.

-- No defined function symbols should appear in any of the type indices,
-- just variables and constructors. That means dependent pattern matching
-- will play nice.

data Composable-<- {X : Set}
     : {xs ys zs : List X}
       (th : xs <: ys)(ph : ys <: zs)(thph : xs <: zs)
       -> Set where
  -- your constructors here!

-- Show that your definition really captures composability by
-- proving the following.

composable-<- : forall {X : Set}{xs ys zs : List X}
                (th : xs <: ys)(ph : ys <: zs) ->
                Composable-<- th ph (th -<- ph)
  -- i.e., we have *at least* composition...
composable-<- th ph = {!!}

composable-unique : forall {X : Set}{xs ys zs : List X}
                    {th : xs <: ys}{ph : ys <: zs}
                    {thph thph' : xs <: zs} ->
                    Composable-<- th ph thph ->
                    Composable-<- th ph thph' ->
                    thph == thph'
  -- ...and nothing but composition.
composable-unique c d = {!!}

-- Your prize for establishing the graph representation is to have a nice time
-- showing that thinnings really are *embeddings* (or "monomorphisms").
-- If you have two thinnings, th and th' that compose with some ph to get
-- equal results, th and th' must have been equal in the first place. That
-- tells you something important about ph, namely that it maps all its source
-- positions to distinct target positions.

composable-mono : forall {X}{xs ys zs : List X}
  {th th' : xs <: ys}{ph : ys <: zs}{ps : xs <: zs} ->
  Composable-<- th ph ps -> Composable-<- th' ph ps ->
  th == th'
composable-mono c d = {!!}

-- Now use composable-<- and composable-mono to get a cheap proof of the
-- following.

mono-<- : forall {X}{xs ys zs : List X}(th th' : xs <: ys)(ph : ys <: zs) ->
             th -<- ph == th' -<- ph ->
             th == th'
mono-<- th th' ph q = {!!}


------------------------------------------------------------------------------
-- 1.7 Pullbacks (pointwise "and")
------------------------------------------------------------------------------

-- If we have a situation like this

--
--                ys
--                |
--                | ph
--                v
--     xs ------> zs
--           th

-- we say a "BackSquare" extends the situation to a square

--         side1
-- corner ------> ys
--      |         |
-- side0|         | ph
--      v         v
--     xs ------> zs
--           th

-- where the *same* diagonal is both side0 -<- th and side1 -<- ph,
-- so either path around the square gives the same thinning.

record BackSquare {X}{xs ys zs : List X}
              (th : xs <: zs)(ph : ys <: zs) : Set where
  constructor backSquare
  field
    {corner}   : List X
    {side0}    : corner <: xs
    {side1}    : corner <: ys
    {diagonal} : corner <: zs
    triangle0  : Composable-<- side0 th diagonal
    triangle1  : Composable-<- side1 ph diagonal

open BackSquare

-- The corner of the "best" BackSquare is called a *pullback*,
-- (and the square is called a "pullback square"). What's best
-- about it is that the corner of every other BackSquare embeds
-- in it. That is, it has all the things that both th and ph
-- select from zs.

-- First, construct the pullback square.

pullback-<- : forall {X}{xs ys zs : List X} ->
              (th : xs <: zs)(ph : ys <: zs) ->
              BackSquare th ph
pullback-<- th ph = {!!}

-- Then show that every other BackSquare has a corner
-- which embeds in the pullback, and that the resulting
-- triangles commute.

pullback-best : forall {X}{xs ys zs : List X} ->
                {th : xs <: zs}{ph : ys <: zs} ->
                let bs = pullback-<- th ph in
                (bs' : BackSquare th ph) ->
                Sg (corner bs' <: corner bs) \ ps ->
                Composable-<- ps (side0 bs) (side0 bs') *
                Composable-<- ps (side1 bs) (side1 bs')
pullback-best bs' = {!!}