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

open import Prelude
open import Relation.Binary

module Data.AVLTree.Internal {k} {K : Type k} {r₁ r₂} (totalOrder : TotalOrder K r₁ r₂) where

open import Relation.Binary.Construct.Bounded totalOrder
open import Data.Nat using (_+_)
open TotalOrder totalOrder using (_<?_; compare)
open TotalOrder b-ord using (<-trans) renaming (refl to <-refl)
import Data.Empty.UniversePolymorphic as Poly

private
  variable
    n m l : ℕ

data Bal : ℕ → ℕ → ℕ → Type where
  ll : Bal (suc n) n (suc n)
  ee : Bal n n n
  rr : Bal n (suc n) (suc n)

balr : Bal n m l → Bal l n l
balr ll = ee
balr ee = ee
balr rr = ll

ball : Bal n m l → Bal m l l
ball ll = rr
ball ee = ee
ball rr = ee

private
  variable
    v : Level
    Val : K → Type v

data Tree {v} (Val : K → Type v) (lb ub : [∙]) : ℕ → Type (k ℓ⊔ r₁ ℓ⊔ v) where
  leaf : (lb<ub : lb [<] ub) →
         Tree Val lb ub zero
  node : (key : K)
         (val : Val key)
         (bal : Bal n m l)
         (lchild : Tree Val lb [ key ] n)
         (rchild : Tree Val [ key ] ub m) →
         Tree Val lb ub (suc l)

private
  variable
    lb ub : [∙]

data Inc {t} (T : ℕ → Type t) (n : ℕ) : Type t where
  stay : T n       → Inc T n
  high : T (suc n) → Inc T n

private
  variable
    t : Level
    N : ℕ → Type t

rotʳ : (x : K) →
       (xv : Val x) →
       (ls : Tree Val lb [ x ] (2 + n)) →
       (rs : Tree Val [ x ] ub n) →
       Inc (Tree Val lb ub) (2 + n)
rotʳ y yv (node x xv ll xl xr) zs = stay (node x xv ee xl (node y yv ee xr zs))
rotʳ y yv (node x xv ee xl xr) zs = high (node x xv rr xl (node y yv ll xr zs))
rotʳ z zv (node x xv rr xl (node y yv bl yl yr)) zr = stay (node y yv ee (node x xv (balr bl) xl yl) (node z zv (ball bl) yr zr))

rotˡ : (x : K) → (xv : Val x) →
       (ls : Tree Val lb [ x ] n) →
       (rs : Tree Val [ x ] ub (2 + n)) →
       Inc (Tree Val lb ub) (2 + n)
rotˡ x xv xl (node y yv ee yl yr) = high (node y yv ll (node x xv rr xl yl) yr)
rotˡ x xv xl (node y yv rr yl yr) = stay (node y yv ee (node x xv ee xl yl) yr)
rotˡ x xv xl (node z zv ll (node y yv bl yl yr) zr) = stay (node y yv ee (node x xv (balr bl) xl yl) (node z zv (ball bl) yr zr))

insertWith : (x : K) → Val x →
             ((new : Val x) → (old : Val x) → Val x) →
             (lb [<] [ x ]) →
             ([ x ] [<] ub) →
             (tr : Tree Val lb ub n) →
             Inc (Tree Val lb ub) n
insertWith x xv xf lb<x x<ub (leaf lb<ub) =
  high (node x xv ee (leaf lb<x) (leaf x<ub))
insertWith x xv xf lb<x x<ub (node y yv bal ls rs) with compare x y
... | lt x<y with insertWith x xv xf lb<x x<y ls
... | stay ls′ = stay (node y yv bal ls′ rs)
... | high ls′ with bal
... | ll = rotʳ y yv ls′ rs
... | ee = high (node y yv ll ls′ rs)
... | rr = stay (node y yv ee ls′ rs)
insertWith x xv xf lb<x x<ub (node y yv bal ls rs)
    | gt y<x with insertWith x xv xf y<x x<ub rs
... | stay rs′ = stay (node y yv bal ls rs′)
... | high rs′ with bal
... | ll = stay (node y yv ee ls rs′)
... | ee = high (node y yv rr ls rs′)
... | rr = rotˡ y yv ls rs′
insertWith x xv xf lb<x x<ub (node y yv bal ls rs)
    | eq x≡y = stay (node y (subst _ x≡y (xf xv (subst _ (sym x≡y) yv))) bal ls rs)

lookup : (x : K) → Tree  Val lb ub n → Maybe (Val x)
lookup x (leaf lb<ub) = nothing
lookup x (node y val bal lhs rhs) with compare y x
... | lt x<y = lookup x lhs
... | eq x≡y = just (subst _ x≡y val)
... | gt x>y = lookup x rhs

record Cons (Val : K → Type v) (lb ub : [∙]) (h : ℕ) : Type (k ℓ⊔ v ℓ⊔ r₁) where
  constructor cons
  field
    head : K
    val  : Val head
    bounds : lb [<] [ head ]
    tail : Inc (Tree Val [ head ] ub) h
open Cons public

map-tail : ∀ {ub₁ ub₂} →
             Cons Val lb ub₁ n →
             (∀ {lb} → Inc (Tree Val lb ub₁) n → Inc (Tree Val lb ub₂) m) →
             Cons Val lb ub₂ m
map-tail (cons h v b t) f = cons h v b (f t)

uncons : (x : K) →
         Val x →
         Bal n m l →
         Tree Val lb [ x ] n →
         Tree Val [ x ] ub m →
         Cons Val lb ub l
uncons x xv bl (leaf lb<ub) rhs .head = x
uncons x xv bl (leaf lb<ub) rhs .val = xv
uncons x xv bl (leaf lb<ub) rhs .bounds = lb<ub
uncons x xv ee (leaf lb<ub) rhs .tail = stay rhs
uncons x xv rr (leaf lb<ub) rhs .tail = stay rhs
uncons x xv bl (node y yv yb ls yrs) rs =
  map-tail (uncons y yv yb ls yrs)
    λ { (high ys) → high (node x xv bl ys rs)
      ; (stay ys) → case bl of
        λ { ll → stay (node x xv ee ys rs)
          ; ee → high (node x xv rr ys rs)
          ; rr → rotˡ x xv ys rs
          }
      }

ext : ∀ {ub′} → ub [<] ub′ → Tree Val lb ub n → Tree Val lb ub′ n
ext {lb = lb} ub<ub′ (leaf lb<ub) = leaf (<-trans {x = lb} lb<ub ub<ub′)
ext ub<ub′ (node x xv bal lhs rhs) = node x xv bal lhs (ext ub<ub′ rhs)

join : ∀ {x} →
       Tree Val lb [ x ] m →
       Bal m n l →
       Tree Val [ x ] ub n →
       Inc (Tree Val lb ub) l
join lhs ll (leaf lb<ub) = stay (ext lb<ub lhs)
join {lb = lb} (leaf lb<ub₁) ee (leaf lb<ub) = stay (leaf (<-trans {x = lb} lb<ub₁ lb<ub))
join lhs bl (node x xv xb xl xr) with uncons x xv xb xl xr
... | cons k′ v′ l<u (high tr′) = high (node k′ v′ bl (ext l<u lhs) tr′)
... | cons k′ v′ l<u (stay tr′) with bl
... | ll = rotʳ k′ v′ (ext l<u lhs) tr′
... | ee = high (node k′ v′ ll (ext l<u lhs) tr′)
... | rr = stay (node k′ v′ ee (ext l<u lhs) tr′)

data Decr {t} (T : ℕ → Type t) : ℕ → Type t where
  same : T n → Decr T n
  decr : T n → Decr T (suc n)

inc→dec : Inc N n → Decr N (suc n)
inc→dec (stay x) = decr x
inc→dec (high x) = same x

delete : (x : K)
        → Tree Val lb ub n
        → Decr (Tree Val lb ub) n
delete x (leaf l<u) = same (leaf l<u)
delete x (node y yv b l r) with compare x y
delete x (node y yv b l r) | eq _ = inc→dec (join l b r)
delete x (node y yv b l r) | lt a with delete x l
... | same l′ = same (node y yv b l′ r)
... | decr l′ with b
... | ll = decr (node y yv ee l′ r)
... | ee = same (node y yv rr l′ r)
... | rr = inc→dec (rotˡ y yv l′ r)
delete x (node y yv b l r) | gt c with delete x r
... | same r′ = same (node y yv b l r′)
... | decr r′ with b
... | ll = inc→dec (rotʳ y yv l r′)
... | ee =  same (node y yv ll  l r′)
... | rr =  decr (node y yv ee  l r′)

data Change {t} (T : ℕ → Type t) : ℕ → Type t where
  up : T (suc n) → Change T n
  ev : T n → Change T n
  dn : T n → Change T (suc n)

inc→changeup : Inc N n → Change N (suc n)
inc→changeup (stay x) = dn x
inc→changeup (high x) = ev x

inc→changedn : Inc N n → Change N n
inc→changedn (stay x) = ev x
inc→changedn (high x) = up x

_<_<_ : [∙] → K → [∙] → Type _
l < x < u = l [<] [ x ] × [ x ] [<] u

alter : (x : K)
      → (Maybe (Val x) → Maybe (Val x))
      → Tree Val lb ub n
      → lb < x < ub
      → Change (Tree Val lb ub) n
alter x f (leaf l<u) (l , u) with f nothing
...  | just xv = up (node x xv ee (leaf l) (leaf u))
...  | nothing = ev (leaf l<u)
alter x f (node y yv b tl tr) (l , u) with compare x y
alter x f (node y yv b tl tr) (l , u)
     | eq x≡y with f (just (subst _ (sym x≡y) yv))
...  | just xv = ev (node y (subst _ x≡y xv) b tl tr)
...  | nothing = inc→changeup (join tl b tr)
alter x f (node y yv b tl tr) (l , u)
      | lt a with alter x f tl (l , a) | b
...  | ev tl′ | _  = ev (node y yv b  tl′ tr)
...  | up tl′ | ll = inc→changedn (rotʳ y yv tl′ tr)
...  | up tl′ | ee = up (node y yv ll  tl′ tr)
...  | up tl′ | rr = ev (node y yv ee  tl′ tr)
...  | dn tl′ | ll = dn (node y yv ee  tl′ tr)
...  | dn tl′ | ee = ev (node y yv rr  tl′ tr)
...  | dn tl′ | rr = inc→changeup (rotˡ y yv tl′ tr)
alter x f (node y yv b tl tr) (l , u)
     | gt c with alter x f tr (c , u) | b
...  | ev tr′ | _  = ev (node y yv b  tl tr′)
...  | up tr′ | ll = ev (node y yv ee tl tr′)
...  | up tr′ | ee = up (node y yv rr  tl tr′)
...  | up tr′ | rr = inc→changedn (rotˡ y yv tl tr′)
...  | dn tr′ | ll = inc→changeup (rotʳ y yv tl tr′)
...  | dn tr′ | ee = ev (node y yv ll  tl tr′)
...  | dn tr′ | rr = dn (node y yv ee  tl tr′)

open import Lens

alterF : (x : K) →
         Tree Val lb ub n →
         lb < x < ub →
         LensPart (Change (Tree Val lb ub) n) (Maybe (Val x))
alterF x xs bnds = go (ev xs) x xs bnds id
  where
  go : A → (x : K) →
       Tree Val lb ub n →
       lb < x < ub →
       (Change (Tree Val lb ub) n → A) →
       LensPart A (Maybe (Val x))
  go xs x (leaf lb<ub) (l , u) k = λ where
    .get → nothing
    .set nothing → xs
    .set (just xv) → k (up (node x xv ee (leaf l) (leaf u)))
  go xs x (node y yv bl yl yr) (l , u) k with compare x y
  go xs x (node y yv bl yl yr) (l , u) k | eq x≡y = λ where
    .get → just (subst _ (sym x≡y) yv)
    .set nothing → k (inc→changeup (join yl bl yr))
    .set (just xv) → k (ev (node y (subst _ x≡y xv) bl yl yr))
  go xs x (node y yv bl yl yr) (l , u) k | lt x<y =
    go xs x yl (l , x<y)
      λ { (up yl′) → case bl of
          λ { ll → k (inc→changedn (rotʳ y yv yl′ yr))
            ; ee → k (up (node y yv ll yl′ yr))
            ; rr → k (ev (node y yv ee yl′ yr))
            }
        ; (ev yl′) → k (ev (node y yv bl yl′ yr))
        ; (dn yl′) → case bl of
          λ { rr → k (inc→changeup (rotˡ y yv yl′ yr))
            ; ee → k (ev (node y yv rr yl′ yr))
            ; ll → k (dn (node y yv ee yl′ yr))
            }
        }
  go xs x (node y yv bl yl yr) (l , u) k | gt x>y =
    go xs x yr (x>y , u)
      λ { (up yr′) → case bl of
          λ { rr → k (inc→changedn (rotˡ y yv yl yr′))
            ; ee → k (up (node y yv rr yl yr′))
            ; ll → k (ev (node y yv ee yl yr′))
            }
        ; (ev yr′) → k (ev (node y yv bl yl yr′))
        ; (dn yr′) → case bl of
          λ { ll → k (inc→changeup (rotʳ y yv yl yr′))
            ; ee → k (ev (node y yv ll yl yr′))
            ; rr → k (dn (node y yv ee yl yr′))
            }
        }

open import Data.List

toList⊙ : Tree Val lb ub n → List (∃ x × Val x) → List (∃ x × Val x)
toList⊙ (leaf lb<ub) ks = ks
toList⊙ (node x xv bal xl xr) ks = toList⊙ xl ((x , xv) ∷ toList⊙ xr ks)

toList : Tree Val lb ub n → List (∃ x × Val x)
toList xs = toList⊙ xs []

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --guardedness #-}

module Stream where

import      Lvl
open import Data.Boolean
open import Data.List as List using (List)
import      Data.List.Functions as List
import      Data.List.Proofs as List
import      Data.List.Equiv.Id as List
open import Functional
open import Function.Iteration
open import Function.Iteration.Proofs
open import Logic
open import Logic.Propositional
open import Numeral.Natural
open import Relator.Equals
open import Relator.Equals.Proofs
open import Type

private variable ℓ : Lvl.Level
private variable T A B : Type{ℓ}
private variable a x init : T
private variable f : A → B
private variable n : ℕ

-- A countably infinite list
record Stream (T : Type{ℓ}) : Type{ℓ} where
  coinductive
  field
    head : T
    tail : Stream(T)
open Stream

module _ where
  -- The n:th element of a stream.
  -- Example: index(2)(0,1,2,…) = 2
  index : Stream(T) → ℕ → T
  index(l)(𝟎)    = head(l)
  index(l)(𝐒(n)) = index(tail(l))(n)

  -- The constant stream, consisting of a single element repeated.
  -- Example: repeat(x) = (x,x,x,..)
  repeat : T → Stream(T)
  head(repeat(x)) = x
  tail(repeat(x)) = repeat(x)

  -- The stream consisting of a list repeated (concatenated infinite many times).
  -- Example: loop(1,2,3) = (1,2,3 , 1,2,3 , 1,2,3 , …)
  loop : (l : List(T)) → (l ≢ List.∅) → Stream(T)
  loop List.∅       p with () ← p [≡]-intro
  head (loop (x List.⊰ l) p) = x
  tail (loop (x List.⊰ l) p) = loop (List.postpend x l) List.[∅]-postpend-unequal

  -- The stream of two interleaved streams.
  -- Example: interleave₂(1,2,3,‥)(a,b,c,…) = (1,a , 2,b , 3,c , …)
  interleave₂ : Stream(T) -> Stream(T) -> Stream(T)
  head(interleave₂(a)(b)) = head(a)
  tail(interleave₂(a)(b)) = interleave₂(b)(tail a)

  -- A stream which skips the first n number of elements from the specified stream.
  -- From the stream of (index 0 l , index 1 l , index 2 l , ..), the stream of (index n l , index (n+1) l , index (n+2) l , ..)
  -- Example: skip(2)(1,2,3,4,…) = (3,4,…)
  skip : ℕ → Stream(T) -> Stream(T)
  head(skip 𝟎      l) = head(l)
  tail(skip 𝟎      l) = tail(l)
  head(skip (𝐒(n)) l) = head(skip n (tail(l)))
  tail(skip (𝐒(n)) l) = tail(skip n (tail(l)))

  -- From the stream of (index 0 l , index 1 l , index 2 l , ..), the stream of (index 0 l , index n l , index (2⋅n) l , ..)
  -- Example: takeMultiples(3)(0,1,2,…) = (0,3,6,…)
  takeMultiples : ℕ → Stream(T) -> Stream(T)
  head(takeMultiples _ l) = head(l)
  tail(takeMultiples n l) = takeMultiples n ((tail ^ n) l)

  -- From the stream of (a,b,c,..), the stream of (x,a,b,c,..)
  _⊰_ : T → Stream(T) -> Stream(T)
  head(x ⊰ _) = x
  tail(_ ⊰ l) = l

  -- Stream of (init , f(init) , f(f(init)) , ..)
  iterated : T -> (T → T) → Stream(T)
  head(iterated init _) = init
  tail(iterated init f) = iterated (f(init)) f

  -- List from the initial part of the stream
  take : ℕ → Stream(T) → List(T)
  take(𝟎)   (l) = List.∅
  take(𝐒(n))(l) = head(l) List.⊰ take(n)(tail(l))

  -- Example: indexIntervals(0,0,2,0,1,2,…)(0,1,2,3,…) = (0,0,2,2,3,5,…)
  indexIntervals : Stream(ℕ) → Stream(T) → Stream(T)
  head (indexIntervals i l) = index l (head i)
  tail (indexIntervals i l) = indexIntervals (tail i) (skip (head i) l)

module _ where
  -- From the stream of (a,b,c,..), the stream of (f(a),f(b),f(c),..)
  map : (A → B) → Stream(A) → Stream(B)
  head(map f(l)) = f(head(l))
  tail(map f(l)) = map f(tail(l))

{- TODO: May not terminate. For example when P = const 𝐹
module _ {ℓ} {A : Type{ℓ}} where
  filter : (A → Bool) → Stream(A) → Stream(A)
  head(filter p(l)) with p(head(l))
  ... | 𝑇 = head(l)
  ... | 𝐹 = head(filter p(tail(l)))
  tail(filter p(l)) = filter p(tail(l))
-}

module _ where
  data _∈_ {T : Type{ℓ}} : T → Stream(T) → Stmt{ℓ} where
    [∈]-head : ∀{l}   → (head(l) ∈ l)
    [∈]-tail : ∀{a l} → (a ∈ tail(l)) → (a ∈ l)

  private variable l : Stream(T)

  index-of-[∈] : (x ∈ l) → ℕ
  index-of-[∈] [∈]-head     = 𝟎
  index-of-[∈] ([∈]-tail p) = 𝐒(index-of-[∈] p)

  index-of-[∈]-correctness : ∀{p : (x ∈ l)} → (index l (index-of-[∈] p) ≡ x)
  index-of-[∈]-correctness {x = .(head l)} {l} {[∈]-head}   = [≡]-intro
  index-of-[∈]-correctness {x = x}         {l} {[∈]-tail p} = index-of-[∈]-correctness {x = x} {tail l} {p}

  _⊆_ : Stream(T) → Stream(T) → Stmt
  _⊆_ l₁ l₂ = ∀{a} → (a ∈ l₁) → (a ∈ l₂)

  [∈]-tails : ((tail ^ n)(l) ⊆ l)
  [∈]-tails {n = 𝟎}   {l = l} {a} tailn = tailn
  [∈]-tails {n = 𝐒 n} {l = l} {a} tailn = [∈]-tail ([∈]-tails {n = n} {l = tail l} {a} ([≡]-substitutionₗ ([^]-inner-value {f = tail}{x = l}{n}) {a ∈_} tailn))

  [∈]-head-tail : (head(tail(l)) ∈ l)
  [∈]-head-tail = [∈]-tail ([∈]-head)

  [∈]-head-tails-membership : (head((tail ^ n)(l)) ∈ l)
  [∈]-head-tails-membership{𝟎}       = [∈]-head
  [∈]-head-tails-membership{𝐒(n)}{l} = [∈]-tails {n = n} ([∈]-head-tail)

  [∈]-disjunction : (x ∈ l) → ((x ≡ head(l)) ∨ (x ∈ tail(l)))
  [∈]-disjunction ([∈]-head)       = [∨]-introₗ [≡]-intro
  [∈]-disjunction ([∈]-tail proof) = [∨]-introᵣ proof

  [∈]-index : (index l n ∈ l)
  [∈]-index {n = 𝟎}    = [∈]-head
  [∈]-index {n = 𝐒(n)} = [∈]-tail ([∈]-index {n = n})

  repeat-[∈] : (x ∈ repeat(a)) ↔ (x ≡ a)
  repeat-[∈] {x = x}{a = a} = [↔]-intro left right where
    left : (x ∈ repeat(a)) ← (x ≡ a)
    left ([≡]-intro) = [∈]-head

    right : (x ∈ repeat(a)) → (x ≡ a)
    right ([∈]-head)       = [≡]-intro
    right ([∈]-tail proof) = right(proof)

  map-[∈] : (x ∈ l) → (f(x) ∈ map f(l))
  map-[∈]         ([∈]-head)       = [∈]-head
  map-[∈] {l = l} ([∈]-tail proof) = [∈]-tail (map-[∈] {l = tail l} (proof))

  [⊰][∈] : (a ∈ (x ⊰ l)) ↔ ((x ≡ a) ∨ (a ∈ l))
  [⊰][∈] {a = a}{x = x}{l = l} = [↔]-intro ll rr where
    ll : (a ∈ (x ⊰ l)) ← ((x ≡ a) ∨ (a ∈ l))
    ll ([∨]-introₗ ([≡]-intro)) = [∈]-head
    ll ([∨]-introᵣ (proof))     = [∈]-tail (proof)

    rr : (a ∈ (x ⊰ l)) → ((x ≡ a) ∨ (a ∈ l))
    rr ([∈]-head)         = [∨]-introₗ ([≡]-intro)
    rr ([∈]-tail (proof)) = [∨]-introᵣ (proof)

  iterated-init-[∈] : (init ∈ iterated(init)(f))
  iterated-init-[∈] = [∈]-head

  iterated-next-[∈] : (x ∈ iterated(init)(f)) → (f(x) ∈ iterated(init)(f))
  iterated-next-[∈] ([∈]-head)       = [∈]-tail ([∈]-head)
  iterated-next-[∈] ([∈]-tail proof) = [∈]-tail (iterated-next-[∈] (proof))
  -- First:
  --   head(iterated(init)(f)) ∈ iterated(init)(f)
  --   init ∈ iterated(init)(f)
  --   ...
  -- Second:
  --   x ∈ tail(iterated(init)(f))
  --   x ∈ iterated (f(init)) f
  --   ...

  iterated-[∈] : ((f ^ n)(init) ∈ iterated(init)(f))
  iterated-[∈] {n = 𝟎}   = iterated-init-[∈]
  iterated-[∈] {n = 𝐒 n} = iterated-next-[∈] (iterated-[∈] {n = n})

-- Stream of (0,1,2,3,..)
[ℕ]-stream : Stream(ℕ)
[ℕ]-stream = iterated(𝟎)(𝐒)

[ℕ]-stream-[∈] : (n ∈ [ℕ]-stream)
[ℕ]-stream-[∈]{𝟎}    = [∈]-head
[ℕ]-stream-[∈]{𝐒(n)} = iterated-next-[∈]([ℕ]-stream-[∈]{n})

-- Stream of (f(0),f(1),f(2),f(3),..)
[ℕ]-function-stream : (ℕ → T) → Stream(T)
[ℕ]-function-stream f = map f([ℕ]-stream)

module _ {ℓ} {T : Type{ℓ}} where
  open import Logic.Predicate
  open import Logic.Predicate.Theorems
  open import Structure.Function.Domain
  open import Type.Size.Countable

  -- This provides another way of proving that a type is countable.
  -- The method is: If a stream can enumerate every object of a certain type, then it is countable.
  countable-equivalence : ∃(l ↦ ∀{x : T} → (x ∈ l)) ↔ Countable(T)
  countable-equivalence = [↔]-intro left right where
    left : ∃(l ↦ ∀{x : T} → (x ∈ l)) ← Countable(T)
    ∃.witness (left ([∃]-intro f ⦃ intro proof ⦄)) = [ℕ]-function-stream f
    ∃.proof   (left ([∃]-intro f ⦃ intro proof ⦄)) {x} with proof{x}
    ... | [∃]-intro n ⦃ [≡]-intro ⦄ = map-[∈] [ℕ]-stream-[∈]

    right : ∃(l ↦ ∀{x : T} → (x ∈ l)) → Countable(T)
    ∃.witness (right ([∃]-intro l ⦃ p ⦄)) = index l
    ∃.witness (Surjective.proof (∃.proof (right ([∃]-intro l ⦃ p ⦄))) {x}) = index-of-[∈] (p{x})
    ∃.proof   (Surjective.proof (∃.proof (right ([∃]-intro l ⦃ p ⦄))) {x}) = index-of-[∈]-correctness {p = p}

ext: agda

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Oscar.Data.AList.properties {𝔣} (FunctionName : Set 𝔣) where

open import Oscar.Category.Category
open import Oscar.Category.Functor
open import Oscar.Category.Morphism
open import Oscar.Category.Semigroupoid
open import Oscar.Category.Semifunctor
open import Oscar.Category.Setoid
open import Oscar.Class.ThickAndThin
open import Oscar.Data.AList FunctionName
open import Oscar.Data.Equality
open import Oscar.Data.Equality.properties
open import Oscar.Data.Fin
open import Oscar.Data.Fin.ThickAndThin
open import Oscar.Data.Maybe
open import Oscar.Data.Nat
open import Oscar.Data.Product
open import Oscar.Data.Term FunctionName
import      Oscar.Data.Term.internal.SubstituteAndSubstitution FunctionName as S
open import Oscar.Data.Term.ThickAndThin FunctionName
open import Oscar.Function

module 𝔊₂ = Category S.𝔾₁
module 𝔉◃ = Functor S.𝔽◂

𝕞₁ = ⇧ AList

module 𝔐₁ = Morphism 𝕞₁

private

  _∙_ : ∀ {m n} → m 𝔐₁.↦ n → ∀ {l} → l 𝔐₁.↦ m → l 𝔐₁.↦ n
  ρ ∙ anil = ρ
  ρ ∙ (σ asnoc t' / x) = (ρ ∙ σ) asnoc t' / x

  ∙-associativity : ∀ {l m} (ρ : l 𝔐₁.↦ m) {n} (σ : n 𝔐₁.↦ _) {o} (τ : o 𝔐₁.↦ _) → (ρ ∙ σ) ∙ τ ≡ ρ ∙ (σ ∙ τ)
  ∙-associativity ρ σ anil = refl
  ∙-associativity ρ σ (τ asnoc t / x) = cong (λ s → s asnoc t / x) (∙-associativity ρ σ τ)

instance

  IsSemigroupoid𝕞₁∙ : IsSemigroupoid 𝕞₁ _∙_
  IsSemigroupoid.extensionality IsSemigroupoid𝕞₁∙ f₁≡f₂ g₁≡g₂ = cong₂ (λ ‵ → _∙_ ‵) g₁≡g₂ f₁≡f₂
  IsSemigroupoid.associativity IsSemigroupoid𝕞₁∙ f g h = ∙-associativity h g f

𝕘₁ : Semigroupoid _ _ _
𝕘₁ = 𝕞₁ , _∙_

private

  ε : ∀ {n} → n 𝔐₁.↦ n
  ε = anil

  ∙-left-identity : ∀ {m n} (σ : AList m n) → ε ∙ σ ≡ σ
  ∙-left-identity anil = refl
  ∙-left-identity (σ asnoc t' / x) = cong (λ σ → σ asnoc t' / x) (∙-left-identity σ)

instance

  IsCategory𝕘₁ε : IsCategory 𝕘₁ ε
  IsCategory.left-identity IsCategory𝕘₁ε = ∙-left-identity
  IsCategory.right-identity IsCategory𝕘₁ε _ = refl

𝔾₁ : Category _ _ _
𝔾₁ = 𝕘₁ , ε

𝕞₂ = 𝔊₂.𝔐
module 𝔐₂ = Morphism 𝕞₂

private

  sub : ∀ {m n} → m 𝔐₁.↦ n → m 𝔊₂.↦ n
  sub anil = i
  sub (σ asnoc t' / x) =  sub σ 𝔊₂.∙ (t' for x)

  fact1 : ∀ {l m n} (ρ : AList m n) (σ : AList l m) → sub (ρ ∙ σ) ≡̇ (sub ρ 𝔊₂.∙ sub σ)
  fact1 ρ anil v = refl
  fact1 {suc l} {m} {n} r (s asnoc t' / x) v = trans hyp-on-terms ◃-assoc
    where
      t = (t' for x) v
      hyp-on-terms = 𝔉◃.extensionality (fact1 r s) t
      ◃-assoc = 𝔉◃.distributivity (sub s) (sub r) t

𝕘₁,₂ : Semigroupoids _ _ _ _ _ _
𝕘₁,₂ = 𝕘₁ , 𝔊₂.semigroupoid

instance

  IsSemifunctorSub∙◇ : IsSemifunctor 𝕘₁,₂ sub
  IsSemifunctor.extensionality IsSemifunctorSub∙◇ refl _ = refl
  IsSemifunctor.distributivity IsSemifunctorSub∙◇ f g x = fact1 g f x

semifunctorSub∙◇ : Semifunctor _ _ _ _ _ _
semifunctorSub∙◇ = 𝕘₁,₂ , sub

instance

  IsFunctor𝔽 : IsFunctor (𝔾₁ , S.𝔾₁) sub
  IsFunctor.identity IsFunctor𝔽 _ _ = refl

𝔽 : Functor _ _ _ _ _ _
𝔽 = (𝔾₁ , S.𝔾₁) , sub

--   fact1 : ∀ {l m n} (ρ : AList m n) (σ : AList l m) → sub (ρ ∙ σ) ≡̇ (sub ρ ◇ sub σ)
--   fact1 ρ anil v = refl
--   fact1 {suc l} {m} {n} r (s asnoc t' / x) v = trans hyp-on-terms ◃-assoc
--     where
--       t = (t' for x) v
--       hyp-on-terms = ◃-extensionality (fact1 r s) t
--       ◃-assoc = ◃-associativity (sub s) (sub r) t

-- _∃asnoc_/_ : ∀ {m} (a : ∃ (AList m)) (t' : Term m) (x : Fin (suc m))
--   → ∃ (AList (suc m))
-- (n , σ) ∃asnoc t' / x = n , σ asnoc t' / x

-- flexFlex : ∀ {m} (x y : Fin m) → ∃ (AList m)
-- flexFlex {suc m} x y with check x y
-- ...              | just y' = m , anil asnoc i y' / x
-- ...              | nothing = suc m , anil
-- flexFlex {zero} () _

-- flexRigid : ∀ {m} (x : Fin m) (t : Term m) → Maybe (∃(AList m))
-- flexRigid {suc m} x t with check x t
-- ...                   | just t' = just (m , anil asnoc t' / x)
-- ...                   | nothing = nothing
-- flexRigid {zero} () _


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

-- Formalization of internal relations
-- (=congruences: https://ncatlab.org/nlab/show/congruence)

open import Categories.Category
module Categories.Object.InternalRelation {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level hiding (zero)
open import Data.Unit
open import Data.Fin using (Fin; zero) renaming (suc to nzero)

import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR
open import Categories.Morphism.Notation

open import Categories.Diagram.Pullback
open import Categories.Diagram.KernelPair
open import Categories.Category.Cartesian

open import Categories.Category.BinaryProducts 𝒞 using (BinaryProducts; module BinaryProducts)

private
  module 𝒞 = Category 𝒞

open Category 𝒞
open Mor 𝒞

-- A relation is a span, "which is (-1)-truncated as a morphism into the cartesian product."
-- (https://ncatlab.org/nlab/show/span#correspondences)
isRelation : {X Y R : 𝒞.Obj} (f : R ⇒ X) (g : R ⇒ Y) → Set (o ⊔ ℓ ⊔ e)
isRelation{X}{Y}{R} f g = JointMono
     (Fin 2)
     (λ{zero → X; (nzero _) → Y})
     (λ{zero → f; (nzero _) → g})

record Relation (X Y : 𝒞.Obj) : Set (suc (o ⊔ ℓ ⊔ e)) where
  open Mor 𝒞

  field
    dom : 𝒞.Obj
    p₁ : dom ⇒ X
    p₂ : dom ⇒ Y

  field
    relation : isRelation p₁ p₂

record isEqSpan {X R : 𝒞.Obj} (f : R ⇒ X) (g : R ⇒ X) : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
     R×R : Pullback 𝒞 f g

  module R×R = Pullback R×R renaming (P to dom)

  field
     refl  : X ⇒ R
     sym   : R ⇒ R
     trans : R×R.dom ⇒ R

     is-refl₁ : f ∘ refl ≈ id
     is-refl₂ : g ∘ refl ≈ id

     is-sym₁ : f ∘ sym ≈ g
     is-sym₂ : g ∘ sym ≈ f

     is-trans₁ : f ∘ trans ≈ f ∘ R×R.p₁
     is-trans₂ : g ∘ trans ≈ g ∘ R×R.p₂

-- Internal equivalence
record Equivalence (X : 𝒞.Obj) : Set (suc (o ⊔ ℓ ⊔ e)) where
  open Mor 𝒞
  open BinaryProducts

  field
     R : Relation X X

  open Relation R
  module R = Relation R

  field
    eqspan : isEqSpan R.p₁ R.p₂

module _ where
  open Pullback hiding (P)

  KP⇒EqSpan : {X Y : 𝒞.Obj} (f : X ⇒ Y) → (kp : KernelPair 𝒞 f) → (p : Pullback 𝒞 (p₁ kp) (p₂ kp)) → isEqSpan (p₁ kp) (p₂ kp)
  KP⇒EqSpan f kp p = record
    { R×R = p
    ; refl = universal kp {_} {id}{id} 𝒞.Equiv.refl
    ; sym  = universal kp {_} {p₂ kp}{p₁ kp} (𝒞.Equiv.sym (commute kp))
    ; trans = universal kp {_}{p₁ kp ∘ p₁ p}{p₂ kp ∘ p₂ p} (∘-resp-≈ʳ (commute p))
    ; is-refl₁  = p₁∘universal≈h₁ kp
    ; is-refl₂  = p₂∘universal≈h₂ kp
    ; is-sym₁   = p₁∘universal≈h₁ kp
    ; is-sym₂   = p₂∘universal≈h₂ kp
    ; is-trans₁ = p₁∘universal≈h₁ kp
    ; is-trans₂ = p₂∘universal≈h₂ kp
    }

  KP⇒Relation : {X Y : 𝒞.Obj} (f : X ⇒ Y) → (kp : KernelPair 𝒞 f) → (p : Pullback 𝒞 (p₁ kp) (p₂ kp)) → isRelation (p₁ kp) (p₂ kp)
  KP⇒Relation f kp _ _ _ eq = unique-diagram kp (eq zero) (eq (nzero zero))


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

open import HoTT

module experimental.CubicalTypes where

data access : ℕ → ℕ → Type₀ where
  [] : access O O
  _#up : ∀ {n} {k} → access n k → access (S n) k
  _#down : ∀ {n} {k} → access n k → access (S n) k
  _#keep : ∀ {n} {k} → access n k → access (S n) (S k)

_a∙_ : ∀ {n k l} → access n k → access k l → access n l
_a∙_ [] a₂ = a₂
_a∙_ (a₁ #up) a₂ = (a₁ a∙ a₂) #up
_a∙_ (a₁ #down) a₂ = (a₁ a∙ a₂) #down
_a∙_ (a₁ #keep) (a₂ #up) = (a₁ a∙ a₂) #up
_a∙_ (a₁ #keep) (a₂ #down) = (a₁ a∙ a₂) #down
_a∙_ (a₁ #keep) (a₂ #keep) = (a₁ a∙ a₂) #keep

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Prelude.List where

open import Prelude.List.Base public

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
-- We can infer the type of a record by comparing the given
-- fields against the fields of the currently known records.
module InferRecordTypes where

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

record _×_ (A B : Set) : Set where
  field
    fst : A
    snd : B

pair = record { fst = zero; snd = zero }

record R₁ : Set where
  field
    x₁ : Nat

r₁ = record { x₁ = zero }

data T {A : Set} : A → Set where
  mkT : ∀ n → T n

record R₂ A : Set where
  field
    {x₁} : A
    x₂   : T x₁

r₂ = record { x₂ = mkT (suc zero) }

record R₃ : Set where
  field
    x₁ x₃ : Nat

r₃ = record { x₁ = zero; x₃ = suc zero }

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

-- This module contains properties that are only about the behavior of the handlers, nothing to do
-- with system state

open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Base.ByteString
open import LibraBFT.Base.Types
open import LibraBFT.Hash
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Util

module LibraBFT.Impl.Consensus.ChainedBFT.EventProcessor.Properties
  (hash    : BitString → Hash)
  (hash-cr : ∀{x y} → hash x ≡ hash y → Collision hash x y ⊎ x ≡ y)
  where

  open import LibraBFT.Impl.Consensus.ChainedBFT.EventProcessor hash hash-cr

  -- The quorum certificates sent in SyncInfo with votes are those from the peer state
  procPMCerts≡ : ∀ {ts pm pre vm αs}
               → (SendVote vm αs) ∈ LBFT-outs (processProposalMsg ts pm) pre
               → vm ^∙ vmSyncInfo ≡ mkSyncInfo (₋epHighestQC pre) (₋epHighestCommitQC pre)
  procPMCerts≡ (there x)   = ⊥-elim (¬Any[] x)  -- processProposalMsg sends only one vote
  procPMCerts≡ (here refl) = refl

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
module unit where

open import level
open import eq

data ⊤ {ℓ : Level} : Set ℓ where
  triv : ⊤

{-# COMPILE GHC ⊤ = data () (()) #-}

single-range : ∀{ℓ}{U : Set ℓ}{g : U → ⊤ {ℓ}} → ∀{u : U} → g u ≡ triv
single-range {_}{U}{g}{u} with g u
... | triv = refl

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-- Andreas, 2020-04-15, issue #4586
-- An unintended internal error.

test : Set₁
test = let ... | _ = Set
       in  Set

-- WAS:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs:1417

-- EXPECTED:
-- Could not parse the left-hand side ... | _
-- Operators used in the grammar:
--   None
-- when scope checking let ... | _ = Set in Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


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

module Control.Category.Slice where

open import Level using (suc; _⊔_)
open import Relation.Binary hiding (_⇒_)

open import Control.Category
open Category using () renaming (Obj to obj)

-- Given a category C and an object Tgt in C we can define a new category
-- whose objects S are pairs of an object Src in C
-- and a morphism out from Src to Tgt.

record SliceObj {o h e} (C : Category o h e) (Tgt : obj C) : Set (o ⊔ h ⊔ e) where
  constructor sliceObj
  open Category C -- public
  field
    Src : Obj
    out : Src ⇒ Tgt

-- In the following, we fix a category C and an object Tgt.

module _ {o h e} {C : Category o h e} {Tgt : obj C} where

  -- We use _⇒_ for C's morphisms and _∘_ for their composition.
  private
    open module C = Category C hiding (id; ops)

    Slice = SliceObj C Tgt
    open module Slice = SliceObj {C = C} {Tgt = Tgt}

  -- A morphism in the slice category into Tgt
  -- from slice (S, s) to (T, t)
  -- is a morphism f : S ⇒ T such that t ∘ f ≡ s.

  record SliceMorphism (S T : Slice) : Set (h ⊔ e)
    where
    constructor sliceMorphism
    field
      mor      : Src S ⇒ Src T
      triangle : (mor ⟫ out T) ≈ out S

  -- Two morphisms in the slice category are equal
  -- iff they are equal in the underlying category C.

  SliceHom : (S T : Slice) → Setoid _ _
  SliceHom S T = record
    { Carrier       = SliceMorphism S T
    ; _≈_           = λ f g → SliceMorphism.mor f ≈ SliceMorphism.mor g
    ; isEquivalence = record
      { refl  = refl
      ; sym   = sym
      ; trans = trans
      }
    } where open IsEquivalence (≈-equiv {Src S} {Src T})

  -- We write S ⇉ T for a morphism from slice S to slice T

  open HomSet SliceHom using () renaming (_⇒_ to _⇉_; _≈_ to _≐_)

  -- The identity slice morphism is just the identity morphism.

  slice-id : ∀ {P} → P ⇉ P
  slice-id = record { mor = C.id; triangle = C.id-first }

  -- The composition of slice morphims is just the composition in C.

  comp : ∀ {S T U} → S ⇉ T → T ⇉ U → S ⇉ U
  comp (sliceMorphism f tri-f) (sliceMorphism g tri-g) = record
    { mor      = f ⟫ g
    ; triangle = ≈-trans (C.∘-assoc f) (≈-trans (C.∘-cong ≈-refl tri-g) tri-f)
    }

  ops : CategoryOps SliceHom
  ops = record { id = slice-id ; _⟫_ = comp}

  sliceIsCategory : IsCategory SliceHom
  sliceIsCategory = record
    { ops = ops
    ; laws = record
      { id-first = C.id-first -- id-first
      ; id-last  = C.id-last
      ; ∘-assoc  = λ f → C.∘-assoc _
      ; ∘-cong   = C.∘-cong
      }
    }

-- The slice category.

module _  {o h e} (C : Category o h e) (Tgt : obj C) where

  module C = Category C

  _/_ : Category (o ⊔ h ⊔ e) (e ⊔ h) e
  _/_ = record
    { Obj = SliceObj C Tgt
    ; Hom = SliceHom
    ; isCategory = sliceIsCategory
    }

  open Category _/_

-- The terminal object in C / Tgt is (Tgt, id).

  terminalSlice : Obj
  terminalSlice = record { Src = Tgt; out = C.id }

  open IsFinal

  isTerminalSlice : IsFinal Hom terminalSlice
  final           isTerminalSlice {sliceObj Src f}
    = sliceMorphism f C.id-last
  final-universal isTerminalSlice {sliceObj Src f} {sliceMorphism g tri}
    = C.≈-trans (C.≈-sym C.id-last) tri

-- The initial object in C / Tgt is (0, initial)

  module _ {⊥ : obj C} (⊥-initial : IsInitial C.Hom ⊥) where

    open IsInitial ⊥-initial
      renaming (initial to abort; initial-universal to abort-unique)

    initialSlice : Obj
    initialSlice = record { Src = ⊥; out = abort }

    open IsInitial

    isInitialSlice : IsInitial Hom initialSlice
    initial           isInitialSlice = sliceMorphism abort abort-unique
    initial-universal isInitialSlice = abort-unique

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
open import Nat
open import Prelude
open import core
open import judgemental-erase
open import moveerase

module sensibility where
  mutual
    -- if an action transforms a ê in a synthetic posistion to another ê,
    -- they have the same type up erasure of the cursor
    actsense-synth : {Γ : ·ctx} {e e' : ê} {e◆ e'◆ : ė} {t t' : τ̇} {α : action} →
                erase-e e e◆  →
                erase-e e' e'◆ →
                Γ ⊢ e => t ~ α ~> e' => t' →
                Γ ⊢ e◆ => t →
                Γ ⊢ e'◆ => t'
    -- in the movement case, we defer to the movement erasure theorem
    actsense-synth er er' (SAMove x) wt with erasee-det (moveerasee' er x) er'
    ... | refl = wt

    -- in all the nonzipper cases, the cursor must be at the top for the
    -- action rule to apply, so we just build the new derivation
    -- directly. no recursion is needed; these are effectively base cases.
    actsense-synth _ EETop SADel _ = SEHole
    actsense-synth EETop (EEAscR ETTop) SAConAsc wt = SAsc (ASubsume wt TCRefl)
    actsense-synth _ EETop (SAConVar p) _ = SVar p
    actsense-synth EETop (EEAscR (ETArrL ETTop)) (SAConLam x) SEHole = SAsc (ALam x MAArr (ASubsume SEHole TCRefl))
    actsense-synth EETop (EEApR EETop) (SAConApArr x) wt = SAp wt x (ASubsume SEHole TCHole1)
    actsense-synth EETop (EEApR EETop) (SAConApOtw x) wt = SAp (SNEHole wt) MAHole (ASubsume SEHole TCRefl)
    actsense-synth _ EETop SAConNumlit _ = SNum
    actsense-synth EETop (EEPlusR EETop) (SAConPlus1 TCRefl) wt = SPlus (ASubsume wt TCRefl) (ASubsume SEHole TCHole1)
    actsense-synth EETop (EEPlusR EETop) (SAConPlus1 TCHole2) wt = SPlus (ASubsume wt TCHole1) (ASubsume SEHole TCHole1)
    actsense-synth EETop (EEPlusR EETop) (SAConPlus2 _) wt = SPlus (ASubsume (SNEHole wt) TCHole1) (ASubsume SEHole TCHole1)
    actsense-synth EETop (EENEHole EETop) SAConNEHole wt = SNEHole wt
    actsense-synth _ EETop (SAFinish x) _ = x

    --- zipper cases. in each, we recur on the smaller action derivation
    --- following the zipper structure, then reassemble the result
    actsense-synth (EEAscL er) (EEAscL er') (SAZipAsc1 x) (SAsc x₁)
      with actsense-ana er er' x x₁
    ... | ih = SAsc ih
    actsense-synth (EEAscR x₁) (EEAscR x) (SAZipAsc2 x₂ x₃ x₄ x₅) (SAsc x₆)
      with eraset-det x x₃
    ... | refl = SAsc x₅

    actsense-synth er (EEApL er') (SAZipApArr x x₁ x₂ act x₃) wt
      with actsense-synth x₁ er' act x₂
    ... | ih = SAp ih x x₃
    actsense-synth (EEApR er) (EEApR er') (SAZipApAna x x₁ x₂) (SAp wt x₃ x₄)
      with synthunicity x₁ wt
    ... | refl with matcharrunicity x x₃
    ... | refl with actsense-ana er er' x₂ x₄
    ... | ih = SAp wt x ih

    actsense-synth (EEPlusL er) (EEPlusL er') (SAZipPlus1 x) (SPlus x₁ x₂)
      with actsense-ana er er' x x₁
    ... | ih = SPlus ih x₂
    actsense-synth (EEPlusR er) (EEPlusR er') (SAZipPlus2 x) (SPlus x₁ x₂)
      with actsense-ana er er' x x₂
    ... | ih = SPlus x₁ ih

    actsense-synth er (EENEHole er') (SAZipHole x x₁ act) wt
      with actsense-synth x er' act x₁
    ... | ih = SNEHole ih

    -- if an action transforms an ê in an analytic posistion to another ê,
    -- they have the same type up erasure of the cursor.
    actsense-ana  : {Γ : ·ctx} {e e' : ê} {e◆ e'◆ : ė} {t : τ̇} {α : action} →
                  erase-e e  e◆ →
                  erase-e e' e'◆ →
                  Γ ⊢ e ~ α ~> e' ⇐ t →
                  Γ ⊢ e◆ <= t →
                  Γ ⊢ e'◆ <= t
    -- in the subsumption case, punt to the other theorem
    actsense-ana er1 er2 (AASubsume x x₁ x₂ x₃) _ = ASubsume (actsense-synth x er2 x₂ x₁) x₃

    -- for movement, appeal to the movement-erasure theorem
    actsense-ana er1 er2 (AAMove x) wt with erasee-det (moveerasee' er1 x) er2
    ... | refl = wt

    -- in the nonzipper cases, we again know where the hole must be, so we
    -- force it and then build the relevant derivation directly.
    actsense-ana EETop EETop AADel wt = ASubsume SEHole TCHole1
    actsense-ana EETop (EEAscR ETTop) AAConAsc wt = ASubsume (SAsc wt) TCRefl
    actsense-ana EETop (EENEHole EETop) (AAConVar x₁ p) wt = ASubsume (SNEHole (SVar p)) TCHole1
    actsense-ana EETop (EELam EETop) (AAConLam1 x₁ x₂) wt = ALam x₁ x₂ (ASubsume SEHole TCHole1)
    actsense-ana EETop (EENEHole EETop) (AAConNumlit x) wt = ASubsume (SNEHole SNum) TCHole1
    actsense-ana EETop EETop (AAFinish x) wt = x
    actsense-ana EETop (EENEHole (EEAscR (ETArrL ETTop))) (AAConLam2 x _) (ASubsume SEHole q) =
                     ASubsume (SNEHole (SAsc (ALam x MAArr (ASubsume SEHole TCRefl)))) q

    -- all subsumptions in the right derivation are bogus, because there's no
    -- rule for lambdas synthetically
    actsense-ana (EELam _) (EELam _) (AAZipLam _ _ _) (ASubsume () _)

    -- that leaves only the zipper cases for lambda, where we force the
    -- forms and then recurr into the body of the lambda being checked.
    actsense-ana (EELam er1) (EELam er2) (AAZipLam x₁ x₂ act) (ALam x₄ x₅ wt)
      with matcharrunicity x₂ x₅
    ... | refl with actsense-ana er1 er2 act wt
    ... | ih = ALam x₄ x₅ ih


text:
open import Agda.Primitive
open import Agda.Builtin.List
open import Agda.Builtin.Maybe

data Coercible (A : Set) (B : Set) : Set where
  TrustMe : Coercible A B

postulate coerce : {A B : Set} {{_ : Coercible A B}} → A → B

instance
  coerce-fun : {A B : Set} {{_ : Coercible A B}}
             → {C D : Set} {{_ : Coercible C D}}
             → Coercible (B → C) (A → D)
  coerce-fun = TrustMe

  coerce-refl : {A : Set} → Coercible A A
  coerce-refl = TrustMe

postulate
  primCatMaybes : {A : Set} → List (Maybe A) → List A

catMaybes : {A : Set} → List (Maybe A) → List A
catMaybes = coerce (primCatMaybes {_})

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- Monotone functions
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

module Partiality-monad.Inductive.Monotone where

open import Equality.Propositional
open import Prelude

open import Bijection equality-with-J using (_↔_)

import Partiality-algebra.Monotone as M
open import Partiality-monad.Inductive

-- Definition of monotone functions.

[_⊥→_⊥]⊑ : ∀ {a b} → Type a → Type b → Type (a ⊔ b)
[ A ⊥→ B ⊥]⊑ = M.[ partiality-algebra A ⟶ partiality-algebra B ]⊑

module [_⊥→_⊥]⊑ {a b} {A : Type a} {B : Type b} (f : [ A ⊥→ B ⊥]⊑) =
  M.[_⟶_]⊑ f

open [_⊥→_⊥]⊑

-- Identity.

id⊑ : ∀ {a} {A : Type a} → [ A ⊥→ A ⊥]⊑
id⊑ = M.id⊑

-- Composition.

infixr 40 _∘⊑_

_∘⊑_ : ∀ {a b c} {A : Type a} {B : Type b} {C : Type c} →
       [ B ⊥→ C ⊥]⊑ → [ A ⊥→ B ⊥]⊑ → [ A ⊥→ C ⊥]⊑
_∘⊑_ = M._∘⊑_

-- Equality characterisation lemma for monotone functions.

equality-characterisation-monotone :
  ∀ {a b} {A : Type a} {B : Type b} {f g : [ A ⊥→ B ⊥]⊑} →
  (∀ x → function f x ≡ function g x) ↔ f ≡ g
equality-characterisation-monotone =
  M.equality-characterisation-monotone

-- Composition is associative.

∘⊑-assoc :
  ∀ {a b c d} {A : Type a} {B : Type b} {C : Type c} {D : Type d}
  (f : [ C ⊥→ D ⊥]⊑) (g : [ B ⊥→ C ⊥]⊑) {h : [ A ⊥→ B ⊥]⊑} →
  f ∘⊑ (g ∘⊑ h) ≡ (f ∘⊑ g) ∘⊑ h
∘⊑-assoc = M.∘⊑-assoc

module _ {a b} {A : Type a} {B : Type b} where

  -- If a monotone function is applied to an increasing sequence,
  -- then the result is another increasing sequence.

  [_$_]-inc :
    [ A ⊥→ B ⊥]⊑ → Increasing-sequence A → Increasing-sequence B
  [_$_]-inc = M.[_$_]-inc

  -- A lemma relating monotone functions and least upper bounds.

  ⨆$⊑$⨆ : (f : [ A ⊥→ B ⊥]⊑) →
          ∀ s → ⨆ [ f $ s ]-inc ⊑ function f (⨆ s)
  ⨆$⊑$⨆ = M.⨆$⊑$⨆

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


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

module SDG.Extra.OrderedAlgebra where

open import Relation.Binary
open import Algebra.FunctionProperties
open import Level

open import SDG.Extra.OrderedAlgebra.Structures

record OrderedCommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
  infix 8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix 4 _≈_
  field
    Carrier : Set c
    _≈_ : Rel Carrier ℓ
    _<_ : Rel Carrier ℓ
    _+_ : Op₂ Carrier
    _*_ : Op₂ Carrier
    -_ : Op₁ Carrier
    0# : Carrier
    1# : Carrier
    isOrderedCommutativeRing : IsOrderedCommutativeRing _≈_ _<_ _+_ _*_ -_ 0# 1#

  open IsOrderedCommutativeRing isOrderedCommutativeRing public

max_stars_repo_name: wrrnhttn/agda-sdg

max_issues_repo_name: wrrnhttn/agda-sdg

max_forks_repo_name: wrrnhttn/agda-sdg


text:
module Imports.ImportedDisplayForms where

open import Agda.Builtin.Nat

postulate
  _plus_ : Set

{-# DISPLAY _+_ a b = a plus b #-}


text:
module CP where

open import Level
open import Data.Nat
open import Relation.Nullary
-- open import Data.String using (String)

TypeVar : Set
TypeVar = ℕ

infixl 10 _⨂_
infixl 10 _⅋_
data Type : Set where
    -- ‵_ : TypeVar → Type
    -- _^ : Type → Type
    _⨂_ : Type → Type → Type
    _⅋_ : Type → Type → Type
    -- _⨁_ : Type → Type → Type
    -- _&_ : Type → Type → Type
    -- !_ : Type → Type
    -- ¿_ : Type → Type
    -- ∃[_] : Type → Type
    -- ∀[_] : Type → Type
    𝟙 : Type
    ⊥ : Type
    𝟘 : Type
    ⊤ : Type

infixl 11 _^
_^ : Type → Type
(A ⨂ B) ^ = A ^ ⅋ B ^
(A ⅋ B) ^ = A ^ ⨂ B ^
𝟙 ^ = ⊥
⊥ ^ = 𝟙
𝟘 ^ = ⊤
⊤ ^ = 𝟘

open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Relation.Nullary.Product
open import Data.Product
open import Agda.Builtin.Bool

-- _≟t_ : (A B : Type) → Dec (A ≡ B)
-- (A ⨂ B) ≟t (C ⨂ D) with A ≟t C | B ≟t D
-- ... | yes refl | yes refl = yes refl
-- ... | yes refl | no ¬q    = no λ where refl → ¬q refl
-- ... | no ¬p    | yes q    = no λ where refl → ¬p refl
-- ... | no ¬p    | no ¬q    = no λ where refl → ¬p refl
-- (A ⨂ B) ≟t (C ⅋ D) = no (λ ())
-- (A ⨂ B) ≟t 𝟙 = no (λ ())
-- (A ⨂ B) ≟t ⊥ = no (λ ())
-- (A ⨂ B) ≟t 𝟘 = no (λ ())
-- (A ⨂ B) ≟t ⊤ = no (λ ())
-- (A ⅋ B) ≟t (C ⨂ D) = no (λ ())
-- (A ⅋ B) ≟t (C ⅋ D) with A ≟t C | B ≟t D
-- ... | yes refl | yes refl = yes refl
-- ... | yes refl | no ¬q    = no λ where refl → ¬q refl
-- ... | no ¬p    | yes q    = no λ where refl → ¬p refl
-- ... | no ¬p    | no ¬q    = no λ where refl → ¬p refl
-- (A ⅋ B) ≟t 𝟙 = no (λ ())
-- (A ⅋ B) ≟t ⊥ = no (λ ())
-- (A ⅋ B) ≟t 𝟘 = no (λ ())
-- (A ⅋ B) ≟t ⊤ = no (λ ())
-- 𝟙 ≟t (B ⨂ C) = no (λ ())
-- 𝟙 ≟t (B ⅋ C) = no (λ ())
-- 𝟙 ≟t 𝟙 = yes refl
-- 𝟙 ≟t ⊥ = no (λ ())
-- 𝟙 ≟t 𝟘 = no (λ ())
-- 𝟙 ≟t ⊤ = no (λ ())
-- ⊥ ≟t (B ⨂ C) = no (λ ())
-- ⊥ ≟t (B ⅋ C) = no (λ ())
-- ⊥ ≟t 𝟙 = no (λ ())
-- ⊥ ≟t ⊥ = yes refl
-- ⊥ ≟t 𝟘 = no (λ ())
-- ⊥ ≟t ⊤ = no (λ ())
-- 𝟘 ≟t (B ⨂ C) = no (λ ())
-- 𝟘 ≟t (B ⅋ C) = no (λ ())
-- 𝟘 ≟t 𝟙 = no (λ ())
-- 𝟘 ≟t ⊥ = no (λ ())
-- 𝟘 ≟t 𝟘 = yes refl
-- 𝟘 ≟t ⊤ = no (λ ())
-- ⊤ ≟t (B ⨂ C) = no (λ ())
-- ⊤ ≟t (B ⅋ C) = no (λ ())
-- ⊤ ≟t 𝟙 = no (λ ())
-- ⊤ ≟t ⊥ = no (λ ())
-- ⊤ ≟t 𝟘 = no (λ ())
-- ⊤ ≟t ⊤ = yes refl

Chan : Set
Chan = ℕ

data Proc⁺ : Set
data Proc⁻ : Set

data Proc⁺ where
    _↔_ : Chan → Chan → Proc⁺

    ν_∶_∙_∣_ : Chan → Type → Proc⁻ → Proc⁻ → Proc⁺
-- infixl  7  _⟦⟧0

-- inherited types
data Proc⁻ where

    -- x[y].(P|Q)
    _⟦_⟧_∣_ : Chan → Chan → Proc⁻ → Proc⁻ → Proc⁻

    -- x(y).(P|Q)
    _⦅_⦆_ : Chan → Chan → Proc⁻ → Proc⁻

    -- x[].0
    _⟦⟧0 : Chan → Proc⁻
    -- x().P
    _⦅⦆_ : Chan → Proc⁻ → Proc⁻
    -- x.case()
    _case : Chan → Proc⁻

-- _[_/_] : Type → Type → TypeVar → Type
-- (‵ P) [ T / X ] with P ≟ X
-- ((‵ P) [ T / X ]) | yes p = T
-- ((‵ P) [ T / X ]) | no ¬p = ‵ P
-- (P ^) [ T / X ] = (P [ T / X ]) ^
-- (P ⨂ Q) [ T / X ] = (P [ T / X ]) ⨂ (Q [ T / X ])
-- (P ⅋ Q) [ T / X ] = (P [ T / X ]) ⅋ (Q [ T / X ])
-- (P ⨁ Q) [ T / X ] = (P [ T / X ]) ⨁ (Q [ T / X ])
-- (P & Q) [ T / X ] = (P [ T / X ]) & (Q [ T / X ])
-- (! P) [ T / X ] = ! (P [ T / X ])
-- (¿ P) [ T / X ] = ¿ (P [ T / X ])
-- ∃[ P ] [ T / zero ] = {!   !}
-- ∃[ P ] [ T / suc X ] = {!   !}
-- ∀[ P ] [ T / X ] = {!   !}
-- 𝟙 [ T / X ] = {!   !}
-- ⊥ [ T / X ] = {!   !}
-- 𝟘 [ T / X ] = {!   !}
-- ⊤ [ T / X ] = {!  !}

-- infixl 5 _,_∶_
-- data Session : Set where
--     _,_∶_ : Session → Chan → Type → Session
--     _++_ : Session → Session → Session
--     ∅ : Session

-- infix   4  _⊢↓_
-- infix   4  _⊢↑_
-- data _⊢↑_ : Proc⁺ → Session → Set
-- data _⊢↓_ : Proc⁻ → Session → Set

-- data _⊢↑_ where
--     ⊢↔ : ∀ {w x A}
--         ---------------
--         → w ↔ x ⊢↑ ∅ , w ∶ A ^ , x ∶ A

--     ⊢Cut : ∀ {P Q Γ Δ x A}
--         → P ⊢↓ Γ , x ∶ A
--         → Q ⊢↓ Δ , x ∶ A ^
--         ---------------
--         → ν x ∶ A ∙ P ∣ Q ⊢↑ Γ ++ Δ

-- data _⊢↓_ where

--     ⊢⨂ : ∀ {P Q Γ Δ y x A B}
--         → P ⊢↓ Γ , y ∶ A
--         → Q ⊢↓ Δ , x ∶ B
--         ---------------
--         → x ⟦ y ⟧ P ∣ Q ⊢↓ ∅ , x ∶ 𝟙

--     ⊢⅋ : ∀ {R Θ y x A B}
--         → R ⊢↓ Θ , y ∶ A , x ∶ B
--         ---------------
--         → x ⦅ y ⦆ R ⊢↓ Θ , x ∶ A ⅋ B

--     ⊢𝟏 : ∀ {x}
--         ---------------
--         → x ⟦⟧0 ⊢↓ ∅ , x ∶ 𝟙

--     ⊢⊥ : ∀ {x P Γ}
--         → P ⊢↓ Γ
--         ---------------
--         → x ⦅⦆ P ⊢↓ Γ , x ∶ ⊥

--     ⊢⊤ : ∀ {x Γ}
--         ---------------
--         → x case ⊢↓ Γ , x ∶ ⊤

-- data Result (P : Proc⁺) : Set where
--     known : (Γ : Session) → P ⊢↑ Γ → Result P
--     cntx? : ((Γ : Session) → P ⊢↑ Γ) → Result P
--     type? : ((Γ : Session) → (x : Chan) → (T : Type) → P ⊢↑ Γ , x ∶ T) → Result P
--     wrong : Result P

-- infer : ∀ (P : Proc⁺) → Result P
-- infer (w ↔ x) = type? λ Γ x A → {! ⊢↔ {w} {x} {A} !}
-- infer (ν x ∶ x₁ ∙ x₂ ∣ x₃) = {!   !}

-- open import Data.Bool hiding (_≟_)

open import Relation.Binary using (Decidable; DecSetoid)

ChanSetoid : DecSetoid _ _
ChanSetoid = ≡-decSetoid
    where
        open import Data.Nat.Properties using (≡-decSetoid)

module Example where
    open import CP.Session3 ChanSetoid Type

    Γ : Session
    Γ = (0 ∶ 𝟙) ∷ (1 ∶ 𝟘) ∷ []

    Δ : Session
    Δ = (1 ∶ 𝟘) ∷ (0 ∶ 𝟙) ∷ []

    open import Data.List.Relation.Binary.Subset.DecSetoid typeOfDecSetoid

-- _∋_ : Session → Chan → Bool
-- (Γ , y ∶ A) ∋ x with x ≟ y
-- ... | no ¬p = Γ ∋ x
-- ... | yes p = true
-- (Γ ++ Δ) ∋ x = (Γ ∋ x) ∨ (Δ ∋ x)
-- ∅ ∋ x = false

-- _≈_ : Session → Session → Set
-- Γ ≈ Δ = ∀ x → Γ ∋ x ≡ Δ ∋ x

-- empty : ∀ {Γ x A} → ¬ (∅ ≈ (Γ , x ∶ A))
-- empty {Γ} {x} {A} P with x ≟ x
-- ... | no ¬p = {!   !}
-- ... | yes p = {!   !}

-- lookup : (Γ : Session) (x : Chan) → Dec (∃[ Δ ] ∃[ A ] (Γ ≈ (Δ , x ∶ A)))
-- lookup (Γ , y ∶ A) x = {!   !}
-- lookup (Γ ++ Δ) x with lookup Γ x
-- ... | yes p = {!   !}
-- ... | no ¬p = {!   !}
-- lookup ∅ x = no (λ where (Γ , A , P) → {! P x  !})

-- infer : ∀ (P : Proc⁺) → Dec (∃[ Γ ] (P ⊢↑ Γ))
-- infer' : ∀ (P : Proc⁻) → Dec (∃[ Γ ] (P ⊢↓ Γ))
-- check : ∀ (P : Proc⁻) (Γ : Session) → Dec (P ⊢↓ Γ)

-- infer' (x ⟦ y ⟧ P ∣ Q) = {!   !}
-- infer' (x ⦅ y ⦆ P) with infer' P
-- ... | no ¬p = no λ where ((Γ , x ∶ A ⅋ B) , ⊢⅋ P⊢Γ) → ¬p ((Γ , y ∶ A , x ∶ B) , P⊢Γ)
-- ... | yes (Γ , P⊢Γ) = yes ({!   !} , (⊢⅋ {!   !}))
-- infer' (x ⟦⟧0) = yes (∅ , x ∶ 𝟙 , ⊢𝟏)
-- infer' (x ⦅⦆ P) with infer' P
-- ... | no ¬p = no λ where ((Γ , x ∶ ⊥) , ⊢⊥ P⊢Γ) → ¬p (Γ , P⊢Γ)
-- ... | yes (Γ , P⊢Γ) = yes ((Γ , x ∶ ⊥) , (⊢⊥ P⊢Γ))
-- infer' (x case) = yes (∅ , x ∶ ⊤ , ⊢⊤)

-- infer (w ↔ x) = yes ((∅ , w ∶ {!   !} , x ∶ {!   !}) , ⊢↔)
-- infer (ν x ∶ A ∙ P ∣ Q) with infer' P  | infer' Q
-- ... | no ¬p | no ¬q = {!   !}
-- ... | no ¬p | yes q = no (λ where (.(_ ++ _) , ⊢Cut x _) → ¬p {! x  !})
-- ... | yes p | no ¬q = {!   !}
-- ... | yes (Γ , P⊢Γ) | yes (Δ , Q⊢Δ) = yes ({!   !} , ⊢Cut {! P⊢Γ  !} {!   !})
-- --  = yes ({!   !} , {!   !})

-- check P Γ = {!   !}

-- infixl 4 _∶_∈_
-- data _∶_∈_ : Channel → Type → Session → Set where
--   Z  : ∀ {Γ x A}
--     ------------------
--     → x ∶ A ∈ Γ , x ∶ A

--   S_ : ∀ {Γ x y A B}
--     → x ∶ A ∈ Γ
--     ------------------
--     → x ∶ A ∈ Γ , x ∶ A , y ∶ B

-- ¿[_] : Session → Session
-- ¿[ Γ , x ∶ A ]  = ¿[ Γ ] , x ∶ ¿ A
-- ¿[ Γ ++ Δ ]     = ¿[ Γ ] ++ ¿[ Δ ]
-- ¿[ ∅ ]          = ∅

-- infix 4 ⊢_
-- data ⊢_ : Session → Set where

--     Ax : ∀ {A w x}
--         ---------------------------
--         → ⊢ ∅ , w ∶ A ^ , x ∶ A

--     Cut : ∀ {Γ Δ x A}
--         → (P : ⊢ Γ , x ∶ A)
--         → (Q : ⊢ Δ , x ∶ A ^)
--         ---------------------------
--         → ⊢ Γ ++ Δ

--     Times : ∀ {Γ Δ x y A B}
--         → (P : ⊢ Γ , y ∶ A)
--         → (Q : ⊢ Δ , x ∶ B)
--         ---------------------------
--         → ⊢ Γ ++ Δ , x ∶ A ⨂ B

--     Par : ∀ {Θ x y A B}
--         → (R : ⊢ Θ , y ∶ A , x ∶ B)
--         ---------------------------
--         → ⊢ Θ , x ∶ A ⅋ B

--     PlusL : ∀ {Γ x A B}
--         → (P : ⊢ Γ , x ∶ A)
--         ---------------------------
--         → ⊢ Γ , x ∶ A ⨁ B

--     PlusR : ∀ {Γ x A B}
--         → (P : ⊢ Γ , x ∶ B)
--         ---------------------------
--         → ⊢ Γ , x ∶ A ⨁ B

--     With : ∀ {Δ x A B}
--         → (Q : ⊢ Δ , x ∶ A)
--         → (R : ⊢ Δ , x ∶ B)
--         ---------------------------
--         → ⊢ Δ , x ∶ A & B

--     OfCourse : ∀ {Γ x y A}
--         → (P : ⊢ ¿[ Γ ] , y ∶ A)
--         ---------------------------
--         → ⊢ ¿[ Γ ] , x ∶ ! A

--     WhyNot : ∀ {Δ x y A}
--         → (Q : ⊢ Δ , y ∶ A)
--         ---------------------------
--         → ⊢ Δ , x ∶ ¿ A

--     Weaken : ∀ {Δ x A}
--         → (Q : ⊢ Δ)
--         ---------------------------
--         → ⊢ Δ , x ∶ ¿ A

--     Contract : ∀ {Δ x x' A}
--         → (Q : ⊢ Δ , x ∶ ¿ A , x' ∶ ¿ A)
--         ---------------------------
--         → ⊢ Δ , x ∶ ¿ A

--     -- Exist : ∀ {Γ x x' A}
--     --     → (Q : ⊢ Δ , x ∶ ¿ A , x' ∶ ¿ A)
--     --     ---------------------------
--     --     → ⊢ Δ , x ∶ ¿ A

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


text:
-- Currently modules are not allowed in mutual blocks.
-- This might change.
module ModuleInMutual where

mutual
  module A where
    T : Set -> Set
    T A = A

  module B where
    U : Set -> Set
    U B = B


text:
module lang-text where

open import Data.List
open import Data.String
open import Data.Char
open import Data.Char.Unsafe
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import logic

split : {Σ : Set} → (List Σ → Bool)
      → ( List Σ → Bool) → List Σ → Bool
split x y  [] = x [] /\ y []
split x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
  split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t

contains : String → String → Bool
contains x y = contains1 (toList x ) ( toList y ) where
   contains1 : List Char → List Char → Bool
   contains1 []  [] = false
   contains1 [] ( cx ∷ ly ) = false
   contains1  (cx ∷ lx)  [] = true
   contains1 (cx ∷ lx ) ( cy ∷ ly ) with cx ≟ cy
   ... | yes refl = contains1 lx ly
   ... | no n = false

-- w does not contain the substring ab
ex15a : Set
ex15a = (w : String ) → ¬ (contains w "ab"  ≡ true )

-- w does not contains substring baba
ex15b : Set
ex15b = (w : String ) → ¬ (contains w "baba"  ≡ true )

-- w contains neither the substing ab nor ba
ex15c : Set

-- w is any string not in a*b*
ex15c = (w : String ) → ( ¬ (contains w "ab"  ≡ true )  /\ ( ¬ (contains w "ba"  ≡ true )

ex15d : {!!}
ex15d = {!!}

ex15e : {!!}
ex15e = {!!}

ex15f : {!!}
ex15f = {!!}

ex15g : {!!}
ex15g = {!!}

ex15h : {!!}
ex15h = {!!}

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:
open import Tutorials.Monday-Complete
module Tutorials.Tuesday-Complete where

-----------
-- Pi and Sigma types
-----------

module Product where
  -- The open keyword opens a given module in the current namespace
  -- By default all of the public names of the module are opened
  -- The using keyword limits the imported definitions to those explicitly listed
  open Fin
  open Vec using (Vec; []; _∷_)
  open Simple using (¬_)

  variable
    P Q : A → Set

  -- Pi types: dependent function types
  -- For every x of type A, the predicate P x holds
  Π : (A : Set) → (Pred A) → Set
  Π A P = (x : A) → P x

  infix 5 _,_
  -- Sigma types: dependent product types, existential types
  -- For this x of type A, the predicate P x holds
  record Σ (A : Set) (P : Pred A) : Set where
    -- In the type P fst, fst refers to a previously introduced field
    constructor _,_
    field
      fst : A
      snd : P fst

  open Σ public

  -- By depending on a boolean we can use pi types to represent product types
  Π-× : Set → Set → Set
  Π-× A B = Π Bool λ where
    true  → A
    false → B

  -- By depending on a boolean we can use sigma types to represent sum types
  Σ-⊎ : Set → Set → Set
  Σ-⊎ A B = Σ Bool λ where
    true  → A
    false → B

  -- Use pi types to recover function types
  Π-→ : Set → Set → Set
  Π-→ A B = Π A λ where
    _     → B

  -- Use sigma types to recover product types
  Σ-× : Set → Set → Set
  Σ-× A B = Σ A λ where
    _     → B

  infix 5 _×_
  _×_ : Set → Set → Set
  _×_ = Σ-×

  -- 1) If we can transform the witness and
  -- 2) transform the predicate as per the transformation on the witness
  -- ⇒) then we can transform a sigma type
  map : (f : A → B) → (∀ {x} → P x → Q (f x)) → (Σ A P → Σ B Q)
  map f g (x , y) = (f x , g y)

  -- The syntax keyword introduces notation that can include binders
  infix 4 Σ-syntax
  Σ-syntax : (A : Set) → (A → Set) → Set
  Σ-syntax = Σ
  syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

  example₁ : Σ ℕ EvenData
  example₁ = 0 , zero

  one-is-not-even : ¬ EvenData 1
  one-is-not-even ()

  example₂ : ¬ Π ℕ EvenData
  example₂ f = one-is-not-even (f 1)

  ¬∘ : Pred A → Pred A
  ¬∘ P = ¬_ ∘ P

  -- These can be proven regardless of A

  ¬∃⇒∀¬ : ¬ (Σ A P) → Π A (¬∘ P)
  ¬∃⇒∀¬ f x px = f (x , px)

  ∃¬⇒¬∀ : Σ A (¬∘ P) → ¬ Π A P
  ∃¬⇒¬∀ (a , ¬pa) f = ¬pa (f a)

  ∀¬⇒¬∃ : Π A (¬∘ P) → ¬ Σ A P
  ∀¬⇒¬∃ f (a , pa) = f a pa

  -- Works in classical, not in constructive mathematics
  postulate ¬∀⇒∃¬ : ¬ Π A P → Σ A (¬∘ P)

  -- Show that ≤ is antisymmetric
  ≤-≡ : n ≤ m → m ≤ n → n ≡ m
  ≤-≡ z≤n z≤n = refl
  ≤-≡ (s≤s x) (s≤s y) = cong suc (≤-≡ x y)

  -- By using n ≤ m instead of Fin m we can mention n in the output
  take : Vec A m → n ≤ m → Vec A n
  take xs z≤n = []
  take (x ∷ xs) (s≤s lte) = x ∷ take xs lte

  Fin-to-≤ : (i : Fin m) → to-ℕ i < m
  Fin-to-≤ zero = s≤s z≤n
  Fin-to-≤ (suc i) = s≤s (Fin-to-≤ i)

  -- Proof combining sigma types and equality
  ≤-to-Fin : n < m → Fin m
  ≤-to-Fin (s≤s z≤n) = zero
  ≤-to-Fin (s≤s (s≤s i)) = suc (≤-to-Fin (s≤s i))

  Fin-≤-inv : (i : Fin m) → ≤-to-Fin (Fin-to-≤ i) ≡ i
  Fin-≤-inv zero = refl
  Fin-≤-inv (suc zero) = refl
  Fin-≤-inv (suc (suc i)) = cong suc (Fin-≤-inv (suc i))

  ≤-Fin-inv : (lt : Σ[ n ∈ ℕ ] n < m)
            → (to-ℕ (≤-to-Fin (snd lt)) , Fin-to-≤ (≤-to-Fin (snd lt))) ≡ lt
  ≤-Fin-inv (.zero , s≤s z≤n) = refl
  ≤-Fin-inv (.(suc _) , s≤s (s≤s i)) =
    cong (map suc s≤s) (≤-Fin-inv (_ , s≤s i))

max_stars_repo_name: poncev/agda-bcam

max_issues_repo_name: poncev/agda-bcam

max_forks_repo_name: poncev/agda-bcam


text:
{-# OPTIONS --two-level --no-sized-types --no-guardedness #-}
module Issue2487.e where

postulate admit : {A : Set} -> A


text:
module Type.Size.Finite where

import      Lvl
open import Functional
open import Logic
open import Logic.Predicate
open import Numeral.Finite
open import Numeral.Finite.Equiv
open import Numeral.Natural
open import Structure.Setoid
open import Type
open import Type.Size

private variable ℓ ℓₑ : Lvl.Level

-- A finitely enumerable type is a type where its inhabitants are finitely enumerable (alternatively: listable, able to collect to a finite list (a list containing all inhabitants is constructible)).
-- There is a finite upper bound on the number of inhabitants in the sense that the inverse of a mapping from a type of finite numbers is a function (TODO: Not sure if the implementation actually states this. Maybe Invertible should be used instead of Surjective?).
-- Also called: Finitely indexed.
FinitelyEnumerable : (T : Type{ℓ}) → ⦃ equiv : Equiv{ℓₑ}(T) ⦄ → Stmt
FinitelyEnumerable(T) = ∃(n ↦ 𝕟(n) ≽ T)

-- A finite type have a finite number of inhabitants, and this number is constructable.
Finite : (T : Type{ℓ}) → ⦃ equiv : Equiv{ℓₑ}(T) ⦄ → Stmt
Finite(T) = ∃(n ↦ 𝕟(n) ≍ T)

-- Cardinality of a finite type in the form of a number. Number of inhabitants of a type.
-- The witness of Finite is the exact number of inhabitants of the type (the count).
#_ : (T : Type{ℓ}) → ⦃ equiv : Equiv{ℓₑ}(T) ⦄ → ⦃ fin : Finite(T) ⦄ → ℕ
#_ _ ⦃ fin = [∃]-intro(n) ⦄ = n

enum : ∀{T : Type{ℓ}} → ⦃ equiv : Equiv{ℓₑ}(T) ⦄ → ⦃ fin : Finite(T) ⦄ → 𝕟(# T) → T
enum ⦃ fin = [∃]-intro _ ⦃ [∃]-intro f ⦄ ⦄ = f

module Finite where
  import      Data.Either as Type
  import      Data.Either.Equiv as Either
  import      Data.Tuple as Type
  import      Data.Tuple.Equiv as Tuple
  open import Numeral.Finite.Sequence
  open import Structure.Function.Domain
  import      Numeral.Natural.Oper as ℕ

  private variable A B : Type{ℓ}
  private variable ⦃ equiv-A ⦄ : Equiv{ℓₑ}(A)
  private variable ⦃ equiv-B ⦄ : Equiv{ℓₑ}(B)
  private variable ⦃ equiv-A‖B ⦄ : Equiv{ℓₑ}(A Type.‖ B)
  private variable ⦃ equiv-A⨯B ⦄ : Equiv{ℓₑ}(A Type.⨯ B)

  _+_ :  ⦃ ext : Either.Extensionality ⦃ equiv-A ⦄ ⦃ equiv-B ⦄ (equiv-A‖B) ⦄ → Finite(A) ⦃ equiv-A ⦄ → Finite(B) ⦃ equiv-B ⦄ → Finite(A Type.‖ B) ⦃ equiv-A‖B ⦄
  _+_ ([∃]-intro a ⦃ [∃]-intro af ⦄) ([∃]-intro b ⦃ [∃]-intro bf ⦄) = [∃]-intro (a ℕ.+ b) ⦃ [∃]-intro (interleave af bf) ⦃ interleave-bijective ⦄ ⦄

  -- TODO: Below
  _⋅_ :  ⦃ ext : Tuple.Extensionality ⦃ equiv-A ⦄ ⦃ equiv-B ⦄ (equiv-A⨯B) ⦄ → Finite(A) ⦃ equiv-A ⦄ → Finite(B) ⦃ equiv-B ⦄ → Finite(A Type.⨯ B) ⦃ equiv-A⨯B ⦄
  _⋅_ ([∃]-intro a ⦃ [∃]-intro af ⦄) ([∃]-intro b ⦃ [∃]-intro bf ⦄) = [∃]-intro (a ℕ.⋅ b) ⦃ [∃]-intro (f af bf) ⦃ p ⦄ ⦄ where
    postulate f : (𝕟(a) → _) → (𝕟(b) → _) → 𝕟(a ℕ.⋅ b) → (_ Type.⨯ _)
    postulate p : Bijective(f af bf)

  {-
  _^_ :  Finite(A) → Finite(B) → Finite(A ← B)
  _^_ ([∃]-intro a ⦃ [∃]-intro af ⦄) ([∃]-intro b ⦃ [∃]-intro bf ⦄) = [∃]-intro (a ℕ.^ b) ⦃ [∃]-intro (f af bf) ⦃ p ⦄ ⦄ where
    postulate f : (𝕟(a) → _) → (𝕟(b) → _) → 𝕟(a ℕ.^ b) → (_ ← _)
    postulate p : Bijective(f af bf)
  -}


text:
module Interior where

open import Basics
open import Ix
open import All
open import Cutting

module INTERIOR {I}(C : I |> I) where

  open _|>_ C

  data Interior (P : I -> Set)(i : I) : Set where
    tile : P i -> Interior P i
    <_>  : Cutting C (Interior P) i -> Interior P i

  ifold : forall {P Q} ->
          [ P -:> Q ] ->
          [ Cutting C Q -:> Q ] ->
          [ Interior P -:> Q ]
  ifolds : forall {P Q} ->
          [ P -:> Q ] ->
          [ Cutting C Q -:> Q ] ->
          [ All (Interior P) -:> All Q ]
  ifold pq cq i (tile p) = pq i p
  ifold pq cq i < c 8>< ps > = cq i (c 8>< ifolds pq cq _ ps)
  ifolds pq cq [] <> = <>
  ifolds pq cq (i ,- is) (x , xs) = ifold pq cq i x , ifolds pq cq is xs

  -- tile : [ P -:> Interior P ]

  extend : forall {P Q} ->
          [ P -:> Interior Q ] ->
          [ Interior P -:> Interior Q ]
  extend k = ifold k (\ i x -> < x >)

  -- and we have a monad, not in Set, but in I -> Set

open INTERIOR NatCut
{-
foo : Interior (\ n -> n == 3) 12
foo = < ((3 , 9 , refl _)) 8>< (tile (refl _) , {!!} , <>) >
-}

max_stars_repo_name: pigworker/InteriorDesign

max_issues_repo_name: pigworker/InteriorDesign

max_forks_repo_name: pigworker/InteriorDesign


text:
-- Andreas, 2021-12-22, issue #5706 reported by Trebor-Huang
-- In Agda <= 2.6.2.1, Int overflow can be exploited.

-- Basically just a modified version of Russell's paradox found at
-- http://liamoc.net/posts/2015-09-10-girards-paradox.html.

-- -- This 64bit Int overflow got us Set:Set.
-- WTF : Set₀
-- WTF = Set₁₈₄₄₆₇₄₄₀₇₃₇₀₉₅₅₁₆₁₅
-- -- 18446744073709551615 = 2^64 - 1

-- Some preliminaries, just to avoid any library imports:

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

record ∃ {A : Set} (P : A → Set) : Set where
    constructor _,_
    field
        proj₁ : A
        proj₂ : P proj₁
open ∃

data ⊥ : Set where

-- The rest follows the linked development of Russell's paradox.

-- Naive sets (tree representation), accepted with --type-in-type.

data SET : Set where
  set : (X : Set₁₈₄₄₆₇₄₄₀₇₃₇₀₉₅₅₁₆₁₅) → (X → SET) → SET

-- Elementhood

_∈_ : SET → SET → Set
a ∈ set X f = ∃ λ x → a ≡ f x

_∉_ : SET → SET → Set
a ∉ b = (a ∈ b) → ⊥

-- The set Δ of sets that do not contain themselves.

Δ : SET
Δ = set (∃ λ s → s ∉ s) proj₁

-- Any member of Δ does not contain itself.

x∈Δ→x∉x : ∀ {X} → X ∈ Δ → X ∉ X
x∈Δ→x∉x ((Y , Y∉Y) , refl) = Y∉Y

-- Δ does not contain itself.

Δ∉Δ : Δ ∉ Δ
Δ∉Δ Δ∈Δ = x∈Δ→x∉x Δ∈Δ Δ∈Δ

-- Any set that does not contain itself lives in Δ.

x∉x→x∈Δ : ∀ {X} →  X ∉ X → X ∈ Δ
x∉x→x∈Δ {X} X∉X = (X , X∉X) , refl

-- So Δ must live in Δ, which is absurd.

falso : ⊥
falso = Δ∉Δ (x∉x→x∈Δ Δ∉Δ)


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

module Categories.Category.Construction.Elements where

-- Category of Elements -- given a functor into Sets, construct the category of elements 'above' each object
-- see https://ncatlab.org/nlab/show/category+of+elements
open import Level
open import Data.Product using (Σ; _,_; Σ-syntax; proj₁; proj₂; map)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong)
open import Function hiding (_∘_) renaming (id to idf)

open import Categories.Category using (Category)
open import Categories.Functor hiding (id)
open import Categories.Category.Instance.Sets
open import Categories.Category.Instance.Cats
open import Categories.Category.Construction.Functors
open import Categories.NaturalTransformation.NaturalIsomorphism hiding (refl; sym; trans)
open import Categories.NaturalTransformation hiding (id)
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e o′ : Level

-- the first, most explicit definition is taken as 'canonical'.
Elements : {C : Category o ℓ e} → Functor C (Sets o′) → Category (o ⊔ o′) (ℓ ⊔ o′) e
Elements {C = C} F = record
  { Obj       = Σ Obj F₀
  ; _⇒_       = λ { (c , x) (c′ , x′) → Σ (c ⇒ c′) (λ f → F₁ f x ≡ x′)  }
  ; _≈_       = λ p q → proj₁ p ≈ proj₁ q
  ; id        = id , identity
  ; _∘_       = λ { (f , Ff≡) (g , Fg≡) → f ∘ g ,  trans homomorphism (trans (cong (F₁ f) Fg≡) Ff≡)}
  ; assoc     = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv     = record { refl = Equiv.refl ; sym = Equiv.sym ; trans = Equiv.trans }
  ; ∘-resp-≈  = ∘-resp-≈
  }
  where
  open Category C
  open Functor F

-- This induces a functor. It is largely uninteresting as it is as close to 'strict'
-- as things get in this setting.
El : {C : Category o ℓ e} → Functor (Functors C (Sets o′)) (Cats (o ⊔ o′) (ℓ ⊔ o′) e)
El {C = C} = record
  { F₀ = Elements
  ; F₁ = λ A⇒B → record
    { F₀ = map idf (η A⇒B _)
    ; F₁ = map idf λ {f} eq → trans (sym $ commute A⇒B f) (cong (η A⇒B _) eq)
    ; identity = Equiv.refl
    ; homomorphism = Equiv.refl
    ; F-resp-≈ = idf
    }
  ; identity = λ {P} → record
    { F⇒G = record
      { η           = λ X → id , identity P
      ; commute     = λ _ → MR.id-comm-sym C
      ; sym-commute = λ _ → MR.id-comm C
      }
    ; F⇐G = record
      { η           = λ X → id , identity P
      ; commute     = λ _ → MR.id-comm-sym C
      ; sym-commute = λ _ → MR.id-comm C
      }
    ; iso = λ X → record { isoˡ = identityˡ ; isoʳ = identityʳ } }
  ; homomorphism = λ {X₁} {Y₁} {Z₁} → record
    { F⇒G = record
      { η           = λ X → id , identity Z₁
      ; commute     = λ _ → MR.id-comm-sym C
      ; sym-commute = λ _ → MR.id-comm C
      }
    ; F⇐G = record
      { η           = λ X → id , identity Z₁
      ; commute     = λ _ → MR.id-comm-sym C
      ; sym-commute = λ _ → MR.id-comm C
      }
    ; iso = λ X → record { isoˡ = identityˡ ; isoʳ = identityʳ }
    }
  ; F-resp-≈ = λ {_} {B₁} f≈g → record
    { F⇒G = record
      { η           = λ _ → id , trans (identity B₁) f≈g
      ; commute     = λ _ → MR.id-comm-sym C
      ; sym-commute = λ _ → MR.id-comm C
      }
    ; F⇐G = record
      { η           = λ _ → id , trans (identity B₁) (sym f≈g)
      ; commute     = λ _ → MR.id-comm-sym C
      ; sym-commute = λ _ → MR.id-comm C
      }
    ; iso = λ X → record { isoˡ = identityˡ ; isoʳ = identityʳ } }
  }
  where
  open Category C
  open Functor
  open NaturalTransformation

-- But there are all sorts of interesting alternate definitions
-- note how this one is WAY less level polymorphic than the above!
-- it looks like it contains more information... but not really either.
{-  Unfinished because it is super tedious and not informative!
module Alternate-Pullback {C : Category (suc o) o o} (F : Functor C (Sets o)) where
  open import Categories.Category.Instance.PointedSets
  open import Categories.Category.Instance.Cats
  open import Categories.Diagram.Pullback (Cats (suc o) o o)
  open import Categories.Category.Product using (_※_; πˡ)
  open Category C
  open Functor F

  Pb : Pullback F Underlying
  Pb = record
    { P = Elements F
    ; p₁ = record
     { F₀ = proj₁
     ; F₁ = proj₁
     ; identity = Equiv.refl
     ; homomorphism = Equiv.refl
     ; F-resp-≈ = idf
     }
    ; p₂ = record
     { F₀ = map F₀ idf
     ; F₁ = map F₁ idf
     ; identity = λ x → identity {_} {x}
     ; homomorphism = λ _ → homomorphism
     ; F-resp-≈ = λ f≈g _ → F-resp-≈ f≈g
     }
    ; commute = record
      { F⇒G = record { η = λ _ → idf ; commute = λ _ → refl }
      ; F⇐G = record { η = λ _ → idf ; commute = λ _ → refl }
      ; iso = λ X → record { isoˡ = refl ; isoʳ = refl }
      }
    ; universal = λ {A} {h₁} {h₂} NI → record
      { F₀ = λ X → Functor.F₀ h₁ X , η (F⇐G NI) X (proj₂ $ Functor.F₀ h₂ X)
      ; F₁ = λ f → Functor.F₁ h₁ f ,
        trans (sym $ commute (F⇐G NI) f) (cong (η (F⇐G NI) _) (proj₂ $ Functor.F₁ h₂ f))
      ; identity = Functor.identity h₁
      ; homomorphism = Functor.homomorphism h₁
      ; F-resp-≈ = Functor.F-resp-≈ h₁
      }
    ; unique = λ πˡ∘i≃h₁ map∘i≃h₂ → record
      { F⇒G = record { η = λ X → {!!} ; commute = {!!} }
      ; F⇐G = record { η = {!!} ; commute = {!!} }
      ; iso = λ X → record { isoˡ = {!!} ; isoʳ = {!!} }
      }
    ; p₁∘universal≈h₁ = {!!}
    ; p₂∘universal≈h₂ = {!!}
    }
    where
    open NaturalTransformation
    open NaturalIsomorphism
-}

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import Base using (Type; Type₀; _==_; idp)

module PathInductionSimplified where

{-<pathinduction>-}
record Coh {i} (A : Type i) : Type i where
  field & : A
open Coh public

instance
  J : ∀ {i j} {A : Type i} {a : A} {B : (a' : A) → a == a' → Type j}
    → Coh (B a idp)
    → Coh ({a' : A} (p : a == a') → B a' p)
  & (J d) idp = & d

  idp-Coh : ∀ {i} {A : Type i} {a : A} → Coh (a == a)
  & idp-Coh = idp

path-induction : ∀ {i} {A : Type i} {{a : A}} → A
path-induction {{a}} = a

composition : ∀ {i} {A : Type i} {a : A}
     → Coh ({b : A} (p : a == b) {c : A} (q : b == c) → a == c)
composition = path-induction

postulate
  A : Type₀
  a b c : A
  p : a == b
  q : b == c

pq : a == c
pq = & composition p q
{-</>-}

max_stars_repo_name: guillaumebrunerie/JamesConstruction

max_issues_repo_name: guillaumebrunerie/JamesConstruction

max_forks_repo_name: guillaumebrunerie/JamesConstruction


text:
open import Data.Bool using (Bool; false; true; _∧_)
open import Data.Maybe
open import Data.Nat
open import Data.Nat.Properties --using (_≟_; _<?_)
open import Data.Product
open import Relation.Binary.PropositionalEquality --using (_≡_; refl)
open import Relation.Nullary --using (Dec; yes; no)
--open import Relation.Nullary.Decidable --using (from-yes)

_ : Dec (0 ≡ 2)
_ = no (λ())
--_ = 0 ≟ 2
--_ = 0 ≟ 3

_ : Dec (2 ≡ 2)
_ = yes refl

fun : ℕ → ℕ → Maybe ℕ
fun x y with x <? y
... | yes _ = nothing
... | no _  = just y

_ : fun 3 5 ≡ nothing
_ = refl

_ : fun 3 2 ≡ just 2
_ = refl

--prop-:S : ∀ (x y)
--        → fun x y ≡ nothing
--        → x < y
--prop-:S 0 0 ()
--prop-:S 0 (suc y) refl = s≤s z≤n
--prop-:S (suc x) 0 ()
--prop-:S (suc x) (suc y) funsxsy≡nothing = s≤s (prop-:S x y ?)

--prop : ∀ (x y)
--     → fun x y ≡ nothing
--     → x < y
--prop x y with fun x y
--... | just _  = λ()
--... | nothing = λ{refl → ?} -- from-yes (x <? y)}
--
---- This fails because the pattern matching is incomplete,
---- but it shouldn't. There are no other cases
--prop' : ∀ (x y)
--      → fun x y ≡ nothing
--      → x < y
--prop' x y with fun x y | x <? y
--... | nothing | yes x<y = λ{refl → x<y}
--... | just _  | no _    = λ()
--... | _ | _ = ?

-- From: https://stackoverflow.com/a/63119870/1744344
prop : ∀ x y → fun x y ≡ nothing → x < y
prop x y with x <? y
... | yes p = λ _ → p

prop-old : ∀ x y → fun x y ≡ nothing → x < y
prop-old x y _ with x <? y
prop-old _ _ refl | yes p = p
prop-old _ _ () | no _

data Comp : Set where
  greater equal less : Comp

compare' : ℕ → ℕ → Comp
compare' x y with x <ᵇ y
...          | false with y <ᵇ x
...                  | false = equal
...                  | true  = greater
compare' x y | true = less

--fun2 : Maybe (ℕ × ℕ) → Maybe ℕ
--fun2 pair with pair
--... | just (x , y) with x <? y
--... | just (x , y) | yes _ = nothing
--... | just (x , y) | no _  = just y
--fun2 _ | nothing = nothing

prop-comp : ∀ x y
          → compare' x y ≡ greater
          → (y <ᵇ x) ≡ true
prop-comp x y _ with x <ᵇ y
... | false with y <ᵇ x
...         | true = refl
--same as
--prop-comp x y _ | false with y <ᵇ x
--prop-comp x y _ | false | true = refl

prop-comp← : ∀ x y
           → (y <ᵇ x) ≡ true
           → compare' x y ≡ greater
prop-comp← x y _ with x <ᵇ y
prop-comp← x y _  | true  with y <ᵇ x
prop-comp← _ _ _  | true | true = ?  -- This impossible!
prop-comp← _ _ () | true | false
prop-comp← x y _  | false with y <ᵇ x
prop-comp← _ _ _  | false | true = refl
--prop-comp← x y () | false | false

prop-new← : ∀ x y
           → (x <ᵇ y) ≡ false
           → (y <ᵇ x) ≡ false
           → compare' x y ≡ equal
--Why is this not possible?
--prop-new← x y _ with x <ᵇ y | y <ᵇ x
--... | false | false = refl
prop-new← x y _ _ with x <ᵇ y
... | false with y <ᵇ x
...   | false = refl

--a : inspect 3 2
--a = ?


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

open import library.Basics hiding (Type ; Σ ; S)
open import library.types.Sigma
open import library.types.Bool

open import Sec2preliminaries
open import Sec3hedberg
open import Sec4hasConstToSplit
open import Sec5factorConst
open import Sec6populatedness

module Sec7taboos where

-- Subsection 7.1

-- Lemma 7.1
hasConst-family-dec : {X : Type} → (x₁ x₂ : X) → ((x : X) → hasConst ((x₁ == x) + (x₂ == x))) → (x₁ == x₂) + ¬(x₁ == x₂)
hasConst-family-dec {X} x₁ x₂ hasConst-fam = solution where
  f₋ : (x : X) → (x₁ == x) + (x₂ == x) → (x₁ == x) + (x₂ == x)
  f₋ x = fst (hasConst-fam x)

  E₋ : X → Type
  E₋ x = fix (f₋ x)

  E : Type
  E = Σ X λ x → (E₋ x)

  E-fst-determines-eq : (e₁ e₂ : E) → (fst e₁ == fst e₂) → e₁ == e₂
  E-fst-determines-eq e₁ e₂ p = second-comp-triv (λ x → fixed-point (f₋ x) (snd (hasConst-fam x))) _ _ p

  r : Bool → E
  r true = x₁ , to-fix (f₋ x₁) (snd (hasConst-fam x₁)) (inl idp)
  r false = x₂ , to-fix (f₋ x₂) (snd (hasConst-fam x₂)) (inr idp)

  about-r : (r true == r false) ↔ (x₁ == x₂)
  about-r = (λ p → ap fst p) , (λ p → E-fst-determines-eq _ _ p)

  s : E → Bool
  s (_ , inl _ , _) = true
  s (_ , inr _ , _) = false

  s-section-of-r : (e : E) → r(s e) == e
  s-section-of-r (x , inl p , q) = E-fst-determines-eq _ _ p
  s-section-of-r (x , inr p , q) = E-fst-determines-eq _ _ p

  about-s : (e₁ e₂ : E) → (s e₁ == s e₂) ↔ (e₁ == e₂)
  about-s e₁ e₂ = one , two where
    one : (s e₁ == s e₂) → (e₁ == e₂)
    one p =
      e₁       =⟨ ! (s-section-of-r e₁) ⟩
      r(s(e₁)) =⟨ ap r p ⟩
      r(s(e₂)) =⟨ s-section-of-r e₂ ⟩
      e₂       ∎
    two : (e₁ == e₂) → (s e₁ == s e₂)
    two p = ap s p

  combine : (s (r true) == s (r false)) ↔ (x₁ == x₂)
  combine = (about-s _ _) ◎ about-r

  check-bool : (s (r true) == s (r false)) + ¬(s (r true) == s (r false))
  check-bool = Bool-has-dec-eq _ _

  solution : (x₁ == x₂) + ¬(x₁ == x₂)
  solution with check-bool
  solution | inl p = inl (fst combine p)
  solution | inr np = inr (λ p → np (snd combine p))

-- The assumption that we are discussing:
all-hasConst : Type₁
all-hasConst = (X : Type) → hasConst X

-- Theorem 7.2
all-hasConst→dec-eq : all-hasConst → (X : Type) → has-dec-eq X
all-hasConst→dec-eq ahc X x₁ x₂ = hasConst-family-dec x₁ x₂ (λ x → ahc _)

-- Theorem 7.3
module functional-subrelation (ac : all-hasConst) (X : Type) (R : X × X → Type) where

  all-sets : (Y : Type) → is-set Y
  all-sets Y = pathHasConst→isSet (λ y₁ y₂ → ac _)

  R₋ : (x : X) → Type
  R₋ x = Σ X λ y → R(x , y)

  k : (x : X) → (R₋ x) → (R₋ x)
  k x = fst (ac _)

  kc : (x : X) → const (k x)
  kc x = snd (ac _)

  S : X × X → Type
  S (x , y) = Σ (R(x , y)) λ a →
                (y , a) == k x (y , a)

  -- the relation S
  S₋ : (x : X) → Type
  S₋ x = Σ X λ y → S(x , y)

  -- fix kₓ is equivalent to Sₓ
  -- This is just Σ-assoc. We try to make it more readable by adding some (trivial) steps.
  fixk-S : (x : X) → (fix (k x)) ≃ S₋ x
  fixk-S x =
      (fix (k x))                                           ≃⟨ ide _ ⟩
      (Σ (Σ X λ y → R(x , y)) λ a → a == k x a)             ≃⟨ Σ-assoc ⟩
      (Σ X λ y → Σ (R(x , y)) λ r → (y , r) == k x (y , r)) ≃⟨ ide _ ⟩
      (S₋ x)                                                ≃∎

  -- claim (0)
  subrelation : (x y : X) → S(x , y) →  R(x , y)
  subrelation x y (r , _) = r

   -- claim (1)
  prop-Sx : (x : X) → is-prop (S₋ x)
  prop-Sx x = equiv-preserves-level {A = fix (k x)} {B = (S₋ x)} (fixk-S x) (fixed-point _ (kc x))

  -- claim (2)
  same-domain : (x : X) → (R₋ x) ↔ (S₋ x)
  same-domain x = rs , sr where
    rs : (R₋ x) → (S₋ x)
    rs a = –> (fixk-S x) (to-fix (k x) (kc x) a)
    sr : (S₋ x) → (R₋ x)
    sr (y , r , _) = y , r

  -- claim (3)
  prop-S : (x y : X) → is-prop (S (x , y))
  prop-S x y = all-paths-is-prop all-paths where
    all-paths : (s₁ s₂ : S(x , y)) → s₁ == s₂
    all-paths s₁ s₂ = ss where

      yss : (y , s₁) == (y , s₂)
      yss = prop-has-all-paths (prop-Sx x) _ _

      ss : s₁ == s₂
      ss = set-lemma (all-sets _) y s₁ s₂ yss

-- intermediate definition
-- see the caveat about the notion 'epimorphism' in the article
is-split-epimorphism : {U V : Type} → (U → V) → Type
is-split-epimorphism {U} {V} e = Σ (V → U) λ s → (v : V) → e (s v) == v

is-epimorphism : {U V : Type} → (U → V) → Type₁
is-epimorphism {U} {V} e = (W : Type) → (f g : V → W) → ((u : U) → f (e u) == g (e u)) → (v : V) → f v == g v

-- Lemma 7.4
path-trunc-epi→set : {Y : Type} → ((y₁ y₂ : Y) → is-epimorphism (∣_∣ {X = y₁ == y₂})) → is-set Y
path-trunc-epi→set {Y} path-epi = reminder special-case where

  f : (y₁ y₂ : Y) → Trunc (y₁ == y₂) → Y
  f y₁ _ _ = y₁

  g : (y₁ y₂ : Y) → Trunc (y₁ == y₂) → Y
  g _ y₂ _ = y₂

  special-case : (y₁ y₂ : Y) → Trunc (y₁ == y₂) → y₁ == y₂
  special-case y₁ y₂ = path-epi y₁ y₂ Y (f y₁ y₂) (g y₁ y₂) (idf _)

  reminder : hseparated Y → is-set Y
  reminder = fst set-characterizations ∘ snd (snd set-characterizations)

-- Theorem 7.5 (1)
all-split→all-deceq : ((X : Type) → is-split-epimorphism (∣_∣ {X = X})) → (X : Type) → has-dec-eq X
all-split→all-deceq all-split = all-hasConst→dec-eq ac where
  ac : (X : Type) → hasConst X
  ac X = snd hasConst↔splitSup (fst (all-split X))

-- Theorem 7.5 (2)
all-epi→all-set : ((X : Type) → is-epimorphism (∣_∣ {X = X})) → (X : Type) → is-set X
all-epi→all-set all-epi X = path-trunc-epi→set (λ y₁ y₂ → all-epi (y₁ == y₂))

-- Subsection 7.2

-- Lemma 7.6, first proof
pop-splitSup-1 : {X : Type} → Pop (splitSup X)
pop-splitSup-1 {X} f c = to-fix f c (hasConst→splitSup (g , gc)) where

  g : X → X
  g x = f (λ _ → x) ∣ x ∣

  gc : const g
  gc x₁ x₂ =
    g x₁               =⟨ idp ⟩
    f (λ _ → x₁) ∣ x₁ ∣ =⟨ ap (λ k → k ∣ x₁ ∣) (c (λ _ → x₁) (λ _ → x₂)) ⟩
    f (λ _ → x₂) ∣ x₁ ∣ =⟨ ap (f (λ _ → x₂)) (prop-has-all-paths (h-tr X) ∣ x₁ ∣ ∣ x₂ ∣) ⟩
    f (λ _ → x₂) ∣ x₂ ∣ =⟨ idp ⟩
    g x₂               ∎

-- Lemma 7.6, second proof
pop-splitSup-2 : {X : Type} → Pop (splitSup X)
pop-splitSup-2 {X} = snd (pop-alt₂ {splitSup X}) get-P where
  get-P : (P : Type) → is-prop P → splitSup X ↔ P → P
  get-P P pp (hstp , phst) = hstp free-hst where

    xp : X → P
    xp x = hstp (λ _ → x)

    zp : Trunc X → P
    zp = rec pp xp

    free-hst : splitSup X
    free-hst z = phst (zp z) z

-- Lemma 7.6, third proof
pop-splitSup-3 : {X : Type} → Pop (splitSup X)
pop-splitSup-3 {X} = snd pop-alt translation where

  translation-aux : splitSup (splitSup X) → splitSup X
  translation-aux = λ hsthst z → hsthst (trunc-functorial {X = X} {Y = splitSup X} (λ x _ → x) z) z

  translation : Trunc (splitSup (splitSup X)) → Trunc (splitSup X)
  translation = trunc-functorial translation-aux

-- Theorem 7.7
module thm77 where

  One = (X : Type) → Pop X → Trunc X

  Two = (X : Type) → Trunc (splitSup X)

  Three = (P : Type) → is-prop P → (Y : P → Type) → ((p : P) → Trunc (Y p)) → Trunc ((p : P) → Y p)

  Four = (X Y : Type) → (X → Y) → (Pop X → Pop Y)

  One→Two : One → Two
  One→Two poptr X = poptr (splitSup X) pop-splitSup-1

  Two→One : Two → One
  Two→One trhst X pop = fst pop-alt pop (trhst X)

  One→Four : One → Four
  One→Four poptr X Y f = Trunc→Pop ∘ (trunc-functorial f) ∘ (poptr X)

  Four→One : Four → One
  Four→One funct X px = snd (prop→hasConst×PopX→X (h-tr _)) pz where
    pz : Pop (Trunc X)
    pz  =  funct X (Trunc X) ∣_∣ px

  -- only very slightly different to the proof in the article
  One→Three : One → Three
  One→Three poptr P pp Y = λ py → poptr _ (snd pop-alt' (λ hst p₀ → hst (contr-trick p₀ py) p₀)) where
    contr-trick : (p₀ : P) → ((p : P) → Trunc (Y p)) → Trunc ((p : P) → Y p)
    contr-trick p₀ py = rec {X = Y p₀}
                            {P = Trunc ((p : P) → Y p)}
                            (h-tr _)
                            (λ y₀ → ∣ <– (thm55aux.neutral-contr-exp {P = P} {Y = Y} pp p₀) y₀ ∣) (py p₀)

  Three→Two : Three → Two
  Three→Two proj X = proj (Trunc X) (h-tr _) (λ _ → X) (idf _)

-- Subsection 7.3

-- Some very simple lemmata

-- If P is a proposition, so is P + ¬ P
dec-is-prop : {P : Type} → (Funext {X = P} {Y = Empty}) → is-prop P → is-prop (P + ¬ P)
dec-is-prop {P} fext pp = all-paths-is-prop (λ { (inl p₁) (inl p₂) → ap inl (prop-has-all-paths pp _ _) ;
                                (inl p₁) (inr np₂) → Empty-elim {A = λ _ → inl p₁ == inr np₂} (np₂ p₁) ;
                                (inr np₁) (inl p₂) → Empty-elim {A = λ _ → inr np₁ == inl p₂} (np₁ p₂) ;
                                (inr np₁) (inr np₂) → ap inr (fext np₁ np₂ (λ p → prop-has-all-paths (λ ()) _ _)) })

-- Theorem 7.8
nonempty-pop→lem : ((X : Type) → Funext {X} {Empty})
                         → ((X : Type) → (¬(¬ X) → Pop X)) → LEM
nonempty-pop→lem fext nn-pop P pp = from-fix {X = dec} (idf _) (nn-pop dec nndec (idf _) idc) where
  dec : Type
  dec = P + ¬ P

  idc : const (idf dec)
  idc = λ _ _ → prop-has-all-paths (dec-is-prop {P} (fext P) pp) _ _

  nndec : ¬(¬ dec)
  nndec ndec = (λ np → ndec (inr np)) λ p → ndec (inl p)

-- Corollary 7.9
nonempty-pop↔lem : ((X : Type) → Funext {X} {Empty})
                         → ((X : Type) → (¬(¬ X) → Pop X)) ↔₁₁ LEM
nonempty-pop↔lem fext = nonempty-pop→lem fext , other where
  other : LEM → ((X : Type) → (¬(¬ X) → Pop X))
  other lem X nnX = p where
    pnp : Pop X + ¬ (Pop X)
    pnp = lem (Pop X) pop-property₂

    p : Pop X
    p = match pnp withl idf _ withr (λ np → Empty-elim {A = λ _ → Pop X} (nnX (λ x → np (pop-property₁ x))))

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- Andreas, 2017-08-23, issue #2712
--
-- GHC Pragmas like LANGUAGE have to appear at the top of the Haskell file.

{-# OPTIONS --no-main #-}  -- Recognized as pragma option since #2714

module Issue2712 where

{-# FOREIGN GHC {-# LANGUAGE TupleSections #-} #-}

postulate
  Pair : (A B : Set) → Set
  pair : {A B : Set} → A → B → Pair A B

{-# COMPILE GHC Pair = type (,)            #-}
{-# COMPILE GHC pair = \ _ _ a b -> (a,) b #-}  -- Test the availability of TupleSections

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2016-02-02, issues 480, 1159, 1811

data Unit : Set where
  unit : Unit

-- To make it harder for Agda, we make constructor unit ambiguous.
data Ambiguous : Set where
  unit : Ambiguous

postulate
  f : ∀{A : Set} → (A → A) → A

test : Unit
test = f \{ unit → unit }

-- Extended lambda checking should be postponed until
-- type A has been instantiated to Unit.

-- Should succeed.


text:
-- The sole purpose of this module is to ease compilation of everything.
module Everything where

import Generic
import Structures
import Instances
import FinMap
import CheckInsert
import GetTypes
import FreeTheorems
import BFF
import Bidir
import LiftGet
import Precond
import Examples
import BFFPlug

max_stars_repo_name: jvoigtlaender/bidiragda

max_issues_repo_name: jvoigtlaender/bidiragda

max_forks_repo_name: jvoigtlaender/bidiragda


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Library.Relation.Binary.Equality.Decidable where

open import Light.Library.Relation using (Base)
open import Light.Library.Relation.Binary.Equality using (Equality)
open import Light.Level using (Setω)
import Light.Library.Relation.Decidable as Decidable
open import Light.Package using (Package)
open import Light.Variable.Levels

record DecidableEquality (𝕒 : Set aℓ) (𝕓 : Set aℓ) : Setω where
      constructor wrap
      field ⦃ decidable‐package ⦄ : Package record { Decidable }
      field ⦃ equals ⦄ : Equality 𝕒 𝕓

DecidableSelfEquality : ∀ (𝕒 : Set aℓ) → Setω
DecidableSelfEquality 𝕒 = DecidableEquality 𝕒 𝕒

open DecidableEquality ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
{-# OPTIONS --type-in-type #-}

module z where

{-
Generic Programming with Dependent Types
Stephanie Weirich and Chris Casinghino, University of Pennsylvania, {sweirich,ccasin}@cis.upenn.edu

ccasin@cis.upenn.edu

2010 : https://www.seas.upenn.edu/~sweirich/papers/aritygen.pdf
2012 : https://www.cis.upenn.edu/~sweirich/papers/ssgip-journal.pdf

------------------------------------------------------------------------------
-- Abstract and Intro

2 types of genericity
- datatype
  - operate on type structure of data
  - so no need to define for each new type
- arity
  - enables functions to be applied to a variable number of args.

e.g., generalize arity of map
repeat   :: a               → [a]
map      :: (a → b)         → [a] → [b]
zipWith  :: (a → b → c)     → [a] → [b] → [c]
zipWith3 :: (a → b → c → d) → [a] → [b] → [c] → [d]

code        : http://www.seas.upenn.edu/~sweirich/papers/aritygen-lncs.tar.gz
tested with : Agda version 2.2.10

------------------------------------------------------------------------------
2 SIMPLE TYPE-GENERIC PROGRAMMING IN AGDA

using Agda with flags (which implies cannot do proofs)
{-# OPTIONS --type-in-type #-}
–no-termination-check
{-# OPTIONS --no-positivity-check #-}
-}

data Bool : Set where
  true  : Bool
  false : Bool

¬ : Bool → Bool
¬ true = false
¬ false = true

_∧_ : Bool → Bool → Bool
true ∧ true = true
_    ∧ _    = false

if_then_else : ∀ {A : Set} → Bool → A → A → A
if true  then a1 else a2 = a1
if false then a1 else a2 = a2

data ℕ : Set where
  zero :     ℕ
  suc  : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

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

data List (A : Set) : Set where
  []   :              List A
  _::_ : A → List A → List A
infixr 5 _::_ -- https://agda.github.io/agda-stdlib/Data.Vec.Functional.html

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

data Vec (A : Set) : ℕ → Set where
  [] : Vec A zero
  _::_ : ∀ {n} → A → (Vec A n) → Vec A (suc n)

repeat : ∀ {n} {A} → A → Vec A n
repeat {zero}  x = []
repeat {suc n} x = x :: repeat x

------------------------------------------------------------------------------
-- 2.1 BASIC TYPE-GENERIC PROGRAMMING

eq-bool : Bool → Bool → Bool
eq-bool true  true  = true
eq-bool false false = true
eq-bool _     _     = false

eq-nat : ℕ → ℕ → Bool
eq-nat  zero    zero   = true
eq-nat (suc n) (suc m) = eq-nat n m
eq-nat      _       _  = false

{-
Structural equality functions, like above, motivate type-generic programming:
- enables defining functions that observe and use structure of types

In a dependently typed language, type-generic is accomplished using universes [17, 21].

E.G., universe of natural number, boolean and product types
-}

-- datatype 'Type', called a "universe"
data Type : Set where
  TNat  :               Type
  TBool :               Type
  TProd : Type → Type → Type

open import Data.Product

-- define an interpretation function '⟨_⟩'
-- maps elements of this universe to Agda types
⟨_⟩ : Type → Set
⟨ TNat ⟩        = ℕ
⟨ TBool ⟩       = Bool
⟨ TProd t1 t2 ⟩ = ⟨ t1 ⟩ × ⟨ t2 ⟩

geq : (t : Type) → ⟨ t ⟩ → ⟨ t ⟩ → Bool
geq TNat  n1 n2 = eq-nat  n1 n2
geq TBool b1 b2 = eq-bool b1 b2
geq (TProd a b) (a1 , b1) (a2 , b2) = geq a a1 a2 ∧ geq b b1 b2

geqEx : Bool
geqEx = geq (TProd TNat TBool) (1 , false) (1 , false)

{-
------------------------------------------------------------------------------
-- 3 ARITY-GENERIC PROGRAMMING : generalize over number of arguments

e.g., map-like (above), +, foldl, foldr

e.g., generalize following functions into one definition : maps for vectors
-}

-- infix zipping application, pronounced “zap” for “zip with apply”
_⊗_ : {A B : Set} {n : ℕ} → Vec (A → B) n → Vec A n → Vec B n
[] ⊗ [] = []
(a :: As) ⊗ (b :: Bs) = a b :: As ⊗ Bs
infixl 40 _⊗_

map0 : {m : ℕ} {A     : Set} →  A          →                     Vec A m
map0         = repeat

map1 : {m : ℕ} {A B   : Set} → (A → B)     → Vec A m →           Vec B m
map1 f x     = repeat f ⊗ x

map2 : {m : ℕ} {A B C : Set} → (A → B → C) → Vec A m → Vec B m → Vec C m
map2 f x1 x2 = repeat f ⊗ x1 ⊗ x2

{-
Intuitively, each map defined by a application of repeat and n copies of _⊗_.
nvec-map f n v1 v2 ... vn = repeat f ⊗ v1 ⊗ v2 ⊗ ... ⊗ vn

-- recursion on n in accumulator style
-- after repeating f :  have a vector of functions
-- then zap this vector across n argument vectors
-- NEEDS type declaration - given below (in Arity section)
nvec-map n f = g n (repeat f)
 where
  g0 a = a
  g (suc n) f = (λ a → g n (f ⊗ a))

--------------------------------------------------
3.1 Typing Arity-Generic Vector Map

arity-generic map : instances have different types

Given arity n, generate corresponding type in the sequence

Part of the difficulty is that generic function is curried in both its type and term args.

This subsection starts with an initial def that takes
- all of the type args in a vector,
- curries term arguments

next subsection, shows how to uncurry type args

ℕ for arity

store types in vector of Agda types, Bool :: N :: [].

vector has type Vec Set 2, so can use standard vector operations (such as _⊗_)

(given in OPTIONS at top of file)
--type-in-type : gives Set the type Set
- simplifies presentation by hiding Agda’s infinite hierarchy of Set levels
- at cost of making Agda’s logic inconsistent
-}

-- folds arrow type constructor (→) over vector of types
-- used to construct the type of 1sr arg to nvec-map
arrTy : {n : ℕ} → Vec Set (suc n) → Set
arrTy {0} (A :: []) = A
arrTy {suc n} (A :: As) = A → arrTy As

arrTyTest : Set
arrTyTest = arrTy (ℕ :: ℕ :: Bool :: [])
-- C-c C-n arrTyTest
-- ℕ → ℕ → Bool

-- Constructs result type of arity-generic map for vectors.
-- Map Vec constructor onto the vector of types, then placing arrows between them.
-- There are two indices:
-- - n : number of types (the arity)
-- - m : length of vectors to be mapped over
arrTyVec : {n : ℕ} → ℕ → Vec Set (suc n) → Set
arrTyVec m As = arrTy (repeat (λ A → Vec A m) ⊗ As)

{- alternate type sigs of previous mapN examples:
map0' : {m : ℕ} {A     : Set} → arrTy (A :: [])           → arrTyVec m (A :: [])
map1' : {m : ℕ} {A B   : Set} → arrTy (A :: B :: [])      → arrTyVec m (A :: B :: [])
map2' : {m : ℕ} {A B C : Set} → arrTy (A :: B :: C :: []) → arrTyVec m (A :: B :: C :: [])
-}

nvec-map : {m : ℕ}
         → (n : ℕ) → {As : Vec Set (suc n)}
         → arrTy As → arrTyVec m As
nvec-map n f = g n (repeat f)
 where
  g : {m : ℕ}
    → (n : ℕ) → {As : Vec Set (suc n)}
    → Vec (arrTy As) m → arrTyVec m As
  g      0  {A :: []} a = a
  g (suc n) {A :: As} f = (λ a → g n (f ⊗ a))

nvec-map-Test : Vec ℕ 2 -- 11 :: 15 :: []
nvec-map-Test = nvec-map 1 { ℕ :: ℕ :: [] } (λ x → 10 + x) (1 :: 5 :: [])

{-
annoying : must explicitly supply types
next section : enable inference

--------------------------------------------------
3.2 A Curried Vector Map

Curry type args so they are supplied individually (rather than a ector).
Enables inference (usually).
-}

-- quantify : creates curried version of a type which depends on a vector
∀⇒ : {n : ℕ} {A : Set} → (Vec A n → Set)
   → Set
∀⇒ {zero}       B = B []
∀⇒ {suc n} {A}  B = (a : A) → ∀⇒ {n} (λ as → B (a :: as))

-- curry : creates curried version of a corresponding function term
λ⇒ : {n : ℕ} {A : Set} {B : Vec A n → Set}
   → ((X : Vec A n) → B X)
   → (∀⇒ B)
λ⇒ {zero}       f = f []
λ⇒ {suc n} {A}  f = (λ a → λ⇒ {n} (λ as → f (a :: as))) -- **** HERE
-- 'a' is implicit in paper
-- Victor says 'hidden' lambdas are magic.
-- see: Eliminating the problems of hidden-lambda insertion
--      https://www.cse.chalmers.se/~abela/MScThesisJohanssonLloyd.pdf

-- uncurry (from 2010 paper)
/⇒ : (n : ℕ) → {K : Set} {B : Vec K n → Set}
   → (∀⇒ B)
   → (A : Vec K n)
   → B A
/⇒ (zero)  f       []  = f
/⇒ (suc n) f (a :: as) = /⇒ n (f a) as

-- arity-generic map
nmap : {m : ℕ}
     → (n : ℕ) -- specifies arity
     → ∀⇒ (λ (As : Vec Set (suc n)) → arrTy As → arrTyVec m As)
nmap {m} n = λ⇒ (λ As → nvec-map {m} n {As})

{-
nmap 1
has type
{m : N} → {A B : Set} → (A → B) → (Vec A m) → (Vec B m)
C-c C-d
(a a₁ : Set) → (a → a₁) → arrTyVec _m_193 (a :: a₁ :: [])

nmap 1 (λ x → 10 + x) (10 :: 5 :: [])
evaluates to
11 :: 15 :: []
C-c C-d
(x : ℕ) → ℕ !=< Set
when checking that the expression λ x → 10 + x has type Set

nmap 2
has type
{m : N} → {ABC : Set} → (A → B → C) → Vec A m → Vec B m → Vec C m
C-c C-d
(a a₁ a₂ : Set) → (a → a₁ → a₂) → arrTyVec _m_193 (a :: a₁ :: a₂ :: [])

nmap 2 ( , ) (1 :: 2 :: 3 :: []) (4 :: 5 :: 6 :: [])
evaluates to
(1 , 4) :: (2 , 5) :: (3 , 6) :: []

now : do not need to explicitly specify type of data in vectors
-}

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

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

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


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Implementation.Standard.Data.Empty where

open import Light.Library.Data.Empty using (Library ; Dependencies)

instance dependencies : Dependencies
dependencies = record {}

instance library : Library dependencies
library = record { Implementation }
      where
      module Implementation where
            open import Data.Empty using () renaming (⊥ to Empty ; ⊥-elim to eliminate) public


text:
module Tactic.Nat.Induction where

open import Prelude

nat-induction : (P : Nat → Set) → P 0 → (∀ n → P n → P (suc n)) → ∀ n → P n
nat-induction P base step  zero   = base
nat-induction P base step (suc n) = step n (nat-induction P base step n)

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
open import Agda.Primitive using (lzero; lsuc; _⊔_ ;Level)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; setoid; cong; trans)
import Function.Equality
open import Relation.Binary using (Setoid)

import Categories.Category
import Categories.Functor
import Categories.Category.Instance.Setoids
import Categories.Monad.Relative
import Categories.Category.Equivalence
import Categories.Category.Cocartesian
import Categories.Category.Construction.Functors
import Categories.NaturalTransformation.Equivalence
import Relation.Binary.Core

import SecondOrder.Arity
import SecondOrder.Signature
import SecondOrder.Metavariable
import SecondOrder.VRenaming
import SecondOrder.MRenaming
import SecondOrder.Term
import SecondOrder.IndexedCategory
import SecondOrder.RelativeKleisli
import SecondOrder.Substitution

module SecondOrder.VRelativeMonad
  {ℓ}
  {𝔸 : SecondOrder.Arity.Arity}
  (Σ : SecondOrder.Signature.Signature ℓ 𝔸)
  where

  open SecondOrder.Signature.Signature Σ
  open SecondOrder.Metavariable Σ
  open SecondOrder.Term Σ
  open SecondOrder.VRenaming Σ
  open SecondOrder.MRenaming Σ
  open SecondOrder.Substitution Σ

  -- TERMS FORM A RELATIVE MONAD
  -- (FOR A FUNCTOR WHOSE DOMAIN IS THE
  -- CATEGORY OF VARIABLE CONTEXTS AND RENAMINGS)

  module _ where
    open Categories.Category
    open Categories.Functor using (Functor)
    open Categories.Category.Instance.Setoids
    open import SecondOrder.IndexedCategory

    -- The embedding of contexts into setoids indexed by sorts
    -- (seen as a "variable" functor)

    Jⱽ : Functor VContexts (IndexedCategory sort (Setoids ℓ ℓ))
    Jⱽ = slots

  -- The relative monad over Jⱽ

  module _ {Θ : MContext} where
    open Categories.Category
    open Categories.Functor using (Functor)
    open Categories.Category.Instance.Setoids
    open Categories.Category.Category (Setoids ℓ ℓ)
    open Categories.Monad.Relative
    open Function.Equality using () renaming (setoid to Π-setoid)
    open Categories.Category.Equivalence using (StrongEquivalence)
    open import SecondOrder.IndexedCategory
    open import SecondOrder.RelativeKleisli
    open Function.Equality using (_⟨$⟩_) renaming (cong to func-cong)
    open import Relation.Binary.Reasoning.MultiSetoid

    to-σ  : ∀ {Γ Δ} → (IndexedCategory sort (Setoids ℓ ℓ) Category.⇒ Functor.₀ Jⱽ Γ) (λ A → Term-setoid Θ Δ A) → (Θ ⊕ Γ ⇒ˢ Δ)
    to-σ ℱ {A} x = ℱ A ⟨$⟩ x

    VMonad : Monad Jⱽ
    VMonad = record
               { F₀ = λ Γ A → Term-setoid Θ Γ A
               ; unit = λ A →
                          record
                            { _⟨$⟩_ = λ x → tm-var x
                            ; cong = λ ξ → ≈-≡ (σ-resp-≡ {σ = tm-var} ξ) }
               ; extend = λ ℱ A →
                            record
                              { _⟨$⟩_ = [ to-σ ℱ ]ˢ_
                              ; cong = λ ξ → []ˢ-resp-≈ (λ {B} z → ℱ B ⟨$⟩ z) ξ }
               ; identityʳ = λ {Γ} {Δ} {ℱ} A {x} {y} ξ → func-cong (ℱ A) ξ
               ; identityˡ = λ A ξ → ≈-trans [idˢ] ξ
               ; assoc = λ {Γ} {Δ} {Ξ} {k} {l} A {x} {y} ξ →
                           begin⟨ Term-setoid Θ _ _ ⟩
                             ( ([ (λ {B} r → [ (λ {A = B} z → l B ⟨$⟩ z) ]ˢ (k B ⟨$⟩ r)) ]ˢ x) ) ≈⟨ []ˢ-resp-≈ ((λ {B} r → [ (λ {A = B} z → l B ⟨$⟩ z) ]ˢ (k B ⟨$⟩ r))) ξ ⟩
                             ([ (λ {B} r → [ (λ {A = A₁} z → l A₁ ⟨$⟩ z) ]ˢ (k B ⟨$⟩ r)) ]ˢ y) ≈⟨ [∘ˢ] y ⟩
                             (([ (λ {B} z → l B ⟨$⟩ z) ]ˢ ([ (λ {B} z → k B ⟨$⟩ z) ]ˢ y))) ∎
               ; extend-≈ = λ {Γ} {Δ} {k} {h} ξˢ A {x} {y} ξ →
                           begin⟨ Term-setoid Θ _ _ ⟩
                             ([ (λ {B} z → k B ⟨$⟩ z) ]ˢ x) ≈⟨ []ˢ-resp-≈ ((λ {B} z → k B ⟨$⟩ z)) ξ ⟩
                             ([ (λ {B} z → k B ⟨$⟩ z) ]ˢ y) ≈⟨ []ˢ-resp-≈ˢ y (λ {B} z → ξˢ B refl) ⟩
                             ([ (λ {B} z → h B ⟨$⟩ z) ]ˢ y) ∎
               }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: cilinder/formaltt

max_forks_repo_name: cilinder/formaltt