text:
-- Source: https://raw.githubusercontent.com/gallais/potpourri/master/agda/poc/dimensions/dimensions.agda
-- Author: Original by gallais, modified for test suite by P. Hausmann
-- (Later edited by others.)

{-# OPTIONS --guardedness #-}

module dimensions where

open import Data.Nat     as ℕ using (ℕ; NonZero)
open import Data.Nat.LCM
open import Data.Nat.DivMod hiding (_/_)
open import Data.Integer as ℤ using (ℤ ; +_)

open import Data.Unit.Polymorphic using (⊤)
open import Function
open import Relation.Nullary.Decidable

------------------------------------------------
-- DIMENSIONS
-- record { kilogram = x ; meter = y ; second = z }
-- corresponds to the dimension: kg^x * m^y * s^z

module Dimension where

  record dimension : Set where
    field
      kilogram : ℤ
      meter    : ℤ
      second   : ℤ
  open dimension public

  _*_ : (d e : dimension) → dimension
  d * e = record { kilogram = kilogram d ℤ.+ kilogram e
                 ; meter    = meter d    ℤ.+ meter e
                 ; second   = second d   ℤ.+ second e }

  _/_ : (d e : dimension) → dimension
  d / e = record { kilogram = kilogram d ℤ.- kilogram e
                 ; meter    = meter d    ℤ.- meter e
                 ; second   = second d   ℤ.- second e }

open Dimension using (dimension ; kilogram ; meter ; second)

kgram met sec : dimension
kgram = record { kilogram = + 1
               ; meter    = + 0
               ; second   = + 0 }
met   = record { kilogram = + 0
               ; meter    = + 1
               ; second   = + 0 }
sec   = record { kilogram = + 0
               ; meter    = + 0
               ; second   = + 1 }

≠0-mult :
  (m n : ℕ) (hm : NonZero m) (hn : NonZero n) → NonZero (m ℕ.* n)
≠0-mult ℕ.zero    n         () hn
≠0-mult m         0         hm ()
≠0-mult (ℕ.suc m) (ℕ.suc n) hm hn = _

------------------------------------------------
-- UNITS
-- A unit is a dimension together with a coefficient
-- 60 , _ # sec represents a minute (60 seconds)

module Unit where

  infix 1 _,_#_

  data unit : Set where
    _,_#_ : (n : ℕ) (hn : NonZero n) (d : dimension) → unit

  coeff : (u : unit) → ℕ
  coeff (k , _ # _) = k

  coeff≠0 : (u : unit) → NonZero (coeff u)
  coeff≠0 (k , hk # _) = hk

  _*_ : (u v : unit) → unit
  (k , hk # d) * (l , hl # e) =
    ( k ℕ.* l ) , (≠0-mult k l hk hl) # (d Dimension.* e)

  _/_ : (u v : unit)
        ⦃ ≠0 : NonZero (((coeff u) div (coeff v)) ⦃ coeff≠0 v ⦄) ⦄ →
        unit
  _/_ (k , hk # d) (l , hl # e) ⦃ ≠0 ⦄ =
    (k div l) ⦃ hl ⦄ , ≠0 # (d Dimension./ e)

open Unit using (unit ; _,_#_ ; coeff ; coeff≠0)

------------------------------------------------
-- VALUES
-- Finally, values are natural numbers repackaged
-- with a unit

module Values where

  data [_] : (d : unit) → Set where
    ⟨_∶_⟩ : (value : ℕ) (d : unit) → [ d ]

  val : ∀ {d} → [ d ] → ℕ
  val ⟨ m ∶ _ ⟩ = m

  infix 3 _+_
  infix 4 _*_ _/_

  _+_ : ∀ {k hk l hl m hm} {d : dimension} (v₁ : [ k , hk # d ])
        (v₂ : [ l , hl # d ]) → [ m , hm # d ]
  _+_ {k} {hk} {l} {hl} {m} {hm} ⟨ v₁ ∶ ._ ⟩ ⟨ v₂ ∶ ._ ⟩ =
      ⟨ ((k ℕ.* v₁ ℕ.+ l ℕ.* v₂) div m) ⦃ hm ⦄ ∶ _ ⟩

  _:+_ : ∀ {k hk l hl} {d : dimension} (v₁ : [ k , hk # d ])
         (v₂ : [ l , hl # d ]) → [ 1 , _ # d ]
  _:+_ = _+_

  _*_ : ∀ {k hk l hl m hm} {d e : dimension}
        (vd : [ k , hk #  d ]) (ve : [ l , hl # e ]) →
        [ m , hm # (d Dimension.* e) ]
  _*_ {k} {hk} {l} {hl} {m} {hm} ⟨ vd ∶ ._ ⟩ ⟨ ve ∶ ._ ⟩ =
      ⟨ ((k ℕ.* vd ℕ.* l ℕ.* ve) div m) ⦃ hm ⦄ ∶ _ ⟩

  _:*_ : ∀ {k hk l hl} {d e : dimension}
         (vd : [ k , hk #  d ]) (ve : [ l , hl # e ]) →
         [ 1 , _ # (d Dimension.* e) ]
  _:*_ = _*_

  _/_ :  ∀ {k hk l hl m hm} {d e : dimension}
        (vd : [ k , hk #  d ]) (ve : [ l , hl # e ])
        {≠0 : NonZero (val ve)} → [ m , hm # (d Dimension./ e) ]
  _/_ {k} {hk} {l} {hl} {m} {hm} ⟨ vd ∶ ._ ⟩ ⟨ ve ∶ ._ ⟩ {≠0} =
      ⟨ ((k ℕ.* vd) div (l ℕ.* ve ℕ.* m))
          ⦃ ≠0-mult _ _ (≠0-mult _ _ hl ≠0) hm ⦄ ∶ _ ⟩

  ↑ : ∀ {k hk l hl d} → [ k , hk # d ] → [ l , hl # d ]
  ↑ {k} {hk} {l} {hl} ⟨ v ∶ ._ ⟩ = ⟨ ((k ℕ.* v) div l) ⦃ hl ⦄ ∶ _ ⟩

open Values

------------------------------------------------
-- SI PREFIXES
-- They are simply unit-modifying functions.

infix 5 _**_

_**_ : (k : ℕ) {hk : NonZero k} (d : dimension) → unit
_**_ k {hk} d = k , hk # d

centi : (u : unit) {≠0 : NonZero (coeff u div 100)} → unit
centi (k , hk # d) {≠0} = _ , ≠0 # d
deci : (u : unit) {≠0 : NonZero (coeff u div 10)} → unit
deci  (k , hk # d) {≠0} = _ , ≠0 # d
deca hecto kilo : unit → unit
deca  (k , hk # d) = 10   ℕ.* k , ≠0-mult 10   k _ hk # d
hecto (k , hk # d) = 100  ℕ.* k , ≠0-mult 100  k _ hk # d
kilo  (k , hk # d) = 1000 ℕ.* k , ≠0-mult 1000 k _ hk # d

cst : unit
cst =
  let dcst = record { kilogram = + 0
                    ; meter    = + 0
                    ; second   = + 0 }
  in 1 , _ # dcst

infix 3 κ_

κ_ : (n : ℕ) → [ cst ]
κ n = ⟨ n ∶ cst ⟩

------------------------------------------------
-- EXAMPLES

s min hr : unit
s   = 1         ** sec
min = 60        ** sec
hr  = 60 ℕ.* 60 ** sec

m : unit
m = 1 ** met

1s : [ s ]
1s   = ⟨ 1 ∶ s ⟩
1min : [ min ]
1min = ⟨ 1 ∶ min ⟩

1hr 2hr : [ min ]
1hr = ⟨ 60 ∶ min ⟩
2hr = 1hr + 1hr

1min² : [ s Unit.* s ]
1min² = 1min * 1min

60km : [ kilo m ]
60km = ⟨ 60 ∶ kilo m ⟩

60hm : [ hecto m ]
60hm = ⟨ 60 ∶ hecto m ⟩

60hm/min : [ deca m Unit./ s ]
60hm/min = ⟨ 60 ∶ hecto m ⟩ / ⟨ 1 ∶ min ⟩

acc : unit
acc = m Unit./ (s Unit.* s)

spd : unit
spd = m Unit./ s

------------------------------------------------
-- APPLICATION:
-- free fall of a ball with an initial horizontal speed.

record point : Set where
  field
    accx accy : [ acc ]
    vx vy     : [ spd ]
    x y       : [ m   ]
open point public

g : [ acc ]
g = ⟨ 10 ∶ _ ⟩

newton : ∀ (dt : [ s ]) (p : point) → point
newton dt p =
  record { accx = accx p
         ; accy = accy p + g
         ; vx   = vx p   + (accx p :* dt)
         ; vy   = vy p   + (accy p :* dt)
         ; x    = x p    + (vx p   :* dt)
         ; y    = y p    + (vy p   :* dt) }

------------------------------------------------
-- TRACING

-- the initial condition a point is in
base : point
base = record
         { accx = ⟨ 0  ∶ _ ⟩
         ; accy = ⟨ 0  ∶ _ ⟩
         ; vx   = ⟨ 45 ∶ _ ⟩
         ; vy   = ⟨ 0  ∶ _ ⟩
         ; x    = ⟨ 0  ∶ _ ⟩
         ; y    = ⟨ 0  ∶ _ ⟩ }

-- the consecutive steps of its fall
open import Data.Vec     as V using (Vec)

throw : (n : ℕ) (dt : [ s ]) → point → Vec point (ℕ.suc n)
throw  ℕ.zero   dt p = p V.∷ V.[]
throw (ℕ.suc n) dt p = p V.∷ throw n dt (newton dt p)

-- the display function generating the output
open import Data.String     renaming (_++_ to _+s+_)
open import IO
import IO.Primitive
open import Codata.Musical.Colist
open import Data.Nat.Show as Nat
open import Level using (0ℓ)

printPoint : point → IO {0ℓ} ⊤
printPoint p = putStrLn ((Nat.show (val (x p))) +s+ ";" +s+ Nat.show (val (y p)))

main : IO.Primitive.IO ⊤
main = run (Colist.mapM printPoint (Codata.Musical.Colist.fromList trace) >> return _)
  where trace = V.toList $ throw 15 ⟨ 1 ∶ s ⟩ base


text:
{-# OPTIONS --experimental-irrelevance #-}
-- {-# OPTIONS -v tc.univ:100 -v tc.meta:100 #-}
-- {-# OPTIONS -v tc.rec:100 #-}
-- Andreas, 2011-04-27 universe levels can be made irrelevant
-- Ulf 2011-10-03. No they can't. How is that even consistent?
-- Andreas, 2011-10-03. Yes, they can!
--   .(i : Level)(A : Set i)   does not mean that Set i = Set j for all i,j
-- but nl i A = nl j A  for all i,j.
module IrrelevantLevel where

open import Common.Level

postulate
  Lst : .(i : Level)(A : Set i) -> Set i
  nl  : .(i : Level)(A : Set i) -> Lst i A
  cns : .(i : Level)(A : Set i) -> A -> Lst i A -> Lst i A

data List .(i : Level)(A : Set i) : Set i where
  nil  : List i A
  cons : A -> List i A -> List i A

singleton : .{i : Level}{A : Set i}(a : A) -> List i A
singleton a = cons a nil

record Wrap .(i : Level)(A : Set i) : Set i where
  field
    wrap : A

module M .(i : Level)(A : Set i) where

  data Li : Set i where
    ni : Li
    co : A -> Li -> Li

ext: agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Level as Level using (zero)
open import Size
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P
open ≡-Reasoning

open import Data.List using (List; module List; []; _∷_; _++_; length)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product renaming (map to pmap)

open import Relations

-- Sized streams via head/tail.

record Stream {i : Size} (A : Set) : Set where
  coinductive
  constructor _∷_
  field
    hd : A
    tl : ∀ {j : Size< i} → Stream {j} A
open Stream public

-- Shorthand
Str = Stream

tl' : ∀ {A} → Str A → Str A
tl' s = tl s {∞}

-- Constructor
scons : ∀{A} → A → Str A → Str A
hd (scons a s) = a
tl (scons a s) = s

-- | Corecursion
corec : ∀ {X A : Set} → (X → A) → (X → X) → (X → Str A)
hd (corec h s x) = h x
tl (corec h s x) = corec h s (s x)

-- Functoriality.

map : ∀ {i A B} (f : A → B) (s : Stream {i} A) → Stream {i} B
hd (map     f s)     = f (hd s)
tl (map {i} f s) {j} = map {j} f (tl s {j})

-- Derivative
δ : ∀{A} → ℕ → Stream A → Stream A
δ 0       s = s
δ (suc n) s = δ n (tl s)

-- Indexing
_at_ : ∀{A} → Stream A → ℕ → A
s at n = hd (δ n s)

fromStr = _at_

-- | Inverse for at
toStr : ∀ {A} → (ℕ → A) → Str A
hd (toStr f) = f 0
tl (toStr f) = toStr (λ n → f (suc n))

module Bisim (S : Setoid Level.zero Level.zero) where

  infix 2 _∼_

  open Setoid S renaming (Carrier to A; isEquivalence to S-equiv)
  module SE = IsEquivalence S-equiv

  -- Stream equality is bisimilarity
  record _∼_ {i : Size} (s t : Stream A) : Set where
    coinductive
    field
      hd≈ : hd s ≈ hd t
      tl∼ : ∀ {j : Size< i} → _∼_ {j} (tl s) (tl t)
  open _∼_ public

  _∼[_]_ : Stream A → Size → Stream A → Set
  s ∼[ i ] t = _∼_ {i} s t

  s-bisim-refl : ∀ {i} {s : Stream A} → s ∼[ i ] s
  hd≈ s-bisim-refl               = SE.refl
  tl∼ (s-bisim-refl {_} {s}) {j} = s-bisim-refl {j} {tl s}

  s-bisim-sym : ∀ {i} {s t : Stream A} → s ∼[ i ] t → t ∼[ i ] s
  hd≈ (s-bisim-sym             p)     = SE.sym (hd≈ p)
  tl∼ (s-bisim-sym {_} {s} {t} p) {j} =
    s-bisim-sym {j} {tl s} {tl t} (tl∼ p)

  s-bisim-trans : ∀ {i} {r s t : Stream A} →
                  r ∼[ i ] s → s ∼[ i ] t → r ∼[ i ] t
  hd≈ (s-bisim-trans                 p q)     = SE.trans (hd≈ p) (hd≈ q)
  tl∼ (s-bisim-trans {_} {r} {s} {t} p q) {j} =
    s-bisim-trans {j} {tl r} {tl s} {tl t} (tl∼ p) (tl∼ q)

  stream-setoid : Setoid _ _
  stream-setoid = record
    { Carrier = Stream A
    ; _≈_ = _∼_
    ; isEquivalence = record
      { refl  = s-bisim-refl
      ; sym   = s-bisim-sym
      ; trans = s-bisim-trans
      }
    }

  import Relation.Binary.EqReasoning as EqR

  module ∼-Reasoning where
    module _ where
      open EqR (stream-setoid) public
        hiding (_≡⟨_⟩_) renaming (_≈⟨_⟩_ to _∼⟨_⟩_; begin_ to begin_; _∎ to _∎)

  -- | As usual, bisimilarity implies equality at every index.
  bisim→ext-≡ : ∀ {s t : Stream A} → s ∼ t → ∀ {n} → s at n ≈ t at n
  bisim→ext-≡ p {zero}  = hd≈ p
  bisim→ext-≡ p {suc n} = bisim→ext-≡ (tl∼ p) {n}

  -- | Definition of bisimulation
  isBisim : Rel (Str A) Level.zero → Set
  isBisim R =
    (s t : Str A) → R s t → (hd s ≈ hd t) × R (tl s) (tl t)

  -- | Bisimulation proof principle
  ∃-bisim→∼ : ∀ {R} → isBisim R → (s t : Str A) → R s t → s ∼ t
  hd≈ (∃-bisim→∼ R-isBisim s t q) = proj₁ (R-isBisim s t q)
  tl∼ (∃-bisim→∼ R-isBisim s t q) =
    ∃-bisim→∼ R-isBisim (tl s) (tl t) (proj₂ (R-isBisim s t q))

  StrRel : Set₁
  StrRel = Rel (Str A) Level.zero

  -- | Relation transformer that characterises bisimulations
  Φ : Rel (Str A) Level.zero → Rel (Str A) Level.zero
  Φ R s t = (hd s ≈ hd t) × R (tl s) (tl t)

  isBisim' : Rel (Str A) Level.zero → Set
  isBisim' R = R ⇒ Φ R

  isBisim'→isBisim : ∀ {R} → isBisim' R → isBisim R
  isBisim'→isBisim p s t q = p q

  Φ-compat : RelTrans (Str A) → Set₁
  Φ-compat F = Monotone F × (∀ {R} → F (Φ R) ⇒ Φ (F R))

  isBisim-upto : RelTrans (Str A) → Rel (Str A) Level.zero → Set
  isBisim-upto F R = R ⇒ Φ (F R)

  Φ-compat-pres-upto : {F : RelTrans (Str A)} (P : Φ-compat F) {R : StrRel} →
                       isBisim-upto F R → isBisim-upto F (F R)
  Φ-compat-pres-upto (M , P) p = P ∘ (M p)

  iterTrans : RelTrans (Str A) → ℕ → StrRel → StrRel
  iterTrans F zero R = R
  iterTrans F (suc n) R = iterTrans F n (F R)

  -- Closure of up-to technique, which will be the the bisimulation we generate from it
  bisimCls : RelTrans (Str A) → StrRel → StrRel
  bisimCls F R s t = ∃ λ n → iterTrans F n R s t

  clsIsBisim : {F : RelTrans (Str A)} (P : Φ-compat F) {R : StrRel} →
               isBisim-upto F R → isBisim' (bisimCls F R)
  clsIsBisim P p {s} {t} (zero , sRt) =
    (proj₁ (p sRt) , 1 , proj₂ (p sRt))
  clsIsBisim {F} (M , P) {R} p {s} {t} (suc n , inFIter) =
    let
      foo = clsIsBisim (M , P) {F R} (Φ-compat-pres-upto (M , P) p) (n , inFIter)
    in (proj₁ foo , (pmap suc id) (proj₂ foo))

  -- Compatible up-to techniques are sound
  compat-sound : {F : RelTrans (Str A)} (P : Φ-compat F) {R : StrRel} →
                 isBisim-upto F R → (s t : Str A) → R s t → s ∼ t
  compat-sound {F} P {R} p s t sRt =
    ∃-bisim→∼ (isBisim'→isBisim {bisimCls F R} (clsIsBisim P p))
    s t (0 , sRt)

  -- | Useful general up-to technique: the equivalence closure is Φ-compatible.
  equivCls-compat : Φ-compat EquivCls
  equivCls-compat = equivCls-monotone , compat
    where
      compat : {R : StrRel} → EquivCls (Φ R) ⇒ Φ (EquivCls R)
      compat (cls-incl (h≈ , tR)) = (h≈ , cls-incl tR)
      compat cls-refl             = (SE.refl , cls-refl)
      compat {R} (cls-sym p)      =
        let (h≈ , tR) = compat {R} p
        in (SE.sym h≈ , cls-sym tR)
      compat {R} (cls-trans p q) =
        let (hx≈hy , txRty) = compat {R} p
            (hy≈hz , tyRtz) = compat {R} q
        in (SE.trans hx≈hy hy≈hz , cls-trans txRty tyRtz)

-- | Element repetition
repeat : ∀{A} → A → Stream A
hd (repeat a) = a
tl (repeat a) = repeat a

-- Streams and lists.

-- Prepending a list to a stream.

_++ˢ_ : ∀ {A} → List A → Stream A → Stream A
[]       ++ˢ s = s
(a ∷ as) ++ˢ s = a ∷ (as ++ˢ s)

-- Taking an initial segment of a stream.

takeˢ : ∀ {A} (n : ℕ) (s : Stream A) → List A
takeˢ 0       s = []
takeˢ (suc n) s = hd s ∷ takeˢ n (tl s)

_↓_ : ∀ {A} (s : Stream A) (n : ℕ) → List A
s ↓ n = takeˢ n s

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module instances where
open import lib public renaming (return to returnᵢₒ; _>>_ to _>>ᵢₒ_; _>>=_ to _>>=ᵢₒ_)
open import functions public

record functor {ℓ ℓ'} (F : Set ℓ → Set ℓ') : Set (lsuc (ℓ ⊔ ℓ')) where
  infixl 2 _<$>_ _<$_
  field
    fmap : ∀ {A B : Set ℓ} → (A → B) → F A → F B

  {-functor-identity-law :
      ∀ {A} (fa : F A) →
        fmap id fa ≡ fa
    functor-composition-law :
      ∀ {A B C} (f : B → C) (g : A → B) (fa : F A) →
        fmap (f ∘ g) fa ≡ fmap f (fmap g fa)-}

  _<$>_ = fmap

  _<$_ : ∀ {A B : Set ℓ} → A → F B → F A
  a <$ fb = (λ _ → a) <$> fb

open functor ⦃...⦄ public

record applicative {ℓ ℓ'} (F : Set ℓ → Set ℓ') : Set (lsuc (ℓ ⊔ ℓ')) where
  infixl 2 _<*>_ _<*_ _*>_
  field
    pure : ∀ {A : Set ℓ} → A → F A
    _<*>_ : ∀ {A B : Set ℓ} → F (A → B) → F A → F B
    ⦃ functorF ⦄ : functor F

  {-applicative-identity-law :
      ∀ {A} (v : F A) →
        pure id <*> v ≡ v
    applicative-composition-law :
      ∀ {A B C} (u : F (B → C)) (v : F (A → B)) (w : F A) →
        pure _∘_ <*> u <*> v <*> w ≡ u <*> (v <*> w)
    applicative-homomorphism-law :
      ∀ {A B} (f : A → B) (x : A) →
        pure f <*> pure x ≡ pure (f x)
    applicative-interchange-law :
      ∀ {A B} (u : F (A → B)) (y : A) →
        u <*> pure y ≡ pure (_$ y) <*> u-}

  _<*_ : ∀ {A B : Set ℓ} → F A → F B → F A
  fa <* fb = (λ a b → a) <$> fa <*> fb

  _*>_ : ∀ {A B : Set ℓ} → F A → F B → F B
  fa *> fb = (λ a b → b) <$> fa <*> fb

  liftA : ∀ {A B : Set ℓ} → (A → B) → F A → F B
  liftA g fa = pure g <*> fa

  liftA2 : ∀ {A B C : Set ℓ} → (A → B → C) → F A → F B → F C
  liftA2 g fa fb = pure g <*> fa <*> fb

  sequenceA : ∀ {A : Set ℓ} → 𝕃 (F A) → F (𝕃 A)
  sequenceA = foldr (liftA2 _::_) (pure [])

open applicative ⦃...⦄ public

record monad {ℓ ℓ'} (F : Set ℓ → Set ℓ') : Set (lsuc (ℓ ⊔ ℓ')) where
  infixr 2 _>>_ _>>=_ _=<<_ _>=>_ _>>=c_ _>>c_ _>>=?_ _>>=m_ _>>=s_ _>>=e_ _>>≠_ _>≯_ _>>=r_ _>>r_

  field
    return : ∀{A : Set ℓ} → A → F A
    _>>=_ : ∀{A B : Set ℓ} → F A → (A → F B) → F B

  {-monad-left-identity-law :
      ∀ {A B} (a : A) (k : A → F B) →
        return a >>= k ≡ k a
    monad-right-identity-law :
      ∀ {A} (m : F A) →
        m >>= return ≡ m
    monad-associativity-law :
      ∀ {A B C} (m : F A) (k : A → F B) (h : B → F C) →
        m >>= (λ x → k x >>= h) ≡ (m >>= k) >>= h-}

  _>>_ : ∀ {A B : Set ℓ} → F A → F B → F B
  fa >> fb = fa >>= λ _ → fb

  _=<<_ : ∀ {A B : Set ℓ} → (A → F B) → F A → F B
  fab =<< fa = fa >>= fab

  _>=>_ : ∀ {A B C : Set ℓ} → (A → F B) → (B → F C) → (A → F C)
  fab >=> fbc = λ a → fab a >>= fbc

  _>>=c_ : ∀ {A B C : Set ℓ} → F (A × B) → (A → B → F C) → F C
  p >>=c f = p >>= λ {(a , b) → f a b}

  _>>c_ : ∀ {A B : Set ℓ} → F A → F B → F (A × B)
  fa >>c fb = fa >>= λ a → fb >>= λ b → return (a , b)

  _>>=?_ : ∀ {A B : Set ℓ} → maybe (F A) → (maybe A → F B) → F B
  nothing >>=? f = f nothing
  (just a) >>=? f = a >>= (f ∘ just)

  _>>=s_ : ∀ {A B E : Set ℓ} → F (E ⊎ A) → (A → F (E ⊎ B)) → F (E ⊎ B)
  s >>=s f = s >>= λ {(inj₁ e) → return (inj₁ e); (inj₂ a) → f a}

  _>>=e_ : ∀ {A B : Set ℓ} → F (error-t A) → (A → F (error-t B)) → F (error-t B)
  fe? >>=e f = fe? >>= λ {(no-error a) → f a; (yes-error e) → return (yes-error e)}

  _>>=m_ : ∀{A B : Set ℓ} → F (maybe A) → (A → F (maybe B)) → F (maybe B)
  m >>=m f = m >>= λ {(just a) → f a; nothing → return nothing}

  _>>≠_  : ∀{A B : Set ℓ} → F A → (A → F B) → F A
  (f₁ >>≠ f₂) = f₁ >>= λ result → f₂ result >> return result

  _>≯_ : ∀{A B : Set ℓ} → F A → F B → F A
  (f₁ >≯ f₂) = f₁ >>= λ result → f₂ >> return result

  _>>=r_ : ∀{A B : Set ℓ} → F A → (A → B) → F B
  a >>=r f = a >>= (return ∘ f)

  _>>r_ : ∀{A B : Set ℓ} → F A → B → F B
  a >>r b = a >> return b

  _on-fail_>>=m_ : ∀ {A B : Set ℓ} → F (maybe A) → F B → (A → F B) → F B
  fa? on-fail fb >>=m fab = fa? >>= λ {(just a) → fab a; nothing → fb}

  _on-fail_>>=s_ : ∀ {A B E : Set ℓ} → F (E ⊎ A) → (E → F B) → (A → F B) → F B
  fa+e on-fail feb >>=s fab = fa+e >>= λ {(inj₁ e) → feb e; (inj₂ a) → fab a}

  return2 : ∀ {A B : Set ℓ} → A → B → F (A × B)
  return2 a b = return (a , b)

  foldrM : ∀ {A B} → (A → F B → F B) → F B → 𝕃 (F A) → F B
  foldrM c n [] = n
  foldrM c n (fa :: fas) = fa >>= λ a → c a (foldrM c n fas)

  foldlM : ∀ {A B} → (A → F B → F B) → F B → 𝕃 (F A) → F B
  foldlM c n [] = n
  foldlM c n (fa :: fas) = fa >>= λ a → foldlM c (c a n) fas

  forM_init_use_ : ∀ {A B} → 𝕃 (F A) → F B → (A → F B → F B) → F B
  forM as init b use f = foldrM f b as

open monad ⦃...⦄ public

join : ∀ {ℓ}{F : Set ℓ → Set ℓ}{A : Set ℓ} ⦃ _ : monad F ⦄ → F (F A) → F A
join ffa = ffa >>= id

infixr 2 _>>∘_
_>>∘_ : ∀{ℓ}{F : Set ℓ → Set ℓ}{A B : Set ℓ} ⦃ _ : monad F ⦄ → F A → F (A → F B) → F B
a >>∘ f = a >>= λ a → f >>= λ f → f a

--========== Id ==========--
-- Using "id" itself causes Agda to hang when resolving instances, I suspect due
-- to something like endlessly embedding (id (id (id (...)))). So instead we must
-- use a "newtype" for id.

record Id (A : Set) : Set where
  constructor id-in
  field id-out : A
open Id public

instance
  id-functor : functor Id
  id-applicative : applicative Id
  id-monad : monad Id

  fmap ⦃ id-functor ⦄ f = id-in ∘ (f ∘ id-out)

  pure ⦃ id-applicative ⦄ = id-in
  _<*>_ ⦃ id-applicative ⦄ fab fa = id-in (id-out fab (id-out fa))

  return ⦃ id-monad ⦄ = id-in
  _>>=_ ⦃ id-monad ⦄ a f = f (id-out a)

--========== IO ==========--

instance
  IO-functor : functor IO
  IO-applicative : applicative IO
  IO-monad : monad IO

{-
postulate
  IO-functor-identity-law :
    ∀ {A} →
      fmap ⦃ IO-functor ⦄ {A} id ≡ id
  IO-functor-composition-law :
    ∀ {A B C} (f : B → C) (g : A → B) →
      fmap (f ∘ g) ≡ fmap f ∘ fmap g

  IO-applicative-identity-law :
    ∀ {A} (v : IO A) →
      pure ⦃ IO-applicative ⦄ id <*> v ≡ v
  IO-applicative-composition-law :
    ∀ {A B C} (u : IO (B → C)) (v : IO (A → B)) (w : IO A) →
      pure ⦃ IO-applicative ⦄ _∘_ <*> u <*> v <*> w ≡ u <*> (v <*> w)
  IO-applicative-homomorphism-law :
    ∀ {A B} (f : A → B) (x : A) →
      pure ⦃ IO-applicative ⦄ f <*> pure x ≡ pure (f x)
  IO-applicative-interchange-law :
    ∀ {A B} (u : IO (A → B)) (y : A) →
      u <*> pure y ≡ pure ⦃ IO-applicative ⦄ (_$ y) <*> u

  IO-monad-left-identity-law :
    ∀ {A B} (a : A) (k : A → IO B) →
      (return a >>= k) ≡ k a
  IO-monad-right-identity-law :
    ∀ {A} (m : IO A) →
      (m >>= return) ≡ m
  IO-monad-associativity-law :
    ∀ {A B C} (m : IO A) (k : A → IO B) (h : B → IO C) →
      (m >>= (λ x → k x >>= h)) ≡ ((m >>= k) >>= h)
-}

  fmap ⦃ IO-functor ⦄ g fa = fa >>=ᵢₒ λ a → returnᵢₒ (g a)

  pure ⦃ IO-applicative ⦄ = returnᵢₒ
  _<*>_ ⦃ IO-applicative ⦄ fab fa = fab >>=ᵢₒ λ ab → fa >>=ᵢₒ λ a → returnᵢₒ (ab a)

  return ⦃ IO-monad ⦄ = returnᵢₒ
  _>>=_ ⦃ IO-monad ⦄ = _>>=ᵢₒ_

--========== ⊎ ==========--

instance
  sum-functor : ∀ {ℓ ℓ'} {E : Set ℓ} → functor {ℓ'} {ℓ ⊔ ℓ'} (E ⊎_)
  sum-applicative : ∀ {ℓ ℓ'} {E : Set ℓ} → applicative {ℓ'} {ℓ ⊔ ℓ'} (E ⊎_)
  sum-monad : ∀ {ℓ ℓ'} {E : Set ℓ} → monad {ℓ'} {ℓ ⊔ ℓ'} (E ⊎_)

  fmap ⦃ sum-functor ⦄ f (inj₁ e) = inj₁ e
  fmap ⦃ sum-functor ⦄ f (inj₂ a) = inj₂ (f a)

  pure ⦃ sum-applicative ⦄ = inj₂
  _<*>_ ⦃ sum-applicative ⦄ sf sa =
    sf >>= λ f →
    sa >>= λ a →
    return (f a)

  return ⦃ sum-monad ⦄ = inj₂
  _>>=_ ⦃ sum-monad ⦄ (inj₁ e) f = inj₁ e
  _>>=_ ⦃ sum-monad ⦄ (inj₂ a) f = f a

--========== maybe ==========--

instance
  maybe-functor : ∀ {ℓ} → functor {ℓ} maybe
  maybe-applicative : ∀ {ℓ} → applicative {ℓ} maybe
  maybe-monad : ∀ {ℓ} → monad {ℓ} maybe

  fmap ⦃ maybe-functor ⦄ = maybe-map

  pure ⦃ maybe-applicative ⦄ = just
  _<*>_ ⦃ maybe-applicative ⦄ f? a? =
    f? ≫=maybe λ f → a? ≫=maybe (just ∘ f)

  return ⦃ maybe-monad ⦄ = just
  _>>=_ ⦃ maybe-monad ⦄ = _≫=maybe_

--========== 𝕃 ==========--

instance
  list-functor : ∀ {ℓ} → functor {ℓ} 𝕃
  list-applicative : ∀ {ℓ} → applicative {ℓ} 𝕃
  list-monad : ∀ {ℓ} → monad {ℓ} 𝕃

  fmap ⦃ list-functor ⦄ = map

  pure ⦃ list-applicative ⦄ = [_]
  _<*>_ ⦃ list-applicative ⦄ fs as = map (λ {(f , a) → f a}) (zip fs as)

  return ⦃ list-monad ⦄ = [_]
  _>>=_ ⦃ list-monad ⦄ as f = concat (map f as)

max_stars_repo_name: zmthy/cedille

max_issues_repo_name: zmthy/cedille

max_forks_repo_name: zmthy/cedille


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

open import Relation.Binary using (Rel; Setoid; IsEquivalence)
module Structures
  {a ℓ} {A : Set a}  -- The underlying set
  (_≈_ : Rel A ℓ)    -- The underlying equality relation
  where

open import Algebra.Core
open import Level using (_⊔_)
open import Data.Product using (_,_; proj₁; proj₂)
open import Algebra.Definitions _≈_
open import Algebra.Structures _≈_
open import Definitions _≈_

record IsInverseSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isSemigroup     : IsSemigroup ∙
    pseudoInverse   : PseudoInverse ∙

  open IsSemigroup isSemigroup public

record IsRng (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ) where
  field
    +-isAbelianGroup : IsAbelianGroup + 0# -_
    *-isSemigroup    : IsSemigroup *
    distrib          : * DistributesOver +
    zero             : Zero 0# *

  open IsAbelianGroup +-isAbelianGroup public
    renaming
    ( assoc                   to +-assoc
    ; ∙-cong                  to +-cong
    ; ∙-congˡ                 to +-congˡ
    ; ∙-congʳ                 to +-congʳ
    ; identity                to +-identity
    ; identityˡ               to +-identityˡ
    ; identityʳ               to +-identityʳ
    ; inverse                 to -‿inverse
    ; inverseˡ                to -‿inverseˡ
    ; inverseʳ                to -‿inverseʳ
    ; ⁻¹-cong                 to -‿cong
    ; comm                    to +-comm
    ; isMagma                 to +-isMagma
    ; isSemigroup             to +-isSemigroup
    ; isMonoid                to +-isMonoid
    ; isUnitalMagma           to +-isUnitalMagma
    ; isCommutativeMagma      to +-isCommutativeMagma
    ; isCommutativeMonoid     to +-isCommutativeMonoid
    ; isCommutativeSemigroup  to +-isCommutativeSemigroup
    ; isInvertibleMagma       to +-isInvertibleMagma
    ; isInvertibleUnitalMagma to +-isInvertibleUnitalMagma
    ; isGroup                 to +-isGroup
    )

  open IsSemigroup *-isSemigroup public
    using ()
    renaming
    ( assoc    to *-assoc
    ; ∙-cong   to *-cong
    ; ∙-congˡ  to *-congˡ
    ; ∙-congʳ  to *-congʳ
    ; isMagma  to *-isMagma
    )

record IsNonAssociativeRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    +-isAbelianGroup : IsAbelianGroup + 0# -_
    *-isUnitalMagma  : IsUnitalMagma * 1#
    distrib          : * DistributesOver +
    zero             : Zero 0# *

  open IsAbelianGroup +-isAbelianGroup public
    renaming
    ( assoc                   to +-assoc
    ; ∙-cong                  to +-cong
    ; ∙-congˡ                 to +-congˡ
    ; ∙-congʳ                 to +-congʳ
    ; identity                to +-identity
    ; identityˡ               to +-identityˡ
    ; identityʳ               to +-identityʳ
    ; inverse                 to -‿inverse
    ; inverseˡ                to -‿inverseˡ
    ; inverseʳ                to -‿inverseʳ
    ; ⁻¹-cong                 to -‿cong
    ; comm                    to +-comm
    ; isMagma                 to +-isMagma
    ; isSemigroup             to +-isSemigroup
    ; isMonoid                to +-isMonoid
    ; isUnitalMagma           to +-isUnitalMagma
    ; isCommutativeMagma      to +-isCommutativeMagma
    ; isCommutativeMonoid     to +-isCommutativeMonoid
    ; isCommutativeSemigroup  to +-isCommutativeSemigroup
    ; isInvertibleMagma       to +-isInvertibleMagma
    ; isInvertibleUnitalMagma to +-isInvertibleUnitalMagma
    ; isGroup                 to +-isGroup
    )
  open IsUnitalMagma *-isUnitalMagma public
    using ()
    renaming
    ( ∙-cong   to *-cong
    ; ∙-congˡ  to *-congˡ
    ; ∙-congʳ  to *-congʳ
    ; isMagma  to *-isMagma
    )


text:
------------------------------------------------------------------------
-- Code related to the paper "Logical properties of a modality for
-- erasure"
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

-- Note that the code does not follow the paper exactly. For instance,
-- some definitions use bijections (functions with quasi-inverses)
-- instead of equivalences. Some other differences are mentioned
-- below.

-- This file is not checked using --safe, because some parts use
-- --cubical, and some parts use --with-K. However, all files
-- imported below use --safe.

{-# OPTIONS --cubical --with-K #-}

module README.Erased where

import Agda.Builtin.Equality
import Agda.Builtin.Cubical.Id
import Agda.Builtin.Cubical.Path

import Embedding
import Equality
import Equality.Id
import Equality.Instances-related
import Equality.Path
import Equality.Propositional
import Equivalence
import Erased
import Erased.Cubical
import Erased.With-K
import Function-universe
import H-level
import Nat.Wrapper
import Nat.Wrapper.Cubical
import Prelude
import Queue.Truncated
import Quotient

------------------------------------------------------------------------
-- 3: Erased

-- Erased.

Erased = Erased.Erased

------------------------------------------------------------------------
-- 3.1: Erased is a monad

-- Bind.

bind = Erased._>>=′_

-- Erased is a monad.

erased-monad = Erased.monad

-- Lemma 3.

Lemma-3 = Erased.Erased-Erased↔Erased

------------------------------------------------------------------------
-- 3.2: The relationship between @0 and Erased

-- Lemma 4 and Lemma 5.

Lemmas-4-and-5 = Erased.Π-Erased≃Π0[]

-- The equality type family, defined as an inductive family.

Equality-defined-as-an-inductive-family = Agda.Builtin.Equality._≡_

-- Cubical Agda paths.

Path = Agda.Builtin.Cubical.Path._≡_

-- The Cubical Agda identity type family.

Id = Agda.Builtin.Cubical.Id.Id

-- The code uses an axiomatisation of "equality with J". The
-- axiomatisation is a little convoluted in order to support using
-- equality at all universe levels. Furthermore the axiomatisation
-- supports choosing specific definitions for other functions, like
-- cong, to make the code more usable when it is instantiated with
-- Cubical Agda paths (for which the canonical definition of cong
-- computes in a different way than typical definitions obtained
-- using J).

-- Equality and reflexivity.

≡-refl = Equality.Reflexive-relation

-- The J rule and its computation rule.

J-J-refl = Equality.Equality-with-J₀

-- Extended variants of the two definitions above.

Equivalence-relation⁺ = Equality.Equivalence-relation⁺
Equality-with-J       = Equality.Equality-with-J

-- To see how the code is axiomatised, see the module header of, say,
-- Erased.

module See-the-module-header-of = Erased

-- The equality type family defined as an inductive family, Cubical
-- Agda paths and the Cubical Agda identity type family can all be
-- used to instantiate the axioms.

Equality-with-J-for-equality-defined-as-an-inductive-family =
  Equality.Propositional.equality-with-J
Equality-with-J-for-Path = Equality.Path.equality-with-J
Equality-with-J-for-Id   = Equality.Id.equality-with-J

-- Lemma 7 in Cubical Agda.

Lemma-7-cubical = Erased.Cubical.Π-Erased≃Π0[]

-- Lemma 7 in traditional Agda.

Lemma-7-traditional = Erased.With-K.Π-Erased≃Π0[]

------------------------------------------------------------------------
-- 3.3: Erased commutes

-- Some lemmas.

Lemma-8  = Erased.Erased-⊤↔⊤
Lemma-9  = Erased.Erased-⊥↔⊥
Lemma-10 = Erased.Erased-Π↔Π
Lemma-11 = Erased.Erased-Π↔Π-Erased
Lemma-12 = Erased.Erased-Σ↔Σ

-- W-types.

W = Prelude.W

-- Lemma 14 (Erased commutes with W-types up to logical equivalence).

Lemma-14 = Erased.Erased-W⇔W

-- Erased commutes with W-types, assuming extensionality for functions
-- and []-cong.
--
-- The code uses a universe of "function formers" which makes it
-- possible to prove a single statement that can be instantiated both
-- as a logical equivalence that does not rely on extensionality, as
-- well as an equivalence that does rely on extensionality (and in
-- other ways). This lemma, and several others, are stated in that
-- way.

Lemma-14′ = Erased.Erased-W↔W

------------------------------------------------------------------------
-- 3.4: The []-cong property

-- []-cong, proved in traditional Agda.

[]-cong-traditional = Erased.With-K.[]-cong

-- []-cong, proved in Cubical Agda for paths.

[]-cong-cubical-paths = Erased.Cubical.[]-cong-Path

-- Every family of equality types satisfying the axiomatisation
-- discussed above is in pointwise bijective correspondence with every
-- other, with the bijections mapping reflexivity to reflexivity.

Families-equivalent =
  Equality.Instances-related.all-equality-types-isomorphic

-- []-cong, proved in Cubical Agda for an arbitrary equality type
-- family satisfying the axiomatisation discussed above.

[]-cong-cubical = Erased.Cubical.[]-cong

-- Lemmas 17 and 18 in traditional Agda.

Lemma-17-traditional = Erased.With-K.[]-cong-equivalence
Lemma-18-traditional = Erased.With-K.[]-cong-[refl]

-- Lemmas 17 and 18 in Cubical Agda, with paths.

Lemma-17-cubical-paths = Erased.Cubical.[]-cong-Path-equivalence
Lemma-18-cubical-paths = Erased.Cubical.[]-cong-Path-[refl]

-- Lemmas 17 and 18 in Cubical Agda, with an arbitrary family of
-- equality types satisfying the axiomatisation discussed above.

Lemma-17-cubical = Erased.Cubical.[]-cong-equivalence
Lemma-18-cubical = Erased.Cubical.[]-cong-[refl]

------------------------------------------------------------------------
-- 3.5: H-levels

-- H-level, For-iterated-equality and Contractible.

H-level               = H-level.H-level′
For-iterated-equality = H-level.For-iterated-equality
Contractible          = Equality.Reflexive-relation′.Contractible

-- Sometimes the code uses the following definition of h-levels
-- instead of the one used in the paper.

Other-definition-of-h-levels = H-level.H-level

-- The two definitions are pointwise logically equivalent, and
-- pointwise equivalent if equality is extensional for functions.

H-level≃H-level′ = Function-universe.H-level↔H-level′

-- There is a single statement for Lemmas 22 and 23.

Lemmas-22-and-23 = Erased.Erased-H-level′↔H-level′

------------------------------------------------------------------------
-- 3.6: Erased is a modality

-- Some lemmas.

Lemma-24 = Erased.uniquely-eliminating-modality
Lemma-25 = Erased.lex-modality

-- The map function.

map = Erased.map

-- Erased is a Σ-closed reflective subuniverse.

Σ-closed-reflective-subuniverse =
  Erased.Erased-Σ-closed-reflective-subuniverse

-- Another lemma.

Lemma-27 = Erased.Erased-connected↔Erased-Is-equivalence

------------------------------------------------------------------------
-- 3.7: Is [_] an embedding?

-- The function cong is unique up to pointwise equality if it is
-- required to map the canonical proof of reflexivity to the canonical
-- proof of reflexivity.

cong-canonical =
  Equality.Derived-definitions-and-properties.cong-canonical

-- Is-embedding.

Is-embedding = Embedding.Is-embedding

-- Embeddings are injective.

embeddings-are-injective = Embedding.injective

-- Some lemmas.

Lemma-29 = Erased.Is-proposition→Is-embedding-[]
Lemma-30 = Erased.With-K.Injective-[]
Lemma-31 = Erased.With-K.Is-embedding-[]
Lemma-32 = Erased.With-K.Is-proposition-Erased→Is-proposition

------------------------------------------------------------------------
-- 3.8: More commutation properties

-- There is a single statement for Lemmas 33–38 (and more).

Lemmas-33-to-38 = Erased.Erased-↝↔↝

-- There is also a single statement for the variants of Lemmas 33–38,
-- stated as logical equivalences instead of equivalences, that can be
-- proved without using extensionality.

Lemmas-33-to-38-with-⇔ = Erased.Erased-↝↝↝

-- Some lemmas.

Lemma-39 = Erased.Erased-cong-≃
Lemma-40 = Erased.Erased-Is-equivalence↔Is-equivalence

-- A generalisation of Lemma 41.

Lemma-41 = Function-universe.Σ-cong

-- More lemmas.

Lemma-42 = Erased.Erased-Split-surjective↔Split-surjective
Lemma-43 = Erased.Erased-Has-quasi-inverse↔Has-quasi-inverse
Lemma-44 = Erased.Erased-Injective↔Injective
Lemma-45 = Erased.Erased-Is-embedding↔Is-embedding
Lemma-46 = Erased.map-cong≡cong-map

-- There is a single statement for Lemmas 47–52 (and more).

Lemmas-47-to-52 = Erased.Erased-cong

-- The map function is functorial.

map-id = Erased.map-id
map-∘  = Erased.map-∘

-- All preservation lemmas (47–52) map identity to identity (assuming
-- extensionality, except for logical equivalences).

Erased-cong-id = Erased.Erased-cong-id

-- All preservation lemmas (47–52) commute with composition (assuming
-- extensionality, except for logical equivalences).

Erased-cong-∘ = Erased.Erased-cong-∘

------------------------------------------------------------------------
-- 4.1: Stable types

-- Stable.

Stable = Erased.Stable

-- Some lemmas.

Lemma-54 = Erased.¬¬-stable→Stable
Lemma-55 = Erased.Erased→¬¬
Lemma-56 = Erased.Dec→Stable

------------------------------------------------------------------------
-- 4.2: Very stable types

-- Very-stable.

Very-stable = Erased.Very-stable

-- A generalisation of Very-stable′.

Very-stable′ = Erased.Stable-[_]

-- Very stable types are stable (and Very-stable A implies
-- Very-stable′ A, and more).

Very-stable→Stable = Erased.Very-stable→Stable

-- [_] is an embedding for very stable types.

Very-stable→Is-embedding-[] = Erased.Very-stable→Is-embedding-[]

-- Some lemmas.

Lemma-59 = Erased.Stable→Left-inverse→Very-stable
Lemma-60 = Erased.Stable-proposition→Very-stable
Lemma-61 = Erased.Very-stable-Erased

-- It is not the case that every very stable type is a proposition.

¬-Very-stable→Is-proposition = Erased.¬-Very-stable→Is-proposition

-- More lemmas.

Lemma-62 = Erased.Very-stable-∃-Very-stable
Lemma-63 = Erased.Stable-∃-Very-stable

------------------------------------------------------------------------
-- 4.3: Stability for equality types

-- Stable-≡ and Very-stable-≡.

Stable-≡      = Erased.Stable-≡
Very-stable-≡ = Erased.Very-stable-≡

-- Some lemmas.

Lemma-66 = Erased.Stable→H-level-suc→Very-stable
Lemma-67 = Erased.Decidable-equality→Very-stable-≡
Lemma-68 = Erased.H-level→Very-stable

-- Lemmas 69 and 70, stated both as logical equivalences, and as
-- equivalences depending on extensionality.

Lemma-69 = Erased.Stable-≡↔Injective-[]
Lemma-70 = Erased.Very-stable-≡↔Is-embedding-[]

-- Equality is always very stable in traditional Agda.

Very-stable-≡-trivial = Erased.With-K.Very-stable-≡-trivial

------------------------------------------------------------------------
-- 4.4: Map-like functions

-- Lemma 71.

Lemma-71 = Erased.Stable-map-⇔

-- There is a single statement for Lemmas 72 and 73.

Lemmas-72-and-73 = Erased.Very-stable-cong

-- Lemma 74.

Lemma-74 = Erased.Very-stable-Erased↝Erased

-- Lemma 74, with Stable instead of Very-stable, and no assumption of
-- extensionality.

Lemma-74-Stable = Erased.Stable-Erased↝Erased

------------------------------------------------------------------------
-- 4.5: Closure properties

-- Lots of lemmas.

Lemmas-75-and-76 = Erased.Very-stable→Very-stable-≡
Lemma-77         = Erased.Very-stable-⊤
Lemma-78         = Erased.Very-stable-⊥
Lemma-79         = Erased.Stable-Π
Lemma-80         = Erased.Very-stable-Π
Lemma-81         = Erased.Very-stable-Stable-Σ
Lemma-82         = Erased.Very-stable-Σ
Lemma-83         = Erased.Stable-×
Lemma-84         = Erased.Very-stable-×
Lemma-85         = Erased.Very-stable-W
Lemmas-86-and-87 = Erased.Stable-H-level′
Lemmas-88-and-89 = Erased.Very-stable-H-level′
Lemma-90         = Erased.Stable-≡-⊎
Lemma-91         = Erased.Very-stable-≡-⊎
Lemma-92         = Erased.Stable-≡-List
Lemma-93         = Erased.Very-stable-≡-List
Lemma-94         = Quotient.Very-stable-≡-/

------------------------------------------------------------------------
-- 4.6: []‐cong can be proved using extensionality

-- The proof has been changed. Lemmas 95 and 97 have been removed.

-- A lemma.

Lemma-96 = Equivalence.≃-≡

-- []-cong, proved using extensionality, along with proofs showing
-- that it is an equivalence and that it satisfies the computation
-- rule of []-cong.

Extensionality→[]-cong = Erased.Extensionality→[]-cong-axiomatisation

------------------------------------------------------------------------
-- 5.1: Singleton types with erased equality proofs

-- Some lemmas.

Lemma-99  = Erased.erased-singleton-contractible
Lemma-100 = Erased.erased-singleton-with-erased-center-propositional

-- The generalisation of Lemma 82 used in the proof of Lemma 100.

Lemma-82-generalised = Erased.Very-stable-Σⁿ

-- Another lemma.

Lemma-101 = Erased.Σ-Erased-Erased-singleton↔

------------------------------------------------------------------------
-- 5.2: Efficient natural numbers

-- An implementation of natural numbers as lists of bits with the
-- least significant bit first and an erased invariant that ensures
-- that there are no trailing zeros.

import Nat.Binary

-- Nat-[_].

Nat-[_] = Nat.Wrapper.Nat-[_]

-- A lemma.

Lemma-103 = Nat.Wrapper.[]-cong.Nat-[]-propositional

-- Nat.

Nat = Nat.Wrapper.Nat

-- ⌊_⌋.

@0 ⌊_⌋ : _
⌊_⌋ = Nat.Wrapper.⌊_⌋

-- Another lemma.

Lemma-106 = Nat.Wrapper.[]-cong.≡-for-indices↔≡

------------------------------------------------------------------------
-- 5.2.1: Arithmetic

-- The functions unary-[] and unary.

unary-[] = Nat.Wrapper.unary-[]
unary    = Nat.Wrapper.unary

-- Similar functions for arbitrary arities.

n-ary-[] = Nat.Wrapper.n-ary-[]
n-ary    = Nat.Wrapper.n-ary

------------------------------------------------------------------------
-- 5.2.2: Converting Nat to ℕ

-- Some lemmas.

Lemma-109 = Nat.Wrapper.Nat-[]↔Σℕ
Lemma-110 = Nat.Wrapper.[]-cong.Nat↔ℕ

-- The function Nat→ℕ.

Nat→ℕ = Nat.Wrapper.Nat→ℕ

-- Some lemmas.

@0 Lemma-111 : _
Lemma-111 = Nat.Wrapper.≡⌊⌋
Lemma-112 = Nat.Wrapper.unary-correct

-- A variant of Lemma 112 for n-ary.

Lemma-112-for-n-ary = Nat.Wrapper.n-ary-correct

------------------------------------------------------------------------
-- 5.2.3: Decidable equality

-- Some lemmas.

Lemma-113 = Nat.Wrapper.Operations-for-Nat._≟_
Lemma-114 = Nat.Wrapper.Operations-for-Nat-[]._≟_

------------------------------------------------------------------------
-- 5.3: Queues

-- The implementation of queues (parametrised by an underlying queue
-- implementation).

module Queue = Queue.Truncated

-- The functions enqueue and dequeue.

enqueue = Queue.Truncated.Non-indexed.enqueue
dequeue = Queue.Truncated.Non-indexed.dequeue

------------------------------------------------------------------------
-- 6: Discussion and related work

-- Nat-[_]′.

Nat-[_]′ = Nat.Wrapper.Cubical.Nat-[_]′

-- An alternative implementation of Nat.

Alternative-Nat = Nat.Wrapper.Cubical.Nat-with-∥∥

-- The alternative implementation of Nat is isomorphic to the unit
-- type.

Alternative-Nat-isomorphic-to-⊤ = Nat.Wrapper.Cubical.Nat-with-∥∥↔⊤

-- The alternative implementation of Nat is not isomorphic to the
-- natural numbers.

Alternative-Nat-not-isomorphic-to-ℕ =
  Nat.Wrapper.Cubical.¬-Nat-with-∥∥↔ℕ

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Prelude.Nat where

open import Prelude.Bool

data Nat : Set where
  Z : Nat
  S : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}

infixl 30 _+_

_+_ : Nat -> Nat -> Nat
Z   + m = m
S n + m = S (n + m)

{-# BUILTIN NATPLUS _+_ #-}

_*_ : Nat -> Nat -> Nat
Z   * m = Z
S n * m = (n * m) + m

{-# BUILTIN NATTIMES _*_ #-}

_-_ : Nat -> Nat -> Nat
n     - Z     = n
(S n) - (S m) = n - m
Z     - _     = Z

{-# BUILTIN NATMINUS _-_ #-}

_<_ : Nat -> Nat -> Bool
_   < Z   = false
Z   < S _ = true
S n < S m = n < m

-- {-# BUILTIN NATLESS _<_ #-}

Nid : Nat -> Bool -> Bool
Nid Z     true  = true
Nid Z     false = false
Nid (S n) m     =  (Nid n ( m))

-- {-# BUILTIN NATEQUALS __ #-}


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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Functions.Definition
open import Setoids.Setoids
open import Setoids.Subset
open import Graphs.Definition
open import Sets.FinSet.Definition
open import Sets.FinSet.Lemmas
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Sets.EquivalenceRelations
open import Graphs.PathGraph

module Graphs.CycleGraph where

CycleGraph : (n : ℕ) → .(2 <N n) → Graph _ (reflSetoid (FinSet n))
Graph._<->_ (CycleGraph n _) x y = ((toNat x ≡ succ (toNat y)) || (toNat y ≡ succ (toNat x))) || (((toNat x ≡ 0) && (toNat y ≡ n)) || ((toNat y ≡ 0) && (toNat x ≡ n)))
Graph.noSelfRelation (CycleGraph n _) y (inl (inl x)) = nNotSucc x
Graph.noSelfRelation (CycleGraph n _) y (inl (inr x)) = nNotSucc x
Graph.noSelfRelation (CycleGraph (succ n) _) y (inr (inl (fst ,, snd))) = naughtE (transitivity (equalityCommutative fst) snd)
Graph.noSelfRelation (CycleGraph (succ n) _) y (inr (inr (fst ,, snd))) = naughtE (transitivity (equalityCommutative fst) snd)
Graph.symmetric (CycleGraph n _) (inl (inl x)) = inl (inr x)
Graph.symmetric (CycleGraph n _) (inl (inr x)) = inl (inl x)
Graph.symmetric (CycleGraph n _) (inr (inl x)) = inr (inr x)
Graph.symmetric (CycleGraph n _) (inr (inr x)) = inr (inl x)
Graph.wellDefined (CycleGraph n _) refl refl i = i


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

module Data.Fin.Indexed where

open import Data.Fin.Indexed.Base public

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --copatterns #-}

open import Common.Nat
open import Common.IO
open import Common.Unit

record Test : Set where
  field
    a b c : Nat

f : Test -> Nat
f r = a + b + c
  where open Test r

open Test

r1 : Test
a r1 = 100
b r1 = 120
c r1 = 140

r2 : Test
c r2 = 400
a r2 = 200
b r2 = 300

g : Nat
g = f r1 + a m + b m + c m
  where m = r2

main : IO Unit
main = printNat g

-- Expected Output: 1260

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Lists parameterised on things in Set₁
------------------------------------------------------------------------

-- I want universe polymorphism.

module Data.List1 where

open import Data.List as List using (List; []; _∷_)
open import Data.Nat

infixr 5 _∷_ _++_

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

_++_ : ∀ {a} → List₁ a → List₁ a → List₁ a
[]       ++ bs = bs
(a ∷ as) ++ bs = a ∷ (as ++ bs)

map₀₁ : ∀ {a b} → (a → b) → List a → List₁ b
map₀₁ f []       = []
map₀₁ f (x ∷ xs) = f x ∷ map₀₁ f xs

map₁₁ : ∀ {a b} → (a → b) → List₁ a → List₁ b
map₁₁ f []       = []
map₁₁ f (x ∷ xs) = f x ∷ map₁₁ f xs

replicate : ∀ {a} → (n : ℕ) → a → List₁ a
replicate zero    x = []
replicate (suc n) x = x ∷ replicate n x

foldr₁₀ : {a : Set₁} {b : Set} → (a → b → b) → b → List₁ a → b
foldr₁₀ c n []       = n
foldr₁₀ c n (x ∷ xs) = c x (foldr₁₀ c n xs)

foldr₁₁ : {a b : Set₁} → (a → b → b) → b → List₁ a → b
foldr₁₁ c n []       = n
foldr₁₁ c n (x ∷ xs) = c x (foldr₁₁ c n xs)

length : ∀ {A} → List₁ A → ℕ
length []       = zero
length (x ∷ xs) = suc (length xs)

max_issues_repo_name: larrytheliquid/Lemmachine


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

module Categories.Category.Extensive where

-- https://ncatlab.org/nlab/show/extensive+category

open import Level

open import Categories.Category.Core
open import Categories.Diagram.Pullback
open import Categories.Category.Cocartesian
open import Categories.Object.Coproduct
open import Categories.Morphism

record Extensive {o ℓ e : Level} (𝒞 : Category o ℓ e) : Set (suc (o ⊔ ℓ ⊔ e)) where
  open Category 𝒞
  open Pullback

  field
    cocartesian : Cocartesian 𝒞

  module CC = Cocartesian cocartesian
  open CC using (_+_; i₁; i₂; ¡)

  field
    pullback₁ : {A B C : Obj} (f : A ⇒ B + C) → Pullback 𝒞 f i₁
    pullback₂ : {A B C : Obj} (f : A ⇒ B + C) → Pullback 𝒞 f i₂
    pullback-of-cp-is-cp : {A B C : Obj} (f : A ⇒ _+_ B C) → IsCoproduct 𝒞 (p₁ (pullback₁ f)) (p₁ (pullback₂ f))

    pullback₁-is-mono : ∀ {A B : Obj} → Mono 𝒞 (i₁ {A = A}{B = B})
    pullback₂-is-mono : ∀ {A B : Obj} → Mono 𝒞 (i₂ {A = A}{B = B})

    disjoint : ∀ {A B : Obj} → IsPullback 𝒞 ¡ ¡ (i₁ {A = A}{B = B}) i₂

max_stars_repo_name: sergey-goncharov/agda-categories

max_issues_repo_name: sergey-goncharov/agda-categories

max_forks_repo_name: sergey-goncharov/agda-categories


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

module Fragment.Equational.Structures where

import Fragment.Equational.Theory.Laws as L
open import Fragment.Equational.Theory
open import Fragment.Equational.Theory.Bundles
open import Fragment.Equational.Model

open import Fragment.Algebra.Algebra

open import Level using (Level)
open import Data.Fin using (Fin; #_; suc; zero)
open import Data.Vec using ([]; _∷_)
open import Data.Vec.Relation.Binary.Pointwise.Inductive using ([]; _∷_)
open import Relation.Binary using (Setoid; Rel)

open import Algebra.Core

private
  variable
    a ℓ : Level

module _ {A : Set a} {_≈_ : Rel A ℓ} where

  open import Algebra.Definitions _≈_
  open import Algebra.Structures _≈_

  module _ {_•_ : Op₂ A} where

    module _ (isMagma : IsMagma _•_) where

      open IsMagma isMagma

      magma→setoid : Setoid a ℓ
      magma→setoid = record { Carrier       = A
                            ; _≈_           = _≈_
                            ; isEquivalence = isEquivalence
                            }

      private

        magma→⟦⟧ : Interpretation Σ-magma magma→setoid
        magma→⟦⟧ MagmaOp.• (x ∷ y ∷ []) = _•_ x y

        magma→⟦⟧-cong : Congruent₂ _•_ → Congruence Σ-magma magma→setoid magma→⟦⟧
        magma→⟦⟧-cong c MagmaOp.• (x₁≈x₂ ∷ y₁≈y₂ ∷ []) = c x₁≈x₂ y₁≈y₂

      magma→isAlgebra : IsAlgebra Σ-magma magma→setoid
      magma→isAlgebra = record { ⟦_⟧     = magma→⟦⟧
                               ; ⟦⟧-cong = magma→⟦⟧-cong ∙-cong
                               }

      magma→algebra : Algebra Σ-magma
      magma→algebra = record { ∥_∥/≈           = magma→setoid
                             ; ∥_∥/≈-isAlgebra = magma→isAlgebra
                             }

      private

        magma→models : Models Θ-magma magma→algebra
        magma→models ()

        magma→isModel : IsModel Θ-magma magma→setoid
        magma→isModel = record { isAlgebra = magma→isAlgebra
                               ; models    = magma→models
                               }

      magma→model : Model Θ-magma
      magma→model = record { ∥_∥/≈   = magma→setoid
                           ; isModel = magma→isModel
                           }

    module _ (isSemigroup : IsSemigroup _•_) where

      private

        open IsSemigroup isSemigroup renaming (assoc to •-assoc)

        semigroup→models : Models Θ-semigroup (magma→algebra isMagma)
        semigroup→models assoc θ = •-assoc (θ (# 0)) (θ (# 1)) (θ (# 2))

        semigroup→isModel : IsModel Θ-semigroup (magma→setoid isMagma)
        semigroup→isModel = record { isAlgebra = magma→isAlgebra isMagma
                                   ; models    = semigroup→models
                                   }

      semigroup→model : Model Θ-semigroup
      semigroup→model = record { ∥_∥/≈   = magma→setoid isMagma
                               ; isModel = semigroup→isModel
                               }

    module _ (isCSemigroup : IsCommutativeSemigroup _•_) where

      private

        open IsCommutativeSemigroup isCSemigroup
          renaming (comm to •-comm; assoc to •-assoc)

        csemigroup→models : Models Θ-csemigroup (magma→algebra isMagma)
        csemigroup→models comm θ = •-comm (θ (# 0)) (θ (# 1))
        csemigroup→models assoc θ = •-assoc (θ (# 0)) (θ (# 1)) (θ (# 2))

        csemigroup→isModel : IsModel Θ-csemigroup (magma→setoid isMagma)
        csemigroup→isModel = record { isAlgebra = magma→isAlgebra isMagma
                                    ; models    = csemigroup→models
                                    }

      csemigroup→model : Model Θ-csemigroup
      csemigroup→model = record { ∥_∥/≈   = magma→setoid isMagma
                                ; isModel = csemigroup→isModel
                                }

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
{-# OPTIONS --without-K --safe #-}
module Util.HoTT.Equiv where

open import Util.HoTT.Equiv.Core public

open import Relation.Binary using (Setoid ; IsEquivalence)

open import Util.Data.Product using (map₂)
open import Util.HoTT.HLevel.Core using (IsContr ; IsProp)
open import Util.HoTT.Section
open import Util.HoTT.Singleton using (IsContr-Singleton)
open import Util.Prelude
open import Util.Relation.Binary.PropositionalEquality using
  ( Σ-≡⁻ ; Σ-≡⁺ ; trans-symʳ ; trans-unassoc )

private
  variable
    α β γ : Level
    A B C : Set α

IsIso→HasSection-forth : {f : A → B} → IsIso f → HasSection f
IsIso→HasSection-forth i = record
  { section = i .IsIso.back
  ; isSection = i .IsIso.forth∘back
  }

IsIso→HasSection-back : {f : A → B} → (i : IsIso f) → HasSection (i .IsIso.back)
IsIso→HasSection-back {f = f} i = record
  { section = f
  ; isSection = i .IsIso.back∘forth
  }

IsIso→Injective : {f : A → B} → IsIso f → Injective f
IsIso→Injective f-iso fx≡fy
  = trans (sym (f-iso .IsIso.back∘forth _))
      (trans (cong (f-iso .IsIso.back) fx≡fy)
        (f-iso .IsIso.back∘forth _))

IsEquiv→IsIso : {f : A → B} → IsEquiv f → IsIso f
IsEquiv→IsIso {A = A} {B = B} {forth} equiv = record
  { back = back′ ; back∘forth = back∘forth′ ; forth∘back = forth∘back′ }
  where
  back′ : B → A
  back′ b with equiv b
  ... | (a , _) , _ = a

  back∘forth′ : ∀ x → back′ (forth x) ≡ x
  back∘forth′ a with equiv (forth a)
  ... | (a′ , fortha′≡fortha) , unique = proj₁ (Σ-≡⁻ (unique (a , refl)))

  forth∘back′ : ∀ x → forth (back′ x) ≡ x
  forth∘back′ b with equiv b
  ... | (a , fortha≡b) , _ = fortha≡b

IsEquiv→Injective : {f : A → B} → IsEquiv f → Injective f
IsEquiv→Injective = IsIso→Injective ∘ IsEquiv→IsIso

-- This proof follows Martin Escardó's lecture notes
-- (https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#fibersandequivalences).
IsIso→IsEquiv : {f : A → B} → IsIso f → IsEquiv f
IsIso→IsEquiv {A = A} {B = B} {forth} iso b
  = ◁-pres-IsContr (◁-trans ii iii) IsContr-Singleton
  where
    module I = IsIso iso

    A◁B : A ◁ B
    A◁B = record
      { retraction = I.back
      ; hasSection = IsIso→HasSection-back iso
      }

    i : ∀ b′ → (forth (I.back b′) ≡ b) ◁ (b′ ≡ b)
    i b′ = record
      { retraction = λ b′≡b → trans (I.forth∘back b′) b′≡b
      ; hasSection = record
        { section = λ eq → trans (sym (I.forth∘back b′)) eq
        ; isSection = λ x → let open ≡-Reasoning in
          begin
            trans (I.forth∘back b′) (trans (sym (I.forth∘back b′)) x)
          ≡⟨ trans-unassoc (I.forth∘back b′) ⟩
            trans (trans (I.forth∘back b′) (sym (I.forth∘back b′))) x
          ≡⟨ cong (λ p → trans p x) (trans-symʳ (I.forth∘back b′)) ⟩
            x
          ∎
        }
      }

    ii : ∃[ a ] (forth a ≡ b) ◁ ∃[ b′ ] (forth (I.back b′) ≡ b)
    ii = Σ-◁-reindexing A◁B

    iii : ∃[ b′ ] (forth (I.back b′) ≡ b) ◁ ∃[ b′ ] (b′ ≡ b)
    --                                   aka Singleton b
    iii = Σ-◁ i

≅-refl : A ≅ A
≅-refl .forth x = x
≅-refl .isIso .IsIso.back x = x
≅-refl .isIso .IsIso.forth∘back x = refl
≅-refl .isIso .IsIso.back∘forth x = refl

≅-sym : A ≅ B → B ≅ A
≅-sym A≅B .forth = A≅B .back
≅-sym A≅B .isIso .IsIso.back = A≅B .forth
≅-sym A≅B .isIso .IsIso.back∘forth = A≅B .forth∘back
≅-sym A≅B .isIso .IsIso.forth∘back = A≅B .back∘forth

≅-trans : A ≅ B → B ≅ C → A ≅ C
≅-trans A≅B B≅C .forth = B≅C .forth ∘ A≅B .forth
≅-trans A≅B B≅C .isIso .IsIso.back = A≅B .back ∘ B≅C .back
≅-trans A≅B B≅C .isIso .IsIso.back∘forth x
  = trans (cong (A≅B .back) (B≅C .back∘forth _)) (A≅B .back∘forth _)
≅-trans A≅B B≅C .isIso .IsIso.forth∘back x
  = trans (cong (B≅C .forth) (A≅B .forth∘back _)) (B≅C .forth∘back _)

≅-isEquivalence : IsEquivalence (_≅_ {α})
≅-isEquivalence .IsEquivalence.refl = ≅-refl
≅-isEquivalence .IsEquivalence.sym = ≅-sym
≅-isEquivalence .IsEquivalence.trans = ≅-trans

≅-setoid : ∀ α → Setoid (lsuc α) α
≅-setoid α .Setoid.Carrier = Set α
≅-setoid α .Setoid._≈_ = _≅_
≅-setoid α .Setoid.isEquivalence = ≅-isEquivalence

≅-reflexive : A ≡ B → A ≅ B
≅-reflexive refl = ≅-refl

≡→≅ = ≅-reflexive

≅-Injective : (i : A ≅ B) → Injective (i .forth)
≅-Injective i = IsIso→Injective (i .isIso)

≅→◁ : A ≅ B → A ◁ B
≅→◁ A≅B = record
  { retraction = A≅B .back
  ; hasSection = IsIso→HasSection-back (A≅B .isIso)
  }

≅→▷ : A ≅ B → B ◁ A
≅→▷ A≅B = record
  { retraction = A≅B .forth
  ; hasSection = IsIso→HasSection-forth (A≅B .isIso)
  }

≃→≅ : A ≃ B → A ≅ B
≃→≅ A≃B .forth = A≃B .forth
≃→≅ A≃B .isIso = IsEquiv→IsIso (A≃B .isEquiv)

≅→≃ : A ≅ B → A ≃ B
≅→≃ A≅B .forth = A≅B .forth
≅→≃ A≅B .isEquiv = IsIso→IsEquiv (A≅B .isIso)

id-IsEquiv : IsEquiv (id {A = A})
id-IsEquiv a = (a , refl) , λ { (b , refl) → refl }

≃-refl : A ≃ A
≃-refl = record { forth = id ; isEquiv = id-IsEquiv }

≃-reflexive : A ≡ B → A ≃ B
≃-reflexive refl = ≃-refl

≡→≃ = ≃-reflexive

≃-sym : A ≃ B → B ≃ A
≃-sym = ≅→≃ ∘ ≅-sym ∘ ≃→≅

≃-trans : A ≃ B → B ≃ C → A ≃ C
≃-trans A≃B B≃C = ≅→≃ (≅-trans (≃→≅ A≃B) (≃→≅ B≃C))

≃-isEquivalence : IsEquivalence (_≃_ {α})
≃-isEquivalence .IsEquivalence.refl = ≃-refl
≃-isEquivalence .IsEquivalence.sym = ≃-sym
≃-isEquivalence .IsEquivalence.trans = ≃-trans

≃-setoid : ∀ α → Setoid (lsuc α) α
≃-setoid α .Setoid.Carrier = Set α
≃-setoid α .Setoid._≈_ = _≃_
≃-setoid α .Setoid.isEquivalence = ≃-isEquivalence

≃-Injective : (e : A ≃ B) → Injective (e .forth)
≃-Injective = ≅-Injective ∘ ≃→≅

≃→◁ : A ≃ B → A ◁ B
≃→◁ = ≅→◁ ∘ ≃→≅

≃→▷ : A ≃ B → B ◁ A
≃→▷ = ≅→▷ ∘ ≃→≅

-- Special cases of ≃-pres-IsOfHLevel (in Util.HoTT.HLevel), but proven
-- directly. This means that A and B can be at different levels.
≅-pres-IsContr : A ≅ B → IsContr A → IsContr B
≅-pres-IsContr A≅B (a , canon) = A≅B .forth a , λ a′
  → trans (cong (A≅B .forth) (canon (A≅B .back a′))) (A≅B .forth∘back _)

≃-pres-IsContr : A ≃ B → IsContr A → IsContr B
≃-pres-IsContr A≃B = ≅-pres-IsContr (≃→≅ A≃B)

≅-pres-IsProp : A ≅ B → IsProp A → IsProp B
≅-pres-IsProp A≅B A-prop x y
  = trans (sym (A≅B .forth∘back x))
      (sym (trans (sym (A≅B .forth∘back y)) (cong (A≅B .forth) (A-prop _ _))))

≃-pres-IsProp : A ≃ B → IsProp A → IsProp B
≃-pres-IsProp A≃B = ≅-pres-IsProp (≃→≅ A≃B)

Σ-≅⁺ : {A : Set α} {B : A → Set β} {C : A → Set γ}
  → (∀ a → B a ≅ C a)
  → Σ A B ≅ Σ A C
Σ-≅⁺ eq = record
  { forth = λ { (a , b) → a , eq a .forth b }
  ; isIso = record
    { back = λ { (a , c) → a , eq a .back c }
    ; back∘forth = λ { (a , b) → Σ-≡⁺ (refl , eq a .back∘forth b) }
    ; forth∘back = λ { (a , c) → Σ-≡⁺ (refl , eq a .forth∘back c) }
    }
  }

Σ-≃⁺ : {A : Set α} {B : A → Set β} {C : A → Set γ}
  → (∀ a → B a ≃ C a)
  → Σ A B ≃ Σ A C
Σ-≃⁺ eq = ≅→≃ (Σ-≅⁺ λ a → ≃→≅ (eq a))

map₂-fiber-≃ : {A : Set α} {B : A → Set β} {C : A → Set γ}
  → (f : ∀ a → B a → C a)
  → ∀ a (c : C a)
  → ∃[ b ] (f a b ≡ c) ≃ ∃[ p ] (map₂ f p ≡ (a , c))
map₂-fiber-≃ f a c = ≅→≃ record
  { forth = λ { (b , refl) → (a , b) , refl }
  ; isIso = record
    { back = λ { ((.a , b) , refl) → b , refl }
    ; back∘forth = λ { (b , refl) → refl }
    ; forth∘back = λ { ((.a , b) , refl) → refl }
    }
  }

IsEquiv-map₂-f→IsEquiv-f : {A : Set α} {B : A → Set β} {C : A → Set γ}
  → (f : ∀ a → B a → C a)
  → IsEquiv (map₂ f)
  → ∀ a → IsEquiv (f a)
IsEquiv-map₂-f→IsEquiv-f {A = A} {B} {C} f equiv a c
  = ≃-pres-IsContr (≃-sym (map₂-fiber-≃ f a c)) (equiv (a , c))

sym-≅ : {x y : A} → (x ≡ y) ≅ (y ≡ x)
sym-≅ = record
  { forth = sym
  ; isIso = record
    { back = sym
    ; back∘forth = λ { refl → refl }
    ; forth∘back = λ { refl → refl }
    }
  }

sym-≃ : {x y : A} → (x ≡ y) ≃ (y ≡ x)
sym-≃ = ≅→≃ sym-≅

IsContr→IsIso : IsContr A → IsContr B → (f : A → B) → IsIso f
IsContr→IsIso (a , a-uniq) (b , b-uniq) f = record
  { back = λ _ → a
  ; back∘forth = λ _ → a-uniq _
  ; forth∘back = λ b′ → trans (sym (b-uniq (f a))) (b-uniq b′)
  }

IsContr→IsEquiv : IsContr A → IsContr B → (f : A → B) → IsEquiv f
IsContr→IsEquiv A-contr B-contr f
  = IsIso→IsEquiv (IsContr→IsIso A-contr B-contr f)

proj₁-IsIso : {A : Set α} {B : A → Set β}
  → (∀ a → IsContr (B a))
  → IsIso (proj₁ {A = A} {B})
proj₁-IsIso B-contr = record
  { back = λ a → (a , B-contr a .proj₁)
  ; back∘forth = λ { (a , b) → Σ-≡⁺ (refl , (B-contr a .proj₂ b)) }
  ; forth∘back = λ _ → refl
  }

proj₁-IsEquiv : {A : Set α} {B : A → Set β}
  → (∀ a → IsContr (B a))
  → IsEquiv (proj₁ {A = A} {B})
proj₁-IsEquiv B-contr = IsIso→IsEquiv (proj₁-IsIso B-contr)

Π-distr-Σ-≅ : (A : Set α) (B : A → Set β) (C : ∀ a → B a → Set γ)
  → (∀ a → Σ[ b ∈ B a ] (C a b))
  ≅ (Σ[ f ∈ (∀ a → B a) ] (∀ a → C a (f a)))
Π-distr-Σ-≅ A B C = record
  { forth = λ f → (λ a → f a .proj₁) , (λ a → f a .proj₂)
  ; isIso = record
    { back = λ { (f , g) → λ a → f a , g a }
    ; back∘forth = λ _ → refl
    ; forth∘back = λ _ → refl
    }
  }

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Postulate extensionality of functions.
--
-- Justification on Agda mailing list:
-- http://permalink.gmane.org/gmane.comp.lang.agda/2343
------------------------------------------------------------------------

module Postulate.Extensionality where

open import Relation.Binary.PropositionalEquality

postulate ext : ∀ {a b} → Extensionality a b

-- Convenience of using extensionality 3 times in a row
-- (using it twice in a row is moderately tolerable)
ext³ : ∀
  {A : Set}
  {B : A → Set}
  {C : (a : A) → B a → Set }
  {D : (a : A) → (b : B a) → C a b → Set}
  {f g : (a : A) → (b : B a) → (c : C a b) → D a b c} →
  ((a : A) (b : B a) (c : C a b) → f a b c ≡ g a b c) → f ≡ g

ext³ fabc=gabc = ext (λ a → ext (λ b → ext (λ c → fabc=gabc a b c)))

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

open import Cubical.Core.Everything
open import Cubical.Algebra.Group

module Cubical.Algebra.Group.Construct.Opposite {ℓ} (G : Group ℓ) where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Prod using (_,_)

open Group G

import Cubical.Algebra.Monoid.Construct.Opposite monoid as OpMonoid
open OpMonoid public hiding (Op-isMonoid; Mᵒᵖ)

•ᵒᵖ-inverseˡ : LeftInverse ε _⁻¹ _•ᵒᵖ_
•ᵒᵖ-inverseˡ _ = inverseʳ _

•ᵒᵖ-inverseʳ : RightInverse ε _⁻¹ _•ᵒᵖ_
•ᵒᵖ-inverseʳ _ = inverseˡ _

•ᵒᵖ-inverse : Inverse ε _⁻¹ _•ᵒᵖ_
•ᵒᵖ-inverse = •ᵒᵖ-inverseˡ , •ᵒᵖ-inverseʳ

Op-isGroup : IsGroup Carrier _•ᵒᵖ_ ε _⁻¹
Op-isGroup = record
  { isMonoid = OpMonoid.Op-isMonoid
  ; inverse  = •ᵒᵖ-inverse
  }

Gᵒᵖ : Group ℓ
Gᵒᵖ = record { isGroup = Op-isGroup }


text:
module Issue2224 where
-- This is a placeholder to ensure that the test case is run.
-- The file of interest is `Issue2224.sh`, and the associated file
-- Issue2224WrongExtension.agda.tex

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.RingSolver.IntAsRawRing where

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

open import Cubical.Foundations.Prelude
open import Cubical.Algebra.RingSolver.RawRing

ℤAsRawRing : RawRing {ℓ-zero}
ℤAsRawRing = rawring ℤ (pos zero) (pos (suc zero)) _+_ _·_ (λ k → - k)

+Ridℤ : (k : ℤ) → (pos zero) + k ≡ k
+Ridℤ k = sym (pos0+ k)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
open import Type

-- The relation (_⟶_) should be interpreted as "a term reduces/rewritten to another term".
-- Also called: Abstract reduction system, abstract rewriting system, rewriting system.
module ReductionSystem {ℓ₁ ℓ₂} {Term : Type{ℓ₁}} (_⟶_ : Term → Term → Type{ℓ₂}) where

open import Functional
open import Graph.Properties
open import Graph.Walk
open import Graph.Walk.Proofs
open import Lang.Instance
import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Relator.Converse
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Relator.ReflexiveTransitiveClosure
open import Structure.Setoid.Uniqueness
open import Structure.Relator.Equivalence
open import Structure.Relator.Ordering
open import Structure.Relator.Properties
open import Syntax.Function
open import Syntax.Transitivity

open Graph.Properties using (intro) public

-- The relation (_⟶_) is a function on the left argument.
-- In terms of paths, it means that there are no forks on any paths.
Deterministic = ∀{a} → Unique(a ⟶_)

-- A term is reducible when there is a term it can reduce to.
-- In terms of paths, it means that one can go somewhere else from this point.
Reducible : Term → Stmt
Reducible(a) = ∃(a ⟶_)

-- A term is in normal form when it is irreducible (cannot be reduced any further).
-- Also called: Irreducible term
-- In terms of paths, it means that this point is a dead-end.
NormalForm : Term → Stmt
NormalForm = FinalVertex(_⟶_)
module NormalForm = FinalVertex

-- "a normalizes to b" means that "a" reduces to the normal form "b".
-- In terms of paths, this means that the dead end of one path from "a" is "b".
record _normalizes-to_ (a : Term) (b : Term) : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
  constructor intro
  field
    reduction : Walk(_⟶_) a b
    ⦃ normalForm ⦄ : NormalForm(b)

-- In terms of paths, this means that there is a path which leads to a dead-end.
WeaklyNormalizes : Term → Stmt
WeaklyNormalizes a = ∃(a normalizes-to_)

-- A reduction system is weakly normalizing when all terms in the language have a normal form.
-- In terms of paths, this means that all points have a path whch eventually lead to a dead-end.
WeaklyNormalizing = ∀ₗ(WeaklyNormalizes)

StronglyNormalizes : Term → Stmt
StronglyNormalizes = Strict.Properties.Accessibleₗ(Converse(_⟶_))

-- Every term reduces to a normal form.
-- Also called: Terminating.
StronglyNormalizing : Stmt
StronglyNormalizing = Strict.Properties.WellFounded(Converse(_⟶_))

-- Both a and b reduce to c in zero or more steps.
-- Also called: _⟶*_*⟵_
CommonReduct : Term → Term → Term → Stmt
CommonReduct c a b = (Walk(_⟶_) a c) ∧ (Walk(_⟶_) b c)

-- Both a and b reduce to the same term in zero or more steps.
-- In terms of paths, this means that paths starting from the two points are able to eventually meet.
-- Also called: Joinable, _⟶*_*⟵_ _↓_.
Joinable : Term → Term → Stmt
Joinable a b = ∃(c ↦ CommonReduct c a b)

module Names where
  import Structure.Relator.Names as Names

  EverywhereCommonReduct = Names.Subrelation (Walk(_⟶_)) Joinable

  module _ (a : Term) where
    Confluent         = ∀{b c} → (Walk(_⟶_) a b) → (Walk(_⟶_) a c) → Joinable b c
    Semiconfluent     = ∀{b c} → (a ⟶ b)         → (Walk(_⟶_) a c) → Joinable b c
    LocallyConfluent  = ∀{b c} → (a ⟶ b)         → (a ⟶ c)         → Joinable b c
    StronglyConfluent = ∀{b c} → (a ⟶ b)         → (a ⟶ c)         → ∃(d ↦ (ReflexiveClosure(_⟶_) b d) ∧ (Walk(_⟶_) c d))
    DiamondProperty   = ∀{b c} → (a ⟶ b)         → (a ⟶ c)         → ∃(d ↦ (b ⟶ d) ∧ (c ⟶ d))

  Confluence = ∀ₗ(Confluent)

-- Also called: The Church-Rosser property
EverywhereCommonReduct = (Walk(_⟶_)) ⊆₂ Joinable

module _ (a : Term) where
  -- A term is confluent when all its reducts have a common reduct.
  -- In terms of paths, this means that paths starting from this point will always eventually meet.
  record Confluent : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.Confluent(a)
  confluent = inst-fn Confluent.proof

  record Semiconfluent : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.Semiconfluent(a)
  semiconfluent = inst-fn Semiconfluent.proof

  record LocallyConfluent : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.LocallyConfluent(a)
  locally-confluent = inst-fn LocallyConfluent.proof

  record StronglyConfluent : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.StronglyConfluent(a)
  strongly-confluent = inst-fn StronglyConfluent.proof

  record DiamondProperty : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field proof : Names.DiamondProperty(a)
  diamond-property = inst-fn DiamondProperty.proof

-- All terms are confluent.
-- In terms of paths, this means that parts starting from the same point can always eventually meet.
Confluence = ∀ₗ(Confluent)

Semiconfluence = ∀ₗ(Semiconfluent)

LocalConfluence = ∀ₗ(LocallyConfluent)

StrongConfluence = ∀ₗ(StronglyConfluent)

record Convergent : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
  constructor intro
  field
    ⦃ confluence ⦄ : Confluence
    ⦃ strongly-normalizing ⦄ : StronglyNormalizing

-- Evaluable = ∃(f ↦ )

-- All paths from a dead-end results in going nowhere.
Normal-unique-Path : ∀{a} → ⦃ _ : NormalForm(a) ⦄ → ∀{b} → Walk(_⟶_) a b → (a ≡ b)
Normal-unique-Path              at                 = [≡]-intro
Normal-unique-Path ⦃ intro na ⦄ (prepend ab1 sb1b) = [⊥]-elim(na ab1)

instance
  -- A term reduces to itself in zero steps.
  -- In terms of paths, this means that two paths starting from the same point can reach this same point.
  Joinable-reflexivity : Reflexivity(Joinable)
  ∃.witness (Reflexivity.proof Joinable-reflexivity {x}) = x
  ∃.proof   (Reflexivity.proof Joinable-reflexivity {x}) = [∧]-intro Walk.at Walk.at

instance
  -- When one reduces to the same term as the other, the other also reduces to the same term as the first one.
  Joinable-symmetry : Symmetry(Joinable)
  ∃.witness (Symmetry.proof Joinable-symmetry {x} {y} xy) = [∃]-witness xy
  ∃.proof   (Symmetry.proof Joinable-symmetry {x} {y} xy) = [∧]-intro ([∧]-elimᵣ(∃.proof xy)) (([∧]-elimₗ(∃.proof xy)))

instance
  -- When one reduces to the same term as the other, the other also reduces to the same term as the first one.
  Walk-Joinable-subrelation : Walk(_⟶_) ⊆₂ Joinable
  ∃.witness (_⊆₂_.proof Walk-Joinable-subrelation {y = y} ab) = y
  ∃.proof   (_⊆₂_.proof Walk-Joinable-subrelation ab) = [∧]-intro ab (reflexivity(Walk(_⟶_)))

module _ ⦃ confl : Confluence ⦄ where
  import      Structure.Relator.Names as Names

  instance
    Confluence-to-Joinable-transitivity : Transitivity(Joinable)
    Confluence-to-Joinable-transitivity = intro proof where
      proof : Names.Transitivity(Joinable)
      proof {x}{y}{z} ([∃]-intro obj-xy ⦃ [∧]-intro pxxy pyxy ⦄) ([∃]-intro obj-yz ⦃ [∧]-intro pyyz pzyz ⦄) = [∃]-intro obj ⦃ [∧]-intro l r ⦄ where
        objxy-objyz-common-reduct : Joinable obj-xy obj-yz
        objxy-objyz-common-reduct = confluent(y) pyxy pyyz

        obj : Term
        obj = [∃]-witness objxy-objyz-common-reduct

        l : Walk(_⟶_) x obj
        l = transitivity(Walk(_⟶_)) pxxy ([∧]-elimₗ ([∃]-proof objxy-objyz-common-reduct))

        r : Walk(_⟶_) z obj
        r = transitivity(Walk(_⟶_)) pzyz ([∧]-elimᵣ ([∃]-proof objxy-objyz-common-reduct))

  instance
    Confluence-to-Joinable-equivalence : Equivalence(Joinable)
    Confluence-to-Joinable-equivalence = intro

module _ (det : Deterministic) where
  -- Frege thing
  deterministic-dichotomy : ∀{a b c} → (Walk(_⟶_) a b) → (Walk(_⟶_) a c) → (Walk(_⟶_) b c) ∨ (Walk(_⟶_) c b)
  deterministic-dichotomy at ac = [∨]-introₗ ac
  deterministic-dichotomy (ab @ (prepend _ _)) at = [∨]-introᵣ ab
  deterministic-dichotomy (prepend ab2 b) (prepend ab3 ac) with det ab2 ab3
  ... | [≡]-intro = deterministic-dichotomy b ac

  deterministic-step : ∀{a b c} → (a ⟶ b) → (Walk(_⟶_) a c) → ((a ≡ c) ∨ (Walk(_⟶_) b c))
  deterministic-step ab at = [∨]-introₗ [≡]-intro
  deterministic-step ab (prepend ab₁ ac) rewrite det ab ab₁ = [∨]-introᵣ ac

  instance
    deterministic-confluence : Confluence
    deterministic-confluence = intro proof where
      proof : Names.Confluence
      proof {c = c} at ac = [∃]-intro c ⦃ [∧]-intro ac at ⦄
      {-# CATCHALL #-}
      proof {b = b} ab at = [∃]-intro b ⦃ [∧]-intro at ab ⦄
      proof (prepend ab1 ab) (prepend ab2 ac) rewrite det ab1 ab2 = proof ab ac

  deterministic-unique-normalizes-to : ∀{a} → Unique(a normalizes-to_)
  deterministic-unique-normalizes-to (intro ax) (intro ay) = proof ax ay where
    proof : ∀{a b c} → ⦃ _ : NormalForm(b) ⦄ → ⦃ _ : NormalForm(c) ⦄ → Walk(_⟶_) a b → Walk(_⟶_) a c → (b ≡ c)
    proof                          at              at              = [≡]-intro
    proof ⦃ intro normal-x ⦄ ⦃ _ ⦄ at              (prepend ab by) = [⊥]-elim(normal-x ab)
    proof ⦃ _ ⦄ ⦃ intro normal-y ⦄ (prepend ab bx) at              = [⊥]-elim(normal-y ab)
    proof (prepend ab₁ b₁x) (prepend ab₂ b₂y) rewrite det ab₁ ab₂ = proof b₁x b₂y

confluence-semiconfluence : Confluence ↔ Semiconfluence
confluence-semiconfluence = [↔]-intro (semiconfl ↦ intro(l(semiconfl))) r where
  l : Names.Confluence ← Semiconfluence
  l semiconfl at                xc = sub₂(Walk(_⟶_))(Joinable) xc
  l semiconfl (prepend xb₁ b₁b) xc with Semiconfluent.proof semiconfl xb₁ xc
  ... | [∃]-intro d ⦃ [∧]-intro b₁d c₁d ⦄ with l semiconfl b₁b b₁d
  ... | [∃]-intro e ⦃ [∧]-intro be de ⦄ = [∃]-intro e ⦃ [∧]-intro be (transitivity(Walk(_⟶_)) c₁d de) ⦄

  r : Confluence → Semiconfluence
  Semiconfluent.proof (r confl) xb xc = Confluent.proof confl (sub₂(_⟶_)(Walk(_⟶_)) xb) xc

-- TODO: Not sure, but maybe?
{-# TERMINATING #-}
strong-confluence-confluence : StrongConfluence → Confluence
strong-confluence-confluence strconfl = intro(proof strconfl) where
  proof : StrongConfluence → Names.Confluence
  proof strconfl {x} at at = reflexivity(Joinable)
  proof strconfl {x} at (prepend xb bc) = sub₂(Walk(_⟶_))(Joinable) (prepend xb bc)
  proof strconfl {x} (prepend xb₁ b₁b) at = symmetry(Joinable) (sub₂(Walk(_⟶_))(Joinable) (prepend xb₁ b₁b))
  proof strconfl {x} {b}{c} (prepend xb₁ b₁b) (prepend xb₂ b₂c) with StronglyConfluent.proof strconfl xb₁ xb₂
  proof strconfl {x} {b}{c} (prepend xd db) (prepend xb₁ b₁c) | [∃]-intro d ⦃ [∧]-intro refl b₁d ⦄ with proof strconfl b₁c b₁d
  ... | [∃]-intro e ⦃ [∧]-intro ce de ⦄ with proof strconfl db de
  ... | [∃]-intro f ⦃ [∧]-intro bf ef ⦄ = [∃]-intro f ⦃ [∧]-intro bf (transitivity(Walk(_⟶_)) ce ef) ⦄
  proof strconfl {x} {b}{c} (prepend xb₁ b₁b) (prepend xb₂ b₂c) | [∃]-intro d ⦃ [∧]-intro (super b₁d) b₂d ⦄ with proof strconfl b₁b (sub₂(_⟶_)(Walk(_⟶_)) b₁d)
  ... | [∃]-intro e ⦃ [∧]-intro be de ⦄ with proof strconfl b₂c b₂d
  ... | [∃]-intro f ⦃ [∧]-intro cf df ⦄ with proof strconfl de df
  ... | [∃]-intro g ⦃ [∧]-intro eg fg ⦄ = [∃]-intro g ⦃ [∧]-intro (transitivity(Walk(_⟶_)) be eg) (transitivity(Walk(_⟶_)) cf fg) ⦄

semiconfluence-everywhere-common-reduct : ⦃ _ : Semiconfluence ⦄ → EverywhereCommonReduct
semiconfluence-everywhere-common-reduct ⦃ semiconfl ⦄ = intro proof where
  instance
    confl : Confluence
    confl = [↔]-to-[←] confluence-semiconfluence semiconfl

  proof : Names.EverywhereCommonReduct
  proof at = reflexivity(Joinable)
  proof {a}{c} (prepend {b = b} ab bc) = transitivity(Joinable) (sub₂(Walk(_⟶_))(Joinable) (sub₂(_⟶_)(Walk(_⟶_)) ab)) (proof bc)

diamond-property-locally-confluent : ⦃ _ : ∀ₗ(DiamondProperty) ⦄ → LocalConfluence
LocallyConfluent.proof (diamond-property-locally-confluent {x}) xb xc = [∃]-map-proof ([∧]-map (sub₂(_⟶_)(Walk(_⟶_))) (sub₂(_⟶_)(Walk(_⟶_)))) (diamond-property _ xb xc)

-- locally-confluent-diamond-property : ⦃ LocalConfluence ⦄ → ∀ₗ(DiamondProperty)
-- DiamondProperty.proof locally-confluent-diamond-property xb xc = {!locally-confluent _ xb xc!}

-- Terminating ↔ LocalConfluence (TODO: See Newman's lemma)
-- Convergent → ∀{a} → Unique(a normalizes-to_)
-- Confluence → (Walk(_⟶_) x y) → NormalForm(y) → (ReflexiveClosure(_⟶_) x y)
-- Confluence → (Walk(_⟶_) x y) → Unique(NormalForm)
-- Confluence → ∀{a} → Unique(a normalizes-to_)

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:
-- Andreas, 2016-07-01 issue #2078
-- Holes in postponed type-checking problems cannot be worked on.

-- {-# OPTIONS -v interaction:30 #-}
-- {-# OPTIONS -v tc.term.exlam:30 -v tc:5 #-}

test : Set → Set
test A = (λ{ B → {!B!}}) A

-- splitting on B gives
-- No type nor action available for hole ?0


text:
module Issue475 where

data Box (A : Set) : Set where
  box : A → Box A

postulate
  T : {A : Set} → A → Set

unbox : {A : Set} → Box A → A

data BoxT {A : Set}(b : Box A) : Set where
  boxT : T (unbox b) → BoxT b

-- Can't be projection-like since we've already used it in BoxT
unbox (box x) = x

postulate
  A : Set
  b : Box A

unboxT : BoxT b → T (unbox b)
unboxT (boxT p) = p


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

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

open import Haskell.Modules.RWS
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                          using (String)

module LibraBFT.Impl.OBM.Logging.Logging where

-- NOTE: Logging operations change the structure of the program, and proofs about peer
-- operations are sensitive to this structure. Therefore, we add a "skeleton" of
-- logging operations so that future refinements do not break existing proofs.
-- In the future, we may wish to model and reason about errors and logging in more detail.

postulate -- TODO-1 : errText : Note, the existing Agda ErrLog constructors do not contain text.
  errText  : ErrLog → List String
  errText' : ErrLog →      String

logErr  : ErrLog → LBFT Unit
logErr  x = tell (LogErr  x ∷ [])

logInfo : InfoLog → LBFT Unit
logInfo x = tell (LogInfo x ∷ [])

logEE : ∀ {A} → List String → LBFT A → LBFT A
logEE _ f = logInfo fakeInfo >> f >>= λ r → logInfo fakeInfo >> pure r

withErrCtx : List String → ErrLog → ErrLog
withErrCtx _ = id

withErrCtx' : ∀ {A} → List String → Either ErrLog A → Either ErrLog A
withErrCtx' ctx = λ where
  (Left  e) → Left (withErrCtx ctx e)
  (Right b) → pure b

withErrCtxD'
  : ∀ {ℓ} {E : Set → Set → Set ℓ} ⦃ _ : EitherLike E ⦄
  → ∀ {A : Set} → List String → E ErrLog A → EitherD ErrLog A
withErrCtxD' ctx e = case toEither e of λ where
  (Left  e) → fromEither $ Left (withErrCtx ctx e)
  (Right b) → fromEither $ Right b

lcheck : ∀ {ℓ} {B : Set ℓ} ⦃ _ : ToBool B ⦄ → B → List String → Either ErrLog Unit
lcheck b t = case check (toBool b) t of λ where
  (Left  e) → Left  fakeErr -- (ErrL [e])
  (Right r) → Right r

lcheckInfo : ∀ {ℓ} {B : Set ℓ} ⦃ _ : ToBool B ⦄ → B → List String → Either ErrLog Unit

lcheckInfo b t = case check (toBool b) t of λ where
  (Left  _) → Left (ErrInfo fakeInfo {-InfoL [e]-})
  (Right r) → Right r


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

-- The category of Cats is Monoidal

module Categories.Category.Monoidal.Instance.StrictCats where

open import Level
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; uncurry)
open import Relation.Binary.PropositionalEquality as ≡
  using (_≡_; refl; cong₂; sym; module ≡-Reasoning; subst₂; cong)
open import Function using (_$_)
open import Data.Unit using (⊤; tt)

open import Categories.Category
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Category.Instance.StrictCats
open import Categories.Category.Instance.One using (One)
open import Categories.Category.Monoidal
open import Categories.Functor.Bifunctor
open import Categories.Functor.Construction.Constant
open import Categories.Functor.Equivalence
open import Categories.Category.Product
open import Categories.Category.Product.Properties
import Categories.Category.Cartesian as Cartesian
import Categories.Morphism.HeterogeneousIdentity as HId
import Categories.Morphism.HeterogeneousIdentity.Properties as HIdProps
import Categories.Morphism.Reasoning as MR
open import Categories.Object.Terminal
open import Categories.Utils.Product using (zipWith)
open import Categories.Utils.EqReasoning

-- (Strict) Cats is a (strict) Monoidal Category with Product as Bifunctor
module Product {o ℓ e : Level} where
  private
    C = Cats o ℓ e
    open Cartesian C
    open _≡F_

  Cats-has-all : BinaryProducts
  Cats-has-all = record { product = λ {A} {B} → record
    { A×B = Product A B
    ; π₁ = πˡ
    ; π₂ = πʳ
    ; ⟨_,_⟩ = _※_
    ; project₁ = record { eq₀ = λ _ → ≡.refl ; eq₁ = λ _ → MR.id-comm-sym A }
    ; project₂ = record { eq₀ = λ _ → ≡.refl ; eq₁ = λ _ → MR.id-comm-sym B }
    ; unique = λ {hA} {h} {i} {j} left right →
      let unique-eq₀ X = cong₂ _,_ (≡.sym $ eq₀ left X) (≡.sym $ eq₀ right X)
      in record
      { eq₀ = unique-eq₀
      ; eq₁ = λ {a} {b} f →
          let module A   = Category A
              module B   = Category B
              module C   = Category C
              module A×B = Category (Product A B)
              open A×B.HomReasoning
              open HId
              open HIdProps
              open Functor
              leq a = ≡.sym $ eq₀ left a
              req a = ≡.sym $ eq₀ right a
          in begin
                hid (Product A B) (unique-eq₀ b) A×B.∘ F₁ (i ※ j) f
              ≈˘⟨ A×B.∘-resp-≈ˡ (×-hid A B (leq b) (req b)) ⟩
                (hid A (leq b) A.∘ F₁ i f , hid B (req b) B.∘ F₁ j f)
              ≈⟨ eq₁⁻¹ left f , eq₁⁻¹ right f ⟩
                F₁ (πˡ C.∘ h) f A.∘ hid A (leq a) ,
                F₁ (πʳ C.∘ h) f B.∘ hid B (req a)
              ≈⟨ A×B.∘-resp-≈ʳ (×-hid A B (leq a) (req a)) ⟩
                (F₁ h f) A×B.∘ (hid (Product A B) (unique-eq₀ a))
              ∎
      }
    } }

  private
    unique-One : {l : Level} (x : Lift l ⊤) → lift tt ≡ x
    unique-One (lift tt) = refl

  One-⊤ : Terminal C
  One-⊤ = record
    { ⊤ = One
    ; ! = const (lift tt)
    ; !-unique = λ f → record { eq₀ = λ _ → unique-One _ ; eq₁ = λ _ → lift tt }
    }

  Cats-is : Cartesian
  Cats-is = record { terminal = One-⊤ ; products = Cats-has-all }

  private
    module Cart = Cartesian.Cartesian Cats-is

  Cats-Monoidal : Monoidal C
  Cats-Monoidal = Cart.monoidal

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Inductive.Examples.List where

open import Inductive
open import Tuple hiding (_++_)

open import Data.Fin
open import Data.Product hiding (map)
open import Data.List hiding (List; map; foldr; _++_)
open import Data.Vec hiding (map; foldr; _++_)

List : Set → Set
List A = Inductive (([] , []) ∷ (((A ∷ []) , ([] ∷ [])) ∷ []))

nil : {A : Set} → List A
nil = construct zero [] []

cons : {A : Set} → A → List A → List A
cons x xs = construct (suc zero) (x ∷ []) ((λ _ → xs) ∷ [])

map : {A B : Set} → (A → B) → List A → List B
map f = rec (nil ∷ ((λ a as ras → cons (f a) ras) ∷ []))

foldr : {A B : Set} → (A → B → B) → B → List A → B
foldr f b = rec (b ∷ (λ a as ras → f a ras) ∷ [])

_++_ : {A : Set} → List A → List A → List A
xs ++ ys = rec (ys ∷ (λ a as ras → cons a ras) ∷ []) xs

max_stars_repo_name: mr-ohman/general-induction

max_issues_repo_name: mr-ohman/general-induction

max_forks_repo_name: mr-ohman/general-induction


text:
{-# OPTIONS --without-K  #-}
module function.isomorphism.remove where

open import sum
open import equality
open import function.isomorphism.core
open import function.isomorphism.utils
open import function.isomorphism.properties
open import function.overloading
open import sets.empty

_minus_ : ∀ {i}(A : Set i) → A → Set i
A minus x = Σ A λ x' → ¬ (x' ≡ x)

iso-remove : ∀ {i j}{A : Set i}{B : Set j}
           → (isom : A ≅ B)
           → (x : A)
           → (A minus x)
           ≅ (B minus (apply isom x))
iso-remove {A = A}{B} isom x =
  Σ-ap-iso isom λ a
   → Π-ap-iso (iso≡ isom) λ _
   → refl≅

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-# OPTIONS --without-K  #-}
module container.w where

open import container.w.core public
open import container.w.algebra public
open import container.w.fibration public

max_stars_repo_name: pcapriotti/agda-base


text:
module Issue604 where

f : (y : Set1) → (x : Set) → Set1
f x = ?


text:
open import Nat
open import Prelude
open import contexts
open import dynamics-core
open import lemmas-matching
open import synth-unicity

module elaboration-unicity where
  mutual
    elaboration-unicity-synth : {Γ : tctx} {e : hexp} {τ1 τ2 : htyp} {d1 d2 : ihexp} {Δ1 Δ2 : hctx} →
                            Γ ⊢ e ⇒ τ1 ~> d1 ⊣ Δ1 →
                            Γ ⊢ e ⇒ τ2 ~> d2 ⊣ Δ2 →
                            τ1 == τ2 × d1 == d2 × Δ1 == Δ2
    elaboration-unicity-synth ESNum ESNum = refl , refl , refl
    elaboration-unicity-synth (ESPlus apt1 dis1 x₁ x₂) (ESPlus apt2 dis2 x₃ x₄)
      with elaboration-unicity-ana x₁ x₃ | elaboration-unicity-ana x₂ x₄
    ... | refl , refl , refl | refl , refl , refl = refl , refl , refl
    elaboration-unicity-synth (ESAsc x) (ESAsc x₁)
      with elaboration-unicity-ana x x₁
    ... | refl , refl , refl = refl , refl , refl
    elaboration-unicity-synth (ESVar {Γ = Γ} x₁) (ESVar x₂) = ctxunicity {Γ = Γ} x₁ x₂ , refl , refl
    elaboration-unicity-synth (ESLam apt1 d1) (ESLam apt2 d2)
      with elaboration-unicity-synth d1 d2
    ... | ih1 , ih2 , ih3 = ap1 _ ih1  , ap1 _ ih2 , ih3
    elaboration-unicity-synth (ESAp _ _ x x₁ x₂ x₃) (ESAp _ _ x₄ x₅ x₆ x₇)
      with synthunicity x x₄
    ... | refl with ▸arr-unicity x₁ x₅
    ... | refl with elaboration-unicity-ana x₂ x₆
    ... | refl , refl , refl with elaboration-unicity-ana x₃ x₇
    ... | refl , refl , refl = refl , refl , refl
    elaboration-unicity-synth ESEHole ESEHole = refl , refl , refl
    elaboration-unicity-synth (ESNEHole _ d1) (ESNEHole _ d2)
      with elaboration-unicity-synth d1 d2
    ... | ih1 , ih2 , ih3 = refl , ap1 _ ih2 , ap1 _ ih3
    elaboration-unicity-synth (ESPair x x₁ wt1 wt2) (ESPair x₂ x₃ wt3 wt4)
      with elaboration-unicity-synth wt1 wt3 | elaboration-unicity-synth wt2 wt4
    ... | refl , refl , refl | refl , refl , refl = refl , refl , refl
    elaboration-unicity-synth (ESFst wt1 x₁ d1) (ESFst wt2 x₄ d2)
      with synthunicity wt1 wt2
    ... | refl with ▸prod-unicity x₁ x₄
    ... | refl with elaboration-unicity-ana d1 d2
    ... | refl , refl , refl = refl , refl , refl
    elaboration-unicity-synth (ESSnd wt1 x₁ d1) (ESSnd wt2 x₄ d2)
      with synthunicity wt1 wt2
    ... | refl with ▸prod-unicity x₁ x₄
    ... | refl with elaboration-unicity-ana d1 d2
    ... | refl , refl , refl = refl , refl , refl

    elaboration-unicity-ana : {Γ : tctx} {e : hexp} {τ τ1 τ2 : htyp} {d1 d2 : ihexp} {Δ1 Δ2 : hctx} →
                          Γ ⊢ e ⇐ τ ~> d1 :: τ1 ⊣ Δ1  →
                          Γ ⊢ e ⇐ τ ~> d2 :: τ2 ⊣ Δ2 →
                          d1 == d2 × τ1 == τ2 × Δ1 == Δ2
    elaboration-unicity-ana (EALam x₁ m D1) (EALam x₂ m2 D2)
      with ▸arr-unicity m m2
    ... | refl with elaboration-unicity-ana D1 D2
    ... | refl , refl , refl = refl , refl , refl
    elaboration-unicity-ana (EALam x₁ m D1) (EASubsume x₂ x₃ () x₅)
    elaboration-unicity-ana (EASubsume x₁ x₂ () x₄) (EALam x₅ m D2)
    elaboration-unicity-ana (EASubsume x x₁ x₂ x₃) (EASubsume x₄ x₅ x₆ x₇)
      with elaboration-unicity-synth x₂ x₆
    ... | refl , refl , refl = refl , refl , refl
    elaboration-unicity-ana (EASubsume x x₁ () x₃) (EAInl x₄ wt2)
    elaboration-unicity-ana (EASubsume x x₁ () x₃) (EAInr x₄ wt2)
    elaboration-unicity-ana (EASubsume x x₁ () x₃) (EACase x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ x₁₃ wt2 wt3)
    elaboration-unicity-ana (EASubsume x x₁ x₂ x₃) EAEHole = abort (x _ refl)
    elaboration-unicity-ana (EASubsume x x₁ x₂ x₃) (EANEHole _ x₄) = abort (x₁ _ _ refl)
    elaboration-unicity-ana (EAInl x x₁) (EAInl y y₁)
      with ▸sum-unicity x y
    ... | refl with elaboration-unicity-ana x₁ y₁
    ... | refl , refl , refl = refl , refl , refl
    elaboration-unicity-ana (EAInl x wt1) (EASubsume x₁ x₂ () x₄)
    elaboration-unicity-ana (EAInr x x₁) (EAInr y y₁)
      with ▸sum-unicity x y
    ... | refl with elaboration-unicity-ana x₁ y₁
    ... | refl , refl , refl = refl , refl , refl
    elaboration-unicity-ana (EAInr x wt1) (EASubsume x₁ x₂ () x₄)
    elaboration-unicity-ana (EACase x x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ wt1 wt2) (EASubsume x₁₀ x₁₁ () x₁₃)
    elaboration-unicity-ana (EACase x x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁) (EACase y y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ y₉ y₁₀ y₁₁)
      with elaboration-unicity-synth x₈ y₈
    ... | refl , refl , refl with ▸sum-unicity x₉ y₉
    ... | refl with elaboration-unicity-ana x₁₀ y₁₀
    ... | refl , refl , refl with elaboration-unicity-ana x₁₁ y₁₁
    ... | refl , refl , refl = refl , refl , refl
    elaboration-unicity-ana EAEHole (EASubsume x x₁ x₂ x₃) = abort (x _ refl)
    elaboration-unicity-ana EAEHole EAEHole = refl , refl , refl
    elaboration-unicity-ana (EANEHole _ x) (EASubsume x₁ x₂ x₃ x₄) = abort (x₂ _ _ refl)
    elaboration-unicity-ana (EANEHole _ x) (EANEHole _ x₁)
      with elaboration-unicity-synth x x₁
    ... | refl , refl , refl = refl , refl , refl

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
-- Should fail with S i != i
module Issue216 where

open import Common.Level

Foo : {i : Level} → Set i
Foo {i} = (R : Set i) → R


text:
module relations where

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

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n : ℕ} → zero ≤ n
  s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n

infix 4 _≤_

foo : 2 ≤ 4
foo = s≤s (s≤s z≤n)

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

bar : 1 ≤ 3
bar = inv-s≤s foo

max_stars_repo_name: aronerben/agda-playground

max_issues_repo_name: aronerben/agda-playground

max_forks_repo_name: aronerben/agda-playground


text:
module Crash where

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

data B : Set where
  true : B
  false : B

F : B -> Set
F true  = N
F false = B

not : B -> B
not true  = false
not false = true

h : ((x : F _) -> F (not x)) -> N
h g = g zero