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

open import Agda.Primitive
open import Prelude
import GSeTT.Typed-Syntax
import Globular-TT.Syntax

{- Disk and Sphere contexts - properties -}
module Globular-TT.Disks {l} (index : Set l) (rule : index → GSeTT.Typed-Syntax.Ctx × (Globular-TT.Syntax.Pre-Ty index)) (eqdec-index : eqdec index) where
  open import Globular-TT.Syntax index
  open import Globular-TT.Rules index rule
  open import Globular-TT.CwF-Structure index rule
  open import Globular-TT.Uniqueness-Derivations index rule eqdec-index
  open import Globular-TT.Typed-Syntax index rule eqdec-index

  {- Definition of "universal source and target variables" -}
  n-src : ℕ → ℕ
  n-tgt : ℕ → ℕ
  n⇒ : ℕ → Pre-Ty

  n-src O = O
  n-src (S n) = S (n-tgt n)
  n-tgt n = S (n-src n)

  n⇒ O = ∗
  n⇒ (S n) = ⇒ (n⇒ n) (Var (n-src n)) (Var (n-tgt  n))

  dim⇒ : ∀ (n : ℕ) → dim (n⇒ n) == n
  dim⇒ O = idp
  dim⇒ (S n) = S= (dim⇒ n)

  {- Syntactic definition of disks and spheres -}
  Pre-𝕊 : ℕ → Pre-Ctx
  Pre-𝔻 : ℕ → Pre-Ctx

  Pre-𝕊 O = ⊘
  Pre-𝕊 (S n) = (Pre-𝔻 n) ∙ C-length (Pre-𝔻 n) # n⇒ n
  Pre-𝔻 n = (Pre-𝕊 n) ∙ C-length (Pre-𝕊 n) # n⇒ n

  𝕊-length : ∀ n → C-length (Pre-𝕊 n) == n-src n
  𝕊-length O = idp
  𝕊-length (S n) = S= (S= (𝕊-length n))
  {-# REWRITE 𝕊-length #-}

  {- Disk and Sphere context are valid -}
  𝕊⊢ : ∀ n → Pre-𝕊 n ⊢C
  𝔻⊢ : ∀ n → Pre-𝔻 n ⊢C
  𝕊⊢⇒ : ∀ n → Pre-𝕊 n ⊢T n⇒ n

  𝕊⊢ O = ec
  𝕊⊢ (S n) = cc (𝔻⊢ n) (wkT (𝕊⊢⇒ n) (𝔻⊢ n)) idp
  𝔻⊢ n = cc (𝕊⊢ n) (𝕊⊢⇒ n) idp

  𝕊⊢⇒ O = ob ec
  𝕊⊢⇒ (S n) = ar (wkT (wkT (𝕊⊢⇒ n) (𝔻⊢ n)) (𝕊⊢ (S n))) (wkt (var (𝔻⊢ n) (inr (((𝕊-length n) ^) , idp))) (𝕊⊢ (S n))) (var (𝕊⊢ (S n)) (inr ((S= (𝕊-length n) ^) , idp)))

  𝕊 : ℕ → Ctx
  𝕊 n = Pre-𝕊 n , 𝕊⊢ n

  𝔻 : ℕ → Ctx
  𝔻 n = Pre-𝔻 n , 𝔻⊢ n

  Ty-n : ∀ {Γ} → Σ ℕ (λ n →  Sub Γ (𝕊 n)) → Ty Γ
  Ty-n {Γ} (n , (γ , Γ⊢γ:Sn) ) = ((n⇒ n)[ γ ]Pre-Ty) , ([]T (𝕊⊢⇒ n) Γ⊢γ:Sn)

  private
    Pre-χ : Pre-Ty → Pre-Sub

    Pre-χ ∗ = <>
    Pre-χ (⇒ A t u) = < < Pre-χ A , n-src (dim A) ↦ t > , n-tgt (dim A) ↦ u >

    χ_⊢ : ∀ {Γ A} → (Γ⊢A : Γ ⊢T A) → Γ ⊢S (Pre-χ A) > Pre-𝕊 (dim A)
    ⇒[χ_] : ∀ {Γ A} → (Γ⊢A : Γ ⊢T A) → A == ((n⇒  (dim A))[ Pre-χ A ]Pre-Ty)

    χ ob Γ⊢ ⊢ = es Γ⊢
    χ_⊢ {Γ} {⇒ A t u} (ar Γ⊢A Γ⊢t:A Γ⊢u:A) =
      let Γ⊢χt = sc χ Γ⊢A ⊢ (𝔻⊢ (dim A)) (trT (⇒[χ Γ⊢A ]) Γ⊢t:A) idp in
      sc Γ⊢χt (𝕊⊢ (S (dim A))) (trT (⇒[χ Γ⊢A ] >> (wk[]T (𝕊⊢⇒ (dim A)) Γ⊢χt ^)) Γ⊢u:A) idp

    ⇒[χ_] {Γ} {.∗} (ob _) = idp
    ⇒[χ_] {Γ} {(⇒ A t u)} (ar Γ⊢A Γ⊢t:A Γ⊢u:A) with eqdecℕ (n-src (dim A)) (n-tgt (dim A)) | eqdecℕ (n-src (dim A)) (n-src (dim A)) | eqdecℕ (S (n-src (dim A))) (S (n-src (dim A)))
    ...                                     | inl contra | _ | _ = ⊥-elim (n≠Sn _ contra)
    ...                                     | inr _ | inr n≠n | _ = ⊥-elim (n≠n idp)
    ...                                     | inr _ | inl _ | inr n≠n = ⊥-elim (n≠n idp)
    ...                                     | inr _ | inl _ | inl _ =
      let Γ⊢χt = (sc χ Γ⊢A ⊢ (𝔻⊢(dim A)) (trT ⇒[χ Γ⊢A ] Γ⊢t:A) idp) in
      let A=⇒[γt] = ⇒[χ Γ⊢A ] >> (wk[]T (𝕊⊢⇒ (dim A)) Γ⊢χt ^) in
      ⇒= (A=⇒[γt] >> (wk[]T (wkT (𝕊⊢⇒ (dim A)) (𝔻⊢ (dim A))) (sc Γ⊢χt (𝕊⊢ (S (dim A))) (trT A=⇒[γt] Γ⊢u:A) idp) ^)) idp idp

    χ : ∀ {Γ} → Ty Γ → Σ ℕ λ n → Sub Γ (𝕊 n)
    χ (A , Γ⊢A) = dim A , (Pre-χ A , χ Γ⊢A ⊢)

    dim-Ty-n : ∀ {Γ} (n : ℕ) → (γ : Sub Γ (𝕊 n)) → dim (fst (Ty-n {Γ} (n , γ))) == n
    dim-Ty-n n (γ , Γ⊢γ:Sn) = dim[] (n⇒ n) γ >> (dim⇒ n)

    trS-sph : ∀ {Γ n m} → (p : n == m) → {γ : Sub Γ (𝕊 n)} → {δ : Sub Γ (𝕊 m)} → fst γ == fst δ → transport p γ == δ
    trS-sph {Γ} {n} {m} idp {γ} {δ} x = eqS {Γ} {𝕊 m} γ δ x

    lemma1 : ∀ t u γ n → (if n-src n ≡ S (n-src n) then u else (if n-src n ≡ n-src n then t else (Var (n-src n) [ γ ]Pre-Tm))) == t
    lemma1 t u γ n with eqdecℕ (n-src n) (S (n-src n))
    ... | inl n=Sn = ⊥-elim (n≠Sn _ (n=Sn))
    ... | inr _ with eqdecℕ (n-src n) (n-src n)
    ... | inl _ = idp
    ... | inr n≠n = ⊥-elim (n≠n idp)

    lemma2 : ∀ t u γ n → (if S (n-src n) ≡ S (n-src n) then u else (if S (n-src n) ≡ n-src n then t else (Var (S (n-src n)) [ γ ]Pre-Tm))) == u
    lemma2 t u γ n with eqdecℕ (S (n-src n)) (S (n-src n))
    ... | inl _ = idp
    ... | inr n≠n = ⊥-elim (n≠n idp)

    Pre-χTy-n : ∀ {Γ} (n : ℕ) → (γ : Sub Γ (𝕊 n)) → Pre-χ (fst (Ty-n {Γ} (n , γ))) == fst γ
    Pre-χTy-n O (.<> , (es _)) = idp
    Pre-χTy-n {Γ} (S n) (< < γ , _ ↦ t > , _ ↦ u > , (sc (sc Γ⊢γ:Sn _ Γ⊢t:A idp) _ Γ⊢u:A idp)) with eqdecℕ (n-src n) (S (n-src n)) | eqdecℕ (n-src n) (n-src n) | eqdecℕ (S (n-src n)) (S (n-src n))
    ...                                     | inl contra | _ | _ = ⊥-elim (n≠Sn _ contra)
    ...                                     | inr _ | inr n≠n | _ = ⊥-elim (n≠n idp)
    ...                                     | inr _ | inl _ | inr n≠n = ⊥-elim (n≠n idp)
    ...                                     | inr _ | inl _ | inl _ =
      let χTm-n = (sc Γ⊢γ:Sn (𝔻⊢ n) Γ⊢t:A idp) in
      <,>= (<,>= (ap Pre-χ (wk[]T (wkT (𝕊⊢⇒ n) (𝔻⊢ n)) (sc χTm-n (𝕊⊢ (S n)) Γ⊢u:A idp) >> wk[]T (𝕊⊢⇒ n) χTm-n) >> Pre-χTy-n {Γ} n (γ , Γ⊢γ:Sn))
           (ap n-src (dim[] (n⇒ n) _ >> (dim⇒ n))) (lemma1 t u γ n))
      (S= (ap n-src (dim[] (n⇒ n) _ >> (dim⇒ n))))
      (lemma2 t u γ n)

    χTy-n : ∀ {Γ} (n : ℕ) → (γ : Sub Γ (𝕊 n)) → χ {Γ} (Ty-n {Γ} (n , γ)) == (n , γ)
    χTy-n {Γ} n γ = Σ= (dim-Ty-n {Γ} n γ) (trS-sph {Γ} (dim-Ty-n {Γ} n γ) {snd (χ {Γ} (Ty-n {Γ} (n , γ)))} {γ} (Pre-χTy-n {Γ} n γ))

  Ty-classifier : ∀ Γ → is-equiv (Ty-n {Γ})
  is-equiv.g (Ty-classifier Γ) (A , Γ⊢A) = χ {Γ} (A , Γ⊢A)
  is-equiv.f-g (Ty-classifier Γ) (A , Γ⊢A) = Σ= (⇒[χ Γ⊢A ] ^) (has-all-paths-⊢T _ _)
  is-equiv.g-f (Ty-classifier Γ) (n , γ) = χTy-n {Γ} n γ
  is-equiv.adj (Ty-classifier Γ) (n , γ) = (is-prop-has-all-paths (is-set-Ty Γ _ _)) _ _

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


text:
{-# OPTIONS --cubical --no-import-sorts #-}

module NumberSecondAttempt where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ ℓ' ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Data.Unit.Base -- Unit
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)

open import NumberPostulates
open import NumberStructures ℝℓ ℝℓ'
open import NumberBundles    ℝℓ ℝℓ'
open import NumberInclusions ℝℓ ℝℓ'

module _ where
  open ROrderedField ℝOF
  data Number : Type (ℓ-max ℝℓ ℝℓ') where
    ℕ[_]   : (x : ℝCarrier) → Σ[ z ∈ ℕCarrier ] ℕ↪ℝ z ≡ x → Number
    ℤ[_]   : (x : ℝCarrier) → Σ[ z ∈ ℤCarrier ] ℤ↪ℝ z ≡ x → Number
    ℚ[_]   : (x : ℝCarrier) → Σ[ z ∈ ℚCarrier ] ℚ↪ℝ z ≡ x → Number
    ℝ[_]   : (x : ℝCarrier) → Unit → Number
    ℚ₀⁺[_] : (x : ℝCarrier) → (0f ≤ x) × (Σ[ z ∈ ℚCarrier ] ℚ↪ℝ z ≡ x) → Number
    ℚ⁺[_]  : (x : ℝCarrier) → (0f < x) × (Σ[ z ∈ ℚCarrier ] ℚ↪ℝ z ≡ x) → Number
    ℝ₀⁺[_] : (x : ℝCarrier) → 0f ≤ x → Number
    ℝ⁺[_]  : (x : ℝCarrier) → 0f < x → Number

  num : Number → ℝCarrier
  num (ℕ[   x ] _) = x
  num (ℤ[   x ] _) = x
  num (ℚ[   x ] _) = x
  num (ℝ[   x ] _) = x
  num (ℚ₀⁺[ x ] _) = x
  num (ℚ⁺[  x ] _) = x
  num (ℝ₀⁺[ x ] _) = x
  num (ℝ⁺[  x ] _) = x

  data NumberType : Type where
    Tℕ   : NumberType
    Tℤ   : NumberType
    Tℚ   : NumberType
    Tℝ   : NumberType
    Tℚ₀⁺ : NumberType
    Tℚ⁺  : NumberType
    Tℝ₀⁺ : NumberType
    Tℝ⁺  : NumberType

  totype : NumberType → Type (ℓ-max ℝℓ ℝℓ')
  totype Tℕ   = (x : ℝCarrier) → Lift {ℝℓ} {ℓ-max ℝℓ ℝℓ'} (Σ[ z ∈ ℕCarrier ] ℕ↪ℝ z ≡ x)
  totype Tℤ   = (x : ℝCarrier) → Lift {ℝℓ} {ℓ-max ℝℓ ℝℓ'} (Σ[ z ∈ ℤCarrier ] ℤ↪ℝ z ≡ x)
  totype Tℚ   = (x : ℝCarrier) → Lift {ℝℓ} {ℓ-max ℝℓ ℝℓ'} (Σ[ z ∈ ℚCarrier ] ℚ↪ℝ z ≡ x)
  totype Tℝ   = (x : ℝCarrier) → Lift {ℓ-zero} {ℓ-max ℝℓ ℝℓ'} (Unit)
  totype Tℚ₀⁺ = (x : ℝCarrier) → (0f ≤ x) × (Σ[ z ∈ ℚCarrier ] ℚ↪ℝ z ≡ x)
  totype Tℚ⁺  = (x : ℝCarrier) → (0f < x) × (Σ[ z ∈ ℚCarrier ] ℚ↪ℝ z ≡ x)
  totype Tℝ₀⁺ = (x : ℝCarrier) → 0f ≤ x
  totype Tℝ⁺  = (x : ℝCarrier) → 0f < x

  +-table : NumberType → NumberType → NumberType
  +-table x y = y

module GenericOperations where
  module ℕ' = ROrderedCommSemiring ℕOCSR
  module ℝ' = ROrderedField ℝOF
  module ℚ' = ROrderedField ℚOF

  module _ where
    open ℝ'
    postulate
      lemma1 : ∀ x y → 0f < x → 0f < y → 0f < (x + y)
      lemma2 : ∀ x y → 0f ≤ x → 0f ≤ y → 0f ≤ (x + y)

  _+_ : Number → Number → Number
  -- IsROrderedCommSemiringInclusion.preserves-+ ℕ↪ℝinc
  ℕ[ x ] (x₁ , p₁)        + ℕ[ y ] (y₁ , q₁)        =  ℕ[ x ℝ'.+ y ]
    (x₁ ℕ'.+ y₁ , transport (λ i → ℕ↪ℝ (x₁ ℕ'.+ y₁) ≡ (p₁ i ℝ'.+ q₁ i)) (IsROrderedCommSemiringInclusion.preserves-+ ℕ↪ℝinc x₁ y₁) )
  ℚ⁺[ x ] (p₂ , x₁ , p₁) + ℚ⁺[ y ] (q₂ , y₁ , q₁) = ℚ⁺[ x ℝ'.+ y ]
    (lemma1 x y p₂ q₂ , (x₁ ℚ'.+ y₁ , transport (λ i → ℚ↪ℝ (x₁ ℚ'.+ y₁) ≡ (p₁ i ℝ'.+ q₁ i)) (IsROrderedFieldInclusion.preserves-+ ℚ↪ℝinc x₁ y₁)))
  ℚ₀⁺[ x ] (p₂ , x₁ , p₁) + ℚ₀⁺[ y ] (q₂ , y₁ , q₁) = ℚ₀⁺[ x ℝ'.+ y ]
    (lemma2 x y p₂ q₂ , (x₁ ℚ'.+ y₁ , transport (λ i → ℚ↪ℝ (x₁ ℚ'.+ y₁) ≡ (p₁ i ℝ'.+ q₁ i)) (IsROrderedFieldInclusion.preserves-+ ℚ↪ℝinc x₁ y₁)))
  -- TODO: more cases
  -- default case
  x + y = ℝ[ num x ℝ'.+ num y ] tt

  instance
    0<ℚ⁺ : ∀{x p} → ℝ'.0f ℝ'.< num (ℚ⁺[ x ] p)
    0<ℚ⁺ {x} {0<x , p} = 0<x

ext: agda

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between orders
------------------------------------------------------------------------

-- See Data.Nat.Binary.Properties for examples of how this and similar
-- modules can be used to easily translate properties between types.

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

open import Function
open import Relation.Binary
open import Relation.Binary.Morphism

module Relation.Binary.Morphism.OrderMonomorphism
  {a b ℓ₁ ℓ₂ ℓ₃ ℓ₄} {A : Set a} {B : Set b}
  {_≈₁_ : Rel A ℓ₁} {_≈₂_ : Rel B ℓ₃}
  {_∼₁_ : Rel A ℓ₂} {_∼₂_ : Rel B ℓ₄}
  {⟦_⟧ : A → B}
  (isOrderMonomorphism : IsOrderMonomorphism _≈₁_ _≈₂_ _∼₁_ _∼₂_ ⟦_⟧)
  where

open import Data.Product using (map)
import Relation.Binary.Morphism.RelMonomorphism as RawRelation

open IsOrderMonomorphism isOrderMonomorphism

------------------------------------------------------------------------
-- Re-export equivalence proofs

module EqM = RawRelation Eq.isRelMonomorphism

open RawRelation isRelMonomorphism public

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

reflexive : _≈₂_ ⇒ _∼₂_ → _≈₁_ ⇒ _∼₁_
reflexive refl x≈y = cancel (refl (cong x≈y))

irrefl : Irreflexive _≈₂_ _∼₂_ → Irreflexive _≈₁_ _∼₁_
irrefl irrefl x≈y x∼y = irrefl (cong x≈y) (mono x∼y)

antisym : Antisymmetric _≈₂_ _∼₂_ → Antisymmetric _≈₁_ _∼₁_
antisym antisym x∼y y∼x = injective (antisym (mono x∼y) (mono y∼x))

compare : Trichotomous _≈₂_ _∼₂_ → Trichotomous _≈₁_ _∼₁_
compare compare x y with compare ⟦ x ⟧ ⟦ y ⟧
... | tri< a ¬b ¬c = tri< (cancel a) (¬b ∘ cong) (¬c ∘ mono)
... | tri≈ ¬a b ¬c = tri≈ (¬a ∘ mono) (injective b) (¬c ∘ mono)
... | tri> ¬a ¬b c = tri> (¬a ∘ mono) (¬b ∘ cong) (cancel c)

respˡ : _∼₂_ Respectsˡ _≈₂_ → _∼₁_ Respectsˡ _≈₁_
respˡ resp x≈y x∼z = cancel (resp (cong x≈y) (mono x∼z))

respʳ : _∼₂_ Respectsʳ _≈₂_ → _∼₁_ Respectsʳ _≈₁_
respʳ resp x≈y y∼z = cancel (resp (cong x≈y) (mono y∼z))

resp : _∼₂_ Respects₂ _≈₂_ → _∼₁_ Respects₂ _≈₁_
resp = map respʳ respˡ

------------------------------------------------------------------------
-- Structures

isPreorder : IsPreorder _≈₂_ _∼₂_ → IsPreorder _≈₁_ _∼₁_
isPreorder O = record
  { isEquivalence = EqM.isEquivalence O.isEquivalence
  ; reflexive     = reflexive O.reflexive
  ; trans         = trans O.trans
  } where module O = IsPreorder O

isPartialOrder : IsPartialOrder _≈₂_ _∼₂_ → IsPartialOrder _≈₁_ _∼₁_
isPartialOrder O = record
  { isPreorder = isPreorder O.isPreorder
  ; antisym    = antisym O.antisym
  } where module O = IsPartialOrder O

isTotalOrder : IsTotalOrder _≈₂_ _∼₂_ → IsTotalOrder _≈₁_ _∼₁_
isTotalOrder O = record
  { isPartialOrder = isPartialOrder O.isPartialOrder
  ; total          = total O.total
  } where module O = IsTotalOrder O

isDecTotalOrder : IsDecTotalOrder _≈₂_ _∼₂_ → IsDecTotalOrder _≈₁_ _∼₁_
isDecTotalOrder O = record
  { isTotalOrder = isTotalOrder O.isTotalOrder
  ; _≟_          = EqM.dec O._≟_
  ; _≤?_         = dec O._≤?_
  } where module O = IsDecTotalOrder O

isStrictPartialOrder : IsStrictPartialOrder _≈₂_ _∼₂_ →
                       IsStrictPartialOrder _≈₁_ _∼₁_
isStrictPartialOrder O = record
  { isEquivalence = EqM.isEquivalence O.isEquivalence
  ; irrefl        = irrefl O.irrefl
  ; trans         = trans O.trans
  ; <-resp-≈      = resp O.<-resp-≈
  } where module O = IsStrictPartialOrder O

isStrictTotalOrder : IsStrictTotalOrder _≈₂_ _∼₂_ →
                     IsStrictTotalOrder _≈₁_ _∼₁_
isStrictTotalOrder O = record
  { isEquivalence = EqM.isEquivalence O.isEquivalence
  ; trans         = trans O.trans
  ; compare       = compare O.compare
  } where module O = IsStrictTotalOrder O


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

module Definition.Typed.Consequences.Reduction where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Fundamental.Reducibility

open import Tools.Embedding
open import Tools.Product

-- Helper function where all reducible types can be reduced to WHNF.
whNorm′ : ∀ {A Γ l} ([A] : Γ ⊩⟨ l ⟩ A)
                → ∃ λ B → Whnf B × Γ ⊢ A :⇒*: B
whNorm′ (Uᵣ′ .⁰ 0<1 ⊢Γ) = U , Uₙ , idRed:*: (Uⱼ ⊢Γ)
whNorm′ (ℕᵣ D) = ℕ , ℕₙ , D
whNorm′ (ne′ K D neK K≡K) = K , ne neK , D
whNorm′ (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) = Π F ▹ G , Πₙ , D
whNorm′ (emb′ 0<1 [A]) = whNorm′ [A]

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

-- Helper function where reducible all terms can be reduced to WHNF.
whNormTerm′ : ∀ {a A Γ l} ([A] : Γ ⊩⟨ l ⟩ A) → Γ ⊩⟨ l ⟩ a ∷ A / [A]
                → ∃ λ b → Whnf b × Γ ⊢ a :⇒*: b ∷ A
whNormTerm′ (Uᵣ′ a b c) (Uₜ A d typeA A≡A [t]) = A , typeWhnf typeA , d
whNormTerm′ (ℕᵣ x) (ιx (ℕₜ n d n≡n prop)) =
  let natN = natural prop
  in  n , naturalWhnf natN , convRed:*: d (sym (subset* (red x)))
whNormTerm′ (ne′ K D neK K≡K) (ιx (neₜ k d (neNfₜ neK₁ ⊢k k≡k))) =
  k , ne neK₁ , convRed:*: d (sym (subset* (red D)))
whNormTerm′ (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Πₜ f d funcF f≡f [f] [f]₁) =
  f , functionWhnf funcF , convRed:*: d (sym (subset* (red D)))
whNormTerm′ (emb′ 0<1 [A]) (ιx [a]) = whNormTerm′ [A] [a]

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

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


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

open import LogicalFormulae
open import Groups.Definition
open import Groups.Abelian.Definition
open import Setoids.Setoids
open import Rings.Definition
open import Modules.Definition

module Modules.DirectSum {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+R_ : A → A → A} {_*R_ : A → A → A} (R : Ring S _+R_ _*R_) {m n o p : _} {M : Set m} {T : Setoid {m} {n} M} {_+_ : M → M → M} {G' : Group T _+_} {G : AbelianGroup G'} {_·1_ : A → M → M} {N : Set o} {U : Setoid {o} {p} N} {_+'_ : N → N → N} {H' : Group U _+'_} {H : AbelianGroup H'} {_·2_ : A → N → N} (M1 : Module R G _·1_) (M2 : Module R H _·2_) where

open import Groups.Abelian.DirectSum G H
open import Setoids.Product T U

directSumModule : Module R directSumAbGroup λ r mn → ((r ·1 (_&&_.fst mn)) ,, (r ·2 (_&&_.snd mn)))
Module.dotWellDefined directSumModule r=s t=u = productLift (Module.dotWellDefined M1 r=s (_&&_.fst t=u)) (Module.dotWellDefined M2 r=s (_&&_.snd t=u))
Module.dotDistributesLeft directSumModule = productLift (Module.dotDistributesLeft M1) (Module.dotDistributesLeft M2)
Module.dotDistributesRight directSumModule = productLift (Module.dotDistributesRight M1) (Module.dotDistributesRight M2)
Module.dotAssociative directSumModule = productLift (Module.dotAssociative M1) (Module.dotAssociative M2)
Module.dotIdentity directSumModule = productLift (Module.dotIdentity M1) (Module.dotIdentity M2)


text:
------------------------------------------------------------------------
-- There is a term without a corresponding syntactic type (given some
-- assumptions)
------------------------------------------------------------------------

import Level
open import Data.Universe

module README.DependentlyTyped.Term-without-type
  (Uni₀ : Universe Level.zero Level.zero)
  where

import Axiom.Extensionality.Propositional as E
open import Data.Product
open import Function renaming (const to k)
import README.DependentlyTyped.NBE as NBE; open NBE Uni₀
import README.DependentlyTyped.NormalForm as NF; open NF Uni₀
import README.DependentlyTyped.Term as Term; open Term Uni₀
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
open import Relation.Nullary using (¬_)

abstract

  -- There are no closed neutral terms.

  no-closed-neutral : ∀ {σ} → ¬ (ε ⊢ σ ⟨ ne ⟩)
  no-closed-neutral (var ())
  no-closed-neutral (t₁ · t₂) = no-closed-neutral t₁

  -- There are no closed normal forms of "atomic" type.

  no-closed-atomic-normal :
    ∀ {σ} → ε ⊢ σ atomic-type → ¬ (ε ⊢ σ ⟨ no ⟩)
  no-closed-atomic-normal ⋆  (ne ⋆  t) = no-closed-neutral t
  no-closed-atomic-normal el (ne el t) = no-closed-neutral t

  -- There are no closed terms of "atomic" type (assuming
  -- extensionality).

  no-closed-atomic :
    E.Extensionality Level.zero Level.zero →
    ∀ {σ} → ε ⊢ σ atomic-type → ¬ (ε ⊢ σ)
  no-closed-atomic ext atomic t =
    no-closed-atomic-normal atomic (normalise ext t)

  -- There are terms without syntactic types, assuming that U₀ is
  -- inhabited (and also extensionality).
  --
  -- One could avoid this situation by annotating lambdas with the
  -- (syntactic) type of their domain. I tried this, and found it to
  -- be awkward. One case of the function
  -- README.DependentlyTyped.NBE.Value.řeify returns a lambda, and I
  -- didn't find a way to synthesise the annotation without supplying
  -- syntactic types to V̌alue, řeify, řeflect, etc.

  term-without-type :
    E.Extensionality Level.zero Level.zero → U₀ →
    ∃₂ λ Γ σ → ∃ λ (t : Γ ⊢ σ) → ¬ (Γ ⊢ σ type)
  term-without-type ext u = (ε , (-, σ) , ƛ (var zero) , proof)
    where
    σ : IType ε (π el el)
    σ = k (U-π (U-el u) (k (U-el u)))

    proof : ∀ {σ} → ¬ (ε ⊢ π el el , σ type)
    proof (π (el t) (el t′)) = no-closed-atomic ext ⋆ t

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
module Scope where

{-

  So this goes through (we don't actually check scope). But what could really
  go wrong? This actually isn't captured by the main theorem, since we're type
  checking multiple definitions. Maybe it should be strengthened.

  Still nothing _bad_ happens here. Could we get some weird circular thing?
  Probably not. The main reason to check scope is to be able to state soundness
  in a reasonable way. So maybe we shouldn't make a big deal of scope.

-}

id : _ -> _
id x = x

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

z = id zero

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Coequalizers.Definition

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

open import Graphs.Definition

module Coequalizers.EdgeCoproduct where

module CoeqCoprodEquiv {i j k : ULevel} (V : Type i) (E₁ : Type j) (E₂ : Type k) ⦃ gph : Graph (E₁ ⊔ E₂) V ⦄ where

  instance
    gph1 : Graph E₁ V
    gph1 = record { π₀ = (Graph.π₀ gph) ∘ inl ; π₁ = (Graph.π₁ gph) ∘ inl }

  instance
    gph2 : Graph E₂ (V / E₁)
    gph2 = record { π₀ = c[_] ∘ (Graph.π₀ gph) ∘ inr ; π₁ = c[_] ∘ (Graph.π₁ gph) ∘ inr }

  edge-coproduct-expand : (V / (E₁ ⊔ E₂)) ≃ ((V / E₁) / E₂)
  edge-coproduct-expand = equiv f g f-g g-f
    where
      f : V / (E₁ ⊔ E₂) → (V / E₁) / E₂
      f = Coeq-rec (c[_] ∘ c[_]) λ { (inl x) → ap c[_] (quot x) ; (inr x) → quot x}

      g : (V / E₁) / E₂ → V / (E₁ ⊔ E₂)
      g = Coeq-rec (Coeq-rec c[_] (λ e → quot (inl e))) (λ e → quot (inr e))

      f-g : (x : (V / E₁) / E₂) → (f (g x) == x)
      f-g = Coeq-elim (λ x' → f (g x') == x') (Coeq-elim (λ x' → f (g (c[ x' ])) == c[ x' ]) (λ v → idp) (λ e → ↓-='-in (lemma1 e))) λ e → ↓-app=idf-in $
        idp ∙' quot e
          =⟨ ∙'-unit-l _ ⟩
        quot e
          =⟨ ! (Coeq-rec-β= _ _ _) ⟩
        ap f (quot (inr e))
          =⟨ ap (ap f) (! (Coeq-rec-β= _ _ _)) ⟩
        ap f (ap g (quot e))
          =⟨ ! (ap-∘ f g (quot e)) ⟩
        ap (f ∘ g) (quot e)
          =⟨ ! (∙-unit-r _) ⟩
        ap (f ∘ g) (quot e) ∙ idp
          =∎
        where
          lemma1 : (e : E₁) → idp ∙' ap (λ z → c[ z ]) (quot e) ==
                      ap (λ z → f (g c[ z ])) (quot e) ∙ idp
          lemma1 e =
            idp ∙' ap c[_] (quot e)
              =⟨ ∙'-unit-l _ ⟩
            ap c[_] (quot e)
              =⟨ ! (Coeq-rec-β= _ _ _) ⟩
            ap f (quot (inl e))
              =⟨ ap (ap f) (! (Coeq-rec-β= _ _ _)) ⟩
            ap f (ap (Coeq-rec c[_] (λ e → quot (inl e))) (quot e))
              =⟨ idp ⟩
            ap f (ap (g ∘ c[_]) (quot e))
              =⟨ ! (ap-∘ f (g ∘ c[_]) (quot e)) ⟩
            ap (f ∘ g ∘ c[_]) (quot e)
              =⟨ ! (∙-unit-r _) ⟩
            ap (f ∘ g ∘ c[_]) (quot e) ∙ idp
              =∎

      g-f : (x : V / (E₁ ⊔ E₂)) → (g (f x) == x)
      g-f = Coeq-elim (λ x → g (f x) == x) (λ v → idp) (λ { (inl e) → ↓-app=idf-in (! (lemma1 e)) ; (inr e) → ↓-app=idf-in (! (lemma2 e))})
        where
          lemma1 : (e : E₁) → ap (λ z → g (f z)) (quot (inl e)) ∙ idp == idp ∙' quot (inl e)
          lemma1 e =
            ap (g ∘ f) (quot (inl e)) ∙ idp
              =⟨ ∙-unit-r _ ⟩
            ap (g ∘ f) (quot (inl e))
               =⟨ ap-∘ g f (quot (inl e)) ⟩
            ap g (ap f (quot (inl e)))
              =⟨ ap (ap g) (Coeq-rec-β= _ _ _) ⟩
            ap g (ap c[_] (quot e))
              =⟨ ! (ap-∘ g c[_] (quot e)) ⟩
            ap (g ∘ c[_]) (quot e)
              =⟨ idp ⟩
            ap (Coeq-rec c[_] (λ e' → quot (inl e'))) (quot e)
              =⟨ Coeq-rec-β= _ _ _ ⟩
            quot (inl e)
              =⟨ ! (∙'-unit-l _) ⟩
            idp ∙' quot (inl e)
              =∎

          lemma2 : (e : E₂) → ap (λ z → g (f z)) (quot (inr e)) ∙ idp == idp ∙' quot (inr e)
          lemma2 e =
            ap (g ∘ f) (quot (inr e)) ∙ idp
              =⟨ ∙-unit-r _ ⟩
            ap (g ∘ f) (quot (inr e))
              =⟨ ap-∘ g f (quot (inr e)) ⟩
            ap g (ap f (quot (inr e)))
              =⟨ ap (ap g) (Coeq-rec-β= _ _ _) ⟩
            ap g (quot e)
              =⟨ Coeq-rec-β= _ _ _ ⟩
            quot (inr e)
              =⟨ ! (∙'-unit-l _) ⟩
            idp ∙' quot (inr e)
              =∎

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


text:
module RMonads where

open import Library
open import Categories
open import Functors

record RMonad {a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}(J : Fun C D) :
  Set (a ⊔ b ⊔ c ⊔ d) where
  constructor rmonad
  open Cat
  open Fun
  field T    : Obj C → Obj D
        η    : ∀{X} → Hom D (OMap J  X) (T X)
        bind : ∀{X Y} → Hom D (OMap J X) (T Y) → Hom D (T X) (T Y)
        law1 : ∀{X} → bind (η {X}) ≅ iden D {T X}
        law2 : ∀{X Y}{f : Hom D (OMap J X) (T Y)} → comp D (bind f) η ≅ f
        law3 : ∀{X Y Z}
               {f : Hom D (OMap J X) (T Y)}{g : Hom D (OMap J Y) (T Z)} →
               bind (comp D (bind g) f) ≅ comp D (bind g) (bind f)

open import Functors

TFun : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{J : Fun C D} →
       RMonad J → Fun C D
TFun {C = C}{D}{J} M = let open RMonad M; open Cat; open Fun in record {
  OMap  = T;
  HMap  = bind ∘ comp D η ∘ HMap J;
  fid   =
    proof
    bind (comp D η (HMap J (iden C)))
    ≅⟨ cong (bind ∘ comp D η) (fid J) ⟩
    bind (comp D η (iden D))
    ≅⟨ cong bind (idr D) ⟩
    bind η
    ≅⟨ law1 ⟩
    iden D
    ∎;
  fcomp = λ{_ _ _ f g} →
    proof
    bind (comp D η (HMap J (comp C f g)))
    ≅⟨ cong (bind ∘ comp D η) (fcomp J) ⟩
    bind (comp D η (comp D (HMap J f) (HMap J g)))
    ≅⟨ cong bind (sym (ass D)) ⟩
    bind (comp D (comp D η (HMap J f)) (HMap J g))
    ≅⟨ cong (λ f → bind (comp D f (HMap J g))) (sym law2) ⟩
    bind (comp D (comp D (bind (comp D η (HMap J f))) η) (HMap J g))
    ≅⟨ cong bind (ass D) ⟩
    bind (comp D (bind (comp D η (HMap J f))) (comp D η (HMap J g)))
    ≅⟨ law3 ⟩
    comp D (bind (comp D η (HMap J f))) (bind (comp D η (HMap J g)))
    ∎}

-- any functor is a rel monad over itself
trivRM : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}(J : Fun C D) → RMonad J
trivRM {D = D} J = rmonad OMap (iden D) id refl (idr D) refl
  where open Fun J; open Cat

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
{-# OPTIONS --safe --without-K #-}
module Data.Fin.Subset.Properties.Dec where

open import Data.Nat as ℕ
open import Data.Fin as Fin
open import Data.Empty using (⊥-elim)
open import Data.Fin.Subset
open import Data.Fin.Subset.Dec
open import Data.Fin.Subset.Properties using (⊆⊤; p⊆p∪q; q⊆p∪q ; p∩q⊆p ; p∩q⊆q ; ⊆-poset)
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Unary renaming (Decidable to Decidable₁) using ()
open import Data.Vec
open import Function using (_∘_)
open import Function.Equivalence using (_⇔_ ; equivalence)
open import Relation.Nullary.Negation using (¬?)

subset¬⊆∁subset : ∀ {n}{p} {P : Fin n → Set p}(P? : Decidable₁ P) → subset (¬? ∘ P?) ⊆ ∁ (subset P?)
subset¬⊆∁subset {zero} P? ()
subset¬⊆∁subset {suc n} P? x∈s with P? (# 0)
subset¬⊆∁subset {suc n} P? here | no ¬p0 = here
subset¬⊆∁subset {suc n} P? (there x∈s) | no ¬p0 = there (subset¬⊆∁subset (P? ∘ suc) x∈s)
subset¬⊆∁subset {suc n} P? (there x∈s) | yes p0 = there (subset¬⊆∁subset (P? ∘ suc) x∈s)

∁subset⊆subset¬ : ∀ {n}{p}{P : Fin n → Set p}(P? : Decidable₁ P) →  ∁ (subset P?) ⊆ subset (¬? ∘ P?)
∁subset⊆subset¬  {zero} P? ()
∁subset⊆subset¬ {suc n} P? x∈s with P? (# 0)
∁subset⊆subset¬ {suc n} P? here | no ¬p0 = here
∁subset⊆subset¬ {suc n} P? (there x∈s) | yes p0 = there (∁subset⊆subset¬ (P? ∘ suc) x∈s)
∁subset⊆subset¬ {suc n} P? (there x∈s) | no ¬p0 = there (∁subset⊆subset¬ (P? ∘ suc) x∈s)

subset¬≡∁subset  : ∀ {n}{p}{P : Fin n → Set p}(P? : Decidable₁ P) → subset (¬? ∘ P?) ≡ ∁ (subset P?)
subset¬≡∁subset {n} P? = ⊆-antisym (subset¬⊆∁subset P?) (∁subset⊆subset¬ P?)
  where
    open Poset (⊆-poset n) renaming (antisym to ⊆-antisym) using ()

∈subset⁺ : ∀ {n}{p}{P : Fin n → Set p}(P? : Decidable₁ P){x} → P x → x ∈ subset P?
∈subset⁺ {zero} P? {()} Px
∈subset⁺ {suc n} P? {x} Px with P? (# 0)
∈subset⁺ {suc n} P? {zero} Px | yes p0 = here
∈subset⁺ {suc n} P? {suc x} Px | yes p0 = there (∈subset⁺ (P? ∘ suc) Px)
∈subset⁺ {suc n} P? {zero} Px | no ¬p0 = ⊥-elim (¬p0 Px)
∈subset⁺ {suc n} P? {suc x} Px | no ¬p0 = there (∈subset⁺ (P? ∘ suc) Px)

∈subset⁻ : ∀ {n}{p} {P : Fin n → Set p}(P? : Decidable₁ P){x} → x ∈ subset P? → P x
∈subset⁻ {zero} P? {()} x∈s
∈subset⁻ {suc n} P? {x} x∈s with P? (# 0)
∈subset⁻ {suc n} P? {zero} here | yes p0 = p0
∈subset⁻ {suc n} P? {suc x} (there x∈s) | yes p0 = ∈subset⁻ (P? ∘ suc) x∈s
∈subset⁻ {suc n} P? {.(suc _)} (there x∈s) | no ¬p0 = ∈subset⁻ (P? ∘ suc) x∈s

⇔∈subset : ∀ {n}{p}{P : Fin n → Set p}(P? : Decidable₁ P) {x} → x ∈ subset P? ⇔ P x
⇔∈subset P? = equivalence (∈subset⁻ P?) (∈subset⁺ P?)

∈∁subset⁺ : ∀ {n}{p}{P : Fin n → Set p}(P? : Decidable₁ P){x} → ¬ P x → x ∈ ∁ (subset P?)
∈∁subset⁺ P?  = subset¬⊆∁subset P? ∘ (∈subset⁺ (¬? ∘ P? ))
∈∁subset⁻ : ∀ {n}{p}{P : Fin n → Set p}(P? : Decidable₁ P){x} → x ∈ ∁ (subset P?) → ¬ P x
∈∁subset⁻ P? = ∈subset⁻ (¬? ∘ P?) ∘ ∁subset⊆subset¬ P?

⇔∈∁subset : ∀ {n}{p}{P : Fin n → Set p}(P? : Decidable₁ P) {x} → x ∈ ∁ (subset P?) ⇔ (¬ P x)
⇔∈∁subset P? = equivalence (∈∁subset⁻ P?) (∈∁subset⁺ P?)

max_stars_repo_name: tizmd/agda-finitary

max_issues_repo_name: tizmd/agda-finitary

max_forks_repo_name: tizmd/agda-finitary


text:
{-# OPTIONS --safe --without-K #-}
module Generics.Prelude where

open import Function.Base     public
open import Data.Product      public hiding (map; uncurry; uncurry′; curry′)
open import Level             public using (Setω; Level; _⊔_; Lift; lift)
                                     renaming (zero to lzero; suc to lsuc)

open import Relation.Binary.PropositionalEquality public
  hiding ([_]; Extensionality; ∀-extensionality)
open import Data.Nat.Base        public using (ℕ; zero; suc; _+_)
                                        renaming (_∸_ to _-_)
open import Data.Unit            public using (⊤; tt)
open import Data.Empty           public using (⊥)
open import Data.List            public using (List; []; _∷_)
open import Data.Vec.Base        public using (Vec; []; _∷_; map; lookup)
open import Data.Fin.Base as Fin public using (Fin; zero; suc)
open import Axiom.Extensionality.Propositional public
open import Data.String using (String)

open import Reflection                      public
  hiding (var; return; _>>=_; _>>_; assocˡ; assocʳ; visibility; relevance; module Arg)
import Reflection.Argument
module Arg = Reflection.Argument
open import Reflection.Argument.Information public using (ArgInfo; arg-info; visibility)
                                                   renaming (modality to getModality)
open import Reflection.Argument.Modality    public using (Modality; modality)
open import Reflection.Argument.Relevance   public using (Relevance; relevant; irrelevant)
open import Reflection.Argument.Visibility  public using (Visibility; visible; hidden; instance′)

private variable
  m n   : ℕ
  k     : Fin n
  l l'  : Level
  A B   : Set l

record Irr (A : Set l) : Set l where
  constructor irrv
  field
    .unirr : A
open Irr public

<_>_ : Relevance → Set l → Set l
< relevant   > A = A
< irrelevant > A = Irr A

relevance : ArgInfo → Relevance
relevance = Reflection.Argument.Modality.relevance ∘ getModality

-- withAI : ArgInfo → Term → Term
-- withAI i t with relevance i
-- ... | relevant   = t
-- ... | irrelevant = con (quote irrv) (vArg t ∷ [])
-- macro
--   Π<> : ((n , i) : String × ArgInfo) → Term → Term → Term → TC ⊤
--   Π<> (n , ai) S′ (Term.var k []) =
--     unify (pi (arg ai S′) (abs n (Term.var (suc k) (vArg (withAI ai (Term.var 0 [])) ∷ []))))
--   Π<> (n , ai) S′ _ hole = typeError (strErr "" ∷ [])

-- TODO: do this with reflection, using names
-- TODO: deal with quantities
Π<_> : ((a , i) : String × ArgInfo) (A : Set l) → (< relevance i > A → Set l') → Set (l ⊔ l')
Π< _ , arg-info visible   (modality relevant q)   > A B = (x : A) → B x
Π< _ , arg-info visible   (modality irrelevant q) > A B = .(x : A) → B (irrv x)
Π< _ , arg-info hidden    (modality relevant q)   > A B = {x : A} → B x
Π< _ , arg-info hidden    (modality irrelevant q) > A B = .{x : A} → B (irrv x)
Π< _ , arg-info instance′ (modality relevant q)   > A B = {{x : A}} → B x
Π< _ , arg-info instance′ (modality irrelevant q) > A B = .{{x : A}} → B (irrv x)

_→<_>_ : Set l → String × ArgInfo → Set l' → Set (l ⊔ l')
A →< i > B = Π< i > A λ _ → B

fun<_> : (ai@(a , i) : String × ArgInfo) {A : Set l} {B : < relevance i > A → Set l'}
       → (f : (x : < relevance i > A) → B x) → Π< ai > A B
fun< _ , arg-info visible   (modality relevant q)   > f x     = f x
fun< _ , arg-info visible   (modality irrelevant q) > f x     = f (irrv x)
fun< _ , arg-info hidden    (modality relevant q)   > f {x}   = f x
fun< _ , arg-info hidden    (modality irrelevant q) > f {x}   = f (irrv x)
fun< _ , arg-info instance′ (modality relevant q)   > f {{x}} = f x
fun< _ , arg-info instance′ (modality irrelevant q) > f {{x}} = f (irrv x)

app<_> : (ai@(a , i) : String × ArgInfo) {A : Set l} {B : < relevance i > A → Set l'}
       → (f : Π< ai > A B) → (x : < relevance i > A) → B x
app< _ , arg-info visible   (modality relevant q)   > f x        = f x
app< _ , arg-info visible   (modality irrelevant q) > f (irrv x) = f x
app< _ , arg-info hidden    (modality relevant q)   > f x        = f {x}
app< _ , arg-info hidden    (modality irrelevant q) > f (irrv x) = f {x}
app< _ , arg-info instance′ (modality relevant q)   > f x        = f {{x}}
app< _ , arg-info instance′ (modality irrelevant q) > f (irrv x) = f {{x}}

-- Instead of the definitions from Function.Nary.NonDependent in the
-- standard library, we use a *functional* representation of vectors
-- of levels and types. This makes it much easier to work with
-- operations like lookup and tabulate, at the cost of losing certain
-- eta laws for nil and cons (see the comment for `uncurryₙ` below).

Levels : ℕ → Set
Levels n = Fin n → Level

private variable ls ls' : Levels n

[]l : Levels 0
[]l ()

_∷l_ : Level → Levels n → Levels (suc n)
(l ∷l ls) zero = l
(l ∷l ls) (suc k) = ls k

headl : Levels (suc n) → Level
headl ls = ls zero

taill : Levels (suc n) → Levels n
taill ls = ls ∘ suc

_++l_ : Levels m → Levels n → Levels (m + n)
_++l_ {zero} ls ls' = ls'
_++l_ {suc m} ls ls' zero = headl ls
_++l_ {suc m} ls ls' (suc x) = (taill ls ++l ls') x

⨆ : Levels n → Level
⨆ {zero} ls = lzero
⨆ {suc n} ls = ls zero ⊔ ⨆ (ls ∘ suc)

Sets : (ls : Levels n) → Setω
Sets {n} ls = (k : Fin n) → Set (ls k)

private variable As Bs : Sets ls

[]S : {ls : Levels 0} → Sets ls
[]S ()

_∷S_ : Set (headl ls) → Sets (taill ls) → Sets ls
(A ∷S As) zero    = A
(A ∷S As) (suc k) = As k

headS : Sets ls → Set (headl ls)
headS As = As zero

tailS : Sets ls → Sets (taill ls)
tailS As k = As (suc k)

_++S_ : Sets ls → Sets ls' → Sets (ls ++l ls')
_++S_ {zero}  As Bs = Bs
_++S_ {suc m} As Bs zero = headS As
_++S_ {suc m} As Bs (suc k) = (tailS As ++S Bs) k

Els : (As : Sets ls) → Setω
Els {n} As = (k : Fin n) → As k

private variable xs : Els As

[]El : {As : Sets {zero} ls} → Els As
[]El ()

_∷El_ : headS As → Els (tailS As) → Els As
(x ∷El xs) zero    = x
(x ∷El xs) (suc k) = xs k

headEl : Els As → headS As
headEl xs = xs zero

tailEl : Els As → Els (tailS As)
tailEl xs k = xs (suc k)

_++El_ : Els As → Els Bs → Els (As ++S Bs)
_++El_ {zero} xs ys = ys
_++El_ {suc m} xs ys zero = headEl xs
_++El_ {suc m} xs ys (suc k) = (tailEl xs ++El ys) k

++El-proj₁ : Els (As ++S Bs) → Els As
++El-proj₁ xs zero    = xs zero
++El-proj₁ xs (suc k) = ++El-proj₁ (tailEl xs) k

++El-proj₂ : Els (As ++S Bs) → Els Bs
++El-proj₂ {zero}  xs k = xs k
++El-proj₂ {suc m} xs k = ++El-proj₂ (tailEl xs) k

Pis : (As : Sets ls) (B : Els As → Set l) → Set (⨆ ls ⊔ l)
Pis {zero}  As B = B []El
Pis {suc n} As B = (x : As zero) → Pis (tailS As) (λ xs → B (x ∷El xs))

Arrows : (As : Sets ls) (B : Set l) → Set (⨆ ls ⊔ l)
Arrows As B = Pis As (λ _ → B)

curryₙ : {B : Els As → Set l} → ((xs : Els As) → B xs) → Pis As B
curryₙ {zero}  f = f []El
curryₙ {suc n} f = λ x → curryₙ (λ xs → f (x ∷El xs))

-- It is not possible to define the dependent version of uncurryₙ, as
-- it requires the laws that `xs = []El` for all `xs : Els {zero} As`
-- and `xs = headEl xs ∷El tailEl xs` for all `xs : Els {suc n} As`,
-- which do not hold definitionally and require funExt to prove.
uncurryₙ : Arrows As B → Els As → B
uncurryₙ {zero}  f _  = f
uncurryₙ {suc n} f xs = uncurryₙ (f (headEl xs)) (tailEl xs)

------------------------------------
-- Some utilities to work with Setω

-- TODO: move this somewhere else
-- TODO: consistent naming

record ⊤ω : Setω where
  instance constructor tt

data ⊥ω : Setω where

⊥⇒⊥ω : ⊥ → ⊥ω
⊥⇒⊥ω ()

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

ttω : ⊤ω
ttω = tt

record Liftω (A : Set l) : Setω where
  constructor liftω
  field lower : A

instance
  liftω-inst : {A : Set l} → ⦃ A ⦄ → Liftω A
  liftω-inst ⦃ x ⦄ = liftω x

record _×ω_ (A B : Setω) : Setω where
  constructor _,_
  field fst : A
        snd : B

_ω,ω_ : {A B : Setω} → A → B → A ×ω B
_ω,ω_ = _,_

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

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

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

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

reflω : {A : Setω} {x : A} → x ≡ω x
reflω = refl

transω : {A : Setω} {x y z : A}
       → x ≡ω y → y ≡ω z → x ≡ω z
transω refl refl = refl

symω : {A : Setω} {x y : A} → x ≡ω y → y ≡ω x
symω refl = refl

instance
  ×ω-inst : ∀ {A B} → ⦃ A ⦄ → ⦃ B ⦄ → A ×ω B
  ×ω-inst ⦃ x ⦄ ⦃ y ⦄ = x , y

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

data Decω (A : Setω) : Setω where
  yesω : A       → Decω A
  noω  : (A → ⊥) → Decω A

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
open import Prelude
open import Nat
open import dynamics-core

module binders-disjoint-checks where
  -- these are fairly mechanical lemmas that show that the
  -- judgementally-defined binders-disjoint is really a type-directed
  -- function

  -- numbers
  lem-bdσ-num : ∀{σ n} → binders-disjoint-σ σ (N n)
  lem-bdσ-num {σ = Id Γ} = BDσId
  lem-bdσ-num {σ = Subst d y σ} = BDσSubst BDNum lem-bdσ-num UBNum

  lem-bd-num : ∀{d n} → binders-disjoint d (N n)
  lem-bd-num {d = N x} = BDNum
  lem-bd-num {d = d ·+ d₁} = BDPlus lem-bd-num lem-bd-num
  lem-bd-num {d = X x} = BDVar
  lem-bd-num {d = ·λ x ·[ x₁ ] d} = BDLam lem-bd-num UBNum
  lem-bd-num {d = d ∘ d₁} = BDAp lem-bd-num lem-bd-num
  lem-bd-num {d = inl x d} = BDInl lem-bd-num
  lem-bd-num {d = inr x d} = BDInr lem-bd-num
  lem-bd-num {d = case d x d₁ x₁ d₂} = BDCase lem-bd-num UBNum lem-bd-num UBNum lem-bd-num
  lem-bd-num {d = ⟨ d , d₁ ⟩} = BDPair lem-bd-num lem-bd-num
  lem-bd-num {d = fst d} = BDFst lem-bd-num
  lem-bd-num {d = snd d} = BDSnd lem-bd-num
  lem-bd-num {d = ⦇-⦈⟨ u , σ ⟩} = BDHole lem-bdσ-num
  lem-bd-num {d = ⦇⌜ d ⌟⦈⟨ u , σ ⟩} = BDNEHole lem-bdσ-num lem-bd-num
  lem-bd-num {d = d ⟨ x ⇒ x₁ ⟩} = BDCast lem-bd-num
  lem-bd-num {d = d ⟨ x ⇒⦇-⦈⇏ x₁ ⟩} = BDFailedCast lem-bd-num

  -- plus
  lem-bdσ-into-plus : ∀{σ d1 d2} →
                      binders-disjoint-σ σ d1 →
                      binders-disjoint-σ σ d2 →
                      binders-disjoint-σ σ (d1 ·+ d2)
  lem-bdσ-into-plus BDσId BDσId = BDσId
  lem-bdσ-into-plus (BDσSubst x bd1 x₁) (BDσSubst x₂ bd2 x₃) =
    BDσSubst (BDPlus x x₂) (lem-bdσ-into-plus bd1 bd2) (UBPlus x₁ x₃)

  lem-bdσ-plus : ∀{σ d1 d2} →
                 binders-disjoint-σ σ (d1 ·+ d2) →
                 binders-disjoint-σ σ d1 × binders-disjoint-σ σ d2
  lem-bdσ-plus BDσId = BDσId , BDσId
  lem-bdσ-plus (BDσSubst (BDPlus x x₁) bd (UBPlus ub ub₁))
    with lem-bdσ-plus bd
  ... | dis1 , dis2 = BDσSubst x dis1 ub , BDσSubst x₁ dis2 ub₁

  lem-bd-plus : ∀{d d1 d2} →
                binders-disjoint d (d1 ·+ d2) →
                binders-disjoint d d1 × binders-disjoint d d2
  lem-bd-plus BDNum = BDNum , BDNum
  lem-bd-plus (BDPlus bd bd')
    with lem-bd-plus bd | lem-bd-plus bd'
  ... | bd₁ , bd₂ | bd₁' , bd₂' = BDPlus bd₁ bd₁' , BDPlus bd₂ bd₂'
  lem-bd-plus BDVar = BDVar , BDVar
  lem-bd-plus (BDLam bd (UBPlus x x₁))
    with lem-bd-plus bd
  ... | bd₁ , bd₂  = BDLam bd₁ x , BDLam bd₂ x₁
  lem-bd-plus (BDAp bd bd')
    with lem-bd-plus bd | lem-bd-plus bd'
  ... | bd₁ , bd₂ | bd₁' , bd₂' = BDAp bd₁ bd₁' , BDAp bd₂ bd₂'
  lem-bd-plus (BDInl bd)
    with lem-bd-plus bd
  ... | bd₁ , bd₂ = BDInl bd₁ , BDInl bd₂
  lem-bd-plus (BDInr bd)
    with lem-bd-plus bd
  ... | bd' , bdσ' = BDInr bd' , BDInr bdσ'
  lem-bd-plus (BDCase bd (UBPlus x x₂) bd₁ (UBPlus x₁ x₃) bd₂)
    with lem-bd-plus bd | lem-bd-plus bd₁ | lem-bd-plus bd₂
  ... | bd' , bd'' | bd₁' , bd₁'' | bd₂' , bd₂'' = BDCase bd' x bd₁' x₁ bd₂' , BDCase bd'' x₂ bd₁'' x₃ bd₂''
  lem-bd-plus (BDPair bd bd₁)
    with lem-bd-plus bd | lem-bd-plus bd₁
  ... | bd' , bd'' | bd₁' , bd₁''  = BDPair bd' bd₁' , BDPair bd'' bd₁''
  lem-bd-plus (BDFst bd)
    with lem-bd-plus bd
  ... | bd' , bdσ' = BDFst bd' , BDFst bdσ'
  lem-bd-plus (BDSnd bd)
    with lem-bd-plus bd
  ... | bd' , bdσ' = BDSnd bd' , BDSnd bdσ'
  lem-bd-plus (BDHole x)
    with lem-bdσ-plus x
  ... | bdσ₁ , bdσ₂ = BDHole bdσ₁ , BDHole bdσ₂
  lem-bd-plus (BDNEHole x bd)
    with lem-bdσ-plus x | lem-bd-plus bd
  ... | bdσ₁ , bdσ₂ | bd₁ , bd₂ = BDNEHole bdσ₁ bd₁ , BDNEHole bdσ₂ bd₂
  lem-bd-plus (BDCast bd)
    with lem-bd-plus bd
  ... | bd₁ , bd₂ = BDCast bd₁ , BDCast bd₂
  lem-bd-plus (BDFailedCast bd)
    with lem-bd-plus bd
  ... | bd₁ , bd₂ = BDFailedCast bd₁ , BDFailedCast bd₂

  -- var
  lem-bdσ-var : ∀{σ x} → binders-disjoint-σ σ (X x)
  lem-bdσ-var {σ = Id Γ} = BDσId
  lem-bdσ-var {σ = Subst d y σ} = BDσSubst BDVar lem-bdσ-var UBVar

  lem-bd-var : ∀{d x} → binders-disjoint d (X x)
  lem-bd-var {d = N x} = BDNum
  lem-bd-var {d = d ·+ d₁} = BDPlus lem-bd-var lem-bd-var
  lem-bd-var {d = X x} = BDVar
  lem-bd-var {d = ·λ x ·[ x₁ ] d} = BDLam lem-bd-var UBVar
  lem-bd-var {d = d ∘ d₁} = BDAp lem-bd-var lem-bd-var
  lem-bd-var {d = inl x d} = BDInl lem-bd-var
  lem-bd-var {d = inr x d} = BDInr lem-bd-var
  lem-bd-var {d = case d x d₁ x₁ d₂} = BDCase lem-bd-var UBVar lem-bd-var UBVar lem-bd-var
  lem-bd-var {d = ⟨ d , d₁ ⟩} = BDPair lem-bd-var lem-bd-var
  lem-bd-var {d = fst d} = BDFst lem-bd-var
  lem-bd-var {d = snd d} = BDSnd lem-bd-var
  lem-bd-var {d = ⦇-⦈⟨ u , σ ⟩} = BDHole lem-bdσ-var
  lem-bd-var {d = ⦇⌜ d ⌟⦈⟨ u , σ ⟩} = BDNEHole lem-bdσ-var lem-bd-var
  lem-bd-var {d = d ⟨ x ⇒ x₁ ⟩} = BDCast lem-bd-var
  lem-bd-var {d = d ⟨ x ⇒⦇-⦈⇏ x₁ ⟩} = BDFailedCast lem-bd-var

  -- lambda
  lem-bdσ-into-lam : ∀{x τ d σ} →
                     binders-disjoint-σ σ d →
                     unbound-in-σ x σ →
                     binders-disjoint-σ σ (·λ x ·[ τ ] d)
  lem-bdσ-into-lam BDσId UBσId = BDσId
  lem-bdσ-into-lam (BDσSubst x bd x₁) (UBσSubst x₂ ub x₃) =
    BDσSubst (BDLam x x₂) (lem-bdσ-into-lam bd ub) (UBLam2 (flip x₃) x₁)

  lem-bdσ-lam : ∀{σ x τ d} →
                binders-disjoint-σ σ (·λ x ·[ τ ] d) →
                binders-disjoint-σ σ d × unbound-in-σ x σ
  lem-bdσ-lam BDσId = BDσId , UBσId
  lem-bdσ-lam (BDσSubst (BDLam x₁ x) bd (UBLam2 x₂ ub))
    with lem-bdσ-lam bd
  ... | bdσ , ub' = (BDσSubst x₁ bdσ ub) , (UBσSubst x ub' (flip x₂))

  lem-bd-lam : ∀{d1 x τ1 d} →
               binders-disjoint d1 (·λ x ·[ τ1 ] d) →
               binders-disjoint d1 d × unbound-in x d1
  lem-bd-lam BDNum = BDNum , UBNum
  lem-bd-lam (BDPlus bd bd₁)
    with lem-bd-lam bd | lem-bd-lam bd₁
  ... | bd' , ub | bd₁' , ub₁ = BDPlus bd' bd₁' , UBPlus ub ub₁
  lem-bd-lam BDVar = BDVar , UBVar
  lem-bd-lam (BDLam bd (UBLam2 x x₁))
    with lem-bd-lam bd
  ... | bd' , ub = BDLam bd' x₁ , UBLam2 (flip x) ub
  lem-bd-lam (BDAp bd bd₁)
    with lem-bd-lam bd | lem-bd-lam bd₁
  ... | bd' , ub | bd₁' , ub₁ = BDAp bd' bd₁' , UBAp ub ub₁
  lem-bd-lam (BDInl bd)
    with lem-bd-lam bd
  ... | bd' , ub = BDInl bd' , UBInl ub
  lem-bd-lam (BDInr bd)
    with lem-bd-lam bd
  ... | bd' , ub = BDInr bd' , UBInr ub
  lem-bd-lam (BDCase bd (UBLam2 x x₁) bd₁ (UBLam2 x₂ x₃) bd₂)
    with lem-bd-lam bd | lem-bd-lam bd₁ | lem-bd-lam bd₂
  ... | bd' , ub | bd₁' , ub1 | bd₂' , ub2 = (BDCase bd' x₁ bd₁' x₃ bd₂') , (UBCase ub (flip x) ub1 (flip x₂) ub2)
  lem-bd-lam (BDPair bd bd₁)
    with lem-bd-lam bd | lem-bd-lam bd₁
  ... | bd' , ub | bd₁' , ub1 = BDPair bd' bd₁' , UBPair ub ub1
  lem-bd-lam (BDFst bd)
     with lem-bd-lam bd
  ... | bd' , ub = BDFst bd' , UBFst ub
  lem-bd-lam (BDSnd bd)
     with lem-bd-lam bd
  ... | bd' , ub = BDSnd bd' , UBSnd ub
  lem-bd-lam (BDHole x)
    with lem-bdσ-lam x
  ... | bdσ , ubσ = BDHole bdσ , UBHole ubσ
  lem-bd-lam (BDNEHole x bd)
    with lem-bd-lam bd | lem-bdσ-lam x
  ... | bd' , ub | bdσ , ubσ = BDNEHole bdσ bd' , UBNEHole ubσ ub
  lem-bd-lam (BDCast bd)
    with lem-bd-lam bd
  ... | bd' , ub = BDCast bd' , UBCast ub
  lem-bd-lam (BDFailedCast bd)
    with lem-bd-lam bd
  ... | bd' , ub = BDFailedCast bd' , UBFailedCast ub

  -- application
  lem-bdσ-into-ap : ∀{σ d1 d2} →
                    binders-disjoint-σ σ d1 →
                    binders-disjoint-σ σ d2 →
                    binders-disjoint-σ σ (d1 ∘ d2)
  lem-bdσ-into-ap BDσId BDσId = BDσId
  lem-bdσ-into-ap (BDσSubst x bd1 x₁) (BDσSubst x₂ bd2 x₃) =
    BDσSubst (BDAp x x₂) (lem-bdσ-into-ap bd1 bd2) (UBAp x₁ x₃)

  lem-bdσ-ap : ∀{σ d1 d2} →
               binders-disjoint-σ σ (d1 ∘ d2) →
               binders-disjoint-σ σ d1 × binders-disjoint-σ σ d2
  lem-bdσ-ap BDσId = BDσId , BDσId
  lem-bdσ-ap (BDσSubst (BDAp x x₁) bd (UBAp ub ub₁))
    with lem-bdσ-ap bd
  ... | dis1 , dis2 = BDσSubst x dis1 ub , BDσSubst x₁ dis2 ub₁

  lem-bd-ap : ∀{d d1 d2} →
              binders-disjoint d (d1 ∘ d2) →
              binders-disjoint d d1 × binders-disjoint d d2
  lem-bd-ap BDNum = BDNum , BDNum
  lem-bd-ap (BDPlus bd bd')
    with lem-bd-ap bd | lem-bd-ap bd'
  ... | bd₁ , bd₂ | bd₁' , bd₂' = BDPlus bd₁ bd₁' , BDPlus bd₂ bd₂'
  lem-bd-ap BDVar = BDVar , BDVar
  lem-bd-ap (BDLam bd (UBAp x x₁))
    with lem-bd-ap bd
  ... | bd₁ , bd₂  = BDLam bd₁ x , BDLam bd₂ x₁
  lem-bd-ap (BDAp bd bd')
    with lem-bd-ap bd | lem-bd-ap bd'
  ... | bd₁ , bd₂ | bd₁' , bd₂' = BDAp bd₁ bd₁' , BDAp bd₂ bd₂'
  lem-bd-ap (BDInl bd)
    with lem-bd-ap bd
  ... | bd₁ , bd₂ = BDInl bd₁ , BDInl bd₂
  lem-bd-ap (BDInr bd)
    with lem-bd-ap bd
  ... | bd' , bdσ' = BDInr bd' , BDInr bdσ'
  lem-bd-ap (BDCase bd (UBAp x x₂) bd₁ (UBAp x₁ x₃) bd₂)
    with lem-bd-ap bd | lem-bd-ap bd₁ | lem-bd-ap bd₂
  ... | bd' , bd'' | bd₁' , bd₁'' | bd₂' , bd₂'' = BDCase bd' x bd₁' x₁ bd₂' , BDCase bd'' x₂ bd₁'' x₃ bd₂''
  lem-bd-ap (BDPair bd bd₁)
    with lem-bd-ap bd | lem-bd-ap bd₁
  ... | bd' , bd'' | bd₁' , bd₁'' = BDPair bd' bd₁' , BDPair bd'' bd₁''
  lem-bd-ap (BDFst bd)
    with lem-bd-ap bd
  ... | bd' , bdσ' = BDFst bd' , BDFst bdσ'
  lem-bd-ap (BDSnd bd)
    with lem-bd-ap bd
  ... | bd' , bdσ' = BDSnd bd' , BDSnd bdσ'
  lem-bd-ap (BDHole x)
    with lem-bdσ-ap x
  ... | bdσ₁ , bdσ₂ = BDHole bdσ₁ , BDHole bdσ₂
  lem-bd-ap (BDNEHole x bd)
    with lem-bdσ-ap x | lem-bd-ap bd
  ... | bdσ₁ , bdσ₂ | bd₁ , bd₂ = BDNEHole bdσ₁ bd₁ , BDNEHole bdσ₂ bd₂
  lem-bd-ap (BDCast bd)
    with lem-bd-ap bd
  ... | bd₁ , bd₂ = BDCast bd₁ , BDCast bd₂
  lem-bd-ap (BDFailedCast bd)
    with lem-bd-ap bd
  ... | bd₁ , bd₂ = BDFailedCast bd₁ , BDFailedCast bd₂

  -- inl
  lem-bdσ-into-inl : ∀{σ d τ} →
                     binders-disjoint-σ σ d →
                     binders-disjoint-σ σ (inl τ d)
  lem-bdσ-into-inl BDσId = BDσId
  lem-bdσ-into-inl (BDσSubst x bd x₁) = BDσSubst (BDInl x) (lem-bdσ-into-inl bd) (UBInl x₁)

  lem-bdσ-inl : ∀{σ τ d} →
                binders-disjoint-σ σ (inl τ d) →
                binders-disjoint-σ σ d
  lem-bdσ-inl BDσId = BDσId
  lem-bdσ-inl (BDσSubst (BDInl x) bd (UBInl ub)) = BDσSubst x (lem-bdσ-inl bd) ub

  lem-bd-inl : ∀{d τ d1} →
               binders-disjoint d (inl τ d1) →
               binders-disjoint d d1
  lem-bd-inl BDNum = BDNum
  lem-bd-inl (BDPlus bd bd₁) = BDPlus (lem-bd-inl bd) (lem-bd-inl bd₁)
  lem-bd-inl BDVar = BDVar
  lem-bd-inl (BDLam bd (UBInl x)) = BDLam (lem-bd-inl bd) x
  lem-bd-inl (BDAp bd bd₁) = BDAp (lem-bd-inl bd) (lem-bd-inl bd₁)
  lem-bd-inl (BDInl bd) = BDInl (lem-bd-inl bd)
  lem-bd-inl (BDInr bd) = BDInr (lem-bd-inl bd)
  lem-bd-inl (BDCase bd (UBInl x) bd₁ (UBInl x₁) bd₂) = BDCase (lem-bd-inl bd) x (lem-bd-inl bd₁) x₁ (lem-bd-inl bd₂)
  lem-bd-inl (BDPair bd bd₁) = BDPair (lem-bd-inl bd) (lem-bd-inl bd₁)
  lem-bd-inl (BDFst bd) = BDFst (lem-bd-inl bd)
  lem-bd-inl (BDSnd bd) = BDSnd (lem-bd-inl bd)
  lem-bd-inl (BDHole x) = BDHole (lem-bdσ-inl x)
  lem-bd-inl (BDNEHole x bd) = BDNEHole (lem-bdσ-inl x) (lem-bd-inl bd)
  lem-bd-inl (BDCast bd) = BDCast (lem-bd-inl bd)
  lem-bd-inl (BDFailedCast bd) = BDFailedCast (lem-bd-inl bd)

  -- inr
  lem-bdσ-into-inr : ∀{σ d τ} →
                     binders-disjoint-σ σ d →
                     binders-disjoint-σ σ (inr τ d)
  lem-bdσ-into-inr BDσId = BDσId
  lem-bdσ-into-inr (BDσSubst x bd x₁) = BDσSubst (BDInr x) (lem-bdσ-into-inr bd) (UBInr x₁)

  lem-bdσ-inr : ∀{σ τ d} →
                binders-disjoint-σ σ (inr τ d) →
                binders-disjoint-σ σ d
  lem-bdσ-inr BDσId = BDσId
  lem-bdσ-inr (BDσSubst (BDInr x) bd (UBInr ub)) = BDσSubst x (lem-bdσ-inr bd) ub

  lem-bd-inr : ∀{d τ d1} →
               binders-disjoint d (inr τ d1) →
               binders-disjoint d d1
  lem-bd-inr BDNum = BDNum
  lem-bd-inr (BDPlus bd bd₁) = BDPlus (lem-bd-inr bd) (lem-bd-inr bd₁)
  lem-bd-inr BDVar = BDVar
  lem-bd-inr (BDLam bd (UBInr x)) = BDLam (lem-bd-inr bd) x
  lem-bd-inr (BDAp bd bd₁) = BDAp (lem-bd-inr bd) (lem-bd-inr bd₁)
  lem-bd-inr (BDInl bd) = BDInl (lem-bd-inr bd)
  lem-bd-inr (BDInr bd) = BDInr (lem-bd-inr bd)
  lem-bd-inr (BDCase bd (UBInr x) bd₁ (UBInr x₁) bd₂) = BDCase (lem-bd-inr bd) x (lem-bd-inr bd₁) x₁ (lem-bd-inr bd₂)
  lem-bd-inr (BDPair bd bd₁) = BDPair (lem-bd-inr bd) (lem-bd-inr bd₁)
  lem-bd-inr (BDFst bd) = BDFst (lem-bd-inr bd)
  lem-bd-inr (BDSnd bd) = BDSnd (lem-bd-inr bd)
  lem-bd-inr (BDHole x) = BDHole (lem-bdσ-inr x)
  lem-bd-inr (BDNEHole x bd) = BDNEHole (lem-bdσ-inr x) (lem-bd-inr bd)
  lem-bd-inr (BDCast bd) = BDCast (lem-bd-inr bd)
  lem-bd-inr (BDFailedCast bd) = BDFailedCast (lem-bd-inr bd)

  -- case
  lem-bdσ-into-case : ∀{σ d x d1 y d2} →
                      binders-disjoint-σ σ d →
                      unbound-in-σ x σ →
                      binders-disjoint-σ σ d1 →
                      unbound-in-σ y σ →
                      binders-disjoint-σ σ d2 →
                      binders-disjoint-σ σ (case d x d1 y d2)
  lem-bdσ-into-case BDσId ubx bdσ1 uby bdσ2 = BDσId
  lem-bdσ-into-case (BDσSubst x bdσ x₁) (UBσSubst x₂ ubx x₃) (BDσSubst x₆ bdσ1 x₇) (UBσSubst x₄ uby x₅) (BDσSubst x₈ bdσ2 x₉) =
    BDσSubst (BDCase x x₂ x₆ x₄ x₈) (lem-bdσ-into-case bdσ ubx bdσ1 uby bdσ2) (UBCase x₁ (flip x₃) x₇ (flip x₅) x₉)

  lem-bdσ-case : ∀{σ d x d1 y d2} →
                 binders-disjoint-σ σ (case d x d1 y d2) →
                 (binders-disjoint-σ σ d) ×
                 (unbound-in-σ x σ) ×
                 (binders-disjoint-σ σ d1) ×
                 (unbound-in-σ y σ) ×
                 (binders-disjoint-σ σ d2)
  lem-bdσ-case BDσId = BDσId , UBσId , BDσId , UBσId , BDσId
  lem-bdσ-case (BDσSubst (BDCase x x₁ x₂ x₃ x₄) bd (UBCase x₅ x₆ x₇ x₈ x₉))
    with lem-bdσ-case bd
  ... | bdd , ubx , bdd1 , uby , bdd2 = BDσSubst x bdd x₅ , UBσSubst x₁ ubx (flip x₆) , BDσSubst x₂ bdd1 x₇ , UBσSubst x₃ uby (flip x₈) , BDσSubst x₄ bdd2 x₉

  lem-bd-case : ∀{d x d1 y d2 d3} →
                binders-disjoint d3 (case d x d1 y d2) →
                (binders-disjoint d3 d) ×
                (unbound-in x d3) ×
                (binders-disjoint d3 d1) ×
                (unbound-in y d3) ×
                (binders-disjoint d3 d2)
  lem-bd-case BDNum = BDNum , UBNum , BDNum , UBNum , BDNum
  lem-bd-case (BDPlus bd bd₁)
    with lem-bd-case bd | lem-bd-case bd₁
  ... | bdd , ubx , bdd1 , uby , bdd2 | bdd' , ubx' , bdd1' , uby' , bdd2' = BDPlus bdd bdd' , UBPlus ubx ubx' , BDPlus bdd1 bdd1' , UBPlus uby uby' , BDPlus bdd2 bdd2'
  lem-bd-case BDVar = BDVar , UBVar , BDVar , UBVar , BDVar
  lem-bd-case (BDLam bd (UBCase x x₁ x₂ x₃ x₄))
    with lem-bd-case bd
  ... | bdd , ubx , bdd1 , uby , bdd2  = BDLam bdd x , UBLam2 (flip x₁) ubx , BDLam bdd1 x₂ , UBLam2 (flip x₃) uby , BDLam bdd2 x₄
  lem-bd-case (BDAp bd bd₁)
    with lem-bd-case bd | lem-bd-case bd₁
  ... | bdd , ubx , bdd1 , uby , bdd2 | bdd' , ubx' , bdd1' , uby' , bdd2' = BDAp bdd bdd' , UBAp ubx ubx' , BDAp bdd1 bdd1' , UBAp uby uby' , BDAp bdd2 bdd2'
  lem-bd-case (BDInl bd)
    with lem-bd-case bd
  ... | bdd , ubx , bdd1 , uby , bdd2 = BDInl bdd , UBInl ubx , BDInl bdd1 , UBInl uby , BDInl bdd2
  lem-bd-case (BDInr bd)
    with lem-bd-case bd
  ... | bdd , ubx , bdd1 , uby , bdd2 = BDInr bdd , UBInr ubx , BDInr bdd1 , UBInr uby , BDInr bdd2
  lem-bd-case (BDCase bd (UBCase x x₁ x₂ x₃ x₄) bd₁ (UBCase x₅ x₆ x₇ x₈ x₉) bd₂)
    with lem-bd-case bd | lem-bd-case bd₁ | lem-bd-case bd₂
  ... | bdd , ubx , bdd1 , uby , bdd2 | bdd' , ubx' , bdd1' , uby' , bdd2' | bdd'' , ubx'' , bdd1'' , uby'' , bdd2'' = BDCase bdd x bdd' x₅ bdd'' , UBCase ubx (flip x₁) ubx' (flip x₆) ubx'' , BDCase bdd1 x₂ bdd1' x₇ bdd1'' , UBCase uby (flip x₃) uby' (flip x₈) uby'' , BDCase bdd2 x₄ bdd2' x₉ bdd2''
  lem-bd-case (BDPair bd bd₁)
    with lem-bd-case bd | lem-bd-case bd₁
  ... | bdd , ubx , bdd1 , uby , bdd2 | bdd' , ubx' , bdd1' , uby' , bdd2' = BDPair bdd bdd' , UBPair ubx ubx' , BDPair bdd1 bdd1' , UBPair uby uby' , BDPair bdd2 bdd2'
  lem-bd-case (BDFst bd)
    with lem-bd-case bd
  ... | bdd , ubx , bdd1 , uby , bdd2 = BDFst bdd , UBFst ubx , BDFst bdd1 , UBFst uby , BDFst bdd2
  lem-bd-case (BDSnd bd)
    with lem-bd-case bd
  ... | bdd , ubx , bdd1 , uby , bdd2 = BDSnd bdd , UBSnd ubx , BDSnd bdd1 , UBSnd uby , BDSnd bdd2
  lem-bd-case (BDHole x)
    with lem-bdσ-case x
  ... | bdd , ubx , bdd1 , uby , bdd2 = BDHole bdd , UBHole ubx , BDHole bdd1 , UBHole uby , BDHole bdd2
  lem-bd-case (BDNEHole x bd)
    with lem-bd-case bd | lem-bdσ-case x
  ... | bdd , ubx , bdd1 , uby , bdd2 | bddσ , ubxσ , bdd1σ , ubyσ , bdd2σ = BDNEHole bddσ bdd , UBNEHole ubxσ ubx , BDNEHole bdd1σ bdd1 , UBNEHole ubyσ uby , BDNEHole bdd2σ bdd2
  lem-bd-case (BDCast bd)
    with lem-bd-case bd
  ... | bdd , ubx , bdd1 , uby , bdd2 = BDCast bdd , UBCast ubx , BDCast bdd1 , UBCast uby , BDCast bdd2
  lem-bd-case (BDFailedCast bd)
    with lem-bd-case bd
  ... | bdd , ubx , bdd1 , uby , bdd2 = BDFailedCast bdd , UBFailedCast ubx , BDFailedCast bdd1 , UBFailedCast uby , BDFailedCast bdd2

  -- pairs
  lem-bdσ-into-pair : ∀{σ d1 d2} →
                      binders-disjoint-σ σ d1 →
                      binders-disjoint-σ σ d2 →
                      binders-disjoint-σ σ ⟨ d1 , d2 ⟩
  lem-bdσ-into-pair BDσId BDσId = BDσId
  lem-bdσ-into-pair (BDσSubst x bdσ1 x₁) (BDσSubst x₂ bdσ2 x₃) = BDσSubst (BDPair x x₂) (lem-bdσ-into-pair bdσ1 bdσ2) (UBPair x₁ x₃)

  lem-bdσ-pair : ∀{σ d1 d2} →
                 binders-disjoint-σ σ ⟨ d1 , d2 ⟩ →
                 (binders-disjoint-σ σ d1) × (binders-disjoint-σ σ d2)
  lem-bdσ-pair BDσId = BDσId , BDσId
  lem-bdσ-pair (BDσSubst (BDPair x x₁) bdσ (UBPair x₂ x₃))
    with lem-bdσ-pair bdσ
  ... | bdσ1 , bdσ2 = BDσSubst x bdσ1 x₂ , BDσSubst x₁ bdσ2 x₃

  lem-bd-pair : ∀{d d1 d2} →
                binders-disjoint d ⟨ d1 , d2 ⟩ →
                (binders-disjoint d d1) × (binders-disjoint d d2)
  lem-bd-pair BDNum = BDNum , BDNum
  lem-bd-pair (BDPlus bd bd₁)
    with lem-bd-pair bd | lem-bd-pair bd₁
  ... | bd' , bd'' | bd₁' , bd₁'' = BDPlus bd' bd₁' , BDPlus bd'' bd₁''
  lem-bd-pair BDVar = BDVar , BDVar
  lem-bd-pair (BDLam bd (UBPair x x₁))
    with lem-bd-pair bd
  ... | bd' , bd'' = BDLam bd' x , BDLam bd'' x₁
  lem-bd-pair (BDAp bd bd₁)
    with lem-bd-pair bd | lem-bd-pair bd₁
  ... | bd' , bd'' | bd₁' , bd₁'' = BDAp bd' bd₁' , BDAp bd'' bd₁''
  lem-bd-pair (BDInl bd)
    with lem-bd-pair bd
  ... | bd' , bd'' = BDInl bd' , BDInl bd''
  lem-bd-pair (BDInr bd)
    with lem-bd-pair bd
  ... | bd' , bd'' = BDInr bd' , BDInr bd''
  lem-bd-pair (BDCase bd (UBPair x x₁) bd₁ (UBPair x₂ x₃) bd₂)
     with lem-bd-pair bd | lem-bd-pair bd₁ | lem-bd-pair bd₂
  ... | bd' , bd'' | bd₁' , bd₁'' | bd₂' , bd₂'' = BDCase bd' x bd₁' x₂ bd₂' , BDCase bd'' x₁ bd₁'' x₃ bd₂''
  lem-bd-pair (BDPair bd bd₁)
    with lem-bd-pair bd | lem-bd-pair bd₁
  ... | bd' , bd'' | bd₁' , bd₁'' = BDPair bd' bd₁' , BDPair bd'' bd₁''
  lem-bd-pair (BDFst bd)
    with lem-bd-pair bd
  ... | bd' , bd'' = BDFst bd' , BDFst bd''
  lem-bd-pair (BDSnd bd)
    with lem-bd-pair bd
  ... | bd' , bd'' = BDSnd bd' , BDSnd bd''
  lem-bd-pair (BDHole x)
    with lem-bdσ-pair x
  ... | bdσ' , bdσ'' = BDHole bdσ' , BDHole bdσ''
  lem-bd-pair (BDNEHole x bd)
    with lem-bdσ-pair x | lem-bd-pair bd
  ... | bdσ' , bdσ'' | bd' , bd'' = BDNEHole bdσ' bd' , BDNEHole bdσ'' bd''
  lem-bd-pair (BDCast bd)
    with lem-bd-pair bd
  ... | bd' , bd'' = BDCast bd' , BDCast bd''
  lem-bd-pair (BDFailedCast bd)
    with lem-bd-pair bd
  ... | bd' , bd'' = BDFailedCast bd' , BDFailedCast bd''

  -- fst
  lem-bdσ-into-fst : ∀{σ d} →
                     binders-disjoint-σ σ d →
                     binders-disjoint-σ σ (fst d)
  lem-bdσ-into-fst BDσId = BDσId
  lem-bdσ-into-fst (BDσSubst x bdσ x₁) = BDσSubst (BDFst x) (lem-bdσ-into-fst bdσ) (UBFst x₁)

  lem-bdσ-fst : ∀{σ d} →
                binders-disjoint-σ σ (fst d) →
                binders-disjoint-σ σ d
  lem-bdσ-fst BDσId = BDσId
  lem-bdσ-fst (BDσSubst (BDFst x) bdσ (UBFst x₁)) = BDσSubst x (lem-bdσ-fst bdσ) x₁

  lem-bd-fst : ∀{d d1} →
               binders-disjoint d (fst d1) →
               binders-disjoint d d1
  lem-bd-fst BDNum = BDNum
  lem-bd-fst (BDPlus bd bd₁) = BDPlus (lem-bd-fst bd) (lem-bd-fst bd₁)
  lem-bd-fst BDVar = BDVar
  lem-bd-fst (BDLam bd (UBFst x)) = BDLam (lem-bd-fst bd) x
  lem-bd-fst (BDAp bd bd₁) = BDAp (lem-bd-fst bd) (lem-bd-fst bd₁)
  lem-bd-fst (BDInl bd) = BDInl (lem-bd-fst bd)
  lem-bd-fst (BDInr bd) = BDInr (lem-bd-fst bd)
  lem-bd-fst (BDCase bd (UBFst x) bd₁ (UBFst x₁) bd₂) = BDCase (lem-bd-fst bd) x (lem-bd-fst bd₁) x₁ (lem-bd-fst bd₂)
  lem-bd-fst (BDPair bd bd₁) = BDPair (lem-bd-fst bd) (lem-bd-fst bd₁)
  lem-bd-fst (BDFst bd) = BDFst (lem-bd-fst bd)
  lem-bd-fst (BDSnd bd) = BDSnd (lem-bd-fst bd)
  lem-bd-fst (BDHole x) = BDHole (lem-bdσ-fst x)
  lem-bd-fst (BDNEHole x bd) = BDNEHole (lem-bdσ-fst x) (lem-bd-fst bd)
  lem-bd-fst (BDCast bd) = BDCast (lem-bd-fst bd)
  lem-bd-fst (BDFailedCast bd) = BDFailedCast (lem-bd-fst bd)

  -- snd
  lem-bdσ-into-snd : ∀{σ d} →
                     binders-disjoint-σ σ d →
                     binders-disjoint-σ σ (snd d)
  lem-bdσ-into-snd BDσId = BDσId
  lem-bdσ-into-snd (BDσSubst x bdσ x₁) = BDσSubst (BDSnd x) (lem-bdσ-into-snd bdσ) (UBSnd x₁)

  lem-bdσ-snd : ∀{σ d} →
                binders-disjoint-σ σ (snd d) →
                binders-disjoint-σ σ d
  lem-bdσ-snd BDσId = BDσId
  lem-bdσ-snd (BDσSubst (BDSnd x) bdσ (UBSnd x₁)) = BDσSubst x (lem-bdσ-snd bdσ) x₁

  lem-bd-snd : ∀{d d1} →
               binders-disjoint d (snd d1) →
               binders-disjoint d d1
  lem-bd-snd BDNum = BDNum
  lem-bd-snd (BDPlus bd bd₁) = BDPlus (lem-bd-snd bd) (lem-bd-snd bd₁)
  lem-bd-snd BDVar = BDVar
  lem-bd-snd (BDLam bd (UBSnd x)) = BDLam (lem-bd-snd bd) x
  lem-bd-snd (BDAp bd bd₁) = BDAp (lem-bd-snd bd) (lem-bd-snd bd₁)
  lem-bd-snd (BDInl bd) = BDInl (lem-bd-snd bd)
  lem-bd-snd (BDInr bd) = BDInr (lem-bd-snd bd)
  lem-bd-snd (BDCase bd (UBSnd x) bd₁ (UBSnd x₁) bd₂) = BDCase (lem-bd-snd bd) x (lem-bd-snd bd₁) x₁ (lem-bd-snd bd₂)
  lem-bd-snd (BDPair bd bd₁) = BDPair (lem-bd-snd bd) (lem-bd-snd bd₁)
  lem-bd-snd (BDFst bd) = BDFst (lem-bd-snd bd)
  lem-bd-snd (BDSnd bd) = BDSnd (lem-bd-snd bd)
  lem-bd-snd (BDHole x) = BDHole (lem-bdσ-snd x)
  lem-bd-snd (BDNEHole x bd) = BDNEHole (lem-bdσ-snd x) (lem-bd-snd bd)
  lem-bd-snd (BDCast bd) = BDCast (lem-bd-snd bd)
  lem-bd-snd (BDFailedCast bd) = BDFailedCast (lem-bd-snd bd)

  -- cast
  lem-bdσ-into-cast : ∀{σ d τ1 τ2} →
                      binders-disjoint-σ σ d →
                      binders-disjoint-σ σ (d ⟨ τ1 ⇒ τ2 ⟩)
  lem-bdσ-into-cast BDσId = BDσId
  lem-bdσ-into-cast (BDσSubst x bd x₁) = BDσSubst (BDCast x) (lem-bdσ-into-cast bd) (UBCast x₁)

  lem-bdσ-cast : ∀{σ d τ1 τ2} →
                 binders-disjoint-σ σ (d ⟨ τ1 ⇒ τ2 ⟩) →
                 binders-disjoint-σ σ d
  lem-bdσ-cast BDσId = BDσId
  lem-bdσ-cast (BDσSubst (BDCast x) bd (UBCast ub)) = BDσSubst x (lem-bdσ-cast bd) ub

  lem-bd-cast : ∀{d1 d τ1 τ2} →
                binders-disjoint d1 (d ⟨ τ1 ⇒ τ2 ⟩) →
                binders-disjoint d1 d
  lem-bd-cast BDNum = BDNum
  lem-bd-cast (BDPlus bd bd₁) = BDPlus (lem-bd-cast bd) (lem-bd-cast bd₁)
  lem-bd-cast BDVar = BDVar
  lem-bd-cast (BDLam bd (UBCast x₁)) = BDLam (lem-bd-cast bd) x₁
  lem-bd-cast (BDHole x) = BDHole (lem-bdσ-cast x)
  lem-bd-cast (BDNEHole x bd) = BDNEHole (lem-bdσ-cast x) (lem-bd-cast bd)
  lem-bd-cast (BDAp bd bd₁) = BDAp (lem-bd-cast bd) (lem-bd-cast bd₁)
  lem-bd-cast (BDInl bd) = BDInl (lem-bd-cast bd)
  lem-bd-cast (BDInr bd) = BDInr (lem-bd-cast bd)
  lem-bd-cast (BDCase bd (UBCast x) bd₁ (UBCast x₁) bd₂) = BDCase (lem-bd-cast bd) x (lem-bd-cast bd₁) x₁ (lem-bd-cast bd₂)
  lem-bd-cast (BDPair bd bd₁) = BDPair (lem-bd-cast bd) (lem-bd-cast bd₁)
  lem-bd-cast (BDFst bd) = BDFst (lem-bd-cast bd)
  lem-bd-cast (BDSnd bd) = BDSnd (lem-bd-cast bd)
  lem-bd-cast (BDCast bd) = BDCast (lem-bd-cast bd)
  lem-bd-cast (BDFailedCast bd) = BDFailedCast (lem-bd-cast bd)

  -- failed cast
  lem-bdσ-into-failedcast : ∀{σ d τ1 τ2} →
                            binders-disjoint-σ σ d →
                            binders-disjoint-σ σ (d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩)
  lem-bdσ-into-failedcast BDσId = BDσId
  lem-bdσ-into-failedcast (BDσSubst x bd x₁) =
    BDσSubst (BDFailedCast x) (lem-bdσ-into-failedcast bd) (UBFailedCast x₁)

  lem-bdσ-failedcast : ∀{σ d τ1 τ2} →
                       binders-disjoint-σ σ (d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩) →
                       binders-disjoint-σ σ d
  lem-bdσ-failedcast BDσId = BDσId
  lem-bdσ-failedcast (BDσSubst (BDFailedCast x) bd (UBFailedCast ub)) = BDσSubst x (lem-bdσ-failedcast bd) ub

  lem-bd-failedcast : ∀{d1 d τ1 τ2} → binders-disjoint d1 (d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩) → binders-disjoint d1 d
  lem-bd-failedcast BDNum = BDNum
  lem-bd-failedcast (BDPlus bd bd₁) = BDPlus (lem-bd-failedcast bd) (lem-bd-failedcast bd₁)
  lem-bd-failedcast BDVar = BDVar
  lem-bd-failedcast (BDLam bd (UBFailedCast x₁)) = BDLam (lem-bd-failedcast bd) x₁
  lem-bd-failedcast (BDHole x) = BDHole (lem-bdσ-failedcast x)
  lem-bd-failedcast (BDNEHole x bd) = BDNEHole (lem-bdσ-failedcast x) (lem-bd-failedcast bd)
  lem-bd-failedcast (BDAp bd bd₁) = BDAp (lem-bd-failedcast bd) (lem-bd-failedcast bd₁)
  lem-bd-failedcast (BDInl bd) = BDInl (lem-bd-failedcast bd)
  lem-bd-failedcast (BDInr bd) = BDInr (lem-bd-failedcast bd)
  lem-bd-failedcast (BDCase bd (UBFailedCast x) bd₁ (UBFailedCast x₁) bd₂) =
    BDCase (lem-bd-failedcast bd) x (lem-bd-failedcast bd₁) x₁ (lem-bd-failedcast bd₂)
  lem-bd-failedcast (BDPair bd bd₁) = BDPair (lem-bd-failedcast bd) (lem-bd-failedcast bd₁)
  lem-bd-failedcast (BDFst bd) = BDFst (lem-bd-failedcast bd)
  lem-bd-failedcast (BDSnd bd) = BDSnd (lem-bd-failedcast bd)
  lem-bd-failedcast (BDCast bd) = BDCast (lem-bd-failedcast bd)
  lem-bd-failedcast (BDFailedCast bd) = BDFailedCast (lem-bd-failedcast bd)

  -- holes
  mutual
    -- For terms already holding an env, the equivalent lemms needs a judgement
    -- that two envs are disjoint
    data binders-disjoint-σs : env → env → Set where
      BDσsId    : ∀{Γ σ} → binders-disjoint-σs σ (Id Γ)
      BDσsSubst : ∀{d1 σ' y σ} →
                 binders-disjoint-σ σ' d1 →
                 binders-disjoint-σs σ σ' →
                 unbound-in-σ y σ' →
                 binders-disjoint-σs σ' (Subst d1 y σ)

    lem-bdσs-sym : ∀{σ σ'} →
                   binders-disjoint-σs σ σ' →
                   binders-disjoint-σs σ' σ
    lem-bdσs-sym {σ = Id Γ} bd = BDσsId
    lem-bdσs-sym {σ = Subst d y σ} BDσsId = BDσsSubst BDσId BDσsId UBσId
    lem-bdσs-sym {σ = Subst d y σ} (BDσsSubst (BDσSubst x x₂ x₃) (BDσsSubst x₆ bd x₇) (UBσSubst x₁ x₄ x₅)) = BDσsSubst (BDσSubst (binders-disjoint-sym x) x₆ x₁) (BDσsSubst x₂ (lem-bdσs-sym bd) x₄) (UBσSubst x₃ x₇ (flip x₅))

    lem-bdσ-into-hole : ∀{σ σ' u} →
                        binders-disjoint-σs σ σ' →
                        binders-disjoint-σ σ (⦇-⦈⟨ u , σ' ⟩)
    lem-bdσ-into-hole {σ = Id Γ} bd = BDσId
    lem-bdσ-into-hole {σ = Subst d y σ} BDσsId = BDσSubst (BDHole BDσId) (lem-bdσ-into-hole BDσsId) (UBHole UBσId)
    lem-bdσ-into-hole {σ = Subst d y σ} (BDσsSubst (BDσSubst x x₁ x₂) (BDσsSubst x₆ bd x₇) (UBσSubst x₃ x₄ x₅)) = BDσSubst (BDHole (BDσSubst (binders-disjoint-sym x) x₆ x₃)) (lem-bdσ-into-hole (BDσsSubst x₁ (lem-bdσs-sym bd) x₄)) (UBHole (UBσSubst x₂ x₇ (flip x₅)))

    lem-bdσ-hole : ∀{σ u σ'} →
                   binders-disjoint-σ σ (⦇-⦈⟨ u , σ' ⟩) →
                   binders-disjoint-σs σ σ'
    lem-bdσ-hole {σ = Id Γ} bd = lem-bdσs-sym BDσsId
    lem-bdσ-hole {σ = Subst d y σ} (BDσSubst (BDHole x) bd (UBHole x₁)) = lem-bdσs-sym (BDσsSubst x (lem-bdσ-hole bd) x₁)

    lem-bd-hole : ∀{d u σ} →
                  binders-disjoint d (⦇-⦈⟨ u , σ ⟩) →
                  binders-disjoint-σ σ d
    lem-bd-hole {σ = Id Γ} bd = BDσId
    lem-bd-hole {σ = Subst d y σ} BDNum = BDσSubst BDNum lem-bdσ-num UBNum
    lem-bd-hole {σ = Subst d y σ} (BDPlus bd bd₁)
      with lem-bd-hole bd | lem-bd-hole bd₁
    ... | BDσSubst x bdσ ub | BDσSubst x₁ bdσ₁ ub₁ = BDσSubst (BDPlus x x₁) (lem-bdσ-into-plus bdσ bdσ₁) (UBPlus ub ub₁)

    lem-bd-hole {σ = Subst d y σ} BDVar = BDσSubst BDVar lem-bdσ-var UBVar
    lem-bd-hole {σ = Subst d y σ} (BDLam bd (UBHole (UBσSubst x x₁ x₂)))
      with lem-bd-hole bd
    ... | BDσSubst x₃ bdσ x₄ = BDσSubst (BDLam x₃ x) (lem-bdσ-into-lam bdσ x₁) (UBLam2 (flip x₂) x₄)
    lem-bd-hole {σ = Subst d y σ} (BDAp bd bd₁)
      with lem-bd-hole bd | lem-bd-hole bd₁
    ... | BDσSubst x bdσ ub | BDσSubst x₁ bdσ₁ ub₁ = BDσSubst (BDAp x x₁) (lem-bdσ-into-ap bdσ bdσ₁) (UBAp ub ub₁)
    lem-bd-hole {σ = Subst d y σ} (BDInl bd)
      with lem-bd-hole bd
    ... | BDσSubst x bdσ ub = BDσSubst (BDInl x) (lem-bdσ-into-inl bdσ) (UBInl ub)
    lem-bd-hole {σ = Subst d y σ} (BDInr bd)
      with lem-bd-hole bd
    ... | BDσSubst x bdσ ub = BDσSubst (BDInr x) (lem-bdσ-into-inr bdσ) (UBInr ub)
    lem-bd-hole {σ = Subst d y σ} (BDCase bd (UBHole (UBσSubst x x₁ x₂)) bd₁ (UBHole (UBσSubst x₃ x₄ x₅)) bd₂)
      with lem-bd-hole bd | lem-bd-hole bd₁ | lem-bd-hole bd₂
    ... | BDσSubst y bdσ ub | BDσSubst y₁ bdσ₁ ub₁ | BDσSubst y₂ bdσ₂ ub₂ = BDσSubst (BDCase y x y₁ x₃ y₂) (lem-bdσ-into-case bdσ x₁ bdσ₁ x₄ bdσ₂) (UBCase ub (flip x₂) ub₁ (flip x₅) ub₂)
    lem-bd-hole {σ = Subst d y σ} (BDPair bd bd₁)
      with lem-bd-hole bd | lem-bd-hole bd₁
    ... | BDσSubst x bdσ ub | BDσSubst y₁ bdσ₁ ub₁ = BDσSubst (BDPair x y₁) (lem-bdσ-into-pair bdσ bdσ₁) (UBPair ub ub₁)
    lem-bd-hole {σ = Subst d y σ} (BDFst bd)
      with lem-bd-hole bd
    ... | BDσSubst x bdσ ub = BDσSubst (BDFst x) (lem-bdσ-into-fst bdσ) (UBFst ub)
    lem-bd-hole {σ = Subst d y σ} (BDSnd bd)
      with lem-bd-hole bd
    ... | BDσSubst x bdσ ub = BDσSubst (BDSnd x) (lem-bdσ-into-snd bdσ) (UBSnd ub)
    lem-bd-hole {u = u} {σ = Subst d y σ} (BDHole {u = u₁} {σ = Id Γ} BDσId) =
      BDσSubst (BDHole BDσId)
               (lem-bdσ-into-hole BDσsId) (UBHole UBσId)
    lem-bd-hole {u = u} {σ = Subst d y σ} (BDHole {u = u₁} {σ = Subst d₁ y₁ σ₁} (BDσSubst (BDHole (BDσSubst x x₂ x₃)) bd (UBHole (UBσSubst x₁ x₄ x₅))))
      with lem-bdσ-hole bd
    ... | BDσsSubst x₆ q x₇ = BDσSubst (BDHole (BDσSubst (binders-disjoint-sym x) x₆ x₁)) (lem-bdσ-into-hole (BDσsSubst x₂ (lem-bdσs-sym q) x₄)) (UBHole (UBσSubst x₃ x₇ (flip x₅)))
    lem-bd-hole {σ = Subst d y σ} (BDNEHole {σ = Id Γ} BDσId bd)
      with lem-bd-hole bd
    ... | BDσSubst x bdσ x₁ = BDσSubst (BDNEHole BDσId x) (lem-bdσ-into-nehole BDσsId bdσ) (UBNEHole UBσId x₁)
    lem-bd-hole {σ = Subst d y σ} (BDNEHole {σ = Subst d₁ y₁ σ'} (BDσSubst (BDHole (BDσSubst x x₃ x₄)) x₁ (UBHole (UBσSubst x₂ x₅ x₆))) bd)
      with lem-bd-hole bd | lem-bdσ-hole x₁
    ... | BDσSubst x₇ bdσ x₈ | BDσsSubst x₉ bdσs x₁₀ = BDσSubst (BDNEHole (BDσSubst (binders-disjoint-sym x) x₉ x₂) x₇) (lem-bdσ-into-nehole (BDσsSubst x₃ (lem-bdσs-sym bdσs) x₅) bdσ) (UBNEHole (UBσSubst x₄ x₁₀ (flip x₆)) x₈)
    lem-bd-hole {σ = Subst d y σ} (BDCast bd)
      with lem-bd-hole bd
    ... | BDσSubst y bdσ ub = BDσSubst (BDCast y) (lem-bdσ-into-cast bdσ) (UBCast ub)
    lem-bd-hole {σ = Subst d y σ} (BDFailedCast bd)
      with lem-bd-hole bd
    ... | BDσSubst y bdσ ub = BDσSubst (BDFailedCast y) (lem-bdσ-into-failedcast bdσ) (UBFailedCast ub)

    lem-bdσ-into-nehole : ∀{σ d u σ'} →
                          binders-disjoint-σs σ σ' →
                          binders-disjoint-σ σ d →
                          binders-disjoint-σ σ ⦇⌜ d ⌟⦈⟨ u , σ' ⟩
    lem-bdσ-into-nehole BDσsId BDσId = BDσId
    lem-bdσ-into-nehole BDσsId (BDσSubst x bd x₁) = BDσSubst (BDNEHole BDσId x) (lem-bdσ-into-nehole BDσsId bd) (UBNEHole UBσId x₁)
    lem-bdσ-into-nehole (BDσsSubst x bds x₁) BDσId = BDσId
    lem-bdσ-into-nehole (BDσsSubst (BDσSubst x x₈ x₉) (BDσsSubst x₄ bds x₅) (UBσSubst x₁ x₆ x₇)) (BDσSubst x₂ bd x₃) = BDσSubst (BDNEHole (BDσSubst (binders-disjoint-sym x) x₄ x₁) x₂) (lem-bdσ-into-nehole (BDσsSubst x₈ (lem-bdσs-sym bds) x₆) bd) (UBNEHole (UBσSubst x₉ x₅ (flip x₇)) x₃)

    lem-bdσ-nehole : ∀{d u σ σ'} →
                     binders-disjoint-σ σ ⦇⌜ d ⌟⦈⟨ u , σ' ⟩ →
                     binders-disjoint-σs σ σ' × binders-disjoint-σ σ d
    lem-bdσ-nehole BDσId = (lem-bdσs-sym BDσsId) , BDσId
    lem-bdσ-nehole (BDσSubst (BDNEHole x x₁) bd (UBNEHole x₂ ub))
      with lem-bdσ-nehole bd
    ... | bds' , bd' = (lem-bdσs-sym (BDσsSubst x bds' x₂)) , (BDσSubst x₁ bd' ub)

    lem-bd-nehole : ∀{d1 d u σ} →
                    binders-disjoint d1 ⦇⌜ d ⌟⦈⟨ u , σ ⟩ →
                    binders-disjoint-σ σ d1 × binders-disjoint d1 d
    lem-bd-nehole BDNum = lem-bdσ-num , BDNum
    lem-bd-nehole (BDPlus bd bd₁)
      with lem-bd-nehole bd | lem-bd-nehole bd₁
    ... | bdσ' , bd' | bd₁' , bdσ₁' = lem-bdσ-into-plus bdσ' bd₁' , BDPlus bd' bdσ₁'
    lem-bd-nehole BDVar = lem-bdσ-var , BDVar
    lem-bd-nehole (BDLam bd (UBNEHole x x₁))
      with lem-bd-nehole bd
    ... | bdσ' , bd' = lem-bdσ-into-lam bdσ' x , BDLam bd' x₁
    lem-bd-nehole (BDAp bd bd₁)
      with lem-bd-nehole bd | lem-bd-nehole bd₁
    ... | bdσ' , bd' | bd₁' , bdσ₁' = lem-bdσ-into-ap bdσ' bd₁' , BDAp bd' bdσ₁'
    lem-bd-nehole (BDInl bd)
      with lem-bd-nehole bd
    ... | bdσ' , bd' = lem-bdσ-into-inl bdσ' , BDInl bd'
    lem-bd-nehole (BDInr bd)
      with lem-bd-nehole bd
    ... | bdσ' , bd' = lem-bdσ-into-inr bdσ' , BDInr bd'
    lem-bd-nehole (BDCase bd (UBNEHole x x₁) bd₁ (UBNEHole x₂ x₃) bd₂)
      with lem-bd-nehole bd | lem-bd-nehole bd₁ | lem-bd-nehole bd₂
    ... | bdσ' , bd' | bdσ₁' , bd₁' | bdσ₂' , bd₂' = lem-bdσ-into-case bdσ' x bdσ₁' x₂ bdσ₂' , BDCase bd' x₁ bd₁' x₃ bd₂'
    lem-bd-nehole (BDPair bd bd₁)
       with lem-bd-nehole bd | lem-bd-nehole bd₁
    ... | bdσ' , bd' | bdσ₁' , bd₁' = lem-bdσ-into-pair bdσ' bdσ₁' , BDPair bd' bd₁'
    lem-bd-nehole (BDFst bd)
      with lem-bd-nehole bd
    ... | bdσ' , bd' = lem-bdσ-into-fst bdσ' , BDFst bd'
    lem-bd-nehole (BDSnd bd)
      with lem-bd-nehole bd
    ... | bdσ' , bd' = lem-bdσ-into-snd bdσ' , BDSnd bd'
    lem-bd-nehole (BDHole {u = u} {σ = Id Γ} BDσId) = lem-bdσ-into-hole BDσsId , BDHole BDσId
    lem-bd-nehole (BDHole {u = u} {σ = Subst d y σ'} (BDσSubst (BDNEHole x x₃) x₁ (UBNEHole x₂ x₄)))
      with lem-bdσ-nehole x₁
    ... | bdσ , bdσs = (lem-bdσ-into-hole (BDσsSubst x bdσ x₂)) , (BDHole (BDσSubst x₃ bdσs x₄))
    lem-bd-nehole (BDNEHole {σ = Id Γ} BDσId bd)
      with lem-bd-nehole bd
    ... | bdσ , bdσs = lem-bdσ-into-nehole BDσsId bdσ , BDNEHole BDσId bdσs
    lem-bd-nehole (BDNEHole {σ = Subst d y σ'} (BDσSubst (BDNEHole x x₃) x₁ (UBNEHole x₂ x₄)) bd)
      with lem-bd-nehole bd | lem-bdσ-nehole x₁
    ... | bdσ , bd' | bdσs , bdσ' = (lem-bdσ-into-nehole (BDσsSubst x bdσs x₂) bdσ) , BDNEHole (BDσSubst x₃ bdσ' x₄) bd'
    lem-bd-nehole (BDCast bd)
      with lem-bd-nehole bd
    ... | bdσ' , bd' = lem-bdσ-into-cast bdσ' , BDCast bd'
    lem-bd-nehole (BDFailedCast bd)
      with lem-bd-nehole bd
    ... | bdσ' , bd' = lem-bdσ-into-failedcast bdσ' , BDFailedCast bd'

    binders-disjoint-sym : ∀{d1 d2} → binders-disjoint d1 d2 → binders-disjoint d2 d1
    binders-disjoint-sym {d2 = N x} bd = BDNum
    binders-disjoint-sym {d2 = d2 ·+ d3} bd
      with lem-bd-plus bd
    ... | bd1 , bd2 = BDPlus (binders-disjoint-sym bd1) (binders-disjoint-sym bd2)
    binders-disjoint-sym {d2 = X x} bd = BDVar
    binders-disjoint-sym {d2 = ·λ x ·[ x₁ ] d2} bd
      with lem-bd-lam bd
    ... | bd' , ub = BDLam (binders-disjoint-sym bd') ub
    binders-disjoint-sym {d2 = d2 ∘ d3} bd
      with lem-bd-ap bd
    ... | bd1 , bd2 = BDAp (binders-disjoint-sym bd1) (binders-disjoint-sym bd2)
    binders-disjoint-sym {d2 = inl x d2} bd = BDInl (binders-disjoint-sym (lem-bd-inl bd))
    binders-disjoint-sym {d2 = inr x d2} bd = BDInr (binders-disjoint-sym (lem-bd-inr bd))
    binders-disjoint-sym {d2 = case d2 x d3 x₁ d4} bd
      with lem-bd-case bd
    ... | bdd , ubx , bdd1 , uby , bdd2 = BDCase (binders-disjoint-sym bdd) ubx (binders-disjoint-sym bdd1) uby (binders-disjoint-sym bdd2)
    binders-disjoint-sym {d2 = ⟨ d2 , d3 ⟩} bd
      with lem-bd-pair bd
    ... | bd1 , bd2 = BDPair (binders-disjoint-sym bd1) (binders-disjoint-sym bd2)
    binders-disjoint-sym {d2 = fst d2} bd = BDFst (binders-disjoint-sym (lem-bd-fst bd))
    binders-disjoint-sym {d2 = snd d2} bd = BDSnd (binders-disjoint-sym (lem-bd-snd bd))
    binders-disjoint-sym {d2 = ⦇-⦈⟨ u , σ ⟩} bd = BDHole (lem-bd-hole bd)
    binders-disjoint-sym {d2 = ⦇⌜ d2 ⌟⦈⟨ u , σ ⟩} bd
      with lem-bd-nehole bd
    ... | bdσ , bd' = BDNEHole bdσ (binders-disjoint-sym bd')
    binders-disjoint-sym {d2 = d2 ⟨ x ⇒ x₁ ⟩} bd = BDCast (binders-disjoint-sym (lem-bd-cast bd))
    binders-disjoint-sym {d2 = d2 ⟨ x ⇒⦇-⦈⇏ x₁ ⟩} bd = BDFailedCast (binders-disjoint-sym (lem-bd-failedcast bd))

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
{-

This file proves a variety of basic results about paths:

- refl, sym, cong and composition of paths. This is used to set up
  equational reasoning.

- Transport, subst and functional extensionality

- J and its computation rule (up to a path)

- Σ-types and contractibility of singletons

- Converting PathP to and from a homogeneous path with transp

- Direct definitions of lower h-levels

- Export natural numbers

- Export universe lifting

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.Prelude where

open import Cubical.Core.Primitives public

infixr 30 _∙_
infix  3 _∎
infixr 2 _≡⟨_⟩_

-- Basic theory about paths. These proofs should typically be
-- inlined. This module also makes equational reasoning work with
-- (non-dependent) paths.

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : A → Type ℓ
    x y z : A

refl : x ≡ x
refl {x = x} = λ _ → x

sym : x ≡ y → y ≡ x
sym p i = p (~ i)

symP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} →
       (p : PathP A x y) → PathP (λ i → A (~ i)) y x
symP p j = p (~ j)

cong : ∀ (f : (a : A) → B a) (p : x ≡ y) →
       PathP (λ i → B (p i)) (f x) (f y)
cong f p i = f (p i)

cong₂ : ∀ {C : (a : A) → (b : B a) → Type ℓ} →
        (f : (a : A) → (b : B a) → C a b) →
        (p : x ≡ y) →
        {u : B x} {v : B y} (q : PathP (λ i → B (p i)) u v) →
        PathP (λ i → C (p i) (q i)) (f x u) (f y v)
cong₂ f p q i = f (p i) (q i)

-- The filler of homogeneous path composition:
-- compPath-filler p q = PathP (λ i → x ≡ q i) p (p ∙ q)

compPath-filler : ∀ {x y z : A} → x ≡ y → y ≡ z → I → I → A
compPath-filler {x = x} p q j i =
  hfill (λ j → λ { (i = i0) → x
                  ; (i = i1) → q j }) (inS (p i)) j

_∙_ : x ≡ y → y ≡ z → x ≡ z
(p ∙ q) j = compPath-filler p q i1 j

-- The filler of heterogeneous path composition:
-- compPathP-filler p q = PathP (λ i → PathP (λ j → (compPath-filler (λ i → A i) B i j)) x (q i)) p (compPathP p q)

compPathP-filler : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → {B_i1 : Type ℓ} {B : A i1 ≡ B_i1} → {z : B i1} →
  (p : PathP A x y) → (q : PathP (λ i → B i) y z) → ∀ (i j : I) → compPath-filler (λ i → A i) B j i
compPathP-filler {A = A} {x = x} {B = B} p q i =
  fill (λ j → compPath-filler (λ i → A i) B j i)
       (λ j → λ { (i = i0) → x ;
                   (i = i1) → q j }) (inS (p i))

compPathP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → {B_i1 : Type ℓ} {B : (A i1) ≡ B_i1} → {z : B i1} →
  (p : PathP A x y) → (q : PathP (λ i → B i) y z) → PathP (λ j → ((λ i → A i) ∙ B) j) x z
compPathP p q j = compPathP-filler p q j i1

_≡⟨_⟩_ : (x : A) → x ≡ y → y ≡ z → x ≡ z
_ ≡⟨ x≡y ⟩ y≡z = x≡y ∙ y≡z

≡⟨⟩-syntax : (x : A) → x ≡ y → y ≡ z → x ≡ z
≡⟨⟩-syntax = _≡⟨_⟩_
infixr 2 ≡⟨⟩-syntax
syntax ≡⟨⟩-syntax x (λ i → B) y = x ≡[ i ]⟨ B ⟩ y

_∎ : (x : A) → x ≡ x
_ ∎ = refl

-- another definition of composition, useful for some proofs
compPath'-filler : ∀ {x y z : A} → x ≡ y → y ≡ z → I → I → A
compPath'-filler {z = z} p q j i =
  hfill (λ j → λ { (i = i0) → p (~ j)
                 ; (i = i1) → z }) (inS (q i)) j

_□_ : x ≡ y → y ≡ z → x ≡ z
(p □ q) j = compPath'-filler p q i1 j

□≡∙ : (p : x ≡ y) (q : y ≡ z) → p □ q ≡ p ∙ q
□≡∙ {x = x} {y = y} {z = z} p q i j = hcomp (λ k → \ { (i = i0) → compPath'-filler p q k j
                                             ; (i = i1) → compPath-filler p q k j
                                             ; (j = i0) → p ( ~ i ∧ ~ k)
                                             ; (j = i1) → q (k ∨ ~ i) }) (helper i j)
  where
    helper : PathP (λ i → p (~ i) ≡ q (~ i)) q p
    helper i j = hcomp (λ k → \ { (i = i0) → q (k ∧ j)
                                ; (i = i1) → p (~ k ∨ j)
                                ; (j = i0) → p (~ i ∨ ~ k)
                                ; (j = i1) → q (~ i ∧ k) })
                       y

-- Transport, subst and functional extensionality

-- transport is a special case of transp
transport : {A B : Type ℓ} → A ≡ B → A → B
transport p a = transp (λ i → p i) i0 a

-- Transporting in a constant family is the identity function (up to a
-- path). If we would have regularity this would be definitional.
transportRefl : (x : A) → transport refl x ≡ x
transportRefl {A = A} x i = transp (λ _ → A) i x

-- We want B to be explicit in subst
subst : (B : A → Type ℓ') (p : x ≡ y) → B x → B y
subst B p pa = transport (λ i → B (p i)) pa

substRefl : (px : B x) → subst B refl px ≡ px
substRefl px = transportRefl px

funExt : {f g : (x : A) → B x} → ((x : A) → f x ≡ g x) → f ≡ g
funExt p i x = p x i

-- J for paths and its computation rule

module _ (P : ∀ y → x ≡ y → Type ℓ') (d : P x refl) where
  J : (p : x ≡ y) → P y p
  J p = transport (λ i → P (p i) (λ j → p (i ∧ j))) d

  JRefl : J refl ≡ d
  JRefl = transportRefl d

-- Contractibility of singletons

singl : (a : A) → Type _
singl {A = A} a = Σ[ x ∈ A ] (a ≡ x)

contrSingl : (p : x ≡ y) → Path (singl x) (x , refl) (y , p)
contrSingl p i = (p i , λ j → p (i ∧ j))

-- Converting to and from a PathP

module _ {A : I → Type ℓ} {x : A i0} {y : A i1} where
  toPathP : transp A i0 x ≡ y → PathP A x y
  toPathP p i = hcomp (λ j → λ { (i = i0) → x
                               ; (i = i1) → p j })
                      (transp (λ j → A (i ∧ j)) (~ i) x)

  fromPathP : PathP A x y → transp A i0 x ≡ y
  fromPathP p i = transp (λ j → A (i ∨ j)) i (p i)

-- Direct definitions of lower h-levels

isContr : Type ℓ → Type ℓ
isContr A = Σ[ x ∈ A ] (∀ y → x ≡ y)

isProp : Type ℓ → Type ℓ
isProp A = (x y : A) → x ≡ y

isSet : Type ℓ → Type ℓ
isSet A = (x y : A) → isProp (x ≡ y)

Square
  : ∀{w x y z : A}
  → (p : w ≡ y) (q : w ≡ x) (r : y ≡ z) (s : x ≡ z)
  → Set _
Square p q r s = PathP (λ i → p i ≡ s i) q r

isSet' : Type ℓ → Type ℓ
isSet' A
  = {x y z w : A}
  → (p : x ≡ y) (q : z ≡ w) (r : x ≡ z) (s : y ≡ w)
  → Square r p q s

isGroupoid : Type ℓ → Type ℓ
isGroupoid A = ∀ a b → isSet (Path A a b)

Cube
  : ∀{w x y z w' x' y' z' : A}
  → {p : w ≡ y} {q : w ≡ x} {r : y ≡ z} {s : x ≡ z}
  → {p' : w' ≡ y'} {q' : w' ≡ x'} {r' : y' ≡ z'} {s' : x' ≡ z'}
  → {a : w ≡ w'} {b : x ≡ x'} {c : y ≡ y'} {d : z ≡ z'}
  → (ps : Square a p p' c) (qs : Square a q q' b)
  → (rs : Square c r r' d) (ss : Square b s s' d)
  → (f0 : Square p q r s) (f1 : Square p' q' r' s')
  → Set _
Cube ps qs rs ss f0 f1
  = PathP (λ k → Square (ps k) (qs k) (rs k) (ss k)) f0 f1

isGroupoid' : Set ℓ → Set ℓ
isGroupoid' A
  = ∀{w x y z w' x' y' z' : A}
  → {p : w ≡ y} {q : w ≡ x} {r : y ≡ z} {s : x ≡ z}
  → {p' : w' ≡ y'} {q' : w' ≡ x'} {r' : y' ≡ z'} {s' : x' ≡ z'}
  → {a : w ≡ w'} {b : x ≡ x'} {c : y ≡ y'} {d : z ≡ z'}
  → (fp : Square a p p' c) → (fq : Square a q q' b)
  → (fr : Square c r r' d) → (fs : Square b s s' d)
  → (f0 : Square p q r s) → (f1 : Square p' q' r' s')
  → Cube fp fq fr fs f0 f1

is2Groupoid : Type ℓ → Type ℓ
is2Groupoid A = ∀ a b → isGroupoid (Path A a b)

-- Essential consequences of isProp and isContr
isProp→PathP
  : ((x : A) → isProp (B x)) → {a0 a1 : A}
  → (p : a0 ≡ a1) (b0 : B a0) (b1 : B a1)
  → PathP (λ i → B (p i)) b0 b1
isProp→PathP {B = B} P p b0 b1 = toPathP {A = λ i → B (p i)} {b0} {b1} (P _ _ _)

isPropIsContr : isProp (isContr A)
isPropIsContr z0 z1 j =
  ( z0 .snd (z1 .fst) j
  , λ x i → hcomp (λ k → λ { (i = i0) → z0 .snd (z1 .fst) j
                           ; (i = i1) → z0 .snd x (j ∨ k)
                           ; (j = i0) → z0 .snd x (i ∧ k)
                           ; (j = i1) → z1 .snd x i })
                  (z0 .snd (z1 .snd x i) j))

isContr→isProp : isContr A → isProp A
isContr→isProp (x , p) a b i =
  hcomp (λ j → λ { (i = i0) → p a j
                 ; (i = i1) → p b j }) x

isProp→isSet : isProp A → isSet A
isProp→isSet h a b p q j i =
  hcomp (λ k → λ { (i = i0) → h a a k
                 ; (i = i1) → h a b k
                 ; (j = i0) → h a (p i) k
                 ; (j = i1) → h a (q i) k }) a

-- Universe lifting

record Lift {i j} (A : Type i) : Type (ℓ-max i j) where
  instance constructor lift
  field
    lower : A

open Lift public

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Structures.Group where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Functions.FunExtEquiv

open import Cubical.Homotopy.Base

open import Cubical.Data.Sigma

open import Cubical.Relation.Binary

open import Cubical.Algebra.Group
open import Cubical.Structures.LeftAction

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties
open import Cubical.DStructures.Structures.Constant

open import Cubical.DStructures.Structures.Type

private
  variable
    ℓ ℓ' : Level

open URGStr

-------------------------------------------
-- URG structure on the type of groups
-------------------------------------------

𝒮-group : (ℓ : Level) → URGStr (Group {ℓ}) ℓ
𝒮-group ℓ ._≅_ = GroupEquiv
𝒮-group ℓ .ρ = idGroupEquiv
𝒮-group ℓ .uni = isUnivalent'→isUnivalent GroupEquiv
                                          idGroupEquiv
                                          λ G H → invEquiv (GroupPath G H)

-------------------------------------------
-- 𝒮ᴰ-hierarchies on top of 𝒮-group
--
-- Notation:
--
-- G - group
-- G² - pair of groups
-- F - morphism forth
-- B - morphism back
--
-- F B (FB)
-- \ | /
--   G
--   |
--   G
-------------------------------------------

module _ (ℓ ℓ' : Level) where

  ---- Underlying types

  -- pairs of groups
  G² = Group {ℓ} × Group {ℓ'}
  -- pairs of groups + a morphism forth
  G²F = Σ[ (G , H) ∈ G² ] GroupHom G H
  -- pairs of groups + a morphism back
  G²B = Σ[ (G , H) ∈ G² ] GroupHom H G
  -- pairs of groups + morphisms forth and back
  G²FB = Σ[ (G , H) ∈ G² ] GroupHom G H × GroupHom H G

  ---- 𝒮 and 𝒮ᴰ-structures

  -- Group morphisms displayed over pairs of groups
  𝒮ᴰ-G²\F : URGStrᴰ (𝒮-group ℓ ×𝒮 𝒮-group ℓ')
                    (λ (G , H) → GroupHom G H)
                    (ℓ-max ℓ ℓ')
  𝒮ᴰ-G²\F =
    make-𝒮ᴰ (λ {(G , H)} {(G' , H')} f (eG , eH) f' → (g : ⟨ G ⟩) → GroupEquiv.eq eH .fst ((f .fun) g) ≡ (f' .fun) (GroupEquiv.eq eG .fst g))
            (λ _ _ → refl)
            λ (G , H) f → isContrRespectEquiv (Σ-cong-equiv-snd (λ f' → isoToEquiv (invIso (GroupMorphismExtIso f f'))))
                                              (isContrSingl f)
    where open GroupHom

  -- URG structure on type of two groups with a group morphism
  𝒮-G²F : URGStr G²F (ℓ-max ℓ ℓ')
  𝒮-G²F = ∫⟨ 𝒮-group ℓ ×𝒮 𝒮-group ℓ' ⟩ 𝒮ᴰ-G²\F

  -- Same as 𝒮-G²F but with the morphism going the other way
  𝒮ᴰ-G²\B : URGStrᴰ (𝒮-group ℓ ×𝒮 𝒮-group ℓ')
                             (λ (G , H) → GroupHom H G)
                             (ℓ-max ℓ ℓ')
  𝒮ᴰ-G²\B =
    make-𝒮ᴰ (λ {(_ , H)} f (eG , eH) f' → (h : ⟨ H ⟩) → GroupEquiv.eq eG .fst (f .fun h) ≡ f' .fun (GroupEquiv.eq eH .fst h))
                (λ _ _ → refl)
                λ _ f → isContrRespectEquiv (Σ-cong-equiv-snd (λ f' → isoToEquiv (invIso (GroupMorphismExtIso f f')))) (isContrSingl f)
    where open GroupHom

  -- Type of two groups with a group morphism going back
  𝒮-G²B : URGStr G²B (ℓ-max ℓ ℓ')
  𝒮-G²B = ∫⟨ 𝒮-group ℓ ×𝒮 𝒮-group ℓ' ⟩ 𝒮ᴰ-G²\B

  -- Morphisms going forth and back displayed over pairs of groups
  𝒮ᴰ-G²\FB : URGStrᴰ (𝒮-group ℓ ×𝒮 𝒮-group ℓ')
                   (λ (G , H) → GroupHom G H × GroupHom H G)
                   (ℓ-max ℓ ℓ')
  𝒮ᴰ-G²\FB = combine-𝒮ᴰ 𝒮ᴰ-G²\F 𝒮ᴰ-G²\B

  -- URG structure on type of pairs of groups with morphisms going forth and back
  𝒮-G²FB : URGStr G²FB (ℓ-max ℓ ℓ')
  𝒮-G²FB = ∫⟨ 𝒮-group ℓ ×𝒮 𝒮-group ℓ' ⟩ 𝒮ᴰ-G²\FB

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
-- Hilbert-style formalisation of closed syntax.
-- Nested terms.

module OldBasicILP.UntypedSyntax.ClosedHilbert where

open import OldBasicILP.UntypedSyntax.Common public

-- Closed, untyped representations.

data Rep : Set where
  APP   : Rep → Rep → Rep
  CI    : Rep
  CK    : Rep
  CS    : Rep
  BOX   : Rep → Rep
  CDIST : Rep
  CUP   : Rep
  CDOWN : Rep
  CPAIR : Rep
  CFST  : Rep
  CSND  : Rep
  UNIT  : Rep

-- Anti-bug wrappers.

record Proof : Set where
  constructor [_]
  field
    rep : Rep

open ClosedSyntax (Proof) public

-- Derivations using representations in types.

mutual
  infix 3 ⊢_
  data ⊢_ : Ty → Set where
    app   : ∀ {A B}   → ⊢ A ▻ B → ⊢ A → ⊢ B
    ci    : ∀ {A}     → ⊢ A ▻ A
    ck    : ∀ {A B}   → ⊢ A ▻ B ▻ A
    cs    : ∀ {A B C} → ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C

    box   : ∀ {A}     → (d : ⊢ A)
                      → ⊢ [ ᴿ⌊ d ⌋ ] ⦂ A

    cdist : ∀ {A B}   → {r₁ r₂ : Rep}
                      → ⊢ [ r₁ ] ⦂ (A ▻ B) ▻ [ r₂ ] ⦂ A ▻ [ APP r₁ r₂ ] ⦂ B

    cup   : ∀ {A}     → {r : Rep}
                      → ⊢ [ r ] ⦂ A ▻ [ BOX r ] ⦂ [ r ] ⦂ A

    cdown : ∀ {A}     → {r : Rep}
                      → ⊢ [ r ] ⦂ A ▻ A

    cpair : ∀ {A B}   → ⊢ A ▻ B ▻ A ∧ B
    cfst  : ∀ {A B}   → ⊢ A ∧ B ▻ A
    csnd  : ∀ {A B}   → ⊢ A ∧ B ▻ B
    unit  : ⊢ ⊤

  -- Projection from derivations to representations.

  ᴿ⌊_⌋ : ∀ {A} → ⊢ A → Rep
  ᴿ⌊ app d₁ d₂ ⌋ = APP ᴿ⌊ d₁ ⌋ ᴿ⌊ d₂ ⌋
  ᴿ⌊ ci ⌋        = CI
  ᴿ⌊ ck ⌋        = CK
  ᴿ⌊ cs ⌋        = CS
  ᴿ⌊ box d ⌋     = BOX ᴿ⌊ d ⌋
  ᴿ⌊ cdist ⌋     = CDIST
  ᴿ⌊ cup ⌋       = CUP
  ᴿ⌊ cdown ⌋     = CDOWN
  ᴿ⌊ cpair ⌋     = CPAIR
  ᴿ⌊ cfst ⌋      = CFST
  ᴿ⌊ csnd ⌋      = CSND
  ᴿ⌊ unit ⌋      = UNIT

infix 3 ⊢⋆_
⊢⋆_ : Cx Ty → Set
⊢⋆ ∅     = 𝟙
⊢⋆ Ξ , A = ⊢⋆ Ξ × ⊢ A

-- Cut and multicut.

cut : ∀ {A B} → ⊢ A → ⊢ A ▻ B → ⊢ B
cut d₁ d₂ = app d₂ d₁

multicut : ∀ {Ξ A} → ⊢⋆ Ξ → ⊢ Ξ ▻⋯▻ A → ⊢ A
multicut {∅}     ∙         d₂ = d₂
multicut {Ξ , B} (ds , d₁) d₂ = app (multicut ds d₂) d₁

-- Contraction.

ccont : ∀ {A B} → ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = app (app cs cs) (app ck ci)

cont : ∀ {A B} → ⊢ A ▻ A ▻ B → ⊢ A ▻ B
cont d = app ccont d

-- Exchange, or Schönfinkel’s C combinator.

cexch : ∀ {A B C} → ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = app (app cs (app (app cs (app ck cs))
                         (app (app cs (app ck ck)) cs)))
            (app ck ck)

exch : ∀ {A B C} → ⊢ A ▻ B ▻ C → ⊢ B ▻ A ▻ C
exch d = app cexch d

-- Composition, or Schönfinkel’s B combinator.

ccomp : ∀ {A B C} → ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = app (app cs (app ck cs)) ck

comp : ∀ {A B C} → ⊢ B ▻ C → ⊢ A ▻ B → ⊢ A ▻ C
comp d₁ d₂ = app (app ccomp d₁) d₂

-- Useful theorems in functional form.

dist : ∀ {A B r₁ r₂} → ⊢ [ r₁ ] ⦂ (A ▻ B) → ⊢ [ r₂ ] ⦂ A → ⊢ [ APP r₁ r₂ ] ⦂ B
dist d₁ d₂ = app (app cdist d₁) d₂

up : ∀ {A r} → ⊢ [ r ] ⦂ A → ⊢ [ BOX r ] ⦂ [ r ] ⦂ A
up d = app cup d

down : ∀ {A r} → ⊢ [ r ] ⦂ A → ⊢ A
down d = app cdown d

distup : ∀ {A B r₀ r₁} → ⊢ [ r₁ ] ⦂ ([ r₀ ] ⦂ A ▻ B) → ⊢ [ r₀ ] ⦂ A → ⊢ [ APP r₁ (BOX r₀) ] ⦂ B
distup d₁ d₂ = dist d₁ (up d₂)

pair : ∀ {A B} → ⊢ A → ⊢ B → ⊢ A ∧ B
pair d₁ d₂ = app (app cpair d₁) d₂

fst : ∀ {A B} → ⊢ A ∧ B → ⊢ A
fst d = app cfst d

snd : ∀ {A B} → ⊢ A ∧ B → ⊢ B
snd d = app csnd d

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pairs of lists that share no common elements (setoid equality)
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.List.Relation.Binary.Disjoint.Setoid {c ℓ} (S : Setoid c ℓ) where

open import Level using (_⊔_)
open import Relation.Nullary using (¬_)
open import Function using (_∘_)
open import Data.List.Base using (List; []; [_]; _∷_)
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.Product using (_×_; _,_)

open Setoid S renaming (Carrier to A)
open import Data.List.Membership.Setoid S using (_∈_; _∉_)

------------------------------------------------------------------------
-- Definition

Disjoint : Rel (List A) (ℓ ⊔ c)
Disjoint xs ys = ∀ {v} → ¬ (v ∈ xs × v ∈ ys)

------------------------------------------------------------------------
-- Operations

contractₗ : ∀ {x xs ys} → Disjoint (x ∷ xs) ys → Disjoint xs ys
contractₗ x∷xs∩ys=∅ (v∈xs , v∈ys) = x∷xs∩ys=∅ (there v∈xs , v∈ys)

contractᵣ : ∀ {xs y ys} → Disjoint xs (y ∷ ys) → Disjoint xs ys
contractᵣ xs#y∷ys (v∈xs , v∈ys) = xs#y∷ys (v∈xs , there v∈ys)


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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Setoids.Setoids
open import Setoids.Subset
open import Setoids.Functions.Definition
open import Sets.EquivalenceRelations

module Setoids.Functions.Lemmas {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {f : A → B} (w : WellDefined S T f) where

inverseImagePred : {e : _} → {pred : B → Set e} → (sub : subset T pred) → A → Set (b ⊔ d ⊔ e)
inverseImagePred {pred = pred} subset a = Sg B (λ b → (pred b) && (Setoid._∼_ T (f a) b))

inverseImageWellDefined : {e : _} {pred : B → Set e} → (sub : subset T pred) → subset S (inverseImagePred sub)
inverseImageWellDefined sub {x} {y} x=y (b , (predB ,, fx=b)) = f x , (sub (symmetric fx=b) predB ,, symmetric (w x=y))
  where
    open Setoid T
    open Equivalence eq


text:
------------------------------------------------------------------------------
-- FOT (First-Order Theories)
------------------------------------------------------------------------------

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

-- Code accompanying the PhD thesis "Reasoning about Functional
-- Programs by Combining Interactive and Automatic Proofs" by Andrés
-- Sicard-Ramírez.

-- The code presented here does not match the thesis exactly.

module README where

------------------------------------------------------------------------------
-- Description

-- Examples of the formalization of first-order theories showing the
-- combination of interactive proofs with automatics proofs carried
-- out by first-order automatic theorem provers (ATPs).

------------------------------------------------------------------------------
-- For the thesis, prerequisites, tested versions of the ATPs and use,
-- see https://github.com/asr/fotc/.

------------------------------------------------------------------------------
-- Conventions

-- If the module's name ends in 'I' the module contains interactive
-- proofs, if it ends in 'ATP' the module contains combined proofs,
-- otherwise the module contains definitions and/or interactive proofs
-- that are used by the interactive and combined proofs.

------------------------------------------------------------------------------
-- First-order theories
------------------------------------------------------------------------------

-- • First-order logic with equality

-- First-order logic (FOL)
open import FOL.README

-- Propositional equality
open import Common.FOL.Relation.Binary.PropositionalEquality

-- Equality reasoning
open import Common.FOL.Relation.Binary.EqReasoning

-- • Group theory

open import GroupTheory.README

-- • Distributive laws on a binary operation (Stanovský example)

open import DistributiveLaws.README

-- • First-order Peano arithmetic (PA)

open import PA.README

-- • First-Order Theory of Combinators (FOTC)

open import FOTC.README

-- • Logical Theory of Constructions for PCF (LTC-PCF)

open import LTC-PCF.README

------------------------------------------------------------------------------
-- Agsy examples
------------------------------------------------------------------------------

-- We cannot import the Agsy examples because some modules contain
-- unsolved metas, therefore see examples/Agsy/README.txt

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Type

module Graph.Walk.Proofs {ℓ₁ ℓ₂} {V : Type{ℓ₁}} where

open import Lang.Instance
open import Logic
import      Lvl
open import Graph{ℓ₁}{ℓ₂}(V)
open import Graph.Walk{ℓ₁}{ℓ₂}{V}
open import Relator.Equals.Proofs.Equiv
import      Structure.Relator.Names as Names
open import Structure.Relator.Properties
open import Type.Properties.Singleton

private variable ℓ : Lvl.Level
private variable _⟶_ : Graph
private variable a b : V
private variable _▫_ : V → V → Type{ℓ}

-- There is a walk between two vertices when there is one edge between them.
instance
  Walk-super : (_⟶_) ⊆₂ (Walk(_⟶_))
  _⊆₂_.proof Walk-super p = prepend p at

-- Walk is a "smallest" reflexive-transitive closure
Walk-sub : ⦃ _ : Reflexivity(_▫_) ⦄ → ⦃ _ : Transitivity(_▫_) ⦄ → ⦃ _ : (_⟶_) ⊆₂ (_▫_) ⦄ → (Walk(_⟶_)) ⊆₂ (_▫_)
Walk-sub {_▫_ = _▫_}{_⟶_ = _⟶_} = intro proof where
  proof : Names.Subrelation(Walk(_⟶_))(_▫_)
  proof at                    = transitivity(_▫_) (reflexivity(_▫_)) (reflexivity(_▫_))
  proof (prepend ab1 walkb1b) = transitivity(_▫_) (sub₂(_⟶_)(_▫_) ab1) (proof walkb1b)

Walk-transitivity-raw : Names.Transitivity(Walk(_⟶_))
Walk-transitivity-raw at              xz = xz
Walk-transitivity-raw (prepend xb by) yz = prepend xb (Walk-transitivity-raw by yz)

instance
  -- A walk can be joined/concatenated to form a new walk.
  Walk-transitivity : Transitivity(Walk(_⟶_))
  Transitivity.proof Walk-transitivity = Walk-transitivity-raw

instance
  Walk-reflexivity : Reflexivity(Walk(_⟶_))
  Walk-reflexivity = intro at

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 --safe #-}

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Fundamental.Variable {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

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

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Fundamental theorem for variables.
fundamentalVar : ∀ {Γ A rA x}
               → x ∷ A ^ rA ∈ Γ
               → ([Γ] : ⊩ᵛ Γ)
               → ∃ λ ([A] : Γ ⊩ᵛ⟨ ∞ ⟩ A ^ rA / [Γ])
               → Γ ⊩ᵛ⟨ ∞ ⟩ var x ∷ A ^ rA / [Γ] / [A]
fundamentalVar here (_∙_ {A = A} {rA = rA} {l = l} [Γ] [A]) =
    (λ ⊢Δ [σ] →
       let [σA]  = proj₁ ([A] ⊢Δ (proj₁ [σ]))
           [σA′] = maybeEmb (irrelevance′ (PE.sym (subst-wk A)) [σA])
       in  [σA′]
       ,   (λ [σ′] [σ≡σ′] →
              irrelevanceEq″ (PE.sym (subst-wk A)) (PE.sym (subst-wk A)) PE.refl PE.refl
                              [σA] [σA′] (proj₂ ([A] ⊢Δ (proj₁ [σ]))
                                                (proj₁ [σ′]) (proj₁ [σ≡σ′]))))
    , (λ ⊢Δ [σ] →
         let [σA]  = proj₁ ([A] ⊢Δ (proj₁ [σ]))
             [σA′] = maybeEmb (irrelevance′ (PE.sym (subst-wk A)) [σA])
         in  irrelevanceTerm′ (PE.sym (subst-wk A)) PE.refl PE.refl [σA] [σA′] (proj₂ [σ])
    , (λ [σ′] [σ≡σ′] → irrelevanceEqTerm′ (PE.sym (subst-wk A)) PE.refl PE.refl
                                          [σA] [σA′] (proj₂ [σ≡σ′])))
fundamentalVar (there {A = A} h) ([Γ] ∙ [B]) =
    (λ ⊢Δ [σ] →
       let [h]   = proj₁ (fundamentalVar h [Γ]) ⊢Δ (proj₁ [σ])
           [σA]  = proj₁ [h]
           [σA′] = irrelevance′ (PE.sym (subst-wk A)) [σA]
       in  [σA′]
       ,   (λ [σ′] [σ≡σ′] →
              irrelevanceEq″ (PE.sym (subst-wk A)) (PE.sym (subst-wk A)) PE.refl PE.refl
                              [σA] [σA′]
                              (proj₂ [h] (proj₁ [σ′]) (proj₁ [σ≡σ′]))))
    , (λ ⊢Δ [σ] →
         let [h]   = (proj₁ (fundamentalVar h [Γ])) ⊢Δ (proj₁ [σ])
             [σA]  = proj₁ [h]
             [σA′] = irrelevance′ (PE.sym (subst-wk A)) [σA]
             [h′] = (proj₂ (fundamentalVar h [Γ])) ⊢Δ (proj₁ [σ])
         in  irrelevanceTerm′ (PE.sym (subst-wk A)) PE.refl PE.refl [σA] [σA′] (proj₁ [h′])
         ,   (λ [σ′] [σ≡σ′] →
                irrelevanceEqTerm′ (PE.sym (subst-wk A)) PE.refl PE.refl [σA] [σA′]
                                   (proj₂ [h′] (proj₁ [σ′]) (proj₁ [σ≡σ′]))))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt