text:
module Dual where

open import Prelude using (flip)
open import Logic.Equivalence
open import Category

_op : Cat -> Cat
ℂ@(cat _ _ _ _ _ _ _ _ _) op = cat Obj
	   (\A B -> B ─→ A)
	    id
	   (\{_}{_}{_} -> flip _∘_)
	   (\{_}{_} -> Eq)
	   (\{_}{_}{_}{_}{_}{_}{_} -> flip cong)
	   (\{_}{_}{_} -> idR)
	   (\{_}{_}{_} -> idL)
	   (\{_}{_}{_}{_}{_}{_}{_} -> sym assoc)
  where open module C = Cat ℂ

{-
open Poly-Cat

dualObj : {ℂ : Cat} -> Obj ℂ -> Obj (ℂ op)
dualObj {cat _ _ _ _ _ _ _ _ _}(obj A) = obj A

undualObj : {ℂ : Cat} -> Obj (ℂ op) -> Obj ℂ
undualObj {cat _ _ _ _ _ _ _ _ _}(obj A) = obj A

dualdualArr : {ℂ : Cat}{A B : Obj ℂ} -> A ─→ B -> dualObj B ─→ dualObj A
dualdualArr {cat _ _ _ _ _ _ _ _ _}{A = obj _}{B = obj _}(arr f) = arr f

dualundualArr : {ℂ : Cat}{A : Obj ℂ}{B : Obj (ℂ op)} ->
		A ─→ undualObj B -> B ─→ dualObj A
dualundualArr {cat _ _ _ _ _ _ _ _ _}{A = obj _}{B = obj _}(arr f) = arr f
-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2013-03-20
-- Without termination checking disabled, the positivity checker
-- will throw an error.
module NoTerminationCheckPositivity where

open import Common.Level

module M {a}{A : Set a}(K : A → A → A) where

  -- F fails the termination check
  F : A → A
  F X = K X (F X)

K : Set → Set → Set
K X Y = X

open M K

data E : Set where
  e : F E → E

-- Since F is non-terminating and hence excluded from unfolding
-- in the positivity checker, it will complain unless termination
-- checking is off.

ext: agda

max_stars_repo_name: larrytheliquid/agda


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

-- This file contains an implementation of the stack-based compiler for Hutton's
-- razor, as from:
--
--   P. Bahr and G. Hutton, “Calculating correct compilers,” Journal of
--   Functional Programming, vol. 25, no. e14, Sep. 2015,
--   doi: 10.1017/S0956796815000180.
--
-- The compiler is total and the evaluator is stack-safe, and furthermore we have
-- proven a full isomorphism between the code representation and the AST.

module Data.Dyck.Except where

open import Prelude
open import Data.Nat using (_+_)
open import Data.Vec.Iterated using (Vec; _∷_; []; foldlN; head)

private
  variable
    n : ℕ

--------------------------------------------------------------------------------
-- Language for Arithmetic Expressions
--------------------------------------------------------------------------------

data Expr (A : Type a) : Type a where
  [_] : A → Expr A
  _⊕_ : Expr A → Expr A → Expr A

  throw : Expr A
  catch : Expr A → Expr A → Expr A

--------------------------------------------------------------------------------
-- Code for the virtual stack machine.
--------------------------------------------------------------------------------

data Code (A : Type a) : ℕ → Type a where
  HALT : Code A 1

  PUSH : A → Code A (1 + n) → Code A n
  ADD  : Code A (1 + n) → Code A (2 + n)

  RAISE : Code A (1 + n) → Code A n
  CATCH : Code A (1 + n) → Code A (2 + n)

--------------------------------------------------------------------------------
-- Conversion from a Code to a Expr (evaluation / execution)
--------------------------------------------------------------------------------

code→expr⊙ : Code A n → Vec (Expr A) n → Expr A
code→expr⊙ HALT        (v ∷ [])       = v
code→expr⊙ (PUSH v is) st             = code→expr⊙ is ([ v ] ∷ st)
code→expr⊙ (ADD    is) (t₁ ∷ t₂ ∷ st) = code→expr⊙ is (t₂ ⊕ t₁ ∷ st)
code→expr⊙ (RAISE  is) st             = code→expr⊙ is (throw ∷ st)
code→expr⊙ (CATCH  is) (t₁ ∷ t₂ ∷ st) = code→expr⊙ is (catch t₂ t₁ ∷ st)

code→expr : Code A zero → Expr A
code→expr ds = code→expr⊙ ds []

--------------------------------------------------------------------------------
-- Conversion from a Expr to a Code (compilation)
--------------------------------------------------------------------------------

expr→code⊙ : Expr A → Code A (1 + n) → Code A n
expr→code⊙ [ x ]         = PUSH x
expr→code⊙ (xs ⊕ ys)     = expr→code⊙ xs ∘ expr→code⊙ ys ∘ ADD
expr→code⊙ throw         = RAISE
expr→code⊙ (catch xs ys) = expr→code⊙ xs ∘ expr→code⊙ ys ∘ CATCH

expr→code : Expr A → Code A 0
expr→code tr = expr→code⊙ tr HALT

--------------------------------------------------------------------------------
-- Execution
--------------------------------------------------------------------------------

Func : Type a → ℕ → Type _
Func A zero    = Maybe A
Func A (suc n) = Maybe A → Func A n

open import Data.Maybe.Sugar

exec : Code ℕ n → Func ℕ n
exec HALT        = λ x → x
exec (PUSH x xs) = exec xs (just x)
exec (ADD    xs) = λ x₂ x₁ → exec xs ⦇ x₁ + x₂ ⦈
exec (RAISE  xs) = exec xs nothing
exec (CATCH  xs) = λ x₂ x₁ → exec xs (x₁ <|> x₂)

_ : exec (expr→code (catch ([ 3 ] ⊕ throw) ([ 10 ] ⊕ [ 2 ]))) ≡ just 12
_ = refl

--------------------------------------------------------------------------------
-- Proof of isomorphism
--------------------------------------------------------------------------------

expr→code→expr⊙ : {is : Code A (1 + n)} {st : Vec (Expr A) n} (e : Expr A) →
  code→expr⊙ (expr→code⊙ e is) st ≡ code→expr⊙ is (e ∷ st)
expr→code→expr⊙ [ x ]         = refl
expr→code→expr⊙ (xs ⊕ ys)     = expr→code→expr⊙ xs ; expr→code→expr⊙ ys
expr→code→expr⊙ throw         = refl
expr→code→expr⊙ (catch xs ys) = expr→code→expr⊙ xs ; expr→code→expr⊙ ys

code→expr→code⊙ : {st : Vec (Expr A) n} (is : Code A n) →
 expr→code (code→expr⊙ is st) ≡ foldlN (Code A) expr→code⊙ is st
code→expr→code⊙  HALT       = refl
code→expr→code⊙ (PUSH i is) = code→expr→code⊙ is
code→expr→code⊙ (ADD    is) = code→expr→code⊙ is
code→expr→code⊙ (RAISE  is) = code→expr→code⊙ is
code→expr→code⊙ (CATCH  is) = code→expr→code⊙ is

prog-iso : Code A 0 ⇔ Expr A
prog-iso .fun = code→expr
prog-iso .inv = expr→code
prog-iso .rightInv = expr→code→expr⊙
prog-iso .leftInv  = code→expr→code⊙

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- {-# OPTIONS --show-implicit #-} -- in case of emergency
module ldlc-algo-nosingle where

open import Data.Nat renaming (_+_ to _+ᴺ_ ; _≤_ to _≤ᴺ_ ; _≥_ to _≥ᴺ_ ; _<_ to _<ᴺ_ ; _>_ to _>ᴺ_ ; _≟_ to _≟ᴺ_)
open import Data.Nat.Properties renaming (_<?_ to _<ᴺ?_)
open import Data.Integer renaming (_+_ to _+ᶻ_ ; _≤_ to _≤ᶻ_ ; _≥_ to _≥ᶻ_ ; _<_ to _<ᶻ_ ; _>_ to _>ᶻ_)
open import Data.Integer.Properties using (⊖-≥ ; 0≤n⇒+∣n∣≡n ; +-monoˡ-≤)
open import Data.Fin
open import Data.Fin.Subset renaming (∣_∣ to ∣_∣ˢ)
open import Data.Vec hiding (_++_ ; length)
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary.PropositionalEquality renaming (trans to ≡-trans)
open import Data.Product
open import Data.Sum

open import aux

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

module syntx where
  data Exp {n : ℕ} : Set
  data Val {n : ℕ} : Exp {n} → Set
  data Ty {n : ℕ} : Set

  data Exp {n} where
    Var : ℕ → Exp {n}
    UnitE : Exp {n}
    Abs : Exp {n} → Exp {n}
    App : {e : Exp {n}} → Exp {n} → Val e → Exp {n}
    LabI : Fin n → Exp {n}
    CaseE : {s : Subset n} {e : Exp {n}} → Val e → (f : ∀ l → l ∈ s → Exp {n}) → Exp {n}
    Prod : Exp {n} → Exp {n} → Exp {n}
    ProdV : {e : Exp {n}} → Val e → Exp {n} → Exp {n}
    LetP : Exp {n} → Exp {n} → Exp {n}
    LetE : Exp {n} → Exp {n} → Exp {n}

  data Val {n} where
    VUnit : Val UnitE
    VVar : {i : ℕ} → Val (Var i)
    VLab : {x : Fin n} → Val (LabI x)
    VFun : {N : Exp} → Val (Abs N)
    VProd : {e e' : Exp} → (v : Val e) → Val e' → Val (ProdV v e')

  data Ty {n} where
    UnitT : Ty
    Label : Subset n → Ty
    Pi : Ty {n} → Ty {n} → Ty
    Sigma : Ty {n} → Ty {n} → Ty
    CaseT : {s : Subset n} {e : Exp {n}} → Val e → (f : ∀ l → l ∈ s → Ty {n}) → Ty

  -- variable in expression
  data _∈`_ {n : ℕ} : ℕ → Exp {n} → Set where
    in-var : {x : ℕ} → x ∈` (Var x)
    in-abs : {x : ℕ} {e : Exp {n}} → x ∈` e → (ℕ.suc x) ∈` (Abs e)
    in-app : {x : ℕ} {e e' : Exp {n}} {v : Val e'} → x ∈` e ⊎ x ∈` e' → x ∈` App e v
    in-casee : {x : ℕ} {s : Subset n} {f : (∀ l → l ∈ s → Exp {n})} {e : Exp {n}} {v : Val e} → (∃₂ λ l i → x ∈` (f l i)) ⊎ x ∈` e → x ∈` CaseE v f
    in-prod : {x : ℕ} {e e' : Exp {n}} → x ∈` e ⊎ (ℕ.suc x) ∈` e' → x ∈` Prod e e'
    in-prodv : {x : ℕ} {e e' : Exp {n}} {v : Val e} → x ∈` e ⊎ x ∈` e' → x ∈` ProdV v e'  -- (Pair-A-I => e' has 0 substituted away => just x, not suc x)
    in-letp : {x : ℕ} {e e' : Exp {n}} → x ∈` e ⊎ (ℕ.suc (ℕ.suc x)) ∈` e' → x ∈` LetP e e'
    in-lete : {x : ℕ} {e e' : Exp {n}} → x ∈` e ⊎ (ℕ.suc x) ∈` e' → x ∈` LetE e e'

  -- variable in type
  data _∈`ᵀ_ {n : ℕ} : ℕ → Ty {n} → Set where
    in-pi : {x : ℕ} {A B : Ty {n}} → n ∈`ᵀ A ⊎ n ∈`ᵀ B → n ∈`ᵀ Pi A B
    in-pigma : {x : ℕ} {A B : Ty {n}} → n ∈`ᵀ A ⊎ n ∈`ᵀ B → n ∈`ᵀ Sigma A B
    in-case : {x : ℕ} {s : Subset n} {f : ∀ l → l ∈ s → Ty {n}} {e : Exp {n}} {v : Val e} → (∃₂ λ l i → x ∈`ᵀ (f l i)) ⊎ x ∈` e → x ∈`ᵀ CaseT v f

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

module substitution where
  ---- Substitution and Shifting
  open syntx

  ↑ᴺ_,_[_] : ℤ → ℕ → ℕ → ℕ
  ↑ᴺ d , c [ x ]
    with (x <ᴺ? c)
  ...  | yes p = x
  ...  | no ¬p = ∣ ℤ.pos x +ᶻ d ∣

  ↑_,_[_] : ∀ {n} → ℤ → ℕ → Exp {n} → Exp {n}
  shift-val : ∀ {n d c} {e : Exp {n}} → Val e → Val (↑ d , c [ e ])

  ↑ d , c [ UnitE ] = UnitE
  ↑ d , c [ Var x ] = Var (↑ᴺ d , c [ x ])
  ↑ d , c [ Abs t ] = Abs (↑ d , (ℕ.suc c) [ t ])
  ↑ d , c [ App t v ] = App (↑ d , c [ t ]) (shift-val{d = d}{c = c} v)
  ↑ d , c [ LabI x ] = LabI x
  ↑ d , c [ CaseE{e = e} V f ] = CaseE (shift-val{d = d}{c = c} V) (λ l x → ↑ d , c [ f l x ])
  ↑ d , c [ Prod e e' ] = Prod (↑ d , c [ e ]) (↑ d , (ℕ.suc c) [ e' ])
  ↑ d , c [ ProdV e e' ] = ProdV (shift-val{d = d}{c = c} e) (↑ d , (ℕ.suc c) [ e' ])
  ↑ d , c [ LetP e e' ] = LetP (↑ d , c [ e ]) (↑ d , (ℕ.suc (ℕ.suc c)) [ e' ])
  ↑ d , c [ LetE e e' ] = LetE (↑ d , c [ e ]) (↑ d , (ℕ.suc c) [ e' ])

  shift-val {n} {d} {c} {.UnitE} VUnit = VUnit
  shift-val {n} {d} {c} {.(Var _)} VVar = VVar
  shift-val {n} {d} {c} {.(LabI _)} VLab = VLab
  shift-val {n} {d} {c} {.(Abs _)} VFun = VFun
  shift-val {n} {d} {c} {.(ProdV V _)} (VProd V V₁) = VProd (shift-val V) (shift-val V₁)

  -- shorthands
  ↑¹[_] : ∀ {n} → Exp {n} → Exp
  ↑¹[ e ] = ↑ (ℤ.pos 1) , 0 [ e ]

  ↑ⱽ¹[_] : ∀ {n} {e : Exp {n}} → Val e → Val (↑ (ℤ.pos 1) , 0 [ e ])
  ↑ⱽ¹[_] {n} {e} v = shift-val v

  ↑⁻¹[_] : ∀ {n} → Exp {n} → Exp
  ↑⁻¹[ e ] = ↑ (ℤ.negsuc 0) , 0 [ e ]

  -- substitution
  [_↦_]_ : ∀ {n} {e : Exp {n}} → ℕ → Val e → Exp {n} → Exp {n}
  sub-val : ∀ {n k} {e e' : Exp {n}} {v : Val e'} → Val e → Val ([ k ↦ v ] e)
  [_↦_]_ {n} {e} k v (Var x)
    with (_≟ᴺ_ x k)
  ...  | yes p = e
  ...  | no ¬p = Var x
  [ k ↦ v ] UnitE = UnitE
  [ k ↦ v ] Abs e = Abs (([ ℕ.suc k ↦ shift-val{d = ℤ.pos 1}{c = 0} v ] e))
  [_↦_]_ {n} {e'} k v (App{e = e₁} e v') = App ([ k ↦ v ] e) (sub-val{n}{k}{e₁}{e'}{v} v') -- ([ k ↦ v ] e₁)
  [ k ↦ v ] LabI x = LabI x
  [_↦_]_ {n} {e} k v (CaseE v' f) = CaseE (sub-val{n}{k}{e' = e}{v = v} v') (λ l x₁ → [ k ↦ v ] (f l x₁))
  [ k ↦ v ] Prod e e₁ = Prod ([ k ↦ v ] e) ([ ℕ.suc k ↦ shift-val{d = ℤ.pos 1}{c = 0} v ] e₁)
  [_↦_]_ {n} {e} k v (ProdV v' e') = ProdV (sub-val{n}{k}{e' = e}{v = v} v') ([ ℕ.suc k ↦ shift-val{d = ℤ.pos 1}{c = 0} v ] e')
  [ k ↦ v ] LetP e e₁ = LetE ([ k ↦ v ] e) ([ (ℕ.suc (ℕ.suc k)) ↦ shift-val{d = ℤ.pos 2}{c = 0} v ] e₁)
  [ k ↦ v ] LetE e e₁ = LetE ([ k ↦ v ] e) ([ (ℕ.suc k) ↦ shift-val{d = ℤ.pos 1}{c = 0} v ] e₁)

  sub-val {n} {k} {.UnitE} {e'} {v} VUnit = VUnit
  sub-val {n} {k} {(Var i)} {e'} {v} VVar
    with (_≟ᴺ_ i k)
  ...  | yes p = v
  ...  | no ¬p = VVar
  sub-val {n} {k} {.(LabI _)} {e'} {v} VLab = VLab
  sub-val {n} {k} {.(Abs _)} {e'} {v} VFun = VFun
  sub-val {n} {k} {.(ProdV v' _)} {e'} {v} (VProd v' v'') = VProd (sub-val v') (sub-val v'')

  -- type substitution
  [_↦_]ᵀ_ : ∀ {n} {e : Exp {n}} → ℕ → Val e → Ty {n} → Ty {n}
  [ k ↦ s ]ᵀ UnitT = UnitT
  [ k ↦ s ]ᵀ Label x = Label x
  [ k ↦ s ]ᵀ Pi T T₁ = Pi ([ k ↦ s ]ᵀ T) ([ k ↦ s ]ᵀ T₁)
  [ k ↦ s ]ᵀ Sigma T T₁ = Sigma ([ k ↦ s ]ᵀ T) ([ k ↦ s ]ᵀ T₁)
  [_↦_]ᵀ_ {n} {e} k v (CaseT x f) = CaseT (sub-val{n}{k}{e' = e}{v = v} x) λ l x₁ → [ k ↦ v ]ᵀ (f l x₁)

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

module typing where
  open syntx
  open substitution

  -- Type environment
  data TEnv {n : ℕ} : Set where
    [] : TEnv
    ⟨_,_⟩ : (T : Ty {n}) (Γ : TEnv {n}) → TEnv

  _++_ : {n : ℕ} → TEnv {n} → TEnv {n} → TEnv {n}
  [] ++ Γ' = Γ'
  ⟨ T , Γ ⟩ ++ Γ' = ⟨ T , Γ ++ Γ' ⟩

  ++-assoc : {n : ℕ} {Γ Γ' Γ'' : TEnv {n}} → Γ ++ (Γ' ++ Γ'') ≡ (Γ ++ Γ') ++ Γ''
  ++-assoc {n} {[]} {Γ'} {Γ''} = refl
  ++-assoc {n} {⟨ T , Γ ⟩} {Γ'} {Γ''} = cong (λ x → ⟨ T , x ⟩) (++-assoc{n}{Γ}{Γ'}{Γ''})

  length : {n : ℕ} → TEnv {n} → ℕ
  length {n} [] = zero
  length {n} ⟨ T , Γ ⟩ = ℕ.suc (length Γ)

  data _∶_∈_ {n : ℕ} : ℕ → Ty {n} → TEnv {n} → Set where
    here : {T : Ty} {Γ : TEnv} → 0 ∶ T ∈ ⟨ T , Γ ⟩
    there : {n : ℕ} {T₁ T₂ : Ty} {Γ : TEnv} → n ∶ T₁ ∈ Γ → (ℕ.suc n) ∶ T₁ ∈ ⟨ T₂ , Γ ⟩

  ---- Algorithmic Typing
  -- Type environment formation
  data ⊢_ok {n : ℕ} : TEnv {n} → Set
  -- Type formation
  data _⊢_ {n : ℕ} : TEnv {n}→ Ty {n} → Set
  -- Type synthesis
  data _⊢_⇒_ {n : ℕ} : TEnv {n} → Exp {n} → Ty {n} → Set
  -- Type check
  data _⊢_⇐_ {n : ℕ} : TEnv {n} → Exp {n} → Ty {n} → Set
  -- Check subtype (⇐ instead of ⇒?)
  data _⇒_≤_ {n : ℕ} : TEnv {n} → Ty {n} → Ty {n} → Set
  -- Unfolding (e.g. CaseT ... ⇓ T)
  data _⊢_⇓_ {n : ℕ} : TEnv {n} → Ty {n} → Ty {n} → Set
  -- Conversion
  data _⇒_≡_ {n : ℕ} : TEnv {n} → Ty {n} → Ty {n} → Set

  -- Implementations
  data ⊢_ok {n} where
    empty : ⊢ [] ok
    entry : {Γ : TEnv {n}} {A : Ty {n}} → ⊢ Γ ok → Γ ⊢ A → ⊢ ⟨ A , Γ ⟩ ok

  data _⊢_ {n} where
    UnitF : {Γ : TEnv {n}} → ⊢ Γ ok → Γ ⊢ UnitT
    LabF : {Γ : TEnv {n}} {L : Subset n} → ⊢ Γ ok → Γ ⊢ Label L
    PiF : {Γ : TEnv {n}} {A B : Ty {n}} → Γ ⊢ A → ⟨ A , Γ ⟩ ⊢ B → Γ ⊢ Pi A B
    SigmaF : {Γ : TEnv {n}} {A B : Ty {n}} → Γ ⊢ A → ⟨ A , Γ ⟩ ⊢ B → Γ ⊢ Sigma A B
    CaseF : {Γ : TEnv {n}} {L : Subset n} {e : Exp {n}} {V : Val e} {f : ∀ l → l ∈ L → Ty {n}} {f-ok : ∀ l → (i : l ∈ L) → Γ ⊢ (f l i)} → Γ ⊢ e ⇐ Label L → Γ ⊢ CaseT V f

  data _⊢_⇐_ {n} where
    SubTypeA : {Γ : TEnv {n}} {A B : Ty {n}} {M : Exp {n}}
               → Γ ⊢ M ⇒ A
               → Γ ⇒ A ≤ B
               → Γ ⊢ M ⇐ B

  data _⇒_≤_ {n} where
    ASubUnit : {Γ : TEnv {n}} → Γ ⇒ UnitT ≤ UnitT
    ASubLabel : {Γ : TEnv {n}} {L L' : Subset n} → L ⊆ L' → Γ ⇒ Label L ≤ Label L'
    ASubPi : {Γ : TEnv {n}} {A A' B B' : Ty {n}}
             → Γ ⇒ A' ≤ A
             → ⟨ A' , Γ ⟩ ⇒ B ≤ B'
             → Γ ⇒ Pi A B ≤ Pi A' B'
    ASubSigma : {Γ : TEnv {n}} {A A' B B' : Ty {n}}
                → Γ ⇒ A ≤ A'
                → ⟨ A , Γ ⟩ ⇒ B ≤ B'
                → Γ ⇒ Sigma A B ≤ Sigma A' B'
    ASubCaseLL : {Γ : TEnv {n}} {B : Ty {n}} {e : Exp {n}} {V : Val e} {l : Fin n} {L L' : Subset n} {f : ∀ l → l ∈ L → Ty {n}} {ins : l ∈ L}
                 → Γ ⊢ e ⇒ Label ⁅ l ⁆
                 → L' ⊆ L
                 → Γ ⇒ (f l ins) ≤ B
                 → Γ ⇒ CaseT V f ≤ B
    ASubCaseLR : {Γ : TEnv {n}} {A : Ty {n}} {e : Exp {n}} {V : Val e} {l : Fin n} {L L' : Subset n} {f : ∀ l → l ∈ L → Ty {n}} {ins : l ∈ L}
                 → Γ ⊢ e ⇒ Label ⁅ l ⁆
                 → L' ⊆ L
                 → Γ ⇒ A ≤ (f l ins)
                 → Γ ⇒ A ≤ CaseT V f
    ASubCaseXL : {Γ Γ' : TEnv {n}} {B D : Ty {n}} {L : Subset n} {f : ∀ l → l ∈ L → Ty {n}}
               → Γ ⇒ D ≤ Label L
               → (∀ l → (i : l ∈ L) → (Γ' ++ ⟨ Label ⁅ l ⁆ , Γ ⟩) ⇒ (f l i) ≤ B)
               → (Γ' ++ ⟨ D , Γ ⟩) ⇒ CaseT (VVar{i = length Γ'}) f ≤ B
    ASubCaseXR : {Γ Γ' : TEnv {n}} {A D : Ty {n}} {L : Subset n} {f : ∀ l → l ∈ L → Ty {n}}
               → Γ ⇒ D ≤ Label L
               → (∀ l → (i : l ∈ L) → (Γ' ++ ⟨ Label ⁅ l ⁆ , Γ ⟩) ⇒ A ≤ (f l i))
               → (Γ' ++ ⟨ D , Γ ⟩) ⇒ A ≤ CaseT (VVar{i = length Γ'}) f

  data _⊢_⇒_ {n} where
    VarA : {Γ : TEnv {n}} {A : Ty {n}} {x : ℕ} → ⊢ Γ ok → x ∶ A ∈ Γ → Γ ⊢ Var x ⇒ A
    UnitAI : {Γ : TEnv {n}} → ⊢ Γ ok → Γ ⊢ UnitE ⇒ UnitT
    LabAI : {Γ : TEnv {n}} {l : Fin n} → ⊢ Γ ok → Γ ⊢ LabI l ⇒ Label ⁅ l ⁆
    LabAEl : {Γ : TEnv {n}} {B : Ty {n}} {L L' : Subset n} {l : Fin n} {ins : l ∈ L'} {f : ∀ l → l ∈ L → Exp {n}}
             → Γ ⊢ (LabI l) ⇒ Label L'
             → (s : L' ⊆ L)
             → Γ ⊢ (f l (s ins)) ⇒ B
             → Γ ⊢ CaseE (VLab{x = l}) f ⇒ B
    -- unification has problems with arbitrary functions, hence θ
    -- see https://lists.chalmers.se/pipermail/agda/2020/012293.html
    LabAEx : {Γ Γ' Θ : TEnv {n}} {D : Ty {n}} {L : Subset n} {f : ∀ l → l ∈ L → Exp {n}} {f-t : ∀ l → l ∈ L → Ty {n}} {eq : Θ ≡ (Γ' ++ ⟨ D , Γ ⟩)}
             → Γ ⇒ D ≤ Label L
             → (∀ l → (i : l ∈ L) → (Γ' ++ ⟨ Label ⁅ l ⁆ , Γ ⟩) ⊢ (f l i) ⇒ (f-t l i))
             → Θ ⊢ CaseE (VVar{i = length Γ'}) f ⇒ CaseT (VVar{i = length Γ'}) f-t
    PiAI : {Γ : TEnv {n}} {A B : Ty {n}}  {M : Exp {n}} → ⟨ A , Γ ⟩ ⊢ M ⇒ B → Γ ⊢ Abs M ⇒ Pi A B
    PiAE : {Γ : TEnv {n}} {A B D : Ty {n}} {M e : Exp {n}} {V : Val e}
           → Γ ⊢ M ⇒ D
           → Γ ⊢ D ⇓ Pi A B
           → Γ ⊢ e ⇐ A
           → Γ ⊢ ([ 0 ↦ V ]ᵀ B)
           → Γ ⊢ App M V ⇒ ([ 0 ↦ V ]ᵀ B)
    SigmaAI : {Γ : TEnv {n}} {A A' B : Ty {n}} {M N : Exp {n}}
              → Γ ⊢ M ⇐ A
              → Γ ⇒ A' ≤ A
              → ⟨ A' , Γ ⟩ ⊢ N ⇒ B
              → Γ ⊢ Prod M N ⇒ Sigma A B
    PairAI : {Γ : TEnv {n}} {A B : Ty {n}} {e N : Exp {n}} {V : Val e}
             → Γ ⊢ e ⇒ A
             → Γ ⊢ N ⇒ B
             → Γ ⊢ ProdV V N ⇒ Sigma A B
    SigmaAE : {Γ : TEnv {n}} {A B C D : Ty {n}} {M N : Exp {n}}
            → Γ ⊢ M ⇒ D
            → Γ ⊢ D ⇓ Sigma A B
            → ⟨ B , ⟨ A , Γ ⟩ ⟩ ⊢ N ⇒ C
            → (¬ (0 ∈`ᵀ C)) × (¬ (1 ∈`ᵀ C))
            → Γ ⊢ LetP M N ⇒ C
    Let : {Γ : TEnv {n}} {A B : Ty {n}} {M N : Exp {n}}
          → ¬(0 ∈`ᵀ B)
          → Γ ⊢ M ⇒ A
          → ⟨ A , Γ ⟩ ⊢ N ⇒ B
          → Γ ⊢ LetE M N ⇒ B

  data _⊢_⇓_ {n} where
    AURefl-U : {Γ : TEnv {n}} → Γ ⊢ UnitT ⇓ UnitT
    AURefl-L : {Γ : TEnv {n}} {L : Subset n} → Γ ⊢ Label L ⇓ Label L
    AURefl-P : {Γ : TEnv {n}} {A B : Ty {n}} → Γ ⊢ Pi A B ⇓ Pi A B
    AURefl-S : {Γ : TEnv {n}} {A B : Ty {n}} → Γ ⊢ Sigma A B ⇓ Sigma A B
    AUCaseL : {Γ : TEnv {n}} {D : Ty {n}} {l : Fin n} {L L' : Subset n} {ins : l ∈ L} {f : ∀ l → l ∈ L → Ty {n}} {e : Exp {n}} {V : Val e}
              → Γ ⊢ e ⇒ Label ⁅ l ⁆
              → L' ⊆ L
              → Γ ⊢ (f l ins) ⇓ D
              → Γ ⊢ CaseT V f ⇓ D
    AUCaseX-P : {Γ Γ' : TEnv {n}} {A D : Ty {n}} {L : Subset n} {fᴬ fᴮ fᴰ : (∀ l → l ∈ L → Ty {n})}
              → Γ ⇒ D ≤ Label L
              → (∀ l → (i : l ∈ L) → (Γ' ++ ⟨ Label ⁅ l ⁆ , Γ ⟩) ⊢ (fᴮ l i) ⇓ Pi (fᴬ l i) (fᴰ l i))
              → (∀ l → (i : l ∈ L) → (Γ' ++ ⟨ Label ⁅ l ⁆ , Γ ⟩) ⇒ A ≡ (fᴬ l i))
              → (Γ' ++ ⟨ D , Γ ⟩) ⊢ CaseT (VVar{i = length Γ'}) fᴮ ⇓ Pi A (CaseT (VVar{i = length Γ'}) fᴰ)
    AUCaseX-S : {Γ Γ' : TEnv {n}} {A D : Ty {n}} {L : Subset n} {fᴬ fᴮ fᴰ : (∀ l → l ∈ L → Ty {n})}
              → Γ ⇒ D ≤ Label L
              → (∀ l → (i : l ∈ L) → (Γ' ++ ⟨ Label ⁅ l ⁆ , Γ ⟩) ⊢ (fᴮ l i) ⇓ Sigma (fᴬ l i) (fᴰ l i))
              → (∀ l → (i : l ∈ L) → (Γ' ++ ⟨ Label ⁅ l ⁆ , Γ ⟩) ⇒ A ≡ (fᴬ l i))
              → (Γ' ++ ⟨ D , Γ ⟩) ⊢ CaseT (VVar{i = length Γ'}) fᴮ ⇓ Sigma A (CaseT (VVar{i = length Γ'}) fᴰ)

  data _⇒_≡_ {n} where
    AConvUnit : {Γ : TEnv {n}} → Γ ⇒ UnitT ≡ UnitT
    AConvLabel : {Γ : TEnv {n}} {L : Subset n} → Γ ⇒ Label L ≡ Label L
    AConvPi : {Γ : TEnv {n}} {A A' B B' : Ty} → Γ ⇒ A ≡ A' → ⟨ A' , Γ ⟩ ⇒ B ≡ B' → Γ ⇒ Pi A B ≡ Pi A' B'
    AConvSigma : {Γ : TEnv {n}} {A A' B B' : Ty} → Γ ⇒ A ≡ A' → ⟨ A , Γ ⟩ ⇒ B ≡ B' → Γ ⇒ Sigma A B ≡ Sigma A' B'
    AConvCaseLL : {Γ : TEnv {n}} {B : Ty {n}} {e : Exp {n}} {V : Val e} {L L' : Subset n} {f : (∀ l → l ∈ L → Ty)} {l : Fin n} {ins : l ∈ L}
                  → Γ ⊢ e ⇒ Label ⁅ l ⁆
                  → L ⊆ L'
                  → Γ ⇒ (f l ins) ≡ B
                  → Γ ⇒ CaseT V f ≡ B
    AConvCaseLR : {Γ : TEnv {n}} {A : Ty {n}} {e : Exp {n}} {V : Val e} {L L' : Subset n} {f : (∀ l → l ∈ L → Ty)} {l : Fin n} {ins : l ∈ L}
                  → Γ ⊢ e ⇒ Label ⁅ l ⁆
                  → L ⊆ L'
                  → Γ ⇒ A ≡ (f l ins)
                  → Γ ⇒ A ≡ CaseT V f
    AConvCaseXL : {Γ Γ' : TEnv {n}} {B D : Ty {n}} {L : Subset n} {f : ∀ l → l ∈ L → Ty {n}}
               → Γ ⇒ D ≤ Label L
               → (∀ l → (i : l ∈ L) → (Γ' ++ ⟨ Label ⁅ l ⁆ , Γ ⟩) ⇒ (f l i) ≡ B)
               → (Γ' ++ ⟨ D , Γ ⟩) ⇒ CaseT (VVar{i = length Γ'}) f ≡ B
    AConvCaseXR : {Γ Γ' : TEnv {n}} {A D : Ty {n}} {L : Subset n} {f : ∀ l → l ∈ L → Ty {n}}
               → Γ ⇒ D ≤ Label L
               → (∀ l → (i : l ∈ L) → (Γ' ++ ⟨ Label ⁅ l ⁆ , Γ ⟩) ⇒ A ≡ (f l i))
               → (Γ' ++ ⟨ D , Γ ⟩) ⇒ A ≡ CaseT (VVar{i = length Γ'}) f

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

module semantics where
  open syntx
  open substitution

  data _↠_ {n : ℕ} : Exp {n} → Exp {n} → Set where
    ξ-App : {e₁ e₁' e : Exp {n}} {v : Val e} → e₁ ↠ e₁' → App e₁ v ↠ App e₁' v
    ξ-LetE : {e₁ e₁' e : Exp {n}} → e₁ ↠ e₁' → LetE e₁ e ↠ LetE e₁' e
    ξ-Prod : {e₁ e₁' e : Exp {n}} → e₁ ↠ e₁' → Prod e₁ e ↠ Prod e₁' e
    ξ-ProdV : {e e₂ e₂' : Exp {n}} {v : Val e} → e₂ ↠ e₂' → ProdV v e₂ ↠ ProdV v e₂'
    ξ-LetP : {e₁ e₁' e₂ : Exp {n}} → e₁ ↠ e₁' → LetP e₁ e₂ ↠ LetP e₁' e₂
    β-App : {e e' : Exp {n}} → (v : Val e') → (App (Abs e) v) ↠ (↑⁻¹[ ([ 0 ↦ ↑ⱽ¹[ v ] ] e) ])
    β-Prod : {e e' : Exp {n}} {v : Val e} → Prod e e' ↠ ProdV v (↑⁻¹[ ([ 0 ↦ ↑ⱽ¹[ v ] ] e') ])
    β-LetE : {e e' : Exp {n}} → (v : Val e) → LetE e e' ↠ (↑⁻¹[ ([ 0 ↦ ↑ⱽ¹[ v ] ] e') ])
    β-LetP : {e e' e'' : Exp {n}} → (v : Val e) → (v' : Val e')
                              → LetP (ProdV v e') e''
                                ↠
                                ↑ (ℤ.negsuc 1) , 0 [ ([ 0 ↦ ↑ⱽ¹[ v ] ]
                                                       ([ 0 ↦ shift-val {n} {ℤ.pos 1} {1} v' ] e'')) ]
    β-LabE : {s : Subset n} {f : ∀ l → l ∈ s → Exp {n}} {x : Fin n} → (ins : x ∈ s)
             → CaseE (VLab{x = x}) f ↠ f x ins

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

module progress where
  open syntx
  open substitution
  open typing
  open semantics

  -- To eliminate the possible typing judgement (LabAEx) for case expressions,
  -- we need ([] ≢ Γ' ++ ⟨ D , Γ ⟩. Agda does not know that no possible constructor
  -- for this equality exists, because _++_ is an arbitrary function and therefore
  -- "green slime" (see the link @ (LabAEx) rule).
  --
  -- Workaround: Argue with length of environments
  env-len-++ : {n : ℕ} {Γ Γ' : TEnv {n}} → length (Γ ++ Γ') ≡ length Γ +ᴺ length Γ'
  env-len-++ {n} {[]} {Γ'} = refl
  env-len-++ {n} {⟨ T , Γ ⟩} {Γ'} = cong ℕ.suc (env-len-++ {n} {Γ} {Γ'})

  env-len-> : {n : ℕ} {Γ : TEnv {n}} {T : Ty {n}} → length ⟨ T , Γ ⟩ >ᴺ 0
  env-len-> {n} {Γ} {T} = s≤s z≤n

  env-len->-++ : {n : ℕ} {Γ Γ' : TEnv {n}} → length Γ' >ᴺ 0 → length (Γ ++ Γ') >ᴺ 0
  env-len->-++ {n} {Γ} {⟨ T , Γ' ⟩} gt rewrite (env-len-++ {n} {Γ} {⟨ T , Γ' ⟩})= ≤-trans gt (m≤n+m (length ⟨ T , Γ' ⟩) (length Γ))

  env-len-eq : {n : ℕ} {Γ : TEnv {n}} {Γ' : TEnv {n}} → Γ ≡ Γ' → length Γ ≡ length Γ'
  env-len-eq {n} {Γ} {.Γ} refl = refl

  env-empty-++ : {n : ℕ} {Γ' Γ : TEnv {n}} {D : Ty {n}} → ¬ ([] ≡ Γ' ++ ⟨ D , Γ ⟩)
  env-empty-++ {n} {Γ} {Γ'} {D} eq = contradiction (env-len-eq eq) (<⇒≢ (env-len->-++ (env-len->{T = D})))

  -- Canonical forms
  canonical-forms-pi : {n : ℕ} {e : Exp {n}} {A B D : Ty {n}} → [] ⊢ e ⇒ D → [] ⊢ D ⇓ Pi A B → Val e → (∃[ e' ](e ≡ Abs e'))
  canonical-forms-pi {n} {.(Abs _)} {A} {B} {.(Pi _ _)} (PiAI{M = M} j) u v = M , refl

  canonical-forms-sigma : {n : ℕ} {e : Exp {n}} {A B D : Ty {n}} → [] ⊢ e ⇒ D → [] ⊢ D ⇓ Sigma A B → Val e → (∃{A = Exp {n}} λ e' → ∃{A = Val e'} λ v → ∃ λ e'' → e ≡ ProdV{e = e'} v e'')
  canonical-forms-sigma {n} {.(ProdV _ _)} {A} {B} {.(Sigma _ _)} (PairAI{e = e}{N}{V} j j₁) u v = e , (V , (N , refl))

  -- Main theorem
  data Progress {n : ℕ} (e : Exp {n}) {T : Ty} {j : [] ⊢ e ⇒ T} : Set where
    step : {e' : Exp{n}} → e ↠ e' → Progress e
    value : Val e → Progress e

  progress : {n : ℕ} {e : Exp {n}} {T : Ty} → (j : [] ⊢ e ⇒ T) → Progress e {T} {j}
  progress {n} {Var x} {T} (VarA x₁ x₂) = value VVar
  progress {n} {UnitE} {.UnitT} (UnitAI x) = value VUnit
  progress {n} {Abs e} {.(Pi _ _)} (PiAI j) = value VFun
  progress {n} {App e x} {.([ 0 ↦ x ]ᵀ _)} (PiAE{A = A}{B = B}{D = D} j x₁ x₂ x₃)
    with progress {n} {e} {D} j
  ...  | step x₄ = step (ξ-App x₄)
  ...  | value x₄
       with canonical-forms-pi {n} {e} {A} {B} {D} j x₁ x₄
  ...     | fst , snd rewrite snd = step (β-App x)
  progress {n} {LabI x} {.(Label ⁅ x ⁆)} (LabAI x₁) = value VLab
  progress {n} {Prod e e₁} {.(Sigma A B)} (SigmaAI {A = A} {B = B} (SubTypeA{A = A₁} x x₂) x₁ j)
    with progress {n} {e} {A₁} x
  ...  | step x₃ = step (ξ-Prod x₃)
  ...  | value x₃ = step (β-Prod{v = x₃})
  progress {n} {ProdV x e} {.(Sigma _ _)} (PairAI{A = A} {B = B} j j₁)
    with progress {n} {e} {B} j₁
  ...  | step x₁ = step (ξ-ProdV x₁)
  ...  | value x₁ = value (VProd x x₁)
  progress {n} {LetP e e₁} {T} (SigmaAE{A = A}{B = B}{D = D} j x j₁ x₁)
    with progress {n} {e} {D} j
  ...  | step x₂ = step (ξ-LetP x₂)
  ...  | value x₂
       with canonical-forms-sigma {n} {e} {A} {B} {D} j x x₂
  ...     | fst , fst₁ , fst₂ , snd rewrite snd
          with x₂
  ...        | VProd v v₁ = step (β-LetP v v₁)
  progress {n} {LetE e e₁} {T} (Let{A = A} x j j₁)
    with progress {n} {e} {A} j
  ...  | step x₁ = step (ξ-LetE x₁)
  ...  | value x₁ = step (β-LetE x₁)
  progress {n} {CaseE {e = .(LabI _)} VLab f} {T} (LabAEl {l = _} {ins = ins} (LabAI x₁) x j₁) = step (β-LabE (x ins))
  progress {n} {CaseE .VVar f} {.(CaseT VVar _)} (LabAEx{eq = eq} x x₁) = contradiction eq env-empty-++

max_stars_repo_name: kcaliban/ldlc

max_issues_repo_name: kcaliban/ldlc

max_forks_repo_name: kcaliban/ldlc


text:
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary.PropositionalEquality using
  ( _≡_ ; refl ; sym ; trans ; subst ; cong )

module Cats.Category.Discrete {li} {I : Set li}
  (I-set : ∀ {i j : I} (p q : i ≡ j) → p ≡ q)
  where

open import Data.Product using (Σ-syntax ; _,_ ; proj₁ ; proj₂)
open import Data.Unit using (⊤)
open import Level

open import Cats.Category.Base
open import Cats.Functor using (Functor)

Obj : Set li
Obj = I

data _⇒_ : Obj → Obj → Set li where
  id : ∀ {A} → A ⇒ A

⇒-contr : ∀ {A B} (f : A ⇒ B)
  → Σ[ p ∈ A ≡ B ] (subst (_⇒ B) p f ≡ id)
⇒-contr id = refl , refl

⇒-contr′ : ∀ {A} (f : A ⇒ A)
  → f ≡ id
⇒-contr′ f with ⇒-contr f
... | A≡A , f≡id rewrite I-set A≡A refl = f≡id

⇒-prop : ∀ {A B} (f g : A ⇒ B) → f ≡ g
⇒-prop {A} {B} id g = sym (⇒-contr′ g)

_∘_ : ∀ {A B C} → B ⇒ C → A ⇒ B → A ⇒ C
id ∘ id = id

Discrete : Category li li zero
Discrete = record
    { Obj = Obj
    ; _⇒_ = _⇒_
    ; _≈_ = λ _ _ → ⊤
    ; id = id
    ; _∘_ = _∘_
    ; equiv = _
    ; ∘-resp = _
    ; id-r = _
    ; id-l = _
    ; assoc = _
    }

functor : ∀ {lo la l≈} {C : Category lo la l≈}
  → (I → Category.Obj C)
  → Functor Discrete C
functor {C = C} f = record
    { fobj = f
    ; fmap = fmap
    ; fmap-resp = λ {A} {B} {g} {h} _ → C.≈.reflexive (cong fmap (⇒-prop g h))
    ; fmap-id = C.≈.refl
    ; fmap-∘ = λ { {f = id} {id} → C.id-l }
    }
  where
    module C = Category C

    fmap : ∀ {A B} (g : A ⇒ B) → f A C.⇒ f B
    fmap id = C.id

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
{-# OPTIONS --cubical --safe --guardedness #-}
module Cubical.Codata.M where

open import Cubical.Foundations.Prelude

-- TODO move
module Helpers where
  module _ {ℓ ℓ'} {A : Type ℓ} {x : A} (P : ∀ y → x ≡ y → Type ℓ') (d : P x refl) where
    -- A version with y as an explicit argument can be used to make Agda
    -- infer the family P.
    J' : ∀ y (p : x ≡ y) → P y p
    J' y p = J P d p

  lem-transp : ∀ {ℓ} {A : Type ℓ} (i : I) → (B : Type ℓ) (P : A ≡ B) → (p : P i) → PathP (\ j → P j) (transp (\ k → P (~ k ∧ i)) (~ i) p)
                                                                                (transp (\ k → P (k ∨ i)) i p)
  lem-transp {A = A} i = J' _ (\ p j → transp (\ _ → A) ((~ j ∧ ~ i) ∨ (j ∧ i)) p )

  transp-over : ∀ {ℓ} (A : I → Type ℓ) (i j : I) → A i → A j
  transp-over A i k p = transp (\ j → A ((~ j ∧ i) ∨ (j ∧ k))) (~ i ∧ ~ k) p

  transp-over-1 : ∀ {ℓ} (A : I → Type ℓ) (i j : I) → A i → A j
  transp-over-1 A i k p = transp (\ j → A ((j ∨ i) ∧ (~ j ∨ k))) (i ∧ k) p

  compPathD : {ℓ ℓ' : _} {X : Type ℓ} (F : X → Type ℓ') {A B C : X} (P : A ≡ B) (Q : B ≡ C)
              → ∀ {x y z} → (\ i → F (P i)) [ x ≡ y ] → (\ i → F (Q i)) [ y ≡ z ] → (\ i → F ((P ∙ Q) i)) [ x ≡ z ]
  compPathD F {A = A} P Q {x} p q i =
     comp (\ j → F (hfill (λ j → \ { (i = i0) → A ; (i = i1) → Q j })
                          (inS (P i))
                          j))
          (λ j → \ { (i = i0) → x; (i = i1) → q j })
          (p i)

open Helpers

IxCont : Type₀ → Type₁
IxCont X = Σ (X → Type₀) \ S → ∀ x → S x → X → Type₀

⟦_⟧ : ∀ {X : Type₀} → IxCont X → (X → Type₀) → (X → Type₀)
⟦ (S , P) ⟧ X x = Σ (S x) \ s → ∀ y → P x s y → X y

record M {X : Type₀} (C : IxCont X) (x : X) : Type₀ where
  coinductive
  field
    head : C .fst x
    tails : ∀ y → C .snd x head y → M C y

open M public

module _ {X : Type₀} {C : IxCont X} where

  private
    F = ⟦ C ⟧

  out : ∀ x → M C x → F (M C) x
  out x a = (a .head) , (a .tails)

  mapF : ∀ {A B} → (∀ x → A x → B x) → ∀ x → F A x → F B x
  mapF f x (s , t) = s , \ y p → f _ (t y p)

  unfold : ∀ {A} (α : ∀ x → A x → F A x) → ∀ x → A x → M C x
  unfold α x a .head = α x a .fst
  unfold α x a .tails y p = unfold α y (α x a .snd y p)

  -- We generalize the type to avoid upsetting --guardedness by
  -- transporting after the corecursive call.
  -- Recognizing hcomp/transp as guardedness-preserving could be a better solution.
  unfold-η' : ∀ {A} (α : ∀ x → A x → F A x) → (h : ∀ x → A x → M C x)
                     → (∀ (x : X) (a : A x) → out x (h x a) ≡ mapF h x (α x a))
                     → ∀ (x : X) (a : A x) m → h x a ≡ m → m ≡ unfold α x a
  unfold-η' α h eq x a m eq' = let heq = cong head (sym eq') ∙ cong fst (eq x a)
                               in \ where
                                    i .head → heq i
                                    i .tails y p →
                                     let  p0 = (transp-over-1 (\ k → C .snd x (heq k) y) i i1 p)
                                          p1 = (transp-over (\ k → C .snd x (heq k) y) i i0 p)
                                          pe = lem-transp i _ (\ k → C .snd x (heq k) y) p
                                          tl = compPathD (λ p → C .snd x p y → M C y)
                                                         (cong head (sym eq')) (cong fst (eq x a))
                                                         (cong (\ f → f .tails y) (sym eq'))
                                                         (cong (\ f → f .snd   y) (eq x a))
                                     in unfold-η' α h eq y (α x a .snd y p0)
                                                           (m .tails y p1)
                                                           (sym (\ k → tl k (pe k)))
                                                           i

  unfold-η : ∀ {A} (α : ∀ x → A x → F A x) → (h : ∀ x → A x → M C x)
                     → (∀ (x : X) (a : A x) → out x (h x a) ≡ mapF h x (α x a))
                     → ∀ (x : X) (a : A x) → h x a ≡ unfold α x a
  unfold-η α h eq x a = unfold-η' α h eq x a _ refl

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
-- Andreas, 2019-04-13, issue #3692, reported by xekoukou

-- Feature #1086, omission of trivially absurd clauses,
-- caused wrong polarity computation.

-- {-# OPTIONS -v tc.polarity:20 #-}
-- {-# OPTIONS -v tc.cover.missing:100 #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

data _≤_ : (m n : Nat) → Set where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
≤-pred (s≤s m≤n) = m≤n

data Fin : Nat → Set where
  fzero : (n : Nat) → Fin (suc n)
  fsuc  : (n : Nat) (i : Fin n) → Fin (suc n)

inject≤ : ∀ m n → Fin m → m ≤ n → Fin n
inject≤ m (suc n) (fzero _)   le = fzero _
inject≤ m (suc n) (fsuc m' i) le = fsuc _ (inject≤ m' n i (≤-pred le))
-- Agda 2.6.0 accepts inject≤ without the following clauses,
-- leading to faulty acceptance of test below.
-- inject≤ (suc _) zero (fzero _) ()
-- inject≤ (suc _) zero (fsuc _ _) ()

test : ∀ {m n} (i : Fin m) (m≤n m≤n' : m ≤ n)
     → inject≤ m n i m≤n ≡ inject≤ m n i m≤n'
test i m≤n m≤n' = refl

-- WAS: succeeded because of wrong polarity for inject≤

-- Expected error:

-- m≤n != m≤n' of type m ≤ n
-- when checking that the expression refl has type
-- inject≤ m n i m≤n ≡ inject≤ m n i m≤n'

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Instances.IntMod where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Unit
open import Cubical.Data.Bool hiding (isProp≤)
open import Cubical.Data.Nat renaming (_+_ to _+ℕ_)
open import Cubical.Data.Nat.Mod
open import Cubical.Data.Nat.Order
open import Cubical.Data.Int renaming (_+_ to _+ℤ_)
open import Cubical.Data.Fin
open import Cubical.Data.Fin.Arithmetic
open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid.Base
open import Cubical.Algebra.Semigroup.Base
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Instances.Unit
open import Cubical.Algebra.Group.Instances.Bool
open import Cubical.Algebra.Group.Instances.Int

open GroupStr
open IsGroup
open IsMonoid

ℤGroup/_ : ℕ → Group₀
ℤGroup/ zero = ℤGroup
fst (ℤGroup/ suc n) = Fin (suc n)
1g (snd (ℤGroup/ suc n)) = 0
GroupStr._·_ (snd (ℤGroup/ suc n)) = _+ₘ_
inv (snd (ℤGroup/ suc n)) = -ₘ_
isGroup (snd (ℤGroup/ suc n)) = makeIsGroup
                                isSetFin
                                (λ x y z → sym (+ₘ-assoc x y z))
                                +ₘ-rUnit
                                +ₘ-lUnit
                                +ₘ-rCancel
                                +ₘ-lCancel

ℤGroup/1≅Unit : GroupIso (ℤGroup/ 1) UnitGroup₀
ℤGroup/1≅Unit = contrGroupIsoUnit isContrFin1

Bool≅ℤGroup/2 : GroupIso BoolGroup (ℤGroup/ 2)
Iso.fun (fst Bool≅ℤGroup/2) false = 1
Iso.fun (fst Bool≅ℤGroup/2) true = 0
Iso.inv (fst Bool≅ℤGroup/2) (zero , p) = true
Iso.inv (fst Bool≅ℤGroup/2) (suc zero , p) = false
Iso.inv (fst Bool≅ℤGroup/2) (suc (suc x) , p) =
  ⊥.rec (¬-<-zero (predℕ-≤-predℕ (predℕ-≤-predℕ p)))
Iso.rightInv (fst Bool≅ℤGroup/2) (zero , p) =
  Σ≡Prop (λ _ → isProp≤) refl
Iso.rightInv (fst Bool≅ℤGroup/2) (suc zero , p) =
  Σ≡Prop (λ _ → isProp≤) refl
Iso.rightInv (fst Bool≅ℤGroup/2) (suc (suc x) , p) =
  ⊥.rec (¬-<-zero (predℕ-≤-predℕ (predℕ-≤-predℕ p)))
Iso.leftInv (fst Bool≅ℤGroup/2) false = refl
Iso.leftInv (fst Bool≅ℤGroup/2) true = refl
snd Bool≅ℤGroup/2 =
  makeIsGroupHom λ { false false → refl
                   ; false true → refl
                   ; true false → refl
                   ; true true → refl}

ℤGroup/2≅Bool : GroupIso (ℤGroup/ 2) BoolGroup
ℤGroup/2≅Bool = invGroupIso Bool≅ℤGroup/2

-- Definition of the quotient map homomorphism ℤ → ℤGroup/ (suc n)
-- as a group homomorphism.
ℤ→Fin : (n : ℕ) → ℤ → Fin (suc n)
ℤ→Fin n (pos x) = x mod (suc n) , mod< n x
ℤ→Fin n (negsuc x) = -ₘ (suc x mod suc n , mod< n (suc x))

ℤ→Fin-presinv : (n : ℕ) (x : ℤ) → ℤ→Fin n (- x) ≡ -ₘ ℤ→Fin n x
ℤ→Fin-presinv n (pos zero) =
  Σ≡Prop (λ _ → isProp≤) ((λ _ → zero) ∙ sym (cong fst help))
  where
  help : (-ₘ_ {n = n} 0) ≡ 0
  help = GroupTheory.inv1g (ℤGroup/ (suc n))
ℤ→Fin-presinv n (pos (suc x)) = Σ≡Prop (λ _ → isProp≤) refl
ℤ→Fin-presinv n (negsuc x) =
  sym (GroupTheory.invInv (ℤGroup/ (suc n)) _)

-ₘ1-id : (n : ℕ)
      → Path (Fin (suc n)) (-ₘ (1 mod (suc n) , mod< n 1))
                            (n mod (suc n) , mod< n n)
-ₘ1-id zero = refl
-ₘ1-id (suc n) =
     cong -ₘ_ (FinPathℕ ((1 mod suc (suc n)) , mod< (suc n) 1) 1
                (modIndBase (suc n) 1 (n , +-comm n 2)) .snd)
   ∙ Σ≡Prop (λ _ → isProp≤)
      ((+inductionBase (suc n) _
        (λ x _ → ((suc (suc n)) ∸ x) mod (suc (suc n))) λ _ x → x) 1
        (n , (+-comm n 2)))

suc-ₘ1 : (n y : ℕ)
  → ((suc y mod suc n) , mod< n (suc y)) -ₘ (1 mod (suc n) , mod< n 1)
   ≡ (y mod suc n , mod< n y)
suc-ₘ1 zero y =
  isContr→isProp
    (isOfHLevelRetractFromIso 0 (fst ℤGroup/1≅Unit) isContrUnit) _ _
suc-ₘ1 (suc n) y =
     (λ i → ((suc y mod suc (suc n)) , mod< (suc n) (suc y))
         +ₘ (-ₘ1-id (suc n) i))
   ∙ Σ≡Prop (λ _ → isProp≤)
      (cong (_mod (2 +ℕ n))
         (cong (_+ℕ (suc n) mod (2 +ℕ n))
           (mod+mod≡mod (suc (suc n)) 1 y))
      ∙∙ sym (mod+mod≡mod (suc (suc n))
             ((1 mod suc (suc n))
              +ℕ (y mod suc (suc n))) (suc n))
      ∙∙ (mod-rCancel (suc (suc n)) ((1 mod suc (suc n))
                                     +ℕ (y mod suc (suc n))) (suc n)
          ∙ cong (_mod (suc (suc n)))
           (cong (_+ℕ (suc n mod suc (suc n)))
                 (+-comm (1 mod suc (suc n)) (y mod suc (suc n)))
           ∙ sym (+-assoc (y mod suc (suc n))
                  (1 mod suc (suc n)) (suc n mod suc (suc n))))
      ∙∙ mod-rCancel (suc (suc n)) (y mod suc (suc n))
            ((1 mod suc (suc n)) +ℕ (suc n mod suc (suc n)))
      ∙∙ (cong (_mod (2 +ℕ n))
            (cong ((y mod suc (suc n)) +ℕ_)
                    (sym (mod+mod≡mod (suc (suc n)) 1 (suc n))
                  ∙ zero-charac (suc (suc n)))
                  ∙ +-comm _ 0)
       ∙ mod-idempotent y)))

1-ₘsuc : (n y : ℕ)
  →     ((1 mod (suc n) , mod< n 1)
     +ₘ (-ₘ (((suc y mod suc n) , mod< n (suc y)))))
       ≡ -ₘ ((y mod suc n) , mod< n y)
1-ₘsuc n y =
     sym (GroupTheory.invInv (ℤGroup/ (suc n)) _)
   ∙ cong -ₘ_
      (GroupTheory.invDistr (ℤGroup/ (suc n))
        (modInd n 1 , mod< n 1) (-ₘ (modInd n (suc y) , mod< n (suc y)))
      ∙ cong (_-ₘ (modInd n 1 , mod< n 1))
       (GroupTheory.invInv (ℤGroup/ (suc n)) (modInd n (suc y) , mod< n (suc y)))
       ∙ suc-ₘ1 n y)

isHomℤ→Fin : (n : ℕ) → IsGroupHom (snd ℤGroup) (ℤ→Fin n) (snd (ℤGroup/ (suc n)))
isHomℤ→Fin n =
  makeIsGroupHom
    λ { (pos x) y → pos+case x y
      ; (negsuc x) (pos y) →
             cong (ℤ→Fin n) (+Comm (negsuc x) (pos y))
          ∙∙ pos+case y (negsuc x)
          ∙∙ +ₘ-comm (ℤ→Fin n (pos y)) (ℤ→Fin n (negsuc x))
      ; (negsuc x) (negsuc y) →
           sym (cong (ℤ→Fin n) (-Dist+ (pos (suc x)) (pos (suc y))))
        ∙∙ ℤ→Fin-presinv n (pos (suc x) +ℤ (pos (suc y)))
        ∙∙ cong -ₘ_ (pos+case (suc x) (pos (suc y)))
        ∙∙ GroupTheory.invDistr (ℤGroup/ (suc n))
             (modInd n (suc x)
            , mod< n (suc x)) (modInd n (suc y) , mod< n (suc y))
        ∙∙ +ₘ-comm (ℤ→Fin n (negsuc y)) (ℤ→Fin n (negsuc x))}
  where
  +1case :  (y : ℤ) → ℤ→Fin n (1 +ℤ y) ≡ ℤ→Fin n 1 +ₘ ℤ→Fin n y
  +1case (pos zero) = sym (GroupStr.·IdR (snd (ℤGroup/ (suc n))) _)
  +1case (pos (suc y)) =
       cong (ℤ→Fin n) (+Comm 1 (pos (suc y)))
     ∙ Σ≡Prop (λ _ → isProp≤) (mod+mod≡mod (suc n) 1 (suc y))
  +1case (negsuc zero) =
      Σ≡Prop (λ _ → isProp≤) refl
    ∙ sym (GroupStr.·InvR (snd (ℤGroup/ (suc n))) (modInd n 1 , mod< n 1))
  +1case (negsuc (suc y)) =
    Σ≡Prop (λ _ → isProp≤)
      (cong fst (cong (ℤ→Fin n) (+Comm 1 (negsuc (suc y))))
      ∙∙ cong fst (cong -ₘ_ (refl {x = suc y mod suc n , mod< n (suc y)}))
      ∙∙ cong fst (sym (1-ₘsuc n (suc y)))
       ∙ λ i → fst ((1 mod (suc n) , mod< n 1)
         +ₘ (-ₘ (((suc (suc y) mod suc n) , mod< n (suc (suc y)))))))

  pos+case : (x : ℕ) (y : ℤ)
    → ℤ→Fin n (pos x +ℤ y) ≡ ℤ→Fin n (pos x) +ₘ ℤ→Fin n y
  pos+case zero y =
      cong (ℤ→Fin n) (+Comm 0 y)
    ∙ sym (GroupStr.·IdL (snd (ℤGroup/ (suc n))) (ℤ→Fin n y))
  pos+case (suc zero) y = +1case y
  pos+case (suc (suc x)) y =
       cong (ℤ→Fin n) (cong (_+ℤ y) (+Comm (pos (suc x)) 1)
                     ∙ sym (+Assoc 1 (pos (suc x)) y))
    ∙∙ +1case (pos (suc x) +ℤ y)
    ∙∙ (cong ((modInd n 1 , mod< n 1) +ₘ_) (pos+case (suc x) y)
     ∙∙ sym (+ₘ-assoc (modInd n 1 , mod< n 1)
              (modInd n (suc x) , mod< n (suc x)) (ℤ→Fin n y))
     ∙∙ cong (_+ₘ ℤ→Fin n y) (lem x))
    where
    lem : (x : ℕ)
      → (modInd n 1 , mod< n 1) +ₘ (modInd n (suc x) , mod< n (suc x))
        ≡ ℤ→Fin n (pos (suc (suc x)))
    lem x =
      Σ≡Prop (λ _ → isProp≤) (sym (mod+mod≡mod (suc n) 1 (suc x)))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import Categories.Category

module Categories.Functor.Slice {o ℓ e} (C : Category o ℓ e) where

open import Data.Product using (_,_)

open import Categories.Adjoint
open import Categories.Category.CartesianClosed
open import Categories.Category.CartesianClosed.Locally
open import Categories.Functor
open import Categories.Functor.Properties
open import Categories.Morphism.Reasoning C
open import Categories.NaturalTransformation

import Categories.Category.Slice as S
import Categories.Diagram.Pullback as P
import Categories.Category.Construction.Pullbacks as Pbs

open Category C
open HomReasoning

module _ {A : Obj} where
  open S.SliceObj
  open S.Slice⇒

  Base-F : ∀ {o′ ℓ′ e′} {D : Category o′ ℓ′ e′} (F : Functor C D) → Functor (S.Slice C A) (S.Slice D (Functor.F₀ F A))
  Base-F {D = D} F = record
    { F₀           = λ { (S.sliceobj arr) → S.sliceobj (F₁ arr) }
    ; F₁           = λ { (S.slicearr △) → S.slicearr ([ F ]-resp-∘ △) }
    ; identity     = identity
    ; homomorphism = homomorphism
    ; F-resp-≈     = F-resp-≈
    }
    where module D = Category D
          open Functor F

  open S C

  Forgetful : Functor (Slice A) C
  Forgetful = record
    { F₀           = λ X → Y X
    ; F₁           = λ f → h f
    ; identity     = refl
    ; homomorphism = refl
    ; F-resp-≈     = λ eq → eq
    }

  BaseChange! : ∀ {B} (f : B ⇒ A) → Functor (Slice B) (Slice A)
  BaseChange! f = record
    { F₀           = λ X → sliceobj (f ∘ arr X)
    ; F₁           = λ g → slicearr (pullʳ (△ g))
    ; identity     = refl
    ; homomorphism = refl
    ; F-resp-≈     = λ eq → eq
    }

  module _ (pullbacks : ∀ {X Y Z} (h : X ⇒ Z) (i : Y ⇒ Z) → P.Pullback C h i) where
    private
      open P C
      module pullbacks {X Y Z} h i = Pullback (pullbacks {X} {Y} {Z} h i)
      open pullbacks

    BaseChange* : ∀ {B} (f : B ⇒ A) → Functor (Slice A) (Slice B)
    BaseChange* f = record
      { F₀           = λ X → sliceobj (p₂ (arr X) f)
      ; F₁           = λ {X Y} g → slicearr {h = Pullback.p₂ (unglue (pullbacks (arr Y) f)
                                                                     (Pullback-resp-≈ (pullbacks (arr X) f) (△ g) refl))}
                                            (p₂∘universal≈h₂ (arr Y) f)
      ; identity     = λ {X} → ⟺ (unique (arr X) f id-comm identityʳ)
      ; homomorphism = λ {X Y Z} {h i} → unique-diagram (arr Z) f (p₁∘universal≈h₁ (arr Z) f ○ assoc ○ ⟺ (pullʳ (p₁∘universal≈h₁ (arr Y) f)) ○ ⟺ (pullˡ (p₁∘universal≈h₁ (arr Z) f)))
                                                                  (p₂∘universal≈h₂ (arr Z) f ○ ⟺ (p₂∘universal≈h₂ (arr Y) f) ○ ⟺ (pullˡ (p₂∘universal≈h₂ (arr Z) f)))
      ; F-resp-≈     = λ {X Y} eq″ → unique (arr Y) f (p₁∘universal≈h₁ (arr Y) f ○ ∘-resp-≈ˡ eq″) (p₂∘universal≈h₂ (arr Y) f)
      }

    !⊣* : ∀ {B} (f : B ⇒ A) →  BaseChange! f ⊣ BaseChange* f
    !⊣* f = record
      { unit   = ntHelper record
        { η       = λ X → slicearr (p₂∘universal≈h₂ (f ∘ arr X) f {eq = identityʳ})
        ; commute = λ {X Y} g → unique-diagram (f ∘ arr Y) f
                                               (cancelˡ (p₁∘universal≈h₁ (f ∘ arr Y) f) ○ ⟺ (cancelʳ (p₁∘universal≈h₁ (f ∘ arr X) f)) ○ pushˡ (⟺ (p₁∘universal≈h₁ (f ∘ arr Y) f)))
                                               (pullˡ (p₂∘universal≈h₂ (f ∘ arr Y) f) ○ △ g ○ ⟺ (p₂∘universal≈h₂ (f ∘ arr X) f) ○ pushˡ (⟺ (p₂∘universal≈h₂ (f ∘ arr Y) f)))
        }
      ; counit = ntHelper record
        { η       = λ X → slicearr (pullbacks.commute (arr X) f)
        ; commute = λ {X Y} g → p₁∘universal≈h₁ (arr Y) f
        }
      ; zig    = λ {X} → p₁∘universal≈h₁ (f ∘ arr X) f
      ; zag    = λ {Y} → unique-diagram (arr Y) f
                                        (pullˡ (p₁∘universal≈h₁ (arr Y) f) ○ pullʳ (p₁∘universal≈h₁ (f ∘ pullbacks.p₂ (arr Y) f) f))
                                        (pullˡ (p₂∘universal≈h₂ (arr Y) f) ○ p₂∘universal≈h₂ (f ∘ pullbacks.p₂ (arr Y) f) f ○ ⟺ identityʳ)
      }

    pullback-functorial : ∀ {B} (f : B ⇒ A) → Functor (Slice A) C
    pullback-functorial f = record
      { F₀           = λ X → p.P X
      ; F₁           = λ f → p⇒ _ _ f
      ; identity     = λ {X} → sym (p.unique X id-comm id-comm)
      ; homomorphism = λ {_ Y Z} →
        p.unique-diagram Z (p.p₁∘universal≈h₁ Z ○ ⟺ identityˡ ○ ⟺ (pullʳ (p.p₁∘universal≈h₁ Y)) ○ ⟺ (pullˡ (p.p₁∘universal≈h₁ Z)))
                           (p.p₂∘universal≈h₂ Z ○ assoc ○ ⟺ (pullʳ (p.p₂∘universal≈h₂ Y)) ○ ⟺ (pullˡ (p.p₂∘universal≈h₂ Z)))
      ; F-resp-≈     = λ {_ B} {h i} eq →
        p.unique-diagram B (p.p₁∘universal≈h₁ B ○ ⟺ (p.p₁∘universal≈h₁ B))
                           (p.p₂∘universal≈h₂ B ○ ∘-resp-≈ˡ eq ○ ⟺ (p.p₂∘universal≈h₂ B))
      }
      where p : ∀ X → Pullback f (arr X)
            p X        = pullbacks f (arr X)
            module p X = Pullback (p X)

            p⇒ : ∀ X Y (g : Slice⇒ X Y) → p.P X ⇒ p.P Y
            p⇒ X Y g = Pbs.Pullback⇒.pbarr pX⇒pY
              where pX : Pbs.PullbackObj C A
                    pX = record { pullback = p X }
                    pY : Pbs.PullbackObj C A
                    pY = record { pullback = p Y }
                    pX⇒pY : Pbs.Pullback⇒ C A pX pY
                    pX⇒pY = record
                      { mor₁     = Category.id C
                      ; mor₂     = h g
                      ; commute₁ = identityʳ
                      ; commute₂ = △ g
                      }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Data.Vec.Any.Properties where

open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; inspect; refl)
open import Relation.Unary renaming (_⊆_ to _⋐_) using ()
open import Data.Product as Prod hiding (map; swap)
open import Data.Vec as Vec
open import Data.Vec.Any as Any
open import Data.Vec.Any.Membership.Propositional
--open import Data.Vec.Membership
open import Data.Bool.Base using (Bool; false; true; T)
open import Data.Bool.Properties
open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Data.Sum as Sum hiding (map)
open import Function using (_∘_; _$_; id; flip; const)
open import Function.Inverse as Inv using (_↔_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Eq using (_⇔_ ; module Equivalence)
open import Function.Related as Related using (Related)
open Related.EquationalReasoning
open import Relation.Binary.Sum

map-id : ∀ {a p n}  {A : Set a} {P : A → Set p} (f : P ⋐ P) {xs : Vec A n} →
         (∀ {x} (p : P x) → f p ≡ p) →
         (p : Any P xs) → Any.map f p ≡ p
map-id f hyp (here px) = P.cong here $ hyp px
map-id f hyp (there p) = P.cong there $ map-id f hyp p

map-∘  : ∀ {a p q r n}{A : Set a}{P : A → Set p}{Q : A → Set q}{R : A → Set r}
         (f : Q ⋐ R)(g : P ⋐ Q) {xs : Vec A n}(p : Any P xs) →
         Any.map (f ∘ g) p ≡ Any.map f (Any.map g p)

map-∘ f g (here px) = P.refl
map-∘ f g (there p) = P.cong there $ map-∘ f g p

map∘find′ : ∀ {a n p}{A : Set a} {P : A → Set p}{xs : Vec A n} (p : Any P xs) →
         let (x , x∈xs , px) = find′ p in
           {f : (x ≡_) ⋐ P } →
           f P.refl ≡ px     →
           Any.map f x∈xs ≡ p
map∘find′ (here px) hyp = P.cong here hyp
map∘find′ (there pxs) hyp = P.cong there $ map∘find′ pxs hyp

find′∘map : ∀ {a n p q}{A : Set a}{P : A → Set p}{Q : A → Set q}{xs : Vec A n}(p : Any P xs)(f : P ⋐ Q) →
           find′ (Any.map f p) ≡ Prod.map id (Prod.map id f) (find′ p)
find′∘map (here px) f = P.refl
find′∘map (there pxs) f rewrite find′∘map pxs f = P.refl

find′-∈′ : ∀ {a n}{A : Set a}{x}{xs : Vec A n}(x∈xs : x ∈′ xs) →
  find′ x∈xs ≡ (x , x∈xs , P.refl)
find′-∈′ (here P.refl) = P.refl
find′-∈′ (there x∈xs) rewrite find′-∈′ x∈xs = P.refl

lose′∘find′ : ∀ {a n p}{A : Set a} {P : A → Set p}{xs : Vec A n} (p : Any P xs) →
  uncurry′ lose′ (proj₂ (find′ p)) ≡ p
lose′∘find′ (here px) = P.refl
lose′∘find′ (there p) = P.cong there $ lose′∘find′ p

find′∘lose′ : ∀ {a n p}{A : Set a} (P : A → Set p){x}{xs : Vec A n} (x∈xs : x ∈′ xs)(px : P x) →
  find′ {P = P} (lose′ x∈xs px) ≡ (x , x∈xs , px)
find′∘lose′ P x∈xs px rewrite find′∘map x∈xs (flip (P.subst P) px) | find′-∈′ x∈xs = P.refl

∃∈-Any : ∀ {a p n}{A : Set a} {P : A → Set p}{xs : Vec A n} →
         (∃ λ x → x ∈′ xs × P x) → Any P xs
∃∈-Any = uncurry′ lose′ ∘ proj₂

Any↔  : ∀ {a p n}{A : Set a} {P : A → Set p}{xs : Vec A n} →
  (∃ λ x → x ∈′ xs × P x) ↔ Any P xs

Any↔ {P = P}{xs} = record {
     to = P.→-to-⟶ ∃∈-Any
   ; from = P.→-to-⟶ (find′ {P = P})
   ; inverse-of = record {
         left-inverse-of = λ { (x , x∈xs , px) → find′∘lose′ P x∈xs px}
       ; right-inverse-of = lose′∘find′
     }
  }

Any-cong : ∀ {k a p m n} {A : Set a} {P₁ P₂ : A → Set p} {xs₁ : Vec A m} {xs₂ : Vec A n} →
           (∀ x → Related k (P₁ x) (P₂ x)) → xs₁ ∼[ k ] xs₂ → Related k (Any P₁ xs₁) (Any P₂ xs₂)
Any-cong {P₁ = P₁}{P₂}{xs₁}{xs₂} P₁∼P₂ xs₁∼xs₂ =
  Any P₁ xs₁ ↔⟨ sym $ Any↔ {P = P₁} ⟩ (∃ λ x → x ∈′ xs₁ × P₁ x)
               ∼⟨ Σ.cong Inv.id (xs₁∼xs₂ ×-cong P₁∼P₂ _) ⟩(∃ λ x → x ∈′ xs₂ × P₂ x)
             ↔⟨ Any↔ {P = P₂} ⟩  Any P₂ xs₂ ∎
  where
    open import Relation.Binary.Product.Pointwise
    import Relation.Binary.Sigma.Pointwise as Σ

swap : ∀ {a b p}{A : Set a}{B : Set b}{P : A → B → Set p}
  {m n}{xs : Vec A m}{ys : Vec B n} → Any (λ x → Any (P x) ys) xs → Any (λ y → (Any (flip P y) xs)) ys
swap (here pys) = Any.map here pys
swap (there pxys) = Any.map there $ swap pxys

swap-there : ∀ {a b p}{A : Set a}{B : Set b}{P : A → B → Set p}
    {m n x}{xs : Vec A m}{ys : Vec B n}(any : Any (λ x → Any (P x) ys) xs) →
    swap (Any.map (there {x = x}) any) ≡ there (swap any)
swap-there (here pys) = P.refl
swap-there (there pxys) = P.cong (Any.map there) $ swap-there pxys

swap-invol : ∀ {a b p}{A : Set a}{B : Set b}{P : A → B → Set p}
    {m n}{xs : Vec A m}{ys : Vec B n}(any : Any (λ x → Any (P x) ys) xs) →
      swap (swap any) ≡ any
swap-invol (here (here px)) = P.refl
swap-invol (here (there pys)) = P.cong (Any.map there) $ swap-invol (here pys)
swap-invol (there pxys) = P.trans (swap-there (swap pxys)) $ P.cong there $ swap-invol pxys

swap↔ : ∀ {a b p}{A : Set a}{B : Set b}{P : A → B → Set p}
    {m n}{xs : Vec A m}{ys : Vec B n} →
    Any (λ x → Any (P x) ys) xs ↔  Any (λ y → (Any (flip P y) xs)) ys
swap↔ = record {
    to = P.→-to-⟶ swap
  ; from = P.→-to-⟶ swap
  ; inverse-of = record {
     left-inverse-of = swap-invol
   ; right-inverse-of = swap-invol
  }
  }

⊥↔Any⊥ : ∀ {a n}{A : Set a}{xs : Vec A n} → ⊥ ↔ Any (const ⊥) xs
⊥↔Any⊥ {A = A} = record {
    to = P.→-to-⟶ λ()
  ; from = P.→-to-⟶ (λ p → from p)
  ; inverse-of = record {
      left-inverse-of = λ()
    ; right-inverse-of = λ p → from p
  }
  }
  where
    from : ∀ {n}{xs : Vec A n} → Any (const ⊥) xs → ∀ {b} {B : Set b} → B
    from (here ())
    from (there p) = from p

⊥↔Any[] : ∀ {a}{A : Set a}{P : A → Set}  → ⊥ ↔ Any P []
⊥↔Any[] = record {
    to = P.→-to-⟶ λ()
  ; from = P.→-to-⟶ λ()
  ; inverse-of = record {
      left-inverse-of = λ()
    ; right-inverse-of = λ()
  }
  }

-- any⇔

module _ {a p q}{A : Set a}{P : A → Set p}{Q : A → Set q} where
  Any-⊎⁺ : ∀{n}{xs : Vec A n} → Any P xs ⊎ Any Q xs → Any (λ x → P x ⊎ Q x) xs
  Any-⊎⁺ = [ Any.map inj₁  , Any.map inj₂ ]′

  Any-⊎⁻ : ∀{n}{xs : Vec A n} → Any (λ x → P x ⊎ Q x) xs → Any P xs ⊎ Any Q xs
  Any-⊎⁻ (here (inj₁ px)) = inj₁ (here px)
  Any-⊎⁻ (here (inj₂ qx)) = inj₂ (here qx)
  Any-⊎⁻ (there p) = Sum.map there there (Any-⊎⁻ p)

  ⊎↔ : ∀ {n}{xs : Vec A n} → (Any P xs ⊎ Any Q xs) ↔ Any (λ x → P x ⊎ Q x) xs
  ⊎↔ = record
    { to         = P.→-to-⟶ Any-⊎⁺
    ; from       = P.→-to-⟶ Any-⊎⁻
    ; inverse-of = record
      { left-inverse-of  = from∘to
      ; right-inverse-of = to∘from
      }
    }
    where

    from∘to : ∀ {n}{xs : Vec A n} (p : Any P xs ⊎ Any Q xs) → Any-⊎⁻ (Any-⊎⁺ p) ≡ p
    from∘to (inj₁ (here  p)) = P.refl
    from∘to (inj₁ (there p)) rewrite from∘to (inj₁ p) = P.refl
    from∘to (inj₂ (here  q)) = P.refl
    from∘to (inj₂ (there q)) rewrite from∘to (inj₂ q) = P.refl

    to∘from : ∀ {n}{xs : Vec A n} (p : Any (λ x → P x ⊎ Q x) xs) →
              Any-⊎⁺ (Any-⊎⁻ p) ≡ p
    to∘from (here (inj₁ p)) = P.refl
    to∘from (here (inj₂ q)) = P.refl
    to∘from (there p) with Any-⊎⁻ p | to∘from p
    to∘from (there .(Any.map inj₁ p)) | inj₁ p | P.refl = P.refl
    to∘from (there .(Any.map inj₂ q)) | inj₂ q | P.refl = P.refl

module _ {a b p q} {A : Set a} {B : Set b}
         {P : A → Set p} {Q : B → Set q} where

  Any-×⁺ : ∀ {m n}{xs : Vec A m} {ys : Vec B n} → Any P xs × Any Q ys →
           Any (λ x → Any (λ y → P x × Q y) ys) xs
  Any-×⁺ (p , q) = Any.map (λ p → Any.map (λ q → (p , q)) q) p

  Any-×⁻ : ∀ {m n} {xs : Vec A m}{ys : Vec B n} → Any (λ x → Any (λ y → P x × Q y) ys) xs →
           Any P xs × Any Q ys
  Any-×⁻ pq with Prod.map id (Prod.map id find′) (find′ pq)
  ... | (x , x∈xs , y , y∈ys , p , q) = (lose′ x∈xs p , lose′ y∈ys q)

  ×↔ : ∀ {m n} {xs : Vec A m}{ys : Vec B n} →
       (Any P xs × Any Q ys) ↔ Any (λ x → Any (λ y → P x × Q y) ys) xs
  ×↔ {m}{n}{xs} {ys} = record
    { to         = P.→-to-⟶ Any-×⁺
    ; from       = P.→-to-⟶ Any-×⁻
    ; inverse-of = record
      { left-inverse-of  = from∘to
      ; right-inverse-of = to∘from
      }
    }
    where
      from∘to : ∀ (pq : Any P xs × Any Q ys)
        → Any-×⁻ (Any-×⁺ pq) ≡ pq
      from∘to (p , q)
        rewrite find′∘map {Q = λ x → Any (λ y → P x × Q y) ys}
                       p (λ px → Any.map (λ q → (px , q)) q)
              | find′∘map {Q = λ y → P (proj₁ (find′ p)) × Q y}
                         q (λ q → proj₂ (proj₂ (find′ p)) , q)
              | lose′∘find′ p
              | lose′∘find′ q
              = P.refl

      to∘from : ∀ (pq :  Any (λ x → Any (λ y → P x × Q y) ys) xs) → Any-×⁺ (Any-×⁻ pq) ≡ pq
      to∘from pq  with find′ pq
              | (λ (f : (proj₁ (find′ pq) ≡_) ⋐ _) → map∘find′ pq {f})
      ... | (x , x∈xs , pq′) | lem₁
        with find′ pq′
          | (λ (f : (proj₁ (find′ pq′) ≡_) ⋐ _) → map∘find′ pq′ {f})
      ... | (y , y∈ys , p , q) | lem₂
        rewrite P.sym $ map-∘ {R = λ x → Any (λ y → P x × Q y) ys}
                              (λ p → Any.map (λ q → p , q) (lose′ y∈ys q))
                              (λ y → P.subst P y p)
                              x∈xs
                = lem₁ _ helper
        where
          helper : Any.map (λ q → p , q) (lose′ y∈ys q) ≡ pq′
          helper rewrite P.sym $ map-∘ {R = λ y → P x × Q y}
                                     (λ q → p , q)
                                     (λ y → P.subst Q y q)
                                     y∈ys
                 = lem₂ _ P.refl

module _ {a b} {A : Set a} {B : Set b} where
  map⁺ : ∀ {p} {P : B → Set p} {f : A → B}{n}{xs : Vec A n} →
         Any (P ∘ f) xs → Any P (Vec.map f xs)
  map⁺ (here pfx) = here pfx
  map⁺ (there p) = there (map⁺ p)

  map⁻ : ∀ {p} {P : B → Set p} {f : A → B} {n}{xs : Vec A n} →
         Any P (Vec.map f xs) → Any (P ∘ f) xs
  map⁻ {xs = []}     ()
  map⁻ {xs = x ∷ xs} (here p)  = here p
  map⁻ {xs = x ∷ xs} (there p) = there $ map⁻ p

  map⁺∘map⁻ : ∀ {p} {P : B → Set p} {f : A → B}{n}{xs : Vec A n} →
              (p : Any P (Vec.map f xs)) → map⁺ (map⁻ p) ≡ p
  map⁺∘map⁻ {xs = []}     ()
  map⁺∘map⁻ {xs = x ∷ xs} (here  p) = P.refl
  map⁺∘map⁻ {xs = x ∷ xs} (there p) = P.cong there (map⁺∘map⁻ p)

  map⁻∘map⁺ : ∀ {p} (P : B → Set p) {f : A → B}{n} {xs : Vec A n} →
              (p : Any (P ∘ f) xs) → map⁻ {P = P} (map⁺ p) ≡ p
  map⁻∘map⁺ P (here  p) = P.refl
  map⁻∘map⁺ P (there p) = P.cong there (map⁻∘map⁺ P p)

  map↔ : ∀ {p} {P : B → Set p} {f : A → B} {n}{xs : Vec A n} →
         Any (P ∘ f) xs ↔ Any P (Vec.map f xs)
  map↔ {P = P} {f = f} = record
    { to         = P.→-to-⟶ $ map⁺ {P = P} {f = f}
    ; from       = P.→-to-⟶ $ map⁻ {P = P} {f = f}
    ; inverse-of = record
      { left-inverse-of  = map⁻∘map⁺ P
      ; right-inverse-of = map⁺∘map⁻
      }
    }
------------------------------------------------------------------------

-- _++_

module _ {a p} {A : Set a} {P : A → Set p} where

  ++⁺ˡ : ∀ {m n}{xs : Vec A m} {ys : Vec A n} → Any P xs → Any P (xs ++ ys)
  ++⁺ˡ (here p)  = here p
  ++⁺ˡ (there p) = there (++⁺ˡ p)

  ++⁺ʳ : ∀ {m n} (xs : Vec A m) {ys : Vec A n} → Any P ys → Any P (xs ++ ys)
  ++⁺ʳ []       p = p
  ++⁺ʳ (x ∷ xs) p = there (++⁺ʳ xs p)

  ++⁻ : ∀ {m n} (xs : Vec A m) {ys : Vec A n} → Any P (xs ++ ys) → Any P xs ⊎ Any P ys
  ++⁻ []       p         = inj₂ p
  ++⁻ (x ∷ xs) (here p)  = inj₁ (here p)
  ++⁻ (x ∷ xs) (there p) = Sum.map there id (++⁻ xs p)

  ++⁺∘++⁻ : ∀{m n} (xs : Vec A m) {ys : Vec A n} (p : Any P (xs ++ ys)) →
            [ ++⁺ˡ , ++⁺ʳ xs ]′ (++⁻ xs p) ≡ p
  ++⁺∘++⁻ []       p         = refl
  ++⁺∘++⁻ (x ∷ xs) (here  p) = refl
  ++⁺∘++⁻ (x ∷ xs) (there p) with ++⁻ xs p | ++⁺∘++⁻ xs p
  ++⁺∘++⁻ (x ∷ xs) (there p) | inj₁ p′ | ih = P.cong there ih
  ++⁺∘++⁻ (x ∷ xs) (there p) | inj₂ p′ | ih = P.cong there ih

  ++⁻∘++⁺ : ∀{m n} (xs : Vec A m) {ys : Vec A n} (p : Any P xs ⊎ Any P ys) →
            ++⁻ xs ([ ++⁺ˡ , ++⁺ʳ xs ]′ p) ≡ p
  ++⁻∘++⁺ []            (inj₁ ())
  ++⁻∘++⁺ []            (inj₂ p)         = refl
  ++⁻∘++⁺ (x ∷ xs)      (inj₁ (here  p)) = refl
  ++⁻∘++⁺ (x ∷ xs) {ys} (inj₁ (there p)) rewrite ++⁻∘++⁺ xs {ys} (inj₁ p) = refl
  ++⁻∘++⁺ (x ∷ xs)      (inj₂ p)         rewrite ++⁻∘++⁺ xs      (inj₂ p) = refl

  ++↔ : ∀{m n} {xs : Vec A m}{ys : Vec A n} → (Any P xs ⊎ Any P ys) ↔ Any P (xs ++ ys)
  ++↔ {xs = xs} = record
    { to         = P.→-to-⟶ [ ++⁺ˡ , ++⁺ʳ xs ]′
    ; from       = P.→-to-⟶ $ ++⁻ xs
    ; inverse-of = record
      { left-inverse-of  = ++⁻∘++⁺ xs
      ; right-inverse-of = ++⁺∘++⁻ xs
      }
    }

  ++-comm : ∀ {m n} (xs : Vec A m) (ys : Vec A n) → Any P (xs ++ ys) → Any P (ys ++ xs)
  ++-comm xs ys = [ ++⁺ʳ ys , ++⁺ˡ ]′ ∘ ++⁻ xs

  ++-comm∘++-comm : ∀{m n} (xs : Vec A m) {ys : Vec A n} (p : Any P (xs ++ ys)) →
                    ++-comm ys xs (++-comm xs ys p) ≡ p
  ++-comm∘++-comm [] {ys} p
    rewrite ++⁻∘++⁺ ys {ys = []} (inj₁ p) = P.refl
  ++-comm∘++-comm (x ∷ xs) {ys} (here p)
    rewrite ++⁻∘++⁺ ys {ys = x ∷ xs} (inj₂ (here p)) = P.refl
  ++-comm∘++-comm (x ∷ xs)      (there p) with ++⁻ xs p | ++-comm∘++-comm xs p
  ++-comm∘++-comm (x ∷ xs) {ys} (there .([ ++⁺ʳ xs , ++⁺ˡ ]′ (++⁻ ys (++⁺ʳ ys p))))
    | inj₁ p | P.refl
    rewrite ++⁻∘++⁺ ys (inj₂                 p)
            | ++⁻∘++⁺ ys (inj₂ $ there {x = x} p) = P.refl
  ++-comm∘++-comm (x ∷ xs) {ys} (there .([ ++⁺ʳ xs , ++⁺ˡ ]′ (++⁻ ys (++⁺ˡ p))))
    | inj₂ p | P.refl
    rewrite ++⁻∘++⁺ ys {ys =     xs} (inj₁ p)
            | ++⁻∘++⁺ ys {ys = x ∷ xs} (inj₁ p) = P.refl

  ++↔++ : ∀{m n} (xs : Vec A m) (ys : Vec A n) → Any P (xs ++ ys) ↔ Any P (ys ++ xs)
  ++↔++ xs ys = record
    { to         = P.→-to-⟶ $ ++-comm xs ys
    ; from       = P.→-to-⟶ $ ++-comm ys xs
    ; inverse-of = record
      { left-inverse-of  = ++-comm∘++-comm xs
      ; right-inverse-of = ++-comm∘++-comm ys
      }
    }

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

-- tabulate

module _ {a p} {A : Set a} {P : A → Set p} where
  tabulate⁺ : ∀ {n} {f : Fin n → A} i → P (f i) → Any P (tabulate f)
  tabulate⁺ fzero    p = here p
  tabulate⁺ (fsuc i) p = there (tabulate⁺ i p)

  tabulate⁻ : ∀ {n} {f : Fin n → A} →
              Any P (tabulate f) → ∃ λ i → P (f i)
  tabulate⁻ {zero}  ()
  tabulate⁻ {suc n} (here p)   = fzero , p
  tabulate⁻ {suc n} (there p) = Prod.map fsuc id (tabulate⁻ p)

------------------------------------------------------------------------
-- map-with-∈.

module _ {a b p} {A : Set a} {B : Set b} {P : B → Set p} where

  map-with-∈′⁺ : ∀ {n}{xs : Vec A n} (f : ∀ {x} → x ∈′ xs → B) →
                (∃₂ λ x (x∈xs : x ∈′ xs) → P (f x∈xs)) →
                Any P (map-with-∈′ xs f)
  map-with-∈′⁺ f (_ , here refl  , p) = here p
  map-with-∈′⁺ f (_ , there x∈xs , p) =
    there $ map-with-∈′⁺ (f ∘ there) (_ , x∈xs , p)

  map-with-∈′⁻ : ∀ {n} (xs : Vec A n) (f : ∀ {x} → x ∈′ xs → B) →
                Any P (map-with-∈′ xs f) →
                ∃₂ λ x (x∈xs : x ∈′ xs) → P (f x∈xs)
  map-with-∈′⁻ []       f ()
  map-with-∈′⁻ (y ∷ xs) f (here  p) = (y , here refl , p)
  map-with-∈′⁻ (y ∷ xs) f (there p) =
    Prod.map id (Prod.map there id) $ map-with-∈′⁻ xs (f ∘ there) p

  map-with-∈′↔ : ∀{n}{xs : Vec A n} {f : ∀ {x} → x ∈′ xs → B} →
    (∃₂ λ x (x∈xs : x ∈′ xs) → P (f x∈xs)) ↔ Any P (map-with-∈′ xs f)
  map-with-∈′↔ = record
    { to         = P.→-to-⟶ (map-with-∈′⁺ _)
    ; from       = P.→-to-⟶ (map-with-∈′⁻ _ _)
    ; inverse-of = record
      { left-inverse-of  = from∘to _
      ; right-inverse-of = to∘from _ _
      }
    }
    where

    from∘to : ∀ {n} {xs : Vec A n} (f : ∀ {x} → x ∈′ xs → B)
              (p : ∃₂ λ x (x∈xs : x ∈′ xs) → P (f x∈xs)) →
              map-with-∈′⁻ xs f (map-with-∈′⁺ f p) ≡ p
    from∘to f (_ , here refl  , p) = refl
    from∘to f (_ , there x∈xs , p)
      rewrite from∘to (f ∘ there) (_ , x∈xs , p) = refl

    to∘from : ∀ {n}(xs : Vec A n) (f : ∀ {x} → x ∈′ xs → B)
              (p : Any P (map-with-∈′ xs f)) →
              map-with-∈′⁺ f (map-with-∈′⁻ xs f p) ≡ p
    to∘from []       f ()
    to∘from (y ∷ xs) f (here  p) = refl
    to∘from (y ∷ xs) f (there p) =
      P.cong there $ to∘from xs (f ∘ there) p

------------------------------------------------------------------------
module _ {a p} {A : Set a} {P : A → Set p} where
  return⁺ : ∀ {x} → P x → Any P ([ x ])
  return⁺ = here

  return⁻ : ∀ {x} → Any P ([ x ]) → P x
  return⁻ (here p)   = p
  return⁻ (there ())

  return⁺∘return⁻ : ∀ {x} (p : Any P [ x ]) →
                    return⁺ (return⁻ p) ≡ p
  return⁺∘return⁻ (here p)   = refl
  return⁺∘return⁻ (there ())

  return⁻∘return⁺ : ∀ {x} (p : P x) → return⁻ (return⁺ p) ≡ p
  return⁻∘return⁺ p = refl

  return↔ : ∀ {x} → P x ↔ Any P ([ x ])
  return↔ = record
    { to         = P.→-to-⟶ $ return⁺
    ; from       = P.→-to-⟶ $ return⁻
    ; inverse-of = record
      { left-inverse-of  = return⁻∘return⁺
      ; right-inverse-of = return⁺∘return⁻
      }
    }

-- _∷_.

∷↔ : ∀ {a p n} {A : Set a} (P : A → Set p) {x} {xs : Vec A n} →
     (P x ⊎ Any P xs) ↔ Any P (x ∷ xs)
∷↔ P {x} {xs} =
  (P x         ⊎ Any P xs)  ↔⟨ return↔ {P = P} ⊎-cong (Any P xs ∎) ⟩
  (Any P [ x ] ⊎ Any P xs)  ↔⟨ ++↔ {P = P} {xs = [ x ]} ⟩
  Any P (x ∷ xs)            ∎

max_stars_repo_name: tizmd/agda-vector-any

max_issues_repo_name: tizmd/agda-vector-any

max_forks_repo_name: tizmd/agda-vector-any


text:
{-# OPTIONS -v tc.unquote.clause:30 #-}

open import Common.Reflection
open import Common.Prelude

data Box : Set → Set₁ where
  box : (A : Set) → Box A

unquoteDecl test = define (vArg test) (funDef
 (pi
   (vArg (sort (lit 0)))
   (abs "A" (pi
    (vArg (def (quote Box) (vArg (var 0 []) ∷ [])))
    (abs "x" (sort (lit 0))))))
 (clause
   (vArg dot ∷
    vArg (con (quote box) (vArg (var "dot") ∷ [])) ∷ [])
   (var 1 [])
 ∷ []))

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
-- A generic proof of confluence for a rewriting system with the diamond property.

module Confluence where

open import Prelude

postulate
  Tm : Set
  _=>_ : Tm -> Tm -> Set
  diamond : ∀{M N P : Tm} → (M => N) → (M => P) →
            Σ[ Q :: Tm ] (N => Q × P => Q)

data _=>*_ : Tm → Tm → Set where
  eval-refl : {e : Tm} → e =>* e
  eval-cons : {e e' e'' : Tm} →
              (S1 : e => e') → (D : e' =>* e'') → e =>* e''

strip : ∀{M N P : Tm} → (M => N) → (M =>* P) →
         Σ[ Q :: Tm ] (N =>* Q × P => Q)
strip S1 eval-refl = , (eval-refl , S1)
strip S1 (eval-cons S2 D) with diamond S1 S2
... | Q' , S1' , S2' with strip S2' D
... | Q , D1 , S' = Q , ((eval-cons S1' D1) , S')

confluence : ∀{M N P : Tm} → (M =>* N) → (M =>* P) →
             Σ[ Q :: Tm ] (N =>* Q × P =>* Q)
confluence eval-refl D2 = , (D2 , eval-refl)
confluence (eval-cons S1 D1) D2 with strip S1 D2
... | M' , D3 , S3 with confluence D1 D3
... | Q , D4 , D4' = Q , D4 , eval-cons S3 D4'

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text:
{-# OPTIONS --without-K #-}
-- The core properties behind exploration functions
module Explore.Properties where

open import Level.NP using (_⊔_; ₀; ₁; ₛ; Lift)
open import Type using (★₀; ★₁; ★_)
open import Function.NP using (id; _∘′_; _∘_; flip; const; Π; Cmp)
open import Algebra using (Semigroup; module Semigroup; Monoid; module Monoid; CommutativeMonoid; module CommutativeMonoid)
import      Algebra.FunctionProperties.NP
import      Algebra.FunctionProperties.Derived as FPD
open import Algebra.FunctionProperties.Core using (Op₂)
import Algebra.FunctionProperties.Eq
open Algebra.FunctionProperties.Eq.Explicits using (Injective)
open import Data.Nat.NP using (_+_; _*_; _≤_; _+°_)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂)
open import Data.Sum  using (_⊎_)
open import Data.Zero using (𝟘)
open import Data.One  using (𝟙)
open import Data.Two  using (𝟚; ✓)
open import Data.Fin  using (Fin)
open import Relation.Binary.NP using (module Setoid-Reasoning; _Preserves₂_⟶_⟶_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_)

open import Explore.Core

module FP = Algebra.FunctionProperties.NP Π

module SgrpExtra {c ℓ} (sg : Semigroup c ℓ) where
  open Semigroup sg
  open Setoid-Reasoning (Semigroup.setoid sg) public
  C : ★ _
  C = Carrier
  _≈°_ : ∀ {a} {A : ★ a} (f g : A → C) → ★ _
  f ≈° g = ∀ x → f x ≈ g x
  _∙°_   : ∀ {a} {A : ★ a} (f g : A → C) → A → C
  (f ∙° g) x = f x ∙ g x
  infixl 7 _-∙-_
  _-∙-_ : _∙_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
  _-∙-_ = ∙-cong
  !_ = sym

module Sgrp {c ℓ} (sg : Semigroup c ℓ) where
  open Semigroup sg public
  open SgrpExtra sg public

module RawMon {c} {C : ★ c} (rawMon : C × Op₂ C) where
  ε    = proj₁ rawMon
  _∙_  = proj₂ rawMon

module Mon {c ℓ} (m : Monoid c ℓ) where
  open Monoid m public
  sg = semigroup
  open SgrpExtra semigroup public
  RawMon = C × Op₂ C
  rawMon : RawMon
  rawMon = ε , _∙_

module CMon {c ℓ} (cm : CommutativeMonoid c ℓ) where
  open CommutativeMonoid cm public
  sg = semigroup
  m = monoid
  open SgrpExtra sg public
  open FP _≈_

  ∙-interchange : Interchange _∙_ _∙_
  ∙-interchange = FPD.FromAssocCommCong.interchange
                    _≈_ isEquivalence
                    _∙_ assoc comm (λ _ → flip ∙-cong refl)

module _ {ℓ a} {A : ★ a} where
    ExploreInd : ∀ p → Explore ℓ A → ★ (a ⊔ ₛ (ℓ ⊔ p))
    ExploreInd p exp =
      ∀ (P  : Explore ℓ A → ★ p)
        (Pε : P empty-explore)
        (P∙ : ∀ {e₀ e₁ : Explore ℓ A} → P e₀ → P e₁ → P (merge-explore e₀ e₁))
        (Pf : ∀ x → P (point-explore x))
      → P exp

    module _ {p} where
        point-explore-ind : (x : A) → ExploreInd p (point-explore x)
        point-explore-ind x _ _ _ Pf = Pf x

        empty-explore-ind : ExploreInd p empty-explore
        empty-explore-ind _ Pε _ _ = Pε

        merge-explore-ind : ∀ {e₀ e₁ : Explore ℓ A}
                            → ExploreInd p e₀ → ExploreInd p e₁
                            → ExploreInd p (merge-explore e₀ e₁)
        merge-explore-ind Pe₀ Pe₁ P Pε _P∙_ Pf = (Pe₀ P Pε _P∙_ Pf) P∙ (Pe₁ P Pε _P∙_ Pf)

    ExploreInd₀ : Explore ℓ A → ★ _
    ExploreInd₀ = ExploreInd ₀

    ExploreInd₁ : Explore ℓ A → ★ _
    ExploreInd₁ = ExploreInd ₁

    BigOpMonInd : ∀ p {c} (M : Monoid c ℓ) → BigOpMon M A → ★ _
    BigOpMonInd p {c} M exp =
      ∀ (P  : BigOpMon M A → ★ p)
        (Pε : P (const ε))
        (P∙ : ∀ {e₀ e₁ : BigOpMon M A} → P e₀ → P e₁ → P (λ f → e₀ f ∙ e₁ f))
        (Pf : ∀ x → P (λ f → f x))
        (P≈ : ∀ {e e'} → e ≈° e' → P e → P e')
      → P exp
      where open Mon M

    module _ (eᴬ : Explore {a} (ₛ ℓ) A) where
        Πᵉ : (A → ★ ℓ) → ★ ℓ
        Πᵉ = eᴬ (Lift 𝟙) _×_

        Σᵉ : (A → ★ ℓ) → ★ ℓ
        Σᵉ = eᴬ (Lift 𝟘) _⊎_

module _ {ℓ a} {A : ★ a} where
    module _ (eᴬ : Explore (ₛ ℓ) A) where
        Lookup : ★ (ₛ ℓ ⊔ a)
        Lookup = ∀ {P : A → ★ ℓ} → Πᵉ eᴬ P → Π A P

        -- alternative name suggestion: tabulate
        Reify : ★ (a ⊔ ₛ ℓ)
        Reify = ∀ {P : A → ★ ℓ} → Π A P → Πᵉ eᴬ P

        Unfocus : ★ (a ⊔ ₛ ℓ)
        Unfocus = ∀ {P : A → ★ ℓ} → Σᵉ eᴬ P → Σ A P

        -- alternative name suggestion: inject
        Focus : ★ (a ⊔ ₛ ℓ)
        Focus = ∀ {P : A → ★ ℓ} → Σ A P → Σᵉ eᴬ P

    Adequate-Σ : ((A → ★ ℓ) → ★ _) → ★ _
    Adequate-Σ Σᴬ = ∀ F → Σᴬ F ≡ Σ A F

    Adequate-Π : ((A → ★ ℓ) → ★ _) → ★ _
    Adequate-Π Πᴬ = ∀ F → Πᴬ F ≡ Π A F

-- This module could be parameterised by the relation on types, here _≡_
module Universal-Adequacy {ℓu ℓe ℓr ℓa}
                          (U : ★_ ℓu)(El : U → ★_ ℓe)
                          (_≈_ : ★_ ℓe → ★_ (ℓa ⊔ ℓe) → ★_ ℓr){A : ★_ ℓa} where
    Adequate-univ-sum : ((A → U) → U) → ★_ (ℓa ⊔ (ℓr ⊔ ℓu))
    Adequate-univ-sum sumᴬ = ∀ f → El (sumᴬ f) ≈ Σ A (El ∘ f)

    Adequate-univ-product : ((A → U) → U) → ★_ (ℓa ⊔ (ℓr ⊔ ℓu))
    Adequate-univ-product productᴬ = ∀ f → El (productᴬ f) ≈ Π A (El ∘ f)

module Adequacy {ℓa ℓr}(_≈_ : ★₀ → ★_ ℓa → ★_ ℓr){A : ★_ ℓa} where

    -- Universal-Adequacy.Adequate-univ-sum ℕ Fin _≡_
    Adequate-sum : Sum A → ★_(ℓa ⊔ ℓr)
    Adequate-sum sumᴬ = ∀ f → Fin (sumᴬ f) ≈ Σ A (Fin ∘ f)

    -- Universal-Adequacy.Adequate-univ-product ℕ Fin _≡_
    Adequate-product : Product A → ★_(ℓa ⊔ ℓr)
    Adequate-product productᴬ = ∀ f → Fin (productᴬ f) ≈ Π A (Fin ∘ f)

    -- Universal-Adequacy.Adequate-univ-product 𝟚 ✓ _≡_
    Adequate-any : (any : BigOp 𝟚 A) → ★_(ℓa ⊔ ℓr)
    Adequate-any anyᴬ = ∀ f → ✓ (anyᴬ f) ≈ Σ A (✓ ∘ f)

    -- Universal-Adequacy.Adequate-univ-product 𝟚 ✓ _≡_
    Adequate-all : (all : BigOp 𝟚 A) → ★_(ℓa ⊔ ℓr)
    Adequate-all allᴬ = ∀ f → ✓ (allᴬ f) ≈ Π A (✓ ∘ f)

module _ {m a}{M : ★ m}{A : ★ a}([⊕] : BigOp M A) where
    BigOpStableUnder : (p : A → A) → ★ _
    BigOpStableUnder p = ∀ f → [⊕] f ≡ [⊕] (f ∘ p)

    -- Extensionality of a big-operator
    BigOp= : ★ _
    BigOp= = {f g : A → M} → f ≗ g → [⊕] f ≡ [⊕] g

module _ {ℓ a} {A : ★ a} (eᴬ : Explore ℓ A) where
    StableUnder : (A → A) → ★ _
    StableUnder p = ∀ {M}(ε : M) op → BigOpStableUnder (eᴬ ε op) p

    -- Extensionality of an exploration function
    Explore= : ★ _
    Explore= = ∀ {M}(ε : M) op → BigOp= (eᴬ ε op)
    ExploreExt = Explore=

module _ {ℓ a} {A : ★ a} r (eᴬ : Explore ℓ A) where
    ExploreMono : ★ _
    ExploreMono = ∀ {C} (_⊆_ : C → C → ★ r)
                    {z₀ z₁} (z₀⊆z₁ : z₀ ⊆ z₁)
                    {_∙_} (∙-mono : _∙_ Preserves₂ _⊆_ ⟶ _⊆_ ⟶ _⊆_)
                    {f g} →
                    (∀ x → f x ⊆ g x) → eᴬ z₀ _∙_ f ⊆ eᴬ z₁ _∙_ g

    ExploreMonExt : ★ _
    ExploreMonExt =
      ∀ (m : Monoid ℓ r) {f g}
      → let open Mon m
            bigop = eᴬ ε _∙_
        in
        f ≈° g → bigop f ≈ bigop g

    Exploreε : ★ _
    Exploreε = ∀ (m : Monoid ℓ r) →
                 let open Mon m in
                 eᴬ ε _∙_ (const ε) ≈ ε

    ExploreLinˡ : ★ _
    ExploreLinˡ =
      ∀ m _◎_ f k →
        let open Mon {ℓ} {r} m
            open FP _≈_ in
        k ◎ ε ≈ ε →
        _◎_ DistributesOverˡ _∙_ →
        eᴬ ε _∙_ (λ x → k ◎ f x) ≈ k ◎ eᴬ ε _∙_ f

    ExploreLinʳ : ★ _
    ExploreLinʳ =
      ∀ m _◎_ f k →
        let open Mon {ℓ} {r} m
            open FP _≈_ in
        ε ◎ k ≈ ε →
        _◎_ DistributesOverʳ _∙_ →
        eᴬ ε _∙_ (λ x → f x ◎ k) ≈ eᴬ ε _∙_ f ◎ k

    ExploreHom : ★ _
    ExploreHom =
      ∀ cm f g →
        let open CMon {ℓ} {r} cm in
        eᴬ ε _∙_ (f ∙° g) ≈ eᴬ ε _∙_ f ∙ eᴬ ε _∙_ g

        {-
    ExploreSwap'' : ∀ {b} → ★ _
    ExploreSwap'' {b}
                = ∀ (monM : Monoid _) (monN : Monoid _) →
                    let module M = Mon {_} {r} monM in
                    let module N = Mon {_} {r} monN in
                  ∀ {h : M.C → N.C}
                    (h-ε : h M.ε ≈ N.ε)
                    (h-∙ : ∀ x y → h (x M.∙ y) ≈ h x N.∙ h y)
                    f
                  → eᴬ ε _∙_ (h ∘ f) ≈ h (eᴬ ε _∙_ f)
-}

-- derived from lift-hom with the source monoid being (a → m)
    ExploreSwap : ∀ {b} → ★ _
    ExploreSwap {b}
                = ∀ {B : ★ b} mon →
                    let open Mon {_} {r} mon in
                  ∀ {opᴮ : (B → C) → C}
                    (opᴮ-ε : opᴮ (const ε) ≈ ε)
                    (hom : ∀ f g → opᴮ (f ∙° g) ≈ opᴮ f ∙ opᴮ g)
                    f
                  → eᴬ ε _∙_ (opᴮ ∘ f) ≈ opᴮ (eᴬ ε _∙_ ∘ flip f)

module _ {a} {A : ★ a} (sumᴬ : Sum A) where
    SumStableUnder : (A → A) → ★ _
    SumStableUnder p = ∀ f → sumᴬ f ≡ sumᴬ (f ∘ p)

    SumStableUnderInjection : ★ _
    SumStableUnderInjection = ∀ p → Injective p → SumStableUnder p

    SumInd : ★(₁ ⊔ a)
    SumInd = ∀ (P  : Sum A → ★₀)
               (P0 : P (λ f → 0))
               (P+ : ∀ {s₀ s₁ : Sum A} → P s₀ → P s₁ → P (λ f → s₀ f + s₁ f))
               (Pf : ∀ x → P (λ f → f x))
             → P sumᴬ

    SumExt : ★ _
    SumExt = ∀ {f g} → f ≗ g → sumᴬ f ≡ sumᴬ g

    SumZero : ★ _
    SumZero = sumᴬ (λ _ → 0) ≡ 0

    SumLin : ★ _
    SumLin = ∀ f k → sumᴬ (λ x → k * f x) ≡ k * sumᴬ f

    SumHom : ★ _
    SumHom = ∀ f g → sumᴬ (λ x → f x + g x) ≡ sumᴬ f + sumᴬ g

    SumMono : ★ _
    SumMono = ∀ {f g} → (∀ x → f x ≤ g x) → sumᴬ f ≤ sumᴬ g

    SumConst : ★ _
    SumConst = ∀ x → sumᴬ (const x) ≡ sumᴬ (const 1) * x

    SumSwap : ★ _
    SumSwap = ∀ {B : ★₀}
                {sumᴮ : Sum B}
                (sumᴮ-0 : sumᴮ (const 0) ≡ 0)
                (hom : ∀ f g → sumᴮ (f +° g) ≡ sumᴮ f + sumᴮ g)
                f
              → sumᴬ (sumᴮ ∘ f) ≡ sumᴮ (sumᴬ ∘ flip f)

module _ {a} {A : ★ a} (countᴬ : Count A) where
    CountStableUnder : (A → A) → ★ _
    CountStableUnder p = ∀ f → countᴬ f ≡ countᴬ (f ∘ p)

    CountExt : ★ _
    CountExt = ∀ {f g} → f ≗ g → countᴬ f ≡ countᴬ g

    Unique : Cmp A → ★ _
    Unique cmp = ∀ x → countᴬ (cmp x) ≡ 1
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module Tactic.Reflection.Telescope where

open import Prelude hiding (abs)
open import Builtin.Reflection
open import Tactic.Reflection.DeBruijn

Telescope = List (Arg Type)

telView : Type → Telescope × Type
telView (pi a (abs _ b)) = first (_∷_ a) (telView b)
telView a                = [] , a

visibleArity : Type → Nat
visibleArity = length ∘ filter isVisible ∘ fst ∘ telView

telPi : Telescope → Type → Type
telPi tel b = foldr (λ a b → pi a (abs "_" b)) b tel

arity : Name → TC Nat
arity f = length ∘ fst ∘ telView <$> getType f

argTel : Name → TC Telescope
argTel f = fst ∘ telView <$> getType f

telePat : Telescope → List (Arg Pattern)
telePat = map (var "_" <$_)

private
  teleArgs′ : Nat → List (Arg Type) → List (Arg Term)
  teleArgs′ (suc n) (a ∷ Γ) = (var n [] <$ a) ∷ teleArgs′ n Γ
  teleArgs′ _ _ = []

teleArgs : Telescope → List (Arg Term)
teleArgs Γ = teleArgs′ (length Γ) Γ

conParams : Name → TC Nat
conParams c =
  caseM getDefinition c of λ
  { (data-cons d) → getParameters d
  ; _             → pure 0 }

conPat : Name → TC Pattern
conPat c = do
  np ← conParams c
  con c ∘ telePat ∘ drop np <$> argTel c

conTerm : Name → TC Term
conTerm c = do
  np ← conParams c
  con c ∘ teleArgs ∘ drop np <$> argTel c

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module Common.Char where

postulate
  Char : Set

{-# BUILTIN CHAR Char #-}

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
------------------------------------------------------------------------
-- Extra lemmas about substitutions
------------------------------------------------------------------------

module Data.Fin.Substitution.ExtraLemmas where

open import Data.Fin as Fin using (Fin; zero; suc)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Star using (Star; ε; _◅_; _▻_)
open import Data.Vec using (Vec; _∷_; lookup; map)
open import Data.Vec.All hiding (lookup; map)
open import Data.Vec.Properties using (lookup-map; map-cong; map-∘)
open import Function using (_∘_; _$_; flip)
open import Relation.Binary.PropositionalEquality as PropEq hiding (subst)
open PropEq.≡-Reasoning

-- Simple extension of substitutions.
--
-- FIXME: this should go into Data.Fin.Substitution.
record Extension (T : ℕ → Set) : Set where
  infixr 5 _/∷_

  field weaken : ∀ {n} → T n → T (suc n)  -- Weakens Ts.

  -- Extension.
  _/∷_ : ∀ {m n} → T (suc n) → Sub T m n → Sub T (suc m) (suc n)
  t /∷ ρ = t ∷ map weaken ρ

-- Helper module
module SimpleExt {T} (simple : Simple T) where
  open Simple simple public

  extension : Extension T
  extension = record { weaken = weaken }
  open Extension extension public hiding (weaken)

-- An generalized version of Data.Fin.Lemmas.Lemmas₀
--
-- FIXME: this should go into Data.Fin.Substitution.Lemmas.
module ExtLemmas₀ {T} (lemmas₀ : Lemmas₀ T) where

  open Lemmas₀   lemmas₀ public hiding (lookup-map-weaken-↑⋆)
  open SimpleExt simple

  -- A generalized variant of Lemmas₀.lookup-map-weaken-↑⋆.
  lookup-map-weaken-↑⋆ : ∀ {m n} k x {ρ : Sub T m n} {t} →
                         lookup x (map weaken ρ ↑⋆ k) ≡
                         lookup (Fin.lift k suc x) ((t /∷ ρ) ↑⋆ k)
  lookup-map-weaken-↑⋆ zero    x               = refl
  lookup-map-weaken-↑⋆ (suc k) zero            = refl
  lookup-map-weaken-↑⋆ (suc k) (suc x) {ρ} {t} = begin
      lookup x (map weaken (map weaken ρ ↑⋆ k))
    ≡⟨ lookup-map x weaken _ ⟩
      weaken (lookup x (map weaken ρ ↑⋆ k))
    ≡⟨ cong weaken (lookup-map-weaken-↑⋆ k x) ⟩
      weaken (lookup (Fin.lift k suc x) ((t /∷ ρ) ↑⋆ k))
    ≡⟨ sym (lookup-map (Fin.lift k suc x) weaken _) ⟩
      lookup (Fin.lift k suc x) (map weaken ((t /∷ ρ) ↑⋆ k))
    ∎

-- A generalized version of Data.Fin.Lemmas.Lemmas₄
--
-- FIXME: this should go into Data.Fin.Substitution.Lemmas.
module ExtLemmas₄ {T} (lemmas₄ : Lemmas₄ T) where

  open Lemmas₄    lemmas₄ public hiding (⊙-wk; wk-commutes)
  open Lemmas₃    lemmas₃        using (lookup-wk-↑⋆-⊙; /✶-↑✶′)
  open SimpleExt  simple         using (_/∷_)
  open ExtLemmas₀ lemmas₀        using (lookup-map-weaken-↑⋆)

  private

    ⊙-wk′ : ∀ {m n} {ρ : Sub T m n} {t} k →
            ρ ↑⋆ k ⊙ wk ↑⋆ k ≡ wk ↑⋆ k ⊙ (t /∷ ρ) ↑⋆ k
    ⊙-wk′ {ρ = ρ} {t} k = sym (begin
      wk ↑⋆ k ⊙ (t /∷ ρ) ↑⋆ k   ≡⟨ lemma ⟩
      map weaken ρ ↑⋆ k         ≡⟨ cong (λ ρ′ → ρ′ ↑⋆ k) map-weaken ⟩
      (ρ ⊙ wk) ↑⋆ k             ≡⟨ ↑⋆-distrib k ⟩
      ρ ↑⋆ k ⊙ wk ↑⋆ k          ∎)
      where
      lemma = extensionality λ x → begin
          lookup x (wk ↑⋆ k ⊙ (t /∷ ρ) ↑⋆ k)
        ≡⟨ lookup-wk-↑⋆-⊙ k ⟩
          lookup (Fin.lift k suc x) ((t /∷ ρ) ↑⋆ k)
        ≡⟨ sym (lookup-map-weaken-↑⋆ k x) ⟩
          lookup x (map weaken ρ ↑⋆ k)
        ∎

  ⊙-wk : ∀ {m n} {ρ : Sub T m n} {t} → ρ ⊙ wk ≡ wk ⊙ (t /∷ ρ)
  ⊙-wk = ⊙-wk′ zero

  wk-commutes : ∀ {m n} {ρ : Sub T m n} {t′} t →
                t / ρ / wk ≡ t / wk / (t′ /∷ ρ)
  wk-commutes {ρ = ρ} {t} = /✶-↑✶′ (ε ▻ ρ ▻ wk) (ε ▻ wk ▻ (t /∷ ρ)) ⊙-wk′ zero

  -- A handy helper lemma: weakening commutes with substitution.
  weaken-/ : ∀ {m n} {ρ : Sub T m n} {t′} t →
             weaken (t / ρ) ≡ weaken t / (t′ /∷ ρ)
  weaken-/ {ρ = ρ} {t′} t = begin
    weaken (t / ρ)         ≡⟨ sym /-wk ⟩
    t / ρ / wk             ≡⟨ wk-commutes t ⟩
    t / wk / (t′ /∷ ρ)     ≡⟨ cong₂ _/_ /-wk refl ⟩
    weaken t / (t′ /∷ ρ)   ∎

-- A generalize version of Data.Fin.Lemmas.AppLemmas
--
-- FIXME: this should go into Data.Fin.Substitution.Lemmas.
module ExtAppLemmas {T₁ T₂} (appLemmas : AppLemmas T₁ T₂) where

  open AppLemmas appLemmas public hiding (wk-commutes)
  open SimpleExt simple           using (_/∷_)
  private module L₄ = ExtLemmas₄ lemmas₄

  wk-commutes : ∀ {m n} {ρ : Sub T₂ m n} {t′} t →
                t / ρ / wk ≡ t / wk / (t′ /∷ ρ)
  wk-commutes {ρ = ρ} {t} = ⨀→/✶ (ε ▻ ρ ▻ wk) (ε ▻ wk ▻ (t /∷ ρ)) L₄.⊙-wk

-- Lemmas relating T₃ substitutions in T₁ and T₂.
record LiftAppLemmas (T₁ T₂ T₃ : ℕ → Set) : Set where
  field
    lift          : ∀ {n} → T₃ n → T₂ n
    application₁₃ : Application T₁ T₃
    application₂₃ : Application T₂ T₃
    lemmas₂       : Lemmas₄     T₂
    lemmas₃       : Lemmas₄     T₃

  private
    module L₂ = ExtLemmas₄  lemmas₂
    module L₃ = ExtLemmas₄  lemmas₃
    module A₁ = Application application₁₃
    module A₂ = Application application₂₃

  field
    -- Lifting commutes with application of T₃ substitutions.
    lift-/ : ∀ {m n} t {σ : Sub T₃ m n} → lift (t L₃./ σ) ≡ lift t A₂./ σ

    -- Lifting preserves variables.
    lift-var : ∀ {n} (x : Fin n) → lift (L₃.var x) ≡ L₂.var x

    -- Sequences of T₃ substitutions are equivalent when applied to
    -- T₁s if they are equivalent when applied to T₂ variables.
    /✶-↑✶ :
      ∀ {m n} (σs₁ σs₂ : Subs T₃ m n) →
      (∀ k x → L₂.var x A₂./✶ σs₁ L₃.↑✶ k ≡ L₂.var x A₂./✶ σs₂ L₃.↑✶ k) →
       ∀ k t → t        A₁./✶ σs₁ L₃.↑✶ k ≡ t      A₁./✶ σs₂ L₃.↑✶ k

  lift-lookup-⊙ : ∀ {m n k} x {σ₁ : Sub T₃ m n} {σ₂ : Sub T₃ n k} →
                  lift (lookup x (σ₁ L₃.⊙ σ₂)) ≡ lift (lookup x σ₁) A₂./ σ₂
  lift-lookup-⊙ x {σ₁} {σ₂} = begin
    lift (lookup x (σ₁ L₃.⊙ σ₂))   ≡⟨ cong lift (L₃.lookup-⊙ x) ⟩
    lift (lookup x σ₁ L₃./ σ₂)     ≡⟨ lift-/ _ ⟩
    lift (lookup x σ₁) A₂./ σ₂     ∎

  lift-lookup-⨀ : ∀ {m n} x (σs : Subs T₃ m n) →
                  lift (lookup x (L₃.⨀ σs)) ≡ L₂.var x A₂./✶ σs
  lift-lookup-⨀ x ε = begin
    lift (lookup x L₃.id)    ≡⟨ cong lift (L₃.lookup-id x) ⟩
    lift (L₃.var x)          ≡⟨ lift-var x ⟩
    L₂.var x                 ∎
  lift-lookup-⨀ x (σ ◅ ε) = begin
    lift (lookup x σ)        ≡⟨ cong lift (sym L₃.var-/) ⟩
    lift (L₃.var x L₃./ σ)   ≡⟨ lift-/ _ ⟩
    lift (L₃.var x) A₂./ σ   ≡⟨ cong₂ A₂._/_ (lift-var x) refl ⟩
    L₂.var x A₂./ σ          ∎
  lift-lookup-⨀ x (σ ◅ (σ′ ◅ σs′)) = begin
      lift (lookup x (L₃.⨀ σs L₃.⊙ σ))
    ≡⟨ lift-lookup-⊙ x ⟩
      lift (lookup x (L₃.⨀ σs)) A₂./ σ
    ≡⟨ cong₂ A₂._/_ (lift-lookup-⨀ x (σ′ ◅ σs′)) refl ⟩
      L₂.var x A₂./✶ σs A₂./ σ
    ∎
    where σs = σ′ ◅ σs′

  -- Sequences of T₃ substitutions are equivalent when applied to
  -- T₁s if they are equivalent when applied as composites.
  /✶-↑✶′ : ∀ {m n} (σs₁ σs₂ : Subs T₃ m n) →
           (∀ k → L₃.⨀ (σs₁ L₃.↑✶ k) ≡ L₃.⨀ (σs₂ L₃.↑✶ k)) →
            ∀ k t → t A₁./✶ σs₁ L₃.↑✶ k ≡ t A₁./✶ σs₂ L₃.↑✶ k
  /✶-↑✶′ σs₁ σs₂ hyp = /✶-↑✶ σs₁ σs₂ (λ k x → begin
      L₂.var x A₂./✶ σs₁ L₃.↑✶ k
    ≡⟨ sym (lift-lookup-⨀ x (σs₁ L₃.↑✶ k)) ⟩
      lift (lookup x (L₃.⨀ (σs₁ L₃.↑✶ k)))
    ≡⟨ cong (lift ∘ lookup x) (hyp k) ⟩
      lift (lookup x (L₃.⨀ (σs₂ L₃.↑✶ k)))
    ≡⟨ lift-lookup-⨀ x (σs₂ L₃.↑✶ k) ⟩
      L₂.var x A₂./✶ σs₂ L₃.↑✶ k
    ∎)

  -- Derived lemmas about applications of T₃ substitutions to T₁s.
  appLemmas : AppLemmas T₁ T₃
  appLemmas = record
    { application = application₁₃
    ; lemmas₄     = lemmas₃
    ; id-vanishes = /✶-↑✶′ (ε ▻ L₃.id) ε L₃.id-↑⋆ 0
    ; /-⊙         = /✶-↑✶′ (ε ▻ _ L₃.⊙ _) (ε ▻ _ ▻ _) L₃.↑⋆-distrib 0
    }
  open ExtAppLemmas appLemmas public
    hiding (application; lemmas₂; lemmas₃; var; weaken; subst; simple)

-- Lemmas relating T₂ and T₃ substitutions in T₁.
record LiftSubLemmas (T₁ T₂ T₃ : ℕ → Set) : Set where
  field
    application₁₂ : Application   T₁ T₂
    liftAppLemmas : LiftAppLemmas T₁ T₂ T₃

  open LiftAppLemmas liftAppLemmas hiding (/✶-↑✶; /-wk)
  private
    module L₃  = ExtLemmas₄  lemmas₃
    module L₂  = ExtLemmas₄  lemmas₂
    module A₁₂ = Application application₁₂
    module A₁₃ = Application (AppLemmas.application appLemmas)
    module A₂₃ = Application application₂₃

  field
    -- Weakening commutes with lifting.
    weaken-lift : ∀ {n} (t : T₃ n) → L₂.weaken (lift t) ≡ lift (L₃.weaken t)

    -- Applying a composition of T₂ substitutions to T₁s
    -- corresponds to two consecutive applications.
    /-⊙₂ : ∀ {m n k} {σ₁ : Sub T₂ m n} {σ₂ : Sub T₂ n k} t →
           t A₁₂./ σ₁ L₂.⊙ σ₂ ≡ t A₁₂./ σ₁ A₁₂./ σ₂

    -- Sequences of T₃ substitutions are equivalent to T₂
    -- substitutions when applied to T₁s if they are equivalent when
    -- applied to variables.
    /✶-↑✶₁ :
      ∀ {m n} (σs₁ : Subs T₃ m n) (σs₂ : Subs T₂ m n) →
      (∀ k x → L₂.var x A₂₃./✶ σs₁ ↑✶ k ≡ L₂.var x L₂./✶  σs₂ L₂.↑✶ k) →
       ∀ k t → t        A₁₃./✶ σs₁ ↑✶ k ≡ t        A₁₂./✶ σs₂ L₂.↑✶ k

    -- Sequences of T₃ substitutions are equivalent to T₂
    -- substitutions when applied to T₂s if they are equivalent when
    -- applied to variables.
    /✶-↑✶₂ :
      ∀ {m n} (σs₁ : Subs T₃ m n) (σs₂ : Subs T₂ m n) →
      (∀ k x → L₂.var x A₂₃./✶ σs₁ ↑✶ k ≡ L₂.var x L₂./✶ σs₂ L₂.↑✶ k) →
       ∀ k t → t        A₂₃./✶ σs₁ ↑✶ k ≡ t        L₂./✶ σs₂ L₂.↑✶ k

  -- Lifting of T₃ substitutions to T₂ substitutions.
  liftSub : ∀ {m n} → Sub T₃ m n → Sub T₂ m n
  liftSub σ = map lift σ

  -- The two types of lifting commute.
  liftSub-↑⋆ : ∀ {m n} (σ : Sub T₃ m n) k →
               liftSub σ L₂.↑⋆ k ≡ liftSub (σ ↑⋆ k)
  liftSub-↑⋆ σ zero    = refl
  liftSub-↑⋆ σ (suc k) = cong₂ _∷_ (sym (lift-var _)) (begin
    map L₂.weaken (liftSub σ L₂.↑⋆ k)   ≡⟨ cong (map _) (liftSub-↑⋆ σ k) ⟩
    map L₂.weaken (map lift (σ ↑⋆ k))   ≡⟨ sym (map-∘ _ _ _) ⟩
    map (L₂.weaken ∘ lift) (σ ↑⋆ k)     ≡⟨ map-cong weaken-lift _ ⟩
    map (lift ∘ L₃.weaken)  (σ ↑⋆ k)    ≡⟨ map-∘ _ _ _ ⟩
    map lift (map L₃.weaken (σ ↑⋆ k))   ∎)

  -- The identity substitutions are equivalent up to lifting.
  liftSub-id : ∀ {n} → liftSub (L₃.id {n}) ≡ L₂.id {n}
  liftSub-id {zero}  = refl
  liftSub-id {suc n} = begin
    liftSub (L₃.id L₃.↑)  ≡⟨ sym (liftSub-↑⋆ L₃.id 1) ⟩
    liftSub L₃.id L₂.↑    ≡⟨ cong L₂._↑ liftSub-id ⟩
    L₂.id ∎

  -- Weakening is equivalent up to lifting.
  liftSub-wk⋆ : ∀ k {n} → liftSub (L₃.wk⋆ k {n}) ≡ L₂.wk⋆ k {n}
  liftSub-wk⋆ zero    = liftSub-id
  liftSub-wk⋆ (suc k) = begin
    liftSub (map L₃.weaken (L₃.wk⋆ k))   ≡⟨ sym (map-∘ _ _ _) ⟩
    map (lift ∘ L₃.weaken) (L₃.wk⋆ k)    ≡⟨ sym (map-cong weaken-lift _) ⟩
    map (L₂.weaken ∘ lift) (L₃.wk⋆ k)    ≡⟨ map-∘ _ _ _ ⟩
    map L₂.weaken (liftSub (L₃.wk⋆ k))   ≡⟨ cong (map _) (liftSub-wk⋆ k) ⟩
    map L₂.weaken (L₂.wk⋆ k)             ∎

  -- Weakening is equivalent up to lifting.
  liftSub-wk : ∀ {n} → liftSub (L₃.wk {n}) ≡ L₂.wk {n}
  liftSub-wk = liftSub-wk⋆ 1

  -- Single variable substitution is equivalent up to lifting.
  liftSub-sub : ∀ {n} (t : T₃ n) → liftSub (L₃.sub t) ≡ L₂.sub (lift t)
  liftSub-sub t = cong₂ _∷_ refl liftSub-id

  -- Lifting commutes with application to variables.
  var-/-liftSub-↑⋆ : ∀ {m n} (σ : Sub T₃ m n) k x →
                     L₂.var x A₂₃./ σ ↑⋆ k ≡ L₂.var x L₂./ liftSub σ L₂.↑⋆ k
  var-/-liftSub-↑⋆ σ k x = begin
      L₂.var x A₂₃./ σ ↑⋆ k
    ≡⟨ cong₂ A₂₃._/_ (sym (lift-var x)) refl ⟩
      lift (L₃.var x) A₂₃./ σ ↑⋆ k
    ≡⟨ sym (lift-/ _) ⟩
      lift (L₃.var x L₃./ σ ↑⋆ k)
    ≡⟨ cong lift L₃.var-/ ⟩
      lift (lookup x (σ ↑⋆ k))
    ≡⟨ sym (lookup-map x _ _) ⟩
      lookup x (liftSub (σ ↑⋆ k))
    ≡⟨ sym L₂.var-/ ⟩
      L₂.var x L₂./ liftSub (σ ↑⋆ k)
    ≡⟨ cong (L₂._/_ (L₂.var x)) (sym (liftSub-↑⋆ σ k)) ⟩
      L₂.var x L₂./ liftSub σ L₂.↑⋆ k
    ∎

  -- Lifting commutes with application.
  /-liftSub : ∀ {m n} t {σ : Sub T₃ m n} →
              t A₁₃./ σ ≡ t A₁₂./ liftSub σ
  /-liftSub t {σ} = /✶-↑✶₁ (ε ▻ σ) (ε ▻ liftSub σ)
                           (var-/-liftSub-↑⋆ σ) zero t

  -- Weakening is equivalent up to choice of application.
  /-wk : ∀ {n} {t : T₁ n} → t A₁₃./ L₃.wk ≡ t A₁₂./ L₂.wk
  /-wk {t = t} = begin
    t A₁₃./ L₃.wk           ≡⟨ /-liftSub t ⟩
    t A₁₂./ liftSub L₃.wk   ≡⟨ cong₂ A₁₂._/_ refl liftSub-wk ⟩
    t A₁₂./ L₂.wk           ∎

  -- Single-variable substitution is equivalent up to choice of
  -- application.
  /-sub : ∀ {n} t (s : T₃ n) →
          t A₁₃./ L₃.sub s ≡ t A₁₂./ L₂.sub (lift s)
  /-sub t s = begin
    t A₁₃./ L₃.sub s             ≡⟨ /-liftSub t ⟩
    t A₁₂./ liftSub (L₃.sub s)   ≡⟨ cong₂ A₁₂._/_ refl (liftSub-sub s) ⟩
    t A₁₂./ L₂.sub (lift s)      ∎

  -- Lifting commutes with application.
  /-sub-↑ : ∀ {m n} t s (σ : Sub T₃ m n) →
            t A₁₂./ L₂.sub s A₁₃./ σ ≡ (t A₁₃./ σ ↑) A₁₂./ L₂.sub (s A₂₃./ σ)
  /-sub-↑ t s σ = begin
      t A₁₂./ L₂.sub s A₁₃./ σ
    ≡⟨ /-liftSub _ ⟩
      t A₁₂./ L₂.sub s A₁₂./ liftSub σ
    ≡⟨ sym (/-⊙₂ t) ⟩
      t A₁₂./ (L₂.sub s L₂.⊙ liftSub σ)
    ≡⟨ cong₂ A₁₂._/_ refl (L₂.sub-⊙ s) ⟩
      t A₁₂./ (liftSub σ L₂.↑ L₂.⊙ L₂.sub (s L₂./ liftSub σ))
    ≡⟨ /-⊙₂ t ⟩
      t A₁₂./ liftSub σ L₂.↑ A₁₂./ L₂.sub (s L₂./ liftSub σ)
    ≡⟨ cong₂ (A₁₂._/_ ∘ A₁₂._/_ t) (liftSub-↑⋆ _ 1)
             (cong L₂.sub (sym (/-liftSub₂ s))) ⟩
      t A₁₂./ liftSub (σ ↑) A₁₂./ L₂.sub (s A₂₃./ σ)
    ≡⟨ cong₂ A₁₂._/_ (sym (/-liftSub t)) refl ⟩
      t A₁₃./ σ ↑ A₁₂./ L₂.sub (s A₂₃./ σ)
    ∎
    where
      /-liftSub₂ : ∀ {m n} s {σ : Sub T₃ m n} →
                   s A₂₃./ σ ≡ s L₂./ liftSub σ
      /-liftSub₂ s {σ} = /✶-↑✶₂ (ε ▻ σ) (ε ▻ liftSub σ)
                                (var-/-liftSub-↑⋆ σ) zero s

-- Lemmas for a term-like T₁ derived from term lemmas for T₂
record TermLikeLemmas (T₁ T₂ : ℕ → Set) : Set₁ where
  field
    app         : ∀ {T₃} → Lift T₃ T₂ → ∀ {m n} → T₁ m → Sub T₃ m n → T₁ n
    termLemmas  : TermLemmas T₂

  open TermLemmas termLemmas  using (termSubst)
  open TermSubst  termSubst   using (var; termLift; varLift; module Lifted)

  field /✶-↑✶₁ : ∀ {T₃} {lift : Lift T₃ T₂} →
                 let open Application (record { _/_ = app lift })
                       using ()     renaming (_/✶_ to _/✶₁_)
                     open Lifted lift
                       using (_↑✶_) renaming (_/✶_ to _/✶₂_)
                 in
                 ∀ {m n} (σs₁ : Subs T₃ m n) (σs₂ : Subs T₃ m n) →
                 (∀ k x → var x /✶₂ σs₁ ↑✶ k ≡ var x /✶₂ σs₂ ↑✶ k) →
                  ∀ k t → t     /✶₁ σs₁ ↑✶ k ≡ t     /✶₁ σs₂ ↑✶ k

  termApplication : Application T₁ T₂
  termApplication = record { _/_ = app termLift }

  varApplication : Application T₁ Fin
  varApplication = record { _/_ = app varLift }

  field /✶-↑✶₂ : let open Application varApplication
                       using () renaming (_/✶_ to _/✶₁₃_)
                     open Application termApplication
                       using () renaming (_/✶_ to _/✶₁₂_)
                     open Lifted varLift
                       using () renaming (_↑✶_ to _↑✶₃_; _/✶_ to _/✶₂₃_)
                     open TermSubst termSubst
                       using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂₂_)
                 in
                 ∀ {m n} (σs₁ : Subs Fin m n) (σs₂ : Subs T₂ m n) →
                 (∀ k x → var x /✶₂₃ σs₁ ↑✶₃ k ≡ var x /✶₂₂ σs₂ ↑✶₂ k) →
                  ∀ k t → t     /✶₁₃ σs₁ ↑✶₃ k ≡ t     /✶₁₂ σs₂ ↑✶₂ k

  -- An instantiation of the above lemmas for T₂ substitutions in T₁s.
  termLiftAppLemmas : LiftAppLemmas T₁ T₂ T₂
  termLiftAppLemmas = record
    { lift          = Lift.lift termLift
    ; application₁₃ = termApplication
    ; application₂₃ = TermLemmas.application termLemmas
    ; lemmas₂       = TermLemmas.lemmas₄ termLemmas
    ; lemmas₃       = TermLemmas.lemmas₄ termLemmas
    ; lift-/        = λ _ → refl
    ; lift-var      = λ _ → refl
    ; /✶-↑✶         = /✶-↑✶₁
    }

  open LiftAppLemmas termLiftAppLemmas public hiding (/-wk)

  -- An instantiation of the above lemmas for variable substitutions
  -- (renamings) in T₁s.
  varLiftSubLemmas : LiftSubLemmas T₁ T₂ Fin
  varLiftSubLemmas = record
    { application₁₂ = termApplication
    ; liftAppLemmas = record
      { lift          = Lift.lift varLift
      ; application₁₃ = varApplication
      ; application₂₃ = Lifted.application varLift
      ; lemmas₂       = TermLemmas.lemmas₄ termLemmas
      ; lemmas₃       = VarLemmas.lemmas₄
      ; lift-/        = λ _ → sym (TermLemmas.app-var termLemmas)
      ; lift-var      = λ _ → refl
      ; /✶-↑✶         = /✶-↑✶₁
      }
    ; weaken-lift = λ _ → TermLemmas.weaken-var termLemmas
    ; /-⊙₂        = AppLemmas./-⊙ appLemmas
    ; /✶-↑✶₁      = /✶-↑✶₂
    ; /✶-↑✶₂      = TermLemmas./✶-↑✶ termLemmas
    }

  open Application   varApplication   public using () renaming (_/_ to _/Var_)
  open LiftSubLemmas varLiftSubLemmas public hiding (/✶-↑✶₁; /✶-↑✶₂)
    renaming (liftAppLemmas to varLiftAppLemmas)

  -- Weakening of T₁s.
  weaken : ∀ {n} → T₁ n → T₁ (suc n)
  weaken t = t /Var VarSubst.wk

  -- A version of wk-sub-vanishes for T₁s.
  weaken-sub : ∀ {n t′} → (t : T₁ n) → weaken t / sub t′ ≡ t
  weaken-sub t = begin
    weaken t / sub _   ≡⟨ cong₂ _/_ /-wk refl ⟩
    t / wk / sub _     ≡⟨ wk-sub-vanishes t ⟩
    t                  ∎

max_stars_repo_name: asr/pts-agda

max_issues_repo_name: asr/pts-agda

max_forks_repo_name: asr/pts-agda