text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some examples showing how the AVL tree module can be used
------------------------------------------------------------------------

module README.AVL where

------------------------------------------------------------------------
-- Setup

-- AVL trees are defined in Data.AVL.

import Data.AVL

-- This module is parametrised by keys, which have to form a (strict)
-- total order, and values, which are indexed by keys. Let us use
-- natural numbers as keys and vectors of strings as values.

import Data.Nat.Properties as ℕ
open import Data.String using (String)
open import Data.Vec using (Vec; _∷_; [])
open import Relation.Binary using (module StrictTotalOrder)

open Data.AVL (Vec String)
              (StrictTotalOrder.isStrictTotalOrder ℕ.strictTotalOrder)

------------------------------------------------------------------------
-- Construction of trees

-- Some values.

v₁  = "cepa" ∷ []
v₁′ = "depa" ∷ []
v₂  = "apa" ∷ "bepa" ∷ []

-- Empty and singleton trees.

t₀ : Tree
t₀ = empty

t₁ : Tree
t₁ = singleton 2 v₂

-- Insertion of a key-value pair into a tree.

t₂ = insert 1 v₁ t₁

-- If you insert a key-value pair and the key already exists in the
-- tree, then the old value is thrown away.

t₂′ = insert 1 v₁′ t₂

-- Deletion of the mapping for a certain key.

t₃ = delete 2 t₂

-- Conversion of a list of key-value mappings to a tree.

open import Data.List using (_∷_; [])
open import Data.Product as Prod using (_,_; _,′_)

t₄ = fromList ((2 , v₂) ∷ (1 , v₁) ∷ [])

------------------------------------------------------------------------
-- Queries

-- Let us formulate queries as unit tests.

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

-- Searching for a key.

open import Data.Bool using (true; false)
open import Data.Maybe as Maybe using (just; nothing)

q₀ : lookup 2 t₂ ≡ just v₂
q₀ = refl

q₁ : lookup 2 t₃ ≡ nothing
q₁ = refl

q₂ : 3 ∈? t₂ ≡ false
q₂ = refl

q₃ : 1 ∈? t₄ ≡ true
q₃ = refl

-- Turning a tree into a sorted list of key-value pairs.

q₄ : toList t₁ ≡ (2 , v₂) ∷ []
q₄ = refl

q₅ : toList t₂ ≡ (1 , v₁) ∷ (2 , v₂) ∷ []
q₅ = refl

q₅′ : toList t₂′ ≡ (1 , v₁′) ∷ (2 , v₂) ∷ []
q₅′ = refl

------------------------------------------------------------------------
-- Views

-- Partitioning a tree into the smallest element plus the rest, or the
-- largest element plus the rest.

open import Function using (id)

v₆ : headTail t₀ ≡ nothing
v₆ = refl

v₇ : Maybe.map (Prod.map id toList) (headTail t₂) ≡
     just ((1 , v₁) , ((2 , v₂) ∷ []))
v₇ = refl

v₈ : initLast t₀ ≡ nothing
v₈ = refl

v₉ : Maybe.map (Prod.map toList id) (initLast t₄) ≡
     just (((1 , v₁) ∷ []) ,′ (2 , v₂))
v₉ = refl

------------------------------------------------------------------------
-- Further reading

-- Variations of the AVL tree module are available:

-- • Finite maps with indexed keys and values.

import Data.AVL.IndexedMap

-- • Finite sets.

import Data.AVL.Sets


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

module _ where

postulate
  _≡_ : {A : Set} → A → A → Set

{-# BUILTIN REWRITE _≡_ #-}

record ⊤ : Set where
  constructor []
open ⊤

postulate
  ID : (Δ : Set) (δ₀ δ₁ : Δ) → Set
  ID⊤ : (δ₀ δ₁ : ⊤) → ID ⊤ δ₀ δ₁ ≡ ⊤
  Id : {Δ : Set} (A : Δ → Set) {δ₀ δ₁ : Δ} (δ₂ : ID Δ δ₀ δ₁) (a₀ : A δ₀) (a₁ : A δ₁) → Set
  ap : {Δ : Set} {A : Δ → Set} (f : (δ : Δ) → A δ) {δ₀ δ₁ : Δ} (δ₂ : ID Δ δ₀ δ₁) → Id A δ₂ (f δ₀) (f δ₁)
  AP : {Θ Δ : Set} (f : Θ → Δ) {t₀ t₁ : Θ} (t₂ : ID Θ t₀ t₁) → ID Δ (f t₀) (f t₁)
  Id-AP : {Θ Δ : Set} (f : Θ → Δ) {t₀ t₁ : Θ} (t₂ : ID Θ t₀ t₁) (A : Δ → Set) (a₀ : A (f t₀)) (a₁ : A (f t₁)) →
    Id A (AP f t₂) a₀ a₁ ≡ Id (λ w → A (f w)) t₂ a₀ a₁
  Copy : Set → Set
  uncopy : {A : Set} → Copy A → A

{-# REWRITE ID⊤ #-}
{-# REWRITE Id-AP #-}

postulate
  utr→ : {Δ : Set} (A : Δ → Set) {δ₀ δ₁ : Δ} (δ₂ : ID Δ δ₀ δ₁) (a₁ a₁' : A δ₁) → Id {⊤} (λ _ → A δ₁) [] a₁ a₁'
  IdU : {Δ : Set} {δ₀ δ₁ : Δ} (δ₂ : ID Δ δ₀ δ₁) (A B : Set) →
    Id {Δ} (λ _ → Set) δ₂ A B ≡ Copy ((b₀ : B) (b₁ : B) → Id {⊤} (λ _ → B) [] b₀ b₁)

{-# REWRITE IdU #-}

postulate
  apU : {Δ : Set} (A : Δ → Set) {δ₀ δ₁ : Δ} (δ₂ : ID Δ δ₀ δ₁) → uncopy (ap A δ₂) ≡ utr→ A δ₂

{-# REWRITE apU #-}

ext: agda


text:
module Data.List.Properties.Pointwise where

open import Data.Nat
open import Data.List
open import Relation.Binary.List.Pointwise hiding (refl; map)
open import Relation.Binary.PropositionalEquality

pointwise-∷ʳ : ∀ {a b ℓ A B P l m x y} → Rel {a} {b} {ℓ} {A} {B} P l m → P x y →
              Rel {a} {b} {ℓ} {A} {B} P (l ∷ʳ x) (m ∷ʳ y)
pointwise-∷ʳ [] q = q ∷ []
pointwise-∷ʳ (x∼y ∷ p) q = x∼y ∷ (pointwise-∷ʳ p q)

{-}
pointwise-[]≔ : ∀ {a b ℓ A B P l m i x y} →
                Rel {a} {b} {ℓ} {A} {B} P l m → (p : l [ i ]= x) → P x y →
                Rel {a} {b} {ℓ} {A} {B} P l (m [ fromℕ ([]=-length l p) ]≔ y)
pointwise-[]≔ r p q z = ?
postulate
pointwise-[]≔ [] () r
pointwise-[]≔ (x∼y ∷ r) here (s≤s z≤n) z = z ∷ r
pointwise-[]≔ (x∼y ∷ r) (there p) (s≤s q) z = subst (λ x → Rel _ _ x) {!!} (x∼y ∷ pointwise-[]≔ r p q z)
-}

pointwise-length : ∀ {a b ℓ A B P l m} → Rel {a} {b} {ℓ} {A} {B} P l m → length l ≡ length m
pointwise-length [] = refl
pointwise-length (x∼y ∷ p) = cong suc (pointwise-length p)


text:
-- Pattern synonyms are now allowed in parameterised modules.
module _ where

module L (A : Set) where
  data List : Set where
    nil : List
    cons : A → List → List
  pattern unit x = cons x nil

data Bool : Set where
  true false : Bool

module LB = L Bool
open LB

init : List → List
init nil = nil
init (unit _) = nil
init (cons x xs) = cons x (init xs)

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

test : init (cons true (unit false)) ≡ unit true
test = refl

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{- COMPLEXITY LANGUAGE -}

open import Preliminaries
open import Preorder-Max

module Complexity where

  data CTp : Set where
    unit : CTp
    nat : CTp
    _->c_ : CTp → CTp → CTp
    _×c_ : CTp → CTp → CTp
    list : CTp → CTp
    bool : CTp
    C : CTp

  -- represent a context as a list of types
  Ctx = List CTp

  -- de Bruijn indices (for free variables)
  data _∈_ : CTp → Ctx → Set where
    i0 : ∀ {Γ τ}
       → τ ∈ (τ :: Γ)
    iS : ∀ {Γ τ τ1}
       → τ ∈ Γ
       → τ ∈ (τ1 :: Γ)

  data _|-_ : Ctx → CTp → Set where
    unit : ∀ {Γ}
         → Γ |- unit
    0C : ∀ {Γ}
       → Γ |- C
    1C : ∀ {Γ}
       → Γ |- C
    plusC : ∀ {Γ}
         → Γ |- C
         → Γ |- C
         → Γ |- C
    var : ∀ {Γ τ}
        → τ ∈ Γ
        → Γ |- τ
    z : ∀ {Γ}
      → Γ |- nat
    suc : ∀ {Γ}
        → (e : Γ |- nat)
        → Γ |- nat
    rec : ∀ {Γ τ}
        → Γ |- nat
        → Γ |- τ
        → (nat :: (τ :: Γ)) |- τ
        → Γ |- τ
    lam : ∀ {Γ τ ρ}
        → (ρ :: Γ) |- τ
        → Γ |- (ρ ->c τ)
    app : ∀ {Γ τ1 τ2}
        → Γ |- (τ2 ->c τ1)
        → Γ |- τ2
        → Γ |- τ1
    prod : ∀ {Γ τ1 τ2}
         → Γ |- τ1
         → Γ |- τ2
         → Γ |- (τ1 ×c τ2)
    l-proj : ∀ {Γ τ1 τ2}
           → Γ |- (τ1 ×c τ2)
           → Γ |- τ1
    r-proj : ∀ {Γ τ1 τ2}
           → Γ |- (τ1 ×c τ2)
           → Γ |- τ2
    nil : ∀ {Γ τ} → Γ |- list τ
    _::c_ : ∀ {Γ τ} → Γ |- τ → Γ |- list τ → Γ |- list τ
    listrec : ∀ {Γ τ τ'} → Γ |- list τ → Γ |- τ' → (τ :: (list τ :: (τ' :: Γ))) |- τ' → Γ |- τ'
    true : ∀ {Γ} → Γ |- bool
    false : ∀ {Γ} → Γ |- bool

  _+C_ : ∀ {Γ τ} → Γ |- C  → Γ |- (C ×c τ)→ Γ |- (C ×c τ)
  c +C e = prod (plusC c (l-proj e)) (r-proj e)

------weakening and substitution lemmas

      -- renaming = variable for variable substitution
      --functional view:
      --avoids induction,
      --some associativity/unit properties for free

  -- read: you can rename Γ' as Γ
  rctx : Ctx → Ctx → Set
  rctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → τ ∈ Γ

  rename-var : ∀ {Γ Γ' τ} → rctx Γ Γ' → τ ∈ Γ' → τ ∈ Γ
  rename-var ρ a = ρ a

  idr : ∀ {Γ} → rctx Γ Γ
  idr x = x

  -- weakening with renaming
  p∙ : ∀ {Γ Γ' τ} → rctx Γ Γ' → rctx (τ :: Γ) Γ'
  p∙ ρ = λ x → iS (ρ x)

  p : ∀ {Γ τ} → rctx (τ :: Γ) Γ
  p = p∙ idr

  _∙rr_ : ∀ {A B C} → rctx A B → rctx B C → rctx A C
  ρ1 ∙rr ρ2 = ρ1 o ρ2

  -- free stuff
  rename-var-ident : ∀ {Γ τ} → (x : τ ∈ Γ) → rename-var idr x == x
  rename-var-ident _ = Refl

  rename-var-∙ : ∀ {A B C τ} → (r1 : rctx A B) (r2 : rctx B C) (x : τ ∈ C)
              → rename-var r1 (rename-var r2 x) == rename-var (r1 ∙rr r2) x
  rename-var-∙ _ _ _ = Refl

  ∙rr-assoc : ∀ {A B C D} → (r1 : rctx A B) (r2 : rctx B C) (r3 : rctx C D) → _==_ {_} {rctx A D} (r1 ∙rr (r2 ∙rr r3)) ((r1 ∙rr r2) ∙rr r3)
  ∙rr-assoc r1 r2 r3 = Refl

  r-extend : ∀ {Γ Γ' τ} → rctx Γ Γ' → rctx (τ :: Γ) (τ :: Γ')
  r-extend ρ i0 = i0
  r-extend ρ (iS x) = iS (ρ x)

  ren : ∀ {Γ Γ' τ} → Γ' |- τ → rctx Γ Γ' → Γ |- τ
  ren unit ρ = unit
  ren 0C ρ = 0C
  ren 1C ρ = 1C
  ren (plusC e e₁) ρ = plusC (ren e ρ) (ren e₁ ρ)
  ren (var x) ρ = var (ρ x)
  ren z ρ = z
  ren (suc e) ρ = suc (ren e ρ)
  ren (rec e e₁ e₂) ρ = rec (ren e ρ) (ren e₁ ρ) (ren e₂ (r-extend (r-extend ρ)))
  ren (lam e) ρ = lam (ren e (r-extend ρ))
  ren (app e e₁) ρ = app (ren e ρ) (ren e₁ ρ)
  ren (prod e1 e2) ρ = prod (ren e1 ρ) (ren e2 ρ)
  ren (l-proj e) ρ = l-proj (ren e ρ)
  ren (r-proj e) ρ = r-proj (ren e ρ)
  ren nil ρ = nil
  ren (x ::c xs) ρ = ren x ρ ::c ren xs ρ
  ren true ρ = true
  ren false ρ = false
  ren (listrec e e₁ e₂) ρ = listrec (ren e ρ) (ren e₁ ρ) (ren e₂ (r-extend (r-extend (r-extend ρ))))

  extend-ren-comp-lemma : ∀ {Γ Γ' Γ'' τ τ'} → (x : τ ∈ τ' :: Γ'') (ρ1 : rctx Γ Γ') (ρ2 : rctx Γ' Γ'')
                        → Id {_} {_} ((r-extend ρ1 ∙rr r-extend ρ2) x) (r-extend (ρ1 ∙rr ρ2) x)
  extend-ren-comp-lemma i0 ρ1 ρ2 = Refl
  extend-ren-comp-lemma (iS x) ρ1 ρ2 = Refl

  extend-ren-comp : ∀ {Γ Γ' Γ'' τ} → (ρ1 : rctx Γ Γ') → (ρ2 : rctx Γ' Γ'')
                  → Id {_} {rctx (τ :: Γ) (τ :: Γ'')} (r-extend ρ1 ∙rr r-extend ρ2) (r-extend (ρ1 ∙rr ρ2))
  extend-ren-comp ρ1 ρ2 = λ=i (λ τ → λ= (λ x → extend-ren-comp-lemma x ρ1 ρ2))

  ren-comp : ∀ {Γ Γ' Γ'' τ} → (ρ1 : rctx Γ Γ') → (ρ2 : rctx Γ' Γ'') → (e : Γ'' |- τ)
           → (ren (ren e ρ2) ρ1) == (ren e (ρ1 ∙rr ρ2))
  ren-comp ρ1 ρ2 unit = Refl
  ren-comp ρ1 ρ2 0C = Refl
  ren-comp ρ1 ρ2 1C = Refl
  ren-comp ρ1 ρ2 (plusC e e₁) = ap2 plusC (ren-comp ρ1 ρ2 e) (ren-comp ρ1 ρ2 e₁)
  ren-comp ρ1 ρ2 (var x) = ap var (rename-var-∙ ρ1 ρ2 x)
  ren-comp ρ1 ρ2 z = Refl
  ren-comp ρ1 ρ2 (suc e) = ap suc (ren-comp ρ1 ρ2 e)
  ren-comp ρ1 ρ2 (rec e e₁ e₂) = ap3 rec (ren-comp ρ1 ρ2 e) (ren-comp ρ1 ρ2 e₁)
                                     (ap (ren e₂) (ap r-extend (extend-ren-comp ρ1 ρ2) ∘
                                       extend-ren-comp (r-extend ρ1) (r-extend ρ2)) ∘
                                       ren-comp (r-extend (r-extend ρ1)) (r-extend (r-extend ρ2)) e₂)
  ren-comp ρ1 ρ2 (lam e) = ap lam ((ap (ren e) (extend-ren-comp ρ1 ρ2)) ∘ ren-comp (r-extend ρ1) (r-extend ρ2) e)
  ren-comp ρ1 ρ2 (app e e₁) = ap2 app (ren-comp ρ1 ρ2 e) (ren-comp ρ1 ρ2 e₁)
  ren-comp ρ1 ρ2 (prod e e₁) = ap2 prod (ren-comp ρ1 ρ2 e) (ren-comp ρ1 ρ2 e₁)
  ren-comp ρ1 ρ2 (l-proj e) = ap l-proj (ren-comp ρ1 ρ2 e)
  ren-comp ρ1 ρ2 (r-proj e) = ap r-proj (ren-comp ρ1 ρ2 e)
  ren-comp ρ1 ρ2 nil = Refl
  ren-comp ρ1 ρ2 (e ::c e₁) = ap2 _::c_ (ren-comp ρ1 ρ2 e) (ren-comp ρ1 ρ2 e₁)
  ren-comp ρ1 ρ2 (listrec e e₁ e₂) = ap3 listrec (ren-comp ρ1 ρ2 e) (ren-comp ρ1 ρ2 e₁)
                                       (ap (ren e₂) (ap r-extend (ap r-extend (extend-ren-comp ρ1 ρ2)) ∘
                                       (ap r-extend (extend-ren-comp (r-extend ρ1) (r-extend ρ2)) ∘
                                       extend-ren-comp (r-extend (r-extend ρ1)) (r-extend (r-extend ρ2)))) ∘
                                       ren-comp (r-extend (r-extend (r-extend ρ1)))
                                                (r-extend (r-extend (r-extend ρ2))) e₂)
  ren-comp ρ1 ρ2 true = Refl
  ren-comp ρ1 ρ2 false = Refl

  -- weakening a context
  wkn : ∀ {Γ τ1 τ2} → Γ |- τ2 → (τ1 :: Γ) |- τ2
  wkn e = ren e iS

  sctx : Ctx → Ctx → Set
  sctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → Γ |- τ

  --lem2 (addvar)
  s-extend : ∀ {Γ Γ' τ} → sctx Γ Γ' → sctx (τ :: Γ) (τ :: Γ')
  s-extend Θ i0 = var i0
  s-extend Θ (iS x) = wkn (Θ x)

  ids : ∀ {Γ} → sctx Γ Γ
  ids x = var x

    -- weakening with substitution
  q∙ : ∀ {Γ Γ' τ} → sctx Γ Γ' → sctx (τ :: Γ) Γ'
  q∙ Θ = λ x → wkn (Θ x)

  lem3' : ∀ {Γ Γ' τ} → sctx Γ Γ' → Γ |- τ → sctx Γ (τ :: Γ')
  lem3' Θ e i0 = e
  lem3' Θ e (iS i) = Θ i

    --lem3
  q : ∀ {Γ τ} → Γ |- τ → sctx Γ (τ :: Γ)
  q e = lem3' ids e

  -- subst-var
  svar : ∀ {Γ1 Γ2 τ} → sctx Γ1 Γ2 → τ ∈ Γ2 → Γ1 |- τ
  svar Θ i = q (Θ i) i0

  lem4' : ∀ {Γ Γ' τ1 τ2} → sctx Γ Γ' → Γ |- τ1 → Γ |- τ2 → sctx Γ (τ1 :: (τ2 :: Γ'))
  lem4' Θ a b = lem3' (lem3' Θ b) a

  lem4 : ∀ {Γ τ1 τ2} → Γ |- τ1 → Γ |- τ2 → sctx Γ (τ1 :: (τ2 :: Γ))
  lem4 e1 e2 = lem4' ids e1 e2

  lem5' : ∀ {Γ Γ' τ1 τ2 τ3} → sctx Γ Γ' → Γ |- τ1 → Γ |- τ2 → Γ |- τ3 → sctx Γ (τ1 :: (τ2 :: (τ3 :: Γ')))
  lem5' Θ a b c = lem3' (lem3' (lem3' Θ c) b) a

  lem5 : ∀ {Γ τ1 τ2 τ3} → Γ |- τ1 → Γ |- τ2 → Γ |- τ3 → sctx Γ (τ1 :: (τ2 :: (τ3 :: Γ)))
  lem5 e1 e2 e3 = lem5' ids e1 e2 e3

  subst : ∀ {Γ Γ' τ} → Γ' |- τ → sctx Γ Γ' → Γ |- τ
  subst unit Θ = unit
  subst 0C Θ = 0C
  subst 1C Θ = 1C
  subst (plusC e e₁) Θ = plusC (subst e Θ) (subst e₁ Θ)
  subst (var x) Θ = Θ x
  subst z Θ = z
  subst (suc e) Θ = suc (subst e Θ)
  subst (rec e e₁ e₂) Θ = rec (subst e Θ) (subst e₁ Θ) (subst e₂ (s-extend (s-extend Θ)))
  subst (lam e) Θ = lam (subst e (s-extend Θ))
  subst (app e e₁) Θ = app (subst e Θ) (subst e₁ Θ)
  subst (prod e1 e2) Θ = prod (subst e1 Θ) (subst e2 Θ)
  subst (l-proj e) Θ = l-proj (subst e Θ)
  subst (r-proj e) Θ = r-proj (subst e Θ)
  subst nil Θ = nil
  subst (x ::c xs) Θ = subst x Θ ::c subst xs Θ
  subst true Θ = true
  subst false Θ = false
  subst (listrec e e₁ e₂) Θ = listrec (subst e Θ) (subst e₁ Θ) (subst e₂ (s-extend (s-extend (s-extend Θ))))

  subst1 : ∀ {Γ τ τ1} → Γ |- τ1 → (τ1 :: Γ) |- τ → Γ |- τ
  subst1 e e' = subst e' (q e)

  _rs_ : ∀ {A B C} → rctx A B → sctx B C → sctx A C
  _rs_ ρ Θ x = ren (subst (var x) Θ) ρ

  _ss_ : ∀ {A B C} → sctx A B → sctx B C → sctx A C
  _ss_ Θ1 Θ2 x = subst (subst (var x) Θ2) Θ1

  _sr_ : ∀ {A B C} → sctx A B → rctx B C → sctx A C
  _sr_ Θ ρ x = subst (ren (var x) ρ) Θ

  --free stuff
  svar-rs : ∀ {A B C τ} (ρ : rctx A B) (Θ : sctx B C) (x : τ ∈ C)
          → svar (ρ rs Θ) x == ren (svar Θ x) ρ
  svar-rs = λ ρ Θ x → Refl

  svar-ss : ∀ {A B C τ} (Θ1 : sctx A B) (Θ2 : sctx B C) (x : τ ∈ C)
          → svar (Θ1 ss Θ2) x == subst (svar Θ2 x) Θ1
  svar-ss = λ Θ1 Θ2 x → Refl

  svar-sr : ∀ {A B C τ} (Θ : sctx A B) (ρ : rctx B C) (x : τ ∈ C)
          → svar Θ (rename-var ρ x) == svar (Θ sr ρ) x
  svar-sr = λ Θ ρ x → Refl

  svar-id : ∀ {Γ τ} → (x : τ ∈ Γ) → var x == svar ids x
  svar-id = λ x → Refl

  rsr-assoc : ∀ {A B C D} → (ρ1 : rctx A B) (Θ : sctx B C) (ρ2 : rctx C D)
            → Id {_} {sctx A D} ((ρ1 rs Θ) sr ρ2) (ρ1 rs (Θ sr ρ2))
  rsr-assoc = λ ρ1 Θ ρ2 → Refl

  extend-id-once-lemma : ∀ {Γ τ τ'} → (x : τ ∈ τ' :: Γ) → _==_ {_} {τ' :: Γ |- τ}
                       (ids {τ' :: Γ} {τ} x) (s-extend {Γ} {Γ} {τ'} (ids {Γ}) {τ} x)
  extend-id-once-lemma i0 = Refl
  extend-id-once-lemma (iS x) = Refl

  extend-id-once : ∀ {Γ τ} → Id {_} {sctx (τ :: Γ) (τ :: Γ)} (ids {τ :: Γ}) (s-extend ids)
  extend-id-once = λ=i (λ τ → λ= (λ x → extend-id-once-lemma x))

  extend-id-twice : ∀ {Γ τ1 τ2} → Id {_} {sctx (τ1 :: τ2 :: Γ) (τ1 :: τ2 :: Γ)} (ids {τ1 :: τ2 :: Γ}) (s-extend (s-extend ids))
  extend-id-twice = ap s-extend extend-id-once ∘ extend-id-once

  subst-id : ∀ {Γ τ} (e : Γ |- τ) → e == subst e ids
  subst-id unit = Refl
  subst-id 0C = Refl
  subst-id 1C = Refl
  subst-id (plusC e e₁) = ap2 plusC (subst-id e) (subst-id e₁)
  subst-id (var x) = svar-id x
  subst-id z = Refl
  subst-id (suc e) = ap suc (subst-id e)
  subst-id (rec e e₁ e₂) = ap3 rec (subst-id e) (subst-id e₁) (ap (subst e₂) extend-id-twice ∘ subst-id e₂)
  subst-id (lam e) = ap lam (ap (subst e) extend-id-once ∘ subst-id e)
  subst-id (app e e₁) = ap2 app (subst-id e) (subst-id e₁)
  subst-id (prod e e₁) = ap2 prod (subst-id e) (subst-id e₁)
  subst-id (l-proj e) = ap l-proj (subst-id e)
  subst-id (r-proj e) = ap r-proj (subst-id e)
  subst-id nil = Refl
  subst-id (e ::c e₁) = ap2 _::c_ (subst-id e) (subst-id e₁)
  subst-id true = Refl
  subst-id false = Refl
  subst-id (listrec e e₁ e₂) = ap3 listrec (subst-id e) (subst-id e₁) (ap (subst e₂) (ap s-extend (ap s-extend extend-id-once) ∘ extend-id-twice) ∘ subst-id e₂)

  extend-rs-once-lemma : ∀ {A B C τ τ'} → (x : τ ∈ τ' :: B) (ρ : rctx C A) (Θ : sctx A B) → _==_ {_} {τ' :: C |- τ}
                       (_rs_ {τ' :: C} {τ' :: A} {τ' :: B} (r-extend {C} {A} {τ'} ρ)
                         (s-extend {A} {B} {τ'} Θ) {τ} x)
                         (s-extend {C} {B} {τ'} (_rs_ {C} {A} {B} ρ Θ) {τ} x)
  extend-rs-once-lemma i0 ρ Θ = Refl
  extend-rs-once-lemma (iS x) ρ Θ = ! (ren-comp iS ρ (Θ x)) ∘ ren-comp (r-extend ρ) iS (Θ x)

  extend-rs-once : ∀ {A B C τ} → (ρ : rctx C A) (Θ : sctx A B)
                 → Id {_} {sctx (τ :: C) (τ :: B)} (r-extend ρ rs s-extend Θ) (s-extend (ρ rs Θ))
  extend-rs-once ρ Θ = λ=i (λ τ → λ= (λ x → extend-rs-once-lemma x ρ Θ))

  extend-rs-twice : ∀ {A B C τ τ'} → (ρ : rctx C A) (Θ : sctx A B)
                  → Id {_} {sctx (τ :: τ' :: C) (τ :: τ' :: B)} ((r-extend (r-extend ρ)) rs (s-extend (s-extend Θ))) ((s-extend (s-extend (ρ rs Θ))))
  extend-rs-twice ρ Θ = ap s-extend (extend-rs-once ρ Θ) ∘ extend-rs-once (r-extend ρ) (s-extend Θ)

  subst-rs : ∀ {A B C τ} → (ρ : rctx C A) (Θ : sctx A B) (e : B |- τ)
           → ren (subst e Θ) ρ == subst e (ρ rs Θ)
  subst-rs ρ Θ unit = Refl
  subst-rs ρ Θ 0C = Refl
  subst-rs ρ Θ 1C = Refl
  subst-rs ρ Θ (plusC e e₁) = ap2 plusC (subst-rs ρ Θ e) (subst-rs ρ Θ e₁)
  subst-rs ρ Θ (var x) = svar-rs ρ Θ x
  subst-rs ρ Θ z = Refl
  subst-rs ρ Θ (suc e) = ap suc (subst-rs ρ Θ e)
  subst-rs ρ Θ (rec e e₁ e₂) = ap3 rec (subst-rs ρ Θ e) (subst-rs ρ Θ e₁)
                                 (ap (subst e₂) (extend-rs-twice ρ Θ) ∘
                                 subst-rs (r-extend (r-extend ρ)) (s-extend (s-extend Θ)) e₂)
  subst-rs ρ Θ (lam e) = ap lam (ap (subst e) (extend-rs-once ρ Θ) ∘ subst-rs (r-extend ρ) (s-extend Θ) e)
  subst-rs ρ Θ (app e e₁) = ap2 app (subst-rs ρ Θ e) (subst-rs ρ Θ e₁)
  subst-rs ρ Θ (prod e e₁) = ap2 prod (subst-rs ρ Θ e) (subst-rs ρ Θ e₁)
  subst-rs ρ Θ (l-proj e) = ap l-proj (subst-rs ρ Θ e)
  subst-rs ρ Θ (r-proj e) = ap r-proj (subst-rs ρ Θ e)
  subst-rs ρ Θ nil = Refl
  subst-rs ρ Θ (e ::c e₁) = ap2 _::c_ (subst-rs ρ Θ e) (subst-rs ρ Θ e₁)
  subst-rs ρ Θ true = Refl
  subst-rs ρ Θ false = Refl
  subst-rs ρ Θ (listrec e e₁ e₂) = ap3 listrec (subst-rs ρ Θ e) (subst-rs ρ Θ e₁)
                                       (ap (subst e₂) (ap s-extend (ap s-extend (extend-rs-once ρ Θ)) ∘
                                       extend-rs-twice (r-extend ρ) (s-extend Θ)) ∘
                                       subst-rs (r-extend (r-extend (r-extend ρ))) (s-extend (s-extend (s-extend Θ))) e₂)

  rs-comp : ∀ {Γ Γ' Γ'' τ} → (ρ : rctx Γ Γ') → (Θ : sctx Γ' Γ'') → (e : Γ'' |- τ)
          → (ren (subst e Θ) ρ) == subst e (ρ rs Θ)
  rs-comp ρ Θ unit = Refl
  rs-comp ρ Θ 0C = Refl
  rs-comp ρ Θ 1C = Refl
  rs-comp ρ Θ (plusC e e₁) = ap2 plusC (rs-comp ρ Θ e) (rs-comp ρ Θ e₁)
  rs-comp ρ Θ (var x) = svar-rs ρ Θ x
  rs-comp ρ Θ z = Refl
  rs-comp ρ Θ (suc e) = ap suc (rs-comp ρ Θ e)
  rs-comp ρ Θ (rec e e₁ e₂) = ap3 rec (rs-comp ρ Θ e) (rs-comp ρ Θ e₁)
                              (ap (subst e₂) (extend-rs-twice ρ Θ) ∘ rs-comp (r-extend (r-extend ρ)) (s-extend (s-extend Θ)) e₂)
  rs-comp ρ Θ (lam e) = ap lam (ap (subst e) (extend-rs-once ρ Θ) ∘ rs-comp (r-extend ρ) (s-extend Θ) e)
  rs-comp ρ Θ (app e e₁) = ap2 app (rs-comp ρ Θ e) (rs-comp ρ Θ e₁)
  rs-comp ρ Θ (prod e e₁) = ap2 prod (rs-comp ρ Θ e) (rs-comp ρ Θ e₁)
  rs-comp ρ Θ (l-proj e) = ap l-proj (rs-comp ρ Θ e)
  rs-comp ρ Θ (r-proj e) = ap r-proj (rs-comp ρ Θ e)
  rs-comp ρ Θ nil = Refl
  rs-comp ρ Θ (e ::c e₁) = ap2 _::c_ (rs-comp ρ Θ e) (rs-comp ρ Θ e₁)
  rs-comp ρ Θ (listrec e e₁ e₂) = ap3 listrec (rs-comp ρ Θ e) (rs-comp ρ Θ e₁)
                                    (ap (subst e₂) (ap s-extend (ap s-extend (extend-rs-once ρ Θ)) ∘
                                    extend-rs-twice (r-extend ρ) (s-extend Θ)) ∘
                                    rs-comp (r-extend (r-extend (r-extend ρ)))
                                    (s-extend (s-extend (s-extend Θ))) e₂)
  rs-comp ρ Θ true = Refl
  rs-comp ρ Θ false = Refl

  extend-sr-once-lemma : ∀ {A B C τ τ'} → (Θ : sctx A B) (ρ : rctx B C) (x : τ ∈ τ' :: C)
                       → _==_ {_} {τ' :: A |- τ} (s-extend (_sr_ Θ ρ) x) (_sr_ (s-extend Θ) (r-extend ρ) x)
  extend-sr-once-lemma Θ ρ i0 = Refl
  extend-sr-once-lemma Θ ρ (iS x) = Refl

  extend-sr-once : ∀ {A B C τ} → (Θ : sctx A B) (ρ : rctx B C)
                 → Id {_} {sctx (τ :: A) (τ :: C)} (s-extend Θ sr r-extend ρ) (s-extend (Θ sr ρ))
  extend-sr-once Θ ρ = λ=i (λ τ → λ= (λ x → ! (extend-sr-once-lemma Θ ρ x)))

  extend-sr-twice : ∀ {A B C τ τ'} → (Θ : sctx A B) (ρ : rctx B C)
                 → Id {_} {sctx (τ' :: τ :: A) (τ' :: τ :: C)}
                   (s-extend (s-extend Θ) sr r-extend (r-extend ρ)) (s-extend (s-extend (Θ sr ρ)))
  extend-sr-twice Θ ρ = ap s-extend (extend-sr-once Θ ρ) ∘ extend-sr-once (s-extend Θ) (r-extend ρ)

  sr-comp : ∀ {Γ Γ' Γ'' τ} → (Θ : sctx Γ Γ') → (ρ : rctx Γ' Γ'') → (e : Γ'' |- τ)
          → (subst (ren e ρ) Θ) == subst e (Θ sr ρ)
  sr-comp Θ ρ unit = Refl
  sr-comp Θ ρ 0C = Refl
  sr-comp Θ ρ 1C = Refl
  sr-comp Θ ρ (plusC e e₁) = ap2 plusC (sr-comp Θ ρ e) (sr-comp Θ ρ e₁)
  sr-comp Θ ρ (var x) = svar-sr Θ ρ x
  sr-comp Θ ρ z = Refl
  sr-comp Θ ρ (suc e) = ap suc (sr-comp Θ ρ e)
  sr-comp Θ ρ (rec e e₁ e₂) = ap3 rec (sr-comp Θ ρ e) (sr-comp Θ ρ e₁)
                                      (ap (subst e₂) (ap s-extend (extend-sr-once Θ ρ) ∘
                                      extend-sr-once (s-extend Θ) (r-extend ρ)) ∘
                                      sr-comp (s-extend (s-extend Θ)) (r-extend (r-extend ρ)) e₂)
  sr-comp Θ ρ (lam e) = ap lam (ap (subst e) (extend-sr-once Θ ρ) ∘ sr-comp (s-extend Θ) (r-extend ρ) e)
  sr-comp Θ ρ (app e e₁) = ap2 app (sr-comp Θ ρ e) (sr-comp Θ ρ e₁)
  sr-comp Θ ρ (prod e e₁) = ap2 prod (sr-comp Θ ρ e) (sr-comp Θ ρ e₁)
  sr-comp Θ ρ (l-proj e) = ap l-proj (sr-comp Θ ρ e)
  sr-comp Θ ρ (r-proj e) = ap r-proj (sr-comp Θ ρ e)
  sr-comp Θ ρ nil = Refl
  sr-comp Θ ρ (e ::c e₁) = ap2 _::c_ (sr-comp Θ ρ e) (sr-comp Θ ρ e₁)
  sr-comp Θ ρ (listrec e e₁ e₂) = ap3 listrec (sr-comp Θ ρ e) (sr-comp Θ ρ e₁)
                                              (ap (subst e₂) (ap s-extend (ap s-extend (extend-sr-once Θ ρ)) ∘
                                              extend-sr-twice (s-extend Θ) (r-extend ρ)) ∘
                                                 sr-comp (s-extend (s-extend (s-extend Θ)))
                                                 (r-extend (r-extend (r-extend ρ))) e₂)

  sr-comp Θ ρ true = Refl
  sr-comp Θ ρ false = Refl

  extend-ss-once-lemma : ∀ {A B C τ τ'} → (Θ1 : sctx A B) (Θ2 : sctx B C) (x : τ ∈ τ' :: C)
                       → _==_ {_} {τ' :: A |- τ} (s-extend (_ss_ Θ1 Θ2) x) (_ss_ (s-extend Θ1) (s-extend Θ2) x)
  extend-ss-once-lemma Θ1 Θ2 i0 = Refl
  extend-ss-once-lemma Θ1 Θ2 (iS x) = ! (sr-comp (s-extend Θ1) iS (Θ2 x)) ∘ rs-comp iS Θ1 (Θ2 x)

  extend-ss-once : ∀ {A B C τ} → (Θ1 : sctx A B) (Θ2 : sctx B C)
              → _==_ {_} {sctx (τ :: A) (τ :: C)} (s-extend (Θ1 ss Θ2))
              ((s-extend Θ1) ss
              (s-extend Θ2))
  extend-ss-once Θ1 Θ2 = λ=i (λ τ → λ= (λ x → extend-ss-once-lemma Θ1 Θ2 x))

  subst-ss : ∀ {A B C τ} → (Θ1 : sctx A B) (Θ2 : sctx B C) (e : C |- τ)
           → subst e (Θ1 ss Θ2) == subst (subst e Θ2) Θ1
  subst-ss Θ1 Θ2 unit = Refl
  subst-ss Θ1 Θ2 0C = Refl
  subst-ss Θ1 Θ2 1C = Refl
  subst-ss Θ1 Θ2 (plusC e e₁) = ap2 plusC (subst-ss Θ1 Θ2 e) (subst-ss Θ1 Θ2 e₁)
  subst-ss Θ1 Θ2 (var x) = svar-ss Θ1 Θ2 x
  subst-ss Θ1 Θ2 z = Refl
  subst-ss Θ1 Θ2 (suc e) = ap suc (subst-ss Θ1 Θ2 e)
  subst-ss Θ1 Θ2 (rec e e₁ e₂) = ap3 rec (subst-ss Θ1 Θ2 e) (subst-ss Θ1 Θ2 e₁)
                                 (subst-ss (s-extend (s-extend Θ1)) (s-extend (s-extend Θ2)) e₂ ∘
                                 ap (subst e₂) (extend-ss-once (s-extend Θ1) (s-extend Θ2) ∘
                                 ap s-extend (extend-ss-once Θ1 Θ2)))
  subst-ss Θ1 Θ2 (lam e) = ap lam (subst-ss (s-extend Θ1) (s-extend Θ2) e ∘ ap (subst e) (extend-ss-once Θ1 Θ2))
  subst-ss Θ1 Θ2 (app e e₁) = ap2 app (subst-ss Θ1 Θ2 e) (subst-ss Θ1 Θ2 e₁)
  subst-ss Θ1 Θ2 (prod e e₁) = ap2 prod (subst-ss Θ1 Θ2 e) (subst-ss Θ1 Θ2 e₁)
  subst-ss Θ1 Θ2 (l-proj e) = ap l-proj (subst-ss Θ1 Θ2 e)
  subst-ss Θ1 Θ2 (r-proj e) = ap r-proj (subst-ss Θ1 Θ2 e)
  subst-ss Θ1 Θ2 nil = Refl
  subst-ss Θ1 Θ2 (e ::c e₁) = ap2 _::c_ (subst-ss Θ1 Θ2 e) (subst-ss Θ1 Θ2 e₁)
  subst-ss Θ1 Θ2 true = Refl
  subst-ss Θ1 Θ2 false = Refl
  subst-ss Θ1 Θ2 (listrec e e₁ e₂) = ap3 listrec (subst-ss Θ1 Θ2 e) (subst-ss Θ1 Θ2 e₁)
                                     (subst-ss (s-extend (s-extend (s-extend Θ1))) (s-extend (s-extend (s-extend Θ2))) e₂ ∘
                                     ap (subst e₂) (extend-ss-once (s-extend (s-extend Θ1)) (s-extend (s-extend Θ2)) ∘
                                     ap s-extend (extend-ss-once (s-extend Θ1) (s-extend Θ2) ∘
                                     ap s-extend (extend-ss-once Θ1 Θ2))))

  throw : ∀ {Γ Γ' τ} → sctx Γ (τ :: Γ') → sctx Γ Γ'
  throw Θ x = Θ (iS x)

  fuse1 : ∀ {Γ Γ' τ τ'} (v : Γ |- τ') (Θ : sctx Γ Γ') (x : τ ∈ Γ') → (q v ss q∙ Θ) x == Θ x
  fuse1 v Θ x = subst (ren (Θ x) iS) (q v) =⟨ sr-comp (q v) iS (Θ x) ⟩
                subst (Θ x) (q v sr iS) =⟨ Refl ⟩
                subst (Θ x) ids =⟨ ! (subst-id (Θ x)) ⟩
                (Θ x ∎)

  subst-compose-lemma-lemma : ∀ {Γ Γ' τ τ'} (v : Γ |- τ') (Θ : sctx Γ Γ') (x : τ ∈ τ' :: Γ')
                            → _==_ {_} {Γ |- τ} (_ss_ (q v) (s-extend Θ) x) (lem3' Θ v x)
  subst-compose-lemma-lemma v Θ i0 = Refl
  subst-compose-lemma-lemma v Θ (iS x) = fuse1 v Θ x

  subst-compose-lemma : ∀ {Γ Γ' τ} (v : Γ |- τ) (Θ : sctx Γ Γ')
                      → _==_ {_} {sctx Γ (τ :: Γ')} ((q v) ss (s-extend Θ)) (lem3' Θ v)
  subst-compose-lemma v Θ = λ=i (λ τ → λ= (λ x → subst-compose-lemma-lemma v Θ x))

  subst-compose : ∀ {Γ Γ' τ τ1} (Θ : sctx Γ Γ') (v : Γ |- τ) (e : (τ :: Γ' |- τ1) )
                → subst (subst e (s-extend Θ)) (q v) == subst e (lem3' Θ v)
  subst-compose Θ v e = ap (subst e) (subst-compose-lemma v Θ) ∘ (! (subst-ss (q v) (s-extend Θ) e))

  fuse2 : ∀ {Γ Γ' τ τ1 τ2} (v1 : Γ |- τ1) (v2 : Γ |- τ2) (Θ : sctx Γ Γ') (x : τ ∈ τ2 :: Γ')
        → (lem4 v1 v2 ss throw (s-extend (s-extend Θ))) x == (lem3' Θ v2) x
  fuse2 v1 v2 Θ x = subst (ren (s-extend Θ x) iS) (lem4 v1 v2) =⟨ sr-comp (lem4 v1 v2) iS (s-extend Θ x) ⟩
                    subst (s-extend Θ x) (lem4 v1 v2 sr iS) =⟨ Refl ⟩
                    subst (s-extend Θ x) (lem3' ids v2) =⟨ subst-compose-lemma-lemma v2 Θ x ⟩
                    (lem3' Θ v2 x ∎)

  subst-compose2-lemma-lemma : ∀ {Γ Γ' τ τ1 τ2 τ'} (v1 : Γ |- τ1) (v2 : Γ |- τ2) (e1 : τ1 :: τ2 :: Γ' |- τ) (Θ : sctx Γ Γ') (x : τ' ∈ τ1 :: τ2 :: Γ')
                             → _==_ {_} {_} ((lem4 v1 v2 ss s-extend (s-extend Θ)) x) (lem4' Θ v1 v2 x)
  subst-compose2-lemma-lemma v1 v2 e1 Θ i0 = Refl
  subst-compose2-lemma-lemma v1 v2 e1 Θ (iS x) = fuse2 v1 v2 Θ x

  subst-compose2-lemma : ∀ {Γ Γ' τ τ1 τ2} (v1 : Γ |- τ1) (v2 : Γ |- τ2) (e1 : τ1 :: τ2 :: Γ' |- τ) (Θ : sctx Γ Γ')
                       → _==_ {_} {sctx Γ (τ1 :: τ2 :: Γ')} (lem4 v1 v2 ss s-extend (s-extend Θ)) (lem4' Θ v1 v2)
  subst-compose2-lemma v1 v2 e1 Θ = λ=i (λ τ → λ= (λ x → subst-compose2-lemma-lemma v1 v2 e1 Θ x))

  fuse3 : ∀ {Γ Γ' τ1 τ2 τ'} (Θ : sctx Γ Γ') (v1 : Γ' |- τ1) (v2 : Γ' |- τ2) (x : τ' ∈ τ2 :: Γ')
          → subst (lem3' ids v2 x) Θ == lem3' Θ (subst v2 Θ) x
  fuse3 Θ v1 v2 i0 = Refl
  fuse3 Θ v1 v2 (iS x) = Refl

  subst-compose3-lemma-lemma : ∀ {Γ Γ' τ τ1 τ2 τ'} (Θ : sctx Γ Γ') (e1 : (τ1 :: (τ2 :: Γ')) |- τ) (v1 : Γ' |- τ1) (v2 : Γ' |- τ2) (x : τ' ∈ τ1 :: τ2 :: Γ')
                             → _==_ {_} {_} ((Θ ss lem4 v1 v2) x) (lem4' Θ (subst v1 Θ) (subst v2 Θ) x)
  subst-compose3-lemma-lemma Θ e1 v1 v2 i0 = Refl
  subst-compose3-lemma-lemma Θ e1 v1 v2 (iS x) = fuse3 Θ v1 v2 x

  subst-compose3-lemma : ∀ {Γ Γ' τ τ1 τ2} (Θ : sctx Γ Γ') (e1 : (τ1 :: (τ2 :: Γ')) |- τ) (v1 : Γ' |- τ1) (v2 : Γ' |- τ2)
                      → _==_ {_} {sctx Γ (τ1 :: τ2 :: Γ')} (Θ ss lem4 v1 v2) (lem4' Θ (subst v1 Θ) (subst v2 Θ))
  subst-compose3-lemma Θ e1 v1 v2 = λ=i (λ τ → λ= (λ x → subst-compose3-lemma-lemma Θ e1 v1 v2 x))

  subst-compose2 : ∀ {Γ Γ' τ τ1 τ2} (Θ : sctx Γ Γ') (e1 : (τ1 :: (τ2 :: Γ')) |- τ) (v1 : Γ |- τ1) (v2 : Γ |- τ2)
                 → subst (subst e1 (s-extend (s-extend Θ))) (lem4 v1 v2) == subst e1 (lem4' Θ v1 v2)
  subst-compose2 Θ e1 v1 v2 = ap (subst e1) (subst-compose2-lemma v1 v2 e1 Θ) ∘
                           ! (subst-ss (lem4 v1 v2) (s-extend (s-extend Θ)) e1)

  subst-compose3 : ∀ {Γ Γ' τ τ1 τ2} (Θ : sctx Γ Γ') (e1 : (τ1 :: (τ2 :: Γ')) |- τ) (v1 : Γ' |- τ1) (v2 : Γ' |- τ2)
                 → subst (subst e1 (lem4 v1 v2)) Θ == subst e1 (lem4' Θ (subst v1 Θ) (subst v2 Θ))
  subst-compose3 Θ e1 v1 v2 = ap (subst e1) (subst-compose3-lemma Θ e1 v1 v2) ∘ ! (subst-ss Θ (lem4 v1 v2) e1)

  subst-compose4 : ∀ {Γ Γ' τ} (Θ : sctx Γ Γ') (v' : Γ |- nat) (r : Γ |- τ) (e2 : (nat :: (τ :: Γ')) |- τ)
                 → subst (subst e2 (s-extend (s-extend Θ))) (lem4 v' r) == subst e2 (lem4' Θ v' r)
  subst-compose4 Θ v' r e2 = subst-compose2 Θ e2 v' r

  fuse4-lemma : ∀ {Γ Γ' τ τ1 τ2 τ3} (v1 : Γ |- τ1) (v2 : Γ |- τ2) (v3 : Γ |- τ3) (Θ : sctx Γ Γ') (x : τ ∈ Γ')
              → (lem3' (lem3' ids v3) v2 ss q∙ (q∙ Θ)) x == Θ x
  fuse4-lemma v1 v2 v3 Θ x = subst (ren (wkn (Θ x)) iS) (lem3' (q v3) v2) =⟨ sr-comp (lem3' (q v3) v2) iS (wkn (Θ x)) ⟩
                             subst (wkn (Θ x)) (lem3' (q v3) v2 sr iS) =⟨ Refl ⟩
                             subst (ren (Θ x) iS) (lem3' (q v3) v2 sr iS) =⟨ sr-comp (lem3' (q v3) v2 sr iS) iS (Θ x) ⟩
                             subst (Θ x) ((lem3' (q v3) v2 sr iS) sr iS) =⟨ Refl ⟩
                             subst (Θ x) ids =⟨ ! (subst-id (Θ x)) ⟩
                             (Θ x ∎)

  fuse4 : ∀ {Γ Γ' τ τ1 τ2 τ3} (v1 : Γ |- τ1) (v2 : Γ |- τ2) (v3 : Γ |- τ3) (Θ : sctx Γ Γ') (x : τ ∈ τ2 :: τ3 :: Γ')
        → subst (s-extend (s-extend Θ) x) (lem3' (lem3' ids v3) v2) == lem3' (lem3' Θ v3) v2 x
  fuse4 v1 v2 v3 Θ i0 = Refl
  fuse4 v1 v2 v3 Θ (iS i0) = Refl
  fuse4 v1 v2 v3 Θ (iS (iS x)) = subst (wkn (wkn (Θ x))) (lem3' (lem3' ids v3) v2) =⟨ subst-ss (lem3' (lem3' ids v3) v2) (q∙ (q∙ Θ)) (var x) ⟩
                                 subst (var x) (lem3' (lem3' ids v3) v2 ss q∙ (q∙ Θ)) =⟨ fuse4-lemma v1 v2 v3 Θ x ⟩
                                 subst (var x) Θ =⟨ Refl ⟩
                                 (Θ x ∎)

  subst-compose5-lemma-lemma : ∀ {Γ Γ' τ τ1 τ2 τ3 τ'} (v1 : Γ |- τ1) (v2 : Γ |- τ2) (v3 : Γ |- τ3) (e1 : τ1 :: τ2 :: τ3 :: Γ' |- τ) (Θ : sctx Γ Γ') (x : τ' ∈ τ1 :: τ2 :: τ3 :: Γ')
                             → _==_ {_} {_} ((lem5 v1 v2 v3 ss s-extend (s-extend (s-extend Θ))) x) (lem5' Θ v1 v2 v3 x)
  subst-compose5-lemma-lemma v1 v2 v3 e Θ i0 = Refl
  subst-compose5-lemma-lemma v1 v2 v3 e Θ (iS x) = (lem5 v1 v2 v3 ss s-extend (s-extend (s-extend Θ))) (iS x) =⟨ sr-comp (lem5 v1 v2 v3) iS (s-extend (s-extend Θ) x) ⟩
                                                   subst (s-extend (s-extend Θ) x) (lem3' (lem3' ids v3) v2) =⟨ fuse4 v1 v2 v3 Θ x ⟩
                                                   (lem3' (lem3' Θ v3) v2 x ∎)

  subst-compose5-lemma : ∀ {Γ Γ' τ τ1 τ2 τ3} (v1 : Γ |- τ1) (v2 : Γ |- τ2) (v3 : Γ |- τ3) (e : τ1 :: τ2 :: τ3 :: Γ' |- τ) (Θ : sctx Γ Γ')
                       → _==_ {_} {sctx Γ (τ1 :: τ2 :: τ3 :: Γ')} (lem5 v1 v2 v3 ss (s-extend (s-extend (s-extend Θ)))) (lem5' Θ v1 v2 v3)
  subst-compose5-lemma v1 v2 v3 e Θ = λ=i (λ τ → λ= (λ x → subst-compose5-lemma-lemma v1 v2 v3 e Θ x))

  subst-compose5 : ∀ {Γ Γ' τ τ1 τ2 τ3} (Θ : sctx Γ Γ') (e : (τ1 :: (τ2 :: (τ3 :: Γ'))) |- τ) (v1 : Γ |- τ1) (v2 : Γ |- τ2) (v3 : Γ |- τ3)
                 → subst (subst e (s-extend (s-extend (s-extend (Θ))))) (lem5 v1 v2 v3) == subst e (lem5' Θ v1 v2 v3)
  subst-compose5 Θ e v1 v2 v3 = ap (subst e) (subst-compose5-lemma v1 v2 v3 e Θ) ∘
                                ! (subst-ss (lem5 v1 v2 v3) (s-extend (s-extend (s-extend Θ))) e)

-------

  -- define 'stepping' as a datatype (fig. 1 of proof)
  data _≤s_ : ∀ {Γ T} → Γ |- T → Γ |- T → Set where
    refl-s : ∀ {Γ T}
           → {e : Γ |- T}
           → e ≤s e
    trans-s : ∀ {Γ T}
            → {e e' e'' : Γ |- T}
            → e ≤s e' → e' ≤s e''
            → e ≤s e''
    plus-s : ∀ {Γ}
           → {e1 e2 n1 n2 : Γ |- C}
           → e1 ≤s n1 → e2 ≤s n2
           → (plusC e1 e2) ≤s (plusC n1 n2)
    cong-refl : ∀ {Γ τ} {e e' : Γ |- τ} → e == e' → e ≤s e'
    +-unit-l : ∀ {Γ} {e : Γ |- C} → (plusC 0C e) ≤s e
    +-unit-l' : ∀ {Γ} {e : Γ |- C} → e ≤s (plusC 0C e)
    +-unit-r : ∀ {Γ} {e : Γ |- C} → (plusC e 0C) ≤s e
    +-unit-r' : ∀ {Γ} {e : Γ |- C} → e ≤s (plusC e 0C)
    +-1-r : ∀ {Γ} {e : Γ |- C} → e ≤s (plusC e 1C)
    +-assoc : ∀ {Γ} {e1 e2 e3 : Γ |- C} → (plusC e1 (plusC e2 e3)) ≤s (plusC (plusC e1 e2) e3)
    +-assoc' : ∀ {Γ} {e1 e2 e3 : Γ |- C} → (plusC e1 (plusC e2 e3)) ≤s (plusC (plusC e1 e2) e3)
    refl-+ : ∀ {Γ} {e0 e1 : Γ |- C} → (plusC e0 e1) ≤s (plusC e1 e0)
    cong-+ : ∀ {Γ} {e0 e1 e0' e1' : Γ |- C} → e0 ≤s e0' → e1 ≤s e1' → (plusC e0 e1) ≤s (plusC e0' e1')
    cong-lproj : ∀ {Γ τ τ'} {e e' : Γ |- (τ ×c τ')} → e ≤s e' → (l-proj e) ≤s (l-proj e')
    cong-rproj : ∀ {Γ τ τ'} {e e' : Γ |- (τ ×c τ')} → e ≤s e' → (r-proj e) ≤s (r-proj e')
    cong-app   : ∀ {Γ τ τ'} {e e' : Γ |- (τ ->c τ')} {e1 : Γ |- τ} → e ≤s e' → (app e e1) ≤s (app e' e1)
    cong-rec : ∀ {Γ τ} {e e' : Γ |- nat} {e0 : Γ |- τ} {e1 : (nat :: (τ :: Γ)) |- τ}
             → e ≤s e'
             → rec e e0 e1 ≤s rec e' e0 e1
    cong-listrec : ∀ {Γ τ τ'} {e e' : Γ |- list τ} {e0 : Γ |- τ'} {e1 : (τ :: (list τ :: (τ' :: Γ))) |- τ'}
                 → e ≤s e'
                 → listrec e e0 e1 ≤s listrec e' e0 e1
    lam-s : ∀ {Γ T T'}
          → {e : (T :: Γ) |- T'}
          → {e2 : Γ |- T}
          → subst e (q e2) ≤s app (lam e) e2
    l-proj-s : ∀ {Γ T1 T2}
             → {e1 : Γ |- T1}  {e2 : Γ |- T2}
             → e1 ≤s (l-proj (prod e1 e2))
    r-proj-s : ∀ {Γ T1 T2}
             → {e1 : Γ |- T1} → {e2 : Γ |- T2}
             → e2 ≤s (r-proj (prod e1 e2))
    rec-steps-z : ∀ {Γ T}
                → {e0 : Γ |- T}
                → {e1 : (nat :: (T :: Γ)) |- T}
                → e0 ≤s (rec z e0 e1)
    rec-steps-s : ∀ {Γ T}
                → {e : Γ |- nat}
                → {e0 : Γ |- T}
                → {e1 : (nat :: (T :: Γ)) |- T}
                → subst e1 (lem4 e (rec e e0 e1)) ≤s (rec (suc e) e0 e1)
    listrec-steps-nil : ∀ {Γ τ τ'}
                      → {e0 : Γ |- τ'}
                      → {e1 : (τ :: (list τ :: (τ' :: Γ))) |- τ'}
                      → e0 ≤s (listrec nil e0 e1)
    listrec-steps-cons : ∀ {Γ τ τ'}
                       → {h : Γ |- τ} {t : Γ |- list τ}
                       → {e0 : Γ |- τ'}
                       → {e1 : (τ :: (list τ :: (τ' :: Γ))) |- τ'}
                       → subst e1 (lem5 h t (listrec t e0 e1)) ≤s (listrec (h ::c t) e0 e1)

  _trans_ : ∀ {Γ T}
            → {e e' e'' : Γ |- T}
            → e ≤s e' → e' ≤s e''
            → e ≤s e''
  _trans_ = trans-s
  infixr 10 _trans_

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
-- Andreas, 2017-01-24, issue #2430, reported by nad

-- Regression introduced by updating module parameter substitution
-- when going underAbstraction (80794767db1aceaa78a72e06ad901cfa53f8346d).

record Σ (A : Set) (B : A → Set) : Set where
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

Σ-map : {A : Set} {B : Set} {P : A → Set} {Q : B → Set} →
        (f : A → B) → (∀ {x} → P x → Q (f x)) →
        Σ A P → Σ B Q
Σ-map f g p = record { proj₁ = f (proj₁ p); proj₂ = g (proj₂ p) }

postulate

  _≡_        : {A : Set} → A → A → Set
  refl       : {A : Set} (x : A) → x ≡ x
  cong       : {A : Set} {B : Set} (f : A → B) {x y : A} →
               x ≡ y → f x ≡ f y
  cong-refl  : {A : Set} {B : Set} (f : A → B) {x : A} →
               refl (f x) ≡ cong f (refl x)
  subst      : {A : Set} (P : A → Set) {x y : A} →
               x ≡ y → P x → P y
  subst-refl : ∀ {A : Set} (P : A → Set) {x} (p : P x) →
               subst P (refl x) p ≡ p
  trans      : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z

module _ (_ : Set) where

  postulate

    Σ-≡,≡→≡ : {A : Set} {B : A → Set} {p₁ p₂ : Σ A B} →
              (p : proj₁ p₁ ≡ proj₁ p₂) →
              subst B p (proj₂ p₁) ≡ proj₂ p₂ →
              p₁ ≡ p₂

    Σ-≡,≡→≡-refl-subst-refl :
      ∀ {A : Set} {B : A → Set} {p} →
      Σ-≡,≡→≡ (refl (proj₁ p)) (subst-refl B (proj₂ p)) ≡ refl p

  rejected :
    {A₁ A₂ : Set} {B₁ : A₁ → Set} {B₂ : A₂ → Set}
    (f : A₁ → A₂) (g : ∀ x → B₁ x → B₂ (f x)) (x : Σ A₁ B₁) →
    Σ-≡,≡→≡ (refl _) (subst-refl B₂ _) ≡ cong (Σ-map f (g _)) (refl x)
  rejected {B₁ = B₁} {B₂} f g x =
    trans {x = Σ-≡,≡→≡ (refl _) (subst-refl B₂ _)}
          {z = cong (Σ-map f (g _)) (refl _)}
          Σ-≡,≡→≡-refl-subst-refl
          (cong-refl _)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Generic.Lib.Intro where

open import Level renaming (zero to lzero; suc to lsuc) public
open import Function public
open import Data.Bool.Base hiding (_<_; _≤_) public

infixl 10 _%
infixl 2  _>>>_

data ⊥ {α} : Set α where
record ⊤ {α} : Set α where
  instance constructor tt

⊥₀ = ⊥ {lzero}
⊤₀ = ⊤ {lzero}

tt₀ : ⊤₀
tt₀ = tt

_% = _∘_

_>>>_ : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : ∀ {x} -> B x -> Set γ}
      -> (f : ∀ x -> B x) -> (∀ {x} -> (y : B x) -> C y) -> ∀ x -> C (f x)
(f >>> g) x = g (f x)

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


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

module UnSizedIO.Base where

open import Data.Maybe.Base
open import Data.Sum renaming (inj₁ to left; inj₂ to right; [_,_]′ to either)
open import Function

open import NativeIO

record IOInterface : Set₁ where
  field
    Command   : Set
    Response : (m : Command) → Set
open IOInterface public

module _ (I : IOInterface) (let C = Command I) (let R = Response I) (A : Set)
  where

  mutual
    record IO : Set where
      coinductive
      constructor delay
      field
        force : IO'

    data IO' : Set where
      exec'      : (c : C) (f : R c → IO) → IO'
      return' : (a : A) → IO'

open IO public

module _ {I : IOInterface} (let C = Command I) (let R = Response I)
      where
  return : ∀{A} (a : A) → IO I A
  return a .force = return' a

  exec : ∀{A} (c : C) (f : R c → IO I A) → IO I A
  exec c f .force = exec' c f

  exec1 :  (c : C) → IO I (R c)
  exec1 c = exec c return

  infixl 2 _>>=_ _>>='_ _>>_

  mutual
    _>>='_ : ∀{A B} (m : IO' I A) (k : A → IO I B) → IO' I B
    exec' c f    >>=' k = exec' c λ x → f x >>= k
    return' a >>=' k = force (k a)

    _>>=_ : ∀{A B} (m : IO I A) (k : A → IO I B) → IO I B
    force (m >>= k) = force m >>=' k

  _>>_ : ∀{B} (m : IO I Unit) (k : IO I B) → IO I B
  m >> k = m >>= λ _ → k

module _ {I : IOInterface} (let C = Command I) (let R = Response I)
      where
  {-# NON_TERMINATING #-}
  translateIO : ∀ {A}
    →  (translateLocal : (c : C) → NativeIO (R c))
    →  IO I A
    →  NativeIO A
  translateIO translateLocal m = case (m .force) of
    λ{ (exec' c f)    → (translateLocal c) native>>= λ r →
         translateIO translateLocal (f r)
     ; (return' a) → nativeReturn a
     }

-- Recursion

-- trampoline provides a generic form of loop (generalizing while/repeat).
-- Starting at state s : S, step function f is iterated until it returns
-- a result in A.

module _ (I : IOInterface)(let C = Command I) (let R = Response I)
      where
  data IO+ (A : Set) : Set where
      exec' : (c : C) (f : R c → IO I A) → IO+ A

module _ {I : IOInterface}(let C = Command I) (let R = Response I)
      where
  fromIO+' : ∀{A} → IO+ I A → IO' I A
  fromIO+' (exec' c f) = exec' c f

  fromIO+ : ∀{A} → IO+ I A → IO I A
  fromIO+ (exec' c f) .force = exec' c f

  _>>=+'_ : ∀{A B} (m : IO+ I A) (k : A → IO I B) → IO' I B
  exec' c f >>=+' k = exec' c λ x → f x >>= k

  _>>=+_ : ∀{A B} (m : IO+ I A) (k : A → IO I B) → IO I B
  force (m >>=+ k) = m >>=+' k

  mutual

    _>>+_ : ∀{A B} (m : IO I (A ⊎ B)) (k : A → IO I B) → IO I B
    force (m >>+ k) = force m >>+' k

    _>>+'_ : ∀{A B} (m : IO' I (A ⊎ B)) (k : A → IO I B) → IO' I B
    exec' c f            >>+' k = exec' c λ x → f x >>+ k
    return' (left  a) >>+' k = force (k a)
    return' (right b) >>+' k = return' b

   -- loop

  {-# TERMINATING #-}
  trampoline : ∀{A S} (f : S → IO+ I (S ⊎ A)) (s : S) → IO I A
  force (trampoline f s) = case (f s) of
    \{ (exec' c k) → exec' c λ r → k r >>+ trampoline f }

  -- simple infinite loop

  {-# TERMINATING #-}
  forever : ∀{A B} → IO+ I A → IO I B
  force (forever (exec' c f)) = exec' c λ r → f r >>= λ _ → forever (exec' c f)

  whenJust : {A : Set} → Maybe A → (A → IO I Unit) → IO I Unit
  whenJust nothing  k = return _
  whenJust (just a) k = k a

module _ (I : IOInterface )
         (let C = I .Command)
         (let R = I .Response)
           where

    data IOind (A : Set) : Set where

      exec''     : (c : C) (f : (r : R c) → IOind A) → IOind A
      return'' : (a : A) → IOind A

main : NativeIO Unit
main = nativePutStrLn "Hello, world!"

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

module Definition.Typed.Consequences.Reduction where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Fundamental.Reducibility
import Tools.PropositionalEquality as PE

open import Tools.Product

-- Helper function where all reducible types can be reduced to WHNF.
whNorm′ : ∀ {A rA Γ l} ([A] : Γ ⊩⟨ l ⟩ A ^ rA)
                → ∃ λ B → Whnf B × Γ ⊢ A :⇒*: B ^ rA
whNorm′ (Uᵣ′ _ _ r l _ e d) = Univ r l , Uₙ , PE.subst (λ ll → _ ⊢ _ :⇒*: Univ r l ^ [ ! , ll ]) e d
whNorm′ (ℕᵣ D) = ℕ , ℕₙ , D
whNorm′ (Emptyᵣ {l = l} D) = Empty l , Emptyₙ , D
whNorm′ (ne′ K D neK K≡K) = K , ne neK , D
whNorm′ (Πᵣ {l = l} (Πᵣ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) = Π F ^ rF ° lF ▹ G ° lG ° l , Πₙ , D
whNorm′ (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) = ∃ F ▹ G , ∃ₙ , D
whNorm′ (emb emb< [A]) = whNorm′ [A]
whNorm′ (emb ∞< [A]) = whNorm′ [A]

-- Well-formed types can all be reduced to WHNF.
whNorm : ∀ {A rA Γ} → Γ ⊢ A ^ rA → ∃ λ B → Whnf B × Γ ⊢ A :⇒*: B ^ rA
whNorm A = whNorm′ (reducible A)

-- whNorm-conv : ∀ {A rA Γ} → Γ ⊢ A ≡ B ^ rA → ∃ λ B → Whnf B × Γ ⊢ A :⇒*: B ^ rA
-- whNorm-conv A = whNorm′ (reducible A)

-- Helper function where reducible all terms can be reduced to WHNF.
whNormTerm′ : ∀ {a A Γ l lA} ([A] : Γ ⊩⟨ l ⟩ A ^ [ ! , lA ]) → Γ ⊩⟨ l ⟩ a ∷ A ^ [ ! , lA ] / [A]
                → ∃ λ b → Whnf b × Γ ⊢ a :⇒*: b ∷ A ^ lA
whNormTerm′ (Uᵣ′ _ _ r l _ e dU) (Uₜ A d typeA A≡A [t]) = A , typeWhnf typeA ,
  conv:⇒*: (PE.subst (λ ll → _ ⊢ _ :⇒*: _ ∷ _ ^ ll) e d)
    (sym (subset* (red (PE.subst (λ ll → _ ⊢ _ :⇒*: Univ r l ^ [ ! , ll ]) e dU))))
whNormTerm′ (ℕᵣ x) (ℕₜ n d n≡n prop) =
  let natN = natural prop
  in  n , naturalWhnf natN , convRed:*: d (sym (subset* (red x)))
whNormTerm′ (ne (ne K D neK K≡K)) (neₜ k d (neNfₜ neK₁ ⊢k k≡k)) =
  k , ne neK₁ , convRed:*: d (sym (subset* (red D)))
whNormTerm′ (Πᵣ′ rF lF lG lF≤ lG≤  F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Πₜ f d funcF f≡f [f] [f]₁) =
  f , functionWhnf funcF , convRed:*: d (sym (subset* (red D)))
whNormTerm′ (emb emb< [A]) [a] = whNormTerm′ [A] [a]
whNormTerm′ (emb ∞< [A]) [a] = whNormTerm′ [A] [a]

-- Well-formed terms can all be reduced to WHNF.
whNormTerm : ∀ {a A Γ lA} → Γ ⊢ a ∷ A ^ [ ! , lA ] → ∃ λ b → Whnf b × Γ ⊢ a :⇒*: b ∷ A ^ lA
whNormTerm {a} {A} ⊢a =
  let [A] , [a] = reducibleTerm ⊢a
  in  whNormTerm′ [A] [a]

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
-- Andreas, 2015-05-28 example by Andrea Vezzosi

open import Common.Size

data Nat (i : Size) : Set where
  zero : ∀ (j : Size< i) → Nat i
  suc  : ∀ (j : Size< i) → Nat j → Nat i

{-# TERMINATING #-}
-- This definition is fine, the termination checker is too strict at the moment.
fix : ∀ {C : Size → Set} → (∀ i → (∀ (j : Size< i) → Nat j -> C j) → Nat i → C i) → ∀ i → Nat i → C i
fix t i (zero j)  = t i (λ (j : Size< i) → fix t j) (zero j)
fix t i (suc j n) = t i (λ (j : Size< i) → fix t j) (suc j n)

case : ∀ i {C : Set} (n : Nat i) (z : C) (s : ∀ (j : Size< i) → Nat j → C) → C
case i (zero j)  z s = z
case i (suc j n) z s = s j n

applyfix : ∀ {C : Size → Set} i (n : Nat i)
  → (∀ i → (∀ (j : Size< i) → Nat j -> C j) → Nat i → C i)
  → C i
applyfix i n f = fix f i n

module M (i0 : Size) (bot : ∀{i} → Nat i) (A : Set) (default : A) where

  loops : A
  loops = applyfix (↑ i0) (zero i0) λ i r (_ : Nat i) →
      case i bot default λ (j : Size< i) (n : Nat j) →   -- Size< i is possibly empty, should be rejected
      case j n   default λ (h : Size< j) (_ : Nat h) →
      r (↑ h) (zero h)

  -- loops
  -- --> fix t (↑ i0) (zero i0)
  -- --> t (↑ i0) (fix t) (zero i0)
  -- --> case i0 bot default λ j n → case j n default λ h _ → fix t (↑ h) (zero h)
  -- and we have reproduced (modulo [h/i0]) what we started with

  -- The above needs this inference to typecheck
  -- h < j,   j < i
  -- ---------------------
  -- ↑ h < i


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by decidable total orders
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Properties.DecTotalOrder
         {d₁ d₂ d₃} (DT : DecTotalOrder d₁ d₂ d₃) where

open Relation.Binary.DecTotalOrder DT hiding (trans)
open import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_

strictTotalOrder : StrictTotalOrder _ _ _
strictTotalOrder = record
  { isStrictTotalOrder = <-isStrictTotalOrder₂ isDecTotalOrder
  }

open StrictTotalOrder strictTotalOrder public


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

module Data.List.Kleene where

open import Data.List.Kleene.Base public

max_stars_repo_name: oisdk/agda-kleene-lists

max_issues_repo_name: oisdk/agda-kleene-lists

max_forks_repo_name: oisdk/agda-kleene-lists


text:
module Dave.Algebra.Naturals.Multiplication where
  open import Dave.Algebra.Naturals.Addition public

  _*_ : ℕ → ℕ → ℕ
  zero * b = zero
  suc a * b = (a * b) + b

  infixl 7 _*_

  *-zero : ∀ (m : ℕ) → m * zero ≡ zero
  *-zero zero = refl
  *-zero (suc m) = begin
    suc m * zero ≡⟨⟩
    m * zero + zero ≡⟨ +-right-identity (m * zero) ⟩
    m * zero ≡⟨ *-zero m ⟩
    zero ∎

  {- Identity -}
  ℕ-*-right-identity : ∀ (m : ℕ) → m * 1 ≡ m
  ℕ-*-right-identity zero = refl
  ℕ-*-right-identity (suc m) = begin
    suc m * 1 ≡⟨⟩
    m * 1 + 1 ≡⟨ cong (λ a → a + 1) (ℕ-*-right-identity m) ⟩
    m + 1 ≡⟨ +-add1ᵣ m ⟩
    suc m ∎

  ℕ-*-left-identity : ∀ (m : ℕ) → 1 * m ≡ m
  ℕ-*-left-identity m = refl

  ℕ-*-HasIdentity : Identity _*_ 1
  Identity.left ℕ-*-HasIdentity = ℕ-*-left-identity
  Identity.right ℕ-*-HasIdentity = ℕ-*-right-identity

  {- Distributivity -}
  *-distrib-+ᵣ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
  *-distrib-+ᵣ zero n p = refl
  *-distrib-+ᵣ (suc m) n p = begin
    (suc m + n) * p ≡⟨⟩
    suc (m + n) * p ≡⟨⟩
    (m + n) * p + p ≡⟨ cong (λ a → a + p) (*-distrib-+ᵣ m n p) ⟩
    m * p + n * p + p ≡⟨ IsCommutativeMonoid.swap021 ℕ-+-IsCommutativeMonoid (m * p) (n * p) p ⟩
    m * p + p + n * p ≡⟨ cong (λ a → m * p + a + n * p) (ℕ-*-left-identity p) ⟩
    m * p + 1 * p + n * p ≡⟨ cong (λ a → a + n * p) (sym (*-distrib-+ᵣ m 1 p)) ⟩
    (m + 1) * p + n * p ≡⟨ cong (λ a → a * p + n * p) (+-add1ᵣ m) ⟩
    suc m * p + n * p ∎

  *-distrib1ᵣ-+ᵣ : ∀ (m p : ℕ) → (m + 1) * p ≡ m * p + p
  *-distrib1ᵣ-+ᵣ m p = begin
    (m + 1) * p ≡⟨ *-distrib-+ᵣ m 1 p ⟩
    m * p + 1 * p ≡⟨⟩
    m * p + p ∎

  *-distrib1ₗ-+ᵣ : ∀ (m p : ℕ) → (1 + m) * p ≡ p + m * p
  *-distrib1ₗ-+ᵣ m p = begin
    (1 + m) * p ≡⟨ *-distrib-+ᵣ 1 m p ⟩
    1 * p + m * p ≡⟨⟩
    p + m * p ∎

  *-distrib-+ₗ : ∀ (m n p : ℕ) → m * (n + p) ≡ m * n + m * p
  *-distrib-+ₗ zero n p = refl
  *-distrib-+ₗ (suc m) n p = begin
    suc m * (n + p) ≡⟨⟩
    m * (n + p) + (n + p) ≡⟨ cong (λ a → a + (n + p)) (*-distrib-+ₗ m n p) ⟩
    m * n + m * p + (n + p) ≡⟨ IsCommutativeMonoid.swap021 ℕ-+-IsCommutativeMonoid (m * n) (m * p) (n + p) ⟩
    m * n + (n + p) + m * p ≡⟨ cong (λ a → a + m * p) (sym (IsSemigroup.assoc ℕ-+-IsSemigroup (m * n) n p)) ⟩
    m * n + n + p + m * p ≡⟨ IsCommutativeMonoid.swap021 ℕ-+-IsCommutativeMonoid (m * n + n) p (m * p) ⟩
    m * n + n + m * p + p ≡⟨⟩
    m * n + 1 * n + m * p + 1 * p ≡⟨ cong (λ a → a + m * p + 1 * p) (sym (*-distrib-+ᵣ m 1 n)) ⟩
    (m + 1) * n + m * p + 1 * p ≡⟨ IsSemigroup.assoc ℕ-+-IsSemigroup ((m + 1) * n) (m * p) (1 * p) ⟩
    (m + 1) * n + (m * p + 1 * p) ≡⟨ cong (λ a → (m + 1) * n + a) (sym (*-distrib-+ᵣ m 1 p)) ⟩
    (m + 1) * n + (m + 1) * p ≡⟨ cong (λ a → a * n + (m + 1) * p) (+-add1ᵣ m) ⟩
    suc m * n + (m + 1) * p ≡⟨ cong (λ a → suc m * n + a * p) (+-add1ᵣ m) ⟩
    suc m * n + suc m * p ∎

  {- Semigroup -}
  *-assoc : associative _*_
  *-assoc zero n p = refl
  *-assoc (suc m) n p = begin
    (suc m * n) * p ≡⟨⟩
    (m * n + n) * p ≡⟨ *-distrib-+ᵣ (m * n) n p ⟩
    m * n * p + n * p ≡⟨⟩
    m * n * p + 1 * (n * p) ≡⟨ cong (λ a → a + 1 * (n * p)) (*-assoc m n p) ⟩
    m * (n * p) + 1 * (n * p) ≡⟨ sym (*-distrib-+ᵣ m 1 (n * p)) ⟩
    (m + 1) * (n * p) ≡⟨ cong (λ a → a * (n * p)) (+-add1ᵣ m) ⟩
    suc m * (n * p) ∎

  ℕ-*-IsSemigroup : IsSemigroup _*_
  IsSemigroup.assoc ℕ-*-IsSemigroup = *-assoc

  ℕ-*-Semigroup : Semigroup
  Semigroup.Carrier ℕ-*-Semigroup = ℕ
  Semigroup._·_ ℕ-*-Semigroup = _*_
  Semigroup.isSemigroup ℕ-*-Semigroup = ℕ-*-IsSemigroup

  {- Monoid -}
  ℕ-*-IsMonoid : IsMonoid _*_ 1
  IsMonoid.semigroup ℕ-*-IsMonoid = ℕ-*-IsSemigroup
  IsMonoid.identity ℕ-*-IsMonoid = ℕ-*-HasIdentity

  ℕ-*-Monoid : Monoid
  Monoid.Carrier ℕ-*-Monoid = ℕ
  Monoid._·_ ℕ-*-Monoid = _*_
  Monoid.e ℕ-*-Monoid = 1
  Monoid.isMonoid ℕ-*-Monoid = ℕ-*-IsMonoid

  {- Commutative Monoid -}
  ℕ-*-comm : commutative _*_
  ℕ-*-comm zero n = begin
    zero * n ≡⟨⟩
    zero ≡⟨ sym (*-zero n) ⟩
    n * zero ∎
  ℕ-*-comm (suc m) n = begin
    suc m * n ≡⟨⟩
    m * n + n ≡⟨ +-comm (m * n) n ⟩
    n + m * n ≡⟨ sym (cong (λ a → a + m * n) (ℕ-*-right-identity n)) ⟩
    n * 1 + m * n ≡⟨ cong (λ a → n * 1 + a) (ℕ-*-comm m n) ⟩
    n * 1 + n * m ≡⟨ sym (*-distrib-+ₗ n 1 m) ⟩
    n * (1 + m) ≡⟨⟩
    n * suc m ∎

  ℕ-*-IsCommutativeMonoid : IsCommutativeMonoid _*_ 1
  IsCommutativeMonoid.isSemigroup ℕ-*-IsCommutativeMonoid = ℕ-*-IsSemigroup
  IsCommutativeMonoid.leftIdentity ℕ-*-IsCommutativeMonoid = ℕ-*-left-identity
  IsCommutativeMonoid.comm ℕ-*-IsCommutativeMonoid = ℕ-*-comm

  ℕ-*-CommutativeMonoid : CommutativeMonoid
  CommutativeMonoid.Carrier ℕ-*-CommutativeMonoid = ℕ
  CommutativeMonoid._·_ ℕ-*-CommutativeMonoid = _*_
  CommutativeMonoid.e ℕ-*-CommutativeMonoid = 1
  CommutativeMonoid.isCommutativeMonoid ℕ-*-CommutativeMonoid = ℕ-*-IsCommutativeMonoid

  *-distrib1ᵣ-+ₗ : ∀ (m p : ℕ) → m * (p + 1) ≡ m * p + m
  *-distrib1ᵣ-+ₗ m p = begin
    m * (p + 1) ≡⟨ ℕ-*-comm m (p + 1) ⟩
    (p + 1) * m ≡⟨ *-distrib1ᵣ-+ᵣ p m ⟩
    p * m + m ≡⟨ cong (λ a → a + m) (ℕ-*-comm p m) ⟩
    m * p + m ∎

  *-distrib1ₗ-+ₗ : ∀ (m p : ℕ) → m * (1 + p) ≡ m + m * p
  *-distrib1ₗ-+ₗ m p = begin
    m * (1 + p) ≡⟨ ℕ-*-comm m (1 + p) ⟩
    (1 + p) * m ≡⟨ *-distrib1ₗ-+ᵣ p m ⟩
    m + p * m ≡⟨ cong (λ a → m + a) (ℕ-*-comm p m) ⟩
    m + m * p ∎


text:
open import Structures --using (KS; SKS; ks; TCS; Prog; monadTC; _⊕_; Err; ok; error; list-has-el; lift-state; lift-mstate)
open import Reflection as RE hiding (return; _>>=_; _>>_)
open import Reflection.Show

module Extract (kompile-fun : Type → Term → Name → SKS Prog) where

open import Reflection.Term
import      Reflection.Name as RN
open import Agda.Builtin.Reflection using (withReconstructed; dontReduceDefs; onlyReduceDefs)

open import Data.List as L hiding (_++_)
open import Data.Unit using (⊤)
open import Data.Product
open import Data.Bool
open import Data.String as S hiding (_++_)
open import Data.Maybe as M hiding (_>>=_)

open import Function --using (_$_; case_of_)

open import ReflHelper

open import Category.Monad using (RawMonad)
open import Category.Monad.State using (StateTMonadState; RawMonadState)
open RawMonad {{...}} public

{-# TERMINATING #-}
kompile-fold   : TCS Prog

macro
  -- Main entry point of the extractor.
  -- `n` is a starting function of the extraction
  -- `base` is the set of base functions that we never traverse into.
  -- `skip` is the list of functions that we have traversed already.
  -- The difference between the two is that `base` would be passed to
  -- `dontReduceDefs`, hence never inlined; whereas `skip` mainly avoids
  -- potential recursive extraction.
  kompile : Name → Names → Names → Term → TC ⊤
  kompile n base skip hole = do
    (p , st) ← kompile-fold $ ks [ n ] base skip ε 1
    --let p = KS.defs st ⊕ p
    q ← quoteTC p
    unify hole q

-- Traverse through the list of the functions we need to extract
-- and collect all the definitions.
kompile-fold = do
    s@(ks fs ba done _ c) ← R.get
    case fs of λ where
      []       → return ε
      (f ∷ fs) → case list-has-el (f RN.≟_) done of λ where
        true → do
          R.modify λ k → record k{ funs = fs }
          kompile-fold
        false → do
          (ty , te) ← lift-state {RM = monadTC} $ do
              ty ← getType f
              ty ← withReconstructed $ dontReduceDefs ba $ normalise ty
              te ← withReconstructed $ getDefinition f >>= λ where
                    (function cs) → return $ pat-lam cs []
                    -- FIXME: currently we do not extract data types, which
                    --        we should fix by parametrising this module by
                    --        kompile-type argument, and calling it in the
                    --        same way as we call kompile-fun now.
                    --(data-cons d) → return $ con d []
                    _ → return unknown
              te ← pat-lam-norm te ba
              return $ ty , te
          case te of λ where
            unknown →
              return $ error $ "kompile: attempting to compile `" ++ showName f ++ "` as function"
            _ → do
                R.put (ks fs ba (f ∷ done) ε c)
                -- Compile the function and make an error more specific in
                -- case compilation fails.
                (ok q) ← lift-mstate {RM = monadTC} $ kompile-fun ty te f
                  where (error x) → return $ error $ "in function " ++ showName f ++ ": " ++ x
                defs ← KS.defs <$> R.get
                let q = defs ⊕ q
                   --R.modify $! λ k → record k{ defs = ε }
                kst ← R.get
                  --let q = KS.defs kst ⊕ q
                R.put $! record kst{ defs = ε }
                -- Do the rest of the functions
                p ← kompile-fold
                return $! p ⊕ "\n\n" ⊕ q
  where
    module R = RawMonadState (StateTMonadState KS monadTC)

max_stars_repo_name: ashinkarov/agda-extractor

max_issues_repo_name: ashinkarov/agda-extractor

max_forks_repo_name: ashinkarov/agda-extractor


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Data.Unit
open import Data.Integer as ℤ using (ℤ)
open import Data.List
open import Data.List.Relation.Unary.All as List
open import Relation.Binary.PropositionalEquality

module simple-quantifierIn-temp-output where

emptyList : List ℤ
emptyList = []

abstract
  empty : List.All (λ (x : ℤ) → ⊤) emptyList
  empty = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

abstract
  double : List.All (λ (x : ℤ) → List.All (λ (y : ℤ) → x ≡ y) emptyList) emptyList
  double = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

abstract
  forallForallIn : ∀ (x : ℤ) → List.All (λ (y : ℤ) → x ≡ y) emptyList
  forallForallIn = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

abstract
  forallInForall : List.All (λ (x : ℤ) → ∀ (y : ℤ) → x ≡ y) emptyList
  forallInForall = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
-- Issue reported by Sergei Meshvelliani
-- Simplified example by Guillaume Allais

-- When adding missing absurd clauses, dot patterns were accidentally
-- turned into variable patterns.

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

open import Agda.Builtin.List

open import Agda.Builtin.Equality

data Var (T : Set₂) (σ : T) : List T → Set₂ where
  z : ∀ Γ → Var T σ (σ ∷ Γ)
  s : ∀ τ Γ → Var T σ Γ → Var T σ (τ ∷ Γ)

eq : ∀ Γ (b c : Var _ Set Γ) → b ≡ c → Set
eq .(Set ∷ Γ) (z Γ) (z .Γ) _ = {!!}
eq .(τ ∷ Γ) (s τ Γ m) (s .τ .Γ n) _ = {!!}

-- WAS: Internal error in CompiledClause.Compile
-- SHOULD: Succeed


text:
-- Forced constructor arguments don't count towards the size of the datatype
-- (only if not --withoutK).

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

data Singleton {a} {A : Set a} : A → Set where
  [_] : ∀ x → Singleton x


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

module Dodo.Unary.Disjoint where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Data.Empty using (⊥)
open import Relation.Unary using (Pred)
-- Local imports
open import Dodo.Unary.Empty
open import Dodo.Unary.Intersection

-- # Definitions

Disjoint₁ : ∀ {a ℓ₁ ℓ₂ : Level} {A : Set a}
  → Pred A ℓ₁ → Pred A ℓ₂ → Set _
Disjoint₁ P Q = Empty₁ (P ∩₁ Q)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
------------------------------------------------------------------------------
-- A looping (error) combinator
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module LTC-PCF.Loop where

open import LTC-PCF.Base

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

error : D
error = fix (λ f → f)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --without-K #-}
open import Level.NP
open import Type hiding (★)
open import Type.Identities
open import Function.NP
open import Function.Extensionality
open import Data.Product
open import Data.Sum
open import Relation.Binary.Logical
open import Relation.Binary.PropositionalEquality.NP
open import Relation.Binary.NP
open import HoTT
open Equivalences

open import Explore.Core
open import Explore.Properties
open import Explore.Explorable
import Explore.Monad

-- NOTE: it would be nice to have another module to change the definition of an exploration
-- function by an extensionally equivalent one. Combined with this module one could both
-- pick the reduction behavior we want and save some proof effort.
module Explore.Isomorphism
  {-a-} {A B : ★₀ {-a-}} (e : A ≃ B) where
a = ₀

private
  module M {ℓ} = Explore.Monad {a} ℓ
  e⁻ = ≃-sym e
  module E = Equiv e
  e→ = E.·→

module _ {ℓ} (Aᵉ : Explore ℓ A) where
  explore-iso : Explore ℓ B
  explore-iso = M.map e→ Aᵉ

private
  Bᵉ = explore-iso

module _ {ℓ p} {Aᵉ : Explore ℓ A} (Aⁱ : ExploreInd p Aᵉ) where
  explore-iso-ind : ExploreInd p (Bᵉ Aᵉ)
  explore-iso-ind = M.map-ind e→ Aⁱ

private
  Bⁱ = explore-iso-ind

module _ {ℓ} {Aᵉ : Explore (ₛ ℓ) A} (Aˡ : Lookup {ℓ} Aᵉ) where
  lookup-iso : Lookup {ℓ} (Bᵉ Aᵉ)
  lookup-iso {C} d b = tr C (E.·←-inv-r b) (Aˡ d (E.·← b))

module _ {ℓ} {Aᵉ : Explore (ₛ ℓ) A} (Aᶠ : Focus {ℓ} Aᵉ) where
  focus-iso : Focus {ℓ} (Bᵉ Aᵉ)
  focus-iso {C} (b , c) = Aᶠ (E.·← b , c')
    where c' = tr C (! (E.·←-inv-r b)) c

module _ (Aˢ : Sum A) where
  sum-iso : Sum B
  sum-iso h = Aˢ (h ∘ e→)

module _ (Aᵖ : Product A) where
  product-iso : Product B
  product-iso h = Aᵖ (h ∘ e→)

module FromExplore-iso
         (Aᵉ : ∀ {ℓ} → Explore ℓ A)
       = FromExplore (Bᵉ Aᵉ)

module FromExploreInd-iso
         {Aᵉ : ∀ {ℓ} → Explore ℓ A}
         (Aⁱ : ∀ {ℓ p} → ExploreInd {ℓ} p Aᵉ)
       = FromExploreInd (Bⁱ Aⁱ)

module _ {ℓ} {Aᵉ : Explore (ₛ ℓ) A} (ΣAᵉ-ok : Adequate-Σ (Σᵉ Aᵉ)) {{_ : UA}} {{_ : FunExt}} where
  Σ-iso-ok : Adequate-Σ (Σᵉ (Bᵉ Aᵉ))
  Σ-iso-ok F = ΣAᵉ-ok (F ∘ e→) ∙ Σ-fst≃ e _

module _ {ℓ} {Aᵉ : Explore (ₛ ℓ) A} (ΠAᵉ-ok : Adequate-Π (Πᵉ Aᵉ)) {{_ : UA}} {{_ : FunExt}} where
  Π-iso-ok : Adequate-Π (Πᵉ (Bᵉ Aᵉ))
  Π-iso-ok F = ΠAᵉ-ok (F ∘ e→) ∙ Π-dom≃ e _

open Adequacy _≡_
module _ {Aˢ : Sum A} (Aˢ-ok : Adequate-sum Aˢ) {{_ : UA}} {{_ : FunExt}} where
  sum-iso-ok : Adequate-sum (sum-iso Aˢ)
  sum-iso-ok h = Aˢ-ok (h ∘ e→) ∙ Σ-fst≃ e _

module _ {Aᵖ : Product A} (Aᵖ-ok : Adequate-product Aᵖ) {{_ : UA}} {{_ : FunExt}} where
  product-iso-ok : Adequate-product (product-iso Aᵖ)
  product-iso-ok g = Aᵖ-ok (g ∘ e→) ∙ Π-dom≃ e _

module _
    {ℓ₀ ℓ₁ ℓᵣ}
    {aᵣ} {Aᵣ : ⟦★⟧ aᵣ A A}
    {bᵣ} {Bᵣ : ⟦★⟧ bᵣ B B}
    (e→ᵣ : (Aᵣ ⟦→⟧ Bᵣ) e→ e→)
    {expᴬ₀ : Explore ℓ₀ A} {expᴬ₁ : Explore ℓ₁ A}(expᴬᵣ : ⟦Explore⟧ ℓᵣ Aᵣ expᴬ₀ expᴬ₁) where
  ⟦explore-iso⟧ : ⟦Explore⟧ ℓᵣ Bᵣ (explore-iso expᴬ₀) (explore-iso expᴬ₁)
  ⟦explore-iso⟧ P Pε P⊕ Pf = expᴬᵣ P Pε P⊕ (Pf ∘ e→ᵣ)

-- -}
-- -}
-- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module Issue204.Dependency where

open import Common.Level public renaming (lsuc to suc)

record R (ℓ : Level) : Set (suc ℓ) where

data D (ℓ : Level) : Set (suc ℓ) where

module M {ℓ : Level} (d : D ℓ) where


text:
------------------------------------------------------------------------
-- Coherently constant functions
------------------------------------------------------------------------

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

import Equality.Path as P

module Coherently-constant
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Prelude hiding (_+_)

import Bijection equality-with-J as B
open import Eilenberg-MacLane-space eq as K using (K[_]1; base; loop)
open import Embedding equality-with-J as Emb using (Embedding)
open import Equality.Decidable-UIP equality-with-J using (Constant)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J hiding (id; _∘_)
open import Group equality-with-J
open import Group.Cyclic eq as C using (ℤ/[1+_]ℤ; _≡_mod_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as T using (∥_∥; ∣_∣)
open import Injection equality-with-J using (Injective)
open import Integer equality-with-J
open import Pointed-type.Homotopy-group eq
open import Preimage equality-with-J using (_⁻¹_)
import Quotient eq as Q
open import Univalence-axiom equality-with-J

private
  variable
    a b     : Level
    A B C D : Type a
    f       : A → B
    p       : A

-- Coherently constant functions.
--
-- Shulman uses the term "conditionally constant" in "Not every weakly
-- constant function is conditionally constant"
-- (https://homotopytypetheory.org/2015/06/11/not-every-weakly-constant-function-is-conditionally-constant/).
-- I do not know who first came up with this definition.

Coherently-constant :
  {A : Type a} {B : Type b} → (A → B) → Type (a ⊔ b)
Coherently-constant {A = A} {B = B} f =
  ∃ λ (g : ∥ A ∥ → B) → f ≡ g ∘ ∣_∣

-- Every coherently constant function is weakly constant.
--
-- This result is mentioned by Shulman.

Coherently-constant→Constant :
  Coherently-constant f → Constant f
Coherently-constant→Constant {f = f} (g , eq) x y =
  f x      ≡⟨ cong (_$ x) eq ⟩
  g ∣ x ∣  ≡⟨ cong g (T.truncation-is-proposition _ _) ⟩
  g ∣ y ∣  ≡⟨ sym $ cong (_$ y) eq ⟩∎
  f y      ∎

-- Every weakly constant function with a stable domain is coherently
-- constant.
--
-- This result was proved by Kraus, Escardó, Coquand and Altenkirch in
-- "Notions of Anonymous Existence in Martin-Löf Type Theory".

Stable-domain→Constant→Coherently-constant :
  {f : A → B} →
  (∥ A ∥ → A) → Constant f → Coherently-constant f
Stable-domain→Constant→Coherently-constant {f = f} s c =
    f ∘ s
  , ⟨ext⟩ λ x →
      f x          ≡⟨ c _ _ ⟩∎
      f (s ∣ x ∣)  ∎

private

  -- Definitions used in the proof of ¬-Constant→Coherently-constant.

  module ¬-Constant→Coherently-constant
    (ℓ : Level) (univ : Univalence lzero)
    where

    -- CCC B is the statement that every constant function from a
    -- merely inhabited type in Type ℓ to B is coherently constant.

    CCC : Type ℓ → Type (lsuc ℓ)
    CCC B =
      (A : Type ℓ) → ∥ A ∥ →
      (f : A → B) → Constant f → Coherently-constant f

    Has-retraction : {A B : Type a} → (B → A) → Type a
    Has-retraction f = ∃ λ g → g ∘ f ≡ id

    -- IR A is the statement that every injective, (-1)-connected
    -- function from A to a type in Type ℓ has a retraction.

    IR : Type ℓ → Type (lsuc ℓ)
    IR A =
      (B : Type ℓ) (f : A → B) → (∀ x → ∥ f ⁻¹ x ∥) →
      Injective f → Has-retraction f

    -- CCC C implies IR C.

    CCC→IR : CCC C → IR C
    CCC→IR {C = C} ccc A f conn inj =
        (λ a → proj₁ (cc a) (conn a))
      , ⟨ext⟩ λ c →
          proj₁ (cc (f c)) (conn (f c))    ≡⟨ cong (proj₁ (cc (f c))) $ T.truncation-is-proposition _ _ ⟩
          proj₁ (cc (f c)) ∣ c , refl _ ∣  ≡⟨ sym $ cong (_$ c , refl _) $ proj₂ (cc (f c)) ⟩∎
          c                                ∎
      where
      cc : (a : A) → Coherently-constant {A = f ⁻¹ a} proj₁
      cc a = ccc (f ⁻¹ a) (conn a) proj₁ λ (c₁ , p₁) (c₂ , p₂) →
        inj (f c₁  ≡⟨ p₁ ⟩
             a     ≡⟨ sym p₂ ⟩∎
             f c₂  ∎)

    -- If there is an embedding from C to D, then CCC D implies CCC C.

    CCC→CCC : Embedding C D → CCC D → CCC C
    CCC→CCC emb ccc B ∥B∥ g c = proj₁ ∘ h , refl _
      where
      e = Embedding.to emb

      cc : Coherently-constant (e ∘ g)
      cc = ccc B ∥B∥ (e ∘ g) λ x y →
        e (g x)  ≡⟨ cong e (c x y) ⟩∎
        e (g y)  ∎

      h : (b : ∥ B ∥) → ∃ λ c → e c ≡ proj₁ cc b
      h = T.elim _ (λ _ → Emb.embedding→⁻¹-propositional
                            (Embedding.is-embedding emb) _) λ b →
        g b , cong (_$ b) (proj₂ cc)

    -- If CCC (A ≃ A) holds for every type A, then CCC (↑ ℓ K[ G ]1)
    -- holds for every abelian group G of type Group lzero.

    CCC-≃→CCC-K :
      ((B : Type ℓ) → CCC (B ≃ B)) →
      (G : Group lzero) → Abelian G → CCC (↑ ℓ K[ G ]1)
    CCC-≃→CCC-K ccc G abelian =
                                       $⟨ ccc (↑ ℓ K[ G ]1) ⟩
      CCC (↑ ℓ K[ G ]1 ≃ ↑ ℓ K[ G ]1)  ↝⟨ CCC→CCC emb ⟩□
      CCC (↑ ℓ K[ G ]1)                □
      where
      Aut[K[G]] = (K[ G ]1 ≃ K[ G ]1) , Eq.id

      Aut[K[G]]-groupoid : H-level 3 (K[ G ]1 ≃ K[ G ]1)
      Aut[K[G]]-groupoid = Eq.left-closure ext 2 K.is-groupoid

      Ω[Aut[K[G]]] =
        Fundamental-group′ Aut[K[G]] Aut[K[G]]-groupoid

      emb : Embedding (↑ ℓ K[ G ]1) (↑ ℓ K[ G ]1 ≃ ↑ ℓ K[ G ]1)
      emb =
        ↑ ℓ K[ G ]1                ↔⟨ B.↑↔ ⟩
        K[ G ]1                    ↔⟨ inverse $ K.cong-≃ $ K.Fundamental-group′[K1≃K1]≃ᴳ univ abelian ⟩
        K[ Ω[Aut[K[G]]] ]1         ↝⟨ proj₁ $ K.K[Fundamental-group′]1↣ᴮ univ Aut[K[G]]-groupoid ⟩
        K[ G ]1 ≃ K[ G ]1          ↔⟨ inverse $ Eq.≃-preserves-bijections ext B.↑↔ B.↑↔ ⟩□
        ↑ ℓ K[ G ]1 ≃ ↑ ℓ K[ G ]1  □

    -- The group of integers.

    module ℤG = Group ℤ-group

    -- The groups ℤ/2ℤ and ℤ/4ℤ.

    ℤ/2ℤ = ℤ/[1+ 1 ]ℤ
    ℤ/4ℤ = ℤ/[1+ 3 ]ℤ

    module ℤ/2ℤ where
      open Group ℤ/2ℤ public
        renaming (_∘_ to infixl 6 _+_; _⁻¹ to infix 8 -_)

    module ℤ/4ℤ where
      open Group ℤ/4ℤ public
        renaming (_∘_ to infixl 6 _+_; _⁻¹ to infix 8 -_)

    -- Multiplication by two, as a function from ℤ/2ℤ to ℤ/4ℤ.

    mul2 : ℤ/2ℤ.Carrier → ℤ/4ℤ.Carrier
    mul2 = Q.rec λ where
      .Q.[]ʳ i                                 → Q.[ i *+ 2 ]
      .Q.is-setʳ                               → Q./-is-set
      .Q.[]-respects-relationʳ {x = i} {y = j} →
        i ≡ j mod 2                  ↝⟨ C.*+-cong {j = j} {n = 2} 2 ⟩
        i *+ 2 ≡ j *+ 2 mod 4        ↝⟨ Q.[]-respects-relation ⟩□
        Q.[ i *+ 2 ] ≡ Q.[ j *+ 2 ]  □

    -- The function mul2, expressed as a group homomorphism.

    mul2ʰ : ℤ/2ℤ →ᴳ ℤ/4ℤ
    mul2ʰ = λ where
      .related     → mul2
      .homomorphic → Q.elim-prop λ where
        .Q.is-propositionʳ _ → Π-closure ext 1 λ _ →
                               Group.Carrier-is-set ℤ/[1+ 3 ]ℤ
        .Q.[]ʳ i → Q.elim-prop λ where
          .Q.is-propositionʳ _ → Group.Carrier-is-set ℤ/[1+ 3 ]ℤ
          .Q.[]ʳ j → cong Q.[_]
            ((i + j) *+ 2     ≡⟨ *+-distrib-+ {i = i} 2 ⟩∎
             i *+ 2 + j *+ 2  ∎)

    -- Integer division by 2, as a function from ℤ/4ℤ to ℤ/2ℤ.

    div2 : ℤ/4ℤ.Carrier → ℤ/2ℤ.Carrier
    div2 = Q.rec λ where
      .Q.[]ʳ i                                 → Q.[ ⌊ i /2⌋ ]
      .Q.is-setʳ                               → Q./-is-set
      .Q.[]-respects-relationʳ {x = i} {y = j} →
        i ≡ j mod 4                    ↝⟨ C.⌊/2⌋-cong j 2 ⟩
        ⌊ i /2⌋ ≡ ⌊ j /2⌋ mod 2        ↝⟨ Q.[]-respects-relation ⟩□
        Q.[ ⌊ i /2⌋ ] ≡ Q.[ ⌊ j /2⌋ ]  □

    -- Some lemmas relating mul2 and div2.

    mul2-div2-lemma₁ :
      ∀ i j → div2 (j ℤ/4ℤ.+ ℤ/4ℤ.- mul2 i) ≡ div2 j ℤ/2ℤ.+ ℤ/2ℤ.- i
    mul2-div2-lemma₁ = Q.elim-prop λ where
      .Q.is-propositionʳ _ →
        Π-closure ext 1 λ _ →
        Q./-is-set
      .Q.[]ʳ i → Q.elim-prop λ where
        .Q.is-propositionʳ _ → Q./-is-set
        .Q.[]ʳ j             → cong Q.[_]
          (⌊ j - i *+ 2 /2⌋    ≡⟨ cong (⌊_/2⌋ ∘ _+_ j) $ ℤG.^+⁻¹ {p = i} 2 ⟩
           ⌊ j + - i *+ 2 /2⌋  ≡⟨ ⌊+*+2/2⌋≡ j ⟩∎
           ⌊ j /2⌋ + - i       ∎)

    mul2-div2-lemma₂ :
      ∀ i j → ℤ/2ℤ.- i ℤ/2ℤ.+ div2 (mul2 i ℤ/4ℤ.+ j) ≡ div2 j
    mul2-div2-lemma₂ = Q.elim-prop λ where
      .Q.is-propositionʳ _ →
        Π-closure ext 1 λ _ →
        Q./-is-set
      .Q.[]ʳ i → Q.elim-prop λ where
        .Q.is-propositionʳ _ → Q./-is-set
        .Q.[]ʳ j             → cong Q.[_]
          (- i + ⌊ i *+ 2 + j /2⌋  ≡⟨ cong (_+_ (- i) ∘ ⌊_/2⌋) $ +-comm (i *+ 2) ⟩
           - i + ⌊ j + i *+ 2 /2⌋  ≡⟨ cong (_+_ (- i)) $ ⌊+*+2/2⌋≡ j ⟩
           - i + (⌊ j /2⌋ + i)     ≡⟨ cong (_+_ (- i)) $ +-comm ⌊ j /2⌋ ⟩
           - i + (i + ⌊ j /2⌋)     ≡⟨ +-assoc (- i) ⟩
           - i + i + ⌊ j /2⌋       ≡⟨ cong (_+ ⌊ j /2⌋) $ +-left-inverse i ⟩
           + 0 + ⌊ j /2⌋           ≡⟨ +-left-identity ⟩∎
           ⌊ j /2⌋                 ∎)

    -- The type K[ ℤ/4ℤ ]1 is (-1)-connected.

    K[ℤ/4ℤ]-connected : (x : K[ ℤ/4ℤ ]1) → ∥ K.map mul2ʰ ⁻¹ x ∥
    K[ℤ/4ℤ]-connected = K.elim-set λ where
      .K.baseʳ     → ∣ base , refl _ ∣
      .K.loopʳ _   → T.truncation-is-proposition _ _
      .K.is-setʳ _ → mono₁ 1 T.truncation-is-proposition

    -- Two equivalences.

    Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ : _≡_ {A = K[ ℤ/4ℤ ]1} base base ≃ ℤ/4ℤ.Carrier
    Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ =
      K.Fundamental-group′[K1]≃ᴳ univ K.is-groupoid .related

    Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ : _≡_ {A = K[ ℤ/2ℤ ]1} base base ≃ ℤ/2ℤ.Carrier
    Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ =
      K.Fundamental-group′[K1]≃ᴳ univ K.is-groupoid .related

    -- The function K.map mul2ʰ is injective.

    map-mul2ʰ-injective : Injective (K.map mul2ʰ)
    map-mul2ʰ-injective {x = x} {y = y} = K.elim-set e x y
      where
      lemma = K.elim-set λ where
        .K.is-setʳ _ →
          Π-closure ext 2 λ _ →
          K.is-groupoid
        .K.baseʳ →
          base ≡ base   ↔⟨ Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ ⟩
          ℤ/4ℤ.Carrier  ↝⟨ div2 ⟩
          ℤ/2ℤ.Carrier  ↔⟨ inverse Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ ⟩□
          base ≡ base   □
        .K.loopʳ i → ⟨ext⟩ λ eq →
          let j = _≃_.to Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ eq in

          subst (λ y → base ≡ K.map mul2ʰ y → base ≡ y)
            (loop i) (loop ∘ div2 ∘ _≃_.to Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ) eq        ≡⟨ subst-→ ⟩

          subst (base ≡_) (loop i)
            (loop $ div2 $ _≃_.to Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ $
             subst ((base ≡_) ∘ K.map mul2ʰ) (sym (loop i)) eq)       ≡⟨ trans (sym trans-subst) $
                                                                         cong (flip trans _) $
                                                                         cong (loop ∘ div2 ∘ _≃_.to Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ) $
                                                                         trans (subst-∘ _ _ _) $
                                                                         trans (sym trans-subst) $
                                                                         cong (trans _) $
                                                                         trans (cong-sym _ _) $
                                                                         cong sym $ K.rec-loop ⟩
          trans
            (loop $ div2 $ _≃_.to Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ $
             trans eq (sym (loop (mul2 i))))
            (loop i)                                                  ≡⟨ cong (flip trans _) $ cong (loop ∘ div2) $
                                                                         K.Fundamental-group′[K1]≃ᴳ univ K.is-groupoid .homomorphic
                                                                           eq (sym (loop (mul2 i))) ⟩
          trans
            (loop $ div2 $
             j ℤ/4ℤ.+ _≃_.to Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ (sym (loop (mul2 i))))
            (loop i)                                                  ≡⟨ cong (flip trans _) $ cong (loop ∘ div2 ∘ (j ℤ/4ℤ.+_)) $
                                                                         →ᴳ-⁻¹ (K.Fundamental-group′[K1]≃ᴳ univ K.is-groupoid) _ ⟩
          trans
            (loop $ div2 $
             j ℤ/4ℤ.+ ℤ/4ℤ.- _≃_.to Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ (loop (mul2 i)))
            (loop i)                                                  ≡⟨ cong (flip trans _ ∘ loop ∘ div2 ∘ (j ℤ/4ℤ.+_) ∘ ℤ/4ℤ.-_) $
                                                                         _≃_.right-inverse-of Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ _ ⟩

          trans (loop (div2 (j ℤ/4ℤ.+ ℤ/4ℤ.- mul2 i))) (loop i)       ≡⟨ cong (flip trans _) $ cong loop $ mul2-div2-lemma₁ i j ⟩

          trans (loop (div2 j ℤ/2ℤ.+ ℤ/2ℤ.- i)) (loop i)              ≡⟨ cong (flip trans _) $
                                                                         ≃ᴳ-sym {G₂ = ℤ/2ℤ} (K.Fundamental-group′[K1]≃ᴳ univ K.is-groupoid)
                                                                           .homomorphic _ _ ⟩

          trans (trans (loop (div2 j)) (loop (ℤ/2ℤ.- i))) (loop i)    ≡⟨ cong (flip trans _) $ cong (trans _) $
                                                                         →ᴳ-⁻¹ (≃ᴳ-sym $ K.Fundamental-group′[K1]≃ᴳ univ K.is-groupoid) _ ⟩

          trans (trans (loop (div2 j)) (sym (loop i))) (loop i)       ≡⟨ trans (trans-assoc _ _ _) $
                                                                         trans (cong (trans _) $ trans-symˡ _) $
                                                                         trans-reflʳ _ ⟩∎
          loop (div2 j)                                               ∎

      e = λ where
        .K.is-setʳ _ →
          Π-closure ext 2 λ _ →
          Π-closure ext 2 λ _ →
          K.is-groupoid
        .K.baseʳ   → lemma
        .K.loopʳ i → ⟨ext⟩ $ K.elim-prop λ where
          .K.is-propositionʳ _ → Π-closure ext 2 λ _ →
                                 K.is-groupoid
          .K.baseʳ             → ⟨ext⟩ λ eq →
            let j = _≃_.to Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ eq in

            subst (λ x → ∀ y → K.map mul2ʰ x ≡ K.map mul2ʰ y → x ≡ y)
              (loop i) lemma base eq                                   ≡⟨ trans (cong (_$ eq) $ sym $
                                                                                push-subst-application _ _)
                                                                          subst-→ ⟩
            subst (_≡ base) (loop i)
              (lemma base $
               subst (λ x → K.map mul2ʰ x ≡ K.map mul2ʰ base)
                 (sym (loop i)) eq)                                    ≡⟨ trans subst-trans-sym $
                                                                          cong (trans _) $ cong (lemma base) $
                                                                          trans (subst-∘ _ _ _) $
                                                                          subst-trans-sym ⟩
            trans (sym $ loop i)
              (lemma base $
               trans (sym (cong (K.map mul2ʰ) (sym (loop i)))) eq)     ≡⟨ cong (trans _) $ cong (lemma base) $ cong (flip trans _) $
                                                                          trans (sym $ cong-sym _ _) $
                                                                          cong (cong _) $ sym-sym _ ⟩
            trans (sym $ loop i)
              (lemma base (trans (cong (K.map mul2ʰ) (loop i)) eq))    ≡⟨ cong (trans _) $ cong (lemma base) $ cong (flip trans _)
                                                                          K.rec-loop ⟩
            trans (sym $ loop i)
              (lemma base (trans (loop (mul2 i)) eq))                  ≡⟨⟩

            trans (sym $ loop i)
              (loop $ div2 $ _≃_.to Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ $
               trans (loop (mul2 i)) eq)                               ≡⟨ cong₂ (λ p q → trans p (loop (div2 q)))
                                                                            (sym $
                                                                             →ᴳ-⁻¹ (≃ᴳ-sym $ K.Fundamental-group′[K1]≃ᴳ univ K.is-groupoid) _)
                                                                            (K.Fundamental-group′[K1]≃ᴳ univ K.is-groupoid .homomorphic
                                                                               (loop (mul2 i)) eq) ⟩
            trans (loop (ℤ/2ℤ.- i))
              (loop $ div2 $
               _≃_.to Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ (loop (mul2 i)) ℤ/4ℤ.+ j)        ≡⟨ cong (trans (loop (ℤ/2ℤ.- i)) ∘ loop ∘ div2 ∘ (ℤ/4ℤ._+ j)) $
                                                                          _≃_.right-inverse-of Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ _ ⟩

            trans (loop (ℤ/2ℤ.- i)) (loop (div2 (mul2 i ℤ/4ℤ.+ j)))    ≡⟨ sym $
                                                                          ≃ᴳ-sym (K.Fundamental-group′[K1]≃ᴳ univ K.is-groupoid)
                                                                            .homomorphic _ _ ⟩

            loop (ℤ/2ℤ.- i ℤ/2ℤ.+ div2 (mul2 i ℤ/4ℤ.+ j))              ≡⟨ cong loop $ mul2-div2-lemma₂ i j ⟩

            loop (div2 j)                                              ≡⟨⟩

            lemma base eq                                              ∎

    -- It is not the case that IR holds for ↑ ℓ K[ ℤ/2ℤ ]1.

    ¬IR : ¬ IR (↑ ℓ K[ ℤ/2ℤ ]1)
    ¬IR ir = contradiction
      where

      -- The function K.map mul2ʰ has a retraction.

      map-mul2ʰ-has-retraction : Has-retraction (K.map mul2ʰ)
      map-mul2ʰ-has-retraction =
        let r , is-r = ir (↑ ℓ K[ ℤ/4ℤ ]1) mul2′ conn inj in
          lower ∘ r ∘ lift
        , (⟨ext⟩ λ x →
           lower (r (lift (K.map mul2ʰ x)))  ≡⟨ cong lower $ cong (_$ lift x) is-r ⟩∎
           x                                 ∎)
        where
        mul2′ : ↑ ℓ K[ ℤ/2ℤ ]1 → ↑ ℓ K[ ℤ/4ℤ ]1
        mul2′ = lift ∘ K.map mul2ʰ ∘ lower

        conn : (x : ↑ ℓ K[ ℤ/4ℤ ]1) → ∥ mul2′ ⁻¹ x ∥
        conn =
          T.∥∥-map (Σ-map lift (cong lift)) ∘
          K[ℤ/4ℤ]-connected ∘ lower

        inj : Injective mul2′
        inj = cong lift ∘ map-mul2ʰ-injective ∘ cong lower

      -- The retraction, and the proof showing that it is a
      -- retraction.

      r₁ : K[ ℤ/4ℤ ]1 → K[ ℤ/2ℤ ]1
      r₁ = proj₁ map-mul2ʰ-has-retraction

      r₁-retraction : r₁ ∘ K.map mul2ʰ ≡ id
      r₁-retraction = proj₂ map-mul2ʰ-has-retraction

      -- A lemma related to r₁.

      r₁-lemma :
        trans (sym $ cong (_$ base) r₁-retraction)
          (trans (cong r₁ (cong (K.map mul2ʰ) p))
             (cong (_$ base) r₁-retraction)) ≡
        p
      r₁-lemma {p = p} =
        trans (sym $ cong (_$ base) r₁-retraction)
          (trans (cong r₁ (cong (K.map mul2ʰ) p))
             (cong (_$ base) r₁-retraction))        ≡⟨ cong (trans _) $ cong (flip trans _) $
                                                       cong-∘ _ _ _ ⟩
        trans (sym $ cong (_$ base) r₁-retraction)
          (trans (cong (r₁ ∘ K.map mul2ʰ) p)
             (cong (_$ base) r₁-retraction))        ≡⟨ cong (trans _) $
                                                       naturality (λ x → cong (_$ x) r₁-retraction) ⟩
        trans (sym $ cong (_$ base) r₁-retraction)
          (trans (cong (_$ base) r₁-retraction)
             (cong id p))                           ≡⟨ trans-sym-[trans] _ _ ⟩

        cong id p                                   ≡⟨ sym $ cong-id _ ⟩∎

        p                                           ∎

      -- A variant of r₁ that is definitionally equal to base for
      -- base.

      r₂ : K[ ℤ/4ℤ ]1 → K[ ℤ/2ℤ ]1
      r₂ = K.rec λ where
        .K.baseʳ → base

        .K.loopʳ i →
          base     ≡⟨ sym $ cong (_$ base) r₁-retraction ⟩
          r₁ base  ≡⟨ cong r₁ (loop i) ⟩
          r₁ base  ≡⟨ cong (_$ base) r₁-retraction ⟩∎
          base     ∎

        .K.loop-idʳ →
          trans (sym $ cong (_$ base) r₁-retraction)
            (trans (cong r₁ (loop ℤ/4ℤ.id))
               (cong (_$ base) r₁-retraction))                    ≡⟨ cong (trans _) $ cong (flip trans _) $ cong (cong r₁) $ sym
                                                                     K.rec-loop ⟩
          trans (sym $ cong (_$ base) r₁-retraction)
            (trans (cong r₁ (cong (K.map mul2ʰ) (loop ℤ/2ℤ.id)))
               (cong (_$ base) r₁-retraction))                    ≡⟨ r₁-lemma ⟩

          loop ℤ/2ℤ.id                                            ≡⟨ K.loop-id ⟩∎

          refl _                                                  ∎

        .K.loop-∘ʳ {x = x} {y = y} →
          trans (sym $ cong (_$ base) r₁-retraction)
            (trans (cong r₁ (loop (x ℤ/4ℤ.+ y)))
               (cong (_$ base) r₁-retraction))           ≡⟨ cong (trans _) $ cong (flip trans _) $ cong (cong r₁) $
                                                            K.loop-∘ ⟩
          trans (sym $ cong (_$ base) r₁-retraction)
            (trans (cong r₁ (trans (loop x) (loop y)))
               (cong (_$ base) r₁-retraction))           ≡⟨ trans (cong (trans _) $
                                                                   trans (cong (flip trans _) $
                                                                          cong-trans _ _ _) $
                                                                   trans-assoc _ _ _) $
                                                            sym $ trans-assoc _ _ _ ⟩
          trans
            (trans (sym $ cong (_$ base) r₁-retraction)
               (cong r₁ (loop x)))
            (trans (cong r₁ (loop y))
               (cong (_$ base) r₁-retraction))           ≡⟨ trans (cong (trans _) $ sym $
                                                                   trans--[trans-sym] _ _) $
                                                            trans (sym $ trans-assoc _ _ _) $
                                                            cong (flip trans _) $
                                                            trans-assoc _ _ _ ⟩∎
          trans
            (trans (sym $ cong (_$ base) r₁-retraction)
               (trans (cong r₁ (loop x))
                  (cong (_$ base) r₁-retraction)))
            (trans (sym $ cong (_$ base) r₁-retraction)
               (trans (cong r₁ (loop y))
                  (cong (_$ base) r₁-retraction)))       ∎

        .K.is-groupoidʳ → K.is-groupoid

      -- The functions r₁ and r₂ are pointwise equal.

      r₁≡r₂ : ∀ x → r₁ x ≡ r₂ x
      r₁≡r₂ = K.elim-set λ where
        .K.is-setʳ _ → K.is-groupoid
        .K.baseʳ     →
          r₁ base  ≡⟨ cong (_$ base) r₁-retraction ⟩∎
          r₂ base  ∎
        .K.loopʳ i →
          subst (λ x → r₁ x ≡ r₂ x) (loop i)
            (cong (_$ base) r₁-retraction)                  ≡⟨ subst-in-terms-of-trans-and-cong ⟩

          trans (sym (cong r₁ (loop i)))
            (trans (cong (_$ base) r₁-retraction)
               (cong r₂ (loop i)))                          ≡⟨ cong (trans _) $ cong (trans _)
                                                               K.rec-loop ⟩
          trans (sym (cong r₁ (loop i)))
            (trans (cong (_$ base) r₁-retraction)
               (trans (sym $ cong (_$ base) r₁-retraction)
                  (trans (cong r₁ (loop i))
                     (cong (_$ base) r₁-retraction))))      ≡⟨ cong (trans _) $
                                                               trans--[trans-sym] _ _ ⟩
          trans (sym (cong r₁ (loop i)))
            (trans (cong r₁ (loop i))
               (cong (_$ base) r₁-retraction))              ≡⟨ trans-sym-[trans] _ _ ⟩∎

          cong (_$ base) r₁-retraction                      ∎

      -- Thus r₂ is also a retraction of K.map mul2ʰ.

      r₂-retraction : r₂ ∘ K.map mul2ʰ ≡ id
      r₂-retraction =
        r₂ ∘ K.map mul2ʰ  ≡⟨ cong (_∘ K.map mul2ʰ) $ sym $ ⟨ext⟩ r₁≡r₂ ⟩
        r₁ ∘ K.map mul2ʰ  ≡⟨ r₁-retraction ⟩∎
        id                ∎

      -- A group homomorphism from ℤ/4ℤ to ℤ/2ℤ.

      r₃ : ℤ/4ℤ →ᴳ ℤ/2ℤ
      r₃ .related =
        ℤ/4ℤ.Carrier  ↔⟨ inverse Ω[K[ℤ/4ℤ]]≃ℤ/4ℤ ⟩
        base ≡ base   ↝⟨ cong r₂ ⟩
        base ≡ base   ↔⟨ Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ ⟩□
        ℤ/2ℤ.Carrier  □
      r₃ .homomorphic i j =
        _≃_.to Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ (cong r₂ (loop (i ℤ/4ℤ.+ j)))        ≡⟨ cong (_≃_.to Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ ∘ cong r₂) K.loop-∘ ⟩

        _≃_.to Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ (cong r₂ (trans (loop i) (loop j)))  ≡⟨ cong (_≃_.to Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ) $ cong-trans _ _ _ ⟩

        _≃_.to Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ
          (trans (cong r₂ (loop i)) (cong r₂ (loop j)))             ≡⟨ K.Fundamental-group′[K1]≃ᴳ univ K.is-groupoid
                                                                         .homomorphic _ _ ⟩∎
        _≃_.to Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ (cong r₂ (loop i)) ℤ/2ℤ.+
        _≃_.to Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ (cong r₂ (loop j))                   ∎

      -- The homomorphism r₃ is a retraction of mul2.

      r₃-retraction : ∀ i → Homomorphic.to r₃ (mul2 i) ≡ i
      r₃-retraction i =
        _≃_.to Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ (cong r₂ (loop (mul2 i)))  ≡⟨ cong (_≃_.to Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ) lemma ⟩
        _≃_.to Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ (loop i)                   ≡⟨ _≃_.right-inverse-of Ω[K[ℤ/2ℤ]]≃ℤ/2ℤ _ ⟩∎
        i                                                 ∎
        where
        lemma =
          cong r₂ (loop (mul2 i))                           ≡⟨ K.rec-loop ⟩

          trans (sym $ cong (_$ base) r₁-retraction)
            (trans (cong r₁ (loop (mul2 i)))
               (cong (_$ base) r₁-retraction))              ≡⟨ cong (trans _) $ cong (flip trans _) $ cong (cong r₁) $ sym
                                                               K.rec-loop ⟩
          trans (sym $ cong (_$ base) r₁-retraction)
            (trans (cong r₁ (cong (K.map mul2ʰ) (loop i)))
               (cong (_$ base) r₁-retraction))              ≡⟨ r₁-lemma ⟩∎

          loop i                                            ∎

      -- 0 and 1 are equal when viewed as elements of ℤ/2ℤ.

      0≡1 : _≡_ {A = ℤ/2ℤ.Carrier} Q.[ + 0 ] Q.[ + 1 ]
      0≡1 =
        Q.[ + 0 ]                           ≡⟨ sym $ C.ℤ/2ℤ-+≡0 (Homomorphic.to r₃ Q.[ + 1 ]) ⟩

        Homomorphic.to r₃ Q.[ + 1 ] ℤ/2ℤ.+
        Homomorphic.to r₃ Q.[ + 1 ]         ≡⟨ sym $ r₃ .homomorphic Q.[ + 1 ] Q.[ + 1 ] ⟩

        Homomorphic.to r₃ Q.[ + 2 ]         ≡⟨⟩

        Homomorphic.to r₃ (mul2 Q.[ + 1 ])  ≡⟨ r₃-retraction Q.[ + 1 ] ⟩∎

        Q.[ + 1 ]                           ∎

      -- However, this is contradictory.

      contradiction : ⊥
      contradiction = C.ℤ/ℤ-0≢1 0 0≡1

-- It is not the case that, for every type A : Type a and merely
-- inhabited type B : Type a, every weakly constant function from B to
-- A ≃ A is coherently constant (assuming univalence).
--
-- This result is due to Sattler (personal communication), building on
-- work by Shulman (see "Not every weakly constant function is
-- conditionally constant").

¬-Constant→Coherently-constant :
  Univalence lzero →
  ¬ ((A B : Type a) → ∥ A ∥ →
     (f : A → B ≃ B) → Constant f → Coherently-constant f)
¬-Constant→Coherently-constant {a = a} univ =
  ((A B : Type a) → ∥ A ∥ →
   (f : A → B ≃ B) → Constant f → Coherently-constant f)  ↝⟨ flip ⟩

  ((B : Type a) → CCC (B ≃ B))                            ↝⟨ CCC-≃→CCC-K ⟩

  ((G : Group lzero) → Abelian G → CCC (↑ a K[ G ]1))     ↝⟨ (λ hyp G abelian → CCC→IR (hyp G abelian)) ⟩

  ((G : Group lzero) → Abelian G → IR (↑ a K[ G ]1))      ↝⟨ (λ hyp → hyp ℤ/2ℤ C.ℤ/ℤ-abelian) ⟩

  IR (↑ a K[ ℤ/2ℤ ]1)                                     ↝⟨ ¬IR ⟩□

  ⊥                                                       □
  where
  open ¬-Constant→Coherently-constant a univ

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
{-

https://serokell.io/blog/playing-with-negation

Constructive and Non-Constructive Proofs in Agda (Part 3): Playing with Negation

Danya Rogozin Friday, November 30th, 2018

Present an empty type to work with constructive negation.
Discuss Markov’s principle and apply this principle for one use case.
Declare the double negation elimination as a postulate.
Some examples of non-constructive proofs in Agda.

------------------------------------------------------------------------------
Empty type

-}
-- Type with no constructors (so-called bottom).
-- Type that corresponds to an absurd statement or contradiction.
data ⊥ : Set where

-- ¬ defines negation. ¬A denotes that any proof of A yields a proof of a contradiction:

¬_ : Set → Set
¬ A = A → ⊥

-- elimination of ⊥ : derives an arbitrary statement from bottom
exFalso : {A : Set} → ⊥ → A
exFalso ()

-- examples of propositions with negation that are provable constructively.

-- Derives an arbitrary formula from a contradiction.
-- The first argument f has a type ¬ A (or A → ⊥).
-- The second argument x has a type A.
-- Thus f x is an object of type ⊥.
-- Hence exContr (f x) has a type B.
exContr : {A B : Set} → ¬ A → A → B
exContr f x = exFalso (f x)

exContr2 : {A B : Set} → (A → ⊥) → A → B
exContr2 f x = exFalso (f x)

-- g proves B → ⊥
-- f proves A → B
-- g ∘ f proves A → ⊥, i.e. ¬ A.
contraposition : {A B : Set} → (A → B) → (¬ B → ¬ A)
contraposition f g = g ∘ f

-- negation on formula A.
-- If possible to derive contradictionary consequences B and ¬ B from the statement A,
-- then any proof of A yields ⊥.
¬-intro : {A B : Set} → (A → B) → (A → ¬ B) → ¬ A
¬-intro f g x = g x (f x)

{-
disjImpl establishes a connection between disjunction and implication.
If prove ¬ A ∨ B and have a proof of A.
If have a proof of ¬ A, then we have proved B by ex-falso.
If have a proof of B, then we have already proved B trivially.
So, we have obtained a proof of B by case analysis (i.e., pattern-matching).
-}
disjImpl : {A B : Set} → ¬ A ⊎ B → A → B
disjImpl (inj₁ x) a = exContr x a
disjImpl (inj₂ y) a = y

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

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

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