text:
------------------------------------------------------------------------
-- A definability result: A "closed value" is the semantics of a
-- closed term if and only if it satisfies all "Kripke predicates"
------------------------------------------------------------------------

-- This module is based on parts of Frederik Ramcke's (at the time of
-- writing forthcoming) MSc thesis, "On Definability and Normalization
-- by Evaluation in the Logical Framework". I have not followed
-- Ramcke's development to the letter, but I have taken inspiration
-- from it. Ramcke seems to in turn have taken inspiration from Jung
-- and Tiuryn's "A New Characterization of Lambda Definability".

import Axiom.Extensionality.Propositional as E
open import Level using (Level)
open import Data.Universe

-- The code makes use of the assumption that propositional equality is
-- extensional for functions.

module README.DependentlyTyped.Definability
  (Uni₀ : Universe Level.zero Level.zero)
  (ext : E.Extensionality Level.zero Level.zero)
  where

open import Data.Product as Prod renaming (curry to c)
open import Function.Base hiding (_∋_) renaming (const to k)
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
  using (_⇔_; module Equivalence; equivalence)
open import README.DependentlyTyped.NBE Uni₀ ext
open import README.DependentlyTyped.NormalForm Uni₀
open import README.DependentlyTyped.Term Uni₀
open import Relation.Binary.PropositionalEquality as P using (_≡_)

-- Predicates.

Predicate : Set₁
Predicate = ∀ {Γ σ} → Value Γ σ → Set

private
  variable
    Γ Δ : Ctxt
    Γ₊  : Ctxt₊ Γ
    σ τ : Type Γ
    P   : Predicate

-- Kripke predicates.

record Kripke (P : Predicate) : Set where
  field
    -- Single-step weakening.

    weaken₁ :
      {v : Value Γ σ} →
      P v → P (v /̂Val ŵk[ τ ])

    -- For π-types Kripke predicates have to be defined in a certain
    -- way (up to logical equivalence).

    definition-for-π :
      ∀ {σ τ} {f : Value Γ (Type-π σ τ)} →
      P f
        ⇔
      (∀ (Γ₊ : Ctxt₊ Γ) {v : Value (Γ ++₊ Γ₊) (σ /̂ ŵk₊ Γ₊)} →
         P v → P ((f /̂Val ŵk₊ Γ₊) ˢ v))

  -- Weakening.

  weaken :
    {v : Value Γ σ} (Γ₊ : Ctxt₊ Γ) →
    P v → P (v /̂Val ŵk₊ Γ₊)
  weaken ε        = id
  weaken (σ ◅ Γ₊) = weaken Γ₊ ∘ weaken₁

  -- A "fundamental theorem" for Kripke predicates.

  fundamental :
    {ρ̂ : Γ ⇨̂ Δ} →
    (∀ {σ} (x : Γ ∋ σ) → P (x /̂∋ ρ̂)) →
    (t : Γ ⊢ σ) →
    P (⟦ t ⟧ /̂Val ρ̂)
  fundamental hyp (var x)   = hyp x
  fundamental hyp (t₁ · t₂) =
    (Equivalence.to definition-for-π ⟨$⟩ fundamental hyp t₁)
      ε (fundamental hyp t₂)
  fundamental hyp (ƛ t) =
    Equivalence.from definition-for-π ⟨$⟩ λ Δ₊ p →
      fundamental
        (λ { zero    → p
           ; (suc x) → weaken Δ₊ (hyp x)
           })
        t

  -- A special case for closed terms.

  fundamental-closed : {σ : Type ε} → (t : ε ⊢ σ) → P ⟦ t ⟧
  fundamental-closed = fundamental (λ ())

open Kripke

-- A predicate based on V̌alue.

∃-V̌alue : Predicate
∃-V̌alue {Γ = Γ} {σ = σ} v =
  ∃ λ (v̌ : V̌alue Γ σ) → v ≅-Value ⟦̌ v̌ ⟧

-- ∃-V̌alue is a Kripke predicate.

∃-V̌alue-Kripke : Kripke ∃-V̌alue
weaken₁ ∃-V̌alue-Kripke =
  Prod.map ([_⟶_].function w̌eaken _)
           (λ { P.refl → [_⟶_].corresponds w̌eaken _ _ })
definition-for-π ∃-V̌alue-Kripke {Γ = Γ} {σ = σ} {τ = τ} {f = f} =
  equivalence
    (λ { (f , P.refl) Γ₊ (v , P.refl) →
         proj₁ f Γ₊ v , proj₂ f Γ₊ v
       })
    (λ hyp →
       let
         g : V̌alue-π Γ _ _ (IType-π σ τ)
         g = λ Γ₊ v → proj₁ (hyp Γ₊ (v , P.refl))

         lemma : f ≅-Value ⟦̌ _ ∣ g ⟧-π
         lemma =
           [ f ]                                                    ≡⟨⟩
           [ c ((f /̂Val ŵk₊ (_ ◅ ε)) ˢ ⟦ var zero ⟧n) ]             ≡⟨ curry-cong (ˢ-cong (P.refl {x = [ f /̂Val _ ]})
                                                                                (P.sym $ ňeutral-to-normal-identity _ _)) ⟩
           [ c ((f /̂Val ŵk₊ (_ ◅ ε)) ˢ
                ⟦ ňeutral-to-normal _ (var zero) ⟧n) ]              ≡⟨⟩
           [ c ((f /̂Val ŵk₊ (_ ◅ ε)) ˢ ⟦̌ řeflect _ (var zero) ⟧) ]  ≡⟨ curry-cong (proj₂ (hyp _ _)) ⟩
           [ c ⟦̌ g (_ ◅ ε) (řeflect _ (var zero)) ⟧ ]               ≡⟨ P.sym (unfold-⟦̌∣⟧-π _ g) ⟩
           [ ⟦̌ _ ∣ g ⟧-π ]                                          ∎
       in
         ( g
         , (λ Γ₊ v → [ (⟦̌ _ ∣ g ⟧-π /̂Val ŵk₊ Γ₊) ˢ ⟦̌ v ⟧ ]  ≡⟨ ˢ-cong (/̂Val-cong (P.sym lemma) P.refl) P.refl ⟩
                     [ (f /̂Val ŵk₊ Γ₊) ˢ ⟦̌ v ⟧ ]            ≡⟨ proj₂ (hyp _ _) ⟩
                     [ ⟦̌ g Γ₊ v ⟧ ]                         ∎)
         )
       , lemma
    )
  where
  open P.≡-Reasoning

-- The definability result.

definability :
  {σ : Type ε} {v : Value ε σ} →
  (∃ λ (t : ε ⊢ σ) → v ≡ ⟦ t ⟧)
    ⇔
  ({P : Predicate} → Kripke P → P v)
definability = equivalence
  (λ { (t , P.refl) kripke → fundamental-closed kripke t })
  (λ hyp → Prod.map ([_⟶_].function V̌al-subst.trans _)
                    ≅-Value-⇒-≡
                    (hyp ∃-V̌alue-Kripke))

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
module UntypedLambda where

open import Basics
open import Pr
open import Nom
import Syntacticosmos

data Tag : Set where
  lamT : Tag
  appT : Tag

open module ULam = Syntacticosmos TT TT (\_ -> Tag)

LAM : Kind
LAM = Ty _

SigLAM : Kind
SigLAM = Pi _ conk where
  conk : Tag -> Kind
  conk lamT = (LAM |> LAM) |> LAM
  conk appT = LAM |> LAM |> LAM

Lam : Cxt -> Set
Lam G = G [! SigLAM !]- LAM

lam : {G : Cxt}(x : Nom){Gx : [| G Hasn't x |]} ->
      Lam ((G [ x - LAM ]) {Gx}) -> Lam G
lam x {Gx} b = G[ lamT G^ G\\ (bind x {Gx} b) G& Gnil ]

app : {G : Cxt} -> Lam G -> Lam G -> Lam G
app f s = G[ appT G^ f G& s G& Gnil ]

moo : Lam EC
moo = lam Ze (lam (Su Ze) (var Ze))

noo : Lam EC
noo = lam (Su Ze) (lam Ze (var (Su Ze)))

coo : Id moo noo
coo = refl

ext: agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import LogicalFormulae
open import Numbers.Naturals.Semiring -- for length
open import Numbers.Naturals.Order
open import Semirings.Definition
open import Maybe

module Lists.Lists where

open import Lists.Definition public
open import Lists.Length public
open import Lists.Concat public
open import Lists.Map.Map public
open import Lists.Reversal.Reversal public
open import Lists.Monad public
open import Lists.Filter.AllTrue public
open import Lists.Fold.Fold public

replicate : {a : _} {A : Set a} (n : ℕ) (x : A) → List A
replicate zero x = []
replicate (succ n) x = x :: replicate n x

head : {a : _} {A : Set a} (l : List A) (pr : 0 <N length l) → A
head [] (le x ())
head (x :: l) pr = x

lengthRev : {a : _} {A : Set a} (l : List A) → length (rev l) ≡ length l
lengthRev [] = refl
lengthRev (x :: l) rewrite lengthConcat (rev l) (x :: []) | lengthRev l | Semiring.commutative ℕSemiring (length l) 1 = refl

listLast : {a : _} {A : Set a} (l : List A) → Maybe A
listLast [] = no
listLast (x :: []) = yes x
listLast (x :: y :: l) = listLast (y :: l)

listZip : {a b c : _} {A : Set a} {B : Set b} {C : Set c} (f : A → B → C) → (f1 : A → C) → (f2 : B → C) →(l1 : List A) (l2 : List B) → List C
listZip f f1 f2 [] l2 = map f2 l2
listZip f f1 f2 (x :: l1) [] = map f1 (x :: l1)
listZip f f1 f2 (x :: l1) (y :: l2) = (f x y) :: listZip f f1 f2 l1 l2

contains : {a : _} {A : Set a} (l : List A) (needle : A) → Set a
contains [] needle = False'
contains (x :: l) needle = (x ≡ needle) || contains l needle

containsMap : {a b : _} {A : Set a} {B : Set b} (f : A → B) (l : List A) (needle : A) → (contains l needle) → contains (map f l) (f needle)
containsMap f (x :: l) needle (inl cont) = inl (applyEquality f cont)
containsMap f (x :: l) needle (inr cont) = inr (containsMap f l needle cont)

containsAppend : {a : _} {A : Set a} (l1 l2 : List A) (needle : A) → (contains (l1 ++ l2) needle) → (contains l1 needle) || (contains l2 needle)
containsAppend [] l2 needle cont = inr cont
containsAppend (x :: l1) l2 needle (inl pr) = inl (inl pr)
containsAppend (x :: l1) l2 needle (inr pr) with containsAppend l1 l2 needle pr
containsAppend (x :: l1) l2 needle (inr pr) | inl ans = inl (inr ans)
containsAppend (x :: l1) l2 needle (inr pr) | inr ans = inr ans

containsAppend' : {a : _} {A : Set a} (l1 l2 : List A) (needle : A) → (contains l1 needle) || (contains l2 needle) → contains (l1 ++ l2) needle
containsAppend' (x :: l1) l2 needle (inl (inl pr)) = inl pr
containsAppend' (x :: l1) l2 needle (inl (inr pr)) = inr (containsAppend' l1 l2 needle (inl pr))
containsAppend' [] l2 needle (inr pr) = pr
containsAppend' (x :: l1) l2 needle (inr pr) = inr (containsAppend' l1 l2 needle (inr pr))

containsCons : {a : _} {A : Set a} (x : A) (l : List A) (needle : A) → (contains (x :: l) needle) → (x ≡ needle) || (contains l needle)
containsCons x l needle pr = pr

containsCons' : {a : _} {A : Set a} (x : A) (l : List A) (needle : A) → (x ≡ needle) || (contains l needle) → (contains (x :: l) needle)
containsCons' x l needle pr = pr

containsDecidable : {a : _} {A : Set a} (decidableEquality : (x y : A) → (x ≡ y) || ((x ≡ y) → False)) → (l : List A) → (needle : A) → (contains l needle) || ((contains l needle) → False)
containsDecidable decide [] needle = inr λ ()
containsDecidable decide (x :: l) needle with decide x needle
containsDecidable decide (x :: l) .x | inl refl = inl (inl refl)
containsDecidable decide (x :: l) needle | inr x!=n with containsDecidable decide l needle
containsDecidable decide (x :: l) needle | inr x!=n | inl isIn = inl (inr isIn)
containsDecidable decide (x :: l) needle | inr x!=n | inr notIn = inr t
  where
    t : ((x ≡ needle) || contains l needle) → False
    t (inl x) = x!=n x
    t (inr x) = notIn x

filter' : {a b : _} {A : Set a} {pred : A → Set b} → (dec : (a : A) → pred a || (pred a → False)) → List A → List A
filter' dec [] = []
filter' dec (x :: l) with dec x
... | inl _ = x :: filter' dec l
... | inr _ = filter' dec l


text:
module CTL.Proof.EG where

open import CTL.Modalities.EG
open import FStream.Bisimulation
open import FStream.Core
open import FStream.FVec
open import Library

infixr 5 _▻EG_
infix 6 ⟨_▻EG
infix 7 _⟩EG

infixr 5 _▻EGᵢ_
infix 7 _⟩EGᵢ

data proofEG {ℓ₁ ℓ₂} {C : Container ℓ₁} : {n : ℕ} →
     (props : FVec C (Set ℓ₂) n) → Set (ℓ₁ ⊔ ℓ₂) where
  []EG : proofEG FNil
  ConsEG : ∀ {n} {props : ⟦ C ⟧ (Set ℓ₂ × FVec C (Set ℓ₂) n)} →
    E (fmap (λ x → (proj₁ x) × (proofEG (proj₂ x))) props) →
      proofEG (FCons props)

_pre⟨_▻EG : ∀ {i} {ℓ₁ ℓ₂} {C : Container ℓ₁} {m n}
              {props : FVec C (Set ℓ₂) m} {props' : FVec C (Set ℓ₂) (suc n)}
          → proofEG props
          → proofEG props'
          → EG {i} (props pre⟨ props' ▻⋯)
proj₁ ([]EG pre⟨ ConsEG (pos , _) ▻EG) = pos
nowE (proj₂ ([]EG pre⟨ ConsEG (_ , proof , _) ▻EG)) = proof
laterE (proj₂ ([]EG pre⟨ ConsEG (pos , proof , proofs) ▻EG)) =
  proofs pre⟨ ConsEG (pos , proof , proofs) ▻EG
proj₁ (ConsEG (pos , _) pre⟨ _ ▻EG) = pos
nowE   (proj₂ (ConsEG (pos , proof , proofs) pre⟨ _ ▻EG)) = proof
laterE (proj₂ (ConsEG (_   , _     , proofs) pre⟨ v ▻EG)) = proofs pre⟨ v ▻EG

-- TODO It's worth a thought whether we want to roll our own Sigma types
-- in order to have more meaningful projector names than projᵢ

⟨_▻EG : ∀ {i} {ℓ₁ ℓ₂} {C : Container ℓ₁} {n} {props : FVec C (Set ℓ₂) (suc n)}
      → proofEG props → EG {i} (FNil pre⟨ props ▻⋯)
⟨_▻EG = []EG pre⟨_▻EG

_⟩EG : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} {prop : ⟦ C ⟧ (Set ℓ₂)}
     → E prop
     → proofEG (FCons (fmap (_, FNil) prop))
(pos , proof) ⟩EG = ConsEG (pos , (proof , []EG))

_⟩EGᵢ : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} {prop : ⟦ C ⟧ (Set ℓ₂)}
          {pos : Position C (proj₁ prop)}
      → proj₂ prop pos
      → proofEG (FCons (fmap (_, FNil) prop))
_⟩EGᵢ {pos = pos} proof = ConsEG (pos , (proof , []EG))

_▻EG_ : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁}
        {prop : ⟦ C ⟧ (Set ℓ₂)} {n} {props : FVec C (Set ℓ₂) n}
      → E prop
      → proofEG props
      → proofEG (FCons (fmap (_, props) prop))
(pos , proof) ▻EG proofs = ConsEG (pos , (proof , proofs))

_▻EGᵢ_ : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} {prop : ⟦ C ⟧ (Set ℓ₂)} {n}
           {props : FVec C (Set ℓ₂) n} {pos : Position C (proj₁ prop)}
       → proj₂ prop pos
       → proofEG props
       → proofEG (FCons (fmap (_, props) prop))
_▻EGᵢ_ {pos = pos} proof proofs = ConsEG (pos , (proof , proofs))

mapEGlemma : ∀ {i} {ℓ₁ ℓ₂ ℓ₃} {C : Container ℓ₁} {A : Set ℓ₂}
               {f : A → Set ℓ₃} {m n}
           → (v : FVec C A m)
           → (v' : FVec C A (suc n))
           → EG {i} (vmap f v pre⟨ vmap f v' ▻⋯)
           → EG {i} (map f (v pre⟨ v' ▻⋯))
proj₁ (mapEGlemma FNil (FCons x) (pos , proof)) = pos
nowE (proj₂ (mapEGlemma FNil (FCons x) (pos , proofs))) = nowE proofs
laterE (proj₂ (mapEGlemma {f = f} FNil (FCons (shape , vals)) (pos , proof)))
  with vals pos
... | a , v = mapEGlemma v (FCons (shape , vals)) (laterE proof)
proj₁ (mapEGlemma (FCons (proj₃ , proj₄)) v' (pos , proofs)) = pos
nowE (proj₂ (mapEGlemma (FCons x) v' (pos , proofs))) = nowE proofs
laterE (proj₂ (mapEGlemma (FCons (shape , vals)) v' (pos , proofs)))
  with vals pos
... | a , v = mapEGlemma v v' (laterE proofs)

mapEG : ∀ {i} {ℓ₁ ℓ₂ ℓ₃} {C : Container ℓ₁} {A : Set ℓ₂} {f : A → Set ℓ₃}
          {m n} {v : FVec C A m} {v' : FVec C A (suc n)}
      → EG {i} ((vmap f v pre⟨ vmap f v' ▻⋯))
      → EG {i} (map f (v pre⟨ v' ▻⋯))
mapEG {v = v} {v' = v'} proofs = mapEGlemma v v' proofs

mutual
  -- TODO Rename to ∼EG?
  bisimEG : ∀ {i} {ℓ₁ ℓ₂} {C : Container ℓ₁} {s₁ s₂ : FStream C (Set ℓ₂)}
          → s₁ ~ s₂ → EG {i} s₁ → EG {i} s₂
  proj₁ (bisimEG {C = C} bs (pos , proofs)) =
    subst (Position C) (sameInitShapes bs) pos
  proj₂ (bisimEG bs (pos , proofs)) = bisimEG' (bisim bs pos) proofs

  bisimEG' : ∀ {i} {ℓ₁ ℓ₂} {C : Container ℓ₁} {s₁ s₂ : FStream' C (Set ℓ₂)}
           → s₁ ~' s₂ → EG' {i} s₁ → EG' {i} s₂
  -- TODO This subst trick must already exist in stdlib somewhere
  nowE (bisimEG' bs proof) = subst (λ x → x) (hd∼ bs) (nowE proof)
  laterE (bisimEG' {C = C} bs proof) = bisimEG (tl∼ bs) (laterE proof)

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
module Point where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

record Point : Set where
  field
    x : Nat
    y : Nat

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

open Point renaming (x to getX; y to getY)

<_,_> : Nat -> Nat -> Point
< x , y > = record { x = x; y = y }

η : (p : Point) -> p == record { x = getX p; y = getY p }
η p = refl

swap : Point -> Point
swap p = < getY p , getX p >

swap-idem : (p : Point) -> swap (swap p) == p
swap-idem p = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Nat
open import Prelude
open import aasubsume-min
open import contexts
open import judgemental-erase
open import lemmas-matching
open import statics-core
open import synth-unicity

module determinism where
  -- since we do not specify the name of newly inserted hole names,
  -- we only have determinism up to renaming of holes. we don't
  -- need to consider alpha equivalence for binders, since the
  --
  -- the same action applied to the same type makes the same type
  actdet-type : {t t' t'' : ztyp} {α : action} →
                (t + α +> t') →
                (t + α +> t'') →
                (t' == t'')
  actdet-type TMArrChild1 TMArrChild1 = refl
  actdet-type TMArrChild2 TMArrChild2 = refl
  actdet-type TMArrParent1 TMArrParent1 = refl
  actdet-type TMArrParent1 (TMArrZip1 ())
  actdet-type TMArrParent2 TMArrParent2 = refl
  actdet-type TMArrParent2 (TMArrZip2 ())
  actdet-type TMDel TMDel = refl
  actdet-type TMConArrow TMConArrow = refl
  actdet-type TMConNum TMConNum = refl
  actdet-type (TMArrZip1 ()) TMArrParent1
  actdet-type (TMArrZip1 p1) (TMArrZip1 p2) with actdet-type p1 p2
  ... | refl = refl
  actdet-type (TMArrZip2 ()) TMArrParent2
  actdet-type (TMArrZip2 p1) (TMArrZip2 p2) with actdet-type p1 p2
  ... | refl = refl
  actdet-type TMPlusChild1 TMPlusChild1 = refl
  actdet-type TMPlusChild2 TMPlusChild2 = refl
  actdet-type TMPlusParent1 TMPlusParent1 = refl
  actdet-type (TMPlusZip1 ()) TMPlusParent1
  actdet-type TMPlusParent2 TMPlusParent2 = refl
  actdet-type (TMPlusZip2 ()) TMPlusParent2
  actdet-type TMConPlus TMConPlus = refl
  actdet-type TMPlusParent1 (TMPlusZip1 ())
  actdet-type (TMPlusZip1 x) (TMPlusZip1 y) with actdet-type x y
  ... | refl = refl
  actdet-type TMPlusParent2 (TMPlusZip2 ())
  actdet-type (TMPlusZip2 x) (TMPlusZip2 y) with actdet-type x y
  ... | refl = refl
  actdet-type TMProdChild1 TMProdChild1 = refl
  actdet-type TMProdChild2 TMProdChild2 = refl
  actdet-type TMProdParent1 TMProdParent1 = refl
  actdet-type TMProdParent1 (TMProdZip1 ())
  actdet-type TMProdParent2 TMProdParent2 = refl
  actdet-type TMProdParent2 (TMProdZip2 ())
  actdet-type TMConProd TMConProd = refl
  actdet-type (TMProdZip1 ()) TMProdParent1
  actdet-type (TMProdZip1 x) (TMProdZip1 y) with actdet-type x y
  ... | refl = refl
  actdet-type (TMProdZip2 ()) TMProdParent2
  actdet-type (TMProdZip2 x) (TMProdZip2 y) with actdet-type x y
  ... | refl = refl

  -- all expressions only move to one other expression
  movedet : {e e' e'' : zexp} {δ : direction} →
            (e + move δ +>e e') →
            (e + move δ +>e e'') →
            e' == e''
  movedet EMAscChild1 EMAscChild1 = refl
  movedet EMAscChild2 EMAscChild2 = refl
  movedet EMAscParent1 EMAscParent1 = refl
  movedet EMAscParent2 EMAscParent2 = refl
  movedet EMLamChild1 EMLamChild1 = refl
  movedet EMLamParent EMLamParent = refl
  movedet EMHalfLamChild1 EMHalfLamChild1 = refl
  movedet EMHalfLamChild2 EMHalfLamChild2 = refl
  movedet EMHalfLamParent1 EMHalfLamParent1 = refl
  movedet EMHalfLamParent2 EMHalfLamParent2 = refl
  movedet EMPlusChild1 EMPlusChild1 = refl
  movedet EMPlusChild2 EMPlusChild2 = refl
  movedet EMPlusParent1 EMPlusParent1 = refl
  movedet EMPlusParent2 EMPlusParent2 = refl
  movedet EMApChild1 EMApChild1 = refl
  movedet EMApChild2 EMApChild2 = refl
  movedet EMApParent1 EMApParent1 = refl
  movedet EMApParent2 EMApParent2 = refl
  movedet EMNEHoleChild1 EMNEHoleChild1 = refl
  movedet EMNEHoleParent EMNEHoleParent = refl
  movedet EMInlChild1 EMInlChild1 = refl
  movedet EMInlParent EMInlParent = refl
  movedet EMInrChild1 EMInrChild1 = refl
  movedet EMInrParent EMInrParent = refl
  movedet EMCaseParent1 EMCaseParent1 = refl
  movedet EMCaseParent2 EMCaseParent2 = refl
  movedet EMCaseParent3 EMCaseParent3 = refl
  movedet EMCaseChild1 EMCaseChild1 = refl
  movedet EMCaseChild2 EMCaseChild2 = refl
  movedet EMCaseChild3 EMCaseChild3 = refl
  movedet EMPairChild1 EMPairChild1 = refl
  movedet EMPairChild2 EMPairChild2 = refl
  movedet EMPairParent1 EMPairParent1 = refl
  movedet EMPairParent2 EMPairParent2 = refl
  movedet EMFstChild1 EMFstChild1 = refl
  movedet EMFstParent EMFstParent = refl
  movedet EMSndChild1 EMSndChild1 = refl
  movedet EMSndParent EMSndParent = refl

  -- non-movement lemmas; theses show up pervasively throughout and save a
  -- lot of pattern matching.
  lem-nomove-part : ∀ {t t'} → ▹ t ◃ + move parent +> t' → ⊥
  lem-nomove-part ()

  lem-nomove-pars : ∀{Γ e t e' t'} → Γ ⊢ ▹ e ◃ => t ~ move parent ~> e' => t' → ⊥
  lem-nomove-pars (SAMove ())

  lem-nomove-para : ∀{Γ e t e'} → Γ ⊢ ▹ e ◃ ~ move parent ~> e' ⇐ t → ⊥
  lem-nomove-para (AASubsume e x x₁ x₂) = lem-nomove-pars x₁
  lem-nomove-para (AAMove ())

  -- if a move action on a synthetic action makes a new form, it's unique
  synthmovedet : {Γ : tctx} {e e' e'' : zexp} {t' t'' : htyp} {δ : direction} →
                 Γ ⊢ e => t' ~ move δ ~> e'' => t'' →
                 e + move δ +>e e' →
                 e'' == e'
  synthmovedet (SAMove m1) m2 = movedet m1 m2
  -- all these cases lead to absurdities based on movement
  synthmovedet (SAZipAsc1 x) EMAscParent1 = abort (lem-nomove-para x)
  synthmovedet (SAZipAsc2 x _ _ _) EMAscParent2 = abort (lem-nomove-part x)
  synthmovedet (SAZipApArr _ _ _ x _) EMApParent1 = abort (lem-nomove-pars x)
  synthmovedet (SAZipApAna _ _ x) EMApParent2 = abort (lem-nomove-para x)
  synthmovedet (SAZipPlus1 x) EMPlusParent1 = abort (lem-nomove-para x)
  synthmovedet (SAZipPlus2 x) EMPlusParent2 = abort (lem-nomove-para x)
  synthmovedet (SAZipNEHole _ _ x) EMNEHoleParent = abort (lem-nomove-pars x)
  synthmovedet (SAZipPair1 _ _ x _) EMPairParent1 = abort (lem-nomove-pars x)
  synthmovedet (SAZipPair2 _ _ _ x) EMPairParent2 = abort (lem-nomove-pars x)
  synthmovedet (SAZipFst _ _ _ _ x) EMFstParent = abort (lem-nomove-pars x)
  synthmovedet (SAZipSnd _ _ _ _ x) EMSndParent = abort (lem-nomove-pars x)
  synthmovedet (SAZipLam1 _ _ _ x _ _) EMHalfLamParent1 = abort (lem-nomove-part x)
  synthmovedet (SAZipLam2 _ _ _ x) EMHalfLamParent2 = abort (lem-nomove-pars x)

  anamovedet : {Γ : tctx} {e e' e'' : zexp} {t : htyp} {δ : direction} →
               Γ ⊢ e ~ move δ ~> e'' ⇐ t →
               e + move δ +>e e' →
               e'' == e'
  anamovedet (AASubsume x₂ x x₃ x₁) m = synthmovedet x₃ m
  anamovedet (AAMove x) m = movedet x m
  anamovedet (AAZipLam x₁ x₂ d) EMLamParent = abort (lem-nomove-para d)
  anamovedet (AAZipInl x d) EMInlParent = abort (lem-nomove-para d)
  anamovedet (AAZipInr x d) EMInrParent = abort (lem-nomove-para d)
  anamovedet (AAZipCase1 x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈) EMCaseParent1 =
    abort (lem-nomove-pars x₅)
  anamovedet (AAZipCase2 x₁ x₂ x₃ x₄ d) EMCaseParent2 = abort (lem-nomove-para d)
  anamovedet (AAZipCase3 x₁ x₂ x₃ x₄ d) EMCaseParent3 = abort (lem-nomove-para d)

  lem-plusholematch : ∀ {t t1 t2} → t ~̸ (⦇-⦈ ⊕ ⦇-⦈) → t ~ ⦇-⦈ → t ▸sum (t1 ⊕ t2) → ⊥
  lem-plusholematch a TCRefl MSHole = a TCHole2
  lem-plusholematch a TCHole1 MSHole = a TCHole2
  lem-plusholematch a TCHole1 MSSum = a (TCSum TCHole1 TCHole1)
  lem-plusholematch a TCHole2 MSHole = a TCHole2

  lem-prodholematch : ∀ {t t1 t2} → t ~̸ (⦇-⦈ ⊠ ⦇-⦈) → t ~ ⦇-⦈ → t ▸prod (t1 ⊠ t2) → ⊥
  lem-prodholematch a TCRefl MPHole = a TCHole2
  lem-prodholematch a TCHole1 MPHole = a TCHole2
  lem-prodholematch a TCHole1 MPProd = a (TCProd TCHole1 TCHole1)
  lem-prodholematch a TCHole2 MPHole = a TCHole2

  mutual
    -- an action on an expression in a synthetic position produces one
    -- resultant expression and type.
    actdet-synth : {Γ : tctx} {e e' e'' : zexp} {e◆ : hexp} {t t' t'' : htyp} {α : action} →
                   (E : erase-e e e◆) →
                   (Γ ⊢ e◆ => t) →
                   (d1 : Γ ⊢ e => t ~ α ~> e'  => t') →
                   (d2 : Γ ⊢ e => t ~ α ~> e'' => t'') →
                   {p1 : aasubmin-synth d1} →
                   {p2 : aasubmin-synth d2} →
                   (e' == e'' × t' == t'')
    actdet-synth er wt (SAMove x₁) (SAMove x₂) = movedet x₁ x₂ , refl
    actdet-synth er wt SADel SADel = refl , refl
    actdet-synth er wt SAConAsc SAConAsc = refl , refl
    actdet-synth er wt (SAConPlus1 x₁) (SAConPlus1 x₂) = refl , refl
    actdet-synth er wt (SAConPlus1 x₁) (SAConPlus2 x₂) = abort (x₂ x₁)
    actdet-synth er wt (SAConPlus2 x₁) (SAConPlus1 x₂) = abort (x₁ x₂)
    actdet-synth er wt (SAConPlus2 x₁) (SAConPlus2 x₂) = refl , refl
    actdet-synth er wt (SAConApArr x₁) (SAConApArr x₂)
      with ▸arr-unicity x₁ x₂
    ... | refl = refl , refl
    actdet-synth er wt (SAConApArr x₁) (SAConApOtw x₂) = abort (x₂ (▸arr-consist-hole x₁))
    actdet-synth er wt (SAConApOtw x₁) (SAConApArr x₂) = abort (x₁ (▸arr-consist-hole x₂))
    actdet-synth er wt (SAConApOtw x₁) (SAConApOtw x₂) = refl , refl
    actdet-synth er wt SAConNEHole SAConNEHole = refl , refl

    actdet-synth (EEAscL E) (SAsc x) (SAMove EMAscParent1) (SAZipAsc1 x₂) =
      abort (lem-nomove-para x₂)
    actdet-synth (EEAscL E) (SAsc x) (SAZipAsc1 x₁) (SAMove EMAscParent1) =
      abort (lem-nomove-para x₁)
    actdet-synth (EEAscL E) (SAsc x) (SAZipAsc1 x₁) (SAZipAsc1 x₂) {p1} {p2}
     with actdet-ana E x x₁ x₂ {p1} {p2}
    ... | refl = refl , refl

    actdet-synth (EEAscR x) (SAsc x₁) (SAMove EMAscParent2) (SAZipAsc2 a _ _ _) =
      abort (lem-nomove-part a)
    actdet-synth (EEAscR x) (SAsc x₁) (SAZipAsc2 a _ _ _) (SAMove EMAscParent2) =
      abort (lem-nomove-part a)
    actdet-synth (EEAscR x) (SAsc x₂) (SAZipAsc2 a e1 _ _) (SAZipAsc2 b e2 _ _)
      with actdet-type a b
    ... | refl = refl , eraset-det e1 e2

    actdet-synth (EEHalfLamL x) (SLam x₁ wt) (SAMove EMHalfLamParent1)
                 (SAZipLam1 x₃ x₄ x₅ x₆ x₇ x₈) = abort (lem-nomove-part x₆)
    actdet-synth (EEHalfLamL x) (SLam x₁ wt) (SAZipLam1 x₂ x₃ x₄ x₅ x₆ x₇)
                 (SAMove EMHalfLamParent1) = abort (lem-nomove-part x₅)
    actdet-synth (EEHalfLamL x) (SLam x₁ wt) (SAZipLam1 x₂ x₃ x₄ x₅ x₆ x₇)
                 (SAZipLam1 x₈ x₉ x₁₀ x₁₁ x₁₂ x₁₃) with actdet-type x₅ x₁₁
    ... | refl with eraset-det x₄ x₁₀
    ... | refl with synthunicity x₇ x₁₃
    ... | refl = refl , refl

    actdet-synth (EEHalfLamR er) (SLam x wt) (SAMove EMHalfLamParent2)
                 (SAZipLam2 x₂ x₃ x₄ y) = abort (lem-nomove-pars y)
    actdet-synth (EEHalfLamR er) (SLam x wt) (SAZipLam2 x₁ x₂ x₃ x₄)
                 (SAMove EMHalfLamParent2) = abort (lem-nomove-pars x₄)
    actdet-synth (EEHalfLamR er) (SLam x wt) (SAZipLam2 x₁ x₂ x₃ d1)
                 (SAZipLam2 x₅ x₆ x₇ d2) {p1} {p2} with erasee-det x₂ x₆
    ... | refl with actdet-synth x₂ x₃ d1 d2 {p1} {p2}
    ... | refl , refl = refl , refl

    actdet-synth (EEApL E) (SAp m wt x) (SAMove EMApParent1) (SAZipApArr _ x₂ x₃ d2 x₄) =
      abort (lem-nomove-pars d2)
    actdet-synth (EEApL E) (SAp m wt x) (SAZipApArr _ x₁ x₂ d1 x₃) (SAMove EMApParent1) =
      abort (lem-nomove-pars d1)
    actdet-synth (EEApL E) (SAp m wt x) (SAZipApArr a x₁ x₂ d1 x₃)
                 (SAZipApArr b x₄ x₅ d2 x₆) {p1} {p2}
      with erasee-det x₁ x₄
    ... | refl with synthunicity x₂ x₅
    ... | refl with erasee-det E x₁
    ... | refl with actdet-synth E x₅ d1 d2 {p1} {p2}
    ... | refl , refl with ▸arr-unicity a b
    ... | refl = refl , refl

    actdet-synth (EEApR E) (SAp m wt x) (SAMove EMApParent2) (SAZipApAna x₂ x₃ x₄) =
      abort (lem-nomove-para x₄)
    actdet-synth (EEApR E) (SAp m wt x) (SAZipApAna x₁ x₂ x₃) (SAMove EMApParent2) =
      abort (lem-nomove-para x₃)
    actdet-synth (EEApR E) (SAp m wt x) (SAZipApAna x₁ x₂ d1) (SAZipApAna x₄ x₅ d2)  {p1} {p2}
     with synthunicity m x₂
    ... | refl with ▸arr-unicity x₁ wt
    ... | refl with synthunicity m x₅
    ... | refl with ▸arr-unicity x₄ wt
    ... | refl with actdet-ana E x d1 d2  {p1} {p2}
    ... | refl = refl , refl

    actdet-synth (EEPlusL E) (SPlus x x₁) (SAMove EMPlusParent1) (SAZipPlus1 d2) =
      abort (lem-nomove-para d2)
    actdet-synth (EEPlusL E) (SPlus x x₁) (SAZipPlus1 x₂) (SAMove EMPlusParent1) =
      abort (lem-nomove-para x₂)
    actdet-synth (EEPlusL E) (SPlus x x₁) (SAZipPlus1 x₂) (SAZipPlus1 x₃) {p1} {p2}
      = ap1 (λ x₄ → x₄ ·+₁ _) (actdet-ana E x x₂ x₃  {p1} {p2}) , refl

    actdet-synth (EEPlusR E) (SPlus x x₁) (SAMove EMPlusParent2) (SAZipPlus2 x₃) =
      abort (lem-nomove-para x₃)
    actdet-synth (EEPlusR E) (SPlus x x₁) (SAZipPlus2 x₂) (SAMove EMPlusParent2) =
      abort (lem-nomove-para x₂)
    actdet-synth (EEPlusR E) (SPlus x x₁) (SAZipPlus2 x₂) (SAZipPlus2 x₃) {p1} {p2}
      = ap1 (_·+₂_ _) (actdet-ana E x₁ x₂ x₃ {p1} {p2}) , refl

    actdet-synth EETop SEHole (SAConVar {Γ = G} p) (SAConVar p₁) =
      refl , (ctxunicity {Γ = G} p p₁)
    actdet-synth EETop SEHole (SAConLam x₁) (SAConLam x₂) = refl , refl
    actdet-synth EETop SEHole SAConNumlit SAConNumlit = refl , refl

    actdet-synth EETop (SNEHole wt) (SAFinish x) (SAFinish x₁) = refl , synthunicity x x₁

    actdet-synth (EENEHole E) (SNEHole wt) (SAMove EMNEHoleParent) (SAZipNEHole _ x₁ d2) =
      abort (lem-nomove-pars d2)
    actdet-synth (EENEHole E) (SNEHole wt) (SAZipNEHole _ x d1) (SAMove EMNEHoleParent) =
      abort (lem-nomove-pars d1)
    actdet-synth (EENEHole E) (SNEHole wt) (SAZipNEHole a x d1) (SAZipNEHole b x₁ d2) {p1} {p2}
      with erasee-det a b
    ... | refl with synthunicity x x₁
    ... | refl with actdet-synth a x d1 d2  {p1} {p2}
    ... | refl , refl = refl , refl

      -- new cases for sums
    actdet-synth EETop SEHole SAConInl SAConInl = refl , refl
    actdet-synth EETop SEHole SAConInr SAConInr = refl , refl
    actdet-synth er wt (SAConCase1 x₁ x₂ x₃) (SAConCase1 x₄ x₅ x₆) = refl , refl
    actdet-synth er wt (SAConCase1 x₁ x₂ MSHole) (SAConCase2 x₄ x₅ x₆) = abort (x₆ TCHole2)
    actdet-synth EETop wt (SAConCase1 x₁ x₂ MSSum) (SAConCase2 x₄ x₅ x₆) =
      abort (x₆ (TCSum TCHole1 TCHole1))
    actdet-synth EETop wt (SAConCase2 x₁ x₂ x₃) (SAConCase1 x₄ x₅ MSHole) = abort (x₃ TCHole2)
    actdet-synth EETop wt (SAConCase2 x₁ x₂ x₃) (SAConCase1 x₄ x₅ MSSum) =
      abort (x₃ (TCSum TCHole1 TCHole1))
    actdet-synth er wt (SAConCase2 x₁ x₂ x₃) (SAConCase2 x₄ x₅ x₆) = refl , refl

      -- new cases for products
    actdet-synth EETop wt (SAConFst1 x) (SAConFst1 x₁) with ▸prod-unicity x x₁
    ... | refl = refl , refl
    actdet-synth EETop wt (SAConFst1 x) (SAConFst2 x₁) = abort (x₁ (▸prod-consist-hole x))
    actdet-synth EETop wt (SAConFst2 x) (SAConFst1 x₁) = abort (x (▸prod-consist-hole x₁))
    actdet-synth EETop wt (SAConFst2 x) (SAConFst2 x₁) = refl , refl
    actdet-synth EETop wt (SAConSnd1 x) (SAConSnd1 x₁) with ▸prod-unicity x x₁
    ... | refl = refl , refl
    actdet-synth EETop wt (SAConSnd1 x) (SAConSnd2 x₁) = abort (x₁ (▸prod-consist-hole x))
    actdet-synth EETop wt (SAConSnd2 x) (SAConSnd1 x₁) = abort (x (▸prod-consist-hole x₁))
    actdet-synth EETop wt (SAConSnd2 x) (SAConSnd2 x₁) = refl , refl
    actdet-synth EETop SEHole SAConPair SAConPair = refl , refl
    actdet-synth (EEPairL er) (SPair wt wt₁) (SAMove EMPairParent1)
                 (SAZipPair1 er₁ wt₂ d wt₃) = abort (lem-nomove-pars d)
    actdet-synth (EEPairL er) (SPair wt wt₁) (SAZipPair1 er₁ wt₂ d wt₃)
                 (SAMove EMPairParent1) = abort (lem-nomove-pars d)
    actdet-synth (EEPairL er) (SPair wt wt₁) (SAZipPair1 er₁ wt₂ d₁ wt₃)
                 (SAZipPair1 er₂ wt₄ d₂ wt₅) {p1} {p2}
      with actdet-synth er₁ wt₂ d₁ d₂ {p1} {p2}
    ... | refl , refl = refl , refl
    actdet-synth (EEPairR er) (SPair wt wt₁) (SAMove EMPairParent2)
                 (SAZipPair2 wt₂ er₁ wt₃ d) = abort (lem-nomove-pars d)
    actdet-synth (EEPairR er) (SPair wt wt₁) (SAZipPair2 wt₂ er₁ wt₃ d)
                 (SAMove EMPairParent2) = abort (lem-nomove-pars d)
    actdet-synth (EEPairR er) (SPair wt wt₁) (SAZipPair2 wt₂ er₁ wt₃ d₁)
                 (SAZipPair2 wt₄ er₂ wt₅ d₂) {p1} {p2}
      with actdet-synth er₁ wt₃ d₁ d₂ {p1} {p2}
    ... | refl , refl = refl , refl
    actdet-synth (EEFst er) (SFst wt x₁) (SAMove EMFstParent)
                 (SAZipFst pr pr₁ er₁ wt₁ d) = abort (lem-nomove-pars d)
    actdet-synth (EEFst er) (SFst wt x₁) (SAZipFst pr pr₁ er₁ wt₁ d)
                 (SAMove EMFstParent) = abort (lem-nomove-pars d)
    actdet-synth (EEFst er) (SFst wt x₁) (SAZipFst pr pr₁ er₁ wt₁ d₁)
                 (SAZipFst pr₂ pr₃ er₂ wt₂ d₂) {p1} {p2}
      with erasee-det er₁ er₂
    ... | refl with synthunicity wt₁ wt₂
    ... | refl with actdet-synth er₁ wt₁ d₁ d₂ {p1} {p2}
    ... | refl , refl with ▸prod-unicity pr₁ pr₃
    ... | refl = refl , refl
    actdet-synth (EESnd er) (SSnd wt x₁) (SAMove EMSndParent) (SAZipSnd pr pr₁ er₁ wt₁ d) =
      abort (lem-nomove-pars d)
    actdet-synth (EESnd er) (SSnd wt x₁) (SAZipSnd pr pr₁ er₁ wt₁ d) (SAMove EMSndParent) =
      abort (lem-nomove-pars d)
    actdet-synth (EESnd er) (SSnd wt x₁) (SAZipSnd pr pr₁ er₁ wt₁ d₁)
                 (SAZipSnd pr₂ pr₃ er₂ wt₂ d₂) {p1} {p2}
      with erasee-det er₁ er₂
    ... | refl with synthunicity wt₁ wt₂
    ... | refl with actdet-synth er₁ wt₁ d₁ d₂ {p1} {p2}
    ... | refl , refl with ▸prod-unicity pr₁ pr₃
    ... | refl = refl , refl

    -- an action on an expression in an analytic position produces one
    -- resultant expression and type.
    actdet-ana : {Γ : tctx} {e e' e'' : zexp} {e◆ : hexp} {t : htyp} {α : action} →
                 erase-e e e◆ →
                 Γ ⊢ e◆ <= t →
                 (d1 : Γ ⊢ e ~ α ~> e' ⇐ t) →
                 (d2 : Γ ⊢ e ~ α ~> e'' ⇐ t) →
                 {p1 : aasubmin-ana d1} →
                 {p2 : aasubmin-ana d2} →
                 e' == e''
    -- lambda cases first
    -- an erased lambda can't be typechecked with subsume
    actdet-ana (EELam _) (ASubsume () _) _ _

    -- for things paired with movements, punt to the move determinism case
    actdet-ana _ _ D (AAMove y) = anamovedet D y
    actdet-ana _ _ (AAMove y) D =  ! (anamovedet D y)

    -- lambdas never match with subsumption actions, because it won't be well typed.
    actdet-ana EETop      (ALam x₁ x₂ wt) (AASubsume EETop () x₅ x₆) _
    actdet-ana (EELam _) (ALam x₁ x₂ wt) (AASubsume (EELam x₃) () x₅ x₆) _
    actdet-ana EETop      (ALam x₁ x₂ wt) _ (AASubsume EETop () x₅ x₆)
    actdet-ana (EELam _) (ALam x₁ x₂ wt) _ (AASubsume (EELam x₃) () x₅ x₆)

    -- with the cursor at the top, there are only two possible actions
    actdet-ana EETop (ALam x₁ x₂ wt) AADel AADel = refl
    actdet-ana EETop (ALam x₁ x₂ wt) AAConAsc AAConAsc = refl

    -- and for the remaining case, recurr on the smaller derivations
    actdet-ana (EELam er) (ALam x₁ x₂ wt) (AAZipLam x₃ x₄ d1) (AAZipLam x₅ x₆ d2) {p1} {p2}
       with ▸arr-unicity x₄ x₆
    ... | refl with ▸arr-unicity x₄ x₂
    ... | refl with actdet-ana er wt d1 d2  {p1} {p2}
    ... | refl = refl

    -- now the subsumption cases
    -- subsume / subsume, so pin things down then recurr
    actdet-ana er (ASubsume a b) (AASubsume x x₁ x₂ x₃) (AASubsume x₄ x₅ x₆ x₇) {p1} {p2}
      with erasee-det x₄ x
    ... | refl with erasee-det er x₄
    ... | refl with synthunicity x₅ x₁
    ... | refl = π1 (actdet-synth x x₅ x₂ x₆ {min-ana-lem x₂ p1} {min-ana-lem x₆ p2})

    -- (these are all repeated below, irritatingly.)
    actdet-ana EETop (ASubsume a b) (AASubsume EETop x SADel x₁) AADel = refl
    actdet-ana EETop (ASubsume a b) (AASubsume EETop x SAConAsc x₁) AAConAsc {p1} = abort p1
    actdet-ana EETop (ASubsume SEHole b) (AASubsume EETop SEHole (SAConVar {Γ = Γ} p) x₂)
               (AAConVar x₅ p₁)
      with ctxunicity {Γ = Γ} p p₁
    ... | refl = abort (x₅ x₂)
    actdet-ana EETop (ASubsume SEHole b) (AASubsume EETop SEHole (SAConLam x₄) x₂)
               (AAConLam1 x₅ m) {p1} = abort p1
    actdet-ana EETop (ASubsume a b) (AASubsume EETop x₁ (SAConLam x₃) x₂) (AAConLam2 x₅ x₆) =
      abort (x₆ x₂)
    actdet-ana EETop (ASubsume a b) (AASubsume EETop x₁ SAConNumlit x₂) (AAConNumlit x₄) =
      abort (x₄ x₂)
    actdet-ana EETop (ASubsume a b) (AASubsume EETop x (SAFinish x₂) x₁) (AAFinish x₄) = refl

    -- subsume / del
    actdet-ana er (ASubsume a b) AADel (AASubsume x x₁ SADel x₃) = refl
    actdet-ana er (ASubsume a b) AADel AADel = refl

    -- subsume / conasc
    actdet-ana EETop (ASubsume a b) AAConAsc (AASubsume EETop x₁ SAConAsc x₃) {p2 = p2} =
      abort p2
    actdet-ana er (ASubsume a b) AAConAsc AAConAsc = refl

    -- subsume / convar
    actdet-ana EETop (ASubsume SEHole b) (AAConVar x₁ p)
               (AASubsume EETop SEHole (SAConVar {Γ = Γ} p₁) x₅)
      with ctxunicity {Γ = Γ} p p₁
    ... | refl = abort (x₁ x₅)
    actdet-ana er (ASubsume a b) (AAConVar x₁ p) (AAConVar x₂ p₁) = refl

    -- subsume / conlam1
    actdet-ana EETop (ASubsume SEHole b) (AAConLam1 x₁ x₂)
               (AASubsume EETop SEHole (SAConLam x₃) x₆) {p2 = p2} = abort p2
    actdet-ana er (ASubsume a b) (AAConLam1 x₁ MAHole) (AAConLam2 x₃ x₄) =
      abort (x₄ TCHole2)
    actdet-ana er (ASubsume a b) (AAConLam1 x₁ MAArr) (AAConLam2 x₃ x₄) =
      abort (x₄ (TCArr TCHole1 TCHole1))
    actdet-ana er (ASubsume a b) (AAConLam1 x₁ x₂) (AAConLam1 x₃ x₄) = refl

    -- subsume / conlam2
    actdet-ana EETop (ASubsume SEHole TCRefl) (AAConLam2 x₁ x₂)
               (AASubsume EETop SEHole x₅ x₆) = abort (x₂ TCHole2)
    actdet-ana EETop (ASubsume SEHole TCHole1) (AAConLam2 x₁ x₂)
               (AASubsume EETop SEHole (SAConLam x₃) x₆) = abort (x₂ x₆)
    actdet-ana EETop (ASubsume SEHole TCHole2) (AAConLam2 x₁ x₂)
               (AASubsume EETop SEHole x₅ x₆) = abort (x₂ TCHole2)
    actdet-ana EETop (ASubsume a b) (AAConLam2 x₂ x₁) (AAConLam1 x₃ MAHole) = abort (x₁ TCHole2)
    actdet-ana EETop (ASubsume a b) (AAConLam2 x₂ x₁) (AAConLam1 x₃ MAArr) =
      abort (x₁ (TCArr TCHole1 TCHole1))
    actdet-ana er (ASubsume a b) (AAConLam2 x₂ x) (AAConLam2 x₃ x₄) = refl

    -- subsume / numlit
    actdet-ana er (ASubsume a b) (AAConNumlit x) (AASubsume x₁ x₂ SAConNumlit x₄) = abort (x x₄)
    actdet-ana er (ASubsume a b) (AAConNumlit x) (AAConNumlit x₁) = refl

    -- subsume / finish
    actdet-ana er (ASubsume a b) (AAFinish x) (AASubsume x₁ x₂ (SAFinish x₃) x₄) = refl
    actdet-ana er (ASubsume a b) (AAFinish x) (AAFinish x₁) = refl

    -- new cases for sums

    -- injections and cases, like lambdas, only check. so they can't be
    -- part of a subsume or a subsume action. so a lot of these cases
    -- just fall out immediately.
    actdet-ana (EEInl _) (ASubsume () _) _ _
    actdet-ana (EEInr _) (ASubsume () _) _ _
    actdet-ana (EECase1 _) (ASubsume () _) _ _
    actdet-ana (EECase2 _) (ASubsume () _) _ _
    actdet-ana (EECase3 _) (ASubsume () _) _ _

    actdet-ana EETop (AInl x wt) (AASubsume EETop () _ x₄) _
    actdet-ana EETop (AInl x wt) _ (AASubsume EETop () _ x₄)
    actdet-ana EETop (AInr x wt) (AASubsume EETop () _ x₄) _
    actdet-ana EETop (AInr x wt) _ (AASubsume EETop () _ x₄)
    actdet-ana EETop (ACase _ _ _ _ _ _) _ (AASubsume EETop () _ x₄)
    actdet-ana EETop (ACase _ _ _ _ _ _) (AASubsume EETop () _ x₄) _

    actdet-ana (EEInr er) (AInr x wt) (AASubsume (EEInr x₁) () x₃ x₄) _
    actdet-ana (EEInr er) (AInr x wt) _ (AASubsume (EEInr x₁) () x₃ x₄)
    actdet-ana (EEInl er) (AInl x wt) (AASubsume (EEInl x₁) () x₃ x₄) _
    actdet-ana (EEInl er) (AInl x wt) _ (AASubsume (EEInl x₁) () x₃ x₄)

    actdet-ana (EECase1 er) (ACase x₁ x₂ x₃ x₄ wt wt₁) _ (AASubsume (EECase1 x₉) () x₁₁ x₁₂)
    actdet-ana (EECase2 er) (ACase x₁ x₂ x₃ x₄ wt wt₁) _ (AASubsume (EECase2 x₉) () x₁₁ x₁₂)
    actdet-ana (EECase3 er) (ACase x₁ x₂ x₃ x₄ wt wt₁) _ (AASubsume (EECase3 x₉) () x₁₁ x₁₂)

    actdet-ana (EECase1 er) (ACase x₁ x₂ x₃ x₄ wt wt₁) (AASubsume (EECase1 x₉) () x₁₁ x₁₂) _
    actdet-ana (EECase2 er) (ACase x₁ x₂ x₃ x₄ wt wt₁) (AASubsume (EECase2 x₉) () x₁₁ x₁₂) _
    actdet-ana (EECase3 er) (ACase x₁ x₂ x₃ x₄ wt wt₁) (AASubsume (EECase3 x₉) () x₁₁ x₁₂) _

    actdet-ana EETop (ASubsume SEHole x₂) (AAConCase x₃ x₄)
               (AASubsume EETop SEHole (SAConCase1 x₁ x₅ MSHole) x₈) {p2 = p2} = abort p2
    actdet-ana EETop (ASubsume SEHole x₂) (AAConCase x₃ x₄)
               (AASubsume EETop SEHole (SAConCase2 x₁ x₅ x₆) x₈) = abort (x₆ TCHole2)
    actdet-ana EETop (ASubsume SEHole x₂) (AASubsume EETop SEHole (SAConCase1 x₁ x₃ MSHole) x₆)
               (AAConCase x₇ x₈) {p1} = abort p1
    actdet-ana EETop (ASubsume SEHole x₂) (AASubsume EETop SEHole (SAConCase2 x₁ x₃ x₄) x₆)
               (AAConCase x₇ x₈) = abort (x₄ TCHole2)

      -- the cases where the derivations match just go through
    actdet-ana er (ASubsume x x₁) (AAConInl1 x₂) (AAConInl1 x₃) = refl
    actdet-ana EETop (ASubsume SEHole x₁) (AAConInl2 x₂) (AAConInl2 x₃) = refl
    actdet-ana er (ASubsume x x₁) (AAConInr1 x₂) (AAConInr1 x₃) = refl
    actdet-ana er (ASubsume x x₁) (AAConInr2 x₂) (AAConInr2 x₃) = refl
    actdet-ana EETop (ASubsume SEHole x₂) (AAConCase x₃ x₄) (AAConCase x₅ x₆) = refl
    actdet-ana er (AInl x wt) AADel AADel = refl
    actdet-ana er (AInl x wt) AAConAsc AAConAsc = refl
    actdet-ana er (AInr x wt) AADel AADel = refl
    actdet-ana er (AInr x wt) AAConAsc AAConAsc = refl
    actdet-ana er (ACase x₁ x₂ x₃ x₄ wt wt₁) AADel AADel = refl
    actdet-ana er (ACase x₁ x₂ x₃ x₄ wt wt₁) AAConAsc AAConAsc = refl

    -- everything else we need to argue a little bit more carefully

    -- matching zipper cases; these cause us to recurr
    actdet-ana (EEInl er) (AInl x wt) (AAZipInl x₁ d1) (AAZipInl x₂ d2) {p1} {p2}
       with ▸sum-unicity x₂ x₁
    ... | refl with ▸sum-unicity x x₁
    ... | refl = ap1 inl (actdet-ana er wt d1 d2  {p1} {p2})

    actdet-ana (EEInr er) (AInr x wt) (AAZipInr x₁ d1) (AAZipInr x₂ d2) {p1} {p2}
       with ▸sum-unicity x₂ x₁
    ... | refl with ▸sum-unicity x x₁
    ... | refl = ap1 inr (actdet-ana er wt d1 d2  {p1} {p2})

    actdet-ana (EECase1 er) (ACase x₂ x₃ x₄ x₅ wt wt₁) (AAZipCase1 x₆ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ x₁₃)
               (AAZipCase1 x₁₄ x₁₅ x₁₆ x₁₇ x₁₈ x₁₉ x₂₀ x₂₁) {p1} {p2}
       with erasee-det x₈ x₁₆
    ... | refl with synthunicity x₁₇ x₉
    ... | refl with actdet-synth x₈ x₉ x₁₈ x₁₀ {p2} {p1}
    ... | refl , refl = refl

    actdet-ana (EECase2 er) (ACase x₂ x₃ x₄ x₅ wt wt₁) (AAZipCase2 x₆ x₇ x₈ x₉ d1)
               (AAZipCase2 x₁₁ x₁₂ x₁₃ x₁₄ d2) {p1} {p2}
       with synthunicity x₅ x₈
    ... | refl with synthunicity x₅ x₁₃
    ... | refl with ▸sum-unicity x₁₄ x₉
    ... | refl with ▸sum-unicity x₉ x₄
    ... | refl with actdet-ana er wt d1 d2 {p1} {p2}
    ... | refl = refl

    actdet-ana (EECase3 er) (ACase x₂ x₃ x₄ x₅ wt wt₁) (AAZipCase3 x₆ x₇ x₈ x₉ d1)
               (AAZipCase3 x₁₁ x₁₂ x₁₃ x₁₄ d2) {p1} {p2}
      with synthunicity x₈ x₁₃
    ... | refl with synthunicity x₈ x₅
    ... | refl with ▸sum-unicity x₄ x₉
    ... | refl with ▸sum-unicity x₄ x₁₄
    ... | refl with actdet-ana er wt₁ d1 d2 {p1} {p2}
    ... | refl = refl

    actdet-ana EETop (ASubsume SEHole x₁) (AASubsume EETop SEHole SAConInl x₅)
               (AAConInl1 x₆) {p1} = abort p1
    actdet-ana EETop (ASubsume SEHole x₁) (AASubsume EETop SEHole SAConInl x₅)
               (AAConInl2 x₆) = abort (x₆ x₅)
    actdet-ana EETop (ASubsume SEHole x₁) (AASubsume EETop SEHole SAConInr x₅)
               (AAConInr1 x₆) {p1} = abort p1
    actdet-ana EETop (ASubsume SEHole x₁) (AASubsume EETop SEHole SAConInr x₅)
               (AAConInr2 x₆) = abort (x₆ x₅)
    actdet-ana EETop (ASubsume SEHole x₁) (AAConInl1 x₂)
               (AASubsume EETop SEHole SAConInl x₆) {p2 = p2} = abort p2
    actdet-ana EETop (ASubsume SEHole x₁) (AAConInr1 x₂)
               (AASubsume EETop SEHole SAConInr c) {p2 = p2} = abort p2

    actdet-ana EETop (ASubsume SEHole x₁) (AAConInl1 q) (AAConInl2 x₃) =
      abort (lem-plusholematch x₃ x₁ q)
    actdet-ana EETop (ASubsume SEHole x₁) (AAConInl2 x₂) (AASubsume EETop SEHole SAConInl x₆) =
      abort (x₂ x₆)
    actdet-ana EETop (ASubsume SEHole x₁) (AAConInl2 x₂) (AAConInl1 q) =
      abort (lem-plusholematch x₂ x₁ q)
    actdet-ana EETop (ASubsume SEHole x₁) (AAConInr1 x₂) (AAConInr2 x₃) =
      abort (lem-plusholematch x₃ x₁ x₂)
    actdet-ana EETop (ASubsume SEHole x₁) (AAConInr2 x₂) (AASubsume EETop x₄ SAConInr x₆) =
      abort (x₂ x₆)
    actdet-ana EETop (ASubsume SEHole x₁) (AAConInr2 x₂) (AAConInr1 x₃) =
      abort (lem-plusholematch x₂ x₁ x₃)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
open import Agda.Builtin.Bool

module Issue4166.Import {b : Bool} where

instance

  i : Bool
  i = b

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

module SEquivSCPermEquiv where

-- Data types from standard library

open import Level        using (zero)
open import Data.Nat     using (ℕ; _+_)
open import Data.Fin     using (Fin; inject+; raise)
open import Data.Sum     using (inj₁; inj₂)
open import Data.Product using (_,_; proj₁; proj₂)
open import Data.Vec     using (tabulate) renaming (_++_ to _++V_)
open import Function     using (_∘_; id)

-- Properties from standard library

open import Data.Vec.Properties using    (lookup∘tabulate)
open import Relation.Binary     using    (Setoid)
open import Function.Equality   using    (_⇨_; _⟨$⟩_; _⟶_)
                                renaming (_∘_ to _⊚_; id to id⊚)

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; cong₂; setoid; →-to-⟶;
         module ≡-Reasoning)

-- Next are imports from our libraries of Proofs (FiniteFunctions and
-- VectorLemmas)

open import Proofs using (finext; _!!_; tabulate-split)

-- Next we import our notions of equivalences

open import Equiv using (_∼_; module qinv; mkqinv; _≃_)

-- Next we import sets equipped with equivalence relations and
-- specialize to our notions of equivalence

open import SetoidEquiv
  using (
  ≃S-Setoid;        -- statement of thm2
  _≃S_;             -- statement of thm2
  module _≃S_;      -- proof of thm2
  module _≋_;       -- proof of thm2
  equiv;            -- proof of thm2
  equivS;           -- proof of thm2
  _≋_              -- proof of thm2
--  id≃S
--  0≃S;
--  _≃S≡_;
--  _⊎≃S_
  )

-- Finally we import our definition of permutations. We start with Vec
-- (Fin m) n for arbitrary m and n which---if well-formed---would
-- define a permutation in the Cauchy representation. These vectors
-- assume a canonical enumeration of the finite sets which we make
-- explicit in the module Enumeration. To ensure these vectors are
-- well-formed, we define a concrete permutation as a pair of two such
-- vectors with two proofs that they compose to the identity
-- permutation.

open import FinVec using (_∘̂_; 1C)
open import FinVecProperties using (~⇒≡; !!⇒∘̂; 1C!!i≡i; cauchyext)
open import EnumEquiv using (Enum; 0E; _⊕e_; eval-left; eval-right)
open import FiniteType using (FiniteType; ∣_∣)
open import ConcretePermutation -- using (CPerm; cp; p≡; 0p; idp; _⊎p_) -- ; SCPerm)
open import ConcretePermutationProperties -- using (CPerm; cp; p≡; 0p; idp; _⊎p_) -- ; SCPerm)

------------------------------------------------------------------------------
-- The big (semantic) theorem!

thm2 : ∀ {A B : Set} → (a : FiniteType A) → (b : FiniteType B) →
  (≃S-Setoid A B) ≃S (SCPerm ∣ b ∣ ∣ a ∣)
thm2 {A} {B} (n , (enumA , mkqinv labelA αA βA))
             (m , (enumB , mkqinv labelB αB βB)) =
  equiv fwd' bwd' α β
  where
    open ≡-Reasoning
    AS = setoid A
    BS = setoid B
    A≃Fn : A ≃ Fin n
    A≃Fn = (enumA , mkqinv labelA αA βA)
    B≃Fn : B ≃ Fin m
    B≃Fn = (enumB , mkqinv labelB αB βB)
    CP⇨ = SCPerm m n ⇨ SCPerm m n

    fwd : (AS ≃S BS) → CPerm m n
    fwd A≃B = cp (tabulate f) (tabulate g) (~⇒≡ β) (~⇒≡ α)
      where
        module A≃SB = _≃S_ A≃B
        f : Fin n → Fin m
        f j = enumB (A≃SB.f ⟨$⟩ labelA j)

        g : Fin m → Fin n
        g j =  enumA (A≃SB.g ⟨$⟩ labelB j)

        α : f ∘ g ∼ id
        α i =
          begin
            (enumB (A≃SB.f ⟨$⟩ (labelA (enumA (A≃SB.g ⟨$⟩ labelB i))))
                ≡⟨ cong (λ x → enumB (A≃SB.f ⟨$⟩ x)) (βA ((A≃SB.g  ⟨$⟩ labelB i))) ⟩
            enumB (A≃SB.f ⟨$⟩ (A≃SB.g  ⟨$⟩ labelB i))
                ≡⟨ cong enumB (A≃SB.α refl) ⟩
            enumB (labelB i)
                ≡⟨ αB i ⟩
            i ∎)

        β : g ∘ f ∼ id
        β i =
          begin (
            enumA (A≃SB.g ⟨$⟩ labelB (enumB (A≃SB.f ⟨$⟩ labelA i)))
                ≡⟨ cong (λ x → enumA (A≃SB.g ⟨$⟩ x)) (βB _) ⟩
            enumA (A≃SB.g ⟨$⟩ (A≃SB.f ⟨$⟩ labelA i))
                ≡⟨ cong enumA (A≃SB.β refl) ⟩
            enumA (labelA i)
               ≡⟨ αA i ⟩
            i ∎)

    fwd' : ≃S-Setoid A B ⟶ setoid (CPerm m n)
    fwd' = record
     { _⟨$⟩_ = fwd
      ; cong = λ {i} {j} i≋j → p≡ (finext (λ k → cong enumB (f≡ i≋j (labelA k)) ))
     }
       where open _≋_

    bwd : CPerm m n → (AS ≃S BS)
    bwd (cp p₁ p₂ αp βp) = equiv f g α β
      where
        f : AS ⟶ BS
        f = →-to-⟶ (λ a → labelB (p₁ !! enumA a))

        g : BS ⟶ AS
        g = →-to-⟶ (λ b → labelA (p₂ !! (enumB b)))

        α : Setoid._≈_ (BS ⇨ BS) (f ⊚ g) id⊚
        α {b} {.b} refl =
          begin (
            labelB (p₁ !! (enumA (labelA (p₂ !! (enumB b)))))
              ≡⟨ cong (λ x → labelB (p₁ !! x)) (αA _) ⟩
            labelB (p₁ !! (p₂ !! enumB b))
              ≡⟨ cong labelB (!!⇒∘̂ _ _ (enumB b)) ⟩
            labelB ((p₂ ∘̂ p₁) !! enumB b)
              ≡⟨ cong (λ x → (labelB (x !! enumB b))) βp ⟩
           labelB (1C !! enumB b)
              ≡⟨ cong labelB 1C!!i≡i ⟩
           labelB (enumB b)
              ≡⟨ βB b ⟩
            b ∎)

        β : Setoid._≈_ (AS ⇨ AS) (g ⊚ f) id⊚
        β {a} {.a} refl =
          begin (
            labelA (p₂ !! (enumB (labelB (p₁ !! enumA a))))
              ≡⟨ cong (λ x → labelA (p₂ !! x)) (αB _) ⟩
            labelA (p₂ !! (p₁ !! enumA a))
              ≡⟨ cong labelA (!!⇒∘̂ _ _ (enumA a)) ⟩
            labelA ((p₁ ∘̂ p₂) !! enumA a)
              ≡⟨ cong (λ x → labelA (x !! enumA a)) αp ⟩
            labelA (1C !! enumA a)
              ≡⟨ cong labelA 1C!!i≡i ⟩
            labelA (enumA a)
              ≡⟨ βA a ⟩
            a ∎)

    bwd' : setoid (CPerm m n) ⟶ ≃S-Setoid A B
    bwd' = record
      { _⟨$⟩_ = bwd
      ; cong = λ { {π} {.π} refl → equivS (λ _ → refl) (λ _ → refl) }
      }

    α : Setoid._≈_ CP⇨ (fwd' ⊚ bwd') id⊚
    α {cp π πᵒ αp βp} refl = p≡ (trans (finext pf₁) (cauchyext π))
      where
        pf₁ : (j : Fin n) → enumB (labelB (π !! enumA (labelA j))) ≡ π !! j
        pf₁ j =
          begin (
            enumB (labelB (π !! enumA (labelA j)))
              ≡⟨ αB _ ⟩
            π !! enumA (labelA j)
              ≡⟨ cong (_!!_ π) (αA _) ⟩
            π !! j ∎)

    β : {x y : AS ≃S BS} → x ≋ y → ((bwd' ⊚ fwd') ⟨$⟩ x) ≋ y
    β {equiv f g α β} {equiv f₁ g₁ α₁ β₁} (equivS f≡ g≡) =
      equivS (λ a → trans (pf₁ a) (f≡ a)) (λ b → trans (pf₂ b) (g≡ b))
      where
        pf₁ : ∀ a → labelB (tabulate (λ j → enumB (f ⟨$⟩ labelA j)) !! (enumA a)) ≡ f ⟨$⟩ a
        pf₁ a =
          begin (
            labelB (tabulate (λ j → enumB (f ⟨$⟩ labelA j)) !! enumA a)
              ≡⟨ cong labelB (lookup∘tabulate _ (enumA a)) ⟩
            labelB (enumB (f ⟨$⟩ labelA (enumA a)))
              ≡⟨ βB _ ⟩
            f ⟨$⟩ labelA (enumA a)
              ≡⟨ cong (_⟨$⟩_ f) (βA _) ⟩
            f ⟨$⟩ a ∎)
        pf₂ : ∀ b → labelA (tabulate (λ j → enumA (g ⟨$⟩ labelB j)) !! (enumB b)) ≡ g ⟨$⟩ b
        pf₂ b =
          begin (
            labelA (tabulate (λ j → enumA (g ⟨$⟩ labelB j)) !! enumB b)
              ≡⟨ cong labelA (lookup∘tabulate _ (enumB b)) ⟩
            labelA (enumA (g ⟨$⟩ labelB (enumB b)))
              ≡⟨ βA _ ⟩
            g ⟨$⟩ labelB (enumB b)
              ≡⟨ cong (_⟨$⟩_ g) (βB _) ⟩
            g ⟨$⟩ b ∎ )

-- Start proving some of the transport lemmas.
-- Need to do:
-- 1. prove that we have a bijective morphism of carriers: done, this is thm2 (fwd is the morphism)
-- 2.  prove that it preserves:
--   a. id (done)
--   b. 0 (done)
--   c. + (done)
--   d. *

{--

Is this still important or has it been subsumed by the categorical work ???

Still important, I believe.  It will be used in proving the categorical
components of CPermCat.

open _≃S_

lemma_1a : ∀ {n} {A : Set} → (EA : Enum A n) → f (thm2 EA EA) ⟨$⟩ id≃S ≡ idp
lemma_1a (f' , mkqinv g α _) = p≡ (trans (finext α) F.reveal1C)

-- this is redundant, as it follows from lemma_1a.
lemma_1b : ∀ {n} {A : Set} → (EA : Enum A n) → (g (thm2 EA EA) ⟨$⟩ idp) ≋ id≃S
lemma_1b (enumA , mkqinv g _ β) =
  equivS (λ x → trans (cong g 1C!!i≡i) (β x)) (λ x → trans (cong g 1C!!i≡i) (β x))

lemma2 : f (thm2 0E 0E) ⟨$⟩ 0≃S ≡ 0p
lemma2 = p≡ F.reveal0C -- p≡ refl

lemma3 : ∀ {n₁ n₂} {A B C D : Set} {EA : Enum A n₁} {EB : Enum B n₁}
  {EC : Enum C n₂} {ED : Enum D n₂} → (x : A ≃S≡ B) → (y : C ≃S≡ D) →
   f (thm2 (EA ⊕e EC) (EB ⊕e ED)) ⟨$⟩ (x ⊎≃S y) ≡
   (f (thm2 EA EB) ⟨$⟩ x) ⊎p (f (thm2 EC ED) ⟨$⟩ y)
lemma3 {n₁} {n₂} {EA = EA} {EB} {EC} {ED} (equiv f₄ g₄ α₄ β₄) (equiv f₅ g₅ α₅ β₅) =
  p≡ (
    begin (
       CPerm.π (f (thm2 (EA ⊕e EC) (EB ⊕e ED)) ⟨$⟩ (x ⊎≃S y))
         ≡⟨ refl ⟩ -- inline f, fwd and π
       tabulate {n₁ + n₂} (λ j → enumBD (x⊎y.f ⟨$⟩ qAC.g j))
         ≡⟨ tabulate-split {n₁} {n₂} {f =  λ j → enumBD (x⊎y.f ⟨$⟩ qAC.g j)} ⟩
       tabulate {n₁} (λ j → enumBD (x⊎y.f ⟨$⟩ qAC.g (inject+ n₂ j))) ++V
       tabulate {n₂} (λ j → enumBD (x⊎y.f ⟨$⟩ qAC.g (raise n₁ j)))
         ≡⟨ cong₂ _++V_ (finext {n₁} pf₁) (finext pf₂) ⟩
       tabulate {n₁} (λ j → inject+ n₂ (tabulate (λ i → enumB (f₄ ⟨$⟩ qA.g i)) !! j)) ++V
       tabulate {n₂} (λ j → raise n₁ (tabulate (λ i → enumD (f₅ ⟨$⟩ qC.g i)) !! j))
         ≡⟨ sym F.reveal⊎c ⟩ -- going up, inline f, fwd, ⊎p and π
       CPerm.π ((f (thm2 EA EB) ⟨$⟩ x) ⊎p (f (thm2 EC ED) ⟨$⟩ y)) ∎))
  where
    open ≡-Reasoning
    x = equiv f₄ g₄ α₄ β₄
    y = equiv f₅ g₅ α₅ β₅
    enumB = proj₁ EB
    enumD = proj₁ ED
    enumAC = proj₁ (EA ⊕e EC)
    module qAC = qinv (proj₂ (EA ⊕e EC))
    module qA = qinv (proj₂ EA)
    module qC = qinv (proj₂ EC)
    enumBD = proj₁ (EB ⊕e ED)
    module x⊎y = _≃S_ (x ⊎≃S y)

    pf₁ :  (i : Fin n₁) →
      enumBD (x⊎y.f ⟨$⟩ qAC.g (inject+ n₂ i)) ≡
      inject+ n₂ (tabulate (λ i₁ → enumB (f₄ ⟨$⟩ qA.g i₁)) !! i)
    pf₁ i =
      begin (
        enumBD (x⊎y.f ⟨$⟩ qAC.g (inject+ n₂ i))
          ≡⟨ cong (λ j → enumBD (x⊎y.f ⟨$⟩ j)) (eval-left {eA = EA} {EC} i) ⟩
        enumBD (x⊎y.f ⟨$⟩ inj₁ (qA.g i))
          ≡⟨ refl ⟩ -- once the inj₁ is exposed, the rest happens by β-reduction
        inject+ n₂ (enumB (f₄ ⟨$⟩ qA.g i))
           ≡⟨ cong (inject+ n₂) (sym (lookup∘tabulate _ i)) ⟩
        inject+ n₂ (tabulate (λ j → enumB (f₄ ⟨$⟩ qA.g j)) !! i) ∎)

    pf₂ :  (i : Fin n₂) →
      enumBD (x⊎y.f ⟨$⟩ qAC.g (raise n₁ i)) ≡
      raise n₁ (tabulate (λ i₁ → enumD (f₅ ⟨$⟩ qC.g i₁)) !! i)
    pf₂ i =
      begin (
           enumBD (x⊎y.f ⟨$⟩ qAC.g (raise n₁ i))
             ≡⟨ cong (λ j → enumBD (x⊎y.f ⟨$⟩ j)) (eval-right {eA = EA} {EC} i) ⟩
           enumBD (x⊎y.f ⟨$⟩ inj₂ (qC.g i))
             ≡⟨ refl ⟩
           raise n₁ (enumD (f₅ ⟨$⟩ qC.g i))
             ≡⟨ cong (raise n₁) (sym (lookup∘tabulate _ i)) ⟩
           raise n₁ (tabulate (λ i₁ → enumD (f₅ ⟨$⟩ qC.g i₁)) !! i) ∎)
-}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module OlderBasicILP.Direct.Hilbert.Nested where

open import Common.Context public

-- Propositions of intuitionistic logic of proofs, without ∨, ⊥, or +.

mutual
  infixr 10 _⦂_
  infixl 9 _∧_
  infixr 7 _▻_
  data Ty : Set where
    α_  : Atom → Ty
    _▻_ : Ty → Ty → Ty
    _⦂_ : Box → Ty → Ty
    _∧_ : Ty → Ty → Ty
    ⊤  : Ty

  record Box : Set where
    inductive
    constructor [_]
    field
      {/A} : Ty
      t    : ∅ ⊢ /A

  -- Derivations, as Hilbert-style combinator trees.

  infix 3 _⊢_
  data _⊢_ (Γ : Cx Ty) : Ty → Set where
    var   : ∀ {A}              → A ∈ Γ → Γ ⊢ A
    app   : ∀ {A B}            → Γ ⊢ A ▻ B → Γ ⊢ A → Γ ⊢ B
    ci    : ∀ {A}              → Γ ⊢ A ▻ A
    ck    : ∀ {A B}            → Γ ⊢ A ▻ B ▻ A
    cs    : ∀ {A B C}          → Γ ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
    box   : ∀ {A}              → (t : ∅ ⊢ A) → Γ ⊢ [ t ] ⦂ A
    cdist : ∀ {A B} {t : ∅ ⊢ A ▻ B} {u : ∅ ⊢ A}
                               → Γ ⊢ [ t ] ⦂ (A ▻ B) ▻ [ u ] ⦂ A ▻ [ app t u ] ⦂ B
    cup   : ∀ {A} {t : ∅ ⊢ A} → Γ ⊢ [ t ] ⦂ A ▻ [ box t ] ⦂ [ t ] ⦂ A
    cdown : ∀ {A} {t : ∅ ⊢ A} → Γ ⊢ [ t ] ⦂ A ▻ A
    cpair : ∀ {A B}            → Γ ⊢ A ▻ B ▻ A ∧ B
    cfst  : ∀ {A B}            → Γ ⊢ A ∧ B ▻ A
    csnd  : ∀ {A B}            → Γ ⊢ A ∧ B ▻ B
    unit  : Γ ⊢ ⊤

infix 3 _⊢⋆_
_⊢⋆_ : Cx Ty → Cx Ty → Set
Γ ⊢⋆ ∅     = 𝟙
Γ ⊢⋆ Ξ , A = Γ ⊢⋆ Ξ × Γ ⊢ A

infix 7 _▻◅_
_▻◅_ : Ty → Ty → Ty
A ▻◅ B = (A ▻ B) ∧ (B ▻ A)

-- Additional useful propositions.

_⦂⋆_ : ∀ {n} → VCx Box n → VCx Ty n → Cx Ty
∅        ⦂⋆ ∅       = ∅
(ts , t) ⦂⋆ (Ξ , A) = (ts ⦂⋆ Ξ) , (t ⦂ A)

-- Monotonicity with respect to context inclusion.

mono⊢ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
mono⊢ η (var i)   = var (mono∈ η i)
mono⊢ η (app t u) = app (mono⊢ η t) (mono⊢ η u)
mono⊢ η ci        = ci
mono⊢ η ck        = ck
mono⊢ η cs        = cs
mono⊢ η (box t)   = box t
mono⊢ η cdist     = cdist
mono⊢ η cup       = cup
mono⊢ η cdown     = cdown
mono⊢ η cpair     = cpair
mono⊢ η cfst      = cfst
mono⊢ η csnd      = csnd
mono⊢ η unit      = unit

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

-- Shorthand for variables.

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

v₁ : ∀ {A B Γ} → (Γ , A) , B ⊢ A
v₁ = var i₁

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

-- Reflexivity.

refl⊢⋆ : ∀ {Γ} → Γ ⊢⋆ Γ
refl⊢⋆ {∅}     = ∙
refl⊢⋆ {Γ , A} = mono⊢⋆ weak⊆ refl⊢⋆ , v₀

-- Deduction theorem.

lam : ∀ {A B Γ} → Γ , A ⊢ B → Γ ⊢ A ▻ B
lam (var top)     = ci
lam (var (pop i)) = app ck (var i)
lam (app t u)     = app (app cs (lam t)) (lam u)
lam ci            = app ck ci
lam ck            = app ck ck
lam cs            = app ck cs
lam (box t)       = app ck (box t)
lam cdist         = app ck cdist
lam cup           = app ck cup
lam cdown         = app ck cdown
lam cpair         = app ck cpair
lam cfst          = app ck cfst
lam csnd          = app ck csnd
lam unit          = app ck unit

-- Detachment theorem.

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

-- Cut and multicut.

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

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

-- Transitivity.

trans⊢⋆ : ∀ {Γ″ Γ′ Γ} → Γ ⊢⋆ Γ′ → Γ′ ⊢⋆ Γ″ → Γ ⊢⋆ Γ″
trans⊢⋆ {∅}      ts ∙        = ∙
trans⊢⋆ {Γ″ , A} ts (us , u) = trans⊢⋆ ts us , multicut ts u

-- Contraction.

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

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

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

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

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

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

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

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

-- Useful theorems in functional form.

dist : ∀ {A B Γ} {t : ∅ ⊢ A ▻ B} {u : ∅ ⊢ A}
       → Γ ⊢ [ t ] ⦂ (A ▻ B) → Γ ⊢ [ u ] ⦂ A
       → Γ ⊢ [ app t u ] ⦂ B
dist t u = app (app cdist t) u

up : ∀ {A Γ} {t : ∅ ⊢ A}
     → Γ ⊢ [ t ] ⦂ A
     → Γ ⊢ [ box t ] ⦂ [ t ] ⦂ A
up t = app cup t

down : ∀ {A Γ} {t : ∅ ⊢ A}
       → Γ ⊢ [ t ] ⦂ A
       → Γ ⊢ A
down t = app cdown t

distup : ∀ {A B Γ} {u : ∅ ⊢ A} {t : ∅ ⊢ [ u ] ⦂ A ▻ B}
         → Γ ⊢ [ t ] ⦂ ([ u ] ⦂ A ▻ B) → Γ ⊢ [ u ] ⦂ A
         → Γ ⊢ [ app t (box u) ] ⦂ B
distup t u = dist t (up u)

unbox : ∀ {A C Γ} {t : ∅ ⊢ A} {u : ∅ ⊢ C}
        → Γ ⊢ [ t ] ⦂ A → Γ , [ t ] ⦂ A ⊢ [ u ] ⦂ C
        → Γ ⊢ [ u ] ⦂ C
unbox t u = app (lam u) t

-- FIXME ↓ FIXME ↓ FIXME -----------------------------------------------------
--
-- ???

distup′ : ∀ {A B Γ} {u : ∅ ⊢ A} {t : ∅ , [ u ] ⦂ A ⊢ B}
          → Γ ⊢ [ lam t ] ⦂ ([ u ] ⦂ A ▻ B) → Γ ⊢ [ u ] ⦂ A
          → Γ ⊢ [ app (lam t) (box u) ] ⦂ B
distup′ t u = dist t (up u)

-- multibox : ∀ {n A Γ} {[ss] : VCx Box n} {Ξ : VCx Ty n}
--            → Γ ⊢⋆ [ss] ⦂⋆ Ξ → (u : [ss] ⦂⋆ Ξ ⊢ A)
--            → Γ ⊢ {!!} ⦂ A
-- multibox {[ss] = ∅}            {∅}     ∙        u = box u
-- multibox {[ss] = [ss] , [ s ]} {Ξ , B} (ts , t) u = {!!}

-- FIXME ↑ FIXME ↑ FIXME -----------------------------------------------------

pair : ∀ {A B Γ} → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧ B
pair t u = app (app cpair t) u

fst : ∀ {A B Γ} → Γ ⊢ A ∧ B → Γ ⊢ A
fst t = app cfst t

snd : ∀ {A B Γ} → Γ ⊢ A ∧ B → Γ ⊢ B
snd t = app csnd t

-- Closure under context concatenation.

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

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
open import Agda.Builtin.Equality

record Box (B : Set) : Set₁ where
  constructor box
  field
    unbox   : B

-- here: .unbox is a valid forced pattern

=box : {B : Set} {Γ₀ Γ₁ : Box B} → Box.unbox Γ₀ ≡ Box.unbox Γ₁ → Γ₀ ≡ Γ₁
=box {Γ₀ = box unbox} {box r} p = ?

open Box public

-- here: .unbox is now the name of a projection and should therefore
-- not be generated

=box' : {B : Set} {Γ₀ Γ₁ : Box B} → unbox Γ₀ ≡ unbox Γ₁ → Γ₀ ≡ Γ₁
=box' {Γ₀ = box unbox} {box r} p = ?


text:
module UnSized.SimpleCell where

open import Data.Product
open import Data.String.Base

open import UnSizedIO.Object
open import UnSizedIO.IOObject
open import UnSizedIO.ConsoleObject

open import UnSizedIO.Base hiding (main)
open import UnSizedIO.Console hiding (main)

open import NativeIO

data CellMethod A : Set where
    get : CellMethod A
    put : A → CellMethod A

CellResult : ∀{A} → CellMethod A → Set
CellResult {A} get = A
CellResult (put _) = Unit

-- cellI is the interface of the object of a simple cell
cellI : (A : Set) → Interface
Method  (cellI A)    =  CellMethod A
Result  (cellI A) m  =  CellResult m

-- cellC is the type of consoleObjects with interface (cellI String)
CellC : Set
CellC = ConsoleObject (cellI String)

-- cellO is a program for a simple cell which
-- when get is called writes "getting s" for the string s of the object
-- and when putting s writes "putting s" for the string

-- cellP is constructor for the consoleObject for interface (cellI String)
cellP : (s : String) → CellC
force (method (cellP s) get) =
  exec' (putStrLn ("getting (" ++ s ++ ")")) λ _ →
  delay (return' (s , cellP s))
force (method (cellP s) (put x)) =
  exec' (putStrLn ("putting (" ++ x ++ ")")) λ _ →
  delay (return' (_ , (cellP x)))

-- Program is another program

program : String → IOConsole Unit
program arg =
  let c₀ = cellP "Start" in
  method c₀ get       >>= λ{ (s , c₁) →
  exec1 (putStrLn s)         >>
  method c₁ (put arg) >>= λ{ (_ , c₂) →
  method c₂ get       >>= λ{ (s' , c₃) →
  exec1 (putStrLn s')        }}}

main : NativeIO Unit
main = translateIOConsole (program "hello")

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

module PiLevel1Alternative where

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Vec

open import FinVec
open F

open import ConcretePermutation

------------------------------------------------------------------------------
-- Equivalences between permutations
-- Objects are level 0 permutations ⟷
-- Morphisms are equivalences between these permutations

factorial : ℕ → ℕ
factorial 0 = 1
factorial (suc n) = n * factorial n

record EquivBetweenPerm {values : ℕ} {size : ℕ} (p₁ p₂ : CPerm  values size) : Set where
  constructor ebp
  module p₁ = CPerm p₁
  module p₂ = CPerm p₂
  field
    -- first we have a permutation on the underlying finite sets
    π  : FinVec values size
    πᵒ : FinVec size values
    αp : π ∘̂ πᵒ ≡ F.1C
    βp : πᵒ ∘̂ π ≡ F.1C
    -- then we have a permutation on these maps are consistent with p₁.π, p₂.π, etc.
    ππ : Vec (FinVec values size) (factorial size) -- ??? NO
    -- and so on
    -- and apply

{--
Ex: the two underlying permutations p₁ and p₂ are:
    values = {A,B,C}
    size = 3
    p₁.π = { A <=> C, B <=> A, C <=> B } represented as {C,A,B}
    p₂.π = { A <=> C, B <=> A, C <=> B } represented as {C,A,B}

    one equivalence between these permutations is 'id'; another has:
    π = { A <=> B, B <=> C, C <=> A }
    ππ = { (A <=> C) <=> (B <=> A),
           (B <=> A) <=> (C <=> B),
           (C <=> B) <=> (A <=> C) }
       represented as p₁.πᵒ ???
--}

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


text:
module Naturals where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_ ; refl ; cong )
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎ )

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

infixl 6 _+_
_+_ : ℕ → ℕ → ℕ
zero + x = x
(suc a) + x = suc (a + x)

-- Exercise: Write the reasoning chain of 3 + 4
_ : 3 + 4 ≡ 7
_ =
  begin
    3 + 4
  ≡⟨⟩
    suc (2 + 4)
  ≡⟨⟩
    suc (suc (1 + 4))
  ≡⟨⟩
    suc (suc (suc (0 + 4)))
  ≡⟨⟩
    suc (suc (suc 4))
  ≡⟨⟩
    7
  ∎

infixl 7 _*_
_*_ : ℕ → ℕ → ℕ
zero * y = zero
suc x * y = y + (x * y)

_ : 3 * 4 ≡ 12
_ =
  begin
    3 * 4
  ≡⟨⟩
    4 + (2 * 4)
  ≡⟨⟩
    4 + (4 + (1 * 4))
  ≡⟨⟩
    4 + (4 + (4 + (0 * 4)))
  ≡⟨⟩
    4 + (4 + (4 + (0 * 4)))
  ≡⟨⟩
    4 + (4 + (4 + 0))
  ≡⟨⟩
    12
  ∎

_^_ : ℕ → ℕ → ℕ
x ^ zero = 1
x ^ suc y = x * (x ^ y)

-- Kinda like minus, but not exactly
infixl 6 _monus_
_monus_ : ℕ → ℕ → ℕ
zero monus y = zero
suc x monus zero = suc x
suc x monus suc y = x monus y

_ : 5 monus 3 ≡ 2
_ =
  begin
    5 monus 3
  ≡⟨⟩
    4 monus 2
  ≡⟨⟩
    3 monus 1
  ≡⟨⟩
    2 monus 0
  ≡⟨⟩
    2
  ∎

_ : 3 monus 5 ≡ 0
_ =
  begin
    2 monus 4
  ≡⟨⟩
    1 monus 3
  ≡⟨⟩
    0 monus 2
  ≡⟨⟩
    0
  ∎

{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-# BUILTIN NATMINUS _monus_ #-}

data Bin : Set where
  -- Empty bitstring
  ⟨⟩ : Bin
  -- Append a zero
  _O : Bin → Bin
  -- Append a one
  _I : Bin → Bin

inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (b O) = b I
inc (b I) = (inc b) O

to : ℕ → Bin
to zero = ⟨⟩ O
to (suc n) = inc (to n)

from : Bin → ℕ
from ⟨⟩ = zero
from (b O) = from b * 2
from (b I) = from b * 2 + 1

-- I tried to prove these things doing some basic stuff but sadly got nowhere
-- I probably should just read the next chapter! (lol)
--multCommutes : (a : ℕ) → (b : ℕ) → a * b ≡ b * a
--multCommutes zero zero = refl
--multCommutes zero (suc b) = multCommutes zero b
--multCommutes (suc a) zero = multCommutes a zero
--multCommutes (suc a) (suc b) = {! cong (multCommutes a b) !}

--multIsAssociative : (a : ℕ) → (b : ℕ) → (c : ℕ) → (a * b) * c ≡ a * (b * c)
--multIsAssociative zero b c = refl
--multIsAssociative (suc a) zero c = refl
--multIsAssociative (suc a) (suc b) zero = refl
--multIsAssociative (suc a) (suc b) (suc c) = {! multIsAssociative a b c  !}


text:
module OpAppP where

data Bool
  : Set
  where

  false
    : Bool

  true
    : Bool

_&&_
  : Bool
  → Bool
  → Bool
false && _
  = false
true && b
  = b

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
module SizedIO.coIOIOObject where

open import Data.Unit.Base
open import Data.Product
open import Data.String.Base

open import Size

open import SizedIO.Object

open import SizedIO.Base
open import SizedIO.Console
open import SizedIO.coIOIO
-- open import SizedIO.IOObject

record IOObject' (i : Size) (iface : Interface)(C : Set)(R : C → Set) : Set
  where
  coinductive
  field
    method : ∀{j : Size< i} (m : Method iface) →
             IO j C R (Response iface m × IOObject' j iface C R)
open IOObject' public

-- An IO object is like a simple object,
-- but the method returns IO applied to the result type of a simple object
-- which means the method returns an IO program which when terminating
-- returns the result of the simple object
record coIO²Object (i : Size) (iface : Interface)
                (Cin : Set)(Rin : Cin → Set)
                (Cext : Set)(Rext : Cext → Set)     : Set
  where
  coinductive
  field
    method' : ∀{j : Size< i} (m : Method iface) →
             coIO²∞  ∞  Cin Rin Cext Rext
                     (Response iface m × coIO²Object j iface Cin Rin Cext Rext)
open coIO²Object public

selfrefIOObject : (i : Size) (iface : Interface)
                  (Cext : Set) (Rext : Cext → Set) → Set
selfrefIOObject i iface Cext Rext = coIO²Object i iface (Method iface)
                                    (Response iface) Cext Rext

mutual
  compileSelfRef : (i : Size) (iface : Interface)
                   (Cext : Set) (Rext : Cext → Set)
                   (obj : selfrefIOObject i iface Cext Rext) →
                   IOObject' i iface Cext Rext
  IO.force (method (compileSelfRef i iface Cext Rext obj) {i'} m) {j} =
           compileSelfRefaux  i' j iface Cext Rext (Response iface m) (coIO²∞.force (method' obj {i'} m) j)

  compileSelfRefaux :
    (i : Size) (j : Size< i)
    (iface : Interface) (let M = Method iface) (let R = Response iface)
    (Cext : Set) (Rext : Cext → Set)
    (A : Set)
    (coObj : coIO² ∞ j M R Cext Rext (A × coIO²Object i iface M R Cext Rext))
    → IO' j Cext Rext (A × IOObject' i iface Cext Rext)
  compileSelfRefaux i j iface Cext Rext A (coIO².return (r , obj)) = return' (r , compileSelfRef i iface Cext Rext obj)
  compileSelfRefaux i j iface Cext Rext A (dof i' m f) = {! >>=!}
  compileSelfRefaux i j iface Cext Rext A (do∞ c f) =
         do' c (λ r → compileSelfRefaux'' i j iface Cext Rext A (f r))

  compileSelfRefaux'' : (i : Size) (j : Size< i)
    (iface : Interface) (let M = Method iface) (let R = Response iface)
    (Cext : Set) (Rext : Cext → Set)
    (A : Set)
    (coObj : coIO²∞ j M R Cext Rext (A × coIO²Object i iface M R Cext Rext))
      → IO j Cext Rext (A × IOObject' i iface Cext Rext)
  IO.force (compileSelfRefaux'' i j iface Cext Rext A coObj) {j''} = compileSelfRefaux i j'' iface Cext Rext A (coIO²∞.force coObj j'')

--  compileSelfRefaux'' i' j iface Cext Rext A coObj
--           = compileSelfRefaux' i' j iface Cext Rext A (coIO²∞.force coObj {!!})

{-
  compileSelfRefaux' :
    (i' : Size) (j : Size< i')
    (iface : Interface) (let M = Methods iface) (let R = Responses iface)
    (Cext : Set) (Rext : Cext → Set)
    (A : Set)
    (coObj : coIO² ∞ j M R Cext Rext (A × coIO²Object i' iface M R Cext Rext))
    → IO j Cext Rext (A × IOObject' i' iface Cext Rext)
  IO.force (compileSelfRefaux' i' j iface Cext Rext A coObj) = compileSelfRefaux i' j iface Cext Rext A coObj
-}
{-
123;456hallo789
123;456hallo789
123;789hallo456
123;789hallo456
123;789456
123;789456
123;456789
123;456789
123;456789
123;456789

C-x r k    -- kill rectangle
C-x r y    -- yank rectangle
C-x r t    -- text rectangle
-}

{-
M-x abbrev-mode

C-x ail

crosss
→

\
-}

-- method' obj {j'} m

{-
  compileSelfRefaux :  (j' : Size) (iface : Interface)
                       (Cext : Set) (Rext : Cext → Set)
                       (m : Methods iface)
                       ( p : coIO²∞ ∞ (Methods iface)
                                      (Responses iface) Cext Rext
                                      (Responses iface m ×
                                       coIO²Object j' iface (Methods iface)
                                       (Responses iface) Cext Rext))
                       → IO' j' Cext Rext
                         (Responses iface m ×
                          IOObject' j iface Cext Rext)IO' j' Cext Rext
                          (Responses iface m × IOObject' j iface Cext Rext)

  -}


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

module Light.Library.Data.Empty where

open import Light.Level using (Level ; Setω)
open import Light.Variable.Sets

record Dependencies : Setω where

record Library (dependencies : Dependencies) : Setω where
      field
            ℓ : Level
            Empty : Set ℓ
            eliminate : Empty → 𝕒
open Library ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
open import Everything

module Test.Test6 where

module TestReflexivity where

  postulate

    X : Set
    F : X → X → Set
    instance ReflexivityF : Reflexivity.class F

  test : ∀ {y} → F y y
  test {y = y} = reflexivity

  {-
  Goal: F y y
  Have: {𝔬 : Ł} {𝔒 : Set 𝔬} {𝔯 : Ł} {_∼_ : 𝔒 → 𝔒 → Set 𝔯}
        {{r : 𝓡eflexivity {𝔬} {𝔒} {𝔯} _∼_}} {x  : 𝔒} →
        x ∼ x
  ————————————————————————————————————————————————————————————
  y : X

  _𝔬1 : Ł
  _𝔒1 : Set _𝔬1
  _𝔯1 : Ł
  __∼1_ : _𝔒1 → _𝔒1 → Set _𝔯1
  _r1 : 𝓡eflexivity {_𝔬1} {_𝔒1} {_𝔯1} __∼1_
  _x1 : _𝔒1

  __∼1_ _x1 _x1 = F y y

  __∼1_ := λ s t → F s t
  _x1 := y

  __∼1_ := λ s t → F t s
  _x1 := y

  __∼1_ := λ s t → F y y

  λ {𝔬} {𝔒} {𝔯} {_∼_} → 𝓡eflexivity.reflexivity
  -}

module _Indexed where

  record I (M : Set) (N : M → Set) : Set where
    field f : ∀ {m} → N m

  open I ⦃ … ⦄

  postulate
    A : Set
    B : A → Set
    instance iB : I A B

  test : ∀ {a} → B a
  test {a = a} = f

module IndexedTotal1Var where

  record Indexed (M : Set) (N : M → Set) : Set where
    field fooI : ∀ {m} → N m

  open Indexed ⦃ … ⦄

  record Total (N : Set) : Set where
    field fooT : N

  open Total ⦃ … ⦄

  postulate
    A : Set
    B : A → Set
    B' : A → Set
    instance iIndexed : Indexed A B
    instance iTotal : ∀ {x} → Total (B x)
    instance iIndexed' : Indexed A B'
    instance iTotal' : ∀ {x} → Total (B' x)

  testIndexed : ∀ {a} → B a
  testIndexed {a = a} = fooI

  testTotal : ∀ {a} → B a
  testTotal {a = a} = fooT

  {-

  Goal: B a
  Have: {M : Set} {N : M → Set} {{r : R M N}} {m : M} → N m
  ————————————————————————————————————————————————————————————
  a : A

  _M : Set
  _N : _M → Set
  _r : R _M _N
  _m : _M

  _N _m = B a

  no unconstrained metavariables in type of _r because _M occurs in the type of _N and _N _m = B a

  candidate#1
  _r := iR : R A B
  _M = A
  _M := A
  _N = B
  _N := B

  now we can solve for _m:
  _N := B
  _N _m = B a
  B _m = B a
  _m = a
  _m := a

  -}

module Indexed≡Total2Prop where

  open import Oscar.Data.Proposequality

  record Indexed {M : Set} (N : M → Set) (s : ∀ {m} → N m → N m) (S : ∀ {m} → N m → N m → Set) {F : ∀ {m} (n : N m) → Set} ⦃ _ : (λ {m} (n : N m) → S n (s n)) ≡ F ⦄ : Set where
    field fooI : ∀ {m} {n : N m} → S n (s n)

  open Indexed ⦃ … ⦄

  record Total {N : Set} (s : N → N) (S : N → N → Set) : Set where
    field fooT : ∀ n → S n (s n)

  open Total ⦃ … ⦄

  postulate
    A : Set
    B : A → Set
    f : ∀ {x} → B x → B x
    F : ∀ {x} → B x → B x → Set

    instance iIndexed : Indexed B f F ⦃ ∅ ⦄
    instance iTotal : ∀ {x} → Total (f {x}) (F {x})

  testIndexed : ∀ {a} {b : B a} → F b (f b)
  testIndexed = fooI ⦃ ∅ ⦄

  testTotal : ∀ {a} (b : B a) → F b (f b)
  testTotal = fooT {S = F}

module Indexed≡Total1Prop where

  open import Oscar.Data.Proposequality

  record Indexed {M : Set} (N : M → Set) (s : ∀ {m} → N m → N m) (S : ∀ {m} → N m → Set) {F : ∀ {m} (n : N m) → Set} ⦃ _ : (λ {m} (n : N m) → S (s n)) ≡ F ⦄ : Set where
    field fooI : ∀ {m} {n : N m} → S (s n)

  open Indexed ⦃ … ⦄

  record Total {N : Set} (s : N → N) (S : N → Set) : Set where
    field fooT : ∀ n → S (s n)

  open Total ⦃ … ⦄

  postulate
    A : Set
    B : A → Set
    f : ∀ {x} → B x → B x
    F : ∀ {x} → B x → Set

    instance iIndexed : Indexed B f F ⦃ ∅ ⦄
    instance iTotal : ∀ {x} → Total (f {x}) (F {x})

  testIndexed : ∀ {a} {b : B a} → F (f b)
  testIndexed = fooI ⦃ ∅ ⦄

  testTotal : ∀ {a} (b : B a) → F (f b)
  testTotal = fooT {S = F}

module Indexed≡Total1Prop<Constraint where

  open import Oscar.Data.Proposequality

  data Luft {a} {A : Set a} (x : A) : Set where
    instance ∅ : Luft x

  record Indexed {M : Set} (N : M → Set) (s : ∀ {m} → N m → N m) (S : ∀ {m} → N m → Set) ⦃ _ : Luft (λ {m} → s {m}) ⦄ : Set where
    field fooI : ∀ {m} {n : N m} → S (s n)

  open Indexed ⦃ … ⦄

  record Total {N : Set} (s : N → N) (S : N → Set) : Set where
    field fooT : ∀ n → S (s n)

  open Total ⦃ … ⦄

  postulate
    A : Set
    B : A → Set
    f : ∀ {x} → B x → B x
    F : ∀ {x} → B x → Set

    instance iIndexed : Indexed B f F
    instance iTotal : ∀ {x} → Total (f {x}) (F {x})

  testIndexed : ∀ {a} {b : B a} → F (f b)
  testIndexed = fooI ⦃ ∅ ⦄

  testTotal : ∀ {a} (b : B a) → F (f b)
  testTotal = fooT {S = F}

module Indexed≡Total2Prop<Constraint-Multi where

  open import Oscar.Data.Proposequality

  data Luft {a} {A : Set a} (x : A) : Set where
    instance ∅ : Luft x

  record Indexed {M : Set} (N : M → Set) (s : ∀ {m} → N m → N m) (S : ∀ {m} → N m → N m → Set) ⦃ _ : Luft (λ {m} → s {m}) ⦄ : Set where
    field fooI : ∀ {m} {n : N m} → S n (s n)

  open Indexed ⦃ … ⦄

  record Total {N : Set} (s : N → N) (S : N → N → Set) : Set where
    field fooT : ∀ n → S n (s n)

  open Total ⦃ … ⦄

  postulate
    A : Set
    B : A → Set
    f f' : ∀ {x} → B x → B x
    F F' : ∀ {x} → B x → B x → Set

    instance _ : Indexed B f F
    instance _ : Indexed B f' F
    instance _ : Indexed B f F'
    instance _ : Indexed B f' F'
    instance _ : ∀ {x} → Total (f {x}) (F {x})

  testIndexed : ∀ {a} {b : B a} → F b (f b)
  testIndexed = fooI ⦃ ∅ ⦄

  testIndexed2 : ∀ {a} {b : B a} → F (f b) (f (f b))
  testIndexed2 = fooI ⦃ ∅ ⦄

  testTotal : ∀ {a} (b : B a) → F b (f b)
  testTotal = fooT {S = F}

module Indexed≡Total2Prop<Constraint-Multi-2Fun where

  open import Oscar.Data.Proposequality

  data Luft {a} {A : Set a} (x : A) : Set where
    instance ∅ : Luft x

  record Indexed {M : Set} (N : M → Set) (s t : ∀ {m} → N m → N m) (S : ∀ {m} → N m → N m → Set) ⦃ _ : Luft (λ {m} → s {m}) ⦄ ⦃ _ : Luft (λ {m} → t {m}) ⦄ : Set where
    field fooI : ∀ {m} {n : N m} → S (t n) (s n)

  fooI : {M : Set} {N : M → Set} {s t : ∀ {m} → N m → N m} {S : ∀ {m} → N m → N m → Set} ⦃ _ : Indexed N s t S ⦄ → ∀ {m} {n : N m} → S (t n) (s n)
  fooI ⦃ I ⦄ = Indexed.fooI I -- equivalently, fooI = Indexed.fooI ⦃ ∅ ⦄ ⦃ ∅ ⦄ !

  record Total {N : Set} (s t : N → N) (S : N → N → Set) ⦃ _ : Luft s ⦄ ⦃ _ : Luft t ⦄ : Set where
    field fooT : ∀ {n} → S (t n) (s n)

  fooT : {N : Set} {s t : N → N} {S : N → N → Set} ⦃ _ : Total s t S ⦄ → ∀ {n : N} → S (t n) (s n)
  fooT ⦃ I ⦄ = Total.fooT I

  IndexedTotal : {M : Set} (N : M → Set) (s t : ∀ {m} → N m → N m) (S : ∀ {m} → N m → N m → Set) → Set
  IndexedTotal _ s t S = ∀ {x} → Total (s {x}) (t {x}) (S {x})

  postulate
    A : Set
    B : A → Set
    f f' : ∀ {x} → B x → B x
    g g' : ∀ {x} → B x → B x
    F F' : ∀ {x} → B x → B x → Set

    instance _ : Indexed B f f F
    instance _ : Indexed B f' g F
    instance _ : Indexed B f g F'
    instance _ : Indexed B f' g F'
    instance _ : IndexedTotal B f f F
    instance _ : IndexedTotal B f' g F
    instance _ : IndexedTotal B f g F'
    instance _ : IndexedTotal B f' g F'
    instance _ : Indexed B f g F
    -- instance _ : Indexed B (λ b → f (g' b)) (λ b → g (g' b)) F -- this would overlap with the above
    instance _ : ∀ {x} → Total (f {x}) (g {x}) (F {x})

  testIndexed : ∀ {a} {b : B a} → F (g b) (f b)
  testIndexed = fooI

  testIndexed2 : ∀ {a} {b : B a} → F (g (g' b)) (f (g' b))
  testIndexed2 = fooI

  testIndexed3 : ∀ {a} {b : B a} → F (f (g' b)) (f (g' b))
  testIndexed3 = fooI

  testTotal : ∀ {a} {b : B a} → F (g b) (f b)
  testTotal = fooT

module Indexed≡Total2Prop<Constraint-Multi-2Fun-NoIndexedRecord where

  open import Oscar.Data.Proposequality

  data Luft {a} {A : Set a} (x : A) : Set where
    instance ∅ : Luft x

  record Total {N : Set} (s t : N → N) (S : N → N → Set) ⦃ _ : Luft s ⦄ ⦃ _ : Luft t ⦄ : Set where
    field fooT : ∀ {n} → S (t n) (s n)

  fooT : {N : Set} {s t : N → N} {S : N → N → Set} ⦃ _ : Total s t S ⦄ → ∀ {n : N} → S (t n) (s n)
  fooT ⦃ I ⦄ = Total.fooT I

  Indexed : {M : Set} (N : M → Set) (s t : ∀ {m} → N m → N m) (S : ∀ {m} → N m → N m → Set) (x : M) → Set
  Indexed _ s t S x = Total (s {x}) (t {x}) (S {x})

  IndexedTotal : {M : Set} (N : M → Set) (s t : ∀ {m} → N m → N m) (S : ∀ {m} → N m → N m → Set) → Set
  IndexedTotal _ s t S = ∀ {x} → Total (s {x}) (t {x}) (S {x})

  fooI : {M : Set} {N : M → Set} {s t : ∀ {m} → N m → N m} {S : ∀ {m} → N m → N m → Set} ⦃ _ : IndexedTotal N s t S ⦄ → ∀ {m} {n : N m} → S (t n) (s n)
  fooI = fooT

  fooI' : {M : Set} {N : M → Set} → ∀ {m} {s t : N m → N m} {S : N m → N m → Set} ⦃ _ : Total s t S ⦄ → {n : N m} → S (t n) (s n)
  fooI' = fooT

  postulate
    A : Set
    B : A → Set
    f f' : ∀ {x} → B x → B x
    g g' : ∀ {x} → B x → B x
    F F' : ∀ {x} → B x → B x → Set

    instance _ : IndexedTotal B f f F
    instance _ : IndexedTotal B f' g F
    instance _ : IndexedTotal B f g F'
    instance _ : IndexedTotal B f' g F'
    instance _ : IndexedTotal B f g F
    -- instance _ : Indexed B (λ b → f (g' b)) (λ b → g (g' b)) F -- this would overlap with the above
    -- instance _ : ∀ {x} → Total (f {x}) (g {x}) (F {x})

  module _ {a a' : A} (b : B a) (b' : B a') where
    postulate instance _ : Total (g {a'}) f' F
    postulate instance i2 : Indexed B g f' F a
    testTotal' : F (g _) (f _)
    testTotal' = fooT {n = b}
    testTotal'2 : F (f' _) (g _)
    testTotal'2 = fooT {n = b'}
    testTotal'2I : F (f' b') (g _)
    testTotal'2I = fooI {m = a'} -- use fooI when instance given by Total
    testTotal'2I' : F (f' b') (g b')
    testTotal'2I' = fooI' {N = B}
    testTotal'3 : F (f' b) (g b)
    testTotal'3 = fooI {m = a} -- or by Indexed
    testTotal'3' : F (f' b) (g b)
    testTotal'3' = fooI' {N = B}

  testTotalLhs : ∀ {a} {b : B a} → _
  testTotalLhs {a} {b} = fooT {s = f'} {S = F'} {n = b}

  testIndexed : ∀ {a} {b : B a} → F (g b) (f b)
  testIndexed {a} {b} = fooI {S = λ {x} → F {x}} -- use fooI when instance given by IndexedTotal
{-
Have: {M : Set} {N : M → Set} {s t : {m : M} → N m → N m}
      {S : {m : M} → N m → N m → Set}
      {{_ : Indexed {M} N s t S {{∅}} {{∅}}}} {m : M} {n : N m} →
      S {m} (t {m} n) (s {m} n)

Have: {N : Set} {s t : N → N} {S : N → N → Set}
      {{_ : Total {N} s t S {{∅}} {{∅}}}} {n : N} →
      S (t n) (s n)
-}

  testIndexed2 : ∀ {a} {b : B a} → F (g (g' b)) (f (g' b))
  testIndexed2 = fooT

  testIndexed3 : ∀ {a} {b : B a} → F (f (g' b)) (f (g' b))
  testIndexed3 = fooT

  testTotal : ∀ {a} {b : B a} → F (g b) (f b)
  testTotal = fooT

module Indexed≡Total1Prop+Data where

  open import Oscar.Data.Proposequality

  data [_/_/_]≡_ {M : Set} (N : M → Set) (s : ∀ {m} → N m → N m) (S : ∀ {m} → N m → Set) (F : ∀ {m} (n : N m) → Set) : Set where
    instance ∅ : [ N / s / S ]≡ F

  record Indexed {M : Set} (N : M → Set) (s : ∀ {m} → N m → N m) (S : ∀ {m} → N m → Set) ⦃ _ : [ N / s / S ]≡ λ {m} (n : N m) → S (s n) ⦄ : Set where
    field fooI : ∀ {m} {n : N m} → S (s n)

  open Indexed ⦃ … ⦄

  record Total {N : Set} (s : N → N) (S : N → Set) : Set where
    field fooT : ∀ n → S (s n)

  open Total ⦃ … ⦄

  postulate
    A : Set
    B : A → Set
    f : ∀ {x} → B x → B x
    F : ∀ {x} → B x → Set

    instance iIndexed : Indexed B f F ⦃ ∅ ⦄
    instance iTotal : ∀ {x} → Total (f {x}) (F {x})

  testIndexed : ∀ {a} {b : B a} → F (f b)
  testIndexed = fooI ⦃ ∅ ⦄

  testTotal : ∀ {a} (b : B a) → F (f b)
  testTotal = fooT {S = F}

module Indexed≡Total1Prop+Data2 where

  open import Oscar.Data.Proposequality

  data [_/_] {M : Set} (N : M → Set) (s : ∀ {m} → N m → N m) : Set where
    instance ∅ : [ N / s ]

  record Indexed {M : Set} (N : M → Set) (s : ∀ {m} → N m → N m) (S : ∀ {m} → N m → Set) ⦃ _ : [ N / s ] ⦄ : Set where
    field fooI : ∀ {m} {n : N m} → S (s n)

  open Indexed ⦃ … ⦄

  record Total {N : Set} (s : N → N) (S : N → Set) : Set where
    field fooT : ∀ n → S (s n)

  open Total ⦃ … ⦄

  postulate
    A : Set
    B : A → Set
    f : ∀ {x} → B x → B x
    F : ∀ {x} → B x → Set

    instance iIndexed : Indexed B f F ⦃ ∅ ⦄
    instance iTotal : ∀ {x} → Total (f {x}) (F {x})

  testIndexed : ∀ {a} {b : B a} → F (f b)
  testIndexed = fooI ⦃ ∅ ⦄

  testTotal : ∀ {a} (b : B a) → F (f b)
  testTotal = fooT {S = F}


text:
{-# OPTIONS --cubical-compatible --rewriting -v rewriting:50 #-}

open import Agda.Primitive using (Level; _⊔_; Setω; lzero; lsuc)

module Issue4020 where

data _≡_ {ℓ : Level} {A : Set ℓ} (a : A) : A → Set ℓ where
  refl : a ≡ a

{-# BUILTIN REWRITE _≡_ #-}

ap : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {a₁ a₂} → a₁ ≡ a₂ → f a₁ ≡ f a₂
ap f refl = refl

ap-const-Set : ∀ {a b} {A : Set a} {a₁ a₂ : A} (p : a₁ ≡ a₂) → ap (\ _ → Set b) p ≡ refl
ap-const-Set refl = refl

{-# REWRITE ap-const-Set #-}
{- /home/jason/bug.agda:18,1-29
ap-const-Set  is not a legal rewrite rule, since the following variables are not bound by the left hand side:  b
when checking the pragma REWRITE ap-const-Set -}


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

module PComp where

open import Data.Empty
open import Data.Sum
open import Data.Nat as Nat
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties
open import Data.Product
open import Data.Bool renaming (Bool to 𝔹)
open import Data.Bool.Properties
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Relation.Binary
open DecTotalOrder ≤-decTotalOrder using ()
  renaming (refl to ≤-refl; trans to ≤-trans)

-- open import Size

-- record D {i : Size} (A : Set) : Set where
--   coinductive
--   field step : {j : Size< i} → A ⊎ D {j} A

-- open D public

-- μ' : ∀{i} → (ℕ → 𝔹) → ℕ → D {i} ℕ
-- μ' p n .step = if p n then inj₁ n else inj₂ (μ' p (suc n))

primRec : {X Y : Set} → (X → Y) → (ℕ → Y → X → Y) → ℕ → X → Y
primRec f g zero    x = f x
primRec f g (suc n) x = g n (primRec f g n x) x

record D (A : Set) : Set where
  coinductive
  field step : A ⊎ D A

open D public

μ' : (ℕ → 𝔹) → ℕ → D ℕ
c : (ℕ → 𝔹) → ℕ → 𝔹 → ℕ ⊎ (D ℕ)

μ' p n .step = c p n (p n)

c p n false = inj₂ (μ' p (1 + n))
c p n true  = inj₁ n

μ : (ℕ → 𝔹) → D ℕ
μ p = μ' p 0

isEven : ℕ → 𝔹
isEven zero = true
isEven (suc zero) = false
isEven (suc (suc n)) = isEven n

data _↓_ {A : Set} (d : D A) (a : A) : Set where
  now    :                d .step ≡ inj₁ a            → d ↓ a
  later  : {d' : D A} →  d .step ≡ inj₂ d' → d' ↓ a  → d ↓ a

foo : μ' isEven 3 ↓ 4
foo = later (cong inj₂ refl) (now refl)

μ-finds-tt : ∀{p : ℕ → 𝔹} {m n : ℕ} → μ' p m ↓ n → p n ≡ true
μ-finds-tt {p} {m} (now q)        with p m  | inspect p m
μ-finds-tt {p} {m} (now ())        | false  | _
μ-finds-tt {p} {m} (now refl)      | true   | [ eq ]       = eq
μ-finds-tt {p} {m} (later q t)    with p m
μ-finds-tt {p} {m} (later refl t)  | false = μ-finds-tt t
μ-finds-tt {p} {m} (later () t)    | true

-- | Compute the number of steps taken to obtain p n = tt.
μ-dist : ∀{p : ℕ → 𝔹} {m n : ℕ} → μ' p m ↓ n → ∃ λ k → n ≡ m + k
μ-dist {p} {m} (now q)        with p m
μ-dist {p} {m} (now ())        | false
μ-dist {p} {m} (now refl)      | true = (0 , sym (+-identityʳ m))
μ-dist {p} {m} (later q t)    with p m
μ-dist {p} {m} (later refl t)  | false =
  let (k , e) = μ-dist t
  in (1 + k , trans e (sym (+-suc m k)))
μ-dist {p} {m} (later () t)    | true

empty-interval : ∀ {m k} → m ≤ k → k < m → ⊥
empty-interval z≤n      ()
empty-interval (s≤s p)  (s≤s q) = empty-interval p q

suc≤⇒≤ : ∀ m n → suc m ≤ n → m ≤ n
suc≤⇒≤ m         zero            ()
suc≤⇒≤ .0        (suc n)         (s≤s z≤n)      = z≤n
suc≤⇒≤ .(suc _)  (suc .(suc _))  (s≤s (s≤s p))  = s≤s (suc≤⇒≤ _ _ (s≤s p))

-- | The proof proceeds by induction on the termination proof t : μ' p m ↓ n.
-- In the process, we first distinguishing whether m = k or m < k.
-- Next, we check whether the computation has termination, that is, whether
-- t = now ... or t = later.
-- Finally, we distinguish on the values of p m, which allows us to make
-- a computation step with μ'. The other cases follow then from there.
μ-min : ∀{p : ℕ → 𝔹} {m n : ℕ} → μ' p m ↓ n → ∀ k → m ≤′ k → k < n → p k ≡ false
-- m = k
---- t = now
μ-min {p} {.m} (now q)       m ≤′-refl u with p m
μ-min {p} {.m} (now q)       m ≤′-refl u | false = refl
μ-min {p} {.m} (now refl)    m ≤′-refl u | true  = ⊥-elim (1+n≰n u)

-- m = k
---- t = later
μ-min {p} {.m} (later q t)   m ≤′-refl u with p m
μ-min {p} {.m} (later q t)   m ≤′-refl u | false = refl
μ-min {p} {.m} (later () t)  m ≤′-refl u | true

-- m < k
---- t = now
μ-min {p} {m}        (now q)     .(suc _) (≤′-step l) u    with p m
μ-min {p} {m}        (now ())    .(suc _) (≤′-step l) u       | false
μ-min {p} {.(suc _)} (now refl)  .(suc _) (≤′-step l) (s≤s u) | true =
  ⊥-elim (empty-interval (suc≤⇒≤ _ _ (≤′⇒≤ l)) u)

-- m < k
---- t = later
μ-min {p} {m} (later q    t) .(suc _) (≤′-step {k'} l) u with p m
μ-min {p} {m} (later refl t) .(suc _) (≤′-step {k'} l) u    | false =
  μ-min t (suc k') (s≤′s l) u
μ-min {p} {m} (later ()   t) .(suc n) (≤′-step {n} l)  u    | true

Min : (ℕ → Set) → ℕ → Set
Min P n = P n × ∀ k → k < n → ¬ (P k)

-- | Definition of partial correctness for the μ-operator.
-- This states that if μ p terminates with n as result, then n is the
-- minimal number, for which p n ≡ true.
PartialCorrectness : Set
PartialCorrectness = ∀{p : ℕ → 𝔹} {n : ℕ} →
  μ p ↓ n → Min (λ k → p k ≡ true) n

μ-pcorrect : PartialCorrectness
μ-pcorrect t = (μ-finds-tt t , (λ k u → not-¬ (μ-min t k (z≤′n) u)))

-- Correctness : Set
-- Correctness = ∀{p : ℕ → 𝔹} →
--   ¬(∃ λ n → μ p ↓ n) → ∀ n → ¬(p n ≡ true)

-- find-min' : ∀{p : ℕ → 𝔹} → ∀ n → p n ≡ true → (m : ℕ) → m ≤ n →
--             (∃ λ k → k ≤ n × p k ≡ true)
-- find-min' {p} last pt zero l with p 0 | inspect p 0
-- find-min' {p} last pt zero l | false | e = (last , ≤-refl , pt)
-- find-min' {p} last pt zero l | true | [ e ] = (zero , l , e)
-- find-min' {p} last pt (suc m) l with p m | inspect p m
-- find-min' {p} last pt (suc m) l | false | e =
--   find-min' last pt m (suc≤⇒≤ m last l)
-- find-min' {p} last pt (suc m) l | true | [ e ] =
--   let (k , k≤last , q) = find-min' {p} m e m ≤-refl
--   in (k , ≤-trans k≤last (suc≤⇒≤ m last l) , q)

-- find-min : ∀{p : ℕ → 𝔹} → ∀ n → p n ≡ true → (∃ λ k → k ≤ n × p k ≡ true)
-- find-min {p} n pt = find-min' {p} n pt n ≤-refl

-- min-terminate : ∀{p : ℕ → 𝔹} → ∀ n (e : p n ≡ true) (m : ℕ) → m ≤ n → ∃ λ k → μ p ↓ k
-- min-terminate {p} last pt zero m≤n with p 0 | inspect p 0
-- min-terminate {p} last pt zero m≤n | false | e = {!!} , {!!}
-- min-terminate {p} last pt zero m≤n | true | e = {!!}
-- min-terminate {p} last pt (suc m) m≤n = {!!}

-- lem : ∀{p : ℕ → 𝔹} → ∀ n → p n ≡ true → ∃ λ k → μ p ↓ k
-- lem {p} zero q with p 0   | inspect p 0
-- lem {p} zero () | false | _
-- lem {p} zero q | true | [ e ] = (0 , now (cong (c p 0) e))
-- lem {p} (suc n) q with p (suc n)   | inspect p (suc n)
-- lem {p} (suc n) () | false | e
-- lem {p} (suc n) q | true | e =
--   let (k , t) = lem n {!!}
--   in (suc n , now {!!})

-- μ-correct : Correctness
-- μ-correct q n pt = q (lem n pt)

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
{-# BUILTIN NATURAL ℕ #-}
------------------------------------------------------------------------
-- The Integers
--
-- or an extension of the Naturals (see the-naturals.agda)
------------------------------------------------------------------------

module the-integer where

open import Data.Nat as ℕ
  using (ℕ) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
import Data.Nat.Show as ℕ

import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; sym; cong; cong₂)
open PropEq.≡-Reasoning


text:
-- {-# OPTIONS -v tc.lhs.unify.flexflex:100 -v tc.lhs.unify.assign:100 -v tc.lhs:100 #-}
module Multisplit where

postulate
  Level : Set
  lzero : Level
  lsuc  : Level → Level
  _⊔_   : Level → Level → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO lzero #-}
{-# BUILTIN LEVELSUC  lsuc  #-}
{-# BUILTIN LEVELMAX  _⊔_   #-}

data Bool : Set where
  true false : Bool

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

data Fin : ℕ → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

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

data Fin∘suc : ℕ → Set where
  zero : ∀ {n} → Fin∘suc n
  suc  : ∀ {n} → Fin∘suc n → Fin∘suc (suc n)

_==_ : Bool → Bool → Bool
b₁ == b₂ = {!b₁ b₂!}

lookup : ∀ {a n} {A : Set a} → Vec A n → Fin n → A
lookup xs i = {!xs i!}

32-cases : Bool → Bool → Bool → Bool → Bool → Bool
32-cases a b c d e = {!a b c d e!}

No-splits-after-absurd-pattern-encountered :
  (n : ℕ) → Fin n → Fin n → Set
No-splits-after-absurd-pattern-encountered n i j = {!n i j!}

Dotted-patterns-are-not-split : ∀ n → Fin∘suc n → Set
Dotted-patterns-are-not-split n i = {!i n!}

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
{-# OPTIONS -v tc.meta:20  #-}
-- Andreas, 2011-04-15
-- source: Conor's post "foldl Miller magic" on the Agda list (2008)

module Issue325b where

data Nat : Set where
  zero  : Nat
  suc   : Nat -> Nat

data Vec (X : Set) : Nat -> Set where
  [] : Vec X zero
  cons : (n : Nat) -> X -> Vec X n -> Vec X (suc n)

foldl : (S : Set)(T : Nat -> Set) ->
        ((n : Nat) -> T n -> S -> T (suc n)) ->
        T zero ->
        (n : Nat) -> Vec S n -> T n
foldl S T0  f t ._ [] = t
foldl S Tsn f t ._ (cons m s ss) =
  foldl S _ -- (\ n -> Tsn (suc n))
--        (\ n -> f _) (f _ t s) _ ss
           _ (f zero t s) _ ss
--        (\ n -> f (suc n)) (f zero t s) _ ss

{- PROTOCOL:

term _43 S Tsn f t m s ss zero    := suc zero

term _43 S Tsn f t m s ss (suc n) := suc (_43 S Tsn f t m s ss n)

term _43 S Tsn f t m s ss m       := suc m

Pruning could give us:

_43 m zero    := suc zero
_43 m (suc n) := suc (_43 m n)
_43 m m       := suc m

We could then try
a) _43 x y := suc x  failing
b) _43 x y := suc y  succeeding
but this only complete in the absence of recursion.
-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

module Definition.Typed.Consequences.Inversion where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties

open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Substitution
open import Definition.Typed.Consequences.Inequality

open import Tools.Product
open import Tools.Empty using (⊥; ⊥-elim)

-- Inversion of U (it has no type).
inversion-U : ∀ {Γ C} → Γ ⊢ U ∷ C → ⊥
inversion-U (conv x x₁) = inversion-U x

-- Inversion of natural number type.
inversion-ℕ : ∀ {Γ C} → Γ ⊢ ℕ ∷ C → Γ ⊢ C ≡ U
inversion-ℕ (ℕⱼ x) = refl (Uⱼ x)
inversion-ℕ (conv x x₁) = trans (sym x₁) (inversion-ℕ x)

-- Inversion of Empty.
inversion-Empty : ∀ {Γ C} → Γ ⊢ Empty ∷ C → Γ ⊢ C ≡ U
inversion-Empty (Emptyⱼ x) = refl (Uⱼ x)
inversion-Empty (conv x x₁) = trans (sym x₁) (inversion-Empty x)

-- Inversion of Unit.
inversion-Unit : ∀ {Γ C} → Γ ⊢ Unit ∷ C → Γ ⊢ C ≡ U
inversion-Unit (Unitⱼ x) = refl (Uⱼ x)
inversion-Unit (conv x x₁) = trans (sym x₁) (inversion-Unit x)

-- Inversion of Π-types.
inversion-Π : ∀ {F G Γ C}
            → Γ ⊢ Π F ▹ G ∷ C → Γ ⊢ F ∷ U × Γ ∙ F ⊢ G ∷ U × Γ ⊢ C ≡ U
inversion-Π (Πⱼ x ▹ x₁) = x , x₁ , refl (Uⱼ (wfTerm x))
inversion-Π (conv x x₁) = let a , b , c = inversion-Π x
                          in  a , b , trans (sym x₁) c

inversion-Σ : ∀ {F G Γ C}
            → Γ ⊢ Σ F ▹ G ∷ C → Γ ⊢ F ∷ U × Γ ∙ F ⊢ G ∷ U × Γ ⊢ C ≡ U
inversion-Σ (Σⱼ x ▹ x₁) = x , x₁ , refl (Uⱼ (wfTerm x))
inversion-Σ (conv x x₁) = let a , b , c = inversion-Σ x
                          in  a , b , trans (sym x₁) c

-- Inversion of zero.
inversion-zero : ∀ {Γ C} → Γ ⊢ zero ∷ C → Γ ⊢ C ≡ ℕ
inversion-zero (zeroⱼ x) = refl (ℕⱼ x)
inversion-zero (conv x x₁) = trans (sym x₁) (inversion-zero x)

-- Inversion of successor.
inversion-suc : ∀ {Γ t C} → Γ ⊢ suc t ∷ C → Γ ⊢ t ∷ ℕ × Γ ⊢ C ≡ ℕ
inversion-suc (sucⱼ x) = x , refl (ℕⱼ (wfTerm x))
inversion-suc (conv x x₁) =
  let a , b = inversion-suc x
  in  a , trans (sym x₁) b

-- Inversion of natural recursion.
inversion-natrec : ∀ {Γ c g n A C} → Γ ⊢ natrec C c g n ∷ A
  → (Γ ∙ ℕ ⊢ C)
  × Γ ⊢ c ∷ C [ zero ]
  × Γ ⊢ g ∷ Π ℕ ▹ (C ▹▹ C [ suc (var 0) ]↑)
  × Γ ⊢ n ∷ ℕ
  × Γ ⊢ A ≡ C [ n ]
inversion-natrec (natrecⱼ x d d₁ n) = x , d , d₁ , n , refl (substType x n)
inversion-natrec (conv d x) = let a , b , c , d , e = inversion-natrec d
                              in  a , b , c , d , trans (sym x) e

-- Inversion of application.
inversion-app :  ∀ {Γ f a A} → Γ ⊢ (f ∘ a) ∷ A →
  ∃₂ λ F G → Γ ⊢ f ∷ Π F ▹ G × Γ ⊢ a ∷ F × Γ ⊢ A ≡ G [ a ]
inversion-app (d ∘ⱼ d₁) = _ , _ , d , d₁ , refl (substTypeΠ (syntacticTerm d) d₁)
inversion-app (conv d x) = let a , b , c , d , e = inversion-app d
                           in  a , b , c , d , trans (sym x) e

-- Inversion of lambda.
inversion-lam : ∀ {t A Γ} → Γ ⊢ lam t ∷ A →
  ∃₂ λ F G → Γ ⊢ F × (Γ ∙ F ⊢ t ∷ G × Γ ⊢ A ≡ Π F ▹ G)
inversion-lam (lamⱼ x x₁) = _ , _ , x , x₁ , refl (Πⱼ x ▹ (syntacticTerm x₁))
inversion-lam (conv x x₁) = let a , b , c , d , e = inversion-lam x
                            in  a , b , c , d , trans (sym x₁) e

-- Inversion of products.
inversion-prod : ∀ {t u A Γ} → Γ ⊢ prod t u ∷ A →
  ∃₂ λ F G → Γ ⊢ F × (Γ ∙ F ⊢ G × (Γ ⊢ t ∷ F × Γ ⊢ u ∷ G [ t ] × Γ ⊢ A ≡ Σ F ▹ G))
inversion-prod (prodⱼ ⊢F ⊢G ⊢t ⊢u) =
  -- NOTE fundamental theorem not required since prodⱼ has inversion built-in.
  _ , _ , ⊢F , ⊢G , ⊢t , ⊢u , refl (Σⱼ ⊢F ▹ ⊢G )
inversion-prod (conv x x₁) =
  let F , G , a , b , c , d , e = inversion-prod x
  in F , G , a , b , c , d , trans (sym x₁) e

-- Inversion of star.
inversion-star : ∀ {Γ C} → Γ ⊢ star ∷ C → Γ ⊢ C ≡ Unit
inversion-star (starⱼ x) = refl (Unitⱼ x)
inversion-star (conv x x₁) = trans (sym x₁) (inversion-star x)

-- Inversion of products in WHNF.
whnfProduct : ∀ {Γ p F G} → Γ ⊢ p ∷ Σ F ▹ G → Whnf p → Product p
whnfProduct x prodₙ = prodₙ
whnfProduct x (ne pNe) = ne pNe

whnfProduct x Uₙ = ⊥-elim (inversion-U x)
whnfProduct x Πₙ =
  let _ , _ , Σ≡U = inversion-Π x
  in  ⊥-elim (U≢Σ (sym Σ≡U))
whnfProduct x Σₙ =
  let _ , _ , Σ≡U = inversion-Σ x
  in  ⊥-elim (U≢Σ (sym Σ≡U))
whnfProduct x ℕₙ = ⊥-elim (U≢Σ (sym (inversion-ℕ x)))
whnfProduct x Unitₙ = ⊥-elim (U≢Σ (sym (inversion-Unit x)))
whnfProduct x Emptyₙ = ⊥-elim (U≢Σ (sym (inversion-Empty x)))
whnfProduct x lamₙ =
  let _ , _ , _ , _ , Σ≡Π = inversion-lam x
  in  ⊥-elim (Π≢Σ (sym Σ≡Π))
whnfProduct x zeroₙ = ⊥-elim (ℕ≢Σ (sym (inversion-zero x)))
whnfProduct x sucₙ =
  let _ , A≡ℕ = inversion-suc x
  in  ⊥-elim (ℕ≢Σ (sym A≡ℕ))
whnfProduct x starₙ = ⊥-elim (Unit≢Σⱼ (sym (inversion-star x)))