text:
open import Type

module Structure.Container.IndexedIterable {ℓᵢ} {Index : Type{ℓᵢ}} where

import      Lvl
open import Data
open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.Option
import      Data.Option.Functions as Option
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Natural
open import Numeral.Natural.Relation.Order
open import Relator.Equals

private variable ℓ ℓₑ ℓₑ₁ ℓₑ₂ : Lvl.Level
private variable T : Type{ℓ}
private variable Elem : Type{ℓₑ}
private variable i : Index

module _ (Iter : Index → Type{ℓ}) where
  IsEmptyTypeFn = ∀{i} → Iter(i) → Bool

  IndexStepFn : IsEmptyTypeFn → Type
  IndexStepFn isEmpty = ∀{i} → (iter : Iter(i)) → (if isEmpty(iter) then Unit else Index)

  CurrentFn : Type{ℓₑ} → IsEmptyTypeFn → Type
  CurrentFn Element isEmpty = ∀{i} → (iter : Iter(i)) → (if isEmpty(iter) then Unit else Element)

  StepFn : Type{ℓₑ} → (isEmpty : IsEmptyTypeFn) → IndexStepFn isEmpty → Type
  StepFn Element isEmpty indexStep =  ∀{i} → (iter : Iter(i)) → Out iter where
    Out : Iter(i) → Type
    Out iter with isEmpty iter | indexStep iter
    ... | 𝑇 | <> = Unit
    ... | 𝐹 | is = Iter(is)

-- An iterator type `Iter` is iterable when there may be elements that the iterator can yield in sequence.
-- It should be possible to decide whether the iterator is empty, and when it is not, get the element it points to and advancing to its next state containing the next element in order.
record Iterable (Iter : Index → Type{ℓ}) {ℓₑ} : Type{ℓ Lvl.⊔ ℓᵢ Lvl.⊔ Lvl.𝐒(ℓₑ)} where
  field
    -- The type of the elements in the iterator.
    {Element} : Type{ℓₑ}

    -- Whether there are no elements left in the iterator.
    isEmpty : IsEmptyTypeFn(Iter)

    -- The current/frontmost element in the iterator if it is non-empty.
    current : CurrentFn(Iter) Element isEmpty

    -- The next iterator index. Advances the index if the iterator is non-empty.
    {indexStep} : IndexStepFn(Iter) isEmpty

    -- The next iterator state. Advancing the iterator if it is non-empty.
    step : StepFn(Iter) Element isEmpty indexStep

  -- Whether there are at most the given number of elements in the iterator.
  atMost : ℕ → Iter(i) → Bool
  atMost(𝟎)    iter = isEmpty(iter)
  atMost(𝐒(n)) iter with isEmpty(iter) | indexStep iter | step iter
  ... | 𝑇 | <>  | <> = 𝑇
  ... | 𝐹 | _   | is = atMost(n) is

  -- Skipping the given number of iterator indices. Advances as many steps as possible.
  indexWalk : (n : ℕ) → (iter : Iter(i)) → (if(atMost n iter) then Unit else Index)
  indexWalk {i} 𝟎 iter with isEmpty(iter)
  ... | 𝑇 = <>
  ... | 𝐹 = i
  indexWalk {i} (𝐒(n)) iter with isEmpty(iter) | indexStep iter | step iter
  ... | 𝑇 | <> | <>    = <>
  ... | 𝐹 | _  | iters = indexWalk n iters

  WalkFn : Type
  WalkFn = ∀{i} → (n : ℕ) → (iter : Iter(i)) → Out n iter where
    Out : ℕ → Iter(i) → Type
    Out n iter with atMost n iter | indexWalk n iter
    ... | 𝑇 | <> = Unit
    ... | 𝐹 | is = Iter(is)

    {-
    walk : WalkFn
    walk(𝟎) iter with isEmpty(iter)
    ... | 𝑇 = <>
    ... | 𝐹 = iter
    walk(𝐒(n)) iter with isEmpty(iter) | indexStep iter | step iter | walk n iter
    ... | 𝑇 | <> | <>    | _    = <>
    ... | 𝐹 | _  | iters | iters2 = ? -- walk n iters
    -}

  Foldᵣ : ∀{ℓ} → Type{ℓ} → Type
  Foldᵣ(T) = ∀{i} → (Element → T → T) → T → Iter(i) → T

  FoldᵣCriteria : Foldᵣ(T) → (∀{i} → (Element → T → T) → T → Iter(i) → Type)
  FoldᵣCriteria foldᵣ(_▫_) id iter with isEmpty iter | indexStep iter | current iter | step iter
  ... | 𝑇 | <> | <> | <>    = (foldᵣ(_▫_) id iter ≡ id)
  ... | 𝐹 | _  | x  | iters = (foldᵣ(_▫_) id iter ≡ x ▫ foldᵣ(_▫_) id iters)

  -- An iterator is finite when it is possible to fold it (when a fold function exists).
  -- This works because a fold for an infinite iterator cannot terminate, and only terminating functions exist.
  -- TODO: But it seems to be impossible to define a "foldUntil" function (though it is up to function extensionality).
  Finite = ∀{ℓ}{T : Type{ℓ}} → ∃{Obj = Foldᵣ(T)}(foldᵣ ↦ ∀{i}{_▫_}{id : T}{iter : Iter(i)} → FoldᵣCriteria (\{i}(_▫_) id → foldᵣ{i}(_▫_) id) (_▫_) id iter)
  module _ ⦃ fin : Finite ⦄ where
    foldᵣ : ∀{i} → (Element → T → T) → T → Iter(i) → T
    foldᵣ = [∃]-witness fin

    length : ∀{i} → Iter(i) → ℕ
    length = foldᵣ(const 𝐒) 𝟎

    count : ∀{i} → (Element → Bool) → Iter(i) → ℕ
    count(P) = foldᵣ(x ↦ if P(x) then 𝐒 else id) 𝟎

    foldₗ : (T → Element → T) → T → Iter(i) → T
    foldₗ(_▫_) = swap(foldᵣ(y ↦ f ↦ x ↦ f(x ▫ y)) id)

    last : ∀{i} → Iter(i) → Option(Element)
    last = foldₗ(const Some) None

    -- Note: Below are possibly inefficient implementations of functions because if they were guaranteed to exit early, the number of computations would be reduced.
    first : ∀{i} → Iter(i) → Option(Element)
    first = foldᵣ(const ∘ Some) None

  -- TODO: Complete = Surjective(step)

  record Initialed (i : Index) : Type{ℓᵢ Lvl.⊔ ℓ} where
    constructor initialed
    eta-equality
    field
      iter : Iter(i)
      left : ℕ

  Initialed-iterable : Iterable(Initialed)
  Element   Initialed-iterable = Element
  isEmpty   Initialed-iterable (initialed iter 𝟎)      = 𝑇
  current   Initialed-iterable (initialed iter 𝟎)      = <>
  indexStep Initialed-iterable (initialed iter 𝟎)      = <>
  step      Initialed-iterable (initialed iter 𝟎)      = <>
  isEmpty   Initialed-iterable (initialed iter (𝐒(_))) = isEmpty iter
  current   Initialed-iterable (initialed iter (𝐒(_))) = current iter
  indexStep Initialed-iterable (initialed iter (𝐒(_))) = indexStep iter
  step      Initialed-iterable (initialed iter (𝐒(n))) with isEmpty iter | indexStep iter | step iter
  ... | 𝑇 | _ | _     = <>
  ... | 𝐹 | _ | sIter = initialed sIter n

  {-
  record Skipped (i : Index) : Type{ℓᵢ Lvl.⊔ ℓ} where
    constructor skipped
    eta-equality
    field
      iter  : Iter(i)
      still : ℕ

  Skipped-iterable : Iterable(Skipped)
  Element   Skipped-iterable = Element
  isEmpty   Skipped-iterable (skipped iter 𝟎)      = 𝑇
  current   Skipped-iterable (skipped iter 𝟎)      = <>
  indexStep Skipped-iterable (skipped iter 𝟎)      = <>
  step      Skipped-iterable (skipped iter 𝟎)      = <>
  isEmpty   Skipped-iterable (skipped iter (𝐒(_))) = isEmpty (walk (𝐒(n)) iter)
  current   Skipped-iterable (skipped iter (𝐒(_))) = current (walk (𝐒(n)) iter)
  indexStep Skipped-iterable (skipped iter (𝐒(_))) = indexStep (walk (𝐒(n)) iter)
  step      Skipped-iterable (skipped iter (𝐒(n))) with isEmpty iter | indexStep iter | step iter
  -}

  mapped : (Element → Elem) → Iterable(Iter)
  Element (mapped {Elem = Elem} f) = Elem
  isEmpty (mapped f) = isEmpty
  current (mapped f) iter with isEmpty iter | current iter
  ... | 𝑇 | <> = <>
  ... | 𝐹 | x  = f(x)
  indexStep (mapped f) iter = indexStep iter
  step      (mapped f) iter = step iter

{-record Stored (n : ℕ) {Iter : Index → Type{ℓ₁}} (iterable : Iterable(Iter)) : Type where
  field
    Queue(Iterator.Element(iterable))
-}

  {- TODO: Also needs to store data, so it cannot be the same Iter
  skipped : ℕ → Iterator{ℓₑ} → Iterator
  Iterator.Element (skipped _ iterator) = Iterator.Element iterator
  Iterator.isEmpty (skipped n iterator) = Iterator.atMost n iterator
  Iterator.current (skipped _ iterator) =
  Iterator.indexStep (skipped iterator) =
  Iterator.step      (skipped iterator) =
-}

{-
skipped : ℕ → ∀{iter} → Iterable{ℓₑ}(iter) → Iterable(iter)
skipped 𝟎 iterable = iterable
skipped (𝐒 n) iterable = {!!}
-}

  -- An empty iterator of the iterable.
  EmptyConstruction : ∀{i} → Iter(i) → Type
  EmptyConstruction(empty) = IsTrue(isEmpty empty)

  -- A function prepending an element to an iterator of the iterable.
  PrependConstruction : ∀{indexPrepend : ∀{i} → Element → Iter(i) → Index} → (∀{i} → (x : Element) → (iter : Iter(i)) → Iter(indexPrepend x iter)) → Type
  PrependConstruction{indexPrepend} (prepend) = ∀{i}{x}{iter : Iter(i)} → ∃{Obj = IndexStep x iter}(Out x iter) where
    IndexStep : Element → Iter(i) → Type
    IndexStep{i} x iter with isEmpty(prepend x iter) | indexStep(prepend x iter)
    ... | 𝑇 | _ = Empty
    ... | 𝐹 | p = (p ≡ i)

    Out : (x : Element) → (iter : Iter(i)) → IndexStep x iter → Type
    Out x iter stepProof with isEmpty(prepend x iter) | indexStep(prepend x iter) | current(prepend x iter) | step(prepend x iter)
    ... | 𝐹 | _ | cur | st with [≡]-intro ← stepProof = (x ≡ cur) ∧ (st ≡ iter)

  module _
    {indexEmpty}{empty}
    ⦃ empty-construciton : EmptyConstruction{indexEmpty}(empty) ⦄
    {indexPrepend : ∀{i} → Element → Iter(i) → Index}
    {prepend : ∀{i} → (x : Element) → (iter : Iter(i)) → Iter(indexPrepend x iter)}
    ⦃ prepend-construction : PrependConstruction{indexPrepend}(prepend) ⦄
    where

    singleton : (x : Element) → Iter(indexPrepend x empty)
    singleton x = prepend x empty

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:
------------------------------------------------------------------------------
-- The division result is correct
------------------------------------------------------------------------------

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

module FOTC.Program.Division.ResultATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.PropertiesATP
open import FOTC.Program.Division.Division
open import FOTC.Program.Division.Specification

------------------------------------------------------------------------------
-- The division result is correct when the dividend is less than
-- the divisor.

postulate div-x<y-helper : ∀ {i j} → N i → N j → i < j → i ≡ j * div i j + i
{-# ATP prove div-x<y-helper *-rightZero #-}

div-x<y-resultCorrect : ∀ {i j} → N i → N j → i < j →
                        ∃[ r ] N r ∧ r < j ∧ i ≡ j * div i j + r
div-x<y-resultCorrect Ni Nj i<j = _ , Ni , i<j , div-x<y-helper Ni Nj i<j

-- The division result is correct when the dividend is greater or equal
-- than the divisor.
-- Using the inductive hypothesis ih we know that
--
-- i ∸ j = j * (div (i ∸ j) j) + r.

-- From that we get
--
-- i = j * (succ (div (i ∸ j) j)) + r and we know
--
-- div i j = succ (div (i ∸ j) j) therefore we get
--
-- i = j * div i j + r.
postulate helper : ∀ {i j r} → N i → N j → N r →
                   i ∸ j ≡ j * div (i ∸ j) j + r →
                   i ≡ j * succ₁ (div (i ∸ j) j) + r

postulate div-x≮y-helper : ∀ {i j r} → N i → N j → N r →
                           i ≮ j →
                           i ∸ j ≡ j * div (i ∸ j) j + r →
                           i ≡ j * div i j + r
{-# ATP prove div-x≮y-helper helper #-}

postulate div-x≮y-resultCorrect : ∀ {i j} → N i → N j →
                                  (ih : divSpec (i ∸ j) j (div (i ∸ j) j)) →
                                  i ≮ j →
                                  ∃[ r ] N r ∧ r < j ∧ i ≡ j * div i j + r
{-# ATP prove div-x≮y-resultCorrect div-x≮y-helper #-}

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Cham.Agent where

open import Cham.Context
open import Cham.Label
open import Cham.Name
open import Data.Nat
open import Data.Product

data Agent : Context → Set where
  Nil  : Agent ∅

  _∙_  : ∀ {Γ}
       → (Valence : Label)
       → Agent Γ
       → Agent (Γ ⊢ Valence)

  _∣_  : ∀ {Γ₁ Γ₂}
       → Agent Γ₁
       → Agent Γ₂
       → Agent (Γ₁ , Γ₂)

  _/_  : ∀ {Γ}
       → (Ion : Name)
       → Agent Γ
       → Agent (Γ ⊢ Ion ⁻)

  _[]_ : ∀ {Γ₁ Γ₂}
       → Agent Γ₁
       → Agent Γ₂
       → Agent (Γ₁ , Γ₂)

Reaction : ∀ {Γ₁ Γ₂ Ion}
         → Agent (Γ₁ ⊢ Ion ⁺)
         → Agent (Γ₂ ⊢ Ion ⁻)
         → Agent Γ₁ × Agent Γ₂
Reaction (.(_   ⁺) ∙ a₁) (.(_ ⁻) ∙ a₂) = a₁ , a₂
Reaction (.(Ion ⁺) ∙ a₁) (Ion    / a₂) = a₁ , a₂


text:
module GUIgeneric.GUIExampleBankAccount   where

open import GUIgeneric.Prelude renaming (inj₁ to firstBtn; inj₂ to secondBtn; WxColor to Color;_∸_ to _-_) hiding (addButton; _>>_ ; show)

open import GUIgeneric.GUIDefinitions renaming (add to add'; add' to add)
open import GUIgeneric.GUI
open import GUIgeneric.GUIExampleLib renaming (addButton to addButton')
open import GUIgeneric.GUIExample  hiding (main; changeGUI)

open import Data.Nat.Show
open import heap.libraryNat renaming (_≧ℕb_ to _≧_)

guifullToReturnType : ∀ {i} {g} → GUI {i} → returnType g
guifullToReturnType f = changedGUI (f .defFrame) (f .property)

guifullToReturnType' : ∀ {i} {g} → GUI {i} →
                       Σ[ r ∈ returnType g ]
                       (IOObjectˢ GuiLev1Interface handlerInterface i
                           (nextStateFrame g r))
guifullToReturnType' {i} {g} f = guifullToReturnType f , f .obj

changeGUI : ∀ {i} {g} → GUI {i} →
                       IO GuiLev1Interface ∞ (Σ[ r ∈ returnType g ]
                       (IOObjectˢ GuiLev1Interface handlerInterface i
                           (nextStateFrame g r)))
changeGUI  f = return (guifullToReturnType' f)

threeBtnFrame : (s s' s'' : String) → Frame
threeBtnFrame s s'  s'' = addButton s  (addButton s'
                             (addButton s'' create-frame))

propThreeBtn : ∀{s s' s''} → properties (threeBtnFrame s s' s'')
propThreeBtn = black , black , black , oneColumnLayout

mutual
 atm :  ∀{i} → ℕ → GUI {i}
 atm n   .defFrame  =
      addButton  "Withdraw 10"
     (addButton  "Withdraw 1"
     (addTxtBox  (show n) create-frame))
 atm n   .property =
   black , black , black , oneColumnLayout
 atm n   .obj .method (firstBtn x) =
    if n ≧ 10  then  changeGUI  (atm (n - 10))
               else  changeGUI  (invalid n)

 atm n  .obj .method (secondBtn b) =
     if n ≧ 1  then  changeGUI  (atm (n - 1))
               else  changeGUI  (invalid n)

 invalid : ∀{i} → ℕ → GUI {i}
 invalid n .defFrame =
     addButton "Not enough money" create-frame
 invalid n .property       =  black , oneColumnLayout
 invalid n .obj .method m  =  changeGUI (atm n)

main : NativeIO Unit
main = compileGUI (atm 55)

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
-- {-# OPTIONS -v 100 -v tc.meta.name:100 -v interactive.meta:10 #-}
module Issue526 where

-- Don't just write _49,
-- include the corresponding implicit variable name as well (if any)

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

test : Set
test = f Set

test₁ : Set
test₁ = f {A = _} Set

postulate
  g : (B : Set) → Set

test₂ : Set
test₂ = g _

test₃ : _ → Set
test₃ ()

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module MLib.Prelude.RelProps where

open import MLib.Prelude.FromStdlib

import Relation.Binary.Indexed as I
open FE using (cong)
import Data.Product.Relation.SigmaPropositional as OverΣ

Σ-bij : ∀ {a b c} {A : Set a} {B : A → Set b} {C : A → Set c} → (∀ x → B x ↔ C x) → Σ A B ↔ Σ A C
Σ-bij pw = record
  { to = ≡.→-to-⟶ (uncurry λ x y → x , Inverse.to (pw x) ⟨$⟩ y)
  ; from = ≡.→-to-⟶ (uncurry λ x y → x , Inverse.from (pw x) ⟨$⟩ y)
  ; inverse-of = record
    { left-inverse-of = uncurry λ x y → OverΣ.to-≡ (≡.refl , Inverse.left-inverse-of (pw x) y)
    ; right-inverse-of = uncurry λ x y → OverΣ.to-≡ (≡.refl , Inverse.right-inverse-of (pw x) y)
    }
  }

Σ-↞ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : A → Set c} → (∀ x → B x ↞ C x) → Σ A B ↞ Σ A C
Σ-↞ f = record
  { to = ≡.→-to-⟶ (uncurry λ x y → x , LeftInverse.to (f x) ⟨$⟩ y)
  ; from = ≡.→-to-⟶ (uncurry λ x y → x , LeftInverse.from (f x) ⟨$⟩ y)
  ; left-inverse-of = uncurry λ x y → OverΣ.to-≡ (≡.refl , LeftInverse.left-inverse-of (f x) y)
  }

Σ-↞′ :
  ∀ {a a′ b β} {A : Set a} {A′ : Set a′} {B-setoid : A → Setoid b β} (f : A ↞ A′)
  → LeftInverse (OverΣ.setoid B-setoid) (OverΣ.setoid (B-setoid ∘ (LeftInverse.from f ⟨$⟩_)))
Σ-↞′ {A = A} {A′} {B-setoid} f = record
  { to = record
    { _⟨$⟩_ = uncurry λ x y → LeftInverse.to f ⟨$⟩ x , ≡.subst B (≡.sym (LeftInverse.left-inverse-of f _)) y
    ; cong = uncurry λ {≡.refl y → ≡.refl , subst≈ _ _ (≡.sym (LeftInverse.left-inverse-of f _)) y}
    }
  ; from = record
    { _⟨$⟩_ = uncurry λ x y → LeftInverse.from f ⟨$⟩ x , y
    ; cong = λ { (≡.refl , q) → ≡.refl , q }
    }
  ; left-inverse-of = uncurry λ x y → OverΣ.symmetric sym (OverΣ.subst (≡.sym (LeftInverse.left-inverse-of f _)) refl)
  }
  where
    module B x = Setoid (B-setoid x)
    module B′ {x} = Setoid (B-setoid x)
    open B using () renaming (Carrier to B)
    open B′

    subst≈ : ∀ {i j} (x y : B i) (p : i ≡ j) → x ≈ y → ≡.subst B p x ≈ ≡.subst B p y
    subst≈ x y ≡.refl q = q


text:
module Imports.A where

postulate A : Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module _ where

import Issue1168       ;  module I = Issue1168
import PrettyInterface ;  module P = PrettyInterface

id : {A : Set} → A → A
id {A = A} a = a


text:
module Dot where

postulate h : Set

f : Set -> Set -> Set
f .n n = h

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Cubical.Data.Nat.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat.Base
open import Cubical.Data.Empty
open import Cubical.Data.Prod.Base

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq

open import Cubical.Data.Nat.Algebra public

+-zero : ∀ m → m + 0 ≡ m
+-zero zero = refl
+-zero (suc m) = cong suc (+-zero m)

+-suc : ∀ m n → m + suc n ≡ suc (m + n)
+-suc zero    n = refl
+-suc (suc m) n = cong suc (+-suc m n)

+-comm : ∀ m n → m + n ≡ n + m
+-comm m zero = +-zero m
+-comm m (suc n) = (+-suc m n) ∙ (cong suc (+-comm m n))

-- Addition is associative
+-assoc : ∀ m n o → m + (n + o) ≡ (m + n) + o
+-assoc zero _ _    = refl
+-assoc (suc m) n o = cong suc (+-assoc m n o)

private
  variable
    l m n : ℕ

znots : ¬ (0 ≡ suc n)
znots eq = subst (caseNat ℕ ⊥) eq 0

snotz : ¬ (suc n ≡ 0)
snotz eq = subst (caseNat ⊥ ℕ) eq 0

injSuc : suc m ≡ suc n → m ≡ n
injSuc p = cong predℕ p

inj-m+ : m + l ≡ m + n → l ≡ n
inj-m+ {zero} p = p
inj-m+ {suc m} p = inj-m+ (injSuc p)

inj-+m : l + m ≡ n + m → l ≡ n
inj-+m {l} {m} {n} p = inj-m+ ((+-comm m l) ∙ (p ∙ (+-comm n m)))

m+n≡n→m≡0 : m + n ≡ n → m ≡ 0
m+n≡n→m≡0 {n = zero} = λ p → (sym (+-zero _)) ∙ p
m+n≡n→m≡0 {n = suc n} p = m+n≡n→m≡0 (injSuc ((sym (+-suc _ n)) ∙ p))

m+n≡0→m≡0×n≡0 : m + n ≡ 0 → (m ≡ 0) × (n ≡ 0)
m+n≡0→m≡0×n≡0 {zero} = refl ,_
m+n≡0→m≡0×n≡0 {suc m} p = ⊥-elim (snotz p)

discreteℕ : Discrete ℕ
discreteℕ zero zero = yes refl
discreteℕ zero (suc n) = no znots
discreteℕ (suc m) zero = no snotz
discreteℕ (suc m) (suc n) with discreteℕ m n
... | yes p = yes (cong suc p)
... | no p = no (λ x → p (injSuc x))

isSetℕ : isSet ℕ
isSetℕ = Discrete→isSet discreteℕ

0≡m*0 : ∀ m → 0 ≡ m * 0
0≡m*0 zero = refl
0≡m*0 (suc m) = 0≡m*0 m

*-suc : ∀ m n → m * suc n ≡ m + m * n
*-suc zero n = refl
*-suc (suc m) n
  = cong suc
  ( n + m * suc n ≡⟨ cong (n +_) (*-suc m n) ⟩
    n + (m + m * n) ≡⟨ +-assoc n m (m * n) ⟩
    (n + m) + m * n ≡⟨ cong (_+ m * n) (+-comm n m) ⟩
    (m + n) + m * n ≡⟨ sym (+-assoc m n (m * n)) ⟩
    m + (n + m * n) ∎
  )

*-comm : ∀ m n → m * n ≡ n * m
*-comm zero n = 0≡m*0 n
*-comm (suc m) n = cong (n +_) (*-comm m n) ∙ sym (*-suc n m)

0≡n*sm→0≡n : 0 ≡ n * suc m → 0 ≡ n
0≡n*sm→0≡n {n = zero} p = refl
0≡n*sm→0≡n {n = suc n} p = ⊥-elim (znots p)

inj-*sm : l * suc m ≡ n * suc m → l ≡ n
inj-*sm {zero} {m} {n} p = 0≡n*sm→0≡n p
inj-*sm {l} {m} {zero} p = sym (0≡n*sm→0≡n (sym p))
inj-*sm {suc l} {m} {suc n} p = cong suc (inj-*sm (inj-m+ {m = suc m} p))

inj-sm* : suc m * l ≡ suc m * n → l ≡ n
inj-sm* {m} {l} {n} p = inj-*sm (*-comm l (suc m) ∙ p ∙ *-comm (suc m) n)

max_stars_repo_name: oisdk/cubical

max_issues_repo_name: oisdk/cubical

max_forks_repo_name: oisdk/cubical


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

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

open import Haskell.Modules.RWS.RustAnyHow
import      LibraBFT.Impl.Consensus.ConsensusTypes.BlockRetrieval as BlockRetrieval
import      LibraBFT.Impl.IO.OBM.ObmNeedFetch                     as ObmNeedFetch
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochIndep
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
import      Util.KVMap                                            as Map
open import Util.Prelude
------------------------------------------------------------------------------
import      Data.String                                           as String

module LibraBFT.Impl.Consensus.BlockStorage.BlockRetriever where

pickPeer : ℕ → List Author → Either ErrLog (Author × List Author)

-- LBFT-OBM-DIFF : this lives in sync_manager.rs (in this file to isolate IO)
-- TODO-1 PROVE IT TERMINATES
{-# TERMINATING #-}
retrieveBlockForQCM : BlockRetriever → QuorumCert → U64 → LBFT (Either ErrLog (List Block))
retrieveBlockForQCM _retriever qc numBlocks =
  loop (qc ^∙ qcCertifiedBlock ∙ biId) 0 (Map.kvm-keys (qc ^∙ qcLedgerInfo ∙ liwsSignatures))
 where
  doLoop : HashValue → ℕ → List Author → LBFT (Either ErrLog (List Block))
  logIt  : InfoLog → LBFT Unit
  here'  : List String.String → List String.String

  loop : HashValue → ℕ → List Author → LBFT (Either ErrLog (List Block))
  loop blockId attempt = λ where
    [] → bail fakeErr -- [ "failed to fetch block, no more peers available"
                      -- , lsHV blockId, show attempt ]
    peers0@(_ ∷ _) → do
      mme               ← use (lRoundManager ∙ rmObmMe)
      maybeSD mme (bail fakeErr) $ λ me → do
        nf                ← use lObmNeedFetch
        eitherS (pickPeer attempt peers0) bail $ λ (peer , peers) → do
          let request     = BlockRetrievalRequest∙new me blockId numBlocks
          logIt fakeInfo -- ["to", lsA peer, lsBRQ request]
          let response    = ObmNeedFetch.writeRequestReadResponseUNSAFE nf me peer request
          -- TODO : sign response and check sig on response
          case response ^∙ brpStatus of λ where
            BRSSucceeded → do
              logIt fakeInfo -- (here [lsBRP response])
              vv ← use (lRoundManager ∙ rmEpochState ∙ esVerifier)
              -- LBFT-OBM-DIFF/TODO : this should live in a "network" module
              case BlockRetrieval.verify response (request ^∙ brqBlockId) (request ^∙ brqNumBlocks) vv of λ where
                (Left  e) → bail (withErrCtx (here' []) e)
                (Right _) → ok   (response ^∙ brpBlocks)
            BRSIdNotFound      → doLoop blockId attempt peers
            BRSNotEnoughBlocks → doLoop blockId attempt peers

  doLoop blockId attempt peers = do
    logIt fakeInfo -- (here' ["trying another peer", lsBRP response])
    loop blockId (attempt + 1) peers

  here' t = "BlockRetriever" ∷ "retrieveBlockForQCM" ∷ "NeedFetch" ∷ t
  logIt l = -- do
    logInfo l
    -- let x = Unsafe.unsafePerformIO (putStrLn @Text (show l))
    -- x `seq` pure x

pickPeer _ = λ where
  []       → Left fakeErr -- ["no more peers"]
  (p ∷ ps) → pure (p , ps)


text:
module Data.BitVector.ContainmentOrder where

open import Data.Empty
open import Data.Sum
open import Data.Vec

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Data.Nat hiding (_≟_; _≤_; _≤?_) renaming (zero to Nzero; suc to Nsuc)

open import Data.BitVector

infix 4 _⊂_

data _⊂_ : ∀ {n} → BitVector n → BitVector n → Set where
  []⊂[] : [] ⊂ []
  0#⊂0# : ∀ {n} {x y : BitVector n}     → (x⊂y : x ⊂ y) → (0# ∷ x) ⊂ (0# ∷ y)
  b⊂1#  : ∀ {n} {x y : BitVector n} {b} → (x⊂y : x ⊂ y) → (b  ∷ x) ⊂ (1# ∷ y)

⊂-refl : ∀ {n} → _≡_ ⇒ (_⊂_ {n})
⊂-refl {0} {[]} refl = []⊂[]
⊂-refl {Nsuc n} {0# ∷ xs} refl = 0#⊂0# (⊂-refl refl)
⊂-refl {Nsuc n} {1# ∷ xs} refl = b⊂1# (⊂-refl refl)

⊂-antisym : ∀ {n} → Antisymmetric _≡_ (_⊂_ {n})
⊂-antisym []⊂[] []⊂[] = refl
⊂-antisym (0#⊂0# x⊂y) (0#⊂0# y⊂x) rewrite ⊂-antisym x⊂y y⊂x = refl
⊂-antisym (b⊂1#  x⊂y) (b⊂1#  y⊂x) rewrite ⊂-antisym x⊂y y⊂x = refl

⊂-trans : ∀ {n} → Transitive (_⊂_ {n})
⊂-trans []⊂[] []⊂[] = []⊂[]
⊂-trans (0#⊂0# x⊂y) (0#⊂0# y⊂z) = 0#⊂0# (⊂-trans x⊂y y⊂z)
⊂-trans (0#⊂0# x⊂y) (b⊂1#  y⊂z) = b⊂1#  (⊂-trans x⊂y y⊂z)
⊂-trans (b⊂1#  x⊂y) (b⊂1#  y⊂z) = b⊂1#  (⊂-trans x⊂y y⊂z)

_⊂?_ : ∀ {n} → Decidable (_⊂_ {n})
[] ⊂? [] = yes []⊂[]
(x ∷ xs) ⊂? (y ∷ ys) with xs ⊂? ys
(0# ∷ xs) ⊂? (0# ∷ ys)  | no  xs≢ys = no helper
  where helper : ¬ 0# ∷ xs ⊂ 0# ∷ ys
        helper (0#⊂0# pf) = xs≢ys pf
(x  ∷ xs) ⊂? (1# ∷ ys)  | no  xs≢ys = no helper
  where helper : ¬ x ∷ xs ⊂ 1# ∷ ys
        helper (b⊂1# pf) = xs≢ys pf
(1# ∷ xs) ⊂? (0# ∷ ys)  | no  xs≢ys = no (λ ())
(0# ∷ xs) ⊂? (0# ∷ ys)  | yes xs≡ys = yes (0#⊂0# xs≡ys)
(0# ∷ xs) ⊂? (1# ∷ ys)  | yes xs≡ys = yes (b⊂1#  xs≡ys)
(1# ∷ xs) ⊂? (0# ∷ ys)  | yes xs≡ys = no  (λ ())
(1# ∷ xs) ⊂? (1# ∷ ys)  | yes xs≡ys = yes (b⊂1#  xs≡ys)

decPoset : ∀ {n} → DecPoset _ _ _
decPoset {n} = record
  { Carrier = BitVector n
  ; _≈_ = _≡_
  ; _≤_ = _⊂_
  ; isDecPartialOrder = record
      { isPartialOrder = record
          { isPreorder = record
              { isEquivalence = isEquivalence
              ; reflexive = ⊂-refl
              ; trans = ⊂-trans
              }
          ; antisym = ⊂-antisym
          }
      ; _≟_ = _≟_
      ; _≤?_ = _⊂?_
      }
  }

max_stars_repo_name: copumpkin/bitvector

max_issues_repo_name: copumpkin/bitvector

max_forks_repo_name: copumpkin/bitvector


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of sums (disjoint unions)
------------------------------------------------------------------------

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

module Data.Sum.Properties where

open import Level
open import Data.Sum.Base
open import Function
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (map′)

private
  variable
    a b c d e f : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d
    E : Set e
    F : Set f

inj₁-injective : ∀ {x y} → (A ⊎ B ∋ inj₁ x) ≡ inj₁ y → x ≡ y
inj₁-injective refl = refl

inj₂-injective : ∀ {x y} → (A ⊎ B ∋ inj₂ x) ≡ inj₂ y → x ≡ y
inj₂-injective refl = refl

module _ (dec₁ : Decidable {A = A} {B = A} _≡_)
         (dec₂ : Decidable {A = B} {B = B} _≡_) where

  ≡-dec : Decidable {A = A ⊎ B} _≡_
  ≡-dec (inj₁ x) (inj₁ y) = map′ (cong inj₁) inj₁-injective (dec₁ x y)
  ≡-dec (inj₁ x) (inj₂ y) = no λ()
  ≡-dec (inj₂ x) (inj₁ y) = no λ()
  ≡-dec (inj₂ x) (inj₂ y) = map′ (cong inj₂) inj₂-injective (dec₂ x y)

swap-involutive : swap {A = A} {B = B} ∘ swap ≗ id
swap-involutive = [ (λ _ → refl) , (λ _ → refl) ]

[,]-∘-distr : {f : A → B}
              {g : C → A} {h : D → A} →
              f ∘ [ g , h ] ≗ [ f ∘ g , f ∘ h ]
[,]-∘-distr (inj₁ _) = refl
[,]-∘-distr (inj₂ _) = refl

[,]-map-commute : {f : A → B}  {g : C → D}
                  {f′ : B → E} {g′ : D → E} →
                  [ f′ , g′ ] ∘ (map f g) ≗ [ f′ ∘ f , g′ ∘ g ]
[,]-map-commute (inj₁ _) = refl
[,]-map-commute (inj₂ _) = refl

map-commute : {f : A → B}  {g : C → D}
              {f′ : B → E} {g′ : D → F} →
              ((map f′ g′) ∘ (map f g)) ≗ map (f′ ∘ f) (g′ ∘ g)
map-commute (inj₁ _) = refl
map-commute (inj₂ _) = refl


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence using (pathToEquiv)

open import Cubical.Functions.FunExtEquiv

open import Cubical.Data.Unit
open import Cubical.Data.Nat
open import Cubical.Data.Sigma

open import Cubical.Relation.Binary
open BinaryRelation

open import Cubical.Displayed.Base

private
  variable
    ℓ ℓA ℓA' ℓP ℓ≅A ℓ≅A' ℓB ℓB' ℓ≅B ℓ≅B' ℓC ℓ≅C : Level

-- UARel on Σ-type

module _ {A : Type ℓA} {ℓ≅A : Level} {𝒮-A : UARel A ℓ≅A}
  {B : A → Type ℓB} {ℓ≅B : Level}
  (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B)
  where

  open UARel 𝒮-A
  open DUARel 𝒮ᴰ-B

  ∫ : UARel (Σ A B) (ℓ-max ℓ≅A ℓ≅B)
  UARel._≅_ ∫ (a , b) (a' , b') = Σ[ p ∈ a ≅ a' ] (b ≅ᴰ⟨ p ⟩ b')
  UARel.ua ∫ (a , b) (a' , b') =
    compEquiv
      (Σ-cong-equiv (ua a a') (λ p → uaᴰ b p b'))
      ΣPath≃PathΣ

-- UARel on Π-type

module _ {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) {B : A → Type ℓB} (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B) where

  open UARel 𝒮-A
  open DUARel 𝒮ᴰ-B

  𝒮ᴰ→𝒮-Π : UARel ((a : A) → B a) (ℓ-max ℓA ℓ≅B)
  UARel._≅_ 𝒮ᴰ→𝒮-Π f f' = ∀ a → f a ≅ᴰ⟨ ρ a ⟩ f' a
  UARel.ua 𝒮ᴰ→𝒮-Π f f' =
    compEquiv
      (equivΠCod λ a → uaᴰρ (f a) (f' a))
      funExtEquiv

-- induction principles

module _ {A : Type ℓA} {ℓ≅A : Level} (𝒮-A : UARel A ℓ≅A) where
  open UARel 𝒮-A
  𝒮-J : {a : A}
        (P : (a' : A) → (p : a ≡ a') → Type ℓ)
        (d : P a refl)
        {a' : A}
        (p : a ≅ a')
        → P a' (≅→≡ p)
  𝒮-J {a} P d {a'} p
    = J (λ y q → P y q)
        d
        (≅→≡ p)

  𝒮-J-2 : {a : A}
            (P : (a' : A) → (p : a ≅ a') → Type ℓ)
            (d : P a (ρ a))
            {a' : A}
            (p : a ≅ a')
            → P a' p
  𝒮-J-2 {a = a} P d {a'} p
    = subst (λ r → P a' r) (Iso.leftInv (uaIso a a') p) g
    where
      g : P a' (≡→≅ (≅→≡ p))
      g = J (λ y q → P y (≡→≅ q)) d (≅→≡ p)

-- constructors

module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {B : A → Type ℓB}
  (_≅ᴰ⟨_⟩_ : {a a' : A} → B a → UARel._≅_ 𝒮-A a a' → B a' → Type ℓ≅B)
  where

    open UARel 𝒮-A

    -- constructor that reduces ua to the case where p = ρ a by induction on p
    private
      𝒮ᴰ-make-aux : (uni : {a : A} (b b' : B a) → b ≅ᴰ⟨ ρ a ⟩ b' ≃ (b ≡ b'))
                    → ({a a' : A} (b : B a) (p : a ≅ a') (b' : B a') → (b ≅ᴰ⟨ p ⟩ b') ≃ PathP (λ i → B (≅→≡ p i)) b b')
      𝒮ᴰ-make-aux uni {a} {a'} b p
        = 𝒮-J-2 𝒮-A
                    (λ y q → (b' : B y) → (b ≅ᴰ⟨ q ⟩ b') ≃ PathP (λ i → B (≅→≡ q i)) b b')
                    (λ b' → uni' b')
                    p
        where
          g : (b' : B a) → (b ≡ b') ≡ PathP (λ i → B (≅→≡ (ρ a) i)) b b'
          g b' = subst (λ r → (b ≡ b') ≡ PathP (λ i → B (r i)) b b')
                       (sym (Iso.rightInv (uaIso a a) refl))
                       refl
          uni' : (b' : B a) → b ≅ᴰ⟨ ρ a ⟩ b' ≃ PathP (λ i → B (≅→≡ (ρ a) i)) b b'
          uni' b' = compEquiv (uni b b') (pathToEquiv (g b'))

    𝒮ᴰ-make-1 : (uni : {a : A} (b b' : B a) → b ≅ᴰ⟨ ρ a ⟩ b' ≃ (b ≡ b'))
                → DUARel 𝒮-A B ℓ≅B
    DUARel._≅ᴰ⟨_⟩_ (𝒮ᴰ-make-1 uni) = _≅ᴰ⟨_⟩_
    DUARel.uaᴰ (𝒮ᴰ-make-1 uni) = 𝒮ᴰ-make-aux uni

    -- constructor that reduces univalence further to contractibility of relational singletons

    𝒮ᴰ-make-2 : (ρᴰ : {a : A} → isRefl _≅ᴰ⟨ ρ a ⟩_)
                (contrTotal : (a : A) → contrRelSingl _≅ᴰ⟨ UARel.ρ 𝒮-A a ⟩_)
                → DUARel 𝒮-A B ℓ≅B
    DUARel._≅ᴰ⟨_⟩_ (𝒮ᴰ-make-2 ρᴰ contrTotal) = _≅ᴰ⟨_⟩_
    DUARel.uaᴰ (𝒮ᴰ-make-2 ρᴰ contrTotal)
      = 𝒮ᴰ-make-aux (contrRelSingl→isUnivalent _ ρᴰ (contrTotal _))

-- lifts

module _ {A : Type ℓA} (𝒮-A : UARel A ℓ≅A)
  {B : A → Type ℓB}
  {ℓ≅B : Level}
  (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B)
  {C : A → Type ℓC}
  (𝒮ᴰ-C : DUARel 𝒮-A C ℓ≅C)
  where

  open DUARel 𝒮ᴰ-B

  Lift-𝒮ᴰ : DUARel (∫ 𝒮ᴰ-C) (λ (a , _) → B a) ℓ≅B
  DUARel._≅ᴰ⟨_⟩_ Lift-𝒮ᴰ b p b' = b ≅ᴰ⟨ p .fst ⟩ b'
  DUARel.uaᴰ Lift-𝒮ᴰ b p b' = uaᴰ b (p .fst) b'

-- associativity

module _ {A : Type ℓA} (𝒮-A : UARel A ℓ≅A)
  {B : A → Type ℓB} {ℓ≅B : Level} (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B)
  {C : Σ A B → Type ℓC} {ℓ≅C : Level} (𝒮ᴰ-C : DUARel (∫ 𝒮ᴰ-B) C ℓ≅C)
  where

  open UARel 𝒮-A
  open DUARel 𝒮ᴰ-B renaming (_≅ᴰ⟨_⟩_ to _≅B⟨_⟩_ ; uaᴰ to uaB)
  open DUARel 𝒮ᴰ-C renaming (_≅ᴰ⟨_⟩_ to _≅C⟨_⟩_ ; uaᴰ to uaC)

  splitTotal-𝒮ᴰ : DUARel 𝒮-A (λ a → Σ[ b ∈ B a ] C (a , b)) (ℓ-max ℓ≅B ℓ≅C)
  DUARel._≅ᴰ⟨_⟩_ splitTotal-𝒮ᴰ (b , c) p (b' , c') =
    Σ[ q ∈ b ≅B⟨ p ⟩ b' ]  (c ≅C⟨ p , q ⟩ c')
  DUARel.uaᴰ splitTotal-𝒮ᴰ (b ,  c) p (b' , c') =
    compEquiv
      (Σ-cong-equiv (uaB b p b') (λ q → uaC c (p , q) c'))
      ΣPath≃PathΣ

-- combination

module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {B : A → Type ℓB} {ℓ≅B : Level} (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B)
  {C : A → Type ℓC} {ℓ≅C : Level} (𝒮ᴰ-C : DUARel 𝒮-A C ℓ≅C)
  where

  _×𝒮ᴰ_ : DUARel 𝒮-A (λ a → B a × C a) (ℓ-max ℓ≅B ℓ≅C)
  _×𝒮ᴰ_ = splitTotal-𝒮ᴰ 𝒮-A 𝒮ᴰ-B (Lift-𝒮ᴰ 𝒮-A 𝒮ᴰ-C 𝒮ᴰ-B)

-- constant displayed structure

module _ {A : Type ℓA} (𝒮-A : UARel A ℓ≅A)
  {B : Type ℓB} (𝒮-B : UARel B ℓ≅B)  where

  open UARel 𝒮-B
  open DUARel

  𝒮ᴰ-const : DUARel 𝒮-A (λ _ → B) ℓ≅B
  𝒮ᴰ-const ._≅ᴰ⟨_⟩_ b _ b' = b ≅ b'
  𝒮ᴰ-const .uaᴰ b p b' = ua b b'

  -- UARel product

  _×𝒮_ : UARel (A × B) (ℓ-max ℓ≅A ℓ≅B)
  _×𝒮_ = ∫ 𝒮ᴰ-const

-- relational isomorphisms

𝒮-iso→iso : {A : Type ℓA} (𝒮-A : UARel A ℓ≅A)
               {B : Type ℓB} (𝒮-B : UARel B ℓ≅B)
               (F : RelIso (UARel._≅_ 𝒮-A) (UARel._≅_ 𝒮-B))
               → Iso A B
𝒮-iso→iso 𝒮-A 𝒮-B F
  = RelIso→Iso (UARel._≅_ 𝒮-A)
               (UARel._≅_ 𝒮-B)
               (UARel.≅→≡ 𝒮-A)
               (UARel.≅→≡ 𝒮-B)
               F

-- fiberwise relational isomorphisms

module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {A' : Type ℓA'} {𝒮-A' : UARel A' ℓ≅A'}
  (F : Iso A A')
  {B : A → Type ℓB} (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B)
  {B' : A' → Type ℓB'} (𝒮ᴰ-B' : DUARel 𝒮-A' B' ℓ≅B') where

  open UARel 𝒮-A
  open DUARel 𝒮ᴰ-B renaming (_≅ᴰ⟨_⟩_ to _≅B⟨_⟩_
                            ; uaᴰ to uaB
                            ; fiberRel to fiberRelB
                            ; uaᴰρ to uaᴰρB)
  open DUARel 𝒮ᴰ-B' renaming (_≅ᴰ⟨_⟩_ to _≅B'⟨_⟩_
                             ; uaᴰ to uaB'
                             ; fiberRel to fiberRelB'
                             ; uaᴰρ to uaᴰρB')

  private
    f = Iso.fun F

    -- the following can of course be done slightly more generally
    -- for fiberwise binary relations

    F*fiberRelB' : (a : A) → Rel (B' (f a)) (B' (f a)) ℓ≅B'
    F*fiberRelB' a = fiberRelB' (f a)

  module _ (G : (a : A) → RelIso (fiberRelB a) (F*fiberRelB' a)) where
    private
      fiberIsoOver : (a : A) → Iso (B a) (B' (f a))
      fiberIsoOver a
        = RelIso→Iso (fiberRelB a)
                     (F*fiberRelB' a)
                     (equivFun (uaᴰρB _ _))
                     (equivFun (uaᴰρB' _ _))
                     (G a)

    -- DUARelFiberIsoOver→TotalIso produces an isomorphism of total spaces
    -- from a relational isomorphism between B a and (F * B) a
    𝒮ᴰ-fiberIsoOver→totalIso : Iso (Σ A B) (Σ A' B')
    𝒮ᴰ-fiberIsoOver→totalIso = Σ-cong-iso F fiberIsoOver

-- Special cases:
-- Subtypes
𝒮-type : (A : Type ℓ) → UARel A ℓ
UARel._≅_ (𝒮-type A) = _≡_
UARel.ua (𝒮-type A) a a' = idEquiv (a ≡ a')

module _ {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) where
  𝒮ᴰ-subtype : (P : A → hProp ℓP) → DUARel 𝒮-A (λ a → P a .fst) ℓ-zero
  𝒮ᴰ-subtype P
    = 𝒮ᴰ-make-2 (λ _ _ _ → Unit)
                (λ _ → tt)
                λ a p → isOfHLevelRespectEquiv 0
                                               (invEquiv (Σ-contractSnd (λ _ → isContrUnit)))
                                               (inhProp→isContr p (P a .snd))

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:
{-

This file contains:
    - the abelianization of groups as a coequalizer of sets as performed
      in https://1lab.dev/Algebra.Group.Ab.Free.html
    - the proof that this way of defining the abelianization of groups is equivalent to defining
      it as a HIT, more precisely that there is a unique isomorphism between the resulting
      abelian groups

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Abelianization.AbelianizationAsCoeq where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Sigma

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
  using (isPropIsGroupHom; compGroupHom; idGroupHom; compGroupHomAssoc; invGroupIso;
         compGroupHomId; GroupIso≡; GroupIso→GroupHom)

open import Cubical.Algebra.AbGroup.Base

open import Cubical.HITs.SetCoequalizer

open import Cubical.Algebra.Group.Abelianization.Base
  renaming (Abelianization to HITAbelianization;
            η to HITη;
            comm to HITcomm;
            isset to HITisset)

open import Cubical.Algebra.Group.Abelianization.Properties
  hiding (elimProp; elimProp2; elimProp3; elimContr; elimContr2; rec; rec2)
  renaming (AbelianizationAbGroup to HITasAbelianGroup;
            AbelianizationHom to HITηAsGroupHom)
open Cubical.Algebra.Group.Abelianization.Properties.UniversalProperty
  renaming (inducedHom to HITinducedHom;
            commutativity to HITcommutativity;
            uniqueness to HITuniqueness)

private
  variable
    ℓ : Level
    G : Group ℓ

module AbelianizationAsCoeq (G : Group ℓ) where
  open GroupStr {{...}}
  open GroupTheory G
  private
    instance
      _ = snd G
    G' = fst G

  {-
    The definition of the abelianization of a group as a coequalizer of sets. The generality
    of the coequalized functions will be needed to define the group structure on the
    abelianization.
  -}
  Abelianization : Type ℓ
  Abelianization =
    SetCoequalizer {A = G' × G' × G'} {B = G'}
      (λ (x , y , z) → x · y · z)
      (λ (x , y , z) → x · z · y)

  -- some convenient relabellings, so it looks more similar to the abelianization as a HIT.
  incAb : G' → Abelianization
  incAb = inc

  comm : (x y z : G') → incAb (x · (y · z)) ≡ incAb (x · (z · y))
  comm = λ x y z → coeq (x , y , z)

  {-
    Definition of the group structure on the abelianization. Here the generality of the
    coequalized functions is used.
  -}
  _·Ab_ : Abelianization → Abelianization → Abelianization
  _·Ab_ =
    rec2
      squash
      (λ x y → incAb (x · y))
      (λ (a , b , c) d →
        incAb ((a · (b · c)) · d) ≡⟨ cong (λ x → incAb (x · d)) (assoc _ _ _) ⟩
        incAb (((a · b) · c) · d) ≡⟨ cong incAb (sym (assoc (a · b) c d)) ⟩
        incAb ((a · b) · (c · d)) ≡⟨ comm (a · b) c d ⟩
        incAb ((a · b) · (d · c)) ≡⟨ cong incAb (sym (assoc _ _ _)) ⟩
        incAb (a · (b · (d · c))) ≡⟨ cong (λ x → incAb (a · x)) (assoc _ _ _) ⟩
        incAb (a · ((b · d) · c)) ≡⟨ comm a (b · d) c ⟩
        incAb (a · (c · (b · d))) ≡⟨ cong (λ x → incAb (a · x)) (assoc _ _ _) ⟩
        incAb (a · ((c · b) · d)) ≡⟨ cong incAb (assoc a (c · b) d) ⟩
        incAb ((a · (c · b)) · d) ∎)
      (λ (b , c , d) a →
        incAb (a · (b · (c · d))) ≡⟨ cong incAb (assoc _ _ _) ⟩
        incAb ((a · b) · (c · d)) ≡⟨ comm (a · b) c d ⟩
        incAb ((a · b) · (d · c)) ≡⟨ cong incAb (sym (assoc _ _ _)) ⟩
        incAb (a · (b · (d · c))) ∎)

  1Ab : Abelianization
  1Ab = incAb 1g

  invAb : Abelianization → Abelianization
  invAb =
    rec
      squash
      (λ x → incAb (inv x))
      (λ (a , b , c) →
        incAb (inv (a · (b · c)))              ≡⟨ cong incAb (invDistr a (b · c)) ⟩
        incAb (inv (b · c) · inv a)            ≡⟨ cong (λ x → incAb (x · inv a)) (invDistr b c) ⟩
        incAb ((inv c · inv b) · inv a)        ≡⟨ cong
                                                    incAb
                                                    (sym (lid ((inv c · inv b) · inv a))) ⟩
        incAb (1g · ((inv c · inv b) · inv a)) ≡⟨ comm 1g (inv c · inv b) (inv a) ⟩
        incAb (1g · (inv a · (inv c · inv b))) ≡⟨ cong incAb (lid (inv a · (inv c · inv b))) ⟩
        incAb (inv a · (inv c · inv b))        ≡⟨ comm (inv a) (inv c) (inv b) ⟩
        incAb (inv a · (inv b · inv c))        ≡⟨ cong
                                                    incAb
                                                    (sym (lid (inv a · (inv b · inv c)))) ⟩
        incAb (1g · (inv a · (inv b · inv c))) ≡⟨ comm 1g (inv a) (inv b · inv c) ⟩
        incAb (1g · ((inv b · inv c) · inv a)) ≡⟨ cong incAb (lid ((inv b · inv c) · inv a)) ⟩
        incAb ((inv b · inv c) · inv a)        ≡⟨ cong
                                                    (λ x → incAb (x · inv a))
                                                    (sym (invDistr c b)) ⟩
        incAb (inv (c · b) · inv a)            ≡⟨ cong incAb (sym (invDistr a (c · b))) ⟩
        incAb (inv (a · (c · b))) ∎)

  assocAb : (x y z : Abelianization) → x ·Ab (y ·Ab z) ≡ (x ·Ab y) ·Ab z
  assocAb =
    elimProp3
      (λ x y z → squash (x ·Ab (y ·Ab z))
      ((x ·Ab y) ·Ab z))
      (λ x y z → cong incAb (assoc x y z))

  ridAb : (x : Abelianization) → x ·Ab 1Ab ≡ x
  ridAb =
    elimProp
      (λ x → squash (x ·Ab 1Ab) x)
      (λ x → cong incAb (rid x))

  rinvAb : (x : Abelianization) → x ·Ab (invAb x) ≡ 1Ab
  rinvAb =
    elimProp
      (λ x → squash (x ·Ab (invAb x)) 1Ab)
      (λ x → (incAb x) ·Ab (invAb (incAb x)) ≡⟨ refl ⟩
             (incAb x) ·Ab (incAb (inv x))   ≡⟨ refl ⟩
             incAb (x · (inv x))             ≡⟨ cong incAb (fst (inverse x)) ⟩
             incAb 1g                        ≡⟨ refl ⟩
             1Ab ∎)

  commAb : (x y : Abelianization) → x ·Ab y ≡ y ·Ab x
  commAb =
    elimProp2
      (λ x y → squash (x ·Ab y) (y ·Ab x))
      (λ x y → (incAb x) ·Ab (incAb y) ≡⟨ refl ⟩
               incAb (x · y)           ≡⟨ cong incAb (sym (lid (x · y))) ⟩
               incAb (1g · (x · y))    ≡⟨ comm 1g x y ⟩
               incAb (1g · (y · x))    ≡⟨ cong incAb (lid (y · x)) ⟩
               incAb (y · x)           ≡⟨ refl ⟩
               (incAb y) ·Ab (incAb x) ∎)

  -- The proof that the abelianization is in fact an abelian group.
  asAbelianGroup : AbGroup ℓ
  asAbelianGroup = makeAbGroup 1Ab _·Ab_ invAb squash assocAb ridAb rinvAb commAb

  -- The proof that incAb can be seen as a group homomorphism
  incAbAsGroupHom : GroupHom G (AbGroup→Group asAbelianGroup)
  incAbAsGroupHom = f , fIsHom
    where
    f = λ x → incAb x
    fIsHom : IsGroupHom (snd G) f (snd (AbGroup→Group asAbelianGroup))
    IsGroupHom.pres· fIsHom = λ x y → refl
    IsGroupHom.pres1 fIsHom = refl
    IsGroupHom.presinv fIsHom = λ x → refl

AbelianizationAbGroup : (G : Group ℓ) → AbGroup ℓ
AbelianizationAbGroup G = AbelianizationAsCoeq.asAbelianGroup G

AbelianizationHom : (G : Group ℓ) → GroupHom G (AbGroup→Group (AbelianizationAbGroup G))
AbelianizationHom G = AbelianizationAsCoeq.incAbAsGroupHom G

module UniversalPropertyCoeq (G : Group ℓ) where
  open GroupStr {{...}}
  open GroupTheory G
  open AbelianizationAsCoeq G
  private
    instance
      _ = snd G
    G' = fst G
  abstract
    {- The proof of the universal property of the abelianization.

    G -incAb-> Abelianization
    \         .
      \       .
        f   ∃! inducedHom
          \   .
            \ .
              H
    commuting diagram
    -}
    inducedHom : (H : AbGroup ℓ)
              → (f : GroupHom G (AbGroup→Group H))
              → AbGroupHom asAbelianGroup H
    inducedHom H f = g , gIsHom
      where open IsGroupHom
            instance
              _ : GroupStr (fst H)
              _ = snd (AbGroup→Group H)
            f' : fst G → fst H
            f' = fst f
            g : Abelianization → fst H
            g = rec
                  (isSetAbGroup H)
                  (λ x → (f') x)
                  (λ (a , b , c) →
                    f' (a · b · c)           ≡⟨ (snd f).pres· a (b · c) ⟩
                    (f' a) · (f' (b · c))    ≡⟨ cong (λ x → (f' a) · x) ((snd f).pres· b c) ⟩
                    (f' a) · (f' b) · (f' c) ≡⟨ cong (λ x → (f' a) · x)
                                                     ((snd H).AbGroupStr.comm (f' b) (f' c)) ⟩
                    (f' a) · (f' c) · (f' b) ≡⟨ cong (λ x → (f' a) · x)
                                                     (sym ((snd f).pres· c b)) ⟩
                    (f' a) · (f' (c · b))    ≡⟨ sym ((snd f).pres· a (c · b)) ⟩
                    f' (a · c · b) ∎)
            gIsHom : IsGroupHom (snd (AbGroup→Group asAbelianGroup)) g (snd (AbGroup→Group H))
            pres· gIsHom =
              elimProp2
                (λ x y → isSetAbGroup H _ _)
                ((snd f).pres·)
            pres1 gIsHom = (snd f).pres1
            presinv gIsHom =
              elimProp
                (λ x → isSetAbGroup H _ _)
                ((snd f).presinv)

    commutativity : (H : AbGroup ℓ)
                  → (f : GroupHom G (AbGroup→Group H))
                  → (compGroupHom incAbAsGroupHom (inducedHom H f) ≡ f)
    commutativity H f =
        Σ≡Prop
          (λ _ → isPropIsGroupHom _ _)
          (λ i x → q x i)
      where q : (x : fst  G)
                → fst (compGroupHom incAbAsGroupHom (inducedHom H f)) x ≡ fst f x
            q = (λ x → refl)

    uniqueness : (H : AbGroup ℓ)
              → (f : GroupHom G (AbGroup→Group H))
              → (g : AbGroupHom asAbelianGroup H)
              → (p : compGroupHom incAbAsGroupHom g ≡ f)
              → (g ≡ inducedHom H f)
    uniqueness H f g p =
        Σ≡Prop
          (λ _ → isPropIsGroupHom _ _)
          (λ i x →  q x i)
      where q : (x : Abelianization)
                →  fst g x ≡ fst (inducedHom H f) x
            q = elimProp
                  (λ _ → isSetAbGroup H _ _)
                  (λ x → fst g (incAb x) ≡⟨ cong (λ f → f x) (cong fst p) ⟩
                        (fst f) x       ≡⟨ refl ⟩
                        fst (inducedHom H f) (incAb x)∎)

module IsoCoeqHIT (G : Group ℓ) where
  open GroupStr {{...}}
  open GroupTheory G
  open AbelianizationAsCoeq G
  open UniversalPropertyCoeq G
  private
    instance
      _ = snd G
    G' = fst G

  {- The proof that defining the abelianization of groups as a coequalizer of sets is equivalent
  to defining it as a HIT, more precisely that there is an isomorphism between the resulting
  abelian groups unique with respect to commuting with the constructors η and inc.

  G -incAb-> abelianization as coequalizer
   \         .
     \       .
       η   ∃! isomorphism
         \   .
           \ .
             abelianization as HIT
  commuting diagram
  -}
  isomorphism : AbGroupIso asAbelianGroup (HITasAbelianGroup G)
  isomorphism = h , hIsHomo
    where
    f = inducedHom (HITasAbelianGroup G) (HITηAsGroupHom G)
    g = HITinducedHom G asAbelianGroup incAbAsGroupHom

    HITgfcomm : compGroupHom (HITηAsGroupHom G) (compGroupHom g f) ≡ (HITηAsGroupHom G)
    HITgfcomm =
      compGroupHom (HITηAsGroupHom G) (compGroupHom g f)
        ≡⟨ sym (compGroupHomAssoc (HITηAsGroupHom G) g f) ⟩
      compGroupHom (compGroupHom (HITηAsGroupHom G) g) f
        ≡⟨ cong (λ x → compGroupHom x f) (HITcommutativity G asAbelianGroup incAbAsGroupHom) ⟩
      compGroupHom incAbAsGroupHom f
        ≡⟨ commutativity (HITasAbelianGroup G) (HITηAsGroupHom G) ⟩
      (HITηAsGroupHom G) ∎

    HITidcomm : compGroupHom (HITηAsGroupHom G) idGroupHom ≡ HITηAsGroupHom G
    HITidcomm = compGroupHomId (HITηAsGroupHom G)

    HITidIsInduced : HITinducedHom G (HITasAbelianGroup G) (HITηAsGroupHom G) ≡ idGroupHom
    HITidIsInduced = sym (HITuniqueness G
                           (HITasAbelianGroup G)
                           (HITηAsGroupHom G)
                           idGroupHom
                           HITidcomm)

    HITgfIsInduced : HITinducedHom G (HITasAbelianGroup G) (HITηAsGroupHom G) ≡ compGroupHom g f
    HITgfIsInduced = sym (HITuniqueness G
                           (HITasAbelianGroup G)
                           (HITηAsGroupHom G)
                           (compGroupHom g f)
                           HITgfcomm)

    i : idGroupHom ≡ compGroupHom g f
    i = idGroupHom ≡⟨ sym HITidIsInduced ⟩
        HITinducedHom G (HITasAbelianGroup G) (HITηAsGroupHom G) ≡⟨ HITgfIsInduced ⟩
        compGroupHom g f ∎

    fgcomm : compGroupHom incAbAsGroupHom (compGroupHom f g) ≡ incAbAsGroupHom
    fgcomm =
      compGroupHom incAbAsGroupHom (compGroupHom f g)
        ≡⟨ sym (compGroupHomAssoc incAbAsGroupHom f g) ⟩
      compGroupHom (compGroupHom incAbAsGroupHom f) g
        ≡⟨ cong (λ x → compGroupHom x g) (commutativity (HITasAbelianGroup G) (HITηAsGroupHom G)) ⟩
      compGroupHom (HITηAsGroupHom G) g
        ≡⟨ (HITcommutativity G) asAbelianGroup incAbAsGroupHom ⟩
      incAbAsGroupHom ∎

    idcomm : compGroupHom incAbAsGroupHom idGroupHom ≡ incAbAsGroupHom
    idcomm = compGroupHomId incAbAsGroupHom

    idIsInduced : inducedHom asAbelianGroup incAbAsGroupHom ≡ idGroupHom
    idIsInduced = sym (uniqueness asAbelianGroup incAbAsGroupHom idGroupHom idcomm)

    fgIsInduced : inducedHom asAbelianGroup incAbAsGroupHom ≡ compGroupHom f g
    fgIsInduced = sym (uniqueness asAbelianGroup incAbAsGroupHom (compGroupHom f g) fgcomm)

    j : idGroupHom ≡ compGroupHom f g
    j = idGroupHom ≡⟨ sym idIsInduced ⟩
        inducedHom asAbelianGroup incAbAsGroupHom ≡⟨ fgIsInduced ⟩
        compGroupHom f g ∎

    h = iso
          (fst f)
          (fst g)
          (λ b → cong (λ e → e b) (cong fst (sym i)))
          (λ a → cong (λ e → e a) (cong fst (sym j)))
    hIsHomo = snd f

  isomorphismCommutativity : compGroupHom incAbAsGroupHom (GroupIso→GroupHom isomorphism)
                               ≡ (HITηAsGroupHom G)
  isomorphismCommutativity = commutativity (HITasAbelianGroup G) (HITηAsGroupHom G)

  isomorphismUniqueness : (h : AbGroupIso asAbelianGroup (HITasAbelianGroup G))
    → (hcomm : compGroupHom incAbAsGroupHom (GroupIso→GroupHom h) ≡ (HITηAsGroupHom G))
    → h ≡ isomorphism
  isomorphismUniqueness h hcomm = GroupIso≡ p
    where
      r : (x : fst asAbelianGroup)
        → fst (compGroupHom (GroupIso→GroupHom h) (GroupIso→GroupHom (invGroupIso h))) x ≡ x
      r = λ x → (h .fst .Iso.leftInv) x

      leftInvGroupHom : (compGroupHom
                          (GroupIso→GroupHom h)
                          (GroupIso→GroupHom (invGroupIso h))) ≡ idGroupHom
      leftInvGroupHom =
        Σ≡Prop
          (λ _ → isPropIsGroupHom _ _)
          (λ i x → r x i)

      q : (g : fst  G)
        → fst (compGroupHom
                (HITηAsGroupHom G)
                (GroupIso→GroupHom (invGroupIso h))) g ≡ fst incAbAsGroupHom g
      q = λ g
        → fst (compGroupHom (HITηAsGroupHom G) (GroupIso→GroupHom (invGroupIso h))) g
            ≡⟨ cong
                 (λ f → f g)
                 (cong fst (cong
                             (λ f → compGroupHom f (GroupIso→GroupHom (invGroupIso h)))
                             (sym hcomm))) ⟩
          fst (compGroupHom
                (compGroupHom incAbAsGroupHom (GroupIso→GroupHom h))
                (GroupIso→GroupHom (invGroupIso h))) g
            ≡⟨ cong
                 (λ f → f g)
                 (cong fst (compGroupHomAssoc
                              incAbAsGroupHom
                              (GroupIso→GroupHom h)
                              (GroupIso→GroupHom (invGroupIso h)))) ⟩
          fst (compGroupHom
                incAbAsGroupHom
                (compGroupHom (GroupIso→GroupHom h) (GroupIso→GroupHom (invGroupIso h)))) g
            ≡⟨ cong
                (λ f → f g)
                (cong fst (cong (λ f → (compGroupHom incAbAsGroupHom f)) leftInvGroupHom)) ⟩
          fst incAbAsGroupHom g ∎

      isocomm : compGroupHom
                  (HITηAsGroupHom G)
                  (GroupIso→GroupHom (invGroupIso h)) ≡ incAbAsGroupHom
      isocomm =
        Σ≡Prop
          (λ _ → isPropIsGroupHom _ _)
          (λ i x → q x i)

      p : h .fst ≡ isomorphism .fst
      p =
        Iso≡Set
          (isSetAbGroup asAbelianGroup)
          (isSetAbGroup (HITasAbelianGroup G))
          (h .fst)
          (isomorphism .fst)
          (λ x → cong
                   (λ f → f x)
                   (cong fst (uniqueness
                               (HITasAbelianGroup G)
                               (HITηAsGroupHom G)
                               (GroupIso→GroupHom h)
                               hcomm)))
          (λ x → cong
                   (λ f → f x)
                   (cong fst (HITuniqueness G
                                asAbelianGroup
                                incAbAsGroupHom
                                (GroupIso→GroupHom (invGroupIso h))
                                isocomm)))

AbelianizationComparisonIsomorphism : (G : Group ℓ)
                                    → AbGroupIso (AbelianizationAbGroup G) (HITasAbelianGroup G)
AbelianizationComparisonIsomorphism G = IsoCoeqHIT.isomorphism G

max_stars_repo_name: gmagaf/cubical

max_issues_repo_name: gmagaf/cubical

max_forks_repo_name: gmagaf/cubical


text:
module list-to-string where

open import list
open import string

𝕃-to-string : ∀ {ℓ} {A : Set ℓ} → (f : A → string) → (separator : string) → 𝕃 A → string
𝕃-to-string f sep [] = ""
𝕃-to-string f sep (x1 :: (x2 :: xs)) = (f x1) ^ sep ^ (𝕃-to-string f sep (x2 :: xs))
𝕃-to-string f sep (x1 :: []) = (f x1)

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
module AbstractRationals where

open import Algebra
open import Data.Integer.Base using (+0)
open import Data.Maybe.Base using (just; nothing; decToMaybe)
open import Data.Rational.Base as ℚ public hiding (_+_; _*_; _-_)
open import Data.Rational.Properties as ℚ public
  using (module ≤-Reasoning; <⇒≤)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Function.Base
open import Data.Product using (_×_; _,_)

open import Tactic.RingSolver.Core.AlmostCommutativeRing
open import Tactic.RingSolver.NonReflective (fromCommutativeRing ℚ.+-*-commutativeRing (λ x → decToMaybe (0ℚ ℚ.≟ x)))

open import RationalUtils as ℚ public using (2ℚ; 3ℚ)

infixl 7 _*_
infixl 6 _+_ _-_

abstract
  _+_ : ℚ → ℚ → ℚ
  _+_ = ℚ._+_

  _*_ : ℚ → ℚ → ℚ
  _*_ = ℚ._*_

  _-_ : ℚ → ℚ → ℚ
  _-_ = ℚ._-_

  +-eq : _+_ ≡ ℚ._+_
  +-eq = refl

  *-eq : _*_ ≡ ℚ._*_
  *-eq = refl

  neg-eq : _-_ ≡ ℚ._-_
  neg-eq = refl

  p+q-p≡q : ∀ p q → p + q - p ≡ q
  p+q-p≡q = ℚ.p+q-p≡q

  p+q-q≡p : ∀ p q → p + q - q ≡ p
  p+q-q≡p = ℚ.p+q-q≡p

  p-q+q≡p : ∀ p q → p - q + q ≡ p
  p-q+q≡p = ℚ.p-q+q≡p

  p-[p+q]≡q : ∀ p q → p - (p + q) ≡ q
  p-[p+q]≡q = ℚ.p-[p+q]≡q

  ∣p-q∣≤∣p∣+∣q∣ : ∀ p q → ∣ p - q ∣ ≤ ∣ p ∣ + ∣ q ∣
  ∣p-q∣≤∣p∣+∣q∣ = ℚ.∣p-q∣≤∣p∣+∣q∣

  ∣p∣≤q⇒-q≤p≤q : ∀ p {q} → ∣ p ∣ ≤ q → - q ≤ p × p ≤ q
  ∣p∣≤q⇒-q≤p≤q p = ℚ.∣p∣≤q⇒-q≤p≤q p

  -p<q<p⇒∣q∣<p : ∀ {p q} → - p < q → q < p → ∣ q ∣ < p
  -p<q<p⇒∣q∣<p = ℚ.-p<q<p⇒∣q∣<p

  2*p≡p+p : ∀ p → 2ℚ * p ≡ p + p
  2*p≡p+p = ℚ.2*p≡p+p

  +-assoc : Associative _≡_ _+_
  +-assoc = ℚ.+-assoc

  +-monoˡ-≤ : ∀ r → (_+ r) Preserves _≤_ ⟶ _≤_
  +-monoˡ-≤ = ℚ.+-monoˡ-≤

  +-monoʳ-≤ : ∀ r → (_+_ r) Preserves _≤_ ⟶ _≤_
  +-monoʳ-≤ = ℚ.+-monoʳ-≤

  +-mono-≤ : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
  +-mono-≤ = ℚ.+-mono-≤

  *-monoʳ-≤ : ∀ r → Positive r → (r *_) Preserves _≤_ ⟶ _≤_
  *-monoʳ-≤ = ℚ.*-monoʳ-≤

  ∣p+q∣≤∣p∣+∣q∣ : ∀ p q → ∣ p + q ∣ ≤ ∣ p ∣ + ∣ q ∣
  ∣p+q∣≤∣p∣+∣q∣ = ℚ.∣p+q∣≤∣p∣+∣q∣

  ∣p*q∣≡∣p∣*∣q∣ : ∀ p q → ∣ p * q ∣ ≡ ∣ p ∣ * ∣ q ∣
  ∣p*q∣≡∣p∣*∣q∣ = ℚ.∣p*q∣≡∣p∣*∣q∣

  p<r-q⇒p+q<r : ∀ p q r → p < r - q → p + q < r
  p<r-q⇒p+q<r = ℚ.p<r-q⇒p+q<r

  2p+p≡3p : ∀ p → 2ℚ * p + p ≡ 3ℚ * p
  2p+p≡3p p = begin-equality
    2ℚ * p + p      ≡⟨ cong (2ℚ * p +_) (sym (ℚ.*-identityˡ p)) ⟩
    2ℚ * p + 1ℚ * p ≡⟨ sym (ℚ.*-distribʳ-+ p 2ℚ 1ℚ) ⟩
    (2ℚ + 1ℚ) * p   ∎
    where open ≤-Reasoning

  lem1 : ∀ a b c d e f g → a + (b + c) + d + (e + f + f - g) - (e + f + f - g) ≡
                           c + (a + f + (e + b + d + f)) - g - (f + f + (e - g))
  lem1 = solve 7 (λ a b c d e f g → (a ⊕ (b ⊕ c) ⊕ d ⊕ (e ⊕ f ⊕ f ⊕ (⊝ g)) ⊕ (⊝ (e ⊕ f ⊕ f ⊕ (⊝ g))) ,
                                    c ⊕ (a ⊕ f ⊕ (e ⊕ b ⊕ d ⊕ f)) ⊕ (⊝ g) ⊕ (⊝ (f ⊕ f ⊕ (e ⊕ (⊝ g)))))) refl

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
module Issue461 where

data D : Set where
data D : Set where


text:
{-# OPTIONS --no-auto-inline #-}
module Where where

open import Haskell.Prelude hiding (_+_; _*_; _-_)
open import Agda.Builtin.Nat

postulate
  bool2nat : Bool → Nat

-- no outer arguments
ex1 : Nat
ex1 = mult num + bool2nat true
  where
    num : Nat
    num = 42

    mult : Nat → Nat
    mult = _* 100

-- nested where
ex2 : Nat
ex2 = mult num + bool2nat true
  where
    num : Nat
    num = 42

    mult : Nat → Nat
    mult = _⊗ 100
      where
        _⊗_ = _*_

-- with outer arguments
ex3 : Nat → Bool → Nat
ex3 n b = mult num + bool2nat b
  where
    num = 42 + bool2nat b

    mult : Nat → Nat
    mult = _* n

-- nested where with outer arguments
ex4 : Bool → Nat
ex4 b = mult 42
  where
    mult : Nat → Nat
    mult n = bump n (bool2nat b)
      where
        bump : Nat → Nat → Nat
        bump x y = x * y + (n - bool2nat b)

ex4' : Bool → Nat
ex4' b = mult (bool2nat b)
  where
    mult : Nat → Nat
    mult n = bump n (bool2nat b)
      where
        bump : Nat → Nat → Nat
        bump x y = go (x * y) (n - bool2nat b)
          where
            go : Nat → Nat → Nat
            go z w = z + x + w + y + n + bool2nat b

-- with pattern matching and multiple clauses
ex5 : List Nat → Nat
ex5 [] = zro
  where
    zro : Nat
    zro = 0
ex5 (n ∷ ns) = mult num + 1
  where
    num = 42 + ex5 ns

    mult : Nat → Nat
    mult = _* n

-- mix of patterns + inner multiple clauses + nested where
ex6 : List Nat → Bool → Nat
ex6 [] b = zro
  where
    zro : Nat
    zro = 0
ex6 (n ∷ ns) b = mult (num ∷ 1 ∷ [])
  where
    mult : List Nat → Nat
    mult [] = bump 5 (bool2nat b)
      where
        bump : Nat → Nat → Nat
        bump x y = x * y + n
    mult (m ∷ ms) = bump n m
      where
        bump : Nat → Nat → Nat
        bump x y = x * y + (m - n)

    num = 42 + ex6 ns true

ex7 : Nat → Nat
ex7 n₀ = go₁ n₀
  where
    go₁ : Nat → Nat
    go₁ n₁ = go₂ (n₀ + n₁)
      where
        go₂ : Nat → Nat
        go₂ n₂ = n₀ + n₁ + n₂

ex7' : Nat → Nat
ex7' n₀ = go₁ n₀
  where
    go₁ : Nat → Nat
    go₁ n₁ = go₂ (n₀ + n₁)
      where
        go₂ : Nat → Nat
        go₂ n₂ = go₃ (n₀ + n₁ + n₂)
          where
            go₃ : Nat → Nat
            go₃ n₃ = n₀ + n₁ + n₂ + n₃

ex8 : Nat
ex8 = n₂
  where
    n₁ : Nat
    n₁ = 1
    n₂ = n₁ + 1

{-# COMPILE AGDA2HS bool2nat #-}
{-# COMPILE AGDA2HS ex1 #-}
{-# COMPILE AGDA2HS ex2 #-}
{-# COMPILE AGDA2HS ex3 #-}
{-# COMPILE AGDA2HS ex4 #-}
{-# COMPILE AGDA2HS ex4' #-}
{-# COMPILE AGDA2HS ex5 #-}
{-# COMPILE AGDA2HS ex6 #-}
{-# COMPILE AGDA2HS ex7 #-}
{-# COMPILE AGDA2HS ex7' #-}
{-# COMPILE AGDA2HS ex8 #-}


text:
-- Andreas, 2015-10-05, issue reported by mechvel, test case by Jesper Cockx

-- {-# OPTIONS -v tc.term.exlam:20 #-}

abstract
  foo : Set₁
  foo = Set
    where
      AbstractSet₁ : Set₂
      AbstractSet₁ = Set₁
      f : Set → AbstractSet₁
      f = λ { _ → Set }

{-# NON_TERMINATING #-}
loop : Set → Set
loop = λ { A → loop A }


text:
module Issue65 where

open import Haskell.Prelude

yeet : (c : Bool) → ({{c ≡ true}} → a) → ({{c ≡ false}} → a) → a
yeet false x y = y {{refl}}
yeet true  x y = x {{refl}}
{-# COMPILE AGDA2HS yeet #-}

-- The branches start with instance lambdas that should be dropped.
xx : Int
xx = yeet true 1 2
{-# COMPILE AGDA2HS xx #-}


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Polynomials.Multivariate.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat renaming (_+_ to _+n_)
open import Cubical.Data.Vec

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

private variable
  ℓ ℓ' : Level

module _ (A' : CommRing ℓ) where
  private
    A = fst A'
  open CommRingStr (snd A')

-----------------------------------------------------------------------------
-- Definition

  data Poly (n : ℕ) : Type ℓ where
    -- elements
    0P     : Poly n
    base   : (v : Vec ℕ n) → (a : A) → Poly n
    _Poly+_  : (P : Poly n) → (Q : Poly n) → Poly n
      -- AbGroup eq
    Poly+-assoc : (P Q R : Poly n) → P Poly+ (Q Poly+ R) ≡ (P Poly+ Q) Poly+ R
    Poly+-Rid   : (P : Poly n) → P Poly+ 0P ≡ P
    Poly+-comm  : (P Q : Poly n) → P Poly+ Q ≡ Q Poly+ P
      -- Base eq
    base-0P : (v : Vec ℕ n) → base v 0r ≡ 0P
    base-Poly+     : (v : Vec ℕ n) → (a b : A) → (base v a) Poly+ (base v b) ≡ base v (a + b)
      -- Set Trunc
    trunc : isSet(Poly n)

-----------------------------------------------------------------------------
-- Induction and Recursion

module _ (A' : CommRing ℓ) where
  private
    A = fst A'
  open CommRingStr (snd A')

  module Poly-Ind-Set
    -- types
    (n : ℕ)
    (F : (P : Poly A' n) → Type ℓ')
    (issd : (P : Poly A' n) → isSet (F P))
    -- elements
    (0P* : F 0P)
    (base* : (v : Vec ℕ n) → (a : A) → F (base v a))
    (_Poly+*_ : {P Q : Poly A' n} → (PS : F P) → (QS : F Q) → F (P Poly+ Q))
    -- AbGroup eq
    (Poly+-assoc* : {P Q R : Poly A' n} → (PS : F P) → (QS : F Q) → (RS : F R)
                    → PathP (λ i → F (Poly+-assoc P Q R i)) (PS Poly+* (QS Poly+* RS)) ((PS Poly+* QS) Poly+* RS))
    (Poly+-Rid*   : {P : Poly A' n} → (PS : F P) →
                   PathP (λ i → F (Poly+-Rid P i)) (PS Poly+* 0P*) PS)
    (Poly+-comm*  : {P Q : Poly A' n} → (PS : F P) → (QS : F Q)
                    → PathP (λ i → F (Poly+-comm P Q i)) (PS Poly+* QS) (QS Poly+* PS))
    -- Base eq
    (base-0P* : (v : Vec ℕ n) → PathP (λ i → F (base-0P v i)) (base* v 0r) 0P*)
    (base-Poly+*     : (v : Vec ℕ n) → (a b : A)
                     → PathP (λ i → F (base-Poly+ v a b i)) ((base* v a) Poly+* (base* v b)) (base* v (a + b)))
    where

    f : (P : Poly A' n) → F P
    f 0P = 0P*
    f (base v a) = base* v a
    f (P Poly+ Q) = (f P) Poly+* (f Q)
    f (Poly+-assoc P Q R i) = Poly+-assoc* (f P) (f Q) (f R) i
    f (Poly+-Rid P i) = Poly+-Rid* (f P) i
    f (Poly+-comm P Q i) = Poly+-comm* (f P) (f Q) i
    f (base-0P v i) = base-0P* v i
    f (base-Poly+ v a b i) = base-Poly+* v a b i
    f (trunc P Q p q i j) = isOfHLevel→isOfHLevelDep 2 issd  (f P) (f Q) (cong f p) (cong f q) (trunc P Q p q) i j

  module Poly-Rec-Set
    -- types
    (n  : ℕ)
    (B  : Type ℓ')
    (iss : isSet B)
    -- elements
    (0P*      : B)
    (base*    : (v : Vec ℕ n) → (a : A) → B)
    (_Poly+*_ : B → B → B)
    -- AbGroup eq
    (Poly+-assoc* : (PS QS RS : B) → (PS Poly+* (QS Poly+* RS)) ≡ ((PS Poly+* QS) Poly+* RS))
    (Poly+-Rid*   : (PS : B)       → (PS Poly+* 0P*) ≡  PS)
    (Poly+-comm*  : (PS QS : B)    → (PS Poly+* QS) ≡ (QS Poly+* PS))
    -- Base eq
    (base-0P* : (v : Vec ℕ n) → (base* v 0r) ≡  0P*)
    (base-Poly+*     : (v : Vec ℕ n) → (a b : A) → ((base* v a) Poly+* (base* v b)) ≡ (base* v (a + b)))
    where

    f : Poly A' n → B
    f = Poly-Ind-Set.f n (λ _ → B) (λ _ → iss) 0P* base* _Poly+*_ Poly+-assoc* Poly+-Rid* Poly+-comm* base-0P* base-Poly+*

  module Poly-Ind-Prop
    -- types
    (n : ℕ)
    (F : (P : Poly A' n) → Type ℓ')
    (ispd : (P : Poly A' n) → isProp (F P))
    -- elements
    (0P* : F 0P)
    (base* : (v : Vec ℕ n) → (a : A) → F (base v a))
    (_Poly+*_ : {P Q : Poly A' n} → (PS : F P) → (QS : F Q) → F (P Poly+ Q))
    where

    f : (P : Poly A' n) → F P
    f = Poly-Ind-Set.f n F (λ P → isProp→isSet (ispd P)) 0P* base* _Poly+*_
          (λ {P Q R} PS QS RQ → toPathP (ispd _ (transport (λ i → F (Poly+-assoc P Q R i)) _) _))
          (λ {P} PS           → toPathP (ispd _ (transport (λ i → F (Poly+-Rid P i))       _) _))
          (λ {P Q} PS QS      → toPathP (ispd _ (transport (λ i → F (Poly+-comm P Q i))    _) _))
          (λ v                → toPathP (ispd _ (transport (λ i → F (base-0P v i))    _) _))
          (λ v a b            → toPathP (ispd _ (transport (λ i → F (base-Poly+ v a b i))    _) _))

  module Poly-Rec-Prop
    -- types
    (n : ℕ)
    (B : Type ℓ')
    (isp : isProp B)
    -- elements
    (0P* : B)
    (base* : (v : Vec ℕ n) → (a : A) → B)
    (_Poly+*_ : B → B → B)
    where

    f : Poly A' n → B
    f = Poly-Ind-Prop.f n (λ _ → B) (λ _ → isp) 0P* base* _Poly+*_

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
open import Agda.Builtin.Sigma renaming (fst to proj₁; snd to proj₂)
open import Agda.Builtin.Nat renaming (Nat to ℕ)

NEX : Set₁
NEX = Σ Set λ A → (ℕ → A)

variable
  A : NEX
  B : A .proj₁ → NEX

[Σ] : (A : NEX) → (B : A .proj₁ → NEX) → NEX
[Σ] A B .proj₁ = Σ (A .proj₁) λ x → B x .proj₁
[Σ] A B .proj₂ n = A .proj₂ n , B _ .proj₂ n

_[→]_ : (A B : NEX) → NEX
(A [→] B) .proj₁ = A .proj₁ → B .proj₁
(A [→] B) .proj₂ n x = B .proj₂ n

-- B.A is underdetermined and solved with (A .proj₁ , _snd) for a fresh meta
-- _snd : ℕ → A .proj₁, which is then generalized over. The bug was that _snd
-- turned into an explicit rather than implicit argument.
[π₁] : ([Σ] A B [→] A) .proj₁
[π₁] {A = A} {B = B} {snd = snd} x = x .proj₁

max_forks_repo_name: shlevy/agda


text:
module Haskell.Prim.Tuple where

open import Agda.Builtin.List

open import Haskell.Prim

private
  variable
    as : List Set

--------------------------------------------------
-- Tuples

infixr 5 _∷_
data Tuple : List Set → Set where
  []  : Tuple []
  _∷_ : a → Tuple as → Tuple (a ∷ as)

infix 3 _×_ _×_×_

_×_ : (a b : Set) → Set
a × b = Tuple (a ∷ b ∷ [])

_×_×_ : (a b c : Set) → Set
a × b × c = Tuple (a ∷ b ∷ c ∷ [])

infix -1 _,_ _,_,_

pattern _,_     x y     = x Tuple.∷ y Tuple.∷ []
pattern _,_,_   x y z   = x Tuple.∷ y Tuple.∷ z Tuple.∷ []

uncurry : (a → b → c) → a × b → c
uncurry f (x , y) = f x y

curry : (a × b → c) → a → b → c
curry f x y = f (x , y)

fst : a × b → a
fst (x , _) = x

snd : a × b → b
snd (_ , y) = y

first : (a → b) → a × c → b × c
first f (x , y) = f x , y

second : (a → b) → c × a → c × b
second f (x , y) = x , f y

_***_ : (a → b) → (c → d) → a × c → b × d
(f *** g) (x , y) = f x , g y


text:
module Prelude.Vec where

open import Prelude.Nat
open import Prelude.Fin
open import Prelude.Function
open import Prelude.Functor
open import Prelude.Applicative
open import Prelude.List
open import Prelude.Equality
open import Prelude.Decidable
open import Prelude.Ord
open import Prelude.Semiring

infixr 5 _∷_
data Vec {a} (A : Set a) : Nat → Set a where
  []  : Vec A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

private
  -- These are private. Use pure and _<*>_ instead.
  vec : ∀ {a} {A : Set a} {n} → A → Vec A n
  vec {n = zero } x = []
  vec {n = suc n} x = x ∷ vec x

  vapp : ∀ {a b} {A : Set a} {B : Set b} {n} → Vec (A → B) n → Vec A n → Vec B n
  vapp  []       _       = []
  vapp (f ∷ fs) (x ∷ xs) = f x ∷ vapp fs xs

  vmap : ∀ {a b} {A : Set a} {B : Set b} {n} → (A → B) → Vec A n → Vec B n
  vmap f []       = []
  vmap f (x ∷ xs) = f x ∷ vmap f xs

vecToList : ∀ {a} {A : Set a} {@erased n} → Vec A n → List A
vecToList []       = []
vecToList (x ∷ xs) = x ∷ vecToList xs

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

--- Lookup ---

indexVec : ∀ {a} {A : Set a} {n} → Vec A n → Fin n → A
indexVec (x ∷ xs) zero    = x
indexVec (x ∷ xs) (suc i) = indexVec xs i

tabulate : ∀ {a} {A : Set a} {n} → (Fin n → A) → Vec A n
tabulate {n = zero } f = []
tabulate {n = suc n} f = f zero ∷ tabulate (f ∘ suc)

--- Folding ---

vfoldr : ∀ {a b} {A : Set a} {B : Nat → Set b} → (∀ {@erased n} → A → B n → B (suc n)) → B 0 → ∀ {@erased n} → Vec A n → B n
vfoldr f z [] = z
vfoldr f z (x ∷ xs) = f x (vfoldr (λ {n} → f {n}) z xs)

vfoldl : ∀ {a b} {A : Set a} {B : Nat → Set b} → (∀ {n} → B n → A → B (suc n)) → B 0 → ∀ {@erased n} → Vec A n → B n
vfoldl         f z [] = z
vfoldl {B = B} f z (x ∷ xs) = vfoldl {B = B ∘ suc} f (f z x) xs

--- Other list functions ---

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

  infixr 5 _v++_
  _v++_ : ∀ {m n} → Vec A m → Vec A n → Vec A (m + n)
  []       v++ ys = ys
  (x ∷ xs) v++ ys = x ∷ xs v++ ys

  vreverse : ∀ {@erased n} → Vec A n → Vec A n
  vreverse xs = vfoldl {B = Vec A} (flip _∷_) [] xs

--- Equality ---

vcons-inj-head : ∀ {a} {A : Set a} {x y : A} {n}
                   {xs ys : Vec A n} → x Vec.∷ xs ≡ y ∷ ys → x ≡ y
vcons-inj-head refl = refl

vcons-inj-tail : ∀ {a} {A : Set a} {x y : A} {n}
                   {xs ys : Vec A n} → x Vec.∷ xs ≡ y ∷ ys → xs ≡ ys
vcons-inj-tail refl = refl

instance
  EqVec : ∀ {a} {A : Set a} {{EqA : Eq A}} {n} → Eq (Vec A n)
  _==_ {{EqVec}} [] []             = yes refl
  _==_ {{EqVec}} (x ∷ xs) (y ∷ ys) with x == y
  ... | no neq   = no λ eq → neq (vcons-inj-head eq)
  ... | yes eq with xs == ys
  ...   | no neq  = no λ eq₁ → neq (vcons-inj-tail eq₁)
  ...   | yes eq₁ = yes (_∷_ $≡ eq *≡ eq₁)

--- Ord ---

data LessVec {a} {A : Set a} {{OrdA : Ord A}} : ∀ {n} → Vec A n → Vec A n → Set a where
  head< : ∀ {@erased x y n} {@erased xs ys : Vec A n} → x < y → LessVec (x ∷ xs) (y ∷ ys)
  tail< : ∀ {@erased x n} {@erased xs ys : Vec A n}   → LessVec xs ys → LessVec (x ∷ xs) (x ∷ ys)

private
  compareVec : ∀ {a} {A : Set a} {{OrdA : Ord A}} {@erased n} (xs ys : Vec A n) → Comparison LessVec xs ys
  compareVec [] [] = equal refl
  compareVec (x ∷ xs) (y  ∷  ys) with compare x y
  compareVec (x ∷ xs) (y  ∷  ys) | less    x<y  = less    (head< x<y)
  compareVec (x ∷ xs) (y  ∷  ys) | greater y<x  = greater (head< y<x)
  compareVec (x ∷ xs) (.x ∷  ys) | equal   refl with compareVec xs ys
  compareVec (x ∷ xs) (.x ∷  ys) | equal   refl | less    xs<ys = less (tail< xs<ys)
  compareVec (x ∷ xs) (.x ∷  ys) | equal   refl | greater ys<xs = greater (tail< ys<xs)
  compareVec (x ∷ xs) (.x ∷ .xs) | equal   refl | equal   refl  = equal refl

private
  len : ∀ {a} {A : Set a} {n} → Vec A n → Nat
  len {n = n} _ = n

instance
  OrdVec : ∀ {a} {A : Set a} {{OrdA : Ord A}} {n} → Ord (Vec A n)
  OrdVec = defaultOrd compareVec

  OrdLawsVec : ∀ {a} {A : Set a} {{OrdA : Ord/Laws A}} {n} → Ord/Laws (Vec A n)
  Ord/Laws.super OrdLawsVec = it
  less-antirefl {{OrdLawsVec}} {[]} ()
  less-antirefl {{OrdLawsVec {A = A}}} {x ∷ xs} (head< lt) = less-antirefl {A = A} lt
  less-antirefl {{OrdLawsVec {A = A}}} {x ∷ xs} (tail< lt) = less-antirefl {A = Vec A (len xs)} {xs} lt
  less-trans {{OrdLawsVec {A = A}}} {[]} {[]} () _
  less-trans {{OrdLawsVec {A = A}}} {x ∷ xs} {y ∷ ys} {z ∷ zs} (head< lt) (head< lt₁) = head< (less-trans {A = A} lt lt₁)
  less-trans {{OrdLawsVec {A = A}}} {x ∷ xs} {y ∷ ys} {y ∷ zs} (head< lt) (tail< lt₁) = head< lt
  less-trans {{OrdLawsVec {A = A}}} {x ∷ xs} {x ∷ ys} {z ∷ zs} (tail< lt) (head< lt₁) = head< lt₁
  less-trans {{OrdLawsVec {A = A}}} {x ∷ xs} {x ∷ ys} {x ∷ zs} (tail< lt) (tail< lt₁) = tail< (less-trans {A = Vec A (len xs)} lt lt₁)

--- Functor instances ---

instance
  FunctorVec : ∀ {a n} → Functor {a} (flip Vec n)
  fmap {{FunctorVec}} = vmap

  FunctorVec′ : ∀ {a b n} → Functor′ {a} {b} (flip Vec n)
  fmap′ {{FunctorVec′}} = vmap

  ApplicativeVec : ∀ {a n} → Applicative {a} (flip Vec n)
  pure  {{ApplicativeVec}} = vec
  _<*>_ {{ApplicativeVec}} = vapp

  ApplicativeVec′ : ∀ {a b n} → Applicative′ {a} {b} (flip Vec n)
  _<*>′_ {{ApplicativeVec′}} = vapp

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
-- 2010-10-04
-- termination checker no longer counts stripping off a record constructor
-- as decrease
-- 2019-10-18
-- It does if it's an inductive non-eta record.
module Issue334b where

data Unit : Set where
  unit : Unit

record E : Set where
  inductive
  constructor mkE
  field
    fromE : E
    spam  : Unit

f : E -> Set
f (mkE e unit) = f e

f' : E -> Set
f' (mkE e u) = f e

max_stars_repo_name: strake/agda

max_issues_repo_name: strake/agda


text:
module Structure.Setoid.Size where

import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Function.Domain
open import Structure.Function
open import Syntax.Function
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ₁ ℓₑ₂ : Lvl.Level

_≍_ : (A : Setoid{ℓₑ₁}{ℓ₁}) → (B : Setoid{ℓₑ₂}{ℓ₂}) → Stmt
_≍_ A B = ∃{Obj = Setoid.Type(A) → Setoid.Type(B)} (f ↦ Function(f) ∧ Bijective(f))

_≼_ : (A : Setoid{ℓₑ₁}{ℓ₁}) → (B : Setoid{ℓₑ₂}{ℓ₂}) → Stmt
_≼_ A B = ∃{Obj = Setoid.Type(A) → Setoid.Type(B)} (f ↦ Function(f) ∧ Injective(f))

_≽_ : (A : Setoid{ℓₑ₁}{ℓ₁}) → (B : Setoid{ℓₑ₂}{ℓ₂}) → Stmt
_≽_ A B = ∃{Obj = Setoid.Type(A) → Setoid.Type(B)} (f ↦ Function(f) ∧ Surjective(f))

_≭_ : (A : Setoid{ℓₑ₁}{ℓ₁}) → (B : Setoid{ℓₑ₂}{ℓ₂}) → Stmt
_≭_ A B = ¬(A ≍ B)

_≺_ : (A : Setoid{ℓₑ₁}{ℓ₁}) → (B : Setoid{ℓₑ₂}{ℓ₂}) → Stmt
_≺_ A B = (A ≼ B) ∧ (A ≭ B)

_≻_ : (A : Setoid{ℓₑ₁}{ℓ₁}) → (B : Setoid{ℓₑ₂}{ℓ₂}) → Stmt
_≻_ A B = (A ≽ B) ∧ (A ≭ B)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Containers, based on the work of Abbott and others
------------------------------------------------------------------------

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

module Data.Container where

open import Level using (_⊔_)
open import Codata.M hiding (map)
open import Data.W
open import Size

------------------------------------------------------------------------
-- Re-exporting content to maintain backwards compatibility

open import Data.Container.Core public
open import Data.Container.Relation.Unary.Any
  using (◇) renaming (map to ◇-map) public
open import Data.Container.Relation.Unary.All
  using (□) renaming (map to □-map) public
open import Data.Container.Membership
  using (_∈_) public
open import Data.Container.Relation.Binary.Pointwise
  using () renaming (Pointwise to Eq) public
open import Data.Container.Relation.Binary.Pointwise.Properties
  using (refl; sym; trans) public
open import Data.Container.Relation.Binary.Equality.Setoid
  using (isEquivalence; setoid) public
open import Data.Container.Properties
  using () renaming (map-identity to identity; map-compose to composition) public
open import Data.Container.Related public

module Morphism where

  open import Data.Container.Morphism.Properties
    using (Natural; NT; natural; complete; id-correct; ∘-correct) public

  open import Data.Container.Morphism
    using (id; _∘_) public

-- The least and greatest fixpoints of a container.

μ : ∀ {s p} → Container s p → Set (s ⊔ p)
μ = W

ν : ∀ {s p} → Container s p → Set (s ⊔ p)
ν C = M C ∞


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

module Cubical.Foundations.Logic where

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sum as ⊎ using (_⊎_)
open import Cubical.Data.Unit
open import Cubical.Data.Sigma

open import Cubical.Foundations.Prelude as FP
open import Cubical.Functions.Embedding
open import Cubical.Functions.Fibration as Fib
open import Cubical.Foundations.Equiv

open import Cubical.HITs.PropositionalTruncation as PropTrunc

open import Cubical.Foundations.HLevels using (hProp; isPropΠ; isPropΠ2; isSetΠ; isSetHProp; isOfHLevelΣ; isPropΣ) public
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.Univalence using (ua)

open import Cubical.Relation.Nullary hiding (¬_)

infix 10 ¬_
infixr 8 _⊔_
infixr 8 _⊔′_
infixr 8 _⊓_
infixr 8 _⊓′_
infixr 6 _⇒_
infixr 4 _⇔_
infix 30 _≡ₚ_
infix 30 _≢ₚ_

infix 2 ∃[]-syntax
infix 2 ∃[∶]-syntax

infix 2 ∀[∶]-syntax
infix 2 ∀[]-syntax

infix 2 ⇒∶_⇐∶_
infix 2 ⇐∶_⇒∶_

--------------------------------------------------------------------------------
-- The type hProp of mere propositions
-- the definition hProp is given in Foundations.HLevels
-- hProp ℓ = Σ (Type ℓ) isProp

private
  variable
    ℓ ℓ' ℓ'' : Level
    P Q R : hProp ℓ
    A B C : Type ℓ

[_] : hProp ℓ → Type ℓ
[_] = fst

isProp[] : (A : hProp ℓ) → isProp [ A ]
isProp[] = snd

∥_∥ₚ : Type ℓ → hProp ℓ
∥ A ∥ₚ = ∥ A ∥ , propTruncIsProp

_≡ₚ_ : (x y : A) → hProp _
x ≡ₚ y = ∥ x ≡ y ∥ₚ

hProp≡ : [ P ] ≡ [ Q ] → P ≡ Q
hProp≡ p = Σ≡Prop (\ _ → isPropIsProp) p

--------------------------------------------------------------------------------
-- Logical implication of mere propositions

_⇒_ : (A : hProp ℓ) → (B : hProp ℓ') → hProp _
A ⇒ B = ([ A ] → [ B ]) , isPropΠ λ _ → isProp[] B

⇔toPath : [ P ⇒ Q ] → [ Q ⇒ P ] → P ≡ Q
⇔toPath {P = P} {Q = Q} P⇒Q Q⇒P = hProp≡ (isoToPath
  (iso P⇒Q Q⇒P (λ b → isProp[] Q (P⇒Q (Q⇒P b)) b) λ a → isProp[] P (Q⇒P (P⇒Q a)) a))

pathTo⇒ : P ≡ Q → [ P ⇒ Q ]
pathTo⇒ p x = subst fst  p x

pathTo⇐ : P ≡ Q → [ Q ⇒ P ]
pathTo⇐ p x = subst fst (sym p) x

substₚ : {x y : A} (B : A → hProp ℓ) → [ x ≡ₚ y ⇒ B x ⇒ B y ]
substₚ {x = x} {y = y} B = PropTrunc.elim (λ _ → isPropΠ λ _ → isProp[] (B y)) (subst (fst ∘ B))

--------------------------------------------------------------------------------
-- Mixfix notations for ⇔-toPath
-- see ⊔-identityˡ and ⊔-identityʳ for the difference

⇒∶_⇐∶_ : [ P ⇒ Q ] → [ Q ⇒ P ] → P ≡ Q
⇒∶_⇐∶_ = ⇔toPath

⇐∶_⇒∶_ : [ Q ⇒ P ] → [ P ⇒ Q ] → P ≡ Q
⇐∶ g ⇒∶ f  = ⇔toPath f g
--------------------------------------------------------------------------------
-- False and True

⊥ : hProp _
⊥ = ⊥.⊥ , λ ()

⊤ : hProp _
⊤ = Unit , (λ _ _ _ → tt)

--------------------------------------------------------------------------------
-- Pseudo-complement of mere propositions

¬_ : hProp ℓ → hProp _
¬ A = ([ A ] → ⊥.⊥) , isPropΠ λ _ → ⊥.isProp⊥

_≢ₚ_ : (x y : A) → hProp _
x ≢ₚ y = ¬ x ≡ₚ y

--------------------------------------------------------------------------------
-- Disjunction of mere propositions

_⊔′_ : Type ℓ → Type ℓ' → Type _
A ⊔′ B = ∥ A ⊎ B ∥

_⊔_ : hProp ℓ → hProp ℓ' → hProp _
P ⊔ Q = ∥ [ P ] ⊎ [ Q ] ∥ₚ

inl : A → A ⊔′ B
inl x = ∣ ⊎.inl x ∣

inr : B → A ⊔′ B
inr x = ∣ ⊎.inr x ∣

⊔-elim : (P : hProp ℓ) (Q : hProp ℓ') (R : [ P ⊔ Q ] → hProp ℓ'')
  → (∀ x → [ R (inl x) ]) → (∀ y → [ R (inr y) ]) → (∀ z → [ R z ])
⊔-elim _ _ R P⇒R Q⇒R = PropTrunc.elim (snd ∘ R) (⊎.elim P⇒R Q⇒R)

--------------------------------------------------------------------------------
-- Conjunction of mere propositions
_⊓′_ : Type ℓ → Type ℓ' → Type _
A ⊓′ B = A × B

_⊓_ : hProp ℓ → hProp ℓ' → hProp _
A ⊓ B = [ A ] ⊓′ [ B ] , isOfHLevelΣ 1 (isProp[] A) (\ _ → isProp[] B)

⊓-intro : (P : hProp ℓ) (Q : [ P ] → hProp ℓ') (R : [ P ] → hProp ℓ'')
       → (∀ a → [ Q a ]) → (∀ a → [ R a ]) → (∀ (a : [ P ]) → [ Q a ⊓ R a ] )
⊓-intro _ _ _ = \ f g a → f a , g a

--------------------------------------------------------------------------------
-- Logical bi-implication of mere propositions

_⇔_ : hProp ℓ → hProp ℓ' → hProp _
A ⇔ B = (A ⇒ B) ⊓ (B ⇒ A)

--------------------------------------------------------------------------------
-- Universal Quantifier

∀[∶]-syntax : (A → hProp ℓ) → hProp _
∀[∶]-syntax {A = A} P = (∀ x → [ P x ]) , isPropΠ (isProp[] ∘ P)

∀[]-syntax : (A → hProp ℓ) → hProp _
∀[]-syntax {A = A} P = (∀ x → [ P x ]) , isPropΠ (isProp[] ∘ P)

syntax ∀[∶]-syntax {A = A} (λ a → P) = ∀[ a ∶ A ] P
syntax ∀[]-syntax (λ a → P)          = ∀[ a ] P
--------------------------------------------------------------------------------
-- Existential Quantifier

∃[]-syntax : (A → hProp ℓ) → hProp _
∃[]-syntax {A = A} P = ∥ Σ A ([_] ∘ P) ∥ₚ

∃[∶]-syntax : (A → hProp ℓ) → hProp _
∃[∶]-syntax {A = A} P = ∥ Σ A ([_] ∘ P) ∥ₚ

syntax ∃[∶]-syntax {A = A} (λ x → P) = ∃[ x ∶ A ] P
syntax ∃[]-syntax (λ x → P) = ∃[ x ] P
--------------------------------------------------------------------------------
-- Decidable mere proposition

Decₚ : (P : hProp ℓ) → hProp ℓ
Decₚ P = Dec [ P ] , isPropDec (isProp[] P)

--------------------------------------------------------------------------------
-- Negation commutes with truncation

∥¬A∥≡¬∥A∥ : (A : Type ℓ) → ∥ (A → ⊥.⊥) ∥ₚ ≡ (¬ ∥ A ∥ₚ)
∥¬A∥≡¬∥A∥ _ =
  ⇒∶ (λ ¬A A → PropTrunc.elim (λ _ → ⊥.isProp⊥)
    (PropTrunc.elim (λ _ → isPropΠ λ _ → ⊥.isProp⊥) (λ ¬p p → ¬p p) ¬A) A)
  ⇐∶ λ ¬p → ∣ (λ p → ¬p ∣ p ∣) ∣

--------------------------------------------------------------------------------
-- (hProp, ⊔, ⊥) is a bounded ⊔-semilattice

⊔-assoc : (P : hProp ℓ) (Q : hProp ℓ') (R : hProp ℓ'')
  → P ⊔ (Q ⊔ R) ≡ (P ⊔ Q) ⊔ R
⊔-assoc P Q R =
  ⇒∶ ⊔-elim P (Q ⊔ R) (λ _ → (P ⊔ Q) ⊔ R)
    (inl ∘ inl)
    (⊔-elim Q R (λ _ → (P ⊔ Q) ⊔ R) (inl ∘ inr) inr)

  ⇐∶ assoc2
  where
    assoc2 : (A ⊔′ B) ⊔′ C → A ⊔′ (B ⊔′ C)
    assoc2 ∣ ⊎.inr a ∣              = ∣ ⊎.inr ∣ ⊎.inr a ∣ ∣
    assoc2 ∣ ⊎.inl ∣ ⊎.inr b ∣ ∣  = ∣ ⊎.inr ∣ ⊎.inl b ∣ ∣
    assoc2 ∣ ⊎.inl ∣ ⊎.inl c ∣ ∣  = ∣ ⊎.inl c ∣
    assoc2 ∣ ⊎.inl (squash x y i) ∣ = propTruncIsProp (assoc2 ∣ ⊎.inl x ∣) (assoc2 ∣ ⊎.inl y ∣) i
    assoc2 (squash x y i)             = propTruncIsProp (assoc2 x) (assoc2 y) i

⊔-idem : (P : hProp ℓ) → P ⊔ P ≡ P
⊔-idem P =
  ⇒∶ (⊔-elim P P (\ _ → P) (\ x → x) (\ x → x))
  ⇐∶ inl

⊔-comm : (P : hProp ℓ) (Q : hProp ℓ') → P ⊔ Q ≡ Q ⊔ P
⊔-comm P Q =
  ⇒∶ (⊔-elim P Q (\ _ → (Q ⊔ P)) inr inl)
  ⇐∶ (⊔-elim Q P (\ _ → (P ⊔ Q)) inr inl)

⊔-identityˡ : (P : hProp ℓ) → ⊥ ⊔ P ≡ P
⊔-identityˡ P =
  ⇒∶ (⊔-elim ⊥ P (λ _ → P) (λ ()) (λ x → x))
  ⇐∶ inr

⊔-identityʳ : (P : hProp ℓ) → P ⊔ ⊥ ≡ P
⊔-identityʳ P = ⇔toPath (⊔-elim P ⊥ (λ _ → P) (λ x → x) λ ()) inl

--------------------------------------------------------------------------------
-- (hProp, ⊓, ⊤) is a bounded ⊓-lattice

⊓-assoc : (P : hProp ℓ) (Q : hProp ℓ') (R : hProp ℓ'')
  → P ⊓ Q ⊓ R ≡ (P ⊓ Q) ⊓ R
⊓-assoc _ _ _ =
  ⇒∶ (λ {(x , (y , z)) →  (x , y) , z})
  ⇐∶ (λ {((x , y) , z) → x , (y , z) })

⊓-comm : (P : hProp ℓ) (Q : hProp ℓ') → P ⊓ Q ≡ Q ⊓ P
⊓-comm _ _ = ⇔toPath (\ p → p .snd , p .fst) (\ p → p .snd , p .fst)

⊓-idem : (P : hProp ℓ) → P ⊓ P ≡ P
⊓-idem _ = ⇔toPath fst (λ x → x , x)

⊓-identityˡ : (P : hProp ℓ) → ⊤ ⊓ P ≡ P
⊓-identityˡ _ = ⇔toPath snd λ x → tt , x

⊓-identityʳ : (P : hProp ℓ) → P ⊓ ⊤ ≡ P
⊓-identityʳ _ = ⇔toPath fst λ x → x , tt

--------------------------------------------------------------------------------
-- Distributive laws

⇒-⊓-distrib : (P : hProp ℓ) (Q : hProp ℓ')(R : hProp ℓ'')
  → P ⇒ (Q ⊓ R) ≡ (P ⇒ Q) ⊓ (P ⇒ R)
⇒-⊓-distrib _ _ _ =
  ⇒∶ (λ f → (fst ∘ f) , (snd ∘ f))
  ⇐∶ (λ { (f , g) x → f x , g x})

⊓-⊔-distribˡ : (P : hProp ℓ) (Q : hProp ℓ')(R : hProp ℓ'')
  → P ⊓ (Q ⊔ R) ≡ (P ⊓ Q) ⊔ (P ⊓ R)
⊓-⊔-distribˡ P Q R =
  ⇒∶ (λ { (x , a) → ⊔-elim Q R (λ _ → (P ⊓ Q) ⊔ (P ⊓ R))
        (λ y → ∣ ⊎.inl (x , y) ∣ )
        (λ z → ∣ ⊎.inr (x , z) ∣ ) a })

  ⇐∶ ⊔-elim (P ⊓ Q) (P ⊓ R) (λ _ → P ⊓ Q ⊔ R)
       (λ y → fst y , inl (snd y))
       (λ z → fst z , inr (snd z))

⊔-⊓-distribˡ : (P : hProp ℓ) (Q : hProp ℓ')(R : hProp ℓ'')
  → P ⊔ (Q ⊓ R) ≡ (P ⊔ Q) ⊓ (P ⊔ R)
⊔-⊓-distribˡ P Q R =
  ⇒∶ ⊔-elim P (Q ⊓ R) (λ _ → (P ⊔ Q) ⊓ (P ⊔ R) )
    (\ x → inl x , inl x) (\ p → inr (p .fst) , inr (p .snd))

  ⇐∶ (λ { (x , y) → ⊔-elim P R (λ _ → P ⊔ Q ⊓ R) inl
      (λ z → ⊔-elim P Q (λ _ → P ⊔ Q ⊓ R) inl (λ y → inr (y , z)) x) y })

⊓-∀-distrib :  (P : A → hProp ℓ) (Q : A → hProp ℓ')
  → (∀[ a ∶ A ] P a) ⊓ (∀[ a ∶ A ] Q a) ≡ (∀[ a ∶ A ] (P a ⊓ Q a))
⊓-∀-distrib P Q =
  ⇒∶ (λ {(p , q) a → p a , q a})
  ⇐∶ λ pq → (fst ∘ pq ) , (snd ∘ pq)

--------------------------------------------------------------------------------
-- Introduce the "powerset" of a type in the style of Escardó's lecture notes:
-- https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#propositionalextensionality

ℙ : ∀ {ℓ} → Type ℓ → Type (ℓ-suc ℓ)
ℙ {ℓ} X = X → hProp ℓ

infix 5 _∈_
_∈_ : {X : Type ℓ} → X → ℙ X → Type ℓ
x ∈ A = [ A x ]

_⊆_ : {X : Type ℓ} → ℙ X → ℙ X → Type ℓ
A ⊆ B = ∀ x → x ∈ A → x ∈ B

∈-isProp : {X : Type ℓ} (A : ℙ X) (x : X) → isProp (x ∈ A)
∈-isProp A = isProp[] ∘ A

⊆-isProp : {X : Type ℓ} (A B : ℙ X) → isProp (A ⊆ B)
⊆-isProp A B = isPropΠ2 (λ x _ → ∈-isProp B x)

⊆-refl : {X : Type ℓ} (A : ℙ X) → A ⊆ A
⊆-refl A x = idfun (x ∈ A)

⊆-refl-consequence : {X : Type ℓ} (A B : ℙ X)
                   → A ≡ B → (A ⊆ B) × (B ⊆ A)
⊆-refl-consequence {X} A B p = subst (λ B → (A ⊆ B)) p (⊆-refl A) , subst (λ A → (B ⊆ A)) (sym p) (⊆-refl B)

⊆-extensionality : {X : Type ℓ} (A B : ℙ X)
                 → (A ⊆ B) × (B ⊆ A) → A ≡ B
⊆-extensionality A B (φ , ψ) i x = ⇔toPath {P = (A x)} {Q = (B x)} (φ x) (ψ x) i

powersets-are-sets : {X : Type ℓ} → isSet (ℙ X)
powersets-are-sets {X = X} = isSetΠ (λ _ → isSetHProp)

⊆-extensionalityEquiv : {X : Type ℓ} (A B : ℙ X)
                      → (A ⊆ B) × (B ⊆ A) ≃ (A ≡ B)
⊆-extensionalityEquiv A B = isoToEquiv (iso (⊆-extensionality A B)
                                            (⊆-refl-consequence A B)
                                            (λ _ → powersets-are-sets A B _ _)
                                            (λ _ → isPropΣ (⊆-isProp A B) (λ _ → ⊆-isProp B A) _ _))

-- We show that the powerset is the subtype classifier
-- i.e. ℙ X ≃ Σ[A ∈ Type ℓ] (A ↪ X)
Embedding→Subset : {X : Type ℓ} → Σ[ A ∈ Type ℓ ] (A ↪ X) → ℙ X
Embedding→Subset (_ , f , isPropFiber) x = fiber f x , isPropFiber x

Subset→Embedding : {X : Type ℓ} → ℙ X → Σ[ A ∈ Type ℓ ] (A ↪ X)
Subset→Embedding {X = X} A = D , f , ψ
 where
  D = Σ[ x ∈ X ] x ∈ A

  f : D → X
  f d = d .fst

  ψ : hasPropFibers f
  ψ x ((y , y∈A) , y≡x) ((z , z∈A) , z≡x) = ΣPathP (r , q)
   where
    p : y ≡ z
    p = y≡x ∙ sym z≡x

    r : (y , y∈A) ≡ (z , z∈A)
    r = Σ≡Prop (∈-isProp A) p

    q : PathP (λ i → p i ≡ x) y≡x z≡x
    q i j = hcomp (λ k → λ { (j = i1) → x
                           ; (i = i0) → y≡x j
                           ; (i = i1) → z≡x (~ k ∨ j) })
                  (y≡x (i ∨ j))

Subset→Embedding→Subset : {X : Type ℓ} → section (Embedding→Subset {ℓ} {X}) (Subset→Embedding {ℓ} {X})
Subset→Embedding→Subset _ = funExt λ x → Σ≡Prop (λ _ → FP.isPropIsProp) (ua (Fib.FiberIso.fiberEquiv _ x))

Embedding→Subset→Embedding : {X : Type ℓ} → retract (Embedding→Subset {ℓ} {X}) (Subset→Embedding {ℓ} {X})
Embedding→Subset→Embedding {ℓ = ℓ} {X = X} (A , f , ψ) = cong (Σ-assoc-≃ .fst) p
 where
 χ = Subset→Embedding (Embedding→Subset (A , f , ψ)) .snd .snd

 p : (((Σ[ x ∈ X ] fiber f x) , fst) , χ) ≡ ((A , f) , ψ)
 p = Σ≡Prop (λ _ → hasPropFibersIsProp) ((equivToIso (Fib.fibrationEquiv X ℓ)) .Iso.leftInv (A , f))

Subset≃Embedding : {X : Type ℓ} → ℙ X ≃ (Σ[ A ∈ Type ℓ ] (A ↪ X))
Subset≃Embedding = isoToEquiv (iso Subset→Embedding Embedding→Subset Embedding→Subset→Embedding Subset→Embedding→Subset)

Subset≡Embedding : {X : Type ℓ} → ℙ X ≡ (Σ[ A ∈ Type ℓ ] (A ↪ X))
Subset≡Embedding = ua Subset≃Embedding

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
module Nat where

  import Prelude
  import Equiv
  import Datoid

  open Prelude
  open Equiv
  open Datoid

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

  one : Nat
  one = suc zero

  _+_ : Nat -> Nat -> Nat
  zero  + n = n
  suc m + n = suc (m + n)

  private
    eqNat : Nat -> Nat -> Bool
    eqNat zero    zero    = True
    eqNat (suc m) (suc n) = eqNat m n
    eqNat _       _       = False

    refl' : (x : Nat) -> T (eqNat x x)
    refl' zero    = unit
    refl' (suc n) = refl' n

    sym' : (x y : Nat) -> T (eqNat x y) -> T (eqNat y x)
    sym' zero     zero     _     = unit
    sym' (suc n1) (suc n2) eq    = sym' n1 n2 eq
    sym' (suc _)  zero     wrong = wrong
    sym' zero     (suc _)  wrong = wrong

    trans' : (x y z : Nat) -> T (eqNat x y) -> T (eqNat y z) -> T (eqNat x z)
    trans' zero     _        zero     _     _     = unit
    trans' (suc n1) (suc n2) (suc n3) eq12  eq23  = trans' n1 n2 n3 eq12 eq23
    trans' zero     (suc _)  _        wrong _     = absurdElim wrong
    trans' _        zero     (suc _)  _     wrong = absurdElim wrong
    trans' (suc _)  zero     _        wrong _     = absurdElim wrong
    trans' _        (suc _)  zero     _     wrong = absurdElim wrong

  decidableEquiv : DecidableEquiv Nat
  decidableEquiv = decEquiv (equiv (T' eqNat) refl' sym' trans')
                            (boolFunctionsDecidable eqNat)

  natDatoid : Datoid
  natDatoid = datoid Nat decidableEquiv


text:
------------------------------------------------------------------------
-- Incorrect coinductive axiomatisation of subtyping
------------------------------------------------------------------------

-- This module shows that if we remove transitivity from
-- RecursiveTypes.Subtyping.Axiomatic.Coinductive._≤_, and take the
-- transitive closure of the resulting relation, then we get a weaker
-- (less defined) relation than the one we started with.

module RecursiveTypes.Subtyping.Axiomatic.Incorrect where

open import Codata.Musical.Notation
open import Data.Fin using (Fin; zero; suc)
open import Function using (id; _$_)
open import Data.Nat
  using (ℕ; zero; suc; z≤n; s≤s; ≤′-refl) renaming (_≤_ to _≤ℕ_)
open import Data.Nat.Induction
open import Data.Nat.Properties using (≤-step; ≤⇒≤′)
open import Data.Product as Prod
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

open import RecursiveTypes.Syntax hiding (_≲_)
open import RecursiveTypes.Substitution using (_[0≔_]; unfold[μ_⟶_])
open import RecursiveTypes.Subtyping.Semantic.Coinductive as Sem
  using (_≤Coind_; ⊥; ⊤; _⟶_)

------------------------------------------------------------------------
-- The alternative "subtyping" relation

infixr 10 _⟶_
infix  4  _≤_ _≤′_
infixr 2  _≤⟨_⟩_
infix  2  _∎

-- A definition which does not include a transitivity constructor.

data _≤′_ {n} : Ty n → Ty n → Set where
  ⊥   : ∀ {τ} → ⊥ ≤′ τ
  ⊤   : ∀ {σ} → σ ≤′ ⊤
  _⟶_ : ∀ {σ₁ σ₂ τ₁ τ₂}
        (τ₁≤′σ₁ : ∞ (τ₁ ≤′ σ₁)) (σ₂≤′τ₂ : ∞ (σ₂ ≤′ τ₂)) →
        σ₁ ⟶ σ₂ ≤′ τ₁ ⟶ τ₂

  unfold : ∀ {τ₁ τ₂} → μ τ₁ ⟶ τ₂ ≤′ unfold[μ τ₁ ⟶ τ₂ ]
  fold   : ∀ {τ₁ τ₂} → unfold[μ τ₁ ⟶ τ₂ ] ≤′ μ τ₁ ⟶ τ₂

  _∎ : ∀ τ → τ ≤′ τ

-- The transitive closure of this relation.

data _≤_ {n} : Ty n → Ty n → Set where
  include : ∀ {σ τ} (σ≤τ : σ ≤′ τ) → σ ≤ τ
  _≤⟨_⟩_  : ∀ τ₁ {τ₂ τ₃} (τ₁≤τ₂ : τ₁ ≤ τ₂) (τ₂≤τ₃ : τ₂ ≤ τ₃) → τ₁ ≤ τ₃

------------------------------------------------------------------------
-- Some types used in counterexamples below

σ : Ty zero
σ = μ ⊤ ⟶ var zero

τ : Ty zero
τ = μ ⊥ ⟶ var zero

σ≤τ : σ ≤Coind τ
σ≤τ = ♯ ⊥ ⟶ ♯ σ≤τ

------------------------------------------------------------------------
-- Soundness and incompleteness of _≤′_

sound′ : ∀ {n} {σ τ : Ty n} → σ ≤′ τ → σ ≤Coind τ
sound′ ⊥               = ⊥
sound′ ⊤               = ⊤
sound′ (τ₁≤σ₁ ⟶ σ₂≤τ₂) = ♯ sound′ (♭ τ₁≤σ₁) ⟶ ♯ sound′ (♭ σ₂≤τ₂)
sound′ unfold          = Sem.unfold
sound′ fold            = Sem.fold
sound′ (τ ∎)           = Sem.refl∞ _

incomplete′ : ¬ (∀ {n} {σ τ : Ty n} → σ ≤Coind τ → σ ≤′ τ)
incomplete′ hyp with hyp {σ = σ} {τ = τ} σ≤τ
... | ()

------------------------------------------------------------------------
-- Soundness of _≤_

sound : ∀ {n} {σ τ : Ty n} → σ ≤ τ → σ ≤Coind τ
sound (τ₁ ≤⟨ τ₁≤τ₂ ⟩ τ₂≤τ₃) = Sem.trans (sound τ₁≤τ₂) (sound τ₂≤τ₃)
sound (include σ≤τ)         = sound′ σ≤τ

------------------------------------------------------------------------
-- An alternative definition of the transitive closure of _≤′_

infixr 5 _∷_
infix  4 _≲_

data _≲_ {n} : Ty n → Ty n → Set where
  [_] : ∀ {σ τ} (σ≤τ : σ ≤′ τ) → σ ≲ τ
  _∷_ : ∀ {τ₁ τ₂ τ₃} (τ₁≤τ₂ : τ₁ ≤′ τ₂) (τ₂≲τ₃ : τ₂ ≲ τ₃) → τ₁ ≲ τ₃

-- This definition is transitive.

_++_ : ∀ {n} {τ₁ τ₂ τ₃ : Ty n} → τ₁ ≲ τ₂ → τ₂ ≲ τ₃ → τ₁ ≲ τ₃
[ τ₁≤τ₂ ]       ++ τ₂≤τ₃ = τ₁≤τ₂ ∷ τ₂≤τ₃
(τ₁≤τ₂ ∷ τ₂≤τ₃) ++ τ₃≤τ₄ = τ₁≤τ₂ ∷ (τ₂≤τ₃ ++ τ₃≤τ₄)

-- Hence it is complete with respect to the one above.

≲-complete : ∀ {n} {σ τ : Ty n} → σ ≤ τ → σ ≲ τ
≲-complete (include σ≤τ)         = [ σ≤τ ]
≲-complete (τ₁ ≤⟨ τ₁≤τ₂ ⟩ τ₂≤τ₃) = ≲-complete τ₁≤τ₂ ++ ≲-complete τ₂≤τ₃

-- It is also sound.

≲-sound : ∀ {n} {σ τ : Ty n} → σ ≲ τ → σ ≤ τ
≲-sound [ σ≤τ ]         = include σ≤τ
≲-sound (τ₁≤τ₂ ∷ τ₂≲τ₃) = _ ≤⟨ include τ₁≤τ₂ ⟩ ≲-sound τ₂≲τ₃

-- The number of uses of transitivity in the proof.

length : ∀ {n} {σ τ : Ty n} → σ ≲ τ → ℕ
length [ σ≤τ ]         = 0
length (τ₁≤τ₂ ∷ τ₂≲τ₃) = suc (length τ₂≲τ₃)

------------------------------------------------------------------------
-- Given proofs of certain statements one can extract shorter or
-- equally long proofs for related statements

mutual

  codomain-⟶μ : ∀ {n} {σ₁ σ₂ : Ty n} {τ₁ τ₂} →
                (σ₁⟶σ₂≲μτ₁⟶τ₂ : σ₁ ⟶ σ₂ ≲ μ τ₁ ⟶ τ₂) →
                ∃ λ (σ₂≲τ₂′ : σ₂ ≲ τ₂ [0≔ μ τ₁ ⟶ τ₂ ]) →
                    length σ₂≲τ₂′ ≤ℕ length σ₁⟶σ₂≲μτ₁⟶τ₂
  codomain-⟶μ [ fold ]                  = ([ _ ∎ ] , z≤n)
  codomain-⟶μ (τ₁≤′σ₁ ⟶ σ₂≤′τ₂ ∷ τ₂≲τ₃) = Prod.map (_∷_ (♭ σ₂≤′τ₂)) s≤s (codomain-⟶μ τ₂≲τ₃)
  codomain-⟶μ (fold            ∷ τ₂≲τ₃) = Prod.map id ≤-step (codomain-μμ τ₂≲τ₃)
  codomain-⟶μ ((._ ∎)          ∷ τ₂≲τ₃) = Prod.map id ≤-step (codomain-⟶μ τ₂≲τ₃)
  codomain-⟶μ (⊤               ∷ τ₂≲τ₃) with sound (≲-sound τ₂≲τ₃)
  ... | ()

  codomain-μμ : ∀ {n} {σ₁ σ₂ τ₁ τ₂ : Ty (suc n)} →
                (μσ₁⟶σ₂≲μτ₁⟶τ₂ : μ σ₁ ⟶ σ₂ ≲ μ τ₁ ⟶ τ₂) →
                ∃ λ (σ₂′≲τ₂′ : σ₂ [0≔ μ σ₁ ⟶ σ₂ ] ≲ τ₂ [0≔ μ τ₁ ⟶ τ₂ ]) →
                    length σ₂′≲τ₂′ ≤ℕ length μσ₁⟶σ₂≲μτ₁⟶τ₂
  codomain-μμ [ ._ ∎ ]         = ([ _ ∎ ] , z≤n)
  codomain-μμ (unfold ∷ τ₂≲τ₃) = Prod.map id ≤-step (codomain-⟶μ τ₂≲τ₃)
  codomain-μμ ((._ ∎) ∷ τ₂≲τ₃) = Prod.map id ≤-step (codomain-μμ τ₂≲τ₃)
  codomain-μμ (⊤      ∷ τ₂≲τ₃) with sound (≲-sound τ₂≲τ₃)
  ... | ()

------------------------------------------------------------------------
-- Incompleteness of _≤_

incomplete : ¬ (∀ {n} {σ τ : Ty n} → σ ≤Coind τ → σ ≤ τ)
incomplete hyp = σ≴τ $ ≲-complete $ hyp σ≤τ
  where
  σ≴τ : ¬ σ ≲ τ
  σ≴τ σ≲τ = <′-rec Pred ≴ _ σ≲τ refl
    where
    Pred : ℕ → Set
    Pred n = (σ≲τ : σ ≲ τ) → length σ≲τ ≢ n

    ≴ : ∀ n → <′-Rec Pred n → Pred n
    ≴ n  rec [ () ]           _
    ≴ ._ rec ((._ ∎) ∷ τ₂≲τ₃) refl = rec _ ≤′-refl τ₂≲τ₃ refl
    ≴ ._ rec (unfold ∷ τ₂≲τ₃) refl with codomain-⟶μ τ₂≲τ₃
    ... | (τ₂≲τ₃′ , not-longer) = rec _ (≤⇒≤′ $ s≤s not-longer) τ₂≲τ₃′ refl
    ≴ n  rec (⊤      ∷ τ₂≲τ₃) _    with sound (≲-sound τ₂≲τ₃)
    ... | ()

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
open import Mockingbird.Forest using (Forest)

module Mockingbird.Forest.Combination.Vec.Properties {b ℓ} (forest : Forest {b} {ℓ}) where

open import Data.Vec as Vec using (Vec; []; _∷_; _++_)
import Data.Vec.Relation.Unary.Any as Any
open import Data.Vec.Relation.Unary.Any.Properties as Anyₚ using (++⁺ˡ; ++⁺ʳ)
open import Function using (_$_; flip)
open import Relation.Unary using (Pred; _∈_; _⊆_; ∅)

open Forest forest

open import Mockingbird.Forest.Combination.Vec.Base forest
import Mockingbird.Forest.Combination.Properties forest as Combinationₚ

subst : ∀ {n x y} {bs : Vec Bird n} → x ≈ y → x ∈ ⟨ bs ⟩ → y ∈ ⟨ bs ⟩
subst = Combinationₚ.subst λ x≈y → Any.map (trans (sym x≈y))

subst′ : ∀ {n x y} {bs : Vec Bird n} → y ≈ x → x ∈ ⟨ bs ⟩ → y ∈ ⟨ bs ⟩
subst′ y≈x = subst (sym y≈x)

⟨[]⟩ : ⟨ [] ⟩ ⊆ ∅
⟨[]⟩ (X ⟨∙⟩ Y ∣ xy≈z) = ⟨[]⟩ X

weaken-∷ : ∀ {n x y} {bs : Vec Bird n} → x ∈ ⟨ bs ⟩ → x ∈ ⟨ y ∷ bs ⟩
weaken-∷ = Combinationₚ.weaken there

-- TODO: maybe call this ++⁺ˡ.
weaken-++ˡ : ∀ {m n x} {bs : Vec Bird m} {bs′ : Vec Bird n} → x ∈ ⟨ bs ⟩ → x ∈ ⟨ bs ++ bs′ ⟩
weaken-++ˡ {bs = bs} {bs′} [ x∈bs ] = [ ++⁺ˡ x∈bs ]
weaken-++ˡ {bs = bs} {bs′} (x∈⟨bs⟩ ⟨∙⟩ y∈⟨bs⟩ ∣ xy≈z) = weaken-++ˡ x∈⟨bs⟩ ⟨∙⟩ weaken-++ˡ y∈⟨bs⟩ ∣ xy≈z

-- TODO: maybe call this ++⁺ʳ.
weaken-++ʳ : ∀ {m n x} (bs : Vec Bird m) {bs′ : Vec Bird n} → x ∈ ⟨ bs′ ⟩ → x ∈ ⟨ bs ++ bs′ ⟩
weaken-++ʳ bs {bs′} [ x∈bs′ ] = [ ++⁺ʳ bs x∈bs′ ]
weaken-++ʳ bs {bs′} (x∈⟨bs′⟩ ⟨∙⟩ y∈⟨bs′⟩ ∣ xy≈z) = weaken-++ʳ bs x∈⟨bs′⟩ ⟨∙⟩ weaken-++ʳ bs y∈⟨bs′⟩ ∣ xy≈z

++-comm : ∀ {m n x} (bs : Vec Bird m) (bs′ : Vec Bird n) → x ∈ ⟨ bs ++ bs′ ⟩ → x ∈ ⟨ bs′ ++ bs ⟩
++-comm bs bs′ [ x∈bs++bs′ ] = [ Anyₚ.++-comm bs bs′ x∈bs++bs′ ]
++-comm bs bs′ (x∈⟨bs++bs′⟩ ⟨∙⟩ y∈⟨bs++bs′⟩ ∣ xy≈z) = ++-comm bs bs′ x∈⟨bs++bs′⟩ ⟨∙⟩ ++-comm bs bs′ y∈⟨bs++bs′⟩ ∣ xy≈z

open import Mockingbird.Forest.Birds forest
open import Mockingbird.Forest.Extensionality forest
module _ ⦃ _ : Extensional ⦄ ⦃ _ : HasCardinal ⦄ ⦃ _ : HasIdentity ⦄
         ⦃ _ : HasThrush ⦄ ⦃ _ : HasKestrel ⦄ ⦃ _ : HasStarling ⦄ where
  private
    CI≈T : C ∙ I ≈ T
    CI≈T = ext $ λ x → ext $ λ y → begin
      C ∙ I ∙ x ∙ y  ≈⟨ isCardinal I x y ⟩
      I ∙ y ∙ x      ≈⟨ congʳ $ isIdentity y ⟩
      y ∙ x          ≈˘⟨ isThrush x y ⟩
      T ∙ x ∙ y      ∎

  _ : T ∈  ⟨ C ∷ I ∷ [] ⟩
  _ = subst CI≈T $ [# 0 ] ⟨∙⟩ [# 1 ]

  _ : I ∈ ⟨ S ∷ K ∷ [] ⟩
  _ = flip subst ([# 0 ] ⟨∙⟩ [# 1 ] ⟨∙⟩ [# 1 ]) $ ext $ λ x → begin
    S ∙ K ∙ K ∙ x    ≈⟨ isStarling K K x ⟩
    K ∙ x ∙ (K ∙ x)  ≈⟨ isKestrel x (K ∙ x) ⟩
    x                ≈˘⟨ isIdentity x ⟩
    I ∙ x            ∎

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
{-# OPTIONS --postfix-projections #-}

open import Agda.Builtin.Nat

record R : Set where
  field
    x : Nat → Nat

open R {{...}}

f : R
f .x = {!!}

-- WAS: Case splitting on result produces the following nonsense:
-- f ⦃ .x ⦄ x₁ = ?

-- SHOULD: produce
-- f .x x₁ = ?