text:
import      Lvl
open import Type

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

open import Functional

module Propositional where
  -- Rules of bottom
  record Bottom(⊥ : Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
    field
      elim  : ∀{X} → Proof(⊥) → Proof(X)

  -- Rules of top
  record Top(⊤ : Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
    field
      intro : Proof(⊤)

  -- Rules of conjunction
  record Conjunction(_∧_ : Formula → Formula → Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
    field
      intro : ∀{X Y} → Proof(X) → Proof(Y) → Proof(X ∧ Y)
      elimₗ  : ∀{X Y} → Proof(X ∧ Y) → Proof(X)
      elimᵣ  : ∀{X Y} → Proof(X ∧ Y) → Proof(Y)

    redundancyₗ : ∀{X} → Proof(X ∧ X) ← Proof(X)
    redundancyₗ x = intro x x

    redundancyᵣ : ∀{X} → Proof(X ∧ X) → Proof(X)
    redundancyᵣ = elimₗ

    transitivity : ∀{X Y Z} → Proof(X ∧ Y) → Proof(Y ∧ Z) → Proof(X ∧ Z)
    transitivity xy yz = intro(elimₗ xy) (elimᵣ yz)

    commutativity : ∀{X Y} → Proof(X ∧ Y) → Proof(Y ∧ X)
    commutativity xy = intro(elimᵣ xy) (elimₗ xy)

    associativityₗ : ∀{X Y Z} → Proof((X ∧ Y) ∧ Z) ← Proof(X ∧ (Y ∧ Z))
    associativityₗ xyz = intro (intro (elimₗ xyz) (elimₗ(elimᵣ xyz))) (elimᵣ(elimᵣ xyz))

    associativityᵣ : ∀{X Y Z} → Proof((X ∧ Y) ∧ Z) → Proof(X ∧ (Y ∧ Z))
    associativityᵣ xyz = intro (elimₗ(elimₗ xyz)) (intro (elimᵣ(elimₗ xyz)) (elimᵣ xyz))

  -- Rules of implication
  record Implication(_⟶_ : Formula → Formula → Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
    field
      intro : ∀{X Y} → (Proof(X) → Proof(Y)) → Proof(X ⟶ Y)
      elim  : ∀{X Y} → Proof(X ⟶ Y) → Proof(X) → Proof(Y)

    reflexivity : ∀{X} → Proof(X ⟶ X)
    reflexivity = intro id

    transitivity : ∀{X Y Z} → Proof(X ⟶ Y) → Proof(Y ⟶ Z) → Proof(X ⟶ Z)
    transitivity xy yz = intro((elim yz) ∘ (elim xy))

  -- Rules of reversed implication
  record Consequence(_⟵_ : Formula → Formula → Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
    field
      intro : ∀{X Y} → (Proof(X) → Proof(Y)) → Proof(Y ⟵ X)
      elim  : ∀{X Y} → Proof(Y ⟵ X) → Proof(X) → Proof(Y)

    reflexivity : ∀{X} → Proof(X ⟵ X)
    reflexivity = intro id

    transitivity : ∀{X Y Z} → Proof(X ⟵ Y) → Proof(Y ⟵ Z) → Proof(X ⟵ Z)
    transitivity xy yz = intro((elim xy) ∘ (elim yz))

  -- Rules of equivalence
  record Equivalence(_⟷_ : Formula → Formula → Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
    field
      intro : ∀{X Y} → (Proof(X) ← Proof(Y)) → (Proof(X) → Proof(Y)) → Proof(X ⟷ Y)
      elimₗ  : ∀{X Y} → Proof(X ⟷ Y) → Proof(Y) → Proof(X)
      elimᵣ  : ∀{X Y} → Proof(X ⟷ Y) → Proof(X) → Proof(Y)

    reflexivity : ∀{X} → Proof(X ⟷ X)
    reflexivity = intro id id

    commutativity : ∀{X Y} → Proof(X ⟷ Y) → Proof(Y ⟷ X)
    commutativity xy = intro(elimᵣ xy) (elimₗ xy)

    transitivity : ∀{X Y Z} → Proof(X ⟷ Y) → Proof(Y ⟷ Z) → Proof(X ⟷ Z)
    transitivity xy yz = intro ((elimₗ xy) ∘ (elimₗ yz)) ((elimᵣ yz) ∘ (elimᵣ xy))

  -- Rules of disjunction
  record Disjunction(_∨_  : Formula → Formula → Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
    field
      introₗ : ∀{X Y} → Proof(X) → Proof(X ∨ Y)
      introᵣ : ∀{X Y} → Proof(Y) → Proof(X ∨ Y)
      elim  : ∀{X Y Z} → (Proof(X) → Proof(Z)) → (Proof(Y) → Proof(Z)) → Proof(X ∨ Y) → Proof(Z)

    redundancyₗ : ∀{X} → Proof(X ∨ X) ← Proof(X)
    redundancyₗ = introₗ

    redundancyᵣ : ∀{X} → Proof(X ∨ X) → Proof(X)
    redundancyᵣ = elim id id

    commutativity : ∀{X Y} → Proof(X ∨ Y) → Proof(Y ∨ X)
    commutativity = elim(introᵣ)(introₗ)

    associativityₗ : ∀{X Y Z} → Proof((X ∨ Y) ∨ Z) ← Proof(X ∨ (Y ∨ Z))
    associativityₗ = elim(introₗ ∘ introₗ) (elim (introₗ ∘ introᵣ) (introᵣ))

    associativityᵣ : ∀{X Y Z} → Proof((X ∨ Y) ∨ Z) → Proof(X ∨ (Y ∨ Z))
    associativityᵣ = elim(elim (introₗ) (introᵣ ∘ introₗ)) (introᵣ ∘ introᵣ)

  -- Rules of negation
  record Negation(¬_ : Formula → Formula) {⊥} ⦃ _ : Bottom(⊥) ⦄ : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
    open Bottom ⦃ ... ⦄
    field
      intro : ∀{X} → (Proof(X) → Proof(⊥)) → Proof(¬ X)
      elim  : ∀{X} → Proof(¬ X) → Proof(X) → Proof(⊥)

  record Signature : Type{ℓₗ} where
    infixl 1005 _∧_
    infixl 1000 _⟶_
    infixl 1000 _⟵_
    infixl 1000 _⟷_
    infixl 1004 _∨_
    infixl 1010 ¬_

    field
      ⊥    : Formula
      ⊤    : Formula
      _∧_  : Formula → Formula → Formula
      _⟶_ : Formula → Formula → Formula
      _⟷_ : Formula → Formula → Formula
      _∨_  : Formula → Formula → Formula
      ¬_   : Formula → Formula

    _⟵_ : Formula → Formula → Formula
    _⟵_ = swap _⟶_

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

    field
      instance ⦃ bottom ⦄      : Bottom(⊥)
      instance ⦃ top ⦄         : Top(⊤)
      instance ⦃ conjunction ⦄ : Conjunction(_∧_)
      instance ⦃ disjunction ⦄ : Disjunction(_∨_)
      instance ⦃ implication ⦄ : Implication(_⟶_)
      instance ⦃ consequence ⦄ : Consequence(_⟵_)
      instance ⦃ equivalence ⦄ : Equivalence(_⟷_)
      instance ⦃ negation ⦄    : Negation(¬_) ⦃ bottom ⦄

    module [⊥] = Bottom      (bottom)
    module [⊤] = Top         (top)
    module [∧] = Conjunction (conjunction)
    module [∨] = Disjunction (disjunction)
    module [→] = Implication (implication)
    module [←] = Consequence (consequence)
    module [↔] = Equivalence (equivalence)
    module [¬] = Negation    (negation)

module Domained {ℓₒ} (Domain : Type{ℓₒ}) where
  module Predicate where
    record UniversalQuantification(∀ₗ : (Domain → Formula) → Formula) : Type{ℓₘₗ Lvl.⊔ (ℓₗ Lvl.⊔ ℓₒ)} where
      field
        intro : ∀{P : Domain → Formula} → (∀{x : Domain} → Proof(P(x))) → Proof(∀ₗ P)
        elim  : ∀{P : Domain → Formula} → Proof(∀ₗ P) → (∀{x : Domain} → Proof(P(x)))

    record ExistentialQuantification(∃ₗ : (Domain → Formula) → Formula) : Type{ℓₘₗ Lvl.⊔ (ℓₗ Lvl.⊔ ℓₒ)} where
      field
        intro : ∀{P : Domain → Formula}{a} → Proof(P(a)) → Proof(∃ₗ P)
        elim  : ∀{P : Domain → Formula}{Z : Formula} → (∀{x : Domain} → Proof(P(x)) → Proof(Z)) → Proof(∃ₗ P) → Proof(Z)

    -- These allows the creation of new symbols which points to something which exists and is unique.
    -- TODO: Does this make this theory have no models? For functions, the functions in the meta-theory here (Agda-functions) represent computable things, and all unique existances are not computable. Normally in set theory, one could interpret every (f(x) = y)-formula as ((x,y) ∈ f), so normally it probably works out in the end of the day?
    record ExistentialWitness(∃ₗ : (Domain → Formula) → Formula) : Type{ℓₘₗ Lvl.⊔ (ℓₗ Lvl.⊔ ℓₒ)} where
      field
        [∃]-witness : ∀{P : Domain → Formula} → ⦃ _ : Proof(∃ₗ P) ⦄ → Domain
        [∃]-proof   : ∀{P : Domain → Formula} → ⦃ p : Proof(∃ₗ P) ⦄ → Proof(P([∃]-witness{P} ⦃ p ⦄))

    record Signature : Type{ℓₗ Lvl.⊔ ℓₒ} where
      field
        ∀ₗ : (Domain → Formula) → Formula
        ∃ₗ : (Domain → Formula) → Formula

      NonEmptyDomain = ∀{P} → Proof(P) → Proof(∃ₗ(const P))

    -- A theory of constructive predicate/(first-order) logic expressed using natural deduction rules
    record Theory ⦃ sign : Signature ⦄ : Type{ℓₘₗ Lvl.⊔ (ℓₗ Lvl.⊔ ℓₒ)} where
      open Signature(sign)

      field
        instance ⦃ universalQuantification ⦄   : UniversalQuantification(∀ₗ)
        instance ⦃ existentialQuantification ⦄ : ExistentialQuantification(∃ₗ)

      module [∀] = UniversalQuantification   (universalQuantification)
      module [∃] = ExistentialQuantification (existentialQuantification)

      module NonEmptyDomain ⦃ nonEmptyDomain : NonEmptyDomain ⦄ where
        [∀]-redundancyₗ : ∀{φ} → Proof(∀ₗ(const φ)) ← Proof(φ)
        [∀]-redundancyₗ (proof) = [∀].intro(\{_} → proof)

        [∀]-redundancyᵣ : ∀{φ} → Proof(∀ₗ(const φ)) → Proof(φ)
        [∀]-redundancyᵣ (proof) = [∃].elim(\{x} → _ ↦ [∀].elim(proof){x}) (nonEmptyDomain proof)

        [∃]-redundancyₗ : ∀{φ} → Proof(∃ₗ(const φ)) ← Proof(φ)
        [∃]-redundancyₗ (proof) = [∃].elim(\{x} → _ ↦ [∃].intro{_}{x}(proof)) (nonEmptyDomain proof)

        [∃]-redundancyᵣ : ∀{φ} → Proof(∃ₗ(const φ)) → Proof(φ)
        [∃]-redundancyᵣ = [∃].elim(\{_} → id)

  module Equality where
    -- Rules of equality
    record Equality(_≡_ : Domain → Domain → Formula) : Type{ℓₘₗ Lvl.⊔ (ℓₗ Lvl.⊔ ℓₒ)} where
      field
        intro : ∀{x} → Proof(x ≡ x)
        elimᵣ  : ∀{P : Domain → Formula}{a b} → Proof(a ≡ b) → Proof(P(a)) → Proof(P(b))

      symmetry : ∀{a b} → Proof(a ≡ b) → Proof(b ≡ a)
      symmetry{a} (proof) = elimᵣ{x ↦ x ≡ a} (proof) (intro{a})

      elimₗ : ∀{P : Domain → Formula}{a b} → Proof(a ≡ b) → Proof(P(a)) ← Proof(P(b))
      elimₗ (proof) (pb) = elimᵣ (symmetry proof) (pb)

      transitivity : ∀{a b c} → Proof(a ≡ b) → Proof(b ≡ c) → Proof(a ≡ c)
      transitivity (ab) (bc) = elimᵣ bc ab

    record Signature : Type{ℓₗ Lvl.⊔ ℓₒ} where
      infixl 2000 _≡_
      field
        _≡_ : Domain → Domain → Formula

    module PropositionallyDerivedSignature ⦃ propositional : Propositional.Signature ⦄ ⦃ sign : Signature ⦄ where
      open Propositional.Signature(propositional)
      open Signature(sign)

      _≢_ : Domain → Domain → Formula
      _≢_ a b = ¬(_≡_ a b)

    record Theory ⦃ sign : Signature ⦄ : Type{ℓₘₗ Lvl.⊔ (ℓₗ Lvl.⊔ ℓₒ)} where
      open Signature(sign)

      field
        instance ⦃ equality ⦄ : Equality(_≡_)

      module [≡] = Equality(equality)

  module Uniqueness ⦃ propositionalSign : Propositional.Signature ⦄ ⦃ predicateSign : Predicate.Signature ⦄ ⦃ equalitySign : Equality.Signature ⦄ where
    open Propositional.Signature(propositionalSign)
    open Predicate.Signature(predicateSign)
    open Equality.Signature(equalitySign)

    module Signature where
      -- Definition of uniqueness of a property.
      -- This means that there is at most one element that satisfies this property.
      -- This is similiar to "Injective" for functions, but this is for statements.
      Unique : (Domain → Formula) → Formula
      Unique(P) = ∀ₗ(x ↦ ∀ₗ(y ↦ (P(x) ∧ P(y)) ⟶ (x ≡ y)))

      -- Definition of existence of an unique element satisfying a property.
      -- This means that there is one and only one element that satisfies this property.
      ∃ₗ! : (Domain → Formula) → Formula
      ∃ₗ! P = ((∃ₗ P) ∧ Unique(P))

    module _ ⦃ propositional : Propositional.Theory ⦄ ⦃ predicate : Predicate.Theory ⦄ ⦃ equality : Equality.Theory ⦄ where
      open Signature
      open Propositional.Theory(propositional)
      open Predicate.Theory(predicate)
      open Equality.Theory(equality)

      module WitnessTheory ⦃ existentialWitness : Predicate.ExistentialWitness(∃ₗ) ⦄ where
        open Predicate.ExistentialWitness(existentialWitness)

        [∃!]-witness : ∀{P : Domain → Formula} → ⦃ _ : Proof(∃ₗ! P) ⦄ → Domain
        [∃!]-witness{P} ⦃ proof ⦄ = [∃]-witness{P} ⦃ [∧].elimₗ proof ⦄

        [∃!]-proof : ∀{P : Domain → Formula} → ⦃ p : Proof(∃ₗ! P) ⦄ → Proof(P([∃!]-witness{P} ⦃ p ⦄))
        [∃!]-proof{P} ⦃ proof ⦄ = [∃]-proof{P} ⦃ [∧].elimₗ proof ⦄

        [∃!]-unique : ∀{P : Domain → Formula} → ⦃ p : Proof(∃ₗ! P) ⦄ → Proof(∀ₗ(x ↦ P(x) ⟶ (x ≡ [∃!]-witness{P} ⦃ p ⦄)))
        [∃!]-unique{P} ⦃ proof ⦄ =
          ([∀].intro(\{x} →
            ([→].intro(px ↦
              ([→].elim
                ([∀].elim([∀].elim([∧].elimᵣ proof) {x}) {[∃!]-witness{P} ⦃ proof ⦄})
                ([∧].intro
                  (px)
                  ([∃!]-proof{P} ⦃ proof ⦄)
                )
              )
            ))
          ))

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

    field
      instance ⦃ propositionalSignature ⦄ : Propositional.Signature
      instance ⦃ predicateSignature ⦄     : Predicate.Signature
      instance ⦃ equalitySignature ⦄      : Equality.Signature
    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

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

    field
      instance ⦃ constructiveLogicSignature ⦄ : ConstructiveLogicSignature
    open ConstructiveLogicSignature public

    field
      instance ⦃ propositionalTheory ⦄ : Propositional.Theory
      instance ⦃ predicateTheory ⦄     : Predicate.Theory
      instance ⦃ equalityTheory ⦄      : Equality.Theory
    open Propositional.Theory(propositionalTheory) public
    open Predicate.Theory(predicateTheory) public
    open Equality.Theory(equalityTheory) public

module MultiSorted {ℓₒ} {Sorts : Type{ℓₒ}} (Domain : Sorts → Type{ℓₒ}) where
  module Predicate where
    record UniversalQuantification(∀ₗ : ∀{Sort} → (Domain(Sort) → Formula) → Formula) : Type{ℓₘₗ Lvl.⊔ (ℓₗ Lvl.⊔ ℓₒ)} where
      field
        intro : ∀{Sort}{P : Domain(Sort) → Formula} → (∀{x : Domain(Sort)} → Proof(P(x))) → Proof(∀ₗ P)
        elim  : ∀{Sort}{P : Domain(Sort) → Formula} → Proof(∀ₗ P) → (∀{x : Domain(Sort)} → Proof(P(x)))

    record ExistentialQuantification(∃ₗ : ∀{Sort} → (Domain(Sort) → Formula) → Formula) : Type{ℓₘₗ Lvl.⊔ (ℓₗ Lvl.⊔ ℓₒ)} where
      field
        intro : ∀{Sort}{P : Domain(Sort) → Formula}{a} → Proof(P(a)) → Proof(∃ₗ P)
        elim  : ∀{Sort}{P : Domain(Sort) → Formula}{Z : Formula} → (∀{x : Domain(Sort)} → Proof(P(x)) → Proof(Z)) → Proof(∃ₗ P) → Proof(Z)

    record Signature : Type{ℓₗ Lvl.⊔ ℓₒ} where
      field
        ∀ₗ : ∀{Sort} → (Domain(Sort) → Formula) → Formula
        ∃ₗ : ∀{Sort} → (Domain(Sort) → Formula) → Formula

    -- A theory of constructive predicate/(first-order) multi-sorted logic expressed using natural deduction rules
    record Theory ⦃ sign : Signature ⦄ : Type{ℓₘₗ Lvl.⊔ (ℓₗ Lvl.⊔ ℓₒ)} where
      open Signature(sign)

      field
        instance ⦃ universalQuantification ⦄   : UniversalQuantification(∀ₗ)
        instance ⦃ existentialQuantification ⦄ : ExistentialQuantification(∃ₗ)

      module [∀] = UniversalQuantification   (universalQuantification)
      module [∃] = ExistentialQuantification (existentialQuantification)

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:
{-# OPTIONS --without-K --rewriting #-}

open import lib.Basics
open import lib.Equivalence2
open import lib.Function2
open import lib.NType2
open import lib.types.Coproduct
open import lib.types.Fin
open import lib.types.Group
open import lib.types.Int
open import lib.types.Nat
open import lib.types.Pi
open import lib.types.Subtype
open import lib.types.Truncation
open import lib.groups.SubgroupProp

module lib.groups.Homomorphism where

{-
Group homomorphisms.
-}

preserves-comp : ∀ {i j} {A : Type i} {B : Type j}
  (A-comp : A → A → A) (B-comp : B → B → B) (f : A → B)
  → Type (lmax i j)
preserves-comp Ac Bc f = ∀ a₁ a₂ → f (Ac a₁ a₂) == Bc (f a₁) (f a₂)

preserves-comp-prop : ∀ {i j} {A : Type i} {B : Type j}
  {{_ : is-set B}} (A-comp : A → A → A) (B-comp : B → B → B)
  → SubtypeProp (A → B) (lmax i j)
preserves-comp-prop Ac Bc =
  preserves-comp Ac Bc , ⟨⟩

abstract
  ∼-preserves-preserves-comp : ∀ {i j} {A : Type i} {B : Type j}
    (A-comp : A → A → A) (B-comp : B → B → B) {f₀ f₁ : A → B} → f₀ ∼ f₁
    → preserves-comp A-comp B-comp f₀
    → preserves-comp A-comp B-comp f₁
  ∼-preserves-preserves-comp Ac Bc {f₀ = f₀} {f₁} f₀∼f₁ f₀-pc a₁ a₂ =
    ! (f₀∼f₁ (Ac a₁ a₂)) ∙ f₀-pc a₁ a₂ ∙ ap2 Bc (f₀∼f₁ a₁) (f₀∼f₁ a₂)

record GroupStructureHom {i j} {GEl : Type i} {HEl : Type j}
  (GS : GroupStructure GEl) (HS : GroupStructure HEl) : Type (lmax i j) where
  constructor group-structure-hom
  private
    module G = GroupStructure GS
    module H = GroupStructure HS
  field
    f : GEl → HEl
    pres-comp : preserves-comp G.comp H.comp f

  abstract
    pres-ident : f G.ident == H.ident
    pres-ident = H.cancel-l (f G.ident) $
      H.comp (f G.ident) (f G.ident)
        =⟨ ! (pres-comp G.ident G.ident) ⟩
      f (G.comp G.ident G.ident)
        =⟨ ap f (G.unit-l G.ident) ⟩
      f G.ident
        =⟨ ! (H.unit-r (f G.ident)) ⟩
      H.comp (f G.ident) H.ident =∎

    pres-inv : ∀ g → f (G.inv g) == H.inv (f g)
    pres-inv g = ! $ H.inv-unique-l _ _ $
      H.comp (f (G.inv g)) (f g)
        =⟨ ! (pres-comp (G.inv g) g) ⟩
      f (G.comp (G.inv g) g)
        =⟨ ap f (G.inv-l g) ⟩
      f G.ident
        =⟨ pres-ident ⟩
      H.ident
        =∎

    pres-exp : ∀ g i → f (G.exp g i) == H.exp (f g) i
    pres-exp g (pos O) = pres-ident
    pres-exp g (pos (S O)) = idp
    pres-exp g (pos (S (S n))) = pres-comp g (G.exp g (pos (S n))) ∙ ap (H.comp (f g)) (pres-exp g (pos (S n)))
    pres-exp g (negsucc O) = pres-inv g
    pres-exp g (negsucc (S n)) = pres-comp (G.inv g) (G.exp g (negsucc n)) ∙ ap2 H.comp (pres-inv g) (pres-exp g (negsucc n))

    pres-conj : ∀ g h → f (G.conj g h) == H.conj (f g) (f h)
    pres-conj g h = pres-comp (G.comp g h) (G.inv g) ∙ ap2 H.comp (pres-comp g h) (pres-inv g)

    pres-diff : ∀ g h → f (G.diff g h) == H.diff (f g) (f h)
    pres-diff g h = pres-comp g (G.inv h) ∙ ap (H.comp (f g)) (pres-inv h)

    pres-sum : ∀ {I : ℕ} (g : Fin I → GEl) → f (G.sum g) == H.sum (f ∘ g)
    pres-sum {I = O} _ = pres-ident
    pres-sum {I = S I} g = pres-comp (G.sum (g ∘ Fin-S)) (g (_ , ltS))
      ∙ ap (λ h → H.comp h (f (g (_ , ltS)))) (pres-sum (g ∘ Fin-S))

    pres-subsum-r : ∀ {k l} {I : ℕ} {A : Type k} {B : Type l}
      → (p : Fin I → Coprod A B) (g : B → GEl)
      → f (G.subsum-r p g) == H.subsum-r p (f ∘ g)
    pres-subsum-r p g = pres-sum (Coprod-rec (λ _ → G.ident) g ∘ p)
      ∙ ap H.sum (λ= λ x →
            Coprod-rec-post∘ f (λ _ → G.ident) g (p x)
          ∙ ap (λ h → Coprod-rec h (f ∘ g) (p x)) (λ= λ _ → pres-ident))

  ⊙f : ⊙[ GEl , G.ident ] ⊙→ ⊙[ HEl , H.ident ]
  ⊙f = f , pres-ident

infix 0 _→ᴳˢ_ -- [ˢ] for structures
_→ᴳˢ_ = GroupStructureHom

record GroupHom {i j} (G : Group i) (H : Group j) : Type (lmax i j) where
  constructor group-hom
  private
    module G = Group G
    module H = Group H
  field
    f : G.El → H.El
    pres-comp : ∀ g₁ g₂ → f (G.comp g₁ g₂) == H.comp (f g₁) (f g₂)
  open GroupStructureHom {GS = G.group-struct} {HS = H.group-struct}
    record {f = f ; pres-comp = pres-comp} hiding (f ; pres-comp) public

infix 0 _→ᴳ_
_→ᴳ_ = GroupHom

→ᴳˢ-to-→ᴳ : ∀ {i j} {G : Group i} {H : Group j}
  → (Group.group-struct G →ᴳˢ Group.group-struct H) → (G →ᴳ H)
→ᴳˢ-to-→ᴳ (group-structure-hom f pres-comp) = group-hom f pres-comp

idhom : ∀ {i} (G : Group i) → (G →ᴳ G)
idhom G = group-hom (idf _) (λ _ _ → idp)

idshom : ∀ {i} {GEl : Type i} (GS : GroupStructure GEl) → (GS →ᴳˢ GS)
idshom GS = group-structure-hom (idf _) (λ _ _ → idp)

{- constant (zero) homomorphism -}
module _ where
  cst-hom : ∀ {i j} {G : Group i} {H : Group j} → (G →ᴳ H)
  cst-hom {H = H} = group-hom (cst (Group.ident H)) (λ _ _ → ! (Group.unit-l H _))

{- negation is a homomorphism in an abelian gruop -}
inv-hom : ∀ {i} (G : AbGroup i) → GroupHom (AbGroup.grp G) (AbGroup.grp G)
inv-hom G = group-hom G.inv inv-pres-comp where
  module G = AbGroup G
  abstract
    inv-pres-comp : (g₁ g₂ : G.El) → G.inv (G.comp g₁ g₂) == G.comp (G.inv g₁) (G.inv g₂)
    inv-pres-comp g₁ g₂ = G.inv-comp g₁ g₂ ∙ G.comm (G.inv g₂) (G.inv g₁)

{- equality of homomorphisms -}
abstract
  group-hom= : ∀ {i j} {G : Group i} {H : Group j} {φ ψ : G →ᴳ H}
    → GroupHom.f φ == GroupHom.f ψ → φ == ψ
  group-hom= {G = G} {H = H} p = ap (uncurry group-hom) $
    Subtype=-out (preserves-comp-prop (Group.comp G) (Group.comp H)) p

  group-hom=-↓ : ∀ {i j k} {A : Type i} {G : A → Group j} {H : A → Group k} {x y : A}
    {p : x == y} {φ : G x →ᴳ H x} {ψ : G y →ᴳ H y}
    → GroupHom.f φ == GroupHom.f ψ
      [ (λ a → Group.El (G a) → Group.El (H a)) ↓ p ]
    → φ == ψ [ (λ a → G a →ᴳ H a) ↓ p ]
  group-hom=-↓ {p = idp} = group-hom=

abstract
  instance
    GroupHom-level : ∀ {i j} {G : Group i} {H : Group j} → is-set (G →ᴳ H)
    GroupHom-level {G = G} {H = H} = equiv-preserves-level
      (equiv (uncurry group-hom) (λ x → GroupHom.f x , GroupHom.pres-comp x)
             (λ _ → idp) (λ _ → idp))
      {{Subtype-level
        (preserves-comp-prop (Group.comp G) (Group.comp H))}}

infixr 80 _∘ᴳˢ_ _∘ᴳ_

abstract
  ∘ᴳˢ-pres-comp : ∀ {i j k} {GEl : Type i} {HEl : Type j} {KEl : Type k}
    {GS : GroupStructure GEl} {HS : GroupStructure HEl} {KS : GroupStructure KEl}
    (ψ : HS →ᴳˢ KS) (φ : GS →ᴳˢ HS)
    → preserves-comp (GroupStructure.comp GS) (GroupStructure.comp KS) (GroupStructureHom.f ψ ∘ GroupStructureHom.f φ)
  ∘ᴳˢ-pres-comp ψ φ g₁ g₂ = ap (GroupStructureHom.f ψ) (GroupStructureHom.pres-comp φ g₁ g₂)
    ∙ GroupStructureHom.pres-comp ψ (GroupStructureHom.f φ g₁) (GroupStructureHom.f φ g₂)

  ∘ᴳ-pres-comp : ∀ {i j k} {G : Group i} {H : Group j} {K : Group k} (ψ : H →ᴳ K) (φ : G →ᴳ H)
    → preserves-comp (Group.comp G) (Group.comp K) (GroupHom.f ψ ∘ GroupHom.f φ)
  ∘ᴳ-pres-comp ψ φ g₁ g₂ = ap (GroupHom.f ψ) (GroupHom.pres-comp φ g₁ g₂)
    ∙ GroupHom.pres-comp ψ (GroupHom.f φ g₁) (GroupHom.f φ g₂)

_∘ᴳˢ_ : ∀  {i j k} {GEl : Type i} {HEl : Type j} {KEl : Type k}
  {GS : GroupStructure GEl} {HS : GroupStructure HEl} {KS : GroupStructure KEl}
  → (HS →ᴳˢ KS) → (GS →ᴳˢ HS) → (GS →ᴳˢ KS)
ψ ∘ᴳˢ φ = group-structure-hom (GroupStructureHom.f ψ ∘ GroupStructureHom.f φ) (∘ᴳˢ-pres-comp ψ φ)

_∘ᴳ_ : ∀ {i j k} {G : Group i} {H : Group j} {K : Group k}
  → (H →ᴳ K) → (G →ᴳ H) → (G →ᴳ K)
ψ ∘ᴳ φ = group-hom (GroupHom.f ψ ∘ GroupHom.f φ) (∘ᴳ-pres-comp ψ φ)

{- algebraic properties -}

∘ᴳ-unit-r : ∀ {i j} {G : Group i} {H : Group j} (φ : G →ᴳ H)
  → φ ∘ᴳ idhom G == φ
∘ᴳ-unit-r φ = group-hom= idp

∘ᴳ-unit-l : ∀ {i j} {G : Group i} {H : Group j} (φ : G →ᴳ H)
  → idhom H ∘ᴳ φ == φ
∘ᴳ-unit-l φ = group-hom= idp

∘ᴳ-assoc : ∀ {i j k l} {G : Group i} {H : Group j} {K : Group k} {L : Group l}
  (χ : K →ᴳ L) (ψ : H →ᴳ K) (φ : G →ᴳ H)
  → (χ ∘ᴳ ψ) ∘ᴳ φ == χ ∘ᴳ ψ ∘ᴳ φ
∘ᴳ-assoc χ ψ φ = group-hom= idp

is-injᴳ : ∀ {i j} {G : Group i} {H : Group j}
  → (G →ᴳ H) → Type (lmax i j)
is-injᴳ hom = is-inj (GroupHom.f hom)

is-surjᴳ : ∀ {i j} {G : Group i} {H : Group j}
  → (G →ᴳ H) → Type (lmax i j)
is-surjᴳ hom = is-surj (GroupHom.f hom)

{- subgroups -}

infix 80 _∘subᴳ_
_∘subᴳ_ : ∀ {i j k} {G : Group i} {H : Group j}
  → SubgroupProp H k → (G →ᴳ H) → SubgroupProp G k
_∘subᴳ_ {k = k} {G = G} P φ = record {M} where
  module G = Group G
  module P = SubgroupProp P
  module φ = GroupHom φ
  module M where
    prop : G.El → Type k
    prop = P.prop ∘ φ.f

    abstract
      ident : prop G.ident
      ident = transport! P.prop φ.pres-ident P.ident

      diff : {g₁ g₂ : G.El} → prop g₁ → prop g₂ → prop (G.diff g₁ g₂)
      diff {g₁} {g₂} pφg₁ pφg₂ = transport! P.prop
        (φ.pres-diff g₁ g₂)
        (P.diff pφg₁ pφg₂)

infix 80 _∘nsubᴳ_
_∘nsubᴳ_ : ∀ {i j k} {G : Group i} {H : Group j}
  → NormalSubgroupProp H k → (G →ᴳ H) → NormalSubgroupProp G k
_∘nsubᴳ_ {G = G} {H} P φ = P.propᴳ ∘subᴳ φ , P-φ-is-normal
  where module P = NormalSubgroupProp P
        module φ = GroupHom φ
        abstract
          P-φ-is-normal : is-normal (P.propᴳ ∘subᴳ φ)
          P-φ-is-normal g₁ {g₂} pφg₂ = transport! P.prop
            (φ.pres-conj g₁ g₂)
            (P.conj (φ.f g₁) pφg₂)

{- kernels and images -}

module _ {i j} {G : Group i} {H : Group j} (φ : G →ᴳ H) where
  private
    module G = Group G
    module H = Group H
    module φ = GroupHom φ

  ker-propᴳ : SubgroupProp G j
  ker-propᴳ = record {M} where
    module M where
      prop : G.El → Type j
      prop g = φ.f g == H.ident
      abstract
        ident : prop G.ident
        ident = φ.pres-ident

        diff : {g₁ g₂ : G.El} → prop g₁ → prop g₂ → prop (G.diff g₁ g₂)
        diff {g₁} {g₂} p₁ p₂ = φ.pres-diff g₁ g₂ ∙ ap2 H.diff p₁ p₂ ∙ H.inv-r H.ident

  -- 'n' for 'normal'
  ker-npropᴳ : NormalSubgroupProp G j
  ker-npropᴳ = ker-propᴳ , ker-is-normal where
    abstract
      ker-is-normal : is-normal ker-propᴳ
      ker-is-normal g₁ {g₂} pg₂ =
          φ.pres-conj g₁ g₂
        ∙ ap (H.conj (φ.f g₁)) pg₂
        ∙ H.conj-ident-r (φ.f g₁)

  im-propᴳ : SubgroupProp H (lmax i j)
  im-propᴳ = record {M} where
    module M where
      prop : H.El → Type (lmax i j)
      prop h = Trunc -1 (hfiber φ.f h)

      level : (h : H.El) → is-prop (prop h)
      level h = Trunc-level

      abstract
        ident : prop H.ident
        ident = [ G.ident , φ.pres-ident ]

        diff : {h₁ h₂ : H.El} → prop h₁ → prop h₂ → prop (H.diff h₁ h₂)
        diff = Trunc-fmap2 λ {(g₁ , p₁) (g₂ , p₂)
          → G.diff g₁ g₂ , φ.pres-diff g₁ g₂ ∙ ap2 H.diff p₁ p₂}

  im-npropᴳ : is-abelian H → NormalSubgroupProp H (lmax i j)
  im-npropᴳ H-is-abelian = sub-abelian-normal H-is-abelian im-propᴳ

  has-trivial-kerᴳ : Type (lmax i j)
  has-trivial-kerᴳ = is-trivial-propᴳ ker-propᴳ

  abstract
    -- any homomorphism with trivial kernel is injective
    has-trivial-ker-is-injᴳ : has-trivial-kerᴳ → is-injᴳ φ
    has-trivial-ker-is-injᴳ tk g₁ g₂ p =
      G.zero-diff-same g₁ g₂ $ tk (G.diff g₁ g₂) $
        φ.pres-diff g₁ g₂ ∙ ap (λ h → H.diff h (φ.f g₂)) p ∙ H.inv-r (φ.f g₂)

ker-cst-hom-is-full : ∀ {i j} (G : Group i) (H : Group j)
  → is-fullᴳ (ker-propᴳ (cst-hom {G = G} {H}))
ker-cst-hom-is-full G H g = idp

{- exactness -}

module _ {i j k} {G : Group i} {H : Group j} {K : Group k}
  (φ : G →ᴳ H) (ψ : H →ᴳ K) where

  private
    module G = Group G
    module H = Group H
    module K = Group K
    module φ = GroupHom φ
    module ψ = GroupHom ψ

  record is-exact : Type (lmax k (lmax j i)) where
    field
      im-sub-ker : im-propᴳ φ ⊆ᴳ ker-propᴳ ψ
      ker-sub-im : ker-propᴳ ψ ⊆ᴳ  im-propᴳ φ

  open is-exact public

  abstract
    {- an equivalent version of is-exact-ktoi  -}
    im-sub-ker-in : is-fullᴳ (ker-propᴳ (ψ ∘ᴳ φ)) → im-propᴳ φ ⊆ᴳ ker-propᴳ ψ
    im-sub-ker-in r h = Trunc-rec (λ {(g , p) → ap ψ.f (! p) ∙ r g})

    im-sub-ker-out : im-propᴳ φ ⊆ᴳ ker-propᴳ ψ → is-fullᴳ (ker-propᴳ (ψ ∘ᴳ φ))
    im-sub-ker-out s g = s (φ.f g) [ g , idp ]

{- homomorphisms into an abelian group can be composed with
 - the group operation and form a group -}
module _ {i j} (G : Group i) (H : AbGroup j)
  where

  private
    module G = Group G
    module H = AbGroup H

  hom-comp : (G →ᴳ H.grp) → (G →ᴳ H.grp) → (G →ᴳ H.grp)
  hom-comp φ ψ = group-hom (λ g → H.comp (φ.f g) (ψ.f g)) hom-comp-pres-comp where
    module φ = GroupHom φ
    module ψ = GroupHom ψ
    abstract
      hom-comp-pres-comp : ∀ g₁ g₂
        →  H.comp (φ.f (G.comp g₁ g₂)) (ψ.f (G.comp g₁ g₂))
        == H.comp (H.comp (φ.f g₁) (ψ.f g₁)) (H.comp (φ.f g₂) (ψ.f g₂))
      hom-comp-pres-comp g₁ g₂ =
        H.comp (φ.f (G.comp g₁ g₂)) (ψ.f (G.comp g₁ g₂))
          =⟨ ap2 H.comp (φ.pres-comp g₁ g₂) (ψ.pres-comp g₁ g₂) ⟩
        H.comp (H.comp (φ.f g₁) (φ.f g₂)) (H.comp (ψ.f g₁) (ψ.f g₂))
          =⟨ H.interchange (φ.f g₁) (φ.f g₂) (ψ.f g₁) (ψ.f g₂) ⟩
        H.comp (H.comp (φ.f g₁) (ψ.f g₁)) (H.comp (φ.f g₂) (ψ.f g₂)) =∎

  hom-group-structure : GroupStructure (G →ᴳ H.grp)
  hom-group-structure = record {M} where
    module M where
      ident : G →ᴳ H.grp
      ident = cst-hom

      comp : (G →ᴳ H.grp) → (G →ᴳ H.grp) → (G →ᴳ H.grp)
      comp = hom-comp

      inv : (G →ᴳ H.grp) → (G →ᴳ H.grp)
      inv φ = inv-hom H ∘ᴳ φ

      abstract
        unit-l : ∀ φ → comp ident φ == φ
        unit-l φ = group-hom= $ λ= λ _ → H.unit-l _

        assoc : ∀ φ ψ ξ → comp (comp φ ψ) ξ == comp φ (comp ψ ξ)
        assoc φ ψ ξ = group-hom= $ λ= λ _ → H.assoc _ _ _

        inv-l : ∀ φ → comp (inv φ) φ == ident
        inv-l φ = group-hom= $ λ= λ _ → H.inv-l _

  hom-group : Group (lmax i j)
  hom-group = group (G →ᴳ H.grp) hom-group-structure

  abstract
    hom-group-is-abelian : is-abelian hom-group
    hom-group-is-abelian φ ψ = group-hom= $ λ= λ g → H.comm _ _

  hom-abgroup : AbGroup (lmax i j)
  hom-abgroup = hom-group , hom-group-is-abelian

module _ {i j} {G : Group i} {H : AbGroup j} where
  app-hom : Group.El G → hom-group G H →ᴳ AbGroup.grp H
  app-hom g = group-hom (λ φ → GroupHom.f φ g) lemma
    where abstract lemma = λ φ ψ → idp

  appᴳ = app-hom

pre∘ᴳ-hom : ∀ {i j k} {G : Group i} {H : Group j} (K : AbGroup k)
  → (G →ᴳ H) → (hom-group H K →ᴳ hom-group G K)
pre∘ᴳ-hom K φ = record { f = _∘ᴳ φ ; pres-comp = lemma}
  where abstract lemma = λ _ _ → group-hom= idp

post∘ᴳ-hom : ∀ {i j k} (G : Group i) (H : AbGroup j) (K : AbGroup k)
  → (AbGroup.grp H →ᴳ AbGroup.grp K) → (hom-group G H →ᴳ hom-group G K)
post∘ᴳ-hom G H K φ = record { f = φ ∘ᴳ_ ; pres-comp = lemma}
  where abstract lemma = λ _ _ → group-hom= $ λ= λ _ → GroupHom.pres-comp φ _ _

ext: agda

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Formalization where

module Introduction where

open import Data.Product using (Σ; Σ-syntax; _×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

data Iso (A B : Set): Set where
  iso : (f : A → B) → (g : B → A) → (((x : A) → (g (f x)) ≡ x) × ((y : B) → (f (g y)) ≡ y))  → Iso A B

open import Function using (_∘_)

-- NB: This says every [total] relation can be refined to a function.
-- Kind of ew...
-- The Hott Book notes that though the system is strong enough to sufficiently
-- dilute the consequences of AC, the law of the excluded middle is inconsistent with Univalence
-- because it acts like a "Hilbertian Choice Operator" [p 9].
axiom-of-choice : {A : Set}
       → {B : A → Set}
       → {R : (a : A) → B a → Set}
       → (∀ (x : A) → Σ[ y ∈ B x ](R x y)) -- If for every x : A, ∃ a y : B x s.t. R x y
       → Σ[ f ∈ ((x : A) → B x) ](∀ (x : A) → (R x (f x))) -- then ∃ f : A → B s.t. ∀ x : A we have R (x, f(x))
axiom-of-choice g = proj₁ ∘ g , proj₂ ∘ g

module Chapter where

-- Simple Polymorphic Functions
-- ----------------------------

id : ∀{a}{A : Set a} → A → A
id x = x

swap : ∀{a b c}{A : Set a}{B : Set b}{C : Set c} → (A → B → C) → (B → A → C)
swap g = λ b a → g a b

-- Product Types
-- -------------

-- To specify a type (a la Martin Löf's TT) we need:
-- ∘ Formation Rules ("We can form f : A → B when A : Type and B : Type")
-- ∘ Introduction Rules (Constructors)
-- ∘ Elimination Rules (How to use the type's elements)
-- ∘ Computation Rules (How Elimination Rules act on constructors)
-- OPTIONAL
-- ∘ Uniqueness Principle (Every element of the type is {uniquely} determined by the result of applying Elimination Rules)

-- Formation and Introduction of Pairs is given in Data.Product, so here's an Eliminator

{- Need function extensionality here, but I'm too lazy to postulate it right now.
elimₓ-β : {A B C : Set} → (f : (A × B) → C) → (g : (A → B → C)) → (x : A)(y : B) → (f (x , y) ≡ g x y)
elimₓ-β = λ f g x y → refl
-}

-- The projection functons also count as eliminators, but are too specific on occaision
-- so we introduce the recursor for product types.

recₓ : ∀{a b c}{A : Set a}{B : Set b}{C : Set c} → (A → B → C) → (A × B) → C
recₓ g (a , b) = g a b

-- Then define the projection functions in terms of it.

pr₁ : ∀{a b}{A : Set a}{B : Set b} → (A × B) → A
pr₁ = recₓ λ a → λ b → a

pr₂ : ∀{a b}{A : Set a}{B : Set b} → (A × B) → B
pr₂ = recₓ λ a → λ b → b

-- The Unit Type also has a recursor:

open import Data.Unit

rec₁ : ∀{c}{C : Set c} → C → ⊤ → C
rec₁ c ⋆ = c

-- For dependent functions over the product type, we must first generalize the recursor

recₓ-general : ∀{a b c}{A : Set a}{B : Set b}{C : (A × B) → Set c} → (x : A × B) → (g : (a : A) → (b : B) → C (a , b)) → C x
recₓ-general = λ x g → g (pr₁ x) (pr₂ x)

-- Now we can prove the propositional uniqueness principle

uppt : ∀{a b}{A : Set a}{B : Set b} → (x : A × B) → ((pr₁ x) , (pr₂ x) ≡ x)
uppt x = refl

-- And compute the following equality:

reflₓ : ∀{a b}{A : Set a}{B : Set b}
      → (x : A)(y : B) -- ∀ x, y
      → ((pr₁ (x , y)) , (pr₂ (x , y)) ≡ (x , y)) -- Forming from forming then eliminating is the same as forming
reflₓ x y = refl

-- Now the induction function for product types;

indₓ :  ∀{a b c}{A : Set a}{B : Set b}{C : (A × B) → Set c}
     → ((x : A) → (y : B) -- ∀ x , y
     → C (x , y)) -- and a property that holds for the product (x , y)
     → (x : A × B) → C x -- ∀ products x, C holds
indₓ g (a , b) =  g a b

-- And for the unit type

ind₁ : {C : ⊤ → Set} → C tt → (x : ⊤) → C x
ind₁ c ⋆ = c

-- "Induction enables us to prove the propositional uniqueness principle for 1, which asserts that its
-- only inhabitant is ⋆. That is, we can construct"

upun : (x : ⊤) → x ≡ tt
upun x = refl

-- The uniqueness of unit can also be asserted by induction

upun-ind : (x : ⊤) → x ≡ tt
upun-ind x = ind₁ {C = λ x → x ≡ tt} refl x

-- Sigma (Dependent Pair) Types
-- ----------------------------

-- We'll use the Σ in the Agda Stdlib (because of the cool syntax).
--
-- For a constant type B rather than a B indexed by x : A, dependent pairs
-- and just cartesian products.  With that in mind, the recursor for dependent
-- pairs looks much the same as the one for the cartesian product

recₚ : ∀{a b c}{A : Set a}{B : A → Set b}{C : Set c}
     → ((x : A) → B x → C) -- It suffices to define the dependent function g such that
     → Σ[ x ∈ A ](B x) → C -- ∀ Σ(x : A)B x, C holds.
recₚ g (a , b) = g a b

-- Here's Induction

indₚ : ∀{a b c}{A : Set a}{B : A → Set b}{C : Σ[ x ∈ A ](B x) → Set c}
     → ((x : A)(y : B x) -- ∀ x , y
     → C (x , y)) -- and a property that holds for the pair (x , y)
     → (p : Σ[ x ∈ A ](B x)) → C p -- ∀ pairs x, C holds
indₚ g (a , b) = g a b

-- NB: Read Π as "forall" and Σ as "exists"

record Magma (A : Set) : Set where
  field
    mop : A → A → A
open Magma {{...}} public

record PointedMagma (A : Set) : Set where
  field
    mbasepoint : A
    pmop : (A → A → A)
  pointedMagmaIsMagma : Magma A
  pointedMagmaIsMagma = record { mop = pmop }
open PointedMagma {{...}} public

-- Coproducts

open import Data.Sum

rec₊ : ∀{a b c}{A : Set a}{B : Set b}{C : Set c} → (A → C) → (B → C) → A ⊎ B → C
rec₊ g₀ g₁ (inj₁ x) = g₀ x
rec₊ g₀ g₁ (inj₂ y) = g₁ y

-- Oh look, ⊥

open import Data.Empty

-- Any definition of the recursor would means proving 'ex falso quodlibet'.
-- Let's try not to do that...
rec₀ : ∀{c}{C : Set c} → ⊥ → C
rec₀ ()

ind₊ :  ∀{a b c}{A : Set a}{B : Set b}{C : (A ⊎ B) → Set c}
     → ((x : A) → C (inj₁ x))
     → ((y : B) → C (inj₂ y))
     → (x : A ⊎ B) → C x
ind₊ g₀ g₁ (inj₁ x) = g₀ x
ind₊ g₀ g₁ (inj₂ y) = g₁ y

ind₀ : ∀{c}{C : ⊥ → Set c} → (z : ⊥) → C z
ind₀ ()

-- The type of booleans

open import Data.Bool

rec₂ : ∀{c}{C : Set c} → C → C → Bool → C
rec₂ c₀ c₁ true = c₁
rec₂ c₀ c₁ false = c₀

ind₂ : ∀{c}{C : Bool → Set c} → C false → C true → (x : Bool) → C x
ind₂ c₀ c₁ true = c₁
ind₂ c₀ c₁ false = c₀

dec₂ : (x : Bool) → (x ≡ false) ⊎ (x ≡ true)
dec₂ x = ind₂ {C = λ x → (x ≡ false) ⊎ (x ≡ true)} (inj₁ refl) (inj₂ refl) x

-- The type of Natural Numbers

open import Data.Nat

double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))

add : ℕ → ℕ → ℕ
add zero n = n
add (suc m) n = suc (add m n)

recₙ : ∀{c}{C : Set c} → C → (ℕ → C → C) → ℕ → C
recₙ c₀ cₛ zero = c₀
recₙ c₀ cₛ (suc n) = cₛ n (recₙ c₀ cₛ n)

double-recₙ : ℕ → ℕ
double-recₙ = recₙ 0 (λ n y → suc (suc y))

add-recₙ : ℕ → ℕ → ℕ
add-recₙ = recₙ {C = ℕ → ℕ} (λ n → n) (λ n → λ g m → suc (g m))

indₙ : {C : ℕ → Set} → C 0 → ((n : ℕ) → C n → C (suc n)) → (n : ℕ) → C n
indₙ c₀ cₛ zero = c₀
indₙ c₀ cₛ (suc n) = cₛ n (indₙ c₀ cₛ n)

assoc : (i j k : ℕ) → i + (j + k) ≡ (i + j) + k
assoc = indₙ {C = λ i → (j k : ℕ) → i + (j + k) ≡ (i + j) + k} assoc₀ assocₛ
  where
    assoc₀ : (j k : ℕ) → 0 + (j + k) ≡ (0 + j) + k
    assoc₀ j k = refl

    assocₛ : (i : ℕ) → ((j k : ℕ) → i + (j + k) ≡ (i + j) + k) → (j k : ℕ) → (suc i) + (j + k) ≡ ((suc i) + j) + k
    assocₛ _ i j k = cong suc (i j k)

-- Propositions As Types

{-
¬_ : {A : Set} → A → ⊥
¬ x = ()
-}

-- Path Induction

open import Level

ind₌ : ∀ {i} {A : Set i} → (C : (x y : A) → (x ≡ y) → Set i) → ((x : A) → C x x refl) → {x y : A} → (p : x ≡ y) → C x y p
ind₌ C c {x}{y} p rewrite p = c y

based-ind₌ : ∀ {i} {A : Set i}{a : A} → (C : (x : A) → (a ≡ x) → Set i) → C a refl → {x : A} → (p : a ≡ x) → C x p
based-ind₌ C c p rewrite p = c

{-
ind₌-β : ∀ {i} {A : Set i}
  → (C : (x y : A) → (x ≡ y) → Set i)
  → (c : (x : A) → C x x refl)
  → (x : A)
  → (C' : (y : A) → (x ≡ y) → Set i)
  → (c' : C' x refl)
  → (y : A)
  → (p : x ≡ y)
  → ind₌ C c p <-> based-ind₌ C' c' p
ind₌-β {i} {A} C c x C' c' y p = ? where
    D : (x y : A) → (x ≡ y) → Set i
    D x y p = (C : (z : A) → (x ≡ z) → Set i) → C x refl → C y p

    d : (x : A) → D x x refl
    d = λ x₁ → λ C → (c : C x refl) → c
-}

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
------------------------------------------------------------------------
-- Properties of homogeneous binary relations
------------------------------------------------------------------------

-- This file contains some core definitions which are reexported by
-- Relation.Binary or Relation.Binary.PropositionalEquality.

module Relation.Binary.Core where

open import Data.Product
open import Data.Sum
open import Data.Function
open import Relation.Nullary.Core

------------------------------------------------------------------------
-- Homogeneous binary relations

Rel : Set → Set₁
Rel a = a → a → Set

------------------------------------------------------------------------
-- Simple properties of binary relations

infixr 4 _⇒_ _=[_]⇒_

-- Implication/containment. Could also be written ⊆.

_⇒_ : ∀ {a} → Rel a → Rel a → Set
P ⇒ Q = ∀ {i j} → P i j → Q i j

-- Generalised implication. If P ≡ Q it can be read as "f preserves
-- P".

_=[_]⇒_ : ∀ {a b} → Rel a → (a → b) → Rel b → Set
P =[ f ]⇒ Q = P ⇒ (Q on₁ f)

-- A synonym, along with a binary variant.

_Preserves_⟶_ : ∀ {a₁ a₂} → (a₁ → a₂) → Rel a₁ → Rel a₂ → Set
f Preserves P ⟶ Q = P =[ f ]⇒ Q

_Preserves₂_⟶_⟶_ : ∀ {a₁ a₂ a₃} →
                   (a₁ → a₂ → a₃) → Rel a₁ → Rel a₂ → Rel a₃ → Set
_+_ Preserves₂ P ⟶ Q ⟶ R =
  ∀ {x y u v} → P x y → Q u v → R (x + u) (y + v)

-- Reflexivity of _∼_ can be expressed as _≈_ ⇒ _∼_, for some
-- underlying equality _≈_. However, the following variant is often
-- easier to use.

Reflexive : {a : Set} → (_∼_ : Rel a) → Set
Reflexive _∼_ = ∀ {x} → x ∼ x

-- Irreflexivity is defined using an underlying equality.

Irreflexive : {a : Set} → (_≈_ _<_ : Rel a) → Set
Irreflexive _≈_ _<_ = ∀ {x y} → x ≈ y → ¬ (x < y)

-- Generalised symmetry.

Sym : ∀ {a} → Rel a → Rel a → Set
Sym P Q = P ⇒ flip₁ Q

Symmetric : {a : Set} → Rel a → Set
Symmetric _∼_ = Sym _∼_ _∼_

-- Generalised transitivity.

Trans : ∀ {a} → Rel a → Rel a → Rel a → Set
Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k

Transitive : {a : Set} → Rel a → Set
Transitive _∼_ = Trans _∼_ _∼_ _∼_

Antisymmetric : {a : Set} → (_≈_ _≤_ : Rel a) → Set
Antisymmetric _≈_ _≤_ = ∀ {x y} → x ≤ y → y ≤ x → x ≈ y

Asymmetric : {a : Set} → (_<_ : Rel a) → Set
Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)

_Respects_ : {a : Set} → (a → Set) → Rel a → Set
P Respects _∼_ = ∀ {x y} → x ∼ y → P x → P y

_Respects₂_ : {a : Set} → Rel a → Rel a → Set
P Respects₂ _∼_ =
  (∀ {x} → P x       Respects _∼_) ×
  (∀ {y} → flip₁ P y Respects _∼_)

Substitutive : {a : Set} → Rel a → Set₁
Substitutive _∼_ = ∀ P → P Respects _∼_

Congruential : ({a : Set} → Rel a) → Set₁
Congruential ∼ = ∀ {a b} → (f : a → b) → f Preserves ∼ ⟶ ∼

Congruential₂ : ({a : Set} → Rel a) → Set₁
Congruential₂ ∼ =
  ∀ {a b c} → (f : a → b → c) → f Preserves₂ ∼ ⟶ ∼ ⟶ ∼

Decidable : {a : Set} → Rel a → Set
Decidable _∼_ = ∀ x y → Dec (x ∼ y)

Total : {a : Set} → Rel a → Set
Total _∼_ = ∀ x y → (x ∼ y) ⊎ (y ∼ x)

data Tri (A B C : Set) : Set where
  tri< : ( a :   A) (¬b : ¬ B) (¬c : ¬ C) → Tri A B C
  tri≈ : (¬a : ¬ A) ( b :   B) (¬c : ¬ C) → Tri A B C
  tri> : (¬a : ¬ A) (¬b : ¬ B) ( c :   C) → Tri A B C

Trichotomous : {a : Set} → Rel a → Rel a → Set
Trichotomous _≈_ _<_ = ∀ x y → Tri (x < y) (x ≈ y) (x > y)
  where _>_ = flip₁ _<_

record NonEmpty {I : Set} (T : Rel I) : Set where
  field
    i     : I
    j     : I
    proof : T i j

nonEmpty : ∀ {I} {T : Rel I} {i j} → T i j → NonEmpty T
nonEmpty p = record { i = _; j = _; proof = p }

------------------------------------------------------------------------
-- Propositional equality

-- This dummy module is used to avoid shadowing of the field named
-- refl defined in IsEquivalence below. The module is opened publicly
-- at the end of this file.

private
 module Dummy where

  infix 4 _≡_ _≢_

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

  {-# BUILTIN EQUALITY _≡_ #-}
  {-# BUILTIN REFL refl #-}

  -- Nonequality.

  _≢_ : {a : Set} → a → a → Set
  x ≢ y = ¬ x ≡ y

------------------------------------------------------------------------
-- Equivalence relations

-- The preorders of this library are defined in terms of an underlying
-- equivalence relation, and hence equivalence relations are not
-- defined in terms of preorders.

record IsEquivalence {a : Set} (_≈_ : Rel a) : Set where
  field
    refl  : Reflexive _≈_
    sym   : Symmetric _≈_
    trans : Transitive _≈_

  reflexive : Dummy._≡_ ⇒ _≈_
  reflexive Dummy.refl = refl

open Dummy public

max_issues_repo_name: larrytheliquid/Lemmachine


text:
{-# OPTIONS --safe #-}
{-
  This is inspired by/copied from:
  https://github.com/agda/agda-stdlib/blob/master/src/Tactic/MonoidSolver.agda

  Boilerplate code for calling the ring solver is constructed automatically
  with agda's reflection features.
-}
module Cubical.Algebra.NatSolver.Reflection where

open import Cubical.Foundations.Prelude hiding (Type)
open import Cubical.Functions.Logic

open import Agda.Builtin.Reflection hiding (Type)
open import Agda.Builtin.String

open import Cubical.Reflection.Base

open import Cubical.Data.Maybe
open import Cubical.Data.Sigma
open import Cubical.Data.List
open import Cubical.Data.Nat.Literals
open import Cubical.Data.Nat
open import Cubical.Data.FinData using () renaming (zero to fzero; suc to fsuc)
open import Cubical.Data.Bool
open import Cubical.Data.Bool.SwitchStatement
open import Cubical.Data.Vec using (Vec) renaming ([] to emptyVec; _∷_ to _∷vec_) public

open import Cubical.Algebra.NatSolver.NatExpression
open import Cubical.Algebra.NatSolver.Solver

open EqualityToNormalform renaming (solve to natSolve)
private
  variable
    ℓ : Level

  _==_ = primQNameEquality
  {-# INLINE _==_ #-}

  record VarInfo : Type ℓ-zero where
    field
      varName : String
      varType : Arg Term
      index : ℕ

  {-
    `getLastTwoArgsOf` maps a term 'def n (z₁ ∷ … ∷ zₙ ∷ x ∷ y ∷ [])' to the pair '(x,y)'
    non-visible arguments are ignored.
  -}
  getLastTwoArgsOf : Name → Term → Maybe (Term × Term)
  getLastTwoArgsOf n' (def n xs) =
    if n == n'
    then go xs
    else nothing
      where
      go : List (Arg Term) → Maybe (Term × Term)
      go (varg x ∷ varg y ∷ []) = just (x , y)
      go (x ∷ xs)               = go xs
      go _                      = nothing
  getLastTwoArgsOf n' _ = nothing

  {-
    `getArgs` maps a term 'x ≡ y' to the pair '(x,y)'
  -}
  getArgs : Term → Maybe (Term × Term)
  getArgs = getLastTwoArgsOf (quote PathP)

  firstVisibleArg : List (Arg Term) → Maybe Term
  firstVisibleArg [] = nothing
  firstVisibleArg (varg x ∷ l) = just x
  firstVisibleArg (x ∷ l) = firstVisibleArg l

  {-
    If the solver needs to be applied during equational reasoning,
    the right hand side of the equation to solve cannot be given to
    the solver directly. The folllowing function extracts this term y
    from a more complex expression as in:
      x ≡⟨ solve ... ⟩ (y ≡⟨ ... ⟩ z ∎)
  -}
  getRhs : Term → Maybe Term
  getRhs reasoningToTheRight@(def n xs) =
    if n == (quote _∎)
    then firstVisibleArg xs
    else (if n == (quote _≡⟨_⟩_)
         then firstVisibleArg xs
         else nothing)
  getRhs _ = nothing

  private
    solverCallAsTerm : Arg Term → Term → Term → Term
    solverCallAsTerm varList lhs rhs =
      def
         (quote natSolve)
         (varg lhs ∷ varg rhs
           ∷ varList
           ∷ varg (def (quote refl) []) ∷ [])

  solverCallWithLambdas : ℕ → List VarInfo → Term → Term → Term
  solverCallWithLambdas n varInfos lhs rhs =
    encloseWithIteratedLambda
      (map VarInfo.varName varInfos)
      (solverCallAsTerm (variableList (rev varInfos)) lhs rhs)
    where
      encloseWithIteratedLambda : List String → Term → Term
      encloseWithIteratedLambda (varName ∷ xs) t = lam visible (abs varName (encloseWithIteratedLambda xs t))
      encloseWithIteratedLambda [] t = t

      variableList : List VarInfo → Arg Term
      variableList [] = varg (con (quote emptyVec) [])
      variableList (varInfo ∷ varInfos)
        = varg (con (quote _∷vec_) (varg (var (VarInfo.index varInfo) []) ∷ (variableList varInfos) ∷ []))

  solverCallByVarIndices : ℕ → List ℕ → Term → Term → Term → Term
  solverCallByVarIndices n varIndices R lhs rhs =
      solverCallAsTerm (variableList (rev varIndices)) lhs rhs
      where
        variableList : List ℕ → Arg Term
        variableList [] = varg (con (quote emptyVec) [])
        variableList (varIndex ∷ varIndices)
          = varg (con (quote _∷vec_) (varg (var (varIndex) []) ∷ (variableList varIndices) ∷ []))

module pr {n : ℕ} where
  0' : Expr n
  0' = K 0

  1' : Expr n
  1' = K 1

module _ where
  open pr

  `0` : List (Arg Term) → Term
  `0` [] = def (quote 0') []
  `0` (varg fstcring ∷ xs) = `0` xs
  `0` (harg _ ∷ xs) = `0` xs
  `0` _ = unknown

  `1` : List (Arg Term) → Term
  `1` [] = def (quote 1') []
  `1` (varg fstcring ∷ xs) = `1` xs
  `1` (harg _ ∷ xs) = `1` xs
  `1` _ = unknown

  mutual

    `_·_` : List (Arg Term) → Term
    `_·_` (harg _ ∷ xs) = `_·_` xs
    `_·_` (varg x ∷ varg y ∷ []) =
      con
        (quote _·'_) (varg (buildExpression x) ∷ varg (buildExpression y) ∷ [])
    `_·_` _ = unknown

    `_+_` : List (Arg Term) → Term
    `_+_` (harg _ ∷ xs) = `_+_` xs
    `_+_` (varg x ∷ varg y ∷ []) =
      con
        (quote _+'_) (varg (buildExpression x) ∷ varg (buildExpression y) ∷ [])
    `_+_` _ = unknown

    K' : List (Arg Term) → Term
    K' xs = con (quote K) xs

    finiteNumberAsTerm : ℕ → Term
    finiteNumberAsTerm ℕ.zero = con (quote fzero) []
    finiteNumberAsTerm (ℕ.suc n) = con (quote fsuc) (varg (finiteNumberAsTerm n) ∷ [])

    buildExpression : Term → Term
    buildExpression (var index _) = con (quote ∣) (varg (finiteNumberAsTerm index) ∷ [])
    buildExpression t@(lit n) = K' (varg t ∷ [])
    buildExpression t@(def n xs) =
      switch (n ==_) cases
        case (quote _·_) ⇒ `_·_` xs   break
        case (quote _+_) ⇒ `_+_` xs   break
        default⇒ (K' xs)
    buildExpression t@(con n xs) =
      switch (n ==_) cases
        case (quote _·_) ⇒ `_·_` xs   break
        case (quote _+_) ⇒ `_+_` xs   break
        default⇒ (K' xs)
    buildExpression t = unknown

  toAlgebraExpression : Maybe (Term × Term) → Maybe (Term × Term)
  toAlgebraExpression nothing = nothing
  toAlgebraExpression (just (lhs , rhs)) = just (buildExpression lhs , buildExpression rhs)

private
  adjustDeBruijnIndex : (n : ℕ) → Term → Term
  adjustDeBruijnIndex n (var k args) = var (k + n) args
  adjustDeBruijnIndex n _ = unknown

  extractVarIndices : Maybe (List Term) → Maybe (List ℕ)
  extractVarIndices (just ((var index _) ∷ l)) with extractVarIndices (just l)
  ... | just indices = just (index ∷ indices)
  ... | nothing = nothing
  extractVarIndices (just []) = just []
  extractVarIndices _ = nothing

  getVarsAndEquation : Term → Maybe (List VarInfo × Term)
  getVarsAndEquation t =
    let
      (rawVars , equationTerm) = extractVars t
      maybeVars = addIndices (length rawVars) rawVars
    in map-Maybe (_, equationTerm) maybeVars
    where
          extractVars : Term → List (String × Arg Term) × Term
          extractVars (pi argType (abs varName t)) with extractVars t
          ...                                         | xs , equation
                                                        = (varName , argType) ∷ xs , equation
          extractVars equation = [] , equation

          addIndices : ℕ → List (String × Arg Term) → Maybe (List VarInfo)
          addIndices ℕ.zero         []        = just []
          addIndices (ℕ.suc countVar) ((varName , argType) ∷ list) =
            map-Maybe (λ varList → record { varName = varName ; varType = argType ; index = countVar }
                                   ∷ varList)
                      (addIndices countVar list)
          addIndices _ _ = nothing

  toListOfTerms : Term → Maybe (List Term)
  toListOfTerms (con c []) = if (c == (quote [])) then just [] else nothing
  toListOfTerms (con c (varg t ∷ varg s ∷ args)) with toListOfTerms s
  ... | just terms = if (c == (quote _∷_)) then just (t ∷ terms) else nothing
  ... | nothing = nothing
  toListOfTerms (con c (harg t ∷ args)) = toListOfTerms (con c args)
  toListOfTerms _ = nothing

  solve-macro : Term → TC Unit
  solve-macro hole =
    do
      hole′ ← inferType hole >>= normalise
      just (varInfos , equation) ← returnTC (getVarsAndEquation hole′)
        where
          nothing
            → typeError (strErr "Something went wrong when getting the variable names in "
                           ∷ termErr hole′ ∷ [])
      just (lhs , rhs) ← returnTC (toAlgebraExpression (getArgs equation))
        where
          nothing
            → typeError(
                strErr "Error while trying to build ASTs for the equation " ∷
                termErr equation ∷ [])
      let solution = solverCallWithLambdas (length varInfos) varInfos lhs rhs
      unify hole solution

macro
  solve : Term → TC _
  solve = solve-macro

max_stars_repo_name: FernandoLarrain/cubical


text:
{-# OPTIONS --exact-split #-}
module Issue1383 where

data Bool : Set where
  true false : Bool

xor : Bool → Bool → Bool
xor = \ { true  true  -> false ;
          false false -> false ;
          {-# CATCHALL #-}
          _     _     -> true  }

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Function using (id) renaming (_∘′_ to _∘_)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Control.Monad

module Control.Monad.Error (E : Set) where

-- The Error monad.

data Error (A : Set) : Set where
  fail   : (e : E) → Error A
  return : (a : A) → Error A

-- The following are axiliary definitions for the constructor of errorIsMonad.

module Local where

  -- Bind.

  _>>=_ : ∀ {A B} (m : Error A) (k : A → Error B) → Error B
  fail   e >>= k = fail e
  return a >>= k = k a

  bind = _>>=_

  -- Laws of bind.

  beta : ∀ {A B} (k : A → Error B) (a : A) →
    return a >>= k  ≡  k a
  beta k a = refl

  eta :  ∀ {A} (m : Error A) →
    m >>= return  ≡  m
  eta (fail   e) = refl
  eta (return a) = refl

  assoc : ∀ {A B C} (m : Error A) {k : A → Error B} {l : B → Error C} →
    (m >>= k) >>= l  ≡  m >>= λ a → (k a >>= l)
  assoc (fail   e) = refl
  assoc (return a) = refl

open Local public

-- The monad instance of Error.

errorIsMonad : IsMonad Error
errorIsMonad = record
  { ops  = record
    { return = return
    ; _>>=_  = bind
    }
  ; laws = record
    { bind-β     = beta
    ; bind-η     = eta
    ; bind-assoc = assoc
    }
  }

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Ints.QuoInt.Properties where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws

open import Cubical.HITs.Ints.QuoInt.Base
  renaming (_+ℤ_ to _+_)
open import Cubical.Data.Nat
  hiding (+-comm; +-zero; _+_)

+-pos-0 : ∀ a → pos 0 + a ≡ a
+-pos-0 (pos zero) = refl
+-pos-0 (pos (suc n)) = cong sucℤ (+-pos-0 (pos n))
+-pos-0 (neg zero) = posneg
+-pos-0 (neg (suc n)) = cong predℤ (+-pos-0 (neg n))
+-pos-0 (posneg i) j = posneg (i ∧ j)

+-neg-0 : ∀ a → neg 0 + a ≡ a
+-neg-0 (neg zero) = refl
+-neg-0 (neg (suc n)) = cong predℤ (+-neg-0 (neg n))
+-neg-0 (pos zero) = sym posneg
+-neg-0 (pos (suc n)) = cong sucℤ (+-neg-0 (pos n))
+-neg-0 (posneg i) j = posneg (i ∨ ~ j)

+-pos-suc : ∀ a b → sucℤ (pos b + a) ≡ (pos (suc b) + a)
+-pos-suc (pos zero) b = refl
+-pos-suc (pos (suc n)) b = cong sucℤ (+-pos-suc (pos n) b)
+-pos-suc (neg zero) b = refl
+-pos-suc (posneg i) b = refl
+-pos-suc (neg (suc n)) b =
  sucPredℤ (pos b + neg n) ∙∙
  sym (predSucℤ (pos b + neg n)) ∙∙
  cong predℤ (+-pos-suc (neg n) b)
  -- the following hcomp does not termination-check:
  -- hcomp (λ j → λ
  --  { (i = i0) → sucPredℤ (pos b + neg n) (~ j)
  --  ; (i = i1) → {!predℤ ((+-pos-suc (neg n) b) j)!}
  --  }) (predSucℤ (pos b + neg n) (~ i))

+-neg-pred : ∀ a b → predℤ (neg b + a) ≡ (neg (suc b) + a)
+-neg-pred (pos zero) b = refl
+-neg-pred (neg zero) b = refl
+-neg-pred (neg (suc n)) b = cong predℤ (+-neg-pred (neg n) b)
+-neg-pred (posneg i) b = refl
+-neg-pred (pos (suc n)) b =
  predSucℤ (neg b + pos n) ∙∙
  sym (sucPredℤ (neg b + pos n)) ∙∙
  cong sucℤ (+-neg-pred (pos n) b)

+-comm : ∀ a b → a + b ≡ b + a
+-comm a (pos zero) = sym (+-pos-0 a)
+-comm a (neg zero) = sym (+-neg-0 a)
+-comm a (pos (suc b)) = cong sucℤ (+-comm a (pos b)) ∙ +-pos-suc a b
+-comm a (neg (suc b)) = cong predℤ (+-comm a (neg b)) ∙ +-neg-pred a b
+-comm a (posneg i) = lemma a i
  where
  -- get some help from:
  -- https://www.codewars.com/kata/reviews/5c878e3ef1abb10001e32eb1/groups/5cca3f9e840f4b0001d8ac98
  lemma : ∀ a → (λ i → (a + posneg i) ≡ (posneg i + a))
          [ sym (+-pos-0 a) ≡ sym (+-neg-0 a) ]
  lemma (pos zero) i j = posneg (i ∧ j)
  lemma (pos (suc n)) i = cong sucℤ (lemma (pos n) i)
  lemma (neg zero) i j = posneg (i ∨ ~ j)
  lemma (neg (suc n)) i = cong predℤ (lemma (neg n) i)
  lemma (posneg i) j k = posneg ((i ∧ ~ k) ∨ (i ∧ j) ∨ (j ∧ k))

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
------------------------------------------------------------------------------
-- Totality properties for Forest
------------------------------------------------------------------------------

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

module FOTC.Program.Mirror.Forest.TotalityATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.List
open import FOTC.Program.Mirror.Type

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

++-Forest : ∀ {xs ys} → Forest xs → Forest ys → Forest (xs ++ ys)
++-Forest {ys = ys} fnil Fys = prf
  where postulate prf : Forest ([] ++ ys)
        {-# ATP prove prf #-}
++-Forest {ys = ys} (fcons {x} {xs} Tx Fxs) Fys = prf (++-Forest Fxs Fys)
  where postulate prf : Forest (xs ++ ys) →
                        Forest ((x ∷ xs) ++ ys)
        {-# ATP prove prf #-}

-- We don't use a combined proof, because it is necessary to erase a
-- proof term which we don't know how to erase.
map-Forest : ∀ {xs} f → (∀ {x} → Tree x → Tree (f · x)) →
             Forest xs → Forest (map f xs)
map-Forest f fTree fnil = subst Forest (sym (map-[] f)) fnil
map-Forest f fTree (fcons {x} {xs} Tx Fxs) =
  subst Forest
        (sym (map-∷ f x xs))
        (fcons (fTree Tx) (map-Forest f fTree Fxs))

rev-Forest : ∀ {xs ys} → Forest xs → Forest ys → Forest (rev xs ys)
rev-Forest {ys = ys} fnil Fys = prf
  where postulate prf : Forest (rev [] ys)
        {-# ATP prove prf #-}
rev-Forest {ys = ys} (fcons {x} {xs} Tx Fxs) Fys =
  prf (rev-Forest Fxs (fcons Tx Fys))
  where postulate prf : Forest (rev xs (x ∷ ys)) →
                        Forest (rev (x ∷ xs) ys)
        {-# ATP prove prf #-}

postulate reverse-Forest : ∀ {xs} → Forest xs → Forest (reverse xs)
{-# ATP prove reverse-Forest rev-Forest #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --safe --no-qualified-instances #-}
module CF.Contexts.Lexical where

open import Level
open import Data.Unit
open import Data.Product
open import Data.String using (String)
open import Data.List
open import Data.List.Properties as LP
open import Data.List.Relation.Binary.Sublist.Propositional.Properties

open import Relation.Unary hiding (_⊢_; _⊆_; _∈_)
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Binary.Structures
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax

open import CF.Types

open import Data.List.Relation.Binary.Permutation.Propositional
open import Data.List.Relation.Binary.Sublist.Propositional

Ctx : Set
Ctx = List Ty

_⍮_ : Ctx → List Ty → Ctx
Γ ⍮ Δ = Γ ++ Δ

variable
  K K₁ K₂ K₃ K₄ : Ctx
  Δ Δ₁ Δ₂ : List Ty

module CoDeBruijn where

  open import Relation.Ternary.Construct.List.Overlapping Ty public

  instance list-empty : ∀ {a} {A : Set a} → Emptiness {A = List A} []
  list-empty = record {}

  Vars : Ctx → Pred Ctx 0ℓ
  Vars Γ = Own Γ

  Closed : ∀ {ℓ} → Pred Ctx ℓ → Set ℓ
  Closed P = P ε

  data _∼[_]_ : Ctx → Ctx → Ctx → Set where
    intros : ∀ {Γ Δ Δ′ Γ′} → Δ′ ⊆ Δ → Γ′ ≡ Γ ++ Δ′ → Γ ∼[ Δ ] Γ′

  open import Relation.Ternary.Monad.Possibly
  open Possibly _∼[_]_
    public
    using (possibly; ◇; module ◇-GradedMonad; module ◇-Zip; _∼_; pack)
    renaming
      ( ◇[_] to _⊢_)

  ∼-all : K ∼[ Δ ] (K ⍮ Δ)
  ∼-all = intros ⊆-refl refl

  ∼-none : K ∼[ Δ ] K
  ∼-none {Γ} {Δ} =
    intros (minimum Δ) (sym (++-identityʳ Γ))

  ∼-refl : K ∼[ ε ] K
  ∼-refl = ∼-none

  ∼-trans : K₁ ∼ K₂ → K₂ ∼ K₃ → K₁ ∼ K₃
  ∼-trans {K₁} (Δ₁ , intros {Δ′ = Δ₁′} p refl) (Δ₂ , intros {Δ′ = Δ₂′} q refl) =
    -, intros ⊆-refl (LP.++-assoc _ Δ₁′ Δ₂′)

  ∼-isPreorder : IsPreorder _≡_ _∼_
  IsPreorder.isEquivalence ∼-isPreorder = isEquivalence
  IsPreorder.reflexive ∼-isPreorder refl = -, ∼-refl
  IsPreorder.trans ∼-isPreorder = ∼-trans

  -- frame preserving
  ∼-fp : K₁ ∼ K₂ → (di₁ : K₃ ◆ K₁) → ∃ λ (di₂ : K₃ ◆ K₂) → whole di₁ ∼ whole di₂
  ∼-fp (_ , intros ext refl) (_ , σ₁) = (-, ∙-disjointᵣᵣ σ₁) , _ , intros ⊆-refl refl

  open ◇-Monad _∼[_]_ ∼-isPreorder ∼-fp public

  -- specialized version of graded join because I'm lazy
  ∼-goin : ∀ {p} {P : Pred Ctx p} → ∀[ Δ₁ ⊢ (Δ₂ ⊢ P) ⇒ (Δ₁ ++ Δ₂) ⊢ P ]
  ∼-goin (Possibly.possibly
    (intros {Γ} {Δ′ = Δ₁} r₁ refl)
    (Possibly.possibly (intros r₂ refl) px)) =
      possibly (intros (++⁺ r₁ r₂) (++-assoc Γ Δ₁ _ )) px

  module _ where
    open import Relation.Ternary.Construct.List.Overlapping Ty as Ov
    abstract
      ∼-pull : Δ₁ Ov.⊗ Δ₂ ≣ Δ
             → K₁ ∙ K₃ ≣ K
             → K₁ ∼[ Δ₁ ] K₂
             → K₃ ∼[ Δ₂ ] K₄
             → ∃ λ K' → K₂ ∙ K₄ ≣ K' × K ∼[ Δ ] K'
      ∼-pull δ σ₁ (intros p refl) (intros q refl) with _ , δ′ , r ← Ov.⊆-⊗ p q δ =
        -, ∙-parallel σ₁ δ′ , intros r refl

  open ◇-Zip ∼-pull public renaming (◇-zip to ⊢-zip)

  binders : ∀ {Γ} → ε[ Γ ⊢ Vars Γ ]
  binders = Possibly.possibly ∼-all refl

  Var : Ty → Pred Ctx 0ℓ
  Var a = Vars [ a ]

  pattern vars = refl

module DeBruijn where
  open import Data.List.Membership.Propositional

  Var : Ty → Pred Ctx 0ℓ
  Var a Γ = a ∈ Γ

  _⊢_ : ∀ {ℓ} → List Ty → Pt Ctx ℓ
  Δ ⊢ P = λ Γ → P (Γ ⍮ Δ)

  -- ◇′ : Pt Ctx 0ℓ
  -- ◇′ P = ⋃[ as ∶ _ ] as ⊢ P

open CoDeBruijn public


text:
------------------------------------------------------------------------
-- The Maybe type
------------------------------------------------------------------------

-- The definitions in this file are reexported by Data.Maybe.

module Data.Maybe.Core where

data Maybe (A : Set) : Set where
  just    : (x : A) → Maybe A
  nothing : Maybe A
{-# COMPILED_DATA Maybe Maybe Just Nothing #-}


text:
module Structure.Categorical.Proofs where

open import Data
open import Functional
open import Logic.Propositional
import      Lvl
open import Structure.Setoid
open import Structure.Categorical.Properties
import      Structure.Relator.Names as Names
open import Structure.Relator.Properties
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓₘ ℓₑ : Lvl.Level
private variable Obj A B : Type{ℓ}
private variable _▫_ : Obj → Obj → Type{ℓ}
private variable f : A → B

empty-morphism : ∀{ℓₘ ℓ} → Empty{ℓ} → Empty{ℓ} → Type{ℓₘ}
empty-morphism{ℓₘ}{ℓ} = empty{T = Empty{ℓ} → Type{ℓₘ}}

empty-id : Names.Reflexivity(empty-morphism{ℓₘ}{ℓ})
empty-id {x = ()}

empty-comp : Names.SwappedTransitivity(empty-morphism{ℓₘ}{ℓ})
empty-comp {x = ()}

empty-inv : Names.Symmetry(empty-morphism{ℓₘ}{ℓ})
empty-inv {x = ()}

module _ ⦃ empty-equiv : ∀{x y} → Equiv{ℓₑ}(empty-morphism{ℓₘ}{ℓ} x y) ⦄ where
  instance
    empty-associativity : Morphism.Associativity{Morphism = empty-morphism} ⦃ empty-equiv ⦄ empty-comp
    empty-associativity = Morphism.intro \{}

  instance
    empty-identityₗ : Morphism.Identityₗ{Morphism = empty-morphism} ⦃ empty-equiv ⦄ empty-comp empty-id
    empty-identityₗ = Morphism.intro \{}

  instance
    empty-identityᵣ : Morphism.Identityᵣ{Morphism = empty-morphism} ⦃ empty-equiv ⦄ empty-comp empty-id
    empty-identityᵣ = Morphism.intro \{}

  empty-identity : Morphism.Identity empty-comp empty-id
  empty-identity = [∧]-intro empty-identityₗ empty-identityᵣ

  instance
    empty-inverterₗ : Polymorphism.Inverterₗ {Morphism = empty-morphism} ⦃ empty-equiv ⦄ empty-comp empty-id empty-inv
    empty-inverterₗ = Polymorphism.intro \{}

  instance
    empty-inverterᵣ : Polymorphism.Inverterᵣ {Morphism = empty-morphism} ⦃ empty-equiv ⦄ empty-comp empty-id empty-inv
    empty-inverterᵣ = Polymorphism.intro \{}

  empty-inverter : Polymorphism.Inverter empty-comp empty-id empty-inv
  empty-inverter = [∧]-intro empty-inverterₗ empty-inverterᵣ

single-morphism : ∀{ℓₘ ℓ} → Unit{ℓ} → Unit{ℓ} → Type{ℓₘ}
single-morphism <> <> = Unit

single-id : Names.Reflexivity(single-morphism{ℓₘ}{ℓ})
single-id = <>

single-comp : Names.SwappedTransitivity(single-morphism{ℓₘ}{ℓ})
single-comp <> <> = <>

single-inv : Names.Symmetry(single-morphism{ℓₘ}{ℓ})
single-inv <> = <>

module _ ⦃ single-equiv : ∀{x y} → Equiv{ℓₑ}(single-morphism{ℓₘ}{ℓ} x y) ⦄ where
  instance
    single-associativity : Morphism.Associativity{Morphism = single-morphism{ℓₘ}{ℓ₁}} ⦃ single-equiv ⦄ (single-comp{ℓ = ℓ₂})
    Morphism.Associativity.proof single-associativity {<>}{<>}{<>}{<>}{<>}{<>}{<>} = Reflexivity.proof(Equiv.reflexivity (single-equiv {<>}{<>}))

  instance
    single-identityₗ : Morphism.Identityₗ{Morphism = single-morphism{ℓₘ}{ℓ₁}} ⦃ single-equiv ⦄ (single-comp{ℓ = ℓ₂}) (single-id{ℓ = ℓ₃})
    Morphism.Identityₗ.proof single-identityₗ {<>}{<>}{<>} = Reflexivity.proof(Equiv.reflexivity (single-equiv {<>}{<>}))

  instance
    single-identityᵣ : Morphism.Identityᵣ{Morphism = single-morphism{ℓₘ}{ℓ₁}} ⦃ single-equiv ⦄ (single-comp{ℓ = ℓ₂}) (single-id{ℓ = ℓ₃})
    Morphism.Identityᵣ.proof single-identityᵣ {<>}{<>}{<>} = Reflexivity.proof(Equiv.reflexivity (single-equiv {<>}{<>}))

  single-identity : Morphism.Identity{Morphism = single-morphism{ℓₘ}{ℓ₁}} (single-comp{ℓ = ℓ₂}) (single-id{ℓ = ℓ₃})
  single-identity{ℓ₁}{ℓ₂}{ℓ₃} = [∧]-intro (single-identityₗ{ℓ₁}{ℓ₂}{ℓ₃}) (single-identityᵣ{ℓ₁}{ℓ₂}{ℓ₃})

  instance
    single-inverterₗ : Polymorphism.Inverterₗ {Morphism = single-morphism{ℓₘ}{ℓ₁}} ⦃ single-equiv ⦄ (single-comp{ℓ = ℓ₂}) (single-id{ℓ = ℓ₃}) (single-inv{ℓ = ℓ₄})
    Polymorphism.Inverterₗ.proof single-inverterₗ {<>}{<>}{<>} = Reflexivity.proof(Equiv.reflexivity (single-equiv {<>}{<>}))

  instance
    single-inverterᵣ : Polymorphism.Inverterᵣ {Morphism = single-morphism{ℓₘ}{ℓ₁}} ⦃ single-equiv ⦄ (single-comp{ℓ = ℓ₂}) (single-id{ℓ = ℓ₃}) (single-inv{ℓ = ℓ₄})
    Polymorphism.Inverterᵣ.proof single-inverterᵣ {<>}{<>}{<>} = Reflexivity.proof(Equiv.reflexivity (single-equiv {<>}{<>}))

  single-inverter : Polymorphism.Inverter {Morphism = single-morphism{ℓₘ}{ℓ₁}} ⦃ single-equiv ⦄ (single-comp{ℓ = ℓ₂}) (single-id{ℓ = ℓ₃}) (single-inv{ℓ = ℓ₄})
  single-inverter{ℓ₁}{ℓ₂}{ℓ₃}{ℓ₄} = [∧]-intro (single-inverterₗ{ℓ₁}{ℓ₂}{ℓ₃}{ℓ₄}) (single-inverterᵣ{ℓ₁}{ℓ₂}{ℓ₃}{ℓ₄})

module _ {Morphism : B → B → Type{ℓₘ}} ⦃ morphism-equiv : ∀{x y} → Equiv{ℓₑ}(Morphism x y) ⦄ (f : A → B) where
  module _ {comp : Names.SwappedTransitivity(Morphism)} where
    on₂-associativity : Morphism.Associativity{Morphism = Morphism} ⦃ morphism-equiv ⦄ comp → Morphism.Associativity{Morphism = Morphism on₂ f} comp
    Morphism.Associativity.proof (on₂-associativity p) = Morphism.Associativity.proof p

    module _ {id : Names.Reflexivity(Morphism)} where
      on₂-identityₗ : Morphism.Identityₗ{Morphism = Morphism} ⦃ morphism-equiv ⦄ comp id → Morphism.Identityₗ{Morphism = Morphism on₂ f} comp id
      Morphism.Identityₗ.proof (on₂-identityₗ p) = Morphism.Identityₗ.proof p

      on₂-identityᵣ : Morphism.Identityᵣ{Morphism = Morphism} ⦃ morphism-equiv ⦄ comp id → Morphism.Identityᵣ{Morphism = Morphism on₂ f} comp id
      Morphism.Identityᵣ.proof (on₂-identityᵣ p) = Morphism.Identityᵣ.proof p

      on₂-identity : Morphism.Identity{Morphism = Morphism} ⦃ morphism-equiv ⦄ comp id → Morphism.Identity{Morphism = Morphism on₂ f} comp id
      on₂-identity ([∧]-intro l r) = [∧]-intro (on₂-identityₗ l) (on₂-identityᵣ r)

      module _ {inv : Names.Symmetry(Morphism)} where
        on₂-inverterₗ : Polymorphism.Inverterₗ {Morphism = Morphism} ⦃ morphism-equiv ⦄ comp id inv → Polymorphism.Inverterₗ {Morphism = Morphism on₂ f} comp id inv
        Polymorphism.Inverterₗ.proof (on₂-inverterₗ p) = Polymorphism.Inverterₗ.proof p

        on₂-inverterᵣ : Polymorphism.Inverterᵣ {Morphism = Morphism} ⦃ morphism-equiv ⦄ comp id inv → Polymorphism.Inverterᵣ {Morphism = Morphism on₂ f} comp id inv
        Polymorphism.Inverterᵣ.proof (on₂-inverterᵣ p) = Polymorphism.Inverterᵣ.proof p

        on₂-inverter : Polymorphism.Inverter{Morphism = Morphism} ⦃ morphism-equiv ⦄ comp id inv → Polymorphism.Inverter{Morphism = Morphism on₂ f} comp id inv
        on₂-inverter ([∧]-intro l r) = [∧]-intro (on₂-inverterₗ l) (on₂-inverterᵣ r)


text:
module Lvl.Proofs where

open import Data.Tuple as Tuple using ()
open import Logic.Predicate
open import Lvl
open import Structure.Setoid
open import Structure.Function.Domain
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ : Lvl.Level
private variable T : Type{ℓ}

instance
  LvlUp-equiv : ⦃ equiv : Equiv{ℓₑ}(T) ⦄ → Equiv(Lvl.Up{ℓ}(T))
  Equiv._≡_ (LvlUp-equiv {ℓ = ℓ}) (up x) (up y) = Lvl.Up{ℓ}(x ≡ y)
  Up.obj (Reflexivity.proof (Equivalence.reflexivity (Equiv.equivalence LvlUp-equiv))) = reflexivity(_≡_)
  Up.obj (Symmetry.proof (Equivalence.symmetry (Equiv.equivalence LvlUp-equiv)) (up p)) = symmetry(_≡_) p
  Up.obj (Transitivity.proof (Equivalence.transitivity (Equiv.equivalence LvlUp-equiv)) (up p) (up q)) = transitivity(_≡_) p q

instance
  LvlUpObj-bijective : ⦃ equiv : Equiv{ℓₑ}(T) ⦄ → Bijective(Lvl.Up.obj{ℓ}{T = T})
  Up.obj (∃.witness (Tuple.left (Bijective.proof LvlUpObj-bijective {y}))) = y
  ∃.proof (Tuple.left (Bijective.proof LvlUpObj-bijective)) = reflexivity(_≡_)
  Up.obj (Tuple.right (Bijective.proof LvlUpObj-bijective) p q) = transitivity(_≡_) p (symmetry(_≡_) q)


text:
------------------------------------------------------------------------
-- Simple kinding of Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Kinding.Simple where

open import Data.Context.WellFormed
open import Data.Fin using (Fin; zero; suc)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Fin.Substitution.Typed
open import Data.List as List using ([]; _∷_; _∷ʳ_; map)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Product as Prod using (∃; _,_; _×_)
open import Data.Vec as Vec using ([]; _∷_)
import Data.Vec.Properties as VecProps
open import Function using (_∘_)
import Level
open import Relation.Binary.PropositionalEquality as PropEq using (refl; _≡_)
open import Relation.Nullary.Negation

open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.SingleVariableSubstitution
open import FOmegaInt.Syntax.HereditarySubstitution
open import FOmegaInt.Syntax.Normalization

------------------------------------------------------------------------
-- Simple kinding derivations.
--
-- TODO: explain the point of this and how "simple" kinding differs
-- from "canonical" kinding.

module Kinding where
  open SimpleCtx
  open Syntax

  infix 4 _⊢Var_∈_ _⊢_kds _⊢Nf_∈_ _⊢Ne_∈_ _⊢_∋∙_∈_ _⊢_wfs

  -- Simple kinding of variables.
  data _⊢Var_∈_ {n} (Γ : Ctx n) : Fin n → SKind → Set where
    ∈-var : ∀ {k} x → lookup Γ x ≡ kd k → Γ ⊢Var x ∈ k

  mutual

    -- Simplified well-formedness of kinds: a variant of
    -- well-formedness for η-long β-normal kinds based on simple
    -- kinding.
    data _⊢_kds {n} (Γ : Ctx n) : Kind Elim n → Set where
      kds-⋯ : ∀ {a b} → Γ ⊢Nf a ∈ ★ → Γ ⊢Nf b ∈ ★           → Γ ⊢ a ⋯ b kds
      kds-Π : ∀ {j k} → Γ ⊢ j kds   → kd ⌊ j ⌋ ∷ Γ ⊢ k kds  → Γ ⊢ Π j k kds

    -- Simple kinding of η-long β-normal types.
    data _⊢Nf_∈_ {n} (Γ : Ctx n) : Elim n → SKind → Set where
      ∈-⊥-f : Γ ⊢Nf ⊥∙ ∈ ★
      ∈-⊤-f : Γ ⊢Nf ⊤∙ ∈ ★
      ∈-∀-f : ∀ {k a} → Γ ⊢ k kds → kd ⌊ k ⌋ ∷ Γ ⊢Nf a ∈ ★ →
              Γ ⊢Nf ∀∙ k a ∈ ★
      ∈-→-f : ∀ {a b} → Γ ⊢Nf a ∈ ★ → Γ ⊢Nf b ∈ ★ → Γ ⊢Nf a ⇒∙ b ∈ ★
      ∈-Π-i : ∀ {j a k} → Γ ⊢ j kds → kd ⌊ j ⌋ ∷ Γ ⊢Nf a ∈ k →
              Γ ⊢Nf Λ∙ j a ∈ ⌊ j ⌋ ⇒ k
      ∈-ne  : ∀ {a} → Γ ⊢Ne a ∈ ★ → Γ ⊢Nf a ∈ ★

    -- Simple kinding of neutral types.
    data _⊢Ne_∈_ {n} (Γ : Ctx n) : Elim n → SKind → Set where
      ∈-∙ : ∀ {x j k} {as : Spine n} → Γ ⊢Var x ∈ j →
            Γ ⊢ j ∋∙ as ∈ k → Γ ⊢Ne var x ∙ as ∈ k

    -- Simple spine kinding.
    data _⊢_∋∙_∈_ {n} (Γ : Ctx n) : SKind → Spine n → SKind → Set where
      ∈-[] : ∀ {k} → Γ ⊢ k ∋∙ [] ∈ k
      ∈-∷  : ∀ {a as j k l} → Γ ⊢Nf a ∈ j → Γ ⊢ k ∋∙ as ∈ l →
             Γ ⊢ j ⇒ k ∋∙ a ∷ as ∈ l

  open ContextConversions using (⌊_⌋Ctx)

  -- Simple well-formedness of ascriptions
  data _⊢_wfs {n} (Γ : Ctx n) : ElimAsc n → Set where
    wfs-kd : ∀ {a} → Γ ⊢ a kds   → Γ ⊢ kd a wfs
    wfs-tp : ∀ {a} → Γ ⊢Nf a ∈ ★ → Γ ⊢ tp a wfs

  -- Simply well-formed contexts and context extensions.
  module SimplyWfCtx = ContextFormation (λ Γ a → ⌊ Γ ⌋Ctx ⊢ a wfs)
  open SimplyWfCtx public using () renaming (_wf to _ctxs; _⊢_wfExt to _⊢_exts)

open Syntax
open SimpleCtx
open Kinding
open PropEq

-- An admissible kinding rule for spine concatenation.
∈-++ : ∀ {n} {Γ : Ctx n} {as bs j k l} →
       Γ ⊢ j ∋∙ as ∈ k → Γ ⊢ k ∋∙ bs ∈ l →
       Γ ⊢ j ∋∙ as List.++ bs ∈ l
∈-++ ∈-[]               k∋as∈l = k∋as∈l
∈-++ (∈-∷ b∈j₁ j₂∋as∈k) k∋as∈l = ∈-∷ b∈j₁ (∈-++ j₂∋as∈k k∋as∈l)

-- An admissible kinding rule for appending a normal form to a spine.
∈-∷ʳ : ∀ {n} {Γ : Ctx n} {as a j k l} →
       Γ ⊢ j ∋∙ as ∈ k ⇒ l → Γ ⊢Nf a ∈ k →
       Γ ⊢ j ∋∙ as ∷ʳ a ∈ l
∈-∷ʳ j∋as∈k⇒k a∈k = ∈-++ j∋as∈k⇒k (∈-∷ a∈k ∈-[])

-- An admissible kinding rule for post-application to neutral types.
Ne∈-Π-e : ∀ {n} {Γ : Ctx n} {a b j k} →
          Γ ⊢Ne a ∈ j ⇒ k → Γ ⊢Nf b ∈ j → Γ ⊢Ne a ⌜·⌝ b ∈ k
Ne∈-Π-e (∈-∙ x∈j j∋as∈k) b∈k = ∈-∙ x∈j (∈-∷ʳ j∋as∈k b∈k)

-- An inversion lemma for _⊢_wf.
wfs-kd-inv : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ kd k wfs → Γ ⊢ k kds
wfs-kd-inv (wfs-kd k-kds) = k-kds

-- An inversion lemma for type operators.
Nf∈-⇒-inv : ∀ {n} {Γ : Ctx n} {a k₁ k₂} → Γ ⊢Nf a ∈ k₁ ⇒ k₂ →
            ∃ λ j → ∃ λ b →
              Γ ⊢ j kds × kd k₁ ∷ Γ ⊢Nf b ∈ k₂ × ⌊ j ⌋ ≡ k₁ × a ≡ Λ∙ j b
Nf∈-⇒-inv (∈-Π-i j-kds b∈k₂) = _ , _ , j-kds , b∈k₂ , refl , refl

----------------------------------------------------------------------
-- Well-kinded substitutions (i.e. substitution lemmas) in canonical
-- types

-- Well-kinded variable substitutions (renamings).
module KindedRenaming where

  open ⊤-WellFormed SimpleCtx.weakenOps

  typedVarSubst : TypedVarSubst SAsc Level.zero
  typedVarSubst = record
    { _⊢_wf              = _⊢_wf
    ; typeExtension      = SimpleCtx.weakenOps
    ; typeVarApplication = record { _/_ = λ k _ → k }
    ; /-wk               = refl
    ; id-vanishes        = λ _ → refl
    ; /-⊙                = λ _ → refl
    ; wf-wf            = λ _ → ctx-wf _
    }
  open TypedVarSubst typedVarSubst public
    hiding (∈-weaken)
    renaming (_⊢Var_∈_ to _⊢Var′_∈_; lookup to ∈-lookup)

  open Substitution hiding (subst; _/Var_) renaming (_Elim/Var_ to _/Var_)
  open RenamingCommutes using (Kind[∈⌊⌋]-/Var)
  open PropEq
  open ≡-Reasoning

  -- A helper.
  ∈-↑′ : ∀ {m n} {Δ : Ctx n} {Γ : Ctx m} {k ρ} →
         Δ ⊢/Var ρ ∈ Γ →
         kd ⌊ k Kind′/Var ρ ⌋ ∷ Δ ⊢/Var ρ VarSubst.↑ ∈ kd ⌊ k ⌋ ∷ Γ
  ∈-↑′ {Δ = Δ} {_} {k} ρ∈Γ =
    subst (λ j → kd j ∷ Δ ⊢/Var _ ∈ _) (sym (⌊⌋-Kind′/Var k)) (∈-↑ _ ρ∈Γ)

  -- Convert between well-kindedness judgments for variables.
  Var∈′-Var∈ : ∀ {n} {Γ : Ctx n} {x a k} → a ≡ kd k →
               Γ ⊢Var′ x ∈ a → Γ ⊢Var x ∈ k
  Var∈′-Var∈ Γ[x]≡kd-k (∈-var x Γ-ctx) = ∈-var x Γ[x]≡kd-k

  -- Renamings preserve synthesized kinds of variables.
  Var∈-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {x k ρ} →
              Γ ⊢Var x ∈ k → Δ ⊢/Var ρ ∈ Γ → Δ ⊢Var Vec.lookup ρ x ∈ k
  Var∈-/Var (∈-var x Γ[x]≡kd-k) ρ∈Γ = Var∈′-Var∈ Γ[x]≡kd-k (∈-lookup ρ∈Γ x)

  mutual

    -- Renamings preserve well-formedness of kinds.
    kds-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {k ρ} →
               Γ ⊢ k kds → Δ ⊢/Var ρ ∈ Γ → Δ ⊢ k Kind′/Var ρ kds
    kds-/Var (kds-⋯ a∈★ b∈★) ρ∈Γ = kds-⋯ (Nf∈-/Var a∈★ ρ∈Γ) (Nf∈-/Var b∈★ ρ∈Γ)
    kds-/Var (kds-Π j-kds  k-kds) ρ∈Γ =
      kds-Π (kds-/Var j-kds ρ∈Γ) (kds-/Var k-kds (∈-↑′ ρ∈Γ))

    -- Renamings preserve synthesized kinds of normal types.
    Nf∈-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a k ρ} →
               Γ ⊢Nf a ∈ k → Δ ⊢/Var ρ ∈ Γ → Δ ⊢Nf a /Var ρ ∈ k
    Nf∈-/Var ∈-⊥-f              ρ∈Γ = ∈-⊥-f
    Nf∈-/Var ∈-⊤-f              ρ∈Γ = ∈-⊤-f
    Nf∈-/Var (∈-∀-f k-kds a∈★)  ρ∈Γ =
      ∈-∀-f (kds-/Var k-kds ρ∈Γ) (Nf∈-/Var a∈★ (∈-↑′ ρ∈Γ))
    Nf∈-/Var (∈-→-f a∈★ b∈★)    ρ∈Γ =
      ∈-→-f (Nf∈-/Var a∈★ ρ∈Γ) (Nf∈-/Var b∈★ ρ∈Γ)
    Nf∈-/Var (∈-Π-i {j} {a} {k} j-kds a∈k) ρ∈Γ =
      subst (λ l → _ ⊢Nf Λ∙ j a /Var _ ∈ l ⇒ k) (⌊⌋-Kind′/Var j)
            (∈-Π-i (kds-/Var j-kds ρ∈Γ) (Nf∈-/Var a∈k (∈-↑′ ρ∈Γ)))
    Nf∈-/Var (∈-ne a∈★)         ρ∈Γ = ∈-ne (Ne∈-/Var a∈★ ρ∈Γ)

    -- Renamings preserve synthesized kinds of neutral types.
    Ne∈-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a k ρ} →
               Γ ⊢Ne a ∈ k → Δ ⊢/Var ρ ∈ Γ → Δ ⊢Ne a /Var ρ ∈ k
    Ne∈-/Var (∈-∙ x∈j k∈as∈l) ρ∈Γ =
      ∈-∙ (Var∈-/Var x∈j ρ∈Γ) (Sp∈-/Var k∈as∈l ρ∈Γ)

    Sp∈-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {as j k ρ} →
               Γ ⊢ j ∋∙ as ∈ k → Δ ⊢/Var ρ ∈ Γ → Δ ⊢ j ∋∙ as //Var ρ  ∈ k
    Sp∈-/Var ∈-[]                ρ∈Γ = ∈-[]
    Sp∈-/Var (∈-∷ a∈j k[a]∈as∈l) ρ∈Γ =
      ∈-∷ (Nf∈-/Var a∈j ρ∈Γ) (Sp∈-/Var k[a]∈as∈l ρ∈Γ)

  -- Renamings preserve well-formedness of ascriptions.
  wfs-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a ρ} →
             Γ ⊢ a wfs → Δ ⊢/Var ρ ∈ Γ → Δ ⊢ a ElimAsc/Var ρ wfs
  wfs-/Var (wfs-kd k-kds) ρ∈Γ = wfs-kd (kds-/Var k-kds ρ∈Γ)
  wfs-/Var (wfs-tp a∈★)   ρ∈Γ = wfs-tp (Nf∈-/Var a∈★ ρ∈Γ)

  -- Weakening preserves simple well-formedness of kinds.

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

  kds-weaken⋆ : ∀ {m n} (Δ : CtxExt m n) {Γ : Ctx m} {k} →
                Γ ⊢ k kds → Δ ++ Γ ⊢ weakenKind′⋆ n k kds
  kds-weaken⋆ []       k-kds = k-kds
  kds-weaken⋆ (_ ∷ Δ′) k-kds = kds-weaken (kds-weaken⋆ Δ′ k-kds)

  -- Weakening preserves kinding of normal forms.

  Nf∈-weaken : ∀ {n} {Γ : Ctx n} {a b k} →
               Γ ⊢Nf b ∈ k → (a ∷ Γ) ⊢Nf weakenElim b ∈ k
  Nf∈-weaken b∈k = Nf∈-/Var b∈k (∈-wk _)

  Nf∈-weaken⋆ : ∀ {m n} (Δ : CtxExt m n) {Γ : Ctx m} {a k} →
                Γ ⊢Nf a ∈ k → Δ ++ Γ ⊢Nf weakenElim⋆ n a ∈ k
  Nf∈-weaken⋆ []       a∈k = a∈k
  Nf∈-weaken⋆ (_ ∷ Δ′) a∈k = Nf∈-weaken (Nf∈-weaken⋆ Δ′ a∈k)

  -- Weakening preserves kinding of neutral forms.
  Ne∈-weaken : ∀ {n} {Γ : Ctx n} {a b k} →
               Γ ⊢Ne b ∈ k → (a ∷ Γ) ⊢Ne weakenElim b ∈ k
  Ne∈-weaken b∈k = Ne∈-/Var b∈k (∈-wk _)

  -- Weakening preserves spine kinding.
  Sp∈-weaken : ∀ {n} {Γ : Ctx n} {a bs j k} →
               Γ ⊢ j ∋∙ bs ∈ k → (a ∷ Γ) ⊢ j ∋∙ weakenSpine bs ∈ k
  Sp∈-weaken j∋bs∈k = Sp∈-/Var j∋bs∈k (∈-wk _)

  -- Weakening preserves simple well-formedness of ascriptions.
  wfs-weaken : ∀ {n} {Γ : Ctx n} {a b} →
               Γ ⊢ b wfs → a ∷ Γ ⊢ weakenElimAsc b wfs
  wfs-weaken b-wfs = wfs-/Var b-wfs (∈-wk _)

-- Operations on simply well-formed contexts that require weakening of
-- well-formedness judgments.
module WfsCtxOps where
  open SimplyWfCtx
  open ContextConversions using (⌊_⌋Ctx)
  open KindedRenaming using (wfs-weaken)

  wfsWeakenOps : WellFormedWeakenOps ElimCtx.weakenOps
  wfsWeakenOps = record { wf-weaken = λ _ → wfs-weaken }

  private module W = WellFormedWeakenOps wfsWeakenOps
  open W public hiding (wf-weaken)

  -- Lookup the kind of a type variable in a well-formed context.
  lookup-kd : ∀ {m} {Γ : ElimCtx.Ctx m} {a} x →
              Γ ctxs → ElimCtx.lookup Γ x ≡ kd a → ⌊ Γ ⌋Ctx ⊢ a kds
  lookup-kd x Γ-ctxs Γ[x]≡kd-a =
    wfs-kd-inv (subst (_ ⊢_wfs) Γ[x]≡kd-a (W.lookup Γ-ctxs x))

module KindedHereditarySubstitution where
  open Data.Fin         using (zero; raise; lift)
  open Substitution     hiding (subst; sub; _↑; _↑⋆_)
  open KindedRenaming   using (_⊢/Var_∈_; Nf∈-/Var; Nf∈-weaken⋆; ∈-wk)
  open RenamingCommutes using (wk-/⟨⟩-↑⋆; /Var-wk-↑⋆-hsub-vanishes)
  open PropEq
  open ≡-Reasoning
  private module V = VarSubst

  infix 4 _⊢/⟨_⟩_∈_ _⊢?⟨_⟩_∈_

  -- Simply well-kinded hereditary substitions and lookup results.

  data _⊢/⟨_⟩_∈_ : ∀ {m n} → Ctx n → SKind → SVSub m n → Ctx m → Set where
    ∈-hsub : ∀ {n} {Γ : Ctx n} {k a} →
             Γ ⊢Nf a ∈ k → Γ ⊢/⟨ k ⟩ sub a ∈ kd k ∷ Γ
    ∈-H↑   : ∀ {m n Δ k Γ} {σ : SVSub m n} {a} →
             Δ ⊢/⟨ k ⟩ σ ∈ Γ → a ∷ Δ ⊢/⟨ k ⟩ σ ↑ ∈ a ∷ Γ

  data _⊢?⟨_⟩_∈_ {n} (Γ : Ctx n) (k : SKind) : SVRes n → SAsc n → Set where
    ∈-hit  : ∀ {a}   → Γ ⊢Nf a ∈ k    → Γ ⊢?⟨ k ⟩ hit a ∈ kd k
    ∈-miss : ∀ y {a} → lookup Γ y ≡ a → Γ ⊢?⟨ k ⟩ miss y ∈ a

  -- A variant of `∈-H↑' that applies `σ' in the target context

  ∈-H↑′ : ∀ {m n Δ k Γ} {σ : SVSub m n} {j} →
          Δ ⊢/⟨ k ⟩ σ ∈ Γ →
          kd ⌊ j Kind/⟨ k ⟩ σ ⌋ ∷ Δ ⊢/⟨ k ⟩ σ ↑ ∈ kd ⌊ j ⌋ ∷ Γ
  ∈-H↑′ σ∈Γ =
    subst (λ k → kd k ∷ _ ⊢/⟨ _ ⟩ _ ↑ ∈ kd _ ∷ _)
          (sym (⌊⌋-Kind/⟨⟩ _)) (∈-H↑ σ∈Γ)

  -- Lift a kinded hereditary substitution over multiple additional
  -- variables.

  ∈-H↑⋆ : ∀ {m n i} (E : CtxExt m i) {Δ k Γ} {σ : SVSub m n} →
          Δ ⊢/⟨ k ⟩ σ ∈ Γ → re-idx E ++ Δ ⊢/⟨ k ⟩ σ ↑⋆ i ∈ E ++ Γ
  ∈-H↑⋆ []      σ∈Γ = σ∈Γ
  ∈-H↑⋆ (a ∷ E) σ∈Γ = ∈-H↑ (∈-H↑⋆ E σ∈Γ)

  -- Renamings preserve well-kinded SV results.

  ?∈-/Var : ∀ {m n Γ k Δ r a} {ρ : Sub Fin m n} →
            Γ ⊢?⟨ k ⟩ r ∈ a → Δ ⊢/Var ρ ∈ Γ → Δ ⊢?⟨ k ⟩ r ?/Var ρ ∈ a
  ?∈-/Var                 (∈-hit a∈k)     ρ∈Γ = ∈-hit (Nf∈-/Var a∈k ρ∈Γ)
  ?∈-/Var {Γ = Γ} {k} {Δ} (∈-miss y refl) ρ∈Γ = helper refl (TV.lookup ρ∈Γ y)
    where
      module TV = TypedVarSubst KindedRenaming.typedVarSubst

      helper : ∀ {x a} → a ≡ lookup Γ y → Δ TV.⊢Var x ∈ a →
               Δ ⊢?⟨ k ⟩ miss x ∈ lookup Γ y
      helper Δ[x]≡Γ[y] (TV.∈-var x _) = ∈-miss x Δ[x]≡Γ[y]

  ?∈-weaken : ∀ {n} {Γ : Ctx n} {k r a b} →
              Γ ⊢?⟨ k ⟩ r ∈ a → (b ∷ Γ) ⊢?⟨ k ⟩ weakenSVRes r ∈ a
  ?∈-weaken r∈a = ?∈-/Var r∈a (∈-wk _)

  -- Look up a variable in a well-kinded hereditary substitution.

  lookup-/⟨⟩∈ : ∀ {m n Δ k Γ} {σ : SVSub m n} →
                Δ ⊢/⟨ k ⟩ σ ∈ Γ → (x : Fin m) →
                Δ ⊢?⟨ k ⟩ lookupSV σ x ∈ lookup Γ x
  lookup-/⟨⟩∈                (∈-hsub a∈k) zero    = ∈-hit a∈k
  lookup-/⟨⟩∈ {Γ = kd k ∷ Γ} (∈-hsub a∈k) (suc x) =
    ∈-miss x (cong (λ Γ → Vec.lookup Γ x) (sym (VecProps.map-id (toVec Γ))))
  lookup-/⟨⟩∈ (∈-H↑                     σ∈Γ) zero    = ∈-miss zero refl
  lookup-/⟨⟩∈ (∈-H↑ {Δ = Δ} {_} {Γ} {σ} σ∈Γ) (suc x) =
    ?∈-weaken (subst (λ as → Δ ⊢?⟨ _ ⟩ lookupSV σ x ∈ Vec.lookup as x)
                     (sym (VecProps.map-id (toVec Γ))) (lookup-/⟨⟩∈ σ∈Γ x))

  -- Lookup a hit in a well-kinded hereditary substitution.
  --
  -- NOTE. Since `j ≡ k', we could have formulated this lemma
  -- differently.  In particular, given the premise `Γ ⊢Var x ∈ j', it
  -- would have been more intuitive for the kinding judgment in the
  -- conclusion to use the shape `j' rather than `k' (preserving the
  -- kind of the variable, as usual for substitution lemmas).
  -- However, it is important that the shape `k' of the normal type
  -- returned by this function is syntactically equal to the shape
  -- annotation of the hereditary substitution `Δ ⊢/⟨ k ⟩ σ ∈ Γ'
  -- because it serves as the termination measure for the (hereditary)
  -- substitution lemmas below.

  lookup-/⟨⟩∈-Hit : ∀ {m n Δ k} {σ : SVSub m n} {Γ x j a} →
                    Δ ⊢/⟨ k ⟩ σ ∈ Γ → Γ ⊢Var x ∈ j → Hit σ x a →
                    Δ ⊢Nf a ∈ k × j ≡ k
  lookup-/⟨⟩∈-Hit σ∈Γ (∈-var {j} x Γ[x]≡kd-j) hitP =
    let a∈k , Γ[x]≡kd-k = helper (lookup-Hit hitP) (lookup-/⟨⟩∈ σ∈Γ x)
    in  a∈k , kd-inj′ (trans (sym Γ[x]≡kd-j) Γ[x]≡kd-k)
    where
      helper : ∀ {n} {Δ : Ctx n} {r a b k} →
               r ≡ hit a → Δ ⊢?⟨ k ⟩ r ∈ b → Δ ⊢Nf a ∈ k × b ≡ kd k
      helper refl (∈-hit a∈k) = a∈k , refl

  lookup-/⟨⟩∈-Miss : ∀ {m n Δ k} {σ : SVSub m n} {Γ x y j} →
                     Δ ⊢/⟨ k ⟩ σ ∈ Γ → Γ ⊢Var x ∈ j → Miss σ x y →
                     lookup Δ y ≡ lookup Γ x
  lookup-/⟨⟩∈-Miss σ∈Γ (∈-var {j} x Γ[x]≡kd-j) missP =
    helper (lookup-Miss missP) (lookup-/⟨⟩∈ σ∈Γ x)
    where
      helper : ∀ {n} {Δ : Ctx n} {r y b k} →
               r ≡ miss y → Δ ⊢?⟨ k ⟩ r ∈ b → lookup Δ y ≡ b
      helper refl (∈-miss y Δ[y]≡b) = Δ[y]≡b

  open KindSimpLemmas simpLemmasKind′

  -- TODO: explain why this terminates.
  mutual

    -- Hereditary substitutions preserve simple well-formedness and
    -- kinding (of kinds, normal types and spines).

    kds-/⟨⟩ : ∀ {m n Γ k Δ} {σ : SVSub m n} {j} →
              Γ ⊢ j kds → Δ ⊢/⟨ k ⟩ σ ∈ Γ → Δ ⊢ j Kind/⟨ k ⟩ σ kds
    kds-/⟨⟩ (kds-⋯ a∈★ b∈★)     σ∈Γ = kds-⋯ (Nf∈-/⟨⟩ a∈★ σ∈Γ) (Nf∈-/⟨⟩ b∈★ σ∈Γ)
    kds-/⟨⟩ (kds-Π j-kds k-kds) σ∈Γ =
      kds-Π (kds-/⟨⟩ j-kds σ∈Γ) (kds-/⟨⟩ k-kds (∈-H↑′ σ∈Γ))

    Nf∈-/⟨⟩ : ∀ {m n Γ k Δ} {σ : SVSub m n} {a j} →
              Γ ⊢Nf a ∈ j → Δ ⊢/⟨ k ⟩ σ ∈ Γ → Δ ⊢Nf a /⟨ k ⟩ σ ∈ j
    Nf∈-/⟨⟩ ∈-⊥-f             σ∈Γ = ∈-⊥-f
    Nf∈-/⟨⟩ ∈-⊤-f             σ∈Γ = ∈-⊤-f
    Nf∈-/⟨⟩ (∈-∀-f k-kds a∈★) σ∈Γ =
      ∈-∀-f (kds-/⟨⟩ k-kds σ∈Γ) (Nf∈-/⟨⟩ a∈★ (∈-H↑′ σ∈Γ))
    Nf∈-/⟨⟩ (∈-→-f a∈★ b∈★)   σ∈Γ =
      ∈-→-f (Nf∈-/⟨⟩ a∈★ σ∈Γ) (Nf∈-/⟨⟩ b∈★ σ∈Γ)
    Nf∈-/⟨⟩ (∈-Π-i {j} {a} {k} j-kds a∈k) σ∈Γ =
      subst (λ l → _ ⊢Nf Λ∙ j a /⟨ _ ⟩ _ ∈ l ⇒ k) (⌊⌋-Kind/⟨⟩ j)
            (∈-Π-i (kds-/⟨⟩ j-kds σ∈Γ) (Nf∈-/⟨⟩ a∈k (∈-H↑′ σ∈Γ)))
    Nf∈-/⟨⟩ (∈-ne a∈★)        σ∈Γ = Ne∈-/⟨⟩ a∈★ σ∈Γ

    Sp∈-/⟨⟩ : ∀ {m n Γ k Δ} {σ : SVSub m n} {as j₁ j₂} →
              Γ ⊢ j₁ ∋∙ as ∈ j₂ → Δ ⊢/⟨ k ⟩ σ ∈ Γ → Δ ⊢ j₁ ∋∙ as //⟨ k ⟩ σ ∈ j₂
    Sp∈-/⟨⟩ ∈-[]                   σ∈Γ = ∈-[]
    Sp∈-/⟨⟩ (∈-∷ a∈j₁ j₂[a]∈as∈j₃) σ∈Γ =
      ∈-∷ (Nf∈-/⟨⟩ a∈j₁ σ∈Γ) (Sp∈-/⟨⟩ j₂[a]∈as∈j₃ σ∈Γ)

    -- Hereditary substitutions preserve the shapes of neutral types
    -- (but not neutrality itself).

    Ne∈-/⟨⟩ : ∀ {m n Γ k Δ} {σ : SVSub m n} {a} →
              Γ ⊢Ne a ∈ ★ → Δ ⊢/⟨ k ⟩ σ ∈ Γ → Δ ⊢Nf a /⟨ k ⟩ σ ∈ ★
    Ne∈-/⟨⟩ (∈-∙ (∈-var x Γ[x]≡kd-j) j∈as∈l) σ∈Γ =
      ?⟨⟩∈-?∙∙ (subst (_ ⊢?⟨ _ ⟩ _ ∈_) Γ[x]≡kd-j (lookup-/⟨⟩∈ σ∈Γ x))
               (Sp∈-/⟨⟩ j∈as∈l σ∈Γ)

    -- Applications in simple kinding are admissible.

    ?⟨⟩∈-?∙∙ : ∀ {n} {Γ : Ctx n} {r as k j} →
               Γ ⊢?⟨ k ⟩ r ∈ kd j → Γ ⊢ j ∋∙ as ∈ ★ → Γ ⊢Nf r ?∙∙⟨ k ⟩ as ∈ ★
    ?⟨⟩∈-?∙∙ (∈-hit a∈j)          j∋as∈★ = Nf∈-∙∙ a∈j j∋as∈★
    ?⟨⟩∈-?∙∙ (∈-miss y Γ[y]≡kd-j) j∋as∈★ = ∈-ne (∈-∙ (∈-var y Γ[y]≡kd-j) j∋as∈★)

    Nf∈-∙∙ : ∀ {n} {Γ : Ctx n} {a as j k} →
             Γ ⊢Nf a ∈ j → Γ ⊢ j ∋∙ as ∈ k → Γ ⊢Nf a ∙∙⟨ j ⟩ as ∈ k
    Nf∈-∙∙ a∈j   ∈-[]             = a∈j
    Nf∈-∙∙ a∈j⇒k (∈-∷ b∈j k∋as∈l) = Nf∈-∙∙ (Nf∈-Π-e a∈j⇒k b∈j) k∋as∈l

    Nf∈-Π-e : ∀ {n} {Γ : Ctx n} {a b j k} →
              Γ ⊢Nf a ∈ j ⇒ k → Γ ⊢Nf b ∈ j → Γ ⊢Nf a ⌜·⌝⟨ j ⇒ k ⟩ b ∈ k
    Nf∈-Π-e (∈-Π-i j-kds a∈k) b∈⌊j⌋ = Nf∈-/⟨⟩ a∈k (∈-hsub b∈⌊j⌋)

  -- Concatenation of simply well-formed spines results in application.
  Nf∈-++-∙∙⟨⟩ : ∀ {n} {Γ : Ctx n} {a bs cs j k l} →
                Γ ⊢Nf a ∈ j → Γ ⊢ j ∋∙ bs ∈ k → Γ ⊢ k ∋∙ cs ∈ l →
                a ∙∙⟨ j ⟩ (bs List.++ cs) ≡ a ∙∙⟨ j ⟩ bs ∙∙⟨ k ⟩ cs
  Nf∈-++-∙∙⟨⟩ a∈j     ∈-[]                  k∋cs∈l = refl
  Nf∈-++-∙∙⟨⟩ a∈j₁⇒j₂ (∈-∷ b∈j₁ j₂[b]∋bs∈k) k∋cs∈l =
    Nf∈-++-∙∙⟨⟩ (Nf∈-Π-e a∈j₁⇒j₂ b∈j₁) j₂[b]∋bs∈k k∋cs∈l

  -- Another admissible kinding rule for applications.
  Nf∈-Π-e′ : ∀ {n} {Γ : Ctx n} {a b j k} →
             Γ ⊢Nf a ∈ j ⇒ k → Γ ⊢Nf b ∈ j → Γ ⊢Nf a ↓⌜·⌝ b ∈ k
  Nf∈-Π-e′ (∈-Π-i j-kds a∈k) b∈⌊j⌋ = Nf∈-/⟨⟩ a∈k (∈-hsub b∈⌊j⌋)

  mutual

    -- Simply well-kinded hereditary substitutions in simply
    -- well-formed kinds and simply well-kinded types commute.
    --
    -- NOTE: this is a variant of the `sub-commutes' lemma from
    -- Data.Fin.Substitution.Lemmas adapted to hereditary
    -- substitutions.

    kds-[]-/⟨⟩-↑⋆ : ∀ {i m n} (E : CtxExt (suc m) i) {Γ Δ}
                    {j b k l} {σ : SVSub m n} →
                    E ++ kd k ∷ Γ ⊢ j kds → Γ ⊢Nf b ∈ k → Δ ⊢/⟨ l ⟩ σ ∈ Γ →
                    j Kind/⟨ k ⟩ (sub b ↑⋆ i) Kind/⟨ l ⟩ σ ↑⋆ i ≡
                      j Kind/⟨ l ⟩ (σ ↑) ↑⋆ i Kind/⟨ k ⟩ sub (b /⟨ l ⟩ σ) ↑⋆ i
    kds-[]-/⟨⟩-↑⋆ E (kds-⋯ a∈★ b∈★)     c∈k σ∈Γ =
      cong₂ _⋯_ (Nf∈-[]-/⟨⟩-↑⋆ E a∈★ c∈k σ∈Γ) (Nf∈-[]-/⟨⟩-↑⋆ E b∈★ c∈k σ∈Γ)
    kds-[]-/⟨⟩-↑⋆ E (kds-Π j-kds k-kds) b∈k σ∈Γ =
      cong₂ Π (kds-[]-/⟨⟩-↑⋆ E j-kds b∈k σ∈Γ)
              (kds-[]-/⟨⟩-↑⋆ (_ ∷ E) k-kds b∈k σ∈Γ)

    Nf∈-[]-/⟨⟩-↑⋆ : ∀ {i m n} (E : CtxExt (suc m) i) {Γ Δ}
                    {a b j k l} {σ : SVSub m n} →
                    E ++ kd k ∷ Γ ⊢Nf a ∈ j → Γ ⊢Nf b ∈ k → Δ ⊢/⟨ l ⟩ σ ∈ Γ →
                    a /⟨ k ⟩ (sub b ↑⋆ i) /⟨ l ⟩ σ ↑⋆ i ≡
                      a /⟨ l ⟩ (σ ↑) ↑⋆ i /⟨ k ⟩ sub (b /⟨ l ⟩ σ) ↑⋆ i
    Nf∈-[]-/⟨⟩-↑⋆ E ∈-⊥-f b∈k σ∈Γ = refl
    Nf∈-[]-/⟨⟩-↑⋆ E ∈-⊤-f b∈k σ∈Γ = refl
    Nf∈-[]-/⟨⟩-↑⋆ E (∈-∀-f k-kds a∈★) b∈k σ∈Γ =
      cong (_∙ []) (cong₂ Π (kds-[]-/⟨⟩-↑⋆ E k-kds b∈k σ∈Γ)
                            (Nf∈-[]-/⟨⟩-↑⋆ (_ ∷ E) a∈★ b∈k σ∈Γ))
    Nf∈-[]-/⟨⟩-↑⋆ E (∈-→-f a∈★ b∈★)   c∈k σ∈Γ =
      cong (_∙ []) (cong₂ _⇒_ (Nf∈-[]-/⟨⟩-↑⋆ E a∈★ c∈k σ∈Γ)
                              (Nf∈-[]-/⟨⟩-↑⋆ E b∈★ c∈k σ∈Γ))
    Nf∈-[]-/⟨⟩-↑⋆ E (∈-Π-i j-kds a∈l) b∈k σ∈Γ =
      cong (_∙ []) (cong₂ Λ (kds-[]-/⟨⟩-↑⋆ E j-kds b∈k σ∈Γ)
                            (Nf∈-[]-/⟨⟩-↑⋆ (_ ∷ E) a∈l b∈k σ∈Γ))
    Nf∈-[]-/⟨⟩-↑⋆ E (∈-ne a∈★)        b∈k σ∈Γ = Ne∈-[]-/⟨⟩-↑⋆ E a∈★ b∈k σ∈Γ

    Ne∈-[]-/⟨⟩-↑⋆ : ∀ {i m n} (E : CtxExt (suc m) i) {Γ Δ}
                    {a b j k l} {σ : SVSub m n} →
                    E ++ kd k ∷ Γ ⊢Ne a ∈ j → Γ ⊢Nf b ∈ k → Δ ⊢/⟨ l ⟩ σ ∈ Γ →
                    a /⟨ k ⟩ (sub b ↑⋆ i) /⟨ l ⟩ σ ↑⋆ i ≡
                      a /⟨ l ⟩ (σ ↑) ↑⋆ i /⟨ k ⟩ sub (b /⟨ l ⟩ σ) ↑⋆ i
    Ne∈-[]-/⟨⟩-↑⋆ {i} E {b = b} (∈-∙ (∈-var x _) j∋as∈l) b∈k σ∈Γ
      with hit? (sub b ↑⋆ i) x
    Ne∈-[]-/⟨⟩-↑⋆ {i} E {_} {_} {var x ∙ as} {b} {_} {k} {l} {σ}
                  (∈-∙ (∈-var x Γ[x]=kd-j) j∋as∈l) b∈k σ∈Γ
      | hit a hitP =
      let σ₁′ = sub b ↑⋆ i
          σ₂′ = sub (b /⟨ l ⟩ σ) ↑⋆ i
          as₁ = as //⟨ k ⟩ σ₁′
          as₂ = as //⟨ l ⟩ ((σ ↑) ↑⋆ i)
          [b/i]∈E++k∷Γ = ∈-H↑⋆ E (∈-hsub b∈k)
          _ , j≡k   = lookup-/⟨⟩∈-Hit [b/i]∈E++k∷Γ (∈-var x Γ[x]=kd-j) hitP
          k∋as∈l    = subst (_ ⊢_∋∙ as ∈ _) j≡k j∋as∈l
          σ↑⋆i∈E++Γ = ∈-H↑⋆ (re-idx E) σ∈Γ
      in begin
        lookupSV σ₁′ x ?∙∙⟨ k ⟩ as₁ /⟨ l ⟩ σ ↑⋆ i
      ≡⟨ cong (λ r → r ?∙∙⟨ k ⟩ as₁ /⟨ l ⟩ _)
              (trans (lookup-Hit hitP) (cong hit (Hit-sub-↑⋆₂ i hitP))) ⟩
        weakenElim⋆ i b ∙∙⟨ k ⟩ as₁ /⟨ l ⟩ σ ↑⋆ i
      ≡⟨ Nf∈-∙∙-/⟨⟩ (Nf∈-weaken⋆ (re-idx E) b∈k)
                    (Sp∈-/⟨⟩ k∋as∈l [b/i]∈E++k∷Γ) σ↑⋆i∈E++Γ ⟩
        (weakenElim⋆ i b /⟨ l ⟩ σ ↑⋆ i) ∙∙⟨ k ⟩ (as₁ //⟨ l ⟩ σ ↑⋆ i)
      ≡⟨ cong₂ (_∙∙⟨ k ⟩_) (sym (weaken⋆-/⟨⟩-↑⋆ i b))
               (Sp∈-[]-/⟨⟩-↑⋆ E j∋as∈l b∈k σ∈Γ) ⟩
        weakenElim⋆ i (b /⟨ l ⟩ σ) ∙∙⟨ k ⟩ (as₂ //⟨ k ⟩ σ₂′)
      ≡˘⟨ cong (_?∙∙⟨ k ⟩ (as₂ //⟨ k ⟩ σ₂′)) (lookup-Hit (Hit-sub-↑⋆ i)) ⟩
        lookupSV σ₂′ (raise i zero) ?∙∙⟨ k ⟩ (as₂ //⟨ k ⟩ σ₂′)
      ≡⟨⟩
        miss (raise i zero) ?∙∙⟨ l ⟩ as₂ /⟨ k ⟩ σ₂′
      ≡˘⟨ cong (λ r → r ?∙∙⟨ l ⟩ as₂ /⟨ k ⟩ σ₂′)
               (lookup-Miss (Miss-↑⋆ i under)) ⟩
        lookupSV ((σ ↑) ↑⋆ i) (raise i zero) ?∙∙⟨ l ⟩ as₂ /⟨ k ⟩ σ₂′
      ≡˘⟨ cong (λ y → lookupSV ((σ ↑) ↑⋆ i) y ?∙∙⟨ l ⟩ as₂ /⟨ k ⟩ σ₂′)
               (Hit-sub-↑⋆₁ i hitP) ⟩
        lookupSV ((σ ↑) ↑⋆ i) x ?∙∙⟨ l ⟩ as₂ /⟨ k ⟩ σ₂′
      ∎
    Ne∈-[]-/⟨⟩-↑⋆ {i} E {_} {_} {var x ∙ as} {b} {_} {k} {l} {σ}
                  (∈-∙ (∈-var x Γ[x]=kd-j) j∋as∈l) b∈k σ∈Γ
      | miss y missP-[a/i] with hit? (σ ↑⋆ i) y
    ... | hit a hitP =
      let σ₁′ = sub b ↑⋆ i
          σ₂′ = sub (b /⟨ l ⟩ σ) ↑⋆ i
          as₁ = as //⟨ k ⟩ σ₁′
          as₂ = as //⟨ l ⟩ ((σ ↑) ↑⋆ i)
          hitP-σ↑↑⋆ = Hit-↑-↑⋆ i hitP
          σ₂′∈E++Γ  = ∈-H↑⋆ (re-idx E) (∈-hsub (Nf∈-/⟨⟩ b∈k σ∈Γ))
          σ∈E++k∷Γ  = ∈-H↑⋆ E (∈-H↑ σ∈Γ)
          x≡i+1+y   = Miss-sub-↑⋆′ i y missP-[a/i]
          i+1+y∈j   = subst (_ ⊢Var_∈ _) x≡i+1+y (∈-var x Γ[x]=kd-j)
          a∈l , j≡l = lookup-/⟨⟩∈-Hit σ∈E++k∷Γ i+1+y∈j hitP-σ↑↑⋆
          l∋as₂∈l   = subst (_ ⊢_∋∙ as₂ ∈ _) j≡l (Sp∈-/⟨⟩ j∋as∈l σ∈E++k∷Γ)
      in begin
        lookupSV σ₁′ x ?∙∙⟨ k ⟩ as₁ /⟨ l ⟩ σ ↑⋆ i
      ≡⟨ cong (λ r → r ?∙∙⟨ k ⟩ as₁ /⟨ l ⟩ σ ↑⋆ i) (lookup-Miss missP-[a/i]) ⟩
        var y ∙ as₁ /⟨ l ⟩ σ ↑⋆ i
      ≡⟨⟩
        lookupSV (σ ↑⋆ i) y ?∙∙⟨ l ⟩ (as₁ //⟨ l ⟩ σ ↑⋆ i)
      ≡⟨ cong₂ (_?∙∙⟨ l ⟩_) (lookup-Hit hitP) (Sp∈-[]-/⟨⟩-↑⋆ E j∋as∈l b∈k σ∈Γ) ⟩
        a ∙∙⟨ l ⟩ (as₂ //⟨ k ⟩ σ₂′)
      ≡˘⟨ cong (_∙∙⟨ l ⟩ (as₂ //⟨ k ⟩ σ₂′)) (/Var-wk-↑⋆-hsub-vanishes i a) ⟩
        (a Elim/Var V.wk V.↑⋆ i /⟨ k ⟩ σ₂′) ∙∙⟨ l ⟩ (as₂ //⟨ k ⟩ σ₂′)
      ≡˘⟨ Nf∈-∙∙-/⟨⟩ a∈l l∋as₂∈l σ₂′∈E++Γ ⟩
        (a Elim/Var V.wk V.↑⋆ i) ∙∙⟨ l ⟩ as₂ /⟨ k ⟩ σ₂′
      ≡˘⟨ cong (λ r → r ?∙∙⟨ l ⟩ as₂ /⟨ k ⟩ σ₂′) (lookup-Hit hitP-σ↑↑⋆) ⟩
        lookupSV ((σ ↑) ↑⋆ i) (lift i suc y) ?∙∙⟨ l ⟩ as₂ /⟨ k ⟩ σ₂′
      ≡˘⟨ cong (λ z → lookupSV ((σ ↑) ↑⋆ i) z ?∙∙⟨ l ⟩ as₂ /⟨ k ⟩ σ₂′) x≡i+1+y ⟩
        lookupSV ((σ ↑) ↑⋆ i) x ?∙∙⟨ l ⟩ as₂ /⟨ k ⟩ σ₂′
      ∎
    ... | miss z missP =
      let σ₁′ = sub b ↑⋆ i
          σ₂′ = sub (b /⟨ l ⟩ σ) ↑⋆ i
          as₁ = as //⟨ k ⟩ σ₁′
          as₂ = as //⟨ l ⟩ ((σ ↑) ↑⋆ i)
          missP-σ↑↑⋆ = Miss-↑-↑⋆ i missP
          x≡i+1+y    = Miss-sub-↑⋆′ i y missP-[a/i]
      in begin
        lookupSV σ₁′ x ?∙∙⟨ k ⟩ as₁ /⟨ l ⟩ σ ↑⋆ i
      ≡⟨ cong (λ r → r ?∙∙⟨ k ⟩ as₁ /⟨ l ⟩ σ ↑⋆ i) (lookup-Miss missP-[a/i]) ⟩
        var y ∙ as₁ /⟨ l ⟩ σ ↑⋆ i
      ≡⟨⟩
        lookupSV (σ ↑⋆ i) y ?∙∙⟨ l ⟩ (as₁ //⟨ l ⟩ σ ↑⋆ i)
      ≡⟨ cong₂ (_?∙∙⟨ l ⟩_) (lookup-Miss missP)
               (Sp∈-[]-/⟨⟩-↑⋆ E j∋as∈l b∈k σ∈Γ) ⟩
        var z ∙ (as₂ //⟨ k ⟩ σ₂′)
      ≡˘⟨ cong (_?∙∙⟨ k ⟩ (as₂ //⟨ k ⟩ σ₂′)) (lookup-Miss (Miss-sub-↑⋆ i z)) ⟩
        lookupSV σ₂′ (lift i suc z) ?∙∙⟨ k ⟩ (as₂ //⟨ k ⟩ σ₂′)
      ≡⟨⟩
        var (lift i suc z) ∙ as₂ /⟨ k ⟩ σ₂′
      ≡˘⟨ cong (λ r → r ?∙∙⟨ l ⟩ as₂ /⟨ k ⟩ σ₂′) (lookup-Miss missP-σ↑↑⋆) ⟩
        lookupSV ((σ ↑) ↑⋆ i) (lift i suc y) ?∙∙⟨ l ⟩ as₂ /⟨ k ⟩ σ₂′
      ≡˘⟨ cong (λ z → lookupSV ((σ ↑) ↑⋆ i) z ?∙∙⟨ l ⟩ as₂ /⟨ k ⟩ σ₂′) x≡i+1+y ⟩
        lookupSV ((σ ↑) ↑⋆ i) x ?∙∙⟨ l ⟩ as₂ /⟨ k ⟩ σ₂′
      ∎

    Sp∈-[]-/⟨⟩-↑⋆ : ∀ {i m n} (E : CtxExt (suc m) i) {Γ Δ}
                    {as b j₁ j₂ k l} {σ : SVSub m n} →
                    E ++ kd k ∷ Γ ⊢ j₁ ∋∙ as ∈ j₂ →
                    Γ ⊢Nf b ∈ k → Δ ⊢/⟨ l ⟩ σ ∈ Γ →
                    as //⟨ k ⟩ (sub b ↑⋆ i) //⟨ l ⟩ σ ↑⋆ i ≡
                      as //⟨ l ⟩ (σ ↑) ↑⋆ i //⟨ k ⟩ sub (b /⟨ l ⟩ σ) ↑⋆ i
    Sp∈-[]-/⟨⟩-↑⋆ E ∈-[]                b∈k σ∈Γ = refl
    Sp∈-[]-/⟨⟩-↑⋆ E (∈-∷ a∈j₁ j₂∋as∈j₃) b∈k σ∈Γ =
      cong₂ _∷_ (Nf∈-[]-/⟨⟩-↑⋆ E a∈j₁ b∈k σ∈Γ) (Sp∈-[]-/⟨⟩-↑⋆ E j₂∋as∈j₃ b∈k σ∈Γ)

    -- Reducing applications commute with hereditary substitution.

    Nf∈-∙∙-/⟨⟩ : ∀ {l m n Γ Δ} {σ : SVSub m n} {a as j k} →
                 Γ ⊢Nf a ∈ j → Γ ⊢ j ∋∙ as ∈ k → Δ ⊢/⟨ l ⟩ σ ∈ Γ →
                 a ∙∙⟨ j ⟩ as /⟨ l ⟩ σ ≡ (a /⟨ l ⟩ σ) ∙∙⟨ j ⟩ (as //⟨ l ⟩ σ)
    Nf∈-∙∙-/⟨⟩ a∈j ∈-[] σ∈Γ = refl
    Nf∈-∙∙-/⟨⟩ {l} {σ = σ} {a} {b ∷ bs} {j ⇒ k} a∈j⇒k (∈-∷ b∈j k∋bs∈l) σ∈Γ =
      begin
        a ⌜·⌝⟨ j ⇒ k ⟩ b ∙∙⟨ k ⟩ bs /⟨ l ⟩ σ
      ≡⟨ Nf∈-∙∙-/⟨⟩ (Nf∈-Π-e a∈j⇒k b∈j) k∋bs∈l σ∈Γ ⟩
        (a ⌜·⌝⟨ j ⇒ k ⟩ b /⟨ l ⟩ σ) ∙∙⟨ _ ⟩ (bs //⟨ l ⟩ σ)
      ≡⟨ cong (_∙∙⟨ k ⟩ (bs //⟨ l ⟩ σ)) (Nf∈-Π-e-/⟨⟩ a∈j⇒k b∈j σ∈Γ) ⟩
        (a /⟨ l ⟩ σ) ⌜·⌝⟨ j ⇒ k ⟩ (b /⟨ l ⟩ σ) ∙∙⟨ k ⟩ (bs //⟨ l ⟩ σ)
      ∎

    Nf∈-Π-e-/⟨⟩ : ∀ {l m n Γ Δ} {σ : SVSub m n} {a b j k} →
                  Γ ⊢Nf a ∈ j ⇒ k → Γ ⊢Nf b ∈ j → Δ ⊢/⟨ l ⟩ σ ∈ Γ →
                  a ⌜·⌝⟨ j ⇒ k ⟩ b /⟨ l ⟩ σ ≡
                    (a /⟨ l ⟩ σ) ⌜·⌝⟨ j ⇒ k ⟩ (b /⟨ l ⟩ σ)
    Nf∈-Π-e-/⟨⟩ (∈-Π-i j-kds a∈k) b∈⌊j⌋ σ∈Γ = Nf∈-[]-/⟨⟩-↑⋆ [] a∈k b∈⌊j⌋ σ∈Γ

  -- Potentially reducing applications commute with hereditary
  -- substitution.

  Nf∈-Π-e-/⟨⟩′ : ∀ {l m n Γ Δ} {σ : SVSub m n} {a b j k} →
                Γ ⊢Nf a ∈ j ⇒ k → Γ ⊢Nf b ∈ j → Δ ⊢/⟨ l ⟩ σ ∈ Γ →
                a ↓⌜·⌝ b /⟨ l ⟩ σ ≡ (a /⟨ l ⟩ σ) ↓⌜·⌝ (b /⟨ l ⟩ σ)
  Nf∈-Π-e-/⟨⟩′ {l} {σ = σ} {_} {b} (∈-Π-i {j} {a} j-kds a∈k) b∈⌊j⌋ σ∈Γ =
    begin
      (a [ b ∈ ⌊ j ⌋ ]) /⟨ l ⟩ σ
    ≡⟨ Nf∈-[]-/⟨⟩-↑⋆ [] a∈k b∈⌊j⌋ σ∈Γ ⟩
      (a /⟨ l ⟩ σ ↑) [ b /⟨ l ⟩ σ ∈ ⌊ j ⌋ ]
    ≡⟨ cong ((a /⟨ l ⟩ σ ↑) [ b /⟨ l ⟩ σ ∈_]) (sym (⌊⌋-Kind/⟨⟩ j)) ⟩
      (a /⟨ l ⟩ σ ↑) [ b /⟨ l ⟩ σ ∈ ⌊ j Kind/⟨ l ⟩ σ ⌋ ]
    ∎

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

postulate Char : Set

private
  {-# BUILTIN CHAR Char #-}

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2016-09-22, issue #2183, issue reported by Ulf

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

module _ (n : Nat) where

  foo : (m : Nat) → n ≡ m → Nat
  foo m refl = {!m!}

-- Splitting on m fails currently, as it internally is .n
-- We may be doing something about this in the future.

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.MaybeEmbed {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution

open import Tools.Product

-- Any level can be embedded into the highest level (validity variant).
maybeEmbᵛ : ∀ {l A Γ}
            ([Γ] : ⊩ᵛ Γ)
          → Γ ⊩ᵛ⟨ l ⟩ A / [Γ]
          → Γ ⊩ᵛ⟨ ¹ ⟩ A / [Γ]
maybeEmbᵛ {⁰} [Γ] [A] ⊢Δ [σ] =
  let [σA]  = proj₁ ([A] ⊢Δ [σ])
      [σA]′ = maybeEmb (proj₁ ([A] ⊢Δ [σ]))
  in  [σA]′
  ,   (λ [σ′] [σ≡σ′] → irrelevanceEq [σA] [σA]′ (proj₂ ([A] ⊢Δ [σ]) [σ′] [σ≡σ′]))
maybeEmbᵛ {¹} [Γ] [A] = [A]

-- The lowest level can be embedded in any level (validity variant).
maybeEmbₛ′ : ∀ {l A Γ}
             ([Γ] : ⊩ᵛ Γ)
           → Γ ⊩ᵛ⟨ ⁰ ⟩ A / [Γ]
           → Γ ⊩ᵛ⟨ l ⟩ A / [Γ]
maybeEmbₛ′ {⁰} [Γ] [A] = [A]
maybeEmbₛ′ {¹} [Γ] [A] ⊢Δ [σ] =
  let [σA]  = proj₁ ([A] ⊢Δ [σ])
      [σA]′ = maybeEmb′ (proj₁ ([A] ⊢Δ [σ]))
  in  [σA]′
  ,   (λ [σ′] [σ≡σ′] → irrelevanceEq [σA] [σA]′ (proj₂ ([A] ⊢Δ [σ]) [σ′] [σ≡σ′]))


text:
F : Set → Set
F A = A → A

{-# POLARITY F ++ #-}


text:
module Common.SumProperties where

open import Function as Fun
open import Data.Sum as Sum
open import Relation.Binary.PropositionalEquality as PE hiding ([_])
open ≡-Reasoning

copair-elimˡ : {A B C : Set} {f : A → C} {g : B → C} (x : A) →
               ([ f , g ]′ ) (inj₁ x) ≡ f x
copair-elimˡ x = refl

copair-elimʳ : {A B C : Set} {f : A → C} {g : B → C} (x : B) →
               ([ f , g ]′ ) (inj₂ x) ≡ g x
copair-elimʳ x = refl

copair-sum-map-merge : {A A' B B' C : Set}
                     {f₁ : A → A'} {f₂ : B → B'} {g₁ : A' → C} {g₂ : B' → C}
                     (x : A ⊎ B) →
                     ([ g₁ , g₂ ]′ ∘ Sum.map f₁ f₂) x ≡ [ g₁ ∘ f₁ , g₂ ∘ f₂ ]′ x
copair-sum-map-merge (inj₁ x) = refl
copair-sum-map-merge (inj₂ y) = refl

copair-cong : {A B C : Set} {f f' : A → C} {g : B → C}
              (p : (x : A) → f x ≡ f' x) →
              (x : A ⊎ B) →
              [ f , g ]′ x ≡ [ f' , g ]′ x
copair-cong {A} {B} {C} {f} {f'} {g} p (inj₁ x) =
  begin
    ([ f , g ]′ (inj₁ x))
  ≡⟨ refl ⟩
    f x
  ≡⟨ p x ⟩
    f' x
  ≡⟨ refl ⟩
    [ f' , g ]′ (inj₁ x)
  ∎
copair-cong p (inj₂ y) = refl

copair-distr : {A B C D : Set} {f : A → C} {g : B → C} {h : C → D}
              (x : A ⊎ B) →
              [ h ∘ f , h ∘ g ]′ x ≡ (h ∘ [ f , g ]′) x
copair-distr (inj₁ x) = refl
copair-distr (inj₂ y) = refl

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module bags where

open import Data.PropFormula.Syntax 4
open import Data.PropFormula.SyntaxExperiment 4 public
open import Data.Fin using (suc; zero; #_)
open import Relation.Binary.PropositionalEquality using (_≡_)

p : PropFormula
p = Var (# 0)

q : PropFormula
q = Var (# 1)

pq : PropFormula
pq = p ∧ q

qp : PropFormula
qp = q ∧ p

listpq : List PropFormula
listpq = toList pq

listqp : List PropFormula
listqp = toList qp

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
module seven where

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Naturals using (ℕ; zero; suc)

seven : ℕ
seven = suc (suc (suc (suc (suc (suc (suc zero))))))

_ : seven ≡ 7
_ = refl

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


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

module Definition.Conversion.Universe where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.RedSteps
open import Definition.Conversion
open import Definition.Conversion.Reduction
open import Definition.Conversion.Lift

import Tools.PropositionalEquality as PE

-- Algorithmic equality of terms in WHNF of type U are equal as types.
univConv↓ : ∀ {A B r Γ l}
          → Γ ⊢ A [conv↓] B ∷ Univ r l ^ next l
          → Γ ⊢ A [conv↓] B ^ [ r , ι l ]
univConv↓ X = univ X

-- Algorithmic equality of terms of type U are equal as types.
univConv↑ : ∀ {A B r Γ l}
      → Γ ⊢ A [conv↑] B ∷ Univ r l ^ next l
      → Γ ⊢ A [conv↑] B ^ [ r , ι l ]
univConv↑ ([↑]ₜ B₁ t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u)
      rewrite PE.sym (whnfRed* D Uₙ) =
  reductionConv↑ (univ* d) (univ* d′) whnft′ whnfu′ (liftConv (univConv↓ t<>u))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt