text:
open import Data.Bool as Bool using (Bool; false; true; if_then_else_; not)
open import Data.String using (String)
open import Data.Nat using (ℕ; _+_; _≟_; suc; _>_; _<_; _∸_)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Data.List as l using (List; filter; map; take; foldl; length; []; _∷_)
open import Data.List.Properties
-- open import Data.List.Extrema using (max)
open import Data.Maybe using (to-witness)
open import Data.Fin using (fromℕ; _-_; zero; Fin)
open import Data.Fin.Properties using (≤-totalOrder)
open import Data.Product as Prod using (∃; ∃₂; _×_; _,_; Σ)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning
open import Level using (Level)
open import Data.Vec as v using (Vec; fromList; toList; last; length; []; _∷_; [_]; _∷ʳ_; _++_; lookup; head; initLast; filter; map)
open import Data.Vec.Bounded as vb using ([]; _∷_; fromVec; filter; Vec≤)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl; _≗_; cong₂)
open import Data.Nat.Properties using (+-comm)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary using (does)
open import Data.Vec.Bounded.Base using (padRight; ≤-cast)
import Data.Nat.Properties as ℕₚ
open import Relation.Nullary.Decidable.Core using (dec-false)
open import Function using (_∘_)
open import Data.List.Extrema ℕₚ.≤-totalOrder

-- TODO add to std-lib
vecLast : ∀ {a} {A : Set a} {l} {n : ℕ} (xs : Vec A n) → last (xs ∷ʳ l) ≡ l
vecLast []       = refl
vecLast (_ ∷ xs) = P.trans (prop (xs ∷ʳ _)) (vecLast xs)
  where
    prop : ∀ {a} {A : Set a} {n x} (xs : Vec A (suc n)) → last (x v.∷ xs) ≡ last xs
    prop xs with initLast xs
    ...        | _ , _ , refl = refl

-- operations
  -- AddTodo
  -- DeleteTodo
  -- CompleteTodo
  -- ClearCompleted
  -- CompleteAllTodos

-- horizontal properties
  -- AddTodo
  --   non-commutative
  -- DeleteTodo
  --   idempotent
  -- CompleteTodo
  --   idempotent
  -- ClearCompleted
  --   idempotent
  -- CompleteAllTodos
  --   idempotent
  -- EditTodo
  --   EditTodo - EditTodo Todo list length doesn't change

-- vertical properties
  -- AddTodo
  --   AddTodoSetsNewCompletedToFalse
  --   AddTodoSetsNewIdToNonExistingId
  --   AddTodoSetsNewTextToText
  --   doesn't change id of other Todos
  --   doesn't change text of other Todos
  --   doesn't change completed of other Todos
  -- DeleteTodo
  --   DeleteTodoRemoveTodoWithId
  --   DeleteTodoRemoves1Element
  --     only way to add todo is with AddTodo and AddTodo gives non existing id to new todo
  --   doesn't change id of other Todos
  --   doesn't change text of other Todos
  --   doesn't change completed of other Todos
  -- CompleteTodo
  --   CompleteTodoSetsTodoWithIdCompletedToTrue
  --   doesn't touch any other Todo
  --   doesn't change id of any Todo
  --   doesn't change text of any Todo
  -- ClearCompleted
  --   doesn't remove Todos where completed = false
  --   doesn't change id of any Todo
  --   doesn't change completed of any Todo
  --   doesn't change text of any Todo
  -- CompleteAllTodos
  --   all Todos have completed = true
  --   doesn't change id of any Todo
  --   doesn't change text of any Todo
  -- EditTodo
  --   modifies Todo with given id's text
  --   doesn't change the id
  --   doesn't change completed
  --   doesn't modify other Todos

record Todo : Set where
  field
    text      : String
    completed : Bool
    id        : ℕ

AddTodo : ∀ {n : ℕ} → (Vec Todo n) → String → (Vec Todo (1 + n))
AddTodo todos text =
  todos ∷ʳ
  record
    { id        = 1 -- argmax (λ todo → λ e → e) todos) + 1
    ; completed = false
    ; text      = text
    }

ListAddTodo : List Todo → String → List Todo
ListAddTodo todos text =
  todos l.∷ʳ
  record
    { id        = (max 0 (l.map (λ e → Todo.id e) todos)) + 1
    ; completed = false
    ; text      = text
    }

ListAddTodoAddsNewListItem :
  (todos : List Todo) (text : String) →
    l.length (ListAddTodo todos text) ≡ l.length todos + 1
ListAddTodoAddsNewListItem todos text = length-++ todos

listVec : Vec ℕ 1
listVec = v.fromList (2 l.∷ l.[])

listLast : ℕ
listLast = v.last (v.fromList (2 l.∷ l.[]))

listLastIs2 : v.last (v.fromList (2 l.∷ l.[])) ≡ 2
listLastIs2 = refl

record Id : Set where
  field
    id : ℕ

natListToVec : (xs : List ℕ) → Vec ℕ (l.length xs)
natListToVec nats = v.fromList nats

-- natListLast : List ℕ → ℕ
-- natListLast nats = v.last {(l.length nats) ∸ 1} (v.fromList nats)

-- natListLast : List ℕ → ℕ
-- natListLast []            = 0
-- natListLast nats@(x ∷ xs) = v.last (v.fromList nats)

natListFromList : v.fromList (1 l.∷ l.[]) ≡ (1 v.∷ v.[])
natListFromList = refl

ListOf1sConcatFromList : v.fromList (1 l.∷ l.[] l.++ 1 l.∷ l.[]) ≡ (1 v.∷ v.[] v.++ 1 v.∷ v.[])
ListOf1sConcatFromList = refl

open import Data.Nat.Properties

{-# BUILTIN SIZE     Size   #-}
private
  variable
    a : Level
    A : Set a
    i : Size

vec-length-++ :
  ∀ {n : ℕ} (xs : Vec A n) {ys} →
    v.length (xs v.++ ys) ≡ v.length xs + v.length ys
vec-length-++ xs {ys} = refl

-- vec-fromList-++ :
--   (as bs : List A) →
--     v.fromList (as l.++ bs) ≡ v.fromList as v.++ v.fromList bs
-- vec-fromList-++ []       bs = v.[]
-- vec-fromList-++ (a ∷ as) bs = ?

-- natListConcatFromList : (nats1 : List ℕ) → (nats2 : List ℕ) → v.fromList (nats1 l.++ nats2) ≡ (nats1 v.++ nats2)
-- natListConcatFromList nats = ?

-- natListConcatFromList : (nats : List ℕ) → v.fromList (nats l.++ (1 l.∷ l.[])) ≡ ((v.fromList nats) v.++ (1 v.∷ v.[]))
-- natListConcatFromList = {!   !}

natListLast : List ℕ → ℕ
natListLast [] = 0
natListLast (x ∷ []) = x
natListLast (_ ∷ y ∷ l) = natListLast (y l.∷ l)

natListConcatLast : ∀ l → natListLast (l l.++ l.[ 1 ]) ≡ 1
natListConcatLast [] = refl
natListConcatLast (_ ∷ []) = refl
natListConcatLast (_ ∷ _ ∷ l) = natListConcatLast (_ l.∷ l)

TodoListConcatLast []          = refl
TodoListConcatLast (_ ∷ [])    = refl
TodoListConcatLast (_ ∷ _ ∷ l) = TodoListConcatLast (_ l.∷ l)

TodoListConcatLast : ∀ l → (TodoListLast (l l.++ l.[
  record
    { id        = 1
    ; completed = false
    ; text      = "text"
    }
 ])) ≡
  record
    { id        = 1
    ; completed = false
    ; text      = "text"
    }

TodoListConcatLastCompleted :
  ∀ l →
    Todo.completed (TodoListLast (l l.++ l.[
      record
        { id        = 1
        ; completed = false
        ; text      = "text"
        }
    ])) ≡ false
TodoListConcatLastCompleted []          = refl
TodoListConcatLastCompleted (_ ∷ [])    = refl
TodoListConcatLastCompleted (_ ∷ _ ∷ l) = TodoListConcatLastCompleted (_ l.∷ l)

-- _ : v.last (v.fromList (2 l.∷ l.[] l.++ 1 l.∷ l.[])) ≡ 1
-- _ = refl

-- natListConcatLast : (nats : List ℕ) → natListLast (nats l.++ 1 l.∷ l.[]) ≡ 1
-- natListConcatLast [] = refl
-- natListConcatLast nats@(x ∷ xs) =
--   begin
--     natListLast (nats l.++ 1 l.∷ l.[])
--   ≡⟨⟩
--     v.last (v.fromList ((x l.∷ xs) l.++ 1 l.∷ l.[]))
--   ≡⟨⟩
--     ?
--   ≡⟨⟩
--     1
--   ∎

-- TodoListLast : List Todo → Todo
-- TodoListLast []             = record {}
-- TodoListLast todos@(x ∷ xs) = v.last (v.fromList todos)

-- ListWith2ToVec : v.fromList (2 l.∷ l.[]) ≡ 2 v.∷ v.[]
-- ListWith2ToVec = refl

-- idListLastIdIs2 : Id.id (v.last (v.fromList (record {id = 2} l.∷ l.[]))) ≡ 2
-- idListLastIdIs2 = refl

-- todoListLastIdIs2 : Todo.id (v.last (v.fromList (record {id = 2; text = ""; completed = false} l.∷ l.[]))) ≡ 2
-- todoListLastIdIs2 = refl

-- ListTodoLastTextIsText :
--   (todos : List Todo) (text : String) →
--     Todo.text (v.last (v.fromList (
--       record
--       { text = text
--       ; completed = false
--       ; id = max 0 (l.map Todo.id todos) + 1
--       } l.∷ l.[]
--     ))) ≡ text
-- ListTodoLastTextIsText todos text = refl

-- -- ListAddTodoLastAddedElementIsTodo :
-- --   (todos : List Todo) (text : String) →
-- --     Todo.text (TodoListLast (ListAddTodo todos text)) ≡ text
-- -- ListAddTodoLastAddedElementIsTodo []       text = refl
-- -- ListAddTodoLastAddedElementIsTodo todos@(x ∷ xs) text =
-- --   begin
-- --     Todo.text (TodoListLast (ListAddTodo todos text))
-- --   ≡⟨⟩
-- --     Todo.text (
-- --       TodoListLast (
-- --         todos
-- --         l.++
-- --         (
-- --           record
-- --           { text = text
-- --           ; completed = false
-- --           ; id = max 0 (l.map Todo.id todos) + 1
-- --           }
-- --           l.∷
-- --           l.[]
-- --         )
-- --       )
-- --     )
-- --   ≡⟨⟩
-- --     Todo.text (
-- --       record
-- --       { text = text
-- --       ; completed = false
-- --       ; id = max 0 (l.map Todo.id todos) + 1
-- --       }
-- --     )
-- --   ≡⟨ ? ⟩
-- --     text
-- --   ∎

-- -- open import Data.Nat.Base

-- -- infixr 5 _vb∷ʳ_
-- -- _vb∷ʳ_ : ∀ {n} → Vec≤ A n → A → Vec≤ A (suc n)
-- -- (as , p) vb∷ʳ a = as , s≤s p v.∷ʳ a

-- -- Vec≤AddTodo : ∀ {n : ℕ} → (Vec≤ Todo n) → String → (Vec≤ Todo (1 + n))
-- -- Vec≤AddTodo todos text =
-- --   todos vb∷ʳ
-- --   record
-- --     { id        = 1 -- argmax (λ todo → λ e → e) todos) + 1
-- --     ; completed = false
-- --     ; text      = text
-- --     }

-- vecLength-++ :
--   ∀ {n m} (xs : Vec A n) {ys : Vec A m} →
--     v.length (xs ++ ys) ≡ v.length xs + v.length ys
-- vecLength-++ []       = refl
-- vecLength-++ (x ∷ xs) = cong suc (vecLength-++ xs)

-- AddTodoAddsNewListItem :
--   ∀ {n : ℕ} → (todos : Vec Todo n) (text : String) →
--     v.length (AddTodo todos text) ≡ v.length todos + 1
-- AddTodoAddsNewListItem []       text = refl
-- AddTodoAddsNewListItem (x v.∷ xs) text =
--   begin
--     v.length (AddTodo (x v.∷ xs) text)
--   ≡⟨⟩
--     1 + v.length (x v.∷ xs)
--   ≡⟨ +-comm 1 (v.length (x v.∷ xs))⟩
--     v.length (x v.∷ xs) + 1
--   ∎

-- ListTodoAddTodoAddsNewListItem :
--   (todos : List Todo) (text : String) →
--     l.length (ListAddTodo todos text) ≡ l.length todos + 1
-- ListTodoAddTodoAddsNewListItem []       text = refl
-- ListTodoAddTodoAddsNewListItem todos text =
--   +-comm 1 (l.length todos)

-- AddTodoLastAddedElementIsTodo :
--   ∀ {n} (todos : Vec Todo n) (text : String) →
--     last (AddTodo todos text) ≡
--       record
--         { id        = 1
--         ; completed = false
--         ; text      = text
--         }
-- AddTodoLastAddedElementIsTodo todos text = vecLast todos

-- -- should set (new element).completed to false
-- AddTodoSetsNewCompletedToFalse :
--   ∀ {n} (todos : Vec Todo n) (text : String) →
--     Todo.completed (last (AddTodo todos text)) ≡ false
-- AddTodoSetsNewCompletedToFalse todos text
--   rewrite
--     (AddTodoLastAddedElementIsTodo todos text) =
--       refl
-- -- should set (new element).id to an id not existing already in the list
-- AddTodoSetsNewIdTo1 :
--   ∀ {n} (todos : Vec Todo n) (text : String) →
--     Todo.id (last (AddTodo todos text)) ≡ 1
-- AddTodoSetsNewIdTo1 todos text
--   rewrite
--     (AddTodoLastAddedElementIsTodo todos text) =
--       refl
-- -- TODO should not touch other elements in the list

-- {-# COMPILE JS AddTodo =
--   function (todos) {
--     return function (text) {
--       return [
--         ...todos,
--         {
--           id: todos.reduce((maxId, todo) => Math.max(todo.id, maxId), -1) + 1,
--           completed: false,
--           text: text
--         }
--       ]
--     }
--   }
-- #-}

-- -- DeleteTodo : (List Todo) → ℕ → (List Todo)
-- -- DeleteTodo todos id' = filter (λ todo → Todo.id todo ≟ id') todos

-- open import Relation.Nullary

-- dec-¬ : ∀ {a} {P : Set a} → Dec P → Dec (¬ P)
-- dec-¬ (yes p) = no λ prf → prf p
-- dec-¬ (no ¬p) = yes ¬p

-- VecFilter : Vec≤.vec (v.filter (λ e → e ≟ 2) (2 v.∷ 1 v.∷ v.[])) ≡ (2 v.∷ v.[])
-- VecFilter = refl

-- -- VecFilter' : Vec≤.vec (v.filter (λ e → dec-¬ (e ≟ 2)) (2 v.∷ 1 v.∷ v.[])) ≡ (1 v.∷ v.[])
-- -- VecFilter' = refl

-- -- VecFilter'' : {n : ℕ} → Vec≤.vec (v.filter (λ e → e ≟ 2) (n v.∷ v.[])) ≡ 2 v.∷ v.[]
-- -- VecFilter'' = ?

-- -- VecFilter''' : {n : ℕ} → v.filter (λ e → e ≟ n) (n v.∷ v.[]) ≡ n vb.∷ vb.[]
-- -- VecFilter''' = {!   !}

-- -- ListFilter : l.filter (λ e → e ≟ 2) (2 l.∷ l.[]) ≡ 2 l.∷ l.[]
-- -- ListFilter = refl

-- -- ListFilter' : {n : ℕ} → l.filter (λ e → e ≟ n) (n l.∷ l.[]) ≡ n l.∷ l.[]
-- -- ListFilter' = {!   !}

-- -- DeleteNat : ∀ {n m} → (Vec ℕ n) → ℕ → (Vec ℕ m)
-- -- DeleteNat nats nat = Vec≤.vec (v.filter (λ e → e ≟ nat) nats)

-- DeleteNat : List ℕ → ℕ → List ℕ
-- DeleteNat nats nat = l.filter (λ e → dec-¬ (e ≟ nat)) nats

-- DeleteNat-idem :
--   (nats : List ℕ) →
--     (nat : ℕ) →
--       DeleteNat (DeleteNat nats nat) nat ≡ DeleteNat nats nat
-- DeleteNat-idem nats nat = filter-idem (λ e → dec-¬ (e ≟ nat)) nats
--   -- begin
--   --   DeleteNat (DeleteNat nats nat) nat
--   -- ≡⟨⟩
--   --   DeleteNat (l.filter (λ e → dec-¬ (e ≟ nat)) nats) nat
--   -- ≡⟨⟩
--   --   l.filter (λ e → dec-¬ (e ≟ nat)) (l.filter (λ e → dec-¬ (e ≟ nat)) nats)
--   -- ≡⟨⟩
--   --   (l.filter (λ e → dec-¬ (e ≟ nat)) ∘ l.filter (λ e → dec-¬ (e ≟ nat))) nats
--   -- ≡⟨ filter-idem (λ e → dec-¬ (e ≟ nat)) nats ⟩
--   --   l.filter (λ e → dec-¬ (e ≟ nat)) nats
--   -- ≡⟨⟩
--   --   DeleteNat nats nat
--   -- ∎

-- private
--   variable
--     p : Level

-- -- VecTodoDeleteTodo :
-- --   ∀ {n} →
-- --     (Vec Todo n)
-- --       → ℕ →
-- --         (Vec Todo n)
-- -- VecTodoDeleteTodo todos id' =
-- --   Vec≤.vec (v.filter (λ todo → dec-¬ (Todo.id todo ≟ id')) todos)

-- ListTodoDeleteTodo :
--   ∀ {n} →
--     (List Todo)
--       → ℕ →
--         (List Todo)
-- ListTodoDeleteTodo todos id' =
--   l.filter (λ todo → dec-¬ (Todo.id todo ≟ id')) todos

-- ListTodoDeleteTodo-idem :
--   (todos : List Todo) →
--     (id' : ℕ) →
--       ListTodoDeleteTodo (ListTodoDeleteTodo todos id') id' ≡ ListTodoDeleteTodo todos id'
-- ListTodoDeleteTodo-idem todos id' =
--   filter-idem (λ e → dec-¬ (Todo.id e ≟ id')) todos

-- -- Vec≤DeleteTodo : ∀ {n} → (Vec≤ Todo n) → ℕ → (Vec≤ Todo n)
-- -- Vec≤DeleteTodo todos id' = vb.filter (λ todo → Todo.id todo ≟ id') todos

DeleteNat : (List ℕ) → ℕ → (List ℕ)
DeleteNat nats id = filter' (λ n → not (n ≡ᵇ id)) nats

-- https://stackoverflow.com/questions/65622605/agda-std-lib-list-check-that-a-filtered-list-is-empty/65622709#65622709
DeleteNatRemoveNatWithId :
  (nats : List ℕ) (id : ℕ) →
    filter' (λ n → n ≡ᵇ id) (DeleteNat nats id) ≡ l.[]
DeleteNatRemoveNatWithId []       id         = refl
DeleteNatRemoveNatWithId (x ∷ xs) id with (x ≡ᵇ id) | inspect (_≡ᵇ id) x
... | true  | P.[ eq ] = DeleteNatRemoveNatWithId xs id
... | false | P.[ eq ] rewrite eq = DeleteNatRemoveNatWithId xs id

-- DONT WORK
-- DeleteNatRemoveNatWithId (x ∷ xs) id with x ≡ᵇ id | inspect (l._∷ (filter' (λ n → not (n ≡ᵇ id)) xs)) x
-- ... | true  | P.[ eq ] = DeleteNatRemoveNatWithId xs id
-- ... | false | P.[ eq ] rewrite eq = {!   !}
-- cong (x List.∷_) (DeleteNatRemoveNatWithId xs id)
  -- x List.∷ filter' (λ n → n ≡ᵇ id) (DeleteNat xs id) ≡ x List.∷ List.[]
-- cong (List._∷_) (DeleteNatRemoveNatWithId xs id)
  -- List._∷_ (filter' (λ n → n ≡ᵇ id) (DeleteNat xs id)) ≡ List._∷_ List.[]
-- cong₂ (List._∷_) refl (DeleteNatRemoveNatWithId xs id)
  -- _x_1193 List.∷ filter' (λ n → n ≡ᵇ id) (DeleteNat xs id) ≡ _x_1193 List.∷ List.[]
-- cong₂ (x List.∷_) refl (DeleteNatRemoveNatWithId xs id)
-- cong (filter' (λ n → n ≡ᵇ id) (x List.∷_)) (DeleteNatRemoveNatWithId xs id)
-- cong (filter' (λ n → n ≡ᵇ id)) (DeleteNatRemoveNatWithId xs id)
  -- filter' (λ n → n ≡ᵇ id) (filter' (λ n → n ≡ᵇ id) (DeleteNat xs id)) ≡ List.[]

-- DeleteTodo is well-defined
-- DeleteTodoRemoveTodoWithId :
--   (todos : List Todo) (id : ℕ) →
--     l.filter (λ todo → Todo.id todo ≟ id) (DeleteTodo todos id) ≡ l.[]
-- DeleteTodoRemoveTodoWithId []       id = refl
-- DeleteTodoRemoveTodoWithId (x ∷ xs) id with (Todo.id x ≟ id) | inspect (_≡ᵇ id) (Todo.id x)
-- ... | yes px  | P.[ eq ] = DeleteTodoRemoveTodoWithId xs id
-- ... | no  npx | P.[ eq ] rewrite eq = {!   !}

-- -- filterProof : v.filter (λ e → e ≟ 2) (2 v.∷ v.[]) ≡ (2 vb.∷ vb.[])
-- -- filterProof = refl

-- -- filterProof' : v.filter (λ e → dec-¬ (e ≟ 2)) (2 v.∷ v.[]) ≡ vb.[]
-- -- filterProof' = refl

-- -- dropWhileProof : v.dropWhile (λ e → e ≟ 2) (2 v.∷ 3 v.∷ v.[]) ≡ 3 vb.∷ vb.[]
-- -- dropWhileProof = refl

-- -- dropWhileProof' : v.dropWhile (λ e → e ≟ 3) (2 v.∷ 3 v.∷ v.[]) ≡ (2 vb.∷ 3 vb.∷ vb.[])
-- -- dropWhileProof' = refl

-- -- todoFilterProof :
-- --   v.filter
-- --     (λ todo → dec-¬ ((Todo.id todo) ≟ 2))
-- --     (
-- --       record
-- --         { id        = 2
-- --         ; completed = false
-- --         ; text      = ""
-- --         }
-- --       v.∷
-- --       record
-- --         { id        = 1
-- --         ; completed = false
-- --         ; text      = ""
-- --         }
-- --       v.∷
-- --       v.[]
-- --     )
-- --   ≡
-- --   (
-- --     record
-- --       { id        = 1
-- --       ; completed = false
-- --       ; text      = ""
-- --       }
-- --     vb.∷
-- --     vb.[]
-- --   )
-- -- todoFilterProof = refl

-- -- should remove element from the list unless there are no elements
-- -- should remove element with given id
-- -- DeleteTodoRemoveTodoById :
-- --   ∀ {n : ℕ} (id' : ℕ) (todos : Vec Todo n) →
-- --     padRight
-- --       record
-- --         { id        = 1 -- argmax (λ todo → λ e → e) todos) + 1
-- --         ; completed = false
-- --         ; text      = ""
-- --         }
-- --       (v.filter (λ todo → dec-¬ ((Todo.id todo) ≟ id')) (DeleteTodo todos id'))
-- --     ≡ DeleteTodo todos id'
-- -- DeleteTodoRemoveTodoById id' v.[] = refl
-- -- DeleteTodoRemoveTodoById id' (x v.∷ xs) = {!   !} (DeleteTodoRemoveTodoById xs)

-- -- {-# COMPILE JS DeleteTodo =
-- --   function (todos) {
-- --     return function (id) {
-- --       return todos.filter(function (todo) {
-- --         return todo.id !== id
-- --       });
-- --     }
-- --   }
-- -- #-}
-- -- EditTodo: can't use updateAt since id doesn't necessarily correspond to Vec index
-- VecTodoEditTodo : ∀ {n} → (Vec Todo n) → ℕ → String → (Vec Todo n)
-- VecTodoEditTodo todos id text =
--   v.map (λ todo →
--     if (⌊ Todo.id todo ≟ id ⌋)
--     then record todo { text = text }
--     else todo)
--     todos

-- ListTodoEditTodo : (List Todo) → ℕ → String → (List Todo)
-- ListTodoEditTodo todos id text =
--   l.map (λ todo →
--     if (⌊ Todo.id todo ≟ id ⌋)
--     then record todo { text = text }
--     else todo)
--     todos

-- ListTodoEditTodo-idem :
--   (todos : List Todo) →
--     (id' : ℕ) →
--       (text : String) →
--         ListTodoEditTodo (ListTodoEditTodo todos id' text) id' text ≡ ListTodoEditTodo todos id' text
-- ListTodoEditTodo-idem todos id' text =
--   begin
--     ListTodoEditTodo (ListTodoEditTodo todos id' text) id' text
--   ≡⟨ {!   !} ⟩
--     ListTodoEditTodo todos id' text
--   ∎

-- -- {-# COMPILE JS EditTodo =
-- --   function (todos) {
-- --     return function (id) {
-- --       return function (text) {
-- --         return todos.map(function (todo) {
-- --           if (todo.id === id) {
-- --             todo.text = text;
-- --           }

-- --           return todo;
-- --         });
-- --       }
-- --     }
-- --   }
-- -- #-}

-- VecTodoCompleteTodo : ∀ {n} → (Vec Todo n) → ℕ → (Vec Todo n)
-- VecTodoCompleteTodo todos id =
--   v.map (λ todo →
--     if (⌊ Todo.id todo ≟ id ⌋)
--     then record todo { completed = true }
--     else todo)
--     todos

-- ListTodoCompleteTodo : (List Todo) → ℕ → (List Todo)
-- ListTodoCompleteTodo todos id =
--   l.map (λ todo →
--     if (⌊ Todo.id todo ≟ id ⌋)
--     then record todo { completed = true }
--     else todo)
--     todos

-- ListTodoCompleteTodo-idem :
--   (todos : List Todo) →
--     (id' : ℕ) →
--       ListTodoCompleteTodo (ListTodoCompleteTodo todos id') id' ≡ ListTodoCompleteTodo todos id'
-- ListTodoCompleteTodo-idem todos id' =
--   begin
--     ListTodoCompleteTodo (ListTodoCompleteTodo todos id') id'
--   ≡⟨ {!   !} ⟩
--     ListTodoCompleteTodo todos id'
--   ∎

-- -- {-# COMPILE JS CompleteTodo =
-- --   function (todos) {
-- --     return function (id) {
-- --       return todos.map(function (todo) {
-- --         if (todo.id === id) {
-- --           todo.completed = true;
-- --         }

-- --         return todo;
-- --       });
-- --     }
-- --   }
-- -- #-}

-- CompleteAllTodos : ∀ {n} → (Vec Todo n) → (Vec Todo n)
-- CompleteAllTodos todos =
--   v.map (λ todo →
--     record todo { completed = true })
--     todos

-- ListTodoCompleteAllTodos : (List Todo) → (List Todo)
-- ListTodoCompleteAllTodos todos =
--   l.map (λ todo →
--     record todo { completed = true })
--     todos

-- ListTodoCompleteAllTodos-idem :
--   (todos : List Todo) →
--     ListTodoCompleteAllTodos (ListTodoCompleteAllTodos todos) ≡ ListTodoCompleteAllTodos todos
-- ListTodoCompleteAllTodos-idem todos = {!   !}

-- -- {-# COMPILE JS CompleteAllTodos =
-- --   function (todos) {
-- --     return todos.map(function(todo) {
-- --       todo.completed = true;
-- --       return todo;
-- --     });
-- --   }
-- -- #-}

-- VecTodoClearCompleted : ∀ {n} → (Vec Todo n) → (Vec Todo n)
-- VecTodoClearCompleted todos =
--   padRight
--     record
--       { id        = 1 -- argmax (λ todo → λ e → e) todos) + 1
--       ; completed = false
--       ; text      = ""
--       }
--     (v.filter (λ todo → dec-¬ ((Todo.completed todo) Bool.≟ true)) todos)

-- ListTodoClearCompleted : (List Todo) → (List Todo)
-- ListTodoClearCompleted todos =
--   (l.filter (λ todo → dec-¬ ((Todo.completed todo) Bool.≟ true)) todos)

-- ListTodoClearCompleted-idem :
--   (todos : List Todo) →
--       ListTodoClearCompleted (ListTodoClearCompleted todos) ≡ ListTodoClearCompleted todos
-- ListTodoClearCompleted-idem todos =
--   filter-idem (λ e → dec-¬ (Todo.completed e Bool.≟ true)) todos

-- -- should remove all elements where completed = true
-- -- should not change other elements
-- -- should not change (all elements).text
-- -- should not change (all elements).id

-- -- {-# COMPILE JS ClearCompleted =
-- --   function (todos) {
-- --     return todos.filter(function(todo) {
-- --       return !todo.completed;
-- --     });
-- --   }
-- -- #-}

-- -- add-todos-length-increased-by-1 : ∀ (todos : List Todo) → length (AddTodo todos "test")
-- -- add-todos-length-increased-by-1 = ?
-- -- delete-todos-length-decreased-by-1-except-if-length-0 : ()
-- -- edit-todos-length-not-changed : ()
-- -- complete-todos-length-not-changed : ()
-- -- complete-all-todos-length-not-changed : ()

-- -- clear-completed-todos-not-have-completed : ()

-- -- should not generate duplicate ids after CLEAR_COMPLETE

-- -- data Action : Set where
-- --   ADD_TODO DELETE_TODO EDIT_TODO COMPLETE_TODO COMPLETE_ALL_TODOS CLEAR_COMPLETED : Action

-- -- Reducer : Todos → Action → Todos
-- -- Reducer todos ADD_TODO = AddTodo todos id
-- -- Reducer todos DELETE_TODO = DeleteTodo todos id
-- -- Reducer todos EDIT_TODO = EditTodo todos id
-- -- Reducer todos COMPLETE_TODO = CompleteTodo todos id
-- -- Reducer todos COMPLETE_ALL_TODOS = CompleteAllTodos todos id
-- -- Reducer todos CLEAR_COMPLETED = ClearCompleted todos id

max_stars_repo_name: frankymacster/redux

max_issues_repo_name: frankymacster/redux

max_forks_repo_name: frankymacster/redux


text:
module AmbiguousConstructor where

module Foo where
  data D : Set where
    c0 : D
    c1 : D

module Bar where
  open Foo public

data B : Set where
  tt : B
  ff : B

open Foo renaming (c0 to c2)
open Bar renaming (c1 to c2)

foo : D -> B
-- c2 is ambiguous: it could refer to c0 or c1.
foo c2 = tt
foo _ = ff

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
module List where

import Bool
open Bool

infixr 15 _::_

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

module Eq {A : Set}(_=A=_ : A -> A -> Bool) where

  infix 10 _==_

  _==_ : List A -> List A -> Bool
  []      == []      = true
  x :: xs == y :: ys = (x =A= y) && xs == ys
  []      == _ :: _  = false
  _ :: _  == []      = false

module Subst {A : Set}(_=A=_ : A -> A -> Bool)
             (substA : {x y : A} -> (P : A -> Set) -> IsTrue (x =A= y) -> P x -> P y)
    where

  module EqA = Eq _=A=_
  open EqA

  subst : {xs ys : List A} -> (P : List A -> Set) -> IsTrue (xs == ys) -> P xs -> P ys
  subst {[]     } {_ :: _ } _ () _
  subst {_ :: _ } {[]     } _ () _
  subst {[]     } {[]     } P eq pxs = pxs
  subst {x :: xs} {y :: ys} P eq pxs =
    substA (\z -> P (z :: ys)) x==y (
      subst (\zs -> P (x :: zs)) xs==ys pxs
    )
    where
      x==y : IsTrue (x =A= y)
      x==y = isTrue&&₁ {x =A= y}{xs == ys} eq

      xs==ys : IsTrue (xs == ys)
      xs==ys = isTrue&&₂ {x =A= y}{xs == ys} eq

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2014-09-09

{-# TERMINATING #-}
Foo : Set
Foo = Foo


text:
-- Reported by Nisse on 2018-03-13

-- The `x` in the parent pattern was eta-expanded to `record{}`,
-- but with-abstraction didn't like this.

open import Agda.Builtin.Equality

record R : Set where

postulate
  easy : (A : Set) → A

F : (x : R) → Set₁
F x with easy (x ≡ x)
F x | refl with Set
F x | refl | _ = Set

-- OLD ERROR:
-- With clause pattern x is not an instance of its parent pattern
-- record {}

-- Fixed by allowing parent patterns to be replaced by variables
-- in the with clause (but checking that their instantiation is
-- type-correct).

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- {-# OPTIONS -vtc.with.strip:60 -v tc.lhs.top:50 #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

postulate trustMe : {A : Set} (x y : A) → x ≡ y

data Fin : Nat → Set where
  fzero : ∀ n → Fin (suc n)
  fsuc  : ∀{n} → Fin n → Fin (suc n)

test1 : ∀{n} → Fin n → Nat
test1 (fzero _) = 0
test1 {.(suc n)} (fsuc {n} i) with Fin zero
... | q = {!.!}
-- Current & expected expansion:
-- test1 {.(suc n)} (fsuc {n} i) | q = {!!}

test2 : ∀{n} → Fin n → Nat
test2 (fzero _) = 0
test2 {.(suc n)} (fsuc {n} i) with trustMe n zero
... | refl = {!.!}
-- Current & expected expansion:
-- test2 {.1} (fsuc {.0} i) | refl = {!!}

-- The test cases below do not yet work correctly, but are included
-- here as documentation of the current behaviour of Agda. does not
-- work correctly yet.

test3 : ∀{n} → Fin n → Nat
test3 (fzero _) = 0
test3 {m} (fsuc {n} i) with Fin zero
... | q = {!.!}
-- Current expansion:
-- test3 {.(suc _)} (fsuc {_} i) | q = {!!}
-- Expected expansion:
-- test3 {.(suc n)} (fsuc {n} i) | q = { }

test4 : ∀{n} → Fin n → Nat
test4 (fzero _) = 0
test4 {_} (fsuc {n} i) with Fin zero
... | q = {!.!}
-- Current expansion:
-- test4 {.(suc _)} (fsuc {_} i) | q = {!!}
-- Expected expansion:
-- test4 {_} (fsuc {n} i) | q = {!!}

test5 : ∀{n : Nat} → Fin n → Nat → Nat
test5 (fzero _) _ = 0
test5 {.(suc n)} (fsuc {n} i) m with trustMe m n
... | refl = {!.!}
-- Current expansion:
-- test5 {.(suc n)} (fsuc {n} i) n | refl = {!!}
-- Expected expansion: one of the following:
-- test5 {.(suc n)} (fsuc {n} i) .n | refl = {!!}
-- test5 {.(suc m)} (fsuc {.m} i) m | refl = {!!}

test6 : Nat → ∀{n : Nat} → Fin n → Nat
test6 _ (fzero _) = 0
test6 m {.(suc n)} (fsuc {n} i) with trustMe m n
... | refl = {!.!}
-- Current expansion:
-- test6 m {.(suc m)} (fsuc {.m} i) | refl = {!!}
-- This one is actually good, we should be sure fixing the above
-- examples doesn't change the output here!


text:
open import Prelude
open import core

module grounding where
  grounding : ∀{ τ1 τ2} →
                             τ1 ▸gnd τ2 →
                             ((τ2 ground) × (τ1 ~ τ2) × (τ1 ≠ τ2))
  grounding (MGArr x) = GHole , TCArr TCHole1 TCHole1 , x
  grounding (MGProd x) = GProd , TCProd TCHole1 TCHole1 , x

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


text:
------------------------------------------------------------------------
-- The unit type
------------------------------------------------------------------------

module Data.Unit where

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

------------------------------------------------------------------------
-- Types

-- Note that the name of this type is "\top", not T.

record ⊤ : Set where

tt : ⊤
tt = record {}

record _≤_ (x y : ⊤) : Set where

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

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

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

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

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

preorder : Preorder
preorder = PropEq.preorder ⊤

setoid : Setoid
setoid = PropEq.setoid ⊤

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

decSetoid : DecSetoid
decSetoid = DecTotalOrder.Eq.decSetoid decTotalOrder

poset : Poset
poset = DecTotalOrder.poset decTotalOrder

max_issues_repo_name: larrytheliquid/Lemmachine


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Empty type
------------------------------------------------------------------------

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

module Data.Empty where

open import Level

data ⊥ : Set where

⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
⊥-elim ()


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

open import Categories.Category
open import Categories.Object.Terminal
open import Level

module Categories.Object.Terminal.Products {o ℓ e : Level}
    (C : Category o ℓ e)
    (T : Terminal C) where

open import Categories.Object.Product

open Category C
open Terminal T

[⊤×⊤] : Obj
[⊤×⊤] = ⊤

[⊤×⊤]-product : Product C ⊤ ⊤
[⊤×⊤]-product = record
    { A×B       = [⊤×⊤]
    ; π₁        = !
    ; π₂        = !
    ; ⟨_,_⟩     = λ _ _ → !
    ; commute₁  = !-unique₂ _ _
    ; commute₂  = !-unique₂ _ _
    ; universal = λ _ _ → !-unique _
    }

[⊤×_] : Obj → Obj
[⊤× X ] = X

[⊤×_]-product : (X : Obj) → Product C ⊤ X
[⊤×_]-product X = record
    { A×B       = [⊤× X ]
    ; π₁        = !
    ; π₂        = id
    ; ⟨_,_⟩     = λ _ f → f
    ; commute₁  = !-unique₂ _ _
    ; commute₂  = identityˡ
    ; universal = λ {A}{f}{g}{i} _ id∘i≡g →
        begin
            g
        ↑⟨ id∘i≡g ⟩
            id ∘ i
        ↓⟨ identityˡ ⟩
            i
        ∎
    } where open HomReasoning

[_×⊤] : Obj → Obj
[ X ×⊤] = X

[_×⊤]-product : (X : Obj) → Product C X ⊤
[_×⊤]-product X = record
    { A×B       = [ X ×⊤]
    ; π₁        = id
    ; π₂        = !
    ; ⟨_,_⟩     = λ f _ → f
    ; commute₁  = identityˡ
    ; commute₂  = !-unique₂ _ _
    ; universal = λ {A}{f}{g}{i} id∘i≡f _ →
        begin
            f
        ↑⟨ id∘i≡f ⟩
            id ∘ i
        ↓⟨ identityˡ ⟩
            i
        ∎
    } where open HomReasoning

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module everything where

open import lib public

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


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

open import Cubical.HITs.SetQuotients.Base public
open import Cubical.HITs.SetQuotients.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import HoTT

module homotopy.WedgeOfCircles {i} where

WedgeOfCircles : (I : Type i) → Type i
WedgeOfCircles I = BigWedge {A = I} (λ _ → ⊙S¹)

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

open import LogicalFormulae
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Lists.Lists
open import Rings.Homomorphisms.Definition

module Rings.Polynomial.Evaluation {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where

open Ring R
open Setoid S
open Equivalence eq
open Group additiveGroup
open import Groups.Polynomials.Definition additiveGroup
open import Groups.Polynomials.Addition additiveGroup
open import Rings.Polynomial.Ring R
open import Rings.Polynomial.Multiplication R

inducedFunction : NaivePoly → A → A
inducedFunction [] a = 0R
inducedFunction (x :: p) a = x + (a * inducedFunction p a)

inducedFunctionMult : (as : NaivePoly) (b c : A) → inducedFunction (map (_*_ b) as) c ∼ (inducedFunction as c) * b
inducedFunctionMult [] b c = symmetric (transitive *Commutative timesZero)
inducedFunctionMult (x :: as) b c = transitive (transitive (+WellDefined reflexive (transitive (transitive (*WellDefined reflexive (inducedFunctionMult as b c)) *Associative) *Commutative)) (symmetric *DistributesOver+)) *Commutative

inducedFunctionWellDefined : {a b : NaivePoly} → polysEqual a b → (c : A) → inducedFunction a c ∼ inducedFunction b c
inducedFunctionWellDefined {[]} {[]} a=b c = reflexive
inducedFunctionWellDefined {[]} {x :: b} (fst ,, snd) c = symmetric (transitive (+WellDefined fst (transitive (*WellDefined reflexive (symmetric (inducedFunctionWellDefined {[]} {b} snd c))) (timesZero {c}))) identRight)
inducedFunctionWellDefined {a :: as} {[]} (fst ,, snd) c = transitive (+WellDefined fst reflexive) (transitive identLeft (transitive (*WellDefined reflexive (inducedFunctionWellDefined {as} {[]} snd c)) (timesZero {c})))
inducedFunctionWellDefined {a :: as} {b :: bs} (fst ,, snd) c = +WellDefined fst (*WellDefined reflexive (inducedFunctionWellDefined {as} {bs} snd c))

inducedFunctionGroupHom : {x y : NaivePoly} → (a : A) → inducedFunction (x +P y) a ∼ (inducedFunction x a + inducedFunction y a)
inducedFunctionGroupHom {[]} {[]} a = symmetric identLeft
inducedFunctionGroupHom {[]} {x :: y} a rewrite mapId y = symmetric identLeft
inducedFunctionGroupHom {x :: xs} {[]} a rewrite mapId xs = symmetric identRight
inducedFunctionGroupHom {x :: xs} {y :: ys} a = transitive (symmetric +Associative) (transitive (+WellDefined reflexive (transitive (transitive (+WellDefined reflexive (transitive (*WellDefined reflexive (transitive (inducedFunctionGroupHom {xs} {ys} a) groupIsAbelian)) *DistributesOver+)) +Associative) groupIsAbelian)) +Associative)

inducedFunctionRingHom : (r s : NaivePoly) (a : A) → inducedFunction (r *P s) a ∼ (inducedFunction r a * inducedFunction s a)
inducedFunctionRingHom [] s a = symmetric (transitive *Commutative timesZero)
inducedFunctionRingHom (x :: xs) [] a = symmetric timesZero
inducedFunctionRingHom (b :: bs) (c :: cs) a = transitive (+WellDefined reflexive (*WellDefined reflexive (inducedFunctionGroupHom {map (_*_ b) cs +P map (_*_ c) bs} {0G :: (bs *P cs)} a))) (transitive (+WellDefined reflexive (*WellDefined reflexive (+WellDefined (inducedFunctionGroupHom {map (_*_ b) cs} {map (_*_ c) bs} a) identLeft))) (transitive (transitive (transitive (+WellDefined reflexive (transitive (transitive (transitive (*WellDefined reflexive (transitive (+WellDefined (transitive groupIsAbelian (+WellDefined (inducedFunctionMult bs c a) (inducedFunctionMult cs b a))) (transitive (transitive (*WellDefined reflexive (transitive (inducedFunctionRingHom bs cs a) *Commutative)) *Associative) *Commutative)) (symmetric +Associative))) *DistributesOver+) (+WellDefined reflexive *DistributesOver+)) (+WellDefined *Associative (+WellDefined (transitive *Associative *Commutative) *Associative)))) +Associative) (+WellDefined (symmetric *DistributesOver+') (symmetric *DistributesOver+'))) (symmetric *DistributesOver+)))

inducedFunctionIsHom : (a : A) → RingHom polyRing R (λ p → inducedFunction p a)
RingHom.preserves1 (inducedFunctionIsHom a) = transitive (+WellDefined reflexive (timesZero {a})) identRight
RingHom.ringHom (inducedFunctionIsHom a) {r} {s} = inducedFunctionRingHom r s a
GroupHom.groupHom (RingHom.groupHom (inducedFunctionIsHom a)) {x} {y} = inducedFunctionGroupHom {x} {y} a
GroupHom.wellDefined (RingHom.groupHom (inducedFunctionIsHom a)) x=y = inducedFunctionWellDefined x=y a


text:
module MLib.Fin.Parts.Core where

open import MLib.Prelude

open Nat using (_*_; _+_; _<_)
open Table

record Parts {a} (A : Set a) (size : A → ℕ) : Set a where
  field
    numParts : ℕ
    parts : Table A numParts

  partAt = lookup parts
  sizeAt = size ∘ partAt
  totalSize = sum (map size parts)
  partsizes = tabulate sizeAt

constParts : ℕ → ℕ → Parts ℕ id
constParts numParts partsize = record
  { numParts = numParts
  ; parts = replicate partsize
  }


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

module Data.Ternary where

open import Prelude
open import Relation.Nullary.Discrete.FromBoolean

infixl 5 _,0 _,1 _,2
data Tri : Type where
  0t : Tri
  _,0 _,1 _,2 : Tri → Tri

infix 4 _≡ᴮ_
_≡ᴮ_ : Tri → Tri → Bool
0t   ≡ᴮ 0t   = true
x ,0 ≡ᴮ y ,0 = x ≡ᴮ y
x ,1 ≡ᴮ y ,1 = x ≡ᴮ y
x ,2 ≡ᴮ y ,2 = x ≡ᴮ y
_    ≡ᴮ _    = false

sound : ∀ x y → T (x ≡ᴮ y) → x ≡ y
sound 0t     0t     p = refl
sound (x ,0) (y ,0) p = cong _,0 (sound x y p)
sound (x ,1) (y ,1) p = cong _,1 (sound x y p)
sound (x ,2) (y ,2) p = cong _,2 (sound x y p)

complete : ∀ x → T (x ≡ᴮ x)
complete 0t = tt
complete (x ,0) = complete x
complete (x ,1) = complete x
complete (x ,2) = complete x

_≟_ : (x y : Tri) → Dec (x ≡ y)
_≟_ = from-bool-eq _≡ᴮ_ sound complete

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Sublist where

open import Data.List
open import Data.List.All
open import Data.List.Any
open import Level
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Function
open import Category.Monad
open import Data.Product

open import Membership-equality hiding (_⊆_; set)

infix 3 _⊆_

-- Sublist without re-ordering, to be improved later...
data _⊆_ {a}{A : Set a} : List A → List A → Set a where
  []   : ∀ {ys} → [] ⊆ ys
  keep : ∀ {x xs ys} → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
  skip : ∀ {x xs ys} → xs ⊆ ys → xs ⊆ x ∷ ys

singleton-⊆ : ∀ {a} {A : Set a} {x : A} {xs : List A} → x ∈ xs → [ x ] ⊆ xs
singleton-⊆ (here refl) = keep []
singleton-⊆ (there mem) = skip (singleton-⊆ mem)

reflexive-⊆ : ∀ {a} {A : Set a} {xs : List A} → xs ⊆ xs
reflexive-⊆ {xs = []} = []
reflexive-⊆ {xs = x ∷ xs} = keep reflexive-⊆

All-⊆ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} → xs ⊆ ys → All P ys → All P xs
All-⊆ [] al = []
All-⊆ (keep inc) (px ∷ al) = px ∷ All-⊆ inc al
All-⊆ (skip inc) (px ∷ al) =  All-⊆ inc al

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
{-

This file contains:
  - The reduced version gives the same type as James.

-}
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.HITs.James.Inductive.ColimitEquivalence where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Pointed

open import Cubical.HITs.James.Base
  renaming (James to JamesConstruction)
open import Cubical.HITs.James.Inductive.Reduced
  renaming (𝕁Red to 𝕁RedConstruction ; 𝕁Red∞ to 𝕁amesConstruction)
open import Cubical.HITs.James.Inductive.Coherence

private
  variable
    ℓ : Level

module _
  ((X , x₀) : Pointed ℓ) where

  private
    James = JamesConstruction (X , x₀)
    𝕁ames = 𝕁amesConstruction (X , x₀)
    𝕁Red  =  𝕁RedConstruction (X , x₀)

  -- Mimicking the constructors in each other

  unit' : (x : X)(xs : James) → Path James (x₀ ∷ x ∷ xs) (x ∷ x₀ ∷ xs)
  unit' x xs = sym (unit (x ∷ xs)) ∙∙ refl ∙∙ (λ i → x ∷ unit xs i)

  coh' : (xs : James) → refl ≡ unit' x₀ xs
  coh' xs i j =
    coh-helper {A = James} (unit xs) (unit (x₀ ∷ xs))
      (λ i → x₀ ∷ unit xs i) (λ i j → unit (unit xs j) i) i j

  _∷∞_ : X → 𝕁ames → 𝕁ames
  _∷∞_ x (inl xs) = inl (x ∷ xs)
  _∷∞_ x (push xs i) = (push (x ∷ xs) ∙ (λ i → inl (unit x xs i))) i

  push∞ : (xs : 𝕁ames) → xs ≡ x₀ ∷∞ xs
  push∞ (inl xs) = push xs
  push∞ (push xs i) j =
    push-helper {A = 𝕁ames} (push xs) (push (x₀ ∷ xs))
      (λ i → inl (unit x₀ xs i)) (λ i j → inl (coh xs i j)) j i

  infixr 5 _∷∞_

  -- One side map

  𝕁→James-inl : 𝕁Red → James
  𝕁→James-inl [] = []
  𝕁→James-inl (x ∷ xs) = x ∷ 𝕁→James-inl xs
  𝕁→James-inl (unit x xs i) = unit' x (𝕁→James-inl xs) i
  𝕁→James-inl (coh xs i j) = coh' (𝕁→James-inl xs) i j

  𝕁→James : 𝕁ames → James
  𝕁→James (inl xs) = 𝕁→James-inl xs
  𝕁→James (push xs i) = unit (𝕁→James-inl xs) i

  -- Commutativity with pseudo-constructors

  𝕁→James-∷ : (x : X)(xs : 𝕁ames) → 𝕁→James (x ∷∞ xs) ≡ x ∷ 𝕁→James xs
  𝕁→James-∷ x (inl xs) = refl
  𝕁→James-∷ x (push xs i) j = comp-cong-helper 𝕁→James (push (x ∷ xs)) _ (λ i → inl (unit x xs i)) refl j i

  𝕁→James-push : (xs : 𝕁ames)
    → PathP (λ i → 𝕁→James xs ≡ 𝕁→James-∷ x₀ xs i) (cong 𝕁→James (push∞ xs)) (unit (𝕁→James xs))
  𝕁→James-push (inl xs) = refl
  𝕁→James-push (push xs i) j k =
    hcomp (λ l → λ
      { (i = i0) → unit (𝕁→James-inl xs) k
      ; (i = i1) → unit (x₀ ∷ 𝕁→James-inl xs) k
      ; (j = i0) →
          push-helper-cong 𝕁→James (push xs) (push (x₀ ∷ xs))
            (λ i → inl (unit x₀ xs i)) (λ i j → inl (coh xs i j)) k i (~ l)
      ; (j = i1) → unit (unit (𝕁→James-inl xs) i) k
      ; (k = i0) → unit (𝕁→James-inl xs) i
      ; (k = i1) →
          comp-cong-helper-filler 𝕁→James (push (x₀ ∷ xs)) _
            (λ i → inl (unit x₀ xs i)) refl j i l })
    (push-coh-helper _ _ _ (λ i j → unit (unit (𝕁→James-inl xs) j) i) k i j)

  -- The other-side map

  private
    push-square : (x : X)(xs : 𝕁Red)
      → sym (push (x ∷ xs)) ∙∙ refl ∙∙ (λ i → x ∷∞ push xs i) ≡ (λ i → inl (unit x xs i))
    push-square x xs i j = push-square-helper (push (x ∷ xs)) (λ i → inl (unit x xs i)) i j

    coh-cube : (xs : 𝕁Red)
      → SquareP
          (λ i j → coh-helper _ _ _ (λ i j → push∞ (push xs j) i) i j ≡ inl (coh xs i j))
          (λ i j → inl (x₀ ∷ x₀ ∷ xs))
          (λ i j → push-square-helper (push (x₀ ∷ xs))
                    (λ i → inl (unit x₀ xs i)) j i)
          (λ i j → inl (x₀ ∷ x₀ ∷ xs))
          (λ i j → inl (x₀ ∷ x₀ ∷ xs))
    coh-cube xs =
      coh-cube-helper {A = 𝕁ames} (push xs) (push (x₀ ∷ xs))
        (λ i → inl (unit x₀ xs i)) (λ i j → inl (coh xs i j))

  J→𝕁ames : James → 𝕁ames
  J→𝕁ames [] = inl []
  J→𝕁ames (x ∷ xs) = x ∷∞ (J→𝕁ames xs)
  J→𝕁ames (unit xs i) = push∞ (J→𝕁ames xs) i

  -- The following is the most complicated part.
  -- It seems horrible but mainly it's due to correction of boudaries.

  𝕁→J→𝕁ames-inl : (xs : 𝕁Red) → J→𝕁ames (𝕁→James (inl xs)) ≡ inl xs
  𝕁→J→𝕁ames-inl [] = refl
  𝕁→J→𝕁ames-inl (x ∷ xs) t = x ∷∞ 𝕁→J→𝕁ames-inl xs t
  𝕁→J→𝕁ames-inl (unit x xs i) j =
    hcomp (λ k → λ
      { (i = i0) → square-helper (j ∨ ~ k) i0
      ; (i = i1) → square-helper (j ∨ ~ k) i1
      ; (j = i0) → square-helper (~ k) i
      ; (j = i1) → inl (unit x xs i) })
    (push-square x xs j i)
    where
      square-helper : (i j : I) → 𝕁ames
      square-helper i j =
        doubleCompPath-cong-filler J→𝕁ames
          (sym (unit (x ∷ 𝕁→James-inl xs))) refl (λ i → x ∷ unit (𝕁→James-inl xs) i)
          (λ i j → push∞ (x ∷∞ 𝕁→J→𝕁ames-inl xs i) (~ j))
          (λ i j → x ∷∞ 𝕁→J→𝕁ames-inl xs i)
          (λ i j → x ∷∞ push∞ (𝕁→J→𝕁ames-inl xs i) j) i j i1
  𝕁→J→𝕁ames-inl (coh xs i j) k =
    hcomp (λ l → λ
      { (i = i0) → cube-helper i0 j (k ∨ ~ l)
      ; (i = i1) → inl-filler j k l
      ; (j = i0) → cube-helper i i0 (k ∨ ~ l)
      ; (j = i1) → cube-helper i i1 (k ∨ ~ l)
      ; (k = i0) → cube-helper i j (~ l)
      ; (k = i1) → inl (coh xs i j) })
    (coh-cube xs i j k)
    where
      cube-helper : (i j k : I) → 𝕁ames
      cube-helper i j k =
        coh-helper-cong J→𝕁ames _ _ _
          (λ i j → unit (unit (𝕁→James-inl xs) j) i)
          (λ i j k → push∞ (push∞ (𝕁→J→𝕁ames-inl xs k) j) i) i j k

      inl-filler : (i j k : I) → 𝕁ames
      inl-filler i j k =
        hfill (λ k → λ
          { (i = i0) → square-helper (j ∨ ~ k) i0
          ; (i = i1) → square-helper (j ∨ ~ k) i1
          ; (j = i0) → square-helper (~ k) i
          ; (j = i1) → inl (unit x₀ xs i) })
        (inS (push-square x₀ xs j i)) k
        where
          square-helper : (i j : I) → 𝕁ames
          square-helper i j =
            doubleCompPath-cong-filler J→𝕁ames
              (sym (unit (x₀ ∷ 𝕁→James-inl xs))) refl (λ i → x₀ ∷ unit (𝕁→James-inl xs) i)
              (λ i j → push∞ (x₀ ∷∞ 𝕁→J→𝕁ames-inl xs i) (~ j))
              (λ i j → x₀ ∷∞ 𝕁→J→𝕁ames-inl xs i)
              (λ i j → x₀ ∷∞ push∞ (𝕁→J→𝕁ames-inl xs i) j) i j i1

  -- The main equivalence

  𝕁→J→𝕁ames : (xs : 𝕁ames) → J→𝕁ames (𝕁→James xs) ≡ xs
  𝕁→J→𝕁ames (inl xs) = 𝕁→J→𝕁ames-inl xs
  𝕁→J→𝕁ames (push xs i) j = push∞ (𝕁→J→𝕁ames-inl xs j) i

  J→𝕁→James : (xs : James) → 𝕁→James (J→𝕁ames xs) ≡ xs
  J→𝕁→James [] = refl
  J→𝕁→James (x ∷ xs) = 𝕁→James-∷ x (J→𝕁ames xs) ∙ (λ i → x ∷ J→𝕁→James xs i)
  J→𝕁→James (unit xs i) j =
    hcomp (λ k → λ
      { (i = i0) → J→𝕁→James xs (j ∧ k)
      ; (i = i1) → compPath-filler (𝕁→James-∷ x₀ (J→𝕁ames xs)) (λ i → x₀ ∷ J→𝕁→James xs i) k j
      ; (j = i0) → 𝕁→James (J→𝕁ames (unit xs i))
      ; (j = i1) → unit (J→𝕁→James xs k) i })
    (𝕁→James-push (J→𝕁ames xs) j i)

  James≃𝕁Red∞ : James ≃ 𝕁ames
  James≃𝕁Red∞ = isoToEquiv (iso J→𝕁ames 𝕁→James 𝕁→J→𝕁ames J→𝕁→James)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- 2017-06-16, reported by Ambrus Kaposi on the Agda mailing list

-- WAS:
-- β  is not a legal rewrite rule, since the left-hand side
-- f a  reduces to  f a
-- when checking the pragma REWRITE β

-- SHOULD: succeed

{-# OPTIONS --rewriting #-}

module _ where

module a where

postulate
  _~_ : {A : Set} → A → A → Set

{-# BUILTIN REWRITE _~_ #-}

module m1 (X : Set) where

  postulate
    A B : Set
    a : A
    b : B
    f : A → B

module m2 (X : Set) where

  open m1 X

  postulate
    β : f a ~ b

  {-# REWRITE β #-}

  postulate
    refl : {A : Set}{a : A} → a ~ a

  p : f a ~ b
  p = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --show-implicit #-}

module Substitution where


text:
import      Lvl
open import Data.Boolean
open import Type

module Data.List.Sorting {ℓ} {T : Type{ℓ}} (_≤?_ : T → T → Bool) where

open import Functional using (_∘₂_)
open import Data.Boolean.Stmt
open import Data.List
import      Data.List.Relation.Pairwise
open import Data.List.Relation.Permutation
open import Logic

open Data.List.Relation.Pairwise using (empty ; single ; step) public
Sorted = Data.List.Relation.Pairwise.AdjacentlyPairwise(IsTrue ∘₂ (_≤?_))

-- A sorting algorithm is a function that given a list, always return a sorted list which is a permutation of the original one.
record SortingAlgorithm (f : List(T) → List(T)) : Stmt{Lvl.𝐒(ℓ)} where
  constructor intro
  field
    ⦃ sorts ⦄    : ∀{l} → Sorted(f(l))
    ⦃ permutes ⦄ : ∀{l} → (f(l) permutes l)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K #-}
module NTypes.Sigma where

open import NTypes
open import PathOperations
open import PathStructure.Sigma
open import Transport
open import Types

Σ-isSet : ∀ {a b} {A : Set a} {B : A → Set b} →
  isSet A → (∀ x → isSet (B x)) → isSet (Σ A B)
Σ-isSet {A = A} {B = B} A-set B-set x y p q
  = split-eq p ⁻¹
  · ap₂-dep-eq {B = B} _,_
      (ap π₁ p)
      (ap π₁ q)
      π₁-eq
      (tr-∘ π₁ p (π₂ x) ⁻¹ · apd π₂ p)
      (tr-∘ π₁ q (π₂ x) ⁻¹ · apd π₂ q)
      π₂-eq
  · split-eq q
  where
  split-eq : (p : x ≡ y) →
    ap₂-dep {B = B} _,_ (ap π₁ p)
      (tr-∘ π₁ p (π₂ x) ⁻¹  · apd π₂ p) ≡ p
  split-eq = π₂ (π₂ (π₂ split-merge-eq))

  π₁-eq : ap π₁ p ≡ ap π₁ q
  π₁-eq = A-set _ _ (ap π₁ p) (ap π₁ q)

  π₂-eq : tr (λ z → tr B z (π₂ x) ≡ π₂ y) π₁-eq
            (tr-∘ π₁ p (π₂ x) ⁻¹ · apd π₂ p)
        ≡ tr-∘ π₁ q (π₂ x) ⁻¹ · apd π₂ q
  π₂-eq = B-set _ (tr B (ap π₁ q) (π₂ x)) (π₂ y)
    (tr
      (λ z → tr B z (π₂ x) ≡ π₂ y)
      π₁-eq
      (tr-∘ π₁ p (π₂ x) ⁻¹ · apd π₂ p))
    (tr-∘ π₁ q (π₂ x) ⁻¹ · apd π₂ q)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


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

module Fragment.Setoid.Morphism.Setoid where

open import Fragment.Setoid.Morphism.Base

open import Level using (Level; _⊔_)
open import Relation.Binary using (Setoid; IsEquivalence; Rel)

private
  variable
    a b ℓ₁ ℓ₂ : Level

module _ {S : Setoid a ℓ₁} {T : Setoid b ℓ₂} where

  open Setoid T

  infix 4 _≗_

  _≗_ : Rel (S ↝ T) (a ⊔ ℓ₂)
  f ≗ g = ∀ {x} → ∣ f ∣ x ≈ ∣ g ∣ x

  ≗-refl : ∀ {f} → f ≗ f
  ≗-refl = refl

  ≗-sym : ∀ {f g} → f ≗ g → g ≗ f
  ≗-sym f≗g {x} = sym (f≗g {x})

  ≗-trans : ∀ {f g h} → f ≗ g → g ≗ h → f ≗ h
  ≗-trans f≗g g≗h {x} = trans (f≗g {x}) (g≗h {x})

  ≗-isEquivalence : IsEquivalence _≗_
  ≗-isEquivalence = record { refl  = λ {f} → ≗-refl {f}
                           ; sym   = λ {f g} → ≗-sym {f} {g}
                           ; trans = λ {f g h} → ≗-trans {f} {g} {h}
                           }

_↝_/≗ : Setoid a ℓ₁ → Setoid b ℓ₂ → Setoid _ _
S ↝ T /≗ = record { Carrier       = S ↝ T
                  ; _≈_           = _≗_
                  ; isEquivalence = ≗-isEquivalence
                  }

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
open import Common.Prelude
open import Common.Reflect

module TermSplicingOutOfScope where

f : Set → Set → Set → Set
f x y z = unquote (var 3 [])

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Data.List.First.Membership {ℓ}{A : Set ℓ} where

open import Data.Product
open import Data.List
open import Data.List.Relation.Unary.Any
open import Data.List.First hiding (find)
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Level
open import Function
open import Data.Empty

_∈_ : A → List A → Set _
x ∈ l = first x ∈ l ⇒ (_≡_ x)

¬x∈[] : ∀ {x} → ¬ x ∈ []
¬x∈[] ()

find : Decidable (_≡_ {A = A}) → ∀ x l → Dec (x ∈ l)
find _≟_ x [] = no (λ ())
find _≟_ x (y ∷ l) with x ≟ y
... | yes refl = yes (here refl)
... | no  neq  with find _≟_ x l
... | yes p    = yes (there y neq p)
... | no  ¬p   = no (λ{ (here eq) → neq eq ; (there _ _ p) → ¬p p})


text:
------------------------------------------------------------------------
-- Nullary relations (some core definitions)
------------------------------------------------------------------------

-- The definitions in this file are reexported by Relation.Nullary.

module Relation.Nullary.Core where

open import Data.Empty

-- Negation.

infix 3 ¬_

¬_ : Set → Set
¬ P = P → ⊥

-- Decidable relations.

data Dec (P : Set) : Set where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P


text:
open import Agda.Primitive

f : ∀ {a b c} → Set a → Set b → Set c → Set {!!} -- WAS solution: (a ⊔ (b ⊔ c))
f A B C = A → B → C                              -- NOW:          (a ⊔ b ⊔ c)


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

module Cubical.Categories.Instances.Functors where

open import Cubical.Categories.Category
open import Cubical.Categories.Functor.Base
open import Cubical.Categories.NaturalTransformation.Base
open import Cubical.Categories.NaturalTransformation.Properties
open import Cubical.Categories.Morphism renaming (isIso to isIsoC)
open import Cubical.Foundations.Prelude

private
  variable
    ℓC ℓC' ℓD ℓD' : Level

module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where
  open Category
  open NatTrans
  open Functor

  FUNCTOR : Category (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) (ℓ-max (ℓ-max ℓC ℓC') ℓD')
  ob FUNCTOR           = Functor C D
  Hom[_,_] FUNCTOR     = NatTrans
  id FUNCTOR {F}       = idTrans F
  _⋆_ FUNCTOR          = seqTrans
  ⋆IdL FUNCTOR α       = makeNatTransPath λ i x → D .⋆IdL (α .N-ob x) i
  ⋆IdR FUNCTOR α       = makeNatTransPath λ i x → D .⋆IdR (α .N-ob x) i
  ⋆Assoc FUNCTOR α β γ = makeNatTransPath λ i x → D .⋆Assoc (α .N-ob x) (β .N-ob x) (γ .N-ob x) i
  isSetHom FUNCTOR     = isSetNat

  open isIsoC renaming (inv to invC)
  -- componentwise iso is an iso in Functor
  FUNCTORIso : ∀ {F G : Functor C D} (α : F ⇒ G)
             → (∀ (c : C .ob) → isIsoC D (α ⟦ c ⟧))
             → isIsoC FUNCTOR α
  FUNCTORIso α is .invC .N-ob c = (is c) .invC
  FUNCTORIso {F} {G} α is .invC .N-hom {c} {d} f
    = invMoveL areInv-αc
               ( α ⟦ c ⟧ ⋆⟨ D ⟩ (G ⟪ f ⟫ ⋆⟨ D ⟩ is d .invC)
               ≡⟨ sym (D .⋆Assoc _ _ _) ⟩
                 (α ⟦ c ⟧ ⋆⟨ D ⟩ G ⟪ f ⟫) ⋆⟨ D ⟩ is d .invC
               ≡⟨ sym (invMoveR areInv-αd (α .N-hom f)) ⟩
                 F ⟪ f ⟫
               ∎ )
    where
      areInv-αc : areInv _ (α ⟦ c ⟧) ((is c) .invC)
      areInv-αc = isIso→areInv (is c)

      areInv-αd : areInv _ (α ⟦ d ⟧) ((is d) .invC)
      areInv-αd = isIso→areInv (is d)
  FUNCTORIso α is .sec = makeNatTransPath (funExt (λ c → (is c) .sec))
  FUNCTORIso α is .ret = makeNatTransPath (funExt (λ c → (is c) .ret))

max_stars_repo_name: mzeuner/cubical

max_issues_repo_name: mzeuner/cubical

max_forks_repo_name: mzeuner/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lemmas relating algebraic definitions (such as associativity and
-- commutativity) that don't the equality relation to be a setoid.
------------------------------------------------------------------------

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

module Algebra.Consequences.Base
  {a} {A : Set a} where

open import Algebra.Core
open import Algebra.Definitions
open import Data.Sum.Base
open import Relation.Binary.Core

sel⇒idem : ∀ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) →
           Selective _≈_ _•_ → Idempotent _≈_ _•_
sel⇒idem _ sel x with sel x x
... | inj₁ x•x≈x = x•x≈x
... | inj₂ x•x≈x = x•x≈x


text:
------------------------------------------------------------------------
-- Undecidability of subtyping in Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Undecidable where

open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Decidable

open import FOmegaInt.Syntax
open import FOmegaInt.Typing as Declarative
open import FOmegaInt.Kinding.Canonical as Canonical
open import FOmegaInt.Kinding.Canonical.Equivalence
open import FOmegaInt.Undecidable.SK
open import FOmegaInt.Undecidable.Encoding
open import FOmegaInt.Undecidable.Decoding

open Syntax
open ContextConversions using (⌞_⌟Ctx)
open Canonical.Kinding  using (_⊢_<:_⇇_)
open Declarative.Typing using (_⊢_<:_∈_)
open Encoding
module T = TermCtx
module E = ElimCtx

------------------------------------------------------------------------
-- SK combinator term equality checking reduces to subtype checking in
-- Fω with interval kinds.
--
-- We do not proof undecidability of subtyping directly, but give a
-- reduction from undecidability of checking the equivalence of two SK
-- combinator terms, which is well-known to be undecidable.  In other
-- words, if we could check subtyping, we could also check the
-- equality of two SK combinator terms, which we cannot.
--
-- The following types characterize the decision procedures involved.

SKEqualityCheck : Set
SKEqualityCheck = (s t : SKTerm) → Dec (s ≡SK t)

CanoncialSubtypeCheck : Set
CanoncialSubtypeCheck = ∀ {n} (Γ : E.Ctx n) a b k → Dec (Γ ⊢ a <: b ⇇ k)

DeclarativeSubtypeCheck : Set
DeclarativeSubtypeCheck = ∀ {n} (Γ : T.Ctx n) a b k → Dec (Γ ⊢ a <: b ∈ k)

-- The reduction from SK equality checking to canoncial subtype checking.

module CanoncialReduction (check-<:⇇ : CanoncialSubtypeCheck) where

  canonicalEquivalence : ∀ s t → Γ-SK? ⊢ encode s <: encode t ⇇ ⌜*⌝ ⇔ s ≡SK t
  canonicalEquivalence s t = equivalence decode-<:⇇-encode <:⇇-encode

  check-≡SK : SKEqualityCheck
  check-≡SK s t =
    map (canonicalEquivalence s t) (check-<:⇇ Γ-SK? (encode s) (encode t) ⌜*⌝)

canonicalReduction : CanoncialSubtypeCheck → SKEqualityCheck
canonicalReduction = CanoncialReduction.check-≡SK

-- The reduction from SK equality checking to declarative subtype checking.

module DeclarativeReduction (check-<:∈ : DeclarativeSubtypeCheck) where

  declarativeEquivalence :
    ∀ s t → ⌞Γ-SK?⌟ ⊢ ⌞ encode s ⌟ <: ⌞ encode t ⌟ ∈ * ⇔ s ≡SK t
  declarativeEquivalence s t = equivalence
    (λ es<:et∈* → decode-<:⇇-encode
        (subst₂ (_ ⊢_<:_⇇ _) (nf-encode s) (nf-encode t) (complete-<: es<:et∈*)))
    (λ s≡t → sound-<:⇇ (<:⇇-encode s≡t))

  check-≡SK : SKEqualityCheck
  check-≡SK s t =
    map (declarativeEquivalence s t)
        (check-<:∈ ⌞Γ-SK?⌟ ⌞ encode s ⌟ ⌞ encode t ⌟ *)

declarativeReduction : DeclarativeSubtypeCheck → SKEqualityCheck
declarativeReduction = DeclarativeReduction.check-≡SK

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


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

module Data.List.Smart where

open import Prelude

open import Data.Nat.Properties using (_≡ᴮ_; complete-==)

infixr 5 _∷′_ _++′_
data List {a} (A : Type a) : Type a where
  []′ : List A
  _∷′_ : A → List A → List A
  _++′_ : List A → List A → List A

sz′ : List A → ℕ → ℕ
sz′ []′ k = k
sz′ (x ∷′ xs) k = k
sz′ (xs ++′ ys) k = suc (sz′ xs (sz′ ys k))

sz : List A → ℕ
sz []′ = zero
sz (x ∷′ xs) = zero
sz (xs ++′ ys) = sz′ xs (sz ys)

_HasSize_ : List A → ℕ → Type
xs HasSize n = T (sz xs ≡ᴮ n)

data ListView {a} (A : Type a) : Type a where
  Nil : ListView A
  Cons : A → List A → ListView A

viewˡ : List A → ListView A
viewˡ xs = go xs (sz xs) (complete-== (sz xs))
  where
  go : (xs : List A) → (n : ℕ) → xs HasSize n → ListView A
  go  []′                  n       p = Nil
  go  (x ∷′ xs)            n       p = Cons x xs
  go  ((x ∷′ xs) ++′ ys)   n       p = Cons x (xs ++′ ys)
  go  ([]′ ++′ ys)         n       p = go ys n p
  go  ((xs ++′ ys) ++′ zs) (suc n) p = go (xs ++′ (ys ++′ zs)) n p


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists made up entirely of unique elements (propositional equality)
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.Unique.Propositional {a} {A : Set a} where

open import Relation.Binary.PropositionalEquality using (setoid)
open import Data.List.Relation.Unary.Unique.Setoid as SetoidUnique

------------------------------------------------------------------------
-- Re-export the contents of setoid uniqueness

open SetoidUnique (setoid A) public


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

open import Base
open import Homotopy.Pushout
open import Homotopy.VanKampen.Guide

module Homotopy.VanKampen.Code.LemmaPackB {i} (d : pushout-diag i)
  (l : legend i (pushout-diag.C d)) where

  open pushout-diag d
  open legend l

  open import Homotopy.Truncation
  open import Homotopy.PathTruncation
  open import Homotopy.VanKampen.SplitCode d l

  abstract
    trans-q-code-a : ∀ {a₁ a₂} (q : a₁ ≡ a₂) {a₃} (p : _ ≡₀ a₃)
      → transport (λ x → code-a x a₃) q (a a₁ p)
      ≡ a a₂ (proj (! q) ∘₀ p)
    trans-q-code-a refl p = ap (λ x → a _ x) $ ! $ refl₀-left-unit p

    trans-!q-code-a : ∀ {a₁ a₂} (q : a₂ ≡ a₁) {a₃} (p : _ ≡₀ a₃)
      → transport (λ x → code-a x a₃) (! q) (a a₁ p)
      ≡ a a₂ (proj q ∘₀ p)
    trans-!q-code-a refl p = ap (λ x → a _ x) $ ! $ refl₀-left-unit p

    trans-q-code-ba : ∀ {a₁ a₂} (q : a₁ ≡ a₂) {a₃} n co (p : _ ≡₀ a₃)
      → transport (λ x → code-a x a₃) q (ba a₁ n co p)
      ≡ ba a₂ n (transport (λ x → code-b x (g $ loc n)) q co) p
    trans-q-code-ba refl n co p = refl

    trans-q-code-ab : ∀ {a₁ a₂} (q : a₁ ≡ a₂) {b₃} n co (p : _ ≡₀ b₃)
      → transport (λ x → code-b x b₃) q (ab a₁ n co p)
      ≡ ab a₂ n (transport (λ x → code-a x (f $ loc n)) q co) p
    trans-q-code-ab refl n co p = refl

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

data Bool : Set where true false : Bool

op : Bool → Set → Set
op false _ = Bool
op true  A = A

postulate
  id : Bool → Bool
  id-comp : ∀ y → id y ≡ y
  {-# REWRITE id-comp #-}

postulate
  A : Set
  law : (i : Bool) → op (id i) A ≡ Bool
  {-# REWRITE law #-}

ok : (i : Bool) → op i A ≡ Bool
ok i = refl


text:
-- 2010-09-24
-- example originally stolen from Andrea Vezzosi's post on the Agda list

{-# OPTIONS --no-irrelevant-projections #-}

module IrrelevantRecordFields where

open import Common.Equality

record SemiG : Set1 where
 constructor _,_,_,_,_,_
 field
   M    : Set
   unit : M
   _+_  : M -> M -> M
   .assoc     : ∀ {x y z} ->  x + (y + z) ≡ (x + y) + z
   .leftUnit  : ∀ {x} -> unit + x ≡ x
   .rightUnit : ∀ {x} -> x + unit ≡ x

dual : SemiG -> SemiG
dual (M , e , _+_ , assoc , leftUnit , rightUnit) =
  M , e , (λ x y -> y + x) , sym assoc , rightUnit , leftUnit

open SemiG

-- trivId : ∀ (M : SemiG) -> M ≡ M
-- trivId M = refl

dual∘dual≡id : ∀ M -> dual (dual M) ≡ M
dual∘dual≡id M = refl {x = M}

max_stars_repo_name: larrytheliquid/agda


text:
-- An ATP type must be used with data-types or postulates.

-- This error is detected by Syntax.Translation.ConcreteToAbstract.

module ATPBadType1 where

data Bool : Set where
  false true : Bool

{-# ATP type false #-}

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Machine words: basic type and conversion functions
------------------------------------------------------------------------

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

module Data.Word.Base where

open import Level using (zero)
import Data.Nat.Base as ℕ
open import Function
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Re-export built-ins publicly

open import Agda.Builtin.Word public
  using (Word64)
  renaming
  ( primWord64ToNat   to toℕ
  ; primWord64FromNat to fromℕ
  )

infix 4 _≈_
_≈_ : Rel Word64 zero
_≈_ = _≡_ on toℕ

infix 4 _<_
_<_ : Rel Word64 zero
_<_ = ℕ._<_ on toℕ


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

-- The Category of Algebraic Kan Complexes
module Categories.Category.Instance.KanComplexes where

open import Level

open import Function using (_$_)
open import Data.Product using (Σ; _,_; proj₁)

open import Categories.Category
open import Categories.Category.SubCategory
open import Categories.Category.Construction.KanComplex
open import Categories.Category.Instance.SimplicialSet

import Categories.Category.Instance.SimplicialSet.Properties as ΔSetₚ

import Categories.Morphism.Reasoning as MR

module _ (o ℓ : Level) where
  open Category (SimplicialSet o ℓ)
  open ΔSetₚ o ℓ
  open IsKanComplex
  open Equiv
  open MR (SimplicialSet o ℓ)

  -- As we are working with Algebraic Kan Complexes, maps between two Kan Complexes ought
  -- to take the chosen filler in 'X' to the chosen filler in 'Y'.
  PreservesFiller : ∀ {X Y : ΔSet} → IsKanComplex o ℓ X → IsKanComplex o ℓ Y → (X ⇒ Y) → Set (o ⊔ ℓ)
  PreservesFiller {X} {Y} X-Kan Y-Kan f = ∀ {n} {k} → (i : Λ[ n , k ] ⇒ X) → (f ∘ filler X-Kan {n} i) ≈ filler Y-Kan (f ∘ i)

  KanComplexes : Category (suc o ⊔ suc ℓ) (o ⊔ ℓ ⊔ (o ⊔ ℓ)) (o ⊔ ℓ)
  KanComplexes = SubCategory (SimplicialSet o ℓ) {I = Σ ΔSet (IsKanComplex o ℓ)} $ record
    { U = proj₁
    ; R = λ { {_ , X-Kan} {_ , Y-Kan} f → PreservesFiller X-Kan Y-Kan f }
    ; Rid = λ { {_ , X-Kan} i → begin
        id ∘ filler X-Kan i   ≈⟨ identityˡ {f = filler X-Kan i} ⟩
        filler X-Kan i        ≈˘⟨ filler-cong X-Kan (identityˡ {f = i}) ⟩
        filler X-Kan (id ∘ i) ∎
      }
    ; _∘R_ = λ { {_ , X-Kan} {_ , Y-Kan} {_ , Z-Kan} {f} {g} f-preserves g-preserves i → begin
        (f ∘ g) ∘ filler X-Kan i ≈⟨ assoc {f = filler X-Kan i} {g = g} {h = f} ⟩
        f ∘ (g ∘ filler X-Kan i) ≈⟨ ∘-resp-≈ʳ {f = (g ∘ filler X-Kan i)} {h = filler Y-Kan (g ∘ i)} {g = f} (g-preserves i) ⟩
        f ∘ filler Y-Kan (g ∘ i) ≈⟨ f-preserves (g ∘ i) ⟩
        filler Z-Kan (f ∘ g ∘ i) ≈˘⟨ filler-cong Z-Kan (assoc {f = i} {g = g} {h = f}) ⟩
        filler Z-Kan ((f ∘ g) ∘ i) ∎
      }
    }
    where
      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:
{-# OPTIONS --without-K #-}

open import HoTT

module homotopy.PathSetIsInital {i} (A : Type i)
  -- (A-conn : is-connected 0 A)
  where

  open Cover

  module _
    (a₁ : A)
    -- And an arbitrary covering.
    {k} (cov : Cover A k)
    -- (cov-conn : is-connected 0 (Cover.TotalSpace cov))
    (a↑₁ : Fiber cov a₁)
    where

    private
      univ-cover = path-set-cover ⊙[ A , a₁ ]

    -- Weak initiality by transport.
    quotient-cover : CoverHom univ-cover cov
    quotient-cover _ p = cover-trace cov a↑₁ p

    -- Strong initiality by path induction.
    module Uniqueness
      (cover-hom : CoverHom univ-cover cov)
      (pres-a↑₁ : cover-hom a₁ idp₀ == a↑₁)
      where

      private
        lemma₁ : ∀ a p → cover-hom a [ p ] == quotient-cover a [ p ]
        lemma₁ ._ idp = pres-a↑₁

        lemma₂ : ∀ a p → cover-hom a p == quotient-cover a p
        lemma₂ a = Trunc-elim
          (λ p → =-preserves-level 0 (Cover.Fiber-level cov a))
          (lemma₁ a)

      theorem : cover-hom == quotient-cover
      theorem = λ= λ a → λ= $ lemma₂ a

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


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

mutual

  data E : Set where
    e : F -> E

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

data ⊥ : Set where

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

mutual

  empty : E
  empty = e empty?

  empty? : F
  f empty? = empty

absurd : ⊥
absurd = elim empty

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Generic.Test.Data.List where

module _ where
  open import Generic.Main as Main hiding ([]; _∷_) renaming (List to StdList)

  infixr 5 _∷_ _∷′_

  List : ∀ {α} -> Set α -> Set α
  List = readData StdList

  pattern []       = #₀ lrefl
  pattern _∷_ x xs = !#₁ (relv x , xs , lrefl)

  _∷′_ : ∀ {α} {A : Set α} -> A -> List A -> List A
  _∷′_ = _∷_

  elimList : ∀ {α π} {A : Set α}
           -> (P : List A -> Set π)
           -> (∀ {xs} x -> P xs -> P (x ∷ xs))
           -> P []
           -> ∀ xs
           -> P xs
  elimList P f z  []      = z
  elimList P f z (x ∷ xs) = f x (elimList P f z xs)

  toStdList : ∀ {α} {A : Set α} -> List A -> StdList A
  toStdList xs = guncoerce xs

-- The entire content of `Data.List.Base` (modulo `Generic.Test.Data.Maybe` instead of
-- `Data.Maybe.Base` and _∷_ was renamed to _∷′_ in some places)

open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Data.Bool.Base using (Bool; false; true; not; _∧_; _∨_; if_then_else_)
open import Generic.Test.Data.Maybe
open import Data.Product as Prod using (_×_; _,_)
open import Function

infixr 5 _++_

[_] : ∀ {a} {A : Set a} → A → List A
[ x ] = x ∷ []

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

-- Snoc.

infixl 5 _∷ʳ_

_∷ʳ_ : ∀ {a} {A : Set a} → List A → A → List A
xs ∷ʳ x = xs ++ [ x ]

null : ∀ {a} {A : Set a} → List A → Bool
null []       = true
null (x ∷ xs) = false

-- * List transformations

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

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

zipWith : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
          → (A → B → C) → List A → List B → List C
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
zipWith f _        _        = []

zip : ∀ {a b} {A : Set a} {B : Set b} → List A → List B → List (A × B)
zip = zipWith (_,_)

intersperse : ∀ {a} {A : Set a} → A → List A → List A
intersperse x []           = []
intersperse x (y ∷ [])     = [ y ]
intersperse x (y ∷ z ∷ zs) = y ∷ x ∷ intersperse x (z ∷ zs)

-- * Reducing lists (folds)

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

foldl : ∀ {a b} {A : Set a} {B : Set b} → (A → B → A) → A → List B → A
foldl c n []       = n
foldl c n (x ∷ xs) = foldl c (c n x) xs

-- ** Special folds

concat : ∀ {a} {A : Set a} → List (List A) → List A
concat = foldr _++_ []

concatMap : ∀ {a b} {A : Set a} {B : Set b} →
            (A → List B) → List A → List B
concatMap f = concat ∘ map f

and : List Bool → Bool
and = foldr _∧_ true

or : List Bool → Bool
or = foldr _∨_ false

any : ∀ {a} {A : Set a} → (A → Bool) → List A → Bool
any p = or ∘ map p

all : ∀ {a} {A : Set a} → (A → Bool) → List A → Bool
all p = and ∘ map p

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

product : List ℕ → ℕ
product = foldr _*_ 1

length : ∀ {a} {A : Set a} → List A → ℕ
length = foldr (λ _ → suc) 0

import Data.List.Base

reverse : ∀ {a} {A : Set a} → List A → List A
reverse = foldl (λ rev x → x ∷′ rev) []

-- * Building lists

-- ** Scans

scanr : ∀ {a b} {A : Set a} {B : Set b} →
        (A → B → B) → B → List A → List B
scanr f e []       = e ∷ []
scanr f e (x ∷ xs) with scanr f e xs
... | []     = []                -- dead branch
... | y ∷ ys = f x y ∷ y ∷ ys

scanl : ∀ {a b} {A : Set a} {B : Set b} →
        (A → B → A) → A → List B → List A
scanl f e []       = e ∷ []
scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs

-- ** Unfolding

-- Unfold. Uses a measure (a natural number) to ensure termination.

unfold : ∀ {a b} {A : Set a} (B : ℕ → Set b)
         (f : ∀ {n} → B (suc n) → Maybe (A × B n)) →
         ∀ {n} → B n → List A
unfold B f {n = zero}  s = []
unfold B f {n = suc n} s with f s
... | nothing       = []
... | just (x , s') = x ∷ unfold B f s'

-- downFrom 3 = 2 ∷ 1 ∷ 0 ∷ [].

downFrom : ℕ → List ℕ
downFrom n = unfold Singleton f (wrap n)
  where
  data Singleton : ℕ → Set where
    wrap : (n : ℕ) → Singleton n

  f : ∀ {n} → Singleton (suc n) → Maybe (ℕ × Singleton n)
  f {n} (wrap .(suc n)) = just (n , wrap n)

-- ** Conversions

fromMaybe : ∀ {a} {A : Set a} → Maybe A → List A
fromMaybe (just x) = [ x ]
fromMaybe nothing  = []

-- * Sublists

-- ** Extracting sublists

take : ∀ {a} {A : Set a} → ℕ → List A → List A
take zero    xs       = []
take (suc n) []       = []
take (suc n) (x ∷ xs) = x ∷ take n xs

drop : ∀ {a} {A : Set a} → ℕ → List A → List A
drop zero    xs       = xs
drop (suc n) []       = []
drop (suc n) (x ∷ xs) = drop n xs

splitAt : ∀ {a} {A : Set a} → ℕ → List A → (List A × List A)
splitAt zero    xs       = ([] , xs)
splitAt (suc n) []       = ([] , [])
splitAt (suc n) (x ∷ xs) with splitAt n xs
... | (ys , zs) = (x ∷ ys , zs)

takeWhile : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
takeWhile p []       = []
takeWhile p (x ∷ xs) with p x
... | true  = x ∷ takeWhile p xs
... | false = []

dropWhile : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
dropWhile p []       = []
dropWhile p (x ∷ xs) with p x
... | true  = dropWhile p xs
... | false = x ∷ xs

span : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
span p []       = ([] , [])
span p (x ∷ xs) with p x
... | true  = Prod.map (_∷′_ x) id (span p xs)
... | false = ([] , x ∷ xs)

break : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
break p = span (not ∘ p)

inits : ∀ {a} {A : Set a} → List A → List (List A)
inits []       = [] ∷ []
inits (x ∷ xs) = [] ∷ map (_∷′_ x) (inits xs)

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

infixl 5 _∷ʳ'_

data InitLast {a} {A : Set a} : List A → Set a where
  []ʳ   : InitLast []
  _∷ʳ'_ : (xs : List A) (x : A) → InitLast (xs ∷ʳ x)

initLast : ∀ {a} {A : Set a} (xs : List A) → InitLast xs
initLast []               = []ʳ
initLast (x ∷ xs)         with initLast xs
initLast (x ∷ .[])        | []ʳ      = [] ∷ʳ' x
initLast (x ∷ .(ys ∷ʳ y)) | ys ∷ʳ' y = (x ∷ ys) ∷ʳ' y

-- * Searching lists

-- ** Searching with a predicate

-- A generalised variant of filter.

gfilter : ∀ {a b} {A : Set a} {B : Set b} →
          (A → Maybe B) → List A → List B
gfilter p []       = []
gfilter p (x ∷ xs) with p x
... | just y  = y ∷ gfilter p xs
... | nothing =     gfilter p xs

filter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
filter p = gfilter (λ x → if p x then just′ x else nothing)

partition : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
partition p []       = ([] , [])
partition p (x ∷ xs) with p x | partition p xs
... | true  | (ys , zs) = (x ∷ ys , zs)
... | false | (ys , zs) = (ys , x ∷ zs)

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
------------------------------------------------------------------------
-- Code related to the paper "Total Definitional Interpreters for Time
-- and Space Complexity"
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

-- Note that the code has evolved after the paper was written. For
-- code that is closer to the paper, see the version of the code that
-- is distributed with the paper.

module README where

------------------------------------------------------------------------
-- Pointers to results from the paper

-- In order to more easily find code corresponding to results from the
-- paper, see the following module. Note that some of the code
-- referenced below is not discussed at all in the paper.

import README.Pointers-to-results-from-the-paper

------------------------------------------------------------------------
-- Responses to some challenges from Ancona, Dagnino and Zucca

-- The syntax of a toy programming language that only supports
-- allocation and deallocation of memory.

import Only-allocation

-- Definitional interpreters can model systems with bounded space.

import Bounded-space

-- Upper bounds of colists containing natural numbers.

import Upper-bounds

-- Definitional interpreters can model systems with unbounded space.

import Unbounded-space

------------------------------------------------------------------------
-- An example involving a simple λ-calculus

-- Some developments based on "Operational Semantics Using the
-- Partiality Monad" by Danielsson.
--
-- These developments to a large extent mirror developments in
-- "Coinductive big-step operational semantics" by Leroy and Grall.
--
-- The main differences compared to those two pieces of work are
-- perhaps the following ones:
--
-- * Sized types are used.
--
-- * The infinite set of uninterpreted constants has been replaced by
--   booleans, and definitions (named, unary, recursive functions)
--   are included.
--
-- * The virtual machine and the compiler include support for tail
--   calls.
--
-- * Stack space usage is analysed.

-- The syntax of, and a type system for, an untyped λ-calculus with
-- booleans and recursive unary function calls.

import Lambda.Syntax

-- A delay monad with the possibility of crashing.

import Lambda.Delay-crash

-- A definitional interpreter.

import Lambda.Interpreter

-- A type soundness result.

import Lambda.Type-soundness

-- A combination of the delay monad (with the possibility of crashing)
-- and a kind of writer monad yielding colists.

import Lambda.Delay-crash-trace

-- Virtual machine instructions, state etc.

import Lambda.Virtual-machine.Instructions

-- A virtual machine.

import Lambda.Virtual-machine

-- A compiler.

import Lambda.Compiler

-- Compiler correctness.

import Lambda.Compiler-correctness

-- A definitional interpreter that is instrumented with information
-- about the stack size of the compiled program.

import Lambda.Interpreter.Stack-sizes

-- The actual maximum stack size of the compiled program matches the
-- maximum stack size of the instrumented source-level semantics.

import Lambda.Compiler-correctness.Sizes-match

-- An example: A non-terminating program that runs in bounded stack
-- space.

import Lambda.Interpreter.Stack-sizes.Example

-- A counterexample: The trace of stack sizes produced by the virtual
-- machine is not necessarily bisimilar to that produced by the
-- instrumented interpreter.

import Lambda.Interpreter.Stack-sizes.Counterexample

-- A counterexample: The number of steps taken by the uninstrumented
-- interpreter is not, in general, linear in the number of steps taken
-- by the virtual machine for the corresponding compiled program.

import Lambda.Interpreter.Steps.Counterexample

-- A definitional interpreter that is instrumented with information
-- about the number of steps required to run the compiled program.

import Lambda.Interpreter.Steps

-- The "time complexity" of the compiled program matches the one
-- obtained from the instrumented interpreter.

import Lambda.Compiler-correctness.Steps-match

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


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

module Prob where

open import DescTT

mutual
  data Sch : Set where
    ty   : (S : Set) -> Sch
    exPi : (s : Sch)(T : toType s -> Sch) -> Sch
    imPi : (S : Set)(T : S -> Sch) -> Sch

  toType : Sch -> Set
  toType (ty S)     = S
  toType (exPi s T) = (x : toType s) -> toType (T x)
  toType (imPi S T) = (x : S) -> toType (T x)

Args : Sch -> Set
Args (ty _)     = Unit
Args (exPi s T) = Sigma (toType s) \ x -> Args (T x)
Args (imPi S T) = Sigma S \ x -> Args (T x)

postulate
  UId : Set
  Prp : Set
  Prf : Prp -> Set

data Prob : Set where
  label : (u : UId)(s : Sch)(a : Args s) -> Prob
  patPi : (u : UId)(S : Set)(p : Prob) -> Prob
  hypPi : (p : Prp)(T : Prf p -> Prob) -> Prob
  recPi : (rec : Prob)(p : Prob) -> Prob

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram


text:
{-# OPTIONS --without-K #-}
module HoTT.Equivalence.Proposition where

open import HoTT.Base
open import HoTT.HLevel
open import HoTT.Equivalence

open variables

-- Proven by Theorem 4.3.2
postulate
  isequiv-prop : {f : A → B} → isProp (isequiv f)

{-
  fib : B → 𝒰 _
  fib y = Σ[ x ∶ A ] (f x == y)

  -- Left inverse with coherence
  lcoh : linv → 𝒰 _
  lcoh (g , η) = Σ[ ε ∶ f ∘ g ~ id ] ap g ∘ ε ~ η ∘ g

  -- Right inverse with coherence
  rcoh : rinv → 𝒰 _
  rcoh (g , ε) = Σ[ η ∶ g ∘ f ~ id ] ap f ∘ η ~ ε ∘ f
-}

{-
hae-fib-contr : {f : A → B} → ishae f → (y : B) → isContr (fib f y)
hae-fib-contr {A = A} {f = f} (g , η , ε , τ) y = (g y , ε y) , contr
  where
  contr : (z : fib f y) → (g y , ε y) == z
  contr (x , p) = pair⁼ (qₓ , qₚ)
    where
    qₓ : g y == x
    qₓ = ap g p ⁻¹ ∙ η x
    qₚ : transport (λ x → f x == y) qₓ (ε y) == p
    qₚ = begin
      transport (λ x → f x == y) qₓ (ε y)      =⟨ transport=-constᵣ f y qₓ (ε y) ⟩
      ap f qₓ ⁻¹ ∙ ε y                         =⟨ ap (λ p → p ⁻¹ ∙ ε y) (ap-∙ f (ap g p ⁻¹) (η x)) ⟩
      (ap f (ap g p ⁻¹) ∙ ap f (η x)) ⁻¹ ∙ ε y =⟨ ap (λ p → p ⁻¹ ∙ ε y) (ap (ap f) (ap-⁻¹ g p ⁻¹) ⋆ τ x) ⟩
      (ap f (ap g (p ⁻¹)) ∙ ε (f x)) ⁻¹ ∙ ε y  =⟨ ap (λ p → (p ∙ ε (f x)) ⁻¹ ∙ ε y) (ap-∘ f g (p ⁻¹)) ⟩
      (ap (f ∘ g) (p ⁻¹) ∙ ε (f x)) ⁻¹ ∙ ε y   =⟨ ap (λ p → p ⁻¹ ∙ ε y) (~-naturality ε (p ⁻¹) ⁻¹) ⟩
      (ε y ∙ ap id (p ⁻¹)) ⁻¹ ∙ ε y            =⟨ ap (λ p → (ε y ∙ p) ⁻¹ ∙ ε y) (ap-id (p ⁻¹)) ⟩
      (ε y ∙ p ⁻¹) ⁻¹ ∙ ε y                    =⟨ ∙-⁻¹ (ε y) (p ⁻¹) ∙ᵣ ε y ⟩
      p ⁻¹ ⁻¹ ∙ ε y ⁻¹ ∙ ε y                   =⟨ ∙-assoc _ _ _ ⁻¹ ⟩
      p ⁻¹ ⁻¹ ∙ (ε y ⁻¹ ∙ ε y)                 =⟨ invinv p ⋆ ∙-invₗ (ε y) ⟩
      p ∙ refl                                 =⟨ ∙-unitᵣ p ⁻¹ ⟩
      p                                        ∎
      where
      open =-Reasoning
      ∙-⁻¹ : {A : 𝒰 i} {x y z : A} (p : x == y) (q : y == z) → (p ∙ q) ⁻¹ == q ⁻¹ ∙ p ⁻¹
      ∙-⁻¹ refl refl = refl
      invinv : {A : 𝒰 i} {x y : A} (p : x == y) → p ⁻¹ ⁻¹ == p
      invinv refl = refl

linv-contr : {f : A → B} → qinv f → isContr (linv f)
linv-contr {f = f} (g , η , ε) = {!hae-fib-contr (qinv→ishae e)!}
  where
  q' : qinv (_∘ f)
  q' = _∘ g , (λ x → ap (x ∘_) {!funext ?!}) , {!!}
rinv-contr : {f : A → B} → qinv f → isContr (rinv f)
rinv-contr = {!!}
-}

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
{-# OPTIONS --safe #-}
module STLC.Operational.Eager where

open import STLC.Syntax
open import STLC.Operational.Base
open import Data.Empty using (⊥-elim)
open import Data.Product using (∃-syntax; _,_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Fin using (Fin; _≟_) renaming (zero to fzero; suc to fsuc)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong)
open import Relation.Nullary using (yes; no; ¬_)

private
  variable
    m n : ℕ
    L M M' N N' : Term n
    A B C : Type
    Γ Δ : Ctx n
    v : Fin n

data Value {n} : Term n → Set where
  abs-value
      -----------------
    : Value (abs A M)
  ⋆-value
      -----------------
    : Value ⋆
  pair-value
    : Value M → Value N
      -----------------
    → Value (pair M N)

infix 6 _↦_

data _↦_ : Term n → Term n → Set where
  red-head
    : M ↦ M'
      ------------------
    → app M N ↦ app M' N
  red-arg
    : Value M → N ↦ N'
      ------------------
    → app M N ↦ app M N'
  red-β
    : Value N
      ---------------------------------
    → app (abs A M) N ↦ M [ fzero ≔ N ]
  red-left
    : M ↦ M'
      --------------------
    → pair M N ↦ pair M' N
  red-right
    : Value M     → N ↦ N'
      --------------------
    → pair M N ↦ pair M N'
  red-projₗ-inner
    : M ↦ M'
      ------------------
    → projₗ M ↦ projₗ M'
  red-projₗ
    : Value M → Value N
      --------------------
    → projₗ (pair M N) ↦ M
  red-projᵣ-inner
    : M ↦ M'
      ------------------
    → projᵣ M ↦ projᵣ M'
  red-projᵣ
    : Value M → Value N
      --------------------
    → projᵣ (pair M N) ↦ N

data  _↦*_ : Term n → Term n → Set where
  pure : M ↦ N → M ↦* N
  id : M ↦* M
  comp : L ↦* M → M ↦* N → L ↦* N

open import STLC.Typing

progress : ● ⊢ M ⦂ A → Value M ⊎ (∃[ N ] (M ↦ N))
progress (ty-abs _) = inj₁ abs-value
progress (ty-app {f = f} {x = x} t u) with progress u | progress t
... | inj₁ u-value | inj₁ (abs-value {M = M}) = inj₂ (M [ fzero ≔ x ] , red-β u-value)
... | inj₂ (u' , u-step) | inj₁ t-value = inj₂ (app f u' , red-arg t-value u-step)
... | inj₁ _ | inj₂ (t' , t-step) = inj₂ (app t' x , red-head t-step)
... | inj₂ _ | inj₂ (t' , t-step) = inj₂ (app t' x , red-head t-step)
progress ty-⋆ = inj₁ ⋆-value
progress (ty-pair {a = a} {b = b} t u) with progress t | progress u
... | inj₁ t-value | inj₁ u-value = inj₁ (pair-value t-value u-value)
... | inj₁ t-value | inj₂ (u' , u-step) = inj₂ (pair a u' , red-right t-value u-step)
... | inj₂ (t' , t-step) | _ = inj₂ (pair t' b , red-left t-step)
progress (ty-projₗ t) with progress t
... | inj₁ (pair-value {M = M} M-value N-value) = inj₂ (M , red-projₗ M-value N-value)
... | inj₂ (t' , t-step) = inj₂ (projₗ t' , red-projₗ-inner t-step)
progress (ty-projᵣ t) with progress t
... | inj₁ (pair-value {N = N} M-value N-value) = inj₂ (N , red-projᵣ M-value N-value)
... | inj₂ (t' , t-step) = inj₂ (projᵣ t' , red-projᵣ-inner t-step)

weakening-var
  : ∀ {Γ : Ctx n} {v' : Fin (suc n)} → Γ ∋ v ⦂ A → liftΓ Γ v' B ∋ Data.Fin.punchIn v' v ⦂ A
weakening-var {v' = fzero} vzero = vsuc vzero
weakening-var {v' = fsuc n} vzero = vzero
weakening-var {v' = fzero} (vsuc v) = vsuc (vsuc v)
weakening-var {v' = fsuc n} (vsuc v) = vsuc (weakening-var v)

-- | The weakening lemma: A term typeable in a context is typeable in an extended context.
--
-- https://www.seas.upenn.edu/~sweirich/dsss17/html/Stlc.Lec2.html
weakening
  : ∀ {Γ : Ctx n} {v : Fin (suc n)} {t : Type} → Γ ⊢ M ⦂ A → liftΓ Γ v t ⊢ lift M v ⦂ A
weakening (ty-abs body) = ty-abs (weakening body)
weakening (ty-app f x) = ty-app (weakening f) (weakening x)
weakening (ty-var v) = ty-var (weakening-var v)
weakening ty-⋆ = ty-⋆
weakening (ty-pair l r) = ty-pair (weakening l) (weakening r)
weakening (ty-projₗ p) = ty-projₗ (weakening p)
weakening (ty-projᵣ p) = ty-projᵣ (weakening p)

lemma : ∀ {Γ : Ctx n} → (v : Fin (suc n)) → liftΓ Γ v B ∋ v ⦂ A → A ≡ B
lemma fzero vzero = refl
lemma {Γ = _ ,- _} (fsuc fin) (vsuc v) = lemma fin v

subst-eq
  : (v : Fin (suc n))
  → liftΓ Γ v B ∋ v ⦂ A
  → Γ ⊢ M ⦂ B
  → Γ ⊢ var v [ v ≔ M ] ⦂ A
subst-eq fzero vzero typing = typing
subst-eq {Γ = Γ ,- C} (fsuc fin) (vsuc v) typing with fin ≟ fin
... | yes refl rewrite lemma fin v = typing
... | no neq = ⊥-elim (neq refl)

subst-neq
  : (v v' : Fin (suc n))
  → liftΓ Γ v B ∋ v' ⦂ A
  → (prf : ¬ v ≡ v')
  → Γ ∋ (Data.Fin.punchOut prf) ⦂ A
subst-neq v v' v-typing neq with v ≟ v'
... | yes refl = ⊥-elim (neq refl)
subst-neq fzero fzero _ _ | no neq = ⊥-elim (neq refl)
subst-neq {Γ = Γ ,- C} fzero (fsuc fin) (vsuc v-typing) _ | no neq = v-typing
subst-neq {Γ = Γ ,- C} (fsuc fin) fzero vzero _ | no neq = vzero
subst-neq {Γ = Γ ,- C} (fsuc fin) (fsuc fin') (vsuc v-typing) neq | no _ =
  vsuc (subst-neq fin fin' v-typing λ { assump → neq (cong fsuc assump) })

-- | The substitution lemma: Substitution preserves typing.
subst
  : ∀ {Γ : Ctx n}
  → liftΓ Γ v B ⊢ M ⦂ A → Γ ⊢ N ⦂ B
  → Γ ⊢ M [ v ≔ N ] ⦂ A
subst (ty-abs body) typing = ty-abs (subst body (weakening typing))
subst (ty-app f x) typing = ty-app (subst f typing) (subst x typing)
subst {v = v} {Γ = _} (ty-var {v = v'} v-typing) typing with v' ≟ v
... | yes refl = subst-eq v v-typing typing
subst {v = fzero} (ty-var {v = fzero} v-typing) typing | no neq = ⊥-elim (neq refl)
subst {v = fzero} (ty-var {v = fsuc v'} (vsuc v-typing)) typing | no neq = ty-var v-typing
subst {v = fsuc v} {Γ = Γ ,- C} (ty-var {v = fzero} vzero) typing | no neq = ty-var vzero
subst {v = fsuc v} {Γ = Γ ,- C} (ty-var {v = fsuc v'} (vsuc v-typing)) typing | no neq
  with v ≟ v'
... | yes eq = ⊥-elim (neq (cong fsuc (sym eq)))
... | no neq' = ty-var (vsuc (subst-neq v v' v-typing _))
subst ty-⋆ _ = ty-⋆
subst (ty-pair l r) typing = ty-pair (subst l typing) (subst r typing)
subst (ty-projₗ p) typing = ty-projₗ (subst p typing)
subst (ty-projᵣ p) typing = ty-projᵣ (subst p typing)

preservation : ● ⊢ M ⦂ A → M ↦ N → ● ⊢ N ⦂ A
preservation (ty-app M-ty N-ty) (red-head M-step) = ty-app (preservation M-ty M-step) N-ty
preservation (ty-app M-ty N-ty) (red-arg M-val N-step) =
  ty-app M-ty (preservation N-ty N-step)
preservation (ty-app (ty-abs body-ty) N-ty) (red-β N-value) = subst body-ty N-ty
preservation (ty-pair M-ty N-ty) (red-left M-step) = ty-pair (preservation M-ty M-step) N-ty
preservation (ty-pair M-ty N-ty) (red-right _ N-step) =
  ty-pair M-ty (preservation N-ty N-step)
preservation (ty-projₗ M-ty) (red-projₗ-inner M-step) = ty-projₗ (preservation M-ty M-step)
preservation (ty-projₗ (ty-pair M-ty _)) (red-projₗ _ _) = M-ty
preservation (ty-projᵣ M-ty) (red-projᵣ-inner M-step) = ty-projᵣ (preservation M-ty M-step)
preservation (ty-projᵣ (ty-pair _ N-ty)) (red-projᵣ _ _) = N-ty

max_stars_repo_name: TypesLogicsCats/STLC

max_issues_repo_name: TrulyNonstrict/STLC

max_forks_repo_name: TrulyNonstrict/STLC


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed container combinators
------------------------------------------------------------------------

module Data.Container.Indexed.Combinator where

open import Level
open import Data.Container.Indexed
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤)
open import Data.Product as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_)
open import Data.Sum renaming (_⊎_ to _⟨⊎⟩_)
open import Function as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_)
open import Function.Inverse using (_↔̇_)
open import Relation.Unary using (Pred; _⊆_; _∪_; _∩_; ⋃; ⋂)
  renaming (_⟨×⟩_ to _⟪×⟫_; _⟨⊙⟩_ to _⟪⊙⟫_; _⟨⊎⟩_ to _⟪⊎⟫_)
open import Relation.Binary.PropositionalEquality as P
  using (_≗_; refl)

------------------------------------------------------------------------
-- Combinators

-- Identity.

id : ∀ {o c r} {O : Set o} → Container O O c r
id = F.const (Lift ⊤) ◃ (λ _ → Lift ⊤) / (λ {o} _ _ → o)

-- Constant.

const : ∀ {i o c r} {I : Set i} {O : Set o} →
        Pred O c → Container I O c r
const X = X ◃ (λ _ → Lift ⊥) / λ _ → ⊥-elim ⟨∘⟩ lower

-- Duality.

_^⊥ : ∀ {i o c r} {I : Set i} {O : Set o} →
      Container I O c r → Container I O (c ⊔ r) c
(C ◃ R / n) ^⊥ = record
  { Command  = λ o → (c : C o) → R c
  ; Response = λ {o} _ → C o
  ; next     = λ f c → n c (f c)
  }

-- Strength.

infixl 3 _⋊_

_⋊_ : ∀ {i o c r z} {I : Set i} {O : Set o} (C : Container I O c r)
      (Z : Set z) → Container (I ⟨×⟩ Z) (O ⟨×⟩ Z) c r
C ◃ R / n ⋊ Z = C ⟨∘⟩ proj₁ ◃ R / λ {oz} c r → n c r , proj₂ oz

infixr 3 _⋉_

_⋉_ : ∀ {i o z c r} {I : Set i} {O : Set o} (Z : Set z)
      (C : Container I O c r) → Container (Z ⟨×⟩ I) (Z ⟨×⟩ O) c r
Z ⋉ C ◃ R / n = C ⟨∘⟩ proj₂ ◃ R / λ {zo} c r → proj₁ zo , n c r

-- Composition.

infixr 9 _∘_

_∘_ : ∀ {i j k c r} {I : Set i} {J : Set j} {K : Set k} →
      Container J K c r → Container I J c r → Container I K _ _
C₁ ∘ C₂ = C ◃ R / n
  where
  C : ∀ k → Set _
  C = ⟦ C₁ ⟧ (Command C₂)

  R : ∀ {k} → ⟦ C₁ ⟧ (Command C₂) k → Set _
  R (c , k) = ◇ C₁ {X = Command C₂} (Response C₂ ⟨∘⟩ proj₂) (_ , c , k)

  n : ∀ {k} (c : ⟦ C₁ ⟧ (Command C₂) k) → R c → _
  n (_ , f) (r₁ , r₂) = next C₂ (f r₁) r₂

-- Product. (Note that, up to isomorphism, this is a special case of
-- indexed product.)

infixr 2 _×_

_×_ : ∀ {i o c r} {I : Set i} {O : Set o} →
      Container I O c r → Container I O c r → Container I O c r
(C₁ ◃ R₁ / n₁) × (C₂ ◃ R₂ / n₂) = record
  { Command  = C₁ ∩ C₂
  ; Response = R₁ ⟪⊙⟫ R₂
  ; next     = λ { (c₁ , c₂) → [ n₁ c₁ , n₂ c₂ ] }
  }

-- Indexed product.

Π : ∀ {x i o c r} {X : Set x} {I : Set i} {O : Set o} →
    (X → Container I O c r) → Container I O _ _
Π {X = X} C = record
  { Command  = ⋂ X (Command ⟨∘⟩ C)
  ; Response = ⋃[ x ∶ X ] λ c → Response (C x) (c x)
  ; next     = λ { c (x , r) → next (C x) (c x) r }
  }

-- Sum. (Note that, up to isomorphism, this is a special case of
-- indexed sum.)

infixr 1 _⊎_

_⊎_ : ∀ {i o c r} {I : Set i} {O : Set o} →
      Container I O c r → Container I O c r → Container I O _ _
(C₁ ◃ R₁ / n₁) ⊎ (C₂ ◃ R₂ / n₂) = record
  { Command  = C₁ ∪ C₂
  ; Response = R₁ ⟪⊎⟫ R₂
  ; next     = [ n₁ , n₂ ]
  }

-- Indexed sum.

Σ : ∀ {x i o c r} {X : Set x} {I : Set i} {O : Set o} →
    (X → Container I O c r) → Container I O _ r
Σ {X = X} C = record
  { Command  = ⋃ X (Command ⟨∘⟩ C)
  ; Response = λ { (x , c) → Response (C x) c }
  ; next     = λ { (x , c) r → next (C x) c r }
  }

-- Constant exponentiation. (Note that this is a special case of
-- indexed product.)

infix 0 const[_]⟶_

const[_]⟶_ : ∀ {i o c r ℓ} {I : Set i} {O : Set o} →
             Set ℓ → Container I O c r → Container I O _ _
const[ X ]⟶ C = Π {X = X} (F.const C)

------------------------------------------------------------------------
-- Correctness proofs

module Identity where

  correct : ∀ {o ℓ c r} {O : Set o} {X : Pred O ℓ} →
            ⟦ id {c = c}{r} ⟧ X ↔̇ F.id X
  correct = record
    { to         = P.→-to-⟶ λ xs → proj₂ xs _
    ; from       = P.→-to-⟶ λ x → (_ , λ _ → x)
    ; inverse-of = record
      { left-inverse-of  = λ _ → refl
      ; right-inverse-of = λ _ → refl
      }
    }

module Constant (ext : ∀ {ℓ} → P.Extensionality ℓ ℓ) where

  correct : ∀ {i o ℓ₁ ℓ₂} {I : Set i} {O : Set o} (X : Pred O ℓ₁)
            {Y : Pred O ℓ₂} → ⟦ const X ⟧ Y ↔̇ F.const X Y
  correct X {Y} = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { right-inverse-of = λ _ → refl
      ; left-inverse-of  =
          λ xs → P.cong (_,_ (proj₁ xs)) (ext (⊥-elim ⟨∘⟩ lower))
      }
    }
    where
    to : ⟦ const X ⟧ Y ⊆ X
    to = proj₁

    from : X ⊆ ⟦ const X ⟧ Y
    from = < F.id , F.const (⊥-elim ⟨∘⟩ lower) >

module Duality where

  correct : ∀ {i o c r ℓ} {I : Set i} {O : Set o}
              (C : Container I O c r) (X : Pred I ℓ) →
            ⟦ C ^⊥ ⟧ X ↔̇ (λ o → (c : Command C o) → ∃ λ r → X (next C c r))
  correct C X = record
    { to         = P.→-to-⟶ λ { (f , g) → < f , g > }
    ; from       = P.→-to-⟶ λ f → proj₁ ⟨∘⟩ f , proj₂ ⟨∘⟩ f
    ; inverse-of = record
      { left-inverse-of  = λ { (_ , _) → refl }
      ; right-inverse-of = λ _ → refl
      }
    }

module Composition where

  correct : ∀ {i j k ℓ c r} {I : Set i} {J : Set j} {K : Set k}
              (C₁ : Container J K c r) (C₂ : Container I J c r) →
            {X : Pred I ℓ} → ⟦ C₁ ∘ C₂ ⟧ X ↔̇ (⟦ C₁ ⟧ ⟨∘⟩ ⟦ C₂ ⟧) X
  correct C₁ C₂ {X} = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { left-inverse-of  = λ _ → refl
      ; right-inverse-of = λ _ → refl
      }
    }
    where
    to : ⟦ C₁ ∘ C₂ ⟧ X ⊆ ⟦ C₁ ⟧ (⟦ C₂ ⟧ X)
    to ((c , f) , g) = (c , < f , curry g >)

    from : ⟦ C₁ ⟧ (⟦ C₂ ⟧ X) ⊆ ⟦ C₁ ∘ C₂ ⟧ X
    from (c , f) = ((c , proj₁ ⟨∘⟩ f) , uncurry (proj₂ ⟨∘⟩ f))

module Product (ext : ∀ {ℓ} → P.Extensionality ℓ ℓ) where

  correct : ∀ {i o c r} {I : Set i} {O : Set o}
              (C₁ C₂ : Container I O c r) {X} →
            ⟦ C₁ × C₂ ⟧ X ↔̇ (⟦ C₁ ⟧ X ∩ ⟦ C₂ ⟧ X)
  correct C₁ C₂ {X} = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { left-inverse-of  = from∘to
      ; right-inverse-of = λ _ → refl
      }
    }
    where
    to : ⟦ C₁ × C₂ ⟧ X ⊆ ⟦ C₁ ⟧ X ∩ ⟦ C₂ ⟧ X
    to ((c₁ , c₂) , k) = ((c₁ , k ⟨∘⟩ inj₁) , (c₂ , k ⟨∘⟩ inj₂))

    from : ⟦ C₁ ⟧ X ∩ ⟦ C₂ ⟧ X ⊆ ⟦ C₁ × C₂ ⟧ X
    from ((c₁ , k₁) , (c₂ , k₂)) = ((c₁ , c₂) , [ k₁ , k₂ ])

    from∘to : from ⟨∘⟩ to ≗ F.id
    from∘to (c , _) =
      P.cong (_,_ c) (ext [ (λ _ → refl) , (λ _ → refl) ])

module IndexedProduct where

  correct : ∀ {x i o c r ℓ} {X : Set x} {I : Set i} {O : Set o}
              (C : X → Container I O c r) {Y : Pred I ℓ} →
            ⟦ Π C ⟧ Y ↔̇ ⋂[ x ∶ X ] ⟦ C x ⟧ Y
  correct {X = X} C {Y} = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { left-inverse-of  = λ _ → refl
      ; right-inverse-of = λ _ → refl
      }
    }
    where
    to : ⟦ Π C ⟧ Y ⊆ ⋂[ x ∶ X ] ⟦ C x ⟧ Y
    to (c , k) = λ x → (c x , λ r → k (x , r))

    from : ⋂[ x ∶ X ] ⟦ C x ⟧ Y ⊆ ⟦ Π C ⟧ Y
    from f = (proj₁ ⟨∘⟩ f , uncurry (proj₂ ⟨∘⟩ f))

module Sum where

  correct : ∀ {i o c r ℓ} {I : Set i} {O : Set o}
              (C₁ C₂ : Container I O c r) {X : Pred I ℓ} →
            ⟦ C₁ ⊎ C₂ ⟧ X ↔̇ (⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X)
  correct C₁ C₂ {X} = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { left-inverse-of  = from∘to
      ; right-inverse-of = [ (λ _ → refl) , (λ _ → refl) ]
      }
    }
    where
    to : ⟦ C₁ ⊎ C₂ ⟧ X ⊆ ⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X
    to (inj₁ c₁ , k) = inj₁ (c₁ , k)
    to (inj₂ c₂ , k) = inj₂ (c₂ , k)

    from : ⟦ C₁ ⟧ X ∪ ⟦ C₂ ⟧ X ⊆ ⟦ C₁ ⊎ C₂ ⟧ X
    from = [ Prod.map inj₁ F.id , Prod.map inj₂ F.id ]

    from∘to : from ⟨∘⟩ to ≗ F.id
    from∘to (inj₁ _ , _) = refl
    from∘to (inj₂ _ , _) = refl

module IndexedSum where

  correct : ∀ {x i o c r ℓ} {X : Set x} {I : Set i} {O : Set o}
              (C : X → Container I O c r) {Y : Pred I ℓ} →
            ⟦ Σ C ⟧ Y ↔̇ ⋃[ x ∶ X ] ⟦ C x ⟧ Y
  correct {X = X} C {Y} = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { left-inverse-of  = λ _ → refl
      ; right-inverse-of = λ _ → refl
      }
    }
    where
    to : ⟦ Σ C ⟧ Y ⊆ ⋃[ x ∶ X ] ⟦ C x ⟧ Y
    to ((x , c) , k) = (x , (c , k))

    from : ⋃[ x ∶ X ] ⟦ C x ⟧ Y ⊆ ⟦ Σ C ⟧ Y
    from (x , (c , k)) = ((x , c) , k)

module ConstantExponentiation where

  correct : ∀ {x i o c r ℓ} {X : Set x} {I : Set i} {O : Set o}
              (C : Container I O c r) {Y : Pred I ℓ} →
            ⟦ const[ X ]⟶ C ⟧ Y ↔̇ (⋂ X (F.const (⟦ C ⟧ Y)))
  correct C {Y} = IndexedProduct.correct (F.const C) {Y}


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

module Data.Binary.Definition where

open import Level
open import Data.Bits public renaming (Bits to 𝔹; [] to 0ᵇ; 0∷_ to 1ᵇ_; 1∷_ to 2ᵇ_)

-- The following causes a performance hit:

-- open import Agda.Builtin.List using ([]; _∷_; List)
-- open import Agda.Builtin.Bool using (Bool; true; false)

-- 𝔹 : Type
-- 𝔹 = List Bool

-- infixr 8 1ᵇ_ 2ᵇ_
-- pattern 0ᵇ = []
-- pattern 1ᵇ_ xs = false ∷ xs
-- pattern 2ᵇ_ xs = true  ∷ xs

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground