text:
------------------------------------------------------------------------
-- Total recognisers which can handle left recursion
------------------------------------------------------------------------

-- The recognisers are parametrised on the alphabet.

module TotalRecognisers.LeftRecursion (Tok : Set) where

open import Algebra
open import Codata.Musical.Notation
open import Data.Bool as Bool hiding (_∧_; _≤_)
import Data.Bool.Properties as Bool
private
  module BoolCS = CommutativeSemiring Bool.∧-∨-commutativeSemiring
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Eq
  using (_⇔_; equivalence; module Equivalence)
  renaming (_∘_ to _⟨∘⟩_)
open import Data.List using (List; []; _∷_; _++_; [_])
import Data.List.Properties
private
  module ListMonoid {A : Set} =
    Monoid (Data.List.Properties.++-monoid A)
open import Data.Product as Prod
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary
open import Relation.Nullary.Decidable as Decidable

------------------------------------------------------------------------
-- A "right-strict" variant of _∧_

-- If the left-strict variant of _∧_ were used to type _·_ below, then
-- the inferred definition of D-nullable would not be total; it would
-- contain expressions of the form "D-nullable t (♭ p₁) ∧ false". With
-- the right-strict definition of _∧_ such expressions reduce to
-- "false".

infixr 6 _∧_

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

-- A lemma.

left-zero : ∀ b → false ∧ b ≡ false
left-zero true  = refl
left-zero false = refl

------------------------------------------------------------------------
-- Recogniser combinators

infixl 10 _·_
infixl  5 _∣_

mutual

  -- The index is true if the corresponding language contains the empty
  -- string (is nullable).

  data P : Bool → Set where
    fail     : P false
    empty    : P true
    sat      : (Tok → Bool) → P false
    _∣_      : ∀ {n₁ n₂} →        P n₁ →        P n₂ → P (n₁ ∨ n₂)
    _·_      : ∀ {n₁ n₂} → ∞⟨ n₂ ⟩P n₁ → ∞⟨ n₁ ⟩P n₂ → P (n₁ ∧ n₂)
    nonempty : ∀ {n} → P n → P false
    cast     : ∀ {n₁ n₂} → n₁ ≡ n₂ → P n₁ → P n₂

  -- Delayed if the index is /false/.

  ∞⟨_⟩P : Bool → Bool → Set
  ∞⟨ false ⟩P n = ∞ (P n)
  ∞⟨ true  ⟩P n =    P n

-- Note that fail, nonempty and cast could be defined as derived
-- combinators. (For cast this is obvious, fail could be defined
-- either using sat or the combinator leftRight below, and nonempty is
-- defined in the module AlternativeNonempty. Note also that the proof
-- in TotalRecognisers.LeftRecursion.ExpressiveStrength does not rely
-- on these constructors.) However, Agda uses /guarded/ corecursion,
-- so the fact that nonempty and cast are constructors can be very
-- convenient when constructing other recognisers.

-- For an example of the use of nonempty, see the Kleene star example
-- in TotalRecognisers.LeftRecursion.Lib. For examples of the use of
-- cast, see TotalRecognisers.LeftRecursion.ExpressiveStrength and
-- TotalRecognisers.LeftRecursion.NotOnlyContextFree.

------------------------------------------------------------------------
-- Helpers

♭? : ∀ {b n} → ∞⟨ b ⟩P n → P n
♭? {b = false} x = ♭ x
♭? {b = true}  x =   x

♯? : ∀ {b n} → P n → ∞⟨ b ⟩P n
♯? {b = false} x = ♯ x
♯? {b = true}  x =   x

forced? : ∀ {b n} → ∞⟨ b ⟩P n → Bool
forced? {b = b} _ = b

-- A lemma.

♭?♯? : ∀ b {n} {p : P n} → ♭? {b} (♯? p) ≡ p
♭?♯? false = refl
♭?♯? true  = refl

------------------------------------------------------------------------
-- Semantics

-- The semantics is defined inductively: s ∈ p iff the string s is
-- contained in the language defined by p.

infix 4 _∈_

data _∈_ : ∀ {n} → List Tok → P n → Set where
  empty    : [] ∈ empty
  sat      : ∀ {f t} → T (f t) → [ t ] ∈ sat f
  ∣-left   : ∀ {s n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
             s ∈ p₁ → s ∈ p₁ ∣ p₂
  ∣-right  : ∀ {s n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
             s ∈ p₂ → s ∈ p₁ ∣ p₂
  _·_      : ∀ {s₁ s₂ n₁ n₂}
               {p₁ : ∞⟨ n₂ ⟩P n₁} {p₂ : ∞⟨ n₁ ⟩P n₂} →
             s₁ ∈ ♭? p₁ → s₂ ∈ ♭? p₂ → s₁ ++ s₂ ∈ p₁ · p₂
  nonempty : ∀ {n t s} {p : P n} →
             t ∷ s ∈ p → t ∷ s ∈ nonempty p
  cast     : ∀ {n₁ n₂ s} {p : P n₁} {eq : n₁ ≡ n₂} →
             s ∈ p → s ∈ cast eq p

infix 4 _≤_ _≈_

-- p₁ ≤ p₂ iff the language (defined by) p₂ contains all the strings
-- in the language p₁.

_≤_ : ∀ {n₁ n₂} → P n₁ → P n₂ → Set
p₁ ≤ p₂ = ∀ {s} → s ∈ p₁ → s ∈ p₂

-- p₁ ≈ p₂ iff the languages p₁ and p₂ contain the same strings.

_≈_ : ∀ {n₁ n₂} → P n₁ → P n₂ → Set
p₁ ≈ p₂ = ∀ {s} → s ∈ p₁ ⇔ s ∈ p₂

-- p₁ ≈ p₂ iff both p₁ ≤ p₂ and p₂ ≤ p₁.

≈⇔≤≥ : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
       p₁ ≈ p₂ ⇔ (p₁ ≤ p₂ × p₂ ≤ p₁)
≈⇔≤≥ = equivalence
         (λ p₁≈p₂  → ((λ {s} → _⟨$⟩_ (Equivalence.to   (p₁≈p₂ {s = s})))
                     , λ {s} → _⟨$⟩_ (Equivalence.from (p₁≈p₂ {s = s}))))
         (λ p₁≤≥p₂ {s} → equivalence (proj₁ p₁≤≥p₂ {s = s})
                                     (proj₂ p₁≤≥p₂ {s = s}))

-- Some lemmas.

cast∈ : ∀ {n} {p p′ : P n} {s s′} → s ≡ s′ → p ≡ p′ → s ∈ p → s′ ∈ p′
cast∈ refl refl s∈ = s∈

drop-♭♯ : ∀ n {n′} {p : P n′} → ♭? (♯? {n} p) ≤ p
drop-♭♯ n = cast∈ refl (♭?♯? n)

add-♭♯ : ∀ n {n′} {p : P n′} → p ≤ ♭? (♯? {n} p)
add-♭♯ n = cast∈ refl (sym $ ♭?♯? n)

------------------------------------------------------------------------
-- Example: A definition which is left and right recursive

leftRight : P false
leftRight = ♯ leftRight · ♯ leftRight

-- Note that leftRight is equivalent to fail, so fail does not need to
-- be a primitive combinator.

leftRight≈fail : leftRight ≈ fail
leftRight≈fail = equivalence ≤fail (λ ())
  where
  ≤fail : ∀ {s A} → s ∈ leftRight → A
  ≤fail (∈₁ · ∈₂) = ≤fail ∈₁

-- For more examples, see TotalRecognisers.LeftRecursion.Lib.

------------------------------------------------------------------------
-- Nullability

-- The nullability index is correct.

⇒ : ∀ {n} {p : P n} → [] ∈ p → n ≡ true
⇒ pr = ⇒′ pr refl
  where
  ⇒′ : ∀ {n s} {p : P n} → s ∈ p → s ≡ [] → n ≡ true
  ⇒′ empty                   refl = refl
  ⇒′ (sat _)                 ()
  ⇒′ (∣-left            pr₁) refl with ⇒ pr₁
  ⇒′ (∣-left            pr₁) refl | refl = refl
  ⇒′ (∣-right           pr₂) refl with ⇒ pr₂
  ⇒′ (∣-right {n₁ = n₁} pr₂) refl | refl = proj₂ BoolCS.zero n₁
  ⇒′ (nonempty p)            ()
  ⇒′ (cast {eq = refl} p)    refl = ⇒′ p refl
  ⇒′ (_·_ {[]}    pr₁ pr₂)   refl = cong₂ _∧_ (⇒ pr₁) (⇒ pr₂)
  ⇒′ (_·_ {_ ∷ _} pr₁ pr₂)   ()

⇐ : ∀ {n} (p : P n) → n ≡ true → [] ∈ p
⇐ fail                        ()
⇐ empty                       refl = empty
⇐ (sat f)                     ()
⇐ (_∣_ {true}          p₁ p₂) refl = ∣-left            (⇐ p₁ refl)
⇐ (_∣_ {false} {true}  p₁ p₂) refl = ∣-right {p₁ = p₁} (⇐ p₂ refl)
⇐ (_∣_ {false} {false} p₁ p₂) ()
⇐ (nonempty p)                ()
⇐ (cast refl p)               refl = cast (⇐ p refl)
⇐ (_·_ {.true} {true}  p₁ p₂) refl = ⇐ p₁ refl · ⇐ p₂ refl
⇐ (_·_ {_}     {false} p₁ p₂) ()

index-correct : ∀ {n} {p : P n} → [] ∈ p ⇔ n ≡ true
index-correct = equivalence ⇒ (⇐ _)

-- We can decide if the empty string belongs to a given language.

nullable? : ∀ {n} (p : P n) → Dec ([] ∈ p)
nullable? {n} p = Decidable.map (Eq.sym index-correct) (Bool._≟_ n true)

------------------------------------------------------------------------
-- Derivative

-- The index of the derivative.

D-nullable : ∀ {n} → Tok → P n → Bool
D-nullable t fail         = false
D-nullable t empty        = false
D-nullable t (sat f)      = f t
D-nullable t (p₁ ∣ p₂)    = D-nullable t p₁ ∨ D-nullable t p₂
D-nullable t (nonempty p) = D-nullable t p
D-nullable t (cast _ p)   = D-nullable t p
D-nullable t (p₁ · p₂)    with forced? p₁ | forced? p₂
... | true  | false = D-nullable t p₁
... | false | false = false
... | true  | true  = D-nullable t p₁ ∨ D-nullable t p₂
... | false | true  = D-nullable t p₂

-- D t p is the "derivative" of p with respect to t. It is specified
-- by the equivalence s ∈ D t p ⇔ t ∷ s ∈ p (proved below).

D : ∀ {n} (t : Tok) (p : P n) → P (D-nullable t p)
D t fail         = fail
D t empty        = fail
D t (sat f)      with f t
...              | true  = empty
...              | false = fail
D t (p₁ ∣ p₂)    = D t p₁ ∣ D t p₂
D t (nonempty p) = D t p
D t (cast _ p)   = D t p
D t (p₁ · p₂)    with forced? p₁ | forced? p₂
... | true  | false =   D t    p₁  · ♯? (♭ p₂)
... | false | false = ♯ D t (♭ p₁) · ♯? (♭ p₂)
... | true  | true  =   D t    p₁  · ♯?    p₂ ∣ D t p₂
... | false | true  = ♯ D t (♭ p₁) · ♯?    p₂ ∣ D t p₂

-- D is correct.

D-sound : ∀ {n s t} {p : P n} → s ∈ D t p → t ∷ s ∈ p
D-sound s∈ = D-sound′ _ _ s∈
  where
  sat-lemma : ∀ {s} f t → s ∈ D t (sat f) → T (f t) × s ≡ []
  sat-lemma f t ∈ with f t
  sat-lemma f t empty | true  = (_ , refl)
  sat-lemma f t ()    | false

  D-sound′ : ∀ {s n} (p : P n) t → s ∈ D t p → t ∷ s ∈ p
  D-sound′ fail         t ()
  D-sound′ empty        t ()
  D-sound′ (sat f)      t s∈                  with sat-lemma f t s∈
  ...                                         | (ok , refl) = sat ok
  D-sound′ (p₁ ∣ p₂)    t (∣-left  ∈₁)        = ∣-left (D-sound′ p₁ t ∈₁)
  D-sound′ (p₁ ∣ p₂)    t (∣-right ∈₂)        = ∣-right {p₁ = p₁} (D-sound′ p₂ t ∈₂)
  D-sound′ (nonempty p) t ∈                   = nonempty (D-sound ∈)
  D-sound′ (cast _ p)   t ∈                   = cast (D-sound ∈)
  D-sound′ (p₁ · p₂)    t s∈                  with forced? p₁ | forced? p₂
  D-sound′ (p₁ · p₂)    t (∣-left  (∈₁ · ∈₂)) | true  | true  = D-sound ∈₁ · drop-♭♯ (D-nullable t p₁) ∈₂
  D-sound′ (p₁ · p₂)    t (∣-right ∈₂)        | true  | true  = ⇐ p₁ refl · D-sound′ p₂ t ∈₂
  D-sound′ (p₁ · p₂)    t (∣-left  (∈₁ · ∈₂)) | false | true  = D-sound ∈₁ · drop-♭♯ (D-nullable t (♭ p₁)) ∈₂
  D-sound′ (p₁ · p₂)    t (∣-right ∈₂)        | false | true  = ⇐ (♭ p₁) refl · D-sound′ p₂ t ∈₂
  D-sound′ (p₁ · p₂)    t (∈₁ · ∈₂)           | true  | false = D-sound ∈₁ · drop-♭♯ (D-nullable t    p₁ ) ∈₂
  D-sound′ (p₁ · p₂)    t (∈₁ · ∈₂)           | false | false = D-sound ∈₁ · drop-♭♯ (D-nullable t (♭ p₁)) ∈₂

D-complete : ∀ {n s t} {p : P n} → t ∷ s ∈ p → s ∈ D t p
D-complete {t = t} t∷s∈ = D-complete′ _ t∷s∈ refl
  where
  D-complete′ : ∀ {s s′ n} (p : P n) → s′ ∈ p → s′ ≡ t ∷ s → s ∈ D t p
  D-complete′ fail         ()                   refl
  D-complete′ empty        ()                   refl
  D-complete′ (sat f)      (sat ok)             refl with f t
  D-complete′ (sat f)      (sat ok)             refl | true  = empty
  D-complete′ (sat f)      (sat ())             refl | false
  D-complete′ (p₁ ∣ p₂)    (∣-left  ∈₁)         refl = ∣-left                (D-complete ∈₁)
  D-complete′ (p₁ ∣ p₂)    (∣-right ∈₂)         refl = ∣-right {p₁ = D t p₁} (D-complete ∈₂)
  D-complete′ (nonempty p) (nonempty ∈)         refl = D-complete ∈
  D-complete′ (cast _ p)   (cast ∈)             refl = D-complete ∈
  D-complete′ (p₁ · p₂)    _                    _    with forced? p₁ | forced? p₂
  D-complete′ (p₁ · p₂)    (_·_ {[]}     ∈₁ ∈₂) refl | true  | true  = ∣-right {p₁ = D t p₁ · _} (D-complete ∈₂)
  D-complete′ (p₁ · p₂)    (_·_ {._ ∷ _} ∈₁ ∈₂) refl | true  | true  = ∣-left (D-complete ∈₁ · add-♭♯ (D-nullable t p₁) ∈₂)
  D-complete′ (p₁ · p₂)    (_·_ {[]}     ∈₁ ∈₂) refl | true  | false with ⇒ ∈₁
  D-complete′ (p₁ · p₂)    (_·_ {[]}     ∈₁ ∈₂) refl | true  | false | ()
  D-complete′ (p₁ · p₂)    (_·_ {._ ∷ _} ∈₁ ∈₂) refl | true  | false = D-complete ∈₁ · add-♭♯ (D-nullable t p₁) ∈₂
  D-complete′ (p₁ · p₂)    (_·_ {[]}     ∈₁ ∈₂) refl | false | true  = ∣-right {p₁ = _·_ {n₂ = false} _ _} (D-complete ∈₂)
  D-complete′ (p₁ · p₂)    (_·_ {._ ∷ _} ∈₁ ∈₂) refl | false | true  = ∣-left (D-complete ∈₁ · add-♭♯ (D-nullable t (♭ p₁)) ∈₂)
  D-complete′ (p₁ · p₂)    (_·_ {[]}     ∈₁ ∈₂) refl | false | false with ⇒ ∈₁
  D-complete′ (p₁ · p₂)    (_·_ {[]}     ∈₁ ∈₂) refl | false | false | ()
  D-complete′ (p₁ · p₂)    (_·_ {._ ∷ _} ∈₁ ∈₂) refl | false | false = D-complete ∈₁ · add-♭♯ (D-nullable t (♭ p₁)) ∈₂

D-correct : ∀ {n s t} {p : P n} → s ∈ D t p ⇔ t ∷ s ∈ p
D-correct = equivalence D-sound D-complete

------------------------------------------------------------------------
-- _∈_ is decidable

-- _∈?_ runs a recogniser. Note that the result is yes or no plus a
-- /proof/ verifying that the answer is correct.

infix 4 _∈?_

_∈?_ : ∀ {n} (s : List Tok) (p : P n) → Dec (s ∈ p)
[]    ∈? p = nullable? p
t ∷ s ∈? p with s ∈? D t p
t ∷ s ∈? p | yes s∈Dtp = yes (D-sound s∈Dtp)
t ∷ s ∈? p | no  s∉Dtp = no  (s∉Dtp ∘ D-complete)

-- The last three lines could be replaced by the following one:
--
-- t ∷ s ∈? p = Decidable.map D-correct (s ∈? D t p)

------------------------------------------------------------------------
-- Alternative characterisation of equality

infix 5 _∷_
infix 4 _≈′_

-- Two recognisers/languages are equal if their nullability indices
-- are equal and all their derivatives are equal (coinductively). Note
-- that the elements of this type are bisimulations.

data _≈′_ {n₁ n₂} (p₁ : P n₁) (p₂ : P n₂) : Set where
  _∷_ : n₁ ≡ n₂ → (∀ t → ∞ (D t p₁ ≈′ D t p₂)) → p₁ ≈′ p₂

-- This definition is equivalent to the one above.

≈′-sound : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} → p₁ ≈′ p₂ → p₁ ≈ p₂
≈′-sound (refl ∷ rest) {[]}    = Eq.sym index-correct ⟨∘⟩ index-correct
≈′-sound (refl ∷ rest) {t ∷ s} =
  D-correct ⟨∘⟩ ≈′-sound (♭ (rest t)) ⟨∘⟩ Eq.sym D-correct

same-nullability : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
                   p₁ ≈ p₂ → n₁ ≡ n₂
same-nullability p₁≈p₂ =
  Bool.⇔→≡ (index-correct ⟨∘⟩ p₁≈p₂ ⟨∘⟩ Eq.sym index-correct)

D-cong : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} {t} →
         p₁ ≈ p₂ → D t p₁ ≈ D t p₂
D-cong p₁≈p₂ = Eq.sym D-correct ⟨∘⟩ p₁≈p₂ ⟨∘⟩ D-correct

≈′-complete : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} → p₁ ≈ p₂ → p₁ ≈′ p₂
≈′-complete p₁≈p₂ =
  same-nullability p₁≈p₂ ∷ λ _ → ♯ ≈′-complete (D-cong p₁≈p₂)

≈′-correct : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} → p₁ ≈′ p₂ ⇔ p₁ ≈ p₂
≈′-correct = equivalence ≈′-sound ≈′-complete

------------------------------------------------------------------------
-- The combinator nonempty does not need to be primitive

-- The variant of nonempty which is defined below (nonempty′) makes
-- many recognisers larger, though.

module AlternativeNonempty where

  nonempty′ : ∀ {n} → P n → P false
  nonempty′ fail         = fail
  nonempty′ empty        = fail
  nonempty′ (sat f)      = sat f
  nonempty′ (p₁ ∣ p₂)    = nonempty′ p₁ ∣ nonempty′ p₂
  nonempty′ (nonempty p) = nonempty′ p
  nonempty′ (cast eq p)  = nonempty′ p
  nonempty′ (p₁ · p₂)    with forced? p₁ | forced? p₂
  ... | false | _     = p₁ · p₂
  ... | true  | false = p₁ · p₂
  ... | true  | true  = nonempty′ p₁ ∣ nonempty′ p₂
                      ∣ ♯ nonempty′ p₁ · ♯ nonempty′ p₂

  sound : ∀ {n} {p : P n} → nonempty′ p ≤ nonempty p
  sound {s = []}    pr with ⇒ pr
  ... | ()
  sound {s = _ ∷ _} pr = nonempty (sound′ _ pr refl)
    where
    sound′ : ∀ {n t s s′} (p : P n) →
             s′ ∈ nonempty′ p → s′ ≡ t ∷ s → t ∷ s ∈ p
    sound′ fail         ()                              refl
    sound′ empty        ()                              refl
    sound′ (sat f)      (sat ok)                        refl = sat ok
    sound′ (p₁ ∣ p₂)    (∣-left  pr)                    refl = ∣-left            (sound′ p₁ pr refl)
    sound′ (p₁ ∣ p₂)    (∣-right pr)                    refl = ∣-right {p₁ = p₁} (sound′ p₂ pr refl)
    sound′ (nonempty p) pr                              refl = nonempty (sound′ p pr refl)
    sound′ (cast _ p)   pr                              refl = cast (sound′ p pr refl)
    sound′ (p₁ · p₂)    pr                              _    with forced? p₁ | forced? p₂
    sound′ (p₁ · p₂)    pr                              refl | false | _     = pr
    sound′ (p₁ · p₂)    pr                              refl | true  | false = pr
    sound′ (p₁ · p₂)    (∣-left (∣-left  pr))           refl | true  | true  = cast∈ (proj₂ ListMonoid.identity _) refl $
                                                                                sound′ p₁ pr refl · ⇐ p₂ refl
    sound′ (p₁ · p₂)    (∣-left (∣-right pr))           refl | true  | true  = ⇐ p₁ refl · sound′ p₂ pr refl
    sound′ (p₁ · p₂)    (∣-right (_·_ {[]}    pr₁ pr₂)) refl | true  | true  with ⇒ pr₁
    ... | ()
    sound′ (p₁ · p₂)    (∣-right (_·_ {_ ∷ _} pr₁ pr₂)) refl | true  | true  with sound {p = p₂} pr₂
    ... | nonempty pr₂′ = sound′ p₁ pr₁ refl · pr₂′

  complete : ∀ {n} {p : P n} → nonempty p ≤ nonempty′ p
  complete (nonempty pr) = complete′ _ pr refl
    where
    complete′ : ∀ {n t s s′} (p : P n) →
                s ∈ p → s ≡ t ∷ s′ → t ∷ s′ ∈ nonempty′ p
    complete′ fail         ()                            refl
    complete′ empty        ()                            refl
    complete′ (sat f)      (sat ok)                      refl = sat ok
    complete′ (p₁ ∣ p₂)    (∣-left pr)                   refl = ∣-left               (complete′ p₁ pr refl)
    complete′ (p₁ ∣ p₂)    (∣-right pr)                  refl = ∣-right {n₁ = false} (complete′ p₂ pr refl)
    complete′ (nonempty p) (nonempty pr)                 refl = complete′ p pr refl
    complete′ (cast _ p)   (cast pr)                     refl = complete′ p pr refl
    complete′ (p₁ · p₂)    pr                            _    with forced? p₁ | forced? p₂
    complete′ (p₁ · p₂)    pr                            refl | false | _     = pr
    complete′ (p₁ · p₂)    pr                            refl | true  | false = pr
    complete′ (p₁ · p₂)    (_·_ {[]}            pr₁ pr₂) refl | true  | true  = ∣-left (∣-right {n₁ = false} (complete′ p₂ pr₂ refl))
    complete′ (p₁ · p₂)    (_·_ {_ ∷ _} {[]}    pr₁ pr₂) refl | true  | true  = cast∈ (sym $ proj₂ ListMonoid.identity _) refl $
                                                                                ∣-left (∣-left {n₂ = false} (complete′ p₁ pr₁ refl))
    complete′ (p₁ · p₂)    (_·_ {_ ∷ _} {_ ∷ _} pr₁ pr₂) refl | true  | true  = ∣-right {n₁ = false} (complete′ p₁ pr₁ refl ·
                                                                                complete′ p₂ pr₂ refl)

  correct : ∀ {n} {p : P n} → nonempty′ p ≈ nonempty p
  correct = equivalence sound complete

max_stars_repo_name: nad/parser-combinators


text:
open import Formalization.PredicateLogic.Signature

module Formalization.PredicateLogic.Syntax (𝔏 : Signature) where
open Signature(𝔏)

open import Data.ListSized
import      Lvl
open import Functional using (_∘_ ; _∘₂_ ; swap)
open import Numeral.Finite
open import Numeral.Natural
open import Sets.PredicateSet using (PredSet)
open import Type

private variable ℓ : Lvl.Level
private variable args vars : ℕ

data Term (vars : ℕ) : Type{ℓₒ} where
  var  : 𝕟(vars) → Term(vars)                       -- Variables
  func : Obj(args) → List(Term(vars))(args) → Term(vars) -- Constants/functions

-- Formulas.
-- Inductive definition of the grammatical elements of the language of predicate logic.
data Formula : ℕ → Type{ℓₚ Lvl.⊔ ℓₒ} where
  _$_ : Prop(args) → List(Term(vars))(args) → Formula(vars) -- Relations

  ⊤ : Formula(vars) -- Tautology (Top / True)
  ⊥ : Formula(vars) -- Contradiction (Bottom / False)

  _∧_ : Formula(vars) → Formula(vars) → Formula(vars) -- Conjunction (And)
  _∨_ : Formula(vars) → Formula(vars) → Formula(vars) -- Disjunction (Or)
  _⟶_ : Formula(vars) → Formula(vars) → Formula(vars) -- Implication

  Ɐ : Formula(𝐒(vars)) → Formula(vars)
  ∃ : Formula(𝐒(vars)) → Formula(vars)

-- A sentence is a formula with no variables occurring.
Sentence = Formula(𝟎)

infix  1011 _$_
infixr 1005 _∧_
infixr 1004 _∨_
infixr 1000 _⟶_

-- Negation
¬_ : Formula(vars) → Formula(vars)
¬_ = _⟶ ⊥

-- Double negation
¬¬_ : Formula(vars) → Formula(vars)
¬¬_ = (¬_) ∘ (¬_)

-- Reverse implication
_⟵_ : Formula(vars) → Formula(vars) → Formula(vars)
_⟵_ = swap(_⟶_)

-- Equivalence
_⟷_ : Formula(vars) → Formula(vars) → Formula(vars)
p ⟷ q = (p ⟵ q) ∧ (p ⟶ q)

-- (Nor)
_⊽_ : Formula(vars) → Formula(vars) → Formula(vars)
_⊽_ = (¬_) ∘₂ (_∨_)

-- (Nand)
_⊼_ : Formula(vars) → Formula(vars) → Formula(vars)
_⊼_ = (¬_) ∘₂ (_∧_)

-- (Exclusive or / Xor)
_⊻_ : Formula(vars) → Formula(vars) → Formula(vars)
_⊻_ = (¬_) ∘₂ (_⟷_)

infix  1010 ¬_ ¬¬_
infixl 1000 _⟵_ _⟷_

Ɐ₊ : Formula(vars) → Sentence
Ɐ₊{𝟎}   φ = φ
Ɐ₊{𝐒 v} φ = Ɐ₊{v} (Ɐ φ)

∃₊ : Formula(vars) → Sentence
∃₊{𝟎}   φ = φ
∃₊{𝐒 v} φ = ∃₊{v} (∃ φ)

ext: agda

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-

  In order to solve the metavariables in this example
  we need to solve a constraint of the form

    _1 := unit₂ (_2 y)

  With the flex removal feature the occurs check will
  spot the bad variable 'y' in the instantiation and
  remove it by instantiating

    _2 := λ y → _3

  for a fresh metavariable _3. The instantiation of _1
  can then proceed.

-}
module FlexRemoval where

record Unit : Set where

data Unit₂ : Set where
 unit₂ : Unit → Unit₂

mutual

 data D : Set where
   c₁ : D
   c₂ : (x : Unit₂) → (Unit → D₂ x) → D

 D₂ : Unit₂ → Set
 D₂ (unit₂ x) = D

foo : D
foo = c₂ _ (λ y → c₁)

{- 2011-04-05 Andreas

This test case and the explanation is no longer up to date.
What happens is

  _2 y : Unit

is solved by eta-expansion

  _2 = λ y -> record {}

and then

  _1 = unit₂ (record {})

is in solved form.

-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import HoTT
open import cohomology.Theory

{- Cohomology groups of the n-torus (S¹)ⁿ.
 - We have Ĉᵏ(Tⁿ) == C⁰(S⁰)^(n choose' k) where _choose'_ defined as below.
 - This argument could give Cᵏ((Sᵐ)ⁿ) with a little more work. -}

module cohomology.Torus {i} (OT : OrdinaryTheory i) where

open OrdinaryTheory OT
open import cohomology.Sn OT
open import cohomology.SphereProduct cohomology-theory
open import cohomology.Unit cohomology-theory

{- Almost n choose k, but with n choose' O = 0 for any n. -}
_choose'_ : ℕ → ℤ → ℕ
n choose' (neg _) = 0
n choose' O = 0
n choose' pos O = n
O choose' (pos (S k)) = 0
S n choose' pos (S k) = (n choose' (pos k)) + (n choose' (pos (S k)))

_-⊙Torus : ℕ → Ptd i
O -⊙Torus = ⊙Lift ⊙Unit
(S n) -⊙Torus = (⊙Sphere {i} 1) ⊙× (n -⊙Torus)

C-nTorus : (k : ℤ) (n : ℕ)
  → C k (n -⊙Torus) == (C O (⊙Sphere 0)) ^ᴳ (n choose' k)

C-nTorus (neg k) O = C-Unit-is-trivial (neg k)

C-nTorus (neg k) (S n) =
  C-Sphere× (neg k) 1 (n -⊙Torus)
  ∙ ap (λ K → K ×ᴳ (C (neg k) (⊙Susp^ 1 (n -⊙Torus))
                    ×ᴳ C (neg k) (n -⊙Torus)))
       (C-Sphere-≠ (neg k) 1 (ℤ-neg≠pos _ _))
  ∙ ×ᴳ-unit-l {G = C (neg k) (⊙Susp (n -⊙Torus))
                   ×ᴳ C (neg k) (n -⊙Torus)}
  ∙ ap (λ K → C (neg k) (⊙Susp (n -⊙Torus)) ×ᴳ K)
        (C-nTorus (neg k) n)
  ∙ ×ᴳ-unit-r {G = C (neg k) (⊙Susp (n -⊙Torus))}
  ∙ C-Susp (neg (S k)) (n -⊙Torus)
  ∙ C-nTorus (neg (S k)) n

C-nTorus O O = C-Unit-is-trivial O

C-nTorus O (S n) =
  C-Sphere× O 1 (n -⊙Torus)
  ∙ ap (λ K → K ×ᴳ (C O (⊙Susp (n -⊙Torus)) ×ᴳ C O (n -⊙Torus)))
       (C-Sphere-≠ O 1 (ℤ-O≠pos _))
  ∙ ×ᴳ-unit-l {G = C O (⊙Susp (n -⊙Torus)) ×ᴳ C O (n -⊙Torus)}
  ∙ ap (λ K → C O (⊙Susp (n -⊙Torus)) ×ᴳ K)
       (C-nTorus O n)
  ∙ ×ᴳ-unit-r {G = C O (⊙Susp (n -⊙Torus))}
  ∙ C-Susp (neg O) (n -⊙Torus)
  ∙ C-nTorus (neg O) n

C-nTorus (pos O) O =
  C-Unit-is-trivial (pos O)

C-nTorus (pos O) (S n) =
  C-Sphere× (pos O) 1 (n -⊙Torus)
  ∙ ap (λ K → K ×ᴳ (C (pos O) (⊙Susp (n -⊙Torus))
                     ×ᴳ C (pos O) (n -⊙Torus)))
       (C-Sphere-diag 1)
  ∙ ap (λ K → C O (⊙Sphere O) ×ᴳ K)
       (ap2 _×ᴳ_
         (C-Susp O (n -⊙Torus) ∙ C-nTorus O n)
         (C-nTorus (pos O) n)
        ∙ ×ᴳ-unit-l {G = C O (⊙Sphere 0) ^ᴳ (n choose' pos O)})

C-nTorus (pos (S k)) O =
  C-Unit-is-trivial (pos (S k))

C-nTorus (pos (S k)) (S n) =
  C-Sphere× (pos (S k)) 1 (n -⊙Torus)
  ∙ ap (λ K → K ×ᴳ (C (pos (S k)) (⊙Susp (n -⊙Torus))
                     ×ᴳ C (pos (S k)) (n -⊙Torus)))
       (C-Sphere-≠ (pos (S k)) 1 (ℕ-S≠O k ∘ pos-injective (S k) 0))
  ∙ ×ᴳ-unit-l {G = (C (pos (S k)) (⊙Susp (n -⊙Torus))
                    ×ᴳ (C (pos (S k)) (n -⊙Torus)))}
  ∙ ap2 _×ᴳ_ (C-Susp (pos k) (n -⊙Torus) ∙ C-nTorus (pos k) n)
             (C-nTorus (pos (S k)) n)
  ∙ ^ᴳ-sum (C O (⊙Sphere 0)) (n choose' pos k) (n choose' pos (S k))

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
module Numeral.Natural.Function.GreatestCommonDivisor where

import Lvl
open import Data
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Logic.Propositional
open import Numeral.CoordinateVector as Vector using (Vector)
open import Numeral.Finite using (𝕟 ; 𝟎 ; 𝐒)
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.FlooredDivision
open import Numeral.Natural.Oper.Modulo
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Relation.Divisibility
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Classical
open import Type

-- TODO: Prove that gcd is the infimum in a lattice of ℕ with divisibility as its ordering

{-# TERMINATING #-}
gcdFold : ∀{ℓ}{T : Type{ℓ}} → ((a : ℕ) → (b : ℕ) → (a ≥ b) → (b > 𝟎) → T → T → T) → ((a : ℕ) → (b : ℕ) → (a < b) → (b > 𝟎) → T → T → T) → T → ℕ → ℕ → (ℕ ⨯ T)
gcdFold f g x (a)(𝟎) = (a , x)
gcdFold f g x (a)(𝐒(b)) with [≥]-or-[<] {a}{𝐒(b)}
... | [∨]-introₗ ab = Tuple.mapRight (f a (𝐒(b)) ab (succ min) x) (gcdFold f g x (𝐒(b))(a mod 𝐒(b)))
... | [∨]-introᵣ ba = Tuple.mapRight (g a (𝐒(b)) ba (succ min) x) (gcdFold f g x (𝐒(b))(a))

-- An algorithm for computing the greatest common divisor for two numbers.
-- Also called: Euclid's algorithm.
-- Termination: See `Gcd-existence` for a functionally equal variant of this function that passes the termination checker. It is equal in the sense that the same algorithm is used to construct the existence and to compute the value of this function. This is even more evident when looking at `Gcd-gcd`.
-- Alternative implementation:
--   gcd(a)(𝟎) = a
--   gcd(a)(𝐒(b)) with [≥]-or-[<] {a}{𝐒(b)}
--   ... | [∨]-introₗ _ = gcd(𝐒(b))(a mod 𝐒(b))
--   ... | [∨]-introᵣ _ = gcd(𝐒(b))(a)
gcd : ℕ → ℕ → ℕ
gcd a b = Tuple.left(gcdFold(\_ _ _ _ _ _ → <>) (\_ _ _ _ _ _ → <>) (<>{Lvl.𝟎}) a b)

lcm : ℕ → ℕ → ℕ
lcm(a)(b) = (a ⋅ b) ⌊/⌋₀ gcd(a)(b)

-- `Gcd a b D` is the specialization for 2 elements and states that `D` is a divisor of both `a` and `b`, and the greatest one of them.
-- Example:
--   Divisor(24) = {1,2,3,4,  6,8,   12,      24}
--   Divisor(60) = {1,2,3,4,5,6  ,10,12,15,20,   30,60}
--   24 = 2³ ⋅ 3¹
--   60 = 2² ⋅ 3¹ ⋅ 5¹
--   Gcd 24 60 = {max(Divisor(24) ∩ Divisor(60))} = 2² ⋅ 3¹ = 12
--   Divisor of first : 24 / 12 = 2
--   Divisor of second: 60 / 12 = 5
record GreatestCommonDivisor(n : ℕ) (v : Vector(n)(ℕ)) (D : ℕ) : Type{Lvl.𝟎} where
  constructor intro
  field
    divisor : ∀(i) → (D ∣ v(i))
    maximum : ∀{d} → (∀(i) → (d ∣ v(i))) → (d ∣ D)

Gcd = GreatestCommonDivisor(2) ∘₂ Vector.pair
module Gcd {a b D} where
  intro₂ : _ → _ → (∀{d} → _ → _ → (d ∣ D)) → Gcd a b D
  intro₂ divisorₗ divisorᵣ maximum = intro{2}{Vector.pair a b}
    (\{𝟎 → divisorₗ ; (𝐒(𝟎)) → divisorᵣ})
    (\dv → maximum (dv 𝟎) (dv (𝐒 𝟎)))
  module _ (inst : Gcd a b D) where
    open GreatestCommonDivisor(inst) public
    divisorₗ = divisor 𝟎
    divisorᵣ = divisor(𝐒 𝟎)
    maximum₂ = \{d} a b → maximum{d} \{𝟎 → a ; (𝐒(𝟎)) → b}

-- `Lcm a b M` is the specialization for 2 elements and states that `M` is a multiple of both `a` and `b`, and the smallest one of them.
-- Example:
--   360  = 2³ ⋅ 3² ⋅ 5¹
--   8400 = 2⁴ ⋅ 3¹ ⋅ 5² ⋅ 7¹
--   Lcm 360 8400 = {min(Multiple(360) ∩ Multiple(8400))} = 2⁴ ⋅ 3² ⋅ 5² ⋅ 7¹ = 25200
--   Multiple of first : 360 ⋅ 2¹ ⋅ 5¹ ⋅ 7¹ = 360 ⋅ 70 = 25200
--   Multiple of second: 8400 ⋅ 3¹ = 25200
record LeastCommonMultiple(n : ℕ) (v : Vector(n)(ℕ)) (M : ℕ) : Type{Lvl.𝟎} where
  constructor intro
  field
    multiple : ∀(i) → (v(i) ∣ M)
    minimum  : ∀{m} → (∀(i) → (v(i) ∣ m)) → (M ∣ m)

Lcm = LeastCommonMultiple(2) ∘₂ Vector.pair
module Lcm {a b M} where
  intro₂ : _ → _ → (∀{m} → _ → _ → (M ∣ m)) → Lcm a b M
  intro₂ multipleₗ multipleᵣ minimum = intro{2}{Vector.pair a b}
    (\{𝟎 → multipleₗ ; (𝐒(𝟎)) → multipleᵣ})
    (\dv → minimum (dv 𝟎) (dv (𝐒 𝟎)))
  module _ (inst : Lcm a b M) where
    open LeastCommonMultiple(inst) public
    multipleₗ = multiple 𝟎
    multipleᵣ = multiple(𝐒 𝟎)
    minimum₂ = \{m} a b → minimum{m} \{𝟎 → a ; (𝐒(𝟎)) → b}

open import Logic.Predicate
open import Numeral.Natural.Inductions
open import Numeral.Natural.Oper.Modulo.Proofs
open import Numeral.Natural.Relation.Divisibility.Proofs
open import Numeral.Natural.Relation.Divisibility.Proofs.Modulo
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Sets.PredicateSet using (_∈_ ; _⊆_)
open import Structure.Relator.Properties
open import Structure.Setoid.Uniqueness
open import Syntax.Function

private variable a b d : ℕ

Gcd-unique : Unique(Gcd a b)
Gcd-unique p q = antisymmetry(_∣_)(_≡_)
  (Gcd.maximum₂ q (Gcd.divisorₗ p) (Gcd.divisorᵣ p))
  (Gcd.maximum₂ p (Gcd.divisorₗ q) (Gcd.divisorᵣ q))

Gcd-base : (a ∈ Gcd(a)(𝟎))
Gcd-base = Gcd.intro₂
  divides-reflexivity
  Div𝟎
  const

Gcd-step : (a ≥ 𝐒(b)) → Gcd(a mod 𝐒(b))(𝐒(b)) ⊆ Gcd(a)(𝐒(b))
Gcd-step ab p = Gcd.intro₂
  ([↔]-to-[←] (divides-mod (Gcd.divisorᵣ p)) (Gcd.divisorₗ p))
  (Gcd.divisorᵣ p)
  (\da db → Gcd.maximum₂ p ([↔]-to-[→] (divides-mod db) da) db)

Gcd-swap : Gcd(a)(b) ⊆ Gcd(b)(a)
Gcd-swap p = Gcd.intro₂
  (Gcd.divisorᵣ p)
  (Gcd.divisorₗ p)
  (swap(Gcd.maximum₂ p))

-- Note: The construction for the existence is following the same steps as in the definition of the function `gcd`, but unlike `gcd` which does not pass the termination checker, this uses [ℕ]-strong-induction to pass it.
Gcd-existence : ∃(Gcd a b)
Gcd-existence{a}{b} = [ℕ]-strong-induction {φ = b ↦ ∀{a} → ∃(Gcd a b)} base step {b}{a} where
  base : ∀{a} → ∃(Gcd a 𝟎)
  base{a} = [∃]-intro a ⦃ Gcd-base ⦄

  step : ∀{i} → (∀{j} → (j ≤ i) → ∀{a} → ∃(Gcd a j)) → ∀{a} → ∃(Gcd a (𝐒(i)))
  step {i} prev {a} with [≥]-or-[<] {a}{𝐒(i)}
  ... | [∨]-introₗ ia = [∃]-map-proof (Gcd-step ia ∘ Gcd-swap) (prev{a mod 𝐒(i)} ([≤]-without-[𝐒] (mod-maxᵣ{a}{𝐒(i)})) {𝐒(i)})
  ... | [∨]-introᵣ (succ ai) = [∃]-map-proof Gcd-swap(prev {a} ai {𝐒(i)})

Gcd-gcdFold : ∀{a b}{ℓ}{T : Type{ℓ}}{f}{g}{x : T} → Gcd a b (Tuple.left(gcdFold f g x a b))
Gcd-gcdFold{a}{b}{f = f}{g}{x} = [ℕ]-strong-induction {φ = b ↦ ∀{a} → Gcd a b (Tuple.left(gcdFold f g x a b))} base step {b}{a} where
  base : ∀{a} → Gcd a 𝟎 (Tuple.left(gcdFold f g x a 𝟎))
  base{a} = Gcd-base

  step : ∀{i} → (∀{j} → (j ≤ i) → ∀{a} → Gcd a j (Tuple.left(gcdFold f g x a j))) → ∀{a} → Gcd a (𝐒(i)) (Tuple.left(gcdFold f g x a (𝐒(i))))
  step {i} prev {a} with [≥]-or-[<] {a}{𝐒(i)}
  ... | [∨]-introₗ ia = (Gcd-step ia ∘ Gcd-swap) (prev{a mod 𝐒(i)} ([≤]-without-[𝐒] (mod-maxᵣ{a}{𝐒(i)})) {𝐒(i)})
  ... | [∨]-introᵣ (succ ai) = Gcd-swap(prev {a} ai {𝐒(i)})

-- Usage: This allows the transferrence of proofs between `Gcd` and `gcd`. It is sometimes easier to prove properties by using `Gcd` first and then transfering them so that the proofs also hold for `gcd`.
Gcd-gcdFold-value : ∀{a b D}{ℓ}{T : Type{ℓ}}{f}{g}{x : T} → (Gcd a b D) ↔ (Tuple.left(gcdFold f g x a b) ≡ D)
Gcd-gcdFold-value = [↔]-intro (\{[≡]-intro → Gcd-gcdFold}) (Gcd-unique Gcd-gcdFold)

Gcd-gcd : Gcd a b (gcd a b)
Gcd-gcd = Gcd-gcdFold

Gcd-gcd-value : (Gcd a b d) ↔ (gcd a b ≡ d)
Gcd-gcd-value = Gcd-gcdFold-value


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

open import Fragment.Algebra.Signature

module Fragment.Algebra.Quotient (Σ : Signature) where

open import Fragment.Algebra.Algebra Σ
open import Fragment.Algebra.Homomorphism Σ
open import Fragment.Setoid.Morphism using (_↝_)

open import Level using (Level; Setω; _⊔_; suc)
open import Data.Vec.Properties using (map-id)
open import Relation.Binary using (Setoid; IsEquivalence; Rel)
import Relation.Binary.PropositionalEquality as PE

private
  variable
    a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level

module _
  (A : Algebra {a} {ℓ₁})
  (_≈_ : Rel ∥ A ∥ ℓ₂)
  where

  private
    setoid' : IsEquivalence _≈_ → Setoid _ _
    setoid' isEquivalence =
      record { Carrier       = ∥ A ∥
             ; _≈_           = _≈_
             ; isEquivalence = isEquivalence
             }

  record IsDenominator : Set (a ⊔ suc ℓ₁ ⊔ suc ℓ₂) where
    field
      isEquivalence : IsEquivalence _≈_
      isCoarser     : ∀ {x y} → x =[ A ] y → x ≈ y
      isCompatible  : Congruence (setoid' isEquivalence) (A ⟦_⟧_)

module _
  (A : Algebra {a} {ℓ₁})
  (_≈_ : Rel ∥ A ∥ ℓ₄)
  {{isDenom : IsDenominator A _≈_}}
  where

  record IsQuotient (A/≈ : Algebra {b} {ℓ₂}) : Setω where
    field
      inc : A ⟿ A/≈

      factor : ∀ {c ℓ₃} {X : Algebra {c} {ℓ₃}}
               → (f : A ⟿ X)
               → (Congruent _≈_ ≈[ X ] ∣ f ∣)
               → A/≈ ⟿ X

      commute : ∀ {c ℓ₃} {X : Algebra {c} {ℓ₃}}
               → (f : A ⟿ X)
               → (cong : Congruent _≈_ ≈[ X ] ∣ f ∣)
               → factor f cong ⊙ inc ≗ f

      universal : ∀ {c ℓ₃} {X : Algebra {c} {ℓ₃}}
                  → (f : A ⟿ X)
                  → (cong : Congruent _≈_ ≈[ X ] ∣ f ∣)
                  → {h : A/≈ ⟿ X}
                  → h ⊙ inc ≗ f
                  → factor f cong ≗ h

  open IsDenominator isDenom

  ∥_∥/_ : Setoid _ _
  ∥_∥/_ = record { Carrier       = ∥ A ∥
                 ; _≈_           = _≈_
                 ; isEquivalence = isEquivalence
                 }

  _/_-isAlgebra : IsAlgebra ∥_∥/_
  _/_-isAlgebra = record { ⟦_⟧     = A ⟦_⟧_
                         ; ⟦⟧-cong = isCompatible
                         }

  _/_ : Algebra
  _/_ = record { ∥_∥/≈           = ∥_∥/_
               ; ∥_∥/≈-isAlgebra = _/_-isAlgebra
               }

  private

    ∣inc∣⃗ : ∥ A ∥/≈ ↝ ∥_∥/_
    ∣inc∣⃗ = record { ∣_∣      = λ x → x
                    ; ∣_∣-cong = isCoarser
                    }

    ∣inc∣-hom : Homomorphic A _/_ (λ x → x)
    ∣inc∣-hom f xs =
      Setoid.reflexive ∥_∥/_ (PE.cong (A ⟦ f ⟧_) (map-id xs))

  inc : A ⟿ _/_
  inc = record { ∣_∣⃗    = ∣inc∣⃗
               ; ∣_∣-hom = ∣inc∣-hom
               }

  module _ {c ℓ₃}
    {X : Algebra {c} {ℓ₃}}
    (f : A ⟿ X)
    (cong : Congruent _≈_ ≈[ X ] ∣ f ∣)
    where

    private

      ∣factor∣⃗ : ∥_∥/_ ↝ ∥ X ∥/≈
      ∣factor∣⃗ = record { ∣_∣      = ∣ f ∣
                         ; ∣_∣-cong = cong
                         }

    factor : _/_ ⟿ X
    factor = record { ∣_∣⃗    = ∣factor∣⃗
                    ; ∣_∣-hom = ∣ f ∣-hom
                    }

    factor-commute : factor ⊙ inc ≗ f
    factor-commute = Setoid.refl ∥ X ∥/≈

    factor-universal : ∀ {h : _/_ ⟿ X} → h ⊙ inc ≗ f → factor ≗ h
    factor-universal p {x} = sym (p {x})
      where open Setoid ∥ X ∥/≈

  _/_-isQuotient : IsQuotient (_/_)
  _/_-isQuotient = record { inc       = inc
                          ; factor    = factor
                          ; commute   = factor-commute
                          ; universal = factor-universal
                          }

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
-- Non-index (plain) monads in form of Kleisli triple.

module Control.Monad where

open import Function using () renaming (_∘′_ to _∘_)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Axiom.FunctionExtensionality
open import Control.Functor

-- The operations of a monad.

module T-MonadOps (M : Set → Set) where

  T-return = ∀ {A}   (a : A)                 → M A
  T-bind   = ∀ {A B} (m : M A) (k : A → M B) → M B

record MonadOps (M : Set → Set) : Set₁ where
  open T-MonadOps M

  infixr 6 _>>=_

  field
    return : T-return
    _>>=_  : T-bind

  bind = _>>=_

  functorOps : FunctorOps M
  functorOps = record
    { map = λ f m → m >>= λ a → return (f a)
    }

  open FunctorOps functorOps public

-- The laws of a monad (Kleisli triple variant).

module T-MonadLaws {M : Set → Set} (ops : MonadOps M) where
  open MonadOps ops public

  T-bind-β = ∀ {A B} (k : A → M B) (a : A) →

      return a >>= k  ≡  k a

  T-bind-η = ∀ {A} (m : M A) →

      m >>= return  ≡  m

  T-bind-assoc = ∀ {A B C} (m : M A) {k : A → M B} {l : B → M C} →

      (m >>= k) >>= l  ≡  m >>= λ a → (k a >>= l)

  -- Provable laws.

  -- A variant of bind-β using function extensionality.

  T-bind-β-ext = ∀ {A B C : Set} (f : A → B) (k : B → M C) →

      (λ a → return (f a) >>= k)  ≡  k ∘ f

  T-map-after-bind = ∀ {A B C} (m : M A) {k : A → M B} {f : B → C} →

      f <$> (m >>= k)  ≡  m >>= λ a → f <$> k a

  T-bind-after-map = ∀ {A B C} (m : M A) {k : B → M C} {f : A → B} →

     (f <$> m) >>= k  ≡  m >>= λ a → k (f a)

record MonadLaws {M : Set → Set} (ops : MonadOps M) : Set₁ where
  open T-MonadLaws ops

  -- Axioms.

  field
    bind-β     : T-bind-β
    bind-η     : T-bind-η
    bind-assoc : T-bind-assoc

  -- Derived laws.

  bind-β-ext : T-bind-β-ext
  bind-β-ext f k = fun-ext (λ a → bind-β k (f a))

  map-after-bind : T-map-after-bind
  map-after-bind m = bind-assoc m

  -- A more detailed proof.  (NF: trans (bind-assoc m) refl)
  private
    map-after-bind′ : T-map-after-bind
    map-after-bind′ m {k = k} {f = f} = begin
        f <$> (m >>= k)
      ≡⟨⟩                                        -- definition of map
        ((m >>= k) >>= λ b → return (f b))
      ≡⟨ bind-assoc m ⟩                          -- associativity of bind
        m >>= (λ a → k a >>= λ b → return (f b))
      ≡⟨⟩                                        -- definition of map
        m >>= (λ a → f <$> k a)
      ∎

  bind-after-map : T-bind-after-map
  bind-after-map m {k = k} {f = f} = begin
      (f <$> m) >>= k
    ≡⟨⟩                                        -- definition of map
      (m >>= λ a → return (f a)) >>= k
    ≡⟨ bind-assoc m ⟩                          -- associativity of bind
      m >>= (λ a → return (f a) >>= k)
    ≡⟨ cong (_>>=_ m) (bind-β-ext _ _) ⟩       -- beta for bind
      m >>= (λ a → k (f a))
    ∎

  -- Functor laws.

  open T-FunctorLaws functorOps using (T-map-∘)

  private
    abstract
      map-comp : T-map-∘
      map-comp {f = f} {g = g} = fun-ext λ m → begin
          g ∘ f <$> m                                          ≡⟨⟩
          (m >>= λ a → return (g (f a)))                       ≡⟨ cong (_>>=_ m) (sym (bind-β-ext _ _)) ⟩
          (m >>= λ a → return (f a) >>= λ b → return (g b))    ≡⟨ sym (bind-assoc m) ⟩
          (m >>= λ a → return (f a)) >>= (λ b → return (g b))  ≡⟨⟩
          g <$> f <$> m
        ∎

  functorLaws : FunctorLaws functorOps
  functorLaws = record
    { map-id = fun-ext bind-η
    ; map-∘  = map-comp
    }

  open FunctorLaws functorLaws public

record IsMonad (M : Set → Set) : Set₁ where

  field
    ops  : MonadOps  M
    laws : MonadLaws ops

  open MonadOps  ops  public
  open MonadLaws laws public

{-

-- The operations of a monad.

record MonadOps (M : Set → Set) : Set₁ where

  infixr 6 _>>=_

  T-return = ∀ {A}   (a : A)                 → M A
  T-bind   = ∀ {A B} (m : M A) (k : A → M B) → M B

  field
    return : T-return
    _>>=_  : T-bind

  bind = _>>=_

  functorOps : FunctorOps M
  functorOps = record
    { _<$>_ = λ f m → m >>= λ a → return (f a)
    }

  open FunctorOps functorOps public

-- The laws of a monad (Kleisli triple variant).

record MonadLaws {M : Set → Set} (ops : MonadOps M) : Set₁ where

  open MonadOps ops

  T-bind-β = ∀ {A B} (a : A) (k : A → M B) →

      return a >>= k  ≡  k a

  T-bind-η = ∀ {A} (m : M A) →

      m >>= return  ≡  m

  T-bind-assoc = ∀ {A B C} (m : M A) {k : A → M B} {l : B → M C} →

      (m >>= k) >>= l  ≡  m >>= λ a → (k a >>= l)

  field
    bind-β     : T-bind-β
    bind-η     : T-bind-η
    bind-assoc : T-bind-assoc

  private
    abstract
      map-comp : FunctorLaws.T-map-∘ {!!}
      map-comp = {!!}

  functorLaws : FunctorLaws functorOps
  functorLaws = record
    { map-id = bind-η
    ; map-∘  = {!!}
    }

record IsMonad (M : Set → Set) : Set₁ where

record IsMonad (M : Set → Set) : Set₁ where

  infixr 6 _>>=_

  field
    return : ∀ {A}   (a : A)                 → M A
    _>>=_  : ∀ {A B} (m : M A) (k : A → M B) → M B

    -- Laws

    bind-β : ∀ {A B} (a : A) (k : A → M B) →

      return a >>= k  ≡  k a

    bind-η : ∀ {A} (m : M A) →

      m >>= return  ≡  m

    bind-assoc  : ∀ {A B C} (m : M A) {k : A → M B} {l : B → M C} →

      (m >>= k) >>= l  ≡  m >>= λ a → (k a >>= l)

  bind = _>>=_

  private
    map : Map-T F
    map = λ f m → m >>= λ a → return (f a)

    abstract
      map-comp : Map-Comp-T map

  functor : IsFunctor M
  functor = record
    { _<$>_  = λ f m → m >>= λ a → return (f a)
    ; map-id = bind-η
    ; map-∘  = map-comp
        where x = {!bind-assoc!}
    }
-}

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
module Issue278 where

abstract
  module A where
    Foo : Set₁
    Foo = Set
  module B where
    open A
    Foo≡Set : Foo ≡ Set
    Foo≡Set = refl


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

module Data.Nat.Show where

open import Prelude
open import Data.Nat
open import Data.Nat.DivMod
open import Data.String
open import Data.List

showDig : ℕ → Char
showDig 0 = '0'
showDig 1 = '1'
showDig 2 = '2'
showDig 3 = '3'
showDig 4 = '4'
showDig 5 = '5'
showDig 6 = '6'
showDig 7 = '7'
showDig 8 = '8'
showDig 9 = '9'
showDig _ = '!'

showsℕ : ℕ → List Char → List Char
showsℕ n xs = go xs n n
  where
  go : List Char → ℕ → ℕ → List Char
  go a zero      _       = a
  go a n@(suc _) (suc t) = go (showDig (rem n 10) ∷ a) (n ÷ 10) t
  go a (suc _)   zero    = a

showℕ : ℕ → String
showℕ n = pack (showsℕ n [])

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Data.List.Prefix where

open import Level
open import Data.Nat
open import Data.List
open import Data.List.At
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any hiding (map)
open import Data.List.Relation.Binary.Pointwise as P hiding (refl; map)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as ≡

-- prefix predicate for lists
infix 4 _⊑_
data _⊑_ {a} {A : Set a} : List A → List A → Set a where
  [] : ∀ {ys} → [] ⊑ ys
  _∷_ : ∀ x {xs ys} → xs ⊑ ys → x ∷ xs ⊑ x ∷ ys

⊑-refl : ∀ {a} {A : Set a} → Reflexive (_⊑_ {A = A})
⊑-refl {x = []} = []
⊑-refl {x = x ∷ xs} = x ∷ ⊑-refl

⊑-trans : ∀ {a} {A : Set a} → Transitive (_⊑_ {A = A})
⊑-trans [] _ = []
⊑-trans (x ∷ p) (.x ∷ q) = x ∷ ⊑-trans p q

open import Relation.Binary.PropositionalEquality

⊑-unique : ∀ {a}{A : Set a}{k l : List A}(xs ys : k ⊑ l) → xs ≡ ys
⊑-unique [] [] = refl
⊑-unique (x ∷ xs) (.x ∷ ys) = cong (λ u → x ∷ u) (⊑-unique xs ys)

⊑-trans-refl : ∀ {a}{A : Set a}{k l}{xs : k ⊑ l} → ⊑-trans {A = A} ⊑-refl xs ≡ xs
⊑-trans-refl {xs = []} = refl
⊑-trans-refl {xs = x ∷ xs} = cong (λ u → x ∷ u) ⊑-trans-refl

⊑-trans-refl' : ∀ {a}{A : Set a}{k l}{xs : k ⊑ l} → ⊑-trans {A = A} xs ⊑-refl ≡ xs
⊑-trans-refl' {xs = []} = refl
⊑-trans-refl' {xs = x ∷ xs} = cong (λ u → x ∷ u) ⊑-trans-refl'

⊑-trans-assoc : ∀ {a}{A : Set a}{k l m n : List A}{p : k ⊑ l}{q : l ⊑ m}{r : m ⊑ n} →
                ⊑-trans p (⊑-trans q r) ≡ ⊑-trans (⊑-trans p q) r
⊑-trans-assoc {p = []} {q} = refl
⊑-trans-assoc {p = x ∷ p} {.x ∷ q} {.x ∷ r} = cong (λ u → x ∷ u) ⊑-trans-assoc

remainder : ∀ {a}{A : Set a}{xs ys : List A} → xs ⊑ ys → List A
remainder ([] {ys}) = ys
remainder (x ∷ xs) = remainder xs

-- list extensions; reverse prefix relation
infix 4 _⊒_
_⊒_ : ∀ {a} {A : Set a} → List A → List A → Set a
xs ⊒ ys = ys ⊑ xs

-- appending to a list gives a list extension;
-- or, appending to a list makes the original a prefix
∷ʳ-⊒ : ∀ {a} {A : Set a} (x : A) xs → xs ∷ʳ x ⊒ xs
∷ʳ-⊒ x [] = []
∷ʳ-⊒ x (x₁ ∷ Σ₁) = x₁ ∷ (∷ʳ-⊒ x Σ₁)

-- indexes into a prefix point to the same element in extensions
xs⊒ys[i] : ∀ {a} {A : Set a} {xs : List A} {ys : List A} {i y} →
           xs [ i ]= y → (p : ys ⊒ xs) → ys [ i ]= y
xs⊒ys[i] () []
xs⊒ys[i] {i = zero} p (x ∷ a) = p
xs⊒ys[i] {i = suc i} p (x ∷ a) = xs⊒ys[i] p a

-- prefix is preserved by map
⊑-map : ∀ {a b} {A : Set a} {B : Set b} {xs ys : List A} {f : A → B} →
        xs ⊑ ys → map f xs ⊑ map f ys
⊑-map [] = []
⊑-map {f = f} (x ∷ p) = f x ∷ (⊑-map p)

-- all elemens in a list, also exist in it's extensions
∈-⊒ : ∀ {a}{A : Set a}{xs : List A}{x} → x ∈ xs → ∀ {ys} → ys ⊒ xs → x ∈ ys
∈-⊒ () []
∈-⊒ (here px) (x ∷ q) = here px
∈-⊒ (there p) (x ∷ q) = there (∈-⊒ p q)

∈-⊒-refl : ∀ {a}{A : Set a}{xs : List A}{x}{p : x ∈ xs} → ∈-⊒ p ⊑-refl ≡ p
∈-⊒-refl {p = here px} = refl
∈-⊒-refl {p = there p} = cong there ∈-⊒-refl

∈-⊒-trans : ∀ {a}{A : Set a}{xs ys zs : List A}{x}{p : x ∈ xs}(q : ys ⊒ xs)(r : zs ⊒ ys) → ∈-⊒ p (⊑-trans q r) ≡ ∈-⊒ (∈-⊒ p q) r
∈-⊒-trans {p = here px} (x ∷ l) (.x ∷ r) = refl
∈-⊒-trans {p = there p} (x ∷ l) (.x ∷ r) = cong there (∈-⊒-trans l r)

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

module Decidable {a}{A : Set a}(_≟_ : Decidable (_≡_ {A = A})) where

  _⊑?_ : Decidable (_⊑_ {A = A})
  [] ⊑? _ = yes []
  (x ∷ xs) ⊑? [] = no (λ ())
  (x ∷ xs) ⊑? (y ∷ ys) with x ≟ y
  (x ∷ xs) ⊑? (y ∷ ys) | no ¬p = no (λ{ (.x ∷ z) → ¬p refl })
  (x ∷ xs) ⊑? (.x ∷ ys) | yes refl with xs ⊑? ys
  ... | yes px = yes (x ∷ px)
  ... | no ¬px = no (λ{ (.x ∷ px) → ¬px px})

  _⊒?_ : Decidable (_⊒_ {A = A})
  xs ⊒? ys = ys ⊑? xs

import Relation.Binary.PropositionalEquality.Core as PC
⊑-preorder : ∀ {ℓ}{A : Set ℓ} → Preorder ℓ ℓ ℓ
⊑-preorder {A = A} = record {
  Carrier = List A ; _≈_ = _≡_ ; _∼_ = _⊑_ ;
  isPreorder = record {
    isEquivalence = ≡.isEquivalence ;
    reflexive = λ{ refl → ⊑-refl } ; trans = ⊑-trans } }

⊒-preorder : ∀ {ℓ}{A : Set ℓ} → Preorder _ _ _
⊒-preorder {A = A} = record {
  Carrier = List A ; _≈_ = _≡_ ; _∼_ = _⊒_ ;
  isPreorder = record {
    isEquivalence = ≡.isEquivalence ;
    reflexive = λ{ refl → ⊑-refl } ; trans = λ p q → ⊑-trans q p } }


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

open import Types
open import Functions
open import Paths
open import HLevel
open import Equivalences
open import Univalence
open import Funext

module HLevelBis where

abstract
  -- Every map between contractible types is an equivalence
  contr-to-contr-is-equiv : ∀ {i j} {A : Set i} {B : Set j} (f : A → B)
    → (is-contr A → is-contr B → is-equiv f)
  contr-to-contr-is-equiv f cA cB y =
    ((π₁ cA , (contr-has-all-paths cB _ _))
    , (λ _ → Σ-eq (contr-has-all-paths cA _ _)
                        (contr-has-all-paths (≡-is-truncated _ cB) _ _)))

  is-contr-is-prop : ∀ {i} {A : Set i} → is-prop (is-contr A)
  is-contr-is-prop {A = A} = all-paths-is-prop
    (λ x y → Σ-eq (π₂ y (π₁ x))
                        (funext (lemma x y (π₂ y (π₁ x))))) where

    lemma : (x y : is-contr A) (p : π₁ x ≡ π₁ y) (t : A)
      → transport (λ v → (z : A) → z ≡ v) p (π₂ x) t ≡ π₂ y t
    lemma (x , p) (.x , q) refl t = contr-has-all-paths
                                    (≡-is-truncated _ (x , p)) _ _

  -- Equivalent types have the same truncation level
  equiv-types-truncated : ∀ {i j} {A : Set i} {B : Set j} (n : ℕ₋₂) (f : A ≃ B)
    → (is-truncated n A → is-truncated n B)
  equiv-types-truncated ⟨-2⟩ (f , e) (x , p) =
    (f x , (λ y → ! (inverse-right-inverse (f , e) y) ∘ ap f (p _)))
  equiv-types-truncated (S n) f c = λ x y →
    equiv-types-truncated n (equiv-ap (f ⁻¹) x y ⁻¹) (c (f ⁻¹ ☆ x) (f ⁻¹ ☆ y))

  Π-is-truncated : ∀ {i j} (n : ℕ₋₂) {A : Set i} {P : A → Set j}
    → (((x : A) → is-truncated n (P x)) → is-truncated n (Π A P))
  Π-is-truncated ⟨-2⟩ p =
    ((λ x → π₁ (p x)) , (λ f → funext (λ x → π₂ (p x) (f x))))
  Π-is-truncated (S n) p = λ f g →
    equiv-types-truncated n funext-equiv
      (Π-is-truncated n (λ x → p x (f x) (g x)))

  →-is-truncated : ∀ {i j} (n : ℕ₋₂) {A : Set i} {B : Set j}
    → (is-truncated n B → is-truncated n (A → B))
  →-is-truncated n p = Π-is-truncated n (λ _ → p)

  is-truncated-is-prop : ∀ {i} (n : ℕ₋₂) {A : Set i}
    → is-prop (is-truncated n A)
  is-truncated-is-prop ⟨-2⟩ = is-contr-is-prop
  is-truncated-is-prop (S n) =
    Π-is-truncated _ (λ x → Π-is-truncated _ (λ y → is-truncated-is-prop n))

  is-set-is-prop : ∀ {i} {A : Set i} → is-prop (is-set A)
  is-set-is-prop = is-truncated-is-prop ⟨0⟩

  Σ-is-truncated : ∀ {i j} (n : ℕ₋₂) {A : Set i} {P : A → Set j}
    → (is-truncated n A → ((x : A) → is-truncated n (P x))
      → is-truncated n (Σ A P))
  Σ-is-truncated ⟨-2⟩ p q = ((π₁ p , (π₁ (q (π₁ p)))) ,
                       (λ y → Σ-eq (π₂ p _) (π₂ (q _) _)))
  Σ-is-truncated (S n) p q =
    λ x y → equiv-types-truncated n total-Σ-eq-equiv
                               (Σ-is-truncated n (p _ _) (λ _ → q _ _ _))

  ×-is-truncated : ∀ {i j} (n : ℕ₋₂) {A : Set i} {B : Set j}
    → (is-truncated n A → is-truncated n B → is-truncated n (A × B))
  ×-is-truncated n pA pB = Σ-is-truncated n pA (λ x → pB)

  subtype-truncated-S-is-truncated-S : ∀ {i j} (n : ℕ₋₂)
    {A : Set i} {P : A → Set j}
    → (is-truncated (S n) A → ((x : A) → is-prop (P x))
      → is-truncated (S n) (Σ A P))
  subtype-truncated-S-is-truncated-S n p q =
    Σ-is-truncated (S n) p (λ x → prop-is-truncated-S n (q x))

  is-equiv-is-prop : ∀ {i j} {A : Set i} {B : Set j} (f : A → B)
    → is-prop (is-equiv f)
  is-equiv-is-prop f = Π-is-truncated _ (λ x → is-contr-is-prop)

-- Specilization
module _ where
  Π-is-prop : ∀ {i j} {A : Set i} {P : A → Set j}
    → (((x : A) → is-prop (P x)) → is-prop (Π A P))
  Π-is-prop = Π-is-truncated ⟨-1⟩

  Π-is-set : ∀ {i j} {A : Set i} {P : A → Set j}
    → (((x : A) → is-set (P x)) → is-set (Π A P))
  Π-is-set = Π-is-truncated ⟨0⟩

  →-is-set : ∀ {i j} {A : Set i} {B : Set j}
    → (is-set B → is-set (A → B))
  →-is-set = →-is-truncated ⟨0⟩

  →-is-prop : ∀ {i j} {A : Set i} {B : Set j}
    → (is-prop B → is-prop (A → B))
  →-is-prop = →-is-truncated ⟨-1⟩

-- Type of all n-truncated types

Type≤ : (n : ℕ₋₂) (i : Level) → Set (suc i)
Type≤ n i = Σ (Set i) (is-truncated n)

hProp : (i : Level) → Set (suc i)
hProp = Type≤ ⟨-1⟩

hSet : (i : Level) → Set (suc i)
hSet = Type≤ ⟨0⟩

-- [Type≤ n] is (n+1)-truncated

abstract
  ≃-is-truncated : ∀ {i} (n : ℕ₋₂) {A B : Set i}
    → (is-truncated n A → is-truncated n B → is-truncated n (A ≃ B))
  ≃-is-truncated ⟨-2⟩ pA pB =
    (((λ _ → π₁ pB) , contr-to-contr-is-equiv _ pA pB)
    , (λ _ → Σ-eq (funext (λ _ → contr-has-all-paths pB _ _))
                        (π₁ (is-equiv-is-prop _ _ _))))
  ≃-is-truncated (S n) pA pB = Σ-is-truncated (S n) (→-is-truncated (S n) pB)
                                      (λ _ → prop-is-truncated-S n
                                             (is-equiv-is-prop _))

  ≃-is-set : ∀ {i} {A B : Set i} → (is-set A → is-set B → is-set (A ≃ B))
  ≃-is-set = ≃-is-truncated ⟨0⟩

  universe-≡-is-truncated : ∀ {i} (n : ℕ₋₂) {A B : Set i}
    → (is-truncated n A → is-truncated n B → is-truncated n (A ≡ B))
  universe-≡-is-truncated n pA pB = equiv-types-truncated n eq-to-path-equiv
    $ ≃-is-truncated n pA pB

  universe-≡-is-set : ∀ {i} {A B : Set i}
    → (is-set A → is-set B → is-set (A ≡ B))
  universe-≡-is-set = universe-≡-is-truncated ⟨0⟩

  Type≤-is-truncated : (n : ℕ₋₂) (i : Level)
    → is-truncated (S n) (Type≤ n i)
  Type≤-is-truncated n i A B =
    equiv-types-truncated n total-Σ-eq-equiv
    (Σ-is-truncated n (universe-≡-is-truncated n (π₂ A) (π₂ B))
    (λ _ → contr-is-truncated n (≡-is-truncated _
           (inhab-prop-is-contr (π₂ B) (is-truncated-is-prop n {-(π₁ B)-})))))

  hProp-is-set : (i : Level) → is-set (hProp i)
  hProp-is-set = Type≤-is-truncated _

  hSet-is-gpd : (i : Level) → is-gpd (hSet i)
  hSet-is-gpd = Type≤-is-truncated _

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
open import Coinduction using ( ♭ ; ♯_ )
open import Data.Empty using ( ⊥-elim )
open import System.IO.Transducers.Session using ( Session ; I ; Σ ; IsΣ ; Γ ; _/_ ; _∼_ )
open import System.IO.Transducers.Trace using ( Trace ; [] ; _∷_ ; _⊨_✓ ; _✓ ; _⊑_ )
open import System.IO.Transducers.Lazy using ( _⇒_ ; inp ; out ; done ; ⟦_⟧ ; _≃_ ; equiv )
open import System.IO.Transducers.Reflective using ( Reflective ; inp ; out ; done )
open import System.IO.Transducers.Strict using ( Strict ; inp ; done )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; trans ; cong )
open import Relation.Nullary using ( Dec ; ¬_ ; yes ; no )

module System.IO.Transducers.Properties.Lemmas where

open Relation.Binary.PropositionalEquality.≡-Reasoning

-- ≃ is an equivalence

≃-refl : ∀ {S T} {f : Trace S → Trace T} → (f ≃ f)
≃-refl as = refl

≃-sym : ∀ {S T} {f g : Trace S → Trace T} →
  (f ≃ g) → (g ≃ f)
≃-sym f≃g as = sym (f≃g as)

≃-trans : ∀ {S T} {f g h : Trace S → Trace T} →
  (f ≃ g) → (g ≃ h) → (f ≃ h)
≃-trans f≃g g≃h as = trans (f≃g as) (g≃h as)

-- Completion is decidable

✓-tl : ∀ {S a as} → (S ⊨ a ∷ as ✓) → (S / a ⊨ as ✓)
✓-tl (a ∷ as✓) = as✓

✓? : ∀ {S} as → (Dec (S ⊨ as ✓))
✓? {I}     [] = yes []
✓? {Σ V F} [] = no (λ ())
✓?         (a ∷ as) with ✓? as
✓?         (a ∷ as) | yes as✓ = yes (a ∷ as✓)
✓?         (a ∷ as) | no ¬as✓ = no (λ a∷as✓ → ¬as✓ (✓-tl a∷as✓))

-- Eta conversion for traces of type I

I-η : ∀ (as : Trace I) → (as ≡ [])
I-η [] = refl
I-η (() ∷ as)

-- All traces at type I are complete

I-✓ : ∀ (as : Trace I) → (as ✓)
I-✓ [] = []
I-✓ (() ∷ as)

-- Cons is invertable

∷-refl-≡₁ : ∀ {S a b} {as bs : Trace S} {cs ds} →
  (as ≡ a ∷ cs) → (bs ≡ b ∷ ds) → (as ≡ bs) → (a ≡ b)
∷-refl-≡₁ refl refl refl = refl

∷-refl-≡₂ : ∀ {S a} {as bs : Trace S} {cs ds} →
  (as ≡ a ∷ cs) → (bs ≡ a ∷ ds) → (as ≡ bs) → (cs ≡ ds)
∷-refl-≡₂ refl refl refl = refl

-- Make a function reflective

liat : ∀ {S} → (Trace S) → (Trace S)
liat []           = []
liat (a ∷ [])     = []
liat (a ∷ b ∷ bs) = a ∷ liat (b ∷ bs)

incomplete : ∀ {S} → (Trace S) → (Trace S)
incomplete as with ✓? as
incomplete as | yes ✓as = liat as
incomplete as | no ¬✓as = as

reflective : ∀ {S T} → (Trace S → Trace T) → (Trace S → Trace T)
reflective f as with ✓? as
reflective f as | yes ✓as = f as
reflective f as | no ¬✓as = incomplete (f as)

liat-¬✓ : ∀ {S} a as → ¬ (S ⊨ liat (a ∷ as) ✓)
liat-¬✓         a  (b ∷ bs) (.a ∷ ✓cs) = liat-¬✓ b bs ✓cs
liat-¬✓ {I}     () []       []✓
liat-¬✓ {Σ V F} a  []       ()

incomplete-¬✓ : ∀ {S} {isΣ : IsΣ S} (as : Trace S) → ¬ (incomplete as ✓)
incomplete-¬✓ as with ✓? as
incomplete-¬✓ {I}  {} [] | yes []
incomplete-¬✓ {Σ V F} [] | yes ()
incomplete-¬✓ (a ∷ as)   | yes ✓a∷as = liat-¬✓ a as
incomplete-¬✓ as         | no ¬✓as = ¬✓as

reflective-refl-✓ : ∀ {S T} {isΣ : IsΣ T} (f : Trace S → Trace T) as → (reflective f as ✓) → (as ✓)
reflective-refl-✓             f as ✓bs with ✓? as
reflective-refl-✓             f as ✓bs | yes ✓as = ✓as
reflective-refl-✓ {S} {Σ V F} f as ✓bs | no ¬✓as = ⊥-elim (incomplete-¬✓ (f as) ✓bs)
reflective-refl-✓ {S} {I}  {} f as ✓bs | no ¬✓as

reflective-≡-✓ : ∀ {S T} (f : Trace S → Trace T) {as} → (as ✓) → (reflective f as ≡ f as)
reflective-≡-✓ f {as} ✓as with ✓? as
reflective-≡-✓ f {as} ✓as | yes _   = refl
reflective-≡-✓ f {as} ✓as | no ¬✓as = ⊥-elim (¬✓as ✓as)

-- All transducers are monotone

⟦⟧-mono :  ∀ {S T} (P : S ⇒ T) as bs → (as ⊑ bs) → (⟦ P ⟧ as ⊑ ⟦ P ⟧ bs)
⟦⟧-mono (inp P)   .[]       bs        []          = []
⟦⟧-mono (inp P)   (.a ∷ as) (.a ∷ bs) (a ∷ as⊑bs) = ⟦⟧-mono (♭ P a) as bs as⊑bs
⟦⟧-mono (out b P) as        bs        as⊑bs       = b ∷ (⟦⟧-mono P as bs as⊑bs)
⟦⟧-mono done      as        bs        as⊑bs       = as⊑bs

-- All transducers respect completion

⟦⟧-resp-✓ : ∀ {S T} (P : S ⇒ T) as → (as ✓) → (⟦ P ⟧ as ✓)
⟦⟧-resp-✓ (inp P)    (a ∷ as) (.a ∷ ✓as) = ⟦⟧-resp-✓ (♭ P a) as ✓as
⟦⟧-resp-✓ (out b P)  as       ✓as        = b ∷ ⟦⟧-resp-✓ P as ✓as
⟦⟧-resp-✓ done       as       ✓as        = ✓as
⟦⟧-resp-✓ (inp P)    []       ()

-- Reflective transducers reflect completion

⟦⟧-refl-✓ : ∀ {S T} {P : S ⇒ T} → (Reflective P) → ∀ as → (⟦ P ⟧ as ✓) → (as ✓)
⟦⟧-refl-✓ (inp ⟳P)   (a ∷ as) bs✓ = a ∷ ⟦⟧-refl-✓ (♭ ⟳P a) as bs✓
⟦⟧-refl-✓ (out b ⟳P) as       bs✓ = ⟦⟧-refl-✓ ⟳P as (✓-tl bs✓)
⟦⟧-refl-✓ done       as       bs✓ = bs✓
⟦⟧-refl-✓ (inp ⟳P)   []       ()

-- Any transducer which reflects completion is reflective

⟦⟧-refl-✓⁻¹ : ∀ {S T} (P : S ⇒ T) → (∀ as → (⟦ P ⟧ as ✓) → (as ✓)) → (Reflective P)
⟦⟧-refl-✓⁻¹ {Σ V F} {Σ W G} (inp P)   H = inp (♯ λ a → ⟦⟧-refl-✓⁻¹ (♭ P a) (λ as → λ bs✓ → ✓-tl (H (a ∷ as) bs✓)))
⟦⟧-refl-✓⁻¹                 (out b P) H = out b (⟦⟧-refl-✓⁻¹ P (λ as bs✓ → H as (b ∷ bs✓)))
⟦⟧-refl-✓⁻¹                 done      H = done
⟦⟧-refl-✓⁻¹ {Σ V F} {I}     (inp P)   H with H [] []
⟦⟧-refl-✓⁻¹ {Σ V F} {I}     (inp P)   H | ()

-- Strict transducers respect emptiness.

⟦⟧-resp-[] : ∀ {S T} {P : S ⇒ T} → (Strict P) → (⟦ P ⟧ [] ≡ [])
⟦⟧-resp-[] (inp P) = refl
⟦⟧-resp-[] done    = refl

-- Any transducer which respects emptiness is strict.

⟦⟧-resp-[]⁻¹ : ∀ {S T} (P : S ⇒ T) → (∀ {as} → (as ≡ []) → (⟦ P ⟧ as ≡ [])) → (Strict P)
⟦⟧-resp-[]⁻¹ (inp P)   H = inp P
⟦⟧-resp-[]⁻¹ (out b P) H with H refl
⟦⟧-resp-[]⁻¹ (out b P) H | ()
⟦⟧-resp-[]⁻¹ done      H = done

-- Coherence wrt ∼

⟦⟧-resp-∼ : ∀ {S T} (eq₁ eq₂ : S ∼ T) → ⟦ equiv eq₁ ⟧ ≃ ⟦ equiv eq₂ ⟧
⟦⟧-resp-∼ I       I        as       = refl
⟦⟧-resp-∼ (Σ V F) (Σ .V G) []       = refl
⟦⟧-resp-∼ (Σ V F) (Σ .V G) (a ∷ as) = cong (_∷_ a) (⟦⟧-resp-∼ (♭ F a) (♭ G a) as)

-- IsEquiv P is inhabited whenever P is equivalent to an equivalence

data IsEquiv {S T : Session} (P : S ⇒ T) : Set₁ where
  isEquiv : (S∼T : S ∼ T) → (⟦ P ⟧ ≃ ⟦ equiv S∼T ⟧) → (IsEquiv P)

-- Equivalences are equivalent

≃-equiv : ∀ {S T} {P Q : S ⇒ T} → (IsEquiv P) → (IsEquiv Q) → (⟦ P ⟧ ≃ ⟦ Q ⟧)
≃-equiv {S} {T} {P} {Q} (isEquiv eq₁ P≃eq₁) (isEquiv eq₂ Q≃eq₂) as =
  begin
    ⟦ P ⟧ as
  ≡⟨ P≃eq₁ as ⟩
    ⟦ equiv eq₁ ⟧ as
  ≡⟨ ⟦⟧-resp-∼ eq₁ eq₂ as ⟩
    ⟦ equiv eq₂ ⟧ as
  ≡⟨ sym (Q≃eq₂ as) ⟩
    ⟦ Q ⟧ as
  ∎

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
{-# OPTIONS --universe-polymorphism #-}

-- Should give some unsolved metas
module Issue203b where

open import Imports.Level

-- Should work but give unsolved metas (type of b)
data ↓ {a b} (A : Set a) : Set a where
  [_] : (x : A) → ↓ A

-- Shouldn't instantiate the level of Σ to a
data Σ {a b} (A : Set a) (B : A → Set b) : Set _ where
  _,_ : (x : A) (y : B x) → Σ A B

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

data S1 : Set where
  base : S1
  loop : base ≡ base
postulate
  weird : S1 → I

bad : (x : S1) → I
bad base = {!!}
bad (loop x) = {!!}

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


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

open import OscarPrelude

record HasSubstitution (T : Set) (S : Set) : Set where
  field
    _◃_ : S → T → T

open HasSubstitution ⦃ … ⦄ public

record HasPairUnification (T : Set) (S : Set) : Set where
  field
    ⦃ hasSubstitution ⦄ : HasSubstitution T S

  Property : Set₁
  Property = S × S → Set

  Nothing : Property → Set
  Nothing P = ∀ s → P s → ⊥

  IsPairUnifier : (t₁ t₂ : T) → Property
  IsPairUnifier t₁ t₂ s = let s₁ , s₂ = s in s₁ ◃ t₁ ≡ s₂ ◃ t₂

  field
    unify : (t₁ t₂ : T) → Dec ∘ ∃ $ IsPairUnifier t₁ t₂

open HasPairUnification ⦃ … ⦄ public

open import HasNegation

record HasSubstantiveDischarge (A : Set) : Set₁
 where
  field
    _o≽o_ : A → A → Set

  field
    ⦃ hasNegation ⦄ : HasNegation A

  _⋡_ : A → A → Set
  _⋡_ (+) (-) = ¬ + o≽o -

  field
    ≽-reflexive : (x : A) → x o≽o x
    ≽-consistent : (+ - : A) → + o≽o - → + ⋡ ~ -
    ≽-contrapositive : ∀ x y → ~ x o≽o y → x o≽o ~ y

  ≽-contrapositive' : ∀ x y → x o≽o ~ y → ~ x o≽o y
  ≽-contrapositive' = {!!}

open HasSubstantiveDischarge ⦃ … ⦄ public

{-# DISPLAY HasSubstantiveDischarge._o≽o_ _ = _o≽o_ #-}

open import Membership

record HasGenericSubstantiveDischarge (A : Set) (B : Set) : Set₁
 where
  field
    _≽_ : A → B → Set

open HasGenericSubstantiveDischarge ⦃ … ⦄ public

{-# DISPLAY HasGenericSubstantiveDischarge._≽_ _ = _≽_ #-}

instance HasGenericSubstantiveDischargeReflexive : ∀ {A} ⦃ _ : HasSubstantiveDischarge A ⦄ → HasGenericSubstantiveDischarge A A
HasGenericSubstantiveDischarge._≽_ HasGenericSubstantiveDischargeReflexive = _o≽o_

instance HasGenericSubstantiveDischargeAList : ∀ {A} ⦃ _ : HasSubstantiveDischarge A ⦄ → HasGenericSubstantiveDischarge A (List A)
HasGenericSubstantiveDischarge._≽_ (HasGenericSubstantiveDischargeAList {A}) (+) -s = ∃ λ (i : A) → i ∈ -s × (+ ≽ i)

instance HasGenericSubstantiveDischargeListA : ∀ {A} ⦃ _ : HasSubstantiveDischarge A ⦄ → HasGenericSubstantiveDischarge (List A) A
HasGenericSubstantiveDischarge._≽_ (HasGenericSubstantiveDischargeListA {A}) (+s) (-) = ∃ λ (c : A) → c ∈ +s × c ≽ -

instance HasGenericSubstantiveDischargeListList : ∀ {A} ⦃ _ : HasSubstantiveDischarge A ⦄ → HasGenericSubstantiveDischarge (List A) (List A)
HasGenericSubstantiveDischarge._≽_ (HasGenericSubstantiveDischargeListList {A}) +s -s = ∀ (i : A) → i ∈ -s → +s ≽ i

⋆≽⋆-reflexive : ∀ {A} ⦃ _ : HasSubstantiveDischarge A ⦄ → (xs : List A) → xs ≽ xs
⋆≽⋆-reflexive _ i i∈ys⋆ = _ , i∈ys⋆ , ≽-reflexive i

◁_ : ∀ {A} ⦃ _ : HasSubstantiveDischarge A ⦄ → List A → Set
◁_ {A} +s = ∃ λ (s : A) → s ∈ +s × +s ≽ ~ s

⋪_ : ∀ {A} ⦃ _ : HasSubstantiveDischarge A ⦄ → List A → Set
⋪_ = ¬_ ∘ ◁_

record HasDecidableSubstantiveDischarge (A : Set) : Set₁
 where
  field
    ⦃ hasSubstantiveDischarge ⦄ : HasSubstantiveDischarge A
    _≽?_ : (+ - : A) → Dec $ + o≽o -

open HasDecidableSubstantiveDischarge ⦃ … ⦄ public

{-# DISPLAY HasDecidableSubstantiveDischarge._≽?_ _ = _≽?_ #-}

_⋆≽?_ : ∀ {A} ⦃ _ : HasDecidableSubstantiveDischarge A ⦄ → (+s : List A) → (- : A) → Dec (+s ≽ -)
_⋆≽?_ [] - = no λ { (_ , () , _)}
_⋆≽?_ (+ ∷ +s) - with + ≽? -
… | yes +≽- = yes $ _ , zero , +≽-
… | no +⋡- with +s ⋆≽? -
… | yes (+' , +'∈+s , +'≽-) = yes $ _ , suc +'∈+s , +'≽-
… | no +s⋡- = no λ { (_ , zero , +≽-) → +⋡- +≽-
                   ; (+' , suc +'∈+s , +'≽-) → +s⋡- $ _ , +'∈+s , +'≽- }

_≽⋆?_ : ∀ {A} ⦃ _ : HasDecidableSubstantiveDischarge A ⦄ → (+ : A) → (-s : List A) → Dec (+ ≽ -s)
+ ≽⋆? [] = no (λ { (fst₁ , () , snd₁)})
+ ≽⋆? (- ∷ -s) with + ≽? -
… | yes +≽- = yes (_ , zero , +≽-)
… | no +⋡- with + ≽⋆? -s
… | yes (_ , i∈-s , +≽⋆i) = yes (_ , suc i∈-s , +≽⋆i)
… | no +⋡⋆-s = no (λ { (_ , zero , +≽-) → +⋡- +≽-
                     ; (_ , suc -'∈-s , +≽-') → +⋡⋆-s (_ , -'∈-s , +≽-')})

_⋆≽⋆?_ : ∀ {A} ⦃ _ : HasDecidableSubstantiveDischarge A ⦄ → (+s : List A) → (-s : List A) → Dec (+s ≽ -s)
_⋆≽⋆?_ +s [] = yes λ _ ()
_⋆≽⋆?_ +s (- ∷ -s) with +s ⋆≽? -
… | no +s⋡- = no λ +s≽-∷-s → +s⋡- $ +s≽-∷-s (-) zero
… | yes +s≽- with +s ⋆≽⋆? -s
… | yes +s≽-s = yes λ { _ zero → +s≽-
                      ; -' (suc -'∈-∷-s) → +s≽-s -' -'∈-∷-s }
… | no +s⋡-s = no λ +s≽-∷-s → +s⋡-s λ +' +'∈-s → +s≽-∷-s +' (suc +'∈-s)

◁?_ : ∀ {+} ⦃ _ : HasDecidableSubstantiveDischarge (+) ⦄
            → (+s : List +) → Dec $ ◁ +s
◁? [] = no λ {(_ , () , _)}
◁?_ (+ ∷ +s) with +s ⋆≽? ~ +
… | yes (_ , +'∈+s , +'≽~+) = yes $ _ , zero , _ , suc +'∈+s , +'≽~+
… | no +s⋆⋡~+ with ~ + ≽⋆? +s
… | yes (_ , c∈+s , ~+≽c) = yes (_ , suc c∈+s , _ , zero , ≽-contrapositive (+) _ ~+≽c)
… | no ~+⋡⋆+s with ◁? +s
… | yes (s , s∈+s , c , c∈+s , c≽~s) = yes $ _ , suc s∈+s , _ , suc c∈+s , c≽~s
… | no ⋪+s = no
  λ { (_ , zero , _ , zero , c≽~s) → ≽-consistent (+) (+) (≽-reflexive +) c≽~s
  ; (_ , zero , c , suc c∈+s , c≽~s) → +s⋆⋡~+ (_ , c∈+s , c≽~s)
  ; (s , suc s∈+s , .+ , zero , +≽~s) → ~+⋡⋆+s (_ , s∈+s , ≽-contrapositive' (+) s +≽~s)
  ; (s , suc s∈+s , c , suc c∈+s , c≽~s) → ⋪+s (_ , s∈+s , _ , c∈+s , c≽~s) }


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Constructions.Thin where

open import Cats.Category.Base

open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_)

module _ {lo la l≈} (C : Category lo la l≈) where

  open Category C

  Thin : Set (lo ⊔ la ⊔ l≈)
  Thin = ∀ {A B} {f g : A ⇒ B} → f ≈ g

  StronglyThin : Set (lo ⊔ la)
  StronglyThin = ∀ {A B} {f g : A ⇒ B} → f ≡ g

StronglyThin→Thin : ∀ {lo la l≈} {C : Category lo la l≈}
  → StronglyThin C → Thin C
StronglyThin→Thin {C = C} sthin = ≈.reflexive sthin
  where
    open Category C

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
------------------------------------------------------------------------------
-- All the group theory modules
------------------------------------------------------------------------------

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

module GroupTheory.Everything where

open import GroupTheory.Base
open import GroupTheory.Base.Consistency.Axioms

open import GroupTheory.AbelianGroup.Base
open import GroupTheory.AbelianGroup.Base.Consistency.Axioms
open import GroupTheory.AbelianGroup.PropertiesATP

open import GroupTheory.Commutator
open import GroupTheory.Commutator.PropertiesATP
open import GroupTheory.Commutator.PropertiesI

open import GroupTheory.PropertiesATP
open import GroupTheory.PropertiesI

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --warning=error #-}

module _ (A : Set) where

{-# POLARITY A #-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import prelude renaming (_≟String_ to _≟_)

infixl 5 _$_

-- Copied pretty much verbatim

Var = String

data Term : Set where
  var : Var → Term
  fun : Var → Term → Term
  _$_ : Term → Term → Term

data Value : Term → Set where
  fun : (x : Var) → (t : Term) → Value(fun x t)

-- Free variables of a term.
-- (Turns out to be easiest to define when a variable isn't free rather than when it is.)

data _∉FV_ : Var → Term → Set where

  var : ∀ {x y} →

    x ≢ y →
    -------------
    x ∉FV(var y)

  fun₁ : ∀ {x y t} →

    (x ≡ y) →
    ---------------
    x ∉FV(fun y t)

  fun₂ : ∀ {x y t} →

    (x ∉FV(t)) →
    ---------------
    x ∉FV(fun y t)

  app : ∀ {x t₁ t₂} →

    (x ∉FV(t₁)) →
    (x ∉FV(t₂)) →
    -----------------
    (x ∉FV(t₁ $ t₂))

-- Substitution
-- TAPL defines substitution as a partial function, which Agda doesn't implement.
-- So instead we keep track of the derivation tree.

data [_↦_]_is_ : Var → Term → Term → Term → Set where

  yes : ∀ {x y s} →

    (x ≡ y) →
    ----------------------
    [ x ↦ s ] (var y) is s

  no : ∀ {x y s} →

    (x ≢ y) →
    ----------------------------
    [ x ↦ s ] (var y) is (var y)

  fun₁ : ∀ {x y s t} →

    (x ≡ y) →
    --------------------------------
    [ x ↦ s ] (fun y t) is (fun y t)

  fun₂ : ∀ {x y s t t′} →

    (x ≢ y) →
    (y ∉FV(s)) →
    [ x ↦ s ] t is t′ →
    ---------------------------------
    [ x ↦ s ] (fun y t) is (fun y t′)

  app : ∀ {x s t₁ t₁′ t₂ t₂′} →

    [ x ↦ s ] t₁ is t₁′ →
    [ x ↦ s ] t₂ is t₂′ →
    ---------------------------------
    [ x ↦ s ] (t₁ $ t₂) is (t₁′ $ t₂′)

-- Reduction is as per TAPL

data _⟶_ : Term → Term → Set where

  E─App1 : ∀ {t₁ t₁′ t₂} →

     (t₁ ⟶ t₁′) →
     ------------------------
     (t₁ $ t₂) ⟶ (t₁′ $ t₂)

  E─App2 : ∀ {t₁ t₂ t₂′} →

     (t₂ ⟶ t₂′) →
     ------------------------
     (t₁ $ t₂) ⟶ (t₁ $ t₂′)

  E─AppAbs : ∀ {x t₁ t₂ t₃} →

     [ x ↦ t₂ ] t₁ is t₃ →
     ----------------------
     (fun x t₁ $ t₂) ⟶ t₃

-- A redex is a term which can reduce

data Redex  : Term → Set where

  redex : ∀ {t t′} →

    t ⟶ t′ →
    --------
    Redex(t)

-- A closed term is one with no free variables

Closed : Term → Set
Closed(t) = ∀ {x} → x ∉FV(t)

-- Proving that substitution is well-defined for closed terms

data [_↦_]_⇓ : Var → Term → Term → Set where

  subst : ∀ {x s t t′} →
    ([ x ↦ s ] t is t′) →
    ([ x ↦ s ] t ⇓)

substDef : (x : Var) → (s t : Term) → Closed(s) → ([ x ↦ s ] t ⇓)
substDef x s (var y) c = helper (x ≟ y) where

  helper : Dec(x ≡ y) → ([ x ↦ s ] (var y) ⇓)
  helper (yes p) = subst (yes p)
  helper (no  p) = subst (no p)

substDef x s (fun y t) c = helper₁ (x ≟ y) where

  helper₂ : (x ≢ y) → ([ x ↦ s ] t ⇓) → ([ x ↦ s ] (fun y t) ⇓)
  helper₂ p (subst s) = subst (fun₂ p c s)

  helper₁ : Dec(x ≡ y) → ([ x ↦ s ] (fun y t) ⇓)
  helper₁ (yes p) = subst (fun₁ p)
  helper₁ (no  p) = helper₂ p (substDef x s t c)

substDef x s (t₁ $ t₂) c = helper (substDef x s t₁ c) (substDef x s t₂ c) where

  helper : ([ x ↦ s ] t₁ ⇓) → ([ x ↦ s ] t₂ ⇓) → ([ x ↦ s ] (t₁ $ t₂) ⇓)
  helper (subst s₁) (subst s₂) = subst (app s₁ s₂)

-- Proving that closed terms stay closed

closed₁ : ∀ {t₁ t₂ x} → (x ∉FV(t₁ $ t₂)) → (x ∉FV(t₁))
closed₁ (app p₁ p₂) = p₁

closed₂ :  ∀ {t₁ t₂ x} → (x ∉FV(t₁ $ t₂)) → (x ∉FV(t₂))
closed₂ (app p₁ p₂) = p₂

substClosed₁ : ∀ {y s t t′} → (y ∉FV(s)) → ([ y ↦ s ] t is t′) → (y ∉FV(t′))
substClosed₁ p (yes refl) = p
substClosed₁ p (no q) = var q
substClosed₁ p (fun₁ q) = fun₁ q
substClosed₁ p (fun₂ x x₁ q) = fun₂ (substClosed₁ p q)
substClosed₁ p (app q₁ q₂) = app (substClosed₁ p q₁) (substClosed₁ p q₂)

substClosed₂ : ∀ {x y s t t′} → (x ∉FV(t)) → (x ∉FV(s)) → ([ y ↦ s ] t is t′) → (x ∉FV(t′))
substClosed₂ p q (yes refl) = q
substClosed₂ p q (no r) = p
substClosed₂ p q (fun₁ refl) = p
substClosed₂ (fun₁ p) q (fun₂ x x₁ r) = fun₁ p
substClosed₂ (fun₂ p) q (fun₂ x x₁ r) = fun₂ (substClosed₂ p q r)
substClosed₂ (app p₁ p₂) q (app r₁ r₂) = app (substClosed₂ p₁ q r₁) (substClosed₂ p₂ q r₂)

substClosed₃ : ∀ {x y s t t′} → x ∉FV(fun y t) → x ∉FV(s) → ([ y ↦ s ] t is t′) → x ∉FV(t′)
substClosed₃ (fun₁ refl) q r = substClosed₁ q r
substClosed₃ (fun₂ p)    q r = substClosed₂ p q r

redexClosed : ∀ {t t′} → Closed(t) → (t ⟶ t′) → Closed(t′)
redexClosed c (E─App1 r)   = app (redexClosed (closed₁ c) r) (closed₂ c)
redexClosed c (E─App2 r)   = app (closed₁ c) (redexClosed (closed₂ c) r)
redexClosed c (E─AppAbs s) = substClosed₃ (closed₁ c) (closed₂ c) s

-- Proving that every closed term is a value or a redex

data ValueOrRedex : Term → Set where

  value : ∀ {t} →

    (Value(t)) →
    ---------------
    ValueOrRedex(t)

  redex : ∀ {t t′} →

    t ⟶ t′ →
    ---------------
    ValueOrRedex(t)

valueOrRedex : (t : Term) → Closed(t) → ValueOrRedex(t)
valueOrRedex (var x) c = CONTRADICTION (helper c) where

  helper : (x ∉FV(var x)) → FALSE
  helper (var p) = p refl

valueOrRedex (fun x t) c = value (fun x t)
valueOrRedex (t₁ $ t₂) c = helper₁ (valueOrRedex t₁ (closed₁ c)) where

  helper₃ : ∀ {x s t} → ([ x ↦ s ] t ⇓) → ValueOrRedex((fun x t) $ s)
  helper₃ (subst s) = redex (E─AppAbs s)

  helper₂ : ∀ {t₁} → Value(t₁) → ValueOrRedex(t₂) → ValueOrRedex(t₁ $ t₂)
  helper₂ (fun x t) (value v) = helper₃ (substDef x t₂ t (closed₂ c))
  helper₂ (fun x t) (redex r) = redex (E─App2 r)

  helper₁ : ValueOrRedex(t₁) → ValueOrRedex(t₁ $ t₂)
  helper₁ (value v₁) = helper₂ v₁ (valueOrRedex t₂ (closed₂ c))
  helper₁ (redex r) = redex (E─App1 r)

-- Interpreter!

data _⟶*_ : Term → Term → Set where

  done : ∀ {t} →

    --------
    t ⟶* t

  redex : ∀ {t t′ t″} →

    t ⟶ t′ →
    t′ ⟶* t″ →
    ----------
    t ⟶* t″

-- An interpreter result

data Result  : Term → Set where

  result : ∀ {t t′} →

    t ⟶* t′ →
    Value(t′) →
    ---------
    Result(t)

-- The interpreter just calls `valueOrRedex` until it is a value.
-- This might bot terminate!

{-# NON_TERMINATING #-}
interp : (t : Term) → Closed(t) → Result(t)
interp t c = helper₂ (valueOrRedex t c) where

  helper₁ : ∀ {t′} → (t ⟶ t′) → Result(t′) → Result(t)
  helper₁ r (result s v) = result (redex r s) v

  helper₂ : ValueOrRedex(t) → Result(t)
  helper₂ (value v)           = result done v
  helper₂ (redex {t′ = t′} r) = helper₁ r (interp t′ (redexClosed c r))

-- Examples

zer : Term
zer = fun "z" (fun "s" (var "z"))

succ : Term
succ = fun "x" (fun "z" (fun "s" (var "s" $ var "x")))

add : Term
add = fun "x" (fun "y" (var "x" $ var "y" $ succ))

two : Term
two = succ $ (succ $ zer)

four : Term
four = add $ two $ two

zerC : Closed(zer)
zerC {x} with (x ≟ "z")
... | yes refl = fun₁ refl
... | no  p    = fun₂ (fun₂ (var p))

succC : Closed(succ)
succC {x} with (x ≟ "x") | (x ≟ "s")
... | yes refl | _        = fun₁ refl
... | no  p    | yes refl = fun₂ (fun₂ (fun₁ refl))
... | no  p    | no q     = fun₂ (fun₂ (fun₂ (app (var q) (var p))))

addC : Closed(add)
addC {x} with (x ≟ "x") | (x ≟ "y")
... | yes refl | _        = fun₁ refl
... | no  p    | yes refl = fun₂ (fun₁ refl)
... | no  p    | no q     = fun₂ (fun₂ (app (app (var p) (var q)) succC))

twoC : Closed(two)
twoC = app succC (app succC zerC)

fourC : Closed(four)
fourC = app (app addC twoC) twoC

max_stars_repo_name: asajeffrey/tapl

max_issues_repo_name: asajeffrey/tapl

max_forks_repo_name: asajeffrey/tapl


text:
-- Reported by fredrik.forsberg, Oct 21, 2014
-- The following code gives an internal error

-- "An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/InstanceArguments.hs:269"

-- on Agda head, since "n ≠ zero" is not expanded.

open import Common.Prelude
open import Common.Equality

¬ : (A : Set) → Set
¬ A = A → ⊥

_≠_ : {A : Set} → (A → A → Set)
x ≠ y = ¬ (x ≡ y)

f : (n : Nat) ⦃ _ : n ≠ zero ⦄ -> Nat
f n = n

g : Nat
g = f (suc zero)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module C where

open import B

C : Set
C = B

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ )
open import Relation.Binary.PropositionalEquality using ( refl )
open import Web.Semantic.DL.ABox.Interp using ( ⌊_⌋ ; ind ; _*_ )
open import Web.Semantic.DL.ABox.Model using
  ( _⊨a_ ; ⊨a-resp-≡³ ; on-bnode ; bnodes ; _,_ )
open import Web.Semantic.DL.Category.Object using ( Object ; IN )
open import Web.Semantic.DL.Category.Morphism using
  ( _⇒_ ; BN ; impl ; _⊑_ ; _≣_ ; _,_ )
open import Web.Semantic.DL.Category.Composition using ( _∙_ )
open import Web.Semantic.DL.Category.Tensor using ( _⊗_ ; _⟨⊗⟩_ )
open import Web.Semantic.DL.Category.Wiring using ( identity ; id✓ )
open import Web.Semantic.DL.Category.Properties.Composition.Lemmas using
  ( compose-left ; compose-right ; compose-resp-⊨a )
open import Web.Semantic.DL.Category.Properties.Tensor.Lemmas using
  ( tensor-up ; tensor-down ; tensor-resp-⊨a )
open import Web.Semantic.DL.Category.Properties.Tensor.RespectsWiring using
  ( tensor-resp-wiring )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.DL.TBox.Interp using ( Δ )
open import Web.Semantic.Util using
  ( id ; _∘_ ; _⊕_⊕_ ; inode ; bnode ; enode ; left ; right ; up ; down )

module Web.Semantic.DL.Category.Properties.Tensor.Functor
  {Σ : Signature} {S T : TBox Σ} where

tensor-resp-id : ∀ (A₁ A₂ : Object S T) →
  ((identity A₁ ⟨⊗⟩ identity A₂) ≣ identity (A₁ ⊗ A₂))
tensor-resp-id A₁ A₂ =
  tensor-resp-wiring A₁ A₂ A₁ A₂
    id (id✓ A₁) id (id✓ A₂) id (id✓ (A₁ ⊗ A₂))
    (λ x → refl) (λ x → refl)

tensor-resp-compose :  ∀ {A₁ A₂ B₁ B₂ C₁ C₂ : Object S T}
  (F₁ : A₁ ⇒ B₁) (F₂ : A₂ ⇒ B₂) (G₁ : B₁ ⇒ C₁) (G₂ : B₂ ⇒ C₂) →
    (((F₁ ∙ G₁) ⟨⊗⟩ (F₂ ∙ G₂)) ≣ ((F₁ ⟨⊗⟩ F₂) ∙ (G₁ ⟨⊗⟩ G₂)))
tensor-resp-compose {A₁} {A₂} {B₁} {B₂} {C₁} {C₂} F₁ F₂ G₁ G₂ =
  (LHS⊑RHS , RHS⊑LHS) where

  LHS⊑RHS : (F₁ ∙ G₁) ⟨⊗⟩ (F₂ ∙ G₂) ⊑ (F₁ ⟨⊗⟩ F₂) ∙ (G₁ ⟨⊗⟩ G₂)
  LHS⊑RHS I I⊨STA₁A₂ I⊨LHS = (f , I⊨RHS) where

    f : ((BN F₁ ⊎ BN F₂) ⊕ (IN B₁ ⊎ IN B₂) ⊕ (BN G₁ ⊎ BN G₂)) → Δ ⌊ I ⌋
    f (inode (inj₁ v)) = ind I (bnode (inj₁ (inode v)))
    f (inode (inj₂ v)) = ind I (bnode (inj₂ (inode v)))
    f (bnode (inj₁ y)) = ind I (bnode (inj₁ (bnode y)))
    f (bnode (inj₂ y)) = ind I (bnode (inj₂ (bnode y)))
    f (enode (inj₁ w)) = ind I (bnode (inj₁ (enode w)))
    f (enode (inj₂ w)) = ind I (bnode (inj₂ (enode w)))

    Iˡ₁⊨F₁ : up * left * bnodes I f ⊨a impl F₁
    Iˡ₁⊨F₁ = ⊨a-resp-≡³
      (left * up * I) (on-bnode f (ind I) ∘ left ∘ up) refl (impl F₁)
      (compose-left F₁ G₁ (up * I) (tensor-up (F₁ ∙ G₁) (F₂ ∙ G₂) I I⊨LHS))

    Iˡ₂⊨F₂ : down * (left * bnodes I f) ⊨a impl F₂
    Iˡ₂⊨F₂ = ⊨a-resp-≡³
      (left * down * I) (on-bnode f (ind I) ∘ left ∘ down) refl (impl F₂)
      (compose-left F₂ G₂ (down * I) (tensor-down (F₁ ∙ G₁) (F₂ ∙ G₂) I I⊨LHS))

    Iʳ₁⊨G₁ : up * (right * bnodes I f) ⊨a impl G₁
    Iʳ₁⊨G₁ = ⊨a-resp-≡³
      (right * up * I) (on-bnode f (ind I) ∘ right ∘ up) refl (impl G₁)
      (compose-right F₁ G₁ (up * I) (tensor-up (F₁ ∙ G₁) (F₂ ∙ G₂) I I⊨LHS))

    Iʳ₂⊨G₂ : down * (right * bnodes I f) ⊨a impl G₂
    Iʳ₂⊨G₂ = ⊨a-resp-≡³
      (right * down * I) (on-bnode f (ind I) ∘ right ∘ down) refl (impl G₂)
      (compose-right F₂ G₂ (down * I) (tensor-down (F₁ ∙ G₁) (F₂ ∙ G₂) I I⊨LHS))

    I⊨RHS : bnodes I f ⊨a impl ((F₁ ⟨⊗⟩ F₂) ∙ (G₁ ⟨⊗⟩ G₂))
    I⊨RHS = compose-resp-⊨a (F₁ ⟨⊗⟩ F₂) (G₁ ⟨⊗⟩ G₂) (bnodes I f)
      (tensor-resp-⊨a F₁ F₂ (left * bnodes I f) Iˡ₁⊨F₁ Iˡ₂⊨F₂)
      (tensor-resp-⊨a G₁ G₂ (right * bnodes I f) Iʳ₁⊨G₁ Iʳ₂⊨G₂)

  RHS⊑LHS : (F₁ ⟨⊗⟩ F₂) ∙ (G₁ ⟨⊗⟩ G₂) ⊑ (F₁ ∙ G₁) ⟨⊗⟩ (F₂ ∙ G₂)
  RHS⊑LHS I I⊨STA₁A₂ I⊨RHS = (f , I⊨LHS) where

    f : ((BN F₁ ⊕ IN B₁ ⊕ BN G₁) ⊎ (BN F₂ ⊕ IN B₂ ⊕ BN G₂)) → Δ ⌊ I ⌋
    f (inj₁ (inode v)) = ind I (bnode (inode (inj₁ v)))
    f (inj₁ (bnode y)) = ind I (bnode (bnode (inj₁ y)))
    f (inj₁ (enode w)) = ind I (bnode (enode (inj₁ w)))
    f (inj₂ (inode v)) = ind I (bnode (inode (inj₂ v)))
    f (inj₂ (bnode y)) = ind I (bnode (bnode (inj₂ y)))
    f (inj₂ (enode w)) = ind I (bnode (enode (inj₂ w)))

    I₁ˡ⊨F₁ : left * up * bnodes I f ⊨a impl F₁
    I₁ˡ⊨F₁ = ⊨a-resp-≡³
      (up * left * I) (on-bnode f (ind I) ∘ up ∘ left) refl (impl F₁)
      (tensor-up F₁ F₂ (left * I) (compose-left (F₁ ⟨⊗⟩ F₂) (G₁ ⟨⊗⟩ G₂) I I⊨RHS))

    I₁ʳ⊨G₁ : right * up * bnodes I f ⊨a impl G₁
    I₁ʳ⊨G₁ = ⊨a-resp-≡³
      (up * right * I) (on-bnode f (ind I) ∘ up ∘ right) refl (impl G₁)
      (tensor-up G₁ G₂ (right * I) (compose-right (F₁ ⟨⊗⟩ F₂) (G₁ ⟨⊗⟩ G₂) I I⊨RHS))

    I₂ˡ⊨F₂ : left * down * bnodes I f ⊨a impl F₂
    I₂ˡ⊨F₂ = ⊨a-resp-≡³
      (down * left * I) (on-bnode f (ind I) ∘ down ∘ left) refl (impl F₂)
      (tensor-down F₁ F₂ (left * I) (compose-left (F₁ ⟨⊗⟩ F₂) (G₁ ⟨⊗⟩ G₂) I I⊨RHS))

    I₂ʳ⊨G₂ : right * down * bnodes I f ⊨a impl G₂
    I₂ʳ⊨G₂ = ⊨a-resp-≡³
      (down * right * I) (on-bnode f (ind I) ∘ down ∘ right) refl (impl G₂)
      (tensor-down G₁ G₂ (right * I) (compose-right (F₁ ⟨⊗⟩ F₂) (G₁ ⟨⊗⟩ G₂) I I⊨RHS))

    I⊨LHS : bnodes I f ⊨a impl ((F₁ ∙ G₁) ⟨⊗⟩ (F₂ ∙ G₂))
    I⊨LHS = tensor-resp-⊨a (F₁ ∙ G₁) (F₂ ∙ G₂) (bnodes I f)
      (compose-resp-⊨a F₁ G₁ (up * bnodes I f) I₁ˡ⊨F₁ I₁ʳ⊨G₁)
      (compose-resp-⊨a F₂ G₂ (down * bnodes I f) I₂ˡ⊨F₂ I₂ʳ⊨G₂)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


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

module Fragment.Examples.Semigroup.Arith.Reasoning where

open import Fragment.Examples.Semigroup.Arith.Base

+-direct : ∀ {m n} → (m + 2) + (3 + n) ≡ m + (5 + n)
+-direct {m} {n} = begin
    (m + 2) + (3 + n)
  ≡⟨ fragment SemigroupFrex +-semigroup ⟩
    m + (5 + n)
  ∎

open import Data.Nat.Properties using (*-distribˡ-+)

+-inner : ∀ {m n k} → k * (m + 2) + k * (3 + n) ≡ k * (m + 5 + n)
+-inner {m} {n} {k} = begin
    k * (m + 2) + k * (3 + n)
  ≡⟨ sym (*-distribˡ-+ k (m + 2) (3 + n)) ⟩
    k * ((m + 2) + (3 + n))
  ≡⟨ cong (k *_) (fragment SemigroupFrex +-semigroup) ⟩
    k * (m + 5 + n)
  ∎


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

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

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

data  In2   : Set  where
   i0 : In2
   i1 : In2

record NAutomaton ( Q : Set ) ( Σ : Set  )
       : Set  where
    field
          Nδ : Q → Σ → Q → Bool
          Nend  :  Q → Bool

open NAutomaton

LStates1 : List States1
LStates1 = sr ∷ ss ∷ st ∷ []

-- one of qs q is true
existsS1 : ( States1 → Bool ) → Bool
existsS1 qs = qs sr \/ qs ss \/ qs st

-- extract list of q which qs q is true
to-listS1 : ( States1 → Bool ) → List States1
to-listS1 qs = ss1 LStates1 where
   ss1 : List States1 → List States1
   ss1 [] = []
   ss1 (x ∷ t) with qs x
   ... | true   = x ∷ ss1 t
   ... | false  = ss1 t

Nmoves : { Q : Set } { Σ : Set  }
    → NAutomaton Q  Σ
    → (exists : ( Q → Bool ) → Bool)
    →  ( Qs : Q → Bool )  → (s : Σ ) → ( Q → Bool )
Nmoves {Q} { Σ} M exists  Qs  s  = λ q → exists ( λ qn → (Qs qn /\ ( Nδ M qn s q )  ))

Naccept : { Q : Set } { Σ : Set  }
    → NAutomaton Q  Σ
    → (exists : ( Q → Bool ) → Bool)
    → (Nstart : Q → Bool) → List  Σ → Bool
Naccept M exists sb []  = exists ( λ q → sb q /\ Nend M q )
Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q →  exists ( λ qn → (sb qn /\ ( Nδ M qn i q )  ))) t

{-# TERMINATING #-}
NtraceDepth : { Q : Set } { Σ : Set  }
    → NAutomaton Q  Σ
    → (Nstart : Q → Bool) → List Q  → List  Σ → List (List ( Σ ∧ Q ))
NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where
    ndepth : List Q → (q : Q → Bool ) → List Σ  → List ( Σ ∧ Q )  →  List (List ( Σ ∧ Q )  ) →  List (List ( Σ ∧ Q )  )
    ndepth1 : Q → Σ → List Q →  List Σ  → List ( Σ ∧ Q )  →  List ( List ( Σ ∧ Q )) →  List ( List ( Σ ∧ Q ))
    ndepth1 q i [] is t t1 = t1
    ndepth1 q i (x ∷ qns) is t t1 =  ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 )
    ndepth [] sb is t t1 =  t1
    ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q
    ... | true =  ndepth qs sb [] t ( t  ∷ t1 )
    ... | false =  ndepth qs sb [] t t1
    ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q
    ... | true  = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 )
    ... | false = ndepth qs sb (i ∷ is) t t1

-- trace in state set
--
Ntrace : { Q : Set } { Σ : Set  }
    → NAutomaton Q  Σ
    → (exists : ( Q → Bool ) → Bool)
    → (to-list : ( Q → Bool ) → List Q )
    → (Nstart : Q → Bool) → List  Σ → List (List Q)
Ntrace M exists to-list sb []  = to-list ( λ q → sb q /\ Nend M q ) ∷ []
Ntrace M exists to-list sb (i ∷ t ) =
    to-list (λ q →  sb q ) ∷
    Ntrace M exists to-list (λ q →  exists ( λ qn → (sb qn /\ ( Nδ M qn i q )  ))) t

data-fin-00 : ( Fin 3 ) → Bool
data-fin-00 zero = true
data-fin-00 (suc zero) = true
data-fin-00 (suc (suc zero)) = true
data-fin-00 (suc (suc (suc ())))

data-fin-01 :  (x : ℕ ) → x < 3 → Bool
data-fin-01 zero lt = true
data-fin-01 (suc zero) lt = true
data-fin-01 (suc (suc zero)) lt = true
data-fin-01 (suc (suc (suc x))) (s≤s (s≤s (s≤s ())))

transition3 : States1  → In2  → States1 → Bool
transition3 sr i0 sr = true
transition3 sr i1 ss = true
transition3 sr i1 sr = true
transition3 ss i0 sr = true
transition3 ss i1 st = true
transition3 st i0 sr = true
transition3 st i1 st = true
transition3 _ _ _ = false

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

test5 = existsS1  (λ q → fin1 q )
test6 = to-listS1 (λ q → fin1 q )

start1 : States1 → Bool
start1 sr = true
start1 _ = false

am2  :  NAutomaton  States1 In2
am2  =  record { Nδ = transition3 ; Nend = fin1}

example2-1 = Naccept am2 existsS1 start1 ( i0  ∷ i1  ∷ i0  ∷ [] )
example2-2 = Naccept am2 existsS1 start1 ( i1  ∷ i1  ∷ i1  ∷ [] )

t-1 : List ( List States1 )
t-1 = Ntrace am2 existsS1 to-listS1 start1 ( i1  ∷ i1  ∷ i1  ∷ [] )  -- (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ (sr ∷ ss ∷ st ∷ []) ∷ (st ∷ []) ∷ []
t-2 = Ntrace am2 existsS1 to-listS1 start1 ( i0  ∷ i1  ∷ i0  ∷ [] )  -- (sr ∷ []) ∷ (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ [] ∷ []
t-3 = NtraceDepth am2 start1 LStates1 ( i1  ∷ i1  ∷ i1  ∷ [] )
t-4 = NtraceDepth am2 start1 LStates1 ( i0  ∷ i1  ∷ i0  ∷ [] )
t-5 = NtraceDepth am2 start1 LStates1 ( i0  ∷ i1 ∷ [] )

transition4 : States1  → In2  → States1 → Bool
transition4 sr i0 sr = true
transition4 sr i1 ss = true
transition4 sr i1 sr = true
transition4 ss i0 ss = true
transition4 ss i1 st = true
transition4 st i0 st = true
transition4 st i1 st = true
transition4 _ _ _ = false

fin4 :  States1  → Bool
fin4 st = true
fin4 _ = false

start4 : States1 → Bool
start4 ss = true
start4 _ = false

am4  :  NAutomaton  States1 In2
am4  =  record { Nδ = transition4 ; Nend = fin4}

example4-1 = Naccept am4 existsS1 start4 ( i0  ∷ i1  ∷ i1  ∷ i0 ∷ [] )
example4-2 = Naccept am4 existsS1 start4 ( i0  ∷ i1  ∷ i1  ∷ i1 ∷ [] )

fin0 :  States1  → Bool
fin0 st = false
fin0 ss = false
fin0 sr = false

test0 : Bool
test0 = existsS1 fin0

test1 : Bool
test1 = existsS1 fin1

test2 = Nmoves am2 existsS1 start1

open import automaton

am2def  :  Automaton (States1 → Bool )  In2
am2def  =  record { δ    = λ qs s q → existsS1 (λ qn → qs q /\ Nδ am2 q s qn )
                  ; aend = λ qs     → existsS1 (λ q → qs q /\ Nend am2  q) }

dexample4-1 = accept am2def start1 ( i0  ∷ i1  ∷ i1  ∷ i0 ∷ [] )
texample4-1 = trace am2def start1 ( i0  ∷ i1  ∷ i1  ∷ i0 ∷ [] )

-- LStates1 contains all states in States1

-- a list of Q contains (q : Q)

eqState1? : (x y : States1)  →  Dec ( x ≡ y )
eqState1? sr sr = yes refl
eqState1? ss ss = yes refl
eqState1? st st = yes refl
eqState1? sr ss = no (λ ())
eqState1? sr st = no (λ ())
eqState1? ss sr = no (λ ())
eqState1? ss st = no (λ ())
eqState1? st sr = no (λ ())
eqState1? st ss = no (λ ())

list-contains  : {Q : Set} → ( (x y : Q ) → Dec ( x ≡ y ) ) → (qs : List Q) → (q : Q ) → Bool
list-contains {Q} eq? [] q = false
list-contains {Q} eq? (x ∷ qs) q with eq? x q
... | yes _  = true
... | no _  = list-contains eq? qs q

containsP : {Q : Set} → ( eq? : (x y : Q ) →  Dec ( x ≡ y ))  → (qs : List Q) → (q : Q ) → Set
containsP eq? qs q = list-contains eq? qs q ≡ true

contains-all : (q : States1 ) → containsP eqState1? LStates1 q
contains-all sr = refl
contains-all ss = refl
contains-all st = refl

-- foldr : (A → B → B) → B → List A → B
-- foldr c n []       = n
-- foldr c n (x ∷ xs) = c x (foldr c n xs)

ssQ : {Q : Set } ( qs : Q → Bool ) → List Q → List Q
ssQ qs [] = []
ssQ qs (x ∷ t) with qs x
... | true   = x ∷ ssQ qs t
... | false  = ssQ qs t

bool-t1 : {b : Bool } → b ≡ true → (true /\ b)  ≡ true
bool-t1 refl = refl

bool-1t : {b : Bool } → b ≡ true → (b /\ true)  ≡ true
bool-1t refl = refl

to-list1 : {Q : Set } (qs : Q → Bool ) →  (all : List Q) → foldr (λ q x → qs q /\ x ) true (ssQ  qs all ) ≡ true
to-list1 qs []  = refl
to-list1 qs (x ∷ all)  with qs x  | inspect qs x
... | false | record { eq = eq } = to-list1 qs all
... | true  | record { eq = eq } = subst (λ k → k /\ foldr (λ q → _/\_ (qs q)) true (ssQ qs all) ≡ true ) (sym eq) ( bool-t1 (to-list1 qs all) )

existsS1-valid : ¬ ( (qs : States1 → Bool ) →  ( existsS1 qs ≡ true ) )
existsS1-valid n = ¬-bool refl ( n ( λ x → false ))

--
--  using finiteSet
--

open import finiteSet
open import finiteSetUtil
open FiniteSet

allQ : {Q : Set } (finq : FiniteSet Q) → List Q
allQ {Q} finq = to-list finq (λ x → true)

existQ : {Q : Set } (finq : FiniteSet Q) → (Q → Bool) → Bool
existQ finq qs = exists finq qs

eqQ? : {Q : Set } (finq : FiniteSet Q) → (x y : Q ) → Bool
eqQ? finq x y = equal? finq x y

finState1 : FiniteSet States1
finState1 = record {
     finite = finite0
   ; Q←F = Q←F0
   ; F←Q = F←Q0
   ; finiso→ = finiso→0
   ; finiso← = finiso←0
 } where
     finite0 : ℕ
     finite0 = 3
     Q←F0 : Fin finite0 → States1
     Q←F0 zero = sr
     Q←F0 (suc zero) = ss
     Q←F0 (suc (suc zero)) = st
     F←Q0 : States1 → Fin finite0
     F←Q0 sr = # 0
     F←Q0 ss = # 1
     F←Q0 st = # 2
     finiso→0 : (q : States1) → Q←F0 ( F←Q0 q ) ≡ q
     finiso→0 sr = refl
     finiso→0 ss = refl
     finiso→0 st = 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

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:
module Acme.Type where

open import Agda.Builtin.Bool using (Bool; true; false) public
open import Agda.Builtin.Char using (Char)
  renaming (primCharEquality to _==_) public
open import Agda.Builtin.Equality using (_≡_; refl) public
open import Agda.Builtin.List using (List; []; _∷_) public
open import Agda.Builtin.String using (String)
  renaming (primStringToList to unpack) public
open import Agda.Builtin.Unit using (⊤; tt) public
open import Agda.Builtin.TrustMe using ()
  renaming (primTrustMe to trustMe) public

Type : Set
Type = List Char → Bool

data ⊥ : Set where

IsTrue : Bool → Set
IsTrue true = ⊤
IsTrue false = ⊥

_∈_ : List Char → Type → Set
x ∈ A = IsTrue (A x)

record Elt (A : Type) : Set where
  constructor [_]
  field value     : List Char
        @0 {{check}} : value ∈ A
open Elt public

infix 100 _∋_
_∋_ : (A : Type) (str : String) → {{unpack str ∈ A}} → Elt A
A ∋ str = record { value = unpack str }

infixr 3 _&&_
_&&_ : Bool → Bool → Bool
true && b = b
false && b = false

infixr 2 _||_
_||_ : Bool → Bool → Bool
true || b = true
false || b = b

isNil : List Char → Bool
isNil [] = true
isNil _ = false

data Reflects (a : Char) : Char → Bool → Set where
  true  : Reflects a a true
  false : ∀ {b} → Reflects a b false

mkTrue : ∀ {a b} → a ≡ b → Reflects a b true
mkTrue refl = true

_≟_ : (a b : Char) → Reflects a b (a == b)
a ≟ b with a == b
... | false = false
... | true  = mkTrue trustMe

private

  variable
    A B : Set
    x y z : A

cong : (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

sym : x ≡ y → y ≡ x
sym refl = refl

trans : x ≡ y → y ≡ z → x ≡ z
trans refl eq = eq

max_stars_repo_name: gallais/STRINaGda

max_issues_repo_name: gallais/STRINaGda

max_forks_repo_name: gallais/STRINaGda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed binary relations
------------------------------------------------------------------------

-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Heterogeneous`.

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

module Relation.Binary.Indexed.Heterogeneous.Bundles where

open import Function.Base
open import Level using (suc; _⊔_)
open import Relation.Binary using (_⇒_)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
open import Relation.Binary.Indexed.Heterogeneous.Core
open import Relation.Binary.Indexed.Heterogeneous.Structures

------------------------------------------------------------------------
-- Definitions

record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
  infix 4 _≈_
  field
    Carrier       : I → Set c
    _≈_           : IRel Carrier ℓ
    isEquivalence : IsIndexedEquivalence Carrier _≈_

  open IsIndexedEquivalence isEquivalence public

record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ :
                       Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _∼_
  field
    Carrier    : I → Set c
    _≈_        : IRel Carrier ℓ₁  -- The underlying equality.
    _∼_        : IRel Carrier ℓ₂  -- The relation.
    isPreorder : IsIndexedPreorder Carrier _≈_ _∼_

  open IsIndexedPreorder isPreorder public


text:
-- Partly based on code due to Andrea Vezzosi.

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

open import Agda.Builtin.Bool

data D : Set where
  run-time        : Bool → D
  @0 compile-time : Bool → D

g : D → D
g (run-time x)     = run-time x
g (compile-time x) = compile-time x

h : D → @0 D → D
h (run-time x)     _                = run-time x
h (compile-time x) (run-time y)     = compile-time y
h (compile-time x) (compile-time y) = compile-time x

i : @0 D → D → D
i _                (run-time y)     = run-time y
i (run-time x)     (compile-time y) = compile-time x
i (compile-time x) (compile-time y) = compile-time y

data E (@0 A : Set) : Set where
  c₁ c₂ : E A
  @0 c₃ : A → E A

m : {@0 A : Set} → @0 A → E A → E A
m _ c₁     = c₂
m _ c₂     = c₁
m x (c₃ _) = c₃ x


text:
open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Reflection

postulate
  foo : Set

macro
  bar : Term → TC ⊤
  bar = unify (def (quote foo) [])

test : Set
test = {!bar!}

max_forks_repo_name: shlevy/agda


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

open import LogicalFormulae
open import Categories.Definition

module Categories.Dual.Definition where

dual : {a b : _} → Category {a} {b} → Category {a} {b}
dual record { objects = objects ; arrows = arrows ; id = id ; _∘_ = _∘_ ; rightId = rightId ; leftId = leftId ; compositionAssociative = associative } = record { objects = objects ; arrows = λ i j → arrows j i ; id = id ; _∘_ = λ {x y z} g f → f ∘ g ; rightId = λ {x y} f → leftId f ; leftId = λ {x y} f → rightId f ; compositionAssociative = λ {x y z w} f g h → equalityCommutative (associative h g f) }


text:
---------------------------------------------
-- Consequences of the axiom of regularity
---------------------------------------------
{-# OPTIONS --allow-unsolved-meta #-}

module sv20.assign2.SetTheory.Regularity where

open import sv20.assign2.SetTheory.Logic
open import sv20.assign2.SetTheory.Algebra
open import sv20.assign2.SetTheory.Subset
open import sv20.assign2.SetTheory.ZAxioms
open import sv20.assign2.SetTheory.Pairs

-- Theorem 105, p. 54
A∉A : (A : 𝓢) → A ∉ A
A∉A A h = cont _ (p₄ , notEmpty)
  where
  A∈Aₛ : A ∈ singleton A
  A∈Aₛ = singletonp₂ A

  A∈Aₛ∩A : A ∈ (singleton A ∩ A)
  A∈Aₛ∩A = ∩-d₂ _ _ _ (A∈Aₛ , h)

  notEmpty : (singleton A ∩ A) ≢ ∅
  notEmpty = prop-∅ A _ A∈Aₛ∩A

  Aₛ≢∅ : singleton A ≢ ∅
  Aₛ≢∅ x = prop-∅ _ _ A∈Aₛ x

  reg-step : ∃ (λ x → x ∈ singleton A ∧ ((y : 𝓢) → y ∈ x → y ∉ singleton A))
  reg-step = reg (singleton A) Aₛ≢∅

  aux : 𝓢
  aux = proj₁ reg-step

  aux-p : aux ∈ singleton A ∧ ((y : 𝓢) → y ∈ aux → y ∉ singleton A)
  aux-p = proj₂ _ reg-step

  p : aux ∈ singleton A
  p = ∧-proj₁ aux-p

  aux∈auxₛ : aux ∈ singleton aux
  aux∈auxₛ = singletonp₂ aux

  prop : A ∈ singleton aux → A ∩ singleton aux ≡ ∅
  prop = singletonp₄ A aux

  prop₂ : aux ≡ A
  prop₂ = singletonp _ p

  imp : A ∩ singleton aux ≡ ∅
  imp = prop (subs (λ w → w ∈ singleton aux) (prop₂) aux∈auxₛ)

  p₃ : singleton aux ∩ A ≡ ∅
  p₃ = subs (λ w → w ≡ ∅) (∩-sym _ _) imp

  p₄ : singleton A ∩ A ≡ ∅
  p₄ = subs (λ w → singleton w ∩ A ≡ ∅) prop₂ p₃

reg-cons : (A B : 𝓢) → ¬ (A ∈ B ∧ B ∈ A)
reg-cons A B h = {!!}
  where
  p₁ : A ∈ A ₚ B
  p₁ = pair-d₂ _ _ (inj₁ refl)

  p₂ : A ∈ B
  p₂ = ∧-proj₁ h

  p₃ : A ∈ A ₚ B ∩ B
  p₃ = ∩-d₂ _ _ _ (p₁ , p₂)

  p₄ : (A ₚ B) ≢ ∅
  p₄ = prop-∅ _ _ p₁

  reg-step : ∃ (λ x → x ∈ A ₚ B ∧ ((y : 𝓢) → y ∈ x → y ∉ A ₚ B))
  reg-step = {!!}

  x : 𝓢
  x = proj₁ reg-step

  x-p : x ∈ A ₚ B ∧ ((y : 𝓢) → y ∈ x → y ∉ A ₚ B)
  x-p = proj₂ _ reg-step

  p₆ : (A ₚ B ∩ x) ≡ ∅
  p₆ = {!!}

  p₇ : x ∈ A ₚ B
  p₇ = ∧-proj₁ x-p

  p₈ : x ≡ A ∨ x ≡ B
  p₈ = pair-d₁ _ _ p₇

-- References
--
-- Suppes, Patrick (1960). Axiomatic Set Theory.
-- The University Series in Undergraduate Mathematics.
-- D. Van Nostrand Company, inc.
--
-- Enderton, Herbert B. (1977). Elements of Set Theory.
-- Academic Press Inc.


text:
module FFI.Data.Scientific where

{-# FOREIGN GHC import qualified Data.Scientific #-}

postulate Scientific : Set
{-# COMPILE GHC Scientific = type Data.Scientific.Scientific #-}

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


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

open import lib.Basics
open import lib.NType2
open import lib.types.Int
open import lib.types.Group
open import lib.types.List
open import lib.types.Word
open import lib.groups.Homomorphism
open import lib.groups.Isomorphism
open import lib.groups.FreeAbelianGroup
open import lib.types.SetQuotient

module lib.groups.Int where

ℤ-group-structure : GroupStructure ℤ
ℤ-group-structure = record
  { ident = 0
  ; inv = ℤ~
  ; comp = _ℤ+_
  ; unit-l = ℤ+-unit-l
  ; assoc = ℤ+-assoc
  ; inv-l = ℤ~-inv-l
  }

ℤ-group : Group₀
ℤ-group = group _ ℤ-group-structure

ℤ-group-is-abelian : is-abelian ℤ-group
ℤ-group-is-abelian = ℤ+-comm

ℤ-abgroup : AbGroup₀
ℤ-abgroup = ℤ-group , ℤ-group-is-abelian

ℤ-iso-FreeAbGroup-Unit : ℤ-group ≃ᴳ FreeAbGroup.grp Unit
ℤ-iso-FreeAbGroup-Unit = ≃-to-≃ᴳ (equiv to from to-from from-to) to-pres-comp where
  to = FreeAbGroup.exp Unit fs[ inl unit :: nil ]
  from = FormalSum-extend ℤ-abgroup (λ _ → 1)
  abstract
    to-pres-comp = FreeAbGroup.exp-+ Unit fs[ inl unit :: nil ]

    to-from' : ∀ l → to (Word-extendᴳ ℤ-group (λ _ → 1) l) == fs[ l ]
    to-from' nil = idp
    to-from' (inl unit :: l) =
        FreeAbGroup.exp-succ Unit fs[ inl unit :: nil ] (Word-extendᴳ ℤ-group (λ _ → 1) l)
      ∙ ap (FreeAbGroup.comp Unit fs[ inl unit :: nil ]) (to-from' l)
    to-from' (inr unit :: l) =
        FreeAbGroup.exp-pred Unit fs[ inl unit :: nil ] (Word-extendᴳ ℤ-group (λ _ → 1) l)
      ∙ ap (FreeAbGroup.comp Unit fs[ inr unit :: nil ]) (to-from' l)

    to-from : ∀ fs → to (from fs) == fs
    to-from = FormalSum-elim to-from' (λ _ → prop-has-all-paths-↓)

    from-to : ∀ z → from (to z) == z
    from-to (pos 0) = idp
    from-to (pos 1) = idp
    from-to (negsucc 0) = idp
    from-to (pos (S (S n))) =
        GroupHom.pres-comp (FreeAbGroup-extend ℤ-abgroup (λ _ → 1))
          fs[ inl unit :: nil ] (FreeAbGroup.exp Unit fs[ inl unit :: nil ] (pos (S n)))
      ∙ ap succ (from-to (pos (S n)))
    from-to (negsucc (S n)) =
        GroupHom.pres-comp (FreeAbGroup-extend ℤ-abgroup (λ _ → 1))
          fs[ inr unit :: nil ] (FreeAbGroup.exp Unit fs[ inl unit :: nil ] (negsucc n))
      ∙ ap pred (from-to (negsucc n))

exp-shom : ∀ {i} {GEl : Type i} (GS : GroupStructure GEl) (g : GEl) → ℤ-group-structure →ᴳˢ GS
exp-shom GS g = group-structure-hom (GroupStructure.exp GS g) (GroupStructure.exp-+ GS g)

exp-hom : ∀ {i} (G : Group i) (g : Group.El G) → ℤ-group →ᴳ G
exp-hom G g = group-hom (Group.exp G g) (Group.exp-+ G g)

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda