text:
{-# OPTIONS --without-K #-}
module well-typed-syntax-helpers where
open import common
open import well-typed-syntax

infixl 3 _‘'’ₐ_
infixr 1 _‘→'’_
infixl 3 _‘t’_
infixl 3 _‘t’₁_
infixl 3 _‘t’₂_
infixr 2 _‘∘’_

WS∀ : ∀ {Γ T T' A B} {a : Term {Γ = Γ} T} → Term {Γ = Γ ▻ T'} (W ((A ‘→’ B) ‘’ a)) → Term {Γ ▻ T'} (W ((A ‘’ a) ‘→’ (B ‘’₁ a)))
WS∀ = weakenTyp-substTyp-tProd

_‘→'’_ : ∀ {Γ} → Typ Γ → Typ Γ → Typ Γ
_‘→'’_ {Γ = Γ} A B = _‘→’_ {Γ = Γ} A (W {Γ = Γ} {A = A} B)

_‘'’ₐ_ : ∀ {Γ A B} → Term {Γ} (A ‘→'’ B) → Term A → Term B
_‘'’ₐ_ {Γ} {A} {B} f x = SW (_‘’ₐ_ {Γ} {A} {W B} f x)

_‘t’_ : ∀ {Γ A} {B : Typ (Γ ▻ A)} → (b : Term {Γ = Γ ▻ A} B) → (a : Term {Γ} A) → Term {Γ} (B ‘’ a)
b ‘t’ a = ‘λ∙’ b ‘’ₐ a

substTyp-tProd : ∀ {Γ T A B} {a : Term {Γ} T} →
                         Term {Γ} ((A ‘→’ B) ‘’ a)
                         → Term {Γ} (_‘→’_ {Γ = Γ} (A ‘’ a) (B ‘’₁ a))
substTyp-tProd {Γ} {T} {A} {B} {a} x = SW ((WS∀ (w x)) ‘t’ a)

S∀ = substTyp-tProd

‘λ'∙’ : ∀ {Γ A B} → Term {Γ ▻ A} (W B) -> Term (A ‘→'’ B)
‘λ'∙’ f = ‘λ∙’ f

SW1V : ∀ {Γ A T} → Term {Γ ▻ A} (W1 T ‘’ ‘VAR₀’) → Term {Γ ▻ A} T
SW1V = substTyp-weakenTyp1-VAR₀

S₁∀ : ∀ {Γ T T' A B} {a : Term {Γ} T} → Term {Γ ▻ T' ‘’ a} ((A ‘→’ B) ‘’₁ a) → Term {Γ ▻ T' ‘’ a} ((A ‘’₁ a) ‘→’ (B ‘’₂ a))
S₁∀ = substTyp1-tProd

un‘λ∙’ : ∀ {Γ A B} → Term (A ‘→’ B) → Term {Γ ▻ A} B
un‘λ∙’ f = SW1V (weakenTyp-tProd (w f) ‘’ₐ ‘VAR₀’)

weakenProd : ∀ {Γ A B C} →
                          Term {Γ} (A ‘→’ B)
                          → Term {Γ = Γ ▻ C} (W A ‘→’ W1 B)
weakenProd {Γ} {A} {B} {C} x = weakenTyp-tProd (w x)
w∀ = weakenProd

w1 : ∀ {Γ A B C} → Term {Γ = Γ ▻ B} C → Term {Γ = Γ ▻ A ▻ W {Γ = Γ} {A = A} B} (W1 {Γ = Γ} {A = A} {B = B} C)
w1 x = un‘λ∙’ (weakenTyp-tProd (w (‘λ∙’ x)))

_‘t’₁_ : ∀ {Γ A B C} → (c : Term {Γ = Γ ▻ A ▻ B} C) → (a : Term {Γ} A) → Term {Γ = Γ ▻ B ‘’ a} (C ‘’₁ a)
f ‘t’₁ x = un‘λ∙’ (S∀ (‘λ∙’ (‘λ∙’ f) ‘’ₐ x))
_‘t’₂_ : ∀ {Γ A B C D} → (c : Term {Γ = Γ ▻ A ▻ B ▻ C} D) → (a : Term {Γ} A) → Term {Γ = Γ ▻ B ‘’ a ▻ C ‘’₁ a} (D ‘’₂ a)
f ‘t’₂ x = un‘λ∙’ (S₁∀ (un‘λ∙’ (S∀ (‘λ∙’ (‘λ∙’ (‘λ∙’ f)) ‘’ₐ x))))

S₁₀W' : ∀ {Γ C T A} {a : Term {Γ} C} {b : Term {Γ} (T ‘’ a)} → Term {Γ} (A ‘’ a) → Term {Γ} (W A ‘’₁ a ‘’ b)
S₁₀W' = substTyp1-substTyp-weakenTyp-inv

S₁₀W : ∀ {Γ C T A} {a : Term {Γ} C} {b : Term {Γ} (T ‘’ a)} → Term {Γ} (W A ‘’₁ a ‘’ b) → Term {Γ} (A ‘’ a)
S₁₀W = substTyp1-substTyp-weakenTyp

substTyp1-substTyp-weakenTyp-weakenTyp : ∀ {Γ T A} {B : Typ (Γ ▻ A)}
    → {a : Term {Γ} A}
    → {b : Term {Γ} (B ‘’ a)}
    → Term {Γ} (W (W T) ‘’₁ a ‘’ b)
    → Term {Γ} T
substTyp1-substTyp-weakenTyp-weakenTyp x = SW (S₁₀W x)

S₁₀WW = substTyp1-substTyp-weakenTyp-weakenTyp

S₂₁₀W : ∀ {Γ A B C T} {a : Term {Γ} A} {b : Term {Γ} (B ‘’ a)} {c : Term {Γ} (C ‘’₁ a ‘’ b)}
      → Term {Γ} (W T ‘’₂ a ‘’₁ b ‘’ c)
      → Term {Γ} (T ‘’₁ a ‘’ b)
S₂₁₀W = substTyp2-substTyp1-substTyp-weakenTyp

substTyp2-substTyp1-substTyp-weakenTyp-weakenTyp : ∀ {Γ A B C T}
         {a : Term {Γ} A}
         {b : Term {Γ} (B ‘’ a)}
         {c : Term {Γ} (C ‘’₁ a ‘’ b)} →
    Term {Γ} (W (W T) ‘’₂ a ‘’₁ b ‘’ c)
    → Term {Γ} (T ‘’ a)
substTyp2-substTyp1-substTyp-weakenTyp-weakenTyp x = S₁₀W (S₂₁₀W x)

S₂₁₀WW = substTyp2-substTyp1-substTyp-weakenTyp-weakenTyp

W1W : ∀ {Γ A B C} → Term {Γ ▻ A ▻ W B} (W1 (W C)) → Term {Γ ▻ A ▻ W B} (W (W C))
W1W = weakenTyp1-weakenTyp

W1W1W : ∀ {Γ A B C T} → Term {Γ ▻ A ▻ B ▻ W (W C)} (W1 (W1 (W T))) → Term {Γ ▻ A ▻ B ▻ W (W C)} (W1 (W (W T)))
W1W1W = weakenTyp1-weakenTyp1-weakenTyp

weakenTyp-tProd-nd : ∀ {Γ A B C} →
                          Term {Γ = Γ ▻ C} (W (A ‘→'’ B))
                          → Term {Γ = Γ ▻ C} (W A ‘→'’ W B)
weakenTyp-tProd-nd x = ‘λ'∙’ (W1W (SW1V (weakenTyp-tProd (w (weakenTyp-tProd x)) ‘’ₐ ‘VAR₀’)))

weakenProd-nd : ∀ {Γ A B C} →
                             Term (A ‘→'’ B)
                             → Term {Γ = Γ ▻ C} (W A ‘→'’ W B)
weakenProd-nd {Γ} {A} {B} {C} x = weakenTyp-tProd-nd (w x)

weakenTyp-tProd-nd-tProd-nd : ∀ {Γ A B C D} →
    Term {Γ = Γ ▻ D} (W (A ‘→'’ B ‘→'’ C))
    → Term {Γ = Γ ▻ D} (W A ‘→'’ W B ‘→'’ W C)
weakenTyp-tProd-nd-tProd-nd x = ‘λ∙’ (weakenTyp-tProd-inv (‘λ∙’ (W1W1W (SW1V (w∀ (weakenTyp-tProd (weakenTyp-weakenTyp-tProd (w→ (weakenTyp-tProd-nd x) ‘'’ₐ ‘VAR₀’))) ‘’ₐ ‘VAR₀’)))))

weakenProd-nd-Prod-nd : ∀ {Γ A B C D} →
    Term (A ‘→'’ B ‘→'’ C)
    → Term {Γ = Γ ▻ D} (W A ‘→'’ W B ‘→'’ W C)
weakenProd-nd-Prod-nd {Γ} {A} {B} {C} {D} x = weakenTyp-tProd-nd-tProd-nd (w x)
w→→ = weakenProd-nd-Prod-nd

S₁W1 : ∀ {Γ A B C} {a : Term {Γ} A} → Term {Γ ▻ W B ‘’ a} (W1 C ‘’₁ a) → Term {Γ ▻ B} C
S₁W1 = substTyp1-weakenTyp1

W1S₁W' : ∀ {Γ A T'' T' T} {a : Term {Γ} A}
      → Term {Γ ▻ T'' ▻ W (T' ‘’ a)} (W1 (W (T ‘’ a)))
      → Term {Γ ▻ T'' ▻ W (T' ‘’ a)} (W1 (W T ‘’₁ a))
W1S₁W' = weakenTyp1-substTyp-weakenTyp1-inv

substTyp-weakenTyp1-inv : ∀ {Γ A T' T}
         {a : Term {Γ} A} →
    Term {Γ = (Γ ▻ T' ‘’ a)} (W (T ‘’ a))
    → Term {Γ = (Γ ▻ T' ‘’ a)} (W T ‘’₁ a)
substTyp-weakenTyp1-inv {a = a} x = S₁W1 (W1S₁W' (w1 x) ‘t’₁ a)

S₁W' = substTyp-weakenTyp1-inv

_‘∘’_ : ∀ {Γ A B C}
    → Term {Γ} (A ‘→'’ B)
    → Term {Γ} (B ‘→'’ C)
    → Term {Γ} (A ‘→'’ C)
g ‘∘’ f = ‘λ∙’ (w→ f ‘'’ₐ (w→ g ‘'’ₐ ‘VAR₀’))

WS₀₀W1 : ∀ {Γ T' B A} {b : Term {Γ} B} {a : Term {Γ ▻ B} (W A)} {T : Typ (Γ ▻ A)}
      → Term {Γ ▻ T'} (W (W1 T ‘’ a ‘’ b))
      → Term {Γ ▻ T'} (W (T ‘’ (SW (a ‘t’ b))))
WS₀₀W1 = weakenTyp-substTyp-substTyp-weakenTyp1

WS₀₀W1' : ∀ {Γ T' B A} {b : Term {Γ} B} {a : Term {Γ ▻ B} (W A)} {T : Typ (Γ ▻ A)}
      → Term {Γ ▻ T'} (W (T ‘’ (SW (a ‘t’ b))))
      → Term {Γ ▻ T'} (W (W1 T ‘’ a ‘’ b))
WS₀₀W1' = weakenTyp-substTyp-substTyp-weakenTyp1-inv

substTyp-substTyp-weakenTyp1-inv-arr : ∀ {Γ B A}
         {b : Term {Γ} B}
         {a : Term {Γ ▻ B} (W A)}
         {T : Typ (Γ ▻ A)}
         {X} →
    Term {Γ} (T ‘’ (SW (a ‘t’ b)) ‘→'’ X)
    → Term {Γ} (W1 T ‘’ a ‘’ b ‘→'’ X)
substTyp-substTyp-weakenTyp1-inv-arr x = ‘λ∙’ (w→ x ‘'’ₐ WS₀₀W1 ‘VAR₀’)

S₀₀W1'→ = substTyp-substTyp-weakenTyp1-inv-arr

substTyp-substTyp-weakenTyp1-arr-inv : ∀ {Γ B A}
         {b : Term {Γ} B}
         {a : Term {Γ ▻ B} (W A)}
         {T : Typ (Γ ▻ A)}
         {X} →
    Term {Γ} (X ‘→'’ T ‘’ (SW (a ‘t’ b)))
    → Term {Γ} (X ‘→'’ W1 T ‘’ a ‘’ b)
substTyp-substTyp-weakenTyp1-arr-inv x = ‘λ∙’ (WS₀₀W1' (un‘λ∙’ x))

S₀₀W1'← = substTyp-substTyp-weakenTyp1-arr-inv

substTyp-substTyp-weakenTyp1 : ∀ {Γ B A}
         {b : Term {Γ} B}
         {a : Term {Γ ▻ B} (W A)}
         {T : Typ (Γ ▻ A)} →
    Term {Γ} (W1 T ‘’ a ‘’ b)
    → Term {Γ} (T ‘’ (SW (a ‘t’ b)))
substTyp-substTyp-weakenTyp1 x = (SW (WS₀₀W1 (w x) ‘t’ x))
S₀₀W1 = substTyp-substTyp-weakenTyp1

SW1W : ∀ {Γ T} {A : Typ Γ} {B : Typ Γ}
      → {a : Term {Γ = Γ ▻ T} (W {Γ = Γ} {A = T} B)}
      → Term {Γ = Γ ▻ T} (W1 (W A) ‘’ a)
      → Term {Γ = Γ ▻ T} (W A)
SW1W = substTyp-weakenTyp1-weakenTyp

S₂₀₀W1WW : ∀ {Γ A} {T : Typ (Γ ▻ A)} {T' C B} {a : Term {Γ} A} {b : Term {Γ = (Γ ▻ C ‘’ a)} (B ‘’₁ a)}
         {c : Term {Γ = (Γ ▻ T')} (W (C ‘’ a))}
         → Term {Γ = (Γ ▻ T')} (W1 (W (W T) ‘’₂ a ‘’ b) ‘’ c)
         → Term {Γ = (Γ ▻ T')} (W (T ‘’ a))
S₂₀₀W1WW = substTyp2-substTyp-substTyp-weakenTyp1-weakenTyp-weakenTyp

S₁₀W2W : ∀ {Γ T' A B T} {a : Term {Γ ▻ T'} (W A)} {b : Term {Γ ▻ T'} (W1 B ‘’ a)}
      → Term {Γ ▻ T'} (W2 (W T) ‘’₁ a ‘’ b)
      → Term {Γ ▻ T'} (W1 T ‘’ a)
S₁₀W2W = substTyp1-substTyp-weakenTyp2-weakenTyp

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
module Pi-.AuxLemmas where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Nat.Properties
open import Data.List as L
open import Function using (_∘_)
open import Pi-.Syntax
open import Pi-.Opsem

Lemma₁ : ∀ {A B C D v v' κ κ'} {c : A ↔ B} {c' : C ↔ D}
       → ［ c ∣ v ∣ κ ］◁ ↦ ⟨ c' ∣ v' ∣ κ' ⟩◁
       → A ≡ C × B ≡ D
Lemma₁ ↦⃖₁ = refl , refl
Lemma₁ ↦⃖₂ = refl , refl

Lemma₂ : ∀ {A B v v' κ κ'} {c c' : A ↔ B}
       → ［ c ∣ v ∣ κ ］◁ ↦ ⟨ c' ∣ v' ∣ κ' ⟩◁
       → c ≡ c' × κ ≡ κ'
Lemma₂ ↦⃖₁ = refl , refl
Lemma₂ ↦⃖₂ = refl , refl

Lemma₃ : ∀ {A B v v' κ} {c : A ↔ B}
       → ［ c ∣ v ∣ κ ］◁ ↦ ⟨ c ∣ v' ∣ κ ⟩◁
       → base c ⊎ A ≡ B
Lemma₃ (↦⃖₁ {b = b}) = inj₁ b
Lemma₃ ↦⃖₂ = inj₂ refl

Lemma₄ : ∀ {A v v' κ} {c : A ↔ A}
       → ［ c ∣ v ∣ κ ］◁ ↦ ⟨ c ∣ v' ∣ κ ⟩◁
       → base c ⊎ c ≡ id↔
Lemma₄ (↦⃖₁ {b = b}) = inj₁ b
Lemma₄ ↦⃖₂ = inj₂ refl

Lemma₅ : ∀ {A B C D v v' κ κ'} {c : A ↔ B} {c' : C ↔ D}
       → ［ c ∣ v ∣ κ ］◁ ↦ ［ c' ∣ v' ∣ κ' ］▷
       → A ≡ C × B ≡ D
Lemma₅ ↦η₁ = refl , refl
Lemma₅ ↦η₂ = refl , refl

Lemma₆ : ∀ {A B v v' κ κ'} {c c' : A ↔ B}
       → ［ c ∣ v ∣ κ ］◁ ↦ ［ c' ∣ v' ∣ κ' ］▷
       → c ≡ c' × κ ≡ κ'
Lemma₆ ↦η₁ = refl , refl
Lemma₆ ↦η₂ = refl , refl

Lemma₇ : ∀ {A B v v' κ} {c : A ↔ B}
       → ［ c ∣ v ∣ κ ］◁ ↦ ［ c ∣ v' ∣ κ ］▷
       →  A ≡ 𝟘
Lemma₇ ↦η₁ = refl
Lemma₇ ↦η₂ = refl

Lemma₈ : ∀ {A B C D v v' κ κ'} {c : A ↔ B} {c' : C ↔ D}
           → ⟨ c ∣ v ∣ κ ⟩▷ ↦ ［ c' ∣ v' ∣ κ' ］▷
           → A ≡ C × B ≡ D
Lemma₈ ↦⃗₁ = refl , refl
Lemma₈ ↦⃗₂ = refl , refl

Lemma₉ : ∀ {A B v v' κ κ'} {c c' : A ↔ B}
           → ⟨ c ∣ v ∣ κ ⟩▷ ↦ ［ c' ∣ v' ∣ κ' ］▷
           → c ≡ c' × κ ≡ κ'
Lemma₉ ↦⃗₁ = refl , refl
Lemma₉ ↦⃗₂ = refl , refl

Lemma₁₀ : ∀ {A B v v' κ} {c : A ↔ B}
        → (r : ⟨ c ∣ v ∣ κ ⟩▷ ↦ ［ c ∣ v' ∣ κ ］▷)
        → base c ⊎ A ≡ B
Lemma₁₀ (↦⃗₁ {b = b}) = inj₁ b
Lemma₁₀ ↦⃗₂ = inj₂ refl

Lemma₁₁ : ∀ {A v v' κ} {c : A ↔ A}
       → (r : ⟨ c ∣ v ∣ κ ⟩▷ ↦ ［ c ∣ v' ∣ κ ］▷)
       → base c ⊎ c ≡ id↔
Lemma₁₁ (↦⃗₁ {b = b}) = inj₁ b
Lemma₁₁ ↦⃗₂ = inj₂ refl

ext: agda


text:
module Logic.Classical where

import      Lvl
open import Data
open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.Boolean.Stmt.Proofs using (module IsTrue ; module IsFalse)
open import Data.Boolean.Proofs
open import Data.Either as Either using (_‖_)
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Lang.Instance
open import Logic
open import Logic.Names
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Logic.Predicate
open import Logic.Predicate.Theorems
open import Relator.Equals
open import Syntax.Type
open import Type
open import Type.Properties.Inhabited

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓₒ ℓₒ₁ ℓₒ₂ ℓₒ₃ ℓₗ : Lvl.Level
private variable X Y Z : Type{ℓ}

-- A proposition is behaving classically when excluded middle holds for it.
-- In other words: For the proposition or its negation, if one of them is provable.
-- It could be interpreted as: The proposition is either true or false.
-- In classical logic, this is always the case for any proposition.
-- Note: (∀x. Classical(P(x))) is also called: P is decidable.
module _ (P : Stmt{ℓ}) where
  record Classical : Stmt{ℓ} where -- TODO: Rename to ExcludedMiddle. Define WeakExcludedMiddle = ExcludedMiddle ∘ ¬_ and Classical = ∀ₗ(ExcludedMiddle)
    constructor intro
    field
      ⦃ excluded-middle ⦄ : ExcludedMiddleOn(P)
  excluded-middle = inst-fn Classical.excluded-middle
open Classical ⦃ ... ⦄ hiding (excluded-middle) public

------------------------------------------
-- Classical on predicates.

Classical₁ : (X → Stmt{ℓₗ}) → Stmt
Classical₁(P) = ∀¹(Classical ∘₁ P)

Classical₂ : (X → Y → Stmt{ℓₗ}) → Stmt
Classical₂(P) = ∀²(Classical ∘₂ P)

Classical₃ : (X → Y → Z → Stmt{ℓₗ}) → Stmt
Classical₃(P) = ∀³(Classical ∘₃ P)

------------------------------------------
-- Well-known classical rules.

module _ {P : Stmt{ℓ}} ⦃ classical-P : Classical(P) ⦄ where
  -- Double negation elimination.
  [¬¬]-elim : (¬¬ P) → P
  [¬¬]-elim = [¬¬]-elim-from-excluded-middle (excluded-middle(P))

  -- A double negated proposition is equivalent to the positive.
  double-negation : P ↔ (¬¬ P)
  double-negation = [↔]-intro [¬¬]-elim [¬¬]-intro

  -- The type signature of the "call/cc or "call-with-current-continuation" subroutine in the programming language Scheme.
  -- Also known as: "Peirce's law"
  call-cc-rule : ∀{Q : Stmt{ℓ₂}} → (((P → Q) → P) → P)
  call-cc-rule (pqp) with excluded-middle(P)
  ... | ([∨]-introₗ p ) = p
  ... | ([∨]-introᵣ np) = pqp([⊥]-elim ∘ np)

  -- When the negative implies the positive, thus implying a contradiction, the positive is true.
  -- Also called: "Clavius's Law".
  negative-implies-positive : ((¬ P) → P) → P
  negative-implies-positive npp with excluded-middle(P)
  ... | ([∨]-introₗ p ) = p
  ... | ([∨]-introᵣ np) = npp np

module _ (P : Stmt{ℓ}) ⦃ classical : Classical(P) ⦄ where
  -- Elimination rule for the disjunction in excluded middle.
  excluded-middle-elim : ∀{Q : Stmt{ℓ₂}} → (P → Q) → ((¬ P) → Q) → Q
  excluded-middle-elim pq npq = [∨]-elim pq npq (excluded-middle(P))

------------------------------------------
-- Contraposition rules on implication.

module _ {P : Stmt{ℓ₁}} {Q : Stmt{ℓ₂}} ⦃ classical : Classical(Q) ⦄ where
  -- Contraposition rule in reverse removing negations.
  contrapositiveₗ : (P → Q) ← ((¬ P) ← (¬ Q))
  contrapositiveₗ (npnq) = [¬¬]-elim ∘ (contrapositiveᵣ (npnq)) ∘ [¬¬]-intro

  contrapositive : (P → Q) ↔ ((¬ P) ← (¬ Q))
  contrapositive = [↔]-intro contrapositiveₗ contrapositiveᵣ

  contrapositive-variant2ᵣ : (P ← (¬ Q)) → ((¬ P) → Q)
  contrapositive-variant2ᵣ = [¬¬]-elim ∘₂ (swap _∘_)

module _ {P : Stmt{ℓ₁}} ⦃ classical : Classical(P) ⦄ {Q : Stmt{ℓ₂}} where
  contrapositive-variant2ₗ : ((¬ P) → Q) → (P ← (¬ Q))
  contrapositive-variant2ₗ = contrapositiveₗ ∘ ([¬¬]-intro ∘_)

module _ {P : Stmt{ℓ₁}} ⦃ classic-p : Classical(P) ⦄ {Q : Stmt{ℓ₂}} ⦃ classic-q : Classical(Q) ⦄ where
  contrapositive-variant2 : (P ← (¬ Q)) ↔ ((¬ P) → Q)
  contrapositive-variant2 = [↔]-intro contrapositive-variant2ₗ contrapositive-variant2ᵣ

  one-direction-implication : (P ← Q) ∨ (P → Q)
  one-direction-implication with excluded-middle(P) | excluded-middle(Q)
  one-direction-implication | [∨]-introₗ p  | [∨]-introₗ q  = [∨]-introₗ (const p)
  one-direction-implication | [∨]-introₗ p  | [∨]-introᵣ nq = [∨]-introₗ (const p)
  one-direction-implication | [∨]-introᵣ np | [∨]-introₗ q  = [∨]-introᵣ (const q)
  one-direction-implication | [∨]-introᵣ np | [∨]-introᵣ nq = [∨]-introᵣ ([⊥]-elim ∘ np)

  [¬]-injective : (P ↔ Q) ← ((¬ P) ↔ (¬ Q))
  [¬]-injective ([↔]-intro nqnp npnq) = [↔]-intro (contrapositiveₗ ⦃ classic-p ⦄ npnq) (contrapositiveₗ ⦃ classic-q ⦄ nqnp)

  [↔]-negation : (P ↔ Q) ↔ ((¬ P) ↔ (¬ Q))
  [↔]-negation = [↔]-intro [¬]-injective [¬]-unaryOperator

------------------------------------------
-- XOR.

module _ (P : Stmt{ℓ}) ⦃ classical : Classical(P) ⦄ where
  xor-negation : P ⊕ (¬ P)
  xor-negation with excluded-middle(P)
  ... | [∨]-introₗ p  = [⊕]-introₗ p ([¬¬]-intro p)
  ... | [∨]-introᵣ np = [⊕]-introᵣ np np

module _ {P : Stmt{ℓ₁}} {Q : Stmt{ℓ₂}} where
  classical-from-xorₗ : ⦃ xor : (P ⊕ Q) ⦄ → Classical(P)
  classical-from-xorₗ ⦃ xor ⦄ = intro ⦃ [⊕]-excluded-middleₗ xor ⦄

  classical-from-xorᵣ : ⦃ xor : (P ⊕ Q) ⦄ → Classical(Q)
  classical-from-xorᵣ ⦃ xor ⦄ = intro ⦃ [⊕]-excluded-middleᵣ xor ⦄

------------------------------------------
-- Introduction/elimination rules for Classical when combined with logical connectives.

module _ {P : Stmt{ℓ}} where
  [¬]-classical-intro : ⦃ classical : Classical(P) ⦄ → Classical(¬ P)
  [¬]-classical-intro ⦃ classical-p ⦄ = intro ⦃ proof ⦄ where
    proof : (¬ P) ∨ (¬¬ P)
    proof = Either.swap(Either.mapLeft [¬¬]-intro (excluded-middle(P)))

  excluded-middle-classical-intro : ⦃ _ : Classical(P) ⦄ → Classical(P ∨ (¬ P))
  excluded-middle-classical-intro = intro ⦃ [∨]-introₗ (excluded-middle(P)) ⦄

  -- [¬]-classical-elim : ⦃ _ : Classical(¬ P) ⦄ → Classical(P)
  -- [¬]-classical-elim ⦃ classical ⦄ = intro ⦃ excluded-middle-elim(¬ P) ⦃ classical ⦄ [∨]-introᵣ (nnp ↦ [∨]-introₗ {!!}) ⦄

module _ {P : Stmt{ℓ₁}} {Q : Stmt{ℓ₂}} where
  classical-by-equivalence : (P ↔ Q) → (Classical(P) ↔ Classical(Q))
  classical-by-equivalence (xy) = [↔]-intro (cy ↦ intro ⦃ proofₗ(cy) ⦄) (cx ↦ intro ⦃ proofᵣ(cx) ⦄) where
    proofᵣ : Classical(P) → (Q ∨ (¬ Q))
    proofᵣ (classical-p) with excluded-middle(P) ⦃ classical-p ⦄
    ... | [∨]-introₗ(p)  = [∨]-introₗ([↔]-to-[→] xy p)
    ... | [∨]-introᵣ(nx) = [∨]-introᵣ(nx ∘ ([↔]-to-[←] xy))

    proofₗ : Classical(Q) → (P ∨ (¬ P))
    proofₗ (classical-q) with excluded-middle(Q) ⦃ classical-q ⦄
    ... | [∨]-introₗ(q)  = [∨]-introₗ([↔]-to-[←] xy q)
    ... | [∨]-introᵣ(ny) = [∨]-introᵣ(ny ∘ ([↔]-to-[→] xy))

  instance
    [∧]-classical-intro : ⦃ classical-p : Classical(P) ⦄ → ⦃ classical-q : Classical(Q) ⦄ → Classical(P ∧ Q)
    [∧]-classical-intro ⦃ classical-p ⦄ ⦃ classical-q ⦄ = intro ⦃ proof ⦄ where
      proof : (P ∧ Q) ∨ (¬ (P ∧ Q))
      proof with (excluded-middle(P) , excluded-middle(Q))
      ... | ([∨]-introₗ(p)  , [∨]-introₗ(q))  = [∨]-introₗ([∧]-intro(p)(q))
      ... | ([∨]-introₗ(p)  , [∨]-introᵣ(ny)) = [∨]-introᵣ(xy ↦ ny([∧]-elimᵣ(xy)))
      ... | ([∨]-introᵣ(nx) , [∨]-introₗ(q))  = [∨]-introᵣ(xy ↦ nx([∧]-elimₗ(xy)))
      ... | ([∨]-introᵣ(nx) , [∨]-introᵣ(ny)) = [∨]-introᵣ(xy ↦ nx([∧]-elimₗ(xy)))

  instance
    [∨]-classical-intro : ⦃ classical-p : Classical(P) ⦄ → ⦃ classical-q : Classical(Q) ⦄ → Classical(P ∨ Q)
    [∨]-classical-intro ⦃ classical-p ⦄ ⦃ classical-q ⦄ = intro ⦃ proof ⦄ where
      proof : (P ∨ Q) ∨ (¬ (P ∨ Q))
      proof with (excluded-middle(P) , excluded-middle(Q))
      ... | ([∨]-introₗ(p)  , [∨]-introₗ(q))  = [∨]-introₗ([∨]-introₗ(p))
      ... | ([∨]-introₗ(p)  , [∨]-introᵣ(ny)) = [∨]-introₗ([∨]-introₗ(p))
      ... | ([∨]-introᵣ(nx) , [∨]-introₗ(q))  = [∨]-introₗ([∨]-introᵣ(q))
      ... | ([∨]-introᵣ(nx) , [∨]-introᵣ(ny)) = [∨]-introᵣ(xy ↦ [∨]-elim(nx)(ny) (xy))

  instance
    [→]-classical-intro : ⦃ classical-p : Classical(P) ⦄ → ⦃ classical-q : Classical(Q) ⦄ → Classical(P → Q)
    [→]-classical-intro ⦃ classical-p ⦄ ⦃ classical-q ⦄ = intro ⦃ proof ⦄ where
      proof : (P → Q) ∨ (¬ (P → Q))
      proof with (excluded-middle(P) , excluded-middle(Q))
      ... | ([∨]-introₗ(p)  , [∨]-introₗ(q))  = [∨]-introₗ(const(q))
      ... | ([∨]-introₗ(p)  , [∨]-introᵣ(ny)) = [∨]-introᵣ([¬→][∧]ₗ ([∧]-intro p ny))
      ... | ([∨]-introᵣ(nx) , [∨]-introₗ(q))  = [∨]-introₗ(const(q))
      ... | ([∨]-introᵣ(nx) , [∨]-introᵣ(ny)) = [∨]-introₗ([⊥]-elim ∘ nx)

  instance
    [↔]-classical-intro : ⦃ _ : Classical(P) ⦄ → ⦃ _ : Classical(Q) ⦄ → Classical(P ↔ Q)
    [↔]-classical-intro ⦃ classical-p ⦄ ⦃ classical-q ⦄ = intro ⦃ proof ⦄ where
      proof : (P ↔ Q) ∨ (¬ (P ↔ Q))
      proof with (excluded-middle(P) , excluded-middle(Q))
      ... | ([∨]-introₗ(p)  , [∨]-introₗ(q))  = [∨]-introₗ([↔]-intro (const(p)) (const(q)))
      ... | ([∨]-introₗ(p)  , [∨]-introᵣ(ny)) = [∨]-introᵣ(([¬→][∧]ₗ ([∧]-intro p ny)) ∘ [↔]-to-[→])
      ... | ([∨]-introᵣ(nx) , [∨]-introₗ(q))  = [∨]-introᵣ(([¬→][∧]ₗ ([∧]-intro q nx)) ∘ [↔]-to-[←])
      ... | ([∨]-introᵣ(nx) , [∨]-introᵣ(ny)) = [∨]-introₗ([↔]-intro ([⊥]-elim ∘ ny) ([⊥]-elim ∘ nx))

instance
  [⊤]-classical-intro : Classical(⊤)
  [⊤]-classical-intro = intro ⦃ [∨]-introₗ ([⊤]-intro) ⦄

instance
  [⊥]-classical-intro : Classical(⊥)
  [⊥]-classical-intro = intro ⦃ [∨]-introᵣ (id) ⦄

module _ {X : Type{ℓ₁}} ⦃ _ : (◊ X) ⦄ {P : X → Stmt{ℓ₂}} where
  instance
    [∃]-classical-elim : ⦃ _ : Classical(∃ P) ⦄ → ∃(x ↦ Classical(P(x)))
    [∃]-classical-elim ⦃ classical-expx ⦄ with excluded-middle(∃ P)
    ... | [∨]-introₗ(expx)  = [∃]-intro([∃]-witness(expx)) ⦃ intro ⦃ [∨]-introₗ([∃]-proof(expx)) ⦄ ⦄
    ... | [∨]-introᵣ(nexpx) = [∃]-intro([◊]-existence) ⦃ intro ⦃ [∨]-introᵣ([¬∃]-to-[∀¬] (nexpx) {[◊]-existence}) ⦄ ⦄

------------------------------------------
-- ???

module _ {P : Stmt{ℓ}} {Q : Stmt{ℓ₂}} ⦃ classical-Q : Classical(Q) ⦄ where
  -- One direction of the equivalence of implication using conjunction
  [→][∧]ₗ : (P → Q) ← ¬(P ∧ (¬ Q))
  [→][∧]ₗ (nqnp) = [¬¬]-elim ∘ (Tuple.curry(nqnp))
    -- ¬(A ∧ ¬B) → (A → ¬¬B)
    --   ¬(A ∧ (¬ B)) //assumption
    --   ((A ∧ (B → ⊥)) → ⊥) //Definition: (¬)
    --   (A → (B → ⊥) → ⊥) //Tuple.curry
    --   (A → ¬(B → ⊥)) //Definition: (¬)
    --   (A → ¬(¬ B)) //Definition: (¬)

  [→][∧] : (P → Q) ↔ ¬(P ∧ (¬ Q))
  [→][∧] = [↔]-intro [→][∧]ₗ [→][∧]ᵣ

module _ {P : Stmt{ℓ}} ⦃ classical-P : Classical(P) ⦄ where
  -- One direction of the equivalence of implication using disjunction
  [→]-disjunctive-formᵣ : ∀{Q : Stmt{ℓ₂}} → (P → Q) → ((¬ P) ∨ Q)
  [→]-disjunctive-formᵣ (pq) with excluded-middle(P)
  ... | [∨]-introₗ(p)  = [∨]-introᵣ(pq(p))
  ... | [∨]-introᵣ(np) = [∨]-introₗ(np)

  [→]-disjunctive-form : ∀{Q : Stmt{ℓ₂}} → (P → Q) ↔ ((¬ P) ∨ Q)
  [→]-disjunctive-form = [↔]-intro [→]-disjunctive-formₗ [→]-disjunctive-formᵣ

  [→]-from-contrary : ∀{Q : Stmt{ℓ₂}} → (Q → (¬ P) → ⊥) → (Q → P)
  [→]-from-contrary = [¬¬]-elim ∘_

  [¬→]-disjunctive-formᵣ : ∀{Q : Stmt{ℓ₂}} → ((¬ P) → Q) → (P ∨ Q)
  [¬→]-disjunctive-formᵣ npq = excluded-middle-elim P [∨]-introₗ ([∨]-introᵣ ∘ npq)

  [¬→]-disjunctive-form : ∀{Q : Stmt{ℓ₂}} → ((¬ P) → Q) ↔ (P ∨ Q)
  [¬→]-disjunctive-form = [↔]-intro [¬→]-disjunctive-formₗ [¬→]-disjunctive-formᵣ

  -- [↔]-disjunctive-form : ∀{Q : Stmt{ℓ₂}} → (P ↔ Q) ↔ (P ∧ Q) ∨ ((¬ P) ∧ (¬ Q))
  -- [↔]-disjunctive-form = [↔]-intro [↔]-disjunctive-formₗ ?

  module _ {Q : Stmt{ℓ₂}} {R : Stmt{ℓ₃}} where
    [→][∨]-distributivityₗ : (P → (Q ∨ R)) ↔ ((P → Q) ∨ (P → R))
    [→][∨]-distributivityₗ = [↔]-intro [→][∨]-distributivityₗₗ r where
      r : (P → (Q ∨ R)) → ((P → Q) ∨ (P → R))
      r pqr = excluded-middle-elim P ([∨]-elim2 const const ∘ pqr) ([∨]-introₗ ∘ ([⊥]-elim ∘_))

module _ {P : Stmt{ℓ₁}} ⦃ classic-p : Classical(P) ⦄ {Q : Stmt{ℓ₂}} ⦃ classic-q : Classical(Q) ⦄ where
  [¬→][∧]ᵣ : ¬(P → Q) → (P ∧ (¬ Q))
  [¬→][∧]ᵣ = contrapositive-variant2ₗ ⦃ [∧]-classical-intro {P = P}{Q = ¬ Q} ⦃ classical-q = [¬]-classical-intro ⦄ ⦄ ([→][∧]ₗ {Q = Q})

  [¬→][∧] : ¬(P → Q) ↔ (P ∧ (¬ Q))
  [¬→][∧] = [↔]-intro [¬→][∧]ₗ [¬→][∧]ᵣ

classical-topOrBottom : ∀{P : Stmt{ℓ}} → (Classical(P) ↔ TopOrBottom(_↔_)(P))
_⨯_.left  (classical-topOrBottom {P = P}) tb        = intro ⦃ [∨]-elim2 ([↔]-elimₗ [⊤]-intro) [↔]-to-[→] tb ⦄
_⨯_.right (classical-topOrBottom {P = P}) classical = excluded-middle-elim P ⦃ classical ⦄ ([∨]-introₗ ∘ provable-top-equivalence) (([∨]-introᵣ ∘ unprovable-bottom-equivalence))

------------------------------------------
-- Negation is almost preserved over the conjunction-dijunction dual (De-morgan's laws).

module _ {P : Stmt{ℓ₁}} ⦃ classic-p : Classical(P) ⦄ {Q : Stmt{ℓ₂}} ⦃ classic-q : Classical(Q) ⦄ where
  [¬]-preserves-[∧][∨]ᵣ : ¬(P ∧ Q) → ((¬ P) ∨ (¬ Q))
  [¬]-preserves-[∧][∨]ᵣ npq = [→]-disjunctive-formᵣ {P = P} {Q = ¬ Q} ([→][∧]ₗ ⦃ [¬]-classical-intro ⦄ (npq ∘ (Tuple.mapRight ([¬¬]-elim {P = Q}))))

  [¬]-preserves-[∧][∨] : ¬(P ∧ Q) ↔ ((¬ P) ∨ (¬ Q))
  [¬]-preserves-[∧][∨] = [↔]-intro [¬]-preserves-[∧][∨]ₗ [¬]-preserves-[∧][∨]ᵣ

{- TODO: Organize Logic.Classical.DoubleNegated, and this is already proven in there, though this result is more general.
module _ {P : Stmt{ℓ₁}} {Q : Stmt{ℓ₂}} where
  [¬]-preserves-[∧][∨]ᵣ-weak-excluded-middle : (¬(P ∧ Q) → ((¬ P) ∨ (¬ Q))) ← (Classical(¬ P) ∧ Classical(¬ Q))
  [¬]-preserves-[∧][∨]ᵣ-weak-excluded-middle ([↔]-intro (intro ⦃ pex ⦄) (intro ⦃ qex ⦄)) npq with pex | qex
  ... | [∨]-introₗ np  | [∨]-introₗ nq  = [∨]-introₗ np
  ... | [∨]-introₗ np  | [∨]-introᵣ nnq = [∨]-introₗ np
  ... | [∨]-introᵣ nnp | [∨]-introₗ nq  = [∨]-introᵣ nq
  ... | [∨]-introᵣ nnp | [∨]-introᵣ nnq with () ← (DoubleNegated.[∧]-intro nnp nnq) npq
-}

-- TODO: See TODO directly above
weak-excluded-middle-[¬]-preserves-[∧][∨]ᵣ : (∀{P : Stmt{ℓ}} → Classical(¬ P)) ↔ (∀{P : Stmt{ℓ}}{Q : Stmt{ℓ}} → ¬(P ∧ Q) → ((¬ P) ∨ (¬ Q)))
weak-excluded-middle-[¬]-preserves-[∧][∨]ᵣ = [↔]-intro l r where
  l : (∀{P} → Classical(¬ P)) ← (∀{P}{Q} → ¬(P ∧ Q) → ((¬ P) ∨ (¬ Q)))
  l pres {P} = intro ⦃ pres{P}{¬ P} non-contradiction ⦄
  r : (∀{P} → Classical(¬ P)) → (∀{P}{Q} → ¬(P ∧ Q) → ((¬ P) ∨ (¬ Q)))
  r wem {P}{Q} npq with excluded-middle(¬ P) ⦃ wem ⦄ | excluded-middle(¬ Q) ⦃ wem ⦄
  ... | [∨]-introₗ np  | [∨]-introₗ nq  = [∨]-introₗ np
  ... | [∨]-introₗ np  | [∨]-introᵣ nnq = [∨]-introₗ np
  ... | [∨]-introᵣ nnp | [∨]-introₗ nq  = [∨]-introᵣ nq
  ... | [∨]-introᵣ nnp | [∨]-introᵣ nnq = [∨]-introₗ (p ↦ nnq(q ↦ npq([∧]-intro p q)))

------------------------------------------
-- Predicate logic.

module _ {P : Stmt{ℓ}} ⦃ classical-P : Classical(P) ⦄ {X : Type{ℓ₂}} ⦃ pos@(intro ⦃ x ⦄) : (◊ X) ⦄ {Q : X → Stmt{ℓ₃}} where
  [∃]-unrelatedᵣ-[→]ₗ : ∃(x ↦ (P → Q(x))) ← (P → ∃(x ↦ Q(x)))
  [∃]-unrelatedᵣ-[→]ₗ pexqx with excluded-middle(P)
  ... | ([∨]-introₗ p)  = [∃]-map-proof (const) (pexqx(p))
  ... | ([∨]-introᵣ np) = [∃]-intro(x) ⦃ [⊥]-elim {P = Q(x)} ∘ np ⦄

  [∃]-unrelatedᵣ-[→] : ∃(x ↦ (P → Q(x))) ↔ (P → ∃(x ↦ Q(x)))
  [∃]-unrelatedᵣ-[→] = [↔]-intro [∃]-unrelatedᵣ-[→]ₗ [∃]-unrelatedᵣ-[→]ᵣ

module _ {X : Type{ℓ₁}} ⦃ _ : (◊ X) ⦄ {P : X → Stmt{ℓ₂}} ⦃ classical-expx : Classical(∃ P) ⦄ {Q : X → Stmt{ℓ₃}} where
  [∃][←]-distributivity : ∃(x ↦ (P(x) → Q(x))) ← (∃(x ↦ P(x)) → ∃(x ↦ Q(x)))
  [∃][←]-distributivity (expx-exqx) =
      (([∃]-map-proof (\{x} → proof ↦ proof{x})
        (([∃]-map-proof (\{x} → [↔]-to-[←] ([∀]-unrelatedₗ-[→] {X = X}{P}{Q(x)}))
          (([∃]-unrelatedᵣ-[→]ₗ ⦃ classical-expx ⦄
            (expx-exqx :of: (∃(x ↦ P(x)) → ∃(x ↦ Q(x))))
          )            :of: (∃(x ↦ (∃(x ↦ P(x)) → Q(x)))))
        )              :of: (∃(x ↦ ∀ₗ(y ↦ (P(y) → Q(x))))))
      )                :of: (∃(x ↦ (P(x) → Q(x)))))

{-
module _ {X : Type{ℓ₁}} ⦃ _ : (◊ X) ⦄ {P : X → Stmt{ℓ₂}} where
  [¬∀¬]-to-[∃] : (∃ P) ← ¬(∀ₗ(¬_ ∘ P))
  [¬∀¬]-to-[∃] x = {!!} -- TODO: When is this true?

  [∃]-classical-intro : ⦃ _ : Classical(∀ₗ P) ⦄ ⦃ _ : Classical(∀ₗ(¬_ ∘ P)) ⦄ → Classical(∃ P)
  Classical.excluded-middle ([∃]-classical-intro ⦃ classical-pa ⦄ ⦃ classical-npa ⦄) with excluded-middle(∀ₗ P) | excluded-middle(∀ₗ(¬_ ∘ P))
  ... | [∨]-introₗ ap  | [∨]-introₗ nap  with () ← nap(ap {[◊]-existence})
  ... | [∨]-introₗ ap  | [∨]-introᵣ nanp = [∨]-introₗ ([∃]-intro [◊]-existence ⦃ ap ⦄)
  ... | [∨]-introᵣ npa | [∨]-introₗ nap  = [∨]-introᵣ ([∀¬]-to-[¬∃] nap)
  ... | [∨]-introᵣ npa | [∨]-introᵣ nanp = [∨]-introₗ ([¬∀¬]-to-[∃] nanp)
-}

-- TODO: Maybe try to get rid of the second instance assumption? Idea: Only [¬¬]-elim is needed for that one, so if possible and true, prove: (∀{x} → Classic(P(x)) → P(x)) → (Classic(∃ P) → (∃ P)). No, that is probably not true
module _ {X : Type{ℓ₁}}{P : X → Stmt{ℓ₂}} ⦃ classical-proof1 : ∀{x} → Classical(P(x)) ⦄ ⦃ classical-proof2 : Classical(∃(¬_ ∘ P)) ⦄ where
  [¬∀]-to-[∃¬] : ∃(x ↦ ¬(P(x))) ← ¬(∀ₗ(x ↦ P(x)))
  [¬∀]-to-[∃¬] (naxpx) =
    ([¬¬]-elim ⦃ classical-proof2 ⦄
      ([¬]-intro {P = ¬ ∃(x ↦ ¬(P(x)))} (nexnpx ↦
        (naxpx
          ([∀][→]-distributivity {X = X}{¬¬_ ∘ P}
            ((\{x} → [¬¬]-elim ⦃ classical-proof1{x} ⦄) :of: ∀ₗ(x ↦ (¬¬ P(x) → P(x))))
            ([¬∃]-to-[∀¬] (nexnpx)                      :of: ∀ₗ(x ↦ ¬¬ P(x)))
          :of: ∀ₗ(x ↦ P(x)))
        ) :of: ⊥
      ) :of: (¬¬ ∃(x ↦ ¬ P(x))))
    ) :of: ∃(x ↦ ¬ P(x))
    -- ¬∀x. P(x)
    -- • ¬∃x. ¬P(x)
    --   ¬∃x. ¬P(x)
    --   ⇒ ∀x. ¬¬P(x)
    --   ⇒ ∀x. P(x)
    --   ⇒ ⊥
    -- ⇒ ¬¬∃x. ¬P(x)
    -- ⇒ ∃x. ¬P(x)

  [∃]-unrelatedₗ-[→]ₗ : ⦃ _ : ◊ X ⦄ → ⦃ _ : Classical(∀ₗ P) ⦄ → ∀{Q : Stmt{ℓ₃}} → ∃(x ↦ (P(x) → Q)) ← (∀ₗ(x ↦ P(x)) → Q)
  [∃]-unrelatedₗ-[→]ₗ ⦃ pos-x ⦄ ⦃ classical-axpx ⦄ {Q} axpxq with excluded-middle(∀ₗ P)
  ... | ([∨]-introₗ axpx)  = [∃]-intro([◊]-existence) ⦃ const(axpxq (axpx)) ⦄
  ... | ([∨]-introᵣ naxpx) = [∃]-map-proof ([⊥]-elim ∘_) ([¬∀]-to-[∃¬] (naxpx))
  -- (∀x. P(x)) → Q
  -- • ∀x. P(x)
  --   ∀x. P(x)
  --   ⇒ ∀x. P(x)
  --   ⇒ Q
  --   ⇒ P(a) → Q
  --   ⇒ ∃x. P(x) → Q
  -- • ¬∀x. P(x)
  --   ¬∀x. P(x)
  --   ⇒ ∃x. ¬P(x)
  --   ⇒ ∃x. P(x) → Q

  -- Also known as: Drinker paradox
  drinker-ambiguity : ⦃ _ : ◊ X ⦄ → ⦃ _ : Classical(∀ₗ P) ⦄ → ∃(x ↦ (P(x) → ∀{y} → P(y)))
  drinker-ambiguity = [∃]-map-proof (\pxap px {y} → pxap px {y}) ([∃]-unrelatedₗ-[→]ₗ id)

  drinker-ambiguity-equiv : ⦃ _ : Classical(∀ₗ P) ⦄ → ((◊ X) ↔ ∃(x ↦ (P(x) → ∀{y} → P(y))))
  drinker-ambiguity-equiv ⦃ classical-axpx ⦄ =
    [↔]-intro
      (\ex → intro ⦃ [∃]-witness ex ⦄)
      (\pos-x → drinker-ambiguity ⦃ pos-x ⦄ ⦃ classical-axpx ⦄)

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 SignedBy where

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

-- this is easy to write
--- but ignoring for now
postulate  Word512 : Set

{-
signed by val with noncing by identity ==
really needs to be part of a freshly generated challenge /uuid string mixed into the response to
ensure it can be MIM'd and rerouted to unrelated transactions

a related issue is making sure the signeatures at values and on the overall module/transaction unit are
'entangled' together so that manipulations wont validate

for manny applications it'd suffice to just do a signed by of a module/program as a whole
-}
postulate  signed_nonced_by_ : {a : Set} -> a -> Word512 -> String -> Set
postulate  canonicalHash : {a : Set} -> a -> Word512
postulate canonicalNoncedHash : { a : Set} -> a -> Word512 -> Word512

postulate getSignedVal : {a : Set} ->  {nonce : Word512 } { sig : String } {v : a} (sigVal : signed v nonced  nonce by  sig ) -> a
postulate getSignedValEta :  {a : Set}  {v : a} { n : Word512} {i : String} ->  (x : signed v nonced n by i ) -> ( v ≡  getSignedVal x )

{-

-}

max_stars_repo_name: hopper-lang/hopper

max_issues_repo_name: hopper-lang/hopper

max_forks_repo_name: hopper-lang/hopper


text:
-- Andreas, 2014-10-09, issue reported by Matteo Acerbi

module _ where

module A where

module B (let module F = A) where

module C (let module F = A) where
-- Complains about duplicate F

-- Should work

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2012-05-04 Example from Jason Reed, LFMTP 2009
{-# OPTIONS --allow-unsolved-metas #-}
-- The option is supplied to force a real error to pass the regression test.
module JasonReedPruning where

open import Common.Equality
open import Common.Product

data o : Set where
  f : o -> o

test :
  let U : o → o
      U = _
      V : o → o
      V = _
      W : o → o
      W = _
  in (x y : o) → U x ≡ f (V (W y))
               × V x ≡ U (W y)
test x y = refl , refl
{-
  Considering  U (W y) = V x, we can prune x from V

    V x = V'

  After instantiation

    U x = f V'       (solved)
    V'  = U (W y)    (not solved)

    U  = \ x → f V'
    V' = f V'
    occurs check fails
-}

max_stars_repo_name: dagit/agda

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


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

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

module Decidable.Relations where

DecidableRelation : {a b : _} {A : Set a} (f : A → Set b) → Set (a ⊔ b)
DecidableRelation {A = A} f = (x : A) → (f x) || (f x → False)

orDecidable : {a b c : _} {A : Set a} {f : A → Set b} {g : A → Set c} → DecidableRelation f → DecidableRelation g → DecidableRelation (λ x → (f x) || (g x))
orDecidable fDec gDec x with fDec x
orDecidable fDec gDec x | inl fx = inl (inl fx)
orDecidable fDec gDec x | inr !fx with gDec x
orDecidable fDec gDec x | inr !fx | inl gx = inl (inr gx)
orDecidable {f = f} {g} fDec gDec x | inr !fx | inr !gx = inr t
  where
    t : (f x || g x) → False
    t (inl x) = !fx x
    t (inr x) = !gx x

andDecidable : {a b c : _} {A : Set a} {f : A → Set b} {g : A → Set c} → DecidableRelation f → DecidableRelation g → DecidableRelation (λ x → (f x) && (g x))
andDecidable fDec gDec x with fDec x
andDecidable fDec gDec x | inl fx with gDec x
andDecidable fDec gDec x | inl fx | inl gx = inl (fx ,, gx)
andDecidable fDec gDec x | inl fx | inr !gx = inr (λ x → !gx (_&&_.snd x))
andDecidable fDec gDec x | inr !fx = inr (λ x → !fx (_&&_.fst x))

notDecidable : {a b : _} {A : Set a} {f : A → Set b} → DecidableRelation f → DecidableRelation (λ x → (f x) → False)
notDecidable fDec x with fDec x
notDecidable fDec x | inl fx = inr (λ x → x fx)
notDecidable fDec x | inr !fx = inl !fx

doubleNegation : {a b : _} {A : Set a} {f : A → Set b} → DecidableRelation f → (x : A) → (((f x) → False) → False) → f x
doubleNegation fDec x with fDec x
doubleNegation fDec x | inl fx = λ _ → fx
doubleNegation fDec x | inr !fx = λ p → exFalso (p !fx)


text:
-- 2013-06-15 Andreas, issue reported by Stevan Andjelkovic
module Issue854 where

infixr 1 _⊎_
infixr 2 _×_
infixr 4 _,_
infix 4 _≡_

data ⊥ : Set where

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

record ⊤ : Set where
  constructor tt

data Bool : Set where
  true false : Bool

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

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

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

data _⊎_ (A : Set) (B : Set) : Set where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

[_,_] : ∀ {A : Set} {B : Set} {C : A ⊎ B → Set} →
        ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
        ((x : A ⊎ B) → C x)
[ f , g ] (inj₁ x) = f x
[ f , g ] (inj₂ y) = g y

[_,_]₁ : ∀ {A : Set} {B : Set} {C : A ⊎ B → Set₁} →
        ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
        ((x : A ⊎ B) → C x)
[ f , g ]₁ (inj₁ x) = f x
[ f , g ]₁ (inj₂ y) = g y

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

open Σ public

_×_ : Set → Set → Set
A × B = Σ A λ _ → B

uncurry₁ : {A : Set} {B : A → Set} {C : Σ A B → Set₁} →
          ((x : A) → (y : B x) → C (x , y)) →
          ((p : Σ A B) → C p)
uncurry₁ f (x , y) = f x y

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

infix 5 _◃_
infixr 1 _⊎C_
infixr 2 _×C_

record Container : Set₁ where
  constructor _◃_
  field
    Shape     : Set
    Position  : Shape → Set

open Container public

⟦_⟧ : Container → (Set → Set)
⟦ S ◃ P ⟧ X = Σ S λ s → P s → X

idC : Container
idC = ⊤ ◃ λ _ → ⊤

constC : Set → Container
constC X = X ◃ λ _ → ⊥

𝟘 = constC ⊥
𝟙 = constC ⊤

_⊎C_ : Container → Container → Container
S ◃ P ⊎C S′ ◃ P′ = (S ⊎ S′) ◃ [ P , P′ ]₁

_×C_ : Container → Container → Container
S ◃ P ×C S′ ◃ P′ = (S × S′) ◃ uncurry₁ (λ s s′ → P s ⊎ P′ s′)

data μ (C : Container) : Set where
  ⟨_⟩ : ⟦ C ⟧ (μ C) → μ C

_⋆C_ : Container → Set → Container
C ⋆C X = constC X ⊎C C

_⋆_ : Container → Set → Set
C ⋆ X = μ (C ⋆C X)

AlgIter : Container → Set → Set
AlgIter C X = ⟦ C ⟧ X → X

iter : ∀ {C X} → AlgIter C X → μ C → X
iter φ ⟨ s , k ⟩ = φ (s , λ p → iter φ (k p))

AlgRec : Container → Set → Set
AlgRec C X = ⟦ C ⟧ (μ C × X) → X

rec : ∀ {C X} → AlgRec C X → μ C → X
rec φ ⟨ s , k ⟩ = φ (s , λ p → (k p , rec φ (k p)))

return : ∀ {C X} → X → C ⋆ X
return x = ⟨ inj₁ x , ⊥-elim ⟩

do : ∀ {C X} → ⟦ C ⟧ (C ⋆ X) → C ⋆ X
do (s , k) = ⟨ inj₂ s , k ⟩

_>>=_ : ∀ {C X Y} → C ⋆ X → (X → C ⋆ Y) → C ⋆ Y
_>>=_ {C}{X}{Y} m k = iter φ m
  where
  φ : AlgIter (C ⋆C X) (C ⋆ Y)
  φ (inj₁ x  , _)  = k x
  φ (inj₂ s  , k)  = do (s , k)

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

_↠_ : Set → Set → Container
I ↠ O = I ◃ λ _ → O

State : Set → Container
State S  =   (⊤ ↠ S)   -- get
         ⊎C  (S ↠ ⊤)   -- put

get : ∀ {S} → State S ⋆ S
get = do (inj₁ tt , return)

put : ∀ {S} → S → State S ⋆ ⊤
put s = do (inj₂ s , return)

Homo : Container → Set → Set → Container → Set → Set
Homo Σ X I Σ′ Y = AlgRec (Σ ⋆C X) (I → Σ′ ⋆ Y)

Pseudohomo : Container → Set → Set → Container → Set → Set
Pseudohomo Σ X I Σ′ Y =
    ⟦ Σ ⋆C X ⟧ (((Σ ⊎C Σ′) ⋆ X) × (I → Σ′ ⋆ Y)) → I → Σ′ ⋆ Y

state : ∀ {Σ S X} → Pseudohomo (State S) X S Σ (X × S)
state (inj₁ x         , _)  = λ s  → return (x , s)  -- return
state (inj₂ (inj₁ _)  , k)  = λ s  → proj₂ (k s) s   -- get
state (inj₂ (inj₂ s)  , k)  = λ _  → proj₂ (k tt) s  -- put

Abort : Container
Abort = ⊤ ↠ ⊥

aborting : ∀ {X} → Abort ⋆ X
aborting = do (tt , ⊥-elim)

abort : ∀ {Σ X} → Pseudohomo Abort X ⊤ Σ (Maybe X)
abort (inj₁ x  , _) _ = return (just x)  -- return
abort (inj₂ _  , _) _ = return nothing   -- abort

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

record _⇒_ (C C′ : Container) : Set where
  field
    shape    : Shape C → Shape C′
    position : ∀ {s} → Position C′ (shape s) → Position C s

open _⇒_ public

idMorph : ∀ {C} → C ⇒ C
idMorph = record { shape = λ s → s; position = λ p → p }

inlMorph : ∀ {C C′ : Container} → C ⇒ (C ⊎C C′)
inlMorph = record
  { shape    = inj₁
  ; position = λ p → p
  }

swapMorph : ∀ {C C′} → (C ⊎C C′) ⇒ (C′ ⊎C C)
swapMorph {C}{C′}= record
  { shape    = sh
  ; position = λ {s} p → pos {s} p
  }
  where
  sh : Shape C ⊎ Shape C′ → Shape C′ ⊎ Shape C
  sh (inj₁ s)  = inj₂ s
  sh (inj₂ s′) = inj₁ s′

  pos : ∀ {s} → Position (C′ ⊎C C) (sh s) → Position (C ⊎C C′) s
  pos {inj₁ s}  p  = p
  pos {inj₂ s′} p′ = p′

⟪_⟫ : ∀ {C C′ X} → C ⇒ C′ → ⟦ C ⟧ X → ⟦ C′ ⟧ X
⟪ m ⟫ xs = shape m (proj₁ xs) , λ p′ → proj₂ xs (position m p′)

⟪_⟫Homo : ∀ {C C′ X} → C ⇒ C′ → Homo C X ⊤ C′ X
⟪ m ⟫Homo (inj₁ x , _)  _ = return x
⟪ m ⟫Homo (inj₂ s , k)  _ =  let (s′ , k′) = ⟪ m ⟫ (s , k)
                             in  do (s′ , λ p′ → proj₂ (k′ p′) tt)

natural : ∀ {C C′ X} → C ⇒ C′ → C ⋆ X → C′ ⋆ X
natural f m = rec ⟪ f ⟫Homo m tt

inl : ∀ {C C′ X} → C ⋆ X → (C ⊎C C′) ⋆ X
inl = natural inlMorph

squeeze : ∀ {Σ Σ′ X} → ((Σ ⊎C Σ′) ⊎C Σ′) ⋆ X → (Σ ⊎C Σ′) ⋆ X
squeeze = natural m
  where
  m = record
    { shape    = [ (λ x → x) , inj₂ ]
    ; position = λ { {inj₁ x} p → p ; {inj₂ x} p → p}
    }

lift : ∀ {Σ Σ′ X Y I} → Pseudohomo Σ X I Σ′ Y →
         Pseudohomo (Σ ⊎C Σ′) X I Σ′ Y
lift φ (inj₁ x , _)          i = φ (inj₁ x , ⊥-elim) i
lift φ (inj₂ (inj₁ s) , k)   i = φ (inj₂ s , λ p →
                                     let (w , ih) = k p in squeeze w , ih) i
lift φ (inj₂ (inj₂ s′) , k′) i = do (s′ , λ p′ → proj₂ (k′ p′) i)

weaken : ∀ {Σ Σ′ Σ″ Σ‴ X Y I} → Homo Σ′ X I Σ″ Y →
           Σ ⇒ Σ′ → Σ″ ⇒ Σ‴ → Homo Σ X I Σ‴ Y
weaken {Σ}{Σ′}{Σ″}{Σ‴}{X}{Y} φ f g (s , k) i = w‴
  where
  w : Σ ⋆ X
  w = ⟨ s , (λ p → proj₁ (k p)) ⟩

  w′ : Σ′ ⋆ X
  w′ = natural f w

  w″ : Σ″ ⋆ Y
  w″ = rec φ w′ i

  w‴ : Σ‴ ⋆ Y
  w‴ = natural g w″

⌈_⌉Homo : ∀ {Σ Σ′ X Y I} → Pseudohomo Σ X I Σ′ Y → Homo Σ X I Σ′ Y
⌈ φ ⌉Homo (inj₁ x , _)  = φ (inj₁ x , ⊥-elim)
⌈ φ ⌉Homo (inj₂ s , k)  = φ (inj₂ s , λ p →  let (w , ih) = k p
                                             in  inl w , ih)

run : ∀ {Σ Σ′ Σ″ Σ‴ X Y I} → Pseudohomo Σ X I Σ′ Y →
        Σ″ ⇒ (Σ ⊎C Σ′) → Σ′ ⇒ Σ‴ →
        Σ″ ⋆ X → I → Σ‴ ⋆ Y
run φ p q = rec (weaken ⌈ lift φ ⌉Homo p q)

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

prog : (State ℕ ⊎C Abort) ⋆ Bool
prog =
  ⟨ inj₂ (inj₁ (inj₁ tt)) ,       (λ n →   -- get          >>= λ n →
  ⟨ inj₂ (inj₁ (inj₂ (suc n))) ,  (λ _ →   -- put (suc n)
  ⟨ inj₂ (inj₂ tt) ,              (λ _ →   -- aborting
  return true) ⟩) ⟩) ⟩

progA : State ℕ ⋆ Maybe Bool
progA = run abort swapMorph idMorph prog tt

progS : ℕ → Abort ⋆ (Bool × ℕ)
progS = run state idMorph idMorph prog

progAS : ℕ → 𝟘 ⋆ (Maybe Bool × ℕ)
progAS = run state inlMorph idMorph progA

progSA : ℕ → 𝟘 ⋆ Maybe (Bool × ℕ)
progSA n = run abort inlMorph idMorph (progS n) tt

testSA : progSA zero ≡ return nothing
testSA = refl

testAS : progAS zero ≡ return (nothing , suc zero)
testAS = refl

-- The last statement seemed to make the type checker loop.
-- But it just created huge terms during the conversion check
-- and never finished.
-- These terms contained many projection redexes
-- (projection applied to record value).

-- After changing the strategy, such that these redexes are,
-- like beta-redexes, removed immediately in internal syntax,
-- the code checks instantaneously.


text:
-- Andreas, 2018-09-08, issue #3211
--
-- Bug with parametrized module and constructor rewriting.

{-# OPTIONS --rewriting #-}
-- {-# OPTIONS -v rewriting.match:90 -v rewriting:90 #-}
-- {-# OPTIONS -v tc.getConType:50 #-}

module _ (Base : Set) where

open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

data Form : Set where
  Atom : (P : Base) → Form
  _⇒_ : (A B : Form) → Form

data Cxt : Set where
  ε : Cxt
  _∙_ : (Γ : Cxt) (A : Form) → Cxt

infixl 4 _∙_
infix 3 _≤_

data _≤_ : (Γ Δ : Cxt) → Set where
  id≤ : ∀{Γ} → Γ ≤ Γ
  weak : ∀{A Γ Δ} (τ : Γ ≤ Δ) → Γ ∙ A ≤ Δ
  lift : ∀{A Γ Δ} (τ : Γ ≤ Δ) → Γ ∙ A ≤ Δ ∙ A

postulate lift-id≤ : ∀{Γ A} → lift id≤ ≡ id≤ {Γ ∙ A}
{-# REWRITE lift-id≤ #-}

Mon : (P : Cxt → Set) → Set
Mon P = ∀{Γ Δ} (τ : Γ ≤ Δ) → P Δ → P Γ

infix 2 _⊢_

data _⊢_ (Γ : Cxt) : (A : Form) → Set where
  impI   : ∀{A B} (t : Γ ∙ A ⊢ B) → Γ ⊢ A ⇒ B

Tm = λ A Γ → Γ ⊢ A

monD : ∀{A} → Mon (Tm A)
-- monD : ∀{A Γ Δ} (τ : Γ ≤ Δ) → Tm A Δ → Tm A Γ  -- Works
-- monD : ∀{A Γ Δ} (τ : Γ ≤ Δ) → Δ ⊢ A → Γ ⊢ A    -- Works
monD τ (impI t)    = impI (monD (lift τ) t)

monD-id : ∀{Γ A} (t : Γ ⊢ A) → monD id≤ t ≡ t
monD-id (impI t) = cong impI (monD-id t)  -- REWRITE lift-id≤

-- -}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Type.Cubical.Equiv where

import      Lvl
open import Type.Cubical
open import Type.Cubical.Path.Equality
import      Type.Equiv as Type
open import Type

private variable ℓ₁ ℓ₂ : Lvl.Level

-- `Type.Equiv._≍_` specialized to Path.
_≍_ : (A : Type{ℓ₁}) → (B : Type{ℓ₂}) → Type
A ≍ B = A Type.≍ B
{-# BUILTIN EQUIV _≍_ #-}

instance
  [≍]-reflexivity = \{ℓ} → Type.[≍]-reflexivity {ℓ} ⦃ Path-equiv ⦄

instance
  [≍]-symmetry = \{ℓ} → Type.[≍]-symmetry {ℓ} ⦃ Path-equiv ⦄

instance
  [≍]-transitivity = \{ℓ} → Type.[≍]-transitivity {ℓ} ⦃ Path-equiv ⦄ ⦃ Path-congruence₁ ⦄

instance
  [≍]-equivalence = \{ℓ} → Type.[≍]-equivalence {ℓ} ⦃ Path-equiv ⦄ ⦃ Path-congruence₁ ⦄


text:
open import bool
open import level
open import eq
open import product
open import product-thms
open import relations

-- module closures where

--   module basics {ℓ ℓ' : level}{A : Set ℓ} (_>A_ : A → A → Set ℓ') where

--     data tc : A → A → Set (ℓ ⊔ ℓ') where
--       tc-step : ∀{a b : A} → a >A b → tc a b
--       tc-trans : ∀{a b c : A} → tc a b → tc b c → tc a c

--     data rc : A → A → Set (ℓ ⊔ ℓ') where
--       rc-step : ∀{a b : A} → a >A b → rc a b
--       rc-refl : ∀{a : A} → rc a a

--     tc-transitive : transitive tc
--     tc-transitive = tc-trans

--   module combinations {ℓ ℓ' : level}{A : Set ℓ} (_>A_ : A → A → Set ℓ') where
--      open basics public

--      rtc : A → A → Set (ℓ ⊔ ℓ')
--      rtc = rc (tc _>A_)

--      rtc-refl : reflexive rtc
--      rtc-refl = rc-refl

--      rtc-trans : transitive rtc
--      rtc-trans (rc-step{a}{b} x) (rc-step{.b}{c} x') = rc-step (tc-trans x x')
--      rtc-trans (rc-step x) rc-refl = rc-step x
--      rtc-trans rc-refl (rc-step x) = rc-step x
--      rtc-trans rc-refl rc-refl = rc-refl

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
------------------------------------------------------------------------
-- Typing and kinding of Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Typing where

open import Data.Context.WellFormed
open import Data.Fin using (Fin; zero)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Fin.Substitution.Typed
open import Data.Nat using (ℕ)
open import Data.Product using (_,_; _×_)
open import Level using () renaming (zero to lzero)
open import Relation.Binary.PropositionalEquality as PropEq hiding ([_])

open import FOmegaInt.Syntax

------------------------------------------------------------------------
-- Typing derivations.

module Typing where
  open TermCtx
  open Syntax
  open Substitution using (_[_]; _Kind[_]; weaken)

  infix 4 _ctx _⊢_kd _⊢_wf
  infix 4 _⊢Tp_∈_ _⊢Tm_∈_ _⊢_∈_
  infix 4 _⊢_<:_∈_ _⊢_<∷_ _⊢_≤_
  infix 4 _⊢_≃_∈_ _⊢_≅_ _⊢_≃_wf _≃_ctx
  mutual

    -- Well-formed typing contexts.

    _ctx : ∀ {n} → Ctx n → Set
    _ctx = ContextFormation._wf _⊢_wf

    -- Well-formed type/kind ascriptions in typing contexts.

    data _⊢_wf {n} (Γ : Ctx n) : TermAsc n → Set where
      wf-kd : ∀ {a} → Γ ⊢ a kd    → Γ ⊢ (kd a) wf
      wf-tp : ∀ {a} → Γ ⊢Tp a ∈ * → Γ ⊢ (tp a) wf

    -- Well-formed kinds.

    data _⊢_kd {n} (Γ : Ctx n) : Kind Term n → Set where
      kd-⋯ : ∀ {a b} → Γ ⊢Tp a ∈ * → Γ ⊢Tp b ∈ * → Γ ⊢ a ⋯ b kd
      kd-Π : ∀ {j k} → Γ ⊢ j kd → kd j ∷ Γ ⊢ k kd → Γ ⊢ Π j k kd

    -- Kinding derivations.

    data _⊢Tp_∈_ {n} (Γ : Ctx n) : Term n → Kind Term n → Set where
      ∈-var : ∀ {k} x → Γ ctx → lookup Γ x ≡ kd k → Γ ⊢Tp var x ∈ k
      ∈-⊥-f : Γ ctx → Γ ⊢Tp ⊥ ∈ *
      ∈-⊤-f : Γ ctx → Γ ⊢Tp ⊤ ∈ *
      ∈-∀-f : ∀ {k a} → Γ ⊢ k kd → kd k ∷ Γ ⊢Tp a ∈ * → Γ ⊢Tp Π k a ∈ *
      ∈-→-f : ∀ {a b} → Γ ⊢Tp a ∈ * → Γ ⊢Tp b ∈ * → Γ ⊢Tp a ⇒ b ∈ *
      ∈-Π-i : ∀ {j a k} → Γ ⊢ j kd → kd j ∷ Γ ⊢Tp a ∈ k →
              Γ ⊢Tp Λ j a ∈ Π j k
      ∈-Π-e : ∀ {a b j k} → Γ ⊢Tp a ∈ Π j k → Γ ⊢Tp b ∈ j →
              Γ ⊢Tp a · b ∈ k Kind[ b ]
      ∈-s-i : ∀ {a b c} → Γ ⊢Tp a ∈ b ⋯ c → Γ ⊢Tp a ∈ a ⋯ a
      ∈-⇑   : ∀ {a j k} → Γ ⊢Tp a ∈ j → Γ ⊢ j <∷ k → Γ ⊢Tp a ∈ k

    -- Subkinding derivations.

    data _⊢_<∷_ {n} (Γ : Ctx n) : Kind Term n → Kind Term n → Set where
      <∷-⋯ : ∀ {a₁ a₂ b₁ b₂} →
             Γ ⊢ a₂ <: a₁ ∈ * → Γ ⊢ b₁ <: b₂ ∈ * → Γ ⊢ a₁ ⋯ b₁ <∷ a₂ ⋯ b₂
      <∷-Π : ∀ {j₁ j₂ k₁ k₂} →
             Γ ⊢ j₂ <∷ j₁ → kd j₂ ∷ Γ ⊢ k₁ <∷ k₂ → Γ ⊢ Π j₁ k₁ kd →
             Γ ⊢ Π j₁ k₁ <∷ Π j₂ k₂

    -- Subtyping derivations.

    data _⊢_<:_∈_ {n} (Γ : Ctx n) : Term n → Term n → Kind Term n → Set where
      <:-refl  : ∀ {a k}     → Γ ⊢Tp a ∈ k → Γ ⊢ a <: a ∈ k
      <:-trans : ∀ {a b c k} → Γ ⊢ a <: b ∈ k → Γ ⊢ b <: c ∈ k → Γ ⊢ a <: c ∈ k
      <:-β₁    : ∀ {j a k b} → kd j ∷ Γ ⊢Tp a ∈ k → Γ ⊢Tp b ∈ j →
                 Γ ⊢ (Λ j a) · b <: a [ b ] ∈ k Kind[ b ]
      <:-β₂    : ∀ {j a k b} → kd j ∷ Γ ⊢Tp a ∈ k → Γ ⊢Tp b ∈ j →
                 Γ ⊢ a [ b ] <: (Λ j a) · b ∈ k Kind[ b ]
      <:-η₁    : ∀ {a j k} → Γ ⊢Tp a ∈ Π j k →
                 Γ ⊢ Λ j (weaken a · var zero) <: a ∈ Π j k
      <:-η₂    : ∀ {a j k} → Γ ⊢Tp a ∈ Π j k →
                 Γ ⊢ a <: Λ j (weaken a · var zero) ∈ Π j k
      <:-⊥     : ∀ {a b c} → Γ ⊢Tp a ∈ b ⋯ c → Γ ⊢ ⊥ <: a ∈ *
      <:-⊤     : ∀ {a b c} → Γ ⊢Tp a ∈ b ⋯ c → Γ ⊢ a <: ⊤ ∈ *
      <:-∀     : ∀ {k₁ k₂ a₁ a₂} →
                 Γ ⊢ k₂ <∷ k₁ → kd k₂ ∷ Γ ⊢ a₁ <: a₂ ∈ * → Γ ⊢Tp Π k₁ a₁ ∈ * →
                 Γ ⊢ Π k₁ a₁ <: Π k₂ a₂ ∈ *
      <:-→     : ∀ {a₁ a₂ b₁ b₂} → Γ ⊢ a₂ <: a₁ ∈ * → Γ ⊢ b₁ <: b₂ ∈ * →
                 Γ ⊢ a₁ ⇒ b₁ <: a₂ ⇒ b₂ ∈ *
      <:-λ     : ∀ {j₁ j₂ a₁ a₂ j k} → kd j ∷ Γ ⊢ a₁ <: a₂ ∈ k →
                 Γ ⊢Tp Λ j₁ a₁ ∈ Π j k → Γ ⊢Tp Λ j₂ a₂ ∈ Π j k →
                 Γ ⊢ Λ j₁ a₁ <: Λ j₂ a₂ ∈ Π j k
      <:-·     : ∀ {a₁ a₂ b₁ b₂ j k} → Γ ⊢ a₁ <: a₂ ∈ Π j k → Γ ⊢ b₁ ≃ b₂ ∈ j →
                 Γ ⊢ a₁ · b₁ <: a₂ · b₂ ∈ k Kind[ b₁ ]
      <:-⟨|    : ∀ {a b c} → Γ ⊢Tp a ∈ b ⋯ c → Γ ⊢ b <: a ∈ *
      <:-|⟩    : ∀ {a b c} → Γ ⊢Tp a ∈ b ⋯ c → Γ ⊢ a <: c ∈ *
      <:-⋯-i   : ∀ {a b c d} → Γ ⊢ a <: b ∈ c ⋯ d → Γ ⊢ a <: b ∈ a ⋯ b
      <:-⇑     : ∀ {a b j k} → Γ ⊢ a <: b ∈ j → Γ ⊢ j <∷ k → Γ ⊢ a <: b ∈ k

    -- Type equality.

    data _⊢_≃_∈_ {n} (Γ : Ctx n) : Term n → Term n → Kind Term n → Set where
      <:-antisym : ∀ {a b k} → Γ ⊢ a <: b ∈ k → Γ ⊢ b <: a ∈ k → Γ ⊢ a ≃ b ∈ k

  -- Kind equality.

  data _⊢_≅_ {n} (Γ : Ctx n) : Kind Term n → Kind Term n → Set where
    <∷-antisym : ∀ {j k} → Γ ⊢ j <∷ k → Γ ⊢ k <∷ j → Γ ⊢ j ≅ k

  -- Typing derivations.

  data _⊢Tm_∈_ {n} (Γ : Ctx n) : Term n → Term n → Set where
    ∈-var : ∀ {a} x → Γ ctx → lookup Γ x ≡ tp a → Γ ⊢Tm var x ∈ a
    ∈-∀-i : ∀ {k a b} → Γ ⊢ k kd → kd k ∷ Γ ⊢Tm a ∈ b →
            Γ ⊢Tm Λ k a ∈ Π k b
    ∈-→-i : ∀ {a b c} → Γ ⊢Tp a ∈ * → tp a ∷ Γ ⊢Tm b ∈ weaken c →
            -- NOTE. The following premise is a redundant validity
            -- condition that could be avoided by proving a context
            -- strengthening lemma (showing that unused variables,
            -- i.e. variables not appearing freely to the right of the
            -- turnstyle, can be eliminated from the context).
            Γ ⊢Tp c ∈ * →
            Γ ⊢Tm ƛ a b ∈ a ⇒ c
    ∈-∀-e : ∀ {a b k c} → Γ ⊢Tm a ∈ Π k c → Γ ⊢Tp b ∈ k →
            Γ ⊢Tm a ⊡ b ∈ c [ b ]
    ∈-→-e : ∀ {a b c d} → Γ ⊢Tm a ∈ c ⇒ d → Γ ⊢Tm b ∈ c →
            Γ ⊢Tm a · b ∈ d
    ∈-⇑   : ∀ {a b c} → Γ ⊢Tm a ∈ b → Γ ⊢ b <: c ∈ * → Γ ⊢Tm a ∈ c

  -- Combined typing and kinding of terms and types.

  data _⊢_∈_ {n} (Γ : Ctx n) : Term n → TermAsc n → Set where
    ∈-tp : ∀ {a k} → Γ ⊢Tp a ∈ k → Γ ⊢ a ∈ kd k
    ∈-tm : ∀ {a b} → Γ ⊢Tm a ∈ b → Γ ⊢ a ∈ tp b

  -- Combined subtyping and subkinding.

  data _⊢_≤_ {n} (Γ : Ctx n) : TermAsc n → TermAsc n → Set where
    ≤-<∷ : ∀ {j k} → Γ ⊢ j <∷ k     → Γ ⊢ kd j ≤ kd k
    ≤-<: : ∀ {a b} → Γ ⊢ a <: b ∈ * → Γ ⊢ tp a ≤ tp b

  mutual

    -- Combined kind and type equality, i.e. equality of well-formed
    -- ascriptions.

    data _⊢_≃_wf {n} (Γ : Ctx n) : TermAsc n → TermAsc n → Set where
      ≃wf-≅ : ∀ {j k} → Γ ⊢ j ≅ k     → Γ ⊢ kd j ≃ kd k wf
      ≃wf-≃ : ∀ {a b} → Γ ⊢ a ≃ b ∈ * → Γ ⊢ tp a ≃ tp b wf

    -- Equality of well-formed contexts.

    data _≃_ctx : ∀ {n} → Ctx n → Ctx n → Set where
      ≃-[] : [] ≃ [] ctx
      ≃-∷  : ∀ {n a b} {Γ Δ : Ctx n} →
             Γ ⊢ a ≃ b wf → Γ ≃ Δ ctx → a ∷ Γ ≃ b ∷ Δ ctx

  open PropEq using ([_])

  -- A derived variable rule.

  ∈-var′ : ∀ {n} {Γ : Ctx n} x → Γ ctx → Γ ⊢ var x ∈ lookup Γ x
  ∈-var′ {Γ = Γ} x Γ-ctx with lookup Γ x | inspect (lookup Γ) x
  ∈-var′ x Γ-ctx | kd k | [ Γ[x]≡kd-k ] = ∈-tp (∈-var x Γ-ctx Γ[x]≡kd-k)
  ∈-var′ x Γ-ctx | tp a | [ Γ[x]≡tp-a ] = ∈-tm (∈-var x Γ-ctx Γ[x]≡tp-a)

  -- A derived subsumption rule.

  ∈-⇑′ : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢ a ∈ b → Γ ⊢ b ≤ c → Γ ⊢ a ∈ c
  ∈-⇑′ (∈-tp a∈b) (≤-<∷ b<∷c) = ∈-tp (∈-⇑ a∈b b<∷c)
  ∈-⇑′ (∈-tm a∈b) (≤-<: b<:c) = ∈-tm (∈-⇑ a∈b b<:c)

  open ContextFormation _⊢_wf public
    hiding (_wf) renaming (_⊢_wfExt to _⊢_ext)

------------------------------------------------------------------------
-- Properties of typings

open Syntax
open TermCtx
open Typing

-- Inversion lemmas for _⊢_wf.

wf-kd-inv : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ kd k wf → Γ ⊢ k kd
wf-kd-inv (wf-kd k-kd) = k-kd

wf-tp-inv : ∀ {n} {Γ : Ctx n} {a} → Γ ⊢ tp a wf → Γ ⊢Tp a ∈ *
wf-tp-inv (wf-tp a∈*) = a∈*

-- An inversion lemma for _⊢_≃_wf.

≃wf-kd-inv : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ kd j ≃ kd k wf → Γ ⊢ j ≅ k
≃wf-kd-inv (≃wf-≅ j≅k) = j≅k

-- Kind and type equality imply subkinding and subtyping, respectively.

≅⇒<∷ : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j ≅ k → Γ ⊢ j <∷ k
≅⇒<∷ (<∷-antisym j<∷k k<∷j) = j<∷k

≃⇒<: : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a ≃ b ∈ k → Γ ⊢ a <: b ∈ k
≃⇒<: (<:-antisym a<:b b<:a) = a<:b

-- Reflexivity of subkinding.
<∷-refl : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ ⊢ k <∷ k
<∷-refl (kd-⋯ a∈* b∈*)   = <∷-⋯ (<:-refl a∈*) (<:-refl b∈*)
<∷-refl (kd-Π j-kd k-kd) = <∷-Π (<∷-refl j-kd) (<∷-refl k-kd) (kd-Π j-kd k-kd)

-- Reflexivity of kind equality.
≅-refl : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ ⊢ k ≅ k
≅-refl k-kd = <∷-antisym (<∷-refl k-kd) (<∷-refl k-kd)

-- Symmetry of kind equality.
≅-sym : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j ≅ k → Γ ⊢ k ≅ j
≅-sym (<∷-antisym j<∷k k<∷j) = <∷-antisym k<∷j j<∷k

-- An admissible kind equality rule for interval kinds.
≅-⋯ : ∀ {n} {Γ : Ctx n} {a₁ a₂ b₁ b₂} →
      Γ ⊢ a₁ ≃ a₂ ∈ * → Γ ⊢ b₁ ≃ b₂ ∈ * → Γ ⊢ a₁ ⋯ b₁ ≅ a₂ ⋯ b₂
≅-⋯ (<:-antisym a₁<:a₂ a₂<:a₁) (<:-antisym b₁<:b₂ b₂<:b₁) =
  <∷-antisym (<∷-⋯ a₂<:a₁ b₁<:b₂) (<∷-⋯ a₁<:a₂ b₂<:b₁)

-- Type equality is reflexive.
≃-refl : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Tp a ∈ k → Γ ⊢ a ≃ a ∈ k
≃-refl a∈k = <:-antisym (<:-refl a∈k) (<:-refl a∈k)

-- Type equality is transitive.
≃-trans : ∀ {n} {Γ : Ctx n} {a b c k} →
          Γ ⊢ a ≃ b ∈ k → Γ ⊢ b ≃ c ∈ k → Γ ⊢ a ≃ c ∈ k
≃-trans (<:-antisym a<:b b<:a) (<:-antisym b<:c c<:b) =
  <:-antisym (<:-trans a<:b b<:c) (<:-trans c<:b b<:a)

-- Type equality is symmetric.
≃-sym : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a ≃ b ∈ k → Γ ⊢ b ≃ a ∈ k
≃-sym (<:-antisym a<:b b<:a) = <:-antisym b<:a a<:b

-- Types inhabiting interval kinds are proper Types.
Tp∈-⋯-* : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Tp a ∈ b ⋯ c → Γ ⊢Tp a ∈ *
Tp∈-⋯-* a∈b⋯c = ∈-⇑ (∈-s-i a∈b⋯c) (<∷-⋯ (<:-⊥ a∈b⋯c) (<:-⊤ a∈b⋯c))

-- Well-formedness of the * kind.
*-kd : ∀ {n} {Γ : Ctx n} → Γ ctx → Γ ⊢ * kd
*-kd Γ-ctx = kd-⋯ (∈-⊥-f Γ-ctx) (∈-⊤-f Γ-ctx)

module _ where
  open Substitution

  -- An admissible β-rule for type equality.
  ≃-β : ∀ {n} {Γ : Ctx n} {j a k b} → kd j ∷ Γ ⊢Tp a ∈ k → Γ ⊢Tp b ∈ j →
        Γ ⊢ (Λ j a) · b ≃ a [ b ] ∈ k Kind[ b ]
  ≃-β a∈k b∈j = <:-antisym (<:-β₁ a∈k b∈j) (<:-β₂ a∈k b∈j)

  -- An admissible η-rule for type equality.
  ≃-η : ∀ {n} {Γ : Ctx n} {a j k} →
        Γ ⊢Tp a ∈ Π j k → Γ ⊢ Λ j (weaken a · var zero) ≃ a ∈ Π j k
  ≃-η a∈Πjk = <:-antisym (<:-η₁ a∈Πjk) (<:-η₂ a∈Πjk)

-- An admissible congruence rule for type equality w.r.t. formation of
-- arrow types.
≃-→ : ∀ {n} {Γ : Ctx n} {a₁ a₂ b₁ b₂} →
      Γ ⊢ a₁ ≃ a₂ ∈ * → Γ ⊢ b₁ ≃ b₂ ∈ * → Γ ⊢ a₁ ⇒ b₁ ≃ a₂ ⇒ b₂ ∈ *
≃-→ (<:-antisym a₁<:a₂∈* a₂<:a₁∈*) (<:-antisym b₁<:b₂∈* b₂<:b₁∈*) =
  <:-antisym (<:-→ a₂<:a₁∈* b₁<:b₂∈*) (<:-→ a₁<:a₂∈* b₂<:b₁∈*)

-- An admissible congruence rule for type equality w.r.t. operator
-- abstraction.
≃-λ : ∀ {n} {Γ : Ctx n} {j₁ j₂ a₁ a₂ j k} →
      kd j ∷ Γ ⊢ a₁ ≃ a₂ ∈ k → Γ ⊢Tp Λ j₁ a₁ ∈ Π j k → Γ ⊢Tp Λ j₂ a₂ ∈ Π j k →
      Γ ⊢ Λ j₁ a₁ ≃ Λ j₂ a₂ ∈ Π j k
≃-λ (<:-antisym a₁<:a₂∈k a₂<:a₁∈k) Λj₁a₁∈Πjk Λj₂a₂∈Πjk =
  <:-antisym (<:-λ a₁<:a₂∈k Λj₁a₁∈Πjk Λj₂a₂∈Πjk)
             (<:-λ a₂<:a₁∈k Λj₂a₂∈Πjk Λj₁a₁∈Πjk)

-- An admissible subsumption rule for type equality.
≃-⇑ : ∀ {n} {Γ : Ctx n} {a b j k} → Γ ⊢ a ≃ b ∈ j → Γ ⊢ j <∷ k → Γ ⊢ a ≃ b ∈ k
≃-⇑ (<:-antisym a<:b b<:a) j<∷k = <:-antisym (<:-⇑ a<:b j<∷k) (<:-⇑ b<:a j<∷k)

-- NOTE.  There are more admissible rules one might want to prove
-- here, such as congruence lemmas for type and kind equality
-- w.r.t. the remaining type constructors (e.g. Π and _·_) or
-- transitivity of subkinding and kind equality.  But the proofs of
-- these lemmas require context narrowing and/or validity lemmas which
-- we have not yet established.  We will prove these lemmas once we
-- have established validity of the declarative judgments (see the
-- Typing.Validity module).

-- The contexts of all the above judgments are well-formed.

mutual

  kd-ctx : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ ctx
  kd-ctx (kd-⋯ a∈* b∈*)    = Tp∈-ctx a∈*
  kd-ctx (kd-Π j-kd  k-kd) = kd-ctx j-kd

  Tp∈-ctx : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Tp a ∈ k → Γ ctx
  Tp∈-ctx (∈-var x Γ-ctx Γ[x]≡kd-k) = Γ-ctx
  Tp∈-ctx (∈-⊥-f Γ-ctx)     = Γ-ctx
  Tp∈-ctx (∈-⊤-f Γ-ctx)     = Γ-ctx
  Tp∈-ctx (∈-∀-f k-kd a∈*)  = kd-ctx k-kd
  Tp∈-ctx (∈-→-f a∈* b∈*)   = Tp∈-ctx a∈*
  Tp∈-ctx (∈-Π-i j-kd a∈k)  = kd-ctx j-kd
  Tp∈-ctx (∈-Π-e a∈Πjk b∈j) = Tp∈-ctx a∈Πjk
  Tp∈-ctx (∈-s-i a∈b⋯c)     = Tp∈-ctx a∈b⋯c
  Tp∈-ctx (∈-⇑ a∈j j<∷k)    = Tp∈-ctx a∈j

wf-ctx : ∀ {n} {Γ : Ctx n} {a} → Γ ⊢ a wf → Γ ctx
wf-ctx (wf-kd k-kd) = kd-ctx k-kd
wf-ctx (wf-tp a∈*)  = Tp∈-ctx a∈*

<:-ctx : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a <: b ∈ k → Γ ctx
<:-ctx (<:-refl a∈k)            = Tp∈-ctx a∈k
<:-ctx (<:-trans a<:b∈k b<:c∈k) = <:-ctx a<:b∈k
<:-ctx (<:-β₁ a∈j b∈k) = Tp∈-ctx b∈k
<:-ctx (<:-β₂ a∈j b∈k) = Tp∈-ctx b∈k
<:-ctx (<:-η₁ a∈Πjk)   = Tp∈-ctx a∈Πjk
<:-ctx (<:-η₂ a∈Πjk)   = Tp∈-ctx a∈Πjk
<:-ctx (<:-⊥ a∈b⋯c)    = Tp∈-ctx a∈b⋯c
<:-ctx (<:-⊤ a∈b⋯c)    = Tp∈-ctx a∈b⋯c
<:-ctx (<:-∀ k₂<∷k₁ a₁<:a₂ ∀k₁a₁∈*) = Tp∈-ctx ∀k₁a₁∈*
<:-ctx (<:-→ a₂<:a₁ b₁<:b₂)         = <:-ctx a₂<:a₁
<:-ctx (<:-λ a₂<:a₁∈Πjk Λa₁k₁∈Πjk Λa₂k₂∈Πjk) = Tp∈-ctx Λa₁k₁∈Πjk
<:-ctx (<:-· a₂<:a₁∈Πjk b₂≃b₁∈j)             = <:-ctx a₂<:a₁∈Πjk
<:-ctx (<:-⟨| a∈b⋯c)      = Tp∈-ctx a∈b⋯c
<:-ctx (<:-|⟩ a∈b⋯c)      = Tp∈-ctx a∈b⋯c
<:-ctx (<:-⋯-i a<:b∈c⋯d)  = <:-ctx a<:b∈c⋯d
<:-ctx (<:-⇑ a<:b∈j j<∷k) = <:-ctx a<:b∈j

<∷-ctx : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j <∷ k → Γ ctx
<∷-ctx (<∷-⋯ a₂<:a₁ b₁<:b₂)          = <:-ctx a₂<:a₁
<∷-ctx (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd) = <∷-ctx j₂<∷j₁

≅-ctx : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j ≅ k → Γ ctx
≅-ctx (<∷-antisym j<∷k k<∷j) = <∷-ctx j<∷k

≃-ctx : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a ≃ b ∈ k → Γ ctx
≃-ctx (<:-antisym a<:b∈k b<:a∈k) = <:-ctx a<:b∈k

Tm∈-ctx : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢Tm a ∈ b → Γ ctx
Tm∈-ctx (∈-var x Γ-ctx Γ[x]≡tp-a) = Γ-ctx
Tm∈-ctx (∈-∀-i k-kd a∈b)    = kd-ctx k-kd
Tm∈-ctx (∈-→-i a∈* b∈c c∈*) = Tp∈-ctx a∈*
Tm∈-ctx (∈-∀-e a∈∀kc b∈k)   = Tm∈-ctx a∈∀kc
Tm∈-ctx (∈-→-e a∈c⇒d b∈c)   = Tm∈-ctx a∈c⇒d
Tm∈-ctx (∈-⇑ a∈b b<:c)      = Tm∈-ctx a∈b

∈-ctx : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a ∈ b → Γ ctx
∈-ctx (∈-tp a∈k) = Tp∈-ctx a∈k
∈-ctx (∈-tm a∈b) = Tm∈-ctx a∈b

----------------------------------------------------------------------
-- Well-typed substitutions (i.e. substitution lemmas)

-- A shorthand for kindings and typings of Ts by kind or type
-- ascriptions.
TermAscTyping : (ℕ → Set) → Set₁
TermAscTyping T = Typing TermAsc T TermAsc lzero

-- Liftings from well-typed Ts to well-typed/kinded terms/types.
LiftTo-∈ : ∀ {T} → TermAscTyping T → Set₁
LiftTo-∈ _⊢T_∈_ = LiftTyped Substitution.termAscTermSubst _⊢_wf _⊢T_∈_ _⊢_∈_

-- Helper lemmas about untyped T-substitutions in raw terms and kinds.

record TypedSubstAppHelpers {T} (rawLift : Lift T Term) : Set where
  open Substitution using (weaken; _[_]; _Kind[_])
  module A = SubstApp rawLift
  module L = Lift     rawLift

  field
    -- Substitutions in kinds and types commute.

    Kind/-sub-↑ : ∀ {m n} k a (σ : Sub T m n) →
                  k Kind[ a ] A.Kind/ σ ≡ (k A.Kind/ σ L.↑) Kind[ a A./ σ ]

    /-sub-↑ : ∀ {m n} b a (σ : Sub T m n) →
              b [ a ] A./ σ ≡ (b A./ σ L.↑) [ a A./ σ ]

    -- Weakening of terms commutes with substitution in terms.

    weaken-/ : ∀ {m n} {σ : Sub T m n} a →
               weaken (a A./ σ) ≡ weaken a A./ σ L.↑

-- Application of generic well-typed T-substitutions to all the judgments.

module TypedSubstApp {T : ℕ → Set} (_⊢T_∈_ : TermAscTyping T)
                     (liftTyped : LiftTo-∈ _⊢T_∈_)
                     (helpers : TypedSubstAppHelpers
                                  (LiftTyped.rawLift liftTyped))
                     where

  open LiftTyped liftTyped renaming (lookup to /∈-lookup)
  open TypedSubstAppHelpers helpers

  -- Lift well-kinded Ts to well-kinded types.
  liftTp : ∀ {n} {Γ : Ctx n} {a k kd-k} →
           kd-k ≡ kd k → Γ ⊢T a ∈ kd-k → Γ ⊢Tp L.lift a ∈ k
  liftTp refl a∈kd-k with ∈-lift a∈kd-k
  liftTp refl a∈kd-k | ∈-tp a∈k = a∈k

  -- Lift well-typed Ts to well-typed terms.
  liftTm : ∀ {n} {Γ : Ctx n} {a b tp-b} →
           tp-b ≡ tp b → Γ ⊢T a ∈ tp-b → Γ ⊢Tm L.lift a ∈ b
  liftTm refl a∈tp-b with ∈-lift a∈tp-b
  liftTm refl a∈tp-b | ∈-tm a∈b = a∈b

  mutual

    -- Substitutions preserve well-formedness of kinds and
    -- well-kindedness of types.

    kd-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {k σ} →
           Γ ⊢ k kd → Δ ⊢/ σ ∈ Γ → Δ ⊢ k A.Kind/ σ kd
    kd-/ (kd-⋯ a∈* b∈*)   σ∈Γ = kd-⋯ (Tp∈-/ a∈* σ∈Γ) (Tp∈-/ b∈* σ∈Γ)
    kd-/ (kd-Π j-kd k-kd) σ∈Γ =
      kd-Π j/σ-kd (kd-/ k-kd (∈-↑ (wf-kd j/σ-kd) σ∈Γ))
      where j/σ-kd = kd-/ j-kd σ∈Γ

    Tp∈-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a k σ} →
            Γ ⊢Tp a ∈ k → Δ ⊢/ σ ∈ Γ → Δ ⊢Tp a A./ σ ∈ k A.Kind/ σ
    Tp∈-/ (∈-var x Γ-ctx Γ[x]≡kd-k) σ∈Γ =
      liftTp (cong (_/ _) Γ[x]≡kd-k) (/∈-lookup σ∈Γ x)
    Tp∈-/ (∈-⊥-f Γ-ctx)    σ∈Γ = ∈-⊥-f (/∈-wf σ∈Γ)
    Tp∈-/ (∈-⊤-f Γ-ctx)    σ∈Γ = ∈-⊤-f (/∈-wf σ∈Γ)
    Tp∈-/ (∈-∀-f k-kd a∈*) σ∈Γ =
      ∈-∀-f k/σ-kd (Tp∈-/ a∈* (∈-↑ (wf-kd k/σ-kd) σ∈Γ))
      where k/σ-kd = kd-/ k-kd σ∈Γ
    Tp∈-/ (∈-→-f a∈* b∈*)  σ∈Γ = ∈-→-f (Tp∈-/ a∈* σ∈Γ) (Tp∈-/ b∈* σ∈Γ)
    Tp∈-/ (∈-Π-i j-kd a∈k) σ∈Γ =
      ∈-Π-i j/σ-kd (Tp∈-/ a∈k (∈-↑ (wf-kd j/σ-kd) σ∈Γ))
      where j/σ-kd = kd-/ j-kd σ∈Γ
    Tp∈-/ (∈-Π-e {_} {b} {_} {k} a∈Πjk b∈j) σ∈Γ =
      subst (_ ⊢Tp _ ∈_) (sym (Kind/-sub-↑ k b _))
            (∈-Π-e (Tp∈-/ a∈Πjk σ∈Γ) (Tp∈-/ b∈j σ∈Γ))
    Tp∈-/ (∈-s-i a∈b⋯c)  σ∈Γ = ∈-s-i (Tp∈-/ a∈b⋯c σ∈Γ)
    Tp∈-/ (∈-⇑ a∈j j<∷k) σ∈Γ = ∈-⇑ (Tp∈-/ a∈j σ∈Γ) (<∷-/ j<∷k σ∈Γ)

    -- Substitutions commute with subkinding, subtyping and type
    -- equality.

    <∷-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {j k σ} →
           Γ ⊢ j <∷ k → Δ ⊢/ σ ∈ Γ → Δ ⊢ j A.Kind/ σ <∷ k A.Kind/ σ
    <∷-/ (<∷-⋯ a₂<:a₁ b₁<:b₂) σ∈Γ = <∷-⋯ (<:-/ a₂<:a₁ σ∈Γ) (<:-/ b₁<:b₂ σ∈Γ)
    <∷-/ (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd) σ∈Γ =
      <∷-Π (<∷-/ j₂<∷j₁ σ∈Γ) (<∷-/ k₁<∷k₂ (∈-↑ (<∷-/-wf k₁<∷k₂ σ∈Γ) σ∈Γ))
           (kd-/ Πj₁k₁-kd σ∈Γ)

    <:-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b k σ} →
           Γ ⊢ a <: b ∈ k → Δ ⊢/ σ ∈ Γ → Δ ⊢ a A./ σ <: b A./ σ ∈ k A.Kind/ σ
    <:-/ (<:-refl a∈k)            σ∈Γ = <:-refl (Tp∈-/ a∈k σ∈Γ)
    <:-/ (<:-trans a<:b∈k b<:c∈k) σ∈Γ =
      <:-trans (<:-/ a<:b∈k σ∈Γ) (<:-/ b<:c∈k σ∈Γ)
    <:-/ (<:-β₁ {j} {a} {k} {b} a∈k b∈j) σ∈Γ =
      subst₂ (_ ⊢ (Λ j a) · b A./ _ <:_∈_)
             (sym (/-sub-↑ a b _)) (sym (Kind/-sub-↑ k b _))
             (<:-β₁ (Tp∈-/ a∈k (∈-↑ (Tp∈-/-wf a∈k σ∈Γ) σ∈Γ)) (Tp∈-/ b∈j σ∈Γ))
    <:-/ (<:-β₂ {j} {a} {k} {b} a∈k b∈j) σ∈Γ =
      subst₂ (_ ⊢_<: (Λ j a) · b A./ _ ∈_)
             (sym (/-sub-↑ a b _)) (sym (Kind/-sub-↑ k b _))
             (<:-β₂ (Tp∈-/ a∈k (∈-↑ (Tp∈-/-wf a∈k σ∈Γ) σ∈Γ)) (Tp∈-/ b∈j σ∈Γ))
    <:-/ {Δ = Δ} {σ = σ} (<:-η₁ {a} {j} {k} a∈Πjk) σ∈Γ =
      subst (Δ ⊢_<: a A./ σ ∈ Π j k A.Kind/ σ)
            (cong (Λ _) (cong₂ _·_ (weaken-/ a) (sym (lift-var zero))))
            (<:-η₁ (Tp∈-/ a∈Πjk σ∈Γ))
    <:-/ {Δ = Δ} {σ = σ} (<:-η₂  {a} {j} {k} a∈Πjk) σ∈Γ =
      subst (Δ ⊢ a A./ σ <:_∈ Π j k A.Kind/ σ)
            (cong (Λ _) (cong₂ _·_ (weaken-/ a) (sym (lift-var zero))))
            (<:-η₂ (Tp∈-/ a∈Πjk σ∈Γ))
    <:-/ (<:-⊥ a∈b⋯c) σ∈Γ = <:-⊥ (Tp∈-/ a∈b⋯c σ∈Γ)
    <:-/ (<:-⊤ a∈b⋯c) σ∈Γ = <:-⊤ (Tp∈-/ a∈b⋯c σ∈Γ)
    <:-/ (<:-∀ k₂<∷k₁ a₁<:a₂∈* ∀j₁k₁∈*) σ∈Γ =
      <:-∀ (<∷-/ k₂<∷k₁ σ∈Γ) (<:-/ a₁<:a₂∈* (∈-↑ (<:-/-wf a₁<:a₂∈* σ∈Γ) σ∈Γ))
           (Tp∈-/ ∀j₁k₁∈* σ∈Γ)
    <:-/ (<:-→ a₂<:a₁∈* b₁<:b₂∈*) σ∈Γ =
      <:-→ (<:-/ a₂<:a₁∈* σ∈Γ) (<:-/ b₁<:b₂∈* σ∈Γ)
    <:-/ (<:-λ a₁<:a₂∈k Λj₁a₁∈Πjk Λj₂a₂∈Πjk) σ∈Γ =
      <:-λ (<:-/ a₁<:a₂∈k (∈-↑ (<:-/-wf a₁<:a₂∈k σ∈Γ) σ∈Γ))
           (Tp∈-/ Λj₁a₁∈Πjk σ∈Γ) (Tp∈-/ Λj₂a₂∈Πjk σ∈Γ)
    <:-/ (<:-· {k = k} a₁<:a₂∈Πjk b₁≃b₂∈j) σ∈Γ =
      subst (_ ⊢ _ <: _ ∈_) (sym (Kind/-sub-↑ k _ _))
            (<:-· (<:-/ a₁<:a₂∈Πjk σ∈Γ) (≃-/ b₁≃b₂∈j σ∈Γ))
    <:-/ (<:-⟨| a∈b⋯c)      σ∈Γ = <:-⟨| (Tp∈-/ a∈b⋯c σ∈Γ)
    <:-/ (<:-|⟩ a∈b⋯c)      σ∈Γ = <:-|⟩ (Tp∈-/ a∈b⋯c σ∈Γ)
    <:-/ (<:-⋯-i a<:b∈c⋯d)  σ∈Γ = <:-⋯-i (<:-/ a<:b∈c⋯d σ∈Γ)
    <:-/ (<:-⇑ a<:b∈j j<∷k) σ∈Γ = <:-⇑ (<:-/ a<:b∈j σ∈Γ) (<∷-/ j<∷k σ∈Γ)

    ≃-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b k σ} →
          Γ ⊢ a ≃ b ∈ k → Δ ⊢/ σ ∈ Γ → Δ ⊢ a A./ σ ≃ b A./ σ ∈ k A.Kind/ σ
    ≃-/ (<:-antisym a<:b∈k b<:a∈k) σ∈Γ =
      <:-antisym (<:-/ a<:b∈k σ∈Γ) (<:-/ b<:a∈k σ∈Γ)

    -- Helpers (to satisfy the termination checker).

    kd-/-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {j k σ} →
              kd j ∷ Γ ⊢ k kd → Δ ⊢/ σ ∈ Γ → Δ ⊢ kd (j A.Kind/ σ) wf
    kd-/-wf (kd-⋯ a∈* _)  σ∈Γ = Tp∈-/-wf a∈* σ∈Γ
    kd-/-wf (kd-Π j-kd _) σ∈Γ = kd-/-wf j-kd σ∈Γ

    Tp∈-/-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a j k σ} →
               kd j ∷ Γ ⊢Tp a ∈ k → Δ ⊢/ σ ∈ Γ → Δ ⊢ kd (j A.Kind/ σ) wf
    Tp∈-/-wf (∈-var x (wf-kd k-kd ∷ Γ-ctx) _) σ∈Γ = wf-kd (kd-/ k-kd σ∈Γ)
    Tp∈-/-wf (∈-⊥-f (wf-kd j-kd ∷ Γ-ctx)) σ∈Γ = wf-kd (kd-/ j-kd σ∈Γ)
    Tp∈-/-wf (∈-⊤-f (wf-kd j-kd ∷ Γ-ctx)) σ∈Γ = wf-kd (kd-/ j-kd σ∈Γ)
    Tp∈-/-wf (∈-∀-f k-kd _)      σ∈Γ = kd-/-wf k-kd σ∈Γ
    Tp∈-/-wf (∈-→-f a∈* _)       σ∈Γ = Tp∈-/-wf a∈* σ∈Γ
    Tp∈-/-wf (∈-Π-i j-kd _)      σ∈Γ = kd-/-wf j-kd σ∈Γ
    Tp∈-/-wf (∈-Π-e a∈Πjk _)     σ∈Γ = Tp∈-/-wf a∈Πjk σ∈Γ
    Tp∈-/-wf (∈-s-i a∈b⋯c)       σ∈Γ = Tp∈-/-wf a∈b⋯c σ∈Γ
    Tp∈-/-wf (∈-⇑ a∈b _)         σ∈Γ = Tp∈-/-wf a∈b σ∈Γ

    <:-/-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b j k σ} →
              kd j ∷ Γ ⊢ a <: b ∈ k → Δ ⊢/ σ ∈ Γ → Δ ⊢ kd (j A.Kind/ σ) wf
    <:-/-wf (<:-refl a∈k)        σ∈Γ = Tp∈-/-wf a∈k σ∈Γ
    <:-/-wf (<:-trans a<:b _)    σ∈Γ = <:-/-wf a<:b σ∈Γ
    <:-/-wf (<:-β₁ _ b∈j)        σ∈Γ = Tp∈-/-wf b∈j σ∈Γ
    <:-/-wf (<:-β₂ _ b∈j)        σ∈Γ = Tp∈-/-wf b∈j σ∈Γ
    <:-/-wf (<:-η₁ a∈Πjk)        σ∈Γ = Tp∈-/-wf a∈Πjk σ∈Γ
    <:-/-wf (<:-η₂ a∈Πjk)        σ∈Γ = Tp∈-/-wf a∈Πjk σ∈Γ
    <:-/-wf (<:-⊥ a∈b⋯c)         σ∈Γ = Tp∈-/-wf a∈b⋯c σ∈Γ
    <:-/-wf (<:-⊤ a∈b⋯c)         σ∈Γ = Tp∈-/-wf a∈b⋯c σ∈Γ
    <:-/-wf (<:-∀ j₂<∷j₁ _ _)    σ∈Γ = <∷-/-wf j₂<∷j₁ σ∈Γ
    <:-/-wf (<:-→ a₂<:a₁∈* _)    σ∈Γ = <:-/-wf a₂<:a₁∈* σ∈Γ
    <:-/-wf (<:-λ _ Λj₁a₂∈Πjk _) σ∈Γ = Tp∈-/-wf Λj₁a₂∈Πjk σ∈Γ
    <:-/-wf (<:-· a₁<:a₂∈Πjk _)  σ∈Γ = <:-/-wf a₁<:a₂∈Πjk σ∈Γ
    <:-/-wf (<:-⟨| a∈b⋯c)        σ∈Γ = Tp∈-/-wf a∈b⋯c σ∈Γ
    <:-/-wf (<:-|⟩ a∈b⋯c)        σ∈Γ = Tp∈-/-wf a∈b⋯c σ∈Γ
    <:-/-wf (<:-⋯-i a<:b∈c⋯d)    σ∈Γ = <:-/-wf a<:b∈c⋯d σ∈Γ
    <:-/-wf (<:-⇑ a<:b∈k _)      σ∈Γ = <:-/-wf a<:b∈k σ∈Γ

    <∷-/-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {j k l σ} →
              kd j ∷ Γ ⊢ k <∷ l → Δ ⊢/ σ ∈ Γ → Δ ⊢ kd (j A.Kind/ σ) wf
    <∷-/-wf (<∷-⋯ j₂<:j₁ _)   σ∈Γ = <:-/-wf j₂<:j₁ σ∈Γ
    <∷-/-wf (<∷-Π j₂<∷j₁ _ _) σ∈Γ = <∷-/-wf j₂<∷j₁ σ∈Γ

  -- Substitutions preserve well-formedness of ascriptions.
  wf-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a σ} →
         Γ ⊢ a wf → Δ ⊢/ σ ∈ Γ → Δ ⊢ a A.TermAsc/ σ wf
  wf-/ (wf-kd k-kd) σ∈Γ = wf-kd (kd-/ k-kd σ∈Γ)
  wf-/ (wf-tp a∈b)  σ∈Γ = wf-tp (Tp∈-/ a∈b σ∈Γ)

  -- Substitutions commute with kind equality.
  ≅-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {j k σ} →
        Γ ⊢ j ≅ k → Δ ⊢/ σ ∈ Γ → Δ ⊢ j A.Kind/ σ ≅ k A.Kind/ σ
  ≅-/ (<∷-antisym j<∷k k<∷j) σ∈Γ = <∷-antisym (<∷-/ j<∷k σ∈Γ) (<∷-/ k<∷j σ∈Γ)

  -- Substitutions preserve well-typedness of terms.
  Tm∈-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b σ} →
          Γ ⊢Tm a ∈ b → Δ ⊢/ σ ∈ Γ → Δ ⊢Tm a A./ σ ∈ b A./ σ
  Tm∈-/ (∈-var x Γ-ctx Γ[x]=tp-k) σ∈Γ =
    liftTm (cong (_/ _) Γ[x]=tp-k) (/∈-lookup σ∈Γ x)
  Tm∈-/ (∈-∀-i k-kd a∈*)          σ∈Γ =
    ∈-∀-i k/σ-kd (Tm∈-/ a∈* (∈-↑ (wf-kd k/σ-kd) σ∈Γ))
    where k/σ-kd = kd-/ k-kd σ∈Γ
  Tm∈-/ (∈-→-i {c = c} a∈* b∈c c∈*) σ∈Γ =
    ∈-→-i a/σ∈* (subst (_ ⊢Tm _ ∈_) (sym (weaken-/ c) ) b/σ↑∈c)
          (Tp∈-/ c∈* σ∈Γ)
    where
      a/σ∈*  = Tp∈-/ a∈* σ∈Γ
      b/σ↑∈c = Tm∈-/ b∈c (∈-↑ (wf-tp a/σ∈*) σ∈Γ)
  Tm∈-/ (∈-∀-e {c = c} a∈∀kc b∈k) σ∈Γ =
    subst (_ ⊢Tm _ ∈_) (sym (/-sub-↑ c _ _))
          (∈-∀-e (Tm∈-/ a∈∀kc σ∈Γ) (Tp∈-/ b∈k σ∈Γ))
  Tm∈-/ (∈-→-e a∈c→d b∈c)         σ∈Γ = ∈-→-e (Tm∈-/ a∈c→d σ∈Γ) (Tm∈-/ b∈c σ∈Γ)
  Tm∈-/ (∈-⇑ a∈b b<:c)            σ∈Γ = ∈-⇑ (Tm∈-/ a∈b σ∈Γ) (<:-/ b<:c σ∈Γ)

  -- Substitutions preserve well-kindedness and well-typedness.
  ∈-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b σ} →
        Γ ⊢ a ∈ b → Δ ⊢/ σ ∈ Γ → Δ ⊢ a A./ σ ∈ b A.TermAsc/ σ
  ∈-/ (∈-tp a∈b) σ∈Γ = ∈-tp (Tp∈-/ a∈b σ∈Γ)
  ∈-/ (∈-tm a∈b) σ∈Γ = ∈-tm (Tm∈-/ a∈b σ∈Γ)

  -- Substitutions preserve subkinding and subtyping.
  ≤-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b σ} →
        Γ ⊢ a ≤ b → Δ ⊢/ σ ∈ Γ → Δ ⊢ a A.TermAsc/ σ ≤ b A.TermAsc/ σ
  ≤-/ (≤-<∷ a<∷b)   σ∈Γ = ≤-<∷ (<∷-/ a<∷b σ∈Γ)
  ≤-/ (≤-<: a<:b∈k) σ∈Γ = ≤-<: (<:-/ a<:b∈k σ∈Γ)

  -- Substitutions preserve equality of kind and type ascriptions.
  ≃wf-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b σ} →
          Γ ⊢ a ≃ b wf → Δ ⊢/ σ ∈ Γ → Δ ⊢ a A.TermAsc/ σ ≃ b A.TermAsc/ σ wf
  ≃wf-/ (≃wf-≅ j≅k) σ∈Γ = ≃wf-≅ (≅-/ j≅k σ∈Γ)
  ≃wf-/ (≃wf-≃ a≃b) σ∈Γ = ≃wf-≃ (≃-/ a≃b σ∈Γ)

-- Well-kinded/typed type and term substitutions.
module TypedSubstitution where
  open Substitution           using (simple; termSubst)
  open SimpleExt    simple    using (extension)
  open TermSubst    termSubst using (varLift; termLift)

  private
    module S  = Substitution
    module KL = TermLikeLemmas S.termLikeLemmasKind

  -- Helper lemmas about untyped renamings and substitutions in terms
  -- and kinds.

  varHelpers : TypedSubstAppHelpers varLift
  varHelpers = record
    { Kind/-sub-↑ = KL./-sub-↑
    ; /-sub-↑     = LiftSubLemmas./-sub-↑ S.varLiftSubLemmas
    ; weaken-/    = LiftAppLemmas.wk-commutes S.varLiftAppLemmas
    }

  termHelpers : TypedSubstAppHelpers termLift
  termHelpers = record
    { Kind/-sub-↑ = λ k _ _ → KL.sub-commutes k
    ; /-sub-↑     = λ a _ _ → S.sub-commutes a
    ; weaken-/    = S.weaken-/
    }

  -- Typed term substitutions.

  typedTermSubst : TypedTermSubst TermAsc Term lzero TypedSubstAppHelpers
  typedTermSubst = record
    { _⊢_wf = _⊢_wf
    ; _⊢_∈_ = _⊢_∈_
    ; termLikeLemmas = S.termLikeLemmasTermAsc
    ; varHelpers     = varHelpers
    ; termHelpers    = termHelpers
    ; wf-wf    = wf-ctx
    ; ∈-wf     = ∈-ctx
    ; ∈-var    = ∈-var′
    ; typedApp = TypedSubstApp.∈-/
    }
  open TypedTermSubst typedTermSubst public
    hiding (_⊢_wf; _⊢_∈_; varHelpers; termHelpers; ∈-var; ∈-/Var; ∈-/)
    renaming (lookup to /∈-lookup)
  open TypedSubstApp _⊢Var_∈_ varLiftTyped varHelpers public using () renaming
    ( wf-/  to wf-/Var
    ; kd-/  to kd-/Var
    ; Tp∈-/ to Tp∈-/Var
    ; <∷-/  to <∷-/Var
    ; <:-/  to <:-/Var
    ; ∈-/   to ∈-/Var
    ; ≤-/   to ≤-/Var
    ; ≃wf-/ to ≃wf-/Var
    )
  open Substitution using (weaken; weakenKind; weakenTermAsc)

  -- Weakening preserves the various judgments.

  wf-weaken : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a wf → Γ ⊢ b wf →
              (a ∷ Γ) ⊢ weakenTermAsc b wf
  wf-weaken a-wf b-wf = wf-/Var b-wf (Var∈-wk a-wf)

  kd-weaken : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢ a wf → Γ ⊢ k kd →
              (a ∷ Γ) ⊢ weakenKind k kd
  kd-weaken a-wf k-kd = kd-/Var k-kd (Var∈-wk a-wf)

  Tp∈-weaken : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a wf → Γ ⊢Tp b ∈ k →
               (a ∷ Γ) ⊢Tp weaken b ∈ weakenKind k
  Tp∈-weaken a-wf b∈k = Tp∈-/Var b∈k (Var∈-wk a-wf)

  <∷-weaken : ∀ {n} {Γ : Ctx n} {a j k} → Γ ⊢ a wf → Γ ⊢ j <∷ k →
              (a ∷ Γ) ⊢ weakenKind j <∷ weakenKind k
  <∷-weaken a-wf j<∷k = <∷-/Var j<∷k (Var∈-wk a-wf)

  <:-weaken : ∀ {n} {Γ : Ctx n} {a b c k} → Γ ⊢ a wf → Γ ⊢ b <: c ∈ k →
              (a ∷ Γ) ⊢ weaken b <: weaken c ∈ weakenKind k
  <:-weaken a-wf b<:c∈k = <:-/Var b<:c∈k (Var∈-wk a-wf)

  ∈-weaken : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢ a wf → Γ ⊢ b ∈ c →
             (a ∷ Γ) ⊢ weaken b ∈ weakenTermAsc c
  ∈-weaken a-wf b∈c = ∈-/Var b∈c (Var∈-wk a-wf)

  ≤-weaken : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢ a wf → Γ ⊢ b ≤ c →
             (a ∷ Γ) ⊢ weakenTermAsc b ≤ weakenTermAsc c
  ≤-weaken a-wf b≤c = ≤-/Var b≤c (Var∈-wk a-wf)

  ≃wf-weaken : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢ a wf → Γ ⊢ b ≃ c wf →
               (a ∷ Γ) ⊢ weakenTermAsc b ≃ weakenTermAsc c wf
  ≃wf-weaken a-wf b≃c = ≃wf-/Var b≃c (Var∈-wk a-wf)

  open TypedSubstApp _⊢_∈_ termLiftTyped termHelpers public
  open Substitution using (_/_; _Kind/_; id; sub; _↑⋆_; _[_]; _Kind[_])

  -- Substitution of a single well-typed term or well-kinded type
  -- preserves the various judgments.

  kd-[] : ∀ {n} {Γ : Ctx n} {a b k} →
          b ∷ Γ ⊢ k kd → Γ ⊢ a ∈ b → Γ ⊢ k Kind[ a ] kd
  kd-[] k-kd a∈b = kd-/ k-kd (∈-sub a∈b)

  Tp∈-[] : ∀ {n} {Γ : Ctx n} {a b k c} →
           c ∷ Γ ⊢Tp a ∈ k → Γ ⊢ b ∈ c → Γ ⊢Tp a [ b ] ∈ k Kind[ b ]
  Tp∈-[] a∈k b∈c = Tp∈-/ a∈k (∈-sub b∈c)

  Tm∈-[] : ∀ {n} {Γ : Ctx n} {a b c d} →
           d ∷ Γ ⊢Tm a ∈ c → Γ ⊢ b ∈ d → Γ ⊢Tm a [ b ] ∈ c [ b ]
  Tm∈-[] a∈c b∈d = Tm∈-/ a∈c (∈-sub b∈d)

  <:-[] : ∀ {n} {Γ : Ctx n} {a b c d k} →
          d ∷ Γ ⊢ a <: b ∈ k → Γ ⊢ c ∈ d → Γ ⊢ a [ c ] <: b [ c ] ∈ k Kind[ c ]
  <:-[] a<:b c∈d = <:-/ a<:b (∈-sub c∈d)

-- Operations on well-formed contexts that require weakening of
-- well-formedness judgments.

module WfCtxOps where
  wfWeakenOps : WellFormedWeakenOps weakenOps
  wfWeakenOps = record { wf-weaken = TypedSubstitution.wf-weaken }

  open WellFormedWeakenOps wfWeakenOps public renaming (lookup to lookup-wf)

  -- Lookup the kind of a type variable in a well-formed context.
  lookup-kd : ∀ {m} {Γ : Ctx m} {k} x →
              Γ ctx → TermCtx.lookup Γ x ≡ kd k → Γ ⊢ k kd
  lookup-kd x Γ-ctx Γ[x]≡kd-k =
    wf-kd-inv (subst (_ ⊢_wf) Γ[x]≡kd-k (lookup-wf Γ-ctx x))

  -- Lookup the type of a term variable in a well-formed context.
  lookup-tp : ∀ {m} {Γ : Ctx m} {a} x →
              Γ ctx → TermCtx.lookup Γ x ≡ tp a → Γ ⊢Tp a ∈ *
  lookup-tp x Γ-ctx Γ[x]≡tp-a =
    wf-tp-inv (subst (_ ⊢_wf) Γ[x]≡tp-a (lookup-wf Γ-ctx x))

open TypedSubstitution
open WfCtxOps

----------------------------------------------------------------------
-- Generation lemmas for kinding

-- A generation lemma for kinding of universals.

Tp∈-∀-inv : ∀ {n} {Γ : Ctx n} {a j k} → Γ ⊢Tp Π j a ∈ k →
            Γ ⊢ j kd × kd j ∷ Γ ⊢Tp a ∈ *
Tp∈-∀-inv (∈-∀-f j-kd a∈*) = j-kd , a∈*
Tp∈-∀-inv (∈-s-i ∀ka∈b⋯c)  = Tp∈-∀-inv ∀ka∈b⋯c
Tp∈-∀-inv (∈-⇑ ∀ja∈k k<∷l) = Tp∈-∀-inv ∀ja∈k

-- A generation lemma for kinding of arrows.

Tp∈-→-inv : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢Tp a ⇒ b ∈ k →
            Γ ⊢Tp a ∈ * × Γ ⊢Tp b ∈ *
Tp∈-→-inv (∈-→-f a∈* b∈*)  = a∈* , b∈*
Tp∈-→-inv (∈-s-i a⇒b∈c⋯d)  = Tp∈-→-inv a⇒b∈c⋯d
Tp∈-→-inv (∈-⇑ a⇒b∈j j<∷k) = Tp∈-→-inv a⇒b∈j

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


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

open import lib.Basics
open import lib.types.Paths

module lib.types.Torus where

{-
data Torus : Type₀ where
  baseT : Torus
  loopT1 : baseT == baseT
  loopT2 : baseT == baseT
  surfT : loopT1 ∙ loopT2 == loopT2 ∙ loopT1
-}

module _ where
  private
    data #Torus-aux : Type₀ where
      #baseT : #Torus-aux

    data #Torus : Type₀ where
      #torus : #Torus-aux → (Unit → Unit) → #Torus

  Torus : Type₀
  Torus = #Torus

  baseT : Torus
  baseT = #torus #baseT _

  postulate  -- HIT
    loopT1 : baseT == baseT
    loopT2 : baseT == baseT
    surfT : loopT1 ∙ loopT2 == loopT2 ∙ loopT1

  {- Dependent elimination and computation rules -}
  module TorusElim {i} {P : Torus → Type i} (baseT* : P baseT)
    (loopT1* : baseT* == baseT* [ P ↓ loopT1 ])
    (loopT2* : baseT* == baseT* [ P ↓ loopT2 ])
    (surfT* : loopT1* ∙ᵈ loopT2* == loopT2* ∙ᵈ loopT1*
              [ (λ p → baseT* == baseT* [ P ↓ p ]) ↓ surfT ]) where

    f : Π Torus P
    f = f-aux phantom  where

      f-aux : Phantom surfT* → Π Torus P
      f-aux phantom (#torus #baseT _) = baseT*

    postulate  -- HIT
      loopT1-β : apd f loopT1 == loopT1*
      loopT2-β : apd f loopT2 == loopT2*

    private
      lhs : apd f (loopT1 ∙ loopT2) == loopT1* ∙ᵈ loopT2*
      lhs =
        apd f (loopT1 ∙ loopT2)                   =⟨ apd-∙ f loopT1 loopT2 ⟩
        apd f loopT1 ∙ᵈ apd f loopT2            =⟨ loopT1-β |in-ctx (λ u → u ∙ᵈ apd f loopT2) ⟩
        loopT1* ∙ᵈ apd f loopT2                 =⟨ loopT2-β |in-ctx (λ u → loopT1* ∙ᵈ u) ⟩
        loopT1* ∙ᵈ loopT2* ∎

      rhs : apd f (loopT2 ∙ loopT1) == loopT2* ∙ᵈ loopT1*
      rhs =
        apd f (loopT2 ∙ loopT1)                   =⟨ apd-∙ f loopT2 loopT1 ⟩
        apd f loopT2 ∙ᵈ apd f loopT1            =⟨ loopT2-β |in-ctx (λ u → u ∙ᵈ apd f loopT1) ⟩
        loopT2* ∙ᵈ apd f loopT1                 =⟨ loopT1-β |in-ctx (λ u → loopT2* ∙ᵈ u) ⟩
        loopT2* ∙ᵈ loopT1* ∎

    postulate  -- HIT
      surfT-β : apd (apd f) surfT == lhs ◃ (surfT* ▹! rhs)

module TorusRec {i} {A : Type i} (baseT* : A) (loopT1* loopT2* : baseT* == baseT*)
  (surfT* : loopT1* ∙ loopT2* == loopT2* ∙ loopT1*) where

  private
    module M = TorusElim {P = λ _ → A} baseT* (↓-cst-in loopT1*) (↓-cst-in loopT2*)
                         (↓-cst-in-∙ loopT1 loopT2 loopT1* loopT2*
                         !◃ (↓-cst-in2 surfT* ▹ (↓-cst-in-∙ loopT2 loopT1 loopT2* loopT1*)))

  f : Torus → A
  f = M.f

  loopT1-β : ap f loopT1 == loopT1*
  loopT1-β = apd=cst-in {f = f} M.loopT1-β

  loopT2-β : ap f loopT2 == loopT2*
  loopT2-β = apd=cst-in {f = f} M.loopT2-β

  private
    lhs : ap f (loopT1 ∙ loopT2) == loopT1* ∙ loopT2*
    lhs =
      ap f (loopT1 ∙ loopT2)      =⟨ ap-∙ f loopT1 loopT2 ⟩
      ap f loopT1 ∙ ap f loopT2   =⟨ loopT1-β |in-ctx (λ u → u ∙ ap f loopT2) ⟩
      loopT1* ∙ ap f loopT2       =⟨ loopT2-β |in-ctx (λ u → loopT1* ∙ u) ⟩
      loopT1* ∙ loopT2* ∎

    rhs : ap f (loopT2 ∙ loopT1) == loopT2* ∙ loopT1*
    rhs =
      ap f (loopT2 ∙ loopT1)      =⟨ ap-∙ f loopT2 loopT1 ⟩
      ap f loopT2 ∙ ap f loopT1   =⟨ loopT2-β |in-ctx (λ u → u ∙ ap f loopT1) ⟩
      loopT2* ∙ ap f loopT1       =⟨ loopT1-β |in-ctx (λ u → loopT2* ∙ u) ⟩
      loopT2* ∙ loopT1* ∎

  postulate  -- Does not look easy
    surfT-β : ap (ap f) surfT == (lhs ∙ surfT*) ∙ (! rhs)
--  surfT-β = {!M.surfT-β!}

-- module TorusRecType {i} (baseT* : Type i) (loopT1* loopT2* : baseT* ≃ baseT*)
--   (surfT* : (x : baseT*) → –> loopT2* (–> loopT2* x) == –> loopT1* (–> loopT2* x)) where

--   open TorusRec baseT* (ua loopT1*) (ua loopT2*) {!!} public
--   -- TODO

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

module Experiment.SumFin where

open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

private
  variable
    k : ℕ

Fin : ℕ → Set
Fin zero    = ⊥
Fin (suc n) = ⊤ ⊎ (Fin n)

pattern fzero  = inj₁ tt
pattern fsuc n = inj₂ n

finj : Fin k → Fin (suc k)
finj {suc k} fzero    = fzero
finj {suc k} (fsuc n) = fsuc (finj {k} n)

toℕ : Fin k → ℕ
toℕ {suc k} (inj₁ tt) = zero
toℕ {suc k} (inj₂ x)  = suc (toℕ {k} x)

toℕ-injective : {m n : Fin k} → toℕ m ≡ toℕ n → m ≡ n
toℕ-injective {suc k} {fzero}  {fzero}  _ = refl
toℕ-injective {suc k} {fzero} {fsuc x} ()
toℕ-injective {suc k} {fsuc m} {fzero} ()
toℕ-injective {suc k} {fsuc m} {fsuc x} p = cong fsuc (toℕ-injective (suc-injective p))


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

open import HoTT

module homotopy.TorusIsProductCircles where

surfT' : loopT1 ∙ loopT2 == loopT2 ∙' loopT1
surfT' = surfT ∙ (∙=∙' loopT2 loopT1)

private
  to-surfT : (pair×= loop idp) ∙ (pair×= idp loop)
             == (pair×= idp loop) ∙ (pair×= loop idp)
  to-surfT =
    pair×= loop idp ∙ pair×= idp loop   =⟨ ×-∙ loop idp idp loop ⟩
    pair×= (loop ∙ idp) (idp ∙ loop)    =⟨ ∙-unit-r loop |in-ctx (λ u → pair×= u loop) ⟩
    pair×= loop loop                    =⟨ ! (∙-unit-r loop) |in-ctx (λ u → pair×= loop u) ⟩
    pair×= (idp ∙ loop) (loop ∙ idp)    =⟨ ! (×-∙ idp loop loop idp) ⟩
    pair×= idp loop ∙ pair×= loop idp ∎

module To = TorusRec (base , base) (pair×= loop idp) (pair×= idp loop) to-surfT

{- First map -}
to : Torus → S¹ × S¹
to = To.f

{- Second map -}

from-c : S¹ → (S¹ → Torus)
from-c = FromC.f module M2 where

  module FromCBase = S¹Rec baseT loopT2

  from-c-base : S¹ → Torus
  from-c-base = FromCBase.f

  from-c-loop-loop' : loopT1 ∙ ap from-c-base loop =-= ap from-c-base loop ∙' loopT1
  from-c-loop-loop' =
    loopT1 ∙ ap from-c-base loop   =⟪ FromCBase.loop-β |in-ctx (λ u → loopT1 ∙ u) ⟫
    loopT1 ∙ loopT2                =⟪ surfT' ⟫
    loopT2 ∙' loopT1               =⟪ ! FromCBase.loop-β |in-ctx (λ u → u ∙' loopT1) ⟫
    ap from-c-base loop ∙' loopT1 ∎∎

  from-c-loop-loop : loopT1 == loopT1 [ (λ x → from-c-base x == from-c-base x) ↓ loop ]
  from-c-loop-loop = ↓-='-in (↯ from-c-loop-loop')

  module FromCLoop = S¹Elim loopT1 from-c-loop-loop

  from-c-loop' = FromCLoop.f
  from-c-loop = λ= from-c-loop'

  module FromC = S¹Rec from-c-base from-c-loop

from : S¹ × S¹ → Torus
from (x , y) = from-c x y

open M2

{- First composition -}

thing : (y : S¹) → ap (λ x → from-c x y) loop == from-c-loop' y
thing y =
  ap ((λ u → u y) ∘ from-c) loop   =⟨ ap-∘ (λ u → u y) from-c loop ⟩
  app= (ap from-c loop) y          =⟨ FromC.loop-β |in-ctx (λ u → app= u y)⟩
  app= (λ= from-c-loop') y         =⟨ app=-β from-c-loop' y ⟩
  from-c-loop' y ∎

to-from-c : (x y : S¹) → to (from-c x y) == (x , y)
to-from-c = {!!} --S¹-elim to-from-c-base (↓-cst→app-in to-from-c-loop)
  where

  to-from-c-base-loop' : ap (to ∘ from-c-base) loop =-= ap (λ y → (base , y)) loop
  to-from-c-base-loop' =
    ap (to ∘ from-c-base) loop    =⟪ ap-∘ to from-c-base loop ⟫
    ap to (ap from-c-base loop)   =⟪ FromCBase.loop-β |in-ctx ap to ⟫
    ap to loopT2                  =⟪ To.loopT2-β ⟫
    pair×= idp loop               =⟪ ! (ap-cst,id _ loop) ⟫
    ap (λ y → (base , y)) loop ∎∎

  to-from-c-base-loop : idp == idp [ (λ z → to (from-c-base z) == (base , z)) ↓ loop ]
  to-from-c-base-loop = ↓-='-in (! (↯ to-from-c-base-loop'))

  module ToFromCBase = S¹Elim idp to-from-c-base-loop

  -- 1!to-from-c-base-loop : idp == idp [ (λ z → to (from-c-base (fst z)) == z) ↓ (pair×= loop idp) ]
  -- 1!to-from-c-base-loop = ↓-='-in (! (↯ 1! to-from-c-base-loop'))

--   module 1!ToFromCBase!1 = S¹Elim idp 1!to-from-c-base-loop

  to-from-c-base : (y : S¹) → to (from-c-base y) == (base , y)
  to-from-c-base = ToFromCBase.f

  thing2 : (y : S¹) → ap to (from-c-loop' y) == to-from-c-base y ∙ pair×= loop idp ∙' (! (to-from-c-base y))
  thing2 = {!S¹-elim To.loopT1-β {!To.loopT1-β!}!}

  to-from-c-loop : (y : S¹) → to-from-c-base y == to-from-c-base y [ (λ x → to (from-c x y) == (x , y)) ↓ loop ]
  to-from-c-loop = {!S¹-elim to-from-c-loop-base ?!}  where

    to-from-c-loop-base2 : ap (λ x → (x , base)) loop =-= ap (λ x → to (from-c x base)) loop
    to-from-c-loop-base2 =
      ap (λ z → z , base) loop               =⟪ {!ap-id,cst _ loop!} ⟫
      pair×= loop idp                        =⟪ ! To.loopT1-β ⟫
      ap to loopT1                           =⟪ ! (thing base) |in-ctx ap to ⟫
      ap to (ap (λ z → from-c z base) loop)  =⟪ ! (ap-∘ to (λ z → from-c z base) loop) ⟫
      ap (λ z → to (from-c z base)) loop ∎∎

    to-from-c-loop-base : idp == idp [ (λ x → to (from-c x base) == (x , base)) ↓ loop ]
    to-from-c-loop-base = ↓-='-in (↯ to-from-c-loop-base2)

    lemma : ↯ to-from-c-loop-base2 == ↯ to-from-c-loop-base2 [ (λ y → to-from-c-base y ∙ ap (λ x → x , y) loop == ap (λ x → to (from-c x y)) loop ∙' to-from-c-base y) ↓ loop ]
    lemma = ↓-=-in (
      (↯ to-from-c-loop-base2) ◃ apd (λ y → ap (λ x → to (from-c x y)) loop ∙' to-from-c-base y) loop  =⟨ {!!} ⟩
      (↯ to-from-c-loop-base2) ◃ ((apd (λ y → ap (λ x → to (from-c x y)) loop) loop) ∙'2 (apd to-from-c-base loop)) =⟨ {!!} ⟩
      ((↯ to-from-c-loop-base2) ◃ (apd (λ y → ap (λ x → to (from-c x y)) loop) loop)) ∙'2 (apd to-from-c-base loop) =⟨ {!!} ⟩
      ((↯ (to-from-c-loop-base2 !1)) ◃ ((apd (λ y → ap to (ap (λ x → from-c x y) loop)) loop) ▹ (↯ to-from-c-loop-base2 #1))) ∙'2 (apd to-from-c-base loop) =⟨ {!!} ⟩
      ((↯ (to-from-c-loop-base2 !2)) ◃ ((apd (λ y → ap to (from-c-loop' y)) loop) ▹ (↯ to-from-c-loop-base2 #2))) ∙'2 (apd to-from-c-base loop) =⟨ {!!} ⟩
      ((↯ (to-from-c-loop-base2 !2)) ◃ ((ap↓ (ap to) (apd from-c-loop' loop)) ▹ (↯ to-from-c-loop-base2 #2))) ∙'2 (apd to-from-c-base loop) =⟨ {!!} ⟩
      ((↯ (to-from-c-loop-base2 !2)) ◃ ((ap↓ (ap to) from-c-loop-loop) ▹ (↯ to-from-c-loop-base2 #2))) ∙'2 (apd to-from-c-base loop) =⟨ {!!} ⟩
      apd (λ y → to-from-c-base y ∙ ap (λ x → x , y) loop) loop ▹ (↯ to-from-c-loop-base2) ∎)

{-
Have: PathOver (λ z → to (from-c-base z) == to (from-c-base z))
      loop (ap (λ x → x , base) loop)
      (ap (λ x → to (from-c x base)) loop)

-}

    -- lemma2 : apd (λ y → ap (λ x → to (from-c x y)) loop) loop == {!!}
    -- lemma2 =
    --   apd (λ y → ap (λ x → to (from-c x y)) loop) loop   =⟨ {!!} ⟩
    --   apd (λ y → ap to (ap (λ x → from-c x y) loop)) loop   =⟨ {!!} ⟩
    --   apd (λ y → ap to (from-c-loop' y)) loop   =⟨ {!!} ⟩
    --   api2 (ap to) (apd from-c-loop' loop)   =⟨ {!!} ⟩
    --   apd (ap to) surfT   =⟨ {!!} ⟩
    --   ? ∎

to-from : (x : S¹ × S¹) → to (from x) == x
to-from (x , y) = to-from-c x y

{- Second composition -}

from-to : (x : Torus) → from (to x) == x
from-to = {!Torus-elim idp from-to-loopT1 from-to-loopT2 {!!}!}
  where

  from-to-loopT1 : idp == idp [ (λ z → from (to z) == z) ↓ loopT1 ]
  from-to-loopT1 = ↓-∘=idf-in from to
    (ap from (ap to loopT1)                =⟨ To.loopT1-β |in-ctx ap from ⟩
    ap from (pair×= loop idp)             =⟨ lemma from loop (idp {a = base}) ⟩
    ap (λ u → u base) (ap from-c loop)    =⟨ FromC.loop-β |in-ctx ap (λ u → u base) ⟩
    ap (λ u → u base) (λ= from-c-loop')   =⟨ app=-β from-c-loop' base ⟩
    loopT1 ∎)  where

      lemma : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : A × B → C)
        {x y : A} (p : x == y) {z t : B} (q : z == t)
        → ap f (pair×= p q) == app= (ap (curry f) p) z ∙' ap (curry f y) q
      lemma f idp idp = idp

  from-to-loopT2 : idp == idp [ (λ z → from (to z) == z) ↓ loopT2 ]
  from-to-loopT2 = ↓-∘=idf-in from to
    (ap from (ap to loopT2)                =⟨ To.loopT2-β |in-ctx ap from ⟩
    ap from (pair×= idp loop)             =⟨ lemma' from (idp {a = base}) loop ⟩
    ap from-c-base loop    =⟨ FromCBase.loop-β ⟩
    loopT2 ∎)  where

      lemma' : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : A × B → C)
        {x y : A} (p : x == y) {z t : B} (q : z == t)
        → ap f (pair×= p q) == ap (curry f x) q ∙' app= (ap (curry f) p) t
      lemma' f idp idp = idp

-- to-from-c-app-base : (y : S¹) → to (from-c y base) == (y , base)
-- to-from-c-app-base = S¹-elim {!to (from-c base base) == base , base!} {!!}


text:
open import Common.Prelude
open import Common.Reflection

{-# NON_TERMINATING #-}
-- Note that in the body of the unquote, 'loop' really means 'quote loop'.
unquoteDecl loop =
  define (vArg loop)
         (funDef (def (quote Nat) [])
                 (clause [] (def loop []) ∷ []))

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


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

open import lib.Basics
open import lib.types.Empty
open import lib.types.Sigma
open import lib.types.Paths

module lib.types.Pi where

instance
  Π-level : ∀ {i j} {A : Type i} {B : A → Type j} {n : ℕ₋₂}
    → ((x : A) → has-level n (B x)) → has-level n (Π A B)
  Π-level {n = ⟨-2⟩} p = has-level-in ((λ x → contr-center (p x)) , lemma)
    where abstract lemma = λ f → λ= (λ x → contr-path (p x) (f x))
  Π-level {n = S n} p = has-level-in lemma where
    abstract
      lemma = λ f g →
        equiv-preserves-level λ=-equiv {{Π-level (λ x → has-level-apply (p x) (f x) (g x))}}

  Πi-level : ∀ {i j} {A : Type i} {B : A → Type j} {n : ℕ₋₂}
    → ((x : A) → has-level n (B x)) → has-level n ({x : A} → B x)
  Πi-level {A = A} {B} p = equiv-preserves-level e {{Π-level p}}  where

    e : Π A B ≃ ({x : A} → B x)
    fst e f {x} = f x
    is-equiv.g (snd e) f x = f
    is-equiv.f-g (snd e) _ = idp
    is-equiv.g-f (snd e) _ = idp
    is-equiv.adj (snd e) _ = idp

{- Equivalences in a Π-type -}
Π-emap-l : ∀ {i j k} {A : Type i} {B : Type j} (P : B → Type k)
            → (e : A ≃ B) → Π A (P ∘ –> e) ≃ Π B P
Π-emap-l {A = A} {B = B} P e = equiv f g f-g g-f where
  f : Π A (P ∘ –> e) → Π B P
  f u b = transport P (<–-inv-r e b) (u (<– e b))

  g : Π B P → Π A (P ∘ –> e)
  g v a = v (–> e a)

  abstract
    f-g : ∀ v → f (g v) == v
    f-g v = λ= λ b → to-transp (apd v (<–-inv-r e b))

    g-f : ∀ u → g (f u) == u
    g-f u = λ= λ a → to-transp $ transport (λ p → u _ == _ [ P ↓ p ])
                                           (<–-inv-adj e a)
                                           (↓-ap-in P (–> e)
                                                      (apd u $ <–-inv-l e a))

Π-emap-r : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  → (∀ x → B x ≃ C x) → Π A B ≃ Π A C
Π-emap-r {A = A} {B = B} {C = C} k = equiv f g f-g g-f
  where f : Π A B → Π A C
        f c x = –> (k x) (c x)

        g : Π A C → Π A B
        g d x = <– (k x) (d x)

        abstract
          f-g : ∀ d → f (g d) == d
          f-g d = λ= (λ x →  <–-inv-r (k x) (d x))

          g-f : ∀ c → g (f c) == c
          g-f c = λ= (λ x → <–-inv-l (k x) (c x))

{-
favonia: This part is not used.

module _ {i₀ i₁ j₀ j₁} {A₀ : Type i₀} {A₁ : Type i₁}
         {B₀ : A₀ → Type j₀} {B₁ : A₁ → Type j₁} where
  Π-emap : (u : A₀ ≃ A₁) (v : ∀ a → B₀ (<– u a) ≃ B₁ a) → Π A₀ B₀ ≃ Π A₁ B₁
  Π-emap u v = Π A₀ B₀           ≃⟨ Π-emap-l _ (u ⁻¹) ⁻¹ ⟩
               Π A₁ (B₀ ∘ <– u)  ≃⟨ Π-emap-r v ⟩
               Π A₁ B₁           ≃∎

  Π-emap' : (u : A₀ ≃ A₁) (v : ∀ a → B₀ a ≃ B₁ (–> u a)) → Π A₀ B₀ ≃ Π A₁ B₁
  Π-emap' u v = Π A₀ B₀           ≃⟨ Π-emap-r v ⟩
                Π A₀ (B₁ ∘ –> u)  ≃⟨ Π-emap-l _ u ⟩
                Π A₁ B₁           ≃∎
-}

{- Coversions between functions with implicit and explicit arguments -}

expose-equiv : ∀ {i j} {A : Type i} {B : A → Type j}
  → ({x : A} → B x) ≃ ((x : A) → B x)
expose-equiv = (λ f a → f {a}) , is-eq
  _
  (λ f {a} → f a)
  (λ _ → idp)
  (λ _ → idp)

{- Dependent paths in a Π-type -}
module _ {i j k} {A : Type i} {B : A → Type j} {C : (a : A) → B a → Type k}
  where

  ↓-Π-in : {x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}
    → ({t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
        → u t == u' t' [ uncurry C ↓ pair= p q ])
    → (u == u' [ (λ x → Π (B x) (C x)) ↓ p ])
  ↓-Π-in {p = idp} f = λ= (λ x → f (idp {a = x}))

  ↓-Π-out : {x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}
    → (u == u' [ (λ x → Π (B x) (C x)) ↓ p ])
    → ({t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
        → u t == u' t' [ uncurry C ↓ pair= p q ])
  ↓-Π-out {p = idp} q idp = app= q _

  ↓-Π-β : {x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}
    → (f : {t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
            → u t == u' t' [ uncurry C ↓ pair= p q ])
    → {t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
    → ↓-Π-out (↓-Π-in f) q == f q
  ↓-Π-β {p = idp} f idp = app=-β (λ x → f (idp {a = x})) _

  ↓-Π-η : {x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}
    → (q : (u == u' [ (λ x → Π (B x) (C x)) ↓ p ]))
    → ↓-Π-in (↓-Π-out q) == q
  ↓-Π-η {p = idp} q = ! (λ=-η q)

  ↓-Π-equiv : {x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}
    → ({t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
        → u t == u' t' [ uncurry C ↓ pair= p q ])
    ≃ (u == u' [ (λ x → Π (B x) (C x)) ↓ p ])
  ↓-Π-equiv {p = idp} = equiv ↓-Π-in ↓-Π-out ↓-Π-η
    (λ u → <– (ap-equiv expose-equiv _ _)
      (λ= (λ t → <– (ap-equiv expose-equiv _ _)
        (λ= (λ t' → λ= (↓-Π-β u))))))

{- Dependent paths in a Π-type where the codomain is not dependent on anything

Right now, this is defined in terms of the previous one. Maybe it’s a good idea,
maybe not.
-}
module _ {i j k} {A : Type i} {B : A → Type j} {C : Type k} {x x' : A}
  {p : x == x'} {u : B x → C} {u' : B x' → C} where

  ↓-app→cst-in :
    ({t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
      → u t == u' t')
    → (u == u' [ (λ x → B x → C) ↓ p ])
  ↓-app→cst-in f = ↓-Π-in (λ q → ↓-cst-in (f q))

  ↓-app→cst-out :
    (u == u' [ (λ x → B x → C) ↓ p ])
    → ({t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
        → u t == u' t')
  ↓-app→cst-out r q = ↓-cst-out (↓-Π-out r q)

  ↓-app→cst-β :
    (f : ({t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
           → u t == u' t'))
    → {t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
    → ↓-app→cst-out (↓-app→cst-in f) q == f q
  ↓-app→cst-β f q =
    ↓-app→cst-out (↓-app→cst-in f) q
             =⟨ idp ⟩
    ↓-cst-out (↓-Π-out (↓-Π-in (λ qq → ↓-cst-in (f qq))) q)
             =⟨ ↓-Π-β (λ qq → ↓-cst-in (f qq)) q |in-ctx
                      ↓-cst-out ⟩
    ↓-cst-out (↓-cst-in {p = pair= p q} (f q))
             =⟨ ↓-cst-β (pair= p q) (f q) ⟩
    f q =∎

{- favonia: these lemmas are not used anywhere

{- Similar to above, with domain being the identity function. -}
{- These lemmas were in homotopy.FunctionOver and in different conventions. -}

module _ {i j} {A B : Type i} {C : Type j}
  {u : A → C} {v : B → C} where

  ↓-idf→cst-in : ∀ (p : A == B)
    → u == v ∘ coe p
    → u == v [ (λ x → x → C) ↓ p ]
  ↓-idf→cst-in idp q = q

  ↓-idf→cst-ua-in : ∀ (e : A ≃ B)
    → u == v ∘ –> e
    → u == v [ (λ x → x → C) ↓ ua e ]
  ↓-idf→cst-ua-in e q = ↓-idf→cst-in (ua e) (q ∙ ap (v ∘_) (λ= λ a → ! (coe-β e a)))

  ↓-idf→cst-in' : ∀ (p : A == B)
    → u ∘ coe! p == v
    → u == v [ (λ x → x → C) ↓ p ]
  ↓-idf→cst-in' idp q = q

  ↓-idf→cst-ua-in' : ∀ (e : A ≃ B)
    → u ∘ <– e == v
    → u == v [ (λ x → x → C) ↓ ua e ]
  ↓-idf→cst-ua-in' e q = ↓-idf→cst-in' (ua e) (ap (u ∘_) (λ= λ a → coe!-β e a) ∙ q)

module _ {i j} {A B : Type i} {C : Type j}
  {u : C → A} {v : C → B} where

  ↓-cst→idf-in : ∀ (p : A == B)
    → coe p ∘ u == v
    → u == v [ (λ x → C → x) ↓ p ]
  ↓-cst→idf-in idp q = q

  ↓-cst→idf-ua-in : ∀ (e : A ≃ B)
    → –> e ∘ u == v
    → u == v [ (λ x → C → x) ↓ ua e ]
  ↓-cst→idf-ua-in e q = ↓-cst→idf-in (ua e) (ap (_∘ u) (λ= λ a → coe-β e a) ∙ q)

  ↓-cst→idf-in' : ∀ (p : A == B)
    → u == coe! p ∘ v
    → u == v [ (λ x → C → x) ↓ p ]
  ↓-cst→idf-in' idp q = q

  ↓-cst→idf-ua-in' : ∀ (e : A ≃ B)
    → u == <– e ∘ v
    → u == v [ (λ x → C → x) ↓ ua e ]
  ↓-cst→idf-ua-in' e q = ↓-cst→idf-in' (ua e) (q ∙ ap (_∘ v) (λ= λ a → ! (coe!-β e a)))
-}

{- Dependent paths in an arrow type -}
module _ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  {x x' : A} {p : x == x'} {u : B x → C x} {u' : B x' → C x'} where

  ↓-→-in :
    ({t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
      → u t == u' t' [ C ↓ p ])
    → (u == u' [ (λ x → B x → C x) ↓ p ])
  ↓-→-in f = ↓-Π-in (λ q → ↓-cst2-in p q (f q))

  ↓-→-out :
    (u == u' [ (λ x → B x → C x) ↓ p ])
    → ({t : B x} {t' : B x'} (q : t == t' [ B ↓ p ])
      → u t == u' t' [ C ↓ p ])
  ↓-→-out r q = ↓-cst2-out p q (↓-Π-out r q)

{- Transport form of dependent path in an arrow type -}
module _ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k} where

  ↓-→-from-transp : {x x' : A} {p : x == x'}
    {u : B x → C x} {u' : B x' → C x'}
    → transport C p ∘ u == u' ∘ transport B p
    → u == u' [ (λ x → B x → C x) ↓ p ]
  ↓-→-from-transp {p = idp} q = q

  ↓-→-to-transp : {x x' : A} {p : x == x'}
    {u : B x → C x} {u' : B x' → C x'}
    → u == u' [ (λ x → B x → C x) ↓ p ]
    → transport C p ∘ u == u' ∘ transport B p
  ↓-→-to-transp {p = idp} q = q

-- Dependent paths in a Π-type where the domain is constant
module _ {i j k} {A : Type i} {B : Type j} {C : A → B → Type k} where

  ↓-Π-cst-app-in : {x x' : A} {p : x == x'}
    {u : (b : B) → C x b} {u' : (b : B) → C x' b}
    → ((b : B) → u b == u' b [ (λ x → C x b) ↓ p ])
    → (u == u' [ (λ x → (b : B) → C x b) ↓ p ])
  ↓-Π-cst-app-in {p = idp} f = λ= f

  ↓-Π-cst-app-out : {x x' : A} {p : x == x'}
    {u : (b : B) → C x b} {u' : (b : B) → C x' b}
    → (u == u' [ (λ x → (b : B) → C x b) ↓ p ])
    → ((b : B) → u b == u' b [ (λ x → C x b) ↓ p ])
  ↓-Π-cst-app-out {p = idp} q = app= q

split-ap2 : ∀ {i j k} {A : Type i} {B : A → Type j} {C : Type k} (f : Σ A B → C)
  {x y : A} (p : x == y)
  {u : B x} {v : B y} (q : u == v [ B ↓ p ])
  → ap f (pair= p q) == ↓-app→cst-out (apd (curry f) p) q
split-ap2 f idp idp = idp

{-
Interaction of [apd] with function composition.
The basic idea is that [apd (g ∘ f) p == apd g (apd f p)] but the version here
is well-typed. Note that we assume a propositional equality [r] between
[apd f p] and [q].
-}
apd-∘ : ∀ {i j k} {A : Type i} {B : A → Type j} {C : (a : A) → B a → Type k}
  (g : {a : A} → Π (B a) (C a)) (f : Π A B) {x y : A} (p : x == y)
  {q : f x == f y [ B ↓ p ]} (r : apd f p == q)
  → apd (g ∘ f) p == ↓-apd-out C r (apd↓ g q)
apd-∘ g f idp idp = idp

{- When [g] is nondependent, it’s much simpler -}
apd-∘' : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  (g : {a : A} → B a → C a) (f : Π A B) {x y : A} (p : x == y)
  → apd (g ∘ f) p == ap↓ g (apd f p)
apd-∘' g f idp = idp

∘'-apd : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  (g : {a : A} → B a → C a) (f : Π A B) {x y : A} (p : x == y)
  → ap↓ g (apd f p) == apd (g ∘ f) p
∘'-apd g f idp = idp

{- And when [f] is nondependent, it’s also a bit simpler -}
apd-∘'' : ∀ {i j k} {A : Type i} {B : Type j} {C : (b : B) → Type k}
  (g : Π B C) (f : A → B) {x y : A} (p : x == y)
  {q : f x == f y} (r : ap f p == q)
  → apd (g ∘ f) p == ↓-ap-out= C f p r (apd g q) --(apd↓ g q)
apd-∘'' g f idp idp = idp

{- 2-dimensional coherence conditions -}

-- lhs :
--   ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k} {f g : Π A B}
--   {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
--   (k : (u ◃ apd g p) == (apd f p ▹ v))
--   (h : {a : A} → B a → C a)
--   → ap h u ◃ apd (h ∘ g) p == ap↓ h (u ◃ apd g p)

-- rhs :
--   ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k} {f g : Π A B}
--   {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
--   (k : (u ◃ apd g p) == (apd f p ▹ v))
--   (h : {a : A} → B a → C a)
--   → ap↓ h (apd f p ▹ v) == apd (h ∘ f) p ▹ ap h v

-- ap↓-↓-=-in :
--   ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k} {f g : Π A B}
--   {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
--   (k : (u ◃ apd g p) == (apd f p ▹ v))
--   (h : {a : A} → B a → C a)
--   → ap↓ (λ {a} → ap (h {a = a})) (↓-=-in {p = p} {u = u} {v = v} k)
--   == ↓-=-in (lhs {f = f} {g = g} k h ∙ ap (ap↓ (λ {a} → h {a = a})) k
--                                      ∙ rhs {f = f} {g = g} k h)

{-
Commutation of [ap↓ (ap h)] and [↓-swap!]. This is "just" J, but it’s not as
easy as it seems.
-}

-- module Ap↓-swap! {i j k ℓ} {A : Type i} {B : Type j} {C : Type k}
--   {D : Type ℓ} (h : C → D) (f : A → C) (g : B → C)
--   {a a' : A} {p : a == a'} {b b' : B} {q : b == b'}
--   (r : f a == g b') (s : f a' == g b)
--   (t : r == s ∙ ap g q  [ (λ x → f x == g b') ↓ p ])
--   where

--   lhs : ap h (ap f p ∙' s) == ap (h ∘ f) p ∙' ap h s
--   lhs = ap-∙' h (ap f p) s ∙ (ap (λ u → u ∙' ap h s) (∘-ap h f p))

--   rhs : ap h (s ∙ ap g q) == ap h s ∙ ap (h ∘ g) q
--   rhs = ap-∙ h s (ap g q) ∙ (ap (λ u → ap h s ∙ u) (∘-ap h g q))

--   β : ap↓ (ap h) (↓-swap! f g r s t) ==
--               lhs ◃ ↓-swap! (h ∘ f) (h ∘ g) (ap h r) (ap h s) (ap↓ (ap h) t ▹ rhs)
--   β with a | a' | p | b | b' | q | r | s | t
--   β | a | .a | idp | b | .b | idp | r | s | t = coh r s t  where

--     T : {x x' : C} (r s : x == x') (t : r == s ∙ idp) → Type _
--     T r s t =
--       ap (ap h) (∙'-unit-l s ∙ ! (∙-unit-r s) ∙ ! t) ==
--       (ap-∙' h idp s ∙ idp)
--       ∙
--       (∙'-unit-l (ap h s) ∙
--       ! (∙-unit-r (ap h s)) ∙
--       !
--       (ap (ap h) t ∙'
--         (ap-∙ h s idp ∙ idp)))

--     coh' : {x x' : C} {r s : x == x'} (t : r == s) → T r s (t ∙ ! (∙-unit-r s))
--     coh' {r = idp} {s = .idp} idp = idp

--     coh : {x x' : C} (r s : x == x') (t : r == s ∙ idp) → T r s t
--     coh r s t = transport (λ t → T r s t) (coh2 t (∙-unit-r s)) (coh' (t ∙ ∙-unit-r s))  where

--       coh2 : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : y == z) → (p ∙ q) ∙ ! q == p
--       coh2 idp idp = idp

-- module _ {i j k} {A : Type i} {B B' : Type j} {C : Type k} (f : A → C) (g' : B' → B) (g : B → C) where

--   abc : {a a' : A} {p : a == a'} {c c' : B'} {q' : c == c'} {q : g' c == g' c'}
--     (r : f a == g (g' c')) (s : f a' == g (g' c))
--     (t : q == ap g' q')
--     (α : r == s ∙ ap g q [ (λ x → f x == g (g' c')) ↓ p ])
--     → {!(↓-swap! f g r s α ▹ ?) ∙'2ᵈ ?!} == ↓-swap! f (g ∘ g') {p = p} {q = q'} r s (α ▹ ap (λ u → s ∙ u) (ap (ap g) t ∙ ∘-ap g g' q'))
--   abc = {!!}

{- Functoriality of application and function extensionality -}

∙-app= : ∀ {i j} {A : Type i} {B : A → Type j} {f g h : Π A B}
  (α : f == g) (β : g == h)
  → α ∙ β == λ= (λ x → app= α x ∙ app= β x)
∙-app= idp β = λ=-η β

∙-λ= : ∀ {i j} {A : Type i} {B : A → Type j} {f g h : Π A B}
  (α : f ∼ g) (β : g ∼ h)
  → λ= α ∙ λ= β == λ= (λ x → α x ∙ β x)
∙-λ= α β = ∙-app= (λ= α) (λ= β)
  ∙ ap λ= (λ= (λ x → ap (λ w → w ∙ app= (λ= β) x) (app=-β α x)
                   ∙ ap (λ w → α x ∙ w) (app=-β β x)))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda