text:
{-# OPTIONS --type-in-type #-}  -- yes, I will let you cheat in this exercise
{-# OPTIONS --allow-unsolved-metas #-}  -- allows import, unfinished

------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- CS410 2017/18 Exercise 2  CATEGORIES AND MONADS (worth 25%)
------------------------------------------------------------------------------
------------------------------------------------------------------------------

-- NOTE (19/10/17)  This file is currently incomplete: more will arrive on
-- GitHub.

-- NOTE (29/10/17)  All components are now present.

------------------------------------------------------------------------------
-- Dependencies
------------------------------------------------------------------------------

open import CS410-Prelude
open import CS410-Categories
open import Ex1

------------------------------------------------------------------------------
-- Categorical Jigsaws (based on Ex1)
------------------------------------------------------------------------------

OPE : Category            -- The category of order-preserving embeddings...
OPE = record
  { Obj          = Nat    -- ...has numbers as objects...
  ; _~>_         = _<=_   -- ...and "thinnings" as arrows.
  ; id~>         = oi
  ; _>~>_        = _o>>_
  ; law-id~>>~>  = idThen-o>>
  ; law->~>id~>  = idAfter-o>>
  ; law->~>>~>   = assoc-o>>
  }

VEC : Nat -> SET => SET                -- Vectors of length n...
VEC n = record
  { F-Obj       = \ X -> Vec X n       -- ...give a functor from SET to SET...
  ; F-map       = \ f xs -> vMap f xs  -- ...doing vMap to arrows.

  -- Now prove the laws.
  ; F-map-id~>  = extensionality \ xs -> {!!}
  ; F-map->~>   = \ f g -> extensionality \ xs -> {!!}
  }

Op : Category -> Category             -- Every category has an opposite...
Op C = record
  { Obj          = Obj                -- ...with the same objects, but...
  ; _~>_         = \ S T -> T ~> S    -- ...arrows that go backwards!
                                      -- Now, find the rest!
  ; id~>         = id~>
  ; _>~>_        = \ f g -> g >~> f
  ; law-id~>>~>  = law->~>id~>
  ; law->~>id~>  = law-id~>>~>
  ; law->~>>~>   = {!!}
  } where open Category C

CHOOSE : Set -> OPE => Op SET    -- Show that thinnings from n to m...
CHOOSE X = record                -- ...act by selection...
  { F-Obj       = Vec X          -- ...to cut vectors down from m to n.
  ; F-map       = {!!}
  ; F-map-id~>  = extensionality {!!}
  ; F-map->~>   = \ f g -> extensionality {!!}
  }

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- The List Monad (a warm-up)
------------------------------------------------------------------------------

-- The declaration of List has been added to the CS410-Prelude file:

-- data List (X : Set) : Set where
--   []   : List X
--   _,-_ : (x : X)(xs : List X) -> List X
-- infixr 4 _,-_

-- Appending two lists is rather well known, so I'll not ask you to write it.

_+L_ : {X : Set} -> List X -> List X -> List X
[]        +L ys = ys
(x ,- xs) +L ys = x ,- (xs +L ys)
infixr 4 _+L_

-- But I will ask you to find some structure for it.

--??--2.2---------------------------------------------------------------------

LIST-MONOID : Set -> Category
LIST-MONOID X =            -- Show that _+L_ is the operation of a monoid,...
  record
  { Obj          = One     -- ... i.e., a category with one object.
  ; _~>_         = {!!}
  ; id~>         = {!!}
  ; _>~>_        = {!!}
  ; law-id~>>~>  = {!!}
  ; law->~>id~>  = {!!}
  ; law->~>>~>   = {!!}
  } where
  -- useful helper proofs (lemmas) go here

--??--------------------------------------------------------------------------

-- Next, functoriality of lists. Given a function on elements, show how to
-- apply that function to all the elements of a list. (Haskell calls this
-- operation "map".)

--??--2.3---------------------------------------------------------------------

list : {X Y : Set} -> (X -> Y) -> List X -> List Y
list f xs = {!!}

LIST : SET => SET
LIST = record
  { F-Obj       = List
  ; F-map       = list
  ; F-map-id~>  = extensionality {!!}
  ; F-map->~>   = \ f g -> extensionality {!!}
  } where
  -- useful helper proofs (lemmas) go here

--??--------------------------------------------------------------------------

-- Moreover, applying a function elementwise should respect appending.

--??--2.4---------------------------------------------------------------------

LIST+L : {X Y : Set}(f : X -> Y) -> LIST-MONOID X => LIST-MONOID Y
LIST+L {X}{Y} f = record
  { F-Obj       = id
  ; F-map       = list f -- this yellow will go once LIST-MONOID has arrows!
  ; F-map-id~>  = {!!}
  ; F-map->~>   = {!!}
  } where
  -- useful helper proofs (lemmas) go here

--??--------------------------------------------------------------------------

-- Next, we have two very important "natural transformations".

--??--2.5---------------------------------------------------------------------

SINGLE : ID ~~> LIST
SINGLE = record
  { xf          = \ x -> x ,- []      -- turn a value into a singleton list
  ; naturality  = \ f -> {!!}
  }

--??--------------------------------------------------------------------------

-- Here, naturality means that it doesn't matter
-- whether you apply a function f, then make a singleton list
-- or you make a singleton list, then apply f to all (one of) its elements.

-- Now, define the operation that concatenates a whole list of lists, and
-- show that it, too, is natural. That is, it doesn't matter whether you
-- transform the elements (two layers inside) then concatenate, or you
-- concatenate, then transform the elements.

--??--2.6---------------------------------------------------------------------

concat : {X : Set} -> List (List X) -> List X
concat xss = {!!}

CONCAT : (LIST >=> LIST) ~~> LIST
CONCAT = record
  { xf          = concat
  ; naturality  = {!!}
  } where
  -- useful helper proofs (lemmas) go here

--??--------------------------------------------------------------------------

-- You've nearly built your first monad! You just need to prove that
-- single and concat play nicely with each other.

--??--2.7---------------------------------------------------------------------

module LIST-MONAD where
  open MONAD LIST public
  ListMonad : Monad
  ListMonad = record
    { unit      = SINGLE
    ; mult      = CONCAT
    ; unitMult  = {!!}
    ; multUnit  = {!!}
    ; multMult  = {!!}
    } where
    -- useful helper proofs (lemmas) go here

-- open LIST-MONAD

--??--------------------------------------------------------------------------

-- More monads to come...

------------------------------------------------------------------------------
-- Categories of Indexed Sets
------------------------------------------------------------------------------

-- We can think of some
--   P : I -> Set
-- as a collection of sets indexed by I, such that
--   P i
-- means "exactly the P-things which fit with i".

-- You've met
--   Vec X : Nat -> Set
-- where
--   Vec X n
-- means "exactly the vectors which fit with n".

-- Now, given two such collections, S and T, we can make a collection
-- of function types: the functions which fit with i map the
-- S-things which fit with i to the T-things which fit with i.

_-:>_ : {I : Set} -> (I -> Set) -> (I -> Set) -> (I -> Set)
(S -:> T) i = S i -> T i

-- So, (Vec X -:> Vec Y) n contains the functions which turn
-- n Xs into n Ys.

-- Next, if we know such a collection of sets, we can claim to have
-- one for each index.

[_] : {I : Set} -> (I -> Set) -> Set
[ P ] = forall i -> P i    -- [_] {I} P = (i : I) -> P i

-- E.g., [ Vec X -:> Vec Y ] is the type of functions from X-vectors
-- to Y-vectors which preserve length.

-- For any such I, we get a category of indexed sets with index-preserving
-- functions.

_->SET : Set -> Category
I ->SET = record
  { Obj    = I -> Set                 -- I-indexed sets
  ; _~>_   = \ S T -> [ S -:> T ]     -- index-respecting functions
  ; id~>   = \ i -> id                -- the identity at every index
  ; _>~>_  = \ f g i -> f i >> g i    -- composition at every index
  ; law-id~>>~> = refl                -- and the laws are very boring
  ; law->~>id~> = refl
  ; law->~>>~>  = \ f g h -> refl _
  }

-- In fact, we didn't need to choose SET here. We could do this construction
-- for any category: index the objects; index the morphisms.
-- But SET is plenty to be getting on with.

-- Now, let me define an operation that makes types from lists.

All : {X : Set} -> (X -> Set) -> (List X -> Set)
All P [] = One
All P (x ,- xs) = P x * All P xs

-- The idea is that we get a tuple of P-things: one for each list element.
-- So
--     All P (1 ,- 2 ,- 3 ,- [])
--   = P 1 * P 2 * P 3 * One

-- Note that if you think of List One as a version of Nat,
-- All becomes a lot like Vec.

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

VecCopy : Set -> Nat -> Set
VecCopy X n = All (\ _ -> X) (copy n)

-- Now, your turn...

--??--2.8---------------------------------------------------------------------

-- Show that, for any X, All induces a functor
-- from (X ->SET) to (List X ->SET)

all : {X : Set}{S T : X -> Set} ->
      [ S -:> T ] -> [ All S -:> All T ]
all f xs ss = {!!}

ALL : (X : Set) -> (X ->SET) => (List X ->SET)
ALL X = record
  { F-Obj      = All
  ; F-map      = all
  ; F-map-id~> = {!!}
  ; F-map->~>  = {!!}
  } where
  -- useful helper facts go here

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Cutting Things Up
------------------------------------------------------------------------------

-- Next, we're going to develop a very general technique for building
-- data structures.

-- We may think of an I |> O as a way to "cut O-shapes into I-shaped pieces".
-- The pointy end points to the type being cut; the flat end to the type of
-- pieces.

record _|>_ (I O : Set) : Set where
  field
    Cuts   : O -> Set                      -- given o : O, how may we cut it?
    inners : {o : O} -> Cuts o -> List I   -- given how we cut it, what are
                                           --   the shapes of its pieces?

-- Let us have some examples right away!

VecCut : One |> Nat              -- cut numbers into boring pieces
VecCut = record
  { Cuts = \ n -> One            -- there is one way to cut n
  ; inners = \ {n} _ -> copy n   -- and you get n pieces
  }

-- Here's a less boring example. You can cut a number into *two* pieces
-- by finding two numbers that add to it.

NatCut : Nat |> Nat
NatCut = record
  { Cuts = \ mn -> Sg Nat \ m -> Sg Nat \ n -> (m +N n) == mn
  ; inners = \ { (m , n , _) -> m ,- n ,- [] }
  }

-- The point is that we can make data structures that record how we
-- built an O-shaped thing from I-shaped pieces.

record Cutting {I O}(C : I |> O)(P : I -> Set)(o : O) : Set where
  constructor _8><_               -- "scissors"
  open _|>_ C
  field
    cut     : Cuts o              -- we decide how to cut o
    pieces  : All P (inners cut)  -- then we give all the pieces.
infixr 3 _8><_

-- For example...

VecCutting : Set -> Nat -> Set
VecCutting X = Cutting VecCut (\ _ -> X)

myVecCutting : VecCutting Char 5
myVecCutting = <> 8>< 'h' , 'e' , 'l' , 'l' , 'o' , <>

-- Or, if you let me fiddle about with strings for a moment,...
length : {X : Set} -> List X -> Nat
length [] = zero
length (x ,- xs) = suc (length xs)

listVec : {X : Set}(xs : List X) -> Vec X (length xs)
listVec [] = []
listVec (x ,- xs) = x ,- listVec xs

strVec : (s : String) -> Vec Char (length (primStringToList s))
strVec s = listVec (primStringToList s)

-- ...an example of cutting a number in two, with vector pieces.

footprints : Cutting NatCut (Vec Char) 10
footprints = (4 , 6 , refl 10) 8>< strVec "foot"
                                 , strVec "prints"
                                 , <>

-- Now, let me direct you to the =$ operator, now in CS410-Prelude.agda,
-- which you may find helps with the proofs in the following.

--??--2.9---------------------------------------------------------------------

-- Using what you already built for ALL, show that every Cutting C gives us
-- a functor between categories of indexed sets.

CUTTING : {I O : Set}(C : I |> O) -> (I ->SET) => (O ->SET)
CUTTING {I}{O} C = record
  { F-Obj = Cutting C
  ; F-map = {!!}
  ; F-map-id~> = extensionality \ o -> extensionality \ { (c 8>< ps) ->
     {!!} }
  ; F-map->~> = \ f g ->
     extensionality \ o -> extensionality \ { (c 8>< ps) ->
     {!!} }
  } where
  open _|>_ C
  open _=>_ (ALL I)

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Interiors
------------------------------------------------------------------------------

-- Next, let me define the notion of an algebra for a given functor in C => C

module ALGEBRA {C : Category}(F : C => C) where
  open Category C
  open _=>_ F

  Algebra : (X : Obj) -> Set   -- we call X the "carrier" of the algebra...
  Algebra X = F-Obj X ~> X     -- ...and we explain how to turn a bunch of Xs
                               -- into one
open ALGEBRA

-- Some week, we'll build categories whose objects are algebras. Not this week.

-- Instead, let's work with them a bit.

-- If we know a way to cut I-shapes into I-shaped pieces, we can build the
-- ways to "tile" an I with I-shaped T-tiles.

data Interior {I}(C : I |> I)(T : I -> Set)(i : I) : Set where
                                         -- either...
  tile : T i -> Interior C T i           -- we have a tile that fits, or...
  <_>  : Cutting C (Interior C T) i ->   -- ...we cut, then tile the pieces.
         Interior C T i

-- Let me give you an example of an interior.

subbookkeeper : Interior NatCut (Vec Char) 13
subbookkeeper = < (3 , 10 , refl _)
                  8>< tile (strVec "sub")
                    , < (4 , 6 , refl _)
                        8>< tile (strVec "book")
                          , tile (strVec "keeper")
                          , <> >
                    , <> >

-- We make a 13-interior from
-- a 3-tile and a 10-interior made from a 4-tile and a 6-tile.

-- Guess what? Interior C is always a Monad! We'll get there.

module INTERIOR {I : Set}{C : I |> I} where  -- fix some C...

  open _|>_ C                                -- ...and open it

  open module I->SET {I : Set} = Category (I ->SET)  -- work in I ->SET

  -- tile gives us an arrow from T into Interior C T

  tile' : {T : I -> Set} -> [ T -:> Interior C T ]
  tile' i = tile

  -- <_> gives us an algebra!

  cut' : {T : I -> Set} -> Algebra (CUTTING C) (Interior C T)
  cut' i = <_>

  -- Now, other (CUTTING C) algebras give us operators on interiors.

  module INTERIORFOLD {P Q : I -> Set} where

    interiorFold :
      [ P -:> Q ] ->              -- if we can turn a P into a Q...
      Algebra (CUTTING C) Q ->    -- ...and a bunch of Qs into a Q...
      [ Interior C P -:> Q ]      -- ...we can turn an interior of Ps into a Q

    allInteriorFold :             -- annoyingly, we'll need a specialized "all"
      [ P -:> Q ] ->
      Algebra (CUTTING C) Q ->
      [ All (Interior C P) -:> All Q ]

    interiorFold pq qalg i (tile p)      = pq i p
    interiorFold pq qalg i < c 8>< pis > =
      qalg i (c 8>< allInteriorFold pq qalg (inners c) pis)

    -- recursively turn all the sub-interiors into Qs
    allInteriorFold pq qalg []        <>         = <>
    allInteriorFold pq qalg (i ,- is) (pi , pis) =
      interiorFold pq qalg i pi , allInteriorFold pq qalg is pis

    -- The trouble is that if you use
    --   all (interiorFold pq qalg)
    -- to process the sub-interiors, the termination checker complains.

    -- But if you've built "all" correctly, you should be able to prove this:

--??--2.10--------------------------------------------------------------------

    allInteriorFoldLaw : (pq : [ P -:> Q ])(qalg : Algebra (CUTTING C) Q) ->
      allInteriorFold pq qalg == all (interiorFold pq qalg)
    allInteriorFoldLaw pq qalg = extensionality \ is -> extensionality \ ps ->
      {!!}
      where
      -- helper lemmas go here

--??--------------------------------------------------------------------------

    -- Now, do me a favour and prove this extremely useful fact.
    -- Its purpose is to bottle the inductive proof method for functions
    -- built with interiorFold.

--??--2.11--------------------------------------------------------------------

    interiorFoldLemma :
      (pq : [ P -:> Q ])(qalg : Algebra (CUTTING C) Q)
      (f : [ Interior C P -:> Q ]) ->
      ((i : I)(p : P i) -> pq i p == f i (tile p)) ->
      ((i : I)(c : Cuts i)(ps : All (Interior C P) (inners c)) ->
        qalg i (c 8>< all f (inners c) ps) == f i < c 8>< ps >) ->
      (i : I)(pi : Interior C P i) -> interiorFold pq qalg i pi == f i pi

    interiorFoldLemma pq qalg f base step i pi = {!!}

--??--------------------------------------------------------------------------

    -- We'll use it in this form:

    interiorFoldLaw : (pq : [ P -:> Q ])(qalg : Algebra (CUTTING C) Q)
      (f : [ Interior C P -:> Q ]) ->
      ((i : I)(p : P i) -> pq i p == f i (tile p)) ->
      ((i : I)(c : Cuts i)(ps : All (Interior C P) (inners c)) ->
        qalg i (c 8>< all f (inners c) ps) == f i < c 8>< ps >) ->
      interiorFold pq qalg == f

    interiorFoldLaw pq qalg f base step =
      extensionality \ i -> extensionality \ pi ->
      interiorFoldLemma pq qalg f base step i pi

  open INTERIORFOLD

  -- Let me pay you back immediately!
  -- An interiorBind is an interiorFold which computes an Interior,
  --   rewrapping each layer with < ... >

  interiorBind : {X Y : I -> Set} ->
                 [ X -:> Interior C Y ] -> [ Interior C X -:> Interior C Y ]
  interiorBind f = interiorFold f (\ i -> <_>)

  -- Because an interiorBind *makes* an interior, we can say something useful
  -- about what happens if we follow it with an interiorFold.

  interiorBindFusion : {X Y Z : I -> Set} ->
    (f : [ X -:> Interior C Y ])
    (yz : [ Y -:> Z ])(zalg : Algebra (CUTTING C) Z) ->
    (interiorBind f >~> interiorFold yz zalg) ==
      interiorFold (f >~> interiorFold yz zalg) zalg

  -- That is, we can "fuse" the two together, making one interiorFold.

  -- I'll do the proof as it's a bit hairy. You've given me all I need.
  -- Note that I don't use extensionality, just laws that relate functions.

  interiorBindFusion f yz zalg =
    (interiorBind f >~> interiorFold yz zalg)
      =< interiorFoldLaw
         (f >~> interiorFold yz zalg) zalg
         (interiorBind f >~> interiorFold yz zalg)
         (\ i p -> refl (interiorFold yz zalg i (f i p)))
         (\ i c ps -> refl (zalg i) =$= (refl (c 8><_) =$= (
            ((all (interiorBind f >~> interiorFold yz zalg)
              =[ F-map->~> (interiorBind f) (interiorFold yz zalg) >=
            (all (interiorBind f) >~> all (interiorFold yz zalg))
              =< refl _>~>_
                 =$= allInteriorFoldLaw f cut'
                 =$= allInteriorFoldLaw yz zalg  ]=
            allInteriorFold f (\ i -> <_>) >~> allInteriorFold yz zalg [QED])
           =$ inners c =$= refl ps))))
      ]=
    interiorFold (f >~> interiorFold yz zalg) zalg [QED]
    where open _=>_ (ALL I)

  -- You should find that a very useful piece of kit. In fact, you should
  -- not need extensionality, either.

  -- We need Interior C to be a functor.

--??--2.12--------------------------------------------------------------------

  -- using interiorBind, implement the "F-map" for Interiors as a one-liner

  interior : {X Y : I -> Set} ->
             [ X -:> Y ] -> [ Interior C X -:> Interior C Y ]
  interior f = {!!}

  -- using interiorBindFusion, prove the following law for "fold after map"

  interiorFoldFusion : {P Q R : I -> Set}
    (pq : [ P -:> Q ])(qr : [ Q -:> R ])(ralg : Algebra (CUTTING C) R) ->
    (interior pq >~> interiorFold qr ralg) == interiorFold (pq >~> qr) ralg
  interiorFoldFusion pq qr ralg =
    interior pq >~> interiorFold qr ralg
      =[ {!!} >=
    interiorFold (pq >~> qr) ralg [QED]
    where open _=>_ (ALL I)

  -- and now, using interiorFoldFusion if it helps,
  -- complete the functor construction

  INTERIOR : (I ->SET) => (I ->SET)
  INTERIOR = record
    { F-Obj      = Interior C
    ; F-map      = interior
    ; F-map-id~> = {!!}
    ; F-map->~>  = {!!}
    } where open _=>_ (ALL I)

--??--------------------------------------------------------------------------

  -- Now let's build the Monad.
  -- You should find that all the laws you have to prove follow from the
  -- fusion laws you already have.

  open MONAD INTERIOR

--??--2.13--------------------------------------------------------------------

  WRAP : ID ~~> INTERIOR
  WRAP = record
    { xf         = {!!}
    ; naturality = {!!}
    }

  -- use interiorBind to define the following
  FLATTEN : (INTERIOR >=> INTERIOR) ~~> INTERIOR
  FLATTEN = record
    { xf         = {!!}
    ; naturality = {!!}
    }

  INTERIOR-Monad : Monad
  INTERIOR-Monad = record
    { unit = WRAP
    ; mult = FLATTEN
    ; unitMult = {!!}
    ; multUnit = {!!}
    ; multMult = {!!}
    } where
    open _=>_ INTERIOR

--??--------------------------------------------------------------------------

open INTERIOR
open INTERIORFOLD

-- You should be able to define an algebra on vectors for NatCut, using +V

--??--2.14--------------------------------------------------------------------

NatCutVecAlg : {X : Set} -> Algebra (CUTTING NatCut) (Vec X)
NatCutVecAlg n xsc = {!!}

--??--------------------------------------------------------------------------

-- Check that it puts things together suitably when you evaluate this:

test1 : Vec Char 13
test1 = interiorFold (\ _ -> id) NatCutVecAlg 13 subbookkeeper

------------------------------------------------------------------------------
-- Cutting Up Pairs
------------------------------------------------------------------------------

module CHOICE where
  open _|>_

--??--2.15--------------------------------------------------------------------

  -- Show that if you can cut up I and cut up J, then you can cut up I * J.
  -- You now have two dimensions (I and J). The idea is that you choose one
  -- dimension in which to make a cut, and keep everything in the other
  -- dimension the same.

  _+C_ : {I J : Set} ->  I |> I ->  J |> J  ->  (I * J) |> (I * J)
  Cuts   (P +C Q) (i , j) = Cuts P i + Cuts Q j
  inners (P +C Q) = {!!}

--??--------------------------------------------------------------------------

open CHOICE

-- That should get us the ability to cut up *rectangules* by cutting either
-- vertically or horizontally.

NatCut2D : (Nat * Nat) |> (Nat * Nat)
NatCut2D = NatCut +C NatCut

Matrix : Set -> Nat * Nat -> Set
Matrix X (w , h) = Vec (Vec X w) h

-- If you've done it right, you should find that the following typechecks.
-- It's the interior of a rectangle, tiled with matrices of characters.

rectangle : Interior NatCut2D (Matrix Char) (15 , 6)
rectangle = < inr (4 , 2 , refl _)
            8>< < inl (7 , 8 , refl _)
                8>< tile (strVec "seventy"
                       ,- strVec "kitchen"
                       ,- strVec "program"
                       ,- strVec "mistake"
                       ,- [])
                  , tile (strVec "thousand"
                       ,- strVec "soldiers"
                       ,- strVec "probably"
                       ,- strVec "undefine"
                       ,- [])
                  , <> >
              , tile (strVec "acknowledgement"
                   ,- strVec "procrastination"
                   ,- [])
              , <> >

-- Later, we'll use rectangular interiors as the underlying data structure
-- for a window manager.

-- But for now, one last thing.

--??--2.16--------------------------------------------------------------------

-- Show that if you have a vector of n Ps for every element of a list,
-- then you can make a vector of n (All P)s .
-- Hint: Ex1 provides some useful equipment for this job.

vecAll : {I : Set}{P : I -> Set}{is : List I}{n : Nat} ->
         All (\ i -> Vec (P i) n) is -> Vec (All P is) n
vecAll {is = is} pss = {!!}

-- Given vecAll, show that algebra for any cutting can be lifted
-- to an algebra on vectors.

VecLiftAlg : {I : Set}(C : I |> I){X : I -> Set}
             (alg : Algebra (CUTTING C) X){n : Nat} ->
             Algebra (CUTTING C) (\ i -> Vec (X i) n)
VecLiftAlg C alg i (c 8>< pss) = {!!}

-- Now show that you can build an algebra for matrices
-- which handles cuts in either dimension,
-- combining them either horizontally or vertically!

NatCut2DMatAlg : {X : Set} -> Algebra (CUTTING NatCut2D) (Matrix X)
NatCut2DMatAlg _ (inl c 8>< ms) = {!!}
NatCut2DMatAlg _ (inr c 8>< ms) = {!!}

--??--------------------------------------------------------------------------

-- And that should give you a way to glue pictures together from interiors.

picture : [ Interior NatCut2D (Matrix Char) -:> Matrix Char ]
picture = interiorFold (\ _ -> id) NatCut2DMatAlg

-- You should be able to check that the following gives you something
-- sensible:

test2 = picture _ rectangle


text:
  -- A predicate transformer allowing one to express that
  -- some value definitely does /not/ own some resource
  infixl 9 _◇_
  data _◇_ {p} (P : SPred p) (Φᵢ : Carrier) : SPred (p ⊔ a) where
    ⟪_,_⟫ : ∀ {Φₚ Φ} → P Φₚ → Φᵢ ⊎ Φₚ ≣ Φ → (P ◇ Φᵢ) Φ

  -- | This gives another wand like thing

  module _ {p q} (P : SPred p) (Q : SPred q) where
    infixr 8 _◇─_
    _◇─_ : SPred (p ⊔ q ⊔ a)
    _◇─_ Φᵢ = ∀[ P ◇ Φᵢ ⇒ Q ]

  module _ {p q} {P : SPred p} {Q : SPred q} where
    pair : ε[ P ◇─ (Q ◇─ P ✴ Q) ]
    pair ⟪ px , σ₁ ⟫ ⟪ qx , σ₂ ⟫ rewrite ⊎-id⁻ˡ σ₁ = px ×⟨ σ₂ ⟩ qx

  module _ {p} {P : SPred p} where
    ◇-ε : ∀[ P ◇ ε ⇒ P ]
    ◇-ε ⟪ px , σ ⟫ rewrite ⊎-id⁻ˡ σ = px

    -- pure : ∀ {p q} {P : SPred p} {Q : SPred q} → (P ε → Q Φ) → (P ─✴ Q) Φ
    -- pure f px = {!!}
    -- -- pure = {!!}
    -- a pure wand is a resource-polymorphic function
    -- unwand : ε[ P ─✴ Q ] → ∀[ P ⇒ Q ]
    -- unwand f p = f p ⊎-idˡ

    -- ✴-pure : ∀ {p q} {P : SPred p} {Q : SPred q} → (∀ {Φ} → P Φ → ε ⊎ Φ ≣ Φ → Q Φ) → ε[ P ─✴ Q ]
    -- ✴-pure f px σ rewrite ⊎-id⁻ˡ σ = f px ⊎-idˡ

    -- ✴-flip : ∀ {p q r} {P : SPred p} {Q : SPred q} {R : SPred r} → ε[ (P ─✴ (Q ─✴ R)) ─✴ (Q ─✴ (P ─✴ R)) ]
    -- ✴-flip {P = P} {Q} {R} =
    --   ✴-pure {P = P ─✴ (Q ─✴ R)} {Q = Q ─✴ (P ─✴ R)} λ f σ₁ q σ₂ p σ₃ →
    --   let _ , σ₃ , σ₄ = ⊎-assoc (⊎-comm σ₂) σ₃ in f p σ₄ q (⊎-comm σ₃)

  -- ─[id] : ∀ {p} {P : Pred _ p} → ε[ P ─✴ P ]
  -- ─[id] px σ rewrite ⊎-id⁻ˡ σ = px

ext: agda


text:
-- This file is ported from a part of Martin Escardó's HoTT lecture notes
-- (https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html).

{-# OPTIONS --without-K --safe #-}
module Util.HoTT.Section where

open import Util.HoTT.HLevel.Core
open import Util.Prelude
open import Util.Relation.Binary.PropositionalEquality using
  ( Σ-≡⁺ ; subst-subst-sym )

private
  variable
    α β γ : Level
    A B C : Set α

infix 4 _◁_

record HasSection {A : Set α} {B : Set β} (f : A → B) : Set (α ⊔ℓ β) where
  field
    section : B → A
    isSection : ∀ x → f (section x) ≡ x

open HasSection public

record _◁_ (A : Set α) (B : Set β) : Set (α ⊔ℓ β) where
  field
    retraction : B → A
    hasSection : HasSection retraction

  open HasSection hasSection public renaming (isSection to retraction∘section)

open _◁_ public

◁-refl : A ◁ A
◁-refl = record
  { retraction = id
  ; hasSection = record
    { section = id
    ; isSection = λ _ → refl
    }
  }

◁-trans : A ◁ B → B ◁ C → A ◁ C
◁-trans A◁B B◁C = record
  { retraction = A◁B .retraction ∘ B◁C .retraction
  ; hasSection = record
    { section = B◁C .section ∘ A◁B .section
    ; isSection = λ x
        → trans (cong (A◁B .retraction) (B◁C .retraction∘section _))
            (A◁B .retraction∘section _)
    }
  }

Σ-◁ : {A : Set α} {B : A → Set β} {C : A → Set γ}
  → (∀ a → B a ◁ C a)
  → Σ A B ◁ Σ A C
Σ-◁ B◁C = record
  { retraction = λ { (a , c) → a , B◁C a .retraction c }
  ; hasSection = record
    { section = λ { (a , b) → a , B◁C a .section b }
    ; isSection = λ { (a , b) → cong (a ,_) (B◁C a .retraction∘section b) }
    }
  }

◁-pres-IsContr : A ◁ B → IsContr B → IsContr A
◁-pres-IsContr A◁B (b , canon)
  = A◁B .retraction b
  , λ a
      → trans (cong (A◁B .retraction) (canon (A◁B .section a)))
          (A◁B .retraction∘section a)

Σ-◁-reindexing : {A : Set α} {B : Set β} {P : A → Set γ}
  → (r : A ◁ B)
  → Σ A P ◁ Σ B (P ∘ r .retraction)
Σ-◁-reindexing {P = P} r = record
  { retraction = λ { (b , x) → r .retraction b , x }
  ; hasSection = record
    { section = λ where
        (a , x) → r .section a , subst P (sym (r .retraction∘section a)) x
    ; isSection = λ where
        (a , x) → Σ-≡⁺
          ( r .retraction∘section a
          , subst-subst-sym (r .retraction∘section a)
          )
    }
  }

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module TimeSpace where
open import Data.Product
open import Data.Sum
open import Data.List
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Pi.Syntax
open import Pi.Opsem
open import Pi.Eval
open import Pi.Examples

-- 𝔹+ n = 𝔹 +ᵤ … +ᵤ 𝔹
𝔹+ : ℕ → 𝕌
𝔹+ 0 = 𝟘
𝔹+ 1 = 𝔹
𝔹+ (suc (suc n)) = 𝔹 +ᵤ (𝔹+ (suc n))

-- 𝔹* n = 𝔹 ×ᵤ … ×ᵤ 𝔹
𝔹* : ℕ → 𝕌
𝔹* 0 = 𝔹
𝔹* (suc n) = 𝔹 ×ᵤ 𝔹* n

convert : ∀ {n} → 𝔹+ (2 ^ n) ↔ 𝔹* n
convert {0} = id↔
convert {1} = (uniti⋆l ⊕ uniti⋆l) ⨾ factor
convert {suc (suc n)} = split ⨾ (convert {suc n} ⊕ (coe {n} ⨾ convert {suc n})) ⨾ (uniti⋆l ⊕ uniti⋆l) ⨾ factor
  where
  coe : ∀ {n} → 𝔹+ ((2 ^ n) + ((2 ^ n) + 0) + 0) ↔ 𝔹+ (2 ^ (1 + n))
  coe {n} rewrite +-identityʳ ((2 ^ n) + ((2 ^ n) + 0)) = id↔

  split : ∀ {n m} → 𝔹+ (n + m) ↔ (𝔹+ n +ᵤ 𝔹+ m)
  split {0} {m} = uniti₊l
  split {1} {0} = uniti₊r
  split {1} {1} = id↔
  split {1} {suc (suc m)} = id↔
  split {suc (suc n)} {m} = (id↔ ⊕ split) ⨾ assocl₊

-- flip the last 𝔹
flip+ : (n : ℕ) → 𝔹+ n ↔ 𝔹+ n
flip+ 0 = id↔
flip+ 1 = swap₊
flip+ (suc (suc n)) = id↔ ⊕ flip+ (suc n)

-- flip* n (b₁,…,bₙ,b) = (b₁,…,bₙ,b xor (b₁ ∧ … ∧ bₙ))
flip* : (n : ℕ) → (𝔹* n) ↔ (𝔹* n)
flip* 0 = swap₊
flip* (suc n) = dist ⨾ (id↔ ⊕ (id↔ ⊗ flip* n)) ⨾ factor

v* : (n : ℕ) → ⟦ 𝔹* n ⟧
v* 0 = 𝔽
v* 1 = 𝕋 , v* 0
v* (suc (suc n)) = 𝕋 , v* (suc n)

v+ : (n : ℕ) → n ≢ 0 → ⟦ 𝔹+ n ⟧
v+ 0 0≠0 = 0≠0 refl
v+ 1 _ = 𝔽
v+ (suc (suc n)) _ = inj₂ (v+ (suc n) (λ ()))

-- Counting number of values in given context
#ctx : ∀ {A B} → Context {A} {B} → ℕ
#ctx ☐ = 0
#ctx (☐⨾ c₂ • κ) = #ctx κ
#ctx (c₁ ⨾☐• κ) = #ctx κ
#ctx (☐⊕ c₂ • κ) = #ctx κ
#ctx (c₁ ⊕☐• κ) = #ctx κ
#ctx (☐⊗[ c₂ , x ]• κ) = 1 + #ctx κ
#ctx ([ c₁ , x ]⊗☐• κ) = 1 + #ctx κ

#st : State → ℕ
#st ⟨ c ∣ v ∣ κ ⟩ = 1 + #ctx κ
#st ［ c ∣ v ∣ κ ］ = 1 + #ctx κ

-- Returns the number of steps and maximum #st in a execution trace
runST : ∀ {A B} → A ↔ B → ⟦ A ⟧ → List State × ℕ × ℕ
runST c v = states , length states , foldl (λ { s st → s ⊔ #st st }) 0 states
  where states = evalₜᵣ c v

-- Examples
ex1 : ℕ × ℕ
ex1 = let(_ , t , s) = runST (flip* 9) (v* 9)
      in (t , s)  -- t=128 , s=10

ex2 : ℕ × ℕ
ex2 = let (_ , t , s) = runST (flip+ 512) (v+ 512 (λ ()))
      in  (t , s) -- t=1024 , s=1


text:
open import Oscar.Prelude
open import Oscar.Class.Smap
open import Oscar.Data.Proposequality
open import Oscar.Class.Surjection

module Oscar.Data.Surjcollation where

𝓼urjcollation : ∀ {𝔵₁ 𝔵₂ 𝔞 𝔟} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (surjection : Surjection.type 𝔛₁ 𝔛₂)
  𝔟̇
  (𝔅 : 𝔛₂ → Ø 𝔟)
  (𝔄 : π̂² 𝔞 𝔛₁)
  → Ø 𝔵₁ ∙̂ 𝔞 ∙̂ 𝔟 ∙̂ ↑̂ 𝔟̇
𝓼urjcollation surjection 𝔟̇ 𝔅 𝔄 = ∀ {m} → 𝔅 (surjection m) → 𝔅 (surjection m) → LeftṖroperty 𝔟̇ 𝔄 m

module _ {𝔵₁ 𝔵₂ 𝔞 𝔟 𝔟̇} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (𝔅 : 𝔛₂ → Ø 𝔟)
  (𝔄 : π̂² 𝔞 𝔛₁)
  ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  ⦃ _ : Smaphomarrow!.class 𝔄 𝔅 ⦄
  (𝔅̇ : ∀̇ π̂² 𝔟̇ 𝔅)
  (let infix 4 _⟨𝔅̇⟩_
       _⟨𝔅̇⟩_ : ∀ {x} → 𝔅 x → 𝔅 x → Ø 𝔟̇
       _⟨𝔅̇⟩_ p q = 𝔅̇ p q)
  where
  surjcollation[_]⟦_/_⟧ : 𝓼urjcollation surjection 𝔟̇ 𝔅 𝔄
  surjcollation[_]⟦_/_⟧ p q .π₀ x = x ◃ p ⟨𝔅̇⟩ x ◃ q

module _ {𝔵₁ 𝔵₂ 𝔞 𝔟 𝔟̇} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂} {𝔅 : 𝔛₂ → Ø 𝔟}
  (𝔄 : π̂² 𝔞 𝔛₁)
  ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  ⦃ _ : Smaphomarrow!.class 𝔄 𝔅 ⦄
  (𝔅̇ : ∀̇ π̂² 𝔟̇ 𝔅)
  where
  surjcollation⟦_/_⟧ = surjcollation[ 𝔅 ]⟦ 𝔄 / 𝔅̇ ⟧

module _ {𝔵₁ 𝔵₂ 𝔞} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (𝔄 : 𝔛₁ → 𝔛₁ → Ø 𝔞)
    {𝔟} {𝔅 : 𝔛₂ → Ø 𝔟}
    ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
    ⦃ _ : Smaphomarrow!.class 𝔄 𝔅 ⦄
    {𝔟̇} {𝔅̇ : ∀ {x} → 𝔅 x → 𝔅 x → Ø 𝔟̇}
  where
  surjcollation⟦_⟧ = surjcollation[ 𝔅 ]⟦ 𝔄 / 𝔅̇ ⟧

module _ {𝔵₁ 𝔵₂ 𝔞 𝔟} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (𝔅 : 𝔛₂ → Ø 𝔟)
  (𝔄 : π̂² 𝔞 𝔛₁)
    ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
    ⦃ _ : Smaphomarrow!.class 𝔄 𝔅 ⦄
  where
  ≡-surjcollation[_]⟦_⟧ = surjcollation[ 𝔅 ]⟦ 𝔄 / _≡_ ⟧

module _ {𝔵₁ 𝔞} {𝔛₁ : Ø 𝔵₁}
  (𝔄 : π̂² 𝔞 𝔛₁)
    {𝔵₂} {𝔛₂ : Ø 𝔵₂} ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
    {𝔟} {𝔅 : 𝔛₂ → Ø 𝔟} ⦃ _ : Smaphomarrow!.class 𝔄 𝔅 ⦄
  where
  ≡-surjcollation⟦_⟧ = ≡-surjcollation[ 𝔅 ]⟦ 𝔄 ⟧

module _ {𝔵₁ 𝔞} {𝔛₁ : Ø 𝔵₁} {𝔄 : π̂² 𝔞 𝔛₁}
  where
  ≡-surjcollation = ≡-surjcollation⟦ 𝔄 ⟧

module Surjcollation {𝔵₁ 𝔵₂ 𝔞 𝔟̇} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂} ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  (𝔄 : 𝔛₁ → 𝔛₁ → Ø 𝔞)
  (𝔅̇ : ∀ {𝔟} {𝔅 : 𝔛₂ → Ø 𝔟} → (∀ {x} → 𝔅 x → 𝔅 x → Ø 𝔟̇))
    {𝔟} {𝔅 : 𝔛₂ → Ø 𝔟}
    ⦃ _ : Smaphomarrow!.class 𝔄 𝔅 ⦄
  where
  method = surjcollation[ 𝔅 ]⟦ 𝔄 / 𝔅̇ {𝔅 = 𝔅} ⟧

  infix 18 _⟹_
  _⟹_ = method


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

-- Finished half of the proof!
--  - functions between Bool * A and ∑ A are written
--  - One direction of the inverse proof is done!
--
-- Wrapping up the camera ready version of our
-- PLDI paper took more time than I thought it would and so
-- I got a late start on this. I think by class on Tuesday
-- I could have the other half finished.
--
-- Noet: I collaborated w/ Andre on this some.

module thm8511part2 where

open import Level using (_⊔_)
open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂; Σ; Σ-syntax)
open import Function renaming (_∘_ to _·_)

import Relation.Binary.Core as C
import Relation.Binary.PropositionalEquality as P
--open P.≡-Reasoning

infixr 8  _∘_     -- path composition
infix  4  _≡_     -- propositional equality
infix  4  _∼_     -- homotopy between two functions
infix  4  _≃_     -- type of equivalences
-- macros from tzaikin for equational rewriting over non-standard ≡
infixr 4 _≡⟨_⟩_
infix 4  _∎

indBool : (C : Bool → Set) →
          (C true) →
          (C false) →
          (b : Bool) →
          (C b)
indBool C ct cf true = ct
indBool C ct cf false = cf

ind× : ∀ {A B : Set}
       {C : A × B → Set} →
       ((a : A) → (b : B) → C (a , b)) →
       (p : A × B) →
       (C p)
ind× {C} f (a , b) = f a b

------------------------------------------------------------------------------
-- Some abbreviations and simple lemmas and paths

_≡_ : ∀ {ℓ} {A : Set ℓ} → (x y : A) → Set ℓ
_≡_ {ℓ} {A} x y = C._≡_ {ℓ} {A} x y

-- Groupoid

refl : ∀ {ℓ} {A} → (x : A) → x ≡ x
refl {ℓ} {A} x = C.refl {ℓ} {A} {x}

! : ∀ {u} → {A : Set u} {x y : A} → (x ≡ y) → (y ≡ x)
! = P.sym

_∘_ : ∀ {ℓ} {A : Set ℓ} {x y z : A} →
      (x ≡ y) → (y ≡ z) → (x ≡ z)
_∘_ = P.trans

unitTransL : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ refl x ∘ p)
unitTransL C.refl = C.refl

unitTransR : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ p ∘ refl y)
unitTransR C.refl = C.refl

invComp : {A : Set} {x y z : A} → (p : x ≡ y) → (q : y ≡ z) →
          ! (p ∘ q) ≡ ! q ∘ ! p
invComp C.refl C.refl = C.refl

assocP : {A : Set} {x y z w : A} → (p : x ≡ y) → (q : y ≡ z) → (r : z ≡ w) →
         (p ∘ (q ∘ r) ≡ (p ∘ q) ∘ r)
assocP C.refl C.refl C.refl = C.refl

invTransL : {A : Set} {x y : A} → (p : x ≡ y) → (! p ∘ p ≡ refl y)
invTransL C.refl = C.refl

invId : {A : Set} {x y : A} → (p : x ≡ y) → (! (! p) ≡ p)
invId C.refl = C.refl

-- Handy "macros" (from tzaikin)
_∎ : ∀ {ℓ} → {A : Set ℓ} → (p : A) → p ≡ p
p ∎ = refl p

_≡⟨_⟩_ : ∀ {ℓ} → {A : Set ℓ} → {q r : A} → (p : A) → p ≡ q → q ≡ r → p ≡ r
p ≡⟨ α ⟩ β = α ∘ β

-- Functors

ap : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} →
     (f : A → B) → {x y : A} → (x ≡ y) → (f x ≡ f y)
ap = P.cong

apfId : {A : Set} {x y : A} → (p : x ≡ y) → ap id p ≡ p
apfId C.refl = C.refl

apfInv : ∀ {u} → {A B : Set u} {x y : A} → (f : A → B) → (p : x ≡ y) →
         ap f (! p) ≡ ! (ap f p)
apfInv f C.refl = C.refl

apfTrans : ∀ {u} → {A B : Set u} {x y z : A} →
  (f : A → B) → (p : x ≡ y) → (q : y ≡ z) → ap f (p ∘ q) ≡ (ap f p) ∘ (ap f q)
apfTrans f C.refl C.refl = C.refl

apfComp : {A B C : Set} {x y : A} → (f : A → B) → (g : B → C) → (p : x ≡ y) →
          ap g (ap f p) ≡ ap (g · f) p
apfComp f g C.refl = C.refl

apconst : {A B : Set} {x y : A} → (p : x ≡ y) (b : B) →
          ap (λ _ → b) p ≡ refl b
apconst C.refl b = C.refl

-- Transport

transport : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} (B : A → Set ℓ₂) →
            {x y : A} → (x ≡ y) → B x → B y
transport = P.subst

transportId : {A B : Set} {y z : A} → (f g : A → B) →
  (p : y ≡ z) → (q : f y ≡ g y) →
  transport (λ x → f x ≡ g x) p q ≡ ! (ap f p) ∘ q ∘ (ap g p)
transportId f g C.refl q =
  (q
    ≡⟨ unitTransR q ⟩
   q ∘ C.refl
    ≡⟨ unitTransL (q ∘ C.refl) ⟩
   ! C.refl ∘ (q ∘ C.refl) ∎)

apd : ∀ {ℓ₁ ℓ₂} → {A : Set ℓ₁} {B : A → Set ℓ₂} →
      (f : (x : A) → B x) → {x y : A} → (p : x ≡ y) →
      transport B p (f x) ≡ f y
apd f C.refl = C.refl

-- Homotopies and equivalences

_∼_ : ∀ {ℓ ℓ'} → {A : Set ℓ} {P : A → Set ℓ'} →
      (f g : (x : A) → P x) → Set (ℓ ⊔ ℓ')
_∼_ {ℓ} {ℓ'} {A} {P} f g = (x : A) → f x ≡ g x

record qinv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (ℓ ⊔ ℓ') where
  constructor mkqinv
  field
    g : B → A
    α : (f · g) ∼ id
    β : (g · f) ∼ id

record isequiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (ℓ ⊔ ℓ') where
  constructor mkisequiv
  field
    g : B → A
    α : (f · g) ∼ id
    h : B → A
    β : (h · f) ∼ id

iso : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {f : A → B} → qinv f → isequiv f
iso (mkqinv qg qα qβ) = mkisequiv qg qα qg qβ

_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A ≃ B = Σ (A → B) isequiv

postulate
  univalence : {A B : Set} → (A ≡ B) ≃ (A ≃ B)

------------------------------------------------------------------------------
-- Some higher-inductive types

module Circle where

  private
    data S¹* : Set where
      base* : S¹*

  -- define the interface for S¹

  S¹ : Set
  S¹ = S¹*

  base : S¹
  base = base*

  postulate
    loop : base ≡ base

  -- recursion principle

  recS¹ : {C : Set} → (cbase : C) → (cloop : cbase ≡ cbase) → S¹ → C
  recS¹ cbase cloop base* = cbase

  postulate
    βrecS¹ : {C : Set} → (cbase : C) → (cloop : cbase ≡ cbase) →
      ap (recS¹ cbase cloop) loop ≡ cloop

  -- induction principle

  indS¹ : {C : S¹ → Set} →
    (cbase : C base) → (cloop : transport C loop cbase ≡ cbase) →
    (circle : S¹) → C circle
  indS¹ cbase cloop base* = cbase

------------------------------------------------------------------------------
module Suspension where

  private
    data ∑* (A : Set) : Set where
      N* : ∑* A
      S* : ∑* A

  -- define the interface for ∑A

  ∑ : (A : Set) → Set
  ∑ = ∑*

  N : {A : Set} → ∑ A
  N = N*

  S : {A : Set} → ∑ A
  S = S*

  postulate
    merid : {A : Set} → A → (N {A} ≡ S {A})

  -- recursion principle

  rec∑ : {A : Set} → {C : Set} → (cn cs : C) → (cm : A → (cn ≡ cs)) → ∑ A → C
  rec∑ cn cs cm N* = cn
  rec∑ cn cs cm S* = cs

  postulate
    βrec∑ : {A : Set} → {C : Set} → (cn cs : C) → (cm : A → (cn ≡ cs)) →
      (a : A) → ap (rec∑ cn cs cm) (merid a) ≡ (cm a)

  -- induction principle

  ind∑ : {A : Set} → {C : ∑ A → Set} → (cn : C N) → (cs : C S) →
         ((a : A) → transport C (merid a) cn ≡ cs) → (s : ∑ A) → C s
  ind∑ cn cs m N* = cn
  ind∑ cn cs m S* = cs

------------------------------------------------------------------------------
module Join where

  private
    data _**_ (A B : Set) : Set where
      inl* : A → A ** B
      inr* : B → A ** B

  -- define the interface for A*B

  _*_ : (A B : Set) → Set
  A * B = A ** B

  inl : {A B : Set} → A → A * B
  inl = inl*

  inr : {A B : Set} → B → A * B
  inr = inr*

  postulate
    glue : {A B : Set} → (c : A × B) → inl (proj₁ c) ≡ inr (proj₂ c)

  -- recursion principle

  rec* : {A B : Set} {D : Set} →
         (ad : A → D) → (bd : B → D) →
         (gd : (c : A × B) → ad (proj₁ c) ≡ bd (proj₂ c)) →
         A * B → D
  rec* ad bd gd (inl* a) = ad a
  rec* ad bd gd (inr* b) = bd b

  postulate
    βrec* : {A B : Set} {D : Set} →
            (ad : A → D) → (bd : B → D) →
            (gd : (c : A × B) → ad (proj₁ c) ≡ bd (proj₂ c)) →
            (c : A × B) → ap (rec* ad bd gd) (glue c) ≡ gd c

  -- induction principle

  ind* : {A B : Set} {D : A * B → Set} →
         (ad : (a : A) → D (inl a)) → (bd : (b : B) → D (inr b)) →
         (gd : (c : A × B) → transport D (glue c) (ad (proj₁ c)) ≡ bd (proj₂ c))
         (c : A * B) → D c
  ind* ad bd gd (inl* a) = ad a
  ind* ad bd gd (inr* b) = bd b

------------------------------------------------------------------------------
-- Lemma 6.5.1

module ∑Bool≡S¹ where

  open Circle
  open Suspension

  east : N ≡ S
  east = merid false

  west : N ≡ S
  west = merid true

  -- S¹ → ∑ Bool

  fcircle : S¹ → ∑ Bool
  fcircle = recS¹ N (east ∘ ! west)

  floop : ap fcircle loop ≡ east ∘ ! west
  floop = βrecS¹ N (east ∘ ! west)

  -- ∑ Bool → S¹

  gcircle : ∑ Bool → S¹
  gcircle = rec∑ base base (λ b → if b then refl base else loop)

  geast : ap gcircle east ≡ loop
  geast = βrec∑ base base (λ b → if b then refl base else loop) false

  gwest : ap gcircle west ≡ (refl base)
  gwest = βrec∑ base base (λ b → if b then refl base else loop) true

  -- round trip S¹ → S¹

  gf : S¹ → S¹
  gf = gcircle · fcircle

  gfloop : ap gf loop ≡ loop
  gfloop =
          (ap gf loop
             ≡⟨ ! (apfComp fcircle gcircle loop) ⟩
           ap gcircle (ap fcircle loop)
             ≡⟨ ap (ap gcircle) floop ⟩
           ap gcircle (east ∘ ! west)
             ≡⟨ apfTrans gcircle east (! west) ⟩
           ap gcircle east ∘ ap gcircle (! west)
             ≡⟨ ap (λ x → ap gcircle east ∘ x) (apfInv gcircle west) ⟩
           ap gcircle east ∘ ! (ap gcircle west)
             ≡⟨ ap (λ x → ap gcircle east ∘ ! x) gwest ⟩
           ap gcircle east ∘ (refl base)
             ≡⟨ ! (unitTransR (ap gcircle east)) ⟩
           ap gcircle east
             ≡⟨ geast ⟩
           loop ∎)

  αloop : transport (λ x → gf x ≡ x) loop (refl base) ≡ refl base
  αloop =
         (transport (λ x → gf x ≡ x) loop (refl base)
            ≡⟨ transportId gf id loop (refl base) ⟩
          ! (ap gf loop) ∘ refl base ∘ ap id loop
            ≡⟨ ap (λ x → ! (ap gf loop) ∘ refl base ∘ x) (apfId loop) ⟩
          ! (ap gf loop) ∘ refl base ∘ loop
            ≡⟨ ap (λ x → ! (ap gf loop) ∘ x) (! (unitTransL loop)) ⟩
          ! (ap gf loop) ∘ loop
            ≡⟨ ap (λ x → ! x ∘ loop) gfloop ⟩
          ! loop ∘ loop
            ≡⟨ invTransL loop ⟩
          refl base ∎)

  βcircle : gf ∼ id
  βcircle = indS¹ {λ x → gf x ≡ x} (refl base) αloop

  -- round trip ∑ Bool → ∑ Bool

  fg : ∑ Bool → ∑ Bool
  fg = fcircle · gcircle

  fgeast : ap fg east ≡ east ∘ ! west
  fgeast =
         (ap fg east
             ≡⟨ ! (apfComp gcircle fcircle east) ⟩
           ap fcircle (ap gcircle east)
             ≡⟨ ap (ap fcircle) geast ⟩
           ap fcircle loop
             ≡⟨ floop ⟩
           (east ∘ ! west) ∎)

  fgwest : ap fg west ≡ refl N
  fgwest =
         (ap fg west
             ≡⟨ ! (apfComp gcircle fcircle west) ⟩
           ap fcircle (ap gcircle west)
             ≡⟨ ap (ap fcircle) gwest ⟩
           ap fcircle (refl base)
             ≡⟨ C.refl ⟩
           refl N ∎)

  αeast : transport (λ x → fg x ≡ x) east (refl N) ≡ west
  αeast =
         (transport (λ x → fg x ≡ x) east (refl N)
            ≡⟨ transportId fg id east (refl N) ⟩
          ! (ap fg east) ∘ refl N ∘ ap id east
            ≡⟨ ap (λ x → ! (ap fg east) ∘ refl N ∘ x) (apfId east) ⟩
          ! (ap fg east) ∘ refl N ∘ east
             ≡⟨ ap (λ x → ! (ap fg east) ∘ x) (! (unitTransL east)) ⟩
          ! (ap fg east) ∘ east
             ≡⟨ ap (λ x → ! x ∘ east) fgeast ⟩
          ! (east ∘ ! west) ∘ east
            ≡⟨ ap (λ x → x ∘ east) (invComp east (! west)) ⟩
          (! (! west) ∘ ! east) ∘ east
            ≡⟨ ! (assocP (! (! west)) (! east) east) ⟩
          ! (! west) ∘ ! east ∘ east
            ≡⟨ ap (λ x → ! (! west) ∘ x) (invTransL east) ⟩
          ! (! west) ∘ refl S
            ≡⟨ ! (unitTransR (! (! west)))  ⟩
          ! (! west)
            ≡⟨ invId west ⟩
          west ∎)

  αwest : transport (λ x → fg x ≡ x) west (refl N) ≡ west
  αwest =
         (transport (λ x → fg x ≡ x) west (refl N)
            ≡⟨ transportId fg id west (refl N) ⟩
          ! (ap fg west) ∘ refl N ∘ ap id west
            ≡⟨ ap (λ x → ! (ap fg west) ∘ refl N ∘ x) (apfId west) ⟩
          ! (ap fg west) ∘ refl N ∘ west
             ≡⟨ ap (λ x → ! (ap fg west) ∘ x) (! (unitTransL west)) ⟩
          ! (ap fg west) ∘ west
             ≡⟨ ap (λ x → ! x ∘ west) fgwest ⟩
          ! (refl N) ∘ west
            ≡⟨ ! (unitTransL west) ⟩
          west ∎)

  αcircle : fg ∼ id
  αcircle =
    ind∑ (refl N) west (λ { false → αeast; true → αwest })

  -- main lemmas

  equivlemma : ∑ Bool ≃ S¹
  equivlemma = (gcircle , iso (mkqinv fcircle βcircle αcircle))

  lemma : ∑ Bool ≡ S¹
  lemma with univalence
  ... | (_ , eq) = isequiv.g eq equivlemma

------------------------------------------------------------------------------
-- Lemma 8.5.10

module ∑A≡Bool*A {A : Set} where
  open Suspension
  open Join

  f :  ∑ A → Bool * A
  f  = rec∑ (inl true)
            (inl false)
            (λ a → glue (true , a) ∘ ! (glue (false , a)))
  fmerid : (a : A) →
    ap f (merid a) ≡ glue (true , a) ∘ ! (glue (false , a))
  fmerid =
    βrec∑ (inl true)
          (inl false)
          (λ a → glue (true , a) ∘ ! (glue (false , a)))

  g : Bool * A → ∑ A
  g = rec* (λ b → if b then N else S)
           (λ a → S)
           (λ c → indBool (λ b → (if b then N else S) ≡ S)
                          (merid (proj₂ c))
                          (refl S)
                          (proj₁ c))

  fg = f · g
  gf = g · f

  gglue-true : (a : A) → (ap g (glue (true , a))) ≡ merid a
  gglue-true a =
    βrec* (λ b → if b then N else S)
          (λ a → S)
          (λ c → indBool (λ b → (if b then N else S) ≡ S)
                         (merid (proj₂ c))
                         (refl S)
                         (proj₁ c))
          (true , a)

  gglue-false : (a : A) → (ap g (glue (false , a))) ≡ refl S
  gglue-false a =
    βrec* (λ b → if b then N else S)
          (λ a → S)
          (λ c → indBool (λ b → (if b then N else S) ≡ S)
                         (merid (proj₂ c))
                         (refl S)
                         (proj₁ c))
          (false , a)

  α : (f · g) ∼ id
  α  = ind* (indBool (λ b → fg (inl b) ≡ id (inl b))
                     (refl (inl true))
                     (refl (inl false)))
            (λ a → glue (false , a))
            (λ c →
              ind×
              (λ b a →
                indBool
                 (λ b →
                   transport
                    (λ z → fg z ≡ id z)
                       (glue (b , a))
                       (indBool (λ b₁ → fg (inl b₁) ≡ id (inl b₁))
                                (refl (inl true))
                                (refl (inl false))
                                b)
                   ≡ glue (false , a))
                 -- big α equivalence proof 1
                 (transport (λ z → fg z ≡ id z)
                            (glue (true , a))
                            (refl (inl true))
                   ≡⟨ transportId fg id (glue (true , a))
                                        (refl (inl true)) ⟩
                 ((! (ap fg (glue (true , a))))
                  ∘ (refl (inl true))
                  ∘ ap id (glue (true , a)))
                   ≡⟨ ap (λ p → ((! (ap fg (glue (true , a))))
                                 ∘ (refl (inl true))
                                 ∘ p))
                         (apfId (glue (true , a))) ⟩
                 ((! (ap fg (glue (true , a))))
                  ∘ (refl (inl true))
                  ∘ (glue (true , a)))
                   ≡⟨ ap (λ p → ((! (ap fg (glue (true , a)))) ∘ p))
                         (unitTransL (glue (true , a))) ⟩
                 ((! (ap (f · g) (glue (true , a))))
                  ∘ (glue (true , a)))
                   ≡⟨ ap (λ p → ((! p) ∘ (glue (true , a))))
                         (! (apfComp g f (glue (true , a)))) ⟩
                 ((! (ap f (ap g (glue (true , a)))))
                  ∘ (glue (true , a)))
                   ≡⟨ ap (λ p → (! (ap f p)) ∘ (glue (true , a)))
                         (gglue-true a) ⟩
                 ((! (ap f (merid a))) ∘ (glue (true , a)))
                   ≡⟨ ap (λ p → (! p) ∘ (glue (true , a)))
                         (fmerid a) ⟩
                 ((! (glue (true , a) ∘ ! (glue (false , a))))
                  ∘ (glue (true , a)))
                   ≡⟨ ap (λ p → (p ∘ (glue (true , a))))
                         (invComp (glue (true , a))
                                  (! (glue (false , a)))) ⟩
                 ((! (! (glue (false , a)))) ∘ (! (glue (true , a))))
                  ∘ (glue (true , a))
                   ≡⟨ ! (assocP (! (! (glue (false , a))))
                                (! (glue (true , a)))
                                (glue (true , a))) ⟩
                 (! (! (glue (false , a))))
                 ∘ ((! (glue (true , a))) ∘ (glue (true , a)))
                   ≡⟨ ap (λ p → (! (! (glue (false , a)))) ∘ p)
                          (invTransL (glue (true , a))) ⟩
                 (! (! (glue (false , a)))) ∘ (refl (inr a))
                   ≡⟨ ! (unitTransR (! (! (glue (false , a))))) ⟩
                 (! (! (glue (false , a))))
                   ≡⟨ (invId (glue (false , a))) ⟩
                 (glue (false , a)) ∎)
                 -- big α equivalence proof 2
                 ((transport (λ z → fg z ≡ id z)
                                (glue (false , a))
                                (refl (inl false))
                   ≡⟨ transportId fg id (glue (false , a))
                                        (refl (inl false)) ⟩
                  ((! (ap fg (glue (false , a))))
                   ∘ (refl (inl false))
                   ∘ ap id (glue (false , a)))
                   ≡⟨ ap (λ p → (! (ap fg (glue (false , a))))
                                ∘ (refl (inl false))
                                ∘ p)
                         (apfId (glue (false , a))) ⟩
                 ((! (ap fg (glue (false , a))))
                  ∘ ((refl (inl false))
                     ∘ (glue (false , a))))
                   ≡⟨ ap (λ p → (! (ap fg (glue (false , a)))) ∘ p)
                         (unitTransL (glue (false , a))) ⟩
                 (! (ap (f · g) (glue (false , a))))
                  ∘ (glue (false , a))
                   ≡⟨ ! (ap (λ p → (! p) ∘ (glue (false , a)))
                            (apfComp g f (glue (false , a)))) ⟩
                 (! (ap f (ap g (glue (false , a)))))
                  ∘ (glue (false , a))
                   ≡⟨ ap (λ p → (! (ap f p)) ∘ (glue (false , a)))
                         (gglue-false a) ⟩
                 (! (ap f (refl S))) ∘ (glue (false , a))
                   ≡⟨ C.refl ⟩
                 (refl (inl false)) ∘ (glue (false , a))
                   ≡⟨ unitTransL (glue (false , a)) ⟩
                 (glue (false , a)) ∎))
                 b)
               c)

--   fmerid : (a : A) →
--   ap f (merid a) ≡ glue (true , a) ∘ ! (glue (false , a))

  β : (g · f) ∼ id
  β = ind∑
       (refl N)
       (refl S)
       (λ a →
         transport (λ z → gf z ≡ id z)
                   (merid a)
                   (refl N)
            ≡⟨ transportId gf id (merid a) (refl N) ⟩
         ((! (ap gf (merid a))) ∘ (refl N) ∘ ap id (merid a))
           ≡⟨ ap (λ p → ((! (ap gf (merid a))) ∘ (refl N) ∘ p))
                 (apfId (merid a)) ⟩
         ((! (ap gf (merid a))) ∘ (refl N) ∘ (merid a))
            ≡⟨ ap (λ p → (! (ap gf (merid a))) ∘ p)
                  (! (unitTransL (merid a))) ⟩
         ((! (ap (g · f) (merid a))) ∘ (merid a))
            ≡⟨ ap (λ p → (! p) ∘ (merid a))
                  (! (apfComp f g (merid a))) ⟩
         ((! (ap g (ap f (merid a)))) ∘ (merid a))
            ≡⟨ ap (λ p → ((! (ap g p)) ∘ (merid a)))
                  (fmerid a) ⟩
         ((! (ap g (glue (true , a) ∘ ! (glue (false , a))))) ∘ (merid a))
            ≡⟨ ap (λ p → (! p) ∘ (merid a))
                  (apfTrans g (glue (true , a)) (! (glue (false , a)))) ⟩
         ((! ((ap g (glue (true , a))) ∘ (ap g (! (glue (false , a)))))) ∘ (merid a))
            ≡⟨ ap (λ p → ((! (p ∘ (ap g (! (glue (false , a)))))) ∘ (merid a)))
                  (gglue-true a) ⟩
         ((! ((merid a) ∘ (ap g (! (glue (false , a)))))) ∘ (merid a))
            ≡⟨ ap (λ p → ((! ((merid a) ∘ p)) ∘ (merid a)))
                  (apfInv g (glue (false , a))) ⟩
         ((! ((merid a) ∘ (! (ap g (glue (false , a)))))) ∘ (merid a))
            ≡⟨ ap (λ p → ((! ((merid a) ∘ (! p))) ∘ (merid a)))
                  (gglue-false a) ⟩
         ((! ((merid a) ∘ (! (refl S)))) ∘ (merid a))
            ≡⟨ C.refl ⟩
         ((! ((merid a) ∘ (refl S))) ∘ (merid a))
            ≡⟨ ap (λ p → (! p) ∘ (merid a))
                  (! (unitTransR (merid a))) ⟩
         ((! (merid a)) ∘ (merid a))
            ≡⟨ invTransL (merid a) ⟩
         refl S ∎)

  ΣA≃Bool*A : ∑ A ≃ Bool * A
  ΣA≃Bool*A = (f , iso (mkqinv g α β))

  lemma : ∑ A ≡ Bool * A
  lemma with univalence
  ... | (_ , eq) = isequiv.g eq ΣA≃Bool*A

------------------------------------------------------------------------------
-- Lemma 8.5.9

module JoinAssoc where
  open Join

  lemma : {A B C : Set} → (A * B) * C ≡ A * (B * C)
  lemma {A} {B} {C} = {!!}

------------------------------------------------------------------------------
-- Thm 8.5.11

open Circle
open Suspension
open Join

S² S³ : Set
S² = ∑ S¹
S³ = ∑ S²

-- Proof of the main theorem

S¹*S¹≡S³ : S¹ * S¹ ≡ S³
S¹*S¹≡S³ =
      (S¹ * S¹
          ≡⟨ P.cong (λ a → a * S¹) (! ∑Bool≡S¹.lemma) ⟩
         ∑ Bool * S¹
          ≡⟨ P.cong (λ a → a * S¹) ∑A≡Bool*A.lemma ⟩
         (Bool * Bool) * S¹
          ≡⟨ JoinAssoc.lemma ⟩
         Bool * (Bool * S¹)
          ≡⟨ P.cong (λ b → Bool * b) (! ∑A≡Bool*A.lemma) ⟩
         Bool * S²
          ≡⟨ ! ∑A≡Bool*A.lemma ⟩
         S³ ∎)

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

max_stars_repo_name: andmkent/misc-HoTT

max_issues_repo_name: andmkent/misc-HoTT

max_forks_repo_name: andmkent/misc-HoTT


text:
-- Properties involving susbets and membership
-- between sets.

module sv20.assign2.SetTheory.Subset where

open import sv20.assign2.SetTheory.Logic
open import sv20.assign2.SetTheory.ZAxioms

memberEq : (x y z : 𝓢) → x ∈ y ∧ y ≡ z → x ∈ z
memberEq x y z (x₁ , x₂) = subs _ x₂ x₁

-- Theorem 1, p. 21 (Suppes 1960)
notInEmpty : ∀ x → x ∉ ∅
notInEmpty x h  = (proj₂ _ empt) x h

prop-∅ : (x A : 𝓢) → x ∈ A → A ≢ ∅
prop-∅ x A x∈A h = notInEmpty x (subs _ h x∈A)

prop₂-∅ : (x : 𝓢) → ∃ (λ y → y ∈ x) → x ≢ ∅
prop₂-∅ x h₁ h₂ = cont _ (h₂ , prop-∅ _ _ aux-p)
  where
  aux : 𝓢
  aux = proj₁ h₁

  aux-p : aux ∈ x
  aux-p = proj₂ _ h₁

-- Theorem 3, p. 22 (Suppes 1960)
subsetOfItself : ∀ {x} → x ⊆ x
subsetOfItself _ t∈x = t∈x

-- Theorem 4, p. 22 (Suppes 1960)
equalitySubset :  (x y : 𝓢) → x ⊆ y ∧ y ⊆ x → x ≡ y
equalitySubset x y (x⊆y , y⊆x) = ext x y ((x⊆y x) , (y⊆x x))

-- Theorem 6, p. 23 (Suppes 1960)
trans-⊆ : (x y z : 𝓢) → x ⊆ y ∧ y ⊆ z → x ⊆ z
trans-⊆ x y z (x⊆y , y⊆z) t t∈x = y⊆z t (x⊆y t t∈x)

-- Theorem 7, p. 23 (Suppes 1960)
notContainedInItself : ∀ {x} → ¬ (x ⊂ x)
notContainedInItself (_ , x≢x) = x≢x refl

-- Theorem 8, p. 23 (Suppes 1960)
nonSymmetry-⊂ : (x y : 𝓢) (p : x ⊂ y) → ¬ (y ⊂ x)
nonSymmetry-⊂ x y (x⊆y , x≢y) (y⊆x , _) = x≢y (equalitySubset x y (x⊆y , y⊆x))

-- Theorem 10, p. 23 (Suppes 1960)
⊂→⊆ : ∀ {x y} → x ⊂ y → x ⊆ y
⊂→⊆ (x⊆y , _) z z∈x = x⊆y z z∈x

prop-⊆ : (x A B : 𝓢) → x ∈ A → A ⊆ B → x ∈ B
prop-⊆ x A B x₁ x₂ = i x₁
  where
  i : x ∈ A → x ∈ B
  i = x₂ _

-- References
--
-- Suppes, Patrick (1960). Axiomatic Set Theory.
-- The University Series in Undergraduate Mathematics.
-- D. Van Nostrand Company, inc.
--
-- Enderton, Herbert B. (1977). Elements of Set Theory.
-- Academic Press Inc.


text:
module NaturalAndLevelDifferent where

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

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN LEVEL   ℕ #-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --allow-unsolved-metas #-}

-- {-# OPTIONS -v tc.rewrite:25 -v tc.with:40 --show-implicit #-}
-- {-# OPTIONS -v tc:100 #-}

-- Andreas, 2014-05-17, reported by Fabien Renaud.
-- Error in reification of interaction metas
-- leading to strange error messages for rewrite.

module _ where

open import Common.Prelude
open import Common.Equality

postulate comm : ∀{n m} → n + m ≡ m + n

-- module With where

--   foo : ∀{x y} → x + (x + y) ≡ x + (y + x)
--   foo {x} {y} with x + y | comm {x} {y}
--   foo | ._ | refl = refl

test0 : ∀{x y} → x + (x + y) ≡ x + (y + x)
test0 rewrite comm {n = {!!}} {m = {!!}} = {!!}

test : ∀{x y} → x + (x + y) ≡ x + (y + x)
test {x}{y} rewrite comm {n = {!!}} {m = {!!}} = {!!}

-- Error WAS:
-- .Agda.Primitive.Level !=< Nat of type Set
-- when checking that the expression ?0 has type Nat

-- Now this type checks.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K #-}
open import Type
open import Type.Identities
open import Level.NP
open import Data.Two
open import Function
open import Function.Extensionality
open import Data.Product
open import Data.Sum
open import Data.Fin
open import Relation.Binary.PropositionalEquality.NP using (_≡_; refl; !_; _∙_)
open import Relation.Binary.Sum
open import HoTT

open import Explore.Sum
open import Explore.Core
open import Explore.Properties
open import Explore.Explorable

module Explore.Two where

module _ {ℓ} where
    𝟚ᵉ : Explore ℓ 𝟚
    𝟚ᵉ _ _∙_ f = f 0₂ ∙ f 1₂

    𝟚ⁱ : ∀ {p} → ExploreInd p 𝟚ᵉ
    𝟚ⁱ _ _ _P∙_ Pf = Pf 0₂ P∙ Pf 1₂

module _ {ℓ₁ ℓ₂ ℓᵣ} {R : 𝟚 → 𝟚 → ★₀} {r0 : R 0₂ 0₂}{r1 : R 1₂ 1₂} where
    ⟦𝟚ᵉ⟧ : ⟦Explore⟧ {ℓ₁} {ℓ₂} ℓᵣ R 𝟚ᵉ 𝟚ᵉ
    ⟦𝟚ᵉ⟧ _ _ _∙ᵣ_ fᵣ = fᵣ r0 ∙ᵣ fᵣ r1

module 𝟚ⁱ = FromExploreInd 𝟚ⁱ
open 𝟚ⁱ public using ()
  renaming (sum to 𝟚ˢ
           ;product to 𝟚ᵖ
           ;reify to 𝟚ʳ
           ;unfocus to 𝟚ᵘ
           )

module _ {ℓ} where
    module _ {{_ : UA}}{{_ : FunExt}} where
        Σᵉ𝟚-ok : Adequate-Σ {ℓ} (Σᵉ 𝟚ᵉ)
        Σᵉ𝟚-ok _ = ! Σ𝟚-⊎

        Πᵉ𝟚-ok : Adequate-Π {ℓ} (Πᵉ 𝟚ᵉ)
        Πᵉ𝟚-ok _ = ! Π𝟚-×

    𝟚ˡ : Lookup {ℓ} 𝟚ᵉ
    𝟚ˡ = proj

    𝟚ᶠ : Focus {ℓ} 𝟚ᵉ
    𝟚ᶠ (0₂ , x) = inj₁ x
    𝟚ᶠ (1₂ , x) = inj₂ x

explore𝟚     = 𝟚ᵉ
explore𝟚-ind = 𝟚ⁱ
lookup𝟚      = 𝟚ˡ
reify𝟚       = 𝟚ʳ
focus𝟚       = 𝟚ᶠ
unfocus𝟚     = 𝟚ᵘ
sum𝟚         = 𝟚ˢ

module _ {{_ : UA}}{{_ : FunExt}} where
    open Adequacy _≡_
    𝟚ˢ-ok : Adequate-sum 𝟚ˢ
    𝟚ˢ-ok f = ! (Σ𝟚-⊎ ∙ Fin-⊎-+)

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Membership for containers
------------------------------------------------------------------------

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

module Data.Container.Membership where

open import Level using (_⊔_)
open import Relation.Unary using (Pred)
open import Relation.Binary.PropositionalEquality

open import Data.Container.Core
open import Data.Container.Relation.Unary.Any

module _ {s p} {C : Container s p} {x} {X : Set x} where

  infix 4 _∈_
  _∈_ : X → Pred (⟦ C ⟧ X) (p ⊔ x)
  x ∈ xs = ◇ C (_≡_ x) xs


text:
{-# OPTIONS --cubical --safe #-}

module Data.Maybe.Properties where

open import Data.Maybe.Base
open import Prelude

fromMaybe : A → Maybe A → A
fromMaybe x = maybe x id

just-inj : ∀ {x y : A} → just x ≡ just y → x ≡ y
just-inj {x = x} = cong (fromMaybe x)

just≢nothing : {x : A} → just x ≢ nothing
just≢nothing p = subst (maybe ⊥ (const ⊤)) p tt

nothing≢just : {x : A} → nothing ≢ just x
nothing≢just p = subst (maybe ⊤ (const ⊥)) p tt

discreteMaybe : Discrete A → Discrete (Maybe A)
discreteMaybe _≟_ nothing nothing = yes refl
discreteMaybe _≟_ nothing (just x) = no nothing≢just
discreteMaybe _≟_ (just x) nothing = no just≢nothing
discreteMaybe _≟_ (just x) (just y) = ⟦yes cong just ,no just-inj ⟧ (x ≟ y)

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

open import Base
import Homotopy.TruncationHIT as T

{-
The definition of the truncation is in TruncationHIT, here I just make some
arguments implicit, define easier to use helper functions and prove the
universal property
-}

module Homotopy.Truncation {i} where

τ : (n : ℕ₋₂) → (Set i → Set i)
τ = T.τ

proj : {n : ℕ₋₂} {A : Set i} → (A → τ n A)
proj {n} {A} = T.proj n A

τ-is-truncated : (n : ℕ₋₂) (A : Set i) → is-truncated n (τ n A)
τ-is-truncated = T.τ-is-truncated

τ-is-truncated#instance : {n : ℕ₋₂} {A : Set i} → is-truncated n (τ n A)
τ-is-truncated#instance = T.τ-is-truncated _ _

τ-extend : ∀ {j} {n : ℕ₋₂} {A : Set i} {P : (τ n A) → Set j}
  ⦃ p : (x : τ n A) → is-truncated n (P x) ⦄ (f : (x : A) → P (proj x))
  → ((x : τ n A) → P x)
τ-extend {j} {n} {A} {P} ⦃ p ⦄ f = T.τ-rec _ _ _ f {transp} p where
  abstract
    transp : (pa : n ≡ ⟨-2⟩) (x y : τ n A) (x* : P x) (y* : P y)
      → transport P (T.hack-prop n A pa x y) x* ≡ y*
    transp pa x y x* y* = π₁ (contr-is-prop
                               (transport (λ m → is-truncated m _) pa (p y))
                              _ _)

τ-extend-nondep : ∀ {j} {n : ℕ₋₂} {A : Set i} {B : Set j}
  ⦃ p : is-truncated n B ⦄ → ((f : A → B) → (τ n A → B))
τ-extend-nondep {j} {n} {A} {B} ⦃ p ⦄ f = T.τ-rec-nondep _ _ _ f {transp} p
  where
  abstract
    transp : (pa : n ≡ ⟨-2⟩) (x y : τ n A) (x* y* : B) → x* ≡ y*
    transp pa x y x* y* = π₁ (contr-is-prop
                               (transport (λ m → is-truncated m _) pa p)
                              _ _)

-- Special syntax for hProp-reflection

[_] : Set i → Set i
[_] = τ ⟨-1⟩

abstract
  []-is-prop : {A : Set i} → is-prop [ A ]
  []-is-prop = T.τ-is-truncated _ _

[]-extend : ∀ {j} {A : Set i} {P : [ A ] → Set j}
  ⦃ p : (x : [ A ]) → is-prop (P x) ⦄ (f : (x : A) → P (proj x))
  → ((x : [ A ]) → P x)
[]-extend f = τ-extend f

[]-extend-nondep : ∀ {j} {A : Set i} {B : Set j} ⦃ p : is-prop B ⦄
  → ((f : A → B) → ([ A ] → B))
[]-extend-nondep f = τ-extend-nondep f

-- Special syntax for hSet-reflection

π₀ : Set i → Set i
π₀ = τ ⟨0⟩

π₀-is-set : (A : Set i) → is-set (π₀ A)
π₀-is-set A = T.τ-is-truncated _ _

π₀-extend : ∀ {j} {A : Set i} {P : π₀ A → Set j}
  ⦃ p : (x : π₀ A) → is-set (P x) ⦄ (f : (x : A) → P (proj x))
  → ((x : π₀ A) → P x)
π₀-extend f = τ-extend f

π₀-extend-nondep : ∀ {j} {A : Set i} {B : Set j} ⦃ p : is-set B ⦄
  → ((f : A → B) → (π₀ A → B))
π₀-extend-nondep f = τ-extend-nondep f

-- Universal property of the truncation

abstract
  τ-up : ∀ {j} (n : ℕ₋₂) (A : Set i) (B : Set j)
    ⦃ p : is-truncated n B ⦄
    → is-equiv (λ (f : τ n A → B) → (λ x → f (proj x)))
  τ-up n A B ⦃ p ⦄ = iso-is-eq _
    (τ-extend-nondep)
    (λ _ → refl)
    (λ f → funext (τ-extend ⦃ p = λ x → ≡-is-truncated n p ⦄
                             (λ x → refl)))

  τ-extend-nondep-is-equiv : ∀ {j} (n : ℕ₋₂) (A : Set i) (B : Set j)
    ⦃ p : is-truncated n B ⦄ → is-equiv (τ-extend-nondep {n = n} {A} {B})
  τ-extend-nondep-is-equiv n A B ⦃ p ⦄ = iso-is-eq _
    (λ f → f ◯ proj)
    (λ f → funext (τ-extend ⦃ λ x → ≡-is-truncated n p ⦄
                                (λ x → refl)))
    (λ _ → refl)

-- Equivalence associated to the universal property
τ-equiv : ∀ {j} (n : ℕ₋₂) (A : Set i) (B : Set j)
  ⦃ p : is-truncated n B ⦄ → (τ n A → B) ≃ (A → B)
τ-equiv n A B = (_ , τ-up n _ _)

-- Equivalence associated to the universal property
τ-extend-equiv : ∀ {j} (n : ℕ₋₂) (A : Set i) (B : Set j)
  ⦃ p : is-truncated n B ⦄ → (A → B) ≃ (τ n A → B)
τ-extend-equiv n A B = (τ-extend-nondep , τ-extend-nondep-is-equiv n A B)

τ-fmap : {n : ℕ₋₂} {A B : Set i} → ((A → B) → (τ n A → τ n B))
τ-fmap f = τ-extend-nondep (proj ◯ f)

τ-fpmap : {n : ℕ₋₂} {A B : Set i} {f g : A → B} (h : (a : A) → f a ≡ g a)
  → ((a : τ n A) → τ-fmap f a ≡ τ-fmap g a)
τ-fpmap h = τ-extend ⦃ λ _ → ≡-is-truncated _ (τ-is-truncated _ _) ⦄
              (ap proj ◯ h)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Lists where

open import Nats
open import Bools

open import Agda.Builtin.List public
  using (List; []; _∷_)

infixr 5 _++_ _∷ʳ_

[_] : ∀ {a} {A : Set a} → A → List A
[ x ] = x ∷ []

_++_ : ∀ {a} {A : Set a} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

_∷ʳ_ : ∀ {a} {A : Set a} → List A → A → List A
xs ∷ʳ x = xs ++ [ x ]

null : ∀ {a} {A : Set a} → List A → 𝔹
null []       = true
null (x ∷ xs) = false

reverse : ∀ {a} {A : Set a} → List A → List A
reverse [] = []
reverse (x ∷ xs) = reverse xs ∷ʳ x

replicate : ∀ {a} {A : Set a} → (n : ℕ) → A → List A
replicate zero    x = []
replicate (suc n) x = x ∷ replicate n x


text:
module HelloWorld where

open import IO
open import Data.String
open import Data.Unit

main = run (putStrLn "Hello World!")


text:
open import MJ.Types as Types
import MJ.Classtable.Core as Core

module MJ.Semantics.Environments {c}(Ct : Core.Classtable c) where

open import Prelude
open import Data.List
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.All as All
open import Data.List.Relation.Unary.Any

open import MJ.LexicalScope c

{-
We equip MJ with mutable lexical environments.
We could choose to model this directly, moving the environment from
the Reader part of the evaluation monad to the State part.

Instead we choose to keep our environments immutable and model
mutability of the values in it by an indirection via the mutable store.
This greatly simplifies the treatment of environments in the interpreter
and keeps the representation lightweight, even though we support block scopes.
-}
Env : ∀ (Γ : Ctx)(W : World c) → Set
Env Γ W = All (λ a → vty a ∈ W) Γ

_⊕_ : ∀ {Γ W a} → Env Γ W → (vty a) ∈ W → Env (Γ +local a) W
_⊕_ E v = v ∷ E

open import Data.List.Any
getvar : ∀ {Γ W a} → Var Γ a → Env Γ W → vty a ∈ W
getvar px E = All.lookup E px


text:
------------------------------------------------------------------------------
-- ABP Lemma 2
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

-- From Dybjer and Sander's paper: The second lemma states that given
-- a state of the latter kind (see Lemma 1) we will arrive at a new
-- start state, which is identical to the old start state except that
-- the bit has alternated and the first item in the input stream has
-- been removed.

module FOTC.Program.ABP.Lemma2ATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.Loop
open import FOTC.Data.Bool
open import FOTC.Data.Bool.PropertiesATP
  using ( not-x≢x
        ; not-involutive
        )
open import FOTC.Data.List
open import FOTC.Program.ABP.ABP
open import FOTC.Program.ABP.Fair.Type
open import FOTC.Program.ABP.Fair.PropertiesATP
open import FOTC.Program.ABP.Terms

------------------------------------------------------------------------------
-- 30 November 2013. If we don't have the following definitions
-- outside the where clause, the ATPs cannot prove the theorems.

ds^ : D → D → D
ds^ cs' os₂^ = corrupt os₂^ · cs'
{-# ATP definition ds^ #-}

as^ : D → D → D → D → D → D
as^ b i' is' cs' os₂^ = await b i' is' (ds^ cs' os₂^)
{-# ATP definition as^ #-}

bs^ : D → D → D → D → D → D → D
bs^ b i' is' cs' os₁^ os₂^ = corrupt os₁^ · as^ b i' is' cs' os₂^
{-# ATP definition bs^ #-}

cs^ : D → D → D → D → D → D → D
cs^ b i' is' cs' os₁^ os₂^ = ack (not b) · bs^ b i' is' cs' os₁^ os₂^
{-# ATP definition cs^ #-}

os₁^ : D → D
os₁^ os₁' = tail₁ os₁'
{-# ATP definition os₁^ #-}

os₂^ : D → D → D
os₂^ ft₂ os₂'' = ft₂ ++ os₂''
{-# ATP definition os₂^ #-}

-- Helper function for Lemma 2.
helper₂ : ∀ {b i' is' os₁' os₂' as' bs' cs' ds' js'} →
          Bit b →
          Fair os₁' →
          S' b i' is' os₁' os₂' as' bs' cs' ds' js' →
          ∀ ft₂ os₂'' → F*T ft₂ → Fair os₂'' → os₂' ≡ ft₂ ++ os₂'' →
          ∃[ os₁'' ] ∃[ os₂'' ] ∃[ as'' ] ∃[ bs'' ] ∃[ cs'' ] ∃[ ds'' ]
            Fair os₁''
            ∧ Fair os₂''
            ∧ S (not b) is' os₁'' os₂'' as'' bs'' cs'' ds'' js'
helper₂ {b} {i'} {is'} {js' = js'} Bb Fos₁' s'
       .(T ∷ []) os₂'' f*tnil Fos₂'' os₂'-eq = prf
  where
  postulate
    prf : ∃[ os₁'' ] ∃[ os₂'' ] ∃[ as'' ] ∃[ bs'' ] ∃[ cs'' ] ∃[ ds'' ]
          Fair os₁''
          ∧ Fair os₂''
          ∧ as'' ≡ send (not b) · is' · ds''
          ∧ bs'' ≡ corrupt os₁'' · as''
          ∧ cs'' ≡ ack (not b) · bs''
          ∧ ds'' ≡ corrupt os₂'' · cs''
          ∧ js'  ≡ out (not b) · bs''
  {-# ATP prove prf #-}

helper₂ {b} {i'} {is'} {os₁'} {os₂'} {as'} {bs'} {cs'} {ds'} {js'}
        Bb Fos₁' s'
        .(F ∷ ft₂) os₂'' (f*tcons {ft₂} FTft₂) Fos₂'' os₂'-eq =
        helper₂ Bb (tail-Fair Fos₁') ihS' ft₂ os₂'' FTft₂ Fos₂'' refl
  where
  postulate os₂'-eq-helper : os₂' ≡ F ∷ os₂^ ft₂ os₂''
  {-# ATP prove os₂'-eq-helper #-}

  postulate ds'-eq : ds' ≡ error ∷ ds^ cs' (os₂^ ft₂ os₂'')
  {-# ATP prove ds'-eq os₂'-eq-helper #-}

  postulate as'-eq : as' ≡ < i' , b > ∷ as^ b i' is' cs' (os₂^ ft₂ os₂'')
  {-# ATP prove as'-eq #-}

  postulate
    bs'-eq : bs' ≡ ok < i' , b > ∷ bs^ b i' is' cs' (os₁^ os₁') (os₂^ ft₂ os₂'')
               ∨ bs' ≡ error ∷ bs^ b i' is' cs' (os₁^ os₁') (os₂^ ft₂ os₂'')
  {-# ATP prove bs'-eq as'-eq head-tail-Fair #-}

  postulate
    cs'-eq-helper₁ :
      bs' ≡ ok < i' , b > ∷ bs^ b i' is' cs' (os₁^ os₁') (os₂^ ft₂ os₂'') →
      cs' ≡ b ∷ cs^ b i' is' cs' (os₁^ os₁') (os₂^ ft₂ os₂'')
  {-# ATP prove cs'-eq-helper₁ not-x≢x not-involutive #-}

  postulate
    cs'-eq-helper₂ :
      bs' ≡ error ∷ bs^ b i' is' cs' (os₁^ os₁') (os₂^ ft₂ os₂'') →
      cs' ≡ b ∷ cs^ b i' is' cs' (os₁^ os₁') (os₂^ ft₂ os₂'')
  {-# ATP prove cs'-eq-helper₂ not-involutive #-}

  cs'-eq : cs' ≡ b ∷ cs^ b i' is' cs' (os₁^ os₁') (os₂^ ft₂ os₂'')
  cs'-eq = case cs'-eq-helper₁ cs'-eq-helper₂ bs'-eq

  postulate
    js'-eq : js' ≡ out (not b) · bs^ b i' is' cs' (os₁^ os₁') (os₂^ ft₂ os₂'')
  -- TODO (21 November 2014). See Apia issue 16
  -- {-# ATP prove js'-eq not-x≢x bs'-eq #-}

  postulate
    ds^-eq : ds^ cs' (os₂^ ft₂ os₂'') ≡
             corrupt (os₂^ ft₂ os₂'') ·
               (b ∷ cs^ b i' is' cs' (os₁^ os₁') (os₂^ ft₂ os₂''))
  {-# ATP prove ds^-eq cs'-eq #-}

  ihS' : S' b i' is'
            (os₁^ os₁')
            (os₂^ ft₂ os₂'')
            (as^ b i' is' cs' (os₂^ ft₂ os₂''))
            (bs^ b i' is' cs' (os₁^ os₁') (os₂^ ft₂ os₂''))
            (cs^ b i' is' cs' (os₁^ os₁') (os₂^ ft₂ os₂''))
            (ds^ cs' (os₂^ ft₂ os₂''))
            js'
  ihS' = refl , refl , refl , ds^-eq , js'-eq

-- From Dybjer and Sander's paper: From the assumption that
-- os₂' ∈ Fair and hence by unfolding Fair, we conclude that there are
-- ft₂ : F*T and os₂'' : Fair, such that os₂' = ft₂ ++ os₂''.
--
-- We proceed by induction on ft₂ : F*T using helper.

lemma₂ : ∀ {b i' is' os₁' os₂' as' bs' cs' ds' js'} →
         Bit b →
         Fair os₁' →
         Fair os₂' →
         S' b i' is' os₁' os₂' as' bs' cs' ds' js' →
         ∃[ os₁'' ] ∃[ os₂'' ] ∃[ as'' ] ∃[ bs'' ] ∃[ cs'' ] ∃[ ds'' ]
           Fair os₁''
           ∧ Fair os₂''
           ∧ S (not b) is' os₁'' os₂'' as'' bs'' cs'' ds'' js'
lemma₂ {b} {is' = is'} {os₂' = os₂'} {js' = js'} Bb Fos₁' Fos₂' s' =
  helper₁ (Fair-out Fos₂')
  where
  helper₁ : (∃[ ft₂ ] ∃[ os₂'' ] F*T ft₂ ∧ os₂' ≡ ft₂ ++ os₂'' ∧ Fair os₂'') →
            ∃[ os₁'' ] ∃[ os₂'' ] ∃[ as'' ] ∃[ bs'' ] ∃[ cs'' ] ∃[ ds'' ]
              Fair os₁''
              ∧ Fair os₂''
              ∧ S (not b) is' os₁'' os₂'' as'' bs'' cs'' ds'' js'
  helper₁ (ft₂ , os₂'' , FTft₂ , os₂'-eq , Fos₂'') =
    helper₂ Bb Fos₁' s' ft₂ os₂'' FTft₂ Fos₂'' os₂'-eq

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Rewrite-with-doubly-indexed-equality where

open import Common.Level

infix 4 _≡_

data _≡_ {a} {A : Set a} : A → A → Set a where
  refl : ∀ {x} → x ≡ x

{-# BUILTIN EQUALITY _≡_  #-}
{-# BUILTIN REFL     refl #-}

sym : {A : Set}{x y : A} → x ≡ y → y ≡ x
sym refl = refl

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

infixl 6 _+_

_+_ : Nat → Nat → Nat
zero  + m = m
suc n + m = suc (n + m)

plus-zero : ∀ n → n + zero ≡ n
plus-zero zero    = refl
plus-zero (suc n) rewrite plus-zero n = refl

plus-suc : ∀ n m → n + suc m ≡ suc (n + m)
plus-suc zero    m = refl
plus-suc (suc n) m rewrite plus-suc n m = refl

-- Proving things about functions using rewrite
data IsRefl {A : Set}{x : A} : ∀ {y} → x ≡ y → Set where
  isRefl : IsRefl refl

plus-suc-isrefl : ∀ {n m} → IsRefl (plus-suc n m)
plus-suc-isrefl {zero } {m} = isRefl
plus-suc-isrefl {suc n} {m} rewrite plus-suc n m = isRefl

-- Multiple rewrites
com : ∀ n m → n + m ≡ m + n
com n zero    = plus-zero _
com n (suc m) rewrite plus-suc n m
                    | com n m
              = refl

-- rewrite followed by with
thm : ∀ a b c → a + (b + c) ≡ (c + b) + a
thm a b c rewrite com b c with c + b
... | cb = com a cb

data List A : Set where
  [] : List A
  _∷_ : (x : A)(xs : List A) → List A

infixr 30 _∷_ _++_

_++_ : ∀ {A} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

-- rewrite in parameterised module
module ListProps {A : Set} where

  append-nil : (xs : List A) → xs ++ [] ≡ xs
  append-nil []       = refl
  append-nil (x ∷ xs) rewrite append-nil xs = refl

  append-assoc : (as bs cs : List A) → (as ++ bs) ++ cs ≡ as ++ (bs ++ cs)
  append-assoc []       bs cs = refl
  append-assoc (a ∷ as) bs cs rewrite append-assoc as bs cs = refl

  -- With implicit arguments
  append-assoc′ : ∀ (as : List A) {bs cs} → (as ++ bs) ++ cs ≡ as ++ (bs ++ cs)
  append-assoc′ []       = refl
  append-assoc′ (a ∷ as) {bs}{cs} rewrite append-assoc′ as {bs} {cs} = refl

  reverse : List A → List A
  reverse []       = []
  reverse (x ∷ xs) = reverse xs ++ x ∷ []

  reverse-append : ∀ as bs → reverse (as ++ bs) ≡ reverse bs ++ reverse as
  reverse-append []       bs rewrite append-nil (reverse bs) = refl
  reverse-append (a ∷ as) bs rewrite reverse-append as bs
                          = append-assoc (reverse bs) _ _

  reverse-reverse : ∀ as → reverse (reverse as) ≡ as
  reverse-reverse []       = refl
  reverse-reverse (a ∷ as) rewrite reverse-append (reverse as) (a ∷ [])
                                 | reverse-reverse as
                           = refl

open ListProps

map : ∀ {A B} → (A → B) → List A → List B
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

_∘_ : {A : Set}{B : A → Set}{C : ∀ x → B x → Set}
      (f : ∀ {x} (y : B x) → C x y)(g : ∀ x → B x)
      (x : A) → C x (g x)
(f ∘ g) x = f (g x)

id : {A : Set} → A → A
id x = x

map-id : ∀ {A} (xs : List A) → map id xs ≡ xs
map-id []       = refl
map-id (x ∷ xs) rewrite map-id xs = refl

map-compose : ∀ {A B C} (f : B → C)(g : A → B)(xs : List A) →
              map (f ∘ g) xs ≡ (map f ∘ map g) xs
map-compose f g []       = refl
map-compose f g (x ∷ xs) rewrite map-compose f g xs = refl

map-append : ∀ {A B} (f : A → B) (xs ys : List A) →
             map f (xs ++ ys) ≡ map f xs ++ map f ys
map-append f []       ys = refl
map-append f (x ∷ xs) ys rewrite map-append f xs ys = refl

map-reverse : ∀ {A B} (f : A → B) (xs : List A) →
              map f (reverse xs) ≡ reverse (map f xs)
map-reverse f []       = refl
map-reverse f (x ∷ xs) rewrite map-append f (reverse xs) (x ∷ [])
                             | map-reverse f xs
                       = refl

foldr : {A B : Set} → (A → B → B) → B → List A → B
foldr f z []       = z
foldr f z (x ∷ xs) = f x (foldr f z xs)

foldl : {A B : Set} → (B → A → B) → B → List A → B
foldl f z []       = z
foldl f z (x ∷ xs) = foldl f (f z x) xs

module FoldAssoc
  {A : Set}(_∙_ : A → A → A)
  (assoc : ∀ x y z → ((x ∙ y) ∙ z) ≡ (x ∙ (y ∙ z))) where

  smashr = foldr _∙_
  smashl = foldl _∙_

  foldr-append : ∀ ∅ z xs ys → (∀ x → (∅ ∙ x) ≡ x) →
                 smashr z (xs ++ ys) ≡ (smashr ∅ xs ∙ smashr z ys)
  foldr-append ∅ z []       ys idl = sym (idl _)
  foldr-append ∅ z (x ∷ xs) ys idl rewrite assoc x (smashr ∅ xs) (smashr z ys)
                                         | foldr-append ∅ z xs ys idl
                                   = refl

  foldl-plus : ∀ z₁ z₂ xs → smashl (z₁ ∙ z₂) xs ≡ (z₁ ∙ smashl z₂ xs)
  foldl-plus z₁ z₂ []       = refl
  foldl-plus z₁ z₂ (x ∷ xs) rewrite assoc z₁ z₂ x
                            = foldl-plus _ _ xs

  foldr=foldl : ∀ ∅ → (∀ x → (∅ ∙ x) ≡ (x ∙ ∅)) →
                ∀ xs → foldr _∙_ ∅ xs ≡ foldl _∙_ ∅ xs
  foldr=foldl ∅ id []       = refl
  foldr=foldl ∅ id (x ∷ xs) rewrite id x
                                  | foldl-plus x ∅ xs
                                  | foldr=foldl ∅ id xs
                            = refl

foldr-compose : ∀ {A B C : Set} (f : B → C → C) (z : C) (g : A → B) (xs : List A) →
                foldr (f ∘ g) z xs ≡ foldr f z (map g xs)
foldr-compose f z g []       = refl
foldr-compose f z g (x ∷ xs) rewrite foldr-compose f z g xs = refl

foldr-fusion : ∀ {A B C : Set} (f : B → C) (_⊕_ : A → B → B) (_⊗_ : A → C → C) (z : B) →
               (∀ x y → f (x ⊕ y) ≡ (x ⊗ f y)) →
               ∀ xs → f (foldr _⊕_ z xs) ≡ foldr _⊗_ (f z) xs
foldr-fusion f _⊕_ _⊗_ z distr []       = refl
foldr-fusion f _⊕_ _⊗_ z distr (x ∷ xs)
  rewrite sym (foldr-fusion f _⊕_ _⊗_ z distr xs)
  with    foldr _⊕_ z xs
...  |    y = distr x y


text:
-- | The core type system.
module Ethambda.System where

open import Ethambda.Common using () -- ((<.>), (<.))

data Tp : Type -> Type where
  Var : a -> Tp a
  Fun : Tp a -> Tp a -> Tp a

Show a => Show (Tp a) where
  show t = case t of
    -- Var a => ?foo
    Var a => show a
    Fun a0 b0 => mbrackets a0 <+> "→" <+> show b0
  -- where
  --   brackets : String -> String
  --   brackets s = "(" <+> s <+> ")"
  --   mbrackets : Show a => Tp a -> String
  --   mbrackets a = case a of
  --     Var _   => neutral
  --     Fun _ _ => brackets (show a)

max_stars_repo_name: fredefox/ethambda-agda

max_issues_repo_name: fredefox/ethambda-agda

max_forks_repo_name: fredefox/ethambda-agda


text:
------------------------------------------------------------------------------
-- Properties for the relation _◁_
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Program.McCarthy91.WF-Relation.PropertiesATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesATP
  using ( x<y→y<x→⊥ )
open import FOTC.Data.Nat.Inequalities.PropertiesATP
  using ( x∸y<Sx
        ; <-trans
        ; x<x∸y→⊥
        ; x∸y<x∸z→Sx∸y<Sx∸z
        ; x<y→y≤z→x<z
        ; x∸Sy≤x∸y
        )
open import FOTC.Data.Nat.PropertiesATP
  using ( ∸-N
        ; S∸S
        )
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Data.Nat.UnaryNumbers.TotalityATP using ( 101-N )
open import FOTC.Program.McCarthy91.ArithmeticATP
open import FOTC.Program.McCarthy91.WF-Relation

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

◁-fn-N : ∀ {n} → N n → N (◁-fn n)
◁-fn-N Nn = ∸-N 101-N Nn

0◁x→⊥ : ∀ {n} → N n → ¬ (zero ◁ n)
0◁x→⊥ nzero 0◁n = prf
  where
  postulate prf : ⊥
  {-# ATP prove prf #-}

0◁x→⊥ (nsucc Nn) 0◁Sn = prf
  where
  postulate prf : ⊥
  {-# ATP prove prf ∸-N x∸y<Sx x<y→y<x→⊥ S∸S #-}

◁-trans : ∀ {m n o} → N m → N n → N o → m ◁ n → n ◁ o → m ◁ o
◁-trans Nm Nn No m◁n n◁o =
  <-trans (∸-N 101-N Nm) (∸-N 101-N Nn) (∸-N 101-N No) m◁n n◁o

Sx◁Sy→x◁y : ∀ {m n} → N m → N n → succ₁ m ◁ succ₁ n → m ◁ n
Sx◁Sy→x◁y nzero nzero S0◁S0 = prf
  where
  postulate prf : zero ◁ zero
  {-# ATP prove prf #-}

Sx◁Sy→x◁y nzero (nsucc {n} Nn) S0◁SSn = prf
  where
  postulate prf : zero ◁ succ₁ n
  {-# ATP prove prf x<x∸y→⊥ S∸S #-}

Sx◁Sy→x◁y (nsucc {m} Nm) nzero SSm◁S0 = prf
  where
  postulate prf : succ₁ m ◁ zero
  {-# ATP prove prf ∸-N x∸y<Sx S∸S #-}

Sx◁Sy→x◁y (nsucc {m} Nm) (nsucc {n} Nn) SSm◁SSn = prf
  where
  postulate prf : succ₁ m ◁ succ₁ n
  -- 2018-06-27: The ATPs could not prove the theorem (300 sec), but
  -- Vampire 4.2.2, via `online-atps`, could prove it.
  --
  {-# ATP prove prf x∸y<x∸z→Sx∸y<Sx∸z S∸S #-}

x◁Sy→x◁y : ∀ {m n} → N m → N n → m ◁ succ₁ n → m ◁ n
x◁Sy→x◁y {n = n} nzero Nn 0◁Sn = ⊥-elim (0◁x→⊥ (nsucc Nn) 0◁Sn)

x◁Sy→x◁y (nsucc {m} Nm) nzero Sm◁S0 = prf
   where
   postulate prf : succ₁ m ◁ zero
   {-# ATP prove prf x∸y<Sx S∸S #-}

x◁Sy→x◁y (nsucc {m} Nm) (nsucc {n} Nn) Sm◁SSn =
  x<y→y≤z→x<z (∸-N 101-N (nsucc Nm))
              (∸-N 101-N (nsucc (nsucc Nn)))
              (∸-N 101-N (nsucc Nn))
              Sm◁SSn
              (x∸Sy≤x∸y 101-N (nsucc Nn))


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

module Issue256 where

open import Imports.Level

const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A
const x = λ _ → x

level : ∀ {ℓ} → Set ℓ → Level
level {ℓ} _ = ℓ

-- termination check should fail for the following definition
ℓ : Level
ℓ = const zero (Set ℓ)

-- A : Set (suc {!ℓ!})
-- A = Set (level A)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
open import Prelude
open import core

module lemmas-ground where
  -- not ground types aren't hole to hole
  ground-arr-not-hole : ∀{τ} →
                      (τ ground → ⊥) →
                      (τ ≠ (⦇-⦈ ==> ⦇-⦈))
  ground-arr-not-hole notg refl = notg GHole

  -- not ground types either have to be hole or an arrow
  notground : ∀{τ} → (τ ground → ⊥) → (τ == ⦇-⦈) + (Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ] (τ == (τ1 ==> τ2)))
  notground {b} gnd = abort (gnd GBase)
  notground {⦇-⦈} gnd = Inl refl
  notground {b ==> b} gnd = Inr (b , b , refl)
  notground {b ==> ⦇-⦈} gnd = Inr (b , ⦇-⦈ , refl)
  notground {b ==> τ2 ==> τ3} gnd = Inr (b , τ2 ==> τ3 , refl)
  notground {⦇-⦈ ==> b} gnd = Inr (⦇-⦈ , b , refl)
  notground {⦇-⦈ ==> ⦇-⦈} gnd = abort (gnd GHole)
  notground {⦇-⦈ ==> τ2 ==> τ3} gnd = Inr (⦇-⦈ , τ2 ==> τ3 , refl)
  notground {(τ1 ==> τ2) ==> b} gnd = Inr (τ1 ==> τ2 , b , refl)
  notground {(τ1 ==> τ2) ==> ⦇-⦈} gnd = Inr (τ1 ==> τ2 , ⦇-⦈ , refl)
  notground {(τ1 ==> τ2) ==> τ3 ==> τ4} gnd = Inr (τ1 ==> τ2 , τ3 ==> τ4 , refl)

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda