text:
module Pat (BaseType : Set) where

data Ty : Set where
  ι   : BaseType -> Ty
  _⟶_ : Ty -> Ty -> Ty

data Bwd (A : Set) : Set where
  •   : Bwd A
  _◄_ : Bwd A -> A -> Bwd A

infixl 30 _◄_

Ctx = Bwd Ty

data Take {A : Set} : Bwd A -> A -> Bwd A -> Set where
  hd : forall {x xs} -> Take (xs ◄ x) x xs
  tl : forall {x y xs ys} -> Take xs x ys -> Take (xs ◄ y) x (ys ◄ y)

data Pat : Ctx -> Ctx -> Ty -> Ctx -> Set

data Pats : Ctx -> Ty -> Ctx -> Ty -> Set where
  ε : forall {Θ τ} -> Pats Θ τ Θ τ
  _,_ : forall {Θ₁ Θ₂ Θ₃ ρ σ τ} ->
        Pat • Θ₁ ρ Θ₂ -> Pats Θ₂ σ Θ₃ τ ->
        Pats Θ₁ (ρ ⟶ σ) Θ₃ τ

data Pat where
  ƛ    : forall {Δ Θ Θ' σ τ} -> Pat (Δ ◄ σ) Θ τ Θ' ->
         Pat Δ Θ (σ ⟶ τ) Θ'
  _[_] : forall {Θ Θ' Δ σ τ} ->
         Take Θ σ Θ' -> Pats Δ σ • τ -> Pat Δ Θ τ Θ'

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2012-03-08
module NoNoTerminationCheck where

{-# NON_TERMINATING #-}
f : Set
f = f

-- the pragma should not extend to the following definition

g : Set
g = g

-- error: non-termination

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Common.Prelude
open import Common.Reflection
open import Common.Equality

data Dec {a} (A : Set a) : Set a where
  yes : A → Dec A
  no  : Dec A

record Eq {a} (A : Set a) : Set a where
  constructor eqDict
  field
    _==_ : (x y : A) → Dec (x ≡ y)

module M {a} {A : Set a} {{EqA : Eq A}} where
  _==_ : (x y : A) → Dec (x ≡ y)
  _==_ = Eq._==_ EqA

open Eq {{...}}

private
  eqNat : (x y : Nat) → Dec (x ≡ y)
  eqNat zero zero = yes refl
  eqNat zero (suc y) = no
  eqNat (suc x) zero = no
  eqNat (suc x) (suc y) with eqNat x y
  eqNat (suc x) (suc .x) | yes refl = yes refl
  ... | no     = no

  eqBool : (x y : Bool) → Dec (x ≡ y)
  eqBool true true = yes refl
  eqBool true false = no
  eqBool false true = no
  eqBool false false = yes refl

unquoteDecl EqNat = define (iArg EqNat)
  (funDef (def (quote Eq) (vArg (def (quote Nat) []) ∷ []))
          (clause [] (con (quote eqDict) (vArg (def (quote eqNat) []) ∷ [])) ∷ []))

instance
  EqBool : Eq Bool
  unquoteDef EqBool =
    defineFun EqBool (clause [] (con (quote eqDict) (vArg (def (quote eqBool) []) ∷ [])) ∷ [])

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

tm : QName → Term
tm eq = def (quote id) (vArg (def eq (vArg (lit (nat 0)) ∷ vArg (lit (nat 1)) ∷ [])) ∷ [])

tm₂ : QName → Term
tm₂ eq = def eq (iArg (def (quote EqNat) []) ∷ vArg (lit (nat 0)) ∷ vArg (lit (nat 1)) ∷ [])

_==′_ : ∀ {a} {A : Set a} {{EqA : Eq A}} (x y : A) → Dec (x ≡ y)
_==′_ = _==_

ok₁ : Dec (0 ≡ 1)
ok₁ = unquote (give (tm (quote _==′_)))

ok₂ : Dec (0 ≡ 1)
ok₂ = unquote (give (tm₂ (quote _==_)))

ok₃ : Dec (0 ≡ 1)
ok₃ = unquote (give (tm (quote M._==_)))

ok₄ : Dec (true ≡ false)
ok₄ = true == false

ok₅ : Dec (2 ≡ 2)
ok₅ = 2 == 2

-- Was bad.
bad : Dec (0 ≡ 1)
bad = unquote (give (tm (quote _==_)))

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
{-# OPTIONS --without-K #-}
module well-typed-syntax-eq-dec where
open import well-typed-syntax
open import common

context-pick-if : ∀ {ℓ} {P : Context → Set ℓ}
                        {Γ : Context}
                        (dummy : P (ε ▻ ‘Σ’ ‘Context’ ‘Typ’))
                        (val : P Γ) →
                      P (ε ▻ ‘Σ’ ‘Context’ ‘Typ’)
context-pick-if {P = P} {ε ▻ ‘Σ’ ‘Context’ ‘Typ’} dummy val = val
context-pick-if {P = P} {Γ} dummy val = dummy

context-pick-if-refl : ∀ {ℓ P dummy val} →
                           context-pick-if {ℓ} {P} {ε ▻ ‘Σ’ ‘Context’ ‘Typ’} dummy val ≡ val
context-pick-if-refl {P = P} = refl

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
module Test.NFTest where

open import Data.Nat
open import Data.List
open import Data.Product
open import Test.Factorial
open import NF
open import NF.Nat
open import NF.List
open import NF.Product

l : List (ℕ × ℕ)
l = nf ((1 , factorial 1) ∷ (1 + 1 , factorial (1 + 1)) ∷ [] ++
        (5 , factorial 5) ∷ [])

max_stars_repo_name: yanok/normalize-via-instances

max_issues_repo_name: yanok/normalize-via-instances

max_forks_repo_name: yanok/normalize-via-instances


text:
module Naturals where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

-- suc (suc (suc (suc (suc (suc (suc zero))))))

{-# BUILTIN NATURAL ℕ #-}

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

_+_ : ℕ → ℕ → ℕ
zero + n  = n           -- 0 + n       ≡ n
suc m + n = suc (m + n) -- (1 + m) + n ≡ 1 + (m + n)

_ : 1 + 1 ≡ 2
_ = refl

_ : 3 + 4 ≡ 7
_ =
  begin
    3 + 4
  ≡⟨⟩
    suc 1 + 4
  ∎

max_stars_repo_name: xiongxin/playground

max_issues_repo_name: xiongxin/playground

max_forks_repo_name: xiongxin/playground


text:
------------------------------------------------------------------------------
-- Filter
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.List.Filter where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.PropertiesI
open import FOTC.Base.List
open import FOTC.Data.Bool.Type
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.Type
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI

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

postulate
  filter    : D → D → D
  filter-[] : ∀ p → filter p [] ≡ []
  filter-∷  : ∀ p x xs → filter p (x ∷ xs) ≡
              (if p · x then x ∷ filter p xs else filter p xs)

postulate filter-List : ∀ p {xs} → List xs → List (filter p xs)

from-Bool : ∀ {b} → Bool b → b ≡ true ∨ b ≡ false
from-Bool btrue  = inj₁ refl
from-Bool bfalse = inj₂ refl

-- lenght-filter : ∀ p {xs} → (∀ x → Bool (p · x)) → List xs →
--                 length (filter p xs) ≤ length xs
-- lenght-filter p hp lnil =
--   le (length (filter p [])) (length [])
--     ≡⟨ ltLeftCong (lengthCong (filter-[] p)) ⟩
--   le (length []) (length [])
--     ≡⟨ ltCong length-[] (succCong length-[]) ⟩
--   le zero zero
--     ≡⟨ x≤x nzero ⟩
--   true ∎

-- lenght-filter p hp (lcons x {xs} Lxs) = case prf₁ prf₂ (from-Bool (hp x))
--   where
--   prf₁ : p · x ≡ true →
--          le (length (filter p (x ∷ xs))) (length (x ∷ xs)) ≡ true
--   prf₁ h = {!!}

--   prf₂ : p · x ≡ false →
--          le (length (filter p (x ∷ xs))) (length (x ∷ xs)) ≡ true
--   prf₂ h =
--     le (length (filter p (x ∷ xs))) (length (x ∷ xs))
--       ≡⟨ ltLeftCong (lengthCong {!!}) ⟩
--     le (length (filter p xs)) (length (x ∷ xs))
--       ≡⟨ ≤-trans (lengthList-N (filter-List p Lxs))
--                  (lengthList-N Lxs)
--                  (lengthList-N (lcons x Lxs))
--                  (lenght-filter p hp Lxs)
--                  (x<y→x≤y (lengthList-N Lxs) (lengthList-N (lcons x Lxs))
--                           (lg-x<lg-x∷xs x Lxs)) ⟩
--     true ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Oscar.Prelude
open import Oscar.Class

module Oscar.Class.Symmetry where

module Symmetry'
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  x y
  = ℭLASS (x ,, y ,, _∼_) (x ∼ y → y ∼ x)

module Symmetry
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  where
  class = ∀ {x y} → Symmetry'.class _∼_ x y
  type = ∀ {x y} → Symmetry'.type _∼_ x y
  method : ⦃ _ : class ⦄ → type
  method {x = x} {y} = Symmetry'.method _∼_ x y

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
  where
  symmetry = Symmetry.method _∼_
  syntax symmetry {x} {y} x∼y = x ⟨∼ x∼y ∼⟩ y

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  ⦃ _ : Symmetry.class _∼_ ⦄
  where
  symmetry[_] = λ {x y} (x∼y : x ∼ y) → Symmetry.method _∼_ x∼y


text:
module UniDB.Subst.Shifts where

open import UniDB.Subst.Core
open import UniDB.Morph.Shifts

module _ {T : STX} {{vrT : Vr T}} {{apTT : Ap T T}} {{apVrT : ApVr T}} where

  instance
    iLkCompApShifts : LkCompAp T Shifts
    lk-⊙-ap {{iLkCompApShifts}} ξ₁ ξ₂ i = begin
      vr (lk (ξ₁ ⊙ ξ₂) i)     ≡⟨ cong vr (shiftIx-⊙ ξ₁ ξ₂ i) ⟩
      vr (lk ξ₂ (lk ξ₁ i))     ≡⟨ sym (ap-vr {T} ξ₂ (lk ξ₁ i)) ⟩
      ap {T} ξ₂ (vr (lk ξ₁ i)) ∎

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


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

module Categories.Functor.Profunctor where

open import Level

open import Data.Product
open import Relation.Binary.Bundles
open import Categories.Category
open import Categories.Category.Instance.Setoids
open import Categories.Functor hiding (id)
open import Categories.Functor.Bifunctor
open import Categories.Functor.Hom
open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.Equivalence
open import Function.Equality using (Π; _⟨$⟩_; cong)

Profunctor : ∀ {o ℓ e} {o′ ℓ′ e′} → Category o ℓ e → Category o′ ℓ′ e′ → Set _
Profunctor {ℓ = ℓ} {e} {ℓ′ = ℓ′} {e′} C D = Bifunctor (Category.op D) C (Setoids (ℓ ⊔ ℓ′) (e ⊔ e′))

-- Calling the profunctor identity "id" is a bad idea
proid : ∀ {o ℓ e} → {C : Category o ℓ e} → Profunctor C C
proid {C = C} = Hom[ C ][-,-]

module Profunctor {o ℓ e} {o′} (C : Category o ℓ e) (D : Category o′ ℓ e) where
  module C = Category C
  open module D = Category D hiding (id)
  open D.HomReasoning
  open import Categories.Morphism.Reasoning D using (assoc²''; elimˡ; elimʳ)

  -- representable profunctors
  -- hom(f,1)
  repˡ : ∀ (F : Functor C D) → Profunctor D C
  repˡ F = record
    { F₀ = λ (c , d) → record
      { Carrier = D [ F₀ c , d ]
      ; _≈_ = D._≈_
      ; isEquivalence = D.equiv
      }
    ; F₁ = λ (f , g) → record
      { _⟨$⟩_ = λ x → g ∘ x ∘ F₁ f
      ; cong  = λ x → begin _ ≈⟨ refl⟩∘⟨ x ⟩∘⟨refl ⟩ _ ∎
      }
    ; identity = λ {x} {y} {y'} y≈y' → begin
        D.id ∘ y ∘ F₁ C.id ≈⟨ D.identityˡ ⟩
        y ∘ F₁ C.id        ≈⟨ elimʳ identity ⟩
        y                  ≈⟨ y≈y' ⟩
        y'                 ∎
    ; homomorphism = λ { {f = f0 , f1} {g = g0 , g1} {x} {y} x≈y → begin
        (g1 ∘ f1) ∘ x ∘ F₁ (f0 C.∘ g0)  ≈⟨ refl⟩∘⟨ x≈y ⟩∘⟨ F.homomorphism ⟩
        (g1 ∘ f1) ∘ y ∘ F₁ f0 ∘ F₁ g0   ≈⟨ refl⟩∘⟨ D.sym-assoc ⟩
        (g1 ∘ f1) ∘ (y ∘ F₁ f0) ∘ F₁ g0 ≈⟨ Equiv.sym assoc²'' ⟩
        g1 ∘ (f1 ∘ y ∘ F₁ f0) ∘ F₁ g0   ∎
      }
    ; F-resp-≈ = λ { {f = f0 , f1} {g = g0 , g1} (f0≈g0 , f1≈g1) {x} {y} x≈y → begin
        f1 ∘ x ∘ F₁ f0 ≈⟨ f1≈g1 ⟩∘⟨ x≈y ⟩∘⟨ F-resp-≈ f0≈g0 ⟩
        g1 ∘ y ∘ F₁ g0 ∎
      }
    }
    where
      open module F = Functor F

  -- hom(1,f)
  repʳ : (F : Functor C D) → Profunctor C D
  repʳ F = record
    { F₀ = λ (c , d) → record
      { Carrier = D [ c , F₀ d ]
      ; _≈_ = D._≈_
      ; isEquivalence = D.equiv
      }
    ; F₁ = λ (f , g) → record
      { _⟨$⟩_ = λ x → F₁ g ∘ x ∘ f
      ; cong  = λ x → begin _ ≈⟨ refl⟩∘⟨ x ⟩∘⟨refl ⟩ _ ∎
      }
    ; identity = λ {x} {y} {y'} y≈y' → begin
        F₁ C.id ∘ y ∘ D.id ≈⟨ elimˡ identity ⟩
        y ∘ D.id           ≈⟨ D.identityʳ ⟩
        y                  ≈⟨ y≈y' ⟩
        y'                 ∎
    ; homomorphism = λ { {f = f0 , f1} {g = g0 , g1} {x} {y} x≈y → begin
        F₁ (g1 C.∘ f1) ∘ x ∘ f0 ∘ g0    ≈⟨ F.homomorphism ⟩∘⟨ x≈y ⟩∘⟨refl ⟩
        (F₁ g1 ∘ F₁ f1) ∘ y ∘ f0 ∘ g0   ≈⟨ refl⟩∘⟨ D.sym-assoc ⟩
        (F₁ g1 ∘ F₁ f1) ∘ (y ∘ f0) ∘ g0 ≈⟨ Equiv.sym assoc²'' ⟩
        F₁ g1 ∘ (F₁ f1 ∘ y ∘ f0) ∘ g0   ∎
      }
    ; F-resp-≈ = λ { {f = f0 , f1} {g = g0 , g1} (f0≈g0 , f1≈g1) {x} {y} x≈y → begin
        F₁ f1 ∘ x ∘ f0 ≈⟨ F-resp-≈ f1≈g1 ⟩∘⟨ x≈y ⟩∘⟨ f0≈g0 ⟩
        F₁ g1 ∘ y ∘ g0 ∎
      }
    }
    where
      open module F = Functor F

-- each Prof(C,D) is a category
homProf : {o o′ ℓ e : Level} → (C : Category o ℓ e) → (D : Category o′ ℓ e) → Category _ _ _
homProf C D = record
  { Obj = Profunctor C D
  ; _⇒_ = NaturalTransformation
  ; _≈_ = _≃_
  ; id = id
  ; _∘_ = _∘ᵥ_
  ; assoc     = λ { {f = f} {g} {h} → assoc-lemma {f = f} {g} {h}}
  ; sym-assoc = λ { {f = f} {g} {h} → sym-assoc-lemma {f = f} {g} {h}}
  ; identityˡ = λ { {f = f} → id-lemmaˡ {f = f} }
  ; identityʳ = λ { {f = f} → id-lemmaʳ {f = f} }
  ; identity² = λ z → z
  ; equiv = ≃-isEquivalence
  ; ∘-resp-≈ = λ { {f = f} {h} {g} {i} eq eq' → ∘ᵥ-resp-≃ {f = f} {h} {g} {i} eq eq' }
  }
  where
    id-lemmaˡ : ∀ {o o′ ℓ ℓ′ e e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {P K : Functor C D}
            {f : NaturalTransformation P K} → id ∘ᵥ f ≃ f
    id-lemmaˡ {D = D} = Category.identityˡ D

    id-lemmaʳ : ∀ {o o′ ℓ ℓ′ e e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {P K : Functor C D}
            {f : NaturalTransformation P K} → f ∘ᵥ id ≃ f
    id-lemmaʳ {D = D} = Category.identityʳ D

    assoc-lemma : ∀ {o o′ ℓ ℓ′ e e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {E F G H : Functor C D}
              {f : NaturalTransformation E F}
              {g : NaturalTransformation F G}
              {h : NaturalTransformation G H}
               → (h ∘ᵥ g) ∘ᵥ f ≃ h ∘ᵥ g ∘ᵥ f
    assoc-lemma {D = D} = Category.assoc D

    sym-assoc-lemma : ∀ {o o′ ℓ ℓ′ e e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {E F G H : Functor C D}
              {f : NaturalTransformation E F}
              {g : NaturalTransformation F G}
              {h : NaturalTransformation G H}
               → h ∘ᵥ g ∘ᵥ f ≃ (h ∘ᵥ g) ∘ᵥ f
    sym-assoc-lemma {D = D} = Category.sym-assoc D

    ∘ᵥ-resp-≃ : ∀ {o o′ ℓ ℓ′ e e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {R P K : Functor C D}
        {f h : NaturalTransformation P K}
        {g i : NaturalTransformation R P} → f ≃ h → g ≃ i → f ∘ᵥ g ≃ h ∘ᵥ i
    ∘ᵥ-resp-≃ {D = D} fh gi = Category.∘-resp-≈ D fh gi

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything
open import Agda.Primitive using (lzero)

module Cubical.Data.DescendingList.Strict.Properties
 (A : Type₀)
 (_>_ : A → A → Type₀)
 where

open import Cubical.Data.DescendingList.Strict A _>_
open import Cubical.HITs.ListedFiniteSet renaming (_∈_ to _∈ʰ_)

import Cubical.Data.Empty as Empty
open Empty using (⊥-elim)
open import Cubical.Relation.Nullary.DecidableEq

open import Cubical.Relation.Nullary using (Dec; Discrete) renaming (¬_ to Type¬_)

unsort : SDL → LFSet A
unsort [] = []
unsort (cons x xs x>xs) = x ∷ unsort xs

module _ where
  open import Cubical.Relation.Nullary
  data Tri (A B C : Set) : Set where
    tri-< : A → ¬ B → ¬ C → Tri A B C
    tri-≡ : ¬ A → B → ¬ C → Tri A B C
    tri-> : ¬ A → ¬ B → C → Tri A B C

module IsoToLFSet
   (A-discrete : Discrete A)
   (>-isProp : ∀ {x y} → isProp (x > y))
   (tri : ∀ x y → Tri (y > x) (x ≡ y) (x > y))
   (>-trans : ∀ {x y z} → x > y → y > z → x > z)
   (>-irreflexive : ∀ {x} → Type¬ x > x)
  where

  Tri' : A → A → Set
  Tri' x y = Tri (y > x) (x ≡ y) (x > y)

  open import Cubical.Foundations.Logic
  open import Cubical.HITs.PropositionalTruncation

  -- Membership is defined via `LFSet`.
  -- This computes just as well as a direct inductive definition,
  -- and additionally lets us use the extra `comm` and `dup` paths to prove
  -- things about membership.
  _∈ˡ_ : A → SDL → hProp lzero
  a ∈ˡ l = a ∈ʰ unsort l

  Memˡ : SDL → A → hProp lzero
  Memˡ l a = a ∈ˡ l

  Memʰ : LFSet A → A → hProp lzero
  Memʰ l a = a ∈ʰ l

  >ᴴ-trans : ∀ x y zs → x > y → y >ᴴ zs → x >ᴴ zs
  >ᴴ-trans x y [] x>y y>zs = >ᴴ[]
  >ᴴ-trans x y (cons z zs _) x>y (>ᴴcons y>z) = >ᴴcons (>-trans x>y y>z)

  ≡ₚ-sym : ∀ {A : Set} {x y : A} → [ x ≡ₚ y ] → [ y ≡ₚ x ]
  ≡ₚ-sym p = recPropTrunc squash (λ p → ∣ sym p ∣) p

  >-all : ∀ x l → x >ᴴ l → ∀ a → [ a ∈ˡ l ] → x > a
  >-all x (cons y zs y>zs) (>ᴴcons x>y) a a∈l =
     ⊔-elim (a ≡ₚ y) (a ∈ˡ zs) (λ _ → (x > a) , >-isProp {x} {a})
       (λ a≡ₚy → substₚ (λ q → x > q , >-isProp) (≡ₚ-sym a≡ₚy) x>y)
       (λ a∈zs → >-all x zs (>ᴴ-trans x y zs x>y y>zs) a a∈zs)
       a∈l

  >-absent : ∀ x l → x >ᴴ l → [ ¬ (x ∈ˡ l) ]
  >-absent x l x>l x∈l = ⊥-elim (>-irreflexive (>-all x l x>l x x∈l))

  >ᴴ-isProp : ∀ x xs → isProp (x >ᴴ xs)
  >ᴴ-isProp x _ >ᴴ[] >ᴴ[] = refl
  >ᴴ-isProp x _ (>ᴴcons p) (>ᴴcons q) = cong >ᴴcons (>-isProp p q)

  SDL-isSet : isSet SDL
  SDL-isSet = isSetDL.isSetDL A _>_ >-isProp A-discrete where
    open import Cubical.Data.DescendingList.Properties

  insert : A → SDL → SDL
  >ᴴinsert : {x y : A} {u : SDL} → y >ᴴ u → (y > x) → y >ᴴ insert x u
  insert x [] = cons x [] >ᴴ[]
  insert x (cons y zs good) with tri x y
  insert x (cons y zs good) | tri-< x<y _ _ = cons y (insert x zs) (>ᴴinsert good x<y)
  insert x (cons y zs good) | tri-≡ _ x≡y _ = cons y zs good
  insert x (cons y zs good) | tri-> _ _ x>y = cons x (cons y zs good) (>ᴴcons x>y)
  >ᴴinsert >ᴴ[] y>x = >ᴴcons y>x
  >ᴴinsert {x} (>ᴴcons {y} y>ys) y>x with tri x y
  >ᴴinsert {x} {y} (>ᴴcons {z} z>zs) y>x | tri-< _ _ e = >ᴴcons z>zs
  >ᴴinsert {x} (>ᴴcons {y} y>ys) y>x | tri-≡ _ _ e = >ᴴcons y>ys
  >ᴴinsert {x} (>ᴴcons {y} y>ys) y>x | tri-> _ _ _ = >ᴴcons y>x

  insert-correct : ∀ x ys → unsort (insert x ys) ≡ (x ∷ unsort ys)
  insert-correct x [] = refl
  insert-correct x (cons y zs y>zs) with tri x y
  ... | tri-< _ _ _ =
    y ∷ unsort (insert x zs) ≡⟨ (λ i → y ∷ (insert-correct x zs i)) ⟩
    y ∷ x ∷ unsort zs ≡⟨ comm _ _ _ ⟩
    x ∷ y ∷ unsort zs ∎
  ... | tri-≡ _ x≡y _ = sym (dup y (unsort zs)) ∙ (λ i → (x≡y (~ i)) ∷ y ∷ unsort zs)
  ... | tri-> _ _ _ = refl

  insert-correct₂ : ∀ x y zs → unsort (insert x (insert y zs)) ≡ (x ∷ y ∷ unsort zs)
  insert-correct₂ x y zs =
    insert-correct x (insert y zs)
    ∙ cong (λ q → x ∷ q) (insert-correct y zs)

  abstract
    -- for some reason, making [exclude] non-abstract makes
    -- typechecking noticeably slower
    exclude : A → (A → hProp lzero) → (A → hProp lzero)
    exclude x h a = ¬ a ≡ₚ x ⊓ h a

    >-excluded : ∀ x xs → x >ᴴ xs → exclude x (Memʰ (x ∷ unsort xs)) ≡ Memˡ xs
    >-excluded x xs x>xs = funExt (λ a → ⇔toPath (to a) (from a)) where

     import Cubical.Data.Prod  as D
     import Cubical.Data.Sum   as D

     from : ∀ a → [ a ∈ˡ xs ] → [ ¬ a ≡ₚ x ⊓ (a ≡ₚ x ⊔ a ∈ˡ xs) ]
     from a a∈xs = (recPropTrunc (snd ⊥) a≢x) D., inr a∈xs where
       a≢x : Type¬ (a ≡ x)
       a≢x = λ a≡x → (>-absent x xs x>xs (transport (λ i → [ a≡x i ∈ˡ xs ]) a∈xs ))

     to : ∀ a → [ ¬ a ≡ₚ x ⊓ (a ≡ₚ x ⊔ a ∈ˡ xs) ] → [ a ∈ˡ xs ]
     to a (a≢x D., x) = recPropTrunc (snd (a ∈ˡ xs)) (λ {
       (D.inl a≡x) → ⊥-elim (a≢x a≡x);
       (D.inr x) → x }) x

  cons-eq : ∀ x xs x>xs y ys y>ys → x ≡ y → xs ≡ ys → cons x xs x>xs ≡ cons y ys y>ys
  cons-eq x xs x>xs y ys y>ys x≡y xs≡ys i = cons (x≡y i) (xs≡ys i)
    (>ᴴ-isProp (x≡y i) (xs≡ys i)
           (transp (λ j → (x≡y (i ∧ j)) >ᴴ (xs≡ys) (i ∧ j)) (~ i) x>xs)
           (transp (λ j → (x≡y (i ∨ ~ j)) >ᴴ (xs≡ys) (i ∨ ~ j)) i y>ys)
           i)

  Memˡ-inj-cons : ∀ x xs x>xs y ys y>ys → x ≡ y → Memˡ (cons x xs x>xs) ≡ Memˡ (cons y ys y>ys) → Memˡ xs ≡ Memˡ ys
  Memˡ-inj-cons x xs x>xs y ys y>ys x≡y e =
         Memˡ xs ≡⟨
           sym (>-excluded x xs x>xs)
         ⟩ exclude x (Memʰ (x ∷ unsort xs)) ≡⟨
           (λ i → exclude (x≡y i) (e i))
         ⟩ exclude y (Memʰ (y ∷ unsort ys)) ≡⟨
           (>-excluded y ys y>ys)
         ⟩ Memˡ ys ∎

  Memˡ-inj : ∀ l₁ l₂ → Memˡ l₁ ≡ Memˡ l₂ → l₁ ≡ l₂
  Memˡ-inj [] [] eq = refl
  Memˡ-inj [] (cons y ys y>ys) eq = ⊥-elim (transport (λ i → [ eq (~ i) y ]) (inl ∣ refl ∣))
  Memˡ-inj (cons y ys y>ys) [] eq = ⊥-elim (transport (λ i → [ eq i y ]) (inl ∣ refl ∣))
  Memˡ-inj (cons x xs x>xs) (cons y ys y>ys) e =
     ⊔-elim (x ≡ₚ y) (x ∈ʰ unsort ys)
       (λ _ → ((cons x xs x>xs) ≡ (cons y ys y>ys)) , SDL-isSet _ _)
       (recPropTrunc (SDL-isSet _ _) with-x≡y)
       (⊥-elim ∘ x∉ys)
       (transport (λ i → [ e i x ]) (inl ∣ refl ∣)) where

    xxs = cons x xs x>xs

    x∉ys : [ ¬ x ∈ˡ ys ]
    x∉ys x∈ys = ⊥-elim (>-irreflexive y>y) where
        y>x : y > x
        y>x = (>-all y ys y>ys x x∈ys)

        y∈xxs : [ y ∈ˡ (cons x xs x>xs) ]
        y∈xxs = (transport (λ i → [ e (~ i) y ]) (inl ∣ refl ∣))

        y>y : y > y
        y>y = >-all y xxs (>ᴴcons y>x) y y∈xxs

    with-x≡y : x ≡ y → (cons x xs x>xs) ≡ (cons y ys y>ys)
    with-x≡y x≡y = cons-eq x xs x>xs y ys y>ys x≡y r where

      r : xs ≡ ys
      r = Memˡ-inj _ _ (Memˡ-inj-cons x xs x>xs y ys y>ys x≡y e)

  unsort-inj : ∀ x y → unsort x ≡ unsort y → x ≡ y
  unsort-inj x y e = Memˡ-inj x y λ i a → a ∈ʰ (e i)

  insert-swap : (x y : A) (zs : SDL) → insert x (insert y zs) ≡ insert y (insert x zs)
  insert-swap x y zs =
    unsort-inj (insert x (insert y zs)) (insert y (insert x zs))
      (unsort (insert x (insert y zs))
        ≡⟨ (λ i → insert-correct₂ x y zs i) ⟩
      x ∷ y ∷ unsort zs
        ≡⟨ (λ i → comm x y (unsort zs) i) ⟩
      y ∷ x ∷ unsort zs
        ≡⟨ (λ i → insert-correct₂ y x zs (~ i)) ⟩
      unsort (insert y (insert x zs)) ∎)

  insert-dup : (x : A) (ys : SDL) → insert x (insert x ys) ≡ insert x ys
  insert-dup x ys = unsort-inj (insert x (insert x ys)) (insert x ys)
    (
      unsort (insert x (insert x ys))
        ≡⟨ (λ i → insert-correct₂ x x ys i) ⟩
      x ∷ x ∷ unsort ys
        ≡⟨ dup x (unsort ys) ⟩
      x ∷ unsort ys
        ≡⟨ (λ i → insert-correct x ys (~ i)) ⟩
      unsort (insert x ys) ∎
    )

  sort : LFSet A → SDL
  sort = LFSetRec.f [] insert insert-swap insert-dup SDL-isSet

  unsort∘sort : ∀ x → unsort (sort x) ≡ x
  unsort∘sort =
     LFPropElim.f (λ x → unsort (sort x) ≡ x)
       refl
       (λ x {ys} ys-hyp → insert-correct x (sort ys) ∙ cong (λ q → x ∷ q) ys-hyp)
       (λ xs → trunc (unsort (sort xs)) xs)

  sort∘unsort : ∀ x → sort (unsort x) ≡ x
  sort∘unsort x = unsort-inj (sort (unsort x)) x (unsort∘sort (unsort x))

  SDL-LFSet-iso : Iso SDL (LFSet A)
  SDL-LFSet-iso = (iso unsort sort unsort∘sort sort∘unsort)

  SDL≡LFSet : SDL ≡ LFSet A
  SDL≡LFSet = ua (isoToEquiv SDL-LFSet-iso)

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
{-# OPTIONS --without-K --safe #-}
-- Various operations and proofs on morphisms between products

-- Perhaps a bit of overkill? There is so much here that it's impossible to remember
-- it all
open import Categories.Category

module Categories.Object.Product.Morphisms {o ℓ e} (𝒞 : Category o ℓ e) where

open import Function using (flip)
open import Level

open import Categories.Object.Product.Core 𝒞

open Category 𝒞
open HomReasoning

private
  variable
    A B C D E F : Obj
    f f′ g g′ h i : A ⇒ B

infix 10 [_]⟨_,_⟩ [_⇒_]_×_
infix 12 [[_]] [_]π₁ [_]π₂

[[_]] : Product A B → Obj
[[ p ]] = Product.A×B p

[_]⟨_,_⟩ : ∀ (p : Product B C) → A ⇒ B → A ⇒ C → A ⇒ [[ p ]]
[ p ]⟨ f , g ⟩ = Product.⟨_,_⟩ p f g

[_]π₁ : ∀ (p : Product A B) → [[ p ]] ⇒ A
[_]π₁ = Product.π₁

[_]π₂ : ∀ (p : Product A B) → [[ p ]] ⇒ B
[_]π₂ = Product.π₂

[_⇒_]_×_ : ∀ (p₁ : Product A C) (p₂ : Product B D) →
             (A ⇒ B) → (C ⇒ D) → ([[ p₁ ]] ⇒ [[ p₂ ]])
[ p₁ ⇒ p₂ ] f × g  = [ p₂ ]⟨ f ∘ p₁.π₁ , g ∘ p₁.π₂ ⟩
  where module p₁ = Product p₁
        module p₂ = Product p₂

id×id : ∀ (p : Product A B) → [ p ⇒ p ] id × id ≈ id
id×id p = begin
  ⟨ id ∘ π₁ , id ∘ π₂ ⟩ ≈⟨ ⟨⟩-cong₂ identityˡ identityˡ ⟩
  ⟨ π₁ , π₂ ⟩           ≈⟨ η ⟩
  id                    ∎
  where open Product p

repack≡id×id : ∀ (p₁ p₂ : Product A B) → repack p₁ p₂ ≈ [ p₁ ⇒ p₂ ] id × id
repack≡id×id p₁ p₂ = sym (Product.⟨⟩-cong₂ p₂ identityˡ identityˡ)

[_⇒_]π₁∘× : ∀ (p₁ : Product A C)(p₂ : Product B D) →
              Product.π₁ p₂ ∘ [ p₁ ⇒ p₂ ] f × g ≈ f ∘ Product.π₁ p₁
[_⇒_]π₁∘× _ p₂ = Product.project₁ p₂

[_⇒_]π₂∘× : ∀ (p₁ : Product A C) (p₂ : Product B D) →
              Product.π₂ p₂ ∘ [ p₁ ⇒ p₂ ] f × g ≈ g ∘ Product.π₂ p₁
[_⇒_]π₂∘× _ p₂ = Product.project₂ p₂

[_⇒_]×-cong₂ : ∀ (p₁ : Product A B) (p₂ : Product C D) →
                 f ≈ g → h ≈ i →
                 [ p₁ ⇒ p₂ ] f × h ≈ [ p₁ ⇒ p₂ ] g × i
[_⇒_]×-cong₂ p₁ p₂ f≈g h≈i =
    Product.⟨⟩-cong₂ p₂ (∘-resp-≈ f≈g refl) (∘-resp-≈ h≈i refl)

[_⇒_]×∘⟨⟩ : ∀ (p₁ : Product A B) (p₂ : Product C D) →
              ([ p₁ ⇒ p₂ ] f × g) ∘ [ p₁ ]⟨ f′ , g′ ⟩ ≈ [ p₂ ]⟨ f ∘ f′ , g ∘ g′ ⟩
[_⇒_]×∘⟨⟩ {f = f} {g = g} {f′ = f′} {g′ = g′} p₁ p₂ = begin
  [ p₂ ]⟨ f ∘ p₁.π₁ , g ∘ p₁.π₂ ⟩ ∘ [ p₁ ]⟨ f′ , g′ ⟩ ≈⟨ p₂.∘-distribʳ-⟨⟩ ⟩
  [ p₂ ]⟨ (f ∘ p₁.π₁) ∘ p₁.⟨_,_⟩ f′ g′
        , (g ∘ p₁.π₂) ∘ p₁.⟨_,_⟩ f′ g′ ⟩              ≈⟨ p₂.⟨⟩-cong₂ assoc assoc ⟩
  [ p₂ ]⟨ f ∘ p₁.π₁ ∘ p₁.⟨_,_⟩ f′ g′
        , g ∘ p₁.π₂ ∘ p₁.⟨_,_⟩ f′ g′ ⟩                ≈⟨ p₂.⟨⟩-cong₂ (∘-resp-≈ refl p₁.project₁) (∘-resp-≈ refl p₁.project₂) ⟩
  [ p₂ ]⟨ f ∘ f′ , g ∘ g′ ⟩                           ∎
  where module p₁ = Product p₁
        module p₂ = Product p₂

[_]⟨⟩∘ : ∀ (p : Product A B) → [ p ]⟨ f , g ⟩ ∘ h ≈ [ p ]⟨ f ∘ h , g ∘ h ⟩
[ p ]⟨⟩∘ = ⟺ (unique (⟺ assoc ○ ∘-resp-≈ˡ project₁) (⟺ assoc ○ ∘-resp-≈ˡ project₂))
  where open Product p

repack∘repack≈id : ∀ (p₁ p₂ : Product A B) → repack p₁ p₂ ∘ repack p₂ p₁ ≈ id
repack∘repack≈id p₁ p₂ = [ p₂ ]⟨⟩∘ ○ p₂.⟨⟩-cong₂ p₁.project₁ p₁.project₂ ○ p₂.η
  where module p₁ = Product p₁
        module p₂ = Product p₂

[_⇒_⇒_]×∘× : ∀ (p₁ : Product A B) (p₂ : Product C D) (p₃ : Product E F) →
               ([ p₂ ⇒ p₃ ] g × i) ∘ ([ p₁ ⇒ p₂ ] f × h) ≈ [ p₁ ⇒ p₃ ] (g ∘ f) × (i ∘ h)
[_⇒_⇒_]×∘× {g = g} {i = i} {f = f} {h = h} p₁ p₂ p₃ = begin
  [ p₃ ]⟨ g ∘ p₂.π₁ , i ∘ p₂.π₂ ⟩ ∘ [ p₂ ]⟨ f ∘ p₁.π₁ , h ∘ p₁.π₂ ⟩ ≈⟨ [ p₂ ⇒ p₃ ]×∘⟨⟩ ⟩
  [ p₃ ]⟨ g ∘ f ∘ p₁.π₁ , i ∘ h ∘ p₁.π₂ ⟩                          ≈˘⟨ p₃.⟨⟩-cong₂ assoc assoc ⟩
  [ p₃ ]⟨ (g ∘ f) ∘ p₁.π₁ , (i ∘ h) ∘ p₁.π₂ ⟩                       ∎
  where module p₁ = Product p₁
        module p₂ = Product p₂
        module p₃ = Product p₃

[_⇒_⇒_]repack∘× : ∀ (p₁ : Product A B) (p₂ : Product C D) (p₃ : Product C D) →
                    repack p₂ p₃ ∘ [ p₁ ⇒ p₂ ] f × g ≈ [ p₁ ⇒ p₃ ] f × g
[_⇒_⇒_]repack∘× {f = f} {g = g} p₁ p₂ p₃ = begin
  repack p₂ p₃ ∘ [ p₁ ⇒ p₂ ] f × g            ≈⟨ repack≡id×id p₂ p₃ ⟩∘⟨ refl ⟩
  ([ p₂ ⇒ p₃ ] id × id) ∘ ([ p₁ ⇒ p₂ ] f × g) ≈⟨ [ p₁ ⇒ p₂ ⇒ p₃ ]×∘× ⟩
  [ p₁ ⇒ p₃ ] (id ∘ f) × (id ∘ g)             ≈⟨ [ p₁ ⇒ p₃ ]×-cong₂ identityˡ identityˡ ⟩
  [ p₁ ⇒ p₃ ] f × g                           ∎

[_⇒_⇒_]repack∘repack : ∀ (p₁ p₂ p₃ : Product A B) → repack p₂ p₃ ∘ repack p₁ p₂ ≈ repack p₁ p₃
[_⇒_⇒_]repack∘repack = repack∘

[_⇒_]_×id : ∀ (p₁ : Product A C) (p₂ : Product B C) → A ⇒ B → [[ p₁ ]] ⇒ [[ p₂ ]]
[ p₁ ⇒ p₂ ] f ×id = [ p₁ ⇒ p₂ ] f × id

[_⇒_]id× : ∀ (p₁ : Product A B) (p₂ : Product A C) → B ⇒ C → [[ p₁ ]] ⇒ [[ p₂ ]]
[ p₁ ⇒ p₂ ]id× g = [ p₁ ⇒ p₂ ] id × g

first-id : ∀ (p : Product A B) → [ p ⇒ p ] id ×id ≈ id
first-id = id×id

second-id : ∀ (p : Product A B) → [ p ⇒ p ]id× id ≈ id
second-id = id×id

[_⇒_]×id∘⟨⟩ : ∀ (p₁ : Product B D) (p₂ : Product C D) →
                  [ p₁ ⇒ p₂ ] f ×id ∘ [ p₁ ]⟨ f′ , g′ ⟩ ≈ [ p₂ ]⟨ f ∘ f′ , g′ ⟩
[_⇒_]×id∘⟨⟩ {f = f} {f′ = f′} {g′ = g′} p₁ p₂ = begin
  [ p₁ ⇒ p₂ ] f ×id ∘ [ p₁ ]⟨ f′ , g′ ⟩ ≈⟨ [ p₁ ⇒ p₂ ]×∘⟨⟩ ⟩
  [ p₂ ]⟨ f ∘ f′ , id ∘ g′ ⟩            ≈⟨ p₂.⟨⟩-cong₂ refl identityˡ ⟩
  [ p₂ ]⟨ f ∘ f′ , g′ ⟩                 ∎
  where module p₂ = Product p₂

[_⇒_]id×∘⟨⟩ : ∀ (p₁ : Product B D) (p₂ : Product B E) →
                   [ p₁ ⇒ p₂ ]id× g ∘ [ p₁ ]⟨ f′ , g′ ⟩ ≈ [ p₂ ]⟨ f′ , g ∘ g′ ⟩
[_⇒_]id×∘⟨⟩ {g = g} {f′ = f′} {g′ = g′} p₁ p₂ = begin
  [ p₁ ⇒ p₂ ]id× g ∘ [ p₁ ]⟨ f′ , g′ ⟩ ≈⟨ [ p₁ ⇒ p₂ ]×∘⟨⟩ ⟩
  [ p₂ ]⟨ id ∘ f′ , g ∘ g′ ⟩              ≈⟨ p₂.⟨⟩-cong₂ identityˡ refl ⟩
  [ p₂ ]⟨ f′ , g ∘ g′ ⟩                   ∎
  where module p₂ = Product p₂

[_⇒_⇒_]×id∘×id : ∀ (p₁ : Product A D) (p₂ : Product B D) (p₃ : Product C D) →
                       [ p₂ ⇒ p₃ ] f ×id ∘ [ p₁ ⇒ p₂ ] g ×id ≈ [ p₁ ⇒ p₃ ] f ∘ g ×id
[_⇒_⇒_]×id∘×id {f = f} {g = g} p₁ p₂ p₃ = begin
  [ p₂ ⇒ p₃ ] f ×id ∘ [ p₁ ⇒ p₂ ] g ×id ≈⟨ [ p₁ ⇒ p₂ ⇒ p₃ ]×∘× ⟩
  [ p₁ ⇒ p₃ ] (f ∘ g) × (id ∘ id)       ≈⟨ [ p₁ ⇒ p₃ ]×-cong₂ refl identityˡ ⟩
  [ p₁ ⇒ p₃ ] f ∘ g ×id                 ∎

[_⇒_⇒_]id×∘id× : ∀ (p₁ : Product A B) (p₂ : Product A C) (p₃ : Product A D) →
                         [ p₂ ⇒ p₃ ]id× f ∘ [ p₁ ⇒ p₂ ]id× g ≈ [ p₁ ⇒ p₃ ]id×(f ∘ g)
[_⇒_⇒_]id×∘id× {f = f} {g = g} p₁ p₂ p₃ = begin
  [ p₂ ⇒ p₃ ]id× f ∘ [ p₁ ⇒ p₂ ]id× g ≈⟨ [ p₁ ⇒ p₂ ⇒ p₃ ]×∘× ⟩
  [ p₁ ⇒ p₃ ] (id ∘ id) × (f ∘ g)     ≈⟨ [ p₁ ⇒ p₃ ]×-cong₂ identityˡ refl ⟩
  [ p₁ ⇒ p₃ ]id× (f ∘ g)              ∎

[_⇒_,_⇒_]first↔second : ∀ (p₁ : Product A D) (p₂ : Product B D)
                          (p₃ : Product A C) (p₄ : Product B C) →
                          [ p₁ ⇒ p₂ ] f ×id ∘ [ p₃ ⇒ p₁ ]id× g ≈ [ p₄ ⇒ p₂ ]id× g ∘ [ p₃ ⇒ p₄ ] f ×id
[_⇒_,_⇒_]first↔second {f = f} {g = g} p₁ p₂ p₃ p₄ = begin
  [ p₁ ⇒ p₂ ] f ×id ∘ [ p₃ ⇒ p₁ ]id× g ≈⟨ [ p₃ ⇒ p₁ ⇒ p₂ ]×∘× ⟩
  [ p₃ ⇒ p₂ ] (f ∘ id) × (id ∘ g)      ≈⟨ [ p₃ ⇒ p₂ ]×-cong₂ identityʳ identityˡ ⟩
  [ p₃ ⇒ p₂ ] f × g                    ≈⟨ sym ([ p₃ ⇒ p₂ ]×-cong₂ identityˡ identityʳ) ⟩
  [ p₃ ⇒ p₂ ] (id ∘ f) × (g ∘ id)      ≈⟨ sym ([ p₃ ⇒ p₄ ⇒ p₂ ]×∘×) ⟩
  [ p₄ ⇒ p₂ ]id× g ∘ [ p₃ ⇒ p₄ ] f ×id ∎

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
module LineEndings.Mac where

postulate ThisWorks : Set


text:
{-# OPTIONS --type-in-type #-}

module TypeInTypeAndUnivPoly where

open import UniversePolymorphism

-- The level metas should be solved with 0 when we have --type-in-type
fst′ : ∀ {A B} → Σ A B → A
fst′ x = fst x


text:
module Structure.Relator.Proofs where

import      Data.Either as Either
import      Data.Tuple as Tuple
open import Functional
open import Function.Proofs
open import Logic
open import Logic.Propositional.Proofs.Structures
open import Logic.Propositional
open import Logic.Predicate
import      Lvl
open import Structure.Function
open import Structure.Operator
open import Structure.Setoid
open import Structure.Relator.Properties
open import Structure.Relator
open import Syntax.Transitivity
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓₗ ℓₗ₁ ℓₗ₂ ℓₗ₃ ℓₗ₄ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₑ₄ : Lvl.Level
private variable A B A₁ A₂ B₁ B₂ : Type{ℓ}

[≡]-binaryRelator : ∀ ⦃ equiv : Equiv{ℓₗ}(A) ⦄ → BinaryRelator ⦃ equiv ⦄ (_≡_)
BinaryRelator.substitution [≡]-binaryRelator {x₁} {y₁} {x₂} {y₂} xy1 xy2 x1x2 =
  y₁ 🝖-[ xy1 ]-sym
  x₁ 🝖-[ x1x2 ]
  x₂ 🝖-[ xy2 ]
  y₂ 🝖-end

reflexive-binaryRelator-sub : ∀ ⦃ equiv : Equiv{ℓₗ}(A) ⦄ {_▫_ : A → A → Type{ℓ}} ⦃ refl : Reflexivity(_▫_) ⦄ ⦃ rel : BinaryRelator ⦃ equiv ⦄ (_▫_) ⦄ → ((_≡_) ⊆₂ (_▫_))
_⊆₂_.proof (reflexive-binaryRelator-sub {_▫_ = _▫_}) xy = substitute₂ᵣ(_▫_) xy (reflexivity(_▫_))

module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {f : A → B} ⦃ func : Function(f) ⦄
  {P : B → Stmt{ℓₗ₃}} ⦃ rel : UnaryRelator(P) ⦄
  where

  [∘]-unaryRelator : UnaryRelator(P ∘ f)
  [∘]-unaryRelator = [↔]-to-[←] relator-function₁ ([∘]-function ⦃ equiv-c = [↔]-equiv ⦄ ⦃ func-f = [↔]-to-[→] relator-function₁ rel ⦄)

module _
  ⦃ equiv-A₁ : Equiv{ℓₑ₁}(A₁) ⦄
  ⦃ equiv-B₁ : Equiv{ℓₑ₂}(B₁) ⦄
  ⦃ equiv-A₂ : Equiv{ℓₑ₃}(A₂) ⦄
  ⦃ equiv-B₂ : Equiv{ℓₑ₄}(B₂) ⦄
  {f : A₁ → A₂} ⦃ func-f : Function(f) ⦄
  {g : B₁ → B₂} ⦃ func-g : Function(g) ⦄
  {_▫_ : A₂ → B₂ → Stmt{ℓₗ}} ⦃ rel : BinaryRelator(_▫_) ⦄
  where

  [∘]-binaryRelator : BinaryRelator(x ↦ y ↦ f(x) ▫ g(y))
  BinaryRelator.substitution [∘]-binaryRelator xy1 xy2 = substitute₂(_▫_) (congruence₁(f) xy1) (congruence₁(g) xy2)

module _
  ⦃ equiv-A : Equiv{ℓₑ}(A) ⦄
  {P : A → Stmt{ℓₗ₁}} ⦃ rel-P : UnaryRelator(P) ⦄
  {▫ : Stmt{ℓₗ₁} → Stmt{ℓₗ₂}} ⦃ rel : Function ⦃ [↔]-equiv ⦄ ⦃ [↔]-equiv ⦄ ▫ ⦄
  where

  unaryRelator-sub : UnaryRelator(▫ ∘ P)
  unaryRelator-sub = [∘]-unaryRelator
    ⦃ equiv-B = [↔]-equiv ⦄
    ⦃ func = [↔]-to-[→] relator-function₁ rel-P ⦄
    ⦃ rel = [↔]-to-[←] (relator-function₁ ⦃ [↔]-equiv ⦄) rel ⦄

module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {P : A → Stmt{ℓₗ₁}} ⦃ rel-P : UnaryRelator(P) ⦄
  {Q : B → Stmt{ℓₗ₂}} ⦃ rel-Q : UnaryRelator(Q) ⦄
  {_▫_ : Stmt{ℓₗ₁} → Stmt{ℓₗ₂} → Stmt{ℓₗ₃}} ⦃ rel : BinaryOperator ⦃ [↔]-equiv ⦄ ⦃ [↔]-equiv ⦄ ⦃ [↔]-equiv ⦄ (_▫_) ⦄
  where

  binaryRelator-sub : BinaryRelator(x ↦ y ↦ P(x) ▫ Q(y))
  binaryRelator-sub = [∘]-binaryRelator
    ⦃ equiv-A₂ = [↔]-equiv ⦄
    ⦃ equiv-B₂ = [↔]-equiv ⦄
    ⦃ func-f = [↔]-to-[→] relator-function₁ rel-P ⦄
    ⦃ func-g = [↔]-to-[→] relator-function₁ rel-Q ⦄
    ⦃ rel = [↔]-to-[←] (relator-function₂ ⦃ [↔]-equiv ⦄ ⦃ [↔]-equiv ⦄) rel ⦄

module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {P : A → Stmt{ℓₗ₁}} ⦃ rel-P : UnaryRelator(P) ⦄
  {Q : B → Stmt{ℓₗ₂}} ⦃ rel-Q : UnaryRelator(Q) ⦄
  where

  [→]-binaryRelator : BinaryRelator(x ↦ y ↦ (P(x) → Q(y)))
  [→]-binaryRelator = binaryRelator-sub{_▫_ = _→ᶠ_}

  [↔]-binaryRelator : BinaryRelator(x ↦ y ↦ (P(x) ↔ Q(y)))
  [↔]-binaryRelator = binaryRelator-sub{_▫_ = _↔_}

[→]-unaryRelator : ∀ ⦃ _ : Equiv{ℓₗ₃}(A) ⦄ {P : A → Stmt{ℓₗ₁}}{Q : A → Stmt{ℓₗ₂}} → ⦃ rel-P : UnaryRelator(P) ⦄ → ⦃ rel-Q : UnaryRelator(Q) ⦄ → UnaryRelator(\x → P(x) → Q(x))
UnaryRelator.substitution ([→]-unaryRelator {P = P}{Q = Q}) xy pxqx py = substitute₁(Q) xy (pxqx(substitute₁(P) (symmetry(_≡_) xy) py))

[∀]-unaryRelator : ∀ ⦃ _ : Equiv{ℓₗ₃}(A) ⦄ {P : B → A → Stmt{ℓₗ₁}} → ⦃ rel-P : ∀{x} → UnaryRelator(P(x)) ⦄ → UnaryRelator(\y → ∀{x} → P(x)(y))
UnaryRelator.substitution ([∀]-unaryRelator {P = P}) {x} {a} xy px {b} = substitute₁ (P b) xy px

[∃]-unaryRelator : ∀ ⦃ _ : Equiv{ℓₗ₃}(A) ⦄ {P : B → A → Stmt{ℓₗ₁}} → ⦃ rel-P : ∀{x} → UnaryRelator(P(x)) ⦄ → UnaryRelator(\y → ∃(x ↦ P(x)(y)))
UnaryRelator.substitution ([∃]-unaryRelator {P = P}) xy = [∃]-map-proof (substitute₁(P _) xy)

instance
  const-unaryRelator : ∀{P : Stmt{ℓₗ₁}} → ⦃ _ : Equiv{ℓₗ}(A) ⦄ → UnaryRelator{A = A}(const P)
  UnaryRelator.substitution const-unaryRelator = const id

[¬]-unaryRelator : ∀ ⦃ _ : Equiv{ℓₗ₂}(A) ⦄ {P : A → Stmt{ℓₗ₁}} → ⦃ rel-P : UnaryRelator(P) ⦄ → UnaryRelator(\x → ¬ P(x))
[¬]-unaryRelator {P = P} = [→]-unaryRelator

[∧]-unaryRelator : ∀ ⦃ _ : Equiv{ℓₗ₃}(A) ⦄ {P : A → Stmt{ℓₗ₁}}{Q : A → Stmt{ℓₗ₂}} → ⦃ rel-P : UnaryRelator(P) ⦄ → ⦃ rel-Q : UnaryRelator(Q) ⦄ → UnaryRelator(x ↦ P(x) ∧ Q(x))
UnaryRelator.substitution [∧]-unaryRelator xy = Tuple.map (substitute₁(_) xy) (substitute₁(_) xy)

[∨]-unaryRelator : ∀ ⦃ _ : Equiv{ℓₗ₃}(A) ⦄ {P : A → Stmt{ℓₗ₁}}{Q : A → Stmt{ℓₗ₂}} → ⦃ rel-P : UnaryRelator(P) ⦄ → ⦃ rel-Q : UnaryRelator(Q) ⦄ → UnaryRelator(x ↦ P(x) ∨ Q(x))
UnaryRelator.substitution [∨]-unaryRelator xy = Either.map (substitute₁(_) xy) (substitute₁(_) xy)

binary-unaryRelator : ∀ ⦃ _ : Equiv{ℓₗ₂}(A) ⦄ {P : A → A → Stmt{ℓₗ₁}} → ⦃ rel-P : BinaryRelator(P) ⦄ → UnaryRelator(P $₂_)
UnaryRelator.substitution (binary-unaryRelator {P = P}) xy pxx = substitute₂(P) xy xy pxx

binary-unaryRelatorₗ : ∀ ⦃ _ : Equiv{ℓₗ₁}(A) ⦄ ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ {_▫_ : A → B → Stmt{ℓₗ₃}} → ⦃ rel-P : BinaryRelator(_▫_) ⦄ → ∀{x} → UnaryRelator(x ▫_)
UnaryRelator.substitution binary-unaryRelatorₗ xy x1x2 = substitute₂ _ (reflexivity(_≡_)) xy x1x2

binary-unaryRelatorᵣ : ∀ ⦃ _ : Equiv{ℓₗ₁}(A) ⦄ ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ {_▫_ : A → B → Stmt{ℓₗ₃}} → ⦃ rel-P : BinaryRelator(_▫_) ⦄ → ∀{x} → UnaryRelator(_▫ x)
UnaryRelator.substitution binary-unaryRelatorᵣ xy x1x2 = substitute₂ _ xy (reflexivity(_≡_)) x1x2

binaryRelator-from-unaryRelator : ∀ ⦃ _ : Equiv{ℓₗ₂}(A) ⦄ {_▫_ : A → A → Stmt{ℓₗ₁}} → ⦃ relₗ : ∀{x} → UnaryRelator(_▫ x) ⦄ → ⦃ relᵣ : ∀{x} → UnaryRelator(x ▫_) ⦄ → BinaryRelator(_▫_)
BinaryRelator.substitution binaryRelator-from-unaryRelator xy1 xy2 = substitute₁ _ xy1 ∘ substitute₁ _ xy2

instance
  const-binaryRelator : ∀{P : Stmt{ℓₗ}} → ⦃ equiv-A : Equiv{ℓₗ₁}(A) ⦄ ⦃ equiv-B : Equiv{ℓₗ₂}(B) ⦄ → BinaryRelator{A = A}{B = B}((const ∘ const) P)
  BinaryRelator.substitution const-binaryRelator = (const ∘ const) id

-- TODO: Temporary until substitution is a specialization of congruence
[¬]-binaryRelator : ∀ ⦃ _ : Equiv{ℓₗ₂}(A) ⦄ ⦃ _ : Equiv{ℓₗ₃}(B) ⦄ {P : A → B → Stmt{ℓₗ₁}} → ⦃ rel-P : BinaryRelator(P) ⦄ → BinaryRelator(\x y → ¬ P(x)(y))
BinaryRelator.substitution ([¬]-binaryRelator {P = P}) xy₁ xy₂ npx py = npx(substitute₂(P) (symmetry(_≡_) xy₁) (symmetry(_≡_) xy₂) py)

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:
module SecondOrder.VContext {ℓ} (sort : Set ℓ)  where

  -- a context is a binary tree whose leaves are labeled with sorts
  data VContext : Set ℓ where
    ctx-empty : VContext
    ctx-slot : sort → VContext
    _,,_ : VContext → VContext → VContext

  infixl 5 _,,_

  infix 4 _∈_

  -- the variables of a given type in a context
  data _∈_ (A : sort) : VContext → Set ℓ where
    var-slot : A ∈ ctx-slot A
    var-inl : ∀ {Γ Δ} (x : A ∈ Γ) → A ∈ Γ ,, Δ
    var-inr : ∀ {Γ Δ} (y : A ∈ Δ) → A ∈ Γ ,, Δ

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


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

open import lib.Basics
open import lib.NType2
open import lib.types.Sigma
open import lib.types.Pi
open import lib.types.Group
open import lib.types.Int
open import lib.types.List
open import lib.types.SetQuotient

module lib.groups.FormalSum {i} where

PreFormalSum : Type i → Type i
PreFormalSum A = List (ℤ × A)

module _ {A : Type i} (dec : has-dec-eq A) where

  coef-pre : PreFormalSum A → (A → ℤ)
  coef-pre l a = ℤsum $ map fst $ filter (λ{(_ , a') → dec a' a}) l

  -- Extensional equality
  FormalSum-rel : Rel (PreFormalSum A) i
  FormalSum-rel l₁ l₂ = ∀ a → coef-pre l₁ a == coef-pre l₂ a

  -- The quotient
  FormalSum : Type i
  FormalSum = SetQuotient FormalSum-rel

  -- Properties of [coef-pre]
  coef-pre-++ : ∀ l₁ l₂ a
    → coef-pre (l₁ ++ l₂) a == coef-pre l₁ a ℤ+ coef-pre l₂ a
  coef-pre-++ nil              l₂ a = idp
  coef-pre-++ ((z , a') :: l₁) l₂ a with dec a' a
  ... | inl _ = ap (z ℤ+_) (coef-pre-++ l₁ l₂ a)
              ∙ ! (ℤ+-assoc z (coef-pre l₁ a) (coef-pre l₂ a))
  ... | inr _ = coef-pre-++ l₁ l₂ a

  flip-pre : PreFormalSum A → PreFormalSum A
  flip-pre = map λ{(z , a) → (ℤ~ z , a)}

  coef-pre-flip-pre : ∀ l a
    → coef-pre (flip-pre l) a == ℤ~ (coef-pre l a)
  coef-pre-flip-pre nil a = idp
  coef-pre-flip-pre ((z , a') :: l) a with dec a' a
  ... | inl _ = ap (ℤ~ z ℤ+_) (coef-pre-flip-pre l a)
              ∙ ! (ℤ~-ℤ+ z (coef-pre l a))
  ... | inr _ = coef-pre-flip-pre l a

module _ {A : Type i} {dec : has-dec-eq A} where

  coef : FormalSum dec → (A → ℤ)
  coef = SetQuot-rec (→-is-set ℤ-is-set) (coef-pre dec) λ=

  -- extensionality of formal sums.
  coef-ext : ∀ {fs₁ fs₂} → (∀ a → coef fs₁ a == coef fs₂ a) → fs₁ == fs₂
  coef-ext {fs₁} {fs₂} = ext' fs₁ fs₂ where
    ext' : ∀ fs₁ fs₂ → (∀ a → coef fs₁ a == coef fs₂ a) → fs₁ == fs₂
    ext' = SetQuot-elim
      (λ _ → Π-is-set λ _ → →-is-set $ =-preserves-set SetQuotient-is-set)
      (λ l₁ → SetQuot-elim
        (λ _ → →-is-set $ =-preserves-set SetQuotient-is-set)
        (λ l₂ r → quot-rel r)
        (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → SetQuotient-is-set _ _)))
      (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → Π-is-prop λ _ → SetQuotient-is-set _ _))

  -- TODO Use abstract [FormalSum].

  infixl 80 _⊞_
  _⊞_ : FormalSum dec → FormalSum dec → FormalSum dec
  _⊞_ = SetQuot-rec
    (→-is-set SetQuotient-is-set)
    (λ l₁ → SetQuot-rec SetQuotient-is-set (q[_] ∘ (l₁ ++_))
      (λ {l₂} {l₂'} r → quot-rel λ a
        → coef-pre-++ dec l₁ l₂ a
        ∙ ap (coef-pre dec l₁ a ℤ+_) (r a)
        ∙ ! (coef-pre-++ dec l₁ l₂' a)))
    (λ {l₁} {l₁'} r → λ= $ SetQuot-elim
      (λ _ → =-preserves-set SetQuotient-is-set)
      (λ l₂ → quot-rel λ a
        → coef-pre-++ dec l₁ l₂ a
        ∙ ap (_ℤ+ coef-pre dec l₂ a) (r a)
        ∙ ! (coef-pre-++ dec l₁' l₂ a))
      (λ _ → prop-has-all-paths-↓ (SetQuotient-is-set _ _)))

  coef-⊞ : ∀ fs₁ fs₂ a → coef (fs₁ ⊞ fs₂) a == coef fs₁ a ℤ+ coef fs₂ a
  coef-⊞ = SetQuot-elim
    (λ _ → Π-is-set λ _ → Π-is-set λ _ → =-preserves-set ℤ-is-set)
    (λ l₁ → SetQuot-elim
      (λ _ → Π-is-set λ _ → =-preserves-set ℤ-is-set)
      (λ l₂ → coef-pre-++ dec l₁ l₂)
      (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → ℤ-is-set _ _)))
    (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → Π-is-prop λ _ → ℤ-is-set _ _))

  ⊟ : FormalSum dec → FormalSum dec
  ⊟ = SetQuot-rec SetQuotient-is-set (q[_] ∘ flip-pre dec)
    λ {l₁} {l₂} r → quot-rel λ a
      → coef-pre-flip-pre dec l₁ a ∙ ap ℤ~ (r a) ∙ ! (coef-pre-flip-pre dec l₂ a)

  coef-⊟ : ∀ fs a → coef (⊟ fs) a == ℤ~ (coef fs a)
  coef-⊟ = SetQuot-elim
    (λ _ → Π-is-set λ _ → =-preserves-set ℤ-is-set)
    (λ l a → coef-pre-flip-pre dec l a)
    (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → ℤ-is-set _ _))

  ⊞-unit : FormalSum dec
  ⊞-unit = q[ nil ]

  coef-⊞-unit : ∀ a → coef ⊞-unit a == 0
  coef-⊞-unit a = idp

{-
  -- Favonia: These commented-out proofs are valid, but I want to promote
  -- the usage of [coef-ext].

  ⊞-unit-l : ∀ fs → ⊞-unit ⊞ fs == fs
  ⊞-unit-l = SetQuot-elim
    (λ _ → =-preserves-set SetQuotient-is-set)
    (λ l → idp)
    (λ _ → prop-has-all-paths-↓ (SetQuotient-is-set _ _))

  ⊞-unit-r : ∀ fs → fs ⊞ ⊞-unit == fs
  ⊞-unit-r = SetQuot-elim
    (λ _ → =-preserves-set SetQuotient-is-set)
    (λ l → ap q[_] $ ++-nil-r l)
    (λ _ → prop-has-all-paths-↓ (SetQuotient-is-set _ _))
-}

  ⊞-unit-l : ∀ fs → ⊞-unit ⊞ fs == fs
  ⊞-unit-l fs = coef-ext λ a → coef-⊞ ⊞-unit fs a

  ⊞-unit-r : ∀ fs → fs ⊞ ⊞-unit == fs
  ⊞-unit-r fs = coef-ext λ a → coef-⊞ fs ⊞-unit a ∙ ℤ+-unit-r _

  ⊞-assoc : ∀ fs₁ fs₂ fs₃ → (fs₁ ⊞ fs₂) ⊞ fs₃ == fs₁ ⊞ (fs₂ ⊞ fs₃)
  ⊞-assoc fs₁ fs₂ fs₃ = coef-ext λ a →
    coef ((fs₁ ⊞ fs₂) ⊞ fs₃) a
      =⟨ coef-⊞ (fs₁ ⊞ fs₂) fs₃ a ⟩
    coef (fs₁ ⊞ fs₂) a ℤ+ coef fs₃ a
      =⟨ coef-⊞ fs₁ fs₂ a |in-ctx _ℤ+ coef fs₃ a ⟩
    (coef fs₁ a ℤ+ coef fs₂ a) ℤ+ coef fs₃ a
      =⟨ ℤ+-assoc (coef fs₁ a) (coef fs₂ a) (coef fs₃ a) ⟩
    coef fs₁ a ℤ+ (coef fs₂ a ℤ+ coef fs₃ a)
      =⟨ ! $ coef-⊞ fs₂ fs₃ a |in-ctx coef fs₁ a ℤ+_ ⟩
    coef fs₁ a ℤ+ coef (fs₂ ⊞ fs₃) a
      =⟨ ! $ coef-⊞ fs₁ (fs₂ ⊞ fs₃) a ⟩
    coef (fs₁ ⊞ (fs₂ ⊞ fs₃)) a
      ∎

  ⊟-inv-r : ∀ fs → fs ⊞ (⊟ fs) == ⊞-unit
  ⊟-inv-r fs = coef-ext λ a → coef-⊞ fs (⊟ fs) a
                            ∙ ap (coef fs a ℤ+_) (coef-⊟ fs a)
                            ∙ ℤ~-inv-r (coef fs a)

  ⊟-inv-l : ∀ fs → (⊟ fs) ⊞ fs == ⊞-unit
  ⊟-inv-l fs = coef-ext λ a → coef-⊞ (⊟ fs) fs a
                            ∙ ap (_ℤ+ coef fs a) (coef-⊟ fs a)
                            ∙ ℤ~-inv-l (coef fs a)

  FormalSum-group-structure : GroupStructure (FormalSum dec)
  FormalSum-group-structure = record
    { ident = ⊞-unit
    ; inv = ⊟
    ; comp = _⊞_
    ; unitl = ⊞-unit-l
    ; unitr = ⊞-unit-r
    ; assoc = ⊞-assoc
    ; invr = ⊟-inv-r
    ; invl = ⊟-inv-l
    }

  FormalSum-group : Group i
  FormalSum-group = group _ SetQuotient-is-set FormalSum-group-structure

  has-finite-supports : (A → ℤ) → Type i
  has-finite-supports f = Σ (FormalSum dec) λ fs → ∀ a → f a == coef fs a

  has-finite-supports-is-prop : ∀ f → is-prop (has-finite-supports f)
  has-finite-supports-is-prop f = all-paths-is-prop
    λ{(fs₁ , match₁) (fs₂ , match₂) → pair=
      (coef-ext λ a → ! (match₁ a) ∙ match₂ a)
      (prop-has-all-paths-↓ $ Π-is-prop λ _ → ℤ-is-set _ _)}

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
-- Andreas, 2013-10-20 'with' only abstracts at base type
module WithOfFunctionType where

postulate
  A B : Set
  P : B → Set
  mkP : (x : B) → P x
  f : A → B
  a : A

test : P (f a)
test with f
... | g = mkP (g a)


text:
module _ where

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.TrustMe

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

open _×_

-- Nested pattern prevents record pattern translation.
f : Nat × Nat → Nat
f (zero  , b) = b
f (suc a , b) = a + b

-- With catch-all case
g : Nat × Nat → Nat
g (zero , b) = b
g p          = fst p + snd p

-- Definition by copatterns.
p : Nat × Nat
p .fst = 2
p .snd = 2

test-f : f p ≡ 3
test-f = refl

test-g : g p ≡ 4
test-g = refl

-- Slow reduce. primTrustMe doesn't use fast-reduce

is-refl : ∀ {A : Set} (x y : A) → x ≡ y → Bool
is-refl x y refl = true

test-slow-f : is-refl (f p) 3 primTrustMe ≡ true
test-slow-f = refl

test-slow-g : is-refl (g p) 4 primTrustMe ≡ true
test-slow-g = refl


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

open import HoTT
open import cohomology.CofiberSequence
open import cohomology.Exactness
open import cohomology.FunctionOver
open import cohomology.SplitExactRight
open import cohomology.Theory

module cohomology.Sigma {i} (CT : CohomologyTheory i) where

open CohomologyTheory CT
open import cohomology.Functor CT
open import cohomology.BaseIndependence CT

{- Cⁿ(Σx:X.Y) = Cⁿ(⋁x:X.Y) × Cⁿ(X). The proof is by constructing a
 - splitting exact sequence

       0 → Cⁿ(⋁x:X.Y) → Cⁿ(Σx:X.Y) → Cⁿ(X)

 - by observing that the map [select : x ↦ (x, snd Yₓ)] has a left inverse
 - and satisfies [Cofiber select == ⋁x:X.Y. -}

module CofSelect (X : Ptd i) (Y : fst X → Ptd i) where

  select : fst X → fst (⊙Σ X Y)
  select x = (x , snd (Y x))

  ⊙select : fst (X ⊙→ ⊙Σ X Y)
  ⊙select = (select , idp)

  ⊙Σbwin : fst (⊙Σ X Y ⊙→ ⊙BigWedge Y)
  ⊙Σbwin = (uncurry bwin , ! (bwglue (snd X)))

  eq : Cofiber select ≃ BigWedge Y
  eq = equiv Into.f Out.f into-out out-into
    where
    module Into = CofiberRec select {C = BigWedge Y}
      bwbase (uncurry bwin) bwglue

    module Out = BigWedgeRec {X = Y} {C = Cofiber select}
      (cfbase _) (curry (cfcod _)) (cfglue _)

    into-out : ∀ w → Into.f (Out.f w) == w
    into-out = BigWedge-elim
      idp (λ _ _ → idp)
      (↓-∘=idf-in Into.f Out.f ∘ λ x →
        ap (ap Into.f) (Out.glue-β x) ∙ Into.glue-β x)

    out-into : ∀ c → Out.f (Into.f c) == c
    out-into = Cofiber-elim select
      idp (λ _ → idp)
      (↓-∘=idf-in Out.f Into.f ∘ λ x →
        ap (ap Out.f) (Into.glue-β x) ∙ Out.glue-β x)

  ⊙path : ⊙Cof ⊙select == ⊙BigWedge Y
  ⊙path = ⊙ua eq idp

  cfcod-over : cfcod _ == uncurry bwin [ (λ U → fst (⊙Σ X Y) → fst U) ↓ ⊙path ]
  cfcod-over = ↓-cst2-in _ _ $ codomain-over-equiv _ _

  ext-glue-cst : ext-glue {s = cofiber-span select} == cst (north _)
  ext-glue-cst = λ= $ Cofiber-elim _
    idp
    (λ {(x , y) → ! (merid _ x)})
    (↓-='-from-square ∘ λ x →
      ExtGlue.glue-β x ∙v⊡
        tr-square (merid _ x)
      ⊡v∙ ! (ap-cst (north _) (cfglue _ x)))

  ext-over : ext-glue == cst (north _)
             [ (λ U → fst U → fst (⊙Susp X)) ↓ ⊙path ]
  ext-over = ↓-cst2-in _ _ $ ext-glue-cst ◃ domain-over-equiv _ _

module CΣ (n : ℤ) (X : Ptd i) (Y : fst X → Ptd i) where

  open CofSelect X Y

  private
    seq : HomSequence _ _
    seq =
      C n (⊙Susp X)     ⟨ cst-hom ⟩→
      C n (⊙BigWedge Y) ⟨ CF-hom n ⊙Σbwin ⟩→
      C n (⊙Σ X Y)      ⟨ CF-hom n ⊙select ⟩→
      C n X             ⊣|

    eseq : is-exact-seq seq
    eseq = exact-build seq
      (transport (λ {(φ , ψ) → is-exact ψ φ})
        (pair×= (CF-base-indep n _ _ _) (CF-base-indep n _ _ _ ∙ CF-cst n))
        (transport {A = Σ _ (λ {(U , g , h) → (g (snd (⊙Σ X Y)) == snd U)
                                            × (h (snd U) == north _)})}
          (λ {((_ , g , h) , (p , q)) →
            is-exact (CF-hom n (h , q)) (CF-hom n (g , p))})
          (pair= (pair= ⊙path (↓-×-in cfcod-over ext-over))
                 (↓-×-in (from-transp _ _ idp) (from-transp _ _ idp)))
          (transport {A = Σ _ (λ {(U , g) → g (cfbase _) == snd U})}
            (λ {((_ , g) , p) →
              is-exact (CF-hom n (g , p)) (CF-hom n (⊙cfcod ⊙select))})
            (pair= (pair= (Cof².space-path ⊙select) (Cof².cfcod²-over ⊙select))
                   (from-transp _ _ idp))
            (C-exact n (⊙cfcod ⊙select)))))
      (transport (λ φ → is-exact φ (CF-hom n ⊙select))
        (CF-base-indep n _ _ _)
        (transport {A = Σ _ (λ {(U , g) → g (snd (⊙Σ X Y)) == snd U})}
          (λ {((_ , g) , p) → is-exact (CF-hom n (g , p)) (CF-hom n ⊙select)})
          (pair= (pair= ⊙path cfcod-over) (from-transp _ _ idp))
          (C-exact n ⊙select)))

    module SER = SplitExactRight (C-abelian n _)
      (CF-hom n ⊙Σbwin) (CF-hom n ⊙select)
      eseq
      (CF-hom n (⊙dfst Y))
      (app= $ ap GroupHom.f $ CF-inverse n ⊙select (⊙dfst Y) (λ _ → idp))

  path : C n (⊙Σ X Y) == C n (⊙BigWedge Y) ×ᴳ C n X
  path = SER.iso

  ⊙Σbwin-over : CF-hom n ⊙Σbwin == ×ᴳ-inl
                [ (λ G → GroupHom (C n (⊙BigWedge Y)) G) ↓ path ]
  ⊙Σbwin-over = SER.φ-over-iso

  ⊙select-over : CF-hom n ⊙select == ×ᴳ-snd {G = C n (⊙BigWedge Y)}
                 [ (λ G → GroupHom G (C n X)) ↓ path ]
  ⊙select-over = SER.ψ-over-iso

  open CofSelect public using (select; ⊙select; ⊙Σbwin)

module C⊔ (n : ℤ) (X Y : Ptd i) where

  private
    T : Sphere {i} 0 → Ptd i
    T (lift true) = X
    T (lift false) = Y

  path : C n (X ⊙⊔ Y) == C n (X ⊙∨ Y) ×ᴳ C n (⊙Sphere 0)
  path = ap (C n) (! (⊙ua (ΣBool-equiv-⊔ (fst ∘ T)) idp))
         ∙ CΣ.path n (⊙Sphere 0) T
         ∙ ap (λ Z → C n Z ×ᴳ C n (⊙Sphere 0)) (BigWedge-Bool-⊙path T)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
open import Data.Bool using (Bool; true; false; _∧_)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; subst)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Unit using (⊤; tt)
open import Data.Nat using (ℕ; zero; suc; _≤_; _≥_; _>_)
open import Data.Product using (_×_; _,_; proj₁; proj₂; Σ-syntax; ∃; ∃-syntax)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.List using (List; []; [_]; _∷_; _∷ʳ_; _++_)
open import Data.List.Reverse using (Reverse; reverseView)
open import Function using (_$_)

module SnapshotConsistency
  (Addr : Set) (_≟_ : Addr → Addr → Bool) (_≤?MAXADDR : Addr → Bool) (_≤?MAXWCNT : ℕ → Bool)
  (Data : Set) (defaultData : Data)
  where

infixl 20 _•_
infixl 20 _⊙_
infixl 20 _++RTC_
infixl 20 _<≐>_

variable
  addr : Addr
  dat  : Data

_≐_ : {A B : Set} → (A → B) → (A → B) → Set
s ≐ t = ∀ a → s a ≡ t a

sym-≐ : {A B : Set} {s t : A → B} → s ≐ t → t ≐ s
sym-≐ eq = λ{x → sym (eq x)}

_<≐>_ : {A B : Set} {s t u : A → B} → s ≐ t → t ≐ u → s ≐ u
_<≐>_ {A} {B} {s} {t} {u} e q = λ{x → begin s x ≡⟨ e x ⟩ t x ≡⟨ q x ⟩ u x ∎}

data SnocList (A : Set) : Set where
  []  : SnocList A
  _•_ : (as : SnocList A) → (a : A) → SnocList A

_⊙_ : {A : Set} → SnocList A → SnocList A → SnocList A
xs ⊙ []       = xs
xs ⊙ (ys • y) = (xs ⊙ ys) • y

data All {A : Set} (P : A → Set) : SnocList A → Set where
  []  : All P []
  _∷_ : ∀ {xs : SnocList A} {x : A} → All P xs → P x → All P (xs • x)

_++All_ : {A : Set} {P : A → Set} {xs ys : SnocList A} → All P xs → All P ys → All P (xs ⊙ ys)
all₁ ++All [] = all₁
all₁ ++All (all₂ ∷ x) = all₁ ++All all₂ ∷ x

mapAll : {A : Set} {P Q : A → Set} {xs : SnocList A}
       → ({x : A} → P x → Q x) → All P xs → All Q xs
mapAll pq []        = []
mapAll pq (all ∷ x) = (mapAll pq all) ∷ (pq x)

data Action : Set where
  w[_↦_]  : (addr : Addr) (dat : Data) → Action
  f       :                              Action
  r       :                              Action
  wᶜ[_↦_] : (addr : Addr) (dat : Data) → Action
  fᶜ      :                              Action
  rᶜ      :                              Action
  cp      :                              Action
  er      :                              Action
  cpᶜ     :                              Action
  erᶜ     :                              Action

variable
  ac : Action

data Regular : Action → Set where
  w  : Regular w[ addr ↦ dat ]
  cp : Regular cp
  er : Regular er

data Write : Action → Set where
  w  : Write w[ addr ↦ dat ]

data Snapshot : Action → Set where
  f : Snapshot f

data RecoveryCrash : Action → Set where
  rᶜ : RecoveryCrash rᶜ

data RegularSuccess : Action → Set where
  w : RegularSuccess w[ addr ↦ dat ]
  f : RegularSuccess f

data Regular×Snapshot : Action → Set where
  w  : Regular×Snapshot w[ addr ↦ dat ]
  cp : Regular×Snapshot cp
  er : Regular×Snapshot er
  f  : Regular×Snapshot f

data Regular×SnapshotCrash : Action → Set where
  wᶜ  : Regular×SnapshotCrash wᶜ[ addr ↦ dat ]
  fᶜ  : Regular×SnapshotCrash fᶜ
  cpᶜ : Regular×SnapshotCrash cpᶜ
  erᶜ : Regular×SnapshotCrash erᶜ

Trace = SnocList Action

variable
  ef  : Trace
  ef₁ : Trace
  ef₂ : Trace
  ef₃ : Trace
  frag     : Trace
  frag-w   : Trace
  frag-rᶜ  : Trace
  flist    : SnocList Action
  flist-w  : SnocList Action
  flist-rᶜ : SnocList Action

--Reflexive Transitive Closure
data RTC {A S : Set} (R : S → A → S → Set) : S → SnocList A → S → Set where
  ∅   : ∀ {s : S} → RTC R s [] s
  _•_ : ∀ {s t u : S} {acs : SnocList A} {ac : A}
      → RTC R s acs t → R t ac u → RTC R s (acs • ac) u

_++RTC_ : {A S : Set} {R : S → A → S → Set} {s t u : S} {ef₁ ef₂ : SnocList A}
        → RTC R s ef₁ t → RTC R t ef₂ u → RTC R s (ef₁ ⊙ ef₂) u
tc-s-t ++RTC ∅             = tc-s-t
tc-s-t ++RTC (tc-t-u • rr) = (tc-s-t ++RTC tc-t-u) • rr

splitRTC : {A S : Set} {R : S → A → S → Set} {s s' : S} → (splitOn : SnocList A) → {rest : SnocList A}
         → ( fr : RTC R s (splitOn ⊙ rest) s') → Σ[ s'' ∈ S ] Σ[ fr₁ ∈ RTC R s splitOn s'' ] Σ[ fr₂ ∈ RTC R s'' rest s' ] (fr ≡ (fr₁ ++RTC fr₂))
splitRTC ef₁ {rest = []}                t = (_ , t , ∅ , refl)
splitRTC ef₁ {rest = (ef₂ • ac)} (t • rr) with splitRTC ef₁ t
...                                       | s'' , t₁ , t₂ , refl = s'' , t₁ , t₂ • rr , refl

data OneRecovery : Trace → Set where
  wᶜ     : {tr₁ tr₂ tr₃ : Trace} → All Regular×Snapshot tr₁ → All Regular tr₂ → All RecoveryCrash tr₃
         → OneRecovery (tr₁ ⊙ ([] • f ⊙ tr₂) ⊙ ([] • wᶜ[ addr ↦ dat ] ⊙ tr₃ • r))
  fᶜ     : {tr₁ tr₂ tr₃ : Trace} → All Regular×Snapshot tr₁ → All Regular tr₂ → All RecoveryCrash tr₃
         → OneRecovery (tr₁ ⊙ ([] • f ⊙ tr₂) ⊙ ([] • fᶜ ⊙ tr₃ • r))
  wᶜ-nof : {tr₂ tr₃ : Trace} → All Regular tr₂ → All RecoveryCrash tr₃
         → OneRecovery (tr₂ ⊙ ([] • wᶜ[ addr ↦ dat ] ⊙ tr₃ • r))
  fᶜ-nof : {tr₂ tr₃ : Trace} → All Regular tr₂ → All RecoveryCrash tr₃
         → OneRecovery (tr₂ ⊙ ([] • fᶜ ⊙ tr₃ • r))

data MultiRecovery : Trace → Set where
  init : {tr : Trace} → All RecoveryCrash tr → MultiRecovery (tr • r)
  one  : {tr₁ tr₂ : Trace} → MultiRecovery tr₁ → OneRecovery tr₂ → MultiRecovery (tr₁ ⊙ tr₂)

data 1RFrags {S : Set} {R : S → Action → S → Set} : {s s' : S} {tr : Trace} → OneRecovery tr → RTC R s tr s' → Set where
  wᶜ     : {tr₁ tr₂ tr₃ : Trace} {all₁ : All Regular×Snapshot tr₁} {all₂ : All Regular tr₂} {all₃ : All RecoveryCrash tr₃}
         → {s₁ s₂ s₃ s₄ : S} (fr₁ : RTC R s₁ tr₁ s₂) (fr₂ : RTC R s₂ ([] • f ⊙ tr₂) s₃) (fr₃ : RTC R s₃ ([] • wᶜ[ addr ↦ dat ] ⊙ tr₃ • r) s₄)
         → 1RFrags (wᶜ all₁ all₂ all₃) (fr₁ ++RTC fr₂ ++RTC fr₃)
  fᶜ     : {tr₁ tr₂ tr₃ : Trace} {all₁ : All Regular×Snapshot tr₁} {all₂ : All Regular tr₂} {all₃ : All RecoveryCrash tr₃}
         → {s₁ s₂ s₃ s₄ : S} (fr₁ : RTC R s₁ tr₁ s₂) (fr₂ : RTC R s₂ ([] • f ⊙ tr₂) s₃) (fr₃ : RTC R s₃ ([] • fᶜ ⊙ tr₃ • r) s₄)
         → 1RFrags (fᶜ all₁ all₂ all₃) (fr₁ ++RTC fr₂ ++RTC fr₃)
  wᶜ-nof : {tr₂ tr₃ : Trace} {all₂ : All Regular tr₂} {all₃ : All RecoveryCrash tr₃}
         → {s₂ s₃ s₄ : S} (fr₂ : RTC R s₂ tr₂ s₃) (fr₃ : RTC R s₃ ([] • wᶜ[ addr ↦ dat ] ⊙ tr₃ • r) s₄)
         → 1RFrags (wᶜ-nof all₂ all₃) (fr₂ ++RTC fr₃)
  fᶜ-nof : {tr₂ tr₃ : Trace} {all₂ : All Regular tr₂} {all₃ : All RecoveryCrash tr₃}
         → {s₂ s₃ s₄ : S} (fr₂ : RTC R s₂ tr₂ s₃) (fr₃ : RTC R s₃ ([] • fᶜ ⊙ tr₃ • r) s₄)
         → 1RFrags (fᶜ-nof all₂ all₃) (fr₂ ++RTC fr₃)

view1R : {tr : Trace} (1r : OneRecovery tr) {S : Set} {R : S → Action → S → Set} {s s' : S} (fr : RTC R s tr s') → 1RFrags 1r fr
view1R (wᶜ {tr₁ = tr₁} {tr₂ = tr₂} {tr₃ = tr₃} all₁ all₂ all₃) {s = s₁} {s' = s₄} fr
  with splitRTC (tr₁ ⊙ ([] • f ⊙ tr₂)) {rest = [] • wᶜ[ _ ↦ _ ] ⊙ tr₃ • r} fr
...  | s₃ , fr-l , fr₃ , refl with splitRTC tr₁ {rest = [] • f ⊙ tr₂} fr-l
...  | s₂ , fr₁  , fr₂ , refl = wᶜ fr₁ fr₂ fr₃
view1R (fᶜ {tr₁ = tr₁} {tr₂ = tr₂} {tr₃ = tr₃} all₁ all₂ all₃) {s = s₁} {s' = s₄} fr
  with splitRTC (tr₁ ⊙ ([] • f ⊙ tr₂)) {rest = [] • fᶜ ⊙ tr₃ • r} fr
...  | s₃ , fr-l , fr₃ , refl with splitRTC tr₁ {rest = [] • f ⊙ tr₂} fr-l
...  | s₂ , fr₁  , fr₂ , refl = fᶜ fr₁ fr₂ fr₃
view1R (wᶜ-nof {tr₂ = tr₂} {tr₃ = tr₃} all₂ all₃) fr with splitRTC tr₂ fr
...  | _ , fr₁ , fr₂ , refl = wᶜ-nof fr₁ fr₂
view1R (fᶜ-nof {tr₂ = tr₂} {tr₃ = tr₃} all₂ all₃) fr with splitRTC tr₂ fr
...  | _ , fr₁ , fr₂ , refl = fᶜ-nof fr₁ fr₂

data MRFrags {S : Set} {R : S → Action → S → Set} : {s s' : S} {tr : Trace} → MultiRecovery tr → RTC R s tr s' → Set where
  init : {tr : Trace} {all : All RecoveryCrash tr} {s s' : S} (fr : RTC R s (tr • r) s') → MRFrags (init all) fr
  one  : {tr₁ : Trace} {mr : MultiRecovery tr₁} {s₁ s₂ : S} {fr₁ : RTC R s₁ tr₁ s₂} → MRFrags mr fr₁
       → {tr₂ : Trace} {1r : OneRecovery   tr₂} {s₃    : S} (fr₂ : RTC R s₂ tr₂ s₃) → 1RFrags 1r fr₂ → MRFrags (one mr 1r) (fr₁ ++RTC fr₂)

viewMR : {tr : Trace} (mr : MultiRecovery tr) {S : Set} {R : S → Action → S → Set} {s s' : S} (fr : RTC R s tr s') → MRFrags mr fr
viewMR (init all) fr = init fr
viewMR (one  {tr₁ = tr₁} mr all) fr with splitRTC tr₁ fr
...  | _ , fr-l , fr-r , refl = one  (viewMR mr fr-l) fr-r (view1R all fr-r)

lastr : {S : Set} {s s' : S} {R : S → Action → S → Set} {tr : Trace} (mr : MultiRecovery tr)
      → (fr : RTC R s tr s') → (frs : MRFrags mr fr) → Σ[ s'' ∈ S ] (R s'' r s')
lastr .(init _) .fr (init fr) with fr
... | _ • x =  _ , x
lastr ._ ._ (one _ ._ (wᶜ _ _ (fr₃ • x))) = _ , x
lastr ._ ._ (one _ ._ (fᶜ _ _ (fr₃ • x))) = _ , x
lastr ._ ._ (one _ ._ (wᶜ-nof _ (fr₃ • x))) = _ , x
lastr ._ ._ (one _ ._ (fᶜ-nof _ (fr₃ • x))) = _ , x

SnapshotConsistency : {S : Set} {s s' : S} {R : S → Action → S → Set} (ER : S → S → Set)
                      {tr : Trace} → (1r : OneRecovery tr) → (fr : RTC R s tr s') → 1RFrags 1r fr → Set
SnapshotConsistency ER ._ ._ (wᶜ     {s₂ = s₂} {s₄ = s₄} _ _ _) = ER s₂ s₄
SnapshotConsistency ER ._ ._ (fᶜ     {s₂ = s₂} {s₃} {s₄} _ _ _) = ER s₃ s₄ ⊎ ER s₂ s₄
SnapshotConsistency ER ._ ._ (wᶜ-nof {s₂ = s₂} {s₄ = s₄}   _ _) = ER s₂ s₄
SnapshotConsistency ER ._ ._ (fᶜ-nof {s₂ = s₂} {s₃} {s₄}   _ _) = ER s₃ s₄ ⊎ ER s₂ s₄

module Spec where

  record State : Set where
    field
      volatile : Addr → Data
      stable   : Addr → Data
      w-count  : ℕ

  Init : State → Set
  Init s = (addr : Addr) → (State.stable s addr ≡ defaultData)

  variable
    t  : State
    t' : State

  update : (Addr → Data) → ℕ → Addr → Data → (Addr → Data)
  update s wcnt addr dat i with (addr ≤?MAXADDR) ∧ (wcnt ≤?MAXWCNT)
  update s wcnt addr dat i | false = s i
  update s wcnt addr dat i | true with addr ≟ i
  update s wcnt addr dat i | true | true  = dat
  update s wcnt addr dat i | true | false = s i

  data Step (s s' : State) : Action → Set where
    w   : update (State.volatile s) (State.w-count s) addr dat ≐ State.volatile s'
        → State.stable s ≐ State.stable s'
        → suc (State.w-count s) ≡ State.w-count s'
        → Step s s' w[ addr ↦ dat ]
    f   : State.volatile s ≐ State.volatile s'
        → State.volatile s ≐ State.stable s'
        → State.w-count s' ≡ zero
        → Step s s' f
    r   : State.stable s ≐ State.volatile s'
        → State.stable s ≐ State.stable s'
        → State.w-count s' ≡ zero
        → Step s s' r
    wᶜ  : State.stable s ≐ State.stable s'
        → Step s s' (wᶜ[ addr ↦ dat ])
    fᶜ  : State.volatile s ≐ State.stable s' ⊎ State.stable s ≐ State.stable s'
        → Step s s' fᶜ
    rᶜ  : State.stable s ≐ State.stable s'
        → Step s s' rᶜ
    cp  : State.volatile s ≐ State.volatile s'
        → State.stable s ≐ State.stable s'
        → State.w-count s ≡ State.w-count s'
        → Step s s' cp
    er  : State.volatile s ≐ State.volatile s'
        → State.stable s ≐ State.stable s'
        → State.w-count s ≡ State.w-count s'
        → Step s s' er
    cpᶜ : State.stable s ≐ State.stable s' → Step s s' cpᶜ
    erᶜ : State.stable s ≐ State.stable s' → Step s s' erᶜ

  _⟦_⟧▸_ : State → Action → State → Set
  s ⟦ ac ⟧▸ s' = Step s s' ac

  _⟦_⟧*▸_ = RTC  _⟦_⟧▸_

  record StbP (ac : Action) : Set where --Stability Reserving Actions
    field
      preserve : {s s' : State} → s ⟦ ac ⟧▸ s' → (State.stable s ≐ State.stable s')

  instance
    stb-r   : StbP r
    stb-r   = record { preserve = λ{(r _ ss _) → ss} }
    stb-w   : StbP w[ addr ↦ dat ]
    stb-w   = record { preserve = λ{(w _ ss _ ) → ss} }
    stb-wᶜ  : StbP wᶜ[ addr ↦ dat ]
    stb-wᶜ  = record { preserve = λ{(wᶜ ss) → ss} }
    stb-rᶜ  : StbP rᶜ
    stb-rᶜ  = record { preserve = λ{(rᶜ ss) → ss} }
    stb-cp  : StbP cp
    stb-cp  = record { preserve = λ{(cp _ ss _) → ss}}
    stb-er  : StbP er
    stb-er  = record { preserve = λ{(er _ ss _) → ss}}
    stb-cpᶜ : StbP cpᶜ
    stb-cpᶜ = record { preserve = λ{(cpᶜ ss) → ss}}
    stb-erᶜ : StbP erᶜ
    stb-erᶜ = record { preserve = λ{(erᶜ ss) → ss}}

  idemₛ : {tr : Trace} → All StbP tr
        → ∀ {s s' : State} → s ⟦ tr ⟧*▸ s'
        → State.stable s ≐ State.stable s'
  idemₛ [] ∅ = λ{_ → refl}
  idemₛ (all ∷ x) (s2s'' • s''2s') =
    idemₛ all s2s'' <≐> StbP.preserve x s''2s'

  r→rs : Regular ac → Regular×Snapshot ac
  r→rs w = w
  r→rs cp = cp
  r→rs er = er

  n→sp : Regular ac → StbP ac
  n→sp w  = stb-w
  n→sp cp = stb-cp
  n→sp er = stb-er

  rᶜ→sp : RecoveryCrash ac → StbP ac
  rᶜ→sp rᶜ = stb-rᶜ

  SpecSC-wᶜ : ∀ {s₂ s₃ s₄ : State} {tr-w tr-rᶜ}
             → {{_ : All Regular tr-w}} {{_ : All RecoveryCrash tr-rᶜ}}
             → s₂ ⟦ [] • f ⊙ tr-w ⟧*▸ s₃ → s₃ ⟦ [] • wᶜ[ addr ↦ dat ] ⊙ tr-rᶜ • r ⟧*▸ s₄
             → State.volatile s₂ ≐ State.volatile s₄
  SpecSC-wᶜ {{ all₂ }} {{ all₃ }} s₂▸s₃ (s₃▹ • r sv _ _)
        with splitRTC ([] • f) s₂▸s₃ | splitRTC ([] • wᶜ[ _ ↦ _ ]) s₃▹
  ...      | s₂' , ∅ • (f vv vs _) , s₂'▸s₃ , _ | s₃' , ∅ • (wᶜ ss) , s₃'▸s₄▹ , _ =
               vs <≐> idemₛ (mapAll n→sp  all₂) s₂'▸s₃  <≐>
               ss <≐> idemₛ (mapAll rᶜ→sp all₃) s₃'▸s₄▹ <≐> sv

  SpecSC-wᶜ-nof : ∀ {s₁ s₂ s₃ s₄ : State} {tr-w tr-rᶜ}
                → {{_ : All Regular tr-w}} {{_ : All RecoveryCrash tr-rᶜ}}
                → s₁ ⟦ r ⟧▸ s₂ → s₂ ⟦ tr-w ⟧*▸ s₃ → s₃ ⟦ [] • wᶜ[ addr ↦ dat ] ⊙ tr-rᶜ • r ⟧*▸ s₄
                → State.volatile s₂ ≐ State.volatile s₄
  SpecSC-wᶜ-nof {{ all₂ }} {{ all₃ }} (r sv' ss' _) s₂▸s₃ (s₃▹ • r sv _ _)
           with splitRTC ([] • wᶜ[ _ ↦ _ ]) s₃▹
  ...         | s₃' , ∅ • (wᶜ ss) , s₃'▸s₄▹ , _ =
                  sym-≐ sv' <≐> ss' <≐> idemₛ (mapAll n→sp  all₂) s₂▸s₃  <≐>
                  ss <≐> idemₛ (mapAll rᶜ→sp all₃) s₃'▸s₄▹ <≐> sv

  SpecSC-fᶜ : ∀ {s₂ s₃ s : State} {tr-w tr-rᶜ}
             → {{_ : All Regular tr-w}} {{_ : All RecoveryCrash tr-rᶜ}}
             → s₂ ⟦ ([] • f) ⊙ tr-w ⟧*▸ s₃ → s₃ ⟦ ([] • fᶜ) ⊙ tr-rᶜ • r ⟧*▸ s
             → State.volatile s₃ ≐ State.volatile s ⊎ State.volatile s₂ ≐ State.volatile s
  SpecSC-fᶜ {{all₁}} {{all₂}} s₂▸s₃ (s₃▸s • r sv ss _)
        with splitRTC ([] • f) s₂▸s₃ | splitRTC ([] • fᶜ) s₃▸s
  ...      | _ , ∅ • f vv vs _ , ▸s₃ , _ | s₃' , ∅ • fᶜ (inj₁ vsᶜ) , s₃'▸s , _ =
               inj₁ $ vsᶜ <≐> idemₛ (mapAll rᶜ→sp all₂) s₃'▸s <≐> sv
  ...      | _ , ∅ • f vv vs _ , ▸s₃ , _ | s₃' , ∅ • fᶜ (inj₂ ssᶜ) , s₃'▸s , _ =
               inj₂ $ vs <≐>
               idemₛ (mapAll n→sp all₁) ▸s₃ <≐> ssᶜ <≐>
               idemₛ (mapAll rᶜ→sp all₂) s₃'▸s <≐> sv

  SpecSC-fᶜ-nof : ∀ {s₁ s₂ s₃ s₄ : State} {tr-w tr-rᶜ}
                → {{_ : All Regular tr-w}} {{_ : All RecoveryCrash tr-rᶜ}}
                → s₁ ⟦ r ⟧▸ s₂ → s₂ ⟦ tr-w ⟧*▸ s₃ → s₃ ⟦ [] • fᶜ ⊙ tr-rᶜ • r ⟧*▸ s₄
                → State.volatile s₃ ≐ State.volatile s₄ ⊎ State.volatile s₂ ≐ State.volatile s₄
  SpecSC-fᶜ-nof {{ all₂ }} {{ all₃ }} (r sv' ss' _) s₂▸s₃ (s₃▹ • r sv _ _)
           with splitRTC ([] • fᶜ) s₃▹
  ...         | s₃' , ∅ • fᶜ (inj₁ vsᶜ) , s₃'▸s , _ = inj₁ $ vsᶜ <≐> idemₛ (mapAll rᶜ→sp all₃) s₃'▸s <≐> sv
  ...         | s₃' , ∅ • fᶜ (inj₂ ssᶜ) , s₃'▸s , _ = inj₂ $ sym-≐ sv' <≐> ss' <≐>
                                                             idemₛ (mapAll n→sp  all₂) s₂▸s₃ <≐> ssᶜ <≐>
                                                             idemₛ (mapAll rᶜ→sp all₃) s₃'▸s <≐> sv

  SC : {t₀ t t' : State} {tr₀ tr : Trace} → (mr : MultiRecovery tr₀) → (1r : OneRecovery tr)
     → Init t₀ → (fr₀ : t₀ ⟦ tr₀ ⟧*▸ t) → MRFrags mr fr₀ → (fr : t ⟦ tr ⟧*▸ t') → (frs : 1RFrags 1r fr)
     → SnapshotConsistency (λ t t' → State.volatile t ≐ State.volatile t') 1r fr frs
  SC mr _ init-t₀ fr₀ frs₀ ._ (wᶜ {all₂ = all₂} {all₃} fr₁ fr₂ fr₃) = SpecSC-wᶜ {{all₂}} {{all₃}} fr₂ fr₃
  SC mr _ init-t₀ fr₀ frs₀ ._ (fᶜ {all₂ = all₂} {all₃} fr₁ fr₂ fr₃) = SpecSC-fᶜ {{all₂}} {{all₃}} fr₂ fr₃
  SC mr _ init-t₀ fr₀ frs₀ ._ (wᶜ-nof {all₂ = all₂} {all₃} fr₂ fr₃) = SpecSC-wᶜ-nof {{all₂}} {{all₃}} (proj₂ (lastr mr fr₀ frs₀)) fr₂ fr₃
  SC mr _ init-t₀ fr₀ frs₀ ._ (fᶜ-nof {all₂ = all₂} {all₃} fr₂ fr₃) = SpecSC-fᶜ-nof {{all₂}} {{all₃}} (proj₂ (lastr mr fr₀ frs₀)) fr₂ fr₃

open Spec hiding (SC)

module Prog
  (runSpec : (t : State) (ac : Action) → ∃[ t' ] (t ⟦ ac ⟧▸ t'))
  (RawStateᴾ : Set) (_⟦_⟧ᴿ▸_ : RawStateᴾ → Action → RawStateᴾ → Set)
  (RI CI : RawStateᴾ → Set)
  (AR CR : RawStateᴾ → State → Set)
  (RIRI : {s s' : RawStateᴾ} {ac : Action} → Regular×Snapshot ac → s ⟦ ac ⟧ᴿ▸ s' → RI s → RI s')
  (ARAR : {s s' : RawStateᴾ} {t t' : State} {ac : Action} → Regular×Snapshot ac
        → s ⟦ ac ⟧ᴿ▸ s' → t ⟦ ac ⟧▸ t' → RI s × AR s t → AR s' t')
  (RICI : {s s' : RawStateᴾ} {ac : Action} → Regular×SnapshotCrash ac → s ⟦ ac ⟧ᴿ▸ s' → RI s → CI s')
  (ARCR : {s s' : RawStateᴾ} {t t' : State} {ac : Action} → Regular×SnapshotCrash ac
        → s ⟦ ac ⟧ᴿ▸ s' → t ⟦ ac ⟧▸ t' → RI s × AR s t → CR s' t')
  (CIRI : {s s' : RawStateᴾ} → s ⟦ r ⟧ᴿ▸ s' → CI s → RI s')
  (CRAR : {s s' : RawStateᴾ} {t t' : State} → s ⟦ r ⟧ᴿ▸ s' → t ⟦ r ⟧▸ t' → CI s × CR s t → AR s' t')
  (CICI : {s s' : RawStateᴾ} → s ⟦ rᶜ ⟧ᴿ▸ s' → CI s → CI s')
  (CRCR : {s s' : RawStateᴾ} {t t' : State} → s ⟦ rᶜ ⟧ᴿ▸ s' → t ⟦ rᶜ ⟧▸ t' → CI s × CR s t → CR s' t')
  (read : RawStateᴾ → Addr → Data)
  (AR⇒ObsEquiv : {s : RawStateᴾ} {t : State} → RI s × AR s t → read s ≐ State.volatile t)
  (Initᴿ : RawStateᴾ → Set)
  (initᴿ-CI : (s : RawStateᴾ) → Initᴿ s → CI s)
  (initᴿ-CR : (s : RawStateᴾ) → Initᴿ s → (t : State) → Init t → CR s t)
  (t-init : Σ[ t ∈ State ] Init t)
  where

  variable
    rs    : RawStateᴾ
    rs₁   : RawStateᴾ
    rinv  : RI rs
    cinv  : CI rs
    rs'   : RawStateᴾ
    rs''  : RawStateᴾ
    rs''' : RawStateᴾ
    rinv' : RI rs'
    cinv' : CI rs'

  _⟦_⟧ᴿ*▸_ = RTC _⟦_⟧ᴿ▸_

  data Inv (rs : RawStateᴾ) : Set where
    normal : RI rs → Inv rs
    crash  : CI rs → Inv rs

  Stateᴾ : Set
  Stateᴾ = Σ[ rs ∈ RawStateᴾ ] Inv rs

  data Initᴾ : Stateᴾ → Set where
    init : Initᴿ rs → Initᴾ (rs , crash cinv)

  variable
    s    : Stateᴾ
    s'   : Stateᴾ
    s''  : Stateᴾ
    s''' : Stateᴾ

  data _⟦_⟧ᴾ▸_ : Stateᴾ → Action → Stateᴾ → Set where
    w   : rs ⟦ w[ addr ↦ dat ] ⟧ᴿ▸ rs'  → (rs , normal rinv) ⟦ w[ addr ↦ dat ] ⟧ᴾ▸ (rs' , normal rinv')
    f   : rs ⟦ f   ⟧ᴿ▸ rs'              → (rs , normal rinv) ⟦ f  ⟧ᴾ▸ (rs' , normal rinv')
    wᶜ  : rs ⟦ wᶜ[ addr ↦ dat ] ⟧ᴿ▸ rs' → (rs , normal rinv) ⟦ wᶜ[ addr ↦ dat ] ⟧ᴾ▸ (rs' , crash  cinv')
    fᶜ  : rs ⟦ fᶜ  ⟧ᴿ▸ rs'              → (rs , normal rinv) ⟦ fᶜ ⟧ᴾ▸ (rs' , crash  cinv')
    rᶜ  : rs ⟦ rᶜ  ⟧ᴿ▸ rs'              → (rs , crash  cinv) ⟦ rᶜ ⟧ᴾ▸ (rs' , crash  cinv')
    r   : rs ⟦ r   ⟧ᴿ▸ rs'              → (rs , crash  cinv) ⟦ r  ⟧ᴾ▸ (rs' , normal rinv')
    cp  : rs ⟦ cp  ⟧ᴿ▸ rs'              → (rs , normal rinv) ⟦ cp ⟧ᴾ▸ (rs' , normal rinv')
    er  : rs ⟦ er  ⟧ᴿ▸ rs'              → (rs , normal rinv) ⟦ er ⟧ᴾ▸ (rs' , normal rinv')
    cpᶜ : rs ⟦ cpᶜ ⟧ᴿ▸ rs'              → (rs , normal rinv) ⟦ cpᶜ ⟧ᴾ▸ (rs' , crash cinv')
    erᶜ : rs ⟦ erᶜ ⟧ᴿ▸ rs'              → (rs , normal rinv) ⟦ erᶜ ⟧ᴾ▸ (rs' , crash cinv')

  _⟦_⟧ᴾ*▸_ = RTC  _⟦_⟧ᴾ▸_

  lift-n×s : {tr : Trace} {{_ : All Regular×Snapshot tr}} → rs ⟦ tr ⟧ᴿ*▸ rs' →
             ∃[ rinv' ] ((rs , normal rinv) ⟦ tr ⟧ᴾ*▸ (rs' , normal rinv'))
  lift-n×s ∅ = _ , ∅
  lift-n×s {{all ∷ w}} (rs*▸rs'' • rs''▸rs') =
    let (rinv'' , s*▸s'') = lift-n×s {{all}} rs*▸rs''
    in  RIRI w rs''▸rs' rinv'' , s*▸s'' • w rs''▸rs'
  lift-n×s {{all ∷ f}} (rs*▸rs'' • rs''▸rs') =
    let (rinv'' , s*▸s'') = lift-n×s {{all}} rs*▸rs''
    in  RIRI f rs''▸rs' rinv'' , s*▸s'' • f rs''▸rs'
  lift-n×s {{all ∷ cp}} (rs*▸rs'' • rs''▸rs') =
    let (rinv'' , s*▸s'') = lift-n×s {{all}} rs*▸rs''
    in  RIRI cp rs''▸rs' rinv'' , s*▸s'' • cp rs''▸rs'
  lift-n×s {{all ∷ er}} (rs*▸rs'' • rs''▸rs') =
    let (rinv'' , s*▸s'') = lift-n×s {{all}} rs*▸rs''
    in  RIRI er rs''▸rs' rinv'' , s*▸s'' • er rs''▸rs'

  lift-n : {tr : Trace} {{_ : All Regular tr}} → rs ⟦ tr ⟧ᴿ*▸ rs'
         → ∃[ rinv' ] ((rs , normal rinv) ⟦ tr ⟧ᴾ*▸ (rs' , normal rinv'))
  lift-n {{all}} rs*▸rs' =
    lift-n×s {{(mapAll (λ{w → w; cp → cp; er → er}) all)}} rs*▸rs'

  lift-rᶜ : {tr : Trace} {{_ : All RecoveryCrash tr}} → rs ⟦ tr ⟧ᴿ*▸ rs' →
            ∃[ cinv' ] ((rs , crash cinv) ⟦ tr ⟧ᴾ*▸ (rs' , crash cinv'))
  lift-rᶜ ∅ = _ , ∅
  lift-rᶜ {{all ∷ rᶜ}} (rs*▸rs'' • rs''▸rs') =
    let (cinv'' , s*▸s'') = lift-rᶜ {{all}} rs*▸rs''
    in  CICI rs''▸rs' cinv'' , s*▸s'' • rᶜ rs''▸rs'

  lift-mr : {tr : Trace} (mr : MultiRecovery tr) (fr : rs ⟦ tr ⟧ᴿ*▸ rs') → MRFrags mr fr → Initᴿ rs
          → ∃[ cinv ] ∃[ rinv' ] let s = (rs , crash cinv) in (s ⟦ tr ⟧ᴾ*▸ (rs' , normal rinv')) × Initᴾ s
  lift-mr ._ ._ (init {all = all} fr) init-rs with fr
  ... | fr₀ • rr with lift-rᶜ {cinv = initᴿ-CI _ init-rs} {{all}} fr₀
  ... | cinv₀ , fr₀ᴾ = _ , CIRI rr cinv₀ , fr₀ᴾ • r rr , init init-rs
  lift-mr ._ ._ (one frs₀ fr frs) init-rs with lift-mr _ _ frs₀ init-rs
  lift-mr ._ ._ (one frs₀ ._ (wᶜ {tr₃ = tr₃} {all₁ = all₁} {all₂} {all₃} fr₁ fr₂ fr₃)) init-rs | cinv₀ , rinv₀ , fr₀ᴾ , init-s with splitRTC ([] • (wᶜ[ _ ↦ _ ])) {rest = (tr₃ • r)} fr₃
  ...   | rs'' , ∅ • s₃▸s₃' , s₃'▸r • r▸rs' , eq with lift-n×s {rinv = rinv₀} {{all₁}} fr₁
  ...   | rinv₁ , frP₁ with lift-n×s {rinv = rinv₁} {{ ([] ∷ f) ++All mapAll r→rs all₂ }} fr₂
  ...   | rinv₂ , frP₂ with RICI wᶜ s₃▸s₃' rinv₂
  ...   | cinv₂' with lift-rᶜ {cinv = cinv₂'} {{all₃}} s₃'▸r
  ...   | cinv₃ , frP₃ with CIRI r▸rs' cinv₃
  ...   | rinv₄  = cinv₀ , rinv₄ ,  fr₀ᴾ ++RTC (frP₁ ++RTC frP₂ ++RTC ((∅ • wᶜ s₃▸s₃') ++RTC (frP₃ • r r▸rs'))), init-s
  lift-mr ._ ._ (one frs₀ ._ (fᶜ {tr₃ = tr₃} {all₁ = all₁} {all₂} {all₃} fr₁ fr₂ fr₃)) init-rs | cinv₀ , rinv₀ , fr₀ᴾ , init-s with splitRTC ([] • fᶜ) {rest = (tr₃ • r)} fr₃
  ...   | rs'' , ∅ • s₃▸s₃' , s₃'▸r • r▸rs' , eq with lift-n×s {rinv = rinv₀} {{all₁}} fr₁
  ...   | rinv₁ , frP₁ with lift-n×s {rinv = rinv₁} {{ ([] ∷ f) ++All mapAll r→rs all₂ }} fr₂
  ...   | rinv₂ , frP₂ with RICI fᶜ s₃▸s₃' rinv₂
  ...   | cinv₂' with lift-rᶜ {cinv = cinv₂'} {{all₃}} s₃'▸r
  ...   | cinv₃ , frP₃ with CIRI r▸rs' cinv₃
  ...   | rinv₄  = cinv₀ , rinv₄ ,  fr₀ᴾ ++RTC (frP₁ ++RTC frP₂ ++RTC ((∅ • fᶜ s₃▸s₃') ++RTC (frP₃ • r r▸rs'))), init-s
  lift-mr ._ ._ (one frs₀ ._ (wᶜ-nof {tr₃ = tr₃} {all₂ = all₂} {all₃} fr₂ fr₃)) init-rs | cinv₀ , rinv₀ , fr₀ᴾ , init-s with splitRTC ([] • wᶜ[ _ ↦ _ ]) {rest = (tr₃ • r)} fr₃
  ...   | rs'' , ∅ • s₃▸s₃' , s₃'▸r • r▸rs' , eq with lift-n×s {rinv = rinv₀} {{ mapAll r→rs all₂ }} fr₂
  ...   | rinv₂ , frP₂ with RICI wᶜ s₃▸s₃' rinv₂
  ...   | cinv₂' with lift-rᶜ {cinv = cinv₂'} {{all₃}} s₃'▸r
  ...   | cinv₃ , frP₃ with CIRI r▸rs' cinv₃
  ...   | rinv₄  = cinv₀ , rinv₄ ,  fr₀ᴾ ++RTC (frP₂ ++RTC ((∅ • wᶜ s₃▸s₃') ++RTC (frP₃ • r r▸rs'))), init-s
  lift-mr ._ ._ (one frs₀ ._ (fᶜ-nof {tr₃ = tr₃} {all₂ = all₂} {all₃} fr₂ fr₃)) init-rs | cinv₀ , rinv₀ , fr₀ᴾ , init-s with splitRTC ([] • fᶜ) {rest = (tr₃ • r)} fr₃
  ...   | rs'' , ∅ • s₃▸s₃' , s₃'▸r • r▸rs' , eq with lift-n×s {rinv = rinv₀} {{ mapAll r→rs all₂ }} fr₂
  ...   | rinv₂ , frP₂ with RICI fᶜ s₃▸s₃' rinv₂
  ...   | cinv₂' with lift-rᶜ {cinv = cinv₂'} {{all₃}} s₃'▸r
  ...   | cinv₃ , frP₃ with CIRI r▸rs' cinv₃
  ...   | rinv₄  = cinv₀ , rinv₄ ,  fr₀ᴾ ++RTC (frP₂ ++RTC ((∅ • fᶜ s₃▸s₃') ++RTC (frP₃ • r r▸rs'))), init-s

  ObsEquiv : Stateᴾ → State → Set
  ObsEquiv (rs , _) t = read rs ≐ State.volatile t

  data SR : Stateᴾ → State → Set where
    ar : AR rs t → SR (rs , normal rinv) t
    cr : CR rs t → SR (rs , crash  cinv) t

  simSR : SR s t → s ⟦ ac ⟧ᴾ▸ s' → ∃[ t' ] (t ⟦ ac ⟧▸ t' × SR s' t')
  simSR {s , normal rinv} {t} (ar AR-rs-t) (w {addr = addr} {dat = dat} rs▸rs') =
    let (t' , t▸t') = runSpec t w[ addr ↦ dat ]
    in   t' , t▸t' , ar (ARAR w rs▸rs' t▸t' (rinv , AR-rs-t))
  simSR {s , normal rinv} {t} (ar AR-rs-t) (f rs▸rs')  =
    let (t' , t▸t') = runSpec t f
    in   t' , t▸t' , ar (ARAR f rs▸rs' t▸t' (rinv , AR-rs-t))
  simSR {s , normal rinv} {t} (ar AR-rs-t) (wᶜ {addr = addr} {dat = dat} rs▸rs') =
    let (t' , t▸t') = runSpec t wᶜ[ addr ↦ dat ]
    in   t' , t▸t' , cr (ARCR wᶜ rs▸rs' t▸t' (rinv , AR-rs-t))
  simSR {s , normal rinv} {t} (ar AR-rs-t) (fᶜ rs▸rs') =
    let (t' , t▸t') = runSpec t fᶜ
    in   t' , t▸t' , cr (ARCR fᶜ rs▸rs' t▸t' (rinv , AR-rs-t))
  simSR {s , crash  cinv} {t} (cr CR-rs-t) (rᶜ rs▸rs') =
    let (t' , t▸t') = runSpec t rᶜ
    in   t' , t▸t' , cr (CRCR    rs▸rs' t▸t' (cinv , CR-rs-t))
  simSR {s , crash  cinv} {t} (cr CR-rs-t) (r rs▸rs')  =
    let (t' , t▸t') = runSpec t r
    in   t' , t▸t' , ar (CRAR    rs▸rs' t▸t' (cinv , CR-rs-t))
  simSR {s , normal rinv} {t} (ar AR-rs-t) (cp rs▸rs')  =
    let (t' , t▸t') = runSpec t cp
    in   t' , t▸t' , ar (ARAR cp rs▸rs' t▸t' (rinv , AR-rs-t))
  simSR {s , normal rinv} {t} (ar AR-rs-t) (er rs▸rs')  =
    let (t' , t▸t') = runSpec t er
    in   t' , t▸t' , ar (ARAR er rs▸rs' t▸t' (rinv , AR-rs-t))
  simSR {s , normal rinv} {t} (ar AR-rs-t) (cpᶜ rs▸rs') =
    let (t' , t▸t') = runSpec t cpᶜ
    in   t' , t▸t' , cr (ARCR cpᶜ rs▸rs' t▸t' (rinv , AR-rs-t))
  simSR {s , normal rinv} {t} (ar AR-rs-t) (erᶜ rs▸rs') =
    let (t' , t▸t') = runSpec t erᶜ
    in   t' , t▸t' , cr (ARCR erᶜ rs▸rs' t▸t' (rinv , AR-rs-t))

  runSimSR : SR s t → s ⟦ ef ⟧ᴾ*▸ s' → ∃[ t' ] (t ⟦ ef ⟧*▸ t' × SR s' t')
  runSimSR SR-s-t ∅                 = _ , ∅ , SR-s-t
  runSimSR SR-s-t (s*▸s'' • s''▸s') =
    let (t'' , t*▸t'' , SR-s''-t'') = runSimSR SR-s-t s*▸s''
        (t'  , t''▸t' , SR-s'-t'  ) = simSR SR-s''-t'' s''▸s'
    in  _ , (t*▸t'' • t''▸t') , SR-s'-t'

  Conformant-all : {tr : Trace} {s s' : Stateᴾ} → s ⟦ tr ⟧ᴾ*▸ s' → {t t' : State} → t ⟦ tr ⟧*▸ t' → Set
  Conformant-all {s' = s'} ∅         {t' = t'} ∅         = ⊤
  Conformant-all {s' = s'} (frP • _) {t' = t'} (frS • _) = Conformant-all frP frS × ObsEquiv s' t'

  Conformant-1R : {tr : Trace} (1r : OneRecovery tr)
                 → {s s' : Stateᴾ} (frP : s ⟦ tr ⟧ᴾ*▸ s') → 1RFrags 1r frP
                 → {t t' : State } (frS : t ⟦ tr ⟧*▸  t') → 1RFrags 1r frS → Set
  Conformant-1R ._ {s' = s'} ._ (wᶜ frP₁ frP₂ frP₃) {t' = t'} ._ (wᶜ frS₁ frS₂ frS₃) = Conformant-all (frP₁ ++RTC frP₂) (frS₁ ++RTC frS₂) × ObsEquiv s' t'
  Conformant-1R ._ {s' = s'} ._ (fᶜ frP₁ frP₂ frP₃) {t' = t'} ._ (fᶜ frS₁ frS₂ frS₃) = Conformant-all (frP₁ ++RTC frP₂) (frS₁ ++RTC frS₂) × ObsEquiv s' t'
  Conformant-1R ._ {s' = s'} ._ (wᶜ-nof  frP₂ frP₃) {t' = t'} ._ (wᶜ-nof  frS₂ frS₃) = Conformant-all frP₂ frS₂ × ObsEquiv s' t'
  Conformant-1R ._ {s' = s'} ._ (fᶜ-nof  frP₂ frP₃) {t' = t'} ._ (fᶜ-nof  frS₂ frS₃) = Conformant-all frP₂ frS₂ × ObsEquiv s' t'

  Conformant-all-intermediate : {s₁ s₂ s₃ : Stateᴾ} {t₁ t₂ t₃ : State} {tr tr' : Trace}
                                 (frP : s₁ ⟦ tr ⟧ᴾ*▸ s₂) (frS : t₁ ⟦ tr ⟧*▸ t₂) (frP' : s₂ ⟦ tr' ⟧ᴾ*▸ s₃) (frS' : t₂ ⟦ tr' ⟧*▸ t₃)
                               → Conformant-all (frP ++RTC frP') (frS ++RTC frS') → ObsEquiv s₁ t₁ → ObsEquiv s₂ t₂
  Conformant-all-intermediate ∅ ∅ _ _ conf oe = oe
  Conformant-all-intermediate (frP • sP) (frS • sS) ∅ ∅ conf oe = proj₂ conf
  Conformant-all-intermediate (frP • sP) (frS • sS) (frP' • sP') (frS' • sS') conf oe = Conformant-all-intermediate (frP • sP) (frS • sS) frP' frS' (proj₁ conf) oe

  conf-all++ : {s₁ s₂ s₃ : Stateᴾ} {t₁ t₂ t₃ : State} {tr tr' : Trace}
               (frP : s₁ ⟦ tr ⟧ᴾ*▸ s₂) (frS : t₁ ⟦ tr ⟧*▸ t₂) (frP' : s₂ ⟦ tr' ⟧ᴾ*▸ s₃) (frS' : t₂ ⟦ tr' ⟧*▸ t₃)
             → Conformant-all frP frS → Conformant-all frP' frS'
             → Conformant-all (frP ++RTC frP') (frS ++RTC frS')
  conf-all++ frP frS ∅ ∅ conf conf' = conf
  conf-all++ frP frS (frP' • p) (frS' • s) conf (conf' , oe) = conf-all++ frP frS frP' frS' conf conf' , oe

  Conformant : {tr : Trace} (mr : MultiRecovery tr)
                {s s' : Stateᴾ} (frP : s ⟦ tr ⟧ᴾ*▸ s') → MRFrags mr frP
              → {t t' : State } (frS : t ⟦ tr ⟧*▸  t') → MRFrags mr frS → Set
  Conformant (init _) {s' = s'} _ _ {t' = t'} _ _ = ObsEquiv s' t'
  Conformant (one mr 1r) .(_ ++RTC frP₂) (one {s₂ = s''} frPs frP₂ frPs₂) .(_ ++RTC frS₂) (one {s₂ = t''} frSs frS₂ frSs₂) =
    Conformant mr _ frPs _ frSs × ObsEquiv s'' t'' × Conformant-1R 1r frP₂ frPs₂ frS₂ frSs₂

  BC-all : {tr : Trace} → All Regular×Snapshot tr → {s s' : Stateᴾ} {t : State} →
           SR s t → ObsEquiv s t → (frP : s ⟦ tr ⟧ᴾ*▸ s') →
           Σ[ t' ∈ State ] Σ[ frS ∈ t ⟦ tr ⟧*▸ t' ] SR s' t' × ObsEquiv s' t' × Conformant-all frP frS
  BC-all [] sr oe-s-t ∅ = _ , ∅ , sr , oe-s-t , tt
  BC-all (all ∷ _) sr oe-s-t (frP • _) with BC-all all sr oe-s-t frP
  BC-all (all ∷ _) sr oe-s-t (frP • s''▸s') | t'' , frS'' , sr'' , oe'' , conf'' with simSR sr'' s''▸s'
  BC-all (all ∷ w) sr oe-s-t (frP • w {rinv' = rinv'} rs''▸s') | t'' , frS'' , sr'' , oe'' , conf'' | t' , t''▸t' , ar ar' =
    let oe' = AR⇒ObsEquiv (rinv' , ar') in t' , frS'' • t''▸t' , ar ar' , oe' , conf'' , oe'
  BC-all (all ∷ cp) sr oe-s-t (frP • cp {rinv' = rinv'} rs''▸s') | t'' , frS'' , sr'' , oe'' , conf'' | t' , t''▸t' , ar ar' =
    let oe' = AR⇒ObsEquiv (rinv' , ar') in t' , frS'' • t''▸t' , ar ar' , oe' , conf'' , oe'
  BC-all (all ∷ er) sr oe-s-t (frP • er {rinv' = rinv'} rs''▸s') | t'' , frS'' , sr'' , oe'' , conf'' | t' , t''▸t' , ar ar' =
    let oe' = AR⇒ObsEquiv (rinv' , ar') in t' , frS'' • t''▸t' , ar ar' , oe' , conf'' , oe'
  BC-all (all ∷ f) sr oe-s-t (frP • f {rinv' = rinv'} rs''▸s') | t'' , frS'' , sr'' , oe'' , conf'' | t' , t''▸t' , ar ar' =
    let oe' = AR⇒ObsEquiv (rinv' , ar') in t' , frS'' • t''▸t' , ar ar' , oe' , conf'' , oe'

  BC-1R : {tr : Trace} → (1r : OneRecovery tr) → {s s' : Stateᴾ} {t : State} →
          SR s t → ObsEquiv s t → (frP : s ⟦ tr ⟧ᴾ*▸ s') (frPs : 1RFrags 1r frP) →
          Σ[ t' ∈ State ] Σ[ frS ∈ t ⟦ tr ⟧*▸ t' ] Σ[ frSs ∈ 1RFrags 1r frS ] SR s' t' × ObsEquiv s' t' × Conformant-1R 1r frP frPs frS frSs
  BC-1R 1r sr s=t frP (wᶜ {all₁ = all₁} {all₂ = all₂} fr₁ fr₂ fr₃@(fr₃' • r {rinv' = rinv'} _))
     with BC-all all₁ sr s=t fr₁
  ... | t₁ , frS₁ , sr-s₁-t₁ , s₁=t₁ , conf₁
     with BC-all (([] ∷ f) ++All mapAll r→rs all₂) sr-s₁-t₁ s₁=t₁ fr₂
  ... | t₂ , frS₂ , sr-s₂-t₂ , s₂=t₂ , conf₂ with runSimSR sr-s₂-t₂ fr₃
  ... | t' , frS' , ar ar-s'-t' =
          let oe' = AR⇒ObsEquiv (rinv' , ar-s'-t')
          in  t' , frS₁ ++RTC frS₂ ++RTC frS' , wᶜ frS₁ frS₂ frS' , ar ar-s'-t' , oe' , conf-all++ fr₁ frS₁ fr₂ frS₂ conf₁ conf₂ , oe'
  BC-1R 1r sr s=t frP (fᶜ {all₁ = all₁} {all₂ = all₂} fr₁ fr₂ fr₃@(fr₃' • r {rinv' = rinv'} _))
     with BC-all all₁ sr s=t fr₁
  ... | t₁ , frS₁ , sr-s₁-t₁ , s₁=t₁ , conf₁
     with BC-all (([] ∷ f) ++All mapAll r→rs all₂) sr-s₁-t₁ s₁=t₁ fr₂
  ... | t₂ , frS₂ , sr-s₂-t₂ , s₂=t₂ , conf₂ with runSimSR sr-s₂-t₂ fr₃
  ... | t' , frS' , ar ar-s'-t' =
          let oe' = AR⇒ObsEquiv (rinv' , ar-s'-t')
          in  t' , frS₁ ++RTC frS₂ ++RTC frS' , fᶜ frS₁ frS₂ frS' , ar ar-s'-t' , oe' , conf-all++ fr₁ frS₁ fr₂ frS₂ conf₁ conf₂ , oe'
  BC-1R 1r sr s=t frP (wᶜ-nof {all₂ = all₂} fr₂ fr₃@(fr₃' • r {rinv' = rinv'} _))
     with BC-all (mapAll r→rs all₂) sr s=t fr₂
  ... | _ , frS₂ , sr-s₂-t₂ , s₂=t₂ , conf₂ with runSimSR sr-s₂-t₂ fr₃
  ... | t' , frS' , ar ar-s'-t' =
          let oe' = AR⇒ObsEquiv (rinv' , ar-s'-t')
          in  t' , frS₂ ++RTC frS' , wᶜ-nof frS₂ frS' , ar ar-s'-t' , oe' , conf₂ , oe'
  BC-1R 1r sr s=t frP (fᶜ-nof {all₂ = all₂} fr₂ fr₃@(fr₃' • r {rinv' = rinv'} _))
     with BC-all (mapAll r→rs all₂) sr s=t fr₂
  ... | _ , frS₂ , sr-s₂-t₂ , s₂=t₂ , conf₂ with runSimSR sr-s₂-t₂ fr₃
  ... | t' , frS' , ar ar-s'-t' =
          let oe' = AR⇒ObsEquiv (rinv' , ar-s'-t')
          in  t' , frS₂ ++RTC frS' , fᶜ-nof frS₂ frS' , ar ar-s'-t' , oe' , conf₂ , oe'

  BC-ind : {tr : Trace} (mr : MultiRecovery tr) {s s' : Stateᴾ} → Initᴾ s → (frP : s ⟦ tr ⟧ᴾ*▸ s') (frPs : MRFrags mr frP)
         → Σ[ t ∈ State ] Init t × Σ[ t' ∈ State ] SR s' t' × ObsEquiv s' t' × Σ[ frS ∈ t ⟦ tr ⟧*▸ t' ] Σ[ frSs ∈ MRFrags mr frS ] Conformant mr frP frPs frS frSs
  BC-ind (init all) {s = s₀} (init rs₀) (frP • rP@(r {rinv' = rinv'} rs)) frPs with runSimSR (cr (initᴿ-CR (proj₁ s₀) rs₀ (proj₁ t-init) (proj₂ t-init))) frP
  ... | t'' , frS , sr' with simSR sr' rP
  ... | t' , rS , (ar ar-rs'-t') =
          let eq = AR⇒ObsEquiv (rinv' , ar-rs'-t')
          in  proj₁ t-init , proj₂ t-init , t' , ar ar-rs'-t' , eq , frS • rS , init (frS • rS) , eq
  BC-ind (one mr x) init-s _ (one {mr = mr₁} {fr₁ = frP₁} frPs₁ {1r = 1r} frP₂ frPs₂) with BC-ind mr init-s _ frPs₁
  ... | t , init-t , t'' , sr'' , oe'' , frS₁ , frSs₁ , conf₁ with BC-1R 1r sr'' oe'' frP₂ frPs₂
  ... | t' , frS₂ , frSs₂ , sr' , oe' , conf₂ = t , init-t , t' , sr' , oe' , frS₁ ++RTC frS₂ , one frSs₁ frS₂ frSs₂ , conf₁ , oe'' , conf₂

  BC-mr : {tr : Trace} (mr : MultiRecovery tr) {s s' : Stateᴾ} → Initᴾ s → (frP : s ⟦ tr ⟧ᴾ*▸ s') → (frPs : MRFrags mr frP)
        → Σ[ t ∈ State ] Init t × Σ[ t' ∈ State ] Σ[ frS ∈ t ⟦ tr ⟧*▸ t' ] Σ[ frSs ∈ MRFrags mr frS ] Conformant mr frP frPs frS frSs
  BC-mr mr init-s frP frPs =
    let (t , init-t , t' , _ , _ , frS , frSs , conf) = BC-ind mr init-s frP frPs
    in  (t , init-t , t' , frS ,  frSs , conf)

  BC : {tr : Trace} (mr : MultiRecovery tr) {s s' : Stateᴾ} → Initᴾ s → (frP : s ⟦ tr ⟧ᴾ*▸ s') (frPs : MRFrags mr frP)
     → {tr' : Trace} {s'' : Stateᴾ} → All Regular×Snapshot tr' → (frP' : s' ⟦ tr' ⟧ᴾ*▸ s'')
     → Σ[ t ∈ State ] Init t × Σ[ t' ∈ State ] Σ[ frS ∈ t ⟦ tr ⟧*▸ t' ] Σ[ frSs ∈ MRFrags mr frS ] Σ[ t'' ∈ State ] Σ[ frS' ∈ t' ⟦ tr' ⟧*▸ t'' ]
       Conformant mr frP frPs frS frSs × Conformant-all frP' frS'
  BC mr init-s frP frPs all frP' =
    let (t , init-t , t' , sr' , oe' , frS , frSs , conf) = BC-ind mr init-s frP frPs
        (t'' , frS' , _ , _ , conf') = BC-all all sr' oe' frP'
    in  (t , init-t , t' , frS , frSs , t'' , frS' , conf , conf')

  SC : {s₀ s s' : Stateᴾ} {tr₀ tr : Trace} → (mr : MultiRecovery tr₀) → (1r : OneRecovery tr)
     → Initᴾ s₀ → (fr₀ : s₀ ⟦ tr₀ ⟧ᴾ*▸ s) → MRFrags mr fr₀ → (frP : s ⟦ tr ⟧ᴾ*▸ s') → (frPs : 1RFrags 1r frP)
     → SnapshotConsistency (λ{(rs , _) (rs' , _) → read rs ≐ read rs'}) 1r frP frPs
  SC mr 1r init-s₀ frP₀ frPs₀ frP frPs with BC-mr (one mr 1r) init-s₀ (frP₀ ++RTC frP) (one frPs₀ frP frPs)
  SC mr ._ init-s₀ frP₀ frPs₀ ._ (wᶜ frP₁ frP₂ frP₃) |
     t₀ , init-t₀ , t' , ._ , one frSs ._ (wᶜ {all₁ = all₁} {all₂ = all₂} {all₃ = all₃} frS₁ frS₂ frS₃) , (_ , oe-s-t , conf , oe-s'-t')
       = Conformant-all-intermediate frP₁ frS₁ frP₂ frS₂ conf oe-s-t <≐> SpecSC-wᶜ ⦃ all₂ ⦄ ⦃ all₃ ⦄ frS₂ frS₃ <≐> sym-≐ oe-s'-t'
  SC mr ._ init-s₀ frP₀ frPs₀ ._ (fᶜ frP₁ frP₂ frP₃) |
     t₀ , init-t₀ , t' , ._ , one frSs ._ (fᶜ {all₁ = all₁} {all₂ = all₂} {all₃ = all₃} frS₁ frS₂ frS₃) , (_ , oe-s-t , conf , oe-s'-t')
       with SpecSC-fᶜ {{all₂}} {{all₃}} frS₂ frS₃
  ...  | inj₁ req = inj₁ $ Conformant-all-intermediate (frP₁ ++RTC frP₂) (frS₁ ++RTC frS₂) ∅ ∅ conf oe-s-t <≐> req <≐> sym-≐ oe-s'-t'
  ...  | inj₂ req = inj₂ $ Conformant-all-intermediate frP₁ frS₁ frP₂ frS₂ conf oe-s-t <≐> req <≐> sym-≐ oe-s'-t'
  SC mr ._ init-s₀ frP₀ frPs₀ ._ (wᶜ-nof frP₂ frP₃) |
     t₀ , init-t₀ , t' , ._ , one {fr₁ = frS₀} frSs ._ (wᶜ-nof {all₂ = all₂} {all₃ = all₃} frS₂ frS₃) , (_ , oe-s-t , conf , oe-s'-t')
       = oe-s-t <≐> SpecSC-wᶜ-nof ⦃ all₂ ⦄ ⦃ all₃ ⦄ (proj₂ (lastr mr frS₀ frSs)) frS₂ frS₃ <≐> sym-≐ oe-s'-t'
  SC mr ._ init-s₀ frP₀ frPs₀ ._ (fᶜ-nof frP₂ frP₃) |
     t₀ , init-t₀ , t' , ._ , one frSs ._ (fᶜ-nof {all₂ = all₂} {all₃ = all₃} frS₂ frS₃) , (_ , oe-s-t , conf , oe-s'-t')
       with SpecSC-fᶜ-nof {{all₂}} {{all₃}} (proj₂ (lastr mr _ frSs)) frS₂ frS₃
  ...  | inj₁ req = inj₁ $ Conformant-all-intermediate frP₂ frS₂ ∅ ∅ conf oe-s-t <≐> req <≐> sym-≐ oe-s'-t'
  ...  | inj₂ req = inj₂ $ oe-s-t <≐> req <≐> sym-≐ oe-s'-t'

max_stars_repo_name: yunshengtw/scftl

max_issues_repo_name: yunshengtw/scftl

max_forks_repo_name: yunshengtw/scftl


text:
module IrrelevantModuleParameter .(A : Set) where

postulate
  a : A
-- cannot declare something of type A, since A is irrelevant

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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 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 ℓ₃) (x : A) (y : B x) →
                       cast (Σ A B) (Σ A' B') (x , y) ≡ (cast {ℓ = ℓ} {ℓ₁ = ℓ₂} A A' x , cast (B x) (B' (cast A A' x)) y)

{-# 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)

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

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

{-# REWRITE cast-List-nil #-}

{-# REWRITE cast-List-cons #-}

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

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

{-# REWRITE cast-Nat-zero #-}

{-# REWRITE cast-Nat-suc #-}

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

{-# REWRITE cast-Bool-true #-}

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

{-# REWRITE cast-Bool-false #-}

postulate cast-Unit : cast ⊤ ⊤ tt ≡ tt

{-# REWRITE cast-Unit #-}

{- non-diagonal cases -}

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

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

postulate cast-raise :  ∀ ℓ ℓ₁ → (A : Set ℓ₁) → cast (raise {ℓ = lsuc ℓ} (Set ℓ)) A (raise _) ≡ 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 #-}

{- Rules specific to Unk -}

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

postulate cast-Unk : (A : Set ℓ) (B : Set ℓ₁) (f : A) →
                        cast (Unk ℓ) B (box A f) ≡ cast A B f

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

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

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

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

proj : {A : Set ℓ₁} → Unk ℓ → A
proj {ℓ₁} {ℓ} {A} (box A' a') = cast {ℓ = ℓ} {ℓ₁ = ℓ₁} A' A a'

delta : Unk ℓ → Unk ℓ
delta {ℓ} x = proj {A = Unk ℓ → Unk ℓ} x x

omega : Unk (lsuc ℓ)
omega {ℓ} = delta {ℓ = lsuc ℓ} (box (Unk ℓ → Unk ℓ) (delta {ℓ = ℓ}))

max_stars_repo_name: kyoDralliam/exceptional-tt

max_issues_repo_name: kyoDralliam/exceptional-tt

max_forks_repo_name: kyoDralliam/exceptional-tt


text:
module Issue293b where

module M₁ (_ : Set₁) where

  postulate P : Set

module M₂ (_ : Set) where

  open M₁ Set

  p : P
  p = {!!}

  -- Previous agda2-goal-and-context:

  -- ------------------------
  -- Goal: M₁.P Set

  -- Current agda2-goal-and-context:

  -- ------------------------
  -- Goal: P

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Order morphisms
------------------------------------------------------------------------

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

open import Relation.Binary.Core

module Relation.Binary.Morphism where

------------------------------------------------------------------------
-- Re-export contents of morphisms

open import Relation.Binary.Morphism.Definitions public
open import Relation.Binary.Morphism.Structures public


text:
{-
This second-order term syntax was created from the following second-order syntax description:

syntax Monad | M

type
  T : 1-ary

term
  ret  : α  ->  T α
  bind : T α  α.(T β)  ->  T β | _>>=_ r10

theory
  (LU) a : α   b : α.(T β) |> bind (ret(a), x. b[x]) =  b[a]
  (RU) t : T α |> bind (t, x. ret(x)) = t
  (AS) t : T α  b : α.(T β)  c : β.(T γ) |> bind (bind (t, x.b[x]), y.c[y]) = bind (t, x. bind (b[x], y.c[y]))
-}

module Monad.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import Monad.Signature

private
  variable
    Γ Δ Π : Ctx
    α β : MT
    𝔛 : Familyₛ

-- Inductive term declaration
module M:Terms (𝔛 : Familyₛ) where

  data M : Familyₛ where
    var  : ℐ ⇾̣ M
    mvar : 𝔛 α Π → Sub M Π Γ → M α Γ

    ret   : M α Γ → M (T α) Γ
    _>>=_ : M (T α) Γ → M (T β) (α ∙ Γ) → M (T β) Γ

  infixr 10 _>>=_

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  Mᵃ : MetaAlg M
  Mᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (retₒ  ⋮ a)     → ret   a
      (bindₒ ⋮ a , b) → _>>=_ a b
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module Mᵃ = MetaAlg Mᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : M ⇾̣ 𝒜
    𝕊 : Sub M Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞 (ret   a)   = 𝑎𝑙𝑔 (retₒ  ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (_>>=_ a b) = 𝑎𝑙𝑔 (bindₒ ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ Mᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ M α Γ) → 𝕤𝕖𝕞 (Mᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (retₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (bindₒ ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ M ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : M ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ Mᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : M α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub M Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! (ret a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (_>>=_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
M:Syn : Syntax
M:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = M:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open M:Terms 𝔛 in record
    { ⊥ = M ⋉ Mᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax M:Syn public
open M:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands Mᵃ public
open import SOAS.Metatheory M:Syn public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A type for expressions over a raw ring.
------------------------------------------------------------------------

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

module Tactic.RingSolver.Core.Expression where

open import Data.Nat.Base using (ℕ)
open import Data.Fin.Base using (Fin)
open import Data.Vec.Base as Vec using (Vec)

open import Algebra

infixl 6 _⊕_
infixl 7 _⊗_
infixr 8 _⊛_

data Expr {a} (A : Set a) (n : ℕ) : Set a where
  Κ   : A → Expr A n                   -- Constant
  Ι   : Fin n → Expr A n               -- Variable
  _⊕_ : Expr A n → Expr A n → Expr A n -- Addition
  _⊗_ : Expr A n → Expr A n → Expr A n -- Multiplication
  _⊛_ : Expr A n → ℕ → Expr A n        -- Exponentiation
  ⊝_  : Expr A n → Expr A n            -- Negation

module Eval
  {ℓ₁ ℓ₂} (rawRing : RawRing ℓ₁ ℓ₂)
  (let open RawRing rawRing)
  {a} {A : Set a} (⟦_⟧ᵣ : A → Carrier) where

  open import Algebra.Operations.Ring rawRing

  ⟦_⟧ : ∀ {n} → Expr A n → Vec Carrier n → Carrier
  ⟦ Κ x   ⟧ ρ = ⟦ x ⟧ᵣ
  ⟦ Ι x   ⟧ ρ = Vec.lookup ρ x
  ⟦ x ⊕ y ⟧ ρ = ⟦ x ⟧ ρ + ⟦ y ⟧ ρ
  ⟦ x ⊗ y ⟧ ρ = ⟦ x ⟧ ρ * ⟦ y ⟧ ρ
  ⟦   ⊝ x ⟧ ρ = - ⟦ x ⟧ ρ
  ⟦ x ⊛ i ⟧ ρ = ⟦ x ⟧ ρ ^ i


text:
{-# OPTIONS --cubical #-}
module Exercises where

open import Part2
open import Part3
open import Part4
open import Part5


text:
-- Some basic structures and operations for dealing
-- with non-deterministic values.
--
-- @author Sergio Antoy, Michael Hanus, Steven Libby

module nondet where

open import bool
open import nat
open import list

infixr 8 _??_

----------------------------------------------------------------------
-- A tree datatype to represent a non-deterministic value of some type.
-- It is either a value or a choice between non-deterministic values.
----------------------------------------------------------------------

data ND (A : Set) : Set where
  Val  : A → ND A
  _??_ : ND A → ND A → ND A

----------------------------------------------------------------------
-- Some operations to define functions working this the ND datatype:

-- Apply a (deterministic) function to a non-deterministic argument.
-- This corresponds to a functor on the ND structure.
_$*_ : {A B : Set} → (A → B) → ND A → ND B
f $* (Val xs) = Val (f xs)
f $* (t1 ?? t2) = f $* t1 ?? f $* t2

-- Apply a non-deterministic function to a non-deterministic argument.
-- If ND would be an instance of the monad class, this is a monadic bind
-- with swapped arguments.
_*$*_ : {A B : Set} → (A → ND B) → ND A → ND B
f *$* (Val x)    = f x
f *$* (t1 ?? t2) = f *$* t1 ?? f *$* t2

-- Apply a binary non-deterministic function to non-deterministic arguments.
apply-nd2 : {A B C : Set} → (A → B → ND C) → ND A → ND B → ND C
apply-nd2 f a b = (λ x -> (λ y -> f x y) *$* b) *$* a

-- Apply a ternary non-deterministic function to non-deterministic arguments.
apply-nd3 : {A B C D : Set} → (A → B → C → ND D) → ND A → ND B → ND C → ND D
apply-nd3 f a b c = (λ x -> (λ y -> (λ z → f x y z) *$* c) *$* b) *$* a

-- Extend a deterministic function to one with non-deterministic result:
toND : {A B : Set} → (A → B) → A → ND B
toND f x = Val (f x)

----------------------------------------------------------------------
-- Some operations to define properties of non-deterministic values:

-- Count the number of values:
#vals : {A : Set} → ND A → ℕ
#vals (Val _) = 1
#vals (t1 ?? t2) = #vals t1 + #vals t2

-- Extract the list of all values:
vals-of : {A : Set} → ND A → 𝕃 A
vals-of (Val v)    = v :: []
vals-of (t1 ?? t2) = vals-of t1 ++ vals-of t2

-- All values in a Boolean tree are true:
always : ND 𝔹 → 𝔹
always (Val b)    = b
always (t1 ?? t2) = always t1 && always t2

-- There exists some true value in a Boolean tree:
eventually : ND 𝔹 → 𝔹
eventually (Val b)    = b
eventually (t1 ?? t2) = eventually t1 || eventually t2

-- All non-deterministic values satisfy a given predicate:
_satisfy_ : {A : Set} → ND A → (A → 𝔹) → 𝔹
(Val n)    satisfy p = p n
(t1 ?? t2) satisfy p = t1 satisfy p && t2 satisfy p

-- Every value in a tree is equal to the second argument w.r.t. a
-- comparison function provided as the first argument:
every : {A : Set} → (eq : A → A → 𝔹) → A → ND A → 𝔹
every eq x xs = xs satisfy (eq x)

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

max_stars_repo_name: mihanus/curry-agda

max_issues_repo_name: mihanus/curry-agda

max_forks_repo_name: mihanus/curry-agda


text:
open import Agda.Builtin.Equality

module _ (A : Set) where

data Wrap (X : Set) : Set where
  wrap : X → Wrap X

data D (x : A) : ∀ y → Wrap (x ≡ y) → Set where
  c : ∀ y (x≡y : x ≡ y) → D x y (wrap x≡y)

test : ∀ x y (x≡y x≡y' : Wrap (x ≡ y)) → D x y x≡y → D x y x≡y' → Set
test y .y (wrap refl) .(wrap refl) (c .y .refl) (c .y refl) = A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda