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

open import Prelude

module Cardinality.Finite.Cardinal.Category {ℓ : Level} where

open import Cardinality.Finite.Cardinal
open import HITs.PropositionalTruncation
open import Data.Sigma.Properties
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Categories
open import Cubical.Foundations.Univalence
open import Categories.Product
open import Categories.Exponential
open import Data.Fin
open import Cardinality.Finite.ManifestBishop

𝒞⇒isSet : 𝒞 A → isSet A
𝒞⇒isSet = Discrete→isSet ∘ 𝒞⇒Discrete

finSetPreCategory : PreCategory (ℓsuc ℓ) ℓ
finSetPreCategory .PreCategory.Ob = Σ (Type ℓ) 𝒞
finSetPreCategory .PreCategory.Hom (X , _) (Y , _) = X → Y
finSetPreCategory .PreCategory.Id = id
finSetPreCategory .PreCategory.Comp f g = f ∘ g
finSetPreCategory .PreCategory.assoc-Comp _ _ _ = refl
finSetPreCategory .PreCategory.Comp-Id _ = refl
finSetPreCategory .PreCategory.Id-Comp _ = refl
finSetPreCategory .PreCategory.Hom-Set {X} {Y} = hLevelPi 2 λ _ → Discrete→isSet (𝒞⇒Discrete (Y .snd))

open PreCategory finSetPreCategory

iso-iso : (X ≅ Y) ⇔ (fst X ⇔ fst Y)
iso-iso .fun (f , g , f∘g , g∘f) = iso f g (λ x i → g∘f i x) (λ x i → f∘g i x)
iso-iso .inv (iso f g g∘f f∘g) = f , g  , (λ i x → f∘g x i) , (λ i x → g∘f x i)
iso-iso .rightInv _ = refl
iso-iso .leftInv  _ = refl

finSetCategory : Category (ℓsuc ℓ) ℓ
finSetCategory .Category.preCategory = finSetPreCategory
finSetCategory .Category.univalent {X} {Y} =
  ≃ΣProp≡ (λ _ → squash) ⟨ trans-≃ ⟩
  univalence ⟨ trans-≃ ⟩
  isoToEquiv (
  sym-⇔ (iso⇔equiv (Discrete→isSet (𝒞⇒Discrete (X .snd)))) ⟨ trans-⇔ ⟩
  sym-⇔ (iso-iso {X} {Y}))

finSetHasProducts : HasProducts finSetCategory
finSetHasProducts .HasProducts.product X Y .Product.obj = X .fst × Y .fst , X .snd ∥×∥ Y .snd
finSetHasProducts .HasProducts.product X Y .Product.proj₁ = fst
finSetHasProducts .HasProducts.product X Y .Product.proj₂ = snd
finSetHasProducts .HasProducts.product X Y .Product.ump f g .fst z = f z , g z
finSetHasProducts .HasProducts.product X Y .Product.ump f g .snd .fst .fst = refl
finSetHasProducts .HasProducts.product X Y .Product.ump f g .snd .fst .snd = refl
finSetHasProducts .HasProducts.product X Y .Product.ump f g .snd .snd (f≡ , g≡) i x = f≡ (~ i) x , g≡ (~ i) x

finSetHasExp : HasExponentials finSetCategory finSetHasProducts
finSetHasExp X Y .Exponential.obj = (X .fst → Y .fst) , (X .snd ∥→∥ Y .snd)
finSetHasExp X Y .Exponential.eval (f , x) = f x
finSetHasExp X Y .Exponential.uniq X₁ f .fst = curry f
finSetHasExp X Y .Exponential.uniq X₁ f .snd .fst = refl
finSetHasExp X Y .Exponential.uniq X₁ f .snd .snd x = cong curry (sym x)

open import Categories.Pullback
open import Cardinality.Finite.SplitEnumerable using (ℰ!⟨Lift⟩; ℰ!⟨⊤⟩; ℰ!⟨⊥⟩)

finSetHasPullbacks : HasPullbacks finSetCategory
finSetHasPullbacks {X = X} {Y = Y} {Z = Z} f g .Pullback.P = ∃[ ab ] (f (fst ab) ≡ g (snd ab)) , ((X .snd ∥×∥ Y .snd) ∥Σ∥ λ _ → 𝒞⟨≡⟩ _ _ (Z .snd))
finSetHasPullbacks f g .Pullback.p₁ ((x , _) , _) = x
finSetHasPullbacks f g .Pullback.p₂ ((_ , y) , _) = y
finSetHasPullbacks f g .Pullback.commute = funExt snd
finSetHasPullbacks f g .Pullback.ump {A = A} h₁ h₂ p .fst x = (h₁ x , h₂ x) , λ i → p i x
finSetHasPullbacks f g .Pullback.ump {A = A} h₁ h₂ p .snd .fst .fst = refl
finSetHasPullbacks f g .Pullback.ump {A = A} h₁ h₂ p .snd .fst .snd = refl
finSetHasPullbacks {Z = Z} f g .Pullback.ump {A = A} h₁ h₂ p .snd .snd {i} (p₁e , p₂e) = funExt (λ x → ΣProp≡ (λ _ →  𝒞⇒isSet (Z .snd) _ _) λ j → p₁e (~ j) x , p₂e (~ j) x)

finSetTerminal : Terminal
finSetTerminal .fst = Lift _ ⊤ , ∣ ℰ!⇒ℬ (ℰ!⟨Lift⟩ ℰ!⟨⊤⟩) ∣
finSetTerminal .snd .fst x .lower = tt
finSetTerminal .snd .snd y = funExt λ _ → refl

finSetInitial : Initial
finSetInitial .fst = Lift _ ⊥ , ∣ ℰ!⇒ℬ (ℰ!⟨Lift⟩ ℰ!⟨⊥⟩) ∣
finSetInitial .snd .fst ()
finSetInitial .snd .snd y i ()

open import HITs.PropositionalTruncation
open import Categories.Coequalizer

∃!′ : (A : Type a) → (A → Type b) → Type (a ℓ⊔ b)
∃!′ A P = ∥ Σ A P ∥ Prelude.× AtMostOne P

lemma23 : ∀ {p} {P : A → hProp p} → ∃!′ A (fst ∘ P) → Σ A (fst ∘ P)
lemma23 {P = P} (x , y) = rec (λ xs ys → ΣProp≡ (snd ∘ P) (y (xs .fst) (ys .fst) (xs .snd) (ys .snd))) id x

module _ {A : Type a} {P : A → Type b} (R : ∀ x → P x → hProp c) where
  uniqueChoice : (Π[ x ⦂ A ] (∃!′ (P x) (λ u → R x u .fst))) →
                 Σ[ f ⦂ Π[ x ⦂ A ] P x ] Π[ x ⦂ A ] (R x (f x) .fst)
  uniqueChoice H = fst ∘ mid , snd ∘ mid
    where
    mid : Π[ x ⦂ A ] Σ[ u ⦂ P x ] (R x u .fst)
    mid x = lemma23 {P = R x} (H x)

open import HITs.PropositionalTruncation.Sugar
open import Data.List using (_∷_; [])
open import Cardinality.Finite.SplitEnumerable.Search using (ℰ!⟨fib⟩)

module CoeqProofs {X Y : Ob} (f : X ⟶ Y) where
  KernelPair : Pullback finSetCategory {X = X} {Z = Y} {Y = X} f f
  KernelPair = finSetHasPullbacks f f

  Im : Ob
  Im = ∃[ b ] ∥ fiber f b ∥ , (Y .snd ∥Σ∥ λ x → do cx ← X .snd ; cy ← Y .snd ; ∣ ℰ!⇒ℬ (ℰ!⟨fib⟩ f _ (ℬ⇒ℰ! cx) (ℬ⇒ℰ! cy)) ∣)

  im : X ⟶ Im
  im x = f x , ∣ x , refl ∣

  open Pullback KernelPair

  lem : ∀ {H : Ob} (h : X ⟶ H) → h ∘ p₁ ≡ h ∘ p₂ → Σ[ f ⦂ (Im ⟶ H) ] Π[ x ⦂ Im .fst ] (∀ y → im y ≡ x → h y ≡ f x)
  lem {H = H} h eq = uniqueChoice R prf
    where
    R : Im .fst → H .fst → hProp _
    R w x .fst = ∀ y → im y ≡ w → h y ≡ x
    R w x .snd = hLevelPi 1 λ _ → hLevelPi 1 λ _ → 𝒞⇒isSet (H .snd) _ _

    prf : Π[ x ⦂ Im .fst ] ∃!′ (H .fst) (λ u → ∀ y → im y ≡ x → h y ≡ u)
    prf (xy , p) .fst = (λ { (z , r) → h z , λ y imy≡xyp → cong (_$ ((y , z) , cong fst imy≡xyp ; sym r)) eq }) ∥$∥ p
    prf (xy , p) .snd x₁ x₂ Px₁ Px₂ = rec (𝒞⇒isSet (H .snd) x₁ x₂) (λ { (z , zs) → sym (Px₁ z (ΣProp≡ (λ _ → squash) zs)) ; Px₂ z (ΣProp≡ (λ _ → squash) zs) } ) p

  lem₂ : ∀ (H : Ob) (h : X ⟶ H) (i : Im ⟶ H) (x : Im .fst) (hi : h ≡ i ∘ im) (eq : h ∘ p₁ ≡ h ∘ p₂) → i x ≡ lem {H = H} h eq .fst x
  lem₂ H h i x hi eq = rec (𝒞⇒isSet (H .snd) _ _) (λ { (y , ys) → (cong i (ΣProp≡ (λ _ → squash) (sym ys)) ; sym (cong (_$ y) hi)) ; lem {H = H} h eq .snd x y (ΣProp≡ (λ _ → squash) ys) }) (x .snd)

  finSetCoeq : Coequalizer finSetCategory {X = P} {Y = X} p₁ p₂
  finSetCoeq .Coequalizer.obj = Im
  finSetCoeq .Coequalizer.arr = im
  finSetCoeq .Coequalizer.equality = funExt λ x → ΣProp≡ (λ _ → squash) λ i → commute i x
  finSetCoeq .Coequalizer.coequalize {H = H} {h = h} eq = lem {H = H} h eq .fst
  finSetCoeq .Coequalizer.universal {H = H} {h = h} {eq = eq} = funExt λ x → lem {H = H} h eq .snd (im x) x refl
  finSetCoeq .Coequalizer.unique {H = H} {h = h} {i = i} {eq = eq} prf = funExt λ x → lem₂ H h i x prf eq
open CoeqProofs public using (finSetCoeq)

module PullbackSurjProofs {X Y : Ob} (f : X ⟶ Y) (fSurj : Surjective f) where
  KernelPair : Pullback finSetCategory {X = X} {Z = Y} {Y = X} f f
  KernelPair = finSetHasPullbacks f f

  open Pullback KernelPair

  p₁surj : Surjective p₁
  p₁surj y = ∣ ((y , y) , refl) , refl ∣

  p₂surj : Surjective p₂
  p₂surj y = ∣ ((y , y) , refl) , refl ∣


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

open import Setoids.Setoids
open import Rings.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Groups.Definition
open import Groups.Lemmas
open import Fields.Fields
open import Sets.EquivalenceRelations
open import Sequences
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas

module Fields.CauchyCompletion.Addition {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

open Setoid S
open SetoidTotalOrder (TotallyOrderedRing.total order)
open SetoidPartialOrder pOrder
open Equivalence eq
open PartiallyOrderedRing pRing
open Ring R
open Group additiveGroup
open Field F

open import Fields.Lemmas F
open import Fields.CauchyCompletion.Definition order F
open import Rings.Orders.Partial.Lemmas pRing
open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order })
open import Rings.Orders.Total.AbsoluteValue order
open import Rings.Orders.Total.Lemmas order
open import Rings.Orders.Total.Cauchy order
open import Rings.InitialRing R

private
  lemm : (m : ℕ) (a b : Sequence A) → index (apply _+_ a b) m ≡ (index a m) + (index b m)
  lemm zero a b = refl
  lemm (succ m) a b = lemm m (Sequence.tail a) (Sequence.tail b)

private
  additionConverges : (a b : CauchyCompletion) → cauchy (apply _+_ (CauchyCompletion.elts a) (CauchyCompletion.elts b))
  additionConverges record { elts = a ; converges = convA } record { elts = b ; converges = convB } ε 0<e with halve charNot2 ε
  ... | e/2 , e/2Pr with convA e/2 (halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq e/2Pr) 0<e))
  ... | Na , prA with convB e/2 (halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq e/2Pr) 0<e))
  ... | Nb , prB = (Na +N Nb) , t
    where
      t : {m n : ℕ} → Na +N Nb <N m → Na +N Nb <N n → abs ((index (apply _+_ a b) m) + inverse (index (apply _+_ a b) n)) < ε
      t {m} {n} <m <n with prA {m} {n} (inequalityShrinkLeft <m) (inequalityShrinkLeft <n)
      ... | am-an<e/2 with prB {m} {n} (inequalityShrinkRight <m) (inequalityShrinkRight <n)
      ... | bm-bn<e/2 with triangleInequality (index a m + inverse (index a n)) (index b m + inverse (index b n))
      ... | inl tri rewrite lemm m a b | lemm n a b = SetoidPartialOrder.<WellDefined pOrder (Equivalence.reflexive eq) e/2Pr (SetoidPartialOrder.<Transitive pOrder {_} {(abs ((index a m) + (inverse (index a n)))) + (abs ((index b m) + (inverse (index b n))))} (<WellDefined (absWellDefined _ _ (Equivalence.transitive eq (Equivalence.symmetric eq (+Associative {index a m})) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq {index a m}) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq (+Associative {index b m})) (+WellDefined (Equivalence.reflexive eq {index b m}) (Equivalence.symmetric eq (invContravariant additiveGroup)))))) (+Associative {index a m})))) (Equivalence.reflexive eq) tri) (ringAddInequalities am-an<e/2 bm-bn<e/2))
      ... | inr tri rewrite lemm m a b | lemm n a b = SetoidPartialOrder.<WellDefined pOrder (Equivalence.reflexive eq) e/2Pr (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq tri) (absWellDefined _ _ (Equivalence.transitive eq (Equivalence.symmetric eq (+Associative {index a m})) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq {index a m}) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq (+Associative {index b m})) (+WellDefined (Equivalence.reflexive eq {index b m}) (Equivalence.symmetric eq (invContravariant additiveGroup)))))) (+Associative {index a m}))))) (Equivalence.reflexive eq) (ringAddInequalities am-an<e/2 bm-bn<e/2))

_+C_ : CauchyCompletion → CauchyCompletion → CauchyCompletion
CauchyCompletion.elts (record { elts = a ; converges = convA } +C record { elts = b ; converges = convB }) = apply _+_ a b
CauchyCompletion.converges (a +C b) = additionConverges a b

inverseDistributes : {r s : A} → inverse (r + s) ∼ inverse r + inverse s
inverseDistributes = Equivalence.transitive eq (invContravariant additiveGroup) groupIsAbelian

-C_ : CauchyCompletion → CauchyCompletion
CauchyCompletion.elts (-C a) = map inverse (CauchyCompletion.elts a)
CauchyCompletion.converges (-C record { elts = elts ; converges = converges }) ε 0<e with converges ε 0<e
CauchyCompletion.converges (-C record { elts = elts ; converges = converges }) ε 0<e | N , prN = N , ans
  where
    ans : {m n : ℕ} → (N <N m) → (N <N n) → abs ((index (map inverse elts) m) + inverse (index (map inverse elts) n)) < ε
    ans {m} {n} N<m N<n = <WellDefined (Equivalence.transitive eq (absWellDefined _ _ (Equivalence.reflexive eq)) (Equivalence.transitive eq (absNegation (index elts m + inverse (index elts n))) (absWellDefined _ _ (Equivalence.transitive eq inverseDistributes (+WellDefined (identityOfIndiscernablesLeft _∼_ (Equivalence.reflexive eq) (equalityCommutative (mapAndIndex elts inverse m))) (inverseWellDefined additiveGroup (identityOfIndiscernablesLeft _∼_ (Equivalence.reflexive eq) (equalityCommutative (mapAndIndex elts inverse n))))))))) (Equivalence.reflexive eq) (prN N<m N<n)

ext: agda


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

module Data.Binary where

open import Data.Binary.Definition public
  using (𝔹; 0ᵇ; 1ᵇ_; 2ᵇ_)
open import Data.Binary.Conversion public
  using (⟦_⇑⟧; ⟦_⇓⟧)
open import Data.Binary.Addition public
  using (_+_)
open import Data.Binary.Multiplication public
  using (_*_)
open import Data.Binary.Subtraction public
  using (_-_)
open import Data.Binary.Isomorphism public
  using (𝔹⇔ℕ)
open import Data.Binary.Increment public
  using (inc)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
open import Prelude
open import core

module lemmas-ground where
  -- not ground types aren't hole to hole
  ground-arr-not-hole : ∀{τ} →
                      (τ ground → ⊥) →
                      (τ ≠ (⦇·⦈ ==> ⦇·⦈))
  ground-arr-not-hole notg refl = notg GHole

  ground-prod-not-hole : ∀{τ} →
                     (τ ground → ⊥) →
                     (τ ≠ (⦇·⦈ ⊗ ⦇·⦈))
  ground-prod-not-hole notg refl = notg GProd

  -- not ground types either have to be hole or an arrow or a prod
  notground : ∀{τ} →
              (τ ground → ⊥) →
              (τ == ⦇·⦈) +
                (Σ[ τ1 ∈ typ ] Σ[ τ2 ∈ typ ] (τ == (τ1 ==> τ2))) +
                (Σ[ τ1 ∈ typ ] Σ[ τ2 ∈ typ ] (τ == (τ1 ⊗ τ2)))
  notground {b} gnd = abort (gnd GBase)
  notground {⦇·⦈} gnd = Inl refl
  notground {τ ==> τ₁} gnd = Inr (Inl (τ , τ₁ , refl))
  notground {τ ⊗ τ₁} gnd = Inr (Inr (τ , τ₁ , refl))

  ground-arr-lem :
                   (τ : typ) →
                   ((τ ground) → ⊥) →
                   (τ ≠  ⦇·⦈) →
                   Σ[ τ1 ∈ typ ] Σ[ τ2 ∈ typ ]
                     (((τ == (τ1 ==> τ2)) × ((τ1 ==> τ2) ≠ (⦇·⦈ ==> ⦇·⦈))) +
                      ((τ == (τ1 ⊗ τ2))  × ((τ1 ⊗ τ2)   ≠ (⦇·⦈ ⊗ ⦇·⦈))))
  ground-arr-lem b ng nh = abort (ng GBase)
  ground-arr-lem ⦇·⦈ ng nh = abort (nh refl)
  ground-arr-lem (τ1 ==> τ2) ng nh = τ1 , τ2 , Inl (refl , λ x → ng (lem' x))
    where
      lem' : ∀{τ1 τ2} → τ1 ==> τ2 == ⦇·⦈ ==> ⦇·⦈ → (τ1 ==> τ2) ground
      lem' refl = GHole
  ground-arr-lem (τ1 ⊗ τ2) ng nh = τ1 , τ2 , Inr (refl , (λ x → ng (lem' x)))
    where
      lem' : ∀{τ1 τ2} → τ1 ⊗ τ2 == ⦇·⦈ ⊗ ⦇·⦈ → (τ1 ⊗ τ2) ground
      lem' refl = GProd

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


text:
module New.LangChanges where

open import New.Lang public
open import New.Changes

isChAlgτ : (τ : Type) → IsChAlg ⟦ τ ⟧Type ⟦ Δt τ ⟧Type

Chτ : (τ : Type) → Set
Chτ τ = ⟦ Δt τ ⟧Type

chAlgt : (τ : Type) → ChAlg ⟦ τ ⟧Type
chAlgt τ = record { Ch = Chτ τ ; isChAlg = isChAlgτ τ}

instance
  ichAlgt : ∀ {τ} → ChAlg ⟦ τ ⟧Type
  ichAlgt {τ} = chAlgt τ

isChAlgτ (σ ⇒ τ) = isChAlg {{funCA {{chAlgt σ}} {{chAlgt τ}}}}
isChAlgτ int = isChAlg {{intCA}}
isChAlgτ (pair σ τ) = isChAlg {{pairCA {{chAlgt σ}} {{chAlgt τ}}}}
isChAlgτ (sum σ τ) = isChAlg {{sumCA {{chAlgt σ}} {{chAlgt τ}}}}

ΔΓ : Context → Context
ΔΓ ∅ = ∅
ΔΓ (τ • Γ) = Δt τ • τ • ΔΓ Γ

module _ where
  ChΓ : ∀ (Γ : Context) → Set
  ChΓ Γ = ⟦ ΔΓ Γ ⟧Context

  _e⊕_ : ∀ {Γ} → ⟦ Γ ⟧Context → ChΓ Γ → ⟦ Γ ⟧Context
  _e⊕_ ∅ ∅ = ∅
  _e⊕_ (v • ρ) (dv • _ • dρ) = v ⊕ dv • ρ e⊕ dρ
  _e⊝_ : ∀ {Γ} → ⟦ Γ ⟧Context → ⟦ Γ ⟧Context → ChΓ Γ
  _e⊝_ ∅ ∅ = ∅
  _e⊝_ (v₂ • ρ₂) (v₁ • ρ₁) = v₂ ⊝ v₁ • v₁ • ρ₂ e⊝ ρ₁

  validΓ : ∀ {Γ} → ⟦ Γ ⟧Context → ChΓ Γ → Set
  validΓ ∅ ∅ = ⊤
  validΓ (v • ρ) (dv • v′ • dρ) = valid v dv × v ≡ v′ × validΓ ρ dρ

  e⊝-valid : ∀ {Γ} → (ρ1 ρ2 : ⟦ Γ ⟧Context) → validΓ ρ1 (ρ2 e⊝ ρ1)
  e⊝-valid ∅ ∅ = tt
  e⊝-valid (v₁ • ρ₁) (v₂ • ρ₂) = ⊝-valid v₁ v₂ , refl , e⊝-valid ρ₁ ρ₂
  e⊕-⊝ : ∀ {Γ} → (ρ2 ρ1 : ⟦ Γ ⟧Context) → ρ1 e⊕ (ρ2 e⊝ ρ1) ≡ ρ2
  e⊕-⊝ ∅ ∅ = refl
  e⊕-⊝ (v₂ • ρ₂) (v₁ • ρ₁) = cong₂ _•_ (⊕-⊝ v₂ v₁) (e⊕-⊝ ρ₂ ρ₁)

  {-# TERMINATING #-}
  isEnvCA : ∀ Γ → IsChAlg ⟦ Γ ⟧Context (ChΓ Γ)

  e⊚-valid : ∀ {Γ} → (ρ : ⟦ Γ ⟧Context) (dρ1 : ChΓ Γ) →
      validΓ ρ dρ1 →
      (dρ2 : ChΓ Γ) →
      validΓ (ρ e⊕ dρ1) dρ2 →
      validΓ ρ (IsChAlg.default-⊚ (isEnvCA Γ) dρ1 ρ dρ2)
  e⊚-correct : ∀ {Γ} → (ρ : ⟦ Γ ⟧Context) (dρ1 : ChΓ Γ) →
      validΓ ρ dρ1 →
      (dρ2 : ChΓ Γ) →
      validΓ (ρ e⊕ dρ1) dρ2 →
      (ρ e⊕ IsChAlg.default-⊚ (isEnvCA Γ) dρ1 ρ dρ2) ≡
      ((ρ e⊕ dρ1) e⊕ dρ2)

  isEnvCA Γ = record
    { _⊕_ = _e⊕_
    ; _⊝_ = _e⊝_
    ; valid = validΓ
    ; ⊝-valid = e⊝-valid
    ; ⊕-⊝ = e⊕-⊝
    ; _⊚[_]_ = IsChAlg.default-⊚ (isEnvCA Γ)
    ; ⊚-valid = e⊚-valid
    ; ⊚-correct = e⊚-correct
    }
  e⊚-valid {Γ} = IsChAlg.default-⊚-valid (isEnvCA Γ)
  e⊚-correct {Γ} = IsChAlg.default-⊚-correct (isEnvCA Γ)

  envCA : ∀ Γ → ChAlg ⟦ Γ ⟧Context
  envCA Γ = record
    { Ch = ChΓ Γ
    ; isChAlg = isEnvCA Γ }

instance
  ienvCA : ∀ {Γ} → ChAlg ⟦ Γ ⟧Context
  ienvCA {Γ} = envCA Γ

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

module ConcretePermutation where

open import Level renaming (zero to lzero) hiding (suc)

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin; zero; inject+; fromℕ)
open import Data.Vec using (Vec; tabulate; allFin; []; _∷_)
open import Data.Vec.Properties using (tabulate∘lookup)

open import Function using (_∘_)
open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality using (_≡_; setoid)

--

open import Proofs using (
  -- VectorLemmas
   _!!_
   )

------------------------------------------------------------------------------
-- A concrete permutation has 4 components:
-- - the one-line notation for a permutation
-- - the one-line notation for the inverse permutation
-- - and 2 proofs that these are indeed inverses

-- One-line notation for permutations with identity and composition

FinVec : ℕ → ℕ → Set
FinVec m n = Vec (Fin m) n

1C : {n : ℕ} → FinVec n n
1C {n} = allFin n

_∘̂_ : {n₀ n₁ n₂ : ℕ} → Vec (Fin n₁) n₀ → Vec (Fin n₂) n₁ → Vec (Fin n₂) n₀
π₁ ∘̂ π₂ = tabulate (_!!_ π₂ ∘ _!!_ π₁)

-- Actual permutation

record CPerm (values : ℕ) (size : ℕ) : Set where
  constructor cp
  field
    π  : FinVec values size
    πᵒ : FinVec size values
    αp : π ∘̂ πᵒ ≡ 1C
    βp : πᵒ ∘̂ π ≡ 1C

------------------------------------------------------------------------------
-- We can compare concrete permutations for equality using _≡_
-- It is actually sufficient to compare just the forward π using _≡_

-- The set of permutations under _≡_

SCPerm : ℕ → ℕ → Setoid lzero lzero
SCPerm m n = setoid (CPerm m n)

-- This is just tabulate∘lookup, but it hides the details; should this
-- be called 'join' or 'flatten' ?

cauchyext : {m n : ℕ} (π : FinVec m n) → tabulate (_!!_ π) ≡ π
cauchyext π = tabulate∘lookup π

------------------------------------------------------------------------------
-- I always mix up which way the permutation works. Here is a small
-- example to serve as a reminder:

-- values

0₅ 1₅ 2₅ 3₅ 4₅ : Fin 5
0₅ = zero
1₅ = inject+ 3 (fromℕ 1)
2₅ = inject+ 2 (fromℕ 2)
3₅ = inject+ 1 (fromℕ 3)
4₅ = fromℕ 4

-- indices

0₃ 1₃ 2₃ : Fin 3
0₃ = zero
1₃ = inject+ 1 (fromℕ 1)
2₃ = fromℕ 2

πex : FinVec 5 3
πex = 4₅ ∷ 3₅ ∷ 2₅ ∷ []

fex : Fin 3 → Fin 5
fex i = πex !! i

-- fex 0₃ => 4₅
-- fex 1₃ => 3₅
-- fex 2₃ => 2₅

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

open import Categories.Bicategory using (Bicategory)

module Categories.Bicategory.Extras {o ℓ e t} (Bicat : Bicategory o ℓ e t) where

open import Data.Product using (_,_)

import Categories.Category.Construction.Core as Core
open import Categories.Category.Construction.Functors using (Functors; module curry)
open import Categories.Functor using (Functor)
open import Categories.Functor.Bifunctor using (flip-bifunctor)
open import Categories.Functor.Bifunctor.Properties
open import Categories.NaturalTransformation
  using (NaturalTransformation; ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)

import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR
open import Categories.NaturalTransformation.NaturalIsomorphism.Properties using (push-eq)

open Bicategory Bicat public
private
  variable
    A B C D : Obj
    f g h i : A ⇒₁ B
    α β γ δ : f ⇒₂ g

infixr 10 _▷ᵢ_
infixl 10 _◁ᵢ_
infixr 6  _⟩⊚⟨_ refl⟩⊚⟨_
infixl 7  _⟩⊚⟨refl

module ⊚ {A B C}          = Functor (⊚ {A} {B} {C})
module ⊚-assoc {A B C D}  = NaturalIsomorphism (⊚-assoc {A} {B} {C} {D})
module unitˡ {A B}        = NaturalIsomorphism (unitˡ {A} {B})
module unitʳ {A B}        = NaturalIsomorphism (unitʳ {A} {B})
module id {A}             = Functor (id {A})

private
  module MR′ {A} {B} where
    open Core.Shorthands (hom A B) public
    open MR (hom A B) public hiding (push-eq)
  open MR′

unitorˡ : {A B : Obj} {f : A ⇒₁ B} → id₁ ∘₁ f ≅ f
unitorˡ {_} {_} {f} = record
  { from = unitˡ.⇒.η (_ , f)
  ; to   = unitˡ.⇐.η (_ , f)
  ; iso  = unitˡ.iso (_ , f)
  }

module unitorˡ {A B f} = _≅_ (unitorˡ {A} {B} {f})

unitorʳ : {A B : Obj} {f : A ⇒₁ B} → f ∘₁ id₁ ≅ f
unitorʳ {_} {_} {f} = record
  { from = unitʳ.⇒.η (f , _)
  ; to   = unitʳ.⇐.η (f , _)
  ; iso  = unitʳ.iso (f , _)
  }

module unitorʳ {A B f} = _≅_ (unitorʳ {A} {B} {f})

associator : {A B C D : Obj} {f : D ⇒₁ B} {g : C ⇒₁ D} {h : A ⇒₁ C} →
             (f ∘₁ g) ∘₁ h ≅ f ∘₁ g ∘₁ h
associator {_} {_} {_} {_} {f} {g} {h} = record
  { from = ⊚-assoc.⇒.η ((f , g) , h)
  ; to   = ⊚-assoc.⇐.η ((f , g) , h)
  ; iso  = ⊚-assoc.iso ((f , g) , h)
  }

module associator {A B C D} {f : C ⇒₁ B} {g : D ⇒₁ C} {h} = _≅_ (associator {A = A} {B = B} {f = f} {g = g} {h = h})

module Shorthands where
  λ⇒ = unitorˡ.from
  λ⇐ = unitorˡ.to

  ρ⇒ = unitorʳ.from
  ρ⇐ = unitorʳ.to

  α⇒ = associator.from
  α⇐ = associator.to
open Shorthands

-- Two curried versions of ⊚.

-⊚[-] : Functor (hom A B) (Functors (hom B C) (hom A C))
-⊚[-] = curry.F₀ (flip-bifunctor ⊚)

[-]⊚- : Functor (hom B C) (Functors (hom A B) (hom A C))
[-]⊚- = curry.F₀ ⊚

-⊚_ : A ⇒₁ B → Functor (hom B C) (hom A C)
-⊚_ = Functor.F₀ -⊚[-]

_⊚- : B ⇒₁ C → Functor (hom A B) (hom A C)
_⊚- = Functor.F₀ [-]⊚-

-▷_ : ∀ {C} → f ⇒₂ g → NaturalTransformation (-⊚_ {C = C} f) (-⊚ g)
-▷_ = Functor.F₁ -⊚[-]

_◁- : ∀ {A} → f ⇒₂ g → NaturalTransformation (_⊚- {A = A} f) (g ⊚-)
_◁- = Functor.F₁ [-]⊚-

identity₂ˡ : id₂ ∘ᵥ α ≈ α
identity₂ˡ = hom.identityˡ

identity₂ʳ : α ∘ᵥ id₂ ≈ α
identity₂ʳ = hom.identityʳ

assoc₂ : (α ∘ᵥ β) ∘ᵥ γ ≈ α ∘ᵥ β ∘ᵥ γ
assoc₂ = hom.assoc

id₂◁ : id₂ {f = g} ◁ f ≈ id₂
id₂◁ = ⊚.identity

▷id₂ : f ▷ id₂ {f = g} ≈ id₂
▷id₂ = ⊚.identity

open hom.HomReasoning
open hom.Equiv

_⊚ᵢ_ : f ≅ h → g ≅ i → f ⊚₀ g ≅ h ⊚₀ i
α ⊚ᵢ β = record
  { from = from α ⊚₁ from β
  ; to   = to α ⊚₁ to β
  ; iso  = record
    { isoˡ = [ ⊚ ]-merge (isoˡ α) (isoˡ β) ○ ⊚.identity
    ; isoʳ = [ ⊚ ]-merge (isoʳ α) (isoʳ β) ○ ⊚.identity }
  }

_◁ᵢ_ : {g h : B ⇒₁ C} (α : g ≅ h) (f : A ⇒₁ B) → g ∘₁ f ≅ h ∘₁ f
α ◁ᵢ _ = α ⊚ᵢ idᵢ

_▷ᵢ_ : {f g : A ⇒₁ B} (h : B ⇒₁ C) (α : f ≅ g) → h ∘₁ f ≅ h ∘₁ g
_ ▷ᵢ α = idᵢ ⊚ᵢ α

⊚-resp-≈ : α ≈ β → γ ≈ δ → α ⊚₁ γ ≈ β ⊚₁ δ
⊚-resp-≈ p q = ⊚.F-resp-≈ (p , q)

⊚-resp-≈ˡ : α ≈ β → α ⊚₁ γ ≈ β ⊚₁ γ
⊚-resp-≈ˡ p = ⊚.F-resp-≈ (p , hom.Equiv.refl)

⊚-resp-≈ʳ : γ ≈ δ → α ⊚₁ γ ≈ α ⊚₁ δ
⊚-resp-≈ʳ q = ⊚.F-resp-≈ (hom.Equiv.refl , q)

_⟩⊚⟨_ : α ≈ β → γ ≈ δ → α ⊚₁ γ ≈ β ⊚₁ δ
_⟩⊚⟨_ = ⊚-resp-≈

refl⟩⊚⟨_ : γ ≈ δ → α ⊚₁ γ ≈ α ⊚₁ δ
refl⟩⊚⟨_ = ⊚-resp-≈ʳ

_⟩⊚⟨refl : α ≈ β → α ⊚₁ γ ≈ β ⊚₁ γ
_⟩⊚⟨refl = ⊚-resp-≈ˡ

∘ᵥ-distr-◁ : (α ◁ f) ∘ᵥ (β ◁ f) ≈ (α ∘ᵥ β) ◁ f
∘ᵥ-distr-◁ {f = f} = ⟺ (Functor.homomorphism (-⊚ f))

∘ᵥ-distr-▷ : (f ▷ α) ∘ᵥ (f ▷ β) ≈ f ▷ (α ∘ᵥ β)
∘ᵥ-distr-▷ {f = f} = ⟺ (Functor.homomorphism (f ⊚-))

λ⇒-∘ᵥ-▷ : λ⇒ ∘ᵥ (id₁ ▷ α) ≈ α ∘ᵥ λ⇒
λ⇒-∘ᵥ-▷ {α = α} = begin
  λ⇒ ∘ᵥ (id₁ ▷ α)    ≈˘⟨ refl⟩∘⟨ id.identity ⟩⊚⟨refl ⟩
  λ⇒ ∘ᵥ id.F₁ _ ⊚₁ α ≈⟨ unitˡ.⇒.commute (_ , α) ⟩
  α ∘ᵥ λ⇒            ∎

▷-∘ᵥ-λ⇐ : (id₁ ▷ α) ∘ᵥ λ⇐ ≈ λ⇐ ∘ᵥ α
▷-∘ᵥ-λ⇐ = conjugate-to (unitorˡ ⁻¹) (unitorˡ ⁻¹) λ⇒-∘ᵥ-▷

ρ⇒-∘ᵥ-◁ : ρ⇒ ∘ᵥ (α ◁ id₁) ≈ α ∘ᵥ ρ⇒
ρ⇒-∘ᵥ-◁ {α = α} = begin
  ρ⇒ ∘ᵥ (α ◁ id₁)      ≈˘⟨ refl⟩∘⟨ refl⟩⊚⟨ id.identity ⟩
  ρ⇒ ∘ᵥ (α ⊚₁ id.F₁ _) ≈⟨ unitʳ.⇒.commute (α , _) ⟩
  α ∘ᵥ ρ⇒              ∎

◁-∘ᵥ-ρ⇐ : (α ◁ id₁) ∘ᵥ ρ⇐ ≈ ρ⇐ ∘ᵥ α
◁-∘ᵥ-ρ⇐ = conjugate-to (unitorʳ ⁻¹) (unitorʳ ⁻¹) ρ⇒-∘ᵥ-◁

α⇐-◁-∘₁ : α⇐ ∘ᵥ (γ ◁ (g ∘₁ f)) ≈ ((γ ◁ g) ◁ f) ∘ᵥ α⇐
α⇐-◁-∘₁ {γ = γ} {g = g} {f = f} = begin
  α⇐ ∘ᵥ (γ ◁ (g ∘₁ f))    ≈˘⟨ refl⟩∘⟨ refl⟩⊚⟨ ⊚.identity ⟩
  α⇐ ∘ᵥ (γ ⊚₁ id₂ ⊚₁ id₂)  ≈⟨ ⊚-assoc.⇐.commute ((γ , id₂) , id₂) ⟩
  ((γ ◁ g) ◁ f) ∘ᵥ α⇐      ∎

α⇒-◁-∘₁ : α⇒ ∘ᵥ γ ◁ g ◁ f ≈ γ ◁ (g ∘₁ f) ∘ᵥ α⇒
α⇒-◁-∘₁ = ⟺ (conjugate-to associator associator α⇐-◁-∘₁)

α⇐-▷-◁ : α⇐ ∘ᵥ (f ▷ (γ ◁ g)) ≈ ((f ▷ γ) ◁ g) ∘ᵥ α⇐
α⇐-▷-◁ {f = f} {γ = γ} {g = g} = ⊚-assoc.⇐.commute ((id₂ , γ) , id₂)

α⇒-▷-∘₁ : α⇒ ∘ᵥ (f ∘₁ g) ▷ γ ≈ f ▷ g ▷ γ ∘ᵥ α⇒
α⇒-▷-∘₁{f = f} {g = g} {γ = γ} = begin
  α⇒ ∘ᵥ (f ⊚₀ g) ▷ γ     ≈˘⟨ refl⟩∘⟨ ⊚.identity ⟩⊚⟨refl ⟩
  α⇒ ∘ᵥ (f ▷ id₂) ⊚₁ γ   ≈⟨ ⊚-assoc.⇒.commute ((id₂ , id₂) , γ) ⟩
  f ▷ g ▷ γ ∘ᵥ α⇒        ∎

α⇐-▷-∘₁ : α⇐ ∘ᵥ (g ▷ (f ▷ γ)) ≈ ((g ∘₁ f) ▷ γ) ∘ᵥ α⇐
α⇐-▷-∘₁ = conjugate-from associator associator (⟺ α⇒-▷-∘₁)

◁-▷-exchg : ∀ {α : f ⇒₂ g} {β : h ⇒₂ i} → (i ▷ α) ∘ᵥ (β ◁ f) ≈ (β ◁ g) ∘ᵥ (h ▷ α)
◁-▷-exchg = [ ⊚ ]-commute

triangle-iso : {f : A ⇒₁ B} {g : B ⇒₁ C} →
               (g ▷ᵢ unitorˡ ∘ᵢ associator) ≈ᵢ (unitorʳ ◁ᵢ f)
triangle-iso = ⌞ triangle ⌟

triangle-inv : {f : A ⇒₁ B} {g : B ⇒₁ C} → α⇐ ∘ᵥ g ▷ λ⇐ ≈ ρ⇐ ◁ f
triangle-inv = to-≈ triangle-iso

pentagon-iso : ∀ {E} {f : A ⇒₁ B} {g : B ⇒₁ C} {h : C ⇒₁ D} {i : D ⇒₁ E} →
               (i ▷ᵢ associator ∘ᵢ associator ∘ᵢ associator ◁ᵢ f) ≈ᵢ
               (associator {f = i} {h} {g ∘₁ f} ∘ᵢ associator)
pentagon-iso = ⌞ pentagon ⌟

pentagon-inv : ∀ {E} {f : A ⇒₁ B} {g : B ⇒₁ C} {h : C ⇒₁ D} {i : D ⇒₁ E} →
               (α⇐ ◁ f ∘ᵥ α⇐) ∘ᵥ i ▷ α⇐ ≈ α⇐ ∘ᵥ α⇐ {f = i} {h} {g ∘₁ f}
pentagon-inv = to-≈ pentagon-iso

module UnitorCoherence where

  -- Extra coherence laws for the unitors.
  --
  -- These are similar to the extra coherence laws for monoidal
  -- categories that Kelly proved admissible in 1964.  The proofs are
  -- largely the same.  See Categories.Category.Monoidal.Properties
  -- for the monoidal versions and
  --
  --   https://ncatlab.org/nlab/show/monoidal+category
  --
  -- for an explanation of the proof and references to Kelly's paper.

  open ComHom

  -- As described on nLab, we start by proving that the 'perimeters'
  -- of two large diagrams commute...

  id▷λ-perimeter : [ ((id₁ ⊚₀ id₁) ⊚₀ f) ⊚₀ g ⇒ id₁ ⊚₀ (f ⊚₀ g) ]⟨
                     α⇒ ◁ g       ⇒⟨ (id₁ ⊚₀ (id₁ ⊚₀ f)) ⊚₀ g ⟩
                     α⇒           ⇒⟨ id₁ ⊚₀ ((id₁ ⊚₀ f) ⊚₀ g) ⟩
                     id₁ ▷ α⇒     ⇒⟨ id₁ ⊚₀ (id₁ ⊚₀ (f ⊚₀ g)) ⟩
                     id₁ ▷ λ⇒
                   ≈ ρ⇒ ◁ f ◁ g   ⇒⟨ (id₁ ⊚₀ f) ⊚₀ g ⟩
                     α⇒
                   ⟩
  id▷λ-perimeter {f = f} {g = g} = begin
    id₁ ▷ λ⇒ ∘ᵥ id₁ ▷ α⇒ ∘ᵥ α⇒ ∘ᵥ α⇒ ◁ g   ≈⟨ refl⟩∘⟨ pentagon ⟩
    id₁ ▷ λ⇒ ∘ᵥ α⇒ ∘ᵥ α⇒                   ≈⟨ pullˡ triangle ⟩
    ρ⇒ ◁ (f ⊚₀ g) ∘ᵥ α⇒                    ≈˘⟨ refl⟩⊚⟨ ⊚.identity ⟩∘⟨refl ⟩
    ρ⇒ ⊚₁ (id₂ ◁ g) ∘ᵥ α⇒                  ≈˘⟨ ⊚-assoc.⇒.commute _ ⟩
    α⇒ ∘ᵥ ρ⇒ ◁ f ◁ g                       ∎

  ρ◁id-perimeter : [ ((f ⊚₀ g) ⊚₀ id₁) ⊚₀ id₁ ⇒ f ⊚₀ (g ⊚₀ id₁) ]⟨
                     α⇒ ◁ id₁     ⇒⟨ (f ⊚₀ (g ⊚₀ id₁)) ⊚₀ id₁ ⟩
                     α⇒           ⇒⟨ f ⊚₀ ((g ⊚₀ id₁) ⊚₀ id₁) ⟩
                     f ▷ α⇒       ⇒⟨ f ⊚₀ (g ⊚₀ (id₁ ⊚₀ id₁)) ⟩
                     f ▷ g ▷ λ⇒
                   ≈ ρ⇒ ◁ id₁     ⇒⟨ (f ⊚₀ g) ⊚₀ id₁ ⟩
                     α⇒
                   ⟩
  ρ◁id-perimeter {f = f} {g = g} = begin
    f ▷ g ▷ λ⇒ ∘ᵥ f ▷ α⇒ ∘ᵥ α⇒ ∘ᵥ α⇒ ◁ id₁   ≈⟨ refl⟩∘⟨ pentagon ⟩
    f ▷ g ▷ λ⇒ ∘ᵥ α⇒ ∘ᵥ α⇒                   ≈˘⟨ pushˡ (⊚-assoc.⇒.commute _) ⟩
    (α⇒ ∘ᵥ (f ▷ id₂) ⊚₁ λ⇒) ∘ᵥ α⇒       ≈⟨ pullʳ (⊚.identity ⟩⊚⟨refl ⟩∘⟨refl) ⟩
    α⇒ ∘ᵥ (f ⊚₀ g) ▷ λ⇒ ∘ᵥ α⇒           ≈⟨ refl⟩∘⟨ triangle ⟩
    α⇒ ∘ᵥ ρ⇒ ◁ id₁                      ∎

  -- ... which allow us to prove that the following triangles commute...

  id▷λ-coherence : [ id₁ ⊚₀ ((id₁ ⊚₀ f) ⊚₀ g) ⇒ id₁ ⊚₀ (f ⊚₀ g) ]⟨
                     id₁ ▷ (λ⇒ ◁ g)
                   ≈ id₁ ▷ α⇒         ⇒⟨ id₁ ⊚₀ (id₁ ⊚₀ (f ⊚₀ g)) ⟩
                     id₁ ▷ λ⇒
                   ⟩
  id▷λ-coherence {f = f} {g = g} = begin
      id₁ ▷ (λ⇒ ◁ g)
    ≈⟨ switch-fromtoʳ associator (⟺ (⊚-assoc.⇒.commute _)) ⟩
      (α⇒ ∘ᵥ (id₁ ▷ λ⇒) ◁ g) ∘ᵥ α⇐
    ≈⟨ (refl⟩∘⟨ switch-fromtoʳ associator triangle ⟩⊚⟨refl) ⟩∘⟨refl ⟩
      (α⇒ ∘ᵥ ((ρ⇒ ◁ f ∘ᵥ α⇐) ◁ g)) ∘ᵥ α⇐
    ≈⟨ pushˡ (pushʳ (Functor.homomorphism (-⊚ g))) ⟩
      (α⇒ ∘ᵥ ρ⇒ ◁ f ◁ g) ∘ᵥ (α⇐ ◁ g ∘ᵥ α⇐)
    ≈˘⟨ switch-fromtoʳ (associator ∘ᵢ (associator ⊚ᵢ idᵢ))
                       (hom.assoc ○ id▷λ-perimeter) ⟩
      id₁ ▷ λ⇒ ∘ᵥ id₁ ▷ α⇒
    ∎

  ρ◁id-coherence : [ ((f ⊚₀ g) ⊚₀ id₁) ⊚₀ id₁ ⇒ (f ⊚₀ g) ⊚₀ id₁ ]⟨
                     ρ⇒ ◁ id₁
                   ≈ α⇒ ◁ id₁          ⇒⟨ (f ⊚₀ (g ⊚₀ id₁)) ⊚₀ id₁ ⟩
                     (f ▷ ρ⇒) ◁ id₁
                   ⟩
  ρ◁id-coherence {f = f} {g = g} = begin
      ρ⇒ ◁ id₁
    ≈⟨ switch-fromtoˡ associator (⟺ ρ◁id-perimeter) ⟩
      α⇐ ∘ᵥ f ▷ g ▷ λ⇒ ∘ᵥ f ▷ α⇒ ∘ᵥ α⇒ ∘ᵥ α⇒ ◁ id₁
    ≈˘⟨ pullʳ (pushˡ (Functor.homomorphism (f ⊚-))) ⟩
      (α⇐ ∘ᵥ f ▷ (g ▷ λ⇒ ∘ᵥ α⇒)) ∘ᵥ α⇒ ∘ᵥ α⇒ ◁ id₁
    ≈⟨ pullˡ (pushˡ (refl⟩∘⟨ refl⟩⊚⟨ triangle)) ⟩
      (α⇐ ∘ᵥ f ▷ (ρ⇒ ◁ id₁) ∘ᵥ α⇒) ∘ᵥ α⇒ ◁ id₁
    ≈˘⟨ switch-fromtoˡ associator (⊚-assoc.⇒.commute _) ⟩∘⟨refl ⟩
      (f ▷ ρ⇒) ◁ id₁ ∘ᵥ α⇒ ◁ id₁
    ∎

  -- ... which are the results modulo (id₁ ⊚-) and (-⊚ id₁).

  unitorˡ-coherence : [ (id₁ ⊚₀ f) ⊚₀ g ⇒ f ⊚₀ g ]⟨
                        λ⇒ ◁ g
                      ≈ α⇒         ⇒⟨ id₁ ⊚₀ (f ⊚₀ g) ⟩
                        λ⇒
                      ⟩
  unitorˡ-coherence {f = f} {g = g} = push-eq unitˡ (begin
    id.F₁ _ ⊚₁ (λ⇒ ◁ g)     ≈⟨ id.identity ⟩⊚⟨refl ⟩
    id₁ ▷ (λ⇒ ◁ g)          ≈⟨ id▷λ-coherence ⟩
    id₁ ▷ λ⇒ ∘ᵥ id₁ ▷ α⇒    ≈˘⟨ Functor.homomorphism (id₁ ⊚-) ⟩
    id₁ ▷ (λ⇒ ∘ᵥ α⇒)        ≈˘⟨ id.identity ⟩⊚⟨refl ⟩
    id.F₁ _ ⊚₁ (λ⇒ ∘ᵥ α⇒)   ∎)

  unitorʳ-coherence : [ (f ⊚₀ g) ⊚₀ id₁ ⇒ f ⊚₀ g ]⟨
                        ρ⇒
                      ≈ α⇒         ⇒⟨ f ⊚₀ (g ⊚₀ id₁) ⟩
                        f ▷ ρ⇒
                      ⟩
  unitorʳ-coherence {f = f} {g = g} = push-eq unitʳ (begin
    ρ⇒ ⊚₁ id.F₁ _                ≈⟨ refl⟩⊚⟨ id.identity ⟩
    ρ⇒ ◁ id₁                     ≈⟨ ρ◁id-coherence ⟩
    (f ▷ ρ⇒) ◁ id₁ ∘ᵥ α⇒ ◁ id₁   ≈˘⟨ Functor.homomorphism (-⊚ id₁) ⟩
    (f ▷ ρ⇒ ∘ᵥ α⇒) ◁ id₁         ≈˘⟨ refl⟩⊚⟨ id.identity ⟩
    (f ▷ ρ⇒ ∘ᵥ α⇒) ⊚₁ id.F₁ _    ∎)

open UnitorCoherence public using (unitorˡ-coherence; unitorʳ-coherence)

max_stars_repo_name: maxsnew/agda-categories

max_issues_repo_name: maxsnew/agda-categories

max_forks_repo_name: maxsnew/agda-categories


text:
------------------------------------------------------------------------------
-- Colists
------------------------------------------------------------------------------

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

module FOTC.Data.Colist where

open import FOTC.Base
open import FOTC.Data.Colist.Type public

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module trie-fast where

open import trie-core public
open import string
open import maybe
open import char
open import bool
open import eq

trie-lookup-fast3 : ∀{A : Set} → trie A → string → maybe A
trie-lookup-fast3{A} t s
  = extract (stringFoldl f t s)
  where
    extract : trie A → maybe A
    extract (trie.Node x _) = x

    -- define an "empty trie" and change this to:
    --  (trie A) → char → (trie A)
    f : trie A → char → trie A
    f (Node _ ts) c with cal-lookup ts c
    f (Node _ ts) c | nothing = Node nothing empty-cal
    f (Node _ ts) c | just t = t

trie-lookup : ∀{A : Set} → trie A → string → maybe A
trie-lookup = trie-lookup-fast3

trie-insert-fast2 : ∀{A : Set} → trie A → string → A → trie A
trie-insert-fast2{A} t s new-data = (stringFoldr g initial-f s) t
  where
   initial-f : trie A → trie A
   initial-f (Node _ ts) = Node (just new-data) ts

   g : char → (trie A → trie A) → (trie A → trie A)
   g c f (Node odata ts) with cal-lookup ts c
   g c f (Node odata ts) | nothing = Node odata (cal-add ts c (f empty-trie))
   g c f (Node odata ts) | just t = Node odata (cal-insert ts c (f t))

trie-insert : ∀{A : Set} → trie A → string → A → trie A
trie-insert = trie-insert-fast2

trie-remove-fast : ∀{A : Set} → trie A → string → trie A
trie-remove-fast{A} t s = (stringFoldr g initial-f s) t
  where
   initial-f : trie A → trie A
   initial-f (Node _ ts) = Node nothing ts

   g : char → (trie A → trie A) → (trie A → trie A)
   g c f (Node odata ts) with cal-lookup ts c
   g c f (Node odata ts) | nothing = Node odata ts
   g c f (Node odata ts) | just t = Node odata (cal-insert ts c (f t))

trie-remove : ∀{A : Set} → trie A → string → trie A
trie-remove = trie-remove-fast

open import trie-functions trie-lookup trie-insert trie-remove public

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
module Lambda where

  -- The typed λ-calculus

  -- The type of types
  data ty : Set where
     ι : ty                   -- the base type
     _⇒_ : ty → ty → ty      -- function type
     _×_ : ty → ty → ty      -- product type

  infixr 7 _⇒_
  infixl 8 _×_

  -- A typing context, there are no variable names because we use de Bruijn indices.
  data ctx : Set where
     • : ctx                  -- empty context
     _,_ : ctx → ty → ctx     -- context extension

  infixr 5 _,_

  -- A variable is a natural number (de Bruijn index, position in the context),
  -- but at the same time a proof that a type appears in the context.
  -- We write Γ ∋ A for the type of variables in Γ of type A.
  data _∋_ : (Γ : ctx) (B : ty) → Set where
     Z : {Γ : ctx} {B : ty} → (Γ , B) ∋ B              -- zero index
     S : {Γ : ctx} {A B : ty} → Γ ∋ B → (Γ , A) ∋ B    -- successor index

  infix 4 _∋_

  -- The type of terms in context Γ of type A
  data tm (Γ : ctx) : (A : ty) → Set where
     tm-var : {A : ty} → Γ ∋ A → tm Γ A
     tm-λ : {B : ty} {A : ty} → tm (Γ , A) B → tm Γ (A ⇒ B)
     tm-app : {A B : ty} → tm Γ (A ⇒ B) → tm Γ A → tm Γ B
     tm-pair : {A B : ty} → tm Γ A → tm Γ B → tm Γ (A × B)
     tm-fst : {A B : ty} → tm Γ (A × B) → tm Γ A
     tm-snd : {A B : ty} → tm Γ (A × B) → tm Γ B

  -- We need serveral boring auxiliary functions whose
  -- purpose is to define substitution

  -- A variable renaming is a type-preserving map from variables in Γ to variables in Δ
  -- (In Agda "renaming" is a reserved word.)
  variable-renaming = λ Γ Δ → ∀ {A} → Γ ∋ A → Δ ∋ A

  -- we may extend a renaming by one more variable (which does not get renamed)
  extend-renaming : ∀ {Γ Δ A} → variable-renaming Γ Δ → variable-renaming (Γ , A) (Δ , A)
  extend-renaming ρ Z = Z
  extend-renaming ρ (S x) = S (ρ x)

  -- the action of a renaming on a term
  term-rename : ∀ {Γ Δ} → variable-renaming Γ Δ → (∀ {A} → tm Γ A → tm Δ A)
  term-rename ρ (tm-var x) = tm-var (ρ x)
  term-rename ρ (tm-λ t) = tm-λ (term-rename (extend-renaming ρ) t)
  term-rename ρ (tm-app s t) = tm-app (term-rename ρ s) (term-rename ρ t)
  term-rename ρ (tm-pair s t) = tm-pair (term-rename ρ s) (term-rename ρ t)
  term-rename ρ (tm-fst t) = tm-fst (term-rename ρ t)
  term-rename ρ (tm-snd t) = tm-snd (term-rename ρ t)

  -- a special kind of renaming is weakening by a variable, which we write as ↑
  ↑ : ∀ {Γ A B} → tm Γ A → tm (Γ , B) A
  ↑ = term-rename S

  -- a substitution from Γ to Δ takes variables in Γ to terms in Δ
  substitution = λ Γ Δ → (∀ {A} → Γ ∋ A → tm Δ A)

  extend-substutition : ∀ {Γ Δ A} → substitution Γ Δ → substitution (Γ , A) (Δ , A)
  extend-substutition σ Z = tm-var Z
  extend-substutition σ (S x) = ↑ (σ x)

  -- The action of a substitution on a term
  term-substitute : ∀ {Γ Δ} → substitution Γ Δ → ∀ {A} → tm Γ A → tm Δ A
  term-substitute σ (tm-var x) = σ x
  term-substitute σ (tm-λ t) = tm-λ (term-substitute (extend-substutition σ) t)
  term-substitute σ (tm-app s t) = tm-app (term-substitute σ s) (term-substitute σ t)
  term-substitute σ (tm-pair s t) = tm-pair (term-substitute σ s) (term-substitute σ t)
  term-substitute σ (tm-fst t) = tm-fst (term-substitute σ t)
  term-substitute σ (tm-snd t) = tm-snd (term-substitute σ t)

  -- Auxiliary substitution that replaces just the 0-th variable
  subst-Z : ∀ {Γ A} → tm Γ A → substitution (Γ , A) Γ
  subst-Z t Z = t
  subst-Z T (S x) = tm-var x

  -- A common kind of substitution only replaces the 0-th variable with a term
  -- and leaves all the others intact, so we define its action as a shorthand
  _[_] : ∀ {Γ A B} → tm (Γ , A) B → tm Γ A → tm Γ B
  _[_] {Γ} {A} {B} s t = term-substitute (subst-Z t) s where

  infix 5 _[_]

  -- Judgemental equality
  data _≡_ {Γ : ctx} : {A : ty} (t s : tm Γ A) → Set where
    -- general rules
    eq-refl : {A : ty} {t : tm Γ A} → t ≡ t
    eq-tran : {A : ty} {t s u : tm Γ A} → t ≡ s → s ≡ u → t ≡ u
    eq-sym :  {A : ty} {t s : tm Γ A} → t ≡ s → s ≡ t
    -- congruence rules
    eq-congr-app : ∀ {A B} {t₁ t₂ : tm Γ (A ⇒ B)} {s₁ s₂ : tm Γ A} →
                   t₁ ≡ t₂ → s₁ ≡ s₂ → tm-app t₁ s₁ ≡ tm-app t₂ s₂
    eq-congr-λ : ∀ {A B} {t₁ t₂ : tm (Γ , A) B} → t₁ ≡ t₂ → tm-λ t₁ ≡ tm-λ t₂
    eq-congr-pair : ∀ {A B} {t₁ t₂ : tm Γ (A ⇒ B)} {s₁ s₂ : tm Γ A} →
                   t₁ ≡ t₂ → s₁ ≡ s₂ → tm-pair t₁ s₁ ≡ tm-pair t₂ s₂
    eq-congr-fst : ∀ {A B} {s t : tm Γ (A × B)} → s ≡ t → tm-fst s ≡ tm-fst t
    eq-congr-snd : ∀ {A B} {s t : tm Γ (A × B)} → s ≡ t → tm-snd s ≡ tm-snd t
    -- function type rules
    eq-β : ∀ {A B} {t : tm (Γ , A) B} {s : tm Γ A} → tm-app (tm-λ t) s ≡ t [ s ]
    eq-⇒ : ∀ {A B} {s t : tm Γ (A ⇒ B)} →
             tm-app (↑ s) (tm-var Z) ≡ tm-app (↑ t) (tm-var Z)
             → s ≡ t
    -- product rules
    eq-fst : ∀ {A B} {u : tm Γ A} {v : tm Γ B} → tm-fst (tm-pair u v) ≡ u
    eq-snd : ∀ {A B} {u : tm Γ A} {v : tm Γ B} → tm-snd (tm-pair u v) ≡ v
    eq-× : ∀{A B} {s t : tm Γ (A × B)} → tm-fst s ≡ tm-fst t → tm-snd s ≡ tm-snd t → s ≡ t

  infix 4 _≡_

  -- "η-equivalence" for products
  eq-pair-η : ∀ {Γ A B} {s : tm Γ (A × B)} → tm-pair (tm-fst s) (tm-snd s) ≡ s
  eq-pair-η = eq-× eq-fst eq-snd

  -- subst-↑ : ∀ {Γ A B} (t : tm Γ A) (s : tm Γ B) → (( (↑ t) [ s ] ) ≡ t)
  -- subst-↑ (tm-var x) s = eq-refl
  -- subst-↑ (tm-λ t) s = eq-congr-λ {!!}
  -- subst-↑ (tm-app t₁ t₂) s = eq-congr-app (subst-↑ t₁ s) (subst-↑ t₂ s)
  -- I commented this lemma that we tried to prove this morning because we did not achieve to do it yet, and Agda doesn't like the fact that I did not detail the other case of terms yet

  -- Example: the identity function
  -- Note that we actually define a family of terms, indexed by a context
  -- and a type, but the family is constant, i.e., it is always the same term.
  tm-id : ∀ {Γ A} → tm Γ (A ⇒ A)
  tm-id = tm-λ (tm-var Z)

  -- Appying the identity function twice does nothing
  app-id-id : ∀ {Γ A} {t : tm Γ A} → tm-app tm-id (tm-app tm-id t) ≡ t
  -- app-id-id = eq-tran (eq-congr-app eq-refl eq-β) eq-β
  app-id-id = eq-tran eq-β eq-β

  -- Eta-rule

  eq-η : ∀ {Γ A B} {t : tm Γ (A ⇒ B)} → tm-λ (tm-app (↑ t) (tm-var Z)) ≡ t
  eq-η = eq-⇒(eq-tran eq-β (eq-congr-app {!!} eq-refl))

  -- natural numbers
  data N : Set where
    zero : N
    succ : N → N

  -- church numerals

  tm-numeral : ∀ {Γ} → N → tm Γ ((ι ⇒ ι) ⇒ (ι ⇒ ι))
  tm-numeral zero = tm-id
  tm-numeral (succ n) = tm-λ (tm-λ (tm-app (tm-app (tm-numeral n) (tm-var (S Z))) (tm-app (tm-var (S Z)) (tm-var Z))))

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
open import Prelude
open import Nat
open import core
open import contexts

module lemmas-gcomplete where
  -- if you add a complete type to a complete context, the result is also a
  -- complete context
  gcomp-extend : ∀{Γ τ x} → Γ gcomplete → τ tcomplete → x # Γ → (Γ ,, (x , τ)) gcomplete
  gcomp-extend {Γ} {τ} {x} gc tc apart x_query τ_query x₁ with natEQ x x_query
  gcomp-extend {Γ} {τ} {x} gc tc apart .x τ_query x₂ | Inl refl = tr (λ qq → qq tcomplete) (lem-apart-union-eq {Γ = Γ} apart x₂) tc
  gcomp-extend {Γ} {τ} {x} gc tc apart x_query τ_query x₂ | Inr x₁ = gc x_query τ_query (lem-neq-union-eq {Γ = Γ} (flip x₁) x₂ )


text:
------------------------------------------------------------------------
-- A definitional interpreter
------------------------------------------------------------------------

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

module Lambda.Simplified.Partiality-monad.Inductive.Interpreter where

open import Equality.Propositional.Cubical
open import Prelude hiding (⊥)

open import Bijection equality-with-J using (_↔_)
open import Function-universe equality-with-J hiding (id; _∘_)
open import Monad equality-with-J
open import Univalence-axiom equality-with-J
open import Vec.Function equality-with-J

open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Fixpoints
open import Partiality-monad.Inductive.Monad

open import Lambda.Simplified.Syntax

open Closure Tm

------------------------------------------------------------------------
-- One interpreter

module Interpreter₁ where

  -- This interpreter is defined as the least upper bound of a
  -- sequence of increasingly defined interpreters.

  infix 10 _∙_

  mutual

    ⟦_⟧′ : ∀ {n} → Tm n → Env n → ℕ → Value ⊥
    ⟦ var x ⟧′   ρ n = return (ρ x)
    ⟦ ƛ t ⟧′     ρ n = return (ƛ t ρ)
    ⟦ t₁ · t₂ ⟧′ ρ n = ⟦ t₁ ⟧′ ρ n >>= λ v₁ →
                       ⟦ t₂ ⟧′ ρ n >>= λ v₂ →
                       (v₁ ∙ v₂) n

    _∙_ : Value → Value → ℕ → Value ⊥
    (ƛ t₁ ρ ∙ v₂) zero    = never
    (ƛ t₁ ρ ∙ v₂) (suc n) = ⟦ t₁ ⟧′ (cons v₂ ρ) n

  mutual

    ⟦⟧′-increasing :
      ∀ {n} (t : Tm n) ρ n → ⟦ t ⟧′ ρ n ⊑ ⟦ t ⟧′ ρ (suc n)
    ⟦⟧′-increasing (var x)   ρ n = return (ρ x)   ■
    ⟦⟧′-increasing (ƛ t)     ρ n = return (ƛ t ρ) ■
    ⟦⟧′-increasing (t₁ · t₂) ρ n =
      ⟦⟧′-increasing t₁ ρ n >>=-mono λ v₁ →
      ⟦⟧′-increasing t₂ ρ n >>=-mono λ v₂ →
      ∙-increasing v₁ v₂ n

    ∙-increasing : ∀ v₁ v₂ n → (v₁ ∙ v₂) n ⊑ (v₁ ∙ v₂) (suc n)
    ∙-increasing (ƛ t₁ ρ) v₂ (suc n) = ⟦⟧′-increasing t₁ (cons v₂ ρ) n
    ∙-increasing (ƛ t₁ ρ) v₂ zero    =
      never                  ⊑⟨ never⊑ _ ⟩■
      ⟦ t₁ ⟧′ (cons v₂ ρ) 0  ■

  ⟦_⟧ˢ : ∀ {n} → Tm n → Env n → Increasing-sequence Value
  ⟦ t ⟧ˢ ρ = ⟦ t ⟧′ ρ , ⟦⟧′-increasing t ρ

  ⟦_⟧ : ∀ {n} → Tm n → Env n → Value ⊥
  ⟦ t ⟧ ρ = ⨆ (⟦ t ⟧ˢ ρ)

------------------------------------------------------------------------
-- Another interpreter

module Interpreter₂ where

  -- This interpreter is defined using a fixpoint combinator.

  M : Type → Type₁
  M = Partial (∃ λ n → Tm n × Env n) (λ _ → Value)

  infix 10 _∙_

  _∙_ : Value → Value → M Value
  ƛ t₁ ρ ∙ v₂ = rec (_ , t₁ , cons v₂ ρ)

  ⟦_⟧′ : ∀ {n} → Tm n → Env n → M Value
  ⟦ var x ⟧′   ρ = return (ρ x)
  ⟦ ƛ t ⟧′     ρ = return (ƛ t ρ)
  ⟦ t₁ · t₂ ⟧′ ρ = ⟦ t₁ ⟧′ ρ >>= λ v₁ →
                   ⟦ t₂ ⟧′ ρ >>= λ v₂ →
                   v₁ ∙ v₂

  evalP : (∃ λ n → Tm n × Env n) → M Value
  evalP (_ , t , ρ) = ⟦ t ⟧′ ρ

  eval : Trans-⊑ (∃ λ n → Tm n × Env n) (λ _ → Value)
  eval = transformer evalP

  ⟦_⟧ : ∀ {n} → Tm n → Env n → Value ⊥
  ⟦ t ⟧ ρ = fixP evalP (_ , t , ρ)

------------------------------------------------------------------------
-- The two interpreters are pointwise equal

-- Both interpreters' bodies have the form ⨆ s for some sequences s,
-- and element n in the first interpreter's sequence is equal to
-- element 1 + n in the second interpreter's sequence (when the
-- arguments are equal).

interpreters-equal :
  ∀ {n} (t : Tm n) ρ →
  Interpreter₁.⟦ t ⟧ ρ ≡ Interpreter₂.⟦ t ⟧ ρ
interpreters-equal = λ t ρ →
                                                                $⟨ ⟦⟧-lemma t ρ ⟩
  (∀ n → Interpreter₁.⟦ t ⟧′ ρ n ≡
         app→ Interpreter₂.eval (suc n) (_ , t , ρ))            ↝⟨ cong ⨆ ∘ _↔_.to equality-characterisation-increasing ⟩

  ⨆ (Interpreter₁.⟦ t ⟧ˢ ρ) ≡
  ⨆ (tailˢ (at (fix→-sequence Interpreter₂.eval) (_ , t , ρ)))  ↝⟨ flip trans (⨆tail≡⨆ _) ⟩

  ⨆ (Interpreter₁.⟦ t ⟧ˢ ρ) ≡
  ⨆ (at (fix→-sequence Interpreter₂.eval) (_ , t , ρ))          ↝⟨ id ⟩□

  Interpreter₁.⟦ t ⟧ ρ ≡ Interpreter₂.⟦ t ⟧ ρ                   □
  where
  open Partial
  open Trans-⊑

  mutual

    ⟦⟧-lemma :
      ∀ {n} (t : Tm n) ρ n →
      Interpreter₁.⟦ t ⟧′ ρ n ≡
      function (Interpreter₂.⟦ t ⟧′ ρ)
               (app→ Interpreter₂.eval n)
    ⟦⟧-lemma (var x)   ρ n = refl
    ⟦⟧-lemma (ƛ t)     ρ n = refl
    ⟦⟧-lemma (t₁ · t₂) ρ n =
      cong₂ _>>=_ (⟦⟧-lemma t₁ ρ n) $ ⟨ext⟩ λ v₁ →
      cong₂ _>>=_ (⟦⟧-lemma t₂ ρ n) $ ⟨ext⟩ λ v₂ →
      ∙-lemma v₁ v₂ n

    ∙-lemma :
      ∀ v₁ v₂ n →
      (v₁ Interpreter₁.∙ v₂) n ≡
      function (v₁ Interpreter₂.∙ v₂)
               (app→ Interpreter₂.eval n)
    ∙-lemma (ƛ t₁ ρ) v₂ zero    = refl
    ∙-lemma (ƛ t₁ ρ) v₂ (suc n) = ⟦⟧-lemma t₁ (cons v₂ ρ) n

------------------------------------------------------------------------
-- An example

-- The semantics of Ω is the non-terminating computation never.

-- A proof for Interpreter₁.

Ω-loops₁ : Interpreter₁.⟦ Ω ⟧ nil ≡ never
Ω-loops₁ =
  antisymmetry (least-upper-bound _ _ lemma) (never⊑ _)
  where
  open Interpreter₁

  ω-nil = ƛ (var fzero · var fzero) nil

  reduce-twice :
    ∀ n → ⟦ Ω ⟧′ nil n ≡ (ω-nil ∙ ω-nil) n
  reduce-twice n =
    ⟦ Ω ⟧′ nil n                              ≡⟨ now->>= ⟩
    (⟦ ω ⟧′ nil n >>= λ v₂ → (ω-nil ∙ v₂) n)  ≡⟨ now->>= ⟩∎
    (ω-nil ∙ ω-nil) n                         ∎

  lemma : ∀ n → ⟦ Ω ⟧′ nil n ⊑ never
  lemma zero    =
    ⟦ Ω ⟧′ nil zero       ≡⟨ reduce-twice zero ⟩⊑
    (ω-nil ∙ ω-nil) zero  ⊑⟨⟩
    never                 ■
  lemma (suc n) =
    ⟦ Ω ⟧′ nil (suc n)  ≡⟨ reduce-twice (suc n) ⟩⊑
    ⟦ Ω ⟧′ nil n        ⊑⟨ lemma n ⟩■
    never               ■

-- A direct proof for Interpreter₂.

Ω-loops₂ : Interpreter₂.⟦ Ω ⟧ nil ≡ never
Ω-loops₂ = antisymmetry (least-upper-bound _ _ lemma) (never⊑ _)
  module Ω-loops₂ where
  open Interpreter₂
  open Trans-⊑
  open Partial

  ω-nil = ƛ (var fzero · var fzero) nil

  reduce-twice :
    ∀ f →
    function eval f (_ , Ω , nil) ≡
    f (_ , var fzero · var fzero , cons ω-nil nil)
  reduce-twice f =
    function eval f (_ , Ω , nil)                   ≡⟨⟩
    function (⟦ Ω ⟧′ nil) f                         ≡⟨ cong {x = function (⟦ Ω ⟧′ nil)}              (_$ f) (⟨ext⟩ λ _ → now->>=) ⟩
    function (⟦ ω ⟧′ nil >>= λ v₂ → ω-nil ∙ v₂) f   ≡⟨ cong {x = function (⟦ ω ⟧′ nil >>= ω-nil ∙_)} (_$ f) (⟨ext⟩ λ _ → now->>=) ⟩
    function (ω-nil ∙ ω-nil) f                      ≡⟨⟩
    f (_ , var fzero · var fzero , cons ω-nil nil)  ∎

  lemma : ∀ n → app→ eval n (_ , Ω , nil) ⊑ never
  lemma zero       = never⊑ never
  lemma (suc zero) =
    app→ eval 1 (_ , Ω , nil)  ≡⟨ reduce-twice _ ⟩⊑
    app→ eval 0 (_ , Ω , nil)  ⊑⟨⟩
    never                      ■
  lemma (suc (suc n)) =
    app→ eval (suc (suc n)) (_ , Ω , nil)  ≡⟨ reduce-twice _ ⟩⊑
    app→ eval (suc n) (_ , Ω , nil)        ⊑⟨ lemma (suc n) ⟩■
    never                                  ■

-- Another proof for Interpreter₂. This proof uses Scott induction.

Ω-loops₂′ : Interpreter₂.⟦ Ω ⟧ nil ≡ never
Ω-loops₂′ = antisymmetry lemma (never⊑ _)
  where
  open Interpreter₂
  open Trans-⊑
  open Partial

  lemma =
    ⟦ Ω ⟧ nil                                              ⊑⟨⟩

    fixP evalP (_ , Ω , nil)                               ≡⟨ cong (_$ (_ , Ω , nil)) $
                                                                fixP-is-fixpoint-combinator evalP ⟩⊑
    function eval (fixP evalP) (_ , Ω , nil)               ⊑⟨ fixP-induction₁
                                                                (λ f → function eval f (_ , Ω , nil) ⊑ never) (
        function eval (const never) (_ , Ω , nil)                  ≡⟨ Ω-loops₂.reduce-twice _ ⟩⊑
        never                                                      ■)
                                                                (λ s hyp →
        function eval (⨆ ∘ s) (_ , Ω , nil)                        ≡⟨ Ω-loops₂.reduce-twice _ ⟩⊑
        ⨆ (s _)                                                    ⊑⟨ least-upper-bound _ _ (λ n →

            s _ [ n ]                                                   ≡⟨ sym $ Ω-loops₂.reduce-twice _ ⟩⊑
            function eval (λ x → s x [ n ]) (_ , Ω , nil)               ⊑⟨ hyp n ⟩■
            never                                                       ■) ⟩

        never                                                      ■)
                                                                evalP
                                                                (λ g hyp →
        function eval (function eval g) (_ , Ω , nil)              ≡⟨ Ω-loops₂.reduce-twice _ ⟩⊑
        function eval g (_ , Ω , nil)                              ⊑⟨ hyp ⟩■
        never                                                      ■) ⟩■

    never                                                  ■

------------------------------------------------------------------------
-- Setup

-- Let us use Interpreter₂ as the default interpreter.

open Interpreter₂ public

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module Elements where

open import OscarPrelude
open import Arity
open import Vector
open import Element

record Elements : Set
 where
  constructor ⟨_⟩
  field
    {arity} : Arity
    elements : Vector Element arity

open Elements public

instance EqElements : Eq Elements
Eq._==_ EqElements (⟨_⟩ {𝑎₁} εs₁) (⟨_⟩ {𝑎₂} εs₂)
 with 𝑎₁ ≟ 𝑎₂
… | no 𝑎₁≢𝑎₂ = no λ {refl → 𝑎₁≢𝑎₂ refl}
… | yes refl
 with εs₁ ≟ εs₂
… | yes refl = yes refl
… | no εs₁≢εs₂ = no λ {refl → εs₁≢εs₂ refl}


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Categories.DistLatticeSheaf.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Powerset
open import Cubical.Data.Sigma
open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Nat.Order
open import Cubical.Data.FinData
open import Cubical.Data.FinData.Order

open import Cubical.Relation.Binary.Poset

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Semilattice
open import Cubical.Algebra.Lattice
open import Cubical.Algebra.DistLattice
open import Cubical.Algebra.DistLattice.Basis
open import Cubical.Algebra.DistLattice.BigOps

open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Limits.Pullback
open import Cubical.Categories.Limits.Terminal
open import Cubical.Categories.Limits.Limits
open import Cubical.Categories.Limits.RightKan
open import Cubical.Categories.Instances.Functors
open import Cubical.Categories.Instances.CommRings
open import Cubical.Categories.Instances.Poset
open import Cubical.Categories.Instances.Semilattice
open import Cubical.Categories.Instances.Lattice
open import Cubical.Categories.Instances.DistLattice

open import Cubical.Categories.DistLatticeSheaf.Diagram

private
  variable
    ℓ ℓ' ℓ'' : Level

module PreSheafExtension (L : DistLattice ℓ) (C : Category ℓ' ℓ'')
                         (limitC : Limits {ℓ} {ℓ} C) (L' : ℙ (fst L)) where

 open Functor

 private
  DLCat = DistLatticeCategory L
  DLSubCat = ΣPropCat  DLCat L'
  DLPreSheaf = Functor (DLCat ^op) C
  DLSubPreSheaf = Functor (DLSubCat ^op) C

  i : Functor DLSubCat DLCat
  F-ob i = fst
  F-hom i f = f
  F-id i = refl
  F-seq i _ _ = refl

 DLRan : DLSubPreSheaf → DLPreSheaf
 DLRan = Ran limitC (i ^opF)

module _ (L : DistLattice ℓ) (C : Category ℓ' ℓ'') (T : Terminal C) where
  open Category hiding (_⋆_)
  open Functor
  open Order (DistLattice→Lattice L)
  open DistLatticeStr (snd L)
  open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice L))
  open MeetSemilattice (Lattice→MeetSemilattice (DistLattice→Lattice L))
      using (∧≤RCancel ; ∧≤LCancel)
  open PosetStr (IndPoset .snd) hiding (_≤_)

  𝟙 : ob C
  𝟙 = terminalOb C T

  private
   DLCat : Category ℓ ℓ
   DLCat = DistLatticeCategory L

  open Category DLCat

  -- C-valued presheaves on a distributive lattice
  DLPreSheaf : Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
  DLPreSheaf = Functor (DLCat ^op) C

  module _ (x y : L .fst)where
    hom-∨₁ : DLCat [ x , x ∨l y ]
    hom-∨₁ = ∨≤RCancel _ _

    hom-∨₂ : DLCat [ y , x ∨l y ]
    hom-∨₂ = ∨≤LCancel _ _

    hom-∧₁ : DLCat [ x ∧l y , x ]
    hom-∧₁ = ≤m→≤j _ _ (∧≤RCancel _ _)

    hom-∧₂ : DLCat [ x ∧l y , y ]
    hom-∧₂ = ≤m→≤j _ _ (∧≤LCancel _ _)

    {-
       x ∧ y ----→   x
         |           |
         |    sq     |
         V           V
         y   ----→ x ∨ y
    -}
    sq : hom-∧₂ ⋆ hom-∨₂ ≡ hom-∧₁ ⋆ hom-∨₁
    sq = is-prop-valued (x ∧l y) (x ∨l y) (hom-∧₂ ⋆ hom-∨₂) (hom-∧₁ ⋆ hom-∨₁)

    {-
      F(x ∨ y) ----→ F(x)
         |            |
         |     Fsq    |
         V            V
        F(y) ------→ F(x ∧ y)
    -}
    Fsq : (F : DLPreSheaf)
        → F .F-hom hom-∨₂ ⋆⟨ C ⟩ F .F-hom hom-∧₂ ≡
          F .F-hom hom-∨₁ ⋆⟨ C ⟩ F .F-hom hom-∧₁
    Fsq F = F-square F sq

  isDLSheafPullback : (F : DLPreSheaf) → Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
  isDLSheafPullback F = (F-ob F 0l ≡ 𝟙)
                      × ((x y : L .fst) → isPullback C _ _ _ (Fsq x y F))

  -- TODO: might be better to define this as a record
  DLSheafPullback : Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
  DLSheafPullback = Σ[ F ∈ DLPreSheaf ] isDLSheafPullback F

  -- Now for the proper version using limits of the right kind:
  open Join L
  isDLSheaf : (F : DLPreSheaf) → Type _
  isDLSheaf F = ∀ (n : ℕ) (α : FinVec (fst L) n) → isLimCone _ _ (F-cone F (⋁Cone L α))
  --TODO: Equivalence of isDLSheaf and isDLSheafPullback

module SheafOnBasis (L : DistLattice ℓ) (C : Category ℓ' ℓ'') (T : Terminal C)
                    (L' : ℙ (fst L)) (hB : IsBasis L L') where

 open Category
 open Functor

 open DistLatticeStr ⦃...⦄
 open SemilatticeStr ⦃...⦄
 open IsBasis hB

 private
  DLCat = DistLatticeCategory L
  BasisCat = ΣPropCat  DLCat L'
  DLBasisPreSheaf = Functor (BasisCat ^op) C

  -- to avoid writing 𝟙 L C T
  1c : ob C
  1c = terminalOb C T

  instance
   _ = snd L
   _ = snd (Basis→MeetSemilattice L L' hB)

 module condSquare (x y : ob BasisCat) (x∨y∈L' : fst x ∨l fst y ∈ L') where

  private
   x∨y : ob BasisCat -- = Σ[ x ∈ L ] (x ∈ L')
   x∨y = fst x ∨l fst y , x∨y∈L'

  {-
     x ∧ y ----→   x
       |           |
       |    sq     |
       V           V
       y   ----→ x ∨ y

     but as a square in BasisCat
  -}
  Bsq : seq' BasisCat {x = x · y} {y = y} {z = x∨y} (hom-∧₂ L C T (fst x) (fst y))
                                                    (hom-∨₂ L C T (fst x) (fst y))
      ≡ seq' BasisCat {x = x · y} {y = x} {z = x∨y} (hom-∧₁ L C T (fst x) (fst y))
                                                    (hom-∨₁ L C T (fst x) (fst y))
  Bsq = sq L C T (fst x) (fst y)

  {-
    F(x ∨ y) ----→ F(x)
       |            |
       |     Fsq    |
       V            V
      F(y) ------→ F(x ∧ y)

    square in C but now F is only presheaf on BasisCat
  -}
  BFsq : (F : DLBasisPreSheaf)
       → seq' C {x = F .F-ob x∨y} {y = F .F-ob y} {z = F .F-ob (x · y)}
                (F .F-hom (hom-∨₂ L C T (fst x) (fst y)))
                (F .F-hom (hom-∧₂ L C T (fst x) (fst y)))
       ≡ seq' C {x = F .F-ob x∨y} {y = F .F-ob x} {z = F .F-ob (x · y)}
                (F .F-hom (hom-∨₁ L C T (fst x) (fst y)))
                (F .F-hom (hom-∧₁ L C T (fst x) (fst y)))
  BFsq F = F-square F Bsq

 -- On a basis this is weaker than the definition below!
 isDLBasisSheafPullback : DLBasisPreSheaf → Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
 isDLBasisSheafPullback F = ((0∈L' : 0l ∈ L') → F .F-ob (0l , 0∈L') ≡ 1c)
                          × ((x y : ob BasisCat) (x∨y∈L' : fst x ∨l fst y ∈ L')
                               → isPullback C _ _ _ (BFsq x y x∨y∈L' F))
                                 where open condSquare

 DLBasisSheafPullback : Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
 DLBasisSheafPullback = Σ[ F ∈ DLBasisPreSheaf ] isDLBasisSheafPullback F

 -- the correct defintion
 open Join L
 module condCone {n : ℕ} (α : FinVec (ob BasisCat) n) (⋁α∈L' : ⋁ (λ i →  α i .fst) ∈ L') where
   open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice L))
   open PosetStr (IndPoset .snd) hiding (_≤_)
   open MeetSemilattice (Lattice→MeetSemilattice (DistLattice→Lattice L))
        using (∧≤RCancel ; ∧≤LCancel)
   open Order (DistLattice→Lattice L)
   open Cone
   private
     α' : FinVec (fst L) n
     α' i = α i .fst
     ⋁α : ob BasisCat
     ⋁α = ⋁ α' , ⋁α∈L'

   BDiag : Functor (DLShfDiag n) (BasisCat ^op)
   F-ob BDiag (sing i) = α i
   F-ob BDiag (pair i j _) = α i · α j -- α i ∧ α j + basis is closed under ∧
   F-hom BDiag idAr = is-refl _
   F-hom BDiag singPairL = ≤m→≤j _ _ (∧≤RCancel _ _)
   F-hom BDiag singPairR = ≤m→≤j _ _ (∧≤LCancel _ _)
   F-id BDiag = is-prop-valued _ _ _ _
   F-seq BDiag _ _ = is-prop-valued _ _ _ _

   B⋁Cone : Cone BDiag ⋁α
   coneOut B⋁Cone (sing i) = ind≤⋁ α' i
   coneOut B⋁Cone (pair i _ _) = is-trans _ (α' i) _ (≤m→≤j _ _ (∧≤RCancel _ _)) (ind≤⋁ α' i)
   coneOutCommutes B⋁Cone _ = is-prop-valued _ _ _ _

 isDLBasisSheaf : DLBasisPreSheaf → Type _
 isDLBasisSheaf F = ∀ {n : ℕ} (α : FinVec (ob BasisCat) n) (⋁α∈L' : ⋁ (λ i →  α i .fst) ∈ L')
                  → isLimCone _ _ (F-cone F (B⋁Cone  α ⋁α∈L'))
                    where open condCone

  -- To prove the statement we probably need that C is:
  -- 1. univalent
  -- 2. has finite limits (or pullbacks and a terminal object)
  -- 3. isGroupoid (C .ob)
  -- The last point is not strictly necessary, but we have to have some
  -- control over the hLevel as we want to write F(x) in terms of its
  -- basis cover which is information hidden under a prop truncation...
  -- Alternatively we just prove the statement for C = CommRingsCategory

  -- TODO: is unique existence expressed like this what we want?
  -- statement : (F' : DLBasisSheaf)
  --           → ∃![ F ∈ DLSheaf L C T ] ((x : fst L) → (x ∈ L') → CatIso C (F-ob (fst F) x) (F-ob (fst F') x)) -- TODO: if C is univalent the CatIso could be ≡?
  -- statement (F' , h1 , hPb) = ?

  -- It might be easier to prove all of these if we use the definition
  -- in terms of particular limits instead

  -- Scrap zone:

  -- -- Sublattices: upstream later
  -- record isSublattice (L' : ℙ (fst L)) : Type ℓ where
  --   field
  --     1l-closed  : 1l ∈ L'
  --     0l-closed  : 0l ∈ L'
  --     ∧l-closed  : {x y : fst L} → x ∈ L' → y ∈ L' → x ∧l y ∈ L'
  --     ∨l-closed  : {x y : fst L} → x ∈ L' → y ∈ L' → x ∨l y ∈ L'

  -- open isSublattice

  -- Sublattice : Type (ℓ-suc ℓ)
  -- Sublattice = Σ[ L' ∈ ℙ (fst L) ] isSublattice L'

  -- restrictDLSheaf : DLSheaf → Sublattice → DLSheaf
  -- F-ob (fst (restrictDLSheaf F (L' , HL'))) x = {!F-ob (fst F) x!} -- Hmm, not nice...
  -- F-hom (fst (restrictDLSheaf F L')) = {!!}
  -- F-id (fst (restrictDLSheaf F L')) = {!!}
  -- F-seq (fst (restrictDLSheaf F L')) = {!!}
  -- snd (restrictDLSheaf F L') = {!!}

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
-- This is a selection of useful functions and definitions
-- from the standard library that we tend to use a lot.
module LibraBFT.Prelude where

  open import Level
    renaming (suc to ℓ+1; zero to ℓ0; _⊔_ to _ℓ⊔_)
    public

  1ℓ : Level
  1ℓ = ℓ+1 0ℓ

  open import Agda.Builtin.Unit
    public

  open import Data.Unit.NonEta
    public

  open import Data.Empty
    public

  open import Data.Nat
    renaming (_≟_ to _≟ℕ_; _≤?_ to _≤?ℕ_)
    public

  open import Data.Nat.Properties
    hiding (≡-irrelevant)
    public

  open import Data.List
    renaming (map to List-map ; filter to List-filter ; lookup to List-lookup;
              tabulate to List-tabulate)
    hiding (fromMaybe; [_])
    public

  open import Data.List.Properties
    renaming (≡-dec to List-≡-dec; length-map to List-length-map; map-compose to List-map-compose)
    using (∷-injective; length-++; map-++-commute; sum-++-commute; map-tabulate; ++-identityʳ)
    public

  open import Data.List.Relation.Binary.Subset.Propositional
    renaming (_⊆_ to _⊆List_)
    public

  open import Data.List.Relation.Unary.Any
    using (Any; here; there)
    renaming (lookup to Any-lookup; map to Any-map; satisfied to Any-satisfied
             ;index to Any-index; any to Any-any)
    public

  open import Data.List.Relation.Unary.Any.Properties
    using    (¬Any[])
    renaming ( map⁺       to Any-map⁺
             ; map⁻       to Any-map⁻
             ; concat⁺    to Any-concat⁺
             ; concat⁻    to Any-concat⁻
             ; ++⁻        to Any-++⁻
             ; ++⁺ʳ       to Any-++ʳ
             ; ++⁺ˡ       to Any-++ˡ
             ; singleton⁻ to Any-singleton⁻
             ; tabulate⁺  to Any-tabulate⁺
             )
    public

  open import Data.List.Relation.Unary.All
    using (All; []; _∷_)
    renaming (head to All-head; tail to All-tail;
              lookup to All-lookup; tabulate to All-tabulate;
              reduce to All-reduce)
    public

  open import Data.List.Relation.Unary.All.Properties
    renaming ( tabulate⁻ to All-tabulate⁻
             ; tabulate⁺ to All-tabulate⁺
             ; map⁺      to All-map⁺
             ; map⁻      to All-map⁻
             )
    public

  open import Data.List.Membership.Propositional
    using (_∈_; _∉_)
    public

  open import Data.Vec
    using (Vec; []; _∷_)
    renaming (replicate to Vec-replicate; lookup to Vec-lookup
             ;map to Vec-map; head to Vec-head; tail to Vec-tail
             ;updateAt to Vec-updateAt; tabulate to Vec-tabulate
             ;allFin to Vec-allFin; toList to Vec-toList; fromList to Vec-fromList
             ;_++_ to _Vec-++_)
    public

  open import Data.Vec.Relation.Unary.All
    using ([]; _∷_)
    renaming (All to Vec-All; lookup to Vec-All-lookup)
    public

  open import Data.Vec.Properties
    using ()
    renaming (updateAt-minimal to Vec-updateAt-minimal
             ;[]=⇒lookup to Vec-[]=⇒lookup
             ;lookup⇒[]= to Vec-lookup⇒[]=
             ;lookup∘tabulate to Vec-lookup∘tabulate
             ;≡-dec to Vec-≡-dec)
    public

  open import Data.List.Relation.Binary.Pointwise
    using (decidable-≡)
    public

  open import Data.Bool
    renaming (_≟_ to _≟Bool_)
    hiding (_≤?_; _<_; _<?_; _≤_)
    public

  open import Data.Maybe
    renaming (map to Maybe-map; zip to Maybe-zip ; _>>=_ to _Maybe->>=_)
    hiding (align; alignWith; zipWith)
    public

  open import Data.Maybe.Relation.Unary.Any
    renaming (Any to Maybe-Any; dec to Maybe-Any-dec)
    hiding (map; zip; zipWith; unzip ; unzipWith)
    public

  maybe-any-⊥ : ∀{a}{A : Set a} → Maybe-Any {A = A} (λ _ → ⊤) nothing → ⊥
  maybe-any-⊥ ()

  open import Data.Maybe.Properties
    using (just-injective)
    renaming (≡-dec to Maybe-≡-dec)
    public

  open import Data.Fin
    using (Fin; suc; zero; fromℕ; fromℕ< ; toℕ ; cast)
    renaming (_≟_ to _≟Fin_; _≤?_ to _≤?Fin_; _≤_ to _≤Fin_ ; _<_ to _<Fin_;
              inject₁ to Fin-inject₁; inject+ to Fin-inject+)
    public

  fins : (n : ℕ) → List (Fin n)
  fins n = Vec-toList (Vec-allFin n)

  open import Data.Fin.Properties
    using (toℕ-injective)
    renaming (<-cmp to Fin-<-cmp; <⇒≢ to <⇒≢Fin)
    public

  open import Relation.Binary.PropositionalEquality
    hiding (decSetoid)
    public

  open import Relation.Binary.HeterogeneousEquality
    using (_≅_)
    renaming (cong to ≅-cong; cong₂ to ≅-cong₂)
    public

  open import Relation.Binary
    public

  ≡-irrelevant : ∀{a}{A : Set a} → Irrelevant {a} {A} _≡_
  ≡-irrelevant refl refl = refl

  to-witness-lemma : ∀{ℓ}{A : Set ℓ}{a : A}{f : Maybe A}(x : Is-just f)
                   → to-witness x ≡ a → f ≡ just a
  to-witness-lemma (just x) refl = refl

  open import Data.Sum
    renaming ([_,_] to either; map to ⊎-map)
    public

  open import Function
    using (_∘_; id; case_of_; _on_; typeOf; flip; const)
    public

  open import Data.Product
    renaming (map to ×-map; map₂ to ×-map₂; map₁ to ×-map₁; <_,_> to split; swap to ×-swap)
    hiding (zip)
    public

  open import Data.Product.Properties
    public

  open import Relation.Nullary
    hiding (Irrelevant; proof)
    public

  open import Relation.Nullary.Decidable
    hiding (map)
    public

  infix 0 if-yes_then_else_
  infix 0 if-dec_then_else_
  if-yes_then_else_ : {A B : Set} → Dec A → (A → B) → (¬ A → B) → B
  if-yes (yes prf) then f else _ = f prf
  if-yes (no  prf) then _ else g = g prf

  if-dec_then_else_ : {A B : Set} → Dec A → B → B → B
  if-dec x then f else g = if-yes x then const f else const g

  open import Relation.Nullary.Negation
    using (contradiction; contraposition)
    public

  open import Relation.Binary
    using (Setoid; IsPreorder)
    public

  -- Evidence that a function is not injective
  NonInjective : ∀{a b c}{A : Set a}{B : Set b}
               → (_≈_ : Rel A c)
               → (A → B) → Set (a ℓ⊔ b ℓ⊔ c)
  NonInjective {A = A} _≈_ f
    = Σ (A × A) (λ { (x₁ , x₂) → ¬ (x₁ ≈ x₂) × f x₁ ≡ f x₂ })

  NonInjective-≡ : ∀{a b}{A : Set a}{B : Set b}
                 → (A → B) → Set (a ℓ⊔ b)
  NonInjective-≡ = NonInjective _≡_

  NonInjective-∘ : ∀{a b c}{A : Set a}{B : Set b}{C : Set c}
                 → {f : A → B}(g : B → C)
                 → NonInjective-≡  f
                 → NonInjective-≡ (g ∘ f)
  NonInjective-∘ g ((x0 , x1) , (x0≢x1 , fx0≡fx1))
    = ((x0 , x1) , x0≢x1 , (cong g fx0≡fx1))

  --------------------------------------------
  -- Handy fmap and bind for specific types --

  _<M$>_ : ∀{a b}{A : Set a}{B : Set b}
         → (f : A → B)
         → Maybe A → Maybe B
  _<M$>_ = Maybe-map

  <M$>-univ : ∀{a b}{A : Set a}{B : Set b}
            → (f : A → B)(x : Maybe A)
            → {y : B} → f <M$> x ≡ just y
            → ∃[ x' ] (x ≡ just x' × f x' ≡ y)
  <M$>-univ f (just x) refl = x , (refl , refl)

  maybe-lift : {A : Set}
             → {mx : Maybe A}{x : A}
             → (P : A → Set)
             → P x → mx ≡ just x
             → maybe {B = const Set} P ⊥ mx
  maybe-lift {mx = just .x} {x} P px refl = px

  <M$>-nothing : ∀ {a b}{A : Set a}{B : Set b}(f : A → B)
               → f <M$> nothing ≡ nothing
  <M$>-nothing _ = refl

  _<⊎$>_ : ∀{a b c}{A : Set a}{B : Set b}{C : Set c}
         → (A → B) → C ⊎ A → C ⊎ B
  f <⊎$> (inj₁ hb) = inj₁ hb
  f <⊎$> (inj₂ x)  = inj₂ (f x)

  _⊎⟫=_ : ∀{a b c}{A : Set a}{B : Set b}{C : Set c}
        → C ⊎ A → (A → C ⊎ B) → C ⊎ B
  (inj₁ x) ⊎⟫= _ = inj₁ x
  (inj₂ a) ⊎⟫= f = f a

  -- TODO-1: Maybe this belongs somewhere else?  It's in a similar
  -- category as Optics, so maybe should similarly be in a module that
  -- is separate from the main project?
  ------------------
  -- Guard Syntax --
  --
  -- Example Usage:
  --
  -- > f : ℕ → ℕ
  -- > f x = grd‖ x ≟ℕ 10  ≔ 12
  -- >          ‖ otherwise≔ 40 + 2
  --
  --
  -- > g : ℕ ⊎ ℕ → ℕ
  -- > g x = case x of λ
  -- >     { (inj₁ x) → grd‖ x ≤? 10  ≔ 2 * x
  -- >                     ‖ otherwise≔ 42
  -- >     ; (inj₂ y) → y
  -- >     }
  --
  -- To type: ‖  -->  \Vert
  --          ≔  -->  \:=

  record ToBool {a}(A : Set a) : Set a where
    field
      toBool : A → Bool
  open ToBool {{ ... }} public

  instance
    ToBool-Bool : ToBool Bool
    ToBool-Bool = record { toBool = id }

    ToBool-Dec : ∀{a}{A : Set a} → ToBool (Dec A)
    ToBool-Dec = record { toBool = ⌊_⌋ }

  infix 3 _≔_
  data GuardClause {a}(A : Set a) : Set (ℓ+1 a) where
    _≔_ : {B : Set a}{{ bb : ToBool B }} → B → A → GuardClause A

  infix 3 otherwise≔_
  data Guards {a}(A : Set a) : Set (ℓ+1 a) where
   otherwise≔_ : A → Guards A
   clause     : GuardClause A → Guards A → Guards A

  infixr 2 _‖_
  _‖_ : ∀{a}{A : Set a} → GuardClause A → Guards A → Guards A
  _‖_ = clause

  infix 1 grd‖_
  grd‖_ : ∀{a}{A : Set a} → Guards A → A
  grd‖_ (otherwise≔ a) = a
  grd‖_ (clause (b ≔ a) g)  = if toBool b then a else (grd‖ g)

  Any-satisfied-∈ : ∀{a ℓ}{A : Set a}{P : A → Set ℓ}{xs : List A}
                  → Any P xs → Σ A (λ x → P x × x ∈ xs)
  Any-satisfied-∈ (here px) = _ , (px , here refl)
  Any-satisfied-∈ (there p) = let (a , px , prf) = Any-satisfied-∈ p
                               in (a , px , there prf)

  f-sum : ∀{a}{A : Set a} → (A → ℕ) → List A → ℕ
  f-sum f = sum ∘ List-map f

  open import LibraBFT.Base.Util public

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


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

module Math.NumberTheory.Product.Generic where

-- agda-stdlib
open import Algebra

-- agda-misc
open import Math.NumberTheory.Summation.Generic

-- TODO add syntax
module MonoidProduct {c e} (M : Monoid c e) =
  MonoidSummation M
  renaming
  ( Σ< to Π<
  ; Σ≤ to Π≤
  ; Σ<range to Π<range
  ; Σ≤range to Π≤range
  )
  using ()


text:
postulate
  C : Set
  anything : C

record I : Set where
  constructor c
  field
    f : C

data Wrap : (j : I) → Set where
  wrap : ∀ {j} → Wrap j

-- The following should not pass.
-- It did before the fix of #142.
issue142 : ∀ {j} → Wrap j → C
issue142 {c _} (wrap {c _}) with anything
issue142 {c _} (wrap .{c anything}) | z = z

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Relation.Unary using ( ∅ ; _∪_ )
open import Web.Semantic.DL.Signature using ( Signature ; CN ; RN )
open import Web.Semantic.Util using ( Subset ; ⁅_⁆ )

module Web.Semantic.DL.Role where

data Role (Σ : Signature) : Set where
  ⟨_⟩ : (r : RN Σ) → Role Σ
  ⟨_⟩⁻¹ : (r : RN Σ) → Role Σ

inv : ∀ {Σ} → Role Σ → Role Σ
inv ⟨ r ⟩   = ⟨ r ⟩⁻¹
inv ⟨ r ⟩⁻¹ = ⟨ r ⟩

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


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

   Copyright (c) 2020, 2021 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Types
import      LibraBFT.Yasm.Base as LYB

-- This module provides some definitions and properties that facilitate
-- proofs of properties about a distributed system modeled by Yasm.System
-- paramaterized by some SystemParameters.

module LibraBFT.Yasm.Properties
   (ℓ-EC        : Level)
   (EpochConfig : Set ℓ-EC)
   (epochId     : EpochConfig → EpochId)
   (authorsN    : EpochConfig → ℕ)
   (parms       : LYB.SystemParameters ℓ-EC EpochConfig epochId authorsN)
   -- In addition to the parameters used by the rest of the system model, this module
   -- needs to relate Members to PKs and PeerIds, so that StepPeerState-AllValidParts
   -- can be defined.  This enables the application to prove that honest peers sign
   -- new messages only for their own public key.  The system model does not know that
   -- directly.
   (senderPKOK  : (ec : EpochConfig) → PK → LYB.SystemParameters.PeerId parms → Set)
  where
 open LYB.SystemParameters parms
 open import LibraBFT.Yasm.AvailableEpochs PeerId ℓ-EC EpochConfig epochId authorsN
             using (AvailableEpochs) renaming (lookup'' to EC-lookup)
 import      LibraBFT.Yasm.AvailableEpochs PeerId ℓ-EC EpochConfig epochId authorsN
             as AE
 open import LibraBFT.Yasm.Base   ℓ-EC EpochConfig epochId authorsN
 open import LibraBFT.Yasm.System ℓ-EC EpochConfig epochId authorsN parms
 open import Util.FunctionOverride PeerId _≟PeerId_

 -- A ValidPartForPK collects the assumptions about what a /part/ in the outputs of an honest verifier
 -- satisfies: (i) the epoch field is consistent with the existent epochs and (ii) the verifier is
 -- a member of the associated epoch config, and (iii) has the given PK in that epoch.
 record ValidSenderForPK {e}(𝓔s : AvailableEpochs e)(part : Part)(sender : PeerId)(pk : PK) : Set ℓ-EC where
   constructor mkValidSenderForPK
   field
     vp-epoch           : part-epoch part < e
     vp-ec              : EpochConfig
     vp-ec-≡            : AE.lookup'' 𝓔s vp-epoch ≡ vp-ec
     vp-sender-ok       : senderPKOK vp-ec pk sender
 open ValidSenderForPK public

 -- A valid part remains valid when new epochs are added
 ValidSenderForPK-stable-epoch : ∀{e part α pk}{𝓔s : AvailableEpochs e}(𝓔 : EpochConfigFor e)
                               → ValidSenderForPK 𝓔s part α pk
                               → ValidSenderForPK (AE.append 𝓔 𝓔s) part α pk
 ValidSenderForPK-stable-epoch {pk = pk} {𝓔s = 𝓔s} 𝓔 (mkValidSenderForPK e ec refl vpk) = record
   { vp-epoch           = ≤-step e
   ; vp-ec              = ec
   ; vp-ec-≡            = AE.lookup''-≤-step-lemma 𝓔s 𝓔 e
   ; vp-sender-ok       = vpk
   }

 -- A valid part remains valid
 ValidSenderForPK-stable : ∀{e e' α}{st : SystemState e}{st' : SystemState e'}
                    → Step* st st' → ∀{part pk}
                    → ValidSenderForPK (availEpochs st) part α pk
                    → ValidSenderForPK (availEpochs st') part α pk
 ValidSenderForPK-stable step-0 v = v
 ValidSenderForPK-stable (step-s st (step-epoch 𝓔)) v
   = ValidSenderForPK-stable-epoch 𝓔 (ValidSenderForPK-stable st v)
 ValidSenderForPK-stable (step-s st (step-peer _)) v
   = ValidSenderForPK-stable st v

 sameEpoch⇒sameEC : ∀ {e p1 p2 α1 α2 pk1 pk2}{𝓔s : AvailableEpochs e}
                    → (vp1 : ValidSenderForPK 𝓔s p1 α1 pk1)
                    → (vp2 : ValidSenderForPK 𝓔s p2 α2 pk2)
                    → part-epoch p1 ≡ part-epoch p2
                    → vp-ec vp1 ≡ vp-ec vp2
 sameEpoch⇒sameEC {𝓔s = 𝓔s} vp1 vp2 parts≡ =
   trans (sym (vp-ec-≡ vp1))
         (trans (AE.lookup-𝓔s-injective 𝓔s (vp-epoch vp1) (vp-epoch vp2) parts≡)
                (vp-ec-≡ vp2))

 -- TODO-1 : prove it
 postulate
   ValidSenderForPK⇒ep≡ : ∀ {e p1 p2 α1 pk} {𝓔s : AvailableEpochs e}
                        → WithVerSig pk p1 → WithVerSig pk p2
                        → part-epoch p1 ≡ part-epoch p2
                        → ValidSenderForPK 𝓔s p1 α1 pk
                        → ValidSenderForPK 𝓔s p2 α1 pk

 -- We say that an implementation produces only valid parts iff all parts of every message in the
 -- output of a 'StepPeerState' are either: (i) a valid new part (i.e., the part is valid and no
 -- message with the same signature has been sent previously), or (ii) a message has been sent
 -- with the same signature.
 StepPeerState-AllValidParts : Set ℓ-EC
 StepPeerState-AllValidParts = ∀{e s m part pk initd' outs}{α}{𝓔s : AvailableEpochs e}{st : SystemState e}
   → (r : ReachableSystemState st)
   → Meta-Honest-PK pk
   → StepPeerState α 𝓔s (msgPool st) (initialised st) (peerStates st α) initd' (s , outs)
   → m ∈ outs → part ⊂Msg m → (ver : WithVerSig pk part)
   → (ValidSenderForPK 𝓔s part α pk × ¬ (MsgWithSig∈ pk (ver-signature ver) (msgPool st)))
   ⊎ MsgWithSig∈ pk (ver-signature ver) (msgPool st)

 -- A /part/ was introduced by a specific step when:
 IsValidNewPart : ∀{e e'}{pre : SystemState e}{post : SystemState e'} → Signature → PK → Step pre post → Set ℓ-EC
 IsValidNewPart _ _ (step-epoch _) = Lift (ℓ-EC) ⊥
 -- said step is a /step-peer/ and
 IsValidNewPart {pre = pre} sig pk (step-peer {pid = pid} pstep)
    -- the part has never been seen before
    = ReachableSystemState pre
    × ¬ (MsgWithSig∈ pk sig (msgPool pre))
    × Σ (MsgWithSig∈ pk sig (msgPool (StepPeer-post pstep)))
        (λ m → ValidSenderForPK (availEpochs pre) (msgPart m) (msgSender m) pk)

 -- When we can prove that the implementation provided by 'parms' at the
 -- top of this module satisfies 'StepPeerState-AllValidParts', we can
 -- prove a number of useful structural properties:

 -- TODO-2: Refactor into a file (LibraBFT.Yasm.Properties.Structural) later on
 -- if this grows too large.
 module Structural (sps-avp      : StepPeerState-AllValidParts) where

     -- We can unwind the state and highlight the step where a part was
     -- originally sent. This 'unwind' function combined with Any-Step-elim
     -- enables a powerful form of reasoning. The 'honestVoteEpoch' below
     -- exemplifies this well.
     unwind : ∀{e}{st : SystemState e}(tr : ReachableSystemState st)
            → ∀{p m σ pk} → Meta-Honest-PK pk
            → p ⊂Msg m → (σ , m) ∈ msgPool st → (ver : WithVerSig pk p)
            → Any-Step (IsValidNewPart (ver-signature ver) pk) tr
     unwind (step-s tr (step-epoch _))    hpk p⊂m m∈sm sig
       = step-there (unwind tr hpk p⊂m m∈sm sig)
     unwind (step-s tr (step-peer {pid = β} {outs = outs} {pre = pre} sp)) hpk p⊂m m∈sm sig
       with Any-++⁻ (List-map (β ,_) outs) {msgPool pre} m∈sm
     ...| inj₂ furtherBack = step-there (unwind tr hpk p⊂m furtherBack sig)
     ...| inj₁ thisStep
       with sp
     ...| step-cheat fm isCheat
       with thisStep
     ...| here refl
       with isCheat p⊂m sig
     ...| inj₁ abs    = ⊥-elim (hpk abs)
     ...| inj₂ sentb4
       with unwind tr {p = msgPart sentb4} hpk (msg⊆ sentb4) (msg∈pool sentb4) (msgSigned sentb4)
     ...| res rewrite msgSameSig sentb4 = step-there res
     unwind (step-s tr (step-peer {pid = β} {outs = outs} {pre = pre} sp)) hpk p⊂m m∈sm sig
        | inj₁ thisStep
        | step-honest x
       with Any-satisfied-∈ (Any-map⁻ thisStep)
     ...| (m , refl , m∈outs)
       with sps-avp tr hpk x m∈outs p⊂m sig
     ...| inj₂ sentb4 with unwind tr {p = msgPart sentb4} hpk (msg⊆ sentb4) (msg∈pool sentb4) (msgSigned sentb4)
     ...| res rewrite msgSameSig sentb4 = step-there res
     unwind (step-s tr (step-peer {pid = β} {outs = outs} {pre = pre} sp)) {p} hpk p⊂m m∈sm sig
        | inj₁ thisStep
        | step-honest x
        | (m , refl , m∈outs)
        | inj₁ (valid-part , notBefore) =
               step-here tr (tr , notBefore , MsgWithSig∈-++ˡ (mkMsgWithSig∈ _ _ p⊂m β thisStep sig refl)
                                       , valid-part)

     -- Unwind is inconvenient to use by itself because we have to do
     -- induction on Any-Step-elim. The 'honestPartValid' property below
     -- provides a fairly general result conveniently: for every part
     -- verifiable with an honest PK, there is a msg with the same
     -- signature that is valid for some pid.

     honestPartValid : ∀ {e st} → ReachableSystemState {e} st → ∀ {pk nm v sender}
                     → Meta-Honest-PK pk
                     → v ⊂Msg nm → (sender , nm) ∈ msgPool st → (ver : WithVerSig pk v)
                     → Σ (MsgWithSig∈ pk (ver-signature ver) (msgPool st))
                         (λ msg → (ValidSenderForPK (availEpochs st) (msgPart msg) (msgSender msg) pk))
     honestPartValid {e} {st} r {pk = pk} hpk v⊂m m∈pool ver
     -- We extract two pieces of important information from the place where the part 'v'
     -- was first sent: (a) there is a message with the same signature /in the current pool/
     -- and (b) its epoch is less than e.
        = Any-Step-elim (λ { {st = step-epoch _} ()
                           ; {st = step-peer {pid = pid} ps} (_ , _ , new , valid) tr
                             →  MsgWithSig∈-Step* tr new
                                , ValidSenderForPK-stable tr (subst (λ P → ValidSenderForPK _ P (msgSender (MsgWithSig∈-Step* tr new)) pk)
                                                                         (MsgWithSig∈-Step*-part tr new)
                                                                         (subst (λ sndr → ValidSenderForPK _ _ sndr pk)
                                                                                (MsgWithSig∈-Step*-sender tr new)
                                                                                valid))
                           })
                        (unwind r hpk v⊂m m∈pool ver)

     -- Unforgeability is also an important property stating that every part that is
     -- verified with an honest public key has either been sent by α or is a replay
     -- of another message sent before.
     ext-unforgeability'
       : ∀{e α m part pk}{st : SystemState e} → ReachableSystemState st
       -- If a message m has been sent by α, containing part
       → (α , m) ∈ msgPool st → part ⊂Msg m
       -- And the part can be verified with an honest public key,
       → (sig : WithVerSig pk part) → Meta-Honest-PK pk
       -- then either the part is a valid part by α (meaning that α can
       -- sign the part itself) or a message with the same signature has
       -- been sent previously.
       → ValidSenderForPK (availEpochs st) part α pk
       ⊎ MsgWithSig∈ pk (ver-signature sig) (msgPool st)
     ext-unforgeability' (step-s st (step-epoch 𝓔)) m∈sm p⊆m sig hpk
       = ⊎-map (ValidSenderForPK-stable-epoch 𝓔) id (ext-unforgeability' st m∈sm p⊆m sig hpk)
     ext-unforgeability' {part = part} (step-s st (step-peer {pid = β} {outs = outs} {pre = pre} sp)) m∈sm p⊆m sig hpk
       with Any-++⁻ (List-map (β ,_) outs) {msgPool pre} m∈sm
     ...| inj₂ furtherBack = MsgWithSig∈-++ʳ <⊎$> (ext-unforgeability' st furtherBack p⊆m sig hpk)
     ...| inj₁ thisStep
       with sp
     ...| step-cheat fm isCheat
       with thisStep
     ...| here refl
       with isCheat p⊆m sig
     ...| inj₁ abs    = ⊥-elim (hpk abs)
     ...| inj₂ sentb4 = inj₂ (MsgWithSig∈-++ʳ sentb4)
     ext-unforgeability' {α = α} {m = m} {part = part} (step-s st (step-peer {pid = β} {outs = outs} {pre = pre} sp)) m∈sm p⊆m sig hpk
        | inj₁ thisStep
        | step-honest x
       with Any-satisfied-∈ (Any-map⁻ thisStep)
     ...| (m , refl , m∈outs) = ⊎-map proj₁ MsgWithSig∈-++ʳ (sps-avp st hpk x m∈outs p⊆m sig)

     -- The ext-unforgeability' property can be collapsed in a single clause.

     -- TODO-2: so far, ext-unforgeability is used only to get a MsgWithSig∈ that is passed to
     -- msgWithSigSentByAuthor, which duplicates some of the reasoning in the proof of
     -- ext-unforgeability'; should these properties possibly be combined into one simpler proof?
     ext-unforgeability
       : ∀{e α₀ m part pk}{st : SystemState e} → ReachableSystemState st
       → (α₀ , m) ∈ msgPool st → part ⊂Msg m
       → (sig : WithVerSig pk part) → Meta-Honest-PK pk
       → MsgWithSig∈ pk (ver-signature sig) (msgPool st)
     ext-unforgeability {_} {α₀} {m} {st = st} rst m∈sm p⊂m sig hpk
       with ext-unforgeability' rst m∈sm p⊂m sig hpk
     ...| inj₁ p
        = mkMsgWithSig∈ _ _ p⊂m α₀ m∈sm sig refl
     ...| inj₂ sentb4 = sentb4

     ¬cheatForgeNew : ∀ {e pid pk vsig mst outs m}{st : SystemState e}
                    → (sp : StepPeer st pid mst outs)
                    → outs ≡ m ∷ []
                    → (ic : isCheat sp)
                    → Meta-Honest-PK pk
                    → MsgWithSig∈ pk vsig ((pid , m) ∷ msgPool st)
                    → MsgWithSig∈ pk vsig (msgPool st)
     ¬cheatForgeNew sc@(step-cheat fm isCheat) refl _ hpk mws
        with msg∈pool mws
     ...| there m∈pool = mkMsgWithSig∈ (msgWhole mws) (msgPart mws) (msg⊆ mws) (msgSender mws) m∈pool (msgSigned mws) (msgSameSig mws)
     ...| here m∈pool
        with isCheat (subst (msgPart mws ⊂Msg_) (cong proj₂ m∈pool) (msg⊆ mws)) (msgSigned mws)
     ...| inj₁ dis = ⊥-elim (hpk dis)
     ...| inj₂ mws' rewrite msgSameSig mws = mws'

     msgWithSigSentByAuthor : ∀ {e pk sig}{st : SystemState e}
                            → ReachableSystemState st
                            → Meta-Honest-PK pk
                            → MsgWithSig∈ pk sig (msgPool st)
                            → Σ (MsgWithSig∈ pk sig (msgPool st))
                                λ mws → ValidSenderForPK (availEpochs st) (msgPart mws) (msgSender mws) pk
     msgWithSigSentByAuthor step-0 _ ()
     msgWithSigSentByAuthor (step-s {pre = pre} preach (step-epoch 𝓔)) hpk mws
       rewrite step-epoch-does-not-send pre 𝓔
          with msgWithSigSentByAuthor preach hpk mws
     ...| mws' , vpb =  mws' , ValidSenderForPK-stable {st = pre} (step-s step-0 (step-epoch 𝓔)) vpb
     msgWithSigSentByAuthor {pk = pk} (step-s {pre = pre} preach (step-peer theStep@(step-cheat fm cheatCons))) hpk mws
        with (¬cheatForgeNew theStep refl unit hpk mws)
     ...| mws'
        with msgWithSigSentByAuthor preach hpk mws'
     ...| mws'' , vpb'' = MsgWithSig∈-++ʳ mws'' , vpb''
     msgWithSigSentByAuthor {e} (step-s {pre = pre} preach (step-peer {pid = pid} {outs = outs} (step-honest sps))) hpk mws
       with Any-++⁻ (List-map (pid ,_) outs) {msgPool pre} (msg∈pool mws)
     ...| inj₂ furtherBack
       with msgWithSigSentByAuthor preach hpk (MsgWithSig∈-transp mws furtherBack)
     ...| mws' , vpb' =  MsgWithSig∈-++ʳ mws' , vpb'

     msgWithSigSentByAuthor {e} (step-s {pre = pre} preach (step-peer {pid = pid} {outs = outs} (step-honest sps))) hpk mws
        | inj₁ thisStep
        with Any-satisfied-∈ (Any-map⁻ thisStep)
     ...| (m' , refl , m∈outs)
        with sps-avp preach hpk sps m∈outs (msg⊆ mws) (msgSigned mws)
     ...| inj₁ (vpbα₀ , _) = mws , vpbα₀
     ...| inj₂ mws'
        with msgWithSigSentByAuthor preach hpk mws'
     ...| mws'' , vpb'' rewrite sym (msgSameSig mws) = MsgWithSig∈-++ʳ mws'' , vpb''

     newMsg⊎msgSentB4 :  ∀ {e pk v m pid sndr st' outs} {st : SystemState e}
                   → (r : ReachableSystemState st)
                   → (stP : StepPeer st pid st' outs)
                   → Meta-Honest-PK pk → (sig : WithVerSig pk v)
                   → v ⊂Msg m → (sndr , m) ∈ msgPool (StepPeer-post stP)
                   → (m ∈ outs × ValidSenderForPK (availEpochs st) v pid pk
                      × ¬ (MsgWithSig∈ pk (ver-signature sig) (msgPool st)))
                     ⊎ MsgWithSig∈ pk (ver-signature sig) (msgPool st)
     newMsg⊎msgSentB4 {e} {pk} {v} {m} {pid} {sndr} {_} {outs} {st} r stP pkH sig v⊂m m∈post
        with Any-++⁻ (List-map (pid ,_) outs) m∈post
     ...| inj₂ m∈preSt = inj₂ (mkMsgWithSig∈ m v v⊂m sndr m∈preSt sig refl)
     ...| inj₁ nm∈outs
        with Any-map (cong proj₂) (Any-map⁻ nm∈outs)
     ...| m∈outs
        with stP
     ...| step-honest stH
        with sps-avp r pkH stH m∈outs v⊂m sig
     ...| inj₁ newVote = inj₁ (m∈outs , newVote)
     ...| inj₂ msb4    = inj₂ msb4
     newMsg⊎msgSentB4 {e} {pk} {v} {m} {pid} {sndr} {_} {outs} {st} r stP pkH sig v⊂m m∈post
        | inj₁ nm∈outs
        | here refl
        | step-cheat fm ic
          = let mws = mkMsgWithSig∈ m v v⊂m pid (here refl) sig refl
            in inj₂ (¬cheatForgeNew {st = st} (step-cheat fm ic) refl unit pkH mws)

 -- This could potentially be more general, for example covering the whole SystemState, rather than
 -- just one peer's state.  However, this would put more burden on the user and is not required so
 -- far.
 CarrierProp : Set₁
 CarrierProp = Part → PeerState → Set

 module _ (P   : CarrierProp) where

  record PropCarrier (pk : PK) (sig : Signature) {e} (st : SystemState e) : Set (ℓ-EC ℓ⊔ (ℓ+1 0ℓ)) where
    constructor mkCarrier
    field
      carrStReach : ReachableSystemState st -- Enables use of invariants when proving that steps preserve carrProp
      carrSent    : MsgWithSig∈ pk sig (msgPool st)
      carrValid   : ValidSenderForPK (availEpochs st) (msgPart carrSent) (msgSender carrSent) pk
      carrProp    : P (msgPart carrSent) (peerStates st (msgSender carrSent))
  open PropCarrier public

  PeerStepPreserves : Set (ℓ+1 ℓ0 ℓ⊔ ℓ-EC)
  PeerStepPreserves = ∀ {e initd' ps' outs pk sig}{pre : SystemState e}
                      → (r : ReachableSystemState pre)
                      → (pc : PropCarrier pk sig {e} pre)
                      → (sps : StepPeerState {e} (msgSender (carrSent pc))
                                                 (availEpochs pre)
                                                 (msgPool pre)
                                                 (initialised pre)
                                                 (peerStates pre (msgSender (carrSent pc)))
                                                 initd'
                                                 (ps' , outs))
                      → P (msgPart (carrSent pc)) ps'

  module _ (PSP : PeerStepPreserves) where

    Carrier-transp : ∀ {e' e'' pk sig} {pre : SystemState e'}{post : SystemState e''}
                   → (theStep : Step pre post)
                   → PropCarrier pk sig pre
                   → PropCarrier pk sig post
    Carrier-transp {pre = pre} {post} (step-epoch ec) (mkCarrier r mws vpk lvr) =
       mkCarrier (step-s r (step-epoch ec)) mws (ValidSenderForPK-stable-epoch ec vpk) lvr
    Carrier-transp {e' = e'} {pre = pre} {post} theStep@(step-peer {pid = pid} {st'} {pre = .pre} sps) pc@(mkCarrier r mws vpk prop)
       with step-s r theStep
    ...| postReach
       with sps
    ...| step-cheat fm isch = mkCarrier postReach (MsgWithSig∈-++ʳ mws) vpk
           (subst (λ ps → P (msgPart mws) (ps (msgSender mws))) (sym (cheatStepDNMPeerStates {pre = pre} (step-cheat fm isch) unit)) prop)
    -- PeerStates not changed by cheat steps
    ...| step-honest {st = st} sps'
       with msgSender mws ≟PeerId pid
    ...| no neq   = mkCarrier postReach (MsgWithSig∈-++ʳ mws) vpk
                              (subst (λ ps → P (msgPart mws) ps) (override-target-≢ {f = peerStates pre} neq) prop)
    ...| yes refl = mkCarrier postReach (MsgWithSig∈-++ʳ mws) vpk
                              (subst (λ ps → P (msgPart mws) ps) (sym override-target-≡) (PSP r pc sps'))

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
module Issue252 where

data I : Set where
  zero : I

data D : I → Set where
  c : ∀ i → D i → D i

id : I → I
id i = i

index : ∀ i → D i → I
index i _ = i

foo : ∀ i → D i → D zero
foo .i (c i d) with id i
foo ._ (c i d) | zero = d

bar : ∀ i → D i → D zero
bar .i (c i d) with index i d
bar ._ (c i d) | zero = d

-- In the context of the first goal d has type D i′, in the second it
-- has type D i. Well, not any more.

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Thesis.SIRelBigStep.Normalization where

open import Thesis.SIRelBigStep.Lang

open import Data.Unit.Base hiding (_≤_)
open import Data.Product
open import Relation.Binary.PropositionalEquality

-- Define logical relation for normalization. Adapted from TAPL Ch. 12.
mutual
  normT : ∀ {Γ} τ (t : Term Γ τ) (ρ : ⟦ Γ ⟧Context) → Set
  normT τ t ρ = Σ[ v ∈ Val τ ] ρ ⊢ t ↓[ no ] v × normV τ v

  normV : ∀ τ (v : Val τ) → Set
  normV (σ ⇒ τ) (closure t ρ) = ∀ (v : Val σ) → (vv : normV _ v) → normT τ t (v • ρ)
  normV (pair τ1 τ2) (pairV v1 v2) = normV _ v1 × normV _ v2
  normV nat (natV n) = ⊤

normρ : ∀ Γ (ρ : ⟦ Γ ⟧Context) → Set
normρ ∅ ∅ = ⊤
normρ (τ • Γ) (v • ρ) = normV τ v × normρ Γ ρ

⟦_⟧VarNorm : ∀ {Γ τ} (x : Var Γ τ) {ρ} →
  normρ Γ ρ →
  normV τ (⟦ x ⟧Var ρ)
⟦ this ⟧VarNorm   {v • ρ} (vv , ρρ) = vv
⟦ that x ⟧VarNorm {v • ρ} (vv , ρρ) = ⟦ x ⟧VarNorm ρρ

-- Prove fundamental property.
normT-fund : ∀ {τ Γ} (t : Term Γ τ) ρ (ρρ : normρ Γ ρ) →
  normT τ t ρ

normV-fund-const : ∀ {τ} (c : Const τ) → normV τ (eval-const c)
normV-fund-const (lit n) = tt

normV-fund-sval : ∀ {τ Γ} (sv : SVal Γ τ) ρ (ρρ : normρ Γ ρ) → normV τ (eval sv ρ)
normV-fund-sval (var x) ρ ρρ = ⟦ x ⟧VarNorm ρρ
normV-fund-sval (abs t) ρ ρρ v vv = normT-fund t (v • ρ) (vv , ρρ)
normV-fund-sval (cons sv1 sv2) ρ ρρ = normV-fund-sval sv1 ρ ρρ , normV-fund-sval sv2 ρ ρρ
normV-fund-sval (const c) ρ ρρ = normV-fund-const c

-- Not inlined because it gives the right type ascription to the derivation `val sv`.
normT-fund-sval : ∀ {τ Γ} (sv : SVal Γ τ) ρ (ρρ : normρ Γ ρ) → normT τ (val sv) ρ
normT-fund-sval sv ρ ρρ = eval sv ρ , val sv , normV-fund-sval sv ρ ρρ

normV-fund-primitive : ∀ {σ τ} p →
  ∀ v → (vv : normV σ v) →
  normV τ (eval-primitive p v)
normV-fund-primitive succ (natV n) vv = tt
normV-fund-primitive add (pairV (natV m) (natV n)) vv = tt

open import Data.Nat
normT-fund (val sv) ρ ρρ = normT-fund-sval sv ρ ρρ
normT-fund (primapp p sv) ρ ρρ = eval-primitive p (eval sv ρ) , primapp p sv , normV-fund-primitive p (eval sv ρ) (normV-fund-sval sv ρ ρρ)
normT-fund (app vs vt) ρ ρρ with normT-fund-sval vs ρ ρρ | normT-fund-sval vt ρ ρρ
... | closure t ρ₁ , ↓fv , fvv | av , ↓av , avv with fvv av avv
... | v , ↓v , vv = v , app zero _ ↓fv ↓av ↓v , vv
normT-fund (lett s t) ρ ρρ with normT-fund s ρ ρρ
... | sv , ↓s , svv with normT-fund t (sv • ρ) (svv , ρρ)
... | tv , ↓t , tvv = tv , lett zero zero sv s t ↓s ↓t , tvv

-- Deduce from fundamental property that all terms indeed normalize.
normalize : ∀ {τ} (t : Term ∅ τ) → Σ[ v ∈ Val τ ] ∅ ⊢ t ↓[ no ] v
normalize t with normT-fund t ∅ tt
... | v , ↓ , _ = v , ↓