text:
module Lambda where

open import Prelude
open import Star
open import Examples
open import Modal

-- Environments

record TyAlg (ty : Set) : Set where
  field
    nat : ty
    _⟶_ : ty -> ty -> ty

data Ty : Set where
  <nat> : Ty
  _<⟶>_ : Ty -> Ty -> Ty

freeTyAlg : TyAlg Ty
freeTyAlg = record { nat = <nat>; _⟶_ = _<⟶>_ }

termTyAlg : TyAlg True
termTyAlg = record { nat = _; _⟶_ = \_ _ -> _ }

record TyArrow {ty₁ ty₂ : Set}(T₁ : TyAlg ty₁)(T₂ : TyAlg ty₂) : Set where
  field
    apply   : ty₁ -> ty₂
    respNat : apply (TyAlg.nat T₁) == TyAlg.nat T₂
    resp⟶   : forall {τ₁ τ₂} ->
              apply (TyAlg._⟶_ T₁ τ₁ τ₂) == TyAlg._⟶_ T₂ (apply τ₁) (apply τ₂)

_=Ty=>_ : {ty₁ ty₂ : Set}(T₁ : TyAlg ty₁)(T₂ : TyAlg ty₂) -> Set
_=Ty=>_ = TyArrow

!Ty : {ty : Set}{T : TyAlg ty} -> T =Ty=> termTyAlg
!Ty = record { apply   = !
             ; respNat = refl
             ; resp⟶   = refl
             }

Ctx : Set
Ctx = List Ty

Var : {ty : Set} -> List ty -> ty -> Set
Var Γ τ = Any (_==_ τ) Γ

vzero : {τ : Ty} {Γ : Ctx} -> Var (τ • Γ) τ
vzero = done refl • ε

vsuc : {σ τ : Ty} {Γ : Ctx} -> Var Γ τ -> Var (σ • Γ) τ
vsuc v = step • v

module Term {ty : Set}(T : TyAlg ty) where

  private open module TT = TyAlg T

  data Tm : List ty -> ty -> Set where
    var : forall {Γ τ}   -> Var Γ τ -> Tm Γ τ
    zz  : forall {Γ}     -> Tm Γ nat
    ss  : forall {Γ}     -> Tm Γ (nat ⟶ nat)
    ƛ   : forall {Γ σ τ} -> Tm (σ • Γ) τ -> Tm Γ (σ ⟶ τ)
    _$_ : forall {Γ σ τ} -> Tm Γ (σ ⟶ τ) -> Tm Γ σ -> Tm Γ τ

module Eval where

 private open module TT = Term freeTyAlg

 ty⟦_⟧ : Ty -> Set
 ty⟦ <nat>   ⟧ = Nat
 ty⟦ σ <⟶> τ ⟧ = ty⟦ σ ⟧ -> ty⟦ τ ⟧

 Env : Ctx -> Set
 Env = All ty⟦_⟧

 _[_] : forall {Γ τ} -> Env Γ -> Var Γ τ -> ty⟦ τ ⟧
 ρ [ x ] with lookup x ρ
 ...     | result _ refl v = v

 ⟦_⟧_ : forall {Γ τ} -> Tm Γ τ -> Env Γ -> ty⟦ τ ⟧
 ⟦ var x ⟧ ρ = ρ [ x ]
 ⟦ zz    ⟧ ρ = zero
 ⟦ ss    ⟧ ρ = suc
 ⟦ ƛ t   ⟧ ρ = \x -> ⟦ t ⟧ (check x • ρ)
 ⟦ s $ t ⟧ ρ = (⟦ s ⟧ ρ) (⟦ t ⟧ ρ)

module MoreExamples where

  private open module TT = TyAlg freeTyAlg
  private open module Tm = Term freeTyAlg
  open Eval

  tm-one : Tm ε nat
  tm-one = ss $ zz

  tm-id : Tm ε (nat ⟶ nat)
  tm-id = ƛ (var (done refl • ε))

  tm    : Tm ε nat
  tm    = tm-id $ tm-one

  tm-twice : Tm ε ((nat ⟶ nat) ⟶ (nat ⟶ nat))
  tm-twice = ƛ (ƛ (f $ (f $ x)))
    where Γ : Ctx
          Γ = nat • (nat ⟶ nat) • ε
          f : Tm Γ (nat ⟶ nat)
          f = var (vsuc vzero)
          x : Tm Γ nat
          x = var vzero

  sem : {τ : Ty} -> Tm ε τ -> ty⟦ τ ⟧
  sem e = ⟦ e ⟧ ε

  one : Nat
  one = sem tm

  twice : (Nat -> Nat) -> (Nat -> Nat)
  twice = sem tm-twice


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

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Fin
open import Data.Nat hiding ( _≟_ )
open import Data.List hiding ( any ;  [_] )
-- import Data.Bool using ( Bool ; true ; false ; _∧_ )
-- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
open import  Relation.Binary.PropositionalEquality as RBF hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import regex
open import logic

-- postulate a b c d : Set

data In : Set where
   a : In
   b : In
   c : In
   d : In

-- infixr 40 _&_ _||_

r1' =    (< a > & < b >) & < c >                                         --- abc
r1 =    < a > &  < b > & < c >                                            --- abc
r0 : ¬ (r1' ≡ r1)
r0 ()
any = < a > || < b >  || < c > || < d >                                   --- a|b|c|d
r2 =    ( any * ) & ( < a > & < b > & < c > )                            -- .*abc
r3 =    ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
r4 =    ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
r5 =    ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )

open import nfa

--    former ++ later  ≡ x
split : {Σ : Set} → ((former : List Σ) → Bool) → ((later :  List Σ) → Bool) → (x : List Σ ) → Bool
split x y  [] = x [] /\ y []
split x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
  split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t

-- tt1 : {Σ : Set} → ( P Q :  List In → Bool ) → split P Q ( a ∷ b ∷ c ∷ [] )
-- tt1 P Q = ?

{-# TERMINATING #-}
repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
repeat x [] = true
repeat {Σ} x ( h  ∷ t ) = split x (repeat {Σ} x) ( h  ∷ t )

-- Meaning of regular expression

regular-language : {Σ : Set} → Regex Σ → ((x y : Σ ) → Dec (x ≡ y))  →  List Σ → Bool
regular-language φ cmp _ = false
regular-language ε cmp [] = true
regular-language ε cmp (_ ∷ _) = false
regular-language (x *) cmp = repeat ( regular-language x cmp  )
regular-language (x & y) cmp  = split ( λ z → regular-language x  cmp z ) (λ z →  regular-language y  cmp z )
regular-language (x || y) cmp  = λ s → ( regular-language x  cmp s )  \/  ( regular-language y  cmp s)
regular-language < h > cmp  [] = false
regular-language < h > cmp  (h1  ∷ [] ) with cmp h h1
... | yes _ = true
... | no _  = false
regular-language < h >  _ (_ ∷ _ ∷ _)  = false

cmpi : (x y : In ) → Dec (x ≡ y)
cmpi a a = yes refl
cmpi b b =  yes refl
cmpi c c =  yes refl
cmpi d d =  yes refl
cmpi a b =  no (λ ())
cmpi a c =  no (λ ())
cmpi a d =  no (λ ())
cmpi b a = no (λ ())
cmpi b c = no (λ ())
cmpi b d = no (λ ())
cmpi c a = no (λ ())
cmpi c b = no (λ ())
cmpi c d = no (λ ())
cmpi d a = no (λ ())
cmpi d b = no (λ ())
cmpi d c = no (λ ())

test-regex : regular-language r1' cmpi ( a ∷ [] ) ≡ false
test-regex = refl

test-regex1 : regular-language r2 cmpi ( a ∷ a ∷ b ∷ c ∷ [] ) ≡ true
test-regex1 = refl

test-AB→split : {Σ : Set} → {A B : List In → Bool} → split A B ( a ∷ b ∷ a ∷ [] ) ≡ (
       ( A [] /\ B ( a ∷ b ∷ a ∷ [] ) ) \/
       ( A ( a ∷ [] ) /\ B ( b ∷ a ∷ [] ) ) \/
       ( A ( a ∷ b ∷ [] ) /\ B ( a ∷ [] ) ) \/
       ( A ( a ∷ b ∷ a ∷ [] ) /\ B  []  )
   )
test-AB→split {_} {A} {B} = refl

list-eq : {Σ : Set} → (cmpi : (s t : Σ)  → Dec (s ≡ t ))  → (s t : List Σ ) → Bool
list-eq cmpi [] [] = true
list-eq cmpi [] (x ∷ t) = false
list-eq cmpi (x ∷ s) [] = false
list-eq cmpi (x ∷ s) (y ∷ t) with cmpi x y
... | yes _ = list-eq cmpi s t
... | no _ = false

-- split-spec-01 :  {s t u : List In } → s ++ t ≡ u → split (list-eq cmpi s) (list-eq cmpi t)  u ≡ true
-- split-spec-01 = {!!}

-- from example 1.53 1

ex53-1 : Set
ex53-1 = (s : List In ) → regular-language ( (< a > *) & < b > & (< a > *) ) cmpi s ≡ true → {!!} -- contains exact one b

ex53-2 : Set
ex53-2 = (s : List In ) → regular-language ( (any * ) & < b > & (any *) ) cmpi s ≡ true → {!!} -- contains at lease one b

evenp : {Σ : Set} →  List Σ → Bool
oddp : {Σ : Set} →  List Σ → Bool
oddp [] = false
oddp (_ ∷ t) = evenp t

evenp [] = true
evenp (_ ∷ t) = oddp t

-- from example 1.53 5
egex-even : Set
egex-even = (s : List In ) → regular-language ( ( any & any ) * ) cmpi s ≡ true → evenp s ≡ true

test11 =  regular-language ( ( any & any ) * ) cmpi (a ∷ [])
test12 =  regular-language ( ( any & any ) * ) cmpi (a ∷ b ∷ [])

-- proof-egex-even : egex-even
-- proof-egex-even [] _ = refl
-- proof-egex-even (a ∷ []) ()
-- proof-egex-even (b ∷ []) ()
-- proof-egex-even (c ∷ []) ()
-- proof-egex-even (x ∷ x₁ ∷ s) y = proof-egex-even s {!!}

open import finiteSet

iFin : FiniteSet In
iFin = record {
     finite = finite0
   ; Q←F = Q←F0
   ; F←Q = F←Q0
   ; finiso→ = finiso→0
   ; finiso← = finiso←0
 } where
     finite0 : ℕ
     finite0 = 4
     Q←F0 : Fin finite0 → In
     Q←F0 zero = a
     Q←F0 (suc zero) = b
     Q←F0 (suc (suc zero)) = c
     Q←F0 (suc (suc (suc zero))) = d
     F←Q0 : In → Fin finite0
     F←Q0 a = # 0
     F←Q0 b = # 1
     F←Q0 c = # 2
     F←Q0 d = # 3
     finiso→0 : (q : In) → Q←F0 ( F←Q0 q ) ≡ q
     finiso→0 a = refl
     finiso→0 b = refl
     finiso→0 c =  refl
     finiso→0 d =  refl
     finiso←0 : (f : Fin finite0 ) → F←Q0 ( Q←F0 f ) ≡ f
     finiso←0 zero = refl
     finiso←0 (suc zero) = refl
     finiso←0 (suc (suc zero)) = refl
     finiso←0 (suc (suc (suc zero))) = refl

open import derive In iFin
open import automaton

ra-ex = trace (regex→automaton cmpi r2) (record { state = r2 ; is-derived = unit }) ( a ∷ b ∷ c ∷ [])

ext: agda

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:
------------------------------------------------------------------------
-- Labelled transition systems
------------------------------------------------------------------------

{-# OPTIONS --safe #-}

module Labelled-transition-system where

open import Equality.Propositional
import Logical-equivalence
open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Equivalence equality-with-J using (↔⇒≃)
open import Function-universe equality-with-J hiding (id; _∘_)
open import Univalence-axiom equality-with-J

-- Labelled transition systems were perhaps first defined by Robert M.
-- Keller (https://doi.org/10.1145/360248.360251). The definition
-- below is a variant with a field "is-silent", added by me.
--
-- I don't know who first came up with the concept of a weak
-- transition. The definitions of _⇒_, _[_]⇒_, _[_]⇒̂_ and _[_]⟶̂_ below
-- are based on definitions in "Enhancements of the bisimulation proof
-- method" by Pous and Sangiorgi.

record LTS ℓ : Type (lsuc ℓ) where
  infix 4 _[_]⟶_ _⇒_ _[_]⇒_ _[_]⇒̂_ _[_]⟶̂_
  field
    -- Processes.
    Proc : Type ℓ

    -- Labels.
    Label : Type ℓ

    -- Transitions.
    _[_]⟶_ : Proc → Label → Proc → Type ℓ

    -- Is the label silent?
    is-silent : Label → Bool

  -- Is the label silent?

  Silent : Label → Type
  Silent μ with is-silent μ
  ... | true  = ⊤
  ... | false = ⊥

  -- Silence can be decided.

  silent? : ∀ μ → Dec (Silent μ)
  silent? μ with is-silent μ
  ... | true  = yes _
  ... | false = no id

  -- Sequences of zero or more silent transitions.

  data _⇒_ : Proc → Proc → Type ℓ where
    done : ∀ {p} → p ⇒ p
    step : ∀ {p q r μ} → Silent μ → p [ μ ]⟶ q → q ⇒ r → p ⇒ r

  -- Weak transitions (one kind).

  data _[_]⇒_ (p : Proc) (μ : Label) (q : Proc) : Type ℓ where
    steps : ∀ {p′ q′} → p ⇒ p′ → p′ [ μ ]⟶ q′ → q′ ⇒ q → p [ μ ]⇒ q

  -- Weak transitions (another kind).

  data _[_]⇒̂_ (p : Proc) (μ : Label) (q : Proc) : Type ℓ where
    silent     : Silent μ → p ⇒ q → p [ μ ]⇒̂ q
    non-silent : ¬ Silent μ → p [ μ ]⇒ q → p [ μ ]⇒̂ q

  -- Weak transitions (yet another kind).

  data _[_]⟶̂_ (p : Proc) (μ : Label) : Proc → Type ℓ where
    done : Silent μ → p [ μ ]⟶̂ p
    step : ∀ {q} → p [ μ ]⟶ q → p [ μ ]⟶̂ q

  -- Functions that can be used to aid the instance resolution
  -- mechanism.

  infix -2 ⟶:_ ⇒:_ []⇒:_ ⇒̂:_ ⟶̂:_

  ⟶:_ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]⟶ q
  ⟶:_ = id

  ⇒:_ : ∀ {p q} → p ⇒ q → p ⇒ q
  ⇒:_ = id

  []⇒:_ : ∀ {p μ q} → p [ μ ]⇒ q → p [ μ ]⇒ q
  []⇒:_ = id

  ⇒̂:_ : ∀ {p μ q} → p [ μ ]⇒̂ q → p [ μ ]⇒̂ q
  ⇒̂:_ = id

  ⟶̂:_ : ∀ {p μ q} → p [ μ ]⟶̂ q → p [ μ ]⟶̂ q
  ⟶̂:_ = id

  -- An "equational" reasoning combinator that is not subsumed by the
  -- combinators in Equational-reasoning, because the types of the two
  -- main arguments and the result use three different relations.

  infixr -2 ⟶⇒→[]⇒

  ⟶⇒→[]⇒ : ∀ p μ {q r} → p [ μ ]⟶ q → q ⇒ r → p [ μ ]⇒ r
  ⟶⇒→[]⇒ _ _ = steps done

  syntax ⟶⇒→[]⇒ p μ p⟶q q⇒r = p [ μ ]⇒⟨ p⟶q ⟩ q⇒r

  -- Combinators that can be used to add visible type information to
  -- an expression.

  infix -1 step-with-action step-without-action

  step-with-action : ∀ p μ q → p [ μ ]⟶ q → p [ μ ]⟶ q
  step-with-action _ _ _ p⟶q = p⟶q

  step-without-action : ∀ p {μ} q → p [ μ ]⟶ q → p [ μ ]⟶ q
  step-without-action _ _ p⟶q = p⟶q

  syntax step-with-action    p μ q p⟶q = p [ μ ]⟶⟨ p⟶q ⟩ q
  syntax step-without-action p   q p⟶q = p      ⟶⟨ p⟶q ⟩ q

  -- Regular transitions can (sometimes) be turned into weak ones.

  ⟶→⇒ : ∀ {p μ q} → Silent μ → p [ μ ]⟶ q → p ⇒ q
  ⟶→⇒ s tr = step s tr done

  ⟶→[]⇒ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]⇒ q
  ⟶→[]⇒ tr = steps done tr done

  ⟶→⇒̂ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]⇒̂ q
  ⟶→⇒̂ {μ = μ} tr with silent? μ
  ... | yes s = silent s (⟶→⇒ s tr)
  ... | no ¬s = non-silent ¬s (⟶→[]⇒ tr)

  ⟶→⟶̂ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]⟶̂ q
  ⟶→⟶̂ = step

  -- Several transitivity-like properties.

  ⇒-transitive : ∀ {p q r} → p ⇒ q → q ⇒ r → p ⇒ r
  ⇒-transitive done             p⇒q = p⇒q
  ⇒-transitive (step s p⟶q q⇒r) r⇒s = step s p⟶q (⇒-transitive q⇒r r⇒s)

  ⇒[]⇒-transitive : ∀ {p q r μ} → p ⇒ q → q [ μ ]⇒ r → p [ μ ]⇒ r
  ⇒[]⇒-transitive p⇒q (steps q⇒r r⟶s s⇒t) =
    steps (⇒-transitive p⇒q q⇒r) r⟶s s⇒t

  []⇒⇒-transitive : ∀ {p q r μ} → p [ μ ]⇒ q → q ⇒ r → p [ μ ]⇒ r
  []⇒⇒-transitive (steps p⇒q q⟶r r⇒s) s⇒t =
    steps p⇒q q⟶r (⇒-transitive r⇒s s⇒t)

  ⇒⇒̂-transitive : ∀ {p q r μ} → p ⇒ q → q [ μ ]⇒̂ r → p [ μ ]⇒̂ r
  ⇒⇒̂-transitive p⇒q (silent s q⇒r) = silent s (⇒-transitive p⇒q q⇒r)
  ⇒⇒̂-transitive p⇒q (non-silent ¬s q⇒r) =
    non-silent ¬s (⇒[]⇒-transitive p⇒q q⇒r)

  ⇒̂⇒-transitive : ∀ {p q r μ} → p [ μ ]⇒̂ q → q ⇒ r → p [ μ ]⇒̂ r
  ⇒̂⇒-transitive (silent s p⇒q) q⇒r = silent s (⇒-transitive p⇒q q⇒r)
  ⇒̂⇒-transitive (non-silent ¬s p⇒q) q⇒r =
    non-silent ¬s ([]⇒⇒-transitive p⇒q q⇒r)

  -- More conversion functions.

  []⇒→⇒ : ∀ {p q μ} → Silent μ → p [ μ ]⇒ q → p ⇒ q
  []⇒→⇒ s (steps p⇒p′ p′⟶p″ p″⇒p‴) =
    ⇒-transitive p⇒p′ (step s p′⟶p″ p″⇒p‴)

  ⇒̂→⇒ : ∀ {p q μ} → Silent μ → p [ μ ]⇒̂ q → p ⇒ q
  ⇒̂→⇒ s (silent _ p⇒q)    = p⇒q
  ⇒̂→⇒ s (non-silent ¬s _) = ⊥-elim (¬s s)

  ⇒→⇒̂ : ∀ {p q μ} → p [ μ ]⇒ q → p [ μ ]⇒̂ q
  ⇒→⇒̂ {μ = μ} tr with silent? μ
  ... | yes s = silent s ([]⇒→⇒ s tr)
  ... | no ¬s = non-silent ¬s tr

  ⇒̂→[]⇒ : ∀ {p q μ} → ¬ Silent μ → p [ μ ]⇒̂ q → p [ μ ]⇒ q
  ⇒̂→[]⇒ ¬s (silent s _)      = ⊥-elim (¬s s)
  ⇒̂→[]⇒ _  (non-silent _ tr) = tr

  ⟶̂→⇒̂ : ∀ {p μ q} → p [ μ ]⟶̂ q → p [ μ ]⇒̂ q
  ⟶̂→⇒̂ (done s)  = silent s done
  ⟶̂→⇒̂ (step tr) = ⟶→⇒̂ tr

  ⟶̂→⇒ : ∀ {p q μ} → Silent μ → p [ μ ]⟶̂ q → p ⇒ q
  ⟶̂→⇒ s = ⇒̂→⇒ s ∘ ⟶̂→⇒̂

  -- Lemmas that can be used to show that relations are weak
  -- simulations of various kinds.

  module _
    {ℓ}
    {_%_ _%′_ : Proc → Proc → Type ℓ}
    {_[_]%_ : Proc → Label → Proc → Type ℓ}
    (left-to-right :
       ∀ {p q} → p % q → ∀ {p′ μ} →
       p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]% q′ × p′ %′ q′)
    (%′⇒% : ∀ {p q} → p %′ q → p % q)
    (%⇒⇒ : ∀ {p p′ μ} → Silent μ → p [ μ ]% p′ → p ⇒ p′)
    where

    is-weak⇒ :
      ∀ {p p′ q} →
      p % q → p ⇒ p′ →
      ∃ λ q′ → q ⇒ q′ × (p′ % q′)
    is-weak⇒ p%q done                = _ , done , p%q
    is-weak⇒ p%q (step s p⟶p′ p′⇒p″) =
      let q′ , q%q′  , p′%′q′ = left-to-right p%q p⟶p′
          q″ , q′⇒q″ , p″%q″  = is-weak⇒ (%′⇒% p′%′q′) p′⇒p″
      in q″ , ⇒-transitive (%⇒⇒ s q%q′) q′⇒q″ , p″%q″

    is-weak[]⇒ :
      ∀ {p p′ q μ} →
      (∀ {p p′} → p [ μ ]% p′ → p [ μ ]⇒ p′) →
      p % q → p [ μ ]⇒ p′ →
      ∃ λ q′ → q [ μ ]⇒ q′ × (p′ % q′)
    is-weak[]⇒ %⇒[]⇒ p%q (steps p⇒p′ p′⟶p″ p″⇒p‴) =
      let q′ , q⇒q′  , p′%q′  = is-weak⇒ p%q p⇒p′
          q″ , q′%q″ , p″%′q″ = left-to-right p′%q′ p′⟶p″
          q‴ , q″⇒q‴ , p‴%q‴  = is-weak⇒ (%′⇒% p″%′q″) p″⇒p‴
      in q‴
       , ⇒[]⇒-transitive q⇒q′ ([]⇒⇒-transitive (%⇒[]⇒ q′%q″) q″⇒q‴)
       , p‴%q‴

    is-weak⇒̂ :
      ∀ {p p′ q μ} →
      (∀ {p p′} → p [ μ ]% p′ → p [ μ ]⇒̂ p′) →
      p % q → p [ μ ]⇒̂ p′ →
      ∃ λ q′ → q [ μ ]⇒̂ q′ × (p′ % q′)
    is-weak⇒̂ _ q%r (silent s q⇒q′) =
      Σ-map id (Σ-map (silent s) id) (is-weak⇒ q%r q⇒q′)
    is-weak⇒̂ %⇒⇒̂ q%r (non-silent ¬s q⇒q′) =
      Σ-map id (Σ-map ⇒→⇒̂ id) (is-weak[]⇒ (⇒̂→[]⇒ ¬s ∘ %⇒⇒̂) q%r q⇒q′)

  -- If no action is silent, then _[_]⇒_ is pointwise isomorphic to
  -- _[_]⟶_.

  ⟶↔⇒ : (∀ μ → ¬ Silent μ) →
        ∀ {p μ q} → p [ μ ]⟶ q ↔ p [ μ ]⇒ q
  ⟶↔⇒ ¬silent = record
    { surjection = record
      { logical-equivalence = record
        { to   = ⟶→[]⇒
        ; from = λ
            { (steps (step s _ _) _ _) → ⊥-elim (¬silent _ s)
            ; (steps _ _ (step s _ _)) → ⊥-elim (¬silent _ s)
            ; (steps done tr done)     → tr
            }
        }
      ; right-inverse-of = λ
          { (steps (step s _ _) _ _) → ⊥-elim (¬silent _ s)
          ; (steps _ _ (step s _ _)) → ⊥-elim (¬silent _ s)
          ; (steps done tr done)     → refl
          }
      }
    ; left-inverse-of = λ _ → refl
    }

  -- If no action is silent, then _[_]⇒̂_ is pointwise logically
  -- equivalent to _[_]⟶_, and in the presence of extensionality they
  -- are pointwise isomorphic.

  ⟶↔⇒̂ : ∀ {k} →
        Extensionality? k lzero lzero →
        (∀ μ → ¬ Silent μ) →
        ∀ {p μ q} → p [ μ ]⟶ q ↝[ k ] p [ μ ]⇒̂ q
  ⟶↔⇒̂ ext ¬silent = generalise-ext?
    ⟶⇔⇒̂
    (λ ext →
         (λ { (silent s _)      → ⊥-elim (¬silent _ s)
            ; (non-silent _ tr) →
                cong₂ non-silent
                      (apply-ext ext (⊥-elim ∘ ¬silent _))
                      (_↔_.right-inverse-of (⟶↔⇒ ¬silent) tr)
            })
       , (λ _ → refl))
    ext
    where
    ⟶⇔⇒̂ = record
      { to   = λ tr → non-silent (¬silent _) (_↔_.to (⟶↔⇒ ¬silent) tr)
      ; from = λ
          { (silent s _)      → ⊥-elim (¬silent _ s)
          ; (non-silent _ tr) → _↔_.from (⟶↔⇒ ¬silent) tr
          }
      }

  -- Map-like functions.

  map-⇒′ :
    {F : Proc → Proc} →
    (∀ {p p′ μ} → Silent μ → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    ∀ {p p′} → p ⇒ p′ → F p ⇒ F p′
  map-⇒′ f done                = done
  map-⇒′ f (step s p⟶p′ p′⇒p″) =
    step s (f s p⟶p′) (map-⇒′ f p′⇒p″)

  map-⇒ :
    {F : Proc → Proc} →
    (∀ {p p′ μ} → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    ∀ {p p′} → p ⇒ p′ → F p ⇒ F p′
  map-⇒ f = map-⇒′ (λ _ → f)

  map-[]⇒′ :
    ∀ {μ} {F : Proc → Proc} →
    (∀ {p p′ μ} → Silent μ → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    (∀ {p p′} → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    ∀ {p p′} → p [ μ ]⇒ p′ → F p [ μ ]⇒ F p′
  map-[]⇒′ f g (steps p⇒p′ p′⟶p″ p″⇒p‴) =
    steps (map-⇒′ f p⇒p′) (g p′⟶p″) (map-⇒′ f p″⇒p‴)

  map-[]⇒ :
    {F : Proc → Proc} →
    (∀ {p p′ μ} → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    ∀ {p p′ μ} → p [ μ ]⇒ p′ → F p [ μ ]⇒ F p′
  map-[]⇒ f = map-[]⇒′ (λ _ → f) f

  map-⇒̂′ :
    ∀ {μ} {F : Proc → Proc} →
    (∀ {p p′ μ} → Silent μ → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    (∀ {p p′} → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    ∀ {p p′} → p [ μ ]⇒̂ p′ → F p [ μ ]⇒̂ F p′
  map-⇒̂′ f g (silent s p⇒p′)      = silent s (map-⇒′ f p⇒p′)
  map-⇒̂′ f g (non-silent ¬s p⇒p′) = non-silent ¬s (map-[]⇒′ f g p⇒p′)

  map-⇒̂ :
    {F : Proc → Proc} →
    (∀ {p p′ μ} → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    ∀ {p p′ μ} → p [ μ ]⇒̂ p′ → F p [ μ ]⇒̂ F p′
  map-⇒̂ f = map-⇒̂′ (λ _ → f) f

  map-⟶̂ :
    ∀ {μ p p′} {F : Proc → Proc} →
    (p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    p [ μ ]⟶̂ p′ → F p [ μ ]⟶̂ F p′
  map-⟶̂ f (done s)    = done s
  map-⟶̂ f (step p⟶p′) = step (f p⟶p′)

  -- Zip-like functions.

  module _
    {F : Proc → Proc → Proc}
    (f : ∀ {p p′ q μ} → p [ μ ]⟶ p′ → F p q [ μ ]⟶ F p′ q)
    (g : ∀ {p q q′ μ} → q [ μ ]⟶ q′ → F p q [ μ ]⟶ F p q′)
    where

    zip-⇒ : ∀ {p p′ q q′} → p ⇒ p′ → q ⇒ q′ → F p q ⇒ F p′ q′
    zip-⇒ done done                = done
    zip-⇒ done (step s q⟶q′ q′⇒q″) = step s (g q⟶q′) (zip-⇒ done q′⇒q″)
    zip-⇒ (step s p⟶p′ p′⇒p″) tr   = step s (f p⟶p′) (zip-⇒ p′⇒p″ tr)

    zip-[]⇒ˡ′ :
      ∀ {p p′ q q′ μ₁ μ₃} →
      (∀ {p p′ q} → p [ μ₁ ]⟶ p′ → F p q [ μ₃ ]⟶ F p′ q) →
      p [ μ₁ ]⇒ p′ → q ⇒ q′ → F p q [ μ₃ ]⇒ F p′ q′
    zip-[]⇒ˡ′ h (steps p⇒p′ p′⟶p″ p″⇒p‴) q⇒q′ =
      steps (zip-⇒ p⇒p′ q⇒q′) (h p′⟶p″) (zip-⇒ p″⇒p‴ done)

    zip-[]⇒ˡ : ∀ {p p′ q q′ μ} →
               p [ μ ]⇒ p′ → q ⇒ q′ → F p q [ μ ]⇒ F p′ q′
    zip-[]⇒ˡ = zip-[]⇒ˡ′ f

    zip-[]⇒ʳ′ :
      ∀ {p p′ q q′ μ₂ μ₃} →
      (∀ {p q q′} → q [ μ₂ ]⟶ q′ → F p q [ μ₃ ]⟶ F p q′) →
      p ⇒ p′ → q [ μ₂ ]⇒ q′ → F p q [ μ₃ ]⇒ F p′ q′
    zip-[]⇒ʳ′ h p⇒p′ (steps q⇒q′ q′⟶q″ q″⇒q‴) =
      steps (zip-⇒ p⇒p′ q⇒q′) (h q′⟶q″) (zip-⇒ done q″⇒q‴)

    zip-[]⇒ʳ : ∀ {p p′ q q′ μ} →
               p ⇒ p′ → q [ μ ]⇒ q′ → F p q [ μ ]⇒ F p′ q′
    zip-[]⇒ʳ = zip-[]⇒ʳ′ g

    zip-[]⇒ :
      ∀ {μ₁ μ₂ μ₃} →
      (∀ {p p′ q q′} →
       p [ μ₁ ]⟶ p′ → q [ μ₂ ]⟶ q′ → F p q [ μ₃ ]⟶ F p′ q′) →
      ∀ {p p′ q q′} →
      p [ μ₁ ]⇒ p′ → q [ μ₂ ]⇒ q′ → F p q [ μ₃ ]⇒ F p′ q′
    zip-[]⇒ h (steps p⇒p′ p′⟶p″ p″⇒p‴) (steps q⇒q′ q′⟶q″ q″⇒q‴) =
      steps (zip-⇒ p⇒p′ q⇒q′) (h p′⟶p″ q′⟶q″) (zip-⇒ p″⇒p‴ q″⇒q‴)

    zip-⇒̂ :
      ∀ {μ₁ μ₂ μ₃} →
      (Silent μ₁ → Silent μ₂ → Silent μ₃) →
      (∀ {p p′ q} → p [ μ₁ ]⟶ p′ → Silent μ₂ → F p q [ μ₃ ]⟶ F p′ q) →
      (∀ {p q q′} → Silent μ₁ → q [ μ₂ ]⟶ q′ → F p q [ μ₃ ]⟶ F p q′) →
      (∀ {p p′ q q′} →
       p [ μ₁ ]⟶ p′ → q [ μ₂ ]⟶ q′ → F p q [ μ₃ ]⟶ F p′ q′) →
      ∀ {p p′ q q′} →
      p [ μ₁ ]⇒̂ p′ → q [ μ₂ ]⇒̂ q′ → F p q [ μ₃ ]⇒̂ F p′ q′
    zip-⇒̂ fs hˡ hʳ h = λ where
      (silent s₁ tr₁)      (silent s₂ tr₂)      → silent (fs s₁ s₂) (zip-⇒ tr₁ tr₂)
      (silent s₁ tr₁)      (non-silent ¬s₂ tr₂) → ⇒→⇒̂ (zip-[]⇒ʳ′ (hʳ s₁)      tr₁ tr₂)
      (non-silent ¬s₁ tr₁) (silent s₂ tr₂)      → ⇒→⇒̂ (zip-[]⇒ˡ′ (flip hˡ s₂) tr₁ tr₂)
      (non-silent ¬s₁ tr₁) (non-silent ¬s₂ tr₂) → ⇒→⇒̂ (zip-[]⇒   h            tr₁ tr₂)

  zip-⟶̂ :
    ∀ {F : Proc → Proc → Proc} {μ₁ μ₂ μ₃} →
    (Silent μ₁ → Silent μ₂ → Silent μ₃) →
    (∀ {p p′ q} → p [ μ₁ ]⟶ p′ → Silent μ₂ → F p q [ μ₃ ]⟶ F p′ q) →
    (∀ {p q q′} → Silent μ₁ → q [ μ₂ ]⟶ q′ → F p q [ μ₃ ]⟶ F p q′) →
    (∀ {p p′ q q′} →
     p [ μ₁ ]⟶ p′ → q [ μ₂ ]⟶ q′ → F p q [ μ₃ ]⟶ F p′ q′) →
    ∀ {p p′ q q′} → p [ μ₁ ]⟶̂ p′ → q [ μ₂ ]⟶̂ q′ → F p q [ μ₃ ]⟶̂ F p′ q′
  zip-⟶̂ s f g h (done s₁)   (done s₂)   = done (s s₁ s₂)
  zip-⟶̂ s f g h (done s₁)   (step q⟶q′) = step (g s₁ q⟶q′)
  zip-⟶̂ s f g h (step p⟶p′) (done s₂)   = step (f p⟶p′ s₂)
  zip-⟶̂ s f g h (step p⟶p′) (step q⟶q′) = step (h p⟶p′ q⟶q′)

-- Transforms an LTS into one which uses weak transitions as
-- transitions.

weak : ∀ {ℓ} → LTS ℓ → LTS ℓ
weak lts = record
  { Proc      = Proc
  ; Label     = Label
  ; _[_]⟶_    = _[_]⇒̂_
  ; is-silent = is-silent
  }
  where
  open LTS lts

-- If no lts action is silent, then weak lts is equal to lts (assuming
-- extensionality and univalence).

weak≡id :
  ∀ {ℓ} →
  Extensionality ℓ (lsuc ℓ) →
  Univalence ℓ →
  (lts : LTS ℓ) →
  (∀ μ → ¬ LTS.Silent lts μ) →
  weak lts ≡ lts
weak≡id ext univ lts ¬silent =
  cong (λ _[_]⟶_ → record
          { Proc      = Proc
          ; Label     = Label
          ; _[_]⟶_    = _[_]⟶_
          ; is-silent = is-silent
          })
       (apply-ext ext λ p → apply-ext ext λ μ → apply-ext ext λ q →
          p [ μ ]⇒̂ q  ≡⟨ ≃⇒≡ univ $ ↔⇒≃ $ inverse $ ⟶↔⇒̂ (lower-extensionality _ _ ext) ¬silent ⟩∎
          p [ μ ]⟶ q  ∎)
  where
  open LTS lts

-- An LTS with no processes or labels.

empty : LTS lzero
empty = record
  { Proc      = ⊥
  ; Label     = ⊥
  ; _[_]⟶_    = λ ()
  ; is-silent = λ ()
  }

-- An LTS with a single process, a single (non-silent) label, and a
-- single transition.

one-loop : LTS lzero
one-loop = record
  { Proc      = ⊤
  ; Label     = ⊤
  ; _[_]⟶_    = λ _ _ _ → ⊤
  ; is-silent = λ _ → false
  }

-- An LTS with two distinct, but bisimilar, processes. There are
-- transitions between the two processes.

two-bisimilar-processes : LTS lzero
two-bisimilar-processes = record
  { Proc      = Bool
  ; Label     = ⊤
  ; _[_]⟶_    = λ _ _ _ → ⊤
  ; is-silent = λ _ → false
  }

-- A parametrised LTS for which bisimilarity is logically equivalent
-- to equality.

bisimilarity⇔equality : ∀ {ℓ} → Type ℓ → LTS ℓ
bisimilarity⇔equality A = record
  { Proc      = A
  ; Label     = A
  ; _[_]⟶_    = λ p μ q → p ≡ μ × p ≡ q
  ; is-silent = λ _ → false
  }

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
{-
 following Johnstone's book "Stone Spaces" we define semilattices
 to be commutative monoids such that every element is idempotent.
 In particular, we take every semilattice to have a neutral element
 that is either the maximal or minimal element depending on whether
 we have a join or meet semilattice.
-}

{-# OPTIONS --safe #-}
module Cubical.Algebra.Semilattice.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommMonoid

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Relation.Binary
open import Cubical.Relation.Binary.Poset

open import Cubical.Reflection.RecordEquiv

open Iso

private
  variable
    ℓ ℓ' : Level

record IsSemilattice {A : Type ℓ} (ε : A) (_·_ : A → A → A) : Type ℓ where
  constructor issemilattice

  field
   isCommMonoid : IsCommMonoid ε _·_
   idem : (x : A) → x · x ≡ x

  open IsCommMonoid isCommMonoid public

unquoteDecl IsSemilatticeIsoΣ = declareRecordIsoΣ IsSemilatticeIsoΣ (quote IsSemilattice)

record SemilatticeStr (A : Type ℓ) : Type ℓ where
  constructor semilatticestr

  field
    ε        : A
    _·_      : A → A → A
    isSemilattice : IsSemilattice ε _·_

  infixl 7 _·_

  open IsSemilattice isSemilattice public

Semilattice : ∀ ℓ → Type (ℓ-suc ℓ)
Semilattice ℓ = TypeWithStr ℓ SemilatticeStr

semilattice : (A : Type ℓ) (ε : A) (_·_ : A → A → A) (h : IsSemilattice ε _·_) → Semilattice ℓ
semilattice A ε _·_ h = A , semilatticestr ε _·_ h

-- Easier to use constructors
makeIsSemilattice : {L : Type ℓ} {ε : L} {_·_ : L → L → L}
               (is-setL : isSet L)
               (assoc : (x y z : L) → x · (y · z) ≡ (x · y) · z)
               (rid : (x : L) → x · ε ≡ x)
               (lid : (x : L) → ε · x ≡ x)
               (comm : (x y : L) → x · y ≡ y · x)
               (idem : (x : L) → x · x ≡ x)
             → IsSemilattice ε _·_
IsSemilattice.isCommMonoid (makeIsSemilattice is-setL assoc rid lid comm idem) =
                                        makeIsCommMonoid is-setL assoc rid lid comm
IsSemilattice.idem (makeIsSemilattice is-setL assoc rid lid comm idem) = idem

makeSemilattice : {L : Type ℓ} (ε : L) (_·_ : L → L → L)
             (is-setL : isSet L)
             (assoc : (x y z : L) → x · (y · z) ≡ (x · y) · z)
             (rid : (x : L) → x · ε ≡ x)
             (lid : (x : L) → ε · x ≡ x)
             (comm : (x y : L) → x · y ≡ y · x)
             (idem : (x : L) → x · x ≡ x)
             → Semilattice ℓ
makeSemilattice ε _·_ is-setL assoc rid lid comm idem =
  semilattice _ ε _·_ (makeIsSemilattice is-setL assoc rid lid comm idem)

SemilatticeStr→MonoidStr : {A : Type ℓ} → SemilatticeStr A → MonoidStr A
SemilatticeStr→MonoidStr (semilatticestr _ _ H) =
                          monoidstr _ _ (H .IsSemilattice.isCommMonoid .IsCommMonoid.isMonoid)

Semilattice→Monoid : Semilattice ℓ → Monoid ℓ
Semilattice→Monoid (_ , semilatticestr _ _ H) =
                    _ , monoidstr _ _ (H .IsSemilattice.isCommMonoid .IsCommMonoid.isMonoid)

Semilattice→CommMonoid : Semilattice ℓ → CommMonoid ℓ
Semilattice→CommMonoid (_ , semilatticestr _ _ H) =
                        _ , commmonoidstr _ _ (H .IsSemilattice.isCommMonoid)

SemilatticeHom : (L : Semilattice ℓ) (M : Semilattice ℓ') → Type (ℓ-max ℓ ℓ')
SemilatticeHom L M = MonoidHom (Semilattice→Monoid L) (Semilattice→Monoid M)

IsSemilatticeEquiv : {A : Type ℓ} {B : Type ℓ'}
  (M : SemilatticeStr A) (e : A ≃ B) (N : SemilatticeStr B) → Type (ℓ-max ℓ ℓ')
IsSemilatticeEquiv M e N =
                   IsMonoidHom (SemilatticeStr→MonoidStr M) (e .fst) (SemilatticeStr→MonoidStr N)

SemilatticeEquiv : (M : Semilattice ℓ) (N : Semilattice ℓ') → Type (ℓ-max ℓ ℓ')
SemilatticeEquiv M N = Σ[ e ∈ (M .fst ≃ N .fst) ] IsSemilatticeEquiv (M .snd) e (N .snd)

isPropIsSemilattice : {L : Type ℓ} (ε : L) (_·_ : L → L → L)
             → isProp (IsSemilattice ε _·_)
isPropIsSemilattice ε _·_ (issemilattice LL LC) (issemilattice SL SC) =
  λ i → issemilattice (isPropIsCommMonoid _ _ LL SL i) (isPropIdem LC SC i)
  where
  isSetL : isSet _
  isSetL = LL .IsCommMonoid.isMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

  isPropIdem : isProp ((x : _) → x · x ≡ x)
  isPropIdem = isPropΠ λ _ → isSetL _ _

𝒮ᴰ-Semilattice : DUARel (𝒮-Univ ℓ) SemilatticeStr ℓ
𝒮ᴰ-Semilattice =
  𝒮ᴰ-Record (𝒮-Univ _) IsSemilatticeEquiv
    (fields:
      data[ ε ∣ autoDUARel _ _ ∣ presε ]
      data[ _·_ ∣ autoDUARel _ _ ∣ isHom ]
      prop[ isSemilattice ∣ (λ _ _ → isPropIsSemilattice _ _) ])
  where
  open SemilatticeStr
  open IsMonoidHom

SemilatticePath : (L K : Semilattice ℓ) → SemilatticeEquiv L K ≃ (L ≡ K)
SemilatticePath = ∫ 𝒮ᴰ-Semilattice .UARel.ua

-- TODO: decide if that's the right approach
module JoinSemilattice (L' : Semilattice ℓ) where
 private L = fst L'
 open SemilatticeStr (snd L') renaming (_·_ to _∨l_ ; ε to 1l)
 open CommMonoidTheory (Semilattice→CommMonoid L')

 _≤_ : L → L → Type ℓ
 x ≤ y = x ∨l y ≡ y

 infix 4 _≤_

 IndPoset : Poset ℓ ℓ
 fst IndPoset = L
 PosetStr._≤_ (snd IndPoset) = _≤_
 IsPoset.is-set (PosetStr.isPoset (snd IndPoset)) = is-set
 IsPoset.is-prop-valued (PosetStr.isPoset (snd IndPoset)) = λ _ _ → is-set _ _
 IsPoset.is-refl (PosetStr.isPoset (snd IndPoset)) = idem
 IsPoset.is-trans (PosetStr.isPoset (snd IndPoset)) = path
  where
  path : (a b c : L) → a ∨l b ≡ b → b ∨l c ≡ c → a ∨l c ≡ c
  path a b c a∨b≡b b∨c≡c = a ∨l c ≡⟨ cong (a ∨l_) (sym b∨c≡c) ⟩
                            a ∨l (b ∨l c) ≡⟨ assoc _ _ _ ⟩
                            (a ∨l b) ∨l c ≡⟨ cong (_∨l c) a∨b≡b ⟩
                            b ∨l c ≡⟨ b∨c≡c ⟩
                            c ∎
 IsPoset.is-antisym (PosetStr.isPoset (snd IndPoset)) =
   λ _ _ a∨b≡b b∨a≡a → sym b∨a≡a ∙∙ comm _ _ ∙∙ a∨b≡b

 ∨lIsMax : ∀ x y z → x ≤ z → y ≤ z → x ∨l y ≤ z
 ∨lIsMax x y z x≤z y≤z = cong ((x ∨l y) ∨l_) (sym (idem z)) ∙ commAssocSwap x y z z
                                                            ∙ cong₂ (_∨l_) x≤z y≤z
                                                            ∙ idem z

 ≤-∨Pres : ∀ x y u w → x ≤ y → u ≤ w → x ∨l u ≤ y ∨l w
 ≤-∨Pres x y u w x≤y u≤w = commAssocSwap x u y w ∙ cong₂ (_∨l_) x≤y u≤w

 ≤-∨LPres : ∀ x y z → x ≤ y → z ∨l x ≤ z ∨l y
 ≤-∨LPres x y z x≤y = ≤-∨Pres _ _ _ _ (idem z) x≤y

module MeetSemilattice (L' : Semilattice ℓ) where
 private L = fst L'
 open SemilatticeStr (snd L') renaming (_·_ to _∧l_ ; ε to 0l)
 open CommMonoidTheory (Semilattice→CommMonoid L')

 _≤_ : L → L → Type ℓ
 x ≤ y = x ∧l y ≡ x

 infix 4 _≤_

 IndPoset : Poset ℓ ℓ
 fst IndPoset = L
 PosetStr._≤_ (snd IndPoset) = _≤_
 IsPoset.is-set (PosetStr.isPoset (snd IndPoset)) = is-set
 IsPoset.is-prop-valued (PosetStr.isPoset (snd IndPoset)) = λ _ _ → is-set _ _
 IsPoset.is-refl (PosetStr.isPoset (snd IndPoset)) = idem
 IsPoset.is-trans (PosetStr.isPoset (snd IndPoset)) = path
  where
  path : (a b c : L) → a ∧l b ≡ a → b ∧l c ≡ b → a ∧l c ≡ a
  path a b c a∧b≡a b∧c≡b = a ∧l c ≡⟨ cong (_∧l c) (sym a∧b≡a) ⟩
                            (a ∧l b) ∧l c ≡⟨ sym (assoc _ _ _) ⟩
                            a ∧l (b ∧l c) ≡⟨ cong (a ∧l_) b∧c≡b ⟩
                            a ∧l b ≡⟨ a∧b≡a ⟩
                            a ∎
 IsPoset.is-antisym (PosetStr.isPoset (snd IndPoset)) =
   λ _ _ a∧b≡a b∧a≡b → sym a∧b≡a ∙∙ comm _ _ ∙∙ b∧a≡b

 ≤-∧LPres : ∀ x y z → x ≤ y → z ∧l x ≤ z ∧l y
 ≤-∧LPres x y z x≤y = commAssocSwap z x z y ∙∙ cong (_∧l (x ∧l y)) (idem z) ∙∙ cong (z ∧l_) x≤y

 ∧≤LCancel : ∀ x y → x ∧l y ≤ y
 ∧≤LCancel x y = sym (assoc _ _ _) ∙ cong (x ∧l_) (idem y)

 ∧≤RCancel : ∀ x y → x ∧l y ≤ x
 ∧≤RCancel x y = commAssocr x y x ∙ cong (_∧l y) (idem x)

 ∧lIsMin : ∀ x y z → z ≤ x → z ≤ y → z ≤ x ∧l y
 ∧lIsMin x y z z≤x z≤y = cong (_∧l (x ∧l y)) (sym (idem z)) ∙ commAssocSwap z z x y
                                                            ∙ cong₂ (_∧l_) z≤x z≤y
                                                            ∙ idem z

max_stars_repo_name: dolio/cubical

max_issues_repo_name: dolio/cubical

max_forks_repo_name: dolio/cubical


text:
-- Reported by Nils Anders Danielsson in Issue #3960.

open import Agda.Builtin.Unit
open import Agda.Primitive

id : ∀ {a} (A : Set a) → A → A
id _ a = a

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

postulate
  P : ∀ {a} {A : Set a} → A → A → Set a

Q : ∀ {ℓ} → Set ℓ → Set ℓ
Q A = {x y : A} → P x y

postulate
  F : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
  f : ∀ {a b} {A : Set a} {B : Set b} → Q A → Q (F A B)

g : ∀ {a} (A : Set a) → Q A → ⊤
g A q = apply (λ {_ _} → f q) (id (Q (F A A) → ⊤) _)

-- The previous error message was:
--
-- Cannot instantiate the metavariable _47 to solution
-- piSort _49 (λ z → Set (a ⊔ _b_54 (A = A) (q = q)))
-- since it contains the variable a
-- which is not in scope of the metavariable or irrelevant in the metavariable but relevant in the solution
-- when checking that the expression λ {_} → f q has type
-- {_ = z : _50} → P (_x_59 (A = A) (q = q)) (_y_60 (A = A) (q = q))

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Binary.Raw.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function using (_∘_; _$_; flip; id)

open import Cubical.Relation.Binary.Base
open import Cubical.Relation.Binary.Raw.Definitions

open import Cubical.Relation.Nullary.Decidable

open import Cubical.Data.Maybe using (just; nothing; Dec→Maybe; map-Maybe)
open import Cubical.Data.Sum.Base as Sum using (inl; inr)
open import Cubical.Data.Prod.Base using (_,_)
open import Cubical.Data.Empty using (⊥; isProp⊥) renaming (elim to ⊥-elim)
open import Cubical.HITs.PropositionalTruncation

private
  variable
    a b ℓ ℓ₁ ℓ₂ ℓ₃ p : Level
    A : Type a
    B : Type b

------------------------------------------------------------------------
-- Equality properties

≡Reflexive : Reflexive (Path A)
≡Reflexive = refl

≡Symmetric : Symmetric (Path A)
≡Symmetric = sym

≡Transitive : Transitive (Path A)
≡Transitive = _∙_

≡Substitutive : Substitutive (Path A) ℓ
≡Substitutive P = subst P

------------------------------------------------------------------------
-- Implication properties

⇒-refl : Reflexive (_⇒_ {A = A} {B = A} {ℓ = ℓ})
⇒-refl = id

⇒-trans : Trans (_⇒_ {A = A} {B = B} {ℓ = ℓ₁} {ℓ′ = ℓ₂}) (_⇒_ {ℓ′ = ℓ₃}) _⇒_ -- Transitive _⇒_
⇒-trans f g x = g (f x)

------------------------------------------------------------------------
-- Substitutive properties

module _ (_∼_ : RawRel A ℓ₁) (P : RawRel A p) where

  subst→respˡ : Substitutive _∼_ p → P Respectsˡ _∼_
  subst→respˡ subst {y} x′∼x Px′y = subst (flip P y) x′∼x Px′y

  subst→respʳ : Substitutive _∼_ p → P Respectsʳ _∼_
  subst→respʳ subst {x} y′∼y Pxy′ = subst (P x) y′∼y Pxy′

  subst→resp₂ : Substitutive _∼_ p → P Respects₂ _∼_
  subst→resp₂ subst = subst→respʳ subst , subst→respˡ subst

module _ (_∼_ : RawRel A ℓ) (P : A → Type p) where

  P-resp→¬P-resp : Symmetric _∼_ → P Respects _∼_ → (¬_ ∘ P) Respects _∼_
  P-resp→¬P-resp sym resp x∼y ¬Px Py = ¬Px (resp (sym x∼y) Py)

Respectsʳ≡ : (_∼_ : RawRel A ℓ) → _∼_ Respectsʳ _≡_
Respectsʳ≡ _∼_ = subst→respʳ _≡_ _∼_ ≡Substitutive

Respectsˡ≡ : (_∼_ : RawRel A ℓ) → _∼_ Respectsˡ _≡_
Respectsˡ≡ _∼_ = subst→respˡ _≡_ _∼_ ≡Substitutive

Respects₂≡ : (_∼_ : RawRel A ℓ) → _∼_ Respects₂ _≡_
Respects₂≡ _∼_ = subst→resp₂ _≡_ _∼_ ≡Substitutive

------------------------------------------------------------------------
-- Proofs for non-strict orders

module _ (_≤_ : RawRel A ℓ) where

  total→FromEq : Total _≤_ → FromEq _≤_
  total→FromEq total {x} {y} x≡y with total x y
  ... | inl x∼y = x∼y
  ... | inr y∼x = Respectsʳ≡ _≤_ x≡y (Respectsˡ≡ _≤_ (sym x≡y) y∼x)

  total∧dec→dec : FromEq _≤_ → Antisymmetric _≤_ →
                  Total _≤_ → Discrete A → Decidable _≤_
  total∧dec→dec reflx antisym total _≟_ x y with total x y
  ... | inl x≤y = yes x≤y
  ... | inr y≤x = mapDec reflx (flip antisym y≤x) (x ≟ y)
    where
      mapDec : ∀ {A : Type a} {B : Type b} → (A → B) → (B → A) → Dec A → Dec B
      mapDec f g (yes x) = yes (f x)
      mapDec f g (no ¬x) = no (¬x ∘ g)

------------------------------------------------------------------------
-- Proofs for strict orders

module _ (_<_ : RawRel A ℓ) where

  trans∧irr→asym : Transitive _<_ → Irreflexive _<_ → Asymmetric _<_
  trans∧irr→asym transitive irrefl x<y y<x = irrefl (transitive x<y y<x)

  irr∧antisym→asym : Irreflexive _<_ → Antisymmetric _<_ → Asymmetric _<_
  irr∧antisym→asym irrefl antisym x<y y<x = irrefl→tonoteq irrefl x<y (antisym x<y y<x)
    where
      irrefl→tonoteq : Irreflexive _<_ → ToNotEq _<_
      irrefl→tonoteq irrefl {x} {y} x<y x≡y = irrefl (subst (λ z → x < z) (sym x≡y) x<y)

  asym→antisym : Asymmetric _<_ → Antisymmetric _<_
  asym→antisym asym x<y y<x = ⊥-elim (asym x<y y<x)

  asym→irr : Asymmetric _<_ → Irreflexive _<_
  asym→irr asym {x} x<x = asym x<x x<x

  tri→asym : Trichotomous _<_ → Asymmetric _<_
  tri→asym compare {x} {y} x<y x>y with compare x y
  ... | tri< _   _ x≯y = x≯y x>y
  ... | tri≡ _   _ x≯y = x≯y x>y
  ... | tri> x≮y _ _   = x≮y x<y

  tri→irr : Trichotomous _<_ → Irreflexive _<_
  tri→irr compare {x} x<x with compare x x
  ... | tri< _ _ x≮x = x≮x x<x
  ... | tri≡ _ _ x≮x = x≮x x<x
  ... | tri> x≮x _ _ = x≮x x<x

  tri→dec≡ : Trichotomous _<_ → Discrete A
  tri→dec≡ compare x y with compare x y
  ... | tri< _ x≢y _ = no  x≢y
  ... | tri≡ _ x≡y _ = yes x≡y
  ... | tri> _ x≢y _ = no  x≢y

  tri→dec< : Trichotomous _<_ → Decidable _<_
  tri→dec< compare x y with compare x y
  ... | tri< x<y _ _ = yes x<y
  ... | tri≡ x≮y _ _ = no  x≮y
  ... | tri> x≮y _ _ = no  x≮y

------------------------------------------------------------------------
-- Without Loss of Generality

module _ {_R_ : RawRel A ℓ₁} {Q : RawRel A ℓ₂} where

  wlog : Total _R_ → Symmetric Q →
         (∀ a b → a R b → Q a b) →
         ∀ a b → Q a b
  wlog r-total q-sym prf a b with r-total a b
  ... | inl aRb = prf a b aRb
  ... | inr bRa = q-sym (prf b a bRa)

------------------------------------------------------------------------
-- Other proofs

module _ {P : RawREL A B p} where

  dec→weaklyDec : Decidable P → WeaklyDecidable P
  dec→weaklyDec dec x y = Dec→Maybe (dec x y)

module _ {P : RawRel A ℓ₁} {Q : RawRel A ℓ₂} (f : P ⇒ Q) where

  map-Reflexive : Reflexive P → Reflexive Q
  map-Reflexive reflx = f reflx

  map-FromEq : FromEq P → FromEq Q
  map-FromEq fromEq p = f (fromEq p)

  cmap-Irreflexive : Irreflexive Q → Irreflexive P
  cmap-Irreflexive irrefl x≡x = irrefl (f x≡x)

  cmap-ToNotEq : ToNotEq Q → ToNotEq P
  cmap-ToNotEq toNotEq x = toNotEq (f x)

module _ {P : RawREL A B ℓ₁} {Q : RawREL A B ℓ₂} (f : P ⇒ Q) where

  map-Universal : Universal P → Universal Q
  map-Universal u x y = f (u x y)

  map-NonEmpty : NonEmpty P → NonEmpty Q
  map-NonEmpty = map (λ (x , p) → (x , map (λ (y , q) → y , f q) p) )

module _ {P : RawREL A B ℓ₁} {Q : RawREL B A ℓ₂} where

  flip-Connex : Connex P Q → Connex Q P
  flip-Connex f x y = Sum.swap (f y x)

module _ (_∼_ : RawRel A ℓ) where

  reflx→fromeq : Reflexive _∼_ → FromEq _∼_
  reflx→fromeq reflx {x} = J (λ z _ → x ∼ z) reflx

  fromeq→reflx : FromEq _∼_ → Reflexive _∼_
  fromeq→reflx fromEq = fromEq refl

  irrefl→tonoteq : Irreflexive _∼_ → ToNotEq _∼_
  irrefl→tonoteq irrefl {x} {y} x<y x≡y = irrefl (subst (λ z → x ∼ z) (sym x≡y) x<y)

  tonoteq→irrefl : ToNotEq _∼_ → Irreflexive _∼_
  tonoteq→irrefl toNotEq x<x = toNotEq x<x refl


text:
module examplesPaperJFP.VariableList where

open import Data.Product hiding (map)
open import Data.List

open import NativeIO
open import StateSizedIO.GUI.WxBindingsFFI
open import Relation.Binary.PropositionalEquality

data VarList : Set₁ where
  []      :  VarList
  addVar  :  (A : Set) → Var A → VarList → VarList

prod : VarList → Set
prod  []               =  Unit
prod  (addVar A v [])  =  A
prod  (addVar A v l)   =  A × prod l

takeVar : (l : VarList) → NativeIO (prod l)
takeVar  []                            = nativeReturn unit
takeVar (addVar A v [])                = nativeTakeVar {A} v
takeVar (addVar A v (addVar B v′ l))   =
  nativeTakeVar {A} v       native>>= λ a →
  takeVar (addVar B v′ l)   native>>= λ rest →
  nativeReturn ( a , rest )

putVar : (l : VarList) → prod l → NativeIO Unit
putVar  [] _                                     = nativeReturn unit
putVar  (addVar A v []) a                        = nativePutVar {A} v a
putVar  (addVar A v (addVar B v′ l)) (a , rest)  =
  nativePutVar {A} v a          native>>= λ _ →
  putVar (addVar B v′ l)  rest

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
{-# OPTIONS --cubical #-}
module _ where
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Bool

data S¹ : Set where
  base : S¹
  loop : base ≡ base

-- We cannot allow this definition as
--   decideEq (loop i)  base ↦ false
-- but
--   decideEq (loop i0) base ↦ true

decideEq : ∀ (x y : S¹) → Bool
decideEq base     base     = true
decideEq (loop i) (loop j) = true
decideEq x        y        = false

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2012-06-01, issue reported by fredrik.forsberg
module Issue661 where

import Common.Level

data Top : Set where
  tt : Top

mutual
  data Ctxt  : Set1 where
    [] : Ctxt
    cons : (G : Ctxt) -> (Env G -> Set) -> Ctxt

  Env : Ctxt -> Set --only important that Env x doesn't reduce for x neutral
  Env [] = Top
  Env (cons G A) = Top

module M (dummy : Set1) where

  data Uni (G : Ctxt) : Set1 where
    empty : Uni G
    sig : (A : Env G -> Set) -> Uni (cons G A) -> Uni G

open M Set

-- This example needs special constructor application checking
-- which propagates the parameters in.

c : Uni []
c = sig (\ _ -> Top) (sig (\ { tt -> Top}) empty)

-- Types:
-- empty : Uni _18
-- sig   : (A : Env _15 → Set) → Uni (cons _15 A) → Uni _15

--  c = sig (\ _ → Top) ?2  with ?2 : Uni (cons [] (λ _ → Top))
--  ?2 := sig ?3 ?4  with
--  ?3 : Env (cons [] (λ _ → Top)) → Set
--  ?4 : Uni (cons (cons [] (λ _ → Top)) ?3)

-- Error was:
-- Type mismatch
-- when checking that the pattern tt has type Env _14


text:
module FunSetPerBool where

data Bool : Set where
  True : Bool
  False : Bool

data T : Set where
  E : T

s : Bool -> Set
s True = Bool
s False = T

f = \ (x : s True) -> x
g = f True
f2 = \ (x : Bool) (y : s x) -> y
h = f2 False E
-- i : (xx : _) -> _
i = f2 True
j : (eh : s False) -> s False
j = f2 False

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
module Luau.Syntax.FromJSON where

open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; function⟨_⟩_end; local_←_; function_⟨_⟩_end; return; done; _∙_)

open import Agda.Builtin.List using (List; _∷_; [])

open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; fromString; lookup)
open import FFI.Data.Bool using (true; false)
open import FFI.Data.Either using (Either; Left; Right)
open import FFI.Data.Maybe using (Maybe; nothing; just)
open import FFI.Data.String using (String; _++_)
open import FFI.Data.Vector using (head; tail; null; empty)

args = fromString "args"
body = fromString "body"
func = fromString "func"
lokal = fromString "local"
list = fromString "list"
name = fromString "name"
type = fromString "type"
values = fromString "values"
vars = fromString "vars"

data Lookup : Set where
  _,_ : String → Value → Lookup
  nil : Lookup

lookupIn : List String → Object → Lookup
lookupIn [] obj = nil
lookupIn (key ∷ keys) obj with lookup (fromString key) obj
lookupIn (key ∷ keys) obj | nothing = lookupIn keys obj
lookupIn (key ∷ keys) obj | just value = (key , value)

exprFromJSON : Value → Either String Expr
exprFromObject : Object → Either String Expr
statFromJSON : Value → Either String Stat
statFromObject : Object → Either String Stat
blockFromJSON : Value → Either String Block
blockFromArray : Array → Either String Block

exprFromJSON (object obj) = exprFromObject obj
exprFromJSON val = Left "AstExpr not an object"

exprFromObject obj with lookup type obj
exprFromObject obj | just (string "AstExprCall") with lookup func obj | lookup args obj
exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) with head arr
exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | just value2 with exprFromJSON value | exprFromJSON value2
exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | just value2 | Right fun | Right arg = Right (fun $ arg)
exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | just value2 | Left err | _ = Left err
exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | just value2 | _ | Left err = Left err
exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | nothing = Left ("AstExprCall empty args")
exprFromObject obj | just (string "AstExprCall") | just value | just _ = Left ("AstExprCall args not an array")
exprFromObject obj | just (string "AstExprCall") | nothing | _  = Left ("AstExprCall missing func")
exprFromObject obj | just (string "AstExprCall") | _ | nothing  = Left ("AstExprCall missing args")
exprFromObject obj | just (string "AstExprConstantNil") = Right nil
exprFromObject obj | just (string "AstExprFunction") with lookup args obj | lookup body obj
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value with head arr | blockFromJSON value
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | just (string x) | Right B = Right (function⟨ x ⟩ B end)
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | just _ | Right B = Left "AstExprFunction args not a string array"
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | nothing | Right B = Left "Unsupported AstExprFunction empty args"
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | _ | Left err = Left err
exprFromObject obj | just (string "AstExprFunction") | just _ | just _ = Left "AstExprFunction args not an array"
exprFromObject obj | just (string "AstExprFunction") | nothing | _ = Left "AstExprFunction missing args"
exprFromObject obj | just (string "AstExprFunction") | _ | nothing = Left "AstExprFunction missing body"
exprFromObject obj | just (string "AstExprLocal") with lookup lokal obj
exprFromObject obj | just (string "AstExprLocal") | just (string x) = Right (var x)
exprFromObject obj | just (string "AstExprLocal") | just (_) = Left "AstExprLocal local not a string"
exprFromObject obj | just (string "AstExprLocal") | nothing = Left "AstExprLocal missing local"
exprFromObject obj | just (string ty) = Left ("TODO: Unsupported AstExpr " ++ ty)
exprFromObject obj | just _ = Left "AstExpr type not a string"
exprFromObject obj | nothing = Left "AstExpr missing type"

{-# NON_TERMINATING #-}
statFromJSON (object obj) = statFromObject obj
statFromJSON _ = Left "AstStat not an object"

statFromObject obj with lookup type obj
statFromObject obj | just(string "AstStatLocal") with lookup vars obj | lookup values obj
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) with head(arr1) | head(arr2)
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | just(value) with exprFromJSON(value)
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | just(value) | Right M = Right (local x ← M)
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | just(value) | Left err = Left err
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | nothing = Left "AstStatLocal empty values"
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(_) | _ = Left "AstStatLocal vars not a string array"
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | nothing | _ = Left "AstStatLocal empty vars"
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(_) = Left "AstStatLocal values not an array"
statFromObject obj | just(string "AstStatLocal") | just(_) | just(_) = Left "AstStatLocal vars not an array"
statFromObject obj | just(string "AstStatLocal") | just(_) | nothing = Left "AstStatLocal missing values"
statFromObject obj | just(string "AstStatLocal") | nothing | _ = Left "AstStatLocal missing vars"
statFromObject obj | just(string "AstStatLocalFunction") with lookup name obj | lookup func obj
statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value with exprFromJSON value
statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value | Right (function⟨ x ⟩ B end) = Right (function f ⟨ x ⟩ B end)
statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value | Left err = Left err
statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ | Right _ = Left "AstStatLocalFunction func is not an AstExprFunction"
statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ =  Left "AstStatLocalFunction name is not a string"
statFromObject obj | just(string "AstStatLocalFunction") | nothing | _ = Left "AstStatFunction missing name"
statFromObject obj | just(string "AstStatLocalFunction") | _ | nothing = Left "AstStatFunction missing func"
statFromObject obj | just(string "AstStatReturn") with lookup list obj
statFromObject obj | just(string "AstStatReturn") | just(array arr) with head arr
statFromObject obj | just(string "AstStatReturn") | just(array arr) | just value with exprFromJSON value
statFromObject obj | just(string "AstStatReturn") | just(array arr) | just value | Right M = Right (return M)
statFromObject obj | just(string "AstStatReturn") | just(array arr) | just value | Left err = Left err
statFromObject obj | just(string "AstStatReturn") | just(array arr) | nothing = Left "AstStatReturn empty list"
statFromObject obj | just(string "AstStatReturn") | just(_) = Left "AstStatReturn list not an array"
statFromObject obj | just(string "AstStatReturn") | nothing = Left "AstStatReturn missing list"
statFromObject obj | just (string ty) = Left ("TODO: Unsupported AstStat " ++ ty)
statFromObject obj | just _ = Left "AstStat type not a string"
statFromObject obj | nothing = Left "AstStat missing type"

blockFromJSON (array arr) = blockFromArray arr
blockFromJSON (object obj) with lookup type obj | lookup body obj
blockFromJSON (object obj) | just (string "AstStatBlock") | just value = blockFromJSON value
blockFromJSON (object obj) | just (string "AstStatBlock") | nothing = Left "AstStatBlock missing body"
blockFromJSON (object obj) | just (string ty) | _ = Left ("Unsupported AstBlock " ++ ty)
blockFromJSON (object obj) | just _ | _ = Left "AstStatBlock type not a string"
blockFromJSON (object obj) | nothing | _ = Left "AstStatBlock missing type"
blockFromJSON _ = Left "AstBlock not an array or AstStatBlock object"

blockFromArray arr with head arr
blockFromArray arr | nothing = Right done
blockFromArray arr | just value with statFromJSON value
blockFromArray arr | just value | Left err = Left err
blockFromArray arr | just value | Right S with blockFromArray(tail arr)
blockFromArray arr | just value | Right S | Left err = Left (err)
blockFromArray arr | just value | Right S | Right B  = Right (S ∙ B)

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


text:
module BeforeSpaces where

import BehindSpaces


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

open import Categories.Category

module Categories.Yoneda.Continuous {o ℓ e} (C : Category o ℓ e) where

open import Function.Equality using (Π)
open import Relation.Binary using (Setoid)

open import Categories.Category.Construction.Cones
open import Categories.Category.Construction.Presheaves
open import Categories.Diagram.Cone.Properties
open import Categories.Diagram.Limit
open import Categories.Functor
open import Categories.Functor.Limits
open import Categories.Functor.Hom
open import Categories.Functor.Hom.Properties C
open import Categories.NaturalTransformation
open import Categories.Yoneda

import Categories.Morphism.Reasoning as MR

open Hom C
open Yoneda C
open Π using (_⟨$⟩_)

private
  module C = Category C

module _ {o′ ℓ′ e′} {J : Category o′ ℓ′ e′} {F : Functor J C} (L : Limit F) where
  private
    module J = Category J
    module F = Functor F
    module L = Limit L
    open C.HomReasoning
    open MR C

    yF = embed ∘F F

    ⊤ : Cone yF
    ⊤ = F-map-Coneˡ embed L.limit

    HomL : ∀ X → Limit (Hom[ X ,-] ∘F F)
    HomL X = hom-resp-limit X L
    module HomL X = Limit (HomL X)

    module _ {K : Cone yF} where
      private
        module K where
          open Cone _ K public
          module N   = Functor N
          module ψ j = NaturalTransformation (ψ j)

      KHF : ∀ X → Cone (Hom[ X ,-] ∘F F)
      KHF X = record
        { N    = K.N.₀ X
        ; apex = record
          { ψ       = λ j → K.ψ.η j X
          ; commute = λ f eq → C.∘-resp-≈ʳ C.identityʳ ○ K.commute f eq
          }
        }

      ! : Cones yF [ K , ⊤ ]
      ! = record
        { arr     = ntHelper record
          { η       = λ X → Cone⇒.arr (HomL.terminal.! X {KHF X})
          ; commute = λ {X Y} f {x y} eq → L.terminal.!-unique record
            { arr     = C.id C.∘ L.rep _ C.∘ f
            ; commute = λ {j} → begin
              L.proj j C.∘ C.id C.∘ L.rep _ C.∘ f ≈⟨ refl⟩∘⟨ C.identityˡ ⟩
              L.proj j C.∘ L.rep _ C.∘ f          ≈⟨ pullˡ L.commute ⟩
              (K.ψ.η j X ⟨$⟩ y) C.∘ f             ≈˘⟨ C.identityˡ ⟩
              C.id C.∘ (K.ψ.η j X ⟨$⟩ y) C.∘ f    ≈˘⟨ K.ψ.commute j f eq ⟩
              K.ψ.η j Y ⟨$⟩ (K.N.₁ f ⟨$⟩ x)       ∎
            }
          }
        ; commute = λ eq → L.commute ○ Π.cong (K.ψ.η _ _) eq
        }

      module _ (f : Cones yF [ K , ⊤ ]) where
        private
          module f where
            open Cone⇒ _ f public
            module arr = NaturalTransformation arr

        !-unique : Cones yF [ ! ≈ f ]
        !-unique {X} {x} {y} eq = L.terminal.!-unique record
          { arr     = f.arr.η X ⟨$⟩ y
          ; commute = f.commute (Setoid.sym (K.N.₀ X) eq)
          }

  embed-resp-limit : Limit yF
  embed-resp-limit = record
    { terminal = record
      { ⊤             = ⊤
      ; ⊤-is-terminal = record
        { !        = !
        ; !-unique = !-unique
        }
      }
    }

embed-Continous : ∀ o′ ℓ′ e′ → Continuous o′ ℓ′ e′ embed
embed-Continous _ _ _ L = terminal.⊤-is-terminal
  where open Limit (embed-resp-limit L)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories