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

module LookVsTime where

open import Data.Fin     using (#_)
open import Data.Integer using (+_; -[1+_])
open import Data.List    using (List; _∷_; []; map; concat; _++_; replicate; zip; length; take)
open import Data.Nat     using (_*_; ℕ; suc; _+_)
open import Data.Product using (_,_; uncurry)
open import Data.Vec     using (fromList; Vec; _∷_; []) renaming (replicate to rep; zip to vzip; map to vmap; concat to vconcat; _++_ to _+v_)
open import Function     using (_∘_)

open import Pitch
open import Note         using (tone; rest; Note; Duration; duration; unduration)
open import Music
open import Midi
open import MidiEvent
open import Util         using (repeat; repeatV)

tempo : ℕ
tempo = 84

----

8th : ℕ → Duration
8th n = duration (2 * n)

whole : ℕ → Duration
whole n = duration (16 * n)

melodyChannel : Channel-1
melodyChannel = # 0

melodyInstrument : InstrumentNumber-1
melodyInstrument = # 8 -- celesta

melodyNotes : List Note
melodyNotes =
  tone (8th 3) (c 5) ∷
  tone (8th 5) (d 5) ∷

  tone (8th 3) (c 5) ∷
  tone (8th 5) (d 5) ∷

  tone (8th 1) (g 5) ∷
  tone (8th 1) (f 5) ∷
  tone (8th 1) (e 5) ∷
  tone (8th 5) (d 5) ∷

  tone (8th 1) (g 5) ∷
  tone (8th 1) (f 5) ∷
  tone (8th 1) (e 5) ∷
  tone (8th 5) (d 5) ∷

  tone (8th 1) (a 5) ∷
  tone (8th 1) (g 5) ∷
  tone (8th 1) (f 5) ∷
  tone (8th 2) (e 5) ∷
  tone (8th 1) (c 5) ∷
  tone (8th 2) (d 5) ∷

  tone (8th 1) (a 5) ∷
  tone (8th 1) (g 5) ∷
  tone (8th 1) (f 5) ∷
  tone (8th 2) (e 5) ∷
  tone (8th 1) (c 5) ∷
  tone (8th 2) (d 5) ∷

  tone (8th 3) (b 4) ∷
  tone (8th 5) (c 5) ∷

  tone (8th 1) (f 5) ∷
  tone (8th 1) (e 5) ∷
  tone (8th 1) (d 5) ∷
  tone (8th 5) (c 5) ∷

  tone (8th 3) (g 5) ∷
  tone (8th 3) (e 5) ∷
  tone (8th 2) (d 5) ∷

  tone (8th 3) (g 5) ∷
  tone (8th 3) (e 5) ∷
  tone (8th 2) (d 5) ∷

  tone (8th 8) (c 5) ∷

  tone (8th 8) (b 4) ∷

  tone (8th 3) (c 5) ∷
  tone (8th 5) (d 5) ∷

  tone (8th 3) (c 5) ∷
  tone (8th 5) (d 5) ∷

  tone (8th 3) (a 5) ∷
  tone (8th 5) (f 5) ∷

  tone (8th 3) (e 5) ∷
  tone (8th 5) (d 5) ∷

  tone (8th 8) (c 5) ∷

  tone (8th 8) (d 5) ∷

  tone (8th 1) (c 5) ∷
  tone (8th 1) (c 5) ∷
  tone (8th 1) (c 5) ∷
  tone (8th 5) (d 5) ∷

  tone (8th 1) (c 5) ∷
  tone (8th 1) (c 5) ∷
  tone (8th 1) (c 5) ∷
  tone (8th 5) (d 5) ∷

  tone (8th 3) (a 5) ∷
  tone (8th 5) (f 5) ∷

  tone (8th 3) (a 5) ∷
  tone (8th 5) (g 5) ∷

  tone (8th 1) (a 5) ∷
  tone (8th 1) (g 5) ∷
  tone (8th 1) (f 5) ∷
  tone (8th 2) (e 5) ∷
  tone (8th 1) (c 5) ∷
  tone (8th 2) (d 5) ∷

  tone (8th 1) (a 5) ∷
  tone (8th 1) (g 5) ∷
  tone (8th 1) (f 5) ∷
  tone (8th 2) (e 5) ∷
  tone (8th 1) (c 5) ∷
  tone (8th 2) (d 5) ∷

  tone (8th 3) (b 4) ∷
  tone (8th 5) (c 5) ∷

  tone (8th 24) (b 4) ∷

  []

melodyTrack : MidiTrack
melodyTrack = track "Melody" melodyInstrument melodyChannel tempo (notes→events defaultVelocity melodyNotes)

----

accompChannel : Channel-1
accompChannel = # 1

accompInstrument : InstrumentNumber-1
accompInstrument = # 11 -- vibraphone

accompRhythm : Vec Duration 3
accompRhythm = vmap 8th (3 ∷ 3 ∷ 2 ∷ [])

accompF accompB2 accompC4 : Vec Pitch 3
accompF  = f 4 ∷ a 4 ∷ c 5 ∷ []
accompB2 = f 4 ∷ b 4 ∷ d 4 ∷ []
accompC4 = f 4 ∷ c 5 ∷ e 5 ∷ []

accompFA : Vec Pitch 2
accompFA = f 4 ∷ a 4 ∷ []

accompChords1 : Harmony 3 128
accompChords1 =
  foldIntoHarmony (repeatV 8 accompRhythm)
                  (repeatV 2 (vconcat (vmap (rep {n = 3}) (accompF ∷ accompB2 ∷ accompC4 ∷ accompB2 ∷ []))))

accompChords2 : Harmony 3 64
accompChords2 = addEmptyVoice (pitches→harmony (whole 4) accompFA)

accompChords3 : Harmony 3 64
accompChords3 =
  foldIntoHarmony (repeatV 4 accompRhythm)
                  (vconcat (vmap (rep {n = 3}) (accompF ∷ accompB2 ∷ accompC4 ∷ [])) +v (accompB2 ∷ accompB2 ∷ accompF ∷ []))

accompChords4 : Harmony 3 16
accompChords4 = addEmptyVoice (foldIntoHarmony accompRhythm (rep accompFA))

accompChords5 : Harmony 3 48
accompChords5 = pitches→harmony (8th (8 + 8 + 6)) accompF +H+ pitches→harmony (8th 2) accompF

accompChords6 : Harmony 3 32
accompChords6 = pitches→harmony (8th (8 + 6)) accompB2 +H+ pitches→harmony (8th 2) accompB2

accompChords7 : Harmony 3 32
accompChords7 = pitches→harmony (whole 2) accompF

accompChords : Harmony 3 448
accompChords = accompChords1 +H+ accompChords3 +H+ accompChords2 +H+ accompChords3 +H+ accompChords4
                 +H+ accompChords5 +H+ accompChords6 +H+ accompChords7

accompTrack : MidiTrack
accompTrack = track "Accomp" accompInstrument accompChannel tempo (harmony→events defaultVelocity accompChords)

----

bassChannel : Channel-1
bassChannel = # 2

bassInstrument : InstrumentNumber-1
bassInstrument = # 33 -- finger bass

bassMelody : List Pitch
bassMelody = c 3 ∷ e 3 ∷ f 3 ∷ g 3 ∷ []

bassRhythm : List Duration
bassRhythm = map 8th (3 ∷ 1 ∷ 2 ∷ 2 ∷ [])

bassNotes : List Note
bassNotes = repeat 28 (map (uncurry tone) (zip bassRhythm bassMelody))

bassTrack : MidiTrack
bassTrack = track "Bass" bassInstrument bassChannel tempo (notes→events defaultVelocity bassNotes)

----

drumInstrument : InstrumentNumber-1
drumInstrument = # 0 -- SoCal?

drumChannel : Channel-1
drumChannel = # 9

drumRhythmA : List Duration
drumRhythmA = map duration (2 ∷ [])

drumRhythmB : List Duration
drumRhythmB = map duration (1 ∷ 1 ∷ 2 ∷ [])

drumRhythm : List Duration
drumRhythm = drumRhythmA ++ repeat 3 drumRhythmB ++ drumRhythmA

drumPitches : List Pitch
drumPitches = replicate (length drumRhythm) (b 4) -- Ride In

drumNotes : List Note
drumNotes = rest (whole 1) ∷ repeat 27 (map (uncurry tone) (zip drumRhythm drumPitches))

drumTrack : MidiTrack
drumTrack = track "Drums" drumInstrument drumChannel tempo (notes→events defaultVelocity drumNotes)

----

lookVsTime : List MidiTrack
lookVsTime = melodyTrack ∷ accompTrack ∷ bassTrack ∷ drumTrack ∷ []

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


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

open import Base
open import Homotopy.Pointed
open import Homotopy.Connected

module Homotopy.Cover {i} (A⋆ : pType i)
  (A⋆-is-conn : is-connected⋆ ⟨0⟩ A⋆) where
open pType A⋆ renaming (∣_∣ to A ; ⋆ to a)

open import Homotopy.Cover.Def A

module Reconstruct where
  open import Homotopy.Cover.HomotopyGroupSetIsomorphism A⋆ A⋆-is-conn public

{-
-- The following is still a mess.  Don't read it.
module _ (uc : universal-covering) where
  open covering (π₁ uc)

{-
  path⇒deck-is-equiv : ∀ {a₂} (path : a ≡ a₂) → is-equiv (path⇒deck path)
  path⇒deck-is-equiv path = iso-is-eq
    (transport fiber path)
    (transport fiber (! path))
    (trans-trans-opposite fiber path)
    (trans-opposite-trans fiber path)
-}

  is-nature : (fiber a → fiber a) → Set i
  is-nature f = (p : a ≡ a)
    → ∀ x → transport fiber p (f x) ≡ f (transport fiber p x)

  auto : Set i
  auto = fiber a ≃ fiber a

  -- This Lemma can be made more general as "(m+1)-connected => has-all-paths_m"
  uc-has-all-path₀ : ∀ (p q : Σ A fiber) → p ≡₀ q
  uc-has-all-path₀ p q = inverse τ-path-equiv-path-τ-S
    $ π₂ (π₂ uc) (proj p) ∘ ! (π₂ (π₂ uc) $ proj q)

  nature-auto-eq : ∀ (f₁ f₂ : auto)
    → (f₁-is-nature : is-nature (π₁ f₁))
    → (f₂-is-nature : is-nature (π₁ f₂))
    → Σ (fiber a) (λ x → f₁ ☆ x ≡ f₂ ☆ x)
    → f₁ ≡ f₂
  nature-auto-eq f₁ f₂ f₁-nat f₂-nat (x , path) = equiv-eq $ funext λ y →
    π₀-extend
      ⦃ λ _ → ≡-is-set {x = f₁ ☆ y} {y = f₂ ☆ y} $ fiber-is-set a ⦄
      (λ uc-path →
        f₁ ☆ y
          ≡⟨ ap (π₁ f₁) $ ! $ fiber-path uc-path ⟩
        f₁ ☆ transport fiber (base-path uc-path) x
          ≡⟨ ! $ f₁-nat (base-path uc-path) x ⟩
        transport fiber (base-path uc-path) (f₁ ☆ x)
          ≡⟨ ap (transport fiber $ base-path uc-path) path ⟩
        transport fiber (base-path uc-path) (f₂ ☆ x)
          ≡⟨ f₂-nat (base-path uc-path) x ⟩
        f₂ ☆ transport fiber (base-path uc-path) x
          ≡⟨ ap (π₁ f₂) $ fiber-path uc-path ⟩∎
        f₂ ☆ y
          ∎)
      (uc-has-all-path₀ (a , x) (a , y))
-}

ext: agda

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- ----------------------------------------------------------------------
-- The Agda Descriptor Library
--
-- Natural transformations on indexed families (predicates)
-- ----------------------------------------------------------------------

module Relation.Unary.Predicate.Transformation where

open import Data.Empty.Polymorphic using (⊥)
open import Data.Product using (_×_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Unit.Polymorphic using (⊤)
open import Function using (_∘_)
open import Level using (Level; _⊔_; 0ℓ)
open import Relation.Unary

private
  variable
    a b c d ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d

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

-- A predicate transformation is a morphism between 2 predicates
-- indexed by A and B (w/ levels ℓ₁ ℓ₂ for universe polymorphism)

infixr 0 _▷_ _►_

_▷_ : Set a → Set b → (ℓ₁ ℓ₂ : Level) → Set _
(A ▷ B) ℓ₁ ℓ₂ = Pred A ℓ₁ → Pred B ℓ₂

_►_ : Set a → Set b → Set _
(A ► B) = Pred A 0ℓ → Pred B 0ℓ

-- ----------------------------------------------------------------------
-- Composition and Identity

id : (A ▷ A) ℓ₁ ℓ₁
id = Function.id

_○_ : (B ▷ C) ℓ₂ ℓ₃ → (A ▷ B) ℓ₁ ℓ₂ → (A ▷ C) ℓ₁ _
X ○ Y = X ∘ Y

-- TODO: Cateogrical view

-- ----------------------------------------------------------------------
-- Special transformations

empty : (A ▷ B) ℓ₁ ℓ₂
empty = λ _ _ → ⊥

univ : (A ▷ B) ℓ₁ ℓ₂
univ = λ _ _ → ⊤

-- ----------------------------------------------------------------------
-- Operations on transformations

infixr 8 _⇉_
infixl 7 _⋏_
infixl 6 _⋎_

-- Negation
∼ : (A ▷ B) ℓ₁ ℓ₂ → (A ▷ B) ℓ₁ ℓ₂
∼ X = ∁ ∘ X

-- Implication
_⇉_ : (A ▷ B) ℓ₁ ℓ₂ → (A ▷ B) ℓ₁ ℓ₂ → (A ▷ B) ℓ₁ ℓ₂
X ⇉ Y = λ P → X P ⇒ Y P

-- Intersection
_⋏_ : (A ▷ B) ℓ₁ ℓ₂ → (A ▷ B) ℓ₁ ℓ₂ → (A ▷ B) ℓ₁ ℓ₂
X ⋏ Y = λ P → X P ∩ Y P

-- Union
_⋎_ : (A ▷ B) ℓ₁ ℓ₂ → (A ▷ B) ℓ₁ ℓ₂ → (A ▷ B) ℓ₁ ℓ₂
X ⋎ Y = λ P → X P ∪ Y P

-- TODO: Infinitary union + intersection

-- ----------------------------------------------------------------------
-- Combinators on transformations

-- Disjoint sum
_∣∣_ : (A ▷ C) ℓ₁ ℓ₂ → (B ▷ D) ℓ₁ ℓ₂ → (A ⊎ B ▷ C ⊎ D) ℓ₁ ℓ₂
(X ∣∣ Y) P (inj₁ x) = X (P ∘ inj₁) x
(X ∣∣ Y) P (inj₂ y) = Y (P ∘ inj₂) y

-- TODO: Product, etc

max_stars_repo_name: johnyob/agda-desc

max_issues_repo_name: johnyob/agda-desc

max_forks_repo_name: johnyob/agda-desc


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

module CauchyProofs where

-- Proofs about permutations defined in module Cauchy (everything
-- except the multiplicative ones which are defined in CauchyProofsT and
-- CauchyProofsS

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; subst; subst₂; cong; cong₂; setoid;
        proof-irrelevance; module ≡-Reasoning)
open import Data.Nat.Properties
  using (m≤m+n; n≤m+n; n≤1+n; cancel-*-right-≤; ≰⇒>; ¬i+1+j≤i)
open import Data.Nat.Properties.Simple
  using (+-right-identity; +-suc; +-assoc; +-comm;
        *-assoc; *-comm; *-right-zero; distribʳ-*-+; +-*-suc)

open import Data.Nat using (ℕ; suc; _+_; _∸_; _*_; _<_; _≮_; _≤_; _≰_;
  _≥_; z≤n; s≤s; _≟_; _≤?_; ≤-pred; module ≤-Reasoning)
open import Data.Fin
  using (Fin; zero; suc; toℕ; fromℕ; fromℕ≤; _ℕ-_; _≺_; reduce≥;
         raise; inject+; inject₁; inject≤; _≻toℕ_)
  renaming (_+_ to _F+_)
open import Data.Fin.Properties using (bounded; inject+-lemma; to-from)
open import Data.Vec.Properties
  using (lookup∘tabulate; tabulate∘lookup; lookup-allFin; tabulate-∘;
         tabulate-allFin; allFin-map; lookup-++-inject+; lookup-++-≥)

open import Data.Vec
  using (Vec; tabulate; []; _∷_; tail; lookup; zip; zipWith; splitAt;
         _[_]≔_; allFin; toList)
  renaming (_++_ to _++V_; map to mapV; concat to concatV)
open import Function using (id; _∘_; _$_; _∋_; flip)

open import Proofs
open import Cauchy

------------------------------------------------------------------------------
-- Proofs about sequential composition

-- sequential composition with id on the right is identity

scomprid : ∀ {n} → (perm : Cauchy n) → scompcauchy perm (idcauchy n) ≡ perm
scomprid {n} perm =
  begin (scompcauchy perm (idcauchy n)
           ≡⟨ refl ⟩
         tabulate (λ i → lookup (lookup i perm) (allFin n))
           ≡⟨ finext (λ i → lookup-allFin (lookup i perm)) ⟩
         tabulate (λ i → lookup i perm)
           ≡⟨ tabulate∘lookup perm ⟩
         perm ∎)
  where open ≡-Reasoning

-- sequential composition with id on the left is identity

scomplid : ∀ {n} → (perm : Cauchy n) → scompcauchy (idcauchy n) perm ≡ perm
scomplid {n} perm =
  trans (finext (λ i → cong (λ x → lookup x perm) (lookup-allFin i)))
        (tabulate∘lookup perm)

-- sequential composition is associative
scompassoc : ∀ {n} → (π₁ π₂ π₃ : Cauchy n) →
  scompcauchy π₁ (scompcauchy π₂ π₃) ≡ scompcauchy (scompcauchy π₁ π₂) π₃
scompassoc π₁ π₂ π₃ = finext (lookupassoc π₁ π₂ π₃)

------------------------------------------------------------------------------
-- Proofs about additive permutations

lookup-subst2 : ∀ {m m'}
  (i : Fin m) (xs : Vec (Fin m) m) (eq : m ≡ m') →
  lookup (subst Fin eq i)
              (subst Cauchy eq xs) ≡ subst Fin eq (lookup i xs)
lookup-subst2 i xs refl = refl

allFin+ : (m n : ℕ) → allFin (m + n) ≡
          mapV (inject+ n) (allFin m) ++V mapV (raise m) (allFin n)
allFin+ m n = trans (tabulate-split {m} {n})
   (cong₂ _++V_ (tabulate-allFin {m} (inject+  n)) (tabulate-allFin {n} (raise m)))

-- swap+ is idempotent
--
-- outline of swap+idemp proof
--
-- allFin (m + n) ≡ mapV (inject+ n) (allFin m) ++V mapV (raise m) (allFin n)
-- zero-m : Vec (Fin (m + n)) m ≡ mapV (inject+ n) (allFin m)
-- m-sum  : Vec (Fin (m + n)) n ≡ mapV (raise m) (allFin n)
-- allFin (n + m) ≡ mapV (inject+ m) (allFin n) ++V mapV (raise n) (allFin m)
-- zero-n : Vec (Fin (n + m)) n ≡ mapV (inject+ m) (allFin n)
-- n-sum  : Vec (Fin (n + m)) m ≡ mapV (raise n) (allFin m)
--
-- first swap re-arranges allFin (n + m) to n-sum ++V zero-n
-- second swap re-arranges allfin (m + n) to m-sum ++V zero-m
--
-- for i = 0, ..., m-1, we have inject+ n i : Fin (m + n)
-- lookup (lookup (inject+ n i) (n-sum ++V zero-n)) (m-sum ++V zero-m) ==>
-- lookup (lookup i n-sum) (m-sum ++V zero-m) ==>
-- lookup (raise n i) (m-sum ++V zero-m) ==>
-- lookup i zero-m ==>
-- inject+ n i
--
-- for i = m, ..., m+n-1, we have raise m i : Fin (m + n)
-- lookup (lookup (raise m i) (n-sum ++V zero-n)) (m-sum ++V zero-m) ==>
-- lookup (lookup i zero-n) (m-sum ++V zero-m) ==>
-- lookup (inject+ m i) (m-sum ++V zero-m) ==>
-- lookup i m-sum ==>
-- raise m i

swap+-left : (m n : ℕ) → ∀ (i : Fin m) →
  let q = subst Cauchy (+-comm n m) (swap+cauchy n m) in
  lookup (lookup (inject+ n i) (swap+cauchy m n)) q ≡ inject+ n i
swap+-left m n i =
  let q = subst Cauchy (+-comm n m) (swap+cauchy n m) in
  begin (
  lookup (lookup (inject+ n i) (swap+cauchy m n)) q
    ≡⟨ cong (flip lookup q) ( (lookup-++-inject+ (tabulate {m} (id+ {m} {n} ∘ raise n))
                                                                          (tabulate {n} (id+ {m} {n} ∘ inject+ m)) i)) ⟩
  lookup (lookup i (tabulate (λ x → subst Fin (+-comm n m) (raise n x)))) q
    ≡⟨ cong (flip lookup q) (lookup∘tabulate (λ x → subst Fin (+-comm n m) (raise n x)) i) ⟩
  lookup (subst Fin (+-comm n m) (raise n i)) q
    ≡⟨  lookup-subst2 (raise n i) (swap+cauchy n m) (+-comm n m) ⟩
  subst Fin (+-comm n m) (lookup (raise n i) (swap+cauchy n m))
    ≡⟨  cong (subst Fin (+-comm n m))
                   (lookup-++-raise (tabulate {n} (id+ {n} ∘ raise m)) (tabulate {m} (id+ {n} ∘ inject+ n)) i) ⟩
  subst Fin (+-comm n m)
    (lookup i (tabulate (λ z → subst Fin (+-comm m n) (inject+ n z))))
    ≡⟨  subst-lookup-tabulate-inject+ i ⟩
  inject+ n i ∎)
  where open ≡-Reasoning

swap+-right : (m n : ℕ) → (i : Fin n) →
  let q = subst Cauchy (+-comm n m) (swap+cauchy n m) in
  lookup (lookup (raise m i) (swap+cauchy m n)) q ≡ raise m i
swap+-right m n i =
  let q = subst Cauchy (+-comm n m) (swap+cauchy n m) in
  begin (
  lookup (lookup (raise m i) (swap+cauchy m n)) q
    ≡⟨ cong (flip lookup q) ( (lookup-++-raise (tabulate {m} (id+ {m} {n} ∘ raise n))
                                                                       (tabulate {n} (id+ {m} {n} ∘ inject+ m)) i)) ⟩
  lookup (lookup i (tabulate (λ x → subst Fin (+-comm n m) (inject+ m x)))) q
    ≡⟨ cong (flip lookup q) (lookup∘tabulate (λ x → subst Fin (+-comm n m) (inject+ m x)) i) ⟩
  lookup (subst Fin (+-comm n m) (inject+ m i)) q
    ≡⟨  lookup-subst2 (inject+ m i) (swap+cauchy n m) (+-comm n m) ⟩
  subst Fin (+-comm n m) (lookup (inject+ m i) (swap+cauchy n m))
    ≡⟨  cong (subst Fin (+-comm n m))
                   (lookup-++-inject+ (tabulate {n} (id+ {n} ∘ raise m)) (tabulate {m} (id+ {n} ∘ inject+ n)) i) ⟩
  subst Fin (+-comm n m)
    (lookup i (tabulate (λ z → subst Fin (+-comm m n) (raise m z))))
    ≡⟨  subst-lookup-tabulate-raise i ⟩
  raise m i ∎)
  where open ≡-Reasoning

swap+idemp : (m n : ℕ) →
  scompcauchy
    (swap+cauchy m n)
    (subst Cauchy (+-comm n m) (swap+cauchy n m))
  ≡
  allFin (m + n)
swap+idemp m n =
  let q = subst Cauchy (+-comm n m) (swap+cauchy n m) in
  begin
    (tabulate (λ i → lookup (lookup i (swap+cauchy m n)) q)
         ≡⟨ tabulate-split {m} {n} ⟩
     tabulate {m} (λ i → lookup (lookup (inject+ n i) (swap+cauchy m n)) q)
         ++V
     tabulate {n} (λ i → lookup (lookup (raise m i) (swap+cauchy m n)) q)
         ≡⟨ cong₂ _++V_ (finext (swap+-left m n))
                                     (finext (swap+-right m n)) ⟩
     tabulate {m} (inject+ n) ++V tabulate {n} (raise m)
         ≡⟨ unSplit {m} {n} id ⟩
     allFin (m + n) ∎)
  where open ≡-Reasoning

-- Behaviour of parallel additive composition wrt sequential

-- a direct proof is hard, but this is really a statement about vectors

lookup-left : ∀ {m n} → (i : Fin m) → (pm : Cauchy m) → (pn : Cauchy n) →
  lookup (inject+ n i) (mapV (inject+ n) pm ++V mapV (raise m) pn)
  ≡ inject+ n (lookup i pm)
lookup-left {m} {n} i pm pn = look-left i (inject+ n) (raise m) pm pn

-- as is this

lookup-right : ∀ {m n} → (i : Fin n) → (pm : Cauchy m) → (pn : Cauchy n) →
  lookup (raise m i) (mapV (inject+ n) pm ++V mapV (raise m) pn)
  ≡ raise m (lookup i pn)
lookup-right {m} {n} i pm pn = look-right i (inject+ n) (raise m) pm pn

--- find a better name
look-left' : ∀ {m n} → (pm qm : Cauchy m) → (pn qn : Cauchy n) →
      (i : Fin m) →
      (lookup (lookup (inject+ n i) (pcompcauchy pm pn)) (pcompcauchy qm qn))
      ≡ inject+ n (lookup (lookup i pm) qm)
look-left' {m} {n} pm qm pn qn i =
  let pp = pcompcauchy pm pn in
  let qq = pcompcauchy qm qn in
  begin (
    lookup (lookup (inject+ n i) pp) qq
          ≡⟨ cong (flip lookup qq) (lookup-++-inject+ (mapV (inject+ n) pm) (mapV (raise m) pn) i) ⟩
    lookup (lookup i (mapV (inject+ n) pm)) qq
          ≡⟨ cong (flip lookup qq) (lookup-map i (inject+ n) pm) ⟩
    lookup (inject+ n (lookup i pm)) qq
         ≡⟨ lookup-left (lookup i pm) qm qn ⟩
    inject+ n (lookup (lookup i pm) qm) ∎)
  where open ≡-Reasoning

look-right' : ∀ {m n} → (pm qm : Cauchy m) → (pn qn : Cauchy n) →
      (i : Fin n) →
      (lookup (lookup (raise m i) (pcompcauchy pm pn)) (pcompcauchy qm qn))
      ≡ raise m (lookup (lookup i pn) qn)
look-right' {m} {n} pm qm pn qn i =
  let pp = pcompcauchy pm pn in
  let qq = pcompcauchy qm qn in
  begin (
    lookup (lookup (raise m i) pp) qq
          ≡⟨ cong (flip lookup qq) (lookup-++-raise (mapV (inject+ n) pm) (mapV (raise m) pn) i) ⟩
    lookup (lookup i (mapV (raise m) pn)) qq
          ≡⟨ cong (flip lookup qq) (lookup-map i (raise m) pn) ⟩
    lookup (raise m (lookup i pn)) qq
         ≡⟨ lookup-right (lookup i pn) qm qn ⟩
    raise m (lookup (lookup i pn) qn) ∎)
  where open ≡-Reasoning

pcomp-dist : ∀ {m n} → (pm qm : Cauchy m) → (pn qn : Cauchy n) →
    scompcauchy (pcompcauchy pm pn) (pcompcauchy qm qn) ≡
    pcompcauchy (scompcauchy pm qm) (scompcauchy pn qn)
pcomp-dist {m} {n} pm qm pn qn =
  let pp = pcompcauchy pm pn in
  let qq = pcompcauchy qm qn in
  let look = λ i → lookup (lookup i pp) qq in
  begin (scompcauchy pp qq
           ≡⟨ refl ⟩
         tabulate look
           ≡⟨ tabulate-split {m} {n} ⟩
         splitV+ {m} {n} {f = look}
           ≡⟨ cong₂ _++V_ (finext {m} (look-left' pm qm pn qn))
                                      (finext {n} (look-right' pm qm pn qn)) ⟩
         tabulate (λ i → (inject+ n) (lookup (lookup i pm) qm)) ++V
         tabulate (λ i → (raise m) (lookup (lookup i pn) qn))
            ≡⟨ cong₂ _++V_
               (tabulate-∘ (inject+ n) (λ i → lookup (lookup i pm) qm))
               (tabulate-∘ (raise m) (λ i → lookup (lookup i pn) qn)) ⟩
         mapV (inject+ n) (tabulate (λ i → lookup (lookup i pm) qm)) ++V
         mapV (raise m) (tabulate (λ i → lookup (lookup i pn) qn))
            ≡⟨ refl ⟩
         pcompcauchy (scompcauchy pm qm) (scompcauchy pn qn) ∎)
  where open ≡-Reasoning

pcomp-id : ∀ {m n} → pcompcauchy (idcauchy m) (idcauchy n) ≡ idcauchy (m + n)
pcomp-id {m} {n} =
  begin (mapV (inject+ n) (idcauchy m) ++V (mapV (raise m) (idcauchy n))
    ≡⟨ refl ⟩
  mapV (inject+ n) (allFin m) ++V mapV (raise m) (allFin n)
    ≡⟨ cong₂ _++V_
       (sym (tabulate-allFin {m} (inject+ n)))
       (sym (tabulate-allFin (raise m))) ⟩
  tabulate {m} (inject+ n) ++V tabulate {n} (raise m)
    ≡⟨ unSplit {m} {n} id ⟩
  idcauchy (m + n) ∎)
  where open ≡-Reasoning

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
-- Copyright 2019, Xuanrui Qi
-- Original algorithm by: Jacques Garrigue, Xuanrui Qi & Kazunari Tanaka
open import Data.Nat hiding (compare)
open import Data.Nat.Properties
open import Relation.Binary
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; subst; sym; inspect; [_])
open Eq.≡-Reasoning
open import Data.Product
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)

module RedBlack
  {c r} {A : Set c} {_<_ : Rel A r}
  (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
  where

  open IsStrictTotalOrder isStrictTotalOrder

  data Color : Set where
    Red : Color
    Black : Color

  incr-Black : ℕ → Color → ℕ
  incr-Black d Black = suc d
  incr-Black d Red   = d

  color-valid : Color → Color → Set
  color-valid Red Red = ⊥
  color-valid _ _ = ⊤

  inv : Color → Color
  inv Red = Black
  inv Black = Red

  valid-*-Black : ∀ c → color-valid c Black
  valid-*-Black Red = tt
  valid-*-Black Black = tt

  data Tree : ℕ → Color → Set c where
    Leaf : Tree 0 Black
    Node : ∀ {d cₗ cᵣ} c → color-valid c cₗ → color-valid c cᵣ →
           Tree d cₗ → A → Tree d cᵣ → Tree (incr-Black d c) c

  RNode : ∀ {d} → Tree d Black → A → Tree d Black → Tree d Red
  RNode = Node Red tt tt

  BNode : ∀ {d cₗ cᵣ} → Tree d cₗ → A → Tree d cᵣ → Tree (suc d) Black
  BNode = Node Black tt tt

  -- Insertion algorithm
  data InsTree : ℕ → Color → Set c where
    Fix : ∀ {d} → Tree d Black → A → Tree d Black → A → Tree d Black → InsTree d Red
    T : ∀ {d c} cₚ → Tree d c → InsTree d cₚ

  InsTree-color : ∀ {d c} → InsTree d c → Color
  InsTree-color (Fix _ _ _ _ _) = Red
  InsTree-color (T _ _) = Black

  fix-color : ∀ {d c} → InsTree d c → Color
  fix-color (Fix _ _ _ _ _) = Black
  fix-color (T {c = c} _ _) = c

  fix-InsTree : ∀ {d c} → (t : InsTree d c) → Tree (incr-Black d (inv (InsTree-color t))) (fix-color t)
  fix-InsTree (Fix t₁ x t₂ y t₃) = BNode (RNode t₁ x t₂) y t₃
  fix-InsTree (T _ t) = t

  balanceₗ : ∀ {d cₗ cᵣ} c → (l : InsTree d cₗ) → A → Tree d cᵣ → color-valid c (InsTree-color l) → color-valid c cᵣ → InsTree (incr-Black d c) c
  balanceₗ Black (Fix t₁ x t₂ y t₃) z t₄ _ _ = T Black (RNode (BNode t₁ x t₂) y (BNode t₃ z t₄))
  balanceₗ Black (T _ l) v r _ _ = T Black (BNode l v r)
  balanceₗ {cᵣ = Black} Red (T _ (Node {cₗ = Black} {cᵣ = Black} Red _ _ t₁ x t₂)) y t₃ _ _ = Fix t₁ x t₂ y t₃
  balanceₗ {cᵣ = Black} Red (T {c = Black} _ l) v r _ _ = T Red (RNode l v r)

  balanceᵣ : ∀ {d cₗ cᵣ} c → Tree d cₗ → A → (r : InsTree d cᵣ) → color-valid c cₗ → color-valid c (InsTree-color r) → InsTree (incr-Black d c) c
  balanceᵣ Black t₁ x (Fix t₂ y t₃ z t₄) _ _ = T Black (RNode (BNode t₁ x t₂) y (BNode t₃ z t₄))
  balanceᵣ Black l v (T _ r) _ _ = T Black (BNode l v r)
  balanceᵣ {cₗ = Black} Red t₁ x (T _ (Node {cₗ = Black} {cᵣ = Black} Red _ _ t₂ y t₃)) _ _ = Fix t₁ x t₂ y t₃
  balanceᵣ {cₗ = Black} Red l v (T {c = Black} _ r) _ _ = T Red (RNode l v r)

  ins : ∀ {d c} → A → Tree d c → InsTree d c
  ins x Leaf = T Black (RNode Leaf x Leaf)
  ins x (Node c _ _ l v r) with (compare x v)
  ins x (Node c _ _ l v r)    | tri< x<v _ _ with ins x l | inspect (ins x) l
  ins x (Node Black _ validᵣ l v r) | _ | Fix _ _ _ _ _   | [ insₗ ] = balanceₗ Black (ins x l) v r tt tt
  ins x (Node c     _ validᵣ l v r) | _ | T _ _           | [ insₗ ] = balanceₗ c (ins x l) v r validₗ validᵣ
    where
      validₗ = subst (λ t → color-valid c (InsTree-color t)) (sym insₗ) (valid-*-Black c)
  ins x t@(Node c _ _ l v r)  | tri≈ _ x≡v _ = T _ t
  ins x (Node c _ _ l v r)    | tri> _ _ x>v with ins x r | inspect (ins x) r
  ins x (Node Black validₗ _ l v r) | _ | Fix _ _ _ _ _   | [ insᵣ ] = balanceᵣ Black l v (ins x r) tt tt
  ins x (Node c     validₗ _ l v r) | _ | T _ _           | [ insᵣ ] = balanceᵣ c l v (ins x r) validₗ validᵣ
    where
      validᵣ = subst (λ t → color-valid c (InsTree-color t)) (sym insᵣ) (valid-*-Black c)

  blacken : ∀ {d c} → Tree d c → Tree (incr-Black d (inv c)) Black
  blacken Leaf = Leaf
  blacken (Node Black _ _ l v r) = BNode l v r
  blacken (Node Red _ _ l v r) = BNode l v r

  insert : ∀ {d} → A → Tree d Black → ∃ (λ d' → Tree d' Black)
  insert {d = d} x t with ins x t
  ... | T {c = c} _ t' = (incr-Black d (inv c) , blacken t')

  -- Deletion algorithm
  data DelTree : ℕ → Color → Set c where
    Stay : ∀ {d c} cₚ → color-valid c (inv cₚ) → Tree d c → DelTree d cₚ
    Down : ∀ {d} → Tree d Black → DelTree (suc d) Black

  bal-right : ∀ {d cₗ cᵣ} c → Tree d cₗ → A → DelTree d cᵣ → color-valid c cₗ → color-valid c cᵣ → DelTree (incr-Black d c) c
  bal-right {cₗ = Black} Red l v (Stay {c = Black} _ _ r) _ _ = Stay Red tt (RNode l v r)
  bal-right {cₗ = Black} Red l v (Stay {c = Red} Red _ _) _ ()
  bal-right Red (Node {cᵣ = Black} Black _ _ t₁ x t₂) y (Down t₃) _ _ = Stay Red tt (BNode t₁ x (RNode t₂ y t₃))
  bal-right Red (Node {cᵣ = Red} Black _ _ t₁ x (Node _ _ _ t₂ y t₃)) z (Down t₄) _ _ = Stay Red tt (RNode (BNode t₁ x t₂) y (BNode t₃ z t₄))
  bal-right Black l v (Stay _ _ r) _ _ = Stay Black tt (BNode l v r)
  bal-right Black (Node {cᵣ = Red} Black _ _ t₁ x (Node _ _ _ t₂ y t₃)) z (Down t₄) _ _ = Stay Black tt (BNode (BNode t₁ x t₂) y (BNode t₃ z t₄))
  bal-right Black (Node {cₗ = Black} {cᵣ = Black} Red _ _ t₁ x (Node {cᵣ = Black} _ _ _ t₂ y t₃)) z (Down t₄) _ _ =
    Stay Black tt (BNode t₁ x (BNode t₂ y (RNode t₃ z t₄)))
  bal-right Black (Node {cₗ = Black} {cᵣ = Black} Red _ _ t₁ x (Node {cᵣ = Red} _ _ _ t₂ y (Node {cₗ = Black} {cᵣ = Black} _ _ _ t₃ z t₄))) w (Down t₅) _ _ =
    Stay Black tt (BNode t₁ x (RNode (BNode t₂ y t₃) z (BNode t₄ w t₅)))
  bal-right Black (Node {cᵣ = Black} Black _ _ t₁ x t₂) y (Down t₃) _ _ = Down (BNode t₁ x (RNode t₂ y t₃))

  bal-left : ∀ {d cₗ cᵣ} c → DelTree d cₗ → A → Tree d cᵣ → color-valid c cₗ → color-valid c cᵣ → DelTree (incr-Black d c) c
  bal-left {cₗ = Black} {cᵣ = Black} Red (Stay {c = Black} _ _ l) v r _ _ = Stay Red tt (RNode l v r)
  bal-left {cₗ = Black} {cᵣ = Black} Red (Stay {c = Red} _ () l) v r _ _
  bal-left {cₗ = Black} {cᵣ = Black} Red (Down t₁) x (Node {cₗ = Red} _ _ _ (Node {cₗ = Black} {cᵣ = Black} _ _ _ t₂ y t₃) z t₄) _ _ =
    Stay Red tt (RNode (BNode t₁ x t₂) y (BNode t₃ z t₄))
  bal-left {cₗ = Black} {cᵣ = Black} Red (Down t₁) x (Node {cₗ = Black} _ _ _ t₂ y t₃) _ _ = Stay Red tt (BNode (RNode t₁ x t₂) y t₃)
  bal-left Black (Stay _ _ l) v r _ _ = Stay Black tt (BNode l v r)
  bal-left {cᵣ = Black} Black (Down t₁) x (Node {cₗ = Red} Black _ _ (Node {cₗ = Black} {cᵣ = Black} _ _ _ t₂ y t₃) z t₄) _ _ =
    Stay Black tt (BNode (BNode t₁ x t₂) y (BNode t₃ z t₄))
  bal-left {cᵣ = Red} Black (Down t₁) x (Node {cₗ = Black} {cᵣ = Black} _ _ _ (Node {cₗ = Red} Black _ _ (Node {cₗ = Black} {cᵣ = Black} _ _ _ t₂ y t₃) z t₄) w t₅) _ _ =
    Stay Black tt (BNode (BNode t₁ x t₂) y (RNode (BNode t₃ z t₄) w t₅))
  bal-left {cᵣ = Red} Black (Down t₁) x (Node {cₗ = Black} {cᵣ = Black} _ _ _ (Node {cₗ = Black} _ _ _ t₂ y t₃) z t₄) _ _ =
    Stay Black tt (BNode (BNode (RNode t₁ x t₂) y t₃) z t₄)
  bal-left {cᵣ = Black} Black (Down t₁) x (Node {cₗ = Black} _ _ _ t₂ y t₃) _ _ = Down (BNode (RNode t₁ x t₂) y t₃)

max_stars_repo_name: xuanruiqi/dtp

max_issues_repo_name: xuanruiqi/dtp

max_forks_repo_name: xuanruiqi/dtp


text:
module foldr-++ where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; cong)
open Eq.≡-Reasoning
open import lists using (List; _∷_; []; _++_; foldr)

-- 結合したリストの重畳は、重畳した結果を初期値とした重畳と等しいことの証明
foldr-++ : ∀ {A B : Set} → (_⊗_ : A → B → B) → (e : B) → (xs ys : List A)
  → foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
foldr-++ _⊗_ e [] ys =
  begin
    foldr _⊗_ e ([] ++ ys)
  ≡⟨⟩
    foldr _⊗_ e ys
  ≡⟨⟩
    foldr _⊗_ (foldr _⊗_ e ys) []
  ∎
foldr-++ _⊗_ e (x ∷ xs) ys =
  begin
    foldr _⊗_ e ((x ∷ xs) ++ ys)
  ≡⟨⟩
    x ⊗ (foldr _⊗_ e (xs ++ ys))
  ≡⟨ cong (x ⊗_) (foldr-++ _⊗_ e xs ys) ⟩
    x ⊗ (foldr _⊗_ (foldr _⊗_ e ys) xs)
  ≡⟨⟩
    foldr _⊗_ (foldr _⊗_ e ys) (x ∷ xs)
  ∎

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
module LC.Subst.Term where

open import LC.Base
open import LC.Subst.Var

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Nullary

--------------------------------------------------------------------------------
-- lifting terms

lift : (n i : ℕ) → Term → Term
lift n i (var x) = var (lift-var n i x)
lift n i (ƛ M)   = ƛ lift (suc n) i M
lift n i (M ∙ N) = lift n i M ∙ lift n i N

--------------------------------------------------------------------------------
-- properties of lift

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

--             lift l (n + i)
--        ∙ --------------------------> ∙
--        |                             |
--        |                             |
--   lift l (n + m + i)           lift (l + n) m
--        |                             |
--        ∨                             ∨
--        ∙ --------------------------> ∙
--

lift-lemma : ∀ l m n i N → lift l (n + m + i) N ≡ lift (l + n) m (lift l (n + i) N)
lift-lemma l m n i (var x) = cong var_ (LC.Subst.Var.lift-var-lemma l m n i x)
lift-lemma l m n i (ƛ M)   = cong ƛ_ (lift-lemma (suc l) m n i M)
lift-lemma l m n i (M ∙ N) = cong₂ _∙_ (lift-lemma l m n i M) (lift-lemma l m n i N)

--                lift (l + n) i
--        ∙ --------------------------> ∙
--        |                             |
--        |                             |
--   lift l m                      lift l m
--        |                             |
--        ∨                             ∨
--        ∙ --------------------------> ∙
--              lift (l + m + n) i

lift-lift : ∀ l m n i N → lift l m (lift (l + n) i N) ≡ lift (l + m + n) i (lift l m N)
lift-lift l m n i (var x) = cong var_ (lift-var-lift-var l m n i x)
lift-lift l m n i (ƛ N)   = cong ƛ_ (lift-lift (suc l) m n i N)
lift-lift l m n i (M ∙ N) = cong₂ _∙_ (lift-lift l m n i M) (lift-lift l m n i N)

--------------------------------------------------------------------------------
-- substituting variables

data Match : ℕ → ℕ → Set where
  Under : ∀ {i x} → x     < i → Match x       i
  Exact : ∀ {i x} → x     ≡ i → Match x       i
  Above : ∀ {i} v → suc v > i → Match (suc v) i

open import Relation.Binary.Definitions

match : (x i : ℕ) → Match x i
match x       i with <-cmp x i
match x       i | tri< a ¬b ¬c = Under a
match x       i | tri≈ ¬a b ¬c = Exact b
match (suc x) i | tri> ¬a ¬b c = Above x c

subst-var : ∀ {x i} → Match x i → Term → Term
subst-var {x}     (Under _)     N = var x
subst-var {_} {i} (Exact _)     N = lift 0 i N
subst-var         (Above x _) N = var x

--------------------------------------------------------------------------------
-- properties of subst-var

open import Relation.Nullary.Negation using (contradiction)
open ≡-Reasoning

subst-var-match-< : ∀ {m n} N → (m<n : m < n) → subst-var (match m n) N ≡ var m
subst-var-match-< {m} {n} N m<n with match m n
... | Under m<n' = refl
... | Exact m≡n  = contradiction m≡n (<⇒≢ m<n)
... | Above _ m>n = contradiction m>n (<⇒≱ (≤-step m<n))

subst-var-match-≡ : ∀ {m n} N → (m≡n : m ≡ n) → subst-var {_} {n} (match m n) N ≡ lift 0 n N
subst-var-match-≡ {m} {.m} N refl with match m m
... | Under m<m = contradiction refl (<⇒≢ m<m)
... | Exact m≡m = refl
... | Above _ m>m = contradiction refl (<⇒≢ m>m)

subst-var-match-> : ∀ {m n} N → (1+m>n : suc m > n) → subst-var (match (suc m) n) N ≡ var m
subst-var-match-> {m} {n} N 1+m<n with match (suc m) n
... | Under m<n = contradiction m<n (<⇒≱ (≤-step 1+m<n))
... | Exact m≡n = contradiction (sym m≡n) (<⇒≢ 1+m<n)
... | Above _ m>n = refl

--              subst-var (match x                             m)
--        ∙ -------------------------------------------------------> ∙
--        |                                                          |
--        |                                                          |
--     lift n                                                  lift (m + n)
--        |                                                          |
--        ∨                                                          ∨
--        ∙ --------------------------------------------------------> ∙
--              subst-var (match (lift-var (suc (m + n)) i x) m)

open import Relation.Binary.PropositionalEquality hiding (preorder; [_])
open ≡-Reasoning

subst-var-lift : ∀ m n i x N
    → subst-var (match (lift-var (suc (m + n)) i x) m) (lift n i N)
    ≡ lift (m + n) i (subst-var (match x m) N)
subst-var-lift m n i x N with match x m
... | Under x<m =
    begin
        subst-var (match (lift-var (suc (m + n)) i x) m) (lift n i N)
    ≡⟨ cong (λ w → subst-var (match w m) (lift n i N)) (LC.Subst.Var.lift-var-> prop1) ⟩
        subst-var (match x m) (lift n i N)
    ≡⟨ subst-var-match-< (lift n i N) x<m ⟩
        var x
    ≡⟨ cong var_ (sym (LC.Subst.Var.lift-var-> prop2)) ⟩
        lift (m + n) i (var x)
    ∎
    where
      prop1 : suc (m + n) > x
      prop1 = ≤-trans x<m (≤-step (m≤m+n m n))

      prop2 : m + n > x
      prop2 = ≤-trans x<m (m≤m+n m n)

... | Exact refl =
      begin
        subst-var (match (lift-var (suc (m + n)) i m) m) (lift n i N)
      ≡⟨ cong (λ w → subst-var (match w m) (lift n i N)) (LC.Subst.Var.lift-var-> prop) ⟩
        subst-var (match m m) (lift n i N)
      ≡⟨ subst-var-match-≡ (lift n i N) refl ⟩
        lift 0 m (lift n i N)
      ≡⟨ lift-lift 0 m n i N ⟩
        lift (m + n) i (lift 0 m N)
      ∎
      where
        prop : suc (m + n) > m
        prop =  s≤s (m≤m+n m n)

... | Above v m≤v with inspectBinding (suc m + n) (suc v)
... | Free n≤x =
  begin
    subst-var (match (i + suc v) m) (lift n i N)
  ≡⟨ cong (λ w → subst-var (match w m) (lift n i N)) (+-suc i v) ⟩
    subst-var (match (suc i + v) m) (lift n i N)
  ≡⟨ subst-var-match-> (lift n i N) prop ⟩
    var (i + v)
  ≡⟨ cong var_ (sym (LC.Subst.Var.lift-var-≤ prop2)) ⟩
    var (lift-var (m + n) i v)
  ∎
  where
    prop : suc (i + v) > m
    prop = s≤s (≤-trans (≤-pred m≤v) (m≤n+m v i))

    prop2 : m + n ≤ v
    prop2 = ≤-pred n≤x
... | Bound n>x =
  begin
    subst-var (match (suc v) m) (lift n i N)
  ≡⟨ subst-var-match-> {v} {m} (lift n i N) m≤v ⟩
    var v
  ≡⟨ cong var_ (sym (LC.Subst.Var.lift-var-> {m + n} {i} {v} (≤-pred n>x))) ⟩
    var (lift-var (m + n) i v)
  ∎

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


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.Base.Types
open import LibraBFT.Concrete.Records
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Impl.Consensus.ConsensusProvider            as ConsensusProvider
open import LibraBFT.Impl.Consensus.Properties.ConsensusProvider as ConsensusProviderProps
import      LibraBFT.Impl.IO.OBM.GenKeyFile                      as GenKeyFile
open import LibraBFT.Impl.IO.OBM.InputOutputHandlers
open import LibraBFT.Impl.IO.OBM.Start
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.Impl.Properties.Util
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.NetworkMsg
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.PKCS
open import Util.Prelude
open import Yasm.System ℓ-RoundManager ℓ-VSFP ConcSysParms

open Invariants
open RoundManagerTransProps
open InitProofDefs

module LibraBFT.Impl.IO.OBM.Properties.Start where

module startViaConsensusProviderSpec
  (now   : Instant)
  (nfl   : GenKeyFile.NfLiwsVsVvPe)
  (txTDS : TxTypeDependentStuffForNetwork)
  where
  -- It is somewhat of an overkill to write a separate contract for the last step,
  -- but keeping it explicit for pedagogical reasons
  contract-step₁ : ∀ (tup : (NodeConfig × OnChainConfigPayload × LedgerInfoWithSignatures × SK × ProposerElection))
                 → EitherD-weakestPre (startViaConsensusProvider-ed.step₁ now nfl txTDS tup) (InitContract nothing)
  contract-step₁ (nodeConfig , payload , liws , sk , pe) =
    startConsensusSpec.contract' nodeConfig now payload liws sk ObmNeedFetch∙new
                                 (txTDS ^∙ ttdsnProposalGenerator) (txTDS ^∙ ttdsnStateComputer)

  contract' : EitherD-weakestPre (startViaConsensusProvider-ed-abs now nfl txTDS) (InitContract nothing)
  contract' rewrite startViaConsensusProvider-ed-abs-≡ =
    -- TODO-2: this is silly; perhaps we should have an EitherD-⇒-bind-const or something for when
    -- we don't need to know anything about the values returned by part before the bind?
    EitherD-⇒-bind (ConsensusProvider.obmInitialData-ed-abs nfl)
                   (EitherD-vacuous (ConsensusProvider.obmInitialData-ed-abs nfl))
                   P⇒Q
       where
       P⇒Q : EitherD-Post-⇒ (const Unit) (EitherD-weakestPre-bindPost _ (InitContract nothing))
       P⇒Q (Left _)     _        = tt
       P⇒Q (Right tup') _ c refl = contract-step₁ tup'


text:
open import Level
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

module AlgProg where

-- 1.1 Datatypes

private
 variable
  l : Level

data Bool : Set where
 false : Bool
 true : Bool

data Char : Set where
 ca : Char
 cb : Char
 cc : Char

data Either : Set where
 bool : Bool → Either
 char : Char → Either

data Both : Set where
 tuple : Bool × Char → Both

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

switch : Both → Both
switch (tuple (b , c)) = tuple (not b , c)

and : (Bool × Bool) → Bool
and (false , _) = false
and (true , b) = b

cand : Bool → Bool → Bool
cand false _ = false
cand true b = b

curry' : {A B C : Set} → (B → (C → A)) → ((B × C) → A)
curry' f (b , c) = f b c

data maybe (A : Set l) : Set l where
 nothing : maybe A
 just : (x : A) → maybe A

-- 1.2 Natural Numbers

data Nat : Set where
 zero' : Nat
 1+ : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

{-
plus : Nat × Nat → Nat
plus (n , zero') = n
plus (n , succ m) = succ (plus (n , m))

mult : Nat × Nat → Nat
mult (n , zero') = zero'
mult (n , succ m) = plus (n , mult (n , m))

-}
_+_ : Nat → Nat → Nat
n + 0 = n
n + (1+ m) = 1+ (n + m)

_*_ : Nat → Nat → Nat
n * 0 = 0
n * (1+ m) = n + (n * m)

fact : Nat → Nat
fact 0 = 1
fact (1+ n) = (1+ n) * (fact n)

fib : Nat → Nat
fib 0 = 0
fib (1+ 0) = 1
fib (1+ (1+ n)) = (fib n) + (fib (1+ n))

foldn : {A : Set} → A → (A → A) → (Nat → A)
foldn c h 0 = c
foldn c h (1+ n) = h (foldn c h n)

foldn1+is+ : (m n : Nat) → (m + n) ≡ ((foldn m 1+) n)
foldn1+is+ m 0 = refl
foldn1+is+ m (1+ n) = cong 1+ (foldn1+is+ m n)

foldn+is* : (m n : Nat) → m * n ≡ (foldn 0 (λ x → m + x)) n
foldn+is* m 0 = refl
foldn+is* m (1+ n) = cong (λ x → m + x) (foldn+is* m n)

expn : Nat → Nat → Nat
expn m = foldn 1 (λ n →  m * n)

outl : {A B : Set} → (A × B) → A
outl (fst , snd) = fst

outr : {A B : Set} → (A × B) → B
outr (fst , snd) = snd

f1 : (Nat × Nat) → Nat × Nat
f1 (m , n) = (1+ m , (1+ m) * n)

rec-× : {A B C D : Set} → (f : A → B) → (g : C → D) → ((A × C) -> (B × D))
rec-× f g (a , c) = (f a , g c)

outrFoldnIsFact : (n : Nat) → (foldn (0 , 1) f1 n) ≡ (n , fact n)
outrFoldnIsFact zero' = refl
outrFoldnIsFact (1+ n) rewrite (outrFoldnIsFact n) = refl

-- 1.3 Lists

data listr (A : Set l) : Set l where
 nil : listr A
 cons : A → listr A → listr A

data listl (A : Set l) : Set l where
 nil : listl A
 snoc : listl A → A → listl A

snocr : {A : Set} → listr A → A → listr A
snocr nil a = cons a nil
snocr (cons a0 as) a1 = cons a0 (snocr as a1)

convert : {A : Set} → listl A → listr A
convert nil = nil
convert (snoc xs x) = snocr (convert xs) x

_++_ : {A : Set} → listl A → listl A → listl A
xs ++ nil = xs
xs ++ snoc ys x = snoc (xs ++ ys) x

++-assoc : {A : Set} → (xs ys zs : listl A) → (xs ++ (ys ++ zs)) ≡ ((xs ++ ys) ++ zs)
++-assoc xs ys nil = refl
++-assoc xs ys (snoc zs x) = cong (λ y → snoc y x) (++-assoc xs ys zs)

listrF : {A B : Set} → (A → B) → listr A → listr B
listrF f nil = nil
listrF f (cons x as) = cons (f x) (listrF f as)

foldr : {A B : Set} → B → (A → B → B) → (listr A → B)
foldr c h nil = c
foldr c h (cons a as) = h a (foldr c h as)

max_stars_repo_name: polymonyrks/algprog

max_issues_repo_name: polymonyrks/algprog

max_forks_repo_name: polymonyrks/algprog


text:
{- Formal verification of authenticated append-only skiplists in Agda, version 1.0.

   Copyright (c) 2020 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 Data.Unit.NonEta
open import Data.Empty
open import Data.Sum
open import Data.Product
open import Data.Product.Properties
open import Data.Fin
open import Data.Fin.Properties renaming (_≟_ to _≟Fin_)
open import Data.Nat renaming (_≟_ to _≟ℕ_; _≤?_ to _≤?ℕ_)
open import Data.Nat.Divisibility
open import Data.List renaming (map to List-map)
open import Data.List.Properties using (∷-injective)
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All renaming (map to All-map)
open import Data.List.Relation.Unary.All.Properties hiding (All-map)
open import Data.List.Relation.Unary.Any.Properties
open import Data.List.Relation.Binary.Pointwise using (decidable-≡)
open import Data.Bool
open import Data.Maybe renaming (map to Maybe-map)

open import Function

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Core
open import Relation.Nullary

-- This module provides an injective way to encode natural numbers

module Data.Nat.Encode where

 -- Represents a list of binary digits with
 -- a leading one in reverse order.
 --
 -- 9, in binary: 1001
 --
 -- remove leading 1: 001,
 -- reverse: 100
 --
 -- as 𝔹+1: I O O ε
 --
 data 𝔹+1 : Set where
   ε  : 𝔹+1
   O_ : 𝔹+1 → 𝔹+1
   I_ : 𝔹+1 → 𝔹+1

 from𝔹+1 : 𝔹+1 → ℕ
 from𝔹+1 ε     = 1
 from𝔹+1 (O b) = 2 * from𝔹+1 b
 from𝔹+1 (I b) = suc (2 * from𝔹+1 b)

 -- Adds zero to our representation
 data 𝔹 : Set where
   z : 𝔹
   s : 𝔹+1 → 𝔹

 from𝔹 : 𝔹 → ℕ
 from𝔹 z = 0
 from𝔹 (s b) = from𝔹+1 b

 inc : 𝔹+1 → 𝔹+1
 inc ε     = O ε
 inc (O x) = I x
 inc (I x) = O (inc x)

 inc-ε-⊥ : ∀{b} → inc b ≡ ε → ⊥
 inc-ε-⊥ {ε}   ()
 inc-ε-⊥ {O b} ()
 inc-ε-⊥ {I b} ()

 to𝔹+1 : ℕ → 𝔹+1
 to𝔹+1 zero    = ε
 to𝔹+1 (suc n) = inc (to𝔹+1 n)

 to𝔹 : ℕ → 𝔹
 to𝔹 zero    = z
 to𝔹 (suc n) = s (to𝔹+1 n)

 toBitString+1 : 𝔹+1 → List Bool
 toBitString+1 ε = []
 toBitString+1 (I x) = true ∷ toBitString+1 x
 toBitString+1 (O x) = false ∷ toBitString+1 x

 toBitString : 𝔹 → List Bool
 toBitString z = []
 -- For an actual binary number as we know, we need
 -- to reverse the result of toBitString+1; for the sake of encoding
 -- a number as a list of booleans, this works just fine
 toBitString (s x) = true ∷ toBitString+1 x

 encodeℕ : ℕ → List Bool
 encodeℕ = toBitString ∘ to𝔹

 ---------------------
 -- Injectivity proofs

 O-inj : ∀{b1 b2} → O b1 ≡ O b2 → b1 ≡ b2
 O-inj refl = refl

 I-inj : ∀{b1 b2} → I b1 ≡ I b2 → b1 ≡ b2
 I-inj refl = refl

 s-inj : ∀{b1 b2} → s b1 ≡ s b2 → b1 ≡ b2
 s-inj refl = refl

 inc-inj : ∀ b1 b2 → inc b1 ≡ inc b2 → b1 ≡ b2
 inc-inj ε ε hip = refl
 inc-inj ε (I b2) hip = ⊥-elim (inc-ε-⊥ (sym (O-inj hip)))
 inc-inj (I b1) ε hip = ⊥-elim (inc-ε-⊥ (O-inj hip))
 inc-inj (O b1) (O b2) hip = cong O_ (I-inj hip)
 inc-inj (I b1) (I b2) hip = cong I_ (inc-inj b1 b2 (O-inj hip))

 to𝔹+1-inj : ∀ n m → to𝔹+1 n ≡ to𝔹+1 m → n ≡ m
 to𝔹+1-inj zero zero hip = refl
 to𝔹+1-inj zero (suc m) hip = ⊥-elim (inc-ε-⊥ (sym hip))
 to𝔹+1-inj (suc n) zero hip = ⊥-elim (inc-ε-⊥ hip)
 to𝔹+1-inj (suc n) (suc m) hip = cong suc (to𝔹+1-inj n m (inc-inj _ _ hip))

 to𝔹-inj : ∀ n m → to𝔹 n ≡ to𝔹 m → n ≡ m
 to𝔹-inj zero zero hip = refl
 to𝔹-inj (suc n) (suc m) hip = cong suc (to𝔹+1-inj n m (s-inj hip))

 toBitString+1-inj : ∀ b1 b2 → toBitString+1 b1 ≡ toBitString+1 b2
                   → b1 ≡ b2
 toBitString+1-inj ε ε hip = refl
 toBitString+1-inj (O b1) (O b2) hip
   = cong O_ (toBitString+1-inj b1 b2 (proj₂ (∷-injective hip)))
 toBitString+1-inj (I b1) (I b2) hip
   = cong I_ (toBitString+1-inj b1 b2 (proj₂ (∷-injective hip)))

 toBitString-inj : ∀ b1 b2 → toBitString b1 ≡ toBitString b2
                 → b1 ≡ b2
 toBitString-inj z z hip = refl
 toBitString-inj (s x) (s x₁) hip
   = cong s (toBitString+1-inj x x₁ (proj₂ (∷-injective hip)))

 encodeℕ-inj : ∀ n m → encodeℕ n ≡ encodeℕ m → n ≡ m
 encodeℕ-inj n m hip = to𝔹-inj n m (toBitString-inj (to𝔹 n) (to𝔹 m) hip)


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

open import HoTT
open import groups.Pointed

module groups.Int where

abstract
  ℤ→ᴳ-η : ∀ {i} {G : Group i} (φ : ℤ-group →ᴳ G)
    → GroupHom.f φ ∼ Group.exp G (GroupHom.f φ 1)
  ℤ→ᴳ-η φ (pos 0) = GroupHom.pres-ident φ
  ℤ→ᴳ-η φ (pos 1) = idp
  ℤ→ᴳ-η {G = G} φ (pos (S (S n))) =
      GroupHom.pres-comp φ 1 (pos (S n))
    ∙ ap (Group.comp G (GroupHom.f φ 1)) (ℤ→ᴳ-η φ (pos (S n)))
    ∙ ! (Group.exp-+ G (GroupHom.f φ 1) 1 (pos (S n)))
  ℤ→ᴳ-η φ (negsucc 0) = GroupHom.pres-inv φ 1
  ℤ→ᴳ-η {G = G} φ (negsucc (S n)) =
      GroupHom.pres-comp φ -1 (negsucc n)
    ∙ ap2 (Group.comp G) (GroupHom.pres-inv φ 1) (ℤ→ᴳ-η φ (negsucc n))
    ∙ ! (Group.exp-+ G (GroupHom.f φ 1) -1 (negsucc n))

ℤ-idf-η : ∀ i → i == Group.exp ℤ-group 1 i
ℤ-idf-η = ℤ→ᴳ-η (idhom _)

ℤ→ᴳ-unicity : ∀ {i} {G : Group i}
  → (φ ψ : ℤ-group →ᴳ G)
  → GroupHom.f φ 1 == GroupHom.f ψ 1
  → GroupHom.f φ ∼ GroupHom.f ψ
ℤ→ᴳ-unicity {G = G} φ ψ p i =
  ℤ→ᴳ-η φ i ∙ ap (λ g₁ → Group.exp G g₁ i) p ∙ ! (ℤ→ᴳ-η ψ i)

ℤ→ᴳ-equiv-idf : ∀ {i} (G : Group i) → (ℤ-group →ᴳ G) ≃ Group.El G
ℤ→ᴳ-equiv-idf G = equiv (λ φ → GroupHom.f φ 1) (exp-hom G)
  (λ _ → idp) (λ φ → group-hom= $ λ= $ ! ∘ ℤ→ᴳ-η φ)
  where open Group G

ℤ→ᴳ-iso-idf : ∀ {i} (G : AbGroup i) → hom-group ℤ-group G ≃ᴳ AbGroup.grp G
ℤ→ᴳ-iso-idf G = ≃-to-≃ᴳ (ℤ→ᴳ-equiv-idf (AbGroup.grp G)) (λ _ _ → idp)

ℤ-⊙group : ⊙Group₀
ℤ-⊙group = ⊙[ ℤ-group , 1 ]ᴳ

ℤ-is-infinite-cyclic : is-infinite-cyclic ℤ-⊙group
ℤ-is-infinite-cyclic = is-eq
  (Group.exp ℤ-group 1)
  (idf ℤ)
  (! ∘ ℤ-idf-η)
  (! ∘ ℤ-idf-η)

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

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

module Setoids.Equality {a b : _} {A : Set a} (S : Setoid {a} {b} A) where

open import Setoids.Subset S

_=S_ : {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} (s1 : subset pred1) (s2 : subset pred2) → Set _
_=S_ {pred1 = pred1} {pred2} s1 s2 = (x : A) → (pred1 x → pred2 x) && (pred2 x → pred1 x)

setoidEqualitySymmetric : {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} → (s1 : subset pred1) (s2 : subset pred2) → s1 =S s2 → s2 =S s1
setoidEqualitySymmetric s1 s2 s1=s2 x = _&&_.snd (s1=s2 x) ,, _&&_.fst (s1=s2 x)

setoidEqualityTransitive : {c d e : _} {pred1 : A → Set c} {pred2 : A → Set d} {pred3 : A → Set e} (s1 : subset pred1) (s2 : subset pred2) (s3 : subset pred3) → s1 =S s2 → s2 =S s3 → s1 =S s3
setoidEqualityTransitive s1 s2 s3 s1=s2 s2=s3 x with s1=s2 x
setoidEqualityTransitive s1 s2 s3 s1=s2 s2=s3 x | p1top2 ,, p1top2' with s2=s3 x
setoidEqualityTransitive s1 s2 s3 s1=s2 s2=s3 x | p1top2 ,, p1top2' | fst ,, snd = (λ i → fst (p1top2 i)) ,, λ i → p1top2' (snd i)

setoidEqualityReflexive : {c : _} {pred : A → Set c} (s : subset pred) → s =S s
setoidEqualityReflexive s x = (λ x → x) ,, λ x → x


text:
-- Andreas, 2015-10-28 adapted from test case by
-- Ulf, 2014-02-06, shrunk from Wolfram Kahl's report

open import Common.Equality
open import Common.Unit
open import Common.Nat

postulate
  prop : ∀ x → x ≡ unit

record StrictTotalOrder : Set where
  field compare : Unit
open StrictTotalOrder

module M (Key : StrictTotalOrder) where

    postulate
      intersection′-₁ : ∀ x → x ≡ compare Key

    to-∈-intersection′  : Nat → Unit → Unit → Set
    to-∈-intersection′ zero x h = Unit
    to-∈-intersection′ (suc n) x h with intersection′-₁ x
    to-∈-intersection′ (suc n) ._ h  | refl with prop h
    to-∈-intersection′ (suc n) ._ ._ | refl    | refl = to-∈-intersection′ n unit unit

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- A non-recursive variant of H-level.Truncation.Propositional.Erased
------------------------------------------------------------------------

-- The definition does use natural numbers. The code is based on van
-- Doorn's "Constructing the Propositional Truncation using
-- Non-recursive HITs".

{-# OPTIONS --erased-cubical --safe #-}

import Equality.Path as P

module H-level.Truncation.Propositional.Non-recursive.Erased
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

private
  open module PD = P.Derived-definitions-and-properties eq
    hiding (elim)

open import Logical-equivalence using (_⇔_)
open import Prelude hiding ([_,_])

open import Colimit.Sequential.Very-erased eq as C using (Colimitᴱ)
open import Equality.Decidable-UIP equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Equivalence.Erased.Cubical eq as EEq using (_≃ᴱ_)
open import Erased.Cubical eq
open import Function-universe equality-with-J as F hiding (_∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional.One-step eq as O
  using (∥_∥¹-out-^)

private
  variable
    a p   : Level
    A     : Type a
    P     : A → Type p
    e x z : A

------------------------------------------------------------------------
-- The type

-- The propositional truncation operator.

∥_∥ᴱ : Type a → Type a
∥ A ∥ᴱ = Colimitᴱ A (∥ A ∥¹-out-^ ∘ suc) O.∣_∣ O.∣_∣

-- The point constructor.

∣_∣ : A → ∥ A ∥ᴱ
∣_∣ = C.∣_∣₀

-- The eliminator.

record Elim {A : Type a} (P : ∥ A ∥ᴱ → Type p) : Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ                : ∀ x → P ∣ x ∣
    @0 is-propositionʳ : ∀ x → Is-proposition (P x)

open Elim public

elim : Elim P → (x : ∥ A ∥ᴱ) → P x
elim {A = A} {P = P} e = C.elim λ where
    .C.Elim.∣∣₀ʳ         → E.∣∣ʳ
    .C.Elim.∣∣₊ʳ {n = n} → helper n
    .C.Elim.∣∣₊≡∣∣₀ʳ x   →
      subst P (C.∣∣₊≡∣∣₀ x) (subst P (sym (C.∣∣₊≡∣∣₀ x)) (E.∣∣ʳ x))  ≡⟨ subst-subst-sym _ _ _ ⟩∎
      E.∣∣ʳ x                                                        ∎
    .C.Elim.∣∣₊≡∣∣₊ʳ {n = n} x →
      subst P (C.∣∣₊≡∣∣₊ x) (subst P (sym (C.∣∣₊≡∣∣₊ x)) (helper n x))  ≡⟨ subst-subst-sym _ _ _ ⟩∎
      helper n x                                                        ∎
  where
  module E = Elim e

  @0 helper : ∀ n (x : ∥ A ∥¹-out-^ (suc n)) → P C.∣ x ∣₊

  helper zero = O.elim e₀
    where
    e₀ : O.Elim _
    e₀ .O.Elim.∣∣ʳ x            = subst P (sym (C.∣∣₊≡∣∣₀ x)) (E.∣∣ʳ x)
    e₀ .O.Elim.∣∣-constantʳ _ _ = E.is-propositionʳ _ _ _

  helper (suc n) = O.elim e₊
    where
    e₊ : O.Elim _
    e₊ .O.Elim.∣∣ʳ x            = subst P (sym (C.∣∣₊≡∣∣₊ x))
                                    (helper n x)
    e₊ .O.Elim.∣∣-constantʳ _ _ = E.is-propositionʳ _ _ _

_ : elim e ∣ x ∣ ≡ e .∣∣ʳ x
_ = refl _

-- The propositional truncation operator returns propositions (in
-- erased contexts).

@0 ∥∥ᴱ-proposition : Is-proposition ∥ A ∥ᴱ
∥∥ᴱ-proposition {A = A} = elim lemma₅
  where
  lemma₀ : ∀ n (x : A) → C.∣ O.∣ x ∣-out-^ (1 + n) ∣₊ ≡ ∣ x ∣
  lemma₀ zero x =
    C.∣ O.∣ x ∣ ∣₊  ≡⟨ C.∣∣₊≡∣∣₀ x ⟩∎
    C.∣ x ∣₀        ∎
  lemma₀ (suc n) x =
    C.∣ O.∣ O.∣ x ∣-out-^ (1 + n) ∣ ∣₊  ≡⟨ C.∣∣₊≡∣∣₊ (O.∣ x ∣-out-^ (1 + n)) ⟩
    C.∣ O.∣ x ∣-out-^ (1 + n) ∣₊        ≡⟨ lemma₀ n x ⟩∎
    ∣ x ∣                               ∎

  lemma₁₀ : ∀ (x y : A) → ∣ x ∣ ≡ C.∣ y ∣₀
  lemma₁₀ x y =
    ∣ x ∣                         ≡⟨ sym (lemma₀ 0 x) ⟩
    C.∣ O.∣ x ∣-out-^ 1 ∣₊        ≡⟨⟩
    C.∣ O.∣ O.∣ x ∣-out-^ 0 ∣ ∣₊  ≡⟨ cong C.∣_∣₊ (O.∣∣-constant _ _) ⟩
    C.∣ O.∣ y ∣ ∣₊                ≡⟨ C.∣∣₊≡∣∣₀ y ⟩∎
    C.∣ y ∣₀                      ∎

  lemma₁₊ : ∀ n (x : A) (y : ∥ A ∥¹-out-^ (1 + n)) → ∣ x ∣ ≡ C.∣ y ∣₊
  lemma₁₊ n x y =
    ∣ x ∣                               ≡⟨ sym (lemma₀ (1 + n) x) ⟩
    C.∣ O.∣ x ∣-out-^ (2 + n) ∣₊        ≡⟨⟩
    C.∣ O.∣ O.∣ x ∣-out-^ (1 + n) ∣ ∣₊  ≡⟨ cong C.∣_∣₊ (O.∣∣-constant _ _) ⟩
    C.∣ O.∣ y ∣ ∣₊                      ≡⟨ C.∣∣₊≡∣∣₊ y ⟩∎
    C.∣ y ∣₊                            ∎

  lemma₂ :
    ∀ n (x y : ∥ A ∥¹-out-^ (1 + n))
    (p : x ≡ y) (q : O.∣ x ∣ ≡ O.∣ y ∣) →
    trans (C.∣∣₊≡∣∣₊ {P₊ = ∥ A ∥¹-out-^ ∘ suc} {step₀ = O.∣_∣} x)
      (cong C.∣_∣₊ p) ≡
    trans (cong C.∣_∣₊ q) (C.∣∣₊≡∣∣₊ y)
  lemma₂ n x y p q =
    trans (C.∣∣₊≡∣∣₊ x) (cong C.∣_∣₊ p)                        ≡⟨ PD.elim
                                                                    (λ {x y} p → trans (C.∣∣₊≡∣∣₊ x) (cong C.∣_∣₊ p) ≡
                                                                                trans (cong C.∣_∣₊ (cong O.∣_∣ p)) (C.∣∣₊≡∣∣₊ y))
                                                                    (λ x →
      trans (C.∣∣₊≡∣∣₊ x) (cong C.∣_∣₊ (refl _))                       ≡⟨ cong (trans _) $ cong-refl _ ⟩
      trans (C.∣∣₊≡∣∣₊ x) (refl _)                                     ≡⟨ trans-reflʳ _ ⟩
      C.∣∣₊≡∣∣₊ x                                                      ≡⟨ sym $ trans-reflˡ _ ⟩
      trans (refl _) (C.∣∣₊≡∣∣₊ x)                                     ≡⟨ cong (flip trans _) $ sym $
                                                                          trans (cong (cong C.∣_∣₊) $ cong-refl _) $
                                                                          cong-refl _ ⟩∎
      trans (cong C.∣_∣₊ (cong O.∣_∣ (refl _))) (C.∣∣₊≡∣∣₊ x)          ∎)
                                                                    p ⟩

    trans (cong C.∣_∣₊ (cong O.∣_∣ p)) (C.∣∣₊≡∣∣₊ y)           ≡⟨ cong (flip trans _) $
                                                                  cong-preserves-Constant
                                                                    (λ u v →
      C.∣ u ∣₊                                                          ≡⟨ sym (C.∣∣₊≡∣∣₊ u) ⟩
      C.∣ O.∣ u ∣ ∣₊                                                    ≡⟨ cong C.∣_∣₊ (O.∣∣-constant _ _) ⟩
      C.∣ O.∣ v ∣ ∣₊                                                    ≡⟨ C.∣∣₊≡∣∣₊ v ⟩∎
      C.∣ v ∣₊                                                          ∎)
                                                                    _ _ ⟩∎
    trans (cong C.∣_∣₊ q) (C.∣∣₊≡∣∣₊ y)                        ∎

  lemma₃ :
    ∀ n x y (p : C.∣ O.∣ y ∣ ∣₊ ≡ z) →
    subst (∣ x ∣ ≡_) p (lemma₁₊ n x O.∣ y ∣) ≡
    trans (sym (lemma₀ n x))
      (trans (cong C.∣_∣₊ (O.∣∣-constant _ _)) p)
  lemma₃ n x y p =
    subst (∣ x ∣ ≡_) p (lemma₁₊ n x O.∣ y ∣)                      ≡⟨ sym trans-subst ⟩

    trans (lemma₁₊ n x O.∣ y ∣) p                                 ≡⟨⟩

    trans (trans (sym (trans (C.∣∣₊≡∣∣₊ (O.∣ x ∣-out-^ (1 + n)))
                         (lemma₀ n x)))
             (trans (cong C.∣_∣₊
                       (O.∣∣-constant
                          (O.∣ x ∣-out-^ (1 + n)) O.∣ y ∣))
                (C.∣∣₊≡∣∣₊ O.∣ y ∣)))
      p                                                           ≡⟨ trans (cong (λ eq →
                                                                                trans (trans eq
                                                                                (trans (cong C.∣_∣₊ (O.∣∣-constant _ _))
                                                                                (C.∣∣₊≡∣∣₊ _)))
                                                                                p) $
                                                                            sym-trans _ _) $
                                                                     trans (trans-assoc _ _ _) $
                                                                     trans (trans-assoc _ _ _) $
                                                                     cong (trans (sym (lemma₀ n _))) $
                                                                     sym $ trans-assoc _ _ _ ⟩
    trans (sym (lemma₀ n x))
      (trans (trans (sym (C.∣∣₊≡∣∣₊ (O.∣ x ∣-out-^ (1 + n))))
                (trans (cong C.∣_∣₊
                          (O.∣∣-constant
                             (O.∣ x ∣-out-^ (1 + n)) O.∣ y ∣))
                   (C.∣∣₊≡∣∣₊ O.∣ y ∣)))
         p)                                                       ≡⟨ cong (λ eq → trans (sym (lemma₀ n _))
                                                                                (trans (trans (sym (C.∣∣₊≡∣∣₊ _)) eq) p)) $ sym $
                                                                     lemma₂ _ _ _ _ _ ⟩
    trans (sym (lemma₀ n x))
      (trans (trans (sym (C.∣∣₊≡∣∣₊ (O.∣ x ∣-out-^ (1 + n))))
                (trans (C.∣∣₊≡∣∣₊ (O.∣ x ∣-out-^ (1 + n)))
                   (cong C.∣_∣₊ (O.∣∣-constant _ _))))
         p)                                                       ≡⟨ cong (λ eq → trans (sym (lemma₀ n _)) (trans eq p)) $
                                                                     trans-sym-[trans] _ _ ⟩∎
    trans (sym (lemma₀ n x))
      (trans (cong C.∣_∣₊ (O.∣∣-constant _ _)) p)                 ∎

  lemma₄ : ∀ _ → C.Elim _
  lemma₄ x .C.Elim.∣∣₀ʳ       = lemma₁₀ x
  lemma₄ x .C.Elim.∣∣₊ʳ       = lemma₁₊ _ x
  lemma₄ x .C.Elim.∣∣₊≡∣∣₀ʳ y =
    subst (∣ x ∣ ≡_) (C.∣∣₊≡∣∣₀ y) (lemma₁₊ 0 x O.∣ y ∣)       ≡⟨ lemma₃ _ _ _ _ ⟩

    trans (sym (lemma₀ 0 x))
      (trans (cong C.∣_∣₊ (O.∣∣-constant _ _)) (C.∣∣₊≡∣∣₀ y))  ≡⟨⟩

    lemma₁₀ x y                                                ∎
  lemma₄ x .C.Elim.∣∣₊≡∣∣₊ʳ {n = n} y =
    subst (∣ x ∣ ≡_) (C.∣∣₊≡∣∣₊ y) (lemma₁₊ (1 + n) x O.∣ y ∣)  ≡⟨ lemma₃ _ _ _ _ ⟩

    trans (sym (lemma₀ (1 + n) x))
      (trans (cong C.∣_∣₊ (O.∣∣-constant _ _)) (C.∣∣₊≡∣∣₊ y))   ≡⟨⟩

    lemma₁₊ n x y                                               ∎

  lemma₅ : Elim _
  lemma₅ .is-propositionʳ = Π≡-proposition ext
  lemma₅ .∣∣ʳ x           = C.elim (lemma₄ x)

------------------------------------------------------------------------
-- A lemma

-- A function of type (x : ∥ A ∥ᴱ) → P x, along with an erased proof
-- showing that the function is equal to some erased function, is
-- equivalent to a function of type (x : A) → P ∣ x ∣, along with an
-- erased equality proof.

Σ-Π-∥∥ᴱ-Erased-≡-≃ :
  {@0 g : (x : ∥ A ∥ᴱ) → P x} →
  (∃ λ (f : (x : ∥ A ∥ᴱ) → P x) → Erased (f ≡ g)) ≃
  (∃ λ (f : (x : A) → P ∣ x ∣) → Erased (f ≡ g ∘ ∣_∣))
Σ-Π-∥∥ᴱ-Erased-≡-≃ {A = A} {P = P} {g = g} =
  (∃ λ (f : (x : ∥ A ∥ᴱ) → P x) → Erased (f ≡ g))                         ↝⟨ (inverse $
                                                                              Σ-cong (inverse C.universal-property-Π) λ _ → F.id) ⟩
  (∃ λ (f :
        ∃ λ (f₀ : (x : A) → P ∣ x ∣) →
        Erased (
        ∃ λ (f₊ : ∀ n (x : ∥ A ∥¹-out-^ (suc n)) → P C.∣ x ∣₊) →
        (∀ x → subst P (C.∣∣₊≡∣∣₀ x) (f₊ zero O.∣ x ∣) ≡ f₀ x) ×
        (∀ n x → subst P (C.∣∣₊≡∣∣₊ x) (f₊ (suc n) O.∣ x ∣) ≡
                         f₊ n x))) →
   Erased (u⁻¹ f ≡ g))                                                    ↔⟨ inverse $
                                                                             Σ-assoc F.∘
                                                                             (∃-cong λ _ →
                                                                              Erased-Σ↔Σ F.∘
                                                                              (from-equivalence $ Erased-cong (∃-cong λ _ →
                                                                               Eq.extensionality-isomorphism bad-ext))) ⟩
  (∃ λ (f : (x : A) → P ∣ x ∣) →
   Erased (
   ∃ λ (e :
        ∃ λ (f₊ : ∀ n (x : ∥ A ∥¹-out-^ (suc n)) → P C.∣ x ∣₊) →
        (∀ x → subst P (C.∣∣₊≡∣∣₀ x) (f₊ zero O.∣ x ∣) ≡ f x) ×
        (∀ n x → subst P (C.∣∣₊≡∣∣₊ x) (f₊ (suc n) O.∣ x ∣) ≡ f₊ n x)) →
   ∀ x → u⁻¹ (f , [ e ]) x ≡ g x))                                        ↝⟨ (∃-cong λ _ → Erased-cong (∃-cong λ _ →
                                                                              (∃-cong λ _ → from-bijection $ erased Erased↔) F.∘
                                                                              C.universal-property-Π)) ⟩
  (∃ λ (f : (x : A) → P ∣ x ∣) →
   Erased (
   ∃ λ ((f₊ , eq₀ , eq₊) :
        ∃ λ (f₊ : ∀ n (x : ∥ A ∥¹-out-^ (suc n)) → P C.∣ x ∣₊) →
        (∀ x → subst P (C.∣∣₊≡∣∣₀ x) (f₊ zero O.∣ x ∣) ≡ f x) ×
        (∀ n x → subst P (C.∣∣₊≡∣∣₊ x) (f₊ (suc n) O.∣ x ∣) ≡ f₊ n x)) →
   ∃ λ (f≡g₀ : (x : A) → f x ≡ g ∣ x ∣) →
   ∃ λ (f≡g₊ : ∀ n (x : ∥ A ∥¹-out-^ (suc n)) → f₊ n x ≡ g C.∣ x ∣₊) →
   (∀ x → subst (λ x → u⁻¹ (f , [ f₊ , eq₀ , eq₊ ]) x ≡ g x)
            (C.∣∣₊≡∣∣₀ x) (f≡g₊ zero O.∣ x ∣) ≡
          f≡g₀ x) ×
   (∀ n (x : ∥ A ∥¹-out-^ (suc n)) →
    subst (λ x → u⁻¹ (f , [ f₊ , eq₀ , eq₊ ]) x ≡ g x)
      (C.∣∣₊≡∣∣₊ x) (f≡g₊ (suc n) O.∣ x ∣) ≡
    f≡g₊ n x)))                                                           ↔⟨ (∃-cong λ _ → Erased-cong (
                                                                              (∃-cong λ _ →
                                                                               (∃-cong λ _ →
                                                                                inverse Σ-assoc) F.∘
                                                                               Σ-assoc F.∘
                                                                               (∃-cong λ _ →
                                                                                (inverse $
                                                                                Σ-cong (inverse $
                                                                                Eq.extensionality-isomorphism bad-ext F.∘
                                                                                (∀-cong ext λ _ →
                                                                                Eq.extensionality-isomorphism bad-ext)) λ _ →
                                                                                F.id) F.∘
                                                                                ∃-comm) F.∘
                                                                               inverse Σ-assoc) F.∘
                                                                              ∃-comm)) ⟩
  (∃ λ (f : (x : A) → P ∣ x ∣) →
   Erased (
   ∃ λ (f≡g₀ : (x : A) → f x ≡ g ∣ x ∣) →
   ∃ λ ((f₊ , f≡g₊) :
        ∃ λ (f₊ : ∀ n (x : ∥ A ∥¹-out-^ (suc n)) → P C.∣ x ∣₊) →
        f₊ ≡ λ _ x → g C.∣ x ∣₊) →
   ∃ λ (eq₀ : ∀ x → subst P (C.∣∣₊≡∣∣₀ x) (f₊ zero O.∣ x ∣) ≡ f x) →
   ∃ λ (eq₊ : ∀ n x →
              subst P (C.∣∣₊≡∣∣₊ x) (f₊ (suc n) O.∣ x ∣) ≡ f₊ n x) →
   (∀ x → subst (λ x → u⁻¹ (f , [ f₊ , eq₀ , eq₊ ]) x ≡ g x)
            (C.∣∣₊≡∣∣₀ x) (cong (_$ O.∣ x ∣) (cong (_$ zero) f≡g₊)) ≡
          f≡g₀ x) ×
   (∀ n (x : ∥ A ∥¹-out-^ (suc n)) →
    subst (λ x → u⁻¹ (f , [ f₊ , eq₀ , eq₊ ]) x ≡ g x)
      (C.∣∣₊≡∣∣₊ x) (cong (_$ O.∣ x ∣) (cong (_$ suc n) f≡g₊)) ≡
    cong (_$ x) (cong (_$ n) f≡g₊))))                                     ↔⟨ (∃-cong λ _ → Erased-cong (∃-cong λ _ →
                                                                              (∃-cong λ _ → ∃-cong λ _ →
                                                                               (∀-cong ext λ _ → ≡⇒↝ _ $ cong (_≡ _) $
                                                                                cong (subst (λ x → u⁻¹ _ x ≡ g x) _) $
                                                                                trans (cong (cong (_$ _)) $ cong-refl _) $
                                                                                cong-refl _)
                                                                                ×-cong
                                                                               (∀-cong ext λ _ → ∀-cong ext λ _ → ≡⇒↝ _ $ cong₂ _≡_
                                                                                (cong (subst (λ x → u⁻¹ _ x ≡ g x) _) $
                                                                                trans (cong (cong (_$ _)) $ cong-refl _) $
                                                                                cong-refl _)
                                                                                (trans (cong (cong (_$ _)) $ cong-refl _) $
                                                                                cong-refl _))) F.∘
                                                                              (drop-⊤-left-Σ $
                                                                               _⇔_.to contractible⇔↔⊤ $
                                                                               singleton-contractible _))) ⟩
  (∃ λ (f : (x : A) → P ∣ x ∣) →
   Erased (
   ∃ λ (f≡g₀ : (x : A) → f x ≡ g ∣ x ∣) →
   ∃ λ (eq₀ : ∀ x → subst P (C.∣∣₊≡∣∣₀ x) (g C.∣ O.∣ x ∣ ∣₊) ≡ f x) →
   ∃ λ (eq₊ : ∀ n x →
              subst P (C.∣∣₊≡∣∣₊ x) (g C.∣ O.∣ x ∣ ∣₊) ≡ g C.∣ x ∣₊) →
   (∀ x → subst
            (λ x → u⁻¹ (f , [ (λ _ → g ∘ C.∣_∣₊) , eq₀ , eq₊ ]) x ≡ g x)
            (C.∣∣₊≡∣∣₀ x) (refl _) ≡
          f≡g₀ x) ×
   (∀ n (x : ∥ A ∥¹-out-^ (suc n)) →
    subst (λ x → u⁻¹ (f , [ (λ _ → g ∘ C.∣_∣₊) , eq₀ , eq₊ ]) x ≡ g x)
      (C.∣∣₊≡∣∣₊ x) (refl _) ≡
    refl _)))                                                             ↝⟨ (∃-cong λ _ → Erased-cong (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                              (∀-cong ext λ _ → ≡⇒↝ _ $ cong (_≡ _) $
                                                                               lemma₀ _ _ _ _)
                                                                                ×-cong
                                                                              (∀-cong ext λ _ → ∀-cong ext λ _ → ≡⇒↝ _ $ cong (_≡ refl _) $
                                                                               lemma₊ _ _ _ _ _))) ⟩
  (∃ λ (f : (x : A) → P ∣ x ∣) →
   Erased (
   ∃ λ (f≡g₀ : (x : A) → f x ≡ g ∣ x ∣) →
   ∃ λ (eq₀ : ∀ x → subst P (C.∣∣₊≡∣∣₀ x) (g C.∣ O.∣ x ∣ ∣₊) ≡ f x) →
   ∃ λ (eq₊ : ∀ n x →
              subst P (C.∣∣₊≡∣∣₊ x) (g C.∣ O.∣ x ∣ ∣₊) ≡ g C.∣ x ∣₊) →
   (∀ x → trans (sym (eq₀ x)) (dcong g (C.∣∣₊≡∣∣₀ x)) ≡ f≡g₀ x) ×
   (∀ n (x : ∥ A ∥¹-out-^ (suc n)) →
    trans (sym (eq₊ n x)) (dcong g (C.∣∣₊≡∣∣₊ x)) ≡ refl _)))             ↝⟨ (∃-cong λ _ → Erased-cong (∃-cong λ _ → ∃-cong λ eq₀ → ∃-cong λ eq₊ →
                                                                              (Eq.extensionality-isomorphism bad-ext F.∘
                                                                               (∀-cong ext λ _ →
                                                                                Eq.≃-≡ (Eq.↔⇒≃ ≡-comm) F.∘
                                                                                (≡⇒↝ _ $
                                                                                trans ([trans≡]≡[≡trans-symʳ] _ _ _) $
                                                                                cong (sym (eq₀ _) ≡_) $ sym $ sym-sym _)))
                                                                                ×-cong
                                                                              (Eq.extensionality-isomorphism bad-ext F.∘
                                                                               (∀-cong ext λ _ →
                                                                                Eq.extensionality-isomorphism bad-ext F.∘
                                                                                (∀-cong ext λ _ →
                                                                                Eq.≃-≡ (Eq.↔⇒≃ ≡-comm) F.∘
                                                                                (≡⇒↝ _ $
                                                                                trans ([trans≡]≡[≡trans-symʳ] _ _ _) $
                                                                                cong (sym (eq₊ _ _) ≡_) $ sym $ sym-sym _)))))) ⟩
  (∃ λ (f : (x : A) → P ∣ x ∣) →
   Erased (
   ∃ λ (f≡g₀ : (x : A) → f x ≡ g ∣ x ∣) →
   ∃ λ (eq₀ : ∀ x → subst P (C.∣∣₊≡∣∣₀ x) (g C.∣ O.∣ x ∣ ∣₊) ≡ f x) →
   ∃ λ (eq₊ : ∀ n x →
              subst P (C.∣∣₊≡∣∣₊ x) (g C.∣ O.∣ x ∣ ∣₊) ≡ g C.∣ x ∣₊) →
   eq₀ ≡ (λ x → sym (trans (f≡g₀ x) (sym (dcong g (C.∣∣₊≡∣∣₀ x))))) ×
   eq₊ ≡ (λ _ x → sym (trans (refl _) (sym (dcong g (C.∣∣₊≡∣∣₊ x)))))))   ↔⟨ (∃-cong λ _ → Erased-cong (∃-cong λ _ → ∃-cong λ _ →
                                                                              (drop-⊤-right λ _ →
                                                                               _⇔_.to contractible⇔↔⊤ $
                                                                               singleton-contractible _) F.∘
                                                                              ∃-comm)) ⟩
  (∃ λ (f : (x : A) → P ∣ x ∣) →
   Erased (
   ∃ λ (f≡g₀ : (x : A) → f x ≡ g ∣ x ∣) →
   ∃ λ (eq₀ : ∀ x → subst P (C.∣∣₊≡∣∣₀ x) (g C.∣ O.∣ x ∣ ∣₊) ≡ f x) →
   eq₀ ≡ (λ x → sym (trans (f≡g₀ x) (sym (dcong g (C.∣∣₊≡∣∣₀ x)))))))     ↔⟨ (∃-cong λ _ → Erased-cong (
                                                                              drop-⊤-right λ _ →
                                                                              _⇔_.to contractible⇔↔⊤ $
                                                                              singleton-contractible _)) ⟩

  (∃ λ (f : (x : A) → P ∣ x ∣) → Erased ((x : A) → f x ≡ g ∣ x ∣))        ↝⟨ (∃-cong λ _ → Erased-cong (
                                                                              Eq.extensionality-isomorphism bad-ext)) ⟩□
  (∃ λ (f : (x : A) → P ∣ x ∣) → Erased (f ≡ g ∘ ∣_∣))                    □
  where
  u⁻¹ = _≃_.from C.universal-property-Π

  @0 lemma₀ : ∀ _ _ _ _ → _
  lemma₀ f eq₀ eq₊ x =
    subst (λ x → u⁻¹ (f , [ (λ _ → g ∘ C.∣_∣₊) , eq₀ , eq₊ ]) x ≡ g x)
      (C.∣∣₊≡∣∣₀ x) (refl _)                                            ≡⟨ subst-in-terms-of-trans-and-dcong ⟩

    trans (sym (dcong (u⁻¹ (f , [ (λ _ → g ∘ C.∣_∣₊) , eq₀ , eq₊ ]))
                  (C.∣∣₊≡∣∣₀ x)))
      (trans (cong (subst P (C.∣∣₊≡∣∣₀ x)) (refl _))
         (dcong g (C.∣∣₊≡∣∣₀ x)))                                       ≡⟨ cong₂ (trans ∘ sym)
                                                                             C.elim-∣∣₊≡∣∣₀
                                                                             (trans (cong (flip trans _) $
                                                                                cong-refl _) $
                                                                              trans-reflˡ _) ⟩∎
    trans (sym (eq₀ x)) (dcong g (C.∣∣₊≡∣∣₀ x))                         ∎

  @0 lemma₊ : ∀ _ _ _ _ _ → _
  lemma₊ f eq₀ eq₊ n x =
    subst (λ x → u⁻¹ (f , [ (λ _ → g ∘ C.∣_∣₊) , eq₀ , eq₊ ]) x ≡ g x)
      (C.∣∣₊≡∣∣₊ x) (refl _)                                            ≡⟨ subst-in-terms-of-trans-and-dcong ⟩

    trans (sym (dcong (u⁻¹ (f , [ (λ _ → g ∘ C.∣_∣₊) , eq₀ , eq₊ ]))
                  (C.∣∣₊≡∣∣₊ x)))
      (trans (cong (subst P (C.∣∣₊≡∣∣₊ x)) (refl _))
         (dcong g (C.∣∣₊≡∣∣₊ x)))                                       ≡⟨ cong₂ (trans ∘ sym)
                                                                             C.elim-∣∣₊≡∣∣₊
                                                                             (trans (cong (flip trans _) $
                                                                                cong-refl _) $
                                                                              trans-reflˡ _) ⟩∎
    trans (sym (eq₊ n x)) (dcong g (C.∣∣₊≡∣∣₊ x))                       ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality