text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Colist type and some operations
------------------------------------------------------------------------

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

module Codata.Colist where

open import Level using (Level)
open import Size
open import Data.Unit
open import Data.Nat.Base
open import Data.Product using (_×_ ; _,_)
open import Data.These.Base using (These; this; that; these)
open import Data.Maybe.Base using (Maybe; nothing; just)
open import Data.List.Base using (List; []; _∷_)
open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
open import Data.Vec.Base as Vec using (Vec; []; _∷_)
open import Data.Vec.Bounded as Vec≤ using (Vec≤)
open import Function

open import Codata.Thunk using (Thunk; force)
open import Codata.Conat as Conat using (Conat ; zero ; suc)
open import Codata.Cowriter as CW using (Cowriter; _∷_)
open import Codata.Delay as Delay using (Delay ; now ; later)
open import Codata.Stream using (Stream ; _∷_)

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

private
  variable
    a b c w : Level
    i : Size
    A : Set a
    B : Set b
    C : Set c
    W : Set w

data Colist (A : Set a) (i : Size) : Set a where
  []  : Colist A i
  _∷_ : A → Thunk (Colist A) i → Colist A i

------------------------------------------------------------------------
-- Relationship to Cowriter.

fromCowriter : Cowriter W A i → Colist W i
fromCowriter CW.[ _ ] = []
fromCowriter (w ∷ ca) = w ∷ λ where .force → fromCowriter (ca .force)

toCowriter : Colist A i → Cowriter A ⊤ i
toCowriter []       = CW.[ _ ]
toCowriter (a ∷ as) = a ∷ λ where .force → toCowriter (as .force)

------------------------------------------------------------------------
-- Basic functions.

[_] : A → Colist A ∞
[ a ] = a ∷ λ where .force → []

length : Colist A i → Conat i
length []       = zero
length (x ∷ xs) = suc λ where .force → length (xs .force)

replicate : Conat i → A → Colist A i
replicate zero    a = []
replicate (suc n) a = a ∷ λ where .force → replicate (n .force) a

infixr 5 _++_ _⁺++_
_++_ : Colist A i → Colist A i → Colist A i
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ λ where .force → xs .force ++ ys

lookup : ℕ → Colist A ∞ → Maybe A
lookup n       []       = nothing
lookup zero    (a ∷ as) = just a
lookup (suc n) (a ∷ as) = lookup n (as .force)

colookup : Conat i → Colist A i → Delay (Maybe A) i
colookup n       []       = now nothing
colookup zero    (a ∷ as) = now (just a)
colookup (suc n) (a ∷ as) =
  later λ where .force → colookup (n .force) (as .force)

take : (n : ℕ) → Colist A ∞ → Vec≤ A n
take zero    xs       = Vec≤.[]
take n       []       = Vec≤.[]
take (suc n) (x ∷ xs) = x Vec≤.∷ take n (xs .force)

cotake : Conat i → Stream A i → Colist A i
cotake zero    xs       = []
cotake (suc n) (x ∷ xs) = x ∷ λ where .force → cotake (n .force) (xs .force)

drop : ℕ → Colist A ∞ → Colist A ∞
drop zero    xs       = xs
drop (suc n) []       = []
drop (suc n) (x ∷ xs) = drop n (xs .force)

fromList : List A → Colist A ∞
fromList []       = []
fromList (x ∷ xs) = x ∷ λ where .force → fromList xs

fromList⁺ : List⁺ A → Colist A ∞
fromList⁺ = fromList ∘′ List⁺.toList

_⁺++_ : List⁺ A → Thunk (Colist A) i → Colist A i
(x ∷ xs) ⁺++ ys = x ∷ λ where .force → fromList xs ++ ys .force

concat : Colist (List⁺ A) i → Colist A i
concat []         = []
concat (as ∷ ass) = as ⁺++ λ where .force → concat (ass .force)

fromStream : Stream A i → Colist A i
fromStream = cotake Conat.infinity

module ChunksOf (n : ℕ) where

  chunksOf : Colist A ∞ → Cowriter (Vec A n) (Vec≤ A n) i
  chunksOfAcc : ∀ m →
    -- We have two continuations but we are only ever going to use one.
    -- If we had linear types, we'd write the type using the & conjunction here.
    (k≤ : Vec≤ A m → Vec≤ A n) →
    (k≡ : Vec A m → Vec A n) →
    -- Finally we chop up the input stream.
    Colist A ∞ → Cowriter (Vec A n) (Vec≤ A n) i

  chunksOf = chunksOfAcc n id id

  chunksOfAcc zero    k≤ k≡ as       = k≡ [] ∷ λ where .force → chunksOf as
  chunksOfAcc (suc k) k≤ k≡ []       = CW.[ k≤ Vec≤.[] ]
  chunksOfAcc (suc k) k≤ k≡ (a ∷ as) =
    chunksOfAcc k (k≤ ∘ (a Vec≤.∷_)) (k≡ ∘ (a ∷_)) (as .force)

open ChunksOf using (chunksOf) public

-- Test to make sure that the values are kept in the same order
_ : chunksOf 3 (fromList (1 ∷ 2 ∷ 3 ∷ 4 ∷ []))
  ≡ (1 ∷ 2 ∷ 3 ∷ []) ∷ _
_ = refl

map : (A → B) → Colist A i → Colist B i
map f []       = []
map f (a ∷ as) = f a ∷ λ where .force → map f (as .force)

unfold : (A → Maybe (A × B)) → A → Colist B i
unfold next seed with next seed
... | nothing          = []
... | just (seed′ , b) = b ∷ λ where .force → unfold next seed′

scanl : (B → A → B) → B → Colist A i → Colist B i
scanl c n []       = n ∷ λ where .force → []
scanl c n (a ∷ as) = n ∷ λ where .force → scanl c (c n a) (as .force)

alignWith : (These A B → C) → Colist A i → Colist B i → Colist C i
alignWith f []         bs       = map (f ∘′ that) bs
alignWith f as@(_ ∷ _) []       = map (f ∘′ this) as
alignWith f (a ∷ as)   (b ∷ bs) =
  f (these a b) ∷ λ where .force → alignWith f (as .force) (bs .force)

zipWith : (A → B → C) → Colist A i → Colist B i → Colist C i
zipWith f []       bs       = []
zipWith f as       []       = []
zipWith f (a ∷ as) (b ∷ bs) =
  f a b ∷ λ where .force → zipWith f (as .force) (bs .force)

align : Colist A i → Colist B i → Colist (These A B) i
align = alignWith id

zip : Colist A i → Colist B i → Colist (A × B) i
zip = zipWith _,_

ap : Colist (A → B) i → Colist A i → Colist B i
ap = zipWith _$′_


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- The syntax of function types (Fig. 1a).
------------------------------------------------------------------------

module Parametric.Syntax.Type where

open import Base.Data.DependentList

-- This is a module in the Parametric.* hierarchy, so it defines
-- an extension point for plugins. In this case, the plugin can
-- choose the syntax for data types. We always provide a binding
-- called "Structure" that defines the type of the value that has
-- to be provided by the plugin. In this case, the plugin has to
-- provide a type, so we say "Structure = Set".

Structure : Set₁
Structure = Set

-- Here is the parametric module that defines the syntax of
-- simply types in terms of the syntax of base types. In the
-- Parametric.* hierarchy, we always call these parametric
-- modules "Structure". Note that in Agda, there is a separate
-- namespace for module names and for other bindings, so this
-- doesn't clash with the "Structure" above.
--
-- The idea behind all these structures is that the parametric
-- module lifts some structure of the plugin to the corresponding
-- structure in the full language. In this case, we lift the
-- structure of base types to the structure of simple types.
-- Maybe not the best choice of names, but it seemed clever at
-- the time.

module Structure (Base : Structure) where
  infixr 5 _⇒_

  -- A simple type is either a base type or a function types.
  -- Note that we can use our module parameter "Base" here just
  -- like any other type.
  data Type : Set where
    base : (ι : Base) → Type
    _⇒_ : (σ : Type) → (τ : Type) → Type

  -- We also provide the definitions of contexts of the newly
  -- defined simple types, variables as de Bruijn indices
  -- pointing into such a context, and sets of bound variables.
  open import Base.Syntax.Context Type public
  open import Base.Syntax.Vars Type public

  -- Internalize a context to a type.
  --
  -- Is there a better name for this function?
  internalizeContext : (Σ : Context) (τ′ : Type) → Type
  internalizeContext ∅ τ′ = τ′
  internalizeContext (τ • Σ) τ′ = τ ⇒ internalizeContext Σ τ′

ext: agda

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

open import Fragment.Algebra.Signature

module Fragment.Algebra.Free.Monad (Σ : Signature) where

open import Fragment.Algebra.Free.Base Σ
open import Fragment.Algebra.Algebra Σ
open import Fragment.Algebra.Homomorphism Σ using (_⟿_; Congruent; Homomorphic)
open import Fragment.Setoid.Morphism

open import Level using (Level)

open import Data.Vec using (Vec; []; _∷_; map)
open import Data.Vec.Relation.Binary.Pointwise.Inductive
  using (Pointwise; []; _∷_)

open import Relation.Binary using (Setoid)

private
  variable
    a b ℓ₁ ℓ₂ : Level

unit : ∀ {S : Setoid a ℓ₁} → S ↝ Herbrand S
unit = record { ∣_∣      = atom
              ; ∣_∣-cong = atom
              }

module _
  {A : Setoid a ℓ₁}
  {B : Setoid b ℓ₂}
  (f : A ↝ Herbrand B)
  where

  private

    open Setoid ∥ Free B ∥/≈

    module _ {A : Set a} {B : Set b} where

      mutual
        map-∣bind∣ : ∀ {n} → (A → Term B)
                 → Vec (Term A) n → Vec (Term B) n
        map-∣bind∣ f []       = []
        map-∣bind∣ f (x ∷ xs) = ∣bind∣ f x ∷ map-∣bind∣ f xs

        ∣bind∣ : (A → Term B) → Term A → Term B
        ∣bind∣ f (atom x)     = f x
        ∣bind∣ f (term op xs) = term op (map-∣bind∣ f xs)

    mutual
      map-∣bind∣-cong : ∀ {n} {xs ys : Vec ∥ Free A ∥ n}
                        → Pointwise (_~_ A) xs ys
                        → Pointwise (_~_ B) (map-∣bind∣ ∣ f ∣ xs)
                                            (map-∣bind∣ ∣ f ∣ ys)
      map-∣bind∣-cong []       = []
      map-∣bind∣-cong (p ∷ ps) = ∣bind∣-cong p ∷ map-∣bind∣-cong ps

      ∣bind∣-cong : Congruent (_~_ A) (_~_ B) (∣bind∣ ∣ f ∣)
      ∣bind∣-cong (atom p)                 = ∣ f ∣-cong p
      ∣bind∣-cong {x = term op _} (term p) = term (map-∣bind∣-cong p)

    map-∣bind∣≡map : ∀ {n} {xs : Vec ∥ Free A ∥ n}
                     → Pointwise (_~_ B) (map-∣bind∣ ∣ f ∣ xs)
                                         (map (∣bind∣ ∣ f ∣) xs)
    map-∣bind∣≡map {xs = []}     = []
    map-∣bind∣≡map {xs = x ∷ xs} = refl ∷ map-∣bind∣≡map

    ∣bind∣-hom : Homomorphic (Free A) (Free B) (∣bind∣ ∣ f ∣)
    ∣bind∣-hom op []       = refl
    ∣bind∣-hom op (x ∷ xs) = sym (term (map-∣bind∣≡map {xs = x ∷ xs}))

    ∣bind∣⃗ : Herbrand A ↝ Herbrand B
    ∣bind∣⃗ = record { ∣_∣      = ∣bind∣ ∣ f ∣
                     ; ∣_∣-cong = ∣bind∣-cong
                     }

  bind : Free A ⟿ Free B
  bind = record { ∣_∣⃗    = ∣bind∣⃗
                ; ∣_∣-hom = ∣bind∣-hom
                }

fmap : ∀ {A : Setoid a ℓ₁} {B : Setoid b ℓ₂}
       → A ↝ B
       → Free A ⟿ Free B
fmap f = bind (unit · f)

join : ∀ {A : Setoid a ℓ₁} → Free (Herbrand A) ⟿ Free A
join = bind id

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
module Star where

open import Prelude

infixr 40 _•_ _++_
infixl 30 _on_
infixr 20 _==>_ _=[_]=>_

data Star {X : Set} (R : Rel X) : Rel X where
  ε   : {x : X} -> Star R x x
  _•_ : {x y z : X} -> R x y -> Star R y z -> Star R x z

_++_ : {X : Set}{R : Rel X}{x y z : X} ->
       Star R x y -> Star R y z -> Star R x z
ε        ++ ys  =  ys
(x • xs) ++ ys  =  x • (xs ++ ys)

_==>_ : {X : Set} -> Rel X -> Rel X -> Set
R ==> S = forall {a b} -> R a b -> S a b

_on_ : {X Y : Set} -> (R : Rel X) -> (f : Y -> X) -> Rel Y
R on f = \a b -> R (f a) (f b)

_=[_]=>_ : {X Y : Set} (R : Rel X) (f : X -> Y) (S : Rel Y) -> Set
R =[ f ]=> S = R ==> S on f

return : {X : Set}{R : Rel X} -> R ==> Star R
return x = x • ε

module JoinMap where

  join : {X : Set}{R : Rel X} -> Star (Star R) ==> Star R
  join ε           =  ε
  join (xs • xss)  =  xs ++ join xss

  map : forall {X Y R S} -> (f : X -> Y) ->
        R =[ f ]=> S  ->  Star R =[ f ]=> Star S
  map f pm ε         =  ε
  map f pm (x • xs)  =  pm x • map f pm xs

  bind : forall {X Y R S} -> (f : X -> Y) ->
         R =[ f ]=> Star S  ->  Star R =[ f ]=> Star S
  bind f k m = join (map f k m)

bind : forall {X Y R S} -> (f : X -> Y) ->
        R =[ f ]=> Star S  ->  Star R =[ f ]=> Star S
bind f k ε         =  ε
bind f k (x • xs)  =  k x ++ bind f k xs

join : {X : Set}{R : Rel X} -> Star (Star R) ==> Star R
join = bind id id

map : forall {X Y R S} -> (f : X -> Y) ->
       R =[ f ]=> S  ->  Star R =[ f ]=> Star S
map f k = bind f (return · k)

-- Generic length

length : {X : Set}{R : Rel X} -> Star R =[ ! ]=> Star One
length = map ! !

-- Reverse

_op : {X : Set} -> Rel X -> Rel X
(R op) a b = R b a

reverse : {X : Set}{R : Rel X}{a b : X} -> Star R a b -> Star (R op) b a
reverse {X}{R} xs = rev xs ε
  where
    rev : forall {a b c} ->
          Star R a b -> Star (R op) a c -> Star (R op) b c
    rev ε ys = ys
    rev (x • xs) ys = rev xs (x • ys)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --copatterns #-}
module MixingCoPatternsAndCoConstructors where

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

module MStream where

  record Stream (A : Set) : Set where
    coinductive
    constructor _∷_
    field
      head : A
      tail : Stream A
  open Stream

  weird : (n : ℕ) → Stream ℕ
  head (weird zero)    = zero
  tail (weird zero)    = weird zero
  head (weird (suc n)) = n
  tail (weird (suc n)) = tail (weird n)

  weird' : (n : ℕ) → Stream ℕ
  head (weird' zero) = zero
  tail (weird' zero) = weird' zero
  weird' (suc n) = n ∷ tail (weird' n)

  -- BAD:
  weird'' : (n : ℕ) → Stream ℕ
  weird'' zero    = zero ∷ weird'' zero
  weird'' (suc n) = n ∷ tail (weird'' n)

  -- productive, but not strongly normalizing,
  -- should be rejected by termination checker:

  repeat : {A : Set}(a : A) → Stream A
  head (repeat a) = a
  tail (repeat a) = a ∷ tail (repeat a)

module Coinduction where

  import Common.Level
  open import Common.Coinduction

  record Stream (A : Set) : Set where
    inductive
    constructor _∷_
    field
      head : A
      tail : ∞ (Stream A)
  open Stream

  weird'' : (n : ℕ) → Stream ℕ
  weird'' zero    = zero ∷ (♯ weird'' zero)
  weird'' (suc n) = n ∷ tail (weird'' n)

module CoList where

  mutual

    data CoList (A : Set) : Set where
      []  : CoList A
      _∷_ : (x : A)(xs : CoList∞ A) → CoList A

    record CoList∞ (A : Set) : Set where
      coinductive
      constructor delay
      field
        force : CoList A

  open CoList∞

  downFrom : (n : ℕ) → CoList ℕ
  downFrom zero    = []
  downFrom (suc n) = n ∷ delay (downFrom n)

  down : (n : ℕ) → CoList∞ ℕ
  force (down zero)    = []
  force (down (suc n)) = n ∷ delay (force (down n))
    -- weird detour: delay (force ... to test termination checker

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module cws where

open import lib

open import cws-types public
----------------------------------------------------------------------------------
-- Run-rewriting rules
----------------------------------------------------------------------------------

data gratr2-nt : Set where
  _ws-plus-67 : gratr2-nt
  _ws : gratr2-nt
  _start : gratr2-nt
  _posinfo : gratr2-nt
  _otherpunct-bar-58 : gratr2-nt
  _otherpunct-bar-57 : gratr2-nt
  _otherpunct-bar-56 : gratr2-nt
  _otherpunct-bar-55 : gratr2-nt
  _otherpunct-bar-54 : gratr2-nt
  _otherpunct-bar-53 : gratr2-nt
  _otherpunct-bar-52 : gratr2-nt
  _otherpunct-bar-51 : gratr2-nt
  _otherpunct-bar-50 : gratr2-nt
  _otherpunct-bar-49 : gratr2-nt
  _otherpunct-bar-48 : gratr2-nt
  _otherpunct-bar-47 : gratr2-nt
  _otherpunct-bar-46 : gratr2-nt
  _otherpunct-bar-45 : gratr2-nt
  _otherpunct-bar-44 : gratr2-nt
  _otherpunct-bar-43 : gratr2-nt
  _otherpunct-bar-42 : gratr2-nt
  _otherpunct-bar-41 : gratr2-nt
  _otherpunct-bar-40 : gratr2-nt
  _otherpunct-bar-39 : gratr2-nt
  _otherpunct-bar-38 : gratr2-nt
  _otherpunct-bar-37 : gratr2-nt
  _otherpunct-bar-36 : gratr2-nt
  _otherpunct-bar-35 : gratr2-nt
  _otherpunct-bar-34 : gratr2-nt
  _otherpunct-bar-33 : gratr2-nt
  _otherpunct-bar-32 : gratr2-nt
  _otherpunct-bar-31 : gratr2-nt
  _otherpunct-bar-30 : gratr2-nt
  _otherpunct-bar-29 : gratr2-nt
  _otherpunct-bar-28 : gratr2-nt
  _otherpunct-bar-27 : gratr2-nt
  _otherpunct-bar-26 : gratr2-nt
  _otherpunct-bar-25 : gratr2-nt
  _otherpunct-bar-24 : gratr2-nt
  _otherpunct-bar-23 : gratr2-nt
  _otherpunct-bar-22 : gratr2-nt
  _otherpunct-bar-21 : gratr2-nt
  _otherpunct-bar-20 : gratr2-nt
  _otherpunct-bar-19 : gratr2-nt
  _otherpunct-bar-18 : gratr2-nt
  _otherpunct-bar-17 : gratr2-nt
  _otherpunct-bar-16 : gratr2-nt
  _otherpunct-bar-15 : gratr2-nt
  _otherpunct-bar-14 : gratr2-nt
  _otherpunct-bar-13 : gratr2-nt
  _otherpunct-bar-12 : gratr2-nt
  _otherpunct : gratr2-nt
  _numpunct-bar-9 : gratr2-nt
  _numpunct-bar-8 : gratr2-nt
  _numpunct-bar-7 : gratr2-nt
  _numpunct-bar-6 : gratr2-nt
  _numpunct-bar-11 : gratr2-nt
  _numpunct-bar-10 : gratr2-nt
  _numpunct : gratr2-nt
  _numone-range-4 : gratr2-nt
  _numone : gratr2-nt
  _num-plus-5 : gratr2-nt
  _num : gratr2-nt
  _nonws-plus-70 : gratr2-nt
  _nonws : gratr2-nt
  _entity : gratr2-nt
  _entities : gratr2-nt
  _comment-star-64 : gratr2-nt
  _comment : gratr2-nt
  _aws-bar-66 : gratr2-nt
  _aws-bar-65 : gratr2-nt
  _aws : gratr2-nt
  _anynonwschar-bar-69 : gratr2-nt
  _anynonwschar-bar-68 : gratr2-nt
  _anynonwschar : gratr2-nt
  _anychar-bar-63 : gratr2-nt
  _anychar-bar-62 : gratr2-nt
  _anychar-bar-61 : gratr2-nt
  _anychar-bar-60 : gratr2-nt
  _anychar-bar-59 : gratr2-nt
  _anychar : gratr2-nt
  _alpha-range-2 : gratr2-nt
  _alpha-range-1 : gratr2-nt
  _alpha-bar-3 : gratr2-nt
  _alpha : gratr2-nt

gratr2-nt-eq : gratr2-nt → gratr2-nt → 𝔹
gratr2-nt-eq  _ws-plus-67 _ws-plus-67 = tt
gratr2-nt-eq  _ws _ws = tt
gratr2-nt-eq  _start _start = tt
gratr2-nt-eq  _posinfo _posinfo = tt
gratr2-nt-eq  _otherpunct-bar-58 _otherpunct-bar-58 = tt
gratr2-nt-eq  _otherpunct-bar-57 _otherpunct-bar-57 = tt
gratr2-nt-eq  _otherpunct-bar-56 _otherpunct-bar-56 = tt
gratr2-nt-eq  _otherpunct-bar-55 _otherpunct-bar-55 = tt
gratr2-nt-eq  _otherpunct-bar-54 _otherpunct-bar-54 = tt
gratr2-nt-eq  _otherpunct-bar-53 _otherpunct-bar-53 = tt
gratr2-nt-eq  _otherpunct-bar-52 _otherpunct-bar-52 = tt
gratr2-nt-eq  _otherpunct-bar-51 _otherpunct-bar-51 = tt
gratr2-nt-eq  _otherpunct-bar-50 _otherpunct-bar-50 = tt
gratr2-nt-eq  _otherpunct-bar-49 _otherpunct-bar-49 = tt
gratr2-nt-eq  _otherpunct-bar-48 _otherpunct-bar-48 = tt
gratr2-nt-eq  _otherpunct-bar-47 _otherpunct-bar-47 = tt
gratr2-nt-eq  _otherpunct-bar-46 _otherpunct-bar-46 = tt
gratr2-nt-eq  _otherpunct-bar-45 _otherpunct-bar-45 = tt
gratr2-nt-eq  _otherpunct-bar-44 _otherpunct-bar-44 = tt
gratr2-nt-eq  _otherpunct-bar-43 _otherpunct-bar-43 = tt
gratr2-nt-eq  _otherpunct-bar-42 _otherpunct-bar-42 = tt
gratr2-nt-eq  _otherpunct-bar-41 _otherpunct-bar-41 = tt
gratr2-nt-eq  _otherpunct-bar-40 _otherpunct-bar-40 = tt
gratr2-nt-eq  _otherpunct-bar-39 _otherpunct-bar-39 = tt
gratr2-nt-eq  _otherpunct-bar-38 _otherpunct-bar-38 = tt
gratr2-nt-eq  _otherpunct-bar-37 _otherpunct-bar-37 = tt
gratr2-nt-eq  _otherpunct-bar-36 _otherpunct-bar-36 = tt
gratr2-nt-eq  _otherpunct-bar-35 _otherpunct-bar-35 = tt
gratr2-nt-eq  _otherpunct-bar-34 _otherpunct-bar-34 = tt
gratr2-nt-eq  _otherpunct-bar-33 _otherpunct-bar-33 = tt
gratr2-nt-eq  _otherpunct-bar-32 _otherpunct-bar-32 = tt
gratr2-nt-eq  _otherpunct-bar-31 _otherpunct-bar-31 = tt
gratr2-nt-eq  _otherpunct-bar-30 _otherpunct-bar-30 = tt
gratr2-nt-eq  _otherpunct-bar-29 _otherpunct-bar-29 = tt
gratr2-nt-eq  _otherpunct-bar-28 _otherpunct-bar-28 = tt
gratr2-nt-eq  _otherpunct-bar-27 _otherpunct-bar-27 = tt
gratr2-nt-eq  _otherpunct-bar-26 _otherpunct-bar-26 = tt
gratr2-nt-eq  _otherpunct-bar-25 _otherpunct-bar-25 = tt
gratr2-nt-eq  _otherpunct-bar-24 _otherpunct-bar-24 = tt
gratr2-nt-eq  _otherpunct-bar-23 _otherpunct-bar-23 = tt
gratr2-nt-eq  _otherpunct-bar-22 _otherpunct-bar-22 = tt
gratr2-nt-eq  _otherpunct-bar-21 _otherpunct-bar-21 = tt
gratr2-nt-eq  _otherpunct-bar-20 _otherpunct-bar-20 = tt
gratr2-nt-eq  _otherpunct-bar-19 _otherpunct-bar-19 = tt
gratr2-nt-eq  _otherpunct-bar-18 _otherpunct-bar-18 = tt
gratr2-nt-eq  _otherpunct-bar-17 _otherpunct-bar-17 = tt
gratr2-nt-eq  _otherpunct-bar-16 _otherpunct-bar-16 = tt
gratr2-nt-eq  _otherpunct-bar-15 _otherpunct-bar-15 = tt
gratr2-nt-eq  _otherpunct-bar-14 _otherpunct-bar-14 = tt
gratr2-nt-eq  _otherpunct-bar-13 _otherpunct-bar-13 = tt
gratr2-nt-eq  _otherpunct-bar-12 _otherpunct-bar-12 = tt
gratr2-nt-eq  _otherpunct _otherpunct = tt
gratr2-nt-eq  _numpunct-bar-9 _numpunct-bar-9 = tt
gratr2-nt-eq  _numpunct-bar-8 _numpunct-bar-8 = tt
gratr2-nt-eq  _numpunct-bar-7 _numpunct-bar-7 = tt
gratr2-nt-eq  _numpunct-bar-6 _numpunct-bar-6 = tt
gratr2-nt-eq  _numpunct-bar-11 _numpunct-bar-11 = tt
gratr2-nt-eq  _numpunct-bar-10 _numpunct-bar-10 = tt
gratr2-nt-eq  _numpunct _numpunct = tt
gratr2-nt-eq  _numone-range-4 _numone-range-4 = tt
gratr2-nt-eq  _numone _numone = tt
gratr2-nt-eq  _num-plus-5 _num-plus-5 = tt
gratr2-nt-eq  _num _num = tt
gratr2-nt-eq  _nonws-plus-70 _nonws-plus-70 = tt
gratr2-nt-eq  _nonws _nonws = tt
gratr2-nt-eq  _entity _entity = tt
gratr2-nt-eq  _entities _entities = tt
gratr2-nt-eq  _comment-star-64 _comment-star-64 = tt
gratr2-nt-eq  _comment _comment = tt
gratr2-nt-eq  _aws-bar-66 _aws-bar-66 = tt
gratr2-nt-eq  _aws-bar-65 _aws-bar-65 = tt
gratr2-nt-eq  _aws _aws = tt
gratr2-nt-eq  _anynonwschar-bar-69 _anynonwschar-bar-69 = tt
gratr2-nt-eq  _anynonwschar-bar-68 _anynonwschar-bar-68 = tt
gratr2-nt-eq  _anynonwschar _anynonwschar = tt
gratr2-nt-eq  _anychar-bar-63 _anychar-bar-63 = tt
gratr2-nt-eq  _anychar-bar-62 _anychar-bar-62 = tt
gratr2-nt-eq  _anychar-bar-61 _anychar-bar-61 = tt
gratr2-nt-eq  _anychar-bar-60 _anychar-bar-60 = tt
gratr2-nt-eq  _anychar-bar-59 _anychar-bar-59 = tt
gratr2-nt-eq  _anychar _anychar = tt
gratr2-nt-eq  _alpha-range-2 _alpha-range-2 = tt
gratr2-nt-eq  _alpha-range-1 _alpha-range-1 = tt
gratr2-nt-eq  _alpha-bar-3 _alpha-bar-3 = tt
gratr2-nt-eq  _alpha _alpha = tt
gratr2-nt-eq _ _ = ff

open import rtn gratr2-nt

cws-start : gratr2-nt → 𝕃 gratr2-rule
cws-start _ws-plus-67 = (just "P197" , nothing , just _ws-plus-67 , inj₁ _aws :: inj₁ _ws-plus-67 :: []) :: (just "P196" , nothing , just _ws-plus-67 , inj₁ _aws :: []) :: []
cws-start _ws = (just "P198" , nothing , just _ws , inj₁ _ws-plus-67 :: []) :: []
cws-start _start = (just "File" , nothing , just _start , inj₁ _entities :: []) :: []
cws-start _posinfo = (just "Posinfo" , nothing , just _posinfo , []) :: []
cws-start _otherpunct-bar-58 = (just "P175" , nothing , just _otherpunct-bar-58 , inj₁ _otherpunct-bar-57 :: []) :: (just "P174" , nothing , just _otherpunct-bar-58 , inj₂ '|' :: []) :: []
cws-start _otherpunct-bar-57 = (just "P173" , nothing , just _otherpunct-bar-57 , inj₁ _otherpunct-bar-56 :: []) :: (just "P172" , nothing , just _otherpunct-bar-57 , inj₂ '□' :: []) :: []
cws-start _otherpunct-bar-56 = (just "P171" , nothing , just _otherpunct-bar-56 , inj₁ _otherpunct-bar-55 :: []) :: (just "P170" , nothing , just _otherpunct-bar-56 , inj₂ 'Π' :: []) :: []
cws-start _otherpunct-bar-55 = (just "P169" , nothing , just _otherpunct-bar-55 , inj₁ _otherpunct-bar-54 :: []) :: (just "P168" , nothing , just _otherpunct-bar-55 , inj₂ 'ι' :: []) :: []
cws-start _otherpunct-bar-54 = (just "P167" , nothing , just _otherpunct-bar-54 , inj₁ _otherpunct-bar-53 :: []) :: (just "P166" , nothing , just _otherpunct-bar-54 , inj₂ 'λ' :: []) :: []
cws-start _otherpunct-bar-53 = (just "P165" , nothing , just _otherpunct-bar-53 , inj₁ _otherpunct-bar-52 :: []) :: (just "P164" , nothing , just _otherpunct-bar-53 , inj₂ '∀' :: []) :: []
cws-start _otherpunct-bar-52 = (just "P163" , nothing , just _otherpunct-bar-52 , inj₁ _otherpunct-bar-51 :: []) :: (just "P162" , nothing , just _otherpunct-bar-52 , inj₂ 'π' :: []) :: []
cws-start _otherpunct-bar-51 = (just "P161" , nothing , just _otherpunct-bar-51 , inj₁ _otherpunct-bar-50 :: []) :: (just "P160" , nothing , just _otherpunct-bar-51 , inj₂ '★' :: []) :: []
cws-start _otherpunct-bar-50 = (just "P159" , nothing , just _otherpunct-bar-50 , inj₁ _otherpunct-bar-49 :: []) :: (just "P158" , nothing , just _otherpunct-bar-50 , inj₂ '☆' :: []) :: []
cws-start _otherpunct-bar-49 = (just "P157" , nothing , just _otherpunct-bar-49 , inj₁ _otherpunct-bar-48 :: []) :: (just "P156" , nothing , just _otherpunct-bar-49 , inj₂ '·' :: []) :: []
cws-start _otherpunct-bar-48 = (just "P155" , nothing , just _otherpunct-bar-48 , inj₁ _otherpunct-bar-47 :: []) :: (just "P154" , nothing , just _otherpunct-bar-48 , inj₂ '⇐' :: []) :: []
cws-start _otherpunct-bar-47 = (just "P153" , nothing , just _otherpunct-bar-47 , inj₁ _otherpunct-bar-46 :: []) :: (just "P152" , nothing , just _otherpunct-bar-47 , inj₂ '➔' :: []) :: []
cws-start _otherpunct-bar-46 = (just "P151" , nothing , just _otherpunct-bar-46 , inj₁ _otherpunct-bar-45 :: []) :: (just "P150" , nothing , just _otherpunct-bar-46 , inj₂ '➾' :: []) :: []
cws-start _otherpunct-bar-45 = (just "P149" , nothing , just _otherpunct-bar-45 , inj₁ _otherpunct-bar-44 :: []) :: (just "P148" , nothing , just _otherpunct-bar-45 , inj₂ '↑' :: []) :: []
cws-start _otherpunct-bar-44 = (just "P147" , nothing , just _otherpunct-bar-44 , inj₁ _otherpunct-bar-43 :: []) :: (just "P146" , nothing , just _otherpunct-bar-44 , inj₂ '●' :: []) :: []
cws-start _otherpunct-bar-43 = (just "P145" , nothing , just _otherpunct-bar-43 , inj₁ _otherpunct-bar-42 :: []) :: (just "P144" , nothing , just _otherpunct-bar-43 , inj₂ '(' :: []) :: []
cws-start _otherpunct-bar-42 = (just "P143" , nothing , just _otherpunct-bar-42 , inj₁ _otherpunct-bar-41 :: []) :: (just "P142" , nothing , just _otherpunct-bar-42 , inj₂ ')' :: []) :: []
cws-start _otherpunct-bar-41 = (just "P141" , nothing , just _otherpunct-bar-41 , inj₁ _otherpunct-bar-40 :: []) :: (just "P140" , nothing , just _otherpunct-bar-41 , inj₂ ':' :: []) :: []
cws-start _otherpunct-bar-40 = (just "P139" , nothing , just _otherpunct-bar-40 , inj₁ _otherpunct-bar-39 :: []) :: (just "P138" , nothing , just _otherpunct-bar-40 , inj₂ '.' :: []) :: []
cws-start _otherpunct-bar-39 = (just "P137" , nothing , just _otherpunct-bar-39 , inj₁ _otherpunct-bar-38 :: []) :: (just "P136" , nothing , just _otherpunct-bar-39 , inj₂ '[' :: []) :: []
cws-start _otherpunct-bar-38 = (just "P135" , nothing , just _otherpunct-bar-38 , inj₁ _otherpunct-bar-37 :: []) :: (just "P134" , nothing , just _otherpunct-bar-38 , inj₂ ']' :: []) :: []
cws-start _otherpunct-bar-37 = (just "P133" , nothing , just _otherpunct-bar-37 , inj₁ _otherpunct-bar-36 :: []) :: (just "P132" , nothing , just _otherpunct-bar-37 , inj₂ ',' :: []) :: []
cws-start _otherpunct-bar-36 = (just "P131" , nothing , just _otherpunct-bar-36 , inj₁ _otherpunct-bar-35 :: []) :: (just "P130" , nothing , just _otherpunct-bar-36 , inj₂ '!' :: []) :: []
cws-start _otherpunct-bar-35 = (just "P129" , nothing , just _otherpunct-bar-35 , inj₁ _otherpunct-bar-34 :: []) :: (just "P128" , nothing , just _otherpunct-bar-35 , inj₂ '{' :: []) :: []
cws-start _otherpunct-bar-34 = (just "P127" , nothing , just _otherpunct-bar-34 , inj₁ _otherpunct-bar-33 :: []) :: (just "P126" , nothing , just _otherpunct-bar-34 , inj₂ '}' :: []) :: []
cws-start _otherpunct-bar-33 = (just "P125" , nothing , just _otherpunct-bar-33 , inj₁ _otherpunct-bar-32 :: []) :: (just "P124" , nothing , just _otherpunct-bar-33 , inj₂ '⇒' :: []) :: []
cws-start _otherpunct-bar-32 = (just "P123" , nothing , just _otherpunct-bar-32 , inj₁ _otherpunct-bar-31 :: []) :: (just "P122" , nothing , just _otherpunct-bar-32 , inj₂ '?' :: []) :: []
cws-start _otherpunct-bar-31 = (just "P121" , nothing , just _otherpunct-bar-31 , inj₁ _otherpunct-bar-30 :: []) :: (just "P120" , nothing , just _otherpunct-bar-31 , inj₂ 'Λ' :: []) :: []
cws-start _otherpunct-bar-30 = (just "P119" , nothing , just _otherpunct-bar-30 , inj₁ _otherpunct-bar-29 :: []) :: (just "P118" , nothing , just _otherpunct-bar-30 , inj₂ 'ρ' :: []) :: []
cws-start _otherpunct-bar-29 = (just "P117" , nothing , just _otherpunct-bar-29 , inj₁ _otherpunct-bar-28 :: []) :: (just "P116" , nothing , just _otherpunct-bar-29 , inj₂ 'ε' :: []) :: []
cws-start _otherpunct-bar-28 = (just "P115" , nothing , just _otherpunct-bar-28 , inj₁ _otherpunct-bar-27 :: []) :: (just "P114" , nothing , just _otherpunct-bar-28 , inj₂ 'β' :: []) :: []
cws-start _otherpunct-bar-27 = (just "P113" , nothing , just _otherpunct-bar-27 , inj₁ _otherpunct-bar-26 :: []) :: (just "P112" , nothing , just _otherpunct-bar-27 , inj₂ '-' :: []) :: []
cws-start _otherpunct-bar-26 = (just "P111" , nothing , just _otherpunct-bar-26 , inj₁ _otherpunct-bar-25 :: []) :: (just "P110" , nothing , just _otherpunct-bar-26 , inj₂ '𝒌' :: []) :: []
cws-start _otherpunct-bar-25 = (just "P109" , nothing , just _otherpunct-bar-25 , inj₁ _otherpunct-bar-24 :: []) :: (just "P108" , nothing , just _otherpunct-bar-25 , inj₂ '=' :: []) :: []
cws-start _otherpunct-bar-24 = (just "P107" , nothing , just _otherpunct-bar-24 , inj₁ _otherpunct-bar-23 :: []) :: (just "P106" , nothing , just _otherpunct-bar-24 , inj₂ 'ς' :: []) :: []
cws-start _otherpunct-bar-23 = (just "P105" , nothing , just _otherpunct-bar-23 , inj₁ _otherpunct-bar-22 :: []) :: (just "P104" , nothing , just _otherpunct-bar-23 , inj₂ 'θ' :: []) :: []
cws-start _otherpunct-bar-22 = (just "P103" , nothing , just _otherpunct-bar-22 , inj₁ _otherpunct-bar-21 :: []) :: (just "P102" , nothing , just _otherpunct-bar-22 , inj₂ '+' :: []) :: []
cws-start _otherpunct-bar-21 = (just "P101" , nothing , just _otherpunct-bar-21 , inj₁ _otherpunct-bar-20 :: []) :: (just "P100" , nothing , just _otherpunct-bar-21 , inj₂ '<' :: []) :: []
cws-start _otherpunct-bar-20 = (just "P99" , nothing , just _otherpunct-bar-20 , inj₁ _otherpunct-bar-19 :: []) :: (just "P98" , nothing , just _otherpunct-bar-20 , inj₂ '>' :: []) :: []
cws-start _otherpunct-bar-19 = (just "P97" , nothing , just _otherpunct-bar-19 , inj₁ _otherpunct-bar-18 :: []) :: (just "P96" , nothing , just _otherpunct-bar-19 , inj₂ '≃' :: []) :: []
cws-start _otherpunct-bar-18 = (just "P95" , nothing , just _otherpunct-bar-18 , inj₁ _otherpunct-bar-17 :: []) :: (just "P94" , nothing , just _otherpunct-bar-18 , inj₂ '\"' :: []) :: []
cws-start _otherpunct-bar-17 = (just "P93" , nothing , just _otherpunct-bar-17 , inj₁ _otherpunct-bar-16 :: []) :: (just "P92" , nothing , just _otherpunct-bar-17 , inj₂ 'δ' :: []) :: []
cws-start _otherpunct-bar-16 = (just "P91" , nothing , just _otherpunct-bar-16 , inj₁ _otherpunct-bar-15 :: []) :: (just "P90" , nothing , just _otherpunct-bar-16 , inj₂ 'χ' :: []) :: []
cws-start _otherpunct-bar-15 = (just "P89" , nothing , just _otherpunct-bar-15 , inj₁ _otherpunct-bar-14 :: []) :: (just "P88" , nothing , just _otherpunct-bar-15 , inj₂ 'μ' :: []) :: []
cws-start _otherpunct-bar-14 = (just "P87" , nothing , just _otherpunct-bar-14 , inj₁ _otherpunct-bar-13 :: []) :: (just "P86" , nothing , just _otherpunct-bar-14 , inj₂ 'υ' :: []) :: []
cws-start _otherpunct-bar-13 = (just "P85" , nothing , just _otherpunct-bar-13 , inj₁ _otherpunct-bar-12 :: []) :: (just "P84" , nothing , just _otherpunct-bar-13 , inj₂ 'φ' :: []) :: []
cws-start _otherpunct-bar-12 = (just "P83" , nothing , just _otherpunct-bar-12 , inj₂ 'ω' :: []) :: (just "P82" , nothing , just _otherpunct-bar-12 , inj₂ '◂' :: []) :: []
cws-start _otherpunct = (just "P176" , nothing , just _otherpunct , inj₁ _otherpunct-bar-58 :: []) :: []
cws-start _numpunct-bar-9 = (just "P76" , nothing , just _numpunct-bar-9 , inj₁ _numpunct-bar-8 :: []) :: (just "P75" , nothing , just _numpunct-bar-9 , inj₂ '-' :: []) :: []
cws-start _numpunct-bar-8 = (just "P74" , nothing , just _numpunct-bar-8 , inj₁ _numpunct-bar-7 :: []) :: (just "P73" , nothing , just _numpunct-bar-8 , inj₂ '~' :: []) :: []
cws-start _numpunct-bar-7 = (just "P72" , nothing , just _numpunct-bar-7 , inj₁ _numpunct-bar-6 :: []) :: (just "P71" , nothing , just _numpunct-bar-7 , inj₂ '#' :: []) :: []
cws-start _numpunct-bar-6 = (just "P70" , nothing , just _numpunct-bar-6 , inj₂ '/' :: []) :: (just "P69" , nothing , just _numpunct-bar-6 , inj₂ '_' :: []) :: []
cws-start _numpunct-bar-11 = (just "P80" , nothing , just _numpunct-bar-11 , inj₁ _numpunct-bar-10 :: []) :: (just "P79" , nothing , just _numpunct-bar-11 , inj₁ _numone :: []) :: []
cws-start _numpunct-bar-10 = (just "P78" , nothing , just _numpunct-bar-10 , inj₁ _numpunct-bar-9 :: []) :: (just "P77" , nothing , just _numpunct-bar-10 , inj₂ '\'' :: []) :: []
cws-start _numpunct = (just "P81" , nothing , just _numpunct , inj₁ _numpunct-bar-11 :: []) :: []
cws-start _numone-range-4 = (just "P64" , nothing , just _numone-range-4 , inj₂ '9' :: []) :: (just "P63" , nothing , just _numone-range-4 , inj₂ '8' :: []) :: (just "P62" , nothing , just _numone-range-4 , inj₂ '7' :: []) :: (just "P61" , nothing , just _numone-range-4 , inj₂ '6' :: []) :: (just "P60" , nothing , just _numone-range-4 , inj₂ '5' :: []) :: (just "P59" , nothing , just _numone-range-4 , inj₂ '4' :: []) :: (just "P58" , nothing , just _numone-range-4 , inj₂ '3' :: []) :: (just "P57" , nothing , just _numone-range-4 , inj₂ '2' :: []) :: (just "P56" , nothing , just _numone-range-4 , inj₂ '1' :: []) :: (just "P55" , nothing , just _numone-range-4 , inj₂ '0' :: []) :: []
cws-start _numone = (just "P65" , nothing , just _numone , inj₁ _numone-range-4 :: []) :: []
cws-start _num-plus-5 = (just "P67" , nothing , just _num-plus-5 , inj₁ _numone :: inj₁ _num-plus-5 :: []) :: (just "P66" , nothing , just _num-plus-5 , inj₁ _numone :: []) :: []
cws-start _num = (just "P68" , nothing , just _num , inj₁ _num-plus-5 :: []) :: []
cws-start _nonws-plus-70 = (just "P205" , nothing , just _nonws-plus-70 , inj₁ _anynonwschar :: inj₁ _nonws-plus-70 :: []) :: (just "P204" , nothing , just _nonws-plus-70 , inj₁ _anynonwschar :: []) :: []
cws-start _nonws = (just "P206" , nothing , just _nonws , inj₁ _nonws-plus-70 :: []) :: []
cws-start _entity = (just "EntityWs" , nothing , just _entity , inj₁ _posinfo :: inj₁ _ws :: inj₁ _posinfo :: []) :: (just "EntityNonws" , nothing , just _entity , inj₁ _nonws :: []) :: (just "EntityComment" , nothing , just _entity , inj₁ _posinfo :: inj₁ _comment :: inj₁ _posinfo :: []) :: []
cws-start _entities = (just "Entity" , nothing , just _entities , inj₁ _entity :: inj₁ _entities :: []) :: (just "EndEntity" , nothing , just _entities , []) :: []
cws-start _comment-star-64 = (just "P189" , nothing , just _comment-star-64 , inj₁ _anychar :: inj₁ _comment-star-64 :: []) :: (just "P188" , nothing , just _comment-star-64 , []) :: []
cws-start _comment = (just "P190" , nothing , just _comment , inj₂ '%' :: inj₁ _comment-star-64 :: inj₂ '\n' :: []) :: []
cws-start _aws-bar-66 = (just "P194" , nothing , just _aws-bar-66 , inj₁ _aws-bar-65 :: []) :: (just "P193" , nothing , just _aws-bar-66 , inj₂ '\n' :: []) :: []
cws-start _aws-bar-65 = (just "P192" , nothing , just _aws-bar-65 , inj₂ ' ' :: []) :: (just "P191" , nothing , just _aws-bar-65 , inj₂ '\t' :: []) :: []
cws-start _aws = (just "P195" , nothing , just _aws , inj₁ _aws-bar-66 :: []) :: []
cws-start _anynonwschar-bar-69 = (just "P202" , nothing , just _anynonwschar-bar-69 , inj₁ _anynonwschar-bar-68 :: []) :: (just "P201" , nothing , just _anynonwschar-bar-69 , inj₁ _alpha :: []) :: []
cws-start _anynonwschar-bar-68 = (just "P200" , nothing , just _anynonwschar-bar-68 , inj₁ _otherpunct :: []) :: (just "P199" , nothing , just _anynonwschar-bar-68 , inj₁ _numpunct :: []) :: []
cws-start _anynonwschar = (just "P203" , nothing , just _anynonwschar , inj₁ _anynonwschar-bar-69 :: []) :: []
cws-start _anychar-bar-63 = (just "P186" , nothing , just _anychar-bar-63 , inj₁ _anychar-bar-62 :: []) :: (just "P185" , nothing , just _anychar-bar-63 , inj₁ _alpha :: []) :: []
cws-start _anychar-bar-62 = (just "P184" , nothing , just _anychar-bar-62 , inj₁ _anychar-bar-61 :: []) :: (just "P183" , nothing , just _anychar-bar-62 , inj₁ _numpunct :: []) :: []
cws-start _anychar-bar-61 = (just "P182" , nothing , just _anychar-bar-61 , inj₁ _anychar-bar-60 :: []) :: (just "P181" , nothing , just _anychar-bar-61 , inj₂ '\t' :: []) :: []
cws-start _anychar-bar-60 = (just "P180" , nothing , just _anychar-bar-60 , inj₁ _anychar-bar-59 :: []) :: (just "P179" , nothing , just _anychar-bar-60 , inj₂ ' ' :: []) :: []
cws-start _anychar-bar-59 = (just "P178" , nothing , just _anychar-bar-59 , inj₁ _otherpunct :: []) :: (just "P177" , nothing , just _anychar-bar-59 , inj₂ '%' :: []) :: []
cws-start _anychar = (just "P187" , nothing , just _anychar , inj₁ _anychar-bar-63 :: []) :: []
cws-start _alpha-range-2 = (just "P51" , nothing , just _alpha-range-2 , inj₂ 'Z' :: []) :: (just "P50" , nothing , just _alpha-range-2 , inj₂ 'Y' :: []) :: (just "P49" , nothing , just _alpha-range-2 , inj₂ 'X' :: []) :: (just "P48" , nothing , just _alpha-range-2 , inj₂ 'W' :: []) :: (just "P47" , nothing , just _alpha-range-2 , inj₂ 'V' :: []) :: (just "P46" , nothing , just _alpha-range-2 , inj₂ 'U' :: []) :: (just "P45" , nothing , just _alpha-range-2 , inj₂ 'T' :: []) :: (just "P44" , nothing , just _alpha-range-2 , inj₂ 'S' :: []) :: (just "P43" , nothing , just _alpha-range-2 , inj₂ 'R' :: []) :: (just "P42" , nothing , just _alpha-range-2 , inj₂ 'Q' :: []) :: (just "P41" , nothing , just _alpha-range-2 , inj₂ 'P' :: []) :: (just "P40" , nothing , just _alpha-range-2 , inj₂ 'O' :: []) :: (just "P39" , nothing , just _alpha-range-2 , inj₂ 'N' :: []) :: (just "P38" , nothing , just _alpha-range-2 , inj₂ 'M' :: []) :: (just "P37" , nothing , just _alpha-range-2 , inj₂ 'L' :: []) :: (just "P36" , nothing , just _alpha-range-2 , inj₂ 'K' :: []) :: (just "P35" , nothing , just _alpha-range-2 , inj₂ 'J' :: []) :: (just "P34" , nothing , just _alpha-range-2 , inj₂ 'I' :: []) :: (just "P33" , nothing , just _alpha-range-2 , inj₂ 'H' :: []) :: (just "P32" , nothing , just _alpha-range-2 , inj₂ 'G' :: []) :: (just "P31" , nothing , just _alpha-range-2 , inj₂ 'F' :: []) :: (just "P30" , nothing , just _alpha-range-2 , inj₂ 'E' :: []) :: (just "P29" , nothing , just _alpha-range-2 , inj₂ 'D' :: []) :: (just "P28" , nothing , just _alpha-range-2 , inj₂ 'C' :: []) :: (just "P27" , nothing , just _alpha-range-2 , inj₂ 'B' :: []) :: (just "P26" , nothing , just _alpha-range-2 , inj₂ 'A' :: []) :: []
cws-start _alpha-range-1 = (just "P9" , nothing , just _alpha-range-1 , inj₂ 'j' :: []) :: (just "P8" , nothing , just _alpha-range-1 , inj₂ 'i' :: []) :: (just "P7" , nothing , just _alpha-range-1 , inj₂ 'h' :: []) :: (just "P6" , nothing , just _alpha-range-1 , inj₂ 'g' :: []) :: (just "P5" , nothing , just _alpha-range-1 , inj₂ 'f' :: []) :: (just "P4" , nothing , just _alpha-range-1 , inj₂ 'e' :: []) :: (just "P3" , nothing , just _alpha-range-1 , inj₂ 'd' :: []) :: (just "P25" , nothing , just _alpha-range-1 , inj₂ 'z' :: []) :: (just "P24" , nothing , just _alpha-range-1 , inj₂ 'y' :: []) :: (just "P23" , nothing , just _alpha-range-1 , inj₂ 'x' :: []) :: (just "P22" , nothing , just _alpha-range-1 , inj₂ 'w' :: []) :: (just "P21" , nothing , just _alpha-range-1 , inj₂ 'v' :: []) :: (just "P20" , nothing , just _alpha-range-1 , inj₂ 'u' :: []) :: (just "P2" , nothing , just _alpha-range-1 , inj₂ 'c' :: []) :: (just "P19" , nothing , just _alpha-range-1 , inj₂ 't' :: []) :: (just "P18" , nothing , just _alpha-range-1 , inj₂ 's' :: []) :: (just "P17" , nothing , just _alpha-range-1 , inj₂ 'r' :: []) :: (just "P16" , nothing , just _alpha-range-1 , inj₂ 'q' :: []) :: (just "P15" , nothing , just _alpha-range-1 , inj₂ 'p' :: []) :: (just "P14" , nothing , just _alpha-range-1 , inj₂ 'o' :: []) :: (just "P13" , nothing , just _alpha-range-1 , inj₂ 'n' :: []) :: (just "P12" , nothing , just _alpha-range-1 , inj₂ 'm' :: []) :: (just "P11" , nothing , just _alpha-range-1 , inj₂ 'l' :: []) :: (just "P10" , nothing , just _alpha-range-1 , inj₂ 'k' :: []) :: (just "P1" , nothing , just _alpha-range-1 , inj₂ 'b' :: []) :: (just "P0" , nothing , just _alpha-range-1 , inj₂ 'a' :: []) :: []
cws-start _alpha-bar-3 = (just "P53" , nothing , just _alpha-bar-3 , inj₁ _alpha-range-2 :: []) :: (just "P52" , nothing , just _alpha-bar-3 , inj₁ _alpha-range-1 :: []) :: []
cws-start _alpha = (just "P54" , nothing , just _alpha , inj₁ _alpha-bar-3 :: []) :: []

cws-return : maybe gratr2-nt → 𝕃 gratr2-rule
cws-return _ = []

cws-rtn : gratr2-rtn
cws-rtn = record { start = _start ; _eq_ = gratr2-nt-eq ; gratr2-start = cws-start ; gratr2-return = cws-return }

open import run ptr
open noderiv

------------------------------------------
-- Length-decreasing rules
------------------------------------------

len-dec-rewrite : Run → maybe (Run × ℕ)
len-dec-rewrite {- Entity-} ((Id "Entity") :: (ParseTree (parsed-entity x0)) :: _::_(ParseTree (parsed-entities x1)) rest) = just (ParseTree (parsed-entities (norm-entities (Entity x0 x1))) ::' rest , 3)
len-dec-rewrite {- EntityComment-} ((Id "EntityComment") :: (ParseTree (parsed-posinfo x0)) :: (ParseTree parsed-comment) :: _::_(ParseTree (parsed-posinfo x1)) rest) = just (ParseTree (parsed-entity (norm-entity (EntityComment x0 x1))) ::' rest , 4)
len-dec-rewrite {- EntityNonws-} ((Id "EntityNonws") :: _::_(ParseTree parsed-nonws) rest) = just (ParseTree (parsed-entity (norm-entity EntityNonws)) ::' rest , 2)
len-dec-rewrite {- EntityWs-} ((Id "EntityWs") :: (ParseTree (parsed-posinfo x0)) :: (ParseTree parsed-ws) :: _::_(ParseTree (parsed-posinfo x1)) rest) = just (ParseTree (parsed-entity (norm-entity (EntityWs x0 x1))) ::' rest , 4)
len-dec-rewrite {- File-} ((Id "File") :: _::_(ParseTree (parsed-entities x0)) rest) = just (ParseTree (parsed-start (norm-start (File x0))) ::' rest , 2)
len-dec-rewrite {- P0-} ((Id "P0") :: _::_(InputChar 'a') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P1-} ((Id "P1") :: _::_(InputChar 'b') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P10-} ((Id "P10") :: _::_(InputChar 'k') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P100-} ((Id "P100") :: _::_(InputChar '<') rest) = just (ParseTree parsed-otherpunct-bar-21 ::' rest , 2)
len-dec-rewrite {- P101-} ((Id "P101") :: _::_(ParseTree parsed-otherpunct-bar-20) rest) = just (ParseTree parsed-otherpunct-bar-21 ::' rest , 2)
len-dec-rewrite {- P102-} ((Id "P102") :: _::_(InputChar '+') rest) = just (ParseTree parsed-otherpunct-bar-22 ::' rest , 2)
len-dec-rewrite {- P103-} ((Id "P103") :: _::_(ParseTree parsed-otherpunct-bar-21) rest) = just (ParseTree parsed-otherpunct-bar-22 ::' rest , 2)
len-dec-rewrite {- P104-} ((Id "P104") :: _::_(InputChar 'θ') rest) = just (ParseTree parsed-otherpunct-bar-23 ::' rest , 2)
len-dec-rewrite {- P105-} ((Id "P105") :: _::_(ParseTree parsed-otherpunct-bar-22) rest) = just (ParseTree parsed-otherpunct-bar-23 ::' rest , 2)
len-dec-rewrite {- P106-} ((Id "P106") :: _::_(InputChar 'ς') rest) = just (ParseTree parsed-otherpunct-bar-24 ::' rest , 2)
len-dec-rewrite {- P107-} ((Id "P107") :: _::_(ParseTree parsed-otherpunct-bar-23) rest) = just (ParseTree parsed-otherpunct-bar-24 ::' rest , 2)
len-dec-rewrite {- P108-} ((Id "P108") :: _::_(InputChar '=') rest) = just (ParseTree parsed-otherpunct-bar-25 ::' rest , 2)
len-dec-rewrite {- P109-} ((Id "P109") :: _::_(ParseTree parsed-otherpunct-bar-24) rest) = just (ParseTree parsed-otherpunct-bar-25 ::' rest , 2)
len-dec-rewrite {- P11-} ((Id "P11") :: _::_(InputChar 'l') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P110-} ((Id "P110") :: _::_(InputChar '𝒌') rest) = just (ParseTree parsed-otherpunct-bar-26 ::' rest , 2)
len-dec-rewrite {- P111-} ((Id "P111") :: _::_(ParseTree parsed-otherpunct-bar-25) rest) = just (ParseTree parsed-otherpunct-bar-26 ::' rest , 2)
len-dec-rewrite {- P112-} ((Id "P112") :: _::_(InputChar '-') rest) = just (ParseTree parsed-otherpunct-bar-27 ::' rest , 2)
len-dec-rewrite {- P113-} ((Id "P113") :: _::_(ParseTree parsed-otherpunct-bar-26) rest) = just (ParseTree parsed-otherpunct-bar-27 ::' rest , 2)
len-dec-rewrite {- P114-} ((Id "P114") :: _::_(InputChar 'β') rest) = just (ParseTree parsed-otherpunct-bar-28 ::' rest , 2)
len-dec-rewrite {- P115-} ((Id "P115") :: _::_(ParseTree parsed-otherpunct-bar-27) rest) = just (ParseTree parsed-otherpunct-bar-28 ::' rest , 2)
len-dec-rewrite {- P116-} ((Id "P116") :: _::_(InputChar 'ε') rest) = just (ParseTree parsed-otherpunct-bar-29 ::' rest , 2)
len-dec-rewrite {- P117-} ((Id "P117") :: _::_(ParseTree parsed-otherpunct-bar-28) rest) = just (ParseTree parsed-otherpunct-bar-29 ::' rest , 2)
len-dec-rewrite {- P118-} ((Id "P118") :: _::_(InputChar 'ρ') rest) = just (ParseTree parsed-otherpunct-bar-30 ::' rest , 2)
len-dec-rewrite {- P119-} ((Id "P119") :: _::_(ParseTree parsed-otherpunct-bar-29) rest) = just (ParseTree parsed-otherpunct-bar-30 ::' rest , 2)
len-dec-rewrite {- P12-} ((Id "P12") :: _::_(InputChar 'm') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P120-} ((Id "P120") :: _::_(InputChar 'Λ') rest) = just (ParseTree parsed-otherpunct-bar-31 ::' rest , 2)
len-dec-rewrite {- P121-} ((Id "P121") :: _::_(ParseTree parsed-otherpunct-bar-30) rest) = just (ParseTree parsed-otherpunct-bar-31 ::' rest , 2)
len-dec-rewrite {- P122-} ((Id "P122") :: _::_(InputChar '?') rest) = just (ParseTree parsed-otherpunct-bar-32 ::' rest , 2)
len-dec-rewrite {- P123-} ((Id "P123") :: _::_(ParseTree parsed-otherpunct-bar-31) rest) = just (ParseTree parsed-otherpunct-bar-32 ::' rest , 2)
len-dec-rewrite {- P124-} ((Id "P124") :: _::_(InputChar '⇒') rest) = just (ParseTree parsed-otherpunct-bar-33 ::' rest , 2)
len-dec-rewrite {- P125-} ((Id "P125") :: _::_(ParseTree parsed-otherpunct-bar-32) rest) = just (ParseTree parsed-otherpunct-bar-33 ::' rest , 2)
len-dec-rewrite {- P126-} ((Id "P126") :: _::_(InputChar '}') rest) = just (ParseTree parsed-otherpunct-bar-34 ::' rest , 2)
len-dec-rewrite {- P127-} ((Id "P127") :: _::_(ParseTree parsed-otherpunct-bar-33) rest) = just (ParseTree parsed-otherpunct-bar-34 ::' rest , 2)
len-dec-rewrite {- P128-} ((Id "P128") :: _::_(InputChar '{') rest) = just (ParseTree parsed-otherpunct-bar-35 ::' rest , 2)
len-dec-rewrite {- P129-} ((Id "P129") :: _::_(ParseTree parsed-otherpunct-bar-34) rest) = just (ParseTree parsed-otherpunct-bar-35 ::' rest , 2)
len-dec-rewrite {- P13-} ((Id "P13") :: _::_(InputChar 'n') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P130-} ((Id "P130") :: _::_(InputChar '!') rest) = just (ParseTree parsed-otherpunct-bar-36 ::' rest , 2)
len-dec-rewrite {- P131-} ((Id "P131") :: _::_(ParseTree parsed-otherpunct-bar-35) rest) = just (ParseTree parsed-otherpunct-bar-36 ::' rest , 2)
len-dec-rewrite {- P132-} ((Id "P132") :: _::_(InputChar ',') rest) = just (ParseTree parsed-otherpunct-bar-37 ::' rest , 2)
len-dec-rewrite {- P133-} ((Id "P133") :: _::_(ParseTree parsed-otherpunct-bar-36) rest) = just (ParseTree parsed-otherpunct-bar-37 ::' rest , 2)
len-dec-rewrite {- P134-} ((Id "P134") :: _::_(InputChar ']') rest) = just (ParseTree parsed-otherpunct-bar-38 ::' rest , 2)
len-dec-rewrite {- P135-} ((Id "P135") :: _::_(ParseTree parsed-otherpunct-bar-37) rest) = just (ParseTree parsed-otherpunct-bar-38 ::' rest , 2)
len-dec-rewrite {- P136-} ((Id "P136") :: _::_(InputChar '[') rest) = just (ParseTree parsed-otherpunct-bar-39 ::' rest , 2)
len-dec-rewrite {- P137-} ((Id "P137") :: _::_(ParseTree parsed-otherpunct-bar-38) rest) = just (ParseTree parsed-otherpunct-bar-39 ::' rest , 2)
len-dec-rewrite {- P138-} ((Id "P138") :: _::_(InputChar '.') rest) = just (ParseTree parsed-otherpunct-bar-40 ::' rest , 2)
len-dec-rewrite {- P139-} ((Id "P139") :: _::_(ParseTree parsed-otherpunct-bar-39) rest) = just (ParseTree parsed-otherpunct-bar-40 ::' rest , 2)
len-dec-rewrite {- P14-} ((Id "P14") :: _::_(InputChar 'o') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P140-} ((Id "P140") :: _::_(InputChar ':') rest) = just (ParseTree parsed-otherpunct-bar-41 ::' rest , 2)
len-dec-rewrite {- P141-} ((Id "P141") :: _::_(ParseTree parsed-otherpunct-bar-40) rest) = just (ParseTree parsed-otherpunct-bar-41 ::' rest , 2)
len-dec-rewrite {- P142-} ((Id "P142") :: _::_(InputChar ')') rest) = just (ParseTree parsed-otherpunct-bar-42 ::' rest , 2)
len-dec-rewrite {- P143-} ((Id "P143") :: _::_(ParseTree parsed-otherpunct-bar-41) rest) = just (ParseTree parsed-otherpunct-bar-42 ::' rest , 2)
len-dec-rewrite {- P144-} ((Id "P144") :: _::_(InputChar '(') rest) = just (ParseTree parsed-otherpunct-bar-43 ::' rest , 2)
len-dec-rewrite {- P145-} ((Id "P145") :: _::_(ParseTree parsed-otherpunct-bar-42) rest) = just (ParseTree parsed-otherpunct-bar-43 ::' rest , 2)
len-dec-rewrite {- P146-} ((Id "P146") :: _::_(InputChar '●') rest) = just (ParseTree parsed-otherpunct-bar-44 ::' rest , 2)
len-dec-rewrite {- P147-} ((Id "P147") :: _::_(ParseTree parsed-otherpunct-bar-43) rest) = just (ParseTree parsed-otherpunct-bar-44 ::' rest , 2)
len-dec-rewrite {- P148-} ((Id "P148") :: _::_(InputChar '↑') rest) = just (ParseTree parsed-otherpunct-bar-45 ::' rest , 2)
len-dec-rewrite {- P149-} ((Id "P149") :: _::_(ParseTree parsed-otherpunct-bar-44) rest) = just (ParseTree parsed-otherpunct-bar-45 ::' rest , 2)
len-dec-rewrite {- P15-} ((Id "P15") :: _::_(InputChar 'p') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P150-} ((Id "P150") :: _::_(InputChar '➾') rest) = just (ParseTree parsed-otherpunct-bar-46 ::' rest , 2)
len-dec-rewrite {- P151-} ((Id "P151") :: _::_(ParseTree parsed-otherpunct-bar-45) rest) = just (ParseTree parsed-otherpunct-bar-46 ::' rest , 2)
len-dec-rewrite {- P152-} ((Id "P152") :: _::_(InputChar '➔') rest) = just (ParseTree parsed-otherpunct-bar-47 ::' rest , 2)
len-dec-rewrite {- P153-} ((Id "P153") :: _::_(ParseTree parsed-otherpunct-bar-46) rest) = just (ParseTree parsed-otherpunct-bar-47 ::' rest , 2)
len-dec-rewrite {- P154-} ((Id "P154") :: _::_(InputChar '⇐') rest) = just (ParseTree parsed-otherpunct-bar-48 ::' rest , 2)
len-dec-rewrite {- P155-} ((Id "P155") :: _::_(ParseTree parsed-otherpunct-bar-47) rest) = just (ParseTree parsed-otherpunct-bar-48 ::' rest , 2)
len-dec-rewrite {- P156-} ((Id "P156") :: _::_(InputChar '·') rest) = just (ParseTree parsed-otherpunct-bar-49 ::' rest , 2)
len-dec-rewrite {- P157-} ((Id "P157") :: _::_(ParseTree parsed-otherpunct-bar-48) rest) = just (ParseTree parsed-otherpunct-bar-49 ::' rest , 2)
len-dec-rewrite {- P158-} ((Id "P158") :: _::_(InputChar '☆') rest) = just (ParseTree parsed-otherpunct-bar-50 ::' rest , 2)
len-dec-rewrite {- P159-} ((Id "P159") :: _::_(ParseTree parsed-otherpunct-bar-49) rest) = just (ParseTree parsed-otherpunct-bar-50 ::' rest , 2)
len-dec-rewrite {- P16-} ((Id "P16") :: _::_(InputChar 'q') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P160-} ((Id "P160") :: _::_(InputChar '★') rest) = just (ParseTree parsed-otherpunct-bar-51 ::' rest , 2)
len-dec-rewrite {- P161-} ((Id "P161") :: _::_(ParseTree parsed-otherpunct-bar-50) rest) = just (ParseTree parsed-otherpunct-bar-51 ::' rest , 2)
len-dec-rewrite {- P162-} ((Id "P162") :: _::_(InputChar 'π') rest) = just (ParseTree parsed-otherpunct-bar-52 ::' rest , 2)
len-dec-rewrite {- P163-} ((Id "P163") :: _::_(ParseTree parsed-otherpunct-bar-51) rest) = just (ParseTree parsed-otherpunct-bar-52 ::' rest , 2)
len-dec-rewrite {- P164-} ((Id "P164") :: _::_(InputChar '∀') rest) = just (ParseTree parsed-otherpunct-bar-53 ::' rest , 2)
len-dec-rewrite {- P165-} ((Id "P165") :: _::_(ParseTree parsed-otherpunct-bar-52) rest) = just (ParseTree parsed-otherpunct-bar-53 ::' rest , 2)
len-dec-rewrite {- P166-} ((Id "P166") :: _::_(InputChar 'λ') rest) = just (ParseTree parsed-otherpunct-bar-54 ::' rest , 2)
len-dec-rewrite {- P167-} ((Id "P167") :: _::_(ParseTree parsed-otherpunct-bar-53) rest) = just (ParseTree parsed-otherpunct-bar-54 ::' rest , 2)
len-dec-rewrite {- P168-} ((Id "P168") :: _::_(InputChar 'ι') rest) = just (ParseTree parsed-otherpunct-bar-55 ::' rest , 2)
len-dec-rewrite {- P169-} ((Id "P169") :: _::_(ParseTree parsed-otherpunct-bar-54) rest) = just (ParseTree parsed-otherpunct-bar-55 ::' rest , 2)
len-dec-rewrite {- P17-} ((Id "P17") :: _::_(InputChar 'r') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P170-} ((Id "P170") :: _::_(InputChar 'Π') rest) = just (ParseTree parsed-otherpunct-bar-56 ::' rest , 2)
len-dec-rewrite {- P171-} ((Id "P171") :: _::_(ParseTree parsed-otherpunct-bar-55) rest) = just (ParseTree parsed-otherpunct-bar-56 ::' rest , 2)
len-dec-rewrite {- P172-} ((Id "P172") :: _::_(InputChar '□') rest) = just (ParseTree parsed-otherpunct-bar-57 ::' rest , 2)
len-dec-rewrite {- P173-} ((Id "P173") :: _::_(ParseTree parsed-otherpunct-bar-56) rest) = just (ParseTree parsed-otherpunct-bar-57 ::' rest , 2)
len-dec-rewrite {- P174-} ((Id "P174") :: _::_(InputChar '|') rest) = just (ParseTree parsed-otherpunct-bar-58 ::' rest , 2)
len-dec-rewrite {- P175-} ((Id "P175") :: _::_(ParseTree parsed-otherpunct-bar-57) rest) = just (ParseTree parsed-otherpunct-bar-58 ::' rest , 2)
len-dec-rewrite {- P176-} ((Id "P176") :: _::_(ParseTree parsed-otherpunct-bar-58) rest) = just (ParseTree parsed-otherpunct ::' rest , 2)
len-dec-rewrite {- P177-} ((Id "P177") :: _::_(InputChar '%') rest) = just (ParseTree parsed-anychar-bar-59 ::' rest , 2)
len-dec-rewrite {- P178-} ((Id "P178") :: _::_(ParseTree parsed-otherpunct) rest) = just (ParseTree parsed-anychar-bar-59 ::' rest , 2)
len-dec-rewrite {- P179-} ((Id "P179") :: _::_(InputChar ' ') rest) = just (ParseTree parsed-anychar-bar-60 ::' rest , 2)
len-dec-rewrite {- P18-} ((Id "P18") :: _::_(InputChar 's') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P180-} ((Id "P180") :: _::_(ParseTree parsed-anychar-bar-59) rest) = just (ParseTree parsed-anychar-bar-60 ::' rest , 2)
len-dec-rewrite {- P181-} ((Id "P181") :: _::_(InputChar '\t') rest) = just (ParseTree parsed-anychar-bar-61 ::' rest , 2)
len-dec-rewrite {- P182-} ((Id "P182") :: _::_(ParseTree parsed-anychar-bar-60) rest) = just (ParseTree parsed-anychar-bar-61 ::' rest , 2)
len-dec-rewrite {- P183-} ((Id "P183") :: _::_(ParseTree parsed-numpunct) rest) = just (ParseTree parsed-anychar-bar-62 ::' rest , 2)
len-dec-rewrite {- P184-} ((Id "P184") :: _::_(ParseTree parsed-anychar-bar-61) rest) = just (ParseTree parsed-anychar-bar-62 ::' rest , 2)
len-dec-rewrite {- P185-} ((Id "P185") :: _::_(ParseTree parsed-alpha) rest) = just (ParseTree parsed-anychar-bar-63 ::' rest , 2)
len-dec-rewrite {- P186-} ((Id "P186") :: _::_(ParseTree parsed-anychar-bar-62) rest) = just (ParseTree parsed-anychar-bar-63 ::' rest , 2)
len-dec-rewrite {- P187-} ((Id "P187") :: _::_(ParseTree parsed-anychar-bar-63) rest) = just (ParseTree parsed-anychar ::' rest , 2)
len-dec-rewrite {- P189-} ((Id "P189") :: (ParseTree parsed-anychar) :: _::_(ParseTree parsed-comment-star-64) rest) = just (ParseTree parsed-comment-star-64 ::' rest , 3)
len-dec-rewrite {- P19-} ((Id "P19") :: _::_(InputChar 't') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P190-} ((Id "P190") :: (InputChar '%') :: (ParseTree parsed-comment-star-64) :: _::_(InputChar '\n') rest) = just (ParseTree parsed-comment ::' rest , 4)
len-dec-rewrite {- P191-} ((Id "P191") :: _::_(InputChar '\t') rest) = just (ParseTree parsed-aws-bar-65 ::' rest , 2)
len-dec-rewrite {- P192-} ((Id "P192") :: _::_(InputChar ' ') rest) = just (ParseTree parsed-aws-bar-65 ::' rest , 2)
len-dec-rewrite {- P193-} ((Id "P193") :: _::_(InputChar '\n') rest) = just (ParseTree parsed-aws-bar-66 ::' rest , 2)
len-dec-rewrite {- P194-} ((Id "P194") :: _::_(ParseTree parsed-aws-bar-65) rest) = just (ParseTree parsed-aws-bar-66 ::' rest , 2)
len-dec-rewrite {- P195-} ((Id "P195") :: _::_(ParseTree parsed-aws-bar-66) rest) = just (ParseTree parsed-aws ::' rest , 2)
len-dec-rewrite {- P196-} ((Id "P196") :: _::_(ParseTree parsed-aws) rest) = just (ParseTree parsed-ws-plus-67 ::' rest , 2)
len-dec-rewrite {- P197-} ((Id "P197") :: (ParseTree parsed-aws) :: _::_(ParseTree parsed-ws-plus-67) rest) = just (ParseTree parsed-ws-plus-67 ::' rest , 3)
len-dec-rewrite {- P198-} ((Id "P198") :: _::_(ParseTree parsed-ws-plus-67) rest) = just (ParseTree parsed-ws ::' rest , 2)
len-dec-rewrite {- P199-} ((Id "P199") :: _::_(ParseTree parsed-numpunct) rest) = just (ParseTree parsed-anynonwschar-bar-68 ::' rest , 2)
len-dec-rewrite {- P2-} ((Id "P2") :: _::_(InputChar 'c') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P20-} ((Id "P20") :: _::_(InputChar 'u') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P200-} ((Id "P200") :: _::_(ParseTree parsed-otherpunct) rest) = just (ParseTree parsed-anynonwschar-bar-68 ::' rest , 2)
len-dec-rewrite {- P201-} ((Id "P201") :: _::_(ParseTree parsed-alpha) rest) = just (ParseTree parsed-anynonwschar-bar-69 ::' rest , 2)
len-dec-rewrite {- P202-} ((Id "P202") :: _::_(ParseTree parsed-anynonwschar-bar-68) rest) = just (ParseTree parsed-anynonwschar-bar-69 ::' rest , 2)
len-dec-rewrite {- P203-} ((Id "P203") :: _::_(ParseTree parsed-anynonwschar-bar-69) rest) = just (ParseTree parsed-anynonwschar ::' rest , 2)
len-dec-rewrite {- P204-} ((Id "P204") :: _::_(ParseTree parsed-anynonwschar) rest) = just (ParseTree parsed-nonws-plus-70 ::' rest , 2)
len-dec-rewrite {- P205-} ((Id "P205") :: (ParseTree parsed-anynonwschar) :: _::_(ParseTree parsed-nonws-plus-70) rest) = just (ParseTree parsed-nonws-plus-70 ::' rest , 3)
len-dec-rewrite {- P206-} ((Id "P206") :: _::_(ParseTree parsed-nonws-plus-70) rest) = just (ParseTree parsed-nonws ::' rest , 2)
len-dec-rewrite {- P21-} ((Id "P21") :: _::_(InputChar 'v') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P22-} ((Id "P22") :: _::_(InputChar 'w') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P23-} ((Id "P23") :: _::_(InputChar 'x') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P24-} ((Id "P24") :: _::_(InputChar 'y') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P25-} ((Id "P25") :: _::_(InputChar 'z') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P26-} ((Id "P26") :: _::_(InputChar 'A') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P27-} ((Id "P27") :: _::_(InputChar 'B') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P28-} ((Id "P28") :: _::_(InputChar 'C') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P29-} ((Id "P29") :: _::_(InputChar 'D') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P3-} ((Id "P3") :: _::_(InputChar 'd') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P30-} ((Id "P30") :: _::_(InputChar 'E') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P31-} ((Id "P31") :: _::_(InputChar 'F') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P32-} ((Id "P32") :: _::_(InputChar 'G') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P33-} ((Id "P33") :: _::_(InputChar 'H') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P34-} ((Id "P34") :: _::_(InputChar 'I') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P35-} ((Id "P35") :: _::_(InputChar 'J') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P36-} ((Id "P36") :: _::_(InputChar 'K') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P37-} ((Id "P37") :: _::_(InputChar 'L') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P38-} ((Id "P38") :: _::_(InputChar 'M') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P39-} ((Id "P39") :: _::_(InputChar 'N') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P4-} ((Id "P4") :: _::_(InputChar 'e') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P40-} ((Id "P40") :: _::_(InputChar 'O') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P41-} ((Id "P41") :: _::_(InputChar 'P') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P42-} ((Id "P42") :: _::_(InputChar 'Q') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P43-} ((Id "P43") :: _::_(InputChar 'R') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P44-} ((Id "P44") :: _::_(InputChar 'S') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P45-} ((Id "P45") :: _::_(InputChar 'T') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P46-} ((Id "P46") :: _::_(InputChar 'U') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P47-} ((Id "P47") :: _::_(InputChar 'V') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P48-} ((Id "P48") :: _::_(InputChar 'W') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P49-} ((Id "P49") :: _::_(InputChar 'X') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P5-} ((Id "P5") :: _::_(InputChar 'f') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P50-} ((Id "P50") :: _::_(InputChar 'Y') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P51-} ((Id "P51") :: _::_(InputChar 'Z') rest) = just (ParseTree parsed-alpha-range-2 ::' rest , 2)
len-dec-rewrite {- P52-} ((Id "P52") :: _::_(ParseTree parsed-alpha-range-1) rest) = just (ParseTree parsed-alpha-bar-3 ::' rest , 2)
len-dec-rewrite {- P53-} ((Id "P53") :: _::_(ParseTree parsed-alpha-range-2) rest) = just (ParseTree parsed-alpha-bar-3 ::' rest , 2)
len-dec-rewrite {- P54-} ((Id "P54") :: _::_(ParseTree parsed-alpha-bar-3) rest) = just (ParseTree parsed-alpha ::' rest , 2)
len-dec-rewrite {- P55-} ((Id "P55") :: _::_(InputChar '0') rest) = just (ParseTree parsed-numone-range-4 ::' rest , 2)
len-dec-rewrite {- P56-} ((Id "P56") :: _::_(InputChar '1') rest) = just (ParseTree parsed-numone-range-4 ::' rest , 2)
len-dec-rewrite {- P57-} ((Id "P57") :: _::_(InputChar '2') rest) = just (ParseTree parsed-numone-range-4 ::' rest , 2)
len-dec-rewrite {- P58-} ((Id "P58") :: _::_(InputChar '3') rest) = just (ParseTree parsed-numone-range-4 ::' rest , 2)
len-dec-rewrite {- P59-} ((Id "P59") :: _::_(InputChar '4') rest) = just (ParseTree parsed-numone-range-4 ::' rest , 2)
len-dec-rewrite {- P6-} ((Id "P6") :: _::_(InputChar 'g') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P60-} ((Id "P60") :: _::_(InputChar '5') rest) = just (ParseTree parsed-numone-range-4 ::' rest , 2)
len-dec-rewrite {- P61-} ((Id "P61") :: _::_(InputChar '6') rest) = just (ParseTree parsed-numone-range-4 ::' rest , 2)
len-dec-rewrite {- P62-} ((Id "P62") :: _::_(InputChar '7') rest) = just (ParseTree parsed-numone-range-4 ::' rest , 2)
len-dec-rewrite {- P63-} ((Id "P63") :: _::_(InputChar '8') rest) = just (ParseTree parsed-numone-range-4 ::' rest , 2)
len-dec-rewrite {- P64-} ((Id "P64") :: _::_(InputChar '9') rest) = just (ParseTree parsed-numone-range-4 ::' rest , 2)
len-dec-rewrite {- P65-} ((Id "P65") :: _::_(ParseTree parsed-numone-range-4) rest) = just (ParseTree parsed-numone ::' rest , 2)
len-dec-rewrite {- P66-} ((Id "P66") :: _::_(ParseTree parsed-numone) rest) = just (ParseTree parsed-num-plus-5 ::' rest , 2)
len-dec-rewrite {- P67-} ((Id "P67") :: (ParseTree parsed-numone) :: _::_(ParseTree parsed-num-plus-5) rest) = just (ParseTree parsed-num-plus-5 ::' rest , 3)
len-dec-rewrite {- P68-} ((Id "P68") :: _::_(ParseTree parsed-num-plus-5) rest) = just (ParseTree parsed-num ::' rest , 2)
len-dec-rewrite {- P69-} ((Id "P69") :: _::_(InputChar '_') rest) = just (ParseTree parsed-numpunct-bar-6 ::' rest , 2)
len-dec-rewrite {- P7-} ((Id "P7") :: _::_(InputChar 'h') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P70-} ((Id "P70") :: _::_(InputChar '/') rest) = just (ParseTree parsed-numpunct-bar-6 ::' rest , 2)
len-dec-rewrite {- P71-} ((Id "P71") :: _::_(InputChar '#') rest) = just (ParseTree parsed-numpunct-bar-7 ::' rest , 2)
len-dec-rewrite {- P72-} ((Id "P72") :: _::_(ParseTree parsed-numpunct-bar-6) rest) = just (ParseTree parsed-numpunct-bar-7 ::' rest , 2)
len-dec-rewrite {- P73-} ((Id "P73") :: _::_(InputChar '~') rest) = just (ParseTree parsed-numpunct-bar-8 ::' rest , 2)
len-dec-rewrite {- P74-} ((Id "P74") :: _::_(ParseTree parsed-numpunct-bar-7) rest) = just (ParseTree parsed-numpunct-bar-8 ::' rest , 2)
len-dec-rewrite {- P75-} ((Id "P75") :: _::_(InputChar '-') rest) = just (ParseTree parsed-numpunct-bar-9 ::' rest , 2)
len-dec-rewrite {- P76-} ((Id "P76") :: _::_(ParseTree parsed-numpunct-bar-8) rest) = just (ParseTree parsed-numpunct-bar-9 ::' rest , 2)
len-dec-rewrite {- P77-} ((Id "P77") :: _::_(InputChar '\'') rest) = just (ParseTree parsed-numpunct-bar-10 ::' rest , 2)
len-dec-rewrite {- P78-} ((Id "P78") :: _::_(ParseTree parsed-numpunct-bar-9) rest) = just (ParseTree parsed-numpunct-bar-10 ::' rest , 2)
len-dec-rewrite {- P79-} ((Id "P79") :: _::_(ParseTree parsed-numone) rest) = just (ParseTree parsed-numpunct-bar-11 ::' rest , 2)
len-dec-rewrite {- P8-} ((Id "P8") :: _::_(InputChar 'i') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P80-} ((Id "P80") :: _::_(ParseTree parsed-numpunct-bar-10) rest) = just (ParseTree parsed-numpunct-bar-11 ::' rest , 2)
len-dec-rewrite {- P81-} ((Id "P81") :: _::_(ParseTree parsed-numpunct-bar-11) rest) = just (ParseTree parsed-numpunct ::' rest , 2)
len-dec-rewrite {- P82-} ((Id "P82") :: _::_(InputChar '◂') rest) = just (ParseTree parsed-otherpunct-bar-12 ::' rest , 2)
len-dec-rewrite {- P83-} ((Id "P83") :: _::_(InputChar 'ω') rest) = just (ParseTree parsed-otherpunct-bar-12 ::' rest , 2)
len-dec-rewrite {- P84-} ((Id "P84") :: _::_(InputChar 'φ') rest) = just (ParseTree parsed-otherpunct-bar-13 ::' rest , 2)
len-dec-rewrite {- P85-} ((Id "P85") :: _::_(ParseTree parsed-otherpunct-bar-12) rest) = just (ParseTree parsed-otherpunct-bar-13 ::' rest , 2)
len-dec-rewrite {- P86-} ((Id "P86") :: _::_(InputChar 'υ') rest) = just (ParseTree parsed-otherpunct-bar-14 ::' rest , 2)
len-dec-rewrite {- P87-} ((Id "P87") :: _::_(ParseTree parsed-otherpunct-bar-13) rest) = just (ParseTree parsed-otherpunct-bar-14 ::' rest , 2)
len-dec-rewrite {- P88-} ((Id "P88") :: _::_(InputChar 'μ') rest) = just (ParseTree parsed-otherpunct-bar-15 ::' rest , 2)
len-dec-rewrite {- P89-} ((Id "P89") :: _::_(ParseTree parsed-otherpunct-bar-14) rest) = just (ParseTree parsed-otherpunct-bar-15 ::' rest , 2)
len-dec-rewrite {- P9-} ((Id "P9") :: _::_(InputChar 'j') rest) = just (ParseTree parsed-alpha-range-1 ::' rest , 2)
len-dec-rewrite {- P90-} ((Id "P90") :: _::_(InputChar 'χ') rest) = just (ParseTree parsed-otherpunct-bar-16 ::' rest , 2)
len-dec-rewrite {- P91-} ((Id "P91") :: _::_(ParseTree parsed-otherpunct-bar-15) rest) = just (ParseTree parsed-otherpunct-bar-16 ::' rest , 2)
len-dec-rewrite {- P92-} ((Id "P92") :: _::_(InputChar 'δ') rest) = just (ParseTree parsed-otherpunct-bar-17 ::' rest , 2)
len-dec-rewrite {- P93-} ((Id "P93") :: _::_(ParseTree parsed-otherpunct-bar-16) rest) = just (ParseTree parsed-otherpunct-bar-17 ::' rest , 2)
len-dec-rewrite {- P94-} ((Id "P94") :: _::_(InputChar '\"') rest) = just (ParseTree parsed-otherpunct-bar-18 ::' rest , 2)
len-dec-rewrite {- P95-} ((Id "P95") :: _::_(ParseTree parsed-otherpunct-bar-17) rest) = just (ParseTree parsed-otherpunct-bar-18 ::' rest , 2)
len-dec-rewrite {- P96-} ((Id "P96") :: _::_(InputChar '≃') rest) = just (ParseTree parsed-otherpunct-bar-19 ::' rest , 2)
len-dec-rewrite {- P97-} ((Id "P97") :: _::_(ParseTree parsed-otherpunct-bar-18) rest) = just (ParseTree parsed-otherpunct-bar-19 ::' rest , 2)
len-dec-rewrite {- P98-} ((Id "P98") :: _::_(InputChar '>') rest) = just (ParseTree parsed-otherpunct-bar-20 ::' rest , 2)
len-dec-rewrite {- P99-} ((Id "P99") :: _::_(ParseTree parsed-otherpunct-bar-19) rest) = just (ParseTree parsed-otherpunct-bar-20 ::' rest , 2)
len-dec-rewrite {- EndEntity-} (_::_(Id "EndEntity") rest) = just (ParseTree (parsed-entities (norm-entities EndEntity)) ::' rest , 1)
len-dec-rewrite {- P188-} (_::_(Id "P188") rest) = just (ParseTree parsed-comment-star-64 ::' rest , 1)
len-dec-rewrite {- Posinfo-} (_::_(Posinfo n) rest) = just (ParseTree (parsed-posinfo (ℕ-to-string n)) ::' rest , 1)
len-dec-rewrite x = nothing

rrs : rewriteRules
rrs = record { len-dec-rewrite = len-dec-rewrite }

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


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

open import Groups.Definition
open import Groups.Abelian.Definition
open import Setoids.Setoids
open import Rings.Definition
open import Modules.Definition
open import Fields.Fields

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Vectors.VectorSpace {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+R_ : A → A → A} {_*_ : A → A → A} (R : Ring S _+R_ _*_) {m n : _} {M : Set m} {T : Setoid {m} {n} M} {_+_ : M → M → M} {G' : Group T _+_} (G : AbelianGroup G') (_·_ : A → M → M) where

record VectorSpace : Set (lsuc a ⊔ b ⊔ m ⊔ n) where
  field
    isModule : Module R G _·_
    isField : Field R


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

open import Data.Product renaming (proj₁ to ₁; proj₂ to ₂)
open import Relation.Binary.PropositionalEquality
open import Function

test : Set
test = Set where

  -- (Agda 2.6.1.3)

  -- works
  --------------------------------------------------------------------------------

  -- eliminating projections
  -- m : Set × Set
  -- m = _
  -- p₁ = (m .₁ ≡ Set) ∋ refl
  -- p₂ = (m .₂ ≡ Set) ∋ refl

  -- currying
  -- m : Set × Set → Set
  -- m = _
  -- p = λ (A : Set)(B : Set) → m (A , B) ≡ A ∋ refl

  -- nested currying
  -- m : Set × (Set × Set) → Set
  -- m = _
  -- p = λ (A : Set)(B : Set)(C : Set) → m (A , (B , C)) ≡ A ∋ refl

  -- projected variable under pairing
  -- m : Set × Set → Set
  -- m = _
  -- p = λ (A : Set)(B : Set × Set) → m (A , B .₁) ≡ B .₁ ∋ refl

  -- non-linearity
  -- m : Set → Set → Set → Set
  -- m = _
  -- p = λ (A : Set)(B : Set) → m A B B ≡ A ∋ refl
    -- m A B B =? A
    -- m = λ A _ _. A

    -- m : (a : A)(a' : A) → B a → B a' → C
    -- m a a (b : B a)(b' : B a)

  -- eta-reduction
  -- m : (Set → Set × Set) → Set
  -- m = _
  -- p = λ (f : Set → Set × Set) → m (λ x → f x .₁ , f x .₂) ≡ f Set .₁ ∋ refl
  --   =   p = λ (f : Set → Set × Set) → m f ≡ f Set .₁ ∋ refl

  -- doesn't work
  ------------------------------------------------------------

  -- non-linearity under pairing
  -- m : Set × Set × Set → Set
  -- m = _
  -- p = λ (A : Set)(B : Set) → m (A , B , B) ≡ A ∋ refl

  -- flipping
  -- m : (Set → Set → Set) → Set
  -- m = _
  -- p = λ (f : Set → Set → Set) → m (λ A B → f B A) ≡ f Set (Set → Set) ∋ refl

  -- projection under λ   (no full Skolemization)
  -- m : (Set → Set) → Set
  -- m = _
  -- p = λ (f : Set → Set × Set) → m (λ A → f A .₁) ≡ f Set .₁ ∋ refl

  -- flipping + projection
  -- m : (Set → Set × Set) → Set
  -- m = _
  -- p = λ (f : Set → Set × Set) → m (λ x → f x .₂ , f x .₁) ≡ f Set .₁ ∋ refl

max_stars_repo_name: AndrasKovacs/elaboration-zoo

max_issues_repo_name: lunalunaa/elaboration-zoo

max_forks_repo_name: lunalunaa/elaboration-zoo


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

module sets.unit where

open import level

record ⊤ {i : Level} : Set i where
  constructor tt

⊤-elim : ∀ {i j} (P : ⊤ {i} → Set j) → P tt → (x : ⊤) → P x
⊤-elim P ptt tt = ptt

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Ints.BiInvInt where

open import Cubical.HITs.Ints.BiInvInt.Base public

open import Cubical.HITs.Ints.BiInvInt.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import lib.Basics
open import lib.NType2
open import lib.PathGroupoid

open import lib.types.Bool
open import lib.types.IteratedSuspension
open import lib.types.Lift
open import lib.types.LoopSpace
open import lib.types.Nat
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.types.Suspension
open import lib.types.TLevel
open import lib.types.Unit

open SuspensionRec public using () renaming (f to Susp-rec)

open import nicolai.pseudotruncations.Preliminary-definitions
open import nicolai.pseudotruncations.Liblemmas

module nicolai.pseudotruncations.pointed-O-Sphere where

{- helper file for some technical things -}

module _ {i} where

  bool = fst (⊙Sphere {i} O)
  tt₀ : bool
  tt₀ = snd (⊙Sphere {i} O)
  ff₀ : bool
  ff₀ = lift false

module bool-neutral
           {i j}
           (P : bool {i} → Type j)
           (p₀ : P tt₀) where

  bool-pair : (P tt₀ × P ff₀) ≃ ((b : bool) → P b)
  bool-pair = equiv (λ tf → (λ { (lift true) → fst tf ; (lift false) → snd tf }))
                    (λ f → (f tt₀ , f ff₀))
                    (λ f → λ= (λ { (lift true) → idp ; (lift false) → idp }))
                    (λ tf → idp)

  pair-red : Σ (P tt₀ × P ff₀) (λ tf → fst tf == p₀) → P ff₀
  pair-red ((pt , pf) , q) = pf

  sing-exp : P ff₀ → Σ (P tt₀ × P ff₀) (λ tf → fst tf == p₀)
  sing-exp pf = ((p₀ , pf) , idp)

  red-exp : (pf : P ff₀) → pair-red (sing-exp pf) == pf
  red-exp _ = idp

  exp-red : (x : Σ (P tt₀ × P ff₀) (λ tf → fst tf == p₀)) → sing-exp (pair-red x) == x
  exp-red ((.p₀ , pf) , idp) = idp
  {- I tried to do it with pattern matching, but this does not introduce
     a dot [.] before [p₀]. Thus, is fails. Is this a bug? -}

  pair-one-determined : Σ (P tt₀ × P ff₀) (λ tf → fst tf == p₀) ≃ P ff₀
  pair-one-determined = equiv pair-red sing-exp red-exp exp-red

  {- This reduction result is (on paper) trivial, but for our formalization
     quite powerful! -}
  reduction : (Σ ((b : bool) → P b) λ g → g tt₀ == p₀)   ≃   P ff₀
  reduction = (Σ ((b : bool) → P b) λ g → g tt₀ == p₀)
                 ≃⟨ equiv-Σ-fst {A = P tt₀ × P ff₀}
                                {B = (b : bool) → P b}
                                (λ g → g tt₀ == p₀)
                                {h = fst bool-pair}
                                (snd bool-pair) ⁻¹ ⟩
               Σ (P tt₀ × P ff₀) ((λ g → g tt₀ == p₀) ∘ fst bool-pair)
                 ≃⟨ ide _ ⟩
               Σ (P tt₀ × P ff₀) (λ tf → fst tf == p₀)
                 ≃⟨ pair-one-determined ⟩
               P ff₀
                 ≃∎

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module plfa.part1.Relations where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm; +-identityʳ)

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ}
      --------
    → zero ≤ n

  s≤s : ∀ {m n : ℕ}
    → m ≤ n
      -------------
    → suc m ≤ suc n

infix 4 _≤_

inv-s≤s : ∀ {m n : ℕ}
  → suc m ≤ suc n
    -------------
  → m ≤ n
inv-s≤s (s≤s m≤n) = m≤n

inv-z≤n : ∀ {m : ℕ}
  → m ≤ zero
    --------
  → m ≡ zero
inv-z≤n z≤n = refl

≤-refl : ∀ {n} → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl

≤-trans : ∀ {m n p} → m ≤ n → n ≤ p → m ≤ p
≤-trans z≤n n = z≤n
≤-trans (s≤s m) (s≤s n) = s≤s (≤-trans m n)

≤-antisymm : ∀ {m n} → m ≤ n → n ≤ m → m ≡ n
≤-antisymm z≤n z≤n = refl
≤-antisymm (s≤s m) (s≤s n) = cong suc (≤-antisymm m n)

data Total (m n : ℕ) : Set where

  forward :
      m ≤ n
      ---------
    → Total m n

  flipped :
      n ≤ m
      ---------
    → Total m n

≤-total : ∀ (m n : ℕ) → Total m n
≤-total zero n = forward z≤n
≤-total (suc m) (zero) = flipped z≤n
≤-total (suc m) (suc n) with ≤-total m n
...                        | forward a = forward (s≤s a)
...                        | flipped b = flipped (s≤s b)

+-monoʳ-≤ : ∀ (n p q : ℕ)
  → p ≤ q
    -------------
  → n + p ≤ n + q
+-monoʳ-≤ zero    p q p≤q = p≤q
+-monoʳ-≤ (suc n) p q p≤q = s≤s (+-monoʳ-≤ n p q p≤q)

+-monoˡ-≤ : ∀ (m n p : ℕ)
  → m ≤ n
    -------------
  → m + p ≤ n + p
+-monoˡ-≤ m n p m≤n rewrite +-comm m p | +-comm n p = +-monoʳ-≤ p m n m≤n

+-mono-≤ : ∀ (m n p q : ℕ)
  → m ≤ n
  → p ≤ q
    -------------
  → m + p ≤ n + q
+-mono-≤ m n p q m≤n p≤q =
  ≤-trans (+-monoˡ-≤ m n p m≤n) (+-monoʳ-≤ n p q p≤q)

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  zero :
      ---------
      even zero

  suc  : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where

  suc  : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

e+e≡e : ∀ {m n : ℕ}
  → even m
  → even n
    ------------
  → even (m + n)

o+e≡o : ∀ {m n : ℕ}
  → odd m
  → even n
    -----------
  → odd (m + n)

e+e≡e zero     en  =  en
e+e≡e (suc om) en  =  suc (o+e≡o om en)

o+e≡o (suc em) en  =  suc (e+e≡e em en)

o+o≡e : ∀ {m n : ℕ}
  → odd m
  → odd n
  → even (m + n)
o+o≡e {suc a} {suc b} (suc m) (suc n)
  rewrite +-comm a (suc b) = suc (o+e≡o (suc n) m)

max_stars_repo_name: UnsoundWitch/proofs

max_issues_repo_name: sym-cereal/proofs

max_forks_repo_name: sym-cereal/proofs


text:
module Main where

import PolyDepPrelude
import Homogenous.Base
import Homogenous.Equality
import Homogenous.Reflexivity
import Homogenous.Nat
import Tools
import Reflexivity
import EqBase
import TYPE


text:
module Logic where

data True : Set where
  tt : True

infix 10 _/\_

data _/\_ (P Q : Set) : Set where
  <_,_> : P -> Q -> P /\ Q

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Mockingbird.Forest using (Forest)

-- Craig’s Discovery
module Mockingbird.Problems.Chapter20 {ℓb ℓ} (forest : Forest {ℓb} {ℓ}) where

open import Data.Product using (_,_)
open import Data.Vec using ([]; _∷_)
open import Function using (_$_)
open import Relation.Unary using (Pred; _∈_; _⊆_; _⊇_)

open Forest forest
open import Mockingbird.Forest.Birds forest
open import Mockingbird.Forest.Combination.Vec forest
open import Mockingbird.Forest.Combination.Vec.Properties forest
open import Mockingbird.Forest.Extensionality forest
import Mockingbird.Problems.Chapter11 forest as Chapter₁₁
open import Mockingbird.Problems.Chapter19 forest using (_≐_)

problem₁ : ⦃ _ : HasGoldfinch ⦄ ⦃ _ : HasIdentity ⦄ → HasQuirkyBird
problem₁ = record
  { Q₃ = G ∙ I
  ; isQuirkyBird = λ x y z → begin
      G ∙ I ∙ x ∙ y ∙ z  ≈⟨ isGoldfinch I x y z ⟩
      I ∙ z ∙ (x ∙ y)    ≈⟨ congʳ $ isIdentity z ⟩
      z ∙ (x ∙ y)        ∎
  }

problem₂′ : ⦃ _ : HasQuirkyBird ⦄ ⦃ _ : HasIdentity ⦄ → HasThrush
problem₂′ = record
  { T = Q₃ ∙ I
  ; isThrush = λ x y → begin
      Q₃ ∙ I ∙ x ∙ y  ≈⟨ isQuirkyBird I x y ⟩
      y ∙ (I ∙ x)     ≈⟨ congˡ $ isIdentity x ⟩
      y ∙ x           ∎
  }

problem₂ : ⦃ _ : HasGoldfinch ⦄ ⦃ _ : HasIdentity ⦄ → HasThrush
problem₂ = record
  { T = G ∙ I ∙ I
  ; isThrush = isThrush ⦃ problem₂′ ⦄
  } where
  instance hasQuirkyBird = problem₁

problem₃ : ⦃ _ : HasGoldfinch ⦄ ⦃ _ : HasIdentity ⦄ → HasCardinal
problem₃ = record
  { C = G ∙ G ∙ I ∙ I
  ; isCardinal = λ x y z → begin
      G ∙ G ∙ I ∙ I ∙ x ∙ y ∙ z  ≈⟨ congʳ $ congʳ $ isGoldfinch G I I x ⟩
      G ∙ x ∙ (I ∙ I) ∙ y ∙ z    ≈⟨ isGoldfinch x (I ∙ I) y z ⟩
      x ∙ z ∙ (I ∙ I ∙ y)        ≈⟨ congˡ $ congʳ $ isIdentity I ⟩
      x ∙ z ∙ (I ∙ y)            ≈⟨ congˡ $ isIdentity y ⟩
      x ∙ z ∙ y                  ∎
  }

problem₄-Q : ⦃ _ : HasGoldfinch ⦄ ⦃ _ : HasIdentity ⦄ → HasQueerBird
problem₄-Q = record
  { Q = G ∙ R ∙ Q₃
  ; isQueerBird = λ x y z → begin
      G ∙ R ∙ Q₃ ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isGoldfinch R Q₃ x y ⟩
      R ∙ y ∙ (Q₃ ∙ x) ∙ z    ≈⟨ isRobin y (Q₃ ∙ x) z ⟩
      Q₃ ∙ x ∙ z ∙ y          ≈⟨ isQuirkyBird x z y ⟩
      y ∙ (x ∙ z)             ∎
  } where
  instance
    hasQuirkyBird = problem₁
    hasCardinal = problem₃
    hasRobin = Chapter₁₁.problem₂₃

problem₄-B : ⦃ _ : HasGoldfinch ⦄ ⦃ _ : HasIdentity ⦄ → HasBluebird
problem₄-B = record
  { B = C ∙ Q
  ; isBluebird = λ x y z → begin
      C ∙ Q ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isCardinal Q x y ⟩
      Q ∙ y ∙ x ∙ z      ≈⟨ isQueerBird y x z ⟩
      x ∙ (y ∙ z)        ∎
  } where
  instance
    hasCardinal = problem₃
    hasQueerBird = problem₄-Q

module _ ⦃ _ : Extensional ⦄
         ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄
         ⦃ _ : HasIdentity ⦄ ⦃ _ : HasGoldfinch ⦄ where
  ⟨B,T,I⟩ = ⟨ B ∷ T ∷ I ∷ [] ⟩
  ⟨G,I⟩ = ⟨ G ∷ I ∷ [] ⟩

  module _ where
    private
      instance
        hasCardinal = Chapter₁₁.problem₂₁-bonus
        hasDove = Chapter₁₁.problem₅

      hasGoldfinch = Chapter₁₁.problem₄₇

      b : B ∈ ⟨B,T,I⟩
      b = [ here refl ]

      t : T ∈ ⟨B,T,I⟩
      t = [ there (here refl) ]

      i : I ∈ ⟨B,T,I⟩
      i = [ there (there (here refl)) ]

      c : C ∈ ⟨B,T,I⟩
      c = b ⟨∙⟩ (t ⟨∙⟩ (b ⟨∙⟩ b ⟨∙⟩ t)) ⟨∙⟩ (b ⟨∙⟩ b ⟨∙⟩ t)

      d : D ∈ ⟨B,T,I⟩
      d = b ⟨∙⟩ b

      g : G ∈ ⟨B,T,I⟩
      g = subst′
        (ext′ $ ext′ $ ext′ $ ext′ $ trans
          (isGoldfinch _ _ _ _)
          (sym $ isGoldfinch ⦃ hasGoldfinch ⦄ _ _ _ _))
        (d ⟨∙⟩ c)

    ⟨G,I⟩⊆⟨B,T,I⟩ : ⟨G,I⟩ ⊆ ⟨B,T,I⟩
    ⟨G,I⟩⊆⟨B,T,I⟩ [ here x≈G ] = subst′ x≈G g
    ⟨G,I⟩⊆⟨B,T,I⟩ [ there (here x≈I) ] = [ there (there (here x≈I)) ]
    ⟨G,I⟩⊆⟨B,T,I⟩ (x∈⟨G,I⟩ ⟨∙⟩ y∈⟨G,I⟩ ∣ xy≈z) =
      ⟨G,I⟩⊆⟨B,T,I⟩ x∈⟨G,I⟩ ⟨∙⟩ ⟨G,I⟩⊆⟨B,T,I⟩ y∈⟨G,I⟩ ∣ xy≈z

  module _ where
    private
      g : G ∈ ⟨G,I⟩
      g = [ here refl ]

      i : I ∈ ⟨G,I⟩
      i = [ there (here refl) ]

      t : T ∈ ⟨G,I⟩
      t = subst′
        (ext′ $ ext′ $ trans
          (isThrush _ _)
          (sym $ isThrush ⦃ problem₂ ⦄ _ _))
        (g ⟨∙⟩ i ⟨∙⟩ i)

      b : B ∈ ⟨G,I⟩
      b = subst′
        (ext′ $ ext′ $ ext′ $ trans
          (isBluebird _ _ _)
          (sym $ isBluebird ⦃ problem₄-B ⦄ _ _ _))
        (g ⟨∙⟩ g ⟨∙⟩ i ⟨∙⟩ i ⟨∙⟩ (g ⟨∙⟩ (g ⟨∙⟩ g ⟨∙⟩ i ⟨∙⟩ i ⟨∙⟩ (g ⟨∙⟩ g ⟨∙⟩ i ⟨∙⟩ i)) ⟨∙⟩ (g ⟨∙⟩ i)))

    ⟨G,I⟩⊇⟨B,T,I⟩ : ⟨G,I⟩ ⊇ ⟨B,T,I⟩
    ⟨G,I⟩⊇⟨B,T,I⟩ [ here x≈B ] = subst′ x≈B b
    ⟨G,I⟩⊇⟨B,T,I⟩ [ there (here x≈T) ] = subst′ x≈T t
    ⟨G,I⟩⊇⟨B,T,I⟩ [ there (there (here x≈I)) ] = [ there (here x≈I) ]
    ⟨G,I⟩⊇⟨B,T,I⟩ (x∈⟨B,T,I⟩ ⟨∙⟩ y∈⟨B,T,I⟩ ∣ xy≈z) = ⟨G,I⟩⊇⟨B,T,I⟩ x∈⟨B,T,I⟩ ⟨∙⟩ ⟨G,I⟩⊇⟨B,T,I⟩ y∈⟨B,T,I⟩ ∣ xy≈z

  ⟨G,I⟩≐⟨B,T,I⟩ : ⟨ G ∷ I ∷ [] ⟩ ≐ ⟨ B ∷ T ∷ I ∷ [] ⟩
  ⟨G,I⟩≐⟨B,T,I⟩ = (⟨G,I⟩⊆⟨B,T,I⟩ , ⟨G,I⟩⊇⟨B,T,I⟩)

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
------------------------------------------------------------------------
-- Bi-invertibility
------------------------------------------------------------------------

-- The development is based on the presentation of bi-invertibility
-- (for types and functions) and related things in the HoTT book.

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

open import Equality
open import Prelude hiding (id; _∘_)

-- The code is parametrised by something like a "raw" category.

module Bi-invertibility
  {e⁺}
  (eq : ∀ {a p} → Equality-with-J a p e⁺)
  {o h}
  (Obj : Type o)
  (Hom : Obj → Obj → Type h)
  (id : {A : Obj} → Hom A A)
  (_∘′_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C)
  where

open Derived-definitions-and-properties eq
open import Equivalence eq as Eq using (_≃_; Is-equivalence)
open import Function-universe eq as F hiding (id; _∘_)
open import Logical-equivalence using (_⇔_)
open import H-level eq
open import H-level.Closure eq
open import Preimage eq
open import Surjection eq using (_↠_)

private
  variable
    A B : Obj
    f   : Hom A B

  infixr 9 _∘_

  _∘_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C
  _∘_ = _∘′_

-- Has-left-inverse f means that f has a left inverse.

Has-left-inverse : Hom A B → Type h
Has-left-inverse f = ∃ λ f⁻¹ → f⁻¹ ∘ f ≡ id

-- Has-right-inverse f means that f has a right inverse.

Has-right-inverse : Hom A B → Type h
Has-right-inverse f = ∃ λ f⁻¹ → f ∘ f⁻¹ ≡ id

-- Is-bi-invertible f means that f has a left inverse and a (possibly
-- distinct) right inverse.

Is-bi-invertible : Hom A B → Type h
Is-bi-invertible f =
  Has-left-inverse f × Has-right-inverse f

-- Has-quasi-inverse f means that f has a left inverse that is also a
-- right inverse.

Has-quasi-inverse : Hom A B → Type h
Has-quasi-inverse f =
  ∃ λ f⁻¹ → f ∘ f⁻¹ ≡ id × f⁻¹ ∘ f ≡ id

-- Some notions of isomorphism or equivalence.

infix 4 _≊_ _≅_

_≊_ : Obj → Obj → Type h
A ≊ B = ∃ λ (f : Hom A B) → Is-bi-invertible f

_≅_ : Obj → Obj → Type h
A ≅ B = ∃ λ (f : Hom A B) → Has-quasi-inverse f

-- Morphisms with quasi-inverses are bi-invertible.

Has-quasi-inverse→Is-bi-invertible :
  (f : Hom A B) → Has-quasi-inverse f → Is-bi-invertible f
Has-quasi-inverse→Is-bi-invertible _ (f⁻¹ , f∘f⁻¹≡id , f⁻¹∘f≡id) =
    (f⁻¹ , f⁻¹∘f≡id)
  , (f⁻¹ , f∘f⁻¹≡id)

≅→≊ : A ≅ B → A ≊ B
≅→≊ = ∃-cong Has-quasi-inverse→Is-bi-invertible

-- The remaining code relies on some further assumptions, similar to
-- those of a precategory. However, note that Hom A B is not required
-- to be a set (some properties require Hom A A to be a set for some
-- A).

module More
  (left-identity  : {A B : Obj} (f : Hom A B) → id ∘ f ≡ f)
  (right-identity : {A B : Obj} (f : Hom A B) → f ∘ id ≡ f)
  (associativity  : {A B C D : Obj}
                    (f : Hom C D) (g : Hom B C) (h : Hom A B) →
                    f ∘ (g ∘ h) ≡ (f ∘ g) ∘ h)
  where

  -- Bi-invertible morphisms have quasi-inverses.

  Is-bi-invertible→Has-quasi-inverse :
    Is-bi-invertible f → Has-quasi-inverse f
  Is-bi-invertible→Has-quasi-inverse
    {f = f} ((f⁻¹₁ , f⁻¹₁∘f≡id) , (f⁻¹₂ , f∘f⁻¹₂≡id)) =
      (f⁻¹₁ ∘ f ∘ f⁻¹₂)
    , (f ∘ f⁻¹₁ ∘ f ∘ f⁻¹₂    ≡⟨ cong (f ∘_) $ associativity _ _ _ ⟩
       f ∘ (f⁻¹₁ ∘ f) ∘ f⁻¹₂  ≡⟨ cong (λ f′ → f ∘ f′ ∘ f⁻¹₂) f⁻¹₁∘f≡id ⟩
       f ∘ id ∘ f⁻¹₂          ≡⟨ cong (f ∘_) $ left-identity _ ⟩
       f ∘ f⁻¹₂               ≡⟨ f∘f⁻¹₂≡id ⟩∎
       id                     ∎)
    , ((f⁻¹₁ ∘ f ∘ f⁻¹₂) ∘ f  ≡⟨ cong (λ f′ → (f⁻¹₁ ∘ f′) ∘ f) f∘f⁻¹₂≡id ⟩
       (f⁻¹₁ ∘ id) ∘ f        ≡⟨ cong (_∘ f) $ right-identity _ ⟩
       f⁻¹₁ ∘ f               ≡⟨ f⁻¹₁∘f≡id ⟩∎
       id                     ∎)

  -- Has-left-inverse f is contractible if f has a quasi-inverse.

  Has-left-inverse-contractible :
    Has-quasi-inverse f → Contractible (Has-left-inverse f)
  Has-left-inverse-contractible
    {f = f} (f⁻¹ , f∘f⁻¹≡id , f⁻¹∘f≡id) =
    bijection⁻¹-contractible (record
      { surjection = record
        { logical-equivalence = record
          { to   = _∘ f
          ; from = _∘ f⁻¹
          }
        ; right-inverse-of = λ g →
            (g ∘ f⁻¹) ∘ f  ≡⟨ sym $ associativity _ _ _ ⟩
            g ∘ f⁻¹ ∘ f    ≡⟨ cong (g ∘_) f⁻¹∘f≡id ⟩
            g ∘ id         ≡⟨ right-identity _ ⟩∎
            g              ∎
        }
      ; left-inverse-of = λ g →
          (g ∘ f) ∘ f⁻¹  ≡⟨ sym $ associativity _ _ _ ⟩
          g ∘ f ∘ f⁻¹    ≡⟨ cong (g ∘_) f∘f⁻¹≡id ⟩
          g ∘ id         ≡⟨ right-identity _ ⟩∎
          g              ∎
      })
      id

  -- Has-right-inverse f is contractible if f has a quasi-inverse.

  Has-right-inverse-contractible :
    Has-quasi-inverse f → Contractible (Has-right-inverse f)
  Has-right-inverse-contractible
    {f = f} (f⁻¹ , f∘f⁻¹≡id , f⁻¹∘f≡id) =
    bijection⁻¹-contractible (record
      { surjection = record
        { logical-equivalence = record
          { to   = f ∘_
          ; from = f⁻¹ ∘_
          }
        ; right-inverse-of = λ g →
            f ∘ f⁻¹ ∘ g    ≡⟨ associativity _ _ _ ⟩
            (f ∘ f⁻¹) ∘ g  ≡⟨ cong (_∘ g) f∘f⁻¹≡id ⟩
            id ∘ g         ≡⟨ left-identity _ ⟩∎
            g              ∎
        }
      ; left-inverse-of = λ g →
          f⁻¹ ∘ f ∘ g    ≡⟨ associativity _ _ _ ⟩
          (f⁻¹ ∘ f) ∘ g  ≡⟨ cong (_∘ g) f⁻¹∘f≡id ⟩
          id ∘ g         ≡⟨ left-identity _ ⟩∎
          g              ∎
      })
      id

  -- Is-bi-invertible f is a proposition.

  Is-bi-invertible-propositional :
    (f : Hom A B) → Is-proposition (Is-bi-invertible f)
  Is-bi-invertible-propositional f =
    [inhabited⇒+]⇒+ 0 λ b →
      let q = Is-bi-invertible→Has-quasi-inverse b in
      mono₁ 0 $
      ×-closure 0
        (Has-left-inverse-contractible  q)
        (Has-right-inverse-contractible q)

  -- If Hom A A is a set, where A is the domain of f, then
  -- Has-quasi-inverse f is a proposition.

  Has-quasi-inverse-propositional-domain :
    {f : Hom A B} →
    Is-set (Hom A A) →
    Is-proposition (Has-quasi-inverse f)
  Has-quasi-inverse-propositional-domain {f = f} s =              $⟨ (λ inv → Σ-closure 1
                                                                                (mono₁ 0 $ Has-right-inverse-contractible inv)
                                                                                (λ _ → s)) ⟩
    (Has-quasi-inverse f →
     Is-proposition (∃ λ ((f⁻¹ , _) : Has-right-inverse f) →
                       f⁻¹ ∘ f ≡ id))                             ↝⟨ (∀-cong _ λ _ → H-level-cong _ 1 (inverse Σ-assoc)) ⟩

    (Has-quasi-inverse f → Is-proposition (Has-quasi-inverse f))  ↝⟨ [inhabited⇒+]⇒+ 0 ⟩□

    Is-proposition (Has-quasi-inverse f)                          □

  -- If Hom B B is a set, where B is the codomain of f, then
  -- Has-quasi-inverse f is a proposition.

  Has-quasi-inverse-propositional-codomain :
    {f : Hom A B} →
    Is-set (Hom B B) →
    Is-proposition (Has-quasi-inverse f)
  Has-quasi-inverse-propositional-codomain {f = f} s =            $⟨ (λ inv → Σ-closure 1
                                                                                (mono₁ 0 $ Has-left-inverse-contractible inv)
                                                                                (λ _ → s)) ⟩
    (Has-quasi-inverse f →
     Is-proposition (∃ λ ((f⁻¹ , _) : Has-left-inverse f) →
                       f ∘ f⁻¹ ≡ id))                             ↝⟨ (∀-cong _ λ _ → H-level-cong _ 1 lemma) ⟩

    (Has-quasi-inverse f → Is-proposition (Has-quasi-inverse f))  ↝⟨ [inhabited⇒+]⇒+ 0 ⟩□

    Is-proposition (Has-quasi-inverse f)                          □
    where
    lemma =
      (∃ λ ((f⁻¹ , _) : Has-left-inverse f) → f ∘ f⁻¹ ≡ id)      ↔⟨⟩
      (∃ λ ((f⁻¹ , _) : ∃ λ f⁻¹ → f⁻¹ ∘ f ≡ id) → f ∘ f⁻¹ ≡ id)  ↝⟨ inverse Σ-assoc ⟩
      (∃ λ f⁻¹ → f⁻¹ ∘ f ≡ id × f ∘ f⁻¹ ≡ id)                    ↝⟨ (∃-cong λ _ → ×-comm) ⟩
      (∃ λ f⁻¹ → f ∘ f⁻¹ ≡ id × f⁻¹ ∘ f ≡ id)                    ↔⟨⟩
      Has-quasi-inverse f                                        □

  -- There is a split surjection from Has-quasi-inverse f to
  -- Is-bi-invertible f.

  Has-quasi-inverse↠Is-bi-invertible :
    Has-quasi-inverse f ↠ Is-bi-invertible f
  Has-quasi-inverse↠Is-bi-invertible = record
    { logical-equivalence = record
      { to   = Has-quasi-inverse→Is-bi-invertible _
      ; from = Is-bi-invertible→Has-quasi-inverse
      }
    ; right-inverse-of = λ _ → Is-bi-invertible-propositional _ _ _
    }

  -- There is a split surjection from A ≅ B to A ≊ B.

  ≅↠≊ : (A ≅ B) ↠ (A ≊ B)
  ≅↠≊ = ∃-cong λ _ → Has-quasi-inverse↠Is-bi-invertible

  -- Is-bi-invertible and Has-quasi-inverse are equivalent for
  -- morphisms with domain A for which Hom A A is a set.

  Is-bi-invertible≃Has-quasi-inverse-domain :
    {f : Hom A B} →
    Is-set (Hom A A) →
    Is-bi-invertible f ≃ Has-quasi-inverse f
  Is-bi-invertible≃Has-quasi-inverse-domain s =
    inverse $ Eq.↔⇒≃ (record
      { surjection = Has-quasi-inverse↠Is-bi-invertible
      ; left-inverse-of = λ _ →
          Has-quasi-inverse-propositional-domain s _ _
      })

  -- Is-bi-invertible and Has-quasi-inverse are equivalent for
  -- morphisms with codomain B for which Hom B B is a set.

  Is-bi-invertible≃Has-quasi-inverse-codomain :
    {f : Hom A B} →
    Is-set (Hom B B) →
    Is-bi-invertible f ≃ Has-quasi-inverse f
  Is-bi-invertible≃Has-quasi-inverse-codomain s =
    inverse $ Eq.↔⇒≃ (record
      { surjection = Has-quasi-inverse↠Is-bi-invertible
      ; left-inverse-of = λ _ →
          Has-quasi-inverse-propositional-codomain s _ _
      })

  -- A ≊ B and A ≅ B are equivalent if Hom A A is a set.

  ≊≃≅-domain :
    Is-set (Hom A A) →
    (A ≊ B) ≃ (A ≅ B)
  ≊≃≅-domain s =
    ∃-cong λ _ → Is-bi-invertible≃Has-quasi-inverse-domain s

  -- A ≊ B and A ≅ B are equivalent if Hom B B is a set.

  ≊≃≅-codomain :
    Is-set (Hom B B) →
    (A ≊ B) ≃ (A ≅ B)
  ≊≃≅-codomain s =
    ∃-cong λ _ → Is-bi-invertible≃Has-quasi-inverse-codomain s

  -- An equality characterisation lemma for _≊_.

  equality-characterisation-≊ :
    (f g : A ≊ B) → (f ≡ g) ≃ (proj₁ f ≡ proj₁ g)
  equality-characterisation-≊ _ _ =
    Eq.↔⇒≃ $ inverse $ ignore-propositional-component $
      Is-bi-invertible-propositional _

  -- Two equality characterisation lemmas for _≅_.

  equality-characterisation-≅-domain :
    Is-set (Hom A A) →
    (f g : A ≅ B) → (f ≡ g) ≃ (proj₁ f ≡ proj₁ g)
  equality-characterisation-≅-domain s _ _ =
    Eq.↔⇒≃ $ inverse $ ignore-propositional-component $
      Has-quasi-inverse-propositional-domain s

  equality-characterisation-≅-codomain :
    Is-set (Hom B B) →
    (f g : A ≅ B) → (f ≡ g) ≃ (proj₁ f ≡ proj₁ g)
  equality-characterisation-≅-codomain s _ _ =
    Eq.↔⇒≃ $ inverse $ ignore-propositional-component $
      Has-quasi-inverse-propositional-codomain s

  -- If f : Hom A B has a quasi-inverse, then Has-quasi-inverse f is
  -- equivalent to id ≡ id, where id stands for either the identity at
  -- A or at B.

  Has-quasi-inverse≃id≡id-domain :
    {f : Hom A B} →
    Has-quasi-inverse f →
    Has-quasi-inverse f ≃ (id ≡ id {A = A})
  Has-quasi-inverse≃id≡id-domain {f = f} q-inv@(f⁻¹ , _ , f⁻¹∘f≡id) =
    Has-quasi-inverse f                                     ↔⟨ Σ-assoc ⟩
    (∃ λ ((f⁻¹ , _) : Has-right-inverse f) → f⁻¹ ∘ f ≡ id)  ↔⟨ drop-⊤-left-Σ (_⇔_.to contractible⇔↔⊤ $ Has-right-inverse-contractible q-inv) ⟩
    (f⁻¹ ∘ id) ∘ f ≡ id                                     ↝⟨ ≡⇒↝ _ $ cong (λ f′ → f′ ∘ _ ≡ _) $ right-identity _ ⟩
    f⁻¹ ∘ f ≡ id                                            ↝⟨ ≡⇒↝ _ $ cong (_≡ _) f⁻¹∘f≡id ⟩□
    id ≡ id                                                 □

  Has-quasi-inverse≃id≡id-codomain :
    {f : Hom A B} →
    Has-quasi-inverse f →
    Has-quasi-inverse f ≃ (id ≡ id {A = B})
  Has-quasi-inverse≃id≡id-codomain {f = f} q-inv@(f⁻¹ , f∘f⁻¹≡id , _) =
    Has-quasi-inverse f                                    ↔⟨ Σ-assoc F.∘ (∃-cong λ _ → ×-comm) ⟩
    (∃ λ ((f⁻¹ , _) : Has-left-inverse f) → f ∘ f⁻¹ ≡ id)  ↔⟨ drop-⊤-left-Σ (_⇔_.to contractible⇔↔⊤ $ Has-left-inverse-contractible q-inv) ⟩
    f ∘ id ∘ f⁻¹ ≡ id                                      ↝⟨ ≡⇒↝ _ $ cong (λ f′ → _ ∘ f′ ≡ _) $ left-identity _ ⟩
    f ∘ f⁻¹ ≡ id                                           ↝⟨ ≡⇒↝ _ $ cong (_≡ _) f∘f⁻¹≡id ⟩□
    id ≡ id                                                □

  ----------------------------------------------------------------------
  -- Univalence

  -- The relation _≅_ is reflexive.

  id-≅ : A ≅ A
  id-≅ = id , id , left-identity id , right-identity id

  -- Equal objects are related by _≅_.

  ≡→≅ : A ≡ B → A ≅ B
  ≡→≅ = elim (λ {A B} _ → A ≅ B) (λ _ → id-≅)

  -- A "computation" rule for ≡→≅.

  ≡→≅-refl : ≡→≅ (refl A) ≡ id-≅
  ≡→≅-refl = elim-refl _ _

  -- A notion of univalence, defined using _≅_.

  Univalence-≅ : Type (o ⊔ h)
  Univalence-≅ = {A B : Obj} → Is-equivalence (≡→≅ {A = A} {B = B})

  -- If equality is equivalent to _≅_, then univalence holds.

  ≡≃≅→Univalence-≅ :
    (∀ {A B} → (A ≡ B) ≃ (A ≅ B)) →
    Univalence-≅
  ≡≃≅→Univalence-≅ ≡≃≅ =
    Eq.≡≃→≡→→Is-equivalence (_ ≅_) ≡≃≅ ≡→≅

  -- The relation _≊_ is reflexive.

  id-≊ : A ≊ A
  id-≊ = id , (id , left-identity id) , (id , right-identity id)

  -- Equal objects are related by _≊_.

  ≡→≊ : A ≡ B → A ≊ B
  ≡→≊ = elim (λ {A B} _ → A ≊ B) (λ _ → id-≊)

  -- A "computation" rule for ≡→≊.

  ≡→≊-refl : ≡→≊ (refl A) ≡ id-≊
  ≡→≊-refl = elim-refl _ _

  -- A notion of univalence, defined using _≊_.

  Univalence-≊ : Type (o ⊔ h)
  Univalence-≊ = {A B : Obj} → Is-equivalence (≡→≊ {A = A} {B = B})

  -- If equality is equivalent to _≊_, then univalence holds.

  ≡≃≊→Univalence-≊ :
    (∀ {A B} → (A ≡ B) ≃ (A ≊ B)) →
    Univalence-≊
  ≡≃≊→Univalence-≊ ≡≃≊ =
    Eq.≡≃→≡→→Is-equivalence (_ ≊_) ≡≃≊ ≡→≊

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties for distributive lattice
------------------------------------------------------------------------

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

open import Relation.Binary.Lattice

module Relation.Binary.Properties.DistributiveLattice
  {c ℓ₁ ℓ₂} (L : DistributiveLattice c ℓ₁ ℓ₂) where

open DistributiveLattice L hiding (refl)

open import Algebra.FunctionProperties _≈_
open import Data.Product using (_,_)
open import Relation.Binary
open import Relation.Binary.Reasoning.Setoid setoid
open import Relation.Binary.Properties.Lattice lattice
open import Relation.Binary.Properties.MeetSemilattice meetSemilattice
open import Relation.Binary.Properties.JoinSemilattice joinSemilattice

open Setoid setoid

∧-distribʳ-∨ : _∧_ DistributesOverʳ _∨_
∧-distribʳ-∨ x y z = begin
  (y ∨ z) ∧ x    ≈⟨ ∧-comm _ _ ⟩
  x ∧ (y ∨ z)    ≈⟨ ∧-distribˡ-∨ x y z ⟩
  x ∧ y ∨ x ∧ z  ≈⟨ ∨-cong (∧-comm _ _) (∧-comm _ _) ⟩
  y ∧ x ∨ z ∧ x  ∎

∧-distrib-∨ : _∧_ DistributesOver _∨_
∧-distrib-∨ = ∧-distribˡ-∨ , ∧-distribʳ-∨

∨-distribˡ-∧ : _∨_ DistributesOverˡ _∧_
∨-distribˡ-∧ x y z = begin
  x ∨ y ∧ z                  ≈⟨ ∨-cong (sym (∨-absorbs-∧ x y)) refl ⟩
  (x ∨ x ∧ y) ∨ y ∧ z        ≈⟨ ∨-cong (∨-cong refl (∧-comm _ _)) refl ⟩
  (x ∨ y ∧ x) ∨ y ∧ z        ≈⟨ ∨-assoc x (y ∧ x) (y ∧ z) ⟩
  x ∨ y ∧ x ∨ y ∧ z          ≈⟨ ∨-cong refl (sym (∧-distribˡ-∨ y x z)) ⟩
  x ∨ y ∧ (x ∨ z)            ≈⟨ ∨-cong (sym (∧-absorbs-∨ _ _)) refl ⟩
  x ∧ (x ∨ z) ∨ y ∧ (x ∨ z)  ≈⟨ sym (∧-distribʳ-∨ (x ∨ z) x y) ⟩
  (x ∨ y) ∧ (x ∨ z)          ∎

∨-distribʳ-∧ : _∨_ DistributesOverʳ _∧_
∨-distribʳ-∧ x y z = begin
  y ∧ z ∨ x          ≈⟨ ∨-comm _ _ ⟩
  x ∨ y ∧ z          ≈⟨ ∨-distribˡ-∧ _ _ _ ⟩
  (x ∨ y) ∧ (x ∨ z)  ≈⟨ ∧-cong (∨-comm _ _) (∨-comm _ _) ⟩
  (y ∨ x) ∧ (z ∨ x)  ∎

∨-distrib-∧ : _∨_ DistributesOver _∧_
∨-distrib-∧ = ∨-distribˡ-∧ , ∨-distribʳ-∧