text:
------------------------------------------------------------------------------
-- First-order logic (without equality)
------------------------------------------------------------------------------

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

-- This module is re-exported by the "base" modules whose theories are
-- defined on first-order logic (without equality).

-- The logical connectives are hard-coded in our translation, i.e. the
-- symbols ⊥, ⊤, ¬, ∧, ∨, → and ↔ must be used.
--
-- N.B. For the implication we use the Agda function type.
--
-- N.B For the universal quantifier we use the Agda (dependent)
-- function type.

module Common.FOL.FOL where

infixr 4 _,_
infix  3 ¬_
infixr 2 _∧_
infix  2 ∃
infixr 1 _∨_
infixr 0 _↔_

----------------------------------------------------------------------------
-- The universe of discourse/universal domain.
postulate D : Set

------------------------------------------------------------------------------
-- The conjunction data type.

-- It is not necessary to add the data constructor _,_ as an
-- axiom because the ATPs implement it.
data _∧_ (A B : Set) : Set where
  _,_ : A → B → A ∧ B

-- It is not strictly necessary define the projections ∧-proj₁ and
-- ∧-proj₂ because the ATPs implement them. For the same reason, it is
-- not necessary to add them as (general/local) hints.
∧-proj₁ : ∀ {A B} → A ∧ B → A
∧-proj₁ (a , _) = a

∧-proj₂ : ∀ {A B} → A ∧ B → B
∧-proj₂ (_ , b) = b

-----------------------------------------------------------------------------
-- The disjunction data type.

-- It is not necessary to add the data constructors inj₁ and inj₂ as
-- axioms because the ATPs implement them.
data _∨_ (A B : Set) : Set where
  inj₁ : A → A ∨ B
  inj₂ : B → A ∨ B

-- It is not strictly necessary define the eliminator `case` because
-- the ATPs implement it. For the same reason, it is not necessary to
-- add it as a (general/local) hint.
case : ∀ {A B} → {C : Set} → (A → C) → (B → C) → A ∨ B → C
case f g (inj₁ a) = f a
case f g (inj₂ b) = g b

------------------------------------------------------------------------------
-- The empty type.
data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

------------------------------------------------------------------------------
-- The unit type.
-- N.B. The name of this type is "\top", not T.
data ⊤ : Set where
  tt : ⊤

------------------------------------------------------------------------------
-- Negation.

-- The underscore allows to write for example '¬ ¬ A' instead of '¬ (¬ A)'.

-- We do not add a definition because: i) the definition of negation
-- is not a FOL-definition and ii) the translation of the neagation is
-- hard-coded in Apia.

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

------------------------------------------------------------------------------
-- Biconditional.

-- We do not add a definition because: i) the definition of the
-- biconditional is not a FOL-definition, ii) the translation of the
-- biconditional is hard-coded in Apia.

_↔_ : Set → Set → Set
A ↔ B = (A → B) ∧ (B → A)

------------------------------------------------------------------------------
-- The existential quantifier type on D.
data ∃ (A : D → Set) : Set where
  _,_ : (t : D) → A t → ∃ A

-- Sugar syntax for the existential quantifier.
syntax ∃ (λ x → e) = ∃[ x ] e

-- 2012-03-05: We avoid to use the existential elimination or the
-- existential projections because we use pattern matching (and the
-- Agda's with constructor).

-- The existential elimination.
--
-- NB. We do not use the usual type theory elimination with two
-- projections because we are working in first-order logic where we do
-- not need extract a witness from an existence proof.
-- ∃-elim : {A : D → Set}{B : Set} → ∃ A → (∀ {x} → A x → B) → B
-- ∃-elim (_ , Ax) h = h Ax

-- The existential proyections.
-- ∃-proj₁ : ∀ {A} → ∃ A → D
-- ∃-proj₁ (x , _) = x

-- ∃-proj₂ : ∀ {A} → (h : ∃ A) → A (∃-proj₁ h)
-- ∃-proj₂ (_ , Ax) = Ax

------------------------------------------------------------------------------
-- Properties

→-trans : {A B C : Set} → (A → B) → (B → C) → A → C
→-trans f g a = g (f a)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Andreas, 2014-06-12  This feature has been addressed by issue 907

{-# OPTIONS --copatterns #-}

module CopatternsToRHS where

import Common.Level
open import Common.Equality
open import Common.Prelude using (Bool; true; false)

record R (A : Set) : Set where
  constructor mkR
  field
    fst : A → A
    snd : Bool
open R

someR : {A : Set} → R A
fst someR x = x
snd someR = true

-- This already behaves like:

someR' : {A : Set} → R A
fst someR' = λ x → x
snd someR' = true

-- We translate it to:

someR″ : {A : Set} → R A
someR″ = mkR (λ x → x) true

data C {A : Set} : R A → Set where
   c : ∀ f b → C (mkR f b)

works : {A : Set} → C {A} someR″ → Set₁
works (c .(λ x → x) .true) = Set

test : {A : Set} → C {A} someR → Set₁
test (c .(λ x → x) .true) = Set

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- A tactic aimed at making equational reasoning proofs more readable
-- in modules that are parametrised by an implementation of equality
------------------------------------------------------------------------

-- The tactic uses the first instance of Equality-with-J that it finds
-- in the context.

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

open import Equality
open import Prelude

module Tactic.By.Parametrised
  {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import List eq
open import Monad eq
open import Tactic.By eq as TB
open import TC-monad eq as TC

open TB public using (⟨_⟩)

------------------------------------------------------------------------
-- The ⟨by⟩ tactic

private

  -- Finds the first instance of "∀ Δ → Equality-with-J something" in
  -- the context (if any; Δ must not contain "visible" arguments),
  -- starting from the "outside", and returns a term standing for this
  -- instance.

  find-Equality-with-J : TC Term
  find-Equality-with-J = do
    c ← getContext
    n ← search (reverse c)
    return (var (length c ∸ suc n) [])
    where
    search : List (Arg TC.Type) → TC ℕ
    search [] = typeError (strErr err ∷ [])
      where
      err = "⟨by⟩: No instance of Equality-with-J found in the context."
    search (a@(arg _ t) ∷ args) = do
      if ok t then return 0
              else suc ⟨$⟩ search args
      where
      ok : Term → Bool
      ok (def f _) =
        if eq-Name f (quote Equality-with-J)
        then true
        else false

      ok (pi (arg (arg-info visible _) _) _) = false
      ok (pi _ (abs _ b))                    = ok b
      ok _                                   = false

open ⟨By⟩
  (λ where
     (def (quote Reflexive-relation._≡_)
          (arg _ a ∷ _ ∷ arg _ A ∷ arg _ x ∷ arg _ y ∷ [])) →
       return $ just (a , A , x , y)
     _ → return nothing)
  find-Equality-with-J
  (λ eq p → def (quote sym) (varg eq ∷ varg p ∷ []))
  (λ eq lhs rhs f p → def (quote cong)
                          (varg eq ∷
                           replicate 4 (harg unknown) ++
                           harg lhs ∷ harg rhs ∷ varg f ∷ varg p ∷ []))
  false
  public

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Andreas, 2016-12-28, issue #2360 reported by m0davis
-- Ambigous projection in with-clause triggered internal error

postulate
  A : Set
  a : A

module M (X : Set) where
  record R : Set where
    field f : X

-- Opening two instantiations of M creates and ambiguous projection

open M A using (module R)
open M A

test : R
R.f test with a
R.f test | _ = a  -- WAS: triggered __IMPOSSIBLE__

-- should succeed


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

module Ferros.Prelude where

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Nat.Properties
open import Data.Bool hiding (_≤_)

ℕ-sub : (x y : ℕ) → (y ≤ x) → ℕ
ℕ-sub x .zero z≤n = x
ℕ-sub ._ ._ (s≤s p) = ℕ-sub _ _ p

invert-ℕ-sub : ∀ x y → (p : y ≤ x) → (ℕ-sub x y p) + y ≡ x
invert-ℕ-sub x .zero z≤n = +-identityʳ x
invert-ℕ-sub (suc x) (suc y) (s≤s p) = begin
  (ℕ-sub (suc x) (suc y) (s≤s p)) + suc y   ≡⟨ +-suc (ℕ-sub (suc x) (suc y) (s≤s p)) y ⟩
  suc ((ℕ-sub (suc x) (suc y) (s≤s p)) + y) ≡⟨ cong suc (invert-ℕ-sub x y p) ⟩
  suc x
  ∎ where open ≡-Reasoning

max_stars_repo_name: auxoncorp/ferros-spec

max_issues_repo_name: auxoncorp/ferros-spec

max_forks_repo_name: auxoncorp/ferros-spec


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

module TypeTheory.Nat.Instance where

-- agda-stdlib
open import Level renaming (zero to lzero; suc to lsuc)
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary.PropositionalEquality using (refl)

-- agda-misc
import TypeTheory.Nat.Operations as NatOperations

ℕ-ind : ∀ {l} (P : ℕ → Set l) → P zero → (∀ k → P k → P (suc k)) → ∀ n → P n
ℕ-ind P P-base P-step zero    = P-base
ℕ-ind P P-base P-step (suc n) = P-step n (ℕ-ind P P-base P-step n)

open NatOperations ℕ zero suc ℕ-ind
                   (λ _ _ _ → refl) (λ _ _ _ _ → refl) public


text:
{-# OPTIONS --warning=error #-}

module UselessPrivateImport2 where

private
  open import Common.Issue481ParametrizedModule Set


text: module Numeral.Integer.Relation where

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module OpenPublicPlusTypeError where

module X where

  postulate D : Set

open X public

postulate x : D

typeIncorrect : Set
typeIncorrect = Set1

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Structures.TypeEqvTo where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.HITs.PropositionalTruncation
open import Cubical.Data.Prod hiding (_×_) renaming (_×Σ_ to _×_)

open import Cubical.Foundations.SIP renaming (SNS-PathP to SNS)
open import Cubical.Foundations.Pointed
open import Cubical.Structures.Pointed

private
  variable
    ℓ ℓ' ℓ'' : Level

TypeEqvTo : (ℓ : Level) (X : Type ℓ') → Type (ℓ-max (ℓ-suc ℓ) ℓ')
TypeEqvTo ℓ X = TypeWithStr ℓ (λ Y → ∥ Y ≃ X ∥)

PointedEqvTo : (ℓ : Level) (X : Type ℓ') → Type (ℓ-max (ℓ-suc ℓ) ℓ')
PointedEqvTo ℓ X = TypeWithStr ℓ (λ Y → Y × ∥ Y ≃ X ∥)

module _ (X : Type ℓ') where

  PointedEqvTo-structure : Type ℓ → Type (ℓ-max ℓ ℓ')
  PointedEqvTo-structure = add-to-structure pointed-structure (λ Y _ → ∥ Y ≃ X ∥)

  PointedEqvTo-iso : StrIso PointedEqvTo-structure ℓ''
  PointedEqvTo-iso = add-to-iso pointed-structure pointed-iso (λ Y _ → ∥ Y ≃ X ∥)

  PointedEqvTo-is-SNS : SNS {ℓ} PointedEqvTo-structure PointedEqvTo-iso
  PointedEqvTo-is-SNS = add-axioms-SNS pointed-structure pointed-iso (λ Y _ → ∥ Y ≃ X ∥)
                                       (λ _ _ → squash)
                                       pointed-is-SNS

  PointedEqvTo-SIP : (A B : PointedEqvTo ℓ X) → A ≃[ PointedEqvTo-iso ] B ≃ (A ≡ B)
  PointedEqvTo-SIP = SIP PointedEqvTo-structure PointedEqvTo-iso PointedEqvTo-is-SNS

  PointedEqvTo-sip : (A B : PointedEqvTo ℓ X) → A ≃[ PointedEqvTo-iso ] B → (A ≡ B)
  PointedEqvTo-sip A B = equivFun (PointedEqvTo-SIP A B)

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
module trie-core where

open import bool
open import char
open import list
open import maybe
open import product
open import string
open import unit
open import eq
open import nat

cal : Set → Set
cal A = 𝕃 (char × A)

empty-cal : ∀{A : Set} → cal A
empty-cal = []

cal-lookup : ∀ {A : Set} → cal A → char → maybe A
cal-lookup [] _ = nothing
cal-lookup ((c , a) :: l) c' with c =char c'
... | tt = just a
... | ff = cal-lookup l c'

cal-insert : ∀ {A : Set} → cal A → char → A → cal A
cal-insert [] c a = (c , a) :: []
cal-insert ((c' , a') :: l) c a with c =char c'
... | tt = (c , a) :: l
... | ff = (c' , a') :: (cal-insert l c a)

cal-remove : ∀ {A : Set} → cal A → char → cal A
cal-remove [] _ = []
cal-remove ((c , a) :: l) c' with c =char c'
... | tt = cal-remove l c'
... | ff = (c , a) :: cal-remove l c'

cal-add : ∀{A : Set} → cal A → char → A → cal A
cal-add l c a = (c , a) :: l

test-cal-insert = cal-insert (('a' , 1) :: ('b' , 2) :: []) 'b' 20

data trie (A : Set) : Set where
  Node : maybe A → cal (trie A) → trie A

empty-trie : ∀{A : Set} → trie A
empty-trie = (Node nothing empty-cal)

trie-lookup-h : ∀{A : Set} → trie A → 𝕃 char → maybe A
trie-lookup-h (Node odata ts) (c :: cs) with cal-lookup ts c
trie-lookup-h (Node odata ts) (c :: cs) | nothing = nothing
trie-lookup-h (Node odata ts) (c :: cs) | just t = trie-lookup-h t cs
trie-lookup-h (Node odata ts) [] = odata

trie-insert-h : ∀{A : Set} → trie A → 𝕃 char → A → trie A
trie-insert-h (Node odata ts) [] x = (Node (just x) ts)
trie-insert-h (Node odata ts) (c :: cs) x with cal-lookup ts c
trie-insert-h (Node odata ts) (c :: cs) x | just t =
  (Node odata (cal-insert ts c (trie-insert-h t cs x)))
trie-insert-h (Node odata ts) (c :: cs) x | nothing =
  (Node odata (cal-add ts c (trie-insert-h empty-trie cs x)))

trie-remove-h : ∀{A : Set} → trie A → 𝕃 char → trie A
trie-remove-h (Node odata ts) (c :: cs) with cal-lookup ts c
trie-remove-h (Node odata ts) (c :: cs) | nothing = Node odata ts
trie-remove-h (Node odata ts) (c :: cs) | just t = Node odata (cal-insert ts c (trie-remove-h t cs))
trie-remove-h (Node odata ts) [] = Node nothing ts

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
postulate
  F : Set → Set → Set

syntax F X Y = X ! Y

test : Set → Set → Set
test X = _! X


text:
open import Everything

module Test.Test4
  {𝔵} {𝔛 : Ø 𝔵}
  {𝔞} {𝔒₁ : 𝔛 → Ø 𝔞}
  {𝔟} {𝔒₂ : 𝔛 → Ø 𝔟}
  {ℓ : Ł}
  ⦃ _ : Transitivity.class (Arrow 𝔒₁ 𝔒₂) ⦄
  -- ⦃ _ : [𝓢urjectivity] (Arrow 𝔒₁ 𝔒₂) (Extension $ ArrowṖroperty ℓ 𝔒₁ 𝔒₂) ⦄
  where
  test[∙] : ∀ {x y} → ArrowṖroperty ℓ 𝔒₁ 𝔒₂ x → Arrow 𝔒₁ 𝔒₂ x y → ArrowṖroperty ℓ 𝔒₁ 𝔒₂ y
  test[∙] P f .π₀ g = (f ◃ P) .π₀ g


text:
module parser where
open import lib
open import cedille-types

{-# FOREIGN GHC import qualified CedilleParser #-}

data Either (A : Set)(B : Set) : Set where
  Left : A → Either A B
  Right : B → Either A B
{-# COMPILE GHC Either = data Either (Left | Right) #-}

postulate
  parseStart  : string → Either (Either string string) start
  parseTerm : string → Either string term
  parseType : string → Either string type
  parseKind : string → Either string kind
  parseLiftingType : string → Either string liftingType
  parseDefTermOrType : string → Either string defTermOrType

{-# COMPILE GHC parseStart = CedilleParser.parseTxt #-}
{-# COMPILE GHC parseTerm = CedilleParser.parseTerm #-}
{-# COMPILE GHC parseType = CedilleParser.parseType #-}
{-# COMPILE GHC parseKind = CedilleParser.parseKind #-}
{-# COMPILE GHC parseLiftingType = CedilleParser.parseLiftingType #-}
{-# COMPILE GHC parseDefTermOrType = CedilleParser.parseDefTermOrType #-}

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


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

open import lib.Basics
open import lib.types.Pi
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.types.Span
open import lib.types.Paths
import lib.types.Generic1HIT as Generic1HIT

module lib.types.Pushout where

module _ {i j k} where

  postulate  -- HIT
    Pushout : (d : Span {i} {j} {k}) → Type (lmax (lmax i j) k)

  module _ {d : Span} where

    postulate  -- HIT
      left : Span.A d → Pushout d
      right : Span.B d → Pushout d
      glue : (c : Span.C d) → left (Span.f d c) == right (Span.g d c)

  module PushoutElim {d : Span} {l} {P : Pushout d → Type l}
    (left* : (a : Span.A d) → P (left a))
    (right* : (b : Span.B d) → P (right b))
    (glue* : (c : Span.C d) → left* (Span.f d c) == right* (Span.g d c) [ P ↓ glue c ]) where

    postulate  -- HIT
      f : Π (Pushout d) P
      left-β : ∀ a → f (left a) ↦ left* a
      right-β : ∀ b → f (right b) ↦ right* b
    {-# REWRITE left-β #-}
    {-# REWRITE right-β #-}

    postulate  -- HIT
      glue-β : (c : Span.C d) → apd f (glue c) == glue* c

Pushout-elim = PushoutElim.f

module PushoutRec {i j k} {d : Span {i} {j} {k}} {l} {D : Type l}
  (left* : Span.A d → D) (right* : Span.B d → D)
  (glue* : (c : Span.C d) → left* (Span.f d c) == right* (Span.g d c)) where

  private
    module M = PushoutElim left* right* (λ c → ↓-cst-in (glue* c))

  f : Pushout d → D
  f = M.f

  glue-β : (c : Span.C d) → ap f (glue c) == glue* c
  glue-β c = apd=cst-in {f = f} (M.glue-β c)

Pushout-rec = PushoutRec.f

Pushout-rec-η : ∀ {i j k} {d : Span {i} {j} {k}} {l} {D : Type l} (f : Pushout d → D)
  → Pushout-rec (f ∘ left) (f ∘ right) (ap f ∘ glue) ∼ f
Pushout-rec-η f = Pushout-elim (λ _ → idp) (λ _ → idp)
  (λ c → ↓-='-in' $ ! $ PushoutRec.glue-β (f ∘ left) (f ∘ right) (ap f ∘ glue) c)

module PushoutGeneric {i j k} {d : Span {i} {j} {k}} where

  open Span d renaming (f to g; g to h)

  open Generic1HIT (Coprod A B) C (inl ∘ g) (inr ∘ h) public

  module _ where

    module To = PushoutRec (cc ∘ inl) (cc ∘ inr) pp

    to : Pushout d → T
    to = To.f

    from-cc : Coprod A B → Pushout d
    from-cc (inl a) = left a
    from-cc (inr b) = right b

    module From = Rec from-cc glue

    from : T → Pushout d
    from = From.f

    abstract
      to-from : (x : T) → to (from x) == x
      to-from = elim to-from-cc to-from-pp where

        to-from-cc : (x : Coprod A B)
          → to (from (cc x)) == cc x
        to-from-cc (inl a) = idp
        to-from-cc (inr b) = idp

        to-from-pp :
          (c : C) → idp == idp [ (λ z → to (from z) == z) ↓ pp c ]
        to-from-pp c = ↓-∘=idf-in' to from
          (ap to (ap from (pp c))   =⟨ From.pp-β c |in-ctx ap to ⟩
           ap to (glue c)           =⟨ To.glue-β c ⟩
           pp c =∎)

      from-to : (x : Pushout d) → from (to x) == x
      from-to = Pushout-elim (λ a → idp) (λ b → idp) (λ c → ↓-∘=idf-in' from to
        (ap from (ap to (glue c))   =⟨ To.glue-β c |in-ctx ap from ⟩
         ap from (pp c)             =⟨ From.pp-β c ⟩
         glue c =∎))

  generic-pushout : Pushout d ≃ T
  generic-pushout = equiv to from to-from from-to

_⊔^[_]_/_ : ∀ {i j k} (A : Type i) (C : Type k) (B : Type j)
  (fg : (C → A) × (C → B)) → Type (lmax (lmax i j) k)
A ⊔^[ C ] B  / (f , g) = Pushout (span A B C f g)

⊙Pushout : ∀ {i j k} (d : ⊙Span {i} {j} {k}) → Ptd _
⊙Pushout d = ⊙[ Pushout (⊙Span-to-Span d) , left (pt (⊙Span.X d)) ]

module _ {i j k} (d : ⊙Span {i} {j} {k}) where

  open ⊙Span d

  ⊙left : X ⊙→ ⊙Pushout d
  ⊙left = (left , idp)

  ⊙right : Y ⊙→ ⊙Pushout d
  ⊙right =
    (right , ap right (! (snd g)) ∙ ! (glue (pt Z)) ∙' ap left (snd f))

  ⊙glue : (⊙left ⊙∘ f) == (⊙right ⊙∘ g)
  ⊙glue = pair=
    (λ= glue)
    (↓-app=cst-in $
      ap left (snd f) ∙ idp
        =⟨ ∙-unit-r _ ⟩
      ap left (snd f)
        =⟨ lemma (glue (pt Z)) (ap right (snd g)) (ap left (snd f)) ⟩
      glue (pt Z) ∙ ap right (snd g)
      ∙ ! (ap right (snd g)) ∙ ! (glue (pt Z)) ∙' ap left (snd f)
        =⟨ !-ap right (snd g)
           |in-ctx (λ w → glue (pt Z) ∙ ap right (snd g) ∙ w
                          ∙ ! (glue (pt Z)) ∙' ap left (snd f)) ⟩
      glue (pt Z) ∙ ap right (snd g)
      ∙ ap right (! (snd g)) ∙ ! (glue (pt Z)) ∙' ap left (snd f)
        =⟨ ! (app=-β glue (pt Z))
           |in-ctx (λ w → w ∙ ap right (snd g) ∙ ap right (! (snd g))
                            ∙ ! (glue (pt Z)) ∙' ap left (snd f)) ⟩
      app= (λ= glue) (pt Z) ∙ ap right (snd g)
      ∙ ap right (! (snd g)) ∙ ! (glue (pt Z)) ∙' ap left (snd f) =∎)
    where
    lemma : ∀ {i} {A : Type i} {x y z w : A}
      (p : x == y) (q : y == z) (r : x == w)
      → r == p ∙ q ∙ ! q ∙ ! p ∙' r
    lemma idp idp idp = idp

⊙pushout-J : ∀ {i j k l} (P : ⊙Span → Type l)
  → ({A : Type i} {B : Type j} (Z : Ptd k) (f : de⊙ Z → A) (g : de⊙ Z → B)
     → P (⊙span ⊙[ A , f (pt Z) ] ⊙[ B , g (pt Z) ] Z (f , idp) (g , idp)))
  → ((ps : ⊙Span) → P ps)
⊙pushout-J P t (⊙span ⊙[ _ , ._ ] ⊙[ _ , ._ ] Z (f , idp) (g , idp)) = t Z f g

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- New NO_POSITIVITY_CHECK pragma for data definitions and mutual
-- blocks

-- Skipping an old-style mutual block: Somewhere within a `mutual`
-- block before a data definition.
mutual
  data Cheat : Set where
    cheat : Oops → Cheat

  {-# NO_POSITIVITY_CHECK #-}
  data Oops : Set where
    oops : (Cheat → Cheat) → Oops


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.RingSolver.CommRingEvalHom where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.FinData
open import Cubical.Data.Vec
open import Cubical.Data.Bool.Base

open import Cubical.Algebra.RingSolver.RawAlgebra
open import Cubical.Algebra.RingSolver.CommRingHornerForms
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring

private
  variable
    ℓ : Level

module HomomorphismProperties (R : CommRing {ℓ}) where
  private
    νR = CommRing→RawℤAlgebra R
  open CommRingStr (snd R)
  open Theory (CommRing→Ring R)
  open IteratedHornerOperations νR

  EvalHom+0 : (n : ℕ) (P : IteratedHornerForms νR n) (xs : Vec ⟨ νR ⟩ n)
      → eval n (0ₕ +ₕ P) xs ≡ eval n P xs
  EvalHom+0 ℕ.zero (const x) [] = cong (scalar R) (+Ridℤ x)
  EvalHom+0 (ℕ.suc n) P xs = refl

  Eval0H : (n : ℕ) (xs : Vec ⟨ νR ⟩ n)
         → eval {A = νR} n 0ₕ xs ≡ 0r
  Eval0H .ℕ.zero [] = refl
  Eval0H .(ℕ.suc _) (x ∷ xs) = refl

  combineCasesEval :
    {n : ℕ}  (P : IteratedHornerForms νR (ℕ.suc n)) (Q : IteratedHornerForms νR n)
    (x : (fst R)) (xs : Vec ⟨ νR ⟩ n)
    → eval (ℕ.suc n) (P ·X+ Q) (x ∷ xs) ≡ (eval (ℕ.suc n) P (x ∷ xs)) · x + eval n Q xs
  combineCasesEval {n = n} 0H Q x xs =
    eval n Q xs               ≡⟨ sym (+Lid _) ⟩
    0r + eval n Q xs          ≡[ i ]⟨ 0LeftAnnihilates x (~ i) + eval n Q xs ⟩
    0r · x + eval n Q xs ∎
  combineCasesEval {n = n} (P ·X+ P₁) Q x xs = refl

  Eval1ₕ : (n : ℕ) (xs : Vec ⟨ νR ⟩ n)
         → eval {A = νR} n 1ₕ xs ≡ 1r
  Eval1ₕ .ℕ.zero [] = refl
  Eval1ₕ (ℕ.suc n) (x ∷ xs) =
    eval (ℕ.suc n) 1ₕ (x ∷ xs)                             ≡⟨ refl ⟩
    eval (ℕ.suc n) (0H ·X+ 1ₕ) (x ∷ xs)                    ≡⟨ combineCasesEval 0H 1ₕ x xs ⟩
    eval {A = νR} (ℕ.suc n) 0H (x ∷ xs) · x + eval n 1ₕ xs ≡⟨ cong (λ u → u · x + eval n 1ₕ xs)
                                                                   (Eval0H _ (x ∷ xs)) ⟩
    0r · x + eval n 1ₕ xs                                   ≡⟨ cong (λ u → 0r · x + u)
                                                                    (Eval1ₕ _ xs) ⟩
    0r · x + 1r                                            ≡⟨ cong (λ u → u + 1r)
                                                                   (0LeftAnnihilates _) ⟩
    0r + 1r                                                ≡⟨ +Lid _ ⟩
    1r ∎

  -EvalDist :
    (n : ℕ) (P : IteratedHornerForms νR n) (xs : Vec ⟨ νR ⟩ n)
    → eval n (-ₕ P) xs ≡ - eval n P xs
  -EvalDist .ℕ.zero (const x) []   = -DistScalar R x
  -EvalDist          n       0H  xs =
    eval n (-ₕ 0H) xs  ≡⟨ Eval0H n xs ⟩
    0r                        ≡⟨ sym 0Selfinverse ⟩
    - 0r                      ≡⟨ cong -_ (sym (Eval0H n xs)) ⟩
    - eval n 0H xs     ∎
  -EvalDist .(ℕ.suc _) (P ·X+ Q) (x ∷ xs) =
      eval (ℕ.suc _) (-ₕ (P ·X+ Q)) (x ∷ xs)
    ≡⟨ refl ⟩
      eval (ℕ.suc _) ((-ₕ P) ·X+ (-ₕ Q)) (x ∷ xs)
    ≡⟨ combineCasesEval (-ₕ P) (-ₕ Q) x xs ⟩
      (eval (ℕ.suc _) (-ₕ P) (x ∷ xs)) · x + eval _ (-ₕ Q) xs
    ≡⟨ cong (λ u → u · x + eval _ (-ₕ Q) xs) (-EvalDist _ P _) ⟩
      (- eval (ℕ.suc _) P (x ∷ xs)) · x + eval _ (-ₕ Q) xs
    ≡⟨ cong (λ u → (- eval (ℕ.suc _) P (x ∷ xs)) · x + u) (-EvalDist _ Q _) ⟩
      (- eval (ℕ.suc _) P (x ∷ xs)) · x + - eval _ Q xs
    ≡[ i ]⟨ -DistL· (eval (ℕ.suc _) P (x ∷ xs)) x i +  - eval _ Q xs ⟩
      - ((eval (ℕ.suc _) P (x ∷ xs)) · x) + (- eval _ Q xs)
    ≡⟨ -Dist _ _ ⟩
      - ((eval (ℕ.suc _) P (x ∷ xs)) · x + eval _ Q xs)
    ≡[ i ]⟨ - combineCasesEval P Q x xs (~ i) ⟩
      - eval (ℕ.suc _) (P ·X+ Q) (x ∷ xs) ∎

  combineCases+ : (n : ℕ) (P Q : IteratedHornerForms νR (ℕ.suc n))
                  (r s : IteratedHornerForms νR n)
                  (xs : Vec ⟨ νR ⟩ (ℕ.suc n))
                  → eval (ℕ.suc n) ((P ·X+ r) +ₕ (Q ·X+ s)) xs
                  ≡ eval (ℕ.suc n) ((P +ₕ Q) ·X+ (r +ₕ s)) xs
  combineCases+ ℕ.zero P Q r s xs with (P +ₕ Q) | (r +ₕ s)
  ... | (_ ·X+ _) | const (pos (ℕ.suc _)) = refl
  ... | (_ ·X+ _) | const (negsuc _) = refl
  ... | (_ ·X+ _) | const (pos ℕ.zero)  = refl
  ... | 0H  | const (pos (ℕ.suc _)) = refl
  ... | 0H  | const (negsuc _) = refl
  combineCases+ ℕ.zero P Q r s (x ∷ []) | 0H  | const (pos ℕ.zero) = refl
  combineCases+ (ℕ.suc n) P Q r s (x ∷ xs) with (P +ₕ Q) | (r +ₕ s)
  ... | (_ ·X+ _) | (_ ·X+ _) = refl
  ... | (_ ·X+ _) | 0H  = refl
  ... | 0H        | (_ ·X+ _) = refl
  ... | 0H        | 0H  = sym (Eval0H (ℕ.suc n) xs)

  +Homeval :
    (n : ℕ) (P Q : IteratedHornerForms νR n) (xs : Vec ⟨ νR ⟩ n)
    → eval n (P +ₕ Q) xs ≡ (eval n P xs) + (eval n Q xs)
  +Homeval .ℕ.zero (const x) (const y) [] = +HomScalar R x y
  +Homeval n 0H Q xs =
    eval n (0H +ₕ Q) xs            ≡⟨ refl ⟩
    eval n Q xs                    ≡⟨ sym (+Lid _) ⟩
    0r + eval n Q xs               ≡⟨ cong (λ u → u + eval n Q xs) (sym (Eval0H n xs)) ⟩
    eval n 0H xs + eval n Q xs ∎
  +Homeval .(ℕ.suc _) (P ·X+ Q) 0H xs =
    eval (ℕ.suc _) ((P ·X+ Q) +ₕ 0H) xs                    ≡⟨ refl ⟩
    eval (ℕ.suc _) (P ·X+ Q) xs                            ≡⟨ sym (+Rid _) ⟩
    eval (ℕ.suc _) (P ·X+ Q) xs + 0r
   ≡⟨ cong (λ u → eval (ℕ.suc _) (P ·X+ Q) xs + u) (sym (Eval0H _ xs)) ⟩
    eval (ℕ.suc _) (P ·X+ Q) xs + eval (ℕ.suc _) 0H xs ∎
  +Homeval .(ℕ.suc _) (P ·X+ Q) (S ·X+ T) (x ∷ xs) =
    eval (ℕ.suc _) ((P ·X+ Q) +ₕ (S ·X+ T)) (x ∷ xs)
   ≡⟨ combineCases+ _ P S Q T (x ∷ xs) ⟩
    eval (ℕ.suc _) ((P +ₕ S) ·X+ (Q +ₕ T)) (x ∷ xs)
   ≡⟨ combineCasesEval (P +ₕ S) (Q +ₕ T) x xs ⟩
    (eval (ℕ.suc _) (P +ₕ S) (x ∷ xs)) · x + eval _ (Q +ₕ T) xs
   ≡⟨ cong (λ u → (eval (ℕ.suc _) (P +ₕ S) (x ∷ xs)) · x + u) (+Homeval _ Q T xs) ⟩
    (eval (ℕ.suc _) (P +ₕ S) (x ∷ xs)) · x + (eval _ Q xs + eval _ T xs)
   ≡⟨ cong (λ u → u · x + (eval _ Q xs + eval _ T xs)) (+Homeval (ℕ.suc _) P S (x ∷ xs)) ⟩
    (eval (ℕ.suc _) P (x ∷ xs) + eval (ℕ.suc _) S (x ∷ xs)) · x
    + (eval _ Q xs + eval _ T xs)
   ≡⟨ cong (λ u → u + (eval _ Q xs + eval _ T xs)) (·Ldist+ _ _ _) ⟩
    (eval (ℕ.suc _) P (x ∷ xs)) · x + (eval (ℕ.suc _) S (x ∷ xs)) · x
    + (eval _ Q xs + eval _ T xs)
   ≡⟨ +ShufflePairs _ _ _ _ ⟩
    ((eval (ℕ.suc _) P (x ∷ xs)) · x + eval _ Q xs)
    + ((eval (ℕ.suc _) S (x ∷ xs)) · x + eval _ T xs)
   ≡[ i ]⟨ combineCasesEval P Q x xs (~ i) + combineCasesEval S T x xs (~ i) ⟩
    eval (ℕ.suc _) (P ·X+ Q) (x ∷ xs)
    + eval (ℕ.suc _) (S ·X+ T) (x ∷ xs) ∎

  ⋆Homeval : (n : ℕ)
             (r : IteratedHornerForms νR n)
             (P : IteratedHornerForms νR (ℕ.suc n)) (x : ⟨ νR ⟩) (xs : Vec ⟨ νR ⟩ n)
           → eval (ℕ.suc n) (r ⋆ P) (x ∷ xs) ≡ eval n r xs · eval (ℕ.suc n) P (x ∷ xs)

  ⋆0LeftAnnihilates :
    (n : ℕ) (P : IteratedHornerForms νR (ℕ.suc n)) (xs : Vec ⟨ νR ⟩ (ℕ.suc n))
    → eval (ℕ.suc n) (0ₕ ⋆ P) xs ≡ 0r
  ⋆0LeftAnnihilates n 0H xs = Eval0H (ℕ.suc n) xs
  ⋆0LeftAnnihilates ℕ.zero (P ·X+ Q) (x ∷ xs) = refl
  ⋆0LeftAnnihilates (ℕ.suc n) (P ·X+ Q) (x ∷ xs) = refl

  ·0LeftAnnihilates :
    (n : ℕ) (P : IteratedHornerForms νR n) (xs : Vec ⟨ νR ⟩ n)
    → eval n (0ₕ ·ₕ P) xs ≡ 0r
  ·0LeftAnnihilates .ℕ.zero (const x) xs =
    eval ℕ.zero (const _) xs ≡⟨ Eval0H _ xs ⟩ 0r ∎
  ·0LeftAnnihilates .(ℕ.suc _) 0H xs = Eval0H _ xs
  ·0LeftAnnihilates .(ℕ.suc _) (P ·X+ P₁) xs = Eval0H _ xs

  ·Homeval : (n : ℕ) (P Q : IteratedHornerForms νR n) (xs : Vec ⟨ νR ⟩ n)
    → eval n (P ·ₕ Q) xs ≡ (eval n P xs) · (eval n Q xs)

  combineCases⋆ : (n : ℕ) (xs : Vec ⟨ νR ⟩ (ℕ.suc n))
                → (r : IteratedHornerForms νR n)
                → (P : IteratedHornerForms νR (ℕ.suc n))
                → (Q : IteratedHornerForms νR n)
                → eval (ℕ.suc n) (r ⋆ (P ·X+ Q)) xs ≡ eval (ℕ.suc n) ((r ⋆ P) ·X+ (r ·ₕ Q)) xs
  combineCases⋆ .ℕ.zero (x ∷ []) (const (pos ℕ.zero)) P Q =
      eval _ (const (pos ℕ.zero) ⋆ (P ·X+ Q))  (x ∷ [])                          ≡⟨ refl ⟩
      eval _ 0ₕ  (x ∷ [])                                                         ≡⟨ refl ⟩
      0r             ≡⟨ sym (+Rid _) ⟩
      0r + 0r        ≡[ i ]⟨ 0LeftAnnihilates x (~ i) + 0r ⟩
      0r · x + 0r    ≡[ i ]⟨ ⋆0LeftAnnihilates _ P (x ∷ []) (~ i) · x + ·0LeftAnnihilates _ Q [] (~ i) ⟩
      eval _ (const (pos ℕ.zero) ⋆ P) (x ∷ []) · x + eval _ (const (pos ℕ.zero) ·ₕ Q) []
    ≡⟨ sym (combineCasesEval (const (pos ℕ.zero) ⋆ P) (const (pos ℕ.zero) ·ₕ Q) x []) ⟩
      eval _ ((const (pos ℕ.zero) ⋆ P) ·X+ (const (pos ℕ.zero) ·ₕ Q))  (x ∷ []) ∎
  combineCases⋆ .ℕ.zero (x ∷ []) (const (pos (ℕ.suc n))) P Q = refl
  combineCases⋆ .ℕ.zero (x ∷ []) (const (negsuc n)) P Q = refl
  combineCases⋆ .(ℕ.suc _) (x ∷ xs) 0H P Q =
      eval _ (0H ⋆ (P ·X+ Q))  (x ∷ xs)    ≡⟨ refl ⟩
      eval _ 0ₕ  (x ∷ [])                  ≡⟨ refl ⟩
      0r             ≡⟨ sym (+Rid _) ⟩
      0r + 0r        ≡[ i ]⟨ 0LeftAnnihilates x (~ i) + 0r ⟩
      0r · x + 0r    ≡[ i ]⟨ ⋆0LeftAnnihilates _ P (x ∷ xs) (~ i) · x + ·0LeftAnnihilates _ Q xs (~ i) ⟩
      eval _ (0H ⋆ P) (x ∷ xs) · x + eval _ (0H ·ₕ Q) xs
    ≡⟨ sym (combineCasesEval (0H ⋆ P) (0H ·ₕ Q) x xs) ⟩
      eval _ ((0H ⋆ P) ·X+ (0H ·ₕ Q))  (x ∷ xs) ∎
  combineCases⋆ .(ℕ.suc _) (x ∷ xs) (r ·X+ r₁) P Q = refl

  ⋆Homeval n r 0H x xs =
    eval (ℕ.suc n) (r ⋆ 0H) (x ∷ xs)         ≡⟨ refl ⟩
    0r                                       ≡⟨ sym (0RightAnnihilates _) ⟩
    eval n r xs · 0r                         ≡⟨ refl ⟩
    eval n r xs · eval {A = νR} (ℕ.suc n) 0H (x ∷ xs) ∎
  ⋆Homeval n r (P ·X+ Q) x xs =
      eval (ℕ.suc n) (r ⋆ (P ·X+ Q)) (x ∷ xs)                    ≡⟨ combineCases⋆ n (x ∷ xs) r P Q ⟩
      eval (ℕ.suc n) ((r ⋆ P) ·X+ (r ·ₕ Q)) (x ∷ xs)
    ≡⟨ combineCasesEval (r ⋆ P) (r ·ₕ Q) x xs ⟩
      (eval (ℕ.suc n) (r ⋆ P) (x ∷ xs)) · x + eval n (r ·ₕ Q) xs
    ≡⟨ cong (λ u → u · x + eval n (r ·ₕ Q) xs) (⋆Homeval n r P x xs) ⟩
      (eval n r xs · eval (ℕ.suc n) P (x ∷ xs)) · x + eval n (r ·ₕ Q) xs
    ≡⟨ cong (λ u → (eval n r xs · eval (ℕ.suc n) P (x ∷ xs)) · x + u) (·Homeval n r Q xs) ⟩
      (eval n r xs · eval (ℕ.suc n) P (x ∷ xs)) · x + eval n r xs · eval n Q xs
    ≡⟨ cong (λ u → u  + eval n r xs · eval n Q xs) (sym (·Assoc _ _ _)) ⟩
      eval n r xs · (eval (ℕ.suc n) P (x ∷ xs) · x) + eval n r xs · eval n Q xs
    ≡⟨ sym (·Rdist+ _ _ _) ⟩
      eval n r xs · ((eval (ℕ.suc n) P (x ∷ xs) · x) + eval n Q xs)
    ≡[ i ]⟨ eval n r xs · combineCasesEval P Q x xs (~ i) ⟩
      eval n r xs · eval (ℕ.suc n) (P ·X+ Q) (x ∷ xs) ∎

  combineCases :
    (n : ℕ) (Q : IteratedHornerForms νR n) (P S : IteratedHornerForms νR (ℕ.suc n))
    (xs : Vec ⟨ νR ⟩ (ℕ.suc n))
    → eval (ℕ.suc n) ((P ·X+ Q) ·ₕ S) xs ≡ eval (ℕ.suc n) (((P ·ₕ S) ·X+ 0ₕ) +ₕ (Q ⋆ S)) xs
  combineCases n Q P S (x ∷ xs) with (P ·ₕ S)
  ... | 0H =
    eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs)                ≡⟨ sym (+Lid _) ⟩
    0r + eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs)           ≡⟨ cong (λ u → u + eval _ (Q ⋆ S) (x ∷ xs)) lemma ⟩
    eval (ℕ.suc n) (0H ·X+ 0ₕ) (x ∷ xs)
    + eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs)              ≡⟨ sym (+Homeval (ℕ.suc n)
                                                      (0H ·X+ 0ₕ) (Q ⋆ S) (x ∷ xs)) ⟩
    eval (ℕ.suc n) ((0H ·X+ 0ₕ) +ₕ (Q ⋆ S)) (x ∷ xs) ∎
    where lemma : 0r ≡ eval (ℕ.suc n) (0H ·X+ 0ₕ) (x ∷ xs)
          lemma = 0r
                ≡⟨ sym (+Rid _) ⟩
                  0r + 0r
                ≡⟨ cong (λ u → u + 0r) (sym (0LeftAnnihilates _)) ⟩
                  0r · x + 0r
                ≡⟨ cong (λ u → 0r · x + u) (sym (Eval0H _ xs)) ⟩
                  0r · x + eval n 0ₕ xs
                ≡⟨ cong (λ u → u · x + eval n 0ₕ xs) (sym (Eval0H _ (x ∷ xs))) ⟩
                  eval {A = νR} (ℕ.suc n) 0H (x ∷ xs) · x + eval n 0ₕ xs
                ≡[ i ]⟨ combineCasesEval 0H 0ₕ x xs (~ i) ⟩
                  eval (ℕ.suc n) (0H ·X+ 0ₕ) (x ∷ xs) ∎
  ... | (_ ·X+ _) = refl

  ·Homeval .ℕ.zero (const x) (const y) [] = ·HomScalar R x y
  ·Homeval (ℕ.suc n) 0H Q xs =
    eval (ℕ.suc n) (0H ·ₕ Q) xs        ≡⟨ Eval0H _ xs ⟩
    0r                                 ≡⟨ sym (0LeftAnnihilates _) ⟩
    0r · eval (ℕ.suc n) Q xs          ≡⟨ cong (λ u → u · eval _ Q xs) (sym (Eval0H _ xs)) ⟩
    eval (ℕ.suc n) 0H xs · eval (ℕ.suc n) Q xs ∎
  ·Homeval (ℕ.suc n) (P ·X+ Q) S (x ∷ xs) =
      eval (ℕ.suc n) ((P ·X+ Q) ·ₕ S) (x ∷ xs)
    ≡⟨ combineCases n Q P S (x ∷ xs) ⟩
      eval (ℕ.suc n) (((P ·ₕ S) ·X+ 0ₕ) +ₕ (Q ⋆ S)) (x ∷ xs)
    ≡⟨ +Homeval (ℕ.suc n) ((P ·ₕ S) ·X+ 0ₕ) (Q ⋆ S) (x ∷ xs) ⟩
      eval (ℕ.suc n) ((P ·ₕ S) ·X+ 0ₕ) (x ∷ xs) + eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs)
    ≡⟨ cong (λ u → u + eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs)) (combineCasesEval (P ·ₕ S) 0ₕ x xs) ⟩
      (eval (ℕ.suc n) (P ·ₕ S) (x ∷ xs) · x + eval n 0ₕ xs)
      + eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs)
    ≡⟨ cong (λ u → u + eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs))
          ((eval (ℕ.suc n) (P ·ₕ S) (x ∷ xs) · x + eval n 0ₕ xs)
         ≡⟨ cong (λ u → eval (ℕ.suc n) (P ·ₕ S) (x ∷ xs) · x + u) (Eval0H _ xs) ⟩
           (eval (ℕ.suc n) (P ·ₕ S) (x ∷ xs) · x + 0r)
         ≡⟨ +Rid _ ⟩
           (eval (ℕ.suc n) (P ·ₕ S) (x ∷ xs) · x)
         ≡⟨ cong (λ u → u · x) (·Homeval (ℕ.suc n) P S (x ∷ xs)) ⟩
           ((eval (ℕ.suc n) P (x ∷ xs) · eval (ℕ.suc n) S (x ∷ xs)) · x)
         ≡⟨ sym (·Assoc _ _ _) ⟩
           (eval (ℕ.suc n) P (x ∷ xs) · (eval (ℕ.suc n) S (x ∷ xs) · x))
         ≡⟨ cong (λ u → eval (ℕ.suc n) P (x ∷ xs) · u) (·-comm _ _) ⟩
           (eval (ℕ.suc n) P (x ∷ xs) · (x · eval (ℕ.suc n) S (x ∷ xs)))
         ≡⟨ ·Assoc _ _ _ ⟩
           (eval (ℕ.suc n) P (x ∷ xs) · x) · eval (ℕ.suc n) S (x ∷ xs)
          ∎) ⟩
      (eval (ℕ.suc n) P (x ∷ xs) · x) · eval (ℕ.suc n) S (x ∷ xs)
      + eval (ℕ.suc n) (Q ⋆ S) (x ∷ xs)
    ≡⟨ cong (λ u → (eval (ℕ.suc n) P (x ∷ xs) · x) · eval (ℕ.suc n) S (x ∷ xs) + u)
            (⋆Homeval n Q S x xs) ⟩
      (eval (ℕ.suc n) P (x ∷ xs) · x) · eval (ℕ.suc n) S (x ∷ xs)
      + eval n Q xs · eval (ℕ.suc n) S (x ∷ xs)
    ≡⟨ sym (·Ldist+ _ _ _) ⟩
      ((eval (ℕ.suc n) P (x ∷ xs) · x) + eval n Q xs) · eval (ℕ.suc n) S (x ∷ xs)
    ≡⟨ cong (λ u → u · eval (ℕ.suc n) S (x ∷ xs)) (sym (combineCasesEval P Q x xs)) ⟩
      eval (ℕ.suc n) (P ·X+ Q) (x ∷ xs) · eval (ℕ.suc n) S (x ∷ xs) ∎

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Structure.Operator.Algebra where

open import Lang.Instance
open import Logic.Predicate
import      Lvl
open import Structure.Function.Domain
open import Structure.Operator.Field
open import Structure.Operator.Monoid
open import Structure.Operator.Properties
open import Structure.Operator.Ring
open import Structure.Operator.Ring.Homomorphism
open import Structure.Operator.Vector
open import Structure.Operator.Vector.LinearMap
open import Structure.Setoid
open import Type

module _
  {ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ}
  {V : Type{ℓᵥ}} ⦃ _ : Equiv{ℓᵥₑ}(V) ⦄
  {S : Type{ℓₛ}} ⦃ _ : Equiv{ℓₛₑ}(S) ⦄
  (_+ᵥ_ : V → V → V)
  (_⋅ᵥ_ : V → V → V)
  (_⋅ₛᵥ_ : S → V → V)
  (_+ₛ_ : S → S → S)
  (_⋅ₛ_ : S → S → S)
  where

  record Algebra : Type{ℓₛₑ Lvl.⊔ ℓₛ Lvl.⊔ ℓᵥₑ Lvl.⊔ ℓᵥ} where
    constructor intro
    field
      ⦃ vectorSpace ⦄      : VectorSpace(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_)
      ⦃ [⋅ᵥ]-bilinearity ⦄ : BilinearOperator vectorSpace (_⋅ᵥ_)
    open VectorSpace(vectorSpace)
      renaming (ring to ringₛ)
      public

    ringᵥ : ⦃ Associativity(_⋅ᵥ_) ⦄ → ⦃ ∃(Identity(_⋅ᵥ_)) ⦄ → Ring(_+ᵥ_)(_⋅ᵥ_)
    Rng.[+]-commutative-group    (Ring.rng   ringᵥ) = vectorCommutativeGroup
    Rng.[⋅]-binary-operator      (Ring.rng   ringᵥ) = BilinearMap.binaryOperator [⋅ᵥ]-bilinearity
    Rng.[⋅]-associativity        (Ring.rng   ringᵥ) = infer
    Rng.[⋅][+]-distributivityₗ   (Ring.rng   ringᵥ) = BilinearOperator.[+ᵥ]-distributivityₗ vectorSpace (_⋅ᵥ_) [⋅ᵥ]-bilinearity
    Rng.[⋅][+]-distributivityᵣ   (Ring.rng   ringᵥ) = BilinearOperator.[+ᵥ]-distributivityᵣ vectorSpace (_⋅ᵥ_) [⋅ᵥ]-bilinearity
    Unity.[⋅]-identity-existence (Ring.unity ringᵥ) = infer

  -- TODO: I found some conflicting definitions for a star algebra from different sources. What is a reasonable definition?
  record ⋆-algebra (_⋆ᵥ : V → V) (_⋆ₛ : S → S) : Type{ℓₛₑ Lvl.⊔ ℓₛ Lvl.⊔ ℓᵥₑ Lvl.⊔ ℓᵥ} where
    constructor intro
    field
      ⦃ algebra ⦄ : Algebra
    open Algebra(algebra) public

    field
      ⦃ [⋅ᵥ]-commutativity ⦄             : Commutativity(_⋅ᵥ_)
      ⦃ [⋅ᵥ]-associativity ⦄             : Associativity(_⋅ᵥ_)
      ⦃ [⋅ᵥ]-identity ⦄                  : ∃(Identity(_⋅ᵥ_))
      ⦃ [⋆ₛ]-involution ⦄                : Involution(_⋆ᵥ)
      ⦃ [⋆ᵥ]-involution ⦄                : Involution(_⋆ᵥ)
      [⋆ᵥ]-distribute-over-[⋅ₛᵥ]-to-[⋆ₛ] : ∀{s}{v} → ((s ⋅ₛᵥ v)⋆ᵥ ≡ (s ⋆ₛ) ⋅ₛᵥ (v ⋆ᵥ))
      ⦃ [⋆ₛ]-antihomomorphism ⦄          : Antihomomorphism ringₛ ringₛ (_⋆ₛ)
      ⦃ [⋆ᵥ]-antihomomorphism ⦄          : Antihomomorphism ringᵥ ringᵥ (_⋆ᵥ)


text:
module STLC.Kovacs.Normalisation where

open import STLC.Kovacs.NormalForm public

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

-- (Tyᴺ)
infix 3 _⊩_
_⊩_ : 𝒞 → 𝒯 → Set

Γ ⊩ ⎵      = Γ ⊢ⁿᶠ ⎵

Γ ⊩ A ⇒ B = ∀ {Γ′} → (η : Γ′ ⊇ Γ) (a : Γ′ ⊩ A)
                     → Γ′ ⊩ B

-- (Conᴺ ; ∙ ; _,_)
infix 3 _⊩⋆_
data _⊩⋆_ : 𝒞 → 𝒞 → Set
  where
    ∅   : ∀ {Γ} → Γ ⊩⋆ ∅

    _,_ : ∀ {Γ Ξ A} → (ρ : Γ ⊩⋆ Ξ) (a : Γ ⊩ A)
                    → Γ ⊩⋆ Ξ , A

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

-- (Tyᴺₑ)
acc : ∀ {A Γ Γ′} → Γ′ ⊇ Γ → Γ ⊩ A → Γ′ ⊩ A
acc {⎵}      η M = renⁿᶠ η M
acc {A ⇒ B} η f = λ η′ a → f (η ○ η′) a

-- (Conᴺₑ)
-- NOTE: _⬖_ = acc⋆
_⬖_ : ∀ {Γ Γ′ Ξ} → Γ ⊩⋆ Ξ → Γ′ ⊇ Γ → Γ′ ⊩⋆ Ξ
∅       ⬖ η = ∅
(ρ , a) ⬖ η = ρ ⬖ η , acc η a

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

-- (∈ᴺ)
getᵥ : ∀ {Γ Ξ A} → Γ ⊩⋆ Ξ → Ξ ∋ A → Γ ⊩ A
getᵥ (ρ , a) zero    = a
getᵥ (ρ , a) (suc i) = getᵥ ρ i

-- (Tmᴺ)
eval : ∀ {Γ Ξ A} → Γ ⊩⋆ Ξ → Ξ ⊢ A → Γ ⊩ A
eval ρ (𝓋 i)   = getᵥ ρ i
eval ρ (ƛ M)   = λ η a → eval (ρ ⬖ η , a) M
eval ρ (M ∙ N) = eval ρ M idₑ (eval ρ N)

mutual
  -- (qᴺ)
  reify : ∀ {A Γ} → Γ ⊩ A → Γ ⊢ⁿᶠ A
  reify {⎵}      M = M
  reify {A ⇒ B} f = ƛ (reify (f (wkₑ idₑ) (reflect 0)))

  -- (uᴺ)
  reflect : ∀ {A Γ} → Γ ⊢ⁿᵉ A → Γ ⊩ A
  reflect {⎵}      M = ne M
  reflect {A ⇒ B} M = λ η a → reflect (renⁿᵉ η M ∙ reify a)

-- (uᶜᴺ)
idᵥ : ∀ {Γ} → Γ ⊩⋆ Γ
idᵥ {∅}     = ∅
idᵥ {Γ , A} = idᵥ ⬖ wkₑ idₑ , reflect 0

-- (nf)
nf : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ⁿᶠ A
nf M = reify (eval idᵥ M)

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
open import Oscar.Prelude
open import Oscar.Data.Decidable
open import Oscar.Data.Proposequality

module Oscar.Class.IsDecidable where

record IsDecidable {𝔬} (𝔒 : Ø 𝔬) : Ø 𝔬 where
  infix 4 _≟_
  field
    _≟_ : (x y : 𝔒) → Decidable (x ≡ y)

open IsDecidable ⦃ … ⦄ public


text:
module Syntax where

{-
open import Data.Nat hiding (_>_)
open import Data.Fin
open import Data.Product
open import Data.Bool
open import Relation.Binary.PropositionalEquality
-}

open import StdLibStuff

erase-subst :
 (X : Set) → (Y : X → Set) →
 (F : {x : X} → Y x) →
 (x₁ x₂ : X) →
 (eq : x₁ ≡ x₂) →
 (P : Y x₂ → Set) →
 P F →
 P (subst Y eq F)
erase-subst X Y F .x₂ x₂ refl P h = h

-- type, ctx

data Type (n : ℕ) : Set where
 $o : Type n
 $i : Fin n → Type n
 _>_ : Type n → Type n → Type n

data Ctx (n : ℕ) : Set where
 ε : Ctx n
 _∷_ : Type n → Ctx n → Ctx n

data Var : {n : ℕ} → Ctx n → Set where
 this : ∀ {n t} → {Γ : Ctx n} → Var (t ∷ Γ)
 next : ∀ {n t} → {Γ : Ctx n} → Var Γ → Var (t ∷ Γ)

lookup-Var : ∀ {n} → (Γ : Ctx n) → Var Γ → Type n
lookup-Var ε ()
lookup-Var (t ∷ _) this = t
lookup-Var (_ ∷ Γ) (next x) = lookup-Var Γ x

_++_ : ∀ {n} → Ctx n → Ctx n → Ctx n
ε ++ Γ = Γ
(t ∷ Γ₁) ++ Γ₂ = t ∷ (Γ₁ ++ Γ₂)

_r++_ : ∀ {n} → Ctx n → Ctx n → Ctx n
ε r++ Γ = Γ
(t ∷ Γ₁) r++ Γ₂ = Γ₁ r++ (t ∷ Γ₂)

-- stt formula

data Form : {n : ℕ} → Ctx n → Type n → Set where
 var : ∀ {n} → {Γ : Ctx n} {t : Type n} → (x : Var Γ) → lookup-Var Γ x ≡ t → Form Γ t
 N : ∀ {n} → {Γ : Ctx n} → Form Γ ($o > $o)
 A : ∀ {n} → {Γ : Ctx n} → Form Γ ($o > ($o > $o))
 Π : ∀ {n α} → {Γ : Ctx n} → Form Γ ((α > $o) > $o)
 i : ∀ {n α} → {Γ : Ctx n} → Form Γ ((α > $o) > α)
 app : ∀ {n α β} → {Γ : Ctx n} → Form Γ (α > β) → Form Γ α → Form Γ β
 lam : ∀ {n β} → {Γ : Ctx n} → (α : _) → Form (α ∷ Γ) β → Form Γ (α > β)

-- abbreviations (TPTP-like notation)

~ : ∀ {n} → {Γ : Ctx n} → Form Γ $o → Form Γ $o
~ F = app N F

_||_ : ∀ {n} → {Γ : Ctx n} → Form Γ $o → Form Γ $o → Form Γ $o
F || G = app (app A F) G

_&_ : ∀ {n} → {Γ : Ctx n} → Form Γ $o → Form Γ $o → Form Γ $o
F & G = ~ ((~ F) || (~ G))

_=>_ : ∀ {n} → {Γ : Ctx n} → Form Γ $o → Form Γ $o → Form Γ $o
F => G = (~ F) || G

![_]_ : ∀ {n} → {Γ : Ctx n} → (α : Type n) → Form (α ∷ Γ) $o → Form Γ $o
![ α ] F = app Π (lam α F)

?[_]_ : ∀ {n} → {Γ : Ctx n} → (α : Type n) → Form (α ∷ Γ) $o → Form Γ $o
?[ α ] F = ~ (![ α ] ~ F)

ι : ∀ {n} → {Γ : Ctx n} → (α : Type n) → Form (α ∷ Γ) $o → Form Γ α
ι α F = app i (lam α F)

Q : ∀ {n} → {Γ : Ctx n} → (α : Type n) → Form Γ (α > (α > $o))
Q α = lam α (lam α (![ α > $o ] (app (var this refl) (var (next (next this)) refl) => app (var this refl) (var (next this) refl))))

_==_ : ∀ {n} → {Γ : Ctx n} → {α : Type n} → Form Γ α → Form Γ α → Form Γ $o
F == G = app (app (Q _) F) G

_<=>_ : ∀ {n} → {Γ : Ctx n} → Form Γ $o → Form Γ $o → Form Γ $o
F <=> G = (F => G) & (G => F)

$true : ∀ {n} → {Γ : Ctx n} → Form Γ $o
$true = ![ $o ] (var this refl => var this refl)

$false : ∀ {n} → {Γ : Ctx n} → Form Γ $o
$false = ![ $o ] var this refl

^[_]_ : ∀ {n Γ t₂} → (t₁ : Type n) → Form (t₁ ∷ Γ) t₂ → Form Γ (t₁ > t₂)
^[ tp ] t = lam tp t

_·_ : ∀ {n} → {Γ : Ctx n} → ∀ {t₁ t₂} → Form Γ (t₁ > t₂) → Form Γ t₁ → Form Γ t₂
t₁ · t₂ = app t₁ t₂

$ : ∀ {n Γ} → {t : Type n} (v : Var Γ) → {eq : lookup-Var Γ v ≡ t} → Form Γ t
$ v {p} = var v p

-- occurs in

eq-Var : ∀ {n} {Γ : Ctx n} → Var Γ → Var Γ → Bool
eq-Var this this = true
eq-Var this (next y) = false
eq-Var (next x) this = false
eq-Var (next x) (next y) = eq-Var x y

occurs : ∀ {n Γ} → {t : Type n} → Var Γ → Form Γ t → Bool
occurs x (var x' p) = eq-Var x x'
occurs x N = false
occurs x A = false
occurs x Π = false
occurs x i = false
occurs x (app f₁ f₂) = occurs x f₁ ∨ occurs x f₂
occurs x (lam α f) = occurs (next x) f

-- weakening and substitution

weak-var : ∀ {n} → {β : Type n} (Γ₁ Γ₂ : Ctx n) → (x : Var (Γ₁ ++ Γ₂)) → Var (Γ₁ ++ (β ∷ Γ₂))
weak-var ε Γ₂ x = next x
weak-var (t ∷ Γ₁) Γ₂ this = this
weak-var (t ∷ Γ₁) Γ₂ (next x) = next (weak-var Γ₁ Γ₂ x)

weak-var-p : ∀ {n} → {β : Type n} (Γ₁ Γ₂ : Ctx n) → (x : Var (Γ₁ ++ Γ₂)) →
             lookup-Var (Γ₁ ++ (β ∷ Γ₂)) (weak-var Γ₁ Γ₂ x) ≡ lookup-Var (Γ₁ ++ Γ₂) x
weak-var-p ε Γ₂ x = refl
weak-var-p (t ∷ Γ₁) Γ₂ this = refl
weak-var-p (t ∷ Γ₁) Γ₂ (next x) = weak-var-p Γ₁ Γ₂ x

weak-i : ∀ {n} → {α β : Type n} (Γ₁ Γ₂ : Ctx n) → Form (Γ₁ ++ Γ₂) α → Form (Γ₁ ++ (β ∷ Γ₂)) α
weak-i Γ₁ Γ₂ (var x p) = var (weak-var Γ₁ Γ₂ x) (trans (weak-var-p Γ₁ Γ₂ x) p)
weak-i Γ₁ Γ₂ N = N
weak-i Γ₁ Γ₂ A = A
weak-i Γ₁ Γ₂ Π = Π
weak-i Γ₁ Γ₂ i = i
weak-i Γ₁ Γ₂ (app f₁ f₂) = app (weak-i Γ₁ Γ₂ f₁) (weak-i Γ₁ Γ₂ f₂)
weak-i Γ₁ Γ₂ (lam α f) = lam α (weak-i (α ∷ Γ₁) Γ₂ f)

weak : ∀ {n} → {Γ : Ctx n} {α β : Type n} → Form Γ α → Form (β ∷ Γ) α
weak {_} {Γ} = weak-i ε Γ

sub-var : ∀ {n} → {α β : Type n} (Γ₁ Γ₂ : Ctx n) → Form Γ₂ α → (x : Var (Γ₁ ++ (α ∷ Γ₂))) → lookup-Var (Γ₁ ++ (α ∷ Γ₂)) x ≡ β → Form (Γ₁ ++ Γ₂) β
sub-var ε Γ₂ g this p = subst (Form Γ₂) p g
sub-var ε Γ₂ g (next x) p = var x p
sub-var (t ∷ Γ₁) Γ₂ g this p = var this p
sub-var (t ∷ Γ₁) Γ₂ g (next x) p = weak (sub-var Γ₁ Γ₂ g x p)

sub-i : ∀ {n} → {α β : Type n} (Γ₁ Γ₂ : Ctx n) → Form Γ₂ α → Form (Γ₁ ++ (α ∷ Γ₂)) β → Form (Γ₁ ++ Γ₂) β
sub-i Γ₁ Γ₂ g (var x p) = sub-var Γ₁ Γ₂ g x p
sub-i Γ₁ Γ₂ g N = N
sub-i Γ₁ Γ₂ g A = A
sub-i Γ₁ Γ₂ g Π = Π
sub-i Γ₁ Γ₂ g i = i
sub-i Γ₁ Γ₂ g (app f₁ f₂) = app (sub-i Γ₁ Γ₂ g f₁) (sub-i Γ₁ Γ₂ g f₂)
sub-i Γ₁ Γ₂ g (lam α f) = lam α (sub-i (α ∷ Γ₁) Γ₂ g f)

sub : ∀ {n} → {Γ : Ctx n} {α β : Type n} → Form Γ α → Form (α ∷ Γ) β → Form Γ β
sub {_} {Γ} = sub-i ε Γ

-- properties about weak and sub

sub-weak-var-p-23-this-2 : ∀ {n} → {u v β : Type n} {Γ : Ctx n} (Γ' : Ctx n) (G : Form (v ∷ Γ) u) →
 (Γ'' : Ctx n)
 (h₁ : β ∷ Γ'' ≡ β ∷ (Γ' ++ (u ∷ (v ∷ Γ))))
 (p'' : lookup-Var ((β ∷ Γ') ++ (u ∷ (v ∷ Γ))) (subst Var h₁ this) ≡ lookup-Var (β ∷ (Γ' ++ (v ∷ Γ))) this) →
 var this refl ≡ sub-var (β ∷ Γ') (v ∷ Γ) G (subst Var h₁ this) p''
sub-weak-var-p-23-this-2 {n} {u} {v} {β} {Γ} Γ' G .(Γ' ++ (u ∷ (v ∷ Γ))) refl refl = refl

sub-weak-var-p-23-this-1 : ∀ {n} → {u v β : Type n} {Γ : Ctx n} (Γ' : Ctx n) (G : Form (v ∷ Γ) u) →
 (h₁ : β ∷ ((Γ' ++ (u ∷ ε)) ++ (v ∷ Γ)) ≡ β ∷ (Γ' ++ (u ∷ (v ∷ Γ))))
 (Γ'' : Ctx n)
 (h₂ : β ∷ Γ'' ≡ β ∷ ((Γ' ++ (u ∷ ε)) ++ Γ))
 (p'' : lookup-Var (β ∷ (Γ' ++ (u ∷ (v ∷ Γ)))) (subst Var h₁ (weak-var (β ∷ (Γ' ++ (u ∷ ε))) Γ (subst Var h₂ this))) ≡ β) →
 var this refl ≡
 sub-var (β ∷ Γ') (v ∷ Γ) G (subst Var h₁ (weak-var (β ∷ (Γ' ++ (u ∷ ε))) Γ (subst Var h₂ this))) p''
sub-weak-var-p-23-this-1 {n} {u} {v} {β} {Γ} Γ' G h₁ .((Γ' ++ (u ∷ ε)) ++ Γ) refl p'' = sub-weak-var-p-23-this-2 Γ' G ((Γ' ++ (u ∷ ε)) ++ (v ∷ Γ)) h₁ p''

mutual
 sub-weak-var-p-23-next-2 : ∀ {n} → {u v β t : Type n} {Γ : Ctx n} (Γ' : Ctx n) (x : Var (Γ' ++ Γ)) (G : Form (v ∷ Γ) u) →
  (p : lookup-Var (Γ' ++ (v ∷ Γ)) (weak-var Γ' Γ x) ≡ β)
  (Γ'' : Ctx n)
  (h₁₁ : t ∷ Γ'' ≡ t ∷ (Γ' ++ (u ∷ (v ∷ Γ))))
  (h₁₂ : (Γ' ++ (u ∷ ε)) ++ (v ∷ Γ) ≡ Γ'')
  (h₂ : Γ' ++ (u ∷ Γ) ≡ (Γ' ++ (u ∷ ε)) ++ Γ)
  (p'' : lookup-Var ((t ∷ Γ') ++ (u ∷ (v ∷ Γ))) (subst Var h₁₁ (next (subst Var h₁₂ (weak-var (Γ' ++ (u ∷ ε)) Γ (subst Var h₂ (weak-var Γ' Γ x)))))) ≡ β) →
  var (next (weak-var Γ' Γ x)) p ≡
  sub-var (t ∷ Γ') (v ∷ Γ) G (subst Var h₁₁ (next (subst Var h₁₂ (weak-var (Γ' ++ (u ∷ ε)) Γ (subst Var h₂ (weak-var Γ' Γ x)))))) p''
 sub-weak-var-p-23-next-2 {n} {u} {v} {β} {t} {Γ} Γ' x G p .(Γ' ++ (u ∷ (v ∷ Γ))) refl h₁₂ h₂ p'' = subst (λ z → var (next {_} {t} (weak-var Γ' Γ x)) p ≡ weak-i ε (Γ' ++ (v ∷ Γ)) z) {-{var (weak-var Γ' Γ x) p} {sub-var Γ' (v ∷ Γ) G (subst Var h₁₂ (weak-var (Γ' ++ (u ∷ ε)) Γ (subst Var h₂ (weak-var Γ' Γ x)))) p''}-} (sub-weak-var-p-23 {n} {u} {v} {β} {Γ} Γ' x G p h₁₂ h₂ p'') refl

 sub-weak-var-p-23-next-1 : ∀ {n} → {u v β t : Type n} {Γ : Ctx n} (Γ' : Ctx n) (x : Var (Γ' ++ Γ)) (G : Form (v ∷ Γ) u) →
  (p : lookup-Var (Γ' ++ (v ∷ Γ)) (weak-var Γ' Γ x) ≡ β)
  (h₁ : t ∷ ((Γ' ++ (u ∷ ε)) ++ (v ∷ Γ)) ≡ t ∷ (Γ' ++ (u ∷ (v ∷ Γ))))
  (Γ'' : Ctx n)
  (h₂₁ : t ∷ Γ'' ≡ t ∷ ((Γ' ++ (u ∷ ε)) ++ Γ))
  (h₂₂ : Γ' ++ (u ∷ Γ) ≡ Γ'')
  (p'' : lookup-Var ((t ∷ Γ') ++ (u ∷ (v ∷ Γ))) (subst Var h₁ (weak-var (t ∷ (Γ' ++ (u ∷ ε))) Γ (subst Var h₂₁ (next (subst Var h₂₂ (weak-var Γ' Γ x)))))) ≡ β) →
  var (next (weak-var Γ' Γ x)) p ≡
  sub-var (t ∷ Γ') (v ∷ Γ) G (subst Var h₁ (weak-var (t ∷ (Γ' ++ (u ∷ ε))) Γ (subst Var h₂₁ (next (subst Var h₂₂ (weak-var Γ' Γ x)))))) p''
 sub-weak-var-p-23-next-1 {n} {u} {v} {β} {t} {Γ} Γ' x G p h₁ .((Γ' ++ (u ∷ ε)) ++ Γ) refl h₂₂ p'' = sub-weak-var-p-23-next-2 Γ' x G p ((Γ' ++ (u ∷ ε)) ++ (v ∷ Γ)) h₁ refl h₂₂ p''

 sub-weak-var-p-23 : ∀ {n} → {u v β : Type n} {Γ : Ctx n} (Γ' : Ctx n) (x : Var (Γ' ++ Γ)) (G : Form (v ∷ Γ) u) →
  (p : lookup-Var (Γ' ++ (v ∷ Γ)) (weak-var Γ' Γ x) ≡ β) →
  (h₁ : (Γ' ++ (u ∷ ε)) ++ (v ∷ Γ) ≡ Γ' ++ (u ∷ (v ∷ Γ))) →
  (h₂ : Γ' ++ (u ∷ Γ) ≡ (Γ' ++ (u ∷ ε)) ++ Γ) →
  (p'' : lookup-Var (Γ' ++ (u ∷ (v ∷ Γ))) (subst Var h₁ (weak-var (Γ' ++ (u ∷ ε)) Γ (subst Var h₂ (weak-var Γ' Γ x)))) ≡ β) →
  var (weak-var Γ' Γ x) p ≡
  sub-var Γ' (v ∷ Γ) G (subst Var h₁ (weak-var (Γ' ++ (u ∷ ε)) Γ (subst Var h₂ (weak-var Γ' Γ x)))) p''
 sub-weak-var-p-23 ε x G refl refl refl refl = refl
 sub-weak-var-p-23 {n} {u} {v} {β} {Γ} (.β ∷ Γ') this G refl h₁ h₂ p'' = sub-weak-var-p-23-this-1 Γ' G h₁ (Γ' ++ (u ∷ Γ)) h₂ p''
 sub-weak-var-p-23 {n} {u} {v} {β} {Γ} (t ∷ Γ') (next x) G p h₁ h₂ p'' = sub-weak-var-p-23-next-1 Γ' x G p h₁ (Γ' ++ (u ∷ Γ)) h₂ refl p''

sub-weak-p-23-var-2 : ∀ {n} → {u v β : Type n} {Γ : Ctx n} (Γ' : Ctx n) (x : Var (Γ' ++ Γ)) (G : Form (v ∷ Γ) u) →
 (p : lookup-Var (Γ' ++ Γ) x ≡ β) →
 (Γ'' : Ctx n) →
 (h₁₁ : Γ'' ≡ Γ' ++ (u ∷ (v ∷ Γ))) →
 (h₁₂ : (Γ' ++ (u ∷ ε)) ++ (v ∷ Γ) ≡ Γ'') →
 (h₂ : Γ' ++ (u ∷ Γ) ≡ (Γ' ++ (u ∷ ε)) ++ Γ) →
 (p'' : lookup-Var Γ'' (subst Var h₁₂ (weak-var (Γ' ++ (u ∷ ε)) Γ (subst Var h₂ (weak-var Γ' Γ x)))) ≡ β) →
 var (weak-var Γ' Γ x) (trans (weak-var-p Γ' Γ x) p) ≡
 sub-i Γ' (v ∷ Γ) G (subst (λ z → Form z β) h₁₁ (var (subst Var h₁₂ (weak-var (Γ' ++ (u ∷ ε)) Γ (subst Var h₂ (weak-var Γ' Γ x)))) p''))
sub-weak-p-23-var-2 {n} {u} {v} {β} {Γ} Γ' x G p .(Γ' ++ (u ∷ (v ∷ Γ))) refl h₁₂ h₂ p'' = sub-weak-var-p-23 Γ' x G (trans (weak-var-p Γ' Γ x) p) h₁₂ h₂ p''

sub-weak-p-23-var-1 : ∀ {n} → {u v β : Type n} {Γ : Ctx n} (Γ' : Ctx n) (x : Var (Γ' ++ Γ)) (G : Form (v ∷ Γ) u) →
 (p : lookup-Var (Γ' ++ Γ) x ≡ β) →
 (h₁ : (Γ' ++ (u ∷ ε)) ++ (v ∷ Γ) ≡ Γ' ++ (u ∷ (v ∷ Γ))) →
 (Γ'' : Ctx n) →
 (h₂₁ : Γ'' ≡ (Γ' ++ (u ∷ ε)) ++ Γ) →
 (h₂₂ : Γ' ++ (u ∷ Γ) ≡ Γ'') →
 (p' : lookup-Var Γ'' (subst Var h₂₂ (weak-var Γ' Γ x)) ≡ β) →
 var (weak-var Γ' Γ x) (trans (weak-var-p Γ' Γ x) p) ≡
 sub-i Γ' (v ∷ Γ) G (subst (λ z → Form z β) h₁ (weak-i (Γ' ++ (u ∷ ε)) Γ (subst (λ z → Form z β) h₂₁ (var (subst Var h₂₂ (weak-var Γ' Γ x)) p'))))
sub-weak-p-23-var-1 {n} {u} {v} {β} {Γ} Γ' x G p h₁ .((Γ' ++ (u ∷ ε)) ++ Γ) refl h₂₂ p' = sub-weak-p-23-var-2 Γ' x G p ((Γ' ++ (u ∷ ε)) ++ (v ∷ Γ)) h₁ refl h₂₂ (trans (weak-var-p (Γ' ++ (u ∷ ε)) Γ (subst Var h₂₂ (weak-var Γ' Γ x))) p')

mutual
 sub-weak-p-23-app-2 : ∀ {n} → {t u v w : Type n} {Γ : Ctx n} (Γ' : Ctx n) (f₁ : Form (Γ' ++ Γ) (w > t)) (f₂ : Form (Γ' ++ Γ) w) (G : Form (v ∷ Γ) u) →
  (Γ'' : Ctx n) →
  (h₁₁ : Γ'' ≡ Γ' ++ (u ∷ (v ∷ Γ))) →
  (h₁₂ : (Γ' ++ (u ∷ ε)) ++ (v ∷ Γ) ≡ Γ'') →
  (h₂ : Γ' ++ (u ∷ Γ) ≡ (Γ' ++ (u ∷ ε)) ++ Γ) →
  app (weak-i Γ' Γ f₁) (weak-i Γ' Γ f₂) ≡
  sub-i Γ' (v ∷ Γ) G (subst (λ z → Form z t) h₁₁ (app (subst (λ z → Form z (w > t)) h₁₂ (weak-i (Γ' ++ (u ∷ ε)) Γ (subst (λ z → Form z (w > t)) h₂ (weak-i Γ' Γ f₁)))) (subst (λ z → Form z w) h₁₂ (weak-i (Γ' ++ (u ∷ ε)) Γ (subst (λ z → Form z w) h₂ (weak-i Γ' Γ f₂))))))
 sub-weak-p-23-app-2 {n} {t} {u} {v} {w} {Γ} Γ' f₁ f₂ G .(Γ' ++ (u ∷ (v ∷ Γ))) refl h₁₂ h₂ =
  trans (cong (λ z → app z (weak-i Γ' Γ f₂)) (
    sub-weak-p-23-i Γ' f₁ G h₁₂ h₂
   ))
   (cong (λ z → app (sub-i Γ' (v ∷ Γ) G (subst (λ z → Form z (w > t)) h₁₂ (weak-i (Γ' ++ (u ∷ ε)) Γ (subst (λ z → Form z (w > t)) h₂ (weak-i Γ' Γ f₁))))) z) (
    sub-weak-p-23-i Γ' f₂ G h₁₂ h₂
   ))

 sub-weak-p-23-app-1 : ∀ {n} → {t u v w : Type n} {Γ : Ctx n} (Γ' : Ctx n) (f₁ : Form (Γ' ++ Γ) (w > t)) (f₂ : Form (Γ' ++ Γ) w) (G : Form (v ∷ Γ) u) →
  (h₁ : (Γ' ++ (u ∷ ε)) ++ (v ∷ Γ) ≡ Γ' ++ (u ∷ (v ∷ Γ))) →
  (Γ'' : Ctx n) →
  (h₂₁ : Γ'' ≡ (Γ' ++ (u ∷ ε)) ++ Γ) →
  (h₂₂ : Γ' ++ (u ∷ Γ) ≡ Γ'') →
  app (weak-i Γ' Γ f₁) (weak-i Γ' Γ f₂) ≡
  sub-i Γ' (v ∷ Γ) G (subst (λ z → Form z t) h₁ (weak-i (Γ' ++ (u ∷ ε)) Γ (subst (λ z → Form z t) h₂₁ (app (subst (λ z → Form z (w > t)) h₂₂ (weak-i Γ' Γ f₁)) (subst (λ z → Form z w) h₂₂ (weak-i Γ' Γ f₂))))))
 sub-weak-p-23-app-1 {n} {t} {u} {v} {w} {Γ} Γ' f₁ f₂ G h₁ .((Γ' ++ (u ∷ ε)) ++ Γ) refl h₂₂ = sub-weak-p-23-app-2 Γ' f₁ f₂ G ((Γ' ++ (u ∷ ε)) ++ (v ∷ Γ)) h₁ refl h₂₂

 sub-weak-p-23-lam-2 : ∀ {n} → {u v α β : Type n} {Γ : Ctx n} (Γ' : Ctx n) (f : Form ((α ∷ Γ') ++ Γ) β) (G : Form (v ∷ Γ) u) →
  (Γ'' : Ctx n) →
  (h₁₁ : Γ'' ≡ Γ' ++ (u ∷ (v ∷ Γ))) →
  (h₁₂ : (Γ' ++ (u ∷ ε)) ++ (v ∷ Γ) ≡ Γ'') →
  (h₂ : α ∷ (Γ' ++ (u ∷ Γ)) ≡ α ∷ ((Γ' ++ (u ∷ ε)) ++ Γ)) →
  lam α (weak-i (α ∷ Γ') Γ f) ≡
  sub-i Γ' (v ∷ Γ) G (subst (λ z → Form z (α > β)) h₁₁ (lam α (subst (λ z → Form z β) (cong (_∷_ α) h₁₂) (weak-i (α ∷ (Γ' ++ (u ∷ ε))) Γ (subst (λ z → Form z β) h₂ (weak-i (α ∷ Γ') Γ f))))))
 sub-weak-p-23-lam-2 {n} {u} {v} {α} {β} {Γ} Γ' f G .(Γ' ++ (u ∷ (v ∷ Γ))) refl h₁₂ h₂ = cong (lam α) (
  sub-weak-p-23-i (α ∷ Γ') f G (cong (_∷_ α) h₁₂) h₂)

 sub-weak-p-23-lam-1 : ∀ {n} → {u v α β : Type n} {Γ : Ctx n} (Γ' : Ctx n) (f : Form ((α ∷ Γ') ++ Γ) β) (G : Form (v ∷ Γ) u) →
  (h₁ : (Γ' ++ (u ∷ ε)) ++ (v ∷ Γ) ≡ Γ' ++ (u ∷ (v ∷ Γ))) →
  (Γ'' : Ctx n) →
  (h₂₁ : Γ'' ≡ (Γ' ++ (u ∷ ε)) ++ Γ) →
  (h₂₂ : Γ' ++ (u ∷ Γ) ≡ Γ'') →
  lam α (weak-i (α ∷ Γ') Γ f) ≡
  sub-i Γ' (v ∷ Γ) G (subst (λ z → Form z (α > β)) h₁ (weak-i (Γ' ++ (u ∷ ε)) Γ (subst (λ z → Form z (α > β)) h₂₁ (lam α (subst (λ z → Form z β) (cong (λ z → α ∷ z) h₂₂) (weak-i (α ∷ Γ') Γ f))))))
 sub-weak-p-23-lam-1 {n} {u} {v} {α} {β} {Γ} Γ' f G h₁ .((Γ' ++ (u ∷ ε)) ++ Γ) refl h₂₂ = sub-weak-p-23-lam-2 Γ' f G ((Γ' ++ (u ∷ ε)) ++ (v ∷ Γ)) h₁ refl (cong (_∷_ α) h₂₂)

 sub-weak-p-23-i : ∀ {n} → {t u v : Type n} {Γ : Ctx n} (Γ' : Ctx n) (F : Form (Γ' ++ Γ) t) (G : Form (v ∷ Γ) u) →
  (h₁ : (Γ' ++ (u ∷ ε)) ++ (v ∷ Γ) ≡ Γ' ++ (u ∷ (v ∷ Γ))) →
  (h₂ : Γ' ++ (u ∷ Γ) ≡ (Γ' ++ (u ∷ ε)) ++ Γ) →
  weak-i Γ' Γ F ≡ sub-i Γ' (v ∷ Γ) G (subst (λ z → Form z t) h₁ (weak-i (Γ' ++ (u ∷ ε)) Γ (subst (λ z → Form z t) h₂ (weak-i Γ' Γ F))))
-- sub-weak-p-23-i {_} {.(lookup-Var (Γ' ++ Γ) x)} {u} {v} {Γ} Γ' (var x) G h₁ h₂ = {!!}
 sub-weak-p-23-i {_} {β} {u} {v} {Γ} Γ' (var x p) G h₁ h₂ = sub-weak-p-23-var-1 Γ' x G p h₁ (Γ' ++ (u ∷ Γ)) h₂ refl (trans (weak-var-p Γ' Γ x) p)
 sub-weak-p-23-i {_} {.($o > $o)} {u} {v} {Γ} Γ' N G h₁ h₂ = erase-subst (Ctx _) (λ z → Form z ($o > $o)) N (Γ' ++ (u ∷ Γ)) ((Γ' ++ (u ∷ ε)) ++ Γ) h₂ (λ z → N ≡ sub-i Γ' (v ∷ Γ) G (subst (λ z → Form z ($o > $o)) h₁ (weak-i (Γ' ++ (u ∷ ε)) Γ z))) (erase-subst (Ctx _) (λ z → Form z ($o > $o)) N ((Γ' ++ (u ∷ ε)) ++ (v ∷ Γ)) (Γ' ++ (u ∷ (v ∷ Γ))) h₁ (λ z → N ≡ sub-i Γ' (v ∷ Γ) G z) refl)  -- rewrite h₂ | h₁ = refl
 sub-weak-p-23-i {_} {.($o > ($o > $o))} {u} {v} {Γ} Γ' A G h₁ h₂ = erase-subst (Ctx _) (λ z → Form z ($o > ($o > $o))) A (Γ' ++ (u ∷ Γ)) ((Γ' ++ (u ∷ ε)) ++ Γ) h₂ (λ z → A ≡ sub-i Γ' (v ∷ Γ) G (subst (λ z → Form z ($o > ($o > $o))) h₁ (weak-i (Γ' ++ (u ∷ ε)) Γ z))) (erase-subst (Ctx _) (λ z → Form z ($o > ($o > $o))) A ((Γ' ++ (u ∷ ε)) ++ (v ∷ Γ)) (Γ' ++ (u ∷ (v ∷ Γ))) h₁ (λ z → A ≡ sub-i Γ' (v ∷ Γ) G z) refl)  -- rewrite h₂ | h₁ = refl
 sub-weak-p-23-i {_} {((t > $o) > $o)} {u} {v} {Γ} Γ' Π G h₁ h₂ = erase-subst (Ctx _) (λ z → Form z ((t > $o) > $o)) Π (Γ' ++ (u ∷ Γ)) ((Γ' ++ (u ∷ ε)) ++ Γ) h₂ (λ z → Π ≡ sub-i Γ' (v ∷ Γ) G (subst (λ z → Form z ((t > $o) > $o)) h₁ (weak-i (Γ' ++ (u ∷ ε)) Γ z))) (erase-subst (Ctx _) (λ z → Form z ((t > $o) > $o)) Π ((Γ' ++ (u ∷ ε)) ++ (v ∷ Γ)) (Γ' ++ (u ∷ (v ∷ Γ))) h₁ (λ z → Π ≡ sub-i Γ' (v ∷ Γ) G z) refl)  -- rewrite h₂ | h₁ = refl
 sub-weak-p-23-i {_} {((t > $o) > .t)} {u} {v} {Γ} Γ' i G h₁ h₂ = erase-subst (Ctx _) (λ z → Form z ((t > $o) > t)) i (Γ' ++ (u ∷ Γ)) ((Γ' ++ (u ∷ ε)) ++ Γ) h₂ (λ z → i ≡ sub-i Γ' (v ∷ Γ) G (subst (λ z → Form z ((t > $o) > t)) h₁ (weak-i (Γ' ++ (u ∷ ε)) Γ z))) (erase-subst (Ctx _) (λ z → Form z ((t > $o) > t)) i ((Γ' ++ (u ∷ ε)) ++ (v ∷ Γ)) (Γ' ++ (u ∷ (v ∷ Γ))) h₁ (λ z → i ≡ sub-i Γ' (v ∷ Γ) G z) refl)  -- rewrite h₂ | h₁ = refl
 sub-weak-p-23-i {_} {t} {u} {v} {Γ} Γ' (app f₁ f₂) G h₁ h₂ = sub-weak-p-23-app-1 Γ' f₁ f₂ G h₁ (Γ' ++ (u ∷ Γ)) h₂ refl
 sub-weak-p-23-i {_} {α > β} {u} {v} {Γ} Γ' (lam .α f) G h₁ h₂ = sub-weak-p-23-lam-1 Γ' f G h₁ (Γ' ++ (u ∷ Γ)) h₂ refl

sub-weak-var-p-1-this-2 : ∀ {n} → {u v β : Type n} {Γ : Ctx n} (Γ' : Ctx n) (G : Form Γ u) →
 (Γ'' : Ctx n)
 (h₁ : β ∷ Γ'' ≡ β ∷ (Γ' ++ (v ∷ Γ)))
 (p' : β ≡ β) →
 var this refl ≡
 subst (λ z → Form z β) h₁ (var this p')
sub-weak-var-p-1-this-2 {n} {u} {v} {β} {Γ} Γ' G ._ refl refl = refl

sub-weak-var-p-1-this-1 : ∀ {n} → {u v β : Type n} {Γ : Ctx n} (Γ' : Ctx n) (G : Form Γ u) →
 (h₁ : β ∷ ((Γ' ++ (v ∷ ε)) ++ Γ) ≡ β ∷ (Γ' ++ (v ∷ Γ)))
 (Γ'' : Ctx n)
 (h₂ : β ∷ Γ'' ≡ β ∷ ((Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)))
 (p' : lookup-Var ((β ∷ (Γ' ++ (v ∷ ε))) ++ (u ∷ Γ)) (subst Var h₂ this) ≡ β) →
 var this refl ≡
 subst (λ z → Form z β) h₁ (sub-var (β ∷ (Γ' ++ (v ∷ ε))) Γ G (subst Var h₂ this) p')
sub-weak-var-p-1-this-1 {n} {u} {v} {β} {Γ} Γ' G h₁ ._ refl p' = sub-weak-var-p-1-this-2 Γ' G _ h₁ p'

mutual
 sub-weak-var-p-1-next-2 : ∀ {n} → {u v β t : Type n} {Γ : Ctx n} (Γ' : Ctx n) (x : Var (Γ' ++ Γ)) (G : Form Γ u) →
  (p : lookup-Var (Γ' ++ (v ∷ Γ)) (weak-var Γ' Γ x) ≡ β)
  (Γ'' : Ctx n)
  (h₁₁ : t ∷ Γ'' ≡ t ∷ (Γ' ++ (v ∷ Γ)))
  (h₁₂ : ((Γ' ++ (v ∷ ε)) ++ Γ) ≡ Γ'')
  (h₂ : (Γ' ++ (v ∷ (u ∷ Γ))) ≡ ((Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)))
  (p' : lookup-Var ((Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)) (subst Var h₂ (weak-var Γ' (u ∷ Γ) (weak-var Γ' Γ x))) ≡ β) →
  var (next (weak-var Γ' Γ x)) p ≡
  subst (λ z → Form z β) h₁₁ (weak-i ε Γ'' (subst (λ z → Form z β) h₁₂ (sub-var (Γ' ++ (v ∷ ε)) Γ G (subst Var h₂ (weak-var Γ' (u ∷ Γ) (weak-var Γ' Γ x))) p')))
 sub-weak-var-p-1-next-2 {n} {u} {v} {β} {t} {Γ} Γ' x G p ._ refl h₁₂ h₂ p' =
  subst (λ z → var (next {_} {t} (weak-var Γ' Γ x)) p ≡ weak-i ε (Γ' ++ (v ∷ Γ)) z)
   (sub-weak-var-p-1 Γ' x G p h₁₂ h₂ p')
   refl

 sub-weak-var-p-1-next-1 : ∀ {n} → {u v β t : Type n} {Γ : Ctx n} (Γ' : Ctx n) (x : Var (Γ' ++ Γ)) (G : Form Γ u) →
  (p : lookup-Var (Γ' ++ (v ∷ Γ)) (weak-var Γ' Γ x) ≡ β)
  (h₁ : t ∷ ((Γ' ++ (v ∷ ε)) ++ Γ) ≡ t ∷ (Γ' ++ (v ∷ Γ)))
  (Γ'' : Ctx n)
  (h₂₁ : t ∷ Γ'' ≡ t ∷ ((Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)))
  (h₂₂ : (Γ' ++ (v ∷ (u ∷ Γ))) ≡ Γ'')
  (p' : lookup-Var (t ∷ ((Γ' ++ (v ∷ ε)) ++ (u ∷ Γ))) (subst Var h₂₁ (next (subst Var h₂₂ (weak-var Γ' (u ∷ Γ) (weak-var Γ' Γ x))))) ≡ β) →
  var (next (weak-var Γ' Γ x)) p ≡
  subst (λ z → Form z β) h₁ (sub-var (t ∷ (Γ' ++ (v ∷ ε))) Γ G (subst Var h₂₁ (next (subst Var h₂₂ (weak-var Γ' (u ∷ Γ) (weak-var Γ' Γ x))))) p')
 sub-weak-var-p-1-next-1 {n} {u} {v} {β} {t} {Γ} Γ' x G p h₁ ._ refl h₂₂ p' = sub-weak-var-p-1-next-2 Γ' x G p _ h₁ refl h₂₂ p'

 sub-weak-var-p-1 : ∀ {n} → {u v β : Type n} {Γ : Ctx n} (Γ' : Ctx n) (x : Var (Γ' ++ Γ)) (G : Form Γ u) →
  (p : lookup-Var (Γ' ++ (v ∷ Γ)) (weak-var Γ' Γ x) ≡ β) →
  (h₁ : (Γ' ++ (v ∷ ε)) ++ Γ ≡ Γ' ++ (v ∷ Γ)) →
  (h₂ : Γ' ++ (v ∷ (u ∷ Γ)) ≡ (Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)) →
  (p' : lookup-Var ((Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)) (subst Var h₂ (weak-var Γ' (u ∷ Γ) (weak-var Γ' Γ x))) ≡ β) →
  var (weak-var Γ' Γ x) p ≡
  subst (λ z → Form z β) h₁ (sub-var (Γ' ++ (v ∷ ε)) Γ G (subst Var h₂ (weak-var Γ' (u ∷ Γ) (weak-var Γ' Γ x))) p')
 sub-weak-var-p-1 ε x G refl refl refl refl = refl
 sub-weak-var-p-1 {n} {u} {v} {β} {Γ} (.β ∷ Γ') this G refl h₁ h₂ p' = sub-weak-var-p-1-this-1 Γ' G h₁ _ h₂ p'
 sub-weak-var-p-1 {n} {u} {v} {β} {Γ} (t ∷ Γ') (next x) G p h₁ h₂ p' = sub-weak-var-p-1-next-1 Γ' x G p h₁ _ h₂ refl p'

sub-weak-p-1-var : ∀ {n} → {u v β : Type n} {Γ : Ctx n} (Γ' : Ctx n) (x : Var (Γ' ++ Γ)) (G : Form Γ u) →
 (p : lookup-Var (Γ' ++ Γ) x ≡ β)
 (h₁ : (Γ' ++ (v ∷ ε)) ++ Γ ≡ Γ' ++ (v ∷ Γ))
 (Γ'' : Ctx n)
 (h₂₁ : Γ'' ≡ (Γ' ++ (v ∷ ε)) ++ (u ∷ Γ))
 (h₂₂ : Γ' ++ (v ∷ (u ∷ Γ)) ≡ Γ'')
 (p' : lookup-Var Γ'' (subst Var h₂₂ (weak-var Γ' (u ∷ Γ) (weak-var Γ' Γ x))) ≡ β) →
 var (weak-var Γ' Γ x) (trans (weak-var-p Γ' Γ x) p) ≡
 subst (λ z → Form z β) h₁ (sub-i (Γ' ++ (v ∷ ε)) Γ G (subst (λ z → Form z β) h₂₁ (var (subst Var h₂₂ (weak-var Γ' (u ∷ Γ) (weak-var Γ' Γ x))) p')))
sub-weak-p-1-var {n} {u} {v} {β} {Γ} Γ' x G p h₁ ._ refl h₂₂ p' = sub-weak-var-p-1 Γ' x G (trans (weak-var-p Γ' Γ x) p) h₁ h₂₂ p'

mutual
 sub-weak-p-1-app-2 : ∀ {n} → {t u v w : Type n} {Γ : Ctx n} (Γ' : Ctx n) (f₁ : Form (Γ' ++ Γ) (w > t)) (f₂ : Form (Γ' ++ Γ) w) (G : Form Γ u) →
  (Γ'' : Ctx n) →
  (h₁₁ : Γ'' ≡ Γ' ++ (v ∷ Γ)) →
  (h₁₂ : (Γ' ++ (v ∷ ε)) ++ Γ ≡ Γ'') →
  (h₂ : Γ' ++ (v ∷ (u ∷ Γ)) ≡ (Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)) →
  app (weak-i Γ' Γ f₁) (weak-i Γ' Γ f₂) ≡
  subst (λ z → Form z t) h₁₁ (app (subst (λ z → Form z (w > t)) h₁₂ (sub-i (Γ' ++ (v ∷ ε)) Γ G (subst (λ z → Form z (w > t)) h₂ (weak-i Γ' (u ∷ Γ) (weak-i Γ' Γ f₁))))) (subst (λ z → Form z w) h₁₂ (sub-i (Γ' ++ (v ∷ ε)) Γ G (subst (λ z → Form z w) h₂ (weak-i Γ' (u ∷ Γ) (weak-i Γ' Γ f₂))))))
 sub-weak-p-1-app-2 {n} {t} {u} {v} {w} {Γ} Γ' f₁ f₂ G .(Γ' ++ (v ∷ Γ)) refl h₁₂ h₂ =
  trans (cong (λ z → app z (weak-i Γ' Γ f₂)) (
    sub-weak-p-1-i Γ' f₁ G h₁₂ h₂
   ))
   (cong (λ z → app (subst (λ z → Form z (w > t)) h₁₂ (sub-i (Γ' ++ (v ∷ ε)) Γ G (subst (λ z → Form z (w > t)) h₂ (weak-i Γ' (u ∷ Γ) (weak-i Γ' Γ f₁))))) z) (
    sub-weak-p-1-i Γ' f₂ G h₁₂ h₂
   ))

 sub-weak-p-1-app-1 : ∀ {n} → {t u v w : Type n} {Γ : Ctx n} (Γ' : Ctx n) (f₁ : Form (Γ' ++ Γ) (w > t)) (f₂ : Form (Γ' ++ Γ) w) (G : Form Γ u) →
  (h₁ : (Γ' ++ (v ∷ ε)) ++ Γ ≡ Γ' ++ (v ∷ Γ)) →
  (Γ'' : Ctx n) →
  (h₂₁ : Γ'' ≡ (Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)) →
  (h₂₂ : Γ' ++ (v ∷ (u ∷ Γ)) ≡ Γ'') →
  app (weak-i Γ' Γ f₁) (weak-i Γ' Γ f₂) ≡
  subst (λ z → Form z t) h₁ (sub-i (Γ' ++ (v ∷ ε)) Γ G (subst (λ z → Form z t) h₂₁ (app (subst (λ z → Form z (w > t)) h₂₂ (weak-i Γ' (u ∷ Γ) (weak-i Γ' Γ f₁))) (subst (λ z → Form z w) h₂₂ (weak-i Γ' (u ∷ Γ) (weak-i Γ' Γ f₂))))))
 sub-weak-p-1-app-1 {n} {t} {u} {v} {w} {Γ} Γ' f₁ f₂ G h₁ .((Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)) refl h₂₂ = sub-weak-p-1-app-2 Γ' f₁ f₂ G ((Γ' ++ (v ∷ ε)) ++ Γ) h₁ refl h₂₂

 sub-weak-p-1-lam-2 : ∀ {n} → {u v α β : Type n} {Γ : Ctx n} (Γ' : Ctx n) (f : Form ((α ∷ Γ') ++ Γ) β) (G : Form Γ u) →
  (Γ'' : Ctx n) →
  (h₁₁ : Γ'' ≡ Γ' ++ (v ∷ Γ)) →
  (h₁₂ : (Γ' ++ (v ∷ ε)) ++ Γ ≡ Γ'') →
  (h₂ : Γ' ++ (v ∷ (u ∷ Γ)) ≡ (Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)) →
  lam α (weak-i (α ∷ Γ') Γ f) ≡
  subst (λ z → Form z (α > β)) h₁₁ (lam α (subst (λ z → Form z β) (cong (_∷_ α) h₁₂) (sub-i (α ∷ (Γ' ++ (v ∷ ε))) Γ G (subst (λ z → Form z β) (cong (_∷_ α) h₂) (weak-i (α ∷ Γ') (u ∷ Γ) (weak-i (α ∷ Γ') Γ f))))))
 sub-weak-p-1-lam-2 {n} {u} {v} {α} {β} {Γ} Γ' f G .(Γ' ++ (v ∷ Γ)) refl h₁₂ h₂ = cong (lam α) (
  sub-weak-p-1-i (α ∷ Γ') f G (cong (_∷_ α) h₁₂) (cong (_∷_ α) h₂))

 sub-weak-p-1-lam-1 : ∀ {n} → {u v α β : Type n} {Γ : Ctx n} (Γ' : Ctx n) (f : Form ((α ∷ Γ') ++ Γ) β) (G : Form Γ u) →
  (h₁ : (Γ' ++ (v ∷ ε)) ++ Γ ≡ Γ' ++ (v ∷ Γ)) →
  (Γ'' : Ctx n) →
  (h₂₁ : Γ'' ≡ (Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)) →
  (h₂₂ : Γ' ++ (v ∷ (u ∷ Γ)) ≡ Γ'') →
  lam α (weak-i (α ∷ Γ') Γ f) ≡
  subst (λ z → Form z (α > β)) h₁ (sub-i (Γ' ++ (v ∷ ε)) Γ G (subst (λ z → Form z (α > β)) h₂₁ (lam α (subst (λ z → Form z β) (cong (λ z → α ∷ z) h₂₂) (weak-i (α ∷ Γ') (u ∷ Γ) (weak-i (α ∷ Γ') Γ f))))))
 sub-weak-p-1-lam-1 {n} {u} {v} {α} {β} {Γ} Γ' f G h₁ .((Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)) refl h₂₂ = sub-weak-p-1-lam-2 Γ' f G ((Γ' ++ (v ∷ ε)) ++ Γ) h₁ refl h₂₂

 sub-weak-p-1-i : ∀ {n} → {t u v : Type n} {Γ : Ctx n} (Γ' : Ctx n) (F : Form (Γ' ++ Γ) t) (G : Form Γ u) →
   (h₁ : (Γ' ++ (v ∷ ε)) ++ Γ ≡ Γ' ++ (v ∷ Γ)) →
   (h₂ : Γ' ++ (v ∷ (u ∷ Γ)) ≡ (Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)) →
   weak-i Γ' Γ F ≡ subst (λ z → Form z t) h₁ (sub-i (Γ' ++ (v ∷ ε)) Γ G (subst (λ z → Form z t) h₂ (weak-i Γ' (u ∷ Γ) (weak-i Γ' Γ F))))
 sub-weak-p-1-i {_} {β} {u} {v} {Γ} Γ' (var x p) G h₁ h₂ = sub-weak-p-1-var Γ' x G p h₁ _ h₂ refl (trans (weak-var-p Γ' (u ∷ Γ) (weak-var Γ' Γ x)) (trans (weak-var-p Γ' Γ x) p))
 sub-weak-p-1-i {_} {$o > $o} {u} {v} {Γ} Γ' N G h₁ h₂ = erase-subst (Ctx _) (λ z → Form z ($o > $o)) N (Γ' ++ (v ∷ (u ∷ Γ))) ((Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)) h₂ (λ z → N ≡ subst (λ z → Form z ($o > $o)) h₁ (sub-i (Γ' ++ (v ∷ ε)) Γ G z)) (erase-subst (Ctx _) (λ z → Form z ($o > $o)) N ((Γ' ++ (v ∷ ε)) ++ Γ) (Γ' ++ (v ∷ Γ)) h₁ (λ z → N ≡ z) refl)  -- rewrite h₂ | h₁ = refl
 sub-weak-p-1-i {_} {$o > ($o > $o)} {u} {v} {Γ} Γ' A G h₁ h₂ = erase-subst (Ctx _) (λ z → Form z ($o > ($o > $o))) A (Γ' ++ (v ∷ (u ∷ Γ))) ((Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)) h₂ (λ z → A ≡ subst (λ z → Form z ($o > ($o > $o))) h₁ (sub-i (Γ' ++ (v ∷ ε)) Γ G z)) (erase-subst (Ctx _) (λ z → Form z ($o > ($o > $o))) A ((Γ' ++ (v ∷ ε)) ++ Γ) (Γ' ++ (v ∷ Γ)) h₁ (λ z → A ≡ z) refl)  -- rewrite h₂ | h₁ = refl
 sub-weak-p-1-i {_} {(t > $o) > $o} {u} {v} {Γ} Γ' Π G h₁ h₂ = erase-subst (Ctx _) (λ z → Form z ((t > $o) > $o)) Π (Γ' ++ (v ∷ (u ∷ Γ))) ((Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)) h₂ (λ z → Π ≡ subst (λ z → Form z ((t > $o) > $o)) h₁ (sub-i (Γ' ++ (v ∷ ε)) Γ G z)) (erase-subst (Ctx _) (λ z → Form z ((t > $o) > $o)) Π ((Γ' ++ (v ∷ ε)) ++ Γ) (Γ' ++ (v ∷ Γ)) h₁ (λ z → Π ≡ z) refl)  -- rewrite h₂ | h₁ = refl
 sub-weak-p-1-i {_} {(t > $o) > .t} {u} {v} {Γ} Γ' i G h₁ h₂ = erase-subst (Ctx _) (λ z → Form z ((t > $o) > t)) i (Γ' ++ (v ∷ (u ∷ Γ))) ((Γ' ++ (v ∷ ε)) ++ (u ∷ Γ)) h₂ (λ z → i ≡ subst (λ z → Form z ((t > $o) > t)) h₁ (sub-i (Γ' ++ (v ∷ ε)) Γ G z)) (erase-subst (Ctx _) (λ z → Form z ((t > $o) > t)) i ((Γ' ++ (v ∷ ε)) ++ Γ) (Γ' ++ (v ∷ Γ)) h₁ (λ z → i ≡ z) refl)  -- rewrite h₂ | h₁ = refl
 sub-weak-p-1-i {_} {t} {u} {v} {Γ} Γ' (app f₁ f₂) G h₁ h₂ = sub-weak-p-1-app-1 Γ' f₁ f₂ G h₁ (Γ' ++ (v ∷ (u ∷ Γ))) h₂ refl
 sub-weak-p-1-i {_} {α > β} {u} {v} {Γ} Γ' (lam .α f) G h₁ h₂ = sub-weak-p-1-lam-1 Γ' f G h₁ (Γ' ++ (v ∷ (u ∷ Γ))) h₂ refl

sub-weak-p-1'-var : ∀ {n} → {t u : Type n} {Γ : Ctx n} (Γ' : Ctx n) (x : Var (Γ' ++ Γ)) (G : Form Γ u)
 (p : lookup-Var (Γ' ++ Γ) x ≡ t) →
 var x p ≡ sub-var Γ' Γ G (weak-var Γ' Γ x) (trans (weak-var-p Γ' Γ x) p)
sub-weak-p-1'-var ε x G p = refl
sub-weak-p-1'-var (v ∷ Γ') this G p = refl
sub-weak-p-1'-var {_} {_} {_} {Γ} (v ∷ Γ') (next x) G p =
 subst (λ z → var (next {_} {v} x) p ≡ weak-i ε (Γ' ++ Γ) z)
  (sub-weak-p-1'-var Γ' x G p)
  refl

sub-weak-p-1'-i : ∀ {n} → {t u : Type n} {Γ : Ctx n} (Γ' : Ctx n) (F : Form (Γ' ++ Γ) t) (G : Form Γ u) →
  F ≡ sub-i Γ' Γ G (weak-i Γ' Γ F)
sub-weak-p-1'-i Γ' (var x p) G = sub-weak-p-1'-var Γ' x G p
sub-weak-p-1'-i Γ' N G = refl
sub-weak-p-1'-i Γ' A G = refl
sub-weak-p-1'-i Γ' Π G = refl
sub-weak-p-1'-i Γ' i G = refl
sub-weak-p-1'-i {_} {_} {_} {Γ} Γ' (app f₁ f₂) G = trans (cong (λ z → app z f₂) (sub-weak-p-1'-i Γ' f₁ G)) ((cong (λ z → app (sub-i Γ' Γ G (weak-i Γ' Γ f₁)) z) (sub-weak-p-1'-i Γ' f₂ G)))
sub-weak-p-1'-i Γ' (lam α f) G = cong (lam α) (sub-weak-p-1'-i (α ∷ Γ') f G)

sub-weak-p-1 : ∀ {n} → {t u v : Type n} {Γ : Ctx n} (F : Form Γ t) (G : Form Γ u) →
  weak-i ε Γ F ≡ sub-i (v ∷ ε) Γ G (weak-i ε (u ∷ Γ) (weak-i ε Γ F))
sub-weak-p-1 F G = sub-weak-p-1-i ε F G refl refl

sub-weak-p-23 : ∀ {n} → {t u v : Type n} {Γ : Ctx n} (F : Form Γ t) (G : Form (v ∷ Γ) u) →
 weak-i ε Γ F ≡ sub-i ε (v ∷ Γ) G (weak-i (u ∷ ε) Γ (weak-i ε Γ F))
sub-weak-p-23 F G = sub-weak-p-23-i ε F G refl refl

sub-weak-p-1' : ∀ {n} → {t u : Type n} {Γ : Ctx n} (F : Form Γ t) (G : Form Γ u) →
  F ≡ sub G (weak F)
sub-weak-p-1' F G = sub-weak-p-1'-i ε F G

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

weak-var-irr-proof-2 : ∀ {n} {Γ : Ctx n} (t : Type n) (x : Var Γ)
 (p₁ : lookup-Var Γ x ≡ t)
 (p₂ : lookup-Var Γ x ≡ t) →
 var x p₁ ≡ var x p₂
weak-var-irr-proof-2 {n} {Γ} .(lookup-Var Γ x) x refl refl = refl

weak-var-irr-proof : ∀ {n} {Γ : Ctx n} (t : Type n) (x₁ x₂ : Var Γ)
 (p₁ : lookup-Var Γ x₁ ≡ t)
 (p₂ : lookup-Var Γ x₂ ≡ t) →
 x₁ ≡ x₂ →
 var x₁ p₁ ≡ var x₂ p₂
weak-var-irr-proof {n} {Γ} t .x₂ x₂ p₁ p₂ refl = weak-var-irr-proof-2 t x₂ p₁ p₂  -- rewrite h = weak-var-irr-proof-2 t x₂ p₁ p₂

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

weak-weak-var-p-1-this : ∀ {n} Γ₁ Γ₂ → (t u v w : Type n)
 (Γ'₁ Γ'₂ : Ctx n) →
 (h₁ : w ∷ Γ'₁ ≡ w ∷ ((Γ₂ ++ (t ∷ ε)) ++ Γ₁))
 (h₂ : w ∷ Γ'₂ ≡ w ∷ ((Γ₂ ++ (t ∷ ε)) ++ (u ∷ Γ₁))) →
 weak-var (w ∷ (Γ₂ ++ (t ∷ ε))) Γ₁ (subst Var h₁ this) ≡
 subst Var h₂ this
weak-weak-var-p-1-this Γ₁ Γ₂ t u v w ._ ._ refl refl = refl

mutual
 weak-weak-var-p-1-next : ∀ {n} Γ₁ Γ₂ → (t u v w : Type n) (x : Var (Γ₂ ++ Γ₁))
  (Γ'₁ Γ'₂ : Ctx n) →
  (h₁₁ : w ∷ Γ'₁ ≡ w ∷ ((Γ₂ ++ (t ∷ ε)) ++ Γ₁))
  (h₁₂ : Γ₂ ++ (t ∷ Γ₁) ≡ Γ'₁)
  (h₂₁ : w ∷ Γ'₂ ≡ w ∷ ((Γ₂ ++ (t ∷ ε)) ++ (u ∷ Γ₁)))
  (h₂₂ : Γ₂ ++ (t ∷ (u ∷ Γ₁)) ≡ Γ'₂) →
  weak-var (w ∷ (Γ₂ ++ (t ∷ ε))) Γ₁ (subst Var h₁₁ (next (subst Var h₁₂ (weak-var Γ₂ Γ₁ x)))) ≡
  subst Var h₂₁ (next (subst Var h₂₂ (weak-var Γ₂ (u ∷ Γ₁) (weak-var Γ₂ Γ₁ x))))
 weak-weak-var-p-1-next Γ₁ Γ₂ t u v w x ._ ._ refl h₁₂ refl h₂₂ = cong next (weak-weak-var-p-1 Γ₁ Γ₂ t u v x h₁₂ h₂₂)

 weak-weak-var-p-1 : ∀ {n} Γ₁ Γ₂ → (t u v : Type n) (x : Var (Γ₂ ++ Γ₁))
  (h₁ : Γ₂ ++ (t ∷ Γ₁) ≡ (Γ₂ ++ (t ∷ ε)) ++ Γ₁)
  (h₂ : Γ₂ ++ (t ∷ (u ∷ Γ₁)) ≡ (Γ₂ ++ (t ∷ ε)) ++ (u ∷ Γ₁)) →
  weak-var (Γ₂ ++ (t ∷ ε)) Γ₁ (subst Var h₁ (weak-var Γ₂ Γ₁ x)) ≡
  subst Var h₂ (weak-var Γ₂ (u ∷ Γ₁) (weak-var Γ₂ Γ₁ x))
 weak-weak-var-p-1 Γ₂ ε t u v x refl refl = refl
 weak-weak-var-p-1 Γ₁ (w ∷ Γ₂) t u v this h₁ h₂ = weak-weak-var-p-1-this Γ₁ Γ₂ t u v w _ _ h₁ h₂
 weak-weak-var-p-1 Γ₁ (w ∷ Γ₂) t u v (next x) h₁ h₂ = weak-weak-var-p-1-next Γ₁ Γ₂ t u v w x _ _ h₁ refl h₂ refl

weak-weak-p-1-var : ∀ {n} Γ₁ Γ₂ → (t u v : Type n) (x : Var (Γ₂ ++ Γ₁))
 (Γ'₁ Γ'₂ : Ctx n) →
 (h₁₁ : Γ'₁ ≡ (Γ₂ ++ (t ∷ ε)) ++ Γ₁) →
 (h₁₂ : Γ₂ ++ (t ∷ Γ₁) ≡ Γ'₁) →
 (h₂₁ : Γ'₂ ≡ (Γ₂ ++ (t ∷ ε)) ++ (u ∷ Γ₁)) →
 (h₂₂ : Γ₂ ++ (t ∷ (u ∷ Γ₁)) ≡ Γ'₂) →
 (p₁ : lookup-Var Γ'₁ (subst Var h₁₂ (weak-var Γ₂ Γ₁ x)) ≡ v)
 (p₂ : lookup-Var Γ'₂ (subst Var h₂₂ (weak-var Γ₂ (u ∷ Γ₁) (weak-var Γ₂ Γ₁ x))) ≡ v) →
 weak-i (Γ₂ ++ (t ∷ ε)) Γ₁ (subst (λ z → Form z v) h₁₁ (var (subst Var h₁₂ (weak-var Γ₂ Γ₁ x)) p₁)) ≡
 subst (λ z → Form z v) h₂₁ (var (subst Var h₂₂ (weak-var Γ₂ (u ∷ Γ₁) (weak-var Γ₂ Γ₁ x))) p₂)
weak-weak-p-1-var Γ₁ Γ₂ t u v x .((Γ₂ ++ (t ∷ ε)) ++ Γ₁) .((Γ₂ ++ (t ∷ ε)) ++ (u ∷ Γ₁)) refl h₁₂ refl h₂₂ p₁ p₂ = weak-var-irr-proof _ (weak-var (Γ₂ ++ (t ∷ ε)) Γ₁ (subst Var h₁₂ (weak-var Γ₂ Γ₁ x))) (subst Var h₂₂ (weak-var Γ₂ (u ∷ Γ₁) (weak-var Γ₂ Γ₁ x))) (trans (weak-var-p (Γ₂ ++ (t ∷ ε)) Γ₁ (subst Var h₁₂ (weak-var Γ₂ Γ₁ x))) p₁) p₂ (weak-weak-var-p-1 Γ₁ Γ₂ t u v x h₁₂ h₂₂)

mutual
 weak-weak-p-1-app : ∀ {n} Γ₁ Γ₂ → (t u v α : Type n) (f₁ : Form (Γ₂ ++ Γ₁) (α > v)) (f₂ : Form (Γ₂ ++ Γ₁) α)
  (Γ'₁ Γ'₂ : Ctx n) →
  (h₁₁ : Γ'₁ ≡ (Γ₂ ++ (t ∷ ε)) ++ Γ₁) →
  (h₁₂ : Γ₂ ++ (t ∷ Γ₁) ≡ Γ'₁) →
  (h₂₁ : Γ'₂ ≡ (Γ₂ ++ (t ∷ ε)) ++ (u ∷ Γ₁)) →
  (h₂₂ : Γ₂ ++ (t ∷ (u ∷ Γ₁)) ≡ Γ'₂) →
  weak-i (Γ₂ ++ (t ∷ ε)) Γ₁ (subst (λ z → Form z v) h₁₁ (app (subst (λ z → Form z (α > v)) h₁₂ (weak-i Γ₂ Γ₁ f₁)) (subst (λ z → Form z α) h₁₂ (weak-i Γ₂ Γ₁ f₂)))) ≡
  subst (λ z → Form z v) h₂₁ (app (subst (λ z → Form z (α > v)) h₂₂ (weak-i Γ₂ (u ∷ Γ₁) (weak-i Γ₂ Γ₁ f₁))) (subst (λ z → Form z α) h₂₂ (weak-i Γ₂ (u ∷ Γ₁) (weak-i Γ₂ Γ₁ f₂))))
 weak-weak-p-1-app Γ₁ Γ₂ t u v α f₁ f₂ ._ ._ refl h₁₂ refl h₂₂ =
  trans (cong (λ z → app z (weak-i (Γ₂ ++ (t ∷ ε)) Γ₁ (subst (λ z → Form z α) h₁₂ (weak-i Γ₂ Γ₁ f₂)))) (weak-weak-p-1-i Γ₁ Γ₂ t u (α > v) f₁ h₁₂ h₂₂)) (cong (app (subst (λ z → Form z (α > v)) h₂₂ (weak-i Γ₂ (u ∷ Γ₁) (weak-i Γ₂ Γ₁ f₁)))) (weak-weak-p-1-i Γ₁ Γ₂ t u α f₂ h₁₂ h₂₂))

 weak-weak-p-1-lam : ∀ {n} Γ₁ Γ₂ → (t u α β : Type n) (X : Form (α ∷ (Γ₂ ++ Γ₁)) β)
  (Γ'₁ Γ'₂ : Ctx n) →
  (h₁₁ : Γ'₁ ≡ (Γ₂ ++ (t ∷ ε)) ++ Γ₁) →
  (h₁₂ : Γ₂ ++ (t ∷ Γ₁) ≡ Γ'₁) →
  (h₂₁ : Γ'₂ ≡ (Γ₂ ++ (t ∷ ε)) ++ (u ∷ Γ₁)) →
  (h₂₂ : Γ₂ ++ (t ∷ (u ∷ Γ₁)) ≡ Γ'₂) →
  weak-i (Γ₂ ++ (t ∷ ε)) Γ₁ (subst (λ z → Form z (α > β)) h₁₁ (lam α (subst (λ z → Form z β) (cong (_∷_ α) h₁₂) (weak-i (α ∷ Γ₂) Γ₁ X)))) ≡
  subst (λ z → Form z (α > β)) h₂₁ (lam α (subst (λ z → Form z β) (cong (_∷_ α) h₂₂) (weak-i (α ∷ Γ₂) (u ∷ Γ₁) (weak-i (α ∷ Γ₂) Γ₁ X))))
 weak-weak-p-1-lam Γ₁ Γ₂ t u α β X .((Γ₂ ++ (t ∷ ε)) ++ Γ₁) .((Γ₂ ++ (t ∷ ε)) ++ (u ∷ Γ₁)) refl h₁₂ refl h₂₂ = cong (lam α) (weak-weak-p-1-i Γ₁ (α ∷ Γ₂) t u β X (cong (_∷_ α) h₁₂) (cong (_∷_ α) h₂₂))

 weak-weak-p-1-i : ∀ {n} Γ₁ Γ₂ → (t u v : Type n) (X : Form (Γ₂ ++ Γ₁) v) →
  (h₁ : Γ₂ ++ (t ∷ Γ₁) ≡ (Γ₂ ++ (t ∷ ε)) ++ Γ₁) →
  (h₂ : Γ₂ ++ (t ∷ (u ∷ Γ₁)) ≡ (Γ₂ ++ (t ∷ ε)) ++ (u ∷ Γ₁)) →
  weak-i {n} {v} {u} (Γ₂ ++ (t ∷ ε)) Γ₁ (subst (λ z → Form z v) h₁ (weak-i {n} {v} {t} Γ₂ Γ₁ X)) ≡ subst (λ z → Form z v) h₂ (weak-i {n} {v} {t} Γ₂ (u ∷ Γ₁) (weak-i {n} {v} {u} Γ₂ Γ₁ X))
 weak-weak-p-1-i Γ₁ Γ₂ t u v (var x p) h₁ h₂ = weak-weak-p-1-var Γ₁ Γ₂ t u v x _ _ h₁ refl h₂ refl (trans (weak-var-p Γ₂ Γ₁ x) p) (trans (weak-var-p Γ₂ (u ∷ Γ₁) (weak-var Γ₂ Γ₁ x)) (trans (weak-var-p Γ₂ Γ₁ x) p))
 weak-weak-p-1-i Γ₁ Γ₂ t u .($o > $o) N h₁ h₂ = erase-subst (Ctx _) (λ z → Form z ($o > $o)) N (Γ₂ ++ (t ∷ (u ∷ Γ₁))) ((Γ₂ ++ (t ∷ ε)) ++ (u ∷ Γ₁)) h₂ (λ z → weak-i (Γ₂ ++ (t ∷ ε)) Γ₁ (subst (λ z → Form z ($o > $o)) h₁ N) ≡ z) (erase-subst (Ctx _) (λ z → Form z ($o > $o)) N (Γ₂ ++ (t ∷ Γ₁)) ((Γ₂ ++ (t ∷ ε)) ++ Γ₁) h₁ (λ z → weak-i {_} {_} {u} (Γ₂ ++ (t ∷ ε)) Γ₁ z ≡ N) refl)  -- rewrite h₂ | h₁ = refl
 weak-weak-p-1-i Γ₁ Γ₂ t u .($o > ($o > $o)) A h₁ h₂ = erase-subst (Ctx _) (λ z → Form z ($o > ($o > $o))) A (Γ₂ ++ (t ∷ (u ∷ Γ₁))) ((Γ₂ ++ (t ∷ ε)) ++ (u ∷ Γ₁)) h₂ (λ z → weak-i (Γ₂ ++ (t ∷ ε)) Γ₁ (subst (λ z → Form z ($o > ($o > $o))) h₁ A) ≡ z) (erase-subst (Ctx _) (λ z → Form z ($o > ($o > $o))) A (Γ₂ ++ (t ∷ Γ₁)) ((Γ₂ ++ (t ∷ ε)) ++ Γ₁) h₁ (λ z → weak-i {_} {_} {u} (Γ₂ ++ (t ∷ ε)) Γ₁ z ≡ A) refl)  -- rewrite h₂ | h₁ = refl
 weak-weak-p-1-i Γ₁ Γ₂ t u .((α > $o) > $o) (Π {._} {α}) h₁ h₂ = erase-subst (Ctx _) (λ z → Form z ((α > $o) > $o)) Π (Γ₂ ++ (t ∷ (u ∷ Γ₁))) ((Γ₂ ++ (t ∷ ε)) ++ (u ∷ Γ₁)) h₂ (λ z → weak-i (Γ₂ ++ (t ∷ ε)) Γ₁ (subst (λ z → Form z ((α > $o) > $o)) h₁ Π) ≡ z) (erase-subst (Ctx _) (λ z → Form z ((α > $o) > $o)) Π (Γ₂ ++ (t ∷ Γ₁)) ((Γ₂ ++ (t ∷ ε)) ++ Γ₁) h₁ (λ z → weak-i {_} {_} {u} (Γ₂ ++ (t ∷ ε)) Γ₁ z ≡ Π) refl)  -- rewrite h₂ | h₁ = refl
 weak-weak-p-1-i Γ₁ Γ₂ t u .((α > $o) > α) (i {._} {α}) h₁ h₂ = erase-subst (Ctx _) (λ z → Form z ((α > $o) > α)) i (Γ₂ ++ (t ∷ (u ∷ Γ₁))) ((Γ₂ ++ (t ∷ ε)) ++ (u ∷ Γ₁)) h₂ (λ z → weak-i (Γ₂ ++ (t ∷ ε)) Γ₁ (subst (λ z → Form z ((α > $o) > α)) h₁ i) ≡ z) (erase-subst (Ctx _) (λ z → Form z ((α > $o) > α)) i (Γ₂ ++ (t ∷ Γ₁)) ((Γ₂ ++ (t ∷ ε)) ++ Γ₁) h₁ (λ z → weak-i {_} {_} {u} (Γ₂ ++ (t ∷ ε)) Γ₁ z ≡ i) refl)  -- rewrite h₂ | h₁ = refl
 weak-weak-p-1-i Γ₁ Γ₂ t u v (app f₁ f₂) h₁ h₂ = weak-weak-p-1-app Γ₁ Γ₂ t u v _ f₁ f₂ _ _ h₁ refl h₂ refl
 weak-weak-p-1-i Γ₁ Γ₂ t u .(α > β) (lam {._} {β} α f) h₁ h₂ = weak-weak-p-1-lam Γ₁ Γ₂ t u α β f _ _ h₁ refl h₂ refl

weak-weak-p-1 : ∀ {n} Γ → (t u v : Type n) (X : Form Γ v) →
  weak-i {n} {v} {u} (t ∷ ε) Γ (weak-i {n} {v} {t} ε Γ X) ≡ weak-i {n} {v} {t} ε (u ∷ Γ) (weak-i {n} {v} {u} ε Γ X)
weak-weak-p-1 Γ t u v X = weak-weak-p-1-i Γ ε t u v X refl refl

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

thevar : ∀ {n Γ} → (Γ' : Ctx n) (α : Type n) → Var (Γ' ++ (α ∷ Γ))
thevar ε α = this
thevar (β ∷ Γ') α = next (thevar Γ' α)

occurs-p-2-i-var : ∀ {n} {Γ : Ctx n} {α β : Type n} (Γ' : Ctx n)
 (v : Var (Γ' ++ Γ))
 (p : lookup-Var (Γ' ++ Γ) v ≡ β) →
 eq-Var (thevar Γ' α) (weak-var Γ' Γ v) ≡ false
occurs-p-2-i-var ε v p = refl
occurs-p-2-i-var (γ ∷ Γ') this p = refl
occurs-p-2-i-var (γ ∷ Γ') (next v) p = occurs-p-2-i-var Γ' v p

occurs-p-2-i : ∀ {n} {Γ : Ctx n} {α β : Type n} (Γ' : Ctx n) (F : Form (Γ' ++ Γ) β) →
 occurs {n} {Γ' ++ (α ∷ Γ)} (thevar Γ' α) (weak-i Γ' Γ F) ≡ false
occurs-p-2-i Γ' (var v p) = occurs-p-2-i-var Γ' v p
occurs-p-2-i Γ' N = refl
occurs-p-2-i Γ' A = refl
occurs-p-2-i Γ' Π = refl
occurs-p-2-i Γ' i = refl
occurs-p-2-i {n} {Γ} {α} {β} Γ' (app f₁ f₂) = subst (λ z → z ∨ occurs (thevar Γ' α) (weak-i Γ' Γ f₂) ≡ false) (sym (occurs-p-2-i {n} {Γ} {α} {_ > β} Γ' f₁)) (occurs-p-2-i {n} {Γ} {α} Γ' f₂)  -- rewrite occurs-p-2-i {n} {Γ} {α} {_ > β} Γ' f₁ | occurs-p-2-i {n} {Γ} {α} Γ' f₂ = refl
occurs-p-2-i Γ' (lam γ f) = occurs-p-2-i (γ ∷ Γ') f

occurs-p-2 : ∀ {n} {Γ : Ctx n} {α β : Type n} (F : Form Γ β) →
 occurs {n} {α ∷ Γ} this (weak F) ≡ false
occurs-p-2 F = occurs-p-2-i ε F

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

sub-sub-weak-weak-p-3-i-var-2-this : ∀ {n} → {Γ Γ' : Ctx n} {α β γ : Type n} →
 (Γ1 Γ2 : Ctx n) →
 (eq1 : γ ∷ Γ1 ≡ γ ∷ (Γ' ++ (α ∷ (α ∷ Γ)))) →
 (eq2 : γ ∷ Γ2 ≡ γ ∷ (Γ' ++ (α ∷ Γ))) →
 (p1 : lookup-Var (γ ∷ (Γ' ++ (α ∷ (α ∷ Γ)))) (subst Var eq1 this) ≡ β) →
 (p2 : lookup-Var (γ ∷ (Γ' ++ (α ∷ Γ))) (subst Var eq2 this) ≡ β) →
 sub-var (γ ∷ Γ') (α ∷ Γ) (var this refl) (subst Var eq1 this) p1 ≡ var (subst Var eq2 this) p2
sub-sub-weak-weak-p-3-i-var-2-this {n} {Γ} {Γ'} {α} .(Γ' ++ (α ∷ (α ∷ Γ))) .(Γ' ++ (α ∷ Γ)) refl refl refl refl = refl

mutual
 sub-sub-weak-weak-p-3-i-var-2-next : ∀ {n} → {Γ Γ' : Ctx n} {α β γ : Type n}
  (x : Var ((Γ' ++ (α ∷ ε)) ++ Γ)) →
  (Γ1 Γ2 : Ctx n) →
  (eq1 : γ ∷ Γ1 ≡ γ ∷ (Γ' ++ (α ∷ (α ∷ Γ)))) →
  (eq12 : (Γ' ++ (α ∷ ε)) ++ (α ∷ Γ) ≡ Γ1) →
  (eq2 : γ ∷ Γ2 ≡ γ ∷ (Γ' ++ (α ∷ Γ))) →
  (eq22 : (Γ' ++ (α ∷ ε)) ++ Γ ≡ Γ2) →
  (p1 : lookup-Var ((γ ∷ Γ') ++ (lookup-Var (α ∷ Γ) this ∷ (α ∷ Γ))) (subst Var eq1 (next (subst Var eq12 (weak-var (Γ' ++ (α ∷ ε)) Γ x)))) ≡ β) →
  (p2 : lookup-Var (γ ∷ (Γ' ++ (α ∷ Γ))) (subst Var eq2 (next (subst Var eq22 x))) ≡ β) →
  sub-var (γ ∷ Γ') (α ∷ Γ) (var this refl) (subst Var eq1 (next (subst Var eq12 (weak-var (Γ' ++ (α ∷ ε)) Γ x)))) p1
  ≡ var (subst Var eq2 (next (subst Var eq22 x))) p2
 sub-sub-weak-weak-p-3-i-var-2-next {n} {Γ} {Γ'} {α} x .(Γ' ++ (α ∷ (α ∷ Γ))) .(Γ' ++ (α ∷ Γ)) refl eq12 refl eq22 p1 p2 = cong (weak-i ε (Γ' ++ (α ∷ Γ))) (sub-sub-weak-weak-p-3-i-var-2 {n} {Γ} {Γ'} {α} x eq12 eq22 p1 p2)

 sub-sub-weak-weak-p-3-i-var-2 : ∀ {n} → {Γ Γ' : Ctx n} {α β : Type n} (x : Var ((Γ' ++ (α ∷ ε)) ++ Γ)) →
  (eq1 : (Γ' ++ (α ∷ ε)) ++ (α ∷ Γ) ≡ Γ' ++ (α ∷ (α ∷ Γ))) →
  (eq2 : (Γ' ++ (α ∷ ε)) ++ Γ ≡ Γ' ++ (α ∷ Γ)) →
  (p1 : lookup-Var (Γ' ++ (α ∷ (α ∷ Γ))) (subst Var eq1 (weak-var (Γ' ++ (α ∷ ε)) Γ x)) ≡ β) →
  (p2 : lookup-Var (Γ' ++ (α ∷ Γ)) (subst Var eq2 x) ≡ β) →
  sub-var Γ' (α ∷ Γ) (var this refl) (subst Var eq1 (weak-var (Γ' ++ (α ∷ ε)) Γ x)) p1
  ≡ var (subst Var eq2 x) p2
 sub-sub-weak-weak-p-3-i-var-2 {n} {Γ} {ε} this refl refl refl refl = refl
 sub-sub-weak-weak-p-3-i-var-2 {n} {Γ} {ε} (next x) refl refl refl refl = refl
 sub-sub-weak-weak-p-3-i-var-2 {n} {Γ} {γ ∷ Γ'} this eq1 eq2 p1 p2 = sub-sub-weak-weak-p-3-i-var-2-this {n} {Γ} {Γ'} {_} {_} {γ} ((Γ' ++ (_ ∷ ε)) ++ (_ ∷ Γ)) ((Γ' ++ (_ ∷ ε)) ++ Γ) eq1 eq2 p1 p2
 sub-sub-weak-weak-p-3-i-var-2 {n} {Γ} {γ ∷ Γ'} (next x) eq1 eq2 p1 p2 = sub-sub-weak-weak-p-3-i-var-2-next {n} {Γ} {Γ'} {_} {_} {γ} x ((Γ' ++ (_ ∷ ε)) ++ (_ ∷ Γ)) ((Γ' ++ (_ ∷ ε)) ++ Γ) eq1 refl eq2 refl p1 p2

sub-sub-weak-weak-p-3-i-var : ∀ {n} → {Γ Γ' : Ctx n} {α β : Type n} (x : Var ((Γ' ++ (α ∷ ε)) ++ Γ)) →
 (Γ1 Γ2 : Ctx n) →
 (eq11 : Γ1 ≡ Γ' ++ (α ∷ (α ∷ Γ))) →
 (eq12 : (Γ' ++ (α ∷ ε)) ++ (α ∷ Γ) ≡ Γ1) →
 (eq21 : Γ2 ≡ Γ' ++ (α ∷ Γ)) →
 (eq22 : (Γ' ++ (α ∷ ε)) ++ Γ ≡ Γ2) →
 (p1 : lookup-Var Γ1 (subst Var eq12 (weak-var (Γ' ++ (α ∷ ε)) Γ x)) ≡ β) →
 (p2 : lookup-Var Γ2 (subst Var eq22 x) ≡ β) →
 sub-i Γ' (α ∷ Γ) (var this refl) (subst (λ z → Form z β) eq11 (var (subst Var eq12 (weak-var (Γ' ++ (α ∷ ε)) Γ x)) p1))
 ≡ subst (λ z → Form z β) eq21 (var (subst Var eq22 x) p2)
sub-sub-weak-weak-p-3-i-var {n} {Γ} {Γ'} {α} x .(Γ' ++ (α ∷ (α ∷ Γ))) .(Γ' ++ (α ∷ Γ)) refl eq12 refl eq22 p1 p2 = sub-sub-weak-weak-p-3-i-var-2 {n} {Γ} {Γ'} {α} x eq12 eq22 p1 p2

mutual
 sub-sub-weak-weak-p-3-i-app : ∀ {n} → {Γ Γ' : Ctx n} {α β γ : Type n}
  (f₁ : Form ((Γ' ++ (α ∷ ε)) ++ Γ) (γ > β)) →
  (f₂ : Form ((Γ' ++ (α ∷ ε)) ++ Γ) γ) →
  (Γ1 Γ2 : Ctx n) →
  (eq1 : Γ1 ≡ Γ' ++ (α ∷ (α ∷ Γ))) →
  (eq12 : (Γ' ++ (α ∷ ε)) ++ (α ∷ Γ) ≡ Γ1) →
  (eq2 : Γ2 ≡ Γ' ++ (α ∷ Γ)) →
  (eq22 : (Γ' ++ (α ∷ ε)) ++ Γ ≡ Γ2) →
  sub-i Γ' (α ∷ Γ) (var this refl) (subst (λ z → Form z β) eq1 (app (subst (λ z → Form z (γ > β)) eq12 (weak-i (Γ' ++ (α ∷ ε)) Γ f₁)) (subst (λ z → Form z γ) eq12 (weak-i (Γ' ++ (α ∷ ε)) Γ f₂))))
  ≡ subst (λ z → Form z β) eq2 (app (subst (λ z → Form z (γ > β)) eq22 f₁) (subst (λ z → Form z γ) eq22 f₂))
 sub-sub-weak-weak-p-3-i-app {n} {Γ} {Γ'} {α} {β} {γ} f₁ f₂ .(Γ' ++ (α ∷ (α ∷ Γ))) .(Γ' ++ (α ∷ Γ)) refl eq12 refl eq22 = trans (cong (λ z → app z (sub-i Γ' (α ∷ Γ) (var this refl) (subst (λ z → Form z γ) eq12 (weak-i (Γ' ++ (α ∷ ε)) Γ f₂)))) (sub-sub-weak-weak-p-3-i {n} {Γ} {Γ'} {α} {γ > β} f₁ eq12 eq22)) (cong (app (subst (λ z → Form z (γ > β)) eq22 f₁)) (sub-sub-weak-weak-p-3-i {n} {Γ} {Γ'} {α} {γ} f₂ eq12 eq22))

 sub-sub-weak-weak-p-3-i-lam : ∀ {n} → {Γ Γ' : Ctx n} {α β γ : Type n}
  (f : Form (γ ∷ ((Γ' ++ (α ∷ ε)) ++ Γ)) β)
  (Γ1 Γ2 : Ctx n)
  (eq1 : Γ1 ≡ Γ' ++ (α ∷ (α ∷ Γ)))
  (eq12 : γ ∷ ((Γ' ++ (α ∷ ε)) ++ (α ∷ Γ)) ≡ γ ∷ Γ1)
  (eq2 : Γ2 ≡ Γ' ++ (α ∷ Γ))
  (eq22 : γ ∷ ((Γ' ++ (α ∷ ε)) ++ Γ) ≡ γ ∷ Γ2) →
  sub-i Γ' (α ∷ Γ) (var this refl) (subst (λ z → Form z (γ > β)) eq1 (lam γ (subst (λ z → Form z β) eq12 (weak-i (γ ∷ (Γ' ++ (α ∷ ε))) Γ f))))
  ≡ subst (λ z → Form z (γ > β)) eq2 (lam γ (subst (λ z → Form z β) eq22 f))
 sub-sub-weak-weak-p-3-i-lam {n} {Γ} {Γ'} {α} {β} {γ} f .(Γ' ++ (α ∷ (α ∷ Γ))) .(Γ' ++ (α ∷ Γ)) refl eq12 refl eq22 = cong (lam γ) (sub-sub-weak-weak-p-3-i {n} {Γ} {γ ∷ Γ'} {α} {β} f eq12 eq22)

 sub-sub-weak-weak-p-3-i : ∀ {n} → {Γ Γ' : Ctx n} {α β : Type n} (G : Form ((Γ' ++ (α ∷ ε)) ++ Γ) β) →
  (eq1 : (Γ' ++ (α ∷ ε)) ++ (α ∷ Γ) ≡ Γ' ++ (α ∷ (α ∷ Γ))) →
  (eq2 : (Γ' ++ (α ∷ ε)) ++ Γ ≡ Γ' ++ (α ∷ Γ)) →
  sub-i Γ' (α ∷ Γ) (var this refl) (subst (λ z → Form z β) eq1 (weak-i (Γ' ++ (α ∷ ε)) Γ G)) ≡ subst (λ z → Form z β) eq2 G
 sub-sub-weak-weak-p-3-i {n} {Γ} {Γ'} {α} {β} (var x p) eq1 eq2 = sub-sub-weak-weak-p-3-i-var {n} {Γ} {Γ'} {α} {β} x ((Γ' ++ (α ∷ ε)) ++ (α ∷ Γ)) ((Γ' ++ (α ∷ ε)) ++ Γ) eq1 refl eq2 refl (trans (weak-var-p (Γ' ++ (α ∷ ε)) Γ x) p) p
 sub-sub-weak-weak-p-3-i {_} {Γ} {Γ'} {α} {$o > $o} N eq1 eq2 = erase-subst (Ctx _) (λ z → Form z ($o > $o)) N ((Γ' ++ (α ∷ ε)) ++ Γ) (Γ' ++ (α ∷ Γ)) eq2 (λ z → sub-i Γ' (α ∷ Γ) (var this refl) (subst (λ z → Form z ($o > $o)) eq1 N) ≡ z) (erase-subst (Ctx _) (λ z → Form z ($o > $o)) N ((Γ' ++ (α ∷ ε)) ++ (α ∷ Γ)) (Γ' ++ (α ∷ (α ∷ Γ))) eq1 (λ z → sub-i Γ' (α ∷ Γ) (var this refl) z ≡ N) refl)  -- rewrite eq2 | eq1 = refl
 sub-sub-weak-weak-p-3-i {_} {Γ} {Γ'} {α} {$o > ($o > $o)} A eq1 eq2 = erase-subst (Ctx _) (λ z → Form z ($o > ($o > $o))) A ((Γ' ++ (α ∷ ε)) ++ Γ) (Γ' ++ (α ∷ Γ)) eq2 (λ z → sub-i Γ' (α ∷ Γ) (var this refl) (subst (λ z → Form z ($o > ($o > $o))) eq1 A) ≡ z) (erase-subst (Ctx _) (λ z → Form z ($o > ($o > $o))) A ((Γ' ++ (α ∷ ε)) ++ (α ∷ Γ)) (Γ' ++ (α ∷ (α ∷ Γ))) eq1 (λ z → sub-i Γ' (α ∷ Γ) (var this refl) z ≡ A) refl)  -- rewrite eq2 | eq1 = refl
 sub-sub-weak-weak-p-3-i {_} {Γ} {Γ'} {α} {(β > $o) > $o} Π eq1 eq2 = erase-subst (Ctx _) (λ z → Form z ((β > $o) > $o)) Π ((Γ' ++ (α ∷ ε)) ++ Γ) (Γ' ++ (α ∷ Γ)) eq2 (λ z → sub-i Γ' (α ∷ Γ) (var this refl) (subst (λ z → Form z ((β > $o) > $o)) eq1 Π) ≡ z) (erase-subst (Ctx _) (λ z → Form z ((β > $o) > $o)) Π ((Γ' ++ (α ∷ ε)) ++ (α ∷ Γ)) (Γ' ++ (α ∷ (α ∷ Γ))) eq1 (λ z → sub-i Γ' (α ∷ Γ) (var this refl) z ≡ Π) refl)  -- rewrite eq2 | eq1 = refl
 sub-sub-weak-weak-p-3-i {_} {Γ} {Γ'} {α} {(β > $o) > .β} i eq1 eq2 = erase-subst (Ctx _) (λ z → Form z ((β > $o) > β)) i ((Γ' ++ (α ∷ ε)) ++ Γ) (Γ' ++ (α ∷ Γ)) eq2 (λ z → sub-i Γ' (α ∷ Γ) (var this refl) (subst (λ z → Form z ((β > $o) > β)) eq1 i) ≡ z) (erase-subst (Ctx _) (λ z → Form z ((β > $o) > β)) i ((Γ' ++ (α ∷ ε)) ++ (α ∷ Γ)) (Γ' ++ (α ∷ (α ∷ Γ))) eq1 (λ z → sub-i Γ' (α ∷ Γ) (var this refl) z ≡ i) refl)  -- rewrite eq2 | eq1 = refl
 sub-sub-weak-weak-p-3-i {_} {Γ} {Γ'} {α} (app f₁ f₂) eq1 eq2 = sub-sub-weak-weak-p-3-i-app {_} {Γ} {Γ'} {α} f₁ f₂ ((Γ' ++ (α ∷ ε)) ++ (α ∷ Γ)) ((Γ' ++ (α ∷ ε)) ++ Γ) eq1 refl eq2 refl
 sub-sub-weak-weak-p-3-i {_} {Γ} {Γ'} {α} (lam γ f) eq1 eq2 = sub-sub-weak-weak-p-3-i-lam {_} {Γ} {Γ'} {α} f ((Γ' ++ (α ∷ ε)) ++ (α ∷ Γ)) ((Γ' ++ (α ∷ ε)) ++ Γ) eq1 refl eq2 refl

sub-sub-weak-weak-p-3 : ∀ {n} → {Γ : Ctx n} {α β : Type n} (G : Form (α ∷ Γ) β) →
 sub (var this refl) (weak-i (α ∷ ε) Γ G) ≡ G
sub-sub-weak-weak-p-3 G = sub-sub-weak-weak-p-3-i {_} {_} {ε} G refl refl

sub-sub-weak-weak-p : ∀ {n} → {Γ : Ctx n} {α β : Type n} (F : Form Γ β) (G : Form (α ∷ Γ) β) →
 sub (var this refl) (sub-i (α ∷ (α ∷ ε)) Γ F (weak-i (α ∷ ε) (β ∷ Γ) (weak-i (α ∷ ε) Γ G))) ≡ G
sub-sub-weak-weak-p {_} {Γ} {α} {β} F G = subst (λ z → sub (var this refl) z ≡ G) (sub-weak-p-1-i (α ∷ ε) G F refl refl) (sub-sub-weak-weak-p-3 G)

sub-sub-weak-weak-p-2 : ∀ {n} → {Γ : Ctx n} {α β : Type n} (F G : Form (α ∷ Γ) β) →
 sub (var this refl) (sub-i (α ∷ (α ∷ ε)) Γ (lam α G) (weak-i (α ∷ ε) ((α > β) ∷ Γ) (weak-i (α ∷ ε) Γ F))) ≡ F
sub-sub-weak-weak-p-2 {_} {Γ} {α} {β} F G = subst (λ z → sub (var this refl) z ≡ F) (sub-weak-p-1-i (α ∷ ε) F (lam α G) refl refl) (sub-sub-weak-weak-p-3 F)

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

mutual
 headNorm : {n : ℕ} {Γ : Ctx n} {α : Type n} → ℕ → Form Γ α → Form Γ α
-- headNorm m (app (app (lam α (lam _ (app Π (lam (_ > $o) (app (app A (app N (app (var this _) (var (next (next this)) _)))) (app (var this _) (var (next this) _))))))) F) G) = ?
 headNorm m (app F G) = headNorm' m (headNorm m F) G
 headNorm _ F = F

 headNorm' : {n : ℕ} {Γ : Ctx n} {α β : Type n} → ℕ → Form Γ (α > β) → Form Γ α → Form Γ β
 headNorm' (suc m) (lam _ F) G = headNorm m (sub G F)
 headNorm' 0 (lam _ F) G = app (lam _ F) G
 headNorm' _ F G = app F G

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

!'[_]_ : ∀ {n} → {Γ : Ctx n} → (α : Type n) → Form Γ (α > $o) → Form Γ $o
!'[ α ] F = app Π F

?'[_]_ : ∀ {n} → {Γ : Ctx n} → (α : Type n) → Form Γ (α > $o) → Form Γ $o
?'[ α ] F = ?[ α ] (weak F · $ this {refl})

ι' : ∀ {n} → {Γ : Ctx n} → (α : Type n) → Form Γ (α > $o) → Form Γ α
ι' α F = app i F

max_stars_repo_name: frelindb/agsyHOL

max_issues_repo_name: frelindb/agsyHOL

max_forks_repo_name: frelindb/agsyHOL


text:
-- Andreas, 2018-06-03, issue #3102
-- Regression: slow reduce with lots of module parameters and an import.

-- {-# OPTIONS -v tc.cc:30 -v tc.cover.top:30 --profile=internal #-}

open import Agda.Builtin.Bool

module _ (A B C D E F G H I J K L M O P Q R S T U V W X Y Z
          A₁ B₁ C₁ D₁ E₁ F₁ G₁ H₁ I₁ J₁ K₁ L₁ M₁ O₁ P₁ Q₁ R₁ S₁ T₁ U₁ V₁ W₁ X₁ Y₁ Z₁
          A₂ B₂ C₂ D₂ E₂ F₂ G₂ H₂ I₂ J₂ K₂ L₂ M₂ O₂ P₂ Q₂ R₂ S₂ T₂ U₂ V₂ W₂ X₂ Y₂ Z₂
          A₃ B₃ C₃ D₃ E₃ F₃ G₃ H₃ I₃ J₃ K₃ L₃ M₃ O₃ P₃ Q₃ R₃ S₃ T₃ U₃ V₃ W₃ X₃ Y₃ Z₃
          A₄ B₄ C₄ D₄ E₄ F₄ G₄ H₄ I₄ J₄ K₄ L₄ M₄ O₄ P₄ Q₄ R₄ S₄ T₄ U₄ V₄ W₄ X₄ Y₄ Z₄
          : Set) where

test : Bool → Bool
test true  = false
test false = false

-- Should succeed instantaneously.


text:
module AmbiguousTopLevelModuleName where

import Imports.Ambiguous


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

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

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.ConsensusProvider      as ConsensusProvider
open import LibraBFT.Impl.Properties.Util
import      LibraBFT.Impl.IO.OBM.GenKeyFile                as GenKeyFile
open import LibraBFT.Impl.OBM.Logging.Logging
import      LibraBFT.Impl.Types.ValidatorVerifier          as ValidatorVerifier
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import LibraBFT.ImplShared.Consensus.Types.EpochIndep
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.PKCS
open import Util.Prelude                                   hiding (_++_)

module LibraBFT.Impl.Consensus.Properties.ConsensusProvider where

open InitProofDefs

module startConsensusSpec
  (nodeConfig : NodeConfig)
  (now        : Instant)
  (payload    : OnChainConfigPayload)
  (liws       : LedgerInfoWithSignatures)
  (sk         : SK)
  (needFetch  : ObmNeedFetch)
  (propGen    : ProposalGenerator)
  (stateComp  : StateComputer)
  where

  -- TODO-2: Requires refinement
  postulate
   contract' : EitherD-weakestPre (ConsensusProvider.startConsensus-ed-abs
                                    nodeConfig now payload liws sk needFetch propGen stateComp)
                                  (InitContract nothing)


text:
-- Andreas, 2012-07-26, reported by Nisse
module Issue678 where

module Unit where

  data Unit : Set where
    unit : Unit

  El : Unit → Set
  El unit = Unit

  data IsUnit : Unit → Set where
    isUnit : IsUnit unit

  test : (u : Unit)(x : El u)(p : IsUnit u) → Set
  test .unit unit isUnit = Unit
  -- this requires the coverage checker to skip the first split opportunity, x,
  -- and move on to the second, p

module NisseOriginalTestCase where

  record Box (A : Set) : Set where
    constructor [_]
    field unbox : A

  data U : Set where
    box : U → U

  El : U → Set
  El (box a) = Box (El a)

  data Q : ∀ a → El a → El a → Set where
    q₁ : ∀ {a x} → Q (box a) [ x ] [ x ]
    q₂ : ∀ {a} {x y : El a} → Q a x y

  data P : ∀ a → El a → El a → Set where
    p : ∀ {a x y z} → P a x y → P a y z → P a x z

  foo : ∀ {a xs ys} → P a xs ys → Q a xs ys
  foo (p p₁ p₂) with foo p₁ | foo p₂
  foo (p p₁ p₂) | q₁ | _ = q₂
  foo (p p₁ p₂) | q₂ | _ = q₂

-- Error was:
-- Cannot split on argument of non-datatype El @1
-- when checking the definition of with-33


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

module Naturals where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

_+N_ : ℕ → ℕ → ℕ
zero +N b = b
succ a +N b = succ (a +N b)


text:
module Cats.Category.Base where

open import Level
open import Relation.Binary using
  (Rel ; IsEquivalence ; _Preserves_⟶_ ; _Preserves₂_⟶_⟶_ ; Setoid)
open import Relation.Binary.EqReasoning as EqReasoning

import Cats.Util.SetoidReasoning as SetoidR

record Category lo la l≈ : Set (suc (lo ⊔ la ⊔ l≈)) where
  infixr  9 _∘_
  infix   4 _≈_
  infixr  -1 _⇒_

  field
    Obj : Set lo
    _⇒_ : Obj → Obj → Set la
    _≈_ : ∀ {A B} → Rel (A ⇒ B) l≈
    id : {O : Obj} → O ⇒ O
    _∘_ : ∀ {A B C} → B ⇒ C → A ⇒ B → A ⇒ C
    equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
    ∘-resp : ∀ {A B C} → (_∘_ {A} {B} {C}) Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
    id-r : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f
    id-l : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
    assoc : ∀ {A B C D} {f : C ⇒ D} {g : B ⇒ C} {h : A ⇒ B}
      → (f ∘ g) ∘ h ≈ f ∘ (g ∘ h)

  Hom : (A B : Obj) → Setoid la l≈
  Hom A B = record
      { Carrier = A ⇒ B
      ; _≈_ = _≈_
      ; isEquivalence = equiv
      }

  module ≈ {A B} = IsEquivalence (equiv {A} {B})

  module ≈-Reasoning {A B} where

    open EqReasoning (Hom A B) public

    triangle = SetoidR.triangle (Hom A B)

  unassoc : ∀ {A B C D} {f : C ⇒ D} {g : B ⇒ C} {h : A ⇒ B}
    → f ∘ (g ∘ h) ≈ (f ∘ g) ∘ h
  unassoc = ≈.sym assoc

  ∘-resp-r : ∀ {A B C} {f : B ⇒ C} → (_∘_ {A} f) Preserves _≈_ ⟶ _≈_
  ∘-resp-r eq = ∘-resp ≈.refl eq

  ∘-resp-l :  ∀ {A B C} {g : A ⇒ B} → (λ f → _∘_ {C = C} f g) Preserves _≈_ ⟶ _≈_
  ∘-resp-l eq = ∘-resp eq ≈.refl

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-# OPTIONS --rewriting --confluence-check #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

postulate
  A : Set
  a b : A
  f : (A → A) → A
  g : A → A

  rewf₁ : f (λ x → g x) ≡ a
  rewf₂ : f (λ x → a) ≡ b

  rewg : (x : A) → g x ≡ a

{-# REWRITE rewf₁ rewf₂ rewg #-}


text:
-- 2011-04-12 AIM XIII fixed this issue by freezing metas after declaration (Andreas & Ulf)

module Issue399 where

open import Common.Prelude

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

-- now in Common.Prelude
-- _++_ : {A : Set} → List A → List A → List A
-- []       ++ ys = ys
-- (x ∷ xs) ++ ys = x ∷ (xs ++ ys)

record MyMonadPlus m : Set₁ where
   field mzero : {a : Set} → m a → List a
         mplus : {a : Set} → m a → m a → List a
-- this produces an unsolved meta variable, because it is not clear which
-- level m has.  m could be in Set -> Set or in Set -> Set1
-- if you uncomment the rest of the files, you get unsolved metas here

{- Old error, without freezing:
--Emacs error: and the 10th line is the above line
--/home/j/dev/apps/haskell/agda/learn/bug-in-record.agda:10,36-39
--Set != Set₁
--when checking that the expression m a has type Set₁
-}

mymaybemzero : {a : Set} → Maybe a → List a
mymaybemzero nothing = []
mymaybemzero (just x) = x ∷ []

mymaybemplus : {a : Set} → Maybe a → Maybe a → List a
mymaybemplus x y = (mymaybemzero x) ++ (mymaybemzero y)

-- the following def gives a type error because of unsolved metas in MyMonadPlus
-- if you uncomment it, you see m in MyMonadPlus yellow
mymaybeMonadPlus : MyMonadPlus Maybe
mymaybeMonadPlus = record { mzero = mymaybemzero
                           ; mplus = mymaybemplus }

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --show-implicit #-}

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

postulate
  A B C D : Set
  F : (A → A) → (A → A → A) → A
  a : A

data Tree : Set where
  leaf : Tree
  node : (f : (x : A) → Tree) → Tree

tree1 : Nat → Tree
tree1 zero = leaf
tree1 (suc n) = node (λ x → tree1 n)

tree2 : Nat → Tree
tree2 zero = leaf
tree2 (suc n) = node (λ x → tree2 n)

-- In Agda 2.6.0.1, this takes >50 sec and >5GB to typecheck.
test : tree1 5000 ≡ tree2 5000
test = refl


text:
module FlatDomInequality where

postulate
  A : Set

g : A → A
g x = x

-- this is fine
h : (@♭ x : A) → A
h = g

-- this should fail, although the error message should be improved.
q : A → A
q = h

max_stars_repo_name: Soares/agda

max_issues_repo_name: Soares/agda

max_forks_repo_name: Soares/agda


text:
{-# OPTIONS --prop --rewriting #-}

module Examples.Sorting where

import Examples.Sorting.Sequential
import Examples.Sorting.Parallel

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Automatic solvers for equations over integers
------------------------------------------------------------------------

-- See README.Integer for examples of how to use this solver

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

module Data.Integer.Tactic.RingSolver where

open import Agda.Builtin.Reflection

open import Data.Maybe.Base using (just; nothing)
open import Data.Integer.Base
open import Data.Integer.Properties
open import Level using (0ℓ)
open import Data.Unit using (⊤)
open import Relation.Binary.PropositionalEquality
import Tactic.RingSolver as Solver
import Tactic.RingSolver.Core.AlmostCommutativeRing as ACR

------------------------------------------------------------------------
-- A module for automatically solving propositional equivalences
-- containing _+_ and _*_

ring : ACR.AlmostCommutativeRing 0ℓ 0ℓ
ring = ACR.fromCommutativeRing +-*-commutativeRing
  λ { +0 → just refl; _ → nothing }

macro
  solve-∀ : Term → TC ⊤
  solve-∀ = Solver.solve-∀-macro (quote ring)

macro
  solve : Term → Term → TC ⊤
  solve n = Solver.solve-macro n (quote ring)


text:
open import Relation.Binary
open import Level
module GGT.Setoid
  {a ℓ}
  (S : Setoid a ℓ)
  (l : Level)
  where

open import Level
open Setoid S
open import Data.Product
open import Relation.Unary
open import Relation.Binary.Construct.On renaming (isEquivalence to isEq)

open import Function

subSetoid : (Pred Carrier l) → Setoid (a ⊔ l) ℓ
subSetoid P =
  record { Carrier = Σ Carrier P ;
           _≈_ = (_≈_ on proj₁) ;
           isEquivalence = isEq proj₁ isEquivalence }

max_stars_repo_name: zampino/ggt

max_issues_repo_name: zampino/ggt

max_forks_repo_name: zampino/ggt


text:
open import SOAS.Metatheory.Syntax

-- Metatheory of a second-order syntax
module SOAS.Metatheory {T : Set} (Syn : Syntax {T}) where

open import SOAS.Families.Core {T}

open import SOAS.Abstract.ExpStrength

open Syntax Syn

open CompatStrengths ⅀:CS public renaming (CoalgStr to ⅀:Str ; ExpStr to ⅀:ExpStr)

open import SOAS.Metatheory.Algebra ⅀F public
open import SOAS.Metatheory.Monoid ⅀F ⅀:Str public

module Theory (𝔛 : Familyₛ) where
  open import SOAS.Metatheory.MetaAlgebra   ⅀F 𝔛 public
  open import SOAS.Metatheory.Semantics     ⅀F ⅀:Str 𝔛 (𝕋:Init 𝔛) public
  open import SOAS.Metatheory.Traversal     ⅀F ⅀:Str 𝔛 (𝕋:Init 𝔛) public
  open import SOAS.Metatheory.Renaming      ⅀F ⅀:Str 𝔛 (𝕋:Init 𝔛) public
  open import SOAS.Metatheory.Coalgebraic   ⅀F ⅀:Str 𝔛 (𝕋:Init 𝔛) public
  open import SOAS.Metatheory.Substitution  ⅀F ⅀:Str 𝔛 (𝕋:Init 𝔛) public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
{-# OPTIONS --universe-polymorphism #-}

open import Level

module Categories.Terminal {o ℓ e : Level} where

open import Categories.Category
open import Categories.Functor
open import Categories.Categories
import Categories.Object.Terminal as Terminal

open Terminal (Categories o ℓ e)

record Unit {x : _} : Set x where
  constructor unit

OneC : Category o ℓ e
OneC = record
  { Obj = Unit
  ; _⇒_ = λ _ _ → Unit
  ; _≡_ = λ _ _ → Unit
  ; _∘_ = λ _ _ → unit
  ; id = unit
  ; assoc = unit
  ; identityˡ = unit
  ; identityʳ = unit
  ; equiv = record
    { refl = unit
    ; sym = λ _ → unit
    ; trans = λ _ _ → unit
    }
  ; ∘-resp-≡ = λ _ _ → unit
  }

-- I can probably use Discrete here once we get universe cumulativity in Agda
One : Terminal
One = record
  { ⊤ = OneC
  ; ! = record
    { F₀ = λ _ → unit
    ; F₁ = λ _ → unit
    ; identity = unit
    ; homomorphism = unit
    ; F-resp-≡ = λ _ → unit
    }
  ; !-unique = λ _ _ → Heterogeneous.≡⇒∼ unit
  }

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Andreas, 2013-11-23
-- Make sure sized types work with extended lambda

{-# OPTIONS --copatterns --sized-types #-}

-- {-# OPTIONS -v tc.def:100 -v tc.size:100 -v tc.meta.assign:20 #-}

module SizedTypesExtendedLambda where

open import Common.Size

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

mutual

  data Delay (A : Set) (i : Size) : Set where
    fail  : Delay A i
    now   : A → Delay A i
    later : ∞Delay A i → Delay A i

  record ∞Delay (A : Set) (i : Size) : Set where
    coinductive
    constructor delay
    field
      force : {j : Size< i} → Delay A j

open ∞Delay

postulate
  A : Set
  something : ∀ {C : Set} → (Maybe A → C) → C

mutual
  test : {i : Size} → Delay A i
  test = something λ
           { nothing  -> fail
           ; (just a) -> later (∞test a)
           }

  ∞test : {i : Size} (a : A) → ∞Delay A i
  force (∞test a) {j = _} = test
  -- force (∞test a) = test  -- still fails, unfortunately


text:
module Numeral.Natural.Oper.FlooredDivision where

import Lvl
open import Data
open import Data.Boolean.Stmt
open import Logic.Propositional.Theorems
open import Numeral.Natural
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.Comparisons.Proofs
open import Numeral.Natural.Relation.Order
open import Relator.Equals

infixl 10100 _⌊/⌋_

-- Inductive definition of an algorithm for division.
-- `[ d , b ] a' div b'` should be interpreted as following:
--   `d` is the result of the algorithm that is being incremented as it runs.
--   `b` is the predecessor of the original denominator. This is constant throughout the whole process.
--   `a'` is the numerator. This is decremented as it runs.
--   `b'` is the predecessor of the temporary denominator. This is decremented as it runs.
-- By decrementing both `a'` and `b'`, and incrementing `d` when 'b`' reaches 0, it counts how many times `b` "fits into" `a`.
-- Note: See Numeral.Natural.Oper.Modulo for a similiar algorithm used to determine the modulo.
[_,_]_div_ : ℕ → ℕ → ℕ → ℕ → ℕ
[ d , _ ] 𝟎     div _     = d
[ d , b ] 𝐒(a') div 𝟎     = [ 𝐒(d) , b ] a' div b
[ d , b ] 𝐒(a') div 𝐒(b') = [ d   , b ] a' div b'
{-# BUILTIN NATDIVSUCAUX [_,_]_div_ #-}

-- Floored division operation.
_⌊/⌋_ : ℕ → (m : ℕ) → .⦃ _ : IsTrue(positive?(m)) ⦄ → ℕ
a ⌊/⌋ 𝐒(m) = [ 𝟎 , m ] a div m

_⌊/⌋₀_ : ℕ → ℕ → ℕ
_ ⌊/⌋₀ 𝟎    = 𝟎
a ⌊/⌋₀ 𝐒(m) = a ⌊/⌋ 𝐒(m)
{-# INLINE _⌊/⌋₀_ #-}