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

module LeftCancellation where

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_,_; proj₁; proj₂)
open import Function renaming (_∘_ to _○_)

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong)
  renaming (trans to _∘_; sym to !_)

open import Equiv using (_∼_; _≃_; sym≃; inj≃; qinv; _●_)

------------------------------------------------------------------------------
-- This is WAY simpler than using 'with' and 'inspect'!

record Ev {A B : Set} (f : A → B) (x : A) : Set where
  constructor ev
  field
    v : B
    fx=v : f x ≡ v

mkV : {A B : Set} → (f : A → B) → (x : A) → Ev f x
mkV f x = ev (f x) refl

private
  bad-path : {A B : Set} → (a : A) → (b : B) → inj₁ a ≡ inj₂ b → ⊥
  bad-path x y ()

------------------------------------------------------------------------------
-- Very complex proof that we can cancel units on the left of ⊎

-- Some repeated patterns:

inj₁≡ : {A B : Set} → {a b : A} → inj₁ {A = A} {B} a ≡ inj₁ b → a ≡ b
inj₁≡ refl = refl

inj₂≡ : {A B : Set} → {a b : B} → inj₂ {A = A} {B} a ≡ inj₂ b → a ≡ b
inj₂≡ refl = refl

-- use injectivity of equivalences to go from f x ≡ f y to x ≡ y

injectivity : {A B : Set} (equiv : (⊤ ⊎ A) ≃ (⊤ ⊎ B)) →
  (a : A) → proj₁ equiv (inj₁ tt) ≡ proj₁ equiv (inj₂ a) → (inj₁ tt ≡ inj₂ a)
injectivity equiv x path = inj≃ equiv (inj₁ tt) (inj₂ x) path

left-cancel-⊤ : {A B : Set} →  ((⊤ ⊎ A) ≃ (⊤ ⊎ B)) → A ≃ B
left-cancel-⊤ {A} {B} (f₁ , qinv g₁ α₁ β₁) =
  let eqv = (f₁ , qinv g₁ α₁ β₁) in
  let v₁ = mkV f₁ (inj₁ tt) in
  let v₂ = mkV g₁ (inj₁ tt) in
  mk₁ {A} {B} eqv v₁ v₂
  where
    mk₁ : {A B : Set} (e : (⊤ ⊎ A) ≃ (⊤ ⊎ B)) →
              let (f₁ , qinv g₁ α₁ β₁) = e in
              Ev f₁ (inj₁ tt) → Ev g₁ (inj₁ tt) → A ≃ B
    mk₁ {A} {B} (f , qinv g α β) (ev (inj₁ tt) eq₁) (ev (inj₁ tt) eq₂) = A≃B
      where
        equiv : (⊤ ⊎ A) ≃ (⊤ ⊎ B)
        equiv = (f , qinv g α β)

        elim-path : {X Y Z : Set} → (e : (⊤ ⊎ X) ≃ (⊤ ⊎ Y)) → (x : X) →
           (proj₁ e) (inj₁ tt) ≡ (proj₁ e) (inj₂ x) → Z
        elim-path e a path = ⊥-elim (bad-path tt a (injectivity e a path))

        mkf : (a : A) → Ev f (inj₂ a) → B
        mkf a (ev (inj₁ tt) eq) = elim-path equiv a (eq₁ ∘ ! eq)
        mkf a (ev (inj₂ y) fx≡v) = y

        ff : A → B
        ff a = mkf a (mkV f (inj₂ a))

        mkg : (b : B) → Ev g (inj₂ b) → A
        mkg b (ev (inj₁ tt) eq) = elim-path (sym≃ equiv) b (eq₂ ∘ ! eq)
        mkg b (ev (inj₂ a) eq) = a

        gg : B → A
        gg b = mkg b (mkV g (inj₂ b))

        mkα : (b : B) →  (e : Ev g (inj₂ b)) → ff (mkg b e) ≡ b
        mkα b (ev (inj₁ tt) eq) = elim-path (sym≃ equiv) b (eq₂ ∘ ! eq)
        mkα b (ev (inj₂ a) eq) = mkα' (mkV f (inj₂ a))
          where
            mkα' : (ev : Ev f (inj₂ a)) → mkf a ev ≡ b
            mkα' (ev (inj₁ tt) eq₃) = elim-path equiv a (eq₁ ∘ ! eq₃)
            mkα' (ev (inj₂ _) eq₃) = inj₂≡ (! (cong f eq ∘ eq₃) ∘ α (inj₂ b))

        αα : ff ○ gg ∼ id
        αα b = mkα b (mkV g (inj₂ b))

        -- need to expand the definition of ff and gg "by hand" otherwise there is
        -- nowhere to 'stick in' the explicit e₁ and e₂ we have.

        mkβ : (a : A) → (e₁ : Ev f (inj₂ a)) → (e₂ : Ev g (inj₂ (mkf a e₁))) →
              mkg (mkf a e₁) e₂ ≡ a
        mkβ a (ev (inj₁ tt) eq) _ = elim-path equiv a (eq₁ ∘ ! eq)
        mkβ a (ev (inj₂ y) eq) (ev (inj₁ tt) eq₃) =
          elim-path (sym≃ equiv) y (eq₂ ∘ ! eq₃)
        mkβ a (ev (inj₂ _) eq) (ev (inj₂ _) eq₃) =
          inj₂≡ (((! eq₃) ∘ cong g (! eq)) ∘ β (inj₂ a))

        ββ : gg ○ ff ∼ id
        ββ a = let ev₁ = mkV f (inj₂ a) in mkβ a ev₁ (mkV g (inj₂ (mkf a ev₁)))

        A≃B : A ≃ B
        A≃B = ff , qinv gg αα ββ

    mk₁ (f , qinv g α β) (ev (inj₁ tt) eq₁) (ev (inj₂ a) eq₂) =
      let e = (f , qinv g α β) in
      ⊥-elim
        (bad-path tt a
          (injectivity e a ((eq₁ ∘ ! (α (inj₁ tt))) ∘ cong f eq₂)))
    mk₁ (f , qinv g α β) (ev (inj₂ b) eq₁) (ev (inj₁ tt) eq₂) =
     ⊥-elim (bad-path tt b (((! α (inj₁ tt)) ∘ cong f eq₂) ∘ eq₁))
    mk₁ {A} {B} (f , qinv g α β) (ev (inj₂ x) ftt=x) (ev (inj₂ y) gtt=y) =
      A≃B
      where
        equiv : (⊤ ⊎ A) ≃ (⊤ ⊎ B)
        equiv = (f , qinv g α β)

        elim-path : {X Y Z : Set} → (e : (⊤ ⊎ X) ≃ (⊤ ⊎ Y)) → (x : X) →
           (proj₁ e) (inj₁ tt) ≡ (proj₁ e) (inj₂ x) → Z
        elim-path e a path = ⊥-elim (bad-path tt a (injectivity e a path))

        mkf : (a : A) → Ev f (inj₂ a) → B
        mkf a (ev (inj₁ tt) _) = x
        mkf a (ev (inj₂ y) _) = y

        ff : A → B
        ff a = mkf a (mkV f (inj₂ a))

        mkg : (b : B) → Ev g (inj₂ b) → A
        mkg b (ev (inj₁ tt) eq) = y
        mkg b (ev (inj₂ a) eq) = a

        gg : B → A
        gg b = mkg b (mkV g (inj₂ b))

        mkα : (b : B) →  (e₁ : Ev g (inj₂ b)) → (e₂ : Ev f (inj₂ (mkg b e₁))) →
              mkf (mkg b e₁) e₂ ≡ b
        mkα b (ev (inj₁ tt) gb=tt) (ev (inj₁ tt) fgb=tt) =
          inj₂≡ ((! ftt=x ∘ ! cong f gb=tt) ∘ α (inj₂ b))
        mkα b (ev (inj₁ tt) gb=tt) (ev (inj₂ y₁) fy=y₁) =
          elim-path
            (sym≃ equiv)
            y₁
            ( ! ((! cong g fy=y₁ ∘ β (inj₂ y)) ∘ (! gtt=y)))
        mkα b (ev (inj₂ z) gb=z) (ev (inj₁ tt) fgb=tt) =
          elim-path
            (sym≃ equiv) b ((cong g (! fgb=tt) ∘ β (inj₂ z)) ∘ (! gb=z))
        mkα b (ev (inj₂ z) gb=z) (ev (inj₂ z₂) fgb=z₂) =
            let path = (cong g (! fgb=z₂) ∘ β (inj₂ z)) ∘ ! gb=z in
            inj₂≡ (inj≃ (sym≃ equiv) (inj₂ z₂) (inj₂ b)  path)

        αα : ff ○ gg ∼ id
        αα b = let ev₁ = mkV g (inj₂ b) in mkα b ev₁ (mkV f (inj₂ (mkg b ev₁)))

        -- need to expand the definition of ff and gg "by hand"
        -- otherwise there is nowhere to 'stick in' the explicit e₁
        -- and e₂ we have.

        mkβ : (a : A) → (e₁ : Ev f (inj₂ a)) →
          (e₂ : Ev g (inj₂ (mkf a e₁))) → mkg (mkf a e₁) e₂ ≡ a
        mkβ a (ev (inj₁ tt) eq) (ev (inj₁ _) eq₃) =
          inj₂≡ (! (cong g eq ∘ gtt=y) ∘ β (inj₂ a))
        mkβ a (ev (inj₁ tt) eq) (ev (inj₂ y₁) eq₃) =
          elim-path equiv y₁ ((ftt=x ∘ (! α (inj₂ x))) ∘ cong f eq₃)
        mkβ a (ev (inj₂ z) fa=z) (ev (inj₁ tt) eq₃) =
          elim-path equiv a ((cong f (! eq₃) ∘ α (inj₂ z)) ∘ (! fa=z) )
        mkβ a (ev (inj₂ _) fa=y) (ev (inj₂ _) eq₃) =
          inj₂≡ (((! eq₃) ∘ cong g (! fa=y)) ∘ β (inj₂ a))

        ββ : gg ○ ff ∼ id
        ββ a = let ev₁ = mkV f (inj₂ a) in mkβ a ev₁ (mkV g (inj₂ (mkf a ev₁)))

        A≃B : A ≃ B
        A≃B = ff , qinv gg αα ββ

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

open import Data.Nat using (ℕ; _+_)
open import Data.Fin using (Fin)
open import FinEquivPlusTimes using (module Plus; Fin1≃⊤)
open Plus using (⊎≃+; +≃⊎)
open import Equiv using (_⊎≃_; id≃)

left-cancel-1 : {m n : ℕ} →  (Fin (1 + m) ≃ Fin (1 + n)) → Fin m ≃ Fin n
left-cancel-1 pf = left-cancel-⊤ ((Fin1≃⊤ ⊎≃ id≃) ● +≃⊎ ● (pf ● ⊎≃+) ● (sym≃ Fin1≃⊤ ⊎≃ id≃))

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module maryjohn2 where

postulate Person        : Set
postulate john          : Person
postulate mary          : Person
postulate barbara       : Person
postulate IsStudent     : Person -> Set
postulate maryIsStudent : IsStudent mary
postulate implication   : IsStudent mary -> IsStudent john

Lemma1 : Set
Lemma1 = IsStudent john

proof-lemma1 : Lemma1
proof-lemma1 = implication maryIsStudent

Lemma2 : Set
Lemma2 = IsStudent john -> IsStudent barbara

proof-lemma2 : Lemma2
proof-lemma2 = \(x : IsStudent john) -> _

ext: agda

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Finite sets, based on AVL trees
------------------------------------------------------------------------

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

open import Relation.Binary using (StrictTotalOrder)

module Data.AVL.Sets
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
  where

open import Data.Bool
open import Data.List.Base as List using (List)
open import Data.Maybe.Base as Maybe
open import Data.Product as Prod using (_×_; _,_; proj₁)
open import Data.Unit
open import Function
open import Level

import Data.AVL strictTotalOrder as AVL
open StrictTotalOrder strictTotalOrder renaming (Carrier to A)

------------------------------------------------------------------------
-- The set type (note that Set is a reserved word)

⟨Set⟩ : Set (a ⊔ ℓ₂)
⟨Set⟩ = AVL.Tree (AVL.const ⊤)

------------------------------------------------------------------------
-- Repackaged functions

empty : ⟨Set⟩
empty = AVL.empty

singleton : A → ⟨Set⟩
singleton k = AVL.singleton k _

insert : A → ⟨Set⟩ → ⟨Set⟩
insert k = AVL.insert k _

delete : A → ⟨Set⟩ → ⟨Set⟩
delete = AVL.delete

infix 4 _∈?_

_∈?_ : A → ⟨Set⟩ → Bool
_∈?_ = AVL._∈?_

headTail : ⟨Set⟩ → Maybe (A × ⟨Set⟩)
headTail s = Maybe.map (Prod.map₁ proj₁) (AVL.headTail s)

initLast : ⟨Set⟩ → Maybe (⟨Set⟩ × A)
initLast s = Maybe.map (Prod.map₂ proj₁) (AVL.initLast s)

fromList : List A → ⟨Set⟩
fromList = AVL.fromList ∘ List.map (_, _)

toList : ⟨Set⟩ → List A
toList = List.map proj₁ ∘ AVL.toList


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

open import Everything.Safe

open import Numbers.Reals.Definition
open import Fields.Orders.Limits.Definition
open import Rings.Orders.Partial.Bounded
open import Rings.Orders.Total.Bounded
open import Rings.Orders.Total.BaseExpansion
open import Fields.Orders.Limits.Lemmas
open import Rings.Orders.Total.Examples
--open import Fields.CauchyCompletion.Archimedean

open import Sets.Cardinality.Infinite.Examples

open import ProjectEuler.Problem2

open import LectureNotes.NumbersAndSets.Examples1
open import LectureNotes.Groups.Lecture1

module Everything.Guardedness where


text:
module STLC.Properties.Determinism where

open import STLC.Term
open import STLC.Term.Reduction

open import Data.Nat using (ℕ; _+_)

open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contradiction)

open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)

open import Relation.Binary.PropositionalEquality as Eq
  using (refl; _≡_; cong₂)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

infix 4 _¬—→

_¬—→ : ∀ { n : ℕ } -> Term n -> Set
t₁ ¬—→ = ¬ (∃[ t₂ ] (t₁ —→ t₂))

¬—→-value : ∀ { n : ℕ } { t : Term n }
  -> Value t
  -- --------
  -> t ¬—→
¬—→-value {_} {ƛ _} v = λ ()

—→-¬value : ∀ { n : ℕ } { t₁ t₂ : Term n }
  -> t₁ —→ t₂
  -- ---------
  -> ¬ Value t₁
—→-¬value { _ } { _ } { t₂ } s v = ¬—→-value v (t₂ , s)

determinism : ∀ { n : ℕ } { t₁ t₂ t₃ : Term n }
  -> t₁ —→ t₂
  -> t₁ —→ t₃
  -- --------
  -> t₂ ≡ t₃

determinism (β-·₁ s₁) (β-·₁ s₂) = cong₂ (_·_) (determinism s₁ s₂) refl
determinism (β-·₂ _ s₁) (β-·₂ _ s₂) =  cong₂ (_·_) refl (determinism s₁ s₂)
determinism (β-ƛ _) (β-ƛ _) = refl
determinism (β-·₁ s) (β-·₂ v _) = contradiction v (—→-¬value s)
determinism (β-·₂ v _) (β-·₁ s) = contradiction v (—→-¬value s)
determinism (β-·₂ _ s) (β-ƛ v) = contradiction v (—→-¬value s)
determinism (β-ƛ v) (β-·₂ _ s) = contradiction v (—→-¬value s)

max_stars_repo_name: johnyob/agda-types

max_issues_repo_name: johnyob/agda-types

max_forks_repo_name: johnyob/agda-types


text:
-- Martin-Löf identity type

{-# OPTIONS --without-K --safe #-}
module TypeTheory.Identity where

open import Level renaming (zero to lzero; suc to lsuc)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (refl; _≡_)
  renaming (trans to ≡-trans; sym to ≡-sym; cong to ≡-cong)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

record JBundle a : Set (lsuc a) where
  field
    Carrier : Set a
    _≈_     : Rel Carrier a
    ≈-refl  : ∀ {x} → x ≈ x
    J       : (C : ∀ x y → x ≈ y → Set a) → (∀ x → C x x ≈-refl) →
              ∀ x y (p : x ≈ y) → C x y p
    J-β     : ∀ (C : ∀ x y → x ≈ y → Set a) (c : ∀ x → C x x ≈-refl) x →
              J C c x x ≈-refl ≡ c x

module JBundleProperties {a} (jBundle : JBundle a) where
  open JBundle jBundle renaming (Carrier to A)
  sym : ∀ {x y} → x ≈ y → y ≈ x
  sym {x} {y} x≈y = J (λ x₁ y₁ x₁≈y₁ → y₁ ≈ x₁) (λ _ → ≈-refl) x y x≈y

  sym-≈-refl : ∀ x → sym (≈-refl {x}) ≡ ≈-refl
  sym-≈-refl x = J-β (λ x₁ y₁ x₁≈y₁ → y₁ ≈ x₁) (λ _ → ≈-refl) x

  sym-involutive : ∀ {x y} (p : x ≈ y) → sym (sym p) ≡ p
  sym-involutive {x} {y} p =
   J (λ x₁ y₁ x₁≈y₁ → sym (sym x₁≈y₁) ≡ x₁≈y₁)
     (λ z → ≡-trans (≡-cong sym (sym-≈-refl z)) (sym-≈-refl z)) x y p

  sym-injective : ∀ {x y} {p q : x ≈ y} → sym p ≡ sym q → p ≡ q
  sym-injective {p = p} {q} eq = begin
    p           ≡⟨ ≡-sym (sym-involutive p) ⟩
    sym (sym p) ≡⟨ ≡-cong sym eq ⟩
    sym (sym q) ≡⟨ sym-involutive q ⟩
    q           ∎
    where open P.≡-Reasoning
{-
  trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
  trans {x} {y} {z} x≈y y≈z = J D (λ u → λ w q → q) x y x≈y z y≈z
    where
    D : ∀ u v → u ≈ v → Set _
    D u v u≈v = ∀ w → (q : v ≈ w) → u ≈ w
-}
  trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
  trans {x} {y} {z} x≈y y≈z = J D (λ u → λ w q → J E (λ _ → ≈-refl) u w q) x y x≈y z y≈z
    where
    D : ∀ u v → u ≈ v → Set _
    D u v u≈v = ∀ w → v ≈ w → u ≈ w
    E : ∀ u v → u ≈ v → Set _
    E u v q = u ≈ v


text:
module _ where

open import Common.Prelude hiding (_>>=_)
open import Common.Reflection
open import Common.Equality

infix 0 case_of_
case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

blockOnFresh : TC ⊤
blockOnFresh =
  checkType unknown unknown >>= λ
  { (meta m _) → blockOnMeta m
  ; _ → typeError (strErr "impossible" ∷ []) }

macro
  weirdButShouldWork : Tactic
  weirdButShouldWork hole =
    inferType hole >>= λ goal →
    case goal of λ
    { (meta _ _) → blockOnFresh
    ; _ → unify hole (lit (nat 42))
    }

-- When the goal is a meta the tactic will block on a different, fresh, meta.
-- That's silly, but should still work. Once the goal is resolved the tactic
-- doesn't block any more so everything should be fine.
thing  : _
solves : Nat
thing  = weirdButShouldWork
solves = thing

check : thing ≡ 42
check = refl


text:
open import Syntax
import Renaming
import Instantiation

module Theory (𝕊 : Signature) where

  open Expression 𝕊
  open Instantiation
  open Renaming

  infix 5 □⦂_
  infix 5 _≡_⦂type-by□
  infix 5 _≡_⦂_by□

  data BoundaryThesis : ∀ (cl : Class) (𝕄 : MShape) (γ : VShape) → Set where
    □⦂type : ∀ {𝕄 γ} → BoundaryThesis (obj Ty) 𝕄 γ
    □⦂_ : ∀ {𝕄 γ} (A : ExprTy 𝕄 γ) → BoundaryThesis (obj Tm) 𝕄 γ
    _≡_⦂type-by□ : ∀ {𝕄 γ} (A B : ExprTy 𝕄 γ) → BoundaryThesis EqTy 𝕄 γ
    _≡_⦂_by□ : ∀ {𝕄 γ} (u v : ExprTm 𝕄 γ) (A : ExprTy 𝕄 γ) → BoundaryThesis EqTm 𝕄 γ

  rename-boundary-thesis : ∀ {cl 𝕄 γ δ} → (γ →ʳ δ) → BoundaryThesis cl 𝕄 γ → BoundaryThesis cl 𝕄 δ
  rename-boundary-thesis ρ □⦂type = □⦂type
  rename-boundary-thesis ρ (□⦂ A) = □⦂ [ ρ ]ʳ A
  rename-boundary-thesis ρ (A ≡ B ⦂type-by□) = [ ρ ]ʳ A ≡ [ ρ ]ʳ B ⦂type-by□
  rename-boundary-thesis ρ (u ≡ v ⦂ A by□) = [ ρ ]ʳ u ≡ [ ρ ]ʳ v ⦂ [ ρ ]ʳ A by□

  instantiate-boundary-thesis : ∀ {cl 𝕂 𝕄 γ} → (𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ) → BoundaryThesis cl 𝕂 γ → BoundaryThesis cl 𝕄 γ
  instantiate-boundary-thesis I □⦂type = □⦂type
  instantiate-boundary-thesis I (□⦂ A) = □⦂ [ I ]ⁱ A
  instantiate-boundary-thesis I (A ≡ B ⦂type-by□) = [ I ]ⁱ A ≡ [ I ]ⁱ B ⦂type-by□
  instantiate-boundary-thesis I (u ≡ v ⦂ A by□) = [ I ]ⁱ u ≡ [ I ]ⁱ v ⦂ [ I ]ⁱ A by□

  VContext : ∀ (𝕄 : MShape) (γ : VShape) → Set
  VContext 𝕄 γ = ∀ (x : var γ) → ExprTy 𝕄 γ

  instantiate-vcontext : ∀ {𝕂 𝕄 γ} (I : 𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ) (Γ : VContext 𝕂 γ) → VContext 𝕄 γ
  instantiate-vcontext I Γ x = [ I ]ⁱ Γ x

  VExtension : ∀ (𝕄 : MShape) (γ δ : VShape) → Set
  VExtension 𝕄 γ δ = ∀ (x : var δ) → ExprTy 𝕄 (γ ⊕ δ)

  empty-vextension : ∀ {𝕄 γ} → VExtension 𝕄 γ 𝟘
  empty-vextension ()

  -- variable context extension
  infixl 6 _⊕ᶜ_

  _⊕ᶜ_ : ∀ {𝕄 γ δ} → VContext 𝕄 γ → VExtension 𝕄 γ δ → VContext 𝕄 (γ ⊕ δ)
  (Γ ⊕ᶜ Δ) (var-left x) = [ var-left ]ʳ (Γ x)
  (Γ ⊕ᶜ Δ) (var-right y) = Δ y

  rename-vextension : ∀ {𝕄 β γ δ} → (β →ʳ γ) → VExtension 𝕄 β δ → VExtension 𝕄 γ δ
  rename-vextension ρ Δ x =  [ [ (var-left ∘ʳ ρ) , var-right ]ʳ ]ʳ Δ x

  instantiate-vextension : ∀ {𝕂 𝕄 γ δ} → (I : 𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ) → VExtension 𝕂 γ δ → VExtension 𝕄 γ δ
  instantiate-vextension I Δ x = [ ⇑ⁱ I ]ⁱ (Δ x)

  record JudgementThesis (cl : Class) (𝕄 : MShape) (γ : VShape) : Set where
    constructor _⟦_⟧
    field
      jdg-bdry : BoundaryThesis cl 𝕄 γ
      jdg-head : Expr cl 𝕄 γ

  presupposition : ∀ {cl 𝕄 γ} → JudgementThesis cl 𝕄 γ → BoundaryThesis cl 𝕄 γ
  presupposition (𝒷 ⟦ _ ⟧) = 𝒷

  -- shorthands for the four judgement forms

  infix 5 _⦂type
  _⦂type : ∀ {𝕄 γ} (A : ExprTy 𝕄 γ) → JudgementThesis (obj Ty) 𝕄 γ
  A ⦂type = □⦂type ⟦ A ⟧

  infix 5 _⦂_
  _⦂_ : ∀ {𝕄 γ} (e : ExprTm 𝕄 γ) (A : ExprTy 𝕄 γ) → JudgementThesis (obj Tm) 𝕄 γ
  e ⦂ A = (□⦂ A) ⟦ e ⟧

  infix 5 _≡_by_
  _≡_by_ : ∀ {𝕄 γ} (A B : ExprTy 𝕄 γ) (ξ : Expr EqTy 𝕄 γ) → JudgementThesis (EqTy) 𝕄 γ
  A ≡ B by ξ = (A ≡ B ⦂type-by□) ⟦ ξ ⟧

  infix 5 _≡_⦂_by_
  _≡_⦂_by_ : ∀ {𝕄 γ} (d e : ExprTm 𝕄 γ) (A : ExprTy 𝕄 γ) (ξ : Expr EqTm 𝕄 γ) → JudgementThesis (EqTm) 𝕄 γ
  d ≡ e ⦂ A by ξ = (d ≡ e ⦂ A by□) ⟦ ξ ⟧

  rename-judgement-thesis : ∀ {cl 𝕄 γ δ} → (γ →ʳ δ) → JudgementThesis cl 𝕄 γ → JudgementThesis cl 𝕄 δ
  rename-judgement-thesis ρ (b ⟦ e ⟧) = (rename-boundary-thesis ρ b) ⟦ [ ρ ]ʳ e ⟧

  instantiate-judgement-thesis : ∀ {cl 𝕂 𝕄 γ} → (𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ) → JudgementThesis cl 𝕂 γ → JudgementThesis cl 𝕄 γ
  instantiate-judgement-thesis I (B ⟦ e ⟧) = (instantiate-boundary-thesis I B) ⟦ [ I ]ⁱ e ⟧

  infix 4 ⟪_⟫_

  record Abstracted (F : MShape → VShape → Set) (𝕄 : MShape) (γ δ : VShape) : Set where
    constructor ⟪_⟫_
    field
      abstr-vextenson : VExtension 𝕄 γ δ
      abstr-body : F 𝕄 (γ ⊕ δ)

  non-abstracted : ∀ (F : MShape → VShape → Set) (r : ∀ {𝕄 β γ} → (β →ʳ γ) → F 𝕄 β → F 𝕄 γ)
                     {𝕄 : MShape} {γ : VShape} (t : F 𝕄 γ) → Abstracted F 𝕄 γ 𝟘
  non-abstracted F r t = ⟪ empty-vextension ⟫ (r var-left t)

  rename-abstracted : ∀ (F : MShape → VShape → Set) (r : ∀ {𝕄 β γ} → (β →ʳ γ) → F 𝕄 β → F 𝕄 γ) {𝕄 β γ δ} (ρ : β →ʳ γ) →
                        Abstracted F 𝕄 β δ → Abstracted F 𝕄 γ δ
  rename-abstracted F r ρ (⟪ Δ ⟫ t) = ⟪ rename-vextension ρ Δ ⟫ (r (⇑ʳ ρ) t)

  instantiate-abstracted : ∀ (F : MShape → VShape → Set) (ι : ∀ {𝕂 𝕄 γ} → (𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ) → F 𝕂 γ → F 𝕄 γ)
                             {𝕂 𝕄 γ δ} (I : 𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ) → Abstracted F 𝕂 γ δ → Abstracted F 𝕄 γ δ
  instantiate-abstracted F ι I (⟪ Δ ⟫ t) = ⟪ (instantiate-vextension I Δ) ⟫ ι (⇑ⁱ I) t

  AbstractedBoundary : ∀ cl 𝕄 γ δ → Set
  AbstractedBoundary cl 𝕄 γ δ = Abstracted (BoundaryThesis cl) 𝕄 γ δ

  infix 4 ⟪⟫ᵇ_
  ⟪⟫ᵇ_ : ∀ {cl 𝕄 γ} → BoundaryThesis cl 𝕄 γ → AbstractedBoundary cl 𝕄 γ 𝟘
  ⟪⟫ᵇ_ {cl = cl} 𝒷 = non-abstracted (BoundaryThesis cl) rename-boundary-thesis 𝒷

  rename-abstracted-boundary : ∀ {cl 𝕄 β γ δ} (ρ : β →ʳ γ) →
                                 AbstractedBoundary cl 𝕄 β δ → AbstractedBoundary cl 𝕄 γ δ
  rename-abstracted-boundary {cl = cl} = rename-abstracted (BoundaryThesis cl) rename-boundary-thesis

  instantiate-abstracted-boundary : ∀ {cl 𝕂 𝕄 γ δ} (I : 𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ) →
                                      AbstractedBoundary cl 𝕂 γ δ → AbstractedBoundary cl 𝕄 γ δ
  instantiate-abstracted-boundary {cl = cl} = instantiate-abstracted (BoundaryThesis cl) instantiate-boundary-thesis

  AbstractedJudgement : ∀ cl 𝕄 γ δ → Set
  AbstractedJudgement cl 𝕄 γ δ = Abstracted (JudgementThesis cl) 𝕄 γ δ

  infix 4 ⟪⟫ʲ_
  ⟪⟫ʲ_ : ∀ {cl 𝕄 γ} → JudgementThesis cl 𝕄 γ → AbstractedJudgement cl 𝕄 γ 𝟘
  ⟪⟫ʲ_ {cl = cl} 𝒷 = non-abstracted (JudgementThesis cl) rename-judgement-thesis 𝒷

  fill-abstraction : ∀ {cl 𝕄 γ δ} (ℬ : AbstractedBoundary cl 𝕄 γ δ) → Arg cl 𝕄 γ δ → AbstractedJudgement cl 𝕄 γ δ
  fill-abstraction (⟪ Δ ⟫ 𝒷) e = ⟪ Δ ⟫ (𝒷 ⟦ e ⟧)

  rename-abstracted-judgement : ∀ {cl 𝕄 β γ δ} (ρ : β →ʳ γ) →
                                  AbstractedJudgement cl 𝕄 β δ → AbstractedJudgement cl 𝕄 γ δ
  rename-abstracted-judgement {cl = cl} = rename-abstracted (JudgementThesis cl) rename-judgement-thesis

  instantiate-abstracted-judgement : ∀ {cl 𝕂 𝕄 γ δ} (I : 𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ) →
                                       AbstractedJudgement cl 𝕂 γ δ → AbstractedJudgement cl 𝕄 γ δ
  instantiate-abstracted-judgement {cl = cl} = instantiate-abstracted (JudgementThesis cl) instantiate-judgement-thesis

  MContext : ∀ (𝕄 : MShape) → Set
  MContext 𝕄 = ∀ {clᴹ : Class} {γᴹ : VShape} (M : [ clᴹ , γᴹ ]∈ 𝕄) → AbstractedBoundary clᴹ 𝕄 𝟘 γᴹ

  HypotheticalBoundary : ∀ cl {𝕄 : MShape} {γ} (Θ : MContext 𝕄) (Γ : VContext 𝕄 γ) δ → Set
  HypotheticalBoundary cl {𝕄 = 𝕄} {γ = γ} Θ Γ δ = Abstracted (BoundaryThesis cl) 𝕄 γ δ

  instantiate-hypothetical-boundary :
    ∀ {cl 𝕂 𝕄 γ δ} (I : 𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ) {Ξ : MContext 𝕂} {Γ : VContext 𝕂 γ} {Θ : MContext 𝕄} →
      HypotheticalBoundary cl Ξ Γ δ → HypotheticalBoundary cl Θ (instantiate-vcontext I Γ) δ
  instantiate-hypothetical-boundary I B = instantiate-abstracted-boundary I B

  HypotheticalJudgement : ∀ cl {𝕄 : MShape} {γ} (Θ : MContext 𝕄) (Γ : VContext 𝕄 γ) δ → Set
  HypotheticalJudgement cl {𝕄 = 𝕄} {γ = γ} Θ Γ δ = Abstracted (JudgementThesis cl) 𝕄 γ δ

  instantiate-hypothetical-judgement :
    ∀ {cl 𝕂 𝕄 γ δ} (I : 𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ) {Ξ : MContext 𝕂} {Γ : VContext 𝕂 γ} {Θ : MContext 𝕄} →
      HypotheticalJudgement cl Ξ Γ δ → HypotheticalJudgement cl Θ (instantiate-vcontext I Γ) δ
  instantiate-hypothetical-judgement I B = instantiate-abstracted-judgement I B

  infix 6 _⇛_

  record Rule (cl : Class) (𝕄 : MShape) : Set where
    constructor _⇛_

    field
      premises : MContext 𝕄
      conclusion : JudgementThesis cl 𝕄 𝟘

  Theory = ∀ {cl} {𝕄} → Rule cl 𝕄 → Set

  instantiate-conclusion : ∀ {cl 𝕂 𝕄 γ} (I : 𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ) → JudgementThesis cl 𝕂 𝟘 → JudgementThesis cl 𝕄 γ
  instantiate-conclusion I 𝒿 = instantiate-judgement-thesis I (rename-judgement-thesis 𝟘-initial 𝒿)

  module Derivation (𝒯 : Theory) where

    open Rule

    infix 3 _,_⊢ʲ_
    infix 3 _,_⊢ᵇ_

    data _,_⊢ʲ_ :
      ∀ {cl 𝕄 γ δ} (Θ : MContext 𝕄) (Γ : VContext 𝕄 γ) (𝒥 : HypotheticalJudgement cl Θ Γ δ) → Set

    data _,_⊢ᵇ_ :
      ∀ {cl 𝕄 γ δ} (Θ : MContext 𝕄) (Γ : VContext 𝕄 γ) (ℬ : HypotheticalBoundary cl Θ Γ δ) → Set

    -- derivable instantiation
    is-derivable : ∀ {𝕂 𝕄 γ} (I : 𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ) (Ξ : MContext 𝕂) (Θ : MContext 𝕄) (Γ : VContext 𝕄 γ) → Set
    is-derivable {𝕂 = 𝕂} I Ξ Θ Γ =
       ∀ {clᴷ γᴷ} (M : [ clᴷ , γᴷ ]∈ 𝕂) →
         Θ , Γ ⊢ʲ fill-abstraction (instantiate-abstracted-boundary I (rename-abstracted-boundary 𝟘-initial (Ξ M))) (I M)

    data _,_⊢ʲ_ where

      TT-VAR :
        ∀ {𝕄 γ} {Θ : MContext 𝕄} {Γ : VContext 𝕄 γ} (x : var γ) → Θ , Γ ⊢ʲ (⟪⟫ʲ (expr-var x ⦂ Γ x))

      TT-RULE :
        ∀ {cl 𝕂 𝕄 γ} {Ξ : MContext 𝕂} {Θ : MContext 𝕄} {Γ : VContext 𝕄 γ}
          (I : 𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ) {𝒿 : JudgementThesis cl 𝕂 𝟘} (R : 𝒯 (Ξ ⇛ 𝒿)) →
          Θ , Γ ⊢ᵇ ⟪⟫ᵇ instantiate-boundary-thesis I (rename-boundary-thesis 𝟘-initial (presupposition 𝒿)) →
          is-derivable I Ξ Θ Γ →
          Θ , Γ ⊢ʲ ⟪⟫ʲ instantiate-conclusion I 𝒿

      TT-ABSTR :
        ∀ {cl 𝕄 γ δ} {Θ : MContext 𝕄} {Γ : VContext 𝕄 γ} {Δ : VExtension 𝕄 γ δ} {𝒿 : JudgementThesis cl 𝕄 (γ ⊕ δ) } →
          Θ , Γ ⊕ᶜ Δ ⊢ʲ ⟪⟫ʲ 𝒿 →
          Θ , Γ ⊢ʲ ⟪ Δ ⟫ 𝒿

      TT-META :
        {!!}

      TT-META-CONGR :
        {!!}

      TT-EQTY-REFL :
        {!!}
      TT-EQTY-SYM :
        {!!}
      TT-EQTY-TRANS :
        {!!}
      TT-EQTM-REFL :
        {!!}
      TT-EQTM-SYM :
        {!!}
      TT-EQTM-TRANS :
        {!!}
      TT-CONV-TM :
        {!!}
      TT-CONV-EQTM :
        {!!}

    data _,_⊢ᵇ_ where

      TT-BDRY-TY :
        ∀ {𝕄 γ} {Θ : MContext 𝕄} {Γ : VContext 𝕄 γ} →
          Θ , Γ ⊢ᵇ ⟪⟫ᵇ □⦂type

      TT-BDRY-TM :
        ∀ {𝕄 γ} {Θ : MContext 𝕄} {Γ : VContext 𝕄 γ} {A} →
          Θ , Γ ⊢ʲ ⟪⟫ʲ A ⦂type →
          Θ , Γ ⊢ᵇ ⟪⟫ᵇ □⦂ A

      TT-BDRY-EQTY :
        ∀ {𝕄 γ} {Θ : MContext 𝕄} {Γ : VContext 𝕄 γ} {A B} →
          Θ , Γ ⊢ʲ ⟪⟫ʲ A ⦂type →
          Θ , Γ ⊢ʲ ⟪⟫ʲ B ⦂type →
          Θ , Γ ⊢ᵇ ⟪⟫ᵇ A ≡ B ⦂type-by□

      TT-BDRY-EQTM :
        ∀ {𝕄 γ} {Θ : MContext 𝕄} {Γ : VContext 𝕄 γ} {u v A} →
          Θ , Γ ⊢ʲ ⟪⟫ʲ A ⦂type →
          Θ , Γ ⊢ʲ ⟪⟫ʲ u ⦂ A →
          Θ , Γ ⊢ʲ ⟪⟫ʲ v ⦂ A →
          Θ , Γ ⊢ᵇ ⟪⟫ᵇ u ≡ v ⦂ A by□

      TT-BDRY-ABSTR :
        ∀ {cl 𝕄 γ δ} {Θ : MContext 𝕄} {Γ : VContext 𝕄 γ} {Δ : VExtension 𝕄 γ δ} {𝒷 : BoundaryThesis cl 𝕄 (γ ⊕ δ) } →
          Θ , Γ ⊕ᶜ Δ ⊢ᵇ ⟪⟫ᵇ 𝒷 →
          Θ , Γ ⊢ᵇ ⟪ Δ ⟫ 𝒷

    -- Missing: well-formed extensions and contexts


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Non-empty lists
------------------------------------------------------------------------

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

module Data.List.NonEmpty where

open import Category.Monad
open import Data.Bool.Base using (Bool; false; true; not; T)
open import Data.Bool.Properties
open import Data.List as List using (List; []; _∷_)
open import Data.Maybe.Base using (Maybe ; nothing; just)
open import Data.Nat as Nat
open import Data.Product as Prod using (∃; _×_; proj₁; proj₂; _,_; -,_)
open import Data.These as These using (These; this; that; these)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Data.Unit
open import Data.Vec as Vec using (Vec; []; _∷_)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
  using () renaming (module Equivalence to Eq)
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
open import Relation.Nullary.Decidable using (⌊_⌋)

------------------------------------------------------------------------
-- Non-empty lists

infixr 5 _∷_

record List⁺ {a} (A : Set a) : Set a where
  constructor _∷_
  field
    head : A
    tail : List A

open List⁺ public

-- Basic combinators

module _ {a} {A : Set a} where

  uncons : List⁺ A → A × List A
  uncons (hd ∷ tl) = hd , tl

  [_] : A → List⁺ A
  [ x ] = x ∷ []

  infixr 5 _∷⁺_

  _∷⁺_ : A → List⁺ A → List⁺ A
  x ∷⁺ y ∷ xs = x ∷ y ∷ xs

  length : List⁺ A → ℕ
  length (x ∷ xs) = suc (List.length xs)

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

module _ {a} {A : Set a} where

  toList : List⁺ A → List A
  toList (x ∷ xs) = x ∷ xs

  fromList : List A → Maybe (List⁺ A)
  fromList []       = nothing
  fromList (x ∷ xs) = just (x ∷ xs)

  fromVec : ∀ {n} → Vec A (suc n) → List⁺ A
  fromVec (x ∷ xs) = x ∷ Vec.toList xs

  toVec : (xs : List⁺ A) → Vec A (length xs)
  toVec (x ∷ xs) = x ∷ Vec.fromList xs

lift : ∀ {a b} {A : Set a} {B : Set b} →
       (∀ {m} → Vec A (suc m) → ∃ λ n → Vec B (suc n)) →
       List⁺ A → List⁺ B
lift f xs = fromVec (proj₂ (f (toVec xs)))

------------------------------------------------------------------------
-- Other operations

map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List⁺ A → List⁺ B
map f (x ∷ xs) = (f x ∷ List.map f xs)

-- Right fold. Note that s is only applied to the last element (see
-- the examples below).

foldr : ∀ {a b} {A : Set a} {B : Set b} →
        (A → B → B) → (A → B) → List⁺ A → B
foldr {A = A} {B} c s (x ∷ xs) = foldr′ x xs
  where
  foldr′ : A → List A → B
  foldr′ x []       = s x
  foldr′ x (y ∷ xs) = c x (foldr′ y xs)

-- Right fold.

foldr₁ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldr₁ f = foldr f id

-- Left fold. Note that s is only applied to the first element (see
-- the examples below).

foldl : ∀ {a b} {A : Set a} {B : Set b} →
        (B → A → B) → (A → B) → List⁺ A → B
foldl c s (x ∷ xs) = List.foldl c (s x) xs

-- Left fold.

foldl₁ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldl₁ f = foldl f id

-- Append (several variants).

module _ {a} {A : Set a} where

  infixr 5 _⁺++⁺_ _++⁺_ _⁺++_

  _⁺++⁺_ : List⁺ A → List⁺ A → List⁺ A
  (x ∷ xs) ⁺++⁺ (y ∷ ys) = x ∷ (xs List.++ y ∷ ys)

  _⁺++_ : List⁺ A → List A → List⁺ A
  (x ∷ xs) ⁺++ ys = x ∷ (xs List.++ ys)

  _++⁺_ : List A → List⁺ A → List⁺ A
  xs ++⁺ ys = List.foldr _∷⁺_ ys xs

  concat : List⁺ (List⁺ A) → List⁺ A
  concat (xs ∷ xss) = xs ⁺++ List.concat (List.map toList xss)

concatMap : ∀ {a b} {A : Set a} {B : Set b} → (A → List⁺ B) → List⁺ A → List⁺ B
concatMap f = concat ∘′ map f

-- Reverse

reverse : ∀ {a} {A : Set a} → List⁺ A → List⁺ A
reverse = lift (-,_ ∘′ Vec.reverse)

-- Align and Zip

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where

  alignWith : (These A B → C) → List⁺ A → List⁺ B → List⁺ C
  alignWith f (a ∷ as) (b ∷ bs) = f (these a b) ∷ List.alignWith f as bs

  zipWith : (A → B → C) → List⁺ A → List⁺ B → List⁺ C
  zipWith f (a ∷ as) (b ∷ bs) = f a b ∷ List.zipWith f as bs

  unalignWith : (A → These B C) → List⁺ A → These (List⁺ B) (List⁺ C)
  unalignWith f = foldr (These.alignWith mcons mcons ∘′ f)
                        (These.map [_] [_] ∘′ f)

    where mcons : ∀ {e} {E : Set e} → These E (List⁺ E) → List⁺ E
          mcons = These.fold [_] id _∷⁺_

  unzipWith : (A → B × C) → List⁺ A → List⁺ B × List⁺ C
  unzipWith f (a ∷ as) = Prod.zip _∷_ _∷_ (f a) (List.unzipWith f as)

module _ {a b} {A : Set a} {B : Set b} where

  align : List⁺ A → List⁺ B → List⁺ (These A B)
  align = alignWith id

  zip : List⁺ A → List⁺ B → List⁺ (A × B)
  zip = zipWith _,_

  unalign : List⁺ (These A B) → These (List⁺ A) (List⁺ B)
  unalign = unalignWith id

  unzip : List⁺ (A × B) → List⁺ A × List⁺ B
  unzip = unzipWith id

-- Snoc.

infixl 5 _∷ʳ_ _⁺∷ʳ_

_∷ʳ_ : ∀ {a} {A : Set a} → List A → A → List⁺ A
[]       ∷ʳ y = [ y ]
(x ∷ xs) ∷ʳ y = x ∷ (xs List.∷ʳ y)

_⁺∷ʳ_ : ∀ {a} {A : Set a} → List⁺ A → A → List⁺ A
xs ⁺∷ʳ x = toList xs ∷ʳ x

-- A snoc-view of non-empty lists.

infixl 5 _∷ʳ′_

data SnocView {a} {A : Set a} : List⁺ A → Set a where
  _∷ʳ′_ : (xs : List A) (x : A) → SnocView (xs ∷ʳ x)

snocView : ∀ {a} {A : Set a} (xs : List⁺ A) → SnocView xs
snocView (x ∷ xs)              with List.initLast xs
snocView (x ∷ .[])             | []            = []       ∷ʳ′ x
snocView (x ∷ .(xs List.∷ʳ y)) | xs List.∷ʳ' y = (x ∷ xs) ∷ʳ′ y

-- The last element in the list.

last : ∀ {a} {A : Set a} → List⁺ A → A
last xs with snocView xs
last .(ys ∷ʳ y) | ys ∷ʳ′ y = y

-- Groups all contiguous elements for which the predicate returns the
-- same result into lists.

split : ∀ {a} {A : Set a}
        (p : A → Bool) → List A →
        List (List⁺ (∃ (T ∘ p)) ⊎ List⁺ (∃ (T ∘ not ∘ p)))
split p []       = []
split p (x ∷ xs) with p x | P.inspect p x | split p xs
... | true  | P.[ px≡t ] | inj₁ xs′ ∷ xss = inj₁ ((x , Eq.from T-≡     ⟨$⟩ px≡t) ∷⁺ xs′) ∷ xss
... | true  | P.[ px≡t ] | xss            = inj₁ [ x , Eq.from T-≡     ⟨$⟩ px≡t ]        ∷ xss
... | false | P.[ px≡f ] | inj₂ xs′ ∷ xss = inj₂ ((x , Eq.from T-not-≡ ⟨$⟩ px≡f) ∷⁺ xs′) ∷ xss
... | false | P.[ px≡f ] | xss            = inj₂ [ x , Eq.from T-not-≡ ⟨$⟩ px≡f ]        ∷ xss

-- If we flatten the list returned by split, then we get the list we
-- started with.

flatten : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} →
          List (List⁺ (∃ P) ⊎ List⁺ (∃ Q)) → List A
flatten = List.concat ∘
          List.map Sum.[ toList ∘ map proj₁ , toList ∘ map proj₁ ]

flatten-split :
  ∀ {a} {A : Set a}
  (p : A → Bool) (xs : List A) → flatten (split p xs) ≡ xs
flatten-split p []       = refl
flatten-split p (x ∷ xs)
  with p x | P.inspect p x | split p xs | flatten-split p xs
... | true  | P.[ _ ] | []         | hyp = P.cong (_∷_ x) hyp
... | true  | P.[ _ ] | inj₁ _ ∷ _ | hyp = P.cong (_∷_ x) hyp
... | true  | P.[ _ ] | inj₂ _ ∷ _ | hyp = P.cong (_∷_ x) hyp
... | false | P.[ _ ] | []         | hyp = P.cong (_∷_ x) hyp
... | false | P.[ _ ] | inj₁ _ ∷ _ | hyp = P.cong (_∷_ x) hyp
... | false | P.[ _ ] | inj₂ _ ∷ _ | hyp = P.cong (_∷_ x) hyp

-- Groups all contiguous elements /not/ satisfying the predicate into
-- lists. Elements satisfying the predicate are dropped.

wordsBy : ∀ {a} {A : Set a} → (A → Bool) → List A → List (List⁺ A)
wordsBy p =
  List.mapMaybe Sum.[ const nothing , just ∘′ map proj₁ ] ∘ split p

------------------------------------------------------------------------
-- Examples

-- Note that these examples are simple unit tests, because the type
-- checker verifies them.

private
 module Examples {A B : Set}
                 (_⊕_ : A → B → B)
                 (_⊗_ : B → A → B)
                 (_⊙_ : A → A → A)
                 (f : A → B)
                 (a b c : A)
                 where

  hd : head (a ∷⁺ b ∷⁺ [ c ]) ≡ a
  hd = refl

  tl : tail (a ∷⁺ b ∷⁺ [ c ]) ≡ b ∷ c ∷ []
  tl = refl

  mp : map f (a ∷⁺ b ∷⁺ [ c ]) ≡ f a ∷⁺ f b ∷⁺ [ f c ]
  mp = refl

  right : foldr _⊕_ f (a ∷⁺ b ∷⁺ [ c ]) ≡ (a ⊕ (b ⊕ f c))
  right = refl

  right₁ : foldr₁ _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ (a ⊙ (b ⊙ c))
  right₁ = refl

  left : foldl _⊗_ f (a ∷⁺ b ∷⁺ [ c ]) ≡ ((f a ⊗ b) ⊗ c)
  left = refl

  left₁ : foldl₁ _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ ((a ⊙ b) ⊙ c)
  left₁ = refl

  ⁺app⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺++⁺ (b ∷⁺ [ c ]) ≡
          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
  ⁺app⁺ = refl

  ⁺app : (a ∷⁺ b ∷⁺ [ c ]) ⁺++ (b ∷ c ∷ []) ≡
          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
  ⁺app = refl

  app⁺ : (a ∷ b ∷ c ∷ []) ++⁺ (b ∷⁺ [ c ]) ≡
          a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
  app⁺ = refl

  conc : concat ((a ∷⁺ b ∷⁺ [ c ]) ∷⁺ [ b ∷⁺ [ c ] ]) ≡
         a ∷⁺ b ∷⁺ c ∷⁺ b ∷⁺ [ c ]
  conc = refl

  rev : reverse (a ∷⁺ b ∷⁺ [ c ]) ≡ c ∷⁺ b ∷⁺ [ a ]
  rev = refl

  snoc : (a ∷ b ∷ c ∷ []) ∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ]
  snoc = refl

  snoc⁺ : (a ∷⁺ b ∷⁺ [ c ]) ⁺∷ʳ a ≡ a ∷⁺ b ∷⁺ c ∷⁺ [ a ]
  snoc⁺ = refl

  split-true : split (const true) (a ∷ b ∷ c ∷ []) ≡
               inj₁ ((a , tt) ∷⁺ (b , tt) ∷⁺ [ c , tt ]) ∷ []
  split-true = refl

  split-false : split (const false) (a ∷ b ∷ c ∷ []) ≡
                inj₂ ((a , tt) ∷⁺ (b , tt) ∷⁺ [ c , tt ]) ∷ []
  split-false = refl

  split-≡1 :
    split (λ n → ⌊ n Nat.≟ 1 ⌋) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡
    inj₁ [ 1 , tt ] ∷ inj₂ ((2 , tt) ∷⁺ [ 3 , tt ]) ∷
    inj₁ ((1 , tt) ∷⁺ [ 1 , tt ]) ∷ inj₂ [ 2 , tt ] ∷ inj₁ [ 1 , tt ] ∷
    []
  split-≡1 = refl

  wordsBy-true : wordsBy (const true) (a ∷ b ∷ c ∷ []) ≡ []
  wordsBy-true = refl

  wordsBy-false : wordsBy (const false) (a ∷ b ∷ c ∷ []) ≡
                  (a ∷⁺ b ∷⁺ [ c ]) ∷ []
  wordsBy-false = refl

  wordsBy-≡1 :
    wordsBy (λ n → ⌊ n Nat.≟ 1 ⌋) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡
    (2 ∷⁺ [ 3 ]) ∷ [ 2 ] ∷ []
  wordsBy-≡1 = refl


text:
module Type.Properties.Singleton.Proofs where

import      Data.Tuple as Tuple
open import Data.Proofs
open import Function.Axioms
open import Logic.Classical
open import Logic
import      Lvl
open import Type.Properties.Empty
open import Type.Properties.Inhabited
open import Type.Properties.MereProposition
open import Type.Properties.Singleton
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Type.Identity
open import Syntax.Function
open import Type.Dependent
open import Type

private variable ℓ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₑ₄ ℓₑ₅ : Lvl.Level
private variable A B T U P : Type{ℓ}

module _ ⦃ equiv : Equiv{ℓₑ}(U) ⦄ where
  unit-is-pos : ⦃ proof : IsUnit(U) ⦄ → ◊(U)
  unit-is-pos ⦃ intro unit uniqueness ⦄ = intro ⦃ unit ⦄

  unit-is-prop : ⦃ proof : IsUnit(U) ⦄ → MereProposition(U)
  unit-is-prop ⦃ intro unit uniqueness ⦄ = intro (\{x}{y} → transitivity(_≡_) (uniqueness{x}) (symmetry(_≡_)(uniqueness{y})))

  pos-prop-is-unit : ⦃ _ : (◊ U) ⦄ → ⦃ _ : MereProposition(U) ⦄ → IsUnit(U)
  pos-prop-is-unit ⦃ intro ⦃ unit ⦄ ⦄ ⦃ intro uniqueness ⦄ = intro unit (\{x} → uniqueness{x}{unit})

module _ ⦃ equiv-p : Equiv{ℓₑ}(P) ⦄ ⦃ prop-p : MereProposition(P) ⦄ ⦃ equiv-a : Equiv{ℓₑ₁}(A) ⦄ where
  prop-fn-unique-value : ∀{f : P → A} → ⦃ _ : Function(f) ⦄ → (∀{x y} → (f(x) ≡ f(y)))
  prop-fn-unique-value {f = f}{x}{y} = congruence₁(f) (MereProposition.uniqueness(prop-p){x}{y})

module _ ⦃ equiv-u : Equiv{ℓₑ}(U) ⦄ ⦃ unit-u : IsUnit(U) ⦄ ⦃ equiv-a : Equiv{ℓₑ₁}(A) ⦄ where
  unit-fn-unique-value : ∀{f : U → A} → ⦃ _ : Function(f) ⦄ → (∀{x y} → (f(x) ≡ f(y)))
  unit-fn-unique-value = prop-fn-unique-value ⦃ prop-p = unit-is-prop ⦃ proof = unit-u ⦄ ⦄

module _
  ⦃ equiv-a : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-b : Equiv{ℓₑ₂}(B) ⦄
  ⦃ equiv-ab : Equiv{ℓₑ₃}(A ∧ B) ⦄
  ⦃ op : BinaryOperator([∧]-intro) ⦄ where
  instance
    prop-conjunction : ⦃ prop-a : MereProposition(A) ⦄ ⦃ prop-b : MereProposition(B) ⦄ → MereProposition(A ∧ B)
    MereProposition.uniqueness prop-conjunction {[∧]-intro a₁ b₁} {[∧]-intro a₂ b₂} = congruence₂([∧]-intro) (uniqueness(A)) (uniqueness(B))

module _
  ⦃ equiv-b : Equiv{ℓₑ₁}(B) ⦄
  ⦃ equiv-ab : Equiv{ℓₑ₂}(A → B) ⦄
  ⦃ funcExt : FunctionExtensionality(A)(B) ⦄
  where
  prop-implication : ⦃ prop-b : MereProposition(B) ⦄ → MereProposition(A → B)
  MereProposition.uniqueness prop-implication = functionExtensionality(A)(B) (uniqueness(B))

module _
  {B : A → Type{ℓ}}
  ⦃ equiv-b : ∀{a} → Equiv{ℓₑ₁}(B(a)) ⦄
  ⦃ equiv-ab : Equiv{ℓₑ₂}((a : A) → B(a)) ⦄
  ⦃ funcExt : DependentFunctionExtensionality(A)(B) ⦄
  where
  prop-dependent-implication : ⦃ prop-b : ∀{a} → MereProposition(B(a)) ⦄ → MereProposition((a : A) → B(a))
  MereProposition.uniqueness prop-dependent-implication = dependentFunctionExtensionality(A)(B)(\{a} → uniqueness(B(a)))

module _ ⦃ equiv-top : Equiv{ℓₑ}(⊤) ⦄ where
  instance
    prop-top : MereProposition(⊤) ⦃ equiv-top ⦄
    prop-top = unit-is-prop

module _ ⦃ equiv-bottom : Equiv{ℓₑ}(⊥) ⦄ where
  instance
    prop-bottom : MereProposition(⊥) ⦃ equiv-bottom ⦄
    MereProposition.uniqueness prop-bottom {}

module _
  {P : A → Type{ℓ}} ⦃ equiv-p : ∀{x} → Equiv{ℓₑ₁}(P(x)) ⦄
  ⦃ equiv-ap : Equiv{ℓₑ₂}(∀ₗ P) ⦄
  ⦃ funcExt : DependentImplicitFunctionExtensionality(A)(P) ⦄
  where
  prop-universal : ⦃ prop-p : ∀{x} → MereProposition(P(x)) ⦄ → MereProposition(∀ₗ P)
  MereProposition.uniqueness prop-universal = dependentImplicitFunctionExtensionality(A)(P) (\{x} → uniqueness(P(x)))

module _
  ⦃ equiv-a : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-b : Equiv{ℓₑ₂}(B) ⦄
  ⦃ equiv-ba : Equiv{ℓₑ₃}(A ← B) ⦄
  ⦃ equiv-ab : Equiv{ℓₑ₄}(A → B) ⦄
  ⦃ equiv-eq : Equiv{ℓₑ₅}(A ↔ B) ⦄
  ⦃ op : BinaryOperator([↔]-intro) ⦄
  ⦃ funcExtₗ : FunctionExtensionality(B)(A) ⦄
  ⦃ funcExtᵣ : FunctionExtensionality(A)(B) ⦄
  where
  prop-equivalence : ⦃ prop-a : MereProposition(A) ⦄ → ⦃ prop-b : MereProposition(B) ⦄ → MereProposition(A ↔ B)
  prop-equivalence = prop-conjunction ⦃ prop-a = prop-implication ⦄ ⦃ prop-b = prop-implication ⦄

module _
  ⦃ equiv-a      : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-bottom : Equiv{ℓₑ₂}(⊥) ⦄
  ⦃ equiv-na     : Equiv{ℓₑ₃}(¬ A) ⦄
  ⦃ funcExt : FunctionExtensionality (A)(⊥) ⦃ equiv-bottom ⦄ ⦄
  where
  prop-negation : MereProposition(¬ A)
  prop-negation = prop-implication

module _
  ⦃ equiv-a : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-b : Equiv{ℓₑ₂}(B) ⦄
  ⦃ equiv-ab : Equiv{ℓₑ₃}(A ∨ B) ⦄
  (left-right-neq : ∀{a : A}{b : B} → ([∨]-introₗ a ≢ [∨]-introᵣ b))
  where
  not-prop-disjunction : MereProposition(A ∨ B) → IsEmpty(A ∧ B)
  IsEmpty.empty (not-prop-disjunction (intro uniqueness)) ([∧]-intro a b) with () ← left-right-neq(uniqueness{[∨]-introₗ a}{[∨]-introᵣ b})

{-
module _ {B : A → Type{ℓ}} where
  open import Type.Identity
  open import Relator.Equals.Proofs.Equiv
  open import Structure.Relator
  open import Structure.Setoid.Uniqueness
  open import Syntax.Transitivity

  congruence₁-dependent : ∀{ℓ₁ ℓ₂}{A : Type{ℓ₁}}{B : A → Type{ℓ₂}}{a₁ a₂ : A} → (f : (a : A) → B(a)) → (pa : a₁ ≡ a₂) → (substitute₁(B) pa (f a₁) ≡ f a₂)
  congruence₁-dependent _ intro = intro

  -- congruence₂-dependent : ∀{C : (a : A) → B(a) → Type{ℓ}}{a₁ a₂ : A}{b₁ : B(a₁)}{b₂ : B(a₂)}{f : (a : A) → (b : B(a)) → C a b} → (pa : a₁ ≡ a₂) → (f a₁ b₁ ≡ f a₂ b₂)
  -- (substitute₁(B) ? b₁)

  prop-sigma : Unique(B) → (∀{a} → MereProposition(B(a))) → MereProposition(Σ A B)
  MereProposition.uniqueness (prop-sigma unique-B prop-B) {intro xa xb} {intro ya yb} =
    intro xa xb                                   🝖[ _≡_ ]-[ {!(congruence₁-dependent(intro) (unique-B xb yb))!} ]
    intro ya (substitute₁(B) (unique-B xb yb) xb) 🝖[ _≡_ ]-[ {!intro xa xb!} ]
    intro ya yb                                   🝖-end
-}

{- TODO
module _
  ⦃ equiv-a : Equiv(A) ⦄
  {B : A → Type{ℓ}} ⦃ equiv-b : ∀{x} → Equiv(B(x)) ⦄
  ⦃ equiv-sigma : Equiv(Σ A B) ⦄ -- TODO: Not an arbitrary one
  where
  prop-sigma : MereProposition(Σ A B) → ? -- TODO: Maybe MereProposition(B) → MereProposition(A)
  prop-sigma (intro uniqueness₁) = {!!}
-}

{- TODO: Maybe generalize and move the stuff from Data.Proofs to here
-- Any binary relation on Unit is an equivalence given that it is reflexive.
module _ ⦃ equiv-u : Equiv(U) ⦄ ⦃ is-unit : IsUnit(U) ⦄ {_▫_ : U → U → Stmt} where
  unit-equiv : Equiv(U)
  Equiv._≡_ unit-equiv = (_▫_)
  Reflexivity.proof  (Equivalence.reflexivity  (Equiv.equivalence unit-equiv))       = {!!}
  Symmetry.proof     (Equivalence.symmetry     (Equiv.equivalence unit-equiv)) _     = {!!}
  Transitivity.proof (Equivalence.transitivity (Equiv.equivalence unit-equiv)) _ _   = {!!}
-}

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:
-- Shadowing is allowed.
module Shadow where

module M (A : Set) where

  id : Set -> Set
  id A = A

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Base
open import Homotopy.Connected

{-
    Wedge is a pushout.
-}

module Homotopy.Wedge
  where

  import Homotopy.Pushout as P

  record wedge-diag i : Set (suc i) where
    constructor diag_,_,_,_
    field
      A : Set i
      B : Set i
      a : A
      b : B

    f : unit {i} → A
    f _ = a
    g : unit {i} → B
    g _ = b

  wedge-diag-to-pushout-diag : ∀ {i} → wedge-diag i → P.pushout-diag i
  wedge-diag-to-pushout-diag {i} (diag A , B , a , b) = P.diag A , B , unit {i} , (λ _ → a) , (λ _ → b)

  wedge : ∀ {i} → wedge-diag i → Set i
  wedge d = P.pushout (wedge-diag-to-pushout-diag d)

  left : ∀ {i} {d : wedge-diag i} → wedge-diag.A d → wedge d
  left = P.left

  right : ∀ {i} {d : wedge-diag i} → wedge-diag.B d → wedge d
  right = P.right

  glue : ∀ {i} {d : wedge-diag i} → left (wedge-diag.a d) ≡ right (wedge-diag.b d)
  glue = P.glue tt

  wedge-rec : ∀ {i} {d : wedge-diag i}
    → let open wedge-diag d in
    ∀ {j} (P : wedge d → Set j)
    (left* : ∀ a → P (left a))
    (right* : ∀ b → P (right b))
    (glue* : transport P glue (left* a) ≡ right* b)
    → (∀ x → P x)
  wedge-rec P left* right* glue* = P.pushout-rec P left* right* (λ _ → glue*)

  wedge-rec-nondep : ∀ {i} {d : wedge-diag i}
    → let open wedge-diag d in
    ∀ {j} (P : Set j)
    (left* : ∀ a → P)
    (right* : ∀ b → P)
    (glue* : left* a ≡ right* b)
    → (wedge d → P)
  wedge-rec-nondep P left* right* glue* = P.pushout-rec-nondep P left* right* (λ _ → glue*)

{-
  module _ (f : X → Y) where
  nA (A-is-conn : is-connected n A)
  nB (B-is-conn : is-connected n B)
  (P : A → B → Set k)
  ⦃ P-is-trunc : ∀ a b → is-connected (n +2+ m) (P a b) ⦄
    extension :
-}

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- Patterns are parsed as expressions. That means that expressions can contain
-- pattern parts. That's of course not ok.
module NotAnExpression where

X = x @ y -- as pattern as an expression

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.Bin.BitListBijection where

--
-- This module gives a bijection between the two setoids:
-- - the set (ℕ)
-- - The set (List Bit), interpreted as least-significant-bit first,
--   with the equivalence relation that ignores the zeroes at the end of the list

  open import Data.List
  open import Data.List.Properties
  import Data.Digit
  open Data.Digit using (Bit)
  open import Data.Fin using (zero; suc; Fin; inject₁) renaming (toℕ to finToℕ)
  open import Data.Nat using (ℕ; zero;suc)
  open import Data.Nat using (_+_)
  open import Data.Nat.Properties using (+-suc; +-identityʳ) renaming (suc-injective to suc-inj)
  open import Data.Fin.Properties using () renaming (suc-injective to fin-suc-inj)

  infix 3 _≈_

  0×_ : ℕ → List Bit
  0× n = replicate n zero

  open import Relation.Binary using (IsEquivalence; Setoid; Reflexive; Symmetric; Transitive)
  import Relation.Binary.PropositionalEquality
  module PropEq = Relation.Binary.PropositionalEquality
  open import Algebra
  import Level

  open import Algebra.FunctionProperties
  open import Data.Product renaming (map to pmap)

  ₀ = Level.zero

  open PropEq using (_≡_)

  []-identityʳ : ∀ l → l ++ [] ≡ l
  []-identityʳ = proj₂ (Monoid.identity (Data.List.Properties.++-monoid Bit))

  patternMatch : ∀ {A : Set} (P : A → Set) {x} → P x → ∃ λ z → P z × x ≡ z
  patternMatch _ {x = x} px = (x , (px , PropEq.refl))

  generalizing_case_of_ : ∀ {a b} {A : Set a} {B : Set b} → (P : A → Set) → ∀ {x} → P x → (∀ {z} → P z → x ≡ z → B) → B
  generalizing P case p of f = f p PropEq.refl

  open import Data.Sum

  open import Function

  open import Data.Digit

  data All-zero : List Bit → Set where
    [] : All-zero []
    cons : ∀ {t} → All-zero t → All-zero (0b ∷ t)

  -- ᵢ for "Inductive"
  data _≈_ : List Bit → List Bit → Set where
    both-zero : ∀ {a b} (a-zero : All-zero a) (b-zero : All-zero b) → a ≈ b
    heads-match : ∀ h at bt → at ≈ bt → (h ∷ at) ≈ (h ∷ bt)

  All-zero-respects-equivalence : ∀ {x y} → x ≈ y → All-zero x → All-zero y
  All-zero-respects-equivalence (both-zero a-zero b-zero) z = b-zero
  All-zero-respects-equivalence (heads-match .zero at bt eq) (cons z) = cons (All-zero-respects-equivalence eq z)

  ≈-sym : ∀ {a b} → a ≈ b → b ≈ a
  ≈-sym (both-zero a-zero b-zero) = both-zero b-zero a-zero
  ≈-sym (heads-match h at bt l) = heads-match h bt at (≈-sym l)

  ≈-trans : ∀ {a b c} → a ≈ b → b ≈ c → a ≈ c
  ≈-trans (both-zero a-zero b-zero) b≈c = both-zero a-zero (All-zero-respects-equivalence b≈c b-zero)
  ≈-trans a≈b (both-zero b-zero c-zero) = both-zero (All-zero-respects-equivalence (≈-sym a≈b) b-zero) c-zero
  ≈-trans (heads-match h at bt r1) (heads-match .h .bt bt₁ r2) = heads-match h _ _ (≈-trans r1 r2)

  0×-is-all-zero : ∀ {n} → All-zero (0× n)
  0×-is-all-zero {ℕ.zero} = []
  0×-is-all-zero {ℕ.suc n} = cons 0×-is-all-zero

  az-replicate : ∀ {a} → All-zero a → (0× length a) ≡ a
  az-replicate [] = PropEq.refl
  az-replicate (cons x) = PropEq.cong (λ z → 0b ∷ z) (az-replicate x)

  ≈-refl : Reflexive _≈_
  ≈-refl {[]} = both-zero [] []
  ≈-refl {x ∷ x₁} = heads-match x x₁ x₁ ≈-refl

  ≡→≈ : ∀ {x y} → x ≡ y → x ≈ y
  ≡→≈ {x} .{x} PropEq.refl = ≈-refl {x}

  isEquivalence : IsEquivalence _≈_
  isEquivalence = record
    { refl = ≈-refl
    ; trans = ≈-trans
    ; sym = ≈-sym
    }

  setoid : Setoid ₀ ₀
  setoid = record {isEquivalence = isEquivalence}

  toℕ : List Bit → ℕ
  toℕ = fromDigits

  open import Function using (_∘_; _⟨_⟩_)
  fromℕ : ℕ → List Bit
  fromℕ = proj₁ ∘ toDigits 2

  ℕ-setoid = PropEq.setoid ℕ

  open import Function using (id)
  open import Function.Bijection using (Bijection; Bijective)
  open import Function.Equality using (_⟶_)

  zeroIsZero : ∀ {l} → All-zero l → toℕ l ≡ 0
  zeroIsZero [] = PropEq.refl
  zeroIsZero (cons q) rewrite zeroIsZero q = PropEq.refl

  toℕ-cong : ∀ {x y} → x ≈ y → toℕ x ≡ toℕ y
  toℕ-cong (both-zero a-zero b-zero) =
    PropEq.trans (zeroIsZero a-zero) (PropEq.sym (zeroIsZero b-zero))
  toℕ-cong (heads-match h at bt q) rewrite toℕ-cong q = PropEq.refl

  fromℕ⟶ : ℕ-setoid ⟶ setoid
  fromℕ⟶ = record
    { _⟨$⟩_ = fromℕ
    ; cong = λ eq → ≡→≈ (PropEq.cong fromℕ eq)
    }

  toℕ⟶ : setoid ⟶ ℕ-setoid
  toℕ⟶ = record
    { _⟨$⟩_ = toℕ
    ; cong = toℕ-cong
    }

  fromℕ-inj : ∀ {x y} → fromℕ x ≈ fromℕ y → x ≡ y
  fromℕ-inj {x} {y} eq =
    PropEq.trans
      (PropEq.sym (proj₂ (toDigits 2 x)))
      (PropEq.trans
        (toℕ-cong eq)
        (proj₂ (toDigits 2 y)))

  open import Data.Nat.DivMod

  bitToℕ : Bit → ℕ
  bitToℕ = Data.Fin.toℕ

  open Data.Nat using (_*_)
  +-inj₁ : ∀ c {a b} → c + a ≡ c + b → a ≡ b
  +-inj₁ zero eq = eq
  +-inj₁ (suc c) {a} {b} eq = +-inj₁ c {a} {b} (suc-inj eq)

  module DigitInj where
    open import Data.Nat.Properties using (isCommutativeSemiring)
    open import Algebra.Structures
    open IsCommutativeSemiring isCommutativeSemiring hiding (zero)
    open import Data.Empty using (⊥; ⊥-elim)

    finToℕ-inj : ∀ {base} {x y : Fin base} → finToℕ x ≡ finToℕ y → x ≡ y
    finToℕ-inj {.(suc _)} {zero} {zero} eq = PropEq.refl
    finToℕ-inj {.(suc _)} {zero} {suc y} ()
    finToℕ-inj {.(suc _)} {suc x} {zero} ()
    finToℕ-inj {.(suc _)} {suc x} {suc y} eq = PropEq.cong suc (finToℕ-inj (suc-inj eq))

    fin-not-enough : ∀ {base} → (x : Fin base) → ∀ whatever → finToℕ x ≡ base + whatever → ⊥
    fin-not-enough {.(suc _)} zero _ ()
    fin-not-enough {.(suc _)} (suc x) _ eq = fin-not-enough _ _ (Data.Nat.Properties.suc-injective eq)

    digit-inj2 : ∀ {base : ℕ} (h₁ h₂ : Fin base) (t₁ t₂ : ℕ)
                →   t₁ * base + finToℕ h₁
                  ≡ t₂ * base + finToℕ h₂
                → h₁ ≡ h₂ × t₁ ≡ t₂
    digit-inj2 x y zero zero eq = finToℕ-inj eq , PropEq.refl
    digit-inj2 {base} x y zero (suc ys) eq =
      ⊥-elim (fin-not-enough x (ys * base + finToℕ y) (PropEq.trans eq (+-assoc _ (ys * base) (finToℕ y))))
    digit-inj2 {base} x y (suc xs) zero eq =
      ⊥-elim (fin-not-enough y (xs * base + finToℕ x) (PropEq.trans (PropEq.sym eq) (+-assoc _ (xs * base) (finToℕ x))))
    digit-inj2 {base} x y (suc xs) (suc ys) eq =
       case digit-inj2 x y xs ys (+-inj₁ base  eq') of
       λ { (eq1 , eq2) → eq1 , PropEq.cong suc eq2 } where
      eq' =
        PropEq.trans
          (PropEq.sym (+-assoc base (xs * base) _))
          (PropEq.trans eq
            (+-assoc base (ys * base) _))

    digit-inj : ∀ {base : ℕ} (h₁ h₂ : Fin base) (t₁ t₂ : ℕ)
                →   finToℕ h₁ + t₁ * base
                  ≡ finToℕ h₂ + t₂ * base
                → h₁ ≡ h₂ × t₁ ≡ t₂
    digit-inj x y xs ys eq =
      digit-inj2 _ _ _ _ (PropEq.trans (+-comm (xs * _) (finToℕ x)) (PropEq.trans eq (+-comm _ (ys * _))))

  digit-inj = DigitInj.digit-inj

  toℕ-inj-zero : ∀ xs → toℕ xs ≡ 0 → All-zero xs
  toℕ-inj-zero [] eq = []
  toℕ-inj-zero (x ∷ xs) eq =
    case digit-inj x zero (toℕ xs) 0 eq of
      λ { (PropEq.refl , snd) → cons (toℕ-inj-zero xs snd) }

  toℕ-inj2 : ∀ {x y} → toℕ x ≡ toℕ y → x ≈ y
  toℕ-inj2 {[]} {ys} eq = both-zero [] (toℕ-inj-zero ys (PropEq.sym eq))
  toℕ-inj2 {xs} {[]} eq = both-zero (toℕ-inj-zero xs eq) []
  toℕ-inj2 {x ∷ xs} {y ∷ ys} eq =
    case digit-inj x y (fromDigits xs) (fromDigits ys) eq of
      λ { (PropEq.refl , eq) → heads-match x xs ys (toℕ-inj2 eq) }

  bijective : Bijective toℕ⟶
  bijective = record
    { injective = toℕ-inj2
    ; surjective = record
       { from = fromℕ⟶
       ; right-inverse-of = proj₂ ∘ toDigits 2
       }
    }

  bijection-to-ℕ : Bijection setoid ℕ-setoid
  bijection-to-ℕ = record { bijective = bijective }

max_stars_repo_name: Rotsor/BinDivMod

max_issues_repo_name: Rotsor/BinDivMod

max_forks_repo_name: Rotsor/BinDivMod


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Conat type and some operations
------------------------------------------------------------------------

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

module Codata.Conat where

open import Size
open import Codata.Thunk

open import Data.Nat.Base using (ℕ ; zero ; suc)
open import Relation.Nullary

------------------------------------------------------------------------
-- Definition and first values

data Conat (i : Size) : Set where
  zero : Conat i
  suc : Thunk Conat i → Conat i

infinity : ∀ {i} → Conat i
infinity = suc λ where .force → infinity

fromℕ : ℕ → Conat ∞
fromℕ zero    = zero
fromℕ (suc n) = suc λ where .force → fromℕ n

------------------------------------------------------------------------
-- Arithmetic operations

pred : ∀ {i} {j : Size< i} → Conat i → Conat j
pred zero    = zero
pred (suc n) = n .force

infixl 6 _∸_ _+_
infixl 7 _*_

_∸_ : Conat ∞ → ℕ → Conat ∞
m ∸ zero  = m
m ∸ suc n = pred m ∸ n

_ℕ+_ : ℕ → ∀ {i} → Conat i → Conat i
zero  ℕ+ n = n
suc m ℕ+ n = suc λ where .force → m ℕ+ n

_+ℕ_ : ∀ {i} → Conat i → ℕ → Conat i
zero  +ℕ n = fromℕ n
suc m +ℕ n = suc λ where .force → (m .force) +ℕ n

_+_ : ∀ {i} → Conat i → Conat i → Conat i
zero  + n = n
suc m + n = suc λ where .force → (m .force) + n

_*_ : ∀ {i} → Conat i → Conat i → Conat i
m     * zero  = zero
zero  * n     = zero
suc m * suc n = suc λ where .force → n .force + (m .force * suc n)

-- Max and Min

infixl 6 _⊔_
infixl 7 _⊓_

_⊔_ : ∀ {i} → Conat i → Conat i → Conat i
zero  ⊔ n     = n
m     ⊔ zero  = m
suc m ⊔ suc n = suc λ where .force → m .force ⊔ n .force

_⊓_ : ∀ {i} → Conat i → Conat i → Conat i
zero  ⊓ n     = zero
m     ⊓ zero  = zero
suc m ⊓ suc n = suc λ where .force → m .force ⊔ n .force

------------------------------------------------------------------------
-- Finiteness

data Finite : Conat ∞ → Set where
  zero : Finite zero
  suc  : ∀ {n} → Finite (n .force) → Finite (suc n)

toℕ : ∀ {n} → Finite n → ℕ
toℕ zero    = zero
toℕ (suc n) = suc (toℕ n)

¬Finite∞ : ¬ (Finite infinity)
¬Finite∞ (suc p) = ¬Finite∞ p

------------------------------------------------------------------------
-- Order wrt to Nat

data _ℕ≤_ : ℕ → Conat ∞ → Set where
  zℕ≤n : ∀ {n} → zero ℕ≤ n
  sℕ≤s : ∀ {k n} → k ℕ≤ n .force → suc k ℕ≤ suc n

_ℕ<_ : ℕ → Conat ∞ → Set
k ℕ< n = suc k ℕ≤ n

_ℕ≤infinity : ∀ k → k ℕ≤ infinity
zero  ℕ≤infinity = zℕ≤n
suc k ℕ≤infinity = sℕ≤s (k ℕ≤infinity)


text:
{-# OPTIONS --rewriting --prop --confluence-check --cumulativity  #-}

open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Data.Vec.Base
open import Data.Bool
open import Data.Sum
open import Data.Product using (_×_)
open import ett-rr

{- Axiomatisation of the Cast calculus -}

{- diagonal cases -}

postulate cast : (A : Set ℓ) (B : Set ℓ₁) → A → B

postulate cast-set : (A : Set ℓ) → cast (Set ℓ) (Set ℓ) A ≡ A

{-# REWRITE cast-set #-}

postulate cast-prop : (A : Prop ℓ) → cast (Prop ℓ) (Prop ℓ) A ≡ A

{-# REWRITE cast-prop #-}

postulate cast-Pi : (A : Set ℓ) (B : A → Set ℓ₁) (A' : Set ℓ₂) (B' : A' → Set ℓ₃) (f : (a : A) → B a)  →
                    cast ((a : A) → B a) ((a' : A') → B' a') f ≡
                    λ (a' : A') → cast _ _ (f (cast A' A a'))

{-# REWRITE cast-Pi #-}

postulate cast-Sigma : (A : Set ℓ) (B : A → Set ℓ₁) (A' : Set ℓ₂) (B' : A' → Set ℓ₃) (p : Σ {a = ℓ} {b = ℓ₁} A B) →
                       cast (Σ A B) (Σ A' B') p ≡ (cast {ℓ = ℓ} {ℓ₁ = ℓ₂} A A' (p .fst) , cast (B (p .fst)) (B' (cast A A' (p .fst))) (p .snd))

{-# REWRITE cast-Sigma #-}

postulate cast-Sum-inj₁ : (A A' : Set ℓ) (B B' : Set ℓ₁) (a : A) →
                    cast (A ⊎ B) (A' ⊎ B') (inj₁ a) ≡ inj₁ (cast A A' a)

postulate cast-Sum-inj₂ : (A A' : Set ℓ) (B B' : Set ℓ₁) (b : B) →
                    cast (A ⊎ B) (A' ⊎ B') (inj₂ b) ≡ inj₂ (cast B B' b)

postulate cast-Sum-raise : (A A' : Set ℓ) (B B' : Set ℓ₁) (a : A) →
                    cast (A ⊎ B) (A' ⊎ B') (raise _) ≡ raise _

postulate cast-Sum-unk : (A A' : Set ℓ) (B B' : Set ℓ₁) (a : A) →
                    cast (A ⊎ B) (A' ⊎ B') (unk _) ≡ unk _

{-# REWRITE cast-Sum-inj₁ #-}
{-# REWRITE cast-Sum-inj₂ cast-Sum-raise cast-Sum-unk #-}

postulate cast-List-nil : (A A' : Set ℓ) →
                          cast (List A) (List A') [] ≡ []

postulate cast-List-cons : (A A' : Set ℓ) (a : A) (l : List {a = ℓ} A) →
                           cast (List A) (List {a = ℓ} A') (a ∷ l) ≡
                           cast A A' a ∷ cast (List A) (List A') l

postulate cast-List-raise : (A A' : Set ℓ) →
                          cast (List A) (List A') (raise (List _)) ≡ raise (List _)
postulate cast-List-unk : (A A' : Set ℓ) →
                          cast (List A) (List A') (unk (List _)) ≡ unk (List _)

{-# REWRITE cast-List-nil #-}
{-# REWRITE cast-List-cons cast-List-raise cast-List-unk #-}

postulate cast-Nat-zero : cast Nat Nat 0 ≡ 0

postulate cast-Nat-suc : (n : Nat ) → cast Nat Nat (suc n) ≡ suc (cast _ _ n)

postulate cast-Nat-raise : cast Nat Nat (raise Nat) ≡ raise Nat

postulate cast-Nat-unk : cast Nat Nat (unk Nat) ≡ unk Nat

{-# REWRITE cast-Nat-zero cast-Nat-suc cast-Nat-raise cast-Nat-unk #-}

postulate cast-Bool-true : cast Bool Bool true ≡ true

postulate cast-Bool-false : cast Bool Bool false ≡ false

postulate cast-Bool-raise : cast Bool Bool (raise Bool) ≡ raise Bool

postulate cast-Bool-unk : cast Bool Bool (unk Bool) ≡ unk Bool

{-# REWRITE cast-Bool-true cast-Bool-false cast-Bool-raise cast-Bool-unk #-}

postulate cast-Unit : cast ⊤ ⊤ tt ≡ tt
{- Beware that raise ⊤ ≡ tt ≡ unk ⊤ because of definitional singleton -}
postulate cast-Unit-raise : cast ⊤ ⊤ (raise ⊤) ≡ raise ⊤
postulate cast-Unit-unk : cast ⊤ ⊤ (unk ⊤) ≡ unk ⊤

{-# REWRITE cast-Unit cast-Unit-raise cast-Unit-unk #-}

{- non-diagonal cases -}

postulate cast-Set-bad : (A : Set (lsuc ℓ)) → cast (Set (lsuc ℓ)) (Set ℓ) A ≡ raise _

{-# REWRITE cast-Set-bad #-}

postulate cast-raise :  ∀ ℓ ℓ₁ → (x : raise {ℓ = lsuc ℓ} (Set ℓ)) (A : Set ℓ₁) → cast (raise {ℓ = lsuc ℓ} (Set ℓ)) A x ≡ raise _

{-# REWRITE cast-raise #-}

postulate cast-Pi-Sigma : (A A' : Set ℓ) (B : A → Set ℓ₁) (B' : A' → Set ℓ₁) (f : (a : A) → B a)  →
                    cast ((a : A) → B a) (Σ {a = ℓ} {b = ℓ₁} A' B') f ≡ raise (Σ A' B')

{-# REWRITE cast-Pi-Sigma #-}

postulate cast-Pi-Nat : (A : Set ℓ) (B : A → Set ℓ₁) (f : (a : A) → B a) →
                    cast ((a : A) → B a) Nat f ≡ raise Nat

{-# REWRITE cast-Pi-Nat #-}

-- missing many conflict rules

{- Rules specific to Unk -}

{- unk-cast ℓ A a  is just a copy of  cast A (Unk ℓ) a
   but we need to split it off for rewriting.
   Making it private so that the only closed  values we can create in Unk ℓ come from cast -}
private
  postulate unk-cast : ∀ (A : Set ℓ) → A → Unk (lsuc ℓ)

postulate cast-Unk : (A : Set ℓ) (B : Set ℓ₁) (f : A) →
                        cast (Unk (lsuc ℓ)) B (unk-cast A f) ≡ cast A B f
{-# REWRITE cast-Unk #-}

postulate cast-Unk-raise : ∀ ℓ → (B : Set ℓ₁)  →
                           cast (Unk ℓ) B (raise _) ≡ raise _
{-# REWRITE cast-Unk-raise #-}

postulate cast-Pi-Unk : (A : Set ℓ) (B : A → Set ℓ₁) (f : (a : A) → B a) →
                        cast ((a : A) → B a) (Unk (lsuc (ℓ ⊔ ℓ₁))) f ≡  unk-cast (Unk ℓ → Unk ℓ₁) (cast ((a : A) → B a) (Unk ℓ → Unk ℓ₁) f)

{-# REWRITE cast-Pi-Unk #-}

postulate cast-Pi-Unk-bad : (f : Unk ℓ → Unk ℓ₁) →
                            cast (Unk ℓ → Unk ℓ₁) (Unk (ℓ ⊔ ℓ₁)) f ≡ raise _

{-# REWRITE cast-Pi-Unk-bad #-}

postulate cast-Sigma-Unk : (A : Set ℓ) (B : A → Set ℓ₁) (x : Σ {a = ℓ} {b = ℓ₁} A B) →
                        cast (Σ A B) (Unk (lsuc (ℓ ⊔ ℓ₁))) x ≡ unk-cast (_×_ {a = ℓ} {b = ℓ₁} (Unk ℓ) (Unk ℓ₁)) (cast (Σ A B) (Unk ℓ × Unk ℓ₁) x)

{-# REWRITE cast-Sigma-Unk #-}

delta : Unk ℓ → Unk ℓ
delta {ℓ} x = cast (Unk ℓ) (Unk ℓ → Unk ℓ) x x

omega : Unk ℓ
omega {ℓ} = delta {ℓ = ℓ} (cast (Unk ℓ → Unk ℓ) (Unk ℓ) (delta {ℓ = ℓ}))

foo : Unk (lsuc lzero)
foo = cast (Nat → Nat → Nat) (Unk _) _+_

postulate cast-Nat-Unk : (n : Nat) → cast Nat (Unk (lsuc lzero)) n ≡ unk-cast Nat n

record i (A : Set ℓ) : Set (ℓ ⊔ ℓ₁) where
  constructor inj
  field
    uninj : A

open i public

postulate cast-Nat-Unk' : (n : Nat) → cast (i {ℓ = ℓ} {ℓ₁ = ℓ₁} Nat) (Unk (lsuc ℓ)) (inj n) ≡ unk-cast Nat n

postulate cast-Nat-iNat : (n : Nat) → cast Nat (i {ℓ = ℓ} {ℓ₁ = ℓ₁} Nat) n ≡ inj n

{-# REWRITE cast-Nat-Unk cast-Nat-Unk' cast-Nat-iNat #-}

retr : (A : Set ℓ) (a : A) → A
retr {ℓ} A a = cast (Unk (lsuc ℓ)) A (cast A (Unk (lsuc ℓ)) a)

retr-0 : retr {lzero} Nat 0 ≡ 0
retr-0 = refl

retr-arr : (A : Set ℓ) (a : A) → A
retr-arr {ℓ} A = retr (A → A) (λ a → a)

zero' : Nat
zero' = uninj (retr-arr {lsuc lzero} (i {ℓ₁ = lsuc lzero} Nat) (inj 0))

max_stars_repo_name: CoqHott/exceptional-tt

max_issues_repo_name: CoqHott/exceptional-tt

max_forks_repo_name: CoqHott/exceptional-tt


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

   Copyright (c) 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.Concrete.Records
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Concrete.Obligations.PreferredRound
import      LibraBFT.Concrete.Properties.Common          as Common
import      LibraBFT.Concrete.Properties.PreferredRound  as PR
open import LibraBFT.Impl.Consensus.Network              as Network
open import LibraBFT.Impl.Consensus.Network.Properties   as NetworkProps
open import LibraBFT.Impl.Consensus.RoundManager
import      LibraBFT.Impl.Handle                         as Handle
open import LibraBFT.Impl.Handle.Properties
open import LibraBFT.Impl.Handle.InitProperties
open        initHandlerSpec
open import LibraBFT.Impl.IO.OBM.InputOutputHandlers
open import LibraBFT.Impl.IO.OBM.Properties.InputOutputHandlers
open import LibraBFT.Impl.Properties.Common
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Crypto
open import LibraBFT.ImplShared.Util.Dijkstra.All
open        ReachableSystemStateProps
open import LibraBFT.Impl.Properties.Util
open import Optics.All
open import Util.Lemmas
open import Util.PKCS
open import Util.Prelude

open Invariants
open RoundManagerTransProps

open import LibraBFT.Abstract.Types.EpochConfig UID NodeId

open        ParamsWithInitAndHandlers Handle.InitHandler.initAndHandlers
open import LibraBFT.ImplShared.Util.HashCollisions Handle.InitHandler.initAndHandlers

open import Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms
                      Handle.InitHandler.initAndHandlers
                      PeerCanSignForPK PeerCanSignForPK-stable
open        Structural impl-sps-avp

-- This module proves the two "PreferredRound" proof obligations for our handler.

module LibraBFT.Impl.Properties.PreferredRound (𝓔 : EpochConfig) where

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

preferredRound₁ : PR.ImplObligation₁ Handle.InitHandler.initAndHandlers 𝓔
preferredRound₁ {pid} {pid'} {pk = pk} {pre} preach sps@(step-init rm×acts uni) {v = v} {m = m} {v' = v'} {m' = m'}
                hpk v'⊂m' m'∈acts sig' ¬bootstrap' pcs4' v⊂m m∈pool sig ¬bootstrap eid≡ rnd< v≈vabs v'≈vabs'
                c3
  with initHandlerSpec.contract pid fakeBootstrapInfo rm×acts
...| init-contract
  with initHandlerSpec.ContractOk.isInitPM init-contract m'∈acts
...| (_ , refl , noSigs)
  with v'⊂m'
...| vote∈qc vs∈qc _ qc∈pm = ⊥-elim (noSigs vs∈qc qc∈pm)

preferredRound₁ {pid} {pid'} {pk = pk} {pre} preach sps@(step-msg {sndr , P vm} vm'∈pool ini) {v = v} {m = m} {v' = v'} {m' = m'}
                hpk v'⊂m' m'∈acts sig' ¬bootstrap' pcs4' v⊂m m∈pool sig ¬bootstrap eid≡ rnd< v≈vabs v'≈vabs'
                c3 = obm-dangerous-magic' "Extend and use handleProposalSpec.contract"

preferredRound₁ {pid} {pre = pre} preach sps@(step-msg {_ , V vm} _ _)
                _ v'⊂m' m'∈acts sig' ¬bootstrap' ¬msb _ _ _ _ _ _ _ _ _
   with v'⊂m'
...| vote∈qc vs∈qc v≈rbld qc∈m' rewrite cong _vSignature v≈rbld =
       ⊥-elim ∘′ ¬msb $ qcVoteSigsSentB4-handle pid preach sps m'∈acts qc∈m' sig' vs∈qc v≈rbld ¬bootstrap'
...| vote∈vm = ⊥-elim (sendVote∉actions{outs = hvOut}{st = hvPre} (sym noVotes) m'∈acts)
  where
  hvPre = peerStates pre pid
  hvOut = LBFT-outs (handleVote 0 vm) hvPre
  open handleVoteSpec.Contract (handleVoteSpec.contract! 0 vm (msgPool pre) hvPre)

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

-- This proof is essentially the same as the votesOnce₂: no handler sends two different Votes
-- TODO-2: refactor for DRY?
preferredRound₂ : PR.ImplObligation₂ Handle.InitHandler.initAndHandlers 𝓔

preferredRound₂ {pid} _ (step-init rm×acts uni) _ v⊂m m∈acts _ _ _ _ _ _ _ _ _ _ _ _
  with initHandlerSpec.contract pid fakeBootstrapInfo rm×acts
...| init-contract
  with initHandlerSpec.ContractOk.isInitPM init-contract m∈acts
...| (_ , refl , noSigs)
  with v⊂m
...| vote∈qc vs∈qc _ qc∈pm = ⊥-elim (noSigs vs∈qc qc∈pm)

preferredRound₂ {pid}{pk = pk}{pre} rss (step-msg{sndr , m“} m“∈pool ini) {v = v}{v' = v'} hpk v⊂m m∈acts sig ¬bootstrap ¬msb4 pcsfpk v'⊂m' m'∈acts sig' ¬bootstrap' ¬msb4' _ _ round<
   with v⊂m
...| vote∈qc vs∈qc v≈rbld qc∈m rewrite cong _vSignature v≈rbld =
       ⊥-elim ∘′ ¬msb4 $ qcVoteSigsSentB4-handle pid rss (step-msg m“∈pool ini) m∈acts qc∈m sig vs∈qc v≈rbld ¬bootstrap
...| vote∈vm
  with v'⊂m'
...| vote∈qc vs∈qc' v≈rbld' qc∈m' rewrite cong _vSignature v≈rbld' =
       ⊥-elim ∘′ ¬msb4' $ qcVoteSigsSentB4-handle pid rss (step-msg m“∈pool ini) m'∈acts qc∈m' sig' vs∈qc' v≈rbld' ¬bootstrap'
...| vote∈vm
  with m“
...| P pm = ⊥-elim (<⇒≢ round< (cong (_^∙ vRound) v≡v'))
  where
  hpPool = msgPool pre
  hpPre  = peerStates pre pid
  hpOut  = LBFT-outs (handleProposal 0 pm) hpPre
  open handleProposalSpec.Contract (handleProposalSpec.contract! 0 pm hpPool hpPre)

  v≡v' : v ≡ v'
  v≡v'
    with BlockId-correct? (pm ^∙ pmProposal)
  ...| no ¬validProposal = ⊥-elim (sendVote∉actions {outs = hpOut} {st = hpPre} (sym (proj₂ $ invalidProposal ¬validProposal)) m∈acts)
  ...| yes refl
    with voteAttemptCorrect refl (nohc rss m“∈pool pid ini (invariantsCorrect pid pre ini rss) refl refl   )
  ...| Voting.mkVoteAttemptCorrectWithEpochReq (Left (_ , Voting.mkVoteUnsentCorrect noVoteMsgOuts _)) _ =
    ⊥-elim (sendVote∉actions{outs = hpOut}{st = hpPre} (sym noVoteMsgOuts) m∈acts)
  ...| Voting.mkVoteAttemptCorrectWithEpochReq (Right (Voting.mkVoteSentCorrect vm pid voteMsgOuts _)) _ = begin
    v            ≡⟨        cong (_^∙ vmVote) (sendVote∈actions{outs = hpOut}{st = hpPre} (sym voteMsgOuts) m∈acts) ⟩
    vm ^∙ vmVote ≡⟨ (sym $ cong (_^∙ vmVote) (sendVote∈actions{outs = hpOut}{st = hpPre} (sym voteMsgOuts) m'∈acts)) ⟩
    v'           ∎
    where
    open ≡-Reasoning
... | V vm = ⊥-elim (sendVote∉actions{outs = hvOut}{st = hvPre} (sym noVotes) m∈acts)
  where
  hvPre = peerStates pre pid
  hvOut = LBFT-outs (handle pid (V vm) 0) hvPre
  open handleVoteSpec.Contract (handleVoteSpec.contract! 0 vm (msgPool pre) hvPre)


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Functions.Embedding where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Path
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence using (ua; univalence)
open import Cubical.Functions.Fibration

open import Cubical.Data.Sigma
open import Cubical.Functions.Fibration
open import Cubical.Functions.FunExtEquiv
open import Cubical.Relation.Nullary using (Discrete; yes; no)
open import Cubical.Structures.Axioms

open import Cubical.Reflection.StrictEquiv

open import Cubical.Data.Nat using (ℕ; zero; suc)
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ₁ ℓ₂ : Level
    A B : Type ℓ
    f h : A → B
    w x : A
    y z : B

-- Embeddings are generalizations of injections. The usual
-- definition of injection as:
--
--    f x ≡ f y → x ≡ y
--
-- is not well-behaved with higher h-levels, while embeddings
-- are.
isEmbedding : (A → B) → Type _
isEmbedding f = ∀ w x → isEquiv {A = w ≡ x} (cong f)

isEmbeddingIsProp : isProp (isEmbedding f)
isEmbeddingIsProp {f = f} = isPropΠ2 λ _ _ → isPropIsEquiv (cong f)

-- If A and B are h-sets, then injective functions between
-- them are embeddings.
--
-- Note: It doesn't appear to be possible to omit either of
-- the `isSet` hypotheses.
injEmbedding
  : {f : A → B}
  → isSet A → isSet B
  → (∀{w x} → f w ≡ f x → w ≡ x)
  → isEmbedding f
injEmbedding {f = f} iSA iSB inj w x
  = isoToIsEquiv (iso (cong f) inj sect retr)
  where
  sect : section (cong f) inj
  sect p = iSB (f w) (f x) _ p

  retr : retract (cong f) inj
  retr p = iSA w x _ p

-- If `f` is an embedding, we'd expect the fibers of `f` to be
-- propositions, like an injective function.
hasPropFibers : (A → B) → Type _
hasPropFibers f = ∀ y → isProp (fiber f y)

-- This can be relaxed to having all prop fibers over the image, see [hasPropFibersOfImage→isEmbedding]
hasPropFibersOfImage : (A → B) → Type _
hasPropFibersOfImage f = ∀ x → isProp (fiber f (f x))

-- some notation
_↪_ : Type ℓ₁ → Type ℓ₂ → Type (ℓ-max ℓ₁ ℓ₂)
A ↪ B = Σ[ f ∈ (A → B) ] isEmbedding f

hasPropFibersIsProp : isProp (hasPropFibers f)
hasPropFibersIsProp = isPropΠ (λ _ → isPropIsProp)

private
  lemma₀ : (p : y ≡ z) → fiber f y ≡ fiber f z
  lemma₀ {f = f} p = λ i → fiber f (p i)

  lemma₁ : isEmbedding f → ∀ x → isContr (fiber f (f x))
  lemma₁ {f = f} iE x = value , path
    where
    value : fiber f (f x)
    value = (x , refl)

    path : ∀(fi : fiber f (f x)) → value ≡ fi
    path (w , p) i
      = case equiv-proof (iE w x) p of λ
      { ((q , sq) , _)
      → hfill (λ j → λ { (i = i0) → (x , refl)
                      ; (i = i1) → (w , sq j)
                      })
          (inS (q (~ i) , λ j → f (q (~ i ∨ j))))
          i1
      }

isEmbedding→hasPropFibers : isEmbedding f → hasPropFibers f
isEmbedding→hasPropFibers iE y (x , p)
  = subst (λ f → isProp f) (lemma₀ p) (isContr→isProp (lemma₁ iE x)) (x , p)

private
  fibCong→PathP
    : {f : A → B}
    → (p : f w ≡ f x)
    → (fi : fiber (cong f) p)
    → PathP (λ i → fiber f (p i)) (w , refl) (x , refl)
  fibCong→PathP p (q , r) i = q i , λ j → r j i

  PathP→fibCong
    : {f : A → B}
    → (p : f w ≡ f x)
    → (pp : PathP (λ i → fiber f (p i)) (w , refl) (x , refl))
    → fiber (cong f) p
  PathP→fibCong p pp = (λ i → fst (pp i)) , (λ j i → snd (pp i) j)

PathP≡fibCong
  : {f : A → B}
  → (p : f w ≡ f x)
  → PathP (λ i → fiber f (p i)) (w , refl) (x , refl) ≡ fiber (cong f) p
PathP≡fibCong p
  = isoToPath (iso (PathP→fibCong p) (fibCong→PathP p) (λ _ → refl) (λ _ → refl))

hasPropFibers→isEmbedding : hasPropFibers f → isEmbedding f
hasPropFibers→isEmbedding {f = f} iP w x .equiv-proof p
  = subst isContr (PathP≡fibCong p) (isProp→isContrPathP (λ i → iP (p i)) fw fx)
  where
  fw : fiber f (f w)
  fw = (w , refl)

  fx : fiber f (f x)
  fx = (x , refl)

hasPropFibersOfImage→hasPropFibers : hasPropFibersOfImage f → hasPropFibers f
hasPropFibersOfImage→hasPropFibers {f = f} fibImg y a b =
  subst (λ y → isProp (fiber f y)) (snd a) (fibImg (fst a)) a b

hasPropFibersOfImage→isEmbedding : hasPropFibersOfImage f → isEmbedding f
hasPropFibersOfImage→isEmbedding = hasPropFibers→isEmbedding ∘ hasPropFibersOfImage→hasPropFibers

isEmbedding≡hasPropFibers : isEmbedding f ≡ hasPropFibers f
isEmbedding≡hasPropFibers
  = isoToPath
      (iso isEmbedding→hasPropFibers
           hasPropFibers→isEmbedding
           (λ _ → hasPropFibersIsProp _ _)
           (λ _ → isEmbeddingIsProp _ _))

isEquiv→hasPropFibers : isEquiv f → hasPropFibers f
isEquiv→hasPropFibers e b = isContr→isProp (equiv-proof e b)

isEquiv→isEmbedding : isEquiv f → isEmbedding f
isEquiv→isEmbedding e = λ _ _ → congEquiv (_ , e) .snd

Equiv→Embedding : A ≃ B → A ↪ B
Equiv→Embedding (f , isEquivF) = (f , isEquiv→isEmbedding isEquivF)

iso→isEmbedding : ∀ {ℓ} {A B : Type ℓ}
  → (isom : Iso A B)
  -------------------------------
  → isEmbedding (Iso.fun isom)
iso→isEmbedding {A = A} {B} isom = (isEquiv→isEmbedding (equivIsEquiv (isoToEquiv isom)))

isEmbedding→Injection :
  ∀ {ℓ} {A B C : Type ℓ}
  → (a : A → B)
  → (e : isEmbedding a)
  ----------------------
  → ∀ {f g : C → A} →
  ∀ x → (a (f x) ≡ a (g x)) ≡ (f x ≡ g x)
isEmbedding→Injection a e {f = f} {g} x = sym (ua (cong a , e (f x) (g x)))

-- if `f` has a retract, then `cong f` has, as well. If `B` is a set, then `cong f`
-- further has a section, making `f` an embedding.
module _ {f : A → B} (retf : hasRetract f) where
  open Σ retf renaming (fst to g ; snd to ϕ)

  congRetract : f w ≡ f x → w ≡ x
  congRetract {w = w} {x = x} p = sym (ϕ w) ∙∙ cong g p ∙∙ ϕ x

  isRetractCongRetract : retract (cong {x = w} {y = x} f) congRetract
  isRetractCongRetract p = transport (PathP≡doubleCompPathˡ _ _ _ _) (λ i j → ϕ (p j) i)

  hasRetract→hasRetractCong : hasRetract (cong {x = w} {y = x} f)
  hasRetract→hasRetractCong = congRetract , isRetractCongRetract

  retractableIntoSet→isEmbedding : isSet B → isEmbedding f
  retractableIntoSet→isEmbedding setB w x =
    isoToIsEquiv (iso (cong f) congRetract (λ _ → setB _ _ _ _) (hasRetract→hasRetractCong .snd))

Embedding-into-Discrete→Discrete : A ↪ B → Discrete B → Discrete A
Embedding-into-Discrete→Discrete (f , isEmbeddingF) _≟_ x y with f x ≟ f y
... | yes p = yes (invIsEq (isEmbeddingF x y) p)
... | no ¬p = no (¬p ∘ cong f)

Embedding-into-isProp→isProp : A ↪ B → isProp B → isProp A
Embedding-into-isProp→isProp (f , isEmbeddingF) isProp-B x y
  = invIsEq (isEmbeddingF x y) (isProp-B (f x) (f y))

Embedding-into-isSet→isSet : A ↪ B → isSet B → isSet A
Embedding-into-isSet→isSet (f , isEmbeddingF) isSet-B x y p q =
  p ≡⟨ sym (retIsEq isEquiv-cong-f p) ⟩
  cong-f⁻¹ (cong f p) ≡⟨ cong cong-f⁻¹ cong-f-p≡cong-f-q ⟩
  cong-f⁻¹ (cong f q) ≡⟨ retIsEq isEquiv-cong-f q ⟩
  q ∎
  where
    cong-f-p≡cong-f-q = isSet-B (f x) (f y) (cong f p) (cong f q)
    isEquiv-cong-f = isEmbeddingF x y
    cong-f⁻¹ = invIsEq isEquiv-cong-f

Embedding-into-hLevel→hLevel
  : ∀ n → A ↪ B → isOfHLevel (suc n) B → isOfHLevel (suc n) A
Embedding-into-hLevel→hLevel zero = Embedding-into-isProp→isProp
Embedding-into-hLevel→hLevel (suc n) (f , isEmbeddingF) Blvl x y
  = isOfHLevelRespectEquiv (suc n) (invEquiv equiv) subLvl
  where
  equiv : (x ≡ y) ≃ (f x ≡ f y)
  equiv .fst = cong f
  equiv .snd = isEmbeddingF x y
  subLvl : isOfHLevel (suc n) (f x ≡ f y)
  subLvl = Blvl (f x) (f y)

-- We now show that the powerset is the subtype classifier
-- i.e. ℙ X ≃ Σ[A ∈ Type ℓ] (A ↪ X)
Embedding→Subset : {X : Type ℓ} → Σ[ A ∈ Type ℓ ] (A ↪ X) → ℙ X
Embedding→Subset (_ , f , isEmbeddingF) x = fiber f x , isEmbedding→hasPropFibers isEmbeddingF x

Subset→Embedding : {X : Type ℓ} → ℙ X → Σ[ A ∈ Type ℓ ] (A ↪ X)
Subset→Embedding {X = X} A = D , fst , Ψ
 where
  D = Σ[ x ∈ X ] x ∈ A

  Ψ : isEmbedding fst
  Ψ w x = isEmbeddingFstΣProp (∈-isProp A)

Subset→Embedding→Subset : {X : Type ℓ} → section (Embedding→Subset {ℓ} {X}) (Subset→Embedding {ℓ} {X})
Subset→Embedding→Subset _ = funExt λ x → Σ≡Prop (λ _ → isPropIsProp) (ua (FiberIso.fiberEquiv _ x))

Embedding→Subset→Embedding : {X : Type ℓ} → retract (Embedding→Subset {ℓ} {X}) (Subset→Embedding {ℓ} {X})
Embedding→Subset→Embedding {ℓ = ℓ} {X = X} (A , f , ψ) =
  cong (equivFun Σ-assoc-≃) (Σ≡Prop (λ _ → isEmbeddingIsProp) (secEq (fibrationEquiv X ℓ) (A , f)))

Subset≃Embedding : {X : Type ℓ} → ℙ X ≃ (Σ[ A ∈ Type ℓ ] (A ↪ X))
Subset≃Embedding = isoToEquiv (iso Subset→Embedding Embedding→Subset
                                    Embedding→Subset→Embedding Subset→Embedding→Subset)

Subset≡Embedding : {X : Type ℓ} → ℙ X ≡ (Σ[ A ∈ Type ℓ ] (A ↪ X))
Subset≡Embedding = ua Subset≃Embedding

isEmbedding-∘ : isEmbedding f → isEmbedding h → isEmbedding (f ∘ h)
isEmbedding-∘ {f = f} {h = h} Embf Embh w x
  = compEquiv (cong h , Embh w x) (cong f , Embf (h w) (h x)) .snd

isEmbedding→embedsFibersIntoSingl
  : isEmbedding f
  → ∀ z → fiber f z ↪ singl z
isEmbedding→embedsFibersIntoSingl {f = f} isE z = e , isEmbE where
  e : fiber f z → singl z
  e x = f (fst x) , sym (snd x)

  isEmbE : isEmbedding e
  isEmbE u v = goal where
    -- "adjust" ΣeqCf by trivial equivalences that hold judgementally, which should save compositions
    Dom′ : ∀ u v → Type _
    Dom′ u v = Σ[ p ∈    fst u  ≡    fst v  ] PathP (λ i → f (p i) ≡ z) (snd u) (snd v)
    Cod′ : ∀ u v → Type _
    Cod′ u v = Σ[ p ∈ f (fst u) ≡ f (fst v) ] PathP (λ i →    p i  ≡ z) (snd u) (snd v)
    ΣeqCf : Dom′ u v ≃ Cod′ u v
    ΣeqCf = Σ-cong-equiv-fst (_ , isE _ _)

    dom→ : u ≡ v → Dom′ u v
    dom→ p = cong fst p , cong snd p
    dom← : Dom′ u v → u ≡ v
    dom← p i = p .fst i , p .snd i

    cod→ : e u ≡ e v → Cod′ u v
    cod→ p = cong fst p , cong (sym ∘ snd) p
    cod← : Cod′ u v → e u ≡ e v
    cod← p i = p .fst i , sym (p .snd i)

    goal : isEquiv (cong e)
    goal .equiv-proof x .fst .fst =
      dom← (equivCtr ΣeqCf (cod→ x) .fst)
    goal .equiv-proof x .fst .snd j =
      cod← (equivCtr ΣeqCf (cod→ x) .snd j)
    goal .equiv-proof x .snd (g , p) i .fst =
      dom← (equivCtrPath ΣeqCf (cod→ x) (dom→ g , cong cod→ p) i .fst)
    goal .equiv-proof x .snd (g , p) i .snd j =
      cod← (equivCtrPath ΣeqCf (cod→ x) (dom→ g , cong cod→ p) i .snd j)

isEmbedding→hasPropFibers′ : isEmbedding f → hasPropFibers f
isEmbedding→hasPropFibers′ {f = f} iE z =
  Embedding-into-isProp→isProp (isEmbedding→embedsFibersIntoSingl iE z) isPropSingl

universeEmbedding :
  ∀ {ℓ ℓ₁ : Level}
  → (F : Type ℓ → Type ℓ₁)
  → (∀ X → F X ≃ X)
  → isEmbedding F
universeEmbedding F liftingEquiv = hasPropFibersOfImage→isEmbedding propFibersF where
  lemma : ∀ A B → (F A ≡ F B) ≃ (B ≡ A)
  lemma A B = (F A ≡ F B)  ≃⟨ univalence ⟩
              (F A ≃ F B) ≃⟨ equivComp (liftingEquiv A) (liftingEquiv B) ⟩
              (A ≃ B)     ≃⟨ invEquivEquiv ⟩
              (B ≃ A)     ≃⟨ invEquiv univalence ⟩
              (B ≡ A)      ■
  fiberSingl : ∀ X → fiber F (F X) ≃ singl X
  fiberSingl X = Σ-cong-equiv-snd (λ _ → lemma _ _)
  propFibersF : hasPropFibersOfImage F
  propFibersF X = Embedding-into-isProp→isProp (Equiv→Embedding (fiberSingl X)) isPropSingl

liftEmbedding : (ℓ ℓ₁ : Level)
              → isEmbedding (Lift {i = ℓ} {j = ℓ₁})
liftEmbedding ℓ ℓ₁ = universeEmbedding (Lift {j = ℓ₁}) (λ _ → invEquiv LiftEquiv)

module FibrationIdentityPrinciple {B : Type ℓ} {ℓ₁} where
  -- note that fibrationEquiv (for good reason) uses ℓ₁ = ℓ-max ℓ ℓ₁, so we have to work
  -- some universe magic to achieve good universe polymorphism

  -- First, prove it for the case that's dealt with in fibrationEquiv
  Fibration′ = Fibration B (ℓ-max ℓ ℓ₁)

  module Lifted (f g : Fibration′) where
    f≃g′ : Type (ℓ-max ℓ ℓ₁)
    f≃g′ = ∀ b → fiber (f .snd) b ≃ fiber (g .snd) b

    Fibration′IP : f≃g′ ≃ (f ≡ g)
    Fibration′IP =
        f≃g′
      ≃⟨ equivΠCod (λ _ → invEquiv univalence) ⟩
        (∀ b → fiber (f .snd) b ≡ fiber (g .snd) b)
      ≃⟨ funExtEquiv ⟩
        fiber (f .snd) ≡ fiber (g .snd)
      ≃⟨ invEquiv (congEquiv (fibrationEquiv B ℓ₁)) ⟩
        f ≡ g
      ■

  -- Then embed into the above case by lifting the type
  L : Type _ → Type _ -- local synonym fixing the levels of Lift
  L = Lift {i = ℓ₁} {j = ℓ}

  liftFibration : Fibration B ℓ₁ → Fibration′
  liftFibration (A , f) = L A , f ∘ lower

  hasPropFibersLiftFibration : hasPropFibers liftFibration
  hasPropFibersLiftFibration (A , f) =
    Embedding-into-isProp→isProp (Equiv→Embedding fiberChar)
      (isPropΣ (isEmbedding→hasPropFibers (liftEmbedding _ _) A)
               λ _ → isEquiv→hasPropFibers (snd (invEquiv (preCompEquiv LiftEquiv))) _)
    where
    fiberChar : fiber liftFibration (A , f)
              ≃ (Σ[ (E , eq) ∈ fiber L A ] fiber (_∘ lower) (transport⁻ (λ i → eq i → B) f))
    fiberChar =
        fiber liftFibration (A , f)
      ≃⟨ Σ-cong-equiv-snd (λ _ → invEquiv ΣPath≃PathΣ) ⟩
        (Σ[ (E , g) ∈ Fibration B ℓ₁ ] Σ[ eq ∈ (L E ≡ A) ] PathP (λ i → eq i → B) (g ∘ lower) f)
      ≃⟨ boringSwap ⟩
        (Σ[ (E , eq) ∈ fiber L A ] Σ[ g ∈ (E → B) ] PathP (λ i → eq i → B) (g ∘ lower) f)
      ≃⟨ Σ-cong-equiv-snd (λ _ → Σ-cong-equiv-snd λ _ → transportEquiv (PathP≡Path⁻ _ _ _)) ⟩
        (Σ[ (E , eq) ∈ fiber L A ] fiber (_∘ lower) (transport⁻ (λ i → eq i → B) f))
      ■ where
      unquoteDecl boringSwap =
        declStrictEquiv boringSwap
          (λ ((E , g) , (eq , p)) → ((E , eq) , (g , p)))
          (λ ((E , g) , (eq , p)) → ((E , eq) , (g , p)))

  isEmbeddingLiftFibration : isEmbedding liftFibration
  isEmbeddingLiftFibration = hasPropFibers→isEmbedding hasPropFibersLiftFibration

  -- and finish off
  module _ (f g : Fibration B ℓ₁) where
    open Lifted (liftFibration f) (liftFibration g)
    f≃g : Type (ℓ-max ℓ ℓ₁)
    f≃g = ∀ b → fiber (f .snd) b ≃ fiber (g .snd) b

    FibrationIP : f≃g ≃ (f ≡ g)
    FibrationIP =
      f≃g  ≃⟨ equivΠCod (λ b → equivComp (Σ-cong-equiv-fst LiftEquiv)
                                          (Σ-cong-equiv-fst LiftEquiv)) ⟩
      f≃g′ ≃⟨ Fibration′IP ⟩
      (liftFibration f ≡ liftFibration g) ≃⟨ invEquiv (_ , isEmbeddingLiftFibration _ _) ⟩
      (f ≡ g) ■
open FibrationIdentityPrinciple renaming (f≃g to _≃Fib_) using (FibrationIP) public

Embedding : (B : Type ℓ₁) → (ℓ : Level) → Type (ℓ-max ℓ₁ (ℓ-suc ℓ))
Embedding B ℓ = Σ[ A ∈ Type ℓ ] A ↪ B

module EmbeddingIdentityPrinciple {B : Type ℓ} {ℓ₁} (f g : Embedding B ℓ₁) where
  module _ where
    open Σ f renaming (fst to F) public
    open Σ g renaming (fst to G) public
    open Σ (f .snd) renaming (fst to ffun; snd to isEmbF) public
    open Σ (g .snd) renaming (fst to gfun; snd to isEmbG) public
  f≃g : Type _
  f≃g = (∀ b → fiber ffun b → fiber gfun b) ×
         (∀ b → fiber gfun b → fiber ffun b)
  toFibr : Embedding B ℓ₁ → Fibration B ℓ₁
  toFibr (A , (f , _)) = (A , f)

  isEmbeddingToFibr : isEmbedding toFibr
  isEmbeddingToFibr w x = fullEquiv .snd where
    -- carefully managed such that (cong toFibr) is the equivalence
    fullEquiv : (w ≡ x) ≃ (toFibr w ≡ toFibr x)
    fullEquiv = compEquiv (congEquiv (invEquiv Σ-assoc-≃)) (invEquiv (Σ≡PropEquiv (λ _ → isEmbeddingIsProp)))

  EmbeddingIP : f≃g ≃ (f ≡ g)
  EmbeddingIP =
      f≃g
    ≃⟨ strictIsoToEquiv (invIso toProdIso) ⟩
      (∀ b → (fiber ffun b → fiber gfun b) × (fiber gfun b → fiber ffun b))
    ≃⟨ equivΠCod (λ _ → isEquivPropBiimpl→Equiv (isEmbedding→hasPropFibers isEmbF _)
                                                 (isEmbedding→hasPropFibers isEmbG _)) ⟩
      (∀ b → (fiber (f .snd .fst) b) ≃ (fiber (g .snd .fst) b))
    ≃⟨ FibrationIP (toFibr f) (toFibr g) ⟩
      (toFibr f ≡ toFibr g)
    ≃⟨ invEquiv (_ , isEmbeddingToFibr _ _) ⟩
      f ≡ g
    ■
open EmbeddingIdentityPrinciple renaming (f≃g to _≃Emb_) using (EmbeddingIP) public

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
-- IIRDg is expressible in IIRDr + Identity
module Proof where

open import LF
open import IIRD
open import IIRDr
open import DefinitionalEquality
open import Identity
open import Proof.Setup
import Logic.ChainReasoning as Chain

-- We can then define general IIRDs using the ε function from Proof.Setup.
Ug : {I : Set}{D : I -> Set1} -> OPg I D -> I -> Set
Ug γ = Ur (ε γ)

Tg : {I : Set}{D : I -> Set1}(γ : OPg I D)(i : I) -> Ug γ i -> D i
Tg γ = Tr (ε γ)

introg : {I : Set}{D : I -> Set1}(γ : OPg I D)(a : Gu γ (Ug γ) (Tg γ)) ->
         Ug γ (Gi γ (Ug γ) (Tg γ) a)
introg γ a = intror (G→H γ (Ug γ) (Tg γ) a)

-- To prove the reduction behviour of Tg we first have to prove that the
-- top-level reduction of the encoding behaves as it should. At bit simplified
-- that  Ht (ε γ) (Gi a) ≡ Gt γ a
Tg-eq : {I : Set}{D : I -> Set1}(γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
        (a : Gu γ U T) ->
        Ht (ε γ) U T (Gi γ U T a) (G→H γ U T a) ≡₁ Gt γ U T a
Tg-eq {I}{D} (ι < i | e >') U T ★         = refl-≡₁
Tg-eq        (σ A γ)        U T < a | b > = Tg-eq (γ a) U T b
Tg-eq        (δ A i γ)      U T < g | b > = Tg-eq (γ (T « i × g »)) U T b

-- The statement we're interested in is a special case of the more general
-- lemma above.
Tg-equality : {I : Set}{D : I -> Set1}(γ : OPg I D)(a : Gu γ (Ug γ) (Tg γ)) ->
              Tg γ (Gi γ (Ug γ) (Tg γ) a) (introg γ a) ≡₁ Gt γ (Ug γ) (Tg γ) a
Tg-equality γ a = Tg-eq γ (Ug γ) (Tg γ) a

-- The elimination rule for generalised IIRDs.
-- It's basically the elimination of the encoding followed by the elimination
-- of the proof the the index is the right one.
Rg : {I : Set}{D : I -> Set1}(γ : OPg I D)(F : (i : I) -> Ug γ i -> Set1)
     (h : (a : Gu γ (Ug γ) (Tg γ)) -> KIH γ (Ug γ) (Tg γ) F a -> F (Gi γ (Ug γ) (Tg γ) a) (introg γ a))
     (i : I)(u : Ug γ i) -> F i u
Rg {I}{D} γ F h = Rr (ε γ) F \i a ih ->
                    G→H∘H→G-subst γ U T
                                  (\i a -> F i (intror a))
                                  i a (lem1 i a ih)
  where
    U = Ug γ
    T = Tg γ
    lem1 : (i : I)(a : Hu (ε γ) U T i) ->
           KIH (ε γ i) U T F a ->
           F (Gi γ U T (H→G γ U T i a))
             (intror (G→H γ U T (H→G γ U T i a)))
    lem1 i a ih = h (H→G γ U T i a) (\v -> εIArg-subst γ U T F i a v (ih (εIArg γ U T i a v)))

open module Chain-≡  = Chain.Poly.Heterogenous1 _≡₁_ (\x -> refl-≡₁) trans-≡₁
open module Chain-≡₀ = Chain.Poly.Heterogenous  _≡_  (\x -> refl-≡)  trans-≡
	      renaming (chain>_ to chain>₀_; _===_ to _===₀_; _by_ to _by₀_)

-- Again we have to generalise
Rg-eq : {I : Set}{D : I -> Set1}(γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
        (F : (i : I) -> U i -> Set1)(intro : (a : Gu γ U T) -> U (Gi γ U T a))
        (g : (i : I)(u : U i) -> F i u)
        (h : (a : Gu γ U T) -> KIH γ U T F a -> F (Gi γ U T a) (intro a))
        (a : Gu γ U T) ->
        let i  = Gi γ U T a
            a' = G→H γ U T a
        in h (H→G γ U T i a')
	     (\v -> εIArg-subst γ U T F i a' v
		      (Kmap (ε γ i) U T F g a' (εIArg γ U T i a' v)))
           ≡₁ h a (Kmap γ U T F g a)
Rg-eq {I}{D} γ U T F intro g h a = app-≡₁
  (cong-≡₁⁰ h (H→G∘G→H-identity γ U T a))
  (η-≡₁⁰ \x y p ->
    chain>  εIArg-subst γ U T F i a' x (Kmap (ε γ i) U T F g a' (εIArg γ U T i a' x))
        === Kmap (ε γ i) U T F g a' (εIArg γ U T i a' x)
              by εIArg-identity γ U T F a x (Kmap (ε γ i) U T F g a' (εIArg γ U T i a' x))
        === Kmap γ U T F g a y
              by app-≡₁⁰
                  (cong-≡₁⁰ g
                    (chain>₀ KIArg→I (ε γ i) U T a' (εIArg γ U T i a' x)
                        ===₀ KIArg→I γ U T (H→G γ U T i a') x   by₀  εIArg→I-identity γ U T i a' x
                        ===₀ KIArg→I γ U T a y                  by₀
                                app-≡₀ (cong-≡' (KIArg→I γ U T)
                                                (H→G∘G→H-identity γ U T a)
                                       ) p
                    )
                  )
                  (chain>₀ KIArg→U (ε γ i) U T a' (εIArg γ U T i a' x)
                      ===₀ KIArg→U γ U T (H→G γ U T i a') x   by₀  εIArg→U-identity γ U T i a' x
                      ===₀ KIArg→U γ U T a y                  by₀
                              app-≡₀ (cong-≡' (KIArg→U γ U T)
                                              (H→G∘G→H-identity γ U T a)
                                     ) p
                  )
  )
  where
    i  = Gi γ U T a
    a' = G→H γ U T a

Rg-equality : {I : Set}{D : I -> Set1}(γ : OPg I D)(F : (i : I) -> Ug γ i -> Set1)
              (h : (a : Gu γ (Ug γ) (Tg γ)) -> KIH γ (Ug γ) (Tg γ) F a -> F (Gi γ (Ug γ) (Tg γ) a) (introg γ a))
              (a : Gu γ (Ug γ) (Tg γ)) ->
              Rg γ F h (Gi γ (Ug γ) (Tg γ) a) (introg γ a)
              ≡₁ h a (Kmap γ (Ug γ) (Tg γ) F (Rg γ F h) a)
Rg-equality {I}{D} γ F h a =
  chain> Rg γ F h (Gi γ U T a) (introg γ a)
     === h'' i a' ih    by  refl-≡₁
     === G→H∘H→G-subst γ U T F' i a' (h' i a' ih)
                        by  refl-≡₁
     === h' i a' ih     by G→H∘H→G-identity γ U T F' a (h' i a' ih)
     === h (H→G γ U T i a') (\v -> εIArg-subst γ U T F i a' v (ih (εIArg γ U T i a' v)))
                        by refl-≡₁
     === h a (Kmap γ U T F (Rg γ F h) a)      by  Rg-eq γ U T F (introg γ) (Rg γ F h) h a
  where
    U  = Ug γ
    T  = Tg γ
    F' = \i a -> F i (intror a)
    i  = Gi γ U T a
    a' = G→H γ U T a
    h' : (i : I)(a : Hu (ε γ) U T i) -> KIH (ε γ i) U T F a -> F _ _
    h' = \i a ih -> h (H→G γ U T i a) \v ->
                  εIArg-subst γ U T F i a v
                      (ih (εIArg γ U T i a v))
    h'' = \i a ih -> G→H∘H→G-subst γ U T F' i a (h' i a ih)
    ih  = Kmap (ε γ i) U T F (Rg γ F h) a'

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Deriv where

open import Relation.Binary.Bundles using (DecSetoid)
open import Algebra.Bundles using (Semiring)
open import Level using (0ℓ)
open import Relation.Nullary using (yes; no)

module _ (S : DecSetoid 0ℓ 0ℓ) (Targ : Set) where

  open DecSetoid S renaming (Carrier to Key)

  infixl 6 _+_
  infixl 7 _*_
  data Expr : Set where
    ↑ : Targ → Expr
    ! : Key → Expr
    _+_ : Expr → Expr → Expr
    _*_ : Expr → Expr → Expr

module _ {S : DecSetoid 0ℓ 0ℓ} (R : Semiring 0ℓ 0ℓ) where

  private module S = DecSetoid S
  open S renaming (Carrier to Key)
  private module R = Semiring R
  open R using (0#; 1#) renaming (Carrier to Targ)

  eval
    : (lookup : Key → Targ)
    → (expr : Expr S Targ)
    → Targ
  eval lookup (↑ x) = x
  eval lookup (! x) = lookup x
  eval lookup (x + x₁) = eval lookup x₁ R.+ eval lookup x₁
  eval lookup (x * x₁) = eval lookup x₁ R.* eval lookup x₁

  deriv : Expr S Targ → Key → Expr S Targ
  deriv (↑ x) k = ↑ 0#
  deriv (! x) k with x ≟ k
  deriv (! x) k | yes _ = ↑ 1#
  deriv (! x) k | no _ = ↑ 0#
  deriv (e + e₁) k = deriv e k + deriv e₁ k
  deriv (e * e₁) k = (deriv e k * e₁) + (e * deriv e₁ k)

open import Data.Nat using (ℕ)
open import Data.Nat.Properties using (+-*-semiring)
open import Data.String
open import Relation.Binary.PropositionalEquality using (decSetoid)

asdf : Expr (decSetoid _≟_) ℕ
asdf = ↑ 2 + (↑ 5 * (! "hello" * ! "goodbye"))

asdf' : Expr (decSetoid _≟_) ℕ
asdf' = deriv +-*-semiring asdf "hello"

normalize : ∀ {D} → Expr D ℕ → Expr D ℕ
normalize (x + y) with normalize x | normalize y
normalize (x + y) | ↑ w | ↑ z   = ↑ (w Data.Nat.+ z)
normalize (x + y) | ↑ 0 | z   = z
normalize (x + y) | w   | ↑ 0 = w
normalize (x + y) | w   | z   = w + z
normalize (x * y) with normalize x | normalize y
normalize (x * y) | ↑ w | ↑ z   = ↑ (w Data.Nat.* z)
normalize (x * y) | ↑ 0 | z   = ↑ 0
normalize (x * y) | w   | ↑ 0 = ↑ 0
normalize (x * y) | ↑ 1 | z   = z
normalize (x * y) | w   | ↑ 1 = w
normalize (x * y) | w   | z   = w * z
normalize z = z

module _ (R : Semiring 0ℓ 0ℓ) where
  open Semiring R
  private module R = Semiring R

  asdf'' : Carrier
  asdf'' = 1# R.+ 0#

max_stars_repo_name: cspollard/diff

max_issues_repo_name: cspollard/diff

max_forks_repo_name: cspollard/diff


text:
-- Andreas, 2017-07-27

module _ where

module A where
  record A : Set where

open A

open A

-- ERROR WAS:
-- Ambiguous module name A. It could refer to any one of
--   A.A
--   Issue705.A

-- EXPECTED:
-- Ambiguous module name A. It could refer to any one of
--   A.A (record module)
--   Issue705.A


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Polynomial reasoning
------------------------------------------------------------------------

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

open import Tactic.RingSolver.Core.AlmostCommutativeRing

-- Some specialised tools for equational reasoning.
module Tactic.RingSolver.Core.Polynomial.Reasoning
  {a ℓ} (ring : AlmostCommutativeRing a ℓ)
  where

open AlmostCommutativeRing ring
open import Relation.Binary.Reasoning.Setoid setoid public

infixr 1 ≪+_ +≫_ ≪*_ *≫_
infixr 0 _⊙_

≪+_ : ∀ {x₁ x₂ y} → x₁ ≈ x₂ → x₁ + y ≈ x₂ + y
≪+ prf = +-cong prf refl
{-# INLINE ≪+_ #-}

+≫_ : ∀ {x y₁ y₂} → y₁ ≈ y₂ → x + y₁ ≈ x + y₂
+≫_ = +-cong refl
{-# INLINE +≫_ #-}

≪*_ : ∀ {x₁ x₂ y} → x₁ ≈ x₂ → x₁ * y ≈ x₂ * y
≪* prf = *-cong prf refl
{-# INLINE ≪*_ #-}

*≫_ : ∀ {x y₁ y₂} → y₁ ≈ y₂ → x * y₁ ≈ x * y₂
*≫_ = *-cong refl
{-# INLINE *≫_ #-}

-- transitivity as an operator
_⊙_ : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
_⊙_ = trans
{-# INLINE _⊙_ #-}


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

open import Cubical.Foundations.Everything
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.List
open import Cubical.Data.Maybe
open import Cubical.Data.Prod

module Untruncated2ListInvariant {ℓ} (A : Type ℓ) where

 -- Invariant
 Inv : List A → List A → Type ℓ
 Inv xs ys = ys ≡ [] → xs ≡ []

 isPropInv : (xs ys : List A) → isProp (Inv xs ys)
 isPropInv xs ys = isPropΠ λ _ → isPropXs≡[]

 Inv-ys≡ys' : {xs ys ys' : List A} → (p : ys ≡ ys') →
   (invL : Inv xs ys) → (invR : Inv xs ys') → PathP (λ i → Inv xs (p i)) invL invR
 Inv-ys≡ys' {xs = xs} p invL invR = isProp→PathP (λ i → isPropInv xs (p i)) invL invR

 inv-xs-∷ : {xs ys : List A} {y : A} → Inv xs (y ∷ ys)
 inv-xs-∷ contra = ⊥.rec (¬cons≡nil contra)

 inv-xs-∷ʳ : {xs ys : List A} → {y : A} → Inv xs (ys ∷ʳ y)
 inv-xs-∷ʳ contra = ⊥.rec (¬snoc≡nil contra)

 inv-[]-ys : {ys : List A} → Inv [] ys
 inv-[]-ys ys = refl

 inv-invalid : {xs : List A} {x : A} → Inv (xs ∷ʳ x) [] → ⊥
 inv-invalid inv = ¬snoc≡nil (inv refl)

 -- Queue
 data Q : Type ℓ where
   Q⟨_,_!_⟩ : (xs ys : List A) → (inv : Inv xs ys) → Q
   tilt : ∀ xs ys z l r → Q⟨ xs ++ [ z ] , ys ! l ⟩ ≡ Q⟨ xs , ys ++ [ z ] ! r ⟩

 Q-ys≡ys' : ∀ xs {ys ys' : List A} l r → (p : ys ≡ ys') → Q⟨ xs , ys ! l ⟩ ≡ Q⟨ xs , ys' ! r ⟩
 Q-ys≡ys' xs l r p i = Q⟨ xs , p i ! Inv-ys≡ys' p l r i ⟩

 flush-xs : ∀ xs ys l r → Q⟨ xs , ys ! l ⟩ ≡ Q⟨ [] , ys ++ rev xs ! r ⟩
 flush-xs xs ys l r = helper xs ys l r (snocView xs)
   where
     helper : ∀ xs ys l r → SnocView xs → Q⟨ xs , ys ! l ⟩ ≡ Q⟨ [] , ys ++ rev xs ! r ⟩
     helper .[] ys l r nil i = Q⟨ [] , ++-unit-r ys (~ i) ! Inv-ys≡ys' (++-unit-r ys ⁻¹) l r i  ⟩
     helper .(xs ∷ʳ x) ys l r (snoc x xs s) = move-x ∙ IH ∙ Q-ys≡ys' [] inv-[]-ys r lemma
       where
       move-x : Q⟨ xs ∷ʳ x , ys ! l ⟩ ≡ Q⟨ xs , ys ∷ʳ x ! inv-xs-∷ʳ ⟩
       move-x = tilt xs ys x l inv-xs-∷ʳ
       IH : Q⟨ xs , ys ∷ʳ x ! inv-xs-∷ʳ ⟩ ≡ Q⟨ [] , (ys ∷ʳ x) ++ rev xs ! inv-[]-ys ⟩
       IH = helper xs (ys ∷ʳ x) inv-xs-∷ʳ inv-[]-ys s
       lemma : (ys ∷ʳ x) ++ rev xs ≡ ys ++ rev (xs ∷ʳ x)
       lemma = ++-assoc ys (x ∷ []) (rev xs) ∙ cong (ys ++_) (cons≡rev-snoc x xs)

 emp : Q
 emp = Q⟨ [] , [] ! inv-[]-ys ⟩

 enq : A → Q → Q
 enq a Q⟨ xs , [] ! inv ⟩ = Q⟨ xs , a ∷ [] ! inv-xs-∷ ⟩
 enq a Q⟨ xs , y ∷ ys ! inv ⟩ = Q⟨ a ∷ xs , y ∷ ys ! inv-xs-∷ ⟩
 enq a (tilt xs [] z l r i) = proof i
   where
   proof : Q⟨ xs ++ z ∷ [] , a ∷ [] ! inv-xs-∷ ⟩ ≡ Q⟨ a ∷ xs , z ∷ [] ! inv-xs-∷ ⟩
   proof = ⊥.rec (inv-invalid l)
 enq a (tilt xs (y ∷ ys) z l r i) = tilt (a ∷ xs) (y ∷ ys) z inv-xs-∷ inv-xs-∷ i

 deq : Q → Maybe (Q × A)
 deq Q⟨ xs , [] ! inv ⟩ = nothing
 deq Q⟨ xs , y ∷ [] ! inv ⟩ = just (Q⟨ [] , rev xs ! inv-[]-ys ⟩ , y)
 deq Q⟨ xs , y₁ ∷ y₂ ∷ ys ! inv ⟩ = just (Q⟨ xs , y₂ ∷ ys ! inv-xs-∷ ⟩ , y₁)
 deq (tilt xs [] z l r i) = proof i
   where
   proof : nothing ≡ just (Q⟨ [] , rev xs ! inv-[]-ys ⟩ , z)
   proof = ⊥.rec (inv-invalid l)
 deq (tilt xs (y ∷ []) z l r i) = just (proof i , y)
   where
   proof : Q⟨ [] , rev (xs ∷ʳ z) ! inv-[]-ys ⟩ ≡ Q⟨ xs , z ∷ [] ! inv-xs-∷ ⟩
   proof = Q-ys≡ys' [] inv-[]-ys inv-xs-∷ (cons≡rev-snoc z xs ⁻¹) ∙ flush-xs xs (z ∷ []) inv-xs-∷ inv-xs-∷ ⁻¹
 deq (tilt xs (y₁ ∷ y₂ ∷ ys) z l r i) = just ((tilt xs (y₂ ∷ ys) z inv-xs-∷ inv-xs-∷ i) , y₁)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical