text:
------------------------------------------------------------------------------
-- CS410 Exercise 5
--
-- Given the overrunning of exercise 4, I've decided to shift the deadline
-- for exercise 5 back to the end of semester 2, so you can have a wee go
-- in the last week of semester 1, but then focus on your CS408 projects.
--
-- Exercise 6 will follow directly on from this and share the deadline, but
-- it will be issued at Easter.
--
-- I don't know the precise deadline, because I have not yet been told the
-- mark upload deadline for the semester 2 exam board. I will give you as
-- much time as I can. Usually, I can make the deadline after the last
-- exam, but I haven't seen the timetable yet.
--
-- It's a good idea to start well before the exams, get the basics sorted,
-- then come back to it after the exams and apply polish.
------------------------------------------------------------------------------

module Ex5 where -- Conor: 1.5/15

open import CS410-Prelude
open import CS410-Nat
open import CS410-Vec
open import CS410-Indexed
open import CS410-Monoid

------------------------------------------------------------------------------
-- CHARACTERS AND STRINGS
------------------------------------------------------------------------------
{-
data List (X : Set) : Set where  -- X scopes over the whole declaration...
  []    : List X                 -- ...so you can use it here...
  _::_  : X -> List X -> List X  -- ...and here.
infixr 3 _::_

{-# BUILTIN BOOL Two #-}
{-# BUILTIN TRUE tt #-}
{-# BUILTIN FALSE ff #-}
{-# BUILTIN LIST List #-}
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _::_ #-}
{-# COMPILED_DATA List [] [] (:) #-}

postulate -- this means that we just suppose the following things exist...
  Char : Set
  String : Set
{-# BUILTIN CHAR Char #-}
{-# COMPILED_TYPE Char Char #-}
{-# BUILTIN STRING String #-}
{-# COMPILED_TYPE String String #-}

primitive -- these are baked in; they even work!
  primCharEquality : Char -> Char -> Two
  primStringAppend : String -> String -> String
  primStringToList : String -> List Char
  primStringFromList : List Char -> String
-}

------------------------------------------------------------------------------
-- THE TILING MONAD (from lectures)
------------------------------------------------------------------------------

WH : Set
WH = Nat * Nat

data Tiling (X : WH -> Set)(wh : WH) : Set where
  ! : X wh -> Tiling X wh
  joinH : (wl wr : Nat)(wq : wl +N wr == fst wh) ->
          Tiling X (wl , snd wh) ->  Tiling X (wr , snd wh) -> Tiling X wh
  joinV : (ht hb : Nat)(hq : ht +N hb == snd wh) ->
          Tiling X (fst wh , ht) ->  Tiling X (fst wh , hb) -> Tiling X wh

TilingMonadIx : MonadIx Tiling
TilingMonadIx = record
  { retIx = !
  ; extendIx = help
  } where
  help : {P Q : WH -> Set} -> [ P -:> Tiling Q ] -> [ Tiling P -:> Tiling Q ]
  help f (! p) = f p
  help f (joinH wl wr wq t-l t-r) = joinH wl wr wq (help f t-l) (help f t-r)
  help f (joinV ht hb hq t-t t-b) = joinV ht hb hq (help f t-t) (help f t-b)

-- That's the monad you'll need in this file, so let's open it.

open MonadIx TilingMonadIx
open FunctorIx (monadFunctorIx TilingMonadIx)

------------------------------------------------------------------------------
-- PASTE KITS
------------------------------------------------------------------------------

-- A PasteKit equips rectangular stuff with the means to stick
-- things the same height side-by-side, or things the same width
-- one-on-top-of-the-other

record PasteKit (X : WH -> Set) : Set where
  field
    pasteH :  {wh : WH}(wl wr : Nat)(wq : wl +N wr == fst wh) ->
              X (wl , snd wh) ->  X (wr , snd wh) -> X wh
    pasteV :  {wh : WH}(ht hb : Nat)(hq : ht +N hb == snd wh) ->
              X (fst wh , ht) ->  X (fst wh , hb) -> X wh

-- ??? 5.1 (1 mark) -- Conor: 1/1
-- Show that if you have a PasteKit for X tiles, you can turn a
-- Tiling X into one big X.

paste : forall {X} -> PasteKit X -> [ Tiling X -:> X ]
paste {X} pk = go where
  open PasteKit pk
  go : [ Tiling X -:> X ]
  go (! x) = x
  go (joinH wl wr wq t0 t1) = pasteH wl wr wq (go t0 ) (go t1)
  go (joinV ht hb hq t0 t1) = pasteV ht hb hq (go t0) (go t1)

------------------------------------------------------------------------------
-- CUT KITS
------------------------------------------------------------------------------

-- A CutKit consists of functions which split a rectangular thing in two,
-- horizontally or vertically.

record CutKit (X : WH -> Set) : Set where
  field
    cutH :  {wh : WH}(wl wr : Nat)(wq : wl +N wr == fst wh) ->
            X wh -> X (wl , snd wh) *  X (wr , snd wh)
    cutV :  {wh : WH}(ht hb : Nat)(hq : ht +N hb == snd wh) ->
            X wh -> X (fst wh , ht) *  X (fst wh , hb)

------------------------------------------------------------------------------
-- MATRICES
------------------------------------------------------------------------------

Matrix : Set -> WH -> Set
Matrix C (w , h) = Vec (Vec C w) h

-- ??? 5.2 (2 marks) -- 0/2
-- Equip matrices with a PasteKit and a CutKit. Try to make good use of
-- the operations developed for vectors.

matrixPaste : {C : Set} -> PasteKit (Matrix C)
matrixPaste {C} = record
  {  pasteH = mPH
  ;  pasteV = mPV
  }  where
  mPH : {wh : WH} (wl wr : Nat) -> wl +N wr == fst wh -> Matrix C (wl , snd wh) -> Matrix C (wr , snd wh) -> Matrix C wh
  mPH wl wr wq ml mr = {!!}

  mPV : {wh : WH} (ht hb : Nat) -> ht +N hb == snd wh -> Matrix C (fst wh , ht) -> Matrix C (fst wh , hb) -> Matrix C wh
  mPV ht hb hq mt mb = {!vec !}

matrixCut : {C : Set} -> CutKit (Matrix C)
matrixCut {C} = record
  {  cutH = mCH
  ;  cutV = mCV
  }  where
  mCH : {wh : WH} (wl wr : Nat) -> wl +N wr == fst wh ->
        Matrix C wh -> Matrix C (wl , snd wh) * Matrix C (wr , snd wh)
  mCH wl wr wq m = {!!}
  mCV : {wh : WH} (ht hb : Nat) -> ht +N hb == snd wh ->
        Matrix C wh -> Matrix C (fst wh , ht) * Matrix C (fst wh , hb)
  mCV ht hb hq m = {!!}

---------------------------------------------------------------------------
-- COLOURS
---------------------------------------------------------------------------

-- We're going to be making displays from coloured text.
{-
data Colour : Set where
  black red green yellow blue magenta cyan white : Colour
{-# COMPILED_DATA Colour HaskellSetup.Colour
      HaskellSetup.Black HaskellSetup.Red HaskellSetup.Green
      HaskellSetup.Yellow HaskellSetup.Blue HaskellSetup.Magenta
      HaskellSetup.Cyan HaskellSetup.White #-}
-}
-- Each cell in a display has this information:

record Cell : Set where
  constructor _-_/_
  field
    fgCo  : Colour    -- foreground colour
    char  : Char      -- character to display in cell
    bgCo  : Colour    -- background colour

-- e.g.   white - '*' / black

-- Now,
--      Matrix Cell : WH -> Set
-- is a suitable notion of sized display

---------------------------------------------------------------------------
-- INTERLUDE: TESTING WITH TEXT
---------------------------------------------------------------------------

-- I've written some code which should help you see what you're doing.

-- Turn a list into a vector, either by truncating or padding with
-- a given dummy element.
paddy : {X : Set} -> X -> List X -> {n : Nat} -> Vec X n
paddy _ _         {zero}   = []
paddy x []        {suc n}  = x :: paddy x [] {n}
paddy x (y :: ys) {suc n}  = y :: paddy x ys {n}

-- Turn some colours and a string into a vector of cells
_-_//_ : Colour -> String -> Colour -> {n : Nat} -> Vec Cell n
f - s // b =  vapp  (vapp (vec (_-_/_ f))
                    (paddy ' ' (primStringToList s)))
              (vec b)
infixr 4 _-_//_

-- Build an example matrix
example1 : Matrix Cell (10 , 5)
example1  =   black - "hydrogen"   // white
          ::  black - "helium"     // white
          ::  black - "lithium"    // white
          ::  black - "beryllium"  // white
          ::  black - "boron"      // white
          ::  []

-- Cut it up
example23 : Matrix Cell (5 , 5) * Matrix Cell (5 , 5)
example23 = cutH 5 5 refl example1
  where open CutKit matrixCut

-- Stick the bits back together, vertically
example4 : Matrix Cell (5 , 10)
example4 = pasteV 5 5 refl (fst example23) (snd example23)
  where open PasteKit matrixPaste

---------------------------------------------------------------------------
-- CUTTING UP TILINGS
---------------------------------------------------------------------------

-- Previously...
-- ... we established what it is to be a CutKit, and we built CutKits
-- for some sorts of basic tile. Now we need to build the CutKit for
-- Tilings. Let's think about what that involves for a moment. We're going
-- to need a CutKit for basic tiles to stand a chance. But how do we
-- cut compound tiles?
--
-- Suppose we're writing cutH, and we have some
--   cq : cwl + cwr == w   -- the "cut widths" equation
-- telling us where we want to make the cut in something of width w.
--
--             v
--    +--------:------+
--    |        :      |
--    |        :      |
--    +--cwl---:-cwr--+
--    :        ^      :
--    :.......w.......:
--
-- The tricky part is when the tiling we're cutting here is built with
--   joinH twl twr tq tl tr
-- where
--   tq : twl + twr == w   -- the "tiling widths" equation
--
-- There are three possible situations, all of which you must detect
-- and handle.
--
-- (i) you hit the sweet spot...
--
--             v
--    +--bwl---+-bwr--+
--    |        |      |
--    |        |      |
--    +--cwl---+-cwr--+
--    :        ^      :
--    :.......w.......:
--
--     ...where the box is already divided in the place where the cut
--     has to go. Happy days.
--
-- (ii) you're cutting to the left of the join...
--
--             v
--    +--bwl-----+bwr-+
--    |        : |    |
--    |        : |    |
--    +--cwl---:-cwr--+
--    :        ^      :
--    :.......w.......:
--
--     ...so you'll need to cut the left box in the correct place. You
--     will need some evidence about widths to do that. And then you'll
--     the have three pieces you can see in my diagram, so to complete
--     the cut, you will need to put two of those pieces together, which
--     will take more evidence.
--
-- (iii) you're cutting to the right of the join...
--
--             v
--    +--bwl-+--bwr---+
--    |      | :      |
--    |      | :      |
--    +--cwl---:-cwr--+
--    :        ^      :
--    :.......w.......:
--
--     ...so you'll need to cut the right box in the correct place, and
--     reassemble the bits.
--
-- HINT: The next three tasks go together.

-- ??? 5.3.1 (1 mark) -- Conor: 0.5/1
-- COMPARING THE CUT POSITION

data CutComparable (x x' y y' n : Nat) : Set where
  cutC : y == x -> CutComparable x x' y y' n
--  cutL :
--  cutR :
  -- Give three constructors for this type which characterize the three
  -- possibilities described above whenever
  --   x + x' == n   and   y + y' == n
  -- (E.g., take n to be w, x and x' to be cwl and cwr, y and y' to be
  -- twl and twr. But later, you'll need to do use the same tool for
  -- heights.)
  --
  -- You will need to investigate what evidence must be packaged in each
  -- situation. On the one hand, you need to be able to *generate* the
  -- evidence, with cutCompare, below. On the other hand, the evidence
  -- must be *useful* when you come to write tilingCut, further below.
  -- Don't expect to know what to put here from the get-go. Figure it
  -- out by discovering what you *need*.

  -- YOUR CONSTRUCTORS GO HERE

-- The following facts may come in handy.

sucInject : {m n : Nat} -> suc m == suc n -> m == n
sucInject refl = refl

sucRespect : {m n : Nat} -> m == n -> suc m == suc n
sucRespect refl = refl

-- ??? 5.3.2 (1 mark) -- Conor: 0/1
-- Show that whenever you have two ways to express the same n as a sum,
-- you can always deliver the CutComparable evidence.

cutCompare : (x x' y y' n : Nat) -> x +N x' == n -> y +N y' == n ->
             CutComparable x x' y y' n
cutCompare x x' y y' n xq yq = {!!}

-- ??? 5.3.3 (2 marks) -- Conor: 0/2
-- A CUTKIT FOR TILINGS

-- Now, show that you can construct a CutKit for Tiling X, given a CutKit
-- for X. There will be key points where you get stuck for want of crucial
-- information. The purpose of CutCompare is to *describe* that
-- information. The purpose of cutCompare is to *compute* that information.
-- Note that cutH and cutV will work out very similarly, just exchanging
-- the roles of width and height.

-- Hint: good solutions are likely to use "with" a lot.

tilingCut : {X : WH -> Set} -> CutKit X -> CutKit (Tiling X)
tilingCut {X} ck = record { cutH = cH ; cutV = cV } where
  open CutKit ck
  cH : {wh : WH}(wl wr : Nat)(wq : wl +N wr == fst wh) ->
       Tiling X wh -> Tiling X (wl , snd wh) * Tiling X (wr , snd wh)
  cH cwl cwr cq t = {!!}
  cV : {wh : WH}(ht hb : Nat)(hq : ht +N hb == snd wh) ->
       Tiling X wh -> Tiling X (fst wh , ht) * Tiling X (fst wh , hb)
  cV cht chb cq t = {!!}

---------------------------------------------------------------------------
-- SUPERIMPOSITION
---------------------------------------------------------------------------

-- ??? 5.4 (2 marks) -- Conor: 0/2
-- Suppose you have a tiling made of X tiles in front of a tiling made of
-- Y tiles.  Suppose you have a CutKit for Y. Suppose you know how to
-- superimpose *one* X tile on a Y tiling to make a Z tiling. You should be
-- able to superimpose X tilings on Y tilings to get a Z tiling: you can but
-- the back Y tiling into pieces which fit with the individual X tiles in
-- front.

super : {X Y Z : WH -> Set} -> CutKit Y ->
       [        X -:> Tiling Y -:> Tiling Z ] ->
       [ Tiling X -:> Tiling Y -:> Tiling Z ]
super {X}{Y}{Z} ck m = go where
  open CutKit (tilingCut ck)
  go : [ Tiling X -:> Tiling Y -:> Tiling Z ]
  go xt yt = {!!}

-- HINT: no new recursive operations are needed in the rest of this file.
-- You've done the hard work. Now get paid.

---------------------------------------------------------------------------
-- HOLES
---------------------------------------------------------------------------

-- ??? 5.5 (2 marks) -- Conor: 0/2
-- In order to build up displays in layers, we will need to work with
-- tilings where one sort of primitive tile is, in fact, a hole!

data HoleOr (X : WH -> Set)(wh : WH) : Set where
  hole   : HoleOr X wh           -- a hole you can see through
  block  : X wh -> HoleOr X wh   -- a block of stuff you can't see through

-- Explain how to see through a hole but not through a block

seeThrough : {X : WH -> Set} ->
             [ HoleOr X -:> Tiling (HoleOr X) -:> Tiling (HoleOr X) ]
seeThrough hx thx = {!!}

-- Show that if X has a CutKit, then so has HoleOr X. Cutting up holes is
-- very easy as they don't put up much resistance.

holeCut : {X : WH -> Set} -> CutKit X -> CutKit (HoleOr X)
holeCut ck = record
  { cutH = {!!}
  ; cutV = {!!}
  }
  where open CutKit ck

-- Now, a rectangular layer is a tiling whose pieces are either holes or
-- blocks of coloured text.

Layer : WH -> Set
Layer = Tiling (HoleOr (Matrix Cell))

-- By making careful use of super and seeThrough, show how layers of a given
-- size have monoid structure, where the operation combines "front" and "back"
-- layers by making the back layer visible only through the holes in the front.

layerId : [ Layer ]
layerId = {!!}

layerOp : [ Layer -:> Layer -:> Layer ]
layerOp = super {!!} {!!}

-- I'd ask you to prove that the monoid laws hold (they do), but when I did it,
-- it was too much of a slog for too few ideas.

-- A typical display is made by superimposing a bunch of layers, but you might
-- still leave some holes, so we need to fill in a background. Use the MonadIx
-- structure of tilings to fill in each hole in a Layer with a matrix of black
-- (but who can tell?) spaces on a white background.

background : [ Layer -:> Tiling (Matrix Cell) ]
background = mapIx {!!}

---------------------------------------------------------------------------
-- CHANGES
---------------------------------------------------------------------------

-- Applications change what they display as you use them, of course. Often
-- they change a little at a time, so it's not necessary to repaint the
-- whole thing. Let's build tilings to represent just what changes.

data Change (wh : WH) : Set where
  new : Layer wh -> Change wh
  old : Change wh

-- The idea is that you make a top-level tiling to show which regions have
-- changed, and for the ones with new content, you give the layer which is
-- that content. So a Tiling Change tells you the difference between the
-- old layer and the new layer.

-- ??? 5.6 (1 mark) -- Conor: 0/1
-- You should be able to compute the changed layer given the change and the old
-- layer. Hint: This, also, is a job for super.

changed : [ Tiling Change -:> Layer -:> Layer ]
changed = super {!!} {!!}

---------------------------------------------------------------------------
-- UPDATA
---------------------------------------------------------------------------

-- ??? 5.7 (3 marks) -- Conor: 0/3
-- A notion related to "Change" is "Updata", but they're subtly different:
--   the actual content in a change is just the new stuff, and we've seen we
--     can grab any old parts from the old layer;
--   the Updata structure stores *all* the content, but each tile is tagged
--     with a bit which tells you if it comes from the change or was there
--     before.

record Updata (wh : WH) : Set where
  constructor _-:_
  field
    updated  : Two                      -- has it changed
    content  : HoleOr (Matrix Cell) wh  -- what is it, anyway?

-- Correspondingly, you should be able to generate a Tiling Updata
-- from a Tiling Change and the old Layer. Work in two stages. First,
-- make a thing that generates a Tiling Updata from a Layer by
-- applying the same tag to all tiles.

tagLayer : Two -> [ Layer -:> Tiling Updata ]
tagLayer u = {!!}

-- Now you should be able to generate a version of "changed" that adds tags.

updata : [ Tiling Change -:> Layer -:> Tiling Updata ]
updata = {!!}

-- Last but not least, develop the monoid operations for Updata. Here's where
-- you sort out the logic for displaying changing layers. Content-wise, it should
-- be a lot like the Layer monoid, in that you can see the back stuff through
-- the holes in the front stuff. But what about the "updated" tags? Is there a
-- difference between an "old" hole in the front and a "new" hole in the front?
-- You will need to build a CutKit in order to use super appropriately.

updataId : [ Tiling Updata ]
updataId = {!!}

updataCut : CutKit Updata
updataCut = {!!}

updataOp : [ Tiling Updata -:> Tiling Updata -:> Tiling Updata ]
updataOp = {!!}

---------------------------------------------------------------------------
-- NEXT TIME...
---------------------------------------------------------------------------

-- We'll develop a notion of "Application" which can each display
-- their Layer, and respond to events by delivering a Tiling
-- Change. We'll develop a notion of "Desktop" which amounts to a
-- front-to-back stack of applications. The Desktop display updates
-- by superimposing the Tiling Updata which comes from the change made
-- by each application in the stack.

-- Once we've got that setup, we can run applications by getting events
-- from the keyboard, generating the Tiling Updata for the whole Desktop,
-- then use cursor movement to skip the unchanged parts and just rewrite
-- the regions which need it. It'll actually go!


text:
-- Jesper, 2018-05-14: constructor patterns of the parent clause can
-- now be replaced by a variable in the with clause.

open import Common.Prelude

f : List Nat → List Nat
f [] = []
f (x ∷ xs) with Set
f xs | p = xs

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
private
  record Dummy : Set₁ where
    constructor ⟨_⟩
    field
      {h} : Set
      nh : Set

pattern ⟪_,_⟫ h s = ⟨_⟩ {h} s
pattern ⟪_⟫ h = (⟨_⟩ {h} _)


text:
{-# OPTIONS --without-K --exact-split --safe #-}

module Fragment.Extensions.CSemigroup.Nat where

open import Relation.Binary.PropositionalEquality as PE using (_≡_)

data ℕ⁺ : Set where
  one : ℕ⁺
  suc : ℕ⁺ → ℕ⁺

infixl 6 _+_

_+_ : ℕ⁺ → ℕ⁺ → ℕ⁺
one   + x = suc x
suc x + y = suc (x + y)

+-suc : ∀ x y → x + suc y ≡ suc (x + y)
+-suc one     y = PE.refl
+-suc (suc x) y = PE.cong suc (+-suc x y)

+-one : ∀ x → x + one ≡ suc x
+-one one     = PE.refl
+-one (suc x) = PE.cong suc (+-one x)

+-assoc : ∀ x y z → (x + y) + z ≡ x + (y + z)
+-assoc one     _ _ = PE.refl
+-assoc (suc x) y z = PE.cong suc (+-assoc x y z)

open PE.≡-Reasoning

+-comm : ∀ x y → x + y ≡ y + x
+-comm one one     = PE.refl
+-comm one (suc y) = begin
    one + (suc y) ≡⟨⟩
    suc (suc y)   ≡⟨ PE.sym (PE.cong suc (+-one y)) ⟩
    suc (y + one) ≡⟨ PE.sym PE.refl ⟩
    suc y + one   ∎
+-comm (suc x) y = begin
    suc x + y     ≡⟨⟩
    suc (x + y)   ≡⟨ PE.cong suc (+-comm x y) ⟩
    suc (y + x)   ≡⟨ PE.sym (+-suc y x) ⟩
    y + suc x     ∎

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
open import Agda.Builtin.Float
open import Agda.Builtin.Unit
open import Agda.Builtin.Reflection
open import Agda.Builtin.String
open import Agda.Builtin.Bool
open import Common.IO

data It (a : Float) : Set where
  it : It a

Inf : Float
Inf = primFloatDiv 1.0 0.0

-Inf : Float
-Inf = primFloatNegate Inf

NaN : Float
NaN = primFloatDiv 0.0 0.0

-NaN : Float
-NaN = primFloatNegate NaN

_==_ = primFloatEquality

macro
  literal : Float → Term → TC ⊤
  literal x hole = unify hole (lit (float x))

nl = putStrLn ""

header = putStrLn " Inf  -Inf   NaN  -NaN  |  x"

tick : Bool → String
tick true  = "   x  "
tick false = "   -  "

check : Float → IO _
check x = putStr (tick (x ==  Inf)) ,,
          putStr (tick (x == -Inf)) ,,
          putStr (tick (x ==  NaN)) ,,
          putStr (tick (x == -NaN)) ,,
          putStr "|  " ,, printFloat x ,,
          nl

main : IO _
main =
  header ,,
  check (literal  Inf) ,,
  check (literal -Inf) ,,
  check (literal  NaN) ,,
  check (literal -NaN)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K --exact-split --rewriting #-}

open import lib.Basics
open import lib.PathGroupoid
open import lib.types.Bool
open import lib.types.Sigma
open import lib.types.Pi
open import lib.types.Coproduct
open import lib.types.Unit
open import lib.types.Empty
open import lib.NConnected
open import lib.NType
open import lib.NType2
open import lib.Equivalence
open import lib.types.Truncation

open import Util.Misc

open import Graphs.Definition
open import Graphs.Properties

open import Coequalizers.Definition
open import Coequalizers.EdgeCoproduct
open import Coequalizers.PreserveEquivalence
open import Coequalizers.TrivialExtension

{- Contains a useful lemma about extending subtrees used in the construction of spanning trees. -}
module Graphs.SubTrees where

{- We fix a graph E ⇉ V together with a family of types P over the vertex set. -}
module _ {i j k : ULevel} (E : Type i) (V : Type j) ⦃ gph : Graph E V ⦄
  (P : V → Type k) where
  private
    ijk' = lmax i (lmax j k)

  {- A crossing edge is an edge that has one end in P and one end outside P. -}
  record Crossingedge : Type ijk' where
    constructor
      crossingedge
    field
      edge : E
      dir : Bool
      end-in-P : P (Bool-rec (π₀ edge) (π₁ edge) dir)
      end-notin-P : ¬ (P (Bool-rec (π₁ edge) (π₀ edge) dir))

  {- If the graph is connected, P is decidable and we are given a vertex in P and a vertex outside P,
     then we can show there mereley exists an edge that crosses from P to ¬ P or vice versa. -}
  findedge : (dec : (v : V) → Dec (P v))  (u v : V) (uInP : P u) (vNotinP : ¬ (P v)) (p : c[ u ] == c[ v ] :> V / E) → ∥ Crossingedge ∥
  findedge dec u v uInP vNotinP p = equal-to-X c[ v ] p vNotinP
    where
      edgeequiv : (e : E) → ((¬ (P (π₀ e)) → ∥ Crossingedge ∥) ↔ (¬ (P (π₁ e)) → ∥ Crossingedge ∥))
      edgeequiv e =
        ⊔-rec
          (λ p0 → ⊔-rec
            (λ p1 → (λ _ f → ⊥-elim (f p1)) , λ _ f → ⊥-elim (f p0))
            (λ np1 → haveedge (crossingedge e true p0 np1))
            (dec (π₁ e)))
          (λ np0 → ⊔-rec
            (λ p1 → haveedge (crossingedge e false p1 np0))
            (λ np1 → (λ f _ → f np0) , λ f _ → f np1)
            (dec (π₁ e)))
          (dec ((π₀ e)))
          where
            haveedge : Crossingedge → ((¬ (P (π₀ e)) → ∥ Crossingedge ∥) ↔ (¬ (P (π₁ e)) → ∥ Crossingedge ∥))
            haveedge ce = (λ _ _ → [ ce ]) , λ _ _ → [ ce ]

      {- The key to the proof is to define a family of propositions X over the coequalizer of the graph.
         For this to be well defined we need the lemma edgeequiv above, together with
         propositional extensionality.
      -}
      X : V / E → Type (lmax j (lmax i k))
      X = Coeq-rec (λ v' → ¬ (P v') → ∥ Crossingedge ∥ ) (λ e → prop-extensionality (edgeequiv e))

      equal-to-X : (z : V / E) (p : c[ u ] == z) → X z
      equal-to-X .(c[ u ]) idp = λ nu → ⊥-elim (nu uInP)

module _ {i j k l : ULevel} (E : Type i) (V : Type j) ⦃ gph : Graph E V ⦄ where
  {- A subtree of E ⇉ V consists of a graph D ⇉ U such that U / D is contractible
     together with injection D ↪ E and decidable injection U ↪ V making the obvious squares commute. -}
  record SubTree (D : Type k) (U : Type l) : Type (lmax (lmax i j) (lmax k l)) where
    constructor subtree
    field
      ⦃ gphDU ⦄ : Graph D U
      inD : D → E
      inU : U → V
      D-inj : is-inj inD
      U-inj : is-inj inU
      U-dec : (v : V) → Dec (hfiber inU v)
      comm₀ : π₀ ∘ inD ∼ inU ∘ π₀
      comm₁ : π₁ ∘ inD ∼ inU ∘ π₁
      ⦃ DUistree ⦄ : is-tree gphDU

  {- If we are given subtree D ⇉ U and a vertex in V ∖ U, then we can extend the
     subtree to a slightly larger one that contains one new vertex.
  -}
  extend-subtree : {D : Type k} {U : Type l} ⦃ conn : gph-is-connected gph ⦄ (decV : has-dec-eq V)  → (t : SubTree D U) → (v : V) → ¬ (hfiber (SubTree.inU t) v) →
                   ∥ SubTree (⊤ ⊔ D) (U ⊔ ⊤) ∥
  extend-subtree {D} {U} decV record { gphDU = gphDU ; inD = inD ; inU = inU ; D-inj = D-inj ; U-inj = U-inj ; comm₀ = comm₀ ; comm₁ = comm₁ ; U-dec = U-dec} v f =
    do -- we use do notation to help deal with iterated recursion on propositional truncation (see the definion of >>= in Util/Misc.agda)
      u ← (Coeq-rec [_] (λ e → prop-has-all-paths _ _) (contr-center (⟨⟩ :> is-tree gphDU)))
      p ← (conn-to-path c[ inU u ] c[ v ])
      ce ← (findedge E V (hfiber inU) U-dec (inU u) v (u , idp) f p)
      [ from-ce ce ]
    where
      from-ce : Crossingedge E V (λ v → (hfiber inU v)) → (SubTree (⊤ ⊔ D) (U ⊔ ⊤))
      from-ce (crossingedge edge true end-in-P end-notin-P) =
        record
          { inD = λ { (inl _) → edge ; (inr d) → inD d}
          ; inU = λ { (inl u) → inU u ; (inr _) → π₁ edge}
          ; D-inj = λ { (inl unit) →
                        λ { (inl unit) _ → idp ; (inr d) p → ⊥-elim (end-notin-P ((π₁ d) , ! (ap π₁ p ∙ comm₁ d)))}
                      ; (inr d) →
                        λ { (inl unit) p → ⊥-elim (end-notin-P ((π₁ d) , ! (comm₁ d) ∙ ap π₁ p)) ; (inr d') p → ap inr (D-inj _ _ p)}}
          ; U-inj = λ { (inl u) →
                        λ { (inl u') p → ap inl (U-inj _ _ p) ; (inr unit) p → ⊥-elim (end-notin-P (u , p))}
                      ; (inr unit) →
                        λ { (inl u) p → ⊥-elim (end-notin-P (u , (! p))) ; (inr unit) _ → idp}}
          ; U-dec = λ v → ⊔-rec (λ {(u , p) → inl ((inl u) , p)})
                                   (λ f → ⊔-rec (λ p → inl ((inr unit) , ! p))
                                                (λ g → inr (λ {(inl u , p) → f ((u , p)) ; (inr unit , p) → g (! p)}))
                                                (decV v (π₁ edge)))
                                   (U-dec v)
          ; comm₀ = λ { (inl x) → ! (snd end-in-P) ; (inr d) → comm₀ d}
          ; comm₁ = λ { (inl _) → idp ; (inr d) → comm₁ d}
          ; DUistree = equiv-preserves-level (extn-equiv ⁻¹)
          }
        where
          instance
            gphDU' : Graph (⊤ ⊔ D) (U ⊔ ⊤)
            gphDU' = record { π₀ = λ { (inl _) → inl (fst end-in-P) ; (inr x) → inl (π₀ x) }
                           ; π₁ = λ { (inl _) → inr unit ; (inr x) → inl (π₁ x) }}

            extn-equiv : (U ⊔ ⊤) / (⊤ ⊔ D) ≃ U / D
            extn-equiv =
              (U ⊔ ⊤) / (⊤ ⊔ D)
                ≃⟨ edge-coproduct-expand ⟩
              ((U ⊔ ⊤) / ⊤) / D
                ≃⟨ (Coeq-emap (TExtensionCoeq-l.extn-equiv (fst end-in-P)) (ide D) (λ _ → idp) λ _ → idp) ⁻¹ ⟩
              U / D
                ≃∎
              where
                open CoeqCoprodEquiv (U ⊔ ⊤) ⊤ D -- also defines instances for (U ⊔ ⊤) / ⊤) / D

      from-ce (crossingedge edge false end-in-P end-notin-P) =
        record
          { inD = λ { (inl _) → edge ; (inr d) → inD d}
          ; inU = λ { (inl u) → inU u ; (inr _) → π₀ edge}
          ; D-inj = λ { (inl unit) →
                        λ { (inl unit) _ → idp ; (inr d) p → ⊥-elim (end-notin-P ((π₀ d) , ! (ap π₀ p ∙ comm₀ d)))}
                      ; (inr d) →
                        λ { (inl unit) p → ⊥-elim (end-notin-P ((π₀ d) , ! (comm₀ d) ∙ ap π₀ p)) ; (inr d') p → ap inr (D-inj _ _ p)}}
          ; U-inj = λ { (inl u) →
                        λ { (inl u') p → ap inl (U-inj _ _ p) ; (inr unit) p → ⊥-elim (end-notin-P (u , p))}
                      ; (inr unit) →
                        λ { (inl u) p → ⊥-elim (end-notin-P (u , (! p))) ; (inr unit) _ → idp}}
          ; U-dec = λ v → ⊔-rec (λ {(u , p) → inl ((inl u) , p)})
                                   (λ f → ⊔-rec (λ p → inl ((inr unit) , ! p))
                                                (λ g → inr (λ {(inl u , p) → f ((u , p)) ; (inr unit , p) → g (! p)}))
                                                (decV v (π₀ edge)))
                                   (U-dec v)
          ; comm₀ = λ { (inl _) → idp ; (inr d) → comm₀ d}
          ; comm₁ = λ { (inl x) → ! (snd end-in-P) ; (inr d) → comm₁ d}
          ; DUistree = equiv-preserves-level (extn-equiv ⁻¹)
          }
          where
            instance
              gphDU' : Graph (⊤ ⊔ D) (U ⊔ ⊤)
              gphDU' = record { π₀ = λ { (inl _) →  inr unit ; (inr x) → inl (π₀ x) }
                             ; π₁ = λ { (inl _) → inl (fst end-in-P) ; (inr x) → inl (π₁ x) }}

              extn-equiv : (U ⊔ ⊤) / (⊤ ⊔ D) ≃ U / D
              extn-equiv =
                (U ⊔ ⊤) / (⊤ ⊔ D)
                  ≃⟨ edge-coproduct-expand ⟩
                ((U ⊔ ⊤) / ⊤) / D
                    ≃⟨ Coeq-emap (TExtensionCoeq-r.extn-equiv (fst end-in-P)) (ide D) (λ _ → idp) (λ _ → idp) ⁻¹ ⟩
                U / D
                  ≃∎
                where
                  open CoeqCoprodEquiv (U ⊔ ⊤) ⊤ D -- also defines instances for (U ⊔ ⊤) / ⊤) / D

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


text:
open import Categories
open import Monads
import Monads.CatofAdj
import Monads.CatofAdj.TermAdjObj

module Monads.CatofAdj.TermAdjUniq
  {a b}
  {C : Cat {a}{b}}
  (M : Monad C)
  (A : Monads.CatofAdj.ObjAdj M)
  (V : Monads.CatofAdj.HomAdj M A (Monads.CatofAdj.TermAdjObj.EMObj M))
  where

open import Library
open import Functors
open import Adjunctions
open Monads.CatofAdj M
open import Monads.EM M
open Monads.CatofAdj.TermAdjObj M
open import Monads.CatofAdj.TermAdjHom M A
open import Categories.Terminal
open Fun
open Adj
open ObjAdj
open Cat

omaplem : OMap (HomAdj.K EMHom ) ≅ OMap (HomAdj.K V)
omaplem = ext
  λ X → AlgEq (fcong X (cong OMap (HomAdj.Rlaw V)))
    ((ext λ Y →
        dext
        (λ {f} {f'} p →
           trans
           (trans
            (trans
             (stripsubst
               (λ Z → Hom C Z (OMap (R (adj A)) X))
               (HMap (R (adj A)) (right (adj A) f))
               (fcong Y (cong OMap (law A))))
             (cong' refl (cong
                            (λ (F : Obj (D A) → Obj C) →
                               λ (_ : Hom (D A) (OMap (L (adj A)) Y) X) →
                                 Hom C (F (OMap (L (adj A)) Y)) (F X))
                            (cong OMap (HomAdj.Rlaw V)))
                (icong' refl
                 (cong
                  (λ (F : Obj (D A) → Obj C) →
                     λ (z : Obj (D A)) →
                       Hom (D A) (OMap (L (adj A)) Y) z →
                       Hom C (F (OMap (L (adj A)) Y)) (F z))
                  (cong OMap (HomAdj.Rlaw V)))
                 (icong' refl
                  (cong
                   (λ (F : Obj (D A) → Obj C) →
                      λ (z : Obj (D A)) →
                        {Y₁ : Obj (D A)} → Hom (D A) z Y₁ → Hom C (F z) (F Y₁))
                   (cong OMap (HomAdj.Rlaw V)))
                  (cong HMap (HomAdj.Rlaw V)) (refl {x = OMap (L (adj A)) Y}))
                 (refl {x = X}))
                (refl {x = right (adj A) f})))
            (cong₃ (λ A₁ B → AlgMorph.amor  {A₁} {B})
             (fcong Y (cong OMap (HomAdj.Llaw V))) refl
             (HomAdj.rightlaw V {Y} {X} {f})))
           (cong (Alg.astr (OMap (HomAdj.K V) X) Y)
            (trans
             (stripsubst (Hom C Y) f (fcong X (cong OMap (HomAdj.Rlaw V))))
             p)))))

hmaplem : {X Y : Obj (D A)} (f : Hom (D A) X Y) →
          HMap (HomAdj.K EMHom) f ≅ HMap (HomAdj.K V) f
hmaplem {X}{Y} f = AlgMorphEq'
  (fcong X omaplem)
  (fcong Y omaplem)
  (cong'
    refl
    (cong
      (λ (F : Obj (D A) → Obj C) → λ (_ : Hom (D A) X Y) → Hom C (F X) (F Y))
      (cong OMap (HomAdj.Rlaw V)))
    (icong'
      refl
      (cong
        (λ (F : Obj (D A) → Obj C) → λ (z : Obj (D A)) →
           Hom (D A) X z → Hom C (F X) (F z))
        (cong OMap (HomAdj.Rlaw V)))
      (icong'
        refl
        (cong
          (λ (F : Obj (D A) → Obj C) → λ (z : Obj (D A)) → {Y₁ : Obj (D A)} →
             Hom (D A) z Y₁ → Hom C (F z) (F Y₁))
          (cong OMap (HomAdj.Rlaw V)))
        (cong HMap (HomAdj.Rlaw V))
        (refl {x = X}))
      (refl {x = Y}))
    (refl {x = f}))

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties about signs
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Sign.Properties where

open import Algebra
open import Data.Empty
open import Data.Sign
open import Data.Product using (_,_)
open import Function
open import Level using (0ℓ)
open import Relation.Binary.PropositionalEquality

open import Algebra.Structures {A = Sign} _≡_
open import Algebra.FunctionProperties {A = Sign} _≡_

-- The opposite of a sign is not equal to the sign.

s≢opposite[s] : ∀ s → s ≢ opposite s
s≢opposite[s] - ()
s≢opposite[s] + ()

opposite-injective : ∀ {s t} → opposite s ≡ opposite t → s ≡ t
opposite-injective { - } { - } refl = refl
opposite-injective { - } { + } ()
opposite-injective { + } { - } ()
opposite-injective { + } { + } refl = refl

------------------------------------------------------------------------
-- _*_

-- Algebraic properties of _*_

*-identityˡ : LeftIdentity + _*_
*-identityˡ _ = refl

*-identityʳ : RightIdentity + _*_
*-identityʳ - = refl
*-identityʳ + = refl

*-identity : Identity + _*_
*-identity = *-identityˡ  , *-identityʳ

*-comm : Commutative _*_
*-comm + + = refl
*-comm + - = refl
*-comm - + = refl
*-comm - - = refl

*-assoc : Associative _*_
*-assoc + + _ = refl
*-assoc + - _ = refl
*-assoc - + _ = refl
*-assoc - - + = refl
*-assoc - - - = refl

*-cancelʳ-≡ : RightCancellative _*_
*-cancelʳ-≡ - - _  = refl
*-cancelʳ-≡ - + eq = ⊥-elim (s≢opposite[s] _ $ sym eq)
*-cancelʳ-≡ + - eq = ⊥-elim (s≢opposite[s] _ eq)
*-cancelʳ-≡ + + _  = refl

*-cancelˡ-≡ : LeftCancellative _*_
*-cancelˡ-≡ - eq = opposite-injective eq
*-cancelˡ-≡ + eq = eq

*-cancel-≡ : Cancellative _*_
*-cancel-≡ = *-cancelˡ-≡ , *-cancelʳ-≡

*-isMagma : IsMagma _*_
*-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = cong₂ _*_
  }

*-magma : Magma 0ℓ 0ℓ
*-magma = record
  { isMagma = *-isMagma
  }

*-isSemigroup : IsSemigroup _*_
*-isSemigroup = record
  { isMagma = *-isMagma
  ; assoc   = *-assoc
  }

*-semigroup : Semigroup 0ℓ 0ℓ
*-semigroup = record
  { isSemigroup = *-isSemigroup
  }

*-isMonoid : IsMonoid _*_ +
*-isMonoid = record
  { isSemigroup = *-isSemigroup
  ; identity    = *-identity
  }

*-monoid : Monoid 0ℓ 0ℓ
*-monoid = record
  { isMonoid = *-isMonoid
  }

-- Other properties of _*_

s*s≡+ : ∀ s → s * s ≡ +
s*s≡+ + = refl
s*s≡+ - = refl

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

opposite-not-equal = s≢opposite[s]
{-# WARNING_ON_USAGE opposite-not-equal
"Warning: opposite-not-equal was deprecated in v0.15.
Please use s≢opposite[s] instead."
#-}
opposite-cong = opposite-injective
{-# WARNING_ON_USAGE opposite-cong
"Warning: opposite-cong was deprecated in v0.15.
Please use opposite-injective instead."
#-}
cancel-*-left = *-cancelˡ-≡
{-# WARNING_ON_USAGE cancel-*-left
"Warning: cancel-*-left was deprecated in v0.15.
Please use *-cancelˡ-≡ instead."
#-}
cancel-*-right = *-cancelʳ-≡
{-# WARNING_ON_USAGE cancel-*-right
"Warning: cancel-*-right was deprecated in v0.15.
Please use *-cancelʳ-≡ instead."
#-}
*-cancellative = *-cancel-≡
{-# WARNING_ON_USAGE *-cancellative
"Warning: *-cancellative was deprecated in v0.15.
Please use *-cancel-≡ instead."
#-}


text:
{-# OPTIONS --universe-polymorphism #-}

-- It's possible to compute levels
module ComputedLevels where

open import Common.Level

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

N-ary-level : Level → Level → ℕ → Level
N-ary-level ℓ₁ ℓ₂ zero    = ℓ₂
N-ary-level ℓ₁ ℓ₂ (suc n) = ℓ₁ ⊔ N-ary-level ℓ₁ ℓ₂ n

N-ary : ∀ {ℓ₁ ℓ₂} (n : ℕ) → Set ℓ₁ → Set ℓ₂ → Set (N-ary-level ℓ₁ ℓ₂ n)
N-ary zero    A B = B
N-ary (suc n) A B = A → N-ary n A B


text:
module Ex2 where

open import Ex1

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
module Examples.OpSem where

open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst)
open import Luau.Syntax using (var; nil; local_←_; _∙_; done; return)
open import Luau.Heap using (emp)

x = var "x"

ex1 : emp ⊢ (local "x" ← nil ∙ return x ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ emp
ex1 = subst

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


text:
-- Proof that consistent negative axioms do not jeopardize canonicity.
-- https://www.cs.bham.ac.uk/~mhe/papers/negative-axioms.pdf

{-# OPTIONS --without-K --safe #-}

module Application.NegativeAxioms.Canonicity where

open import Definition.Untyped as U

open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening as T
open import Definition.Typed.Consequences.Inequality
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.Substitution
open import Definition.Typed.Consequences.Syntactic

open import Definition.Conversion.Consequences.Completeness
open import Definition.Conversion.FullReduction

open import Tools.Empty
open import Tools.Fin
open import Tools.Nat
open import Tools.Product
open import Tools.Sum using (_⊎_; inj₁; inj₂)
open import Tools.Unit

-- Preliminaries
---------------------------------------------------------------------------

private
  Ty  = Term
  Cxt = Con Ty
  variable
    m m'  : Nat
    x     : Fin m
    ρ     : Wk m m'
    σ     : Subst m m'
    Γ Δ   : Con Term m
    A B C : Term m
    t u   : Term m

-- Numerals

data Numeral {m : Nat} : Term m → Set where
  zeroₙ : Numeral zero
  sucₙ  : Numeral t → Numeral (suc t)

-- Negative types
---------------------------------------------------------------------------

-- A type is negative if all of its branches end in ⊥.
-- The prime example is negation ¬A.

data NegativeType (Γ : Cxt m) : Ty m → Set where

  empty : NegativeType Γ Empty

  pi    : Γ ⊢ A
        → NegativeType (Γ ∙ A) B
        → NegativeType Γ (Π A ▹ B)

  sigma : Γ ⊢ A
        → NegativeType Γ A
        → NegativeType (Γ ∙ A) B
        → NegativeType Γ (Σ A ▹ B)

  conv  : NegativeType Γ A
        → Γ ⊢ A ≡ B
        → NegativeType Γ B

-- Lemma: Negative types are closed under weakening.

wkNeg : ρ ∷ Δ ⊆ Γ → ⊢ Δ → NegativeType Γ A → NegativeType Δ (U.wk ρ A)

wkNeg w ⊢Δ empty
  = empty

wkNeg w ⊢Δ (pi dA nB)
  = pi dA' (wkNeg (lift w) (⊢Δ ∙ dA') nB)
    where dA' = T.wk w ⊢Δ dA

wkNeg w ⊢Δ (sigma dA nA nB)
  = sigma dA' (wkNeg w ⊢Δ nA) (wkNeg (lift w) (⊢Δ ∙ dA') nB)
    where dA' = T.wk w ⊢Δ dA

wkNeg w ⊢Δ (conv n c)
  = conv (wkNeg w ⊢Δ n) (wkEq w ⊢Δ c)

-- Lemma: Negative types are closed under parallel substitution.

subNeg : NegativeType Γ A → Δ ⊢ˢ σ ∷ Γ → ⊢ Δ → NegativeType Δ (subst σ A)

subNeg empty _ _ = empty

subNeg (pi ⊢A n) s ⊢Δ
  = pi ⊢σA (subNeg n (liftSubst′ (wf ⊢A) ⊢Δ ⊢A s) (⊢Δ ∙ ⊢σA))
    where ⊢σA = substitution ⊢A s ⊢Δ

subNeg (sigma ⊢A nA nB) s ⊢Δ
  = sigma ⊢σA (subNeg nA s ⊢Δ) (subNeg nB (liftSubst′ (wf ⊢A) ⊢Δ ⊢A s) (⊢Δ ∙ ⊢σA))
    where ⊢σA = substitution ⊢A s ⊢Δ

subNeg (conv n c) s ⊢Δ = conv (subNeg n s ⊢Δ) (substitutionEq c (substRefl s) ⊢Δ)

-- Corollary: Negative types are closed under single substitution.

subNeg1 : NegativeType (Γ ∙ A) B → Γ ⊢ t ∷ A → NegativeType Γ (B [ t ])
subNeg1 n ⊢t = subNeg n (singleSubst ⊢t) (wfTerm ⊢t)

-- Lemma: The first component of a negative Σ-type is negative.

fstNeg : NegativeType Γ C → Γ ⊢ C ≡ Σ A ▹ B → NegativeType Γ A
fstNeg empty          c = ⊥-elim (Empty≢Σⱼ c)
fstNeg (pi _ _)       c = ⊥-elim (Π≢Σ c)
fstNeg (sigma _ nA _) c = conv nA (proj₁ (Σ-injectivity c))
fstNeg (conv n c)    c' = fstNeg n (trans c c')

-- Lemma: Any instance of the second component of a negative Σ-type is negative.

sndNeg : NegativeType Γ C → Γ ⊢ C ≡ Σ A ▹ B → Γ ⊢ t ∷ A → NegativeType Γ (B [ t ])
sndNeg empty          c = ⊥-elim (Empty≢Σⱼ c)
sndNeg (pi _ _)       c = ⊥-elim (Π≢Σ c)
sndNeg (sigma _ _ nB) c ⊢t = let (cA , cB) = Σ-injectivity c in
  subNeg (conv nB cB) (singleSubst (conv ⊢t (sym cA))) (wfTerm ⊢t)
sndNeg (conv n c)    c' = sndNeg n (trans c c')

-- Lemma: Any instance of the codomain of a negative Π-type is negative.

appNeg : NegativeType Γ C → Γ ⊢ C ≡ Π A ▹ B → Γ ⊢ t ∷ A → NegativeType Γ (B [ t ])
appNeg empty          c = ⊥-elim (Empty≢Πⱼ c)
appNeg (sigma _ _ _)  c = ⊥-elim (Π≢Σ (sym c))
appNeg (pi _ nB) c ⊢t = let (cA , cB) = injectivity c in
  subNeg (conv nB cB) (singleSubst (conv ⊢t (sym cA))) (wfTerm ⊢t)
appNeg (conv n c)    c' = appNeg n (trans c c')

-- Lemma: The type ℕ is not negative.

¬negℕ : NegativeType Γ C → Γ ⊢ C ≡ ℕ → ⊥
¬negℕ empty         c = ℕ≢Emptyⱼ (sym c)
¬negℕ (pi _ _)      c = ℕ≢Π (sym c)
¬negℕ (sigma _ _ _) c = ℕ≢Σ (sym c)
¬negℕ (conv n c)   c' = ¬negℕ n (trans c c')

-- Negative contexts
---------------------------------------------------------------------------

-- A context is negative if all of its type entries are negative.

data NegativeContext : Con Ty m → Set where
  ε   : NegativeContext ε
  _∙_ : NegativeContext Γ → NegativeType Γ A → NegativeContext (Γ ∙ A)

-- Lemma: Any entry in negative context is a negative type (needs weakening).

lookupNegative : ⊢ Γ → NegativeContext Γ → (x ∷ A ∈ Γ) → NegativeType Γ A
lookupNegative ⊢Γ∙A            (nΓ ∙ nA) here
  = wkNeg (step id) ⊢Γ∙A nA
lookupNegative ⊢Γ∙A@(⊢Γ ∙ Γ⊢A) (nΓ ∙ nA) (there h)
  = wkNeg (step id) ⊢Γ∙A (lookupNegative ⊢Γ nΓ h)

-- Main results
---------------------------------------------------------------------------

-- We assume a negative, consistent context.

module Main (nΓ : NegativeContext Γ) (consistent : ∀{t} → Γ ⊢ t ∷ Empty → ⊥) where

  -- Lemma: A neutral has negative type in a consistent negative context.

  neNeg : (d : Γ ⊢ u ∷ A) (n : NfNeutral u) → NegativeType Γ A
  neNeg (var ⊢Γ h       ) (var _           ) = lookupNegative ⊢Γ nΓ h
  neNeg (d ∘ⱼ ⊢t        ) (∘ₙ n _          ) = appNeg (neNeg d n) (refl (syntacticTerm d)) ⊢t
  neNeg (fstⱼ ⊢A A⊢B d  ) (fstₙ n          ) = fstNeg (neNeg d n) (refl (Σⱼ ⊢A ▹ A⊢B))
  neNeg (sndⱼ ⊢A A⊢B d  ) (sndₙ n          ) = sndNeg (neNeg d n) (refl (Σⱼ ⊢A ▹ A⊢B)) (fstⱼ ⊢A A⊢B d)
  neNeg (natrecⱼ _ _ _ d) (natrecₙ _ _ _ n ) = ⊥-elim (¬negℕ (neNeg d n) ⊢ℕ) where ⊢ℕ = refl (ℕⱼ (wfTerm d))
  neNeg (Emptyrecⱼ _ d  ) (Emptyrecₙ _ _   ) = ⊥-elim (consistent d)
  neNeg (conv d c       ) n                  = conv (neNeg d n) c

  -- Lemma: A normal form of type ℕ is a numeral in a consistent negative context.

  nfN : (d : Γ ⊢ u ∷ A)
      → (n : Nf u)
      → (c : Γ ⊢ A ≡ ℕ)
      → Numeral u

  -- Case: neutrals. The type cannot be ℕ since it must be negative.
  nfN d (ne n) c = ⊥-elim (¬negℕ (neNeg d n) c)

  -- Case: numerals.
  nfN (zeroⱼ x) zeroₙ   c = zeroₙ
  nfN (sucⱼ d) (sucₙ n) c = sucₙ (nfN d n c)

  -- Case: conversion.
  nfN (conv d c) n c' = nfN d n (trans c c')

  -- Impossible cases: type is not ℕ.

  -- * Canonical types
  nfN (Πⱼ _ ▹ _)      (Πₙ _ _)    c = ⊥-elim (U≢ℕ c)
  nfN (Σⱼ _ ▹ _)      (Σₙ _ _)    c = ⊥-elim (U≢ℕ c)
  nfN (ℕⱼ _)           ℕₙ         c = ⊥-elim (U≢ℕ c)
  nfN (Emptyⱼ _)       Emptyₙ     c = ⊥-elim (U≢ℕ c)
  nfN (Unitⱼ _)        Unitₙ      c = ⊥-elim (U≢ℕ c)

  -- * Canonical forms
  nfN (lamⱼ _ _)      (lamₙ _)    c = ⊥-elim (ℕ≢Π (sym c))
  nfN (prodⱼ _ _ _ _) (prodₙ _ _) c = ⊥-elim (ℕ≢Σ (sym c))
  nfN (starⱼ _)       starₙ       c = ⊥-elim (ℕ≢Unitⱼ (sym c))
  -- q.e.d

  -- Canonicity theorem: Any well-typed term Γ ⊢ t : ℕ is convertible to a numeral.

  thm : (⊢t : Γ ⊢ t ∷ ℕ) → ∃ λ u → Numeral u × Γ ⊢ t ≡ u ∷ ℕ

  thm ⊢t with fullRedTerm (completeEqTerm (refl ⊢t))
  ... | u , nf , eq = u , nfN (proj₂ (proj₂ (syntacticEqTerm eq))) nf (refl (ℕⱼ (wfTerm ⊢t))) , eq

-- Q.E.D. 2021-05-27

max_stars_repo_name: mr-ohman/logrel-ml

max_issues_repo_name: mr-ohman/logrel-ml

max_forks_repo_name: mr-ohman/logrel-ml


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Discrete where

open import Level
open import Data.Unit
open import Function
open import Relation.Binary.PropositionalEquality as ≡

open import Categories.Category
open import Categories.Functor

Discrete : ∀ {a} (A : Set a) → Category a a a
Discrete A = record
  { Obj       = A
  ; _⇒_       = _≡_
  ; _≈_       = _≡_
  ; id        = refl
  ; _∘_       = flip ≡.trans
  ; assoc     = λ {_ _ _ _ g} → sym (trans-assoc g)
  ; sym-assoc = λ {_ _ _ _ g} → trans-assoc g
  ; identityˡ = λ {_ _ f} → trans-reflʳ f
  ; identityʳ = refl
  ; identity² = refl
  ; equiv     = isEquivalence
  ; ∘-resp-≈  = λ where
    refl refl → refl
  }

module _ {a o ℓ e} {A : Set a} (C : Category o ℓ e) where
  open Category C renaming (id to one)

  module _ (f : A → Obj) where

    lift-func : Functor (Discrete A) C
    lift-func = record
      { F₀           = f
      ; F₁           = λ { refl → one }
      ; identity     = Equiv.refl
      ; homomorphism = λ { {_} {_} {_} {refl} {refl} → Equiv.sym identity² }
      ; F-resp-≈     = λ { {_} {_} {refl} refl → Equiv.refl }
      }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
{-# OPTIONS --without-K #-}
module Equivalence where

open import Homotopy
open import PathOperations
open import Types

infix  1 _≃_

qinv : ∀ {a b} {A : Set a} {B : Set b}
  (f : A → B) → Set _
qinv {A = A} {B = B} f =
  Σ (B → A) λ g → (f ∘ g ∼ id) × (g ∘ f ∼ id)

isequiv : ∀ {a b} {A : Set a} {B : Set b}
  (f : A → B) → Set _
isequiv {A = A} {B = B} f
  = (Σ (B → A) λ g → f ∘ g ∼ id)
  × (Σ (B → A) λ h → h ∘ f ∼ id)

_≃_ : ∀ {a b} (A : Set a) (B : Set b) → Set _
A ≃ B = Σ (A → B) isequiv

qi→eq : ∀ {a b} {A : Set a} {B : Set b}
  {f : A → B} → qinv f → isequiv f
qi→eq (g , p , q) = (g , p) , (g , q)

eq→qi : ∀ {a b} {A : Set a} {B : Set b}
  {f : A → B} → isequiv f → qinv f
eq→qi {f = f} ((g , p) , (h , q)) =
  g , p , λ _ → q _ ⁻¹ · ap h (p _) · q _

≡→eq : ∀ {ℓ} {A : Set ℓ} {B : Set ℓ} → A ≡ B → A ≃ B
≡→eq p
  = tr id p
  , (tr id (p ⁻¹) , λ b → J
      (λ _ B p → (b : B) → tr id p (tr id (p ⁻¹) b) ≡ b)
      (λ _ _ → refl)
      _ _ p b)
  , (tr id (p ⁻¹) , λ a → J
      (λ A _ p → (a : A) → tr id (p ⁻¹) (tr id p a) ≡ a)
      (λ _ _ → refl)
      _ _ p a)

refl-equiv : ∀ {a} {A : Set a} → A ≃ A
refl-equiv = id , (id , λ _ → refl) , (id , λ _ → refl)

sym-equiv : ∀ {a b} {A : Set a} {B : Set b} →
  A ≃ B → B ≃ A
sym-equiv (f , (g , p) , (h , q))
  = g
  , (f , λ _ → q _ ⁻¹ · ap h (p _) · q _)
  , (f , p)

trans-equiv : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
  A ≃ B → B ≃ C → A ≃ C
trans-equiv
  (f₁ , (g₁ , p₁) , (h₁ , q₁)) (f₂ , (g₂ , p₂) , (h₂ , q₂))
  =  f₂ ∘ f₁
  , (g₁ ∘ g₂ , λ _ → ap f₂ (p₁ _) · p₂ _)
  , (h₁ ∘ h₂ , λ _ → ap h₁ (q₂ _) · q₁ _)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
module RTN where

  data Nat : Set where
    zero : Nat
    suc  : Nat -> Nat

  {-# BUILTIN NATURAL Nat #-}
  {-# BUILTIN SUC suc #-}
  {-# BUILTIN ZERO zero #-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --without-K #-}

open import Data.Nat
open import Data.List using (List ; [] ; _∷_ ; length) renaming (_++_ to _++L_ )
open import Data.Vec  using (Vec ; [] ; _∷_ ) renaming (_++_ to _++V_ )
open import Data.Fin hiding (_+_ ; _≤_ )
open import Data.Product
open import Data.Maybe

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Algebra
open import Level renaming (zero to lzero ; suc to lsuc)

open import Function using () renaming (case_of_ to CASE_OF_)

data Multiplicity : Set where
  one   : Multiplicity
  omega : Multiplicity

-- Multiplicities with 0.
-- This is a deviation from the papers. Having 0 is convenient for handling uses of variables.
data Multiplicity₀ : Set where
  zero  : Multiplicity₀
  one   : Multiplicity₀
  omega : Multiplicity₀

-- Embedding
M→M₀ : Multiplicity -> Multiplicity₀
M→M₀ one   = one
M→M₀ omega = omega

-- Instead of having constructors, we have (additive) sums and
-- (multiplicative) products, together with iso-recursive types. The
-- type constructor Many can be used for representing non-linear
-- constructors.
data Ty : ℕ -> Set where
  _⊕_    : ∀ {n} -> Ty n -> Ty n -> Ty n
  tunit  : ∀ {n} -> Ty n
  _⊗_   : ∀ {n} -> Ty n -> Ty n -> Ty n
  Many   : ∀ {n} -> Multiplicity -> Ty n -> Ty n
  _#_~>_ : ∀ {n} -> Ty n -> Multiplicity -> Ty n -> Ty n
  _●     : ∀ {n} -> Ty n -> Ty n
  μ_    : ∀ {n} -> Ty (suc n) -> Ty n
  tvar   : ∀ {n} -> Fin n -> Ty n
  _↔_    : ∀ {n} -> Ty n -> Ty n -> Ty n

_⊸_ : ∀ {n} -> Ty n -> Ty n -> Ty n
t ⊸ t' = t # one ~> t'

infixr 4 _⊗_
infixr 1 _⊕_
infixr 0 _#_~>_
infixr 0 _⊸_

tbool : Ty zero
tbool = tunit ⊕ tunit

module _ where
  -- Several properties to handle recursive types.
  open import Data.Nat.Properties
  private
    lemma : ∀ {m n} -> m ≤ n -> ∃[ k ] (k + m ≡ n)
    lemma {n = n} z≤n = n , +-identityʳ n
    lemma (s≤s r) with lemma r
    ... | k , refl = k , +-suc k _

    weakenVarK : ∀ {m n k} -> k + m ≡ n -> Fin m -> Fin (k + m)
    weakenVarK {k = zero} refl  x = x
    weakenVarK {n = suc n} {suc k} eq x = suc (weakenVarK {n = n} {k = k} (suc-injective eq) x)

  weakenVar : ∀ {m n} -> m ≤ n -> Fin m -> Fin n
  weakenVar r x with lemma r
  ... | k , r' = subst Fin r' (weakenVarK r' x)

  substTyVar : ∀ {m n k} -> m + n ≤ k -> Fin (m + suc n) -> Ty k -> Ty k
  substTyVar {zero} r zero t = t
  substTyVar {zero} r (suc x) t = tvar (weakenVar r x)
  substTyVar {suc m} {k = suc k} r zero t = tvar zero
  substTyVar {suc m} (s≤s r) (suc x) t = substTyVar {m} (≤-trans r (≤-step ≤-refl)) x t

  weaken : ∀ {m n} -> m ≤ n -> Ty m -> Ty n
  weaken r (t ⊕ t₁) = weaken r t ⊕ weaken r t₁
  weaken r tunit =  tunit
  weaken r (t ⊗ t₁) = weaken r t ⊗ weaken r t₁
  weaken r (Many x t) = Many x (weaken r t)
  weaken r (t # x ~> t₁) = weaken r t # x ~> weaken r t₁
  weaken r (t ●) = weaken r t ●
  weaken r (μ t) = μ (weaken (s≤s r) t)
  weaken r (tvar x) = tvar (weakenVar r x)
  weaken r (t₁ ↔ t₂) = weaken r t₁ ↔ weaken r t₂

  substTyGen : ∀ {m n} -> Ty (m + suc n) -> Ty (m + n) -> Ty (m + n)
  substTyGen (s₁ ⊕ s₂) t = substTyGen s₁ t ⊕ substTyGen s₂ t
  substTyGen tunit t = tunit
  substTyGen (s₁ ⊗ s₂) t = substTyGen s₁ t ⊗ substTyGen s₂ t
  substTyGen (Many x s) t = Many x (substTyGen s t)
  substTyGen (s # x ~> s₁) t = substTyGen s t # x ~> substTyGen s₁ t
  substTyGen (s ●) t = (substTyGen s t) ●
  substTyGen {m} (μ s) t = μ (substTyGen {m = suc m} s (weaken (n≤1+n _) t))
  substTyGen (tvar x) t = substTyVar ≤-refl x t
  substTyGen (s₁ ↔ s₂) t = substTyGen s₁ t ↔ substTyGen s₂ t

  substTy : ∀ {n} -> Ty (suc n) -> Ty n -> Ty n
  substTy = substTyGen {zero}

module TyExamples where
  nat : ∀ {n} -> Ty n
  nat = μ (tunit ⊕ tvar zero)

  natlist : ∀ {n} -> Ty n
  natlist = μ (tunit ⊕ (nat ⊗ tvar zero))

-- Instead of using environments that maps variables to pairs of types
-- and multiplicities, we use two sort of environments: one maps
-- variables to types and the other maps variables to multiplicities.
--
-- We will use de Bruijn indices for variables, and thus type
-- environments are represented as a list of types. The treatment of
-- multiplicity environment is similar but we assume that it has the
-- same length with the corresponding type environment; so we use Vec
-- for multiplicity environments.

TyEnv : Set
TyEnv = List (Ty zero)

MultEnv : ∀ ℕ -> Set
MultEnv n = Vec Multiplicity₀ n

-----------------------------------------------------------------------------
-- Operations and properties for multiplicities

mul : Multiplicity -> Multiplicity -> Multiplicity
mul one   y = y
mul omega y = omega

mul₀ : Multiplicity₀ -> Multiplicity₀ -> Multiplicity₀
mul₀ zero y = zero
mul₀ one y = y
mul₀ omega zero = zero
mul₀ omega one = omega
mul₀ omega omega = omega

mul₀-m-zero : ∀ m -> mul₀ m zero ≡ zero
mul₀-m-zero zero = refl
mul₀-m-zero one = refl
mul₀-m-zero omega = refl

_×ₘ_ : ∀{n} -> Multiplicity -> MultEnv n -> MultEnv n
m ×ₘ Γ = Data.Vec.map (mul₀ (M→M₀ m)) Γ

add₀ : Multiplicity₀ -> Multiplicity₀ -> Multiplicity₀
add₀ zero m = m
add₀ one zero  = one
add₀ one one   = omega
add₀ one omega = omega
add₀ omega _   = omega

add₀-m-zero : ∀ m -> add₀ m zero ≡ m
add₀-m-zero zero = refl
add₀-m-zero one = refl
add₀-m-zero omega = refl

add₀-comm : ∀ x y -> add₀ x y ≡ add₀ y x
add₀-comm zero zero = refl
add₀-comm zero one = refl
add₀-comm zero omega = refl
add₀-comm one zero = refl
add₀-comm one one = refl
add₀-comm one omega = refl
add₀-comm omega zero = refl
add₀-comm omega one = refl
add₀-comm omega omega = refl

add₀-assoc : ∀ x y z -> add₀ (add₀ x y) z ≡ add₀ x (add₀ y z)
add₀-assoc zero y z = refl
add₀-assoc one zero z = refl
add₀-assoc one one zero = refl
add₀-assoc one one one = refl
add₀-assoc one one omega = refl
add₀-assoc one omega z = refl
add₀-assoc omega y z = refl

mul₀-dist-add₀ : ∀ x y z -> mul₀ x (add₀ y z) ≡ add₀ (mul₀ x y) (mul₀ x z)
mul₀-dist-add₀ zero y z = refl
mul₀-dist-add₀ one y z = refl
mul₀-dist-add₀ omega zero z = refl
mul₀-dist-add₀ omega one zero = refl
mul₀-dist-add₀ omega one one = refl
mul₀-dist-add₀ omega one omega = refl
mul₀-dist-add₀ omega omega z = refl

-----------------------------------------------------------------------------
-- Operations and properties for multiplicity environments

infixr 7 _×ₘ_
infixl 6 _+ₘ_

_+ₘ_ : ∀ {n} -> MultEnv n -> MultEnv n -> MultEnv n
[] +ₘ [] = []
(m₁ ∷ Δ₁) +ₘ (m₂ ∷ Δ₂) = add₀ m₁ m₂ ∷ (Δ₁ +ₘ Δ₂)

+ₘ-comm : ∀ {n} -> ∀ (Δ₁ Δ₂ : MultEnv n) -> Δ₁ +ₘ Δ₂ ≡ Δ₂ +ₘ Δ₁
+ₘ-comm [] [] = refl
+ₘ-comm (x₁ ∷ Δ₁) (x₂ ∷ Δ₂) =
  begin
    add₀ x₁ x₂ ∷ Δ₁ +ₘ Δ₂
    ≡⟨ cong (_∷ Δ₁ +ₘ Δ₂) (add₀-comm x₁ x₂) ⟩
    add₀ x₂ x₁ ∷ Δ₁ +ₘ Δ₂
    ≡⟨ cong (add₀ x₂ x₁ ∷_) (+ₘ-comm Δ₁ Δ₂) ⟩
    add₀ x₂ x₁ ∷ Δ₂ +ₘ Δ₁
  ∎

+ₘ-assoc : ∀ {n} -> ∀ (Δ₁ Δ₂ Δ₃ : MultEnv n) ->
           (Δ₁ +ₘ Δ₂) +ₘ Δ₃ ≡ Δ₁ +ₘ (Δ₂ +ₘ Δ₃)
+ₘ-assoc [] [] [] = refl
+ₘ-assoc (x₁ ∷ Δ₁) (x₂ ∷ Δ₂) (x₃ ∷ Δ₃) =
  begin
   add₀ (add₀ x₁ x₂) x₃ ∷ Δ₁ +ₘ Δ₂ +ₘ Δ₃
   ≡⟨ cong₂ (_∷_) (add₀-assoc x₁ x₂ _) (+ₘ-assoc Δ₁ Δ₂ _) ⟩
   add₀ x₁ (add₀ x₂ x₃) ∷ Δ₁ +ₘ (Δ₂ +ₘ Δ₃)
  ∎

-- The multiplicity environment that maps all variables into 0.
∅ : ∀ {n} -> MultEnv n
∅ = Data.Vec.replicate zero

∅-lid : ∀ {n} (Δ : MultEnv n) -> ∅ +ₘ Δ ≡ Δ
∅-lid [] = refl
∅-lid (x ∷ Δ) = cong (x ∷_) (∅-lid Δ)

∅-rid : ∀ {n} (Δ : MultEnv n) -> Δ +ₘ ∅ ≡ Δ
∅-rid [] = refl
∅-rid (x ∷ Δ) = cong₂ (_∷_) (add₀-m-zero x) (∅-rid Δ)

+ₘ-commutativeMonoid : ∀ (n : ℕ) -> CommutativeMonoid 0ℓ 0ℓ
+ₘ-commutativeMonoid n = record
                           { Carrier = MultEnv n
                           ; _≈_ = _≡_
                           ; _∙_ = _+ₘ_
                           ; ε = ∅
                           ; isCommutativeMonoid = record { isMonoid = +ₘ-isMonoid ; comm = +ₘ-comm }
                             -- record {
                             -- isSemigroup = record { isMagma = record { isEquivalence =  Relation.Binary.PropositionalEquality.isEquivalence  ;
                             --                                           ∙-cong = cong₂ (_+ₘ_) } ;
                             --                        assoc = +ₘ-assoc } ;
                             -- ; identityˡ = ∅-lid
                             -- ; comm = +ₘ-comm }
                           }
  where
    +ₘ-isMonoid : IsMonoid _≡_ _+ₘ_ ∅
    +ₘ-isMonoid = record { isSemigroup = record { isMagma = record { isEquivalence = Relation.Binary.PropositionalEquality.isEquivalence ; ∙-cong = cong₂ (_+ₘ_) } ; assoc = +ₘ-assoc } ; identity = ∅-lid , ∅-rid }

+ₘ-transpose :
  ∀ {n} (Δ₁ Δ₂ Δ₃ Δ₄ : MultEnv n) ->
  ((Δ₁ +ₘ Δ₂) +ₘ (Δ₃ +ₘ Δ₄)) ≡ ((Δ₁ +ₘ Δ₃) +ₘ (Δ₂ +ₘ Δ₄))
+ₘ-transpose Δ₁ Δ₂ Δ₃ Δ₄ =
  begin
    (Δ₁ +ₘ Δ₂) +ₘ (Δ₃ +ₘ Δ₄)
  ≡⟨ +ₘ-assoc Δ₁ Δ₂ _ ⟩
    Δ₁ +ₘ (Δ₂ +ₘ (Δ₃ +ₘ Δ₄))
  ≡⟨ cong (Δ₁ +ₘ_) (+ₘ-comm Δ₂ _) ⟩
    (Δ₁ +ₘ ((Δ₃ +ₘ Δ₄) +ₘ Δ₂))
  ≡⟨ cong (Δ₁ +ₘ_) (+ₘ-assoc Δ₃ Δ₄ _) ⟩
    (Δ₁ +ₘ (Δ₃ +ₘ (Δ₄ +ₘ Δ₂)))
  ≡⟨ cong (Δ₁ +ₘ_) (cong (Δ₃ +ₘ_) (+ₘ-comm Δ₄ _)) ⟩
    (Δ₁ +ₘ (Δ₃ +ₘ (Δ₂ +ₘ Δ₄)))
  ≡⟨ sym (+ₘ-assoc Δ₁ Δ₃ _) ⟩
    ((Δ₁ +ₘ Δ₃) +ₘ (Δ₂ +ₘ Δ₄))
  ∎

one×ₘ : ∀ {n} (Δ : MultEnv n) -> one ×ₘ Δ ≡ Δ
one×ₘ [] = refl
one×ₘ (x ∷ Δ) = cong (_∷_ x) (one×ₘ Δ)

×ₘ∅ : ∀ {n} m -> m ×ₘ ∅ {n} ≡ ∅ {n}
×ₘ∅ {zero} m = refl
×ₘ∅ {suc n} one   = cong (_∷_ zero) (×ₘ∅ one)
×ₘ∅ {suc n} omega = cong (_∷_ zero) (×ₘ∅ omega)

omega×ₘm×ₘ-omega×ₘ : ∀ {n} (m : Multiplicity) (Δ : MultEnv n) -> omega ×ₘ m ×ₘ Δ ≡ omega ×ₘ Δ
omega×ₘm×ₘ-omega×ₘ {zero}   m [] = refl
omega×ₘm×ₘ-omega×ₘ {suc n} m (zero ∷ Δ) rewrite mul₀-m-zero (M→M₀ m) = cong (zero ∷_) (omega×ₘm×ₘ-omega×ₘ {n} m Δ)
omega×ₘm×ₘ-omega×ₘ {suc n} one (one ∷ Δ)   = cong (omega ∷_) (omega×ₘm×ₘ-omega×ₘ {n} one Δ)
omega×ₘm×ₘ-omega×ₘ {suc n} omega (one ∷ Δ) = cong (omega ∷_) (omega×ₘm×ₘ-omega×ₘ {n} omega Δ)
omega×ₘm×ₘ-omega×ₘ {suc n} one (omega ∷ Δ) = cong (omega ∷_) (omega×ₘm×ₘ-omega×ₘ {n} one Δ)
omega×ₘm×ₘ-omega×ₘ {suc n} omega (omega ∷ Δ) = cong (omega ∷_) (omega×ₘm×ₘ-omega×ₘ {n} omega Δ)

mul-×ₘ : ∀ {n} m₁ m₂ (Δ : MultEnv n)  -> mul m₁ m₂ ×ₘ Δ ≡ m₁ ×ₘ (m₂ ×ₘ Δ)
mul-×ₘ one m₂ Δ = sym (one×ₘ _)
mul-×ₘ omega m₂ Δ = sym (omega×ₘm×ₘ-omega×ₘ m₂ Δ)

module _ where
  open import Data.Vec.Properties

  omega×ₘ∅-inv : ∀ {n} (Δ : MultEnv n) -> omega ×ₘ Δ ≡ ∅ -> Δ ≡ ∅
  omega×ₘ∅-inv [] eq = refl
  omega×ₘ∅-inv (x ∷ Δ) eq with  ∷-injective eq
  omega×ₘ∅-inv (zero ∷ Δ) eq | eq₁ , eq₂ = cong (zero ∷_) (omega×ₘ∅-inv Δ eq₂)

  add₀-0-0-inv : ∀ x y -> add₀ x y ≡ zero -> x ≡ zero × y ≡ zero
  add₀-0-0-inv zero zero eq = refl , refl
  add₀-0-0-inv one zero ()
  add₀-0-0-inv one one ()
  add₀-0-0-inv one omega ()

  ∅+ₘ∅-inv : ∀ {n} (Δ₁ Δ₂ : MultEnv n) -> Δ₁ +ₘ Δ₂ ≡ ∅ -> Δ₁ ≡ ∅ × Δ₂ ≡ ∅
  ∅+ₘ∅-inv [] [] eq = refl , refl
  ∅+ₘ∅-inv (x₁ ∷ Δ₁) (x₂ ∷ Δ₂) eq with ∷-injective eq
  ... | eq₁ , eq₂ with add₀-0-0-inv x₁ x₂ eq₁ | ∅+ₘ∅-inv Δ₁ Δ₂ eq₂
  ... | refl , refl | refl , refl = refl , refl

×ₘ-dist : ∀ {n} m (Δ₁ Δ₂ : MultEnv n) ->
          (m ×ₘ (Δ₁ +ₘ Δ₂)) ≡ (m ×ₘ Δ₁) +ₘ (m ×ₘ Δ₂)
×ₘ-dist m [] [] = refl
×ₘ-dist m (x₁ ∷ Δ₁) (x₂ ∷ Δ₂) =
  cong₂ (_∷_) (mul₀-dist-add₀ (M→M₀ m) x₁ x₂) (×ₘ-dist m Δ₁ Δ₂)

×ₘ-split : ∀ {n} m (Δ : MultEnv n)  -> ∃[ Δ' ] (m ×ₘ Δ ≡ Δ +ₘ Δ' )
×ₘ-split m [] = [] , refl
×ₘ-split m (x ∷ Δ) with ×ₘ-split m Δ
×ₘ-split one (x ∷ Δ) | Δ' , eq = zero ∷ Δ' , cong₂ (_∷_) (sym (add₀-m-zero x)) eq
×ₘ-split omega (zero ∷ Δ) | Δ' , eq = zero ∷ Δ' , cong (_∷_ zero) eq
×ₘ-split omega (one ∷ Δ) | Δ' , eq = one ∷ Δ' , cong (_∷_ omega) eq
×ₘ-split omega (omega ∷ Δ) | Δ' , eq = one ∷ Δ' , cong (_∷_ omega) eq

-----------------------------------------------------------------------------
-- Constraints on multiplicity environments

open import Data.Vec.Relation.Unary.All

-- all-zero Δ essentially asserts that Δ is ∅
all-zero : ∀ {n} -> Vec Multiplicity₀ n -> Set
all-zero = All (λ x -> x ≡ zero)

all-zero-∅ : ∀ {n} -> all-zero {n} ∅
all-zero-∅ {zero}  = []
all-zero-∅ {suc n} = refl ∷ all-zero-∅ {n}

all-zero-∅-inv : ∀ {n} -> (Δ : MultEnv n) -> all-zero {n} Δ -> Δ ≡ ∅
all-zero-∅-inv .[] [] = refl
all-zero-∅-inv .(zero ∷ _) (refl ∷ az) = cong (_∷_ zero) (all-zero-∅-inv _ az)

data no-omega : (m : Multiplicity₀) -> Set where
  zero : no-omega zero
  one  : no-omega one

no-omega-dist : ∀ x y -> no-omega (add₀ x y) -> no-omega x × no-omega y
no-omega-dist zero y noω   = zero , noω
no-omega-dist one zero noω = one , zero

-- all-no-omega Δ asserts that Δ(x) cannot be omega.
all-no-omega : ∀ {n} -> Vec Multiplicity₀ n -> Set
all-no-omega = All no-omega

-- Several properties of all-no-omega.

all-no-omega-∅ : ∀ {n} -> all-no-omega (∅ {n})
all-no-omega-∅ {zero}  = []
all-no-omega-∅ {suc n} = zero ∷ all-no-omega-∅

all-no-omega-dist : ∀ {n} (Δ₁ Δ₂ : MultEnv n) -> all-no-omega (Δ₁ +ₘ Δ₂) ->
                    all-no-omega Δ₁ × all-no-omega Δ₂
all-no-omega-dist [] [] ano = [] , []
all-no-omega-dist (x₁ ∷ Δ₁) (x₂ ∷ Δ₂) (noω ∷ ano)
  with no-omega-dist x₁ x₂ noω | all-no-omega-dist Δ₁ Δ₂ ano
... | no₁ , no₂ | ano₁ , ano₂ = no₁ ∷ ano₁ , no₂ ∷ ano₂

all-no-omega-dist-×ₘ :
  ∀ {n} m (Δ : MultEnv n) ->
  all-no-omega (m ×ₘ Δ) -> all-no-omega Δ
all-no-omega-dist-×ₘ m [] ano = []
all-no-omega-dist-×ₘ one (x ∷ Δ) (px ∷ ano) = px ∷ (all-no-omega-dist-×ₘ one Δ ano)
all-no-omega-dist-×ₘ omega (zero ∷ Δ) (px ∷ ano) = zero ∷ all-no-omega-dist-×ₘ omega Δ ano

all-no-omega-weaken-right :
  ∀ {n} {Δ₁ Δ₂ : MultEnv n} {m} ->
  all-no-omega (Δ₁ +ₘ m ×ₘ Δ₂) -> all-no-omega (Δ₁ +ₘ Δ₂)
all-no-omega-weaken-right {Δ₁ = Δ₁} {Δ₂} {m} ano with ×ₘ-split m Δ₂
... | Δ' , eq with all-no-omega-dist (Δ₁ +ₘ Δ₂) Δ' (subst all-no-omega lemma ano)
  where
    lemma : Δ₁ +ₘ m ×ₘ Δ₂ ≡ Δ₁ +ₘ Δ₂ +ₘ Δ'
    lemma = begin
              Δ₁ +ₘ m ×ₘ Δ₂
            ≡⟨ cong (Δ₁ +ₘ_) eq ⟩
              Δ₁ +ₘ (Δ₂ +ₘ Δ')
            ≡⟨ sym (+ₘ-assoc Δ₁ Δ₂ _) ⟩
             Δ₁ +ₘ Δ₂ +ₘ Δ'
            ∎
... | ano₁ , _ = ano₁

all-no-omega-omega×ₘ : ∀ {n} (Δ : MultEnv n) -> all-no-omega (omega ×ₘ Δ) -> Δ ≡ ∅
all-no-omega-omega×ₘ [] ano = refl
all-no-omega-omega×ₘ (zero ∷ Δ) (px ∷ ano) = cong (_∷_ zero) (all-no-omega-omega×ₘ Δ ano)

-----------------------------------------------------------------------------

-- Variables, or de Bruijn indices
data _∋_ : ∀ TyEnv  -> Ty zero -> Set where
  vz : ∀ {Γ : TyEnv} {a : Ty zero} -> (a ∷ Γ) ∋ a
  vs : ∀ {Γ : TyEnv} {a b : Ty zero} -> Γ ∋ a -> (b ∷ Γ) ∋ a

-- 'discardable' means that a corresponding variable need not be used.
data discardable : Multiplicity₀ -> Set where
  omega : discardable omega
  zero  : discardable zero

omega×ₘ-discardable : ∀ {n} (Δ : MultEnv n) ->  All discardable (omega ×ₘ Δ)
omega×ₘ-discardable [] = []
omega×ₘ-discardable (zero ∷ Δ)  = zero ∷ omega×ₘ-discardable Δ
omega×ₘ-discardable (one ∷ Δ)   = omega ∷ omega×ₘ-discardable Δ
omega×ₘ-discardable (omega ∷ Δ) = omega ∷ omega×ₘ-discardable Δ

-- 'usable' means that a corresponding variable can be used.
data usable : Multiplicity₀ -> Set where
  omega : usable omega
  one   : usable one

-- varOk means that the use of variable x in Γ is compatible with Δ; that is,
-- x is usable in Δ and other variables must be discardable in Δ.
data varOk : (Γ : TyEnv) {a : Ty zero} -> Γ ∋ a -> (Δ : MultEnv (length Γ)) -> Set where
  there :
    ∀ {Γ : TyEnv} {m a b} {x : Γ ∋ a} {Δ} ->
    (d : discardable m) ->
    (ok : varOk Γ x Δ) ->
    varOk (b ∷ Γ) (vs x) (m  ∷ Δ)
  here    :
    ∀ {Γ : TyEnv} {a} {Δ} {m} ->
      (u : usable m) ->
      (ad : All discardable Δ) ->
      varOk (a ∷ Γ) vz (m ∷ Δ)

-- varOk● is similar to varOk but is for invertible variables. The definition is simplified as
-- we assume Ξ cannot contain omega.
data varOk● : (Θ : TyEnv) {a : Ty zero} -> Θ ∋ a -> (Ξ : MultEnv (length Θ)) -> Set where
  there :
    ∀ {Θ : TyEnv} {a b} {x : Θ ∋ a} {Ξ} ->
    (ok : varOk● Θ x Ξ) ->
    varOk● (b ∷ Θ) (vs x) (zero ∷ Ξ)

  here :
    ∀ {Θ : TyEnv} {a} {Ξ} ->
    (ad : all-zero Ξ) ->
    varOk● (a ∷ Θ) vz (one ∷ Ξ)

-- Now, we are ready to define the intrinsically-typed syntax of Sparcl.
data Term : ∀ (Γ : TyEnv) -> MultEnv (length Γ) -> (Θ : TyEnv) -> MultEnv (length Θ) -> Ty zero -> Set where
  var  :
    ∀ {Γ Δ Θ A} ->
    (x : Γ ∋ A) -> (ok : varOk Γ x Δ) ->
    Term Γ Δ Θ ∅ A

  abs  :
    ∀ {Γ Δ Θ Ξ A B} -> (m : Multiplicity) ->
    Term (A ∷ Γ) (M→M₀ m ∷ Δ) Θ Ξ B ->
    Term Γ Δ Θ Ξ (A # m ~> B)

  app :
    ∀ {Γ Δ₁ Δ₂ Θ Ξ₁ Ξ₂ A B m} ->
    Term Γ Δ₁ Θ Ξ₁ (A # m ~> B) ->
    Term Γ Δ₂ Θ Ξ₂ A ->
    Term Γ (Δ₁ +ₘ m ×ₘ Δ₂) Θ (Ξ₁ +ₘ m ×ₘ Ξ₂) B

  unit :
    ∀ {Γ Δ Θ} ->
    (ad : All discardable Δ) ->
    Term Γ Δ Θ ∅ tunit

  letunit :
    ∀ {Γ Δ₀ Δ Θ Ξ₀ Ξ A} ->
    (m : Multiplicity) ->
    Term Γ Δ₀ Θ Ξ₀ tunit ->
    Term Γ Δ  Θ Ξ  A ->
    Term Γ (m ×ₘ Δ₀ +ₘ Δ) Θ (m ×ₘ Ξ₀ +ₘ Ξ) A

  pair :
    ∀ {Γ Δ₁ Δ₂ Θ Ξ₁ Ξ₂ A B} ->
    Term Γ Δ₁ Θ Ξ₁ A ->
    Term Γ Δ₂ Θ Ξ₂ B ->
    Term Γ (Δ₁ +ₘ Δ₂) Θ (Ξ₁ +ₘ Ξ₂) (A ⊗ B)

  letpair :
    ∀ {Γ Δ₀ Δ Θ Ξ₀ Ξ A B C} ->
    (m : Multiplicity) ->
    Term Γ Δ₀ Θ Ξ₀ (A ⊗ B) ->
    Term (A ∷ B ∷ Γ) (M→M₀ m ∷ M→M₀ m ∷ Δ) Θ Ξ C ->
    Term Γ (m ×ₘ Δ₀ +ₘ Δ) Θ (m ×ₘ Ξ₀ +ₘ Ξ) C

  many :
    ∀ {Γ Δ Θ Ξ A} ->
    (m : Multiplicity) ->
    Term Γ Δ Θ Ξ A ->
    Term Γ (m ×ₘ Δ) Θ (m ×ₘ Ξ) (Many m A)

  unmany :
    ∀ {Γ Δ₀ Δ Θ Ξ₀ Ξ m₀ A B} ->
    (m : Multiplicity) ->
    Term Γ Δ₀ Θ Ξ₀ (Many m₀ A) ->
    Term (A ∷ Γ) (M→M₀ (mul m m₀) ∷ Δ) Θ Ξ B ->
    Term Γ (m ×ₘ Δ₀ +ₘ Δ) Θ (m ×ₘ Ξ₀ +ₘ Ξ) B

  inl  :
    ∀ {Γ Δ Θ Ξ} {A B} ->
    Term Γ Δ Θ Ξ A ->
    Term Γ Δ Θ Ξ (A ⊕ B)

  inr :
    ∀ {Γ Δ Θ Ξ} {A B} ->
    Term Γ Δ Θ Ξ B ->
    Term Γ Δ Θ Ξ (A ⊕ B)

  case :
    ∀ {Γ Δ₀ Δ Θ Ξ₀ Ξ A B C} ->
    (m : Multiplicity) ->
    Term Γ Δ₀ Θ Ξ₀ (A ⊕ B) ->
    Term (A ∷ Γ) (M→M₀ m ∷ Δ) Θ Ξ C ->
    Term (B ∷ Γ) (M→M₀ m ∷ Δ) Θ Ξ C ->
    Term Γ (m ×ₘ Δ₀ +ₘ Δ) Θ (m ×ₘ Ξ₀ +ₘ Ξ) C

  roll :
    ∀ {Γ Δ Θ Ξ F} ->
    Term Γ Δ Θ Ξ (substTy F (μ F)) ->
    Term Γ Δ Θ Ξ (μ F)

  unroll :
    ∀ {Γ Δ Θ Ξ F} ->
    Term Γ Δ Θ Ξ (μ F) ->
    Term Γ Δ Θ Ξ (substTy F (μ F))

  unit● :
    ∀ {Γ Δ Θ} ->
    (ad : All discardable Δ) ->
    Term Γ Δ Θ ∅ (tunit ●)

  letunit● :
    ∀ {Γ Δ₀ Δ Θ Ξ₀ Ξ A} ->
    Term Γ Δ₀ Θ Ξ₀ (tunit ●) ->
    Term Γ Δ  Θ Ξ  (A ●) ->
    Term Γ (Δ₀ +ₘ Δ) Θ (Ξ₀ +ₘ Ξ) (A ●)

  pair● :
    ∀ {Γ Δ₁ Δ₂ Θ Ξ₁ Ξ₂ A B} ->
    Term Γ Δ₁ Θ Ξ₁ (A ●) ->
    Term Γ Δ₂ Θ Ξ₂ (B ●) ->
    Term Γ (Δ₁ +ₘ Δ₂) Θ (Ξ₁ +ₘ Ξ₂) ((A ⊗ B) ●)

  letpair● :
    ∀ {Γ Δ₀ Δ Θ Ξ₀ Ξ A B C} ->
    Term Γ Δ₀ Θ Ξ₀ ((A ⊗ B) ●) ->
    Term Γ Δ  (A ∷ B ∷ Θ) (one ∷ one ∷ Ξ) (C ●) ->
    Term Γ (Δ₀ +ₘ Δ) Θ (Ξ₀ +ₘ Ξ) (C ●)

  inl● :
    ∀ {Γ Δ Θ Ξ} {A B} ->
    Term Γ Δ Θ Ξ (A ●) ->
    Term Γ Δ Θ Ξ ((A ⊕ B) ●)

  inr● :
    ∀ {Γ Δ Θ Ξ} {A B} ->
    Term Γ Δ Θ Ξ (B ●) ->
    Term Γ Δ Θ Ξ ((A ⊕ B) ●)

  case● :
    ∀ {Γ Δ₀ Δ Δ' Θ Ξ₀ Ξ Ξ' A B C} ->
    Term Γ Δ₀ Θ Ξ₀ ((A ⊕ B) ●) ->
    Term Γ Δ  (A ∷ Θ) (one ∷ Ξ) (C ●) ->
    Term Γ Δ  (B ∷ Θ) (one ∷ Ξ) (C ●) ->
    Term Γ Δ' Θ Ξ' (C # omega ~> tbool) ->
    Term Γ (Δ₀ +ₘ Δ +ₘ omega ×ₘ Δ') Θ (Ξ₀ +ₘ Ξ +ₘ omega ×ₘ Ξ') (C ●)

  var● : ∀ {Γ Δ Θ Ξ A} ->
         (x : Θ ∋ A) ->
         (ad : All discardable Δ) -> varOk● Θ x Ξ ->
         Term Γ Δ Θ Ξ (A ●)

  pin : ∀ {Γ Δ₁ Δ₂ Θ Ξ₁ Ξ₂ A B} ->
        Term Γ Δ₁ Θ Ξ₁ (A ●) ->
        Term Γ Δ₂ Θ Ξ₂ (A # omega ~> B ●)  ->
        Term Γ (Δ₁ +ₘ Δ₂) Θ (Ξ₁ +ₘ Ξ₂) ((A ⊗ B) ●)

  unlift :
    ∀ {Γ Δ Θ Ξ A B}
    -> Term Γ Δ Θ Ξ (A ● ⊸ B ●)
    -> Term Γ (omega ×ₘ Δ) Θ (omega ×ₘ Ξ) (A ↔ B)

  fapp :
    ∀ {Γ Δ₁ Δ₂ Θ Ξ₁ Ξ₂ A B}
    -> Term Γ Δ₁ Θ Ξ₁ (A ↔ B)
    -> Term Γ Δ₂ Θ Ξ₂ A
    -> Term Γ (Δ₁ +ₘ omega ×ₘ Δ₂) Θ (Ξ₁ +ₘ omega ×ₘ Ξ₂) B

  bapp :
    ∀ {Γ Δ₁ Δ₂ Θ Ξ₁ Ξ₂ A B}
    -> Term Γ Δ₁ Θ Ξ₁ (A ↔ B)
    -> Term Γ Δ₂ Θ Ξ₂ B
    -> Term Γ (Δ₁ +ₘ omega ×ₘ Δ₂) Θ (Ξ₁ +ₘ omega ×ₘ Ξ₂) A

-- fwd and bwd are obtained as derived constructs.
fwd :
  ∀ {Γ Δ₁ Δ₂ Θ Ξ₁ Ξ₂ A B} ->
  Term Γ Δ₁ Θ Ξ₁ (A ● ⊸ B ●) ->
  Term Γ Δ₂ Θ Ξ₂ A ->
  Term Γ (omega ×ₘ Δ₁ +ₘ omega ×ₘ Δ₂) Θ (omega ×ₘ Ξ₁ +ₘ omega ×ₘ Ξ₂) B
fwd e1 e2 = fapp (unlift e1) e2

bwd :
  ∀ {Γ Δ₁ Δ₂ Θ Ξ₁ Ξ₂ A B} ->
  Term Γ Δ₁ Θ Ξ₁ (A ● ⊸ B ●) ->
  Term Γ Δ₂ Θ Ξ₂ B ->
  Term Γ (omega ×ₘ Δ₁ +ₘ omega ×ₘ Δ₂) Θ (omega ×ₘ Ξ₁ +ₘ omega ×ₘ Ξ₂) A
bwd e1 e2 = bapp (unlift e1) e2

-- compatΘ Θ Ξ Θ' Ξ' asserts that environments ((Θ , Ξ) and
-- (Θ' , Ξ')) differ only in variables with multiplicity zero. That
-- is, (Θ , Ξ) and (Θ' , Ξ') denote the same environement in
-- paper's representation.

data compatΘ : (Θ : TyEnv)  (Ξ : MultEnv (length Θ))
                (Θ' : TyEnv) (Ξ' : MultEnv (length Θ')) -> Set where
  compat-[] :
    compatΘ [] [] [] []

  compat-ext-here :
    ∀ {Θ Ξ Θ' Ξ' A} ->
    compatΘ Θ Ξ Θ' Ξ' ->
    compatΘ Θ Ξ (A ∷ Θ') (zero ∷ Ξ')

  compat-reduce-here :
    ∀ {Θ Ξ Θ' Ξ' A} ->
    compatΘ Θ Ξ Θ' Ξ' ->
    compatΘ (A ∷ Θ) (zero ∷ Ξ) Θ' Ξ'

  compat-skip :
    ∀ {Θ Ξ Θ' Ξ' A m } ->
    compatΘ Θ Ξ Θ' Ξ' ->
    compatΘ (A ∷ Θ) (m ∷ Ξ) (A ∷ Θ') (m ∷ Ξ')

-- Some useful examples of compatΘ

ext-id : ∀ {Θ Ξ} ->  compatΘ Θ Ξ Θ Ξ
ext-id {[]} {[]}         = compat-[]
ext-id {_ ∷ Θ} {_ ∷ Ξ} = compat-skip (ext-id {Θ} {Ξ})

smashΘ : ∀ {Θ} -> compatΘ Θ ∅ [] ∅
smashΘ {[]} = compat-[]
smashΘ {_ ∷ Θ} = compat-reduce-here smashΘ

extendΘ : ∀ {Θ} -> compatΘ [] ∅ Θ ∅
extendΘ {[]} = compat-[]
extendΘ {_ ∷ Θ} = compat-ext-here extendΘ

adjust∅Θ : ∀ {Θ Θ'} -> compatΘ Θ ∅ Θ' ∅
adjust∅Θ {[]} = extendΘ
adjust∅Θ {_ ∷ Θ} = compat-reduce-here adjust∅Θ

-- Some properties on compatΘ

compatΘ-∅ : ∀ {Θ Θ' Ξ'} -> compatΘ Θ ∅ Θ' Ξ' -> Ξ' ≡ ∅
compatΘ-∅ compat-[] = refl
compatΘ-∅ (compat-reduce-here ext) = compatΘ-∅ ext
compatΘ-∅ (compat-ext-here  ext) = cong (_∷_ zero) (compatΘ-∅ ext)
compatΘ-∅ (compat-skip ext) = cong (_∷_ zero) (compatΘ-∅ ext)

compatΘ-split :
  ∀ {Θ Ξ₁ Ξ₂ Θ' Ξ'} ->
  compatΘ Θ (Ξ₁ +ₘ Ξ₂) Θ' Ξ' ->
    ∃ λ (Ξ₁' : MultEnv (length Θ')) -> ∃ λ (Ξ₂' : MultEnv (length Θ')) ->
      compatΘ Θ Ξ₁ Θ' Ξ₁' × compatΘ Θ Ξ₂ Θ' Ξ₂' × Ξ₁' +ₘ Ξ₂' ≡ Ξ'
compatΘ-split {[]} {[]} {[]} {.[]} {.[]} compat-[] = ∅ , ∅ , compat-[] , compat-[] , refl
compatΘ-split {[]} {[]} {[]} {.(_ ∷ _)} {.(zero ∷ _)} (compat-ext-here ext)
  with compatΘ-split ext
... | Ξ₁' ,  Ξ₂' , ext₁ , ext₂ , refl =
   zero ∷ Ξ₁' , zero ∷ Ξ₂' , compat-ext-here ext₁ , compat-ext-here ext₂ , refl
compatΘ-split {x ∷ Θ} {zero ∷ Ξ₁} {.zero ∷ Ξ₂} {[]} {[]} (compat-reduce-here ext)
  with compatΘ-split ext
... | [] ,  [] , ext₁ , ext₂ , eq  =
  [] , [] , compat-reduce-here ext₁ , compat-reduce-here ext₂ , refl
compatΘ-split {x ∷ Θ} {one ∷ Ξ₁} {zero ∷ Ξ₂} {[]} {[]} ()
compatΘ-split {x ∷ Θ} {one ∷ Ξ₁} {one ∷ Ξ₂} {[]} {[]} ()
compatΘ-split {x ∷ Θ} {one ∷ Ξ₁} {omega ∷ Ξ₂} {[]} {[]} ()

compatΘ-split {x ∷ Θ} {zero ∷ Ξ₁} {x₂ ∷ Ξ₂} {x₃ ∷ Θ'} {.zero ∷ Ξ'} (compat-ext-here ext)
  with compatΘ-split {x ∷ Θ} {zero ∷ Ξ₁} {x₂ ∷ Ξ₂}  ext
... | Ξ₁' ,  Ξ₂' , ext₁ , ext₂ , refl =
   zero ∷ Ξ₁' , zero ∷ Ξ₂' , compat-ext-here ext₁ , compat-ext-here ext₂ , refl
compatΘ-split {x ∷ Θ} {zero ∷ Ξ₁} {.zero ∷ Ξ₂} {x₃ ∷ Θ'} {x₄ ∷ Ξ'} (compat-reduce-here ext)
  with compatΘ-split ext
... | Ξ₁' ,  Ξ₂' , ext₁ , ext₂ , eq =
  Ξ₁' , Ξ₂' , compat-reduce-here ext₁ , compat-reduce-here ext₂ , eq
compatΘ-split {x ∷ Θ} {zero ∷ Ξ₁} {x₂ ∷ Ξ₂} {.x ∷ Θ'} {.x₂ ∷ Ξ'} (compat-skip ext)
  with compatΘ-split ext
... | Ξ₁' ,  Ξ₂' , ext₁ , ext₂ , refl =
  zero ∷ Ξ₁' , x₂ ∷ Ξ₂' , compat-skip ext₁ , compat-skip ext₂ , refl

compatΘ-split {x ∷ Θ} {one ∷ Ξ₁} {zero ∷ Ξ₂} {x₃ ∷ Θ'} {.zero ∷ Ξ'} (compat-ext-here ext)
  with compatΘ-split {x ∷ Θ} {one ∷ Ξ₁} {zero ∷ Ξ₂}  ext
... | Ξ₁' ,  Ξ₂' , ext₁ , ext₂ , refl =
   zero ∷ Ξ₁' , zero ∷ Ξ₂' , compat-ext-here ext₁ , compat-ext-here ext₂ , refl
compatΘ-split {x ∷ Θ} {one ∷ Ξ₁} {zero ∷ Ξ₂} {.x ∷ Θ'} {.one ∷ Ξ'} (compat-skip ext)
  with compatΘ-split ext
... | Ξ₁' ,  Ξ₂' , ext₁ , ext₂ , refl =
  one ∷ Ξ₁' , zero ∷ Ξ₂' , compat-skip ext₁ , compat-skip ext₂ , refl

compatΘ-split {x ∷ Θ} {one ∷ Ξ₁} {one ∷ Ξ₂} {x₃ ∷ Θ'} {.zero ∷ Ξ'} (compat-ext-here ext)
  with compatΘ-split {x ∷ Θ} {one ∷ Ξ₁} {one ∷ Ξ₂}  ext
... | Ξ₁' ,  Ξ₂' , ext₁ , ext₂ , refl =
   zero ∷ Ξ₁' , zero ∷ Ξ₂' , compat-ext-here ext₁ , compat-ext-here ext₂ , refl
compatΘ-split {x ∷ Θ} {one ∷ Ξ₁} {one ∷ Ξ₂} {.x ∷ Θ'} {.omega ∷ Ξ'} (compat-skip ext)
  with compatΘ-split ext
... | Ξ₁' ,  Ξ₂' , ext₁ , ext₂ , refl =
  one ∷ Ξ₁' , one ∷ Ξ₂' , compat-skip ext₁ , compat-skip ext₂ , refl

compatΘ-split {x ∷ Θ} {one ∷ Ξ₁} {omega ∷ Ξ₂} {x₃ ∷ Θ'} {.zero ∷ Ξ'} (compat-ext-here ext)
  with compatΘ-split {x ∷ Θ} {one ∷ Ξ₁} {omega ∷ Ξ₂}  ext
... | Ξ₁' ,  Ξ₂' , ext₁ , ext₂ , refl =
   zero ∷ Ξ₁' , zero ∷ Ξ₂' , compat-ext-here ext₁ , compat-ext-here ext₂ , refl
compatΘ-split {x ∷ Θ} {one ∷ Ξ₁} {omega ∷ Ξ₂} {.x ∷ Θ'} {.omega ∷ Ξ'} (compat-skip ext)
  with compatΘ-split ext
... | Ξ₁' ,  Ξ₂' , ext₁ , ext₂ , refl =
  one ∷ Ξ₁' , omega ∷ Ξ₂' , compat-skip ext₁ , compat-skip ext₂ , refl

compatΘ-split {x ∷ Θ} {omega ∷ Ξ₁} {x₂ ∷ Ξ₂} {x₃ ∷ Θ'} {.zero ∷ Ξ'} (compat-ext-here ext)
  with compatΘ-split {x ∷ Θ} {omega ∷ Ξ₁} {x₂ ∷ Ξ₂}  ext
... | Ξ₁' ,  Ξ₂' , ext₁ , ext₂ , refl =
   zero ∷ Ξ₁' , zero ∷ Ξ₂' , compat-ext-here ext₁ , compat-ext-here ext₂ , refl
compatΘ-split {x ∷ Θ} {omega ∷ Ξ₁} {x₂ ∷ Ξ₂} {.x ∷ Θ'} {.omega ∷ Ξ'} (compat-skip ext)
  with compatΘ-split ext
... | Ξ₁' ,  Ξ₂' , ext₁ , ext₂ , refl =
  omega ∷ Ξ₁' , x₂ ∷ Ξ₂' , compat-skip ext₁ , compat-skip ext₂ , refl

compatΘ-preserves-all-no-omega :
  ∀ {Θ Ξ Θ' Ξ'} ->
  compatΘ Θ Ξ Θ' Ξ' -> all-no-omega Ξ -> all-no-omega Ξ'
compatΘ-preserves-all-no-omega compat-[] ano = ano
compatΘ-preserves-all-no-omega (compat-ext-here ext) ano = zero ∷ compatΘ-preserves-all-no-omega ext ano
compatΘ-preserves-all-no-omega (compat-reduce-here ext) (px ∷ ano) = compatΘ-preserves-all-no-omega ext ano
compatΘ-preserves-all-no-omega (compat-skip ext) (px ∷ ano) = px ∷ compatΘ-preserves-all-no-omega ext ano

compatΘ-preserves-all-zero :
  ∀ {Θ Ξ Θ' Ξ'} ->
  compatΘ Θ Ξ Θ' Ξ' -> all-zero Ξ -> all-zero Ξ'
compatΘ-preserves-all-zero compat-[] az = az
compatΘ-preserves-all-zero (compat-ext-here ext) az = refl ∷ compatΘ-preserves-all-zero ext az
compatΘ-preserves-all-zero (compat-reduce-here ext) (px ∷ az) = compatΘ-preserves-all-zero ext az
compatΘ-preserves-all-zero (compat-skip ext) (px ∷ az) = px ∷ compatΘ-preserves-all-zero ext az

compatΘ-preserves-varOk● :
  ∀ {Θ Ξ Θ' Ξ' A} {x : Θ ∋ A} ->
  compatΘ Θ Ξ Θ' Ξ' -> varOk● Θ x Ξ -> ∃ λ (x' : Θ' ∋ A) -> varOk● Θ' x' Ξ'
compatΘ-preserves-varOk● (compat-ext-here ext) ok with compatΘ-preserves-varOk● ext ok
... | x' , ok'  =  vs x' , there ok'
compatΘ-preserves-varOk● (compat-reduce-here ext) (there ok) = compatΘ-preserves-varOk● ext ok
compatΘ-preserves-varOk● (compat-skip ext) (there ok) with compatΘ-preserves-varOk● ext ok
... | x' , ok' = vs x' , there ok'
compatΘ-preserves-varOk● (compat-skip ext) (here ad) = vz , here (compatΘ-preserves-all-zero ext ad)

compatΘ-×ₘ :
  ∀ {Θ m Ξ Θ' Ξ'} ->
  compatΘ Θ (m ×ₘ Ξ) Θ' Ξ' ->
   ∃ λ (Ξ'' : MultEnv (length Θ')) ->
     compatΘ Θ Ξ Θ' Ξ'' × m ×ₘ Ξ'' ≡ Ξ'
compatΘ-×ₘ {[]} {m} {[]} {.[]} {.[]} compat-[] = [] , compat-[] , refl
compatΘ-×ₘ {[]} {m} {[]} {.(_ ∷ _)} {.(zero ∷ _)} (compat-ext-here ext) with compatΘ-×ₘ {[]} {m} {[]} ext
... | Ξ' , ext' , refl = zero ∷ Ξ' , compat-ext-here ext' , cong (_∷ m ×ₘ Ξ') (mul₀-m-zero _)

compatΘ-×ₘ {_ ∷ Θ} {one} {.zero ∷ Ξ} {[]} {[]} (compat-reduce-here ext) with compatΘ-×ₘ ext
... | [] , ext' , eq = [] , compat-reduce-here ext' , refl
compatΘ-×ₘ {_ ∷ Θ} {omega} {zero ∷ Ξ} {[]} {[]} (compat-reduce-here ext) with compatΘ-×ₘ ext
... | [] , ext' , eq = [] , compat-reduce-here ext' , refl

compatΘ-×ₘ {_ ∷ Θ} {one} {n ∷ Ξ} {_ ∷ Θ'} {.zero ∷ Ξ'} (compat-ext-here ext)
  with compatΘ-×ₘ ext
... | Ξ'' , ext' , refl = zero ∷ Ξ'' , compat-ext-here ext' , refl
compatΘ-×ₘ {_ ∷ Θ} {one} {.zero ∷ Ξ} {_ ∷ Θ'} {n' ∷ Ξ'} (compat-reduce-here ext)
  with compatΘ-×ₘ ext
... | Ξ'' , ext' , eq = Ξ'' , compat-reduce-here ext' , eq
compatΘ-×ₘ {_ ∷ Θ} {one} {n ∷ Ξ} {_ ∷ Θ'} {.n ∷ Ξ'} (compat-skip ext)
  with compatΘ-×ₘ ext
... | Ξ'' , ext' , refl = n ∷ Ξ'' , compat-skip ext' , refl

compatΘ-×ₘ {_ ∷ Θ} {omega} {zero ∷ Ξ} {_ ∷ Θ'} {.zero ∷ Ξ'} (compat-ext-here ext)
  with compatΘ-×ₘ {m = omega} {zero ∷ Ξ} ext
... | Ξ'' , ext' , refl = zero ∷ Ξ'' , compat-ext-here ext' , refl
compatΘ-×ₘ {_ ∷ Θ} {omega} {zero ∷ Ξ} {_ ∷ Θ'} {n' ∷ Ξ'} (compat-reduce-here ext)
  with compatΘ-×ₘ ext
... | Ξ'' , ext' , eq = Ξ'' , compat-reduce-here ext' , eq
compatΘ-×ₘ {_ ∷ Θ} {omega} {zero ∷ Ξ} {_ ∷ Θ'} {.zero ∷ Ξ'} (compat-skip ext)
  with compatΘ-×ₘ ext
... | Ξ'' , ext' , refl = zero ∷ Ξ'' , compat-skip ext' , refl

compatΘ-×ₘ {_ ∷ Θ} {omega} {one ∷ Ξ} {_ ∷ Θ'} {.zero ∷ Ξ'} (compat-ext-here ext)
  with compatΘ-×ₘ {m = omega} {one ∷ Ξ} ext
... | Ξ'' , ext' , refl = zero ∷ Ξ'' , compat-ext-here ext' , refl
compatΘ-×ₘ {_ ∷ Θ} {omega} {one ∷ Ξ} {_ ∷ Θ'} {.omega ∷ Ξ'} (compat-skip ext)
  with compatΘ-×ₘ ext
... | Ξ'' , ext' , refl = one ∷ Ξ'' , compat-skip ext' , refl

compatΘ-×ₘ {_ ∷ Θ} {omega} {omega ∷ Ξ} {_ ∷ Θ'} {.zero ∷ Ξ'} (compat-ext-here ext)
  with compatΘ-×ₘ {m = omega} {omega ∷ Ξ} ext
... | Ξ'' , ext' , refl = zero ∷ Ξ'' , compat-ext-here ext' , refl
compatΘ-×ₘ {_ ∷ Θ} {omega} {omega ∷ Ξ} {_ ∷ Θ'} {.omega ∷ Ξ'} (compat-skip ext)
  with compatΘ-×ₘ ext
... | Ξ'' , ext' , refl = omega ∷ Ξ'' , compat-skip ext' , refl

-- Well-typed terms can also be typed compatible environments.Due to a
-- historical reason, this property is called weakenΘ-term as
-- compatΘ was initially used only for adding variables with
-- multiplicity zero.

weakenΘ-term : ∀ {Γ Δ Θ Ξ Θ' Ξ' A} ->
                  compatΘ Θ Ξ Θ' Ξ' ->
                  Term Γ Δ Θ  Ξ A ->
                  Term Γ Δ Θ' Ξ' A
weakenΘ-term ext (var x ok) with compatΘ-∅ ext
... | refl = var x ok
weakenΘ-term ext (abs m t) = abs m (weakenΘ-term ext t)
weakenΘ-term ext (app t₁ t₂) with compatΘ-split ext
... | Ξ₁' , Ξ₂' , ext₁ , ext₂ , refl with compatΘ-×ₘ ext₂
... | Ξ₂'' , ext₂' , refl = app (weakenΘ-term ext₁ t₁) (weakenΘ-term ext₂' t₂)
weakenΘ-term ext (unit ad) with compatΘ-∅ ext
... | refl = unit ad
weakenΘ-term ext (letunit m t₁ t₂) with compatΘ-split ext
... | Ξ₁'  , Ξ₂' , ext₁ , ext₂ , refl with compatΘ-×ₘ ext₁
... | Ξ₁'' , ext₁' , refl = letunit m (weakenΘ-term ext₁' t₁) (weakenΘ-term ext₂ t₂)
weakenΘ-term ext (pair t₁ t₂) with compatΘ-split ext
... | Ξ₁'  , Ξ₂' , ext₁ , ext₂ , refl = pair (weakenΘ-term ext₁ t₁) (weakenΘ-term ext₂ t₂)
weakenΘ-term ext (letpair m t₁ t₂) with compatΘ-split ext
... | Ξ₁'  , Ξ₂' , ext₁ , ext₂ , refl with compatΘ-×ₘ ext₁
... | Ξ₁'' , ext₁' , refl = letpair m (weakenΘ-term ext₁' t₁) (weakenΘ-term ext₂ t₂)

weakenΘ-term ext (many m t) with compatΘ-×ₘ ext
... | Ξ'' , ext' , refl = many m (weakenΘ-term ext' t)

weakenΘ-term ext (unmany m' t₁ t₂) with compatΘ-split ext
... | Ξ₁'  , Ξ₂' , ext₁ , ext₂ , refl with compatΘ-×ₘ ext₁
... | Ξ₁'' , ext₁' , refl = unmany m' (weakenΘ-term ext₁' t₁) (weakenΘ-term ext₂ t₂)

weakenΘ-term ext (inl t) = inl (weakenΘ-term ext t)
weakenΘ-term ext (inr t) = inr (weakenΘ-term ext t)
weakenΘ-term ext (case m t₀ t₁ t₂) with compatΘ-split ext
... | Ξ₁'  , Ξ₂' , ext₁ , ext₂ , refl with compatΘ-×ₘ ext₁
... | Ξ₁'' , ext₁' , refl = case m (weakenΘ-term ext₁' t₀) (weakenΘ-term ext₂ t₁) (weakenΘ-term ext₂ t₂)
weakenΘ-term ext (roll t)   = roll (weakenΘ-term ext t)
weakenΘ-term ext (unroll t) = unroll (weakenΘ-term ext t)
weakenΘ-term ext (unit● ad) with compatΘ-∅ ext
... | refl  = unit● ad
weakenΘ-term ext (letunit● t₁ t₂)
  with compatΘ-split ext
... | Ξ₁'  , Ξ₂' , ext₁ , ext₂ , refl = letunit● (weakenΘ-term ext₁ t₁) (weakenΘ-term ext₂ t₂)
weakenΘ-term ext (pair● t₁ t₂)
  with compatΘ-split ext
... | Ξ₁'  , Ξ₂' , ext₁ , ext₂ , refl = pair● (weakenΘ-term ext₁ t₁) (weakenΘ-term ext₂ t₂)
weakenΘ-term ext (letpair● t₁ t₂)
  with compatΘ-split ext
... | Ξ₁'  , Ξ₂' , ext₁ , ext₂ , refl = letpair● (weakenΘ-term ext₁ t₁) (weakenΘ-term (compat-skip (compat-skip ext₂)) t₂)
weakenΘ-term ext (inl● t) = inl● (weakenΘ-term ext t)
weakenΘ-term ext (inr● t) = inr● (weakenΘ-term ext t)
weakenΘ-term ext (case● t t₁ t₂ t₃)
  with compatΘ-split ext
... | _ , _ , ext₁₂ , ext₃ , refl with compatΘ-split ext₁₂
... | _ , _ , ext₁ , ext₂ , refl with compatΘ-×ₘ ext₃
... | _ , ext₃' , refl = case● (weakenΘ-term ext₁ t) (weakenΘ-term (compat-skip ext₂) t₁) (weakenΘ-term (compat-skip ext₂) t₂) (weakenΘ-term ext₃' t₃)
weakenΘ-term ext (var● x ad ok) with compatΘ-preserves-varOk● ext ok
... | x' , ok' = var● x' ad ok'
weakenΘ-term ext (pin t₁ t₂)
  with compatΘ-split ext
... | Ξ₁'  , Ξ₂' , ext₁ , ext₂ , refl = pin (weakenΘ-term ext₁ t₁) (weakenΘ-term ext₂ t₂)
weakenΘ-term ext (unlift t) =
  CASE compatΘ-×ₘ ext OF λ {
    (_ , ext' , refl) -> unlift (weakenΘ-term ext' t)
  }
weakenΘ-term ext (fapp t₁ t₂) =
  CASE compatΘ-split ext OF λ {
    (_ , _ , ext₁ , ext₂ , refl) -> CASE compatΘ-×ₘ ext₂ OF λ {
      (_ , ext₂' , refl) -> fapp (weakenΘ-term ext₁ t₁) (weakenΘ-term ext₂' t₂)
    }
  }
weakenΘ-term ext (bapp t₁ t₂) =
  CASE compatΘ-split ext OF λ {
    (_ , _ , ext₁ , ext₂ , refl) -> CASE compatΘ-×ₘ ext₂ OF λ {
      (_ , ext₂' , refl) -> bapp (weakenΘ-term ext₁ t₁) (weakenΘ-term ext₂' t₂)
    }
  }

max_stars_repo_name: kztk-m/sparcl-agda

max_issues_repo_name: kztk-m/sparcl-agda

max_forks_repo_name: kztk-m/sparcl-agda


text:
module GUIgeneric.GUIDefinitions where

open import GUIgeneric.Prelude

open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe)

open import Relation.Nullary

data _⊎Comp_ {a b} (A : Set a) (B : Set b) : Set (a ⊔Level b) where
  button : (x : A) → A ⊎Comp B
  txtbox : (y : B) → A ⊎Comp B

data Direction : Set where
  left right : Direction

data Comp : Set where
  frame atomicComp : Comp

SubCompsIndex : Comp → Set
SubCompsIndex frame = ⊤
SubCompsIndex atomicComp = ⊥

data isSubComp : (c c' : Comp) → Set where
 buttonFrame  :  isSubComp  atomicComp frame

subComp : (c : Comp){c' : Comp}
         (is : isSubComp c' c) → Comp
subComp  .frame  {cButton}  buttonFrame  =  cButton

createParameters : Comp → Set
createParameters atomicComp = String ⊎Comp String
createParameters _ = ⊤

data IsOptimized : Set where
  optimized notOptimzed : IsOptimized

data CompEls (c : Comp) :  Set where
 createC  :  createParameters c → CompEls c
 add      :  {c' : Comp}(c'c : isSubComp c' c)
             (e' : CompEls c')(e : CompEls c)(isOpt : IsOptimized)
            → CompEls c

data _<c_  : {c c' : Comp}(e : CompEls c)(e' : CompEls c') → Set where
  addsub : {c' c : Comp}(c'c : isSubComp c' c)
           (e' : CompEls c')
           (e : CompEls c)
           (isOpt : IsOptimized)
           → e' <c add c'c e' e isOpt

  addlift : {c' c : Comp}(c'c : isSubComp c' c)
           (e' : CompEls c')
           (e : CompEls c)
           (isOpt : IsOptimized)
           → e <c add c'c e' e isOpt

data _<c+_  : {c c' : Comp}(e : CompEls c)(e' : CompEls c') → Set where
  in1 : {c c' : Comp} (e : CompEls c)(e' : CompEls c')
        (ee' : e <c e') → e <c+ e'
  in2 : {c c' c'' : Comp} (e : CompEls c)(e' : CompEls c')(e'' : CompEls c'')
        (ee' : e <c e')(e'e'' : e' <c+ e'') → (e <c+ e'')

data _<=c+_ : {c c' : Comp}(e : CompEls c)(e' : CompEls c') → Set where

  in0= : {c : Comp} (e : CompEls c)
        →  e <=c+ e
  in2= : {c c' c'' : Comp} (e : CompEls c)(e' : CompEls c')
                               (e'' : CompEls c'')
        →  e <c e' → e' <=c+ e'' → e <=c+ e''

in1= : {c c' : Comp} (e : CompEls c)(e' : CompEls c')
        (ee' : e <c e') → e <=c+ e'
in1= e e' ee' = in2= e e' e' ee' (in0= e')

trans<=c+ : {c c' c'' : Comp} (e : CompEls c)(e' : CompEls c')
                                   (e'' : CompEls c'')
            (ee' : e <=c+ e')
            (e'e'' : e' <=c+ e'')
            → e <=c+ e''
trans<=c+ {c} {.c} {c''} e .e e'' (in0= .e) e'e'' = e'e''
trans<=c+ {c} {c'} {c''} e e' e'' (in2= .e e'₁ .e' ee'₁ e'₁e') e'e'' = in2= e e'₁ e'' ee'₁ (trans<=c+ e'₁ e' e'' e'₁e' e'e'')

--
--  DEC Equality
--
module _ where
  sameOptimized : IsOptimized → IsOptimized → Bool
  sameOptimized optimized optimized = true
  sameOptimized notOptimzed notOptimzed = true
  sameOptimized _ _ = false

  _≟CompBool_ : {c c' : Comp} → CompEls c → CompEls c' → Bool
  _≟CompBool_ {frame} {frame} (add c₁c₂ c₁ c₂ isOpt) (add c₃c₄ c₃ c₄ isOpt') =
    (c₁ ≟CompBool c₃) ∧ (c₂ ≟CompBool c₄) ∧ (sameOptimized isOpt isOpt')

  _≟CompBool_ {atomicComp} {atomicComp} (add {frame} () _ _ _)
  _≟CompBool_ {atomicComp} {atomicComp} (add {atomicComp} () _ _ _)

  _≟CompBool_ {frame} {frame} (createC tt) (createC tt) = true
  _≟CompBool_ {atomicComp} {atomicComp} (createC (button x)) (createC (button y)) = x ==Str y
  _≟CompBool_ {atomicComp} {atomicComp} (createC (txtbox x)) (createC (txtbox y)) = x ==Str y

  _≟CompBool_ {atomicComp} {atomicComp} (createC (button x)) (createC (txtbox y)) = false
  _≟CompBool_ {atomicComp} {atomicComp} (createC (txtbox x)) (createC (button y)) = false

  _≟CompBool_ {frame} {atomicComp} _ _ = false
  _≟CompBool_ {atomicComp} {frame} _ _ = false

  createC _ ≟CompBool add _ _ _ _ = false
  add _ _ _ _ ≟CompBool createC _ = false

  unused = Dec

{- add buttonFrame a c notOptimzed ≡ add buttonFrame b d notOptimzedadd buttonFrame a c notOptimzed ≡ add buttonFrame b d notOptimzed -}
  lemmaAddEqProj1 : ∀ {a} {c} {opt} {b} {d} {opt'} → add buttonFrame a c opt ≡ add buttonFrame b d opt' → a ≡ b
  lemmaAddEqProj1 refl = refl

  lemmaAddEqProj2 : ∀ {a} {c} {opt} {b} {d} {opt'} → add buttonFrame a c opt ≡ add buttonFrame b d opt' → c ≡ d
  lemmaAddEqProj2 refl = refl

  lemmaCreateCBtnEq : ∀ {s1} {s2} → ((createC (button s1))  ≡ (createC (button s2))) → (s1 ≡ s2)
  lemmaCreateCBtnEq refl = refl

  lemmaCreateCTxtbxEq : ∀ {s1} {s2} → ((createC (txtbox s1))  ≡ (createC (txtbox s2))) → (s1 ≡ s2)
  lemmaCreateCTxtbxEq refl = refl

  mutual
   _≟CompFr_ : Decidable {A = CompEls frame} _≡_
   createC tt ≟CompFr createC tt = Dec.yes refl
   createC tt ≟CompFr add  _ _ _ _ = Dec.no (λ ())
   add _ _ _ _ ≟CompFr createC _ = Dec.no (λ ())
   add _ _ _ optimized ≟CompFr add _ _ _ notOptimzed = Dec.no (λ ())
   add _ _ _ notOptimzed ≟CompFr add _ _ _ optimized =  Dec.no (λ ())

   add buttonFrame a c optimized ≟CompFr add buttonFrame b d optimized with (a ≟Comp b) | (c ≟Comp d)
   ... | Dec.yes p | Dec.yes q = yes (cong₂ (λ x y → add buttonFrame x y optimized ) p q)
   ... | Dec.yes p | Dec.no ¬p = no (λ addp → ¬p (lemmaAddEqProj2 addp))
   ... | Dec.no ¬p | _ = no ((λ addp → ¬p (lemmaAddEqProj1 addp)))

   add buttonFrame a c notOptimzed ≟CompFr add buttonFrame b d notOptimzed with (a ≟Comp b) | (c ≟Comp d)
   ... | yes p | yes q = yes (cong₂ (λ x y → add buttonFrame x y notOptimzed ) p q)
   ... | yes p | no ¬p = no (λ addp → ¬p (lemmaAddEqProj2 addp))
   ... | no ¬p | q = no ((λ addp → ¬p (lemmaAddEqProj1 addp)))

   _≟Comp_ : {c : Comp} → Decidable {A = CompEls c} _≡_

   _≟Comp_ (createC _) (add _ _ _ isOpt) = Dec.no (λ ())
   _≟Comp_ (add _ _ _ isOpt) (createC _) = Dec.no (λ ())

   _≟Comp_ {atomicComp} (add () a b isOpt) (add cd c d isOpt')

   _≟Comp_ {frame} (createC tt) (createC tt) = Dec.yes refl

   _≟Comp_ {atomicComp} (createC (button s1)) (createC (button s2)) with (s1 ≟Str s2)
   ... | Dec.yes p = Dec.yes (cong (createC ∘ button) p)
   ... | Dec.no q = Dec.no  (λ neq →   q  (lemmaCreateCBtnEq neq)  )

   _≟Comp_ {atomicComp} (createC (txtbox s1)) (createC (txtbox s2)) with (s1 ≟Str s2)
   ... | Dec.yes p = Dec.yes (cong (createC ∘ txtbox) p)
   ... | Dec.no q = Dec.no (λ neq →   q  (lemmaCreateCTxtbxEq neq)  )

   _≟Comp_ {atomicComp} (createC (button s1)) (createC (txtbox s2)) = Dec.no (λ ())
   _≟Comp_ {atomicComp} (createC (txtbox s1)) (createC (button s2)) = Dec.no (λ ())

   _≟Comp_ {frame} (add c'c x x₁ isOpt) (add c'c₁ y y₁ isOpt₁) =
       _≟CompFr_ (add c'c x x₁ isOpt) (add c'c₁ y y₁ isOpt₁)

create-frame : CompEls frame
create-frame = createC{frame} tt

create-button : (s : String) → CompEls atomicComp
create-button s = createC{atomicComp} (button s)

create-txtbox : (s : String) → CompEls atomicComp
create-txtbox s = createC{atomicComp} (txtbox s)

validAdd : (c c' : Comp) → Set
validAdd atomicComp frame = ⊤
validAdd _ _ = ⊥

addReturnType : (c c' : Comp){_ : validAdd c c'} → Set
addReturnType atomicComp frame = CompEls frame
addReturnType frame frame {()}
addReturnType frame atomicComp {()}
addReturnType atomicComp atomicComp {()}

add' : {c c' : Comp}{va : validAdd c c'} → CompEls c → CompEls c'
      → (isOpt : IsOptimized) → addReturnType c c'{va}
add' {atomicComp} {frame} bt fr isOpt = add buttonFrame bt fr isOpt
add' {frame} {frame} {()} isOpt
add' {frame} {atomicComp} {()} isOpt
add' {atomicComp} {atomicComp} {()} isOpt

properties : {c : Comp}(e : CompEls c) → Set
properties {c} (add c'c e e' isOpt) = properties e × properties e'
properties {frame} (createC x) = (ℕ × ℕ × ℕ × ℕ)
properties {atomicComp} (createC x) = WxColor

ComponentEls : Comp → Set
ComponentEls = CompEls

Component : Set
Component = Comp

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Natural numbers with fast addition (for use together with
-- DifferenceVec)
------------------------------------------------------------------------

module Data.DifferenceNat where

open import Data.Nat as N using (ℕ)
open import Function

infixl 6 _+_

Diffℕ : Set
Diffℕ = ℕ → ℕ

0# : Diffℕ
0# = λ k → k

suc : Diffℕ → Diffℕ
suc n = λ k → N.suc (n k)

1# : Diffℕ
1# = suc 0#

_+_ : Diffℕ → Diffℕ → Diffℕ
m + n = λ k → m (n k)

toℕ : Diffℕ → ℕ
toℕ n = n 0

-- fromℕ n is linear in the size of n.

fromℕ : ℕ → Diffℕ
fromℕ n = λ k → n ⟨ N._+_ ⟩ k


text:
{-# OPTIONS --safe #-}
module Generics where

open import Data.Unit                    public using (⊤; tt)
open import Generics.Prelude             public using (liftω; liftω-inst)
open import Generics.HasDesc             public using (HasDesc)
open import Generics.Reflection          public using (deriveDesc)
open import Generics.Helpers             public

open import Generics.Constructions.Case       public using (deriveCase)
open import Generics.Constructions.Cong       public using (deriveCong)
open import Generics.Constructions.DecEq      public using (DecEq; _≟_; deriveDecEq)
open import Generics.Constructions.Elim       public using (deriveElim)
open import Generics.Constructions.Fold       public using (deriveFold)
open import Generics.Constructions.Recursion  public using (rec; Below)
open import Generics.Constructions.Show       public using (Show; show; deriveShow)

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics