text:
module Pi.Properties where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Pi.Syntax
open import Pi.Opsem
open import Pi.NoRepeat
open import Pi.Invariants
open import Pi.Eval
open import Pi.Interp

-- Forward evaluation is deterministic
deterministic-eval : ∀ {A B} → (c : A ↔ B) (v : ⟦ A ⟧) (v₁ v₂ : ⟦ B ⟧)
                   → ⟨ c ∣ v ∣ ☐ ⟩ ↦* ［ c ∣ v₁ ∣ ☐ ］
                   → ⟨ c ∣ v ∣ ☐ ⟩ ↦* ［ c ∣ v₂ ∣ ☐ ］
                   → v₁ ≡ v₂
deterministic-eval c v v₁ v₂ ↦*₁ ↦*₂ with deterministic* ↦*₁ ↦*₂ (λ ()) (λ ())
... | refl = refl

-- Backward evaluation is deterministic
deterministic-evalᵣₑᵥ : ∀ {A B} → (c : A ↔ B) (v : ⟦ B ⟧) (v₁ v₂ : ⟦ A ⟧)
                      → ［ c ∣ v ∣ ☐ ］ ↦ᵣₑᵥ* ⟨ c ∣ v₁ ∣ ☐ ⟩
                      → ［ c ∣ v ∣ ☐ ］ ↦ᵣₑᵥ* ⟨ c ∣ v₂ ∣ ☐ ⟩
                      → v₁ ≡ v₂
deterministic-evalᵣₑᵥ c v v₁ v₂ ↦ᵣₑᵥ*₁ ↦ᵣₑᵥ*₂ with deterministicᵣₑᵥ* ↦ᵣₑᵥ*₁ ↦ᵣₑᵥ*₂ (λ ()) (λ ())
... | refl = refl

-- Forward evaluator is reversible
evalIsRev : ∀ {A B} → (c : A ↔ B) (v₁ : ⟦ A ⟧) (v₂ : ⟦ B ⟧)
          → eval c v₁ ≡ v₂ → evalᵣₑᵥ c v₂ ≡ v₁
evalIsRev c v₁ v₂ eq with ev {κ = ☐} c v₁
... | v₂' , c↦* with eq
... | refl with evᵣₑᵥ {κ = ☐} c v₂
... | v₁' , c↦*ᵣₑᵥ with deterministicᵣₑᵥ* c↦*ᵣₑᵥ (Rev↦ c↦*) (λ ()) (λ ())
... | refl = refl

-- Backward evaluator is reversible
evalᵣₑᵥIsRev : ∀ {A B} → (c : A ↔ B) (v₁ : ⟦ B ⟧) (v₂ : ⟦ A ⟧)
             → evalᵣₑᵥ c v₁ ≡ v₂ → eval c v₂ ≡ v₁
evalᵣₑᵥIsRev c v₁ v₂ eq with evᵣₑᵥ {κ = ☐} c v₁
... | v₂' , c↦ᵣₑᵥ* with eq
... | refl with ev {κ = ☐} c v₂
... | v₁' , c↦* with deterministic* c↦* (Rev↦ᵣₑᵥ c↦ᵣₑᵥ*) (λ ()) (λ ())
... | refl = refl

-- The abstract machine semantics is equivalent to the big-step semantics
eval≡interp : ∀ {A B} → (c : A ↔ B) → (v : ⟦ A ⟧) → eval c v ≡ interp c v
eval≡interp unite₊l (inj₂ y) = refl
eval≡interp uniti₊l v = refl
eval≡interp swap₊ (inj₁ x) = refl
eval≡interp swap₊ (inj₂ y) = refl
eval≡interp assocl₊ (inj₁ x) = refl
eval≡interp assocl₊ (inj₂ (inj₁ y)) = refl
eval≡interp assocl₊ (inj₂ (inj₂ z)) = refl
eval≡interp assocr₊ (inj₁ (inj₁ x)) = refl
eval≡interp assocr₊ (inj₁ (inj₂ y)) = refl
eval≡interp assocr₊ (inj₂ z) = refl
eval≡interp unite⋆l (tt , v) = refl
eval≡interp uniti⋆l v = refl
eval≡interp swap⋆ (x , y) = refl
eval≡interp assocl⋆ (x , (y , z)) = refl
eval≡interp assocr⋆ ((x , y) , z) = refl
eval≡interp dist (inj₁ x , z) = refl
eval≡interp dist (inj₂ y , z) = refl
eval≡interp factor (inj₁ (x , z)) = refl
eval≡interp factor (inj₂ (y , z)) = refl
eval≡interp id↔ v = refl
eval≡interp (c₁ ⨾ c₂) v with ev {κ = ☐} c₁ v | inspect (ev {κ = ☐} c₁) v
... | (v' , rs)   | [ eq ] with ev {κ = ☐} c₂ v' | inspect (ev {κ = ☐} c₂) v'
... | (v'' , rs') | [ eq' ] with ev {κ = ☐} (c₁ ⨾ c₂) v | inspect (ev {κ = ☐} (c₁ ⨾ c₂)) v
... | (u , rs'')  | [ refl ] rewrite (sym (eval≡interp c₁ v)) | eq | (sym (eval≡interp c₂ v')) | eq' with deterministic* ((↦₃ ∷ ◾) ++↦ appendκ↦* rs refl (☐⨾ c₂ • ☐) ++↦ (↦₇ ∷ ◾) ++↦ appendκ↦* rs' refl (c₁ ⨾☐• ☐) ++↦ (↦₁₀ ∷ ◾)) rs'' (λ ()) (λ ())
... | refl = refl
eval≡interp (c₁ ⊕ c₂) (inj₁ x) with ev {κ = ☐} c₁ x | inspect (ev {κ = ☐} c₁) x
... | (x' , rs) | [ eq ] with ev {κ = ☐} (c₁ ⊕ c₂) (inj₁ x) | inspect (ev {κ = ☐} (c₁ ⊕ c₂)) (inj₁ x)
... | (v , rs') | [ refl ] rewrite (sym (eval≡interp c₁ x)) | eq with deterministic* ((↦₄ ∷ ◾) ++↦ appendκ↦* rs refl (☐⊕ c₂ • ☐) ++↦ (↦₁₁ ∷ ◾)) rs' (λ ()) (λ ())
... | refl = refl
eval≡interp (c₁ ⊕ c₂) (inj₂ y) with ev {κ = ☐} c₂ y | inspect (ev {κ = ☐} c₂) y
... | (x' , rs) | [ eq ] with ev {κ = ☐} (c₁ ⊕ c₂) (inj₂ y) | inspect (ev {κ = ☐} (c₁ ⊕ c₂)) (inj₂ y)
... | (v , rs') | [ refl ] rewrite (sym (eval≡interp c₂ y)) | eq with deterministic* ((↦₅ ∷ ◾) ++↦ appendκ↦* rs refl (c₁ ⊕☐• ☐) ++↦ (↦₁₂ ∷ ◾)) rs' (λ ()) (λ ())
... | refl = refl
eval≡interp (c₁ ⊗ c₂) (x , y) with ev {κ = ☐} c₁ x | inspect (ev {κ = ☐} c₁) x
... | (x' , rs) | [ eq ] with ev {κ = ☐} c₂ y | inspect (ev {κ = ☐} c₂) y
... | (y' , rs') | [ eq' ] with ev {κ = ☐} (c₁ ⊗ c₂) (x , y) | inspect (ev {κ = ☐} (c₁ ⊗ c₂)) (x , y)
... | (_ , rs'') | [ refl ] rewrite (sym (eval≡interp c₁ x)) | eq | (sym (eval≡interp c₂ y)) | eq' with deterministic* (((↦₆ ∷ ◾) ++↦ appendκ↦* rs refl (☐⊗[ c₂ , y ]• ☐)) ++↦ (↦₈ ∷ ◾) ++↦ appendκ↦* rs' refl ([ c₁ , x' ]⊗☐• ☐) ++↦ (↦₉ ∷ ◾)) rs'' (λ ()) (λ ())
... | refl = refl

c⨾!c≡id↔ : ∀ {A B} (c : A ↔ B) → (x : ⟦ A ⟧) → interp (c ⨾ ! c) x ≡ interp id↔ x
c⨾!c≡id↔ unite₊l (inj₂ y) = refl
c⨾!c≡id↔ uniti₊l x = refl
c⨾!c≡id↔ swap₊ (inj₁ x) = refl
c⨾!c≡id↔ swap₊ (inj₂ y) = refl
c⨾!c≡id↔ assocl₊ (inj₁ x) = refl
c⨾!c≡id↔ assocl₊ (inj₂ (inj₁ y)) = refl
c⨾!c≡id↔ assocl₊ (inj₂ (inj₂ z)) = refl
c⨾!c≡id↔ assocr₊ (inj₁ (inj₁ x)) = refl
c⨾!c≡id↔ assocr₊ (inj₁ (inj₂ y)) = refl
c⨾!c≡id↔ assocr₊ (inj₂ z) = refl
c⨾!c≡id↔ unite⋆l (tt , x) = refl
c⨾!c≡id↔ uniti⋆l x = refl
c⨾!c≡id↔ swap⋆ (x , y) = refl
c⨾!c≡id↔ assocl⋆ (x , (y , z)) = refl
c⨾!c≡id↔ assocr⋆ ((x , y) , z) = refl
c⨾!c≡id↔ dist (inj₁ x , z) = refl
c⨾!c≡id↔ dist (inj₂ y , z) = refl
c⨾!c≡id↔ factor (inj₁ (x , z)) = refl
c⨾!c≡id↔ factor (inj₂ (y , z)) = refl
c⨾!c≡id↔ id↔ x = refl
c⨾!c≡id↔ (c₁ ⨾ c₂) x rewrite c⨾!c≡id↔ c₂ (interp c₁ x) = c⨾!c≡id↔ c₁ x
c⨾!c≡id↔ (c₁ ⊕ c₂) (inj₁ x) rewrite c⨾!c≡id↔ c₁ x = refl
c⨾!c≡id↔ (c₁ ⊕ c₂) (inj₂ y) rewrite c⨾!c≡id↔ c₂ y = refl
c⨾!c≡id↔ (c₁ ⊗ c₂) (x , y) rewrite c⨾!c≡id↔ c₁ x | c⨾!c≡id↔ c₂ y = refl

!!c≡c : ∀ {A B} (c : A ↔ B) → ! (! c) ≡ c
!!c≡c unite₊l = refl
!!c≡c uniti₊l = refl
!!c≡c swap₊ = refl
!!c≡c assocl₊ = refl
!!c≡c assocr₊ = refl
!!c≡c unite⋆l = refl
!!c≡c uniti⋆l = refl
!!c≡c swap⋆ = refl
!!c≡c assocl⋆ = refl
!!c≡c assocr⋆ = refl
!!c≡c absorbr = refl
!!c≡c factorzl = refl
!!c≡c dist = refl
!!c≡c factor = refl
!!c≡c id↔ = refl
!!c≡c (c₁ ⨾ c₂) rewrite !!c≡c c₁ | !!c≡c c₂ = refl
!!c≡c (c₁ ⊕ c₂) rewrite !!c≡c c₁ | !!c≡c c₂ = refl
!!c≡c (c₁ ⊗ c₂) rewrite !!c≡c c₁ | !!c≡c c₂ = refl

!c⨾c≡id↔ : ∀ {A B} (c : A ↔ B) → (x : ⟦ B ⟧) → interp (! c ⨾ c) x ≡ interp id↔ x
!c⨾c≡id↔ c x = trans (cong (λ c' → interp c' (interp (! c) x)) (sym (!!c≡c c)))
                    (c⨾!c≡id↔ (! c) x)


text:
module Propositional where

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

open import Holes.Term using (⌞_⌟)
open import Holes.Cong.Propositional

open ≡-Reasoning

--------------------------------------------------------------------------------
--  Some easy lemmas
--------------------------------------------------------------------------------

+-zero : ∀ a → a + zero ≡ a
+-zero zero = refl
+-zero (suc a) rewrite +-zero a = refl

+-suc : ∀ a b → a + suc b ≡ suc (a + b)
+-suc zero b = refl
+-suc (suc a) b rewrite +-suc a b = refl

+-assoc : ∀ a b c → a + b + c ≡ a + (b + c)
+-assoc zero b c = refl
+-assoc (suc a) b c rewrite +-assoc a b c = refl

--------------------------------------------------------------------------------
--  Proofs by equational reasoning
--------------------------------------------------------------------------------

-- commutativity of addition proved traditionally

+-comm₁ : ∀ a b → a + b ≡ b + a
+-comm₁ zero b = sym (+-zero b)
+-comm₁ (suc a) b =
  suc ⌞ a + b ⌟   ≡⟨ cong suc (+-comm₁ a b) ⟩
  suc (b + a)     ≡⟨ sym (+-suc b a) ⟩
  b + suc a       ∎

-- commutativity of addition proved with holes

+-comm : ∀ a b → a + b ≡ b + a
+-comm zero b = sym (+-zero b)
+-comm (suc a) b =
  suc ⌞ a + b ⌟   ≡⟨ cong! (+-comm a b) ⟩
  suc (b + a)     ≡⟨ cong! (+-suc b a) ⟩
  b + suc a       ∎

-- distributivity of multiplication over addition proved traditionally

*-distrib-+₁ : ∀ a b c → a * (b + c) ≡ a * b + a * c
*-distrib-+₁ zero b c = refl
*-distrib-+₁ (suc a) b c =
    b + c + a * (b + c)          ≡⟨ cong (λ h → b + c + h) (*-distrib-+₁ a b c) ⟩
    (b + c) + (a * b + a * c)    ≡⟨ sym (+-assoc (b + c) (a * b) (a * c)) ⟩
    ((b + c) + a * b) + a * c    ≡⟨ cong (λ h → h + a * c) (+-assoc b c (a * b)) ⟩
    (b + (c + a * b)) + a * c    ≡⟨ cong (λ h → (b + h) + a * c) (+-comm c (a * b)) ⟩
    (b + (a * b + c)) + a * c    ≡⟨ cong (λ h → h + a * c) (sym (+-assoc b (a * b) c)) ⟩
    ((b + a * b) + c) + a * c    ≡⟨ +-assoc (b + a * b) c (a * c) ⟩
    (b + a * b) + (c + a * c)
  ∎

-- distributivity of multiplication over addition proved with holes

*-distrib-+ : ∀ a b c → a * (b + c) ≡ a * b + a * c
*-distrib-+ zero b c = refl
*-distrib-+ (suc a) b c =
  b + c + ⌞ a * (b + c) ⌟         ≡⟨ cong! (*-distrib-+ a b c) ⟩
  ⌞ (b + c) + (a * b + a * c) ⌟   ≡⟨ cong! (+-assoc (b + c) (a * b) (a * c)) ⟩
  ⌞ (b + c) + a * b ⌟ + a * c     ≡⟨ cong! (+-assoc b c (a * b)) ⟩
  (b + ⌞ c + a * b ⌟) + a * c     ≡⟨ cong! (+-comm c (a * b)) ⟩
  ⌞ b + (a * b + c) ⌟ + a * c     ≡⟨ cong! (+-assoc b (a * b) c) ⟩
  ⌞ ((b + a * b) + c) + a * c ⌟   ≡⟨ cong! (+-assoc (b + a * b) c (a * c)) ⟩
  (b + a * b) + (c + a * c)
  ∎

ext: agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Printf
------------------------------------------------------------------------

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

module Text.Printf where

open import Level using (0ℓ; Lift)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.Nat.Base using (ℕ)
open import Data.Product
open import Data.Product.Nary.NonDependent
open import Data.String.Base
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Data.Unit using (⊤)
open import Function.Nary.NonDependent
open import Function
open import Strict

import Data.Char.Base as Cₛ
import Data.Integer   as ℤₛ
import Data.Float     as Fₛ
import Data.Nat.Show  as ℕₛ

open import Text.Format as Format hiding (Error)

assemble : ∀ fmt → Product⊤ _ ⟦ fmt ⟧ → List String
assemble []              vs       = []
assemble (`ℕ      ∷ fmt) (n , vs) = ℕₛ.show n  ∷ assemble fmt vs
assemble (`ℤ      ∷ fmt) (z , vs) = ℤₛ.show z  ∷ assemble fmt vs
assemble (`Float  ∷ fmt) (f , vs) = Fₛ.show f  ∷ assemble fmt vs
assemble (`Char   ∷ fmt) (c , vs) = fromChar c ∷ assemble fmt vs
assemble (`String ∷ fmt) (s , vs) = s          ∷ assemble fmt vs
assemble (Raw str ∷ fmt) vs       = str ∷ assemble fmt vs

record Error (e : Format.Error) : Set where

private

  Size : Format.Error ⊎ Format → ℕ
  Size (inj₁ err) = 0
  Size (inj₂ fmt) = size fmt

  Printf : ∀ pr → Set (⨆ (Size pr) 0ℓs)
  Printf (inj₁ err) = Error err
  Printf (inj₂ fmt) = Arrows _ ⟦ fmt ⟧ String

  printf' : ∀ pr → Printf pr
  printf' (inj₁ err) = _
  printf' (inj₂ fmt) = curry⊤ₙ _ (concat ∘′ assemble fmt)

printf : (input : String) → Printf (lexer input)
printf input = printf' (lexer input)


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

module Cubical.Data.Strict2Group.Categorical where

open import Cubical.Foundations.Prelude
open import Cubical.Categories.InternalCategory
open import Cubical.Categories.Groups

{-- Formalization of strict 2-groups as
internal categories of the 1-category Grp
of Groups. --}

Strict2GroupInternalCat : (ℓ : Level) → Type (ℓ-suc ℓ)
Strict2GroupInternalCat ℓ = InternalCategory (1BGROUP ℓ)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{-# OPTIONS --cumulativity #-}

open import Agda.Primitive

-- Defaulting of level metas does not apply to interaction metas, so
-- the type of test₁ should be `Set ?0`, not `Set`.
test₁ : Set {!!}
test₁ = {!!}

postulate
  F : ∀ a (A : Set a) → A → Set

-- In this example, t first argument of F should not default to lzero
-- because it occurs in the type of another meta.
test₂ : F _ _ _
test₂ = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module examplesPaperJFP.loadAllOOAgdaPart1 where

-- This file loads the files containing the code examples in the ooAgda paper
-- ordered by sections
-- The code is divided into files
--    loadAllOOAgdaPart1.agda and loadAllOOAgdaPart2.agda
-- loadAllOOAgdaPart1.agda loads code from Sect. 1 - 7
-- loadAllOOAgdaPart2.agda loads code from Sect. 8 - 12
--
-- The reason for splitting it into  two files is that because of some
--  Builtin the code from the first file cannot be loaded at the same
--  time as the code from the second one.
-- The difference is loading  NativeIOSafe.agda vs NativeIO.agda
--
-- Important changes due to updating it to current agda
-- ####################################################
--      * do is now a keyword and therefore replaced by exec
--      * some other small changes mainly because of changes in the
--           standard library have been made
--
-- Files from the Library
-- #########################
-- loadAllOOAgdaFilesAsInLibrary.agda
-- loads corresponding code from the library which is slightly different
--   from how it is represented in the paper

-- Source of paper, presentations, slides
-- #######################################
--  Andreas Abel, Stephan Adelsberger, Anton Setzer:
--    Interactive Programming in Agda - Objects and Graphical User Interfaces
--    Journal of Functional Programming, 27, 2017
--    doi: http://dx.doi.org/10.1145/2976022.2976032
--    authors copy: http://www.cs.swan.ac.uk/~csetzer/articles/ooAgda.pdf
--    bibtex: http://www.cs.swan.ac.uk/~csetzer/articles/ooAgda.bib

-- 1. Introdution
-- 2. Introduction to Agda

import examplesPaperJFP.finn
import examplesPaperJFP.exampleFinFun
import examplesPaperJFP.Equality

-- 3. Coalgebras in Agda
-- 3.1. Coalgebra by example: Colists

import examplesPaperJFP.Colists
import examplesPaperJFP.Collatz

-- 3.2. Coalgebras in General

import examplesPaperJFP.Coalgebra

-- 4. Interactive Programs in Agda
-- 4.1. Interaction interfaces

import examplesPaperJFP.NativeIOSafe
import examplesPaperJFP.BasicIO
import examplesPaperJFP.triangleRightOperator
import examplesPaperJFP.ConsoleInterface

-- 4.2. Interaction trees

import examplesPaperJFP.Console
import examplesPaperJFP.CatNonTerm
import examplesPaperJFP.CatTerm

-- 4.3. Running interactive programs

import examplesPaperJFP.IOExampleConsole

-- 5. Objects in Agda

-- code as in paper adapted to new Agda
import examplesPaperJFP.Object
-- code as in library see loadAllOOAgdaFilesAsInLibrary.agda
-- open import SizedIO.Object

-- 6. Sized Coinductive Types

import examplesPaperJFP.Sized

-- 7. Interface Extension and Delegation

-- code as in paper adapted to new Agda
import examplesPaperJFP.CounterCell
-- code as in library see loadAllOOAgdaFilesAsInLibrary.agda
-- open import Sized.CounterCell

--  *** Code from Sect 8 - 12 can be found in loadAllOOAgdaPart2.agda ***

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
{-# OPTIONS --without-K --safe #-}
-- verbatim dual of Categories.Category.Construction.Properties.EilenbergMoore
module Categories.Category.Construction.Properties.CoEilenbergMoore where

open import Level
import Relation.Binary.PropositionalEquality.Core as ≡

open import Categories.Adjoint
open import Categories.Adjoint.Properties
open import Categories.Category
open import Categories.Functor using (Functor; _∘F_)
open import Categories.Functor.Equivalence
open import Categories.Comonad

open import Categories.NaturalTransformation.Core renaming (id to idN)
open import Categories.Morphism.HeterogeneousIdentity
open import Categories.Morphism.Reasoning

open import Categories.Adjoint.Construction.CoEilenbergMoore
open import Categories.Category.Construction.CoEilenbergMoore

private
  variable
    o ℓ e : Level
    𝒞 𝒟 : Category o ℓ e

module _ {F : Functor 𝒟 𝒞} {G : Functor 𝒞 𝒟} (F⊣G : Adjoint F G) where
  private
    T : Comonad 𝒞
    T = adjoint⇒comonad F⊣G

    coEM𝒞 : Category _ _ _
    coEM𝒞 = CoEilenbergMoore T

    module 𝒞 = Category 𝒞
    module 𝒟 = Category 𝒟
    module coEM𝒞 = Category coEM𝒞

    open 𝒞.HomReasoning

    module T = Comonad T
    module F = Functor F
    module G = Functor G
    module FG = Functor (F ∘F G)

    open Adjoint F⊣G
    open NaturalTransformation
    open Category.Equiv

  -- Maclane's Comparison Functor
  ComparisonF : Functor 𝒟 coEM𝒞
  ComparisonF = record
   { F₀ = λ X → record
    { A = F.F₀ X
    ; coaction = F.F₁ (unit.η X)
    ; commute = commute-obj
    ; identity = zig
    }
   ; F₁ = λ {A} {B} f → record
    { arr = F.F₁ f
    ; commute = commute-mor
    }
   ; identity = F.identity
   ; homomorphism = F.homomorphism
   ; F-resp-≈ = F.F-resp-≈
   }
   where
    commute-obj : {X : Category.Obj 𝒟} → T.F.F₁ (F.F₁ (unit.η X)) 𝒞.∘ F.F₁ (unit.η X) 𝒞.≈ T.δ.η (F.F₀ X) 𝒞.∘ F.F₁ (unit.η X)
    commute-obj {X} = begin
      F.F₁ (G.F₁ (F.F₁ (unit.η X))) 𝒞.∘ F.F₁ (unit.η X) ≈⟨ sym 𝒞 (F.homomorphism) ⟩
      F.F₁ (G.F₁ (F.F₁ (unit.η X)) 𝒟.∘ unit.η X)        ≈⟨ Functor.F-resp-≈ F (unit.sym-commute (unit.η X)) ⟩
      F.F₁ (unit.η (G.F₀ (F.F₀ X)) 𝒟.∘ unit.η X)        ≈⟨ F.homomorphism ⟩
      T.δ.η (F.F₀ X) 𝒞.∘ F.F₁ (unit.η X)                ∎
    commute-mor : {A B : Category.Obj 𝒟} {f : 𝒟 [ A , B ]} → F.F₁ (unit.η B) 𝒞.∘ F.F₁ f 𝒞.≈ T.F.F₁ (F.F₁ f) 𝒞.∘ F.F₁ (unit.η A)
    commute-mor {A} {B} {f} = begin
     F.F₁ (unit.η B) 𝒞.∘ F.F₁ f          ≈⟨ sym 𝒞 (F.homomorphism) ⟩
     F.F₁ (unit.η B 𝒟.∘ f)               ≈⟨ Functor.F-resp-≈ F (unit.commute f) ⟩
     F.F₁ (G.F₁ (F.F₁ f) 𝒟.∘ unit.η A)   ≈⟨ F.homomorphism ⟩
     T.F.F₁ (F.F₁ f) 𝒞.∘ F.F₁ (unit.η A) ∎

  Comparison∘F≡Free : (ComparisonF ∘F G) ≡F Cofree T
  Comparison∘F≡Free = record
   { eq₀ = λ X → ≡.refl
   ; eq₁ = λ f → id-comm-sym 𝒞
   }

  Forgetful∘ComparisonF≡G : (Forgetful T ∘F ComparisonF) ≡F F
  Forgetful∘ComparisonF≡G = record
   { eq₀ = λ X → ≡.refl
   ; eq₁ = λ f → id-comm-sym 𝒞
   }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
open import Prelude
open import Data.Nat.Properties.Simple
  using (+-comm; +-right-identity; +-assoc)

open import RW.Language.RTerm

open import Relation.Binary.PropositionalEquality
open import RW.Strategy.PropEq

open import RW.RW (≡-strat ∷ [])

module PropEqTransitivityTest where

  open ≡-Reasoning

  -- This is pretty slow...
  test2 : (x y : ℕ) → (x + y) + 0 ≡ y + (x + 0)
  test2 x y
    = begin
      (x + y) + 0
    ≡⟨ (tactic (by*-≡ (quote +-comm ∷ quote +-assoc ∷ []))) ⟩
      y + (x + 0)
    ∎

  {-

  Using a max height of 2 in the goal guesser.

  Finished RWTestingTrans.
  46,981,963,256 bytes allocated in the heap
   7,318,699,728 bytes copied during GC
     387,537,960 bytes maximum residency (20 sample(s))
       8,253,392 bytes maximum slop
            1042 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     90092 colls,     0 par   17.25s   17.25s     0.0002s    0.0030s
  Gen  1        20 colls,     0 par    5.15s    5.17s     0.2587s    0.6522s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  241.64s  (241.88s elapsed)
  GC      time   22.40s  ( 22.42s elapsed)
  EXIT    time    0.09s  (  0.09s elapsed)
  Total   time  264.12s  (264.40s elapsed)

  %GC     time       8.5%  (8.5% elapsed)

  Alloc rate    194,432,035 bytes per MUT second

  Productivity  91.5% of total user, 91.4% of total elapsed

  -}
  {-

  Using a height of 1

  Finished RWTestingTrans.
  31,222,657,544 bytes allocated in the heap
   5,109,928,984 bytes copied during GC
     355,162,768 bytes maximum residency (18 sample(s))
       7,579,240 bytes maximum slop
             952 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     59723 colls,     0 par   12.21s   12.22s     0.0002s    0.0036s
  Gen  1        18 colls,     0 par    3.91s    3.92s     0.2179s    0.6516s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  154.42s  (154.57s elapsed)
  GC      time   16.12s  ( 16.14s elapsed)
  EXIT    time    0.09s  (  0.09s elapsed)
  Total   time  170.63s  (170.80s elapsed)

  %GC     time       9.5%  (9.5% elapsed)

  Alloc rate    202,197,812 bytes per MUT second

  Productivity  90.5% of total user, 90.5% of total elapsed

  -}

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
{-# OPTIONS --type-in-type --no-termination-check
 #-}

module Data where

_-_ : {A : Set}{B : A -> Set}{C : (a : A) -> B a -> Set} ->
      ({a : A}(b : B a) -> C a b) -> (f : (a : A) -> B a) ->
      (a : A) -> C a (f a)
f - g = \ x -> f (g x)

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

konst : {S : Set}{T : S -> Set} -> ({x : S} -> T x) -> (x : S) -> T x
konst c x = c

data Zero : Set where
record One : Set where

record Sig (S : Set)(T : S -> Set) : Set where
  field
    fst : S
    snd : T fst

open module Sig' {S : Set}{T : S -> Set} = Sig {S}{T}

_,_ : forall {S T}(s : S) -> T s -> Sig S T
s , t = record {fst = s; snd = t}

infixr 40 _,_

_*_ : Set -> Set -> Set
S * T = Sig S \ _ -> T

sig : forall {S T}{P : Sig S T -> Set} ->
      ((s : S)(t : T s) -> P (s , t)) -> (st : Sig S T) -> P st
sig f st = f (fst st) (snd st)

data Two : Set where
  tt : Two
  ff : Two

cond : {S : Two -> Set} -> S tt -> S ff -> (b : Two) -> S b
cond t f tt = t
cond t f ff = f

_+_ : Set -> Set -> Set
S + T = Sig Two (cond S T)

[_,_] : {S T : Set}{P : S + T -> Set} ->
        ((s : S) -> P (tt , s)) -> ((t : T) -> P (ff , t)) ->
        (x : S + T) -> P x
[ f , g ] = sig (cond f g)

data PROP : Set where
  Absu : PROP
  Triv : PROP
  _/\_ : PROP -> PROP -> PROP
  All : (S : Set) -> (S -> PROP) -> PROP

Prf : PROP -> Set
Prf Absu = Zero
Prf Triv = One
Prf (P /\ Q) = Prf P * Prf Q
Prf (All S P) = (x : S) -> Prf (P x)

data CON (I : Set) : Set where
  ?? : I -> CON I
  PrfC : PROP -> CON I
  _*C_ : CON I -> CON I -> CON I
  PiC : (S : Set) -> (S -> CON I) -> CON I
  SiC : (S : Set) -> (S -> CON I) -> CON I
  MuC : (O : Set) -> (O -> CON (I + O)) -> O -> CON I
  NuC : (O : Set) -> (O -> CON (I + O)) -> O -> CON I

mutual
  [|_|] : {I : Set} -> CON I -> (I -> Set) -> Set
  [| ?? i |]       X = X i
  [| PrfC P |]     X = Prf P
  [| C *C D |]     X = [| C |] X * [| D |] X
  [| PiC S C |]    X = (s : S) -> [| C s |] X
  [| SiC S C |]    X = Sig S \ s -> [| C s |] X
  [| MuC O C o |]  X = Mu C X o
  [| NuC O C o |]  X = Nu C X o

  data Mu {I O : Set}(C : O -> CON (I + O))(X : I -> Set)(o : O) : Set where
    con : [| C o |] [ X , Mu C X ] -> Mu C X o
  codata Nu {I O : Set}(C : O -> CON (I + O))(X : I -> Set)(o : O) : Set where
    con : [| C o |] [ X , Nu C X ] -> Nu C X o

noc :  {I O : Set}{C : O -> CON (I + O)}{X : I -> Set}{o : O} ->
       Nu C X o -> [| C o |] [ X , Nu C X ]
noc (con xs) = xs

mutual
  map : {I : Set}{X Y : I -> Set} -> (C : CON I) -> ((i : I) -> X i -> Y i) ->
        [| C |] X -> [| C |] Y
  map (?? i)       f = f i
  map (PrfC P)     f = id
  map (C *C D)     f = sig \ c d -> map C f c , map D f d
  map (PiC S C)    f = \ c s -> map (C s) f (c s)
  map (SiC S C)    f = sig \ s c -> s , map (C s) f c
  map (MuC O C o)  f = fold C (Mu C _) (\ o xs -> con (map (C o) [ f , konst id ] xs)) o
  map (NuC O C o)  f = unfold C (Nu C _) (\ o ss -> map (C o) [ f , konst id ] (noc ss)) o

  fold :  {I O : Set}(C : O -> CON (I + O)){X : I -> Set}(Y : O -> Set) ->
          ((o : O) -> [| C o |] [ X , Y ] -> Y o) ->
          (o : O) -> Mu C X o -> Y o
  fold C Y f o (con xs) = f o (map (C o) [ konst id , fold C Y f ] xs)

  unfold :  {I O : Set}(C : O -> CON (I + O)){X : I -> Set}(Y : O -> Set) ->
            ((o : O) -> Y o -> [| C o |] [ X , Y ]) ->
            (o : O) -> Y o -> Nu C X o
  unfold C Y f o y = con (map (C o) [ konst id , unfold C Y f ] (f o y))

induction : {I O : Set}(C : O -> CON (I + O)){X : I -> Set}
            (P : (o : O) -> Mu C X o -> Set) ->
            ((o : O)(xyps : [| C o |] [ X , (\ o -> Sig (Mu C X o) (P o)) ]) ->
             P o (con (map (C o) [ konst id , konst fst ] xyps))) ->
            (o : O)(y : Mu C X o) -> P o y
induction C P p o (con xys) =
  p o (map (C o) [ konst id , (\ o y -> (y , induction C P p o y)) ] xys)

moo : {I O : Set}(C : O -> CON (I + O)){X : I -> Set}(o : O)
      (W : (o : O) -> Mu C X o -> Set)(w : (o : O)(y : Mu C X o) -> W o y)
      (P : (io : I + O) -> [| ?? io |] [ X , Mu C X ] -> Set)
      (io : I + O)(xy : [| ?? io |] [ X , Mu C X ]) -> P io xy ->
      let g : (io : I + O) ->
              [| ?? io |] [ X , Mu C X ] -> [| ?? io |] [ X , (\ o -> Sig (Mu C X o) (W o)) ]
          g = [ konst id , (\ o y -> (y , w o y)) ]
          f : (io : I + O) ->
              [| ?? io |] [ X , (\ o -> Sig (Mu C X o) (W o)) ] -> [| ?? io |] [ X , Mu C X ]
          f = [ konst id , konst fst ]
      in  P io (f io (g io xy))
moo C o W w P io xy p = {!p!}

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram


text:
{- small library for MGS 2021 -}

{- products and sums -}

infix 10 _×_
record _×_ (A B : Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B

open _×_ public

variable
  A B C M : Set

curry : (A × B → C) → (A → B → C)
curry f a b = f (a , b) -- C-c C-,
uncurry : (A → B → C) → (A × B → C)
uncurry f (a , b) = f a b

infix 5 _⊎_
data _⊎_(A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

case : (A → C) → (B → C) → (A ⊎ B → C)
case f g (inj₁ a) = f a
case f g (inj₂ b) = g b

uncase : (A ⊎ B → C) → (A → C) × (B → C)
uncase f = (λ a → f (inj₁ a)) , λ b → f (inj₂ b)

--case' : (A → C) × (B → C) → (A ⊎ B → C)
--case' = uncurry case

record ⊤ : Set where
  constructor tt

open ⊤ public

data ⊥ : Set where

case⊥ : ⊥ → A
case⊥ ()

data Bool : Set where
  true : Bool
  false : Bool

if_then_else_ : Bool → A → A → A
if true then x else y = x
if false then x else y = y

{- bool logic -}

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

{- ∣ = \mid -}

_∣_ : Bool → Bool → Bool
true ∣ y = true
false ∣ y = y

!_ : Bool → Bool
! true = false
! false = true

_⇒b_ : Bool → Bool → Bool
true ⇒b y = y
false ⇒b y = true

{- prop logic -}

prop = Set

variable
  P Q R : prop

infix 3 _∧_
_∧_ : prop → prop → prop
P ∧ Q = P × Q

infix 2 _∨_
_∨_ : prop → prop → prop
P ∨ Q = P ⊎ Q

infixr 1 _⇒_
_⇒_ : prop → prop → prop
P ⇒ Q = P → Q

False : prop
False = ⊥

True : prop
True = ⊤

¬_ : prop → prop
¬ P = P ⇒ False

infix 0 _⇔_
_⇔_ : prop → prop → prop
P ⇔ Q = (P ⇒ Q) ∧ (Q ⇒ P)

efq : False ⇒ P
efq = case⊥

{- classical principles -}

TND : prop → prop
TND P = P ∨ ¬ P

RAA : prop → prop
RAA P = ¬ ¬ P ⇒ P

tnd⇒raa : TND P ⇒ RAA P
tnd⇒raa (inj₁ p) nnp = p
tnd⇒raa (inj₂ np) nnp = efq (nnp np)

nnpnp : ¬ ¬ (P ∨ ¬ P)
nnpnp h = h (inj₂ (λ p → h (inj₁ p)))

raa⇒tnd : RAA (P ∨ ¬ P) ⇒ TND P
raa⇒tnd raa = raa nnpnp

{- natural numbers -}

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

{-# BUILTIN NATURAL ℕ #-}

infixl 6 _+_

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

infixl 7 _*_

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

{- Lists -}

infixr 5 _∷_

data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A -- \::

_++_ : List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

{- Streams -}

record Stream (A : Set) : Set where
  constructor _∷_
  coinductive
  field
    head : A
    tail : Stream A

open Stream public

mapS : (A → B) → Stream A → Stream B
head (mapS f as) = f (head as)
tail (mapS f as) = mapS f (tail as)

{- conatural numbers -}

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A → Maybe A

record ℕ∞ : Set where
  coinductive
  field
    pred∞ : Maybe ℕ∞

open ℕ∞ public

zero∞ : ℕ∞
pred∞ zero∞ = nothing

suc∞ : ℕ∞ → ℕ∞
pred∞ (suc∞ n) = just n

∞ : ℕ∞
pred∞ ∞ = just ∞

_+∞_ : ℕ∞ → ℕ∞ → ℕ∞
pred∞ (m +∞ n) with pred∞ m
... | nothing = pred∞ n
... | just m' = just (m' +∞ n)

{- Vectors and Fin -}

variable i j k m n : ℕ

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

_++v_ : Vec A m → Vec A n → Vec A (m + n)
[] ++v ys = ys
(x ∷ xs) ++v ys = x ∷ (xs ++v ys)

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

_!!v_ : Vec A n → Fin n → A
(x ∷ xs) !!v zero = x
(x ∷ xs) !!v suc i = xs !!v i

max_stars_repo_path: Type Theory/mylib.agda

max_issues_repo_path: Type Theory/mylib.agda

max_forks_repo_path: Type Theory/mylib.agda


text:
{-# OPTIONS --cubical --no-import-sorts #-}

module Number.Prelude.Nat where

open import Cubical.Data.Nat.Order public using () renaming
  ( _<_      to _<ⁿᵗ_
  ; <-trans  to <ⁿ-trans -- TODO: use different version
  ; _≟_      to _≟ⁿ_
  ; lt       to ltⁿ
  ; gt       to gtⁿ
  ; eq       to eqⁿ
  ; ¬-<-zero to ¬-<ⁿ-zero
  )
open import Data.Nat public using () renaming
  ( _⊔_    to maxⁿ
  ; _⊓_    to minⁿ
  ; _+_    to _+ⁿ_
  ; _*_    to _·ⁿ_
  ; pred   to predⁿ
  )
open import Cubical.Data.Nat public using (suc; zero; ℕ; HasFromNat) renaming
  ( +-comm      to +ⁿ-comm
  ; +-assoc     to +ⁿ-assoc
  ; *-comm      to ·ⁿ-comm
  ; *-suc       to ·ⁿ-suc
  ; *-assoc     to ·ⁿ-assoc
  ; +-suc       to +ⁿ-suc
  ; *-distribˡ  to ·ⁿ-distribˡ
  ; *-distribʳ  to ·ⁿ-distribʳ
  ; *-identityʳ to ·ⁿ-identityʳ
  ; *-identityˡ to ·ⁿ-identityˡ
  ; snotz       to snotzⁿ
  ; injSuc      to injSucⁿ
  ; isSetℕ      to is-setⁿ
  ; inj-m+      to +ⁿ-preserves-≡ˡ
  ; inj-+m      to +ⁿ-preserves-≡ʳ
  ; inj-sm*     to ·ⁿ-reflects-≡ˡ'
  ; inj-*sm     to ·ⁿ-reflects-≡ʳ'
  )
open import Number.Instances.Nat as Nat public using () renaming
  ( bundle         to ℕbundle
  ; _<_            to _<ⁿ_
  ; 0<suc          to 0<ⁿsuc
  ; ·-nullifiesˡ   to ·ⁿ-nullifiesˡ
  ; ·-nullifiesʳ   to ·ⁿ-nullifiesʳ
  ; <-irrefl       to <ⁿ-irrefl
  ; suc-creates-<  to sucⁿ-creates-<ⁿ
  ; <-cotrans      to <ⁿ-cotrans
  ; ¬suc<0         to ¬suc<ⁿ0
  ; ·-reflects-<   to ·ⁿ-reflects-<ⁿ
  ; ·-preserves-<  to ·ⁿ-preserves-<ⁿ
  ; +-createsʳ-<   to +ⁿ-createsʳ-<ⁿ
  ; +-createsˡ-<   to +ⁿ-createsˡ-<ⁿ
  ; min-comm       to minⁿ-comm
  ; min-tightˡ     to minⁿ-tightˡ
  ; min-tightʳ     to minⁿ-tightʳ
  ; min-identity   to minⁿ-identity
  ; max-comm       to maxⁿ-comm
  ; max-tightˡ     to maxⁿ-tightˡ
  ; max-tightʳ     to maxⁿ-tightʳ
  ; max-identity   to maxⁿ-identity
  ; MinTrichtotomy to MinTrichtotomyⁿ
  ; MaxTrichtotomy to MaxTrichtotomyⁿ
  ; min-trichotomy to minⁿ-trichotomy
  ; max-trichotomy to maxⁿ-trichotomy
  ; is-min         to is-minⁿ
  ; is-max         to is-maxⁿ
  ; +-<-ext        to +ⁿ-<ⁿ-ext
  ; ·-reflects-≡ʳ  to ·ⁿ-reflects-≡ʳ
  ; ·-reflects-≡ˡ  to ·ⁿ-reflects-≡ˡ
  )

open import MorePropAlgebra.Definitions
open import MorePropAlgebra.Structures
open import Number.Structures2

open IsMonoid            Nat.+-Monoid            public using () renaming (is-identity to +ⁿ-identity)
open IsMonoid            Nat.·-Monoid            public using () renaming (is-identity to ·ⁿ-identity)
open IsSemiring          Nat.is-Semiring         public using () renaming (is-dist     to is-distⁿ)
open IsStrictLinearOrder Nat.<-StrictLinearOrder public using () renaming (is-tricho   to is-trichoⁿ)
-- <-StrictLinearOrder .IsStrictLinearOrder.is-trans  a b c = <-trans {a} {b} {c}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
module _ where

data Bool : Set where
  false true : Bool

{-# COMPILED_DATA Bool Bool False True #-}

postulate
  IO : Set → Set
  return : {A : Set} → A → IO A

{-# COMPILED_TYPE IO IO #-}
{-# COMPILED return \ _ -> return #-}
{-# COMPILED_UHC return \ _ x -> UHC.Agda.Builtins.primReturn x #-}
{-# COMPILED_JS return function(u) { return function(x) { return function(cb) { cb(x); }; }; } #-}

{-# IMPORT Data.Maybe #-}

{-# HASKELL printMaybe = putStrLn . Data.Maybe.fromMaybe "" #-}

returnTrue : IO Bool
returnTrue = return true

{-# COMPILED_EXPORT  returnTrue returnTrue #-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
open import Nat
open import Prelude
open import List

open import contexts
open import core

open import lemmas-env
open import lemmas-progress
open import decidability
open import results-checks

-- TODO we're forced to prove this weaker version, since the strong version is
--      unprovable. That said, this weak version is still disappointing, so we
--      should come up with some more thoerems to shore up its deficiencies -
--      in particular, we should do something to mitigate the fact that an e
--      may succeed for every even n and fail for every odd n
--      - also, that evaluation may return different results for different n
-- TODO complete, then delete
--      e => r → ∀{n} e [n]=> r
--        something similar for =>∅ ?
--      (Σ[r] (e => r) ∧ e => ∅) → ⊥
--      ∀{k} → Σ[r] (e [k]=> r) ∨ e [k]=> ∅
module progress where
  progress : ∀{Δ Σ' Γ E e τ n} →
               Δ , Σ' , Γ ⊢ E →
               Δ , Σ' , Γ ⊢ e :: τ →
               -- Either there's some properly-typed result that e will eval to ...
               Σ[ r ∈ result ] Σ[ k ∈ constraints ] (
                  (E ⊢ e ⌊ ⛽⟨ n ⟩ ⌋⇒ r ⊣ k) ∧
                  Δ , Σ' ⊢ r ·: τ)
               -- ... or evaluation will have a constraint failure
               ∨ E ⊢ e ⌊ ⛽⟨ n ⟩ ⌋⇒∅

  xc-progress : ∀{Δ Σ' r1 r2 τ n} →
                  Δ , Σ' ⊢ r1 ·: τ →
                  Δ , Σ' ⊢ r2 ·: τ →
                  Σ[ k ∈ constraints ] Constraints⦃ r1 , r2 ⦄⌊ ⛽⟨ n ⟩ ⌋:= k
                  ∨ Constraints⦃ r1 , r2 ⦄⌊ ⛽⟨ n ⟩ ⌋:=∅

  xb-progress : ∀{Δ Σ' r ex τ n} →
                  Δ , Σ' ⊢ r ·: τ →
                  Δ , Σ' ⊢ ex :· τ →
                  Σ[ k ∈ constraints ] (r ⇐ ex ⌊ ⛽⟨ n ⟩ ⌋:= k)
                  ∨ r ⇐ ex ⌊ ⛽⟨ n ⟩ ⌋:=∅

  rule-fails : {n↓ : Nat} {E : env} {r : result} {ex : ex} → Set
  rule-fails {n↓} {E} {r} {ex} =
              Σ[ c-j ∈ Nat ] Σ[ x-j ∈ Nat ] Σ[ e-j ∈ exp ] (
                 r ⇐ C[ c-j ] ¿¿ ⌊ ⛽⟨ 1+ n↓ ⟩ ⌋:=∅
                 ∨ Σ[ k1 ∈ constraints ] (
                      r ⇐ C[ c-j ] ¿¿ ⌊ ⛽⟨ 1+ n↓ ⟩ ⌋:= k1 ∧ (E ,, (x-j , C⁻[ c-j ] r)) ⊢ e-j ⌊ ⛽⟨ n↓ ⟩ ⌋⇒∅)
                 ∨ Σ[ k1 ∈ constraints ] Σ[ k2 ∈ constraints ] Σ[ r-j ∈ result ] (
                      r ⇐ C[ c-j ] ¿¿ ⌊ ⛽⟨ 1+ n↓ ⟩ ⌋:= k1 ∧ (E ,, (x-j , C⁻[ c-j ] r)) ⊢ e-j ⌊ ⛽⟨ n↓ ⟩ ⌋⇒ r-j ⊣ k2 ∧ r-j ⇐ ex ⌊ ⛽⟨ n↓ ⟩ ⌋:=∅))

  lemma-xb-progress-case : ∀{Δ Σ' E r rules ex τ n n↓} →
                             (n == 1+ n↓) →
                             (len : Nat) →
                             (unchecked : rule ctx) →
                             len == ∥ unchecked ∥ →
                             (failed : (rule-fails {n↓} {E} {r} {ex}) ctx) →
                             (∀{c rule} → (c , rule) ∈ unchecked → (c , rule) ∈ rules) →
                             (∀{c c-j x-j e-j p-j} →
                                (c , c-j , x-j , e-j , p-j) ∈ failed →
                                c == c-j ∧ (c , |C x-j => e-j) ∈ rules) →
                             (∀{c} → dom rules c → dom unchecked c ∨ dom failed c) →
                             Δ , Σ' ⊢ [ E ]case r of⦃· rules ·⦄ ·: τ →
                             Δ , Σ' ⊢ ex :· τ →
                             ex ≠ ¿¿ →
                             Σ[ k ∈ constraints ] ([ E ]case r of⦃· rules ·⦄ ⇐ ex ⌊ ⛽⟨ n ⟩ ⌋:= k)
                             ∨ [ E ]case r of⦃· rules ·⦄ ⇐ ex ⌊ ⛽⟨ n ⟩ ⌋:=∅

  progress {n = Z} Γ⊢E ta
    = Inl (_ , _ , ELimit , π2 (typ-inhabitance-pres Γ⊢E ta))
  progress {n = 1+ n} Γ⊢E ta'@(TAFix ta) = Inl (_ , _ , EFix , TAFix Γ⊢E ta')
  progress {n = 1+ n} Γ⊢E (TAVar x∈Γ)
    with env-all-Γ Γ⊢E x∈Γ
  ... | _ , x∈E , ta = Inl (_ , _ , EVar x∈E , ta)
  progress {n = 1+ n} Γ⊢E (TAApp _ ta-f ta-arg)
    with progress Γ⊢E ta-arg
  ... | Inr arg-fails = Inr (EFAppArg arg-fails)
  ... | Inl (rarg , _ , arg-evals , ta-rarg)
    with progress Γ⊢E ta-f
  ... | Inr f-fails = Inr (EFAppFun f-fails)
  progress {n = 1+ n} Γ⊢E (TAApp _ ta-f ta-arg) | Inl (rarg , _ , arg-evals , ta-rarg) | Inl ([ E' ]fix f ⦇·λ x => ef ·⦈ , _ , f-evals , ta'@(TAFix Γ'⊢E' (TAFix ta-ef)))
    with progress {n = n} (EnvInd (EnvInd Γ'⊢E' ta') ta-rarg) ta-ef
  ... | Inr ef-fails = Inr (EFAppFixEval CF⛽ refl f-evals arg-evals ef-fails)
  ... | Inl (ref , _ , ef-evals , ta-ref) = Inl (_ , _ , EAppFix CF⛽ refl f-evals arg-evals ef-evals , ta-ref)
  progress {n = 1+ n} Γ⊢E (TAApp _ ta-f ta-arg) | Inl (rarg , _ , arg-evals , ta-rarg) | Inl ([ E' ]??[ u ] , _ , f-evals , ta-rf)
    = Inl (_ , _ , EAppUnfinished f-evals (λ ()) arg-evals , TAApp ta-rf ta-rarg)
  progress {n = 1+ n} Γ⊢E (TAApp _ ta-f ta-arg) | Inl (rarg , _ , arg-evals , ta-rarg) | Inl ((rf-f ∘ rf-arg) , _ , f-evals , ta-rf)
    = Inl (_ , _ , EAppUnfinished f-evals (λ ()) arg-evals , TAApp ta-rf ta-rarg)
  progress {n = 1+ n} Γ⊢E (TAApp _ ta-f ta-arg) | Inl (rarg , _ , arg-evals , ta-rarg) | Inl (fst _ , _ , f-evals , ta-rf)
    = Inl (_ , _ , EAppUnfinished f-evals (λ ()) arg-evals , TAApp ta-rf ta-rarg)
  progress {n = 1+ n} Γ⊢E (TAApp _ ta-f ta-arg) | Inl (rarg , _ , arg-evals , ta-rarg) | Inl (snd _ , _ , f-evals , ta-rf)
    = Inl (_ , _ , EAppUnfinished f-evals (λ ()) arg-evals , TAApp ta-rf ta-rarg)
  progress {n = 1+ n} Γ⊢E (TAApp _ ta-f ta-arg) | Inl (rarg , _ , arg-evals , ta-rarg) | Inl ([ E' ]case rf of⦃· rules ·⦄ , _ , f-evals , ta-rf)
    = Inl (_ , _ , EAppUnfinished f-evals (λ ()) arg-evals , TAApp ta-rf ta-rarg)
  progress {n = 1+ n} Γ⊢E (TAApp _ ta-f ta-arg) | Inl (rarg , _ , arg-evals , ta-rarg) | Inl ((C⁻[ _ ] _) , _ , f-evals , ta-rf)
    = Inl (_ , _ , EAppUnfinished f-evals (λ ()) arg-evals , TAApp ta-rf ta-rarg)
  progress {n = 1+ n} Γ⊢E TAUnit = Inl (_ , _ , EUnit , TAUnit)
  progress {n = 1+ n} Γ⊢E (TAPair _ ta1 ta2)
    with progress Γ⊢E ta1
  ... | Inr fails                    = Inr (EFPair1 fails)
  ... | Inl (_ , _ , evals1 , ta-r1)
    with progress Γ⊢E ta2
  ... | Inr fails                    = Inr (EFPair2 fails)
  ... | Inl (_ , _ , evals2 , ta-r2) = Inl (_ , _ , EPair evals1 evals2 , TAPair ta-r1 ta-r2)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TAFst ta)
    with progress Γ⊢E ta
  ... | Inr fails = Inr (EFFst fails)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TAFst ta) | Inl (⟨ r1 , r2 ⟩ , _ , evals , TAPair ta-r1 ta-r2)
    = Inl (_ , _ , EFst evals , ta-r1)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TAFst ta) | Inl ([ x ]fix x₁ ⦇·λ x₂ => x₃ ·⦈ , _ , evals , TAFix _ ())
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TAFst ta) | Inl ((C⁻[ x ] q) , _ , evals , ta-r)
    = Inl (_ , _ , EFstUnfinished evals (λ ()) , TAFst ta-r)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TAFst ta) | Inl ([ x ]??[ x₁ ] , _ , evals , ta-r)
    = Inl (_ , _ , EFstUnfinished evals (λ ()) , TAFst ta-r)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TAFst ta) | Inl ((q ∘ q₁) , _ , evals , ta-r)
    = Inl (_ , _ , EFstUnfinished evals (λ ()) , TAFst ta-r)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TAFst ta) | Inl (fst q , _ , evals , ta-r)
    = Inl (_ , _ , EFstUnfinished evals (λ ()) , TAFst ta-r)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TAFst ta) | Inl (snd q , _ , evals , ta-r)
    = Inl (_ , _ , EFstUnfinished evals (λ ()) , TAFst ta-r)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TAFst ta) | Inl ([ x ]case q of⦃· x₁ ·⦄ , _ , evals , ta-r)
    = Inl (_ , _ , EFstUnfinished evals (λ ()) , TAFst ta-r)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TASnd ta)
    with progress Γ⊢E ta
  ... | Inr fails = Inr (EFSnd fails)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TASnd ta) | Inl (⟨ r1 , r2 ⟩ , _ , evals , TAPair ta-r1 ta-r2)
    = Inl (_ , _ , ESnd evals , ta-r2)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TASnd ta) | Inl ([ x ]fix x₁ ⦇·λ x₂ => x₃ ·⦈ , _ , evals , TAFix _ ())
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TASnd ta) | Inl ((C⁻[ x ] q) , _ , evals , ta-r)
    = Inl (_ , _ , ESndUnfinished evals (λ ()) , TASnd ta-r)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TASnd ta) | Inl ([ x ]??[ x₁ ] , _ , evals , ta-r)
    = Inl (_ , _ , ESndUnfinished evals (λ ()) , TASnd ta-r)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TASnd ta) | Inl ((q ∘ q₁) , _ , evals , ta-r)
    = Inl (_ , _ , ESndUnfinished evals (λ ()) , TASnd ta-r)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TASnd ta) | Inl (fst q , _ , evals , ta-r)
    = Inl (_ , _ , ESndUnfinished evals (λ ()) , TASnd ta-r)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TASnd ta) | Inl (snd q , _ , evals , ta-r)
    = Inl (_ , _ , ESndUnfinished evals (λ ()) , TASnd ta-r)
  progress {Δ} {Σ'} {E = E} {τ = τ} {1+ n} Γ⊢E (TASnd ta) | Inl ([ x ]case q of⦃· x₁ ·⦄ , _ , evals , ta-r)
    = Inl (_ , _ , ESndUnfinished evals (λ ()) , TASnd ta-r)
  progress {n = 1+ n} Γ⊢E (TACtor d∈Σ' c∈d ta)
    with progress Γ⊢E ta
  ... | Inr e-fails = Inr (EFCtor e-fails)
  ... | Inl (_ , _ , e-evals , ta-r) = Inl (_ , _ , ECtor e-evals , TACtor d∈Σ' c∈d ta-r)
  progress {Σ' = Σ'} {n = 1+ n} Γ⊢E (TACase d∈σ' e-ta cctx⊆rules h-rules)
    with progress Γ⊢E e-ta
  ... | Inr e-fails = Inr (EFMatchScrut e-fails)
  ... | Inl ([ x ]fix x₁ ⦇·λ x₂ => x₃ ·⦈ , _ , e-evals , TAFix _ ())
  ... | Inl ([ x ]??[ x₁ ] , _ , e-evals , ta-re)
          = Inl (_ , _ , EMatchUnfinished e-evals (λ ()) , TACase d∈σ' Γ⊢E ta-re cctx⊆rules (λ form →
                 let _ , _ , _ , c∈cctx , ec-ta = h-rules form in
                 _ , c∈cctx , ec-ta))
  ... | Inl ((re ∘ re₁) , _ , e-evals , ta-re)
          = Inl (_ , _ , EMatchUnfinished e-evals (λ ()) , TACase d∈σ' Γ⊢E ta-re cctx⊆rules (λ form →
                 let _ , _ , _ , c∈cctx , ec-ta = h-rules form in
                 _ , c∈cctx , ec-ta))
  ... | Inl (fst _ , _ , e-evals , ta-re)
          = Inl (_ , _ , EMatchUnfinished e-evals (λ ()) , TACase d∈σ' Γ⊢E ta-re cctx⊆rules (λ form →
                 let _ , _ , _ , c∈cctx , ec-ta = h-rules form in
                 _ , c∈cctx , ec-ta))
  ... | Inl (snd _ , _ , e-evals , ta-re)
          = Inl (_ , _ , EMatchUnfinished e-evals (λ ()) , TACase d∈σ' Γ⊢E ta-re cctx⊆rules (λ form →
                 let _ , _ , _ , c∈cctx , ec-ta = h-rules form in
                 _ , c∈cctx , ec-ta))
  ... | Inl ([ x ]case re of⦃· x₁ ·⦄ , _ , e-evals , ta-re)
          = Inl (_ , _ , EMatchUnfinished e-evals (λ ()) , TACase d∈σ' Γ⊢E ta-re cctx⊆rules (λ form →
                 let _ , _ , _ , c∈cctx , ec-ta = h-rules form in
                 _ , c∈cctx , ec-ta))
  ... | Inl ((C⁻[ _ ] _) , _ , e-evals , ta-re)
          = Inl (_ , _ , EMatchUnfinished e-evals (λ ()) , TACase d∈σ' Γ⊢E ta-re cctx⊆rules (λ form →
                 let _ , _ , _ , c∈cctx , ec-ta = h-rules form in
                 _ , c∈cctx , ec-ta))
  ... | Inl ((C[ c ] re) , _ , e-evals , TACtor d∈'σ' c∈cctx' ta-re)
    rewrite ctxunicity d∈'σ' d∈σ'
    with π2 (cctx⊆rules (_ , c∈cctx'))
  ... | form
    with h-rules form
  ... | _ , _ , _ , c∈cctx , ec-ta
    rewrite ctxunicity c∈cctx c∈cctx'
    with progress {n = n} (EnvInd Γ⊢E ta-re) ec-ta
  ... | Inr ec-fails = Inr (EFMatchRule CF⛽ form e-evals ec-fails)
  ... | Inl (_ , _ , ec-evals , ta-rec) = Inl (_ , _ , EMatch CF⛽ form e-evals ec-evals , ta-rec)
  progress {n = 1+ n} Γ⊢E (TAHole u∈Δ) = Inl (_ , _ , EHole , TAHole u∈Δ Γ⊢E)
  progress {n = 1+ n} Γ⊢E (TAAsrt _ ta1 ta2)
    with progress Γ⊢E ta1
  ... | Inr e1-fails = Inr (EFAsrtL e1-fails)
  ... | Inl (r1 , _ , e1-evals , ta-r1)
    with progress Γ⊢E ta2
  ... | Inr e2-fails = Inr (EFAsrtR e2-fails)
  ... | Inl (r2 , _ , e2-evals , ta-r2)
    with xc-progress ta-r1 ta-r2
  ... | Inl (_ , c-succ) = Inl (_ , _ , EAsrt e1-evals e2-evals c-succ , TAUnit)
  ... | Inr c-fail       = Inr (EFAsrt e1-evals e2-evals c-fail)

  lemma-xc-no-coerce : ∀{Δ Σ' r1 r2 τ n} →
                         Δ , Σ' ⊢ r1 ·: τ →
                         Δ , Σ' ⊢ r2 ·: τ →
                         r1 ≠ r2 →
                         (∀{ex} → Coerce r1 := ex → ⊥) →
                         r1 ≠ ⟨⟩ →
                         (∀{r'1 r'2} → r1 ≠ ⟨ r'1 , r'2 ⟩) →
                         (∀{c r} → r1 ≠ (C[ c ] r)) →
                         Σ[ k ∈ constraints ] Constraints⦃ r1 , r2 ⦄⌊ ⛽⟨ n ⟩ ⌋:= k
                         ∨ Constraints⦃ r1 , r2 ⦄⌊ ⛽⟨ n ⟩ ⌋:=∅
  lemma-xc-no-coerce ta1 (TAFix x x₁) r1≠r2 no-coerce not-unit not-pair not-ctor
    = Inr (XCFNoCoerce r1≠r2 (Inl not-pair) (Inl not-ctor) no-coerce λ ())
  lemma-xc-no-coerce ta1 (TAApp ta2 ta3) r1≠r2 no-coerce not-unit not-pair not-ctor
    = Inr (XCFNoCoerce r1≠r2 (Inl not-pair) (Inl not-ctor) no-coerce λ ())
  lemma-xc-no-coerce ta1 TAUnit r1≠r2 no-coerce not-unit not-pair not-ctor
    with xb-progress ta1 TAUnit
  ...  | Inl (_ , xb) = Inl (_ , (XCBackProp1 r1≠r2 (Inl not-pair) (Inl not-ctor) CoerceUnit xb))
  ...  | Inr xb-fails = Inr (XCFXB1 r1≠r2 (Inl not-pair) (Inl not-ctor) CoerceUnit xb-fails)
  lemma-xc-no-coerce ta1 ta2@(TAPair _ _) r1≠r2 no-coerce not-unit not-pair not-ctor
    with Coerce-dec
  ...  | Inr nc         = Inr (XCFNoCoerce r1≠r2 (Inl not-pair) (Inl not-ctor) no-coerce λ {c-r2 → nc (_ , c-r2)})
  ...  | Inl (_ , c-r2)
    with xb-progress ta1 (Coerce-preservation ta2 c-r2)
  ...  | Inr xb-fails   = Inr (XCFXB1 r1≠r2 (Inl not-pair) (Inl not-ctor) c-r2 xb-fails)
  ...  | Inl (_ , xb)   = Inl (_ , (XCBackProp1 r1≠r2 (Inl not-pair) (Inl not-ctor) c-r2 xb))
  lemma-xc-no-coerce ta1 (TAFst ta2) r1≠r2 no-coerce not-unit not-pair not-ctor
    = Inr (XCFNoCoerce r1≠r2 (Inl not-pair) (Inl not-ctor) no-coerce λ ())
  lemma-xc-no-coerce ta1 (TASnd ta2) r1≠r2 no-coerce not-unit not-pair not-ctor
    = Inr (XCFNoCoerce r1≠r2 (Inl not-pair) (Inl not-ctor) no-coerce λ ())
  lemma-xc-no-coerce ta1 ta2@(TACtor _ _ _) r1≠r2 no-coerce not-unit not-pair not-ctor
    with Coerce-dec
  ...  | Inr nc         = Inr (XCFNoCoerce r1≠r2 (Inl not-pair) (Inl not-ctor) no-coerce λ {c-r2 → nc (_ , c-r2)})
  ...  | Inl (_ , c-r2)
    with xb-progress ta1 (Coerce-preservation ta2 c-r2)
  ...  | Inr xb-fails   = Inr (XCFXB1 r1≠r2 (Inl not-pair) (Inl not-ctor) c-r2 xb-fails)
  ...  | Inl (_ , xb)   = Inl (_ , (XCBackProp1 r1≠r2 (Inl not-pair) (Inl not-ctor) c-r2 xb))
  lemma-xc-no-coerce ta1 (TAUnwrapCtor x x₁ ta2) r1≠r2 no-coerce not-unit not-pair not-ctor
    = Inr (XCFNoCoerce r1≠r2 (Inl not-pair) (Inl not-ctor) no-coerce λ ())
  lemma-xc-no-coerce ta1 (TACase x x₁ ta2 x₂ x₃) r1≠r2 no-coerce not-unit not-pair not-ctor
    = Inr (XCFNoCoerce r1≠r2 (Inl not-pair) (Inl not-ctor) no-coerce λ ())
  lemma-xc-no-coerce ta1 (TAHole x x₁) r1≠r2 no-coerce not-unit not-pair not-ctor
    = Inr (XCFNoCoerce r1≠r2 (Inl not-pair) (Inl not-ctor) no-coerce λ ())

  xc-progress {r1 = r1} {r2} ta1 ta2
    with result-==-dec r1 r2
  ... | Inl refl = Inl (_ , XCExRefl)
  xc-progress {r1 = _} {_} ta1@(TAFix x x₁) ta2 | Inr r1≠r2
    = lemma-xc-no-coerce ta1 ta2 r1≠r2 (λ ()) (λ ()) (λ ()) λ ()
  xc-progress {r1 = _} {_} ta1@(TAApp _ _) ta2 | Inr r1≠r2
    = lemma-xc-no-coerce ta1 ta2 r1≠r2 (λ ()) (λ ()) (λ ()) λ ()
  xc-progress {r1 = _} {_} TAUnit ta2 | Inr r1≠r2
    with xb-progress ta2 TAUnit
  ...  | Inl (_ , xb) = Inl (_ , (XCBackProp2 r1≠r2 (Inl (λ ())) (Inl (λ ())) CoerceUnit xb))
  ...  | Inr xb-fails = Inr (XCFXB2 r1≠r2 (Inl (λ ())) (Inl (λ ())) CoerceUnit xb-fails)
  xc-progress (TAPair ta1a ta1b) (TAPair ta2a ta2b) | Inr r1≠r2
    with xc-progress ta1a ta2a
  ...  | Inr xca-fails = Inr (XCFPair1 xca-fails)
  ...  | Inl (_ , xca)
    with xc-progress ta1b ta2b
  ...  | Inr xcb-fails = Inr (XCFPair2 xcb-fails)
  ...  | Inl (_ , xcb) = Inl (_ , XCPair r1≠r2 xca xcb)
  xc-progress ta1@(TAPair _ _) ta2@(TAApp _ _) | Inr r1≠r2
    with Coerce-dec
  ...  | Inr nc         = Inr (XCFNoCoerce r1≠r2 (Inr (λ ())) (Inr (λ ())) (λ {c-r1 → nc (_ , c-r1)}) λ ())
  ...  | Inl (_ , c-r1)
    with xb-progress ta2 (Coerce-preservation ta1 c-r1)
  ...  | Inr xb-fails   = Inr (XCFXB2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb-fails)
  ...  | Inl (_ , xb)   = Inl (_ , (XCBackProp2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb))
  xc-progress ta1@(TAPair _ _) ta2@(TAFst _) | Inr r1≠r2
    with Coerce-dec
  ...  | Inr nc         = Inr (XCFNoCoerce r1≠r2 (Inr (λ ())) (Inr (λ ())) (λ {c-r1 → nc (_ , c-r1)}) λ ())
  ...  | Inl (_ , c-r1)
    with xb-progress ta2 (Coerce-preservation ta1 c-r1)
  ...  | Inr xb-fails   = Inr (XCFXB2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb-fails)
  ...  | Inl (_ , xb)   = Inl (_ , (XCBackProp2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb))
  xc-progress ta1@(TAPair _ _) ta2@(TASnd _) | Inr r1≠r2
    with Coerce-dec
  ...  | Inr nc         = Inr (XCFNoCoerce r1≠r2 (Inr (λ ())) (Inr (λ ())) (λ {c-r1 → nc (_ , c-r1)}) λ ())
  ...  | Inl (_ , c-r1)
    with xb-progress ta2 (Coerce-preservation ta1 c-r1)
  ...  | Inr xb-fails   = Inr (XCFXB2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb-fails)
  ...  | Inl (_ , xb)   = Inl (_ , (XCBackProp2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb))
  xc-progress ta1@(TAPair _ _) ta2@(TAUnwrapCtor _ _ _) | Inr r1≠r2
    with Coerce-dec
  ...  | Inr nc         = Inr (XCFNoCoerce r1≠r2 (Inr (λ ())) (Inr (λ ())) (λ {c-r1 → nc (_ , c-r1)}) λ ())
  ...  | Inl (_ , c-r1)
    with xb-progress ta2 (Coerce-preservation ta1 c-r1)
  ...  | Inr xb-fails   = Inr (XCFXB2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb-fails)
  ...  | Inl (_ , xb)   = Inl (_ , (XCBackProp2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb))
  xc-progress ta1@(TAPair _ _) ta2@(TACase _ _ _ _ _) | Inr r1≠r2
    with Coerce-dec
  ...  | Inr nc         = Inr (XCFNoCoerce r1≠r2 (Inr (λ ())) (Inr (λ ())) (λ {c-r1 → nc (_ , c-r1)}) λ ())
  ...  | Inl (_ , c-r1)
    with xb-progress ta2 (Coerce-preservation ta1 c-r1)
  ...  | Inr xb-fails   = Inr (XCFXB2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb-fails)
  ...  | Inl (_ , xb)   = Inl (_ , (XCBackProp2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb))
  xc-progress ta1@(TAPair _ _) ta2@(TAHole _ _) | Inr r1≠r2
    with Coerce-dec
  ...  | Inr nc         = Inr (XCFNoCoerce r1≠r2 (Inr (λ ())) (Inr (λ ())) (λ {c-r1 → nc (_ , c-r1)}) λ ())
  ...  | Inl (_ , c-r1)
    with xb-progress ta2 (Coerce-preservation ta1 c-r1)
  ...  | Inr xb-fails   = Inr (XCFXB2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb-fails)
  ...  | Inl (_ , xb)   = Inl (_ , (XCBackProp2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb))
  xc-progress ta1@(TAFst _) ta2 | Inr r1≠r2
    = lemma-xc-no-coerce ta1 ta2 r1≠r2 (λ ()) (λ ()) (λ ()) λ ()
  xc-progress {r1 = _} {_} ta1@(TASnd _) ta2 | Inr r1≠r2
    = lemma-xc-no-coerce ta1 ta2 r1≠r2 (λ ()) (λ ()) (λ ()) λ ()
  xc-progress (TACtor {c = c1} d∈σ1 c1∈cctx ta1) (TACtor {c = c2} d∈σ2 c2∈cctx ta2) | Inr r1≠r2
    with natEQ c1 c2
  ...  | Inr ne         = Inr (XCFCtorMM ne)
  ...  | Inl refl
    rewrite ctxunicity d∈σ1 d∈σ2 | ctxunicity c1∈cctx c2∈cctx
    with xc-progress ta1 ta2
  ...  | Inr xc-fails   = Inr (XCFCtor xc-fails)
  ...  | Inl (_ , xc)   = Inl (_ , XCCtor (λ where refl → r1≠r2 refl) xc)
  xc-progress ta1@(TACtor _ _ _) ta2@(TAApp _ _) | Inr r1≠r2
    with Coerce-dec
  ...  | Inr nc         = Inr (XCFNoCoerce r1≠r2 (Inr (λ ())) (Inr (λ ())) (λ {c-r1 → nc (_ , c-r1)}) λ ())
  ...  | Inl (_ , c-r1)
    with xb-progress ta2 (Coerce-preservation ta1 c-r1)
  ...  | Inr xb-fails   = Inr (XCFXB2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb-fails)
  ...  | Inl (_ , xb)   = Inl (_ , (XCBackProp2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb))
  xc-progress ta1@(TACtor _ _ _) ta2@(TAFst _) | Inr r1≠r2
    with Coerce-dec
  ...  | Inr nc         = Inr (XCFNoCoerce r1≠r2 (Inr (λ ())) (Inr (λ ())) (λ {c-r1 → nc (_ , c-r1)}) λ ())
  ...  | Inl (_ , c-r1)
    with xb-progress ta2 (Coerce-preservation ta1 c-r1)
  ...  | Inr xb-fails   = Inr (XCFXB2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb-fails)
  ...  | Inl (_ , xb)   = Inl (_ , (XCBackProp2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb))
  xc-progress ta1@(TACtor _ _ _) ta2@(TASnd _) | Inr r1≠r2
    with Coerce-dec
  ...  | Inr nc         = Inr (XCFNoCoerce r1≠r2 (Inr (λ ())) (Inr (λ ())) (λ {c-r1 → nc (_ , c-r1)}) λ ())
  ...  | Inl (_ , c-r1)
    with xb-progress ta2 (Coerce-preservation ta1 c-r1)
  ...  | Inr xb-fails   = Inr (XCFXB2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb-fails)
  ...  | Inl (_ , xb)   = Inl (_ , (XCBackProp2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb))
  xc-progress ta1@(TACtor _ _ _) ta2@(TAUnwrapCtor _ _ _) | Inr r1≠r2
    with Coerce-dec
  ...  | Inr nc         = Inr (XCFNoCoerce r1≠r2 (Inr (λ ())) (Inr (λ ())) (λ {c-r1 → nc (_ , c-r1)}) λ ())
  ...  | Inl (_ , c-r1)
    with xb-progress ta2 (Coerce-preservation ta1 c-r1)
  ...  | Inr xb-fails   = Inr (XCFXB2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb-fails)
  ...  | Inl (_ , xb)   = Inl (_ , (XCBackProp2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb))
  xc-progress ta1@(TACtor _ _ _) ta2@(TACase _ _ _ _ _) | Inr r1≠r2
    with Coerce-dec
  ...  | Inr nc         = Inr (XCFNoCoerce r1≠r2 (Inr (λ ())) (Inr (λ ())) (λ {c-r1 → nc (_ , c-r1)}) λ ())
  ...  | Inl (_ , c-r1)
    with xb-progress ta2 (Coerce-preservation ta1 c-r1)
  ...  | Inr xb-fails   = Inr (XCFXB2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb-fails)
  ...  | Inl (_ , xb)   = Inl (_ , (XCBackProp2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb))
  xc-progress ta1@(TACtor _ _ _) ta2@(TAHole _ _) | Inr r1≠r2
    with Coerce-dec
  ...  | Inr nc         = Inr (XCFNoCoerce r1≠r2 (Inr (λ ())) (Inr (λ ())) (λ {c-r1 → nc (_ , c-r1)}) λ ())
  ...  | Inl (_ , c-r1)
    with xb-progress ta2 (Coerce-preservation ta1 c-r1)
  ...  | Inr xb-fails   = Inr (XCFXB2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb-fails)
  ...  | Inl (_ , xb)   = Inl (_ , (XCBackProp2 r1≠r2 (Inr (λ ())) (Inr (λ ())) c-r1 xb))
  xc-progress {r1 = _} {_} ta1@(TAUnwrapCtor _ _ _) ta2 | Inr r1≠r2
    = lemma-xc-no-coerce ta1 ta2 r1≠r2 (λ ()) (λ ()) (λ ()) λ ()
  xc-progress {r1 = _} {_} ta1@(TACase _ _ _ _ _) ta2 | Inr r1≠r2
    = lemma-xc-no-coerce ta1 ta2 r1≠r2 (λ ()) (λ ()) (λ ()) λ ()
  xc-progress {r1 = _} {_} ta1@(TAHole _ _) ta2 | Inr r1≠r2
    = lemma-xc-no-coerce ta1 ta2 r1≠r2 (λ ()) (λ ()) (λ ()) λ ()

  xb-progress {n = Z} _ _ = Inl (_ , XBLimit)
  xb-progress {ex = ex} {n = 1+ n} ta-r ta-ex
    with ex-¿¿-dec {ex}
  ... | Inl refl = Inl (_ , XBNone)
  xb-progress {n = 1+ n} ta-f@(TAFix Γ⊢E (TAFix ta-e)) (TAMap _ ta-v ta-ex) | Inr ne
    with progress {n = n} (EnvInd (EnvInd Γ⊢E ta-f) ta-v) ta-e
  ... | Inr fails    = Inr (XBFFixEval CF⛽ refl fails)
  ... | Inl (_ , _ , evals , ta)
    with xb-progress {n = n} ta ta-ex
  ... | Inr fails    = Inr (XBFFix CF⛽ refl evals fails)
  ... | Inl (_ , xb) = Inl (_ , XBFix CF⛽ refl evals xb)
  xb-progress (TAFix x (TAFix _)) TADC | Inr ne = Inl (_ , XBNone)
  xb-progress (TAApp {arg = v} ta-rf ta-rarg) ta-ex | Inr ne
    with value-dec {v}
  ... | Inr nv  = Inr (XBFAppNonVal ne nv)
  ... | Inl val
    with xb-progress ta-rf (TAMap val ta-rarg ta-ex)
  ... | Inr fails    = Inr (XBFApp ne val fails)
  ... | Inl (_ , xb) = Inl (_ , XBApp ne val xb)
  xb-progress TAUnit TAUnit | Inr ne = Inl (_ , XBUnit)
  xb-progress TAUnit TADC   | Inr ne = Inl (_ , XBNone)
  xb-progress (TAPair ta-r1 ta-r2) (TAPair ta-ex1 ta-ex2) | Inr ne
    with xb-progress ta-r1 ta-ex1
  ... | Inr fails     = Inr (XBFPair1 fails)
  ... | Inl (_ , xb1)
    with xb-progress ta-r2 ta-ex2
  ... | Inr fails     = Inr (XBFPair2 fails)
  ... | Inl (_ , xb2) = Inl (_ , XBPair xb1 xb2)
  xb-progress (TAPair ta-r1 ta-r2) TADC | Inr ne = Inl (_ , XBNone)
  xb-progress (TAFst ta-r) ta-ex | Inr ne
    with xb-progress ta-r (TAPair ta-ex TADC)
  ... | Inr fails    = Inr (XBFFst ne fails)
  ... | Inl (_ , xb) = Inl (_ , XBFst ne xb)
  xb-progress (TASnd ta-r) ta-ex | Inr ne
    with xb-progress ta-r (TAPair TADC ta-ex)
  ... | Inr fails    = Inr (XBFSnd ne fails)
  ... | Inl (_ , xb) = Inl (_ , XBSnd ne xb)
  xb-progress (TACtor {c = c1} h1a h1b ta-r) (TACtor {c = c2} h2a h2b ta-ex) | Inr ne
    with natEQ c1 c2
  ... | Inr ne'  = Inr (XBFCtorMM ne')
  ... | Inl refl
    rewrite ctxunicity h1a h2a | ctxunicity h1b h2b
    with xb-progress ta-r ta-ex
  ... | Inr fails    = Inr (XBFCtor fails)
  ... | Inl (_ , xb) = Inl (_ , XBCtor xb)
  xb-progress (TACtor x x₁ ta-r) TADC | Inr ne = Inl (_ , XBNone)
  xb-progress (TAUnwrapCtor h1 h2 ta-r) ta-ex | Inr ne
    with xb-progress ta-r (TACtor h1 h2 ta-ex)
  ... | Inr fails    = Inr (XBFUnwrapCtor ne fails)
  ... | Inl (_ , xb) = Inl (_ , XBUnwrapCtor ne xb)
  xb-progress {n = 1+ n} ta-C@(TACase {rules = rules} x x₁ ta-r x₂ x₃) ta-ex | Inr ne
    = lemma-xb-progress-case {n = 1+ n} {n} refl ∥ rules ∥ rules refl ∅ (λ y → y) (λ ()) Inl ta-C ta-ex ne
  xb-progress (TAHole x x₁) TAUnit | Inr ne
    = Inl (_ , XBHole ne λ ())
  xb-progress (TAHole x x₁) (TAPair ta-ex ta-ex₁) | Inr ne
    = Inl (_ , XBHole ne λ ())
  xb-progress (TAHole x x₁) (TACtor x₂ x₃ ta-ex) | Inr ne
    = Inl (_ , XBHole ne λ ())
  xb-progress (TAHole x x₁) TADC | Inr ne = Inl (_ , XBNone)
  xb-progress (TAHole x x₁) (TAMap x₂ x₃ ta-ex) | Inr ne
    = Inr XBFHole

  lemma-xb-progress-case {E = E} {r} {rules} {ex} {n = n} {n↓} refl Z [] len-unchecked failed unchecked-wf failed-wf exh ta-C ta-ex n¿¿
    = Inr (XBFMatch CF⛽ n¿¿ all-failed)
      where
        all-failed : ∀{c-j x-j : Nat} {e-j : exp} →
                       (c-j , |C x-j => e-j) ∈ rules →
                       r ⇐ C[ c-j ] ¿¿ ⌊ ⛽⟨ n ⟩ ⌋:=∅
                       ∨ Σ[ k1 ∈ constraints ] (
                             r ⇐ C[ c-j ] ¿¿ ⌊ ⛽⟨ n ⟩ ⌋:= k1 ∧ (E ,, (x-j , C⁻[ c-j ] r)) ⊢ e-j ⌊ ⛽⟨ n↓ ⟩ ⌋⇒∅)
                       ∨ Σ[ k1 ∈ constraints ] Σ[ k2 ∈ constraints ] Σ[ r-j ∈ result ] (
                             r ⇐ C[ c-j ] ¿¿ ⌊ ⛽⟨ n ⟩ ⌋:= k1 ∧ (E ,, (x-j , C⁻[ c-j ] r)) ⊢ e-j ⌊ ⛽⟨ n↓ ⟩ ⌋⇒ r-j ⊣ k2 ∧ r-j ⇐ ex ⌊ ⛽⟨ n↓ ⟩ ⌋:=∅)
        all-failed c-j∈rules
          with exh (_ , c-j∈rules)
        ... | Inl (_ , ())
        ... | Inr ((c-j , x-j , e-j , p-j) , c-j∈f)
          with failed-wf c-j∈f
        ... | refl , c-j∈'rules
          with ctxunicity c-j∈rules c-j∈'rules
        ... | refl = p-j
  lemma-xb-progress-case {n = 1+ n↓} {n↓} refl (1+ len) unchecked len-unchecked failed unchecked-wf failed-wf exh ta-C@(TACase {rules = rules} d∈σ' Γ⊢E ta-r _ ta-rules) ta-ex n¿¿
    with ctx-elim {Γ = unchecked}
  ... | Inl refl = abort (0≠1+n (! len-unchecked))
  ... | Inr (c , |C x-j => e-j , unchecked' , refl , c#unchecked')
    with unchecked-wf (x,a∈Γ,,x,a {Γ = unchecked'})
  ... | c∈rules
    with ta-rules c∈rules
  ... | _ , c∈cctx , ta-be
    with xb-progress ta-r (TACtor d∈σ' c∈cctx TADC)
  ... | Inr fails
          = lemma-xb-progress-case
              refl
              len
              unchecked'
              (1+inj (len-unchecked · ctx-decreasing c#unchecked'))
              (failed ,, (c , fail))
              unchecked-wf' failed-wf' exh' ta-C ta-ex n¿¿
            where
              fail = c , x-j , e-j , (Inl fails)
              unchecked-wf' : ∀{c' rule'} → (c' , rule') ∈ unchecked' → (c' , rule') ∈ rules
              unchecked-wf' {c' = c'} c'∈uc'
                with natEQ c c'
              ... | Inl refl = abort (c#unchecked' (_ , c'∈uc'))
              ... | Inr cne  = unchecked-wf (x∈Γ→x∈Γ+ (flip cne) c'∈uc')
              failed-wf' : ∀{c' c-j' x-j' e-j' p-j'} →
                             (c' , c-j' , x-j' , e-j' , p-j') ∈ (failed ,, (c , fail)) →
                             c' == c-j' ∧ ((c' , (|C x-j' => e-j')) ∈ rules)
              failed-wf' {c' = c'} {c-j'} c'∈f+
                with natEQ c c'
              ... | Inr cne  = failed-wf (x∈Γ+→x∈Γ (flip cne) c'∈f+)
              ... | Inl refl
                with ctxunicity c'∈f+ (x,a∈Γ,,x,a {Γ = failed})
              ... | refl = refl , c∈rules
              exh' : ∀{c'} → dom rules c' → dom unchecked' c' ∨ dom (failed ,, (c , fail)) c'
              exh' {c' = c'} c'∈rules
                with natEQ c c'
              ... | Inl refl = Inr (_ , x,a∈Γ,,x,a {Γ = failed})
              ... | Inr cne
                with exh c'∈rules
              ... | Inl (_ , c'∈uc) = Inl (_ , (x∈Γ+→x∈Γ (flip cne) c'∈uc))
              ... | Inr (_ , c'∈f)  = Inr (_ , x∈Γ→x∈Γ+ (flip cne) c'∈f)
  ... | Inl (_ , xb-r)
    with progress {n = n↓} (EnvInd Γ⊢E (TAUnwrapCtor d∈σ' c∈cctx ta-r)) ta-be
  ... | Inr fails
          = lemma-xb-progress-case
              refl
              len
              unchecked'
              (1+inj (len-unchecked · ctx-decreasing c#unchecked'))
              (failed ,, (c , fail))
              unchecked-wf' failed-wf' exh' ta-C ta-ex n¿¿
            where
              fail = c , x-j , e-j , (Inr (Inl (_ , xb-r , fails)))
              unchecked-wf' : ∀{c' rule'} → (c' , rule') ∈ unchecked' → (c' , rule') ∈ rules
              unchecked-wf' {c' = c'} c'∈uc'
                with natEQ c c'
              ... | Inl refl = abort (c#unchecked' (_ , c'∈uc'))
              ... | Inr cne  = unchecked-wf (x∈Γ→x∈Γ+ (flip cne) c'∈uc')
              failed-wf' : ∀{c' c-j' x-j' e-j' p-j'} →
                             (c' , c-j' , x-j' , e-j' , p-j') ∈ (failed ,, (c , fail)) →
                             c' == c-j' ∧ ((c' , (|C x-j' => e-j')) ∈ rules)
              failed-wf' {c' = c'} {c-j'} c'∈f+
                with natEQ c c'
              ... | Inr cne  = failed-wf (x∈Γ+→x∈Γ (flip cne) c'∈f+)
              ... | Inl refl
                with ctxunicity c'∈f+ (x,a∈Γ,,x,a {Γ = failed})
              ... | refl = refl , c∈rules
              exh' : ∀{c'} → dom rules c' → dom unchecked' c' ∨ dom (failed ,, (c , fail)) c'
              exh' {c' = c'} c'∈rules
                with natEQ c c'
              ... | Inl refl = Inr (_ , x,a∈Γ,,x,a {Γ = failed})
              ... | Inr cne
                with exh c'∈rules
              ... | Inl (_ , c'∈uc) = Inl (_ , (x∈Γ+→x∈Γ (flip cne) c'∈uc))
              ... | Inr (_ , c'∈f)  = Inr (_ , x∈Γ→x∈Γ+ (flip cne) c'∈f)
  ... | Inl (_ , _ , evals , ta-br)
    with xb-progress {n = n↓} ta-br ta-ex
  ... | Inr fails
          = lemma-xb-progress-case
              refl
              len
              unchecked'
              (1+inj (len-unchecked · ctx-decreasing c#unchecked'))
              (failed ,, (c , fail))
              unchecked-wf' failed-wf' exh' ta-C ta-ex n¿¿
            where
              fail = c , x-j , e-j , (Inr (Inr (_ , _ , _ , xb-r , evals , fails)))
              unchecked-wf' : ∀{c' rule'} → (c' , rule') ∈ unchecked' → (c' , rule') ∈ rules
              unchecked-wf' {c' = c'} c'∈uc'
                with natEQ c c'
              ... | Inl refl = abort (c#unchecked' (_ , c'∈uc'))
              ... | Inr cne  = unchecked-wf (x∈Γ→x∈Γ+ (flip cne) c'∈uc')
              failed-wf' : ∀{c' c-j' x-j' e-j' p-j'} →
                             (c' , c-j' , x-j' , e-j' , p-j') ∈ (failed ,, (c , fail)) →
                             c' == c-j' ∧ ((c' , (|C x-j' => e-j')) ∈ rules)
              failed-wf' {c' = c'} {c-j'} c'∈f+
                with natEQ c c'
              ... | Inr cne  = failed-wf (x∈Γ+→x∈Γ (flip cne) c'∈f+)
              ... | Inl refl
                with ctxunicity c'∈f+ (x,a∈Γ,,x,a {Γ = failed})
              ... | refl = refl , c∈rules
              exh' : ∀{c'} → dom rules c' → dom unchecked' c' ∨ dom (failed ,, (c , fail)) c'
              exh' {c' = c'} c'∈rules
                with natEQ c c'
              ... | Inl refl = Inr (_ , x,a∈Γ,,x,a {Γ = failed})
              ... | Inr cne
                with exh c'∈rules
              ... | Inl (_ , c'∈uc) = Inl (_ , (x∈Γ+→x∈Γ (flip cne) c'∈uc))
              ... | Inr (_ , c'∈f)  = Inr (_ , x∈Γ→x∈Γ+ (flip cne) c'∈f)
  ... | Inl (_ , xb)
          = Inl (_ , (XBMatch CF⛽ n¿¿ c∈rules xb-r evals xb))

{- TODO delete - this strong version is unprovable
module progress where
  progress : ∀{Δ Σ' Γ E e τ} →
               Δ , Σ' , Γ ⊢ E →
               Δ , Σ' , Γ ⊢ e :: τ →
               -- Either there's some properly-typed result that e will eval to
               -- for any beta reduction limit ...
               Σ[ r ∈ result ] (
                  Δ , Σ' ⊢ r ·: τ ∧
                  ∀{n} → Σ[ k ∈ constraints ] (E ⊢ e ⌊ ⛽⟨ n ⟩ ⌋⇒ r ⊣ k))
               ∨
               -- ... or evaluation will have a constraint failure for any
               -- beta reduction limit
               (∀{n} → E ⊢ e ⌊ ⛽⟨ n ⟩ ⌋⇒∅)
  progress Γ⊢E ta'@(TALam _ ta) = Inl (_ , TALam Γ⊢E ta' , (_ , EFun))
  progress Γ⊢E ta'@(TAFix _ _ ta) = Inl (_ , TAFix Γ⊢E ta' , (_ , EFix))
  progress Γ⊢E (TAVar x∈Γ)
    with env-all-Γ Γ⊢E x∈Γ
  ... | _ , x∈E , ta = Inl (_ , ta , (_ , EVar x∈E))
  progress Γ⊢E (TAApp _ ta-f ta-arg)
    with progress Γ⊢E ta-arg
  ... | Inr arg-fails = Inr (EFAppArg arg-fails)
  ... | Inl (_ , ta-rarg , arg-evals)
    with progress Γ⊢E ta-f
  ... | Inr f-fails = Inr (EFAppFun f-fails)
  progress Γ⊢E (TAApp _ ta-f ta-arg) | Inl (_ , ta-rarg , arg-evals) | Inl (([ E' ]λ x => ef) , TALam Γ'⊢E' (TALam x#Γ' ta-ef) , f-evals)
    with progress (EnvInd Γ'⊢E' ta-rarg) ta-ef
  ... | q = {!!}
  progress Γ⊢E (TAApp _ ta-f ta-arg) | Inl (_ , ta-rarg , arg-evals) | Inl ([ E' ]fix f ⦇·λ x => ef ·⦈ , ta-rf , f-evals) = {!!}
  progress Γ⊢E (TAApp _ ta-f ta-arg) | Inl (_ , ta-rarg , arg-evals) | Inl ([ x ]??[ x₁ ] , ta-rf , f-evals) = {!!}
  progress Γ⊢E (TAApp _ ta-f ta-arg) | Inl (_ , ta-rarg , arg-evals) | Inl ((rf ∘ rf₁) , ta-rf , f-evals) = {!!}
  progress Γ⊢E (TAApp _ ta-f ta-arg) | Inl (_ , ta-rarg , arg-evals) | Inl ((get[ x th-of x₁ ] rf) , ta-rf , f-evals) = {!!}
  progress Γ⊢E (TAApp _ ta-f ta-arg) | Inl (_ , ta-rarg , arg-evals) | Inl ([ x ]case rf of⦃· x₁ ·⦄ , ta-rf , f-evals) = {!!}
  progress Γ⊢E (TAApp _ ta-f ta-arg) | Inl (_ , ta-rarg , arg-evals) | Inl (PF x , ta-rf , f-evals) = {!!}
  progress Γ⊢E (TATpl ∥es∥==∥τs∥ _ tas) = {!!}
  progress {Δ} {Σ'} {E = E} {τ = τ} Γ⊢E (TAGet {i = i} {len} {e} len==∥τs∥ i<∥τs∥ ta)
    with progress Γ⊢E ta
  ... | Inr e-fails = Inr (EFGet e-fails)
  ... | Inl (⟨ rs ⟩ , TATpl ∥rs∥==∥τs∥ tas , e-evals)
          = let i<∥rs∥ = tr (λ y → i < y) (! ∥rs∥==∥τs∥) i<∥τs∥ in
            Inl (_ , tas i<∥rs∥ i<∥τs∥ , _ , EGet (len==∥τs∥ · ! ∥rs∥==∥τs∥) i<∥rs∥ (π2 e-evals))
  ... | Inl (([ x ]λ x₁ => x₂) , TALam _ () , e-evals)
  ... | Inl ([ x ]fix x₁ ⦇·λ x₂ => x₃ ·⦈ , TAFix _ () , e-evals)
  ... | Inl ([ x ]??[ x₁ ] , ta-r , e-evals)
          rewrite len==∥τs∥ = Inl (_ , TAGet i<∥τs∥ ta-r , _ , EGetUnfinished (π2 e-evals) λ ())
  ... | Inl ((r ∘ r₁) , ta-r , e-evals)
          rewrite len==∥τs∥ = Inl (_ , TAGet i<∥τs∥ ta-r , _ , EGetUnfinished (π2 e-evals) λ ())
  ... | Inl ((get[ x th-of x₁ ] r) , ta-r , e-evals)
          rewrite len==∥τs∥ = Inl (_ , TAGet i<∥τs∥ ta-r , _ , EGetUnfinished (π2 e-evals) λ ())
  ... | Inl ([ x ]case r of⦃· x₁ ·⦄ , ta-r , e-evals)
          rewrite len==∥τs∥ = Inl (_ , TAGet i<∥τs∥ ta-r , _ , EGetUnfinished (π2 e-evals) λ ())
  ... | Inl (PF x , TAPF () , e-evals)
  progress Γ⊢E (TACtor d∈Σ' c∈d ta)
    with progress Γ⊢E ta
  ... | Inl (_ , ta-r , e-evals) = Inl (_ , TACtor d∈Σ' c∈d ta-r , _ , ECtor (π2 e-evals))
  ... | Inr e-fails = Inr (EFCtor e-fails)
  progress Γ⊢E (TACase x ta x₁ x₂) = {!!}
  progress Γ⊢E (TAHole u∈Δ) = Inl (_ , TAHole u∈Δ Γ⊢E , (_ , EHole))
  progress Γ⊢E (TAPF ta) = Inl (_ , TAPF ta , (_ , EPF))
  progress Γ⊢E (TAAsrt x ta ta₁) = {!!}
-}

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-


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

open import Prelude
open import GSeTT.Syntax
open import GSeTT.Rules
open import GSeTT.Uniqueness-Derivations
open import Sets ℕ eqdecℕ
open import GSeTT.Dec-Type-Checking
open import CaTT.Ps-contexts

{- PS-contexts -}
module CaTT.Relation where

  -- The relation ◃ generating cases
  data _,_◃₀_ Γ x y : Set₁ where
    ◃∂⁻ : ∀{A z} → Γ ⊢t (Var y) # (⇒ A (Var x) (Var z)) → Γ , x ◃₀ y
    ◃∂⁺ : ∀{A z} → Γ ⊢t (Var x) # (⇒ A (Var z) (Var y)) → Γ , x ◃₀ y

  -- Transitive closure : we associate on the right
  data _,_◃_ Γ x y : Set₁ where
    gen : Γ , x ◃₀ y → Γ , x ◃ y
    ◃T : ∀{z} → Γ , x ◃ z → Γ , z ◃₀ y → Γ , x ◃ y

  rel : ∀ Γ x y → Set₁
  rel Γ x y = Γ , x ◃ y

  W◃₀ : ∀ {Γ x y z A} → (Γ :: (z , A)) ⊢C → Γ , x ◃₀ y → (Γ :: (z , A)) , x ◃₀ y
  W◃₀ Γ+⊢ (◃∂⁻ Γ⊢x) = ◃∂⁻ (wkt Γ⊢x Γ+⊢)
  W◃₀ Γ+⊢ (◃∂⁺ Γ⊢x) = ◃∂⁺ (wkt Γ⊢x Γ+⊢)

  W◃ : ∀ {Γ x y z A} → (Γ :: (z , A)) ⊢C → Γ , x ◃ y → (Γ :: (z , A)) , x ◃ y
  W◃ Γ+⊢ (gen x◃₀y) = gen (W◃₀ Γ+⊢ x◃₀y)
  W◃ Γ+⊢ (◃T x◃y y◃₀z) = ◃T (W◃ Γ+⊢ x◃y) (W◃₀ Γ+⊢ y◃₀z)

  WW◃ : ∀ {Γ x y z f A B} → ((Γ :: (z , A)) :: (f , B)) ⊢C → Γ , x ◃ y → ((Γ :: (z , A)) :: (f , B)) , x ◃ y
  WW◃ Γ+⊢@(cc Γ⊢ _ idp) x◃y = W◃ Γ+⊢ (W◃ Γ⊢ x◃y)

  ◃-trans : ∀ {Γ x y z} → Γ , x ◃ y → Γ , y ◃ z → Γ , x ◃ z
  ◃-trans x◃y (gen y◃₀z) = ◃T x◃y y◃₀z
  ◃-trans x◃y (◃T y◃z z◃₀w) = ◃T (◃-trans x◃y y◃z) z◃₀w

  -- TODO : Move at the right place
  x#A∈Γ→x∈Γ : ∀ {Γ x A} → x # A ∈ Γ → x ∈ Γ
  x#A∈Γ→x∈Γ {Γ :: (y , _)} (inl x#A∈Γ) = inl (x#A∈Γ→x∈Γ x#A∈Γ)
  x#A∈Γ→x∈Γ {Γ :: (y , _)} (inr (idp , idp)) = inr idp

  Γ⊢x:A→x∈Γ : ∀ {Γ x A} → Γ ⊢t (Var x) # A → x ∈ Γ
  Γ⊢x:A→x∈Γ (var _ x#A∈Γ) = x#A∈Γ→x∈Γ x#A∈Γ

  data _,_⟿_ : Pre-Ctx → ℕ → ℕ → Set₁ where -- y is an iterated target of x in Γ
    ∂⁺⟿ : ∀{Γ x a y A} → Γ ⊢t (Var x) # (⇒ A (Var a) (Var y)) → Γ , x ⟿ y
    x⟿∂⁺ : ∀{Γ x a y z A} → Γ ⊢t (Var x) # (⇒ A (Var a) (Var y)) → Γ , y ⟿ z → Γ , x ⟿ z

  W⟿ : ∀ {Γ x y z A} → (Γ :: (z , A)) ⊢C → Γ , x ⟿ y → (Γ :: (z , A)) , x ⟿ y
  W⟿ Γ+⊢ (∂⁺⟿ Γ⊢x) = ∂⁺⟿ (wkt Γ⊢x Γ+⊢)
  W⟿ Γ+⊢ (x⟿∂⁺ Γ⊢x x⟿y) = x⟿∂⁺ (wkt Γ⊢x Γ+⊢) (W⟿ Γ+⊢ x⟿y)

  WW⟿ : ∀ {Γ x y z w A B} → ((Γ :: (z , A)) :: (w , B)) ⊢C → Γ , x ⟿ y → ((Γ :: (z , A)) :: (w , B)) , x ⟿ y
  WW⟿ Γ++⊢@(cc Γ+⊢ _ idp) x⟿y = W⟿ Γ++⊢ (W⟿ Γ+⊢ x⟿y)

  ⟿→◃ : ∀ {Γ x y} → Γ , x ⟿ y → Γ , x ◃ y
  ⟿→◃ (∂⁺⟿ Γ⊢x) = gen (◃∂⁺ Γ⊢x)
  ⟿→◃ (x⟿∂⁺ Γ⊢x x⟿y) = ◃-trans (gen (◃∂⁺ Γ⊢x)) (⟿→◃ x⟿y)

  Γ++ : ∀ {Γ x A} → Γ ⊢ps x # A → Pre-Ctx
  Γ++ {Γ} {x} {A} _ = (Γ :: (length Γ , A)) :: (S (length Γ) , ⇒ A (Var x) (Var (length Γ)))

  //⟿ : ∀ {Γ Δ x y A a} → Γ ⊢t (Var x) # A → Δ ⊢t (Var y) # A → Γ , x ⟿ a → Δ , y ⟿ a
  //⟿ Γ⊢x Δ⊢y (∂⁺⟿ Γ⊢x') with unique-type Γ⊢x Γ⊢x' idp
  ... | idp = ∂⁺⟿ Δ⊢y
  //⟿ Γ⊢x Δ⊢y (x⟿∂⁺ Γ⊢x' x⟿a) with unique-type Γ⊢x Γ⊢x' idp
  ... | idp = x⟿∂⁺ Δ⊢y (//⟿ (Γ⊢tgt (Γ⊢t:A→Γ⊢A Γ⊢x)) (Γ⊢tgt (Γ⊢t:A→Γ⊢A Δ⊢y)) x⟿a)

  T⟿ : ∀ {Γ x y z} → Γ , x ⟿ y → Γ , y ⟿ z → Γ , x ⟿ z
  T⟿ (∂⁺⟿ Γ⊢x) y⟿z = x⟿∂⁺ Γ⊢x y⟿z
  T⟿ (x⟿∂⁺ Γ⊢x x⟿y) y⟿z = x⟿∂⁺ Γ⊢x (T⟿ x⟿y y⟿z)

  ⟿dim : ∀ {Γ x y A B} → Γ ⊢t Var x # A → Γ ⊢t Var y # B → Γ , x ⟿ y → dim B < dim A
  ⟿dim Γ⊢x:A Γ⊢y:B (∂⁺⟿ Γ⊢x) with unique-type Γ⊢x:A Γ⊢x idp | unique-type Γ⊢y:B (Γ⊢tgt(Γ⊢t:A→Γ⊢A Γ⊢x)) idp
  ... | idp | idp = n≤n _
  ⟿dim Γ⊢x:A Γ⊢y:B (x⟿∂⁺ Γ⊢x z⟿y) with unique-type Γ⊢x:A Γ⊢x idp
  ... | idp = n≤m→n≤Sm (⟿dim (Γ⊢tgt(Γ⊢t:A→Γ⊢A Γ⊢x)) Γ⊢y:B z⟿y)

  𝔻0-◃ : ∀ z → ¬ ((nil :: (0 , ∗)) , 0 ◃ z)
  𝔻0-◃ z (gen (◃∂⁻ (var _ (inl ()))))
  𝔻0-◃ z (gen (◃∂⁻ (var _ (inr ()))))
  𝔻0-◃ z (gen (◃∂⁺ (var _ (inl ()))))
  𝔻0-◃ z (gen (◃∂⁺ (var _ (inr ()))))
  𝔻0-◃ z (◃T 0◃x _) = 𝔻0-◃ _ 0◃x

  𝔻0-⟿ : ∀ z → ¬ ((nil :: (0 , ∗)) , 0 ⟿ z)
  𝔻0-⟿ z (∂⁺⟿ (var _ (inl ())))
  𝔻0-⟿ z (∂⁺⟿ (var _ (inr ())))
  𝔻0-⟿ z (x⟿∂⁺ (var _ (inl ())) _)
  𝔻0-⟿ z (x⟿∂⁺ (var _ (inr ())) _)

  n≮n : ∀ n → ¬ (n < n)
  n≮n n n<n = Sn≰n _ n<n

  ⟿-is-tgt : ∀ {Γ x y z A} → Γ ⊢t Var x # ⇒ A (Var y) (Var z) → Γ , x ⟿ y → y == z
  ⟿-is-tgt Γ⊢x (∂⁺⟿ Γ⊢'x) with unique-type Γ⊢x Γ⊢'x idp
  ... | idp = idp
  ⟿-is-tgt Γ⊢x (x⟿∂⁺ Γ⊢'x y'⟿y) with unique-type Γ⊢x Γ⊢'x idp
  ... | idp = ⊥-elim (Sn≰n _ (⟿dim (Γ⊢tgt (Γ⊢t:A→Γ⊢A Γ⊢'x)) (Γ⊢src (Γ⊢t:A→Γ⊢A Γ⊢x)) y'⟿y))

  no-loop : ∀{Γ x y z T a A} → Γ ⊢ps a # A → Γ ⊢t (Var x) # ⇒ T (Var y) (Var z) → y ≠ z
  no-loop pss (var _ (inl ())) idp
  no-loop pss (var _ (inr ())) idp
  no-loop (psd Γ⊢psf) Γ⊢x idp = no-loop Γ⊢psf Γ⊢x idp
  no-loop (pse Γ⊢psb idp idp idp idp idp) (var _ (inl (inl x∈Γ))) idp = no-loop Γ⊢psb (var (Γ⊢psx:A→Γ⊢ Γ⊢psb) x∈Γ) idp
  no-loop (pse Γ⊢psb idp idp idp idp idp) (var _ (inl (inr (idp , idp)))) idp = no-loop Γ⊢psb (Γ⊢psx:A→Γ⊢x:A Γ⊢psb) idp
  no-loop (pse Γ⊢psb idp idp idp idp idp) (var _ (inr (idp , idp))) idp = x∉ (Γ⊢psx:A→Γ⊢ Γ⊢psb) (n≤n _) (Γ⊢psx:A→Γ⊢x:A Γ⊢psb)

  dangling-is-not-a-source : ∀ {Γ x A} → Γ ⊢ps x # A → (∀ f z {B} →  ¬ (Γ ⊢t Var f # ⇒ B (Var x) (Var z)))
  post-dangling-is-not-a-source : ∀ {Γ x A} → Γ ⊢ps x # A → (∀ {y B} f z → Γ , x ⟿ y →  ¬ (Γ ⊢t (Var f) # ⇒ B (Var y) (Var z)))

  dangling-is-not-a-source pss _ _ (var _ (inl ()))
  dangling-is-not-a-source pss _ _ (var _ (inr ()))
  dangling-is-not-a-source {x = x} (psd Γ⊢ps) t u Γ⊢t = post-dangling-is-not-a-source Γ⊢ps t u  (∂⁺⟿ (psvar Γ⊢ps)) Γ⊢t
  dangling-is-not-a-source (pse Γ⊢ps idp idp idp idp idp) _ _ (var _ (inl (inl x∈Γ))) = x∉ (psv Γ⊢ps) (n≤Sn _) (Γ⊢src (Γ⊢t:A→Γ⊢A (var (psv Γ⊢ps) x∈Γ)))
  dangling-is-not-a-source (pse Γ⊢ps idp idp idp idp idp) _ _ (var _ (inl (inr (idp , idp)))) = x∉ (psv Γ⊢ps) (n≤Sn _) (Γ⊢src (Γ⊢t:A→Γ⊢A (psvar Γ⊢ps)))
  dangling-is-not-a-source (pse Γ⊢ps idp idp idp idp idp) _ _ (var _ (inr (idp , idp))) = x∉ (psv Γ⊢ps) (n≤Sn _) (psvar Γ⊢ps)
  post-dangling-is-not-a-source pss t u x⟿y Γ⊢t = 𝔻0-⟿ _ x⟿y
  post-dangling-is-not-a-source (psd Γ⊢ps) t u x⟿y Γ⊢t = post-dangling-is-not-a-source Γ⊢ps t u (T⟿ (∂⁺⟿ (psvar Γ⊢ps)) x⟿y) Γ⊢t
  post-dangling-is-not-a-source Γ+⊢@(pse Γ⊢ps idp idp idp idp idp) t u (∂⁺⟿ Γ⊢Sl) Γ⊢t with unique-type Γ⊢Sl (psvar Γ+⊢) idp
  post-dangling-is-not-a-source (pse Γ⊢ps idp idp idp idp idp) _ _ (∂⁺⟿ Γ⊢Sl) (var _ (inl (inl t∈Γ))) | idp = x∉ (psv Γ⊢ps) (n≤n _) (Γ⊢src (Γ⊢t:A→Γ⊢A (var (psv Γ⊢ps) t∈Γ)))
  post-dangling-is-not-a-source (pse Γ⊢ps idp idp idp idp idp) _ _ (∂⁺⟿ Γ⊢Sl) (var _ (inl (inr (idp , idp)))) | idp = x∉ (psv Γ⊢ps) (n≤n _) (Γ⊢src (Γ⊢t:A→Γ⊢A (psvar Γ⊢ps)))
  post-dangling-is-not-a-source (pse Γ⊢ps idp idp idp idp idp) _ _ (∂⁺⟿ Γ⊢Sl) (var _ (inr (idp , idp))) | idp = x∉ (psv Γ⊢ps) (n≤n _) (psvar Γ⊢ps)
  post-dangling-is-not-a-source Γ+⊢@(pse Γ⊢ps idp idp idp idp idp) t u (x⟿∂⁺ Γ⊢Sl x⟿y) Γ⊢t with unique-type Γ⊢Sl (psvar Γ+⊢) idp
  post-dangling-is-not-a-source (pse Γ⊢ps idp idp idp idp idp) _ _ (x⟿∂⁺ Γ⊢Sl x⟿y) (var Γ+⊢ (inl (inl t∈Γ))) | idp =
         post-dangling-is-not-a-source Γ⊢ps _ _ (//⟿ (var Γ+⊢ (inl (inr (idp , idp)))) (psvar Γ⊢ps) x⟿y) (var (psv Γ⊢ps) t∈Γ)
  post-dangling-is-not-a-source (pse Γ⊢ps  idp idp idp idp idp)  _ _ (x⟿∂⁺ Γ⊢Sl x⟿y) (var Γ+⊢ (inl (inr (idp , idp)))) | idp with ⟿-is-tgt (var Γ+⊢ (inl (inr (idp , idp)))) x⟿y
  ... | idp = no-loop Γ⊢ps (psvar Γ⊢ps) idp
  post-dangling-is-not-a-source (pse Γ⊢ps idp idp idp idp idp) _ _ (x⟿∂⁺ Γ⊢Sl x⟿y) (var Γ++⊢@(cc Γ+⊢ _ p) (inr (idp , idp))) | idp = n≮n _ (⟿dim (var Γ++⊢ (inl (inr (idp , idp)))) (wkt (wkt (psvar Γ⊢ps) Γ+⊢) Γ++⊢) x⟿y)

  ⊢psx-◃₀→⟿ : ∀ {Γ x a A} → Γ ⊢ps x # A → Γ , x ◃₀ a → Γ , x ⟿ a
  ⊢psx-◃₀→⟿ Γ⊢psx (◃∂⁻ Γ⊢a) = ⊥-elim (dangling-is-not-a-source Γ⊢psx _ _ Γ⊢a)
  ⊢psx-◃₀→⟿ Γ⊢psx (◃∂⁺ Γ⊢x) = ∂⁺⟿ Γ⊢x

  ⊢psx-◃₀→⟿+ : ∀ {Γ x y a A} → Γ ⊢ps x # A → Γ , x ⟿ y → Γ , y ◃₀ a → Γ , y ⟿ a
  ⊢psx-◃₀→⟿+ Γ⊢psx x⟿y (◃∂⁻ Γ⊢a) = ⊥-elim (post-dangling-is-not-a-source Γ⊢psx _ _ x⟿y Γ⊢a)
  ⊢psx-◃₀→⟿+ Γ⊢psx x⟿y (◃∂⁺ Γ⊢y) = ∂⁺⟿ Γ⊢y

  ⊢psx-◃→⟿ : ∀ {Γ x a A} → Γ ⊢ps x # A → Γ , x ◃ a → Γ , x ⟿ a
  ⊢psx-◃→⟿+ : ∀ {Γ x a b A} → Γ ⊢ps x # A → Γ , x ⟿ a → Γ , a ◃ b → Γ , a ⟿ b

  ⊢psx-◃→⟿ Γ⊢psx (gen x◃₀a) = ⊢psx-◃₀→⟿ Γ⊢psx x◃₀a
  ⊢psx-◃→⟿ Γ⊢psx (◃T x◃z z◃₀a) = T⟿ (⊢psx-◃→⟿ Γ⊢psx x◃z) (⊢psx-◃₀→⟿+ Γ⊢psx (⊢psx-◃→⟿ Γ⊢psx x◃z) z◃₀a)
  ⊢psx-◃→⟿+ Γ⊢psx x⟿y (gen y◃₀a) = ⊢psx-◃₀→⟿+ Γ⊢psx x⟿y y◃₀a
  ⊢psx-◃→⟿+ Γ⊢psx x⟿y (◃T y◃z z◃₀a) = T⟿ (⊢psx-◃→⟿+ Γ⊢psx x⟿y y◃z) (⊢psx-◃₀→⟿+ Γ⊢psx (T⟿ x⟿y (⊢psx-◃→⟿+ Γ⊢psx x⟿y y◃z)) z◃₀a)

  -- easy to finish, and follows the paper proof
  psx-◃-linear→ : ∀ {Γ x A} → Γ ⊢ps x # A → (∀ a b → a ∈ Γ → b ∈ Γ → (((Γ , a ◃ b) + (Γ , b ◃ a)) + (a == b)))
  psx-◃-linear→ pss .0 .0 (inr idp) (inr idp) = inr idp
  psx-◃-linear→ (psd Γ⊢psx) a b a∈Γ b∈Γ = psx-◃-linear→ Γ⊢psx a b a∈Γ b∈Γ
  psx-◃-linear→ Γ++⊢ps@(pse Γ⊢psx idp idp idp idp idp) a b (inl (inl a∈Γ)) (inl (inl b∈Γ)) with psx-◃-linear→ Γ⊢psx a b a∈Γ b∈Γ
  ... | inl (inl a◃b) = inl (inl (WW◃ (psv Γ++⊢ps) a◃b))
  ... | inl (inr b◃a) = inl (inr (WW◃ (psv Γ++⊢ps) b◃a))
  ... | inr idp = inr idp
  psx-◃-linear→ Γ++⊢ps@(pse {x = x} Γ⊢psx idp idp idp idp idp) a .(length _) (inl (inl a∈Γ)) (inl (inr idp)) with psx-◃-linear→ Γ⊢psx a x a∈Γ (Γ⊢x:A→x∈Γ (psvar Γ⊢psx)) -- a ∈ Γ , b = y
  ... | inl (inl a◃x) = inl (inl (◃-trans (WW◃ (psv Γ++⊢ps) a◃x) (◃T (gen (◃∂⁻ (psvar Γ++⊢ps))) ((◃∂⁺ (psvar Γ++⊢ps)))))) -- a ◃ x
  ... | inl (inr x◃a) = inl (inr (⟿→◃ (//⟿ (psvar Γ⊢psx) (var (psv Γ++⊢ps) (inl (inr (idp , idp)))) (⊢psx-◃→⟿ Γ⊢psx x◃a)))) -- x ◃ a
  ... | inr idp = inl (inl (◃T (gen (◃∂⁻ (psvar Γ++⊢ps))) (◃∂⁺ (psvar Γ++⊢ps)))) -- a = x
  psx-◃-linear→ Γ++⊢ps@(pse {x = x} Γ⊢psx idp idp idp idp idp) a .(S (length _)) (inl (inl a∈Γ)) (inr idp) with psx-◃-linear→ Γ⊢psx a x a∈Γ (Γ⊢x:A→x∈Γ (psvar Γ⊢psx)) -- a ∈ Γ , b = f (**)
  ... | inl (inl a◃x) = inl (inl (◃T (WW◃ (psv Γ++⊢ps) a◃x) (◃∂⁻ (psvar Γ++⊢ps)))) -- a ◃ x
  ... | inl (inr x◃a) = inl (inr (⟿→◃ (x⟿∂⁺ (psvar Γ++⊢ps) (//⟿ (psvar Γ⊢psx) (var (psv Γ++⊢ps) (inl (inr (idp , idp)))) (⊢psx-◃→⟿ Γ⊢psx x◃a))))) -- x ◃ a
  ... | inr idp = inl (inl (gen (◃∂⁻ (psvar Γ++⊢ps)))) -- a = x
  psx-◃-linear→ Γ++⊢ps@(pse {x = x} Γ⊢psx idp idp idp idp idp) .(length _) b (inl (inr idp)) (inl (inl b∈Γ)) with psx-◃-linear→ Γ⊢psx b x b∈Γ (Γ⊢x:A→x∈Γ (psvar Γ⊢psx)) -- a = y, b ∈ Γ
  ... | inl (inl b◃x) = inl (inr (◃-trans (WW◃ (psv Γ++⊢ps) b◃x) (◃T (gen (◃∂⁻ (psvar Γ++⊢ps))) (◃∂⁺ (psvar Γ++⊢ps))))) -- b ◃ x
  ... | inl (inr x◃b) = inl (inl (⟿→◃ (//⟿ (psvar Γ⊢psx) (var (psv Γ++⊢ps) (inl (inr (idp , idp)))) (⊢psx-◃→⟿ Γ⊢psx x◃b)))) -- x ◃ b
  ... | inr idp = inl (inr (◃T (gen (◃∂⁻ (psvar Γ++⊢ps))) (◃∂⁺ (psvar Γ++⊢ps)))) -- b = x
  psx-◃-linear→ (pse Γ⊢psx idp idp idp idp idp) .(length _) .(length _) (inl (inr idp)) (inl (inr idp)) = inr idp
  psx-◃-linear→ Γ++⊢ps@(pse Γ⊢psx idp idp idp idp idp) .(length _) .(S (length _)) (inl (inr idp)) (inr idp) = inl (inr (gen (◃∂⁺ (psvar Γ++⊢ps)))) -- a = y, b = f
  psx-◃-linear→ Γ++⊢ps@(pse {x = x} Γ⊢psx  idp idp idp idp idp) .(S (length _)) b (inr idp) (inl (inl b∈Γ)) with psx-◃-linear→ Γ⊢psx b x b∈Γ (Γ⊢x:A→x∈Γ (psvar Γ⊢psx)) -- a = f b ∈ Γ
  ... | inl (inl b◃x) = inl (inr (◃T (WW◃ (psv Γ++⊢ps) b◃x) (◃∂⁻ (psvar Γ++⊢ps)))) -- b ◃ x
  ... | inl (inr x◃b) = inl (inl (⟿→◃ (x⟿∂⁺ (psvar Γ++⊢ps) (//⟿ (psvar Γ⊢psx) (var (psv Γ++⊢ps) (inl (inr (idp , idp)))) (⊢psx-◃→⟿ Γ⊢psx x◃b)))))  -- x ◃ b
  ... | inr idp = inl (inr (gen (◃∂⁻ (psvar Γ++⊢ps)))) -- b = x
  psx-◃-linear→ Γ++⊢ps@(pse Γ⊢psx idp idp idp idp idp) .(S (length _)) .(length _) (inr idp) (inl (inr idp)) = inl (inl (gen (◃∂⁺ (psvar Γ++⊢ps)))) -- a = f, b = y
  psx-◃-linear→ (pse Γ⊢psx idp idp idp idp idp) .(S (length _)) .(S (length _)) (inr idp) (inr idp) = inr idp

  strengthen : ∀ {Γ x A y B} → (Γ :: (y , B)) ⊢t Var x # A → x ∈ Γ → Γ ⊢t Var x # A
  strengthen (var (cc Γ⊢ _ idp) (inl x#A∈Γ)) x∈Γ = var Γ⊢ x#A∈Γ
  strengthen (var (cc Γ⊢ _ idp) (inr (idp , idp))) x∈Γ = ⊥-elim (l∉ Γ⊢ (n≤n _) x∈Γ)

  strengthen+ : ∀ {Γ x A y B z C} → ((Γ :: (y , B)) :: (z , C)) ⊢t Var x # A → x ∈ Γ → Γ ⊢t Var x # A
  strengthen+ Γ++⊢x x∈Γ = strengthen (strengthen Γ++⊢x (inl x∈Γ)) x∈Γ

  ◃₀∈ : ∀ {Γ x a} → Γ , x ◃₀ a → a ∈ Γ
  ◃₀∈ (◃∂⁻ Γ⊢a) = Γ⊢x:A→x∈Γ Γ⊢a
  ◃₀∈ (◃∂⁺ Γ⊢x) = Γ⊢x:A→x∈Γ (Γ⊢tgt (Γ⊢t:A→Γ⊢A Γ⊢x))

  ◃∈ : ∀ {Γ x a} → Γ , x ◃ a → a ∈ Γ
  ◃∈ (gen x◃₀a) = ◃₀∈ x◃₀a
  ◃∈ (◃T _ z◃₀x) = ◃₀∈ z◃₀x

  ∈◃₀ : ∀ {Γ x a} → Γ , x ◃₀ a → x ∈ Γ
  ∈◃₀ (◃∂⁻ Γ⊢a) = Γ⊢x:A→x∈Γ (Γ⊢src (Γ⊢t:A→Γ⊢A Γ⊢a))
  ∈◃₀ (◃∂⁺ Γ⊢x) = Γ⊢x:A→x∈Γ Γ⊢x

  ∈◃ : ∀ {Γ x a} → Γ , x ◃ a → x ∈ Γ
  ∈◃ (gen x◃₀a) = ∈◃₀ x◃₀a
  ∈◃ (◃T x◃z _) = ∈◃ x◃z

  WWpsx : ∀ {Γ x A} → (Γ⊢ps : Γ ⊢ps x # A) → Γ++ Γ⊢ps ⊢t (Var x) # A
  WWpsx Γ⊢ps = wkt (wkt (psvar Γ⊢ps) (cc (psv Γ⊢ps) (Γ⊢t:A→Γ⊢A (psvar Γ⊢ps)) idp)) (psv (pse Γ⊢ps idp idp idp idp idp))

  dangling-◃₀ : ∀ {Γ x A a} → (Γ⊢ps : Γ ⊢ps x # A) → Γ++ Γ⊢ps , S (length Γ) ◃₀ a → a == length Γ
  dangling-◃₀ Γ⊢ps (◃∂⁻ Γ⊢a) = ⊥-elim (dangling-is-not-a-source (pse Γ⊢ps idp idp idp idp idp) _ _ Γ⊢a)
  dangling-◃₀ Γ⊢ps (◃∂⁺ (var _ (inl (inl Sl∈Γ)))) = ⊥-elim (l∉ (psv Γ⊢ps) (n≤Sn _) (x#A∈Γ→x∈Γ Sl∈Γ))
  dangling-◃₀ Γ⊢ps (◃∂⁺ (var _ (inl (inr (Sl=l , idp))))) = ⊥-elim (Sn≠n _ Sl=l)
  dangling-◃₀ Γ⊢ps (◃∂⁺ (var _ (inr (_ , idp)))) = idp

  ◃₀-dangling : ∀ {Γ x A a} → (Γ⊢ps : Γ ⊢ps x # A) → Γ++ Γ⊢ps , a ◃₀ S (length Γ)  → a == x
  ◃₀-dangling Γ⊢ps (◃∂⁻ Γ+⊢Sl) with unique-type Γ+⊢Sl (psvar (pse Γ⊢ps idp idp idp idp idp)) idp
  ... | idp = idp
  ◃₀-dangling Γ⊢ps (◃∂⁺ (var x (inl (inl a∈Γ)))) = ⊥-elim (x∉ (psv Γ⊢ps) (n≤Sn _) (Γ⊢tgt (Γ⊢t:A→Γ⊢A (var (psv Γ⊢ps) a∈Γ))))
  ◃₀-dangling Γ⊢ps (◃∂⁺ (var x (inl (inr (idp , idp))))) = ⊥-elim (x∉ (psv Γ⊢ps) (n≤Sn _) (Γ⊢tgt (Γ⊢t:A→Γ⊢A (psvar Γ⊢ps))))
  ◃₀-dangling Γ⊢ps (◃∂⁺ (var x (inr (idp , abs)))) = ⊥-elim (Sn≠n _ (=Var (snd (=⇒ abs))))

  ◃₀-dangling-tgt : ∀ {Γ x A a} → (Γ⊢ps : Γ ⊢ps x # A) → Γ++ Γ⊢ps , a ◃₀ length Γ  → (a == S (length Γ)) + (Γ++ Γ⊢ps , a ◃₀ x)
  ◃₀-dangling-tgt Γ⊢ps (◃∂⁻ Γ+⊢l) with unique-type Γ+⊢l (var (psv (pse Γ⊢ps idp idp idp idp idp)) (inl (inr (idp , idp)))) idp
  ... | idp = inr (◃∂⁻ (WWpsx Γ⊢ps))
  ◃₀-dangling-tgt Γ⊢ps (◃∂⁺ (var x (inl (inl a∈Γ)))) = ⊥-elim (x∉ (psv Γ⊢ps) (n≤n _) (Γ⊢tgt (Γ⊢t:A→Γ⊢A (var (psv Γ⊢ps) a∈Γ))))
  ◃₀-dangling-tgt Γ⊢ps (◃∂⁺ (var x (inl (inr (idp , idp))))) = ⊥-elim (x∉ (psv Γ⊢ps) (n≤n _) (Γ⊢tgt (Γ⊢t:A→Γ⊢A (psvar Γ⊢ps))))
  ◃₀-dangling-tgt Γ⊢ps (◃∂⁺ (var x (inr (p , _)))) = inl p

  ◃-dangling : ∀ {Γ x A a} → (Γ⊢ps : Γ ⊢ps x # A) → Γ++ Γ⊢ps , a ◃ S (length Γ)  → (a == x) + (Γ++ Γ⊢ps , a ◃ x)
  ◃-dangling Γ⊢ps (gen x◃₀Sl) with ◃₀-dangling Γ⊢ps x◃₀Sl
  ... | idp = inl idp
  ◃-dangling Γ⊢ps (◃T a◃x x◃₀Sl) with ◃₀-dangling Γ⊢ps x◃₀Sl
  ... | idp = inr a◃x

  ◃-dangling-tgt : ∀ {Γ x A a} → (Γ⊢ps : Γ ⊢ps x # A) → Γ++ Γ⊢ps , a ◃ length Γ  → (a == S (length Γ) + (a == x)) + (Γ++ Γ⊢ps , a ◃ x)
  ◃-dangling-tgt Γ⊢ps (gen a◃₀l) with ◃₀-dangling-tgt Γ⊢ps a◃₀l
  ... | inl idp = inl (inl idp)
  ... | inr a◃₀x = inr (gen a◃₀x)
  ◃-dangling-tgt Γ⊢ps (◃T a◃z z◃₀l) with ◃₀-dangling-tgt Γ⊢ps z◃₀l
  ... | inl idp with ◃-dangling Γ⊢ps a◃z
  ... | inl idp = inl (inr idp)
  ... | inr a◃x = inr a◃x
  ◃-dangling-tgt Γ⊢ps (◃T a◃z z◃₀l) | inr z◃₀x = inr (◃T a◃z z◃₀x)

  strengthen-◃₀ : ∀ {Γ x A a b} → (Γ⊢ps : Γ ⊢ps x # A) → a ∈ Γ → b ∈ Γ → Γ++ Γ⊢ps , a ◃₀ b → Γ , a ◃₀ b
  strengthen-◃₀ Γ⊢ps a∈Γ b∈Γ (◃∂⁻ Γ⊢b) = ◃∂⁻ (strengthen+ Γ⊢b b∈Γ)
  strengthen-◃₀ Γ⊢ps a∈Γ b∈Γ (◃∂⁺ Γ⊢a) = ◃∂⁺ (strengthen+ Γ⊢a a∈Γ)

  -- useful particular case
  strengthen-◃₀-dangling : ∀ {Γ x A a} → (Γ⊢ps : Γ ⊢ps x # A) → Γ++ Γ⊢ps , length Γ ◃₀ a → Γ , x ◃₀ a
  strengthen-◃₀-dangling Γ⊢ps (◃∂⁻ Γ⊢a) = ⊥-elim (post-dangling-is-not-a-source (pse Γ⊢ps idp idp idp idp idp) _ _ (∂⁺⟿ (psvar (pse Γ⊢ps idp idp idp idp idp))) Γ⊢a)
  strengthen-◃₀-dangling Γ⊢ps (◃∂⁺ (var _ (inl (inl l∈Γ)))) = ⊥-elim (l∉ (psv Γ⊢ps) (n≤n _) (x#A∈Γ→x∈Γ l∈Γ))
  strengthen-◃₀-dangling Γ⊢ps (◃∂⁺ (var _ (inl (inr (_ , idp))))) = ◃∂⁺ (psvar Γ⊢ps)
  strengthen-◃₀-dangling Γ⊢ps (◃∂⁺ (var _ (inr (l=Sl , _)))) = ⊥-elim (Sn≠n _ (l=Sl ^))

  ∈-dangling : ∀ {Γ x A} → Γ ⊢ps x # A → x ∈ Γ
  ∈-dangling Γ⊢ps = Γ⊢x:A→x∈Γ (psvar Γ⊢ps)

  ∈-dangling-◃₀ : ∀ {Γ x A a} → (Γ⊢ps : Γ ⊢ps x # A) → Γ++ Γ⊢ps , a ◃₀ x → a ∈ Γ
  ∈-dangling-◃₀ Γ⊢ps (◃∂⁻ Γ+⊢x) with unique-type Γ+⊢x  (WWpsx Γ⊢ps) idp
  ... | idp = Γ⊢x:A→x∈Γ (Γ⊢src (Γ⊢t:A→Γ⊢A (psvar Γ⊢ps)))
  ∈-dangling-◃₀ Γ⊢ps (◃∂⁺ (var _ (inl (inl a∈Γ)))) = x#A∈Γ→x∈Γ a∈Γ
  ∈-dangling-◃₀ Γ⊢ps (◃∂⁺ (var _ (inl (inr (idp , idp))))) with unique-type (psvar Γ⊢ps) (Γ⊢tgt (Γ⊢t:A→Γ⊢A (psvar Γ⊢ps))) idp
  ... | ()
  ∈-dangling-◃₀ Γ⊢ps (◃∂⁺ (var _ (inr (idp , idp)))) = ⊥-elim (x∉ (psv Γ⊢ps) (n≤n _) (psvar Γ⊢ps))

  strengthen-dangling-◃₀ : ∀ {Γ x A a} → (Γ⊢ps : Γ ⊢ps x # A) → Γ++ Γ⊢ps , a ◃₀ x → Γ , a ◃₀ x
  strengthen-dangling-◃₀ Γ⊢ps a◃₀x = strengthen-◃₀ Γ⊢ps (∈-dangling-◃₀ Γ⊢ps a◃₀x) (∈-dangling Γ⊢ps) a◃₀x

  -- Not easy to find a way to express in a terminating way
  pse-◃-elim : ∀ {Γ x A a b} → (Γ⊢ps : Γ ⊢ps x # A) → a ∈ Γ → b ∈ Γ → Γ++ Γ⊢ps , a ◃ b → Γ , a ◃ b
  pse-◃-elim Γ⊢ps a∈Γ b∈Γ (gen a◃₀b) = gen (strengthen-◃₀ Γ⊢ps a∈Γ b∈Γ a◃₀b)
  pse-◃-elim Γ⊢ps a∈Γ b∈Γ (◃T a◃z z◃₀b) with ◃∈ a◃z
  pse-◃-elim Γ⊢ps a∈Γ b∈Γ (◃T a◃z z◃₀b) | inl (inl z∈Γ) = ◃T (pse-◃-elim Γ⊢ps a∈Γ z∈Γ a◃z) (strengthen-◃₀ Γ⊢ps z∈Γ b∈Γ z◃₀b)
  pse-◃-elim Γ⊢ps a∈Γ b∈Γ (◃T (gen a◃₀l) l◃₀b) | inl (inr idp) with ◃₀-dangling-tgt Γ⊢ps a◃₀l
  ... | inl idp = ⊥-elim (l∉ (psv Γ⊢ps) (n≤Sn _) a∈Γ)
  ... | inr a◃₀x = ◃T (gen (strengthen-◃₀ Γ⊢ps a∈Γ (∈-dangling Γ⊢ps) a◃₀x)) (strengthen-◃₀-dangling Γ⊢ps l◃₀b)
  pse-◃-elim Γ⊢ps a∈Γ b∈Γ (◃T (◃T a◃z z◃₀l) l◃₀b) | inl (inr idp) with ◃₀-dangling-tgt Γ⊢ps z◃₀l
  ... | inr z◃₀x = ◃T (◃T (pse-◃-elim Γ⊢ps a∈Γ (∈-dangling-◃₀ Γ⊢ps z◃₀x) a◃z) (strengthen-dangling-◃₀ Γ⊢ps z◃₀x)) (strengthen-◃₀-dangling Γ⊢ps l◃₀b)
  pse-◃-elim Γ⊢ps a∈Γ b∈Γ (◃T (◃T (gen a◃₀Sl) Sl◃₀l) l◃₀b) | inl (inr idp) | inl idp with ◃₀-dangling Γ⊢ps a◃₀Sl
  ... | idp = gen (strengthen-◃₀-dangling Γ⊢ps l◃₀b)
  pse-◃-elim Γ⊢ps a∈Γ b∈Γ (◃T (◃T (◃T a◃z z◃₀Sl) Sl◃₀l) l◃₀b) | inl (inr idp) | inl idp with ◃₀-dangling Γ⊢ps z◃₀Sl
  ... | idp = ◃T (pse-◃-elim Γ⊢ps a∈Γ (∈-dangling Γ⊢ps) a◃z) (strengthen-◃₀-dangling Γ⊢ps l◃₀b)
  pse-◃-elim Γ⊢ps a∈Γ b∈Γ (◃T a◃z z◃₀b) | inr idp with dangling-◃₀ Γ⊢ps z◃₀b
  ... | idp = ⊥-elim (l∉ (psv Γ⊢ps) (n≤n _) b∈Γ)

  psx-◃-linear← : ∀ {Γ z A} → Γ ⊢ps z # A → (∀ x → x ∈ Γ →  ¬ (Γ , x ◃ x))
  psx-◃-linear← pss .0 (inr idp) x◃x = 𝔻0-◃ 0 x◃x
  psx-◃-linear← (psd Γ⊢psz) x x∈Γ x◃x = psx-◃-linear← Γ⊢psz x x∈Γ x◃x
  psx-◃-linear← (pse Γ⊢psz idp idp idp idp idp) x (inl (inl x∈Γ)) x◃x = psx-◃-linear← Γ⊢psz x x∈Γ (pse-◃-elim Γ⊢psz x∈Γ x∈Γ x◃x)
  psx-◃-linear← Γ+⊢ps@(pse Γ⊢psz idp idp idp idp idp) x (inl (inr idp)) x◃x = ⊥-elim (Sn≰n _ (⟿dim (var (psv Γ+⊢ps) (inl (inr (idp , idp)))) (var (psv Γ+⊢ps) (inl (inr (idp , idp)))) (⊢psx-◃→⟿+ Γ+⊢ps (∂⁺⟿ (psvar Γ+⊢ps)) x◃x)))
  psx-◃-linear← Γ+⊢ps@(pse Γ⊢psz idp idp idp idp idp) x (inr idp) x◃x = ⊥-elim (Sn≰n _ (⟿dim (psvar Γ+⊢ps) (psvar Γ+⊢ps) (⊢psx-◃→⟿ Γ+⊢ps x◃x)))

  ◃-linear : Pre-Ctx → Set₁
  ◃-linear Γ = ∀ x y → x ∈ Γ → y ∈ Γ → (x ≠ y) ↔ ((Γ , x ◃ y) + (Γ , y ◃ x))

  ps-◃-linear : ∀ Γ → Γ ⊢ps → ◃-linear Γ
  fst (ps-◃-linear Γ (ps Γ⊢psz) x y x∈Γ y∈Γ) x≠y with psx-◃-linear→ Γ⊢psz x y x∈Γ y∈Γ
  ... | inl H = H
  ... | inr x=y = ⊥-elim (x≠y x=y)
  snd (ps-◃-linear Γ (ps Γ⊢psz) x .x x∈Γ y∈Γ) (inl x◃x) idp = psx-◃-linear← Γ⊢psz x x∈Γ x◃x
  snd (ps-◃-linear Γ (ps Γ⊢psz) x .x x∈Γ y∈Γ) (inr x◃x) idp = psx-◃-linear← Γ⊢psz x x∈Γ x◃x

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


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

open import Prelude
open import GSeTT.Syntax
open import GSeTT.Rules
open import GSeTT.Uniqueness-Derivations
open import Sets ℕ eqdecℕ
open import GSeTT.Dec-Type-Checking
open import CaTT.Ps-contexts
open import CaTT.Relation

{- PS-contexts -}
module CaTT.Uniqueness-Derivations-Ps where
  Γ⊢psx-dim≤ : ∀ {Γ x A} → Γ ⊢ps x # A → dim A ≤ dimC Γ
  Γ⊢psx-dim≤  pss = n≤n 0
  Γ⊢psx-dim≤ (psd Γ⊢psy) = Sn≤m→n≤m (Γ⊢psx-dim≤ Γ⊢psy)
  Γ⊢psx-dim≤ {((Γ :: (_ , A)) :: (_ , _))} {_} {_} (pse Γ⊢psx idp idp idp idp idp) with dec-≤ (dimC (Γ :: (length Γ , A))) (S (dim A))
  ... | inr res = Sn≤m→n≤m (≰ res)
  ... | inl res = n≤n (S (dim A))

  Γ⊢psx-dim : ∀ {Γ x y A B} → Γ ⊢ps x # A → Γ ⊢ps y # B → dim A == dim B → x == y
  Γ⊢psx-dim pss pss dimA=dimB = idp
  Γ⊢psx-dim {x = x} {y = y} {A = A} {B = B} (psd {x = x₁} Γ⊢psx) (psd {x = x₂} Γ⊢psy) dimA=dimB  = =Var (tgt= (unique-type (Γ⊢psx:A→Γ⊢x:A Γ⊢psx) (Γ⊢psx:A→Γ⊢x:A Γ⊢psy) (ap Var (Γ⊢psx-dim Γ⊢psx Γ⊢psy (ap S dimA=dimB)))))
  Γ⊢psx-dim {B = ∗} pss (psd Γ⊢psy) dimA=dimB = ⊥-elim (Sn≰n _ ((Γ⊢psx-dim≤ Γ⊢psy)))
  Γ⊢psx-dim {A = ∗} (psd Γ⊢psx) pss dimA=dimB = ⊥-elim (Sn≰n _ ((Γ⊢psx-dim≤ Γ⊢psx)))
  Γ⊢psx-dim (pse _ _ _ _ idp idp) (pse _ _ _ _ idp idp) dimA==dimB = idp
  Γ⊢psx-dim Γ++⊢psx@(psd Γ++⊢_) Γ++⊢psy@(pse _ idp idp idp idp idp) dimA=dimB with psx-◃-linear→ Γ++⊢psx _ _ (Γ⊢x:A→x∈Γ (psvar Γ++⊢psx)) (Γ⊢x:A→x∈Γ (psvar Γ++⊢psy))
  ... | inl (inl x◃Sl) = ⊥-elim (Sn≰n-t (dimA=dimB ^) (⟿dim (psvar Γ++⊢psx) (psvar Γ++⊢psy) (⊢psx-◃→⟿ Γ++⊢psx x◃Sl)))
  ... | inl (inr Sl◃x) = ⊥-elim (Sn≰n-t (dimA=dimB) (⟿dim (psvar Γ++⊢psy) (psvar Γ++⊢psx) (⊢psx-◃→⟿ Γ++⊢psy Sl◃x)))
  ... | inr idp = idp
  Γ⊢psx-dim Γ++⊢psx@(pse _  idp idp idp idp idp) Γ++⊢psy@(psd _) dimA=dimB with psx-◃-linear→ Γ++⊢psx _ _ (Γ⊢x:A→x∈Γ (psvar Γ++⊢psx)) (Γ⊢x:A→x∈Γ (psvar Γ++⊢psy))
  ... | inl (inl Sl◃y) = ⊥-elim (Sn≰n-t (dimA=dimB ^) (⟿dim (psvar Γ++⊢psx) (psvar Γ++⊢psy) (⊢psx-◃→⟿ Γ++⊢psx Sl◃y)))
  ... | inl (inr y◃Sl) = ⊥-elim (Sn≰n-t (dimA=dimB) (⟿dim (psvar Γ++⊢psy) (psvar Γ++⊢psx) (⊢psx-◃→⟿ Γ++⊢psy y◃Sl)))
  ... | inr idp = idp

  has-all-paths-⊢psx : ∀ {Γ x A} → has-all-paths (Γ ⊢ps x # A)
  has-all-paths-⊢psx pss pss = idp
  has-all-paths-⊢psx (psd a) (psd b) with (Γ⊢psx-dim a b idp)
  ... | idp with unique-type (psvar a) (psvar b) idp
  ... | p = psd↓ a b (=Var (snd (fst (=⇒ p)))) (has-all-paths-⊢psx _ _)
  has-all-paths-⊢psx  pss (psd b) with (psvar b)
  ... | var _ (inl ())
  ... | var _ (inr ())
  has-all-paths-⊢psx (psd a) pss with (psvar a)
  ... | var _ (inl ())
  ... | var _ (inr ())
  has-all-paths-⊢psx (psd a) (pse b idp idp idp idp idp) with (psvar a)
  ... | var _ (inl (inl contra)) = ⊥-elim (l∉ (psv b) (n≤Sn _) (Γ⊢x:A→x∈Γ (Γ⊢tgt (Γ⊢t:A→Γ⊢A (var (psv b) contra)))))
  has-all-paths-⊢psx (pse a idp idp idp idp idp) (psd b) with psvar b
  ... | var _ (inl (inl contra)) = ⊥-elim (l∉ (psv a) (n≤Sn _) (Γ⊢x:A→x∈Γ (Γ⊢tgt (Γ⊢t:A→Γ⊢A (var (psv a) contra)))))
  has-all-paths-⊢psx (pse a idp idp idp idp idp) (pse b p q r s u) = let eq = =Var (snd (fst (=⇒ r))) in pse↓ a _ _ _ _ _ b _ _ _ _ _ eq (has-all-paths-⊢psx _ _)

  has-all-paths-⊢ps : ∀ Γ → has-all-paths (Γ ⊢ps)
  has-all-paths-⊢ps Γ (ps Γ⊢psx₁) (ps Γ⊢psx₂) = ps↓ Γ⊢psx₁ Γ⊢psx₂ (Γ⊢psx-dim Γ⊢psx₁ Γ⊢psx₂ idp) (has-all-paths-⊢psx _ _)

  is-prop-⊢ps : ∀ Γ → is-prop (Γ ⊢ps)
  is-prop-⊢ps Γ = has-all-paths-is-prop (has-all-paths-⊢ps Γ)

  eqdec-ps : eqdec ps-ctx
  eqdec-ps (Γ , Γ⊢ps) (Δ , Δ⊢ps) with eqdec-PreCtx Γ Δ
  ... | inl idp = inl (Σ= idp (is-prop-has-all-paths (is-prop-⊢ps Γ) _ _))
  ... | inr Γ≠Δ = inr λ{idp → Γ≠Δ idp}


text:
module LateMetaVariableInstantiation where

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ    #-}

postulate
  yippie : (A : Set) → A

slow : (A : Set) → ℕ → A
slow A zero    = yippie A
slow A (suc n) = slow _ n

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

foo : slow ℕ 1000 ≡ yippie ℕ
foo = refl

-- Consider the function slow. Previously normalisation of slow n
-- seemed to take time proportional to n². The reason was that, even
-- though the meta-variable corresponding to the underscore was
-- solved, the stored code still contained a meta-variable:

--   slow A (suc n) = slow (_173 A n) n

-- (For some value of 173.) The evaluation proceeded as follows:

--   slow A 1000 =
--   slow (_173 A 999) 999 =
--   slow (_173 (_173 A 999) 998) 998 =
--   ...

-- Furthermore, in every iteration the Set argument was traversed, to
-- see if there was any de Bruijn index to raise.

max_stars_repo_name: masondesu/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Categories.Category
open import Categories.Monad

module Categories.Category.Construction.EilenbergMoore {o ℓ e} {C : Category o ℓ e} (M : Monad C) where

open import Level

open import Categories.Morphism.Reasoning C

private
  module C = Category C
  module M = Monad M
  open C
  open M.F
  open HomReasoning

record Module : Set (o ⊔ ℓ ⊔ e) where
  field
    A        : Obj
    action   : F₀ A ⇒ A
    commute  : action ∘ F₁ action ≈ action ∘ M.μ.η A
    identity : action ∘ M.η.η A ≈ C.id

record Module⇒ (X Y : Module) : Set (ℓ ⊔ e) where
  private
    module X = Module X
    module Y = Module Y
  field
    arr     : X.A ⇒ Y.A
    commute : arr ∘ X.action ≈ Y.action ∘ F₁ arr

EilenbergMoore : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e
EilenbergMoore = record
  { Obj       = Module
  ; _⇒_       = Module⇒
  ; _≈_       = λ f g → Module⇒.arr f ≈ Module⇒.arr g
  ; id        = record
    { arr     = C.id
    ; commute = id-comm-sym ○ ∘-resp-≈ʳ (⟺ identity)
    }
  ; _∘_       = compose
  ; assoc     = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv     = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  ; ∘-resp-≈  = ∘-resp-≈
  }
  where compose : ∀ {X Y Z} → Module⇒ Y Z → Module⇒ X Y → Module⇒ X Z
        compose {X} {Y} {Z} f g = record
          { arr     = f.arr ∘ g.arr
          ; commute = begin
            (f.arr ∘ g.arr) ∘ Module.action X       ≈⟨ pullʳ g.commute ⟩
            f.arr ∘ Module.action Y ∘ F₁ g.arr      ≈⟨ pullˡ f.commute ⟩
            (Module.action Z ∘ F₁ f.arr) ∘ F₁ g.arr ≈˘⟨ pushʳ homomorphism ⟩
            Module.action Z ∘ F₁ (f.arr ∘ g.arr)    ∎
          }
          where module f = Module⇒ f
                module g = Module⇒ g

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- A variant of code reported by Andreas Abel.

{-# OPTIONS --guardedness --sized-types #-}

open import Agda.Builtin.Size

data ⊥ : Set where

mutual
  data D : Size → Set where
    inn : ∀ i → D' i → D (↑ i)

  record D' (i : Size) : Set where
    coinductive
    constructor ♯
    field ♭   : D i
open D'

iter : ∀{i} → D i → ⊥
iter (inn i t) = iter (♭ t)

-- Should be rejected by termination checker
bla : D' ∞
♭ bla = inn ∞ bla

false : ⊥
false = iter (♭ bla)


text:
-- data construction, disproving

module Auto-DataConstruction where

open import Auto.Prelude

module Disproving where

 h0 : {X : Set} → (xs ys : List X) → (xs ++ ys) ≡ (ys ++ xs)
 h0 = {!-d Fin!}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Sum.Relation.Binary.LeftOrder directly.
------------------------------------------------------------------------

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

module Data.Sum.Relation.LeftOrder where

open import Data.Sum.Relation.Binary.LeftOrder public

{-# WARNING_ON_IMPORT
"Data.Sum.Relation.LeftOrder was deprecated in v1.0.
Use Data.Sum.Relation.Binary.LeftOrder instead."
#-}


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.ListedFiniteSet.Base where

open import Cubical.Core.Everything
open import Cubical.Foundations.Logic
open import Cubical.Foundations.Everything

private
  variable
    A : Type₀

infixr 20 _∷_
infix 30 _∈_

data LFSet (A : Type₀) : Type₀ where
  []    : LFSet A
  _∷_   : (x : A) → (xs : LFSet A) → LFSet A
  dup   : ∀ x xs   → x ∷ x ∷ xs ≡ x ∷ xs
  comm  : ∀ x y xs → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
  trunc : isSet (LFSet A)

-- Membership.
--
-- Doing some proofs with equational reasoning adds an extra "_∙ refl"
-- at the end.
-- We might want to avoid it, or come up with a more clever equational reasoning.
_∈_ : A → LFSet A → hProp
z ∈ []                  = ⊥
z ∈ (y ∷ xs)            = (z ≡ₚ y) ⊔ (z ∈ xs)
z ∈ dup x xs i          = proof i
  where
    -- proof : z ∈ (x ∷ x ∷ xs) ≡ z ∈ (x ∷ xs)
    proof = z ≡ₚ x  ⊔ (z ≡ₚ x ⊔ z ∈ xs) ≡⟨ ⊔-assoc (z ≡ₚ x) (z ≡ₚ x) (z ∈ xs) ⟩
            (z ≡ₚ x ⊔ z ≡ₚ x) ⊔ z ∈ xs  ≡⟨ cong (_⊔ (z ∈ xs)) (⊔-idem (z ≡ₚ x)) ⟩
            z ≡ₚ x            ⊔ z ∈ xs  ∎
z ∈ comm x y xs i       = proof i
  where
    -- proof : z ∈ (x ∷ y ∷ xs) ≡ z ∈ (y ∷ x ∷ xs)
    proof = z ≡ₚ x  ⊔ (z ≡ₚ y ⊔ z ∈ xs) ≡⟨ ⊔-assoc (z ≡ₚ x) (z ≡ₚ y) (z ∈ xs) ⟩
            (z ≡ₚ x ⊔ z ≡ₚ y) ⊔ z ∈ xs  ≡⟨ cong (_⊔ (z ∈ xs)) (⊔-comm (z ≡ₚ x) (z ≡ₚ y)) ⟩
            (z ≡ₚ y ⊔ z ≡ₚ x) ⊔ z ∈ xs  ≡⟨ sym (⊔-assoc (z ≡ₚ y) (z ≡ₚ x) (z ∈ xs)) ⟩
            z ≡ₚ y  ⊔ (z ≡ₚ x ⊔ z ∈ xs) ∎

x ∈ trunc xs ys p q i j = isSetHProp (x ∈ xs) (x ∈ ys) (cong (x ∈_) p) (cong (x ∈_) q) i j

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical