text:
{-

This module converts between the path types and the inductively
defined equality types.

-}
{-# OPTIONS --safe #-}

module Cubical.Data.Equality where

open import Cubical.Foundations.Prelude public
  hiding ( _≡_ ; _≡⟨_⟩_ ; _∎ ; isPropIsContr)
  renaming ( refl      to reflPath
           ; transport to transportPath
           ; J         to JPath
           ; JRefl     to JPathRefl
           ; sym       to symPath
           ; _∙_       to compPath
           ; cong      to congPath
           ; subst     to substPath
           ; funExt    to funExtPath
           ; isContr   to isContrPath
           ; isProp    to isPropPath )
open import Cubical.Foundations.Equiv
  renaming ( fiber     to fiberPath
           ; isEquiv   to isEquivPath
           ; _≃_       to EquivPath
           ; equivFun  to equivFunPath
           ; isPropIsEquiv to isPropIsEquivPath )
  hiding   ( equivCtr
           ; equivIsEquiv )
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence hiding (univalence)
open import Cubical.HITs.PropositionalTruncation public
  renaming (rec to recPropTruncPath
           ; elim to elimPropTruncPath )
open import Cubical.HITs.S1 as S1
  renaming (loop to loopPath)
  hiding (helix ; winding ; ΩS¹ ; encode ; intLoop ; decode ; decodeEncode)
open import Cubical.Data.Nat
open import Cubical.Data.Int

-- Import the builtin equality type defined as an inductive family
open import Agda.Builtin.Equality public

private
 variable
  ℓ ℓ' : Level
  A B : Type ℓ
  x y z : A

infix  3 _∎
infixr 2 _≡⟨_⟩_

ap : (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
ap f refl = refl

_∙_ : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
refl ∙ q = q

_≡⟨_⟩_ : (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
_ ≡⟨ p ⟩ q = p ∙ q

_∎ : (x : A) → x ≡ x
_ ∎ = refl

transport : ∀ (C : A → Type ℓ') {x y : A} → x ≡ y → C x → C y
transport C refl b = b

sym : {x y : A} → x ≡ y → y ≡ x
sym refl = refl

apd : {C : A → Type ℓ} (f : (x : A) → C x) {x y : A} (p : x ≡ y) → transport C p (f x) ≡ f y
apd f refl = refl

congPathd : {C : A → Type ℓ} (f : (x : A) → C x) {x y : A} (p : Path A x y) → Path (C y) (substPath C p (f x)) (f y)
congPathd f p = fromPathP (congPath f p)

-- Equality between Path and equality
eqToPath : {x y : A} → x ≡ y → Path A x y
eqToPath refl = reflPath

pathToEq : {x y : A} → Path A x y → x ≡ y
pathToEq {x = x} = JPath (λ y _ → x ≡ y) refl

eqToPath-pathToEq : {x y : A} → (p : Path A x y) → Path _ (eqToPath (pathToEq p)) p
eqToPath-pathToEq p =
  JPath (λ _ h → Path _ (eqToPath (pathToEq h)) h)
        (congPath eqToPath (transportRefl refl)) p

pathToEq-eqToPath : {x y : A} → (p : x ≡ y) → Path _ (pathToEq (eqToPath p)) p
pathToEq-eqToPath refl = transportRefl refl

PathIsoEq : {x y : A} → Iso (Path A x y) (x ≡ y)
PathIsoEq = iso pathToEq eqToPath pathToEq-eqToPath eqToPath-pathToEq

PathPathEq : {x y : A} → Path _ (Path A x y) (x ≡ y)
PathPathEq = isoToPath PathIsoEq

Path≡Eq : {x y : A} → (Path A x y) ≡ (x ≡ y)
Path≡Eq = pathToEq PathPathEq

-- We get funext by going back and forth between Path and Eq
funExt : {B : A → Type ℓ} {f g : (x : A) → B x} → ((x : A) → f x ≡ g x) → f ≡ g
funExt p = pathToEq (λ i x → eqToPath (p x) i)

-- Some lemmas relating the definitions for Path and ≡
substPath≡transport' : (C : A → Type ℓ) {x y : A} (b : C x) (p : x ≡ y) → substPath C (eqToPath p) b ≡ transport C p b
substPath≡transport' C b refl = pathToEq (transportRefl b)

substPath≡transport : (C : A → Type ℓ) {x y : A} (b : C x) (p : Path _ x y) → substPath C p b ≡ transport C (pathToEq p) b
substPath≡transport C b p = ap (λ x → substPath C x b) (pathToEq (symPath (eqToPath-pathToEq p)))
                          ∙ substPath≡transport' C b (pathToEq p)

congPath≡ap : {x y : A} → (f : A → B) (p : x ≡ y) → congPath f (eqToPath p) ≡ eqToPath (ap f p)
congPath≡ap f refl = refl

ap≡congPath : {x y : A} → (f : A → B) (p : Path A x y) → ap f (pathToEq p) ≡ pathToEq (congPath f p)
ap≡congPath {x = x} f p = JPath (λ _ q → ap f (pathToEq q) ≡ pathToEq (congPath f q)) rem p
  where
  rem : ap f (transp (λ i → x ≡ x) i0 refl) ≡ transp (λ i → f x ≡ f x) i0 refl
  rem = pathToEq (compPath (λ i → ap f (transportRefl refl i)) (symPath (transportRefl refl)))

-- Equivalences expressed using ≡ everywhere
fiber : ∀ {A : Type ℓ} {B : Type ℓ'} (f : A → B) (y : B) → Type (ℓ-max ℓ ℓ')
fiber {A = A} f y = Σ[ x ∈ A ] f x ≡ y

isContr : Type ℓ → Type ℓ
isContr A = Σ[ x ∈ A ] (∀ y → x ≡ y)

isProp : Type ℓ → Type ℓ
isProp A = (x y : A) → x ≡ y

record isEquiv {A : Type ℓ} {B : Type ℓ'} (f : A → B) : Type (ℓ-max ℓ ℓ') where
  field
    equiv-proof : (y : B) → isContr (fiber f y)

open isEquiv public

infix 4 _≃_

_≃_ : ∀ (A : Type ℓ) (B : Type ℓ') → Type (ℓ-max ℓ ℓ')
A ≃ B = Σ[ f ∈ (A → B) ] (isEquiv f)

equivFun : A ≃ B → A → B
equivFun e = e .fst

equivIsEquiv : (e : A ≃ B) → isEquiv (equivFun e)
equivIsEquiv e = e .snd

equivCtr : (e : A ≃ B) (y : B) → fiber (equivFun e) y
equivCtr e y = e .snd .equiv-proof y .fst

-- Functions for going between the various definitions. This could
-- also be achieved by making lines in the universe and transporting
-- back and forth along them.

fiberPathToFiber : {f : A → B} {y : B} → fiberPath f y → fiber f y
fiberPathToFiber (x , p) = (x , pathToEq p)

fiberToFiberPath : {f : A → B} {y : B} → fiber f y → fiberPath f y
fiberToFiberPath (x , p) = (x , eqToPath p)

fiberToFiber : {f : A → B} {y : B} (p : fiber f y) → Path _ (fiberPathToFiber (fiberToFiberPath p)) p
fiberToFiber (x , p) i = x , pathToEq-eqToPath p i

fiberPathToFiberPath : {f : A → B} {y : B} (p : fiberPath f y) → Path _ (fiberToFiberPath (fiberPathToFiber p)) p
fiberPathToFiberPath (x , p) i = x , eqToPath-pathToEq p i

isContrPathToIsContr : isContrPath A → isContr A
isContrPathToIsContr (ctr , p) = (ctr , λ y → pathToEq (p y))

isContrToIsContrPath : isContr A → isContrPath A
isContrToIsContrPath (ctr , p) = (ctr , λ y → eqToPath (p y))

isPropPathToIsProp : isPropPath A → isProp A
isPropPathToIsProp H x y = pathToEq (H x y)

isPropToIsPropPath : isProp A → isPropPath A
isPropToIsPropPath H x y = eqToPath (H x y)

-- Specialized helper lemmas for going back and forth between
-- isContrPath and isContr:

helper1 : {A B : Type ℓ} (f : A → B) (g : B → A) (h : ∀ y → Path _ (f (g y)) y)
        → isContrPath A → isContr B
helper1 f g h (x , p) =
  (f x , λ y → pathToEq (λ i → hcomp (λ j → λ { (i = i0) → f x
                                              ; (i = i1) → h y j })
                                     (f (p (g y) i))))

helper2 : {A B : Type ℓ} (f : A → B) (g : B → A) (h : ∀ y → Path _ (g (f y)) y)
        → isContr B → isContrPath A
helper2 {A = A} f g h (x , p) = (g x , λ y → eqToPath (ap g (p (f y)) ∙ pathToEq (h y)))

-- This proof is essentially the one for proving that isContr with
-- Path is a proposition, but as we are working with ≡ we have to
-- insert a lof of conversion functions.
-- TODO: prove this directly following the HoTT proof?
isPropIsContr : (p1 p2 : isContr A) → Path (isContr A) p1 p2
isPropIsContr (a0 , p0) (a1 , p1) j =
  ( eqToPath (p0 a1) j ,
    hcomp (λ i → λ { (j = i0) →  λ x → pathToEq-eqToPath (p0 x) i
                   ; (j = i1) →  λ x → pathToEq-eqToPath (p1 x) i })
          (λ x → pathToEq (λ i → hcomp (λ k → λ { (i = i0) → eqToPath (p0 a1) j
                                                ; (i = i1) → eqToPath (p0 x) (j ∨ k)
                                                ; (j = i0) → eqToPath (p0 x) (i ∧ k)
                                                ; (j = i1) → eqToPath (p1 x) i })
                                       (eqToPath (p0 (eqToPath (p1 x) i)) j))))

-- We now prove that isEquiv is a proposition
isPropIsEquiv : {A B : Type ℓ} {f : A → B} (h1 h2 : isEquiv f) → Path _ h1 h2
equiv-proof (isPropIsEquiv h1 h2 i) y = isPropIsContr (h1 .equiv-proof y) (h2 .equiv-proof y) i

equivToEquivPath : A ≃ B → EquivPath A B
equivToEquivPath (f , p) =
  (f , λ { .equiv-proof y → helper2 fiberPathToFiber fiberToFiberPath fiberPathToFiberPath (p .equiv-proof y) })

-- Go from a Path equivalence to an ≡ equivalence
equivPathToEquiv : EquivPath A B → A ≃ B
equivPathToEquiv (f , p) =
  (f , λ { .equiv-proof y → helper1 fiberPathToFiber fiberToFiberPath fiberToFiber (p .equiv-proof y) })

equivToEquiv : {A B : Type ℓ} (p : A ≃ B) → Path _ (equivPathToEquiv (equivToEquivPath p)) p
equivToEquiv (f , p) i =
  (f , isPropIsEquiv (λ { .equiv-proof y → helper1 fiberPathToFiber fiberToFiberPath fiberToFiber
                                             (helper2 fiberPathToFiber fiberToFiberPath fiberPathToFiberPath (p .equiv-proof y)) }) p i)

equivPathToEquivPath : {A B : Type ℓ} (p : EquivPath A B) → Path _ (equivToEquivPath (equivPathToEquiv p)) p
equivPathToEquivPath (f , p) i =
  ( f , isPropIsEquivPath f (equivToEquivPath (equivPathToEquiv (f , p)) .snd) p i )

equivPath≡Equiv : {A B : Type ℓ} → Path _ (EquivPath A B) (A ≃ B)
equivPath≡Equiv {ℓ} = isoToPath (iso (equivPathToEquiv {ℓ}) equivToEquivPath equivToEquiv equivPathToEquivPath)

path≡Eq : {A B : Type ℓ} → Path _ (Path _ A B) (A ≡ B)
path≡Eq = isoToPath (iso pathToEq eqToPath pathToEq-eqToPath eqToPath-pathToEq)

-- Univalence formulated using ≡ everywhere
univalenceEq : (A ≡ B) ≃ (A ≃ B)
univalenceEq {A = A} {B = B} = equivPathToEquiv rem
  where
  rem0 : Path _ (Lift (EquivPath A B)) (Lift (A ≃ B))
  rem0 = congPath Lift equivPath≡Equiv

  rem1 : Path _ (A ≡ B) (Lift (A ≃ B))
  rem1 i = hcomp (λ j → λ { (i = i0) → path≡Eq {A = A} {B = B} j
                          ; (i = i1) → rem0 j })
                 (univalencePath {A = A} {B = B} i)

  rem : EquivPath (A ≡ B) (A ≃ B)
  rem = compEquiv (eqweqmap rem1) (invEquiv LiftEquiv)

-- Propositional truncation using ≡ with paths under the hood

∥∥-isProp : ∀ (x y : ∥ A ∥₁) → x ≡ y
∥∥-isProp x y = pathToEq (squash₁ x y)

∥∥-recursion : ∀ {A : Type ℓ} {P : Type ℓ} → isProp P → (A → P) → ∥ A ∥₁ → P
∥∥-recursion Pprop = recPropTruncPath (isPropToIsPropPath Pprop)

∥∥-induction : ∀ {A : Type ℓ} {P : ∥ A ∥₁ → Type ℓ} → ((a : ∥ A ∥₁) → isProp (P a)) →
                ((x : A) → P ∣ x ∣₁) → (a : ∥ A ∥₁) → P a
∥∥-induction Pprop = elimPropTruncPath (λ a → isPropToIsPropPath (Pprop a))

-- The circle using ≡

loop : base ≡ base
loop = pathToEq loopPath

S¹-rec : {A : Type ℓ} (b : A) (l : b ≡ b) → S¹ → A
S¹-rec b l = S1.rec b (eqToPath l)

S¹-recβ : (b : A) (l : b ≡ b) → ap (S¹-rec b l) loop ≡ l
S¹-recβ b l =
  ap (S¹-rec b l) loop ≡⟨ ap≡congPath (S¹-rec b l) loopPath ⟩
  pathToEq (congPath (S¹-rec b l) loopPath) ≡⟨ refl ⟩
  pathToEq (eqToPath l) ≡⟨ pathToEq (pathToEq-eqToPath l) ⟩
  l ∎

-- TODO: see https://github.com/agda/cubical/pull/309#discussion_r424664465
-- S¹-elimβ : (C : S¹ → Type ℓ) (b : C base) (l : transport C loop b ≡ b) → apd (S¹-elim C b l) loop ≡ l
-- S¹-elimβ C b l =
  -- apd (S¹-elim C b l) (pathToEq loopPath) ≡⟨ {!!} ⟩
  -- {!!} ≡⟨ {!!} ⟩
  -- l ∎

-- We now compute some winding numbers to check that everything computes as expected

Cover : S¹ → Type₀
Cover = S¹-rec ℤ (pathToEq sucPathℤ)

ΩS¹ : Type₀
ΩS¹ = base ≡ base

encode : {x : S¹} → base ≡ x → Cover x
encode p = transport Cover p (pos zero)

winding : ΩS¹ → ℤ
winding = encode {base}

loop^ : ℤ → ΩS¹
loop^ (pos zero)       = refl
loop^ (pos (suc n))    = loop^ (pos n) ∙ loop
loop^ (negsuc zero)    = sym loop
loop^ (negsuc (suc n)) = loop^ (negsuc n) ∙ sym loop

private
  test-winding-refl : winding refl ≡ pos 0
  test-winding-refl = refl

  -- These should type check if things would compute:

  -- test-winding-loop : winding loop ≡ pos 1
  -- test-winding-loop = refl

  -- test-winding-pos5 : winding (loop^ (pos 2)) ≡ pos 2
  -- test-winding-pos5 = refl

  -- test-winding-neg5 : winding (loop^ (negsuc 2)) ≡ negsuc 2
  -- test-winding-neg5 = refl

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, issue #2482, reported by Guillaume Allais
-- Internal error because of wrong value for
-- number of parameters for data type.

-- {-# OPTIONS -v tc.data.sort:50 #-}
-- {-# OPTIONS -v tc.term.con:50 #-}

data D {b} (B : Set b) : Set b

-- This used to falsely compute the number of parameters to 1

data D B where
  c : B → D B

-- ... leading to a violated invariant when applying the constructor.

test : ∀ {B : Set} (b : B) → D B
test b = c b

-- n  = npars  = conPars (c)
-- n' = npars' = getNumberOfParameters (D)
-- should be the same

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module UniDB.Morph.Sub where

open import UniDB.Spec
open import UniDB.Morph.Depth

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

data Single (T : STX) : MOR where
  single : {γ : Dom} (t : T γ) → Single T (suc γ) γ

instance
  iLkSingle : {T : STX} {{vrT : Vr T}} → Lk T (Single T)
  lk {{iLkSingle {T}}} (single t) zero    = t
  lk {{iLkSingle {T}}} (single t) (suc i) = vr {T} i

  iBetaSingle : {T : STX} → Beta T (Single T)
  beta {{iBetaSingle}} = single

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

data Sub (T : STX) : MOR where
  sub : {γ₁ γ₂ : Dom} (ξ : Depth (Single T) γ₁ γ₂) → Sub T γ₁ γ₂

module _ {T : STX} where
  instance
    iLkSub : {{vrT : Vr T}} {{wkT : Wk T}} → Lk T (Sub T)
    lk {{iLkSub}} (sub ξ) = lk {T} {Depth (Single T)} ξ

    iUpSub : Up (Sub T)
    _↑₁ {{iUpSub}} (sub ζ)    = sub (ζ ↑₁)
    _↑_ {{iUpSub}} ξ 0        = ξ
    _↑_ {{iUpSub}} ξ (suc δ⁺) = ξ ↑ δ⁺ ↑₁
    ↑-zero {{iUpSub}} ξ       = refl
    ↑-suc {{iUpSub}}  ξ δ     = refl

    iBetaSub : Beta T (Sub T)
    beta {{iBetaSub}} t = sub (beta {T} {Depth (Single T)} t)

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

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
-- Andreas, 2022-06-14, issue #4725 reported by nad

-- The termination checker needs to recognize
-- dotted variable and record patterns as patterns
-- for this example to pass.
-- These should be harmless even with --cubical
-- (dotted constructor patterns are not, see #4606).
-- Keep fingers crossed.

{-# OPTIONS --cubical #-}

open import Agda.Builtin.Sigma

mutual

  data D : Set where
    d : S → D

  S : Set
  S = Σ D λ x → R x

  fst′ : S → D
  fst′ s = fst s

  data R : D → Set where
    r : ∀ x → R (fst′ x) → R (d x)

module _
  (P : D → Set)
  (Q : ∀ x → P x → R x → Set)
  (p : ∀ s (p : P (fst s)) → Q (fst s) p (snd s) → P (d s))
  (q : ∀ s rs (ps : P (fst s)) (qs : Q (fst s) ps (snd s)) →
       Q (fst s) ps rs → Q (d s) (p s ps qs) (r s rs))
  where

  mutual

    f : (x : D) → P x
    f (d (x , r₁)) = p (x , r₁) (f x) (g x r₁)

    g : (x : D) (x⊑y : R x) → Q x (f x) x⊑y
    g (d (x , r₁)) (r .(x , r₁) r₂) =
      q (x , r₁) r₂ (f x) (g x r₁) (g (fst′ (x , r₁)) r₂)

-- Should termination check.


text:
module examplesPaperJFP.safeFibStackMachineObjectOriented where

open import Data.Nat
open import Data.List
open import Data.Vec
open import Data.Sum
open import Data.Fin renaming (_+_ to _+f_)
open import Data.Product
open import examplesPaperJFP.StatefulObject
open import examplesPaperJFP.StackBisim

open import examplesPaperJFP.triangleRightOperator

{- Object based version of safe stack
   it is essentially the last part of safeFibStackMachine.agda
   with the names simplified -}

{- the state is what we are computing right now:
   fib n  menas we need to compute fib n
   val k  means we have computed   the value k
-}

data FibState : Set where
  fib  :  ℕ  →  FibState
  val  :  ℕ  →  FibState

data FibStackEl : Set where
  _+•     :  ℕ  →  FibStackEl
  •+fib_  :  ℕ  →  FibStackEl

FibStack : ℕ → Set
FibStack = Objectˢ (StackInterfaceˢ FibStackEl)

FibStackmachine : Set
FibStackmachine = Σ[ n ∈ ℕ ] (FibState × FibStack n)

reduce : FibStackmachine →  FibStackmachine ⊎ ℕ
reduce  (n      ,  fib 0             ,  stack)  =  inj₁ (n  ,  val 1  ,  stack)
reduce  (n      ,  fib 1             ,  stack)  =  inj₁ (n  ,  val 1  ,  stack)
reduce  (n      ,  fib (suc (suc m)) ,  stack)  =
        objectMethod stack (push (•+fib m))   ▹   λ  {  (_ , stack₁) →
        inj₁ ( suc n , fib (suc m) , stack₁)         }
reduce  (0      ,  val k             ,  stack)  =   inj₂ k
reduce  (suc n  ,  val k             ,  stack)  =
        objectMethod stack pop                ▹   λ  {  (k′ +•    , stack₁) →
        inj₁ (n , val (k′ + k) , stack₁)
                                                     ;  (•+fib m  , stack₁) →
        objectMethod stack₁ (push (k +•))     ▹   λ  {  (_ , stack₂) →
        inj₁ (suc n , fib m , stack₂)                }}

iter : (m : ℕ) → FibStackmachine →  FibStackmachine ⊎ ℕ
iter  0        s  =  inj₁ s
iter  (suc n)  s  with  reduce s
... |  inj₁ s′    =  iter n s′
... |  inj₂ m     =  inj₂ m

computeFib : ℕ → ℕ →  FibStackmachine ⊎ ℕ
computeFib n m = iter n (0 , fib m , stack [])

fibO0 :  FibStackmachine ⊎ ℕ
fibO0 = computeFib 2 0

-- evaluates to inj₂ 1

fibO1 :  FibStackmachine ⊎ ℕ
fibO1 = computeFib 2 1
-- evaluates to inj₂ 1

fibO2 :  FibStackmachine ⊎ ℕ
fibO2 = computeFib 10 2
-- evaluates to inj₂ 2

fibO3 :  FibStackmachine ⊎ ℕ
fibO3 = computeFib 14 3
-- evaluates to inj₂ 3

fibO4 :  FibStackmachine ⊎ ℕ
fibO4 = computeFib 30 4
-- evaluates to inj₂ 5

fibO5 :  FibStackmachine ⊎ ℕ
fibO5 = computeFib 30 5
-- evaluates to inj₂ 8

{-# TERMINATING #-}
computeFibRec : FibStackmachine → ℕ
computeFibRec s with reduce s
... | inj₁ s′   = computeFibRec s′
... | inj₂ k    = k

fibUsingStack : ℕ → ℕ
fibUsingStack m = computeFibRec (0 , fib m , stack [])

test : List ℕ
test = fibUsingStack 0 ∷ fibUsingStack 1 ∷ fibUsingStack 2 ∷ fibUsingStack 3 ∷ fibUsingStack 4 ∷ fibUsingStack 5 ∷ fibUsingStack 6  ∷ []

testExpected : List ℕ
testExpected = 1 ∷ 1 ∷ 2 ∷ 3 ∷ 5 ∷ 8 ∷ 13 ∷ []

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
-- Andreas, 2021-09-06, issue #5545,
-- regression introduced by #5522 (fix for #5291).
--
-- Note: this test requires that there is no newline at the end of file.
-- So, it violates the whitespace requirement of fix-whitespace,
-- and needs to be an exception in the configuration of fix-whitespace.

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

-- No newline at end of file triggered "Unterminated {!" error.

_ : Set
_ = {! !}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
import      Data.Vec.Relation.Unary.All as Vec-All
import      Data.Fin                    as Fin

-- This module defines the EpochConfigs available in the system, along
-- with a function to add a new EpochConfig and some properties that
-- facilitate proofs across state transitions that add an EpochConfig.

module LibraBFT.Yasm.AvailableEpochs
   (NodeId      : Set)
   (ℓ-EC        : Level)
   (EpochConfig : Set ℓ-EC)
   (epochId     : EpochConfig → ℕ)
   (authorsN    : EpochConfig → ℕ)
 where
 open import LibraBFT.Yasm.Base ℓ-EC EpochConfig epochId authorsN

 fin-lower-toℕ : ∀{e}(i : Fin (suc e))(prf : e ≢ toℕ i) → toℕ (Fin.lower₁ i prf) ≡ toℕ i
 fin-lower-toℕ {zero} zero prf = ⊥-elim (prf refl)
 fin-lower-toℕ {suc e}  zero prf = refl
 fin-lower-toℕ {suc e} (suc i) prf = cong suc (fin-lower-toℕ i (prf ∘ cong suc))

 toℕ-correct : ∀{n}(i : Fin n) → toℕ i < n
 toℕ-correct zero = s≤s z≤n
 toℕ-correct (suc i) = s≤s (toℕ-correct i)

 toℕ-inject₁-≡ : ∀{n}(i : Fin n) → toℕ i ≡ toℕ (Fin.inject₁ i)
 toℕ-inject₁-≡ zero = refl
 toℕ-inject₁-≡ (suc i) = cong suc (toℕ-inject₁-≡ i)

 lower₁-inject₁-id : ∀{n}(i : Fin n)(prf : n ≢ toℕ (Fin.inject₁ i)) → Fin.lower₁ (Fin.inject₁ i) prf ≡ i
 lower₁-inject₁-id zero prf = refl
 lower₁-inject₁-id (suc i) prf = cong suc (lower₁-inject₁-id i (prf ∘ cong suc))

 fromℕ-≤-step-natural : ∀{n m}(prf : n < m) → fromℕ< (≤-step prf) ≡ Fin.inject₁ (fromℕ< prf)
 fromℕ-≤-step-natural (s≤s z≤n) = refl
 fromℕ-≤-step-natural (s≤s (s≤s prf)) = cong suc (fromℕ-≤-step-natural (s≤s prf))

 Vec-All-lookup∘tabulate : ∀{n}{A : Set}{v : Vec A n}{ℓ : Level}{P : A → Set ℓ}
                         → (f : (x : Fin n) → P (Vec-lookup v x))(i : Fin n)
                         → Vec-All.lookup {P = P} i (Vec-All.tabulate {xs = v} f) ≡ f i
 Vec-All-lookup∘tabulate {v = v₀ ∷ vs} f zero = refl
 Vec-All-lookup∘tabulate {v = v₀ ∷ vs} f (suc i) = Vec-All-lookup∘tabulate (f ∘ suc) i

 subst-elim : {A : Set}{ℓ : Level}(P : A → Set ℓ){a₀ a₁ : A}
            → (prf : a₀ ≡ a₁)(x : P a₁)
            → subst P prf (subst P (sym prf) x) ≡ x
 subst-elim _ refl x = refl

 -- Available epochs consist of a vector of EpochConfigs with
 -- the correct epoch ids.
 AvailableEpochs : ℕ → Set ℓ-EC
 AvailableEpochs = Vec-All (EpochConfigFor ∘ toℕ) ∘ Vec-allFin

 lookup : ∀{e} → AvailableEpochs e → (ix : Fin e) → EpochConfigFor (toℕ ix)
 lookup 𝓔s ix =  subst EpochConfigFor (cong toℕ (Vec-lookup∘tabulate id ix)) (Vec-All-lookup ix 𝓔s)

 lookup' : ∀{e} → AvailableEpochs e → Fin e → EpochConfig
 lookup' 𝓔s ix = EpochConfigFor.epochConfig (lookup 𝓔s ix)

 lookup'' : ∀{e m} → AvailableEpochs e → m < e → EpochConfig
 lookup'' 𝓔s ix = lookup' 𝓔s (fromℕ< ix)

 lookup-𝓔s-injective : ∀ {e m1 m2} → (𝓔s : AvailableEpochs e)
                     → (p1 : m1 < e) → (p2 : m2 < e) → m1 ≡ m2
                     → lookup'' 𝓔s p1 ≡ lookup'' 𝓔s p2
 lookup-𝓔s-injective {e} 𝓔s p1 p2 refl = cong (lookup'' 𝓔s) (<-irrelevant p1 p2)

 -- The /transpose/ of append is defined by the semantics of a lookup
 -- over an append; the /append/ function below is defined by tabulating this
 -- monster.
 appendᵀ : ∀{e} → EpochConfigFor e → AvailableEpochs e → (i : Fin (suc e)) → EpochConfigFor (toℕ i)
 appendᵀ {e} ecf al i with e ≟ℕ toℕ i
 ...| yes e≡i = subst EpochConfigFor e≡i ecf
 ...| no  prf = subst EpochConfigFor
                      (trans (cong toℕ (Vec-lookup∘tabulate id (Fin.lower₁ i prf)))
                             (fin-lower-toℕ i prf))
                      (Vec-All-lookup (Fin.lower₁ i prf) al)

 -- Append is defined by tabulating appendᵀ
 append : ∀{e} → EpochConfigFor e → AvailableEpochs e → AvailableEpochs (suc e)
 append {e} ecf al = Vec-All.tabulate
    (λ i → subst (EpochConfigFor) (sym (cong toℕ (Vec-lookup∘tabulate id i))) (appendᵀ ecf al i))

 lookup-append-lemma
   : ∀{e}(𝓔s : AvailableEpochs e)(𝓔 : EpochConfigFor e)(ix : Fin (suc e))
   → lookup (append 𝓔 𝓔s) ix ≡ appendᵀ 𝓔 𝓔s ix
 lookup-append-lemma al ecf ix
   rewrite Vec-All-lookup∘tabulate
          {v = zero ∷ Vec-tabulate suc}
          {P = EpochConfigFor ∘ toℕ}
          (λ i → subst EpochConfigFor (sym (cong toℕ (Vec-lookup∘tabulate id i))) (appendᵀ ecf al i)) ix
        = subst-elim EpochConfigFor (cong toℕ (Vec-lookup∘tabulate id ix)) (appendᵀ ecf al ix)

 -- Ok, let's bring in the big guns
 import Relation.Binary.HeterogeneousEquality as HE

 append-inject₁-lemma
   : ∀{e}(𝓔s : AvailableEpochs e)(𝓔 : EpochConfigFor e)(ix : Fin e)
   → appendᵀ 𝓔 𝓔s (Fin.inject₁ ix)
   ≅ lookup 𝓔s ix
 append-inject₁-lemma {e} 𝓔s 𝓔 ix
   with e ≟ℕ (toℕ (Fin.inject₁ ix))
 ...| yes abs = ⊥-elim (<⇒≢ (toℕ-correct ix) (trans (toℕ-inject₁-≡ ix) (sym abs)))
 ...| no  prf = HE.trans (HE.≡-subst-removable EpochConfigFor
                           (trans (cong toℕ (Vec-lookup∘tabulate id (Fin.lower₁ (Fin-inject₁ ix) prf)))
                                  (fin-lower-toℕ (Fin.inject₁ ix) prf))
                           (Vec-All-lookup (Fin.lower₁ (Fin.inject₁ ix) prf) 𝓔s))
               (HE.trans (≅-cong (λ P → Vec-All-lookup P 𝓔s) (HE.≡-to-≅ (lower₁-inject₁-id ix prf)))
                         (HE.sym (HE.≡-subst-removable EpochConfigFor
                                   (cong toℕ (Vec-lookup∘tabulate id ix))
                                   (Vec-All-lookup ix 𝓔s))))

 lookup''-≤-step-lemma
   : ∀{e m}(𝓔s : AvailableEpochs e)(𝓔 : EpochConfigFor e)(prf : m < e)
   → lookup'' (append 𝓔 𝓔s) (≤-step prf) ≡ lookup'' 𝓔s prf
 lookup''-≤-step-lemma al ecf prf
   rewrite fromℕ-≤-step-natural prf
         | lookup-append-lemma al ecf (Fin.inject₁ (fromℕ< prf))
         = ECF-cong (append-inject₁-lemma al ecf (fromℕ< prf))
                    (sym (toℕ-inject₁-≡ (fromℕ< prf)))
   where
    ECF-cong : ∀{e e'}{ef : EpochConfigFor e}{ef' : EpochConfigFor e'}
             → ef ≅ ef' → e ≡ e'
             → EpochConfigFor.epochConfig ef ≡ EpochConfigFor.epochConfig ef'
    ECF-cong {e} {e'} {ef} {ef'} HE.refl refl = refl

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
module ZTF where

infixr 40 _◎_

open import Data.Integer
open import Data.Product
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------------
-- Zero totalized fields

data B : Set where
  ZERO   : B
  ONE    : B
  PLUS   : B → B → B
  TIMES  : B → B → B
  RECIP  : B → B
  NEG    : B → B

normalizeB : B → ℤ × ℤ
normalizeB ZERO = (+ 0 , + 1)
normalizeB ONE = (+ 1 , + 1)
normalizeB (PLUS b₁ b₂) with normalizeB b₁ | normalizeB b₂
... | (n1 , d1) | (n2 , d2) = (n1 * d2 + n2 * d1 , d1 * d2)
normalizeB (TIMES b₁ b₂) with normalizeB b₁ | normalizeB b₂
... | (n1 , d1) | (n2 , d2) = (n1 * n2 , d1 * d2)
normalizeB (RECIP b) with normalizeB b
... | (n , d) = (d , n)
normalizeB (NEG b) with normalizeB b
... | (n , d) = (- n , d)

b1 : ℤ × ℤ
b1 = normalizeB (
       RECIP (PLUS
               (TIMES (PLUS ONE ONE) (PLUS ONE (PLUS ONE ONE)))
               (NEG (TIMES (PLUS ONE ONE) (PLUS ONE (PLUS ONE ONE))))))

helper : ℤ × ℤ → B
helper (+ 0 , _) = ZERO
helper (_ , + 0) = ZERO
helper _         = ONE

ztf : B → B
ztf b = helper (normalizeB b)

rlem : {b : B} → normalizeB b ≡ swap (normalizeB (RECIP b))
rlem = refl

{--
helperlem : {z₁ z₂ : ℤ} → helper (z₁ , z₂) ≡ helper (z₂ , z₁)
helperlem {+ 0} {_} = refl
helperlem {_} {+ 0} = refl
helperlem {_} {_} = refl
--}

data X : Set where
  P0 : X
  P1 : X
  P2  : X

helperX : X × X → B
helperX (P0 , P0) = ZERO
helperX (_  ,  _) = ZERO
--helperX (P0 , _) = ZERO
--helperX (_ , P0) = ZERO
--helperX _        = ONE

helperlemX : {a b : X} → helperX (a , b) ≡ helperX (b , a)
helperlemX {P0} {P0} = refl
helperlemX {P1} {P0} = refl
helperlemX {P2} {P0} = refl
helperlemX {_} {P1} = refl
helperlemX {_} {P2} = refl

blemX : {b : B} → b ≡ b
blemX = refl

{--
helperlemX : ∀ a b → helperX (a , b) ≡ helperX (b , a)
helperlemX {P0} {P0} = refl
helperlemX {P0} {P1} = refl
helperlemX {P0} {P2} = refl
helperlemX {P1} {P0} = refl
helperlemX {P1} {P1} = refl
helperlemX {P1} {P2} = refl
helperlemX {P2} {P0} = refl
helperlemX {P2} {P1} = refl
helperlemX {P2} {P2} = refl

rlem2 : (b : B) → ztf b ≡ ztf (RECIP b)
rlem2 b = refl

with normalizeB b | normalizeB (RECIP b)
... | (n , + 0) | .(+ 0 , n) = refl
... | (+ 0 , d) | .(d , + 0) = refl
... | (n  ,  d) | .(d , n)   = refl
--}

data _⟷_ : B → B → Set₁ where
  unite₊ : {b : B} → PLUS ZERO b ⟷ b
  uniti₊ : {b : B} → b ⟷ PLUS ZERO b
  swap₊ : {b₁ b₂ : B} → PLUS b₁ b₂ ⟷ PLUS b₂ b₁
  assocl₊ : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷ PLUS (PLUS b₁ b₂) b₃
  assocr₊ : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷ PLUS b₁ (PLUS b₂ b₃)
  unitez⋆  : { b : B } → TIMES (ztf b) b ⟷ b
  unitiz⋆  : { b : B } → b ⟷ TIMES (ztf b) b
-- subsumed by above
--  unite⋆  : { b : B } → TIMES ONE b ⟷ b
--  uniti⋆  : { b : B } → b ⟷ TIMES ONE b
--  distZ    : { b : B } → TIMES ZERO b ⟷ ZERO
--  factorZ  : { b : B } → ZERO ⟷ TIMES ZERO b
  swap⋆ : {b₁ b₂ : B} → TIMES b₁ b₂ ⟷ TIMES b₂ b₁
  assocl⋆ : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷ TIMES (TIMES b₁ b₂) b₃
  assocr⋆ : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷ TIMES b₁ (TIMES b₂ b₃)
  dist    : { b₁ b₂ b₃ : B } →
            TIMES (PLUS b₁ b₂) b₃ ⟷ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
  factor  : { b₁ b₂ b₃ : B } →
            PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ⟷ TIMES (PLUS b₁ b₂) b₃
  id⟷ : {b : B } → b ⟷ b
  op    : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
  _◎_    : { b₁ b₂ b₃ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₃) → (b₁ ⟷ b₃)
  _⊕_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (PLUS b₁ b₂ ⟷ PLUS b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (TIMES b₁ b₂ ⟷ TIMES b₃ b₄)
  η⋆ : {b : B} → ztf b ⟷ TIMES (RECIP b) b
  ε⋆ : {b : B} → TIMES (RECIP b) b ⟷ ztf b
  η₊ : {b : B} → ZERO ⟷ PLUS (NEG b) b
  ε₊ : {b : B} → PLUS (NEG b) b ⟷ ZERO

------------------------------------------------------------------------------
-- Examples

_⇒⋆_ : B → B → B
b₁ ⇒⋆ b₂ = TIMES (RECIP b₁) b₂

_⇒₊_ : B → B → B
b₁ ⇒₊ b₂ = PLUS (NEG b₁) b₂

name : {b₁ b₂ : B} → (b₁ ⟷ b₂) → (ztf b₁ ⟷ (b₁ ⇒⋆ b₂))
name c = η⋆ ◎ (id⟷ ⊗ c)

{--

doubleDiv : { b : B } → b ⟷ RECIP (RECIP b)
doubleDiv = unitiz⋆ ◎
            (η⋆ ⊗ id⟷) ◎
            assocr⋆ ◎
            (id⟷ ⊗ ε⋆) ◎
            swap⋆ ◎
            unitez⋆

--}

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- The unit type (in Set₁)
------------------------------------------------------------------------

module Data.Unit1 where

record ⊤₁ : Set₁ where

max_issues_repo_name: larrytheliquid/Lemmachine


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

open import lib.Basics
open import lib.types.Pi
open import lib.types.Paths
open import lib.types.Sigma

module lib.types.Flattening {i j k}
  (A : Type i) (B : Type j) (f g : B → A)
  (C : A → Type k) (D : (b : B) → C (f b) ≃ C (g b)) where

{- The base HIT -}

import lib.types.Generic1HIT as Generic1HIT

module W = Generic1HIT A B f g
open W public using (cc; pp)
              renaming (T to W)

module P = W.RecType C D
open P public -- using (↓-pp-in; ↓-pp-out; ↓-pp-β)
              renaming (f to P)

{- The flattened HIT -}

At : Type _
At = Σ A C

Bt : Type _
Bt = Σ B (C ∘ f)

ft : Bt → At
ft (b , d) = (f b , d)

gt : Bt → At
gt (b , d) = (g b , –> (D b) d)

module Wt = Generic1HIT At Bt ft gt
open Wt public using ()
               renaming (T to Wt)

cct = curry Wt.cc
ppt = curry Wt.pp

private
  {- Flattening -}

  module _ where
    paths-flatten :
      (b : B) → (cct (f b) == cct (g b) [ (λ w → (P w → Wt)) ↓ pp b ])
    paths-flatten b =
      ↓-app→cst-in (λ q → ppt b _ ∙' ap (cct (g b)) (↓-pp-out q))

  module FlattenCurried = W.Elim cct paths-flatten

  flatten-curried : (w : W) → (P w → Wt)
  flatten-curried = W.Elim.f cct paths-flatten

  flatten : Σ W P → Wt
  flatten (w , x) = flatten-curried w x

  {- Unflattening -}

  unflatten-cc : (ac : At) → Σ W P
  unflatten-cc (a , c) = (cc a , c)

  unflatten-pp : (bd : Bt) → unflatten-cc (ft bd) == unflatten-cc (gt bd)
  unflatten-pp (b , d) = pair= (pp b) (↓-pp-in idp)

  module Unflatten = Wt.Rec unflatten-cc unflatten-pp

  unflatten : Wt → Σ W P
  unflatten = Unflatten.f

  {- First composition -}

  flatten-unflatten : (w : Wt) → flatten (unflatten w) == w
  flatten-unflatten = Wt.elim
    (λ _ → idp)
    (λ bd → let (b , d) = bd in
      ↓-∘=idf-in flatten unflatten
      (ap flatten (ap unflatten (ppt b d))
                 =⟨ Unflatten.pp-β bd |in-ctx ap flatten ⟩
       ap flatten (pair= (pp b) (↓-pp-in idp))
                 =⟨ split-ap2 flatten (pp b) (↓-pp-in idp) ⟩
       ↓-app→cst-out (apd flatten-curried (pp b)) (↓-pp-in idp)
                 =⟨ FlattenCurried.pp-β b
                    |in-ctx (λ u → ↓-app→cst-out u (↓-pp-in idp)) ⟩
       ↓-app→cst-out (paths-flatten b) (↓-pp-in idp)
                 =⟨ idp ⟩
       ↓-app→cst-out (↓-app→cst-in
         (λ q → ppt b _ ∙' ap (cct (g b)) (↓-pp-out q))) (↓-pp-in idp)
                 =⟨ ↓-app→cst-β (λ q → ppt b _ ∙' ap (cct (g b)) (↓-pp-out q))
                                (↓-pp-in idp) ⟩
       ppt b d ∙' ap (cct (g b)) (↓-pp-out (↓-pp-in idp))
                 =⟨ ↓-pp-β idp |in-ctx (λ u → ppt b d ∙' ap (cct (g b)) u) ⟩
       ppt b d ∎))

  {- Second composition -}

  unflatten-flatten-curried : (w : W) (x : P w)
    →  unflatten (flatten-curried w x) == (w , x)
  unflatten-flatten-curried = W.elim
    (λ a x → idp)
    (λ b → ↓-Π-in
    (λ q → ↓-∘=idf-in unflatten flatten
      (ap unflatten (ap flatten (pair= (pp b) q))
                 =⟨ split-ap2 flatten (pp b) q |in-ctx ap unflatten ⟩
       ap unflatten (↓-app→cst-out (apd flatten-curried (pp b)) q)
                 =⟨ FlattenCurried.pp-β b
                    |in-ctx (λ u → ap unflatten (↓-app→cst-out u q)) ⟩
       ap unflatten (↓-app→cst-out (paths-flatten b) q)
                 =⟨ idp ⟩
       ap unflatten (↓-app→cst-out (↓-app→cst-in (λ qq → ppt b _ ∙' ap (cct (g b)) (↓-pp-out qq))) q)
                 =⟨ ↓-app→cst-β (λ qq → ppt b _ ∙' ap (cct (g b)) (↓-pp-out qq)) q |in-ctx ap unflatten ⟩
       ap unflatten (ppt b _ ∙' ap (cct (g b)) (↓-pp-out q))
                 =⟨ ap-∙' unflatten (ppt b _) (ap (cct (g b)) (↓-pp-out q)) ⟩
       ap unflatten (ppt b _) ∙' ap unflatten (ap (cct (g b)) (↓-pp-out q))
                 =⟨ Unflatten.pp-β (b , _) |in-ctx (λ u → u ∙' ap unflatten (ap (cct (g b)) (↓-pp-out q))) ⟩
       pair= (pp b) (↓-pp-in idp) ∙' ap unflatten (ap (cct (g b)) (↓-pp-out q))
                 =⟨ ∘-ap unflatten (cct (g b)) (↓-pp-out q) |in-ctx (λ u → (pair= (pp b) (↓-pp-in idp) ∙' u)) ⟩
       pair= (pp b) (↓-pp-in idp) ∙' ap (unflatten ∘ cct (g b)) (↓-pp-out q)
                 =⟨ idp ⟩
       pair= (pp b) (↓-pp-in idp) ∙' ap (λ x → (cc (g b), x)) (↓-pp-out q)
                 =⟨ ap-cst,id P (↓-pp-out q) |in-ctx (λ u → pair= (pp b) (↓-pp-in idp) ∙' u) ⟩
       pair= (pp b) (↓-pp-in idp) ∙' pair= idp (↓-pp-out q)
                 =⟨ Σ-∙' (↓-pp-in idp) (↓-pp-out q) ⟩
       pair= (pp b) (↓-pp-in idp ∙'ᵈ ↓-pp-out q)
                 =⟨ to-transp-weird q (coe-pp-β _ _) |in-ctx pair= (pp b) ⟩
       pair= (pp b) q ∎)))

  unflatten-flatten : (wx : Σ W P) → unflatten (flatten wx) == wx
  unflatten-flatten (w , x) = unflatten-flatten-curried w x

{- The equivalence -}

abstract
  flattening-equiv : Σ W P ≃ Wt
  flattening-equiv = equiv flatten unflatten flatten-unflatten unflatten-flatten

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-

Definition of what it means to be a notion of relational structure

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.RelationalStructure where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Univalence
open import Cubical.Functions.FunExtEquiv
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation as Trunc
open import Cubical.HITs.SetQuotients
open import Cubical.Relation.Binary.Base
open import Cubical.Relation.ZigZag.Base

open BinaryRelation

private
  variable
    ℓ ℓ' ℓ'' ℓ''' : Level

-- A notion of structured relation for a structure S assigns a relation on S X and S Y to every relation on X
-- and Y. We require the output to be proposition-valued when the input is proposition-valued.
StrRel : (S : Type ℓ → Type ℓ') (ℓ'' : Level) → Type (ℓ-max (ℓ-suc (ℓ-max ℓ ℓ'')) ℓ')
StrRel {ℓ = ℓ} S ℓ'' = ∀ {A B} (R : Rel A B ℓ) → Rel (S A) (S B) ℓ''

-- Given a type A and relation R, a quotient structure is a structure on the set quotient A/R such that
-- the graph of [_] : A → A/R is a structured relation
InducedQuotientStr : (S : Type ℓ → Type ℓ') (ρ : StrRel S ℓ'')
  (A : TypeWithStr ℓ S) (R : Rel (typ A) (typ A) ℓ)
  → Type (ℓ-max ℓ' ℓ'')
InducedQuotientStr S ρ A R =
  Σ[ s ∈ S (typ A / R) ] ρ (graphRel [_]) (A .snd) s

-- A structured equivalence relation R on a structured type A should induce a structure on A/R
InducesQuotientStr : (S : Type ℓ → Type ℓ') (ρ : StrRel S ℓ'') → Type _
InducesQuotientStr {ℓ = ℓ} S ρ =
  (A : TypeWithStr ℓ S) (R : EquivPropRel (typ A) ℓ)
  → ρ (R .fst .fst) (A .snd) (A .snd)
  → ∃![ s ∈ S (typ A / R .fst .fst) ] ρ (graphRel [_]) (A .snd) s

-- The inverse of a structured relation should be structured
isSymmetricStrRel : {S : Type ℓ → Type ℓ'} (ρ : StrRel S ℓ'') → Type _
isSymmetricStrRel {ℓ = ℓ} {S = S} ρ =
  {X Y : Type ℓ} (R : PropRel X Y ℓ)
  {sx : S X} {sy : S Y}
  → ρ (R .fst) sx sy
  → ρ (invPropRel R .fst) sy sx

-- The composite of structured relations should be structured
isTransitiveStrRel : {S : Type ℓ → Type ℓ'} (ρ : StrRel S ℓ'') → Type _
isTransitiveStrRel {ℓ = ℓ} {S = S} ρ =
  {X Y Z : Type ℓ}
  (R₀ : PropRel X Y ℓ) (R₁ : PropRel Y Z ℓ)
  {sx : S X} {sy : S Y} {sz : S Z}
  → ρ (R₀ .fst) sx sy
  → ρ (R₁ .fst) sy sz
  → ρ (compPropRel R₀ R₁ .fst) sx sz

-- The type of structures on a prop-valued relation should be a prop
preservesPropsStrRel : {S : Type ℓ → Type ℓ'} (ρ : StrRel S ℓ'') → Type _
preservesPropsStrRel {ℓ = ℓ} {S = S} ρ =
  {X Y : Type ℓ} {R : Rel X Y ℓ}
  → (∀ x y → isProp (R x y))
  → (sx : S X) (sy : S Y)
  → isProp (ρ R sx sy)

record SuitableStrRel (S : Type ℓ → Type ℓ') (ρ : StrRel S ℓ'') : Type (ℓ-max (ℓ-max (ℓ-suc ℓ) ℓ') ℓ'')
  where
  field
    quo : InducesQuotientStr S ρ
    symmetric : isSymmetricStrRel ρ
    transitive : isTransitiveStrRel ρ
    prop : preservesPropsStrRel ρ

open SuitableStrRel

-- We can also ask for a notion of structured relations to agree with some notion of structured equivalences.
StrRelMatchesEquiv : {S : Type ℓ → Type ℓ'}
  → StrRel S ℓ'' → StrEquiv S ℓ''' → Type _
StrRelMatchesEquiv {S = S} ρ ι =
  (A B : TypeWithStr _ S) (e : typ A ≃ typ B) →
  ρ (graphRel (e .fst)) (A .snd) (B .snd) ≃ ι A B e

-- Given a suitable notion of structured relation, if we have a structured quasi equivalence relation R
-- between structured types A and B, we get induced structures on the quotients A/(R ∙ R⁻¹) and B/(R⁻¹ ∙ R),
-- and the induced equivalence e : A/(R ∙ R⁻¹) ≃ B/(R⁻¹ ∙ R) is structured with respect to those quotient
-- structures.

quotientPropRel : ∀ {ℓ} {A : Type ℓ} (R : Rel A A ℓ) → PropRel A (A / R) ℓ
quotientPropRel R .fst a t = [ a ] ≡ t
quotientPropRel R .snd _ _ = squash/ _ _

record QERDescends (S : Type ℓ → Type ℓ') (ρ : StrRel S ℓ'')
  (A B : TypeWithStr ℓ S) (R : QuasiEquivRel (typ A) (typ B) ℓ) : Type (ℓ-max ℓ' ℓ'')
  where
  private
    module E = QER→Equiv R

  field
    quoᴸ : InducedQuotientStr S ρ A E.Rᴸ
    quoᴿ : InducedQuotientStr S ρ B E.Rᴿ
    rel : ρ (graphRel (E.Thm .fst)) (quoᴸ .fst) (quoᴿ .fst)

open QERDescends
open isQuasiEquivRel

structuredQER→structuredEquiv : {S : Type ℓ → Type ℓ'} (ρ : StrRel S ℓ'')
  (θ : SuitableStrRel S ρ)
  (A B : TypeWithStr ℓ S) (R : QuasiEquivRel (typ A) (typ B) ℓ)
  → ρ (R .fst .fst) (A .snd) (B .snd)
  → QERDescends S ρ A B R
structuredQER→structuredEquiv ρ θ (X , s) (Y , t) R r .quoᴸ =
  θ .quo (X , s) (QER→EquivRel R)
    (subst (λ R' → ρ R' s s) correction
      (θ .transitive (R .fst) (invPropRel (R .fst)) r (θ .symmetric (R .fst) r)))
    .fst
  where
  correction : compPropRel (R .fst) (invPropRel (R .fst)) .fst ≡ QER→EquivRel R .fst .fst
  correction =
    funExt₂ λ x₀ x₁ →
      (hPropExt squash (R .fst .snd _ _)
        (Trunc.rec (R .fst .snd _ _) (λ {(y , r , r') → R .snd .zigzag r r' (R .snd .fwdRel _)}))
        (λ r → ∣ _ , r , R .snd .fwdRel _ ∣))

structuredQER→structuredEquiv ρ θ (X , s) (Y , t) R r .quoᴿ =
  θ .quo (Y , t) (QER→EquivRel (invQER R))
    (subst (λ R' → ρ R' t t) correction
      (θ .transitive (invPropRel (R .fst)) (R .fst) (θ .symmetric (R .fst) r) r))
    .fst
  where
  correction : compPropRel (invPropRel (R .fst)) (R .fst) .fst ≡ QER→EquivRel (invQER R) .fst .fst
  correction =
    funExt₂ λ y₀ y₁ →
      (hPropExt squash (R .fst .snd _ _)
        (Trunc.rec (R .fst .snd _ _) (λ {(x , r , r') → R .snd .zigzag (R .snd .bwdRel _) r' r}))
        (λ r → ∣ _ , r , R .snd .bwdRel _ ∣))

structuredQER→structuredEquiv ρ θ (X , s) (Y , t) R r .rel =
  subst (λ R' → ρ R' (quol .fst) (quor .fst)) correction
    (θ .transitive (compPropRel (invPropRel (quotientPropRel E.Rᴸ)) (R .fst)) (quotientPropRel E.Rᴿ)
      (θ .transitive (invPropRel (quotientPropRel E.Rᴸ)) (R .fst)
        (θ .symmetric (quotientPropRel E.Rᴸ) (quol .snd))
        r)
      (quor .snd))
  where
  module E = QER→Equiv R
  quol = structuredQER→structuredEquiv ρ θ (X , s) (Y , t) R r .quoᴸ
  quor = structuredQER→structuredEquiv ρ θ (X , s) (Y , t) R r .quoᴿ
  [R] = compPropRel (compPropRel (invPropRel (quotientPropRel E.Rᴸ)) (R .fst)) (quotientPropRel E.Rᴿ)

  correction : [R] .fst ≡ graphRel (E.Thm .fst)
  correction =
    funExt₂ λ qx qy →
      (hPropExt squash (squash/ _ _)
        (Trunc.rec (squash/ _ _)
          (λ {(y , qr , py) →
            Trunc.rec
              (squash/ _ _)
              (λ {(x , px , r) →
                cong (E.Thm .fst) (sym px)
                ∙ eq/ (R .snd .fwd x) y (R .snd .zigzag (R .snd .bwdRel y) r (R .snd .fwdRel x))
                ∙ py})
              qr}))
        (elimProp
          {B = λ qx →
            E.Thm .fst qx ≡ qy → [R] .fst qx qy}
          (λ _ → isPropΠ λ _ → squash)
          (λ x p → ∣ _ , ∣ _ , refl , R .snd .fwdRel x ∣ , p ∣)
          qx))

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Relation.Nullary where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

open import Cubical.Data.Empty

private
  variable
    ℓ  : Level
    A  : Type ℓ

-- Negation
infix 3 ¬_

¬_ : Type ℓ → Type ℓ
¬ A = A → ⊥

isProp¬ : (A : Type ℓ) → isProp (¬ A)
isProp¬ A p q i x = isProp⊥ (p x) (q x) i

-- Decidable types (inspired by standard library)
data Dec (P : Type ℓ) : Type ℓ where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P

Stable : Type ℓ → Type ℓ
Stable A = ¬ ¬ A → A

Discrete : Type ℓ → Type ℓ
Discrete A = (x y : A) → Dec (x ≡ y)

Stable¬ : Stable (¬ A)
Stable¬ ¬¬¬a a = ¬¬¬a ¬¬a
  where
  ¬¬a = λ ¬a → ¬a a

fromYes : A → Dec A → A
fromYes _ (yes a) = a
fromYes a (no _) = a

discreteDec : (Adis : Discrete A) → Discrete (Dec A)
discreteDec Adis (yes p) (yes p') = decideYes (Adis p p') -- TODO: monad would simply stuff
  where
    decideYes : Dec (p ≡ p') → Dec (yes p ≡ yes p')
    decideYes (yes eq) = yes (cong yes eq)
    decideYes (no ¬eq) = no λ eq → ¬eq (cong (fromYes p) eq)
discreteDec Adis (yes p) (no ¬p) = ⊥-elim (¬p p)
discreteDec Adis (no ¬p) (yes p) = ⊥-elim (¬p p)
discreteDec {A = A} Adis (no ¬p) (no ¬p') = yes (cong no (isProp¬ A ¬p ¬p'))

isPropDec : (Aprop : isProp A) → isProp (Dec A)
isPropDec Aprop (yes a) (yes a') = cong yes (Aprop a a')
isPropDec Aprop (yes a) (no ¬a) = ⊥-elim (¬a a)
isPropDec Aprop (no ¬a) (yes a) = ⊥-elim (¬a a)
isPropDec {A = A} Aprop (no ¬a) (no ¬a') = cong no (isProp¬ A ¬a ¬a')

mapDec : ∀ {B : Type ℓ} → (A → B) → (¬ A → ¬ B) → Dec A → Dec B
mapDec f _ (yes p) = yes (f p)
mapDec _ f (no ¬p) = no (f ¬p)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
------------------------------------------------------------------------
-- Non-dependent and dependent lenses
-- Nils Anders Danielsson
------------------------------------------------------------------------

{-# OPTIONS --cubical --guardedness #-}

module README where

-- Non-dependent lenses.

import Lens.Non-dependent
import Lens.Non-dependent.Traditional
import Lens.Non-dependent.Traditional.Combinators
import Lens.Non-dependent.Higher
import Lens.Non-dependent.Higher.Combinators
import Lens.Non-dependent.Higher.Capriotti.Variant
import Lens.Non-dependent.Higher.Capriotti
import Lens.Non-dependent.Higher.Coherently.Not-coinductive
import Lens.Non-dependent.Higher.Coherently.Coinductive
import Lens.Non-dependent.Higher.Coinductive
import Lens.Non-dependent.Higher.Coinductive.Small
import Lens.Non-dependent.Higher.Surjective-remainder
import Lens.Non-dependent.Equivalent-preimages
import Lens.Non-dependent.Bijection

-- Non-dependent lenses with erased proofs.

import Lens.Non-dependent.Traditional.Erased
import Lens.Non-dependent.Higher.Erased
import Lens.Non-dependent.Higher.Capriotti.Variant.Erased
import Lens.Non-dependent.Higher.Capriotti.Variant.Erased.Variant
import Lens.Non-dependent.Higher.Coinductive.Erased
import Lens.Non-dependent.Higher.Coinductive.Small.Erased
import Lens.Non-dependent.Higher.Coherently.Coinductive.Erased

-- Dependent lenses.

import Lens.Dependent

-- Comparisons of different kinds of lenses, focusing on the
-- definition of composable record getters and setters.

import README.Record-getters-and-setters

-- Some code suggesting that types used in "programs" might not
-- necessarily be sets. (If lenses are only used in programs, and
-- types used in programs are always sets, then higher lenses might be
-- pointless.)

import README.Not-a-set

-- Pointers to code corresponding to many definitions and results from
-- the paper "Higher Lenses" by Paolo Capriotti, Nils Anders
-- Danielsson and Andrea Vezzosi.

import README.Higher-Lenses

-- The lenses fst and snd.

import README.Fst-snd

-- Pointers to code corresponding to some definitions and results from
-- the paper "Compiling Programs with Erased Univalence" by Andreas
-- Abel, Nils Anders Danielsson and Andrea Vezzosi.

import README.Compiling-Programs-with-Erased-Univalence

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
------------------------------------------------------------------------
-- A library of parser combinators
------------------------------------------------------------------------

module RecursiveDescent.Coinductive.Lib where

open import Utilities
open import RecursiveDescent.Coinductive
import RecursiveDescent.Coinductive.Internal as Internal
open import RecursiveDescent.Index

open import Data.Bool hiding (_≟_)
open import Data.Nat  hiding (_≟_)
open import Data.Product.Record using (_,_)
open import Data.Product renaming (_,_ to pair)
open import Data.List hiding (any)
open import Data.Function
open import Data.Maybe
open import Data.Unit hiding (_≟_)
import Data.Char as C
open import Relation.Nullary
open import Relation.Binary

------------------------------------------------------------------------
-- Applicative functor parsers

-- We could get these for free with better library support.

infixl 50 _⊛_ _<⊛_ _⊛>_ _<$>_ _<$_

-- Note that all the resulting indices can be inferred.

_⊛_ : forall {tok i₁ i₂ r₁ r₂} ->
      Parser tok i₁ (r₁ -> r₂) -> Parser tok i₂ r₁ -> Parser tok _ r₂
p₁ ⊛ p₂ = p₁ >>= \f -> p₂ >>= \x -> return (f x)

_<$>_ : forall {tok r₁ r₂ i} ->
        (r₁ -> r₂) -> Parser tok i r₁ -> Parser tok _ r₂
f <$> x = return f ⊛ x

_<⊛_ : forall {tok i₁ i₂ r₁ r₂} ->
       Parser tok i₁ r₁ -> Parser tok i₂ r₂ -> Parser tok _ r₁
x <⊛ y = const <$> x ⊛ y

_⊛>_ : forall {tok i₁ i₂ r₁ r₂} ->
       Parser tok i₁ r₁ -> Parser tok i₂ r₂ -> Parser tok _ r₂
x ⊛> y = flip const <$> x ⊛ y

_<$_ : forall {tok r₁ r₂ i} ->
       r₁ -> Parser tok i r₂ -> Parser tok _ r₁
x <$ y = const x <$> y

------------------------------------------------------------------------
-- Parsers for sequences

infix 60 _⋆ _+

-- Not accepted by the productivity checker:

-- mutual

--   _⋆ : forall {tok r d} ->
--        Parser tok (false , d) r     ->
--        Parser tok _           (List r)
--   p ⋆ ~ return [] ∣ p +

--   _+ : forall {tok r d} ->
--        Parser tok (false , d) r     ->
--        Parser tok _           (List r)
--   p + ~ _∷_ <$> p ⊛ p ⋆

-- By inlining some definitions we can show that the definitions are
-- productive, though. The following definitions have also been
-- simplified:

mutual

  _⋆ : forall {tok r d} ->
       Parser tok (false , d) r     ->
       Parser tok _           (List r)
  p ⋆ ~ Internal.alt₀ (return []) (p +)

  _+ : forall {tok r d} ->
       Parser tok (false , d) r     ->
       Parser tok _           (List r)
  p + ~ Internal.bind₁ p     \x  ->
        Internal.bind₀ (p ⋆) \xs ->
        return (x ∷ xs)

-- p sepBy sep parses one or more ps separated by seps.

_sepBy_ : forall {tok r r' i d} ->
          Parser tok i r -> Parser tok (false , d) r' ->
          Parser tok _ (List r)
p sepBy sep = _∷_ <$> p ⊛ (sep ⊛> p) ⋆

chain₁ :  forall {tok d₁ i₂ r}
       -> Assoc
       -> Parser tok (false , d₁) r
       -> Parser tok i₂ (r -> r -> r)
       -> Parser tok _ r
chain₁ a p op = chain₁-combine a <$> (pair <$> p ⊛ op) ⋆ ⊛ p

chain :  forall {tok d₁ i₂ r}
      -> Assoc
      -> Parser tok (false , d₁) r
      -> Parser tok i₂ (r -> r -> r)
      -> r
      -> Parser tok _ r
chain a p op x = return x ∣ chain₁ a p op

------------------------------------------------------------------------
-- sat and friends

sat : forall {tok r} ->
      (tok -> Maybe r) -> Parser tok _ r
sat {tok} {r} p = symbol !>>= \c -> ok (p c)
  where
  okIndex : Maybe r -> Index
  okIndex nothing  = _
  okIndex (just _) = _

  ok : (x : Maybe r) -> Parser tok (okIndex x) r
  ok nothing  = fail
  ok (just x) = return x

sat' : forall {tok} -> (tok -> Bool) -> Parser tok _ ⊤
sat' p = sat (boolToMaybe ∘ p)

any : forall {tok} -> Parser tok _ tok
any = sat just

------------------------------------------------------------------------
-- Parsing a given token (symbol)

module Sym (a : DecSetoid) where

  open DecSetoid a using (_≟_) renaming (carrier to tok)

  sym : tok -> Parser tok _ tok
  sym x = sat p
    where
    p : tok -> Maybe tok
    p y with x ≟ y
    ... | yes _ = just y
    ... | no  _ = nothing

------------------------------------------------------------------------
-- Character parsers

digit : Parser C.Char _ ℕ
digit = 0 <$ sym '0'
      ∣ 1 <$ sym '1'
      ∣ 2 <$ sym '2'
      ∣ 3 <$ sym '3'
      ∣ 4 <$ sym '4'
      ∣ 5 <$ sym '5'
      ∣ 6 <$ sym '6'
      ∣ 7 <$ sym '7'
      ∣ 8 <$ sym '8'
      ∣ 9 <$ sym '9'
  where open Sym C.decSetoid

number : Parser C.Char _ ℕ
number = toNum <$> digit +
  where
  toNum = foldr (\n x -> 10 * x + n) 0 ∘ reverse

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


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

open import Cubical.Core.Everything
open import Cubical.Relation.Binary
open import Cubical.Algebra.Semigroup

module Cubical.Algebra.Semigroup.Construct.Quotient {c ℓ} (S : Semigroup c) {R : Rel (Semigroup.Carrier S) ℓ} (isEq : IsEquivalence R)
                                                              (closed : Congruent₂ R (Semigroup._•_ S)) where

open import Cubical.Foundations.Prelude
open import Cubical.Algebra.Properties
open import Cubical.HITs.SetQuotients

open Semigroup S
open IsEquivalence isEq

import Cubical.Algebra.Magma.Construct.Quotient magma isEq closed as QMagma
open QMagma public hiding (M/R-isMagma; M/R)

•ᴿ-assoc : Associative _•ᴿ_
•ᴿ-assoc = elimProp3 (λ _ _ _ → squash/ _ _) (λ x y z → cong [_] (assoc x y z))

S/R-isSemigroup : IsSemigroup Carrier/R _•ᴿ_
S/R-isSemigroup = record
  { isMagma = QMagma.M/R-isMagma
  ; assoc   = •ᴿ-assoc
  }

S/R : Semigroup (ℓ-max c ℓ)
S/R = record { isSemigroup = S/R-isSemigroup }


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

module Cubical.Data.Fin.Properties where

open import Cubical.Core.Everything

open import Cubical.Functions.Embedding
open import Cubical.Functions.Surjection
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport

open import Cubical.Data.Fin.Base as Fin
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty as Empty
open import Cubical.Data.Unit
open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Data.FinData.Base renaming (Fin to FinData) hiding (¬Fin0 ; toℕ)

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

open import Cubical.Induction.WellFounded

open import Cubical.Relation.Nullary

private
 variable
   a b ℓ : Level
   n : ℕ
   A : Type a

-- Fin 0 is empty, and thus a proposition.
isPropFin0 : isProp (Fin 0)
isPropFin0 = Empty.rec ∘ ¬Fin0

-- Fin 1 has only one value.
isContrFin1 : isContr (Fin 1)
isContrFin1
  = fzero , λ
  { (zero , _) → toℕ-injective refl
  ; (suc k , sk<1) → Empty.rec (¬-<-zero (pred-≤-pred sk<1))
  }

Unit≃Fin1 : Unit ≃ Fin 1
Unit≃Fin1 =
  isoToEquiv
    (iso
      (const fzero)
      (const tt)
      (isContrFin1 .snd)
      (isContrUnit .snd)
    )

-- Regardless of k, Fin k is a set.
isSetFin : ∀{k} → isSet (Fin k)
isSetFin {k} = isSetΣ isSetℕ (λ _ → isProp→isSet m≤n-isProp)

discreteFin : ∀ {n} → Discrete (Fin n)
discreteFin {n} (x , hx) (y , hy) with discreteℕ x y
... | yes prf = yes (Σ≡Prop (λ _ → m≤n-isProp) prf)
... | no prf = no λ h → prf (cong fst h)

inject<-ne : ∀ {n} (i : Fin n) → ¬ inject< ≤-refl i ≡ (n , ≤-refl)
inject<-ne {n} (k , k<n) p = <→≢ k<n (cong fst p)

Fin-fst-≡ : ∀ {n} {i j : Fin n} → fst i ≡ fst j → i ≡ j
Fin-fst-≡ = Σ≡Prop (λ _ → m≤n-isProp)

private
  subst-app : (B : A → Type b) (f : (x : A) → B x) {x y : A} (x≡y : x ≡ y) →
              subst B x≡y (f x) ≡ f y
  subst-app B f {x = x} =
    J (λ y e → subst B e (f x) ≡ f y) (substRefl {B = B} (f x))

-- Computation rules for the eliminator.
module _ (P : ∀ {k} → Fin k → Type ℓ)
         (fz : ∀ {k} → P {suc k} fzero)
         (fs : ∀ {k} {fn : Fin k} → P fn → P (fsuc fn))
         {k : ℕ} where
  elim-fzero : Fin.elim P fz fs {k = suc k} fzero ≡ fz
  elim-fzero =
    subst P (toℕ-injective _) fz ≡⟨ cong (λ p → subst P p fz) (isSetFin _ _ _ _) ⟩
    subst P refl fz              ≡⟨ substRefl {B = P} fz ⟩
    fz                           ∎

  elim-fsuc : (fk : Fin k) → Fin.elim P fz fs (fsuc fk) ≡ fs (Fin.elim P fz fs fk)
  elim-fsuc fk =
    subst P (toℕ-injective (λ _ → toℕ (fsuc fk′))) (fs (Fin.elim P fz fs fk′))
      ≡⟨ cong (λ p → subst P p (fs (Fin.elim P fz fs fk′)) ) (isSetFin _ _ _ _) ⟩
    subst P (cong fsuc fk′≡fk) (fs (Fin.elim P fz fs fk′))
      ≡⟨ subst-app _ (λ fj → fs (Fin.elim P fz fs fj)) fk′≡fk ⟩
    fs (Fin.elim P fz fs fk)
      ∎
    where
    fk′ = fst fk , pred-≤-pred (snd (fsuc fk))
    fk′≡fk : fk′ ≡ fk
    fk′≡fk = toℕ-injective refl

-- Helper function for the reduction procedure below.
--
-- If n = expand o k m, then n is congruent to m modulo k.
expand : ℕ → ℕ → ℕ → ℕ
expand 0 k m = m
expand (suc o) k m = k + expand o k m

expand≡ : ∀ k m o → expand o k m ≡ o · k + m
expand≡ k m zero = refl
expand≡ k m (suc o)
  = cong (k +_) (expand≡ k m o) ∙ +-assoc k (o · k) m

-- Expand a pair. This is useful because the whole function is
-- injective.
expand× : ∀{k} → (Fin k × ℕ) → ℕ
expand× {k} (f , o) = expand o k (toℕ f)

private
  lemma₀ : ∀{k m n r} → r ≡ n → k + m ≡ n → k ≤ r
  lemma₀ {k = k} {m} p q = m , +-comm m k ∙ q ∙ sym p

  expand×Inj : ∀ k → {t1 t2 : Fin (suc k) × ℕ} → expand× t1 ≡ expand× t2 → t1 ≡ t2
  expand×Inj k {f1 , zero} {f2 , zero} p i
    = toℕ-injective {fj = f1} {f2} p i , zero
  expand×Inj k {f1 , suc o1} {(r , r<sk) , zero} p
    = Empty.rec (<-asym r<sk (lemma₀ refl p))
  expand×Inj k {(r , r<sk) , zero} {f2 , suc o2} p
    = Empty.rec (<-asym r<sk (lemma₀ refl (sym p)))
  expand×Inj k {f1 , suc o1} {f2 , suc o2}
    = cong (λ { (f , o) → (f , suc o) })
    ∘ expand×Inj k {f1 , o1} {f2 , o2}
    ∘ inj-m+ {suc k}

  expand×Emb : ∀ k → isEmbedding (expand× {k})
  expand×Emb 0 = Empty.rec ∘ ¬Fin0 ∘ fst
  expand×Emb (suc k)
    = injEmbedding (isSetΣ isSetFin (λ _ → isSetℕ)) isSetℕ (expand×Inj k)

-- A Residue is a family of types representing evidence that a
-- natural is congruent to a value of a finite type.
Residue : ℕ → ℕ → Type₀
Residue k n = Σ[ tup ∈ Fin k × ℕ ] expand× tup ≡ n

-- There is at most one canonical finite value congruent to each
-- natural.
isPropResidue : ∀ k n → isProp (Residue k n)
isPropResidue k = isEmbedding→hasPropFibers (expand×Emb k)

-- A value of a finite type is its own residue.
Fin→Residue : ∀{k} → (f : Fin k) → Residue k (toℕ f)
Fin→Residue f = (f , 0) , refl

-- Fibers of numbers that differ by k are equivalent in a more obvious
-- way than via the fact that they are propositions.
Residue+k : (k n : ℕ) → Residue k n → Residue k (k + n)
Residue+k k n ((f , o) , p) = (f , suc o) , cong (k +_) p

Residue-k : (k n : ℕ) → Residue k (k + n) → Residue k n
Residue-k k n (((r , r<k) , zero) , p) = Empty.rec (<-asym r<k (lemma₀ p refl))
Residue-k k n ((f , suc o) , p) = ((f , o) , inj-m+ p)

Residue+k-k
  : (k n : ℕ)
  → (R : Residue k (k + n))
  → Residue+k k n (Residue-k k n R) ≡ R
Residue+k-k k n (((r , r<k) , zero) , p) = Empty.rec (<-asym r<k (lemma₀ p refl))
Residue+k-k k n ((f , suc o) , p)
  = Σ≡Prop (λ tup → isSetℕ (expand× tup) (k + n)) refl

Residue-k+k
  : (k n : ℕ)
  → (R : Residue k n)
  → Residue-k k n (Residue+k k n R) ≡ R
Residue-k+k k n ((f , o) , p)
  = Σ≡Prop (λ tup → isSetℕ (expand× tup) n) refl

private
  Residue≃ : ∀ k n → Residue k n ≃ Residue k (k + n)
  Residue≃ k n
    = Residue+k k n
    , isoToIsEquiv (iso (Residue+k k n) (Residue-k k n)
                        (Residue+k-k k n) (Residue-k+k k n))

Residue≡ : ∀ k n → Residue k n ≡ Residue k (k + n)
Residue≡ k n = ua (Residue≃ k n)

-- For positive `k`, all `n` have a canonical residue mod `k`.
module Reduce (k₀ : ℕ) where
  k : ℕ
  k = suc k₀

  base : ∀ n (n<k : n < k) → Residue k n
  base n n<k = Fin→Residue (n , n<k)

  step : ∀ n → Residue k n → Residue k (k + n)
  step n = transport (Residue≡ k n)

  reduce : ∀ n → Residue k n
  reduce = +induction k₀ (Residue k) base step

  reduce≡
    : ∀ n → transport (Residue≡ k n) (reduce n) ≡ reduce (k + n)
  reduce≡ n
    = sym (+inductionStep k₀ _ base step n)

  reduceP
    : ∀ n → PathP (λ i → Residue≡ k n i) (reduce n) (reduce (k + n))
  reduceP n = toPathP (reduce≡ n)

open Reduce using (reduce; reduce≡) public

extract : ∀{k n} → Residue k n → Fin k
extract = fst ∘ fst

private
  lemma₅
    : ∀ k n (R : Residue k n)
    →  extract R ≡ extract (transport (Residue≡ k n) R)
  lemma₅ k n = sym ∘ cong extract ∘ uaβ (Residue≃ k n)

-- The residue of n modulo k is the same as the residue of k + n.
extract≡ : ∀ k n → extract (reduce k n) ≡ extract (reduce k (suc k + n))
extract≡ k n
  = lemma₅ (suc k) n (reduce k n) ∙ cong extract (Reduce.reduce≡ k n)

isContrResidue : ∀{k n} → isContr (Residue (suc k) n)
isContrResidue {k} {n} = inhProp→isContr (reduce k n) (isPropResidue (suc k) n)

-- the modulo operator on ℕ

_%_ : ℕ → ℕ → ℕ
n % zero = n
n % (suc k) = toℕ (extract (reduce k n))

_/_ : ℕ → ℕ → ℕ
n / zero = zero
n / (suc k) = reduce k n .fst .snd

moddiv : ∀ n k → (n / k) · k + n % k ≡ n
moddiv n zero = refl
moddiv n (suc k) = sym (expand≡ _ _ (n / suc k)) ∙ reduce k n .snd

n%k≡n[modk] : ∀ n k → Σ[ o ∈ ℕ ] o · k + n % k ≡ n
n%k≡n[modk] n k = (n / k) , moddiv n k

n%sk<sk : (n k : ℕ) → (n % suc k) < suc k
n%sk<sk n k = extract (reduce k n) .snd

fznotfs : ∀ {m : ℕ} {k : Fin m} → ¬ fzero ≡ fsuc k
fznotfs {m} p = subst F p tt
  where
    F : Fin (suc m) → Type₀
    F (zero , _) = Unit
    F (suc _ , _) = ⊥

fsuc-inj : {fj fk : Fin n} → fsuc fj ≡ fsuc fk → fj ≡ fk
fsuc-inj = toℕ-injective ∘ injSuc ∘ cong toℕ

punchOut : ∀ {m} {i j : Fin (suc m)} → (¬ i ≡ j) → Fin m
punchOut {_} {i} {j} p with fsplit i | fsplit j
punchOut {_} {i} {j} p | inl prfi | inl prfj =
  Empty.elim (p (i ≡⟨ sym prfi ⟩ fzero ≡⟨ prfj ⟩ j ∎))
punchOut {_} {i} {j} p | inl prfi | inr (kj , prfj) =
  kj
punchOut {zero} {i} {j} p  | inr (ki , prfi) | inl prfj =
  Empty.elim (p (
    i ≡⟨ sym (isContrFin1 .snd i) ⟩
    c ≡⟨ isContrFin1 .snd j ⟩
    j ∎
  ))
  where c = isContrFin1 .fst
punchOut {suc _} {i} {j} p | inr (ki , prfi) | inl prfj =
  fzero
punchOut {zero} {i} {j} p | inr (ki , prfi) | inr (kj , prfj) =
  Empty.elim ((p (
    i ≡⟨ sym (isContrFin1 .snd i) ⟩
    c ≡⟨ isContrFin1 .snd j ⟩
    j ∎)
  ))
  where c = isContrFin1 .fst
punchOut {suc _} {i} {j} p | inr (ki , prfi) | inr (kj , prfj) =
  fsuc (punchOut {i = ki} {j = kj}
    (λ q → p (i ≡⟨ sym prfi ⟩ fsuc ki ≡⟨ cong fsuc q ⟩ fsuc kj ≡⟨ prfj ⟩ j ∎))
  )

punchOut-inj
  : ∀ {m} {i j k : Fin (suc m)} (i≢j : ¬ i ≡ j) (i≢k : ¬ i ≡ k)
  → punchOut i≢j ≡ punchOut i≢k → j ≡ k
punchOut-inj {_} {i} {j} {k} i≢j i≢k p with fsplit i | fsplit j | fsplit k
punchOut-inj {zero} {i} {j} {k} i≢j i≢k p | _ | _ | _ =
  Empty.elim (i≢j (i ≡⟨ sym (isContrFin1 .snd i) ⟩ c ≡⟨ isContrFin1 .snd j ⟩ j ∎))
    where c = isContrFin1 .fst
punchOut-inj {suc _} {i} {j} {k} i≢j i≢k p | inl prfi | inl prfj | _ =
  Empty.elim (i≢j (i ≡⟨ sym prfi ⟩ fzero ≡⟨ prfj ⟩ j ∎))
punchOut-inj {suc _} {i} {j} {k} i≢j i≢k p | inl prfi | _ | inl prfk =
  Empty.elim (i≢k (i ≡⟨ sym prfi ⟩ fzero ≡⟨ prfk ⟩ k ∎))
punchOut-inj {suc _} {i} {j} {k} i≢j i≢k p | inl prfi | inr (kj , prfj) | inr (kk , prfk) =
  j       ≡⟨ sym prfj ⟩
  fsuc kj ≡⟨ cong fsuc p ⟩
  fsuc kk ≡⟨ prfk ⟩
  k       ∎
punchOut-inj {suc _} {i} {j} {k} i≢j i≢k p | inr (ki , prfi) | inl prfj | inl prfk =
  j     ≡⟨ sym prfj ⟩
  fzero ≡⟨ prfk ⟩
  k     ∎
punchOut-inj {suc _} {i} {j} {k} i≢j i≢k p | inr (ki , prfi) | inr (kj , prfj) | inr (kk , prfk) =
  j ≡⟨ sym prfj ⟩
  fsuc kj ≡⟨ cong fsuc lemma4 ⟩
  fsuc kk ≡⟨ prfk ⟩
  k ∎
  where
    lemma1 = λ q → i≢j (i ≡⟨ sym prfi ⟩ fsuc ki ≡⟨ cong fsuc q ⟩ fsuc kj ≡⟨ prfj ⟩ j ∎)
    lemma2 = λ q → i≢k (i ≡⟨ sym prfi ⟩ fsuc ki ≡⟨ cong fsuc q ⟩ fsuc kk ≡⟨ prfk ⟩ k ∎)
    lemma3 = fsuc-inj p
    lemma4 = punchOut-inj lemma1 lemma2 lemma3
punchOut-inj {suc m} {i} {j} {k} i≢j i≢k p | inr (ki , prfi) | inl prfj | inr (kk , prfk) =
  Empty.rec (fznotfs p)
punchOut-inj {suc _} {i} {j} {k} i≢j i≢k p | inr (ki , prfi) | inr (kj , prfj) | inl prfk =
  Empty.rec (fznotfs (sym p))

pigeonhole-special
  : ∀ {n}
  → (f : Fin (suc n) → Fin n)
  → Σ[ i ∈ Fin (suc n) ] Σ[ j ∈ Fin (suc n) ] (¬ i ≡ j) × (f i ≡ f j)
pigeonhole-special {zero} f = Empty.rec (¬Fin0 (f fzero))
pigeonhole-special {suc n} f =
  proof (any?
    (λ (i : Fin (suc n)) →
      discreteFin (f (inject< ≤-refl i)) (f (suc n , ≤-refl))
    ))
  where
    proof
      : Dec (Σ (Fin (suc n)) (λ z → f (inject< ≤-refl z) ≡ f (suc n , ≤-refl)))
      → Σ[ i ∈ Fin (suc (suc n)) ] Σ[ j ∈ Fin (suc (suc n)) ] (¬ i ≡ j) × (f i ≡ f j)
    proof (yes (i , prf)) = inject< ≤-refl i , (suc n , ≤-refl) , inject<-ne i , prf
    proof (no h) =
      let
        g : Fin (suc n) → Fin n
        g k = punchOut
          {i = f (suc n , ≤-refl)}
          {j = f (inject< ≤-refl k)}
          (λ p → h (k , Fin-fst-≡ (sym (cong fst p))))
        i , j , i≢j , p = pigeonhole-special g
      in
        inject< ≤-refl i
      , inject< ≤-refl j
      , (λ q → i≢j (Fin-fst-≡ (cong fst q)))
      , punchOut-inj
          {i = f (suc n , ≤-refl)}
          {j = f (inject< ≤-refl i)}
          {k = f (inject< ≤-refl j)}
          (λ q → h (i , Fin-fst-≡ (sym (cong fst q))))
          (λ q → h (j , Fin-fst-≡ (sym (cong fst q))))
          (Fin-fst-≡ (cong fst p))

pigeonhole
  : ∀ {m n}
  → m < n
  → (f : Fin n → Fin m)
  → Σ[ i ∈ Fin n ] Σ[ j ∈ Fin n ] (¬ i ≡ j) × (f i ≡ f j)
pigeonhole {m} {n} (zero , sm≡n) f =
  transport transport-prf (pigeonhole-special f′)
  where
    f′ : Fin (suc m) → Fin m
    f′ = subst (λ h → Fin h → Fin m) (sym sm≡n) f

    f′≡f : PathP (λ i → Fin (sm≡n i) → Fin m) f′ f
    f′≡f i = transport-fillerExt (cong (λ h → Fin h → Fin m) (sym sm≡n)) (~ i) f

    transport-prf
      : (Σ[ i ∈ Fin (suc m) ] Σ[ j ∈ Fin (suc m) ] (¬ i ≡ j) × (f′ i ≡ f′ j))
      ≡ (Σ[ i ∈ Fin n ] Σ[ j ∈ Fin n ] (¬ i ≡ j) × (f i ≡ f j))
    transport-prf φ =
      Σ[ i ∈ Fin (sm≡n φ) ] Σ[ j ∈ Fin (sm≡n φ) ]
        (¬ i ≡ j) × (f′≡f φ i ≡ f′≡f φ j)
pigeonhole {m} {n} (suc k , prf) f =
  let
    g : Fin (suc n′) → Fin n′
    g k = fst (f′ k) , <-trans (snd (f′ k)) m<n′
    i , j , ¬q , r = pigeonhole-special g
  in transport transport-prf (i , j , ¬q , Σ≡Prop (λ _ → m≤n-isProp) (cong fst r))
  where
    n′ : ℕ
    n′ = k + suc m

    n≡sn′ : n ≡ suc n′
    n≡sn′ =
      n ≡⟨ sym prf ⟩
      suc (k + suc m) ≡⟨ refl ⟩
      suc n′ ∎

    m<n′ : m < n′
    m<n′ = k , injSuc (suc (k + suc m) ≡⟨ prf ⟩ n ≡⟨ n≡sn′ ⟩ suc n′ ∎)

    f′ : Fin (suc n′) → Fin m
    f′ = subst (λ h → Fin h → Fin m) n≡sn′ f

    f′≡f : PathP (λ i → Fin (n≡sn′ (~ i)) → Fin m) f′ f
    f′≡f i = transport-fillerExt (cong (λ h → Fin h → Fin m) n≡sn′) (~ i) f

    transport-prf
      : (Σ[ i ∈ Fin (suc n′) ] Σ[ j ∈ Fin (suc n′) ] (¬ i ≡ j) × (f′ i ≡ f′ j))
      ≡ (Σ[ i ∈ Fin n ] Σ[ j ∈ Fin n ] (¬ i ≡ j) × (f i ≡ f j))
    transport-prf φ =
      Σ[ i ∈ Fin (n≡sn′ (~ φ)) ] Σ[ j ∈ Fin (n≡sn′ (~ φ)) ]
        (¬ i ≡ j) × (f′≡f φ i ≡ f′≡f φ j)

Fin-inj′ : {n m : ℕ} → n < m → ¬ Fin m ≡ Fin n
Fin-inj′ n<m p =
  let
    i , j , i≢j , q = pigeonhole n<m (transport p)
  in i≢j (
    i ≡⟨ refl ⟩
    fst (pigeonhole n<m (transport p)) ≡⟨ transport-p-inj {p = p} q ⟩
    fst (snd (pigeonhole n<m (transport p))) ≡⟨ refl ⟩
    j ∎
  )
  where
    transport-p-inj
      : ∀ {A B : Type ℓ} {x y : A} {p : A ≡ B}
      → transport p x ≡ transport p y
      → x ≡ y
    transport-p-inj {x = x} {y = y} {p = p} q =
      x ≡⟨ sym (transport⁻Transport p x) ⟩
      transport (sym p) (transport p x) ≡⟨ cong (transport (sym p)) q ⟩
      transport (sym p) (transport p y) ≡⟨ transport⁻Transport p y ⟩
      y ∎

Fin-inj : (n m : ℕ) → Fin n ≡ Fin m → n ≡ m
Fin-inj n m p with n ≟ m
... | eq prf = prf
... | lt n<m = Empty.rec (Fin-inj′ n<m (sym p))
... | gt n>m = Empty.rec (Fin-inj′ n>m p)

≤-·sk-cancel : ∀ {m} {k} {n} → m · suc k ≤ n · suc k → m ≤ n
≤-·sk-cancel {m} {k} {n} (d , p) = o , inj-·sm {m = k} goal where
  r = d % suc k
  o = d / suc k
  resn·k : Residue (suc k) (n · suc k)
  resn·k = ((r , n%sk<sk d k) , (o + m)) , reason where
   reason = expand× ((r , n%sk<sk d k) , o + m) ≡⟨ expand≡ (suc k) r (o + m) ⟩
            (o + m) · suc k + r                 ≡[ i ]⟨ +-comm (·-distribʳ o m (suc k) (~ i)) r i ⟩
            r + (o · suc k + m · suc k)         ≡⟨ +-assoc r (o · suc k) (m · suc k) ⟩
            (r + o · suc k) + m · suc k         ≡⟨ cong (_+ m · suc k) (+-comm r (o · suc k) ∙ moddiv d (suc k)) ⟩
            d + m · suc k                       ≡⟨ p ⟩
            n · suc k ∎

  residuek·n : ∀ k n → (r : Residue (suc k) (n · suc k)) → ((fzero , n) , expand≡ (suc k) 0 n ∙ +-zero _) ≡ r
  residuek·n _ _ = isContr→isProp isContrResidue _

  r≡0 : r ≡ 0
  r≡0 = cong (toℕ ∘ extract) (sym (residuek·n k n resn·k))
  d≡o·sk : d ≡ o · suc k
  d≡o·sk = sym (moddiv d (suc k)) ∙∙ cong (o · suc k +_) r≡0 ∙∙ +-zero _
  goal : (o + m) · suc k ≡ n · suc k
  goal = sym (·-distribʳ o m (suc k)) ∙∙ cong (_+ m · suc k) (sym d≡o·sk) ∙∙ p

<-·sk-cancel : ∀ {m} {k} {n} → m · suc k < n · suc k → m < n
<-·sk-cancel {m} {k} {n} p = goal where
  ≤-helper : m ≤ n
  ≤-helper = ≤-·sk-cancel (pred-≤-pred (<≤-trans p (≤-suc ≤-refl)))
  goal : m < n
  goal = case <-split (suc-≤-suc ≤-helper) of λ
    { (inl g) → g
    ; (inr e) → Empty.rec (¬m<m (subst (λ m → m · suc k < n · suc k) e p))
    }

factorEquiv : ∀ {n} {m} → Fin n × Fin m ≃ Fin (n · m)
factorEquiv {zero} {m} = uninhabEquiv (¬Fin0 ∘ fst) ¬Fin0
factorEquiv {suc n} {m} = intro , isEmbedding×isSurjection→isEquiv (isEmbeddingIntro , isSurjectionIntro) where
  intro : Fin (suc n) × Fin m → Fin (suc n · m)
  intro (nn , mm) = nm , subst (λ nm₁ → nm₁ < suc n · m) (sym (expand≡ _ (toℕ nn) (toℕ mm))) nm<n·m where
    nm : ℕ
    nm = expand× (nn , toℕ mm)
    nm<n·m : toℕ mm · suc n + toℕ nn < suc n · m
    nm<n·m =
      toℕ mm · suc n + toℕ nn <≤⟨ <-k+ (snd nn) ⟩
      toℕ mm · suc n + suc n  ≡≤⟨ +-comm _ (suc n) ⟩
      suc (toℕ mm) · suc n    ≤≡⟨ ≤-·k (snd mm) ⟩
      m · suc n               ≡⟨ ·-comm _ (suc n) ⟩
      suc n · m               ∎ where open <-Reasoning

  intro-injective : ∀ {o} {p} → intro o ≡ intro p → o ≡ p
  intro-injective {o} {p} io≡ip = λ i → io′≡ip′ i .fst , toℕ-injective {fj = snd o} {fk = snd p} (cong snd io′≡ip′) i where
    io′≡ip′ : (fst o , toℕ (snd o)) ≡ (fst p , toℕ (snd p))
    io′≡ip′ = expand×Inj _ (cong fst io≡ip)
  isEmbeddingIntro : isEmbedding intro
  isEmbeddingIntro = injEmbedding (isSet× isSetFin isSetFin) isSetFin intro-injective

  elimF : ∀ nm → fiber intro nm
  elimF nm = ((nn , nn<n) , (mm , mm<m)) , toℕ-injective (reduce n (toℕ nm) .snd) where
    mm = toℕ nm / suc n
    nn = toℕ nm % suc n

    nmmoddiv : mm · suc n + nn ≡ toℕ nm
    nmmoddiv = moddiv _ (suc n)
    nn<n : nn < suc n
    nn<n = n%sk<sk (toℕ nm) _

    nmsnd : mm · suc n + nn < suc n · m
    nmsnd = subst (λ l → l < suc n · m) (sym nmmoddiv) (snd nm)
    mm·sn<m·sn : mm · suc n < m · suc n
    mm·sn<m·sn =
      mm · suc n      ≤<⟨ nn , +-comm nn (mm · suc n) ⟩
      mm · suc n + nn <≡⟨ nmsnd ⟩
      suc n · m       ≡⟨ ·-comm (suc n) m ⟩
      m · suc n       ∎ where open <-Reasoning
    mm<m : mm < m
    mm<m = <-·sk-cancel mm·sn<m·sn

  isSurjectionIntro : isSurjection intro
  isSurjectionIntro = ∣_∣ ∘ elimF

-- Fin (m + n) ≡ Fin m ⊎ Fin n
-- ===========================

o<m→o<m+n : (m n o : ℕ) → o < m → o < (m + n)
o<m→o<m+n m n o (k , p) = (n + k) , (n + k + suc o    ≡⟨ sym (+-assoc n k _)  ⟩
                                     n + (k + suc o)  ≡⟨ cong (λ - → n + -) p ⟩
                                     n + m            ≡⟨ +-comm n m           ⟩
                                     m + n            ∎)

∸-<-lemma : (m n o : ℕ) → o < m + n → m ≤ o → o ∸ m < n
∸-<-lemma zero    n o       o<m+n m<o = o<m+n
∸-<-lemma (suc m) n zero    o<m+n m<o = Empty.rec (¬-<-zero m<o)
∸-<-lemma (suc m) n (suc o) o<m+n m<o =
  ∸-<-lemma m n o (pred-≤-pred o<m+n) (pred-≤-pred m<o)

-- A convenient wrapper on top of trichotomy, as we will be interested in
-- whether `m < n` or `n ≤ m`.
_≤?_ : (m n : ℕ) → (m < n) ⊎ (n ≤ m)
_≤?_ m n with m ≟ n
_≤?_ m n | lt m<n = inl m<n
_≤?_ m n | eq m=n = inr (subst (λ - → - ≤ m) m=n ≤-refl)
_≤?_ m n | gt n<m = inr (<-weaken n<m)

¬-<-and-≥ : {m n : ℕ} → m < n → ¬ n ≤ m
¬-<-and-≥ {m}     {zero}  m<n n≤m = ¬-<-zero m<n
¬-<-and-≥ {zero}  {suc n} m<n n≤m = ¬-<-zero n≤m
¬-<-and-≥ {suc m} {suc n} m<n n≤m = ¬-<-and-≥ (pred-≤-pred m<n) (pred-≤-pred n≤m)

m+n∸n=m : (n m : ℕ) → (m + n) ∸ n ≡ m
m+n∸n=m zero    k = +-zero k
m+n∸n=m (suc m) k = (k + suc m) ∸ suc m   ≡⟨ cong (λ - → - ∸ suc m) (+-suc k m) ⟩
                    suc (k + m) ∸ (suc m) ≡⟨ refl                               ⟩
                    (k + m) ∸ m           ≡⟨ m+n∸n=m m k                        ⟩
                    k                     ∎

∸-lemma : {m n : ℕ} → m ≤ n → m + (n ∸ m) ≡ n
∸-lemma {zero}  {k}     _   = refl {x = k}
∸-lemma {suc m} {zero}  m≤k = Empty.rec (¬-<-and-≥ (suc-≤-suc zero-≤) m≤k)
∸-lemma {suc m} {suc k} m≤k =
  suc m + (suc k ∸ suc m)   ≡⟨ refl                                 ⟩
  suc (m + (suc k ∸ suc m)) ≡⟨ refl                                 ⟩
  suc (m + (k ∸ m))         ≡⟨ cong suc (∸-lemma (pred-≤-pred m≤k)) ⟩
  suc k                     ∎

Fin+≅Fin⊎Fin : (m n : ℕ) → Iso (Fin (m + n)) (Fin m ⊎ Fin n)
Iso.fun (Fin+≅Fin⊎Fin m n) = f
  where
    f : Fin (m + n) → Fin m ⊎ Fin n
    f (k , k<m+n) with k ≤? m
    f (k , k<m+n) | inl k<m = inl (k , k<m)
    f (k , k<m+n) | inr k≥m = inr (k ∸ m , ∸-<-lemma m n k k<m+n k≥m)
Iso.inv (Fin+≅Fin⊎Fin m n) = g
  where
    g :  Fin m  ⊎  Fin n  →  Fin (m + n)
    g (inl (k , k<m)) = k     , o<m→o<m+n m n k k<m
    g (inr (k , k<n)) = m + k , <-k+ k<n
Iso.rightInv (Fin+≅Fin⊎Fin m n) = sec-f-g
  where
    sec-f-g : _
    sec-f-g (inl (k , k<m)) with k ≤? m
    sec-f-g (inl (k , k<m)) | inl _   = cong inl (Σ≡Prop (λ _ → m≤n-isProp) refl)
    sec-f-g (inl (k , k<m)) | inr m≤k = Empty.rec (¬-<-and-≥ k<m m≤k)
    sec-f-g (inr (k , k<n)) with (m + k) ≤? m
    sec-f-g (inr (k , k<n)) | inl p   = Empty.rec (¬m+n<m {m} {k} p)
    sec-f-g (inr (k , k<n)) | inr k≥m = cong inr (Σ≡Prop (λ _ → m≤n-isProp) rem)
      where
        rem : (m + k) ∸ m ≡ k
        rem = subst (λ - → - ∸ m ≡ k) (+-comm k m) (m+n∸n=m m k)
Iso.leftInv  (Fin+≅Fin⊎Fin m n) = ret-f-g
  where
    ret-f-g : _
    ret-f-g (k , k<m+n) with k ≤? m
    ret-f-g (k , k<m+n) | inl _   = Σ≡Prop (λ _ → m≤n-isProp) refl
    ret-f-g (k , k<m+n) | inr m≥k = Σ≡Prop (λ _ → m≤n-isProp) (∸-lemma m≥k)

Fin+≡Fin⊎Fin : (m n : ℕ) → Fin (m + n) ≡ Fin m ⊎ Fin n
Fin+≡Fin⊎Fin m n = isoToPath (Fin+≅Fin⊎Fin m n)

-- Equivalence between FinData and Fin

sucFin : {N : ℕ} → Fin N → Fin (suc N)
sucFin (k , n , p) = suc k , n , (+-suc _ _ ∙ cong suc p)

FinData→Fin : (N : ℕ) → FinData N → Fin N
FinData→Fin zero ()
FinData→Fin (suc N) zero = 0 , suc-≤-suc zero-≤
FinData→Fin (suc N) (suc k) = sucFin (FinData→Fin N k)

Fin→FinData : (N : ℕ) → Fin N → FinData N
Fin→FinData zero (k , n , p) = Empty.rec (snotz (sym (+-suc n k) ∙ p))
Fin→FinData (suc N) (0 , n , p) = zero
Fin→FinData (suc N) ((suc k) , n , p) = suc (Fin→FinData N (k , n , p')) where
  p' : n + suc k ≡ N
  p' = injSuc (sym (+-suc n (suc k)) ∙ p)

secFin : (n : ℕ) → section (FinData→Fin n) (Fin→FinData n)
secFin 0 (k , n , p) = Empty.rec (snotz (sym (+-suc n k) ∙ p))
secFin (suc N) (0 , n , p) = Fin-fst-≡ refl
secFin (suc N) (suc k , n , p) = Fin-fst-≡ (cong suc (cong fst (secFin N (k , n , p')))) where
  p' : n + suc k ≡ N
  p' = injSuc (sym (+-suc n (suc k)) ∙ p)

retFin : (n : ℕ) → retract (FinData→Fin n) (Fin→FinData n)
retFin 0 ()
retFin (suc N) zero = refl
retFin (suc N) (suc k) = cong FinData.suc (cong (Fin→FinData N) (Fin-fst-≡ refl) ∙ retFin N k)

FinDataIsoFin : (N : ℕ) → Iso (FinData N) (Fin N)
Iso.fun (FinDataIsoFin N) = FinData→Fin N
Iso.inv (FinDataIsoFin N) = Fin→FinData N
Iso.rightInv (FinDataIsoFin N) = secFin N
Iso.leftInv (FinDataIsoFin N) = retFin N

FinData≃Fin : (N : ℕ) → FinData N ≃ Fin N
FinData≃Fin N = isoToEquiv (FinDataIsoFin N)

FinData≡Fin : (N : ℕ) → FinData N ≡ Fin N
FinData≡Fin N = ua (FinData≃Fin N)

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
import      Lvl
open import Structure.Setoid
open import Type

module Structure.Operator.Vector.Subspaces.Kernel
  {ℓₛ ℓₛₑ}
  {S : Type{ℓₛ}}
  ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  {_+ₛ_ _⋅ₛ_ : S → S → S}
  where

open import Logic.Predicate
open import Sets.ExtensionalPredicateSet as PredSet using (PredSet ; _∈_ ; [∋]-binaryRelator)
open import Structure.Container.SetLike as SetLike using (SetElement)
open import Structure.Function.Multi
open import Structure.Operator
open import Structure.Operator.Properties
open import Structure.Operator.Vector
open import Structure.Operator.Vector.LinearMap
open import Structure.Operator.Vector.Proofs
open import Structure.Operator.Vector.Subspace
open import Structure.Relator.Properties
open import Syntax.Implication
open import Syntax.Transitivity

open VectorSpace ⦃ … ⦄
open VectorSpaceVObject ⦃ … ⦄ using (_+ᵥ_; _⋅ₛᵥ_)
open VectorSpaceVObject       using (Vector)

private variable ℓ ℓᵥ ℓᵥₑ : Lvl.Level
private variable V W : VectorSpaceVObject {ℓᵥ = ℓᵥ} {ℓᵥₑ = ℓᵥₑ} ⦃ equiv-S = equiv-S ⦄ (_+ₛ_)(_⋅ₛ_)
private variable F : V →ˡⁱⁿᵉᵃʳᵐᵃᵖ W

kernel : (V →ˡⁱⁿᵉᵃʳᵐᵃᵖ W) → PredSet(Vector(V))
kernel {V = V}{W = W} ([∃]-intro f) = PredSet.unapply f(𝟎ᵥ)

kernel-subspace : Subspace(kernel(F))
SetLike.FunctionProperties._closed-under₂_.proof (Subspace.add-closure (kernel-subspace {_} {_} {V} {_} {_} {W} {F = F@([∃]-intro f)})) {x} {y} xkern ykern =
  • (
    xkern         ⇒
    x ∈ kernel(F) ⇒-[]
    f(x) ≡ 𝟎ᵥ     ⇒-end
  )
  • (
    ykern         ⇒
    y ∈ kernel(F) ⇒-[]
    f(y) ≡ 𝟎ᵥ     ⇒-end
  )                       ⇒₂-[ congruence₂{A₁ = Vector(W)}{A₂ = Vector(W)}(_+ᵥ_) ]
  f(x) +ᵥ f(y) ≡ 𝟎ᵥ +ᵥ 𝟎ᵥ ⇒-[ _🝖 identityᵣ(_+ᵥ_)(𝟎ᵥ) ]
  f(x) +ᵥ f(y) ≡ 𝟎ᵥ       ⇒-[ preserving₂(f)(_+ᵥ_)(_+ᵥ_) 🝖_ ]
  f(x +ᵥ y) ≡ 𝟎ᵥ          ⇒-[]
  (x +ᵥ y) ∈ kernel(F)    ⇒-end
  where
    instance _ = V
    instance _ = W
SetLike.FunctionProperties._closed-under₁_.proof (Subspace.mul-closure (kernel-subspace {_}{_}{V}{_}{_}{W} {F = F@([∃]-intro f)}) {s}) {v} vkern =
  vkern ⇒
  v ∈ kernel(F)         ⇒-[]
  f(v) ≡ 𝟎ᵥ             ⇒-[ congruence₂ᵣ(_⋅ₛᵥ_)(s) ]
  s ⋅ₛᵥ f(v) ≡ s ⋅ₛᵥ 𝟎ᵥ ⇒-[ _🝖 [⋅ₛᵥ]-absorberᵣ ]
  s ⋅ₛᵥ f(v) ≡ 𝟎ᵥ       ⇒-[ preserving₁(f)(s ⋅ₛᵥ_)(s ⋅ₛᵥ_) 🝖_ ]
  f(s ⋅ₛᵥ v) ≡ 𝟎ᵥ       ⇒-[]
  (s ⋅ₛᵥ v) ∈ kernel(F) ⇒-end
  where
    instance _ = V
    instance _ = W

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:
-- Andreas and James, Nov 2011 and Oct 2012
-- function with flexible arity
-- {-# OPTIONS -v tc.cover:20 #-}
module FlexibleInterpreter where

open import Common.Equality
open import Common.IO
open import Common.Nat renaming (zero to Z; suc to S) hiding (pred)

data Ty : Set where
  nat : Ty
  arr : Ty -> Ty -> Ty

data Exp : Ty -> Set where
  zero : Exp nat
  suc  : Exp (arr nat nat)
  pred : Exp (arr nat nat)
  app  : {a b : Ty} -> Exp (arr a b) -> Exp a -> Exp b

Sem : Ty -> Set
Sem nat = Nat
Sem (arr a b) = Sem a -> Sem b

module Flex where
  -- Haskell does not seem to handle this

  eval' : (a : Ty) -> Exp a -> Sem a
  eval' ._ zero = Z
  eval' ._ suc  = S
  eval' b (app f e) = eval' _ f (eval' _ e)
  eval' .(arr nat nat) pred Z = Z
  eval' ._ pred (S n) = n

  eval : {a : Ty} -> Exp a -> Sem a
  eval zero         = Z
  eval suc          = S
  eval pred Z       = Z
  eval pred (S n)   = n
  eval (app f e)    = eval f (eval e)

  testEvalSuc : ∀ {n} → eval suc n ≡ S n
  testEvalSuc = refl

  testEvalPredZero : eval pred Z ≡ Z
  testEvalPredZero = refl

  testEvalPredSuc : ∀ {n} → eval pred (S n) ≡ n
  testEvalPredSuc = refl

module Rigid where
  -- This executes fine

  eval : {a : Ty} -> Exp a -> Sem a
  eval zero      = Z
  eval suc       = S
  eval pred      = λ { Z    -> Z
                     ; (S n) -> n
                     }
  eval (app f e) = eval f (eval e)

open Flex

expr = (app pred (app suc (app suc zero)))
test = eval expr
main = printNat test
-- should print 1

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Nat.Coprime where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Data.Sigma
open import Cubical.Data.NatPlusOne

open import Cubical.HITs.PropositionalTruncation as PropTrunc

open import Cubical.Data.Nat.Base
open import Cubical.Data.Nat.Properties
open import Cubical.Data.Nat.Divisibility
open import Cubical.Data.Nat.GCD

areCoprime : ℕ × ℕ → Type₀
areCoprime (m , n) = isGCD m n 1

-- Any pair (m , n) can be converted to a coprime pair (m' , n') s.t.
--  m' ∣ m, n' ∣ n if and only if one of m or n is nonzero

module _ ((m , n) : ℕ × ℕ₊₁) where
  private
    d    = gcd m (ℕ₊₁→ℕ n)
    d∣m  = gcdIsGCD m (ℕ₊₁→ℕ n) .fst .fst
    d∣sn = gcdIsGCD m (ℕ₊₁→ℕ n) .fst .snd
    gr   = gcdIsGCD m (ℕ₊₁→ℕ n) .snd

    c₁ : ℕ
    p₁ : c₁ * d ≡ m
    c₁ = ∣-untrunc d∣m .fst; p₁ = ∣-untrunc d∣m .snd

    c₂ : ℕ₊₁
    p₂ : (ℕ₊₁→ℕ c₂) * d ≡ (ℕ₊₁→ℕ n)
    c₂ = 1+ (∣s-untrunc d∣sn .fst); p₂ = ∣s-untrunc d∣sn .snd

  toCoprime : ℕ × ℕ₊₁ → ℕ × ℕ₊₁
  toCoprime (m , n) = (c₁ , c₂)

  private
    lem : ∀ a {b c d e} → a * b ≡ c → c * d ≡ e → a * (b * d) ≡ e
    lem a p q = *-assoc a _ _ ∙ cong (_* _) p ∙ q

    gr' : ∀ d' → prediv d' c₁ → prediv d' (ℕ₊₁→ℕ c₂) → (d' * d) ∣ d
    gr' d' (b₁ , q₁) (b₂ , q₂) = gr (d' * d) ((∣ b₁ , lem b₁ q₁ p₁ ∣) ,
                                              (∣ b₂ , lem b₂ q₂ p₂ ∣))

    -- this only works because d > 0 (<=> m > 0 or n > 0)
    d-cancelʳ : ∀ d' → (d' * d) ∣ d → d' ∣ 1
    d-cancelʳ d' div = ∣-cancelʳ d-1 (∣-trans (subst (λ x → (d' * x) ∣ x) p div)
                                              (∣-refl (sym (*-identityˡ _))))
      where d-1 = m∣sn→z<m d∣sn .fst
            p : d ≡ suc d-1
            p = sym (+-comm 1 d-1 ∙ m∣sn→z<m d∣sn .snd)

  toCoprimeAreCoprime : areCoprime (c₁ , ℕ₊₁→ℕ c₂)
  fst toCoprimeAreCoprime = ∣-oneˡ c₁ , ∣-oneˡ (ℕ₊₁→ℕ c₂)
  snd toCoprimeAreCoprime d' (d'∣c₁ , d'∣sc₂) = PropTrunc.rec isProp∣ (λ a →
                                                PropTrunc.rec isProp∣ (λ b →
                                                 d-cancelʳ d' (gr' d' a b)) d'∣sc₂) d'∣c₁

  toCoprime∣ : (c₁ ∣ m) × (ℕ₊₁→ℕ c₂ ∣ ℕ₊₁→ℕ n)
  toCoprime∣ = ∣ d , *-comm d c₁ ∙ p₁ ∣ , ∣ d , *-comm d (ℕ₊₁→ℕ c₂) ∙ p₂ ∣


text:
-- Andreas, 2015-02-24

data Wrap (A : Set) : Set where
  wrap : A → Wrap A

data D : Set → Set1 where
  c : (A : Set) → D (Wrap A)

test : (A : Set) → D A → Set
test .(Wrap A) (c A) = A

-- this should crash Epic as long as A is considered forced in constructor c

-- should succeed now


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Comonads
------------------------------------------------------------------------

-- Note that currently the monad laws are not included here.

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

module Category.Comonad where

open import Level
open import Function

record RawComonad {f} (W : Set f → Set f) : Set (suc f) where

  infixl 1 _=>>_ _=>=_
  infixr 1 _<<=_ _=<=_

  field
    extract : ∀ {A} → W A → A
    extend  : ∀ {A B} → (W A → B) → (W A → W B)

  duplicate : ∀ {A} → W A → W (W A)
  duplicate = extend id

  liftW : ∀ {A B} → (A → B) → W A → W B
  liftW f = extend (f ∘′ extract)

  _=>>_ : ∀ {A B} → W A → (W A → B) → W B
  _=>>_ = flip extend

  _=>=_ : ∀ {c A B} {C : Set c} → (W A → B) → (W B → C) → W A → C
  f =>= g = g ∘′ extend f

  _<<=_ : ∀ {A B} → (W A → B) → W A → W B
  _<<=_ = extend

  _=<=_ : ∀ {A B c} {C : Set c} → (W B → C) → (W A → B) → W A → C
  _=<=_ = flip _=>=_


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A pointwise lifting of a relation to incorporate an additional point.
------------------------------------------------------------------------

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

-- This module is designed to be used with
-- Relation.Nullary.Construct.Add.Point

open import Relation.Binary

module Relation.Binary.Construct.Add.Point.Equality
  {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where

open import Level using (_⊔_)
open import Function
import Relation.Binary.PropositionalEquality as P
open import Relation.Nullary
open import Relation.Nullary.Construct.Add.Point
import Relation.Nullary.Decidable as Dec

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

data _≈∙_ : Rel (Pointed A) (a ⊔ ℓ) where
  ∙≈∙ :                     ∙     ≈∙ ∙
  [_] : {k l : A} → k ≈ l → [ k ] ≈∙ [ l ]

------------------------------------------------------------------------
-- Relational properties

[≈]-injective : ∀ {k l} → [ k ] ≈∙ [ l ] → k ≈ l
[≈]-injective [ k≈l ] = k≈l

≈∙-refl : Reflexive _≈_ → Reflexive _≈∙_
≈∙-refl ≈-refl {∙}     = ∙≈∙
≈∙-refl ≈-refl {[ k ]} = [ ≈-refl ]

≈∙-sym : Symmetric _≈_ → Symmetric _≈∙_
≈∙-sym ≈-sym ∙≈∙     = ∙≈∙
≈∙-sym ≈-sym [ x≈y ] = [ ≈-sym x≈y ]

≈∙-trans : Transitive _≈_ → Transitive _≈∙_
≈∙-trans ≈-trans ∙≈∙     ∙≈z     = ∙≈z
≈∙-trans ≈-trans [ x≈y ] [ y≈z ] = [ ≈-trans x≈y y≈z ]

≈∙-dec : Decidable _≈_ → Decidable _≈∙_
≈∙-dec _≟_ ∙     ∙     = yes ∙≈∙
≈∙-dec _≟_ ∙     [ l ] = no (λ ())
≈∙-dec _≟_ [ k ] ∙     = no (λ ())
≈∙-dec _≟_ [ k ] [ l ] = Dec.map′ [_] [≈]-injective (k ≟ l)

≈∙-irrelevant : Irrelevant _≈_ → Irrelevant _≈∙_
≈∙-irrelevant ≈-irr ∙≈∙   ∙≈∙   = P.refl
≈∙-irrelevant ≈-irr [ p ] [ q ] = P.cong _ (≈-irr p q)

≈∙-substitutive : ∀ {ℓ} → Substitutive _≈_ ℓ → Substitutive _≈∙_ ℓ
≈∙-substitutive ≈-subst P ∙≈∙   = id
≈∙-substitutive ≈-subst P [ p ] = ≈-subst (P ∘′ [_]) p

------------------------------------------------------------------------
-- Structures

≈∙-isEquivalence : IsEquivalence _≈_ → IsEquivalence _≈∙_
≈∙-isEquivalence ≈-isEquivalence = record
  { refl  = ≈∙-refl refl
  ; sym   = ≈∙-sym sym
  ; trans = ≈∙-trans trans
  } where open IsEquivalence ≈-isEquivalence

≈∙-isDecEquivalence : IsDecEquivalence _≈_ → IsDecEquivalence _≈∙_
≈∙-isDecEquivalence ≈-isDecEquivalence = record
  { isEquivalence = ≈∙-isEquivalence isEquivalence
  ; _≟_           = ≈∙-dec _≟_
  } where open IsDecEquivalence ≈-isDecEquivalence


text:
module _ where

module A where

  postulate
    _∷_ _∙_ bind : Set

  infixr 5 _∷_
  infixr 5 _∙_
  infix  1 bind

  syntax bind c (λ x → d) = x ← c , d

module B where

  postulate
    _∷_ _∙_ bind : Set

  infix  5 _∷_
  infixr 4 _∙_
  infixl 2 bind

  syntax bind c d = c ∙ d

module C where

  postulate
    bind : Set

  infixr 2 bind

  syntax bind c d = c ∙ d

open A
open B
open C

-- _∷_ is infix 5.
-- _∙_ has two fixities: infixr 4 and infixr 5.
-- A.bind's notation is infix 1.
-- B.bind and C.bind's notations are infix 2.

-- There is one instance of _∷_ in the grammar.

-- There are three instances of _∙_ in the grammar, one
-- corresponding to A._∙_, one corresponding to B._∙_, and one
-- corresponding to both B.bind and C.bind.

Foo : Set
Foo = ∷ ∙ ← ,


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

open import LogicalFormulae
open import Groups.Lemmas
open import Groups.Definition
open import Setoids.Orders.Partial.Definition
open import Setoids.Setoids
open import Functions.Definition
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.Orders.Partial.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order

module Rings.Orders.Partial.Lemmas {n m p : _} {A : Set n} {S : Setoid {n} {m} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {_} {p} A} {R : Ring S _+_ _*_} {pOrder : SetoidPartialOrder S _<_} (pRing : PartiallyOrderedRing R pOrder) where

abstract

  open PartiallyOrderedRing pRing
  open Setoid S
  open SetoidPartialOrder pOrder
  open Ring R
  open Group additiveGroup
  open Equivalence eq

  open import Rings.Lemmas R

  ringAddInequalities : {w x y z : A} → w < x → y < z → (w + y) < (x + z)
  ringAddInequalities {w = w} {x} {y} {z} w<x y<z = <Transitive (orderRespectsAddition w<x y) (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition y<z x))

  ringCanMultiplyByPositive : {x y c : A} → (Ring.0R R) < c → x < y → (x * c) < (y * c)
  ringCanMultiplyByPositive {x} {y} {c} 0<c x<y = SetoidPartialOrder.<WellDefined pOrder reflexive (Group.identRight additiveGroup) q'
    where
      have : 0R < (y + Group.inverse additiveGroup x)
      have = SetoidPartialOrder.<WellDefined pOrder (Group.invRight additiveGroup) reflexive (orderRespectsAddition x<y (Group.inverse additiveGroup x))
      p1 : 0R < ((y * c) + ((Group.inverse additiveGroup x) * c))
      p1 = SetoidPartialOrder.<WellDefined pOrder reflexive (transitive *Commutative (transitive *DistributesOver+ ((Group.+WellDefined additiveGroup) *Commutative *Commutative))) (orderRespectsMultiplication have 0<c)
      p' : 0R < ((y * c) + (Group.inverse additiveGroup (x * c)))
      p' = SetoidPartialOrder.<WellDefined pOrder reflexive (Group.+WellDefined additiveGroup reflexive (transitive (transitive *Commutative ringMinusExtracts) (inverseWellDefined additiveGroup *Commutative))) p1
      q : (0R + (x * c)) < (((y * c) + (Group.inverse additiveGroup (x * c))) + (x * c))
      q = orderRespectsAddition p' (x * c)
      q' : (x * c) < ((y * c) + 0R)
      q' = SetoidPartialOrder.<WellDefined pOrder (Group.identLeft additiveGroup) (transitive (symmetric (Group.+Associative additiveGroup)) (Group.+WellDefined additiveGroup reflexive (Group.invLeft additiveGroup))) q

  ringCanMultiplyByPositive' : {x y c : A} → (Ring.0R R) < c → x < y → (c * x) < (c * y)
  ringCanMultiplyByPositive' {x} {y} {c} 0<c x<y = SetoidPartialOrder.<WellDefined pOrder *Commutative *Commutative (ringCanMultiplyByPositive 0<c x<y)

  ringMultiplyPositives : {x y a b : A} → 0R < x → 0R < a → (x < y) → (a < b) → (x * a) < (y * b)
  ringMultiplyPositives {x} {y} {a} {b} 0<x 0<a x<y a<b = SetoidPartialOrder.<Transitive pOrder (ringCanMultiplyByPositive 0<a x<y) (<WellDefined *Commutative *Commutative (ringCanMultiplyByPositive (SetoidPartialOrder.<Transitive pOrder 0<x x<y) a<b))

  ringSwapNegatives : {x y : A} → (Group.inverse (Ring.additiveGroup R) x) < (Group.inverse (Ring.additiveGroup R) y) → y < x
  ringSwapNegatives {x} {y} -x<-y = SetoidPartialOrder.<WellDefined pOrder (transitive (symmetric (Group.+Associative additiveGroup)) (transitive (Group.+WellDefined additiveGroup reflexive (Group.invLeft additiveGroup)) (Group.identRight additiveGroup))) (Group.identLeft additiveGroup) v
    where
      t : ((Group.inverse additiveGroup x) + y) < ((Group.inverse additiveGroup y) + y)
      t = orderRespectsAddition -x<-y y
      u : (y + (Group.inverse additiveGroup x)) < 0R
      u = SetoidPartialOrder.<WellDefined pOrder (groupIsAbelian) (Group.invLeft additiveGroup) t
      v : ((y + (Group.inverse additiveGroup x)) + x) < (0R + x)
      v = orderRespectsAddition u x

  ringSwapNegatives' : {x y : A} → x < y → (Group.inverse (Ring.additiveGroup R) y) < (Group.inverse (Ring.additiveGroup R) x)
  ringSwapNegatives' {x} {y} x<y = ringSwapNegatives (<WellDefined (Equivalence.symmetric eq (invTwice additiveGroup _)) (Equivalence.symmetric eq (invTwice additiveGroup _)) x<y)

  ringCanMultiplyByNegative : {x y c : A} → c < (Ring.0R R) → x < y → (y * c) < (x * c)
  ringCanMultiplyByNegative {x} {y} {c} c<0 x<y = ringSwapNegatives u
    where
    open Equivalence eq
    p1 : (c + Group.inverse additiveGroup c) < (0R + Group.inverse additiveGroup c)
    p1 = orderRespectsAddition c<0 _
    0<-c : 0R < (Group.inverse additiveGroup c)
    0<-c = SetoidPartialOrder.<WellDefined pOrder (Group.invRight additiveGroup) (Group.identLeft additiveGroup) p1
    t : (x * Group.inverse additiveGroup c) < (y * Group.inverse additiveGroup c)
    t = ringCanMultiplyByPositive 0<-c x<y
    u : (Group.inverse additiveGroup (x * c)) < Group.inverse additiveGroup (y * c)
    u = SetoidPartialOrder.<WellDefined pOrder ringMinusExtracts ringMinusExtracts t

  anyComparisonImpliesNontrivial : {a b : A} → a < b → (0R ∼ 1R) → False
  anyComparisonImpliesNontrivial {a} {b} a<b 0=1 = irreflexive (<WellDefined (oneZeroImpliesAllZero 0=1) (oneZeroImpliesAllZero 0=1) a<b)

  moveInequality : {a b : A} → a < b → 0R < (b + inverse a)
  moveInequality {a} {b} a<b = <WellDefined invRight reflexive (orderRespectsAddition a<b (inverse a))

  moveInequality' : {a b : A} → a < b → (a + inverse b) < 0R
  moveInequality' {a} {b} a<b = <WellDefined reflexive invRight (orderRespectsAddition a<b (inverse b))

  greaterImpliesNotEqual : {a b : A} → a < b → (a ∼ b → False)
  greaterImpliesNotEqual {a} {b} a<b a=b = irreflexive (<WellDefined a=b reflexive a<b)

  greaterImpliesNotEqual' : {a b : A} → a < b → (b ∼ a → False)
  greaterImpliesNotEqual' {a} {b} a<b a=b = irreflexive (<WellDefined reflexive a=b a<b)

  negativeInequality : {a : A} → a < 0G → 0G < inverse a
  negativeInequality {a} a<0 = <WellDefined invRight identLeft (orderRespectsAddition a<0 (inverse a))

  negativeInequality' : {a : A} → 0G < a → inverse a < 0G
  negativeInequality' {a} 0<a = <WellDefined identLeft invRight (orderRespectsAddition 0<a (inverse a))

open import Rings.InitialRing R

fromNIncreasing : (0R < 1R) → (n : ℕ) → (fromN n) < (fromN (succ n))
fromNIncreasing 0<1 zero = <WellDefined reflexive (symmetric identRight) 0<1
fromNIncreasing 0<1 (succ n) = <WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (fromNIncreasing 0<1 n) 1R)

fromNPreservesOrder : (0R < 1R) → {a b : ℕ} → (a <N b) → (fromN a) < (fromN b)
fromNPreservesOrder 0<1 {zero} {succ zero} a<b = fromNIncreasing 0<1 0
fromNPreservesOrder 0<1 {zero} {succ (succ b)} a<b = <Transitive (fromNPreservesOrder 0<1 (succIsPositive b)) (fromNIncreasing 0<1 (succ b))
fromNPreservesOrder 0<1 {succ a} {succ b} a<b = <WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (fromNPreservesOrder 0<1 (canRemoveSuccFrom<N a<b)) 1R)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Endomorphisms on a Setoid
------------------------------------------------------------------------

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

open import Relation.Binary

module Function.Endomorphism.Setoid {c e} (S : Setoid c e) where

open import Agda.Builtin.Equality

open import Algebra
open import Algebra.Structures
open import Algebra.Morphism; open Definitions
open import Function.Equality
open import Data.Nat.Base using (ℕ; _+_); open ℕ
open import Data.Nat.Properties
open import Data.Product

import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial

private
  module E = Setoid (setoid S (Trivial.indexedSetoid S))
  open E hiding (refl)

------------------------------------------------------------------------
-- Basic type and functions

Endo : Set _
Endo = S ⟶ S

_^_ : Endo → ℕ → Endo
f ^ zero  = id
f ^ suc n = f ∘ (f ^ n)

^-cong₂ : ∀ f → (f ^_) Preserves _≡_ ⟶ _≈_
^-cong₂ f {n} refl = cong (f ^ n)

^-homo : ∀ f → Homomorphic₂ ℕ Endo _≈_ (f ^_) _+_ _∘_
^-homo f zero    n x≈y = cong (f ^ n) x≈y
^-homo f (suc m) n x≈y = cong f (^-homo f m n x≈y)

------------------------------------------------------------------------
-- Structures

∘-isMagma : IsMagma _≈_ _∘_
∘-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = λ g f x → g (f x)
  }

∘-magma : Magma _ _
∘-magma = record { isMagma = ∘-isMagma }

∘-isSemigroup : IsSemigroup _≈_ _∘_
∘-isSemigroup = record
  { isMagma = ∘-isMagma
  ; assoc   = λ h g f x≈y → cong h (cong g (cong f x≈y))
  }

∘-semigroup : Semigroup _ _
∘-semigroup = record { isSemigroup = ∘-isSemigroup }

∘-id-isMonoid : IsMonoid _≈_ _∘_ id
∘-id-isMonoid = record
  { isSemigroup = ∘-isSemigroup
  ; identity    = cong , cong
  }

∘-id-monoid : Monoid _ _
∘-id-monoid = record { isMonoid = ∘-id-isMonoid }

------------------------------------------------------------------------
-- Homomorphism

^-isSemigroupMorphism : ∀ f → IsSemigroupMorphism +-semigroup ∘-semigroup (f ^_)
^-isSemigroupMorphism f = record
  { ⟦⟧-cong = ^-cong₂ f
  ; ∙-homo  = ^-homo f
  }

^-isMonoidMorphism : ∀ f → IsMonoidMorphism +-0-monoid ∘-id-monoid (f ^_)
^-isMonoidMorphism f = record
  { sm-homo = ^-isSemigroupMorphism f
  ; ε-homo  = λ x≈y → x≈y
  }


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

open import lib.Basics
open import lib.NType2
open import lib.types.TLevel
open import lib.types.Sigma
open import lib.types.Pi

module lib.types.Groupoid where

record GroupoidStructure {i j} {El : Type i} (Arr : El → El → Type j)
  (_ : ∀ x y → has-level 0 (Arr x y)) : Type (lmax i j) where
  field
    id : ∀ {x} → Arr x x
    inv : ∀ {x y} → Arr x y → Arr y x
    comp : ∀ {x y z} → Arr x y → Arr y z → Arr x z
    unit-l : ∀ {x y} (a : Arr x y) → comp id a == a
    unit-r : ∀ {x y} (a : Arr x y) → comp a id == a
    assoc   : ∀ {x y z w} (a : Arr x y) (b : Arr y z) (c : Arr z w)
              → comp (comp a b) c == comp a (comp b c)
    inv-r    : ∀ {x y} (a : Arr x y) → (comp a (inv a)) == id
    inv-l    : ∀ {x y } (a : Arr x y) → (comp (inv a) a) == id

record Groupoid {i j} : Type (lsucc (lmax i j)) where
  constructor groupoid
  field
    El : Type i
    Arr : El → El → Type j
    Arr-level : ∀ x y → has-level 0 (Arr x y)
    groupoid-struct : GroupoidStructure Arr Arr-level

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


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

module Data.ByteString.Primitive where

open import Data.Word8.Primitive using (Word8)
open import Data.Nat using (ℕ; _<_)
open import Data.Colist using (Colist)
open import Data.List using (List; length)
open import Agda.Builtin.String using (String)
open import Agda.Builtin.Bool using (Bool)
open import Agda.Builtin.IO using (IO)
open import Data.Tuple.Base using (Pair)

open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe)

{-# FOREIGN GHC import qualified Data.ByteString.Lazy    #-}
open import Data.ByteString.Primitive.Int
open import Data.ByteString.Primitive.Lazy
open import Data.ByteString.Primitive.Strict

-- properties
module _ where
  List→Strict→List : (l : List Word8) → List←Strict (List→Strict l) ≡ l
  List→Strict→List l = trustMe

  Strict→List→Strict : (bs : ByteStringStrict) → List→Strict (List←Strict bs) ≡ bs
  Strict→List→Strict bs = trustMe

  ∣Strict∣≡∣List∣ : (bs : ByteStringStrict) → IntToℕ (lengthStrict bs) ≡ length (List←Strict bs)
  ∣Strict∣≡∣List∣ bs = trustMe

  2³¹ = 2147483648
  ∣List∣≡∣Strict∣ : (l : List Word8) → (l-small : length l < 2³¹) → IntToℕ (lengthStrict (List→Strict l)) ≡ length l
  ∣List∣≡∣Strict∣ l l-small = trustMe

postulate
  toLazy : ByteStringStrict → ByteStringLazy
  toStrict : ByteStringLazy  → ByteStringStrict
  lazy≟lazy : ByteStringLazy → ByteStringLazy → Bool
  strict≟strict : ByteStringStrict → ByteStringStrict → Bool
{-# COMPILE GHC toLazy = (Data.ByteString.Lazy.fromStrict) #-}
{-# COMPILE GHC toStrict = (Data.ByteString.Lazy.toStrict) #-}
{-# COMPILE GHC lazy≟lazy = (==) #-}
{-# COMPILE GHC strict≟strict = (==) #-}

lazy≟strict : ByteStringLazy → ByteStringStrict → Bool
lazy≟strict l s = lazy≟lazy l (toLazy s)
strict≟lazy : ByteStringStrict → ByteStringLazy → Bool
strict≟lazy s l = lazy≟lazy (toLazy s) l

postulate
  fromChunks : List ByteStringStrict → ByteStringLazy
  toChunks : ByteStringLazy → List ByteStringStrict
{-# COMPILE GHC fromChunks = (Data.ByteString.Lazy.fromChunks) #-}
{-# COMPILE GHC toChunks = (Data.ByteString.Lazy.toChunks) #-}

max_stars_repo_name: semenov-vladyslav/bytes-agda

max_issues_repo_name: semenov-vladyslav/bytes-agda

max_forks_repo_name: semenov-vladyslav/bytes-agda