text:
import Relation.Binary.PropositionalEquality as PE

module x01 where

import Data.Empty.Polymorphic as DEP
open import Data.Unit.Polymorphic
import Data.Maybe as Maybe

{-
Dependent Types at Work
Ana Bove and Peter Dybjer
Chalmers University of Technology, Göteborg, Sweden

intro to functional programming with dependent types

- simply typed functional programming in style of Haskell and ML
- discuss differences between Agda’s type system and Hindley-Milner type system of Haskell/ML
- how to use dependent types for programming
- explain ideas behind type-checking dependent types
- explain Curry-Howard identification of propositions and types
- show a method to encode partial/general recursive functions
  as total functions using dependent types

Dependent types are types that depend on elements of other types (e.g., Vec of length n)
Invariants can be expressed with dependent type (e.g., sorted list)

Agda's dependent type system is an extension of Martin-Löf type theory [20,21,22,25].

Parametrised types
- e.g., [A]
- usually not called dependent types
- they are are families of types indexed by other types
  - NOT families of types indexed by ELEMENTS of another type
- however, in dependent type theories, there is a type of small types (a universe),
  so that we have a type [A] of lists of elements of a given small type A.
- FORTRAN could define arrays of a given dimension, so a form a dependent type on small type
- simply typed lambda calculus and the Hindley-Milner type system,
  (e.g., Haskell/ML) do not include dependent types, only parametrised types
- polymorphic lambda calculus System F [15] has types like
  ∀X.A where X ranges over all types,
  but no quantification over ELEMENTS of other types

development of dependently typed programming languages has
origins in Curry-Howard isomorphism between propositions and types

1930’s : Curry noticed similarity between axioms of implicational logic
   P ⊃ Q ⊃ P                                (P ⊃ Q ⊃ R) ⊃ (P ⊃ Q) ⊃ P ⊃ R
and types of combinators
   K              and                       S
   A → B → A                                (A → B → C) → (A → B) → A → C

K can be viewed as a witness (i.e., proof object) of the truth of P ⊃ Q ⊃ P
S can be viewed as a withness of the truth of (P ⊃ Q ⊃ R) ⊃ (P ⊃ Q) ⊃ P ⊃ R

typing rule for application
corresponds to the inference rule modus ponens: from P ⊃ Q and P conclude Q
- f : A → B
- a : A
- f a → B

product types correspond to conjunctions
sum types (disjoint unions) to disjunctions

to extend this correspondence to predicate logic
Howard and de Bruijn introduced dependent types A(x) corresponding to predicates P(x).
They formed
indexed products Π x : D.A(x) : corresponding to universal   quantifications ∀x : D.P (x)
indexed sums     Σ x : D.A(x) :                  existential quantifications ∃x : D.P (x)

this gives a Curry-Howard interpretation of intuitionistic predicate logic

one-to-one correspondence between propositions and types
in a type system with dependent types

one-to-one correspondence between
- proofs of a certain proposition in constructive predicate logic, and
- terms of the corresponding type

To accommodate equality in predicate logic
introduce the type a == b of proofs that a and b are equal.
Gives a Curry-Howard interpretation of predicate logic with equality.

Can go further and add natural numbers with addition and multiplication
to obtain a Curry-Howard version of Heyting (intuitionistic) arithmetic.

Curry-Howard interpretation was basis for Martin-Löf’s intuitionistic type theory [20,21,22].
- propositions and types are identified
- intended to be a foundational system for constructive mathematics
- can also be used as a programming language [21]
- from 1980’s and onwards, systems implementing variants of Martin-Löf type theory
  - NuPRL [6] : implementing an extensional version of the theory
  - Coq [33]  : implementing an intensional impredicative version
  - Agda      : implements   an intensional predicative extension

About these Notes

Agda's type-checking algorithm
- Section 5
- ideas first presented by Coquand [7]
- more information
  - Norell’s thesis [26]
  - Abel, Coquand, and Dybjer [1,2]
  - Coquand, Kinoshita, Nordström, and Takeyama [8].

more complete understanding of dependent type theory
- read a book about Martin-Löf type theory and related systems
- Martin-Löf’s “Intuitionistic Type Theory” [22] is a classic
  - be aware that it describes an extensional version of the theory
- Nordström, Petersson, and Smith [25]
  description of the later intensional theory on which Agda is based
- variants of dependent type theory are
  - Thompson [34]
  - Constable et al     [6] : NuPRL
  - Bertot and Casteran [4] : Coq
- lecture notes (Agda wiki [3]) by Norell
  - collection of advanced examples of how to use Agda for dependently typed programming
- Geuvers’ lecture notes : introduction to type theory
  - including Barendregt’s pure type systems and important meta-theoretic properties
- Bertot’s notes : how dependent types (in Coq) can be used for
  implementing a number of concepts of programming language theory
  - focus on abstract interpretation
- Barthe, Grégoire, and Riba’s notes
  - method for making termination-checkers

Section 2 : ordinary functional programming
Section 3 : basic dependent types and shows how to use them
Section 4 : Curry-Howard isomorphism
Section 5 : aspects of type-checking and pattern matching with dependent types
Section 6 : use Agda as a programming logic
Section 7 : how to represent general recursion and partial functions as total functions in Agda

------------------------------------------------------------------------------
2 Simply Typed Functional Programming in Agda

2.1 Truth Values
-}
data Bool : Set where
  true  : Bool
  false : Bool
{-
states
- Bool is a data type with the two (no-arg) constructors
- “:” denotes type membership
- Bool is a member of the type Set
- Set
  - the type of sets (using a terminology introduced by Martin-Löf [22])
    or small types (mentioned in the introduction).
- Bool is a small type, but Set itself is not, it is a large type.
- allowing Set : Set, would make the system inconsistent
-}
not : Bool -> Bool
not true  = false
not false = true
{-
Agda cannot generally infer types.
Because Agda type-checking done via normalisation (simplification)
- without the normality restriction it may not terminate
-}
equiv : Bool -> Bool -> Bool
equiv false false = true
equiv  true false = false
equiv false  true = false
equiv  true  true = true

_||_ : Bool -> Bool -> Bool
true  || _     = true
false || true  = true
false || false = false
infixl 60 _||_

-- EXERCISE: Define some more truth functions, such as conjunction and implication/TODO.

_&&_ : Bool -> Bool -> Bool
false && _     = false
true  && false = false
true  && true  = true
-- infixl ?? _&&_

-- 2.2 Natural Numbers

-- such data types known as recursive in Haskell
-- in constructive type theory, referred to as inductive types or inductively defined types

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat
{-# BUILTIN NATURAL Nat #-}

pred : Nat -> Nat
pred  zero    = zero
pred (succ n) = n

_+_ : Nat -> Nat -> Nat
zero + m = m
succ n + m = succ (n + m)
{-# BUILTIN NATPLUS _+_ #-}

_*_ : Nat -> Nat -> Nat
zero   * n = zero
succ n * m = (n * m) + m
{-# BUILTIN NATTIMES _*_ #-}

infixl 6  _+_  _∸_
infixl 7  _*_

_ : (2 * 3) + 10 PE.≡ 16
_ = PE.refl
{-
+ and * are defined by PRIMITIVE RECURSION in FIRST ARG.
  - PRIMITIVE RECURSIION :
    - upper bound of number of iterations of every loop can be determined before entering loop
    - time complexity of PR functions bounded by the input size
- base case for zero
- step case for non zero defined recursively

Given a first order data type
- distinguish between
  - canonical form
    - built by constructors only
    - e.g., true, false,  zero, succ zero, succ (succ zero), ...
  - non-canonical forms
    - whereas non-canonical elements might contain defined functions
    - e.g., not true, zero + zero, zero * zero, succ (zero + zero)

Martin-Löf [21] instead considers lazy canonical forms
- a term begins with a constructor to be considered a canonical form
- e.g., succ (zero + zero) is a lazy canonical form, but not a “full” canonical form
- Lazy canonical forms are appropriate for lazy functional programming languages (e.g., Haskell)

-- EXERCISE: Write the cut-off subtraction function
-- the function on natural numbers, which returns 0
-- if the second argument is greater than or equal to the first.
-}
_∸_ : Nat -> Nat -> Nat
zero   ∸    _   = zero
succ n ∸ zero   = succ n
succ n ∸ succ m = n ∸ m

_ :  0 ∸  0 PE.≡  0
_ = PE.refl
_ :  0 ∸ 10 PE.≡  0
_ = PE.refl
_ : 10 ∸  0 PE.≡ 10
_ = PE.refl
_ : 10 ∸ 10 PE.≡  0
_ = PE.refl
_ : 10 ∸  9 PE.≡  1
_ = PE.refl

-- EXERCISE: Also write some more numerical functions like < or <=

_<_ : Nat -> Nat -> Bool
zero   < zero   = false
zero   < succ _ = true
succ _ < zero   = false
succ n < succ m = n < m

_ :  9 < 10 PE.≡ true
_ = PE.refl
_ : 10 < 10 PE.≡ false
_ = PE.refl

_<=_ : Nat -> Nat -> Bool
zero   <= zero   = true
zero   <= succ _ = true
succ _ <= zero   = false
succ n <= succ m = n <= m

_ :  9 <= 10 PE.≡ true
_ = PE.refl
_ : 10 <= 10 PE.≡ true
_ = PE.refl

_>_ : Nat -> Nat -> Bool
zero   > zero   = false
zero   > succ _ = false
succ _ > zero   = true
succ n > succ m = n > m

{-
2.3 Lambda Notation and Polymorphism

Agda is based on the typed lambda calculus.

APPLICATION is juxtaposition

lambda ABSTRACTION written either
- Curry-style (without a type label)
   \x -> e
- Church-style (with a type label)
  \(x : A) -> e

a family of identity functions, one for each small type:
-}
-- idE(xplicit)
idE :  (A : Set) ->       A  -> A
idE = \(A : Set) -> \(x : A) -> x
{-
apply this “generic” identity function id to a type argument A
to obtain the identity function from A to A

1st use of dependent types: type A -> A depends on variable A : Set
- ranging over the small types

Agda’s notation for dependent function types
- if A is a type and B[x] is a type which depends on (is indexed by) (x : A)
  then (x : A) -> B[x] is the type of functions f mapping arguments (x : A) to values f x : B[x].

If the type-checker can figure out value of an arg, can use a wild card character:
id _ x : A

K and S combinators in Agda (uses telescopic notation (A B : Set)
-}
K : (A B : Set) -> A -> B -> A
K _ _ x _     = x

S : (A B C : Set) -> (A -> B -> C) -> (A -> B) -> A -> C
S _ _ _ f g x = f x (g x)
{-
2.4 Implicit Arguments : declared by enclosing typings in curly brackets
-}

id : {A : Set} -> A -> A
id x = x

-- implicit arguments are omitted in applications
_ : id       zero PE.≡ zero
_ = PE.refl
-- can explicitly write an implicit argument by using curly brackets if needed
_ : id {Nat} zero PE.≡ zero
_ = PE.refl
_ : id {_}   zero PE.≡ zero
_ = PE.refl
{-
2.5 Gödel System T is a subsystem of Agda.

System of primitive recursive functionals [16]
- important in logic and a precursor to Martin-Löf type theory

recursion restricted to primitive recursion : to make sure programs terminate

Gödel System T
- based on simply typed lambda calculus
- with two base types : truth values and natural numbers
  - (some formulations code truth values as 0 and 1)
- constants for constructors true, false, zero
- conditional and primitive recursion combinators
-}

-- conditional
if_then_else_ : {C : Set} -> Bool -> C -> C -> C
if true  then x else _ = x
if false then _ else y = y

-- primitive recursion combinator for natural numbers
-- natrec is a higher-order function defined by primitive recursion with args
-- - (implicit) return type
-- - c     : element returned in base case
-- - 𝕟→c→c : step function
-- - the Nat on which to perform the recursion
natrec : {C : Set} -> C -> (Nat -> C -> C) -> Nat -> C
natrec c 𝕟→c→c  zero    = c
natrec c 𝕟→c→c (succ n) = 𝕟→c→c n (natrec c 𝕟→c→c n)

-- natrec definitions of addition and multiplication
_plus_ : Nat -> Nat -> Nat
_plus_ n m = natrec m    (\x y -> succ y)   n

_mult_ : Nat -> Nat -> Nat
_mult_ n m = natrec zero (\x y -> y plus m) n

-- compare plus/mult to _+_/_*_

_ : succ (succ  zero) + 2   PE.≡
    succ (succ  zero  + 2)
_ = PE.refl
_ : succ (succ  zero  + 2)  PE.≡
    succ (succ (zero  + 2))
_ = PE.refl
_ : succ (succ (zero  + 2)) PE.≡
    succ (succ          2 )
_ = PE.refl

_ :                                                      succ (succ  zero) plus 2                     PE.≡
                                                         natrec 2 (\x y -> succ y) (succ (succ zero))
_ = PE.refl
_ :                                                      natrec 2 (\x y -> succ y) (succ (succ zero)) PE.≡
    (\x y -> succ y) (succ zero)                        (natrec 2 (\x y -> succ y)       (succ zero))
_ = PE.refl
_ : (\x y -> succ y) (succ zero)                        (natrec 2 (\x y -> succ y)       (succ zero)) PE.≡
    (\  y -> succ y)                                    (natrec 2 (\x y -> succ y)       (succ zero))
_ = PE.refl
_ : (\  y -> succ y)                                    (natrec 2 (\x y -> succ y)       (succ zero)) PE.≡
             succ                                       (natrec 2 (\x y -> succ y)       (succ zero))
_ = PE.refl
_ :          succ                                       (natrec 2 (\x y -> succ y)       (succ zero)) PE.≡
             succ                ((\x y -> succ y) zero (natrec 2 (\x y -> succ y)             zero))
_ = PE.refl
_ :          succ                ((\x y -> succ y) zero (natrec 2 (\x y -> succ y)             zero)) PE.≡
             succ                ((\  y -> succ y)      (natrec 2 (\x y -> succ y)             zero))
_ = PE.refl
_ :          succ                ((\  y -> succ y)      (natrec 2 (\x y -> succ y)             zero)) PE.≡
             succ                (         succ         (natrec 2 (\x y -> succ y)             zero))
_ = PE.refl
_ :          succ                (         succ         (natrec 2 (\x y -> succ y)             zero)) PE.≡
             succ                (         succ                 2                                   )
_ = PE.refl

{-
to stay entirely in Gödel system T
- use terms built up by variables, application, lambda abstraction,
- and constants true, false, zero, succ, if_then_else_, natrec

Gödel system T has unusual property (for a programming language)
- all typable programs terminate

not only do terms in base types Bool and Nat terminate whatever reduction is chosen,
but also terms of function type terminate

reduction rules
- β-reduction
- defining equations for if_then_else and natrec

reductions can be performed anywhere in a term,
so there may be several ways to reduce a term

therefore, Gödel system T is strongly normalising
- any typable term reaches a normal form whatever reduction strategy is chosen

Even in this restrictive Gödel system T, possible to define many numerical functions.
Can define all primitive recursive functions
(in the usual sense without higher-order functions).

Can also define functions which are not primitive recursive, such as the Ackermann function.

Gödel system T is important in the history of ideas that led to
the Curry-Howard isomorphism and Martin-Löf type theory.

Gödel system T
- is the simply typed kernel of Martin-Löf’s constructive type theory,
Martin-Löf type theory
- is the foundational system from which Agda grew

relationship between Agda and Martin-Löf type theory is much like the
relationship between Haskell and the simply typed lambda calculus.
Or compare it with the relationship between Haskell and Plotkin’s PCF [30].

Like Gödel system T,
PCF is based on the simply typed lambda calculus with truth values and natural numbers.
But PCF includes a fixed point combinator
- used for encoding arbitrary general recursive definitions
  - therefore can define non-terminating functions in PCF.
-}

-- Exercise/TODO: Define all functions previously given in the text in Gödel System T.

-- induction principle for booleans (from Mimram)
Bool-rec : (P : Bool → Set) → P false → P true → (b : Bool) → P b
Bool-rec P Pf Pt false = Pf
Bool-rec P Pf Pt true  = Pt

not' : Bool -> Bool
not' b = Bool-rec (λ bool → Bool) true false b

_ : not' false PE.≡ not false
_ = PE.refl
_ : not' true  PE.≡ not true
_ = PE.refl

equiv' : Bool -> Bool -> Bool
equiv' b false = Bool-rec (λ bool → Bool) true false b
equiv' b true  = Bool-rec (λ bool → Bool) false true b

_ : equiv' false false PE.≡ equiv false false
_ = PE.refl
_ : equiv'  true false PE.≡ equiv  true false
_ = PE.refl
_ : equiv' false  true PE.≡ equiv false  true
_ = PE.refl
_ : equiv'  true  true PE.≡ equiv  true  true
_ = PE.refl

_||'_ : Bool -> Bool -> Bool
b ||' false = Bool-rec (λ bool → Bool)      b  b b
b ||'  true = Bool-rec (λ bool → Bool) (not b) b b

_ : false ||' false PE.≡ false || false
_ = PE.refl
_ : false ||'  true PE.≡ false ||  true
_ = PE.refl
_ :  true ||' false PE.≡  true || false
_ = PE.refl
_ :  true ||'  true PE.≡  true ||  true
_ = PE.refl

_&&'_ : Bool -> Bool -> Bool
b &&' false = Bool-rec (λ bool → Bool) false false b
b &&'  true = Bool-rec (λ bool → Bool) b     b     b

_ : false &&' false PE.≡ false && false
_ = PE.refl
_ : false &&'  true PE.≡ false &&  true
_ = PE.refl
_ :  true &&' false PE.≡  true && false
_ = PE.refl
_ :  true &&'  true PE.≡  true &&  true
_ = PE.refl

pred' : Nat -> Nat
pred'  zero    = natrec zero (\x y -> zero) zero
pred' (succ n) = natrec zero (\_ _ -> n)    n
-- test after List def

{-
2.6 Parametrised Types

Haskell parametrised types : [a]
-}
data List (A : Set) : Set where
  []   :                List A
  _::_ : A -> List A -> List A
infixr 5 _::_
{-# BUILTIN LIST List #-}
{-
(A : Set) to the left of the colon
- tells Agda that A is a parameter
- and it becomes an implicit argument to the constructors:
  []   : {A : Set} -> List A
  _::_ : {A : Set} -> A -> List A -> List A

def only allows defining lists with elements in arbitrary SMALL types
- cannot define lists of sets using this definition, since sets form a large type
-}

-- test for pred'
_ : (pred' 0 :: pred' 1 :: pred' 2 :: pred' 101 :: []) PE.≡ (pred 0 :: pred 1 :: pred 2 :: pred 101 :: [])
_ = PE.refl

mapL : {A B : Set} -> (A -> B) -> List A -> List B
mapL f       []  = []
mapL f (x :: xs) = f x :: mapL f xs

_ : mapL succ (1 :: 2 :: []) PE.≡ (2 :: 3 :: [])
_ = PE.refl

-- Exercise: Define some more list combinators like for example foldl or filter.
filter : {A : Set} -> (A -> Bool) -> List A -> List A
filter f       []  = []
filter f (x :: xs) = let tail = filter f xs in if f x then x :: tail else tail

_ : filter (_< 4) (5 :: 4 :: 3 :: 2 :: 1 :: []) PE.≡ (3 :: 2 :: 1 :: [])
_ = PE.refl

foldl : {A B : Set} -> (B -> A -> B) -> B -> List A -> B
foldl _ b       []  = b
foldl f b (a :: as) = foldl f (f b a) as

foldr : {A B : Set} -> (A -> B -> B) -> B -> List A -> B
foldr f b       []  = b
foldr f b (a :: as) = f a (foldr f b as)

_ : foldl _+_ 0 (3 :: 2 :: 1 :: []) PE.≡ 6
_ = PE.refl

_ : foldl _∸_ 0 (3 :: 1 :: []) PE.≡ 0
_ = PE.refl

_ : foldr _∸_ 0 (3 :: 1 :: []) PE.≡ 2
_ = PE.refl

-- Exercise: define list recursion combinator listrec (like natrec, but for lists)
-- from Mimram
List-rec
  : {A : Set}
  → (P : List A → Set)
  → P []
  → ((x : A) → (xs : List A) → P xs → P (x :: xs))
  → (xs : List A)
  → P xs
List-rec P Pe Pc       []  = Pe
List-rec P Pe Pc (x :: xs) = Pc x xs (List-rec P Pe Pc xs)

mapL' : {A B : Set} -> (A -> B) -> List A -> List B
mapL' {_} {B} f xs = List-rec (λ _ → List B) [] (λ a _ bs → f a :: bs) xs

_ : mapL' succ (1 :: 2 :: []) PE.≡ mapL succ (1 :: 2 :: [])
_ = PE.refl

filter' : {A : Set} -> (A -> Bool) -> List A -> List A
filter' {A} f xs = List-rec (λ _ → List A) [] (λ a _ as' → if f a then a :: as' else as') xs

_ : filter' (_< 4) (5 :: 4 :: 3 :: 2 :: 1 :: []) PE.≡ filter (_< 4) (5 :: 4 :: 3 :: 2 :: 1 :: [])
_ = PE.refl

foldl' : {A B : Set} -> (B -> A -> B) -> B -> List A -> B
foldl' {_} {B} f b as = List-rec (λ _ → B) b (λ a _ b → f b a) as

_ : foldl' _+_ 0 (3 :: 2 :: 1 :: []) PE.≡ foldl _+_ 0 (3 :: 2 :: 1 :: [])
_ = PE.refl

foldr' : {A B : Set} -> (A -> B -> B) -> B -> List A -> B
foldr' {A} {B} f b as = List-rec (λ _ → B) b (λ a as b → f a b) as

_ : foldr' _∸_ 0 (3 :: 1 :: []) PE.≡ foldr _∸_ 0 (3 :: 1 :: [])
_ = PE.refl

-- binary Cartesian product AKA pair
data _X_ (A B : Set) : Set where
  <_,_> : A -> B -> A X B

-- prime because these are never used but are redeinfed later
fst' : {A B : Set} -> A X B -> A
fst' < a , b > = a

snd' : {A B : Set} -> A X B -> B
snd' < a , b > = b

-- Usually want to zip lists of equal length.
-- Can fix that with runtime Maybe or compiletime dependent types (later).
zipL : {A B : Set} -> List A -> List B -> List (A X B)
zipL       []         _  = []
zipL (_ ::  _)       []  = []
zipL (x :: xs) (y :: ys) = < x , y > :: zipL xs ys

-- Exercise: Define the sum A + B of two small types with constructors: inl, inr.
data Either (A B : Set) : Set where
  inl : A -> Either A B
  inr : B -> Either A B

-- Exercise: Define a function from A + B to a small type C by cases.
toC : {A B C : Set} → (A -> C) -> (B -> C) -> (Either A B) -> C
toC ac  _ (inl a) = ac a
toC  _ bc (inr b) = bc b

{-
2.7 Termination-checking

General recursion allowed in most languages.
Therefore possible to define "partial" functions (e.g., divide by 0)

How to ensure functions terminate?
- one solution : restrict recursion to primitive recursion (like in Gödel system T)
  - the approach taken in Martin-Löf type theory
    where primitive recursion as a kind of structural recursion on well-founded data types
    (see Martin-Löf’s book [22] and Dybjer’s schema for inductive definitions [10])
  - but structural recursion (in one argument at a time) is often inconvenient

Agda’s termination-checker
- generalisation of primitive recursion which is practically useful
- enables doing pattern matching on several arguments simultaneously
- and having recursive calls to structurally smaller arguments

But repeated subtraction is rejected by Agda termination-checker although it is terminating.
Because Agda does not recognise the recursive call to (m - n) as structurally smaller.
Because subtraction is not a constructor for natural numbers.
Further reasoning required to deduce the recursive call is on a smaller argument.

Section 7 : describes how partial and general recursive functions can be represented in Agda.
Idea is to replace a partial function by a total function with an extra argument:
a proof that the function terminates on its arguments.

------------------------------------------------------------------------------
3 Dependent Types

3.1 Vectors of a Given Length

2 ways to define
- Recursive family
  - by primitive recursion/induction on n
- Inductive family
  - as a family of data types by declaring its constructors and the types of constructors
  - like def of List, except length info included in types

paper mostly uses inductive families

--------------------------------------------------
Vectors as a Recursive Family

In math : define vectors by induction on n:
  A   0 = 1
  A n+1 = A × An
In Agda (and Martin-Löf type theory):
-}
-- type with only one element
data Unit : Set where
  <> : Unit

VecR : Set -> Nat -> Set
VecR A  zero    = Unit
VecR A (succ n) = A X VecR A n

{-
Up till now, only used primitive recursion for defining functions
where the range is in a given set (in a given small type).
Here, primitive recursion used for defining a family of sets
- a family of elements in a given large type.
-}

zipR : {A B : Set} {n : Nat} -> VecR A n -> VecR B n -> VecR (A X B) n
zipR {n =  zero}          _          _   = <>
zipR {n = succ n'} < a , as > < b , bs > = < < a , b > , zipR {n = n'} as bs >

{-
base case : type-correct since the right hand side has type
            VecR (A X B) zero     = <>
step case : type-correct since the right hand side has type
            VecR (A X B) (succ n) = (A X B) X (VecR (A X B) n)
-}

-- Exercise. Write the functions head, tail, and map for the recursive vectors.

headR : {A : Set} {n : Nat} -> VecR A (succ n) ->      A
headR < x , _ > = x

tailR : {A : Set} {n : Nat} -> VecR A (succ n) -> VecR A n
tailR < _ ,  t > = t

mapR : {A B : Set} {n : Nat} -> (A -> B) -> VecR A n -> VecR B n
mapR {n = zero}    _        _   = <>
mapR {n = succ n'} f < a , as > = < f a , mapR {n = n'} f as >

_ : mapR succ < 1 , < 2 , < 0 , <> > > > PE.≡ < 2 , < 3 , < 1 , <> > > >
_ = PE.refl

--------------------------------------------------
-- Vectors as an Inductive Family

data Vec (A : Set) : Nat -> Set where
  []   :                              Vec A  zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (succ n)

{-
this time no induction on length
instead : constructors generate vectors of different lengths
[] : length 0
:: : length (n + 1)

Definition style called an inductive family, or an inductively defined family of sets.

Terminology comes from constructive type theory,
where data types such as Nat and (List A) are called inductive types.

Remark: Beware of terminological confusion:
- In programming languages one talks about recursive types for such data
  types defined by declaring the constructors with their types.
- May be confusing since the word recursive family was used for a different notion.
- Reason for terminological distinction between data types in ordinary functional languages,
  and data types in languages where all programs terminate.
- In terminating languages, there will not be any non-terminating numbers or non-terminating lists.
- The set-theoretic meaning of such types is therefore simple:
  - build the set inductively generated by the constructors, see [9] for details.
- In non-terminating language, the semantic domains are more complex.
  - One typically considers various kinds of Scott domains which are complete partially orders.

(Vec A n) has two args:
- small type A of the elements
  - A is a parameter in the sense that it remains the same throughout the definition:
    for a given A, define the family Vec A : Nat -> Set
- length n of type Nat.
  - n is not a parameter since it varies in the types of the constructors

Non-parameters are often called INDICES
- say that Vec A is an inductive family indexed by natural numbers

In Agda data type definitions
- parameters are placed to the left of the colon
  and become implicit arguments to the constructors
- indices are placed to the right
-}

zip : {A B : Set} {n : Nat} -> Vec A n -> Vec B n -> Vec (A X B) n
zip {n = zero}          []        []  = []
zip {n = succ n'} (x :: xs) (y :: ys) = < x , y > :: zip {n = n'} xs ys

head : {A : Set} {n : Nat} -> Vec A (succ n) -> A
head (x :: _) = x

tail : {A : Set} {n : Nat} -> Vec A (succ n) -> Vec A n
tail (_ :: xs) = xs

map : {A B : Set} {n : Nat} -> (A -> B) -> Vec A n -> Vec B n
map f [] = []
map f (x :: xs) = f x :: map f xs

--------------------------------------------------
-- 3.2 Finite Sets

data Fin : Nat -> Set where
  fzero : {n : Nat} ->          Fin (succ n)
  fsucc : {n : Nat} -> Fin n -> Fin (succ n)

{-
for each n, Fin n contains n elements
e.g., Fin 3 contains fzero, fsucc fzero and fsucc (fsucc fzero)

useful to access element in a vector
- for Vec A n
- position given by (Fin n)
- ensures accessing an element inside the vector

For empty vector n is zero.
So would use (Fin 0) --- which has no elements.
There is no such case.
Expressed in Agda via "absurd" pattern '()'
-}

_!_ : {A : Set} {n : Nat} -> Vec A n -> Fin n -> A
[]        ! ()
(x ::  _) ! fzero   = x
(_ :: xs) ! fsucc i = xs ! i

-- Exercise: Rewrite the function !! so that it has the following type:
-- This eliminates the empty vector case, but other cases are needed.

_!!_  : {A : Set} {n : Nat} -> Vec A (succ n) -> Fin (succ n) -> A
_!!_  {_}   {zero} (a ::  f_)  fzero    = a
_!!_  {_} {succ n} (a ::  _)  fzero    = a
_!!_  {_} {succ n} (_ :: as) (fsucc f) = _!!_  {n = n} as f

_!!'_ : {A : Set} {n : Nat} -> Vec A (succ n) -> Fin (succ n) -> A
_!!'_              (a ::  _)  fzero    = a
_!!'_ {_} {succ n} (_ :: as) (fsucc f) = _!!'_ {n = n} as f

_ : (0 :: 1 :: 2 :: []) !   fsucc fzero PE.≡ 1
_ = PE.refl
_ : (0 :: 1 :: 2 :: []) !!  fsucc fzero PE.≡ 1
_ = PE.refl
_ : (0 :: 1 :: 2 :: []) !!' fsucc fzero PE.≡ 1
_ = PE.refl

-- Exercise: Give an alternative definition of Fin as a recursive family.

-- from Conal Eliot https://raw.githubusercontent.com/conal/agda-play/main/DependentTypesAtWork/RecVec.agda
FinR : Nat -> Set
FinR  zero    = DEP.⊥
FinR (succ n) = Maybe.Maybe (FinR n)

f5 : FinR 5
f5 = Maybe.nothing
f5' : FinR 5 PE.≡ Maybe.Maybe (Maybe.Maybe (Maybe.Maybe (Maybe.Maybe (Maybe.Maybe DEP.⊥))))
f5' = PE.refl
f4 : FinR 4
f4 = Maybe.nothing
f3 : FinR 3
f3 = Maybe.nothing
f2 : FinR 2
f2 = Maybe.nothing
f1 : FinR 1
f1 = Maybe.nothing
f1' : FinR 1 PE.≡ Maybe.Maybe DEP.⊥
f1' = PE.refl
--f0 : FinR 0
--f0 = {!!} -- no solution found
f0' : FinR 0 PE.≡ DEP.⊥
f0' = PE.refl

_!'_ : {A : Set} {n : Nat} → VecR A n → FinR n → A
_!'_  {n = succ m} < a ,  _ >  Maybe.nothing    = a
_!'_  {n = succ m} < _ , as > (Maybe.just finm) = as !' finm

_    : < 0 , < 1 , < 2 , <> > > >  !'                                    Maybe.nothing   PE.≡ 0
_    = PE.refl
_    : < 0 , < 1 , < 2 , <> > > >  !'                         Maybe.just Maybe.nothing   PE.≡ 1
_    = PE.refl
_    : < 0 , < 1 , < 2 , <> > > >  !'             Maybe.just (Maybe.just Maybe.nothing)  PE.≡ 2
_    = PE.refl
-- (Maybe.Maybe _A_645) !=< DEP.⊥
-- _ : < 0 , < 1 , < 2 , <> > > >  !' Maybe.just (Maybe.just (Maybe.just Maybe.nothing)) PE.≡ 100
-- _ = PE.refl

--------------------------------------------------
-- 3.3 More Inductive Families

-- binary trees of a certain height
-- any given (t : DBTree A n) is a perfectly balanced tree
-- with 2n elements and information in the leaves
data DBTree (A : Set) : Nat -> Set where
  leaf :                     A                 -> DBTree A zero
  node : {n : Nat} -> DBTree A n -> DBTree A n -> DBTree A (succ n)

l1       : DBTree Nat 0
l1       = leaf 1
l2       : DBTree Nat 0
l2       = leaf 2
n1-2     : DBTree Nat 1
n1-2     = node l1 l2
l3       : DBTree Nat 0
l3       = leaf 3
l4       : DBTree Nat 0
l4       = leaf 4
n3-4     : DBTree Nat 1
n3-4     = node l3 l4
n1-2-3-4 : DBTree Nat 2
n1-2-3-4 = node n1-2 n3-4

-- Exercise/TODO: Modify DBTree def to define the height balanced binary trees
-- i.e., binary trees where difference between heights of left and right subtree is at most one.

-- Exercise/TODO: Define lambda terms as an inductive family
-- indexed by the maximal number of free variables allowed in the term.

-- Exercise/TODO: define typed lambda terms as an inductive family indexed by the type of the term.

{-
------------------------------------------------------------------------------
Curry, 1930’s : one-to-one correspondence between propositions in propositional logic and types.
1960’s de Bruijn and Howard introduced dependent types to extend Curry’s correspondence to predicate logic.
Scott [31] and Martin-Löf [20], correspondence became building block of foundation for constructive math:
- Martin-Löf’s intuitionistic type theory.

Will now show how intuitionistic predicate logic with equality is a subsystem of
Martin-Löf type theory by realising it as a theory in Agda.

4.1 Propositional Logic

isomorphism : each proposition is interpreted as the set of its proofs.
To emphazie PROOFS here are FIRST-CLASS mathematical object, say PROOF OBJECTS.
aka : CONSTRUCTIONS

proposition
- is true IFF its set of proofs is inhabited
- it is false iff its set of proofs is empty
-}

-- CONJUNCTION (aka AND)
-- A and B are two propositions represented by their sets of proofs.
-- A & B is also a set of proofs, representing the conjunction of A and B.
-- Note : conjunction is same as Cartesian product of two sets.
-- applying & constructor is &-introduction
data _&_ (A B : Set) : Set where
  <_,_> : A -> B -> A & B

-- alternate def
_&'_ : Set -> Set -> Set
A &' B = A X B

-- two rules of &-elimination
-- rules state that if A & B is true then A and B are also true
fst : {A B : Set} -> A & B -> A
fst < a , _ > = a

snd : {A B : Set} -> A & B -> B
snd < _ , b > = b

sndP : {A B : Set} -> A &' B -> B
sndP < _ , b > = b

-- DISJUNCTION (aka OR)
-- disjunction corresponds to disjoint union
data _\/_ (A B : Set) : Set where
  inl : A -> A \/ B
  inr : B -> A \/ B

-- alternate def
_\/'_ : Set -> Set -> Set
A \/' B = Either A B

-- rule of \/-elimination is case analysis for a disjoint union
case : {A B C : Set} -> A \/ B -> (A -> C) -> (B -> C) -> C
case (inl a) d e = d a
case (inr b) d e = e b

-- proposition which is always true
-- corresponds to the unit set (see page 14) according to Curry-Howard:
data True : Set where
  <> : True

-- proposition False is the proposition that is false by definition
-- corresponds to the the empty set according to Curry-Howard.
-- This is the set which is defined by stating that it has no canonical elements.
-- sometimes referred as the “absurdity” set and denoted by ⊥
data False : Set where

-- rule of ⊥-elimination states that if False has been proved, then can prove any proposition A.
-- Can only happen by starting with contradictory assumptions.
nocase : {A : Set} -> False -> A
nocase () -- tells agda no cases to consider
{-
Justification of this rule is same as justification of existence of
an empty function from the empty set into an arbitrary set.
Since the empty set has no elements there is nothing to define; it is definition by no cases.
Recall the explanation on page 16 when we used the notation ().
-}

-- In constructive logic
-- - proving negation of a proposition is the same as
-- - proving the proposition leads to absurdity:
Not : Set -> Set
Not A = A -> False

{-
BHK-interpretation says an implication is proved by providing a method for transforming
a proof of A into a proof of B.

When Brouwer pioneered this 100 years ago, there were no computers and no models of computation.
In contemporary constructive mathematics in general, and in Martin-Löf type theory in particular,
a “method” is usually understood as a computable function (or computer program) which transforms proofs.
Implication is defined as function space.
Emphasized via new notation:
-}

_==>_ : (A B : Set) -> Set
A ==> B = A -> B

_ : False ==> False -- T
_ = λ ()
_ : False ==> True  -- T
_ = λ ()
_ : True  ==> False -- F
_ = λ _ → {!!}
_ : True  ==> True  -- T
_ = λ _ → <>

{-
Above def not accepted in Martin-Löf’s version of propositions-as-sets.
Because each proposition should be defined by stating what its canonical proofs are.
A canonical proof should always begin with a constructor.
A function in A -> B does not, unless one considers the lambda-sign as a constructor.

Instead, Martin-Löf defines implication as a set with one constructor:
Using this, a canonical proof of A ==>' B always begins with the constructor fun.
-}
data _==>'_ (A B : Set) : Set where
  fun : (A -> B) -> A ==>' B

-- rule of ==>-elimination (modus ponens)
apply : {A B : Set} -> A ==>' B -> A -> B
apply (fun f) a = f a

-- equivalence of propositions
_<==>_ : Set -> Set -> Set
A <==> B = (A ==> B) & (B ==> A)

_ : False <==> False
_ = < ( λ () ) , ( λ () ) >
_ : False <==> True
_ = < (λ () ) , (λ { <> → {!!}}) >
_ : True  <==> False
_ = < (λ { <> → {!!}}) , (λ () ) >
_ : True  <==> True
_ = < (λ _ → <>) , (λ _ → <>) >

{-
Exercise/TODO: Prove your favourite tautology from propositional logic.
Beware that you will not be able to prove the law of the excluded middle A \/ Not A.
This is a consequence of the definition of disjunction, can you explain why?.
The law of the excluded middle is not available in intuitonistic logic, only in classical logic.
-}

le : ∀ {P Q : Set} → (P ==> Q) <==> (Not P \/ Q)
le {P} {Q} = < (λ {P==>Q → {!!} }) , (λ { (inl NotP) p → {!!} ; (inr q) p → q}) >

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:
{-# OPTIONS --safe --warning=error #-}

open import Sets.EquivalenceRelations
open import Functions.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_; Setω)
open import Setoids.Setoids
open import Groups.Definition
open import LogicalFormulae
open import Orders.WellFounded.Definition
open import Numbers.Naturals.Semiring
open import Groups.Lemmas

module Groups.FreeProduct.Addition {i : _} {I : Set i} (decidableIndex : (x y : I) → ((x ≡ y) || ((x ≡ y) → False))) {a b : _} {A : I → Set a} {S : (i : I) → Setoid {a} {b} (A i)} {_+_ : (i : I) → (A i) → (A i) → A i} (decidableGroups : (i : I) → (x y : A i) → ((Setoid._∼_ (S i) x y)) || ((Setoid._∼_ (S i) x y) → False)) (G : (i : I) → Group (S i) (_+_ i)) where

open import Groups.FreeProduct.Definition decidableIndex decidableGroups G
open import Groups.FreeProduct.Setoid decidableIndex decidableGroups G

prependEqual : (i : I) (g : A i) .(nonZero : (Setoid._∼_ (S i) g (Group.0G (G i))) → False) → (j : I) → i ≡ j → (w : ReducedSequenceBeginningWith j) → ReducedSequence
prependEqual i g nonzero .i refl (ofEmpty .i h nonZero) with decidableGroups i (_+_ i g h) (Group.0G (G i))
prependEqual i g nonzero .i refl (ofEmpty .i h nonZero) | inl sumZero = empty
prependEqual i g nonzero .i refl (ofEmpty .i h nonZero) | inr sumNotZero = nonempty i (ofEmpty i (_+_ i g h) sumNotZero)
prependEqual i g nonzero .i refl (prependLetter .i h nonZero x x₁) with decidableGroups i (_+_ i g h) (Group.0G (G i))
prependEqual i g nonzero .i refl (prependLetter .i h nonZero {j} x x₁) | inl sumZero = nonempty j x
prependEqual i g nonzero .i refl (prependLetter .i h nonZero x pr) | inr sumNotZero = nonempty i (prependLetter i (_+_ i g h) sumNotZero x pr)

prepend : (i : I) → (g : A i) → .(nonZero : (Setoid._∼_ (S i) g (Group.0G (G i))) → False) → ReducedSequence → ReducedSequence
prepend i g nonzero empty = nonempty i (ofEmpty i g nonzero)
prepend i g nonzero (nonempty j x) with decidableIndex i j
prepend i g nonzero (nonempty j w) | inl i=j = prependEqual i g nonzero j i=j w
prepend i g nonzero (nonempty j x) | inr i!=j = nonempty i (prependLetter i g nonzero x i!=j)

plus' : {j : _} → (ReducedSequenceBeginningWith j) → ReducedSequence → ReducedSequence
plus' (ofEmpty i g nonZero) s = prepend i g nonZero s
plus' (prependLetter i g nonZero x pr) s = prepend i g nonZero (plus' x s)

_+RP_ : ReducedSequence → ReducedSequence → ReducedSequence

empty +RP b = b
nonempty i x +RP b = plus' x b

abstract
  prependWD : {i : I} → (g1 g2 : A i) → .(nz1 : _) → .(nz2 : _) → (y : ReducedSequence) (eq : Setoid._∼_ (S i) g1 g2) → prepend i g1 nz1 y =RP prepend i g2 nz2 y
  prependWD {i} g1 g2 nz1 nz2 empty g1=g2 with decidableIndex i i
  prependWD {i} g1 g2 nz1 nz2 empty g1=g2 | inl refl = g1=g2
  prependWD {i} g1 g2 nz1 nz2 empty g1=g2 | inr x = exFalso (x refl)
  prependWD {i} g1 g2 nz1 nz2 (nonempty j x) g1=g2 with decidableIndex i j
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (ofEmpty .j g nonZero)) g1=g2 | inl refl with decidableGroups j ((j + g1) g) (Group.0G (G j))
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (ofEmpty .j g nonZero)) g1=g2 | inl refl | inl x with decidableGroups j ((j + g2) g) (Group.0G (G j))
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (ofEmpty .j g nonZero)) g1=g2 | inl refl | inl x | inl x₁ = record {}
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (ofEmpty .j g nonZero)) g1=g2 | inl refl | inl x | inr bad = exFalso (bad (Equivalence.transitive (Setoid.eq (S j)) (Group.+WellDefined (G j) (Equivalence.symmetric (Setoid.eq (S j)) g1=g2) (Equivalence.reflexive (Setoid.eq (S j)))) x))
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (ofEmpty .j g nonZero)) g1=g2 | inl refl | inr x with decidableGroups j ((j + g2) g) (Group.0G (G j))
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (ofEmpty .j g nonZero)) g1=g2 | inl refl | inr bad | inl p = exFalso (bad (Equivalence.transitive (Setoid.eq (S j)) (Group.+WellDefined (G j) g1=g2 (Equivalence.reflexive (Setoid.eq (S j)))) p))
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (ofEmpty .j g nonZero)) g1=g2 | inl refl | inr x | inr x₁ with decidableIndex j j
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (ofEmpty .j g nonZero)) g1=g2 | inl refl | inr x | inr x₁ | inl refl = Group.+WellDefined (G j) g1=g2 (Equivalence.reflexive (Setoid.eq (S j)))
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (ofEmpty .j g nonZero)) g1=g2 | inl refl | inr x | inr x₁ | inr bad = exFalso (bad refl)
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (prependLetter .j g nonZero w x₁)) g1=g2 | inl refl with decidableGroups j ((j + g1) g) (Group.0G (G j))
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (prependLetter .j g nonZero w x₁)) g1=g2 | inl refl | inl x with decidableGroups j ((j + g2) g) (Group.0G (G j))
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (prependLetter .j g nonZero w x₁)) g1=g2 | inl refl | inl x | inl x₂ = =RP'reflex w
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (prependLetter .j g nonZero w x₁)) g1=g2 | inl refl | inl x | inr bad = exFalso (bad (Equivalence.transitive (Setoid.eq (S j)) (Group.+WellDefined (G j) (Equivalence.symmetric (Setoid.eq (S j)) g1=g2) (Equivalence.reflexive (Setoid.eq (S j)))) x))
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (prependLetter .j g nonZero w x₁)) g1=g2 | inl refl | inr neq with decidableGroups j ((j + g2) g) (Group.0G (G j))
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (prependLetter .j g nonZero w x₁)) g1=g2 | inl refl | inr neq | inl x = exFalso (neq (Equivalence.transitive (Setoid.eq (S j)) (Group.+WellDefined (G j) g1=g2 (Equivalence.reflexive (Setoid.eq (S j)))) x))
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (prependLetter .j g nonZero w x₁)) g1=g2 | inl refl | inr neq | inr x with decidableIndex j j
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (prependLetter .j g nonZero w x₁)) g1=g2 | inl refl | inr neq | inr x | inl refl = Group.+WellDefined (G j) g1=g2 (Equivalence.reflexive (Setoid.eq (S j))) ,, =RP'reflex w
  prependWD {.j} g1 g2 nz1 nz2 (nonempty j (prependLetter .j g nonZero w x₁)) g1=g2 | inl refl | inr neq | inr x | inr bad = exFalso (bad refl)
  prependWD {i} g1 g2 nz1 nz2 (nonempty j x) g1=g2 | inr i!=j with decidableIndex i i
  prependWD {i} g1 g2 nz1 nz2 (nonempty j x) g1=g2 | inr i!=j | inl refl = g1=g2 ,, =RP'reflex x
  prependWD {i} g1 g2 nz1 nz2 (nonempty j x) g1=g2 | inr i!=j | inr bad = exFalso (bad refl)

abstract
  prependWD' : {i : I} → (g : A i) → .(nz : _) → (y1 y2 : ReducedSequence) (eq : y1 =RP y2) → prepend i g nz y1 =RP prepend i g nz y2
  prependWD' {i} g1 nz empty empty eq with decidableIndex i i
  prependWD' {i} g1 nz empty empty eq | inl refl = Equivalence.reflexive (Setoid.eq (S i))
  prependWD' {i} g1 nz empty empty eq | inr x = exFalso (x refl)
  prependWD' {i} g1 nz (nonempty j x) (nonempty k x₁) eq with decidableIndex i j
  prependWD' {.j} g1 nz (nonempty j w1) (nonempty k w2) eq | inl refl with decidableIndex j k
  prependWD' {.j} g1 nz (nonempty j (ofEmpty .j g nonZero)) (nonempty .j (ofEmpty .j h nonZero₁)) eq | inl refl | inl refl with decidableGroups j ((j + g1) g) (Group.0G (G j))
  prependWD' {.j} g1 nz (nonempty j (ofEmpty .j g nonZero)) (nonempty .j (ofEmpty .j h nonZero₁)) eq | inl refl | inl refl | inl eq1 with decidableGroups j ((j + g1) h) (Group.0G (G j))
  prependWD' {.j} g1 nz (nonempty j (ofEmpty .j g nonZero)) (nonempty .j (ofEmpty .j h nonZero₁)) eq | inl refl | inl refl | inl eq1 | inl x = record {}
  prependWD' {.j} g1 nz (nonempty j (ofEmpty .j g nonZero)) (nonempty .j (ofEmpty .j h nonZero₁)) eq | inl refl | inl refl | inl eq1 | inr x with decidableIndex j j
  prependWD' {.j} g1 nz (nonempty j (ofEmpty .j g nonZero)) (nonempty .j (ofEmpty .j h nonZero₁)) eq | inl refl | inl refl | inl eq1 | inr x | inl refl = exFalso (x (Equivalence.transitive (Setoid.eq (S j)) (Group.+WellDefined (G j) (Equivalence.reflexive (Setoid.eq (S j))) (Equivalence.symmetric (Setoid.eq (S j)) eq)) eq1))
  prependWD' {.j} g1 nz (nonempty j (ofEmpty .j g nonZero)) (nonempty .j (ofEmpty .j h nonZero₁)) eq | inl refl | inl refl | inr neq1 with decidableGroups j ((j + g1) h) (Group.0G (G j))
  prependWD' {.j} g1 nz (nonempty j (ofEmpty .j g nonZero)) (nonempty .j (ofEmpty .j h nonZero₁)) eq | inl refl | inl refl | inr neq1 | inl x with decidableIndex j j
  prependWD' {.j} g1 nz (nonempty j (ofEmpty .j g nonZero)) (nonempty .j (ofEmpty .j h nonZero₁)) eq | inl refl | inl refl | inr neq1 | inl x | inl refl = exFalso (neq1 (Equivalence.transitive (Setoid.eq (S j)) (Group.+WellDefined (G j) (Equivalence.reflexive (Setoid.eq (S j))) eq) x))
  prependWD' {.j} g1 nz (nonempty j (ofEmpty .j g nonZero)) (nonempty .j (ofEmpty .j h nonZero₁)) eq | inl refl | inl refl | inr neq1 | inr x with decidableIndex j j
  prependWD' {.j} g1 nz (nonempty j (ofEmpty .j g nonZero)) (nonempty .j (ofEmpty .j h nonZero₁)) eq | inl refl | inl refl | inr neq1 | inr x | inl refl = Group.+WellDefined (G j) (Equivalence.reflexive (Setoid.eq (S j))) eq
  prependWD' {.j} g1 nz (nonempty j (prependLetter .j g nonZero w1 x)) (nonempty .j (prependLetter .j h nonZero₁ w2 x₁)) eq | inl refl | inl refl with decidableIndex j j
  prependWD' {.j} g1 nz (nonempty j (prependLetter .j g nonZero w1 x)) (nonempty .j (prependLetter .j h nonZero₁ w2 x₁)) eq | inl refl | inl refl | inl refl with decidableGroups j ((j + g1) g) (Group.0G (G j))
  prependWD' {.j} g1 nz (nonempty j (prependLetter .j g nonZero w1 x)) (nonempty .j (prependLetter .j h nonZero₁ w2 x₁)) eq | inl refl | inl refl | inl refl | inl eq1 with decidableGroups j ((j + g1) h) (Group.0G (G j))
  prependWD' {.j} g1 nz (nonempty j (prependLetter .j g nonZero w1 x)) (nonempty .j (prependLetter .j h nonZero₁ w2 x₁)) eq | inl refl | inl refl | inl refl | inl eq1 | inl eq2 = _&&_.snd eq
  prependWD' {.j} g1 nz (nonempty j (prependLetter .j g nonZero w1 x)) (nonempty .j (prependLetter .j h nonZero₁ w2 x₁)) eq | inl refl | inl refl | inl refl | inl eq1 | inr neq2 = exFalso (neq2 (Equivalence.transitive (Setoid.eq (S j)) (Group.+WellDefined (G j) (Equivalence.reflexive (Setoid.eq (S j))) (Equivalence.symmetric (Setoid.eq (S j)) (_&&_.fst eq))) eq1))
  prependWD' {.j} g1 nz (nonempty j (prependLetter .j g nonZero w1 x)) (nonempty .j (prependLetter .j h nonZero₁ w2 x₁)) eq | inl refl | inl refl | inl refl | inr neq1 with decidableGroups j ((j + g1) h) (Group.0G (G j))
  prependWD' {.j} g1 nz (nonempty j (prependLetter .j g nonZero w1 x)) (nonempty .j (prependLetter .j h nonZero₁ w2 x₁)) eq | inl refl | inl refl | inl refl | inr neq1 | inl eq2 = exFalso (neq1 (Equivalence.transitive (Setoid.eq (S j)) (Group.+WellDefined (G j) (Equivalence.reflexive (Setoid.eq (S j))) (_&&_.fst eq)) eq2))
  prependWD' {.j} g1 nz (nonempty j (prependLetter .j g nonZero w1 x)) (nonempty .j (prependLetter .j h nonZero₁ w2 x₁)) eq | inl refl | inl refl | inl refl | inr neq1 | inr _ with decidableIndex j j
  prependWD' {.j} g1 nz (nonempty j (prependLetter .j g nonZero w1 x)) (nonempty .j (prependLetter .j h nonZero₁ w2 x₁)) eq | inl refl | inl refl | inl refl | inr neq1 | inr _ | inl refl = Group.+WellDefined (G j) (Equivalence.reflexive (Setoid.eq (S j))) (_&&_.fst eq) ,, _&&_.snd eq
  prependWD' {.j} g1 nz (nonempty j (prependLetter .j g nonZero w1 x)) (nonempty .j (prependLetter .j h nonZero₁ w2 x₁)) eq | inl refl | inl refl | inl refl | inr neq1 | inr _ | inr bad = exFalso (bad refl)
  prependWD' {.j} g1 nz (nonempty j (ofEmpty .j g nonZero)) (nonempty k (ofEmpty .k g₁ nonZero₁)) eq | inl refl | inr j!=k with decidableIndex j k
  prependWD' {j} g1 nz (nonempty j (ofEmpty j g nonZero)) (nonempty k (ofEmpty .k g₁ nonZero₁)) eq | inl refl | inr j!=k | inl j=k = exFalso (j!=k j=k)
  prependWD' {.j} g1 nz (nonempty j (prependLetter .j g nonZero w1 x)) (nonempty k (prependLetter .k g₁ nonZero₁ w2 x₁)) eq | inl refl | inr j!=k with decidableIndex j k
  prependWD' {.j} g1 nz (nonempty j (prependLetter .j g nonZero w1 x)) (nonempty k (prependLetter .k g₁ nonZero₁ w2 x₁)) eq | inl refl | inr j!=k | inl j=k = exFalso (j!=k j=k)
  prependWD' {i} g1 nz (nonempty j w1) (nonempty k w2) eq | inr i!=j with decidableIndex i k
  prependWD' {.k} g1 nz (nonempty j (ofEmpty .j g nonZero)) (nonempty k (ofEmpty .k g₁ nonZero₁)) eq | inr i!=j | inl refl with decidableIndex j k
  prependWD' {.k} g1 nz (nonempty .k (ofEmpty .k g nonZero)) (nonempty k (ofEmpty .k g₁ nonZero₁)) eq | inr i!=j | inl refl | inl refl = exFalso (i!=j refl)
  prependWD' {.k} g1 nz (nonempty j (prependLetter .j g nonZero w1 x)) (nonempty k (prependLetter .k g₁ nonZero₁ w2 x₁)) eq | inr i!=j | inl refl with decidableIndex j k
  prependWD' {.k} g1 nz (nonempty .k (prependLetter .k g nonZero w1 x)) (nonempty k (prependLetter .k g₁ nonZero₁ w2 x₁)) eq | inr i!=j | inl refl | inl refl = exFalso (i!=j refl)
  prependWD' {i} g1 nz (nonempty j w1) (nonempty k w2) eq | inr i!=j | inr i!=k with decidableIndex i i
  prependWD' {i} g1 nz (nonempty j w1) (nonempty k w2) eq | inr i!=j | inr i!=k | inl refl = Equivalence.reflexive (Setoid.eq (S i)) ,, eq
  prependWD' {i} g1 nz (nonempty j w1) (nonempty k w2) eq | inr i!=j | inr i!=k | inr x = exFalso (x refl)

private
  prependLetterWD : {i : I} {h1 h2 : A i} (h1=h2 : Setoid._∼_ (S i) h1 h2) → .(nonZero1 : _) .(nonZero2 : _) {j1 j2 : I} (w1 : ReducedSequenceBeginningWith j1) (w2 : ReducedSequenceBeginningWith j2) → (eq : =RP' w1 w2) → (x1 : i ≡ _ → False) (x2 : i ≡ _ → False) → nonempty i (prependLetter i h1 nonZero1 w1 x1) =RP nonempty i (prependLetter i h2 nonZero2 w2 x2)
  prependLetterWD {i} h1=h2 nonZero1 nonZero2 {j1} {j2} w1 w2 eq x1 x2 with decidableIndex i i
  prependLetterWD {i} h1=h2 nonZero1 nonZero2 {j1} {j2} w1 w2 eq x1 x2 | inl refl = h1=h2 ,, eq
  prependLetterWD {i} h1=h2 nonZero1 nonZero2 {j1} {j2} w1 w2 eq x1 x2 | inr x = exFalso (x refl)

abstract
  plus'WD' : {i : I} (x : ReducedSequenceBeginningWith i) (y1 y2 : ReducedSequence) → (y1 =RP y2) → plus' x y1 =RP plus' x y2
  plus'WD' x empty empty eq = Equivalence.reflexive (Setoid.eq freeProductSetoid) {plus' x empty}
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty i1 w1) (nonempty i2 w2) eq with decidableIndex j i1
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j w1) (nonempty i2 w2) eq | inl refl with decidableIndex j i2
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (ofEmpty .j g₁ nonZero₁)) (nonempty .j (ofEmpty .j g₂ nonZero₂)) eq | inl refl | inl refl with decidableIndex j j
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (ofEmpty .j h1 nonZero₁)) (nonempty .j (ofEmpty .j h2 nonZero₂)) eq | inl refl | inl refl | inl refl with decidableGroups j ((j + g) h1) (Group.0G (G j))
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (ofEmpty .j h1 nonZero₁)) (nonempty .j (ofEmpty .j h2 nonZero₂)) eq | inl refl | inl refl | inl refl | inl x with decidableGroups j ((j + g) h2) (Group.0G (G j))
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (ofEmpty .j h1 nonZero₁)) (nonempty .j (ofEmpty .j h2 nonZero₂)) eq | inl refl | inl refl | inl refl | inl x | inl x₁ = record {}
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (ofEmpty .j h1 nonZero₁)) (nonempty .j (ofEmpty .j h2 nonZero₂)) eq | inl refl | inl refl | inl refl | inl x | inr bad = exFalso (bad (Equivalence.transitive (Setoid.eq (S j)) (Group.+WellDefined (G j) (Equivalence.reflexive (Setoid.eq (S j))) (Equivalence.symmetric (Setoid.eq (S j)) eq)) x))
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (ofEmpty .j h1 nonZero₁)) (nonempty .j (ofEmpty .j h2 nonZero₂)) eq | inl refl | inl refl | inl refl | inr x with decidableGroups j ((j + g) h2) (Group.0G (G j))
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (ofEmpty .j h1 nonZero₁)) (nonempty .j (ofEmpty .j h2 nonZero₂)) eq | inl refl | inl refl | inl refl | inr x | inl bad = exFalso (x (Equivalence.transitive (Setoid.eq (S j)) (Group.+WellDefined (G j) (Equivalence.reflexive (Setoid.eq (S j))) eq) bad))
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (ofEmpty .j h1 nonZero₁)) (nonempty .j (ofEmpty .j h2 nonZero₂)) eq | inl refl | inl refl | inl refl | inr x | inr x₁ with decidableIndex j j
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (ofEmpty .j h1 nonZero₁)) (nonempty .j (ofEmpty .j h2 nonZero₂)) eq | inl refl | inl refl | inl refl | inr x | inr x₁ | inl refl = Group.+WellDefined (G j) (Equivalence.reflexive (Setoid.eq (S j))) eq
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (ofEmpty .j h1 nonZero₁)) (nonempty .j (ofEmpty .j h2 nonZero₂)) eq | inl refl | inl refl | inl refl | inr x | inr x₁ | inr bad = exFalso (bad refl)
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (prependLetter .j h1 nonZero₁ w1 x)) (nonempty .j (prependLetter .j h2 nonZero₂ w2 x₁)) eq | inl refl | inl refl with decidableGroups j ((j + g) h1) (Group.0G (G j))
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (prependLetter .j h1 nonZero₁ w1 x)) (nonempty .j (prependLetter .j h2 nonZero₂ w2 x₁)) eq | inl refl | inl refl | inl eq1 with decidableGroups j ((j + g) h2) (Group.0G (G j))
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (prependLetter .j h1 nonZero₁ w1 x)) (nonempty .j (prependLetter .j h2 nonZero₂ w2 x₁)) eq | inl refl | inl refl | inl eq1 | inl x₂ with decidableIndex j j
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (prependLetter .j h1 nonZero₁ w1 x)) (nonempty .j (prependLetter .j h2 nonZero₂ w2 x₁)) eq | inl refl | inl refl | inl eq1 | inl x₂ | inl refl = _&&_.snd eq
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (prependLetter .j h1 nonZero₁ w1 x)) (nonempty .j (prependLetter .j h2 nonZero₂ w2 x₁)) eq | inl refl | inl refl | inl eq1 | inr neq2 with decidableIndex j j
  ... | inl refl = exFalso (neq2 (Equivalence.transitive (Setoid.eq (S j)) (Group.+WellDefined (G j) (Equivalence.reflexive (Setoid.eq (S j))) (Equivalence.symmetric (Setoid.eq (S j)) (_&&_.fst eq))) eq1))
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (prependLetter .j h1 nonZero₁ w1 x)) (nonempty .j (prependLetter .j h2 nonZero₂ w2 x₁)) eq | inl refl | inl refl | inr neq1 with decidableGroups j ((j + g) h2) (Group.0G (G j))
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (prependLetter .j h1 nonZero₁ w1 x)) (nonempty .j (prependLetter .j h2 nonZero₂ w2 x₁)) eq | inl refl | inl refl | inr neq1 | inl eq2 with decidableIndex j j
  ... | inl refl = exFalso (neq1 (Equivalence.transitive (Setoid.eq (S j)) (Group.+WellDefined (G j) (Equivalence.reflexive (Setoid.eq (S j))) (_&&_.fst eq)) eq2))
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (prependLetter .j h1 nonZero₁ w1 x)) (nonempty .j (prependLetter .j h2 nonZero₂ w2 x₁)) eq | inl refl | inl refl | inr neq1 | inr x₂ with decidableIndex j j
  ... | inl refl = Group.+WellDefined (G j) (Equivalence.reflexive (Setoid.eq (S j))) (_&&_.fst eq) ,, _&&_.snd eq
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (ofEmpty .j g₁ nonZero₁)) (nonempty i2 (ofEmpty .i2 g₂ nonZero₂)) eq | inl refl | inr x with decidableIndex j i2
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (ofEmpty .j g₁ nonZero₁)) (nonempty .j (ofEmpty .j g₂ nonZero₂)) eq | inl refl | inr x | inl refl = exFalso (x refl)
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty .j (prependLetter .j g₁ nonZero₁ w1 x₁)) (nonempty i2 (prependLetter .i2 g₂ nonZero₂ w2 x₂)) eq | inl refl | inr x with decidableIndex j i2
  plus'WD' {.i2} (ofEmpty .i2 g nonZero) (nonempty .i2 (prependLetter .i2 g₁ nonZero₁ w1 x₁)) (nonempty i2 (prependLetter .i2 g₂ nonZero₂ w2 x₂)) eq | inl refl | inr x | inl refl = exFalso (x refl)
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty i1 w1) (nonempty i2 w2) eq | inr j!=i1 with decidableIndex j i2
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty i1 (ofEmpty .i1 g₁ nonZero₁)) (nonempty .j (ofEmpty .j g₂ nonZero₂)) eq | inr j!=i1 | inl refl with decidableIndex i1 j
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty i1 (ofEmpty .i1 g₁ nonZero₁)) (nonempty .j (ofEmpty .j g₂ nonZero₂)) eq | inr j!=i1 | inl refl | inl x = exFalso (j!=i1 (equalityCommutative x))
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty i1 (prependLetter .i1 g₁ nonZero₁ w1 x)) (nonempty .j (prependLetter .j g₂ nonZero₂ w2 x₁)) eq | inr j!=i1 | inl refl with decidableIndex i1 j
  ... | inl bad = exFalso (j!=i1 (equalityCommutative bad))
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty i1 w1) (nonempty i2 w2) eq | inr j!=i1 | inr j!=i2 with decidableIndex j j
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty i1 w1) (nonempty i2 w2) eq | inr j!=i1 | inr j!=i2 | inl refl = Equivalence.reflexive (Setoid.eq (S j)) ,, eq
  plus'WD' {j} (ofEmpty j g nonZero) (nonempty i1 w1) (nonempty i2 w2) eq | inr j!=i1 | inr j!=i2 | inr x = exFalso (x refl)
  plus'WD' {j} (prependLetter j g nonZero l x) (nonempty i (ofEmpty .i h1 nonZero1)) (nonempty i2 (ofEmpty .i2 h2 nonZero2)) eq with decidableIndex i i2
  ... | inl refl = prependWD' g nonZero (plus' l (nonempty i (ofEmpty i h1 nonZero1))) (plus' l (nonempty i2 (ofEmpty i2 h2 nonZero2))) (plus'WD' l (nonempty i2 (ofEmpty i2 h1 nonZero1)) (nonempty i2 (ofEmpty i2 h2 nonZero2)) t)
    where
      t : =RP' (ofEmpty i2 h1 nonZero1) (ofEmpty i2 h2 nonZero2)
      t with decidableIndex i2 i2
      t | inl refl = eq
      t | inr x = exFalso (x refl)
  ... | inr i!=i2 = exFalso' eq
  plus'WD' {j} (prependLetter j g nonZero l x) (nonempty i (prependLetter .i g₁ nonZero₁ w1 x₁)) (nonempty i2 (prependLetter .i2 g₂ nonZero₂ w2 x₂)) eq with decidableIndex i i2
  plus'WD' {j} (prependLetter j g nonZero l x) (nonempty i (prependLetter .i h1 nonZero1 w1 x1)) (nonempty .i (prependLetter .i h2 nonZero2 w2 x2)) eq | inl refl = prependWD' g nonZero (plus' l (nonempty i (prependLetter i h1 nonZero1 w1 x1))) (plus' l (nonempty i (prependLetter i h2 nonZero2 w2 x2))) (plus'WD' l (nonempty i (prependLetter i h1 nonZero1 w1 x1)) (nonempty i (prependLetter i h2 nonZero2 w2 x2)) (prependLetterWD (_&&_.fst eq) nonZero1 nonZero2 w1 w2 (_&&_.snd eq) x1 x2))

abstract
  plusEmptyRight : {i : I} (x : ReducedSequenceBeginningWith i) → _=RP_ (plus' x empty) (nonempty i x)
  plusEmptyRight (ofEmpty i g nonZero) with decidableIndex i i
  plusEmptyRight (ofEmpty i g nonZero) | inl refl = Equivalence.reflexive (Setoid.eq (S i))
  plusEmptyRight (ofEmpty i g nonZero) | inr x = exFalso (x refl)
  plusEmptyRight (prependLetter i g nonZero {j} x i!=j) with plusEmptyRight x
  ... | b with plus' x empty
  plusEmptyRight (prependLetter i g nonZero {j} x i!=j) | b | nonempty k w with decidableIndex i k
  plusEmptyRight (prependLetter .k g nonZero {j} x i!=j) | b | nonempty k (ofEmpty .k h nonZero₁) | inl refl with decidableGroups k ((k + g) h) (Group.0G (G k))
  plusEmptyRight (prependLetter .k g nonZero {.i} (ofEmpty i g₁ nonZero₂) i!=j) | b | nonempty k (ofEmpty .k h nonZero₁) | inl refl | inl g+k=hinv with decidableIndex k i
  plusEmptyRight (prependLetter .i g nonZero {.i} (ofEmpty i g₁ nonZero₂) i!=j) | b | nonempty .i (ofEmpty .i h nonZero₁) | inl refl | inl g+k=hinv | inl refl = exFalso (i!=j refl)
  plusEmptyRight (prependLetter .k g nonZero {.i} (ofEmpty i g₁ nonZero₂) i!=j) | b | nonempty k (ofEmpty .k h nonZero₁) | inl refl | inr x₁ with decidableIndex k i
  plusEmptyRight (prependLetter .i g nonZero {.i} (ofEmpty i g₁ nonZero₂) i!=j) | b | nonempty .i (ofEmpty .i h nonZero₁) | inl refl | inr x₁ | inl refl = exFalso (i!=j refl)
  plusEmptyRight (prependLetter .k g nonZero {j} w1 i!=j) | b | nonempty k (prependLetter .k h nonZero₁ w x₁) | inl refl with decidableGroups k ((k + g) h) (Group.0G (G k))
  plusEmptyRight (prependLetter .k g nonZero {.i} (prependLetter i g₁ nonZero₂ w1 x) i!=j) | b | nonempty k (prependLetter .k h nonZero₁ w x₁) | inl refl | inl p with decidableIndex k i
  plusEmptyRight (prependLetter .i g nonZero {.i} (prependLetter i g₁ nonZero₂ w1 x) i!=j) | b | nonempty .i (prependLetter .i h nonZero₁ w x₁) | inl refl | inl p | inl refl = exFalso (i!=j refl)
  plusEmptyRight (prependLetter .k g nonZero {j} w1 i!=j) | b | nonempty k (prependLetter .k h nonZero₁ w x₁) | inl refl | inr x₂ with decidableIndex k k
  plusEmptyRight (prependLetter .k g nonZero {.i} (prependLetter i g₁ nonZero₂ w1 x) i!=j) | b | nonempty k (prependLetter .k h nonZero₁ w x₁) | inl refl | inr x₂ | inl refl with decidableIndex k i
  plusEmptyRight (prependLetter .i g nonZero {.i} (prependLetter i g₁ nonZero₂ w1 x) i!=j) | b | nonempty .i (prependLetter .i h nonZero₁ w x₁) | inl refl | inr x₂ | inl refl | inl refl = exFalso (i!=j refl)
  plusEmptyRight (prependLetter .k g nonZero {j} w1 i!=j) | b | nonempty k (prependLetter .k h nonZero₁ w x₁) | inl refl | inr x₂ | inr x = exFalso (x refl)
  plusEmptyRight (prependLetter i g nonZero {j} w1 i!=j) | b | nonempty k w | inr i!=k with decidableIndex i i
  plusEmptyRight (prependLetter i g nonZero {j} w1 i!=j) | b | nonempty k w | inr i!=k | inl refl = Equivalence.reflexive (Setoid.eq (S i)) ,, b
  plusEmptyRight (prependLetter i g nonZero {j} w1 i!=j) | b | nonempty k w | inr i!=k | inr x = exFalso (x refl)

abstract
  prependFrom : {i : I} (g1 g2 : A i) (pr : (Setoid._∼_ (S i) (_+_ i g1 g2) (Group.0G (G i))) → False) (c : ReducedSequence) .(p2 : _) .(p3 : _) → prepend i (_+_ i g1 g2) pr c =RP prepend i g1 p2 (prepend i g2 p3 c)
  prependFrom {i} g1 g2 pr empty _ _ with decidableIndex i i
  prependFrom {i} g1 g2 pr empty _ _ | inl refl with decidableGroups i ((i + g1) g2) (Group.0G (G i))
  prependFrom {i} g1 g2 pr empty _ _ | inl refl | inl bad = exFalso (pr bad)
  prependFrom {i} g1 g2 pr empty _ _ | inl refl | inr _ with decidableIndex i i
  prependFrom {i} g1 g2 pr empty _ _ | inl refl | inr _ | inl refl = Equivalence.reflexive (Setoid.eq (S i))
  prependFrom {i} g1 g2 pr empty _ _ | inl refl | inr _ | inr bad = exFalso (bad refl)
  prependFrom {i} g1 g2 pr empty _ _ | inr bad = exFalso (bad refl)
  prependFrom {i} g1 g2 pr (nonempty j x) _ _ with decidableIndex i j
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl with decidableGroups j ((j + (j + g1) g2) g) (Group.0G (G j))
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inl eq with decidableGroups j ((j + g2) g) (Group.0G (G j))
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) g1Nonzero _ | inl refl | inl eq3 | inl eq2 = exFalso (g1Nonzero t)
    where
      open Setoid (S j)
      open Group (G j)
      open Equivalence eq
      t : g1 ∼ 0G
      t = transitive (symmetric identRight) (transitive (+WellDefined reflexive (symmetric eq2)) (transitive +Associative eq3))
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inl eq | inr neq with decidableIndex j j
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inl eq | inr neq | inl refl with decidableGroups j ((j + g1) ((j + g2) g)) (Group.0G (G j))
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inl eq | inr neq | inl refl | inl eq2 = record {}
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inl eq | inr neq | inl refl | inr neq2 = exFalso (neq2 (Equivalence.transitive (Setoid.eq (S j)) (Group.+Associative (G j)) eq))
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inl eq | inr neq | inr bad = exFalso (bad refl)
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inr neq with decidableGroups j ((j + g2) g) (Group.0G (G j))
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inr neq | inl eq2 with decidableIndex j j
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inr neq | inl eq2 | inl refl = transitive (symmetric +Associative) (transitive (+WellDefined reflexive eq2) identRight)
    where
      open Setoid (S j)
      open Group (G j)
      open Equivalence eq
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inr neq | inl eq2 | inr bad = exFalso (bad refl)
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inr neq | inr neq2 with decidableIndex j j
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inr neq | inr neq2 | inl refl with decidableGroups j ((j + g1) ((j + g2) g)) (Group.0G (G j))
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inr neq | inr neq2 | inl refl | inl eq2 = exFalso (neq (Equivalence.transitive (Setoid.eq (S j)) (Equivalence.symmetric (Setoid.eq (S j)) (Group.+Associative (G j))) eq2))
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inr neq | inr neq2 | inl refl | inr neq3 with decidableIndex j j
  ... | inl refl = Equivalence.symmetric (Setoid.eq (S j)) (Group.+Associative (G j))
  ... | inr bad = exFalso (bad refl)
  prependFrom {.j} g1 g2 pr (nonempty _ (ofEmpty j g nonZero)) _ _ | inl refl | inr neq | inr neq2 | inr bad = exFalso (bad refl)
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero x x₁)) _ _ | inl refl with decidableGroups j ((j + (j + g1) g2) g) (Group.0G (G j))
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero x x₁)) _ _ | inl refl | inl eq1 with decidableGroups j ((j + g2) g) (Group.0G (G j))
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero {k} x x₁)) p2 _ | inl refl | inl eq1 | inl eq2 = exFalso (p2 (transitive (transitive (symmetric identRight) (transitive (+WellDefined reflexive (symmetric eq2)) +Associative)) eq1))
    where
      open Setoid (S j)
      open Group (G j)
      open Equivalence eq
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero x x₁)) _ _ | inl refl | inl eq1 | inr neq with decidableIndex j j
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero x x₁)) _ _ | inl refl | inl eq1 | inr neq | inl refl with decidableGroups j ((j + g1) ((j + g2) g)) (Group.0G (G j))
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero x x₁)) _ _ | inl refl | inl eq1 | inr neq | inl refl | inl eq2 = =RP'reflex x
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero x x₁)) _ _ | inl refl | inl eq1 | inr neq | inl refl | inr neq2 = exFalso (neq2 (Equivalence.transitive (Setoid.eq (S j)) (Group.+Associative (G j)) eq1))
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero x x₁)) _ _ | inl refl | inl eq1 | inr neq | inr bad = exFalso (bad refl)
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero x x₁)) _ _ | inl refl | inr neq1 with decidableGroups j ((j + g2) g) (Group.0G (G j))
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero {k} x x₁)) _ _ | inl refl | inr neq1 | inl eq1 with decidableIndex j k
  prependFrom {j} g1 g2 pr (nonempty _ (prependLetter _ g nonZero {_} (ofEmpty _ h nonZero₁) bad)) _ _ | inl refl | inr neq1 | inl eq1 | inl refl = exFalso (bad refl)
  prependFrom {_} g1 g2 pr (nonempty _ (prependLetter _ g nonZero {_} (prependLetter _ g₁ nonZero₁ x x₂) bad)) _ _ | inl refl | inr neq1 | inl eq1 | inl refl = exFalso (bad refl)
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero {k} x x₁)) _ _ | inl refl | inr neq1 | inl eq1 | inr j!=k with decidableIndex j j
  ... | inl refl = transitive (symmetric +Associative) (transitive (+WellDefined reflexive eq1) identRight) ,, =RP'reflex x
    where
      open Setoid (S j)
      open Group (G j)
      open Equivalence eq
  ... | inr bad = exFalso (bad refl)
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero x x₁)) _ _ | inl refl | inr neq1 | inr neq2 with decidableIndex j j
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero x x₁)) _ _ | inl refl | inr neq1 | inr neq2 | inl refl with decidableGroups j ((j + g1) ((j + g2) g)) (Group.0G (G j))
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero x x₁)) _ _ | inl refl | inr neq1 | inr neq2 | inl refl | inl eq1 = exFalso (neq1 (transitive (symmetric +Associative) eq1))
    where
      open Setoid (S j)
      open Group (G j)
      open Equivalence eq
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero x x₁)) _ _ | inl refl | inr neq1 | inr neq2 | inl refl | inr neq3 with decidableIndex j j
  ... | inl refl = Equivalence.symmetric (Setoid.eq (S j)) (Group.+Associative (G j)) ,, =RP'reflex x
  ... | inr bad = exFalso (bad refl)
  prependFrom {.j} g1 g2 pr (nonempty _ (prependLetter j g nonZero x x₁)) _ _ | inl refl | inr neq1 | inr neq2 | inr bad = exFalso (bad refl)
  prependFrom {i} g1 g2 pr (nonempty j x) _ _  | inr i!=j with decidableIndex i i
  prependFrom {i} g1 g2 pr (nonempty j x) _ _  | inr i!=j | inl refl with decidableGroups i ((i + g1) g2) (Group.0G (G i))
  prependFrom {i} g1 g2 pr (nonempty j x) _ _ | inr i!=j | inl refl | inl eq1 = exFalso (pr eq1)
  prependFrom {i} g1 g2 pr (nonempty j x) _ _ | inr i!=j | inl refl | inr neq1 with decidableIndex i i
  prependFrom {i} g1 g2 pr (nonempty j x) _ _ | inr i!=j | inl refl | inr neq1 | inl refl = Equivalence.reflexive (Setoid.eq (S i)) ,, =RP'reflex x
  prependFrom {i} g1 g2 pr (nonempty j x) _ _ | inr i!=j | inl refl | inr neq1 | inr bad = exFalso (bad refl)
  prependFrom {i} g1 g2 pr (nonempty j x) _ _  | inr i!=j | inr bad = exFalso (bad refl)

  prependFrom' : {i : I} (g h : A i) (pr : (Setoid._∼_ (S i) (_+_ i g h) (Group.0G (G i)))) (c : ReducedSequence) .(p2 : _) .(p3 : _) → prepend i g p2 (prepend i h p3 c) =RP c
  prependFrom' {i} g h pr empty _ _ with decidableIndex i i
  prependFrom' {i} g h pr empty _ _ | inl refl with decidableGroups i ((i + g) h) (Group.0G (G i))
  ... | inl _ = record {}
  ... | inr bad = exFalso (bad pr)
  prependFrom' {i} g h pr empty _ _ | inr bad = exFalso (bad refl)
  prependFrom' {i} g h pr (nonempty j x) _ _ with decidableIndex i j
  prependFrom' {.j} g h pr (nonempty j (ofEmpty .j g1 nonZero)) _ _ | inl refl with decidableGroups j ((j + h) g1) (Group.0G (G j))
  prependFrom' {.j} g h pr (nonempty j (ofEmpty .j g1 nonZero)) _ _ | inl refl | inl eq1 with decidableIndex j j
  prependFrom' {.j} g h pr (nonempty j (ofEmpty .j g1 nonZero)) _ _ | inl refl | inl eq1 | inl refl = transitive t (symmetric u)
    where
      open Setoid (S j)
      open Equivalence eq
      t : Setoid._∼_ (S j) g (Group.inverse (G j) h)
      t = rightInversesAreUnique (G j) pr
      u : Setoid._∼_ (S j) g1 (Group.inverse (G j) h)
      u = leftInversesAreUnique (G j) eq1
  prependFrom' {.j} g h pr (nonempty j (ofEmpty .j g1 nonZero)) _ _ | inl refl | inl eq1 | inr bad = exFalso (bad refl)
  prependFrom' {.j} g h pr (nonempty j (ofEmpty .j g1 nonZero)) _ _ | inl refl | inr neq with decidableIndex j j
  prependFrom' {.j} g h pr (nonempty j (ofEmpty .j g1 nonZero)) p2 _ | inl refl | inr neq | inl refl with decidableGroups j ((j + g) ((j + h) g1)) (Group.0G (G j))
  ... | inl eq1 = exFalso (nonZero t)
    where
      open Setoid (S j)
      open Equivalence eq
      open Group (G j)
      t : g1 ∼ 0G
      t = transitive (transitive (symmetric identLeft) (transitive (+WellDefined (symmetric pr) reflexive) (symmetric +Associative))) eq1
  prependFrom' {.j} g h pr (nonempty j (ofEmpty .j g1 nonZero)) _ _ | inl refl | inr neq | inl refl | inr neq2 with decidableIndex j j
  ... | inl refl = transitive (transitive +Associative (+WellDefined pr reflexive)) identLeft
    where
      open Setoid (S j)
      open Equivalence eq
      open Group (G j)
  ... | inr bad = exFalso (bad refl)
  prependFrom' {.j} g h pr (nonempty j (ofEmpty .j g1 nonZero)) _ _ | inl refl | inr neq | inr bad = exFalso (bad refl)
  prependFrom' {.j} g h pr (nonempty j (prependLetter .j g1 nonZero x x₁)) _ _ | inl refl with decidableGroups j ((j + h) g1) (Group.0G (G j))
  prependFrom' {.j} g h pr (nonempty j (prependLetter .j g1 nonZero {k} x bad)) _ _ | inl refl | inl eq1 with decidableIndex j k
  prependFrom' {.j} g h pr (nonempty j (prependLetter .j g1 nonZero {k} x bad)) _ _ | inl refl | inl eq1 | inl j=k = exFalso (bad j=k)
  prependFrom' {.j} g h pr (nonempty j (prependLetter .j g1 nonZero {k} x bad)) _ _ | inl refl | inl eq1 | inr j!=k with decidableIndex j j
  prependFrom' {.j} g h pr (nonempty j (prependLetter .j g1 nonZero {k} x bad)) _ _ | inl refl | inl eq1 | inr j!=k | inl refl = transitive {g} {inverse h} (rightInversesAreUnique (G j) pr) (symmetric (leftInversesAreUnique (G j) eq1)) ,, =RP'reflex x
    where
      open Setoid (S j)
      open Equivalence eq
      open Group (G j)
  prependFrom' {.j} g h pr (nonempty j (prependLetter .j g1 nonZero {k} x _)) _ _ | inl refl | inl eq1 | inr j!=k | inr bad = exFalso (bad refl)
  prependFrom' {.j} g h pr (nonempty j (prependLetter .j g1 nonZero {k} x x₁)) _ _ | inl refl | inr neq1 with decidableIndex j j
  prependFrom' {.j} g h pr (nonempty j (prependLetter .j g1 nonZero {k} x x₁)) _ _ | inl refl | inr neq1 | inl refl with decidableGroups j ((j + g) ((j + h) g1)) (Group.0G (G j))
  prependFrom' {.j} g h pr (nonempty j (prependLetter .j g1 nonZero {k} x x₁)) _ _ | inl refl | inr neq1 | inl refl | inl eq1 = exFalso (nonZero (transitive (transitive (symmetric identLeft) (transitive (+WellDefined (symmetric pr) reflexive) (symmetric +Associative))) eq1))
    where
      open Setoid (S j)
      open Equivalence eq
      open Group (G j)
  prependFrom' {.j} g h pr (nonempty j (prependLetter .j g1 nonZero {k} x x₁)) _ _ | inl refl | inr neq1 | inl refl | inr neq2 with decidableIndex j j
  prependFrom' {.j} g h pr (nonempty j (prependLetter .j g1 nonZero {k} x x₁)) _ _ | inl refl | inr neq1 | inl refl | inr neq2 | inl refl = transitive +Associative (transitive (+WellDefined pr reflexive) identLeft) ,, =RP'reflex x
    where
      open Setoid (S j)
      open Equivalence eq
      open Group (G j)
  prependFrom' {.j} g h pr (nonempty j (prependLetter .j g1 nonZero {k} x x₁)) _ _ | inl refl | inr neq1 | inl refl | inr neq2 | inr bad = exFalso (bad refl)
  prependFrom' {.j} g h pr (nonempty j (prependLetter .j g1 nonZero {k} x x₁)) _ _ | inl refl | inr neq1 | inr bad = exFalso (bad refl)
  prependFrom' {i} g h pr (nonempty j x) _ _ | inr i!=j with decidableIndex i i
  prependFrom' {i} g h pr (nonempty j x) _ _ | inr i!=j | inl refl with decidableGroups i ((i + g) h) (Group.0G (G i))
  prependFrom' {i} g h pr (nonempty j x) _ _ | inr i!=j | inl refl | inl eq1 = =RP'reflex x
  prependFrom' {i} g h pr (nonempty j x) _ _ | inr i!=j | inl refl | inr neq1 = exFalso (neq1 pr)
  prependFrom' {i} g h pr (nonempty j x) _ _ | inr i!=j | inr bad = exFalso (bad refl)

ext: agda


text:
-- Interface to standard library.

module Library where

open import Function public
  hiding (_∋_)

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

open import Size public

open import Category.Monad public
  using (RawMonad; module RawMonad)

open import Data.Empty public
  using (⊥; ⊥-elim)

open import Data.List public
  using (List; []; _∷_; map)

open import Data.Maybe public
  using (Maybe; just; nothing) renaming (map to fmap)

open import Data.Nat public
  using (ℕ; zero; suc; _+_; _≟_)

open import Data.Product public
  using (∃; _×_; _,_) renaming (proj₁ to fst; proj₂ to snd)
--infixr 1 _,_

open import Data.Sum public
  using (_⊎_; [_,_]′) renaming (inj₁ to inl; inj₂ to inr)

open import Data.Unit  public
  using (⊤)

open import Function public
  using (_∘_; flip; case_of_)
  renaming (id to idf)

open import Relation.Nullary public
  using (Dec; yes; no)

open import Relation.Binary public
  using (Setoid; module Setoid)

import Relation.Binary.PreorderReasoning
module Pre = Relation.Binary.PreorderReasoning

open import Relation.Binary.PropositionalEquality public
  using ( _≡_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning
        ; inspect; [_])

--open ≡-Reasoning renaming (begin_ to proof_) public

open import Relation.Binary.HeterogeneousEquality public
  using (_≅_; refl; ≡-to-≅; module ≅-Reasoning)
  renaming (sym to hsym; trans to htrans; cong to hcong;
            cong₂ to hcong₂; subst to hsubst)
{-
hcong₃ : {A : Set}
         {B : A → Set}
         {C : ∀ a → B a → Set}
         {D : ∀ a b → C a b → Set}
         (f : ∀ a b c → D a b c)
         {a a' : A} → a ≅ a' →
         {b : B a}{b' : B a'} → b ≅ b' →
         {c : C a b}{c' : C a' b'} → c ≅ c' →
         f a b c ≅ f a' b' c'
hcong₃ f refl refl refl = refl

≅-to-≡ : ∀ {a} {A : Set a} {x y : A} → x ≅ y → x ≡ y
≅-to-≡ refl = refl

record Cat : Set1 where
  field Obj  : Set
        Hom  : Obj → Obj → Set
        iden : ∀{X} → Hom X X
        comp : ∀{X Y Z} → Hom Y Z → Hom X Y → Hom X Z
        idl  : ∀{X Y}{f : Hom X Y} → comp iden f ≅ f
        idr  : ∀{X Y}{f : Hom X Y} → comp f iden ≅ f
        ass  : ∀{W X Y Z}{f : Hom Y Z}{g : Hom X Y}{h : Hom W X} →
               comp (comp f g) h ≅ comp f (comp g h)
open Cat public

record Fun (C D : Cat) : Set where
  open Cat
  field OMap  : Obj C → Obj D
        HMap  : ∀{X Y} → Hom C X Y → Hom D (OMap X) (OMap Y)
        fid   : ∀{X} → HMap (iden C {X}) ≅ iden D {OMap X}
        fcomp : ∀{X Y Z}{f : Hom C Y Z}{g : Hom C X Y} →
                HMap (comp C f g) ≅ comp D (HMap f) (HMap g)

open Fun public

postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} →
                (∀ a → f a ≅ g a) → f ≅ g

postulate iext : {A : Set}{B B' : A → Set}
                 {f : ∀ {a} → B a}{g : ∀{a} → B' a} →
                 (∀ a → f {a} ≅ g {a}) →
                 _≅_ {_}{ {a : A} → B a} f { {a : A} → B' a} g
-}

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Universe.Base where

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
open import Data.Product renaming (_,_ to _,,_) -- just to avoid clash with other commas
open import Algebra.Structures           using (IsSemigroup)
open import Algebra.FunctionProperties   using (LeftIdentity; Commutative)

module Preliminaries where

Rel : Set -> Set₁
Rel A  =  A -> A -> Set

Entire : {A B : Set} -> (_R_ : A -> B -> Set) -> Set
Entire _R_ = ∀ a -> ∃ \ b -> a R b

fun : {A B : Set} -> {_R_ : A -> B -> Set} -> Entire _R_ -> A -> B
fun ent a = proj₁ (ent a)

correct :  {A B : Set} -> {_R_ : A -> B -> Set} -> (ent : Entire _R_) ->
           let f = fun ent in  ∀ {a : A} -> a R (f a)
correct ent {a} = proj₂ (ent a)

Entire3 : {A B C D : Set} -> (R : A -> B -> C -> D -> Set) -> Set
Entire3 R = ∀ x y z -> ∃ (R x y z)

fun3 : {A B C D : Set} -> {R : A -> B -> C -> D -> Set} -> Entire3 R -> A -> B -> C -> D
fun3 ent a b c = proj₁ (ent a b c)

correct3 :  {A B C D : Set} -> {R : A -> B -> C -> D -> Set} -> (e : Entire3 R) ->
           ∀ {a : A} {b : B} {c : C} -> R a b c (fun3 e a b c)
correct3 ent {a} {b} {c} = proj₂ (ent a b c)

UniqueSolution : {A : Set} -> Rel A -> (A -> Set) -> Set
UniqueSolution _≃_ P = ∀ {x y} -> P x -> P y  ->  x ≃ y

LowerBound : {A : Set} -> Rel A -> (A -> Set) -> (A -> Set)
LowerBound _≤_ P  a = ∀ z -> (P z -> a ≤ z)

Least   : {A : Set} -> Rel A -> (A -> Set) -> (A -> Set)
Least   _≤_ P  a =  P a  ×  LowerBound _≤_ P a

max_stars_repo_name: DSLsofMath/ValiantAgda

max_issues_repo_name: DSLsofMath/ValiantAgda

max_forks_repo_name: DSLsofMath/ValiantAgda


text:
------------------------------------------------------------------------------
-- The division specification
------------------------------------------------------------------------------

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

module FOTC.Program.Division.Specification where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities

------------------------------------------------------------------------------
-- Specification: The division is total and the result is correct.
divSpec : D → D → D → Set
divSpec i j q = N q ∧ (∃[ r ] N r ∧ r < j ∧ i ≡ j * q + r)
{-# ATP definition divSpec #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Andreas, 2016-06-11

postulate Foo : Foo → Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
----------------------------------------------------------------------------------
-- Types for parse trees
----------------------------------------------------------------------------------

module options-types where

open import ial
open import parse-tree

posinfo = string
alpha = string
alpha-bar-4 = string
alpha-range-2 = string
alpha-range-3 = string
anychar = string
anychar-bar-10 = string
anychar-bar-11 = string
anychar-bar-12 = string
anychar-bar-13 = string
anychar-bar-14 = string
anychar-bar-15 = string
anychar-bar-16 = string
anychar-bar-17 = string
anychar-bar-18 = string
anychar-bar-19 = string
anychar-bar-20 = string
anychar-bar-21 = string
anychar-bar-22 = string
anychar-bar-23 = string
anychar-bar-24 = string
anychar-bar-25 = string
anychar-bar-26 = string
anychar-bar-27 = string
anychar-bar-28 = string
anychar-bar-29 = string
anychar-bar-9 = string
num = string
num-plus-6 = string
numone = string
numone-range-5 = string
numpunct = string
numpunct-bar-7 = string
numpunct-bar-8 = string
path = string
path-star-1 = string

{-# FOREIGN GHC import qualified CedilleOptionsParser #-}
{-# FOREIGN GHC import qualified CedilleOptionsLexer #-}

data paths : Set where
    PathsCons : path → paths → paths
    PathsNil : paths
{-# COMPILE GHC paths = data CedilleOptionsLexer.Paths (CedilleOptionsLexer.PathsCons | CedilleOptionsLexer.PathsNil) #-}

--data data-encoding : Set where
--  Mendler : data-encoding
--  Mendler-old : data-encoding
--{-# COMPILE GHC data-encoding = data CedilleOptionsLexer.DataEnc (CedilleOptionsLexer.Mendler | CedilleOptionsLexer.MendlerOld) #-}

data opt : Set where
    GenerateLogs : 𝔹 → opt
    Lib : paths → opt
    MakeRktFiles : 𝔹 → opt
    ShowQualifiedVars : 𝔹 → opt
    UseCedeFiles : 𝔹 → opt
    EraseTypes : 𝔹 → opt
    PrettyPrintColumns : string → opt
    DatatypeEncoding : maybe path → opt
{-# COMPILE GHC opt = data CedilleOptionsLexer.Opt (CedilleOptionsLexer.GenerateLogs | CedilleOptionsLexer.Lib | CedilleOptionsLexer.MakeRktFiles | CedilleOptionsLexer.ShowQualifiedVars | CedilleOptionsLexer.UseCedeFiles | CedilleOptionsLexer.EraseTypes | CedilleOptionsLexer.PrintColumns | CedilleOptionsLexer.DatatypeEncoding) #-}

data opts : Set where
    OptsCons : opt → opts → opts
    OptsNil : opts
{-# COMPILE GHC opts = data CedilleOptionsLexer.Opts (CedilleOptionsLexer.OptsCons | CedilleOptionsLexer.OptsNil) #-}

data start : Set where
    File : opts → start
{-# COMPILE GHC start = data CedilleOptionsLexer.Start (CedilleOptionsLexer.File) #-}

data Either (A : Set)(B : Set) : Set where
  Left : A → Either A B
  Right : B → Either A B
{-# COMPILE GHC Either = data Either (Left | Right) #-}

postulate
  scanOptions  : string → Either string start

{-# COMPILE GHC scanOptions = CedilleOptionsParser.parseOptions #-}

-- embedded types:

data ParseTreeT : Set where
  parsed-opt : opt → ParseTreeT
  parsed-opts : opts → ParseTreeT
  parsed-paths : paths → ParseTreeT
  parsed-start : start → ParseTreeT
  parsed-bool : 𝔹 → ParseTreeT
  parsed-posinfo : posinfo → ParseTreeT
  parsed-alpha : alpha → ParseTreeT
  parsed-alpha-bar-4 : alpha-bar-4 → ParseTreeT
  parsed-alpha-range-2 : alpha-range-2 → ParseTreeT
  parsed-alpha-range-3 : alpha-range-3 → ParseTreeT
  parsed-anychar : anychar → ParseTreeT
  parsed-anychar-bar-10 : anychar-bar-10 → ParseTreeT
  parsed-anychar-bar-11 : anychar-bar-11 → ParseTreeT
  parsed-anychar-bar-12 : anychar-bar-12 → ParseTreeT
  parsed-anychar-bar-13 : anychar-bar-13 → ParseTreeT
  parsed-anychar-bar-14 : anychar-bar-14 → ParseTreeT
  parsed-anychar-bar-15 : anychar-bar-15 → ParseTreeT
  parsed-anychar-bar-16 : anychar-bar-16 → ParseTreeT
  parsed-anychar-bar-17 : anychar-bar-17 → ParseTreeT
  parsed-anychar-bar-18 : anychar-bar-18 → ParseTreeT
  parsed-anychar-bar-19 : anychar-bar-19 → ParseTreeT
  parsed-anychar-bar-20 : anychar-bar-20 → ParseTreeT
  parsed-anychar-bar-21 : anychar-bar-21 → ParseTreeT
  parsed-anychar-bar-22 : anychar-bar-22 → ParseTreeT
  parsed-anychar-bar-23 : anychar-bar-23 → ParseTreeT
  parsed-anychar-bar-24 : anychar-bar-24 → ParseTreeT
  parsed-anychar-bar-25 : anychar-bar-25 → ParseTreeT
  parsed-anychar-bar-26 : anychar-bar-26 → ParseTreeT
  parsed-anychar-bar-27 : anychar-bar-27 → ParseTreeT
  parsed-anychar-bar-28 : anychar-bar-28 → ParseTreeT
  parsed-anychar-bar-29 : anychar-bar-29 → ParseTreeT
  parsed-anychar-bar-9 : anychar-bar-9 → ParseTreeT
  parsed-num : num → ParseTreeT
  parsed-num-plus-6 : num-plus-6 → ParseTreeT
  parsed-numone : numone → ParseTreeT
  parsed-numone-range-5 : numone-range-5 → ParseTreeT
  parsed-numpunct : numpunct → ParseTreeT
  parsed-numpunct-bar-7 : numpunct-bar-7 → ParseTreeT
  parsed-numpunct-bar-8 : numpunct-bar-8 → ParseTreeT
  parsed-path : path → ParseTreeT
  parsed-path-star-1 : path-star-1 → ParseTreeT
  parsed-aws : ParseTreeT
  parsed-aws-bar-31 : ParseTreeT
  parsed-aws-bar-32 : ParseTreeT
  parsed-aws-bar-33 : ParseTreeT
  parsed-comment : ParseTreeT
  parsed-comment-star-30 : ParseTreeT
  parsed-ows : ParseTreeT
  parsed-ows-star-35 : ParseTreeT
  parsed-squote : ParseTreeT
  parsed-ws : ParseTreeT
  parsed-ws-plus-34 : ParseTreeT

------------------------------------------
-- Parse tree printing functions
------------------------------------------

posinfoToString : posinfo → string
posinfoToString x = "(posinfo " ^ x ^ ")"
alphaToString : alpha → string
alphaToString x = "(alpha " ^ x ^ ")"
alpha-bar-4ToString : alpha-bar-4 → string
alpha-bar-4ToString x = "(alpha-bar-4 " ^ x ^ ")"
alpha-range-2ToString : alpha-range-2 → string
alpha-range-2ToString x = "(alpha-range-2 " ^ x ^ ")"
alpha-range-3ToString : alpha-range-3 → string
alpha-range-3ToString x = "(alpha-range-3 " ^ x ^ ")"
anycharToString : anychar → string
anycharToString x = "(anychar " ^ x ^ ")"
anychar-bar-10ToString : anychar-bar-10 → string
anychar-bar-10ToString x = "(anychar-bar-10 " ^ x ^ ")"
anychar-bar-11ToString : anychar-bar-11 → string
anychar-bar-11ToString x = "(anychar-bar-11 " ^ x ^ ")"
anychar-bar-12ToString : anychar-bar-12 → string
anychar-bar-12ToString x = "(anychar-bar-12 " ^ x ^ ")"
anychar-bar-13ToString : anychar-bar-13 → string
anychar-bar-13ToString x = "(anychar-bar-13 " ^ x ^ ")"
anychar-bar-14ToString : anychar-bar-14 → string
anychar-bar-14ToString x = "(anychar-bar-14 " ^ x ^ ")"
anychar-bar-15ToString : anychar-bar-15 → string
anychar-bar-15ToString x = "(anychar-bar-15 " ^ x ^ ")"
anychar-bar-16ToString : anychar-bar-16 → string
anychar-bar-16ToString x = "(anychar-bar-16 " ^ x ^ ")"
anychar-bar-17ToString : anychar-bar-17 → string
anychar-bar-17ToString x = "(anychar-bar-17 " ^ x ^ ")"
anychar-bar-18ToString : anychar-bar-18 → string
anychar-bar-18ToString x = "(anychar-bar-18 " ^ x ^ ")"
anychar-bar-19ToString : anychar-bar-19 → string
anychar-bar-19ToString x = "(anychar-bar-19 " ^ x ^ ")"
anychar-bar-20ToString : anychar-bar-20 → string
anychar-bar-20ToString x = "(anychar-bar-20 " ^ x ^ ")"
anychar-bar-21ToString : anychar-bar-21 → string
anychar-bar-21ToString x = "(anychar-bar-21 " ^ x ^ ")"
anychar-bar-22ToString : anychar-bar-22 → string
anychar-bar-22ToString x = "(anychar-bar-22 " ^ x ^ ")"
anychar-bar-23ToString : anychar-bar-23 → string
anychar-bar-23ToString x = "(anychar-bar-23 " ^ x ^ ")"
anychar-bar-24ToString : anychar-bar-24 → string
anychar-bar-24ToString x = "(anychar-bar-24 " ^ x ^ ")"
anychar-bar-25ToString : anychar-bar-25 → string
anychar-bar-25ToString x = "(anychar-bar-25 " ^ x ^ ")"
anychar-bar-26ToString : anychar-bar-26 → string
anychar-bar-26ToString x = "(anychar-bar-26 " ^ x ^ ")"
anychar-bar-27ToString : anychar-bar-27 → string
anychar-bar-27ToString x = "(anychar-bar-27 " ^ x ^ ")"
anychar-bar-28ToString : anychar-bar-28 → string
anychar-bar-28ToString x = "(anychar-bar-28 " ^ x ^ ")"
anychar-bar-29ToString : anychar-bar-29 → string
anychar-bar-29ToString x = "(anychar-bar-29 " ^ x ^ ")"
anychar-bar-9ToString : anychar-bar-9 → string
anychar-bar-9ToString x = "(anychar-bar-9 " ^ x ^ ")"
numToString : num → string
numToString x = "(num " ^ x ^ ")"
num-plus-6ToString : num-plus-6 → string
num-plus-6ToString x = "(num-plus-6 " ^ x ^ ")"
numoneToString : numone → string
numoneToString x = "(numone " ^ x ^ ")"
numone-range-5ToString : numone-range-5 → string
numone-range-5ToString x = "(numone-range-5 " ^ x ^ ")"
numpunctToString : numpunct → string
numpunctToString x = "(numpunct " ^ x ^ ")"
numpunct-bar-7ToString : numpunct-bar-7 → string
numpunct-bar-7ToString x = "(numpunct-bar-7 " ^ x ^ ")"
numpunct-bar-8ToString : numpunct-bar-8 → string
numpunct-bar-8ToString x = "(numpunct-bar-8 " ^ x ^ ")"
pathToString : path → string
pathToString x = "(path " ^ x ^ ")"
path-star-1ToString : path-star-1 → string
path-star-1ToString x = "(path-star-1 " ^ x ^ ")"

mutual
  boolToString : 𝔹 → string
  boolToString tt = "true"
  boolToString ff = "false"

  optToString : opt → string
  optToString (GenerateLogs x0) = "(GenerateLogs" ^ " " ^ (boolToString x0) ^ ")"
  optToString (Lib x0) = "(Lib" ^ " " ^ (pathsToString x0) ^ ")"
  optToString (MakeRktFiles x0) = "(MakeRktFiles" ^ " " ^ (boolToString x0) ^ ")"
  optToString (ShowQualifiedVars x0) = "(ShowQualifiedVars" ^ " " ^ (boolToString x0) ^ ")"
  optToString (UseCedeFiles x0) = "(UseCedeFiles" ^ " " ^ (boolToString x0) ^ ")"
  optToString (EraseTypes x0) = "(EraseTypes" ^ " " ^ (boolToString x0) ^ ")"
  optToString (PrettyPrintColumns x0) = "PrettyPrintColumns" ^ " " ^ x0 ^ ")"
  optToString (DatatypeEncoding nothing) = "(DatatypeEncoding nothing)"
  optToString (DatatypeEncoding (just x0)) = "(DatatypeEncoding (just " ^ x0 ^ "))"

  optsToString : opts → string
  optsToString (OptsCons x0 x1) = "(OptsCons" ^ " " ^ (optToString x0) ^ " " ^ (optsToString x1) ^ ")"
  optsToString (OptsNil) = "OptsNil" ^ ""

  pathsToString : paths → string
  pathsToString (PathsCons x0 x1) = "(PathsCons" ^ " " ^ (pathToString x0) ^ " " ^ (pathsToString x1) ^ ")"
  pathsToString (PathsNil) = "PathsNil" ^ ""

--  data-encodingToString : data-encoding → string
--  data-encodingToString Mendler = "Mendler"
--  data-encodingToString Mendler-old = "Mendler-old"

  startToString : start → string
  startToString (File x0) = "(File" ^ " " ^ (optsToString x0) ^ ")"

ParseTreeToString : ParseTreeT → string
ParseTreeToString (parsed-opt t) = optToString t
ParseTreeToString (parsed-opts t) = optsToString t
ParseTreeToString (parsed-paths t) = pathsToString t
ParseTreeToString (parsed-start t) = startToString t
ParseTreeToString (parsed-bool t) = boolToString t
ParseTreeToString (parsed-posinfo t) = posinfoToString t
ParseTreeToString (parsed-alpha t) = alphaToString t
ParseTreeToString (parsed-alpha-bar-4 t) = alpha-bar-4ToString t
ParseTreeToString (parsed-alpha-range-2 t) = alpha-range-2ToString t
ParseTreeToString (parsed-alpha-range-3 t) = alpha-range-3ToString t
ParseTreeToString (parsed-anychar t) = anycharToString t
ParseTreeToString (parsed-anychar-bar-10 t) = anychar-bar-10ToString t
ParseTreeToString (parsed-anychar-bar-11 t) = anychar-bar-11ToString t
ParseTreeToString (parsed-anychar-bar-12 t) = anychar-bar-12ToString t
ParseTreeToString (parsed-anychar-bar-13 t) = anychar-bar-13ToString t
ParseTreeToString (parsed-anychar-bar-14 t) = anychar-bar-14ToString t
ParseTreeToString (parsed-anychar-bar-15 t) = anychar-bar-15ToString t
ParseTreeToString (parsed-anychar-bar-16 t) = anychar-bar-16ToString t
ParseTreeToString (parsed-anychar-bar-17 t) = anychar-bar-17ToString t
ParseTreeToString (parsed-anychar-bar-18 t) = anychar-bar-18ToString t
ParseTreeToString (parsed-anychar-bar-19 t) = anychar-bar-19ToString t
ParseTreeToString (parsed-anychar-bar-20 t) = anychar-bar-20ToString t
ParseTreeToString (parsed-anychar-bar-21 t) = anychar-bar-21ToString t
ParseTreeToString (parsed-anychar-bar-22 t) = anychar-bar-22ToString t
ParseTreeToString (parsed-anychar-bar-23 t) = anychar-bar-23ToString t
ParseTreeToString (parsed-anychar-bar-24 t) = anychar-bar-24ToString t
ParseTreeToString (parsed-anychar-bar-25 t) = anychar-bar-25ToString t
ParseTreeToString (parsed-anychar-bar-26 t) = anychar-bar-26ToString t
ParseTreeToString (parsed-anychar-bar-27 t) = anychar-bar-27ToString t
ParseTreeToString (parsed-anychar-bar-28 t) = anychar-bar-28ToString t
ParseTreeToString (parsed-anychar-bar-29 t) = anychar-bar-29ToString t
ParseTreeToString (parsed-anychar-bar-9 t) = anychar-bar-9ToString t
ParseTreeToString (parsed-num t) = numToString t
ParseTreeToString (parsed-num-plus-6 t) = num-plus-6ToString t
ParseTreeToString (parsed-numone t) = numoneToString t
ParseTreeToString (parsed-numone-range-5 t) = numone-range-5ToString t
ParseTreeToString (parsed-numpunct t) = numpunctToString t
ParseTreeToString (parsed-numpunct-bar-7 t) = numpunct-bar-7ToString t
ParseTreeToString (parsed-numpunct-bar-8 t) = numpunct-bar-8ToString t
ParseTreeToString (parsed-path t) = pathToString t
ParseTreeToString (parsed-path-star-1 t) = path-star-1ToString t
ParseTreeToString parsed-aws = "[aws]"
ParseTreeToString parsed-aws-bar-31 = "[aws-bar-31]"
ParseTreeToString parsed-aws-bar-32 = "[aws-bar-32]"
ParseTreeToString parsed-aws-bar-33 = "[aws-bar-33]"
ParseTreeToString parsed-comment = "[comment]"
ParseTreeToString parsed-comment-star-30 = "[comment-star-30]"
ParseTreeToString parsed-ows = "[ows]"
ParseTreeToString parsed-ows-star-35 = "[ows-star-35]"
ParseTreeToString parsed-squote = "[squote]"
ParseTreeToString parsed-ws = "[ws]"
ParseTreeToString parsed-ws-plus-34 = "[ws-plus-34]"

------------------------------------------
-- Reorganizing rules
------------------------------------------

mutual

  {-# TERMINATING #-}
  norm-bool : (x : bool) → bool
  norm-bool x = x

  {-# TERMINATING #-}
  norm-start : (x : start) → start
  norm-start x = x

  {-# TERMINATING #-}
  norm-posinfo : (x : posinfo) → posinfo
  norm-posinfo x = x

  {-# TERMINATING #-}
  norm-paths : (x : paths) → paths
  norm-paths x = x

  {-# TERMINATING #-}
  norm-opts : (x : opts) → opts
  norm-opts x = x

  {-# TERMINATING #-}
  norm-opt : (x : opt) → opt
  norm-opt x = x

isParseTree : ParseTreeT → 𝕃 char → string → Set
isParseTree p l s = ⊤ {- this will be ignored since we are using simply typed runs -}

ptr : ParseTreeRec
ptr = record { ParseTreeT = ParseTreeT ; isParseTree = isParseTree ; ParseTreeToString = ParseTreeToString }


text:
module reductionSystems1 where

data ℕ : Set where
  Z : ℕ
  S : ℕ -> ℕ

_+_ : ℕ -> ℕ -> ℕ
n + Z   = n
n + S m = S (n + m)

_*_ : ℕ -> ℕ -> ℕ
n * Z = Z
n * S m = (n * m) + n

{-
{-# BUILTIN NATURAL  ℕ  #-}
{-# BUILTIN ZERO     Z #-}
{-# BUILTIN SUC      S  #-}
{-# BUILTIN NATPLUS  _+_  #-}
{-# BUILTIN NATTIMES _*_  #-}
-}

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
{-# OPTIONS --rewriting #-}
-- {-# OPTIONS --confluence-check #-}

-- Formulæ and hypotheses (contexts)

open import Library

module Formulas (Base : Set) where

-- Propositional formulas

data Form : Set where
  Atom : (P : Base) → Form
  True False : Form
  _∨_ _∧_ _⇒_ : (A B : Form) → Form

infixl 8 _∧_
infixl 7 _∨_
infixr 6 _⇒_
infixr 5 ¬_

¬_ : (A : Form) → Form
¬ A = A ⇒ False

-- Contexts

data Cxt : Set where
  ε : Cxt
  _∙_ : (Γ : Cxt) (A : Form) → Cxt

infixl 4 _∙_

-- Context extension (thinning)

infix 3 _≤_

data _≤_ : (Γ Δ : Cxt) → Set where
  ε    : ε ≤ ε
  weak : ∀{A Γ Δ} (τ : Γ ≤ Δ) → Γ ∙ A ≤ Δ
  lift : ∀{A Γ Δ} (τ : Γ ≤ Δ) → Γ ∙ A ≤ Δ ∙ A

id≤ : ∀{Γ} → Γ ≤ Γ
id≤ {ε}     = ε
id≤ {Γ ∙ A} = lift id≤

-- Category of thinnings

_•_ : ∀{Γ Δ Φ} (τ : Γ ≤ Δ) (σ : Δ ≤ Φ) → Γ ≤ Φ
ε      • σ = σ
weak τ • σ = weak (τ • σ)
lift τ • weak σ = weak (τ • σ)
lift τ • lift σ = lift (τ • σ)

•-id-l : ∀{Γ Δ} (τ : Γ ≤ Δ) → id≤ • τ  ≡ τ
•-id-l ε = refl
•-id-l (weak τ) = cong weak (•-id-l τ)
•-id-l (lift τ) = cong lift (•-id-l τ)

•-id-r : ∀{Γ Δ} (τ : Γ ≤ Δ) → τ • id≤ ≡ τ
•-id-r ε = refl
•-id-r (weak τ) = cong weak (•-id-r τ)
•-id-r (lift τ) = cong lift (•-id-r τ)

•-ε-r : ∀{Γ} (τ : Γ ≤ ε) → τ • ε ≡ τ
•-ε-r ε = refl
•-ε-r (weak τ) = cong weak (•-ε-r τ)

{-# REWRITE •-id-l •-id-r •-ε-r #-}

-- Pullbacks

record RawPullback {Γ Δ₁ Δ₂} (τ₁ : Δ₁ ≤ Γ) (τ₂ : Δ₂ ≤ Γ) : Set where
  constructor rawPullback; field
    {Γ'} : Cxt
    τ₁' : Γ' ≤ Δ₁
    τ₂' : Γ' ≤ Δ₂
    comm : τ₁' • τ₁ ≡ τ₂' • τ₂

-- The glb is only unique up to isomorphism:
-- for glb (weak τ₁) (weak τ₂) we have two choices how to proceed.

glb : ∀ {Γ Δ₁ Δ₂} (τ₁ : Δ₁ ≤ Γ) (τ₂ : Δ₂ ≤ Γ) → RawPullback τ₁ τ₂
glb ε τ₂ = rawPullback τ₂ id≤ refl  -- REWRITE (•-id-r τ₂)
glb τ₁ ε = rawPullback id≤ τ₁ refl  -- REWRITE (•-id-l τ₁)
glb (weak τ₁) τ₂ =
  let rawPullback τ₁' τ₂' comm = glb τ₁ τ₂
  in  rawPullback (lift τ₁') (weak τ₂') (cong weak comm)
glb τ₁ (weak τ₂) =
  let rawPullback τ₁' τ₂' comm = glb τ₁ τ₂
  in  rawPullback (weak τ₁') (lift τ₂') (cong weak comm)
glb (lift τ₁) (lift τ₂) =
  let rawPullback τ₁' τ₂' comm = glb τ₁ τ₂
  in  rawPullback (lift τ₁') (lift τ₂') (cong lift comm)

-- glb (weak τ₁) (weak τ₂) =
--   let rawPullback τ₁' τ₂' comm = glb τ₁ τ₂
--   in  rawPullback (weak (lift τ₁')) (lift (weak τ₂')) (cong (weak ∘ weak) comm)
--   -- Here is a choice: it would also work the other way round:
--   -- rawPullback (lift (weak τ₁')) (weak (lift τ₂')) (cong (weak ∘ weak) comm)
-- glb (weak τ₁) (lift τ₂) =
--   let rawPullback τ₁' τ₂' comm = glb τ₁ (lift τ₂)
--   in  rawPullback (lift τ₁') (weak τ₂') (cong weak comm)

record WeakPullback {Γ Δ₁ Δ₂} (τ₁ : Δ₁ ≤ Γ) (τ₂ : Δ₂ ≤ Γ) : Set where
  constructor weakPullback
  field
    rawpullback : RawPullback τ₁ τ₂
  open RawPullback rawpullback public
  -- field
    -- largest : ∀ (pb : RawPullback τ₁ τ₂)

-- There are actually no pullbacks in the OPE category

-- Hypotheses

data Hyp (A : Form) : (Γ : Cxt) → Set where
  top : ∀{Γ} → Hyp A (Γ ∙ A)
  pop : ∀{Γ B} (x : Hyp A Γ) → Hyp A (Γ ∙ B)

Mon : (P : Cxt → Set) → Set
Mon P = ∀{Γ Δ} (τ : Γ ≤ Δ) → P Δ → P Γ

monH : ∀{A} → Mon (Hyp A)
monH ε      ()
monH (weak τ) x       = pop (monH τ x)
monH (lift τ) top     = top
monH (lift τ) (pop x) = pop (monH τ x)

monH-id : ∀{Γ A} (x : Hyp A Γ) → monH id≤ x ≡ x
monH-id top     = refl
monH-id (pop x) = cong pop (monH-id x)

monH• : ∀{Γ Δ Φ A} (τ : Γ ≤ Δ) (σ : Δ ≤ Φ) (x : Hyp A Φ) → monH (τ • σ) x ≡ monH τ (monH σ x)
monH• ε ε ()
monH• (weak τ) σ        x       = cong pop (monH• τ σ x)
monH• (lift τ) (weak σ) x       = cong pop (monH• τ σ x)
monH• (lift τ) (lift σ) top     = refl
monH• (lift τ) (lift σ) (pop x) = cong pop (monH• τ σ x)

{-# REWRITE monH-id monH• #-}

□ : (P : Cxt → Set) → Cxt → Set
□ P Γ = ∀{Δ} (τ : Δ ≤ Γ) → P Δ

mon□ : ∀{P} → Mon (□ P)
mon□ τ x τ′ = x (τ′ • τ)

infix 1 _→̇_
infixr 2 _⇒̂_

-- Presheaf morphism

_→̇_ : (P Q : Cxt → Set) → Set
P →̇ Q = ∀{Γ} → P Γ → Q Γ

⟨_⊙_⟩→̇_ : (P Q R : Cxt → Set) → Set
⟨ P ⊙ Q ⟩→̇ R = ∀{Γ} → P Γ → Q Γ → R Γ

⟨_⊙_⊙_⟩→̇_ : (P Q R S : Cxt → Set) → Set
⟨ P ⊙ Q ⊙ R ⟩→̇ S = ∀{Γ} → P Γ → Q Γ → R Γ → S Γ

-- Pointwise presheaf arrow (not a presheaf)

CFun : (P Q : Cxt → Set) → Cxt → Set
CFun P Q Γ = P Γ → Q Γ

-- Presheaf exponentional (Kripke function space)

KFun : (P Q : Cxt → Set) → Cxt → Set
KFun P Q = □ (CFun P Q)

-- Again, in expanded form.

_⇒̂_  : (P Q : Cxt → Set) → Cxt → Set
P ⇒̂ Q = λ Γ → ∀{Δ} (τ : Δ ≤ Γ) → P Δ → Q Δ

-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text: module Categories.Monad.EilenbergMoore where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Issue87 where

data I : Set where

data D : I -> Set where
  d : forall {i} (x : D i) -> D i

bar : forall {i} -> D i -> D i -> D i
bar (d x) (d     y) with y
bar (d x) (d {i} y) | z = d {i} y

-- Panic: unbound variable i
-- when checking that the expression i has type I

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda