text:
{-# OPTIONS --type-in-type #-}
open import Data.Unit
open import Data.Product hiding ( curry ; uncurry )
open import Data.List hiding ( concat )
open import Data.String
open import Relation.Binary.PropositionalEquality
module Spire.Examples.PropositionalLevDesc where

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

Label : Set
Label = String

Enum : Set
Enum = List Label

data Tag : Enum → Set where
  here : ∀{l E} → Tag (l ∷ E)
  there : ∀{l E} → Tag E → Tag (l ∷ E)

Cases : (E : Enum) (P : Tag E → Set) → Set
Cases [] P = ⊤
Cases (l ∷ E) P = P here × Cases E λ t → P (there t)

case : (E : Enum) (P : Tag E → Set) (cs : Cases E P) (t : Tag E) → P t
case (l ∷ E) P (c , cs) here = c
case (l ∷ E) P (c , cs) (there t) = case E (λ t → P (there t)) cs t

UncurriedCases : (E : Enum) (P : Tag E → Set) (X : Set)
  → Set
UncurriedCases E P X = Cases E P → X

CurriedCases : (E : Enum) (P : Tag E → Set) (X : Set)
  → Set
CurriedCases [] P X = X
CurriedCases (l ∷ E) P X = P here → CurriedCases E (λ t → P (there t)) X

curryCases : (E : Enum) (P : Tag E → Set) (X : Set)
  (f : UncurriedCases E P X) → CurriedCases E P X
curryCases [] P X f = f tt
curryCases (l ∷ E) P X f = λ c → curryCases E (λ t → P (there t)) X (λ cs → f (c , cs))

uncurryCases : (E : Enum) (P : Tag E → Set) (X : Set)
  (f : CurriedCases E P X) → UncurriedCases E P X
uncurryCases [] P X x tt = x
uncurryCases (l ∷ E) P X f (c , cs) = uncurryCases E (λ t → P (there t)) X (f c) cs

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

data Desc (I : Set) : Set₁ where
  `End : (i : I) → Desc I
  `Rec : (i : I) (D : Desc I) → Desc I
  `Arg : (A : Set) (B : A → Desc I) → Desc I
  `RecFun : (A : Set) (B : A → I) (D : Desc I) → Desc I

ISet : Set → Set₁
ISet I = I → Set

El : (I : Set) (D : Desc I) (X : ISet I) → ISet I
El I (`End j) X i = j ≡ i
El I (`Rec j D) X i = X j × El I D X i
El I (`Arg A B) X i = Σ A (λ a → El I (B a) X i)
El I (`RecFun A B D) X i = ((a : A) → X (B a)) × El I D X i

Hyps : (I : Set) (D : Desc I) (X : ISet I) (P : (i : I) → X i → Set) (i : I) (xs : El I D X i) → Set
Hyps I (`End j) X P i q = ⊤
Hyps I (`Rec j D) X P i (x , xs) = P j x × Hyps I D X P i xs
Hyps I (`Arg A B) X P i (a , b) = Hyps I (B a) X P i b
Hyps I (`RecFun A B D) X P i (f , xs) = ((a : A) → P (B a) (f a)) × Hyps I D X P i xs

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

TagDesc : (I : Set) → Set
TagDesc I = Σ Enum (λ E → Cases E (λ _ → Desc I))

toCase : (I : Set) (E,cs : TagDesc I) → Tag (proj₁ E,cs) → Desc I
toCase I (E , cs) = case E (λ _ → Desc I) cs

toDesc : (I : Set) → TagDesc I → Desc I
toDesc I (E , cs) = `Arg (Tag E) (toCase I (E , cs))

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

UncurriedEl : (I : Set) (D : Desc I) (X : ISet I) → Set
UncurriedEl I D X = {i : I} → El I D X i → X i

CurriedEl : (I : Set) (D : Desc I) (X : ISet I) → Set
CurriedEl I (`End i) X = X i
CurriedEl I (`Rec j D) X = (x : X j) → CurriedEl I D X
CurriedEl I (`Arg A B) X = (a : A) → CurriedEl I (B a) X
CurriedEl I (`RecFun A B D) X = ((a : A) → X (B a)) → CurriedEl I D X

curryEl : (I : Set) (D : Desc I) (X : ISet I)
  (cn : UncurriedEl I D X) → CurriedEl I D X
curryEl I (`End i) X cn = cn refl
curryEl I (`Rec i D) X cn = λ x → curryEl I D X (λ xs → cn (x , xs))
curryEl I (`Arg A B) X cn = λ a → curryEl I (B a) X (λ xs → cn (a , xs))
curryEl I (`RecFun A B D) X cn = λ f → curryEl I D X (λ xs → cn (f , xs))

uncurryEl : (I : Set) (D : Desc I) (X : ISet I)
  (cn : CurriedEl I D X) → UncurriedEl I D X
uncurryEl I (`End i) X cn refl = cn
uncurryEl I (`Rec i D) X cn (x , xs) = uncurryEl I D X (cn x) xs
uncurryEl I (`Arg A B) X cn (a , xs) = uncurryEl I (B a) X (cn a) xs
uncurryEl I (`RecFun A B D) X cn (f , xs) = uncurryEl I D X (cn f) xs

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

CasesD : (I : Set) (E : Enum) → Set
CasesD I E = Cases E (λ _ → Desc I)

Args : (I : Set) (E : Enum) (t : Tag E) (cs : CasesD I E) → Desc I
Args I E t cs = case E (λ _ → Desc I) cs t

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

data μ (I : Set) (E : Enum) (cs : CasesD I E) : I → Set where
  con : (t : Tag E) → UncurriedEl I (Args I E t cs) (μ I E cs)

con2 : (I : Set) (E : Enum) (cs : CasesD I E) (t : Tag E)
  → CurriedEl I (Args I E t cs) (μ I E cs)
con2 I E cs t = curryEl I (Args I E t cs) (μ I E cs) (con t)

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

UncurriedHyps : (I : Set) (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : {i : I} → El I D X i → X i)
  → Set
UncurriedHyps I D X P cn =
  (i : I) (xs : El I D X i) → Hyps I D X P i xs → P i (cn xs)

CurriedHyps : (I : Set) (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedEl I D X)
  → Set
CurriedHyps I (`End i) X P cn =
  P i (cn refl)
CurriedHyps I (`Rec i D) X P cn =
  (x : X i) → P i x → CurriedHyps I D X P (λ xs → cn (x , xs))
CurriedHyps I (`Arg A B) X P cn =
  (a : A) → CurriedHyps I (B a) X P (λ xs → cn (a , xs))
CurriedHyps I (`RecFun A B D) X P cn =
  (f : (a : A) → X (B a)) (ihf : (a : A) → P (B a) (f a)) → CurriedHyps I D X P (λ xs → cn (f , xs))

curryHyps : (I : Set) (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedEl I D X)
  (pf : UncurriedHyps I D X P cn)
  → CurriedHyps I D X P cn
curryHyps I (`End i) X P cn pf =
  pf i refl tt
curryHyps I (`Rec i D) X P cn pf =
  λ x ih → curryHyps I D X P (λ xs → cn (x , xs)) (λ i xs ihs → pf i (x , xs) (ih , ihs))
curryHyps I (`Arg A B) X P cn pf =
  λ a → curryHyps I (B a) X P (λ xs → cn (a , xs)) (λ i xs ihs → pf i (a , xs) ihs)
curryHyps I (`RecFun A B D) X P cn pf =
  λ f ihf → curryHyps I D X P (λ xs → cn (f , xs)) (λ i xs ihs → pf i (f , xs) (ihf , ihs))

uncurryHyps : (I : Set) (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedEl I D X)
  (pf : CurriedHyps I D X P cn)
  → UncurriedHyps I D X P cn
uncurryHyps I (`End .i) X P cn pf i refl tt =
  pf
uncurryHyps I (`Rec j D) X P cn pf i (x , xs) (ih , ihs) =
  uncurryHyps I D X P (λ ys → cn (x , ys)) (pf x ih) i xs ihs
uncurryHyps I (`Arg A B) X P cn pf i (a , xs) ihs =
  uncurryHyps I (B a) X P (λ ys → cn (a , ys)) (pf a) i xs ihs
uncurryHyps I (`RecFun A B D) X P cn pf i (f , xs) (ihf , ihs) =
  uncurryHyps I D X P (λ ys → cn (f , ys)) (pf f ihf) i xs ihs

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

ind :
  (I : Set)
  (E : Enum)
  (cs : CasesD I E)
  (P : (i : I) → μ I E cs i → Set)
  (pcon : (t : Tag E) → UncurriedHyps I (Args I E t cs) (μ I E cs) P (con t))
  (i : I)
  (x : μ I E cs i)
  → P i x

hyps :
  (I : Set)
  (E : Enum)
  (cs : CasesD I E)
  (P : (i : I) → μ I E cs i → Set)
  (pcon : (t : Tag E) → UncurriedHyps I (Args I E t cs) (μ I E cs) P (con t))
  (D : Desc I)
  (i : I)
  (xs : El I D (μ I E cs) i)
  → Hyps I D (μ I E cs) P i xs

ind I E cs P pcon i (con t as) = pcon t i as (hyps I E cs P pcon (Args I E t cs) i as)

hyps I E cs P pcon (`End j) i q = tt
hyps I E cs P pcon (`Rec j A) i (x , xs) = ind I E cs P pcon j x , hyps I E cs P pcon A i xs
hyps I E cs P pcon (`Arg A B) i (a , b) = hyps I E cs P pcon (B a) i b
hyps I E cs P pcon (`RecFun A B D) i (f , xs) = (λ a → ind I E cs P pcon (B a) (f a)) , hyps I E cs P pcon D i xs

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

ind2 :
  (I : Set)
  (E : Enum)
  (cs : CasesD I E)
  (P : (i : I) → μ I E cs i → Set)
  (pcon : (t : Tag E) → CurriedHyps I (Args I E t cs) (μ I E cs) P (con t))
  (i : I)
  (x : μ I E cs i)
  → P i x
ind2 I E cs P pcon i x =
  ind I E cs P (λ t → uncurryHyps I (Args I E t cs) (μ I E cs) P (con t) (pcon t)) i x

elim :
  (I : Set)
  (E : Enum)
  (cs : CasesD I E)
  (P : (i : I) → μ I E cs i → Set)
  → let
    Q = λ t → CurriedHyps I (Args I E t cs) (μ I E cs) P (con t)
    X = (i : I) (x : μ I E cs i) → P i x
  in UncurriedCases E Q X
elim I E cs P ds i x =
  let Q = λ t → CurriedHyps I (Args I E t cs) (μ I E cs) P (con t)
  in ind2 I E cs P (case E Q ds) i x

elim2 :
  (I : Set)
  (E : Enum)
  (cs : CasesD I E)
  (P : (i : I) → μ I E cs i → Set)
  → let
    Q = λ t → CurriedHyps I (Args I E t cs) (μ I E cs) P (con t)
    X = (i : I) (x : μ I E cs i) → P i x
  in CurriedCases E Q X
elim2 I E cs P =
  let
    Q = λ t → CurriedHyps I (Args I E t cs) (μ I E cs) P (con t)
    X = (i : I) (x : μ I E cs i) → P i x
  in curryCases E Q X (elim I E cs P)

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

ℕT : Enum
ℕT = "zero" ∷ "suc" ∷ []

VecT : Enum
VecT = "nil" ∷ "cons" ∷ []

ℕD : CasesD ⊤ ℕT
ℕD =
    `End tt
  , `Rec tt (`End tt)
  , tt

ℕ : ⊤ → Set
ℕ = μ ⊤ ℕT ℕD

zero : ℕ tt
zero = con here refl

suc : ℕ tt → ℕ tt
suc n = con (there here) (n , refl)

zero2 : ℕ tt
zero2 = con2 ⊤ ℕT ℕD here

suc2 : ℕ tt → ℕ tt
suc2 = con2 ⊤ ℕT ℕD (there here)

VecD : (A : Set) → CasesD (ℕ tt) VecT
VecD A =
    `End zero
  , `Arg (ℕ tt) (λ n → `Arg A λ _ → `Rec n (`End (suc n)))
  , tt

Vec : (A : Set) (n : ℕ tt) → Set
Vec A n = μ (ℕ tt) VecT (VecD A) n

nil : (A : Set) → Vec A zero
nil A = con here refl

cons : (A : Set) (n : ℕ tt) (x : A) (xs : Vec A n) → Vec A (suc n)
cons A n x xs = con (there here) (n , x , xs , refl)

nil2 : (A : Set) → Vec A zero
nil2 A = con2 (ℕ tt) VecT (VecD A) here

cons2 : (A : Set) (n : ℕ tt) (x : A) (xs : Vec A n) → Vec A (suc n)
cons2 A = con2 (ℕ tt) VecT (VecD A) (there here)

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

module GenericEliminator where

  add : ℕ tt → ℕ tt → ℕ tt
  add = elim2 ⊤ ℕT ℕD _
    (λ n → n)
    (λ m ih n → suc (ih n))
    tt

  mult : ℕ tt → ℕ tt → ℕ tt
  mult = elim2 ⊤ ℕT ℕD _
    (λ n → zero)
    (λ m ih n → add n (ih n))
    tt

  append : (A : Set) (m : ℕ tt) (xs : Vec A m) (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)
  append A = elim2 (ℕ tt) VecT (VecD A) _
    (λ n ys → ys)
    (λ m x xs ih n ys → cons A (add m n) x (ih n ys))

  concat : (A : Set) (m n : ℕ tt) (xss : Vec (Vec A m) n) → Vec A (mult n m)
  concat A m = elim2 (ℕ tt) VecT (VecD (Vec A m)) _
    (nil A)
    (λ n xs xss ih → append A m xs (mult n m) ih)

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

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


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

module FinEquivTypeEquiv where

-- The goal is to establish that finite sets and equivalences form a
-- commutative semiring.

import Level using (zero)

open import Data.Nat using (ℕ; _+_; _*_)
open import Data.Fin using (Fin)

open import Relation.Binary using (IsEquivalence)
open import Algebra using (CommutativeSemiring)
open import Algebra.Structures
  using (IsSemigroup; IsCommutativeMonoid; IsCommutativeSemiring)

open import Equiv using (_≃_; id≃; sym≃; trans≃; _●_; _⊎≃_; _×≃_)
open import TypeEquiv
  using (assocl₊equiv; unite₊equiv; unite₊′equiv; swap₊equiv;
         unite⋆equiv; unite⋆′equiv; swap⋆equiv; assocl⋆equiv;
         distzequiv; distzrequiv; distequiv; distlequiv)

open import FinEquivPlusTimes using (F0≃⊥; module Plus; Fin1≃⊤; module Times)
open Plus using (+≃⊎; ⊎≃+)
open Times using (*≃×; ×≃*)

------------------------------------------------------------------------------
-- This is the relation we are interested in showing is a commutative
-- semiring.

_fin≃_ : (m n : ℕ) → Set
m fin≃ n = Fin m ≃ Fin n

------------------------------------------------------------------------------
-- Additive monoid

module PlusE where

  infix 9 _+F_

  -- additive monoid equivalences

  -- unite+

  unite+ : {m : ℕ} → Fin (0 + m) ≃ Fin m
  unite+ = unite₊equiv ● F0≃⊥ ⊎≃ id≃ ● +≃⊎

  -- and on the other side as well

  unite+r : {m : ℕ} → Fin (m + 0) ≃ Fin m
  unite+r = unite₊′equiv ● id≃ ⊎≃ F0≃⊥ ● +≃⊎

  -- swap₊

  swap+ : {m n : ℕ} → Fin (m + n) ≃ Fin (n + m)
  swap+ {m} = ⊎≃+ ● swap₊equiv ● +≃⊎ {m}

  -- associativity

  assocl+ : {m n o : ℕ} → Fin (m + (n + o)) ≃ Fin ((m + n) + o)
  assocl+ {m} = ⊎≃+ ● ⊎≃+ ⊎≃ id≃ ● assocl₊equiv ● id≃ ⊎≃ +≃⊎ ● +≃⊎ {m}

  -- congruence

  _+F_ : {m n o p : ℕ} → (Fin m ≃ Fin n) → (Fin o ≃ Fin p) →
              Fin (m + o) ≃ Fin (n + p)
  Fm≃Fn +F Fo≃Fp = ⊎≃+ ● Fm≃Fn ⊎≃ Fo≃Fp ● +≃⊎

  uniti+ : {m : ℕ} → Fin m ≃ Fin (0 + m)
  uniti+ = sym≃ unite+

  uniti+r : {m : ℕ} → Fin m ≃ Fin (m + 0)
  uniti+r = sym≃ unite+r

  assocr+ : {m n o : ℕ} → Fin ((m + n) + o) ≃ Fin (m + (n + o))
  assocr+ {m} = sym≃ (assocl+ {m})

  sswap+ : {m n : ℕ} → Fin (n + m) ≃ Fin (m + n)
  sswap+ {m} {n} = sym≃ (swap+ {m} {n})

-----------------------------------------------------------------------------
-- Multiplicative monoid

module TimesE where

  infixl 7 _*F_

  -- multiplicative monoid equivalences

  -- unite*

  unite* : {m : ℕ} → Fin (1 * m) ≃ Fin m
  unite* {m} = unite⋆equiv ● Fin1≃⊤ ×≃ id≃ ● *≃×

  -- unite*r

  unite*r : {m : ℕ} → Fin (m * 1) ≃ Fin m
  unite*r {m} = unite⋆′equiv ● id≃ ×≃ Fin1≃⊤ ● *≃×

  -- swap*

  swap* : {m n : ℕ} → Fin (m * n) ≃ Fin (n * m)
  swap* {m} {n} = ×≃* ● swap⋆equiv ● *≃× {m}

  -- associativity

  assocl* : {m n o : ℕ} → Fin (m * (n * o)) ≃ Fin ((m * n) * o)
  assocl* {m} {n} {o} = ×≃* ● ×≃* ×≃ id≃ ● assocl⋆equiv ● id≃ ×≃ *≃× ● *≃× {m}

  -- congruence

  _*F_ : {m n o p : ℕ} → Fin m ≃ Fin n → Fin o ≃ Fin p →
              Fin (m * o) ≃ Fin (n * p)
  Fm≃Fn *F Fo≃Fp = ×≃* ● Fm≃Fn ×≃ Fo≃Fp ● *≃×

  uniti* : {m : ℕ} → Fin m ≃ Fin (1 * m)
  uniti* = sym≃ unite*

  uniti*r : {m : ℕ} → Fin m ≃ Fin (m * 1)
  uniti*r = sym≃ unite*r

  assocr* : {m n o : ℕ} → Fin ((m * n) * o) ≃ Fin (m * (n * o))
  assocr* {m} {n} {o} = sym≃ (assocl* {m})

  sswap* : {m n : ℕ} → Fin (n * m) ≃ Fin (m * n)
  sswap* {m} {n} = sym≃ (swap* {m} {n})

------------------------------------------------------------------------------
-- Distributivity of multiplication over addition

module PlusTimesE where

  -- now that we have two monoids, we need to check distributivity

  -- note that the sequence below is "logically right", *but* could be
  -- replaced by id≃ !
  distz : {m : ℕ} → Fin (0 * m) ≃ Fin 0
  distz {m} = sym≃ F0≃⊥ ● distzequiv ● F0≃⊥ ×≃ id≃ ● *≃× {0} {m}
    where open Times

  distzr : {m : ℕ} → Fin (m * 0) ≃ Fin 0
  distzr {m} = sym≃ F0≃⊥ ● distzrequiv ● id≃ ×≃ F0≃⊥ ● *≃× {m} {0}
    where open Times

  dist : {m n o : ℕ} → Fin ((m + n) * o) ≃ Fin ((m * o) + (n * o))
  dist {m} {n} {o} = ⊎≃+ {m * o} {n * o} ● ×≃* {m} ⊎≃ ×≃* ● distequiv ● +≃⊎ ×≃ id≃ ● *≃×
    where open Times
          open Plus

  distl : {m n o : ℕ} → Fin (m * (n + o)) ≃ Fin ((m * n) + (m * o))
  distl {m} {n} {o} = ⊎≃+ {m * n} {m * o} ● ×≃* {m} ⊎≃ ×≃* ● distlequiv ● id≃ ×≃ +≃⊎ ● *≃×
    where open Plus
          open Times

  factorzr : {n : ℕ} → Fin 0 ≃ Fin (n * 0)
  factorzr {n} = sym≃ (distzr {n})

  factorz : {m : ℕ} → Fin 0 ≃ Fin (0 * m)
  factorz {m} = sym≃ (distz {m})

  factor : {m n o : ℕ} → Fin ((m * o) + (n * o)) ≃ Fin ((m + n) * o)
  factor {m} = sym≃ (dist {m})

  factorl : {m n o : ℕ} → Fin ((m * n) + (m * o)) ≃ Fin (m * (n + o))
  factorl {m} = sym≃ (distl {m})

------------------------------------------------------------------------------
-- Summarizing... we have a commutative semiring structure

fin≃IsEquiv : IsEquivalence _fin≃_
fin≃IsEquiv = record {
  refl = id≃ ;
  sym = sym≃ ;
  trans = trans≃
  }

finPlusIsSG : IsSemigroup _fin≃_ _+_
finPlusIsSG = record {
  isEquivalence = fin≃IsEquiv ;
  assoc = λ m n o → PlusE.assocr+ {m} {n} {o} ;
  ∙-cong = PlusE._+F_
  }

finTimesIsSG : IsSemigroup _fin≃_ _*_
finTimesIsSG = record {
  isEquivalence = fin≃IsEquiv ;
  assoc = λ m n o → TimesE.assocr* {m} {n} {o} ;
  ∙-cong = TimesE._*F_
  }

finPlusIsCM : IsCommutativeMonoid _fin≃_ _+_ 0
finPlusIsCM = record {
  isSemigroup = finPlusIsSG ;
  identityˡ = λ m → id≃ ;
  comm = λ m n → PlusE.swap+ {m} {n}
  }

finTimesIsCM : IsCommutativeMonoid _fin≃_ _*_ 1
finTimesIsCM = record {
  isSemigroup = finTimesIsSG ;
  identityˡ = λ m → TimesE.unite* {m} ;
  comm = λ m n → TimesE.swap* {m} {n}
  }

finIsCSR : IsCommutativeSemiring _fin≃_ _+_ _*_ 0 1
finIsCSR = record {
  +-isCommutativeMonoid = finPlusIsCM ;
  *-isCommutativeMonoid = finTimesIsCM ;
  distribʳ = λ o m n → PlusTimesE.dist {m} {n} {o} ;
  zeroˡ = λ m → PlusTimesE.distz {m}
  }

finCSR : CommutativeSemiring Level.zero Level.zero
finCSR = record {
  Carrier = ℕ ;
  _≈_ = _fin≃_ ;
  _+_ = _+_ ;
  _*_ = _*_ ;
  0# = 0 ;
  1# = 1 ;
  isCommutativeSemiring = finIsCSR
  }

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

ext: agda

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

module Erased-cubical-Module-application.Cubical (_ : Set₁) where

open import Agda.Builtin.Cubical.Path

data ∥_∥ (A : Set) : Set where
  ∣_∣     : A → ∥ A ∥
  trivial : (x y : ∥ A ∥) → x ≡ y

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

open import Cubical.Foundations.Prelude

open import Cubical.Data.Sigma

open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.AbGroup

private
  variable
    ℓ : Level

record IsAlmostRing {R : Type ℓ}
                  (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) : Type ℓ where

  constructor isalmostring

  field
    +IsMonoid : IsMonoid 0r _+_
    ·IsMonoid : IsMonoid 1r _·_
    +Comm : (x y : R) → x + y ≡ y + x
    ·Comm : (x y : R) → x · y ≡ y · x
    ·DistR+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z)
    ·DistL+ :  (x y z : R) → (x + y) · z ≡ (x · z) + (y · z)
    -Comm· : (x y : R) → - (x · y) ≡ (- x) · y
    -Dist+ : (x y : R) → - (x + y) ≡ (- x) + (- y)

  open IsMonoid +IsMonoid public
    renaming
      ( assoc       to +Assoc
      ; identity    to +Identity
      ; lid         to +Lid
      ; rid         to +Rid
      ; isSemigroup to +IsSemigroup)

  open IsMonoid ·IsMonoid public
    renaming
      ( assoc       to ·Assoc
      ; identity    to ·Identity
      ; lid         to ·Lid
      ; rid         to ·Rid
      ; isSemigroup to ·IsSemigroup )
    hiding
      ( is-set ) -- We only want to export one proof of this

record AlmostRing : Type (ℓ-suc ℓ) where

  constructor almostring

  field
    Carrier : Type ℓ
    0r      : Carrier
    1r      : Carrier
    _+_     : Carrier → Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    isAlmostRing  : IsAlmostRing 0r 1r _+_ _·_ -_

  infixl 8 _·_
  infixl 7 -_
  infixl 6 _+_

  open IsAlmostRing isAlmostRing public

-- Extractor for the carrier type
⟨_⟩ : AlmostRing → Type ℓ
⟨_⟩ = AlmostRing.Carrier

isSetAlmostRing : (R : AlmostRing {ℓ}) → isSet ⟨ R ⟩
isSetAlmostRing R = R .AlmostRing.isAlmostRing .IsAlmostRing.·IsMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
module Issue326 where

open import Common.Prelude

postulate
  QName : Set
  Unit : Set
  IO   : Set → Set
  printBool : Bool → IO Unit

{-# BUILTIN QNAME QName #-}
{-# BUILTIN IO IO #-}
{-# COMPILED_TYPE IO IO #-}
{-# COMPILED_TYPE Unit () #-}
{-# COMPILED printBool print #-}

primitive primQNameEquality : QName → QName → Bool

main : IO Unit
main = printBool (primQNameEquality (quote Unit) (quote IO))

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


text:
module REMatch where

open import Data.Char
import Data.Nat
--open import Data.List
open import Data.Bool

open import Data.Product

import Algebra
import Algebra.FunctionProperties

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

open import Data.List
open import Data.List.Properties

open import Data.Sum

open import Data.List.NonEmpty

--open List-solver renaming (nil to :[]; _⊕_ to _:++_; _⊜_ to _:≡_; solve to listSolve; prove to listProve)

open import Algebra
import Algebra.FunctionProperties as FunProp

open import Data.Maybe

open import Data.Nat

open import RETypes

import Relation.Binary.Reflection as Ref

import Data.Bool.Properties

listDivisions : List Char -> List (List Char × List Char)
listDivisions [] = ( [] , []) ∷ []
listDivisions (h ∷ t) = ([] , h ∷ t ) ∷ (Data.List.map (λ p -> ( (h ∷ proj₁ p) , proj₂ p )) (listDivisions t) )

elementMatches : {A : Set} (f : A -> Bool) -> List A -> Bool
elementMatches f [] = false
elementMatches f (h ∷ t) = (f h) ∨ elementMatches f t

{-
mutual

  starMatch : {n : Null?} -> (RE n) -> List Char -> List Char -> (List Char -> Bool) -> Bool
  starMatch (r *) s1 (sh ∷ st) k =  (acc r (s1 ++ Data.List.[ sh ]) null ∧ acc ( r *) st k )  ∨ starMatch (r *) (s1 ++ Data.List.[ sh ]) st k
  starMatch (r *) s1 [] k = false
  starMatch _ _ _ _ = false
-}

{-# TERMINATING #-}
acc :  {n : Null?} -> RE n -> List Char -> (List Char -> Bool) -> Bool
acc ε s k = k s
acc ∅ _ _ = false
acc (Lit _) [] _ = false
acc (Lit c) (sFirst ∷ sRest) k with (c Data.Char.≟ sFirst)
... | yes pf  = (k sRest)
... | no _  = false
acc (r₁ + r₂) s k = (acc r₁ s k) ∨ (acc r₂ s k)
acc (r₁ · r₂) s k = acc r₁ s (λ s' -> acc r₂ s' k)
acc (r *) [] k = (k [])
acc (r *) (ch ∷ ct) k =
  let
    cs = ch ∷ ct
  in k cs ∨ acc r cs (\cs' -> acc (r *) cs' k)
  --acc r cs (\cs' -> acc (r) cs' k)
  --acc (r *) (sFirst ∷ sRest) k =  starMatch r (sFirst ∷ [] ) sRest k

accept : {n : Null?} -> RE n -> List Char -> Bool
accept r s = acc r s null

concatPreservesNonNull : {s1 : List Char}
  -> {s2 : List Char}
  -> (∃ λ (h : Char) -> ∃ λ (t : List Char) -> (s1 ≡ h ∷ t) )
  -> (∃ λ (h : Char) -> ∃ λ (t : List Char) -> (s1 ++ s2 ≡ h ∷ t) )
concatPreservesNonNull {s1} {s2 = []} (sh , st , pf) =
  let
    concatPf : s1 ++ [] ≡ s1
    concatPf = (solve (suc zero) (λ x → x ⊕ nil , x) (λ {x} → refl)) s1 --Should be easy, I might have already proved something similar,
    --This is probably a good place to try the List prover stuff
  in sh , st , trans concatPf pf
  where open List-solver
concatPreservesNonNull {s1} {s2 = x ∷ s2} (sh , st , pf) =
  let
    --subProof : (∃ λ (h : Char) -> ∃ λ (t : List Char) -> (s1 ++ s2 ≡ h ∷ t) )
    (h , t , subProof) = concatPreservesNonNull {s1} {s2} (sh , st , pf)
    p2 : ((sh ∷ st) ++ s2 ≡ h ∷ t)
    p2 = subst (λ x₁ → x₁ ++ s2 ≡ h ∷ t) pf subProof
  in sh , (st ++ (x ∷ s2)) , cong (λ x₁ → x₁ ++ x ∷ s2) pf

concatPreservesNonNull2 : {s1 : List Char}
  -> {s2 : List Char}
  -> (∃ λ (h : Char) -> ∃ λ (t : List Char) -> (s2 ≡ h ∷ t) )
  -> (∃ λ (h : Char) -> ∃ λ (t : List Char) -> (s1 ++ s2 ≡ h ∷ t) )
concatPreservesNonNull2 {[]} (sh , st , pf) = sh , st , pf
concatPreservesNonNull2 {x ∷ s1} {s2} (sh , st , pf) = x , s1 ++ s2 , refl

open ≡-Reasoning

nullCorrect : (r : RE NonNull) -> (s : List Char ) -> (REMatch s r)
  -> (∃ λ (h : Char) -> ∃ λ (t : List Char) -> (s ≡ h ∷ t) )
nullCorrect .(Lit c) .(c ∷ []) (LitMatch c) = c , [] , refl
nullCorrect ._ s (LeftPlusMatch {nb = BothNullB} {r1 = r1} r2 match) = nullCorrect r1 s match
nullCorrect ._ s (RightPlusMatch {nb = BothNullB} r1 {r2 = r2} match) = nullCorrect r2 s match
nullCorrect .(r1 · r2) s (ConcatMatch {nt = LeftNullT} {s1 = s1} {s2 = s2} {spf = spf} {r1 = r1} {r2 = r2}  match1 match2) =
  let
    sh , st , subPf = concatPreservesNonNull2 {s1 = s1} {s2 = s2} (nullCorrect r2 s2 match2)
  in sh , st , trans (sym spf) subPf   --subH , subT , ?
nullCorrect ._ s (ConcatMatch {nt = BothNonNullT} {s1 = s1} {s2 = s2} {spf = spf} {r1 = r1} {r2 = r2} match1 match2) =
  let
    sh , st , subPf = concatPreservesNonNull2 {s1 = s1} {s2 = s2} (nullCorrect r2 s2 match2)
  in sh , st , trans (sym spf) subPf
nullCorrect ._ s (ConcatMatch {nt = RightNullT} {s1 = s1} {s2 = s2} {spf = spf} {r1 = r1} {r2 = r2} match1 match2) =
  let
    sh , st , subPf = concatPreservesNonNull {s1 = s1} {s2 = s2} (nullCorrect r1 s1 match1)
  in sh , st , trans (sym spf) subPf  -- concatPreservesNonNull (nullCorrect r1 s1 match1)

--Taken from http://gelisam.blogspot.ca/2010/10/equality-is-useless-transmutation.html
--Can probably be done with more complicated existing stuff, but this is easier
mySubst : {X : Set}
       → (P : X → Set)
       → (x y : X)
       → x ≡ y
       → P x
       → P y
mySubst P v .v refl p = p

orLemma1 : {x : Bool} {y : Bool} -> (y ≡ true) -> (y ∨ x) ≡ true
orLemma1 {x} {true} pf = refl
orLemma1 {x} {false} ()

andElim1 : {x : Bool} {y : Bool} -> (x ∧ y) ≡ true -> (x ≡ true)
andElim1 {true} pf = refl
andElim1 {false} ()

--TODO Pattern match on and first
andElim2 : {x : Bool} {y : Bool} -> (x ∧ y) ≡ true -> (y ≡ true)
andElim2 {y = true} pf = refl
andElim2 {true} {false} ()
andElim2 {false} {false} ()

andCombine : {x : Bool} {y : Bool} -> x ≡ true -> y ≡ true -> (x ∧ y) ≡ true
andCombine {true} pfx pfy = pfy
andCombine {false} ()

{-
orCommut : {x : Bool} {y : Bool} -> (y ∨ x) ≡ (x ∨ y)
orCommut {true} {true} = refl
orCommut {false} {true} = refl
orCommut {true} {false} = refl
orCommut {false} {false} = refl
-}

orLemma2 : {x : Bool} {y : Bool} -> (y ≡ true) -> (x ∨ y) ≡ true
orLemma2 {true} {true} pf = refl
orLemma2 {false} {true} pf = refl
orLemma2 {true} {false} pf = refl
orLemma2 {false} {false} ()

orCases : {x : Bool} {y : Bool} -> (x ∨ y ≡ true) -> (x ≡ true) ⊎ (y ≡ true)
orCases {true} y = inj₁ refl
orCases {false} y = inj₂ y

listRightIdent : { x : List Char} -> (x ++ []) ≡ x
listRightIdent {[]} = refl
listRightIdent {x ∷ x₁} = cong (_∷_ x) (listRightIdent {x₁})

listAssoc : {x y z : List Char} -> (x ++ y) ++ z ≡ x ++ (y ++ z)
listAssoc {[]} = λ {y} {z} → refl
listAssoc {xh ∷ xt} {y} {z} = cong (_∷_ xh) (listAssoc {xt} {y} {z})

maybeHead : List Char -> Maybe Char
maybeHead [] = nothing
maybeHead (x ∷ _) = just x

fakeTail : List Char -> List Char
fakeTail [] = []
fakeTail (_ ∷ t) = t

myFromJust : Maybe Char -> Char
myFromJust (just x) = x
myFromJust (nothing) = 'a'

sameHead : {a : Char}{b : Char}{l1 : List Char}{l2 : List Char} -> ((a ∷ l1) ≡ (b ∷ l2)) -> (a ≡ b)
sameHead {a} {b} {l1} {l2} pf =
  let
    maybeSameHead : (just a) ≡ (just b)
    maybeSameHead = cong (maybeHead) pf
  in cong myFromJust maybeSameHead

sameTail : {a : Char}{b : Char}{l1 : List Char}{l2 : List Char} -> ((a ∷ l1) ≡ (b ∷ l2)) -> (l1 ≡ l2)
sameTail {a} {b} {l1} {l2} pf = cong fakeTail pf

emptyMiddleList : {c : Char}{s1 s2 : List Char} -> (c ∷ s1 ≡ (c ∷ []) ++ s2 ) -> s1 ≡ s2
emptyMiddleList {c} {s1} {s2} spf =

  let
    p0 : (s1 ≡ [] ++ s2 )
    p0 = cong fakeTail spf
    p1 : [] ++ s2 ≡ s2
    p1 = refl
  in trans p0 p1

accCorrect :
  {n : Null? }
  (r : RE n)
  (s : List Char) (s1 : List Char) (s2 : List Char)
  (k : (List Char -> Bool))
  -> ( (s1 ++ s2) ≡ s)
  -> (REMatch s1 r)
  -> (k s2 ≡ true)
  -> (acc r s k ≡ true )
--accCorrect ∅ [] [] [] k _ () kproof
accCorrect ε  [] ._ []  k _ EmptyMatch kproof = kproof
accCorrect (Lit .c) (c1 ∷ srest ) (.c ∷ []) s2 k stringProof (LitMatch c) kproof with (c Data.Char.≟ c1)
... | yes eqPf =   let
    sameHeads : c ≡ c1
    sameHeads = sameHead stringProof
    p0 : c Data.List.∷ srest ≡ c1 Data.List.∷ srest
    p0 = cong (λ x → x ∷ srest) sameHeads

    flipProof : (c1 ∷ srest ) ≡ (c ∷ []) ++ s2
    flipProof = sym stringProof
    cFlip : (c ∷ srest ) ≡ (c ∷ []) ++ s2
    cFlip = trans p0 flipProof
    restProof : srest ≡ s2
    restProof = emptyMiddleList cFlip

    primEq : (Dec (c ≡ c1))
    primEq = yes sameHeads

    pf3 = cong (λ theChar -> acc (Lit c) (c ∷ srest) k ) sameHeads

  in trans (cong k restProof) kproof
accCorrect (Lit .c) (c1 ∷ srest ) (.c ∷ []) s2 k stringProof (LitMatch c) () | no pf

{-
  let
    sameHeads = sameHead stringProof
    primEq : (Dec (c ≡ c1))
    primEq = yes sameHeads
    pf3 = cong (λ theChar -> acc (Lit c) (c ∷ srest) k ) sameHeads
    restProof : srest ≡ s2
    restProof = {!!}
  in cong k restProof
-}
accCorrect (.r1 · .r2 ) s .s1 s2  k  split1 (ConcatMatch {_} {_} {n3} {nt} {s1'} {s2'} {s1} {spf'} {r1} {r2} subMatch1 subMatch2) kproof  =
  let
           --s1 = s1' ++ s2'
           split2 : (s1' ++ s2') ≡ s1
           split2 = spf' --refl
           split3 : (s1' ++ s2') ++ s2 ≡ s1 ++ s2
           split3 = cong (λ x -> x ++ s2) split2
           split4 : s1' ++ s2' ++ s2 ≡ (s1' ++ s2') ++ s2
           split4 =  sym (listAssoc {s1'} {s2'} {s2})
           transChain : s1' ++ s2' ++ s2 ≡ s
           transChain = trans split4 (trans split3 split1)
  in accCorrect r1 s s1' (s2' ++ s2) (\cs -> acc r2 cs k) transChain
    subMatch1 (accCorrect r2 (s2' ++ s2) s2' s2 k refl subMatch2 kproof)
accCorrect (.r1 + .r2 ) s .s1 s2  k
  splitProof (LeftPlusMatch {_} {_} {n3} {nb} {s1} {r1} (r2) subMatch) kproof  =
   orLemma1 (accCorrect r1 s s1 s2 k splitProof subMatch kproof )
accCorrect (.r1 + .r2) s .s1 s2  k
  splitProof (RightPlusMatch {_} {_} {n3} {nb} {s1} (r1) {r2} subMatch) kproof  =
    let subCorrect = accCorrect r2 s s1 s2 k splitProof subMatch kproof
    in orLemma2 {acc r1 s k} {acc r2 s k} subCorrect
accCorrect (.r *) [] ._ [] k _ (EmptyStarMatch {r}) kproof = kproof

accCorrect {MaybeNull} (.r *) (sh ∷ st ) .s1 s2  k  split1 (StarMatch {c1} {s1t'} {s2'} {s1} {spf} {r} subMatch1 subMatch2) kproof  =
  let
           s = (sh ∷ st )
           s1' = (c1 ∷ s1t')

           split2 : (s1' ++ s2') ≡ s1
           split2 = spf
           split3 : (s1' ++ s2') ++ s2 ≡ s1 ++ s2
           split3 = cong (λ x -> x ++ s2) split2
           split4 : s1' ++ s2' ++ s2 ≡ (s1' ++ s2') ++ s2
           split4 =  sym (listAssoc {s1'} {s2'} {s2})
           transChain : s1' ++ s2' ++ s2 ≡ s
           transChain = trans split4 (trans split3 split1)
           sub2' : REMatch {MaybeNull} s2' (r *)
           sub2' = subMatch2
           subCorrect : acc (r *) (s2' ++ s2) k ≡ true
           subCorrect = accCorrect (r *) (s2' ++ s2) s2' s2 k refl subMatch2 kproof
           rightCorrect : acc r s (\cs' -> acc (r *) cs' k) ≡ true
           rightCorrect = accCorrect r s s1' (s2' ++ s2) (λ cs → acc (r *) cs k) transChain subMatch1 subCorrect
           orCorrect : (k s ∨ acc r s (\cs' -> acc (r *) cs' k) ) ≡ true
           orCorrect = orLemma2 {x = k s} rightCorrect
  --TODO pass in x and y explicitly
  in orCorrect --accCorrect r s s1' (s2' ++ s2) (\cs -> acc (r *) cs k) transChain
    --subMatch1 (accCorrect (r *) (s2' ++ s2) s2' s2 k refl subMatch2 kproof)

accCorrect (r *) (sh ∷ st) [] s2 k sp1 _ kproof =
  let
    s = sh ∷ st
    sp2 : s2 ≡ s
    sp2 = sp1
    kproof2 : k s ≡ k s2
    kproof2 = cong k (sym sp1)
    kproof3 : k s ≡ true
    kproof3 = trans kproof2 kproof
    --orProof : (k s ∨ starMatch r [] s k) ≡ true
    orProof = orLemma1 kproof3
  in orProof
 --accCorrect r s s1' (s2' ++ s2) (\cs -> acc (r *) cs k) transChain
    --subMatch1 (accCorrect (r *) (s2' ++ s2) s2' s2 k refl subMatch2 kproof)
--accCorrect  (.r *) s ._ s2 k sp1 (StarMatch {s1'} {s1''} {r} sub1 sub2) kproof = ?
accCorrect ∅ _ _ _ _ _ ()
accCorrect ε (_ ∷ _ ) _ _ _ () _
accCorrect _ [] (_ ∷ _ ) _ _ () _ _
accCorrect _ [] _ (_ ∷ _ ) _ () _ _
accCorrect (Lit _) [] _ _ _ () _ _
accCorrect {._} (_* _) [] [] [] _ _
             (StarMatch {_} {_} {_} {._} {()} {._} _ _) _
--accCorrect _ _ _ _ _ _ _ _ = {!!} --This case should disappear when I finish star

boolExclMiddle : {x : Bool} { y : Bool } -> (x ∨ y ≡ true ) -> (x ≡ false) -> (y ≡ true)
boolExclMiddle {true} p1 ()
boolExclMiddle {false} p1 p2 = p1

{-# TERMINATING #-}
accComplete :
  {n : Null?}
  (r : RE n)
  (s : List Char)
  (k : (List Char -> Bool))
  -> (acc r s k ≡ true)
  -> ∃ (λ s1 -> ∃ (λ s2 -> (s1 ++ s2 ≡ s) × ( k s2 ≡ true) × (REMatch s1 r ) ) )
accComplete ε [] k pf =  [] , [] , refl , pf , EmptyMatch
accComplete ε s k pf = [] , s , refl , pf , EmptyMatch
accComplete (Lit c) (c1 ∷ srest) k accProof with (c Data.Char.≟ c1)
...| yes eqProof =
    let
      charsEqual : c ≡ c1
      charsEqual = eqProof
    in  Data.List.[ c ] , srest , cong (λ x → x ∷ srest) charsEqual , accProof , LitMatch c
accComplete (Lit c) (c1 ∷ srest) k () | no _
accComplete (_·_ {n1} {n2} r1  r2) s k pf =
  let
    sub1 : acc r1 s (λ s' -> acc r2 s' k) ≡ true
    sub1 = pf
    s11 , s2' , psub1 , psub2 , match1  = accComplete r1 s (λ s' -> acc r2 s' k) pf
    s12 , s2 , p1 , p2 , match2 = accComplete r2 s2' k psub2
    localAssoc :  s11 ++ (s12 ++ s2) ≡ (s11 ++ s12) ++ s2
    localAssoc = sym (listAssoc {s11} {s12} {s2})
    subProof1 : s11 ++ s2' ≡ s11 ++ (s12 ++ s2)
    subProof1 = sym ( cong (λ x -> s11 ++ x) p1 )
    subProof2 : s11 ++ s2' ≡ (s11 ++ s12) ++ s2
    subProof2 = trans subProof1 localAssoc
    stringProof = trans (sym subProof2) psub1
  in (s11 ++ s12 ) , s2 , stringProof , p2 , (ConcatMatch {spf = refl} match1 match2)

accComplete (r1 + r2) s k accProof with (orCases accProof)
...  | inj₁ leftTrue  =
  let
    s1 , s2 , p1 , p2 , match = accComplete r1 s k leftTrue
  in s1 , s2 , p1 , p2 , LeftPlusMatch r2 match
...  | inj₂ rightTrue  = let
    s1 , s2 , p1 , p2 , match = accComplete r2 s k rightTrue
  in s1 , s2 , p1 , p2 , RightPlusMatch r1 match
accComplete (r *) [] k pf =  [] , [] , refl , pf , EmptyStarMatch
accComplete {MaybeNull} (r *) (sh ∷ st) k accProof with (orCases accProof)
... | inj₁ leftTrue  =  [] , (sh ∷ st) , refl , leftTrue , EmptyStarMatch
... | inj₂ rightTrue  =
  let
    rTest : RE NonNull
    rTest = r
    s = sh ∷ st
    sub1 : acc r s (λ s' -> acc (r *) s' k) ≡ true
    sub1 = rightTrue
    s11 , s2' , psub1 , psub2 , match1  = accComplete r s (λ s' -> acc (r *) s' k) rightTrue
    s12 , s2 , p1 , p2 , match2 = accComplete (r *) s2' k psub2
    localAssoc :  s11 ++ (s12 ++ s2) ≡ (s11 ++ s12) ++ s2
    localAssoc = sym (listAssoc {s11} {s12} {s2})
    subProof1 : s11 ++ s2' ≡ s11 ++ (s12 ++ s2)
    subProof1 = sym ( cong (λ x -> s11 ++ x) p1 )
    subProof2 : s11 ++ s2' ≡ (s11 ++ s12) ++ s2
    subProof2 = trans subProof1 localAssoc
    stringProof = trans (sym subProof2) psub1

    s11h , s11t , nnpf = nullCorrect r s11 match1
    nonNullPf : s11 ≡ s11h ∷ s11t
    nonNullPf = nnpf

    m1 : REMatch (s11h ∷ s11t) r
    m1 = mySubst (λ str → REMatch str r) s11 (s11h ∷ s11t) (nonNullPf) match1
    m2 : REMatch s12 (r *)
    m2 = match2
    newSpf : (s11h ∷ s11t) ++ s2' ≡ s11 ++ s2'
    newSpf = {!!}
    --ourMatch : REMatch (s11 ++ s12) (r *)
    ourMatch = StarMatch {spf = newSpf} {r = rTest} m1 ? --m2
  in (s11 ++ s12 ) , s2 , stringProof , p2 , {!!} --ourMatch
accComplete ∅ _ _ ()
accComplete (Lit _) [] _ ()

acceptCorrect :
  {n : Null? }
  (r : RE n)
  (s : List Char)
  -> (REMatch s r)
  -> (accept r s ≡ true )
acceptCorrect r s match = accCorrect r s s [] null listRightIdent match refl

nullEq : {x : List Char} -> (null x ≡ true ) -> (x ≡ [])
nullEq {[]} pf = refl
nullEq {x ∷ x₁} ()

substMatch : {n : Null?}{r : RE n}{s s1 : List Char} -> s1 ≡ s -> REMatch s1 r -> REMatch s r
substMatch refl m = m

acceptComplete :
  {n : Null? }
  (r : RE n)
  (s : List Char)
  -> (accept r s ≡ true )
  -> REMatch s r
acceptComplete r s pf =
  let
    s1 , s2 , sproof , ks2Proof , match = accComplete r s null pf
    s2Null : s2 ≡ []
    s2Null = nullEq ks2Proof
    sp3 : s1 ++ s2 ≡ s1 ++ []
    sp3 = cong (λ x -> s1 ++ x) s2Null
    sp4 : s1 ++ s2 ≡ s1
    sp4 = trans sp3 listRightIdent
    sp5 : s1 ≡ s
    sp5 = sym (trans (sym sproof) sp4)
  in substMatch sp5 match --match

max_stars_repo_name: JoeyEremondi/agda-parikh

max_issues_repo_name: JoeyEremondi/agda-parikh

max_forks_repo_name: JoeyEremondi/agda-parikh


text:
-- Define the integers as a HIT by identifying +0 and -0
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Ints.QuoInt.Base where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Relation.Nullary

open import Cubical.Data.Int as Int using (Int; sucInt; predInt; discreteInt; isSetInt)
open import Cubical.Data.Nat as ℕ using (ℕ; zero; suc)
open import Cubical.Data.Bool as Bool using (Bool; not; notnot)

variable
  l : Level

Sign : Type₀
Sign = Bool

pattern spos = Bool.false
pattern sneg = Bool.true

_·S_ : Sign → Sign → Sign
_·S_ = Bool._⊕_

data ℤ : Type₀ where
  signed : (s : Sign) (n : ℕ) → ℤ
  posneg : signed spos 0 ≡ signed sneg 0

pattern pos n = signed spos n
pattern neg n = signed sneg n

sign : ℤ → Sign
sign (signed _ zero) = spos
sign (signed s (suc _)) = s
sign (posneg i) = spos

sign-pos : ∀ n → sign (pos n) ≡ spos
sign-pos zero = refl
sign-pos (suc n) = refl

abs : ℤ → ℕ
abs (signed _ n) = n
abs (posneg i) = zero

signed-inv : ∀ n → signed (sign n) (abs n) ≡ n
signed-inv (pos zero) = refl
signed-inv (neg zero) = posneg
signed-inv (signed s (suc n)) = refl
signed-inv (posneg i) j = posneg (i ∧ j)

signed-zero : ∀ s₁ s₂ → signed s₁ zero ≡ signed s₂ zero
signed-zero spos spos = refl
signed-zero sneg sneg = refl
signed-zero spos sneg = posneg
signed-zero sneg spos = sym posneg

rec : ∀ {A : Type l} → (pos' neg' : ℕ → A) → pos' 0 ≡ neg' 0 → ℤ → A
rec pos' neg' eq (pos m)    = pos' m
rec pos' neg' eq (neg m)    = neg' m
rec pos' neg' eq (posneg i) = eq i

elim : ∀ (P : ℤ → Type l)
       → (pos' : ∀ n → P (pos n))
       → (neg' : ∀ n → P (neg n))
       → (λ i → P (posneg i)) [ pos' 0 ≡ neg' 0 ]
       → ∀ z → P z
elim P pos' neg' eq (pos n) = pos' n
elim P pos' neg' eq (neg n) = neg' n
elim P pos' neg' eq (posneg i) = eq i

Int→ℤ : Int → ℤ
Int→ℤ (Int.pos n) = pos n
Int→ℤ (Int.negsuc n) = neg (suc n)

ℤ→Int : ℤ → Int
ℤ→Int (pos n) = Int.pos n
ℤ→Int (neg zero) = Int.pos 0
ℤ→Int (neg (suc n)) = Int.negsuc n
ℤ→Int (posneg _) = Int.pos 0

ℤ→Int→ℤ : ∀ (n : ℤ) → Int→ℤ (ℤ→Int n) ≡ n
ℤ→Int→ℤ (pos n) _       = pos n
ℤ→Int→ℤ (neg zero) i    = posneg i
ℤ→Int→ℤ (neg (suc n)) _ = neg (suc n)
ℤ→Int→ℤ (posneg j) i    = posneg (j ∧ i)

Int→ℤ→Int : ∀ (n : Int) → ℤ→Int (Int→ℤ n) ≡ n
Int→ℤ→Int (Int.pos n) _ = Int.pos n
Int→ℤ→Int (Int.negsuc n) _ = Int.negsuc n

Int≡ℤ : Int ≡ ℤ
Int≡ℤ = isoToPath (iso Int→ℤ ℤ→Int ℤ→Int→ℤ Int→ℤ→Int)

discreteℤ : Discrete ℤ
discreteℤ = subst Discrete Int≡ℤ discreteInt

isSetℤ : isSet ℤ
isSetℤ = subst isSet Int≡ℤ isSetInt

-_ : ℤ → ℤ
- signed s n = signed (not s) n
- posneg i   = posneg (~ i)

negate-invol : ∀ n → - - n ≡ n
negate-invol (signed s n) i = signed (notnot s i) n
negate-invol (posneg i)   _ = posneg i

negateEquiv : ℤ ≃ ℤ
negateEquiv = isoToEquiv (iso -_ -_ negate-invol negate-invol)

negateEq : ℤ ≡ ℤ
negateEq = ua negateEquiv

infixl 6 _+_
infixl 7 _·_

sucℤ : ℤ → ℤ
sucℤ (pos n)       = pos (suc n)
sucℤ (neg zero)    = pos 1
sucℤ (neg (suc n)) = neg n
sucℤ (posneg _)    = pos 1

predℤ : ℤ → ℤ
predℤ = subst (λ Z → (Z → Z)) negateEq sucℤ
  -- definitionally equal to λ n → - (sucℤ (- n))
  -- strictly more useful than the direct pattern matching version,
  --  see negateSuc and negatePred

sucPredℤ : ∀ n → sucℤ (predℤ n) ≡ n
sucPredℤ (pos zero)    = sym posneg
sucPredℤ (pos (suc _)) = refl
sucPredℤ (neg _)       = refl
sucPredℤ (posneg i) j  = posneg (i ∨ ~ j)

predSucℤ : ∀ n → predℤ (sucℤ n) ≡ n
predSucℤ (pos _)       = refl
predSucℤ (neg zero)    = posneg
predSucℤ (neg (suc _)) = refl
predSucℤ (posneg i) j  = posneg (i ∧ j)

_+_ : ℤ → ℤ → ℤ
(signed _ zero) + n = n
(posneg _)      + n = n
(pos (suc m))   + n = sucℤ  (pos m + n)
(neg (suc m))   + n = predℤ (neg m + n)

sucPathℤ : ℤ ≡ ℤ
sucPathℤ  = isoToPath (iso sucℤ predℤ sucPredℤ predSucℤ)

-- We do the same trick as in Cubical.Data.Int to prove that addition
-- is an equivalence
addEqℤ : ℕ → ℤ ≡ ℤ
addEqℤ zero    = refl
addEqℤ (suc n) = addEqℤ n ∙ sucPathℤ

predPathℤ : ℤ ≡ ℤ
predPathℤ = isoToPath (iso predℤ sucℤ predSucℤ sucPredℤ)

subEqℤ : ℕ → ℤ ≡ ℤ
subEqℤ zero    = refl
subEqℤ (suc n) = subEqℤ n ∙ predPathℤ

addℤ : ℤ → ℤ → ℤ
addℤ (pos m) n    = transport (addEqℤ m) n
addℤ (neg m) n    = transport (subEqℤ m) n
addℤ (posneg _) n = n

isEquivAddℤ : (m : ℤ) → isEquiv (addℤ m)
isEquivAddℤ (pos n)    = isEquivTransport (addEqℤ n)
isEquivAddℤ (neg n)    = isEquivTransport (subEqℤ n)
isEquivAddℤ (posneg _) = isEquivTransport refl

addℤ≡+ℤ : addℤ ≡ _+_
addℤ≡+ℤ i  (pos (suc m)) n = sucℤ   (addℤ≡+ℤ i (pos m) n)
addℤ≡+ℤ i  (neg (suc m)) n = predℤ  (addℤ≡+ℤ i (neg m) n)
addℤ≡+ℤ i  (pos zero) n    = n
addℤ≡+ℤ i  (neg zero) n    = n
addℤ≡+ℤ _  (posneg _) n    = n

isEquiv+ℤ : (m : ℤ) → isEquiv (m +_)
isEquiv+ℤ = subst (λ _+_ → (m : ℤ) → isEquiv (m +_)) addℤ≡+ℤ isEquivAddℤ

_·_ : ℤ → ℤ → ℤ
m · n = signed (sign m ·S sign n) (abs m ℕ.· abs n)

private
  ·-abs : ∀ m n → abs (m · n) ≡ abs m ℕ.· abs n
  ·-abs m n = refl

-- Natural number and negative integer literals for ℤ

open import Cubical.Data.Nat.Literals public

instance
  fromNatℤ : HasFromNat ℤ
  fromNatℤ = record { Constraint = λ _ → Unit ; fromNat = λ n → pos n }

instance
  fromNegℤ : HasFromNeg ℤ
  fromNegℤ = record { Constraint = λ _ → Unit ; fromNeg = λ n → neg n }

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Oscar.Data.Term.internal.SubstituteAndSubstitution {𝔣} (FunctionName : Set 𝔣) where

open import Oscar.Category.Action
open import Oscar.Category.Category
open import Oscar.Category.CategoryAction
open import Oscar.Category.Functor
open import Oscar.Category.Morphism
open import Oscar.Category.Semifunctor
open import Oscar.Category.Semigroupoid
open import Oscar.Category.Setoid
open import Oscar.Category.SemigroupoidAction
open import Oscar.Data.Equality
open import Oscar.Data.Equality.properties
open import Oscar.Data.Fin
open import Oscar.Data.Nat
open import Oscar.Data.Term FunctionName
open import Oscar.Data.Vec
open import Oscar.Function
open import Oscar.Level
open import Oscar.Relation

𝕞₁ : Morphism _ _ _
𝕞₁ = Fin ⇨ Term

𝕞₂ : Morphism _ _ _
𝕞₂ = Term ⇨ Term

𝕞₂ₛ : Nat → Morphism _ _ _
𝕞₂ₛ N = Terms N ⇨ Terms N

module 𝔐₁ = Morphism 𝕞₁
module 𝔐₂ = Morphism 𝕞₂
module 𝔐₂ₛ (N : Nat) where open Morphism (𝕞₂ₛ N) public using () renaming (_↦_ to _[_↦_])

private

  infix 19 _◂_ _◂s_

  mutual

    _◂_ : ∀ {m n} → m 𝔐₁.↦ n → m 𝔐₂.↦ n
    σ̇ ◂ i 𝑥 = σ̇ 𝑥
    _ ◂ leaf = leaf
    σ̇ ◂ (τl fork τr) = (σ̇ ◂ τl) fork (σ̇ ◂ τr)
    σ̇ ◂ (function fn τs) = function fn (σ̇ ◂s τs) where

    _◂s_ : ∀ {m n} → m ⊸ n → ∀ {N} → N 𝔐₂ₛ.[ m ↦ n ] -- Vec (Term m) N → Vec (Term n) N
    f ◂s [] = []
    f ◂s (t ∷ ts) = f ◂ t ∷ f ◂s ts

  _∙_ : ∀ {m n} → m ⊸ n → ∀ {l} → l ⊸ m → l ⊸ n
  _∙_ f g = (f ◂_) ∘ g

  mutual

    ◂-extensionality : ∀ {m n} {f g : m ⊸ n} → f ≡̇ g → f ◂_ ≡̇ g ◂_
    ◂-extensionality p (i x) = p x
    ◂-extensionality p leaf = refl
    ◂-extensionality p (s fork t) = cong₂ _fork_ (◂-extensionality p s) (◂-extensionality p t)
    ◂-extensionality p (function fn ts) = cong (function fn) (◂s-extensionality p ts)

    ◂s-extensionality : ∀ {m n} {f g : m ⊸ n} → f ≡̇ g → ∀ {N} → _◂s_ f {N} ≡̇ _◂s_ g
    ◂s-extensionality p [] = refl
    ◂s-extensionality p (t ∷ ts) = cong₂ _∷_ (◂-extensionality p t) (◂s-extensionality p ts)

  mutual

    ◂-associativity : ∀ {l m} (f : l ⊸ m) {n} (g : m ⊸ n) → (g ∙ f) ◂_ ≡̇ (g ◂_) ∘ (f ◂_)
    ◂-associativity _ _ (i _) = refl
    ◂-associativity _ _ leaf = refl
    ◂-associativity _ _ (τ₁ fork τ₂) = cong₂ _fork_ (◂-associativity _ _ τ₁) (◂-associativity _ _ τ₂)
    ◂-associativity f g (function fn ts) = cong (function fn) (◂s-associativity f g ts)

    ◂s-associativity : ∀ {l m n} (f : l ⊸ m) (g : m ⊸ n) → ∀ {N} → (_◂s_ (g ∙ f) {N}) ≡̇ (g ◂s_) ∘ (f ◂s_)
    ◂s-associativity _ _ [] = refl
    ◂s-associativity _ _ (τ ∷ τs) = cong₂ _∷_ (◂-associativity _ _ τ) (◂s-associativity _ _ τs)

  ∙-associativity : ∀ {k l} (f : k ⊸ l) {m} (g : l ⊸ m) {n} (h : m ⊸ n) → (h ∙ g) ∙ f ≡̇ h ∙ (g ∙ f)
  ∙-associativity f g h x rewrite ◂-associativity g h (f x) = refl

  ∙-extensionality : ∀ {l m} {f₁ f₂ : l ⊸ m} → f₁ ≡̇ f₂ → ∀ {n} {g₁ g₂ : m ⊸ n} → g₁ ≡̇ g₂ → g₁ ∙ f₁ ≡̇ g₂ ∙ f₂
  ∙-extensionality {f₂ = f₂} f₁≡̇f₂ g₁≡̇g₂ x rewrite f₁≡̇f₂ x = ◂-extensionality g₁≡̇g₂ (f₂ x)

instance

  IsSemigroupoid𝕞₁∙ : IsSemigroupoid 𝕞₁ _∙_
  IsSemigroupoid.extensionality IsSemigroupoid𝕞₁∙ = ∙-extensionality
  IsSemigroupoid.associativity IsSemigroupoid𝕞₁∙ = ∙-associativity

𝕘₁ : Semigroupoid _ _ _
𝕘₁ = 𝕞₁ , _∙_

𝕘₂ : Semigroupoid _ _ _
𝕘₂ = 𝕞₂ , (λ ‵ → _∘_ ‵)

𝕘₂ₛ : Nat → Semigroupoid _ _ _
𝕘₂ₛ N = 𝕞₂ₛ N , (λ ‵ → _∘_ ‵)

𝕘₁,₂ : Semigroupoids _ _ _ _ _ _
𝕘₁,₂ = 𝕘₁ , 𝕘₂

instance

  IsSemifunctor𝕘₁₂◂ : IsSemifunctor 𝕘₁,₂ _◂_
  IsSemifunctor.extensionality IsSemifunctor𝕘₁₂◂ = ◂-extensionality
  IsSemifunctor.distributivity IsSemifunctor𝕘₁₂◂ = ◂-associativity

𝕗◂ : Semifunctor _ _ _ _ _ _
𝕗◂ = 𝕘₁,₂ , _◂_

𝕘₁,₂ₛ : Nat → Semigroupoids _ _ _ _ _ _
𝕘₁,₂ₛ N = 𝕘₁ , 𝕘₂ₛ N

instance

  IsSemifunctor𝕘₁,₂ₛ◂s : ∀ {N} → IsSemifunctor (𝕘₁,₂ₛ N) (λ ‵ → _◂s_ ‵)
  IsSemifunctor.extensionality IsSemifunctor𝕘₁,₂ₛ◂s f≡̇g τs = ◂s-extensionality f≡̇g τs
  IsSemifunctor.distributivity IsSemifunctor𝕘₁,₂ₛ◂s f g x = ◂s-associativity f g x

𝕗◂s : Nat → Semifunctor _ _ _ _ _ _
𝕗◂s N = 𝕘₁,₂ₛ N , (λ ‵ → _◂s_ ‵)

𝕒₂ : Action _ _ _
𝕒₂ = actionΣ Term

𝕒₂ₛ : Nat → Action _ _ _
𝕒₂ₛ N = actionΣ (Terms N)

instance

  IsSemigroupoidAction𝕘₁𝕒₂◂ : IsSemigroupoidAction 𝕘₁ 𝕒₂ _◂_
  IsSemigroupoidAction.extensionality IsSemigroupoidAction𝕘₁𝕒₂◂ {s₁ = s₁} refl f₁≡̇f₂ = ◂-extensionality f₁≡̇f₂ s₁
  IsSemigroupoidAction.associativity IsSemigroupoidAction𝕘₁𝕒₂◂ s f g = ◂-associativity f g s

  IsSemigroupoidAction𝕘₁𝕒₂ₛ◂s : ∀ {N} → IsSemigroupoidAction 𝕘₁ (𝕒₂ₛ N) (λ ‵ → _◂s_ ‵)
  IsSemigroupoidAction.extensionality IsSemigroupoidAction𝕘₁𝕒₂ₛ◂s {s₁ = s₁} refl f₁≡̇f₂ = ◂s-extensionality f₁≡̇f₂ s₁
  IsSemigroupoidAction.associativity IsSemigroupoidAction𝕘₁𝕒₂ₛ◂s s f g = ◂s-associativity f g s

𝕟◂ : SemigroupoidAction _ _ _ _ _
𝕟◂ = [ 𝕘₁ / 𝕒₂ ] _◂_

𝕟◂s : Nat → SemigroupoidAction _ _ _ _ _
𝕟◂s N = [ 𝕘₁ / 𝕒₂ₛ N ] (λ ‵ → _◂s_ ‵)

private

  ε : ∀ {m} → m ⊸ m
  ε = i

  mutual

    ◂-identity : ∀ {m} (t : Term m) → ε ◂ t ≡ t
    ◂-identity (i x) = refl
    ◂-identity leaf = refl
    ◂-identity (s fork t) = cong₂ _fork_ (◂-identity s) (◂-identity t)
    ◂-identity (function fn ts) = cong (function fn) (◂s-identity ts)

    ◂s-identity : ∀ {N m} (t : Vec (Term m) N) → ε ◂s t ≡ t
    ◂s-identity [] = refl
    ◂s-identity (t ∷ ts) = cong₂ _∷_ (◂-identity t) (◂s-identity ts)

  ∙-left-identity : ∀ {m n} (f : m ⊸ n) → ε ∙ f ≡̇ f
  ∙-left-identity f = ◂-identity ∘ f

  ∙-right-identity : ∀ {m n} (f : m ⊸ n) → f ∙ ε ≡̇ f
  ∙-right-identity _ _ = refl

instance

  IsCategory𝕘₁ε : IsCategory 𝕘₁ ε
  IsCategory.left-identity IsCategory𝕘₁ε = ∙-left-identity
  IsCategory.right-identity IsCategory𝕘₁ε = ∙-right-identity

𝔾₁ : Category _ _ _
𝔾₁ = 𝕘₁ , ε

𝔾₂ : Category _ _ _
𝔾₂ = 𝕘₂ , id

𝔾₂ₛ : Nat → Category _ _ _
𝔾₂ₛ N = 𝕘₂ₛ N , id

𝔾₁,₂ : Categories _ _ _ _ _ _
𝔾₁,₂ = 𝔾₁ , 𝔾₂

𝔾₁,₂ₛ : Nat → Categories _ _ _ _ _ _
𝔾₁,₂ₛ N = 𝔾₁ , 𝔾₂ₛ N

instance

  IsFunctor𝔾₁,₂◂ : IsFunctor 𝔾₁,₂ _◂_
  IsFunctor.identity IsFunctor𝔾₁,₂◂ _ = ◂-identity

𝔽◂ : Functor _ _ _ _ _ _
𝔽◂ = 𝔾₁,₂ , _◂_

instance

  IsFunctor𝔾₁,₂ₛ◂ : ∀ {N} → IsFunctor (𝔾₁,₂ₛ N) (λ ‵ → _◂s_ ‵)
  IsFunctor.identity IsFunctor𝔾₁,₂ₛ◂ _ = ◂s-identity -- ◂-identity

𝔽s : Nat → Functor _ _ _ _ _ _
𝔽s N = 𝔾₁,₂ₛ N , (λ ‵ → _◂s_ ‵)

instance

  IsCategoryAction𝔾₁𝕒₂◂ : IsCategoryAction 𝔾₁ 𝕒₂ _◂_
  IsCategoryAction.identity IsCategoryAction𝔾₁𝕒₂◂ = ◂-identity

  IsCategoryAction𝔾₁𝕒₂ₛ◂s : ∀ {N} → IsCategoryAction 𝔾₁ (𝕒₂ₛ N) (λ ‵ → _◂s_ ‵)
  IsCategoryAction.identity IsCategoryAction𝔾₁𝕒₂ₛ◂s = ◂s-identity

ℕ◂ : CategoryAction _ _ _ _ _
ℕ◂ = [ 𝔾₁ / 𝕒₂ ] _◂_

ℕ◂s : Nat → CategoryAction _ _ _ _ _
ℕ◂s N = [ 𝔾₁ / 𝕒₂ₛ N ] (λ ‵ → _◂s_ ‵)


text:
module Lemmachine.Default where
open import Lemmachine

resource : Hooks
resource = []

main = runResolve (toApp resource)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
import Lvl

-- TODO: Just testing how it goes with creating an axiomatic system
module Geometry.Test2 (Point : Set(Lvl.𝟎)) where

open import Functional
open import Logic.Propositional{Lvl.𝟎}
open import Logic.Predicate{Lvl.𝟎}{Lvl.𝟎}
open import Relator.Equals{Lvl.𝟎}{Lvl.𝟎}
-- open import Structure.Setoid.Uniqueness{Lvl.𝟎}{Lvl.𝟎}{Lvl.𝟎} hiding (Theorems)
open import Structure.Relator.Equivalence{Lvl.𝟎}{Lvl.𝟎}
open import Structure.Relator.Ordering{Lvl.𝟎}{Lvl.𝟎}
-- open import Structure.Relator.Properties{Lvl.𝟎}{Lvl.𝟎} hiding (Theorems)

-- A line of finite length
record Line : Set(Lvl.𝟎) where
  constructor line
  field
    a : Point
    b : Point

-- A circle
record Circle : Set(Lvl.𝟎) where
  constructor circle
  field
    middle : Point
    outer : Point

record Theory : Set(Lvl.𝐒(Lvl.𝟎)) where
  -- Symbols
  field
    PointOnLine : Point → Line → Set(Lvl.𝟎) -- The point lies on the line
    PointOnCircle : Point → Circle → Set(Lvl.𝟎) -- The point lies on the circle
    _≾_ : Line → Line → Set(Lvl.𝟎) -- Comparison of line length

  _≿_ : Line → Line → Set(Lvl.𝟎) -- Comparison of line length
  _≿_ l₁ l₂ = l₂ ≾ l₁

  _≋_ : Line → Line → Set(Lvl.𝟎) -- Equality of line length
  _≋_ l₁ l₂ = (l₁ ≾ l₂) ∧ (l₁ ≿ l₂)

  -- Axioms
  field
    [≾]-weak-total-order : Weak.TotalOrder(_≾_)(_≋_) -- (_≾_) is a weak total order

    point-on-line-existence : ∀{l : Line} → ∃(p ↦ PointOnLine(p)(l)) -- There is a point on a line
    endpoint1-on-line : ∀{l : Line} → PointOnLine(Line.a(l))(l)
    endpoint2-on-line : ∀{l : Line} → PointOnLine(Line.b(l))(l)
    single-point-line : ∀{p : Point}{x : Point} → PointOnLine(x) (line(p)(p)) → (x ≡ p) -- There is only a simgle point on a line of zero length

    point-on-circle-existence : ∀{c : Circle} → ∃(p ↦ PointOnCircle(p)(c)) -- There is a point on a circle
    outer-on-circle : ∀{c : Circle} → PointOnCircle(Circle.outer(c))(c)
    single-point-circle : ∀{p : Point}{x : Point} → PointOnCircle(x) (circle(p)(p)) → (x ≡ p) -- There is only a simgle point on a circle of zero radius

    line-symmetry : ∀{a : Point}{b : Point} → (line(a)(b) ≡ line(b)(a)) -- A line is non-directional

    circle-intersection : ∀{a : Point}{b : Point} → ∃(i ↦ PointOnCircle(i)(circle(a)(b)) ∧ PointOnCircle(i)(circle(b)(a))) ∧ ∃(i ↦ PointOnCircle(i)(circle(a)(b)) ∧ PointOnCircle(i)(circle(b)(a)))

module Theorems ⦃ _ : Theory ⦄ where
  open Theory ⦃ ... ⦄

  -- middlepoint : Line → Point
  -- middlepoint(line(a)(b)) =

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

-- Interface to the standard library.
-- Place to add own auxiliary definitions.

module Library where

open import Size         public
open import Level        public using () renaming (zero to lzero)

open import Data.Unit    public using (⊤)
open import Data.Empty   public using (⊥; ⊥-elim)
open import Data.Product public using (Σ; ∃; _×_; _,_; proj₁; proj₂; <_,_>; curry; uncurry) renaming (map to map-×)
open import Data.Sum     public using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′) renaming (map to map-⊎)

open import Data.List     public using (List; []; _∷_) hiding (module List)
open import Data.List.Relation.Unary.All public using (All; []; _∷_)  hiding (module All)
open import Data.List.Relation.Unary.Any public using (here; there)
open import Data.List.Membership.Propositional         public using (_∈_)
open import Data.List.Relation.Binary.Sublist.Propositional   public using (_⊆_; []; _∷_; _∷ʳ_; ⊆-refl; ⊆-trans) renaming (lookup to ⊆-lookup)

open import Function     public using (_∘_; _∘′_; id; _$_; _ˢ_; case_of_; const; flip)

open import Relation.Binary.PropositionalEquality public using (_≡_; refl; sym; trans; cong; cong₂; subst; _≗_)

{-# BUILTIN REWRITE _≡_ #-}

module All where
  open import Data.List.Relation.Unary.All public

module Any where
  open import Data.List.Relation.Unary.Any public

-- open import Axiom.Extensionality.Propositional    public using (Extensionality)
-- postulate
--   funExt : ∀{a b} → Extensionality a b  -- inline to avoid library incomp.

postulate
  funExt : ∀{a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x}
    → (∀ x → f x ≡ g x)
    → f ≡ g
  funExtH : ∀{a b} {A : Set a} {B : A → Set b} {f g : {x : A} → B x}
    → (∀ {x} → f {x} ≡ g {x})
    → (λ {x} → f {x}) ≡ g

⊥-elim-ext : ∀{a b} {A : Set a} {B : Set b} {f : A → ⊥} {g : A → B} → ⊥-elim {b} {B} ∘ f ≡ g
⊥-elim-ext {f = f} = funExt λ a → ⊥-elim (f a)

cong₃ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
        (f : A → B → C → D) {a a' b b' c c'} → a ≡ a' → b ≡ b' → c ≡ c' → f a b c ≡ f a' b' c'
cong₃ f refl refl refl = refl

_×̇_ : ∀{A B C D : Set} → (A → C) → (B → D) → A × B → C × D
(f ×̇ g) (x , y) = f x , g y

-- Application (S-combinator)

apply : ∀{A B C : Set} (f : C → A → B) (d : C → A) → C → B
apply f a = λ c → f c (a c)

-- Kripke application

kapply : ∀{A B C D : Set} (f : C → A → B) (τ : D → C) (d : D → A) → D → B
kapply f τ a = apply (f ∘ τ) a
-- kapply f τ a = λ d → f (τ d) (a d)

caseof : ∀{A B C D : Set} (f : C → A ⊎ B) (g : C × A → D) (h : C × B → D) → C → D
caseof f g h = λ c → [ curry g c , curry h c ]′ (f c)

sum-eta : ∀{A B : Set} (x : A ⊎ B) → [ inj₁ , inj₂ ] x ≡ x
sum-eta (inj₁ x) = refl
sum-eta (inj₂ y) = refl

caseof-eta : ∀{A B C : Set} (f : C → A ⊎ B) → caseof f (inj₁ ∘ proj₂) (inj₂ ∘ proj₂) ≡ f
caseof-eta f = funExt λ c → sum-eta (f c)

sum-perm : ∀{A B C D : Set} (k : C → D) {g : A → C} {h : B → C} (x : A ⊎ B) →
  [ k ∘ g , k ∘ h ]′ x ≡ k ([ g , h ]′ x)
sum-perm k (inj₁ x) = refl
sum-perm k (inj₂ y) = refl

caseof-perm' : ∀{A B C D E : Set}
  (k : C → D → E) {f : C → A ⊎ B} {g : C × A → D} {h : C × B → D} →
  caseof f (apply (k ∘ proj₁) g) (apply (k ∘ proj₁) h)
    ≡ apply k (caseof f g h)
caseof-perm' k {f} = funExt λ c → sum-perm (k c) (f c)

caseof-perm : ∀{A B C D E : Set} (k : D → E) {f : C → A ⊎ B} {g : C × A → D} {h : C × B → D}
  → caseof f (k ∘ g) (k ∘ h) ≡ k ∘ caseof f g h
caseof-perm = caseof-perm' ∘ const

caseof-wk : ∀{A B C D E : Set} (k : D → C) {f : C → A ⊎ B} {g : C × A → E} {h : C × B → E}
  → caseof (f ∘ k) (g ∘ (k ×̇ id)) (h ∘ (k ×̇ id)) ≡ caseof f g h ∘ k
caseof-wk {A} {B} {C} {D} {E} k {f} {g} {h} = refl

caseof-apply : ∀{A B C D E : Set}
  (f : C → A ⊎ B) {g : C × A → D → E} {h : C × B → D → E} (d : C → D)

  → caseof f (apply g (d ∘ proj₁)) (apply h (d ∘ proj₁))
     ≡ apply (caseof f g h) d

caseof-apply f {g} {h} d = funExt λ c → sum-perm (λ z → z (d c)) {curry g c} {curry h c} (f c)

-- caseof-apply {A} {B} {C} {D} {E} d {f} {g} {h} = funExt λ c → aux (f c)
--   where
--   aux : ∀ {c : C} (w : A ⊎ B) →
--       [ (λ y → curry g c y (d c)) , (λ y → curry h c y (d c)) ]′ w ≡
--       [ curry g c , curry h c ]′ w (d c)
--   aux (inj₁ a) = refl
--   aux (inj₂ b) = refl

-- caseof (f ∘ τ)
--       (apply (g ∘ (τ ×̇ id)) (a ∘ proj₁))
--       (apply (h ∘ (τ ×̇ id)) (a ∘ proj₁))
--       ≡
--       apply (caseof f g h ∘ τ) a

caseof-kapply : ∀{A B C D E F : Set}
  (f : C → A ⊎ B) (g : C × A → E → F) (h : C × B → E → F) (τ : D → C) (a : D → E)
  → caseof (f ∘ τ)
      (kapply g (τ ×̇ id) (a ∘ proj₁))
      (kapply h (τ ×̇ id) (a ∘ proj₁))
      ≡
    kapply (caseof f g h) τ a
caseof-kapply f g h τ a = caseof-apply (f ∘ τ) a

caseof-swap : ∀{A B C D X Y : Set}
    (f : C → X ⊎ Y)
    (i : C × X → A ⊎ B)
    (j : C × Y → A ⊎ B)
    (g : C → A → D)
    (h : C → B → D) →
    caseof f (caseof i (uncurry (g ∘ proj₁)) (uncurry (h ∘ proj₁)))
             (caseof j (uncurry (g ∘ proj₁)) (uncurry (h ∘ proj₁)))
      ≡ caseof (caseof f i j) (uncurry g) (uncurry h)
caseof-swap {A} {B} {C} {D} {X} {Y} f i j g h = funExt λ c →
  sum-perm [ (g c) , (h c) ] (f c)

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- The syntax of types with the Nehemiah plugin.
------------------------------------------------------------------------

module Nehemiah.Syntax.Type where

import Parametric.Syntax.Type as Type

data Base : Type.Structure where
  base-int : Base
  base-bag : Base

open Type.Structure Base public

pattern int = base base-int
pattern bag = base base-bag

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Relations between properties of scaling and other operations
------------------------------------------------------------------------

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

module Algebra.Module.Consequences where

open import Algebra.Core using (Op₂; Opₗ; Opᵣ)
import Algebra.Definitions as Defs
open import Algebra.Module.Definitions
open import Function.Base using (flip)
open import Level using (Level)
open import Relation.Binary using (Rel; Setoid)
import Relation.Binary.Reasoning.Setoid as Rea

private
  variable
    a b c ℓ ℓa : Level
    A : Set a
    B : Set b

module _ (_≈ᴬ_ : Rel {a} A ℓa) (S : Setoid c ℓ) where

  open Setoid S
  open Rea S
  open Defs _≈ᴬ_

  private
    module L = LeftDefs A _≈_
    module R = RightDefs A _≈_
    module B = BiDefs A A _≈_

  module _ {_*_ : Op₂ A} {_*ₗ_ : Opₗ A Carrier} where

    private
      _*ᵣ_ = flip _*ₗ_

    *ₗ-assoc+comm⇒*ᵣ-assoc :
      L.RightCongruent _≈ᴬ_ _*ₗ_ →
      L.Associative _*_ _*ₗ_ → Commutative _*_ → R.Associative _*_ _*ᵣ_
    *ₗ-assoc+comm⇒*ᵣ-assoc *ₗ-congʳ *ₗ-assoc *-comm m x y = begin
      (m *ᵣ x) *ᵣ y  ≈⟨ refl ⟩
      y *ₗ (x *ₗ m)  ≈˘⟨ *ₗ-assoc _ _ _ ⟩
      (y * x) *ₗ m   ≈⟨ *ₗ-congʳ (*-comm y x) ⟩
      (x * y) *ₗ m   ≈⟨ refl ⟩
      m *ᵣ (x * y)   ∎

    *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc :
      L.RightCongruent _≈ᴬ_ _*ₗ_ →
      L.Associative _*_ _*ₗ_ → Commutative _*_ → B.Associative _*ₗ_ _*ᵣ_
    *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc *ₗ-congʳ *ₗ-assoc *-comm x m y = begin
      ((x *ₗ m) *ᵣ y)  ≈⟨ refl ⟩
      (y *ₗ (x *ₗ m))  ≈˘⟨ *ₗ-assoc _ _ _ ⟩
      ((y * x) *ₗ m)   ≈⟨ *ₗ-congʳ (*-comm y x) ⟩
      ((x * y) *ₗ m)   ≈⟨ *ₗ-assoc _ _ _ ⟩
      (x *ₗ (y *ₗ m))  ≈⟨ refl ⟩
      (x *ₗ (m *ᵣ y))  ∎

  module _ {_*_ : Op₂ A} {_*ᵣ_ : Opᵣ A Carrier} where

    private
      _*ₗ_ = flip _*ᵣ_

    *ᵣ-assoc+comm⇒*ₗ-assoc :
      R.LeftCongruent _≈ᴬ_ _*ᵣ_ →
      R.Associative _*_ _*ᵣ_ → Commutative _*_ → L.Associative _*_ _*ₗ_
    *ᵣ-assoc+comm⇒*ₗ-assoc *ᵣ-congˡ *ᵣ-assoc *-comm x y m = begin
      ((x * y) *ₗ m)   ≈⟨ refl ⟩
      (m *ᵣ (x * y))   ≈⟨ *ᵣ-congˡ (*-comm x y) ⟩
      (m *ᵣ (y * x))   ≈˘⟨ *ᵣ-assoc _ _ _ ⟩
      ((m *ᵣ y) *ᵣ x)  ≈⟨ refl ⟩
      (x *ₗ (y *ₗ m))  ∎

    *ᵣ-assoc+comm⇒*ₗ-*ᵣ-assoc :
      R.LeftCongruent _≈ᴬ_ _*ᵣ_ →
      R.Associative _*_ _*ᵣ_ → Commutative _*_ → B.Associative _*ₗ_ _*ᵣ_
    *ᵣ-assoc+comm⇒*ₗ-*ᵣ-assoc *ᵣ-congˡ *ᵣ-assoc *-comm x m y = begin
      ((x *ₗ m) *ᵣ y)  ≈⟨ refl ⟩
      ((m *ᵣ x) *ᵣ y)  ≈⟨ *ᵣ-assoc _ _ _ ⟩
      (m *ᵣ (x * y))   ≈⟨ *ᵣ-congˡ (*-comm x y) ⟩
      (m *ᵣ (y * x))   ≈˘⟨ *ᵣ-assoc _ _ _ ⟩
      ((m *ᵣ y) *ᵣ x)  ≈⟨ refl ⟩
      (x *ₗ (m *ᵣ y))  ∎


text:
module Module where

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

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

import Data.Nat using (ℕ; zero; suc; _+_)


text:
-- Andreas, 2015-05-10  Report wrong hiding for copattern

{-# OPTIONS --copatterns #-}

record ⊤ : Set where

record Foo (A : Set) : Set where
  field
    foo : A

bar : Foo ⊤
Foo.foo {bar} = _

-- Error WAS: Unexpected implicit argument

-- Better error:
-- Wrong hiding used for projection  Foo.foo
-- when checking that the clause Foo.foo {bar} = _ has type Foo ⊤

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic definitions for Characters
------------------------------------------------------------------------

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

module Data.Char.Base where

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

------------------------------------------------------------------------
-- Re-export the type, and renamed primitives

open import Agda.Builtin.Char public using ( Char )
  renaming
  -- testing
  ( primIsLower    to isLower
  ; primIsDigit    to isDigit
  ; primIsAlpha    to isAlpha
  ; primIsSpace    to isSpace
  ; primIsAscii    to isAscii
  ; primIsLatin1   to isLatin1
  ; primIsPrint    to isPrint
  ; primIsHexDigit to isHexDigit
  -- transforming
  ; primToUpper to toUpper
  ; primToLower to toLower
  -- converting
  ; primCharToNat to toℕ
  ; primNatToChar to fromℕ
  )

open import Agda.Builtin.String public using ()
  renaming ( primShowChar to show )

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

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

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.1

toNat = toℕ
{-# WARNING_ON_USAGE toNat
"Warning: toNat was deprecated in v1.1.
Please use toℕ instead."
#-}

fromNat = fromℕ
{-# WARNING_ON_USAGE fromNat
"Warning: fromNat was deprecated in v1.1.
Please use fromℕ instead."
#-}


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

private
 variable
  A : Set
  a : A
  variable
   A : Set
 private
  A = B
   where
    B = Set

max_stars_repo_name: dubinsky/intellij-dtlc

max_issues_repo_name: dubinsky/intellij-dtlc

max_forks_repo_name: dubinsky/intellij-dtlc


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

module Categories.Category.Instance.Properties.Setoids.Choice where

open import Categories.Category using (Category)
open import Categories.Category.Exact using (Exact)
open import Categories.Category.Instance.Setoids using (Setoids)

open import Data.Product using (∃; proj₁; proj₂; _,_; Σ-syntax; _×_; -,_; map; zip; swap; map₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function.Equality as SΠ using (Π; _⇨_) renaming (id to ⟶-id; _∘_ to _∘⟶_)

open import Level
open import Relation.Binary using (Setoid; Rel; REL; IsEquivalence)
import Relation.Binary.Reasoning.Setoid as SR

open import Data.Nat.Base
import Relation.Binary.PropositionalEquality.Core as P

open Setoid renaming (_≈_ to [_][_≈_]; Carrier to ∣_∣) using (isEquivalence; refl; sym; trans)
open Π using (_⟨$⟩_; cong)

module _ ℓ where
  private
    S = Setoids ℓ ℓ
    open Category S hiding (_≈_)
    module S = Category S

  open import Categories.Category.Instance.Properties.Setoids.Exact
  open import Categories.Object.InternalRelation using (Relation)

  -- Presentation axiom, aka CoSHEP (http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/presentation+axiom)
  record CoSHEP (A : Setoid ℓ ℓ) : Set (Level.suc ℓ) where
    field
      {P} : Setoid ℓ ℓ
      pre   : P ⇒ A
      surj  : SSurj ℓ pre
      split : {X : Setoid ℓ ℓ} (f : X ⇒ P) → SSurj ℓ f → Σ[ g ∈ ∣ P ⇨ X ∣ ] [ P ⇨ P ][ f ∘ g ≈ id ]

  Setoid-CoSHEP : (A : Setoid ℓ ℓ) → CoSHEP A
  Setoid-CoSHEP A = record
    { P = record
           { Carrier = ∣ A ∣
           ; _≈_ = P._≡_
           ; isEquivalence = record { refl = P.refl ; sym = P.sym ; trans = P.trans }
           }
    ; pre = record
           { _⟨$⟩_ = λ x → x
           ; cong = λ {x} eq → P.subst (λ z → [ A ][ x ≈ z ]) eq (refl A)
           }
    ; surj = λ x → x , refl A
    ; split = λ {X} f surj → record
           { _⟨$⟩_ = λ y → let x , _ = surj y in x
           ; cong = λ {x}{y} x≡y → P.subst (λ z → [ X ][ proj₁ (surj x) ≈ proj₁ (surj z) ]) x≡y (refl X)
           }
           , λ {x}{y} x≡y → let z , eq = surj x in P.trans eq x≡y
    }

  entire : {A B : Setoid ℓ ℓ} → (R : Relation S A B) → Set ℓ
  entire {A} R = ∀ (x : ∣ A ∣) →  Σ[ e ∈ ∣ dom ∣ ]  [ A ][ p₁ ⟨$⟩ e ≈ x ]
    where open Relation R

  ℕ-Setoid : Setoid ℓ ℓ
  ℕ-Setoid = record { Carrier = Lift _ ℕ ; _≈_ = P._≡_  ; isEquivalence = record { refl = P.refl ; sym = P.sym ; trans = P.trans } }

  record DepChoice {A : Setoid ℓ ℓ} (R : Relation S A A) (inhb : ∣ A ∣) (ent : entire R) : Set (Level.suc ℓ) where
    open Relation R

    field
      pair   : ℕ → ∣ dom ∣
      chain  : ∀ (n : ℕ) → [ A ][ p₁ ⟨$⟩ pair (ℕ.suc n) ≈ p₂ ⟨$⟩ pair n ]

  -- Dependent choice for setoids
  Setoid-DepChoice :  {A : Setoid ℓ ℓ} (R : Relation S A A) (inhb : ∣ A ∣) (ent : entire R) → DepChoice R inhb ent
  Setoid-DepChoice {A} R inhb ent = record
    { pair  = pair
    ; chain = chain
    }
      where
        open Relation R

        pair : ℕ → ∣ dom ∣
        pair ℕ.zero = proj₁ (ent inhb)
        pair (ℕ.suc n) = let x , _ = ent (p₂ ⟨$⟩ pair n) in x

        chain : (n : ℕ) → [ A ][ p₁ ⟨$⟩ proj₁ (ent (p₂ ⟨$⟩ pair n)) ≈ p₂ ⟨$⟩ pair n ]
        chain ℕ.zero    = let _ , eq = ent (p₂ ⟨$⟩ proj₁ (ent inhb)) in eq
        chain (ℕ.suc n) = let x , eq = ent (p₂ ⟨$⟩ proj₁ (ent (p₂ ⟨$⟩ pair n))) in eq

  -- Countable choice for setoids
  ℕ-Choice :  ∀ {A : Setoid ℓ ℓ} (f : A ⇒ ℕ-Setoid) → SSurj ℓ f → Σ[ g ∈ ∣ ℕ-Setoid ⇨ A ∣ ] [ ℕ-Setoid ⇨ ℕ-Setoid ][ f ∘ g ≈ id ]
  ℕ-Choice {A} f surj = record
    { _⟨$⟩_ = λ n → let x , eq = surj n in x
    ; cong = λ {n}{m} eq → let x , _ = surj n; y , _ = surj m in P.subst (λ m → [ A ][ proj₁ (surj n) ≈ proj₁ (surj m) ]) eq (refl A)
    }
    , λ {n}{m} n≡m → let _ , eq = surj n in P.trans eq n≡m

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:
------------------------------------------------------------------------
-- Properties of functions
------------------------------------------------------------------------

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

module Math.Combinatorics.ListFunction.Properties where

-- agda-stdlib
open import Data.List hiding (_∷ʳ_)
import Data.List.Properties as Lₚ
open import Data.List.Membership.Propositional using (_∈_; _∉_)
import Data.List.Membership.Propositional.Properties as ∈ₚ
open import Data.List.Relation.Binary.BagAndSetEquality
open import Data.List.Relation.Binary.Sublist.Propositional using (_⊆_; []; _∷_; _∷ʳ_)
import Data.List.Relation.Binary.Sublist.Propositional.Properties as Sublistₚ
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
import Data.List.Relation.Unary.All.Properties as Allₚ
open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
import Data.List.Relation.Unary.Unique.Propositional as UniqueP
import Data.List.Relation.Unary.Unique.Propositional.Properties as UniquePₚ
import Data.List.Relation.Unary.Unique.Setoid as UniqueS
import Data.List.Relation.Unary.Unique.Setoid.Properties as UniqueSₚ
open import Data.Nat
open import Data.Product as Prod using (_×_; _,_; ∃; proj₁; proj₂)
open import Data.Sum using (inj₁; inj₂)
open import Function.Base
open import Function.Equivalence using (_⇔_; equivalence) -- TODO: use new packages
open import Relation.Binary.PropositionalEquality as P

-- agda-combinatorics
open import Math.Combinatorics.Function
open import Math.Combinatorics.Function.Properties
open import Math.Combinatorics.ListFunction
import Math.Combinatorics.ListFunction.Properties.Lemma as Lemma

------------------------------------------------------------------------
-- Properties of `applyEach`

module _ {a} {A : Set a} where
  open ≡-Reasoning

  length-applyEach : ∀ (f : A → A) (xs : List A) →
                     length (applyEach f xs) ≡ length xs
  length-applyEach f []       = refl
  length-applyEach f (x ∷ xs) = begin
    1 + length (map (x ∷_) (applyEach f xs))
      ≡⟨ cong suc $ Lₚ.length-map (x ∷_) (applyEach f xs ) ⟩
    1 + length (applyEach f xs)
      ≡⟨ cong suc $ length-applyEach f xs ⟩
    1 + length xs
      ∎

  All-length-applyEach : ∀ (f : A → A) (xs : List A) →
                         All (λ ys → length ys ≡ length xs) (applyEach f xs)
  All-length-applyEach f []       = []
  All-length-applyEach f (x ∷ xs) =
    refl ∷ (Allₚ.map⁺ $ All.map (cong suc) $ All-length-applyEach f xs)

  applyEach-cong : ∀ (f g : A → A) (xs : List A) →
    (∀ x → f x ≡ g x) → applyEach f xs ≡ applyEach g xs
  applyEach-cong f g []       f≡g = refl
  applyEach-cong f g (x ∷ xs) f≡g = begin
    (f x ∷ xs) ∷ map (_∷_ x) (applyEach f xs)
      ≡⟨ cong₂ (λ u v → (u ∷ xs) ∷ map (_∷_ x) v) (f≡g x) (applyEach-cong f g xs f≡g) ⟩
    (g x ∷ xs) ∷ map (_∷_ x) (applyEach g xs)
      ∎

------------------------------------------------------------------------
-- Properties of `combinations`

module _ {a} {A : Set a} where
  open ≡-Reasoning

  length-combinations : ∀ (k : ℕ) (xs : List A) →
                        length (combinations k xs) ≡ C (length xs) k
  length-combinations 0       xs       = refl
  length-combinations (suc k) []       = refl
  length-combinations (suc k) (x ∷ xs) = begin
    length (map (x ∷_) (combinations k xs) ++ combinations (suc k) xs)
      ≡⟨ Lₚ.length-++ (map (x ∷_) (combinations k xs)) ⟩
    length (map (x ∷_) (combinations k xs)) + length (combinations (suc k) xs)
      ≡⟨ cong₂ _+_ (Lₚ.length-map (x ∷_) (combinations k xs)) refl ⟩
    length (combinations k xs) + length (combinations (suc k) xs)
      ≡⟨ cong₂ _+_ (length-combinations k xs) (length-combinations (suc k) xs) ⟩
    C (length xs) k + C (length xs) (suc k)
      ≡⟨ sym $ C[1+n,1+k]≡C[n,k]+C[n,1+k] (length xs) k ⟩
    C (length (x ∷ xs)) (suc k)
      ∎

  All-length-combinations : ∀ (k : ℕ) (xs : List A) →
                            All (λ ys → length ys ≡ k) (combinations k xs)
  All-length-combinations 0       xs       = refl ∷ []
  All-length-combinations (suc k) []       = []
  All-length-combinations (suc k) (x ∷ xs) =
    Allₚ.++⁺ (Allₚ.map⁺ $ All.map (cong suc) $ All-length-combinations k xs)
             (All-length-combinations (suc k) xs)

  ∈-length-combinations : ∀ (xs : List A) k ys → xs ∈ combinations k ys → length xs ≡ k
  ∈-length-combinations xs k ys xs∈combinations[k,ys] =
    All.lookup (All-length-combinations k ys) xs∈combinations[k,ys]

  combinations-⊆⇒∈ : ∀ {xs ys : List A} → xs ⊆ ys → xs ∈ combinations (length xs) ys
  combinations-⊆⇒∈ {[]}     {ys}     xs⊆ys              = here refl
  combinations-⊆⇒∈ {x ∷ xs} {y ∷ ys} (.y  ∷ʳ x∷xs⊆ys)   =
    ∈ₚ.∈-++⁺ʳ (map (y ∷_) (combinations (length xs) ys)) (combinations-⊆⇒∈ x∷xs⊆ys)
  combinations-⊆⇒∈ {x ∷ xs} {.x ∷ ys} (refl ∷  xs⊆ys)   =
    ∈ₚ.∈-++⁺ˡ $ ∈ₚ.∈-map⁺ (x ∷_) $ combinations-⊆⇒∈ xs⊆ys

  combinations-∈⇒⊆ : ∀ {xs ys : List A} → xs ∈ combinations (length xs) ys → xs ⊆ ys
  combinations-∈⇒⊆ {[]}     {ys}     _                       = Lemma.[]⊆xs ys
  combinations-∈⇒⊆ {x ∷ xs} {y ∷ ys} x∷xs∈c[len[x∷xs],y∷ys]
    with ∈ₚ.∈-++⁻ (map (y ∷_) (combinations (length xs) ys)) x∷xs∈c[len[x∷xs],y∷ys]
  ... | inj₁ x∷xs∈map[y∷-][c[len[xs],ys]]
      with ∈ₚ.∈-map⁻ (y ∷_) x∷xs∈map[y∷-][c[len[xs],ys]] -- ∷ ∃ λ zs → zs ∈ combinations (length xs) ys × x ∷ xs ≡ y ∷ zs
  combinations-∈⇒⊆ {x ∷ xs} {y ∷ ys} _ | inj₁ _
         | zs , (zs∈c[len[xs],ys] , x∷xs≡y∷zs) = x≡y ∷ xs⊆ys
    where
    xs≡zs : xs ≡ zs
    xs≡zs = Lₚ.∷-injectiveʳ x∷xs≡y∷zs
    x≡y : x ≡ y
    x≡y = Lₚ.∷-injectiveˡ x∷xs≡y∷zs
    xs⊆ys : xs ⊆ ys
    xs⊆ys = combinations-∈⇒⊆ $ subst (λ v → v ∈ combinations (length xs) ys)
                                      (sym xs≡zs) zs∈c[len[xs],ys]
  combinations-∈⇒⊆ {x ∷ xs} {y ∷ ys} _ | inj₂ x∷xs∈c[len[x∷xs],ys] = y ∷ʳ x∷xs⊆ys
    where
    x∷xs⊆ys : x ∷ xs ⊆ ys
    x∷xs⊆ys = combinations-∈⇒⊆ x∷xs∈c[len[x∷xs],ys]

  combinations-∈⇔⊆ : ∀ {xs ys : List A} → (xs ∈ combinations (length xs) ys) ⇔ (xs ⊆ ys)
  combinations-∈⇔⊆ = equivalence combinations-∈⇒⊆ combinations-⊆⇒∈

  All-⊆-combinations : ∀ k (xs : List A) → All (_⊆ xs) (combinations k xs)
  All-⊆-combinations k xs = All.tabulate λ {ys} ys∈combinations[k,xs] →
    combinations-∈⇒⊆ $ subst (λ v → ys ∈ combinations v xs)
      (sym $ ∈-length-combinations ys k xs ys∈combinations[k,xs])
      ys∈combinations[k,xs]

  combinations-∈⇒⊆∧length : ∀ {xs : List A} {k ys} →
                            xs ∈ combinations k ys → (xs ⊆ ys × length xs ≡ k)
  combinations-∈⇒⊆∧length {xs} {k} {ys} xs∈c[k,ys] =
    combinations-∈⇒⊆ xs∈c[len[xs],ys] , length[xs]≡k
    where
    length[xs]≡k : length xs ≡ k
    length[xs]≡k = ∈-length-combinations xs k ys xs∈c[k,ys]
    xs∈c[len[xs],ys] : xs ∈ combinations (length xs) ys
    xs∈c[len[xs],ys] =
      subst (λ v → xs ∈ combinations v ys) (sym length[xs]≡k) xs∈c[k,ys]

  combinations-⊆∧length⇒∈ : ∀ {xs ys : List A} {k} →
    (xs ⊆ ys × length xs ≡ k) → xs ∈ combinations k ys
  combinations-⊆∧length⇒∈ {xs} {ys} {k} (xs⊆ys , len[xs]≡k) =
    subst (λ v → xs ∈ combinations v ys) len[xs]≡k (combinations-⊆⇒∈ xs⊆ys)

  combinations-∈⇔⊆∧length : ∀ {xs : List A} {k} {ys} →
                            xs ∈ combinations k ys ⇔ (xs ⊆ ys × length xs ≡ k)
  combinations-∈⇔⊆∧length =
    equivalence combinations-∈⇒⊆∧length combinations-⊆∧length⇒∈

  unique-combinations : ∀ k {xs : List A} →
    UniqueP.Unique xs → UniqueP.Unique (combinations k xs)
  unique-combinations 0      {xs}      xs-unique                = [] ∷ []
  unique-combinations (suc k) {[]}     xs-unique                = []
  unique-combinations (suc k) {x ∷ xs} (All[x≢-]xs ∷ xs-unique) =
    UniquePₚ.++⁺ {_} {_} {map (x ∷_) (combinations k xs)} {combinations (suc k) xs}
      (UniquePₚ.map⁺ Lₚ.∷-injectiveʳ (unique-combinations k {xs} xs-unique))
      (unique-combinations (suc k) {xs} xs-unique)
      λ {vs} vs∈map[x∷-]c[k,xs]×vs∈c[1+k,xs] →
      let
        vs∈map[x∷-]c[k,xs] = proj₁ vs∈map[x∷-]c[k,xs]×vs∈c[1+k,xs]
        vs∈c[1+k,xs] = proj₂ vs∈map[x∷-]c[k,xs]×vs∈c[1+k,xs]
        proof = ∈ₚ.∈-map⁻ (x ∷_) vs∈map[x∷-]c[k,xs]
        us = proj₁ proof
        vs≡x∷us : vs ≡ x ∷ us
        vs≡x∷us = proj₂ (proj₂ proof)
        x∈vs : x ∈ vs
        x∈vs = subst (x ∈_) (sym vs≡x∷us) (here refl)
        vs⊆xs : vs ⊆ xs
        vs⊆xs = proj₁ $ combinations-∈⇒⊆∧length {vs} {suc k} {xs} vs∈c[1+k,xs]
        All[x≢-]vs : All (x ≢_) vs
        All[x≢-]vs = Sublistₚ.All-resp-⊆ vs⊆xs All[x≢-]xs
        x∉vs : x ∉ vs
        x∉vs = Allₚ.All¬⇒¬Any All[x≢-]vs
      in x∉vs x∈vs
  {-
  --   unique⇒drop-cons-set : ∀ {a} {A : Set a} {x : A} {xs ys} →
  unique-combinations-set : ∀ k {xs : List A} →
    UniqueP.Unique xs → UniqueS.Unique ([ set ]-Equality A) (combinations k xs)
  unique-combinations-set 0                xs-unique          = [] ∷ []
  unique-combinations-set (suc k) {[]}     xs-unique          = []
  unique-combinations-set (suc k) {x ∷ xs} (this ∷ xs-unique) =
    UniqueSₚ.++⁺ ([ set ]-Equality A)
      (UniqueSₚ.map⁺ ([ set ]-Equality A) ([ set ]-Equality A) (λ → {!   !}) (unique-combinations-set k {xs} xs-unique))
      (unique-combinations-set (suc k) {xs} xs-unique)
      {!   !}
  -- {- x∉xs -} Unique -[ set ] xs → Unique -[ set ] (x ∷ xs)
  -}

module _ {a b} {A : Set a} {B : Set b} where
  combinations-map : ∀ k (f : A → B) (xs : List A) →
    combinations k (map f xs) ≡ map (map f) (combinations k xs)
  combinations-map 0       f xs       = refl
  combinations-map (suc k) f []       = refl
  combinations-map (suc k) f (x ∷ xs) = begin
    map (f x ∷_) (combinations k (map f xs)) ++ combinations (suc k) (map f xs)
      ≡⟨ cong₂ _++_ (cong (map (f x ∷_)) (combinations-map k f xs)) (combinations-map (suc k) f xs) ⟩
    map (f x ∷_) (map (map f) (combinations k xs)) ++ map (map f) (combinations (suc k) xs)
      ≡⟨ cong (_++ map (map f) (combinations (suc k) xs)) $ Lemma.lemma₁ f x (combinations k xs) ⟩
    map (map f) (map (x ∷_) (combinations k xs)) ++ map (map f) (combinations (suc k) xs)
      ≡⟨ sym $ Lₚ.map-++-commute (map f) (map (x ∷_) (combinations k xs)) (combinations (suc k) xs) ⟩
    map (map f) (map (x ∷_) (combinations k xs) ++ combinations (suc k) xs)
      ∎
    where open ≡-Reasoning

------------------------------------------------------------------------
-- Properties of `combinationsWithComplement`

module _ {a} {A : Set a} where
  open ≡-Reasoning

  map-proj₁-combinationsWithComplement : ∀ k (xs : List A) →
    map proj₁ (combinationsWithComplement k xs) ≡ combinations k xs
  map-proj₁-combinationsWithComplement 0       xs       = refl
  map-proj₁-combinationsWithComplement (suc k) []       = refl
  map-proj₁-combinationsWithComplement (suc k) (x ∷ xs) = begin
    map proj₁ (map f ys ++ map g zs)
      ≡⟨ Lₚ.map-++-commute proj₁ (map f ys) (map g zs) ⟩
    map proj₁ (map f ys) ++ map proj₁ (map g zs)
      ≡⟨ sym $ Lₚ.map-compose ys ⟨ cong₂ _++_ ⟩ Lₚ.map-compose zs ⟩
    map (proj₁ ∘′ f) ys ++ map (λ v → proj₁ (g v)) zs
      ≡⟨ Lₚ.map-cong lemma₁ ys ⟨ cong₂ _++_ ⟩ Lₚ.map-cong lemma₂ zs ⟩
    map ((x ∷_) ∘′ proj₁) ys ++ map proj₁ zs
      ≡⟨ cong (_++ map proj₁ zs) $ Lₚ.map-compose ys ⟩
    map (x ∷_) (map proj₁ ys) ++ map proj₁ zs
      ≡⟨ cong (map (x ∷_)) (map-proj₁-combinationsWithComplement k xs) ⟨ cong₂ _++_ ⟩ map-proj₁-combinationsWithComplement (suc k) xs ⟩
    map (x ∷_) (combinations k xs) ++ combinations (suc k) xs
      ∎
    where
    ys = combinationsWithComplement k xs
    zs = combinationsWithComplement (suc k) xs
    f g : List A × List A → List A × List A
    f = Prod.map₁ (x ∷_)
    g = Prod.map₂ (x ∷_)
    lemma₁ : ∀ (t : List A × List A) → proj₁ (Prod.map₁ (x ∷_) t) ≡ x ∷ proj₁ t
    lemma₁ t = Lemma.proj₁-map₁ (x ∷_) t
    lemma₂ : ∀ (t : List A × List A) → Lemma.proj₁′ {_} {_} {_} {List A} (Prod.map₂ (x ∷_) t) ≡ proj₁ t
    lemma₂ t = Lemma.proj₁-map₂ (x ∷_) t

  length-combinationsWithComplement : ∀ k (xs : List A) →
    length (combinationsWithComplement k xs) ≡ C (length xs) k
  length-combinationsWithComplement k xs = begin
    length (combinationsWithComplement k xs)
      ≡⟨ sym $ Lₚ.length-map proj₁ (combinationsWithComplement k xs) ⟩
    length (map proj₁ (combinationsWithComplement k xs))
      ≡⟨ cong length $ map-proj₁-combinationsWithComplement k xs ⟩
    length (combinations k xs)
      ≡⟨ length-combinations k xs ⟩
    C (length xs) k
      ∎

------------------------------------------------------------------------
-- Properties of `splits₂`

module _ {a} {A : Set a} where
  open ≡-Reasoning
  open Prod using (map₁; map₂)

  length-splits₂ : ∀ (xs : List A) → length (splits₂ xs) ≡ 1 + length xs
  length-splits₂ []       = refl
  length-splits₂ (x ∷ xs) = begin
    1 + length (map (map₁ (x ∷_)) (splits₂ xs))
      ≡⟨ cong (1 +_) $ Lₚ.length-map (map₁ (x ∷_)) (splits₂ xs) ⟩
    1 + length (splits₂ xs)
      ≡⟨ cong (1 +_) $ length-splits₂ xs ⟩
    1 + length (x ∷ xs)
      ∎

  splits₂-defn : ∀ (xs : List A) → splits₂ xs ≡ zip (inits xs) (tails xs)
  splits₂-defn []       = refl
  splits₂-defn (x ∷ xs) = begin
    splits₂ (x ∷ xs) ≡⟨⟩
    ([] , x ∷ xs) ∷ map (map₁ (x ∷_)) (splits₂ xs)
      ≡⟨ cong (([] , x ∷ xs) ∷_) (begin
        map (map₁ (x ∷_)) (splits₂ xs)
          ≡⟨ cong (map (map₁ (x ∷_))) $ splits₂-defn xs ⟩
        map (map₁ (x ∷_)) (zip is ts)
          ≡⟨ Lₚ.map-zipWith _,_ (map₁ (x ∷_)) is ts ⟩
        zipWith (λ ys zs → map₁ (x ∷_) (ys , zs)) is ts
          ≡⟨ sym $ Lₚ.zipWith-map _,_ (x ∷_) id is ts ⟩
        zip (map (x ∷_) is) (map id ts)
          ≡⟨ cong (zip (map (x ∷_) is)) $ Lₚ.map-id ts ⟩
        zip (map (x ∷_) is) ts
          ∎) ⟩
    ([] , x ∷ xs) ∷ zip (map (x ∷_) is) ts
      ∎
    where
    is = inits xs
    ts = tails xs

  All-++-splits₂ : (xs : List A) →
    All (Prod.uncurry (λ ys zs → ys ++ zs ≡ xs)) (splits₂ xs)
  All-++-splits₂ []       = refl ∷ []
  All-++-splits₂ (x ∷ xs) =
    All._∷_ refl $ Allₚ.map⁺ $ All.map (cong (x ∷_)) $ All-++-splits₂ xs

  splits₂-∈⇒++ : {xs ys zs : List A} → (ys , zs) ∈ splits₂ xs → ys ++ zs ≡ xs
  splits₂-∈⇒++ {xs = xs} = All.lookup (All-++-splits₂ xs)

  private
    [],xs∈splits₂[xs] : (xs : List A) → ([] , xs) ∈ splits₂ xs
    [],xs∈splits₂[xs] []       = here refl
    [],xs∈splits₂[xs] (x ∷ xs) = here refl

  ∈-split₂-++ : (xs ys : List A) → (xs , ys) ∈ splits₂ (xs ++ ys)
  ∈-split₂-++ []       ys = [],xs∈splits₂[xs] ys
  ∈-split₂-++ (x ∷ xs) ys =
    Any.there $ ∈ₚ.∈-map⁺ (map₁ (x ∷_)) $ ∈-split₂-++ xs ys

  splits₂-++⇒∈ : {xs ys zs : List A} → xs ++ ys ≡ zs → (xs , ys) ∈ splits₂ zs
  splits₂-++⇒∈ {xs} {ys} {zs} xs++ys≡zs =
    subst (λ v → (xs , ys) ∈ splits₂ v) xs++ys≡zs (∈-split₂-++ xs ys)

  splits₂-∈⇔++ : {xs ys zs : List A} → (xs , ys) ∈ splits₂ zs ⇔ xs ++ ys ≡ zs
  splits₂-∈⇔++ = equivalence splits₂-∈⇒++ splits₂-++⇒∈

module _ {a b} {A : Set a} {B : Set b} where
  open ≡-Reasoning

  {-
  splits₂-map : ∀ (f : A → B) (xs : List A) →
    splits₂ (map f xs) ≡ map (Prod.map (map f) (map f)) (splits₂ xs)
  splits₂-map f []       = refl
  splits₂-map f (x ∷ xs) = {!   !}
  -}
  -- length[xs]<k⇒combinations[k,xs]≡[]
  -- All-unique-combinations : UniqueP.Unique xs → All (UniqueP.Unique) (combinations k xs)
  -- All-unique-combinations-set : UniqueP.Unique xs → All (UniqueS.Unique [ set ]-Equality A) (combinations k xs)
  -- unique-combinations-PW : UniqueS.Unique S xs → UniqueS.Unique (Equality S) (combinations k xs)
  -- unique-combinations-set : UniqueP.Unique xs → Unique (_-[ set ]_) (combinations k xs)
  -- sorted-combinations : Sorted _<_ xs → Sorted {- Lex._<_ _<_ -} (combinations k xs)
  -- All-sorted-combinations : Sorted _<_ xs → All (Sorted _<_) (combinations k xs)
  -- filter-combinations = filter P ∘ combinations k xs
  -- each-disjoint-combinationsWithComplement : Unique zs → (xs , ys) ∈ combinationsWithComplement k zs → Disjoint xs ys
  -- combinationsWithComplement-∈⇒⊆ : (xs , ys) ∈ combinationsWithComplement (length xs) zs → xs ⊆ zs × ys ⊆ zs
  -- length-splits : length (splits k xs) ≡ C (length xs + k ∸ 1) (length xs)
  -- length-partitionsAll : length (partitionsAll xs) ≡ B (length xs)
  -- length-insertEverywhere : length (insertEverywhere x xs) ≡ 1 + length xs
  -- All-length-insertEverywhere : All (λ ys → length ys ≡ 1 + length xs) (insertEverywhere x xs)
  -- length-permutations : length (permutations xs) ≡ length xs !


text:
-- Andreas, 2017-11-01, issue #2824
-- allow built-in pragmas in parametrized modules

data Nat : Set where
  zero : Nat
  suc : Nat → Nat

module M (A : Set) where

  {-# BUILTIN NATURAL Nat #-}

  test = 5

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Common.Prelude
open import Common.Reflection

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

idTerm : Term
idTerm = lam visible (abs "x" (def (quote id) (arg₁ ∷ arg₂ ∷ [])))
  where
    arg₁ = arg (argInfo hidden relevant) (def (quote Nat) [])
    arg₂ = arg (argInfo visible relevant) (var 0 [])

-- Should fail since idTerm "λ z → id {Nat} z"
id₂ : {A : Set} → A → A
id₂ = unquote (give idTerm)


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

module Cubical.Categories.Adjoint where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation
open import Cubical.Foundations.Isomorphism

open Functor

open Iso
open Precategory

{-
==============================================
                  Overview
==============================================

This module contains two definitions for adjoint
functors, and functions witnessing their
logical (and maybe eventually actual?)
equivalence.
-}

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

{-
==============================================
             Adjoint definitions
==============================================

We provide two alternative definitions for
adjoint functors: the unit-counit
definition, followed by the natural bijection
definition.
-}

module UnitCounit where

  -- Adjoint def 1: unit-counit
  record _⊣_ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor C D) (G : Functor D C)
                  : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
    field
      -- unit
      η : 𝟙⟨ C ⟩ ⇒ (funcComp G F)
      -- counit
      ε : (funcComp F G) ⇒ 𝟙⟨ D ⟩
      -- triangle identities
      Δ₁ : PathP (λ i → NatTrans (F-lUnit {F = F} i) (F-rUnit {F = F} i))
        (seqTransP F-assoc (F ∘ʳ η) (ε ∘ˡ F))
        (1[ F ])
      Δ₂ : PathP (λ i → NatTrans (F-rUnit {F = G} i) (F-lUnit {F = G} i))
        (seqTransP (sym F-assoc) (η ∘ˡ G) (G ∘ʳ ε))
        (1[ G ])

  {-
   Helper function for building unit-counit adjunctions between categories,
   using that equality of natural transformations in a category is equality on objects
  -}

  module _ {ℓC ℓC' ℓD ℓD'}
    {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} {F : Functor C D} {G : Functor D C}
    ⦃ isCatC : isCategory C ⦄ ⦃ isCatD : isCategory D ⦄
    (η : 𝟙⟨ C ⟩ ⇒ (funcComp G F))
    (ε : (funcComp F G) ⇒ 𝟙⟨ D ⟩)
    (Δ₁ : ∀ c → F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ≡ D .id (F ⟅ c ⟆))
    (Δ₂ : ∀ d → η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫ ≡ C .id (G ⟅ d ⟆))
    where

    make⊣ : F ⊣ G
    make⊣ ._⊣_.η = η
    make⊣ ._⊣_.ε = ε
    make⊣ ._⊣_.Δ₁ =
      makeNatTransPathP F-lUnit F-rUnit
        (funExt λ c → cong (D ._⋆_ (F ⟪ η ⟦ c ⟧ ⟫)) (transportRefl _) ∙ Δ₁ c)
    make⊣ ._⊣_.Δ₂ =
      makeNatTransPathP F-rUnit F-lUnit
        (funExt λ d → cong (C ._⋆_ (η ⟦ G ⟅ d ⟆ ⟧)) (transportRefl _) ∙ Δ₂ d)

module NaturalBijection where
  -- Adjoint def 2: natural bijection
  record _⊣_ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor C D) (G : Functor D C) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
    field
      adjIso : ∀ {c d} → Iso (D [ F ⟅ c ⟆ , d ]) (C [ c , G ⟅ d ⟆ ])

    infix 40 _♭
    infix 40 _♯
    _♭ : ∀ {c d} → (D [ F ⟅ c ⟆ , d ]) → (C [ c , G ⟅ d ⟆ ])
    (_♭) {_} {_} = adjIso .fun

    _♯ : ∀ {c d} → (C [ c , G ⟅ d ⟆ ]) → (D [ F ⟅ c ⟆ , d ])
    (_♯) {_} {_} = adjIso .inv

    field
      adjNatInD : ∀ {c : C .ob} {d d'} (f : D [ F ⟅ c ⟆ , d ]) (k : D [ d , d' ])
                → (f ⋆⟨ D ⟩ k) ♭ ≡ f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫

      adjNatInC : ∀ {c' c d} (g : C [ c , G ⟅ d ⟆ ]) (h : C [ c' , c ])
                → (h ⋆⟨ C ⟩ g) ♯ ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯

{-
==============================================
            Proofs of equivalence
==============================================

This first unnamed module provides a function
adj'→adj which takes you from the second
definition to the first.

The second unnamed module does the reverse.
-}

module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor C D) (G : Functor D C) where
  open UnitCounit
  open NaturalBijection renaming (_⊣_ to _⊣²_)
  module _ (adj : F ⊣² G) where
    open _⊣²_ adj
    open _⊣_

    -- Naturality condition implies that a commutative square in C
    -- appears iff the transpose in D is commutative as well
    -- Used in adj'→adj
    adjNat' : ∀ {c c' d d'} {f : D [ F ⟅ c ⟆ , d ]} {k : D [ d , d' ]}
            → {h : C [ c , c' ]} {g : C [ c' , G ⟅ d' ⟆ ]}
            -- commutativity of squares is iff
            → ((f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯) → (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g))
            × ((f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g) → (f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯))
    adjNat' {c} {c'} {d} {d'} {f} {k} {h} {g} = D→C , C→D
      where
        D→C : (f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯) → (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g)
        D→C eq = f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫
              ≡⟨ sym (adjNatInD _ _) ⟩
                ((f ⋆⟨ D ⟩ k) ♭)
              ≡⟨ cong _♭ eq ⟩
                (F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯) ♭
              ≡⟨ sym (cong _♭ (adjNatInC _ _)) ⟩
                (h ⋆⟨ C ⟩ g) ♯ ♭
              ≡⟨ adjIso .rightInv _ ⟩
                h ⋆⟨ C ⟩ g
              ∎
        C→D : (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g) → (f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯)
        C→D eq = f ⋆⟨ D ⟩ k
              ≡⟨ sym (adjIso .leftInv _) ⟩
                (f ⋆⟨ D ⟩ k) ♭ ♯
              ≡⟨ cong _♯ (adjNatInD _ _) ⟩
                (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫) ♯
              ≡⟨ cong _♯ eq ⟩
                (h ⋆⟨ C ⟩ g) ♯
              ≡⟨ adjNatInC _ _ ⟩
                F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯
              ∎

    open NatTrans

    -- note : had to make this record syntax because termination checker was complaining
    -- due to referencing η and ε from the definitions of Δs
    adj'→adj : ⦃ isCatC : isCategory C ⦄ ⦃ isCatD : isCategory D ⦄ → F ⊣ G
    adj'→adj = record
      { η = η'
      ; ε = ε'
      ; Δ₁ = Δ₁'
      ; Δ₂ = Δ₂' }

      where
        -- ETA

        -- trivial commutative diagram between identities in D
        commInD : ∀ {x y} (f : C [ x , y ]) → (D .id _) ⋆⟨ D ⟩ F ⟪ f ⟫ ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ (D .id _)
        commInD f = (D .⋆IdL _) ∙ sym (D .⋆IdR _)

        sharpen1 : ∀ {x y} (f : C [ x , y ]) → F ⟪ f ⟫ ⋆⟨ D ⟩ (D .id _) ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ (D .id _) ♭ ♯
        sharpen1 f = cong (λ v → F ⟪ f ⟫ ⋆⟨ D ⟩ v) (sym (adjIso .leftInv _))

        η' : 𝟙⟨ C ⟩ ⇒ G ∘F F
        η' .N-ob x = (D .id _) ♭
        η' .N-hom f = sym (fst (adjNat') (commInD f ∙ sharpen1 f))

        -- EPSILON

        -- trivial commutative diagram between identities in C
        commInC : ∀ {x y} (g : D [ x , y ]) → (C .id _) ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ G ⟪ g ⟫ ⋆⟨ C ⟩ (C .id _)
        commInC g = (C .⋆IdL _) ∙ sym (C .⋆IdR _)

        sharpen2 : ∀ {x y} (g : D [ x , y ]) → (C .id _ ♯ ♭) ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ (C .id _) ⋆⟨ C ⟩ G ⟪ g ⟫
        sharpen2 g = cong (λ v → v ⋆⟨ C ⟩ G ⟪ g ⟫) (adjIso .rightInv _)

        ε' : F ∘F G ⇒ 𝟙⟨ D ⟩
        ε' .N-ob x = (C .id _) ♯
        ε' .N-hom g = sym (snd adjNat' (sharpen2 g ∙ commInC g))

        -- DELTA 1

        expL : ∀ (c)
            → (seqTransP F-assoc (F ∘ʳ η') (ε' ∘ˡ F) .N-ob c)
              ≡ F ⟪ η' ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε' ⟦ F ⟅ c ⟆ ⟧
        expL c = seqTransP F-assoc (F ∘ʳ η') (ε' ∘ˡ F) .N-ob c
              ≡⟨ refl ⟩
                seqP {C = D} {p = refl} (F ⟪ η' ⟦ c ⟧ ⟫) (ε' ⟦ F ⟅ c ⟆ ⟧)
              ≡⟨ seqP≡seq {C = D} _ _ ⟩
                F ⟪ η' ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε' ⟦ F ⟅ c ⟆ ⟧
              ∎

        body : ∀ (c)
            → (idTrans F) ⟦ c ⟧ ≡ (seqTransP F-assoc (F ∘ʳ η') (ε' ∘ˡ F) .N-ob c)
        body c = (idTrans F) ⟦ c ⟧
              ≡⟨ refl ⟩
                D .id _
              ≡⟨ sym (D .⋆IdL _) ⟩
                D .id _ ⋆⟨ D ⟩ D .id _
              ≡⟨ snd adjNat' (cong (λ v → (η' ⟦ c ⟧) ⋆⟨ C ⟩ v) (G .F-id)) ⟩
                F ⟪ η' ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε' ⟦ F ⟅ c ⟆ ⟧
              ≡⟨ sym (expL c) ⟩
                seqTransP F-assoc (F ∘ʳ η') (ε' ∘ˡ F) .N-ob c
              ∎

        Δ₁' : PathP (λ i → NatTrans (F-lUnit {F = F} i) (F-rUnit {F = F} i))
                    (seqTransP F-assoc (F ∘ʳ η') (ε' ∘ˡ F))
                    (1[ F ])
        Δ₁' = makeNatTransPathP F-lUnit F-rUnit (sym (funExt body))

        -- DELTA 2

        body2 : ∀ (d)
            →  seqP {C = C} {p = refl} ((η' ∘ˡ G) ⟦ d ⟧) ((G ∘ʳ ε') ⟦ d ⟧) ≡ C .id (G .F-ob d)
        body2 d = seqP {C = C} {p = refl} ((η' ∘ˡ G) ⟦ d ⟧) ((G ∘ʳ ε') ⟦ d ⟧)
                ≡⟨ seqP≡seq {C = C} _ _ ⟩
                  ((η' ∘ˡ G) ⟦ d ⟧) ⋆⟨ C ⟩ ((G ∘ʳ ε') ⟦ d ⟧)
                ≡⟨ refl ⟩
                  (η' ⟦ G ⟅ d ⟆ ⟧) ⋆⟨ C ⟩ (G ⟪ ε' ⟦ d ⟧ ⟫)
                ≡⟨ fst adjNat' (cong (λ v → v ⋆⟨ D ⟩ (ε' ⟦ d ⟧)) (sym (F .F-id))) ⟩
                  C .id _ ⋆⟨ C ⟩ C .id _
                ≡⟨ C .⋆IdL _ ⟩
                  C .id (G .F-ob d)
                ∎

        Δ₂' : PathP (λ i → NatTrans (F-rUnit {F = G} i) (F-lUnit {F = G} i))
              (seqTransP (sym F-assoc) (η' ∘ˡ G) (G ∘ʳ ε'))
              (1[ G ])
        Δ₂' = makeNatTransPathP F-rUnit F-lUnit (funExt body2)

  module _ (adj : F ⊣ G) where
    open _⊣_ adj
    open _⊣²_
    open NatTrans

    -- helper functions for working with this Adjoint definition

    δ₁ : ∀ {c} → (F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧) ≡ D .id _
    δ₁ {c} = (F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧)
          ≡⟨ sym (seqP≡seq {C = D} _ _) ⟩
            seqP {C = D} {p = refl} (F ⟪ η ⟦ c ⟧ ⟫) (ε ⟦ F ⟅ c ⟆ ⟧)
          ≡⟨ (λ j → (Δ₁ j) .N-ob c) ⟩
            D .id _
          ∎

    δ₂ : ∀ {d} → (η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫) ≡ C .id _
    δ₂ {d} = (η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫)
        ≡⟨ sym (seqP≡seq {C = C} _ _) ⟩
          seqP {C = C} {p = refl} (η ⟦ G ⟅ d ⟆ ⟧) (G ⟪ ε ⟦ d ⟧ ⟫)
        ≡⟨ (λ j → (Δ₂ j) .N-ob d) ⟩
          C .id _
        ∎

    adj→adj' : F ⊣² G
    -- ∀ {c d} → Iso (D [ F ⟅ c ⟆ , d ]) (C [ c , G ⟅ d ⟆ ])
    -- takes f to Gf precomposed with the unit
    adj→adj' .adjIso {c = c} .fun f = η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ f ⟫
    -- takes g to Fg postcomposed with the counit
    adj→adj' .adjIso {d = d} .inv g = F ⟪ g ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧
    -- invertibility follows from the triangle identities
    adj→adj' .adjIso {c = c} {d} .rightInv g
      = η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧ ⟫ -- step0 ∙ step1 ∙ step2 ∙ (C .⋆IdR _)
      ≡⟨ cong (λ v → η ⟦ c ⟧ ⋆⟨ C ⟩ v) (G .F-seq _ _) ⟩
        η ⟦ c ⟧ ⋆⟨ C ⟩ (G ⟪ F ⟪ g ⟫ ⟫ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫)
      ≡⟨ sym (C .⋆Assoc _ _ _) ⟩
        η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⟫ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫
      -- apply naturality
      ≡⟨ rPrecatWhisker {C = C} _ _ _ natu ⟩
        (g ⋆⟨ C ⟩ η ⟦ G ⟅ d ⟆ ⟧) ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫
      ≡⟨ C .⋆Assoc _ _ _ ⟩
        g ⋆⟨ C ⟩ (η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫)
      ≡⟨ lPrecatWhisker {C = C} _ _ _ δ₂ ⟩
        g ⋆⟨ C ⟩ C .id _
      ≡⟨ C .⋆IdR _ ⟩
        g
      ∎
      where
        natu : η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⟫ ≡ g ⋆⟨ C ⟩ η ⟦ G ⟅ d ⟆ ⟧
        natu = sym (η .N-hom _)
    adj→adj' .adjIso {c = c} {d} .leftInv f
      = F ⟪ η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧
      ≡⟨ cong (λ v → v ⋆⟨ D ⟩ ε ⟦ d ⟧) (F .F-seq _ _) ⟩
        F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ F ⟪ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧
      ≡⟨ D .⋆Assoc _ _ _ ⟩
        F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ (F ⟪ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧)
      -- apply naturality
      ≡⟨ lPrecatWhisker {C = D} _ _ _ natu ⟩
        F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ (ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f)
      ≡⟨ sym (D .⋆Assoc _ _ _) ⟩
        F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f
      -- apply triangle identity
      ≡⟨ rPrecatWhisker {C = D} _ _ _ δ₁ ⟩
        (D .id _) ⋆⟨ D ⟩ f
      ≡⟨ D .⋆IdL _ ⟩
        f
      ∎
      where
        natu : F ⟪ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧ ≡ ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f
        natu = ε .N-hom _
    -- follows directly from functoriality
    adj→adj' .adjNatInD {c = c} f k = cong (λ v → η ⟦ c ⟧ ⋆⟨ C ⟩ v) (G .F-seq _ _) ∙ (sym (C .⋆Assoc _ _ _))
    adj→adj' .adjNatInC {d = d} g h = cong (λ v → v ⋆⟨ D ⟩ ε ⟦ d ⟧) (F .F-seq _ _) ∙ D .⋆Assoc _ _ _

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module my-integer where

open import bool
open import bool-thms2
open import eq
open import nat
open import nat-thms
open import product
--open import product-thms
open import sum
-- open import unit

data ⊤ : Set where
  triv : ⊤

ℤ-pos-t : ℕ → Set
ℤ-pos-t 0 = ⊤
ℤ-pos-t (suc _) = 𝔹

data ℤ : Set where
  mkℤ : (n : ℕ) → ℤ-pos-t n → ℤ

0ℤ : ℤ
0ℤ = mkℤ 0 triv

1ℤ : ℤ
1ℤ = mkℤ 1 tt

-1ℤ : ℤ
-1ℤ = mkℤ 1 ff

abs-val : ℤ → ℕ
abs-val (mkℤ n _) = n

is-evenℤ : ℤ → 𝔹
is-evenℤ (mkℤ n _) = is-even n

is-oddℤ : ℤ → 𝔹
is-oddℤ (mkℤ n _) = is-odd n

{- subtract the second natural number from the first, returning an integer.
   This is mostly a helper for _+ℤ_ -}
diffℤ : ℕ → ℕ → ℤ
diffℤ n m with ℕ-trichotomy n m
diffℤ n m | inj₁ p with <∸suc{m}{n} p               -- n < m
diffℤ n m | inj₁ p | x , _ = mkℤ (suc x) ff
diffℤ n m | inj₂ (inj₁ p) = mkℤ 0 triv              -- n = m
diffℤ n m | inj₂ (inj₂ p) with <∸suc{n}{m} p
diffℤ n m | inj₂ (inj₂ p) | x , _ = mkℤ (suc x) tt  -- m < n

_+ℤ_ : ℤ → ℤ → ℤ
(mkℤ 0 _) +ℤ x = x
x +ℤ (mkℤ 0 _) = x
(mkℤ (suc n) p1) +ℤ (mkℤ (suc m) p2) with p1 xor p2
(mkℤ (suc n) p1) +ℤ (mkℤ (suc m) p2) | ff = mkℤ (suc n + suc m) p1
(mkℤ (suc n) p1) +ℤ (mkℤ (suc m) p2) | tt = if p1 imp p2 then diffℤ m n else diffℤ n m

max_stars_repo_name: logicshan/IAL

max_issues_repo_name: logicshan/IAL

max_forks_repo_name: logicshan/IAL