text:
------------------------------------------------------------------------------
-- Arithmetic properties using instances of the induction principle
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Nat.Induction.Instances.PropertiesATP where

open import FOTC.Base
open import FOTC.Data.Nat

------------------------------------------------------------------------------
-- Totality properties

N→0∨S-ind-instance :
  zero ≡ zero ∨ (∃[ n' ] zero ≡ succ₁ n' ∧ N n') →
  (∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ N n') →
    succ₁ n ≡ zero ∨ (∃[ n' ] succ₁ n ≡ succ₁ n' ∧ N n')) →
  ∀ {n} → N n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ N n')
N→0∨S-ind-instance = N-ind (λ i → i ≡ zero ∨ (∃[ i' ] i ≡ succ₁ i' ∧ N i'))

postulate N→0∨S : ∀ {n} → N n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ N n')
{-# ATP prove N→0∨S N→0∨S-ind-instance #-}

pred-N-ind-instance :
  N (pred₁ zero) →
  (∀ {n} → N (pred₁ n) → N (pred₁ (succ₁ n))) →
  ∀ {n} → N n → N (pred₁ n)
pred-N-ind-instance = N-ind (λ i → N (pred₁ i))

-- 2018-06-28. The ATPs could not prove this conjecture (300 sec).
-- postulate pred-N' : ∀ {n} → N n → N (pred₁ n)
-- {-# ATP prove pred-N' pred-N-ind-instance #-}

postulate pred-N : ∀ {n} → N n → N (pred₁ n)
{-# ATP prove pred-N pred-N-ind-instance N→0∨S #-}

+-N-ind-instance :
  ∀ {n} →
  N (zero + n) →
  (∀ {m} → N (m + n) → N (succ₁ m + n)) →
  ∀ {m} → N m → N (m + n)
+-N-ind-instance {n} = N-ind (λ i → N (i + n))

postulate +-N : ∀ {m n} → N m → N n → N (m + n)
{-# ATP prove +-N +-N-ind-instance #-}

∸-N-ind-instance :
  ∀ {m} →
  N (m ∸ zero) →
  (∀ {n} → N (m ∸ n) → N (m ∸ succ₁ n)) →
  ∀ {n} → N n → N (m ∸ n)
∸-N-ind-instance {n} = N-ind (λ i → N (n ∸ i))

postulate ∸-N : ∀ {m n} → N m → N n → N (m ∸ n)
{-# ATP prove ∸-N ∸-N-ind-instance pred-N #-}

*-N-ind-instance :
  ∀ {n} →
  N (zero * n) →
  (∀ {m} → N (m * n) → N (succ₁ m * n)) →
  ∀ {m} → N m → N (m * n)
*-N-ind-instance {n} = N-ind (λ i → N (i * n))

postulate *-N : ∀ {m n} → N m → N n → N (m * n)
{-# ATP prove *-N *-N-ind-instance +-N #-}

+-rightIdentity-ind-instance :
  zero + zero ≡ zero →
  (∀ {n} → n + zero ≡ n → succ₁ n + zero ≡ succ₁ n) →
  ∀ {n} → N n → n + zero ≡ n
+-rightIdentity-ind-instance = N-ind (λ i → i + zero ≡ i)

postulate +-rightIdentity : ∀ {n} → N n → n + zero ≡ n
{-# ATP prove +-rightIdentity +-rightIdentity-ind-instance #-}

+-assoc-ind-instance :
  ∀ {n} {o} →
  zero + n + o ≡ zero + (n + o) →
  (∀ {m} → m + n + o ≡ m + (n + o) → succ₁ m + n + o ≡ succ₁ m + (n + o)) →
  ∀ {m} → N m → m + n + o ≡ m + (n + o)
+-assoc-ind-instance {n} {o} = N-ind (λ i → i + n + o ≡ i + (n + o))

postulate +-assoc : ∀ {m} → N m → ∀ n o → m + n + o ≡ m + (n + o)
{-# ATP prove +-assoc +-assoc-ind-instance #-}

x+Sy≡S[x+y]-ind-instance :
  ∀ {n} →
  zero + succ₁ n ≡ succ₁ (zero + n) →
  (∀ {m} →
    m + succ₁ n ≡ succ₁ (m + n) → succ₁ m + succ₁ n ≡ succ₁ (succ₁ m + n)) →
  ∀ {m} → N m → m + succ₁ n ≡ succ₁ (m + n)
x+Sy≡S[x+y]-ind-instance {n} = N-ind (λ i → i + succ₁ n ≡ succ₁ (i + n))

postulate x+Sy≡S[x+y] : ∀ {m} → N m → ∀ n → m + succ₁ n ≡ succ₁ (m + n)
{-# ATP prove x+Sy≡S[x+y] x+Sy≡S[x+y]-ind-instance #-}

+-comm-ind-instance :
  ∀ {n} →
  zero + n ≡ n + zero →
  (∀ {m} → m + n ≡ n + m → succ₁ m + n ≡ n + succ₁ m) →
  ∀ {m} → N m → m + n ≡ n + m
+-comm-ind-instance {n} = N-ind (λ i → i + n ≡ n + i)

postulate +-comm : ∀ {m n} → N m → N n → m + n ≡ n + m
{-# ATP prove +-comm +-comm-ind-instance +-rightIdentity x+Sy≡S[x+y] #-}

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import LogicalFormulae
open import Numbers.Integers.Integers
open import Numbers.Integers.Definition
open import Lists.Lists
open import Maybe

module Groups.Polynomials.Examples where

open import Groups.Polynomials.Definition ℤGroup

private
  decide : _
  decide = (λ a → ℤDecideEquality a (nonneg 0))

  p1 : degree decide [] ≡ no
  p1 = refl

  p2 : degree decide (nonneg 0 :: []) ≡ no
  p2 = refl

  p3 : degree decide (nonneg 1 :: []) ≡ yes 0
  p3 = refl


text:
Id : {A B : Set} → (A → B) → A → B
Id F = F

syntax Id (λ X → B) = ƛ X ⟶ B

postulate
  A : Set
  a : A

example₁ : A → A
example₁ = ƛ x ⟶ x

example₂ : A → A
example₂ = ƛ !_ ⟶ !_

example₃ : A → A
example₃ = ƛ !_ ⟶ (!_)

example₄ : (A → A) → A
example₄ = ƛ !_ ⟶ ! a

example₅ : (A → A) → A
example₅ = ƛ !_ ⟶ (! a)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- {-# OPTIONS -v tc.meta:30 #-}
{-# OPTIONS --show-implicit --show-irrelevant #-}
module Issue629 where

infixr 4 _,_
infixr 2 _×_

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

const : {A : Set₁} {B : Set} → A → (B → A)
const a = λ b → a

_×_ : Set → Set → Set
A × B = Σ A (const B)

uncurry : {A : Set} {B : A → Set} {C : Σ A B → Set} →
          ((x : A) (y : B x) → C (x , y)) →
          ((p : Σ A B) → C p)
uncurry f (x , y) = f x y

flip : {A B : Set} {C : A → B → Set} →
       ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ x y → f y x

assoc : {A B C : Set} → (A × B) × C → A × (B × C)
assoc {A}{B}{C} = uncurry (flip λ z → uncurry λ x y → (x , (y , z)))

-- The code above is accepted if const is inlined in the definition of
-- _×_.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2016-07-20, issue #2100 termination and where

data D : Set where
  pair : (x y : D) → D

works : (p q : D) → D
works (pair a b) (pair c d) = pair
  (works a (pair c d))
  (works (pair a b) c)

-- If we abstract out the two calls with where
-- termination check fails.

fails : (p q : D) → D
fails (pair a b) (pair c d) = pair u v
  where
  u = (fails a (pair c d))
  v = (fails (pair a b) c)

-- Would be nice if this succeeded.
-- (Ideally before the year 2100.)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This file contains some core definitions which are re-exported by
-- Data.List.Relation.Binary.Sublist.Heterogeneous.
------------------------------------------------------------------------

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

open import Relation.Binary using (REL)

module Data.List.Relation.Binary.Sublist.Heterogeneous.Core
       {a b r} {A : Set a} {B : Set b} (R : REL A B r)
       where

open import Level using (_⊔_)
open import Data.List.Base using (List; []; _∷_; [_])

data Sublist : REL (List A) (List B) (a ⊔ b ⊔ r) where
  []   : Sublist [] []
  _∷ʳ_ : ∀ {xs ys} → ∀ y → Sublist xs ys → Sublist xs (y ∷ ys)
  _∷_  : ∀ {x xs y ys} → R x y → Sublist xs ys → Sublist (x ∷ xs) (y ∷ ys)


text:
-- Currently pragmas are not allowed in mutual blocks.
-- This might change.
module PragmaInMutual where

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

mutual
  {-# BUILTIN NATURAL Nat #-}
  T : Set -> Set
  T A = A


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

open import LogicalFormulae
open import Orders.WellFounded.Definition
open import Orders.WellFounded.Induction
open import Orders.Partial.Definition
open import Orders.Total.Definition
open import Functions
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Ordinals where

record Ordinal {a b : _} : Set (lsuc a ⊔ lsuc b) where
  field
    A : Set a
    _<_ : Rel {a} {b} A
    wf : WellFounded _<_

succSet : {a b : _} → (o : Ordinal {a} {b}) → Set a
succSet o = True || Ordinal.A o

succComp : {a b : _} → (o : Ordinal {a} {b}) → Rel (succSet o)
succComp o (inl record {}) y = False'
succComp o (inr x) (inl record {}) = True'
succComp o (inr x) (inr y) = Ordinal._<_ o x y

private
  lemma' : {a b : _} → {o : Ordinal {a} {b}} → (x : Ordinal.A o) → Accessible (Ordinal._<_ o) x → Accessible (succComp o) (inr x)
  lemma' {o = o} = rec (Ordinal.wf o) _ ans
    where
      open Ordinal o
      ans : (x : A) → ((y : A) → y < x → Accessible _<_ y → Accessible (succComp o) (inr y)) → Accessible _<_ x → Accessible (succComp o) (inr x)
      ans x induction (access f) = access u
        where
          u : (y : succSet o) → succComp o y (inr x) → Accessible (succComp o) y
          u (inr y) y<x = induction y y<x (f y y<x)

  lemma : {a b : _} → {o : Ordinal {a} {b}} → (x : Ordinal.A o) → Accessible (succComp o) (inr x)
  lemma {o = o} x with Ordinal.wf o x
  ... | access f = access t
    where
      t : (y : succSet o) → succComp o y (inr x) → Accessible (succComp o) y
      t (inr y) y<x with f y y<x
      ... | u = lemma' _ u

succWf : {a b : _} → (o : Ordinal {a} {b}) → WellFounded (succComp o)
succWf o (inl record {}) = access t
  where
    t : (y : succSet o) → succComp o y (inl (record {})) → Accessible (succComp o) y
    t (inr x) record {} = lemma x
succWf o (inr x) = access t
  where
    t : (y : succSet o) → succComp o y (inr x) → Accessible (succComp o) y
    t (inr y) y<x = lemma y

succ : {a b : _} → Ordinal {a} {b} → Ordinal
succ o = record { A = succSet o ; _<_ = succComp o ; wf = succWf o }

OrdinalIsomorphism : {a b c d : _} {o1 : Ordinal {a} {b}} {o2 : Ordinal {c} {d}} → {f : Ordinal.A o1 → Ordinal.A o2} → Bijection f → Set (a ⊔ b ⊔ d)
OrdinalIsomorphism {o1 = o1} {o2 = o2} {f = f} bij = (x y : Ordinal.A o1) → Ordinal._<_ o1 x y → Ordinal._<_ o2 (f x) (f y)

wellOrderIsTotal : {a b : _} {A : Set a} {_<_ : Rel {a} {b} A} → WellFounded _<_ → TotalOrder A {b}
PartialOrder._<_ (TotalOrder.order (wellOrderIsTotal {_<_ = _<_} wf)) = _<_
PartialOrder.irreflexive (TotalOrder.order (wellOrderIsTotal {A = A} {_<_ = _<_} wf)) {x} = ans x
  where
    ans : (x : A) → ((x < x) → False)
    ans = rec wf (λ z → (x : z < z) → False) λ i pr i<i → pr i i<i i<i
PartialOrder.<Transitive (TotalOrder.order (wellOrderIsTotal {A = A} {_<_ = _<_} wf)) {a} {b} {c} = ans b
  where
    pr : (x : A) → ((y : A) → y < x → a < y → y < c → a < c) → a < x → x < c → a < c
    pr x induction a<x x<c with wf x
    ... | access xAc = induction {!!} {!!} {!!} {!!}
    ans : (b : A) → (a < b) → (b < c) → a < c
    ans = rec wf _ pr
TotalOrder.totality (wellOrderIsTotal {A = A} {_<_ = _<_} wf) a b = {!!}
  where
    pr : (x : A) → ((y : A) → y < x → ((y < b) || (b < y)) || (y ≡ b)) → ((x < b) || (b < x)) || (x ≡ b)
    pr x induction with wf x
    pr x induction | access x₁ = {!!}
    ans : (a : A) → ((a < b) || (b < a)) || (a ≡ b)
    ans = rec wf _ pr

record OrdinalsIsomorphic {a b c d : _} (o1 : Ordinal {a} {b}) (o2 : Ordinal {c} {d}) : Set (a ⊔ b ⊔ c ⊔ d) where
  field
    f : Ordinal.A o1 → Ordinal.A o2
    bij : Bijection f
    isIso : OrdinalIsomorphism {o1 = o1} {o2 = o2} {f = f} bij

isoImpliesUniqueIso : {a b c d : _} {o1 : Ordinal {a} {b}} {o2 : Ordinal {c} {d}} → (iso1 iso2 : OrdinalsIsomorphic o1 o2) → (x : Ordinal.A o1) → OrdinalsIsomorphic.f iso1 x ≡ OrdinalsIsomorphic.f iso2 x
isoImpliesUniqueIso {o1 = o1} record { f = f1 ; bij = bij1 ; isIso = isIso1 } record { f = f2 ; bij = bij2 ; isIso = isIso2 } = rec (Ordinal.wf o1) _ ans
  where
    ans : (x : Ordinal.A o1) → ((y : Ordinal.A o1) → (Ordinal._<_ o1) y x → f1 y ≡ f2 y) → f1 x ≡ f2 x
    ans x induction = {!!}

succNotIsomorphic : {a b : _} → (o : Ordinal {a} {b}) → OrdinalsIsomorphic o (succ o) → False
succNotIsomorphic o record { f = f ; bij = bij ; isIso = isIso } = {!!}


text:
{-# OPTIONS --sized-types #-}
-- {-# OPTIONS -v term:10 #-}
module BoundedSizeNoMatch where

open import Common.Size
open import Common.Equality

T : Size → Set
T i = (j : Size< i) → T j
-- this should not termination check, otherwise
-- eta expansion can loop

-- loops : (i j : Size) → T i ≡ T j
-- loops i j = refl

max_stars_repo_name: masondesu/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module vector-sort where

open import level
open import bool
open import nat
open import product
open import vector

insert𝕍 : ∀{ℓ}{A : Set ℓ}{n : ℕ} → (_<_ : A → A → 𝔹) → (_≅_ : A → A → 𝔹) → A → 𝕍 A n → Σi ℕ (λ m → 𝕍 A (suc m))
insert𝕍 _<_ _≅_ x [] = , [ x ]𝕍
insert𝕍 _<_ _≅_ x (y :: ys) with x < y
... | tt = , x :: y :: ys
... | ff with x ≅ y
... | tt = , y :: ys
... | ff with (insert𝕍 _<_ _≅_ x ys)
... | , r = , y :: r

insertion-sort𝕍 : ∀{ℓ}{A : Set ℓ}{n : ℕ} → (_<_ : A → A → 𝔹) → (_≅_ : A → A → 𝔹) → 𝕍 A (suc n) → Σi ℕ (λ m → 𝕍 A (suc m))
insertion-sort𝕍 _ _ (x :: []) = , [ x ]𝕍
insertion-sort𝕍 _<_ _≅_ (x :: (y :: ys)) with insertion-sort𝕍 _<_ _≅_ (y :: ys)
... | , (z :: zs) = insert𝕍 _<_ _≅_ x (z :: zs)

test-insertion-sort𝕍 = insertion-sort𝕍 _<_ _=ℕ_ (3 :: 5 :: 2 :: 7 :: 1 :: 2 :: 3 :: 9 :: [])

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
open import Relation.Binary.Core

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

open import Data.Sum
open import Induction.WellFounded
open import PLRTree {A}
open import PLRTree.Compound {A}
open import PLRTree.Order {A}
open import PLRTree.Order.Properties {A}
open import Relation.Binary.PropositionalEquality

last : (t : PLRTree) → Compound t → A
last (node perfect x _ r) compound
    with r
... | leaf = x
... | node t' y' l' r' =  last (node t' y' l' r') compound
last (node left x l _) compound
    with l
... | leaf = x
... | node t' y' l' r' =  last (node t' y' l' r') compound
last (node right x l r) compound
    with l | r
... | leaf | _ = x
... | node _ y' _ _ | leaf =  y'
... | node t' y' l' r' | node perfect _ _ _ = last (node t' y' l' r') compound
... | _ | node t' y' l' r' = last (node t' y' l' r') compound

dropLast : PLRTree → PLRTree
dropLast leaf = leaf
dropLast (node perfect x l r)
    with r
... | leaf = leaf
... | node _ _ _ _ = node right x l (dropLast r)
dropLast (node left x l r)
    with l | dropLast l
... | leaf | _ = leaf
... | node _ _ _ _ | node perfect y' l' r' = node perfect x (node perfect y' l' r') r
... | node _ _ _ _ | t = node left x t r
dropLast (node right x l r)
    with r
... | leaf = node perfect x leaf leaf
... | node perfect y' l' r' = node left x (dropLast l) (node perfect y' l' r')
... | node _ _ _ _ = node right x l (dropLast r)

push : (t : PLRTree) → Acc _≺_ t → PLRTree
push leaf _ = leaf
push (node t x  leaf _) _ = node t x leaf leaf
push (node t x (node t' x' _ _) leaf) _
    with tot≤ x x'
... | inj₁ x≤x' = node t x (node t' x' leaf leaf) leaf
... | inj₂ x'≤x = node t x' (node t' x leaf leaf) leaf
push (node t x (node t' x' l' r') (node t'' x'' l'' r'')) (acc rs)
    with tot≤ x x' | tot≤ x x'' | tot≤ x' x''
... | inj₁ x≤x' | inj₁ x≤x'' | _ = node t x (node t' x' l' r') (node t'' x'' l'' r'')
... | inj₁ x≤x' | inj₂ x''≤x | _ rewrite lemma-≡-height t'' x x'' l'' r'' =
           let acc-t''xl''r'' = rs (node t'' x l'' r'') (lemma-≺-right t x (node t' x' l' r') (node t'' x'' l'' r''))
           in node t x'' (node t' x' l' r') (push (node t'' x l'' r'') acc-t''xl''r'')
... | inj₂ x'≤x | inj₁ x≤x'' | _ rewrite lemma-≡-height t' x x' l' r' =
           let acc-t'xl'r' = rs (node t' x l' r') (lemma-≺-left t x (node t' x' l' r') (node t'' x'' l'' r''))
           in node t x' (push (node t' x l' r') acc-t'xl'r') (node t'' x'' l'' r'')
... | inj₂ x'≤x | inj₂ x''≤x | inj₁ x'≤x'' rewrite lemma-≡-height t' x x' l' r' =
           let acc-t'xl'r' = rs (node t' x l' r') (lemma-≺-left t x (node t' x' l' r') (node t'' x'' l'' r''))
           in node t x' (push (node t' x l' r') acc-t'xl'r') (node t'' x'' l'' r'')
... | inj₂ x'≤x | inj₂ x''≤x | inj₂ x''≤x' rewrite lemma-≡-height t'' x x'' l'' r'' =
           let acc-t''xl''r'' = rs (node t'' x l'' r'') (lemma-≺-right t x (node t' x' l' r') (node t'' x'' l'' r''))
           in node t x'' (node t' x' l' r') (push (node t'' x l'' r'') acc-t''xl''r'')

setRoot : A → PLRTree → PLRTree
setRoot _ leaf = leaf
setRoot x (node t _ l r) = node t x l r

drop : PLRTree → PLRTree
drop leaf = leaf
drop (node _ _ leaf leaf) = leaf
drop (node t x l r) = push (setRoot z t') (≺-wf (setRoot z t'))
           where z = last (node t x l r) compound ;
                      t' = dropLast (node t x l r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bounded vectors
------------------------------------------------------------------------

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

module Data.Vec.Bounded where

open import Level using (Level)
open import Data.Nat.Base
open import Data.Vec as Vec using (Vec)
open import Function
open import Relation.Binary using (_Preserves_⟶_)
open import Relation.Unary using (Pred; Decidable)

private
  variable
    a p : Level
    A : Set a

------------------------------------------------------------------------
-- Publicly re-export the contents of the base module

open import Data.Vec.Bounded.Base public

------------------------------------------------------------------------
-- Additional operations

lift : ∀ {f} → f Preserves _≤_ ⟶ _≤_ →
       (∀ {n} → Vec A n  → Vec≤ A (f n)) →
       ∀ {n} →  Vec≤ A n → Vec≤ A (f n)
lift incr f (as , p) = ≤-cast (incr p) (f as)

lift′ : (∀ {n} → Vec A n  → Vec≤ A n) →
        (∀ {n} → Vec≤ A n → Vec≤ A n)
lift′ = lift id

------------------------------------------------------------------------
-- Additional operations

module _ {P : Pred A p} (P? : Decidable P) where

  filter : ∀ {n} → Vec≤ A n → Vec≤ A n
  filter = lift′ (Vec.filter P?)

  takeWhile : ∀ {n} → Vec≤ A n → Vec≤ A n
  takeWhile = lift′ (Vec.takeWhile P?)

  dropWhile : ∀ {n} → Vec≤ A n → Vec≤ A n
  dropWhile = lift′ (Vec.dropWhile P?)


text:
{-# OPTIONS --experimental-irrelevance #-}
module ExplicitLambdaExperimentalIrrelevance where

postulate
  A : Set
  T : ..(x : A) -> Set  -- shape irrelevant type

test : .(a : A) -> T a -> Set
test a = λ (x : T a) -> A
-- this should type check and not complain about irrelevance of a

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.
   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output
open import Optics.All
open import Util.KVMap                           as Map
open import Util.PKCS
open import Util.Prelude

module LibraBFT.Impl.Consensus.EpochManagerTypes where

------------------------------------------------------------------------------
-- in Haskell, this lives in LBFT.Consensus.Types
-- It lives here because of the dependency on RoundManager.

data RoundProcessor : Set where
  RoundProcessorRecovery : RecoveryManager → RoundProcessor
  RoundProcessorNormal   : RoundManager    → RoundProcessor

record EpochManager : Set where
  constructor mkEpochManager
  field
    _emAuthor             : Author
    _emConfig             : ConsensusConfig
    _emStateComputer      : StateComputer
    _emStorage            : PersistentLivenessStorage
    _emSafetyRulesManager : SafetyRulesManager
    _emProcessor          : Maybe RoundProcessor
open EpochManager public
unquoteDecl emAuthor   emConfig   emStateComputer   emStorage   emSafetyRulesManager   emProcessor = mkLens (quote EpochManager)
           (emAuthor ∷ emConfig ∷ emStateComputer ∷ emStorage ∷ emSafetyRulesManager ∷ emProcessor ∷ [])

-- getter only in Haskell
emEpochState : Lens EpochManager (Either ErrLog EpochState)
emEpochState = mkLens' g s
 where
  g : EpochManager → Either ErrLog EpochState
  g em = case em ^∙ emProcessor of λ where
           (just (RoundProcessorNormal   p)) → pure (p ^∙ rmEpochState)
           (just (RoundProcessorRecovery p)) → pure (p ^∙ rcmEpochState)
           nothing                           → Left fakeErr
  s : EpochManager → Either ErrLog EpochState → EpochManager
  s em _ = em

-- getter only in Haskell
emEpoch : Lens EpochManager (Either ErrLog Epoch)
emEpoch = mkLens' g s
 where
  g : EpochManager → Either ErrLog Epoch
  g em = (_^∙ esEpoch) <$> (em ^∙ emEpochState)
  s : EpochManager → Either ErrLog Epoch → EpochManager
  s em _ = em

-- getter only in Haskell
emObmRoundManager : Lens EpochManager (Either ErrLog RoundManager)
emObmRoundManager = mkLens' g s
 where
  g : EpochManager → Either ErrLog RoundManager
  g em = case em ^∙ emProcessor of λ where
           (just (RoundProcessorNormal rm))  → pure rm
           (just (RoundProcessorRecovery _)) → Left fakeErr
           nothing                           → Left fakeErr
  s : EpochManager → Either ErrLog RoundManager -> EpochManager
  s em _ = em


text:
module BoehmBerarducci where

open import Data.Nat
open import Data.List

NatQ : Set₁
NatQ = {A : Set} -> (A -> A) -> A -> A

unNatQ : {A : Set} -> (A -> A) -> A -> NatQ -> A
unNatQ f a q = q f a

succQ : NatQ -> NatQ
succQ q = \f a -> f (q f a)

zeroQ : NatQ
zeroQ = \f a -> a

fromNatQ : NatQ -> ℕ
fromNatQ q = unNatQ suc zero q

toNatQ : ℕ -> NatQ
toNatQ (suc n) = succQ (toNatQ n)
toNatQ zero    = zeroQ

ListQ : Set -> Set₁
ListQ A = {B : Set} -> (A -> B -> B) -> B -> B

unListQ : {A B : Set} -> (A -> B -> B) -> B -> ListQ A -> B
unListQ f b q = q f b

consQ : {A : Set} -> A -> ListQ A -> ListQ A
consQ a q = \f b -> f a (q f b)

nilQ : {A : Set} -> ListQ A
nilQ = \f b -> b

fromListQ : {A : Set} -> ListQ A -> List A
fromListQ q = unListQ (_∷_) [] q

toListQ : {A : Set} -> List A -> ListQ A
toListQ (a ∷ aa) = consQ a (toListQ aa)
toListQ []       = nilQ

max_stars_repo_name: mietek/scott-encoding

max_issues_repo_name: mietek/scott-encoding

max_forks_repo_name: mietek/scott-encoding


text:
{-
   Checking that nesting invertible functions works properly. In this example
   we should get

    El2 α = B         {reduces to}
    El1 (embed α) = B {simplifies by invertibility to}
    embed α = b       {simplifies by invertibility to}
    α = b
-}
module NestedInj where

data A : Set where
  theA : A

data B : Set where
  theB : B

data U1 : Set where
  a : U1
  b : U1

data U2 : Set where
  b : U2

El1 : U1 -> Set
El1 a = A
El1 b = B

embed : U2 -> U1
embed b = b

El2 : U2 -> Set
El2 c = El1 (embed c)

f1 : {c : U1} -> El1 c -> El1 c
f1 {a} theA = theA
f1 {b} theB = theB

f2 : {c : U2} -> El2 c -> El2 c
f2 x = f1 x

test : B
test = f2 theB


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

module Categories.Adjoint.TwoSided.Compose where

open import Level

open import Categories.Adjoint
open import Categories.Adjoint.TwoSided
open import Categories.Category.Core using (Category)
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Properties
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism as ≃ using (_≃_; NaturalIsomorphism)
open import Categories.NaturalTransformation.NaturalIsomorphism.Properties
import Categories.Morphism.Reasoning as MR

open import Relation.Binary using (Setoid; IsEquivalence)

private
  variable
    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ : Level

_∘⊣⊢_ : {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {E : Category o″ ℓ″ e″}
        {L : Functor C D} {R : Functor D C} {L′ : Functor D E} {R′ : Functor E D}
        (L⊣⊢R : L ⊣⊢ R) (L′⊣⊢R′ : L′ ⊣⊢ R′) → (L′ ∘F L) ⊣⊢ (R ∘F R′)
_∘⊣⊢_ {C = C} {D} {E} {L} {R} {L′} {R′} L⊣⊢R L′⊣⊢R′ = withZig record
  { unit   = unit
  ; counit = counit
  ; zig    = zig
  }
  where
  private
    module C   = Category C using (_∘_; id; assoc; identityˡ; module HomReasoning)
    module D   = Category D using (id)
    module E   = Category E using (_∘_; id; _≈_; assoc; identityˡ; module HomReasoning)
    module L   = Functor L using (₀; ₁)
    module R   = Functor R using (₀; ₁; identity)
    module L′  = Functor L′ using (₀; ₁; identity)
    module R′  = Functor R′ using (₀; ₁)
    module ⊣⊢₁ = _⊣⊢_ L⊣⊢R using (zig; module unit; module counit)
    module ⊣⊢₂ = _⊣⊢_ L′⊣⊢R′ using (zig; module unit; module counit)

    unit : idF ≃ (R ∘F R′) ∘F L′ ∘F L
    unit = record
      { F⇒G = ntHelper record
        { η       = λ c → R.₁ (⊣⊢₂.unit.⇒.η (L.₀ c)) ∘ ⊣⊢₁.unit.⇒.η c
        ; commute = λ {x} {y} f → begin
          (R.₁ (⊣⊢₂.unit.⇒.η (L.₀ y)) ∘ ⊣⊢₁.unit.⇒.η y) ∘ f
            ≈⟨ pullʳ (⊣⊢₁.unit.⇒.commute f) ⟩
          R.₁ (⊣⊢₂.unit.⇒.η (L.₀ y)) ∘ R.₁ (L.₁ f) ∘ ⊣⊢₁.unit.⇒.η x
            ≈⟨ pullˡ ([ R ]-resp-square (⊣⊢₂.unit.⇒.commute (L.₁ f))) ⟩
          (R.₁ (R′.₁ (L′.₁ (L.₁ f))) ∘ R.₁ (⊣⊢₂.unit.⇒.η (L.₀ x))) ∘ ⊣⊢₁.unit.⇒.η x
            ≈⟨ assoc ⟩
          R.₁ (R′.₁ (L′.₁ (L.₁ f))) ∘ R.₁ (⊣⊢₂.unit.⇒.η (L.₀ x)) ∘ ⊣⊢₁.unit.⇒.η x
            ∎
        }
      ; F⇐G = ntHelper record
        { η       = λ c → ⊣⊢₁.unit.⇐.η c ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ c))
        ; commute = λ {x} {y} f → begin
          (⊣⊢₁.unit.⇐.η y ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ y))) ∘ R.₁ (R′.₁ (L′.₁ (L.₁ f)))
            ≈⟨ pullʳ ([ R ]-resp-square (⊣⊢₂.unit.⇐.commute (L.₁ f))) ⟩
          ⊣⊢₁.unit.⇐.η y ∘ R.₁ (L.₁ f) ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ x))
            ≈⟨ pullˡ (⊣⊢₁.unit.⇐.commute f) ⟩
          (f ∘ ⊣⊢₁.unit.⇐.η x) ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ x))
            ≈⟨ assoc ⟩
          f ∘ ⊣⊢₁.unit.⇐.η x ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ x))
            ∎
        }
      ; iso = λ c → record
        { isoˡ = begin
          (⊣⊢₁.unit.⇐.η c ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ c))) ∘ R.₁ (⊣⊢₂.unit.⇒.η (L.₀ c)) ∘ ⊣⊢₁.unit.⇒.η c
            ≈⟨ center ([ R ]-resp-∘ (⊣⊢₂.unit.iso.isoˡ (L.₀ c))) ⟩
          ⊣⊢₁.unit.⇐.η c ∘ R.₁ D.id ∘ ⊣⊢₁.unit.⇒.η c
            ≈⟨ refl⟩∘⟨ elimˡ R.identity ⟩
          ⊣⊢₁.unit.⇐.η c ∘ ⊣⊢₁.unit.⇒.η c
            ≈⟨ ⊣⊢₁.unit.iso.isoˡ c ⟩
          id
            ∎
        ; isoʳ = begin
          (R.₁ (⊣⊢₂.unit.⇒.η (L.₀ c)) ∘ ⊣⊢₁.unit.⇒.η c) ∘ ⊣⊢₁.unit.⇐.η c ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ c))
            ≈⟨ center (⊣⊢₁.unit.iso.isoʳ c) ⟩
          R.₁ (⊣⊢₂.unit.⇒.η (L.₀ c)) ∘ id ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ c))
            ≈⟨ refl⟩∘⟨ identityˡ ⟩
          R.₁ (⊣⊢₂.unit.⇒.η (L.₀ c)) ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ c))
            ≈⟨ [ R ]-resp-∘ (⊣⊢₂.unit.iso.isoʳ (L.₀ c)) ⟩
          R.₁ D.id
            ≈⟨ R.identity ⟩
          id
            ∎
        }
      }
      where open C
            open HomReasoning
            open MR C

    module unit = NaturalIsomorphism unit using (module ⇒)

    counit : (L′ ∘F L) ∘F R ∘F R′ ≃ idF
    counit = record
      { F⇒G = ntHelper record
        { η       = λ e → ⊣⊢₂.counit.⇒.η e ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ e))
        ; commute = λ {x} {y} f → begin
          (⊣⊢₂.counit.⇒.η y ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ y))) ∘ L′.₁ (L.₁ (R.₁ (R′.₁ f)))
            ≈⟨ pullʳ ([ L′ ]-resp-square (⊣⊢₁.counit.⇒.commute (R′.₁ f))) ⟩
          ⊣⊢₂.counit.⇒.η y ∘ L′.₁ (R′.₁ f) ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ x))
            ≈⟨ pullˡ (⊣⊢₂.counit.⇒.commute f) ⟩
          (f ∘ ⊣⊢₂.counit.⇒.η x) ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ x))
            ≈⟨ assoc ⟩
          f ∘ ⊣⊢₂.counit.⇒.η x ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ x))
            ∎
        }
      ; F⇐G = ntHelper record
        { η       = λ e → L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ e)) ∘ ⊣⊢₂.counit.⇐.η e
        ; commute = λ {x} {y} f → begin
          (L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ y)) ∘ ⊣⊢₂.counit.⇐.η y) ∘ f
            ≈⟨ pullʳ (⊣⊢₂.counit.⇐.commute f) ⟩
          L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ y)) ∘ L′.₁ (R′.₁ f) ∘ ⊣⊢₂.counit.⇐.η x
            ≈⟨ pullˡ ([ L′ ]-resp-square (⊣⊢₁.counit.⇐.commute (R′.₁ f))) ⟩
          (L′.₁ (L.₁ (R.₁ (R′.₁ f))) ∘ L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ x))) ∘ ⊣⊢₂.counit.⇐.η x
            ≈⟨ assoc ⟩
          L′.₁ (L.₁ (R.₁ (R′.₁ f))) ∘ L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ x)) ∘ ⊣⊢₂.counit.⇐.η x
            ∎
        }
      ; iso = λ e → record
        { isoˡ = begin
          (L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ e)) ∘ ⊣⊢₂.counit.⇐.η e) ∘ ⊣⊢₂.counit.⇒.η e ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ e))
            ≈⟨ center (⊣⊢₂.counit.iso.isoˡ e) ⟩
          L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ e)) ∘ id ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ e))
            ≈⟨ refl⟩∘⟨ identityˡ ⟩
          L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ e)) ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ e))
            ≈⟨ [ L′ ]-resp-∘ (⊣⊢₁.counit.iso.isoˡ (R′.₀ e)) ⟩
          L′.₁ D.id
            ≈⟨ L′.identity ⟩
          id
            ∎
        ; isoʳ = begin
          (⊣⊢₂.counit.⇒.η e ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ e))) ∘ L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ e)) ∘ ⊣⊢₂.counit.⇐.η e
            ≈⟨ center ([ L′ ]-resp-∘ (⊣⊢₁.counit.iso.isoʳ (R′.₀ e))) ⟩
          ⊣⊢₂.counit.⇒.η e ∘ L′.₁ D.id ∘ ⊣⊢₂.counit.⇐.η e
            ≈⟨ refl⟩∘⟨ elimˡ L′.identity ⟩
          ⊣⊢₂.counit.⇒.η e ∘ ⊣⊢₂.counit.⇐.η e
            ≈⟨ ⊣⊢₂.counit.iso.isoʳ e ⟩
          id
            ∎
        }
      }
      where open E
            open HomReasoning
            open MR E

    module counit = NaturalIsomorphism counit using (module ⇒)

    zig : ∀ {c} → counit.⇒.η (L′.₀ (L.₀ c)) E.∘ L′.₁ (L.₁ (unit.⇒.η c)) E.≈ E.id
    zig {c} = begin
      counit.⇒.η (L′.₀ (L.₀ c)) ∘ L′.₁ (L.₁ (unit.⇒.η c))
        ≈⟨ refl⟩∘⟨ Functor.homomorphism (L′ ∘F L) ⟩
      counit.⇒.η (L′.₀ (L.₀ c)) ∘ L′.₁ (L.₁ (R.₁ (⊣⊢₂.unit.⇒.η (L.₀ c)))) ∘ L′.₁ (L.₁ (⊣⊢₁.unit.⇒.η c))
        ≈⟨ center ([ L′ ]-resp-square (⊣⊢₁.counit.⇒.commute (⊣⊢₂.unit.⇒.η (L.₀ c)))) ⟩
      ⊣⊢₂.counit.⇒.η (L′.₀ (L.₀ c)) ∘ (L′.₁ (⊣⊢₂.unit.⇒.η (L.₀ c)) ∘ L′.₁ (⊣⊢₁.counit.⇒.η (L.₀ c))) ∘ L′.₁ (L.₁ (⊣⊢₁.unit.⇒.η c))
        ≈⟨ pull-first ⊣⊢₂.zig ⟩
      id ∘ L′.₁ (⊣⊢₁.counit.⇒.η (L.₀ c)) ∘ L′.₁ (L.₁ (⊣⊢₁.unit.⇒.η c))
        ≈⟨ elimʳ (([ L′ ]-resp-∘ ⊣⊢₁.zig) ○ L′.identity) ⟩
      id
        ∎
      where open E
            open HomReasoning
            open MR E

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- {-# OPTIONS -v tc.constr.findInScope:50 #-}
module InstanceArguments.06-listEquality where

infixr 5 _∷_

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

data Bool : Set where
  true : Bool
  false : Bool

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

or : Bool → Bool → Bool
or true _ = true
or _ true = true
or false false = false

and : Bool → Bool → Bool
and false _ = false
and _ false = false
and true true = false

not : Bool → Bool
not true = false
not false = true

record Eq (A : Set) : Set where
  field eq : A → A → Bool

instance
  listEq : {A : Set} {{EqA : Eq A}} → Eq (List A)
  listEq {A} {{eqA}} = record { eq = eq' } where
    eq' : List A → List A → Bool
    eq' [] [] = true
    eq' (a ∷ as) (b ∷ bs) = and (Eq.eq eqA a b) (eq' as bs)
    eq' _ _ = false

primEqBool : Bool → Bool → Bool
primEqBool true = id
primEqBool false = not

instance
  eqBool : Eq Bool
  eqBool = record { eq = primEqBool }

open Eq {{...}}

test = eq (true ∷ false ∷ true ∷ []) (true ∷ false ∷ [])


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

works : Nat → Nat
works 0 = 0
works x@(suc _) = x

forced-implicit : ∀ x {y} → x ≡ y → Nat
forced-implicit x .{x} refl = x

forced-instance : ∀ x {{y}} → x ≡ y → Nat
forced-instance x .{{x}} refl = x

fails : ∀ {x : Nat} → Nat
fails {0} = 0
fails x@{suc _} = x

forced-implicit' : ∀ x {y} → x ≡ y → Nat
forced-implicit' x x@.{_} refl = x

forced-instance' : ∀ x {{y}} → x ≡ y → Nat
forced-instance' x x@.{{_}} refl = x


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Definitions for types of functions that only require an equality
-- relation over the co-domain.
------------------------------------------------------------------------

-- The contents of this file should usually be accessed from `Function`.

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

open import Relation.Binary

module Function.Definitions.Core2
  {b ℓ₂} {B : Set b} (_≈₂_ : Rel B ℓ₂)
  where

open import Data.Product using (∃)
open import Level using (Level; _⊔_)

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

Surjective : ∀ {a} {A : Set a} → (A → B) → Set (a ⊔ b ⊔ ℓ₂)
Surjective f = ∀ y → ∃ λ x → f x ≈₂ y

-- (Note the name `LeftInverse` is used for the bundle)
Inverseˡ : ∀ {a} {A : Set a} → (A → B) → (B → A) → Set (b ⊔ ℓ₂)
Inverseˡ f g = ∀ x → f (g x) ≈₂ x


text:
module RandomAccessList.Standard.Core.Properties where

open import BuildingBlock
open import BuildingBlock.BinaryLeafTree using (BinaryLeafTree; Node; Leaf)
open import RandomAccessList.Standard.Core

open import Data.Nat
open import Data.Nat.Etc
open import Data.Nat.Properties.Simple
open import Data.Product as Prod
open import Data.Product hiding (map)

open import Function
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Nullary.Decidable using (False; True; fromWitnessFalse)
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; cong₂; trans; sym; inspect)
open PropEq.≡-Reasoning

--------------------------------------------------------------------------------
-- On ⟦_⟧ and ⟦_⟧ₙ

-- identity
⟦[]⟧ₙ≡0 : ∀ {A n} → (xs : 0-1-RAL A n) → xs ≡ [] → ⟦ xs ⟧ₙ ≡ 0
⟦[]⟧ₙ≡0 (     []) p  = refl
⟦[]⟧ₙ≡0 (  0∷ xs) ()
⟦[]⟧ₙ≡0 (x 1∷ xs) ()

⟦[]⟧≡0 : ∀ {n A} → (xs : 0-1-RAL A n) → xs ≡ [] → ⟦ xs ⟧ ≡ 0
⟦[]⟧≡0 {zero }       []  p  = refl
⟦[]⟧≡0 {suc n}       []  p  = *-right-zero (2 * 2 ^ n)
⟦[]⟧≡0         (  0∷ xs) ()
⟦[]⟧≡0         (x 1∷ xs) ()

⟦[]⟧≡⟦[]⟧ : ∀ {n A} → ⟦ [] {A} {suc n} ⟧ ≡ ⟦ [] {A} {n} ⟧
⟦[]⟧≡⟦[]⟧ {n} =
    begin
        (2 * 2 ^ n) * 0
    ≡⟨ *-right-zero (2 * 2 ^ n) ⟩
        0
    ≡⟨ sym (*-right-zero (2 ^ n)) ⟩
        2 ^ n * 0
    ∎

⟦0∷xs⟧≡⟦xs⟧ : ∀ {n A} → (xs : 0-1-RAL A (suc n)) → ⟦ 0∷ xs ⟧ ≡ ⟦ xs ⟧
⟦0∷xs⟧≡⟦xs⟧ {zero} xs = +-right-identity (2 * ⟦ xs ⟧ₙ)
⟦0∷xs⟧≡⟦xs⟧ {suc n} xs =
    begin
        2 * 2 ^ n * (2 * ⟦ xs ⟧ₙ)
    ≡⟨ sym (*-assoc (2 * 2 ^ n) 2 ⟦ xs ⟧ₙ) ⟩
        2 * 2 ^ n * 2 * ⟦ xs ⟧ₙ
    ≡⟨ cong (λ x → x * ⟦ xs ⟧ₙ) (*-assoc 2 (2 ^ n) 2) ⟩
        2 * (2 ^ n * 2) * ⟦ xs ⟧ₙ
    ≡⟨ cong (λ x → 2 * x * ⟦ xs ⟧ₙ) (*-comm (2 ^ n) 2) ⟩
        (2 * (2 * 2 ^ n)) * ⟦ xs ⟧ₙ
    ∎

⟦0∷xs⟧≢0⇒⟦xs⟧≢0  : ∀ {n A}
                → (xs : 0-1-RAL A (suc n))
                → ⟦ 0∷ xs ⟧ ≢ 0
                → ⟦ xs ⟧ ≢ 0
⟦0∷xs⟧≢0⇒⟦xs⟧≢0 xs p = contraposition (trans (⟦0∷xs⟧≡⟦xs⟧ xs)) p

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module Naturals where

-- The naturals are an inductive datatype

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

-- A pragma

{-# BUILTIN NATURAL ℕ #-}

-- Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

-- Operations on naturals are recursive functions

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩    -- is shorthand for
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩    -- inductive case
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩    -- inductive case
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩    -- base case
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩    -- is longhand for
    5
  ∎

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩
    suc (1 + 3)
  ≡⟨⟩
    suc (suc (0 + 3))
  ≡⟨⟩
    suc (suc 3)
  ≡⟨⟩
    5
  ∎

_ : 2 + 3 ≡ 5
_ = refl

-- Multiplication

_*_ : ℕ → ℕ → ℕ
zero    * n  =  zero
(suc m) * n  =  n + (m * n)

_ =
  begin
    2 * 3
  ≡⟨⟩    -- inductive case
    3 + (1 * 3)
  ≡⟨⟩    -- inductive case
    3 + (3 + (0 * 3))
  ≡⟨⟩    -- base case
    3 + (3 + 0)
  ≡⟨⟩    -- simplify
    6
  ∎

-- Monus

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

_ =
  begin
    3 ∸ 2
  ≡⟨⟩
    2 ∸ 1
  ≡⟨⟩
    1 ∸ 0
  ≡⟨⟩
    1
  ∎

_ =
  begin
    2 ∸ 3
  ≡⟨⟩
    1 ∸ 2
  ≡⟨⟩
    0 ∸ 1
  ≡⟨⟩
    0
  ∎

-- Precedence

infixl 6  _+_  _∸_
infixl 7  _*_

-- More pragmas

{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-# BUILTIN NATMINUS _∸_ #-}

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


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

module WithoutK6 where

-- Equality defined with two indices.

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ x → x ≡ x

weak-K : {A : Set} {a b : A} (p q : a ≡ b) (α β : p ≡ q) → α ≡ β
weak-K (refl a) .(refl a) (refl .(refl a)) (refl .(refl a)) =
  refl (refl (refl a))


text:
open import Agda.Builtin.Reflection

t = quoteTerm (∀ {α} {A : Set α} -> A -> A)

macro
  m : Type -> Term -> TC _
  m = unify

idType = m t

max_forks_repo_name: shlevy/agda


text:
------------------------------------------------------------------------------
-- Definition of addition using a recursive equation
------------------------------------------------------------------------------

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

module FOTC.AddRecursiveEquation where

open import FOTC.Base

-- We add 3 to the fixities of the Agda standard library 0.8.1 (see
-- Data/Nat.agda).
infixl 9 _+_

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

postulate
  _+_  : D → D → D
  +-eq : ∀ m n → m + n ≡ (if (iszero₁ m) then n else succ₁ (pred₁ m + n))
{-# ATP axiom +-eq #-}

postulate
  +-0x : ∀ n → zero + n      ≡ n
  +-Sx : ∀ m n → succ₁ m + n ≡ succ₁ (m + n)
{-# ATP prove +-0x #-}
{-# ATP prove +-Sx #-}

-- $ cd fotc/notes/thesis
-- $ agda -i. -i ~/fot FOTC/AddRecursiveEquation.agda
-- $ apia -i. -i ~/fot FOTC/AddRecursiveEquation.agda
-- Proving the conjecture in /tmp/FOTC/AddRecursiveEquation/21-43-Sx.tptp ...
-- Vampire 0.6 (revision 903) proved the conjecture
-- Proving the conjecture in /tmp/FOTC/AddRecursiveEquation/20-43-0x.tptp ...
-- Vampire 0.6 (revision 903) proved the conjecture


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

open import Util.HoTT.HLevel.Core
open import Util.Prelude

private
  variable
    α : Level
    A : Set α

Singleton : {A : Set α} (x : A) → Set α
Singleton x = ∃[ y ] (y ≡ x)

IsContr-Singleton : {x : A} → IsContr (Singleton x)
IsContr-Singleton {x = x} = (x , refl) , λ { (x′ , refl) → refl }

Singleton-HContr : {A : Set α} (x : A) → HContr α
Singleton-HContr x = HLevel⁺ (Singleton x) IsContr-Singleton

Singleton′ : {A : Set α} (x : A) → Set α
Singleton′ x = ∃[ y ] (x ≡ y)

IsContr-Singleton′ : {x : A} → IsContr (Singleton′ x)
IsContr-Singleton′ {x = x} = (x , refl) , λ { (x′ , refl) → refl }

Singleton′-HContr : {A : Set α} (x : A) → HContr α
Singleton′-HContr x = HLevel⁺ (Singleton′ x) IsContr-Singleton′

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
------------------------------------------------------------------------
-- A virtual machine
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module Lambda.Delay-monad.Virtual-machine where

open import Equality.Propositional

open import Maybe equality-with-J
open import Monad equality-with-J

open import Delay-monad
open import Delay-monad.Monad

open import Lambda.Delay-monad.Interpreter
open import Lambda.Syntax
open import Lambda.Virtual-machine

open Closure Code

mutual

  -- A functional semantics for the VM.

  exec : ∀ {i} → State → M i Value
  exec s with step s
  ... | continue s′ = laterM (∞exec s′)
  ... | done v      = return v
  ... | crash       = fail

  ∞exec : ∀ {i} → State → M′ i Value
  force (run (∞exec s)) = run (exec s)

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module +*^ where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_)

open import Induction′ using (+-identityʳ)
open import *-comm using (*-comm)
open import *-assoc using (*-assoc)

-- 積法の左単位元
*-identityˡ : ∀ (n : ℕ) → 1 * n ≡ n
*-identityˡ zero    = refl
*-identityˡ (suc n) =
  begin
    1 * (suc n)
  ≡⟨⟩
    (suc n) + (zero * (suc n))
  ≡⟨⟩
    (suc n) + zero
  ≡⟨ +-identityʳ (suc n) ⟩
    (suc n)
  ∎

*-swap : ∀ (m n p : ℕ) → m * n * p ≡ m * p * n
*-swap m n p =
  begin
    (m * n) * p
  ≡⟨ *-assoc m n p ⟩
    m * (n * p)
  ≡⟨ cong (m *_) (*-comm n p) ⟩
    m * (p * n)
  ≡⟨ sym (*-assoc m p n) ⟩
    (m * p) * n
  ∎

^-distribˡ-+-* : ∀ (m n p : ℕ) → m ^ (n + p) ≡ (m ^ n) * (m ^ p)
^-distribˡ-+-* m zero p =
  begin
    m ^ (zero + p)
  ≡⟨⟩
    m ^ p
  ≡⟨ sym (*-identityˡ (m ^ p)) ⟩
    1 * (m ^ p)
  ≡⟨⟩
    (m ^ zero) * (m ^ p)
  ∎
^-distribˡ-+-* zero (suc n) p =
  begin
    zero ^ ((suc n) + p)
  ≡⟨⟩
    zero * (zero ^ (n + p))
  ≡⟨⟩
    zero
  ≡⟨⟩
    (zero ^ (suc n)) * (zero ^ p)
  ∎
^-distribˡ-+-* (suc m) (suc n) p =
  begin
    (suc m) ^ ((suc n) + p)
  ≡⟨⟩
    (suc m) * ((suc m) ^ (n + p))
  ≡⟨ cong ((suc m) *_) (^-distribˡ-+-* ((suc m)) n p) ⟩
    (suc m) * (((suc m) ^ n) * ((suc m) ^ p))
  ≡⟨ sym (*-assoc (suc m) (suc m ^ n) (suc m ^ p)) ⟩
    ((suc m) * ((suc m) ^ n)) * ((suc m) ^ p)
  ≡⟨⟩
    ((suc m) ^ (suc n)) * ((suc m) ^ p)
  ∎

^-distribʳ-* : ∀ (m n p : ℕ) → (m * n) ^ p ≡ (m ^ p) * (n ^ p)
^-distribʳ-* m n zero =
  begin
    (m * n) ^ zero
  ≡⟨⟩
    1
  ≡⟨⟩
    (m ^ zero) * (n ^ zero)
  ∎
^-distribʳ-* m n (suc p) =
  begin
    (m * n) ^ (suc p)
  ≡⟨⟩
    (m * n) * ((m * n) ^ p)
  ≡⟨ cong ((m * n) *_) (^-distribʳ-* m n p) ⟩
    (m * n) * ((m ^ p) * (n ^ p))
  ≡⟨ sym (*-assoc (m * n) (m ^ p) (n ^ p)) ⟩
    ((m * n) * (m ^ p)) * (n ^ p)
  ≡⟨ cong (_* (n ^ p)) (*-swap m n (m ^ p)) ⟩
    ((m * (m ^ p)) * n) * (n ^ p)
  ≡⟨⟩
    ((m ^ (suc p)) * n) * (n ^ p)
  ≡⟨ *-assoc (m * (m ^ p)) n (n ^ p) ⟩
    (m ^ (suc p)) * (n * (n ^ p))
  ≡⟨⟩
    (m ^ (suc p)) * (n ^ (suc p))
  ∎

^-*-assoc : ∀ (m n p : ℕ) → (m ^ n) ^ p ≡ m ^ (n * p)
^-*-assoc m n zero =
  begin
    (m ^ n) ^ zero
  ≡⟨⟩
    1
  ≡⟨⟩
    m ^ (zero * n)
  ≡⟨ cong (m ^_) (*-comm zero n) ⟩
    m ^ (n * zero)
  ∎
^-*-assoc m n (suc p) =
  begin
    (m ^ n) ^ (suc p)
  ≡⟨⟩
    (m ^ n) * ((m ^ n) ^ p)
  ≡⟨ cong ((m ^ n) *_) (^-*-assoc m n p) ⟩
    (m ^ n) * (m ^ (n * p))
  ≡⟨ sym (^-distribˡ-+-* m n (n * p)) ⟩
    m ^ (n + (n * p))
  ≡⟨ cong (λ p*n → m ^ (n + p*n)) (*-comm n p) ⟩
    m ^ (n + (p * n))
  ≡⟨⟩
    m ^ ((suc p) * n)
  ≡⟨ cong (m ^_) (*-comm (suc p) n) ⟩
    m ^ (n * (suc p))
  ∎


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Setoids.Facts.Limit where

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

open import Cats.Category
open import Cats.Category.Cones as Cones using (Cone)
open import Cats.Category.Setoids as Setoids using (Setoids ; ≈-intro ; ≈-elim)
open import Cats.Functor using (Functor)

open Cone
open Cones._⇒_
open Functor
open Setoid using (Carrier)
open Setoids._⇒_

record Lim {l} {J : Category l l l} (F : Functor J (Setoids l l)) : Set l where
  private
    module J = Category J
    module F$ {x} = Setoid (F .fobj x)

  field
    arr : ∀ j → F .fobj j .Carrier
    consistent : ∀ {i j} (f : i J.⇒ j)
      → arr j F$.≈ F .fmap f .Setoids._⇒_.arr (arr i)

open Lim public

instance
  complete : ∀ {l} → Complete (Setoids l l) l l l
  complete .Complete.lim′ {J} F = record
    { cone = record
      { Apex = record
        { Carrier = Lim F
        ; _≈_ = λ f g → ∀ j → f .arr j F$.≈ g .arr j
        ; isEquivalence = record
          { refl = λ j → F$.refl
          ; sym = λ eq j → F$.sym (eq j)
          ; trans = λ eq₁ eq₂ j → F$.trans (eq₁ j) (eq₂ j)
          }
        }
      ; arr = λ j → record { resp = λ eq → eq j }
      ; commute = λ h → ≈-intro λ {f} {g} f≈g → F$.trans (f≈g _) (g .consistent h)
      }
    ; isLimit = λ X → record
      { arr = record
        { arr = record
          { arr = λ x → record
            { arr = λ j → X .arr j .arr x
            ; consistent = λ f → X .commute f .≈-elim (Setoid.refl (Apex X))
            }
          ; resp = λ eq j → X .arr j .resp eq
          }
        ; commute = λ j → ≈-intro λ eq → X .arr j .resp eq
        }
      ; unique = λ {g} _ → ≈-intro λ eq j
          → F$.sym (g .commute j .≈-elim (Setoid.sym (Apex X) eq))
      }
    }
    where
      module F$ {x} = Setoid (F .fobj x)

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax Semiring | SR

type
  * : 0-ary

term
  zero : * | 𝟘
  add  : *  *  ->  * | _⊕_ l20
  one  : * | 𝟙
  mult : *  *  ->  * | _⊗_ l30

theory
  (𝟘U⊕ᴸ) a |> add (zero, a) = a
  (𝟘U⊕ᴿ) a |> add (a, zero) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊕C) a b |> add(a, b) = add(b, a)
  (𝟙U⊗ᴸ) a |> mult (one, a) = a
  (𝟙U⊗ᴿ) a |> mult (a, one) = a
  (⊗A) a b c |> mult (mult(a, b), c) = mult (a, mult(b, c))
  (⊗D⊕ᴸ) a b c |> mult (a, add (b, c)) = add (mult(a, b), mult(a, c))
  (⊗D⊕ᴿ) a b c |> mult (add (a, b), c) = add (mult(a, c), mult(b, c))
  (𝟘X⊗ᴸ) a |> mult (zero, a) = zero
  (𝟘X⊗ᴿ) a |> mult (a, zero) = zero
-}

module Semiring.Signature where

open import SOAS.Context

open import SOAS.Common

open import SOAS.Syntax.Signature *T public
open import SOAS.Syntax.Build *T public

-- Operator symbols
data SRₒ : Set where
  zeroₒ addₒ oneₒ multₒ : SRₒ

-- Term signature
SR:Sig : Signature SRₒ
SR:Sig = sig λ
  {  zeroₒ  → ⟼₀ *
  ;  addₒ   → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  ;  oneₒ   → ⟼₀ *
  ;  multₒ  → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  }

open Signature SR:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
-- Andreas, 2014-10-23

data Bool : Set where
  true false : Bool

module _ (b : Bool) where

  f : Set
  f = {!b!}

-- Agda produces garbage when splitting on b.
-- Splitting on module parameters should be forbidden outright.


text:
module Issue892 where

data D : Set where
  d : D

module I where
  i : D
  i = d

module M0 (X : Set) where
  module M1 where
    h : D
    h = d
  module M2 where
    open M1 public
    open I public

module M = M0 D

good : D
good = M.M1.h

bad : D
bad = M.M2.h


text:
module Dave.Structures.Semigroup where
    open import Dave.Structures.Definitions public

    record IsSemigroup {A : Set} (_·_ : op₂ A) : Set where
        field
            assoc : associative _·_

    record Semigroup : Set₁ where
        field
            Carrier : Set
            _·_ : op₂ Carrier
            isSemigroup : IsSemigroup _·_


text:
module Tactic.Reflection.Parse where

open import Prelude
open import Control.Monad.State
open import Control.Monad.Zero
open import Builtin.Reflection
open import Tactic.Reflection.Equality
open import Container.Traversable

ParseTerm : (Set → Set) → Set → Set
ParseTerm M = StateT (Nat × List (Term × Nat)) M

module _ {M : Set → Set} {{_ : MonadZero M}} where

  runParse : ∀ {A} → ParseTerm M A → M (A × List Term)
  runParse r =
    second (reverse ∘ map fst ∘ snd) <$>
    runStateT r (0 , [])

  private
    fresh : Term → ParseTerm M Nat
    fresh t =
      get >>= uncurry′ λ i Γ →
      i <$ put (suc i , (t , i) ∷ Γ)

    pAtom : Term → ParseTerm M Nat
    pAtom v = maybe (fresh v) pure =<< gets (flip lookup v ∘ snd)

  module _ {F : Set → Set} {{_ : Traversable F}} {E : Set}
           (mkVar : Nat → F E) (matchTm : Term → Maybe (F Term)) (fold : F E → E) where

    {-# TERMINATING #-}
    parseTerm : Term → ParseTerm M E
    parseTerm v =
      case matchTm v of λ where
        nothing  → fold ∘ mkVar <$> pAtom v
        (just s) → fold <$> traverse parseTerm s

    parseEqn : Term → ParseTerm M (E × E)
    parseEqn (def (quote _≡_) (_ ∷ _ ∷ vArg x ∷ vArg y ∷ [])) =
      ⦇ parseTerm x , parseTerm y ⦈
    parseEqn goal = empty

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
open import Prelude

module Implicits.Semantics.Lemmas where

open import SystemF.Everything as F using ()
open import Extensions.ListFirst
open import Data.Fin.Substitution
open import Data.Vec hiding ([_])
open import Data.Vec.Properties
open import Extensions.Vec

open import Implicits.Syntax
open import Implicits.WellTyped
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Implicits.Semantics.Type
open import Implicits.Semantics.Context

private
  module TS = TypeSubst

⟦a/var⟧ : ∀ {ν ν'} (a : Type ν) (s : Sub Fin ν ν') → ⟦ a TS./Var s ⟧tp→ ≡ ⟦ a ⟧tp→ F./Var s
⟦a/var⟧ (simpl (tc x)) s = refl
⟦a/var⟧ (simpl (tvar n)) s = refl
⟦a/var⟧ (simpl (a →' b)) s = cong₂ F._→'_ (⟦a/var⟧ a s) (⟦a/var⟧ b s)
⟦a/var⟧ (a ⇒ b) s = cong₂ F._→'_ (⟦a/var⟧ a s) (⟦a/var⟧ b s)
⟦a/var⟧ (∀' a) s = cong F.∀' (⟦a/var⟧ a (s VarSubst.↑))

⟦weaken⟧ : ∀ {ν} (a : Type ν) → ⟦ TS.weaken a ⟧tp→ ≡ F.weaken ⟦ a ⟧tp→
⟦weaken⟧ x = ⟦a/var⟧ x VarSubst.wk

-- helper lemma on mapping type-semantics over weakend substitutions
⟦weaken⟧tps→ : ∀ {ν n} (xs : Vec (Type ν) n) →
               ⟦ (map TS.weaken xs) ⟧tps→ ≡ (map F.weaken ⟦ xs ⟧tps→)
⟦weaken⟧tps→ xs = begin
  (map ⟦_⟧tp→ ∘ map TS.weaken) xs
    ≡⟨ sym $ (map-∘ ⟦_⟧tp→ TS.weaken) xs ⟩
  map (⟦_⟧tp→ ∘ TS.weaken) xs
    ≡⟨ (map-cong ⟦weaken⟧) xs ⟩
  map (F.weaken ∘ ⟦_⟧tp→) xs
    ≡⟨ (map-∘ F.weaken ⟦_⟧tp→) xs ⟩
  map F.weaken (map ⟦_⟧tp→ xs) ∎

-- the semantics of identity type-substitution is exactly
-- system-f's identity type substitution
⟦id⟧tp→ : ∀ {n} → map ⟦_⟧tp→ (TS.id {n}) ≡ F.id
⟦id⟧tp→ {zero} = refl
⟦id⟧tp→ {suc n} = begin
  map ⟦_⟧tp→ (simpl (tvar zero) ∷ map TS.weaken (TS.id {n}))
    ≡⟨ refl ⟩
  F.tvar zero ∷ (map ⟦_⟧tp→ (map TS.weaken (TS.id {n})))
    ≡⟨ cong (_∷_ (F.tvar zero)) (⟦weaken⟧tps→ (TS.id {n})) ⟩
  F.tvar zero ∷ (map F.weaken (map ⟦_⟧tp→ (TS.id {n})))
    ≡⟨ cong (λ e → F.tvar zero ∷ (map F.weaken e)) ⟦id⟧tp→ ⟩
  F.tvar zero ∷ (map F.weaken (F.id {n}))
    ≡⟨ refl ⟩
  F.id ∎

-- the semantics of type weakening is exactly system-f's type weakening
⟦wk⟧tp→ : ∀ {n} → map ⟦_⟧tp→ (TS.wk {n}) ≡ F.wk {n}
⟦wk⟧tp→ = begin
  map ⟦_⟧tp→ TS.wk
    ≡⟨ ⟦weaken⟧tps→ TS.id ⟩
  map F.weaken (map ⟦_⟧tp→ TS.id)
    ≡⟨ cong (map F.weaken) ⟦id⟧tp→ ⟩
  F.wk ∎

⟦↑⟧tps→ :  ∀ {ν n} (v : Vec (Type ν) n) → ⟦ v TS.↑ ⟧tps→ ≡ ⟦ v ⟧tps→ F.↑
⟦↑⟧tps→ xs = begin
  F.tvar zero ∷ (map ⟦_⟧tp→ (map TS.weaken xs))
    ≡⟨ cong (_∷_ (F.tvar zero)) (⟦weaken⟧tps→ xs) ⟩
  F.tvar zero ∷ (map F.weaken (map ⟦_⟧tp→ xs))
    ≡⟨ refl ⟩
  (map ⟦_⟧tp→ xs) F.↑ ∎

-- lookup in and interpreted context Γ is equivalent to interpreting a type, looked up in K
lookup-⟦⟧ctx→ : ∀ {ν n} (Γ : Ctx ν n) x → ⟦ lookup x Γ ⟧tp→ ≡ lookup x ⟦ Γ ⟧ctx→
lookup-⟦⟧ctx→ Γ x = lookup⋆map Γ ⟦_⟧tp→ x

-- type substitution commutes with interpreting types
⟦a/s⟧tp→ : ∀ {ν μ} (tp : Type ν) (σ : Sub Type ν μ) → ⟦ tp TS./ σ ⟧tp→ ≡ ⟦ tp ⟧tp→ F./ (map ⟦_⟧tp→ σ)
⟦a/s⟧tp→ (simpl (tc c)) σ = refl
⟦a/s⟧tp→  (simpl (tvar n)) σ = begin
  ⟦ lookup n σ ⟧tp→
    ≡⟨ lookup⋆map σ ⟦_⟧tp→ n ⟩
  ⟦ simpl (tvar n) ⟧tp→ F./ (map ⟦_⟧tp→ σ) ∎
⟦a/s⟧tp→ (l ⇒ r) σ = cong₂ F._→'_ (⟦a/s⟧tp→ l σ) (⟦a/s⟧tp→ r σ)
⟦a/s⟧tp→ (simpl (l →' r)) σ = cong₂ F._→'_ (⟦a/s⟧tp→ l σ) (⟦a/s⟧tp→ r σ)
⟦a/s⟧tp→ (∀' a) σ = begin
  F.∀' ⟦ (a TS./ σ TS.↑) ⟧tp→
    ≡⟨ cong F.∀' (⟦a/s⟧tp→ a (σ TS.↑)) ⟩
  F.∀' (⟦ a ⟧tp→ F./ ⟦ σ TS.↑ ⟧tps→)
    ≡⟨ cong (λ u → F.∀' (⟦ a ⟧tp→ F./ u)) ((⟦↑⟧tps→ σ)) ⟩
  ⟦ ∀' a ⟧tp→ F./ (map ⟦_⟧tp→ σ) ∎

-- forall' application commutes with interpreting types
⟦a/sub⟧tp→ : ∀ {ν} (a : Type (suc ν)) b → ⟦ a TS./ (TS.sub b) ⟧tp→ ≡ ⟦ a ⟧tp→ F./ (F.sub ⟦ b ⟧tp→)
⟦a/sub⟧tp→ a b = begin
  ⟦ a TS./ (TS.sub b) ⟧tp→
  ≡⟨ ⟦a/s⟧tp→ a (b ∷ TS.id) ⟩
  (⟦ a ⟧tp→ F./ (map ⟦_⟧tp→ (b ∷ TS.id)) )
  ≡⟨ refl ⟩
  (⟦ a ⟧tp→ F./ (⟦ b ⟧tp→ ∷ (map ⟦_⟧tp→ TS.id)) )
  ≡⟨ cong (λ s → ⟦ a ⟧tp→ F./ (⟦ b ⟧tp→ ∷ s)) ⟦id⟧tp→ ⟩
  (⟦ a ⟧tp→ F./ (F.sub ⟦ b ⟧tp→)) ∎

⟦a/wk⟧tp→ : ∀ {ν} (tp : Type ν) → ⟦ tp TS./ TS.wk ⟧tp→ ≡ ⟦ tp ⟧tp→ F./ F.wk
⟦a/wk⟧tp→ tp = begin
  ⟦ tp TS./ TS.wk ⟧tp→
    ≡⟨ ⟦a/s⟧tp→ tp TS.wk ⟩
  ⟦ tp ⟧tp→ F./ (map ⟦_⟧tp→ TS.wk)
    ≡⟨ cong (λ e → ⟦ tp ⟧tp→ F./ e) ⟦wk⟧tp→ ⟩
  ⟦ tp ⟧tp→ F./ F.wk ∎

-- type weakening commutes with interpreting types
⟦weaken⟧tp→ : ∀ {ν} (tp : Type ν) → ⟦ tp-weaken tp ⟧tp→ ≡ F.tp-weaken ⟦ tp ⟧tp→
⟦weaken⟧tp→ tp = begin
  ⟦ tp-weaken tp ⟧tp→
    ≡⟨ cong ⟦_⟧tp→ (sym $ TypeLemmas./-wk {t = tp})⟩
  ⟦ tp TS./ TS.wk ⟧tp→
    ≡⟨ ⟦a/wk⟧tp→ tp ⟩
  ⟦ tp ⟧tp→ F./ F.wk
    ≡⟨ F./-wk {t = ⟦ tp ⟧tp→} ⟩
  F.tp-weaken ⟦ tp ⟧tp→ ∎

-- context weakening commutes with interpreting contexts
⟦weaken⟧ctx→ : ∀ {ν n} (Γ : Ctx ν n) → ⟦ ctx-weaken Γ ⟧ctx→ ≡ F.ctx-weaken ⟦ Γ ⟧ctx→
⟦weaken⟧ctx→ [] = refl
⟦weaken⟧ctx→ (x ∷ Γ) with ⟦weaken⟧ctx→ Γ
⟦weaken⟧ctx→ (x ∷ Γ) | ih = begin
  ⟦ (ctx-weaken (x ∷ Γ)) ⟧ctx→ ≡⟨ refl ⟩
  ⟦ x TS./ TS.wk ⟧tp→ ∷ xs ≡⟨ cong (flip _∷_ xs) (⟦a/wk⟧tp→ x) ⟩
  (⟦ x ⟧tp→ F./ F.wk) ∷ ⟦ (ctx-weaken Γ) ⟧ctx→ ≡⟨ cong (_∷_ (⟦ x ⟧tp→ F./ F.wk)) ih ⟩
  (⟦ x ⟧tp→ F./ F.wk) ∷ (F.ctx-weaken ⟦ Γ ⟧ctx→) ≡⟨ refl ⟩
  F.ctx-weaken ⟦ x ∷ Γ ⟧ctx→ ∎
  where
    xs = map ⟦_⟧tp→ $ map (λ s → s TS./ TS.wk ) Γ


text:
-- Andreas, 2017-11-04, while refactoring for issue #2822

-- This is a test case for a with-pattern that overloads operator names

postulate
  A : Set
  _<_ _>_ : A → A → A

data D : Set where
  c : A → A → D

postulate
  f : D

bla : D → Set
bla (c < >) = A

test : Set
test with f
test | c < > = A
  -- This triggers a call to Agda.Syntax.Concrete.Operators.validConPattern, case WithP

-- Should parse.


text:
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Float
  renaming ( primFloatEquality       to _≡ᵇ_
           ; primFloatInequality     to _≤ᵇ_
           ; primFloatLess           to _<ᵇ_
           ; primFloatPlus           to infixl 6 _+_
           ; primFloatMinus          to infixl 6 _-_
           ; primFloatTimes          to infixl 7 _*_
           ; primFloatDiv            to infixl 7 _÷_
           ; primFloatPow            to infix  8 _**_
           ; primFloatNegate         to infix  9 -_
           ; primFloatSqrt           to sqrt
           ; primFloatExp            to e^_
           ; primFloatLog            to log
           ; primFloatSin            to sin
           ; primFloatCos            to cos
           ; primFloatTan            to tan
           ; primFloatASin           to asin
           ; primFloatACos           to acos
           ; primFloatATan           to atan
           ; primFloatATan2          to atan2
           ; primFloatSinh           to sinh
           ; primFloatCosh           to cosh
           ; primFloatTanh           to tanh
           ; primFloatASinh          to asinh
           ; primFloatACosh          to acosh
           ; primFloatATanh          to atanh
           ; primFloatRound          to round
           ; primFloatFloor          to floor
           ; primFloatCeiling        to ceiling
           ; primShowFloat           to show
           ; primFloatToWord64       to toWord
           ; primFloatToRatio        to toRatio
           ; primRatioToFloat        to fromRatio
           ; primFloatDecode         to decode
           ; primFloatEncode         to encode
           ; primFloatIsInfinite     to isInfinite
           ; primFloatIsNaN          to isNaN
           ; primFloatIsNegativeZero to isNegativeZero
           ; primFloatIsSafeInteger  to isSafeInteger
           )
open import Agda.Builtin.Int
open import Agda.Builtin.Maybe
open import Agda.Builtin.Sigma
open import Agda.Builtin.Word
  renaming ( primWord64ToNat to toℕ
           )

-- Prelude

data ⊥ : Set where

_≢_ : {A : Set} (P Q : A) → Set
P ≢ Q = P ≡ Q → ⊥

NaN : Float
NaN = 0.0 ÷ 0.0

-NaN : Float
-NaN = - NaN

Infinity : Float
Infinity = 1.0 ÷ 0.0

-Infinity : Float
-Infinity = - Infinity

MaxFloat : Float
MaxFloat = 1.7976931348623157e308

MinFloat : Float
MinFloat = 2.2250738585072014e-308

MaxSafeIntF : Float
MaxSafeIntF = 9007199254740991.0

MaxSafeIntZ : Int
MaxSafeIntZ = pos 9007199254740991

-- * Tests

-- ** Relations

_ : -NaN      ≡    NaN      ; _ = refl
_ : -0.0      ≢    0.0      ; _ = λ ()
_ :  Infinity ≢   -Infinity ; _ = λ ()
_ :  Infinity ≡    Infinity ; _ = refl
_ : -Infinity ≡   -Infinity ; _ = refl
_ :  Infinity ≡ - -Infinity ; _ = refl
_ :  Infinity ≢   -Infinity ; _ = λ ()

_ :  NaN      ≡ᵇ  NaN      ≡ false ; _ = refl
_ : -NaN      ≡ᵇ  NaN      ≡ false ; _ = refl
_ :  NaN      ≡ᵇ -NaN      ≡ false ; _ = refl
_ : -NaN      ≡ᵇ -NaN      ≡ false ; _ = refl
_ :  Infinity ≡ᵇ  Infinity ≡ true  ; _ = refl
_ : -Infinity ≡ᵇ  Infinity ≡ false ; _ = refl
_ :  Infinity ≡ᵇ -Infinity ≡ false ; _ = refl
_ : -Infinity ≡ᵇ -Infinity ≡ true  ; _ = refl
_ :  MaxFloat ≡ᵇ  MaxFloat ≡ true  ; _ = refl
_ :  MinFloat ≡ᵇ  MinFloat ≡ true  ; _ = refl
_ :  1.0      ≡ᵇ  1.5      ≡ false ; _ = refl
_ :  1.0      ≡ᵇ  1.0      ≡ true  ; _ = refl
_ :  1.5      ≡ᵇ  1.5      ≡ true  ; _ = refl

_ :  NaN      ≤ᵇ  NaN      ≡ false ; _ = refl
_ : -NaN      ≤ᵇ  NaN      ≡ false ; _ = refl
_ :  NaN      ≤ᵇ -NaN      ≡ false ; _ = refl
_ : -NaN      ≤ᵇ -NaN      ≡ false ; _ = refl
_ :  NaN      ≤ᵇ  5.0      ≡ false ; _ = refl
_ : -NaN      ≤ᵇ  5.0      ≡ false ; _ = refl
_ :  5.0      ≤ᵇ -NaN      ≡ false ; _ = refl
_ : -5.0      ≤ᵇ -NaN      ≡ false ; _ = refl
_ :  NaN      ≤ᵇ  Infinity ≡ false ; _ = refl
_ : -NaN      ≤ᵇ  Infinity ≡ false ; _ = refl
_ :  Infinity ≤ᵇ -NaN      ≡ false ; _ = refl
_ : -Infinity ≤ᵇ -NaN      ≡ false ; _ = refl
_ :  Infinity ≤ᵇ  Infinity ≡ true  ; _ = refl
_ : -Infinity ≤ᵇ  Infinity ≡ true  ; _ = refl
_ :  Infinity ≤ᵇ -Infinity ≡ false ; _ = refl
_ : -Infinity ≤ᵇ -Infinity ≡ true  ; _ = refl
_ :  MaxFloat ≤ᵇ  MaxFloat ≡ true  ; _ = refl
_ :  MinFloat ≤ᵇ  MinFloat ≡ true  ; _ = refl
_ :  1.0      ≤ᵇ  1.5      ≡ true  ; _ = refl
_ :  1.0      ≤ᵇ  1.0      ≡ true  ; _ = refl
_ :  1.5      ≤ᵇ  1.5      ≡ true  ; _ = refl

_ :  NaN      <ᵇ  NaN      ≡ false ; _ = refl
_ : -NaN      <ᵇ  NaN      ≡ false ; _ = refl
_ :  NaN      <ᵇ -NaN      ≡ false ; _ = refl
_ : -NaN      <ᵇ -NaN      ≡ false ; _ = refl
_ :  NaN      <ᵇ  5.0      ≡ false ; _ = refl
_ : -NaN      <ᵇ  5.0      ≡ false ; _ = refl
_ :  5.0      <ᵇ -NaN      ≡ false ; _ = refl
_ : -5.0      <ᵇ -NaN      ≡ false ; _ = refl
_ :  NaN      <ᵇ  Infinity ≡ false ; _ = refl
_ : -NaN      <ᵇ  Infinity ≡ false ; _ = refl
_ :  Infinity <ᵇ -NaN      ≡ false ; _ = refl
_ : -Infinity <ᵇ -NaN      ≡ false ; _ = refl
_ :  Infinity <ᵇ  Infinity ≡ false ; _ = refl
_ : -Infinity <ᵇ  Infinity ≡ true  ; _ = refl
_ :  Infinity <ᵇ -Infinity ≡ false ; _ = refl
_ : -Infinity <ᵇ -Infinity ≡ false ; _ = refl
_ :  MaxFloat <ᵇ  MaxFloat ≡ false ; _ = refl
_ :  MinFloat <ᵇ  MinFloat ≡ false ; _ = refl
_ :  1.0      <ᵇ  1.5      ≡ true  ; _ = refl
_ :  1.0      <ᵇ  1.0      ≡ false ; _ = refl
_ :  1.5      <ᵇ  1.5      ≡ false ; _ = refl

_ : isNaN  NaN      ≡ true  ; _ = refl
_ : isNaN -NaN      ≡ true  ; _ = refl
_ : isNaN  Infinity ≡ false ; _ = refl
_ : isNaN -Infinity ≡ false ; _ = refl
_ : isNaN  0.0      ≡ false ; _ = refl
_ : isNaN -0.0      ≡ false ; _ = refl
_ : isNaN  1.0      ≡ false ; _ = refl
_ : isNaN  1.5      ≡ false ; _ = refl

_ : isInfinite  NaN      ≡ false ; _ = refl
_ : isInfinite -NaN      ≡ false ; _ = refl
_ : isInfinite  Infinity ≡ true  ; _ = refl
_ : isInfinite -Infinity ≡ true  ; _ = refl
_ : isInfinite  0.0      ≡ false ; _ = refl
_ : isInfinite -0.0      ≡ false ; _ = refl
_ : isInfinite  1.0      ≡ false ; _ = refl
_ : isInfinite  1.5      ≡ false ; _ = refl

_ : isInfinite ((MaxFloat * MaxFloat) ÷ MaxFloat) ≡ true ; _ = refl

_ : isNegativeZero  NaN      ≡ false ; _ = refl
_ : isNegativeZero -NaN      ≡ false ; _ = refl
_ : isNegativeZero  Infinity ≡ false ; _ = refl
_ : isNegativeZero -Infinity ≡ false ; _ = refl
_ : isNegativeZero  0.0      ≡ false ; _ = refl
_ : isNegativeZero -0.0      ≡ true  ; _ = refl
_ : isNegativeZero  1.0      ≡ false ; _ = refl
_ : isNegativeZero  1.5      ≡ false ; _ = refl

_ : isSafeInteger 1.0         ≡ true  ; _ = refl
_ : isSafeInteger 1.5         ≡ false ; _ = refl
_ : isSafeInteger MaxFloat    ≡ false ; _ = refl
_ : isSafeInteger MinFloat    ≡ false ; _ = refl
_ : isSafeInteger MaxSafeIntF ≡ true  ; _ = refl

-- ** Conversions

_ : show  NaN      ≡  "NaN"      ; _ = refl
_ : show -NaN      ≡  "NaN"      ; _ = refl
_ : show  0.0      ≡  "0.0"      ; _ = refl
_ : show -0.0      ≡ "-0.0"      ; _ = refl
_ : show  Infinity ≡  "Infinity" ; _ = refl
_ : show -Infinity ≡ "-Infinity" ; _ = refl
_ : show  1.0      ≡  "1.0"      ; _ = refl
_ : show  1.5      ≡  "1.5"      ; _ = refl

_ : toℕ (toWord 1.0)       ≡ 4607182418800017408  ; _ = refl
_ : toℕ (toWord 1.5)       ≡ 4609434218613702656  ; _ = refl
_ : toℕ (toWord 0.0)       ≡ 0                    ; _ = refl
_ : toℕ (toWord -0.0)      ≡ 9223372036854775808  ; _ = refl
_ : toℕ (toWord NaN)       ≡ 18444492273895866368 ; _ = refl
_ : toℕ (toWord -NaN)      ≡ 18444492273895866368 ; _ = refl
_ : toℕ (toWord Infinity)  ≡ 9218868437227405312  ; _ = refl
_ : toℕ (toWord -Infinity) ≡ 18442240474082181120 ; _ = refl

_ : round 1.0       ≡ just (pos 1) ; _ = refl
_ : round 1.5       ≡ just (pos 2) ; _ = refl
_ : round NaN       ≡ nothing      ; _ = refl
_ : round -NaN      ≡ nothing      ; _ = refl
_ : round Infinity  ≡ nothing      ; _ = refl
_ : round -Infinity ≡ nothing      ; _ = refl
_ : round MinFloat  ≡ just (pos 0) ; _ = refl
_ : round MaxFloat  ≡ just (pos 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368) ; _ = refl

_ : floor 1.0       ≡ just (pos 1) ; _ = refl
_ : floor 1.5       ≡ just (pos 1) ; _ = refl
_ : floor NaN       ≡ nothing      ; _ = refl
_ : floor -NaN      ≡ nothing      ; _ = refl
_ : floor Infinity  ≡ nothing      ; _ = refl
_ : floor -Infinity ≡ nothing      ; _ = refl
_ : floor MinFloat  ≡ just (pos 0) ; _ = refl
_ : floor MaxFloat  ≡ just (pos 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368) ; _ = refl

_ : ceiling 1.0       ≡ just (pos 1) ; _ = refl
_ : ceiling 1.5       ≡ just (pos 2) ; _ = refl
_ : ceiling NaN       ≡ nothing      ; _ = refl
_ : ceiling -NaN      ≡ nothing      ; _ = refl
_ : ceiling Infinity  ≡ nothing      ; _ = refl
_ : ceiling -Infinity ≡ nothing      ; _ = refl
_ : ceiling MinFloat  ≡ just (pos 1) ; _ = refl
_ : ceiling MaxFloat  ≡ just (pos 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368) ; _ = refl

_ : decode  NaN      ≡ nothing                           ; _ = refl
_ : decode  Infinity ≡ nothing                           ; _ = refl
_ : decode -Infinity ≡ nothing                           ; _ = refl
_ : decode  1.0      ≡ just (pos       1 , pos       0)  ; _ = refl
_ : decode  1.5      ≡ just (pos       3 , negsuc    0)  ; _ = refl
_ : decode  MaxFloat ≡ just (MaxSafeIntZ , pos     971)  ; _ = refl
_ : decode  MinFloat ≡ just (pos       1 , negsuc 1021)  ; _ = refl

_ : encode  (pos     1) (pos       0) ≡ just 1.0         ; _ = refl
_ : encode  (pos     3) (negsuc    0) ≡ just 1.5         ; _ = refl
_ : encode  MaxSafeIntZ (pos       0) ≡ just MaxSafeIntF ; _ = refl
_ : encode  MaxSafeIntZ (pos     971) ≡ just MaxFloat    ; _ = refl
_ : encode  MaxSafeIntZ (pos     972) ≡ nothing          ; _ = refl
_ : encode  (pos     1) (negsuc 1021) ≡ just MinFloat    ; _ = refl
_ : encode  MaxSafeIntZ (negsuc 1075) ≡ nothing          ; _ = refl

_ : toRatio  NaN      ≡ (pos 0    , pos 0) ; _ = refl
_ : toRatio  Infinity ≡ (pos 1    , pos 0) ; _ = refl
_ : toRatio -Infinity ≡ (negsuc 0 , pos 0) ; _ = refl
_ : toRatio  1.0      ≡ (pos 1    , pos 1) ; _ = refl
_ : toRatio  1.5      ≡ (pos 3    , pos 2) ; _ = refl

_ : fromRatio (pos 0)    (pos 0) ≡  NaN      ; _ = refl
_ : fromRatio (pos 1)    (pos 0) ≡  Infinity ; _ = refl
_ : fromRatio (negsuc 0) (pos 0) ≡ -Infinity ; _ = refl
_ : fromRatio (pos 1)    (pos 1) ≡  1.0      ; _ = refl
_ : fromRatio (pos 3)    (pos 2) ≡  1.5      ; _ = refl

_ : e^ 1.0              ≡ 2.718281828459045 ; _ = refl
_ : sin (asin 0.6)      ≡ 0.6               ; _ = refl
_ : cos (acos 0.6)      ≡ 0.6               ; _ = refl
_ : tan (atan 0.4)      ≡ 0.4               ; _ = refl
_ : tan (atan2 0.4 1.0) ≡ 0.4               ; _ = refl


text:
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
import Relation.Binary.EqReasoning as EqReasoning
open import Algebra.FunctionProperties using (LeftZero; RightZero)
open import Algebra.Structures using (module IsCommutativeMonoid;
                                             IsCommutativeMonoid)
open import Data.Product
  -- just to avoid clash with other commas
open import Data.Unit
import OrderLemmas
import Level
open import SemiNearRingRecords
open import Preliminaries

module ValiantRefinement where

record ClosedSemiNearRing : Set₁ where            -- \structure{3}{|ClosedSemiNearRing|}

  field
    snr2 : SemiNearRing2  -- includes |s|, |u| and corresponding operations

  open SemiNearRing2 snr2

  Q : u → u → Set                                 -- \structure{3.1}{Quadratic equation |Q| + properties}
  Q w c = w  +u  c *u c  ≃u  c

  Closure : u -> u -> Set
  Closure w c = Least _≤u_ (Q w) c

  field
    entireQ : Entire Q
  closure : u → u                                 -- \structure{3.2}{Closure function and correctness}
  closure = fun entireQ

  closureHasAll  : ∀ {w : u} → Q w (closure w)
  closureHasAll  = correct entireQ
  field                                           -- \structure{3.3}{Function for |L| and its correctness}
    entireL    : Entire3 L

  completion : u → s → u → s
  completion = fun3 entireL

  completionHasAll : ∀ {a y b} →  L a y b (completion a y b)
  completionHasAll = correct3 entireL

  field                                           -- \structure{3.4}{Ordering properties of |L| and |Q|}
    uniqueL         : UniqueL
    congL           : CongL
    completionMono  : ∀ {a a' y y' b b'} →   a ≤u a'  →  y ≤s y'  →  b ≤u b'  →
                                             completion a y b ≤s completion a' y' b'
    closureIsLeast  : {w : u} -> LowerBound _≤u_ (Q w) (closure w)

  open OrderLemmas snr public

  completionIsLeast : ∀ (a : u) (y : s) (b : u) -> LowerBounds (L a y b) (completion a y b)
  completionIsLeast a y b z p = ≃sTo≤s (uniqueL completionHasAll p)

  open SemiNearRing2 snr2 public
                                                  -- \structure{4}{2-by-2 block matrix, preserving |ClosedSemiNearRing|}
Square : ClosedSemiNearRing -> ClosedSemiNearRing
Square csnr = CSNR where
  open ClosedSemiNearRing csnr

  record S : Set where                            -- \structure{4.1}{Square matrix}
    constructor ⟨_,_,_,_⟩
    field
      s00  : s;  s01  : s
      s10  : s;  s11  : s
  infix 4 ⟨_,_,_,_⟩

  record U : Set where                            -- \structure{4.2}{Upper triangular matrix}
    constructor ⟨_,_,•,_⟩
    field
      uu00 : u;  us01  : s;
                 uu11  : u
  infix 4 ⟨_,_,•,_⟩

  _+S_  : S →  S → S
  _+S_  ⟨ a         ,  b         ,  c         ,  d         ⟩
        ⟨       a'  ,        b'  ,        c'  ,        d'  ⟩ =
        ⟨ a +s  a'  ,  b +s  b'  ,  c +s  c'  ,  d +s  d'  ⟩

  _*S_  : S → S → S
  _*S_  ⟨  a  , b ,
           c  , d ⟩  ⟨  a'  , b'  ,
                        c'  , d'  ⟩  =  ⟨  (a *s a')  +s  (b *s c')  ,  (a *s b')  +s  (b *s d')
                                        ,  (c *s a')  +s  (d *s c')  ,  (c *s b')  +s  (d *s d') ⟩

  infixl  6  _+S_
  infixl  7  _*S_

  zerS : S
  zerS = ⟨  zers , zers ,
            zers , zers ⟩

  _+U_  : U → U → U
  _+U_ ⟨ xl , xm ,•, xr ⟩ ⟨ yl , ym ,•, yr ⟩ = ⟨ xl +u yl , xm +s ym ,•, xr +u yr ⟩

  _*U_ : U → U → U
  _*U_  ⟨  xl  ,  xm
           ,•,    xr ⟩  ⟨  yl ,   ym
                           ,•,    yr ⟩  =  ⟨  xl *u yl  ,   xl u*s ym  +s  xm s*u yr
                                              ,•,           xr *u yr                  ⟩

  _≃S_ : S → S → Set
  _≃S_ ⟨ a , b , c , d ⟩ ⟨ a' , b' , c' , d' ⟩  =  (a ≃s a')  ×  (b ≃s b')
                                                ×  (c ≃s c')  ×  (d ≃s d')

  infix 4 _≃S_

  U2S : U → S
  U2S ⟨ uu00 , us01 ,•, uu11 ⟩ =  ⟨  u2s uu00  ,  us01      ,
                                     zers      ,  u2s uu11   ⟩

  reflS : {x : S} → x ≃S x                        -- \structure{4.3}{Laws}
  reflS =  refls , refls ,
           refls , refls

  symS : {i j : S} → i ≃S j → j ≃S i
  symS (p00 , p01 , p10 , p11) = ( syms p00 , syms p01 , syms p10 , syms p11 )

  transS : {i j k : S} →  i ≃S j  →  j ≃S k  →  i ≃S k
  transS  (p00 , p01 , p10 , p11) (q00 , q01 , q10 , q11) =
          ( transs p00 q00 , transs p01 q01 , transs p10 q10 , transs p11 q11 )

  assocS : (x y z : S) →  (x +S y) +S z  ≃S  x +S (y +S z)
  assocS  ⟨ x00  , x01  , x10  , x11 ⟩
          ⟨ y00  , y01  , y10  , y11 ⟩
          ⟨ z00  , z01  , z10  , z11 ⟩ =
          (  assocs x00  y00  z00  , assocs x01  y01  z01 ,
             assocs x10  y10  z10  , assocs x11  y11  z11 )

  _<+S>_ : {a1 a2 b1 b2 : S} →  a1 ≃S a2  →  b1 ≃S b2  →  a1 +S b1  ≃S  a2 +S b2
  _<+S>_  (p00 , p01 , p10 , p11) (q00 , q01 , q10 , q11) =
          (  (p00  <+> q00)  , (p01  <+> q01)  ,
             (p10  <+> q10)  , (p11  <+> q11)  )

  _<*S>_ : {x1 y1 x2 y2 : S} →  x1 ≃S x2  →  y1 ≃S y2  →  x1 *S y1  ≃S  x2 *S y2
  _<*S>_ (p00 , p01 , p10 , p11) (q00 , q01 , q10 , q11) =
         (  (p00  <*> q00) <+> (p01  <*> q10) , (p00  <*> q01) <+> (p01  <*> q11)  ,
            (p10  <*> q00) <+> (p11  <*> q10) , (p10  <*> q01) <+> (p11  <*> q11)  )

  swapMid : ∀ {a b c d}  →   (a +s b)  +s  (c +s d)
                         ≃s  (a +s c)  +s  (b +s d)

  swapMid {a} {b} {c} {d}
           =  begin
                (a +s b) +s (c +s d)
              ≈⟨ assocs _ _ _ ⟩
                 a +s (b +s (c +s d))
              ≈⟨ refls <+> sym (assocs _ _ _) ⟩
                 a +s ((b +s c) +s d)
              ≈⟨ refls <+> (comms _ _ <+> refls) ⟩
                a +s ((c +s b) +s d)
              ≈⟨ refls <+> (assocs _ _ _) ⟩
                a +s (c +s (b +s d))
              ≈⟨ sym (assocs _ _ _) ⟩
                (a +s c) +s (b +s d)
              ∎
     where open EqReasoning sSetoid

  distlS : (x y z : S) → x *S (y +S z) ≃S x *S y +S x *S z
  distlS _ _ _ =  distrHelp , distrHelp , distrHelp , distrHelp
     where  distrHelp : ∀ {a b c d e f}  →   a *s (b +s c)       +s  d *s (e +s f)
                                         ≃s  (a *s b +s d *s e)  +s (a *s c +s d *s f)
            distrHelp = transs (distl _ _ _ <+> distl _ _ _) swapMid

  distrS : (x y z : S) → (y +S z) *S x ≃S y *S x +S z *S x
  distrS _ _ _ = distrHelp , distrHelp , distrHelp , distrHelp
     where  distrHelp : ∀ {a b c d e f}  →  (a +s b) *s c       +s (d +s e) *s f
                                         ≃s (a *s c +s d *s f)  +s (b *s c +s e *s f)
            distrHelp = transs (distr _ _ _ <+> distr _ _ _) swapMid

  identityˡS : (x : S) →  zerS +S x  ≃S  x
  identityˡS ⟨ s00 , s01 , s10 , s11 ⟩ =  identityˡs s00 , identityˡs s01 , identityˡs s10 , identityˡs s11

  commS : (x y : S) →  x +S y ≃S y +S x
  commS  ⟨ x00 , x01 , x10 , x11 ⟩ ⟨ y00 , y01 , y10 , y11 ⟩ =  (comms x00 y00 , comms x01 y01 ,
                                                                 comms x10 y10 , comms x11 y11 )

  idemS : (x : S) → x +S x  ≃S  x
  idemS ⟨ x00 , x01 , x10 , x11 ⟩ = ( idem x00 , idem x01 , idem x10 , idem x11 )

  open import ZeroLemmas snr

  zeroˡS : LeftZero _≃S_ zerS _*S_
  zeroˡS ⟨ s00 , s01 , s10 , s11 ⟩ = ( zeroˡLemma s00 s10 , zeroˡLemma s01 s11 , zeroˡLemma s00 s10 , zeroˡLemma s01 s11)

  zeroʳS : RightZero _≃S_ zerS _*S_
  zeroʳS ⟨ s00 , s01 , s10 , s11 ⟩ = ( zeroʳLemma s00 s01 , zeroʳLemma s00 s01 , zeroʳLemma s10 s11 , zeroʳLemma s10 s11)

  isCommMonS : IsCommutativeMonoid _≃S_ _+S_ zerS
  isCommMonS = record {
     isSemigroup = record {
        isEquivalence  = record { refl = reflS; sym = symS; trans = transS };
        assoc          = assocS;
        ∙-cong         = _<+S>_ };
     identityˡ   = identityˡS;
     comm        = commS }

  SNR : SemiNearRingRecords.SemiNearRing
  SNR = record {
           s         = S;
           zers      = zerS;
           _+s_      = _+S_;
           _≃s_      = _≃S_;
           isCommMon = isCommMonS;
           _*s_      = _*S_;
           zeroˡ     = zeroˡS;
           zeroʳ     = zeroʳS;
           _<*>_     = _<*S>_;
           distr     = distrS;
           distl     = distlS;
           idem      = idemS
           }

  SNR2 : SemiNearRing2
  SNR2 = record {
           snr       = SNR ;
           u         = U;
           _+u_      = _+U_;
           _*u_      = _*U_;
           u2s       = U2S }

  _≃U_ : U → U → Set
  _≃U_ = SemiNearRing2._≃u_ SNR2

  _U*S_ : U → S → S
  _U*S_ = SemiNearRing2._u*s_ SNR2

  _S*U_ : S → U → S
  _S*U_ = SemiNearRing2._s*u_ SNR2

  congU :  ∀ {x1 x2 y1 y2 z1 z2} → x1 ≃u x2  →  y1 ≃s y2  →  z1 ≃u z2  →
           ⟨ x1 , y1 ,•, z1 ⟩ ≃U ⟨ x2 , y2 ,•, z2 ⟩
  congU p1 p2 p3 = (p1 , p2 , refls , p3)

  congS :  ∀ {x1 x2 y1 y2 z1 z2 w1 w2} →
           x1 ≃s x2  →  y1 ≃s y2  →  z1 ≃s z2  →  w1 ≃s w2  →
           ⟨ x1 , y1 , z1 , w1 ⟩ ≃S ⟨ x2 , y2 , z2 , w2 ⟩
  congS p1 p2 p3 p4 = (p1 , p2 , p3 , p4)

  QU = \ W C -> (W  +U  (C *U C)) ≃U C            -- \structure{4.4}{Lifting |Q| and its proof}

  entireQStep : ∀ W -> ∃ (QU W)
  entireQStep W = C , proof where
         C : U
         C = _

         open EqReasoning (SemiNearRing2.uSetoid SNR2)
         proof : (W  +U  (C *U C))  ≃U  C
         proof =  begin
                    (W  +U  (C *U C))
                  ≡⟨ refl ⟩  -- expand matrix components
                    let   ⟨ A   , Y   ,•, B    ⟩ = W
                          ⟨ A'  , Y'  ,•, B'   ⟩ = C in
                    ⟨ A , Y ,•, B ⟩  +U (⟨ A' , Y' ,•, B' ⟩ *U ⟨ A' , Y' ,•, B' ⟩)
                  ≡⟨ refl ⟩  -- expand definition of |*U|
                    ⟨ A , Y ,•, B ⟩  +U   ⟨ A' *u A'  ,  (A' u*s Y'  +s Y' s*u B')
                                                      ,•,  B' *u B' ⟩
                  ≡⟨ refl ⟩  -- by def. of |+U|
                    ⟨  A +u A' *u A'      ,     Y +s (A' u*s Y'  +s  Y' s*u B')
                                          ,•,   B +u B' *u B'  ⟩
                  ≈⟨ congU closureHasAll completionHasAll closureHasAll ⟩
                    ⟨ A' , Y' ,•, B' ⟩
                  ≡⟨ refl ⟩
                     C
                  ∎

  entireQStep2 : ∀ W -> ∃ (QU W)
  entireQStep2 W = C , proof where
         C : U

         C =  let   ⟨ A , Y ,•, B ⟩  = W
                    (A' , proofA)    = entireQ A
                    (B' , proofB)    = entireQ B
                    (Y' , proofY)    = entireL A' Y B'
              in    ⟨ A' , Y' ,•, B' ⟩

         open EqReasoning (SemiNearRing2.uSetoid SNR2)
         proof : (W  +U  (C *U C))  ≃U  C

         proof = congU closureHasAll completionHasAll closureHasAll

  _≤U_ = SemiNearRing2._≤u_  SNR2                 -- \structure{4.5}{Lifting orders and their properties}
  _≤S_ = SemiNearRing2._≤s_  SNR2
  closureIsLeastS : ∀ {W} -> LowerBound _≤U_ (QU W) (fun entireQStep W)
  closureIsLeastS  Z   QUWZ =
    let  ⟨ z00  , z01 ,•,     z11 ⟩  = Z      -- every matrix |Z|
         ( p00  , p01 , _ ,   p11)   = QUWZ   -- which satisfies |(QU W Z)|
         q10      = identityˡs zers
         q00      = closureIsLeast z00 p00    -- is bigger than |C = fun entireQStep W|
         q11      = closureIsLeast z11 p11
         vs01     = completionIsLeast _ _ _ z01 p01
         mono01   = completionMono q00 (≃sTo≤s refls) q11
    in  (  q00  , ≤s-trans mono01 vs01
        ,  q10  , q11 )

                                                  -- \structure{4.6}{Lifting the proof of |L|}
  entireLS : ∀ (A : U) (Y : S) (B : U) → ∃ (\ X → Y +S (A U*S X +S X S*U B) ≃S X)
  entireLS A Y B = X , proof where
    X : S
    X = _    -- filled in by unification with |Y +S (U2S A *S X +S X *S U2S B)|
    proof : Y +S (U2S A *S X +S X *S U2S B) ≃S X
    open EqReasoning (SemiNearRing2.sSetoid SNR2)
    proof =  -- continued below to fit the width of the paper (it is still in the |where| clause)

      begin
        (Y  +S  (A U*S X  +S  X S*U B) )
      ≡⟨ refl ⟩ -- name the components
        let  ⟨ a00 , a01 ,•, a11 ⟩      = A
             ⟨ b00 , b01 ,•, b11 ⟩      = B
             ⟨ y00 , y01 , y10 , y11 ⟩  = Y
             ⟨ x00 , x01 , x10 , x11 ⟩  = X
        in   Y  +S  (A U*S X  +S  X S*U B)

      ≡⟨ refl ⟩ -- expand |U*S| and |S*U| and use components
        let  AU*SX =  ⟨  a00 u*s x00      +s   a01  *s x10   , a00 u*s x01  +s a01    *s x11
                      ,  zers *s x00      +s   a11 u*s x10   , zers *s x01  +s a11   u*s x11 ⟩
             XS*UB =  ⟨  x00 s*u b00      +s   x01 *s zers   , x00 *s b01   +s x01   s*u b11
                      ,  x10 s*u b00      +s   x11 *s zers   , x10 *s b01   +s x11   s*u b11 ⟩
        in   Y +S (AU*SX  +S  XS*UB)

      ≡⟨ refl ⟩ -- Expand |≃S|, |+S| and collect components
        ⟨  y00   +s ( (a00   u*s  x00   +s   a01  *s x10)  +s (x00 s*u b00   +s x01   *s   zers) )
        ,  y01   +s ( (a00   u*s  x01   +s   a01  *s x11)  +s (x00  *s b01   +s x01  s*u   b11 ) )
        ,  y10   +s ( (zers  *s   x00   +s   a11 u*s x10)  +s (x10 s*u b00   +s x11   *s   zers) )
        ,  y11   +s ( (zers  *s   x01   +s   a11 u*s x11)  +s (x10  *s b01   +s x11  s*u   b11 ) ) ⟩

      ≈⟨ congS zeroLemma00 zeroLemma01 zeroLemma10 zeroLemma11 ⟩
         -- assoc. and comm. of +; zero absorption.
        ⟨  y00 +s a01 *s x10 +s                 (a00 u*s x00 +s x00 s*u b00)
        ,  y01 +s a01 *s x11 +s x00 *s b01 +s   (a00 u*s x01 +s x01 s*u b11)
        ,  y10 +s                               (a11 u*s x10 +s x10 s*u b00)
        ,  y11 +s x10 *s b01 +s                 (a11 u*s x11 +s x11 s*u b11) ⟩

      ≈⟨ congS  completionHasAll completionHasAll completionHasAll  completionHasAll ⟩
        ⟨  x00 , x01 , x10 , x11  ⟩
      ≡⟨ refl ⟩
        X
      ∎

  uniqueLS : SemiNearRing2.UniqueL SNR2           -- \structure{4.7}{Proofs for ordering |L|-solutions}
  uniqueLS (p00 , p01 , p10 , p11) (q00 , q01 , q10 , q11) =  eq00 , eq01 , eq10 , eq11
     where mutual
             s00 = congL (refls <+> (refls <*> sym eq10))
             s11 = congL (refls <+> (sym eq10 <*> refls))
             s01 = congL ((refls <+> (refls <*> sym eq11)) <+> (sym eq00 <*> refls))
             r10 =        trans (sym zeroLemma10) q10
             r00 = s00 (  trans (sym zeroLemma00) q00)
             r11 = s11 (  trans (sym zeroLemma11) q11)
             r01 = s01 (  trans (sym zeroLemma01) q01)
             eq10 = uniqueL (trans (sym zeroLemma10)  p10)  r10
             eq00 = uniqueL (trans (sym zeroLemma00)  p00)  r00
             eq11 = uniqueL (trans (sym zeroLemma11)  p11)  r11
             eq01 = uniqueL (trans (sym zeroLemma01)  p01)  r01

  completionMonoS :  ∀ {a a' y y' b b'} → a ≤U a'  →  y ≤S y'  →  b ≤U b'  →
                     proj₁ (entireLS a y b) ≤S proj₁ (entireLS a' y' b')
  completionMonoS  (p00 , p01 , p10 , p11) (q00 , q01 , q10 , q11)
                   (r00 , r01 , r10 , r11) = m00 , m01 , m10 , m11
     where  m10 = completionMono p11  q10 r00
            m00 = completionMono p00  (q00 [+] p01 [*] m10) r00
            m11 = completionMono p11  (q11 [+] m10 [*] r01) r11
            m01 = completionMono p00  (q01 [+] p01 [*] m11 [+] m00 [*] r01) r11

  congLS : SemiNearRing2.CongL SNR2
  congLS P Q = transS (symS P <+S> reflS) Q

  CSNR : ClosedSemiNearRing
  CSNR = record {
   snr2             = SNR2;
   entireQ          = entireQStep ;
   closureIsLeast   = closureIsLeastS ;
   entireL          = entireLS;
   uniqueL          = uniqueLS ;
   congL            = congLS ;
   completionMono   = completionMonoS }

module Knot where

--  open import Data.Nat
  OneByOne : SemiNearRing -> ClosedSemiNearRing
  OneByOne snr = record {
    snr2            = snr2;

    entireQ          = entireQBase;
    entireL          = entireLBase;
    closureIsLeast   = leastQBase;
    completionMono   = \ _ w<w' _ → w<w';
    uniqueL          = \p q → transs (syms p) (transs (zeroˡʳLemma _ _ _) (transs (syms (zeroˡʳLemma _ _ _)) q));
    congL            = \p q → transs (syms p <+> refls) q

                           }
    where  open SemiNearRing snr using (zers)
           snr2 = record {  snr = snr; u = ⊤;  _+u_ = \ _ _ → tt;
                            u2s = \ _ → zers;  _*u_ = \ _ _ → tt }

           open SemiNearRing snr using (s; _≃s_; refls; _+s_; _*s_; identityˡs; syms; transs; _<+>_)
           open SemiNearRing2 snr2 using (_+u_; _*u_; _≃u_)

           entireQBase : ∀ (w : ⊤) → ∃ \(c : ⊤)  →  w  +u  c *u c  ≃u  c
           entireQBase tt = _ , refls

           open SemiNearRing2 snr2 using (_s*u_; _u*s_)

           open import ZeroLemmas snr             -- \structure{5.1}{Base case for |L|}
           entireLBase : (a : ⊤) (y : s) (b : ⊤) → ∃ (\ x → y +s (a u*s x +s x s*u b) ≃s x)
           entireLBase tt y tt = y , zeroˡʳLemma y y y

           leastQBase = \ _ _ → identityˡs zers   -- \structure{5.2}{Base case for least |Q| }

  open import Data.Nat

  Mat : ℕ → SemiNearRing → ClosedSemiNearRing     -- \structure{6}{Top level recursion for matrices}
  Mat zero     el = OneByOne el
  Mat (suc n)  el = Square (Mat n el)

  Upper : ℕ → SemiNearRing → Set
  Upper n el = ClosedSemiNearRing.u (Mat n el)

                                                  -- \structure{6.1}{Top level algorithm extraction}
  valiantAlgorithm : (el : SemiNearRing) → ∀ n → Upper n el → Upper n el
  valiantAlgorithm el n u = ClosedSemiNearRing.closure (Mat n el) u

max_stars_repo_name: DSLsofMath/ValiantAgda

max_issues_repo_name: DSLsofMath/ValiantAgda

max_forks_repo_name: DSLsofMath/ValiantAgda


text:
module Any? where

open import Relation.Nullary using (¬_; Dec; yes; no)

open import lists using ([]; _∷_; Any; here; there; Decidable)

-- All?のAny版
Any? : ∀ {A : Set} {P : A → Set} → Decidable P → Decidable (Any P)
Any? P? []                                = no (λ ())
Any? P? (x ∷ xs) with P? x   | Any? P? xs
...                 | yes Px | _          = yes (here Px)
...                 | no _   | yes Pxs    = yes (there Pxs)
...                 | no ¬Px | no ¬Pxs    = no λ{ (here Px)   → ¬Px Px
                                                ; (there Pxs) → ¬Pxs Pxs }


text:
{-# NO_POSITIVITY_CHECK #-}
data D : Set
data D where
  d : (D → D) → D

data E : Set
{-# NO_POSITIVITY_CHECK #-}
data E where
  e : (E → E) → E

{-# NO_POSITIVITY_CHECK #-}
data F : Set
{-# NO_POSITIVITY_CHECK #-}
data F where
  e : (F → F) → F


text:
open import Agda.Builtin.Reflection

postulate
  A : Set
  B : A → Set

macro
  foo : Term → TC _
  foo m = bindTC getContext \ cxt →
          inContext cxt (unify m (quoteTerm A))

test : ∀ x → B x → Set
test x y = foo

max_forks_repo_name: Agda-zh/agda


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

open import HoTT
open import cohomology.Exactness
open import cohomology.FunctionOver
open import cohomology.ProductRepr
open import cohomology.Theory
open import cohomology.WedgeCofiber

{- For the cohomology group of a suspension ΣX, the group inverse has the
   explicit form Cⁿ(flip-susp) : Cⁿ(ΣX) → Cⁿ(ΣX). The proof is via the
   hexagon lemma, with the diagram

                Cⁿ(X)
                  |
                fold*
         winl*    ↓    winr*
   Cⁿ(X) ←–––– Cⁿ(X∨X) ––––→ Cⁿ(X)
                  |
                diff*
                  ↓
                Cⁿ(X)

-}

module cohomology.InverseInSusp {i} (CT : CohomologyTheory i)
  (n : ℤ) {X : Ptd i} where

open CohomologyTheory CT
open import cohomology.ConstantFunction CT
open import cohomology.Wedge CT

private
  open WedgeCofiber X X
  open CSusp^Wedge n X X 1

  module Diff = SuspensionRec (fst X)
    (north (X ∨ X)) (north (X ∨ X))
    (λ x → merid _ (winl x) ∙ ! (merid _ (winr x)))

  diff = Diff.f

  ⊙diff : fst (⊙Susp X ⊙→ ⊙Susp (X ⊙∨ X))
  ⊙diff = (diff , idp)

  module HL = HexagonLemma
    (CF-hom n (⊙susp-fmap ⊙fold))
    (CF-hom n ⊙diff)
    (app= $ ap GroupHom.f $
      ! (CF-comp n (⊙susp-fmap ⊙fold) ⊙diff)
      ∙ ap (CF-hom n)
           (⊙λ= (Suspension-elim _ idp idp
                     (λ x → ↓-app=cst-from-square $ vert-degen-square $
                       ap-∘ (susp-fmap fold) diff (merid _ x)
                       ∙ ap (ap (susp-fmap fold)) (Diff.glue-β x)
                       ∙ ap-∙ (susp-fmap fold) (merid _ (winl x))
                                               (! (merid _ (winr x)))
                       ∙ ap2 _∙_ (SuspFmap.glue-β fold (winl x))
                                 (ap-! (susp-fmap fold) (merid _ (winr x))
                                  ∙ ap ! (SuspFmap.glue-β fold (winr x)))
                       ∙ !-inv-r (merid _ x)))
                   idp)
      ∙ CF-cst n)

CF-flip : CF-hom n (⊙flip-susp X) == inv-hom _ (C-abelian n (⊙Susp X))
CF-flip =
  ! C-right-reduce
  ∙ (hom= _ _ $ λ= $ ! ∘ HL.inv₁)
  ∙ ap (λ φ → inv-hom _ (C-abelian n (⊙Susp X)) ∘ᴳ φ) C-left-reduce
  where
  {- Lemmas are all just reducing compositions -}

  β : {A B C D : Type i} (h : C → D) (g : B → C) (f : A → B) (a : A)
    → ap (susp-fmap h ∘ susp-fmap g ∘ susp-fmap f) (merid _ a)
      == merid _ (h (g (f a)))
  β h g f a =
      ap-∘ (susp-fmap h ∘ susp-fmap g) (susp-fmap f) (merid _ a)
    ∙ ap (ap (susp-fmap h ∘ susp-fmap g)) (SuspFmap.glue-β f a)
    ∙ ap-∘ (susp-fmap h) (susp-fmap g) (merid _ (f a))
    ∙ ap (ap (susp-fmap h)) (SuspFmap.glue-β g (f a))
    ∙ SuspFmap.glue-β h (g (f a))

  left-β = β (fold {X = X}) winl projl
  right-β = β (fold {X = X}) winr projr

  left-reduce : ((⊙susp-fmap {Y = X} ⊙fold
                 ⊙∘ ⊙susp-fmap ⊙winl)
                 ⊙∘ ⊙susp-fmap ⊙projl) ⊙∘ ⊙diff
                == ⊙idf (⊙Susp X)
  left-reduce = ⊙λ=
    (Suspension-elim (fst X) idp (merid _ (snd X))
      (λ x → ↓-='-from-square $
        (ap-∘ (susp-fmap fold ∘ susp-fmap winl ∘ susp-fmap projl)
           diff (merid _ x)
         ∙ ap (ap (susp-fmap fold ∘ susp-fmap winl ∘ susp-fmap projl))
             (Diff.glue-β x)
         ∙ ap-∙ (susp-fmap fold ∘ susp-fmap winl ∘ susp-fmap projl)
               (merid _ (winl x)) (! (merid _ (winr x)))
         ∙ (left-β (winl x)
           ∙2 (ap-! (susp-fmap fold ∘ susp-fmap winl ∘ susp-fmap projl)
                 (merid _ (winr x))
               ∙ ap ! (left-β (winr x)))))
        ∙v⊡ (vid-square {p = merid _ x} ⊡h rt-square (merid _ (snd X)))
        ⊡v∙ (∙-unit-r _ ∙ ! (ap-idf (merid _ x)))))
    idp

  right-reduce : ((⊙susp-fmap {Y = X} ⊙fold
                 ⊙∘ ⊙susp-fmap ⊙winr)
                 ⊙∘ ⊙susp-fmap ⊙projr) ⊙∘ ⊙diff
                == ⊙flip-susp X
  right-reduce = ⊙λ=
    (Suspension-elim (fst X) (merid _ (snd X)) idp
      (λ x → ↓-='-from-square $
        (ap-∘ (susp-fmap fold ∘ susp-fmap winr ∘ susp-fmap projr)
           diff (merid _ x)
         ∙ ap (ap (susp-fmap fold ∘ susp-fmap winr ∘ susp-fmap projr))
             (Diff.glue-β x)
         ∙ ap-∙ (susp-fmap fold ∘ susp-fmap winr ∘ susp-fmap projr)
               (merid _ (winl x)) (! (merid _ (winr x)))
         ∙ (right-β (winl x)
           ∙2 (ap-! (susp-fmap fold ∘ susp-fmap winr ∘ susp-fmap projr)
                 (merid _ (winr x))
               ∙ ap ! (right-β (winr x)))))
        ∙v⊡ ((lt-square (merid _ (snd X)) ⊡h vid-square {p = ! (merid _ x)}))
        ⊡v∙ ! (FlipSusp.glue-β x)))
    (! (!-inv-r (merid _ (snd X))))

  C-β : {Y Z U V W : Ptd i} (k : fst (V ⊙→ W))
    (h : fst (U ⊙→ V)) (g : fst (Z ⊙→ U)) (f : fst (Y ⊙→ Z))
    → CF-hom n f ∘ᴳ CF-hom n g ∘ᴳ CF-hom n h ∘ᴳ CF-hom n k
      == CF-hom n (((k ⊙∘ h) ⊙∘ g) ⊙∘ f)
  C-β k h g f =
    ap (λ w → CF-hom n f ∘ᴳ CF-hom n g ∘ᴳ w) (! (CF-comp n k h))
    ∙ ap (λ w → CF-hom n f ∘ᴳ w) (! (CF-comp n (k ⊙∘ h) g))
    ∙ ! (CF-comp n ((k ⊙∘ h) ⊙∘ g) f)

  C-left-reduce = C-β (⊙susp-fmap ⊙fold) (⊙susp-fmap ⊙winl)
                      (⊙susp-fmap ⊙projl) ⊙diff
                  ∙ ap (CF-hom n) left-reduce ∙ CF-ident n

  C-right-reduce = C-β (⊙susp-fmap ⊙fold) (⊙susp-fmap ⊙winr)
                       (⊙susp-fmap ⊙projr) ⊙diff
                   ∙ ap (CF-hom n) right-reduce

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
------------------------------------------------------------------------
-- The identity monad
------------------------------------------------------------------------

module Category.Monad.Identity where

open import Category.Monad

Identity : Set → Set
Identity A = A

IdentityMonad : RawMonad Identity
IdentityMonad = record
  { return = λ x → x
  ; _>>=_  = λ x f → f x
  }

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module Numeral.Sign.Proofs where

open import Logic.IntroInstances
open import Numeral.Sign
open import Numeral.Sign.Oper
open import Numeral.Sign.Oper0 renaming (_+_ to _+₀_ ; _⨯_ to _⨯₀_ ; −_ to −₀_)
open import Relator.Equals
open import Relator.Equals.Proofs.Equivalence
open import Structure.Function.Domain
open import Structure.Operator.Properties
open import Structure.Setoid hiding (_≢_)

instance
  [−|+]-equiv : Equiv(−|+)
  [−|+]-equiv = [≡]-equiv

instance
  [−|0|+]-equiv : Equiv(−|0|+)
  [−|0|+]-equiv = [≡]-equiv

instance
  [+]-commutativity : Commutativity(_+_)
  Commutativity.proof [+]-commutativity {➕} {➕} = [≡]-intro
  Commutativity.proof [+]-commutativity {➕} {➖} = [≡]-intro
  Commutativity.proof [+]-commutativity {➖} {➕} = [≡]-intro
  Commutativity.proof [+]-commutativity {➖} {➖} = [≡]-intro

instance
  [⨯]-commutativity : Commutativity(_⨯_)
  Commutativity.proof [⨯]-commutativity {➕} {➕} = [≡]-intro
  Commutativity.proof [⨯]-commutativity {➕} {➖} = [≡]-intro
  Commutativity.proof [⨯]-commutativity {➖} {➕} = [≡]-intro
  Commutativity.proof [⨯]-commutativity {➖} {➖} = [≡]-intro

instance
  [+₀]-identityₗ : Identityₗ(_+₀_)(𝟎)
  Identityₗ.proof [+₀]-identityₗ {➕} = [≡]-intro
  Identityₗ.proof [+₀]-identityₗ {𝟎} = [≡]-intro
  Identityₗ.proof [+₀]-identityₗ {➖} = [≡]-intro

instance
  [+₀]-identityᵣ : Identityᵣ(_+₀_)(𝟎)
  Identityᵣ.proof [+₀]-identityᵣ {➕} = [≡]-intro
  Identityᵣ.proof [+₀]-identityᵣ {𝟎} = [≡]-intro
  Identityᵣ.proof [+₀]-identityᵣ {➖} = [≡]-intro

instance
  [+₀]-identity : Identity(_+₀_)(𝟎)
  [+₀]-identity = intro

instance
  [+₀]-inverseFunctionₗ : InverseFunctionₗ(_+₀_)(−₀_)
  InverseFunctionₗ.proof [+₀]-inverseFunctionₗ {➕} = [≡]-intro
  InverseFunctionₗ.proof [+₀]-inverseFunctionₗ {𝟎} = [≡]-intro
  InverseFunctionₗ.proof [+₀]-inverseFunctionₗ {➖} = [≡]-intro

instance
  [+₀]-inverseFunctionᵣ : InverseFunctionᵣ(_+₀_)(−₀_)
  InverseFunctionᵣ.proof [+₀]-inverseFunctionᵣ {➕} = [≡]-intro
  InverseFunctionᵣ.proof [+₀]-inverseFunctionᵣ {𝟎} = [≡]-intro
  InverseFunctionᵣ.proof [+₀]-inverseFunctionᵣ {➖} = [≡]-intro

instance
  [+₀]-inverseFunction : InverseFunction(_+₀_)(−₀_)
  [+₀]-inverseFunction = intro

instance
  [⨯₀]-commutativity : Commutativity(_⨯₀_)
  Commutativity.proof [⨯₀]-commutativity {➕} {➕} = [≡]-intro
  Commutativity.proof [⨯₀]-commutativity {➕} {𝟎} = [≡]-intro
  Commutativity.proof [⨯₀]-commutativity {➕} {➖} = [≡]-intro
  Commutativity.proof [⨯₀]-commutativity {𝟎} {➕} = [≡]-intro
  Commutativity.proof [⨯₀]-commutativity {𝟎} {𝟎} = [≡]-intro
  Commutativity.proof [⨯₀]-commutativity {𝟎} {➖} = [≡]-intro
  Commutativity.proof [⨯₀]-commutativity {➖} {➕} = [≡]-intro
  Commutativity.proof [⨯₀]-commutativity {➖} {𝟎} = [≡]-intro
  Commutativity.proof [⨯₀]-commutativity {➖} {➖} = [≡]-intro

instance
  [⨯₀]-associativity : Associativity(_⨯₀_)
  Associativity.proof [⨯₀]-associativity {➕} {➕} {➕} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➕} {➕} {𝟎} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➕} {➕} {➖} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➕} {𝟎} {➕} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➕} {𝟎} {𝟎} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➕} {𝟎} {➖} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➕} {➖} {➕} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➕} {➖} {𝟎} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➕} {➖} {➖} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {𝟎} {➕} {➕} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {𝟎} {➕} {𝟎} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {𝟎} {➕} {➖} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {𝟎} {𝟎} {➕} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {𝟎} {𝟎} {𝟎} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {𝟎} {𝟎} {➖} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {𝟎} {➖} {➕} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {𝟎} {➖} {𝟎} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {𝟎} {➖} {➖} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➖} {➕} {➕} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➖} {➕} {𝟎} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➖} {➕} {➖} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➖} {𝟎} {➕} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➖} {𝟎} {𝟎} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➖} {𝟎} {➖} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➖} {➖} {➕} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➖} {➖} {𝟎} = [≡]-intro
  Associativity.proof [⨯₀]-associativity {➖} {➖} {➖} = [≡]-intro

instance
  [⨯₀]-absorberₗ : Absorberₗ(_⨯₀_)(𝟎)
  Absorberₗ.proof [⨯₀]-absorberₗ {➕} = [≡]-intro
  Absorberₗ.proof [⨯₀]-absorberₗ {𝟎} = [≡]-intro
  Absorberₗ.proof [⨯₀]-absorberₗ {➖} = [≡]-intro

instance
  [⨯₀]-absorberᵣ : Absorberᵣ(_⨯₀_)(𝟎)
  Absorberᵣ.proof [⨯₀]-absorberᵣ {➕} = [≡]-intro
  Absorberᵣ.proof [⨯₀]-absorberᵣ {𝟎} = [≡]-intro
  Absorberᵣ.proof [⨯₀]-absorberᵣ {➖} = [≡]-intro

instance
  [⨯₀]-absorber : Absorber(_⨯₀_)(𝟎)
  [⨯₀]-absorber = intro

instance
  [⨯]-identityₗ : Identityₗ(_⨯_)(➕)
  Identityₗ.proof [⨯]-identityₗ {➕} = [≡]-intro
  Identityₗ.proof [⨯]-identityₗ {➖} = [≡]-intro

instance
  [⨯]-identityᵣ : Identityᵣ(_⨯_)(➕)
  Identityᵣ.proof [⨯]-identityᵣ {➕} = [≡]-intro
  Identityᵣ.proof [⨯]-identityᵣ {➖} = [≡]-intro

instance
  [⨯]-identity : Identity(_⨯_)(➕)
  [⨯]-identity = intro

instance
  [−]-involution : Involution(−_)
  Involution.proof [−]-involution {➕} = [≡]-intro
  Involution.proof [−]-involution {➖} = [≡]-intro

[−]-no-fixpoints : ∀{s} → (− s ≢ s)
[−]-no-fixpoints {➕} ()
[−]-no-fixpoints {➖} ()

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Structure.Operator.Ring.Homomorphism where

import      Lvl
open import Logic
open import Logic.Predicate
open import Structure.Function
open import Structure.Function.Multi
open import Structure.Setoid
open import Structure.Operator.Ring
open import Type

record Homomorphism
  {ℓ₁ ℓ₂ ℓₑ₁ ℓₑ₂}
  {X : Type{ℓ₁}} ⦃ _ : Equiv{ℓₑ₁}(X) ⦄ {_+X_ _⋅X_ : X → X → X} (structureₗ : Ring(_+X_)(_⋅X_))
  {Y : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(Y) ⦄ {_+Y_ _⋅Y_ : Y → Y → Y} (structureᵣ : Ring(_+Y_)(_⋅Y_))
  (f : X → Y)
  : Stmt{ℓ₁ Lvl.⊔ ℓₑ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓₑ₂} where

  constructor intro

  𝟏ₗ = Ring.𝟏(structureₗ)
  𝟏ᵣ = Ring.𝟏(structureᵣ)

  field
    ⦃ function ⦄     : Function(f)
    ⦃ preserve-[+] ⦄ : Preserving₂(f)(_+X_)(_+Y_)
    ⦃ preserve-[⋅] ⦄ : Preserving₂(f)(_⋅X_)(_⋅Y_)
    ⦃ preserve-𝟏 ⦄   : Preserving₀(f)(𝟏ₗ)(𝟏ᵣ)

record Antihomomorphism
  {ℓ₁ ℓ₂ ℓₑ₁ ℓₑ₂}
  {X : Type{ℓ₁}} ⦃ _ : Equiv{ℓₑ₁}(X) ⦄ {_+X_ _⋅X_ : X → X → X} (structureₗ : Ring(_+X_)(_⋅X_))
  {Y : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(Y) ⦄ {_+Y_ _⋅Y_ : Y → Y → Y} (structureᵣ : Ring(_+Y_)(_⋅Y_))
  (f : X → Y)
  : Stmt{ℓ₁ Lvl.⊔ ℓₑ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓₑ₂} where

  constructor intro

  𝟏ₗ = Ring.𝟏(structureₗ)
  𝟏ᵣ = Ring.𝟏(structureᵣ)

  field
    ⦃ function ⦄         : Function(f)
    ⦃ preserve-[+] ⦄     : Preserving₂(f)(_+X_)(_+Y_)
    ⦃ antipreserve-[⋅] ⦄ : ∀{x y} → (f(x ⋅X y) ≡ f(y) ⋅Y f(x))
    ⦃ preserve-𝟏 ⦄       : Preserving₀(f)(𝟏ₗ)(𝟏ᵣ)

_→ʳⁱⁿᵍ_ : ∀{ℓₗ ℓₗₑ ℓᵣ ℓᵣₑ} → RingObject{ℓₗ}{ℓₗₑ} → RingObject{ℓᵣ}{ℓᵣₑ} → Type
A →ʳⁱⁿᵍ B = ∃(Homomorphism(RingObject.ring A)(RingObject.ring B))