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

open import Categories.Category.Monoidal
open import Categories.Functor.Monoidal

module Categories.NaturalTransformation.NaturalIsomorphism.Monoidal
  where

open import Level
open import Data.Product using (_,_)
open import Relation.Binary using (IsEquivalence; Setoid)

open import Categories.Category.Product
import Categories.Category.Monoidal.Reasoning as MonoidalReasoning
import Categories.Category.Monoidal.Utilities as MonoidalUtilities
open import Categories.Functor hiding (id)
open import Categories.Functor.Monoidal.Properties using () renaming
  ( idF-Monoidal to idFˡ  ; idF-StrongMonoidal to idFˢ
  ; ∘-Monoidal   to _∘Fˡ_ ; ∘-StrongMonoidal   to _∘Fˢ_
  )
import Categories.Morphism.Reasoning as MorphismReasoning
import Categories.NaturalTransformation.Monoidal as NT
open import Categories.NaturalTransformation.NaturalIsomorphism as NI
  using (NaturalIsomorphism)

open NaturalIsomorphism using (F⇒G; F⇐G)

-- Monoidal natural isomorphisms between lax monoidal functors.

module Lax where
  open NT.Lax hiding (id)

  module _ {o ℓ e o′ ℓ′ e′}
           {C : MonoidalCategory o ℓ e} {D : MonoidalCategory o′ ℓ′ e′}
           (F G : MonoidalFunctor C D) where

    private
      module C = MonoidalCategory C
      module D = MonoidalCategory D
      module F = MonoidalFunctor F renaming (F to U)
      module G = MonoidalFunctor G renaming (F to U)

    IsMonoidalNaturalIsomorphism : NaturalIsomorphism F.U G.U → Set (o ⊔ ℓ′ ⊔ e′)
    IsMonoidalNaturalIsomorphism α = IsMonoidalNaturalTransformation F G (F⇒G α)

    record MonoidalNaturalIsomorphism : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
      field
        U              : NaturalIsomorphism F.U G.U
        F⇒G-isMonoidal : IsMonoidalNaturalIsomorphism U

      open NaturalIsomorphism              U              public
      open IsMonoidalNaturalTransformation F⇒G-isMonoidal public

      open D using (module Equiv)
      open MorphismReasoning D.U using (switch-fromtoˡ; conjugate-from)
      open MonoidalUtilities D.monoidal using (_⊗ᵢ_)

      F⇐G-isMonoidal : IsMonoidalNaturalTransformation G F (F⇐G U)
      F⇐G-isMonoidal = record
        { ε-compat      = Equiv.sym (switch-fromtoˡ FX≅GX ε-compat)
        ; ⊗-homo-compat =
            conjugate-from (FX≅GX ⊗ᵢ FX≅GX) FX≅GX (Equiv.sym ⊗-homo-compat)
        }

      F⇒G-monoidal : MonoidalNaturalTransformation F G
      F⇒G-monoidal = record { U = F⇒G U ; isMonoidal = F⇒G-isMonoidal }

      F⇐G-monoidal : MonoidalNaturalTransformation G F
      F⇐G-monoidal = record { U = F⇐G U ; isMonoidal = F⇐G-isMonoidal }

    infix 4 _≃_

    _≃_ = MonoidalNaturalIsomorphism

  open MonoidalNaturalTransformation using (isMonoidal)
  open MonoidalNaturalIsomorphism

  -- Identity and compositions

  module _ {o ℓ e o′ ℓ′ e′}
           {C : MonoidalCategory o ℓ e} {D : MonoidalCategory o′ ℓ′ e′} where

    infixr 9 _ⓘᵥ_

    id : {F : MonoidalFunctor C D} → F ≃ F
    id = record { U = NI.refl ; F⇒G-isMonoidal = isMonoidal NT.Lax.id }

    _ⓘᵥ_ : {F G H : MonoidalFunctor C D} → G ≃ H → F ≃ G → F ≃ H
    _ⓘᵥ_ α β = record
      { U              = U α NI.ⓘᵥ U β
      ; F⇒G-isMonoidal = isMonoidal (F⇒G-monoidal α ∘ᵥ F⇒G-monoidal β)
      }

    isEquivalence : IsEquivalence _≃_
    isEquivalence = record
      { refl  = id
      ; sym   = λ α → record
        { U              = NI.sym (U α)
        ; F⇒G-isMonoidal = F⇐G-isMonoidal α
        }
      ; trans = λ α β → β ⓘᵥ α
      }

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″}
           {C : MonoidalCategory o ℓ e} {D : MonoidalCategory o′ ℓ′ e′}
           {E : MonoidalCategory o″ ℓ″ e″} where

    infixr 9 _ⓘₕ_ _ⓘˡ_ _ⓘʳ_

    _ⓘₕ_ : {F G : MonoidalFunctor C D} {H I : MonoidalFunctor D E} →
            H ≃ I → F ≃ G → (H ∘Fˡ F) ≃ (I ∘Fˡ G)
    _ⓘₕ_ α β = record
      { U              = U α NI.ⓘₕ U β
      ; F⇒G-isMonoidal = isMonoidal (F⇒G-monoidal α ∘ₕ F⇒G-monoidal β)
      }

    _ⓘˡ_ : {F G : MonoidalFunctor C D}
           (H : MonoidalFunctor D E) → F ≃ G → (H ∘Fˡ F) ≃ (H ∘Fˡ G)
    H ⓘˡ α = id {F = H} ⓘₕ α

    _ⓘʳ_ : {G H : MonoidalFunctor D E} →
           G ≃ H → (F : MonoidalFunctor C D) → (G ∘Fˡ F) ≃ (H ∘Fˡ F)
    α ⓘʳ F = α ⓘₕ id {F = F}

  -- Left and right unitors.

  module _ {o ℓ e o′ ℓ′ e′}
           {C : MonoidalCategory o ℓ e} {D : MonoidalCategory o′ ℓ′ e′}
           {F : MonoidalFunctor C D} where
    private
      module C = MonoidalCategory C
      module D = MonoidalCategory D
      module F = MonoidalFunctor F
    open D hiding (U; id; unitorˡ; unitorʳ)
    open MorphismReasoning D.U using (id-comm-sym)
    open MonoidalReasoning D.monoidal

    unitorˡ : idFˡ D ∘Fˡ F ≃ F
    unitorˡ = record
      { U = NI.unitorˡ
      ; F⇒G-isMonoidal = record
        { ε-compat      = identityˡ ○ identityʳ
        ; ⊗-homo-compat = λ {X Y} → begin
            D.id D.∘ F.⊗-homo.η (X , Y) D.∘ D.id  ≈⟨ identityˡ ⟩
            F.⊗-homo.η (X , Y) D.∘ D.id           ≈˘⟨ refl⟩∘⟨ ⊗.identity ⟩
            F.⊗-homo.η (X , Y) D.∘ D.id ⊗₁ D.id   ∎
        }
      }

    unitorʳ : F ∘Fˡ idFˡ C ≃ F
    unitorʳ = record
      { U               = NI.unitorʳ
      ; F⇒G-isMonoidal  = record
        { ε-compat      = begin
            D.id ∘ F.₁ C.id ∘ F.ε  ≈⟨ identityˡ ⟩
            F.₁ C.id ∘ F.ε         ≈⟨ F.identity ⟩∘⟨refl ⟩
            D.id ∘ F.ε             ≈⟨ identityˡ ⟩
            F.ε ∎
        ; ⊗-homo-compat = λ {X Y} → begin
            D.id D.∘ F.₁ C.id ∘ F.⊗-homo.η (X , Y)  ≈⟨ identityˡ ⟩
            F.₁ C.id ∘ F.⊗-homo.η (X , Y)           ≈⟨ F.identity ⟩∘⟨refl ⟩
            D.id ∘ F.⊗-homo.η (X , Y)               ≈⟨ id-comm-sym ⟩
            F.⊗-homo.η (X , Y) D.∘ D.id             ≈˘⟨ refl⟩∘⟨ ⊗.identity ⟩
            F.⊗-homo.η (X , Y) D.∘ D.id ⊗₁ D.id     ∎
        }
      }

  -- Associator.

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴}
           {B : MonoidalCategory o ℓ e} {C : MonoidalCategory o′ ℓ′ e′}
           {D : MonoidalCategory o″ ℓ″ e″} {E : MonoidalCategory o‴ ℓ‴ e‴}
           {F : MonoidalFunctor B C} {G : MonoidalFunctor C D}
           {H : MonoidalFunctor D E} where
    private
      module D = MonoidalCategory D
      module E = MonoidalCategory E
      module F = MonoidalFunctor F
      module G = MonoidalFunctor G
      module H = MonoidalFunctor H
    open E hiding (U; id; associator)
    open MorphismReasoning E.U
    open MonoidalReasoning E.monoidal

    associator : (H ∘Fˡ G) ∘Fˡ F ≃ H ∘Fˡ (G ∘Fˡ F)
    associator = record
      { U               = NI.associator (F.F) (G.F) (H.F)
      ; F⇒G-isMonoidal  = record
        { ε-compat      = begin
            E.id ∘ H.₁ (G.₁ F.ε) ∘ H.₁ G.ε ∘ H.ε  ≈⟨ identityˡ ⟩
            H.₁ (G.₁ F.ε) ∘ H.₁ G.ε ∘ H.ε         ≈˘⟨ pushˡ H.homomorphism ⟩
            H.₁ (G.₁ F.ε D.∘ G.ε) ∘ H.ε           ∎
        ; ⊗-homo-compat = λ {X Y} → begin
            E.id ∘ H.₁ (G.₁ (F.⊗-homo.η (X , Y))) ∘
            H.₁ (G.⊗-homo.η (F.F₀ X , F.F₀ Y)) ∘
            H.⊗-homo.η (G.F₀ (F.F₀ X) , G.F₀ (F.F₀ Y))
          ≈⟨ identityˡ ⟩
            H.₁ (G.₁ (F.⊗-homo.η (X , Y))) ∘
            H.₁ (G.⊗-homo.η (F.F₀ X , F.F₀ Y)) ∘
            H.⊗-homo.η (G.F₀ (F.F₀ X) , G.F₀ (F.F₀ Y))
          ≈˘⟨ pushˡ H.homomorphism ⟩
            H.₁ (G.₁ (F.⊗-homo.η (X , Y)) D.∘ G.⊗-homo.η (F.F₀ X , F.F₀ Y)) ∘
            H.⊗-homo.η (G.F₀ (F.F₀ X) , G.F₀ (F.F₀ Y))
          ≈˘⟨ identityʳ ⟩
            (H.₁ (G.₁ (F.⊗-homo.η (X , Y)) D.∘ G.⊗-homo.η (F.F₀ X , F.F₀ Y)) ∘
            H.⊗-homo.η (G.F₀ (F.F₀ X) , G.F₀ (F.F₀ Y))) ∘ E.id
          ≈˘⟨ refl⟩∘⟨ ⊗.identity ⟩
            (H.₁ (G.₁ (F.⊗-homo.η (X , Y)) D.∘ G.⊗-homo.η (F.F₀ X , F.F₀ Y)) ∘
             H.⊗-homo.η (G.F₀ (F.F₀ X) , G.F₀ (F.F₀ Y))) ∘
            E.id ⊗₁ E.id
          ∎
        }
      }

-- Monoidal natural isomorphisms between strong monoidal functors.

module Strong where
  open NT.Strong using (IsMonoidalNaturalTransformation)
  open StrongMonoidalFunctor renaming (F to UF; monoidalFunctor to laxF)

  module _ {o ℓ e o′ ℓ′ e′}
           {C : MonoidalCategory o ℓ e} {D : MonoidalCategory o′ ℓ′ e′}
           (F G : StrongMonoidalFunctor C D) where

    IsMonoidalNaturalIsomorphism : NaturalIsomorphism (UF F) (UF G) →
                                   Set (o ⊔ ℓ′ ⊔ e′)
    IsMonoidalNaturalIsomorphism α = IsMonoidalNaturalTransformation F G (F⇒G α)

    -- NOTE. This record contains the same data as the lax version,
    -- but the type arguments are different.  This helps type
    -- inference by providing the right constraints.

    record MonoidalNaturalIsomorphism : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
      field
        U              : NaturalIsomorphism (UF F) (UF G)
        F⇒G-isMonoidal : IsMonoidalNaturalIsomorphism U

      laxNI : Lax.MonoidalNaturalIsomorphism (laxF F) (laxF G)
      laxNI = record { U = U ; F⇒G-isMonoidal = F⇒G-isMonoidal }
      open Lax.MonoidalNaturalIsomorphism laxNI public
        hiding (U; F⇒G-isMonoidal)

    infix 4 _≃_

    _≃_ = MonoidalNaturalIsomorphism

  open MonoidalNaturalIsomorphism

  module _ {o ℓ e o′ ℓ′ e′}
           {C : MonoidalCategory o ℓ e} {D : MonoidalCategory o′ ℓ′ e′} where

    infixr 9 _ⓘᵥ_

    -- Since they contain the same data, we can strengthen a lax
    -- monoidal isomorphism to a strong one.

    strengthen : {F G : StrongMonoidalFunctor C D} →
                 (laxF F) Lax.≃ (laxF G) → F ≃ G
    strengthen α = record { U = L.U ; F⇒G-isMonoidal = L.F⇒G-isMonoidal }
      where module L = Lax.MonoidalNaturalIsomorphism α

    -- Identity and compositions

    id : {F : StrongMonoidalFunctor C D} → F ≃ F
    id = strengthen Lax.id

    _ⓘᵥ_ : {F G H : StrongMonoidalFunctor C D} → G ≃ H → F ≃ G → F ≃ H
    α ⓘᵥ β = strengthen (laxNI α Lax.ⓘᵥ laxNI β)

    isEquivalence : IsEquivalence _≃_
    isEquivalence = record
      { refl  = λ {F} → id {F}
      ; sym   = λ α → record
        { U              = NI.sym (U α)
        ; F⇒G-isMonoidal = F⇐G-isMonoidal α
        }
      ; trans = λ {F} {G} {H} α β → _ⓘᵥ_ {F} {G} {H} β α
      }

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″}
           {C : MonoidalCategory o ℓ e} {D : MonoidalCategory o′ ℓ′ e′}
           {E : MonoidalCategory o″ ℓ″ e″} where

    open Lax.MonoidalNaturalIsomorphism

    infixr 9 _ⓘₕ_ _ⓘˡ_ _ⓘʳ_

    _ⓘₕ_ : {F G : StrongMonoidalFunctor C D} {H I : StrongMonoidalFunctor D E} →
            H ≃ I → F ≃ G → (H ∘Fˢ F) ≃ (I ∘Fˢ G)
    -- FIXME: this definition is clearly equivalent to
    --
    --   α ⓘₕ β = strengthen (laxNI α Lax.ⓘₕ laxNI β)
    --
    -- but the latter takes an unreasonably long time to typecheck,
    -- while the unfolded version typechecks almost immediately.
    α ⓘₕ β = record
      { U               = L.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = L.ε-compat
        ; ⊗-homo-compat = L.⊗-homo-compat }
        }
      where
        module L = Lax.MonoidalNaturalIsomorphism (laxNI α Lax.ⓘₕ laxNI β)

    _ⓘˡ_ : {F G : StrongMonoidalFunctor C D}
           (H : StrongMonoidalFunctor D E) → F ≃ G → (H ∘Fˢ F) ≃ (H ∘Fˢ G)
    H ⓘˡ α = id {F = H} ⓘₕ α

    _ⓘʳ_ : {G H : StrongMonoidalFunctor D E} →
           G ≃ H → (F : StrongMonoidalFunctor C D) → (G ∘Fˢ F) ≃ (H ∘Fˢ F)
    α ⓘʳ F = α ⓘₕ id {F = F}

  -- Left and right unitors.

  module _ {o ℓ e o′ ℓ′ e′}
           {C : MonoidalCategory o ℓ e} {D : MonoidalCategory o′ ℓ′ e′}
           {F : StrongMonoidalFunctor C D} where

    unitorˡ : idFˢ D ∘Fˢ F ≃ F
    -- FIXME: Again, this unfolded definition typechecks considerably
    -- faster than the equivalent
    --
    --   strengthen (Lax.unitorʳ {F = laxF F})
    unitorˡ = record
      { U               = L.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = L.ε-compat
        ; ⊗-homo-compat = L.⊗-homo-compat
        }
      }
      where module L = Lax.MonoidalNaturalIsomorphism (Lax.unitorˡ {F = laxF F})

    unitorʳ : F ∘Fˢ idFˢ C ≃ F
    -- FIXME: ... same here ...
    unitorʳ = record
      { U               = L.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = L.ε-compat
        ; ⊗-homo-compat = L.⊗-homo-compat
        }
      }
      where module L = Lax.MonoidalNaturalIsomorphism (Lax.unitorʳ {F = laxF F})

  -- Associator.

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴}
           {B : MonoidalCategory o ℓ e} {C : MonoidalCategory o′ ℓ′ e′}
           {D : MonoidalCategory o″ ℓ″ e″} {E : MonoidalCategory o‴ ℓ‴ e‴}
           {F : StrongMonoidalFunctor B C} {G : StrongMonoidalFunctor C D}
           {H : StrongMonoidalFunctor D E} where

    associator : (H ∘Fˢ G) ∘Fˢ F ≃ H ∘Fˢ (G ∘Fˢ F)
    -- FIXME: ... and here.  Though, for this one, even the unfolded
    -- version takes a lot of time.
    associator = record
      { U               = L.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = L.ε-compat
        ; ⊗-homo-compat = L.⊗-homo-compat
        }
      }
      where
        α = Lax.associator {F = laxF F} {laxF G} {laxF H}
        module L = Lax.MonoidalNaturalIsomorphism α

max_stars_repo_name: iblech/agda-categories

max_issues_repo_name: andrejbauer/agda-categories

max_forks_repo_name: andrejbauer/agda-categories


text:
postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

{-# COMPILE GHC ♭ as flat #-}

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Some basic stuff for Conor's talk.
module SomeBasicStuff where

infixr 40 _::_ _↦_∣_
infix 30 _∈_ _==_
infixr 10 _,_

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

data Σ (A : Set)(B : A -> Set) : Set where
  _,_ : (x : A) -> B x -> Σ A B

_×_ : Set -> Set -> Set
A × B = Σ A \_ -> B

fst : {A : Set}{B : A -> Set} -> Σ A B -> A
fst (x , y) = x

snd : {A : Set}{B : A -> Set}(p : Σ A B) -> B (fst p)
snd (x , y) = y

data   False : Set where
record True  : Set where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data [_] (A : Set) : Set where
  []   : [ A ]
  _::_ : A -> [ A ] -> [ A ]

data _∈_ {A : Set} : A -> [ A ] -> Set where
  zero : forall {x xs} -> x ∈ x :: xs
  suc  : forall {x y xs} -> x ∈ xs -> x ∈ y :: xs

postulate Tag : Set
{-# BUILTIN STRING Tag #-}

Enumeration = [ Tag ]

data Enum (ts : Enumeration) : Set where
  enum : (t : Tag) -> t ∈ ts -> Enum ts

data Table (A : Set1) : Enumeration -> Set1 where
  []    : Table A []
  _↦_∣_ : forall {ts} -> (t : Tag) -> A -> Table A ts ->
          Table A (t :: ts)

lookup : forall {A ts} -> Table A ts -> Enum ts -> A
lookup []             (enum _ ())
lookup (.t ↦ v ∣ tbl) (enum t zero)    = v
lookup (_  ↦ v ∣ tbl) (enum t (suc p)) = lookup tbl (enum t p)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module sn-calculus-confluence.potpot where

open import utility
open import sn-calculus
open import context-properties
  using (->pot-view)

open import Esterel.Lang
open import Esterel.Lang.CanFunction
  using (Can ; Canₛ ; Canₛₕ ; Canθ ; Canθₛ ; Canθₛₕ)
open import Esterel.Lang.CanFunction.Properties
  using ( canθₛ-set-sig-monotonic-absence-lemma ; canθₛₕ-set-sig-monotonic-absence-lemma
        ; canθ-shr-var-irr
        )
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.Context
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import Esterel.Variable.Signal as Signal
  using (Signal)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)

open import Data.Bool
  using (Bool ; true ; false ; if_then_else_)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; [] ; _∷_ ; [_])
open import Data.List.Any
  using (Any ; here ; there ; any)
open import Data.Maybe
  using (Maybe ; just ; nothing)
open import Data.Nat
  using (ℕ ; _≟_ ; zero ; suc ; _+_)
open import Data.Nat.Properties.Simple
  using ( +-comm ; +-assoc)
open import Data.Product
  using (Σ ; Σ-syntax ; _,_ ; proj₁ ; proj₂ ; _,′_ ; _×_)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Function
  using (_∘_ ; id ; _∋_)
open import Relation.Nullary
  using (¬_ ; Dec ; yes ; no)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; sym ; trans ; cong ; subst ; module ≡-Reasoning)

open ->pot-view
open ≡-Reasoning
  using (begin_ ; _∎ ; _≡⟨_⟩_ ; _≡⟨⟩_)

open import Data.OrderedListMap Signal Signal.unwrap Signal.Status as SigM
open import Data.OrderedListMap SharedVar SharedVar.unwrap (Σ SharedVar.Status (λ _ → ℕ)) as ShrM
open import Data.OrderedListMap SeqVar SeqVar.unwrap ℕ as SeqM

pot-pot-conf-rec : ∀{p θ ql θl qr θr eql eqr A Al Ar Aql Arl}
                 → {ρθ·psn⟶₁ρθl·ql  :  (ρ⟨ θ , A ⟩· p) sn⟶₁ (ρ⟨ θl , Al ⟩· ql)}
                 → {ρθ·psn⟶₁ρθr·qr  :  (ρ⟨ θ , A ⟩· p) sn⟶₁ (ρ⟨ θr , Ar ⟩· qr)}
                 → ->pot-view  ρθ·psn⟶₁ρθl·ql  eql Aql
                 → ->pot-view  ρθ·psn⟶₁ρθr·qr  eqr Arl
                 → (ρ⟨ θl , Al ⟩· ql ≡ ρ⟨ θr , Ar ⟩· qr)
                   ⊎
                   Σ[ θo ∈ Env ]
                   (ρ⟨ θl , Al ⟩· ql) sn⟶₁ (ρ⟨ θo , A ⟩· p) ×
                   (ρ⟨ θr , Ar ⟩· qr) sn⟶₁ (ρ⟨ θo , A ⟩· p)

pot-pot-conf-rec {p} {θ} {.p} {θl} {.p} {θr} {_} {_} {A} {.A} {.A} {refl} {refl}
                 {.(rabsence {θ} {p} {S} S∈ θS≡unknown S∉can-p-θ)}
                 {.(rabsence {θ} {p} {S'} S'∈ θS'≡unknown S'∉can-p-θ)}
                 (vabsence S S∈ θS≡unknown S∉can-p-θ)
                 (vabsence S' S'∈ θS'≡unknown S'∉can-p-θ)
  with S Signal.≟ S'
... | yes refl = inj₁ refl
... | no S≢S' =
  inj₂
  (_ ,
   subst (λ sig* → ρ⟨ θl , A ⟩· p sn⟶₁ ρ⟨ (Θ sig* (Env.shr θl) (Env.var θl))  , A ⟩· p)
     (SigMap.put-comm {_} {Env.sig θ} {S} {S'} {Signal.absent} {Signal.absent} S≢S')
     (rabsence {θl} {p} {S'} S'∈Domθl θlS'≡unknown
       (λ S'∈can-p-θl →
         S'∉can-p-θ
           (canθₛ-set-sig-monotonic-absence-lemma (Env.sig θ) 0 p S Env.[]env
             S∈ θS≡unknown (Signal.unwrap S') S'∈can-p-θl))) ,′
   rabsence {θr} {p} {S} S∈Domθr θrS≡unknown
     (λ S∈can-p-θr →
       S∉can-p-θ
         (canθₛ-set-sig-monotonic-absence-lemma (Env.sig θ) 0 p S' Env.[]env
             S'∈ θS'≡unknown (Signal.unwrap S) S∈can-p-θr)))
  where
    S∈Domθr      = Env.sig-set-mono' {S}  {S'} {θ} {Signal.absent} {S'∈} S∈
    S'∈Domθl     = Env.sig-set-mono' {S'} {S}  {θ} {Signal.absent} {S∈}  S'∈
    θrS≡unknown  = SigMap.putputget {_} {Env.sig θ} {S}  {S'} {Signal.unknown} {Signal.absent}
                      S≢S'         S∈  S∈Domθr  θS≡unknown
    θlS'≡unknown = SigMap.putputget {_} {Env.sig θ} {S'} {S}  {Signal.unknown} {Signal.absent}
                     (S≢S' ∘ sym) S'∈ S'∈Domθl θS'≡unknown

pot-pot-conf-rec {p} {θ} {.p} {θl} {.p} {θr} {_} {_} {A} {.A} {.A} {refl} {refl}
                 {.(rabsence {θ} {p} {S} S∈ θS≡unknown S∉can-p-θ)}
                 {.(rreadyness {θ} {p} {s} s∈ θs≡old⊎θs≡new s∉can-p-θ)}
                 (vabsence S S∈ θS≡unknown S∉can-p-θ)
                 (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ) =
  inj₂
  (_ ,
   rreadyness {θl} {p} {s} s∈ θs≡old⊎θs≡new
     (λ s∈can-p-θl →
       s∉can-p-θ
         (canθₛₕ-set-sig-monotonic-absence-lemma (Env.sig θ) 0 p S Env.[]env
           S∈ θS≡unknown (SharedVar.unwrap s) s∈can-p-θl)) ,′
   rabsence {θr} {p} {S} S∈ θS≡unknown
     (λ S∈can-p-θr →
       S∉can-p-θ
         (subst (Signal.unwrap S ∈_)
           (cong proj₁ (canθ-shr-var-irr (Env.sig θ) 0 p Env.[]env Env.[]env refl))
           S∈can-p-θr)))

pot-pot-conf-rec {p} {θ} {.p} {θl} {.p} {θr} {_} {_} {A} {.A} {.A} {refl} {refl}
                 {.(rreadyness {θ} {p} {s} s∈ θs≡old⊎θs≡new s∉can-p-θ)}
                 {.(rabsence {θ} {p} {S} S∈ θS≡unknown S∉can-p-θ)}
                 (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
                 (vabsence S S∈ θS≡unknown S∉can-p-θ) =
  inj₂
  (_ ,
   rabsence {θl} {p} {S} S∈ θS≡unknown
     (λ S∈can-p-θl →
       S∉can-p-θ
         (subst (Signal.unwrap S ∈_)
           (cong proj₁ (canθ-shr-var-irr (Env.sig θ) 0 p Env.[]env Env.[]env refl))
           S∈can-p-θl)) ,′
   rreadyness {θr} {p} {s} s∈ θs≡old⊎θs≡new
     (λ s∈can-p-θr →
       s∉can-p-θ
         (canθₛₕ-set-sig-monotonic-absence-lemma (Env.sig θ) 0 p S Env.[]env
           S∈ θS≡unknown (SharedVar.unwrap s) s∈can-p-θr)))

pot-pot-conf-rec {p} {θ} {.p} {θl} {.p} {θr} {_} {_} {A} {.A} {.A} {refl} {refl}
                 {.(rreadyness {θ} {p} {s} s∈ θs≡old⊎θs≡new s∉can-p-θ)}
                 {.(rreadyness {θ} {p} {s'} s'∈ θs'≡old⊎θs'≡new s'∉can-p-θ)}
                 (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
                 (vreadyness s' s'∈ θs'≡old⊎θs'≡new s'∉can-p-θ)
  with s SharedVar.≟ s'
... | yes refl rewrite Env.shr-vals-∈-irr {s'} {θ} s∈ s'∈ = inj₁ refl
... | no s≢s' =
  inj₂
  (_ ,
   subst (λ shr* → ρ⟨ θl  , A ⟩· p sn⟶₁ ρ⟨ (Θ (Env.sig θl) shr* (Env.var θl))  , A ⟩· p)
     (cong Env.shr
       (begin
           Env.set-shr {s'} θl s'∈Domθl SharedVar.ready
             (Env.shr-vals {s'} θl s'∈Domθl)
        ≡⟨ cong (Env.set-shr {s'} θl s'∈Domθl SharedVar.ready ∘ proj₂) θls'≡θs' ⟩
           Env.set-shr {s'} θl s'∈Domθl SharedVar.ready θs'
        ≡⟨ cong (λ shr* → Θ (Env.sig θ) shr* (Env.var θ))
             (ShrMap.put-comm {_} {Env.shr θ} {s} {s'}
               {SharedVar.ready , θs} {SharedVar.ready , θs'} s≢s') ⟩
           Env.set-shr {s} θr s∈Domθr SharedVar.ready θs
        ≡⟨ cong (Env.set-shr {s} θr s∈Domθr SharedVar.ready ∘ proj₂) (sym θrs≡θs) ⟩
           Env.set-shr {s} θr s∈Domθr SharedVar.ready
             (Env.shr-vals {s} θr s∈Domθr)
        ∎))
     (rreadyness {θl} {p} {s'} s'∈Domθl
       (Data.Sum.map
         (trans (cong proj₁ θls'≡θs'))
         (trans (cong proj₁ θls'≡θs'))
         θs'≡old⊎θs'≡new)
       (λ s'∈can-p-θl →
         s'∉can-p-θ
           (subst (SharedVar.unwrap s' ∈_)
             (cong (proj₂ ∘ proj₂) (canθ-shr-var-irr (Env.sig θ) 0 p Env.[]env Env.[]env refl))
             s'∈can-p-θl))) ,′
   rreadyness {θr} {p} {s} s∈Domθr
     (Data.Sum.map
       (trans (cong proj₁ θrs≡θs))
       (trans (cong proj₁ θrs≡θs))
       θs≡old⊎θs≡new)
     (λ s∈can-p-θr →
       s∉can-p-θ
         (subst (SharedVar.unwrap s ∈_)
           (cong (proj₂ ∘ proj₂) (canθ-shr-var-irr (Env.sig θ) 0 p Env.[]env Env.[]env refl))
           s∈can-p-θr)))
  where
    θs       = Env.shr-vals {s} θ s∈
    θs'      = Env.shr-vals {s'} θ s'∈
    s∈Domθr  = Env.shr-set-mono' {s}  {s'} {θ} {SharedVar.ready} {θs'} {s'∈} s∈
    s'∈Domθl = Env.shr-set-mono' {s'} {s}  {θ} {SharedVar.ready} {θs}  {s∈}  s'∈
    θrs≡θs   = ShrMap.putputget {_} {Env.shr θ} {s}  {s'} {_} {SharedVar.ready ,′ θs'}
                      s≢s'         s∈  s∈Domθr  refl
    θls'≡θs' = ShrMap.putputget {_} {Env.shr θ} {s'}  {s} {_} {SharedVar.ready ,′ θs}
                     (s≢s' ∘ sym) s'∈ s'∈Domθl  refl

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
{-# OPTIONS --safe #-}
module Issue2487.d where

-- trying to import a two-level, non-safe module
open import Issue2487.e


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Support.EqReasoning where

open import Categories.Support.Equivalence using (Setoid; module Setoid)
open import Relation.Binary.PropositionalEquality using () renaming (_≡_ to _≣_; trans to ≣-trans; sym to ≣-sym; refl to ≣-refl)

module SetoidReasoning {s₁ s₂} (S : Setoid s₁ s₂) where
  open Setoid S

  infix  4 _IsRelatedTo_
  infix  1 begin_
  infixr 2 _≈⟨_⟩_ _↓⟨_⟩_ _↑⟨_⟩_ _↓≣⟨_⟩_ _↑≣⟨_⟩_ _↕_
  infix  3 _∎

  -- This seemingly unnecessary type is used to make it possible to
  -- infer arguments even if the underlying equality evaluates.

  data _IsRelatedTo_ (x y : Carrier) : Set s₂ where
    relTo : (x∼y : x ≈ y) → x IsRelatedTo y

  .begin_ : ∀ {x y} → x IsRelatedTo y → x ≈ y
  begin relTo x∼y = x∼y

  ._↓⟨_⟩_ : ∀ x {y z} → x ≈ y → y IsRelatedTo z → x IsRelatedTo z
  _ ↓⟨ x∼y ⟩ relTo y∼z = relTo (trans x∼y y∼z)
    -- where open IsEquivalence isEquivalence

  ._↑⟨_⟩_ : ∀ x {y z} → y ≈ x → y IsRelatedTo z → x IsRelatedTo z
  _ ↑⟨ y∼x ⟩ relTo y∼z = relTo (trans (sym y∼x) y∼z)
    -- where open IsEquivalence isEquivalence

  -- the syntax of the ancients, for compatibility
  ._≈⟨_⟩_ : ∀ x {y z} → x ≈ y → y IsRelatedTo z → x IsRelatedTo z
  _≈⟨_⟩_ = _↓⟨_⟩_

  ._↓≣⟨_⟩_ : ∀ x {y z} → x ≣ y → y IsRelatedTo z → x IsRelatedTo z
  _ ↓≣⟨ ≣-refl ⟩ y∼z = y∼z

  ._↑≣⟨_⟩_ : ∀ x {y z} → y ≣ x → y IsRelatedTo z → x IsRelatedTo z
  _ ↑≣⟨ ≣-refl ⟩ y∼z = y∼z

  ._↕_ : ∀ x {z} → x IsRelatedTo z → x IsRelatedTo z
  _ ↕ x∼z = x∼z

  ._∎ : ∀ x → x IsRelatedTo x
  _∎ _ = relTo refl
    -- where open IsEquivalence isEquivalence

module ≣-reasoning {ℓ} (S : Set ℓ) where
  infix  4 _IsRelatedTo_
  infix  2 _∎
  infixr 2 _≈⟨_⟩_
  infixr 2 _↓⟨_⟩_
  infixr 2 _↑⟨_⟩_
  infixr 2 _↕_
  infix  1 begin_

  -- This seemingly unnecessary type is used to make it possible to
  -- infer arguments even if the underlying equality evaluates.

  data _IsRelatedTo_ (x y : S) : Set ℓ where
    relTo : (x∼y : x ≣ y) → x IsRelatedTo y

  begin_ : ∀ {x y} → x IsRelatedTo y → x ≣ y
  begin relTo x∼y = x∼y

  -- the syntax of the ancients, for compatibility
  _≈⟨_⟩_ : ∀ x {y z} → x ≣ y → y IsRelatedTo z → x IsRelatedTo z
  _ ≈⟨ x∼y ⟩ relTo y∼z = relTo (≣-trans x∼y y∼z)

  _↓⟨_⟩_ : ∀ x {y z} → x ≣ y → y IsRelatedTo z → x IsRelatedTo z
  _ ↓⟨ x∼y ⟩ relTo y∼z = relTo (≣-trans x∼y y∼z)

  _↑⟨_⟩_ : ∀ x {y z} → y ≣ x → y IsRelatedTo z → x IsRelatedTo z
  _ ↑⟨ y∼x ⟩ relTo y∼z = relTo (≣-trans (≣-sym y∼x) y∼z)

  _↕_ : ∀ x {z} → x IsRelatedTo z → x IsRelatedTo z
  _ ↕ x∼z = x∼z

  _∎ : ∀ x → x IsRelatedTo x
  _∎ _ = relTo ≣-refl

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-

This file contains a summary of what remains for π₄(S³) ≡ ℤ/2ℤ to be proved.

See the module π₄S³ at the end of this file.

-}

{-# OPTIONS --safe #-}
module Cubical.Homotopy.Group.Pi4S3.Summary where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed

open import Cubical.Data.Nat.Base
open import Cubical.Data.Sigma.Base
open import Cubical.Data.Int renaming (ℤ to Int) hiding (_+_)

open import Cubical.HITs.Sn
open import Cubical.HITs.SetTruncation

open import Cubical.Homotopy.Group.Base hiding (π)
open import Cubical.Homotopy.HopfInvariant.Base
open import Cubical.Homotopy.HopfInvariant.Homomorphism
open import Cubical.Homotopy.HopfInvariant.HopfMap
open import Cubical.Homotopy.Whitehead
open import Cubical.Homotopy.Group.Pi3S2

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.Group.Instances.IntMod
open import Cubical.Algebra.Group.ZAction

private
  variable
    ℓ : Level

-- TODO: ideally this would not be off by one in the definition of π'Gr
π : ℕ → Pointed ℓ → Group ℓ
π n X = π'Gr (predℕ n) X

-- Nicer notation for the spheres (as pointed types)
𝕊² 𝕊³ : Pointed₀
𝕊² = S₊∙ 2
𝕊³ = S₊∙ 3

-- Whitehead product
[_]× : {X : Pointed ℓ} {n m : ℕ} → π' (suc n) X × π' (suc m) X → π' (suc (n + m)) X
[_]× (f , g) = [ f ∣ g ]π'

-- Some type abbreviations (unproved results)
π₄S³≡ℤ/something : GroupEquiv (π 3 𝕊²) ℤ → Type₁
π₄S³≡ℤ/something eq =
  π 4 𝕊³ ≡ ℤ/ abs (eq .fst .fst [ ∣ idfun∙ _ ∣₂ , ∣ idfun∙ _ ∣₂ ]×)

-- Summary of the last steps of the proof
module π₄S³
  (π₃S²≃ℤ           : GroupEquiv (π 3 𝕊²) ℤ)
  (gen-by-HopfMap   : gen₁-by (π 3 𝕊²) ∣ HopfMap ∣₂)
  (π₄S³≡ℤ/whitehead : π₄S³≡ℤ/something π₃S²≃ℤ)
  (hopfWhitehead    : abs (HopfInvariant-π' 0 ([ (∣ idfun∙ _ ∣₂ , ∣ idfun∙ _ ∣₂) ]×)) ≡ 2)
  where

  -- Package the Hopf invariant up into a group equivalence
  hopfInvariantEquiv : GroupEquiv (π 3 𝕊²) ℤ
  fst (fst hopfInvariantEquiv) = HopfInvariant-π' 0
  snd (fst hopfInvariantEquiv) =
    GroupEquivℤ-isEquiv (invGroupEquiv π₃S²≃ℤ) ∣ HopfMap ∣₂
                        gen-by-HopfMap (GroupHom-HopfInvariant-π' 0)
                        (abs→⊎ _ _ HopfInvariant-HopfMap)
  snd hopfInvariantEquiv = snd (GroupHom-HopfInvariant-π' 0)

  -- The two equivalences map [ (∣ idfun∙ _ ∣₂ , ∣ idfun∙ _ ∣₂) ]× to
  -- the same number, modulo the sign
  remAbs : abs (groupEquivFun π₃S²≃ℤ [ (∣ idfun∙ _ ∣₂ , ∣ idfun∙ _ ∣₂) ]×)
         ≡ abs (groupEquivFun hopfInvariantEquiv [ (∣ idfun∙ _ ∣₂ , ∣ idfun∙ _ ∣₂) ]×)
  remAbs = absGroupEquivℤGroup (invGroupEquiv π₃S²≃ℤ) (invGroupEquiv hopfInvariantEquiv) _

  -- So the image of [ (∣ idfun∙ _ ∣₂ , ∣ idfun∙ _ ∣₂) ]× under π₃S²≃ℤ
  -- is 2 (modulo the sign)
  remAbs₂ : abs (groupEquivFun π₃S²≃ℤ [ (∣ idfun∙ _ ∣₂ , ∣ idfun∙ _ ∣₂) ]×) ≡ 2
  remAbs₂ = remAbs ∙ hopfWhitehead

  -- The final result then follows
  π₄S³≡ℤ : π 4 𝕊³ ≡ ℤ/ 2
  π₄S³≡ℤ = π₄S³≡ℤ/whitehead ∙ cong (ℤ/_) remAbs₂

-- In order to instantiate the module, we need the four following lemmas:
-- Proved: 2/4

{- Lemma 1 -}
Lemma₁ : GroupEquiv ℤ (π'Gr 2 (S₊∙ 2))
Lemma₁ = invGroupEquiv π₃S²≅ℤ

{- Lemma 2 -}
Lemma₂ : gen₁-by (π 3 𝕊²) ∣ HopfMap ∣₂
Lemma₂ = π₂S³-gen-by-HopfMap

{- Lemma 3 (WIP) -}
{-
Lemma₃ : π₄S³≡ℤ/something (invGroupEquiv π₃S²≅ℤ)
Lemma₃ = ?
-}

{- Lemma 4 (WIP) -}
{-
Lemma₄ : abs (HopfInvariant-π' 0 ([ (∣ idfun∙ _ ∣₂ , ∣ idfun∙ _ ∣₂) ]×)) ≡ 2)
Lemma₄ = ?
-}

max_stars_repo_name: FernandoLarrain/cubical

max_issues_repo_name: FernandoLarrain/cubical

max_forks_repo_name: FernandoLarrain/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- More efficient mod and divMod operations (require the K axiom)
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Nat.DivMod.WithK where

open import Data.Nat using (ℕ; _+_; _*_; _≟_; zero; suc)
open import Data.Nat.DivMod hiding (_mod_; _divMod_)
open import Data.Nat.Properties using (≤⇒≤″)
open import Data.Nat.WithK
open import Data.Fin using (Fin; toℕ; fromℕ≤″)
open import Data.Fin.Properties using (toℕ-fromℕ≤″)
open import Function using (_$_)
open import Relation.Nullary.Decidable using (False)
open import Relation.Binary.PropositionalEquality
  using (refl; sym; cong; module ≡-Reasoning)
open import Relation.Binary.PropositionalEquality.WithK

open ≡-Reasoning

infixl 7 _mod_ _divMod_

------------------------------------------------------------------------
-- Certified modulus

_mod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → Fin divisor
(a mod 0) {}
(a mod suc n) = fromℕ≤″ (a % suc n) (≤″-erase (≤⇒≤″ (a%n<n a n)))

------------------------------------------------------------------------
-- Returns modulus and division result with correctness proof

_divMod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
           DivMod dividend divisor
(a divMod 0) {}
(a divMod suc n) = result (a div suc n) (a mod suc n) $ ≡-erase $ begin
  a                                 ≡⟨ a≡a%n+[a/n]*n a n ⟩
  a % suc n              + [a/n]*n  ≡⟨ cong (_+ [a/n]*n) (sym (toℕ-fromℕ≤″ lemma′)) ⟩
  toℕ (fromℕ≤″ _ lemma′) + [a/n]*n  ∎
  where
  lemma′ = ≤″-erase (≤⇒≤″ (a%n<n a n))
  [a/n]*n = a div suc n * suc n


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

mutual

  record R : Set₁ where
    constructor c
    field
      @0 A : Set
      x    : _

  _ : (@0 A : Set) → A → R
  _ = c


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

  -- This module provides a utility function to make it easy to
  -- provide the bft-lemma for implementations in which the
  -- participants can have different voting power.

  -- The module is parametrized with the number of participants -
  -- `authorsN`, and with a function - `votPower` - that assigns to
  -- each participant its voting power. The parameter `N` corresponds
  -- to the total voting power of all participants, as required by the
  -- parameter `totalVotPower` in the inner module. These
  -- implementations should assume a fixed unknown subset of malicious
  -- nodes - Byzantine - but should also assume a security threshold
  -- `bizF`, such that N > 3 * bizF, which should be provided in
  -- parameter `isBFT`.  Finally, the `bft-assumption` states that the
  -- combined voting power of Byzantine nodes must not exceed the
  -- security threshold `bizF`.

  -- The bft-lemma is the last lemma in this file and proves that in
  -- the intersection of any quorums, whose combined voting power is
  -- greater than or equal to `N - bizF`, there is an honest Member.

module LibraBFT.Abstract.BFT
  (authorsN      : ℕ)
  (votPower      : Fin authorsN → ℕ)
  (bizF          : ℕ)
  (isBFT         : f-sum votPower (allFin authorsN) ≥ suc (3 * bizF))
  (getPubKey     : Fin authorsN → PK)
 where

 -- The set of members of this epoch.
 Member : Set
 Member = Fin authorsN

 Meta-dishonest? :  ∀ (m : Member) → Dec (Meta-Dishonest-PK (getPubKey m))
 Meta-dishonest? m = Meta-DishonestPK? (getPubKey m)

 CombinedPower : List Member → ℕ
 CombinedPower = f-sum votPower

 TotalVotPower : ℕ
 TotalVotPower = f-sum votPower (allFin authorsN)

 open DecLemmas {A = Member} _≟Fin_

 -- The bft-assumption states that the combined voting power of
 -- Byzantine nodes must not exceed the security threshold
 -- `bizF`. Therefore, for any list of distinct participants, the
 -- combined power of the dishonest nodes is less than or equal to
 -- `bizF`.
 module _  (bft-assumption : ∀ (xs : List Member)
                           → allDistinct xs
                           → CombinedPower (List-filter Meta-dishonest? xs) ≤ bizF)
   where

   participants : List Member
   participants = allFin authorsN

   members⊆ : ∀ {xs : List Member} → xs ⊆List participants
   members⊆ {_} {x} _ = Any-tabulate⁺ {f = id} x refl

   union-votPower≤N : ∀ (xs ys : List Member)
                  → allDistinct xs → allDistinct ys
                  → CombinedPower (union xs ys) ≤ TotalVotPower
   union-votPower≤N xs ys dxs dys
     = sum-⊆-≤ (union xs ys) votPower (unionDistinct xs ys dxs dys) members⊆

   union-votPower≡ :  ∀ (xs ys : List Member)
                      → allDistinct xs → allDistinct ys
                      → CombinedPower (union xs ys) ≡ CombinedPower (xs ++ ys)
                                                    ∸ CombinedPower (intersect xs ys)
   union-votPower≡ xs [] dxs dys rewrite ++-identityʳ xs = refl
   union-votPower≡ xs (y ∷ ys) dxs dys
     with y ∈? xs
   ...| yes y∈xs rewrite union-votPower≡ xs ys dxs (allDistinctTail dys)
                       | sym (m+n∸n≡m (CombinedPower (xs ++ ys)) (votPower y))
                       | ∸-+-assoc (CombinedPower (xs ++ ys) + votPower y)
                                   (votPower y)
                                   (CombinedPower (intersect xs ys))
                       | map-++-commute votPower xs ys
                       | sum-++-commute (List-map votPower xs) (List-map votPower ys)
                       | +-assoc (CombinedPower xs)
                                 (CombinedPower ys)
                                 (votPower y)
                       | +-comm (CombinedPower ys) (votPower y)
                       | sym (sum-++-commute (List-map votPower xs) (List-map votPower (y ∷ ys)))
                       | sym (map-++-commute votPower xs (y ∷ ys)) = refl
   ...| no  y∉xs rewrite union-votPower≡ xs ys dxs (allDistinctTail dys)
                       | sym (+-∸-assoc (votPower y) (sumIntersect≤ xs ys votPower))
                       | map-++-commute votPower xs ys
                       | sum-++-commute (List-map votPower xs) (List-map votPower ys)
                       | sym (+-assoc (votPower y) (CombinedPower xs) (CombinedPower ys))
                       | +-comm (votPower y) (CombinedPower xs)
                       | +-assoc (CombinedPower xs) (votPower y) (CombinedPower ys)
                       | sym (sum-++-commute (List-map votPower xs) (List-map votPower (y ∷ ys)))
                       | sym (map-++-commute votPower xs (y ∷ ys)) = refl

   quorumInt>biz : ∀ (xs ys : List Member)
                 → TotalVotPower ∸ bizF ≤ CombinedPower xs
                 → TotalVotPower ∸ bizF ≤ CombinedPower ys
                 → CombinedPower (xs ++ ys) ∸ TotalVotPower ≤ CombinedPower (intersect xs ys)
                 → bizF + 1 ≤ CombinedPower (intersect xs ys)
   quorumInt>biz xs ys q≤x q≤y ≤combPower
     rewrite map-++-commute votPower xs ys
           | sum-++-commute (List-map votPower xs) (List-map votPower ys)
           = let powInt = CombinedPower (intersect xs ys)
                 p₁     = ≤-trans (∸-monoˡ-≤ TotalVotPower (+-mono-≤ q≤x q≤y)) ≤combPower
                 p₂     = subst (_≤ powInt) (simpExp₁ TotalVotPower bizF) p₁
                 p₃     = ≤-trans (∸-monoˡ-≤ (2 * bizF) isBFT) p₂
             in subst (_≤ powInt) (simpExp₂ bizF) p₃
       where  simpExp₁ : ∀ (x y : ℕ) → (x ∸ y) + (x ∸ y) ∸ x ≡ x ∸ (2 * y)
              simpExp₁ x y rewrite sym (*-identityʳ (x ∸ y))
                                 | sym (*-distribˡ-+ (x ∸ y) 1 1)
                                 | *-comm (x ∸ y) 2
                                 | *-distribˡ-∸ 2 x y
                                 | ∸-+-assoc (2 * x) (2 * y) x
                                 | +-comm (2 * y) x
                                 | sym (∸-+-assoc (2 * x) x (2 * y))
                                 | +-identityʳ x
                                 | m+n∸n≡m x x = refl

              simpExp₂ : ∀ (x : ℕ) → suc (3 * x) ∸ 2 * x ≡ x + 1
              simpExp₂ x rewrite +-∸-assoc 1 (*-monoˡ-≤ x {2} {3} (s≤s (s≤s z≤n)))
                               | sym (*-distribʳ-∸ x 3 2)
                               | sym (+-suc x 0) = refl

   partition-hon : ∀ {xs dis hon : List Member} {x : Member}
            → partition Meta-dishonest? xs ≡ (dis , x ∷ hon)
            → x ∈ xs × Meta-Honest-PK (getPubKey x)
   partition-hon {x ∷ xs} eq
     with Meta-dishonest? x | eq
   ...| no imp  | refl = here refl , imp
   ...| yes _   | eq₁
     with partition Meta-dishonest? xs | inspect (partition Meta-dishonest?) xs
   ...| _ , x₂ ∷ _ | [ eq₂ ] rewrite just-injective (cong (head ∘ proj₂) eq₁)
     = ×-map₁ there (partition-hon eq₂)

   partition-dis : ∀ {xs dis : List Member}
            → partition Meta-dishonest? xs ≡ (dis , [])
            → List-filter Meta-dishonest? xs ≡ xs
   partition-dis {[]} _ = refl
   partition-dis {x ∷ xs} eq
      with Meta-dishonest? x | eq
   ...| no ¬dis  | ()
   ...| yes _  | _
      with partition Meta-dishonest? xs | inspect (partition Meta-dishonest?) xs
   ...| _ , [] | [ eq₁ ] = cong (x ∷_) (partition-dis {xs} eq₁)

   -- TODO-1 : An alternative to prove this lemma would be:
   -- - First prove that
   --   CombinedPower (List-filter Meta-dishonest? xs) ≤ CombinedPower xs.
   -- - Then prove that:
   --   - If CombinedPower (List-filter Meta-dishonest? xs) < CombinedPower xs
   --     then ∃[ α ] (α ∈ xs × Meta-Honest-PK (getPubKey α)).
   --   - If CombinedPower (List-filter Meta-dishonest? xs ≡ CombinedPower xs we
   --   get a contradiction using the bft assumption (as we have now).
   find-honest : ∀ {xs : List Member}
               → allDistinct xs
               → bizF < CombinedPower xs
               → ∃[ α ] (α ∈ xs × Meta-Honest-PK (getPubKey α))
   find-honest {xs} sxs biz<
     with partition Meta-dishonest? xs | inspect (partition Meta-dishonest?) xs
   ...| dis , [] | [ eq ]
          = let bft     = bft-assumption xs sxs
                xsVot≤f = subst (_≤ bizF) (cong CombinedPower (partition-dis {xs} eq)) bft
            in ⊥-elim (<⇒≱ biz< xsVot≤f)
   ...| dis , x ∷ hon | [ eq ] = x , partition-hon eq

   bft-lemma : {xs ys : List Member}
             → allDistinct xs → allDistinct ys
             → TotalVotPower ∸ bizF ≤ CombinedPower xs
             → TotalVotPower ∸ bizF ≤ CombinedPower ys
             → ∃[ α ] (α ∈ xs × α ∈ ys × Meta-Honest-PK (getPubKey α))
   bft-lemma {xs} {ys} all≢xs all≢ys q≤≢xs q≤≢ys
     = let |q₁|+|q₂|   = CombinedPower (xs ++ ys)
           |q₁∩q₂|     = CombinedPower (intersect xs ys)
           |q₁∪q₂|≤n   = union-votPower≤N xs ys all≢xs all≢ys
           |q₁∪q₂|≡    = union-votPower≡ xs ys all≢xs all≢ys
           exp₁        = subst (_≤ TotalVotPower) |q₁∪q₂|≡ |q₁∪q₂|≤n
           exp₂        = m∸n≤o⇒m∸o≤n |q₁|+|q₂| |q₁∩q₂| TotalVotPower exp₁
           f+1≤|q₁∩q₂| = quorumInt>biz xs ys q≤≢xs q≤≢ys exp₂
           f<|q₁∩q₂|   = subst (_≤ |q₁∩q₂|) (+-comm bizF 1) f+1≤|q₁∩q₂|
           intDist     = intersectDistinct xs ys all≢xs all≢ys
           honInf      = find-honest {intersect xs ys} intDist f<|q₁∩q₂|
           h∈∩         = ∈-intersect xs ys ((proj₁ ∘ proj₂) honInf)
       in proj₁ honInf ,  proj₁ h∈∩ , proj₂ h∈∩ , (proj₂ ∘ proj₂) honInf

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
module Coirc.Bot where
open import Coirc
open import Coirc.Network
open import Coinduction
open import IO
open import Data.String

server = "irc.freenode.org"
name = "coalgbot"
real = "Coalgebra Bot"

bot : Bot
bot =
  put (nick name)
  (♯ put (user name real)
  (♯ loop)) where
  loop = get f where
    f : Event → Bot
    f notice = put (print "<notice>") (♯ loop)
    f numeric = put (print "<numeric-reply>") (♯ loop)
    f mode = put (print "<mode>") (♯ loop)
    f ping = put (print "<ping/pong>") (♯ put (pong name) (♯ loop))
    f (privmsg source "/quit") =
      put (privmsg source "ciao")
      (♯ put (quit (source ++ " told me to leave"))
      (♯ loop))
    f (privmsg source text) =
      put (print ("<privmsg>: " ++ text))
      (♯ put (privmsg source "interesting, tell me more!")
      (♯ loop))

main = run (runBot bot server)

max_stars_repo_name: larrytheliquid/coirc

max_issues_repo_name: larrytheliquid/coirc

max_forks_repo_name: larrytheliquid/coirc


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

open import Prelude
open import Relation.Binary

module LexPerm where

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

module Implicits.Resolution.Finite.Resolution where

open import Coinduction
open import Data.Fin.Substitution
open import Data.List
open import Data.List.Any
open Membership-≡
open import Implicits.Syntax
open import Implicits.Substitutions
open import Implicits.Resolution.Termination
open import Induction
open import Induction.Nat
open import Relation.Binary using (Rel)

mutual

  data _⊢_↓_ {ν} (Δ : ICtx ν) : Type ν → SimpleType ν → Set where
    i-simp : ∀ a → Δ ⊢ simpl a ↓ a
    i-iabs : ∀ {ρ₁ ρ₂ a} → (, ρ₁) hρ< (, ρ₂) → Δ ⊢ᵣ ρ₁ → Δ ⊢ ρ₂ ↓ a → Δ ⊢ ρ₁ ⇒ ρ₂ ↓ a
    i-tabs : ∀ {ρ a} b → Δ ⊢ ρ tp[/tp b ] ↓ a → Δ ⊢ ∀' ρ ↓ a

  data _⊢ᵣ_ {ν} (Δ : ICtx ν) : Type ν → Set where
    r-simp : ∀ {r τ} → r ∈ Δ → Δ ⊢ r ↓ τ → Δ  ⊢ᵣ simpl τ
    r-iabs : ∀ {ρ₁ ρ₂} → ((ρ₁ ∷ Δ) ⊢ᵣ ρ₂) → Δ ⊢ᵣ (ρ₁ ⇒ ρ₂)
    r-tabs : ∀ {ρ} → ictx-weaken Δ ⊢ᵣ ρ → Δ ⊢ᵣ ∀' ρ


text:
module Data.Fin.Sigma where

open import Prelude
open import Data.Nat
open import Data.Nat.Properties

Fin : ℕ → Type
Fin n = ∃ m × (m < n)

open import Data.List

_!!_ : (xs : List A) → Fin (length xs) → A
(x ∷ xs) !! (zero  , p) = x
(x ∷ xs) !! (suc n , p) = xs !! (n , p)


text:
module VariableName where

open import OscarPrelude

record VariableName : Set
 where
  constructor ⟨_⟩
  field
    name : Nat

open VariableName public

instance EqVariableName : Eq VariableName
Eq._==_ EqVariableName _ = decEq₁ (cong name) ∘ (_≟_ on name $ _)


text:
------------------------------------------------------------------------
-- A self-interpreter (without correctness proof)
------------------------------------------------------------------------

module Self-interpreter where

open import Prelude hiding (const)

-- To simplify the development, let's work with actual natural numbers
-- as variables and constants (see
-- Atom.one-can-restrict-attention-to-χ-ℕ-atoms).

open import Atom

open import Chi            χ-ℕ-atoms
open import Constants      χ-ℕ-atoms
open import Free-variables χ-ℕ-atoms

open χ-atoms χ-ℕ-atoms

open import Combinators

-- Substitution.

internal-subst : Exp
internal-subst = lambda v-x (lambda v-new body)
  module Internal-subst where
  private
    rec-or-lambda : _ → _
    rec-or-lambda = λ c →
      branch c (v-y ∷ v-e ∷ []) (
        case (equal-ℕ (var v-x) (var v-y)) (
          branch c-true [] (const c (var v-y ∷ var v-e ∷ [])) ∷
          branch c-false [] (
            const c (var v-y ∷ apply (var v-subst) (var v-e) ∷ [])) ∷
          []))

  branches =
    branch c-apply (v-e₁ ∷ v-e₂ ∷ []) (
      const c-apply (apply (var v-subst) (var v-e₁) ∷
                     apply (var v-subst) (var v-e₂) ∷ [])) ∷
    branch c-case (v-e ∷ v-bs ∷ []) (
      const c-case (
        apply (var v-subst) (var v-e) ∷
        apply (var v-subst) (var v-bs) ∷ [])) ∷
    rec-or-lambda c-rec ∷
    rec-or-lambda c-lambda ∷
    branch c-const (v-c ∷ v-es ∷ []) (
      const c-const (var v-c ∷ apply (var v-subst) (var v-es) ∷ [])) ∷
    branch c-var (v-y ∷ []) (
      case (equal-ℕ (var v-x) (var v-y)) (
        branch c-true [] (var v-new) ∷
        branch c-false [] (const c-var (var v-y ∷ [])) ∷ [])) ∷
    branch c-branch (v-c ∷ v-ys ∷ v-e ∷ []) (
      const c-branch (
        var v-c ∷
        var v-ys ∷
        case (member (var v-x) (var v-ys)) (
          branch c-true [] (var v-e) ∷
          branch c-false [] (apply (var v-subst) (var v-e)) ∷
          []) ∷ [])) ∷
    branch c-nil [] (const c-nil []) ∷
    branch c-cons (v-e ∷ v-es ∷ []) (
      const c-cons (apply (var v-subst) (var v-e) ∷
                    apply (var v-subst) (var v-es) ∷ [])) ∷
    []

  body = rec v-subst (lambda v-e (case (var v-e) branches))

-- Searches for a branch matching a given natural number.

internal-lookup : Exp
internal-lookup =
  lambda v-c (rec v-lookup (lambda v-bs (case (var v-bs) (
    branch c-cons (v-b ∷ v-bs ∷ []) (case (var v-b) (
      branch c-branch (v-c′ ∷ v-underscore ∷ v-underscore ∷ []) (
        case (equal-ℕ (var v-c) (var v-c′)) (
          branch c-false [] (apply (var v-lookup) (var v-bs)) ∷
          branch c-true [] (var v-b) ∷ [])) ∷ [])) ∷ []))))

-- Tries to apply multiple substitutions.

internal-substs : Exp
internal-substs =
  rec v-substs (lambda v-xs (lambda v-es (lambda v-e′ (
    case (var v-xs) (
      branch c-nil [] (case (var v-es) (
        branch c-nil [] (var v-e′) ∷ [])) ∷
      branch c-cons (v-x ∷ v-xs ∷ []) (case (var v-es) (
        branch c-cons (v-e ∷ v-es ∷ []) (
          apply (apply (apply internal-subst (var v-x)) (var v-e))
            (apply (apply (apply (var v-substs) (var v-xs))
               (var v-es)) (var v-e′))) ∷ [])) ∷ [])))))

-- A map function. The application of map to the function is done at
-- the meta-level in order to simplify proofs.

map : Exp → Exp
map f = rec v-map (lambda v-xs (case (var v-xs) branches))
  module Map where
  branches =
    branch c-nil [] (const c-nil []) ∷
    branch c-cons (v-x ∷ v-xs ∷ []) (
      const c-cons (apply f (var v-x) ∷
                    apply (var v-map) (var v-xs) ∷
                    [])) ∷
    []

-- The self-interpreter.

eval : Exp
eval =
  rec v-eval (lambda v-p (case (var v-p) branches))
  module Eval where
  apply-branch =
    branch c-lambda (v-x ∷ v-e ∷ []) (
      apply (var v-eval) (
        apply (apply (apply internal-subst (var v-x))
                 (apply (var v-eval) (var v-e₂)))
          (var v-e))) ∷
    []

  case-body₂ =
    case (apply (apply internal-lookup (var v-c)) (var v-bs)) (
      branch c-branch (v-underscore ∷ v-xs ∷ v-e ∷ []) (
        apply (var v-eval) (
          apply (apply (apply internal-substs (var v-xs))
            (var v-es)) (var v-e))) ∷
      [])

  case-body₁ =
    case (apply (var v-eval) (var v-e)) (
      branch c-const (v-c ∷ v-es ∷ []) case-body₂ ∷
      [])

  branches =
    branch c-apply (v-e₁ ∷ v-e₂ ∷ []) (
      case (apply (var v-eval) (var v-e₁)) apply-branch) ∷
    branch c-case (v-e ∷ v-bs ∷ []) case-body₁ ∷
    branch c-rec (v-x ∷ v-e ∷ []) (
      apply (var v-eval) (
        apply (apply (apply internal-subst (var v-x))
                 (const c-rec (var v-x ∷ var v-e ∷ [])))
          (var v-e))) ∷
    branch c-lambda (v-x ∷ v-e ∷ []) (
      const c-lambda (var v-x ∷ var v-e ∷ [])) ∷
    branch c-const (v-c ∷ v-es ∷ []) (
      const c-const (var v-c ∷
                     apply (map (var v-eval)) (var v-es) ∷
                     [])) ∷
    []

eval-closed : Closed eval
eval-closed = from-⊎ (closed? eval)

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Core where

open import Level
open import Function.Base using (flip)

open import Relation.Binary using (Rel; IsEquivalence; Setoid)
import Relation.Binary.Reasoning.Setoid as SetoidR

-- Basic definition of a |Category| with a Hom setoid.
-- Also comes with some reasoning combinators (see HomReasoning)
record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  eta-equality
  infix  4 _≈_ _⇒_
  infixr 9 _∘_

  field
    Obj : Set o
    _⇒_ : Rel Obj ℓ
    _≈_ : ∀ {A B} → Rel (A ⇒ B) e

    id  : ∀ {A} → (A ⇒ A)
    _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)

  field
    assoc     : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f)
    -- We add a symmetric proof of associativity so that the opposite category of the
    -- opposite category is definitionally equal to the original category. See how
    -- `op` is implemented.
    sym-assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → h ∘ (g ∘ f) ≈ (h ∘ g) ∘ f
    identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
    identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f
    -- We add a proof of "neutral" identity proof, in order to ensure the opposite of
    -- constant functor is definitionally equal to itself.
    identity² : ∀ {A} → id ∘ id {A} ≈ id {A}
    equiv     : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
    ∘-resp-≈  : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i

  module Equiv {A B : Obj} = IsEquivalence (equiv {A} {B})

  open Equiv

  ∘-resp-≈ˡ : ∀ {A B C} {f h : B ⇒ C} {g : A ⇒ B} → f ≈ h → f ∘ g ≈ h ∘ g
  ∘-resp-≈ˡ pf = ∘-resp-≈ pf refl

  ∘-resp-≈ʳ : ∀ {A B C} {f h : A ⇒ B} {g : B ⇒ C} → f ≈ h → g ∘ f ≈ g ∘ h
  ∘-resp-≈ʳ pf = ∘-resp-≈ refl pf

  hom-setoid : ∀ {A B} → Setoid _ _
  hom-setoid {A} {B} = record
    { Carrier       = A ⇒ B
    ; _≈_           = _≈_
    ; isEquivalence = equiv
    }

  -- When a category is quatified, it is convenient to refer to the levels from a module,
  -- so we do not have to explicitly quantify over a category when universe levels do not
  -- play a big part in a proof (which is the case probably all the time).
  o-level : Level
  o-level = o

  ℓ-level : Level
  ℓ-level = ℓ

  e-level : Level
  e-level = e

  -- Reasoning combinators.  _≈⟨_⟩_ and _≈˘⟨_⟩_ from SetoidR.
  -- Also some useful combinators for doing reasoning on _∘_ chains
  module HomReasoning {A B : Obj} where
    open SetoidR (hom-setoid {A} {B}) public
    -- open Equiv {A = A} {B = B} public

    infixr 4 _⟩∘⟨_ refl⟩∘⟨_
    infixl 5 _⟩∘⟨refl
    _⟩∘⟨_ : ∀ {M} {f h : M ⇒ B} {g i : A ⇒ M} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i
    _⟩∘⟨_ = ∘-resp-≈

    refl⟩∘⟨_ : ∀ {M} {f : M ⇒ B} {g i : A ⇒ M} → g ≈ i → f ∘ g ≈ f ∘ i
    refl⟩∘⟨_ = Equiv.refl ⟩∘⟨_

    _⟩∘⟨refl : ∀ {M} {f h : M ⇒ B} {g : A ⇒ M} → f ≈ h → f ∘ g ≈ h ∘ g
    _⟩∘⟨refl = _⟩∘⟨ Equiv.refl

    -- convenient inline versions
    infix 2 ⟺
    infixr 3 _○_
    ⟺ : {f g : A ⇒ B} → f ≈ g → g ≈ f
    ⟺ = Equiv.sym
    _○_ : {f g h : A ⇒ B} → f ≈ g → g ≈ h → f ≈ h
    _○_ = Equiv.trans

  op : Category o ℓ e
  op = record
    { Obj       = Obj
    ; _⇒_       = flip _⇒_
    ; _≈_       = _≈_
    ; _∘_       = flip _∘_
    ; id        = id
    ; assoc     = sym-assoc
    ; sym-assoc = assoc
    ; identityˡ = identityʳ
    ; identityʳ = identityˡ
    ; identity² = identity²
    ; equiv     = equiv
    ; ∘-resp-≈  = flip ∘-resp-≈
    }


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

module Categories.Adjoint.Equivalence where

open import Level

open import Categories.Adjoint
open import Categories.Adjoint.TwoSided
open import Categories.Adjoint.TwoSided.Compose
open import Categories.Category.Core using (Category)
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.NaturalTransformation.NaturalIsomorphism as ≃ using (_≃_)

open import Relation.Binary using (Setoid; IsEquivalence)

private
  variable
    o ℓ e o′ ℓ′ e′ : Level
    C D E    : Category o ℓ e

record ⊣Equivalence (C : Category o ℓ e) (D : Category o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    L    : Functor C D
    R    : Functor D C
    L⊣⊢R : L ⊣⊢ R

  module L    = Functor L
  module R    = Functor R

  open _⊣⊢_ L⊣⊢R public

refl : ⊣Equivalence C C
refl = record
  { L    = idF
  ; R    = idF
  ; L⊣⊢R = id⊣⊢id
  }

sym : ⊣Equivalence C D → ⊣Equivalence D C
sym e = record
  { L    = R
  ; R    = L
  ; L⊣⊢R = op₂
  }
  where open ⊣Equivalence e

trans : ⊣Equivalence C D → ⊣Equivalence D E → ⊣Equivalence C E
trans e e′ = record
  { L    = e′.L ∘F e.L
  ; R    = e.R ∘F e′.R
  ; L⊣⊢R = e.L⊣⊢R ∘⊣⊢ e′.L⊣⊢R
  }
  where module e  = ⊣Equivalence e using (L; R; L⊣⊢R)
        module e′ = ⊣Equivalence e′ using (L; R; L⊣⊢R)

isEquivalence : ∀ {o ℓ e} → IsEquivalence (⊣Equivalence {o} {ℓ} {e})
isEquivalence = record
  { refl  = refl
  ; sym   = sym
  ; trans = trans
  }

setoid : ∀ o ℓ e → Setoid _ _
setoid o ℓ e = record
  { Carrier       = Category o ℓ e
  ; _≈_           = ⊣Equivalence
  ; isEquivalence = isEquivalence
  }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --without-K #-}
module sets.properties where

open import sum
open import equality.core
open import equality.calculus
open import function.isomorphism
open import function.overloading
open import hott.level
open import hott.equivalence.core
open import hott.equivalence.alternative
open import sets.unit

mk-prop-iso : ∀ {i j}{A : Set i}{B : Set j}
            → h 1 A → h 1 B
            → (A → B) → (B → A)
            → A ≅ B
mk-prop-iso hA hB f g
  = iso f g (λ x → h1⇒prop hA _ _)
            (λ y → h1⇒prop hB _ _)

iso-coherence-h2 : ∀ {i j}(A : HSet i)(B : HSet j)
                 → (proj₁ A ≅' proj₁ B)
                 ≅ (proj₁ A ≅ proj₁ B)
iso-coherence-h2 (A , hA)(B , hB) = begin
    (A ≅' B)
  ≅⟨ ( Σ-ap-iso₂ λ isom
      → contr-⊤-iso (Π-level λ x → hB _ _ _ _) ) ⟩
    ((A ≅ B) × ⊤)
  ≅⟨ ×-right-unit ⟩
    (A ≅ B)
  ∎
  where open ≅-Reasoning

iso-equiv-h2 : ∀ {i j}{A : Set i}{B : Set j}
             → h 2 A → h 2 B
             → (A ≈ B) ≅ (A ≅ B)
iso-equiv-h2 hA hB = trans≅ ≈⇔≅'
  (iso-coherence-h2 (_ , hA) (_ , hB))

iso-eq-h2 : ∀ {i j}{A : Set i}{B : Set j}
          → h 2 A → h 2 B
          → {isom isom' : A ≅ B}
          → (apply isom ≡ apply isom')
          → isom ≡ isom'
iso-eq-h2 hA hB p =
  subtype-eq (λ f → weak-equiv-h1 f)
             (sym≅ (iso-equiv-h2 hA hB)) p

inj-eq-h2 : ∀ {i j}{A : Set i}{B : Set j}
          → h 2 A → {f f' : A ↣ B}
          → (apply f ≡ apply f')
          → f ≡ f'
inj-eq-h2 hA refl
  = ap (_,_ _) (h1⇒prop (inj-level _ hA) _ _)

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

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

module Setoids.Union.Lemmas {a b : _} {A : Set a} (S : Setoid {a} {b} A) {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} (s1 : subset S pred1) (s2 : subset S pred2) where

open import Setoids.Union.Definition S
open import Setoids.Equality S

unionCommutative : union s1 s2 =S union s2 s1
unionCommutative i = ans1 ,, ans2
  where
    ans1 : unionPredicate s1 s2 i → unionPredicate s2 s1 i
    ans1 (inl x) = inr x
    ans1 (inr x) = inl x
    ans2 : unionPredicate s2 s1 i → unionPredicate s1 s2 i
    ans2 (inl x) = inr x
    ans2 (inr x) = inl x

unionAssociative : {e : _} {pred3 : A → Set e} (s3 : subset S pred3) → union (union s1 s2) s3 =S union s1 (union s2 s3)
unionAssociative s3 x = ans1 ,, ans2
  where
    ans1 : unionPredicate (union s1 s2) s3 x → unionPredicate s1 (union s2 s3) x
    ans1 (inl (inl x)) = inl x
    ans1 (inl (inr x)) = inr (inl x)
    ans1 (inr x) = inr (inr x)
    ans2 : _
    ans2 (inl x) = inl (inl x)
    ans2 (inr (inl x)) = inl (inr x)
    ans2 (inr (inr x)) = inr x


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Susp.Base where

open import Cubical.Core.Glue

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

open import Cubical.Data.Bool

open import Cubical.HITs.S1
open import Cubical.HITs.S2
open import Cubical.HITs.S3

data Susp {ℓ} (A : Type ℓ) : Type ℓ where
  north : Susp A
  south : Susp A
  merid : (a : A) → north ≡ south

SuspBool : Type₀
SuspBool = Susp Bool

SuspBool→S¹ : SuspBool → S¹
SuspBool→S¹ north = base
SuspBool→S¹ south = base
SuspBool→S¹ (merid false i) = loop i
SuspBool→S¹ (merid true i)  = base

S¹→SuspBool : S¹ → SuspBool
S¹→SuspBool base     = north
S¹→SuspBool (loop i) = (merid false ∙ (sym (merid true))) i

SuspBool→S¹→SuspBool : (x : SuspBool) → Path _ (S¹→SuspBool (SuspBool→S¹ x)) x
SuspBool→S¹→SuspBool north = refl
SuspBool→S¹→SuspBool south = merid true
SuspBool→S¹→SuspBool (merid false i) = λ j → hcomp (λ k → (λ { (j = i1) → merid false i
                                                             ; (i = i0) → north
                                                             ; (i = i1) → merid true (j ∨ ~ k)}))
                                                   (merid false i)
SuspBool→S¹→SuspBool (merid true i)  = λ j → merid true (i ∧ j)

S¹→SuspBool→S¹ : (x : S¹) → SuspBool→S¹ (S¹→SuspBool x) ≡ x
S¹→SuspBool→S¹ base     = refl
S¹→SuspBool→S¹ (loop i) = λ j →
  hfill (λ k → λ { (i = i0) → base
                 ; (i = i1) → base })
        (inS (loop i)) (~ j)

S¹≃SuspBool : S¹ ≃ SuspBool
S¹≃SuspBool = isoToEquiv (iso S¹→SuspBool SuspBool→S¹ SuspBool→S¹→SuspBool S¹→SuspBool→S¹)

S¹≡SuspBool : S¹ ≡ SuspBool
S¹≡SuspBool = isoToPath (iso S¹→SuspBool SuspBool→S¹ SuspBool→S¹→SuspBool S¹→SuspBool→S¹)

-- Now the sphere

SuspS¹ : Type₀
SuspS¹ = Susp S¹

SuspS¹→S² : SuspS¹ → S²
SuspS¹→S² north = base
SuspS¹→S² south = base
SuspS¹→S² (merid base i) = base
SuspS¹→S² (merid (loop j) i) = surf i j

meridian-contraction : I → I → I → SuspS¹
meridian-contraction i j l = hfill (λ k → λ { (i = i0) → north
                                            ; (i = i1) → merid base (~ k)
                                            ; (j = i0) → merid base (~ k ∧ i)
                                            ; (j = i1) → merid base (~ k ∧ i) })
                                   (inS (merid (loop j) i)) l

S²→SuspS¹ : S² → SuspS¹
S²→SuspS¹ base = north
S²→SuspS¹ (surf i j) = meridian-contraction i j i1

S²→SuspS¹→S² : ∀ x → SuspS¹→S² (S²→SuspS¹ x) ≡ x
S²→SuspS¹→S² base k = base
S²→SuspS¹→S² (surf i j) k = SuspS¹→S² (meridian-contraction i j (~ k))

SuspS¹→S²→SuspS¹ : ∀ x → S²→SuspS¹ (SuspS¹→S² x) ≡ x
SuspS¹→S²→SuspS¹ north k = north
SuspS¹→S²→SuspS¹ south k = merid base k
SuspS¹→S²→SuspS¹ (merid base j) k = merid base (k ∧ j)
SuspS¹→S²→SuspS¹ (merid (loop j) i) k = meridian-contraction i j (~ k)

S²≡SuspS¹ : S² ≡ SuspS¹
S²≡SuspS¹ = isoToPath (iso S²→SuspS¹ SuspS¹→S² SuspS¹→S²→SuspS¹ S²→SuspS¹→S²)

-- And the 3-sphere

SuspS² : Type₀
SuspS² = Susp S²

SuspS²→S³ : SuspS² → S³
SuspS²→S³ north = base
SuspS²→S³ south = base
SuspS²→S³ (merid base i) = base
SuspS²→S³ (merid (surf j k) i) = surf i j k

meridian-contraction-2 : I → I → I → I → SuspS²
meridian-contraction-2 i j k l = hfill (λ m → λ { (i = i0) → north
                                                ; (i = i1) → merid base (~ m)
                                                ; (j = i0) → merid base (~ m ∧ i)
                                                ; (j = i1) → merid base (~ m ∧ i)
                                                ; (k = i0) → merid base (~ m ∧ i)
                                                ; (k = i1) → merid base (~ m ∧ i) })
                                       (inS (merid (surf j k) i)) l

S³→SuspS² : S³ → SuspS²
S³→SuspS² base = north
S³→SuspS² (surf i j k) = meridian-contraction-2 i j k i1

S³→SuspS²→S³ : ∀ x → SuspS²→S³ (S³→SuspS² x) ≡ x
S³→SuspS²→S³ base l = base
S³→SuspS²→S³ (surf i j k) l = SuspS²→S³ (meridian-contraction-2 i j k (~ l))

SuspS²→S³→SuspS² : ∀ x → S³→SuspS² (SuspS²→S³ x) ≡ x
SuspS²→S³→SuspS² north l = north
SuspS²→S³→SuspS² south l = merid base l
SuspS²→S³→SuspS² (merid base j) l = merid base (l ∧ j)
SuspS²→S³→SuspS² (merid (surf j k) i) l = meridian-contraction-2 i j k (~ l)

S³≡SuspS² : S³ ≡ SuspS²
S³≡SuspS² = isoToPath (iso S³→SuspS² SuspS²→S³ SuspS²→S³→SuspS² S³→SuspS²→S³)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
-- # A Reflexive Graph Model of Sized Types

-- This is the formalisation of my M.Sc. thesis, available at

--   https://limperg.de/paper/msc-thesis/

-- I define λST, a simply typed lambda calculus extended with sized types. I
-- then give a reflexive graph model of λST which incorporates a notion of size
-- irrelevance. This document lists all modules belonging to the development,
-- roughly in dependency order.

module index where

-- ## Object Language

-- The following modules define the syntax and type system of λST.

-- Sizes, size contexts, size comparison.
import Source.Size

-- First formulation of size substitutions.
import Source.Size.Substitution.Canonical

-- Second formulation of size substitutions.
import Source.Size.Substitution.Universe

-- An abstraction for things which size substitutions can be applied to.
import Source.Size.Substitution.Theory

-- Types.
import Source.Type

-- Terms.
import Source.Term

-- ## Model

-- The following modules define the reflexive graph model of λST.

-- Propositional reflexive graphs and their morphisms.
import Model.RGraph

-- Model of sizes, size contexts, size comparison.
import Model.Size

-- Families of propositional reflexive graphs (PRGraph families) and their
-- morphisms.
import Model.Type.Core

-- The terminal PRGraph family.
import Model.Terminal

-- Binary products of PRGraph families.
import Model.Product

-- Exponentials of PRGraph families (model of the function space).
import Model.Exponential

-- Model of size quantification.
import Model.Quantification

-- Model of the natural number type.
import Model.Nat

-- Model of the stream type.
import Model.Stream

-- Model of types and type contexts.
import Model.Type

-- Model of terms.
import Model.Term

-- ## Utility Library

-- The following modules contain utility code. The majority of this is an
-- implementation of (parts of) Homotopy Type Theory.

import Util.Data.Product
import Util.HoTT.Equiv
import Util.HoTT.Equiv.Core
import Util.HoTT.Equiv.Induction
import Util.HoTT.FunctionalExtensionality
import Util.HoTT.HLevel
import Util.HoTT.HLevel.Core
import Util.HoTT.Homotopy
import Util.HoTT.Section
import Util.HoTT.Singleton
import Util.HoTT.Univalence
import Util.HoTT.Univalence.Axiom
import Util.HoTT.Univalence.Beta
import Util.HoTT.Univalence.ContrFormulation
import Util.HoTT.Univalence.Statement
import Util.Induction.WellFounded
import Util.Prelude
import Util.Relation.Binary.Closure.SymmetricTransitive
import Util.Relation.Binary.LogicalEquivalence
import Util.Relation.Binary.PropositionalEquality
import Util.Vec

-- ## Miscellaneous

-- Some terms of λST and their typing derivations.
import Source.Examples

-- Experiments with a hypothetical Agda without the ∞ < ∞ rule.
import irreflexive-lt

-- Ordinals as defined in the HoTT book.
import Ordinal.HoTT

-- Plump ordinals as presented by Shulman.
import Ordinal.Shulman

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module New.Correctness where

open import Function hiding (const)
open import New.Lang
open import New.Changes
open import New.Derive
open import New.LangChanges
open import New.LangOps
open import New.FunctionLemmas
open import New.Unused

⟦Γ≼ΔΓ⟧ : ∀ {Γ} (ρ : ⟦ Γ ⟧Context) (dρ : ChΓ Γ) → validΓ ρ dρ →
  ρ ≡ ⟦ Γ≼ΔΓ ⟧≼ dρ
⟦Γ≼ΔΓ⟧ ∅ ∅ tt = refl
⟦Γ≼ΔΓ⟧ (v • ρ) (dv • .v • dρ) (vdv , refl , ρdρ) = cong₂ _•_ refl (⟦Γ≼ΔΓ⟧ ρ dρ ρdρ)

fit-sound : ∀ {Γ τ} → (t : Term Γ τ) →
  (ρ : ⟦ Γ ⟧Context) (dρ : ChΓ Γ) → validΓ ρ dρ →
  ⟦ t ⟧Term ρ ≡ ⟦ fit t ⟧Term dρ
fit-sound t ρ dρ ρdρ = trans
  (cong ⟦ t ⟧Term (⟦Γ≼ΔΓ⟧ ρ dρ ρdρ))
  (sym (weaken-sound t _))

correctDeriveConst : ∀ {τ} (c : Const τ) → ⟦ c ⟧Const ≡ ⟦ c ⟧Const ⊕ (⟦_⟧ΔConst c)
correctDeriveConst (lit n) = sym (right-id-int n)
correctDeriveConst plus = ext (λ m → ext (lemma m))
  where
    lemma : ∀ m n → m + n ≡ m + n + (m + - m + (n + - n))
    lemma m n rewrite right-inv-int m | right-inv-int n | right-id-int (m + n) = refl

correctDeriveConst minus = ext (λ m → ext (λ n → lemma m n))
  where
    lemma : ∀ m n → m - n ≡ m - n + (m + - m - (n + - n))
    lemma m n rewrite right-inv-int m | right-inv-int n | right-id-int (m - n) = refl
correctDeriveConst cons = ext (λ v1 → ext (λ v2 → sym (update-nil (v1 , v2))))
correctDeriveConst fst = ext (λ vp → sym (update-nil (proj₁ vp)))
correctDeriveConst snd = ext (λ vp → sym (update-nil (proj₂ vp)))
correctDeriveConst linj = ext (λ va → sym (cong inj₁ (update-nil va)))
correctDeriveConst rinj = ext (λ vb → sym (cong inj₂ (update-nil vb)))
correctDeriveConst (match {t1} {t2} {t3}) = ext³ lemma
  where
    lemma : ∀ s f g →
      ⟦ match {t1} {t2} {t3} ⟧Const s f g ≡
      (⟦ match ⟧Const ⊕ ⟦ match ⟧ΔConst) s f g
    lemma (inj₁ x) f g rewrite update-nil x | update-nil (f x) = refl
    lemma (inj₂ y) f g rewrite update-nil y | update-nil (g y) = refl

validDeriveConst : ∀ {τ} (c : Const τ) → valid ⟦ c ⟧Const (⟦_⟧ΔConst c)
validDeriveConst (lit n) = tt
validDeriveConst {τ = t1 ⇒ t2 ⇒ pair .t1 .t2} cons = binary-valid (λ a da ada b db bdb → (ada , bdb)) dcons-eq
  where
    open BinaryValid ⟦ cons {t1} {t2} ⟧Const (⟦ cons ⟧ΔConst)
    dcons-eq : binary-valid-eq-hp
    dcons-eq a da ada b db bdb rewrite update-nil (a ⊕ da) | update-nil (b ⊕ db) = refl
validDeriveConst fst (a , b) (da , db) (ada , bdb) = ada , update-nil (a ⊕ da)
validDeriveConst snd (a , b) (da , db) (ada , bdb) = bdb , update-nil (b ⊕ db)

validDeriveConst plus = binary-valid (λ a da ada b db bdb → tt) dplus-eq
  where
    open BinaryValid ⟦ plus ⟧Const (⟦ plus ⟧ΔConst)
    dplus-eq : binary-valid-eq-hp
    dplus-eq a da ada b db bdb rewrite right-inv-int (a + da) | right-inv-int (b + db) | right-id-int (a + da + (b + db)) = mn·pq=mp·nq {a} {da} {b} {db}
validDeriveConst minus = binary-valid (λ a da ada b db bdb → tt) dminus-eq
  where
    open BinaryValid ⟦ minus ⟧Const (⟦ minus ⟧ΔConst)
    dminus-eq : binary-valid-eq-hp
    dminus-eq a da ada b db bdb rewrite right-inv-int (a + da) | right-inv-int (b + db) | right-id-int (a + da - (b + db)) | sym (-m·-n=-mn {b} {db}) = mn·pq=mp·nq {a} {da} { - b} { - db}
validDeriveConst linj a da ada = sv₁ a da ada , cong inj₁ (update-nil (a ⊕ da))
validDeriveConst rinj b db bdb = sv₂ b db bdb , cong inj₂ (update-nil (b ⊕ db))
validDeriveConst (match {t1} {t2} {t3}) =
  ternary-valid dmatch-valid dmatch-eq
  where
    open TernaryValid {{chAlgt (sum t1 t2)}} {{chAlgt (t1 ⇒ t3)}} {{chAlgt (t2 ⇒ t3)}} {{chAlgt t3}} ⟦ match ⟧Const (⟦ match ⟧ΔConst)

    dmatch-valid : ternary-valid-preserve-hp
    dmatch-valid .(inj₁ a) .(inj₁ (inj₁ da)) (sv₁ a da ada) f df fdf g dg gdg = proj₁ (fdf a da ada)
    dmatch-valid .(inj₂ b) .(inj₁ (inj₂ db)) (sv₂ b db bdb) f df fdf g dg gdg = proj₁ (gdg b db bdb)
    dmatch-valid .(inj₁ a1) .(inj₂ (inj₂ b2)) (svrp₁ a1 b2) f df fdf g dg gdg
      rewrite changeMatchSem-lem1 f df g dg a1 b2
      = ⊝-valid (f a1) (g b2 ⊕ dg b2 (nil b2))
    dmatch-valid .(inj₂ b1) .(inj₂ (inj₁ a2)) (svrp₂ b1 a2) f df fdf g dg gdg
      rewrite changeMatchSem-lem2 f df g dg b1 a2
      = ⊝-valid (g b1) (f a2 ⊕ df a2 (nil a2))
    dmatch-eq : ternary-valid-eq-hp
    dmatch-eq .(inj₁ a) .(inj₁ (inj₁ da)) (sv₁ a da ada) f df fdf g dg gdg
      rewrite update-nil (a ⊕ da)
      | update-nil (f (a ⊕ da) ⊕ df (a ⊕ da) (nil (a ⊕ da))) = proj₂ (fdf a da ada)
    dmatch-eq .(inj₂ b) .(inj₁ (inj₂ db)) (sv₂ b db bdb) f df fdf g dg gdg
      rewrite update-nil (b ⊕ db)
      | update-nil (g (b ⊕ db) ⊕ dg (b ⊕ db) (nil (b ⊕ db))) = proj₂ (gdg b db bdb)
    dmatch-eq .(inj₁ a1) .(inj₂ (inj₂ b2)) (svrp₁ a1 b2) f df fdf g dg gdg
      rewrite changeMatchSem-lem1 f df g dg a1 b2
      | update-nil b2
      | update-diff (g b2 ⊕ dg b2 (nil b2)) (f a1)
      | update-nil (g b2 ⊕ dg b2 (nil b2))
      = refl
    dmatch-eq .(inj₂ b1) .(inj₂ (inj₁ a2)) (svrp₂ b1 a2) f df fdf g dg gdg
      rewrite changeMatchSem-lem2 f df g dg b1 a2
      | update-nil a2
      | update-diff (f a2 ⊕ df a2 (nil a2)) (g b1)
      | update-nil (f a2 ⊕ df a2 (nil a2))
      = refl

validDeriveVar : ∀ {Γ τ} → (x : Var Γ τ) →
  (ρ : ⟦ Γ ⟧Context) (dρ : ChΓ Γ) →
  validΓ ρ dρ → valid (⟦ x ⟧Var ρ) (⟦ x ⟧ΔVar ρ dρ)

validDeriveVar this (v • ρ) (dv • .v • dρ) (vdv , refl , ρdρ) = vdv
validDeriveVar (that x) (v • ρ) (dv • .v • dρ) (vdv , refl , ρdρ) = validDeriveVar x ρ dρ ρdρ

correctDeriveVar : ∀ {Γ τ} → (x : Var Γ τ) →
  IsDerivative ⟦ x ⟧Var (⟦ x ⟧ΔVar)
correctDeriveVar this (v • ρ) (dv • v' • dρ) ρdρ = refl
correctDeriveVar (that x) (v • ρ) (dv • .v • dρ) (vdv , refl , ρdρ) = correctDeriveVar x ρ dρ ρdρ

validDerive : ∀ {Γ τ} → (t : Term Γ τ) →
  (ρ : ⟦ Γ ⟧Context) (dρ : ChΓ Γ) → validΓ ρ dρ →
    valid (⟦ t ⟧Term ρ) (⟦ t ⟧ΔTerm ρ dρ)
correctDerive : ∀ {Γ τ} → (t : Term Γ τ) →
  IsDerivative ⟦ t ⟧Term ⟦ t ⟧ΔTerm

correctDerive (const c) ρ dρ ρdρ rewrite ⟦ c ⟧ΔConst-rewrite ρ dρ = correctDeriveConst c
correctDerive (var x) ρ dρ ρdρ = correctDeriveVar x ρ dρ ρdρ
correctDerive (app s t) ρ dρ ρdρ rewrite sym (fit-sound t ρ dρ ρdρ) =
  let
    open ≡-Reasoning
    a0 = ⟦ t ⟧Term ρ
    da0 = ⟦ derive t ⟧Term dρ
    a0da0 = validDerive t ρ dρ ρdρ
  in
    begin
      ⟦ s ⟧Term (ρ ⊕ dρ) (⟦ t ⟧Term (ρ ⊕ dρ))
    ≡⟨ correctDerive s ρ dρ ρdρ ⟨$⟩ correctDerive t ρ dρ ρdρ ⟩
      (⟦ s ⟧Term ρ ⊕ ⟦ s ⟧ΔTerm ρ dρ) (⟦ t ⟧Term ρ ⊕ ⟦ t ⟧ΔTerm ρ dρ)
    ≡⟨ proj₂ (validDerive s ρ dρ ρdρ a0 da0 a0da0)  ⟩
      ⟦ s ⟧Term ρ (⟦ t ⟧Term ρ) ⊕ (⟦ s ⟧ΔTerm ρ dρ) (⟦ t ⟧Term ρ) (⟦ t ⟧ΔTerm ρ dρ)
    ∎
  where
    open import Theorem.CongApp
correctDerive (abs t) ρ dρ ρdρ = ext $ λ a →
  let
    open ≡-Reasoning
    ρ1 = a • ρ
    dρ1 = nil a • a • dρ
    ρ1dρ1 = nil-valid a , refl , ρdρ
  in
    -- equal-future-expand-derivative ⟦ t ⟧Term ⟦ t ⟧ΔTerm (correctDerive t)
    --   ρ1 dρ1 ρ1dρ1
    --   (a • (ρ ⊕ dρ))
    --   (cong (_• ρ ⊕ dρ) (sym (update-nil a)))
    begin
      ⟦ t ⟧Term (a • ρ ⊕ dρ)
    ≡⟨ cong (λ a′ → ⟦ t ⟧Term (a′ • ρ ⊕ dρ)) (sym (update-nil a)) ⟩
      ⟦ t ⟧Term (ρ1 ⊕ dρ1)
    ≡⟨ correctDerive t ρ1 dρ1 ρ1dρ1 ⟩
      ⟦ t ⟧Term ρ1 ⊕ ⟦ t ⟧ΔTerm ρ1 dρ1
    ∎

validDerive (app s t) ρ dρ ρdρ =
  let
    f = ⟦ s ⟧Term ρ
    df = ⟦ derive s ⟧Term dρ
    v = ⟦ t ⟧Term ρ
    dv = ⟦ derive t ⟧Term dρ
    vdv = validDerive t ρ dρ ρdρ
    fdf = validDerive s ρ dρ ρdρ
    fvdfv = proj₁ (fdf v dv vdv)
  in subst (λ v′ → valid (f v) (df v′ dv)) (fit-sound t ρ dρ ρdρ) fvdfv
validDerive (abs t) ρ dρ ρdρ =
  λ a da ada →
  let
    ρ1 = a ⊕ da • ρ
    dρ1 = nil (a ⊕ da) • (a ⊕ da) • dρ
    ρ2 = a • ρ
    dρ2 = da • a • dρ
    ρ1dρ1 = nil-valid (a ⊕ da) , refl , ρdρ
    ρ2dρ2 = ada , refl , ρdρ
    rdr = validDerive t ρ2 dρ2 ρ2dρ2
    open ≡-Reasoning
   in
     rdr ,
     equal-future-derivative ⟦ t ⟧Term ⟦ t ⟧ΔTerm (correctDerive t)
       ρ1 dρ1 ρ1dρ1
       ρ2 dρ2 ρ2dρ2
       (cong (λ a′ → (a′ • ρ ⊕ dρ)) (update-nil (a ⊕ da)))
validDerive (var x) ρ dρ ρdρ = validDeriveVar x ρ dρ ρdρ
validDerive (const c) ρ dρ ρdρ rewrite ⟦ c ⟧ΔConst-rewrite ρ dρ = validDeriveConst c

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:
module _ where

module M (X : Set₁) where

  record Raw : Set₁ where
    field return : Set
    postulate fmap : Set

  module Fails = Raw ⦃ … ⦄
  module Works ⦃ r : Raw ⦄ = Raw r

open M

postulate r : Raw Set

fail : Set
fail = Fails.fmap Set ⦃ r ⦄
-- C-c C-n fail
-- M.Raw.fmap Set r

good : Set
good = Works.fmap Set ⦃ r ⦄
-- C-c C-n good
-- M.Raw.fmap r

-- Checking using reflection saves us an interaction test.

open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Unit

macro
  `_ : Name → Term → TC ⊤
  (` x) hole = do
    v  ← normalise (def x [])
    `v ← quoteTC v
    unify hole `v

pattern vArg x = arg (arg-info visible relevant) x
pattern hArg x = arg (arg-info hidden  relevant) x
pattern `fmap x y = def (quote M.Raw.fmap) (x ∷ y ∷ [])
`Set = agda-sort (lit 0)
`r   = def (quote r) []

check-good : ` good ≡ `fmap (hArg `Set) (vArg `r)
check-good = refl

check-bad : ` fail ≡ ` good
check-bad = refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use Data.List.Relation.Unary.All
-- directly.
------------------------------------------------------------------------

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

module Data.List.All where

open import Data.List.Relation.Unary.All public


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Limits.Initial where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_)
open import Cubical.HITs.PropositionalTruncation.Base

open import Cubical.Data.Sigma

open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.Adjoint

private
  variable
    ℓ ℓ' : Level
    ℓC ℓC' ℓD ℓD' : Level

module _ (C : Category ℓ ℓ') where
  open Category C

  isInitial : (x : ob) → Type (ℓ-max ℓ ℓ')
  isInitial x = ∀ (y : ob) → isContr (C [ x , y ])

  Initial : Type (ℓ-max ℓ ℓ')
  Initial = Σ[ x ∈ ob ] isInitial x

  initialOb : Initial → ob
  initialOb = fst

  initialArrow : (T : Initial) (y : ob) → C [ initialOb T , y ]
  initialArrow T y = T .snd y .fst

  initialArrowUnique : {T : Initial} {y : ob} (f : C [ initialOb T , y ])
                      → initialArrow T y ≡ f
  initialArrowUnique {T} {y} f = T .snd y .snd f

  initialEndoIsId : (T : Initial) (f : C [ initialOb T , initialOb T ])
                   → f ≡ id
  initialEndoIsId T f = isContr→isProp (T .snd (initialOb T)) f id

  hasInitial : Type (ℓ-max ℓ ℓ')
  hasInitial = ∥ Initial ∥₁

  -- Initiality of an object is a proposition.
  isPropIsInitial : (x : ob) → isProp (isInitial x)
  isPropIsInitial _ = isPropΠ λ _ → isPropIsContr

  open CatIso

  -- Objects that are initial are isomorphic.
  initialToIso : (x y : Initial) → CatIso C (initialOb x) (initialOb y)
  mor (initialToIso x y) = initialArrow x (initialOb y)
  inv (initialToIso x y) = initialArrow y (initialOb x)
  sec (initialToIso x y) = initialEndoIsId y _
  ret (initialToIso x y) = initialEndoIsId x _

  open isUnivalent

  -- The type of initial objects of a univalent category is a proposition,
  -- i.e. all initial objects are equal.
  isPropInitial : (hC : isUnivalent C) → isProp Initial
  isPropInitial hC x y =
    Σ≡Prop isPropIsInitial (CatIsoToPath hC (initialToIso x y))

module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) where
  open Category
  open Functor
  open NaturalBijection
  open _⊣_
  open _≅_

  preservesInitial : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
  preservesInitial = ∀ (x : ob C) → isInitial C x → isInitial D (F-ob F x)

  isLeftAdjoint→preservesInitial : isLeftAdjoint F → preservesInitial
  fst (isLeftAdjoint→preservesInitial (G , F⊣G) x initX y) = _♯ F⊣G (fst (initX (F-ob G y)))
  snd (isLeftAdjoint→preservesInitial (G , F⊣G) x initX y) ψ =
    _♯ F⊣G (fst (initX (F-ob G y)))
      ≡⟨ cong (F⊣G ♯) (snd (initX (F-ob G y)) (_♭ F⊣G ψ)) ⟩
    _♯ F⊣G (_♭ F⊣G ψ)
      ≡⟨ leftInv (adjIso F⊣G) ψ ⟩
    ψ ∎

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import lib.Basics hiding (_⊔_)
open import lib.types.Sigma
open import lib.types.Bool
open import lib.types.Empty

open import Preliminaries
open import Truncation_Level_Criteria
open import Anonymous_Existence_CollSplit
open import Anonymous_Existence_Populatedness

module Anonymous_Existence_Comparison where

-- Chapter 4.3: Comparison of Notions of Existence

-- Section 4.3.1: Inhabited and Merely Inhabited

-- Lemma 4.3.1
coll-family-dec : ∀ {i} {X : Type i} → (x₁ x₂ : X) → ((x : X) → coll (Coprod (x₁ == x) (x₂ == x))) → Coprod (x₁ == x₂) (¬(x₁ == x₂))
coll-family-dec {i} {X} x₁ x₂ coll-fam = solution where
  f₋ : (x : X) → Coprod (x₁ == x) (x₂ == x) → Coprod (x₁ == x) (x₂ == x)
  f₋ x = fst (coll-fam x)

  E₋ : X → Type i
  E₋ x = fix (f₋ x)

  E : Type i
  E = Σ X λ x → (E₋ x)

  E-fst-determines-eq : (e₁ e₂ : E) → (fst e₁ == fst e₂) → e₁ == e₂
  E-fst-determines-eq e₁ e₂ p = second-comp-triv (λ x → fixed-point (f₋ x) (snd (coll-fam x))) _ _ p

  r : Bool → E
  r true = x₁ , to-fix (f₋ x₁) (snd (coll-fam x₁)) (inl idp)
  r false = x₂ , to-fix (f₋ x₂) (snd (coll-fam x₂)) (inr idp)

  about-r : (r true == r false) ↔ (x₁ == x₂)
  about-r = (λ p → ap fst p) , (λ p → E-fst-determines-eq _ _ p)

  s : E → Bool
  s (_ , inl _ , _) = true
  s (_ , inr _ , _) = false

  s-section-of-r : (e : E) → r(s e) == e
  s-section-of-r (x , inl p , q) = E-fst-determines-eq _ _ p
  s-section-of-r (x , inr p , q) = E-fst-determines-eq _ _ p

  about-s : (e₁ e₂ : E) → (s e₁ == s e₂) ↔ (e₁ == e₂)
  about-s e₁ e₂ = one , two where
    one : (s e₁ == s e₂) → (e₁ == e₂)
    one p =
      e₁       =⟨ ! (s-section-of-r e₁) ⟩
      r(s(e₁)) =⟨ ap r p ⟩
      r(s(e₂)) =⟨ s-section-of-r e₂ ⟩
      e₂       ∎
    two : (e₁ == e₂) → (s e₁ == s e₂)
    two p = ap s p

  combine : (s (r true) == s (r false)) ↔ (x₁ == x₂)
  combine = (about-s _ _) ◎ about-r

  check-bool : Coprod (s (r true) == s (r false)) (¬(s (r true) == s (r false)))
  check-bool = Bool-has-dec-eq _ _

  solution : Coprod (x₁ == x₂) (¬(x₁ == x₂))
  solution with check-bool
  solution | inl p = inl (fst combine p)
  solution | inr np = inr (λ p → np (snd combine p))

-- definition: "all types have a weakly constant endofunction".
-- this assumption is, if we have ∣∣_∣∣, logically equivalent to saying that
-- every type has split support.
all-coll : ∀ {i} → Type (lsucc i)
all-coll {i} = (X : Type i) → coll X

-- Proposition 4.3.2
all-coll→dec-eq : ∀ {i} → all-coll {i} → (X : Type i) → has-dec-eq X
all-coll→dec-eq all-coll X x₁ x₂ = coll-family-dec x₁ x₂ (λ x → all-coll _)

open with-weak-trunc
open wtrunc

--  Proposition 4.3.3
module functional-subrelation {i : ULevel} (ac : all-coll {i}) (X : Type i) (R : X × X → Type i) where

  all-sets : (Y : Type i) → is-set Y
  all-sets Y = pathColl→isSet (λ y₁ y₂ → ac _)

  R₋ : (x : X) → Type i
  R₋ x = Σ X λ y → R(x , y)

  k : (x : X) → (R₋ x) → (R₋ x)
  k x = fst (ac _)

  kc : (x : X) → const (k x)
  kc x = snd (ac _)

  SS : X × X → Type i
  SS (x , y) = Σ (R(x , y)) λ a →
                (y , a) == k x (y , a)

  -- the relation S
  SS₋ : (x : X) → Type i
  SS₋ x = Σ X λ y → SS(x , y)

  -- fix kₓ is equivalent to Sₓ
  -- This is just Σ-assoc. We try to make it more readable by adding some (trivial) steps.
  fixk-SS : (x : X) → (fix (k x)) ≃ SS₋ x
  fixk-SS x =
      (fix (k x))                                           ≃⟨ ide _ ⟩
      (Σ (Σ X λ y → R(x , y)) λ a → a == k x a)             ≃⟨ Σ-assoc ⟩
      (Σ X λ y → Σ (R(x , y)) λ r → (y , r) == k x (y , r)) ≃⟨ ide _ ⟩
      (SS₋ x)                                                ≃∎

  -- claim (0)
  subrelation : (x y : X) → SS(x , y) →  R(x , y)
  subrelation x y (r , _) = r

   -- claim (1)
  prop-SSx : (x : X) → is-prop (SS₋ x)
  prop-SSx x = equiv-preserves-level {A = fix (k x)} {B = (SS₋ x)} (fixk-SS x) (fixed-point _ (kc x))

  -- claim (2)
  same-domain : (x : X) → (R₋ x) ↔ (SS₋ x)
  same-domain x = rs , sr where
    rs : (R₋ x) → (SS₋ x)
    rs a = –> (fixk-SS x) (to-fix (k x) (kc x) a)
    sr : (SS₋ x) → (R₋ x)
    sr (y , r , _) = y , r

  -- claim (3)
  prop-SS : (x y : X) → is-prop (SS (x , y))
  prop-SS x y = all-paths-is-prop all-paths where
    all-paths : (s₁ s₂ : SS(x , y)) → s₁ == s₂
    all-paths s₁ s₂ = ss where

      yss : (y , s₁) == (y , s₂)
      yss = prop-has-all-paths (prop-SSx x) _ _

      ss : s₁ == s₂
      ss = set-lemma (all-sets _) y s₁ s₂ yss

-- intermediate definition
-- see the caveat about the notion 'epimorphism' in the article
is-split-epimorphism : ∀ {i j} {U : Type i} {V : Type j} → (U → V) → Type (i ⊔ j)
is-split-epimorphism {U = U} {V = V} e = Σ (V → U) λ s → (v : V) → e (s v) == v

is-epimorphism : ∀ {i j} {U : Type i} {V : Type j} → (U → V) → Type (lsucc (i ⊔ j))
is-epimorphism {i} {j} {U = U} {V = V} e = (W : Type (i ⊔ j)) → (f g : V → W) → ((u : U) → f (e u) == g (e u)) → (v : V) → f v == g v

-- Lemma 4.3.4
path-trunc-epi→set : ∀ {i} {Y : Type i} → ((y₁ y₂ : Y) → is-epimorphism (∣_∣ {X = y₁ == y₂})) → is-set Y
path-trunc-epi→set {Y = Y} path-epi = reminder special-case where

  f : (y₁ y₂ : Y) → ∣∣ y₁ == y₂ ∣∣ → Y
  f y₁ _ _ = y₁

  g : (y₁ y₂ : Y) → ∣∣ y₁ == y₂ ∣∣ → Y
  g _ y₂ _ = y₂

  special-case : (y₁ y₂ : Y) → ∣∣ y₁ == y₂ ∣∣ → y₁ == y₂
  special-case y₁ y₂ = path-epi y₁ y₂ Y (f y₁ y₂) (g y₁ y₂) (idf _)

  -- we know that hSeparated(X) implies that X is a set,
  -- from the previous Proposition 3.1.9;
  -- however, we have proved it in such a way which forces
  -- us to combine three directions:
  reminder : hSeparated Y → is-set Y
  reminder = (fst (set-characterisations Y)) ∘ (fst (snd (snd (set-characterisations Y)))) ∘ (snd (snd (snd (snd (set-characterisations Y)))))

-- Proposition 4.3.5 (1)
all-split→all-deceq : ∀ {i} → ((X : Type i) → is-split-epimorphism (∣_∣ {X = X})) → (X : Type i) → has-dec-eq X
all-split→all-deceq {i} all-split = all-coll→dec-eq ac where
  ac : (X : Type i) → coll X
  ac X = snd coll↔splitSup (fst (all-split X))

-- Proposition 4.3.5 (2)
all-epi→all-set : ∀ {i} → ((X : Type i) → is-epimorphism (∣_∣ {X = X})) → (X : Type i) → is-set X
all-epi→all-set all-epi X = path-trunc-epi→set (λ y₁ y₂ → all-epi (y₁ == y₂))

-- Section 4.3.2: Merely Inhabited and Populated

-- Lemma 4.3.6, first proof
pop-hstable-1 : ∀ {i} {X : Type i} → ⟪ splitSup X ⟫
pop-hstable-1 {X = X} f c = to-fix f c (coll→splitSup (g , gc)) where

  g : X → X
  g x = f (λ _ → x) ∣ x ∣

  gc : const g
  gc x₁ x₂ =
    g x₁               =⟨ idp ⟩
    f (λ _ → x₁) ∣ x₁ ∣ =⟨ ap (λ k → k ∣ x₁ ∣) (c (λ _ → x₁) (λ _ → x₂)) ⟩
    f (λ _ → x₂) ∣ x₁ ∣ =⟨ ap (f (λ _ → x₂)) (prop-has-all-paths tr-is-prop ∣ x₁ ∣ ∣ x₂ ∣) ⟩
    f (λ _ → x₂) ∣ x₂ ∣ =⟨ idp ⟩
    g x₂               ∎

-- Lemma 4.3.6, second proof
pop-hstable-2 : ∀ {i} {X : Type i} → ⟪ splitSup X ⟫
pop-hstable-2 {i} {X} = snd (pop-alt₂ {X = splitSup X}) get-P where
  get-P : (P : Type i) → is-prop P → splitSup X ↔ P → P
  get-P P pp (hstp , phst) = hstp free-hst where

    xp : X → P
    xp x = hstp (λ _ → x)

    zp : ∣∣ X ∣∣ → P
    zp = tr-rec pp xp

    free-hst : splitSup X
    free-hst z = phst (zp z) z

-- Lemma 4.3.6, third proof
pop-hstable-3 : ∀ {i} {X : Type i} → ⟪ splitSup X ⟫
pop-hstable-3 {X = X} = snd pop-alt translation where

  translation-aux : splitSup (splitSup X) → splitSup X
  translation-aux = λ hsthst z → hsthst (trunc-functorial {X = X} {Y = splitSup X} (λ x _ → x) z) z

  translation :  ∣∣ splitSup (splitSup X) ∣∣ → ∣∣ splitSup X ∣∣
  translation = trunc-functorial translation-aux

-- Lemma 4.3.7
module tlem437 {i : ULevel} where

  One = (X : Type i) → ⟪ X ⟫ → ∣∣ X ∣∣

  Two = (X : Type i) → ∣∣ splitSup X ∣∣

  Three = (P : Type i) → is-prop P → (Y : P → Type i) → ((p : P) → ∣∣ Y p ∣∣) → ∣∣ ((p : P) → Y p) ∣∣

  Four = (X Y : Type i) → (X → Y) → (⟪ X ⟫ → ⟪ Y ⟫)

  One→Two : One → Two
  One→Two poptr X = poptr (splitSup X) pop-hstable-1

  Two→One : Two → One
  Two→One trhst X pop = fst pop-alt pop (trhst X)

  One→Four : One → Four
  One→Four poptr X Y f = Trunc→Pop ∘ (trunc-functorial f) ∘ (poptr X)

  Four→One : Four → One
  Four→One funct X px = prop-pop tr-is-prop pz where -- (tr-rec _) pz where
    pz : ⟪ ∣∣ X ∣∣ ⟫
    pz  =  funct X (∣∣ X ∣∣) ∣_∣ px

  -- only very slightly different to the proof in the article
  One→Three : One → Three
  One→Three poptr P pp Y = λ py → poptr _ (snd pop-alt' (λ hst p₀ → hst (contr-trick p₀ py) p₀)) where
    contr-trick : (p₀ : P) → ((p : P) → ∣∣ Y p ∣∣) → ∣∣ ((p : P) → Y p) ∣∣
    contr-trick p₀ py = tr-rec {X = Y p₀}
                               {P = ∣∣ ((p : P) → Y p) ∣∣}
                               tr-is-prop
                               (λ y₀ → ∣ (λ p → transport Y (prop-has-all-paths pp p₀ p) y₀) ∣)
                               (py p₀)

  Three→Two : Three → Two
  Three→Two proj X = proj (∣∣ X ∣∣) tr-is-prop (λ _ → X) (idf _)

-- Section 4.3.3: Populated and Non-Empty

-- We now need function extensionality. We
-- start with some very simple auxiliary
-- lemmata (not numbered in the thesis).

-- If P is a proposition, so is P + ¬ P
dec-is-prop : ∀ {i} {P : Type i} → is-prop P → is-prop (Coprod P (¬ P))
dec-is-prop {P = P} pp = all-paths-is-prop (λ { (inl p₁) (inl p₂) → ap inl (prop-has-all-paths pp _ _) ;
                                (inl p₁) (inr np₂) → Empty-elim {P = λ _ → inl p₁ == inr np₂} (np₂ p₁) ;
                                (inr np₁) (inl p₂) → Empty-elim {P = λ _ → inr np₁ == inl p₂} (np₁ p₂) ;
                                (inr np₁) (inr np₂) → ap inr (λ= (λ x → prop-has-all-paths Empty-is-prop _ _ )) })

-- Proposition 4.3.8
nonempty-pop→LEM : ∀ {i} → ((X : Type i) → (¬(¬ X) → ⟪ X ⟫)) → LEM {i}
nonempty-pop→LEM {i} nn-pop P pp = from-fix {X = dec} (idf _) (nn-pop dec nndec (idf _) idc) where
  dec : Type i
  dec = Coprod P (¬ P)

  idc : const (idf dec)
  idc = λ _ _ → prop-has-all-paths (dec-is-prop {P = P} pp) _ _

  nndec : ¬(¬ dec)
  nndec ndec = (λ np → ndec (inr np)) λ p → ndec (inl p)

-- Corollary 4.3.9
nonempty-pop↔lem : ∀ {i} → ((X : Type i) → (¬(¬ X) → ⟪ X ⟫)) ↔ LEM {i}
nonempty-pop↔lem {i} = nonempty-pop→LEM , other where
  other : LEM {i} → ((X : Type i) → (¬(¬ X) → ⟪ X ⟫))
  other lem X nnX = p where
    pnp : Coprod ⟪ X ⟫ (¬ ⟪ X ⟫)
    pnp = lem ⟪ X ⟫ pop-property₂

    p : ⟪ X ⟫
    p = match pnp withl idf _ withr (λ np → Empty-elim {P = λ _ → ⟪ X ⟫} (nnX (λ x → np (pop-property₁ x))))

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Luau.RuntimeType where

open import Luau.Syntax using (Value; nil; addr; number; bool; string)

data RuntimeType : Set where
  function : RuntimeType
  number : RuntimeType
  nil : RuntimeType
  boolean : RuntimeType
  string : RuntimeType

valueType : Value → RuntimeType
valueType nil = nil
valueType (addr a) = function
valueType (number n) = number
valueType (bool b) = boolean
valueType (string x) = string

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
{-# OPTIONS --allow-unsolved-metas #-}
module automaton-ex where

open import Data.Nat
open import Data.List
open import Data.Maybe
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Binary.Definitions
open import Relation.Nullary using (¬_; Dec; yes; no)
open import logic

open import automaton
open Automaton

data  StatesQ   : Set  where
   q1 : StatesQ
   q2 : StatesQ
   q3 : StatesQ

data  In2   : Set  where
   i0 : In2
   i1 : In2

transitionQ : StatesQ → In2 → StatesQ
transitionQ q1 i0 = q1
transitionQ q1 i1 = q2
transitionQ q2 i0 = q3
transitionQ q2 i1 = q2
transitionQ q3 i0 = q2
transitionQ q3 i1 = q2

aendQ : StatesQ → Bool
aendQ q2 = true
aendQ _ = false

a1 : Automaton StatesQ In2
a1 = record {
       δ = transitionQ
     ; aend = aendQ
   }

test1 : accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ false
test1 = refl
test2 = accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ i1 ∷ [] )
test3 = trace a1 q1 ( i0 ∷ i1 ∷ i0 ∷ i1 ∷ [] )

data  States1   : Set  where
   sr : States1
   ss : States1
   st : States1

transition1 : States1  → In2  → States1
transition1 sr i0  = sr
transition1 sr i1  = ss
transition1 ss i0  = sr
transition1 ss i1  = st
transition1 st i0  = sr
transition1 st i1  = st

fin1 :  States1  → Bool
fin1 st = true
fin1 ss = false
fin1 sr = false

am1  :  Automaton  States1 In2
am1  =  record {  δ = transition1 ; aend = fin1   }

example1-1 = accept am1 sr ( i0  ∷ i1  ∷ i0  ∷ [] )
example1-2 = accept am1 sr ( i1  ∷ i1  ∷ i1  ∷ [] )
trace-2 = trace am1 sr ( i1  ∷ i1  ∷ i1  ∷ [] )

example1-3 = reachable am1 sr st ( i1  ∷ i1  ∷ i1  ∷ [] )

-- data Dec' (A : Set)  : Set where
--    yes' :   A → Dec' A
--    no'  : ¬ A → Dec' A
--
-- ieq' : (i i' : In2 ) → Dec' ( i ≡ i' )
-- ieq' i0 i0 = yes' refl
-- ieq' i1 i1 = yes' refl
-- ieq' i0 i1 = no' ( λ () )
-- ieq' i1 i0 = no' ( λ () )

ieq : (i i' : In2 ) → Dec ( i ≡ i' )
ieq i0 i0 = yes refl
ieq i1 i1 = yes refl
ieq i0 i1 = no ( λ () )
ieq i1 i0 = no ( λ () )

-- p.83 problem 1.4
--
-- w has at least three i0's and at least two i1's

count-chars : List In2 → In2 → ℕ
count-chars [] _ = 0
count-chars (h ∷ t) x with ieq h x
... | yes y = suc ( count-chars t x )
... | no  n = count-chars t x

test11 : count-chars (  i1  ∷ i1  ∷ i0  ∷ []  ) i0 ≡ 1
test11 = refl

ex1_4a : (x : List In2) → Bool
ex1_4a x =  ( count-chars x i0 ≥b 3 ) /\ ( count-chars x i1 ≥b 2 )

language' : { Σ : Set } → Set
language' {Σ} = List Σ → Bool

lang14a :  language' {In2}
lang14a = ex1_4a

open _∧_

am14a-tr :  ℕ ∧ ℕ → In2 → ℕ ∧ ℕ
am14a-tr p i0 = record { proj1 = suc (proj1 p) ; proj2 = proj2 p }
am14a-tr p i1 = record { proj1 = proj1 p ; proj2 = suc (proj2 p) }

am14a  :  Automaton  (ℕ ∧ ℕ)  In2
am14a  =  record {  δ = am14a-tr ; aend = λ x → ( proj1 x ≥b 3 ) /\ ( proj2 x ≥b 2 )}

data am14s : Set where
  a00 : am14s
  a10 : am14s
  a20 : am14s
  a30 : am14s
  a01 : am14s
  a11 : am14s
  a21 : am14s
  a31 : am14s
  a02 : am14s
  a12 : am14s
  a22 : am14s
  a32 : am14s

am14a-tr' :  am14s  → In2 → am14s
am14a-tr' a00 i0 = a10
am14a-tr' _ _ = a10

am14a'  :  Automaton  am14s  In2
am14a'  =  record {  δ = am14a-tr' ; aend = λ x → {!!} }

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
apply :
  ∀ {a b} {A : Set a} {B : A → Set b} →
  ((x : A) → B x) → (x : A) → B x
apply f x = f x

syntax apply f x = f x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Agda.Primitive
open import Prelude
import GSeTT.Syntax

{- Syntax for a globular type theory, with arbitrary term constructors -}
module Globular-TT.Syntax {l} (index : Set l) where

  data Pre-Ty : Set (lsuc l)
  data Pre-Tm : Set (lsuc l)
  data Pre-Sub : Set (lsuc l)
  data Pre-Ctx : Set (lsuc l)

  data Pre-Ty where
    ∗ : Pre-Ty
    ⇒ : Pre-Ty → Pre-Tm → Pre-Tm → Pre-Ty

  data Pre-Tm where
    Var : ℕ → Pre-Tm
    Tm-constructor : ∀ (i : index) → Pre-Sub → Pre-Tm

  data Pre-Sub where
    <> : Pre-Sub
    <_,_↦_> : Pre-Sub → ℕ → Pre-Tm → Pre-Sub

  data Pre-Ctx where
    ⊘ : Pre-Ctx
    _∙_#_ : Pre-Ctx → ℕ → Pre-Ty → Pre-Ctx

  C-length : Pre-Ctx → ℕ
  C-length ⊘ = O
  C-length (Γ ∙ _ # _) = S (C-length Γ)

  -- Equality elimination
  ⇒= : ∀ {A B t t' u u'} → A == B → t == t' → u == u' → ⇒ A t u == ⇒ B t' u'
  ⇒= idp idp idp = idp

  =⇒ : ∀ {A B t t' u u'} → ⇒ A t u == ⇒ B t' u' → ((A == B) × (t == t')) × (u == u')
  =⇒ idp = (idp , idp) , idp

  Var= : ∀ {v w} → v == w → Var v == Var w
  Var= idp = idp

  Tm-constructor= : ∀ {i j γ δ} → i == j → γ == δ → (Tm-constructor i γ) == (Tm-constructor j δ)
  Tm-constructor= idp idp = idp

  =Tm-constructor : ∀ {i j γ δ} → (Tm-constructor i γ) == (Tm-constructor j δ) → i == j × γ == δ
  =Tm-constructor idp = idp , idp

  <,>= : ∀ {γ δ x y t u} → γ == δ → x == y → t == u → < γ , x ↦ t > == < δ , y ↦ u >
  <,>= idp idp idp = idp

  =<,> : ∀ {γ δ x y t u} → < γ , x ↦ t > == < δ , y ↦ u > → ((γ == δ) × (x == y)) × (t == u)
  =<,> idp = (idp , idp) , idp

  ∙= : ∀ {Γ Δ x y A B} → Γ == Δ → x == y → A == B → (Γ ∙ x # A) == (Δ ∙ y # B)
  ∙= idp idp idp = idp

  {- Action of substitutions on types and terms and substitutions on a syntactical level -}
  _[_]Pre-Ty : Pre-Ty → Pre-Sub → Pre-Ty
  _[_]Pre-Tm : Pre-Tm → Pre-Sub → Pre-Tm
  _∘_ : Pre-Sub → Pre-Sub → Pre-Sub

  ∗ [ σ ]Pre-Ty = ∗
  ⇒ A t u [ σ ]Pre-Ty = ⇒ (A [ σ ]Pre-Ty) (t [ σ ]Pre-Tm) (u [ σ ]Pre-Tm)
  Var x [ <> ]Pre-Tm = Var x
  Var x [ < σ , v ↦ t > ]Pre-Tm = if x ≡ v then t else ((Var x) [ σ ]Pre-Tm)
  Tm-constructor i γ [ σ ]Pre-Tm = Tm-constructor i (γ ∘ σ)
  <> ∘ γ = <>
  < γ , x ↦ t > ∘ δ = < γ ∘ δ , x ↦ t [ δ ]Pre-Tm >

  _#_∈_ : ℕ → Pre-Ty → Pre-Ctx → Set (lsuc l)
  _ # _ ∈ ⊘ = ⊥
  x # A ∈ (Γ ∙ y # B) = (x # A ∈ Γ) + ((x == y) × (A == B))

  {- dimension of types -}
  dim : Pre-Ty → ℕ
  dim ∗ = O
  dim (⇒ A t u) = S (dim A)

  dim[] : ∀ (A : Pre-Ty) (γ : Pre-Sub) → dim (A [ γ ]Pre-Ty) == dim A
  dim[] ∗ γ = idp
  dim[] (⇒ A x x₁) γ = S= (dim[] A γ)

  dimC : Pre-Ctx → ℕ
  dimC ⊘ = O
  dimC (Γ ∙ x # A) = max (dimC Γ) (dim A)

  {- Identity and canonical projection -}
  Pre-id : ∀ (Γ : Pre-Ctx) → Pre-Sub
  Pre-id ⊘ = <>
  Pre-id (Γ ∙ x # A) = < Pre-id Γ , x ↦ Var x >

  Pre-π : ∀ (Γ : Pre-Ctx) (x : ℕ) (A : Pre-Ty) → Pre-Sub
  Pre-π Γ x A = Pre-id Γ

  {- Translation of GSeTT to a globular-TT -}
  GPre-Ctx : GSeTT.Syntax.Pre-Ctx → Pre-Ctx
  GPre-Ty : GSeTT.Syntax.Pre-Ty → Pre-Ty
  GPre-Tm : GSeTT.Syntax.Pre-Tm → Pre-Tm

  GPre-Ctx nil = ⊘
  GPre-Ctx (Γ :: (x , A)) = (GPre-Ctx Γ) ∙ x # (GPre-Ty A)
  GPre-Ty GSeTT.Syntax.∗ = ∗
  GPre-Ty (GSeTT.Syntax.⇒ A t u) = ⇒ (GPre-Ty A) (GPre-Tm t) (GPre-Tm u)
  GPre-Tm (GSeTT.Syntax.Var x) = Var x

  {- Depth of a term -}
  depth : Pre-Tm → ℕ
  depthS : Pre-Sub → ℕ

  depth (Var x) = O
  depth (Tm-constructor i γ) = S (depthS γ)

  depthS <> = O
  depthS < γ , x ↦ t > = max (depthS γ) (depth t)

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization