text:
import      Lvl
open import Type

module Structure.Logic.Classical.NaturalDeduction {ℓₗ} {Formula : Type{ℓₗ}} {ℓₘₗ} (Proof : Formula → Type{ℓₘₗ}) where

open import Functional hiding (Domain)
import      Structure.Logic.Constructive.NaturalDeduction
private module Constructive = Structure.Logic.Constructive.NaturalDeduction(Proof)

-- TODO: Maybe it is worth to try and take a more minimal approach? (Less axioms? Is this more practical/impractical?)

module Propositional where
  open Constructive.Propositional hiding (Theory) public

  -- A theory of classical propositional logic expressed using natural deduction rules
  record Theory ⦃ sign : Signature ⦄ : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
    open Signature(sign)

    field
      instance ⦃ constructive ⦄ : Constructive.Propositional.Theory ⦃ sign ⦄

    open Constructive.Propositional.Theory (constructive) public

    field
      excluded-middle : ∀{P} → Proof(P ∨ (¬ P))

module Domained = Constructive.Domained

module MultiSorted = Constructive.MultiSorted

  {-
  Propositional-from-[∧][∨][⊥] : ∀{ℓₗ} → (_∧_ _∨_ : Formula → Formula → Formula) → (⊥ : Formula) →
    ([∧]-intro : ∀{X Y} → X → Y → (X ∧ Y)) →
    ([∧]-elimₗ  : ∀{X Y} → (X ∧ Y) → X) →
    ([∧]-elimᵣ  : ∀{X Y} → (X ∧ Y) → Y) →
    ([∨]-introₗ : ∀{X Y} → X → (X ∨ Y)) →
    ([∨]-introᵣ : ∀{X Y} → Y → (X ∨ Y)) →
    ([∨]-elim  : ∀{X Y Z : Formula} → (X → Z) → (Y → Z) → (X ∨ Y) → Z) →
    ([⊥]-intro : ∀{X : Formula} → X → (X → ⊥) → ⊥) →
    ([⊥]-elim  : ∀{X : Formula} → ⊥ → X) →
    Propositional{ℓₗ}
  Propositional-from-[∧][∨][⊥]
    (_∧_) (_∨_) (⊥)
    ([∧]-intro)
    ([∧]-elimₗ)
    ([∧]-elimᵣ)
    ([∨]-introₗ)
    ([∨]-introᵣ)
    ([∨]-elim)
    ([⊥]-intro)
    ([⊥]-elim)
    = record{
      _∧_  = _∧_ ;
      _∨_  = _∨_ ;
      _⟶_ = (x ↦ y ↦ (x ∨ (¬ y))) ;
      _⟵_ = swap _⟶_ ;
      _⟷_ = (x ↦ y ↦ ((x ⟵ y)∧(x ⟶ y))) ;
      ¬_   = (x ↦ (x ⟶ ⊥)) ;
      ⊥    = ⊥ ;
      ⊤    = ¬ ⊥
    }
  -}

module _ {ℓₒ} (Domain : Type{ℓₒ}) where
  record ClassicalLogicSignature : Type{ℓₘₗ Lvl.⊔ (ℓₗ Lvl.⊔ ℓₒ)} where
    open Domained(Domain)

    field
      instance ⦃ propositionalSignature ⦄ : Propositional.Signature
      instance ⦃ predicateSignature ⦄     : Predicate.Signature
      instance ⦃ equalitySignature ⦄      : Equality.Signature

    constructiveLogicSignature : Constructive.ConstructiveLogicSignature(Domain)
    constructiveLogicSignature =
      record{
        propositionalSignature = propositionalSignature ;
        predicateSignature     = predicateSignature ;
        equalitySignature      = equalitySignature
      }

    open Propositional.Signature(propositionalSignature) public
    open Predicate.Signature(predicateSignature) public
    open Equality.Signature(equalitySignature) public
    open Equality.PropositionallyDerivedSignature ⦃ propositionalSignature ⦄ ⦃ equalitySignature ⦄ public
    open Uniqueness.Signature ⦃ propositionalSignature ⦄ ⦃ predicateSignature ⦄ ⦃ equalitySignature ⦄ public

  -- A theory of classical predicate/(first-order) logic expressed using natural deduction rules
  record ClassicalLogic : Type{ℓₘₗ Lvl.⊔ (ℓₗ Lvl.⊔ ℓₒ)} where
    open Domained(Domain)

    field
      instance ⦃ classicalLogicSignature ⦄ : ClassicalLogicSignature
    open ClassicalLogicSignature(classicalLogicSignature) public

    field
      instance ⦃ propositionalTheory ⦄ : Propositional.Theory ⦃ propositionalSignature ⦄
      instance ⦃ predicateTheory ⦄     : Predicate.Theory
      instance ⦃ equalityTheory ⦄      : Equality.Theory
      instance ⦃ existentialWitness ⦄  : Predicate.ExistentialWitness(∃ₗ)
      ⦃ nonEmptyDomain ⦄               : NonEmptyDomain

    constructivePropositionalTheory = Propositional.Theory.constructive(propositionalTheory)

    constructiveLogic : Constructive.ConstructiveLogic(Domain)
    constructiveLogic =
      record{
        constructiveLogicSignature = constructiveLogicSignature ;
        propositionalTheory        = constructivePropositionalTheory ;
        predicateTheory            = predicateTheory ;
        equalityTheory             = equalityTheory
      }

    open Propositional.Theory(propositionalTheory) public
    open Predicate.Theory(predicateTheory) public
    open Equality.Theory(equalityTheory) public
    open Predicate.ExistentialWitness(existentialWitness) public
    open Uniqueness.WitnessTheory ⦃ propositionalSignature ⦄ ⦃ predicateSignature ⦄ ⦃ equalitySignature ⦄ ⦃ constructivePropositionalTheory ⦄ ⦃ predicateTheory ⦄ ⦃ equalityTheory ⦄ ⦃ existentialWitness ⦄ public
    open NonEmptyDomain ⦃ nonEmptyDomain ⦄ public

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:
------------------------------------------------------------------------
-- Internal coding
------------------------------------------------------------------------

module Internal-coding where

open import Equality.Propositional
open import Prelude hiding (const)
open import Tactic.By.Propositional

-- To simplify the development, let's work with actual natural numbers
-- as variables and constants (see
-- Atom.one-can-restrict-attention-to-χ-ℕ-atoms).

open import Atom

open import Chi            χ-ℕ-atoms
open import Coding         χ-ℕ-atoms
open import Constants      χ-ℕ-atoms
open import Free-variables χ-ℕ-atoms
open import Reasoning      χ-ℕ-atoms

open χ-atoms χ-ℕ-atoms

import Coding.Instances.Nat

abstract

  -- Some auxiliary definitions.

  private

    cd : Var → Exp
    cd x = apply (var v-internal-code) (var x)

    nullary-branch : Const → Br
    nullary-branch c =
      branch c [] (
        const c-const (⌜ c ⌝ ∷
          ⌜ [] ⦂ List Exp ⌝ ∷ []))

    unary-branch : Const → Br
    unary-branch c =
      branch c (v-x ∷ []) (
        const c-const (⌜ c ⌝ ∷
          const c-cons (cd v-x ∷
            ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []))

    binary-branch : Const → Br
    binary-branch c =
      branch c (v-x ∷ v-y ∷ []) (
        const c-const (⌜ c ⌝ ∷
          const c-cons (cd v-x ∷
            const c-cons (cd v-y ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ []))

    trinary-branch : Const → Br
    trinary-branch c =
      branch c (v-x ∷ v-y ∷ v-z ∷ []) (
        const c-const (⌜ c ⌝ ∷
          const c-cons (cd v-x ∷
            const c-cons (cd v-y ∷
              const c-cons (cd v-z ∷
                ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ []) ∷ []))

    branches : List Br
    branches =
      nullary-branch c-zero ∷
      unary-branch c-suc ∷
      nullary-branch c-nil ∷
      binary-branch c-cons ∷
      binary-branch c-apply ∷
      binary-branch c-lambda ∷
      binary-branch c-case ∷
      binary-branch c-rec ∷
      unary-branch c-var ∷
      binary-branch c-const ∷
      trinary-branch c-branch ∷
      []

  -- Internal coding.

  internal-code : Exp
  internal-code =
    rec v-internal-code (lambda v-p (case (var v-p) branches))

  internal-code-closed : Closed internal-code
  internal-code-closed = from-⊎ (closed? internal-code)

  -- The internal coder encodes natural numbers correctly.

  internal-code-correct-ℕ :
    (n : ℕ) → apply internal-code ⌜ n ⌝ ⇓ ⌜ ⌜ n ⌝ ⦂ Exp ⌝
  internal-code-correct-ℕ n =
    apply internal-code ⌜ n ⌝  ⟶⟨ apply (rec lambda) (rep⇓rep n) ⟩
    case ⌜ n ⌝ branches′       ⇓⟨ lemma n ⟩■
    ⌜ ⌜ n ⌝ ⦂ Exp ⌝
    where
    branches′ : List Br
    branches′ = branches [ v-internal-code ← internal-code ]B⋆

    lemma : (n : ℕ) → case ⌜ n ⌝ branches′ ⇓ ⌜ ⌜ n ⌝ ⦂ Exp ⌝
    lemma zero =
      case ⌜ zero ⌝ branches′  ⇓⟨ case (rep⇓rep zero) here [] (rep⇓rep (⌜ zero ⌝ ⦂ Exp)) ⟩■
      ⌜ ⌜ zero ⌝ ⦂ Exp ⌝

    lemma (suc n) =
      case ⌜ suc n ⌝ branches′                        ⟶⟨ case (rep⇓rep (suc n)) (there (λ ()) here) (∷ []) ⟩

      const c-const (⌜ c-suc ⌝ ∷
        const c-cons (apply internal-code ⌜ n ⌝ ∷
          ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ [])               ⇓⟨ const (rep⇓rep c-suc ∷
                                                           const (internal-code-correct-ℕ n ∷ rep⇓rep ([] ⦂ List Exp) ∷ []) ∷ []) ⟩■
      ⌜ ⌜ suc n ⌝ ⦂ Exp ⌝

  -- The internal coder encodes lists of variables correctly.

  internal-code-correct-Var⋆ :
    (xs : List Var) →
    apply internal-code ⌜ xs ⌝ ⇓ ⌜ ⌜ xs ⌝ ⦂ Exp ⌝
  internal-code-correct-Var⋆ xs =
    apply internal-code ⌜ xs ⌝  ⟶⟨ apply (rec lambda) (rep⇓rep xs) ⟩
    case ⌜ xs ⌝ branches′       ⇓⟨ lemma xs ⟩■
    ⌜ ⌜ xs ⌝ ⦂ Exp ⌝
    where
    branches′ : List Br
    branches′ = branches [ v-internal-code ← internal-code ]B⋆

    lemma : (xs : List Var) →
            case ⌜ xs ⌝ branches′ ⇓ ⌜ ⌜ xs ⌝ ⦂ Exp ⌝
    lemma [] =
      case ⌜ [] ⦂ List Var ⌝ branches′  ⇓⟨ case (rep⇓rep ([] ⦂ List Var)) (there (λ ()) (there (λ ()) here)) []
                                                (rep⇓rep (⌜ [] ⦂ List Var ⌝ ⦂ Exp)) ⟩■
      ⌜ ⌜ [] ⦂ List Var ⌝ ⦂ Exp ⌝

    lemma (x ∷ xs) =
      case ⌜ x List.∷ xs ⌝ branches′                                      ⟶⟨ case (rep⇓rep (x List.∷ xs))
                                                                                (there (λ ()) (there (λ ()) (there (λ ()) here))) (∷ ∷ []) ⟩
      const c-const (⌜ c-cons ⌝ ∷
        const c-cons (apply internal-code ⌜ x ⌝ ∷
          const c-cons (apply internal-code ⟨ ⌜ xs ⌝ [ v-x ← ⌜ x ⌝ ] ⟩ ∷
            ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                           ≡⟨ ⟨by⟩ (subst-rep xs) ⟩⟶

      const c-const (⌜ c-cons ⌝ ∷
        const c-cons (apply internal-code ⌜ x ⌝ ∷
          const c-cons (apply internal-code ⌜ xs ⌝ ∷
            ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                           ⇓⟨ const (rep⇓rep c-cons ∷
                                                                               const (internal-code-correct-ℕ x ∷
                                                                                const (internal-code-correct-Var⋆ xs ∷
                                                                                rep⇓rep ([] ⦂ List Exp) ∷ []) ∷ []) ∷ []) ⟩■
      ⌜ ⌜ x List.∷ xs ⌝ ⦂ Exp ⌝

  mutual

    -- The internal coder encodes expressions correctly.

    internal-code-correct :
      (p : Exp) → apply internal-code ⌜ p ⌝ ⇓ ⌜ ⌜ p ⌝ ⦂ Exp ⌝
    internal-code-correct p =
      apply internal-code ⌜ p ⌝  ⟶⟨ apply (rec lambda) (rep⇓rep p) ⟩
      case ⌜ p ⌝ branches′       ⇓⟨ lemma p ⟩■
      ⌜ ⌜ p ⌝ ⦂ Exp ⌝
      where
      branches′ : List Br
      branches′ = branches [ v-internal-code ← internal-code ]B⋆

      lemma : (p : Exp) → case ⌜ p ⌝ branches′ ⇓ ⌜ ⌜ p ⌝ ⦂ Exp ⌝
      lemma (apply p₁ p₂) =
        case ⌜ Exp.apply p₁ p₂ ⌝ branches′                                   ⟶⟨ case (rep⇓rep (Exp.apply p₁ p₂))
                                                                                (there (λ ()) (there (λ ()) (there (λ ())
                                                                                (there (λ ()) here))))
                                                                                (∷ ∷ []) ⟩
        const c-const (⌜ c-apply ⌝ ∷
          const c-cons (apply internal-code ⌜ p₁ ⌝ ∷
            const c-cons (apply internal-code ⟨ ⌜ p₂ ⌝ [ v-x ← ⌜ p₁ ⌝ ] ⟩ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                            ≡⟨ ⟨by⟩ (subst-rep p₂) ⟩⟶

        const c-const (⌜ c-apply ⌝ ∷
          const c-cons (apply internal-code ⌜ p₁ ⌝ ∷
            const c-cons (apply internal-code ⌜ p₂ ⌝ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                            ⇓⟨ const (rep⇓rep c-apply ∷
                                                                                const (internal-code-correct p₁ ∷
                                                                                const (internal-code-correct p₂ ∷
                                                                                rep⇓rep ([] ⦂ List Exp) ∷ []) ∷ []) ∷ []) ⟩■
        ⌜ ⌜ Exp.apply p₁ p₂ ⌝ ⦂ Exp ⌝

      lemma (lambda x p) =
        case ⌜ Exp.lambda x p ⌝ branches′                                  ⟶⟨ case (rep⇓rep (Exp.lambda x p))
                                                                                (there (λ ()) (there (λ ()) (there (λ ())
                                                                                (there (λ ()) (there (λ ()) here)))))
                                                                                (∷ ∷ []) ⟩
        const c-const (⌜ c-lambda ⌝ ∷
          const c-cons (apply internal-code ⌜ x ⌝ ∷
            const c-cons (apply internal-code ⟨ ⌜ p ⌝ [ v-x ← ⌜ x ⌝ ] ⟩ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                          ≡⟨ ⟨by⟩ (subst-rep p) ⟩⟶

        const c-const (⌜ c-lambda ⌝ ∷
          const c-cons (apply internal-code ⌜ x ⌝ ∷
            const c-cons (apply internal-code ⌜ p ⌝ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                          ⇓⟨ const (rep⇓rep c-lambda ∷
                                                                                const (internal-code-correct-ℕ x ∷
                                                                                const (internal-code-correct p ∷
                                                                                rep⇓rep ([] ⦂ List Exp) ∷ []) ∷ []) ∷ []) ⟩■
        ⌜ ⌜ Exp.lambda x p ⌝ ⦂ Exp ⌝

      lemma (case p bs) =
        case ⌜ Exp.case p bs ⌝ branches′                                    ⟶⟨ case (rep⇓rep (Exp.case p bs))
                                                                                (there (λ ()) (there (λ ()) (there (λ ())
                                                                                (there (λ ()) (there (λ ()) (there (λ ()) here))))))
                                                                                (∷ ∷ []) ⟩
        const c-const (⌜ c-case ⌝ ∷
          const c-cons (apply internal-code ⌜ p ⌝ ∷
            const c-cons (apply internal-code ⟨ ⌜ bs ⌝ [ v-x ← ⌜ p ⌝ ] ⟩ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                           ≡⟨ ⟨by⟩ (subst-rep bs) ⟩⟶

        const c-const (⌜ c-case ⌝ ∷
          const c-cons (apply internal-code ⌜ p ⌝ ∷
            const c-cons (apply internal-code ⌜ bs ⌝ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                           ⇓⟨ const (rep⇓rep c-case ∷
                                                                                const (internal-code-correct p ∷
                                                                                const (internal-code-correct-B⋆ bs ∷
                                                                                rep⇓rep ([] ⦂ List Exp) ∷ []) ∷ []) ∷ []) ⟩■
        ⌜ ⌜ Exp.case p bs ⌝ ⦂ Exp ⌝

      lemma (rec x p) =
        case ⌜ Exp.rec x p ⌝ branches′                                     ⟶⟨ case (rep⇓rep (Exp.rec x p))
                                                                                (there (λ ()) (there (λ ()) (there (λ ()) (there (λ ())
                                                                                (there (λ ()) (there (λ ()) (there (λ ()) here)))))))
                                                                                (∷ ∷ []) ⟩
        const c-const (⌜ c-rec ⌝ ∷
          const c-cons (apply internal-code ⌜ x ⌝ ∷
            const c-cons (apply internal-code ⟨ ⌜ p ⌝ [ v-x ← ⌜ x ⌝ ] ⟩ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                          ≡⟨ ⟨by⟩ (subst-rep p) ⟩⟶
        const c-const (⌜ c-rec ⌝ ∷
          const c-cons (apply internal-code ⌜ x ⌝ ∷
            const c-cons (apply internal-code ⌜ p ⌝ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                          ⇓⟨ const (rep⇓rep c-rec ∷
                                                                                const (internal-code-correct-ℕ x ∷
                                                                                const (internal-code-correct p ∷
                                                                                rep⇓rep ([] ⦂ List Exp) ∷ []) ∷ []) ∷ []) ⟩■
        ⌜ ⌜ Exp.rec x p ⌝ ⦂ Exp ⌝

      lemma (var x) =
        case ⌜ Exp.var x ⌝ branches′                 ⟶⟨ case (rep⇓rep (Exp.var x))
                                                             (there (λ ()) (there (λ ()) (there (λ ()) (there (λ ()) (there (λ ())
                                                                (there (λ ()) (there (λ ()) (there (λ ()) here))))))))
                                                             (∷ []) ⟩
        const c-const (⌜ c-var ⌝ ∷
          const c-cons (apply internal-code ⌜ x ⌝ ∷
            ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ [])            ⇓⟨ const (rep⇓rep c-var ∷
                                                          const (internal-code-correct-ℕ x ∷ rep⇓rep ([] ⦂ List Exp) ∷ []) ∷ []) ⟩■
        ⌜ ⌜ Exp.var x ⌝ ⦂ Exp ⌝

      lemma (const c ps) =
        case ⌜ Exp.const c ps ⌝ branches′                                   ⟶⟨ case (rep⇓rep (Exp.const c ps))
                                                                                (there (λ ()) (there (λ ()) (there (λ ()) (there (λ ())
                                                                                (there (λ ()) (there (λ ()) (there (λ ()) (there (λ ())
                                                                                (there (λ ()) here)))))))))
                                                                                (∷ ∷ []) ⟩
        const c-const (⌜ c-const ⌝ ∷
          const c-cons (apply internal-code ⌜ c ⌝ ∷
            const c-cons (apply internal-code ⟨ ⌜ ps ⌝ [ v-x ← ⌜ c ⌝ ] ⟩ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                           ≡⟨ ⟨by⟩ (subst-rep ps) ⟩⟶

        const c-const (⌜ c-const ⌝ ∷
          const c-cons (apply internal-code ⌜ c ⌝ ∷
            const c-cons (apply internal-code ⌜ ps ⌝ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                           ⇓⟨ const (rep⇓rep c-const ∷
                                                                                const (internal-code-correct-ℕ c ∷
                                                                                const (internal-code-correct-⋆ ps ∷
                                                                                rep⇓rep ([] ⦂ List Exp) ∷ []) ∷ []) ∷ []) ⟩■
        ⌜ ⌜ Exp.const c ps ⌝ ⦂ Exp ⌝

    -- The internal coder encodes branches correctly.

    internal-code-correct-B :
      (b : Br) → apply internal-code ⌜ b ⌝ ⇓ ⌜ ⌜ b ⌝ ⦂ Exp ⌝
    internal-code-correct-B (branch c xs e) =
      apply internal-code ⌜ branch c xs e ⌝                                ⟶⟨ apply (rec lambda) (rep⇓rep (branch c xs e)) ⟩

      case ⌜ branch c xs e ⌝ branches′                                     ⟶⟨ case (rep⇓rep (branch c xs e))
                                                                                (there (λ ()) (there (λ ()) (there (λ ()) (there (λ ())
                                                                                (there (λ ()) (there (λ ()) (there (λ ()) (there (λ ())
                                                                                (there (λ ()) (there (λ ()) here))))))))))
                                                                                (∷ ∷ ∷ []) ⟩
      const c-const (⌜ c-branch ⌝ ∷
        const c-cons (apply internal-code ⌜ c ⌝ ∷
          const c-cons (apply internal-code ⌜ xs ⌝ [ v-x ← ⌜ c ⌝ ] ∷
            const c-cons (apply internal-code ⟨ ⌜ e ⌝ [ v-y ← ⌜ xs ⌝ ]
                                                      [ v-x ← ⌜ c ⌝ ] ⟩ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ []) ∷ [])                    ≡⟨ ⟨by⟩ (substs-rep e ((v-x , ⌜ c ⌝) ∷ (v-y , ⌜ xs ⌝) ∷ [])) ⟩⟶

      const c-const (⌜ c-branch ⌝ ∷
        const c-cons (apply internal-code ⌜ c ⌝ ∷
          const c-cons (apply internal-code ⟨ ⌜ xs ⌝ [ v-x ← ⌜ c ⌝ ] ⟩ ∷
            const c-cons (apply internal-code ⌜ e ⌝ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ []) ∷ [])                    ≡⟨ ⟨by⟩ (subst-rep xs) ⟩⟶

      const c-const (⌜ c-branch ⌝ ∷
        const c-cons (apply internal-code ⌜ c ⌝ ∷
          const c-cons (apply internal-code ⌜ xs ⌝ ∷
            const c-cons (apply internal-code ⌜ e ⌝ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ []) ∷ [])                    ⇓⟨ const (rep⇓rep c-branch ∷
                                                                                const (internal-code-correct-ℕ c ∷
                                                                                const (internal-code-correct-Var⋆ xs ∷
                                                                                const (internal-code-correct e ∷
                                                                                rep⇓rep ([] ⦂ List Exp) ∷ []) ∷ []) ∷ []) ∷ []) ⟩■
      ⌜ ⌜ branch c xs e ⌝ ⦂ Exp ⌝
      where
      branches′ : List Br
      branches′ = branches [ v-internal-code ← internal-code ]B⋆

    -- The internal coder encodes lists of expressions correctly.

    internal-code-correct-⋆ :
      (ps : List Exp) →
      apply internal-code ⌜ ps ⌝ ⇓ ⌜ ⌜ ps ⌝ ⦂ Exp ⌝
    internal-code-correct-⋆ ps =
      apply internal-code ⌜ ps ⌝  ⟶⟨ apply (rec lambda) (rep⇓rep ps) ⟩
      case ⌜ ps ⌝ branches′       ⇓⟨ lemma ps ⟩■
      ⌜ ⌜ ps ⌝ ⦂ Exp ⌝
      where
      branches′ : List Br
      branches′ = branches [ v-internal-code ← internal-code ]B⋆

      lemma : (ps : List Exp) →
              case ⌜ ps ⌝ branches′ ⇓ ⌜ ⌜ ps ⌝ ⦂ Exp ⌝
      lemma [] =
        case ⌜ [] ⦂ List Exp ⌝ branches′  ⇓⟨ case (rep⇓rep ([] ⦂ List Exp)) (there (λ ()) (there (λ ()) here)) []
                                                  (rep⇓rep (⌜ [] ⦂ List Exp ⌝ ⦂ Exp)) ⟩■
        ⌜ ⌜ [] ⦂ List Exp ⌝ ⦂ Exp ⌝

      lemma (p ∷ ps) =
        case ⌜ p List.∷ ps ⌝ branches′                                      ⟶⟨ case (rep⇓rep (p List.∷ ps))
                                                                                (there (λ ()) (there (λ ()) (there (λ ()) here))) (∷ ∷ []) ⟩
        const c-const (⌜ c-cons ⌝ ∷
          const c-cons (apply internal-code ⌜ p ⌝ ∷
            const c-cons (apply internal-code ⟨ ⌜ ps ⌝ [ v-x ← ⌜ p ⌝ ] ⟩ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                           ≡⟨ ⟨by⟩ (subst-rep ps) ⟩⟶
        const c-const (⌜ c-cons ⌝ ∷
          const c-cons (apply internal-code ⌜ p ⌝ ∷
            const c-cons (apply internal-code ⌜ ps ⌝ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                           ⇓⟨ const (rep⇓rep c-cons ∷
                                                                                const (internal-code-correct p ∷
                                                                                const (internal-code-correct-⋆ ps ∷
                                                                                rep⇓rep ([] ⦂ List Exp) ∷ []) ∷ []) ∷ []) ⟩■
        ⌜ ⌜ p List.∷ ps ⌝ ⦂ Exp ⌝

    -- The internal coder encodes lists of branches correctly.

    internal-code-correct-B⋆ :
      (bs : List Br) →
      apply internal-code ⌜ bs ⌝ ⇓ ⌜ ⌜ bs ⌝ ⦂ Exp ⌝
    internal-code-correct-B⋆ bs =
      apply internal-code ⌜ bs ⌝  ⟶⟨ apply (rec lambda) (rep⇓rep bs) ⟩
      case ⌜ bs ⌝ branches′       ⇓⟨ lemma bs ⟩■
      ⌜ ⌜ bs ⌝ ⦂ Exp ⌝
      where
      branches′ : List Br
      branches′ = branches [ v-internal-code ← internal-code ]B⋆

      lemma : (bs : List Br) →
              case ⌜ bs ⌝ branches′ ⇓ ⌜ ⌜ bs ⌝ ⦂ Exp ⌝
      lemma [] =
        case ⌜ [] ⦂ List Br ⌝ branches′  ⇓⟨ case (rep⇓rep ([] ⦂ List Br)) (there (λ ()) (there (λ ()) here)) []
                                                 (rep⇓rep (⌜ [] ⦂ List Br ⌝ ⦂ Exp)) ⟩■
        ⌜ ⌜ [] ⦂ List Br ⌝ ⦂ Exp ⌝

      lemma (b ∷ bs) =
        case ⌜ b List.∷ bs ⌝ branches′                                      ⟶⟨ case (rep⇓rep (b List.∷ bs))
                                                                                (there (λ ()) (there (λ ()) (there (λ ()) here))) (∷ ∷ []) ⟩
        const c-const (⌜ c-cons ⌝ ∷
          const c-cons (apply internal-code ⌜ b ⌝ ∷
            const c-cons (apply internal-code ⟨ ⌜ bs ⌝ [ v-x ← ⌜ b ⌝ ] ⟩ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                           ≡⟨ ⟨by⟩ (subst-rep bs) ⟩⟶
        const c-const (⌜ c-cons ⌝ ∷
          const c-cons (apply internal-code ⌜ b ⌝ ∷
            const c-cons (apply internal-code ⌜ bs ⌝ ∷
              ⌜ [] ⦂ List Exp ⌝ ∷ []) ∷ []) ∷ [])                           ⇓⟨ const (rep⇓rep c-cons ∷
                                                                                const (internal-code-correct-B b ∷
                                                                                const (internal-code-correct-B⋆ bs ∷
                                                                                rep⇓rep ([] ⦂ List Exp) ∷ []) ∷ []) ∷ []) ⟩■
        ⌜ ⌜ b List.∷ bs ⌝ ⦂ Exp ⌝

ext: agda

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
module Everything where

import Control.Category
import Control.Category.Functor
import Control.Category.Product
import Control.Category.SetsAndFunctions
import Control.Category.Slice
import Control.Decoration
import Control.Functor
import Control.Functor.NaturalTransformation
import Control.Functor.Product
import Control.Kleisli
import Control.Lens
import Control.Monad
import Control.Monad.Error
import Control.Monad.KleisliTriple
import Control.Comonad
import Control.Comonad.Store

import Dimension.PartialWeakening
import Dimension.PartialWeakening.Model

-- import Dimension.PartialWeakening.Soundness -- still broken

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
------------------------------------------------------------------------
-- The lens type in Lens.Non-dependent.Higher.Capriotti.Variant, but
-- with erased "proofs"
------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

import Equality.Path as P

module Lens.Non-dependent.Higher.Capriotti.Variant.Erased
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Equivalence.Erased.Cubical eq as EEq using (_≃ᴱ_)
open import Equivalence.Erased.Contractible-preimages.Cubical eq as ECP
  using (_⁻¹ᴱ_)
open import Erased.Cubical eq
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as T using (∥_∥; ∣_∣)
open import Preimage equality-with-J using (_⁻¹_)
open import Univalence-axiom equality-with-J

open import Lens.Non-dependent eq
import Lens.Non-dependent.Higher.Erased eq as Higher
import Lens.Non-dependent.Higher.Capriotti.Variant eq as V

private
  variable
    a b p : Level
    A B   : Type a

------------------------------------------------------------------------
-- The lens type family

-- Coherently constant type-valued functions.

Coherently-constant :
  {A : Type a} → (A → Type p) → Type (a ⊔ lsuc p)
Coherently-constant {p = p} {A = A} P =
  ∃ λ (Q : ∥ A ∥ → Type p) → ∀ x → P x ≃ᴱ Q ∣ x ∣

-- Higher lenses with erased "proofs".

Lens : Type a → Type b → Type (lsuc (a ⊔ b))
Lens A B = ∃ λ (get : A → B) → Coherently-constant (get ⁻¹ᴱ_)

-- In erased contexts Lens A B is equivalent to V.Lens A B.

@0 Lens≃Variant-lens : Lens A B ≃ V.Lens A B
Lens≃Variant-lens =
  (∃ λ get → ∃ λ Q → ∀ x → get ⁻¹ᴱ x ≃ᴱ Q ∣ x ∣)  ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ → inverse
                                                      EEq.≃≃≃ᴱ) ⟩
  (∃ λ get → ∃ λ Q → ∀ x → get ⁻¹ᴱ x ≃  Q ∣ x ∣)  ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ →
                                                      Eq.≃-preserves ext (inverse ECP.⁻¹≃⁻¹ᴱ) F.id) ⟩□
  (∃ λ get → ∃ λ Q → ∀ x → get ⁻¹  x ≃  Q ∣ x ∣)  □

-- Some derived definitions.

module Lens {A : Type a} {B : Type b} (l : Lens A B) where

  -- A getter.

  get : A → B
  get = proj₁ l

  -- A predicate.

  H : Pow a ∥ B ∥
  H = proj₁ (proj₂ l)

  -- An equivalence (with erased proofs).

  get⁻¹ᴱ-≃ᴱ : ∀ b → get ⁻¹ᴱ b ≃ᴱ H ∣ b ∣
  get⁻¹ᴱ-≃ᴱ = proj₂ (proj₂ l)

  -- All the getter's "preimages" are equivalent (with erased proofs).

  get⁻¹ᴱ-constant : (b₁ b₂ : B) → get ⁻¹ᴱ b₁ ≃ᴱ get ⁻¹ᴱ b₂
  get⁻¹ᴱ-constant b₁ b₂ =
    get ⁻¹ᴱ b₁  ↝⟨ get⁻¹ᴱ-≃ᴱ b₁ ⟩
    H ∣ b₁ ∣    ↔⟨ ≡⇒≃ $ cong H $ T.truncation-is-proposition _ _ ⟩
    H ∣ b₂ ∣    ↝⟨ inverse $ get⁻¹ᴱ-≃ᴱ b₂ ⟩□
    get ⁻¹ᴱ b₂  □

  -- The two directions of get⁻¹ᴱ-constant.

  get⁻¹ᴱ-const : (b₁ b₂ : B) → get ⁻¹ᴱ b₁ → get ⁻¹ᴱ b₂
  get⁻¹ᴱ-const b₁ b₂ = _≃ᴱ_.to (get⁻¹ᴱ-constant b₁ b₂)

  get⁻¹ᴱ-const⁻¹ᴱ : (b₁ b₂ : B) → get ⁻¹ᴱ b₂ → get ⁻¹ᴱ b₁
  get⁻¹ᴱ-const⁻¹ᴱ b₁ b₂ = _≃ᴱ_.from (get⁻¹ᴱ-constant b₁ b₂)

  -- Some coherence properties.

  @0 get⁻¹ᴱ-const-∘ :
    (b₁ b₂ b₃ : B) (p : get ⁻¹ᴱ b₁) →
    get⁻¹ᴱ-const b₂ b₃ (get⁻¹ᴱ-const b₁ b₂ p) ≡ get⁻¹ᴱ-const b₁ b₃ p
  get⁻¹ᴱ-const-∘ b₁ b₂ b₃ p =
    _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₃)
      (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b₂)
            (_≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₂)
               (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
                  (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b₁) p)))))                ≡⟨ cong (_≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ _) ∘ ≡⇒→ _) $
                                                                   _≃ᴱ_.right-inverse-of (get⁻¹ᴱ-≃ᴱ _) _ ⟩
    _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₃)
      (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
         (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
            (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b₁) p)))                        ≡⟨ cong (λ eq → _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ _) (_≃_.to eq (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ _) _))) $ sym $
                                                                   ≡⇒≃-trans ext _ _ ⟩
    _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₃)
      (≡⇒→ (trans (cong H $ T.truncation-is-proposition _ _)
              (cong H $ T.truncation-is-proposition _ _))
            (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b₁) p))                         ≡⟨ cong (λ eq → _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₃) (≡⇒→ eq _)) $
                                                                   trans (sym $ cong-trans _ _ _) $
                                                                   cong (cong H) $ mono₁ 1 T.truncation-is-proposition _ _ ⟩∎
    _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₃)
      (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b₁) p))                            ∎

  @0 get⁻¹ᴱ-const-id :
    (b : B) (p : get ⁻¹ᴱ b) → get⁻¹ᴱ-const b b p ≡ p
  get⁻¹ᴱ-const-id b p =
    get⁻¹ᴱ-const b b p                                           ≡⟨ sym $ _≃ᴱ_.left-inverse-of (get⁻¹ᴱ-constant _ _) _ ⟩
    get⁻¹ᴱ-const⁻¹ᴱ b b (get⁻¹ᴱ-const b b (get⁻¹ᴱ-const b b p))  ≡⟨ cong (get⁻¹ᴱ-const⁻¹ᴱ b b) $ get⁻¹ᴱ-const-∘ _ _ _ _ ⟩
    get⁻¹ᴱ-const⁻¹ᴱ b b (get⁻¹ᴱ-const b b p)                     ≡⟨ _≃ᴱ_.left-inverse-of (get⁻¹ᴱ-constant _ _) _ ⟩∎
    p                                                            ∎

  @0 get⁻¹ᴱ-const-inverse :
    (b₁ b₂ : B) (p : get ⁻¹ᴱ b₁) →
    get⁻¹ᴱ-const b₁ b₂ p ≡ get⁻¹ᴱ-const⁻¹ᴱ b₂ b₁ p
  get⁻¹ᴱ-const-inverse b₁ b₂ p =
    sym $ _≃_.to-from (EEq.≃ᴱ→≃ (get⁻¹ᴱ-constant _ _)) (
      get⁻¹ᴱ-const b₂ b₁ (get⁻¹ᴱ-const b₁ b₂ p)  ≡⟨ get⁻¹ᴱ-const-∘ _ _ _ _ ⟩
      get⁻¹ᴱ-const b₁ b₁ p                       ≡⟨ get⁻¹ᴱ-const-id _ _ ⟩∎
      p                                          ∎)

  -- A setter.

  set : A → B → A
  set a b =                      $⟨ get⁻¹ᴱ-const _ _ ⟩
    (get ⁻¹ᴱ get a → get ⁻¹ᴱ b)  ↝⟨ _$ (a , [ refl _ ]) ⟩
    get ⁻¹ᴱ b                    ↝⟨ proj₁ ⟩□
    A                            □

  -- Lens laws.

  @0 get-set : ∀ a b → get (set a b) ≡ b
  get-set a b =
    get (proj₁ (get⁻¹ᴱ-const (get a) b (a , [ refl _ ])))  ≡⟨ erased (proj₂ (get⁻¹ᴱ-const (get a) b (a , [ refl _ ]))) ⟩∎
    b                                                      ∎

  @0 set-get : ∀ a → set a (get a) ≡ a
  set-get a =
    proj₁ (get⁻¹ᴱ-const (get a) (get a) (a , [ refl _ ]))  ≡⟨ cong proj₁ $ get⁻¹ᴱ-const-id _ _ ⟩∎
    a                                                      ∎

  @0 set-set : ∀ a b₁ b₂ → set (set a b₁) b₂ ≡ set a b₂
  set-set a b₁ b₂ =
    proj₁ (get⁻¹ᴱ-const (get (set a b₁)) b₂ (set a b₁ , [ refl _ ]))  ≡⟨ elim¹
                                                                           (λ {b} eq →
                                                                              proj₁ (get⁻¹ᴱ-const (get (set a b₁)) b₂ (set a b₁ , [ refl _ ])) ≡
                                                                              proj₁ (get⁻¹ᴱ-const b b₂ (set a b₁ , [ eq ])))
                                                                           (refl _)
                                                                           (get-set a b₁) ⟩
    proj₁ (get⁻¹ᴱ-const b₁ b₂ (set a b₁ , [ get-set a b₁ ]))          ≡⟨⟩

    proj₁ (get⁻¹ᴱ-const b₁ b₂
             (get⁻¹ᴱ-const (get a) b₁ (a , [ refl _ ])))              ≡⟨ cong proj₁ $ get⁻¹ᴱ-const-∘ _ _ _ _ ⟩∎

    proj₁ (get⁻¹ᴱ-const (get a) b₂ (a , [ refl _ ]))                  ∎

  -- TODO: Can get-set-get and get-set-set be proved for the lens laws
  -- given above?

instance

  -- The lenses defined above have getters and setters.

  has-getter-and-setter :
    Has-getter-and-setter (Lens {a = a} {b = b})
  has-getter-and-setter = record
    { get = Lens.get
    ; set = Lens.set
    }

------------------------------------------------------------------------
-- Equality characterisation lemmas

-- An equality characterisation lemma.

@0 equality-characterisation₁ :
  {A : Type a} {B : Type b} {l₁ l₂ : Lens A B} →
  Block "equality-characterisation" →
  let open Lens in

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b p →
     subst (_$ ∣ b ∣) h
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym g) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)
equality-characterisation₁ {a = a} {l₁ = l₁} {l₂ = l₂} ⊠ =
  l₁ ≡ l₂                                                           ↝⟨ inverse $ Eq.≃-≡ Lens≃Variant-lens ⟩

  l₁′ ≡ l₂′                                                         ↝⟨ V.equality-characterisation₁ ⊠ ⟩

  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b p →
     subst (_$ ∣ b ∣) h
       (_≃_.to (V.Lens.get⁻¹-≃ l₁′ b) (subst (_⁻¹ b) (sym g) p)) ≡
     _≃_.to (V.Lens.get⁻¹-≃ l₂′ b) p)                               ↝⟨ (∃-cong λ g → ∃-cong λ h → ∀-cong ext λ b →
                                                                        Π-cong ext ECP.⁻¹≃⁻¹ᴱ λ p →
                                                                        ≡⇒↝ _ $ cong (λ p′ → subst (_$ _) h (_≃_.to (V.Lens.get⁻¹-≃ l₁′ _) p′) ≡
                                                                                _≃_.to (V.Lens.get⁻¹-≃ l₂′ _) p)
                                                                          (
     subst (_⁻¹ b) (sym g) p                                               ≡⟨ elim₁
                                                                                (λ g → subst (_⁻¹ b) (sym g) p ≡
                                                                                Σ-map id erased (subst (_⁻¹ᴱ b) (sym g) (Σ-map id [_]→ p)))
                                                                                (
       subst (_⁻¹ b) (sym (refl _)) p                                            ≡⟨ trans (cong (flip (subst (_⁻¹ b)) _) sym-refl) $
                                                                                subst-refl _ _ ⟩

       p                                                                         ≡⟨ cong (Σ-map id erased) $ sym $
                                                                                trans (cong (flip (subst (_⁻¹ᴱ b)) _) sym-refl) $
                                                                                subst-refl _ _ ⟩∎
       Σ-map id erased
         (subst (_⁻¹ᴱ b) (sym (refl _)) (Σ-map id [_]→ p))                       ∎)
                                                                                _ ⟩
     Σ-map id erased (subst (_⁻¹ᴱ b) (sym g) (Σ-map id [_]→ p))            ≡⟨⟩

     _≃_.from ECP.⁻¹≃⁻¹ᴱ
       (subst (_⁻¹ᴱ b) (sym g) (_≃_.to ECP.⁻¹≃⁻¹ᴱ p))                      ∎)) ⟩□

  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b p →
     subst (_$ ∣ b ∣) h
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym g) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                    □
  where
  open Lens

  l₁′ = _≃_.to Lens≃Variant-lens l₁
  l₂′ = _≃_.to Lens≃Variant-lens l₂

-- Another equality characterisation lemma.

@0 equality-characterisation₂ :
  {l₁ l₂ : Lens A B} →
  Block "equality-characterisation" →
  let open Lens in

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∀ b p →
     subst id (h ∣ b ∣)
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)
equality-characterisation₂ {l₁ = l₁} {l₂ = l₂} ⊠ =
  l₁ ≡ l₂                                                               ↝⟨ equality-characterisation₁ ⊠ ⟩

  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b p →
     subst (_$ ∣ b ∣) h
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym g) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        ↝⟨ (Σ-cong-contra (Eq.extensionality-isomorphism bad-ext) λ _ →
                                                                            Σ-cong-contra (Eq.extensionality-isomorphism bad-ext) λ _ →
                                                                            F.id) ⟩
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∀ b p →
     subst (_$ ∣ b ∣) (⟨ext⟩ h)
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                            ≡⇒↝ _ $ cong (_≡ _) $
                                                                            subst-ext _ _) ⟩□
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∀ b p →
     subst id (h ∣ b ∣)
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        □
  where
  open Lens

-- Yet another equality characterisation lemma.

@0 equality-characterisation₃ :
  {A : Type a} {B : Type b}
  {l₁ l₂ : Lens A B} →
  Block "equality-characterisation" →
  Univalence (a ⊔ b) →
  let open Lens in

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≃ H l₂ b) →
     ∀ b p →
     _≃_.to (h ∣ b ∣)
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)
equality-characterisation₃ {l₁ = l₁} {l₂ = l₂} ⊠ univ =
  l₁ ≡ l₂                                                               ↝⟨ equality-characterisation₂ ⊠ ⟩

  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∀ b p →
     subst id (h ∣ b ∣)
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        ↝⟨ (∃-cong λ _ →
                                                                            Σ-cong-contra (∀-cong ext λ _ → inverse $ ≡≃≃ univ) λ _ → F.id) ⟩
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≃ H l₂ b) →
     ∀ b p →
     subst id (≃⇒≡ univ (h ∣ b ∣))
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                            ≡⇒↝ _ $ cong (_≡ _) $
                                                                            trans (subst-id-in-terms-of-≡⇒↝ equivalence) $
                                                                            cong (λ eq → _≃_.to eq _) $
                                                                            _≃_.right-inverse-of (≡≃≃ univ) _) ⟩□
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≃ H l₂ b) →
     ∀ b p →
     _≃_.to (h ∣ b ∣)
       (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        □
  where
  open Lens

------------------------------------------------------------------------
-- Conversion functions

-- The lenses defined above can be converted to and from the lenses
-- defined in Higher.

Lens⇔Higher-lens :
  Block "conversion" →
  Lens A B ⇔ Higher.Lens A B
Lens⇔Higher-lens {A = A} {B = B} ⊠ = record
  { to = λ (g , H , eq) → record
           { R = Σ ∥ B ∥ H

           ; equiv =
               A                                               ↝⟨ (inverse $ drop-⊤-right λ _ → _⇔_.to EEq.Contractibleᴱ⇔≃ᴱ⊤
                                                                   Contractibleᴱ-Erased-other-singleton) ⟩
               (∃ λ (a : A) → ∃ λ (b : B) → Erased (g a ≡ b))  ↔⟨ ∃-comm ⟩
               (∃ λ (b : B) → g ⁻¹ᴱ b)                         ↝⟨ ∃-cong eq ⟩
               (∃ λ (b : B) → H ∣ b ∣)                         ↔⟨ (Σ-cong (inverse T.∥∥×≃) λ _ → ≡⇒≃ $ cong H $ T.truncation-is-proposition _ _) ⟩
               (∃ λ ((b , _) : ∥ B ∥ × B) → H b)               ↔⟨ Σ-assoc F.∘
                                                                  (∃-cong λ _ → ×-comm) F.∘
                                                                  inverse Σ-assoc ⟩□
               Σ ∥ B ∥ H × B                                   □

           ; inhabited = proj₁
           }
  ; from = λ l →
               Higher.Lens.get l
             , (λ _ → Higher.Lens.R l)
             , (λ b → inverse (Higher.remainder≃ᴱget⁻¹ᴱ l b))
  }

-- The conversion preserves getters and setters.

Lens⇔Higher-lens-preserves-getters-and-setters :
  (bl : Block "conversion") →
  Preserves-getters-and-setters-⇔ A B (Lens⇔Higher-lens bl)
Lens⇔Higher-lens-preserves-getters-and-setters bl@⊠ =
    (λ l@(g , H , eq) →
         refl _
       , ⟨ext⟩ λ a → ⟨ext⟩ λ b →
         let h₁ = _≃ᴱ_.to (eq (g a)) (a , [ refl _ ])

             h₂ =
               _≃_.from (≡⇒≃ (cong H _))
                 (subst (H ∘ proj₁) (sym (_≃_.left-inverse-of T.∥∥×≃ _))
                    (≡⇒→ (cong H _) h₁))

             h₃ = ≡⇒→ (cong H _) h₁

             lemma =
               h₂                                                         ≡⟨ sym $ subst-in-terms-of-inverse∘≡⇒↝ equivalence _ _ _ ⟩

               subst H _
                 (subst (H ∘ proj₁) (sym (_≃_.left-inverse-of T.∥∥×≃ _))
                    (≡⇒→ (cong H _) h₁))                                  ≡⟨ cong (λ x → subst H (sym $ T.truncation-is-proposition _ _)
                                                                                (subst (H ∘ proj₁)
                                                                                (sym (_≃_.left-inverse-of T.∥∥×≃ (∣ g a ∣ , b)))
                                                                                x)) $ sym $
                                                                             subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩
               subst H _
                 (subst (H ∘ proj₁) (sym (_≃_.left-inverse-of T.∥∥×≃ _))
                    (subst H _ h₁))                                       ≡⟨ cong (λ x → subst H (sym $ T.truncation-is-proposition _ _) x) $
                                                                             subst-∘ _ _ _ ⟩

               subst H _ (subst H _ (subst H _ h₁))                       ≡⟨ cong (λ x → subst H (sym $ T.truncation-is-proposition _ _) x) $
                                                                             subst-subst _ _ _ _ ⟩

               subst H _ (subst H _ h₁)                                   ≡⟨ subst-subst _ _ _ _ ⟩

               subst H _ h₁                                               ≡⟨ cong (λ eq → subst H eq h₁) $
                                                                             mono₁ 1 T.truncation-is-proposition _ _ ⟩

               subst H _ h₁                                               ≡⟨ subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩∎

               ≡⇒→ (cong H _) h₁                                          ∎
         in
         proj₁ (_≃ᴱ_.from (eq b) h₂)  ≡⟨ cong (λ h → proj₁ (_≃ᴱ_.from (eq b) h)) lemma ⟩∎
         proj₁ (_≃ᴱ_.from (eq b) h₃)  ∎)
  , (λ l →
         refl _
       , ⟨ext⟩ λ a → ⟨ext⟩ λ b →
         Lens.set (_⇔_.from (Lens⇔Higher-lens bl) l) a b   ≡⟨⟩

         _≃ᴱ_.from (Higher.Lens.equiv l)
           ( ≡⇒→ (cong (λ _ → Higher.Lens.R l) _)
               (Higher.Lens.remainder l a)
           , b
           )                                               ≡⟨ cong (λ eq → _≃ᴱ_.from (Higher.Lens.equiv l) (≡⇒→ eq _ , b)) $
                                                              cong-const _ ⟩
         _≃ᴱ_.from (Higher.Lens.equiv l)
           (≡⇒→ (refl _) (Higher.Lens.remainder l a) , b)  ≡⟨ cong (λ f → _≃ᴱ_.from (Higher.Lens.equiv l) (f _ , b)) $
                                                              ≡⇒→-refl ⟩
         _≃ᴱ_.from (Higher.Lens.equiv l)
           (Higher.Lens.remainder l a , b)                 ≡⟨⟩

         Higher.Lens.set l a b                             ∎)

-- Lens A B is equivalent to Higher.Lens A B (with erased proofs,
-- assuming univalence).

Lens≃ᴱHigher-lens :
  {A : Type a} {B : Type b} →
  Block "conversion" →
  @0 Univalence (a ⊔ b) →
  Lens A B ≃ᴱ Higher.Lens A B
Lens≃ᴱHigher-lens {A = A} {B = B} bl univ =
  EEq.↔→≃ᴱ
    (_⇔_.to (Lens⇔Higher-lens bl))
    (_⇔_.from (Lens⇔Higher-lens bl))
    (to∘from bl)
    (from∘to bl)
  where
  @0 to∘from :
    (bl : Block "conversion") →
    ∀ l →
    _⇔_.to (Lens⇔Higher-lens bl) (_⇔_.from (Lens⇔Higher-lens bl) l) ≡ l
  to∘from ⊠ l = _↔_.from (Higher.equality-characterisation₂ univ)
    ( (∥ B ∥ × R  ↔⟨ (drop-⊤-left-× λ r → _⇔_.to contractible⇔↔⊤ $
                      propositional⇒inhabited⇒contractible
                        T.truncation-is-proposition
                        (inhabited r)) ⟩□
       R          □)
    , (λ a →
         ≡⇒→ (cong (λ _ → R) (T.truncation-is-proposition _ _))
           (remainder a)                                         ≡⟨ cong (λ eq → ≡⇒→ eq _) $ cong-const _ ⟩

         ≡⇒→ (refl _) (remainder a)                              ≡⟨ cong (_$ _) ≡⇒→-refl ⟩∎

         remainder a                                             ∎)
    , (λ _ → refl _)
    )
    where
    open Higher.Lens l

  @0 from∘to :
    (bl : Block "conversion") →
    ∀ l →
    _⇔_.from (Lens⇔Higher-lens bl) (_⇔_.to (Lens⇔Higher-lens bl) l) ≡ l
  from∘to bl@⊠ l = _≃_.from (equality-characterisation₃ ⊠ univ)
    ( (λ _ → refl _)
    , Σ∥B∥H≃H
    , (λ b p@(a , [ get-a≡b ]) →
         _≃_.to (Σ∥B∥H≃H ∣ b ∣)
           (_≃ᴱ_.from (Higher.remainder≃ᴱget⁻¹ᴱ
                         (_⇔_.to (Lens⇔Higher-lens bl) l) b)
              (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ λ _ → refl _)) p))       ≡⟨ cong (_≃_.to (Σ∥B∥H≃H ∣ b ∣) ∘
                                                                            _≃ᴱ_.from (Higher.remainder≃ᴱget⁻¹ᴱ
                                                                                (_⇔_.to (Lens⇔Higher-lens bl) l) b)) $
                                                                      trans (cong (flip (subst (_⁻¹ᴱ b)) p) $
                                                                             trans (cong sym ext-refl) $
                                                                             sym-refl) $
                                                                      subst-refl _ _ ⟩
         _≃_.to (Σ∥B∥H≃H ∣ b ∣)
           (_≃ᴱ_.from (Higher.remainder≃ᴱget⁻¹ᴱ
                         (_⇔_.to (Lens⇔Higher-lens bl) l) b)
              p)                                                   ≡⟨⟩

         _≃_.to (Σ∥B∥H≃H ∣ b ∣)
           (Higher.Lens.remainder
              (_⇔_.to (Lens⇔Higher-lens bl) l) a)                  ≡⟨⟩

         subst H _
           (≡⇒→ (cong H _) (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a))
                              (a , [ refl _ ])))                   ≡⟨ cong (subst H _) $ sym $
                                                                      subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩

         subst H _ (subst H _ (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a))
                                 (a , [ refl _ ])))                ≡⟨ subst-subst _ _ _ _ ⟩

         subst H _ (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ]))  ≡⟨ cong (λ eq → subst H eq (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ]))) $
                                                                      mono₁ 1 T.truncation-is-proposition _ _ ⟩
         subst H (cong ∣_∣ get-a≡b)
           (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ]))          ≡⟨ elim¹
                                                                        (λ {b} eq →
                                                                           subst H (cong ∣_∣ eq)
                                                                             (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ])) ≡
                                                                           _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b) (a , [ eq ]))
                                                                        (
           subst H (cong ∣_∣ (refl _))
             (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ]))              ≡⟨ trans (cong (flip (subst H) _) $ cong-refl _) $
                                                                            subst-refl _ _ ⟩
           _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ])                  ∎)
                                                                        _ ⟩∎
         _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b) p                                   ∎)
    )
    where
    open Lens l

    Σ∥B∥H≃H = λ b →
      Σ ∥ B ∥ H  ↔⟨ (drop-⊤-left-Σ $ _⇔_.to contractible⇔↔⊤ $
                     propositional⇒inhabited⇒contractible
                       T.truncation-is-proposition b) ⟩□
      H b        □

-- The equivalence preserves getters and setters.

Lens≃ᴱHigher-lens-preserves-getters-and-setters :
  {A : Type a} {B : Type b}
  (bl : Block "conversion")
  (@0 univ : Univalence (a ⊔ b)) →
  Preserves-getters-and-setters-⇔ A B
    (_≃ᴱ_.logical-equivalence (Lens≃ᴱHigher-lens bl univ))
Lens≃ᴱHigher-lens-preserves-getters-and-setters bl univ =
  Lens⇔Higher-lens-preserves-getters-and-setters bl

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Binary.Fiberwise where

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

open import Cubical.Data.Sigma

open import Cubical.Relation.Binary.Base

private
  variable
    ℓA ℓA' ℓ≅A ℓ≅A' ℓB ℓ≅B ℓ≅B' ℓB' : Level

-- given a type A, this is the type of relational families on A
RelFamily : (A : Type ℓA) (ℓB ℓ≅B : Level) → Type (ℓ-max (ℓ-max ℓA (ℓ-suc ℓB)) (ℓ-suc ℓ≅B))
RelFamily A ℓB ℓ≅B = Σ[ B ∈ (A → Type ℓB) ] ({a : A} → Rel (B a) (B a) ℓ≅B)

-- property for a relational family to be fiberwise reflexive
isFiberwiseReflexive : {A : Type ℓA} {ℓB ℓ≅B : Level}
                       (B : RelFamily A ℓB ℓ≅B)
                       → Type (ℓ-max (ℓ-max ℓA ℓB) ℓ≅B)
isFiberwiseReflexive {A = A} (B , _≅_) = {a : A} → isRefl (_≅_ {a = a})

-- property for a relational fiberwise reflexive family to be fiberwise univalent:
isFiberwiseUnivalent : {A : Type ℓA} {ℓB ℓ≅B : Level}
                       (B : RelFamily A ℓB ℓ≅B)
                       (ρ : isFiberwiseReflexive B)
                       → Type (ℓ-max (ℓ-max ℓA ℓB) ℓ≅B)
isFiberwiseUnivalent {A = A} (B , _≅_) ρ = {a : A} → isUnivalent (_≅_ {a = a}) (ρ {a = a})

-- pulling back a relational family along a map
♭RelFamily : {A : Type ℓA} {A' : Type ℓA'}
             {ℓB ℓ≅B : Level} (B : RelFamily A' ℓB ℓ≅B)
             (f : A → A')
             → RelFamily A ℓB ℓ≅B
♭RelFamily (B , _) f .fst a = B (f a)
♭RelFamily (_ , _≅_) f .snd = _≅_

-- the type of relational isomorphisms over f
♭RelFiberIsoOver : {A : Type ℓA} {A' : Type ℓA'}
                  (f : A → A')
                  (B : RelFamily A ℓB ℓ≅B)
                  (B' : RelFamily A' ℓB' ℓ≅B')
                  → Type (ℓ-max ℓA (ℓ-max (ℓ-max ℓB ℓB') (ℓ-max ℓ≅B ℓ≅B')))
♭RelFiberIsoOver {A = A} f B B' = (a : A) → RelIso (B .snd {a = a}) (♭B' .snd {a = a})
  where
    ♭B' = ♭RelFamily B' f

module _ {A : Type ℓA} {A' : Type ℓA'} (F : Iso A A')
         (ℬ : RelFamily A ℓB ℓ≅B) {ρ : isFiberwiseReflexive ℬ} (uni : isFiberwiseUnivalent ℬ ρ)
         (ℬ' : RelFamily A' ℓB' ℓ≅B') {ρ' : isFiberwiseReflexive ℬ'} (uni' : isFiberwiseUnivalent ℬ' ρ') where

       private
         f = Iso.fun F
         B = ℬ .fst
         B' = ℬ' .fst
         ♭B' = ♭RelFamily ℬ' f .fst
         ♭ℬ' = ♭RelFamily ℬ' f

       private
         RelFiberIsoOver→♭FiberIso : (e≅♭ : (a : A) → RelIso (ℬ .snd {a = a}) (♭ℬ' .snd {a = a}))
                                     → (a : A)
                                     → Iso (B a) (B' (f a))
         RelFiberIsoOver→♭FiberIso e≅♭ a = RelIso→Iso (ℬ .snd {a = a}) (ℬ' .snd {a = f a}) uni uni' (e≅♭ a)

       RelFiberIsoOver→Iso : (e≅♭ : (a : A) → RelIso (ℬ .snd {a = a}) (♭ℬ' .snd {a = a}))
                             → Iso (Σ A B) (Σ A' B')
       RelFiberIsoOver→Iso e≅♭ = Σ-cong-iso F (RelFiberIsoOver→♭FiberIso e≅♭)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
------------------------------------------------------------------------------
-- Type theory: The identity type
------------------------------------------------------------------------------

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

-- We can prove the properties of equality used in the formalization
-- of FOTC, from refl and J.

module FOT.Common.FOL.Relation.Binary.PropositionalEquality.TypeTheory where

infix 7 _≡_

postulate
  D    : Set
  _≡_  : D → D → Set
  refl : ∀ {x} → x ≡ x

module TypeTheory where

  -- Using the type-theoretic eliminator for equality.

  postulate J : (C : ∀ x y → x ≡ y → Set) →
                (∀ x → (C x x refl)) →
                ∀ x y → (c : x ≡ y) → C x y c

  -- From Thorsten's slides: A short history of equality.
  sym : ∀ {x y} → x ≡ y → y ≡ x
  sym {x} {y} = J (λ x' y' _ → y' ≡ x') (λ x' → refl) x y

  -- From Thorsten's slides: A short history of equality.
  trans : ∀ {x y z} → x ≡ y → y ≡ z → x ≡ z
  trans {x} {y} {z} = J (λ x' y' _ → y' ≡ z → x' ≡ z) (λ x' pr → pr) x y

  subst : (A : D → Set) → ∀ {x y} → x ≡ y → A x → A y
  subst A {x} {y} x≡y = J (λ x' y' _ → A x' → A y') (λ x' pr → pr) x y x≡y

module FOL where

  -- Using the usual elimination schema for predicate logic.

  postulate J : (A : D → Set) → ∀ {x y} → x ≡ y → A x → A y

  sym : ∀ {x y} → x ≡ y → y ≡ x
  sym {x} {y} x≡y = J (λ y' → y' ≡ x) x≡y refl

  trans : ∀ {x y z} → x ≡ y → y ≡ z → x ≡ z
  trans {x} {y} {z} x≡y = J (λ y' → y' ≡ z → x ≡ z) x≡y (λ pr → pr)

  subst : (A : D → Set) → ∀ {x y} → x ≡ y → A x → A y
  subst = J

module ML where

  -- Using Martin-Löf elimination ("Hauptsatz ...", 1971).

  postulate J : (C : D → D → Set) →
                (∀ x → (C x x)) →
                ∀ x y → x ≡ y → C x y

  sym : ∀ {x y} → x ≡ y → y ≡ x
  sym {x} {y} = J (λ x' y' → y' ≡ x') (λ x' → refl) x y

  trans : ∀ {x y z} → x ≡ y → y ≡ z → x ≡ z
  trans {x} {y} {z} = J (λ x' y' → y' ≡ z → x' ≡ z) (λ x' pr → pr) x y

  subst : (A : D → Set) → ∀ {x y} → x ≡ y → A x → A y
  subst A {x} {y} x≡y = J (λ x' y' → A x' → A y') (λ x' pr → pr) x y x≡y

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Crash where

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

data Bool : Set where
  true : Bool
  false : Bool

F : Bool -> Set
F true  = Nat
F false = Bool

not : Bool -> Bool
not true  = false
not false = true

h : ((x : F ?) -> F (not x)) -> Nat
h g = g zero

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Data.FinData.Order where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Bool.Base
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary

open import Cubical.Data.FinData.Base
open import Cubical.Data.FinData.Properties

private
  variable
    ℓ : Level

-- Order relation:
_≤Fin_ : {n : ℕ} → Fin n → Fin n → Type
i ≤Fin j = (toℕ i) ≤ (toℕ j)

_<Fin_ : {n : ℕ} → Fin n → Fin n → Type
i <Fin j = (suc i) ≤Fin (weakenFin j)

open BinaryRelation
≤FinIsPropValued : ∀ {n : ℕ} → isPropValued (_≤Fin_ {n})
≤FinIsPropValued _ _ = isProp≤

-- inductive version
_≤'Fin_ : {n : ℕ} → Fin n → Fin n → Type
i ≤'Fin j = (toℕ i) ≤' (toℕ j)

_<'Fin_ : {n : ℕ} → Fin n → Fin n → Type
i <'Fin j = (suc i) ≤'Fin (weakenFin j)

open BinaryRelation
≤'FinIsPropValued : ∀ {n : ℕ} → isPropValued (_≤'Fin_ {n})
≤'FinIsPropValued _ _ = ≤'IsPropValued _ _

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------
-- Equivalence of declarative and canonical kinding of Fω with
-- interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Kinding.Canonical.Equivalence where

open import Data.Fin using (zero)
open import Data.Fin.Substitution using (module VarSubst)
open import Data.Fin.Substitution.Typed
open import Data.Product as Prod using (_,_; proj₁; proj₂)
open import Data.Vec using ([])
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality hiding ([_])

open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.HereditarySubstitution
open import FOmegaInt.Syntax.Normalization
open import FOmegaInt.Syntax.WeakEquality
import FOmegaInt.Typing                            as Original
import FOmegaInt.Typing.Validity                   as OriginalValidity
import FOmegaInt.Kinding.Declarative               as Extended
import FOmegaInt.Kinding.Declarative.Validity      as ExtendedValidity
import FOmegaInt.Kinding.Declarative.Equivalence   as ExtendedEquiv
import FOmegaInt.Kinding.Declarative.Normalization as OriginalNorm
open import FOmegaInt.Kinding.Canonical            as Canonical
open import FOmegaInt.Kinding.Canonical.Validity
open import FOmegaInt.Kinding.Canonical.WeakEquality
import FOmegaInt.Kinding.Simple              as SimpKind
import FOmegaInt.Kinding.Simple.EtaExpansion as SimpEtaExp
open import FOmegaInt.Kinding.Simple.Normalization

private

  -- Original declarative rules and lemmas.
  module O where
    open Original            public
    open Typing              public
    open TermCtx             public
    open TypedSubstitution   public
    open OriginalValidity    public
    open OriginalNorm        public

  -- Extended declarative rules and lemmas.
  module E where
    open Extended           public
    open Extended.Kinding   public
    open TermCtx            public
    open KindedSubstitution public
    open ExtendedValidity   public
    open ExtendedEquiv      public

  -- Canonical rules and lemmas.
  module C where
    open Canonical public
    open Kinding   public
    open ElimCtx   public

open Syntax
open Substitution using (_Kind[_])
open ElimCtx
open SimpleCtx using (kd)
open ContextConversions
open WeakEqNormalization
open Kinding
open KindedRenaming
open ContextNarrowing
open Original.Typing  hiding (_ctx; _⊢_wf; _⊢_kd; _⊢_<∷_; _⊢_<:_∈_; _⊢_≅_)
open Extended.Kinding hiding (_ctx; _⊢_wf; _⊢_kd; _⊢_<∷_; _⊢_<:_∈_; _⊢_≅_)

------------------------------------------------------------------------
-- Soundness of canonical (sub)kinding w.r.t. declarative (sub)kinding

mutual

  sound-wf : ∀ {n} {Γ : Ctx n} {a} → Γ ⊢ a wf → ⌞ Γ ⌟Ctx O.⊢ ⌞ a ⌟Asc wf
  sound-wf (wf-kd k-kd)  = wf-kd (sound-kd k-kd)
  sound-wf (wf-tp a⇉a⋯a) = wf-tp (O.Tp∈-⋯-* (sound-Nf⇉ a⇉a⋯a))

  sound-ctx : ∀ {n} {Γ : Ctx n} → Γ ctx → ⌞ Γ ⌟Ctx O.ctx
  sound-ctx C.[]             = O.[]
  sound-ctx (a-wf C.∷ Γ-ctx) = sound-wf a-wf O.∷ sound-ctx Γ-ctx

  sound-kd : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → ⌞ Γ ⌟Ctx O.⊢ ⌞ k ⌟Kd kd
  sound-kd (kd-⋯ a⇉a⋯a b⇉b⋯b) =
    kd-⋯ (O.Tp∈-⋯-* (sound-Nf⇉ a⇉a⋯a)) (O.Tp∈-⋯-* (sound-Nf⇉ b⇉b⋯b))
  sound-kd (kd-Π j-kd k-kd)   = kd-Π (sound-kd j-kd) (sound-kd k-kd)

  sound-Nf⇉ : ∀ {n} {Γ : Ctx n} {a k} →
              Γ ⊢Nf a ⇉ k → ⌞ Γ ⌟Ctx O.⊢Tp ⌞ a ⌟ ∈ ⌞ k ⌟Kd
  sound-Nf⇉ (⇉-⊥-f Γ-ctx)       = ∈-s-i (∈-⊥-f (sound-ctx Γ-ctx))
  sound-Nf⇉ (⇉-⊤-f Γ-ctx)       = ∈-s-i (∈-⊤-f (sound-ctx Γ-ctx))
  sound-Nf⇉ (⇉-∀-f k-kd a⇉a⋯a)  =
    ∈-s-i (∈-∀-f (sound-kd k-kd) (O.Tp∈-⋯-* (sound-Nf⇉ a⇉a⋯a)))
  sound-Nf⇉ (⇉-→-f a⇉a⋯a b⇉b⋯b) =
    ∈-s-i (∈-→-f (O.Tp∈-⋯-* (sound-Nf⇉ a⇉a⋯a)) (O.Tp∈-⋯-* (sound-Nf⇉ b⇉b⋯b)))
  sound-Nf⇉ (⇉-Π-i j-kd a⇉k)    =
    let ⌞a⌟∈⌞k⌟ = sound-Nf⇉ a⇉k
    in ∈-Π-i (sound-kd j-kd) ⌞a⌟∈⌞k⌟
  sound-Nf⇉ (⇉-s-i a⇉b⋯c)       = ∈-s-i (sound-Ne∈ a⇉b⋯c)

  sound-Ne∈ : ∀ {n} {Γ : Ctx n} {a k} →
              Γ ⊢Ne a ∈ k → ⌞ Γ ⌟Ctx O.⊢Tp ⌞ a ⌟ ∈ ⌞ k ⌟Kd
  sound-Ne∈ (∈-∙ x∈j j⇉as⇉k) = sound-Sp⇉ (sound-Var∈ x∈j) j⇉as⇉k

  sound-Sp⇉ : ∀ {n} {Γ : Ctx n} {a bs j k} →
              ⌞ Γ ⌟Ctx O.⊢Tp a ∈ ⌞ j ⌟Kd → Γ ⊢ j ⇉∙ bs ⇉ k →
              ⌞ Γ ⌟Ctx O.⊢Tp a ⌞∙⌟ ⌞ bs ⌟Sp ∈ ⌞ k ⌟Kd
  sound-Sp⇉ a∈⌞j⌟ ⇉-[] = a∈⌞j⌟
  sound-Sp⇉ a∈⌞Πjk⌟ (⇉-∷ b⇇j j-kd k[b]⇉bs⇉l) with O.Tp∈-valid a∈⌞Πjk⌟
  ... | (kd-Π ⌞j⌟-kd ⌞k⌟-kd) =
    let ⌞b⌟∈⌞j⌟ = sound-Nf⇇ b⇇j
    in sound-Sp⇉ (∈-⇑ (∈-Π-e a∈⌞Πjk⌟ ⌞b⌟∈⌞j⌟)
                      (O.≅⇒<∷ (O.kd-⌞⌟-[]-≅ ⌞k⌟-kd ⌞b⌟∈⌞j⌟)))
                 k[b]⇉bs⇉l

  sound-Nf⇇ : ∀ {n} {Γ : Ctx n} {a k} →
              Γ ⊢Nf a ⇇ k → ⌞ Γ ⌟Ctx O.⊢Tp ⌞ a ⌟ ∈ ⌞ k ⌟Kd
  sound-Nf⇇ (⇇-⇑ a⇉j j<∷k) = ∈-⇑ (sound-Nf⇉ a⇉j) (sound-<∷ j<∷k)

  sound-Var∈ : ∀ {n} {Γ : Ctx n} {x k} →
               Γ ⊢Var x ∈ k → ⌞ Γ ⌟Ctx O.⊢Tp var x ∈ ⌞ k ⌟Kd
  sound-Var∈ {_} {Γ} (⇉-var {k} x Γ-ctx Γ[x]≡kd-k) =
    ∈-var x (sound-ctx Γ-ctx) (begin
      TermCtx.lookup ⌞ Γ ⌟Ctx x  ≡⟨ ⌞⌟Asc-lookup Γ x ⟩
      ⌞ lookup Γ x ⌟Asc          ≡⟨ cong ⌞_⌟Asc Γ[x]≡kd-k ⟩
      kd ⌞ k ⌟Kd                 ∎)
    where
      open ≡-Reasoning
      open Substitution using (⌞⌟Asc-weaken)
  sound-Var∈ (⇇-⇑ x∈j j<∷k k-kd) = ∈-⇑ (sound-Var∈ x∈j) (sound-<∷ j<∷k)

  sound-<∷ : ∀ {n} {Γ : Ctx n} {j k} →
             Γ ⊢ j <∷ k → ⌞ Γ ⌟Ctx O.⊢ ⌞ j ⌟Kd <∷ ⌞ k ⌟Kd
  sound-<∷ (<∷-⋯ a₂<:a₁ b₁<:b₂)          =
    <∷-⋯ (sound-<: a₂<:a₁) (sound-<: b₁<:b₂)
  sound-<∷ (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd) =
    <∷-Π (sound-<∷ j₂<∷j₁) (sound-<∷ k₁<∷k₂) (sound-kd Πj₁k₁-kd)

  sound-<: : ∀ {n} {Γ : Ctx n} {a b} →
             Γ ⊢ a <: b → ⌞ Γ ⌟Ctx O.⊢ ⌞ a ⌟ <: ⌞ b ⌟ ∈ *
  sound-<: (<:-trans a<:b b<:c) =
    <:-trans (sound-<: a<:b) (sound-<: b<:c)
  sound-<: (<:-⊥ a⇉a⋯a) = <:-⊥ (O.Tp∈-⋯-* (sound-Nf⇉ a⇉a⋯a))
  sound-<: (<:-⊤ a⇉a⋯a) = <:-⊤ (O.Tp∈-⋯-* (sound-Nf⇉ a⇉a⋯a))
  sound-<: (<:-∀ k₂<∷k₁ a₁<:a₂ Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁) =
    <:-∀ (sound-<∷ k₂<∷k₁) (sound-<: a₁<:a₂)
         (O.Tp∈-⋯-* (sound-Nf⇉ Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁))
  sound-<: (<:-→ a₂<:a₁ b₁<:b₂) =
    <:-→ (sound-<: a₂<:a₁) (sound-<: b₁<:b₂)
  sound-<: (<:-∙ x∈j j⇉as⇉k) =
    O.<:-⋯-* (sound-<:-∙-≃ (<:-refl (sound-Var∈ x∈j)) j⇉as⇉k)
  sound-<: (<:-⟨| a∈b⋯c) = <:-⟨| (sound-Ne∈ a∈b⋯c)
  sound-<: (<:-|⟩ a∈b⋯c) = <:-|⟩ (sound-Ne∈ a∈b⋯c)

  sound-<:⇇ : ∀ {n} {Γ : Ctx n} {a b k} →
              Γ ⊢ a <: b ⇇ k → ⌞ Γ ⌟Ctx O.⊢ ⌞ a ⌟ <: ⌞ b ⌟ ∈ ⌞ k ⌟Kd
  sound-<:⇇ (<:-⇇ (⇇-⇑ a₁⇉c₁⋯d₁ (<∷-⋯ c₁<:c d<:d₁))
                  (⇇-⇑ a₂⇉c₂⋯d₂ (<∷-⋯ c₂<:c d<:d₂)) a<:b)
    with Nf⇉-≡ a₁⇉c₁⋯d₁ | Nf⇉-≡ a₂⇉c₂⋯d₂
  sound-<:⇇ (<:-⇇ (⇇-⇑ a₁⇉a₁⋯a₁ (<∷-⋯ c<:a₁ _))
                  (⇇-⇑ a₂⇉a₂⋯a₂ (<∷-⋯ _ a₂<:d)) a<:b)
    | refl , refl | refl , refl =
      <:-⇑ (<:-⋯-i (sound-<: a<:b)) (<∷-⋯ (sound-<: c<:a₁) (sound-<: a₂<:d))
  sound-<:⇇ (<:-λ a₁<:a₂⇇k Λj₁a₁⇇Πjk Λj₂a₂⇇Πjk) =
    <:-λ (sound-<:⇇ a₁<:a₂⇇k) (sound-Nf⇇ Λj₁a₁⇇Πjk) (sound-Nf⇇ Λj₂a₂⇇Πjk)

  sound-≅ : ∀ {n} {Γ : Ctx n} {j k} →
            Γ ⊢ j ≅ k → ⌞ Γ ⌟Ctx O.⊢ ⌞ j ⌟Kd ≅ ⌞ k ⌟Kd
  sound-≅ (<∷-antisym _ _ j<∷k k<∷j) =
    <∷-antisym (sound-<∷ j<∷k) (sound-<∷ k<∷j)

  sound-≃ : ∀ {n} {Γ : Ctx n} {a b k} →
            Γ ⊢ a ≃ b ⇇ k → ⌞ Γ ⌟Ctx O.⊢ ⌞ a ⌟ ≃ ⌞ b ⌟ ∈ ⌞ k ⌟Kd
  sound-≃ (<:-antisym k-kd a<:b⇇k b<:a⇇k) =
    <:-antisym (sound-<:⇇ a<:b⇇k) (sound-<:⇇ b<:a⇇k)

  sound-<:-∙-≃ : ∀ {n} {Γ : Ctx n} {a b as bs j k} →
                 ⌞ Γ ⌟Ctx O.⊢ a <: b ∈ ⌞ j ⌟Kd → Γ ⊢ j ⇉∙ as ≃ bs ⇉ k →
                 ⌞ Γ ⌟Ctx O.⊢ a ⌞∙⌟ ⌞ as ⌟Sp <: b ⌞∙⌟ ⌞ bs ⌟Sp ∈ ⌞ k ⌟Kd
  sound-<:-∙-≃ a<:b∈⌞j⌟ ≃-[] = a<:b∈⌞j⌟
  sound-<:-∙-≃ a<:b∈⌞Πjk⌟ (≃-∷ c≃d⇇j k[c]⇉cs≃ds⇉l) with O.<:-valid-kd a<:b∈⌞Πjk⌟
  ... | (kd-Π ⌞j⌟-kd ⌞k⌟-kd) =
    let ⌞c⌟≃⌞d⌟∈⌞j⌟ = sound-≃ c≃d⇇j
        ⌞c⌟∈⌞j⌟ , _ = O.≃-valid ⌞c⌟≃⌞d⌟∈⌞j⌟
    in sound-<:-∙-≃ (<:-⇑ (<:-· a<:b∈⌞Πjk⌟ ⌞c⌟≃⌞d⌟∈⌞j⌟)
                          (O.≅⇒<∷ (O.kd-⌞⌟-[]-≅ ⌞k⌟-kd ⌞c⌟∈⌞j⌟)))
                    k[c]⇉cs≃ds⇉l

------------------------------------------------------------------------
-- Completeness of canonical (sub)kinding w.r.t. declarative
-- (sub)kinding

open Substitution hiding (subst)

module TrackSimpleKindsCanonicalEtaExp where
  open RenamingCommutes
  open SimpHSubstLemmas
  private
    module V   = VarSubst
    module TK  = TrackSimpleKindsEtaExp
    module TKE = SimpEtaExp.TrackSimpleKindsKindedEtaExp

  -- Hereditary substitutions of a variable by its well-kinded
  -- η-expansion in well-formed kinds vanish.
  --
  -- NOTE. We will strengthen this lemma below, once we have proven
  -- that η-expansion preserves canonical kinding.
  kd-[]-η-var : ∀ {k n} {Γ : Ctx n} {j l} →
                Γ ⊢ j kd → kd j ∷ Γ ⊢ l kd →
                let j′  = weakenKind′ j in (hyp : ⌊ j′ ⌋≡ k) →
                let η-z = TK.η-exp j′ hyp (var∙ zero)
                in kd j ∷ Γ ⊢Nf η-z ⇇ j′ →
                   kd j ∷ Γ ⊢ (l Kind′/Var V.wk V.↑) Kind[ η-z ∈ ⌊ j′ ⌋ ] ≅ l
  kd-[]-η-var j-kd l-kd hyp η-z⇇j =
    let open TypedVarSubst    typedVarSubst
        open SimpKind.Kinding using (_⊢_kds)
        open SimpleCtx        using (kd)

        j-wf     = wf-kd j-kd
        j-kd′    = kd-weaken j-wf j-kd
        ⌊j⌋≡k    = trans (sym (⌊⌋-Kind′/Var _)) (⌊⌋≡⇒⌊⌋-≡ hyp)
        η-z      = TK.η-exp _ hyp (var∙ zero)
        j-kds′   = subst (λ k → kd k ∷ _ ⊢ _ kds) ⌊j⌋≡k (kd-kds j-kd′)
        l-kds    = subst (λ k → kd k ∷ _ ⊢ _ kds) ⌊j⌋≡k (kd-kds l-kd)
        l[z]≋l   = TKE.kds-[]-η-var [] hyp j-kds′ l-kds
        wk↑∈j∷Γ  = ∈-↑′ j-kd′ (∈-wk j-wf)
        l[z]-kd  = kd-[] (kd-/Var l-kd wk↑∈j∷Γ) η-z⇇j
    in ≋-≅ l[z]-kd l-kd (subst (λ l → _ Kind[ η-z ∈ l ] ≋ _)
                               (sym (⌊⌋≡⇒⌊⌋-≡ hyp)) l[z]≋l)

  -- NOTE. The definition of the function η-exp-Ne∈ below is
  -- structurally recursive in the *shape* parameter k, but *not* in
  -- the kind j because we need to weaken the domain j₁ of the
  -- dependent kind (j = Π j₁ j₂) in the arrow case.  The additional
  -- hypothesis ⌊ j ⌋≡ k ensures that k is indeed the shape of the
  -- kind j.

  -- η-expansion preserves canonical kinding of neutral types.
  η-exp-Ne∈ : ∀ {n} {Γ : Ctx n} {a j k l} (hyp : ⌊ j ⌋≡ k) →
              Γ ⊢ j kd → Γ ⊢Ne a ∈ l → Γ ⊢ l <∷ j → Γ ⊢Nf TK.η-exp j hyp a ⇇ j
  η-exp-Ne∈ is-★ b₂⋯c₂-kd a∈b₁⋯c₁ (<∷-⋯ b₂<:b₁ c₁<:c₂) =
    Nf⇇-⇑ (Nf⇇-ne a∈b₁⋯c₁) (<∷-⋯ b₂<:b₁ c₁<:c₂)
  η-exp-Ne∈ (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) (kd-Π j₁-kd j₂-kd)
            (∈-∙ {x} {_} {_} {as} x∈l l⇉as∈Πl₁l₂)
            (<∷-Π j₁<∷l₁ l₂<∷j₂ (kd-Π l₁-kd l₂-kd)) =
    Nf⇇-Π-i j₁-kd (η-exp-Ne∈ ⌊j₂⌋≡k₂ j₂-kd x∙as·z∈l₂[z] l₂[z]<∷j₂)
    where
      open TypedVarSubst    typedVarSubst

      j₁-wf     = wf-kd j₁-kd
      j₁∷Γ-ctx  = j₁-wf C.∷ Var∈-ctx x∈l
      j₁-kd′    = kd-weaken j₁-wf j₁-kd
      l₁-kd′    = kd-weaken j₁-wf l₁-kd
      ⌊j₁′⌋≡k₁  = ⌊⌋≡-weaken ⌊j₁⌋≡k₁
      η-z       = TK.η-exp _ ⌊j₁′⌋≡k₁ (var∙ zero)
      z⇇j₁      = η-exp-Ne∈ ⌊j₁′⌋≡k₁ j₁-kd′
                            (∈-∙ (⇉-var zero j₁∷Γ-ctx refl) ⇉-[])
                            (<∷-refl j₁-kd′)
      z⇇l₁      = Nf⇇-⇑ z⇇j₁ (<∷-weaken j₁-wf j₁<∷l₁)
      wk↑∈j₁∷Γ  = ∈-↑′ j₁-kd′ (∈-wk j₁-wf)
      j₂[z]<∷j₂ = ≅⇒<∷ (kd-[]-η-var j₁-kd j₂-kd ⌊j₁′⌋≡k₁ z⇇j₁)
      l₂[z]<∷j₂[z] = <∷-[≃] (<∷-/Var l₂<∷j₂ wk↑∈j₁∷Γ) (≃-reflNf⇇ z⇇j₁ j₁-kd′)
      l₂[z]<∷j₂ = subst (λ l → _ ⊢ _ Kind[ η-z ∈ l ] <∷ _)
                        (<∷-⌊⌋ (<∷-weaken j₁-wf j₁<∷l₁))
                        (<∷-trans l₂[z]<∷j₂[z] j₂[z]<∷j₂)
      x∙as·z∈l₂[z] = (∈-∙ (Var∈-weaken j₁-wf x∈l)
                          (⇉-∷ʳ (Sp⇉-weaken j₁-wf l⇉as∈Πl₁l₂) z⇇l₁ l₁-kd′))

private module TK  = TrackSimpleKindsCanonicalEtaExp

-- η-expansion preserves canonical kinding of neutral types.

η-exp-Ne∈ : ∀ {n} {Γ : Ctx n} {a k} →
            Γ ⊢ k kd → Γ ⊢Ne a ∈ k → Γ ⊢Nf η-exp k a ⇇ k
η-exp-Ne∈ k-kd a∈k = TK.η-exp-Ne∈ (⌊⌋-⌊⌋≡ _) k-kd a∈k (<∷-refl k-kd)

η-exp-Var∈ : ∀ {n} {Γ : Ctx n} {x k} → Γ ⊢ k kd → Γ ⊢Var x ∈ k →
             Γ ⊢Nf η-exp k (var∙ x) ⇇ k
η-exp-Var∈ k-kd x∈k = η-exp-Ne∈ k-kd (∈-∙ x∈k ⇉-[])

-- Hereditary substitutions in well-formed kinds of a variable by its
-- η-expansion vanish.
kd-[]-η-var : ∀ {n} {Γ : Ctx n} {j l} → Γ ⊢ j kd → kd j ∷ Γ ⊢ l kd →
              let j′  = weakenKind′ j
                  l′  = l Kind′/Var VarSubst.wk VarSubst.↑
              in kd j ∷ Γ ⊢ l′ Kind[ η-exp j′ (var∙ zero) ∈ ⌊ j′ ⌋ ] ≅ l
kd-[]-η-var j-kd l-kd =
  let j-kd′ = kd-weaken (wf-kd j-kd) j-kd
  in TK.kd-[]-η-var j-kd l-kd (⌊⌋-⌊⌋≡ _)
                    (η-exp-Var∈ j-kd′ (⇉-var zero (kd-ctx j-kd′) refl))

open RenamingCommutesNorm

-- Completeness of canonical (sub)kinding w.r.t. extended declarative
-- (sub)kinding
module CompletenessExtended where

  mutual

    complete-wf : ∀ {n} {Γ : E.Ctx n} {a} → Γ E.⊢ a wf →
                  nfCtx Γ ⊢ nfAsc (nfCtx Γ) a wf
    complete-wf (wf-kd k-kd) = wf-kd (complete-kd k-kd)
    complete-wf (wf-tp a∈*)  = wf-tp (Nf⇇-s-i (complete-Tp∈ a∈*))

    complete-ctx : ∀ {n} {Γ : E.Ctx n} → Γ E.ctx → nfCtx Γ ctx
    complete-ctx E.[]             = C.[]
    complete-ctx (a-wf E.∷ Γ-ctx) = complete-wf a-wf C.∷ complete-ctx Γ-ctx

    complete-kd : ∀ {n} {Γ : E.Ctx n} {k} → Γ E.⊢ k kd →
                  nfCtx Γ ⊢ nfKind (nfCtx Γ) k kd
    complete-kd (kd-⋯ a∈* b∈*)   =
      kd-⋯ (Nf⇇-s-i (complete-Tp∈ a∈*)) (Nf⇇-s-i (complete-Tp∈ b∈*))
    complete-kd (kd-Π j-kd k-kd) = kd-Π (complete-kd j-kd) (complete-kd k-kd)

    complete-Tp∈ : ∀ {n} {Γ : E.Ctx n} {a k} → Γ E.⊢Tp a ∈ k →
                   nfCtx Γ ⊢Nf nf (nfCtx Γ) a ⇇ nfKind (nfCtx Γ) k
    complete-Tp∈ {_} {Γ} (∈-var x Γ-ctx Γ[x]≡kd-k)
      with C.lookup (nfCtx Γ) x | nfCtx-lookup-kd x Γ Γ[x]≡kd-k
    complete-Tp∈ {_} {Γ} (∈-var x Γ-ctx Γ[x]≡kd-k) | kd ._ | refl =
      η-exp-Var∈ (WfCtxOps.lookup-kd x nf-Γ-ctx nf-Γ[x]≡kd-nf-k)
                 (⇉-var x nf-Γ-ctx nf-Γ[x]≡kd-nf-k)
      where
        nf-Γ-ctx        = complete-ctx Γ-ctx
        nf-Γ[x]≡kd-nf-k = nfCtx-lookup-kd x Γ Γ[x]≡kd-k
    complete-Tp∈ (∈-⊥-f Γ-ctx) = Nf⇉-⋯-* (⇉-⊥-f (complete-ctx Γ-ctx))
    complete-Tp∈ (∈-⊤-f Γ-ctx) = Nf⇉-⋯-* (⇉-⊤-f (complete-ctx Γ-ctx))
    complete-Tp∈ (∈-∀-f k-kd a∈*) = Nf⇇-∀-f (complete-kd k-kd) (complete-Tp∈ a∈*)
    complete-Tp∈ (∈-→-f a∈* b∈*)  = Nf⇇-→-f (complete-Tp∈ a∈*) (complete-Tp∈ b∈*)
    complete-Tp∈ (∈-Π-i j-kd a∈k k-kd) =
      Nf⇇-Π-i (complete-kd j-kd) (complete-Tp∈ a∈k)
    complete-Tp∈ (∈-Π-e {a} {b} a∈Πjk b∈j k-kd k[a]-kd) =
      Nf⇇-⇑ (Nf⇇-Π-e′ (complete-Tp∈ a∈Πjk) (complete-Tp∈ b∈j))
            (≅⇒<∷ (≅-nfKind-[] k-kd b∈j k[a]-kd))
    complete-Tp∈ (∈-s-i a∈b⋯c) =
      let nf-a⇉a⋯a = Nf⇇-s-i (complete-Tp∈ a∈b⋯c)
      in ⇇-⇑ nf-a⇉a⋯a (<∷-⋯ (<:-reflNf⇉ nf-a⇉a⋯a) (<:-reflNf⇉ nf-a⇉a⋯a))
    complete-Tp∈ (∈-⇑ a∈j j<∷k) = Nf⇇-⇑ (complete-Tp∈ a∈j) (complete-<∷ j<∷k)

    complete-<∷ : ∀ {n} {Γ : E.Ctx n} {j k} → Γ E.⊢ j <∷ k →
                  nfCtx Γ ⊢ nfKind (nfCtx Γ) j <∷ nfKind (nfCtx Γ) k
    complete-<∷ (<∷-⋯ a₂<:a₁ b₁<:b₂) =
      <∷-⋯ (complete-<:-⋯ a₂<:a₁) (complete-<:-⋯ b₁<:b₂)
    complete-<∷ (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd) with complete-kd Πj₁k₁-kd
    ... | kd-Π nf-j₁-kd nf-k₁-kd =
      let nf-j₂<∷j₁  = complete-<∷ j₂<∷j₁
          nf-k₁′<∷k₂ = complete-<∷ k₁<∷k₂
          ⌊nf-j₁∷Γ⌋≡⌊nf-j₂∷Γ⌋ = cong (λ k → kd k ∷ _) (sym (<∷-⌊⌋ nf-j₂<∷j₁))
          nf-k₁≋k₁′  = ≋-nfKind ⌊nf-j₁∷Γ⌋≡⌊nf-j₂∷Γ⌋ _
          nf-j₂-kd   = proj₁ (<∷-valid nf-j₂<∷j₁)
          nf-k₁′-kd  = proj₁ (<∷-valid nf-k₁′<∷k₂)
          nf-k₁<∷k₁′ = ≋-<∷ (⇓-kd nf-j₂-kd nf-j₂<∷j₁ nf-k₁-kd)
                            nf-k₁′-kd nf-k₁≋k₁′
          nf-k₁<∷k₂ = <∷-trans nf-k₁<∷k₁′ nf-k₁′<∷k₂
      in <∷-Π nf-j₂<∷j₁ nf-k₁<∷k₂ (kd-Π nf-j₁-kd nf-k₁-kd)

    complete-<:-⋯ : ∀ {n} {Γ : E.Ctx n} {a b c d} → Γ E.⊢ a <: b ∈ c ⋯ d →
                    nfCtx Γ ⊢ nf (nfCtx Γ) a <: nf (nfCtx Γ) b
    complete-<:-⋯ a<:b∈c⋯d with complete-<: a<:b∈c⋯d
    complete-<:-⋯ a<:b∈c⋯d | <:-⇇ _ _ a<:b = a<:b

    complete-<: : ∀ {n} {Γ : E.Ctx n} {a b k} → Γ E.⊢ a <: b ∈ k →
                  nfCtx Γ ⊢ nf (nfCtx Γ) a  <:
                    nf (nfCtx Γ) b ⇇ nfKind (nfCtx Γ) k
    complete-<: (<:-refl a∈k) =
      let nf-a∈k  = complete-Tp∈ a∈k
      in <:⇇-reflNf⇇ nf-a∈k (Nf⇇-valid nf-a∈k)
    complete-<: (<:-trans a<:b b<:c) =
      <:⇇-trans (complete-<: a<:b) (complete-<: b<:c)
    complete-<: (<:-β₁ a∈k b∈j a[b]∈k[b] k-kd k[b]-kd) =
      ≃⇒<: (≃-β-nf a∈k b∈j k-kd a[b]∈k[b] k[b]-kd)
    complete-<: (<:-β₂ a∈k b∈j a[b]∈k[b] k-kd k[b]-kd) =
      ≃⇒<: (≃-sym (≃-β-nf a∈k b∈j k-kd a[b]∈k[b] k[b]-kd))
    complete-<: (<:-η₁ a∈Πjk) = ≃⇒<: (≃-η-nf a∈Πjk)
    complete-<: (<:-η₂ a∈Πjk) = ≃⇒<: (≃-sym (≃-η-nf a∈Πjk))
    complete-<: (<:-⊥ a∈b⋯c) = <:-⋯-* (<:-⊥ (Nf⇇-s-i (complete-Tp∈ a∈b⋯c)))
    complete-<: (<:-⊤ a∈b⋯c) = <:-⋯-* (<:-⊤ (Nf⇇-s-i (complete-Tp∈ a∈b⋯c)))
    complete-<: (<:-∀ {a₁ = a₁} k₂<∷k₁ a₁<:a₂ Πk₁a₁∈*) with complete-Tp∈ Πk₁a₁∈*
    ... | (⇇-⇑ (⇉-∀-f nf-k₁-kd nf-a₁⇉a₁⋯a₁) _) =
      let nf-k₂<∷k₁    = complete-<∷ k₂<∷k₁
          nf-a₁′<:a₂   = complete-<:-⋯ a₁<:a₂
          ⌊nf-k₁∷Γ⌋≡⌊nf-k₂∷Γ⌋ = cong (λ k → kd k ∷ _) (sym (<∷-⌊⌋ nf-k₂<∷k₁))
          nf-a₁≈a₁′    = ≈-nf ⌊nf-k₁∷Γ⌋≡⌊nf-k₂∷Γ⌋ a₁
          nf-k₂-kd     = proj₁ (<∷-valid nf-k₂<∷k₁)
          nf-a₁⇉a₁⋯a₁′ = proj₁ (<:-valid nf-a₁′<:a₂)
          nf-a₁<:a₁′   = ≈-<: (⇓-Nf⇉ nf-k₂-kd nf-k₂<∷k₁ nf-a₁⇉a₁⋯a₁)
                              nf-a₁⇉a₁⋯a₁′ nf-a₁≈a₁′
          nf-a₁<:a₂ = <:-trans nf-a₁<:a₁′ nf-a₁′<:a₂
      in <:-⋯-* (<:-∀ nf-k₂<∷k₁ nf-a₁<:a₂ (⇉-∀-f nf-k₁-kd nf-a₁⇉a₁⋯a₁))
    ... | (⇇-⇑ (⇉-s-i ()) _)
    complete-<: (<:-→ a₂<:a₁ b₁<:b₂) =
      <:-⋯-* (<:-→ (complete-<:-⋯ a₂<:a₁) (complete-<:-⋯ b₁<:b₂))
    complete-<: (<:-λ {a₁ = a₁} {a₂} a₁<:a₂∈k Λj₁a₁∈Πjk Λj₂a₂∈Πjk)
      with complete-Tp∈ Λj₁a₁∈Πjk | complete-Tp∈ Λj₂a₂∈Πjk
    ... | ⇇-⇑ (⇉-Π-i nf-j₁-kd nf-a₁⇉k₁) (<∷-Π nf-j<∷j₁ nf-k₁<∷k Πj₁k₁-kd)
        | ⇇-⇑ (⇉-Π-i nf-j₂-kd nf-a₂⇉k₂) (<∷-Π nf-j<∷j₂ nf-k₂<∷k Πj₂k₂-kd) =
      let nf-a₁′<:a₂′⇇k = complete-<: a₁<:a₂∈k
          nf-a₁′⇇k , nf-a₂′⇇k = <:⇇-valid nf-a₁′<:a₂′⇇k
          j-kd          = proj₁ (<∷-valid nf-j<∷j₁)
          k-kd          = proj₂ (<∷-valid nf-k₁<∷k)
          ⌊nf-j₁∷Γ⌋≡⌊nf-j∷Γ⌋  = cong (λ k → kd k ∷ _) (sym (<∷-⌊⌋ nf-j<∷j₁))
          ⌊nf-j∷Γ⌋≡⌊nf-j₂∷Γ⌋  = cong (λ k → kd k ∷ _) (<∷-⌊⌋ nf-j<∷j₂)
          nf-a₁≈a₁′     = ≈-nf ⌊nf-j₁∷Γ⌋≡⌊nf-j∷Γ⌋ a₁
          nf-a₂′≈a₂     = ≈-nf ⌊nf-j∷Γ⌋≡⌊nf-j₂∷Γ⌋ a₂
          nf-a₁<:a₁′⇇k  = ≈-<:⇇ k-kd
                                (⇇-⇑ (⇓-Nf⇉ j-kd nf-j<∷j₁ nf-a₁⇉k₁) nf-k₁<∷k)
                                nf-a₁′⇇k nf-a₁≈a₁′
          nf-a₂′<:a₂⇇k  = ≈-<:⇇ k-kd nf-a₂′⇇k
                                (⇇-⇑ (⇓-Nf⇉ j-kd nf-j<∷j₂ nf-a₂⇉k₂) nf-k₂<∷k)
                                nf-a₂′≈a₂
          nf-a₁<:a₂⇇k   = <:⇇-trans (<:⇇-trans nf-a₁<:a₁′⇇k nf-a₁′<:a₂′⇇k)
                                    nf-a₂′<:a₂⇇k
      in <:-λ nf-a₁<:a₂⇇k
              (⇇-⇑ (⇉-Π-i nf-j₁-kd nf-a₁⇉k₁) (<∷-Π nf-j<∷j₁ nf-k₁<∷k Πj₁k₁-kd))
              (⇇-⇑ (⇉-Π-i nf-j₂-kd nf-a₂⇉k₂) (<∷-Π nf-j<∷j₂ nf-k₂<∷k Πj₂k₂-kd))
    ... | ⇇-⇑ (⇉-Π-i _ _) _ | ⇇-⇑ (⇉-s-i ()) _
    ... | ⇇-⇑ (⇉-s-i ()) _  | _
    complete-<: (<:-· {a₁} {a₂} {b₁} {b₂} a₁<:a₂∈Πjk b₁≃b₂∈j
                      b₁∈j k-kd k[b₁]-kd) =
      let nf-a₁<:a₂⇇Πjk         = complete-<: a₁<:a₂∈Πjk
          nf-a₁⇇Πjk , nf-a₂⇇Πjk = <:⇇-valid nf-a₁<:a₂⇇Πjk
      in <:⇇-⇑ (<:-↓⌜·⌝ nf-a₁<:a₂⇇Πjk (complete-≃ b₁≃b₂∈j))
               (≅⇒<∷ (≅-nfKind-[] k-kd b₁∈j k[b₁]-kd)) (complete-kd k[b₁]-kd)
    complete-<: (<:-⟨| a∈b⋯c) = <:-⋯-* (<:-⟨|-Nf⇇ (complete-Tp∈ a∈b⋯c))
    complete-<: (<:-|⟩ a∈b⋯c) = <:-⋯-* (<:-|⟩-Nf⇇ (complete-Tp∈ a∈b⋯c))
    complete-<: (<:-⋯-i a<:b) = <:⇇-⋯-i (complete-<: a<:b)
    complete-<: (<:-⇑ a<:b∈j j<∷k) =
      let nf-j<∷k = complete-<∷ j<∷k
      in <:⇇-⇑ (complete-<: a<:b∈j) nf-j<∷k (proj₂ (<∷-valid nf-j<∷k))

    complete-≅ : ∀ {n} {Γ : E.Ctx n} {j k} → Γ E.⊢ j ≅ k →
                 nfCtx Γ ⊢ nfKind (nfCtx Γ) j ≅ nfKind (nfCtx Γ) k
    complete-≅ (<∷-antisym j<∷k k<∷j) =
      let nf-j<∷k           = complete-<∷ j<∷k
          nf-j-kd , nf-k-kd = <∷-valid nf-j<∷k
      in <∷-antisym nf-j-kd nf-k-kd nf-j<∷k (complete-<∷ k<∷j)

    complete-≃ : ∀ {n} {Γ : E.Ctx n} {a b k} → Γ E.⊢ a ≃ b ∈ k →
                 nfCtx Γ ⊢ nf (nfCtx Γ) a ≃ nf (nfCtx Γ) b ⇇ nfKind (nfCtx Γ) k
    complete-≃ (<:-antisym a<:b∈k b<:a∈k) =
      let nf-a<:b⇇k = complete-<: a<:b∈k
      in <:-antisym (<:⇇-valid-kd nf-a<:b⇇k) nf-a<:b⇇k (complete-<: b<:a∈k)

    -- η-expansion of normal forms is admissible in canonical kinding.
    ≃-η-nf : ∀ {n} {Γ : E.Ctx n} {a j k} → Γ E.⊢Tp a ∈ Π j k →
             nfCtx Γ ⊢ nf (nfCtx Γ) (Λ j (weaken a · var zero))  ≃
               nf (nfCtx Γ) a ⇇ nfKind (nfCtx Γ) (Π j k)
    ≃-η-nf                 a∈Πjk with complete-Tp∈ a∈Πjk
    ≃-η-nf {_} {Γ} {a} {j} a∈Πjk | nf-a⇇Πjk with Nf⇇-valid nf-a⇇Πjk
    ... | (kd-Π nf-j-kd nf-k-kd) =
      let nf-Γ      = nfCtx Γ
          nf-j      = nfKind nf-Γ j
          nf-j-wf   = wf-kd nf-j-kd
          nf-j-kd′  = kd-weaken nf-j-wf nf-j-kd
          nf-a⇇Πjk′ = subst (kd nf-j ∷ nf-Γ ⊢Nf_⇇ _) (nf-weaken (kd nf-j) a)
                            (Nf⇇-weaken nf-j-wf nf-a⇇Πjk)
          η-z⇇j′    = η-exp-Var∈ nf-j-kd′ (⇉-var zero (kd-ctx nf-j-kd′) refl)
          nf-a·z⇇k[z] = Nf⇇-Π-e′ nf-a⇇Πjk′ η-z⇇j′
          nf-a·z⇇k    = Nf⇇-⇑ nf-a·z⇇k[z] (≅⇒<∷ (kd-[]-η-var nf-j-kd nf-k-kd))
      in ≈-≃ (kd-Π nf-j-kd nf-k-kd) (Nf⇇-Π-i nf-j-kd nf-a·z⇇k) nf-a⇇Πjk
             (≈-η-nf a∈Πjk)

    -- Substitution in well-formed kinds commutes with normalization.
    ≅-nfKind-[] : ∀ {n} {Γ : E.Ctx n} {a j k} →
                  kd k ∷ Γ E.⊢ j kd → Γ E.⊢Tp a ∈ k → Γ E.⊢ j Kind[ a ] kd →
                  nfCtx Γ ⊢ (nfKind (nfCtx (kd k ∷ Γ)) j) Kind[
                    nf (nfCtx Γ) a ∈ ⌊ nfKind (nfCtx Γ) k ⌋ ]  ≅
                      nfKind (nfCtx Γ) (j Kind[ a ])
    ≅-nfKind-[] {_} {Γ} {a} {j} {k} j-kd a∈k j[a]-kd =
      let nf-Γ         = nfCtx Γ
          nf-k         = nfKind nf-Γ k
          nf-a         = nf nf-Γ a
          nf-k∷Γ       = kd nf-k ∷ nf-Γ
          nf-j         = nfKind (nf-k∷Γ) j
          ⌊k⌋≡⌊nf-k⌋   = sym (⌊⌋-nf {_} {nf-Γ} k)
          nf-j-kd      = complete-kd j-kd
          nf-a⇇k       = complete-Tp∈ a∈k
          nf-j[a]-kd   = complete-kd j[a]-kd
          nf-j[a∈⌊k⌋]-kd   = kd-[] nf-j-kd nf-a⇇k
          nf-j[a∈⌊k⌋]≋j[a] = subst (λ l → nf-j Kind[ nf-a ∈ l ] ≋ _)
                                   ⌊k⌋≡⌊nf-k⌋ (≋-sym (nfKind-[] j-kd a∈k))
      in ≋-≅ nf-j[a∈⌊k⌋]-kd nf-j[a]-kd nf-j[a∈⌊k⌋]≋j[a]

    -- β-reduction of normal forms is admissible in canonical kinding.
    ≃-β-nf : ∀ {n} {Γ : E.Ctx n} {a b j k} →
             kd j ∷ Γ E.⊢Tp a ∈ k → Γ E.⊢Tp b ∈ j → kd j ∷ Γ E.⊢ k kd →
             Γ E.⊢Tp a [ b ] ∈ k Kind[ b ] → Γ E.⊢ k Kind[ b ] kd →
             nfCtx Γ ⊢ nf (nfCtx Γ) ((Λ j a) · b)  ≃
               nf (nfCtx Γ) (a [ b ]) ⇇ nfKind (nfCtx Γ) (k Kind[ b ])
    ≃-β-nf {_} {Γ} {a} {b} {j} {k} a∈k b∈j k-kd a[b]∈k[b] k[b]-kd =
      let nf-Γ         = nfCtx Γ
          nf-j         = nfKind nf-Γ j
          nf-b         = nf nf-Γ b
          nf-j∷Γ       = kd nf-j ∷ nf-Γ
          nf-a         = nf (nf-j∷Γ) a
          ⌊j⌋≡⌊nf-j⌋   = sym (⌊⌋-nf {_} {nf-Γ} j)
          nf-a⇇k       = complete-Tp∈ a∈k
          nf-b⇇j       = complete-Tp∈ b∈j
          nf-a[b]⇇k[b] = complete-Tp∈ a[b]∈k[b]
          nf-k[b]-kd   = complete-kd k[b]-kd
          nf-a[b∈⌊j⌋]⇇k[b∈⌊j⌋] = Nf⇇-[] nf-a⇇k nf-b⇇j
          nf-k[b∈⌊j⌋]<∷k[b]    = ≅⇒<∷ (≅-nfKind-[] k-kd b∈j k[b]-kd)
          nf-a[b∈⌊j⌋]⇇k[b]     = Nf⇇-⇑ nf-a[b∈⌊j⌋]⇇k[b∈⌊j⌋] nf-k[b∈⌊j⌋]<∷k[b]
          nf-a[b∈⌊j⌋]≈a[b]     = subst (λ l → nf-a [ nf-b ∈ l ] ≈ _) ⌊j⌋≡⌊nf-j⌋
                                       (≈-sym (nf-[] a∈k b∈j))
      in ≈-≃ nf-k[b]-kd nf-a[b∈⌊j⌋]⇇k[b] nf-a[b]⇇k[b] nf-a[b∈⌊j⌋]≈a[b]

-- Completeness of canonical subkinding and subtyping
-- w.r.t. declarative subkinding and subtyping

complete-<:-⋯ : ∀ {n} {Γ : E.Ctx n} {a b c d} → Γ O.⊢ a <: b ∈ c ⋯ d →
                nfCtx Γ ⊢ nf (nfCtx Γ) a <: nf (nfCtx Γ) b
complete-<:-⋯ = CompletenessExtended.complete-<:-⋯ ∘ E.complete-<:

complete-<: : ∀ {n} {Γ : E.Ctx n} {a b k} → Γ O.⊢ a <: b ∈ k →
              nfCtx Γ ⊢ nf (nfCtx Γ) a <: nf (nfCtx Γ) b ⇇ nfKind (nfCtx Γ) k
complete-<: = CompletenessExtended.complete-<: ∘ E.complete-<:

complete-<∷ : ∀ {n} {Γ : E.Ctx n} {j k} → Γ O.⊢ j <∷ k →
              nfCtx Γ ⊢ nfKind (nfCtx Γ) j <∷ nfKind (nfCtx Γ) k
complete-<∷ = CompletenessExtended.complete-<∷ ∘ E.complete-<∷

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:
module Prelude where

open import Data.Unit using (⊤) public
open import Data.Empty using (⊥) public
open import Function using (id; const; flip) public
open import Data.Sum using (_⊎_; inj₁; inj₂) public
open import Data.Product using (Σ; proj₁; proj₂; _,_; _×_) public
open import Data.Maybe using (Maybe; nothing; just) public
open import Data.Nat using (ℕ; _+_; zero; suc) public
open import Data.Fin using (Fin; zero; suc; toℕ; fromℕ) public
open import Data.Vec using (Vec; _∷_; []) public
open import Data.String using (String) public
open import Data.Float using (Float) renaming (show to primShowFloat) public

open import Agda.Builtin.Float

variable S T A B C D S' T' A' B' : Set

-- redefine Bool to avoid COMPILE JS pragma on std-lib's Bool
data Bool : Set where
  false true : Bool

not : Bool → Bool
not true = false
not false = true

if_then_else_ : Bool → A → A → A
if true  then a else b = a
if false then a else b = b

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

maybe : B → (A → B) → Maybe A → B
maybe b f nothing = b
maybe b f (just x) = f x

mapMaybe : (A → B) → Maybe A → Maybe B
mapMaybe f = maybe nothing λ a → just (f a)

data _⊍_ (A B : Set) : Set where
  inj₁ : A → A ⊍ B
  inj₂ : B → A ⊍ B
  both : A → B → A ⊍ B

variable n : ℕ

postulate
  showNat           : ℕ → String
  primStringAppend  : String → String → String
  primParseFloat    : String → Float
  isNaN             : Float → Bool
{-# COMPILE JS showNat          = a=>JSON.stringify(a) #-}
{-# COMPILE JS primStringAppend = a=>b=>a+b #-}
{-# COMPILE JS primParseFloat   = a=>Number(a) #-}
{-# COMPILE JS isNaN            = a=>b=>b[isNaN(a)?1:0]() #-}

Iso   = λ (S T A B : Set) → (S → A) × (B → T)
Lens  = λ (S T A B : Set) → S → A × (B → T)
Prism = λ (S T A B : Set) → (S → A ⊎ T) × (B → T)

plusIso : Float → Iso Float Float Float Float
plusIso x = primFloatPlus x , λ y → primFloatMinus y x

mulIso : Float → Iso Float Float Float Float
mulIso x = primFloatTimes x , λ y → primFloatDiv y x

prismToLens : Prism S T A B → Lens (Maybe S) (Maybe T) (Maybe A) (Maybe B)
prismToLens (p1 , p2) nothing = nothing , mapMaybe p2
prismToLens (p1 , p2) (just s) with p1 s
... | inj₁ a = just a , mapMaybe p2
... | inj₂ t = nothing , const (just t)

floatPrism : Prism String (Maybe String) Float Float
floatPrism = parse , (λ x → just (primShowFloat x))
  where
    parse : String → _
    parse s = if isNaN p then inj₂ nothing else inj₁ p
      where
        p = primParseFloat s


text:
open import AEff
open import EffectAnnotations
open import Types hiding (``)

open import Relation.Binary.PropositionalEquality hiding ([_] ; Extensionality)

module Renamings where

-- SET OF RENAMINGS BETWEEN CONTEXTS

data Ren : Ctx → Ctx → Set where

  ⟨_,_⟩ : {Γ Γ' : Ctx} {X : VType} →
          Ren Γ Γ' →
          X ∈ Γ' →
          --------------------------
          Ren (Γ ∷ X) Γ'

  ε     : {Γ' : Ctx} →
          ------------
          Ren [] Γ'

  π     : {Γ Γ' : Ctx} {X : VType} →
          Ren Γ Γ' →
          --------------------------
          Ren Γ (Γ' ∷ X)

  φ     : {Γ Γ' : Ctx} →
          Ren Γ Γ' →
          ----------------
          Ren (Γ ■) (Γ' ■)

-- RENAMING VARIABLES

ren-var : {Γ Γ' : Ctx} {X : VType} →
          Ren Γ Γ' →
          X ∈ Γ →
          --------------------------
          X ∈ Γ'

ren-var ⟨ f , x ⟩ Hd =
  x
ren-var (π f) Hd =
  Tl-v (ren-var f Hd)
ren-var ⟨ f , y ⟩ (Tl-v x) =
  ren-var f x
ren-var (π f) (Tl-v x) =
  Tl-v (ren-var f (Tl-v x))
ren-var (π f) (Tl-■ p x) =
  Tl-v (ren-var f (Tl-■ p x))
ren-var (φ f) (Tl-■ p x) =
  Tl-■ p (ren-var f x)

-- IDENTITY RENAMING

ren-id : {Γ : Ctx} →
         -----------
         Ren Γ Γ

ren-id {[]} =
  ε
ren-id {Γ ∷ X} =
  ⟨ π ren-id , Hd ⟩
ren-id {Γ ■} =
  φ ren-id

-- EXCHANGE RENAMING

ren-exch : {Γ : Ctx} {X Y : VType} →
           ---------------------------
           Ren (Γ ∷ X ∷ Y) (Γ ∷ Y ∷ X)

ren-exch {Γ} = ⟨ ⟨ π (π ren-id) , Hd ⟩ , Tl-v Hd ⟩

-- COMPOSITION OF RENAMINGS

ren-comp : {Γ Γ' Γ'' : Ctx} →
           Ren Γ' Γ'' →
           Ren Γ Γ' →
           ------------------
           Ren Γ Γ''

ren-comp g ⟨ f , x ⟩ =
  ⟨ ren-comp g f , ren-var g x ⟩
ren-comp g ε =
  ε
ren-comp ⟨ g , x ⟩ (π f) =
  ren-comp g f
ren-comp (π g) (π f) =
  π (ren-comp g (π f))
ren-comp (π g) (φ f) =
  π (ren-comp g (φ f))
ren-comp (φ g) (φ f) =
  φ (ren-comp g f)

-- WEAKENING OF RENAMINGS

ren-wk : {Γ : Ctx} {X : VType} →
         -----------------------
         Ren Γ (Γ ∷ X)

ren-wk =
  π ren-id

-- CONGRUENCE OF RENAMINGS

ren-cong : {Γ Γ' : Ctx} {X : VType} →
           Ren Γ Γ' →
           --------------------------
           Ren (Γ ∷ X) (Γ' ∷ X)

ren-cong f =
  ⟨ π f , Hd ⟩

-- ACTION OF RENAMING ON WELL-TYPED VALUES AND COMPUTATIONS

mutual

  V-rename : {X : VType} {Γ Γ' : Ctx} →
             Ren Γ Γ' →
             Γ ⊢V⦂ X →
             --------------------------
             Γ' ⊢V⦂ X

  V-rename f (` x) =
    ` ren-var f x
  V-rename f (´ c) =
    ´ c
  V-rename f ⋆ =
    ⋆
  V-rename f (ƛ M) =
    ƛ (C-rename (ren-cong f) M)
  V-rename f ⟨ V ⟩ =
    ⟨ V-rename f V ⟩
  V-rename f (□ V) =
    □ (V-rename (φ f) V)

  C-rename : {C : CType} {Γ Γ' : Ctx} →
             Ren Γ Γ' →
             Γ ⊢C⦂ C →
             --------------------------
             Γ' ⊢C⦂ C

  C-rename f (return V) =
    return (V-rename f V)
  C-rename f (let= M `in N) =
    let= C-rename f M `in C-rename (ren-cong f) N
  C-rename f (V · W) =
    V-rename f V · V-rename f W
  C-rename f (↑ op p V M) =
    ↑ op p (V-rename f V) (C-rename f M)
  C-rename f (↓ op V M) =
    ↓ op (V-rename f V) (C-rename f M)
  C-rename f (promise op ∣ p ↦ M `in N) =
    promise op ∣ p ↦ C-rename (ren-cong (ren-cong f)) M `in C-rename (ren-cong f) N
  C-rename f (await V until M) =
    await (V-rename f V) until (C-rename (ren-cong f) M)
  C-rename f (unbox V `in M) =
    unbox (V-rename f V) `in (C-rename (ren-cong f) M)
  C-rename f (spawn M N) =
    spawn (C-rename (φ f) M) (C-rename f N)
  C-rename f (coerce p q M) =
    coerce p q (C-rename f M)

-- ACTION OF RENAMING ON WELL-TYPED PROCESSES

P-rename : {o : O} {PP : PType o} {Γ Γ' : Ctx} → Ren Γ Γ' → Γ ⊢P⦂ PP → Γ' ⊢P⦂ PP
P-rename f (run M) =
  run (C-rename f M)
P-rename f (P ∥ Q) =
  P-rename f P ∥ P-rename f Q
P-rename f (↑ op p V P) =
  ↑ op p (V-rename f V) (P-rename f P)
P-rename f (↓ op V P) =
  ↓ op (V-rename f V) (P-rename f P)

max_stars_repo_name: danelahman/higher-order-aeff-agda

max_issues_repo_name: danelahman/modal-aeff-agda

max_forks_repo_name: danelahman/modal-aeff-agda


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

open import Agda.Primitive
open import Prelude
open import GSeTT.Syntax

{- Typing Rules and basic syntactic properties for the type theory for globular sets -}
module GSeTT.Rules where
  {- Well-formedness statements ≡ inference rules -}
  data _⊢C : Pre-Ctx → Set₁
  data _⊢T_ : Pre-Ctx → Pre-Ty → Set₁
  data _⊢t_#_ : Pre-Ctx → Pre-Tm → Pre-Ty → Set₁
  data _⊢S_>_ : Pre-Ctx → Pre-Sub → Pre-Ctx → Set₁

  data _⊢C where
    ec : nil ⊢C
    cc : ∀ {Γ x A} → Γ ⊢C → Γ ⊢T A → x == length Γ → (Γ :: (x , A)) ⊢C

  data _⊢T_ where
    ob : ∀ {Γ} → Γ ⊢C → Γ ⊢T ∗
    ar : ∀ {Γ A t u} → Γ ⊢t t # A → Γ ⊢t u # A → Γ ⊢T ⇒ A t u

  data _⊢t_#_ where
    var : ∀ {Γ x A} → Γ ⊢C → x # A ∈ Γ → Γ ⊢t (Var x) # A

  data _⊢S_>_ where
    es : ∀ {Δ} → Δ ⊢C → Δ ⊢S nil > nil
    sc : ∀ {Δ Γ γ x y A t} → Δ ⊢S γ > Γ → (Γ :: (x , A)) ⊢C → (Δ ⊢t t # (A [ γ ]Pre-Ty)) → x == y → Δ ⊢S (γ :: (y , t)) > (Γ :: (x , A))

  {- Weakening admissibility -}

  wkT : ∀ {Γ A y B} → Γ ⊢T A → (Γ :: (y , B)) ⊢C → (Γ :: (y , B)) ⊢T A
  wkt : ∀ {Γ A t y B} → Γ ⊢t t # A → (Γ :: (y , B)) ⊢C → (Γ :: (y , B)) ⊢t t # A

  wkT (ob _) Γ,y:B⊢ = ob Γ,y:B⊢
  wkT (ar Γ⊢t:A Γ⊢u:A) Γ,y:B⊢ = ar (wkt Γ⊢t:A Γ,y:B⊢) (wkt Γ⊢u:A Γ,y:B⊢)
  wkt (var Γ⊢C x∈Γ) Γ,y:B⊢ = var Γ,y:B⊢ (inl x∈Γ)

  wkS : ∀ {Δ Γ γ y B} → Δ ⊢S γ > Γ → (Δ :: (y , B)) ⊢C → (Δ :: (y , B)) ⊢S γ > Γ
  wkS (es _) Δ,y:B⊢ = es Δ,y:B⊢
  wkS (sc Δ⊢γ:Γ Γ,x:A⊢ Δ⊢t:A[γ] idp) Δ,y:B⊢ = sc (wkS Δ⊢γ:Γ Δ,y:B⊢) Γ,x:A⊢ (wkt Δ⊢t:A[γ] Δ,y:B⊢) idp

  {- Consistency : all objects appearing in derivable judgments are derivable -}
  Γ⊢A→Γ⊢ : ∀ {Γ A} → Γ ⊢T A → Γ ⊢C
  Γ⊢t:A→Γ⊢ : ∀ {Γ A t} → Γ ⊢t t # A → Γ ⊢C

  Γ⊢A→Γ⊢ (ob Γ⊢) = Γ⊢
  Γ⊢A→Γ⊢ (ar Γ⊢t:A Γ⊢u:A) = Γ⊢t:A→Γ⊢ Γ⊢t:A
  Γ⊢t:A→Γ⊢ (var Γ⊢ _) = Γ⊢

  Δ⊢γ:Γ→Γ⊢ : ∀ {Δ Γ γ} → Δ ⊢S γ > Γ → Γ ⊢C
  Δ⊢γ:Γ→Γ⊢ (es Δ⊢) = ec
  Δ⊢γ:Γ→Γ⊢ (sc Δ⊢γ:Γ Γ,x:A⊢ Δ⊢t:A[γ] idp) = Γ,x:A⊢

  Δ⊢γ:Γ→Δ⊢ : ∀ {Δ Γ γ} → Δ ⊢S γ > Γ → Δ ⊢C
  Δ⊢γ:Γ→Δ⊢ (es Δ⊢) = Δ⊢
  Δ⊢γ:Γ→Δ⊢ (sc Δ⊢γ:Γ Γ,x:A⊢ Δ⊢t:A[γ] idp) = Δ⊢γ:Γ→Δ⊢ Δ⊢γ:Γ

  Γ,x:A⊢→Γ,x:A⊢A : ∀ {Γ x A} → (Γ :: (x , A)) ⊢C → (Γ :: (x , A)) ⊢T A
  Γ,x:A⊢→Γ,x:A⊢A Γ,x:A⊢@(cc Γ⊢ Γ⊢A idp) = wkT Γ⊢A Γ,x:A⊢

  Γ,x:A⊢→Γ,x:A⊢x:A : ∀ {Γ x A} → (Γ :: (x , A)) ⊢C → (Γ :: (x , A)) ⊢t (Var x) # A
  Γ,x:A⊢→Γ,x:A⊢x:A Γ,x:A⊢ = var Γ,x:A⊢ (inr (idp , idp))

  Γ,x:A⊢→Γ⊢ : ∀ {Γ x A} → (Γ :: (x , A)) ⊢C → Γ ⊢C
  Γ,x:A⊢→Γ⊢ (cc Γ⊢ _ _) = Γ⊢

  Γ⊢t:A→Γ⊢A : ∀ {Γ A t} → Γ ⊢t t # A → Γ ⊢T A
  Γ⊢t:A→Γ⊢A (var Γ,x:A⊢@(cc Γ⊢ Γ⊢A idp) (inl y∈Γ)) = wkT (Γ⊢t:A→Γ⊢A (var Γ⊢ y∈Γ)) Γ,x:A⊢
  Γ⊢t:A→Γ⊢A (var Γ,x:A⊢@(cc _ _ idp) (inr (idp , idp))) = Γ,x:A⊢→Γ,x:A⊢A Γ,x:A⊢

  Γ⊢src : ∀ {Γ A t u} → Γ ⊢T ⇒ A t u → Γ ⊢t t # A
  Γ⊢src (ar Γ⊢t Γ⊢u) = Γ⊢t

  Γ⊢tgt : ∀ {Γ A t u} → Γ ⊢T ⇒ A t u → Γ ⊢t u # A
  Γ⊢tgt (ar Γ⊢t Γ⊢u) = Γ⊢u

  {- Cut-admissibility -}
  -- notational shortcut : if A = B a term of type A is also of type B
  trT : ∀ {Γ A B t} → A == B → Γ ⊢t t # A → Γ ⊢t t # B
  trT idp Γ⊢t:A = Γ⊢t:A

  n∉Γ : ∀ {Γ A n} → Γ ⊢C → (length Γ ≤ n) → ¬ (n # A ∈ Γ)
  n∉Γ (cc Γ⊢ _ _) l+1≤n (inl n∈Γ) = n∉Γ Γ⊢ (Sn≤m→n≤m l+1≤n) n∈Γ
  n∉Γ (cc Γ⊢ _ idp) Sn≤n (inr (idp , idp)) = Sn≰n _ Sn≤n

  lΓ∉Γ : ∀ {Γ A} → Γ ⊢C → ¬ ((length Γ) # A ∈ Γ)
  lΓ∉Γ Γ⊢ = n∉Γ Γ⊢ (n≤n _)

  Γ+⊢l : ∀ {Γ x A} → (Γ :: (x , A)) ⊢C → x == length Γ
  Γ+⊢l (cc _ _ idp) = idp

  {- action on weakened types and terms -}
  wk[]T : ∀ {Γ Δ γ x u A B} → Γ ⊢T A → Δ ⊢S (γ :: (x , u)) > (Γ :: (x , B)) → (A [ (γ :: (x , u)) ]Pre-Ty) == (A [ γ ]Pre-Ty)
  wk[]t : ∀ {Γ Δ γ x u A t B} → Γ ⊢t t # A → Δ ⊢S (γ :: (x , u)) > (Γ :: (x , B)) → (t [ (γ :: (x , u)) ]Pre-Tm) == (t [ γ ]Pre-Tm)

  wk[]T (ob Γ⊢) _ = idp
  wk[]T (ar Γ⊢t:A Γ⊢u:A) Δ⊢γ+:Γ+ = ⇒= (wk[]T (Γ⊢t:A→Γ⊢A Γ⊢t:A) Δ⊢γ+:Γ+)  (wk[]t Γ⊢t:A Δ⊢γ+:Γ+) (wk[]t Γ⊢u:A Δ⊢γ+:Γ+)
  wk[]t {x = x} (var {x = y} Γ⊢ y∈Γ) Δ⊢γ+:Γ+ with (eqdecℕ y x)
  wk[]t {x = x} (var {x = y} Γ⊢ y∈Γ) Δ⊢γ+:Γ+ | inr _ = idp
  wk[]t (var {Γ = Γ} Γ⊢ x∈Γ) Δ⊢γ+:Γ+ | inl idp = ⊥-elim (lΓ∉Γ Γ⊢ (transport {B = λ n → n # _ ∈ Γ} (Γ+⊢l (Δ⊢γ:Γ→Γ⊢ Δ⊢γ+:Γ+)) x∈Γ))

  dim[] : ∀ (A : Pre-Ty) (γ : Pre-Sub) → dim (A [ γ ]Pre-Ty) == dim A
  dim[] ∗ γ = idp
  dim[] (⇒ A x x₁) γ = S= (dim[] A γ)

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization