text:
module x10-747Lists-hc where

-- Library

import Relation.Binary.PropositionalEquality as Eq
open Eq                         using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Data.Bool           using (Bool; true; false; T; _∧_; _∨_; not)
open import Data.Nat            using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
open import Data.Nat.Properties using (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
open import Relation.Nullary    using (¬_; Dec; yes; no)
open import Data.Product        using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum            using (_⊎_; inj₁; inj₂)
open import Function            using (_∘_)
open import Level               using (Level)
open import Data.Empty          using (⊥)

------------------------------------------------------------------------------
-- Copied from 747Isomorphism.

infix 0 _≃_
record _≃_ (A B : Set) : Set where
  constructor mk-≃  -- This has been added, not in PLFA
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

infix 0 _≲_
record _≲_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
open _≲_

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
open _⇔_

------------------------------------------------------------------------------
-- Polymorphic lists (parameterized version).

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

infixr 5 _∷_

-- example
_ : List ℕ
_ = 0 ∷ 1 ∷ 2 ∷ []

-- equivalent indexed version
data List' : Set → Set where
  []'  : ∀ {A : Set} →               List' A
  _∷'_ : ∀ {A : Set} → A → List' A → List' A

-- using implicit arguments in above example (why?)
_ : List ℕ
_ = _∷_ {ℕ} 0 (_∷_ {ℕ} 1 (_∷_ {ℕ} 2 ([] {ℕ})))

-- tell Agda to use Haskell lists internally
{-# BUILTIN LIST List #-}

-- useful syntax
pattern [_] z = z ∷ []
pattern [_,_] y z = y ∷ z ∷ []
pattern [_,_,_] x y z = x ∷ y ∷ z ∷ []
pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_] v w x y z = v ∷ w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_,_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []

-- append for lists
infixr 5 _++_

_++_ : ∀ {A : Set} → List A → List A → List A
[]       ++ ys =            ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

_ : [ 0 , 2 , 4 ] ++ [ 3 , 5 ] ≡ [ 0 , 2 , 4 , 3 , 5 ]
_ = refl

-- associativity of append
++-assoc : ∀ {A : Set} → (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc      []  ys zs = refl
++-assoc (x ∷ xs) ys zs rewrite ++-assoc xs ys zs = refl

-- left/right identities for append
++-identityˡ : ∀ {A : Set} → (xs : List A) → [] ++ xs ≡ xs
++-identityˡ xs = refl

++-identityʳ : ∀ {A : Set} → (xs : List A) → xs ++ [] ≡ xs
++-identityʳ      [] = refl
++-identityʳ (x ∷ xs) rewrite ++-identityʳ xs = refl

-- length of a list
length : ∀ {A : Set} → List A → ℕ
length      []  = zero
length (x ∷ xs) = suc (length xs)

_ : length [ 0 , 1 , 2 ] ≡ 3
_ = refl

-- reasoning about length.
length-++ : ∀ {A : Set} → (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys
length-++      []  ys = refl
length-++ (x ∷ xs) ys rewrite length-++ xs ys = refl

-- quadratic time reverse using structural recursion
reverse : ∀ {A : Set} → List A → List A
reverse      []  = []
reverse (x ∷ xs) = reverse xs ++ [ x ]

_ : reverse [ 0 , 1 , 2 ] ≡ [ 2 , 1 , 0 ]
_ = refl

-- 747/PLFA exercise: RevCommApp (1 point)
-- reverse commutes with ++
-- https://gist.github.com/pedrominicz/012e842362f6c65361722ed1aaf10178
-- The key to this one is NOT splitting ys.
reverse-++-commute : ∀ {A : Set}
  → (xs ys : List A)
  → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++-commute      []  ys  rewrite ++-identityʳ (reverse ys) = refl
reverse-++-commute (x ∷ xs) ys
-- reverse   ((x ∷ xs) ++ ys)          ≡ reverse ys ++ reverse (x ∷ xs)
-- reverse        (xs  ++ ys) ++ [ x ] ≡ reverse ys ++ reverse      xs ++ [ x ]
  rewrite
    reverse-++-commute xs ys
-- (reverse ys ++ reverse xs) ++ [ x ] ≡ reverse ys ++ reverse      xs ++ [ x ]
  | ++-assoc (reverse ys) (reverse xs) [ x ]
--  reverse ys ++ reverse xs  ++ [ x ] ≡ reverse ys ++ reverse      xs ++ [ x ]
  = refl

-- NOT USED
snoc : {A : Set} → List A → A → List A
snoc     []  x = x ∷ []
snoc (y ∷ l) x = y ∷ (snoc l x)

-- NOT USED
snoc≡app : {A : Set} → (l : List A) → (a : A) → snoc l a ≡ l ++ [ a ]
snoc≡app     []  a = refl
snoc≡app (x ∷ l) a rewrite (snoc≡app l a) = refl

-- NOT USED
reverse-snoc : ∀ {A : Set} → (xs : List A) → List A
reverse-snoc      []  = []
reverse-snoc (x ∷ xs) = snoc (reverse-snoc xs) x

_ : reverse-snoc [ 0 , 1 , 2 ] ≡ [ 2 , 1 , 0 ]
_ = refl

-- NOT USED
reverse≡reverse-snoc : ∀ {A : Set} → (xs : List A) → reverse xs ≡ reverse-snoc xs
reverse≡reverse-snoc      [] = refl
reverse≡reverse-snoc (x ∷ xs)     -- reverse (x ∷ xs)         ≡ reverse-snoc  (x ∷ xs)
                                  -- reverse      xs ++ [ x ] ≡ snoc (reverse-snoc xs) x
  rewrite
    reverse≡reverse-snoc xs       -- reverse-snoc xs ++ [ x ] ≡ snoc (reverse-snoc xs) x
  | snoc≡app (reverse-snoc xs) x  -- reverse-snoc xs ++ [ x ] ≡ reverse-snoc xs ++   [ x ]
  = refl

-- 747/PLFA exercise: RevInvol (1 point)
-- Reverse is its own inverse.
reverse-involutive : ∀ {A : Set} → (xs : List A) → reverse (reverse xs) ≡ xs
reverse-involutive      []  = refl
reverse-involutive (x ∷ xs)                 -- reverse (reverse (x ∷ xs))         ≡ x ∷ xs
                                            -- reverse (reverse      xs ++ [ x ]) ≡ x ∷ xs
  rewrite
    (reverse-++-commute (reverse xs) [ x ]) -- x ∷ reverse (reverse xs)           ≡ x ∷ xs
  | reverse-involutive xs                   -- x ∷ xs                             ≡ x ∷ xs
  = refl

-- towards more efficient linear time reverse

-- generalization of reverse
shunt : ∀ {A : Set} → List A → List A → List A
shunt      []  ys =               ys
shunt (x ∷ xs) ys = shunt xs (x ∷ ys)

-- explanation of what shunt is doing
shunt-reverse : ∀ {A : Set} → (xs ys : List A) → shunt xs ys ≡ reverse xs ++ ys
shunt-reverse      []       ys  = refl
shunt-reverse (x ∷ xs)      [] -- shunt (x ∷ xs)   []    ≡ reverse (x ∷ xs)           ++ []
                               -- shunt      xs    [ x ] ≡ (reverse     xs  ++ [ x ]) ++ []
  rewrite
   ++-identityʳ (reverse     xs  ++ [ x ])
                               -- shunt      xs    [ x ] ≡ reverse xs ++ [ x ]
  | shunt-reverse xs [ x ]     -- reverse    xs ++ [ x ] ≡ reverse xs ++ [ x ]
  = refl
shunt-reverse (x ∷ xs) (y ∷ ys)
                           -- shunt (x ∷ xs)      (y ∷ ys) ≡ reverse (x ∷ xs)          ++ y ∷ ys
                           -- shunt      xs   (x ∷ y ∷ ys) ≡ (reverse     xs ++ [ x ]) ++ y ∷ ys
  rewrite
    shunt-reverse xs (x ∷ y ∷ ys)
                           -- reverse    xs ++ x ∷ y ∷ ys  ≡ (reverse     xs ++ [ x ]) ++ y ∷ ys
  | ++-assoc (reverse xs) [ x ] (y ∷ ys)
                           -- reverse    xs ++ x ∷ y ∷ ys  ≡  reverse     xs ++   x ∷     y ∷ ys
  = refl

-- linear reverse is a special case of shunt
reverse' : ∀ {A : Set} → List A → List A
reverse' xs = shunt xs []

_ : reverse' [ 0 , 1 , 2 ] ≡ [ 2 , 1 , 0 ]
_ = refl

-- prove quadratic and linear reverse are equivalent
reverses : ∀ {A : Set} → (xs : List A) → reverse' xs ≡ reverse xs
reverses      []  = refl
reverses (x ∷ xs)                -- reverse' (x ∷ xs)   ≡ reverse (x ∷ xs)
                                 -- reverse' (x ∷ xs)   ≡ reverse xs ++ [ x ]
  rewrite shunt-reverse xs [ x ] -- reverse xs ++ [ x ] ≡ reverse xs ++ [ x ]
  = refl

-- common higher-order list functions

map : ∀ {A B : Set} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

_ : map suc [ 0 , 1 , 2 ] ≡ [ 1 , 2 , 3 ]
_ = refl

-- 747/PLFA exercise: MapCompose (1 point)
-- The map of a composition is the composition of maps.
-- Changed from PLFA: some arguments made explicit, uses pointwise equality.
map-compose : ∀ {A B C : Set} (f : A → B) (g : B → C) (xs : List A)
  → map (g ∘ f) xs ≡ (map g ∘ map f) xs
map-compose f g      []  = refl
map-compose f g (x ∷ xs) --              map (g ∘ f) (x ∷ xs) ≡ (map g ∘ map f) (x ∷ xs)
                         -- (g ∘ f) x  ∷ map (g ∘ f)      xs  ≡ (map g ∘ map f) (x ∷ xs)
  rewrite
    map-compose f g xs   --    g (f x) ∷ map g (map f xs)     ≡ g (f x) ∷ map g (map f xs)
  = refl

-- 747/PLFA exercise: MapAppendComm (1 point)
-- The map of an append is the append of maps.
-- Changed from PLFA: some arguments made explicit.
map-++-commute : ∀ {A B : Set} (f : A → B) (xs ys : List A)
 →  map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++-commute f      []  ys = refl
map-++-commute f (x ∷ xs) ys -- map f ((x ∷ xs) ++ ys) ≡ map f (x ∷ xs) ++ map f ys
                             -- f x ∷ map f (xs ++ ys) ≡ f x ∷ map f xs ++ map f ys
  rewrite
    map-++-commute f xs ys   -- f x ∷ map f xs ++ map f ys ≡ f x ∷ map f xs ++ map f ys
  = refl

------------------------------------------------------------------------------

-- PLFA exercise: map over trees
-- trees with leaves of type A and internal nodes of type B
data Tree (A B : Set) : Set where
  leaf : A                       → Tree A B
  node : Tree A B → B → Tree A B → Tree A B

map-Tree : ∀ {A B C D : Set} → (A → C) → (B → D) → Tree A B → Tree C D
map-Tree f g (leaf a)       = leaf (f a)
map-Tree f g (node tl b tr) = node (map-Tree f g tl) (g b) (map-Tree f g tr)

------------------------------------------------------------------------------

-- Fold-right: put operator ⊗ between each list element (and supplied final element).
--             ⊗ is considered right-associative.
-- Fold-right is universal for structural recursion on one argument.

foldr : ∀ {A B : Set} → (A → B → B) → B → List A → B
foldr _⊗_ e [] = e
foldr _⊗_ e (x ∷ xs) = x ⊗ foldr _⊗_ e xs

_ : foldr _+_ 0 [ 1 , 2 , 3 , 4 ] ≡ 10
_ = refl

-- Summing a list using foldr.

sum : List ℕ → ℕ
sum = foldr _+_ 0

_ : sum [ 1 , 2 , 3 , 4 ] ≡ 10
_ = refl

-- PLFA exercise: use foldr to define product on lists of naturals
product : List ℕ → ℕ
product = foldr _*_ 1

_ : product [ 1 , 2 , 3 , 4 ] ≡ 24
_ = refl

-- 747/PLFA exercise: FoldrOverAppend (1 point)
-- prove foldr over an append can be expressed as foldrs over each list.
foldr-++ : ∀ {A B : Set} (_⊗_ : A → B → B) (b : B) (xs ys : List A) →
  foldr _⊗_ b (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ b ys) xs
foldr-++ _⊗_ b      []  ys = refl
foldr-++ _⊗_ b (x ∷ xs) ys
  -- foldr _⊗_ b ((x ∷ xs) ++ ys)        ≡ foldr _⊗_ (foldr _⊗_ b ys) (x ∷ xs)
  -- (x ⊗ foldr _⊗_ b (xs ++ ys))        ≡  (x ⊗ foldr _⊗_ (foldr _⊗_ b ys) xs)
  rewrite foldr-++ _⊗_ b xs ys
  -- (x ⊗ foldr _⊗_ (foldr _⊗_ b ys) xs) ≡ (x ⊗ foldr _⊗_ (foldr _⊗_ b ys) xs)
  = refl

-- 747/PLFA exercise: MapIsFoldr (1 point)
-- Show that map can be expressed as a fold.
-- Changed from PLFA: some arguments made explicit, uses pointwise equality.
map-is-foldr : ∀ {A B : Set} (f : A → B) (xs : List A)
  → map f xs ≡ foldr (λ x rs → f x ∷ rs) [] xs
map-is-foldr f      []  = refl
map-is-foldr f (x ∷ xs) rewrite map-is-foldr f xs = refl

-- PLFA exercise: write a fold for trees
fold-Tree : ∀ {A B C : Set} → (A → C) → (C → B → C → C) → Tree A B → C
fold-Tree f g (leaf a)       = f a
fold-Tree f g (node tl b tr) = g (fold-Tree f g tl) b (fold-Tree f g tr)

-- PLFA exercise: the downFrom function computes a countdown list
-- Prove an equality about its sum

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

_ : downFrom 4 ≡ [ 3 , 2 , 1 , 0 ]
_ = refl

_ : sum (downFrom 4) ≡ 6
_ = refl
{- TODO
sum-downFrom : ∀ (n : ℕ) → sum (downFrom n) * 2 ≡ n * (n ∸ 1)
sum-downFrom n = {!!}
-}

------------------------------------------------------------------------------

-- 'Monoid' : set with
-- - an associative operator
-- - an element which is the left and right identity
record IsMonoid (A : Set) : Set where
  field
    id        : A
    _⊗_       : A → A → A
    assoc     : ∀ (x y z : A) → (x ⊗ y) ⊗ z ≡ x ⊗ (y ⊗ z)
    identityˡ : ∀ (x : A) → id ⊗ x          ≡ x
    identityʳ : ∀ (x : A) → x ⊗ id          ≡ x

-- The following open command is different from PLFA; it uses instance arguments,
-- which work like typeclasses in Haskell (allow overloading, which is cleaner).

open IsMonoid {{ ...}} public

-- These pragmas make displays of goal and context look nicer.
{-# DISPLAY IsMonoid.id  _ = id #-}
{-# DISPLAY IsMonoid._⊗_ _ = _⊗_ #-}

-- instances of Monoid
instance

 +-monoid : IsMonoid ℕ
 IsMonoid.id        +-monoid = 0
 IsMonoid._⊗_       +-monoid = _+_
 IsMonoid.assoc     +-monoid = +-assoc
 IsMonoid.identityˡ +-monoid = +-identityˡ
 IsMonoid.identityʳ +-monoid = +-identityʳ

 *-monoid : IsMonoid ℕ
 IsMonoid.id        *-monoid = 1
 IsMonoid._⊗_       *-monoid = _*_
 IsMonoid.assoc     *-monoid = *-assoc
 IsMonoid.identityˡ *-monoid = *-identityˡ
 IsMonoid.identityʳ *-monoid = *-identityʳ

 ++-monoid : ∀ {A : Set} → IsMonoid (List A)
 IsMonoid.id        ++-monoid = []
 IsMonoid._⊗_       ++-monoid = _++_
 IsMonoid.assoc     ++-monoid = ++-assoc
 IsMonoid.identityˡ ++-monoid = ++-identityˡ
 IsMonoid.identityʳ ++-monoid = ++-identityʳ

-- property of foldr over a monoid
foldr-monoid : ∀ {A : Set} → {{m : IsMonoid A}} →
  ∀ (xs : List A) (y : A)
  → foldr _⊗_ y xs ≡ (foldr _⊗_ id xs) ⊗ y
foldr-monoid {A} ⦃ m ⦄ [] y
  rewrite identityˡ y = refl
foldr-monoid {A} ⦃ m ⦄ (x ∷ xs) y
  with foldr-monoid xs y
... | xxx
  rewrite
      xxx
    | sym (assoc x (foldr _⊗_ id xs) y)
  = refl

foldr-monoid-++ : ∀ {A : Set} → {{m : IsMonoid A}} →
  ∀ (xs ys : List A)
  → foldr _⊗_ id (xs ++ ys) ≡ foldr _⊗_ id xs ⊗ foldr _⊗_ id ys
foldr-monoid-++ {A} ⦃ m ⦄ [] ys
  rewrite
    sym (foldr-monoid {A} {{m}} [] (foldr _⊗_ id ys))
  = refl
foldr-monoid-++ {A} ⦃ m ⦄ (x ∷ xs) ys
  rewrite
    foldr-monoid-++ {A} {{m}} xs ys
  | assoc x (foldr _⊗_ id xs) (foldr _⊗_ id ys)
  = refl

-- 747/PLFA exercise: Foldl (1 point)
-- Define foldl, which associates left instead of right, e.g.
--   foldr _⊗_ e [ x , y , z ]  =  x ⊗ (y ⊗ (z ⊗ e))
--   foldl _⊗_ e [ x , y , z ]  =  ((e ⊗ x) ⊗ y) ⊗ z

foldl : ∀ {A B : Set} → (B → A → B) → B → List A → B
foldl _⊗_ e      []  = e
foldl _⊗_ e (x ∷ xs) = foldl _⊗_ (e ⊗ x) xs

sum-foldl : foldl _+_ 0 [ 4 , 3 , 2 , 1 ] ≡ 10
sum-foldl = refl

monus-foldl : foldl _∸_ 20 [ 4 , 3 , 2 ] ≡ 11
monus-foldl = refl

monus-foldr : foldr _∸_ 20 [ 4 , 3 , 2 ] ≡ 1
monus-foldr = refl

-- 747/PLFA exercise: FoldrMonFoldl (2 points)
-- Show that foldr and foldl compute the same value on a monoid
-- when the base case is the identity.
-- Hint: generalize to when the base case is an arbitrary value.

foldl-r-mon-helper : ∀ {A : Set} {{m : IsMonoid A}}
  → ∀ (xs : List A) (y : A)
  → foldl _⊗_ y xs ≡ y ⊗ foldl _⊗_ id xs
foldl-r-mon-helper      []  y rewrite identityʳ y = refl
foldl-r-mon-helper (x ∷ xs) y      -- foldl _⊗_ y (x ∷ xs) ≡ (y ⊗ foldl _⊗_ id (x ∷ xs))
                                   -- foldl _⊗_ (y ⊗ x) xs ≡ (y ⊗ foldl _⊗_ (id ⊗ x) xs)
  rewrite
    identityˡ x                    --             foldl _⊗_ (y ⊗ x) xs ≡ (y ⊗ foldl _⊗_ x xs)
  | foldl-r-mon-helper xs (y ⊗ x)  -- ((y ⊗ x) ⊗ foldl _⊗_ id xs)     ≡ (y ⊗ foldl _⊗_ x xs)
  | assoc y x (foldl _⊗_ id xs)    -- (y ⊗ (x ⊗ foldl _⊗_ id xs))     ≡ (y ⊗ foldl _⊗_ x xs)
  | foldl-r-mon-helper xs x        -- (y ⊗ (x ⊗ foldl _⊗_ id xs)) ≡ (y ⊗ (x ⊗ foldl _⊗_ id xs))
  = refl

foldl-r-mon : ∀ {A : Set} → {{m : IsMonoid A}}
  → ∀ (xs : List A)  → foldl _⊗_ id xs ≡ foldr _⊗_ id xs
foldl-r-mon      []  = refl
foldl-r-mon (x ∷ xs)
                            -- foldl _⊗_ id (x ∷ xs) ≡ foldr _⊗_ id (x ∷ xs)
                            -- foldl _⊗_ (id ⊗ x) xs ≡ (x ⊗ foldr _⊗_ id xs)
  rewrite
    identityˡ x             -- foldl _⊗_       x  xs ≡ (x ⊗ foldr _⊗_ id xs)
  | foldl-r-mon-helper xs x -- (x ⊗ foldl _⊗_ id xs) ≡ (x ⊗ foldr _⊗_ id xs)
  | foldl-r-mon xs          -- (x ⊗ foldr _⊗_ id xs) ≡ (x ⊗ foldr _⊗_ id xs)
  = refl

------------------------------------------------------------------------------

-- Inductively-defined predicates over lists

-- All P xs means P x holds for every element of xs
data All {A : Set} (P : A → Set) : List A → Set where
  []  :                                            All P []
  _∷_ : ∀ {x : A} {xs : List A} → P x → All P xs → All P (x ∷ xs)

_ : All (_≤ 2) [ 0 , 1 , 2 ]
_ = z≤n ∷ s≤s z≤n ∷ s≤s (s≤s z≤n) ∷ []

-- Any P xs means P x holds for some element of xs
data Any {A : Set} (P : A → Set) : List A → Set where
  here  : ∀ {x : A} {xs : List A} →     P x  → Any P (x ∷ xs)
  there : ∀ {x : A} {xs : List A} → Any P xs → Any P (x ∷ xs)

-- membership in list as application of Any
infix 4 _∈_ _∉_
_∈_ : ∀ {A : Set} (x : A) (xs : List A) → Set
x ∈ xs = Any (x ≡_) xs

_∉_ : ∀ {A : Set} (x : A) (xs : List A) → Set
x ∉ xs = ¬ (x ∈ xs)

_ : 0 ∈ [ 0 , 1 , 0 , 2 ]
_ = here refl

_ : 0 ∈ [ 1 , 2 , 0 ]
_ = there (there (here refl))

not-in : 3 ∉ [ 0 , 1 , 0 , 2 ]
not-in (here ())
not-in (there (here ()))
not-in (there (there (here ())))
not-in (there (there (there (here ()))))

-- The development in PLFA, repeated with our notation.

All-++-⇔ : ∀ {A : Set} {P : A → Set}
         → (xs ys : List A)
         → All P (xs ++ ys) ⇔ (All P xs × All P ys)
to   (All-++-⇔ xs ys) = to'   xs ys
 where
  to' : ∀ {A : Set} {P : A → Set} (xs ys : List A)
      → All P (xs ++ ys) → (All P xs × All P ys)
  to' []       ys = λ All-P-ys   → ⟨ [] , All-P-ys ⟩
  to' (x ∷ xs) ys (Px ∷ All-P-xs++ys) with to' xs ys All-P-xs++ys
  ... | ⟨ All-P-xs , All-PP-ys ⟩ = ⟨ Px ∷ All-P-xs , All-PP-ys ⟩
from (All-++-⇔ xs ys) = from' xs ys
 where
  from' : ∀ { A : Set} {P : A → Set} (xs ys : List A)
        → All P xs × All P ys → All P (xs ++ ys)
  from'      []  ys = λ { ⟨ All-P-[]      , All-P-ys ⟩ → All-P-ys }
  from' (x ∷ xs) ys = λ { ⟨ Px ∷ All-P-xs , All-P-ys ⟩ → Px ∷ from' xs ys ⟨ All-P-xs , All-P-ys ⟩ }

-- PLFA exercise: state and prove Any-++-⇔
Any-++-⇔ : ∀ {A : Set} {P : A → Set}
         → (xs ys : List A)
         → Any P (xs ++ ys) ⇔ (Any P xs ⊎ Any P ys)
to   (Any-++-⇔ xs ys) = to'   xs ys
 where
  to' : ∀ {A : Set} {P : A → Set}
      → (xs ys : List A)
      →  Any P (xs ++ ys)
      → (Any P  xs ⊎ Any P ys)
  to'      []  ys = λ Any-P-ys → inj₂ Any-P-ys
  to' (x ∷ xs) ys (here  Px )  = inj₁ (here Px)
  to' (x ∷ xs) ys (there Any-P-xs++ys) with to' xs ys Any-P-xs++ys
  ... | inj₁ Any-P-xs          = inj₁ (there Any-P-xs)
  ... | inj₂ Any-P-ys          = inj₂        Any-P-ys
from (Any-++-⇔ xs ys) = from' xs ys
 where
  from' : ∀ {A : Set} {P : A → Set}
        → (xs ys : List A)
        → (Any P  xs ⊎ Any P ys)
        →  Any P (xs ++ ys)
  from'      []  ys (inj₂        Any-P-ys)  = Any-P-ys
  from' (x ∷ xs) ys (inj₂        Any-P-ys)  = there (from' xs ys (inj₂ Any-P-ys))
  from' (x ∷ xs) ys (inj₁ (here      Px))   = here Px
  from' (x ∷ xs) ys (inj₁ (there Any-P-xs)) = there (from' xs ys (inj₁ Any-P-xs))

-- use Any-++-⇔ to demonstrate an equivalence relating ∈ and _++_ TODO

-- PLFA exercise: Show that the equivalence All-++-⇔ can be extended to an isomorphism.

-- PLFA exercise: Here is a universe-polymorphic version of composition,
-- and a version of DeMorgan's law for Any and All expressed using it.

_∘'_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
     → (B → C) → (A → B) → A → C
(g ∘' f) x = g (f x)

¬Any≃All¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
          → (¬_ ∘' Any P) xs ≃ All (¬_ ∘' P) xs
to      (¬Any≃All¬ _      [])  ¬_∘'AnyPxs = []
to      (¬Any≃All¬ P (_ ∷ xs)) ¬_∘'AnyPxs with to (¬Any≃All¬ P xs)
... | AnyPxs→⊥→Allλx₁→Px₁→⊥xs
  = (λ Px → ¬ here Px ∘'AnyPxs) ∷ AnyPxs→⊥→Allλx₁→Px₁→⊥xs (λ AnyPxs → ¬ there AnyPxs ∘'AnyPxs)

from    (¬Any≃All¬ _      [])  All¬_∘'Pxs ()
from    (¬Any≃All¬ P (x ∷ xs)) All¬_∘'Pxs (here     Px) with from (¬Any≃All¬ P xs)
... | All-λx₁→Px₁→⊥-xs→AnyPxs→⊥
  = All-λx₁→Px₁→⊥-xs→AnyPxs→⊥ {!!} {!!}
from    (¬Any≃All¬ _ (x ∷ xs)) All¬_∘'Pxs (there AnyPxs) = {!!}

from∘to (¬Any≃All¬ P xs) = {!!}
to∘from (¬Any≃All¬ P xs) = {!!}
{-
-- Can we prove the following? If not, explain why.
--  ¬All≃Any¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
--    → (¬_ ∘' All P) xs ≃ Any (¬_ ∘' P) xs

-- End of PLFA exercise

-- Decidability of All

-- A Boolean analogue of All

all : ∀ {A : Set} → (A → Bool) → List A → Bool
all p  =  foldr _∧_ true ∘ map p

-- A Dec analogue of All

-- A definition of a predicate being decidable

Decidable : ∀ {A : Set} → (A → Set) → Set
Decidable {A} P  =  ∀ (x : A) → Dec (P x)

All? : ∀ {A : Set} {P : A → Set} → Decidable P → Decidable (All P)
All? P? [] = yes []
All? P? (x ∷ xs) with P? x | All? P? xs
All? P? (x ∷ xs) | yes p | yes p₁ = yes (p ∷ p₁)
All? P? (x ∷ xs) | yes p | no ¬p = no (λ { (x ∷ x₁) → ¬p x₁})
All? P? (x ∷ xs) | no ¬p | _ = no (λ { (x ∷ x₁) → ¬p x})

-- PLFA exercise: repeat above for Any

-- PLFA exercises: All-∀ and Any-∃
-- You will need the stronger version of extensionality
-- (for dependent function types) given in PLFA Isomorphism.

-- PLFA exercise: a version of 'filter' for decidable predicates

-- filter? : ∀ {A : Set} {P : A → Set}
--   → (P? : Decidable P) → List A → ∃[ ys ]( All P ys )
-- filter? P? xs = {!!}
-}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


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

variable  -- WORKS if replaced by postulate
  a : A

module _ (p : P a) (let q = p) where

  postulate r : Q q

-- Panic: unbound variable q (id: 18@787003719158301342)
-- when checking that the expression q has type P _a_12

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Level
open import Relation.Unary using (Pred)
open import Data.Product hiding (swap; curry)
open import Data.List
open import Data.List.Relation.Unary.All as All
open import Data.List.Relation.Unary.Any
open import Data.List.Membership.Propositional
open import Data.List.Prefix
open import Function as Fun using (case_of_)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

import Experiments.Category as Cat

module Experiments.StrongMonad
  (Type : Set)
  (Val : Type → Cat.MP₀ (⊑-preorder {A = Type}))
  (funext : ∀ {a b} → Extensionality a b) where

open import Relation.Binary.PropositionalEquality.Extensionality funext

open Cat (⊑-preorder {A = Type})
open Product

World = List Type

Store : World → Set
Store Σ = All (λ a → Val a · Σ) Σ

import Relation.Binary.HeterogeneousEquality as H
module HR = H.≅-Reasoning

mcong : ∀ {Σₛ Σ Σ' ℓ}{P : MP ℓ}
        {μ : Store Σ}{μ' : Store Σ'}{p : Σ ⊒ Σₛ}{p' : Σ' ⊒ Σₛ}{q : P · Σ}{q' : P · Σ'} →
        Σ ≡ Σ' → p H.≅ p' → μ H.≅ μ' → q H.≅ q' → (Σ , p , μ , q) ≡ (Σ' , p' , μ' , q')
mcong refl H.refl H.refl H.refl = refl

-- The monad takes monotone predicates over worlds
-- to monotone functions over stores in these worlds.
M : ∀ {ℓ} → MP ℓ → MP ℓ
M P = mp (λ Σ → ∀ Σ₁ → (ext : Σ ⊑ Σ₁) → (μ : Store Σ₁) → ∃ λ Σ₂ → Σ₂ ⊒ Σ₁ × Store Σ₂ × P · Σ₂)
  record {
    monotone = λ w₀ f Σ w₁ μ → f Σ (⊑-trans w₀ w₁) μ ;
    monotone-refl = λ f → funext³ (λ Σ₁ _ μ → cong (λ u → f Σ₁ u μ) ⊑-trans-refl) ;
    monotone-trans = λ f w₀ w₁ → funext³ (λ Σ₁ w₂ μ → cong (λ u → f Σ₁ u μ) (sym ⊑-trans-assoc))
  }

-- η is the natural transformation between the identity functor and the functor M
η : ∀ {p}(P : MP p) → P ⇒ M P
η P =
  mk⇒
    (λ p Σ ext μ → Σ , ⊑-refl , μ , MP.monotone P ext p)
    (λ c~c' {p} → begin
      (λ z ext μ → z , ⊑-refl , μ , MP.monotone P ext (MP.monotone P c~c' p))
        ≡⟨ funext³ (λ z ext μ → cong (λ u → z , ⊑-refl , μ , u) (sym (MP.monotone-trans P p c~c' ext))) ⟩
      (λ z ext μ → z , ⊑-refl , μ , MP.monotone P (⊑-trans c~c' ext) p)
        ≡⟨ refl ⟩
      MP.monotone (M P) c~c' (λ z ext μ → z , ⊑-refl , μ , MP.monotone P ext p)
    ∎)

μ : ∀ {p}(P : MP p) → M (M P) ⇒ M P
μ P = mk⇒
  (λ pc Σ₁ ext μ →
    case pc Σ₁ ext μ of λ{
      (Σ₂ , ext₁ , μ₁ , f) →
        case f Σ₂ ⊑-refl μ₁ of λ{
          (Σ₃ , ext₂ , μ₂ , v) → Σ₃ , ⊑-trans ext₁ ext₂ , μ₂ , v
        }
    })
  (λ c~c' → refl)

fmap : ∀ {p q}{P : MP p}{Q : MP q} → (P ⇒ Q) → M P ⇒ M Q
fmap F = mk⇒
  (λ x Σ₁ ext μ → case x Σ₁ ext μ of λ{
    (Σ₂ , ext₁ , μ₁ , v) → Σ₂ , ext₁ , μ₁ , apply F v
  })
  (λ c~c' → refl)

bind : ∀ {p q}{P : MP p}(Q : MP q) → (P ⇒ M Q) → M P ⇒ M Q
bind Q F = μ Q ∘ fmap F

open Exponential (sym ⊑-trans-assoc) ⊑-trans-refl ⊑-trans-refl'

module Coherence where
  -- We prove that η is the component of a natural transformation between the functors
  -- 𝕀 and M where 𝕀 is the identity functor.
  η-natural : ∀ {p q}(P : MP p)(Q : MP q)(F : P ⇒ Q) → η Q ∘ F ⇒≡ (fmap F) ∘ η P
  η-natural P Q F p =
    begin
      apply (η Q ∘ F) p
        ≡⟨ refl ⟩
      apply (η Q) (apply F p)
        ≡⟨ refl ⟩
      (λ Σ ext μ → Σ , ⊑-refl , μ , MP.monotone Q ext (apply F p))
        ≡⟨ funext³ (λ Σ ext μ → cong (λ u → Σ , ⊑-refl , μ , u) (sym (monotone-comm F ext))) ⟩
      (λ Σ ext μ → Σ , ⊑-refl , μ , apply F (MP.monotone P ext p))
        ≡⟨ refl ⟩
      apply (fmap F) (λ Σ ext μ → Σ , ⊑-refl , μ , MP.monotone P ext p)
        ≡⟨ refl ⟩
      apply (fmap F) (apply (η P) p)
        ≡⟨ refl ⟩
      apply (fmap F ∘ η P) p
    ∎

  -- We prove that μ is the component of a natural transformation between
  -- the functors M² and M.
  μ-natural : ∀ {p q}(P : MP p)(Q : MP q)(F : P ⇒ Q) → μ Q ∘ (fmap (fmap F)) ⇒≡ (fmap F) ∘ μ P
  μ-natural P Q F = λ p → refl

  -- from these facts we can prove the monad laws
  left-id : ∀ {p}{P : MP p} → μ P ∘ fmap (η P) ⇒≡ id (M P)
  left-id {P = P} p = funext³
    λ Σ₁ ext μ₁ → mcong {P = P} refl (lem refl) H.refl (H.≡-to-≅ (MP.monotone-refl P _))
    where
      lem : ∀ {Σ Σ' Σ'' : World}{xs : Σ'' ⊒ Σ'}{ys : Σ'' ⊒ Σ} → Σ ≡ Σ' →  ⊑-trans xs ⊑-refl H.≅ ys
      lem {xs = xs}{ys} refl with ⊑-unique xs ys
      ... | refl = H.≡-to-≅ ⊑-trans-refl'

  right-id : ∀ {p}{P : MP p} → μ P ∘ (η (M P)) ⇒≡ id (M P)
  right-id {P = P} p = funext³ λ Σ₁ ext μ₁ →
    let f = (λ{(Σ₃ , ext₂ , μ₂ , v) → Σ₃ , ⊑-trans ⊑-refl ext₂ , μ₂ , v}) in
      trans
        (cong f (cong (λ u → p Σ₁ u μ₁) ⊑-trans-refl'))
        (mcong {P = P} refl (H.≡-to-≅ ⊑-trans-refl) H.refl H.refl )

  -- if we have a (M³ P) then it doesn't matter if we join
  -- the outer or inner ones first.
  assoc : ∀ {p}{P : MP p} → μ P ∘ (fmap (μ P)) ⇒≡ μ P ∘ μ (M P)
  assoc {P = P} p = funext³ λ Σ₁ ext μ → mcong {P = P} refl (H.≡-to-≅ ⊑-trans-assoc) H.refl H.refl

  -- fmap makes M a functor
  fmap-id : ∀ {ℓ}{P : MP ℓ} → fmap (id P) ⇒≡ id (M P)
  fmap-id = λ p → refl

  fmap-∘ : ∀ {ℓ₁ ℓ₂ ℓ₃}{P : MP ℓ₁}{Q : MP ℓ₂}{R : MP ℓ₃}(F : P ⇒ Q)(G : Q ⇒ R) →
           fmap (G ∘ F) ⇒≡ fmap G ∘ fmap F
  fmap-∘ F G = λ p → refl

module Strong where
  -- tensorial strength
  ts : ∀ {p q}(P : MP p)(Q : MP q) → P ⊗ M Q ⇒ M (P ⊗ Q)
  ts P Q = mk⇒
    (λ x Σ₁ ext μ →
      case (proj₂ x) Σ₁ ext μ of λ{
        (_ , ext₁ , μ₁ , v ) → _ , ext₁ , μ₁ , (MP.monotone P (⊑-trans ext ext₁) (proj₁ x)) , v
      }
    )
    (λ c~c' →
      funext³ λ Σ₁ ext μ₁ →
      mcong {P = (P ⊗ Q)} refl H.refl H.refl (
        H.cong₂ {A = P · _}{B = λ _ → Q · _} (λ u v → u , v)
          (H.≡-to-≅ (begin
            MP.monotone P (⊑-trans ext _) _
              ≡⟨ (MP.monotone-trans P _ _ _) ⟩
            MP.monotone P _ (MP.monotone P ext (MP.monotone P c~c' _))
              ≡⟨ cong (λ x → MP.monotone P _ x) (sym ((MP.monotone-trans P _ _ _))) ⟩
            MP.monotone P _ (MP.monotone P (⊑-trans c~c' ext) _)
              ≡⟨ sym ((MP.monotone-trans P _ _ _)) ⟩
            MP.monotone P (⊑-trans (⊑-trans c~c' ext) _) _
          ∎))
          H.refl
      ))

  ts' : ∀ {p q}(P : MP p)(Q : MP q) → M P ⊗ Q ⇒ M (P ⊗ Q)
  ts' P Q = fmap (swap Q P) ∘ ts Q P ∘ swap _ _

  diagram₁ : ∀ {ℓ}{P : MP ℓ} → fmap {P = ⊤ ⊗ P} (π₂ {P = ⊤}) ∘ ts ⊤ P ⇒≡ π₂ {P = ⊤}
  diagram₁ = λ p → refl

  diagram₂ : ∀ {ℓ₁ ℓ₂ ℓ₃}{A : MP ℓ₁}{B : MP ℓ₂}{C : MP ℓ₃} →
            fmap (comm A B C) ∘ ts (A ⊗ B) C ⇒≡ ts A (B ⊗ C) ∘ xmap (id A) (ts B C) ∘ comm A B (M C)
  diagram₂ = λ p → refl

  diagram₃ : ∀ {ℓ₁ ℓ₂}(A : MP ℓ₁)(B : MP ℓ₂) →
             η (A ⊗ B) ⇒≡ ts A B ∘ xmap (id A) (η B)
  diagram₃ A B (a , b) = funext³ λ Σ ext r → mcong {P = A ⊗ B} refl H.refl H.refl
    (H.≡-to-≅
      (cong₂ _,_
        (cong₂
          (λ ext a → MP.monotone A ext a)
          (trans (sym ⊑-trans-refl') (cong (λ r → ⊑-trans ext r) refl))
          refl
        )
        (cong (λ x → x) refl)))

  diagram₄ : ∀ {ℓ₁ ℓ₂}{A : MP ℓ₁}{B : MP ℓ₂} →
            ts A B ∘ xmap (id A) (μ B) ⇒≡ μ (A ⊗ B) ∘ fmap (ts A B) ∘ ts A (M B)
  diagram₄ {A = A}{B} p@(l , r) =
    funext³ λ Σ₁ ext μ' →
      mcong {P = A ⊗ B} refl H.refl H.refl (
        H.cong (Fun.flip _,_ _)
          (H.≡-to-≅ (
            trans
              (cong (λ u → MP.monotone A u l) ⊑-trans-assoc)
              (trans
                (MP.monotone-trans A l (⊑-trans ext _) _)
                (cong
                  (λ u → MP.monotone A u (MP.monotone A (⊑-trans _ _) l))
                  (sym ⊑-trans-refl))))))

  -- internal fmap
  fmap' : ∀ {p q}{P : MP p}{Q : MP q} → (Q ^ P) ⇒ (M Q) ^ (M P)
  fmap' {P = P}{Q} = curry (fmap ε ∘ ts (Q ^ P) P)

  -- internal bind
  bind' : ∀ {p q}{P : MP p}(Q : MP q) → (M P ⊗ (M Q ^ P)) ⇒ M Q
  bind' {P = P} Q =
    μ Q
    ∘ fmap (ε ∘ swap P (M Q ^ P))
    ∘ ts' P (M Q ^ P)


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

postulate Y : Set

module Inner (X : Set) where

  module M (A : Set) where
    postulate R : Set

    module R (r : R) where
      postulate C : Set

  open module MX = M Y

  module M' (r : R) where
    open module Rr = R r

    c : C
    c = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module SizedTypesLoopDueInadmissibility where

postulate
  Size : Set
  _^   : Size -> Size
  ∞    : Size

{-# BUILTIN SIZE Size  #-}
{-# BUILTIN SIZESUC _^ #-}
{-# BUILTIN SIZEINF ∞  #-}

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {size ^}
  suc  : {size : Size} -> Nat {size} -> Nat {size ^}

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A -> Maybe A

shift_case : {i : Size} -> Maybe (Nat {i ^}) -> Maybe (Nat {i})
shift_case nothing = nothing
shift_case (just zero) = nothing
shift_case (just (suc x)) = just x

shift  : {i : Size} -> (Nat -> Maybe (Nat {i ^})) ->
                       (Nat -> Maybe (Nat {i}))
shift f n = shift_case (f (suc n))

inc : Nat -> Maybe Nat
inc n = just (suc n)

-- the type of the following recursive function should be rejected!!
-- it is inadmissible (see Abel, RAIRO 2004 or CSL 2006)
loop : {i : Size} -> Nat {i} -> (Nat -> Maybe (Nat {i})) -> Set
loop (suc n) f = loop n (shift f)
loop zero f with (f zero)
... | nothing = Nat
... | (just zero) = Nat
... | (just (suc y)) = loop y (shift f)

{-
mutual

  loop : {i : Size} -> Nat {i} -> (Nat -> Maybe (Nat {i})) -> Set
  loop .{i ^} (suc {i} n) f = loop {i} n (shift {i} f)
  loop .{i ^} (zero {i}) f = loop_case {i ^} (f zero) f

  loop_case : {i : Size} -> Maybe (Nat {i}) -> (Nat -> Maybe (Nat {i})) -> Set
  loop_case nothing f = Nat
  loop_case (just zero) f = Nat
  loop_case (just (suc y)) f = loop y (shift f)
-}

diverge = loop zero inc

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
------------------------------------------------------------------------
-- Some definitions related to and properties of booleans
------------------------------------------------------------------------

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

open import Equality

module Bool
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Logical-equivalence using (_⇔_)
open import Prelude hiding (id; _∘_; swap)

open import Bijection eq as Bijection using (_↔_)
open Derived-definitions-and-properties eq
open import Equality.Decision-procedures eq
open import Equivalence eq using (_≃_; ↔⇒≃; lift-equality)
open import Function-universe eq
open import H-level eq
open import H-level.Closure eq

-- The not function is involutive.

not-involutive : (b : Bool) → not (not b) ≡ b
not-involutive true  = refl _
not-involutive false = refl _

-- Bool is isomorphic to Fin 2.

Bool↔Fin2 : Bool ↔ Fin 2
Bool↔Fin2 =
  ⊤ ⊎ ⊤      ↝⟨ inverse $ id ⊎-cong ⊎-right-identity ⟩□
  ⊤ ⊎ ⊤ ⊎ ⊥  □

-- A non-trivial automorphism on Bool.

swap : Bool ↔ Bool
swap = record
  { surjection = record
    { logical-equivalence = record
      { to   = not
      ; from = not
      }
    ; right-inverse-of = not-involutive
    }
  ; left-inverse-of = not-involutive
  }

private

  non-trivial : _↔_.to swap ≢ id
  non-trivial not≡id = Bool.true≢false (cong (_$ false) not≡id)

-- Equality rearrangement lemmas.

not≡⇒≢ : (b₁ b₂ : Bool) → not b₁ ≡ b₂ → b₁ ≢ b₂
not≡⇒≢ true  true  f≡t _   = Bool.true≢false (sym f≡t)
not≡⇒≢ true  false _   t≡f = Bool.true≢false t≡f
not≡⇒≢ false true  _   f≡t = Bool.true≢false (sym f≡t)
not≡⇒≢ false false t≡f _   = Bool.true≢false t≡f

≢⇒not≡ : (b₁ b₂ : Bool) → b₁ ≢ b₂ → not b₁ ≡ b₂
≢⇒not≡ true  true  t≢t = ⊥-elim (t≢t (refl _))
≢⇒not≡ true  false _   = refl _
≢⇒not≡ false true  _   = refl _
≢⇒not≡ false false f≢f = ⊥-elim (f≢f (refl _))

not≡↔≡not : {b₁ b₂ : Bool} → not b₁ ≡ b₂ ↔ b₁ ≡ not b₂
not≡↔≡not {true} {true} =
  false ≡ true  ↝⟨ inverse $ Bijection.⊥↔uninhabited (Bool.true≢false ∘ sym) ⟩
  ⊥₀            ↝⟨ Bijection.⊥↔uninhabited Bool.true≢false ⟩□
  true ≡ false  □
not≡↔≡not {true} {false} =
  false ≡ false  ↝⟨ inverse Bijection.≡↔inj₂≡inj₂ ⟩
  tt ≡ tt        ↝⟨ Bijection.≡↔inj₁≡inj₁ ⟩□
  true ≡ true    □
not≡↔≡not {false} {true} =
  true ≡ true    ↝⟨ inverse Bijection.≡↔inj₁≡inj₁ ⟩
  tt ≡ tt        ↝⟨ Bijection.≡↔inj₂≡inj₂ ⟩□
  false ≡ false  □
not≡↔≡not {false} {false} =
  true ≡ false  ↝⟨ inverse $ Bijection.⊥↔uninhabited Bool.true≢false ⟩
  ⊥₀            ↝⟨ Bijection.⊥↔uninhabited (Bool.true≢false ∘ sym) ⟩□
  false ≡ true  □

-- Some lemmas related to T.

T↔≡true : {b : Bool} → T b ↔ b ≡ true
T↔≡true {false} =   $⟨ Bool.true≢false ⟩
  true ≢ false      ↝⟨ (_∘ sym) ⟩
  false ≢ true      ↝⟨ Bijection.⊥↔uninhabited ⟩□
  ⊥ ↔ false ≡ true  □
T↔≡true {true} =              $⟨ refl true ⟩
  true ≡ true                 ↝⟨ propositional⇒inhabited⇒contractible Bool-set ⟩
  Contractible (true ≡ true)  ↝⟨ _⇔_.to contractible⇔↔⊤ ⟩
  true ≡ true ↔ ⊤             ↝⟨ inverse ⟩□
  ⊤ ↔ true ≡ true             □

T-not↔≡false : ∀ {b} → T (not b) ↔ b ≡ false
T-not↔≡false {b} =
  T (not b)     ↝⟨ T↔≡true ⟩
  not b ≡ true  ↝⟨ not≡↔≡not ⟩□
  b ≡ false     □

T-not⇔¬T :
  (b : Bool) → T (not b) ⇔ ¬ T b
T-not⇔¬T true =
  ⊥        ↔⟨ Bijection.⊥↔uninhabited (_$ _) ⟩
  (⊤ → ⊥)  □
T-not⇔¬T false =
  ⊤    ↝⟨ record { to = λ _ → id } ⟩□
  ¬ ⊥  □

T-not↔¬T : (b : Bool) → T (not b) ↝[ lzero ∣ lzero ] ¬ T b
T-not↔¬T true _ =
  ⊥        ↔⟨ Bijection.⊥↔uninhabited (_$ _) ⟩
  (⊤ → ⊥)  □
T-not↔¬T false ext =
  ⊤    ↝⟨ inverse-ext? ¬⊥↔⊤ ext ⟩□
  ¬ ⊥  □

¬T⇔≡false : ∀ {b} → ¬ T b ⇔ b ≡ false
¬T⇔≡false {b} =
  ¬ T b      ↝⟨ inverse $ T-not⇔¬T b ⟩
  T (not b)  ↔⟨ T-not↔≡false ⟩□
  b ≡ false  □

¬T↔≡false : ∀ {b} → ¬ T b ↝[ lzero ∣ lzero ] b ≡ false
¬T↔≡false {b = b} ext =
  ¬ T b      ↝⟨ inverse-ext? (T-not↔¬T b) ext ⟩
  T (not b)  ↔⟨ T-not↔≡false ⟩□
  b ≡ false  □

T-∧↔T×T : ∀ b₁ {b₂} → T (b₁ ∧ b₂) ↔ T b₁ × T b₂
T-∧↔T×T true {b₂} =
  T b₂      ↝⟨ inverse ×-left-identity ⟩□
  ⊤ × T b₂  □
T-∧↔T×T false {b₂} =
  ⊥         ↝⟨ inverse ×-left-zero ⟩□
  ⊥ × T b₂  □

T-∨⇔T⊎T : ∀ b₁ {b₂} → T (b₁ ∨ b₂) ⇔ T b₁ ⊎ T b₂
T-∨⇔T⊎T true       = record { to = inj₁ }
T-∨⇔T⊎T false {b₂} =
  T b₂      ↔⟨ inverse ⊎-left-identity ⟩□
  ⊥ ⊎ T b₂  □

-- Bool ≃ Bool is isomorphic to Bool (assuming extensionality).

[Bool≃Bool]↔Bool₁ : Extensionality lzero lzero →
                    (Bool ≃ Bool) ↔ Bool
[Bool≃Bool]↔Bool₁ ext = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ eq → _≃_.to eq true
      ; from = if_then id else ↔⇒≃ swap
      }
    ; right-inverse-of = λ { true → refl _; false → refl _ }
    }
  ; left-inverse-of = λ eq →
      lift-equality ext (apply-ext ext (lemma₂ eq))
  }
  where
  lemma₁ : ∀ b → _≃_.to (if b then id else ↔⇒≃ swap) false ≡ not b
  lemma₁ true  = refl _
  lemma₁ false = refl _

  lemma₂ : ∀ eq b →
           _≃_.to (if _≃_.to eq true then id else ↔⇒≃ swap) b ≡
           _≃_.to eq b
  lemma₂ eq true  with _≃_.to eq true
  ...             | true  = refl _
  ...             | false = refl _
  lemma₂ eq false =
    _≃_.to (if _≃_.to eq true then id else ↔⇒≃ swap) false  ≡⟨ lemma₁ (_≃_.to eq true) ⟩
    not (_≃_.to eq true)                                    ≡⟨ ≢⇒not≡ _ _ (Bool.true≢false ∘ _≃_.injective eq) ⟩∎
    _≃_.to eq false                                         ∎

-- Another proof showing that Bool ≃ Bool is isomorphic to Bool
-- (assuming extensionality).

[Bool≃Bool]↔Bool₂ : Extensionality lzero lzero →
                    (Bool ≃ Bool) ↔ Bool
[Bool≃Bool]↔Bool₂ ext = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ eq → _≃_.to eq false
      ; from = if_then ↔⇒≃ swap else id
      }
    ; right-inverse-of = λ { true → refl _; false → refl _ }
    }
  ; left-inverse-of = λ eq →
      lift-equality ext (apply-ext ext (lemma₂ eq))
  }
  where
  lemma₁ : ∀ b → _≃_.to (if b then ↔⇒≃ swap else id) true ≡ not b
  lemma₁ true  = refl _
  lemma₁ false = refl _

  lemma₂ : ∀ eq b →
           _≃_.to (if _≃_.to eq false then ↔⇒≃ swap else id) b ≡
           _≃_.to eq b
  lemma₂ eq false with _≃_.to eq false
  ...             | true  = refl _
  ...             | false = refl _
  lemma₂ eq true  =
    _≃_.to (if _≃_.to eq false then ↔⇒≃ swap else id) true  ≡⟨ lemma₁ (_≃_.to eq false) ⟩
    not (_≃_.to eq false)                                   ≡⟨ ≢⇒not≡ _ _ (Bool.true≢false ∘ sym ∘ _≃_.injective eq) ⟩∎
    _≃_.to eq true                                          ∎

private

  -- The two proofs are not equal.

  distinct : {ext : Extensionality lzero lzero} →
             [Bool≃Bool]↔Bool₁ ext ≢ [Bool≃Bool]↔Bool₂ ext
  distinct =
    Bool.true≢false ∘ cong (λ iso → _≃_.to (_↔_.from iso true) true)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
postulate
  A : Set

open import Agda.Builtin.Equality

foo : (f : A → A → A) (@0 g : @0 A → @0 A → A)
    → @0 _≡_ {A = @0 A → @0 A → A} g (\ x y → f y x)
    → @0 A → @0 A → A
foo f g refl = g
  -- In the goal, `C-c C-n g` gives
  -- λ (@0 x) (@0 y) → f y x
  -- which is only well-typed in an erased context.

bad : (f : A → A → A) → @0 A → @0 A → A
bad f = foo f (\ x y → f y x) refl


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Sum.Base where

open import Cubical.Core.Everything

private
  variable
    ℓ ℓ' : Level
    A B C D : Type ℓ

data _⊎_ (A : Type ℓ)(B : Type ℓ') : Type (ℓ-max ℓ ℓ') where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

elim-⊎ : {C : A ⊎ B → Type ℓ} →  ((a : A) → C (inl a)) → ((b : B) → C (inr b))
       → (x : A ⊎ B) → C x
elim-⊎ f _ (inl x) = f x
elim-⊎ _ g (inr y) = g y

map-⊎ : (A → C) → (B → D) → A ⊎ B → C ⊎ D
map-⊎ f _ (inl x) = inl (f x)
map-⊎ _ g (inr y) = inr (g y)

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

open import Cubical.Data.Int hiding (_+_)
open import Cubical.Data.Bool
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Univalence
open import Cubical.HITs.S1
open import Cubical.HITs.S3
open import Cubical.Data.Nat
open import Cubical.Data.Prod
open import Cubical.HITs.Sn.Base
open import Cubical.HITs.Susp
open import Cubical.Data.Unit
open import Cubical.HITs.Join
open import Cubical.HITs.Pushout
open import Cubical.HITs.SmashProduct
open import Cubical.HITs.PropositionalTruncation

open Iso

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : Type ℓ'

--- Some silly lemmas on S1 ---

isGroupoidS1 : isGroupoid (S₊ 1)
isGroupoidS1 = isGroupoidS¹

isConnectedS1 : (x : S₊ 1) → ∥ base ≡ x ∥
isConnectedS1 = isConnectedS¹

max_stars_repo_name: mchristianl/cubical

max_issues_repo_name: mchristianl/cubical

max_forks_repo_name: aljungstrom/cubical


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

open import Agda.Primitive
open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Glue
open import Agda.Builtin.Bool

-- If primGlue does not reduce away we should report an error for
-- patterns of other types.
--
-- In the future we might want to allow the constructor glue itself as
-- a pattern.
test : ∀ φ → primGlue {ℓ' = lzero} Bool {φ = φ} ? ? → Bool
test _ true = ?
test _ false = ?


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Values for caching evaluation of MTerm
------------------------------------------------------------------------
import Parametric.Syntax.Type as Type
import Parametric.Syntax.MType as MType

import Parametric.Denotation.Value as Value
import Parametric.Denotation.MValue as MValue

module Parametric.Denotation.CachingMValue
    (Base : Type.Structure)
    (⟦_⟧Base : Value.Structure Base)
  where

open import Base.Data.DependentList
open import Base.Denotation.Notation

open Type.Structure Base
open MType.Structure Base
open Value.Structure Base ⟦_⟧Base
open MValue.Structure Base ⟦_⟧Base

open import Data.Product hiding (map)
open import Data.Sum hiding (map)
open import Data.Unit
open import Level
open import Function hiding (const)

Structure : Set
Structure = Base → Type

module Structure (ΔBase : Structure) where
  {-# TERMINATING #-}
  ⟦_⟧ValTypeHidCache : (τ : ValType) → Set
  ⟦_⟧CompTypeHidCache : (τ : CompType) → Set

  ⟦ U c ⟧ValTypeHidCache = ⟦ c ⟧CompTypeHidCache
  ⟦ B ι ⟧ValTypeHidCache = ⟦ base ι ⟧
  ⟦ vUnit ⟧ValTypeHidCache = ⊤
  ⟦ τ₁ v× τ₂ ⟧ValTypeHidCache = ⟦ τ₁ ⟧ValTypeHidCache × ⟦ τ₂ ⟧ValTypeHidCache
  ⟦ τ₁ v+ τ₂ ⟧ValTypeHidCache = ⟦ τ₁ ⟧ValTypeHidCache ⊎ ⟦ τ₂ ⟧ValTypeHidCache

  --
  -- XXX The termination checker isn't happy with it, and it may be right ─ if
  -- you keep substituting τ₁ = U (F τ), you can make the cache arbitrarily big.
  -- I think we don't do that unless we are caching a non-terminating
  -- computation to begin with, but I'm not entirely sure.
  --
  -- However, the termination checker can't prove that the function is
  -- terminating because it's not structurally recursive, but one call of the
  -- function will produce another call of the function stuck on a neutral term:
  -- So the computation will have terminated, just in an unusual way!
  --
  -- Anyway, I need not mechanize this part of the proof for my goals.
  --
  -- XXX: This line is the only change, up to now, for the caching semantics,
  -- the rest is copied. Inheritance would handle this precisely; without
  -- inheritance, we might want to use one of the standard encodings of related
  -- features (delegation?).
  ⟦ F τ ⟧CompTypeHidCache = (Σ[ τ₁ ∈ ValType ] ⟦ τ ⟧ValTypeHidCache × ⟦ τ₁ ⟧ValTypeHidCache )
  ⟦ σ ⇛ τ ⟧CompTypeHidCache = ⟦ σ ⟧ValTypeHidCache → ⟦ τ ⟧CompTypeHidCache

  ⟦_⟧ValCtxHidCache : (Γ : ValContext) → Set
  ⟦_⟧ValCtxHidCache = DependentList ⟦_⟧ValTypeHidCache

  {-# TERMINATING #-}
  ⟦_⟧ΔValType : ValType → Set
  ⟦_⟧ΔCompType : CompType → Set
  ⟦_⟧ΔCompType (F τ) = Σ[ τ₁ ∈ ValType ] (⟦ τ₁ ⟧ValTypeHidCache → ⟦ τ ⟧ΔValType × ⟦ τ₁ ⟧ValTypeHidCache)
  ⟦_⟧ΔCompType (σ ⇛ τ) = ⟦ σ ⟧ΔValType → ⟦ τ ⟧ΔCompType

  ⟦_⟧ΔValType (U c) = ⟦ c ⟧ΔCompType
  ⟦_⟧ΔValType (B ι) = ⟦ ΔBase ι ⟧
  ⟦_⟧ΔValType vUnit = ⊤
  ⟦_⟧ΔValType (τ₁ v× τ₂) = ⟦_⟧ΔValType τ₁ × ⟦_⟧ΔValType τ₂
  ⟦_⟧ΔValType (τ₁ v+ τ₂) = (⟦_⟧ΔValType τ₁ ⊎ ⟦_⟧ΔValType τ₂) ⊎ (⟦ τ₁ ⟧ ⊎ ⟦ τ₂ ⟧)

open import Data.Product
open import Level

-- -- Needed to allow storing functions in cache:
-- record _↝_↝_ {a b} (S : Set a) c (T : Set b) : Set (a ⊔ b ⊔ suc c) where
--   field
--     cache : Set c
--     fun : S → (T × cache)

-- record _↝′_↝′_ {a b} (dS : Set a) c (dT : Set b) : Set (a ⊔ b ⊔ suc c) where
--   field
--     cache : Set c
--     fun : dS → cache → (dT × cache)

-- -- -- For simplicity, but won't work:
-- --
-- -- record _↝_ {a b} (S : Set a) (T : Set b) : Set (a ⊔ b ⊔ suc zero) where
-- --   field
-- --     cache : Set
-- --     fun : S → (T × cache)
-- -- record _↝′_ (da : Set₁) (db : Set₁) : Set₁ where
-- --   field
-- --     cache : Set
-- --     dfun : da → cache → (db × cache)

-- fooo : (a b : Set₁) → Set₁
-- fooo a b = a ↝ zero ↝ (b ↝ zero ↝ b)

-- dfooo : (da db : Set₁) → Set₁
-- dfooo da db = da ↝′ zero ↝′ (db ↝′ zero ↝′ db)

-- Since caches can contain caches, including function caches, we can't use the
-- above. The existentials must store object-language codes of some sort. For
-- extra fun, the resulting code is not typeable with simple types, so we can't
-- use codes for simple types but must store, say, function bodies.

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:
open import Relation.Binary.Core

module PLRTree.Insert.Properties {A : Set}
                     (_≤_ : A → A → Set)
                     (tot≤ : Total _≤_) where

open import Data.Sum
open import PLRTree {A}
open import PLRTree.Compound {A}
open import PLRTree.Insert _≤_ tot≤

lemma-insert-compound : (x : A)(t : PLRTree) → Compound (insert x t)
lemma-insert-compound x leaf = compound
lemma-insert-compound x (node perfect y l r)
    with tot≤ x y | l | r
... | inj₁ x≤y | leaf | leaf = compound
... | inj₁ x≤y | leaf | node _ _ _ _ = compound
... | inj₁ x≤y | node _ _ _ _ | leaf = compound
... | inj₁ x≤y | node _ _ _ _ | node _ _ _ _ = compound
... | inj₂ y≤x | leaf | leaf = compound
... | inj₂ y≤x | leaf | node _ _ _ _ = compound
... | inj₂ y≤x | node _ _ _ _ | leaf = compound
... | inj₂ y≤x | node _ _ _ _ | node _ _ _ _ = compound
lemma-insert-compound x (node left y l _)
    with tot≤ x y
... | inj₁ x≤y
    with insert y l | lemma-insert-compound y l
... | node perfect _ _ _ | compound = compound
... | node left _ _ _ | compound = compound
... | node right _ _ _ | compound = compound
lemma-insert-compound x (node left y l _) | inj₂ y≤x
    with insert x l | lemma-insert-compound x l
... | node perfect _ _ _ | compound = compound
... | node left _ _ _ | compound = compound
... | node right _ _ _ | compound = compound
lemma-insert-compound x (node right y _ r)
    with tot≤ x y
... | inj₁ x≤y
    with insert y r | lemma-insert-compound y r
... | node perfect _ _ _ | compound = compound
... | node left _ _ _ | compound = compound
... | node right _ _ _ | compound = compound
lemma-insert-compound x (node right y _ r) | inj₂ y≤x
    with insert x r | lemma-insert-compound x r
... | node perfect _ _ _ | compound = compound
... | node left _ _ _ | compound = compound
... | node right _ _ _ | compound = compound

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text: -- Placeholder


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Homotopy.WedgeConnectivity where

open import Cubical.Foundations.Everything
open import Cubical.Data.HomotopyGroup
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.HITs.Nullification
open import Cubical.HITs.Susp
open import Cubical.HITs.Truncation as Trunc
open import Cubical.Homotopy.Connected

module WedgeConnectivity {ℓ ℓ' ℓ''} (n m : ℕ)
  (A : Pointed ℓ) (connA : isConnected (suc n) (typ A))
  (B : Pointed ℓ') (connB : isConnected (suc m) (typ B))
  (P : typ A → typ B → TypeOfHLevel ℓ'' (n + m))
  (f : (a : typ A) → P a (pt B) .fst)
  (g : (b : typ B) → P (pt A) b .fst)
  (p : f (pt A) ≡ g (pt B))
  where

  private
    Q : typ A → TypeOfHLevel _ n
    Q a =
      ( (Σ[ k ∈ ((b : typ B) → P a b .fst) ] k (pt B) ≡ f a)
      , isOfHLevelRetract n
          (λ {(h , q) → h , funExt λ _ → q})
          (λ {(h , q) → h , funExt⁻ q _})
          (λ _ → refl)
          (isOfHLevelPrecomposeConnected n m (P a) (λ _ → pt B)
            (isConnectedPoint m connB (pt B)) (λ _ → f a))
      )

    main : isContr (fiber (λ s _ → s (pt A)) (λ _ → g , p ⁻¹))
    main =
      elim.isEquivPrecompose (λ _ → pt A) n Q
        (isConnectedPoint n connA (pt A))
        .equiv-proof (λ _ → g , p ⁻¹)

  extension : ∀ a b → P a b .fst
  extension a b = main .fst .fst a .fst b

  left : ∀ a → extension a (pt B) ≡ f a
  left a = main .fst .fst a .snd

  right : ∀ b → extension (pt A) b ≡ g b
  right = funExt⁻ (cong fst (funExt⁻ (main .fst .snd) _))

    -- TODO: left (pt A) ⁻¹ ∙ right (pt B) ≡ p

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --without-K #-}
-- most of this is subsumed by crypto-agda Search code
open import Type hiding (★)
open import Data.Nat.NP hiding (_==_) renaming (_<=_ to _ℕ<=_)
open import Data.Bits
open import Data.Bit hiding (_==_)
open import Data.Bool.Properties using (not-involutive)
import Data.Vec.NP as V
open V hiding (rewire; rewireTbl; sum) renaming (map to vmap; swap to vswap)

import Relation.Binary.PropositionalEquality.NP as ≡
open ≡
open import Function.NP hiding (_→⟨_⟩_)
open import Algebra.FunctionProperties.NP

module Data.Bits.Search where
module Search {i} {I : ★ i} (`1 : I) (`2*_ : I → I)
              {a} {A : I → ★ a} (_∙_ : ∀ {m} → A m → A m → A (`2* m)) where

  `2^_ : ℕ → I
  `2^_ = fold `1 `2*_

  search : ∀ {n} → (Bits n → A `1) → A (`2^ n)
  search {zero}  f = f []
  search {suc n} f = search (f ∘ 0∷_) ∙ search (f ∘ 1∷_)

  searchBit : (Bit → A `1) → A (`2* `1)
  searchBit f = f 0b ∙ f 1b

  -- search-ext
  search-≗ : ∀ {n} (f g : Bits n → A `1) → f ≗ g → search f ≡ search g
  search-≗ {zero}  f g f≗g = f≗g []
  search-≗ {suc n} f g f≗g
    rewrite search-≗ (f ∘ 0∷_) (g ∘ 0∷_) (f≗g ∘ 0∷_)
          | search-≗ (f ∘ 1∷_) (g ∘ 1∷_) (f≗g ∘ 1∷_) = refl

  module Comm (∙-comm : ∀ {m} (x y : A m) → x ∙ y ≡ y ∙ x) where

    {- This pad bit vector allows to specify which bit do we negate in the vector. -}
    search-comm : ∀ {n} (pad : Bits n) (f : Bits n → A `1) → search f ≡ search (f ∘ _⊕_ pad)
    search-comm {zero} pad f = refl
    search-comm {suc n} (b ∷ pad) f
      rewrite search-comm pad (f ∘ 0∷_)
              | search-comm pad (f ∘ 1∷_)
      with b
    ... | true  = ∙-comm (search (f ∘ 0∷_ ∘ _⊕_ pad)) _
    ... | false = refl
  open Comm public

module SimpleSearch {a} {A : ★ a} (_∙_ : A → A → A) where

    open Search 1 2*_ {A = const A} _∙_ public

    module SearchUnit ε (ε∙ε : ε ∙ ε ≡ ε) where
        search-constε≡ε : ∀ n → search {n = n} (const ε) ≡ ε
        search-constε≡ε zero = refl
        search-constε≡ε (suc n) rewrite search-constε≡ε n = ε∙ε

    searchBit-search : ∀ n (f : Bits (suc n) → A) → searchBit (λ b → search (f ∘ _∷_ b)) ≡ search f
    searchBit-search n f = refl

    search-≗₂ : ∀ {m n} (f g : Bits m → Bits n → A) → f ≗₂ g
                  → search (search ∘ f) ≡ search (search ∘ g)
    search-≗₂ f g f≗g = search-≗ (search ∘ f) (search ∘ g) (λ xs →
                          search-≗ (f xs) (g xs) (λ ys →
                            f≗g xs ys))

    search-+ : ∀ {m n} (f : Bits (m + n) → A) →
                 search {m + n} f
               ≡ search {m} (λ xs → search {n} (λ ys → f (xs ++ ys)))
    search-+ {zero} f = refl
    search-+ {suc m} f rewrite search-+ {m} (f ∘ 0∷_)
                             | search-+ {m} (f ∘ 1∷_) = refl

    module SearchInterchange (∙-interchange : Interchange _≡_ _∙_ _∙_) where

        search-dist : ∀ {n} (f₀ f₁ : Bits n → A) → search (λ x → f₀ x ∙ f₁ x) ≡ search f₀ ∙ search f₁
        search-dist {zero}  _ _ = refl
        search-dist {suc n} f₀ f₁
          rewrite search-dist (f₀ ∘ 0∷_) (f₁ ∘ 0∷_)
                | search-dist (f₀ ∘ 1∷_) (f₁ ∘ 1∷_)
                = ∙-interchange _ _ _ _

        search-searchBit : ∀ {n} (f : Bits (suc n) → A) →
                             search (λ xs → searchBit (λ b → f (b ∷ xs))) ≡ search f
        search-searchBit f = search-dist (f ∘ 0∷_) (f ∘ 1∷_)

        search-search : ∀ {m n} (f : Bits (m + n) → A) →
                          search {m} (λ xs → search {n} (λ ys → f (xs ++ ys)))
                        ≡ search {n} (λ ys → search {m} (λ xs → f (xs ++ ys)))
        search-search {zero} f = refl
        search-search {suc m} {n} f
          rewrite search-search {m} {n} (f ∘ 0∷_)
                | search-search {m} {n} (f ∘ 1∷_)
                | search-searchBit {n} (λ { (b ∷ ys) → search {m} (λ xs → f (b ∷ xs ++ ys)) })
                = refl
        {- -- It might also be done by using search-dist twice and commutativity of addition.
           -- However, this also affect 'f' and makes this proof actually longer.
           search-search {m} {n} f =
                             search {m} (λ xs → search {n} (λ ys → f (xs ++ ys)))
                           ≡⟨ {!!} ⟩
                             search {m + n} f
                           ≡⟨ {!!} ⟩
                             search {n + m} (f ∘ vswap n)
                           ≡⟨ {!!} ⟩
                             search {n} (λ ys → search {m} (λ xs → f (vswap n (ys ++ xs))))
                           ≡⟨ {!!} ⟩
                             search {n} (λ ys → search {m} (λ xs → f (xs ++ ys)))
                           ∎
                           where open ≡-Reasoning
         -}

        search-swap : ∀ {m n} (f : Bits (m + n) → A) → search {n + m} (f ∘ vswap n) ≡ search {m + n} f
        search-swap {m} {n} f =
                     search {n + m} (f ∘ vswap n)
                   ≡⟨ search-+ {n} {m} (f ∘ vswap n) ⟩
                     search {n} (λ ys → search {m} (λ xs → f (vswap n (ys ++ xs))))
                   ≡⟨ search-≗₂ {n} {m}
                                (λ ys → f ∘ vswap n ∘ _++_ ys)
                                (λ ys → f ∘ flip _++_ ys)
                                (λ ys xs → cong f (swap-++ n ys xs)) ⟩
                     search {n} (λ ys → search {m} (λ xs → f (xs ++ ys)))
                   ≡⟨ sym (search-search {m} {n} f) ⟩
                     search {m} (λ xs → search {n} (λ ys → f (xs ++ ys)))
                   ≡⟨ sym (search-+ {m} {n} f) ⟩
                     search {m + n} f
                   ∎ where open ≡-Reasoning

        search-0↔1 : ∀ {n} (f : Bits n → A) → search {n} (f ∘ 0↔1) ≡ search {n} f
        search-0↔1 {zero}        _ = refl
        search-0↔1 {suc zero}    _ = refl
        search-0↔1 {suc (suc n)} _ = ∙-interchange _ _ _ _

    module Bij (∙-comm : Commutative _≡_ _∙_)
              (∙-interchange : Interchange _≡_ _∙_ _∙_) where
        open SearchInterchange ∙-interchange using (search-0↔1)
        open import Data.Bits.OperationSyntax hiding (_∙_)
        search-bij : ∀ {n} f (g : Bits n → A) → search (g ∘ eval f) ≡ search g
        search-bij `id     _ = refl
        search-bij `0↔1    f = search-0↔1 f
        search-bij (f `⁏ g) h
          rewrite search-bij f (h ∘ eval g)
                | search-bij g h
                = refl
        search-bij {suc n} (`id   `∷ f) g
          rewrite search-bij (f 0b) (g ∘ 0∷_)
                | search-bij (f 1b) (g ∘ 1∷_)
                = refl
        search-bij {suc n} (`notᴮ `∷ f) g
          rewrite search-bij (f 1b) (g ∘ 0∷_)
                | search-bij (f 0b) (g ∘ 1∷_)
                = ∙-comm _ _

|de-morgan| : ∀ {n} (f g : Bits n → Bit) → f |∨| g ≗ not ∘ ((not ∘ f) |∧| (not ∘ g))
|de-morgan| f g x with f x
... | true = refl
... | false = sym (not-involutive _)

open SimpleSearch

search-de-morgan : ∀ {n} op (f g : Bits n → Bit) →
                   search op (f |∨| g) ≡ search op (not ∘ ((not ∘ f) |∧| (not ∘ g)))
search-de-morgan op f g = search-≗ op _ _ (|de-morgan| f g)

search-hom :
  ∀ {n a b}
    {A : ★ a} {B : ★ b}
    (_+_ : A → A → A)
    (_*_ : B → B → B)
    (f : A → B)
    (p : Bits n → A)
    (hom : ∀ x y → f (x + y) ≡ f x * f y)
    → f (search _+_ p) ≡ search _*_ (f ∘ p)
search-hom {zero}  _   _   _ _ _   = refl
search-hom {suc n} _+_ _*_ f p hom =
   trans (hom _ _)
         (cong₂ _*_ (search-hom _+_ _*_ f (p ∘ 0∷_) hom)
                    (search-hom _+_ _*_ f (p ∘ 1∷_) hom))

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


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

   Copyright (c) 2020 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 Category.Functor
open import Data.Maybe
open import Function
open import Level
open import Relation.Binary.PropositionalEquality

module Optics.Functorial where

  Lens' : (F : Set → Set) → RawFunctor F → Set → Set → Set
  Lens' F _ S A = (A → F A) → S → F S

  data Lens (S A : Set) : Set₁ where
    lens : ((F : Set → Set)(rf : RawFunctor F) → Lens' F rf S A)
         → Lens S A

  private
    cf : {A : Set} → RawFunctor {Level.zero} (const A)
    cf = record { _<$>_ = λ x x₁ → x₁ }

    if : RawFunctor {Level.zero} id
    if = record { _<$>_ = λ x x₁ → x x₁ }

  -- We can make lenses relatively painlessly without requiring reflection
  -- by providing getter and setter functions
  mkLens' : ∀ {A B : Set}
          → (B → A)
          → (B → A → B)
          → Lens B A
  mkLens' {A} {B} get set =
    lens (λ F rf f b → Category.Functor.RawFunctor._<$>_
                         {F = F} rf
                         {A = A}
                         {B = B}
                         (set b)
                         (f (get b)))

  -- Getter:

  -- this is typed as ^\.
  _^∙_ : ∀{S A} → S → Lens S A → A
  _^∙_ {_} {A} s (lens p) = p (const A) cf id s

   -- Setter:

  set : ∀{S A} → Lens S A → A → S → S
  set (lens p) a s = p id if (const a) s

  infixr 4 _∙~_
  _∙~_ = set

  -- _|>_ is renamed to _&_ by Util.Prelude
  set? : ∀{S A} → Lens S (Maybe A) → A → S → S
  set? l a s = s |> l ∙~ just a

  infixr 4 _?~_
  _?~_ = set?

  -- Modifier:
  over : ∀{S A} → Lens S A → (A → A) → S → S
  over (lens p) f s = p id if f s

  infixr 4 _%~_
  _%~_ = over

  -- Composition
  infixr 30 _∙_
  _∙_ : ∀{S A B} → Lens S A → Lens A B → Lens S B
  (lens p) ∙ (lens q) = lens (λ F rf x x₁ → p F rf (q F rf x) x₁)

  -- Relation between the same field of two states This most general form allows us to specify a
  -- Lens S A, a function A → B, and a relation between two B's, and holds iff the relation holds
  -- between the values yielded by applying the Lens to two S's and then applying the function to
  -- the results; more specific variants are provided below
  _[_]L_f=_at_ : ∀ {ℓ} {S A B : Set} → S → (B → B → Set ℓ) → S → (A → B) → Lens S A → Set ℓ
  s₁ [ _~_ ]L s₂ f= f at l = f (s₁ ^∙ l) ~ f (s₂ ^∙ l)

  _[_]L_at_ : ∀ {ℓ} {S A} → S → (A → A → Set ℓ) → S → Lens S A → Set ℓ
  s₁ [ _~_ ]L s₂ at l = _[_]L_f=_at_ s₁ _~_ s₂ id l

  infix 4 _≡L_f=_at_
  _≡L_f=_at_ : ∀ {S A B : Set} → (s₁ s₂ : S) → (A → B) → Lens S A → Set
  s₁ ≡L s₂ f= f at l = _[_]L_f=_at_ s₁ _≡_ s₂ f l

  infix 4 _≡L_at_
  _≡L_at_ : ∀ {S A} → (s₁ s₂ : S) → Lens S A → Set
  s₁ ≡L s₂ at l = _[_]L_f=_at_ s₁ _≡_ s₂ id l


text:
-- Andreas, 2015-05-28

open import Common.Size

fix : ∀ {C : Size → Set} → (∀ i → (∀ (j : Size< i) → C j) → C i) → ∀ i → C i
fix t i = t i λ (j : Size< i) → fix t j
-- Expected error:
-- Possibly empty type of sizes  (Size< i)
-- when checking that the expression λ (j : Size< i) → fix t j has
-- type (j : Size< i) → .C j


text:
module Main where

open import Category.Functor
open import Category.Monad
open import Data.Unit
open import Data.Container.Indexed
open import Data.Maybe
open import Data.Product
open import IO.Primitive hiding (_>>=_)

open import Signature
open import Sodium
open import Model
open import View

------------------------------------------------------------------------

postulate
  eEvent : Event VtyEvent
  bMode  : Behaviour Mode

eCommand : Event (∃ (Command Hårss))
eCommand = filterJust (snapshot (λ v m → forget (vtyToCmd v m))
                                eEvent bMode)
  where
  forget : ∀ {m} → Maybe (Command Hårss m) → Maybe (∃ (Command Hårss))
  forget nothing  = nothing
  forget (just c) = just (_ , c)

eResponse : Event (∃₂ λ m (c : Command Hårss m) → Response Hårss c)
eResponse = executeAsyncIO (snapshot
  (λ c m → fmap (forget c) (cmdToResp (proj₂ c) m)) eCommand bModel)
  where
  forget : (c : ∃ (Command Hårss)) → Response Hårss (proj₂ c) →
           ∃₂ λ m (c : Command Hårss m) → Response Hårss c
  forget (m , c) r = m , (c , r)

  postulate
    fmap : ∀ {A B} → (A → B) → IO A → IO B
    bModel : Behaviour Model

bModel : Reactive (Behaviour Model)
bModel = accum initialModel (update <$> eResponse)
  where
  open RawFunctor eventFunctor

  update : (∃₂ λ m (c : Command Hårss m) →
           (Response Hårss c)) → Model → Model
  update (._ , moveP d    , _)        m = moveModel d m
  update (._ , promptP p  , _)        m = setMode (input p) m
  update (._ , putCharP c , _)        m = addCharToBuffer c m
  update (._ , doneP , (s , search))  m = searchModel s m
  update (._ , doneP , (s , addFeed)) m = addFeedToModel s m
  update (._ , fetchP     , f)        m = setCurrentFeed m f
  update (._ , searchNextP , s)       m = searchNextModel s m

setup : Reactive (IO ⊤)
setup =
  bModel >>= λ m →
  listen (updates m) view
  where
  open RawMonad reactiveMonad

max_stars_repo_name: stevana/haarss

max_issues_repo_name: stevana/haarss

max_forks_repo_name: stevana/haarss


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

module Data.Binary.Operations.Multiplication where

open import Data.Binary.Definitions
open import Data.Binary.Operations.Addition

mul : 𝔹⁺ → 𝔹⁺ → 𝔹⁺
mul 1ᵇ ys = ys
mul (O ∷ xs) ys = O ∷ (mul xs ys)
mul (I ∷ xs) ys = add O (O ∷ mul ys xs) ys

_*_ :  𝔹 → 𝔹 → 𝔹
0ᵇ * ys = 0ᵇ
(0< _) * 0ᵇ = 0ᵇ
(0< xs) * (0< ys) = 0< mul xs ys
{-# INLINE _*_ #-}

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


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

open import Base

module Homotopy.Cover.Def {i} (A : Set i) where

record covering : Set (suc i) where
  constructor cov[_,_]
  field
    fiber : A → Set i
    fiber-is-set : ∀ a → is-set (fiber a)

open import Homotopy.Truncation
open import Homotopy.Connected
open import Homotopy.PathTruncation

-- In terms of connectedness
is-universal : covering → Set i
is-universal cov[ fiber , _ ] = is-connected ⟨1⟩ $ Σ A fiber

-- In terms of connectedness
universal-covering : Set (suc i)
universal-covering = Σ covering is-universal

tracing : ∀ cov → let open covering cov in
  ∀ {a₁ a₂} → fiber a₁ → a₁ ≡₀ a₂ → fiber a₂
tracing cov[ fiber , fiber-is-set ] y =
  π₀-extend-nondep
    ⦃ fiber-is-set _ ⦄
    (λ p → transport fiber p y)

compose-tracing : ∀ cov → let open covering cov in
  ∀ {a₁ a₂ a₃} y (p₁ : a₁ ≡₀ a₂) (p₂ : a₂ ≡₀ a₃)
  → tracing cov (tracing cov y p₁) p₂ ≡ tracing cov y (p₁ ∘₀ p₂)
compose-tracing cov y = let open covering cov in
  π₀-extend
    ⦃ λ _ → Π-is-set λ _ → ≡-is-set $ fiber-is-set _ ⦄
    (λ p₁ → π₀-extend
      ⦃ λ _ → ≡-is-set $ fiber-is-set _ ⦄
      (λ p₂ → compose-trans fiber p₂ p₁ y))

covering-eq : ∀ {co₁ co₂ : covering}
  → covering.fiber co₁ ≡ covering.fiber co₂
  → co₁ ≡ co₂
covering-eq {cov[ _ , set₁ ]} {cov[ ._ , set₂ ]} refl =
  ap (λ set → cov[ _ , set ])
    (prop-has-all-paths (Π-is-prop λ _ → is-set-is-prop) _ _)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import Calf.CostMonoid

module Calf.Types.Eq where

open import Calf.Prelude
open import Calf.Metalanguage
open import Calf.PhaseDistinction
open import Relation.Binary.PropositionalEquality

postulate
  eq : (A : tp pos) → val A → val A → tp pos
  eq/intro : ∀ {A v1 v2} → v1 ≡ v2 → val (eq A v1 v2)
  eq/ref : ∀ {A v1 v2} → cmp (F (eq A v1 v2)) → v1 ≡ v2

  eq/uni : ∀ {A v1 v2} → (p q : cmp (F (eq A v1 v2))) →
    (u : ext) → p ≡ q

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Primality
------------------------------------------------------------------------

module Data.Nat.Primality where

open import Data.Empty
open import Data.Fin as Fin hiding (_+_)
open import Data.Fin.Dec
open import Data.Nat
open import Data.Nat.Divisibility
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Negation
open import Relation.Unary

-- Definition of primality.

Prime : ℕ → Set
Prime 0             = ⊥
Prime 1             = ⊥
Prime (suc (suc n)) = (i : Fin n) → ¬ (2 + Fin.toℕ i ∣ 2 + n)

-- Decision procedure for primality.

prime? : Decidable Prime
prime? 0             = no λ()
prime? 1             = no λ()
prime? (suc (suc n)) = all? λ _ → ¬? (_ ∣? _)

private

  -- Example: 2 is prime.

  2-is-prime : Prime 2
  2-is-prime = from-yes (prime? 2)


text:
module Rev {A : Set} where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open Eq.≡-Reasoning
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List
  using (List; []; _∷_; _++_; map; foldr; replicate; length; _∷ʳ_)
  -- renaming (reverse to rev)
open import Data.List.Properties
  using (++-assoc; ++-identityʳ)
  -- renaming (unfold-reverse to revʳ;
  --           reverse-++-commute to rev-++;
  --           reverse-involutive to rev-inv)
open import Data.List.All using (All; []; _∷_)
open import Data.List.All.Properties
  renaming (++⁺ to _++All_)

pattern [_]       x        =  x ∷ []
pattern [_,_]     x y      =  x ∷ y ∷ []
pattern [_,_,_]   x y z    =  x ∷ y ∷ z ∷ []
pattern [_,_,_,_] x y z w  =  x ∷ y ∷ z ∷ w ∷ []

rev : List A → List A
rev [] =  []
rev (x ∷ xs) =  rev xs ++ [ x ]

rev-++ : ∀ xs ys → rev (xs ++ ys) ≡ rev ys ++ rev xs
rev-++ [] ys =
  begin
    rev ([] ++ ys)
  ≡⟨ sym (++-identityʳ (rev ys)) ⟩
    rev ys ++ rev []
  ∎
rev-++ (x ∷ xs) ys =
  begin
    rev (x ∷ xs ++ ys)
  ≡⟨⟩
    rev (xs ++ ys) ++ [ x ]
  ≡⟨ cong (_++ [ x ]) (rev-++ xs ys) ⟩
    (rev ys ++ rev xs) ++ [ x ]
  ≡⟨ ++-assoc (rev ys) (rev xs) [ x ] ⟩
    rev ys ++ (rev xs ++ [ x ])
  ≡⟨⟩
    rev ys ++ (rev (x ∷ xs))
  ∎

rev-inv : ∀ xs → rev (rev xs) ≡ xs
rev-inv [] =
  begin
    rev (rev [])
  ≡⟨⟩
    []
  ∎
rev-inv (x ∷ xs) =
  begin
    rev (rev (x ∷ xs))
  ≡⟨⟩
    rev (rev xs ++ [ x ])
  ≡⟨ rev-++ (rev xs) [ x ] ⟩
    rev [ x ] ++ rev (rev xs)
  ≡⟨ cong (rev [ x ] ++_) (rev-inv xs) ⟩
    rev [ x ] ++ xs
  ≡⟨⟩
    x ∷ xs
  ∎

revAll : ∀ (P : A → Set) → ∀ {xs} → All P xs → All P (rev xs)
revAll P [] = []
revAll P (Px ∷ Pxs) =  revAll P Pxs ++All [ Px ]


text:
-- Andreas, 2021-04-10, issue #5288
-- De Bruijn index problem in treeless compiler

-- {-# OPTIONS -v tc.cc:20 #-}
-- {-# OPTIONS -v treeless:40 #-}
-- {-# OPTIONS -v treeless.convert.lambdas:40 #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.IO
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit

f : Nat → Nat → Nat
f _ zero = 0
f m      = λ _ → m   -- this catch-all was wrongly compiled

postulate
  printNat : Nat → IO ⊤

{-# COMPILE GHC printNat = print #-}
{-# COMPILE JS  printNat = function (x) { return function(cb) { process.stdout.write(x + "\n"); cb(0); }; } #-}

test : Nat
test = f 123 1

prf : test ≡ 123
prf = refl

main = printNat test

-- Should print 123


text:
-- Andreas, 2012-09-17
{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.with.type:15 -v syntax.reify.con:30 #-}
module ReifyConstructorParametersForWith where

import Common.Level

module M {i} {I : Set i} where

  data D : Set i where
    c : {i : I} → D  -- danger of confusion for c {i = ...}

  data P : D → Set i where
    p : {x : I} → P (c {x})

  Pc : (x : I) → Set i
  Pc x = P (c {x})

  works : ∀ (x : I) → Pc x → Pc x
  works x y with Set
  ... | _ = y

  module N (x : I) where

    bla : Pc x → Pc x
    bla y with Set
    ... | _ = y

open M

test : ∀ {i}{I : Set i}(x : I) → Pc x → Pc x
test x y with Set
... | _ = y
-- If reification does not reify constructor parameters
-- for generating the with type, it confuses constructor
-- parameter {i} with constructor argument {i}.


text:
module slots.defs where

open import slots.imports

record config
  : Set where

  field
    n : ℕ -- reel count
    m : ℕ -- fruit count

  Win/Bet = ℕ -- win per 1 bet
  Fruit = Fin m
  ReelNo = Fin n
  Reel = List Fruit
  Reels = Vec Reel n
  WinLine = Vec Win/Bet n
  WinTable = Vec WinLine m
  Line = Vec Fruit n

record game (cfg : config) : Set where
  open config cfg

  field
    reels : Reels
    winTable : WinTable

max_stars_repo_name: semenov-vladyslav/slots-agda

max_issues_repo_name: semenov-vladyslav/slots-agda

max_forks_repo_name: semenov-vladyslav/slots-agda


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

open import HoTT

module cohomology.WithCoefficients where

→Ω-group-structure : ∀ {i j} (X : Ptd i) (Y : Ptd j)
  → GroupStructure (fst (X ⊙→ ⊙Ω Y))
→Ω-group-structure X Y = record {
  ident = ((λ _ → idp) , idp);
  inv = λ F → ((! ∘ fst F) , ap ! (snd F));
  comp = λ F G →
    ((λ x → fst F x ∙ fst G x), ap2 _∙_ (snd F) (snd G));
  unitl = λ G → pair= idp (ap2-idp-l _∙_ {x = idp} (snd G) ∙ ap-idf (snd G));
  unitr = λ F → ⊙λ=
    (∙-unit-r ∘ fst F)
    (ap2-idp-r _∙_ (snd F) ∙ unitr-lemma (snd F));
  assoc = λ F G H → ⊙λ=
    (λ x → ∙-assoc (fst F x) (fst G x) (fst H x))
    (! (∙-unit-r _) ∙ assoc-lemma (snd F) (snd G) (snd H));
  invl = λ F → ⊙λ=
    (!-inv-l ∘ fst F)
    (invl-lemma (snd F) ∙ ! (∙-unit-r _));
  invr = λ F → ⊙λ=
    (!-inv-r ∘ fst F)
    (invr-lemma (snd F) ∙ ! (∙-unit-r _))}
  where

  unitr-lemma : ∀ {i} {A : Type i} {x : A} {p : x == x} (α : p == idp)
    → ap (λ r → r ∙ idp) α == ∙-unit-r p ∙ α
  unitr-lemma idp = idp

  assoc-lemma : ∀ {i} {A : Type i} {w x y z : A}
    {p₁ p₂ : w == x} {q₁ q₂ : x == y} {r₁ r₂ : y == z}
    (α : p₁ == p₂) (β : q₁ == q₂) (γ : r₁ == r₂)
    → ap2 _∙_ (ap2 _∙_ α β) γ ∙ ∙-assoc p₂ q₂ r₂ ==
      ∙-assoc p₁ q₁ r₁ ∙ ap2 _∙_ α (ap2 _∙_ β γ)
  assoc-lemma idp idp idp = ! (∙-unit-r _)

  invl-lemma : ∀ {i} {A : Type i} {x : A} {p : x == x} (α : p == idp)
    → ap2 _∙_ (ap ! α) α == !-inv-l p
  invl-lemma idp = idp

  invr-lemma : ∀ {i} {A : Type i} {x : A} {p : x == x} (α : p == idp)
    → ap2 _∙_ α (ap ! α) == !-inv-r p
  invr-lemma idp = idp

→Ω-Group : ∀ {i j} (X : Ptd i) (Y : Ptd j) → Group (lmax i j)
→Ω-Group X Y = Trunc-Group (→Ω-group-structure X Y)

{- Pointed maps out of bool -}

Bool⊙→-out : ∀ {i} {X : Ptd i}
  → fst (⊙Lift {j = i} ⊙Bool ⊙→ X) → fst X
Bool⊙→-out (h , _) = h (lift false)

Bool⊙→-equiv : ∀ {i} (X : Ptd i)
  → fst (⊙Lift {j = i} ⊙Bool ⊙→ X) ≃ fst X
Bool⊙→-equiv {i} X = equiv Bool⊙→-out g f-g g-f
  where
  g : fst X → fst (⊙Lift {j = i} ⊙Bool ⊙→ X)
  g x = ((λ {(lift b) → if b then snd X else x}) , idp)

  f-g : ∀ x → Bool⊙→-out (g x) == x
  f-g x = idp

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

abstract
  Bool⊙→-path : ∀ {i} (X : Ptd i)
    → fst (⊙Lift {j = i} ⊙Bool ⊙→ X) == fst X
  Bool⊙→-path X = ua (Bool⊙→-equiv X)

abstract
  Bool⊙→Ω-is-π₁ : ∀ {i} (X : Ptd i)
    → →Ω-Group (⊙Lift {j = i} ⊙Bool) X == π 1 (ℕ-S≠O _) X
  Bool⊙→Ω-is-π₁ {i} X =
    group-ua
      (record {
         f = Trunc-fmap Bool⊙→-out;
         pres-comp = Trunc-elim {i = i}
           (λ _ → Π-level {j = i} (λ _ → =-preserves-level _ Trunc-level))
           (λ g₁ → Trunc-elim
             (λ _ → =-preserves-level _ Trunc-level)
             (λ g₂ → idp))} ,
       is-equiv-Trunc ⟨0⟩ _ (snd (Bool⊙→-equiv (⊙Ω X))))

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
postulate P : Set -> Set

test : (B : Set) -> P B -> P B
test = λ p p -> {!!}

postulate A : Set

test₂ : Set → A
test₂ A = {!!}


text:
module Haskell.RangedSetsProp.BoundariesProperties where

open import Haskell.RangedSetsProp.library

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool

open import Haskell.Prim
open import Haskell.Prim.Ord
open import Haskell.Prim.Bool
open import Haskell.Prim.Maybe
open import Haskell.Prim.Enum
open import Haskell.Prim.Eq
open import Haskell.Prim.List
open import Haskell.Prim.Integer
open import Haskell.Prim.Double

open import Haskell.RangedSets.Boundaries

prop_no_boundary_smaller : {{ o : Ord a }} -> {{ dio : DiscreteOrdered a}} -> (r1 : Boundary a) -> (r1 < BoundaryBelowAll) ≡ false
prop_no_boundary_smaller BoundaryBelowAll = refl
prop_no_boundary_smaller BoundaryAboveAll = refl
prop_no_boundary_smaller (BoundaryAbove x) = refl
prop_no_boundary_smaller (BoundaryBelow x) = refl

prop_no_boundary_greater : {{ o : Ord a }} -> {{ dio : DiscreteOrdered a}} -> (r1 : Boundary a) -> (r1 > BoundaryAboveAll) ≡ false
prop_no_boundary_greater BoundaryBelowAll = refl
prop_no_boundary_greater BoundaryAboveAll = refl
prop_no_boundary_greater (BoundaryAbove x) = refl
prop_no_boundary_greater (BoundaryBelow x) = refl

BoundaryBelowAllSmaller :  ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (b : Boundary a)
      → (BoundaryBelowAll <= b) ≡ true
BoundaryBelowAllSmaller BoundaryBelowAll = refl
BoundaryBelowAllSmaller BoundaryAboveAll = refl
BoundaryBelowAllSmaller (BoundaryBelow _) = refl
BoundaryBelowAllSmaller (BoundaryAbove _)  = refl

postulate
  prop_max_sym : {{ o : Ord a }} -> {{ dio : DiscreteOrdered a}} -> (r1 : Boundary a) -> (r2 : Boundary a) -> max r1 r2 ≡ max r2 r1
  prop_min_sym : {{ o : Ord a }} -> {{ dio : DiscreteOrdered a}} -> (r1 : Boundary a) -> (r2 : Boundary a) -> min r1 r2 ≡ min r2 r1

-- prop_max_sym : {{ o : Ord a }} -> {{ dio : DiscreteOrdered a}} -> (r1 : Boundary a) -> (r2 : Boundary a) -> max r1 r2 ≡ max r2 r1
-- prop_max_sym {{o}} {{dio}} r1 r2 =
--     begin
--         max r1 r2
--     =⟨⟩
--         if (compare x y == GT) then x else y
--     =⟨⟩
--         if (compare y x == GT) then y else x
--     =⟨⟩
--         max r2 r1
--     end


text:
{- Type class for natural transformations. -}
module CategoryTheory.NatTrans where

open import CategoryTheory.Categories
open import CategoryTheory.Functor
open import Relation.Binary using (IsEquivalence)

infixr 25 _⟹_

-- Natural transformation between two functors
record _⟹_ {n} {ℂ 𝔻 : Category n} (F : Functor ℂ 𝔻) (G : Functor ℂ 𝔻) : Set (lsuc n) where
    private module ℂ = Category ℂ
    private module 𝔻 = Category 𝔻
    private module F = Functor F
    private module G = Functor G
    field
        -- || Definitions
        -- One component of the natural transformations.
        at : ∀(A : ℂ.obj) -> (F.omap A) 𝔻.~> (G.omap A)

        -- || Laws
        -- Naturality condition
        nat-cond : ∀{A B : ℂ.obj} {f : A ℂ.~> B}
                -> (G.fmap f 𝔻.∘ at A) 𝔻.≈ (at B 𝔻.∘ F.fmap f)

-- Identity natural transformation
ιd : ∀ {n} {ℂ 𝔻 : Category n} -> (F : Functor ℂ 𝔻) -> F ⟹ F
ιd {n} {ℂ} {𝔻} F = record
        { at = λ A -> F.fmap ℂ.id
        ; nat-cond =  λ {A} {B} {f} ->
            begin
                F.fmap f ∘ F.fmap ℂ.id
            ≈⟨ ≈-cong-right (F.fmap-id) ⟩
                F.fmap f ∘ id
            ≈⟨ id-comm ⟩
                id ∘ F.fmap f
            ≈⟨ ≈-cong-left (F.fmap-id [sym]) ⟩
                F.fmap ℂ.id ∘ F.fmap  f
            ∎
        }

    where
    private module F = Functor F
    private module ℂ = Category ℂ
    open Category 𝔻

-- Vertical composition of natural transformations
_⊚_ : ∀ {n} {ℂ 𝔻 : Category n} -> {F G H : Functor ℂ 𝔻}
   -> (G ⟹ H) -> (F ⟹ G) -> (F ⟹ H)
_⊚_ {n} {ℂ} {𝔻} {F} {G} {H} φ ψ = record
    { at = λ A -> (φ.at A) ∘ (ψ.at A)
    ; nat-cond =  λ {A} {B} {f} ->
        begin
            H.fmap f ∘ (φ.at A ∘ ψ.at A)
        ≈⟨ ∘-assoc [sym] ⟩
            (H.fmap f ∘ φ.at A) ∘ ψ.at A
        ≈⟨ ≈-cong-left (φ.nat-cond) ≈> ∘-assoc ⟩
            φ.at B ∘ (G.fmap f ∘ ψ.at A)
        ≈⟨ ≈-cong-right (ψ.nat-cond) ≈> (∘-assoc [sym])⟩
            (φ.at B ∘ ψ.at B) ∘ F.fmap f
        ∎
    }
    where
    open Category 𝔻
    private module F = Functor F
    private module G = Functor G
    private module H = Functor H
    private module φ   = _⟹_ φ
    private module ψ = _⟹_ ψ
    open import Relation.Binary using (IsEquivalence)

-- Horizontal composition of natural tranformations
_✦_ : ∀ {n} {ℂ 𝔻 𝔼 : Category n} {F F′ : Functor ℂ 𝔻} {G G′ : Functor 𝔻 𝔼}
   -> (G ⟹ G′) -> (F ⟹ F′) -> (G ◯ F ⟹ G′ ◯ F′)
_✦_ {n} {ℂ} {𝔻} {𝔼} {F} {F′} {G} {G′} ψ φ = record
    { at = λ A → G′.fmap (φ.at A) ∘ ψ.at (F.omap A)
    ; nat-cond = λ {A} {B} {f} →
        begin
            Functor.fmap (G′ ◯ F′) f ∘ (G′.fmap (φ.at A) ∘ ψ.at (F.omap A))
        ≈⟨ ∘-assoc [sym] ≈> ≈-cong-left (G′.fmap-∘ [sym]) ⟩
            G′.fmap (F′.fmap f 𝔻.∘ φ.at A) ∘ ψ.at (F.omap A)
        ≈⟨ ≈-cong-left (G′.fmap-cong (φ.nat-cond)) ⟩
            G′.fmap (φ.at B 𝔻.∘ F.fmap f) ∘ ψ.at (F.omap A)
        ≈⟨ ≈-cong-left (G′.fmap-∘) ≈> ∘-assoc ⟩
            G′.fmap (φ.at B) ∘ (Functor.fmap (G′ ◯ F) f ∘ ψ.at (F.omap A))
        ≈⟨ ≈-cong-right (ψ.nat-cond) ≈> ∘-assoc [sym] ⟩
            (G′.fmap (φ.at B) ∘ ψ.at (F.omap B)) ∘ Functor.fmap (G ◯ F) f
        ∎
    }
    where
    private module 𝔻 = Category 𝔻
    open Category 𝔼
    private module F = Functor F
    private module G = Functor G
    private module F′ = Functor F′
    private module G′ = Functor G′
    private module φ   = _⟹_ φ
    private module ψ = _⟹_ ψ

-- Natural isomorphism between two functors
record _⟺_  {n} {ℂ 𝔻 : Category n} (F : Functor ℂ 𝔻) (G : Functor ℂ 𝔻) : Set (lsuc n) where
    private module ℂ = Category ℂ
    private module 𝔻 = Category 𝔻
    private module F = Functor F
    private module G = Functor G
    field
        -- || Definitions
        -- NT from F to G
        to   : F ⟹ G
        -- NT from G to F
        from : G ⟹ F

    private module to   = _⟹_ to
    private module from = _⟹_ from

    field
        -- || Isomorphism laws
        iso1 : ∀{A : ℂ.obj} -> (from.at A) 𝔻.∘ (to.at A)   𝔻.≈ 𝔻.id
        iso2 : ∀{A : ℂ.obj} -> (to.at A)   𝔻.∘ (from.at A) 𝔻.≈ 𝔻.id

-- Natural isomorphism is an equivalence
⟺-equiv : ∀ {n} {ℂ 𝔻 : Category n} -> IsEquivalence (_⟺_ {n} {ℂ} {𝔻})
⟺-equiv {n} {ℂ} {𝔻} = record
         { refl = λ {F} -> record
             { to = ιd F
             ; from = ιd F
             ; iso1 = λ {A} -> refl-iso-proof {A} {F}
             ; iso2 = λ {A} -> refl-iso-proof {A} {F} }
         ; sym = λ {F} {G} F⟺G -> record
             { to = _⟺_.from F⟺G
             ; from = _⟺_.to F⟺G
             ; iso1 = _⟺_.iso2 F⟺G
             ; iso2 = _⟺_.iso1 F⟺G }
         ; trans = λ {F} {G} {H} F⟺G G⟺H -> record
             { to = (_⟺_.to G⟺H) ⊚ (_⟺_.to F⟺G)
             ; from = (_⟺_.from F⟺G) ⊚ (_⟺_.from G⟺H)
             ; iso1 = λ {A} →
                begin
                    at (from F⟺G ⊚ from G⟺H) A ∘ at (to G⟺H ⊚ to F⟺G) A
                ≈⟨ ∘-assoc [sym] ≈> ≈-cong-left (∘-assoc) ⟩
                    (at (from F⟺G) A ∘ (at (from G⟺H) A ∘ at (to G⟺H) A)) ∘ at (to F⟺G) A
                ≈⟨ ≈-cong-left (≈-cong-right (iso1 G⟺H)) ⟩
                    (at (from F⟺G) A ∘ id) ∘ at (to F⟺G) A
                ≈⟨ ≈-cong-left (id-right) ⟩
                    at (from F⟺G) A ∘ at (to F⟺G) A
                ≈⟨ iso1 F⟺G ⟩
                    id
                ∎
             ; iso2 = λ {A} →
                begin
                    at (to G⟺H ⊚ to F⟺G) A ∘ at (from F⟺G ⊚ from G⟺H) A
                ≈⟨ (∘-assoc [sym]) ≈> ≈-cong-left (∘-assoc) ⟩
                    (at (to G⟺H) A ∘ (at (to F⟺G) A ∘ at (from F⟺G) A)) ∘ at (from G⟺H) A
                ≈⟨ ≈-cong-left (≈-cong-right (iso2 F⟺G)) ⟩
                    (at (to G⟺H) A ∘ id) ∘ at (from G⟺H) A
                ≈⟨ ≈-cong-left (id-right) ⟩
                    at (to G⟺H) A ∘ at (from G⟺H) A
                ≈⟨ iso2 G⟺H ⟩
                    id
                ∎
             }
         }
    where
    private module ℂ = Category ℂ
    open Category 𝔻
    open _⟹_
    open _⟺_
    refl-iso-proof : {A : ℂ.obj} {F : Functor ℂ 𝔻}
             -> _⟹_.at (ιd F) A ∘ _⟹_.at (ιd F) A ≈ id
    refl-iso-proof {A} {F} =
        begin
            _⟹_.at (ιd F) A ∘ _⟹_.at (ιd F) A
        ≈⟨ ≈-cong-left (Functor.fmap-id F) ⟩
            id ∘ _⟹_.at (ιd F) A
        ≈⟨ ≈-cong-right (Functor.fmap-id F) ⟩
            id ∘ id
        ≈⟨ id-left ⟩
            id
        ∎

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
-- Andreas, AIM XXIII, Issue 1944

-- {-# OPTIONS -v tc.proj.amb:30 #-}

-- Non-overloaded

record Wrap (A : Set) : Set where
  field wrapped : A
open Wrap

-- Overloaded

record Sg (A : Set) : Set where
  field head : A
open Sg

record Sg' (A : Set) : Set where
  field head : A
open Sg'

-- ov/ov

works : ∀ {A : Set} (w : Sg (Sg' A)) → Sg A
head (works w) = head (head w)

-- ov/nov

test : ∀ {A : Set} (w : Wrap (Sg' A)) → Sg A
head (test w) = head (wrapped w)

-- WAS: failed because of a missing `reduce`


text:
module SizedIO.coIOIO where

open import Size

mutual
  data coIO²  (i : Size) (j : Size)
              (Cin : Set ) (Rin : Cin  → Set)
              (Cext : Set) (Rext : Cext → Set)
              (A : Set) : Set where
     return : A → coIO² i j Cin Rin Cext Rext A
     dof    : (i' : Size< i) →
              (c : Cin) → (Rin c → coIO² i' j Cin Rin Cext Rext A)
              → coIO² i j Cin Rin Cext Rext A
     do∞    : (c : Cext)
              → (Rext c → coIO²∞ j Cin Rin Cext Rext A)
              → coIO² i j Cin Rin Cext Rext A

  record coIO²∞ (j : Size) (Cin : Set ) (Rin : Cin  → Set)
                            (Cext : Set) (Rext : Cext → Set)
                            (A : Set) : Set where
    coinductive
    field
      force : (j' : Size< j)
               → coIO² ∞ j' Cin Rin Cext Rext A

open coIO²∞ public

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
-- Andreas, 2012-02-24 example by Ramana Kumar
{-# OPTIONS --sized-types #-}
-- {-# OPTIONS --show-implicit -v tc.size.solve:20 -v tc.conv.size:15 #-}
module SizeInconsistentMeta4 where

open import Data.Nat using (ℕ;zero;suc) renaming (_<_ to _N<_)
open import Data.Product using (_,_;_×_)
open import Data.Product.Relation.Binary.Lex.Strict using (×-Lex; ×-transitive)
open import Data.List using (List)
open import Data.List.Relation.Binary.Lex.Strict using (Lex-<) renaming (<-transitive to Lex<-trans)
open import Relation.Binary using (Rel;_Respects₂_;Transitive;IsEquivalence)

open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)

open import Level using (0ℓ)
open import Size using (Size;↑_)

-- keeping the definition of Vec for the positivity check
infixr 5 _∷_
data Vec {a} (A : Set a) : ℕ → Set a where
  []  : Vec A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

{- produces different error
data Lex-< {A : _} (_≈_ _<_ : Rel A Level.zero) : Rel (List A) Level.zero where
postulate
  Lex<-trans : ∀ {P _≈_ _<_} →
               IsEquivalence _≈_ → _<_ Respects₂ _≈_ → Transitive _<_ →
               Transitive (Lex-< _≈_ _<_)
-}

postulate
  N<-trans : Transitive _N<_
  -- Vec : ∀ {a} (A : Set a) → ℕ → Set a
  Vec→List : ∀ {a n} {A : Set a} → Vec A n → List A

data Type : Size → Set where
  TyApp : {z : Size} (n : ℕ) → (as : Vec (Type z) n) → Type (↑ z)

<-transf : ∀ {z} → Rel (Type z) 0ℓ → Rel (ℕ × List (Type z)) 0ℓ
<-transf _<_ = ×-Lex _≡_ _N<_ (Lex-< _≡_ _<_)

infix 4 _<_
data _<_ : {z : Size} → Rel (Type z) 0ℓ where
  TyApp<TyApp : ∀ {z} {n₁} {as₁} {n₂} {as₂} →
                <-transf (_<_ {z}) (n₁ , Vec→List as₁) (n₂ , Vec→List as₂) →
                _<_ {↑ z} (TyApp n₁ as₁) (TyApp n₂ as₂)

<-trans : ∀ {z} → Transitive (_<_ {z})
<-trans (TyApp<TyApp p) (TyApp<TyApp q) =
  TyApp<TyApp (×-transitive {_<₂_ = Lex-< _≡_ _<_}
                 PropEq.isEquivalence
                (PropEq.resp₂ _N<_)
                N<-trans
                (Lex<-trans PropEq.isEquivalence (PropEq.resp₂ _<_) <-trans)
                p q)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Globe where

import Level
open import Relation.Binary using (IsEquivalence; module IsEquivalence)
open import Relation.Binary.PropositionalEquality using (isEquivalence)
open import Data.Nat using (ℕ; zero; suc; _<_; _≤_; z≤n; s≤s)
open import Data.Nat.Properties using (<-trans)

open import Categories.Support.PropositionalEquality
open import Categories.Category

-- the stdlib doesn't have this
private
  ≤-unique : ∀ {m n} {x y : m ≤ n} → x ≣ y
  ≤-unique {x = z≤n} {z≤n} = ≣-refl
  ≤-unique {x = s≤s m≤n} {s≤s m≤n'} = ≣-cong s≤s ≤-unique

data GlobeHom : (m n : ℕ) → Set where
  I : {place : ℕ} → GlobeHom place place
  σ : {m n : ℕ} (n<m : n < m) → GlobeHom n m
  τ : {m n : ℕ} (n<m : n < m) → GlobeHom n m

infixl 7 _⊚_

_⊚_ : ∀ {l m n} → GlobeHom m n → GlobeHom l m → GlobeHom l n
I ⊚ y = y
x ⊚ I = x
σ n<m ⊚ σ m<l = σ (<-trans m<l n<m)
σ n<m ⊚ τ m<l = τ (<-trans m<l n<m)
τ n<m ⊚ σ m<l = σ (<-trans m<l n<m)
τ n<m ⊚ τ m<l = τ (<-trans m<l n<m)

Globe : Category Level.zero Level.zero Level.zero
Globe = record
  { Obj = ℕ
  ; _⇒_ = GlobeHom
  ; _≡_ = _≣_
  ; id = I
  ; _∘_ = _⊚_
  ; assoc = λ {_} {_} {_} {_} {f} {g} {h} → assoc {f = f} {g} {h}
  ; identityˡ = λ {A} {B} {f} → ≣-refl
  ; identityʳ = identityʳ
  ; equiv = isEquivalence
  ; ∘-resp-≡ = ∘-resp-≡
  }
  where

  assoc : ∀ {A B C D} {f : GlobeHom A B} {g : GlobeHom B C} {h : GlobeHom C D} → (h ⊚ g) ⊚ f ≣ h ⊚ (g ⊚ f)
  assoc {f = I} {I} {I} = ≣-refl
  assoc {f = I} {I} {σ _} = ≣-refl
  assoc {f = I} {I} {τ _} = ≣-refl
  assoc {f = I} {σ _} {I} = ≣-refl
  assoc {f = I} {σ _} {σ _} = ≣-refl
  assoc {f = I} {σ _} {τ _} = ≣-refl
  assoc {f = I} {τ _} {I} = ≣-refl
  assoc {f = I} {τ _} {σ _} = ≣-refl
  assoc {f = I} {τ _} {τ _} = ≣-refl
  assoc {f = σ _} {I} {I} = ≣-refl
  assoc {f = σ _} {I} {σ _} = ≣-refl
  assoc {f = σ _} {I} {τ _} = ≣-refl
  assoc {f = σ _} {σ _} {I} = ≣-refl
  assoc {f = σ _} {σ _} {σ _} = ≣-cong σ ≤-unique
  assoc {f = σ _} {σ _} {τ _} = ≣-cong σ ≤-unique
  assoc {f = σ _} {τ _} {I} = ≣-refl
  assoc {f = σ _} {τ _} {σ _} = ≣-cong σ ≤-unique
  assoc {f = σ _} {τ _} {τ _} = ≣-cong σ ≤-unique
  assoc {f = τ n<m} {I} {I} = ≣-refl
  assoc {f = τ n<m} {I} {σ _} = ≣-refl
  assoc {f = τ n<m} {I} {τ _} = ≣-refl
  assoc {f = τ n<m} {σ _} {I} = ≣-refl
  assoc {f = τ n<m} {σ _} {σ _} = ≣-cong τ ≤-unique
  assoc {f = τ n<m} {σ _} {τ _} = ≣-cong τ ≤-unique
  assoc {f = τ n<m} {τ _} {I} = ≣-refl
  assoc {f = τ n<m} {τ _} {σ _} = ≣-cong τ ≤-unique
  assoc {f = τ n<m} {τ _} {τ _} = ≣-cong τ ≤-unique

  -- this is necessary because Agda lies...
  identityʳ : ∀ {A B} {f : GlobeHom A B} → f ⊚ I ≣ f
  identityʳ {f = I} = ≣-refl
  identityʳ {f = σ _} = ≣-refl
  identityʳ {f = τ _} = ≣-refl

  ∘-resp-≡ : ∀ {A B C} {f h : GlobeHom B C} {g i : GlobeHom A B} → f ≣ h → g ≣ i → f ⊚ g ≣ h ⊚ i
  ∘-resp-≡ ≣-refl ≣-refl = ≣-refl

infixl 30 _σ′
infixl 30 _τ′

data GlobeHom′ : (m n : ℕ) → Set where
  I : ∀ {place : ℕ} → GlobeHom′ place place
  _σ′ : ∀ {n m : ℕ} → GlobeHom′ (suc n) m → GlobeHom′ n m
  _τ′ : ∀ {n m : ℕ} → GlobeHom′ (suc n) m → GlobeHom′ n m

data GlobeEq′ : {m n : ℕ} → GlobeHom′ m n → GlobeHom′ m n → Set where
  both-I : ∀ {m} → GlobeEq′ {m} {m} I I
  both-σ : ∀ {m n x y} → GlobeEq′ {m} {n} (x σ′) (y σ′)
  both-τ : ∀ {m n x y} → GlobeEq′ {m} {n} (x τ′) (y τ′)

GlobeEquiv : ∀ {m n} → IsEquivalence (GlobeEq′ {m} {n})
GlobeEquiv = record { refl = refl; sym = sym; trans = trans }
  where
  refl : ∀ {m n} {x : GlobeHom′ m n} → GlobeEq′ x x
  refl {x = I} = both-I
  refl {x = y σ′} = both-σ
  refl {x = y τ′} = both-τ
  sym : ∀ {m n} {x y : GlobeHom′ m n} → GlobeEq′ x y → GlobeEq′ y x
  sym both-I = both-I
  sym both-σ = both-σ
  sym both-τ = both-τ
  trans : ∀ {m n} {x y z : GlobeHom′ m n} → GlobeEq′ x y → GlobeEq′ y z → GlobeEq′ x z
  trans both-I y∼z = y∼z
  trans both-σ both-σ = both-σ
  trans both-τ both-τ = both-τ

infixl 7 _⊚′_

_⊚′_ : ∀ {l m n} → GlobeHom′ m n → GlobeHom′ l m → GlobeHom′ l n
x ⊚′ I = x
x ⊚′ y σ′ = (x ⊚′ y) σ′
x ⊚′ y τ′ = (x ⊚′ y) τ′

Globe′ : Category Level.zero Level.zero Level.zero
Globe′ = record
  { Obj = ℕ
  ; _⇒_ = GlobeHom′
  ; _≡_ = GlobeEq′
  ; id = I
  ; _∘_ = _⊚′_
  ; assoc = λ {_ _ _ _ f g h} → assoc {f = f} {g} {h}
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; equiv = GlobeEquiv
  ; ∘-resp-≡ = ∘-resp-≡
  }
  where
  assoc : ∀ {A B C D} {f : GlobeHom′ A B} {g : GlobeHom′ B C} {h : GlobeHom′ C D} → GlobeEq′ ((h ⊚′ g) ⊚′ f) (h ⊚′ (g ⊚′ f))
  assoc {f = I} = refl
    where open IsEquivalence GlobeEquiv
  assoc {f = y σ′} = both-σ
  assoc {f = y τ′} = both-τ
  identityˡ : ∀ {A B} {f : GlobeHom′ A B} → GlobeEq′ (I ⊚′ f) f
  identityˡ {f = I} = both-I
  identityˡ {f = y σ′} = both-σ
  identityˡ {f = y τ′} = both-τ
  identityʳ : ∀ {A B} {f : GlobeHom′ A B} → GlobeEq′ (f ⊚′ I) f
  identityʳ = IsEquivalence.refl GlobeEquiv
  ∘-resp-≡ : ∀ {A B C} {f h : GlobeHom′ B C} {g i : GlobeHom′ A B} → GlobeEq′ f h → GlobeEq′ g i → GlobeEq′ (f ⊚′ g) (h ⊚′ i)
  ∘-resp-≡ f∼h both-I = f∼h
  ∘-resp-≡ f∼h both-σ = both-σ
  ∘-resp-≡ f∼h both-τ = both-τ

-- Fix this
{-
data ReflexiveGlobeHom : (m n : ℕ) → Set where
  plain : ∀ {m n} → GlobeHom m n → ReflexiveGlobeHom m n
  ι : ∀ {m n} → ReflexiveGlobeHom m n → ReflexiveGlobeHom m (suc n)

stripped : ∀ {m n} → (cons : n < m → GlobeHom n m) → n < suc m → GlobeHom n m
stripped cons n<Sm with <-unsucʳ n<Sm
stripped cons n<Sm | inl ≣-refl = I
stripped cons n<Sm | inr n<m = cons n<m

_⊚ʳ_ : ∀ {l m n} → ReflexiveGlobeHom m n → ReflexiveGlobeHom l m → ReflexiveGlobeHom l n
ι x ⊚ʳ y = ι (x ⊚ʳ y)
plain x ⊚ʳ plain y = plain (x ⊚ y)
plain I ⊚ʳ ι y = ι y
plain (σ _) ⊚ʳ ι y = (plain (stripped σ n<m)) ⊚ʳ y
plain (τ n<m) ⊚ʳ ι y = (plain (stripped τ n<m)) ⊚ʳ y
-}

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
primitive

abstract

postulate

private

mutual

macro

variable

instance

record F : Set where
  field

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Common.Level

-- Note that this is level-polymorphic
record ⊤ {a} : Set a where
  constructor tt

data ⊥ {a} : Set a where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

lzero' : ℕ → Level
lzero' zero    = lzero
lzero' (suc n) = lzero ⊔ (lzero' n)

IsZero : (x : ℕ) → Set (lsuc (lzero' x))
IsZero zero = ⊤
IsZero (suc _) = ⊥

test : IsZero (suc _)
test = tt


text:
open import Level using (_⊔_)
open import Data.Maybe using (Maybe; nothing; just)
open import Data.List.Any as A hiding (map)
open import Relation.Binary.PropositionalEquality.Core as PropEq
open import Relation.Binary

open import Prelude hiding (map)
open Eq {{...}}

module RW.Data.PMap (A : Set){{eqA : Eq A}} where

  private
    _≟_ : (a₁ a₂ : A) → Dec (a₁ ≡ a₂)
    a₁ ≟ a₂ = Eq.cmp eqA a₁ a₂

  -- Naive Partial Map representation
  to_ : ∀{b} → Set b → Set b
  to B = List (A × B)

  to_default : ∀{b} → Set b → Set b
  to B default = B × List (A × B)

  onDef : ∀{b c}{B : Set b}{C : Set c}
        → (m : to B → C) → to B default → C
  onDef f (_ , m) = f m

  onDef' : ∀{b}{B : Set b}
         → (m : to B → to B) → to B default → to B default
  onDef' f (def , m) = def , f m

  empty : ∀{b}{B : Set b}
        → to B
  empty = []

  -- Membership
  _∈_ : ∀{b}{B : Set b}
      → A → (to B) → Set _
  a ∈ m = A.Any ((_≡_ a) ∘ p1) m

  _∉_ : ∀{b}{B : Set b}
      → A → (to B) → Set _
  a ∉ m = (a ∈ m) → ⊥

  -- Decidable membership
  dec∈ : ∀{b}{B : Set b}
       → (a : A) → (m : to B) → Dec (a ∈ m)
  dec∈ a [] = no (λ ())
  dec∈ a (x ∷ m) with a ≟ (p1 x)
  ...| yes a≡x = yes (here a≡x)
  ...| no  a≢x with dec∈ a m
  ...| yes a∈m = yes (there a∈m)
  ...| no  a∉m = no (a∉m ∘ tail a≢x)

  -- Look up
  lkup : ∀{b}{B : Set b} → A → (to B) → Maybe B
  lkup k [] = nothing
  lkup k ((h , r) ∷ ts)
    with k ≟ h
  ...| yes _ = just r
  ...| no  _ = lkup k ts

  -- Look up in a map with a default value
  lkupDef : ∀{b}{B : Set b} → A → to B default → B
  lkupDef a (b , m) = maybe id b (lkup a m)

  -- Total version
  lkup' : ∀{b}{B : Set b}
        → (a : A) → (m : to B) → a ∈ m → B
  lkup' a (m ∷ _)  (here px)   = p2 m
  lkup' a (_ ∷ ms) (there prf) = lkup' a ms prf

  -- Insertion / Removal
  alter : ∀{b}{B : Set b}
        → (Maybe B → Maybe B) → A → (to B) → (to B)
  alter f a [] with f nothing
  ...| just b  = (a , b) ∷ []
  ...| nothing = []
  alter f a (x ∷ m) with a ≟ p1 x
  ...| no  _ = x ∷ alter f a m
  ...| yes _ with f $ just (p2 x)
  ...| nothing = m
  ...| just b  = (a , b) ∷ m

  alterPrf : ∀{b}{B : Set b}
           → B → (a : A) → (m : to B) → Σ (to B) (_∈_ a)
  alterPrf b a m with dec∈ a m
  ...| yes a∈m = m , a∈m
  ...| no  a∉m = (a , b) ∷ m , here refl

  insert : ∀{b}{B : Set b}
         → A → B → (to B) → (to B)
  insert a b m = alter (const $ just b) a m

  delete : ∀{b}{B : Set b}
         → A → (to B) → (to B)
  delete a m = alter (const nothing) a m

  -- Map
  map : ∀{b}{B B′ : Set b} → (B → B′) → (to B) → (to B′)
  map f [] = []
  map f ((a , b) ∷ m) = (a , f b) ∷ map f m

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


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

open import Level

module Categories.Categories.Products (o ℓ e : Level) where

open import Categories.Category
open import Categories.Categories

import Categories.Object.Products
open Categories.Object.Products (Categories o ℓ e)

open import Categories.Product
import Categories.Product.Projections
import Categories.Product.Properties

open import Categories.Terminal

private
    import Categories.Object.Product
    open Categories.Object.Product (Categories o ℓ e)
        renaming (Product to ProductObject)

    product :
        {A B : Category o ℓ e}
        → ProductObject A B

    product {A}{B} = record
        { A×B       = Product A B
        ; π₁        = ∏₁
        ; π₂        = ∏₂
        ; ⟨_,_⟩     = _※_
        ; commute₁  = λ {C}{f}{g}    → ※-commute₁  {A = C}{f}{g}
        ; commute₂  = λ {C}{f}{g}    → ※-commute₂  {A = C}{f}{g}
        ; universal = λ {C}{f}{g}{i} → ※-universal {A = C}{f}{g}{i}
        } where
            open Categories.Product.Projections A B
            open Categories.Product.Properties  A B

products : Products
products = record
    { terminal = One {o}{ℓ}{e}
    ; binary = record
        { product = λ {A}{B} → product {A}{B}
        }
    }


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

open import Categories.Category.Core using (Category)
open import Categories.Functor.Bifunctor using (Bifunctor)

module Categories.Diagram.Cowedge {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
  (F : Bifunctor (Category.op C) C D) where

private
  module C = Category C
  module D = Category D
  open D
  open HomReasoning
  open Equiv
  variable
    A : Obj

open import Level

open import Categories.Functor
open import Categories.Functor.Construction.Constant
open import Categories.NaturalTransformation.Dinatural

open Functor F

record Cowedge : Set (levelOfTerm F) where
  field
    E         : Obj
    dinatural : DinaturalTransformation F (const E)

  module dinatural = DinaturalTransformation dinatural

Cowedge-∘ : (W : Cowedge) → Cowedge.E W ⇒ A → Cowedge
Cowedge-∘ {A = A} W f = record
  { E         = A
  ; dinatural = extranaturalˡ (λ X → f ∘ dinatural.α X)
                              (assoc ○ ∘-resp-≈ʳ (extranatural-commˡ dinatural) ○ sym-assoc)
  }
  where open Cowedge W

record Cowedge-Morphism (W₁ W₂ : Cowedge) : Set (levelOfTerm F) where
  private
    module W₁ = Cowedge W₁
    module W₂ = Cowedge W₂
    open DinaturalTransformation
  field
    u : W₁.E ⇒ W₂.E
    commute : ∀ {C} → u ∘ W₁.dinatural.α C ≈ W₂.dinatural.α C

Cowedge-id : ∀ {W} → Cowedge-Morphism W W
Cowedge-id {W} = record { u = D.id ; commute = D.identityˡ }

Cowedge-Morphism-∘ : {A B C : Cowedge} → Cowedge-Morphism B C → Cowedge-Morphism A B → Cowedge-Morphism A C
Cowedge-Morphism-∘ M N = record { u = u M ∘ u N ; commute = assoc ○ (∘-resp-≈ʳ (commute N) ○ commute M) }
  where
  open Cowedge-Morphism
  open HomReasoning

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:
{- 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 LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.KVMap                          as Map hiding (empty)
open import Util.Prelude

module LibraBFT.Impl.Types.OnChainConfig.ValidatorSet where

new : List ValidatorInfo → ValidatorSet
new = ValidatorSet∙new ConsensusScheme∙new

empty : ValidatorSet
empty = new []

obmFromVV : ValidatorVerifier → ValidatorSet
obmFromVV vv0 = record -- ValidatorSet
  { _vsScheme  = ConsensusScheme∙new -- TODO
  ; _vsPayload = fmap go (Map.toList (vv0 ^∙ vvAddressToValidatorInfo))
  }
 where
  go : (Author × ValidatorConsensusInfo) → ValidatorInfo
  go (address , ValidatorConsensusInfo∙new pk vp) =
    record -- ValidatorInfo
    { _viAccountAddress = address
    ; _viConsensusVotingPower = vp
    ; _viConfig = record -- ValidatorConfig
                  { _vcConsensusPublicKey      = pk
                  ; _vcValidatorNetworkAddress = address ^∙ aAuthorName } }

obmGetValidatorInfo : AuthorName → ValidatorSet → Either ErrLog ValidatorInfo
obmGetValidatorInfo name vs =
  case List-filter (λ vi → vi ^∙ viAccountAddress ∙ aAuthorName ≟ name) (vs ^∙ vsPayload) of λ where
    (vi ∷ []) → pure vi
    _         → Left fakeErr  -- ["ValidatorSet", "obmGetValidatorInfo", "TODO better err msg"]


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

open import equality.core
open import function.core
open import function.isomorphism.core
open import hott.equivalence.alternative
open import hott.univalence

≅⇒≡ : ∀ {i}{X Y : Set i}
     → X ≅ Y → X ≡ Y
≅⇒≡ = ≈⇒≡ ∘ ≅⇒≈

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base