text:
{-# OPTIONS --warning=error --safe --without-K #-}

open import LogicalFormulae
open import Lists.Lists
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Semirings.Definition
open import Orders.Total.Definition

module Numbers.BinaryNaturals.Definition where

data Bit : Set where
  zero : Bit
  one : Bit

BinNat : Set
BinNat = List Bit

::Inj : {xs ys : BinNat} {i : Bit} → i :: xs ≡ i :: ys → xs ≡ ys
::Inj {i = zero} refl = refl
::Inj {i = one} refl = refl

nonEmptyNotEmpty : {a : _} {A : Set a} {l1 : List A} {i : A} → i :: l1 ≡ [] → False
nonEmptyNotEmpty {l1 = l1} {i} ()

-- TODO - maybe we should do the floating-point style of assuming there's a leading bit and not storing it.
-- That way, everything is already canonical.

canonical : BinNat → BinNat
canonical [] = []
canonical (zero :: n) with canonical n
canonical (zero :: n) | [] = []
canonical (zero :: n) | x :: bl = zero :: x :: bl
canonical (one :: n) = one :: canonical n

Canonicalised : Set
Canonicalised = Sg BinNat (λ i → canonical i ≡ i)

binNatToN : BinNat → ℕ
binNatToN [] = 0
binNatToN (zero :: b) = 2 *N binNatToN b
binNatToN (one :: b) = 1 +N (2 *N binNatToN b)

incr : BinNat → BinNat
incr [] = one :: []
incr (zero :: n) = one :: n
incr (one :: n) = zero :: (incr n)

incrNonzero : (x : BinNat) → canonical (incr x) ≡ [] → False

incrPreservesCanonical : (x : BinNat) → (canonical x ≡ x) → canonical (incr x) ≡ incr x
incrPreservesCanonical [] pr = refl
incrPreservesCanonical (zero :: xs) pr with canonical xs
incrPreservesCanonical (zero :: xs) pr | x :: t = applyEquality (one ::_) (::Inj pr)
incrPreservesCanonical (one :: xs) pr with inspect (canonical (incr xs))
incrPreservesCanonical (one :: xs) pr | [] with≡ x = exFalso (incrNonzero xs x)
incrPreservesCanonical (one :: xs) pr | (x₁ :: y) with≡ x rewrite x = applyEquality (zero ::_) (transitivity (equalityCommutative x) (incrPreservesCanonical xs (::Inj pr)))

incrPreservesCanonical' : (x : BinNat) → canonical (incr x) ≡ incr (canonical x)

incrC : Canonicalised → Canonicalised
incrC (a , b) = incr a , incrPreservesCanonical a b

NToBinNat : ℕ → BinNat
NToBinNat zero = []
NToBinNat (succ n) with NToBinNat n
NToBinNat (succ n) | t = incr t

NToBinNatC : ℕ → Canonicalised
NToBinNatC zero = [] , refl
NToBinNatC (succ n) = incrC (NToBinNatC n)

incrInj : {x y : BinNat} → incr x ≡ incr y → canonical x ≡ canonical y

incrNonzero' : (x : BinNat) → (incr x) ≡ [] → False
incrNonzero' (zero :: xs) ()
incrNonzero' (one :: xs) ()

canonicalRespectsIncr' : {x y : BinNat} → canonical (incr x) ≡ canonical (incr y) → canonical x ≡ canonical y

binNatToNSucc : (n : BinNat) → binNatToN (incr n) ≡ succ (binNatToN n)
NToBinNatSucc : (n : ℕ) → incr (NToBinNat n) ≡ NToBinNat (succ n)

binNatToNZero : (x : BinNat) → binNatToN x ≡ 0 → canonical x ≡ []
binNatToNZero' : (x : BinNat) → canonical x ≡ [] → binNatToN x ≡ 0

NToBinNatZero : (n : ℕ) → NToBinNat n ≡ [] → n ≡ 0
NToBinNatZero zero pr = refl
NToBinNatZero (succ n) pr with NToBinNat n
NToBinNatZero (succ n) pr | zero :: bl = exFalso (nonEmptyNotEmpty pr)
NToBinNatZero (succ n) pr | one :: bl = exFalso (nonEmptyNotEmpty pr)

canonicalAscends : {i : Bit} → (a : BinNat) → 0 <N binNatToN a → i :: canonical a ≡ canonical (i :: a)

canonicalAscends' : {i : Bit} → (a : BinNat) → (canonical a ≡ [] → False) → i :: canonical a ≡ canonical (i :: a)
canonicalAscends' {i} a pr = canonicalAscends {i} a (t a pr)
  where
    t : (a : BinNat) → (canonical a ≡ [] → False) → 0 <N binNatToN a
    t a pr with TotalOrder.totality ℕTotalOrder 0 (binNatToN a)
    t a pr | inl (inl x) = x
    t a pr | inr x = exFalso (pr (binNatToNZero a (equalityCommutative x)))

canonicalIdempotent : (a : BinNat) → canonical a ≡ canonical (canonical a)
canonicalIdempotent [] = refl
canonicalIdempotent (zero :: a) with inspect (canonical a)
canonicalIdempotent (zero :: a) | [] with≡ y rewrite y = refl
canonicalIdempotent (zero :: a) | (x :: bl) with≡ y = transitivity (equalityCommutative (canonicalAscends' {zero} a λ p → contr p y)) (transitivity (applyEquality (zero ::_) (canonicalIdempotent a)) (equalityCommutative v))
  where
    contr : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
    contr {l1 = []} p1 ()
    contr {l1 = x :: l1} () p2
    u : canonical (canonical (zero :: a)) ≡ canonical (zero :: canonical a)
    u = applyEquality canonical (equalityCommutative (canonicalAscends' {zero} a λ p → contr p y))
    v : canonical (canonical (zero :: a)) ≡ zero :: canonical (canonical a)
    v = transitivity u (equalityCommutative (canonicalAscends' {zero} (canonical a) λ p → contr (transitivity (canonicalIdempotent a) p) y))
canonicalIdempotent (one :: a) rewrite equalityCommutative (canonicalIdempotent a) = refl

canonicalAscends'' : {i : Bit} → (a : BinNat) → canonical (i :: canonical a) ≡ canonical (i :: a)

binNatToNInj : (x y : BinNat) → binNatToN x ≡ binNatToN y → canonical x ≡ canonical y

NToBinNatInj : (x y : ℕ) → canonical (NToBinNat x) ≡ canonical (NToBinNat y) → x ≡ y

NToBinNatIsCanonical : (x : ℕ) → NToBinNat x ≡ canonical (NToBinNat x)
NToBinNatIsCanonical zero = refl
NToBinNatIsCanonical (succ x) with NToBinNatC x
NToBinNatIsCanonical (succ x) | a , b = equalityCommutative (incrPreservesCanonical (NToBinNat x) (equalityCommutative (NToBinNatIsCanonical x)))

contr' : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
contr' {l1 = []} p1 ()
contr' {l1 = x :: l1} () p2

binNatToNIsCanonical : (x : BinNat) → binNatToN (canonical x) ≡ binNatToN x
binNatToNIsCanonical [] = refl
binNatToNIsCanonical (zero :: x) with inspect (canonical x)
binNatToNIsCanonical (zero :: x) | [] with≡ t rewrite t | binNatToNZero' x t = refl
binNatToNIsCanonical (zero :: x) | (x₁ :: bl) with≡ t rewrite (equalityCommutative (canonicalAscends' {zero} x λ p → contr' p t)) | binNatToNIsCanonical x = refl
binNatToNIsCanonical (one :: x) rewrite binNatToNIsCanonical x = refl

-- The following two theorems demonstrate that Canonicalised is isomorphic to ℕ

nToN : (x : ℕ) → binNatToN (NToBinNat x) ≡ x

binToBin : (x : BinNat) → NToBinNat (binNatToN x) ≡ canonical x
binToBin x = transitivity (NToBinNatIsCanonical (binNatToN x)) (binNatToNInj (NToBinNat (binNatToN x)) x (nToN (binNatToN x)))

doubleIsBitShift' : (a : ℕ) → NToBinNat (2 *N succ a) ≡ zero :: NToBinNat (succ a)
doubleIsBitShift' zero = refl
doubleIsBitShift' (succ a) with doubleIsBitShift' a
... | bl rewrite Semiring.commutative ℕSemiring a (succ (succ (a +N 0))) | Semiring.commutative ℕSemiring (succ (a +N 0)) a | Semiring.commutative ℕSemiring a (succ (a +N 0)) | Semiring.commutative ℕSemiring (a +N 0) a | bl = refl

doubleIsBitShift : (a : ℕ) → (0 <N a) → NToBinNat (2 *N a) ≡ zero :: NToBinNat a
doubleIsBitShift zero ()
doubleIsBitShift (succ a) _ = doubleIsBitShift' a

canonicalDescends : {a : Bit} (as : BinNat) → (prA : a :: as ≡ canonical (a :: as)) → as ≡ canonical as
canonicalDescends {zero} as pr with canonical as
canonicalDescends {zero} as pr | x :: bl = ::Inj pr
canonicalDescends {one} as pr = ::Inj pr

--- Proofs

parity : (a b : ℕ) → succ (2 *N a) ≡ 2 *N b → False
doubleInj : (a b : ℕ) → (2 *N a) ≡ (2 *N b) → a ≡ b

incrNonzeroTwice : (x : BinNat) → canonical (incr (incr x)) ≡ one :: [] → False
incrNonzeroTwice (zero :: xs) pr with canonical (incr xs)
incrNonzeroTwice (zero :: xs) () | []
incrNonzeroTwice (zero :: xs) () | x :: bl
incrNonzeroTwice (one :: xs) pr = exFalso (incrNonzero xs (::Inj pr))

canonicalRespectsIncr' {[]} {[]} pr = refl
canonicalRespectsIncr' {[]} {zero :: y} pr with canonical y
canonicalRespectsIncr' {[]} {zero :: y} pr | [] = refl
canonicalRespectsIncr' {[]} {one :: y} pr with canonical (incr y)
canonicalRespectsIncr' {[]} {one :: y} () | []
canonicalRespectsIncr' {[]} {one :: y} () | x :: bl
canonicalRespectsIncr' {zero :: xs} {y} pr with canonical xs
canonicalRespectsIncr' {zero :: xs} {[]} pr | [] = refl
canonicalRespectsIncr' {zero :: xs} {zero :: y} pr | [] with canonical y
canonicalRespectsIncr' {zero :: xs} {zero :: y} pr | [] | [] = refl
canonicalRespectsIncr' {zero :: xs} {one :: y} pr | [] with canonical (incr y)
canonicalRespectsIncr' {zero :: xs} {one :: y} () | [] | []
canonicalRespectsIncr' {zero :: xs} {one :: y} () | [] | x :: bl
canonicalRespectsIncr' {zero :: xs} {zero :: ys} pr | x :: bl with canonical ys
canonicalRespectsIncr' {zero :: xs} {zero :: ys} pr | x :: bl | x₁ :: th = applyEquality (zero ::_) (::Inj pr)
canonicalRespectsIncr' {zero :: xs} {one :: ys} pr | x :: bl with canonical (incr ys)
canonicalRespectsIncr' {zero :: xs} {one :: ys} () | x :: bl | []
canonicalRespectsIncr' {zero :: xs} {one :: ys} () | x :: bl | x₁ :: th
canonicalRespectsIncr' {one :: xs} {[]} pr with canonical (incr xs)
canonicalRespectsIncr' {one :: xs} {[]} () | []
canonicalRespectsIncr' {one :: xs} {[]} () | x :: bl
canonicalRespectsIncr' {one :: xs} {zero :: ys} pr with canonical ys
canonicalRespectsIncr' {one :: xs} {zero :: ys} pr | [] with canonical (incr xs)
canonicalRespectsIncr' {one :: xs} {zero :: ys} () | [] | []
canonicalRespectsIncr' {one :: xs} {zero :: ys} () | [] | x :: t
canonicalRespectsIncr' {one :: xs} {zero :: ys} pr | x :: bl with canonical (incr xs)
canonicalRespectsIncr' {one :: xs} {zero :: ys} () | x :: bl | []
canonicalRespectsIncr' {one :: xs} {zero :: ys} () | x :: bl | x₁ :: t
canonicalRespectsIncr' {one :: xs} {one :: ys} pr with inspect (canonical (incr xs))
canonicalRespectsIncr' {one :: xs} {one :: ys} pr | [] with≡ x = exFalso (incrNonzero xs x)
canonicalRespectsIncr' {one :: xs} {one :: ys} pr | (x+1 :: x+1s) with≡ bad rewrite bad = applyEquality (one ::_) ans
  where
    ans : canonical xs ≡ canonical ys
    ans with inspect (canonical (incr ys))
    ans | [] with≡ x = exFalso (incrNonzero ys x)
    ans | (x₁ :: y) with≡ x rewrite x = canonicalRespectsIncr' {xs} {ys} (transitivity bad (transitivity (::Inj pr) (equalityCommutative x)))

binNatToNInj[] : (y : BinNat) → 0 ≡ binNatToN y → [] ≡ canonical y
binNatToNInj[] [] pr = refl
binNatToNInj[] (zero :: y) pr with productZeroImpliesOperandZero {2} {binNatToN y} (equalityCommutative pr)
binNatToNInj[] (zero :: y) pr | inr x with inspect (canonical y)
binNatToNInj[] (zero :: y) pr | inr x | [] with≡ canYPr rewrite canYPr = refl
binNatToNInj[] (zero :: ys) pr | inr x | (y :: canY) with≡ canYPr with binNatToNZero ys x
... | r with canonical ys
binNatToNInj[] (zero :: ys) pr | inr x | (y :: canY) with≡ canYPr | r | [] = refl
binNatToNInj[] (zero :: ys) pr | inr x | (y :: canY) with≡ canYPr | () | x₁ :: t

binNatToNInj [] y pr = binNatToNInj[] y pr
binNatToNInj (zero :: xs) [] pr = equalityCommutative (binNatToNInj[] (zero :: xs) (equalityCommutative pr))
binNatToNInj (zero :: xs) (zero :: ys) pr with doubleInj (binNatToN xs) (binNatToN ys) pr
... | x=y with binNatToNInj xs ys x=y
... | t with canonical xs
binNatToNInj (zero :: xs) (zero :: ys) pr | x=y | t | [] with canonical ys
binNatToNInj (zero :: xs) (zero :: ys) pr | x=y | t | [] | [] = refl
binNatToNInj (zero :: xs) (zero :: ys) pr | x=y | t | x :: cxs with canonical ys
binNatToNInj (zero :: xs) (zero :: ys) pr | x=y | t | x :: cxs | x₁ :: cys = applyEquality (zero ::_) t
binNatToNInj (zero :: xs) (one :: ys) pr = exFalso (parity (binNatToN ys) (binNatToN xs) (equalityCommutative pr))
binNatToNInj (one :: xs) (zero :: ys) pr = exFalso (parity (binNatToN xs) (binNatToN ys) pr)
binNatToNInj (one :: xs) (one :: ys) pr = applyEquality (one ::_) (binNatToNInj xs ys (doubleInj (binNatToN xs) (binNatToN ys) (succInjective pr)))

NToBinNatInj zero zero pr = refl
NToBinNatInj zero (succ y) pr with NToBinNat y
NToBinNatInj zero (succ y) pr | bl = exFalso (incrNonzero bl (equalityCommutative pr))
NToBinNatInj (succ x) zero pr with NToBinNat x
... | bl = exFalso (incrNonzero bl pr)
NToBinNatInj (succ x) (succ y) pr with inspect (NToBinNat x)
NToBinNatInj (succ zero) (succ zero) pr | [] with≡ nToBinXPr = refl
NToBinNatInj (succ zero) (succ (succ y)) pr | [] with≡ nToBinXPr with NToBinNat y
NToBinNatInj (succ zero) (succ (succ y)) pr | [] with≡ nToBinXPr | y' = exFalso (incrNonzeroTwice y' (equalityCommutative pr))
NToBinNatInj (succ (succ x)) (succ y) pr | [] with≡ nToBinXPr with NToBinNat x
NToBinNatInj (succ (succ x)) (succ y) pr | [] with≡ nToBinXPr | t = exFalso (incrNonzero' t nToBinXPr)
NToBinNatInj (succ x) (succ y) pr | (x₁ :: nToBinX) with≡ nToBinXPr with NToBinNatInj x y (canonicalRespectsIncr' {NToBinNat x} {NToBinNat y} pr)
NToBinNatInj (succ x) (succ .x) pr | (x₁ :: nToBinX) with≡ nToBinXPr | refl = refl

incrInj {[]} {[]} pr = refl
incrInj {[]} {zero :: ys} pr rewrite equalityCommutative (::Inj pr) = refl
incrInj {zero :: xs} {[]} pr rewrite ::Inj pr = refl
incrInj {zero :: xs} {zero :: .xs} refl = refl
incrInj {one :: xs} {one :: ys} pr = applyEquality (one ::_) (incrInj {xs} {ys} (l (incr xs) (incr ys) pr))
  where
    l : (a : BinNat) → (b : BinNat) → zero :: a ≡ zero :: b → a ≡ b
    l a .a refl = refl

doubleInj zero zero pr = refl
doubleInj (succ a) (succ b) pr = applyEquality succ (doubleInj a b u)
  where
    t : a +N a ≡ b +N b
    t rewrite Semiring.commutative ℕSemiring (succ a) 0 | Semiring.commutative ℕSemiring (succ b) 0 | Semiring.commutative ℕSemiring a (succ a) | Semiring.commutative ℕSemiring b (succ b) = succInjective (succInjective pr)
    u : a +N (a +N zero) ≡ b +N (b +N zero)
    u rewrite Semiring.commutative ℕSemiring a 0 | Semiring.commutative ℕSemiring b 0 = t

binNatToNZero [] pr = refl
binNatToNZero (zero :: xs) pr with inspect (canonical xs)
binNatToNZero (zero :: xs) pr | [] with≡ x rewrite x = refl
binNatToNZero (zero :: xs) pr | (x₁ :: y) with≡ x with productZeroImpliesOperandZero {2} {binNatToN xs} pr
binNatToNZero (zero :: xs) pr | (x₁ :: y) with≡ x | inr pr' with binNatToNZero xs pr'
... | bl with canonical xs
binNatToNZero (zero :: xs) pr | (x₁ :: y) with≡ x | inr pr' | bl | [] = refl
binNatToNZero (zero :: xs) pr | (x₁ :: y) with≡ x | inr pr' | () | x₂ :: t

binNatToNSucc [] = refl
binNatToNSucc (zero :: n) = refl
binNatToNSucc (one :: n) rewrite Semiring.commutative ℕSemiring (binNatToN n) zero | Semiring.commutative ℕSemiring (binNatToN (incr n)) 0 | binNatToNSucc n = applyEquality succ (Semiring.commutative ℕSemiring (binNatToN n) (succ (binNatToN n)))

incrNonzero (one :: xs) pr with inspect (canonical (incr xs))
incrNonzero (one :: xs) pr | [] with≡ x = incrNonzero xs x
incrNonzero (one :: xs) pr | (y :: ys) with≡ x with canonical (incr xs)
incrNonzero (one :: xs) pr | (y :: ys) with≡ () | []
incrNonzero (one :: xs) () | (.x₁ :: .th) with≡ refl | x₁ :: th

nToN zero = refl
nToN (succ x) with inspect (NToBinNat x)
nToN (succ x) | [] with≡ pr = ans
  where
    t : x ≡ zero
    t = NToBinNatInj x 0 (applyEquality canonical pr)
    ans : binNatToN (incr (NToBinNat x)) ≡ succ x
    ans rewrite t | pr = refl
nToN (succ x) | (bit :: xs) with≡ pr = transitivity (binNatToNSucc (NToBinNat x)) (applyEquality succ (nToN x))

parity zero (succ b) pr rewrite Semiring.commutative ℕSemiring b (succ (b +N 0)) = bad pr
  where
    bad : (1 ≡ succ (succ ((b +N 0) +N b))) → False
    bad ()
parity (succ a) (succ b) pr rewrite Semiring.commutative ℕSemiring b (succ (b +N 0)) | Semiring.commutative ℕSemiring a (succ (a +N 0)) | Semiring.commutative ℕSemiring (a +N 0) a | Semiring.commutative ℕSemiring (b +N 0) b = parity a b (succInjective (succInjective pr))

binNatToNZero' [] pr = refl
binNatToNZero' (zero :: xs) pr with inspect (canonical xs)
binNatToNZero' (zero :: xs) pr | [] with≡ p2 = ans
  where
    t : binNatToN xs ≡ 0
    t = binNatToNZero' xs p2
    ans : 2 *N binNatToN xs ≡ 0
    ans rewrite t = refl
binNatToNZero' (zero :: xs) pr | (y :: ys) with≡ p rewrite p = exFalso (bad pr)
  where
    bad : zero :: y :: ys ≡ [] → False
    bad ()
binNatToNZero' (one :: xs) ()

canonicalAscends {zero} a 0<a with inspect (canonical a)
canonicalAscends {zero} (zero :: a) 0<a | [] with≡ x = exFalso (contr'' (binNatToN a) t v)
  where
    u : binNatToN (zero :: a) ≡ 0
    u = binNatToNZero' (zero :: a) x
    v : binNatToN a ≡ 0
    v with inspect (binNatToN a)
    v | zero with≡ x = x
    v | succ a' with≡ x with inspect (binNatToN (zero :: a))
    v | succ a' with≡ x | zero with≡ pr2 rewrite pr2 = exFalso (TotalOrder.irreflexive ℕTotalOrder 0<a)
    v | succ a' with≡ x | succ y with≡ pr2 rewrite u = exFalso (TotalOrder.irreflexive ℕTotalOrder 0<a)
    t : 0 <N binNatToN a
    t with binNatToN a
    t | succ bl rewrite Semiring.commutative ℕSemiring (succ bl) 0 = succIsPositive bl
    contr'' : (x : ℕ) → (0 <N x) → (x ≡ 0) → False
    contr'' x 0<x x=0 rewrite x=0 = TotalOrder.irreflexive ℕTotalOrder 0<x
canonicalAscends {zero} a 0<a | (x₁ :: y) with≡ x rewrite x = refl
canonicalAscends {one} a 0<a = refl

canonicalAscends'' {i} a with inspect (canonical a)
canonicalAscends'' {zero} a | [] with≡ x rewrite x = refl
canonicalAscends'' {one} a | [] with≡ x rewrite x = refl
canonicalAscends'' {i} a | (x₁ :: y) with≡ x = transitivity (applyEquality canonical (canonicalAscends' {i} a λ p → contr p x)) (equalityCommutative (canonicalIdempotent (i :: a)))
  where
    contr : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
    contr {l1 = []} p1 ()
    contr {l1 = x :: l1} () p2

incrPreservesCanonical' [] = refl
incrPreservesCanonical' (zero :: xs) with inspect (canonical xs)
incrPreservesCanonical' (zero :: xs) | [] with≡ x rewrite x = refl
incrPreservesCanonical' (zero :: xs) | (x₁ :: y) with≡ x rewrite x = refl
incrPreservesCanonical' (one :: xs) with inspect (canonical (incr xs))
... | [] with≡ pr = exFalso (incrNonzero xs pr)
... | (_ :: _) with≡ pr rewrite pr = applyEquality (zero ::_) (transitivity (equalityCommutative pr) (incrPreservesCanonical' xs))

NToBinNatSucc zero = refl
NToBinNatSucc (succ n) with NToBinNat n
... | [] = refl
... | a :: as = refl


text:
module Id where

{-
postulate x : Set
postulate y : Set
postulate _p_ : Set -> Set -> Set

e : Set
e = x p y
-}

{-
id2 : (A : Set0) -> (_ : A) -> A
id2 = \ (C : Set) (z : C) -> z
-}

{-
id : (A : Set) -> A -> A
id = \ A x -> x
-}

{-
idImp : {A : Set} -> A -> A
idImp = \ {A} x -> x
-}

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

idd = id id

ext: agda

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
module deriveUtil where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat
open import Data.Fin
open import Data.List

open import regex
open import automaton
open import nfa
open import logic
open NAutomaton
open Automaton
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary

open Bool

data alpha2 : Set where
   a : alpha2
   b : alpha2

a-eq? : (x y : alpha2) → Dec (x ≡ y)
a-eq? a a = yes refl
a-eq? b b = yes refl
a-eq? a b = no (λ ())
a-eq? b a = no (λ ())

open Regex

open import finiteSet

fin-a : FiniteSet alpha2
fin-a  = record {
     finite = finite0
   ; Q←F = Q←F0
   ; F←Q = F←Q0
   ; finiso→ = finiso→0
   ; finiso← = finiso←0
 } where
     finite0 : ℕ
     finite0 = 2
     Q←F0 : Fin finite0 → alpha2
     Q←F0 zero = a
     Q←F0 (suc zero) = b
     F←Q0 : alpha2 → Fin finite0
     F←Q0 a = # 0
     F←Q0 b = # 1
     finiso→0 : (q : alpha2) → Q←F0 ( F←Q0 q ) ≡ q
     finiso→0 a = refl
     finiso→0 b = refl
     finiso←0 : (f : Fin finite0 ) → F←Q0 ( Q←F0 f ) ≡ f
     finiso←0 zero = refl
     finiso←0 (suc zero) = refl

open import derive alpha2 fin-a a-eq?
test11 = regex→automaton ( < a > & < b > )

test12 = accept test11 record { state =  < a > & < b > ; is-derived = unit } ( a ∷ b ∷ [] )
test13 = accept test11 record { state =  < a > & < b > ; is-derived = unit } ( a ∷ a ∷ [] )

test14 = regex-match ( (  < a > & < b > ) * ) ( a ∷ b ∷ a ∷ a ∷ [] )

test15 = regex-derive ( (  < a > & < b > ) * ∷ [] )
test16 = regex-derive test15
test17 : regex-derive test16 ≡ test16
test17 = refl

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


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

module higher.interval where

open import Relation.Binary.PropositionalEquality

open import equality-groupoid

postulate
  I : Set

  zero : I
  one : I
  path : zero ≡ one

module DepElim (B : I → Set)
               (x : B zero)
               (y : B one)
               (p : subst B path x ≡ y) where
  postulate
    elim : (t : I) → B t
    β-zero : elim zero ≡ x
    β-one : elim one ≡ y
    β-path : ap (subst B path) (sym β-zero)
           · lem-naturality elim path
           · β-one
           ≡ p

module Elim {X : Set}
            (x y : X)
            (p : x ≡ y) where
  open DepElim (λ _ → X) x y p

  postulate
    elim' : I → X
    β-zero' : elim zero ≡ x
    β-one' : elim one ≡ y
    β-path' : sym (β-zero') · ap elim path · β-one' ≡ p

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
-- Jesper, 2019-09-12: The fix of #3541 introduced a regression: the
-- index of the equality type is treated as a positive argument.

data _≡_ (A : Set) : Set → Set where
  refl : A ≡ A

postulate X : Set

data D : Set where
  c : X ≡ D → D

max_stars_repo_name: strake/agda

max_issues_repo_name: strake/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2017-07-26, issue #2331.
-- Andrea found a counterexample against the "usable decrease" feature:

open import Agda.Builtin.Size

data D (i : Size) : Set where
  c : (j : Size< i) → D i

mutual
  test : (i : Size) → D i → Set
  test  i (c j) = (k : Size< j) (l : Size< k) → helper i j k (c l)

  helper : (i : Size) (j : Size< i) (k : Size< j) → D k → Set
  helper i j k d = test k d

-- Should not termination check.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
module ConstructorHeadedDivergenceIn2-2-10 where

data ⊤ : Set where
  tt : ⊤

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

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

{- Brandon Moore reports (July 2011)
In 2.2.10 the following code seems to cause typechecking
to diverge.
-}

f : ℕ → Set
f zero = ⊤
f (suc n) = ℕ × f n

enum : (n : ℕ) → f n
enum zero = tt
enum (suc n) = n , enum n

n : ℕ
n = _

test : f n
test = enum (suc n)
{-
This typechecks quickly if the definition
of test is changed to

test = enum n

I think the problem is that the body has type ℕ × f n,
and unifying it with the expected type f n invokes the
constructor-headed function specialization to resolve
n to suc n', and the process repeats.

Brandon
-}

-- Andreas, 2011-07-28 This bug is not reproducible in the darcs
-- version.
--
-- This file should fail with unresolved metas.

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x
infix 0 _≡_

{-# BUILTIN EQUALITY _≡_ #-}

data Sigma {l} (A : Set l) (B : A -> Set l) : Set l where
  _**_ : (a : A) -> B a -> Sigma A B

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

trans : ∀ {a} {A : Set a} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl eq = eq

subst : ∀ {a b} {x y : Set a} → (P : Set a → Set b) → x ≡ y → P x ≡ P y
subst P refl = refl

cong : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl
fst : ∀ {l} -> {A : Set l}{B : A -> Set l} -> Sigma A B -> A
fst (x ** _) = x

snd : ∀ {l} -> {A : Set l}{B : A -> Set l} -> (sum : Sigma A B) -> B (fst sum)
snd (x ** y) = y

record Group {l} (G : Set l) (_op_ : G -> G -> G) : Set l where
  field
    assoc : {a b c : G} -> ((a op b) op c) ≡ (a op (b op c))
    id : {a : G} -> Sigma G (\e -> e op a ≡ a)
    inv : {a : G} -> Sigma G (\a^-1 -> (a^-1 op a) ≡ (fst (id {a})))
  e : {a : G} -> G
  e {a} = fst (id {a})

  _^-1 : G -> G
  x ^-1 = fst (inv {x})

  a^-1-op-a==e : {a : G} -> ((a ^-1) op a) ≡ e {a}
  a^-1-op-a==e {a} with inv {a}
  ...                   | (_ ** p) = p

  id-lem-right : {a : G} -> (e {a} op a) ≡ a
  id-lem-right {a} = snd (id {a})

  id-lem-left : {a : G} -> (a op e {a}) ≡ a
  id-lem-left {a} rewrite id-lem-right {a} = {!!}

-- In Agda 2.4.2.5 the error was:

-- Function does not accept argument {r = _}
-- when checking that {r = a} is a valid argument to a function of
-- type {a : G} → G

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module plfa.part1.Naturals where

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

seven = suc (suc (suc (suc (suc (suc (suc zero))))))

{-# BUILTIN NATURAL ℕ #-}

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

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

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩    -- is shorthand for
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩    -- inductive case
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩    -- inductive case
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩    -- base case
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩    -- is longhand for
    5
  ∎

_*_ : ℕ → ℕ → ℕ
zero    * n  =  zero
(suc m) * n  =  n + (m * n)

_̂_ : ℕ → ℕ → ℕ
n ̂ zero  = 1
n ̂ (suc m)  =  n * (n ̂ m)

_ : 3 ̂ 4 ≡ 81
_ =
  begin
    3 ̂ 4
  ≡⟨⟩
   81
  ∎

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

max_stars_repo_name: UnsoundWitch/proofs

max_issues_repo_name: sym-cereal/proofs

max_forks_repo_name: sym-cereal/proofs


text:
open import Categories
open import Monads

module Monads.Kleisli.Functors {a b}{C : Cat {a}{b}}(M : Monad C) where

open import Library
open import Functors
open import Monads.Kleisli M

open Cat C
open Fun
open Monad M

KlL : Fun C Kl
KlL = record{
  OMap  = id;
  HMap  = comp η;
  fid   = idr;
  fcomp = λ{_}{_}{_}{f}{g} →
    proof
    comp η (comp f g)
    ≅⟨ sym ass ⟩
    comp (comp η f) g
    ≅⟨ cong (λ f → comp f g) (sym law2) ⟩
    comp (comp (bind (comp η f)) η) g
    ≅⟨ ass ⟩
    comp (bind (comp η f)) (comp η g)
    ∎}

KlR : Fun Kl C
KlR = record{
  OMap  = T;
  HMap  = bind;
  fid   = law1;
  fcomp = law3}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
mutual
  Loop : Set
  Loop = {!!}

  -- Should not solve ?0 := Loop → Loop
  solve : Loop → Loop → Loop
  solve x = x


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

module Calf.Types.Unit where

open import Calf.Prelude
open import Calf.Metalanguage

open import Data.Unit public using (⊤) renaming (tt to triv)

unit : tp pos
unit = U (meta ⊤)

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


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

open import lib.Basics
open import lib.NType2
open import lib.types.Group
open import lib.types.List
open import lib.types.Pi
open import lib.types.SetQuotient
open import lib.types.Word
open import lib.groups.GeneratedGroup
open import lib.groups.Homomorphism

module lib.groups.GeneratedAbelianGroup {i} {m} where

module GeneratedAbelianGroup (A : Type i) (R : Rel (Word A) m) where

  data AbGroupRel : Word A → Word A → Type (lmax i m) where
    agr-commutes : ∀ l₁ l₂ → AbGroupRel (l₁ ++ l₂) (l₂ ++ l₁)
    agr-rel : ∀ {l₁ l₂} → R l₁ l₂ → AbGroupRel l₁ l₂

  private
    module Gen = GeneratedGroup A AbGroupRel
  open Gen hiding (module HomomorphismEquiv; rel-holds) public

  agr-reverse : (w : Word A) → QuotWordRel (reverse w) w
  agr-reverse nil = qwr-refl idp
  agr-reverse (x :: w) =
    reverse w ++ (x :: nil)
      qwr⟨ qwr-rel (agr-commutes (reverse w) (x :: nil)) ⟩
    x :: reverse w
      qwr⟨ qwr-cong-r (x :: nil) (agr-reverse w) ⟩
    x :: w qwr∎

  GenAbGroup : AbGroup (lmax i m)
  GenAbGroup = grp , grp-is-abelian
    where
    grp : Group (lmax i m)
    grp = GenGroup
    module grp = Group grp
    grp-is-abelian : is-abelian grp
    grp-is-abelian =
      QuotWord-elim {P = λ a → ∀ b → grp.comp a b == grp.comp b a}
        (λ la →
          QuotWord-elim {P = λ b → grp.comp qw[ la ] b == grp.comp b qw[ la ]}
            (λ lb → quot-rel (qwr-rel (agr-commutes la lb)))
            (λ _ → prop-has-all-paths-↓))
        (λ _ → prop-has-all-paths-↓ {{Π-level ⟨⟩}})

  rel-holds : ∀ {w₁} {w₂} (r : R w₁ w₂) → qw[ w₁ ] == qw[ w₂ ]
  rel-holds r = Gen.rel-holds (agr-rel r)

  module GenAbGroup = AbGroup GenAbGroup

  {- Universal Properties -}
  module HomomorphismEquiv {j} (G : AbGroup j) where

    private
      module G = AbGroup G
      module R-RFs = RelationRespectingFunctions A R G.grp
      module AbGroupRel-RFs = RelationRespectingFunctions A AbGroupRel G.grp

    open R-RFs public

    private
      legal-functions-equiv : R-RFs.RelationRespectingFunction
                            ≃ AbGroupRel-RFs.RelationRespectingFunction
      legal-functions-equiv =
        equiv to from
              (λ lf → AbGroupRel-RFs.RelationRespectingFunction= idp)
              (λ lf → R-RFs.RelationRespectingFunction= idp)
        where
        to : R-RFs.RelationRespectingFunction → AbGroupRel-RFs.RelationRespectingFunction
        to (R-RFs.rel-res-fun f respects-R) =
          AbGroupRel-RFs.rel-res-fun f respects-AbGroupRel
          where
          respects-AbGroupRel : AbGroupRel-RFs.respects-rel f
          respects-AbGroupRel (agr-commutes l₁ l₂) =
            Word-extendᴳ G.grp f (l₁ ++ l₂)
              =⟨ Word-extendᴳ-++ G.grp f l₁ l₂ ⟩
            G.comp (Word-extendᴳ G.grp f l₁) (Word-extendᴳ G.grp f l₂)
              =⟨ G.comm (Word-extendᴳ G.grp f l₁) (Word-extendᴳ G.grp f l₂) ⟩
            G.comp (Word-extendᴳ G.grp f l₂) (Word-extendᴳ G.grp f l₁)
              =⟨ ! (Word-extendᴳ-++ G.grp f l₂ l₁) ⟩
            Word-extendᴳ G.grp f (l₂ ++ l₁) =∎
          respects-AbGroupRel (agr-rel r) = respects-R r
        from : AbGroupRel-RFs.RelationRespectingFunction → R-RFs.RelationRespectingFunction
        from (AbGroupRel-RFs.rel-res-fun f respects-AbGroupRel) =
          R-RFs.rel-res-fun f respects-R
          where
          respects-R : R-RFs.respects-rel f
          respects-R r = respects-AbGroupRel (agr-rel r)

    extend-equiv : R-RFs.RelationRespectingFunction ≃ (GenAbGroup.grp →ᴳ G.grp)
    extend-equiv =
      Gen.HomomorphismEquiv.extend-equiv G.grp ∘e legal-functions-equiv

    extend : R-RFs.RelationRespectingFunction → (GenAbGroup.grp →ᴳ G.grp)
    extend = –> extend-equiv

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Modalities.Everything where

open import Cubical.Modalities.Modality public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax PCF

type
  N   : 0-ary
  _↣_ : 2-ary | r30
  B   : 0-ary

term
  app : α ↣ β  α  ->  β | _$_ l20
  lam : α.β  ->  α ↣ β | ƛ_ r10
  tr  : B
  fl  : B
  ze  : N
  su  : N  ->  N
  pr  : N  ->  N
  iz  : N  ->  B | 0?
  if  : B  α  α  ->  α
  fix : α.α  ->  α

theory
  (ƛβ) b : α.β  a : α |> app (lam(x.b[x]), a) = b[a]
  (ƛη) f : α ↣ β      |> lam (x. app(f, x))   = f
  (zz)       |> iz (ze)       = tr
  (zs) n : N |> iz (su (n)) = fl
  (ps) n : N |> pr (su (n)) = n
  (ift) t f : α |> if (tr, t, f) = t
  (iff) t f : α |> if (fl, t, f) = f
  (fix) t : α.α |> fix (x.t[x]) = t[fix (x.t[x])]
-}

module PCF.Signature where

open import SOAS.Context

-- Type declaration
data PCFT : Set where
  N   : PCFT
  _↣_ : PCFT → PCFT → PCFT
  B   : PCFT
infixr 30 _↣_

open import SOAS.Syntax.Signature PCFT public
open import SOAS.Syntax.Build PCFT public

-- Operator symbols
data PCFₒ : Set where
  appₒ lamₒ : {α β : PCFT} → PCFₒ
  trₒ flₒ zeₒ suₒ prₒ izₒ : PCFₒ
  ifₒ fixₒ : {α : PCFT} → PCFₒ

-- Term signature
PCF:Sig : Signature PCFₒ
PCF:Sig = sig λ
  { (appₒ {α}{β}) → (⊢₀ α ↣ β) , (⊢₀ α) ⟼₂ β
  ; (lamₒ {α}{β}) → (α ⊢₁ β) ⟼₁ α ↣ β
  ;  trₒ          → ⟼₀ B
  ;  flₒ          → ⟼₀ B
  ;  zeₒ          → ⟼₀ N
  ;  suₒ          → (⊢₀ N) ⟼₁ N
  ;  prₒ          → (⊢₀ N) ⟼₁ N
  ;  izₒ          → (⊢₀ N) ⟼₁ B
  ; (ifₒ  {α})    → (⊢₀ B) , (⊢₀ α) , (⊢₀ α) ⟼₃ α
  ; (fixₒ {α})    → (α ⊢₁ α) ⟼₁ α
  }

open Signature PCF:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module ShouldBeEmpty where

data Zero : Set where
data One : Set where
  one : One

ok : Zero -> One
ok ()

bad : One -> One
bad ()


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Concrete.System.Parameters

-- This module collects the implementation obligations for our (fake/simple, for now)
-- "implementation" into the structure required by Concrete.Properties.
open import LibraBFT.Impl.Handle.Properties
import      LibraBFT.Impl.Properties.VotesOnce   as VO
import      LibraBFT.Impl.Properties.PreferredRound as PR
open import LibraBFT.Concrete.Obligations
open import LibraBFT.Concrete.System

module LibraBFT.Impl.Properties where
  theImplObligations : ImplObligations
  theImplObligations = record { sps-cor = impl-sps-avp
                              ; vo₁     = VO.vo₁
                              ; vo₂     = VO.vo₂
                              ; pr₁     = PR.pr₁ }

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


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

open import GroupoidStructure
open import PathOperations
open import Types

tr-post : ∀ {a} {A : Set a} (a : A) {x y : A}
  (p : x ≡ y) (q : a ≡ x) →
  tr (λ x → a ≡ x) p q ≡ q · p
tr-post a = J
  (λ x _ p → (q : a ≡ x) → tr (λ x → a ≡ x) p q ≡ q · p)
  (λ _ q → p·id q ⁻¹)
  _ _

tr-pre : ∀ {a} {A : Set a} (a : A) {x y : A}
  (p : x ≡ y) (q : x ≡ a) →
  tr (λ x → x ≡ a) p q ≡ p ⁻¹ · q
tr-pre a = J
  (λ x _ p → (q : x ≡ a) → tr (λ x → x ≡ a) p q ≡ p ⁻¹ · q)
  (λ _ q → id·p q ⁻¹)
  _ _

tr-both : ∀ {a} {A : Set a} (a : A) {x y : A}
  (p : x ≡ y) (q : x ≡ x) →
  tr (λ x → x ≡ x) p q ≡ p ⁻¹ · q · p
tr-both a = J
  (λ x _ p → (q : x ≡ x) → tr (λ x → x ≡ x) p q ≡ p ⁻¹ · q · p)
  (λ _ q → p·id q ⁻¹ · id·p (q · refl) ⁻¹)
  _ _

tr-∘ : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
  (f : A → B) {x y : A} (p : x ≡ y) (u : P (f x)) →
  tr (P ∘ f) p u ≡ tr P (ap f p) u
tr-∘ {P = P} f = J
  (λ x _ p → (u : P (f x)) → tr (P ∘ f) p u ≡ tr P (ap f p) u)
  (λ _ _ → refl) _ _

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Homogeneously-indexed binary relations
------------------------------------------------------------------------

-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Homogeneous`.

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

open import Relation.Binary.Indexed.Homogeneous.Core

module Relation.Binary.Indexed.Homogeneous.Structures
  {i a ℓ} {I : Set i}
  (A : I → Set a)   -- The underlying indexed sets
  (_≈ᵢ_ : IRel A ℓ) -- The underlying indexed equality relation
  where

open import Data.Product using (_,_)
open import Function using (_⟨_⟩_)
open import Level using (Level; _⊔_; suc)
open import Relation.Binary as B using (_⇒_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Binary.Indexed.Homogeneous.Definitions

------------------------------------------------------------------------
-- Equivalences

-- Indexed structures are laid out in a similar manner as to those
-- in Relation.Binary. The main difference is each structure also
-- contains proofs for the lifted version of the relation.

record IsIndexedEquivalence : Set (i ⊔ a ⊔ ℓ) where
  field
    reflᵢ  : Reflexive  A _≈ᵢ_
    symᵢ   : Symmetric  A _≈ᵢ_
    transᵢ : Transitive A _≈ᵢ_

  reflexiveᵢ : ∀ {i} → _≡_ ⟨ _⇒_ ⟩ _≈ᵢ_ {i}
  reflexiveᵢ P.refl = reflᵢ

  -- Lift properties

  reflexive : _≡_ ⇒ (Lift A _≈ᵢ_)
  reflexive P.refl i = reflᵢ

  refl : B.Reflexive (Lift A _≈ᵢ_)
  refl i = reflᵢ

  sym : B.Symmetric (Lift A _≈ᵢ_)
  sym x≈y i = symᵢ (x≈y i)

  trans : B.Transitive (Lift A _≈ᵢ_)
  trans x≈y y≈z i = transᵢ (x≈y i) (y≈z i)

  isEquivalence : B.IsEquivalence (Lift A _≈ᵢ_)
  isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }

record IsIndexedDecEquivalence : Set (i ⊔ a ⊔ ℓ) where
  infix 4 _≟ᵢ_
  field
    _≟ᵢ_           : Decidable A _≈ᵢ_
    isEquivalenceᵢ : IsIndexedEquivalence

  open IsIndexedEquivalence isEquivalenceᵢ public

------------------------------------------------------------------------
-- Preorders

record IsIndexedPreorder {ℓ₂} (_∼ᵢ_ : IRel A ℓ₂)
                       : Set (i ⊔ a ⊔ ℓ ⊔ ℓ₂) where
  field
    isEquivalenceᵢ : IsIndexedEquivalence
    reflexiveᵢ     : _≈ᵢ_ ⇒[ A ] _∼ᵢ_
    transᵢ         : Transitive A _∼ᵢ_

  module Eq = IsIndexedEquivalence isEquivalenceᵢ

  reflᵢ : Reflexive A _∼ᵢ_
  reflᵢ = reflexiveᵢ Eq.reflᵢ

  ∼ᵢ-respˡ-≈ᵢ : Respectsˡ A _∼ᵢ_ _≈ᵢ_
  ∼ᵢ-respˡ-≈ᵢ x≈y x∼z = transᵢ (reflexiveᵢ (Eq.symᵢ x≈y)) x∼z

  ∼ᵢ-respʳ-≈ᵢ : Respectsʳ A _∼ᵢ_ _≈ᵢ_
  ∼ᵢ-respʳ-≈ᵢ x≈y z∼x = transᵢ z∼x (reflexiveᵢ x≈y)

  ∼ᵢ-resp-≈ᵢ : Respects₂ A _∼ᵢ_ _≈ᵢ_
  ∼ᵢ-resp-≈ᵢ = ∼ᵢ-respʳ-≈ᵢ , ∼ᵢ-respˡ-≈ᵢ

  -- Lifted properties

  reflexive : Lift A _≈ᵢ_ B.⇒ Lift A _∼ᵢ_
  reflexive x≈y i = reflexiveᵢ (x≈y i)

  refl : B.Reflexive (Lift A _∼ᵢ_)
  refl i = reflᵢ

  trans : B.Transitive (Lift A _∼ᵢ_)
  trans x≈y y≈z i = transᵢ (x≈y i) (y≈z i)

  ∼-respˡ-≈ : (Lift A _∼ᵢ_) B.Respectsˡ (Lift A _≈ᵢ_)
  ∼-respˡ-≈ x≈y x∼z i = ∼ᵢ-respˡ-≈ᵢ (x≈y i) (x∼z i)

  ∼-respʳ-≈ : (Lift A _∼ᵢ_) B.Respectsʳ (Lift A _≈ᵢ_)
  ∼-respʳ-≈ x≈y z∼x i = ∼ᵢ-respʳ-≈ᵢ (x≈y i) (z∼x i)

  ∼-resp-≈ : (Lift A _∼ᵢ_) B.Respects₂ (Lift A _≈ᵢ_)
  ∼-resp-≈ = ∼-respʳ-≈ , ∼-respˡ-≈

  isPreorder : B.IsPreorder (Lift A _≈ᵢ_) (Lift A _∼ᵢ_)
  isPreorder = record
    { isEquivalence = Eq.isEquivalence
    ; reflexive     = reflexive
    ; trans         = trans
    }

------------------------------------------------------------------------
-- Partial orders

record IsIndexedPartialOrder {ℓ₂} (_≤ᵢ_ : IRel A ℓ₂)
                           : Set (i ⊔ a ⊔ ℓ ⊔ ℓ₂) where
  field
    isPreorderᵢ : IsIndexedPreorder _≤ᵢ_
    antisymᵢ    : Antisymmetric A _≈ᵢ_ _≤ᵢ_

  open IsIndexedPreorder isPreorderᵢ public
    renaming
    ( ∼ᵢ-respˡ-≈ᵢ to ≤ᵢ-respˡ-≈ᵢ
    ; ∼ᵢ-respʳ-≈ᵢ to ≤ᵢ-respʳ-≈ᵢ
    ; ∼ᵢ-resp-≈ᵢ  to ≤ᵢ-resp-≈ᵢ
    ; ∼-respˡ-≈   to ≤-respˡ-≈
    ; ∼-respʳ-≈   to ≤-respʳ-≈
    ; ∼-resp-≈    to ≤-resp-≈
    )

  antisym : B.Antisymmetric (Lift A _≈ᵢ_) (Lift A _≤ᵢ_)
  antisym x≤y y≤x i = antisymᵢ (x≤y i) (y≤x i)

  isPartialOrder : B.IsPartialOrder (Lift A _≈ᵢ_) (Lift A _≤ᵢ_)
  isPartialOrder = record
    { isPreorder = isPreorder
    ; antisym    = antisym
    }


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

open import lib.Basics
open import lib.NConnected
open import lib.types.Empty
open import lib.types.Nat
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.types.TLevel
open import lib.types.Truncation

module lib.types.LoopSpace where

{- loop space -}

module _ {i} where

  ⊙Ω : Ptd i → Ptd i
  ⊙Ω ⊙[ A , a ] = ⊙[ (a == a) , idp ]

  Ω : Ptd i → Type i
  Ω = de⊙ ∘ ⊙Ω

module _ {i} {X : Ptd i} where

  Ω-! : Ω X → Ω X
  Ω-! = !

  Ω-∙ : Ω X → Ω X → Ω X
  Ω-∙ = _∙_

{- pointed versions of functions on paths -}

⊙Ω-∙ : ∀ {i} {X : Ptd i} → ⊙Ω X ⊙× ⊙Ω X ⊙→ ⊙Ω X
⊙Ω-∙ = (uncurry Ω-∙ , idp)

⊙Ω-fmap : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → X ⊙→ Y → ⊙Ω X ⊙→ ⊙Ω Y
⊙Ω-fmap (f , idp) = ap f , idp

Ω-fmap : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → X ⊙→ Y → (Ω X → Ω Y)
Ω-fmap F = fst (⊙Ω-fmap F)

Ω-fmap-β : ∀ {i j} {X : Ptd i} {Y : Ptd j} (F : X ⊙→ Y) (p : Ω X)
  → Ω-fmap F p == ! (snd F) ∙ ap (fst F) p ∙' snd F
Ω-fmap-β (_ , idp) _ = idp

Ω-isemap : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  (F : X ⊙→ Y) → is-equiv (fst F) → is-equiv (Ω-fmap F)
Ω-isemap (f , idp) e = ap-is-equiv e _ _

Ω-emap : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → (X ⊙≃ Y) → (Ω X ≃ Ω Y)
Ω-emap (F , F-is-equiv) = Ω-fmap F , Ω-isemap F F-is-equiv

⊙Ω-emap : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → (X ⊙≃ Y) → (⊙Ω X ⊙≃ ⊙Ω Y)
⊙Ω-emap (F , F-is-equiv) = ⊙Ω-fmap F , Ω-isemap F F-is-equiv

⊙Ω-fmap2 : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → X ⊙× Y ⊙→ Z → ⊙Ω X ⊙× ⊙Ω Y ⊙→ ⊙Ω Z
⊙Ω-fmap2 (f , idp) = (λ{(p , q) → ap2 (curry f) p q}) , idp

⊙Ω-fmap-∘ : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : Y ⊙→ Z) (f : X ⊙→ Y)
  → ⊙Ω-fmap (g ⊙∘ f) == ⊙Ω-fmap g ⊙∘ ⊙Ω-fmap f
⊙Ω-fmap-∘ (g , idp) (f , idp) = ⊙λ=' (λ p → ap-∘ g f p) idp

⊙Ω-csmap : ∀ {i₀ i₁ j₀ j₁} {X₀ : Ptd i₀} {X₁ : Ptd i₁}
  {Y₀ : Ptd j₀} {Y₁ : Ptd j₁} {f : X₀ ⊙→ Y₀} {g : X₁ ⊙→ Y₁}
  {hX : X₀ ⊙→ X₁} {hY : Y₀ ⊙→ Y₁}
  → ⊙CommSquare f g hX hY
  → ⊙CommSquare (⊙Ω-fmap f) (⊙Ω-fmap g) (⊙Ω-fmap hX) (⊙Ω-fmap hY)
⊙Ω-csmap {f = f} {g} {hX} {hY} (⊙comm-sqr cs) = ⊙comm-sqr $ ⊙app= $
  ⊙Ω-fmap hY ⊙∘ ⊙Ω-fmap f
    =⟨ ! $ ⊙Ω-fmap-∘ hY f ⟩
  ⊙Ω-fmap (hY ⊙∘ f)
    =⟨ ap ⊙Ω-fmap $ ⊙λ= cs ⟩
  ⊙Ω-fmap (g ⊙∘ hX)
    =⟨ ⊙Ω-fmap-∘ g hX ⟩
  ⊙Ω-fmap g ⊙∘ ⊙Ω-fmap hX
    =∎

⊙Ω-csemap : ∀ {i₀ i₁ j₀ j₁} {X₀ : Ptd i₀} {X₁ : Ptd i₁}
  {Y₀ : Ptd j₀} {Y₁ : Ptd j₁} {f : X₀ ⊙→ Y₀} {g : X₁ ⊙→ Y₁}
  {hX : X₀ ⊙→ X₁} {hY : Y₀ ⊙→ Y₁}
  → ⊙CommSquareEquiv f g hX hY
  → ⊙CommSquareEquiv (⊙Ω-fmap f) (⊙Ω-fmap g) (⊙Ω-fmap hX) (⊙Ω-fmap hY)
⊙Ω-csemap {f = f} {g} {hX} {hY} (⊙comm-sqr cs , hX-ise , hY-ise) =
  (⊙comm-sqr $ ⊙app= $
    ⊙Ω-fmap hY ⊙∘ ⊙Ω-fmap f
      =⟨ ! $ ⊙Ω-fmap-∘ hY f ⟩
    ⊙Ω-fmap (hY ⊙∘ f)
      =⟨ ap ⊙Ω-fmap $ ⊙λ= cs ⟩
    ⊙Ω-fmap (g ⊙∘ hX)
      =⟨ ⊙Ω-fmap-∘ g hX ⟩
    ⊙Ω-fmap g ⊙∘ ⊙Ω-fmap hX
      =∎) ,
  Ω-isemap hX hX-ise , Ω-isemap hY hY-ise

⊙Ω-fmap-idf : ∀ {i} {X : Ptd i} → ⊙Ω-fmap (⊙idf X) == ⊙idf _
⊙Ω-fmap-idf = ⊙λ=' ap-idf idp

⊙Ω-fmap2-fst : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → ⊙Ω-fmap2 {X = X} {Y = Y} ⊙fst == ⊙fst
⊙Ω-fmap2-fst = ⊙λ=' (uncurry ap2-fst) idp

⊙Ω-fmap2-snd : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → ⊙Ω-fmap2 {X = X} {Y = Y} ⊙snd == ⊙snd
⊙Ω-fmap2-snd = ⊙λ=' (uncurry ap2-snd) idp

⊙Ω-fmap-fmap2 : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (G : Z ⊙→ W) (F : X ⊙× Y ⊙→ Z)
  → ⊙Ω-fmap G ⊙∘ ⊙Ω-fmap2 F == ⊙Ω-fmap2 (G ⊙∘ F)
⊙Ω-fmap-fmap2 (g , idp) (f , idp) =
  ⊙λ=' (uncurry (ap-ap2 g (curry f))) idp

⊙Ω-fmap2-fmap : ∀ {i j k l m}
  {X : Ptd i} {Y : Ptd j} {U : Ptd k} {V : Ptd l} {Z : Ptd m}
  (G : (U ⊙× V) ⊙→ Z) (F₁ : X ⊙→ U) (F₂ : Y ⊙→ V)
  → ⊙Ω-fmap2 G ⊙∘ ⊙×-fmap (⊙Ω-fmap F₁) (⊙Ω-fmap F₂) == ⊙Ω-fmap2 (G ⊙∘ ⊙×-fmap F₁ F₂)
⊙Ω-fmap2-fmap (g , idp) (f₁ , idp) (f₂ , idp) =
  ⊙λ=' (λ {(p , q) → ap2-ap-l (curry g) f₁ p (ap f₂ q)
                   ∙ ap2-ap-r (λ x v → g (f₁ x , v)) f₂ p q})
       idp

⊙Ω-fmap2-diag : ∀ {i j} {X : Ptd i} {Y : Ptd j} (F : X ⊙× X ⊙→ Y)
  → ⊙Ω-fmap2 F ⊙∘ ⊙diag == ⊙Ω-fmap (F ⊙∘ ⊙diag)
⊙Ω-fmap2-diag (f , idp) = ⊙λ=' (ap2-diag (curry f)) idp

{- iterated loop spaces. [Ω^] and [Ω^'] iterates [Ω] from different sides:
   [Ω^ (S n) X = Ω (Ω^ n X)] and [Ω^' (S n) X = Ω^' n (Ω X)]. -}

module _ {i} where

  ⊙Ω^ : (n : ℕ) → Ptd i → Ptd i
  ⊙Ω^ O X = X
  ⊙Ω^ (S n) X = ⊙Ω (⊙Ω^ n X)

  Ω^ : (n : ℕ) → Ptd i → Type i
  Ω^ n X = de⊙ (⊙Ω^ n X)

  ⊙Ω^' : (n : ℕ) → Ptd i → Ptd i
  ⊙Ω^' O X = X
  ⊙Ω^' (S n) X = (⊙Ω^' n (⊙Ω X))

  Ω^' : (n : ℕ) → Ptd i → Type i
  Ω^' n X = de⊙ (⊙Ω^' n X)

{- [⊙Ω^-fmap] and [⊙Ω^-fmap2] for higher loop spaces -}

⊙Ω^-fmap : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → X ⊙→ Y → ⊙Ω^ n X ⊙→ ⊙Ω^ n Y
⊙Ω^-fmap O F = F
⊙Ω^-fmap (S n) F = ⊙Ω-fmap (⊙Ω^-fmap n F)

Ω^-fmap : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → X ⊙→ Y → (de⊙ (⊙Ω^ n X) → de⊙ (⊙Ω^ n Y))
Ω^-fmap n F = fst (⊙Ω^-fmap n F)

⊙Ω^-csmap : ∀ {i₀ i₁ j₀ j₁} (n : ℕ) {X₀ : Ptd i₀} {X₁ : Ptd i₁}
  {Y₀ : Ptd j₀} {Y₁ : Ptd j₁} {f : X₀ ⊙→ Y₀} {g : X₁ ⊙→ Y₁}
  {hX : X₀ ⊙→ X₁} {hY : Y₀ ⊙→ Y₁}
  → ⊙CommSquare f g hX hY
  → ⊙CommSquare (⊙Ω^-fmap n f) (⊙Ω^-fmap n g) (⊙Ω^-fmap n hX) (⊙Ω^-fmap n hY)
⊙Ω^-csmap O cs = cs
⊙Ω^-csmap (S n) cs = ⊙Ω-csmap (⊙Ω^-csmap n cs)

⊙Ω^'-fmap : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → X ⊙→ Y → ⊙Ω^' n X ⊙→ ⊙Ω^' n Y
⊙Ω^'-fmap O F = F
⊙Ω^'-fmap (S n) F = ⊙Ω^'-fmap n (⊙Ω-fmap F)

⊙Ω^'-csmap : ∀ {i₀ i₁ j₀ j₁} (n : ℕ) {X₀ : Ptd i₀} {X₁ : Ptd i₁}
  {Y₀ : Ptd j₀} {Y₁ : Ptd j₁} {f : X₀ ⊙→ Y₀} {g : X₁ ⊙→ Y₁}
  {hX : X₀ ⊙→ X₁} {hY : Y₀ ⊙→ Y₁}
  → ⊙CommSquare f g hX hY
  → ⊙CommSquare (⊙Ω^'-fmap n f) (⊙Ω^'-fmap n g) (⊙Ω^'-fmap n hX) (⊙Ω^'-fmap n hY)
⊙Ω^'-csmap O cs = cs
⊙Ω^'-csmap (S n) cs = ⊙Ω^'-csmap n (⊙Ω-csmap cs)

Ω^'-fmap : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → X ⊙→ Y → (de⊙ (⊙Ω^' n X) → de⊙ (⊙Ω^' n Y))
Ω^'-fmap n F = fst (⊙Ω^'-fmap n F)

⊙Ω^-fmap2 : ∀ {i j k} (n : ℕ) {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → ((X ⊙× Y) ⊙→ Z)
  → ((⊙Ω^ n X ⊙× ⊙Ω^ n Y) ⊙→ ⊙Ω^ n Z)
⊙Ω^-fmap2 O F = F
⊙Ω^-fmap2 (S n) F = ⊙Ω-fmap2 (⊙Ω^-fmap2 n F)

Ω^-fmap2 : ∀ {i j k} (n : ℕ) {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → ((X ⊙× Y) ⊙→ Z)
  → ((Ω^ n X) × (Ω^ n Y) → Ω^ n Z)
Ω^-fmap2 n F = fst (⊙Ω^-fmap2 n F)

⊙Ω^'-fmap2 : ∀ {i j k} (n : ℕ) {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → ((X ⊙× Y) ⊙→ Z)
  → ((⊙Ω^' n X ⊙× ⊙Ω^' n Y) ⊙→ ⊙Ω^' n Z)
⊙Ω^'-fmap2 O F = F
⊙Ω^'-fmap2 (S n) F = ⊙Ω^'-fmap2 n (⊙Ω-fmap2 F)

Ω^'-fmap2 : ∀ {i j k} (n : ℕ) {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → ((X ⊙× Y) ⊙→ Z)
  → ((Ω^' n X) × (Ω^' n Y) → Ω^' n Z)
Ω^'-fmap2 n F = fst (⊙Ω^'-fmap2 n F)

⊙Ω^-fmap-∘ : ∀ {i j k} (n : ℕ) {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : Y ⊙→ Z) (f : X ⊙→ Y)
  → ⊙Ω^-fmap n (g ⊙∘ f) == ⊙Ω^-fmap n g ⊙∘ ⊙Ω^-fmap n f
⊙Ω^-fmap-∘ O _ _ = idp
⊙Ω^-fmap-∘ (S n) g f = ap ⊙Ω-fmap (⊙Ω^-fmap-∘ n g f)
                     ∙ ⊙Ω-fmap-∘ (⊙Ω^-fmap n g) (⊙Ω^-fmap n f)

⊙Ω^-fmap-idf : ∀ {i} (n : ℕ) {X : Ptd i} → ⊙Ω^-fmap n (⊙idf X) == ⊙idf _
⊙Ω^-fmap-idf O = idp
⊙Ω^-fmap-idf (S n) = ap ⊙Ω-fmap (⊙Ω^-fmap-idf n) ∙ ⊙Ω-fmap-idf

Ω^-fmap-idf : ∀ {i} (n : ℕ) {X : Ptd i} → Ω^-fmap n (⊙idf X) == idf _
Ω^-fmap-idf n = fst= $ ⊙Ω^-fmap-idf n

⊙Ω^'-fmap-idf : ∀ {i} (n : ℕ) {X : Ptd i} → ⊙Ω^'-fmap n (⊙idf X) == ⊙idf _
⊙Ω^'-fmap-idf O = idp
⊙Ω^'-fmap-idf (S n) = ap (⊙Ω^'-fmap n) ⊙Ω-fmap-idf ∙ ⊙Ω^'-fmap-idf n

Ω^'-fmap-idf : ∀ {i} (n : ℕ) {X : Ptd i} → Ω^'-fmap n (⊙idf X) == idf _
Ω^'-fmap-idf n = fst= $ ⊙Ω^'-fmap-idf n

⊙Ω^-fmap-fmap2 : ∀ {i j k l} (n : ℕ) {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (G : Z ⊙→ W) (F : (X ⊙× Y) ⊙→ Z)
  → ⊙Ω^-fmap n G ⊙∘ ⊙Ω^-fmap2 n F == ⊙Ω^-fmap2 n (G ⊙∘ F)
⊙Ω^-fmap-fmap2 O G F = idp
⊙Ω^-fmap-fmap2 (S n) G F = ⊙Ω-fmap-fmap2 (⊙Ω^-fmap n G) (⊙Ω^-fmap2 n F) ∙ ap ⊙Ω-fmap2 (⊙Ω^-fmap-fmap2 n G F)

Ω^-fmap-fmap2 : ∀ {i j k l} (n : ℕ) {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (G : Z ⊙→ W) (F : (X ⊙× Y) ⊙→ Z)
  → Ω^-fmap n G ∘ Ω^-fmap2 n F == Ω^-fmap2 n (G ⊙∘ F)
Ω^-fmap-fmap2 n G F = fst= $ ⊙Ω^-fmap-fmap2 n G F

⊙Ω^-fmap2-fst : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → ⊙Ω^-fmap2 n {X} {Y} ⊙fst == ⊙fst
⊙Ω^-fmap2-fst O = idp
⊙Ω^-fmap2-fst (S n) = ap ⊙Ω-fmap2 (⊙Ω^-fmap2-fst n) ∙ ⊙Ω-fmap2-fst

Ω^-fmap2-fst : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → Ω^-fmap2 n {X} {Y} ⊙fst == fst
Ω^-fmap2-fst n = fst= $ ⊙Ω^-fmap2-fst n

⊙Ω^-fmap2-snd : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → ⊙Ω^-fmap2 n {X} {Y} ⊙snd == ⊙snd
⊙Ω^-fmap2-snd O = idp
⊙Ω^-fmap2-snd (S n) = ap ⊙Ω-fmap2 (⊙Ω^-fmap2-snd n) ∙ ⊙Ω-fmap2-snd

Ω^-fmap2-snd : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → Ω^-fmap2 n {X} {Y} ⊙snd == snd
Ω^-fmap2-snd n = fst= $ ⊙Ω^-fmap2-snd n

⊙Ω^-fmap2-fmap : ∀ {i j k l m} (n : ℕ)
  {X : Ptd i} {Y : Ptd j} {U : Ptd k} {V : Ptd l} {Z : Ptd m}
  (G : (U ⊙× V) ⊙→ Z) (F₁ : X ⊙→ U) (F₂ : Y ⊙→ V)
  → ⊙Ω^-fmap2 n G ⊙∘ ⊙×-fmap (⊙Ω^-fmap n F₁) (⊙Ω^-fmap n F₂) == ⊙Ω^-fmap2 n (G ⊙∘ ⊙×-fmap F₁ F₂)
⊙Ω^-fmap2-fmap O G F₁ F₂ = idp
⊙Ω^-fmap2-fmap (S n) G F₁ F₂ =
  ⊙Ω-fmap2-fmap (⊙Ω^-fmap2 n G) (⊙Ω^-fmap n F₁) (⊙Ω^-fmap n F₂) ∙ ap ⊙Ω-fmap2 (⊙Ω^-fmap2-fmap n G F₁ F₂)

Ω^-fmap2-fmap : ∀ {i j k l m} (n : ℕ)
  {X : Ptd i} {Y : Ptd j} {U : Ptd k} {V : Ptd l} {Z : Ptd m}
  (G : (U ⊙× V) ⊙→ Z) (F₁ : X ⊙→ U) (F₂ : Y ⊙→ V)
  → Ω^-fmap2 n G ∘ ×-fmap (Ω^-fmap n F₁) (Ω^-fmap n F₂) == Ω^-fmap2 n (G ⊙∘ ⊙×-fmap F₁ F₂)
Ω^-fmap2-fmap n G F₁ F₂ = fst= $ ⊙Ω^-fmap2-fmap n G F₁ F₂

⊙Ω^-fmap2-diag : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j} (F : X ⊙× X ⊙→ Y)
  → ⊙Ω^-fmap2 n F ⊙∘ ⊙diag == ⊙Ω^-fmap n (F ⊙∘ ⊙diag)
⊙Ω^-fmap2-diag O F = idp
⊙Ω^-fmap2-diag (S n) F = ⊙Ω-fmap2-diag (⊙Ω^-fmap2 n F) ∙ ap ⊙Ω-fmap (⊙Ω^-fmap2-diag n F)

Ω^-fmap2-diag : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j} (F : X ⊙× X ⊙→ Y)
  → Ω^-fmap2 n F ∘ diag == Ω^-fmap n (F ⊙∘ ⊙diag)
Ω^-fmap2-diag n F = fst= $ ⊙Ω^-fmap2-diag n F

{- for n ≥ 1, we have a group structure on the loop space -}
module _ {i} (n : ℕ) {X : Ptd i} where

  Ω^S-! : Ω^ (S n) X → Ω^ (S n) X
  Ω^S-! = Ω-!

  Ω^S-∙ : Ω^ (S n) X → Ω^ (S n) X → Ω^ (S n) X
  Ω^S-∙ = Ω-∙

module _ {i} where

  Ω^'S-! : (n : ℕ) {X : Ptd i} → Ω^' (S n) X → Ω^' (S n) X
  Ω^'S-! O = Ω-!
  Ω^'S-! (S n) {X} = Ω^'S-! n {⊙Ω X}

  Ω^'S-∙ : (n : ℕ) {X : Ptd i} → Ω^' (S n) X → Ω^' (S n) X → Ω^' (S n) X
  Ω^'S-∙ O = Ω-∙
  Ω^'S-∙ (S n) {X} = Ω^'S-∙ n {⊙Ω X}

idp^ : ∀ {i} (n : ℕ) {X : Ptd i} → Ω^ n X
idp^ n {X} = pt (⊙Ω^ n X)

idp^' : ∀ {i} (n : ℕ) {X : Ptd i} → Ω^' n X
idp^' n {X} = pt (⊙Ω^' n X)

module _ {i} (n : ℕ) {X : Ptd i} where

  {- Prove these as lemmas now
   - so we don't have to deal with the n = O case later -}

  Ω^S-∙-unit-l : (q : Ω^ (S n) X)
    → (Ω^S-∙ n (idp^ (S n)) q) == q
  Ω^S-∙-unit-l _ = idp

  Ω^S-∙-unit-r : (q : Ω^ (S n) X)
    → (Ω^S-∙ n q (idp^ (S n))) == q
  Ω^S-∙-unit-r = ∙-unit-r

  Ω^S-∙-assoc : (p q r : Ω^ (S n) X)
    → Ω^S-∙ n (Ω^S-∙ n p q) r == Ω^S-∙ n p (Ω^S-∙ n q r)
  Ω^S-∙-assoc = ∙-assoc

  Ω^S-!-inv-l : (p : Ω^ (S n) X)
    → Ω^S-∙ n (Ω^S-! n p) p == idp^ (S n)
  Ω^S-!-inv-l = !-inv-l

  Ω^S-!-inv-r : (p : Ω^ (S n) X)
    → Ω^S-∙ n p (Ω^S-! n p) == idp^ (S n)
  Ω^S-!-inv-r = !-inv-r

module _ {i} where

  Ω^'S-∙-unit-l : (n : ℕ) {X : Ptd i} (q : Ω^' (S n) X)
    → (Ω^'S-∙ n (idp^' (S n)) q) == q
  Ω^'S-∙-unit-l O _ = idp
  Ω^'S-∙-unit-l (S n) = Ω^'S-∙-unit-l n

  Ω^'S-∙-unit-r : (n : ℕ) {X : Ptd i} (q : Ω^' (S n) X)
    → (Ω^'S-∙ n q (idp^' (S n))) == q
  Ω^'S-∙-unit-r O = ∙-unit-r
  Ω^'S-∙-unit-r (S n) = Ω^'S-∙-unit-r n

  Ω^'S-∙-assoc : (n : ℕ) {X : Ptd i} (p q r : Ω^' (S n) X)
    → Ω^'S-∙ n (Ω^'S-∙ n p q) r == Ω^'S-∙ n p (Ω^'S-∙ n q r)
  Ω^'S-∙-assoc O = ∙-assoc
  Ω^'S-∙-assoc (S n) = Ω^'S-∙-assoc n

  Ω^'S-!-inv-l : (n : ℕ) {X : Ptd i} (p : Ω^' (S n) X)
    → Ω^'S-∙ n (Ω^'S-! n p) p == idp^' (S n)
  Ω^'S-!-inv-l O = !-inv-l
  Ω^'S-!-inv-l (S n) = Ω^'S-!-inv-l n

  Ω^'S-!-inv-r : (n : ℕ) {X : Ptd i} (p : Ω^' (S n) X)
    → Ω^'S-∙ n p (Ω^'S-! n p) == idp^' (S n)
  Ω^'S-!-inv-r O = !-inv-r
  Ω^'S-!-inv-r (S n) = Ω^'S-!-inv-r n

module _ where
  Ω-fmap-∙ : ∀ {i j} {X : Ptd i} {Y : Ptd j} (F : X ⊙→ Y) (p q : Ω X)
    → Ω-fmap F (p ∙ q) == Ω-fmap F p ∙ Ω-fmap F q
  Ω-fmap-∙ (f , idp) p q = ap-∙ f p q

  Ω^S-fmap-∙ : ∀ {i j} (n : ℕ)
    {X : Ptd i} {Y : Ptd j} (F : X ⊙→ Y) (p q : Ω^ (S n) X)
    → Ω^-fmap (S n) F (Ω^S-∙ n p q)
      == Ω^S-∙ n (Ω^-fmap (S n) F p) (Ω^-fmap (S n) F q)
  Ω^S-fmap-∙ n F = Ω-fmap-∙ (⊙Ω^-fmap n F)

  Ω^'S-fmap-∙ : ∀ {i j} (n : ℕ)
    {X : Ptd i} {Y : Ptd j} (F : X ⊙→ Y) (p q : Ω^' (S n) X)
    → Ω^'-fmap (S n) F (Ω^'S-∙ n p q)
      == Ω^'S-∙ n (Ω^'-fmap (S n) F p) (Ω^'-fmap (S n) F q)
  Ω^'S-fmap-∙ O = Ω-fmap-∙
  Ω^'S-fmap-∙ (S n) F = Ω^'S-fmap-∙ n (⊙Ω-fmap F)

{- [Ω^] preserves (pointed) equivalences -}
module _ {i j} {X : Ptd i} {Y : Ptd j} where

  Ω^-isemap : (n : ℕ) (F : X ⊙→ Y) (e : is-equiv (fst F))
    → is-equiv (Ω^-fmap n F)
  Ω^-isemap O F e = e
  Ω^-isemap (S n) F e = Ω-isemap (⊙Ω^-fmap n F) (Ω^-isemap n F e)

  ⊙Ω^-isemap = Ω^-isemap

  Ω^-emap : (n : ℕ) → X ⊙≃ Y → Ω^ n X ≃ Ω^ n Y
  Ω^-emap n (F , e) = Ω^-fmap n F , Ω^-isemap n F e

  ⊙Ω^-emap : (n : ℕ) → X ⊙≃ Y → ⊙Ω^ n X ⊙≃ ⊙Ω^ n Y
  ⊙Ω^-emap n (F , e) = ⊙Ω^-fmap n F , ⊙Ω^-isemap n F e

⊙Ω^-csemap : ∀ {i₀ i₁ j₀ j₁} (n : ℕ) {X₀ : Ptd i₀} {X₁ : Ptd i₁}
  {Y₀ : Ptd j₀} {Y₁ : Ptd j₁} {f : X₀ ⊙→ Y₀} {g : X₁ ⊙→ Y₁}
  {hX : X₀ ⊙→ X₁} {hY : Y₀ ⊙→ Y₁}
  → ⊙CommSquareEquiv f g hX hY
  → ⊙CommSquareEquiv (⊙Ω^-fmap n f) (⊙Ω^-fmap n g) (⊙Ω^-fmap n hX) (⊙Ω^-fmap n hY)
⊙Ω^-csemap n {hX = hX} {hY} (cs , hX-ise , hY-ise) = ⊙Ω^-csmap n cs , Ω^-isemap n hX hX-ise , Ω^-isemap n hY hY-ise

{- [Ω^'] preserves (pointed) equivalences too -}
module _ {i j} where

  Ω^'-isemap : {X : Ptd i} {Y : Ptd j} (n : ℕ) (F : X ⊙→ Y) (e : is-equiv (fst F))
    → is-equiv (Ω^'-fmap n F)
  Ω^'-isemap O F e = e
  Ω^'-isemap (S n) F e = Ω^'-isemap n (⊙Ω-fmap F) (Ω-isemap F e)

  ⊙Ω^'-isemap = Ω^'-isemap

  Ω^'-emap : {X : Ptd i} {Y : Ptd j} (n : ℕ) → X ⊙≃ Y → Ω^' n X ≃ Ω^' n Y
  Ω^'-emap n (F , e) = Ω^'-fmap n F , Ω^'-isemap n F e

  ⊙Ω^'-emap : {X : Ptd i} {Y : Ptd j} (n : ℕ) → X ⊙≃ Y → ⊙Ω^' n X ⊙≃ ⊙Ω^' n Y
  ⊙Ω^'-emap n (F , e) = ⊙Ω^'-fmap n F , ⊙Ω^'-isemap n F e

⊙Ω^'-csemap : ∀ {i₀ i₁ j₀ j₁} (n : ℕ) {X₀ : Ptd i₀} {X₁ : Ptd i₁}
  {Y₀ : Ptd j₀} {Y₁ : Ptd j₁} {f : X₀ ⊙→ Y₀} {g : X₁ ⊙→ Y₁}
  {hX : X₀ ⊙→ X₁} {hY : Y₀ ⊙→ Y₁}
  → ⊙CommSquareEquiv f g hX hY
  → ⊙CommSquareEquiv (⊙Ω^'-fmap n f) (⊙Ω^'-fmap n g) (⊙Ω^'-fmap n hX) (⊙Ω^'-fmap n hY)
⊙Ω^'-csemap n {hX = hX} {hY} (cs , hX-ise , hY-ise) = ⊙Ω^'-csmap n cs , Ω^'-isemap n hX hX-ise , Ω^'-isemap n hY hY-ise

Ω^-level : ∀ {i} (m : ℕ₋₂) (n : ℕ) (X : Ptd i)
  → (has-level (⟨ n ⟩₋₂ +2+ m) (de⊙ X) → has-level m (Ω^ n X))
Ω^-level m O X pX = pX
Ω^-level m (S n) X pX =
  has-level-apply (Ω^-level (S m) n X
    (transport (λ k → has-level k (de⊙ X)) (! (+2+-βr ⟨ n ⟩₋₂ m)) pX))
    (idp^ n) (idp^ n)

{- As for the levels of [Ω^'], these special cases can avoid
   trailing constants, and it seems we only need the following
   two special cases. -}

Ω^'-is-set : ∀ {i} (n : ℕ) (X : Ptd i)
  → (has-level ⟨ n ⟩ (de⊙ X) → is-set (Ω^' n X))
Ω^'-is-set O X pX = pX
Ω^'-is-set (S n) X pX = Ω^'-is-set n (⊙Ω X) (has-level-apply pX (pt X) (pt X))

Ω^'-is-prop : ∀ {i} (n : ℕ) (X : Ptd i)
  → (has-level ⟨ n ⟩₋₁ (de⊙ X) → is-prop (Ω^' n X))
Ω^'-is-prop O X pX = pX
Ω^'-is-prop (S n) X pX = Ω^'-is-prop n (⊙Ω X) (has-level-apply pX (pt X) (pt X))

Ω^-conn : ∀ {i} (m : ℕ₋₂) (n : ℕ) (X : Ptd i)
  → (is-connected (⟨ n ⟩₋₂ +2+ m) (de⊙ X)) → is-connected m (Ω^ n X)
Ω^-conn m O X pX = pX
Ω^-conn m (S n) X pX =
  path-conn $ Ω^-conn (S m) n X $
    transport (λ k → is-connected k (de⊙ X)) (! (+2+-βr ⟨ n ⟩₋₂ m)) pX

{- Eckmann-Hilton argument -}
module _ {i} {X : Ptd i} where

  Ω-fmap2-∙ : (α β : Ω^ 2 X) → ap2 _∙_ α β == Ω^S-∙ 1 α β
  Ω-fmap2-∙ α β = ap2-out _∙_ α β ∙ ap2 _∙_ (lemma α) (ap-idf β)
    where
    lemma : ∀ {i} {A : Type i} {x y : A} {p q : x == y} (α : p == q)
      → ap (λ r → r ∙ idp) α == ∙-unit-r p ∙ α ∙' ! (∙-unit-r q)
    lemma {p = idp} idp = idp

  ⊙Ω-fmap2-∙ : ⊙Ω-fmap2 (⊙Ω-∙ {X = X}) == ⊙Ω-∙
  ⊙Ω-fmap2-∙ = ⊙λ=' (uncurry Ω-fmap2-∙) idp

  Ω^2-∙-comm : (α β : Ω^ 2 X) → Ω^S-∙ 1 α β == Ω^S-∙ 1 β α
  Ω^2-∙-comm α β = ! (⋆2=Ω^S-∙ α β) ∙ ⋆2=⋆'2 α β ∙ ⋆'2=Ω^S-∙ α β
    where
      ⋆2=Ω^S-∙ : (α β : Ω^ 2 X) → α ⋆2 β == Ω^S-∙ 1 α β
      ⋆2=Ω^S-∙ α β = ap (λ π → π ∙ β) (∙-unit-r α)

      ⋆'2=Ω^S-∙ : (α β : Ω^ 2  X) → α ⋆'2 β == Ω^S-∙ 1 β α
      ⋆'2=Ω^S-∙ α β = ap (λ π → β ∙ π) (∙-unit-r α)

{- NOT USED and DUPLICATE of [Ω^S-Trunc-preiso] in lib.groups.HomotopyGroup.
   XXX Should be an equivalence.

{- Pushing truncation through loop space -}
module _ {i} where

  Trunc-Ω^-conv : (m : ℕ₋₂) (n : ℕ) (X : Ptd i)
    → ⊙Trunc m (⊙Ω^ n X) == ⊙Ω^ n (⊙Trunc (⟨ n ⟩₋₂ +2+ m) X)
  Trunc-Ω^-conv m O X = idp
  Trunc-Ω^-conv m (S n) X =
    ⊙Trunc m (⊙Ω^ (S n) X)
      =⟨ ! (pair= (Trunc=-path [ _ ] [ _ ]) (↓-idf-ua-in _ idp)) ⟩
    ⊙Ω (⊙Trunc (S m) (⊙Ω^ n X))
      =⟨ ap ⊙Ω (Trunc-Ω^-conv (S m) n X) ⟩
    ⊙Ω^ (S n) (⊙Trunc (⟨ n ⟩₋₂ +2+ S m) X)
      =⟨ +2+-βr ⟨ n ⟩₋₂ m |in-ctx (λ k → ⊙Ω^ (S n) (⊙Trunc k X)) ⟩
    ⊙Ω^ (S n) (⊙Trunc (S ⟨ n ⟩₋₂ +2+ m) X) =∎

  Ω-Trunc-econv : (m : ℕ₋₂) (X : Ptd i)
    → Ω (⊙Trunc (S m) X) ≃ Trunc m (Ω X)
  Ω-Trunc-econv m X = Trunc=-equiv [ pt X ] [ pt X ]
-}

{- Our definition of [Ω^] builds up loops from the outside,
 - but this is equivalent to building up from the inside -}
module _ {i} where
  ⊙Ω^-Ω-split : (n : ℕ) (X : Ptd i)
    → (⊙Ω^ (S n) X ⊙→ ⊙Ω^ n (⊙Ω X))
  ⊙Ω^-Ω-split O _ = (idf _ , idp)
  ⊙Ω^-Ω-split (S n) X = ⊙Ω-fmap (⊙Ω^-Ω-split n X)

  Ω^-Ω-split : (n : ℕ) (X : Ptd i)
    → (Ω^ (S n) X → Ω^ n (⊙Ω X))
  Ω^-Ω-split n X = fst (⊙Ω^-Ω-split n X)

  Ω^S-Ω-split-∙ : (n : ℕ)
    (X : Ptd i) (p q : Ω^ (S (S n)) X)
    → Ω^-Ω-split (S n) X (Ω^S-∙ (S n) p q)
      == Ω^S-∙ n (Ω^-Ω-split (S n) X p) (Ω^-Ω-split (S n) X q)
  Ω^S-Ω-split-∙ n X p q =
    Ω^S-fmap-∙ 0 (⊙Ω^-Ω-split n X) p q

  Ω^-Ω-split-is-equiv : (n : ℕ) (X : Ptd i)
    → is-equiv (Ω^-Ω-split n X)
  Ω^-Ω-split-is-equiv O X = is-eq (idf _) (idf _) (λ _ → idp) (λ _ → idp)
  Ω^-Ω-split-is-equiv (S n) X =
    ⊙Ω^-isemap 1 (⊙Ω^-Ω-split n X) (Ω^-Ω-split-is-equiv n X)

  Ω^-Ω-split-equiv : (n : ℕ) (X : Ptd i) → Ω^ (S n) X ≃ Ω^ n (⊙Ω X)
  Ω^-Ω-split-equiv n X = _ , Ω^-Ω-split-is-equiv n X

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  Ω-× : Ω (X ⊙× Y) ≃ Ω X × Ω Y
  Ω-× = equiv
    (λ p → fst×= p , snd×= p)
    (λ p → pair×= (fst p) (snd p))
    (λ p → pair×= (fst×=-β (fst p) (snd p)) (snd×=-β (fst p) (snd p)))
    (! ∘ pair×=-η)

  ⊙Ω-× : ⊙Ω (X ⊙× Y) ⊙≃ ⊙Ω X ⊙× ⊙Ω Y
  ⊙Ω-× = ≃-to-⊙≃ Ω-× idp

  Ω-×-∙ : ∀ (p q : Ω (X ⊙× Y))
    → –> Ω-× (p ∙ q) == (fst (–> Ω-× p) ∙ fst (–> Ω-× q) , snd (–> Ω-× p) ∙ snd (–> Ω-× q))
  Ω-×-∙ p q = pair×= (Ω-fmap-∙ ⊙fst p q) (Ω-fmap-∙ ⊙snd p q)

module _ {i j} where

  ⊙Ω^-× : ∀ (n : ℕ) (X : Ptd i) (Y : Ptd j)
    → ⊙Ω^ n (X ⊙× Y) ⊙≃ ⊙Ω^ n X ⊙× ⊙Ω^ n Y
  ⊙Ω^-× O _ _ = ⊙ide _
  ⊙Ω^-× (S n) X Y = ⊙Ω-× (⊙Ω^ n X) (⊙Ω^ n Y) ⊙∘e ⊙Ω-emap (⊙Ω^-× n X Y)

  ⊙Ω^'-× : ∀ (n : ℕ) (X : Ptd i) (Y : Ptd j)
    → ⊙Ω^' n (X ⊙× Y) ⊙≃ ⊙Ω^' n X ⊙× ⊙Ω^' n Y
  ⊙Ω^'-× O _ _ = ⊙ide _
  ⊙Ω^'-× (S n) X Y = ⊙Ω^'-× n (⊙Ω X) (⊙Ω Y) ⊙∘e ⊙Ω^'-emap n (⊙Ω-× X Y)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- Step-indexed logical relations based on relational big-step semantics
-- for ILC-based incremental computation.

-- Goal: prove the fundamental lemma for a ternary logical relation (change
-- validity) across t1, dt and t2. The fundamnetal lemma relates t, derive t and
-- t. That is, we relate a term evaluated relative to an original environment,
-- its derivative evaluated relative to a valid environment change, and the
-- original term evaluated relative to an updated environment.
--
-- Missing goal: here ⊕ isn't defined and wouldn't yet agree with change
-- validity.
--
-- This development is strongly inspired by "Imperative self-adjusting
-- computation" (ISAC below), POPL'08, including the choice of using ANF syntax
-- to simplify some step-indexing proofs.
--
-- In fact, this development is typed, hence some parts of the model are closer
-- to Ahmed (ESOP 2006), "Step-Indexed Syntactic Logical Relations for Recursive
-- and Quantified Types". But for many relevant aspects, the two papers are
-- very similar. In fact, I first defined similar logical relations
-- without types, but they require a trickier recursion scheme for well-founded
-- recursion, and I failed to do any proof in that setting.
--
-- The original inspiration came from Dargaye and Leroy (2010), "A verified
-- framework for higher-order uncurrying optimizations", but we ended up looking
-- at their source.
--
-- The main insight from the ISAC paper missing from the other one is how to
-- step-index a big-step semantics correctly: just ensure that the steps in the
-- big-step semantics agree with the ones in the small-step semantics. *Then*
-- everything just works with big-step semantics. Quite a few other details are
-- fiddly, but those are the same in small-step semantics.
--
-- The crucial novelty here is that we relate two computations on different
-- inputs. So we only conclude their results are related if both terminate; the
-- relation for computations does not prove that if the first computation
-- terminates, then the second terminates as well.
--
-- Instead, e1, de and e2 are related at k steps if, whenever e1 terminates in j
-- < k steps and e2 terminates with any step count, then de terminates (with any
-- step count) and their results are related at k - j steps.
--
-- Even when e1 terminates in j steps implies that e2 terminates, e2 gets no
-- bound. Similarly, we do not bound in how many steps de terminates, since on
-- big inputs it might take long.

module Thesis.SIRelBigStep.README where

-- Base language
import Thesis.SIRelBigStep.Lang
-- Which comprises:
import Thesis.SIRelBigStep.Types
import Thesis.SIRelBigStep.Syntax
-- Denotational semantics:
import Thesis.SIRelBigStep.DenSem
-- Big-step operations semantics:
import Thesis.SIRelBigStep.OpSem
-- Show these two semantics are equivalent:
import Thesis.SIRelBigStep.SemEquiv
-- It follows that the big-step semantics is deterministic.

-- To show that the big-step semantics is total, give a proof of (CBV) strong
-- normalization for this calculus, using a unary logical relation.
-- This is just TAPL Ch. 12, adapted to our environment-based big-step
-- semantics.
import Thesis.SIRelBigStep.Normalization

-- Change language
import Thesis.SIRelBigStep.DLang

-- Which comprises:
import Thesis.SIRelBigStep.DSyntax
-- The operational semantics also defines ⊕:
import Thesis.SIRelBigStep.DOpSem

-- Differentiation:
import Thesis.SIRelBigStep.DLangDerive

-- Small extra arithmetic lemmas for step-indexes.
import Thesis.SIRelBigStep.ArithExtra
-- Step-indexed logical relations for validity, their monotonicity and agreement with ⊕
import Thesis.SIRelBigStep.IlcSILR
-- Prove the fundamental property
import Thesis.SIRelBigStep.FundamentalProperty

-- Conclude our thesis
import Thesis.SIRelBigStep.DeriveCorrect

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module PiFrac.Eval where
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Data.List as L hiding (_∷_)
open import Data.Maybe
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_)
open import PiFrac.Syntax
open import PiFrac.Opsem
open import PiFrac.NoRepeat

-- Stuck states must be either of the form ［ c ∣ v ∣ ☐ ］ or ⊠
Stuck : ∀ {st} → is-stuck st
      → (Σ[ A ∈ 𝕌 ] Σ[ B ∈ 𝕌 ] Σ[ c ∈ A ↔ B ] Σ[ v ∈ ⟦ B ⟧ ] st ≡ ［ c ∣ v ∣ ☐ ］) ⊎ st ≡ ⊠
Stuck {⟨ uniti₊l  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ unite₊l  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ swap₊    ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ assocl₊  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ assocr₊  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ unite⋆l  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ uniti⋆l  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ swap⋆    ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ assocl⋆  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ assocr⋆  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ dist     ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ factor   ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ id↔      ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₂))
Stuck {⟨ ηₓ v     ∣ tt      ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦η))
Stuck {⟨ εₓ v     ∣ v' , ↻  ∣ κ ⟩} stuck with v ≟ v'
... | yes eq  = ⊥-elim (stuck (_ , ↦ε₁ {eq = eq}))
... | no  neq = ⊥-elim (stuck (_ , ↦ε₂ {neq = neq}))
Stuck {⟨ c₁ ⨾ c₂  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₃))
Stuck {⟨ c₁ ⊕ c₂  ∣ inj₁ x  ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₄))
Stuck {⟨ c₁ ⊕ c₂  ∣ inj₂ y  ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₅))
Stuck {⟨ c₁ ⊗ c₂  ∣ (x , y) ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₆))
Stuck {［ c ∣ v ∣ ☐               ］} stuck = inj₁ (_ , _ , _ , _ , refl)
Stuck {［ c ∣ v ∣ ☐⨾ c₂ • κ       ］} stuck = ⊥-elim (stuck (_ , ↦₇))
Stuck {［ c ∣ v ∣ c₁ ⨾☐• κ        ］} stuck = ⊥-elim (stuck (_ , ↦₁₀))
Stuck {［ c ∣ v ∣ ☐⊕ c₂ • κ       ］} stuck = ⊥-elim (stuck (_ , ↦₁₁))
Stuck {［ c ∣ v ∣ c₁ ⊕☐• κ        ］} stuck = ⊥-elim (stuck (_ , ↦₁₂))
Stuck {［ c ∣ v ∣ ☐⊗[ c₂ , y ]• κ ］} stuck = ⊥-elim (stuck (_ , ↦₈))
Stuck {［ c ∣ v ∣ [ c₁ , x ]⊗☐• κ ］} stuck = ⊥-elim (stuck (_ , ↦₉))
Stuck {⊠} stuck = inj₂ refl

-- Auxiliary function for forward evaluator
ev : ∀ {A B κ} → (c : A ↔ B) (v : ⟦ A ⟧)
   → Σ[ v' ∈ ⟦ B ⟧ ] ⟨ c ∣ v ∣ κ ⟩ ↦* ［ c ∣ v' ∣ κ ］
   ⊎ ⟨ c ∣ v ∣ κ ⟩ ↦* ⊠
ev uniti₊l v = inj₁ ((inj₂ v) , ↦₁ ∷ ◾)
ev unite₊l (inj₂ y) = inj₁ (y , ↦₁ ∷ ◾)
ev swap₊ (inj₁ v) = inj₁ (inj₂ v , (↦₁ ∷ ◾))
ev swap₊ (inj₂ v) = inj₁ (inj₁ v , (↦₁ ∷ ◾))
ev assocl₊ (inj₁ v) = inj₁ (inj₁ (inj₁ v) , (↦₁ ∷ ◾))
ev assocl₊ (inj₂ (inj₁ v)) = inj₁ (inj₁ (inj₂ v) , (↦₁ ∷ ◾))
ev assocl₊ (inj₂ (inj₂ v)) = inj₁ (inj₂ v , (↦₁ ∷ ◾))
ev assocr₊ (inj₁ (inj₁ v)) = inj₁ (inj₁ v , (↦₁ ∷ ◾))
ev assocr₊ (inj₁ (inj₂ v)) = inj₁ (inj₂ (inj₁ v) , (↦₁ ∷ ◾))
ev assocr₊ (inj₂ v) = inj₁ (inj₂ (inj₂ v) , (↦₁ ∷ ◾))
ev unite⋆l (tt , v) = inj₁ (v , (↦₁ ∷ ◾))
ev uniti⋆l v = inj₁ ((tt , v) , (↦₁ ∷ ◾))
ev swap⋆ (x , y) = inj₁ ((y , x) , (↦₁ ∷ ◾))
ev assocl⋆ (x , (y , z)) = inj₁ (((x , y) , z) , (↦₁ ∷ ◾))
ev assocr⋆ ((x , y) , z) = inj₁ ((x , (y , z)) , (↦₁ ∷ ◾))
ev dist (inj₁ x , z) = inj₁ (inj₁ (x , z) , (↦₁ ∷ ◾))
ev dist (inj₂ y , z) = inj₁ (inj₂ (y , z) , (↦₁ ∷ ◾))
ev factor (inj₁ (x , z)) = inj₁ ((inj₁ x , z) , (↦₁ ∷ ◾))
ev factor (inj₂ (y , z)) = inj₁ ((inj₂ y , z) , (↦₁ ∷ ◾))
ev id↔ v = inj₁ (v , (↦₂ ∷ ◾))
ev {κ = κ} (c₁ ⨾ c₂) v₁ with ev {κ = ☐⨾ c₂ • κ} c₁ v₁
... | inj₁ (v₂ , c₁↦*) with ev {κ = c₁ ⨾☐• κ} c₂ v₂
... | inj₁ (v₃ , c₂↦*) = inj₁ (v₃ , ((↦₃ ∷ c₁↦* ++↦ (↦₇ ∷ ◾)) ++↦ (c₂↦* ++↦ (↦₁₀ ∷ ◾))))
... | inj₂ c₂↦* = inj₂ ((↦₃ ∷ c₁↦* ++↦ (↦₇ ∷ ◾)) ++↦ c₂↦*)
ev {κ = κ} (c₁ ⨾ c₂) v₁ | inj₂ c₁↦* = inj₂ (↦₃ ∷ c₁↦*)
ev {κ = κ} (c₁ ⊕ c₂) (inj₁ x) with ev {κ = ☐⊕ c₂ • κ} c₁ x
... | inj₁ (x' , c₁↦*) = inj₁ (inj₁ x' , ↦₄ ∷ c₁↦* ++↦ (↦₁₁ ∷ ◾))
... | inj₂ c₁↦* = inj₂ (↦₄ ∷ c₁↦*)
ev {κ = κ} (c₁ ⊕ c₂) (inj₂ y) with ev {κ = c₁ ⊕☐• κ} c₂ y
... | inj₁ (y' , c₂↦*) = inj₁ (inj₂ y' , ↦₅ ∷ c₂↦* ++↦ (↦₁₂ ∷ ◾))
... | inj₂ c₂↦* = inj₂ (↦₅ ∷ c₂↦*)
ev {κ = κ} (c₁ ⊗ c₂) (x , y) with ev {κ = ☐⊗[ c₂ , y ]• κ} c₁ x
... | inj₁ (x' , c₁↦*) with ev {κ = [ c₁ , x' ]⊗☐• κ} c₂ y
... | inj₁ (y' , c₂↦*) = inj₁ ((x' , y') , ((↦₆ ∷ c₁↦*) ++↦ ((↦₈ ∷ c₂↦*) ++↦ (↦₉ ∷ ◾))))
... | inj₂ c₂↦* = inj₂ ((↦₆ ∷ c₁↦*) ++↦ (↦₈ ∷ c₂↦*))
ev {κ = κ} (c₁ ⊗ c₂) (x , y) | inj₂ c₁↦* = inj₂ (↦₆ ∷ c₁↦*)
ev (ηₓ v) tt = inj₁ ((v , ↻) , (↦η ∷ ◾))
ev (εₓ v) (v' , ↻) with v ≟ v'
... | yes eq  = inj₁ (tt , (↦ε₁ {eq = eq} ∷ ◾))
... | no  neq = inj₂ (↦ε₂ {neq = neq} ∷ ◾)

-- Forward evaluator for PiFrac
eval : ∀ {A B} → (c : A ↔ B) → ⟦ A ⟧ → Maybe ⟦ B ⟧
eval c v = [ just ∘ proj₁ , (λ _ → nothing) ]′ (ev {κ = ☐} c v)

-- Forward evaluator which returns execution trace
evalₜᵣ : ∀ {A B} → (c : A ↔ B) → ⟦ A ⟧ → List State
evalₜᵣ c v = [ convert ∘ proj₂ , convert ]′ (ev {κ = ☐} c v)
  where
    convert : ∀ {st st'} → st ↦* st' → List State
    convert (◾ {st}) = st L.∷ []
    convert (_∷_ {st} r rs) = st L.∷ convert rs

-- Auxiliary function for backward evaluator
evᵣₑᵥ : ∀ {A B κ} → (c : A ↔ B) (v : ⟦ B ⟧)
      → Σ[ v' ∈ ⟦ A ⟧ ] ［ c ∣ v ∣ κ ］ ↦ᵣₑᵥ* ⟨ c ∣ v' ∣ κ ⟩
      ⊎ ∃[ A ] (∃[ v' ] (∃[ v'' ] (∃[ κ' ] (v' ≢ v'' × ［ c ∣ v ∣ κ ］ ↦ᵣₑᵥ* ［ ηₓ {A} v' ∣ (v'' , ↻) ∣ κ' ］))))
evᵣₑᵥ uniti₊l (inj₂ v) = inj₁ (v , (↦₁ ᵣₑᵥ ∷ ◾))
evᵣₑᵥ unite₊l v = inj₁ ((inj₂ v) , (↦₁ ᵣₑᵥ ∷ ◾))
evᵣₑᵥ swap₊ (inj₁ x) = inj₁ (inj₂ x , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ swap₊ (inj₂ y) = inj₁ (inj₁ y , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocl₊ (inj₁ (inj₁ x)) = inj₁ (inj₁ x , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocl₊ (inj₁ (inj₂ y)) = inj₁ (inj₂ (inj₁ y) , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocl₊ (inj₂ z) = inj₁ (inj₂ (inj₂ z) , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocr₊ (inj₁ x) = inj₁ (inj₁ (inj₁ x) , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocr₊ (inj₂ (inj₁ y)) = inj₁ (inj₁ (inj₂ y) , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocr₊ (inj₂ (inj₂ z)) = inj₁ (inj₂ z , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ unite⋆l v = inj₁ ((tt , v) , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ uniti⋆l (tt , v) = inj₁ (v , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ swap⋆ (x , y) = inj₁ ((y , x) , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocl⋆ ((x , y) , z) = inj₁ ((x , (y , z)) , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocr⋆ (x , (y , z)) = inj₁ (((x , y) , z) , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ dist (inj₁ (x , z)) = inj₁ ((inj₁ x , z) , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ dist (inj₂ (y , z)) = inj₁ ((inj₂ y , z) , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ factor (inj₁ x , z) = inj₁ (inj₁ (x , z) , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ factor (inj₂ y , z) = inj₁ (inj₂ (y , z) , (↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ id↔ v = inj₁ (v , (↦₂ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ {κ = κ} (c₁ ⨾ c₂) v₃ with evᵣₑᵥ {κ = c₁ ⨾☐• κ} c₂ v₃
... | inj₁ (v₂ , rs) with evᵣₑᵥ {κ = ☐⨾ c₂ • κ} c₁ v₂
... | inj₁ (v₁ , rs') = inj₁ (v₁ , ((↦₁₀ ᵣₑᵥ) ∷ (rs ++↦ᵣₑᵥ ((↦₇ ᵣₑᵥ) ∷ ◾))) ++↦ᵣₑᵥ (rs' ++↦ᵣₑᵥ ((↦₃ ᵣₑᵥ) ∷ ◾)))
... | inj₂ (_ , _ , _ , _ , neq , rs') = inj₂ (_ , _ , _ , _ , neq , (((↦₁₀ ᵣₑᵥ) ∷ (rs ++↦ᵣₑᵥ ((↦₇ ᵣₑᵥ) ∷ ◾))) ++↦ᵣₑᵥ rs'))
evᵣₑᵥ (c₁ ⨾ c₂) v₃ | inj₂ (_ , _ , _ , _ , neq , rs) = inj₂ (_ , _ , _ , _ , neq , (((↦₁₀ ᵣₑᵥ) ∷ ◾) ++↦ᵣₑᵥ rs))
evᵣₑᵥ {κ = κ} (c₁ ⊕ c₂) (inj₁ x) with evᵣₑᵥ {κ = ☐⊕ c₂ • κ} c₁ x
... | inj₁ (x' , rs) = inj₁ (inj₁ x' , (↦₁₁ ᵣₑᵥ) ∷ (rs ++↦ᵣₑᵥ ((↦₄ ᵣₑᵥ) ∷ ◾)))
... | inj₂ (_ , _ , _ , _ , neq , rs) = inj₂ (_ , _ , _ , _ , neq , (↦₁₁ ᵣₑᵥ) ∷ rs)
evᵣₑᵥ {κ = κ} (c₁ ⊕ c₂) (inj₂ y) with evᵣₑᵥ {κ = c₁ ⊕☐• κ} c₂ y
... | inj₁ (y' , rs) = inj₁ (inj₂ y' , (↦₁₂ ᵣₑᵥ) ∷ (rs ++↦ᵣₑᵥ ((↦₅ ᵣₑᵥ) ∷ ◾)))
... | inj₂ (_ , _ , _ , _ , neq , rs) = inj₂ (_ , _ , _ , _ , neq , (↦₁₂ ᵣₑᵥ) ∷ rs)
evᵣₑᵥ {κ = κ} (c₁ ⊗ c₂) (x , y) with evᵣₑᵥ {κ = [ c₁ , x ]⊗☐• κ} c₂ y
... | inj₁ (y' , rs) with evᵣₑᵥ {κ = ☐⊗[ c₂ , y' ]• κ} c₁ x
... | inj₁ (x' , rs') = inj₁ ((x' , y') , (((↦₉ ᵣₑᵥ) ∷ (rs ++↦ᵣₑᵥ ((↦₈ ᵣₑᵥ) ∷ ◾))) ++↦ᵣₑᵥ (rs' ++↦ᵣₑᵥ ((↦₆ ᵣₑᵥ) ∷ ◾))))
... | inj₂ (_ , _ , _ , _ , neq , rs') = inj₂ (_ , _ , _ , _ , neq , (((↦₉ ᵣₑᵥ) ∷ (rs ++↦ᵣₑᵥ ((↦₈ ᵣₑᵥ) ∷ ◾))) ++↦ᵣₑᵥ rs'))
evᵣₑᵥ (c₁ ⊗ c₂) (x , y) | inj₂ (_ , _ , _ , _ , neq , rs) = inj₂ (_ , _ , _ , _ , neq , ((↦₉ ᵣₑᵥ) ∷ rs))
evᵣₑᵥ (ηₓ v) (v' , ↻) with v ≟ v'
... | yes refl = inj₁ (tt , ((↦η ᵣₑᵥ) ∷ ◾))
... | no  neq  = inj₂ (_ , _ , _ , _ , neq , ◾)
evᵣₑᵥ (εₓ v) tt = inj₁ ((v , ↻) , ((↦ε₁ {eq = refl} ᵣₑᵥ) ∷ ◾))

-- Backward evaluator for Pi
evalᵣₑᵥ : ∀ {A B} → (c : A ↔ B) → ⟦ B ⟧ → Maybe ⟦ A ⟧
evalᵣₑᵥ c v = [ just ∘ proj₁ , (λ _ → nothing) ]′ (evᵣₑᵥ {κ = ☐} c v)


text:
{-# OPTIONS --no-termination-check --universe-polymorphism #-}

module PiF where

open import Level
open import Data.Empty
open import Data.Unit
open import Data.Bool
open import Data.Sum hiding (map)
open import Data.Product hiding (map)

open import Relation.Binary.PropositionalEquality hiding (sym; [_])

open import Singleton

infixr 30 _⟷_
infixr 30 _⟺_
infixr 20 _◎_

------------------------------------------------------------------------------
-- A universe of our value types

mutual
  data BF : Set zero where
    ZEROF  : BF
    ONEF   : BF
    PLUSF  : BF → BF → BF
    TIMESF : BF → BF → BF
    RECIP  : BF → BF

--data VF : Set where
--  unitF :

-- data hasType :

-- normalize : (b : BF) → (hasType v b) → normalform v b

-- fractional types are un-interpreted

data Reciprocal (A : Set) : Set where
  rec : (b : A) → ((x : Singleton b) → ⊤) → Reciprocal A

data Recip (A : Set) : Set where
  recip : (a : A) → Recip A

⟦_⟧F : BF → Set zero
⟦ ZEROF ⟧F         = ⊥
⟦ ONEF ⟧F          = ⊤
⟦ PLUSF b1 b2 ⟧F   = ⟦ b1 ⟧F ⊎ ⟦ b2 ⟧F
⟦ TIMESF b1 b2 ⟧F  = ⟦ b1 ⟧F × ⟦ b2 ⟧F
⟦ RECIP b ⟧F  = -- Σ ⟦ b ⟧F (λ v → ((x : Singleton v) → ⊤))
                Reciprocal ⟦ b ⟧F

------------------------------------------------------------------------------
-- Primitive isomorphisms

data _⟷_ : BF → BF → Set where
  -- (+,0) commutative monoid
  unite₊  : { b : BF } → PLUSF ZEROF b ⟷ b
  uniti₊  : { b : BF } → b ⟷ PLUSF ZEROF b
  swap₊   : { b₁ b₂ : BF } → PLUSF b₁ b₂ ⟷ PLUSF b₂ b₁
  assocl₊ : { b₁ b₂ b₃ : BF } → PLUSF b₁ (PLUSF b₂ b₃) ⟷ PLUSF (PLUSF b₁ b₂) b₃
  assocr₊ : { b₁ b₂ b₃ : BF } → PLUSF (PLUSF b₁ b₂) b₃ ⟷ PLUSF b₁ (PLUSF b₂ b₃)
  -- (*,1) commutative monoid
  unite⋆  : { b : BF } → TIMESF ONEF b ⟷ b
  uniti⋆  : { b : BF } → b ⟷ TIMESF ONEF b
  swap⋆   : { b₁ b₂ : BF } → TIMESF b₁ b₂ ⟷ TIMESF b₂ b₁
  assocl⋆ : { b₁ b₂ b₃ : BF } → TIMESF b₁ (TIMESF b₂ b₃) ⟷ TIMESF (TIMESF b₁ b₂) b₃
  assocr⋆ : { b₁ b₂ b₃ : BF } → TIMESF (TIMESF b₁ b₂) b₃ ⟷ TIMESF b₁ (TIMESF b₂ b₃)
  -- * distributes over +
  dist    : { b₁ b₂ b₃ : BF } →
            TIMESF (PLUSF b₁ b₂) b₃ ⟷ PLUSF (TIMESF b₁ b₃) (TIMESF b₂ b₃)
  factor  : { b₁ b₂ b₃ : BF } →
            PLUSF (TIMESF b₁ b₃) (TIMESF b₂ b₃) ⟷ TIMESF (PLUSF b₁ b₂) b₃
  -- id
  id⟷    : { b : BF } → b ⟷ b

adjointP : { b₁ b₂ : BF } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
adjointP unite₊    = uniti₊
adjointP uniti₊    = unite₊
adjointP swap₊     = swap₊
adjointP assocl₊   = assocr₊
adjointP assocr₊   = assocl₊
adjointP unite⋆    = uniti⋆
adjointP uniti⋆    = unite⋆
adjointP swap⋆     = swap⋆
adjointP assocl⋆   = assocr⋆
adjointP assocr⋆   = assocl⋆
adjointP dist      = factor
adjointP factor    = dist
adjointP id⟷      = id⟷

evalP : { b₁ b₂ : BF } → (b₁ ⟷ b₂) → ⟦ b₁ ⟧F → ⟦ b₂ ⟧F
evalP unite₊ (inj₁ ())
evalP unite₊ (inj₂ v) = v
evalP uniti₊ v = inj₂ v
evalP swap₊ (inj₁ v) = inj₂ v
evalP swap₊ (inj₂ v) = inj₁ v
evalP assocl₊ (inj₁ v) = inj₁ (inj₁ v)
evalP assocl₊ (inj₂ (inj₁ v)) = inj₁ (inj₂ v)
evalP assocl₊ (inj₂ (inj₂ v)) = inj₂ v
evalP assocr₊ (inj₁ (inj₁ v)) = inj₁ v
evalP assocr₊ (inj₁ (inj₂ v)) = inj₂ (inj₁ v)
evalP assocr₊ (inj₂ v) = inj₂ (inj₂ v)
evalP unite⋆ (tt , v) = v
evalP uniti⋆ v = (tt , v)
evalP swap⋆ (v₁ , v₂) = (v₂ , v₁)
evalP assocl⋆ (v₁ , (v₂ , v₃)) = ((v₁ , v₂) , v₃)
evalP assocr⋆ ((v₁ , v₂) , v₃) = (v₁ , (v₂ , v₃))
evalP dist (inj₁ v₁ , v₃) = inj₁ (v₁ , v₃)
evalP dist (inj₂ v₂ , v₃) = inj₂ (v₂ , v₃)
evalP factor (inj₁ (v₁ , v₃)) = (inj₁ v₁ , v₃)
evalP factor (inj₂ (v₂ , v₃)) = (inj₂ v₂ , v₃)
evalP id⟷ v = v

-- normalize values in BF to x * 1/y and then decide equality of normalized values

-- _≡B_ {b₁ = ONEF} {b₂ = ONEF} tt tt = true
--_≡B_ {b₁ = TIMESF d c} {b₂ = TIMESF c d} (v₁ , v₃) (v₄ , v₂) =
--  _≡B_ {b₁ = d} {b₂ = d} v₁ v₂ ∧ _≡B_ {b₁ = c} {b₂ = c} v₃ v₄
  -- zero??

-- Backwards evaluator

bevalP : { b₁ b₂ : BF } → (b₁ ⟷ b₂) → ⟦ b₂ ⟧F → ⟦ b₁ ⟧F
bevalP c v = evalP (adjointP c) v

------------------------------------------------------------------------------
-- Closure combinators

data _⟺_ : BF → BF → Set where
  iso    : { b₁ b₂ : BF } → (b₁ ⟷ b₂) → (b₁ ⟺ b₂)
  sym    : { b₁ b₂ : BF } → (b₁ ⟺ b₂) → (b₂ ⟺ b₁)
  _◎_    : { b₁ b₂ b₃ : BF } → (b₁ ⟺ b₂) → (b₂ ⟺ b₃) → (b₁ ⟺ b₃)
  _⊕_    : { b₁ b₂ b₃ b₄ : BF } →
           (b₁ ⟺ b₃) → (b₂ ⟺ b₄) → (PLUSF b₁ b₂ ⟺ PLUSF b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : BF } →
           (b₁ ⟺ b₃) → (b₂ ⟺ b₄) → (TIMESF b₁ b₂ ⟺ TIMESF b₃ b₄)
  refe⋆  : { b : BF } → RECIP (RECIP b) ⟺ b
  refi⋆  : { b : BF } → b ⟺ RECIP (RECIP b)
  rile⋆  : { b : BF } → TIMESF b (TIMESF b (RECIP b)) ⟺ b
  rili⋆  : { b : BF } → b ⟺ TIMESF b (TIMESF b (RECIP b))

--

adjoint : { b₁ b₂ : BF } → (b₁ ⟺ b₂) → (b₂ ⟺ b₁)
adjoint (iso c) = iso (adjointP c)
adjoint (sym c)   = c
adjoint (c₁ ◎ c₂) = adjoint c₂ ◎ adjoint c₁
adjoint (c₁ ⊕ c₂) = adjoint c₁ ⊕ adjoint c₂
adjoint (c₁ ⊗ c₂) = adjoint c₁ ⊗ adjoint c₂
adjoint refe⋆ = refi⋆
adjoint refi⋆ = refe⋆
adjoint rile⋆ = rili⋆
adjoint rili⋆ = rile⋆

--

-- (Context a b c d) represents a combinator (c <-> d) with a hole
-- requiring something of type (a <-> b). When we use these contexts,
-- it is always the case that the (c <-> a) part of the computation
-- has ALREADY been done and that we are about to evaluate (a <-> b)
-- using a given 'a'. The continuation takes the output 'b' and
-- produces a 'd'.

data Context : BF → BF → BF → BF → Set where
  emptyC : {a b : BF} → Context a b a b
  seqC₁ : {a b c i o : BF} → (b ⟺ c) → Context a c i o → Context a b i o
  seqC₂ : {a b c i o : BF} → (a ⟺ b) → Context a c i o → Context b c i o
  leftC : {a b c d i o : BF} →
          (c ⟺ d) → Context (PLUSF a c) (PLUSF b d) i o → Context a b i o
  rightC : {a b c d i o : BF} →
           (a ⟺ b) → Context (PLUSF a c) (PLUSF b d) i o → Context c d i o
  -- the (i <-> a) part of the computation is completely done; so we must store
  -- the value of type [[ c ]] as part of the context
  fstC : {a b c d i o : BF} →
         ⟦ c ⟧F → (c ⟺ d) → Context (TIMESF a c) (TIMESF b d) i o → Context a b i o
  -- the (i <-> c) part of the computation and the (a <-> b) part of
  -- the computation are completely done; so we must store the value
  -- of type [[ b ]] as part of the context
  sndC : {a b c d i o : BF} →
         (a ⟺ b) → ⟦ b ⟧F → Context (TIMESF a c) (TIMESF b d) i o → Context c d i o

-- Evaluation

mutual

  -- The (c <-> a) part of the computation has been done.
  -- We have an 'a' and we are about to do the (a <-> b) computation.
  -- We get a 'b' and examine the context to get the 'd'
  eval_c : { a b c : BF } → (a ⟺ b) → ⟦ a ⟧F → Context a b c c → ⟦ c ⟧F
  eval_c (iso f) v C = eval_k (iso f) (evalP f v) C
  eval_c (sym c) v C = eval_c (adjoint c) v C
  eval_c (f ◎ g) v C = eval_c f v (seqC₁ g C)
  eval_c (f ⊕ g) (inj₁ v) C = eval_c f v (leftC g C)
  eval_c (f ⊕ g) (inj₂ v) C = eval_c g v (rightC f C)
  eval_c (f ⊗ g) (v₁ , v₂) C = eval_c f v₁ (fstC v₂ g C)
  eval_c refe⋆ (rec (rec v _) _)  C = eval_k refe⋆ v C
  eval_c refi⋆ v C = eval_k refi⋆ (rec (rec v (λ x → tt)) ff) C
    where ff = λ x → tt
  eval_c rile⋆ (v₁ , (v₂ , rec v₃ _)) C = eval_k rile⋆ v₁ C
  eval_c rili⋆ v C = eval_k rili⋆ (v , (v , {!!})) C

  -- The (c <-> a) part of the computation has been done.
  -- The (a <-> b) part of the computation has been done.
  -- We need to examine the context to get the 'd'.
  -- We rebuild the combinator on the way out.
  eval_k : { a b c : BF } → (a ⟺ b) → ⟦ b ⟧F → Context a b c c → ⟦ c ⟧F
  eval_k f v emptyC = v
  eval_k f v (seqC₁ g C) = eval_c g v (seqC₂ f C)
  eval_k g v (seqC₂ f C) = eval_k (f ◎ g) v C
  eval_k f v (leftC g C) = eval_k (f ⊕ g) (inj₁ v) C
  eval_k g v (rightC f C) = eval_k (f ⊕ g) (inj₂ v) C
  eval_k f v₁ (fstC v₂ g C) = eval_c g v₂ (sndC f v₁ C)
  eval_k g v₂ (sndC f v₁ C) = eval_k (f ⊗ g) (v₁ , v₂) C

  -- Backwards evaluator

  -- The (d <-> b) part of the computation has been done.
  -- We have a 'b' and we are about to do the (a <-> b) computation backwards.
  -- We get an 'a' and examine the context to get the 'c'
  beval_c : { a b c : BF } → (a ⟺ b) → ⟦ b ⟧F → Context a b c c → ⟦ c ⟧F
  beval_c (iso f) v C = beval_k (iso f) (bevalP f v) C
  beval_c (sym c) v C = beval_c (adjoint c) v C
  beval_c (f ◎ g) v C = beval_c g v (seqC₂ f C)
  beval_c (f ⊕ g) (inj₁ v) C = beval_c f v (leftC g C)
  beval_c (f ⊕ g) (inj₂ v) C = beval_c g v (rightC f C)
  beval_c (f ⊗ g) (v₁ , v₂) C = beval_c g v₂ (sndC f v₁ C)
  beval_c refe⋆ v C = beval_k refe⋆ {!!} C
  beval_c refi⋆ _ C = beval_k refi⋆ {!!} C
  beval_c rile⋆ v C = beval_k rile⋆ (v , (v , {!!})) C
  beval_c rili⋆ (v₁ , (v₂ , _)) C = {!!}

  -- The (d <-> b) part of the computation has been done.
  -- The (a <-> b) backwards computation has been done.
  -- We have an 'a' and examine the context to get the 'c'
  beval_k : { a b c : BF } → (a ⟺ b) → ⟦ a ⟧F → Context a b c c → ⟦ c ⟧F
  beval_k f v emptyC = v
  beval_k g v (seqC₂ f C) = beval_c f v (seqC₁ g C)
  beval_k f v (seqC₁ g C) = beval_k (f ◎ g) v C
  beval_k f v (leftC g C) = beval_k (f ⊕ g) (inj₁ v) C
  beval_k g v (rightC f C) = beval_k (f ⊕ g) (inj₂ v) C
  beval_k g v₂ (sndC f v₁ C) = beval_c f v₁ (fstC v₂ g C)
  beval_k f v₁ (fstC v₂ g C) = beval_k (f ⊗ g) (v₁ , v₂) C

------------------------------------------------------------------------------
-- Top level eval

eval : { a : BF } → (a ⟺ a) → ⟦ a ⟧F → ⟦ a ⟧F
eval f v = eval_c f v emptyC

--

BOOL : BF
BOOL = PLUSF ONEF ONEF

test1 : ⟦ BOOL ⟧F
test1 = eval {BOOL} (iso swap₊) (inj₁ tt)

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
-- Basic intuitionistic contextual modal logic, without ∨ or ⊥.
-- Gentzen-style formalisation of syntax with context pairs, after Nanevski-Pfenning-Pientka.
-- Simple terms.

module BasicICML.Syntax.DyadicGentzen where

open import BasicICML.Syntax.Common public

-- Derivations.

-- NOTE: Only var is an instance constructor, which allows the instance argument for mvar to be automatically inferred, in many cases.

mutual
  infix 3 _⊢_
  data _⊢_ : Cx² Ty Box → Ty → Set where
    instance
      var : ∀ {A Γ Δ}     → A ∈ Γ → Γ ⁏ Δ ⊢ A
    lam   : ∀ {A B Γ Δ}   → Γ , A ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ A ▻ B
    app   : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ A ▻ B → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ B
    mvar  : ∀ {Ψ A Γ Δ}   → [ Ψ ] A ∈ Δ → {{_ : Γ ⁏ Δ ⊢⋆ Ψ}} → Γ ⁏ Δ ⊢ A
    box   : ∀ {Ψ A Γ Δ}   → Ψ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ [ Ψ ] A
    unbox : ∀ {Ψ A C Γ Δ} → Γ ⁏ Δ ⊢ [ Ψ ] A → Γ ⁏ Δ , [ Ψ ] A ⊢ C → Γ ⁏ Δ ⊢ C
    pair  : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ A ∧ B
    fst   : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ A ∧ B → Γ ⁏ Δ ⊢ A
    snd   : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ A ∧ B → Γ ⁏ Δ ⊢ B
    unit  : ∀ {Γ Δ}       → Γ ⁏ Δ ⊢ ⊤

  infix 3 _⊢⋆_
  data _⊢⋆_ : Cx² Ty Box → Cx Ty → Set where
    instance
      ∙   : ∀ {Γ Δ}     → Γ ⁏ Δ ⊢⋆ ∅
      _,_ : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢⋆ Ξ → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢⋆ Ξ , A

-- Monotonicity with respect to context inclusion.

mutual
  mono⊢ : ∀ {A Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢ A → Γ′ ⁏ Δ ⊢ A
  mono⊢ η (var i)         = var (mono∈ η i)
  mono⊢ η (lam t)         = lam (mono⊢ (keep η) t)
  mono⊢ η (app t u)       = app (mono⊢ η t) (mono⊢ η u)
  mono⊢ η (mvar i {{ts}}) = mvar i {{mono⊢⋆ η ts}}
  mono⊢ η (box t)         = box t
  mono⊢ η (unbox t u)     = unbox (mono⊢ η t) (mono⊢ η u)
  mono⊢ η (pair t u)      = pair (mono⊢ η t) (mono⊢ η u)
  mono⊢ η (fst t)         = fst (mono⊢ η t)
  mono⊢ η (snd t)         = snd (mono⊢ η t)
  mono⊢ η unit            = unit

  mono⊢⋆ : ∀ {Ξ Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢⋆ Ξ → Γ′ ⁏ Δ ⊢⋆ Ξ
  mono⊢⋆ η ∙        = ∙
  mono⊢⋆ η (ts , t) = mono⊢⋆ η ts , mono⊢ η t

-- Monotonicity with respect to modal context inclusion.

mutual
  mmono⊢ : ∀ {A Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ′ ⊢ A
  mmono⊢ θ (var i)         = var i
  mmono⊢ θ (lam t)         = lam (mmono⊢ θ t)
  mmono⊢ θ (app t u)       = app (mmono⊢ θ t) (mmono⊢ θ u)
  mmono⊢ θ (mvar i {{ts}}) = mvar (mono∈ θ i) {{mmono⊢⋆ θ ts}}
  mmono⊢ θ (box t)         = box (mmono⊢ θ t)
  mmono⊢ θ (unbox t u)     = unbox (mmono⊢ θ t) (mmono⊢ (keep θ) u)
  mmono⊢ θ (pair t u)      = pair (mmono⊢ θ t) (mmono⊢ θ u)
  mmono⊢ θ (fst t)         = fst (mmono⊢ θ t)
  mmono⊢ θ (snd t)         = snd (mmono⊢ θ t)
  mmono⊢ θ unit            = unit

  mmono⊢⋆ : ∀ {Ξ Δ Δ′ Γ} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢⋆ Ξ → Γ ⁏ Δ′ ⊢⋆ Ξ
  mmono⊢⋆ θ ∙        = ∙
  mmono⊢⋆ θ (ts , t) = mmono⊢⋆ θ ts , mmono⊢ θ t

-- Monotonicity using context pairs.

mono²⊢ : ∀ {A Π Π′} → Π ⊆² Π′ → Π ⊢ A → Π′ ⊢ A
mono²⊢ (η , θ) = mono⊢ η ∘ mmono⊢ θ

-- Shorthand for variables.

v₀ : ∀ {A Γ Δ} → Γ , A ⁏ Δ ⊢ A
v₀ = var i₀

v₁ : ∀ {A B Γ Δ} → Γ , A , B ⁏ Δ ⊢ A
v₁ = var i₁

v₂ : ∀ {A B C Γ Δ} → Γ , A , B , C ⁏ Δ ⊢ A
v₂ = var i₂

mv₀ : ∀ {Ψ A Γ Δ}
      → {{_ : Γ ⁏ Δ , [ Ψ ] A ⊢⋆ Ψ}}
      → Γ ⁏ Δ , [ Ψ ] A ⊢ A
mv₀ = mvar i₀

mv₁ : ∀ {Ψ Ψ′ A B Γ Δ}
      → {{_ : Γ ⁏ Δ , [ Ψ ] A , [ Ψ′ ] B ⊢⋆ Ψ}}
      → Γ ⁏ Δ , [ Ψ ] A , [ Ψ′ ] B ⊢ A
mv₁ = mvar i₁

mv₂ : ∀ {Ψ Ψ′ Ψ″ A B C Γ Δ}
      → {{_ : Γ ⁏ Δ , [ Ψ ] A , [ Ψ′ ] B , [ Ψ″ ] C ⊢⋆ Ψ}}
      → Γ ⁏ Δ , [ Ψ ] A , [ Ψ′ ] B , [ Ψ″ ] C ⊢ A
mv₂ = mvar i₂

-- Generalised reflexivity.

instance
  refl⊢⋆ : ∀ {Γ Ψ Δ} → {{_ : Ψ ⊆ Γ}} → Γ ⁏ Δ ⊢⋆ Ψ
  refl⊢⋆ {∅}     {{done}}   = ∙
  refl⊢⋆ {Γ , A} {{skip η}} = mono⊢⋆ weak⊆ (refl⊢⋆ {{η}})
  refl⊢⋆ {Γ , A} {{keep η}} = mono⊢⋆ weak⊆ (refl⊢⋆ {{η}}) , v₀

-- Deduction theorem is built-in.

-- Modal deduction theorem.

mlam : ∀ {Ψ A B Γ Δ}
      → Γ ⁏ Δ , [ Ψ ] A ⊢ B
      → Γ ⁏ Δ ⊢ [ Ψ ] A ▻ B
mlam t = lam (unbox v₀ (mono⊢ weak⊆ t))

-- Detachment theorems.

det : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ▻ B → Γ , A ⁏ Δ ⊢ B
det t = app (mono⊢ weak⊆ t) v₀

mdet : ∀ {Ψ A B Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ] A ▻ B
      → Γ ⁏ Δ , [ Ψ ] A ⊢ B
mdet t = app (mmono⊢ weak⊆ t) (box mv₀)

-- Cut and multicut.

cut : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A → Γ , A ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ B
cut t u = app (lam u) t

mcut : ∀ {Ψ A B Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ] A
      → Γ ⁏ Δ , [ Ψ ] A ⊢ B
      → Γ ⁏ Δ ⊢ B
mcut t u = app (mlam u) t

multicut : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢⋆ Ξ → Ξ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ A
multicut ∙        u = mono⊢ bot⊆ u
multicut (ts , t) u = app (multicut ts (lam u)) t

-- Contraction.

ccont : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = lam (lam (app (app v₁ v₀) v₀))

cont : ∀ {A B Γ Δ} → Γ , A , A ⁏ Δ ⊢ B → Γ , A ⁏ Δ ⊢ B
cont t = det (app ccont (lam (lam t)))

mcont : ∀ {Ψ A B Γ Δ} → Γ ⁏ Δ , [ Ψ ] A , [ Ψ ] A ⊢ B → Γ ⁏ Δ , [ Ψ ] A ⊢ B
mcont t = mdet (app ccont (mlam (mlam t)))

-- Exchange, or Schönfinkel’s C combinator.

cexch : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = lam (lam (lam (app (app v₂ v₀) v₁)))

exch : ∀ {A B C Γ Δ} → Γ , A , B ⁏ Δ ⊢ C → Γ , B , A ⁏ Δ ⊢ C
exch t = det (det (app cexch (lam (lam t))))

mexch : ∀ {Ψ Ψ′ A B C Γ Δ}
      → Γ ⁏ Δ , [ Ψ ] A , [ Ψ′ ] B ⊢ C
      → Γ ⁏ Δ , [ Ψ′ ] B , [ Ψ ] A ⊢ C
mexch t = mdet (mdet (app cexch (mlam (mlam t))))

-- Composition, or Schönfinkel’s B combinator.

ccomp : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = lam (lam (lam (app v₂ (app v₁ v₀))))

comp : ∀ {A B C Γ Δ} → Γ , B ⁏ Δ ⊢ C → Γ , A ⁏ Δ ⊢ B → Γ , A ⁏ Δ ⊢ C
comp t u = det (app (app ccomp (lam t)) (lam u))

mcomp : ∀ {Ψ Ψ′ Ψ″ A B C Γ Δ}
      → Γ ⁏ Δ , [ Ψ′ ] B ⊢ [ Ψ″ ] C
      → Γ ⁏ Δ , [ Ψ ] A ⊢ [ Ψ′ ] B
      → Γ ⁏ Δ , [ Ψ ] A ⊢ [ Ψ″ ] C
mcomp t u = mdet (app (app ccomp (mlam t)) (mlam u))

-- Useful theorems in functional form.

dist : ∀ {Ψ A B Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ] (A ▻ B)
      → Γ ⁏ Δ ⊢ [ Ψ ] A
      → Γ ⁏ Δ ⊢ [ Ψ ] B
dist t u = unbox t (unbox (mmono⊢ weak⊆ u) (box (app mv₁ mv₀)))

up : ∀ {Ψ A Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ] A
      → Γ ⁏ Δ ⊢ [ Ψ ] [ Ψ ] A
up t = unbox t (box (box mv₀))

down : ∀ {Ψ A Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ] A
      → {{_ : Γ ⁏ Δ , [ Ψ ] A ⊢⋆ Ψ}}
      → Γ ⁏ Δ ⊢ A
down t = unbox t mv₀

distup : ∀ {Ψ A B Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ] ([ Ψ ] A ▻ B)
      → Γ ⁏ Δ ⊢ [ Ψ ] A
      → Γ ⁏ Δ ⊢ [ Ψ ] B
distup t u = dist t (up u)

-- Useful theorems in combinatory form.

ci : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A ▻ A
ci = lam v₀

ck : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ▻ B ▻ A
ck = lam (lam v₁)

cs : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
cs = lam (lam (lam (app (app v₂ v₀) (app v₁ v₀))))

cdist : ∀ {Ψ A B Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ] (A ▻ B) ▻
                  [ Ψ ] A ▻
                  [ Ψ ] B
cdist = lam (lam (dist v₁ v₀))

cup : ∀ {Ψ A Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ] A ▻
                  [ Ψ ] [ Ψ ] A
cup = lam (up v₀)

cdistup : ∀ {Ψ A B Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ] ([ Ψ ] A ▻ B) ▻
                  [ Ψ ] A ▻ [ Ψ ] B
cdistup = lam (lam (dist v₁ (up v₀)))

cunbox : ∀ {Ψ A C Γ Δ}
      → Γ ⁏ Δ ⊢ [ Ψ ] A ▻
                  ([ Ψ ] A ▻ C) ▻
                  C
cunbox = lam (lam (app v₀ v₁))

cpair : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ▻ B ▻ A ∧ B
cpair = lam (lam (pair v₁ v₀))

cfst : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ∧ B ▻ A
cfst = lam (fst v₀)

csnd : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ∧ B ▻ B
csnd = lam (snd v₀)

-- Closure under context concatenation.

concat : ∀ {A B Γ} Γ′ {Δ} → Γ , A ⁏ Δ ⊢ B → Γ′ ⁏ Δ ⊢ A → Γ ⧺ Γ′ ⁏ Δ ⊢ B
concat Γ′ t u = app (mono⊢ (weak⊆⧺₁ Γ′) (lam t)) (mono⊢ weak⊆⧺₂ u)

mconcat : ∀ {Ψ A B Γ Δ} Δ′ → Γ ⁏ Δ , [ Ψ ] A ⊢ B → Γ ⁏ Δ′ ⊢ [ Ψ ] A → Γ ⁏ Δ ⧺ Δ′ ⊢ B
mconcat Δ′ t u = app (mmono⊢ (weak⊆⧺₁ Δ′) (mlam t)) (mmono⊢ weak⊆⧺₂ u)

-- Substitution.

mutual
  [_≔_]_ : ∀ {A C Γ Δ} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ C → Γ ∖ i ⁏ Δ ⊢ C
  [ i ≔ s ] var j         with i ≟∈ j
  [ i ≔ s ] var .i        | same   = s
  [ i ≔ s ] var ._        | diff j = var j
  [ i ≔ s ] lam t         = lam ([ pop i ≔ mono⊢ weak⊆ s ] t)
  [ i ≔ s ] app t u       = app ([ i ≔ s ] t) ([ i ≔ s ] u)
  [ i ≔ s ] mvar j {{ts}} = mvar j {{[ i ≔ s ]⋆ ts}}
  [ i ≔ s ] box t         = box t
  [ i ≔ s ] unbox t u     = unbox ([ i ≔ s ] t) ([ i ≔ mmono⊢ weak⊆ s ] u)
  [ i ≔ s ] pair t u      = pair ([ i ≔ s ] t) ([ i ≔ s ] u)
  [ i ≔ s ] fst t         = fst ([ i ≔ s ] t)
  [ i ≔ s ] snd t         = snd ([ i ≔ s ] t)
  [ i ≔ s ] unit          = unit

  [_≔_]⋆_ : ∀ {Ξ A Γ Δ} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢⋆ Ξ → Γ ∖ i ⁏ Δ ⊢⋆ Ξ
  [_≔_]⋆_ i s ∙        = ∙
  [_≔_]⋆_ i s (ts , t) = [ i ≔ s ]⋆ ts , [ i ≔ s ] t

-- Modal substitution.

mutual
  m[_≔_]_ : ∀ {Ψ A C Γ Δ} → (i : [ Ψ ] A ∈ Δ) → Ψ ⁏ Δ ∖ i ⊢ A → Γ ⁏ Δ ⊢ C → Γ ⁏ Δ ∖ i ⊢ C
  m[ i ≔ s ] var j          = var j
  m[ i ≔ s ] lam t          = lam (m[ i ≔ s ] t)
  m[ i ≔ s ] app t u        = app (m[ i ≔ s ] t) (m[ i ≔ s ] u)
  m[ i ≔ s ] mvar j  {{ts}} with i ≟∈ j
  m[ i ≔ s ] mvar .i {{ts}} | same   = multicut (m[ i ≔ s ]⋆ ts) s
  m[ i ≔ s ] mvar ._ {{ts}} | diff j = mvar j {{m[ i ≔ s ]⋆ ts}}
  m[ i ≔ s ] box t          = box (m[ i ≔ s ] t)
  m[ i ≔ s ] unbox t u      = unbox (m[ i ≔ s ] t) (m[ pop i ≔ mmono⊢ weak⊆ s ] u)
  m[ i ≔ s ] pair t u       = pair (m[ i ≔ s ] t) (m[ i ≔ s ] u)
  m[ i ≔ s ] fst t          = fst (m[ i ≔ s ] t)
  m[ i ≔ s ] snd t          = snd (m[ i ≔ s ] t)
  m[ i ≔ s ] unit           = unit

  m[_≔_]⋆_ : ∀ {Ξ Ψ A Γ Δ} → (i : [ Ψ ] A ∈ Δ) → Ψ ⁏ Δ ∖ i ⊢ A → Γ ⁏ Δ ⊢⋆ Ξ → Γ ⁏ Δ ∖ i ⊢⋆ Ξ
  m[_≔_]⋆_ i s ∙        = ∙
  m[_≔_]⋆_ i s (ts , t) = m[ i ≔ s ]⋆ ts , m[ i ≔ s ] t

-- Convertibility.

data _⋙_ {Δ : Cx Box} {Γ : Cx Ty} : ∀ {A} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ A → Set where
  refl⋙      : ∀ {A} → {t : Γ ⁏ Δ ⊢ A}
                      → t ⋙ t

  trans⋙     : ∀ {A} → {t t′ t″ : Γ ⁏ Δ ⊢ A}
                      → t ⋙ t′ → t′ ⋙ t″
                      → t ⋙ t″

  sym⋙       : ∀ {A} → {t t′ : Γ ⁏ Δ ⊢ A}
                      → t ⋙ t′
                      → t′ ⋙ t

  conglam⋙   : ∀ {A B} → {t t′ : Γ , A ⁏ Δ ⊢ B}
                        → t ⋙ t′
                        → lam t ⋙ lam t′

  congapp⋙   : ∀ {A B} → {t t′ : Γ ⁏ Δ ⊢ A ▻ B} → {u u′ : Γ ⁏ Δ ⊢ A}
                        → t ⋙ t′ → u ⋙ u′
                        → app t u ⋙ app t′ u′

  -- NOTE: Rejected by Pfenning and Davies.
  -- congbox⋙   : ∀ {Ψ A} → {t t′ : Ψ ⁏ Δ ⊢ A}
  --                       → t ⋙ t′
  --                       → box t ⋙ box t′

  congunbox⋙ : ∀ {Ψ A C} → {t t′ : Γ ⁏ Δ ⊢ [ Ψ ] A} → {u u′ : Γ ⁏ Δ , [ Ψ ] A ⊢ C}
                          → t ⋙ t′ → u ⋙ u′
                          → unbox t u ⋙ unbox t′ u′

  congpair⋙  : ∀ {A B} → {t t′ : Γ ⁏ Δ ⊢ A} → {u u′ : Γ ⁏ Δ ⊢ B}
                        → t ⋙ t′ → u ⋙ u′
                        → pair t u ⋙ pair t′ u′

  congfst⋙   : ∀ {A B} → {t t′ : Γ ⁏ Δ ⊢ A ∧ B}
                        → t ⋙ t′
                        → fst t ⋙ fst t′

  congsnd⋙   : ∀ {A B} → {t t′ : Γ ⁏ Δ ⊢ A ∧ B}
                        → t ⋙ t′
                        → snd t ⋙ snd t′

  beta▻⋙     : ∀ {A B} → {t : Γ , A ⁏ Δ ⊢ B} → {u : Γ ⁏ Δ ⊢ A}
                        → app (lam t) u ⋙ ([ top ≔ u ] t)

  eta▻⋙      : ∀ {A B} → {t : Γ ⁏ Δ ⊢ A ▻ B}
                        → t ⋙ lam (app (mono⊢ weak⊆ t) v₀)

  beta□⋙     : ∀ {Ψ A C} → {t : Ψ ⁏ Δ ⊢ A} → {u : Γ ⁏ Δ , [ Ψ ] A ⊢ C}
                          → unbox (box t) u ⋙ (m[ top ≔ t ] u)

  eta□⋙      : ∀ {Ψ A} → {t : Γ ⁏ Δ ⊢ [ Ψ ] A}
                        → t ⋙ unbox t (box mv₀)

  -- TODO: What about commuting conversions for □?

  beta∧₁⋙    : ∀ {A B} → {t : Γ ⁏ Δ ⊢ A} → {u : Γ ⁏ Δ ⊢ B}
                        → fst (pair t u) ⋙ t

  beta∧₂⋙    : ∀ {A B} → {t : Γ ⁏ Δ ⊢ A} → {u : Γ ⁏ Δ ⊢ B}
                        → snd (pair t u) ⋙ u

  eta∧⋙      : ∀ {A B} → {t : Γ ⁏ Δ ⊢ A ∧ B}
                        → t ⋙ pair (fst t) (snd t)

  eta⊤⋙     : ∀ {t : Γ ⁏ Δ ⊢ ⊤} → t ⋙ unit

-- Examples from the Nanevski-Pfenning-Pientka paper.

-- NOTE: In many cases, the instance argument for mvar can be automatically inferred, but not always.

module Examples where
  e₁ : ∀ {A C D Γ Δ}
        → Γ ⁏ Δ ⊢ [ ∅ , C ] A ▻
                    [ ∅ , C , D ] A
  e₁ = lam (unbox v₀ (box mv₀))

  e₂ : ∀ {A C Γ Δ}
        → Γ ⁏ Δ ⊢ [ ∅ , C , C ] A ▻
                    [ ∅ , C ] A
  e₂ = lam (unbox v₀ (box mv₀))

  e₃ : ∀ {A Γ Δ}
        → Γ ⁏ Δ ⊢ [ ∅ , A ] A
  e₃ = box v₀

  e₄ : ∀ {A B C Γ Δ}
        → Γ ⁏ Δ ⊢ [ ∅ , A ] B ▻
                    [ ∅ , A ] [ ∅ , B ] C ▻
                    [ ∅ , A ] C
  e₄ = lam (lam (unbox v₁ (unbox v₀ (box
         (unbox mv₀ (mv₀ {{∙ , mv₂}}))))))

  e₅ : ∀ {A Γ Δ}
        → Γ ⁏ Δ ⊢ [ ∅ ] A ▻ A
  e₅ = lam (unbox v₀ mv₀)

  e₆ : ∀ {A C D Γ Δ}
        → Γ ⁏ Δ ⊢ [ ∅ , C ] A ▻
                    [ ∅ , D ] [ ∅ , C ] A
  e₆ = lam (unbox v₀ (box (box mv₀)))

  e₇ : ∀ {A B C D Γ Δ}
        → Γ ⁏ Δ ⊢ [ ∅ , C ] (A ▻ B) ▻
                    [ ∅ , D ] A ▻
                    [ ∅ , C , D ] B
  e₇ = lam (lam (unbox v₁ (unbox v₀ (box
         (app mv₁ mv₀)))))

  e₈ : ∀ {A B C Γ Δ}
        → Γ ⁏ Δ ⊢ [ ∅ , A ] (A ▻ B) ▻
                    [ ∅ , B ] C ▻
                    [ ∅ , A ] C
  e₈ = lam (lam (unbox v₁ (unbox v₀ (box
         (mv₀ {{∙ , app mv₁ v₀}})))))

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-# OPTIONS --without-K #-}
module AC {a b c} {A : Set a} {B : A → Set b} {C : (x : A) → B x → Set c} where

open import Equivalence
open import FunExt
open import Types

left : Set _
left = (x : A) → Σ (B x) λ y → C x y

right : Set _
right = Σ ((x : A) → B x) λ f → (x : A) → C x (f x)

to : left → right
to f = π₁ ∘ f , π₂ ∘ f

from : right → left
from f x = π₁ f x , π₂ f x

AC∞ : right ≃ left
AC∞
  = from
  , (to , λ _ → refl)
  , (to , λ _ → refl)


text:
module Oscar.Data.Vec.Properties where

open import Oscar.Data.Vec
open import Data.Vec.Properties public

open import Data.Nat
open import Data.Product renaming (map to mapP)
open import Relation.Binary.PropositionalEquality
open import Data.Fin

map-∈ : ∀ {a b} {A : Set a} {B : Set b} {y : B} {f : A → B} {n} {xs : Vec A n} → y ∈ map f xs → ∃ λ x → f x ≡ y
map-∈ {xs = []} ()
map-∈ {xs = x ∷ xs} here = x , refl
map-∈ {xs = x ∷ xs} (there y∈mapfxs) = map-∈ y∈mapfxs

∈-map₂ : ∀ {a b} {A : Set a} {B : Set b} {m n : ℕ}
             → ∀ {c} {F : Set c} (f : A → B → F)
             {xs : Vec A m} {ys : Vec B n}
             {x y} → x ∈ xs → y ∈ ys → (f x y) ∈ map₂ f xs ys
∈-map₂ f {xs = x ∷ xs} {ys} here         y∈ys =
  ∈-++ₗ (∈-map (f x) y∈ys)
∈-map₂ f {xs = x ∷ xs} {ys} (there x∈xs) y∈ys =
  ∈-++ᵣ (map (f x) ys) (∈-map₂ f x∈xs y∈ys)

lookup-delete-thin : ∀ {a n} {A : Set a} (x : Fin (suc n)) (y : Fin n) (v : Vec A (suc n)) →
                     lookup y (delete x v) ≡ lookup (thin x y) v
lookup-delete-thin zero zero (_ ∷ _) = refl
lookup-delete-thin zero (suc _) (_ ∷ _) = refl
lookup-delete-thin (suc _) zero (_ ∷ _) = refl
lookup-delete-thin (suc x) (suc y) (_ ∷ v) = lookup-delete-thin x y v


text:
{-# OPTIONS --copatterns #-}

module IOExampleGraphicsDrawingProgram where

open import Data.Bool.Base
open import Data.Char.Base renaming (primCharEquality to charEquality)
open import Data.Nat.Base hiding (_≟_;_⊓_; _+_; _*_)
open import Data.List.Base hiding (_++_)
open import Data.Integer.Base hiding (suc)
open import Data.String.Base
open import Data.Maybe.Base

open import Function

open import SizedIO.Base
open import SizedIO.IOGraphicsLib

open import NativeInt --PrimTypeHelpers
open import NativeIO

integerLess     :  ℤ →  ℤ → Bool
integerLess x y with ∣(y - (x ⊓ y))∣
... | zero = true
... | z = false

line : Point → Point → Graphic
line p  newpoint = withColor red (polygon
                       (nativePoint x y
                        ∷ nativePoint a b
                        ∷ nativePoint (a + xAddition) (b + yAddition)
                        ∷ nativePoint (x + xAddition) (y + yAddition)
                        ∷ [] ) )
  where
  x = nativeProj1Point p
  y = nativeProj2Point p
  a = nativeProj1Point newpoint
  b = nativeProj2Point newpoint

  diffx = + ∣ (a - x) ∣
  diffy = + ∣ (b - y) ∣

  diffx*3 = diffx * (+ 3)
  diffy*3 = diffy * (+ 3)

  condition = (integerLess diffx diffy*3) ∧ (integerLess diffy diffx*3)

  xAddition = if condition then + 2 else + 1
  yAddition = if condition then + 2 else + 1

State = Maybe Point

loop                 :  ∀{i} → Window → State → IOGraphics i Unit
force (loop w s)     =  exec'  (getWindowEvent w)
  λ{  (Key c t)      →  if charEquality c 'x' then (exec (closeWindow w) return)
                                              else loop w s
   ;  (MouseMove p₂) →  case s of
      λ{ nothing     →  loop w (just p₂)
       ; (just p₁)   →  exec (drawInWindow w (line p₁ p₂)) λ _ →
                        loop w (just p₂)
       }
   ; _               →  loop w  s
   }

{-
loop                 :  ∀{i} → Window → State → IOGraphics i Unit
force (loop w s)     =  exec'  (getWindowEvent w)
  λ{  (Key c t)      →  if charEquality c 'x' then return _ else loop w s
   ;  (MouseMove p₂) →  case s of
      λ{ nothing     →  loop w (just p₂)
       ; (just p₁)   →  exec (drawInWindow w (line p₁ p₂)) λ _ →
                        loop w (just p₂)
       }
   ; _               →  loop w  s
   }
-}

{-
mutual
  loop                 :  ∀{i} → Window → State → IOGraphics i Unit
  force (loop w s)     =  exec'  (getWindowEvent w)  (λ e → aux w e s)

  aux                  :  ∀{i} → Window → Event → State → IOGraphics i Unit
  aux w (Key c t) s              = if charEquality c 'x' then (exec (closeWindow w) λ _ → return _)
                                   else loop w s
  aux w (MouseMove p₂) (just p₁) = exec (drawInWindow w (line p₁ p₂)) (λ _ →
                                   loop w (just p₂))
  aux w (MouseMove p₂) nothing   = loop w (just p₂)
  aux w _  s                     = loop w s
-}

{-
tailrecursion discussion

mutual
  loop                 :  ∀{i} → Window → State → IOGraphics i Unit
  command (force (loop w s))     =  (getWindowEvent w)
  response (force (loop w s)) e    = aux w e s

  aux                  :  ∀{i} → Window → Event → State → IOGraphics i Unit
  command (aux w (MouseMove p₂) (just p₁)) = (drawInWindow w (line p₁ p₂))
  response (aux w (MouseMove p₂) (just p₁)) _ = loop w (just p₂))
  aux w (MouseMove p₂) nothing   = loop w (just p₂)
  aux w _  s                     = loop w s

-}

{-
  λ{  (Key c t)      →  if charEquality c 'x' then
                          (exec ? λ _ → return _) else loop w s
   ;  (MouseMove p₂) →  case s of
      λ{ nothing     →  loop w (just p₂)
       ; (just p₁)   →  exec (drawInWindow w (line p₁ p₂)) λ _ →
                        loop w (just p₂)
       }
   ; _               →  loop w  s
   }
-}

myProgram : ∀{i} → IOGraphics i Unit
myProgram =
  exec (openWindow "Drawing Program" nothing
       1000 1000 nativeDrawGraphic nothing) λ window →
  loop window nothing

main : NativeIO Unit
main = nativeRunGraphics (translateIOGraphics myProgram)

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda