text:
module Pi0 where

open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product

open import Groupoid

infixr 10 _◎_
infixr 30 _⟷_

------------------------------------------------------------------------------
-- Level 0:
-- Types at this level are just plain sets with no interesting path structure.
-- The path structure is defined at levels 1 and beyond.

data U : Set where
  ZERO  : U
  ONE   : U
  PLUS  : U → U → U
  TIMES : U → U → U

⟦_⟧ : U → Set
⟦ ZERO ⟧        = ⊥
⟦ ONE ⟧         = ⊤
⟦ PLUS t₁ t₂ ⟧  = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
⟦ TIMES t₁ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧

-- Programs
-- We use pointed types; programs map a pointed type to another
-- In other words, each program takes one particular value to another; if we
-- want to work on another value, we generally use another program

record U• : Set where
  constructor •[_,_]
  field
    ∣_∣ : U
    • : ⟦ ∣_∣ ⟧

open U•

Space : (t• : U•) → Set
Space •[ t , v ] = ⟦ t ⟧

point : (t• : U•) → Space t•
point •[ t , v ] = v

-- examples of plain types, values, and pointed types

ONE• : U•
ONE• = •[ ONE , tt ]

BOOL : U
BOOL = PLUS ONE ONE

BOOL² : U
BOOL² = TIMES BOOL BOOL

TRUE : ⟦ BOOL ⟧
TRUE = inj₁ tt

FALSE : ⟦ BOOL ⟧
FALSE = inj₂ tt

BOOL•F : U•
BOOL•F = •[ BOOL , FALSE ]

BOOL•T : U•
BOOL•T = •[ BOOL , TRUE ]

-- The actual programs are the commutative semiring isomorphisms between
-- pointed types.

data _⟷_ : U• → U• → Set where
  unite₊  : ∀ {t v} → •[ PLUS ZERO t , inj₂ v ] ⟷ •[ t , v ]
  uniti₊  : ∀ {t v} → •[ t , v ] ⟷ •[ PLUS ZERO t , inj₂ v ]
  swap1₊  : ∀ {t₁ t₂ v₁} → •[ PLUS t₁ t₂ , inj₁ v₁ ] ⟷ •[ PLUS t₂ t₁ , inj₂ v₁ ]
  swap2₊  : ∀ {t₁ t₂ v₂} → •[ PLUS t₁ t₂ , inj₂ v₂ ] ⟷ •[ PLUS t₂ t₁ , inj₁ v₂ ]
  assocl1₊ : ∀ {t₁ t₂ t₃ v₁} →
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₁ v₁ ] ⟷
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ]
  assocl2₊ : ∀ {t₁ t₂ t₃ v₂} →
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₁ v₂) ] ⟷
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ]
  assocl3₊ : ∀ {t₁ t₂ t₃ v₃} →
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₂ v₃) ] ⟷
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₂ v₃ ]
  assocr1₊ : ∀ {t₁ t₂ t₃ v₁} →
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ] ⟷
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₁ v₁ ]
  assocr2₊ : ∀ {t₁ t₂ t₃ v₂} →
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ] ⟷
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₁ v₂) ]
  assocr3₊ : ∀ {t₁ t₂ t₃ v₃} →
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₂ v₃ ] ⟷
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₂ v₃) ]
  unite⋆  : ∀ {t v} → •[ TIMES ONE t , (tt , v) ] ⟷ •[ t , v ]
  uniti⋆  : ∀ {t v} → •[ t , v ] ⟷ •[ TIMES ONE t , (tt , v) ]
  swap⋆   : ∀ {t₁ t₂ v₁ v₂} →
              •[ TIMES t₁ t₂ , (v₁ , v₂) ] ⟷ •[ TIMES t₂ t₁ , (v₂ , v₁) ]
  assocl⋆ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
            •[ TIMES t₁ (TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ] ⟷
            •[ TIMES (TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ]
  assocr⋆ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
            •[ TIMES (TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ] ⟷
            •[ TIMES t₁ (TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ]
  distz : ∀ {t v absurd} →
            •[ TIMES ZERO t , (absurd , v) ] ⟷ •[ ZERO , absurd ]
  factorz : ∀ {t v absurd} →
            •[ ZERO , absurd ] ⟷ •[ TIMES ZERO t , (absurd , v) ]
  dist1   : ∀ {t₁ t₂ t₃ v₁ v₃} →
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ] ⟷
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₁ (v₁ , v₃) ]
  dist2   : ∀ {t₁ t₂ t₃ v₂ v₃} →
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ] ⟷
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₂ (v₂ , v₃) ]
  factor1   : ∀ {t₁ t₂ t₃ v₁ v₃} →
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₁ (v₁ , v₃) ] ⟷
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ]
  factor2   : ∀ {t₁ t₂ t₃ v₂ v₃} →
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₂ (v₂ , v₃) ] ⟷
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ]
  id⟷    : ∀ {t v} → •[ t , v ] ⟷ •[ t , v ]
  sym⟷   : ∀ {t₁ t₂ v₁ v₂} → (•[ t₁ , v₁ ] ⟷ •[ t₂ , v₂ ]) →
           (•[ t₂ , v₂ ] ⟷ •[ t₁ , v₁ ])
  _◎_    : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} → (•[ t₁ , v₁ ] ⟷ •[ t₂ , v₂ ]) →
           (•[ t₂ , v₂ ] ⟷ •[ t₃ , v₃ ]) →
           (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ])
  _⊕1_   : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
           (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ]) → (•[ t₂ , v₂ ] ⟷ •[ t₄ , v₄ ]) →
           (•[ PLUS t₁ t₂ , inj₁ v₁ ] ⟷ •[ PLUS t₃ t₄ , inj₁ v₃ ])
  _⊕2_   : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
           (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ]) → (•[ t₂ , v₂ ] ⟷ •[ t₄ , v₄ ]) →
           (•[ PLUS t₁ t₂ , inj₂ v₂ ] ⟷ •[ PLUS t₃ t₄ , inj₂ v₄ ])
  _⊗_     : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
           (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ]) → (•[ t₂ , v₂ ] ⟷ •[ t₄ , v₄ ]) →
          (•[ TIMES t₁ t₂ , (v₁ , v₂) ] ⟷ •[ TIMES t₃ t₄ , (v₃ , v₄) ])

-- example programs

NOT•T : •[ BOOL , TRUE ] ⟷ •[ BOOL , FALSE ]
NOT•T = swap1₊

NOT•F : •[ BOOL , FALSE ] ⟷ •[ BOOL , TRUE ]
NOT•F = swap2₊

CNOT•Fx : {b : ⟦ BOOL ⟧} →
          •[ BOOL² , (FALSE , b) ] ⟷ •[ BOOL² , (FALSE , b) ]
CNOT•Fx = dist2 ◎ ((id⟷ ⊗ NOT•F) ⊕2 id⟷) ◎ factor2

CNOT•TF : •[ BOOL² , (TRUE , FALSE) ] ⟷ •[ BOOL² , (TRUE , TRUE) ]
CNOT•TF = dist1 ◎
          ((id⟷ ⊗ NOT•F) ⊕1 (id⟷ {TIMES ONE BOOL} {(tt , TRUE)})) ◎
          factor1

CNOT•TT : •[ BOOL² , (TRUE , TRUE) ] ⟷ •[ BOOL² , (TRUE , FALSE) ]
CNOT•TT = dist1 ◎
          ((id⟷ ⊗ NOT•T) ⊕1 (id⟷ {TIMES ONE BOOL} {(tt , TRUE)})) ◎
          factor1

-- The evaluation of a program is not done in order to figure out the output
-- value. Both the input and output values are encoded in the type of the
-- program; what the evaluation does is follow the path to constructively
-- reach the ouput value from the input value. Even though programs of the
-- same pointed types are, by definition, observationally equivalent, they
-- may follow different paths. At this point, we simply declare that all such
-- programs are "the same." At the next level, we will weaken this "path
-- irrelevant" equivalence and reason about which paths can be equated to
-- other paths via 2paths etc.

-- Even though individual types are sets, the universe of types is a
-- groupoid. The objects of this groupoid are the pointed types; the
-- morphisms are the programs; and the equivalence of programs is the
-- degenerate observational equivalence that equates every two programs that
-- are extensionally equivalent.

_obs≅_ : {t₁ t₂ : U•} → (c₁ c₂ : t₁ ⟷ t₂) → Set
c₁ obs≅ c₂ = ⊤

UG : 1Groupoid
UG = record
       { set = U•
       ; _↝_ = _⟷_
       ; _≈_ = _obs≅_
       ; id = id⟷
       ; _∘_ = λ y⟷z x⟷y → x⟷y ◎ y⟷z
       ; _⁻¹ = sym⟷
       ; lneutr = λ _ → tt
       ; rneutr = λ _ → tt
       ; assoc = λ _ _ _ → tt
       ; equiv = record { refl = tt
                        ; sym = λ _ → tt
                        ; trans = λ _ _ → tt
                        }
       ; linv = λ _ → tt
       ; rinv = λ _ → tt
       ; ∘-resp-≈ = λ _ _ → tt
       }

------------------------------------------------------------------------------
-- Simplifiy various compositions

simplifySym : {t₁ t₂ : U•} → (c₁ : t₁ ⟷ t₂) → (t₂ ⟷ t₁)
simplifySym unite₊ = uniti₊
simplifySym uniti₊ = unite₊
simplifySym swap1₊ = swap2₊
simplifySym swap2₊ = swap1₊
simplifySym assocl1₊ = assocr1₊
simplifySym assocl2₊ = assocr2₊
simplifySym assocl3₊ = assocr3₊
simplifySym assocr1₊ = assocl1₊
simplifySym assocr2₊ = assocl2₊
simplifySym assocr3₊ = assocl3₊
simplifySym unite⋆ = uniti⋆
simplifySym uniti⋆ = unite⋆
simplifySym swap⋆ = swap⋆
simplifySym assocl⋆ = assocr⋆
simplifySym assocr⋆ = assocl⋆
simplifySym distz = factorz
simplifySym factorz = distz
simplifySym dist1 = factor1
simplifySym dist2 = factor2
simplifySym factor1 = dist1
simplifySym factor2 = dist2
simplifySym id⟷ = id⟷
simplifySym (sym⟷ c) = c
simplifySym (c₁ ◎ c₂) = simplifySym c₂ ◎ simplifySym c₁
simplifySym (c₁ ⊕1 c₂) = simplifySym c₁ ⊕1 simplifySym c₂
simplifySym (c₁ ⊕2 c₂) = simplifySym c₁ ⊕2 simplifySym c₂
simplifySym (c₁ ⊗ c₂) = simplifySym c₁ ⊗ simplifySym c₂

simplifyl◎ : {t₁ t₂ t₃ : U•} → (c₁ : t₁ ⟷ t₂) → (c₂ : t₂ ⟷ t₃) → (t₁ ⟷ t₃)
simplifyl◎ id⟷ c = c
simplifyl◎ unite₊ uniti₊ = id⟷
simplifyl◎ uniti₊ unite₊ = id⟷
simplifyl◎ swap1₊ swap2₊ = id⟷
simplifyl◎ swap2₊ swap1₊ = id⟷
simplifyl◎ assocl1₊ assocr1₊ = id⟷
simplifyl◎ assocl2₊ assocr2₊ = id⟷
simplifyl◎ assocl3₊ assocr3₊ = id⟷
simplifyl◎ assocr1₊ assocl1₊ = id⟷
simplifyl◎ assocr2₊ assocl2₊ = id⟷
simplifyl◎ assocr3₊ assocl3₊ = id⟷
simplifyl◎ unite⋆ uniti⋆ = id⟷
simplifyl◎ uniti⋆ unite⋆ = id⟷
simplifyl◎ swap⋆ swap⋆ = id⟷
simplifyl◎ assocl⋆ assocr⋆ = id⟷
simplifyl◎ assocr⋆ assocl⋆ = id⟷
simplifyl◎ factorz distz = id⟷
simplifyl◎ dist1 factor1 = id⟷
simplifyl◎ dist2 factor2 = id⟷
simplifyl◎ factor1 dist1 = id⟷
simplifyl◎ factor2 dist2 = id⟷
simplifyl◎ (c₁ ◎ c₂) c₃ = c₁ ◎ (c₂ ◎ c₃)
simplifyl◎ (c₁ ⊕1 c₂) swap1₊ = swap1₊ ◎ (c₂ ⊕2 c₁)
simplifyl◎ (c₁ ⊕2 c₂) swap2₊ = swap2₊ ◎ (c₂ ⊕1 c₁)
simplifyl◎ (_⊗_ {ONE} c₁ c₂) unite⋆ = unite⋆ ◎ c₂
simplifyl◎ (c₁ ⊗ c₂) swap⋆ = swap⋆ ◎ (c₂ ⊗ c₁)
simplifyl◎ (c₁ ⊗ c₂) (c₃ ⊗ c₄) = (c₁ ◎ c₃) ⊗ (c₂ ◎ c₄)
simplifyl◎ c₁ c₂ = c₁ ◎ c₂

simplifyr◎ : {t₁ t₂ t₃ : U•} → (c₁ : t₁ ⟷ t₂) → (c₂ : t₂ ⟷ t₃) → (t₁ ⟷ t₃)
simplifyr◎ c id⟷ = c
simplifyr◎ unite₊ uniti₊ = id⟷
simplifyr◎ uniti₊ unite₊ = id⟷
simplifyr◎ swap1₊ swap2₊ = id⟷
simplifyr◎ swap2₊ swap1₊ = id⟷
simplifyr◎ assocl1₊ assocr1₊ = id⟷
simplifyr◎ assocl2₊ assocr2₊ = id⟷
simplifyr◎ assocl3₊ assocr3₊ = id⟷
simplifyr◎ assocr1₊ assocl1₊ = id⟷
simplifyr◎ assocr2₊ assocl2₊ = id⟷
simplifyr◎ assocr3₊ assocl3₊ = id⟷
simplifyr◎ unite⋆ uniti⋆ = id⟷
simplifyr◎ uniti⋆ unite⋆ = id⟷
simplifyr◎ swap⋆ swap⋆ = id⟷
simplifyr◎ assocl⋆ assocr⋆ = id⟷
simplifyr◎ assocr⋆ assocl⋆ = id⟷
simplifyr◎ factorz distz = id⟷
simplifyr◎ dist1 factor1 = id⟷
simplifyr◎ dist2 factor2 = id⟷
simplifyr◎ factor1 dist1 = id⟷
simplifyr◎ factor2 dist2 = id⟷
simplifyr◎ (c₁ ◎ c₂) c₃ = c₁ ◎ (c₂ ◎ c₃)
simplifyr◎ (c₁ ⊕1 c₂) swap1₊ = swap1₊ ◎ (c₂ ⊕2 c₁)
simplifyr◎ (c₁ ⊕2 c₂) swap2₊ = swap2₊ ◎ (c₂ ⊕1 c₁)
simplifyr◎ (_⊗_ {ONE} {ONE} c₁ c₂) unite⋆ = unite⋆ ◎ c₂
simplifyr◎ (c₁ ⊗ c₂) swap⋆ = swap⋆ ◎ (c₂ ⊗ c₁)
simplifyr◎ (c₁ ⊗ c₂) (c₃ ⊗ c₄) = (c₁ ◎ c₃) ⊗ (c₂ ◎ c₄)
simplifyr◎ c₁ c₂ = c₁ ◎ c₂

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Issue939 where

record Sigma (A : Set)(P : A → Set) : Set where
  field
    fst : A
    .snd : P fst
open Sigma

postulate
  A : Set
  P : A → Set
  x : A
  .p : P x

ex : Sigma A P
ex = record
       { fst = x
       ; snd = p
       }

-- Note: we do not need --irrelevant-projections to use them on the lhs.
ex' : Sigma A P
fst ex' = x
snd ex' = p

-- WAS: Giving p yields the following error:
-- Identifier p is declared irrelevant, so it cannot be used here
-- when checking that the expression p has type P (fst ex')

-- Fixed.  Andreas, 2013-11-05

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Data.Nat
open import Data.Product
open import Data.Empty
open import Relation.Binary.PropositionalEquality

module Stream where

  record Stream (A : Set) : Set where
    coinductive
    field
      head : A
      tail : Stream A
  open Stream public

  get : ∀ {A : Set} → Stream A → ℕ → A
  get s zero = head s
  get s (suc i) = get s i

{-
  natsFrom : ℕ → Stream ℕ
  head (natsFrom x) = x
  tail (natsFrom x) = natsFrom (suc x)

  nats : Stream ℕ
  nats = natsFrom 0

  complicated-way-to-say-2 : head (tail (tail nats)) ≡ 2
  complicated-way-to-say-2 = refl

  -- thread a relation R through the elements of a stream
  record Trans {A : Set}(R : A → A → Set)(as : Stream A) : Set where
    coinductive
    field
      trans-head : R (head as) (head (tail as))
      trans-tail : Trans R (tail as)
  open Trans

  -- We can prove our generation of natural numbers to be correct!
  nats-correct : (n : ℕ) → Trans (λ x y → suc x ≡ y) (natsFrom n)
  trans-head (nats-correct n) = refl
  trans-tail (nats-correct n) = nats-correct (suc n)

  -----------------------------
  -- Talking Distr. Systems! --

  -- I hope I got the names right
  postulate
    State   : Set
    Event   : Set
    Enabled : State → Event → Set

    action  : (s : State)(e : Event)
            → (enev : Enabled s e)
            → State

    _l-t_ : (State → Set) → (State → Set) → Set

  -- indicates a given post-state is a possible
  -- outcome from a given pre-state; witnesses the
  -- translation to the relational scheme I mentioned
  _⟶_ : State → State → Set
  s ⟶ s' = ∃[ e ] (Σ (Enabled s e) (λ enev → action s e enev ≡ s'))

  -- A Behavior, then, is a stream of states
  -- such that it starts at s₀ and all states
  -- are linked through the _⟶_ relation.
  -- You might want to have this in a single Beh record
  -- instead of assembling it from primitives
  Beh : State → Set
  Beh s₀ = Σ (Stream State)
             (λ st → head st ≡ s₀ × Trans _⟶_ st)

  module Absurd-DO-NOT-TRY-AT-HOME where

    data HeadOrTail {A : Set}(P : A → Set)(Q : Stream A → Set)
       : Stream A → Set where
     on-head : ∀{s} → P (head s) → HeadOrTail P Q s

     -- there might be a case for including (¬ P (head s)) here...
     on-tail : ∀{s} → Q (tail s) → HeadOrTail P Q s

    record Any {A : Set}(P : A → Set)(as : Stream A) : Set where
      coinductive
      field
        any : HeadOrTail P (Any P) as
    open Any public

    -- Witness is a proof by induction that places us
    -- at the position where P 'holds'; but as we shall see,
    -- this might never be the case and; even though the
    -- 'recursive' call makes 'progress' by traversing to the tail,
    -- it is not enough and we broke math anyway
    --
    -- Exercise to the reader: mark this function as
    -- NON_TERMINATING instead to see how Agda would stop us
    -- from breaking math! NON_TERMINATING definitions never reduce
    -- during typechecking; rendering them almost useless. They are only used
    -- when doing actual user IO AFAIC
    {-# TERMINATING #-}
    witness : {A : Set}{P : A → Set}{as : Stream A}
            → Any P as → Stream A
    witness x with any x
    ...| on-head {s} _  = s
    ...| on-tail {s} x' = witness {as = tail s} x'

    {-# NON_TERMINATING #-}
    witness-satP : {A : Set}{P : A → Set}{as : Stream A}
                 → (x : Any P as) → P (head (witness x))
    witness-satP x with any x
    ...| on-head {s} p  = p
    ...| on-tail     x' = witness-satP x'

    never : {A : Set}(P : A → Set)(as : Stream A) → Any P as
    any (never P as) = on-tail (never P (tail as))

    -- This is why induction and coinduction can't be mixed! xD
    -- note that even marking one of them as non-terminating we still
    -- run into trouble
    oh-no! : ⊥
    oh-no! = witness-satP (never (λ _ → ⊥) nats)

  -----------------------------------------
  -- Trying Again; with naturals to help --

  mutual
    data AtF {A : Set}(P : A → Set)
       : Stream A → ℕ → Set where
     on-head : ∀{s} → P (head s) → AtF P s 0

     on-tail : ∀{s n} → At P (tail s) n → AtF P s (suc n)

    record At {A : Set}(P : A → Set)(as : Stream A)(i : ℕ) : Set where
      coinductive
      field
        α : AtF P as i

  open At

  _satisfies_at_ : ∀{s₀}(σ : Beh s₀)(P : State → Set) → ℕ → Set
  σ satisfies P at i = At P (proj₁ σ) i

  -- Now, we can prove that a for all finite prefixes
  -- of an infinite behaviour such that they satisfy P
  -- at some observable point, they will satisfy Q at
  -- some future obervable point.

  -- Note the use of the word observable here! I like to think of coinduction
  -- in terms of dominos-chain-reaction. Imagine we want to knock a domino
  -- x₀ and we want to reason whether or not it knocks over a domino x'.
  -- Now sawy we reason like this:
  -- that we x₀ will knock x₁; which in turn will knock x₂; ... and
  -- eventually will knock x'. Well; it is induction that guarantees
  -- this for us, and induction requires the number of dominoes between
  -- x and x' to be countable (isomorphic to ℕ).
  --
  -- If there truly is an infinite number of dominoes between x and x',
  -- it means that no matter how far we get, there will always be
  -- at least one domino between where we are and x'; and the wave of
  -- knocks will never reach x', hence, that type of reasoning is plain invalid.
  --
  -- Behaviors are pottentially plain infinite; some systems never stop.
  -- We still want to guarantee certain invariants.
  --

  -- Soundness, as I see it, is a proof that given any behavior σ
  -- that eventually satisfy P; and given that P leads to Q;
  -- any behaviour that forks of the point where σ satisfied P
  -- must satisfy Q; A first sketch in agda could be:
  soundness : {P Q : State → Set}
            → ∀{s₀ i}(σ : Beh s₀)(prf : σ satisfies P at i)
            → P l-t Q
            → Σ ℕ (λ j → σ satisfies Q at (j + i)) -- j + i already guarantess it is the future
  soundness = {! may-the-force-be-with-us !}
-}

max_stars_repo_name: lisandrasilva/agda-liveness

max_issues_repo_name: lisandrasilva/agda-liveness

max_forks_repo_name: lisandrasilva/agda-liveness


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

mutual

  data E : Set where
    e : F -> E

  record F : Set where
    inductive
    constructor c
    field f : E
open F

data ⊥ : Set where

elim : E → ⊥
elim (e (c x)) = elim x

elim' : E → ⊥
elim' (e y) = elim' (f y)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --no-main #-}

data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A

{-# COMPILE GHC List = data Non (Sense) #-} -- should result in warning when compiling
{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _∷_  #-}


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

open import LogicalFormulae
open import Setoids.Setoids
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Groups.Definition

module Groups.Subgroups.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where

open import Setoids.Subset S
open Group G

record Subgroup {c : _} (pred : A → Set c) : Set (a ⊔ b ⊔ c) where
  field
    isSubset : subset pred
    closedUnderPlus : {g h : A} → (pred g) → (pred h) → pred (g + h)
    containsIdentity : pred 0G
    closedUnderInverse : ({g : A} → (pred g) → (pred (inverse g)))

subgroupOp : {c : _} {pred : A → Set c} → (s : Subgroup pred) → Sg A pred → Sg A pred → Sg A pred
subgroupOp {pred = pred} record { closedUnderPlus = one } (a , prA) (b , prB) = (a + b) , one prA prB

subgroupIsGroup : {c : _} {pred : A → Set c} → (s : Subgroup pred) → Group (subsetSetoid (Subgroup.isSubset s)) (subgroupOp s)
Group.+WellDefined (subgroupIsGroup s) {m , prM} {n , prN} {x , prX} {y , prY} m=x n=y = +WellDefined m=x n=y
Group.0G (subgroupIsGroup record { containsIdentity = two }) = 0G , two
Group.inverse (subgroupIsGroup record { closedUnderInverse = three }) (a , prA) = (inverse a) , three prA
Group.+Associative (subgroupIsGroup s) {a , prA} {b , prB} {c , prC} = +Associative
Group.identRight (subgroupIsGroup s) {a , prA} = identRight
Group.identLeft (subgroupIsGroup s) {a , prA} = identLeft
Group.invLeft (subgroupIsGroup s) {a , prA} = invLeft
Group.invRight (subgroupIsGroup s) {a , prA} = invRight


text:
------------------------------------------------------------------------------
-- Generic well-founded induction on trees
------------------------------------------------------------------------------

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

-- Adapted from FOTC.Data.Nat.Induction.Acc.WellFounded.

module FOT.FOTC.Program.Mirror.Induction.Acc.WellFounded where

open import FOTC.Base

open import FOTC.Program.Mirror.Type

------------------------------------------------------------------------------
-- The accessibility predicate: x is accessible if everything which is
-- smaller than x is also accessible (inductively).
data Acc (_<_ : D → D → Set)(t : D) : Set where
 acc : (∀ {t'} → Tree t' → t' < t → Acc _<_ t') → Acc _<_ t

accFold : {P : D → Set}(_<_ : D → D → Set) →
          (∀ {t} → Tree t → (∀ {t'} → Tree t' → t' < t → P t') → P t) →
          ∀ {t} → Tree t → Acc _<_ t → P t
accFold _<_ f Tt (acc h) = f Tt (λ Tt' t'<t → accFold _<_ f Tt' (h Tt' t'<t))

-- The accessibility predicate encodes what it means to be
-- well-founded; if all elements are accessible, then _<_ is
-- well-founded.
WellFounded : (D → D → Set) → Set
WellFounded _<_ = ∀ {t} → Tree t → Acc _<_ t

WellFoundedInduction :
  {P : D → Set}{_<_ : D → D → Set} →
  WellFounded _<_ →
  (∀ {t} → Tree t → (∀ {t'} → Tree t' → t' < t → P t') → P t) →
  ∀ {t} → Tree t → P t
WellFoundedInduction {_<_ = _<_} wf f Tt = accFold _<_ f Tt (wf Tt)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- Example: Right recursive expression grammar
------------------------------------------------------------------------

module TotalRecognisers.Simple.Expression where

open import Codata.Musical.Notation
open import Data.Bool
open import Data.Char as Char using (Char)
open import Data.String as String using (String)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable

import TotalRecognisers.Simple as P

private
  open module PC = P Char Char._≟_ hiding (_·_)
  open PC.P using (_·_)

------------------------------------------------------------------------
-- Recognisers for bits and binary numbers

-- Bits.

bit = tok '0' ∣ tok '1'

-- Numbers.

number = bit · ♯ (empty ∣ number)

------------------------------------------------------------------------
-- An expression grammar

-- t ∷= f '+' t ∣ f
-- f ∷= a '*' f ∣ a
-- a ∷= '(' t ')' ∣ n

mutual

  term   = factor · ♯ (tok '+' · ♯ term)
         ∣ factor

  factor = atom · ♯ (tok '*' · ♯ factor)
         ∣ atom

  atom   = tok '(' · ♯ term · ♯ tok ')'
         ∣ number

------------------------------------------------------------------------
-- Unit tests

module Tests where

  test : ∀ {n} → P n → String → Bool
  test p s = ⌊ String.toList s ∈? p ⌋

  ex₁ : test term "0*(0+0)" ≡ true
  ex₁ = refl

  ex₂ : test term "0*(0+0" ≡ false
  ex₂ = refl

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed universes
------------------------------------------------------------------------

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

module Data.Universe.Indexed where

open import Data.Product
open import Data.Universe
open import Function
open import Level

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

record IndexedUniverse i u e : Set (suc (i ⊔ u ⊔ e)) where
  field
    I  : Set i                 -- Index set.
    U  : I → Set u             -- Codes.
    El : ∀ {i} → U i → Set e   -- Decoding function.

  -- An indexed universe can be turned into an unindexed one.

  unindexed-universe : Universe (i ⊔ u) e
  unindexed-universe = record
    { U  = ∃ λ i → U i
    ; El = El ∘ proj₂
    }


text:
module Integer.Signed where

open import Data.Empty as ⊥
open import Data.Product as Σ
open import Data.Product.Relation.Pointwise.NonDependent
open import Data.Sum as ⊎
open import Data.Unit as ⊤
open import Equality
open import Function
open import Natural as ℕ
open import Quotient as /
open import Relation.Binary
open import Syntax

open Equality.FunctionProperties

⟦ℤ⟧ = ℕ ⊎ ℕ
⟦ℤ²⟧ = ⟦ℤ⟧ × ⟦ℤ⟧

infix 10 +1*_ -1*_
pattern +1*_ x = inj₁ x
pattern -1*_ x = inj₂ x

infix 1 _≈_
_≈_ : ⟦ℤ⟧ → ⟦ℤ⟧ → Set
+1* x ≈ +1* y = x ≡ y
+1* x ≈ -1* y = x ≡ 0 × y ≡ 0
-1* x ≈ +1* y = x ≡ 0 × y ≡ 0
-1* x ≈ -1* y = x ≡ y

≈-refl : ∀ {x} → x ≈ x
≈-refl {+1* x} = refl
≈-refl { -1* x} = refl

≈-sym : ∀ {x y} → x ≈ y → y ≈ x
≈-sym {+1* x} {+1* y} = sym
≈-sym {+1* x} { -1* y} = Σ.swap
≈-sym { -1* x} {+1* y} = Σ.swap
≈-sym { -1* x} { -1* y} = sym

≈-trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
≈-trans {+1* x} {+1* y} {+1* z} p q = compPath p q
≈-trans {+1* x} {+1* y} { -1* z} p (q , r) = p ≫ q , r
≈-trans {+1* x} { -1* y} {+1* z} (p , q) (r , s) = p ≫ sym s
≈-trans {+1* x} { -1* y} { -1* z} (p , q) r = p , sym r ≫ q
≈-trans { -1* x} {+1* y} {+1* z} (p , q) r = p , sym r ≫ q
≈-trans { -1* x} {+1* y} { -1* z} (p , q) (r , s) = p ≫ sym s
≈-trans { -1* x} { -1* y} {+1* z} p (q , r) = p ≫ q , r
≈-trans { -1* x} { -1* y} { -1* z} p q = compPath p q

ℤ = ⟦ℤ⟧ / _≈_
ℤ² = ⟦ℤ²⟧ / Pointwise _≈_ _≈_

instance
  ⟦ℤ⟧-Number : Number ⟦ℤ⟧
  ⟦ℤ⟧-Number = record { Constraint = λ _ → ⊤ ; fromNat = λ n → +1* n }

  ℤ-Number : Number ℤ
  ℤ-Number = record { Constraint = λ _ → ⊤ ; fromNat = λ n → ⟦ fromNat n ⟧ }

  ⟦ℤ⟧-Negative : Negative ⟦ℤ⟧
  ⟦ℤ⟧-Negative = record { Constraint = λ _ → ⊤ ; fromNeg = λ n → -1* n }

  ℤ-Negative : Negative ℤ
  ℤ-Negative = record { Constraint = λ _ → ⊤ ; fromNeg = λ n → ⟦ fromNeg n ⟧ }

⟦negate⟧ : ⟦ℤ⟧ → ⟦ℤ⟧
⟦negate⟧ (+1* n) = -1* n
⟦negate⟧ (-1* n) = +1* n

negate : ℤ → ℤ
negate =
  ⟦negate⟧ // λ where
    (+1* x) (+1* y) → id
    (+1* x) (-1* y) → id
    (-1* x) (+1* y) → id
    (-1* x) (-1* y) → id

ℕ-minus : ℕ → ℕ → ⟦ℤ⟧
ℕ-minus zero n = -1* n
ℕ-minus m zero = +1* m
ℕ-minus (suc m) (suc n) = ℕ-minus m n

instance
  ℕ-minus-syntax : minus-syntax-simple ℕ ℕ ⟦ℤ⟧
  ℕ-minus-syntax = λ where ._-_ → ℕ-minus

ℕ-minus-identityˡ : ∀ a → ℕ-minus 0 a ≈ -1* a
ℕ-minus-identityˡ a = refl

ℕ-minus-identityʳ : ∀ a → ℕ-minus a 0 ≈ +1* a
ℕ-minus-identityʳ zero = refl , refl
ℕ-minus-identityʳ (suc a) = refl

⟦plus⟧ : ⟦ℤ²⟧ → ⟦ℤ⟧
⟦plus⟧ (+1* a , +1* b) = +1* (a + b)
⟦plus⟧ (+1* a , -1* b) = a - b
⟦plus⟧ (-1* a , +1* b) = b - a
⟦plus⟧ (-1* a , -1* b) = -1* (a + b)

plus : ℤ² → ℤ
plus =
  ⟦plus⟧ // λ where
    (+1* a , +1* b) (+1* c , +1* d) (p , q) → cong₂ _+_ p q
    (+1* a , +1* b) (+1* c , -1* d) (p , (q , r)) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ ,′ ⟪ r ⟫ of λ where
        (♥ , ♥ , ♥) →
          ≈-trans
            (⟨ ℕ.+-identityʳ a ⟩)
            (≈-sym (ℕ-minus-identityʳ a))
    (+1* a , +1* b) (-1* c , +1* d) ((p , q) , r) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ ,′ ⟪ r ⟫ of λ where
        (♥ , ♥ , ♥) →
          ≈-sym (ℕ-minus-identityʳ b)
    (+1* a , +1* b) (-1* c , -1* d) ((p , q) , (r , s)) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ ,′ ⟪ r ⟫ ,′ ⟪ s ⟫ of λ where
        (♥ , ♥ , ♥ , ♥) →
          refl , refl
    (+1* a , -1* b) (+1* c , +1* d) (p , (q , r)) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ ,′ ⟪ r ⟫ of λ where
        (♥ , ♥ , ♥) →
          ≈-trans {ℕ-minus a 0} {+1* a} {+1* (a + 0)}
            (ℕ-minus-identityʳ a)
            (sym ⟨ ℕ.+-identityʳ a ⟩)
    (+1* a , -1* b) (+1* c , -1* d) (p , q) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ of λ where
        (♥ , ♥) →
          ≈-refl
    (+1* a , -1* b) (-1* c , +1* d) ((p , q) , (r , s)) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ ,′ ⟪ r ⟫ ,′ ⟪ s ⟫ of λ where
        (♥ , ♥ , ♥ , ♥) →
          refl
    (+1* a , -1* b) (-1* c , -1* d) ((p , q) , r) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ ,′ ⟪ r ⟫ of λ where
        (♥ , ♥ , ♥) →
          refl
    (-1* a , +1* b) (+1* c , +1* d) ((p , q) , r) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ ,′ ⟪ r ⟫ of λ where
        (♥ , ♥ , ♥) →
          ℕ-minus-identityʳ b
    (-1* a , +1* b) (+1* c , -1* d) ((p , q) , (r , s)) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ ,′ ⟪ r ⟫ ,′ ⟪ s ⟫ of λ where
        (♥ , ♥ , ♥ , ♥) →
          refl
    (-1* a , +1* b) (-1* c , +1* d) (p , q) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ of λ where
        (♥ , ♥) →
          ≈-refl
    (-1* a , +1* b) (-1* c , -1* d) (p , (q , r)) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ ,′ ⟪ r ⟫ of λ where
        (♥ , ♥ , ♥) →
          sym ⟨ ℕ.+-identityʳ a ⟩
    (-1* a , -1* b) (+1* c , +1* d) ((p , q) , (r , s)) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ ,′ ⟪ r ⟫ ,′ ⟪ s ⟫ of λ where
        (♥ , ♥ , ♥ , ♥) →
          refl , refl
    (-1* a , -1* b) (+1* c , -1* d) ((p , q) , r) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ ,′ ⟪ r ⟫ of λ where
        (♥ , ♥ , ♥) →
          refl
    (-1* a , -1* b) (-1* c , +1* d) (p , (q , r)) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ ,′ ⟪ r ⟫ of λ where
        (♥ , ♥ , ♥) →
          ⟨ ℕ.+-identityʳ a ⟩
    (-1* a , -1* b) (-1* c , -1* d) (p , q) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ of λ where
        (♥ , ♥) →
          refl

⟦times⟧ : ⟦ℤ²⟧ → ⟦ℤ⟧
⟦times⟧ (+1* a , +1* b) = +1* (a * b)
⟦times⟧ (+1* a , -1* b) = -1* (a * b)
⟦times⟧ (-1* a , +1* b) = -1* (a * b)
⟦times⟧ (-1* a , -1* b) = +1* (a * b)

times : ℤ² → ℤ
times =
  ⟦times⟧ // λ where
    (+1* a , +1* b) (+1* c , +1* d) (p , q) → cong₂ _*_ p q
    (+1* a , -1* b) (+1* c , -1* d) (p , q) → cong₂ _*_ p q
    (-1* a , +1* b) (-1* c , +1* d) (p , q) → cong₂ _*_ p q
    (-1* a , -1* b) (-1* c , -1* d) (p , q) → cong₂ _*_ p q
    (+1* a , +1* b) (+1* c , -1* d) (p , q , r) →
      case ⟪ q ⟫ ,′ ⟪ r ⟫ of λ where
        (♥ , ♥) → ⟨ *-zeroʳ a ⟩ , ⟨ *-zeroʳ c ⟩
    (+1* a , -1* b) (+1* c , +1* d) (p , (q , r)) →
      case ⟪ q ⟫ ,′ ⟪ r ⟫ of λ where
        (♥ , ♥) → ⟨ *-zeroʳ a ⟩ , ⟨ *-zeroʳ c ⟩
    (-1* a , +1* b) (-1* c , -1* d) (p , (q , r)) →
      case ⟪ q ⟫ ,′ ⟪ r ⟫ of λ where
        (♥ , ♥) → ⟨ *-zeroʳ a ⟩ , ⟨ *-zeroʳ c ⟩
    (-1* a , -1* b) (-1* c , +1* d) (p , (q , r)) →
      case ⟪ q ⟫ ,′ ⟪ r ⟫ of λ where
        (♥ , ♥) → ⟨ *-zeroʳ a ⟩ , ⟨ *-zeroʳ c ⟩
    (+1* a , +1* b) (-1* c , +1* d) ((p , q) , r) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ of λ where
        (♥ , ♥) → refl , refl
    (+1* a , -1* b) (-1* c , -1* d) ((p , q) , r) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ of λ where
        (♥ , ♥) → refl , refl
    (-1* a , +1* b) (+1* c , +1* d) ((p , q) , r) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ of λ where
        (♥ , ♥) → refl , refl
    (-1* a , -1* b) (+1* c , -1* d) ((p , q) , r) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ of λ where
        (♥ , ♥) → refl , refl
    (+1* a , +1* b) (-1* c , -1* d) ((p , q) , r) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ of λ where
        (♥ , ♥) → refl
    (+1* a , -1* b) (-1* c , +1* d) ((p , q) , r) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ of λ where
        (♥ , ♥) → refl
    (-1* a , +1* b) (+1* c , -1* d) ((p , q) , r) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ of λ where
        (♥ , ♥) → refl
    (-1* a , -1* b) (+1* c , +1* d) ((p , q) , r) →
      case ⟪ p ⟫ ,′ ⟪ q ⟫ of λ where
        (♥ , ♥) → refl

instance
  ℤ-plus-syntax : plus-syntax-simple ℤ ℤ ℤ
  ℤ-plus-syntax = λ where ._+_ → /.uncurry ≈-refl ≈-refl plus

  ℤ-minus-syntax : minus-syntax-simple ℤ ℤ ℤ
  ℤ-minus-syntax = λ where ._-_ x y → x + negate y

  ℤ-times-syntax : times-syntax-simple ℤ ℤ ℤ
  ℤ-times-syntax = λ where ._*_ → /.uncurry ≈-refl ≈-refl times


text:
-- 2014-02-08 Andreas
-- Eta-equality for records that are recursive via some data type

module _ where

open import Common.Equality

module Nested where

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

  record Tree (A : Set) : Set where
    constructor tree
    field
      elem     : A
      subtrees : List (Tree A)
  open Tree

  test : ∀ {A} (t : Tree A) → t ≡ tree (elem t) (subtrees t)
  test t = refl

  -- we should have eta for Tree!

module Mutual where

  mutual
    data TreeList (A : Set) : Set where
      []  : TreeList A
      _∷_ : (x : Tree A)(xs : TreeList A) → TreeList A

    record Tree (A : Set) : Set where
      constructor tree
      field
        elem     : A
        subtrees : TreeList A
  open Tree

  test : ∀ {A} (t : Tree A) → t ≡ tree (elem t) (subtrees t)
  test t = refl

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
module JVM.Defaults.Syntax.Instructions.Show where

open import Data.String as String hiding (show)
open import Data.Nat.Show as Nat hiding (show)
open import Relation.Binary.PropositionalEquality
open import Relation.Ternary.Structures.Syntax
open import Relation.Ternary.Monad.Weakening
open import Relation.Ternary.Data.ReflexiveTransitive

open import JVM.Types
open import JVM.Contexts
open import JVM.Defaults.Syntax.Values
open import JVM.Defaults.Syntax.Instructions
open import JVM.Model using (↑; ↓)

show-instr : ∀ {Φ} → ⟨ Γ ∣ ψ₁ ⇒ ψ₂ ⟩ Φ → String
show-instr noop      = "noop"
show-instr pop       = "pop"
show-instr (push x)  = "push"
  where
    show-const : Const a → String
    show-const null    = "null"
    show-const unit    = "unit"
    show-const (num x) = Nat.show x
show-instr dup       = "dup"
show-instr swap      = "swap"
show-instr (bop x)   = "bop"
show-instr new       = "new"
show-instr read      = "read"
show-instr write     = "write"
show-instr (load (refl ⇈ wk))  = "load "  ++ Nat.show (indexOf wk)
show-instr (store (refl ⇈ wk)) = "store " ++ Nat.show (indexOf wk)
show-instr (goto x)  = "goto"
show-instr (if c x₁) = "if" ++ show-comp c
  where
    show-comp : Comparator → String
    show-comp eq = "eq"
    show-comp ne = "ne"
    show-comp lt = "lt"
    show-comp ge = "ge"
    show-comp gt = "gt"
    show-comp le = "le"
show-instr ret       = "ret"

show-code : ∀ {Γ Φ} → Code Γ ψ₁ ψ₂ Φ → String
show-code (labeled (_ ∙⟨ _ ⟩ ↓ i))   = "<>: " ++ show-instr i
show-code (instr (↓ i))              = "    " ++ show-instr i

show : ∀ {Φ} → ⟪ Γ ∣ ψ₁ ⇒ ψ₂ ⟫ Φ → String
show nil      = ""
show (c ▹⟨ σ ⟩ is) = show-code c ++ "\n" ++ show is


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

module Haskell.Modules.ToBool where

open import Data.Bool hiding (not)
import      Function
import      Relation.Nullary                as RN
import      Relation.Nullary.Decidable.Core as RNDC

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

not : ∀ {b} {B : Set b} ⦃ _ : ToBool B ⦄ → B → Bool
not b = Data.Bool.not (toBool b)

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

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


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Logical relation for erasure with the Nehemiah plugin.
------------------------------------------------------------------------

module Nehemiah.Change.Implementation where

open import Nehemiah.Syntax.Type
open import Nehemiah.Syntax.Term
open import Nehemiah.Denotation.Value
open import Nehemiah.Denotation.Evaluation
open import Nehemiah.Change.Validity
open import Nehemiah.Change.Type
open import Nehemiah.Change.Value
open import Nehemiah.Change.Derive

open import Relation.Binary.PropositionalEquality
open import Data.Unit
open import Data.Product
open import Data.Integer
open import Structure.Bag.Nehemiah

import Parametric.Change.Implementation
    Const ⟦_⟧Base ⟦_⟧Const ΔBase
    ⟦apply-base⟧ ⟦diff-base⟧ ⟦nil-base⟧ derive-const as Implementation

private
  implements-base : ∀ ι {v : ⟦ ι ⟧Base} → Δ₍ ι ₎ v → ⟦ ΔBase ι ⟧Type → Set
  implements-base base-int {v} Δv Δv′ = Δv ≡ Δv′
  implements-base base-bag {v} Δv Δv′ = Δv ≡ Δv′

  u⊟v≈u⊝v-base : ∀ ι → {u v : ⟦ ι ⟧Base} →
      implements-base ι {v} (u ⊟₍ ι ₎ v) (⟦diff-base⟧ ι u v)
  u⊟v≈u⊝v-base base-int = refl
  u⊟v≈u⊝v-base base-bag = refl

  nil-v≈⟦nil⟧-v-base : ∀ ι {v : ⟦ ι ⟧Base} →
    implements-base ι (nil₍ ι ₎ v) (⟦nil-base⟧ ι v)
  nil-v≈⟦nil⟧-v-base base-int = refl
  nil-v≈⟦nil⟧-v-base base-bag = refl

  carry-over-base : ∀ {ι}
    {v : ⟦ ι ⟧Base}
    (Δv : Δ₍ ι ₎ v)
    {Δv′ : ⟦ ΔBase ι ⟧Type} (Δv≈Δv′ : implements-base ι {v} Δv Δv′) →
      v ⊞₍ base ι ₎ Δv ≡ v ⟦⊕₍ base ι ₎⟧ Δv′
  carry-over-base {base-int} {v} Δv Δv≈Δv′ = cong (_+_ v) Δv≈Δv′
  carry-over-base {base-bag} Δv Δv≈Δv′ = cong (_++_ (before₍ bag ₎ Δv)) Δv≈Δv′

implementation-structure : Implementation.Structure
implementation-structure = record
    { implements-base = implements-base
    ; u⊟v≈u⊝v-base = u⊟v≈u⊝v-base
    ; nil-v≈⟦nil⟧-v-base = nil-v≈⟦nil⟧-v-base
    ; carry-over-base = carry-over-base
    }

open Implementation.Structure implementation-structure public

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The max operator derived from an arbitrary total order
------------------------------------------------------------------------

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

open import Relation.Binary

module Algebra.Construct.NaturalChoice.Max
  {a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂) where

open import Algebra.FunctionProperties
open import Relation.Binary.Construct.Converse using ()
  renaming (totalOrder to flip)

open TotalOrder totalOrder renaming (Carrier to A)

------------------------------------------------------------------------
-- Max is just min with a flipped order

import Algebra.Construct.NaturalChoice.Min (flip totalOrder) as Min

infixl 6 _⊔_

_⊔_ : Op₂ A
_⊔_ = Min._⊓_

open Min public using ()
  renaming
  ( ⊓-cong          to ⊔-cong
  ; ⊓-idem          to ⊔-idem
  ; ⊓-sel           to ⊔-sel
  ; ⊓-assoc         to ⊔-assoc
  ; ⊓-comm          to ⊔-comm
  ; ⊓-identityˡ     to ⊔-identityˡ
  ; ⊓-identityʳ     to ⊔-identityʳ
  ; ⊓-identity      to ⊔-identity
  ; ⊓-zeroˡ         to ⊔-zeroˡ
  ; ⊓-zeroʳ         to ⊔-zeroʳ
  ; ⊓-zero          to ⊔-zero
  ; ⊓-isMagma       to ⊔-isMagma
  ; ⊓-isSemigroup   to ⊔-isSemigroup
  ; ⊓-isBand        to ⊔-isBand
  ; ⊓-isSemilattice to ⊔-isSemilattice
  ; ⊓-isMonoid      to ⊔-isMonoid
  ; ⊓-magma         to ⊔-magma
  ; ⊓-semigroup     to ⊔-semigroup
  ; ⊓-band          to ⊔-band
  ; ⊓-semilattice   to ⊔-semilattice
  ; ⊓-monoid        to ⊔-monoid
  ; x⊓y≈y⇒y≤x       to x⊔y≈y⇒x≤y
  ; x⊓y≈x⇒x≤y       to x⊔y≈x⇒y≤x
  )


text:
module string where

open import bool
open import eq
open import char
open import list
open import nat
open import unit
open import maybe
open import product

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

postulate
  Pair : (A B : Set) → Set
  pair : {A B : Set} → A → B → Pair A B
  pair-fst : {A B : Set} → Pair A B → A
  pair-snd : {A B : Set} → Pair A B → B

{-# COMPILE GHC Pair = type (,)           #-}
{-# COMPILE GHC pair = \ _ _ a b -> (a, b) #-}
{-# COMPILE GHC pair-fst = \ _ _ p -> fst p #-}
{-# COMPILE GHC pair-snd = \ _ _ p -> snd p #-}

postulate
  string : Set
  stringUncons   : string → maybe (Pair char string)
  stringFoldl : ∀{A : Set} → (A → char → A) → A → string → A
  stringFoldr : ∀{A : Set} → (char → A → A) → A → string → A

{-# BUILTIN STRING string #-}
{-# COMPILE GHC stringUncons = Data.Text.uncons #-}
{-# COMPILE GHC stringFoldl = \ x -> Data.Text.foldl #-}
{-# COMPILE GHC stringFoldr = \ x -> Data.Text.foldr #-}

private
 primitive
  primStringToList   : string → 𝕃 char
  primStringAppend   : string → string → string
  primStringFromList : 𝕃 char → string
  primStringEquality : string → string → 𝔹

-- see string-thms.agda for some axioms about the above primitive functions

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infixr 6 _^_
infix 8 _=string_

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------

_^_ : string → string → string
_^_ = primStringAppend

string-uncons : string → maybe (char × string)
string-uncons x with stringUncons x
string-uncons x | nothing = nothing
string-uncons x | just x₁ = just (pair-fst x₁ , pair-snd x₁)

string-to-𝕃char : string → 𝕃 char
string-to-𝕃char = primStringToList

𝕃char-to-string : 𝕃 char → string
𝕃char-to-string = primStringFromList

_=string_ : string → string → 𝔹
_=string_ = primStringEquality

char-to-string : char → string
char-to-string c = 𝕃char-to-string [ c ]

string-append-t : ℕ → Set
string-append-t 0 = string → string
string-append-t (suc n) = string → (string-append-t n)

string-append-h : (n : ℕ) → string → string-append-t n
string-append-h 0 ret = λ x → ret ^ x
string-append-h (suc n) ret = λ x → (string-append-h n (ret ^ x))

string-append : (n : ℕ) → string-append-t n
string-append n = string-append-h n ""

string-concat : 𝕃 string → string
string-concat [] = ""
string-concat (s :: ss) = s ^ (string-concat ss)

string-concat-sep : (separator : string) → 𝕃 string → string
string-concat-sep sep [] = ""
string-concat-sep sep (s1 :: ss) with ss
... | [] = s1
... | s2 :: ss' = s1 ^ sep ^ (string-concat-sep sep ss)

string-concat-sep-map : ∀{A : Set} → (separator : string) → (A → string) → 𝕃 A → string
string-concat-sep-map sep f l = string-concat-sep sep (map f l)

escape-string-h : 𝕃 char → 𝕃 char
escape-string-h ('\n' :: cs) = '\\' :: 'n' :: (escape-string-h cs)
escape-string-h ('"' :: cs) = '\\' :: '"' :: (escape-string-h cs)
escape-string-h (c :: cs) = c :: escape-string-h cs
escape-string-h [] = []

escape-string : string → string
escape-string s = 𝕃char-to-string( escape-string-h( string-to-𝕃char s ) )

string-length : string → ℕ
string-length s = length (string-to-𝕃char s)

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


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

module Categories.Functor.Monoidal where

open import Level
open import Data.Product using (Σ; _,_)

open import Categories.Category
open import Categories.Category.Product
open import Categories.Category.Monoidal

open import Categories.Functor hiding (id)
open import Categories.NaturalTransformation hiding (id)

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

module _  (MC : Monoidal C) (MD : Monoidal D) where
  private
    module C  = Category C
    module D  = Category D
    module MC = Monoidal MC
    module MD = Monoidal MD

  record MonoidalFunctor : Set (levelOfTerm MC ⊔ levelOfTerm MD) where
    field
      F : Functor C D

    open Functor F public

    field
      ε      : D [ MD.unit , F₀ MC.unit ]
      ⊗-homo : NaturalTransformation (MD.⊗ ∘F (F ⁂ F)) (F ∘F MC.⊗)

    module ⊗-homo = NaturalTransformation ⊗-homo

    -- coherence condition
    open D
    open MD
    open Commutation

    field
      associativity : ∀ {X Y Z} →
                      [ (F₀ X ⊗₀ F₀ Y) ⊗₀ F₀ Z ⇒ F₀ (X MC.⊗₀ Y MC.⊗₀ Z) ]⟨
                        ⊗-homo.η (X , Y) ⊗₁ id                          ⇒⟨ F₀ (X MC.⊗₀ Y) ⊗₀ F₀ Z ⟩
                        ⊗-homo.η (X MC.⊗₀ Y , Z)                        ⇒⟨ F₀ ((X MC.⊗₀ Y) MC.⊗₀ Z) ⟩
                        F₁ MC.associator.from
                      ≈ associator.from                                 ⇒⟨ F₀ X ⊗₀ F₀ Y ⊗₀ F₀ Z ⟩
                        id ⊗₁ ⊗-homo.η (Y , Z)                          ⇒⟨ F₀ X ⊗₀ F₀ (Y MC.⊗₀ Z) ⟩
                        ⊗-homo.η (X , Y MC.⊗₀ Z)
                      ⟩
      unitaryˡ      : ∀ {X} →
                      [ unit ⊗₀ F₀ X ⇒ F₀ X    ]⟨
                        ε ⊗₁ id                ⇒⟨ F₀ MC.unit ⊗₀ F₀ X ⟩
                        ⊗-homo.η (MC.unit , X) ⇒⟨ F₀ (MC.unit MC.⊗₀ X) ⟩
                        F₁ MC.unitorˡ.from
                      ≈ unitorˡ.from
                      ⟩
      unitaryʳ      : ∀ {X} →
                      [ F₀ X ⊗₀ unit ⇒ F₀ X    ]⟨
                        id ⊗₁ ε                ⇒⟨ F₀ X ⊗₀ F₀ MC.unit ⟩
                        ⊗-homo.η (X , MC.unit) ⇒⟨ F₀ (X MC.⊗₀ MC.unit) ⟩
                        F₁ MC.unitorʳ.from
                      ≈ unitorʳ.from
                      ⟩

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- Andreas, 2017-01-08
-- Error range when "The name of the top level module does not match" to big

{-# OPTIONS --allow-unsolved-metas #-}

{-# OPTIONS --type-in-type #-}

-- {-# OPTIONS -v scope.checkModuleName:100 #-}

module ThisIsTheWrongName where

postulate Something : Set

-- WAS: Error range included option pragmas.

-- Expected range: only the module name


text:
{-# OPTIONS -v tc.cover.splittree:50 #-}

open import Agda.Builtin.Nat

data Vec (A : Set) : Nat → Set where
  nil  : Vec A zero
  cons : (n : Nat) → A → Vec A n → Vec A (suc n)

append : {A : Set} (m n : Nat) → Vec A m → Vec A n → Vec A (m + n)
append .zero    n nil            ys = ys
append (.suc m) n (cons .m x xs) ys = cons (m + n) x (append m n xs ys)

open import Agda.Builtin.Equality

data _×_ (A B : Set) : Set where
  pair : A → B → A × B

test : (p q : Nat × Nat) → p ≡ q → Set₁
test (.(pair x) y) (pair x .y) refl = Set


text:
open import Agda.Primitive using (_⊔_)

import Categories.Category as Category
import Categories.Category.Cartesian as Cartesian

open import MultiSorted.AlgebraicTheory

-- Finite products indexed by contexts
module MultiSorted.Product
       {o ℓ e}
       (𝒞 : Category.Category o ℓ e)
       {𝓈 ℴ}
       {Σ : Signature {𝓈} {ℴ}}
       (interp-sort : Signature.sort Σ → Category.Category.Obj 𝒞) where

  open Signature Σ
  open Category.Category 𝒞
  open HomReasoning

  interp-sort-var : {Γ : Context} → var Γ → Obj
  interp-sort-var {Γ} x = interp-sort (sort-of Γ x)

  record Producted : Set (o ⊔ ℓ ⊔ e ⊔ 𝓈) where

    field
      prod : Context → Obj
      π : ∀ {Γ} (x : var Γ) → prod Γ ⇒ interp-sort-var x
      tuple : ∀ Γ {B} → ((x : var Γ) → B ⇒ interp-sort-var x) → B ⇒ prod Γ
      project : ∀ {Γ} {B} {x : var Γ} {fs : (y : var Γ) → B ⇒ interp-sort-var y} → π x ∘ tuple Γ fs ≈ fs x
      unique : ∀ {Γ} {B} {fs : (x : var Γ) → B ⇒ interp-sort-var x} {g : B ⇒ prod Γ} → (∀ i → π i ∘ g ≈ fs i) → tuple Γ fs ≈ g

    η : ∀ {Γ} → tuple Γ π ≈ id
    η = unique (λ i → identityʳ)

    ! : ∀ {B : Obj} → B ⇒ prod ctx-empty
    ! {B} = tuple ctx-empty ctx-empty-absurd

    !-unique : ∀ {B : Obj} {f : B ⇒ prod ctx-empty} → ! ≈ f
    !-unique {f = f} = unique ctx-empty-absurd

    !-unique₂ : ∀ {B : Obj} {f g : B ⇒ prod ctx-empty} → f ≈ g
    !-unique₂ = (⟺ !-unique) ○ !-unique

    tuple-cong : ∀ {B : Obj} {Γ} {fs gs : (x : var Γ) → B ⇒ interp-sort-var x} → (∀ i → fs i ≈ gs i) →
                 tuple Γ fs ≈ tuple Γ gs
    tuple-cong ξ = unique (λ i →  project ○ ⟺ (ξ i))

    ∘-distribʳ-tuple : ∀ {B C} {Γ} {fs : (x : var Γ) → B ⇒ interp-sort-var x} {g : C ⇒ B}  →
                       tuple Γ (λ x → fs x ∘ g) ≈ tuple Γ fs ∘ g
    ∘-distribʳ-tuple = unique (λ i → ⟺ assoc ○ ∘-resp-≈ˡ project)

  -- A cartesian category has a standard products structure (which we need not use)
  module _ (cartesian-𝒞 : Cartesian.Cartesian 𝒞) where
    open Cartesian.Cartesian cartesian-𝒞

    standard-prod : Context → Obj
    standard-prod ctx-empty = ⊤
    standard-prod (ctx-slot A) = interp-sort A
    standard-prod (ctx-concat Γ Δ) = standard-prod Γ × standard-prod Δ

    standard-π : ∀ {Γ} (x : var Γ) → standard-prod Γ ⇒ interp-sort-var x
    standard-π var-var = id
    standard-π (var-inl i) = standard-π i ∘ π₁
    standard-π (var-inr i) = standard-π i ∘ π₂

    standard-tuple : ∀ Γ {B} → ((x : var Γ) → B ⇒ interp-sort-var x) → B ⇒ standard-prod Γ
    standard-tuple ctx-empty fs = !
    standard-tuple (ctx-slot _) fs = fs var-var
    standard-tuple (ctx-concat Γ Δ) fs = ⟨ standard-tuple Γ (λ i → fs (var-inl i)) , standard-tuple Δ (λ j → fs (var-inr j)) ⟩

    standard-project : ∀ {Γ} {B} {x : var Γ} {fs : (x : var Γ) → B ⇒ interp-sort-var x} →
                       standard-π x ∘ standard-tuple Γ fs ≈ fs x
    standard-project {x = var-var} = identityˡ
    standard-project {x = var-inl x} = assoc ○ ((∘-resp-≈ʳ project₁) ○ standard-project {x = x})
    standard-project {x = var-inr x} = assoc ○ ((∘-resp-≈ʳ project₂) ○ standard-project {x = x})

    standard-unique : ∀ {Γ} {B} {fs : (x : var Γ) → B ⇒ interp-sort-var x} {g : B ⇒ standard-prod Γ} → (∀ i → standard-π i ∘ g ≈ fs i) →
                      standard-tuple Γ fs ≈ g
    standard-unique {ctx-empty} ξ = !-unique _
    standard-unique {ctx-slot _} ξ = ⟺ (ξ var-var) ○ identityˡ
    standard-unique {ctx-concat Γ Δ} {fs = fs} ξ =
      unique
         (⟺ (standard-unique (λ x → sym-assoc ○ (ξ (var-inl x)))))
         (⟺ (standard-unique (λ y → sym-assoc ○ (ξ (var-inr y)))))

    StandardProducted : Producted
    StandardProducted =
      record
      { prod = standard-prod
      ; π = standard-π
      ; tuple = standard-tuple
      ; project = λ {Γ} → standard-project {Γ}
      ; unique = standard-unique }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
-- In a module instantiation 'module A = e', 'e' should have the form 'm e1 ..
-- en' where 'm' is a module name.
module NotAModuleExpr where

module Bad = \x -> x


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

open import HoTT
import homotopy.WedgeExtension as WedgeExt
import homotopy.SuspAdjointLoop as SAL

module homotopy.Freudenthal where

{- lemma (move this where?) -}
private
  move1-left-on-left : ∀ {i} {A : Type i} {x y : A} (p : x == y) (q : x == y)
    → ((! q) ∙ p == idp → p == q)
  move1-left-on-left p idp h = h

module FreudenthalEquiv
  {i} (n k : ℕ₋₂) (kle : k ≤T S n +2+ S n)
  (X : Ptd i) {{cX : is-connected (S (S n)) (de⊙ X)}} where

  Q : Susp (de⊙ X) → Type i
  Q x = Trunc k (north == x)

  ⊙up : X ⊙→ ⊙Ω (⊙Susp X)
  ⊙up = SAL.η _

  up = fst ⊙up

  Codes-mer-args : WedgeExt.args {a₀ = pt X} {b₀ = [_] {n = k} (pt X)}
  Codes-mer-args = record {n = S n; m = S n;
    P = λ _ _ → (Trunc k (de⊙ X) , raise-level-≤T kle Trunc-level);
    f = [_]; g = idf _; p = idp}

  Codes-mer : de⊙ X → Trunc k (de⊙ X) → Trunc k (de⊙ X)
  Codes-mer = WedgeExt.ext Codes-mer-args

  Codes-mer-β-l : (λ a → Codes-mer a [ pt X ]) == [_]
  Codes-mer-β-l = λ= $ WedgeExt.β-l {r = Codes-mer-args}

  Codes-mer-β-r : (λ b → Codes-mer (pt X) b) == idf _
  Codes-mer-β-r = λ= $ WedgeExt.β-r {r = Codes-mer-args}

  Codes-mer-coh : app= Codes-mer-β-l (pt X) == app= Codes-mer-β-r [ pt X ]
  Codes-mer-coh =
    app= Codes-mer-β-l (pt X)
      =⟨ app=-β (WedgeExt.β-l {r = Codes-mer-args}) (pt X) ⟩
    WedgeExt.β-l {r = Codes-mer-args} (pt X)
      =⟨ ! (move1-left-on-left _ _ (WedgeExt.coh {r = Codes-mer-args})) ⟩
    WedgeExt.β-r {r = Codes-mer-args} [ pt X ]
      =⟨ ! (app=-β (WedgeExt.β-r {r = Codes-mer-args}) [ pt X ]) ⟩
    app= Codes-mer-β-r [ pt X ] ∎

  Codes-mer-is-equiv : (x : de⊙ X) → is-equiv (Codes-mer x)
  Codes-mer-is-equiv =
    conn-extend (pointed-conn-out {n = S n} (de⊙ X) (pt X))
      (λ x' → (is-equiv (Codes-mer x') , is-equiv-level))
      (λ tt → transport is-equiv (! (Codes-mer-β-r)) (idf-is-equiv _))

  Codes-mer-equiv : (x : de⊙ X) → Trunc k (de⊙ X) ≃ Trunc k (de⊙ X)
  Codes-mer-equiv x = (Codes-mer x , Codes-mer-is-equiv x)

  Codes-mer-inv-x₀ : <– (Codes-mer-equiv (pt X)) == idf _
  Codes-mer-inv-x₀ =
       ap is-equiv.g (conn-extend-β
          (pointed-conn-out (de⊙ X) (pt X))
          (λ x' → (is-equiv (Codes-mer x') , is-equiv-level))
          _ unit)
     ∙ lemma (! (Codes-mer-β-r)) (snd $ ide _)
    where lemma : ∀ {i j} {A : Type i} {B : Type j} {f g : A → B}
            (α : f == g) (e : is-equiv f)
            → is-equiv.g (transport is-equiv α e) == is-equiv.g e
          lemma idp e = idp

  Codes : Susp (de⊙ X) → Type i
  Codes = SuspRec.f (Trunc k (de⊙ X)) (Trunc k (de⊙ X)) (ua ∘ Codes-mer-equiv)

  Codes-has-level : (x : Susp (de⊙ X)) → has-level k (Codes x)
  Codes-has-level = Susp-elim Trunc-level Trunc-level
                      (λ _ → prop-has-all-paths-↓)

  {-
    favonia:

    This equation should be true: [⊙Trunc-fmap ⊙up = (decodeN , decodeN-pt)].
    Maybe there is a way to refactor the following code so that
    pointedness is handled more elegantly.
  -}

  decodeN : Codes north → Trunc k (north' (de⊙ X) == north)
  decodeN = Trunc-fmap up

  decodeN-pt : decodeN [ pt X ] == [ idp ]
  decodeN-pt = snd (⊙Trunc-fmap ⊙up)

  decodeS : Codes south → Q south
  decodeS = Trunc-fmap merid

  encode₀ : {x : Susp (de⊙ X)} → north == x → Codes x
  encode₀ α = transport Codes α [ pt X ]

  encode : {x : Susp (de⊙ X)} → Trunc k (north == x) → Codes x
  encode {x} tα = Trunc-rec {{Codes-has-level x}} encode₀ tα

  abstract
    encode-decodeN : (c : Codes north) → encode (decodeN c) == c
    encode-decodeN = Trunc-elim
      {{λ _ → =-preserves-level Trunc-level}}
      (λ x →
        encode (decodeN [ x ])
          =⟨ idp ⟩
        coe (ap Codes (merid x ∙ ! (merid (pt X)))) [ pt X ]
          =⟨ ap-∙ Codes (merid x) (! (merid (pt X))) |in-ctx (λ w → coe w [ pt X ]) ⟩
        coe (ap Codes (merid x) ∙ ap Codes (! (merid (pt X)))) [ pt X ]
          =⟨ coe-∙ (ap Codes (merid x)) (ap Codes (! (merid (pt X)))) [ pt X ] ⟩
        coe (ap Codes (! (merid (pt X)))) (coe (ap Codes (merid x)) [ pt X ])
          =⟨ SuspRec.merid-β _ _ (ua ∘ Codes-mer-equiv) x
            |in-ctx (λ w → coe (ap Codes (! (merid (pt X)))) (coe w [ pt X ])) ⟩
        coe (ap Codes (! (merid (pt X)))) (coe (ua (Codes-mer-equiv x)) [ pt X ])
          =⟨ coe-β (Codes-mer-equiv x) [ pt X ]
            |in-ctx (λ w → coe (ap Codes (! (merid (pt X)))) w) ⟩
        coe (ap Codes (! (merid (pt X)))) (Codes-mer x [ pt X ])
          =⟨ app= Codes-mer-β-l x
            |in-ctx (λ w → coe (ap Codes (! (merid (pt X)))) w) ⟩
        coe (ap Codes (! (merid (pt X)))) [ x ]
          =⟨ coe-ap-! Codes (merid (pt X)) [ x ] ⟩
        coe! (ap Codes (merid (pt X))) [ x ]
          =⟨ SuspRec.merid-β _ _ (ua ∘ Codes-mer-equiv) (pt X)
            |in-ctx (λ w → coe! w [ x ]) ⟩
        coe! (ua (Codes-mer-equiv (pt X))) [ x ]
          =⟨ coe!-β (Codes-mer-equiv (pt X)) [ x ] ⟩
        <– (Codes-mer-equiv (pt X)) [ x ]
          =⟨ app= Codes-mer-inv-x₀ [ x ] ⟩
        [ x ] ∎)

  decode : {x : Susp (de⊙ X)} → Codes x → Q x
  decode {x} = Susp-elim
    {P = λ y → Codes y → Q y}
    decodeN decodeS
    (λ x' → ↓-→-from-transp (λ= (STS x')))
    x
    where
    abstract
      coh : {s₁ s₂ : Susp (de⊙ X)} (p : s₁ == s₂)
        → (ap (λ s → s ∙ p) (!-inv-r p))
          == ∙-assoc p (! p) p ∙ ap (λ s → p ∙ s) (!-inv-l p) ∙ ∙-unit-r p
      coh idp = idp

      P : de⊙ X → de⊙ X → (S (n +2+ (S n))) -Type (lmax i i)
      P = λ x₁ x₂ →
        ((transport Q (merid x₁) (Trunc-fmap up [ x₂ ])
          == Trunc-fmap merid (transport Codes (merid x₁) [ x₂ ])),
         =-preserves-level (raise-level-≤T kle Trunc-level))

      f : (a : de⊙ X) → fst (P a (pt X))
      f a =
        transport Q (merid a) [ up (pt X) ]
          =⟨ transport-Trunc (north ==_) (merid a) (up (pt X)) ⟩
        [ transport (north ==_) (merid a) (up (pt X)) ]
          =⟨ ap [_] $ transp-cst=idf {A = Susp (de⊙ X)} (merid a) (up (pt X)) ⟩
        [ (merid (pt X) ∙ ! (merid (pt X))) ∙ merid a ]
          =⟨ ap [_] $ ap (λ s → s ∙ merid a) (!-inv-r (merid (pt X))) ⟩
        [ merid a ]
          =⟨ idp ⟩
        Trunc-fmap merid [ a ]
          =⟨ ap (Trunc-fmap merid) (! (app= Codes-mer-β-l a)) ⟩
        Trunc-fmap merid (Codes-mer a [ pt X ])
          =⟨ ap (Trunc-fmap merid) (! (coe-β (Codes-mer-equiv a) [ pt X ])) ⟩
        Trunc-fmap merid (coe (ua (Codes-mer-equiv a)) [ pt X ])
          =⟨ ! (SuspRec.merid-β _ _ (ua ∘ Codes-mer-equiv) a)
            |in-ctx (λ w → Trunc-fmap merid (coe w [ pt X ])) ⟩
        Trunc-fmap merid (transport Codes (merid a) [ pt X ]) ∎

      g : (b : de⊙ X) → fst (P (pt X) b)
      g b =
        transport Q (merid (pt X)) [ up b ]
          =⟨ transport-Trunc (north ==_) (merid (pt X)) (up b) ⟩
        [ transport (north ==_) (merid (pt X)) (up b) ]
          =⟨ ap [_] $ transp-cst=idf {A = Susp (de⊙ X)} (merid (pt X)) (up b)  ⟩
        [ (merid b ∙ ! (merid (pt X))) ∙ merid (pt X) ]
          =⟨ ap [_] $ ∙-assoc (merid b) (! (merid (pt X))) (merid (pt X))
                      ∙ ap (λ s → merid b ∙ s) (!-inv-l (merid (pt X)))
                      ∙ ∙-unit-r (merid b) ⟩
        [ merid b ]
          =⟨ idp ⟩
        Trunc-fmap merid [ b ]
          =⟨ ap (Trunc-fmap merid) (! (app= Codes-mer-β-r [ b ])) ⟩
        Trunc-fmap merid (Codes-mer (pt X) [ b ])
          =⟨ ap (Trunc-fmap merid) (! (coe-β (Codes-mer-equiv (pt X)) [ b ])) ⟩
        Trunc-fmap merid (coe (ua (Codes-mer-equiv (pt X))) [ b ])
          =⟨ ! (SuspRec.merid-β _ _ (ua ∘ Codes-mer-equiv) (pt X))
            |in-ctx (λ w → Trunc-fmap merid (coe w [ b ])) ⟩
        Trunc-fmap merid (transport Codes (merid (pt X)) [ b ]) ∎

      p : f (pt X) == g (pt X)
      p = ap2
        (λ p₁ p₂ →
          transport Q (merid (pt X)) [ up (pt X) ]
            =⟨ transport-Trunc (north ==_) (merid (pt X)) (up (pt X)) ⟩
          [ transport (north ==_) (merid (pt X)) (up (pt X)) ]
            =⟨ ap [_] $ transp-cst=idf {A = Susp (de⊙ X)} (merid (pt X)) (up (pt X)) ⟩
          [ (merid (pt X) ∙ ! (merid (pt X))) ∙ merid (pt X) ]
            =⟨ ap [_] p₁ ⟩
          [ merid (pt X) ]
            =⟨ idp ⟩
          Trunc-fmap merid [ pt X ]
            =⟨ ap (Trunc-fmap merid) (! p₂) ⟩
          Trunc-fmap merid (Codes-mer (pt X) [ pt X ])
            =⟨ ap (Trunc-fmap merid) (! (coe-β (Codes-mer-equiv (pt X)) [ pt X ])) ⟩
          Trunc-fmap merid (coe (ua (Codes-mer-equiv (pt X))) [ pt X ])
            =⟨ ! (SuspRec.merid-β _ _ (ua ∘ Codes-mer-equiv) (pt X))
              |in-ctx (λ w → Trunc-fmap merid (coe w [ pt X ])) ⟩
          Trunc-fmap merid (transport Codes (merid (pt X)) [ pt X ]) ∎)
        (coh (merid (pt X))) Codes-mer-coh

      STS-args : WedgeExt.args {a₀ = pt X} {b₀ = pt X}
      STS-args =
        record {n = S n; m = S n; P = P; f = f; g = g; p = p}

      STS : (x' : de⊙ X) (c : Codes north) →
        transport Q (merid x') (Trunc-fmap up c)
        == Trunc-fmap merid (transport Codes (merid x') c)
      STS x' = Trunc-elim {{λ _ → =-preserves-level Trunc-level}}
                          (WedgeExt.ext STS-args x')

  abstract
    decode-encode : {x : Susp (de⊙ X)} (tα : Q x)
      → decode {x} (encode {x} tα) == tα
    decode-encode {x} = Trunc-elim
      {P = λ tα → decode {x} (encode {x} tα) == tα}
      {{λ _ → =-preserves-level Trunc-level}}
      (J (λ y p → decode {y} (encode {y} [ p ]) == [ p ])
         (ap [_] (!-inv-r (merid (pt X)))))

  eq : Trunc k (de⊙ X) ≃ Trunc k (north' (de⊙ X) == north)
  eq = equiv decodeN encode decode-encode encode-decodeN

  ⊙eq : ⊙Trunc k X ⊙≃ ⊙Trunc k (⊙Ω (⊙Susp X))
  ⊙eq = ≃-to-⊙≃ eq (ap [_] (!-inv-r (merid (pt X))))

  path : Trunc k (de⊙ X) == Trunc k (north' (de⊙ X) == north)
  path = ua eq

  ⊙path : ⊙Trunc k X == ⊙Trunc k (⊙Ω (⊙Susp X))
  ⊙path = ⊙ua ⊙eq

{- Used to prove stability in iterated suspensions -}
module FreudenthalIso
  {i} (n : ℕ₋₂) (k : ℕ) (kle : ⟨ S k ⟩ ≤T S n +2+ S n)
  (X : Ptd i) {{_ : is-connected (S (S n)) (de⊙ X)}} where

  open FreudenthalEquiv n ⟨ S k ⟩ kle X public

  hom : Ω^S-group k (⊙Trunc ⟨ S k ⟩ X)
     →ᴳ Ω^S-group k (⊙Trunc ⟨ S k ⟩ (⊙Ω (⊙Susp X)))
  hom = Ω^S-group-fmap k (decodeN , decodeN-pt)

  iso : Ω^S-group k (⊙Trunc ⟨ S k ⟩ X)
     ≃ᴳ Ω^S-group k (⊙Trunc ⟨ S k ⟩ (⊙Ω (⊙Susp X)))
  iso = Ω^S-group-emap k ⊙eq

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Structure.Groupoid.Functor where

open import Functional using (_on₂_)
open import Lang.Instance
import      Lvl
open import Logic.Predicate
open import Structure.Category
import      Structure.Category.Functor as Category
open import Structure.Function
open import Structure.Groupoid
import      Structure.Relator.Names as Names
open import Structure.Setoid
open import Syntax.Function
open import Type

private variable ℓ ℓₒ ℓₘ ℓₗₒ ℓₗₘ ℓᵣₒ ℓᵣₘ ℓₑ ℓₗₑ ℓᵣₑ : Lvl.Level
private variable Obj Objₗ Objᵣ : Type{ℓ}
private variable _⟶_ _⟶ₗ_ _⟶ᵣ_ : Objₗ → Objᵣ → Type{ℓ}

module _
  ⦃ morphism-equivₗ : ∀{x y : Objₗ} → Equiv{ℓₗₑ}(x ⟶ₗ y) ⦄
  ⦃ morphism-equivᵣ : ∀{x y : Objᵣ} → Equiv{ℓᵣₑ}(x ⟶ᵣ y) ⦄
  (Groupoidₗ : Groupoid(_⟶ₗ_))
  (Groupoidᵣ : Groupoid(_⟶ᵣ_))
  where

  -- A covariant functor.
  -- A mapping which transforms objects and morphisms from one category to another while "preserving" the groupoid structure.
  -- A homomorphism between groupoids.
  record Functor (F : Objₗ → Objᵣ) : Type{Lvl.of(Type.of(Groupoidₗ)) Lvl.⊔ Lvl.of(Type.of(Groupoidᵣ))} where
    constructor intro
    open Groupoid ⦃ … ⦄

    private instance _ = Groupoidₗ
    private instance _ = Groupoidᵣ

    field
      map : Names.Subrelation(_⟶ₗ_) ((_⟶ᵣ_) on₂ F)

    field
      ⦃ map-function ⦄     : ∀{x y} → Function(map{x}{y})
      ⦃ op-preserving ⦄    : ∀{x y z : Objₗ}{f : y ⟶ₗ z}{g : x ⟶ₗ y} → (map(f ∘ g) ≡ map(f) ∘ map(g))
      ⦃ inv-preserving ⦄   : ∀{x y : Objₗ}{f : x ⟶ₗ y} → (map(inv f) ≡ inv(map f))
      ⦃ id-preserving ⦄    : ∀{x : Objₗ} → (map(id {x = x}) ≡ id)

    categoryFunctor : Category.Functor(category ⦃ r = Groupoidₗ ⦄)(category ⦃ r = Groupoidᵣ ⦄) (F)
    Category.Functor.map           categoryFunctor = map
    Category.Functor.map-function  categoryFunctor = map-function
    Category.Functor.op-preserving categoryFunctor = op-preserving
    Category.Functor.id-preserving categoryFunctor = id-preserving
    open Category.Functor(categoryFunctor) public hiding (map ; map-function ; op-preserving ; id-preserving)

module _
  ⦃ morphism-equiv : ∀{x y : Obj} → Equiv{ℓₑ}(x ⟶ y) ⦄
  (Groupoid : Groupoid(_⟶_))
  where

  Endofunctor = Functor(Groupoid)(Groupoid)
  module Endofunctor = Functor{Groupoidₗ = Groupoid}{Groupoidᵣ = Groupoid}

_→ᶠᵘⁿᶜᵗᵒʳ_ : GroupoidObject{ℓₗₒ}{ℓₗₘ}{ℓₗₑ} → GroupoidObject{ℓᵣₒ}{ℓᵣₘ}{ℓᵣₑ} → Type
grpₗ →ᶠᵘⁿᶜᵗᵒʳ grpᵣ = ∃(Functor (GroupoidObject.groupoid(grpₗ)) ((GroupoidObject.groupoid(grpᵣ))))

⟲ᶠᵘⁿᶜᵗᵒʳ_ : GroupoidObject{ℓₒ}{ℓₘ}{ℓₑ} → Type
⟲ᶠᵘⁿᶜᵗᵒʳ grp = grp →ᶠᵘⁿᶜᵗᵒʳ grp

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module _ where

open import Agda.Builtin.Nat using (mod-helper)
open import Common.Prelude
open import Common.Equality

_mod_ : Nat → Nat → Nat
n mod zero  = 0
n mod suc m = mod-helper 0 m n m

{-# INLINE _mod_ #-}

primitive
  primForce      : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x
  primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x

force      = primForce
forceLemma = primForceLemma

infixr 0 _$!_
_$!_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x → B x
f $! x = force x f

-- Memory leak without proper seq --

pow′ : Nat → Nat → Nat
pow′ zero    acc = acc
pow′ (suc n) acc = pow′ n $! (acc + acc) mod 234576373

pow : Nat → Nat
pow n = pow′ n 1

main : IO Unit
main = printNat (pow 5000000)


text:
module PLRTree.Complete {A : Set} where

open import PLRTree {A}
open import PLRTree.Equality {A}

data _⋗_ :  PLRTree → PLRTree → Set where
  ⋗lf : (x : A)
                   → node perfect x leaf leaf ⋗ leaf
  ⋗nd : {l r l' r' : PLRTree}
                   (x x' : A)
                   → l ≃ r
                   → l' ≃ r'
                   → l ⋗ l'
                   → node perfect x l r ⋗ node perfect x' l' r'

mutual
  data _⋘_ : PLRTree → PLRTree → Set where
    x⋘ : (x y z : A)
                  → node right x (node perfect y leaf leaf) leaf ⋘ node perfect z leaf leaf
    l⋘ : {l r l' r' : PLRTree}
                  → (x x' : A)
                  → l ⋘ r
                  → l' ≃ r'
                  → r ≃ l'
                  → (node left x l r) ⋘ (node perfect x' l' r')
    r⋘ : {l r l' r' : PLRTree}
                  → (x x' : A)
                  → l ⋙ r
                  → l' ≃ r'
                  → l ⋗ l'
                  → (node right x l r) ⋘ (node perfect x' l' r')

  data _⋙_ : PLRTree → PLRTree → Set where
    ⋙p : {l r : PLRTree}
                  → l ⋗ r
                  → l ⋙ r
    ⋙l : {l r l' r' : PLRTree}
                  → (x x' : A)
                  → l ≃ r
                  → l' ⋘ r'
                  → l ⋗ r'
                  → (node perfect x l r) ⋙ (node left x' l' r')
    ⋙r : {l r l' r' : PLRTree}
                  → (x x' : A)
                  → l ≃ r
                  → l' ⋙ r'
                  → l ≃ l'
                  → (node perfect x l r) ⋙ (node right x' l' r')

data Complete : PLRTree → Set where
  leaf : Complete leaf
  perfect : {l r : PLRTree}
                   (x : A)
                   → Complete l
                   → Complete r
                   → l ≃ r
                   → Complete (node perfect x l r)
  left : {l r : PLRTree}
                   (x : A)
                   → Complete l
                   → Complete r
                   → l ⋘ r
                   → Complete (node left x l r)
  right : {l r : PLRTree}
                   (x : A)
                   → Complete l
                   → Complete r
                   → l ⋙ r
                   → Complete (node right x l r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-
-- an ≃ equivalence of types can be lifted to a ≃S equivalence
-- (over their ≡-Setoids)
-- NOT NEEDED
lift≃ : ∀ {ℓ} → {A B : Set ℓ} → A ≃ B → (≡-Setoid A) ≃S (≡-Setoid B)
lift≃ {_} {A} {B} (f , mkqinv g α β) = equiv AS BS α' β'
  where
    module AA = Setoid (≡-Setoid A)
    module BB = Setoid (≡-Setoid B)
    AS : ≡-Setoid A ⟶ ≡-Setoid B
    AS = →to⟶ f
    BS : ≡-Setoid B ⟶ ≡-Setoid A
    BS = →to⟶ g
    α' : {x y : B} → P._≡_ x y → P._≡_ (f (g x)) y
    α' = λ {x} {y} p → BB.trans (α x) p
    β' : {x y : A} → P._≡_ x y → P._≡_ (g (f x)) y
    β' = λ {x} {y} p → AA.trans (β x) p

-}


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

open import lib.Basics
open import lib.NType2
open import lib.types.Bool
open import lib.types.Empty
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Sigma

{-
This file contains various lemmas that rely on lib.types.Paths or
functional extensionality for pointed maps.
-}

module lib.types.Pointed where

{- Pointed maps -}

-- function extensionality for pointed maps
⊙λ= : ∀ {i j} {X : Ptd i} {Y : Ptd j} {f g : X ⊙→ Y}
  (p : ∀ x → fst f x == fst g x)
  (α : snd f == snd g [ (λ y → y == pt Y) ↓ p (pt X) ])
  → f == g
⊙λ= {g = g} p α =
  pair= (λ= p) (↓-app=cst-in (↓-idf=cst-out α ∙ ap (_∙ snd g) (! (app=-β p _))))

{-
⊙λ=' : ∀ {i j} {X : Ptd i} {Y : Ptd j} {f g : X ⊙→ Y}
  (p : ∀ x → fst f x == fst g x) (α : snd f == p (pt X) ∙ snd g)
  → f == g
⊙λ=' p α = ⊙λ= p (↓-idf=cst-in α)
-}

-- associativity of pointed maps
⊙∘-assoc-pt : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  {a₁ a₂ : A} (f : A → B) {b : B} (g : B → C) {c : C}
  (p : a₁ == a₂) (q : f a₂ == b) (r : g b == c)
  → ⊙∘-pt (g ∘ f) p (⊙∘-pt g q r) == ⊙∘-pt g (⊙∘-pt f p q) r
⊙∘-assoc-pt _ _ idp _ _ = idp

⊙∘-assoc : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (h : Z ⊙→ W) (g : Y ⊙→ Z) (f : X ⊙→ Y)
  → ((h ⊙∘ g) ⊙∘ f) == (h ⊙∘ (g ⊙∘ f))
⊙∘-assoc (h , hpt) (g , gpt) (f , fpt) = ⊙λ= (λ _ → idp) (⊙∘-assoc-pt g h fpt gpt hpt)

{- Pointed equivalences -}

-- Extracting data from an pointed equivalence
module _ {i j} {X : Ptd i} {Y : Ptd j} (⊙e : X ⊙≃ Y) where

  private
    e : de⊙ X ≃ de⊙ Y
    e = (fst (fst ⊙e) , snd ⊙e)

  ⊙≃-to-≃ = e

  ⊙–>-pt : –> e (pt X) == pt Y
  ⊙–>-pt = snd (fst ⊙e)

  private
    p = ⊙–>-pt

  ⊙–> : X ⊙→ Y
  ⊙–> = fst ⊙e

  ⊙<–-pt : <– e (pt Y) == pt X
  ⊙<–-pt = ap (<– e) (! ⊙–>-pt) ∙ <–-inv-l e (pt X)

  ⊙<– : Y ⊙→ X
  ⊙<– = <– e , ⊙<–-pt

  infix 120 _⊙⁻¹
  _⊙⁻¹ : Y ⊙≃ X
  _⊙⁻¹ = ⊙<– , is-equiv-inverse (snd ⊙e)

  ⊙<–-inv-l : ⊙<– ⊙∘ ⊙–> == ⊙idf _
  ⊙<–-inv-l = ⊙λ= (<–-inv-l e) $ ↓-idf=cst-in $
    ap (<– e) p ∙ ap (<– e) (! p) ∙ <–-inv-l e (pt X)
      =⟨ ! (∙-assoc (ap (<– e) p) (ap (<– e) (! p)) (<–-inv-l e (pt X))) ⟩
    (ap (<– e) p ∙ ap (<– e) (! p)) ∙ <–-inv-l e (pt X)
      =⟨ ∙-ap (<– e) p (! p) ∙ ap (ap (<– e)) (!-inv-r p)
         |in-ctx (λ w → w ∙ <–-inv-l e (pt X)) ⟩
    <–-inv-l e (pt X)
      =⟨ ! (∙-unit-r _) ⟩
    <–-inv-l e (pt X) ∙ idp =∎

  ⊙<–-inv-r : ⊙–> ⊙∘ ⊙<– == ⊙idf _
  ⊙<–-inv-r = ⊙λ= (<–-inv-r e) $ ↓-idf=cst-in $
    ap (–> e) (ap (<– e) (! p) ∙ <–-inv-l e (pt X)) ∙ p
      =⟨ ap-∙ (–> e) (ap (<– e) (! p)) (<–-inv-l e (pt X))
         |in-ctx (λ w → w ∙ p) ⟩
    (ap (–> e) (ap (<– e) (! p)) ∙ ap (–> e) (<–-inv-l e (pt X))) ∙ p
      =⟨ <–-inv-adj e (pt X)
         |in-ctx (λ w → (ap (–> e) (ap (<– e) (! p)) ∙ w) ∙ p) ⟩
    (ap (–> e) (ap (<– e) (! p)) ∙ <–-inv-r e (–> e (pt X))) ∙ p
      =⟨ ∘-ap (–> e) (<– e) (! p)
         |in-ctx (λ w → (w ∙ <–-inv-r e (–> e (pt X))) ∙ p) ⟩
    (ap (–> e ∘ <– e) (! p) ∙ <–-inv-r e (–> e (pt X))) ∙ p
      =⟨ ap (_∙ p) (! (↓-app=idf-out (apd (<–-inv-r e) (! p))))  ⟩
    (<–-inv-r e (pt Y) ∙' (! p)) ∙ p
      =⟨ ∙'=∙ (<–-inv-r e (pt Y)) (! p) |in-ctx _∙ p ⟩
    (<–-inv-r e (pt Y) ∙ (! p)) ∙ p
      =⟨ ∙-assoc (<–-inv-r e (pt Y)) (! p) p ⟩
    <–-inv-r e (pt Y) ∙ (! p ∙ p)
      =⟨ !-inv-l p |in-ctx (<–-inv-r e (pt Y)) ∙_ ⟩
    <–-inv-r e (pt Y) ∙ idp =∎

module _ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} (⊙e : X ⊙≃ Y) where

  post⊙∘-is-equiv : is-equiv (λ (k : Z ⊙→ X) → ⊙–> ⊙e ⊙∘ k)
  post⊙∘-is-equiv = is-eq f g f-g g-f
    where f = ⊙–> ⊙e ⊙∘_
          g = ⊙<– ⊙e ⊙∘_
          abstract
            f-g = λ k → ! (⊙∘-assoc (⊙–> ⊙e) (⊙<– ⊙e) k) ∙ ap (_⊙∘ k) (⊙<–-inv-r ⊙e) ∙ ⊙∘-unit-l k
            g-f = λ k → ! (⊙∘-assoc (⊙<– ⊙e) (⊙–> ⊙e) k) ∙ ap (_⊙∘ k) (⊙<–-inv-l ⊙e) ∙ ⊙∘-unit-l k

  pre⊙∘-is-equiv : is-equiv (λ (k : Y ⊙→ Z) → k ⊙∘ ⊙–> ⊙e)
  pre⊙∘-is-equiv = is-eq f g f-g g-f
    where f = _⊙∘ ⊙–> ⊙e
          g = _⊙∘ ⊙<– ⊙e
          abstract
            f-g = λ k → ⊙∘-assoc k (⊙<– ⊙e) (⊙–> ⊙e) ∙ ap (k ⊙∘_) (⊙<–-inv-l ⊙e) ∙ ⊙∘-unit-r k
            g-f = λ k → ⊙∘-assoc k (⊙–> ⊙e) (⊙<– ⊙e) ∙ ap (k ⊙∘_) (⊙<–-inv-r ⊙e) ∙ ⊙∘-unit-r k

  pre⊙∘-equiv : (Y ⊙→ Z) ≃ (X ⊙→ Z)
  pre⊙∘-equiv = _ , pre⊙∘-is-equiv

{- Pointed maps out of bool -}

-- intuition : [f true] is fixed and the only changable part is [f false].

⊙Bool→-to-idf : ∀ {i} {X : Ptd i}
  → ⊙Bool ⊙→ X → de⊙ X
⊙Bool→-to-idf (h , _) = h false

⊙Bool→-equiv-idf : ∀ {i} (X : Ptd i)
  → (⊙Bool ⊙→ X) ≃ de⊙ X
⊙Bool→-equiv-idf {i} X = equiv ⊙Bool→-to-idf g f-g g-f
  where
  g : de⊙ X → ⊙Bool ⊙→ X
  g x = (if_then pt X else x) , idp

  abstract
    f-g : ∀ x → ⊙Bool→-to-idf (g x) == x
    f-g x = idp

    g-f : ∀ H → g (⊙Bool→-to-idf H) == H
    g-f (h , hpt) = pair=
      (λ= lemma)
      (↓-app=cst-in $
        idp
          =⟨ ! (!-inv-l hpt) ⟩
        ! hpt ∙ hpt
          =⟨ ! (app=-β lemma true) |in-ctx (λ w → w ∙ hpt) ⟩
        app= (λ= lemma) true ∙ hpt
          =∎)
      where lemma : ∀ b → fst (g (h false)) b == h b
            lemma true = ! hpt
            lemma false = idp

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module AndOrNot where

open import Data.Bool
open import Data.Product

test : Bool → Bool → Bool × Bool × Bool
test x y = x ∧ y , x ∨ y , not x

max_stars_repo_name: mullikine/RosettaCodeData

max_issues_repo_name: seanwallawalla-forks/RosettaCodeData

max_forks_repo_name: seanwallawalla-forks/RosettaCodeData


text:
open import Prelude

module Implicits.Resolution.GenericFinite.Algorithm.Soundness where

open import Induction.WellFounded
open import Induction.Nat
open import Data.List
open import Data.List.Any
open Membership-≡
open import Data.Fin.Substitution
open import Data.Nat.Base using (_<′_)
open import Data.Maybe as Maybe
open import Data.Nat hiding (_<_)
open import Data.Nat.Properties
open import Relation.Binary using (module DecTotalOrder)
open DecTotalOrder decTotalOrder using () renaming (refl to ≤-refl; trans to ≤-trans)

open import Implicits.Syntax
open import Implicits.Syntax.Type.Unification
open import Implicits.Syntax.Type.Unification.Lemmas as mgu hiding (sound)
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Implicits.Resolution.GenericFinite.Resolution
open import Implicits.Resolution.GenericFinite.Algorithm
open import Implicits.Resolution.GenericFinite.TerminationCondition
open import Implicits.Resolution.Termination

open import Data.Vec hiding (_∈_)
open import Extensions.Bool as Bl

private
  module M = MetaTypeMetaSubst

module ResolutionSound (cond : TerminationCondition) where

  open TerminationCondition cond
  open ResolutionAlgorithm cond
  open ResolutionRules cond

  open Lemmas

  postulate lem₄ : ∀ {m ν} (a : MetaType m (suc ν)) u us →
                   from-meta ((M.open-meta a) M./ (us M.↑) M./ (M.sub u))
                     ≡ (from-meta (a M./ (us M.↑tp))) tp[/tp from-meta u ]

  open-↓-∀ : ∀ {ν m} {Δ : ICtx ν} {Φ} (a : MetaType m (suc ν)) τ u us →
        Δ , Φ ⊢ (from-meta ((open-meta a) M./ (u ∷ us))) ↓ τ →
        Δ , Φ ⊢ (from-meta (∀' a M./ us)) ↓ τ
  open-↓-∀ {Δ = Δ} {Φ = Φ} a τ u us p = (i-tabs (from-meta u) (subst (λ v → Δ , Φ ⊢ v ↓ τ) (begin
        from-meta (M._/_ (open-meta a) (u ∷ us))
          ≡⟨ cong (λ v → from-meta (M._/_ (open-meta a) v)) (sym $ us↑-⊙-sub-u≡u∷us u us) ⟩
        from-meta ((open-meta a) M./ (us M.↑ M.⊙ (M.sub u)))
          ≡⟨ cong from-meta (/-⊙ (open-meta a)) ⟩
        from-meta ((open-meta a) M./ us M.↑ M./ (M.sub u))
          ≡⟨ lem₄ a u us ⟩
        from-meta (M._/_ a (us M.↑tp)) tp[/tp from-meta u ] ∎) p))
      where open MetaTypeMetaLemmas hiding (subst)

  mutual
    match'-sound : ∀ {ν m} (Δ : ICtx ν) (Φ : TCtx) τ (r : MetaType m ν) →
                  (Φ↓ : T-Acc Φ) → (m↓ : m<-Acc r) →
                  Maybe.All (λ u → Δ , Φ ⊢ from-meta (r M./ u) ↓ τ) (match' Δ Φ τ r Φ↓ m↓)
    match'-sound Δ Φ τ (a ⇒ b) Φ↓ (acc m↓)
      with match'       Δ Φ τ b Φ↓ (m↓ _ (b-m<-a⇒b a b))
         | match'-sound Δ Φ τ b Φ↓ (m↓ _ (b-m<-a⇒b a b))
    match'-sound Δ Φ τ (a ⇒ b) Φ↓ (acc m↓) | just u | just pu
      with (step Φ Δ (from-meta (a M./ u)) (from-meta (b M./ u)) τ) <? Φ
    match'-sound Δ Φ τ (a ⇒ b) (acc Φ↓) (acc m↓) | just u | just pu | no Φ> = nothing
    match'-sound Δ Φ τ (a ⇒ b) (acc Φ↓) (acc m↓) | just u | just pu | yes Φ<
      with resolve' Δ (step Φ Δ (from-meta (a M./ u)) (from-meta (b M./ u)) τ)
                    (from-meta (a M./ u)) (Φ↓ _ Φ<)
         | sound'   Δ (step Φ Δ (from-meta (a M./ u)) (from-meta (b M./ u)) τ)
                    (from-meta (a M./ u)) (Φ↓ _ Φ<)
    match'-sound Δ Φ τ (a ⇒ b) (acc Φ↓) (acc m↓) | just u | just pu | yes Φ< | true | true px =
      just (i-iabs Φ< px pu)
    match'-sound Δ Φ τ (a ⇒ b) (acc Φ↓) (acc m↓) | just u | just pu | yes Φ< | false | false = nothing
    match'-sound Δ Φ τ (a ⇒ b) (acc Φ↓) (acc m↓) | nothing | _ = nothing
    match'-sound Δ Φ τ (∀' r) Φ↓ (acc m↓)
      with match'       Δ Φ τ (open-meta r) Φ↓ (m↓ _ (open-meta-a-m<-∀'a r))
         | match'-sound Δ Φ τ (open-meta r) Φ↓ (m↓ _ (open-meta-a-m<-∀'a r))
    match'-sound Δ Φ τ (∀' r) Φ↓ (acc m↓) | just (u ∷ us) | just px = just (open-↓-∀ r τ u us px)
    match'-sound Δ Φ τ (∀' r) Φ↓ (acc m↓) | nothing | nothing = nothing
    match'-sound Δ Φ τ (simpl x) Φ↓ m↓ with mgu (simpl x) τ | mgu.sound (simpl x) τ
    match'-sound Δ Φ τ (simpl x) Φ↓ m↓ | just _ | just px =
      just (subst (λ z → Δ , Φ ⊢ z ↓ τ) (sym px) (i-simp τ))
    match'-sound Δ Φ τ (simpl x) Φ↓ m↓ | nothing | nothing = nothing

    match-sound : ∀ {ν} (Δ : ICtx ν) (Φ : TCtx) τ r → (Φ↓ : T-Acc Φ) →
                  Bl.All (Δ , Φ ⊢ r ↓ τ) (match Δ Φ τ r Φ↓)
    match-sound Δ Φ τ r Φ↓ with
      match' Δ Φ τ (to-meta {zero} r) Φ↓ (m<-well-founded _) |
      match'-sound Δ Φ τ (to-meta {zero} r) Φ↓ (m<-well-founded _)
    match-sound Δ Φ τ r Φ↓ | just x | just px = true (subst (λ z → Δ , Φ ⊢ z ↓ τ) eq px)
      where
        eq : ∀ {ν} {a : Type ν} {s} → from-meta (to-meta {zero} a M./ s) ≡ a
        eq {a = a} {s = []} = begin
            from-meta (M._/_ (to-meta {zero} a) [])
          ≡⟨ cong (λ q → from-meta q) (MetaTypeMetaLemmas.id-vanishes (to-meta {zero} a)) ⟩
            from-meta (to-meta {zero} a)
          ≡⟨ to-meta-zero-vanishes ⟩
            a ∎
    match-sound Δ Φ τ r Φ↓ | nothing | q = false

    match1st-sound : ∀ {ν} (Δ : ICtx ν) (Φ : TCtx) (ρs : ICtx ν) → (τ : SimpleType ν) → (Φ↓ : T-Acc Φ) →
                    Bl.All (∃ λ r → (r ∈ ρs) × (Δ , Φ ⊢ r ↓ τ)) (match1st Δ Φ ρs τ Φ↓)
    match1st-sound Δ Φ [] τ Φ↓ = false
    match1st-sound Δ Φ (x ∷ ρs) τ Φ↓ with match Δ Φ τ x Φ↓ | match-sound Δ Φ τ x Φ↓
    match1st-sound Δ Φ (x ∷ ρs) τ Φ↓ | true | true px = true (x , (here refl , px))
    match1st-sound Δ Φ (x ∷ ρs) τ Φ↓ | false | false =
      all-map (match1st-sound Δ Φ ρs τ Φ↓) (λ{ (r , r∈ρs , r↓τ) → r , ((there r∈ρs) , r↓τ) })

    sound' : ∀ {ν} (Δ : ICtx ν) Φ r → (Φ↓ : T-Acc Φ) → Bl.All (Δ , Φ ⊢ᵣ r) (resolve' Δ Φ r Φ↓)
    sound' Δ Φ (simpl x) Φ↓ =
      all-map (match1st-sound Δ Φ Δ x Φ↓) (λ{ (r , r∈Δ , r↓τ) → r-simp r∈Δ r↓τ })
    sound' Δ Φ (a ⇒ b) Φ↓ = all-map (sound' (a ∷ Δ) Φ b Φ↓) (λ x → r-iabs a x)
    sound' Δ Φ (∀' r) Φ↓ = all-map (sound' (ictx-weaken Δ) Φ r Φ↓) r-tabs

    sound : ∀ {ν} (Δ : ICtx ν) r {Φ} → (Φ↓ : T-Acc Φ) → Bl.All (Δ , Φ ⊢ᵣ r) (resolve Δ Φ r)
    sound Δ r Φ↓ = sound' Δ _ r (wf-< _)


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

module Categories.Adjoint.Instance.PathsOf where

-- PathsOf is adjoint to Underlying Quiver, i.e.
-- The "Underlying Graph" (of a Category) <-> "Path Category on a Quiver" Adjunction.

-- Lots of surprises here, of various level of surprisingness
-- 1. The PathCategory rises universe levels of arrows (and equivalences); the Underlying Quiver does not
--   (due to the Transitive Closure "Star" construction)
-- 2. As a consequence of (1), the eventual Adjunction will be for all Levels being the same
-- 3. To build a Functor from Categories to Quivers, then the object/hom levels are straightforward,
--   but "Categories" has NaturalIsomorphism as the notion of equivalence of Functors. This means
--   that, for example, the 2-point Groupoid is contractible
--   (thus equivalent to the 1-point Category), and yet those two "Graphs" shouldn't be considered to
--   be the same!  This is because there isn't an equivalently natural notion of equivalence of
--   Graph (Quiver) Homomorphism.
--   Interestingly, this only shows up when trying to prove that the Underlying Functor respects
--   _≈_, which is not traditionally a requirement of a Functor! This requirement is usually left
--   implicit.  (See Categories.Function.Construction.FreeCategory for the details)
--
-- In other words, the adjunction doesn't involve Cats, but StrictCats as one of the endpoints.

open import Level
open import Function using (_$_; flip) renaming (id to id→; _∘_ to _⊚_)
import Relation.Binary.PropositionalEquality as ≡
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Data.Quiver using (Quiver)
open import Data.Quiver.Paths
import Data.Quiver.Morphism as QM
open QM using (Morphism; _≃_)

open import Categories.Adjoint using (Adjoint)
open import Categories.Category.Core using (Category)
import Categories.Category.Construction.PathCategory as PC
open import Categories.Category.Instance.Quivers
open import Categories.Functor using (Functor)
open import Categories.Functor.Construction.PathsOf using (PathsOf)
open import Categories.Functor.Instance.UnderlyingQuiver using (Underlying₀; Underlying₁; Underlying)
open import Categories.NaturalTransformation using (ntHelper)
import Categories.Morphism.Reasoning as MR

module _ (o ℓ e : Level) where

  -- the unit morphism from a Quiver X to U∘Free X.
  unit : (X : Quiver o (o ⊔ ℓ) (o ⊔ ℓ ⊔ e)) → Morphism X (Underlying₀ (PC.PathCategory X))
  unit X = let open Paths X in record { F₀ = id→ ; F₁ = return ; F-resp-≈ = _◅ ε }

  module _ (X : Category o (o ⊔ ℓ) (o ⊔ ℓ ⊔ e)) where
    open Category X
    open HomReasoning
    open Paths (Underlying₀ X)

    -- "unwind" a path by using repeated composition
    unwind : {A B : Obj} → Star _⇒_ A B → A ⇒ B
    unwind = fold _⇒_ (flip _∘_) id

    unwind-◅◅ : {A B C : Obj} {f : Star _⇒_ A B} {g : Star _⇒_ B C} →
                unwind (f ◅◅ g) ≈ (unwind g) ∘ (unwind f)
    unwind-◅◅ {f = ε} {g} = Equiv.sym identityʳ
    unwind-◅◅ {f = x ◅ f} {g} = ∘-resp-≈ˡ (unwind-◅◅ {f = f} {g}) ○ assoc

    unwind-resp-≈ : {A B : Obj} {f g : Star _⇒_ A B} → f ≈* g → unwind f ≈ unwind g
    unwind-resp-≈ ε = Equiv.refl
    unwind-resp-≈ (x ◅ eq) = ∘-resp-≈ (unwind-resp-≈ eq) x

    unwindF : Functor (PC.PathCategory (Underlying₀ X)) X
    unwindF = record
        { F₀ = id→
        ; F₁ = unwind
        ; identity = Category.Equiv.refl X
        ; homomorphism = λ { {f = f} {g} → unwind-◅◅ {f = f} {g} }
        ; F-resp-≈ = unwind-resp-≈
        }

  module _ (X : Quiver o (o ⊔ ℓ) (o ⊔ ℓ ⊔ e)) where
    open Paths X

    zig′ : {A B : Quiver.Obj X} → (f : Star (Quiver._⇒_ X) A B) →
      unwind (PC.PathCategory X) (QM.qmap (unit X) f) ≈* f
    zig′ ε        = ε
    zig′ (fs ◅ f) = Quiver.Equiv.refl X ◅ zig′ f

  module _ {X Y : Category o (o ⊔ ℓ) (o ⊔ ℓ ⊔ e)} (F : Functor X Y) where
    module X = Category X
    module Y = Category Y
    open Category.HomReasoning Y
    open Functor F
    unwind-natural : {A B : X.Obj} (f : Star X._⇒_ A B) → unwind Y (QM.qmap (Underlying₁ F) f) Y.≈ F₁ (unwind X f)
    unwind-natural ε = Y.Equiv.sym identity
    unwind-natural (x ◅ f) = Y.Equiv.sym (homomorphism ○ Category.∘-resp-≈ˡ Y (Y.Equiv.sym (unwind-natural f)))

  Free⊣Underlying : Adjoint (PathsOf {o} {o ⊔ ℓ} {o ⊔ ℓ ⊔ e}) Underlying
  Free⊣Underlying = record
    { unit = ntHelper record
      { η = unit
      ; commute = λ {X} {Y} f → let open Paths Y in record { F₀≡ = ≡.refl ; F₁≡ = Quiver.Equiv.refl Y ◅ ε }
      }
    ; counit = ntHelper record
      { η = unwindF
      ; commute = λ {_} {Y} F → record
        { eq₀ = λ _ → ≡.refl
        ; eq₁ = λ f → toSquare Y (unwind-natural F f)
        }
      }
    ; zig = λ {G} → record
      { eq₀ = λ _ → ≡.refl
      ; eq₁ = λ f → toSquare (PC.PathCategory G) (zig′ G f)
      }
    ; zag = λ {B} → record { F₀≡ = ≡.refl ; F₁≡ = Category.identityˡ B  }
    }
    where
    open MR using (toSquare)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Type(s) used (only) when calling out to Haskell via the FFI
------------------------------------------------------------------------

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

module Foreign.Haskell where

open import Level

-- A unit type.

data Unit : Set where
  unit : Unit

{-# COMPILE GHC Unit = data () (()) #-}
{-# COMPILE UHC Unit = data __UNIT__ (__UNIT__) #-}

-- A pair type

record Pair {ℓ ℓ′ : Level} (A : Set ℓ) (B : Set ℓ′) : Set (ℓ ⊔ ℓ′) where
  constructor _,_
  field  fst : A
         snd : B
open Pair public

{-# FOREIGN GHC type AgdaPair l1 l2 a b = (a , b) #-}
{-# COMPILE GHC Pair = data MAlonzo.Code.Foreign.Haskell.AgdaPair ((,)) #-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some unit types
------------------------------------------------------------------------

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

module Data.Unit where

open import Data.Sum
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl)

-- Some types are defined in Data.Unit.Base.

open import Data.Unit.Base public

------------------------------------------------------------------------
-- Operations

infix 4 _≟_ _≤?_

_≟_ : Decidable {A = ⊤} _≡_
_ ≟ _ = yes refl

_≤?_ : Decidable _≤_
_ ≤? _ = yes _

total : Total _≤_
total _ _ = inj₁ _

------------------------------------------------------------------------
-- Properties

preorder : Preorder _ _ _
preorder = PropEq.preorder ⊤

setoid : Setoid _ _
setoid = PropEq.setoid ⊤

decTotalOrder : DecTotalOrder _ _ _
decTotalOrder = record
  { Carrier         = ⊤
  ; _≈_             = _≡_
  ; _≤_             = _≤_
  ; isDecTotalOrder = record
      { isTotalOrder = record
          { isPartialOrder = record
              { isPreorder = record
                  { isEquivalence = PropEq.isEquivalence
                  ; reflexive     = λ _ → _
                  ; trans         = λ _ _ → _
                  }
              ; antisym  = antisym
              }
          ; total = total
          }
      ; _≟_  = _≟_
      ; _≤?_ = _≤?_
      }
  }
  where
  antisym : Antisymmetric _≡_ _≤_
  antisym _ _ = refl

decSetoid : DecSetoid _ _
decSetoid = DecTotalOrder.Eq.decSetoid decTotalOrder

poset : Poset _ _ _
poset = DecTotalOrder.poset decTotalOrder


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Universe-sensitive functor and monad instances for the Product type.
------------------------------------------------------------------------

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

open import Algebra

module Data.Product.Categorical.Examples
  {a e b} {A : Monoid a e} {B : Set b} where

open import Level using (Lift; lift; _⊔_)
open import Category.Functor using (RawFunctor)
open import Category.Monad using (RawMonad)
open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Function
import Function.Identity.Categorical as Id
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

------------------------------------------------------------------------
-- Examples

-- Note that these examples are simple unit tests, because the type
-- checker verifies them.

private

  module A = Monoid A

  open import Data.Product.Categorical.Left A.rawMonoid b

  _≈_ : Rel (A.Carrier × Lift a B) (e ⊔ a ⊔ b)
  _≈_ = Pointwise A._≈_ _≡_

  open RawFunctor functor

  -- This type to the right of × needs to be a "lifted" version of (B : Set b)
  -- that lives in the universe (Set (a ⊔ b)).
  fmapIdₗ : (x : A.Carrier × Lift a B) → (id <$> x) ≈ x
  fmapIdₗ x = A.refl , refl

  open RawMonad monad

  -- Now, let's show that "return" is a unit for >>=. We use Lift in exactly
  -- the same way as above. The data (x : B) then needs to be "lifted" to
  -- this new type (Lift B).
  returnUnitL : ∀ {x : B} {f : Lift a B → A.Carrier × Lift a B} →
                ((return (lift x)) >>= f) ≈ f (lift x)
  returnUnitL = A.identityˡ _ , refl

  returnUnitR : {x : A.Carrier × Lift a B} → (x >>= return) ≈ x
  returnUnitR = A.identityʳ _ , refl

  -- And another (limited version of a) monad law...
  bindCompose : ∀ {f g : Lift a B → A.Carrier × Lift a B} →
                {x : A.Carrier × Lift a B} →
                ((x >>= f) >>= g) ≈ (x >>= (λ y → (f y >>= g)))
  bindCompose = A.assoc _ _ _ , refl


text:
module InstanceArgumentsNotFound where

postulate A B : Set
          f : {{a : A}} → B

test : B
test = f


text:
{-# OPTIONS --sized-types #-}

module FormalLanguage {ℓ} where

import      Lvl
open import Sized.Data.List renaming (∅ to [])
open import Lang.Size
open import Data.Boolean
open import Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Data.Boolean.Stmt
open import Functional
open import Relator.Equals
open import Type

-- Definitions:
--   A language is a set of words.
--   A word in a language is a list of valid symbols in the language.
--   A valid symbol in the language is an element in the alphabet of the language.
--   An alphabet of a language is a set.
--   A string is a word.
-- Standard conventions for variable naming in languages:
--   L is a language
--   Σ is an alphabet

Alphabet = Type{ℓ}
Word     = List

-- Language is defined as a trie: (LHS is using the definition of Language, RHS is using the usual "semantics" of languages as sets):
--   For a language L
--   accepts-ε:
--     (accepts-ε(L) = 𝑇) ↔ (ε ∈ L)
--     accepts-ε(L) returns a boolean determining whether the empty word is accepted in the language.
--   suffix-lang:
--     ∀word∀c. (word ∈ suffix-lang(L)(c)) ↔ ((c 𝁼 word) ∈ L)
--     suffix-lang(L)(c) is the language that consists of the rest of the words when a word is starting with c in L.
-- Copied (with modifications) from: http://agda.readthedocs.io/en/v2.5.2/language/sized-types.html (2017-05-13)
-- which links the following paper: "Formal Languages, Formally and Coinductively, Dmitriy Traytel, FSCD (2016)" [https://www21.in.tum.de/~traytel/papers/fscd16-coind_lang/paper.pdf]
-- Example:
--   A language 𝔏 consists of 6 words:
--   𝔏 = {"" , "aa" , "aaa" , "aab" , "aba" , "aaab"}
--   accepts-ε  (𝔏)    = 𝑇
--   suffix-lang(𝔏)(a) = {"a" , "aa" , "ab" , "ba" , "aab"}
--   accepts-ε  (suffix-lang(𝔏)(a))    = 𝐹
--   suffix-lang(suffix-lang(𝔏)(a))(a) = {"" , "a" , "b" , "ab"}
--   suffix-lang(suffix-lang(𝔏)(a))(b) = {"a"}
record Language (Σ : Alphabet) {s : Size} : Type{ℓ} where
  constructor intro
  coinductive
  field
    accepts-ε : Bool
    suffix-lang : ∀{sₛ : <ˢⁱᶻᵉ s} → Σ → Language(Σ){sₛ}

module Oper {Σ} where
  infixl 1003 _∪_
  infixl 1002 _∩_
  infixl 1001 _𝁼_
  infixl 1000 _*

  -- The empty language.
  -- The language that does not include any word at all.
  ∅ : ∀{s} → Language(Σ){s}
  Language.accepts-ε   ∅   = 𝐹
  Language.suffix-lang ∅ _ = ∅

  -- The empty word language.
  -- The language with only the empty word.
  ε : ∀{s} → Language(Σ){s}
  Language.accepts-ε   ε   = 𝑇
  Language.suffix-lang ε _ = ∅

  -- The language of length 1 words that only accepts some symbols of its alphabet
  alphabet-filter : ∀{s} → (Σ → Bool) → Language(Σ){s}
  Language.accepts-ε   (alphabet-filter f)   = 𝐹
  Language.suffix-lang (alphabet-filter f) c = if f(c) then ε else ∅

  -- The single symbol language.
  -- The language consisting of a single word with a single letter
  -- Note: This is only possible when Alphabet has a computably decidable equality relation
  single : ⦃ _ : ComputablyDecidable(_≡_) ⦄ → ∀{s} → Σ → Language(Σ){s}
  single(a) = alphabet-filter(ComputablyDecidable.decide(_≡_) a)

  -- The sublanguage filtered by a decidable predicate.
  filter : ∀{s} → (Word(Σ) → Bool) → Language(Σ){s} → Language(Σ){s}
  Language.accepts-ε   (filter P(𝔏))   = P(List.∅)
  Language.suffix-lang (filter P(𝔏)) c = filter (P ∘ tail) (Language.suffix-lang(𝔏)(c))

  -- The language where every letter in the alphabet is applied to a function.
  unmap : ∀{Σ₂}{s} → (Σ → Σ₂) → Language(Σ₂){s} → Language(Σ){s}
  Language.accepts-ε   (unmap f(𝔏))   = Language.accepts-ε (𝔏)
  Language.suffix-lang (unmap f(𝔏)) c = unmap f(Language.suffix-lang(𝔏)(f(c)))

  -- Union.
  -- The language that includes any words that the two languages have.
  _∪_ : ∀{s} → Language(Σ){s} → Language(Σ){s} → Language(Σ){s}
  Language.accepts-ε   (L₁ ∪ L₂)   = Language.accepts-ε(L₁) || Language.accepts-ε(L₂)
  Language.suffix-lang (L₁ ∪ L₂) c = Language.suffix-lang(L₁)(c) ∪ Language.suffix-lang(L₂)(c)

  -- Intersection.
  -- The language that only includes the words that both languages have in common.
  _∩_ : ∀{s} → Language(Σ){s} → Language(Σ){s} → Language(Σ){s}
  Language.accepts-ε   (L₁ ∩ L₂)   = Language.accepts-ε(L₁) && Language.accepts-ε(L₂)
  Language.suffix-lang (L₁ ∩ L₂) c = Language.suffix-lang(L₁)(c) ∩ Language.suffix-lang(L₂)(c)

  -- Concatenation.
  -- The language that includes words that start with a word the first language and end in a word from the second language.
  _𝁼_ : ∀{s} → Language(Σ){s} → Language(Σ){s} → Language(Σ){s}
  Language.accepts-ε   (L₁ 𝁼 L₂)   = Language.accepts-ε(L₁) && Language.accepts-ε(L₂)
  Language.suffix-lang (L₁ 𝁼 L₂) c =
    if   Language.accepts-ε(L₁)
    then (Language.suffix-lang(L₁)(c) 𝁼 L₂) ∪ Language.suffix-lang(L₂)(c)
    else (Language.suffix-lang(L₁)(c) 𝁼 L₂)

  -- Star/Closure
  -- The language that includes words in any number of concatenations with itself.
  _* : ∀{s} → Language(Σ){s} → Language(Σ){s}
  Language.accepts-ε   (L *)   = 𝑇
  Language.suffix-lang (L *) c = Language.suffix-lang(L)(c) 𝁼 (L *)

  -- Complement
  -- The language that includes all words that a language does not have.
  ∁_ : ∀{s} → Language(Σ){s} → Language(Σ){s}
  Language.accepts-ε   (∁ L)   = !(Language.accepts-ε(L))
  Language.suffix-lang (∁ L) c = ∁(Language.suffix-lang(L)(c))

  -- The universal language.
  -- The language that includes all words in any combination of the alphabet.
  -- The largest language (with most words) with a certain alphabet.
  𝐔 : ∀{s} → Language(Σ){s}
  𝐔 = ∁(∅)

  -- Containment check
  -- Checks whether a word is in the language.
  _∈?_ : ∀{s} → Word{s = s}(Σ) → Language(Σ) → Bool
  _∈?_ []             L = Language.accepts-ε(L)
  _∈?_ (_⊰_ {sₗ} c w) L = _∈?_ {s = sₗ} w (Language.suffix-lang L c)

  -- Containment
  -- The relation of whether a word is in the language or not.
  _∈_ : ∀{s} → Word{s = s}(Σ) → Language(Σ) → Type
  _∈_ {s} a b = IsTrue(_∈?_ {s} a b)

  [_]_∈_ : ∀(s) → Word{s = s}(Σ) → Language(Σ) → Type
  [ s ] a ∈ b = _∈_ {s} a b

  -- Uncontainment
  -- The relation of whether a word is not in the language or not.
  _∉_ : ∀{s} → Word{s = s}(Σ) → Language(Σ) → Type
  _∉_ {s} a b = IsFalse(_∈?_ {s} a b)

  [_]_∉_ : ∀(s) → Word{s = s}(Σ) → Language(Σ) → Type
  [ s ] a ∉ b = _∉_ {s} a b


text:
module Data.Bin.Addition where

  open import Data.List using ([]; _∷_)
  open import Data.Bin using(addBits; addBitLists; addCarryToBitList)
  open import Relation.Binary.PropositionalEquality
  private
    module PropEq = Relation.Binary.PropositionalEquality
  open import Data.Fin using (zero; suc) renaming (toℕ to bitToℕ; _+_ to _+F_)
  open import Data.Fin.Properties using (_+′_)
  open import Data.Digit using (fromDigits)
  open import Data.Product
  import Data.Nat.Properties

  open import Data.Bin.Bijection using (fromℕ-bijection)

  module Solving where

   open Relation.Binary.PropositionalEquality

   open ≡-Reasoning
   open import Algebra
--   open Algebra.Structures
   open CommutativeSemiring Data.Nat.Properties.commutativeSemiring hiding (sym; refl)

   open Data.Product

   open Data.Nat.Properties.SemiringSolver

   lem : ∀ {a b c as bs b' c' r}
          → c' * 2 + b' ≡ c + a + b
          → r ≡ c' + (as + bs)
          → b' + r * 2 ≡ c + (a + as * 2 + (b + bs * 2))
   lem {a} {b} {c} {as} {bs} {b'} {c'} {r} eq1 eq2 =
     begin
      b' + r * 2
       ≡⟨ cong (λ x → b' + x * 2) eq2 ⟩
      b' + (c' + (as + bs))  * 2
       ≡⟨ cong (λ x → b' + x) (proj₂ distrib 2 c' (as + bs)) ⟩
      b' + (c' * 2 + (as + bs) * 2)
       ≡⟨ sym (+-assoc b' (c' * 2) ((as + bs) * 2)) ⟩
      b' + c' * 2 + (as + bs) * 2
       ≡⟨  +-cong (+-comm b' (c' * 2)) refl ⟩
      c' * 2 + b' + (as + bs) * 2
       ≡⟨  +-cong eq1 refl ⟩
      c + a + b + (as + bs) * 2
       ≡⟨ solve 5 (λ a b c as bs →
            c :+ a :+ b :+ (as :+ bs) :* con 2
         := c :+ (a :+ as :* con 2 :+ (b :+ bs :* con 2))
           ) refl a b c as bs ⟩
      c + (a + as * 2 + (b + bs * 2))
     ∎

  open import Data.Nat using () renaming (_+_ to _+_; _*_ to _*_)
  open Data.Bin using (toℕ; toBits)

  addBits-is-addition : ∀ {c a b} → bitToℕ (proj₁ (addBits c a b)) * 2 + bitToℕ (proj₂ (addBits c a b)) ≡ bitToℕ c + bitToℕ a + bitToℕ b
  -- Brute force!!! (LOL)
  addBits-is-addition {zero} {zero} {zero} = refl
  addBits-is-addition {zero} {zero} {suc zero} = refl
  addBits-is-addition {zero} {suc zero} {zero} = refl
  addBits-is-addition {zero} {suc zero} {suc zero} = refl
  addBits-is-addition {suc zero} {zero} {zero} = refl
  addBits-is-addition {suc zero} {zero} {suc zero} = refl
  addBits-is-addition {suc zero} {suc zero} {zero} = refl
  addBits-is-addition {suc zero} {suc zero} {suc zero} = refl
  addBits-is-addition {suc (suc ())}
  addBits-is-addition {_} {suc (suc ())}
  addBits-is-addition {_} {_} {suc (suc ())}

  addCarryToBitLists-is-addition : ∀ c b → fromDigits (addCarryToBitList c b) ≡ bitToℕ c + fromDigits b
  addCarryToBitLists-is-addition zero _ = refl
  addCarryToBitLists-is-addition (suc zero) [] = refl
  addCarryToBitLists-is-addition (suc zero) (zero ∷ t) = refl
  addCarryToBitLists-is-addition (suc zero) (suc zero ∷ t) = cong (λ x → x * 2) (addCarryToBitLists-is-addition (suc zero) t)
  addCarryToBitLists-is-addition (suc (suc ())) _
  addCarryToBitLists-is-addition _ ((suc (suc ())) ∷ _)

  open import Data.Nat.Properties using (isCommutativeSemiring)
  open import Algebra.Structures
     using (module IsCommutativeSemiring;
            module IsCommutativeMonoid)
  open IsCommutativeSemiring isCommutativeSemiring
     using (+-isCommutativeMonoid)
  open IsCommutativeMonoid +-isCommutativeMonoid using (identity; comm) renaming (∙-cong to +-cong)

  addBitLists-is-addition : ∀ c a b → fromDigits (addBitLists c a b) ≡ bitToℕ c + (fromDigits a + fromDigits b)
  addBitLists-is-addition c [] b = addCarryToBitLists-is-addition c b
  addBitLists-is-addition c (a ∷ as) [] = trans (addCarryToBitLists-is-addition c (a ∷ as)) (+-cong {bitToℕ c} refl (sym (proj₂ identity (fromDigits (a ∷ as)))))
  addBitLists-is-addition c (a ∷ as) (b ∷ bs) with addBits c a b | addBits-is-addition {c} {a} {b}
  ... | (c' , b') | abia with addBitLists c' as bs | addBitLists-is-addition c' as bs
  ... | r | ria = Solving.lem {bitToℕ a} {bitToℕ b} {bitToℕ c} {fromDigits as} {fromDigits bs} {bitToℕ b'} {bitToℕ c'} abia ria

  open import Function.Inverse using (Inverse)
  open import Function.Equality
  open import Data.Bin.BitListBijection using () renaming (toℕ⟶ to bits-to-ℕ)
  open import Data.Bin.Bijection using (Bits-inverse-Bin)

  simplify-fromBits-to-ℕ : ∀ a → toℕ (Data.Bin.fromBits a) ≡ bits-to-ℕ ⟨$⟩ a
  simplify-fromBits-to-ℕ a = Π.cong bits-to-ℕ (Inverse.left-inverse-of Bits-inverse-Bin a )

  +-is-addition : ∀ a b → toℕ (Data.Bin._+_ a b) ≡ toℕ a + toℕ b
  +-is-addition a b =
    trans
      (simplify-fromBits-to-ℕ (addBitLists zero (toBits a) (toBits b)))
      (addBitLists-is-addition zero as bs)
      where
    as = toBits a
    bs = toBits b

  import Algebra.Lifting
  open import Data.Nat using (ℕ)
  open import Data.Bin using (Bin; 0#)
  open import Algebra.Structures using (IsCommutativeMonoid)
  private module Lifting = Algebra.Lifting _ _ fromℕ-bijection

  is-commutativeMonoid : IsCommutativeMonoid _≡_ Data.Bin._+_ 0#
  is-commutativeMonoid = lift-isCommutativeMonoid 0 +-isCommutativeMonoid
   where
     open Lifting.WithOp₂ _+_ Data.Bin._+_ +-is-addition

max_stars_repo_name: Rotsor/BinDivMod

max_issues_repo_name: Rotsor/BinDivMod

max_forks_repo_name: Rotsor/BinDivMod