text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Structures for types of functions
------------------------------------------------------------------------

-- The contents of this file should usually be accessed from `Function`.

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

open import Relation.Binary

module Function.Structures
  {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
  where

open import Data.Product using (∃; _×_; _,_)
open import Function.Base
open import Function.Definitions
open import Level using (_⊔_)

------------------------------------------------------------------------
-- Definitions

record IsCongruent (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    cong           : Congruent _≈₁_ _≈₂_ f
    isEquivalence₁ : IsEquivalence _≈₁_
    isEquivalence₂ : IsEquivalence _≈₂_

  module Eq₁ where

    setoid : Setoid a ℓ₁
    setoid = record
      { isEquivalence = isEquivalence₁
      }

    open Setoid setoid public

  module Eq₂ where

    setoid : Setoid b ℓ₂
    setoid = record
      { isEquivalence = isEquivalence₂
      }

    open Setoid setoid public

record IsInjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isCongruent : IsCongruent f
    injective   : Injective _≈₁_ _≈₂_ f

  open IsCongruent isCongruent public

record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isCongruent : IsCongruent f
    surjective  : Surjective _≈₁_ _≈₂_ f

  open IsCongruent isCongruent public

record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isInjection : IsInjection f
    surjective  : Surjective _≈₁_ _≈₂_ f

  open IsInjection isInjection public

  bijective : Bijective _≈₁_ _≈₂_ f
  bijective = injective , surjective

  isSurjection : IsSurjection f
  isSurjection = record
    { isCongruent = isCongruent
    ; surjective  = surjective
    }

record IsLeftInverse (f : A → B) (g : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isCongruent  : IsCongruent f
    cong₂        : Congruent _≈₂_ _≈₁_ g
    inverseˡ     : Inverseˡ _≈₁_ _≈₂_ f g

  open IsCongruent isCongruent public
    renaming (cong to cong₁)

record IsRightInverse (f : A → B) (g : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isCongruent : IsCongruent f
    cong₂       : Congruent _≈₂_ _≈₁_ g
    inverseʳ    : Inverseʳ _≈₁_ _≈₂_ f g

  open IsCongruent isCongruent public
    renaming (cong to cong₁)

record IsBiEquivalence
  (f : A → B) (g₁ : B → A) (g₂ : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    f-isCongruent : IsCongruent f
    cong₂         : Congruent _≈₂_ _≈₁_ g₁
    cong₃         : Congruent _≈₂_ _≈₁_ g₂

  open IsCongruent f-isCongruent public
    renaming (cong to cong₁)

record IsBiInverse
  (f : A → B) (g₁ : B → A) (g₂ : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    f-isCongruent : IsCongruent f
    cong₂         : Congruent _≈₂_ _≈₁_ g₁
    inverseˡ      : Inverseˡ _≈₁_ _≈₂_ f g₁
    cong₃         : Congruent _≈₂_ _≈₁_ g₂
    inverseʳ      : Inverseʳ _≈₁_ _≈₂_ f g₂

  open IsCongruent f-isCongruent public
    renaming (cong to cong₁)

record IsInverse (f : A → B) (g : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isLeftInverse : IsLeftInverse f g
    inverseʳ      : Inverseʳ _≈₁_ _≈₂_ f g

  open IsLeftInverse isLeftInverse public

  isRightInverse : IsRightInverse f g
  isRightInverse = record
    { isCongruent = isCongruent
    ; cong₂       = cong₂
    ; inverseʳ    = inverseʳ
    }

  inverse : Inverseᵇ _≈₁_ _≈₂_ f g
  inverse = inverseˡ , inverseʳ


text:
-- Andreas, 2016-07-28, issue #779

record P : Set where
  postulate Bla : Set
  field F : Set

-- Current error:
-- Missing definition for Bla

-- Expected:
-- Success, or error outlawing postulate before last field.

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-

This is a HoTT-UF core library based on cubical type theory, where the
cubical machinery is hidden, using the HoTT Book terminology and
notation.

The point is that function extensionality, propositional truncation
and univalence compute (an example is given below).

For the moment, this requires the development version of Agda.

-}

{-# OPTIONS --cubical --exact-split --safe #-}

module Cubical.Foundations.HoTT-UF where

open import Cubical.Core.Primitives hiding ( _≡_ )
open import Cubical.Core.Id public

open import Cubical.Foundations.Id public
     using ( _≡_            -- The identity type.
           ; refl           -- Unfortunately, pattern matching on refl is not available.
           ; J              -- Until it is, you have to use the induction principle J.

           ; transport      -- As in the HoTT Book.
           ; ap
           ; _∙_
           ; _⁻¹

           ; _≡⟨_⟩_         -- Standard equational reasoning.
           ; _∎

           ; funExt         -- Function extensionality
                            -- (can also be derived from univalence).

           ; Σ              -- Sum type. Needed to define contractible types, equivalences
           ; _,_            -- and univalence.
           ; pr₁            -- The eta rule is available.
           ; pr₂

           ; isProp         -- The usual notions of proposition, contractible type, set.
           ; isContr
           ; isSet

           ; isEquiv        -- A map with contractible fibers
                            -- (Voevodsky's version of the notion).
           ; _≃_            -- The type of equivalences between two given types.
           ; EquivContr     -- A formulation of univalence.

           ; ∥_∥             -- Propositional truncation.
           ; ∣_∣             -- Map into the propositional truncation.
           ; ∥∥-isProp       -- A truncated type is a proposition.
           ; ∥∥-recursion    -- Non-dependent elimination.
           ; ∥∥-induction    -- Dependent elimination.
           )

{-

Here is an illustration of how function extensionality computes.

-}

private

  data ℕ : Type₀ where
   zero : ℕ
   succ : ℕ → ℕ

  f g : ℕ → ℕ

  f n = n

  g zero = zero
  g (succ n) = succ (g n)

  h : (n : ℕ) → f n ≡ g n
  h zero = refl
  h (succ n) = ap succ (h n)

  p : f ≡ g
  p = funExt h

  five : ℕ
  five = succ (succ (succ (succ (succ zero))))

  a : Σ ℕ (λ n → f n ≡ five)
  a = five , refl

  b : Σ ℕ (λ n → g n ≡ five)
  b = transport (λ - → Σ ℕ (λ n → - n ≡ five)) p a

  c : pr₁ b ≡ five
  c = refl

{-

If we had funExt as a postulate, then the definition of c would not
type check. Moreover, the term pr₁ b would not evaluate to five, as it
does with the cubical type theory implementation of funext.

TODO. A similar computational example with univalence.

-}

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module Logic.Relations where

import Logic.Base
import Data.Bool

Rel : Set -> Set1
Rel A = A -> A -> Set

Reflexive : {A : Set} -> Rel A -> Set
Reflexive {A} _R_ = (x : A) -> x R x

Symmetric : {A : Set} -> Rel A -> Set
Symmetric {A} _R_  = (x y : A) -> x R y -> y R x

Transitive : {A : Set} -> Rel A -> Set
Transitive {A} _R_ = (x y z : A) -> x R y -> y R z -> x R z

Congruent : {A : Set} -> Rel A -> Set
Congruent {A} _R_ = (f : A -> A)(x y : A) -> x R y -> f x R f y

Substitutive : {A : Set} -> Rel A -> Set1
Substitutive {A} _R_ = (P : A -> Set)(x y : A) -> x R y -> P x -> P y

module PolyEq (_≡_ : {A : Set} -> Rel A) where

  Antisymmetric : {A : Set} -> Rel A -> Set
  Antisymmetric {A} _R_ = (x y : A) -> x R y -> y R x -> x ≡ y

module MonoEq {A : Set}(_≡_ : Rel A) where

  Antisymmetric : Rel A -> Set
  Antisymmetric _R_ = (x y : A) -> x R y -> y R x -> x ≡ y

open Logic.Base

Total : {A : Set} -> Rel A -> Set
Total {A} _R_ = (x y : A) -> (x R y) \/ (y R x)

Decidable : (P : Set) -> Set
Decidable P = P \/ ¬ P


text:
{-  -}
-- starting from builtins
-- forgot what the point of this was...
module Oscar.Data6 where

open import Oscar.Category.Semigroupoid
open import Oscar.Category.Category
open import Oscar.Category.Morphism
open import Oscar.Category.Setoid
open import Oscar.Function

open import Agda.Builtin.Unit using () renaming (⊤ to 𝟙; tt to ∅)
open import Agda.Builtin.Nat using () renaming (Nat to ℕ; zero to ∅; suc to ↑_)
open import Agda.Builtin.List using () renaming (List to [_]ℕ; [] to ∅; _∷_ to _+_)

open import Oscar.Level

⟦_⟧ℕ[<_↓]
⟦_⟧ℕ[_≤_↓]
⟦_⟧ℕ[↥_≤_]
⟦_⟧ℕ[↓_≤_↓]

-- Fin (with a payload)
data ⟦_⟧ℕ[0…_-1] {a} (A : ℕ → Set a) : ℕ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧ℕ[<↑ ↑ n ]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧ℕ[ n ] → ⟦ A ⟧ℕ[<↑ ↑ n ]

-- Vec (with an (optional) index)
data ⟦_⟧ℕ[≤_] {a} (A : ℕ → Set a) : ℕ → Set a where
  ∅ : ⟦ A ⟧ℕ[ ∅ ₀]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧ℕ[ n ₀] → ⟦ A ⟧ℕ[ ¡ n ₀]

-- m ≤ n, counting down from n-1 to m
data ⟦_⟧ℕ[_≤_↓] {a} (A : ℕ → Set a) (m : ℕ) : ℕ → Set a where
  ∅ : ⟦ A ⟧ℕ[ m ≤ m ↓]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧ℕ[ m ≤ n ↓] → ⟦ A ⟧ℕ[ m ≤ ¡ n ↓]

-- m ≤ n, counting up from m to n-1
data ⟦_⟧ℕ[↑_≤_] {a} (A : ℕ → Set a) (m : ℕ) : ℕ → Set a where
  ∅ : ⟦ A ⟧ℕ[↑ m ≤ m ]
  _∷_ : ∀ {n} → A m → ⟦ A ⟧ℕ[↑ ¡ m ≤ n ] → ⟦ A ⟧ℕ[↑ m ≤ n ]

-- Inj (almost)
data ⟦_⟧ℕ[↓_≤_↓] {a} (A : ℕ → ℕ → Set a) : ℕ → ℕ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧ℕ[↓ ∅ ≤ n ↓]
  _∷_ : ∀ {m n} → A m n → ⟦ A ⟧ℕ[↓ m ≤ n ↓] → ⟦ A ⟧ℕ[↓ ¡ m ≤ ¡ n ↓]

⟦_⟧ℕ[_⇒_]∞ : ∀ {a} (A : ℕ → Set a) → ℕ → ℕ → Set a
⟦ A ⟧ℕ[ m ⇒ n ]∞ = A m → A n

-- Fin (with a payload)
data ⟦_⟧ℕ[<_↓] {a} (A : ℕ → Set a) : ℕ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧[< ↑ n ↓]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧ℕ[< n ] → ⟦ A ⟧[< ↑ n ↓]

-- -- Vec (with an (optional) index)
data ℕ[_]=_ {a} (A : ℕ → Set a) : ℕ → Set a where
  ∅ : ℕ[ A ]= ∅
  _∷_ : ∀ {n} → A n → ℕ[ A ]= ↑ n → ℕ[ A ]= ↑ n

ℕ=_ = ℕ[ const 𝟙 ]=_

-- m ≤ n, counting down from n-1 to m

data ℕ[_]≥_<↓_ {a} (A : ℕ → Set a) (m : ℕ) : ℕ → Set a where
  ∅ : ℕ[ A ]≥ m <↓ m
  _∷_ : ∀ {n} → A n → ℕ[ A ]≥ m <↓ n → ℕ[ A ]≥ m <↓ ↑ n

ℕ≥_<↓_ = ℕ[ const 𝟙 ]≥_<↓_

-- m ≤ n, counting up from m to n-1
data ℕ[_]≥↑_<_ {a} (A : ℕ → Set a) (m : ℕ) : ℕ → Set a where
  ∅ : ℕ[ A ]≥↑ m < m
  _∷_ : ∀ {n} → A m → ℕ[ A ]≥↑ ↑ m < n → ℕ[ A ]≥↑ m < n

ℕ≥↑_<_ = ℕ[ const 𝟙 ]≥↑_<_

-- -- Inj (almost)
-- data ⟦_⟧[↓_≤_↓] {a} (A : ⟦⟧ → ⟦⟧ → Set a) : ⟦⟧ → ⟦⟧ → Set a where
--   ∅ : ∀ {n} → ⟦ A ⟧[↓ ∅ ≤ n ↓]
--   _∷_ : ∀ {m n} → A m n → ⟦ A ⟧[↓ m ≤ n ↓] → ⟦ A ⟧[↓ ¡ m ≤ ¡ n ↓]

-- ⟦⟧[↓_≤_↓] = ⟦ Const Const ⊤ ⟧[↓_≤_↓]

-- ⟦_⟧[_⇒_]∞ : ∀ {a} (A : ⟦⟧ → Set a) → ⟦⟧ → ⟦⟧ → Set a
-- ⟦ A ⟧[ m ⇒ n ]∞ = A m → A n

-- --open import Oscar.Data.Equality
-- --open import Oscar.Data.Equality.properties

-- module _ {𝔬 𝔪 𝔮} (G : Semigroupoid 𝔬 𝔪 𝔮) where
--   open Semigroupoid G

-- {-
--   _≋̇_ : ∀ {a} {A : ⋆ → Set a} {m n : ⋆} → (A m → A n) → (A m → A n) → Set 𝔮
--   _≋̇_ {A = A} {m = m} m→n₁ m→n₂ = {!∀ (am : A m) → m→n₁ am ≋ m→n₂ am!}

--   cat2 : ∀ {a} (A : ⋆ → Set a) → Category {!!} {!!} {!!}
--   Semigroupoid.⋆ (Category.semigroupoid (cat2 A)) = ⋆
--   Setoid.⋆ ((Semigroupoid.𝔐 (Category.semigroupoid (cat2 A)) Morphism.⇒ m) n) = A m → A n
--   IsSetoid._≋_ (Setoid.isSetoid ((Semigroupoid.𝔐 (Category.semigroupoid (cat2 A)) Morphism.⇒ m) n)) = _≡̇_
--   IsSetoid.isEquivalence (Setoid.isSetoid ((Semigroupoid.𝔐 (Category.semigroupoid (cat2 A)) Morphism.⇒ m) n)) = it
--   Semigroupoid._∙_ (Category.semigroupoid (cat2 A)) g f = g ∘ f
--   Semigroupoid.isSemigroupoid (Category.semigroupoid (cat2 A)) = it
--   Category.ε (cat2 A) = id
--   Category.isCategory (cat2 A) = it

--   cat2G : ∀ {a} (A : ⋆ → Set a) → ∀ ℓ ⦃ _ : ∀ {n : ⋆} → IsSetoid (A n) ℓ ⦄ → Category {!!} {!!} {!!}
--   Semigroupoid.⋆ (Category.semigroupoid (cat2G A ℓ)) = ⋆
--   Setoid.⋆ ((Semigroupoid.𝔐 (Category.semigroupoid (cat2G A ℓ)) Morphism.⇒ m) n) = A m → A n
--   IsSetoid._≋_ (Setoid.isSetoid ((Semigroupoid.𝔐 (Category.semigroupoid (cat2G A ℓ)) Morphism.⇒ m) n)) m↦n₁ m↦n₂ = ∀ (am : A m) → m↦n₁ am ≋ m↦n₂ am
--   -- ∀ (am : A m) → m↦n₁ am ≋ m↦n₂ am
--   {-
--   _≋̇_ : ∀ {a} {A : ⋆ → Set a} {m n : ⋆} → (A m → A n) → (A m → A n) → Set 𝔮
--   _≋̇_ {A = A} {m = m} m→n₁ m→n₂ = {!∀ (am : A m) → m→n₁ am ≋ m→n₂ am!}
--   -}
--   IsSetoid.isEquivalence (Setoid.isSetoid ((Semigroupoid.𝔐 (Category.semigroupoid (cat2G A ℓ)) Morphism.⇒ m) n)) = {!it!}
--   Semigroupoid._∙_ (Category.semigroupoid (cat2G A ℓ)) g f = g ∘ f
--   Semigroupoid.isSemigroupoid (Category.semigroupoid (cat2G A ℓ)) = {!it!}
--   Category.ε (cat2G A ℓ) = id
--   Category.isCategory (cat2G A ℓ) = {!it!}
-- -}

-- infix 21 ‼_
-- pattern ‼_ ⟦A⟧ = tt ∷ ⟦A⟧ -- tricky, works for all above _∷_ constructors only because it is defined afterwards, won't work for any later-defined constructors

-- open import Agda.Primitive
-- open import Oscar.Data.Product
-- open import Oscar.Function

-- postulate
--   ℓ : Level
--   Term : ⟦⟧ → Set ℓ
--   Step : ⟦⟧ → Set ℓ

-- Fin = ⟦⟧[_]

-- Inj = ⟦ Const Fin ⟧[↓_≤_↓]

-- Terms = λ N n → ⟦ Const (Term n) ⟧[ N ₀]

-- AList = ⟦ (λ n → Term n × Fin (¡ n)) ⟧[_≤_↓]

-- Fx : ∀ {a} {A : Set a} → A → A → ∀ {b₁} (B₁ : A → Set b₁) → ∀ {b₂} (B₂ : A → Set b₂) → Set (b₁ ⊔ b₂)
-- Fx m n B₁ B₂ = B₁ m → B₂ n

-- Fx₁ : ∀ {a} {A : Set a} → A → ∀ {b₁} (B₁ : A → Set b₁) → ∀ {b₂} (B₂ : A → Set b₂) → Set (b₁ ⊔ b₂)
-- Fx₁ n B₁ B₂ = Fx n n B₁ B₂

-- ListStep = λ n → ⟦ Step n ⟧

-- Rel : ∀ {a} {A : Set a} {b₁} (B₁ : A → Set b₁) {b₂} (B₂ : A → Set b₂) {c₁} (C₁ : A → Set c₁) {c₂} (C₂ : A → Set c₂) → Set (a ⊔ b₁ ⊔ b₂ ⊔ c₁ ⊔ c₂)
-- Rel B₁ B₂ C₁ C₂ = ∀ {m n} → Fx m n B₁ B₂ → Fx m n C₁ C₂

-- Morph : ∀ {a} {A : Set a} {b₁} {b₂} (B : (A → Set b₁) × (A → Set b₂)) {c₁} {c₂} (C₂ : (A → Set c₁) × (A → Set c₂)) → Set (a ⊔ b₁ ⊔ b₂ ⊔ c₁ ⊔ c₂)
-- Morph (B₁ , B₂) (C₁ , C₂) = ∀ {m n} → Fx m n B₁ B₂ → Fx m n C₁ C₂

-- -- functor mappings
-- postulate
--   _◃_ : Morph (Fin , Term) (Term , Term)
--   _◃s_ : ∀ N → Morph (Fin , Term) (Terms N , Terms N)
--   sub : ∀ {m n} → AList m n → Fx m n Fin Term
--   fmapS : Morph (Term , Term) (Step , Step)
--   _◃S_ : Morph (Fin , Term) (ListStep , ListStep)

-- -- ?
-- postulate
--   _⊹_ : ∀ {n} → ⟦ Step n ⟧ → Fx₁ n Term Term

-- testNat : ⟦⟧
-- testNat = ¡ ∅

-- testListNat : ⟦ ⟦⟧ ⟧
-- testListNat = ¡ ∅ ∷ ‼ ∅ ∷ ‼ ‼ ∅ ∷ ∅ ∷ ¡ ¡ ¡ ∅ ∷ ∅

-- testFin : ⟦⟧[ ¡ ¡ ∅ ]
-- testFin = ‼ ∅

-- test≤↓ : ⟦⟧[ ‼ ‼ ‼ ∅ ≤ ‼ ‼ ‼ ‼ ‼ ∅ ↓]
-- test≤↓ = ‼ ‼ ∅

-- ⓪ ⑴ ⑵ ⑶ : ⟦⟧
-- ⓪ = ∅
-- ⑴ = ‼ ∅
-- ⑵ = ‼ ⑴
-- ⑶ = ‼ ⑵

-- testInj : Inj ⑵ ⑶
-- testInj = ‼ ∅ ∷ ∅ ∷ ∅


text:
-- Currently postulates are not allowed in mutual blocks.
-- This might change.
module PostulateInMutual where

mutual
  postulate A : Set
  postulate B : Set

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

module Conaturals where
  open import Basics
  open import Bool
  open import lib.Basics
  open import lib.types.Nat
  open import lib.types.Bool

  {-

  _is-increasing-b : (ℕ → Bool) → Type _
  P is-increasing-b = (n m : ℕ) → n ≤ m → (P n) holds-b → (P m) holds-b

  increasing-b-is-a-prop : (P : ℕ → Bool) → (P is-increasing-b) is-a-prop
  increasing-b-is-a-prop P =
    mp (λ _ → mp (λ x → mp (λ _ → mp (λ _ → (Bool-to-Prop₀ (P x)) holds-is-a-prop ))))
    where mp = mapping-into-prop-is-a-prop

  ℕ∞-prop : SubtypeProp (ℕ → Bool) _
  ℕ∞-prop = _is-increasing-b , increasing-b-is-a-prop

  ℕ∞ : Type₀
  ℕ∞ = Subtype ℕ∞-prop

  -}

  -- I'm having trouble using coinduction =[
  -- The type of conatural numbers
  record ℕ∞ : Type₀ where
    coinductive
    field
      pred∞ : ℕ∞ ⊔ ⊤
    pattern go∞ x = inl x
    pattern stop∞ = inr unit
  open ℕ∞ public

  coO : ℕ∞
  pred∞ coO = stop∞

  co∞ : ℕ∞
  pred∞ co∞ = go∞ co∞

  suc∞ : ℕ∞ → ℕ∞
  pred∞ (suc∞ x) = go∞ x

  ℕ-to-ℕ∞ : ℕ → ℕ∞
  ℕ-to-ℕ∞ O = coO
  ℕ-to-ℕ∞ (S n) = suc∞ (ℕ-to-ℕ∞ n)

  case-pred∞_of_ : {i : ULevel} {A : Type i}
                  (n : ℕ∞) (f :  ℕ∞ ⊔ ⊤ → A)
                  → A
  case-pred∞ n of f = f (pred∞ n)
  {-
    For a paradigmatic use of this function, see below:
  -}

  pred∞-is-coO : ℕ∞ → Bool
  pred∞-is-coO n =
    case-pred∞ n of (λ {
      (go∞ _) → false ;
      stop∞   → true   })

  case∞ : {i : ULevel} {A : Type i}
          (a : A) (f : ℕ∞ → A)
          → ℕ∞ → A
  case∞ a f n = case-pred∞ n of (λ {
                   stop∞ → a       ;
                   (go∞ x) → f x   })

  syntax case∞ a (λ m → t) n = case∞ n of-co0→ a suc∞- m -→ t

  -- ℕ∞-to-ℕ→Prop : ℕ∞ → (ℕ → Bool)
  -- ℕ∞-to-ℕ→Prop n = case∞ n
  --                    of-co0→ (λ _ → true )
  --                    suc∞- m -→ {! λ { O → false ; (S k) → ℕ∞-to-ℕ→Prop m k }!}
  -- previous 4 lines commented by jonas
{- ℕ∞-to-ℕ→Prop n O = pred∞-is-coO n

    ℕ∞-to-ℕ→Prop n (S k) = {!helperS (pred∞ n) k!}
      where
        helperS : ℕ∞ ⊔ ⊤ → ℕ → Bool
        helperS (go∞ pn) O = {!!}
        helperS (go∞ pn) (S k) = {!!}
        helperS stop∞ k = true -}

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


text:
module help where

open import univ
open import Base

-- Prelims
infixl 150 _#_

K : {A : S} -> S -> Fam A
K B = fam (\_ -> B) (\_ -> refS)

_#_ : {A : S}{F : Fam A} -> El (pi A F) -> (x : El A) -> El (F ! x)
el < f , _ > # x = f x

pFun : {A : S}{F : Fam A}(f : El (pi A F)){x y : El A}(x=y : x == y) ->
       f # x == pFam F x=y << f # y
pFun (el < f , pf >) x=y = pf x=y

p# : {A : S}{F : Fam A}{f g : El (pi A F)}{x : El A} -> f == g -> f # x == g # x
p# {A}{F}{el < f , _ >}{el < g , _ >} (eq f=g) = f=g _

eqDom : {A B : S}{F : Fam A}{G : Fam B} ->
        pi A F =S pi B G -> B =S A
eqDom (eqS < B=A , _ >) = B=A

eqCod : {A B : S}{F : Fam A}{G : Fam B} ->
        (AF=BG : pi A F =S pi B G)(x : El A) ->
        F ! x =S G ! (eqDom AF=BG << x)
eqCod (eqS < B=A , F=G >) = F=G

distr<<# : {A B : S}{F : Fam A}{G : Fam B}(f : El (pi A F)){x : El B}
            (BG=AF : pi B G =S pi A F) ->
            (BG=AF << f) # x == eqCod BG=AF x << f # (eqDom BG=AF << x)
distr<<# (el < f , pf >) {x} (eqS < A=B , G=F >) = ref

eqSnd : {A : S}{F : Fam A}{x : El A}{y z : El (F ! x)} ->
        y == z -> _==_ {sigma A F} (el < x , y >) (el < x , z >)
eqSnd {A}{F}{x}{y}{z} y=z = eq < ref , y=cz >
  where
    y=cz : y == pFam F ref << z
    y=cz = trans y=z (sym (castref _ _))

IsFun : {A : S}{F : Fam A}(f : (x : El A) -> El (F ! x)) -> Set
IsFun {A}{F} f = {x y : El A}(p : F ! x =S F ! y)(x=y : x == y) ->
                 f x == p << f y

mkFun : {A : S}{F : Fam A}(f : (x : El A) -> El (F ! x)) ->
        IsFun {A}{F} f -> El (pi A F)
mkFun {A}{F} f pf = el < f , (\{x}{y} x=y -> pf (pFam F x=y) x=y) >

curryFam : {A : S}{F : Fam A} -> Fam (sigma A F) -> (x : El A) -> Fam (F ! x)
curryFam {A}{F} G x = fam H pH
  where
    H : El (F ! x) -> S
    H y = G ! el < x , y >

    pH : Map _==_ _=S_ H
    pH y=z = pFam G (eq < ref , trans y=z (sym (castref _ _)) >)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Definition.Conversion.Transitivity where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.RedSteps
open import Definition.Conversion
open import Definition.Conversion.Soundness
open import Definition.Conversion.Stability
open import Definition.Conversion.Whnf
open import Definition.Conversion.Conversion
open import Definition.Conversion.Reduction
open import Definition.Conversion.Lift
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Injectivity
import Definition.Typed.Consequences.Inequality as WF
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Substitution
open import Definition.Typed.Consequences.NeTypeEq
open import Definition.Typed.Consequences.SucCong
open import Definition.Typed.Consequences.Inversion
open import Definition.Typed.Consequences.Reduction

open import Tools.Nat
open import Tools.Product
open import Tools.Empty
import Tools.PropositionalEquality as PE

mutual
  -- Transitivity of algorithmic equality of neutrals.
  trans~↑ : ∀ {t u v A B Γ}
         → Γ ⊢ t ~ u ↑ A
         → Γ ⊢ u ~ v ↑ B
         → Γ ⊢ t ~ v ↑ A
         × Γ ⊢ A ≡ B
  trans~↑ (var-refl x₁ x≡y) (var-refl x₂ x≡y₁) =
    var-refl x₁ (PE.trans x≡y x≡y₁)
    , neTypeEq (var _) x₁
               (PE.subst (λ x → _ ⊢ var x ∷ _) (PE.sym x≡y)
                         x₂)
  trans~↑ (app-cong t~u a<>b) (app-cong u~v b<>c) =
    let t~v , ΠFG≡ΠF′G′ = trans~↓ t~u u~v
        F≡F₁ , G≡G₁ = injectivity ΠFG≡ΠF′G′
        a<>c = transConv↑Term F≡F₁ a<>b b<>c
    in  app-cong t~v a<>c , substTypeEq G≡G₁ (soundnessConv↑Term a<>b)
  trans~↑ (fst-cong t~u) (fst-cong u~v) =
    let t~v , ΣFG≡ΣF′G′ = trans~↓ t~u u~v
        F≡F′ , _ = Σ-injectivity ΣFG≡ΣF′G′
    in  fst-cong t~v , F≡F′
  trans~↑ (snd-cong t~u) (snd-cong u~v) =
    let t~v , ΣFG≡ΣF′G′ = trans~↓ t~u u~v
        F≡F′ , G≡G′ = Σ-injectivity ΣFG≡ΣF′G′
    in  snd-cong t~v , substTypeEq G≡G′ (soundness~↑ (fst-cong t~u))
  trans~↑ (natrec-cong A<>B a₀<>b₀ aₛ<>bₛ t~u) (natrec-cong B<>C b₀<>c₀ bₛ<>cₛ u~v) =
    let ⊢Γ = wf (proj₁ (syntacticEqTerm (soundness~↓ t~u)))
        A≡B = soundnessConv↑ A<>B
        F[0]≡F₁[0] = substTypeEq A≡B (refl (zeroⱼ ⊢Γ))
        ΠℕFs≡ΠℕF₁s = sucCong A≡B
        A<>C = transConv↑ A<>B B<>C
        a₀<>c₀ = transConv↑Term F[0]≡F₁[0] a₀<>b₀ b₀<>c₀
        aₛ<>cₛ = transConv↑Term ΠℕFs≡ΠℕF₁s aₛ<>bₛ bₛ<>cₛ
        t~v , _ = trans~↓ t~u u~v
    in  natrec-cong A<>C a₀<>c₀ aₛ<>cₛ t~v
    ,   substTypeEq A≡B (soundness~↓ t~u)
  trans~↑ (Emptyrec-cong A<>B t~u) (Emptyrec-cong B<>C u~v) =
    let A≡B = soundnessConv↑ A<>B
        A<>C = transConv↑ A<>B B<>C
        t~v , _ = trans~↓  t~u u~v
    in  Emptyrec-cong A<>C t~v , A≡B

  -- Transitivity of algorithmic equality of neutrals with types in WHNF.
  trans~↓ : ∀ {t u v A B Γ}
          → Γ ⊢ t ~ u ↓ A
          → Γ ⊢ u ~ v ↓ B
          → Γ ⊢ t ~ v ↓ A
          × Γ ⊢ A ≡ B
  trans~↓ ([~] A₁ D whnfA k~l) ([~] A₂ D₁ whnfA₁ k~l₁) =
    let t~v , A≡B = trans~↑ k~l k~l₁
    in  [~] A₁ D whnfA t~v
    ,   trans (sym (subset* D))
              (trans A≡B
                     (subset* D₁))

  -- Transitivity of algorithmic equality of types.
  transConv↑ : ∀ {A B C Γ}
            → Γ ⊢ A [conv↑] B
            → Γ ⊢ B [conv↑] C
            → Γ ⊢ A [conv↑] C
  transConv↑ ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′)
             ([↑] A″ B″ D₁ D″ whnfA″ whnfB″ A′<>B″) =
    [↑] A′ B″ D D″ whnfA′ whnfB″
        (transConv↓ A′<>B′
                    (PE.subst (λ x → _ ⊢ x [conv↓] B″)
                              (whrDet* (D₁ , whnfA″)
                                        (D′ , whnfB′))
                              A′<>B″))
  transConv↑′ : ∀ {A B C Γ Δ}
              → ⊢ Γ ≡ Δ
              → Γ ⊢ A [conv↑] B
              → Δ ⊢ B [conv↑] C
              → Γ ⊢ A [conv↑] C
  transConv↑′ Γ≡Δ aConvB bConvC =
    transConv↑ aConvB (stabilityConv↑ (symConEq Γ≡Δ) bConvC)

  -- Transitivity of algorithmic equality of types in WHNF.
  transConv↓ : ∀ {A B C Γ}
            → Γ ⊢ A [conv↓] B
            → Γ ⊢ B [conv↓] C
            → Γ ⊢ A [conv↓] C
  transConv↓ (U-refl x) (U-refl x₁) = U-refl x
  transConv↓ (ℕ-refl x) (ℕ-refl x₁) = ℕ-refl x
  transConv↓ (Empty-refl x) (Empty-refl x₁) = Empty-refl x
  transConv↓ (Unit-refl x) (Unit-refl x₁) = Unit-refl x
  transConv↓ (ne x) (ne x₁) =
    let A~C , U≡U = trans~↓ x x₁
    in  ne A~C
  transConv↓ (Π-cong x x₁ x₂) (Π-cong x₃ x₄ x₅) =
    Π-cong x (transConv↑ x₁ x₄) (transConv↑′ (reflConEq (wf x) ∙ soundnessConv↑ x₁) x₂ x₅)
  transConv↓ (Σ-cong x x₁ x₂) (Σ-cong x₃ x₄ x₅) =
    Σ-cong x (transConv↑ x₁ x₄) (transConv↑′ (reflConEq (wf x) ∙ soundnessConv↑ x₁) x₂ x₅)
  -- Refutable cases
  transConv↓ (U-refl x) (ne ([~] A D whnfB ()))
  transConv↓ (ℕ-refl x) (ne ([~] A D whnfB ()))
  transConv↓ (Empty-refl x) (ne ([~] A D whnfB ()))
  transConv↓ (Π-cong x x₁ x₂) (ne ([~] A D whnfB ()))
  transConv↓ (Σ-cong x x₁ x₂) (ne ([~] A D whnfB ()))
  transConv↓ (ne ([~] A₁ D whnfB ())) (U-refl x₁)
  transConv↓ (ne ([~] A₁ D whnfB ())) (ℕ-refl x₁)
  transConv↓ (ne ([~] A₁ D whnfB ())) (Empty-refl x₁)
  transConv↓ (ne ([~] A₁ D whnfB ())) (Π-cong x₁ x₂ x₃)
  transConv↓ (ne ([~] A₁ D whnfB ())) (Σ-cong x₁ x₂ x₃)

  -- Transitivity of algorithmic equality of terms.
  transConv↑Term : ∀ {t u v A B Γ}
                → Γ ⊢ A ≡ B
                → Γ ⊢ t [conv↑] u ∷ A
                → Γ ⊢ u [conv↑] v ∷ B
                → Γ ⊢ t [conv↑] v ∷ A
  transConv↑Term A≡B ([↑]ₜ B₁ t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u)
                 ([↑]ₜ B₂ t″ u″ D₁ d₁ d″ whnfB₁ whnft″ whnfu″ t<>u₁) =
    let B₁≡B₂ = trans (sym (subset* D))
                      (trans A≡B
                             (subset* D₁))
        d₁″ = conv* d″ (sym B₁≡B₂)
        d₁′  = conv* d′ B₁≡B₂
    in  [↑]ₜ B₁ t′ u″ D d d₁″ whnfB whnft′ whnfu″
             (transConv↓Term B₁≡B₂ t<>u
                             (PE.subst (λ x → _ ⊢ x [conv↓] u″ ∷ B₂)
                                       (whrDet*Term (d₁ , whnft″)
                                                    (d₁′ , whnfu′))
                                       t<>u₁))

  transConv↑Term′ : ∀ {t u v A B Γ Δ}
                  → ⊢ Γ ≡ Δ
                  → Γ ⊢ A ≡ B
                  → Γ ⊢ t [conv↑] u ∷ A
                  → Δ ⊢ u [conv↑] v ∷ B
                  → Γ ⊢ t [conv↑] v ∷ A
  transConv↑Term′ Γ≡Δ A≡B tConvU uConvV =
    transConv↑Term A≡B tConvU (stabilityConv↑Term (symConEq Γ≡Δ) uConvV)

  -- Transitivity of algorithmic equality of terms in WHNF.
  transConv↓Term : ∀ {t u v A B Γ}
                → Γ ⊢ A ≡ B
                → Γ ⊢ t [conv↓] u ∷ A
                → Γ ⊢ u [conv↓] v ∷ B
                → Γ ⊢ t [conv↓] v ∷ A
  transConv↓Term A≡B (ℕ-ins x) (ℕ-ins x₁) =
    ℕ-ins (proj₁ (trans~↓ x x₁))
  transConv↓Term A≡B (Empty-ins x) (Empty-ins x₁) =
    Empty-ins (proj₁ (trans~↓ x x₁))
  transConv↓Term A≡B (Unit-ins t~u) uConvV =
    let _ , [t] , _ = syntacticEqTerm (soundness~↓ t~u)
        _ , tNe , _ = ne~↓ t~u
        _ , _ , [v] = syntacticEqTerm (soundnessConv↓Term uConvV)
        [v] = conv [v] (sym A≡B)
        _ , _ , vWhnf = whnfConv↓Term uConvV
    in  η-unit [t] [v] (ne tNe) vWhnf
  transConv↓Term A≡B (ne-ins t u x x₁) (ne-ins t′ u′ x₂ x₃) =
    ne-ins t (conv u′ (sym A≡B)) x
           (proj₁ (trans~↓ x₁ x₃))
  transConv↓Term A≡B (univ x x₁ x₂) (univ x₃ x₄ x₅) =
    univ x x₄ (transConv↓ x₂ x₅)
  transConv↓Term A≡B (zero-refl x) conv↓ =
    convConv↓Term (reflConEq x) (sym A≡B) ℕₙ conv↓
  transConv↓Term A≡B conv↓ (zero-refl _) = conv↓
  transConv↓Term A≡B (suc-cong x) (suc-cong x₁) =
    suc-cong (transConv↑Term A≡B x x₁)
  transConv↓Term A≡B (η-eq x₁ x₂ y y₁ x₃) (η-eq x₅ x₆ y₂ y₃ x₇) =
    let F₁≡F , G₁≡G = injectivity A≡B
    in  η-eq x₁ (conv x₆ (sym A≡B))
             y y₃ (transConv↑Term′ (reflConEq (wfEq F₁≡F) ∙ F₁≡F) G₁≡G x₃ x₇)
  transConv↓Term A≡B (Σ-η ⊢p ⊢r pProd rProd fstConv sndConv)
                     (Σ-η ⊢r′ ⊢q _ qProd fstConv′ sndConv′) =
    let F≡ , G≡ = Σ-injectivity A≡B
        Gfst≡ = substTypeEq G≡ (soundnessConv↑Term fstConv)
    in  Σ-η ⊢p (conv ⊢q (sym A≡B)) pProd qProd
            (transConv↑Term F≡ fstConv fstConv′)
            (transConv↑Term Gfst≡ sndConv sndConv′)
  transConv↓Term A≡B (η-unit [t] [u] tUnit uUnit) uConvV =
    let _ , _ , [v] = syntacticEqTerm (soundnessConv↓Term uConvV)
        [v] = conv [v] (sym A≡B)
        _ , _ , vWhnf = whnfConv↓Term uConvV
    in  η-unit [t] [v] tUnit vWhnf

  -- Refutable cases
  transConv↓Term A≡B (ℕ-ins x) (ne-ins t u x₂ x₃) = ⊥-elim (WF.ℕ≢ne x₂ A≡B)
  transConv↓Term A≡B (ℕ-ins x) (univ x₂ x₃ x₄) = ⊥-elim (WF.U≢ℕ (sym A≡B))
  transConv↓Term A≡B (ℕ-ins x) (Empty-ins x₁) = ⊥-elim (WF.ℕ≢Emptyⱼ A≡B)
  transConv↓Term A≡B (ℕ-ins x) (Unit-ins x₁) = ⊥-elim (WF.ℕ≢Unitⱼ A≡B)
  transConv↓Term A≡B (ℕ-ins ([~] A D whnfB ())) (suc-cong x₂)
  transConv↓Term A≡B (ℕ-ins x) (η-eq x₃ x₄ y y₁ x₅) = ⊥-elim (WF.ℕ≢Π A≡B)
  transConv↓Term A≡B (ℕ-ins x₁) (Σ-η x₂ x₃ x₄ x₅ x₆ x₇) = ⊥-elim (WF.ℕ≢Σ A≡B)
  transConv↓Term A≡B (ℕ-ins x) (η-unit _ _ _ _) = ⊥-elim (WF.ℕ≢Unitⱼ A≡B)
  transConv↓Term A≡B (Empty-ins x) (ne-ins t u x₂ x₃) = ⊥-elim (WF.Empty≢neⱼ x₂ A≡B)
  transConv↓Term A≡B (Empty-ins x) (univ x₂ x₃ x₄) = ⊥-elim (WF.U≢Emptyⱼ (sym A≡B))
  transConv↓Term A≡B (Empty-ins x₁) (ℕ-ins x) = ⊥-elim (WF.ℕ≢Emptyⱼ (sym A≡B))
  transConv↓Term A≡B (Empty-ins x₁) (Unit-ins x) = ⊥-elim (WF.Empty≢Unitⱼ A≡B)
  transConv↓Term A≡B (Empty-ins ([~] A D whnfB ())) (suc-cong x₂)
  transConv↓Term A≡B (Empty-ins x) (η-eq x₃ x₄ y y₁ x₅) = ⊥-elim (WF.Empty≢Πⱼ A≡B)
  transConv↓Term A≡B (Empty-ins x₁) (Σ-η x₂ x₃ x₄ x₅ x₆ x₇) = ⊥-elim (WF.Empty≢Σⱼ A≡B)
  transConv↓Term A≡B (Empty-ins x₁) (η-unit _ _ _ _) = ⊥-elim (WF.Empty≢Unitⱼ A≡B)
  transConv↓Term A≡B (ne-ins t u x x₁) (ℕ-ins x₂) = ⊥-elim (WF.ℕ≢ne x (sym A≡B))
  transConv↓Term A≡B (ne-ins t u x x₁) (Empty-ins x₂) = ⊥-elim (WF.Empty≢neⱼ x (sym A≡B))
  transConv↓Term A≡B (ne-ins t u x x₁) (Unit-ins x₂) = ⊥-elim (WF.Unit≢neⱼ x (sym A≡B))
  transConv↓Term A≡B (ne-ins t u x x₁) (univ x₃ x₄ x₅) = ⊥-elim (WF.U≢ne x (sym A≡B))
  transConv↓Term A≡B (ne-ins t u x ([~] A D whnfB ())) (suc-cong x₃)
  transConv↓Term A≡B (ne-ins t u x x₁) (η-eq x₄ x₅ y y₁ x₆) = ⊥-elim (WF.Π≢ne x (sym A≡B))
  transConv↓Term A≡B (ne-ins t u x x₁) (Σ-η x₅ x₆ x₇ x₈ x₉ x₁₀) = ⊥-elim (WF.Σ≢ne x (sym A≡B))
  transConv↓Term A≡B (ne-ins t u x x₁) (η-unit _ _ _ _) = ⊥-elim (WF.Unit≢neⱼ x (sym A≡B))
  transConv↓Term A≡B (univ x x₁ x₂) (ℕ-ins x₃) = ⊥-elim (WF.U≢ℕ A≡B)
  transConv↓Term A≡B (univ x x₁ x₂) (Empty-ins x₃) = ⊥-elim (WF.U≢Emptyⱼ A≡B)
  transConv↓Term A≡B (univ x x₁ x₂) (Unit-ins x₃) = ⊥-elim (WF.U≢Unitⱼ A≡B)
  transConv↓Term A≡B (univ x x₁ x₂) (ne-ins t u x₃ x₄) = ⊥-elim (WF.U≢ne x₃ A≡B)
  transConv↓Term A≡B (univ x x₁ x₂) (suc-cong x₃) = ⊥-elim (WF.U≢ℕ A≡B)
  transConv↓Term A≡B (univ x x₁ x₂) (η-eq x₄ x₅ y y₁ x₆) = ⊥-elim (WF.U≢Π A≡B)
  transConv↓Term A≡B (univ x₁ x₂ x₃) (Σ-η x₄ x₅ x₆ x₇ x₈ x₉) = ⊥-elim (WF.U≢Σ A≡B)
  transConv↓Term A≡B (univ x x₁ x₂) (η-unit _ _ _ _) = ⊥-elim (WF.U≢Unitⱼ A≡B)
  transConv↓Term A≡B (suc-cong x) (ℕ-ins ([~] A D whnfB ()))
  transConv↓Term A≡B (suc-cong x) (Empty-ins ([~] A D whnfB ()))
  transConv↓Term A≡B (suc-cong x) (ne-ins t u x₁ ([~] A D whnfB ()))
  transConv↓Term A≡B (suc-cong x) (univ x₁ x₂ x₃) = ⊥-elim (WF.U≢ℕ (sym A≡B))
  transConv↓Term A≡B (suc-cong x) (η-eq x₂ x₃ y y₁ x₄) = ⊥-elim (WF.ℕ≢Π A≡B)
  transConv↓Term A≡B (suc-cong x₁) (Σ-η x₂ x₃ x₄ x₅ x₆ x₇) = ⊥-elim (WF.ℕ≢Σ A≡B)
  transConv↓Term A≡B (suc-cong x) (η-unit _ _ _ _) = ⊥-elim (WF.ℕ≢Unitⱼ A≡B)
  transConv↓Term A≡B (η-eq x₁ x₂ y y₁ x₃) (ℕ-ins x₄) = ⊥-elim (WF.ℕ≢Π (sym A≡B))
  transConv↓Term A≡B (η-eq x₁ x₂ y y₁ x₃) (Empty-ins x₄) = ⊥-elim (WF.Empty≢Πⱼ (sym A≡B))
  transConv↓Term A≡B (η-eq x₁ x₂ y y₁ x₃) (Unit-ins _) = ⊥-elim (WF.Unit≢Πⱼ (sym A≡B))
  transConv↓Term A≡B (η-eq x₁ x₂ y y₁ x₃) (ne-ins t u x₄ x₅) = ⊥-elim (WF.Π≢ne x₄ A≡B)
  transConv↓Term A≡B (η-eq x₁ x₂ y y₁ x₃) (univ x₄ x₅ x₆) = ⊥-elim (WF.U≢Π (sym A≡B))
  transConv↓Term A≡B (η-eq x₁ x₂ y y₁ x₃) (suc-cong x₄) = ⊥-elim (WF.ℕ≢Π (sym A≡B))
  transConv↓Term A≡B (η-eq x₂ x₃ x₄ x₅ x₆) (Σ-η x₇ x₈ x₉ x₁₀ x₁₁ x₁₂) = ⊥-elim (WF.Π≢Σ A≡B)
  transConv↓Term A≡B (η-eq x₁ x₂ y y₁ x₃) (η-unit _ _ _ _) = ⊥-elim (WF.Unit≢Πⱼ (sym A≡B))
  transConv↓Term A≡B (Σ-η x₁ x₂ x₃ x₄ x₅ x₆) (ℕ-ins x₇) = ⊥-elim (WF.ℕ≢Σ (sym A≡B))
  transConv↓Term A≡B (Σ-η x₁ x₂ x₃ x₄ x₅ x₆) (Empty-ins x₇) = ⊥-elim (WF.Empty≢Σⱼ (sym A≡B))
  transConv↓Term A≡B (Σ-η x₁ x₂ x₃ x₄ x₅ x₆) (Unit-ins x₇) = ⊥-elim (WF.Unit≢Σⱼ (sym A≡B))
  transConv↓Term A≡B (Σ-η x₁ x₂ x₃ x₄ x₅ x₆) (ne-ins x₇ x₈ x₉ x₁₀) = ⊥-elim (WF.Σ≢ne x₉ A≡B)
  transConv↓Term A≡B (Σ-η x₁ x₂ x₃ x₄ x₅ x₆) (univ x₇ x₈ x₉) = ⊥-elim (WF.U≢Σ (sym A≡B))
  transConv↓Term A≡B (Σ-η x₁ x₂ x₃ x₄ x₅ x₆) (suc-cong x₇) = ⊥-elim (WF.ℕ≢Σ (sym A≡B))
  transConv↓Term A≡B (Σ-η x₁ x₂ x₃ x₄ x₅ x₆) (η-eq x₈ x₉ x₁₀ x₁₁ x₁₂) = ⊥-elim (WF.Π≢Σ (sym A≡B))
  transConv↓Term A≡B (Σ-η x₁ x₂ x₃ x₄ x₅ x₆) (η-unit x₇ x₈ x₉ x₁₀) = ⊥-elim (WF.Unit≢Σⱼ (sym A≡B))

-- Transitivity of algorithmic equality of types of the same context.
transConv : ∀ {A B C Γ}
          → Γ ⊢ A [conv↑] B
          → Γ ⊢ B [conv↑] C
          → Γ ⊢ A [conv↑] C
transConv A<>B B<>C = transConv↑ A<>B B<>C

-- Transitivity of algorithmic equality of terms of the same context.
transConvTerm : ∀ {t u v A Γ}
              → Γ ⊢ t [conv↑] u ∷ A
              → Γ ⊢ u [conv↑] v ∷ A
              → Γ ⊢ t [conv↑] v ∷ A
transConvTerm t<>u u<>v =
  let t≡u = soundnessConv↑Term t<>u
      ⊢A , _ , _ = syntacticEqTerm t≡u
  in  transConv↑Term (refl ⊢A) t<>u u<>v


text:
module Test where

import Lvl

{- TODO: Unsolved metas
module NumAndDivisionProofs where
  open import Functional
  open import Logic.Propositional{Lvl.𝟎}
  open import Logic.Convenience{Lvl.𝟎}
  open import Numeral.Natural
  open import Numeral.Natural.Oper
  open import Numeral.Natural.Relation
  open import Numeral.Natural.Relation.Divisibility
  open import Relator.Equals{Lvl.𝟎}{Lvl.𝟎}
  open import Relator.Equals.Proofs{Lvl.𝟎}{Lvl.𝟎}
  open import Structure.Relator.Properties{Lvl.𝟎}{Lvl.𝟎}

  ℕ4IsEven : Even((𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒)(𝟎))
  ℕ4IsEven = Even0 ⇒ Even𝐒 ⇒ Even𝐒

  ℕ5IsOdd : Odd((𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒)(𝟎))
  ℕ5IsOdd = Odd0 ⇒ Odd𝐒 ⇒ Odd𝐒

  ℕ2Dividesℕ4 : (𝐒 ∘ 𝐒)(𝟎) ∣ (𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒)(𝟎)
  ℕ2Dividesℕ4 = Div𝟎 ⇒ Div𝐒 ⇒ Div𝐒

  ℕ6IsDividesℕ12 : (𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒)(𝟎) ∣ (𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒)(𝟎)
  ℕ6IsDividesℕ12 = Div𝟎 ⇒ Div𝐒 ⇒ Div𝐒

  ℕ4IsDividesℕ12 : (𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒)(𝟎) ∣ (𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒)(𝟎)
  ℕ4IsDividesℕ12 = Div𝟎 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒

  ℕ3IsDividesℕ12 : (𝐒 ∘ 𝐒 ∘ 𝐒)(𝟎) ∣ (𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒)(𝟎)
  ℕ3IsDividesℕ12 = Div𝟎 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒

  ℕ2IsDividesℕ12 : (𝐒 ∘ 𝐒)(𝟎) ∣ (𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒)(𝟎)
  ℕ2IsDividesℕ12 = Div𝟎 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒

  ℕ1IsDividesℕ12 : 𝐒(𝟎) ∣ (𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒 ∘ 𝐒)(𝟎)
  ℕ1IsDividesℕ12 = Div𝟎 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒 ⇒ Div𝐒

  test22 : (2 ∣ 4) → (2 ∣ 2)
  test22 (Div𝐒{2} (proof)) = proof

  test23 : ¬(2 ∣ 3)
  test23 (Div𝐒{1} ())

  -- TODO
  -- ℕ3IsDividesℕ7Remℕ1 : 3 ∣ 7 withRemainder 1
  -- ℕ3IsDividesℕ7Remℕ1 = DivRem𝟎 ⇒ DivRem𝐒 ⇒ DivRem𝐒

  ℕ3Eqℕ2+1 : (𝐒 ∘ 𝐒 ∘ 𝐒)(𝟎) ≡ (𝐒 ∘ 𝐒)(𝟎) + 𝐒(𝟎)
  ℕ3Eqℕ2+1 = reflexivity

  testImpl : 𝐒(𝟎) ≡ (𝟎 ⇒ 𝐒)
  testImpl = reflexivity

  fnℕ+1 : (𝟎 ≡ 𝐒(𝟎)) → (𝐒(𝟎) ≡ (𝐒 ∘ 𝐒)(𝟎))
  fnℕ+1 = congruence₁(𝐒)

  fnℕ+3 : ∀{x} → (x ≡ 5) → (x + 3 ≡ 8)
  fnℕ+3 = congruence₁(x ↦ x + 3)

  ℕ8Eqℕ2⋅4 : 8 ≡ 2 ⋅ 4
  ℕ8Eqℕ2⋅4 = reflexivity

  ℕ0Eqℕ0⋅4 : 0 ≡ 0 ⋅ 4
  ℕ0Eqℕ0⋅4 = reflexivity

  testBottom : (⊥ ∧ ℕ) → ℕ
  testBottom = [∧]-elimᵣ
-}
module DataTest where
  open import Data
  open import Type{Lvl.𝟎}

  data Data1 : Type where
    data1,1 : Data1

  data Data2 : Type where
    data2,1 : Data2
    data2,2 : Data2

  data Data3 : Type where
    data3,1 : Data3
    data3,2 : Data3
    data3,3 : Data3

  dataTest : (Data1 ⨯ Data2 ⨯ Data3) → Data3
  dataTest(x , y , z) = z

-- coprimes m n = ((2*m-n,m) , (2*m+n,m) , (m+2*n,n))
-- coprimes' m n = (a1/a2,b1/b2,c1/c2) where ((a1,a2),(b1,b2),(c1,c2))=f m n
-- map (\m -> map (\n -> (m,n,coprimes m n,coprimes' m n)) [1..m-1]) [1..10]

-- 2 − n/m
-- 2 + n/m
-- 2 + m/n

-- 2 − n₁/m₁ + 2 − n₂/m₂
-- 4 − n₁/m₁ − n₂/m₂
-- 4 − (m₂⋅n₁ − m₁⋅n₂)/(m₁⋅m₂)
-- 4 + (m₁⋅n₂ − m₂⋅n₁)/(m₁⋅m₂)
-- 2 + 2 + (m₁⋅n₂ − m₂⋅n₁)/(m₁⋅m₂)
-- 2 + (2⋅m₁⋅m₂)/(m₁⋅m₂) + (m₁⋅n₂ − m₂⋅n₁)/(m₁⋅m₂)
-- 2 + (2⋅m₁⋅m₂ + m₁⋅n₂ − m₂⋅n₁)/(m₁⋅m₂)

-- 1  1
-- 2  3
-- 3  6
-- 4  10
-- 5  15
-- 6  21
-- 7  28
-- 8  36
-- 9  45
-- 10 55
-- n⋅(n+1)/2 = x
-- n⋅(n+1) = 2⋅x
-- n²+n = 2⋅x
-- n = 1/2 + √(1/4+2⋅x)
-- n = 1/2 + √(9⋅x/4)
-- n = 1/2 + 3⋅√x/2
-- n = (1 + 3⋅√x)/2
-- permutation with sum 4: 1/3 2/2 3/1

-- curryN : {T : Set}{a : _} → ℕ → (a → T) → (a → T)
-- curryN 𝟎 = id
-- curryN (𝐒(n)) = Tuple.curry ∘ (curryN n)

-- test : {a b b1 c : _} → (((a , b) , b1) -> c) -> a -> b -> b1 -> c
-- test = curryN 2

-- test : {a b c d : Set} → (((a ⨯ b) ⨯ c) -> d) -> a -> b -> c -> d
-- test = Tuple.curry ∘ Tuple.curry

-- data repeatType (b : Set) : ∀{q} {a : Set q} -> a -> Set where
--   simple : repeatType b (b -> b)
--   complex : repeatType b (b -> (∀{c : Set} -> b -> c))

-- repeat2 : ∀{b d c} {q : repeatType c d} -> (r : repeatType b c) -> c -> b -> d
-- repeat2 f x simple = f (f x)
-- repeat2 f x complex = f (f x)

module TestRepeatingStuff where
  open import Data
  open import Data.Tuple.Raise
  open import Numeral.Natural
  open import Type

  repeat' : {R : Set} → R → (R → R) → ℕ → R
  repeat' x _ 𝟎 = x
  repeat' x f (𝐒 n) = f(repeat' x f n)

  _⨯^_ : ∀{n} → Set n → ℕ → Set n
  _⨯^_ _    𝟎      = Unit
  _⨯^_ type (𝐒(𝟎)) = type
  _⨯^_ type (𝐒(n)) = type ⨯ (type ⨯^ n)

  _→^_ : ∀{n} → Set n → ℕ → Set n
  _→^_ _    𝟎      = Unit
  _→^_ type (𝐒(𝟎)) = type
  _→^_ type (𝐒(n)) = type → (type →^ n)

  repeatOp : ∀{n} → Set n → (Set n → Set n → Set n) → ℕ → Set n
  repeatOp type _  𝟎      = type
  repeatOp type op (𝐒(n)) = op type (repeatOp type op n)

  _⨯^₂_ : ∀{n} → Set n → ℕ → Set n
  _⨯^₂_ _ 𝟎 = Unit
  _⨯^₂_ type (𝐒(n)) = repeatOp type (_⨯_) n

  testTupleRaise : (ℕ ^ 4) → ℕ ⨯ ℕ ⨯ ℕ ⨯ ℕ
  testTupleRaise x = x

-- curryN : {n : ℕ} → ∀{T} → (T →^ n)

-- not mine
-- data repeatType (b : Set) : ∀{q} {a : Set q} -> a -> Set where
--   simple : repeatType b (b -> b)
--   complex : repeatType b (b -> (∀{c : Set} -> b -> c))
-- repeat2 : ∀{b d c} {q : repeatType c d} -> (r : repeatType b c) -> c -> b -> d
-- repeat2 f x simple = f (f x)
-- repeat2 f x complex = f (f x)

-- module Test1 where
--   F : (ℕ ⨯ ℕ) → ℕ
--   F(x , y) = x + y
--   f : ℕ → ℕ → ℕ
--   f = (Function.Iteration.repeatᵣ 1 Tuple.curry (_∘_) id) F
--
--   testf₁ : F(1 , 2) ≡ 1 + 2
--   testf₁ = [≡]-reflexivity
--
--   testf₂ : f 1 2 ≡ 1 + 2
--   testf₂ = [≡]-reflexivity

module Test2 where
  open import Functional
  open import Function.Iteration
  open import Numeral.Natural
  open import Relator.Equals{Lvl.𝟎}{Lvl.𝟎}
  open import Relator.Equals.Proofs{Lvl.𝟎}{Lvl.𝟎}
  open import Structure.Relator.Properties{Lvl.𝟎}{Lvl.𝟎}

  f : ℕ
  f = (repeatᵣ 4 𝐒 (_∘_) id) 0

  testf₁ : f ≡ 4
  testf₁ = reflexivity

-- f₂ : ∀{n}{A B C D : TypeN n} → (((A ⨯ B) ⨯ C) -> D) -> (A -> B -> C -> D)
-- f₂ = Function.Iteration.repeatᵣ 2 id (_∘_) Tuple.curry

module TestTypeAscription where
  open import Numeral.Natural
  open import Type{Lvl.𝟎}

  ty = 1 :of: ℕ
  -- ty2 = 1 :of: ⊥

-- Testing universes
module TestSetUniverses {n} (Type : Set n) where
  postulate _→₂_ : Type → Type → Set n
  data TestData1 (A : Type) (B : Type) : Set n where
  -- data TestData2 (A : Type) (B : Type) : Type where -- Data of arbitrary type seems to not be okay
  data TestData3 (A : Type) (B : Type) : Set n where
    testConstruct1 : TestData3 A B
    -- testConstruct2 : A → TestData3 A B -- Because of (_→_ : (Set _) → (Set _))?
    -- testConstruct3 : A →₂ (TestData3 A B)
    testConstruct4 : (A →₂ B) → (TestData3 A B)
  testFn : Type → Type
  testFn x = x

module testEqProof where
  open import Logic.Propositional{Lvl.𝟎}
  open import Numeral.Natural.Oper
  open import Relator.Equals{Lvl.𝟎}{Lvl.𝟎}
  open import Relator.Equals.Proofs{Lvl.𝟎}{Lvl.𝟎}
  open import Structure.Operator.Properties{Lvl.𝟎}
  open import Structure.Relator.Properties{Lvl.𝟎}{Lvl.𝟎}
  open import Type{Lvl.𝟎}

  minSkit : ⦃ _ : Absorberₗ (_⋅_) (0) ⦄ → ⦃ _ : Identityᵣ (_+_) (0) ⦄ → ∀{x} → (1 ≡ ((0 ⋅ x) + 1) + 0)
  minSkit ⦃ absorb ⦄ ⦃ id ⦄ {x} =
    ((congruence₁(_+ 1)
      ((symmetry (absorb {x})) :of: (0 ≡ 0 ⋅ x))
    ) :of: (1 ≡ (0 ⋅ x) + 1))
    🝖 ((symmetry id) :of: (_ ≡ ((0 ⋅ x) + 1) + 0))

module testDiv where
  open import Numeral.Natural.Oper
  open import Numeral.Natural.UnclosedOper
  open import Relator.Equals{Lvl.𝟎}{Lvl.𝟎}
  open import Relator.Equals.Proofs{Lvl.𝟎}{Lvl.𝟎}
  open import Structure.Relator.Properties{Lvl.𝟎}{Lvl.𝟎}

  testDiv1 : 4 ⌈/₀⌉ 2 ≡ 2
  testDiv1 = reflexivity

  testDiv2 : 2 ⌈/₀⌉ 2 ≡ 1
  testDiv2 = reflexivity

  testDiv3 : 1 ⌈/₀⌉ 2 ≡ 1
  testDiv3 = reflexivity

  -- test1 : ∀{f : ℕ → ℕ} → (f(0) ≡ 0) ∧ (∀{n : ℕ} → f(n + 1) ≡ f(n) + n + 1) → (∀{n : ℕ} → f(n) ≡ (n ⋅ (n + 1)) ⌈/₀⌉ 2)
  -- test1 ()

module testList where
  open import Data.List
  open import Relator.Equals{Lvl.𝟎}{Lvl.𝟎}
  open import Relator.Equals.Proofs{Lvl.𝟎}{Lvl.𝟎}
  open import Numeral.Natural

  -- rev1 : (4 ⊰ 3 ⊰ 2 ⊰ 1 ⊰ ∅) → reverse(1 ⊰ 2 ⊰ 3 ⊰ 4 ⊰ ∅)
  -- rev1 = id

  len1 : length{_}{ℕ}(1 ⊰ 2 ⊰ 3 ⊰ 4 ⊰ ∅) ≡ 4
  len1 = [≡]-intro

  testFoldᵣ : (foldᵣ{_}{_}{ℕ} (_⊰_) ∅ (1 ⊰ 2 ⊰ 3 ⊰ 4 ⊰ ∅)) ≡ (1 ⊰ 2 ⊰ 3 ⊰ 4 ⊰ ∅)
  testFoldᵣ = [≡]-intro

  testReduceOrᵣ0 : (reduceOrᵣ (_++_ {_}{ℕ}) (0 ⊰ ∅) ∅) ≡ (0 ⊰ ∅)
  testReduceOrᵣ0 = [≡]-intro

  testReduceOrᵣ1 : (reduceOrᵣ (_++_ {_}{ℕ}) (0 ⊰ ∅) ((1 ⊰ ∅) ⊰ ∅)) ≡ (1 ⊰ ∅)
  testReduceOrᵣ1 = [≡]-intro

  testReduceOrᵣ2 : (reduceOrᵣ (_++_ {_}{ℕ}) (0 ⊰ ∅) ((1 ⊰ ∅) ⊰ (2 ⊰ ∅) ⊰ (3 ⊰ ∅) ⊰ (4 ⊰ ∅) ⊰ ∅)) ≡ (1 ⊰ 2 ⊰ 3 ⊰ 4 ⊰ ∅)
  testReduceOrᵣ2 = [≡]-intro

module testTransitivity where
  open import Numeral.Natural
  open import Structure.Relator.Properties{Lvl.𝟎}{Lvl.𝟎}
  open import Relator.Equals{Lvl.𝟎}{Lvl.𝟎}
  open import Relator.Equals.Proofs{Lvl.𝟎}{Lvl.𝟎}
  open import Type

  test1 : (0 :of: ℕ ≡ 1) → (1 ≡ 2) → (0 ≡ 2)
  test1 (0≡1) (1≡2) = (0≡1) 🝖 (1≡2)

-- module testPropositionalLogic where
--   open import Functional
--   open import Logic.Propositional{Lvl.𝟎}
--   module Propositional = Logic.Classical.Propositional
--   open import Type{Lvl.𝟎}
--
--   symbols : ∀{T : Set(Lvl.𝟎)} → Propositional.Syntax.Symbols T (const (Set(Lvl.𝟎)))
--   symbols =
--     record {
--       •_ = typeOf ;
--       ⊤   = ⊤ ;
--       ⊥   = ⊥ ;
--       ¬_  = ¬_ ;
--       _∧_ = _∧_ ;
--       _∨_ = _∨_ ;
--       _⇒_ = _→ᶠ_ ;
--       _⇔_ = _↔_
--       -- _⊕_ = a ↦ b ↦ ((a ∨ b) ∧ ¬(a ∧ b))
--     }

module testListSublist where
  open import Functional
  open import Numeral.Natural
  open import Data.List
  import      List.Theorems
  open        List.Theorems{Lvl.𝟎}{Lvl.𝟎}
  open        List.Theorems.Sublist hiding (_⊑_)
  open import Type

  test1 : ([ 1 ]) ⊑ ([ 1 ] :of: List(ℕ))
  test1 = use(empty)

  test2 : ([ 1 ⊰ 2 ]) ⊑ ([ 1 ] :of: List(ℕ))
  test2 = (use ∘ skip)(empty)

  test3 : ([ 1 ⊰ 2 ]) ⊑ ([ 1 ⊰ 2 ] :of: List(ℕ))
  test3 = (use ∘ use)(empty)

  test4 : ([ 1 ⊰ 10 ⊰ 2 ]) ⊑ ([ 1 ⊰ 2 ] :of: List(ℕ))
  test4 = (use ∘ skip ∘ use)(empty)

  test5 : ([ 1 ⊰ 10 ⊰ 2 ⊰ 3 ]) ⊑ ([ 1 ⊰ 2 ⊰ 3 ] :of: List(ℕ))
  test5 = (use ∘ skip ∘ use ∘ use)(empty)

  test6 : ([ 1 ⊰ 10 ⊰ 2 ⊰ 3 ⊰ 20 ⊰ 30 ⊰ 4 ⊰ 40 ]) ⊑ ([ 1 ⊰ 2 ⊰ 3 ⊰ 4 ] :of: List(ℕ))
  test6 = (use ∘ skip ∘ use ∘ use ∘ skip ∘ skip ∘ use ∘ skip)(empty)

module testPrimitiveRecursiveDefinitions where
  open import   Data
  import        Function.PrimitiveRecursion
  open          Function.PrimitiveRecursion
  open          Function.PrimitiveRecursion.OperShortcut
  open import   Numeral.Natural
  import Numeral.Natural.Oper     as Nat
  import Numeral.Natural.Function as Nat
  open import   Relator.Equals{Lvl.𝟎}{Lvl.𝟎}
  open import   Relator.Equals.Proofs{Lvl.𝟎}{Lvl.𝟎}

  plus   = Rec(2) (P(1)(0)) (Comp(1)(3) (Succ) (P(3)(1)))
  pred   = Rec(1) (Zero) (P(2)(0))
  monus  = Comp(2)(2) (Rec(2) (P(1)(0)) (Comp(1)(3) (pred) (P(3)(1)))) (P(2)(1) , P(2)(0))
  max    = Comp(2)(2) (plus) (P(2)(0) , Comp(2)(2) (monus) (P(2)(1) , P(2)(0)))
  min    = Comp(2)(2) (monus) (plus , max)
  iszero = Rec(1) (Comp(1)(0) (Succ) (Zero)) (Comp(0)(2) (Zero) <>)
  const3 = Comp(1)(0) (Succ) (Comp(1)(0) (Succ) (Comp(1)(0) (Succ) (Zero)))

  -- testPlus1 : evaluate plus(4 , 2) ≡ 6
  -- testPlus1 = [≡]-intro

  -- testMonus1 : evaluate monus(4 , 0) ≡ 4
  -- testMonus1 = [≡]-intro

  -- testMonus2 : evaluate monus(0 , 4) ≡ 0
  -- testMonus2 = [≡]-intro

  -- testMonus3 : evaluate monus(10 , 2) ≡ 8
  -- testMonus3 = [≡]-intro

  -- testMonus4 : evaluate monus(2 , 10) ≡ 0
  -- testMonus4 = [≡]-intro

  -- testMin1 : evaluate min(3 , 2) ≡ Nat.min(3)(2)
  -- testMin1 = [≡]-intro

  proofPred : ∀{n} → evaluate pred(n) ≡ 𝐏(n)
  proofPred{𝟎}    = [≡]-intro
  proofPred{𝐒(n)} = [≡]-intro

  proofPlus : ∀{a b} → evaluate plus(b , a) ≡ (a Nat.+ b)
  proofPlus{𝟎}   {𝟎}    = [≡]-intro
  proofPlus{𝐒(_)}{𝟎}    = [≡]-intro
  proofPlus{a}   {𝐒(b)} = congruence₁(𝐒) (proofPlus{a}{b})

  is-zero : ℕ → ℕ
  is-zero(0) = 1
  is-zero(_) = 0

  proofIsZero : ∀{n} → evaluate iszero(n) ≡ is-zero(n)
  proofIsZero{𝟎}    = [≡]-intro
  proofIsZero{𝐒(_)} = [≡]-intro

  proofMonus : ∀{a} → evaluate monus(a , 𝟎) ≡ (a Nat.−₀ 𝟎)
  proofMonus{𝟎} = [≡]-intro
  proofMonus{_} = [≡]-intro

  proofMax : ∀{a} → evaluate max(0 , a) ≡ Nat.max(a)(0)
  proofMax{𝟎}    = [≡]-intro
  proofMax{𝐒(_)} = [≡]-intro

  -- proofMin : ∀{a} → evaluate min(0 , a) ≡ Nat.min(a)(0)
  -- proofMin{𝟎}    = [≡]-intro
  -- proofMin{𝐒(_)} = [≡]-intro

module testEq where
  -- testEqInstance : ∀{T} ⦃ _ : Equivalence {T} (_≡_ {T}) ⦄ → Symmetry {T} (_≡_ {T})
  -- testEqInstance ⦃ eq ⦄ = Equivalence.symmetry eq
  -- testEqInstance2 : ∀{T} → Symmetry {T} (_≡_ {T})
  -- testEqInstance2 = testEqInstance

  -- testSymInstance : ∀{T} ⦃ _ : Symmetry {T} (_≡_ {T}) ⦄ → Symmetry {T} (_≡_ {T})
  -- testSymInstance ⦃ sym ⦄ = sym

module testExistential where
  -- TODO
  -- testExists : ∀{T : Type}{f : T → Type} → (∃[ x ∈ T ] (f x)) → (∃ {T} (x ↦ f x))
  -- testExists x = x

module testCantor where
  import      Boolean
  open        Boolean
  import      Data.Boolean.Operators
  open        Data.Boolean.Operators.Programming
  open import Functional
  open import Logic.Propositional{Lvl.𝟎}
  open import Logic.Predicate{Lvl.𝟎}{Lvl.𝟎}
  open import Logic.DiagonalProof{Lvl.𝟎}{Lvl.𝟎}
  open import Numeral.Natural
  open import Numeral.Natural.Relation.Countable{Lvl.𝟎}{Lvl.𝟎}
  open import Relator.Bijection{Lvl.𝟎}{Lvl.𝟎}
  open import Relator.Equals {Lvl.𝟎}{Lvl.𝟎}
  open import Type{Lvl.𝟎}

  BitSequence           = (ℕ → Bool)
  CountableBitSequences = (ℕ → BitSequence)

  -- ∀l∃seq∀n. l(n)(n)≠seq(n)
  -- There is a bit sequence that is not in the countable list of bit sequences
  bitSequenceCantor : (l : CountableBitSequences) → ∃{BitSequence}(seq ↦ ∀{n : ℕ} → (l(n)(n) ≢ seq(n)))
  bitSequenceCantor = diagonal-proof (!_) ([!]-unequality) where
    [!]-unequality : ∀{b : Bool} → (b ≢ ! b)
    [!]-unequality {𝑇} ()
    [!]-unequality {𝐹} ()

  -- uncountableProof : CountableBitSequences → ¬(Countable(BitSequence))
  -- uncountableProof (l) ([∃]-intro(seq-to-n) ⦃ inj ⦄) =
  --   [∃]-elim f (bitSequenceCantor(l)) where
  --     postulate f : ∀{seq}{x : ℕ → Bool} → {n : ℕ} → (l n n ≢ x n) → ⊥ -- ∀{T}{seq}{n : ℕ} → (l(n)(n) ≢ seq(n)) → T
  --     f : ∀{_}{_}(₎
  --     f{_}{n}(lnn≢seqn) = lnn≢seqn ∘ inj
  -- Countable: ∃(seq-to-n: (ℕ → Bool) → ℕ)∀(x₁ : ℕ → Bool)∀(x₂: ℕ → Bool). (seq-to-n(seq₁)=seq-to-n(seq₂)) → (seq₁=seq₂)

module testListSets where
  open import Functional
  open import Data.List
  import      Data.List.Relation.Membership
  open        Data.List.Relation.Membership{Lvl.𝟎}
  open        Data.List.Relation.Membership.[∈]-proof
  open import Logic.Propositional
  open import Type{Lvl.𝟎}

  -- TODO: Probably incorrectly formulated
  -- Example:
  --   (∀a. a∈{P,Q} → R)
  --   P → Q → R
  -- [∈]-list : ∀{L : List(Type)}{Out : Type} → (∀{a} → (a ∈ L) → Out) → (foldᵣ (_→ᶠ_) (Out) (L))
  -- [∈]-list{∅}(f) = f ∘ [⊥]-elim ∘ [∉]-empty
  -- f            : ∀{a} → (a ∈ ∅) → Out
  -- f ∘ [⊥]-elim : ⊥ → Out

  -- [∈]-list : ∀{L : List(Type)}{Out : Type} → (foldᵣ (_→ᶠ_) (Out) (L)) → (∀{a} → (a ∈ L) → Out)
  -- [∈]-list{∅}     (out) (a∈∅)   = out
  -- [∈]-list{x ⊰ l} (f)   (a∈x⊰l) = [∈]-list{l} (f)

module testFinite where
  open import Numeral.FiniteInclusive

  test2-0 : ℕfin(2)
  test2-0 = 𝟎fin

  test2-1 : ℕfin(2)
  test2-1 = 𝐒fin(𝟎fin)

  test2-2 : ℕfin(2)
  test2-2 = 𝐒fin(𝐒fin(𝟎fin))

  -- test2-3 : ℕfin(2)
  -- test2-3 = 𝐒fin(𝐒fin(𝐒fin(𝟎fin)))

  -- test2-4 : ℕfin(2)
  -- test2-4 = 𝐒fin(𝐒fin(𝐒fin(𝐒fin(𝟎fin))))

module testResolveInstance where
  open import Functional
  open import Data.List
  open import Numeral.Natural
  open import Type

  data _∈_ {T : Set} (x : T) : List(T) → Set where
    instance
      𝟎 : ∀{l} → x ∈ (x ⊰ l)
      𝐒 : ∀{l}{y} → (x ∈ l) → (x ∈ (y ⊰ l))

  test1 : 2 ∈ ((1 ⊰ 2 ⊰ 3 ⊰ 4 ⊰ ∅) :of: List(ℕ))
  test1 = resolve(_)  -- Becomes 𝐒(𝐒(𝟎))

module testPureSet where
  open import Logic.Propositional{Lvl.𝟎}

  -- TODO: Does not seem to work. Undefinable because of positivity requirement
  data PureSet : Set₁ where
    ∅ : PureSet
    _∪_ : PureSet → PureSet → PureSet
    ℘ : PureSet → PureSet
    -- subset : PureSet → (PureSet → Stmt) → PureSet

  data _∈_ (x : PureSet) : PureSet → Set₀ where
    empty : ⊥ → (x ∈ ∅)
    union : ∀{s₁ s₂} → (x ∈ s₁)∨(x ∈ s₂) → (x ∈ (s₁ ∪ s₂))
    -- power : ∀{s} → (∀{y} → (y ∈ x) → (y ∈ s)) → (x ∈ ℘(s))

{- TODO: Stuck
module testInstanceResolution where
  open import Logic.Propositional{Lvl.𝟎}
  open import Functional

  postulate A₁ : Set → Set
  postulate A₂ : Set

  instance postulate test0 : ∀{x}{y} → ⦃ _ : x ← y ⦄ → ⦃ _ : x → y ⦄ → (x ↔ y)
  instance postulate test1 : A₁(A₂) ← A₁(A₂)
  instance postulate test2 : A₁(A₂) → A₁(A₂)

  B = A₁(A₂) ↔ A₁(A₂)
  f : (B → ⊤) → ⊤
  f(g) = g(resolve(B))
-}

module inferAbstract where
  open import Functional

  postulate A : Set -> Set

  abstract -- TODO: This pattern could be a macro? See http://agda.readthedocs.io/en/v2.5.3/language/reflection.html for docs and https://github.com/asr/my-agda/blob/4ef826275053a502075e66de7a5cc77964b4291c/test/Succeed/UnquoteDef.agda for examples of macros
    Test = ∀{a} → A(a) → A(a)

    Test-elim : Test → ∀{a} → A(a) → A(a)
    Test-elim(x) = x

  instance
    postulate test2 : Test

  postulate test3 : Test → Test

  test4 : Test
  test4 = test3(infer)

module testDomainRaise where
  open import Function.DomainRaise
  open import Data.List
  open import Numeral.Natural
  open import Numeral.Finite
  open import Numeral.Natural.Oper
  open import Syntax.Number
  open import Relator.Equals {Lvl.𝟎}{Lvl.𝟎}

  f : (ℕ →̂ List(ℕ))(3)
  f a b c = (a ⋅ 10) ⊰ (b ⋅ 100) ⊰ (c ⋅ 1000) ⊰ ∅

  testApplyRepeated : applyRepeated{Lvl.𝟎}{Lvl.𝟎}{3}(f)(1) ≡ 10 ⊰ 100 ⊰ 1000 ⊰ ∅
  testApplyRepeated = [≡]-intro

  g : 𝕟(3) → ℕ
  g(𝐒(𝐒(𝟎))) = 1
  g(𝐒(𝟎))    = 2
  g(𝟎)       = 3

  testApplyFn : applyFn{Lvl.𝟎}{Lvl.𝟎}{3}(f)(g) ≡ 10 ⊰ 200 ⊰ 3000 ⊰ ∅
  testApplyFn = [≡]-intro

  testOn : _on_{Lvl.𝟎}{Lvl.𝟎}{Lvl.𝟎}{3} (𝐒) f 1 2 3 ≡ (𝐒(1) ⋅ 10) ⊰ (𝐒(2) ⋅ 100) ⊰ (𝐒(3) ⋅ 1000) ⊰ ∅
  testOn = [≡]-intro

  testNaryL1 : naryₗ{Lvl.𝟎}{2}{List(ℕ)}(_++_) (0 ⊰ ∅) (1 ⊰ ∅) (2 ⊰ ∅) (3 ⊰ ∅) ≡ 0 ⊰ 1 ⊰ 2 ⊰ 3 ⊰ ∅
  testNaryL1 = [≡]-intro

  testNaryL2 : naryₗ{Lvl.𝟎}{2}{ℕ}(_−₀_) (12) (5) (2) (1) ≡ ((12 −₀ 5) −₀ 2) −₀ 1
  testNaryL2 = [≡]-intro
  -- 12−(5−(2−1)) = 8
  -- (((12−5)−2)−1) = 4

  testNaryR1 : naryᵣ{Lvl.𝟎}{2}{List(ℕ)}(_++_) (0 ⊰ ∅) (1 ⊰ ∅) (2 ⊰ ∅) (3 ⊰ ∅) ≡ 0 ⊰ 1 ⊰ 2 ⊰ 3 ⊰ ∅
  testNaryR1 = [≡]-intro

  testNaryR2 : naryᵣ{Lvl.𝟎}{2}{ℕ}(_−₀_) (12) (5) (2) (1) ≡ 12 −₀ (5 −₀ (2 −₀ 1))
  testNaryR2 = [≡]-intro

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 --type-in-type --without-K #-}

{- Semi-simplicial types: A small demonstration that the "usual approach"
   works if we postulate the required coherence for the functorial behaviour
   of the "Skeleton" functor.
   This coherence can be achieved in a 2-level system, where the required
   functor law can be shown to hold strictly. -}

module nicolai.SemiSimp.SStypes where

open import lib.Basics
open import lib.types.Unit
open import lib.types.Nat

-- This is the usual lemma about equality of pairs
-- (ideally, it should be imported from lib.types.Sigma )
pair== : {A : Set}{B : A → Set}{ab ab' : Σ A B}
     → (Σ (fst ab == fst ab') (λ α → transport B α (snd ab) == snd ab')) → ab == ab'
pair== {ab = (a , b)}{ab' = (.a , .b)} ( idp , idp ) = idp

-- Finite types
data Fin : ℕ → Set where
  fz : {n : ℕ} → Fin (S n)
  fs : {n : ℕ} → Fin n → Fin (S n)

_>fin_ : {n : ℕ} → (i j : Fin n) → Set
fz >fin i = Empty
fs j >fin fz = ⊤
fs j >fin fs i = j >fin i

-- The category Δ₊ can be implemented such that the categorical laws
-- (unit, associativity) hold strictly (see my thesis).
-- Objects are natural numbers.

is-increasing : {m n : ℕ} → (Fin m → Fin n) → Set
is-increasing {m} {n} f = {j i : Fin m} → (j >fin i) → ((f j) >fin (f i))

-- hom-sets of Δ₊

_⇒+_ : ℕ → ℕ → Set
m ⇒+ n = Σ (Fin (S m) → Fin (S n)) is-increasing

-- composition:

_∘+_ : {l m n : ℕ} → (m ⇒+ n) → (l ⇒+ m) → (l ⇒+ n)
(g , p₂) ∘+ (f , p₁) = (λ i → g(f(i))) , (λ p → p₂ (p₁ p))

-- general lemmas (possibly in the library, should be added if they are not there)

trans-ap : {A B : Set} → (f : B → A) → (F : A → Set) → {b₁ b₂ : B} → (p : b₁ == b₂) → (x : F (f b₁)) → (transport (λ b → F (f b)) p x) == (transport F (ap f p) x)
trans-ap f F idp x = idp

trans-λ : {A B : Set} → (F : A → B → Set) → {a₁ a₂ : A} → (f : (b : B) → F a₁ b) → (p : a₁ == a₂) → transport (λ a → (b : B) → F a b) p f == λ b → transport (λ a → F a b) p (f b)
trans-λ F f idp = idp

-- Semi-simplicial types

-- SST j is the type of (j-1)-truncated semi-simplicial types, i.e. "Σ X₀ Σ ... Xⱼ₋₁"
SST : ℕ → Set

-- skeleton of a k-simplex: cells lower (!) than level j
Sk : {j : ℕ} → (SST j) → (k : ℕ) → Set

Skm : {j : ℕ} → (X : SST j) → {k₁ k₂ : ℕ} → (k₁ ⇒+ k₂) → Sk {j = j} X k₂ → Sk {j = j} X k₁

Skm-∘ : {j : ℕ} → (X : SST j) → {k₁ k₂ k₃ : ℕ} → (f : k₁ ⇒+ k₂) → (g : k₂ ⇒+ k₃) → (x : Sk X k₃) → Skm X (g ∘+ f) x == Skm X f (Skm X g x)

-- We postulate that Skm is coherent. This is automatic if we use equality with K.
-- We want to demonstrate that the "usual" construction of semi-simplicial types
-- (the one that many people have tried; see Herbelin's paper) works if we can
-- somehow get this coherence.
-- Of course, this is not new (see e.g. Herbelin).

postulate
  Skm-∘-coh :  {j : ℕ} → (X : SST j) → {k₀ k₁ k₂ k₃ : ℕ} → (h : k₀ ⇒+ k₁) → (f : k₁ ⇒+ k₂) → (g : k₂ ⇒+ k₃) → (x : Sk X k₃)
                → ((Skm-∘ X h (g ∘+ f) x) ∙ (ap (Skm X h) (Skm-∘ X f g x)))
                  ==
                  (Skm-∘ X (f ∘+ h) g x) ∙ (Skm-∘ X h f (Skm X g x))

SST O = ⊤
SST (S j) = Σ (SST j) λ X →
               Sk X j → Set

Sk {O} ⋆ k = ⊤
Sk {S j} (X , Fibʲ) k = Σ (Sk {j} X k) λ sk →
                           (f : j ⇒+ k) → Fibʲ (Skm X f sk)

Skm {O} ⋆ f sk = ⋆
Skm {S j} (X , Fibʲ) f (x , fibs) = Skm {j} X f x , λ g → transport Fibʲ (Skm-∘ X g f x) (fibs (f ∘+ g))

Skm-∘ {O} ⊤ f g x = idp
Skm-∘ {S j} (X , Fibʲ) {k₁} {k₂} {k₃} f g (x , fibs) =

    Skm (X , Fibʲ) (g ∘+ f) (x , fibs)

  =⟨ idp ⟩

    Skm X (g ∘+ f) x , (λ h → transport Fibʲ (Skm-∘ X h (g ∘+ f) x) (fibs ((g ∘+ f) ∘+ h)))

  =⟨ pair== (Skm-∘ X f g x , idp) ⟩

    Skm X f (Skm X g x)  ,  transport (λ y → (h : j ⇒+ k₁) → Fibʲ (Skm X h y)) (Skm-∘ X f g x) (λ h → transport Fibʲ (Skm-∘ X h (g ∘+ f) x) (fibs ((g ∘+ f) ∘+ h)))

  =⟨ idp ⟩

    Skm X f (Skm X g x)  ,  transport  (λ y → (h : j ⇒+ k₁) → Fibʲ (Skm X h y))  (Skm-∘ X f g x)  (λ h → transport Fibʲ (Skm-∘ X h (g ∘+ f) x) (fibs ((g ∘+ f) ∘+ h)))

  =⟨ pair== (idp , trans-λ {B = j ⇒+ k₁} (λ y h → Fibʲ (Skm X h y))
                                       (λ h → transport Fibʲ (Skm-∘ X h (g ∘+ f) x) (fibs ((g ∘+ f) ∘+ h)))
                                       (Skm-∘ X f g x)) ⟩

    Skm X f (Skm X g x)  ,  (λ (h : j ⇒+ k₁) → transport  (λ y → Fibʲ (Skm X h y))  (Skm-∘ X f g x)  (transport Fibʲ (Skm-∘ X h (g ∘+ f) x) (fibs ((g ∘+ f) ∘+ h))))

  =⟨ pair== (idp , λ= (λ (h : j ⇒+ k₁) → trans-ap (Skm X h) Fibʲ (Skm-∘ X f g x) (transport Fibʲ (Skm-∘ X h (g ∘+ f) x) (fibs ((g ∘+ f) ∘+ h)))  )) ⟩

    Skm X f (Skm X g x)  ,  (λ (h : j ⇒+ k₁) → transport  Fibʲ (ap (Skm X h) (Skm-∘ X f g x))  (transport Fibʲ (Skm-∘ X h (g ∘+ f) x) (fibs ((g ∘+ f) ∘+ h))))

  =⟨ pair== (idp , λ= (λ (h : j ⇒+ k₁) → ! (trans-∙ ((Skm-∘ X h (g ∘+ f) x)) ((ap (Skm X h) (Skm-∘ X f g x))) _))) ⟩

    Skm X f (Skm X g x)  ,  (λ (h : j ⇒+ k₁) → transport  Fibʲ ((Skm-∘ X h (g ∘+ f) x) ∙ (ap (Skm X h) (Skm-∘ X f g x))) (fibs ((g ∘+ f) ∘+ h)))

  =⟨ pair== (idp , λ= (λ (h : j ⇒+ k₁) → ap (λ p → transport Fibʲ p (fibs ((g ∘+ f) ∘+ h))) (Skm-∘-coh X h f g _ ))) ⟩ -- crucial step that requires coherence! Easy with equality that has K.

    Skm X f (Skm X g x)  ,  (λ (h : j ⇒+ k₁) → transport Fibʲ  ((Skm-∘ X (f ∘+ h) g x) ∙ (Skm-∘ X h f (Skm X g x))) (fibs ((g ∘+ f) ∘+ h)))

  =⟨ pair== (idp ,  λ= (λ (h : j ⇒+ k₁) → trans-∙ (Skm-∘ X (f ∘+ h) g x) ((Skm-∘ X h f (Skm X g x))) (fibs ((g ∘+ f) ∘+ h))) ) ⟩  -- functoriality of transport; very simple. Uses funext.

    Skm X f (Skm X g x)  ,  (λ (h : j ⇒+ k₁) → transport Fibʲ  (Skm-∘ X h f (Skm X g x)) (transport Fibʲ (Skm-∘ X (f ∘+ h) g x) (fibs ((g ∘+ f) ∘+ h))))

  =⟨ idp ⟩  -- nothing happening here, only formatting

    Skm X f (Skm X g x) , (λ h → transport Fibʲ (Skm-∘ X h f (Skm X g x)) (transport Fibʲ (Skm-∘ X (f ∘+ h) g x) (fibs ((g ∘+ f) ∘+ h))))

  =⟨ idp ⟩ -- at this point, we use the strictness of Δ₊ in Agda!

    Skm X f (Skm X g x) , (λ h → transport Fibʲ (Skm-∘ X h f (Skm X g x)) (transport Fibʲ (Skm-∘ X (f ∘+ h) g x) (fibs (g ∘+ (f ∘+ h)))))

  =⟨ idp ⟩

    Skm (X , Fibʲ) f (Skm X g x , λ h' → transport Fibʲ (Skm-∘ X h' g x) (fibs (g ∘+ h')))

  =⟨ idp ⟩

    Skm (X , Fibʲ) f (Skm (X , Fibʲ) g (x , fibs))

  ∎

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
record R : Set₁ where
  field
    _A : Set

P : Set → Set₁
P R.A = Set


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Vec.Properties where

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

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat
open import Cubical.Data.Vec.Base
open import Cubical.Data.FinData
open import Cubical.Relation.Nullary

private
  variable
    ℓ : Level
    A : Type ℓ

-- This is really cool!
-- Compare with: https://github.com/agda/agda-stdlib/blob/master/src/Data/Vec/Properties/WithK.agda#L32
++-assoc : ∀ {m n k} (xs : Vec A m) (ys : Vec A n) (zs : Vec A k) →
           PathP (λ i → Vec A (+-assoc m n k (~ i))) ((xs ++ ys) ++ zs) (xs ++ ys ++ zs)
++-assoc {m = zero} [] ys zs = refl
++-assoc {m = suc m} (x ∷ xs) ys zs i = x ∷ ++-assoc xs ys zs i

-- Equivalence between Fin n → A and Vec A n

FinVec : (A : Type ℓ) (n : ℕ) → Type ℓ
FinVec A n = Fin n → A

FinVec→Vec : {n : ℕ} → FinVec A n → Vec A n
FinVec→Vec {n = zero}  xs = []
FinVec→Vec {n = suc _} xs = xs zero ∷ FinVec→Vec (λ x → xs (suc x))

Vec→FinVec : {n : ℕ} → Vec A n → FinVec A n
Vec→FinVec xs f = lookup f xs

FinVec→Vec→FinVec : {n : ℕ} (xs : FinVec A n) → Vec→FinVec (FinVec→Vec xs) ≡ xs
FinVec→Vec→FinVec {n = zero} xs = funExt λ f → ⊥.rec (¬Fin0 f)
FinVec→Vec→FinVec {n = suc n} xs = funExt goal
  where
  goal : (f : Fin (suc n))
       → Vec→FinVec (xs zero ∷ FinVec→Vec (λ x → xs (suc x))) f ≡ xs f
  goal zero = refl
  goal (suc f) i = FinVec→Vec→FinVec (λ x → xs (suc x)) i f

Vec→FinVec→Vec : {n : ℕ} (xs : Vec A n) → FinVec→Vec (Vec→FinVec xs) ≡ xs
Vec→FinVec→Vec {n = zero}  [] = refl
Vec→FinVec→Vec {n = suc n} (x ∷ xs) i = x ∷ Vec→FinVec→Vec xs i

FinVecIsoVec : (n : ℕ) → Iso (FinVec A n) (Vec A n)
FinVecIsoVec n = iso FinVec→Vec Vec→FinVec Vec→FinVec→Vec FinVec→Vec→FinVec

FinVec≃Vec : (n : ℕ) → FinVec A n ≃ Vec A n
FinVec≃Vec n = isoToEquiv (FinVecIsoVec n)

FinVec≡Vec : (n : ℕ) → FinVec A n ≡ Vec A n
FinVec≡Vec n = ua (FinVec≃Vec n)

isContrVec0 : isContr (Vec A 0)
isContrVec0 = [] , λ { [] → refl }

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
open import Agda.Primitive using (_⊔_ ; lsuc ; Level)

import Categories.Category as Category
import Categories.Category.Cartesian as Cartesian
open import Categories.Object.Terminal using (Terminal)
open import Categories.Object.Product using (Product)

open import MultiSorted.AlgebraicTheory
open import MultiSorted.Substitution
import MultiSorted.Product as Product
import MultiSorted.Interpretation as Interpretation
import MultiSorted.Model as Is-Model
import MultiSorted.InterpretationCategory as InterpretationCategory

module MultiSorted.ModelCategory
         {ℓt o ℓ e}
         {𝓈 ℴ}
         {Σ : Signature {𝓈} {ℴ}}
         (T : Theory ℓt Σ)
         {𝒞 : Category.Category o ℓ e}
         (cartesian-𝒞 : Cartesian.Cartesian 𝒞) where
  open Signature Σ
  open Theory T
  open Category.Category 𝒞
  open Interpretation Σ cartesian-𝒞
  open Is-Model {o = o} {ℓ = ℓ} {e = e} {Σ = Σ} T

  -- Useful shortcuts for levels
  ℓℴ : Level
  ℓℴ = lsuc (o ⊔ ℓ ⊔ e ⊔ 𝓈 ⊔ ℴ ⊔ ℓt)

  ℓ𝒽 : Level
  ℓ𝒽 = ℓ ⊔ o ⊔ e ⊔ 𝓈 ⊔ ℴ

  ℓ𝓇 : Level
  ℓ𝓇 = e ⊔ 𝓈

  -- New definition of models (as a set, not only a property of interpretations)
  record Model : Set ℓℴ where
    field
      interpretation : Interpretation
      is-model : Is-Model.Is-Model T interpretation

  open Model

  -- Homomorphisms of models
  _⇒M_ : ∀ (M N : Model) → Set ℓ𝒽
  _⇒M_ M N = (interpretation M) ⇒I (interpretation N)

  -- Equality of homomorphisms of models (the same as for the interpretations)
  _≈M_ : ∀ {M N : Model} → M ⇒M N → M ⇒M N → Set ℓ𝓇
  _≈M_ {M} {N} ϕ ψ =
                   let open _⇒I_ in
                   ∀ A → (hom-morphism ϕ {A}) ≈ (hom-morphism ψ)

  -- The identity morphism on models
  id-M : (M : Model) → M ⇒M M
  id-M = λ M → id-I {interpretation M}

  -- Composition of morphisms of Models
  _∘M_ : ∀ {M N O : Model} →  N ⇒M O → M ⇒M N → M ⇒M O
  _∘M_ ϕ ψ = ϕ ∘I ψ

  -- The category of Models of Σ in 𝒞
  ℳ : Category.Category ℓℴ ℓ𝒽 ℓ𝓇
  ℳ = record
          { Obj = Model
          ; _⇒_ = _⇒M_
          ; _≈_ = λ {M} {N} ϕ ψ → _≈M_ {M} {N} ϕ ψ
          ; id = λ {M} → id-M M
          ; _∘_ = λ {M} {N} {O} ϕ ψ → _∘M_ {M} {N} {O} ϕ ψ
          ; assoc = λ A → assoc -- λ A → assoc
          ; sym-assoc = λ A → sym-assoc
          ; identityˡ = λ A → identityˡ
          ; identityʳ = λ A → identityʳ
          ; identity² = λ A → identity²
          ; equiv = record { refl = λ A → Equiv.refl
                           ; sym = λ p A → Equiv.sym (p A)
                           ; trans = λ p₁ p₂ A → Equiv.trans (p₁ A) (p₂ A)
                           }
          ; ∘-resp-≈ = λ p₁ p₂ A → ∘-resp-≈ (p₁ A) (p₂ A)
          }

  -- The product of "Model proofs"

  module _ (M N : Model) where
    open Product.Producted
    open HomReasoning
    open InterpretationCategory
    open Cartesian.Cartesian cartesian-𝒞
    open Interpretation.Interpretation
    open import Categories.Object.Product.Morphisms {o} {ℓ} {e} 𝒞
    open Equation

    -- A proof that an axiom holds in a product interpretation amounts to a apir of proofs that the axiom holds in each model
    is-model-pairs : ∀ ε → (interp-term (interpretation M) (Equation.eq-lhs (ax-eq ε)) ⁂  interp-term (interpretation N) (Equation.eq-lhs (ax-eq ε)))
                               ≈ (interp-term (interpretation M) (Equation.eq-rhs (ax-eq ε)) ⁂  interp-term (interpretation N) (Equation.eq-rhs (ax-eq ε))) →
                               Interpretation.interp-term (A×B-ℐ𝓃𝓉 Σ cartesian-𝒞 (interpretation M) (interpretation N)) (Equation.eq-lhs (ax-eq ε))
                               ≈ Interpretation.interp-term (A×B-ℐ𝓃𝓉 Σ cartesian-𝒞 (interpretation M) (interpretation N)) (Equation.eq-rhs (ax-eq ε))
    is-model-pairs ε p =
                            begin
                              Interpretation.interp-term
                                (A×B-ℐ𝓃𝓉 Σ cartesian-𝒞 (interpretation M) (interpretation N))
                                (Equation.eq-lhs (ax-eq ε)) ≈⟨ ⟺
                                                                 (Cartesian.Cartesian.unique cartesian-𝒞
                                                                   (natural-π₁ Σ cartesian-𝒞 {I = interpretation M} {interpretation N} (ax-lhs ε))
                                                                   (natural-π₂ Σ cartesian-𝒞 {I = interpretation M} {interpretation N} (ax-lhs ε))) ⟩
                              product.⟨
                                Interpretation.interp-term (interpretation M) (eq-lhs (ax-eq ε)) ∘
                                π₁
                                ,
                                Interpretation.interp-term (interpretation N) (eq-lhs (ax-eq ε)) ∘
                                π₂
                                ⟩ ≈⟨ ⟨⟩-cong₂ (∘-resp-≈ˡ (Is-Model.model-eq (is-model M) ε)) (∘-resp-≈ˡ (Is-Model.model-eq (is-model N) ε)) ⟩
                              product.⟨
                                Interpretation.interp-term (interpretation M) (eq-rhs (ax-eq ε)) ∘
                                π₁
                                ,
                                Interpretation.interp-term (interpretation N) (eq-rhs (ax-eq ε)) ∘
                                π₂
                                ⟩ ≈⟨ Cartesian.Cartesian.unique cartesian-𝒞
                                     (natural-π₁ Σ cartesian-𝒞 {I = interpretation M} {interpretation N} (ax-rhs ε))
                                     (natural-π₂ Σ cartesian-𝒞 {I = interpretation M} {interpretation N} (ax-rhs ε)) ⟩
                              Interpretation.interp-term
                                (A×B-ℐ𝓃𝓉 Σ cartesian-𝒞 (interpretation M) (interpretation N))
                                (eq-rhs (ax-eq ε)) ∎

    -- The proof that the product interpetation of two models is a model
    is-model-product : Is-Model (A×B-ℐ𝓃𝓉 Σ cartesian-𝒞 (interpretation M) (interpretation N))
    Is-Model.model-eq is-model-product ε =
                                           begin
                                             Interpretation.interp-term
                                               (A×B-ℐ𝓃𝓉 Σ cartesian-𝒞 (interpretation M) (interpretation N))
                                               (Equation.eq-lhs (ax-eq ε)) ≈⟨ is-model-pairs ε (⁂-cong₂ (Is-Model.model-eq (is-model M) ε) (Is-Model.model-eq (is-model N) ε)) ⟩
                                             Interpretation.interp-term
                                               (A×B-ℐ𝓃𝓉 Σ cartesian-𝒞 (interpretation M) (interpretation N))
                                               (Equation.eq-rhs (ax-eq ε)) ∎

  -- The product of ℐ𝓃𝓉 carries over the models : the product of two models is a model
  module _ (M N : Model) where
    open Product.Producted
    open HomReasoning
    open InterpretationCategory
    A×B-ℳ : Model
    A×B-ℳ = record
              { interpretation = A×B-ℐ𝓃𝓉 Σ cartesian-𝒞 (interpretation M) (interpretation N)
              ; is-model = is-model-product M N
              }

  -- The cartesian structure of the category of models

  module _ {M N : Model} where
    import Categories.Object.Product.Core
    open Categories.Object.Product.Core.Product
    open InterpretationCategory Σ cartesian-𝒞
    private
      UM UN : Interpretation
      UM = interpretation M
      UN = interpretation N
      UM×UN : Product ℐ𝓃𝓉 UM UN
      UM×UN = product-ℐ𝓃𝓉
    product-ℳ : Product ℳ M N
    -- Structure
    A×B      product-ℳ = A×B-ℳ M N
    π₁       product-ℳ = π₁    UM×UN
    π₂       product-ℳ = π₂    UM×UN
    ⟨_,_⟩    product-ℳ = ⟨_,_⟩ UM×UN
    -- Properties
    project₁ product-ℳ {O} {h} {i}     = project₁ UM×UN {interpretation O} {h} {i}
    project₂ product-ℳ {O} {h} {i}     = project₂ UM×UN {interpretation O} {h} {i}
    unique   product-ℳ {O} {h} {i} {j} = unique   UM×UN {interpretation O} {h} {i} {j}

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
-- Andreas, 2017-08-14, issue #2682, test case by Ulf

-- WAS: CheckInternal treats abstract projections as not in scope,
-- while the type checker allows them.

-- Adapted solution: allow also in CheckInternal

-- {-# OPTIONS -v tc.rec.proj:20 #-}
-- {-# OPTIONS -v tc.deftype:25 #-}
-- {-# OPTIONS -v tc:20 #-}

abstract
  record R : Set₁ where
    field X : Set

works : R → Set
works r = R.X r

test : R → Set
test r = {!R.X r!}

-- WAS: On give:
-- Expected non-abstract record type, found R
-- when checking that the expression R.X r has type Set

test2 : R → Set
test2 r = {! r .X !}
  where open R


text:
module CoprodMonad where

open import functor
open import monad

data PlusT (t₁ t₂ : Set → Set) (a : Set) (p₁ : Triple t₁)(p₂ : Triple t₂) : Set where
  T₁ : (t₁ (PlusT t₁ t₂ a p₁ p₂)) → PlusT t₁ t₂ a p₁ p₂

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Instances.CommRings where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure

open import Cubical.Data.Unit
open import Cubical.Data.Sigma

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FiberedProduct
open import Cubical.Algebra.CommRing.Instances.Unit

open import Cubical.Categories.Category
open import Cubical.Categories.Limits.Terminal
open import Cubical.Categories.Limits.Pullback

open Category hiding (_∘_)
open CommRingHoms

private
  variable
    ℓ : Level

CommRingsCategory : Category (ℓ-suc ℓ) ℓ
ob CommRingsCategory                     = CommRing _
Hom[_,_] CommRingsCategory               = CommRingHom
id CommRingsCategory {R}                 = idCommRingHom R
_⋆_ CommRingsCategory {R} {S} {T}        = compCommRingHom R S T
⋆IdL CommRingsCategory {R} {S}           = compIdCommRingHom {R = R} {S}
⋆IdR CommRingsCategory {R} {S}           = idCompCommRingHom {R = R} {S}
⋆Assoc CommRingsCategory {R} {S} {T} {U} = compAssocCommRingHom {R = R} {S} {T} {U}
isSetHom CommRingsCategory               = isSetRingHom _ _

TerminalCommRing : Terminal {ℓ-suc ℓ-zero} CommRingsCategory
fst TerminalCommRing = UnitCommRing
fst (fst (snd TerminalCommRing y)) _ = tt
snd (fst (snd TerminalCommRing y)) = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl)
snd (snd TerminalCommRing y) f = RingHom≡ (funExt (λ _ → refl))

open Pullback

{-
   A x_C B -----> A
      |           |
      |           | α
      |           |
      V           V
      B --------> C
            β
-}
PullbackCommRing : Pullbacks {ℓ-suc ℓ} CommRingsCategory
pbOb (PullbackCommRing (cospan A C B α β)) = fiberedProduct A B C α β
pbPr₁ (PullbackCommRing (cospan A C B α β)) = fiberedProductPr₁ A B C α β
pbPr₂ (PullbackCommRing (cospan A C B α β)) = fiberedProductPr₂ A B C α β
pbCommutes (PullbackCommRing (cospan A C B α β)) = fiberedProductPr₁₂Commutes A B C α β
univProp (PullbackCommRing (cospan A C B α β)) {d = D} = fiberedProductUnivProp A B C α β D


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

open import Cubical.HITs.AssocList.Base as AL
open import Cubical.Foundations.Everything
open import Cubical.HITs.FiniteMultiset as FMS
open import Cubical.Data.Nat   using (ℕ; zero; suc; _+_)

private
  variable
    ℓ : Level
    A : Type₀

multiPer : (a b : A) (m n : ℕ) (xs : AssocList A)
          → ⟨ a , m ⟩∷ ⟨ b , n ⟩∷ xs ≡ ⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs
multiPer a b zero n xs = del a (⟨ b , n ⟩∷ xs) ∙ cong (λ ys → ⟨ b , n ⟩∷ ys) (sym (del a xs))
multiPer a b (suc m) zero xs = cong (λ ys → ⟨ a , suc m ⟩∷ ys) (del b xs) ∙ sym (del b (⟨ a , suc m ⟩∷ xs))
multiPer a b (suc m) (suc n) xs =

 ⟨ a , suc m ⟩∷ ⟨ b , suc n ⟩∷ xs               ≡⟨ sym (agg a 1 m (⟨ b , suc n ⟩∷ xs)) ⟩
 ⟨ a , 1 ⟩∷ ⟨ a , m ⟩∷ ⟨ b , suc n ⟩∷ xs        ≡⟨ cong (λ ys → ⟨ a , 1 ⟩∷ ys) (multiPer a b m (suc n) xs) ⟩
 ⟨ a , 1 ⟩∷ ⟨ b , suc n ⟩∷ ⟨ a , m ⟩∷ xs        ≡⟨ cong (λ ys → ⟨ a , 1 ⟩∷ ys) (sym (agg b 1 n (⟨ a , m ⟩∷ xs))) ⟩
 ⟨ a , 1 ⟩∷ ⟨ b , 1 ⟩∷ ⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs ≡⟨ per a b (⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs) ⟩
 ⟨ b , 1 ⟩∷ ⟨ a , 1 ⟩∷ ⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs ≡⟨ cong (λ ys → ⟨ b , 1 ⟩∷ ⟨ a , 1 ⟩∷ ys) (multiPer b a n m xs) ⟩
 ⟨ b , 1 ⟩∷ ⟨ a , 1 ⟩∷ ⟨ a , m ⟩∷ ⟨ b , n ⟩∷ xs ≡⟨ cong (λ ys → ⟨ b , 1 ⟩∷ ys) (agg a 1 m (⟨ b , n ⟩∷ xs)) ⟩
 ⟨ b , 1 ⟩∷ ⟨ a , suc m ⟩∷ ⟨ b , n ⟩∷ xs        ≡⟨ cong (λ ys → ⟨ b , 1 ⟩∷ ys) (multiPer a b (suc m) n xs) ⟩
 ⟨ b , 1 ⟩∷ ⟨ b , n ⟩∷ ⟨ a , suc m ⟩∷ xs        ≡⟨ agg b 1 n (⟨ a , suc m ⟩∷ xs) ⟩
 ⟨ b , suc n ⟩∷ ⟨ a , suc m ⟩∷ xs               ∎

-- Show that association lists and finite multisets are equivalent
multi-∷ : A → ℕ → FMSet A → FMSet A
multi-∷ x zero xs = xs
multi-∷ x (suc n) xs = x ∷ multi-∷ x n xs

multi-∷-agg : (x : A) (m n : ℕ) (b : FMSet A) → multi-∷ x m (multi-∷ x n b) ≡ multi-∷ x (m + n) b
multi-∷-agg x zero n b = refl
multi-∷-agg x (suc m) n b i = x ∷ (multi-∷-agg x m n b i)

AL→FMS : AssocList A → FMSet A
AL→FMS = AL.Rec.f FMS.trunc [] multi-∷ comm multi-∷-agg λ _ _ → refl

FMS→AL : FMSet A → AssocList A
FMS→AL = FMS.Rec.f AL.trunc ⟨⟩ (λ x xs → ⟨ x , 1 ⟩∷ xs) per

AL→FMS∘FMS→AL≡id : section {A = AssocList A} AL→FMS FMS→AL
AL→FMS∘FMS→AL≡id = FMS.ElimProp.f (FMS.trunc _ _) refl (λ x p → cong (λ ys → x ∷ ys) p)

-- need a little lemma for other direction
multi-∷-id : (x : A) (n : ℕ) (u : FMSet A)
            → FMS→AL (multi-∷ x n u) ≡ ⟨ x , n ⟩∷ FMS→AL u
multi-∷-id x zero u = sym (del x (FMS→AL u))
multi-∷-id x (suc n) u = FMS→AL (multi-∷ x (suc n) u)     ≡⟨ cong (λ ys → ⟨ x , 1 ⟩∷ ys) (multi-∷-id x n u) ⟩
                         ⟨ x , 1 ⟩∷ ⟨ x , n ⟩∷ (FMS→AL u) ≡⟨ agg x 1 n (FMS→AL u) ⟩
                         ⟨ x , (suc n) ⟩∷ (FMS→AL u)      ∎

FMS→AL∘AL→FMS≡id : retract {A = AssocList A} AL→FMS FMS→AL
FMS→AL∘AL→FMS≡id = AL.ElimProp.f (AL.trunc _ _) refl (λ x n {xs} p → (multi-∷-id x n (AL→FMS xs)) ∙ cong (λ ys → ⟨ x , n ⟩∷ ys) p)

AssocList≃FMSet : AssocList A ≃ FMSet A
AssocList≃FMSet = isoToEquiv (iso AL→FMS FMS→AL AL→FMS∘FMS→AL≡id FMS→AL∘AL→FMS≡id)

AssocList≡FMSet : AssocList A ≡ FMSet A
AssocList≡FMSet = ua AssocList≃FMSet

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
module Agda.Builtin.FromString where

open import Agda.Primitive
open import Agda.Builtin.String

record IsString {a} (A : Set a) : Set (lsuc a) where
  field
    Constraint : String → Set a
    fromString : (s : String) {{_ : Constraint s}} → A

open IsString {{...}} public using (fromString)

{-# BUILTIN FROMSTRING fromString #-}
{-# DISPLAY IsString.fromString _ s = fromString s #-}


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

module Data.Tree.Braun where

open import Prelude
open import Data.Nat

data Bal (n : ℕ) : ℕ → ℕ → Type where
  one : Bal n n       (1 + n * 2)
  two : Bal n (suc n) (2 + n * 2)

data Tree {a} (A : Type a) : ℕ → Type a where
  leaf : Tree A 0
  node : ∀ {n m r} → (bal : Bal n m r) → A → (ls : Tree A m) → (rs : Tree A n) → Tree A r

private
  variable
    n : ℕ

inc : A → Tree A n → Tree A (suc n)
inc x leaf = node one x leaf leaf
inc x (node one y ls rs) = node two x (inc y rs) ls
inc x (node two y ls rs) = node one x (inc y rs) ls

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A solver for proving that one list is a sublist of the other.
------------------------------------------------------------------------

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

open import Relation.Binary using (Rel; Reflexive; Decidable)

module Data.List.Relation.Binary.Sublist.Heterogeneous.Solver
  {a r} {A : Set a} (R : Rel A r)
  (R-refl : Reflexive R) (R? : Decidable R)
  where

-- Note that we only need the above two constraints to define the
-- solver itself. The data structures do not depend on them. However,
-- having the whole module parametrised by them means that we can
-- instantiate them upon import.

open import Level using (_⊔_)
open import Data.Fin as Fin
open import Data.Maybe as M
open import Data.Nat.Base as Nat using (ℕ)
open import Data.Product
open import Data.Vec as Vec using (Vec ; lookup)
open import Data.List hiding (lookup)
open import Data.List.Properties
open import Data.List.Relation.Binary.Sublist.Heterogeneous
  hiding (lookup)
open import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
open import Function

open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≗_; sym; cong; cong₂; subst₂)
open import Relation.Nullary

open P.≡-Reasoning

------------------------------------------------------------------------
-- Reified list expressions

-- Basic building blocks: variables and values
data Item (n : ℕ) : Set a where
  var : Fin n → Item n
  val : A → Item n

-- Abstract Syntax Trees
infixr 5 _<>_
data TList (n : ℕ) : Set a where
  It   : Item n → TList n
  _<>_ : TList n → TList n → TList n
  []   : TList n

-- Equivalent linearised representation
RList : ∀ n → Set a
RList n = List (Item n)

-- Semantics
⟦_⟧I : ∀ {n} → Item n → Vec (List A) n → List A
⟦ var k ⟧I ρ = lookup ρ k
⟦ val a ⟧I ρ = [ a ]

⟦_⟧T : ∀ {n} → TList n → Vec (List A) n → List A
⟦ It it  ⟧T ρ = ⟦ it ⟧I ρ
⟦ t <> u ⟧T ρ = ⟦ t ⟧T ρ ++ ⟦ u ⟧T ρ
⟦ []     ⟧T ρ = []

⟦_⟧R : ∀ {n} → RList n → Vec (List A) n → List A
⟦ []     ⟧R ρ = []
⟦ x ∷ xs ⟧R ρ = ⟦ x ⟧I ρ ++ ⟦ xs ⟧R ρ

-- Orders
data _⊆I_ {n} : (d e : Item n) → Set (a ⊔ r) where
  var : ∀ {k l} → k ≡ l → var k ⊆I var l
  val : ∀ {a b} → R a b → val a ⊆I val b

_⊆T_ : ∀ {n} → (d e : TList n) → Set (a ⊔ r)
d ⊆T e = ∀ ρ → Sublist R (⟦ d ⟧T ρ) (⟦ e ⟧T ρ)

_⊆R_ : ∀ {n} (d e : RList n) → Set (a ⊔ r)
d ⊆R e = ∀ ρ → Sublist R (⟦ d ⟧R ρ) (⟦ e ⟧R ρ)

-- Flattening in a semantics-respecting manner

⟦++⟧R : ∀ {n} xs ys (ρ : Vec (List A) n) → ⟦ xs ++ ys ⟧R ρ ≡ ⟦ xs ⟧R ρ ++ ⟦ ys ⟧R ρ
⟦++⟧R []       ys ρ = P.refl
⟦++⟧R (x ∷ xs) ys ρ = begin
  ⟦ x ⟧I ρ ++ ⟦ xs ++ ys ⟧R ρ
    ≡⟨ cong (⟦ x ⟧I ρ ++_) (⟦++⟧R xs ys ρ) ⟩
  ⟦ x ⟧I ρ ++ ⟦ xs ⟧R ρ ++ ⟦ ys ⟧R ρ
    ≡⟨ sym $ ++-assoc (⟦ x ⟧I ρ) (⟦ xs ⟧R ρ) (⟦ ys ⟧R ρ) ⟩
  (⟦ x ⟧I ρ ++ ⟦ xs ⟧R ρ) ++ ⟦ ys ⟧R ρ
    ∎

flatten : ∀ {n} (t : TList n) → Σ[ r ∈ RList n ] ⟦ r ⟧R ≗ ⟦ t ⟧T
flatten []       = [] , λ _ → P.refl
flatten (It it)  = it ∷ [] , λ ρ → ++-identityʳ (⟦ It it ⟧T ρ)
flatten (t <> u) =
  let (rt , eqt) = flatten t
      (ru , equ) = flatten u
  in rt ++ ru , λ ρ → begin
    ⟦ rt ++ ru ⟧R ρ        ≡⟨ ⟦++⟧R rt ru ρ ⟩
    ⟦ rt ⟧R ρ ++ ⟦ ru ⟧R ρ ≡⟨ cong₂ _++_ (eqt ρ) (equ ρ) ⟩
    ⟦ t ⟧T ρ ++ ⟦ u ⟧T ρ   ≡⟨⟩
    ⟦ t <> u ⟧T ρ          ∎

------------------------------------------------------------------------
-- Solver for the sublist problem

-- auxiliary lemmas

private

  keep-it : ∀ {n a b} → a ⊆I b → (xs ys : RList n) → xs ⊆R ys → (a ∷ xs) ⊆R (b ∷ ys)
  keep-it (var a≡b) xs ys hyp ρ = ++⁺ (reflexive R-refl (cong _ a≡b)) (hyp ρ)
  keep-it (val rab) xs ys hyp ρ = rab ∷ hyp ρ

  skip-it : ∀ {n} it (d e : RList n) → d ⊆R e → d ⊆R (it ∷ e)
  skip-it it d ys hyp ρ = ++ˡ (⟦ it ⟧I ρ) (hyp ρ)

-- Solver for items
solveI : ∀ {n} (a b : Item n) → Maybe (a ⊆I b)
solveI (var k) (var l) = M.map var $ decToMaybe (k Fin.≟ l)
solveI (val a) (val b) = M.map val $ decToMaybe (R? a b)
solveI _ _ = nothing

-- Solver for linearised expressions
solveR : ∀ {n} (d e : RList n) → Maybe (d ⊆R e)
-- trivial
solveR [] e  = just (λ ρ → minimum _)
solveR d  [] = nothing
-- actual work
solveR (a ∷ d) (b ∷ e) with solveI a b
... | just it = M.map (keep-it it d e) (solveR d e)
... | nothing = M.map (skip-it b (a ∷ d) e) (solveR (a ∷ d) e)

-- Coming back to ASTs thanks to flatten

solveT : ∀ {n} (t u : TList n) → Maybe (t ⊆T u)
solveT t u =
  let (rt , eqt) = flatten t
      (ru , equ) = flatten u
  in case solveR rt ru of λ where
    (just hyp) → just (λ ρ → subst₂ (Sublist R) (eqt ρ) (equ ρ) (hyp ρ))
    nothing    → nothing

-- Prover for ASTs

prove : ∀ {n} (d e : TList n) → From-just (solveT d e)
prove d e = from-just (solveT d e)


text:
open import Relation.Binary.Core

module TreeSort.Everything {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import TreeSort.Impl1.Correctness.Order _≤_ tot≤ trans≤
open import TreeSort.Impl1.Correctness.Permutation _≤_ tot≤

open import TreeSort.Impl2.Correctness.Order _≤_ tot≤ trans≤
open import TreeSort.Impl2.Correctness.Permutation _≤_ tot≤

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------
-- The reflexive transitive closures of McBride, Norell and Jansson
------------------------------------------------------------------------

-- This module could be placed under Relation.Binary. However, since
-- its primary purpose is to be used for _data_ it has been placed
-- under Data instead.

module Data.Star where

open import Relation.Binary
open import Data.Function

infixr 5 _◅_

-- Reflexive transitive closure.

data Star {I : Set} (T : Rel I) : Rel I where
  ε   : Reflexive (Star T)
  _◅_ : ∀ {i j k} (x : T i j) (xs : Star T j k) → Star T i k
        -- The type of _◅_ is Trans T (Star T) (Star T); I expanded
        -- the definition in order to be able to name the arguments (x
        -- and xs).

-- Append/transitivity.

infixr 5 _◅◅_

_◅◅_ : ∀ {I} {T : Rel I} → Transitive (Star T)
ε        ◅◅ ys = ys
(x ◅ xs) ◅◅ ys = x ◅ (xs ◅◅ ys)

-- Sometimes you want to view cons-lists as snoc-lists. Then the
-- following "constructor" is handy. Note that this is _not_ snoc for
-- cons-lists, it is just a synonym for cons (with a different
-- argument order).

infixl 5 _▻_

_▻_ : ∀ {I} {T : Rel I} {i j k} →
      Star T j k → T i j → Star T i k
_▻_ = flip _◅_

-- A corresponding variant of append.

infixr 5 _▻▻_

_▻▻_ : ∀ {I} {T : Rel I} {i j k} →
       Star T j k → Star T i j → Star T i k
_▻▻_ = flip _◅◅_

-- A generalised variant of map which allows the index type to change.

gmap : ∀ {I} {T : Rel I} {J} {U : Rel J} →
       (f : I → J) → T =[ f ]⇒ U → Star T =[ f ]⇒ Star U
gmap f g ε        = ε
gmap f g (x ◅ xs) = g x ◅ gmap f g xs

map : ∀ {I} {T U : Rel I} → T ⇒ U → Star T ⇒ Star U
map = gmap id

-- TransFlip is used to state the type signature of gfold.

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

-- A generalised variant of fold.

gfold : ∀ {I J T} (f : I → J) P →
        Trans     T        (P on₁ f) (P on₁ f) →
        TransFlip (Star T) (P on₁ f) (P on₁ f)
gfold f P _⊕_ ∅ ε        = ∅
gfold f P _⊕_ ∅ (x ◅ xs) = x ⊕ gfold f P _⊕_ ∅ xs

fold : ∀ {I T} (P : Rel I) →
       Trans T P P → Reflexive P → Star T ⇒ P
fold P _⊕_ ∅ = gfold id P _⊕_ ∅

gfoldl : ∀ {I J T} (f : I → J) P →
         Trans (P on₁ f) T        (P on₁ f) →
         Trans (P on₁ f) (Star T) (P on₁ f)
gfoldl f P _⊕_ ∅ ε        = ∅
gfoldl f P _⊕_ ∅ (x ◅ xs) = gfoldl f P _⊕_ (∅ ⊕ x) xs

foldl : ∀ {I T} (P : Rel I) →
        Trans P T P → Reflexive P → Star T ⇒ P
foldl P _⊕_ ∅ = gfoldl id P _⊕_ ∅

concat : ∀ {I} {T : Rel I} → Star (Star T) ⇒ Star T
concat {T = T} = fold (Star T) _◅◅_ ε

-- If the underlying relation is symmetric, then the reflexive
-- transitive closure is also symmetric.

revApp : ∀ {I} {T U : Rel I} → Sym T U →
         ∀ {i j k} → Star T j i → Star U j k → Star U i k
revApp rev ε        ys = ys
revApp rev (x ◅ xs) ys = revApp rev xs (rev x ◅ ys)

reverse : ∀ {I} {T U : Rel I} → Sym T U → Sym (Star T) (Star U)
reverse rev xs = revApp rev xs ε

-- Reflexive transitive closures form a (generalised) monad.

-- return could also be called singleton.

return : ∀ {I} {T : Rel I} → T ⇒ Star T
return x = x ◅ ε

-- A generalised variant of the Kleisli star (flip bind, or
-- concatMap).

kleisliStar : ∀ {I J} {T : Rel I} {U : Rel J} (f : I → J) →
              T =[ f ]⇒ Star U → Star T =[ f ]⇒ Star U
kleisliStar f g = concat ∘ gmap f g

_⋆ : ∀ {I} {T U : Rel I} →
     T ⇒ Star U → Star T ⇒ Star U
_⋆ = kleisliStar id

infixl 1 _>>=_

_>>=_ : ∀ {I} {T U : Rel I} {i j} →
        Star T i j → T ⇒ Star U → Star U i j
m >>= f = (f ⋆) m

-- Note that the monad-like structure above is not an indexed monad
-- (as defined in Category.Monad.Indexed). If it were, then _>>=_
-- would have a type similar to
--
--   ∀ {I} {T U : Rel I} {i j k} →
--   Star T i j → (T i j → Star U j k) → Star U i k.
--                  ^^^^^
-- Note, however, that there is no scope for applying T to any indices
-- in the definition used in Category.Monad.Indexed.

max_issues_repo_name: larrytheliquid/Lemmachine


text:
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

idTrue : ∀ b → b ≡ true → Bool
idTrue b eq = {!!}

-- C-c C-c b RET gives us:
-- idTrue false eq = {!!}
-- idTrue true eq = {!!}

-- Now that we can leave `idTrue false eq` out because it's
-- trivially an impossible clause, it'd be nice to only get:
-- idTrue true eq = {!!}

-- But we should still get an absurd clause when we explictly
-- ask for it as in the following example:
-- C-c C-c e RET should give use
-- absurd ()

data Empty : Set where

absurd : ∀ {a} {A : Set a} → Empty → A
absurd e = {!!}

-- Similarly, C-C C-c b eq RET should give us
-- idTrue' false ()
-- idTrue' true refl = {!!}

idTrue' : ∀ b → b ≡ true → Bool
idTrue' b eq = {!!}

-- If the demanded split leads to trivially absurd clauses but the
-- function has a single clause, then we need to generate at least
-- one clause.

-- Therefore C-c C-c e RET should give us:
-- both .true refl f = {!!}

both : ∀ b → b ≡ true → b ≡ false → Bool
both b e f = {!!}

-- This should still be true in an already specialised context

both' : ∀ (c : Bool) b → b ≡ true → b ≡ false → Bool
both' false b e f = {!!}
both' true  b e f = {!!}


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

module Calf.Types.List where

open import Calf.Prelude
open import Calf.Metalanguage

open import Data.List public using (List; []; _∷_; _∷ʳ_; [_]; length; _++_)

list : tp pos → tp pos
list A = U (meta (List (val A)))

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
{-# OPTIONS --rewriting --allow-unsolved-metas #-}

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

postulate
  I : Set
  A : I → Set
  HEq : (i0 i1 : I) → A i0 → A i1 → Set
  HEq-on-refl : (i : I) (a0 a1 : A i) → HEq i i a0 a1 ≡ I
{-# REWRITE HEq-on-refl #-}

record Con : Set where
  field
    f : I → I
open Con public

postulate
  Ty : Con → Set

module M (Γ : Con) (_ : Ty Γ) where

  test : let aux1 : A (f Γ _)
             aux1 = _
             aux2 : A (f Γ _)
             aux2 = _
         in HEq _ _ aux1 aux2
  test = _

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Code for converting Vec A n → B to and from n-ary functions
------------------------------------------------------------------------

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

module Data.Vec.N-ary where

open import Data.Nat.Base hiding (_⊔_)
open import Data.Product as Prod
open import Data.Vec
open import Function
open import Function.Equivalence using (_⇔_; equivalence)
open import Level using (Level; _⊔_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable

------------------------------------------------------------------------
-- N-ary functions

N-ary-level : Level → Level → ℕ → Level
N-ary-level ℓ₁ ℓ₂ zero    = ℓ₂
N-ary-level ℓ₁ ℓ₂ (suc n) = ℓ₁ ⊔ N-ary-level ℓ₁ ℓ₂ n

N-ary : ∀ {ℓ₁ ℓ₂} (n : ℕ) → Set ℓ₁ → Set ℓ₂ → Set (N-ary-level ℓ₁ ℓ₂ n)
N-ary zero    A B = B
N-ary (suc n) A B = A → N-ary n A B

------------------------------------------------------------------------
-- Conversion

curryⁿ : ∀ {n a b} {A : Set a} {B : Set b} →
         (Vec A n → B) → N-ary n A B
curryⁿ {zero}  f = f []
curryⁿ {suc n} f = λ x → curryⁿ (f ∘ _∷_ x)

_$ⁿ_ : ∀ {n a b} {A : Set a} {B : Set b} → N-ary n A B → (Vec A n → B)
f $ⁿ []       = f
f $ⁿ (x ∷ xs) = f x $ⁿ xs

------------------------------------------------------------------------
-- Quantifiers

-- Universal quantifier.

∀ⁿ : ∀ n {a ℓ} {A : Set a} →
     N-ary n A (Set ℓ) → Set (N-ary-level a ℓ n)
∀ⁿ zero    P = P
∀ⁿ (suc n) P = ∀ x → ∀ⁿ n (P x)

-- Universal quantifier with implicit (hidden) arguments.

∀ⁿʰ : ∀ n {a ℓ} {A : Set a} →
     N-ary n A (Set ℓ) → Set (N-ary-level a ℓ n)
∀ⁿʰ zero    P = P
∀ⁿʰ (suc n) P = ∀ {x} → ∀ⁿʰ n (P x)

-- Existential quantifier.

∃ⁿ : ∀ n {a ℓ} {A : Set a} →
     N-ary n A (Set ℓ) → Set (N-ary-level a ℓ n)
∃ⁿ zero    P = P
∃ⁿ (suc n) P = ∃ λ x → ∃ⁿ n (P x)

------------------------------------------------------------------------
-- N-ary function equality

Eq : ∀ {a b c ℓ} {A : Set a} {B : Set b} {C : Set c} n →
     REL B C ℓ → REL (N-ary n A B) (N-ary n A C) (N-ary-level a ℓ n)
Eq n _∼_ f g = ∀ⁿ n (curryⁿ {n = n} λ xs → (f $ⁿ xs) ∼ (g $ⁿ xs))

-- A variant where all the arguments are implicit (hidden).

Eqʰ : ∀ {a b c ℓ} {A : Set a} {B : Set b} {C : Set c} n →
      REL B C ℓ → REL (N-ary n A B) (N-ary n A C) (N-ary-level a ℓ n)
Eqʰ n _∼_ f g = ∀ⁿʰ n (curryⁿ {n = n} λ xs → (f $ⁿ xs) ∼ (g $ⁿ xs))

------------------------------------------------------------------------
-- Some lemmas

-- The functions curryⁿ and _$ⁿ_ are inverses.

left-inverse : ∀ {n a b} {A : Set a} {B : Set b} (f : Vec A n → B) →
               ∀ xs → (curryⁿ f $ⁿ xs) ≡ f xs
left-inverse f []       = refl
left-inverse f (x ∷ xs) = left-inverse (f ∘ _∷_ x) xs

right-inverse : ∀ {a b} {A : Set a} {B : Set b} n (f : N-ary n A B) →
                Eq n _≡_ (curryⁿ (_$ⁿ_ {n} f)) f
right-inverse zero    f = refl
right-inverse (suc n) f = λ x → right-inverse n (f x)

-- ∀ⁿ can be expressed in an "uncurried" way.

uncurry-∀ⁿ : ∀ n {a ℓ} {A : Set a} {P : N-ary n A (Set ℓ)} →
             ∀ⁿ n P ⇔ (∀ (xs : Vec A n) → P $ⁿ xs)
uncurry-∀ⁿ n {a} {ℓ} {A} = equivalence (⇒ n) (⇐ n)
  where
  ⇒ : ∀ n {P : N-ary n A (Set ℓ)} →
      ∀ⁿ n P → (∀ (xs : Vec A n) → P $ⁿ xs)
  ⇒ zero    p []       = p
  ⇒ (suc n) p (x ∷ xs) = ⇒ n (p x) xs

  ⇐ : ∀ n {P : N-ary n A (Set ℓ)} →
      (∀ (xs : Vec A n) → P $ⁿ xs) → ∀ⁿ n P
  ⇐ zero    p = p []
  ⇐ (suc n) p = λ x → ⇐ n (p ∘ _∷_ x)

-- ∃ⁿ can be expressed in an "uncurried" way.

uncurry-∃ⁿ : ∀ n {a ℓ} {A : Set a} {P : N-ary n A (Set ℓ)} →
             ∃ⁿ n P ⇔ (∃ λ (xs : Vec A n) → P $ⁿ xs)
uncurry-∃ⁿ n {a} {ℓ} {A} = equivalence (⇒ n) (⇐ n)
  where
  ⇒ : ∀ n {P : N-ary n A (Set ℓ)} →
      ∃ⁿ n P → (∃ λ (xs : Vec A n) → P $ⁿ xs)
  ⇒ zero    p       = ([] , p)
  ⇒ (suc n) (x , p) = Prod.map (_∷_ x) id (⇒ n p)

  ⇐ : ∀ n {P : N-ary n A (Set ℓ)} →
      (∃ λ (xs : Vec A n) → P $ⁿ xs) → ∃ⁿ n P
  ⇐ zero    ([] , p)     = p
  ⇐ (suc n) (x ∷ xs , p) = (x , ⇐ n (xs , p))

-- Conversion preserves equality.

curryⁿ-cong : ∀ {n a b c ℓ} {A : Set a} {B : Set b} {C : Set c}
              (_∼_ : REL B C ℓ) (f : Vec A n → B) (g : Vec A n → C) →
              (∀ xs → f xs ∼ g xs) →
              Eq n _∼_ (curryⁿ f) (curryⁿ g)
curryⁿ-cong {zero}  _∼_ f g hyp = hyp []
curryⁿ-cong {suc n} _∼_ f g hyp = λ x →
  curryⁿ-cong _∼_ (f ∘ _∷_ x) (g ∘ _∷_ x) (λ xs → hyp (x ∷ xs))

curryⁿ-cong⁻¹ : ∀ {n a b c ℓ} {A : Set a} {B : Set b} {C : Set c}
                (_∼_ : REL B C ℓ) (f : Vec A n → B) (g : Vec A n → C) →
                Eq n _∼_ (curryⁿ f) (curryⁿ g) →
                ∀ xs → f xs ∼ g xs
curryⁿ-cong⁻¹ _∼_ f g hyp []       = hyp
curryⁿ-cong⁻¹ _∼_ f g hyp (x ∷ xs) =
  curryⁿ-cong⁻¹ _∼_ (f ∘ _∷_ x) (g ∘ _∷_ x) (hyp x) xs

appⁿ-cong : ∀ {n a b c ℓ} {A : Set a} {B : Set b} {C : Set c}
            (_∼_ : REL B C ℓ) (f : N-ary n A B) (g : N-ary n A C) →
            Eq n _∼_ f g →
            (xs : Vec A n) → (f $ⁿ xs) ∼ (g $ⁿ xs)
appⁿ-cong _∼_ f g hyp []       = hyp
appⁿ-cong _∼_ f g hyp (x ∷ xs) = appⁿ-cong _∼_ (f x) (g x) (hyp x) xs

appⁿ-cong⁻¹ : ∀ {n a b c ℓ} {A : Set a} {B : Set b} {C : Set c}
              (_∼_ : REL B C ℓ) (f : N-ary n A B) (g : N-ary n A C) →
              ((xs : Vec A n) → (f $ⁿ xs) ∼ (g $ⁿ xs)) →
              Eq n _∼_ f g
appⁿ-cong⁻¹ {zero}  _∼_ f g hyp = hyp []
appⁿ-cong⁻¹ {suc n} _∼_ f g hyp = λ x →
  appⁿ-cong⁻¹ _∼_ (f x) (g x) (λ xs → hyp (x ∷ xs))

-- Eq and Eqʰ are equivalent.

Eq-to-Eqʰ : ∀ {a b c ℓ} {A : Set a} {B : Set b} {C : Set c}
            n (_∼_ : REL B C ℓ) {f : N-ary n A B} {g : N-ary n A C} →
            Eq n _∼_ f g → Eqʰ n _∼_ f g
Eq-to-Eqʰ zero    _∼_ eq = eq
Eq-to-Eqʰ (suc n) _∼_ eq = Eq-to-Eqʰ n _∼_ (eq _)

Eqʰ-to-Eq : ∀ {a b c ℓ} {A : Set a} {B : Set b} {C : Set c}
            n (_∼_ : REL B C ℓ) {f : N-ary n A B} {g : N-ary n A C} →
            Eqʰ n _∼_ f g → Eq n _∼_ f g
Eqʰ-to-Eq zero    _∼_ eq = eq
Eqʰ-to-Eq (suc n) _∼_ eq = λ _ → Eqʰ-to-Eq n _∼_ eq


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Concrete.Obligations
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types
open        EpochConfig
open import LibraBFT.Concrete.System
open import LibraBFT.Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms PeerCanSignForPK (λ {st} {part} {pk} → PeerCanSignForPK-stable {st} {part} {pk})

-- In this module, we assume that the implementation meets its
-- obligations, and use this assumption to prove that, in any reachable
-- state, the implementatioon enjoys one of the per-epoch correctness
-- conditions proved in Abstract.Properties.  It can be extended to other
-- properties later.
module LibraBFT.Concrete.Properties
         (impl-correct : ImplObligations)
         (st : SystemState)
         (r : ReachableSystemState st)
         (𝓔 : EpochConfig)
         where
    open        ImplObligations impl-correct
    open        WithSPS sps-cor
    open        PerState st r
    open        PerEpoch 𝓔

    open import LibraBFT.Abstract.Abstract     UID _≟UID_ NodeId 𝓔 (ConcreteVoteEvidence 𝓔) as Abs
    open import LibraBFT.Concrete.Intermediate                   𝓔 (ConcreteVoteEvidence 𝓔)
    import      LibraBFT.Concrete.Obligations.VotesOnce          𝓔 (ConcreteVoteEvidence 𝓔) as VO-obl
    import      LibraBFT.Concrete.Obligations.PreferredRound     𝓔 (ConcreteVoteEvidence 𝓔) as PR-obl
    open import LibraBFT.Concrete.Properties.VotesOnce                                       as VO
    open import LibraBFT.Concrete.Properties.PreferredRound                                  as PR

    --------------------------------------------------------------------------------------------
    -- * A /ValidSysState/ is one in which both peer obligations are obeyed by honest peers * --
    --------------------------------------------------------------------------------------------

    record ValidSysState {ℓ}(𝓢 : IntermediateSystemState ℓ) : Set (ℓ+1 ℓ0 ℓ⊔ ℓ) where
      field
        vss-votes-once      : VO-obl.Type 𝓢
        vss-preferred-round : PR-obl.Type 𝓢
    open ValidSysState public

    -- TODO-2 : This should be provided as a module parameter here, and the
    -- proofs provided to instantiate it should be refactored into LibraBFT.Impl.
    -- However, see the TODO-3 in LibraBFT.Concrete.Intermediate, which suggests
    -- that those proofs may change, perhaps some parts of them will remain in
    -- Concrete and others should be in Impl, depending on how that TODO-3 is
    -- addressed.  There is not much point in doing said refactoring until we
    -- make progress on that question.

    validState : ValidSysState IntSystemState
    validState = record
      { vss-votes-once      = VO.Proof.voo sps-cor vo₁ vo₂ st r 𝓔
      ; vss-preferred-round = PR.Proof.prr sps-cor pr₁     st r 𝓔
      }

    open IntermediateSystemState IntSystemState

    open All-InSys-props InSys
    open WithAssumptions InSys

    -- We can now invoke the various abstract correctness properties.  Note that the arguments are
    -- expressed in Abstract terms (RecordChain, CommitRule).  Proving the corresponding properties
    -- for the actual implementation will involve proving that the implementation decides to commit
    -- only if it has evidence of the required RecordChains and CommitRules such that the records in
    -- the RecordChains are all "InSys" according to the implementation's notion thereof (defined in
    -- Concrete.System.IntSystemState).
    ConcCommitsDoNotConflict :
       ∀{q q'}
       → {rc  : RecordChain (Abs.Q q)}  → All-InSys rc
       → {rc' : RecordChain (Abs.Q q')} → All-InSys rc'
       → {b b' : Abs.Block}
       → CommitRule rc  b
       → CommitRule rc' b'
       → NonInjective-≡ Abs.bId ⊎ ((Abs.B b) ∈RC rc' ⊎ (Abs.B b') ∈RC rc)
    ConcCommitsDoNotConflict = CommitsDoNotConflict
           (VO-obl.proof IntSystemState (vss-votes-once validState))
           (PR-obl.proof IntSystemState (vss-preferred-round validState))

    module _ (∈QC⇒AllSent : Complete InSys) where

      ConcCommitsDoNotConflict' :
        ∀{q q'}{rc  : RecordChain (Abs.Q q)}{rc' : RecordChain (Abs.Q q')}{b b' : Abs.Block}
        → InSys (Abs.Q q) → InSys (Abs.Q q')
        → CommitRule rc  b
        → CommitRule rc' b'
        → NonInjective-≡ Abs.bId ⊎ ((Abs.B b) ∈RC rc' ⊎ (Abs.B b') ∈RC rc)
      ConcCommitsDoNotConflict' = CommitsDoNotConflict'
           (VO-obl.proof IntSystemState (vss-votes-once validState))
           (PR-obl.proof IntSystemState (vss-preferred-round validState))
           ∈QC⇒AllSent

      ConcCommitsDoNotConflict''
        : ∀{o o' q q'}
        → {rcf  : RecordChainFrom o  (Abs.Q q)}
        → {rcf' : RecordChainFrom o' (Abs.Q q')}
        → {b b' : Abs.Block}
        → InSys (Abs.Q q)
        → InSys (Abs.Q q')
        → CommitRuleFrom rcf  b
        → CommitRuleFrom rcf' b'
        → NonInjective-≡ Abs.bId ⊎ Σ (RecordChain (Abs.Q q')) ((Abs.B b)  ∈RC_)
                                 ⊎ Σ (RecordChain (Abs.Q q))  ((Abs.B b') ∈RC_)
      ConcCommitsDoNotConflict'' = CommitsDoNotConflict''
           (VO-obl.proof IntSystemState (vss-votes-once validState))
           (PR-obl.proof IntSystemState (vss-preferred-round validState))
           ∈QC⇒AllSent

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
module empty where

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

data ⊥ : Set where

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

----------------------------------------------------------------------
-- theorems
----------------------------------------------------------------------
⊥-elim : ⊥ → ∀ {P : Set} → P
⊥-elim ()

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial