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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Macro
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.AbGroup

open import Cubical.Reflection.StrictEquiv

open Iso

private
  variable
    ℓ ℓ' : Level

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

  constructor isring

  field
    +IsAbGroup : IsAbGroup 0r _+_ -_
    ·IsMonoid  : IsMonoid 1r _·_
    dist        : (x y z : R) → (x · (y + z) ≡ (x · y) + (x · z))
                              × ((x + y) · z ≡ (x · z) + (y · z))
    -- This is in the Agda stdlib, but it's redundant
    -- zero             : (x : R) → (x · 0r ≡ 0r) × (0r · x ≡ 0r)

  open IsAbGroup +IsAbGroup public
    renaming
      ( assoc       to +Assoc
      ; identity    to +Identity
      ; lid         to +Lid
      ; rid         to +Rid
      ; inverse     to +Inv
      ; invl        to +Linv
      ; invr        to +Rinv
      ; comm        to +Comm
      ; isSemigroup to +IsSemigroup
      ; isMonoid    to +IsMonoid
      ; isGroup     to +IsGroup )

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

  ·Rdist+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z)
  ·Rdist+ x y z = dist x y z .fst

  ·Ldist+ : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z)
  ·Ldist+ x y z = dist x y z .snd

record RingStr (A : Type ℓ) : Type (ℓ-suc ℓ) where

  constructor ringstr

  field
    0r      : A
    1r      : A
    _+_     : A → A → A
    _·_     : A → A → A
    -_      : A → A
    isRing  : IsRing 0r 1r _+_ _·_ -_

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

  open IsRing isRing public

Ring : Type (ℓ-suc ℓ)
Ring = TypeWithStr _ RingStr

isSetRing : (R : Ring {ℓ}) → isSet ⟨ R ⟩
isSetRing R = R .snd .RingStr.isRing .IsRing.·IsMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

makeIsRing : {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} { -_ : R → R}
             (is-setR : isSet R)
             (+-assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
             (+-rid : (x : R) → x + 0r ≡ x)
             (+-rinv : (x : R) → x + (- x) ≡ 0r)
             (+-comm : (x y : R) → x + y ≡ y + x)
             (r+-assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
             (·-rid : (x : R) → x · 1r ≡ x)
             (·-lid : (x : R) → 1r · x ≡ x)
             (·-rdist-+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
             (·-ldist-+ : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z))
           → IsRing 0r 1r _+_ _·_ -_
makeIsRing is-setR assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-lid ·-rdist-+ ·-ldist-+ =
  isring (makeIsAbGroup is-setR assoc +-rid +-rinv +-comm)
         (makeIsMonoid is-setR ·-assoc ·-rid ·-lid)
         λ x y z → ·-rdist-+ x y z , ·-ldist-+ x y z

makeRing : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R)
           (is-setR : isSet R)
           (+-assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
           (+-rid : (x : R) → x + 0r ≡ x)
           (+-rinv : (x : R) → x + (- x) ≡ 0r)
           (+-comm : (x y : R) → x + y ≡ y + x)
           (+-assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
           (·-rid : (x : R) → x · 1r ≡ x)
           (·-lid : (x : R) → 1r · x ≡ x)
           (·-rdist-+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
           (·-ldist-+ : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z))
         → Ring
makeRing 0r 1r _+_ _·_ -_ is-setR assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-lid ·-rdist-+ ·-ldist-+ =
  _ , ringstr 0r 1r _+_ _·_ -_
       (makeIsRing is-setR assoc +-rid +-rinv +-comm
                   ·-assoc ·-rid ·-lid ·-rdist-+ ·-ldist-+ )

record RingEquiv (R : Ring {ℓ}) (S : Ring {ℓ'}) (e : ⟨ R ⟩ ≃ ⟨ S ⟩) : Type (ℓ-max ℓ ℓ') where

  constructor ringequiv

  private
    module R = RingStr (snd R)
    module S = RingStr (snd S)

  field
    pres1 : equivFun e R.1r ≡ S.1r
    isHom+ : (x y : ⟨ R ⟩) → equivFun e (x R.+ y) ≡ equivFun e x S.+ equivFun e y
    isHom· : (x y : ⟨ R ⟩) → equivFun e (x R.· y) ≡ equivFun e x S.· equivFun e y

record RingHom (R S : Ring {ℓ}) : Type ℓ where

  constructor ringhom

  private
    module R = RingStr (snd R)
    module S = RingStr (snd S)

  field
    f : ⟨ R ⟩ → ⟨ S ⟩
    pres1 : f R.1r ≡ S.1r
    isHom+ : (x y : ⟨ R ⟩) → f (x R.+ y) ≡ f x S.+ f y
    isHom· : (x y : ⟨ R ⟩) → f (x R.· y) ≡ f x S.· f y

_$_ : {R S : Ring {ℓ}} → (φ : RingHom R S) → (x : ⟨ R ⟩) → ⟨ S ⟩
φ $ x = RingHom.f φ x

module RingΣTheory {ℓ} where

  RawRingStructure = λ (X : Type ℓ) → (X → X → X) × X × (X → X → X)

  RawRingEquivStr = AutoEquivStr RawRingStructure

  rawRingUnivalentStr : UnivalentStr _ RawRingEquivStr
  rawRingUnivalentStr = autoUnivalentStr RawRingStructure

  RingAxioms : (R : Type ℓ) (s : RawRingStructure R) → Type ℓ
  RingAxioms R (_+_ , 1r , _·_) =
    AbGroupΣTheory.AbGroupAxioms R _+_
    × IsMonoid 1r _·_
    × ((x y z : R) → (x · (y + z) ≡ (x · y) + (x · z)) × ((x + y) · z ≡ (x · z) + (y · z)))

  RingStructure : Type ℓ → Type ℓ
  RingStructure = AxiomsStructure RawRingStructure RingAxioms

  RingΣ : Type (ℓ-suc ℓ)
  RingΣ = TypeWithStr ℓ RingStructure

  RingEquivStr : StrEquiv RingStructure ℓ
  RingEquivStr = AxiomsEquivStr RawRingEquivStr RingAxioms

  isPropRingAxioms : (R : Type ℓ) (s : RawRingStructure R) → isProp (RingAxioms R s)
  isPropRingAxioms R (_+_ , 1r , _·_) =
    isProp× (AbGroupΣTheory.isPropAbGroupAxioms R _+_)
            (isPropΣ (isPropIsMonoid 1r _·_)
                     λ R → isPropΠ3 λ _ _ _ →
                           isProp× (IsSemigroup.is-set (R .IsMonoid.isSemigroup) _ _)
                                   (IsSemigroup.is-set (R .IsMonoid.isSemigroup) _ _))

  Ring→RingΣ : Ring → RingΣ
  Ring→RingΣ (R , ringstr 0r 1r _+_ _·_ -_ (isring +-isAbelianGroup ·-isMonoid dist)) =
    ( R
    , (_+_ , 1r , _·_)
    , AbGroupΣTheory.AbGroup→AbGroupΣ (_ , abgroupstr _ _ _ +-isAbelianGroup) .snd .snd
    , ·-isMonoid , dist
    )

  RingΣ→Ring : RingΣ → Ring
  RingΣ→Ring (_ , (y1 , y2 , y3) , z , w1 , w2) =
    _ , ringstr _ y2 y1 y3 _
      (isring (AbGroupΣTheory.AbGroupΣ→AbGroup (_ , _ , z ) .snd .AbGroupStr.isAbGroup)
              w1 w2)

  RingIsoRingΣ : Iso Ring RingΣ
  RingIsoRingΣ = iso Ring→RingΣ RingΣ→Ring (λ _ → refl) (λ _ → refl)

  ringUnivalentStr : UnivalentStr RingStructure RingEquivStr
  ringUnivalentStr = axiomsUnivalentStr _ isPropRingAxioms rawRingUnivalentStr

  RingΣPath : (R S : RingΣ) → (R ≃[ RingEquivStr ] S) ≃ (R ≡ S)
  RingΣPath = SIP ringUnivalentStr

  RingEquivΣ : (R S : Ring) → Type ℓ
  RingEquivΣ R S = Ring→RingΣ R ≃[ RingEquivStr ] Ring→RingΣ S

  RingIsoΣPath : {R S : Ring} → Iso (Σ[ e ∈ ⟨ R ⟩ ≃ ⟨ S ⟩ ] RingEquiv R S e) (RingEquivΣ R S)
  fun RingIsoΣPath (e , ringequiv h1 h2 h3) = e , h2 , h1 , h3
  inv RingIsoΣPath (e , h1 , h2 , h3)       = e , ringequiv h2 h1 h3
  rightInv RingIsoΣPath _                   = refl
  leftInv RingIsoΣPath _                    = refl

  RingPath : (R S : Ring) → (Σ[ e ∈ ⟨ R ⟩ ≃ ⟨ S ⟩ ] RingEquiv R S e) ≃ (R ≡ S)
  RingPath R S =
    Σ[ e ∈ ⟨ R ⟩ ≃ ⟨ S ⟩ ] RingEquiv R S e ≃⟨ strictIsoToEquiv RingIsoΣPath ⟩
    RingEquivΣ R S              ≃⟨ RingΣPath _ _ ⟩
    Ring→RingΣ R ≡ Ring→RingΣ S ≃⟨ isoToEquiv (invIso (congIso RingIsoRingΣ)) ⟩
    R ≡ S ■

RingPath : (R S : Ring {ℓ}) → (Σ[ e ∈ ⟨ R ⟩ ≃ ⟨ S ⟩ ] RingEquiv R S e) ≃ (R ≡ S)
RingPath = RingΣTheory.RingPath

isPropIsRing : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R)
             → isProp (IsRing 0r 1r _+_ _·_ -_)
isPropIsRing 0r 1r _+_ _·_ -_ (isring RG RM RD) (isring SG SM SD) =
  λ i → isring (isPropIsAbGroup _ _ _ RG SG i)
               (isPropIsMonoid _ _ RM SM i)
               (isPropDistr RD SD i)
  where
  isSetR : isSet _
  isSetR = RM .IsMonoid.isSemigroup .IsSemigroup.is-set

  isPropDistr : isProp ((x y z : _) → ((x · (y + z)) ≡ ((x · y) + (x · z)))
                                    × (((x + y) · z) ≡ ((x · z) + (y · z))))
  isPropDistr = isPropΠ3 λ _ _ _ → isProp× (isSetR _ _) (isSetR _ _)

-- Rings have an abelian group and a monoid

Ring→AbGroup : Ring {ℓ} → AbGroup {ℓ}
Ring→AbGroup (A , ringstr _ _ _ _ _ R) = A , abgroupstr _ _ _ (IsRing.+IsAbGroup R)

Ring→Monoid : Ring {ℓ} → Monoid {ℓ}
Ring→Monoid (A , ringstr _ _ _ _ _ R) = monoid _ _ _ (IsRing.·IsMonoid R)


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

module Categories.Functor.Cocontinuous where

open import Level
open import Data.Product using (Σ)

open import Categories.Category
open import Categories.Functor
import Categories.Category.Construction.Cocones as Coc
import Categories.Diagram.Cocone.Properties as Cocₚ
import Categories.Diagram.Colimit as Col
import Categories.Morphism as Mor

private
  variable
    o ℓ e : Level
    C D E J : Category o ℓ e

-- G preserves the colimit of F.
CoimitPreserving : (G : Functor C D) {F : Functor J C} (L : Col.Colimit F) → Set _
CoimitPreserving {C = C} {D = D} G {F} L = Σ (Col.Colimit (G ∘F F)) λ L′ → G.F₀ (Col.Colimit.coapex L) ≅ Col.Colimit.coapex L′
  where module F = Functor F
        module G = Functor G
        open Mor D

-- cocontinuous functors preserves all colimits.
Cocontinuous : ∀ (o ℓ e : Level) (G : Functor C D) → Set _
Cocontinuous {C = C} o ℓ e G = ∀ {J : Category o ℓ e} {F : Functor J C} (L : Col.Colimit F) → CoimitPreserving G L

ext: agda

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Data.Num.Unary where

open import Data.Unit
open import Data.Empty
open import Data.List
open import Data.Nat renaming (_+_ to _⊹_)

data Digit : Set where
    [1] : Digit

Unary : Set
Unary = List Digit

_⊕_ : Digit → Digit → Digit
[1] ⊕ [1] = [1]

_⊚_ : Digit → Digit → Digit
[1] ⊚ [1] = [1]

add : Digit → Unary → Unary
add [1] [] = [1] ∷ []
add [1] ([1] ∷ xs) = [1] ∷ add [1] xs

_+_ : Unary → Unary → Unary
[] + ys = ys
xs + [] = xs
(x ∷ xs) + (y ∷ ys) = x ⊕ y ∷ add (x ⊚ y) (xs + ys)

_≈_ : Unary → Unary → Set
[] ≈ [] = ⊤
[] ≈ (x ∷ ys) = ⊥
(x ∷ xs) ≈ [] = ⊥
(x ∷ xs) ≈ (y ∷ ys) = xs ≈ ys

fromℕ : ℕ → Unary
fromℕ zero = []
fromℕ (suc n) = fromℕ n

-- fromℕ zero    = []
-- fromℕ (suc n) = [1] ∷ fromℕ n

toℕ : Unary → ℕ
toℕ []       = zero
toℕ (_ ∷ xs) = suc (toℕ xs)

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Pointwise.Inductive directly.
------------------------------------------------------------------------

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

module Data.Vec.Relation.Pointwise.Inductive where

open import Data.Vec.Relation.Binary.Pointwise.Inductive public

{-# WARNING_ON_IMPORT
"Data.Vec.Relation.Pointwise.Inductive was deprecated in v1.0.
Use Data.Vec.Relation.Binary.Pointwise.Inductive instead."
#-}


text:
-- The previous error was:
-- Auto in hole `?0` raises a typing error:
--   (zero ∷ L) != L of type (List ℕ)
--   when checking that the expression x₁ has type (foo L)

open import Agda.Builtin.List
open import Agda.Builtin.Nat

data ⊥ : Set where

foo : List Nat → Set
foo []          = ⊥
foo (zero ∷ L)  = foo L
foo (suc N ∷ L) = foo (suc N ∷ L)

bar : (L : List Nat) → (foo L) → List Nat
bar [] x = []
bar (zero ∷ L) x₁ = bar L {!!}
bar (suc x ∷ L) x₁ = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Common.Nat
open import Common.Equality

postulate _↦_ : ∀ {a} {A : Set a} → A → A → Set

{-# BUILTIN REWRITE _↦_ #-}

postulate
  P : ∀ {a} {A : Set a} → A → Set

postulate rew₁ : (f : Nat → Nat → Nat) → P (λ (x y z : Nat) → f z x) ↦ P f

{-# REWRITE rew₁ #-}

f : Nat → Nat → Nat → Nat
f x _ z = x + z

test : P f ≡ P (λ x z → z + x)
test = refl

postulate rew₂ : (f : Nat → Nat) → P (λ (x y : Nat) → f y) ↦ P f

{-# REWRITE rew₂ #-}

g : Nat → Nat → Nat
g x y = y

test₂ : P g ≡ P (λ (y : Nat) → y)
test₂ = refl

h : Nat → Nat → Nat → Nat
h x y z = x

test₃ : P h ≡ P (λ (z : Nat) → z)
test₃ = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module SizedIO.Console where

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

open import NativeIO
open import SizedIO.Base

data ConsoleCommand : Set where
  putStrLn : String → ConsoleCommand
  getLine  : ConsoleCommand

ConsoleResponse : ConsoleCommand → Set
ConsoleResponse (putStrLn s) = Unit
ConsoleResponse  getLine     = String

consoleI : IOInterface
Command  consoleI  = ConsoleCommand
Response consoleI  = ConsoleResponse

IOConsole : Size → Set → Set
IOConsole i = IO consoleI i

IOConsole+ : Size → Set → Set
IOConsole+ i = IO+ consoleI i

translateIOConsoleLocal : (c : ConsoleCommand) → NativeIO (ConsoleResponse c)
translateIOConsoleLocal (putStrLn s) = nativePutStrLn s
translateIOConsoleLocal getLine      = nativeGetLine

translateIOConsole : {A : Set} → IOConsole ∞ A → NativeIO A
translateIOConsole = translateIO translateIOConsoleLocal

main : NativeIO Unit
main = nativePutStrLn "Console"

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
{-# OPTIONS --cubical-compatible #-}
module Common.Nat where

open import Agda.Builtin.Nat public
  using    ( Nat; zero; suc; _+_; _*_ )
  renaming ( _-_ to _∸_ )

pred : Nat → Nat
pred zero    = zero
pred (suc n) = n


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of permutation
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Permutation.Inductive.Properties where

open import Algebra
open import Algebra.FunctionProperties
open import Algebra.Structures
open import Data.List.Base as List
open import Data.List.Relation.Binary.Permutation.Inductive
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
open import Data.List.Relation.Binary.BagAndSetEquality
  using (bag; _∼[_]_; empty-unique; drop-cons; commutativeMonoid)
import Data.List.Properties as Lₚ
open import Data.Product using (_,_; _×_; ∃; ∃₂)
open import Function using (_∘_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as Inv using (inverse)
open import Relation.Unary using (Pred)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as ≡
  using (_≡_ ; refl ; cong; cong₂; _≢_; inspect)

open PermutationReasoning

------------------------------------------------------------------------
-- sym

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

  ↭-sym-involutive : ∀ {xs ys : List A} (p : xs ↭ ys) → ↭-sym (↭-sym p) ≡ p
  ↭-sym-involutive refl          = refl
  ↭-sym-involutive (prep x ↭)    = cong (prep x) (↭-sym-involutive ↭)
  ↭-sym-involutive (swap x y ↭)  = cong (swap x y) (↭-sym-involutive ↭)
  ↭-sym-involutive (trans ↭₁ ↭₂) =
    cong₂ trans (↭-sym-involutive ↭₁) (↭-sym-involutive ↭₂)

------------------------------------------------------------------------
-- Relationships to other predicates

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

  All-resp-↭ : ∀ {ℓ} {P : Pred A ℓ} → (All P) Respects _↭_
  All-resp-↭ refl wit                     = wit
  All-resp-↭ (prep x p) (px ∷ wit)        = px ∷ All-resp-↭ p wit
  All-resp-↭ (swap x y p) (px ∷ py ∷ wit) = py ∷ px ∷ All-resp-↭ p wit
  All-resp-↭ (trans p₁ p₂) wit            = All-resp-↭ p₂ (All-resp-↭ p₁ wit)

  Any-resp-↭ : ∀ {ℓ} {P : Pred A ℓ} → (Any P) Respects _↭_
  Any-resp-↭ refl         wit                 = wit
  Any-resp-↭ (prep x p)   (here px)           = here px
  Any-resp-↭ (prep x p)   (there wit)         = there (Any-resp-↭ p wit)
  Any-resp-↭ (swap x y p) (here px)           = there (here px)
  Any-resp-↭ (swap x y p) (there (here px))   = here px
  Any-resp-↭ (swap x y p) (there (there wit)) = there (there (Any-resp-↭ p wit))
  Any-resp-↭ (trans p p₁) wit                 = Any-resp-↭ p₁ (Any-resp-↭ p wit)

  ∈-resp-↭ : ∀ {x : A} → (x ∈_) Respects _↭_
  ∈-resp-↭ = Any-resp-↭

------------------------------------------------------------------------
-- map

module _ {a b} {A : Set a} {B : Set b} (f : A → B) where

  map⁺ : ∀ {xs ys} → xs ↭ ys → map f xs ↭ map f ys
  map⁺ refl          = refl
  map⁺ (prep x p)    = prep _ (map⁺ p)
  map⁺ (swap x y p)  = swap _ _ (map⁺ p)
  map⁺ (trans p₁ p₂) = trans (map⁺ p₁) (map⁺ p₂)

------------------------------------------------------------------------
-- _++_

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

  ++⁺ˡ : ∀ xs {ys zs : List A} → ys ↭ zs → xs ++ ys ↭ xs ++ zs
  ++⁺ˡ []       ys↭zs = ys↭zs
  ++⁺ˡ (x ∷ xs) ys↭zs = prep x (++⁺ˡ xs ys↭zs)

  ++⁺ʳ : ∀ {xs ys : List A} zs → xs ↭ ys → xs ++ zs ↭ ys ++ zs
  ++⁺ʳ zs refl          = refl
  ++⁺ʳ zs (prep x ↭)    = prep x (++⁺ʳ zs ↭)
  ++⁺ʳ zs (swap x y ↭)  = swap x y (++⁺ʳ zs ↭)
  ++⁺ʳ zs (trans ↭₁ ↭₂) = trans (++⁺ʳ zs ↭₁) (++⁺ʳ zs ↭₂)

  ++⁺ : _++_ Preserves₂ _↭_ ⟶ _↭_ ⟶ _↭_
  ++⁺ ws↭xs ys↭zs = trans (++⁺ʳ _ ws↭xs) (++⁺ˡ _ ys↭zs)

  -- Some useful lemmas

  zoom : ∀ h {t xs ys : List A} → xs ↭ ys → h ++ xs ++ t ↭ h ++ ys ++ t
  zoom h {t} = ++⁺ˡ h ∘ ++⁺ʳ t

  inject : ∀  (v : A) {ws xs ys zs} → ws ↭ ys → xs ↭ zs →
           ws ++ [ v ] ++ xs ↭ ys ++ [ v ] ++ zs
  inject v ws↭ys xs↭zs = trans (++⁺ˡ _ (prep v xs↭zs)) (++⁺ʳ _ ws↭ys)

  shift : ∀ v (xs ys : List A) → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
  shift v []       ys = refl
  shift v (x ∷ xs) ys = begin
    x ∷ (xs ++ [ v ] ++ ys) <⟨ shift v xs ys ⟩
    x ∷ v ∷ xs ++ ys        <<⟨ refl ⟩
    v ∷ x ∷ xs ++ ys        ∎

  drop-mid-≡ : ∀ {x} ws xs {ys} {zs} →
               ws ++ [ x ] ++ ys ≡ xs ++ [ x ] ++ zs →
               ws ++ ys ↭ xs ++ zs
  drop-mid-≡ []       []       eq   with cong tail eq
  drop-mid-≡ []       []       eq   | refl = refl
  drop-mid-≡ []       (x ∷ xs) refl = shift _ xs _
  drop-mid-≡ (w ∷ ws) []       refl = ↭-sym (shift _ ws _)
  drop-mid-≡ (w ∷ ws) (x ∷ xs) eq with Lₚ.∷-injective eq
  ... | refl , eq′ = prep w (drop-mid-≡ ws xs eq′)

  drop-mid : ∀ {x} ws xs {ys zs} →
             ws ++ [ x ] ++ ys ↭ xs ++ [ x ] ++ zs →
             ws ++ ys ↭ xs ++ zs
  drop-mid {x} ws xs p = drop-mid′ p ws xs refl refl
    where
    drop-mid′ : ∀ {l′ l″ : List A} → l′ ↭ l″ →
                ∀ ws xs {ys zs : List A} →
                ws ++ [ x ] ++ ys ≡ l′ →
                xs ++ [ x ] ++ zs ≡ l″ →
                ws ++ ys ↭ xs ++ zs
    drop-mid′ refl         ws           xs           refl eq   = drop-mid-≡ ws xs (≡.sym eq)
    drop-mid′ (prep x p)   []           []           refl eq   with cong tail eq
    drop-mid′ (prep x p)   []           []           refl eq   | refl = p
    drop-mid′ (prep x p)   []           (x ∷ xs)     refl refl = trans p (shift _ _ _)
    drop-mid′ (prep x p)   (w ∷ ws)     []           refl refl = trans (↭-sym (shift _ _ _)) p
    drop-mid′ (prep x p)   (w ∷ ws)     (x ∷ xs)     refl refl = prep _ (drop-mid′ p ws xs refl refl)
    drop-mid′ (swap y z p) []           []           refl refl = prep _ p
    drop-mid′ (swap y z p) []           (x ∷ [])     refl eq   with cong {B = List _}
                                                                         (λ { (x ∷ _ ∷ xs) → x ∷ xs
                                                                            ; _            → []
                                                                            })
                                                                         eq
    drop-mid′ (swap y z p) []           (x ∷ [])     refl eq   | refl = prep _ p
    drop-mid′ (swap y z p) []           (x ∷ _ ∷ xs) refl refl = prep _ (trans p (shift _ _ _))
    drop-mid′ (swap y z p) (w ∷ [])     []           refl eq   with cong tail eq
    drop-mid′ (swap y z p) (w ∷ [])     []           refl eq   | refl = prep _ p
    drop-mid′ (swap y z p) (w ∷ x ∷ ws) []           refl refl = prep _ (trans (↭-sym (shift _ _ _)) p)
    drop-mid′ (swap y y p) (y ∷ [])     (y ∷ [])     refl refl = prep _ p
    drop-mid′ (swap y z p) (y ∷ [])     (z ∷ y ∷ xs) refl refl = begin
        _ ∷ _             <⟨ p ⟩
        _ ∷ (xs ++ _ ∷ _) <⟨ shift _ _ _ ⟩
        _ ∷ _ ∷ xs ++ _   <<⟨ refl ⟩
        _ ∷ _ ∷ xs ++ _   ∎
    drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ [])     refl refl = begin
        _ ∷ _ ∷ ws ++ _   <<⟨ refl ⟩
        _ ∷ (_ ∷ ws ++ _) <⟨ ↭-sym (shift _ _ _) ⟩
        _ ∷ (ws ++ _ ∷ _) <⟨ p ⟩
        _ ∷ _             ∎
    drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ y ∷ xs) refl refl = swap y z (drop-mid′ p _ _ refl refl)
    drop-mid′ (trans p₁ p₂) ws  xs refl refl with ∈-∃++ (∈-resp-↭ p₁ (∈-insert ws))
    ... | (h , t , refl) = trans (drop-mid′ p₁ ws h refl refl) (drop-mid′ p₂ h xs refl refl)

  -- Algebraic properties

  ++-identityˡ : LeftIdentity {A = List A} _↭_ [] _++_
  ++-identityˡ xs = refl

  ++-identityʳ : RightIdentity {A = List A} _↭_ [] _++_
  ++-identityʳ xs = ↭-reflexive (Lₚ.++-identityʳ xs)

  ++-identity : Identity {A = List A} _↭_ [] _++_
  ++-identity = ++-identityˡ , ++-identityʳ

  ++-assoc : Associative {A = List A} _↭_ _++_
  ++-assoc xs ys zs = ↭-reflexive (Lₚ.++-assoc xs ys zs)

  ++-comm : Commutative _↭_ _++_
  ++-comm []       ys = ↭-sym (++-identityʳ ys)
  ++-comm (x ∷ xs) ys = begin
    x ∷ xs ++ ys         ↭⟨ prep x (++-comm xs ys) ⟩
    x ∷ ys ++ xs         ≡⟨ cong (λ v → x ∷ v ++ xs) (≡.sym (Lₚ.++-identityʳ _)) ⟩
    (x ∷ ys ++ []) ++ xs ↭⟨ ++⁺ʳ xs (↭-sym (shift x ys [])) ⟩
    (ys ++ [ x ]) ++ xs  ↭⟨ ++-assoc ys [ x ] xs ⟩
    ys ++ ([ x ] ++ xs)  ≡⟨⟩
    ys ++ (x ∷ xs)       ∎

  ++-isMagma : IsMagma _↭_ _++_
  ++-isMagma = record
    { isEquivalence = ↭-isEquivalence
    ; ∙-cong        = ++⁺
    }

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

  ++-isSemigroup : IsSemigroup _↭_ _++_
  ++-isSemigroup = record
    { isMagma = ++-isMagma
    ; assoc   = ++-assoc
    }

  ++-semigroup : Semigroup a _
  ++-semigroup = record
    { isSemigroup = ++-isSemigroup
    }

  ++-isMonoid : IsMonoid _↭_ _++_ []
  ++-isMonoid = record
    { isSemigroup = ++-isSemigroup
    ; identity    = ++-identity
    }

  ++-monoid : Monoid a _
  ++-monoid = record
    { isMonoid = ++-isMonoid
    }

  ++-isCommutativeMonoid : IsCommutativeMonoid _↭_ _++_ []
  ++-isCommutativeMonoid = record
    { isSemigroup = ++-isSemigroup
    ; identityˡ   = ++-identityˡ
    ; comm        = ++-comm
    }

  ++-commutativeMonoid : CommutativeMonoid _ _
  ++-commutativeMonoid = record
    { isCommutativeMonoid = ++-isCommutativeMonoid
    }

------------------------------------------------------------------------
-- _∷_

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

  drop-∷ : ∀ {x : A} {xs ys} → x ∷ xs ↭ x ∷ ys → xs ↭ ys
  drop-∷ = drop-mid [] []

------------------------------------------------------------------------
-- _∷ʳ_

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

  ∷↭∷ʳ : ∀ (x : A) xs → x ∷ xs ↭ xs ∷ʳ x
  ∷↭∷ʳ x xs = ↭-sym (begin
    xs ++ [ x ]   ↭⟨ shift x xs [] ⟩
    x ∷ xs ++ []  ≡⟨ Lₚ.++-identityʳ _ ⟩
    x ∷ xs        ∎)

------------------------------------------------------------------------
-- Relationships to other relations

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

  ↭⇒∼bag : _↭_ ⇒ _∼[ bag ]_
  ↭⇒∼bag xs↭ys {v} = inverse (to xs↭ys) (from xs↭ys) (from∘to xs↭ys) (to∘from xs↭ys)
    where
    to : ∀ {xs ys} → xs ↭ ys → v ∈ xs → v ∈ ys
    to xs↭ys = Any-resp-↭ {A = A} xs↭ys

    from : ∀ {xs ys} → xs ↭ ys → v ∈ ys → v ∈ xs
    from xs↭ys = Any-resp-↭ (↭-sym xs↭ys)

    from∘to : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ xs) → from p (to p q) ≡ q
    from∘to refl          v∈xs                 = refl
    from∘to (prep _ _)    (here refl)          = refl
    from∘to (prep _ p)    (there v∈xs)         = cong there (from∘to p v∈xs)
    from∘to (swap x y p)  (here refl)          = refl
    from∘to (swap x y p)  (there (here refl))  = refl
    from∘to (swap x y p)  (there (there v∈xs)) = cong (there ∘ there) (from∘to p v∈xs)
    from∘to (trans p₁ p₂) v∈xs
      rewrite from∘to p₂ (Any-resp-↭ p₁ v∈xs)
            | from∘to p₁ v∈xs                  = refl

    to∘from : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ ys) → to p (from p q) ≡ q
    to∘from p with from∘to (↭-sym p)
    ... | res rewrite ↭-sym-involutive p = res

  ∼bag⇒↭ : _∼[ bag ]_ ⇒ _↭_
  ∼bag⇒↭ {[]} eq with empty-unique (Inv.sym eq)
  ... | refl = refl
  ∼bag⇒↭ {x ∷ xs} eq with ∈-∃++ (to ⟨$⟩ (here ≡.refl))
    where open Inv.Inverse (eq {x})
  ... | zs₁ , zs₂ , p rewrite p = begin
    x ∷ xs           <⟨ ∼bag⇒↭ (drop-cons (Inv._∘_ (comm zs₁ (x ∷ zs₂)) eq)) ⟩
    x ∷ (zs₂ ++ zs₁) <⟨ ++-comm zs₂ zs₁ ⟩
    x ∷ (zs₁ ++ zs₂) ↭˘⟨ shift x zs₁ zs₂ ⟩
    zs₁ ++ x ∷ zs₂   ∎
    where open CommutativeMonoid (commutativeMonoid bag A)

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

-- Version 1.0

↭⇒~bag = ↭⇒∼bag
{-# WARNING_ON_USAGE ↭⇒~bag
"Warning: ↭⇒~bag was deprecated in v1.0.
Please use ? instead (now typed with '\\sim' rather than '~')."
#-}

~bag⇒↭ = ∼bag⇒↭
{-# WARNING_ON_USAGE ~bag⇒↭
"Warning: ~bag⇒↭ was deprecated in v1.0.
Please use ? instead (now typed with '\\sim' rather than '~')."
#-}


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

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

open import Graphs.Definition
open import Coequalizers.Definition
open import Util.Misc

module Coequalizers.PullbackStability where

module PullbackStability {i k j : ULevel} (E : Type i) (V : Type k) ⦃ gph : Graph E V ⦄
  (X : (V / E) → Type j) where

  VX = Σ V (X ∘ c[_])
  EX = Σ E (X ∘ c[_] ∘ π₀)

  instance
    gph-pb : Graph EX VX
    gph-pb = record { π₀ = λ {(e , x) → ((π₀ e) , x)} ; π₁ = λ {(e , x) → ((π₁ e) , (transport X (quot e) x))} }

  pb-equiv : (VX / EX) ≃ Σ (V / E) X
  pb-equiv = equiv f g (λ {(e , x) → f-g' e x}) g-f
    where

      f-point : VX → Σ (V / E) X
      f-point (v , x) = (c[ v ] , x)

      f : (VX / EX) → Σ (V / E) X
      f = Coeq-rec f-point
               λ {(e , x) → pair= (quot e) (transp-↓' X (quot e) x)}

      g'-path : (e : E) → (λ x → c[ (π₀ e , x) ]) == (λ x → c[ (π₁ e , x) ]) [ (λ z → X z → VX / EX) ↓ (quot e) ]
      g'-path e = ↓-app→cst-in (λ {t} {t'} q → quot (e , t) ∙ ap c[_] (pair= idp (to-transp q)))

      g'-point : (v : V) → (X c[ v ]) → (VX / EX)
      g'-point v x = c[ v , x ]

      g' : (z : V / E) → (X z) → (VX / EX)
      g' = Coeq-elim (λ z → (X z) → (VX / EX))
                     g'-point g'-path

      g : Σ (V / E) X → (VX / EX)
      g (z , x) = g' z x

      g-f : (z : VX / EX) → (g (f z) == z)
      g-f = Coeq-elim _ (λ _ → idp) λ {(e , x) → ↓-app=idf-in (lemma e x)}
        where
          lemma1 : {z z' : V / E} (p : z == z') (x : X z) → ap g (pair= p (transp-↓' X p x)) == ↓-app→cst-out (apd g' p) (transp-↓' X p x)
          lemma1 idp x = idp

          lemma2 : {z z' : V / E} (p : z == z') (x : X z) → (to-transp ((transp-↓' X p x))) == idp
          lemma2 idp x = idp

          lemma : (e : E) → (x : X c[ π₀ e ]) → idp ∙' quot (e , x) == ap (g ∘ f) (quot (e , x)) ∙ idp
          lemma e x = ! $
            ap (g ∘ f) (quot (e , x)) ∙ idp
              =⟨ ∙-unit-r _ ⟩
            ap (g ∘ f) (quot (e , x))
              =⟨ ap-∘ g f (quot (e , x)) ⟩
            ap g (ap f (quot (e , x)))
              =⟨ ap (ap g) (Coeq-rec-β= _ _ _) ⟩
            ap g (pair= (quot e) (transp-↓' X (quot e) x))
              =⟨ lemma1 (quot e) x ⟩
            ↓-app→cst-out (apd g' (quot e)) (transp-↓' X (quot e) x)
              =⟨ ap (λ w → ↓-app→cst-out w (transp-↓' X (quot e) x) ) (Coeq-β= _ _ _ _) ⟩
            ↓-app→cst-out (↓-app→cst-in λ q → quot (e , _) ∙ ap c[_] (pair= idp (to-transp q))) (transp-↓' X (quot e) x)
              =⟨ ↓-app→cst-β ((λ q → quot (e , _) ∙ ap c[_] (pair= idp (to-transp q)))) ((transp-↓' X (quot e) x)) ⟩
            (λ q → quot (e , _) ∙ ap c[_] (pair= idp (to-transp q))) (transp-↓' X (quot e) x)
              =⟨ idp ⟩
            quot (e , _) ∙ ap c[_] (pair= idp (to-transp ((transp-↓' X (quot e) x))))
              =⟨ quot (e , x) ∙ₗ ap (ap c[_]) (pair== idp (lemma2 (quot e) x)) ⟩
            quot (e , x) ∙ idp
              =⟨ ∙-unit-r _ ⟩
            quot (e , x)
              =⟨ ! (∙'-unit-l _) ⟩
            idp ∙' quot (e , x)
              =∎

      f-g' : (z : V / E) → (x : X z) → f (g' z x) == (z , x)
      f-g' = Coeq-elim (λ z → (x : X z) → f (g' z x) == (z , x) )
                       (λ v x → idp) λ e → lemma1 (quot e) (λ _ → idp) (λ _ → idp) (λ x → (lemma2 (e , x)))
           where
             fg : (z : V / E) → (x : X z) → Σ (V / E) X
             fg z x = f (g' z x)

             lemma1 : {z z' : V / E} (p : z == z') (α : (x : X z) → f (g' z x) == (z , x))
                            (β : (x' : X z') → f (g' z' x') == (z' , x')) →
                            ((x : X z) → ((α x) ∙ Σ-transp X p x) == (↓-app→cst-out (apd fg p) (transp-↓' _ p x) ∙ (β (transport X p x)))) →
                            α == β [ (λ z'' → (x : X z'') → f (g' z'' x) == (z'' , x)) ↓ p ]

             lemma1 idp α β q = λ= (λ x → ! (∙-unit-r _) ∙ q x)

             expandapd : {z z' : V / E} (p : z == z') {x : X z} {x' : X z'} (q : x == x' [ X ↓ p ]) → ↓-app→cst-out (apd fg p) q == ap f (↓-app→cst-out (apd g' p) q)
             expandapd idp idp = idp

             lemma2 : (ex : EX) →
                          (idp ∙ Σ-transp X (quot (fst ex)) (snd ex)) == (↓-app→cst-out (apd fg (quot (fst ex))) (transp-↓' _ (quot (fst ex)) (snd ex)) ∙ idp)
             lemma2 ex@(e , x) = ! $
               ↓-app→cst-out (apd fg (quot e)) (transp-↓' _ (quot e) x) ∙ idp
                 =⟨ ∙-unit-r _ ⟩
               ↓-app→cst-out (apd fg (quot e)) (transp-↓' _ (quot e) x)
                 =⟨ expandapd (quot e) ((transp-↓' _ (quot e) x)) ⟩
               ap f (↓-app→cst-out (apd g' (quot e)) ((transp-↓' _ (quot e) x)))
                 =⟨ ap (λ w → ap f (↓-app→cst-out w (((transp-↓' _ (quot e) x))))) (Coeq-β= ((λ z → (X z) → (VX / EX))) (λ v x → c[ v , x ]) g'-path e) ⟩
               ap f (↓-app→cst-out (g'-path e) (transp-↓' _ (quot e) x))
                 =⟨ ap (ap f) (↓-app→cst-β ((λ {t} {t'} q → quot (e , t) ∙ ap c[_] (pair= idp (to-transp q)))) ((transp-↓' _ (quot e) x))) ⟩
               ap f (quot ex ∙ ap c[_] (pair= idp (to-transp (transp-↓' X (quot e) x))))
                 =⟨ ap-∙ f (quot ex) (ap c[_] (pair= idp (to-transp (transp-↓' X (quot e) x)))) ⟩
               ap f (quot ex) ∙ ap f (ap c[_] (pair= idp (to-transp (transp-↓' X (quot e) x))))
                 =⟨ ap f (quot ex) ∙ₗ ∘-ap f c[_] _ ⟩
               ap f (quot ex) ∙ ap (f ∘ c[_]) (pair= idp (to-transp (transp-↓' X (quot e) x)))
                 =⟨ idp ⟩
               ap f (quot ex) ∙ ap f-point (pair= idp (to-transp (transp-↓' X (quot e) x)))
                 =⟨ Coeq-rec-β= _ _ _ ∙ᵣ ap f-point (pair= idp (to-transp (transp-↓' X (quot e) x))) ⟩
               pair= (quot e) (transp-↓' X (quot e) x) ∙ ap f-point (pair= idp (to-transp (transp-↓' X (quot e) x)))
                 =⟨ ap (λ w → pair= (quot e) (transp-↓' X (quot e) x) ∙ ap f-point (pair= idp w)) (lemma2a (quot e) x) ⟩
               pair= (quot e) (transp-↓' X (quot e) x) ∙ ap f-point (pair= idp idp)
                 =⟨ ∙-unit-r _ ⟩
               pair= (quot e) (transp-↓' X (quot e) x)
                 =⟨ idp ⟩
               Σ-transp X (quot e) x
                 =⟨ idp ⟩
               idp ∙ Σ-transp X (quot e) x
                 =∎
               where
                 lemma2a : {z z' : V / E} (p : z == z') (x : X z) → (to-transp (transp-↓' X p x)) == idp
                 lemma2a idp x = idp

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


text:
module WrongHidingInLambda where

f : (A : Set) -> A -> A
f = \{A} x -> x


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Universe levels
------------------------------------------------------------------------

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

module Level where

-- Levels.

open import Agda.Primitive as Prim public
  using    (Level; _⊔_; Setω)
  renaming (lzero to zero; lsuc to suc)

-- Lifting.

record Lift {a} ℓ (A : Set a) : Set (a ⊔ ℓ) where
  constructor lift
  field lower : A

open Lift public

-- Synonyms

0ℓ : Level
0ℓ = zero

levelOfType : ∀ {a} → Set a → Level
levelOfType {a} _ = a

levelOfTerm : ∀ {a} {A : Set a} → A → Level
levelOfTerm {a} _ = a


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

open import Categories.Category

module Categories.Category.Construction.Properties.Presheaves.Complete {o ℓ e} (C : Category o ℓ e) where

open import Categories.Category.Complete
open import Categories.Category.Complete.Finitely
open import Categories.Category.Complete.Properties
open import Categories.Category.Cocomplete
open import Categories.Category.Cocomplete.Finitely
open import Categories.Category.Cocomplete.Properties
open import Categories.Category.Construction.Presheaves
open import Categories.Category.Instance.Setoids
open import Categories.Category.Instance.Properties.Setoids

private
  module C = Category C

Presheaves-Complete : ∀ o′ ℓ′ e′ ℓ″ e″ → Complete o′ ℓ′ e′ (Presheaves C)
Presheaves-Complete o′ ℓ′ e′ ℓ″ e″ = Functors-Complete C.op (Setoids-Complete o′ ℓ′ e′ ℓ″ e″)

Presheaves-FinitelyComplete : ∀ o′ ℓ′ e′ ℓ″ e″ → FinitelyComplete (Presheaves C)
Presheaves-FinitelyComplete o′ ℓ′ e′ ℓ″ e″ = Complete⇒FinitelyComplete (Presheaves C) (Presheaves-Complete o′ ℓ′ e′ ℓ″ e″)

Presheaves-Cocomplete : ∀ o′ ℓ′ e′ ℓ″ e″ → Cocomplete o′ ℓ′ e′ (Presheaves C)
Presheaves-Cocomplete o′ ℓ′ e′ ℓ″ e″ = Functors-Cocomplete C.op (Setoids-Cocomplete o′ ℓ′ e′ ℓ″ e″)

Presheaves-FinitelyCocomplete : ∀ o′ ℓ′ e′ ℓ″ e″ → FinitelyCocomplete (Presheaves C)
Presheaves-FinitelyCocomplete o′ ℓ′ e′ ℓ″ e″ = Cocomplete⇒FinitelyCocomplete (Presheaves C) (Presheaves-Cocomplete o′ ℓ′ e′ ℓ″ e″)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------
-- The parser type
------------------------------------------------------------------------

module TotalParserCombinators.Parser where

open import Algebra
open import Category.Monad
open import Codata.Musical.Notation
open import Data.List
open import Data.Maybe using (Maybe; nothing; just)
open import Data.List.Categorical as ListMonad
  using () renaming (module MonadProperties to ListMonadProp)
open import Data.List.Relation.Binary.BagAndSetEquality
open import Data.Product using (proj₂)
open import Function
open import Level
open import Relation.Binary.PropositionalEquality

open RawMonadPlus {f = zero} ListMonad.monadPlus
  using ()
  renaming ( return to return′
           ; ∅      to fail′
           ; _∣_    to _∣′_
           ; _⊛_    to _⊛′_
           ; _>>=_  to _>>=′_
           )

------------------------------------------------------------------------
-- Helper functions

-- Flattening for potential lists.

flatten : {A : Set} → Maybe (List A) → List A
flatten nothing   = []
flatten (just xs) = xs

-- fs ⊛flatten mxs is a variant of fs ⊛′ flatten mxs, with the
-- property that fs ⊛flatten nothing evaluates to [].

_⊛flatten_ : {A B : Set} → List (A → B) → Maybe (List A) → List B
fs ⊛flatten nothing = []
fs ⊛flatten just xs = fs ⊛′ xs

-- Applies the function to the value, returning the empty list if
-- there is no function.

apply : {A B : Set} → Maybe (A → List B) → A → List B
apply nothing  x = []
apply (just f) x = f x

-- bind mxs mf is a variant of flatten mxs >>=′ apply mf, with the
-- property that bind mxs nothing evaluates to [].

bind :  {A B : Set} → Maybe (List A) → Maybe (A → List B) → List B
bind mxs nothing  = []
bind mxs (just f) = flatten mxs >>=′ f

-- Verification of some claims made above.

module Claims where

  ⊛flatten-⊛-flatten : ∀ {A B : Set} (fs : List (A → B)) mxs →
                       fs ⊛flatten mxs ≡ (fs ⊛′ flatten mxs)
  ⊛flatten-⊛-flatten fs nothing   = sym $ ListMonadProp.right-zero fs
  ⊛flatten-⊛-flatten fs (just xs) = refl

  ⊛flatten-nothing : {A B : Set} (fs : List (A → B)) →
                     fs ⊛flatten nothing ≡ []
  ⊛flatten-nothing fs = refl

  bind-flatten->>=-apply : ∀ {A B : Set} mxs (mf : Maybe (A → List B)) →
                           bind mxs mf ≡ (flatten mxs >>=′ apply mf)
  bind-flatten->>=-apply mxs (just f) = refl
  bind-flatten->>=-apply mxs nothing  =
    sym $ ListMonadProp.right-zero (flatten mxs)

  bind-nothing : {A B : Set} (mxs : Maybe (List A)) →
                 bind mxs nothing ≡ [] {A = B}
  bind-nothing mxs = refl

------------------------------------------------------------------------
-- Parsers

infixl 50 _⊛_ _<$>_ _⊛flatten_
infixl 10 _>>=_
infixl  5 _∣_

-- The list index is the "initial bag"; it contains the results which
-- can be emitted without consuming any input. For
--   p : Parser Tok R xs
-- we have
--   x ∈ xs  iff  x ∈ p · []
-- (see TotalParserCombinators.InitialBag).

mutual

  data Parser (Tok : Set) : (R : Set) → List R → Set₁ where
    return   : ∀ {R} (x : R) → Parser Tok R (return′ x)
    fail     : ∀ {R} → Parser Tok R fail′
    token    : Parser Tok Tok fail′
    _∣_      : ∀ {R xs₁ xs₂}
               (p₁ : Parser Tok R  xs₁       )
               (p₂ : Parser Tok R         xs₂) →
                     Parser Tok R (xs₁ ∣′ xs₂)
    _<$>_    : ∀ {R₁ R₂ xs}
               (f : R₁ → R₂)
               (p : Parser Tok R₁        xs) →
                    Parser Tok R₂ (map f xs)
    _⊛_      : ∀ {R₁ R₂ fs xs}
               (p₁ : ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs)            )
               (p₂ : ∞⟨ fs ⟩Parser Tok  R₁                   (flatten xs)) →
                            Parser Tok       R₂  (flatten fs ⊛flatten xs)
    _>>=_    : ∀ {R₁ R₂ xs} {f : Maybe (R₁ → List R₂)}
               (p₁ :            ∞⟨ f  ⟩Parser Tok R₁ (flatten xs))
               (p₂ : (x : R₁) → ∞⟨ xs ⟩Parser Tok R₂ (apply f x)) →
                                       Parser Tok R₂ (bind xs f)
    nonempty : ∀ {R xs} (p : Parser Tok R xs) → Parser Tok R []
    cast     : ∀ {R xs₁ xs₂} (xs₁≈xs₂ : xs₁ ∼[ bag ] xs₂)
               (p : Parser Tok R xs₁) → Parser Tok R xs₂

  ∞⟨_⟩Parser : {A : Set} → Maybe A → Set → (R : Set) → List R → Set₁
  ∞⟨ nothing ⟩Parser Tok R₁ xs = ∞ (Parser Tok R₁ xs)
  ∞⟨ just _  ⟩Parser Tok R₁ xs =    Parser Tok R₁ xs

-- Note that, with the definition above, a sequenced parser is
-- /allowed/ to be delayed if the "other" parser is not nullable, but
-- it does not have to be.

-- Note also that it would be safe to make the first argument of _>>=_
-- coinductive if apply f x ≡_[] for all x in xs. I suspect that this
-- criterion would be awkward to work with, though. Instead I only
-- allow the argument to be coinductive if f ≡ nothing.

-- Finally note that some of the combinators above are not included in
-- the paper "Total Parser Combinators".

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

private

  -- Note that these parsers can be both left and right recursive:

  leftRight : ∀ {R Tok} → Parser Tok R _
  leftRight {R} = ♯ (const <$> leftRight) ⊛ ♯ leftRight {R}

  leftRight′ : ∀ {R Tok} → Parser Tok R _
  leftRight′ {R} = ♯ leftRight′ {R} >>= λ _ → ♯ leftRight′

  -- More examples, included to ensure that all implicit arguments are
  -- inferred automatically.

  p : {Tok R : Set} → Parser Tok R _
  p = token >>= λ _ → ♯ p

  p′ : {Tok : Set} → Parser Tok Tok _
  p′ = ♯ p′ >>= λ _ → token

------------------------------------------------------------------------
-- Helper functions

-- Returns the initial bag.

initial-bag : ∀ {Tok R xs} → Parser Tok R xs → List R
initial-bag {xs = xs} _ = xs

-- Forces if necessary.

♭? : ∀ {Tok R₁ R₂} {m : Maybe R₂} {xs} →
     ∞⟨ m ⟩Parser Tok R₁ xs → Parser Tok R₁ xs
♭? {m = nothing} = ♭
♭? {m = just _}  = id

-- Is the argument parser forced? If the result is just something,
-- then it is.

forced? : ∀ {Tok A R xs} {m : Maybe A} →
          ∞⟨ m ⟩Parser Tok R xs → Maybe A
forced? {m = m} _ = m

forced?′ : {Tok R₁ R₂ A : Set} {m : Maybe A} {f : R₁ → List R₂} →
           ((x : R₁) → ∞⟨ m ⟩Parser Tok R₂ (f x)) → Maybe A
forced?′ {m = m} _ = m

-- Short synonyms for just and nothing. ◌ stands for "delayed" (think
-- "not here") and ○ for "not delayed".

◌ : {R : Set} → Maybe R
◌ = nothing

○ : {R : Set} {x : R} → Maybe R
○ {x = x} = just x

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module io where

open import bool
open import char
open import list
open import string
open import unit

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

postulate
  IO : Set → Set

{-# COMPILED_TYPE IO IO #-}
{-# BUILTIN IO IO #-}

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infixl 1 _>>=_
infixl 1 _>>_

----------------------------------------------------------------------
-- postulated operations
----------------------------------------------------------------------

postulate
  return : ∀ {A : Set} → A → IO A
  _>>=_  : ∀ {A B : Set} → IO A → (A → IO B) → IO B

{-# COMPILED return (\ _ -> return )   #-}
{-# COMPILED _>>=_  (\ _ _ -> (>>=)) #-}

postulate
  putStr : string -> IO ⊤

  -- Reads a file, which is assumed to be finite.
  readFiniteFile : string → IO string

  writeFile : string → string → IO ⊤

private
  data simple-list (A : Set) : Set where
    nil : simple-list A
    cons : A → simple-list A → simple-list A

  simple-list-to-𝕃 : ∀ {A : Set} → simple-list A → 𝕃 A
  simple-list-to-𝕃 nil = []
  simple-list-to-𝕃 (cons x xs) = x :: (simple-list-to-𝕃 xs)

{-# COMPILED_DATA simple-list ([]) [] (:) #-}

private
  postulate
    privGetArgs : IO (simple-list string)
    privDoesFileExist : string → IO 𝔹
    privTakeDirectory : string → string
    privTakeFileName : string → string
    privCombineFileNames : string → string → string

{-# COMPILED putStr         putStr                #-}
{-# COMPILED readFiniteFile readFile #-}
{-# COMPILED writeFile      writeFile             #-}
{-# IMPORT System.Environment #-}
{-# COMPILED privGetArgs System.Environment.getArgs #-}
{-# IMPORT System.Directory #-}
{-# COMPILED privDoesFileExist System.Directory.doesFileExist #-}
{-# IMPORT System.FilePath #-}
{-# COMPILED privTakeDirectory System.FilePath.takeDirectory #-}
{-# COMPILED privTakeFileName System.FilePath.takeFileName #-}
{-# COMPILED privCombineFileNames System.FilePath.combine #-}

getArgs : IO (𝕃 string)
getArgs = privGetArgs >>= (λ args → return (simple-list-to-𝕃 args))

doesFileExist : string → IO 𝔹
doesFileExist = privDoesFileExist

takeDirectory : string → string
takeDirectory = privTakeDirectory

takeFileName : string → string
takeFileName = privTakeFileName

combineFileNames : string → string → string
combineFileNames = privCombineFileNames

----------------------------------------------------------------------
-- defined operations
----------------------------------------------------------------------

_>>_ : ∀ {A B : Set} → IO A → IO B → IO B
x >> y = x >>= (λ q -> y)

base-filenameh : 𝕃 char → 𝕃 char
base-filenameh [] = []
base-filenameh ('.' :: cs) = cs
base-filenameh (_ :: cs) = base-filenameh cs

-- return the part of the string up to the last (rightmost) period ('.'); so for "foo.txt" return "foo"
base-filename : string → string
base-filename s = 𝕃char-to-string (reverse (base-filenameh (reverse (string-to-𝕃char s))))

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
import Relation.Binary.EqReasoning as EqReasoning
open import SemiNearRingRecords
module OrderLemmas (snro : SemiNearRing) where

open SemiNearRing snro -- public
open import CommAssocLemmas s _≃s_ _+s_ zers isCommMon
     using (assoc; comm)
     renaming (SA to Ss)

open EqReasoning Ss

monoPlusLeft : ∀ {a} {b} {c} →  a ≤s b  →
                        (a +s c)  ≤s  (b +s c)
monoPlusLeft {a} {b} {c} a≤b =
  begin
    (a +s c)  +s  (b +s c)
  ≈⟨ assoc _ _ _ ⟩
    a +s (c  +s  (b +s c))
  ≈⟨ refls <+> comm _ _ ⟩
    a +s ((b +s c) +s c)
  ≈⟨ refls <+> assoc _ _ _ ⟩
    a +s (b +s (c +s c))
  ≈⟨ sym (assoc _ _ _) ⟩
    (a +s b) +s (c +s c)
  ≈⟨ a≤b <+> idem _ ⟩
    b +s c
  ∎

monoTimesLeft : ∀ {a} {b} {c} →  a ≤s b →
                         (a *s c)  ≤s  (b *s c)
monoTimesLeft {a} {b} {c} a≤b =
  begin
    (a *s c) +s (b *s c)
  ≈⟨ sym (distr _ _ _) ⟩
    (a +s b) *s c
  ≈⟨  a≤b    <*> refls  ⟩ -- a≤=b means a+b==b
          b  *s c
  ∎
infixl 6 _[+]_
infixl 7 _[*]_

_[+]_ : ∀ {a} {a'} {b} {b'} ->  a ≤s a' -> b ≤s b' ->
                                (a +s b) ≤s (a' +s b')
_[+]_ {a} {a'} {b} {b'} pa pb =
  begin
    (a +s b) +s (a' +s b')
  ≈⟨ assoc _ _ _ ⟩
    a +s (b +s (a' +s b'))
  ≈⟨  refls <+> comm _ _  ⟩
    a +s ((a' +s b') +s b)
  ≈⟨  refls <+> assoc _ _ _  ⟩
    a +s (a' +s (b' +s b))
  ≈⟨  sym (assoc _ _ _)  ⟩
    (a +s a') +s (b' +s b)
  ≈⟨  pa <+> comm _ _  ⟩
    a' +s (b +s b')
  ≈⟨  refls <+> pb  ⟩
    a' +s b'
  ∎

_[*]_ : ∀ {a} {a'} {b} {b'} ->  a ≤s a' -> b ≤s b' ->
                                (a *s b) ≤s (a' *s b')
_[*]_ {a} {a'} {b} {b'} pa pb =
  begin
    (a *s b) +s (a' *s b')
  ≈⟨  refls <+> (sym pa <*> refls)  ⟩
    a *s b +s (a +s a') *s b'
  ≈⟨  refls <+> distr _ _ _  ⟩
    a *s b +s (a *s b' +s a' *s b')
  ≈⟨  sym (assoc _ _ _)  ⟩
    (a *s b +s a *s b') +s a' *s b'
  ≈⟨  sym (distl _ _ _) <+> (refls <*> sym pb)  ⟩
    a *s (b +s b') +s a' *s (b +s b')
  ≈⟨  sym (distr _ _ _)  ⟩
    (a +s a') *s (b +s b')
  ≈⟨  pa <*> pb  ⟩
    a' *s b'
  ∎

≤s-trans : ∀ {a b c} →  a ≤s b  →  b ≤s c  →  a ≤s c
≤s-trans {a} {b} {c} p q =
  begin
    a +s c
  ≈⟨  refls <+> sym q ⟩
    a +s (b +s c)
  ≈⟨  sym (assoc _ _ _) ⟩
    (a +s b) +s c
  ≈⟨  p <+> refls ⟩
    b +s c
  ≈⟨ q ⟩
    c
  ∎

≃sTo≤s : ∀ {a b} →  a ≃s b  →  a ≤s b
≃sTo≤s {a} {b} a=b =
  begin
    a +s b
  ≈⟨ a=b <+> refls ⟩
    b +s b
  ≈⟨ idem _ ⟩
    b
  ∎

max_stars_repo_name: DSLsofMath/ValiantAgda

max_issues_repo_name: DSLsofMath/ValiantAgda

max_forks_repo_name: DSLsofMath/ValiantAgda


text:
-- The ATP roles must to have at least an argument

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

module ATPMissingArgument where

{-# ATP axiom #-}

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Inductive pointwise lifting of relations to vectors
------------------------------------------------------------------------

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

module Data.Vec.Relation.Binary.Pointwise.Inductive where

open import Data.Fin.Base using (Fin; zero; suc)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Product using (_×_; _,_; uncurry; <_,_>)
open import Data.Vec.Base as Vec hiding ([_]; head; tail; map; lookup; uncons)
open import Data.Vec.Relation.Unary.All using (All; []; _∷_)
open import Level using (Level; _⊔_)
open import Function.Base using (_∘_)
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Decidable using (map′)
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Unary using (Pred)

private
  variable
    a b c d ℓ ℓ₁ ℓ₂ : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d

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

infixr 5 _∷_

data Pointwise {a b ℓ} {A : Set a} {B : Set b} (_∼_ : REL A B ℓ) :
               ∀ {m n} (xs : Vec A m) (ys : Vec B n) → Set (a ⊔ b ⊔ ℓ)
               where
  []  : Pointwise _∼_ [] []
  _∷_ : ∀ {m n x y} {xs : Vec A m} {ys : Vec B n}
        (x∼y : x ∼ y) (xs∼ys : Pointwise _∼_ xs ys) →
        Pointwise _∼_ (x ∷ xs) (y ∷ ys)

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

length-equal : ∀ {m n} {_∼_ : REL A B ℓ} {xs : Vec A m} {ys : Vec B n} →
               Pointwise _∼_ xs ys → m ≡ n
length-equal []          = P.refl
length-equal (_ ∷ xs∼ys) = P.cong suc (length-equal xs∼ys)

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

module _ {_∼_ : REL A B ℓ} where

  head : ∀ {m n x y} {xs : Vec A m} {ys : Vec B n} →
         Pointwise _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y
  head (x∼y ∷ xs∼ys) = x∼y

  tail : ∀ {m n x y} {xs : Vec A m} {ys : Vec B n} →
         Pointwise _∼_ (x ∷ xs) (y ∷ ys) → Pointwise _∼_ xs ys
  tail (x∼y ∷ xs∼ys) = xs∼ys

  uncons : ∀ {m n x y} {xs : Vec A m} {ys : Vec B n} →
           Pointwise _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y × Pointwise _∼_ xs ys
  uncons = < head , tail >

  lookup : ∀ {n} {xs : Vec A n} {ys : Vec B n} → Pointwise _∼_ xs ys →
           ∀ i → (Vec.lookup xs i) ∼ (Vec.lookup ys i)
  lookup (x∼y ∷ _)     zero    = x∼y
  lookup (_   ∷ xs∼ys) (suc i) = lookup xs∼ys i

  map : ∀ {ℓ₂} {_≈_ : REL A B ℓ₂} →
        _≈_ ⇒ _∼_ → ∀ {m n} → Pointwise _≈_ ⇒ Pointwise _∼_ {m} {n}
  map ∼₁⇒∼₂ []             = []
  map ∼₁⇒∼₂ (x∼y ∷ xs∼ys) = ∼₁⇒∼₂ x∼y ∷ map ∼₁⇒∼₂ xs∼ys

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

refl : ∀ {_∼_ : Rel A ℓ} {n} →
       Reflexive _∼_ → Reflexive (Pointwise _∼_ {n})
refl ∼-refl {[]}      = []
refl ∼-refl {x ∷ xs} = ∼-refl ∷ refl ∼-refl

sym : ∀ {P : REL A B ℓ} {Q : REL B A ℓ} {m n} →
      Sym P Q → Sym (Pointwise P) (Pointwise Q {m} {n})
sym sm []             = []
sym sm (x∼y ∷ xs∼ys) = sm x∼y ∷ sym sm xs∼ys

trans : ∀ {P : REL A B ℓ} {Q : REL B C ℓ} {R : REL A C ℓ} {m n o} →
        Trans P Q R →
        Trans (Pointwise P {m}) (Pointwise Q {n} {o}) (Pointwise R)
trans trns []             []             = []
trans trns (x∼y ∷ xs∼ys) (y∼z ∷ ys∼zs) =
  trns x∼y y∼z ∷ trans trns xs∼ys ys∼zs

decidable : ∀ {_∼_ : REL A B ℓ} →
            Decidable _∼_ → ∀ {m n} → Decidable (Pointwise _∼_ {m} {n})
decidable dec []       []       = yes []
decidable dec []       (y ∷ ys) = no λ()
decidable dec (x ∷ xs) []       = no λ()
decidable dec (x ∷ xs) (y ∷ ys) =
  map′ (uncurry _∷_) uncons (dec x y ×-dec decidable dec xs ys)

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

module _ {_∼_ : Rel A ℓ} where

  isEquivalence : IsEquivalence _∼_ → ∀ n →
                  IsEquivalence (Pointwise _∼_ {n})
  isEquivalence equiv n = record
    { refl  = refl  Eq.refl
    ; sym   = sym   Eq.sym
    ; trans = trans Eq.trans
    } where module Eq = IsEquivalence equiv

  isDecEquivalence : IsDecEquivalence _∼_ → ∀ n →
                     IsDecEquivalence (Pointwise _∼_ {n})
  isDecEquivalence decEquiv n = record
    { isEquivalence = isEquivalence Eq.isEquivalence n
    ; _≟_           = decidable Eq._≟_
    } where module Eq = IsDecEquivalence decEquiv

------------------------------------------------------------------------
-- Bundles

setoid : Setoid a ℓ → ℕ → Setoid a (a ⊔ ℓ)
setoid S n = record
   { isEquivalence = isEquivalence Eq.isEquivalence n
   } where module Eq = Setoid S

decSetoid : DecSetoid a ℓ → ℕ → DecSetoid a (a ⊔ ℓ)
decSetoid S n = record
   { isDecEquivalence = isDecEquivalence Eq.isDecEquivalence n
   } where module Eq = DecSetoid S

------------------------------------------------------------------------
-- map

module _ {_∼₁_ : REL A B ℓ₁} {_∼₂_ : REL C D ℓ₂}
         {f : A → C} {g : B → D}
         where

  map⁺ : (∀ {x y} → x ∼₁ y → f x ∼₂ g y) →
         ∀ {m n xs ys} → Pointwise _∼₁_ {m} {n} xs ys →
         Pointwise _∼₂_ (Vec.map f xs) (Vec.map g ys)
  map⁺ ∼₁⇒∼₂ []             = []
  map⁺ ∼₁⇒∼₂ (x∼y ∷ xs∼ys) = ∼₁⇒∼₂ x∼y ∷ map⁺ ∼₁⇒∼₂ xs∼ys

------------------------------------------------------------------------
-- _++_

module _ {_∼_ : REL A B ℓ} where

  ++⁺ : ∀ {m n p q}
        {ws : Vec A m} {xs : Vec B p} {ys : Vec A n} {zs : Vec B q} →
        Pointwise _∼_ ws xs → Pointwise _∼_ ys zs →
        Pointwise _∼_ (ws ++ ys) (xs ++ zs)
  ++⁺ []            ys∼zs = ys∼zs
  ++⁺ (w∼x ∷ ws∼xs) ys∼zs = w∼x ∷ (++⁺ ws∼xs ys∼zs)

  ++ˡ⁻ : ∀ {m n}
         (ws : Vec A m) (xs : Vec B m) {ys : Vec A n} {zs : Vec B n} →
         Pointwise _∼_ (ws ++ ys) (xs ++ zs) → Pointwise _∼_ ws xs
  ++ˡ⁻ []       []        _                    = []
  ++ˡ⁻ (w ∷ ws) (x ∷ xs) (w∼x ∷ ps) = w∼x ∷ ++ˡ⁻ ws xs ps

  ++ʳ⁻ : ∀ {m n}
         (ws : Vec A m) (xs : Vec B m) {ys : Vec A n} {zs : Vec B n} →
         Pointwise _∼_ (ws ++ ys) (xs ++ zs) → Pointwise _∼_ ys zs
  ++ʳ⁻ [] [] ys∼zs = ys∼zs
  ++ʳ⁻ (w ∷ ws) (x ∷ xs) (_ ∷ ps) = ++ʳ⁻ ws xs ps

  ++⁻ : ∀ {m n}
        (ws : Vec A m) (xs : Vec B m) {ys : Vec A n} {zs : Vec B n} →
        Pointwise _∼_ (ws ++ ys) (xs ++ zs) →
        Pointwise _∼_ ws xs × Pointwise _∼_ ys zs
  ++⁻ ws xs ps = ++ˡ⁻ ws xs ps , ++ʳ⁻ ws xs ps

------------------------------------------------------------------------
-- concat

module _ {_∼_ : REL A B ℓ} where

  concat⁺ : ∀ {m n p q}
            {xss : Vec (Vec A m) n} {yss : Vec (Vec B p) q} →
            Pointwise (Pointwise _∼_) xss yss →
            Pointwise _∼_ (concat xss) (concat yss)
  concat⁺ []           = []
  concat⁺ (xs∼ys ∷ ps) = ++⁺ xs∼ys (concat⁺ ps)

  concat⁻ : ∀ {m n} (xss : Vec (Vec A m) n) (yss : Vec (Vec B m) n) →
            Pointwise _∼_ (concat xss) (concat yss) →
            Pointwise (Pointwise _∼_) xss yss
  concat⁻ []         []         [] = []
  concat⁻ (xs ∷ xss) (ys ∷ yss) ps =
    ++ˡ⁻ xs ys ps ∷ concat⁻ xss yss (++ʳ⁻ xs ys ps)

------------------------------------------------------------------------
-- tabulate

module _ {_∼_ : REL A B ℓ} where

  tabulate⁺ : ∀ {n} {f : Fin n → A} {g : Fin n → B} →
              (∀ i → f i ∼ g i) →
              Pointwise _∼_ (tabulate f) (tabulate g)
  tabulate⁺ {zero}  f∼g = []
  tabulate⁺ {suc n} f∼g = f∼g zero ∷ tabulate⁺ (f∼g ∘ suc)

  tabulate⁻ : ∀ {n} {f : Fin n → A} {g : Fin n → B} →
              Pointwise _∼_ (tabulate f) (tabulate g) →
              (∀ i → f i ∼ g i)
  tabulate⁻ (f₀∼g₀ ∷ _)   zero    = f₀∼g₀
  tabulate⁻ (_     ∷ f∼g) (suc i) = tabulate⁻ f∼g i

------------------------------------------------------------------------
-- Degenerate pointwise relations

module _ {P : Pred A ℓ} where

  Pointwiseˡ⇒All : ∀ {m n} {xs : Vec A m} {ys : Vec B n} →
                   Pointwise (λ x y → P x) xs ys → All P xs
  Pointwiseˡ⇒All []       = []
  Pointwiseˡ⇒All (p ∷ ps) = p ∷ Pointwiseˡ⇒All ps

  Pointwiseʳ⇒All : ∀ {n} {xs : Vec B n} {ys : Vec A n} →
                   Pointwise (λ x y → P y) xs ys → All P ys
  Pointwiseʳ⇒All []       = []
  Pointwiseʳ⇒All (p ∷ ps) = p ∷ Pointwiseʳ⇒All ps

  All⇒Pointwiseˡ : ∀ {n} {xs : Vec A n} {ys : Vec B n} →
                   All P xs → Pointwise (λ x y → P x) xs ys
  All⇒Pointwiseˡ {ys = []}    []       = []
  All⇒Pointwiseˡ {ys = _ ∷ _} (p ∷ ps) = p ∷ All⇒Pointwiseˡ ps

  All⇒Pointwiseʳ : ∀ {n} {xs : Vec B n} {ys : Vec A n} →
                   All P ys → Pointwise (λ x y → P y) xs ys
  All⇒Pointwiseʳ {xs = []}    []       = []
  All⇒Pointwiseʳ {xs = _ ∷ _} (p ∷ ps) = p ∷ All⇒Pointwiseʳ ps

------------------------------------------------------------------------
-- Pointwise _≡_ is equivalent to _≡_

Pointwise-≡⇒≡ : ∀ {n} {xs ys : Vec A n} → Pointwise _≡_ xs ys → xs ≡ ys
Pointwise-≡⇒≡ []               = P.refl
Pointwise-≡⇒≡ (P.refl ∷ xs∼ys) = P.cong (_ ∷_) (Pointwise-≡⇒≡ xs∼ys)

≡⇒Pointwise-≡ : ∀ {n} {xs ys : Vec A n} → xs ≡ ys → Pointwise _≡_ xs ys
≡⇒Pointwise-≡ P.refl = refl P.refl

Pointwise-≡↔≡ : ∀ {n} {xs ys : Vec A n} → Pointwise _≡_ xs ys ⇔ xs ≡ ys
Pointwise-≡↔≡ = equivalence Pointwise-≡⇒≡ ≡⇒Pointwise-≡

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

-- Version 0.15

Pointwise-≡ = Pointwise-≡↔≡
{-# WARNING_ON_USAGE Pointwise-≡
"Warning: Pointwise-≡ was deprecated in v0.15.
Please use Pointwise-≡↔≡ instead."
#-}


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
open import LibraBFT.Concrete.Obligations
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types
open        EpochConfig
open import LibraBFT.Yasm.Yasm (ℓ+1 0ℓ) EpochConfig epochId authorsN ConcSysParms NodeId-PK-OK

-- In this module, we assume that the implementation meets its
-- obligations, and use this assumption to prove that, in any reachable
-- state, the implementatioon enjoys one of the per-epoch correctness
-- conditions proved in Abstract.Properties.  It can be extended to other
-- properties later.
module LibraBFT.Concrete.Properties
         (impl-correct : ImplObligations)
         {e}(st : SystemState e)
         (r : ReachableSystemState st)
         (eid : Fin e)
         where
    open        ImplObligations impl-correct
    open import LibraBFT.Concrete.System sps-cor
    open        PerState st r
    open        PerEpoch eid

    open import LibraBFT.Abstract.Abstract     UID _≟UID_ NodeId 𝓔 (ConcreteVoteEvidence 𝓔) as Abs
    open import LibraBFT.Concrete.Intermediate                   𝓔 (ConcreteVoteEvidence 𝓔)
    import      LibraBFT.Concrete.Obligations.VotesOnce          𝓔 (ConcreteVoteEvidence 𝓔) as VO-obl
    import      LibraBFT.Concrete.Obligations.LockedRound        𝓔 (ConcreteVoteEvidence 𝓔) as LR-obl
    open import LibraBFT.Concrete.Properties.VotesOnce                                       as VO
    open import LibraBFT.Concrete.Properties.LockedRound                                     as LR

    --------------------------------------------------------------------------------------------
    -- * A /ValidSysState/ is one in which both peer obligations are obeyed by honest peers * --
    --------------------------------------------------------------------------------------------

    record ValidSysState {ℓ}(𝓢 : IntermediateSystemState ℓ) : Set (ℓ+1 ℓ0 ℓ⊔ ℓ) where
      field
        vss-votes-once   : VO-obl.Type 𝓢
        vss-locked-round : LR-obl.Type 𝓢
    open ValidSysState public

    -- TODO-2 : This should be provided as a module parameter here, and the
    -- proofs provided to instantiate it should be refactored into LibraBFT.Impl.
    -- However, see the TODO-3 in LibraBFT.Concrete.Intermediate, which suggests
    -- that those proofs may change, perhaps some parts of them will remain in
    -- Concrete and others should be in Impl, depending on how that TODO-3 is
    -- addressed.  There is not much point in doing said refactoring until we
    -- make progress on that question.

    validState : ValidSysState IntSystemState
    validState = record
      { vss-votes-once   = VO.Proof.voo sps-cor vo₁ vo₂ st r eid
      ; vss-locked-round = LR.Proof.lrr sps-cor lr₁ st r eid
      }

    open IntermediateSystemState IntSystemState

    open All-InSys-props InSys
    open WithAssumptions InSys

    -- We can now invoke the various abstract correctness properties, using
    --
    ConcCommitsDoNotConflict :
       ∀{q q'}
       → {rc  : RecordChain (Abs.Q q)}  → All-InSys rc
       → {rc' : RecordChain (Abs.Q q')} → All-InSys rc'
       → {b b' : Abs.Block}
       → CommitRule rc  b
       → CommitRule rc' b'
       → NonInjective-≡ Abs.bId ⊎ ((Abs.B b) ∈RC rc' ⊎ (Abs.B b') ∈RC rc)
    ConcCommitsDoNotConflict = CommitsDoNotConflict
           (VO-obl.proof IntSystemState (vss-votes-once validState))
           (LR-obl.proof IntSystemState (vss-locked-round validState))

    module _ (∈QC⇒AllSent : Complete InSys) where

      ConcCommitsDoNotConflict' :
        ∀{q q'}{rc  : RecordChain (Abs.Q q)}{rc' : RecordChain (Abs.Q q')}{b b' : Abs.Block}
        → InSys (Abs.Q q) → InSys (Abs.Q q')
        → CommitRule rc  b
        → CommitRule rc' b'
        → NonInjective-≡ Abs.bId ⊎ ((Abs.B b) ∈RC rc' ⊎ (Abs.B b') ∈RC rc)
      ConcCommitsDoNotConflict' = CommitsDoNotConflict'
           (VO-obl.proof IntSystemState (vss-votes-once validState))
           (LR-obl.proof IntSystemState (vss-locked-round validState))
           ∈QC⇒AllSent

      ConcCommitsDoNotConflict''
        : ∀{o o' q q'}
        → {rcf  : RecordChainFrom o  (Abs.Q q)}
        → {rcf' : RecordChainFrom o' (Abs.Q q')}
        → {b b' : Abs.Block}
        → InSys (Abs.Q q)
        → InSys (Abs.Q q')
        → CommitRuleFrom rcf  b
        → CommitRuleFrom rcf' b'
        → NonInjective-≡ Abs.bId ⊎ Σ (RecordChain (Abs.Q q')) ((Abs.B b)  ∈RC_)
                                 ⊎ Σ (RecordChain (Abs.Q q))  ((Abs.B b') ∈RC_)
      ConcCommitsDoNotConflict'' = CommitsDoNotConflict''
           (VO-obl.proof IntSystemState (vss-votes-once validState))
           (LR-obl.proof IntSystemState (vss-locked-round validState))
           ∈QC⇒AllSent

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:
{-# OPTIONS --without-K #-}
module hott.equivalence.coind where

open import level
open import sum
open import equality.core
open import equality.calculus
open import equality.reasoning
open import function.core
open import function.extensionality
open import function.fibration
open import function.isomorphism
open import function.overloading
open import container.core
open import container.fixpoint
open import container.m
open import hott.equivalence.core
open import hott.equivalence.alternative
open import hott.level
open import sets.unit

apply≅' : ∀ {i j}{X : Set i}{Y : Set j}
        → X ≅' Y → X → Y
apply≅' (i , _) = _≅_.to i

is-≅' : ∀ {i j}{X : Set i}{Y : Set j} → (X → Y) → Set _
is-≅' {X = X}{Y = Y} f = apply≅' ⁻¹ f

abstract
  ≅'-≈-fib-comm : ∀ {i j}{X : Set i}{Y : Set j}(eq : X ≅' Y)
                → proj₁ (≅'⇒≈ eq) ≡ apply≅' eq
  ≅'-≈-fib-comm eq = refl

  ≅'⇒≈-we : ∀ {i j}{X : Set i}{Y : Set j}
           → weak-equiv (≅'⇒≈ {X = X}{Y = Y})
  ≅'⇒≈-we = proj₂ (≅⇒≈ (sym≅ ≈⇔≅'))

  is-≅'-≈-iso : ∀ {i j}{X : Set i}{Y : Set j}(f : X → Y)
              → is-≅' f ≅ weak-equiv f
  is-≅'-≈-iso {X = X}{Y = Y} f = begin
      is-≅' f
    ≡⟨ refl ⟩
      (fib weak-equiv ∘' ≅'⇒≈) ⁻¹ f
    ≅⟨ fib-compose ≅'⇒≈ (fib weak-equiv) f ⟩
      ( Σ (fib weak-equiv ⁻¹ f) λ { (we , _) → ≅'⇒≈ ⁻¹ we } )
    ≅⟨ ( Σ-ap-iso refl≅ λ { (we , _)
        → contr-⊤-iso (≅'⇒≈-we we) } ) ⟩
      ( fib weak-equiv ⁻¹ f × ⊤ )
    ≅⟨ ×-right-unit ⟩
      fib weak-equiv ⁻¹ f
    ≅⟨ fib-iso f ⟩
      weak-equiv f
    ∎
    where open ≅-Reasoning

is-≅'-h1 : ∀ {i j}{X : Set i}{Y : Set j}
         → (f : X → Y) → h 1 (is-≅' f)
is-≅'-h1 f = iso-level (sym≅ (is-≅'-≈-iso f)) (weak-equiv-h1 f)

≅'-Σ-iso : ∀ {i j}{X : Set i}{Y : Set j}
         → (X ≅' Y) ≅ (Σ (X → Y) λ f → is-≅' f)
≅'-Σ-iso {X = X}{Y = Y} = sym≅ (total-iso apply≅')

≅'-equality : ∀ {i j}{X : Set i}{Y : Set j}
            → {isom₁ isom₂ : X ≅' Y}
            → (apply isom₁ ≡ apply isom₂)
            → isom₁ ≡ isom₂
≅'-equality {X = X}{Y = Y} {isom₁}{isom₂} p = iso⇒inj ≅'-Σ-iso q
  where
    q : apply ≅'-Σ-iso isom₁ ≡ apply ≅'-Σ-iso isom₂
    q = unapΣ (p , h1⇒prop (is-≅'-h1 _) _ _)

record F {i j}(Z : ∀ {i j} → Set i → Set j → Set (i ⊔ j))
         (X : Set i)(Y : Set j) : Set (i ⊔ j) where
  constructor mk-F
  field
    f : X → Y
    g : Y → X
    φ : (x : X)(y : Y) → Z (f x ≡ y) (x ≡ g y)

~-container : ∀ i → Container _ _ _
~-container i = record
  { I = Set i × Set i
  ; A = λ { (X , Y) → (X → Y) × (Y → X) }
  ; B = λ { {X , Y} _ → X × Y }
  ; r = λ { {a = f , g} (x , y) → (f x ≡ y) , (x ≡ g y) } }

module D {i} where
  open Definition (~-container i) public
  open Fixpoint (fix M fixpoint) public
    hiding (fixpoint)

unfold≅' : ∀ {i}{X Y : Set i}
         → X ≅' Y → D.F (λ { (X , Y) → X ≅' Y }) (X , Y)
unfold≅' (isom , _)
  = (to , from)
  , λ { (x , y) → ≅⇒≅' (iso-adjunction isom x y) }
  where
    open _≅_ isom

--unfold≅' : ∀ {i}{X Y : Set i}
--         → X ≅' Y → D.F (λ { (X , Y) → X ≅' Y }) (X , Y)
--unfold≅' {X = X}{Y = Y} (iso f g α β , δ) =
--    ((f , g) , λ {(x , y) → ≅⇒≅' (φ x y)})
--  where
--    open ≡-Reasoning
--
--    δ' = co-coherence (iso f g α β) δ
--
--    iso₁ : {x : X}{y : Y}(p : f x ≡ y)
--         → ap f (sym (α x) · ap g p) · β y ≡ p
--    iso₁ {x} .{f x} refl = begin
--        ap f (sym (α x) · refl) · β (f x)
--      ≡⟨ ap (λ z → ap f z · β (f x)) (left-unit (sym (α x)))  ⟩
--        ap f (sym (α x)) · β (f x)
--      ≡⟨ ap (λ z → z · β (f x)) (ap-inv f (α x)) ⟩
--        sym (ap f (α x)) · β (f x)
--      ≡⟨ ap (λ z → sym z · β (f x)) (δ x) ⟩
--        sym (β (f x)) · β (f x)
--      ≡⟨ right-inverse (β (f x)) ⟩
--        refl
--      ∎
--
--    iso₂' : {x : X}{y : Y}(q : g y ≡ x)
--         → sym (α x) · ap g (ap f (sym q) · β y) ≡ sym q
--    iso₂' .{g y}{y} refl = begin
--        sym (α (g y)) · ap g (refl · β y)
--      ≡⟨ ap (λ z → sym (α (g y)) · ap g z) (right-unit (β y)) ⟩
--        sym (α (g y)) · ap g (β y)
--      ≡⟨ ap (λ z → sym (α (g y)) · z) (δ' y) ⟩
--        sym (α (g y)) · α (g y)
--      ≡⟨ right-inverse (α (g y)) ⟩
--        refl
--      ∎
--
--    iso₂ : {x : X}{y : Y}(q : x ≡ g y)
--         → sym (α x) · ap g (ap f q · β y) ≡ q
--    iso₂ {x}{y} q =
--      subst (λ z → sym (α x) · ap g (ap f z · β y) ≡ z)
--            (double-inverse q)
--            (iso₂' (sym q))
--
--    φ : (x : X)(y : Y) → (f x ≡ y) ≅ (x ≡ g y)
--    φ x y = record
--      { to = λ p → sym (α x) · ap g p
--      ; from = λ q → ap f q · β y
--      ; iso₁ = iso₁
--      ; iso₂ = iso₂ }

Iso' : ∀ {i} → Set i × Set i → Set _
Iso' (X , Y) = X ≅' Y

_~_ : ∀ {i} → Set i → Set i → Set i
_~_ {i} X Y = D.M (X , Y)

apply~ : ∀ {i}{X Y : Set i} → X ~ Y → X → Y
apply~ eq = proj₁ (D.head eq)

invert~ : ∀ {i}{X Y : Set i} → X ~ Y → Y → X
invert~ eq = proj₂ (D.head eq)

private
  u : ∀ {i}(XY : Set i × Set i)
    → let (X , Y) = XY in X ~ Y → X ≅' Y
  u (X , Y) eq = ≅⇒≅' (iso f g α β)
    where
      f : X → Y
      f = apply~ eq

      g : Y → X
      g = invert~ eq

      φ : (x : X)(y : Y) → (f x ≡ y) ~ (x ≡ g y)
      φ x y = D.tail eq (x , y)

      α : (x : X) → g (f x) ≡ x
      α x = sym (apply~ (φ x (f x)) refl)

      β : (y : Y) → f (g y) ≡ y
      β y = invert~ (φ (g y) y) refl

--   u-morphism : ∀ {i}{X Y : Set i}
--              → (eq : X ~ Y)
--              → unfold≅' (u _ eq)
--              ≡ D.imap u _ (D.out _ eq)
--   u-morphism {i}{X}{Y} eq = unapΣ (refl , funext λ {(x , y) → lem₂ x y})
--     where
--       f : X → Y
--       f = apply~ eq
--
--       g : Y → X
--       g = invert~ eq
--
--       φ : (x : X)(y : Y) → (f x ≡ y) ~ (x ≡ g y)
--       φ x y = D.tail eq (x , y)
--
--       σ τ : (x : X)(y : Y) → (f x ≡ y) ≅' (x ≡ g y)
--       σ x y = proj₂ (unfold≅' (u _ eq)) (x , y)
--       τ x y = u _ (φ x y)
--
--       lem : (x : X)(y : Y)(p : f x ≡ y)
--            → apply≅' (σ x y) p ≡ apply≅' (τ x y) p
--       lem x .(f x) refl = ?
--
--       lem₂ : (x : X)(y : Y) → proj₂ (unfold≅' (u (X , Y) eq)) (x , y)
--                             ≡ u _ (D.tail eq (x , y))
--       lem₂ x y = ≅'-equality (funext (lem x y))
--
--   v : ∀ {i}(XY : Set i × Set i) → let (X , Y) = XY in X ≅' Y → X ~ Y
--   v = D.unfold (λ _ → unfold≅')
--
--   vu-morphism : ∀ {i}{X Y : Set i}
--               → (eq : X ~ Y)
--               → D.out _ (v _ (u _ eq))
--               ≡ D.imap (v D.∘ⁱ u) _ (D.out _ eq)
--   vu-morphism {X = X}{Y = Y} eq = ap (D.imap v _) (u-morphism eq)
--
--   vu-id : ∀ {i}{X Y : Set i} (eq : X ~ Y) → v _ (u _ eq) ≡ eq
--   vu-id eq = D.unfold-η D.out (v D.∘ⁱ u) vu-morphism eq · D.unfold-id eq
--
--   uv-id : ∀ {i}{X Y : Set i} (i : X ≅' Y) → u _ (v _ i) ≡ i
--   uv-id {X = X}{Y = Y} i = ≅'-equality refl
--
-- ~⇔≅' : ∀ {i}{X Y : Set i} → (X ~ Y) ≅ (X ≅' Y)
-- ~⇔≅' = iso (u _) (v _) vu-id uv-id

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


text:
module TestInt where

open import PreludeInt
open import PreludeShow

mainS = showInt result where
  result = (mod (((int 2) + (int 2)) * (int 5)) (int 3))

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------------
-- Arithmetic properties
------------------------------------------------------------------------------

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

module LTC-PCF.Data.Nat.Properties where

open import Common.FOL.Relation.Binary.EqReasoning

open import LTC-PCF.Base
open import LTC-PCF.Base.Properties
open import LTC-PCF.Data.Nat
open import LTC-PCF.Data.Nat.Rec
open import LTC-PCF.Data.Nat.Rec.ConversionRules
open import LTC-PCF.Data.Nat.UnaryNumbers

------------------------------------------------------------------------------
-- Congruence properties

+-leftCong : ∀ {m n o} → m ≡ n → m + o ≡ n + o
+-leftCong refl = refl

+-rightCong : ∀ {m n o} → n ≡ o → m + n ≡ m + o
+-rightCong refl = refl

∸-leftCong : ∀ {m n o} → m ≡ n → m ∸ o ≡ n ∸ o
∸-leftCong refl = refl

∸-rightCong : ∀ {m n o} → n ≡ o → m ∸ n ≡ m ∸ o
∸-rightCong refl = refl

*-leftCong : ∀ {m n o} → m ≡ n → m * o ≡ n * o
*-leftCong refl = refl

*-rightCong : ∀ {m n o} → n ≡ o → m * n ≡ m * o
*-rightCong refl = refl

------------------------------------------------------------------------------
-- Conversion rules

+-0x : ∀ n → zero + n ≡ n
+-0x n = rec zero n _ ≡⟨ rec-0 n ⟩
         n            ∎

+-Sx : ∀ m n → succ₁ m + n ≡ succ₁ (m + n)
+-Sx m n =
  rec (succ₁ m) n (lam (λ _ → lam succ₁))
    ≡⟨ rec-S m n (lam (λ _ → lam succ₁)) ⟩
  (lam (λ _ → lam succ₁)) · m · (m + n)
    ≡⟨ ·-leftCong (beta (λ _ → lam succ₁) m) ⟩
  lam succ₁ · (m + n)
    ≡⟨ beta succ₁ (m + n) ⟩
  succ₁ (m + n) ∎

∸-x0 : ∀ n → n ∸ zero ≡ n
∸-x0 n = rec zero n _ ≡⟨ rec-0 n ⟩
         n            ∎

∸-xS : ∀ m n → m ∸ succ₁ n ≡ pred₁ (m ∸ n)
∸-xS m n =
  rec (succ₁ n) m (lam (λ _ → lam pred₁))
    ≡⟨ rec-S n m (lam (λ _ → lam pred₁)) ⟩
  lam (λ x → lam pred₁) · n · (m ∸ n)
    ≡⟨ ·-leftCong (beta (λ _ → lam pred₁) n) ⟩
  lam pred₁ · (m ∸ n)
    ≡⟨ beta pred₁ (m ∸ n) ⟩
  pred₁ (m ∸ n) ∎

*-0x : ∀ n → zero * n ≡ zero
*-0x n = rec zero zero (lam (λ _ → lam (_+_ n))) ≡⟨ rec-0 zero ⟩
         zero                                          ∎

*-Sx : ∀ m n → succ₁ m * n ≡ n + m * n
*-Sx m n =
  rec (succ₁ m) zero (lam (λ _ → lam (_+_ n)))
    ≡⟨ rec-S m zero (lam (λ _ → lam (_+_ n))) ⟩
  (lam (λ _ → lam (_+_ n))) · m · (m * n)
    ≡⟨ ·-leftCong (beta (λ _ → lam (_+_ n)) m) ⟩
  lam (_+_ n) · (m * n)
    ≡⟨ beta (_+_ n) (m * n) ⟩
  n + (m * n) ∎

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

+-leftIdentity : ∀ n → zero + n ≡ n
+-leftIdentity = +-0x

+-rightIdentity : ∀ {n} → N n → n + zero ≡ n
+-rightIdentity nzero          = +-leftIdentity zero
+-rightIdentity (nsucc {n} Nn) =
  trans (+-Sx n zero) (succCong (+-rightIdentity Nn))

pred-N : ∀ {n} → N n → N (pred₁ n)
pred-N nzero          = subst N (sym pred-0) nzero
pred-N (nsucc {n} Nn) = subst N (sym (pred-S n)) Nn

+-N : ∀ {m n} → N m → N n → N (m + n)
+-N {n = n} nzero          Nn = subst N (sym (+-leftIdentity n)) Nn
+-N {n = n} (nsucc {m} Nm) Nn = subst N (sym (+-Sx m n)) (nsucc (+-N Nm Nn))

∸-N : ∀ {m n} → N m → N n → N (m ∸ n)
∸-N {m} Nm nzero          = subst N (sym (∸-x0 m)) Nm
∸-N {m} Nm (nsucc {n} Nn) = subst N (sym (∸-xS m n)) (pred-N (∸-N Nm Nn))

+-assoc : ∀ {m} → N m → ∀ n o → m + n + o ≡ m + (n + o)
+-assoc nzero n o =
  zero + n + o   ≡⟨ +-leftCong (+-leftIdentity n) ⟩
  n + o          ≡⟨ sym (+-leftIdentity (n + o)) ⟩
  zero + (n + o) ∎

+-assoc (nsucc {m} Nm) n o =
  succ₁ m + n + o     ≡⟨ +-leftCong (+-Sx m n) ⟩
  succ₁ (m + n) + o   ≡⟨ +-Sx (m + n) o ⟩
  succ₁ (m + n + o)   ≡⟨ succCong (+-assoc Nm n o) ⟩
  succ₁ (m + (n + o)) ≡⟨ sym (+-Sx m (n + o)) ⟩
  succ₁ m + (n + o)   ∎

x+Sy≡S[x+y] : ∀ {m} → N m → ∀ n → m + succ₁ n ≡ succ₁ (m + n)
x+Sy≡S[x+y] nzero n =
  zero + succ₁ n   ≡⟨ +-leftIdentity (succ₁ n) ⟩
  succ₁ n          ≡⟨ succCong (sym (+-leftIdentity n)) ⟩
  succ₁ (zero + n) ∎

x+Sy≡S[x+y] (nsucc {m} Nm) n =
  succ₁ m + succ₁ n     ≡⟨ +-Sx m (succ₁ n) ⟩
  succ₁ (m + succ₁ n)   ≡⟨ succCong (x+Sy≡S[x+y] Nm n) ⟩
  succ₁ (succ₁ (m + n)) ≡⟨ succCong (sym (+-Sx m n)) ⟩
  succ₁ (succ₁ m + n)   ∎

0∸x : ∀ {n} → N n → zero ∸ n ≡ zero
0∸x nzero          = ∸-x0 zero
0∸x (nsucc {n} Nn) =
  zero ∸ succ₁ n   ≡⟨ ∸-xS zero n ⟩
  pred₁ (zero ∸ n) ≡⟨ predCong (0∸x Nn) ⟩
  pred₁ zero       ≡⟨ pred-0 ⟩
  zero             ∎

S∸S : ∀ {m n} → N m → N n → succ₁ m ∸ succ₁ n ≡ m ∸ n
S∸S {m} _ nzero =
  succ₁ m ∸ [1]          ≡⟨ ∸-xS (succ₁ m) zero ⟩
  pred₁ (succ₁ m ∸ zero) ≡⟨ predCong (∸-x0 (succ₁ m)) ⟩
  pred₁ (succ₁ m)        ≡⟨ pred-S m ⟩
  m                      ≡⟨ sym (∸-x0 m) ⟩
  m ∸ zero               ∎

S∸S nzero (nsucc {n} Nn) =
  [1] ∸ succ₁ (succ₁ n) ≡⟨ ∸-xS [1] (succ₁ n) ⟩
  pred₁ ([1] ∸ succ₁ n) ≡⟨ predCong (S∸S nzero Nn) ⟩
  pred₁ (zero ∸ n)      ≡⟨ predCong (0∸x Nn) ⟩
  pred₁ zero            ≡⟨ pred-0 ⟩
  zero                  ≡⟨ sym (0∸x (nsucc Nn)) ⟩
  zero ∸ succ₁ n        ∎

S∸S (nsucc {m} Nm) (nsucc {n} Nn) =
  succ₁ (succ₁ m) ∸ succ₁ (succ₁ n) ≡⟨ ∸-xS (succ₁ (succ₁ m)) (succ₁ n) ⟩
  pred₁ (succ₁ (succ₁ m) ∸ succ₁ n) ≡⟨ predCong (S∸S (nsucc Nm) Nn) ⟩
  pred₁ (succ₁ m ∸ n)               ≡⟨ sym (∸-xS (succ₁ m) n) ⟩
  succ₁ m ∸ succ₁ n                 ∎

[x+y]∸[x+z]≡y∸z : ∀ {m n o} → N m → N n → N o → (m + n) ∸ (m + o) ≡ n ∸ o
[x+y]∸[x+z]≡y∸z {n = n} {o} nzero _ _ =
  (zero + n) ∸ (zero + o) ≡⟨ ∸-leftCong (+-leftIdentity n) ⟩
    n ∸ (zero + o)        ≡⟨ ∸-rightCong (+-leftIdentity o) ⟩
    n ∸ o                 ∎

[x+y]∸[x+z]≡y∸z {n = n} {o} (nsucc {m} Nm) Nn No =
  (succ₁ m + n) ∸ (succ₁ m + o) ≡⟨ ∸-leftCong (+-Sx m n) ⟩
  succ₁ (m + n) ∸ (succ₁ m + o) ≡⟨ ∸-rightCong (+-Sx m o) ⟩
  succ₁ (m + n) ∸ succ₁ (m + o) ≡⟨ S∸S (+-N Nm Nn) (+-N Nm No) ⟩
  (m + n) ∸ (m + o)             ≡⟨ [x+y]∸[x+z]≡y∸z Nm Nn No ⟩
  n ∸ o                         ∎

+-comm : ∀ {m n} → N m → N n → m + n ≡ n + m
+-comm {n = n} nzero Nn =
  zero + n ≡⟨ +-leftIdentity n ⟩
  n        ≡⟨ sym (+-rightIdentity Nn) ⟩
  n + zero ∎

+-comm {n = n} (nsucc {m} Nm) Nn =
  succ₁ m + n   ≡⟨ +-Sx m n ⟩
  succ₁ (m + n) ≡⟨ succCong (+-comm Nm Nn) ⟩
  succ₁ (n + m) ≡⟨ sym (x+Sy≡S[x+y] Nn m) ⟩
  n + succ₁ m   ∎

*-leftZero : ∀ n → zero * n ≡ zero
*-leftZero = *-0x

*-rightZero : ∀ {n} → N n → n * zero ≡ zero
*-rightZero nzero          = *-leftZero zero
*-rightZero (nsucc {n} Nn) =
  trans (*-Sx n zero)
        (trans (+-leftIdentity (n * zero)) (*-rightZero Nn))

*-N : ∀ {m n} → N m → N n → N (m * n)
*-N {n = n} nzero          _  = subst N (sym (*-leftZero n)) nzero
*-N {n = n} (nsucc {m} Nm) Nn = subst N (sym (*-Sx m n)) (+-N Nn (*-N Nm Nn))

*-leftIdentity : ∀ {n} → N n → [1] * n ≡ n
*-leftIdentity {n} Nn =
  [1] * n      ≡⟨ *-Sx zero n ⟩
  n + zero * n ≡⟨ +-rightCong (*-leftZero n) ⟩
  n + zero     ≡⟨ +-rightIdentity Nn ⟩
  n            ∎

x*Sy≡x+xy : ∀ {m n} → N m → N n → m * succ₁ n ≡ m + m * n
x*Sy≡x+xy {n = n} nzero Nn = sym
  (
    zero + zero * n ≡⟨ +-rightCong (*-leftZero n) ⟩
    zero + zero     ≡⟨ +-leftIdentity zero ⟩
    zero            ≡⟨ sym (*-leftZero (succ₁ n)) ⟩
    zero * succ₁ n  ∎
  )

x*Sy≡x+xy {n = n} (nsucc {m} Nm) Nn =
  succ₁ m * succ₁ n
    ≡⟨ *-Sx m (succ₁ n) ⟩
  succ₁ n + m * succ₁ n
    ≡⟨ +-rightCong (x*Sy≡x+xy Nm Nn) ⟩
  succ₁ n + (m + m * n)
    ≡⟨ +-Sx n (m + m * n) ⟩
  succ₁ (n + (m + m * n))
    ≡⟨ succCong (sym (+-assoc Nn m (m * n))) ⟩
  succ₁ (n + m + m * n)
    ≡⟨ succCong (+-leftCong (+-comm Nn Nm)) ⟩
  succ₁ (m + n + m * n)
    ≡⟨ succCong (+-assoc Nm n (m * n)) ⟩
  succ₁ (m + (n + m * n))
    ≡⟨ sym (+-Sx m (n + m * n)) ⟩
  succ₁ m + (n + m * n)
    ≡⟨ +-rightCong (sym (*-Sx m n)) ⟩
  succ₁ m + succ₁ m * n ∎

*-comm : ∀ {m n} → N m → N n → m * n ≡ n * m
*-comm {n = n} nzero          Nn = trans (*-leftZero n) (sym (*-rightZero Nn))
*-comm {n = n} (nsucc {m} Nm) Nn =
  succ₁ m * n  ≡⟨ *-Sx m n ⟩
  n + m * n    ≡⟨ +-rightCong (*-comm Nm Nn) ⟩
  n + n * m    ≡⟨ sym (x*Sy≡x+xy Nn Nm) ⟩
  n * succ₁ m  ∎

*∸-leftDistributive : ∀ {m n o} → N m → N n → N o → (m ∸ n) * o ≡ m * o ∸ n * o
*∸-leftDistributive {m} {o = o} _ nzero _ =
  (m ∸ zero) * o   ≡⟨ *-leftCong (∸-x0 m) ⟩
  m * o            ≡⟨ sym (∸-x0 (m * o)) ⟩
  m * o ∸ zero     ≡⟨ ∸-rightCong (sym (*-leftZero o)) ⟩
  m * o ∸ zero * o ∎

*∸-leftDistributive {o = o} nzero (nsucc {n} Nn) No =
  (zero ∸ succ₁ n) * o   ≡⟨ *-leftCong (0∸x (nsucc Nn)) ⟩
  zero * o               ≡⟨ *-leftZero o ⟩
  zero                   ≡⟨ sym (0∸x (*-N (nsucc Nn) No)) ⟩
  zero ∸ succ₁ n * o     ≡⟨ ∸-leftCong (sym (*-leftZero o)) ⟩
  zero * o ∸ succ₁ n * o ∎

*∸-leftDistributive (nsucc {m} Nm) (nsucc {n} Nn) nzero =
  (succ₁ m ∸ succ₁ n) * zero
    ≡⟨ *-comm (∸-N (nsucc Nm) (nsucc Nn)) nzero ⟩
  zero * (succ₁ m ∸ succ₁ n)
    ≡⟨ *-leftZero (succ₁ m ∸ succ₁ n) ⟩
  zero
    ≡⟨ sym (0∸x (*-N (nsucc Nn) nzero)) ⟩
  zero ∸ succ₁ n * zero
    ≡⟨ ∸-leftCong (sym (*-leftZero (succ₁ m))) ⟩
  zero * succ₁ m ∸ succ₁ n * zero
    ≡⟨ ∸-leftCong (*-comm nzero (nsucc Nm)) ⟩
  succ₁ m * zero ∸ succ₁ n * zero ∎

*∸-leftDistributive (nsucc {m} Nm) (nsucc {n} Nn) (nsucc {o} No) =
  (succ₁ m ∸ succ₁ n) * succ₁ o
    ≡⟨ *-leftCong (S∸S Nm Nn) ⟩
  (m ∸ n) * succ₁ o
     ≡⟨ *∸-leftDistributive Nm Nn (nsucc No) ⟩
  m * succ₁ o ∸ n * succ₁ o
    ≡⟨ sym ([x+y]∸[x+z]≡y∸z (nsucc No) (*-N Nm (nsucc No)) (*-N Nn (nsucc No))) ⟩
  (succ₁ o + m * succ₁ o) ∸ (succ₁ o + n * succ₁ o)
    ≡⟨ ∸-leftCong (sym (*-Sx m (succ₁ o))) ⟩
  (succ₁ m * succ₁ o) ∸ (succ₁ o + n * succ₁ o)
    ≡⟨ ∸-rightCong (sym (*-Sx n (succ₁ o))) ⟩
  (succ₁ m * succ₁ o) ∸ (succ₁ n * succ₁ o) ∎

*+-leftDistributive : ∀ {m n o} → N m → N n → N o → (m + n) * o ≡ m * o + n * o
*+-leftDistributive {m} {n} Nm Nn nzero =
  (m + n) * zero
    ≡⟨ *-comm (+-N Nm Nn) nzero ⟩
  zero * (m + n)
    ≡⟨ *-leftZero (m + n) ⟩
  zero
    ≡⟨ sym (*-leftZero m) ⟩
  zero * m
    ≡⟨ *-comm nzero Nm ⟩
  m * zero
    ≡⟨ sym (+-rightIdentity (*-N Nm nzero)) ⟩
  m * zero + zero
    ≡⟨ +-rightCong (trans (sym (*-leftZero n)) (*-comm nzero Nn)) ⟩
  m * zero + n * zero ∎

*+-leftDistributive {n = n} nzero Nn (nsucc {o} No) =
  (zero + n) * succ₁ o         ≡⟨ *-leftCong (+-leftIdentity n) ⟩
  n * succ₁ o                  ≡⟨ sym (+-leftIdentity (n * succ₁ o)) ⟩
  zero + n * succ₁ o           ≡⟨ +-leftCong (sym (*-leftZero (succ₁ o))) ⟩
  zero * succ₁ o + n * succ₁ o ∎

*+-leftDistributive (nsucc {m} Nm) nzero (nsucc {o} No) =
  (succ₁ m + zero) * succ₁ o
    ≡⟨ *-leftCong (+-rightIdentity (nsucc Nm)) ⟩
  succ₁ m * succ₁ o
    ≡⟨ sym (+-rightIdentity (*-N (nsucc Nm) (nsucc No))) ⟩
  succ₁ m * succ₁ o + zero
    ≡⟨ +-rightCong (sym (*-leftZero (succ₁ o))) ⟩
  succ₁ m * succ₁ o + zero * succ₁ o ∎

*+-leftDistributive (nsucc {m} Nm) (nsucc {n} Nn) (nsucc {o} No) =
  (succ₁ m + succ₁ n) * succ₁ o
    ≡⟨ *-leftCong (+-Sx m (succ₁ n)) ⟩
  succ₁ (m + succ₁ n) * succ₁ o
    ≡⟨ *-Sx (m + succ₁ n) (succ₁ o) ⟩
  succ₁ o + (m + succ₁ n) * succ₁ o
    ≡⟨ +-rightCong (*+-leftDistributive Nm (nsucc Nn) (nsucc No)) ⟩
  succ₁ o + (m * succ₁ o + succ₁ n * succ₁ o)
    ≡⟨ sym (+-assoc (nsucc No) (m * succ₁ o) (succ₁ n * succ₁ o)) ⟩
  succ₁ o + m * succ₁ o + succ₁ n * succ₁ o
    ≡⟨ +-leftCong (sym (*-Sx m (succ₁ o))) ⟩
  succ₁ m * succ₁ o + succ₁ n * succ₁ o ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import lib.Basics
open import lib.types.TLevel
open import lib.types.Pi
open import lib.types.Truncation

-- This module is dedicated to [Trunc 0 (x == y)]

module lib.types.PathSet where

_=₀_ : ∀ {i} {A : Type i} → A → A → Type i
_=₀_ x y = Trunc 0 (x == y)

_=0_ : ∀ {i} {A : Type i} → A → A → Type i
_=0_ = _=₀_

infix 80 _∙₀_ _∙₀'_ -- \.\0
_∙₀_ : ∀ {i} {A : Type i} {x y z : A} → x =₀ y → y =₀ z → x =₀ z
_∙₀_ = Trunc-fmap2 _∙_

_∙₀'_ : ∀ {i} {A : Type i} {x y z : A} → x =₀ y → y =₀ z → x =₀ z
_∙₀'_ = Trunc-fmap2 _∙'_

!₀ : ∀ {i} {A : Type i} {x y : A} → x =₀ y → y =₀ x
!₀ = Trunc-fmap !

idp₀ : ∀ {i} {A : Type i} {a : A} → a =₀ a
idp₀ = [ idp ]

ap₀ : ∀ {i j} {A : Type i} {B : Type j} {x y : A} (f : A → B)
  → x =₀ y → f x =₀ f y
ap₀ f = Trunc-rec Trunc-level ([_] ∘ ap f)

coe₀ : ∀ {i} {A B : Type i} (_ : is-set B) (p : A =₀ B) → A → B
coe₀ B-level = Trunc-rec (→-is-set B-level) coe

transport₀ : ∀ {i j} {A : Type i} (B : A → Type j) {x y : A}
  (B-level : is-set (B y)) (p : x =₀ y) → (B x → B y)
transport₀ B B-level p = coe₀ B-level (ap₀ B p)

module _ {i} {A : Type i} where

  abstract
    ∙₀-unit-r : ∀ {x y : A} (q : x =₀ y) → (q ∙₀ idp₀) == q
    ∙₀-unit-r = Trunc-elim
      (λ _ →  =-preserves-level 0 Trunc-level)
      (λ p → ap [_] $ ∙-unit-r p)

    ∙₀-unit-l : ∀ {x y : A} (q : x =₀ y) → (idp₀ ∙₀ q) == q
    ∙₀-unit-l = Trunc-elim
      (λ _ →  =-preserves-level 0 Trunc-level)
      (λ _ → idp)

    ∙₀-assoc : {x y z t : A} (p : x =₀ y) (q : y =₀ z) (r : z =₀ t)
      → (p ∙₀ q) ∙₀ r == p ∙₀ (q ∙₀ r)
    ∙₀-assoc = Trunc-elim
      (λ _ → Π-is-set λ _ → Π-is-set λ _ → =-preserves-level 0 Trunc-level)
      (λ p → Trunc-elim
        (λ _ → Π-is-set λ _ → =-preserves-level 0 Trunc-level)
        (λ q → Trunc-elim
          (λ _ → =-preserves-level 0 Trunc-level)
          (λ r → ap [_] $ ∙-assoc p q r)))

    !₀-inv-l : {x y : A} (p : x =₀ y) → (!₀ p) ∙₀ p == idp₀
    !₀-inv-l = Trunc-elim
      (λ _ →  =-preserves-level 0 Trunc-level)
      (λ p → ap [_] $ !-inv-l p)

    !₀-inv-r : {x y : A} (p : x =₀ y) → p ∙₀ (!₀ p) == idp₀
    !₀-inv-r = Trunc-elim
      (λ _ →  =-preserves-level 0 Trunc-level)
      (λ p → ap [_] $ !-inv-r p)

    ∙₀-ap₀ : ∀ {j} {B : Type j} (f : A → B) {x y z : A} (p : x =₀ y) (q : y =₀ z)
      → ap₀ f p ∙₀ ap₀ f q == ap₀ f (p ∙₀ q)
    ∙₀-ap₀ f = Trunc-elim
      (λ _ → Π-is-set λ _ → =-preserves-level 0 Trunc-level)
      (λ p → Trunc-elim
        (λ _ → =-preserves-level 0 Trunc-level)
        (λ q → ap [_] $ ∙-ap f p q))

    ap₀-∘ : ∀ {j k} {B : Type j} {C : Type k} (g : B → C) (f : A → B)
      {x y : A} (p : x =₀ y) → ap₀ (g ∘ f) p == ap₀ g (ap₀ f p)
    ap₀-∘ f g = Trunc-elim
      (λ _ → =-preserves-level 0 Trunc-level)
      (λ p → ap [_] $ ap-∘ f g p)

    coe₀-∙₀ : {B C : Type i} (B-level : is-set B) (C-level : is-set C)
      → (p : A =₀ B) (q : B =₀ C) (a : A)
      → coe₀ C-level (p ∙₀ q) a == coe₀ C-level q (coe₀ B-level p a)
    coe₀-∙₀ B-level C-level = Trunc-elim
      (λ _ → Π-is-set λ _ → Π-is-set λ _ → =-preserves-level 0 C-level)
      (λ p → Trunc-elim
        (λ _ → Π-is-set λ _ → =-preserves-level 0 C-level)
        (λ q a → coe-∙ p q a))

    trans₀-∙₀ : ∀ {j} {B : A → Type j}
      → (B-level : ∀ a → is-set (B a))
      → {x y z : A} (p : x =₀ y) (q : y =₀ z) (b : B x)
      → transport₀ B (B-level _) (p ∙₀ q) b
      == transport₀ B (B-level _) q (transport₀ B (B-level _) p b)
    trans₀-∙₀ B-level = Trunc-elim
      (λ _ → Π-is-set λ _ → Π-is-set λ _ → =-preserves-level 0 $ B-level _)
      (λ p → Trunc-elim
        (λ _ → Π-is-set λ _ → =-preserves-level 0 $ B-level _)
        (λ q b → trans-∙ p q b))

    trans₀-∙₀' : ∀ {j} {B : A → Type j}
      → (B-level : ∀ a → is-set (B a))
      → {x y z : A} (p : x =₀ y) (q : y =₀ z) (b : B x)
      → transport₀ B (B-level _) (p ∙₀' q) b
      == transport₀ B (B-level _) q (transport₀ B (B-level _) p b)
    trans₀-∙₀' B-level = Trunc-elim
      (λ _ → Π-is-set λ _ → Π-is-set λ _ → =-preserves-level 0 $ B-level _)
      (λ p → Trunc-elim
        (λ _ → Π-is-set λ _ → =-preserves-level 0 $ B-level _)
        (λ q b → trans-∙' p q b))

{-
module _ {i} {A : Type i} where
  trans-id≡₀cst : {a b c : A} (p : b ≡ c) (q : b ≡₀ a)
    → transport (λ x → x ≡₀ a) p q ≡ proj (! p) ∘₀ q
  trans-id≡₀cst refl q = ! $ refl₀-left-unit q

  trans-cst≡₀id : {a b c : A} (p : b ≡ c) (q : a ≡₀ b)
    → transport (λ x → a ≡₀ x) p q ≡ q ∘₀ proj p
  trans-cst≡₀id refl q = ! $ refl₀-right-unit q

module _ {i} {A : Set i} where
  homotopy₀-naturality : ∀ {j} {B : Set j} (f g : A → B)
    (p : (x : A) → f x ≡₀ g x) {x y : A} (q : x ≡₀ y)
    → ap₀ f q ∘₀ p y ≡ p x ∘₀ ap₀ g q
  homotopy₀-naturality f g p {x} {y} q = π₀-extend
    ⦃ λ q → ≡-is-set {x = ap₀ f q ∘₀ p y} {y = p x ∘₀ ap₀ g q}
            $ π₀-is-set (f x ≡ g y) ⦄
    (lemma {x} {y}) q
    where
      lemma : ∀ {x y : A} (q : x ≡ y) → ap₀ f (proj q) ∘₀ p y ≡ p x ∘₀ ap₀ g (proj q)
      lemma refl =
        refl₀ ∘₀ p _
          ≡⟨ refl₀-left-unit (p _) ⟩
        p _
          ≡⟨ ! $ refl₀-right-unit _ ⟩∎
        p _ ∘₀ refl₀
          ∎

-- Loop space commutes with truncation in the sense that
-- τ n (Ω X) = Ω (τ (S n) X)
-- (actually, this is true more generally for paths spaces and we need this
-- level of generality to prove it)

module _ {i} {n : ℕ₋₂} {A : Set i} where

  private
    to : (x y : A) → (τ n (x ≡ y)) → ((proj {n = S n} x) ≡ (proj y))
    to x y = τ-extend-nondep ⦃ τ-is-truncated (S n) A _ _ ⦄ (ap proj)

    -- [truncated-path-space (proj x) (proj y)] is [τ n (x ≡ y)]
    truncated-path-space : (u v : τ (S n) A) → Type≤ n i
    truncated-path-space = τ-extend-nondep
                             ⦃ →-is-truncated (S n) (Type≤-is-truncated n _) ⦄
                             (λ x → τ-extend-nondep ⦃ Type≤-is-truncated n _ ⦄
                               (λ y → τ n (x ≡ y) , τ-is-truncated n _))

    -- We now extend [to] to the truncation of [A], and this is why we needed to
    -- first extend the return type of [to]
    to' : (u v : τ (S n) A) → (π₁ (truncated-path-space u v) → u ≡ v)
    to' = τ-extend ⦃ λ x → Π-is-truncated (S n) (λ a →
                             Π-is-truncated (S n) (λ b →
                               ≡-is-truncated (S n)
                                 (τ-is-truncated (S n) A)))⦄
            (λ x → τ-extend ⦃ λ t → Π-is-truncated (S n) (λ a →
                                      ≡-is-truncated (S n)
                                        (τ-is-truncated (S n) A))⦄
              (λ y → to x y))

    from'-refl : (u : τ (S n) A) → (π₁ (truncated-path-space u u))
    from'-refl = τ-extend ⦃ λ x → truncated-is-truncated-S n
                                    (π₂ (truncated-path-space x x))⦄
                   (λ x → proj refl)

    from' : (u v : τ (S n) A) → (u ≡ v → π₁ (truncated-path-space u v))
    from' u .u refl = from'-refl u

    from : (x y : A) → (proj {n = S n} x ≡ proj y → τ n (x ≡ y))
    from x y p = from' (proj x) (proj y) p

    from-to : (x y : A) (p : τ n (x ≡ y)) → from x y (to x y p) ≡ p
    from-to x y = τ-extend ⦃ λ _ → ≡-is-truncated n (τ-is-truncated n _)⦄
                    (from-to' x y) where

      from-to' : (x y : A) (p : x ≡ y) → from x y (to x y (proj p)) ≡ proj p
      from-to' x .x refl = refl

    to'-from' : (u v : τ (S n) A) (p : u ≡ v) → to' u v (from' u v p) ≡ p
    to'-from' x .x refl = to'-from'-refl x where
      to'-from'-refl : (u : τ (S n) A) → to' u u (from' u u refl) ≡ refl
      to'-from'-refl = τ-extend ⦃ λ _ → ≡-is-truncated (S n)
                                          (≡-is-truncated (S n)
                                            (τ-is-truncated (S n) A))⦄
                         (λ _ → refl)

    to-from : (x y : A) (p : proj {n = S n} x ≡ proj y) → to x y (from x y p) ≡ p
    to-from x y p = to'-from' (proj x) (proj y) p

  τ-path-equiv-path-τ-S : {x y : A} → τ n (x ≡ y) ≃ (proj {n = S n} x ≡ proj y)
  τ-path-equiv-path-τ-S {x} {y} =
    (to x y , iso-is-eq _ (from x y) (to-from x y) (from-to x y))

  module _ where
    open import Homotopy.Connected

    abstract
      connected-has-connected-paths : is-connected (S n) A → (p q : A) → is-connected n (p ≡ q)
      connected-has-connected-paths conn p q =
        equiv-types-truncated ⟨-2⟩ (τ-path-equiv-path-τ-S ⁻¹) (contr-is-prop conn (proj p) (proj q))

    connected-has-all-τ-paths : is-connected (S n) A → (p q : A) → τ n (p ≡ q)
    connected-has-all-τ-paths conn p q = π₁ $ connected-has-connected-paths conn p q
-}

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
-- Issue #2791, reported by Ulf 2017-10-05
-- Reported fixed by Victor 2018-08-11

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

IF : Bool → Set → Set → Set
IF true  X Y = X
IF false X Y = Y

postulate
  F : (A : Set) (x : A) (B : Set) (y : B) → Set

mutual
  ?b : Bool
  ?b = _

  IFb = IF ?b Nat Bool

  ?X : IFb
  ?X = _

  ?Y : Nat
  ?Y = _

  foo : F Bool true Nat ?Y ≡ F IFb ?X IFb ?X
  foo = refl

-- ?Y gets solved with 'true'
error : ?Y + 1 ≡ 3
error = refl

-- Expected failure:

-- Nat != Bool of type Set
-- when checking that the expression refl has type
-- F Bool true Nat ?Y ≡ F IFb ?X IFb ?X