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

-- This is more a pair of constructions that a property...
-- but show that one can build a Cone for the Twisted Arrow functor from a Wedge
-- and vice-versa.

open import Categories.Category
open import Categories.Functor.Bifunctor

module Categories.Diagram.Wedge.Properties {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
  (F : Bifunctor (Category.op C) C D) where

private
  module C = Category C
  module D = Category D
  open D
  open HomReasoning
  variable
    A : Obj

open import Level
open import Data.Product using (Σ; _,_)

open import Categories.Category.Construction.TwistedArrow
open import Categories.Category.Equivalence using (StrongEquivalence)
open import Categories.Category.Construction.Cones using (Cones)
open import Categories.Category.Construction.Wedges
open import Categories.Diagram.Cone
open import Categories.Diagram.Wedge F
open import Categories.Functor hiding (id)
open import Categories.Functor.Bifunctor.Properties
open import Categories.Functor.Construction.Constant
open import Categories.Functor.Instance.Twisted C D
import Categories.Morphism as M
open import Categories.Morphism.Reasoning D
open import Categories.NaturalTransformation.Dinatural
open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)

open Functor F

-- There is a construction that builds a Cone (Twist F) from a Wedge
module _ (w : Wedge)  where
  open Wedge w
  open DinaturalTransformation
  open Morphism
  open Morphism⇒

  private
    Wedge-to-Cone′ : {C C′ : C.Obj} (f : C C.⇒ C′) → Wedge.E w ⇒ F₀ (C , C′)
    Wedge-to-Cone′ {C} {C′} f = F₁ (C.id , f) ∘ α dinatural C

  Wedge-to-Cone : Cone (Twist F)
  Wedge-to-Cone = record
    { N = E
    ; apex = record
      { ψ = λ Tw → Wedge-to-Cone′ (arr Tw)
      ; commute = λ { {record { dom = dom₁ ; cod = cod₁ ; arr = arr₁ }}
                      {record { dom = dom ; cod = cod ;  arr = arr }}
                      (record { dom⇐ = dom⇐₁ ; cod⇒ = cod⇒₁; square = square₁}) → begin
        F₁ (dom⇐₁ , cod⇒₁) ∘ F₁ (C.id , arr₁) ∘ dinatural.α dom₁                      ≈⟨ pullˡ (Equiv.sym homomorphism) ⟩
        F₁ (C.id C.∘ dom⇐₁ , cod⇒₁ C.∘ arr₁) ∘ dinatural.α dom₁                       ≈⟨ ([ F ]-decompose₁ ⟩∘⟨refl) ⟩
        (F₁ (C.id C.∘ dom⇐₁ , C.id) ∘ F₁ (C.id , cod⇒₁ C.∘ arr₁)) ∘ dinatural.α dom₁  ≈⟨ (F-resp-≈ (C.identityˡ , C.Equiv.refl) ⟩∘⟨refl ⟩∘⟨refl) ⟩
        (F₁ (dom⇐₁ , C.id) ∘ F₁ (C.id , cod⇒₁ C.∘ arr₁)) ∘ dinatural.α dom₁           ≈⟨ pullʳ (extranatural-commʳ dinatural) ⟩
        F₁ (dom⇐₁ , C.id) ∘ (F₁ (cod⇒₁ C.∘ arr₁ , C.id) ∘ dinatural.α cod)            ≈⟨ pullˡ (Equiv.sym homomorphism) ⟩
        F₁ ((cod⇒₁ C.∘ arr₁) C.∘ dom⇐₁ , C.id C.∘ C.id) ∘ dinatural.α cod             ≈⟨ (F-resp-≈ (C.assoc , C.identity²) ⟩∘⟨refl) ⟩
        F₁ (cod⇒₁ C.∘ arr₁ C.∘ dom⇐₁ , C.id) ∘ dinatural.α cod                        ≈⟨ (F-resp-≈ (square₁ , C.Equiv.refl) ⟩∘⟨refl) ⟩
        F₁ (arr , C.id) ∘ dinatural.α cod                                              ≈˘⟨ extranatural-commʳ dinatural ⟩
        F₁ (C.id , arr) ∘ dinatural.α dom   ∎             }
      }
    }

-- And a construction that builds a Wedge from a Cone (Twist F)
module _ (c : Cone (Twist F)) where
  open Cone c
  open DinaturalTransformation

  private
    fam : {A B : C.Obj} (f : A C.⇒ B) → N ⇒ F₀ (A , B)
    fam f = ψ record { arr = f }
    id² : {A B : C.Obj} (f : A C.⇒ B) → f C.∘ C.id C.∘ C.id C.≈ f
    id² f = C.∘-resp-≈ʳ C.identity² HR.○ C.identityʳ
      where
      module HR = C.HomReasoning

  Cone-to-Wedge : Wedge
  Cone-to-Wedge = record
    { E = N
    ; dinatural = dtHelper record
      { α = λ _ → fam C.id
      ; commute = λ f → begin
        F₁ (C.id , f) ∘ fam C.id ∘ id ≈⟨ pullˡ (Cone.commute c (mor⇒ (id² f))) ⟩
        ψ (record { arr = f }) ∘ id   ≈⟨ pushˡ (Equiv.sym (Cone.commute c (mor⇒ (C.identityˡ C.HomReasoning.○ C.identityˡ)))) ⟩
        F₁ (f , C.id) ∘ fam C.id ∘ id ∎
      }
    }

ConeTwist⇒WedgeF : Functor (Cones (Twist F)) (Wedges F)
ConeTwist⇒WedgeF = record
  { F₀ = Cone-to-Wedge
  ; F₁ = λ c⇒ → record
    { u = Cone⇒.arr c⇒
    ; commute = Cone⇒.commute c⇒
    }
  ; identity = Equiv.refl
  ; homomorphism = Equiv.refl
  ; F-resp-≈ = λ f≈g → f≈g
  }
Wedge⇒ConeTwistF : Functor (Wedges F) (Cones (Twist F))
Wedge⇒ConeTwistF = record
  { F₀ = Wedge-to-Cone
  ; F₁ = λ {A} {B} f → record
    { arr = u f
    ; commute = pullʳ (commute f)
    }
  ; identity = Equiv.refl
  ; homomorphism = Equiv.refl
  ; F-resp-≈ = λ f≈g → f≈g
  }
  where
  open Wedge-Morphism

ConesTwist≅Wedges : StrongEquivalence (Cones (Twist F)) (Wedges F)
ConesTwist≅Wedges = record
  { F = ConeTwist⇒WedgeF
  ; G = Wedge⇒ConeTwistF
  ; weak-inverse = record
    { F∘G≈id = niHelper record
      { η = λ _ → record { u = id ; commute = id-comm ○ (Equiv.sym identity ⟩∘⟨refl) }
      ; η⁻¹ = λ _ → record { u = id ; commute = assoc ○ identity ⟩∘⟨refl ○ (identityˡ ○ identityʳ) }
      ; commute = λ _ → id-comm-sym
      ; iso = λ X → record { isoˡ = identity² ; isoʳ = identity² }
      }
    ; G∘F≈id = niHelper record
      { η = λ Co → record
        { arr = id
        ; commute = λ {X} →
          let m = record { dom⇐ = C.id; cod⇒ = Morphism.arr X; square = (C.∘-resp-≈ʳ C.identity²) C.HomReasoning.○ C.identityʳ}
              a = record { arr = C.id } in begin
          ψ (apex Co) X ∘ id                ≈⟨ identityʳ ⟩
          ψ (apex Co) X                     ≈˘⟨ commute Co m ⟩
          F₁ (C.id , arr X) ∘ ψ (apex Co) a ∎ --
        }
      ; η⁻¹ = λ Co → record
        { arr = id
        ; commute = λ {X} →
        let m = record { dom⇐ = C.id; cod⇒ = Morphism.arr X; square = (C.∘-resp-≈ʳ C.identity²) C.HomReasoning.○ C.identityʳ}
            a = record { arr = C.id } in begin
        (F₁ (C.id , arr X) ∘ ψ (apex Co) a) ∘ id ≈⟨ identityʳ ⟩
        F₁ (C.id , arr X) ∘ ψ (apex Co) a        ≈⟨ commute Co m ⟩
        ψ (apex Co) X ∎
        }
      ; commute = λ f → id-comm-sym
      ; iso = λ X → record { isoˡ = identity² ; isoʳ = identity² }
      }
    }
  }
  where
  open Cone
  open Apex
  open Morphism

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

module Erased-cubical.Cubical where

open import Agda.Builtin.Cubical.Path

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

data D′ : Set where
  @0 c′ : D′

ext: agda

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- Andreas, 2015-12-01, test case to trigger error ModuleArityMismatch EmptyTel
module _ where

  module M where

  module M′ = M Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of vector's Any
------------------------------------------------------------------------

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

module Data.Vec.Relation.Unary.Any.Properties where

open import Function
open import Function.Inverse using (_↔_; inverse)
  renaming (_∘_ to _∘↔_; id to id↔)
open import Data.Vec
  using ( Vec; []; _∷_; _++_; [_]; _>>=_
        ; toList; fromList; map; concat; tabulate; lookup )
open import Data.Vec.Relation.Unary.Any as Any using (Any; here; there)
open import Data.Nat using (suc; zero)
open import Data.Fin using (Fin) renaming (suc to fsuc; zero to fzero)
open import Data.Empty using (⊥)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Data.Sum.Function.Propositional using (_⊎-cong_)
open import Data.Product as Prod using (∃; ∃₂; _×_; _,_; proj₁; proj₂)
open import Relation.Nullary using (¬_)
open import Relation.Unary hiding (_∈_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_; refl)

------------------------------------------------------------------------
-- Equality properties

module _ {a p ℓ} {A : Set a} {P : A → Set p} {_≈_ : Rel A ℓ} where

  open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)

  lift-resp : ∀ {n} → P Respects _≈_ → (Any P {n}) Respects (Pointwise _≈_)
  lift-resp resp []             ()
  lift-resp resp (x∼y ∷ xs∼ys) (here px)   = here (resp x∼y px)
  lift-resp resp (x∼y ∷ xs∼ys) (there pxs) = there (lift-resp resp xs∼ys pxs)

module _ {a p} {A : Set a} {P : Pred A p} where

  here-injective : ∀ {n x xs} {p q : P x} →
                   here {P = P} {n = n} {xs = xs} p ≡ here q → p ≡ q
  here-injective refl = refl

  there-injective : ∀ {n x xs} {p q : Any P xs} →
                    there {n = n} {x = x} p ≡ there q → p ≡ q
  there-injective refl = refl

------------------------------------------------------------------------
-- Misc

  ¬Any[] : ¬ Any P []
  ¬Any[] ()

  lookup-index : ∀ {m} {xs : Vec A m} (p : Any P xs) →
                 P (lookup xs (Any.index p))
  lookup-index (here px) = px
  lookup-index (there p) = lookup-index p

------------------------------------------------------------------------
-- Convert from/to List.Any

  open import Data.List.Relation.Unary.Any as List using (here; there)
  open import Data.List using ([]; _∷_)

  fromList⁺ : ∀ {xs} → List.Any P xs → Any P (fromList xs)
  fromList⁺ (here px) = here px
  fromList⁺ (there v) = there (fromList⁺ v)

  fromList⁻ : ∀ {xs} → Any P (fromList xs) → List.Any P xs
  fromList⁻ {[]}     ()
  fromList⁻ {x ∷ xs} (here px)   = here px
  fromList⁻ {x ∷ xs} (there pxs) = there (fromList⁻ pxs)

  toList⁺ : ∀ {n} {xs : Vec A n} → Any P xs → List.Any P (toList xs)
  toList⁺ (here px) = here px
  toList⁺ (there v) = there (toList⁺ v)

  toList⁻ : ∀ {n} {xs : Vec A n} → List.Any P (toList xs) → Any P xs
  toList⁻ {xs = []}     ()
  toList⁻ {xs = x ∷ xs} (here px)   = here px
  toList⁻ {xs = x ∷ xs} (there pxs) = there (toList⁻ pxs)

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

map-id : ∀ {a p} {A : Set a} {P : A → Set p} (f : P ⊆ P) {n xs} →
         (∀ {x} (p : P x) → f p ≡ p) →
         (p : Any P {n} xs) → Any.map f p ≡ p
map-id f hyp (here  p) = P.cong here (hyp p)
map-id f hyp (there p) = P.cong there $ map-id f hyp p

map-∘ : ∀ {a p q r}
          {A : Set a} {P : A → Set p} {Q : A → Set q} {R : A → Set r}
        (f : Q ⊆ R) (g : P ⊆ Q)
        {n xs} (p : Any P {n} xs) →
        Any.map (f ∘ g) p ≡ Any.map f (Any.map g p)
map-∘ f g (here  p) = refl
map-∘ f g (there p) = P.cong there $ map-∘ f g p

------------------------------------------------------------------------
-- Swapping

module _ {a b ℓ} {A : Set a} {B : Set b} {P : A → B → Set ℓ} where

  swap : ∀ {n m} {xs : Vec A n} {ys : Vec B m} →
         Any (λ x → Any (P x) ys) xs →
         Any (λ y → Any (flip P y) xs) ys
  swap (here  pys)  = Any.map here pys
  swap (there pxys) = Any.map there (swap pxys)

  swap-there : ∀ {n m x xs ys} → (any : Any (λ x → Any (P x) {n} ys) {m} xs) →
               swap (Any.map (there {x = x}) any) ≡ there (swap any)
  swap-there (here  pys)  = refl
  swap-there (there pxys) = P.cong (Any.map there) (swap-there pxys)

module _ {a b ℓ} {A : Set a} {B : Set b} {P : A → B → Set ℓ} where

  swap-invol : ∀ {n m} {xs : Vec A n} {ys : Vec B m} →
               (any : Any (λ x → Any (P x) ys) xs) →
               swap (swap any) ≡ any
  swap-invol (here (here _)) = refl
  swap-invol (here (there pys)) = P.cong (Any.map there) (swap-invol (here pys))
  swap-invol (there pxys) = P.trans (swap-there (swap pxys))
                          $ P.cong there (swap-invol pxys)

module _ {a b ℓ} {A : Set a} {B : Set b} {P : A → B → Set ℓ} where

  swap↔ : ∀ {n m} {xs : Vec A n} {ys : Vec B m} →
          Any (λ x → Any (P x) ys) xs ↔ Any (λ y → Any (flip P y) xs) ys
  swap↔ = inverse swap swap swap-invol swap-invol

------------------------------------------------------------------------
-- Lemmas relating Any to ⊥

⊥↔Any⊥ : ∀ {a} {A : Set a} {n} {xs : Vec A n} → ⊥ ↔ Any (const ⊥) xs
⊥↔Any⊥ = inverse (λ ()) (λ p → from p) (λ ()) (λ p → from p)
  where
  from : ∀ {n xs} → Any (const ⊥) {n} xs → ∀ {b} {B : Set b} → B
  from (here ())
  from (there p) = from p

⊥↔Any[] : ∀ {a p} {A : Set a} {P : A → Set p} → ⊥ ↔ Any P []
⊥↔Any[] = inverse (λ()) (λ()) (λ()) (λ())

------------------------------------------------------------------------
-- Sums commute with Any

module _ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} where

  Any-⊎⁺ : ∀ {n} {xs : Vec A n} → Any P xs ⊎ Any Q xs → Any (λ x → P x ⊎ Q x) xs
  Any-⊎⁺ = [ Any.map inj₁ , Any.map inj₂ ]′

  Any-⊎⁻ : ∀ {n} {xs : Vec A n} → Any (λ x → P x ⊎ Q x) xs → Any P xs ⊎ Any Q xs
  Any-⊎⁻ (here (inj₁ p)) = inj₁ (here p)
  Any-⊎⁻ (here (inj₂ q)) = inj₂ (here q)
  Any-⊎⁻ (there p)       = Sum.map there there (Any-⊎⁻ p)

  ⊎↔ : ∀ {n} {xs : Vec A n} → (Any P xs ⊎ Any Q xs) ↔ Any (λ x → P x ⊎ Q x) xs
  ⊎↔ = inverse Any-⊎⁺ Any-⊎⁻ from∘to to∘from
    where
    from∘to : ∀ {n} {xs : Vec A n} (p : Any P xs ⊎ Any Q xs) → Any-⊎⁻ (Any-⊎⁺ p) ≡ p
    from∘to (inj₁ (here  p)) = refl
    from∘to (inj₁ (there p)) rewrite from∘to (inj₁ p) = refl
    from∘to (inj₂ (here  q)) = refl
    from∘to (inj₂ (there q)) rewrite from∘to (inj₂ q) = refl

    to∘from : ∀ {n} {xs : Vec A n} (p : Any (λ x → P x ⊎ Q x) xs) →
              Any-⊎⁺ (Any-⊎⁻ p) ≡ p
    to∘from (here (inj₁ p)) = refl
    to∘from (here (inj₂ q)) = refl
    to∘from (there p) with Any-⊎⁻ p | to∘from p
    to∘from (there .(Any.map inj₁ p)) | inj₁ p | refl = refl
    to∘from (there .(Any.map inj₂ q)) | inj₂ q | refl = refl

------------------------------------------------------------------------
-- Products "commute" with Any.

module _ {a b p q} {A : Set a} {B : Set b} {P : Pred A p} {Q : Pred B q} where

  open import Data.Vec.Membership.Propositional using (_∈_; find; lose)

  Any-×⁺ : ∀ {n m} {xs : Vec A n} {ys : Vec B m} → Any P xs × Any Q ys →
           Any (λ x → Any (λ y → P x × Q y) ys) xs
  Any-×⁺ (p , q) = Any.map (λ p → Any.map (p ,_) q) p

  Any-×⁻ : ∀ {n m} {xs : Vec A n} {ys : Vec B m} →
           Any (λ x → Any (λ y → P x × Q y) ys) xs →
           Any P xs × Any Q ys
  Any-×⁻ pq with find pq
  ... | x , x∈xs , pxys with find pxys
  ...   | y , y∈ys , px , py = lose x∈xs px , lose y∈ys py

------------------------------------------------------------------------
-- Invertible introduction (⁺) and elimination (⁻) rules for various
-- vector functions

------------------------------------------------------------------------
-- Singleton ([_])

module _ {a p} {A : Set a} {P : Pred A p} where

  singleton⁺ : ∀ {x} → P x → Any P [ x ]
  singleton⁺ Px = here Px

  singleton⁻ : ∀ {x} → Any P [ x ] → P x
  singleton⁻ (here Px) = Px
  singleton⁻ (there ())

  singleton⁺∘singleton⁻ : ∀ {x} (p : Any P [ x ]) →
                          singleton⁺ (singleton⁻ p) ≡ p
  singleton⁺∘singleton⁻ (here px) = refl
  singleton⁺∘singleton⁻ (there ())

  singleton⁻∘singleton⁺ : ∀ {x} (p : P x) →
                          singleton⁻ (singleton⁺ p) ≡ p
  singleton⁻∘singleton⁺ p = refl

  singleton↔ : ∀ {x} → P x ↔ Any P [ x ]
  singleton↔ = inverse singleton⁺ singleton⁻ singleton⁻∘singleton⁺ singleton⁺∘singleton⁻

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

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

  map⁺ : ∀ {p} {P : B → Set p} {n} {xs : Vec A n} →
         Any (P ∘ f) xs → Any P (map f xs)
  map⁺ (here p)  = here p
  map⁺ (there p) = there $ map⁺ p

  map⁻ : ∀ {p} {P : B → Set p} {n} {xs : Vec A n} →
         Any P (map f xs) → Any (P ∘ f) xs
  map⁻ {xs = []}     ()
  map⁻ {xs = x ∷ xs} (here p)  = here p
  map⁻ {xs = x ∷ xs} (there p) = there $ map⁻ p

  map⁺∘map⁻ : ∀ {p} {P : B → Set p} {n} {xs : Vec A n} →
              (p : Any P (map f xs)) → map⁺ (map⁻ p) ≡ p
  map⁺∘map⁻ {xs = []}     ()
  map⁺∘map⁻ {xs = x ∷ xs} (here  p) = refl
  map⁺∘map⁻ {xs = x ∷ xs} (there p) = P.cong there (map⁺∘map⁻ p)

  map⁻∘map⁺ : ∀ {p} (P : B → Set p) {n} {xs : Vec A n} →
              (p : Any (P ∘ f) xs) → map⁻ {P = P} (map⁺ p) ≡ p
  map⁻∘map⁺ P (here  p) = refl
  map⁻∘map⁺ P (there p) = P.cong there (map⁻∘map⁺ P p)

  map↔ : ∀ {p} {P : B → Set p} {n} {xs : Vec A n} →
         Any (P ∘ f) xs ↔ Any P (map f xs)
  map↔ = inverse map⁺ map⁻ (map⁻∘map⁺ _) map⁺∘map⁻

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

module _ {a p} {A : Set a} {P : A → Set p} where

  ++⁺ˡ : ∀ {n m} {xs : Vec A n} {ys : Vec A m} → Any P xs → Any P (xs ++ ys)
  ++⁺ˡ (here p)  = here p
  ++⁺ˡ (there p) = there (++⁺ˡ p)

  ++⁺ʳ : ∀ {n m} (xs : Vec A n) {ys : Vec A m} → Any P ys → Any P (xs ++ ys)
  ++⁺ʳ []       p = p
  ++⁺ʳ (x ∷ xs) p = there (++⁺ʳ xs p)

  ++⁻ : ∀ {n m} (xs : Vec A n) {ys : Vec A m} → Any P (xs ++ ys) → Any P xs ⊎ Any P ys
  ++⁻ []       p         = inj₂ p
  ++⁻ (x ∷ xs) (here p)  = inj₁ (here p)
  ++⁻ (x ∷ xs) (there p) = Sum.map there id (++⁻ xs p)

  ++⁺∘++⁻ : ∀ {n m} (xs : Vec A n) {ys : Vec A m} (p : Any P (xs ++ ys)) →
           [ ++⁺ˡ , ++⁺ʳ xs ]′ (++⁻ xs p) ≡ p
  ++⁺∘++⁻ []       p         = refl
  ++⁺∘++⁻ (x ∷ xs) (here  p) = refl
  ++⁺∘++⁻ (x ∷ xs) (there p) with ++⁻ xs p | ++⁺∘++⁻ xs p
  ++⁺∘++⁻ (x ∷ xs) (there p) | inj₁ p′ | ih = P.cong there ih
  ++⁺∘++⁻ (x ∷ xs) (there p) | inj₂ p′ | ih = P.cong there ih

  ++⁻∘++⁺ : ∀ {n m} (xs : Vec A n) {ys : Vec A m} (p : Any P xs ⊎ Any P ys) →
            ++⁻ xs ([ ++⁺ˡ , ++⁺ʳ xs ]′ p) ≡ p
  ++⁻∘++⁺ []            (inj₁ ())
  ++⁻∘++⁺ []            (inj₂ p)         = refl
  ++⁻∘++⁺ (x ∷ xs)      (inj₁ (here  p)) = refl
  ++⁻∘++⁺ (x ∷ xs) {ys} (inj₁ (there p)) rewrite ++⁻∘++⁺ xs {ys} (inj₁ p) = refl
  ++⁻∘++⁺ (x ∷ xs)      (inj₂ p)         rewrite ++⁻∘++⁺ xs      (inj₂ p) = refl

  ++↔ : ∀ {n m} {xs : Vec A n} {ys : Vec A m} →
        (Any P xs ⊎ Any P ys) ↔ Any P (xs ++ ys)
  ++↔ {xs = xs} = inverse [ ++⁺ˡ , ++⁺ʳ xs ]′ (++⁻ xs) (++⁻∘++⁺ xs) (++⁺∘++⁻ xs)

  ++-comm : ∀ {n m} (xs : Vec A n) (ys : Vec A m) →
            Any P (xs ++ ys) → Any P (ys ++ xs)
  ++-comm xs ys = [ ++⁺ʳ ys , ++⁺ˡ ]′ ∘ ++⁻ xs

  ++-comm∘++-comm : ∀ {n m} (xs : Vec A n) {ys : Vec A m} (p : Any P (xs ++ ys)) →
                    ++-comm ys xs (++-comm xs ys p) ≡ p
  ++-comm∘++-comm [] {ys} p
    rewrite ++⁻∘++⁺ ys {ys = []} (inj₁ p) = refl
  ++-comm∘++-comm (x ∷ xs) {ys} (here p)
    rewrite ++⁻∘++⁺ ys {ys = x ∷ xs} (inj₂ (here p)) = refl
  ++-comm∘++-comm (x ∷ xs)      (there p) with ++⁻ xs p | ++-comm∘++-comm xs p
  ++-comm∘++-comm (x ∷ xs) {ys} (there .([ ++⁺ʳ xs , ++⁺ˡ ]′ (++⁻ ys (++⁺ʳ ys p))))
    | inj₁ p | refl
    rewrite ++⁻∘++⁺ ys (inj₂                 p)
            | ++⁻∘++⁺ ys (inj₂ $ there {x = x} p) = refl
  ++-comm∘++-comm (x ∷ xs) {ys} (there .([ ++⁺ʳ xs , ++⁺ˡ ]′ (++⁻ ys (++⁺ˡ p))))
    | inj₂ p | refl
    rewrite ++⁻∘++⁺ ys {ys =     xs} (inj₁ p)
            | ++⁻∘++⁺ ys {ys = x ∷ xs} (inj₁ p) = refl

  ++↔++ : ∀ {n m} (xs : Vec A n) (ys : Vec A m) → Any P (xs ++ ys) ↔ Any P (ys ++ xs)
  ++↔++ xs ys = inverse (++-comm xs ys) (++-comm ys xs)
                        (++-comm∘++-comm xs) (++-comm∘++-comm ys)

  ++-insert : ∀ {n m x} (xs : Vec A n) {ys : Vec A m} → P x → Any P (xs ++ [ x ] ++ ys)
  ++-insert xs Px = ++⁺ʳ xs (++⁺ˡ (singleton⁺ Px))

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

module _ {a p} {A : Set a} {P : A → Set p} where

  concat⁺ : ∀ {n m} {xss : Vec (Vec A n) m} → Any (Any P) xss → Any P (concat xss)
  concat⁺ (here p)           = ++⁺ˡ p
  concat⁺ (there {x = xs} p) = ++⁺ʳ xs (concat⁺ p)

  concat⁻ : ∀ {n m} (xss : Vec (Vec A n) m) → Any P (concat xss) → Any (Any P) xss
  concat⁻ []         ()
  concat⁻ (xs ∷ xss) p = [ here , there ∘ concat⁻ xss ]′ (++⁻ xs p)

  concat⁻∘++⁺ˡ : ∀ {n m xs} (xss : Vec (Vec A n) m) (p : Any P xs) →
                concat⁻ (xs ∷ xss) (++⁺ˡ p) ≡ here p
  concat⁻∘++⁺ˡ xss p rewrite ++⁻∘++⁺ _ {concat xss} (inj₁ p) = refl

  concat⁻∘++⁺ʳ : ∀ {n m} xs (xss : Vec (Vec A n) m) (p : Any P (concat xss)) →
                concat⁻ (xs ∷ xss) (++⁺ʳ xs p) ≡ there (concat⁻ xss p)
  concat⁻∘++⁺ʳ xs xss p rewrite ++⁻∘++⁺ xs (inj₂ p) = refl

  concat⁺∘concat⁻ : ∀ {n m} (xss : Vec (Vec A n) m) (p : Any P (concat xss)) →
                   concat⁺ (concat⁻ xss p) ≡ p
  concat⁺∘concat⁻ []         ()
  concat⁺∘concat⁻ (xs ∷ xss) p  with ++⁻ xs p | P.inspect (++⁻ xs) p
  ... | inj₁ pxs | P.[ p=inj₁ ]
    = P.trans (P.cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (P.sym p=inj₁))
    $ ++⁺∘++⁻ xs p
  ... | inj₂ pxss | P.[ p=inj₂ ] rewrite concat⁺∘concat⁻ xss pxss
    = P.trans (P.cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (P.sym p=inj₂))
    $ ++⁺∘++⁻ xs p

  concat⁻∘concat⁺ : ∀ {n m} {xss : Vec (Vec A n) m} (p : Any (Any P) xss) →
                    concat⁻ xss (concat⁺ p) ≡ p
  concat⁻∘concat⁺ {xss = xs ∷ xss} (here p)
    rewrite ++⁻∘++⁺ xs {concat xss} (inj₁ p) = refl
  concat⁻∘concat⁺ {xss = xs ∷ xss} (there p)
    rewrite ++⁻∘++⁺ xs {concat xss} (inj₂ (concat⁺ p))
            | concat⁻∘concat⁺ p = refl

  concat↔ : ∀ {n m} {xss : Vec (Vec A n) m} → Any (Any P) xss ↔ Any P (concat xss)
  concat↔ {xss = xss} = inverse concat⁺ (concat⁻ xss) concat⁻∘concat⁺ (concat⁺∘concat⁻ xss)

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

module _ {a p} {A : Set a} {P : A → Set p} where

  tabulate⁺ : ∀ {n} {f : Fin n → A} i → P (f i) → Any P (tabulate f)
  tabulate⁺ fzero    p = here p
  tabulate⁺ (fsuc i) p = there (tabulate⁺ i p)

  tabulate⁻ : ∀ {n} {f : Fin n → A} →
              Any P (tabulate f) → ∃ λ i → P (f i)
  tabulate⁻ {zero}  ()
  tabulate⁻ {suc n} (here p)  = fzero , p
  tabulate⁻ {suc n} (there p) = Prod.map fsuc id (tabulate⁻ p)

------------------------------------------------------------------------
-- mapWith∈

module _ {a b p} {A : Set a} {B : Set b} {P : B → Set p} where

  open import Data.Vec.Membership.Propositional using (_∈_; mapWith∈)

  mapWith∈⁺ : ∀ {n} {xs : Vec A n} (f : ∀ {x} → x ∈ xs → B) →
              (∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) →
              Any P (mapWith∈ xs f)
  mapWith∈⁺ f (_ , here refl  , p) = here p
  mapWith∈⁺ f (_ , there x∈xs , p) =
    there $ mapWith∈⁺ (f ∘ there) (_ , x∈xs , p)

  mapWith∈⁻ : ∀ {n} (xs : Vec A n) (f : ∀ {x} → x ∈ xs → B) →
              Any P (mapWith∈ xs f) →
              ∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)
  mapWith∈⁻ []       f ()
  mapWith∈⁻ (y ∷ xs) f (here  p) = (y , here refl , p)
  mapWith∈⁻ (y ∷ xs) f (there p) =
    Prod.map id (Prod.map there id) $ mapWith∈⁻ xs (f ∘ there) p

  mapWith∈↔ : ∀ {n} {xs : Vec A n} {f : ∀ {x} → x ∈ xs → B} →
    (∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) ↔ Any P (mapWith∈ xs f)
  mapWith∈↔ = inverse (mapWith∈⁺ _) (mapWith∈⁻ _ _) (from∘to _) (to∘from _ _)
    where
    from∘to : ∀ {n} {xs : Vec A n} (f : ∀ {x} → x ∈ xs → B)
              (p : ∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) →
              mapWith∈⁻ xs f (mapWith∈⁺ f p) ≡ p
    from∘to f (_ , here refl  , p) = refl
    from∘to f (_ , there x∈xs , p)
      rewrite from∘to (f ∘ there) (_ , x∈xs , p) = refl

    to∘from : ∀ {n} (xs : Vec A n) (f : ∀ {x} → x ∈ xs → B)
              (p : Any P (mapWith∈ xs f)) →
              mapWith∈⁺ f (mapWith∈⁻ xs f p) ≡ p
    to∘from []       f ()
    to∘from (y ∷ xs) f (here  p) = refl
    to∘from (y ∷ xs) f (there p) =
      P.cong there $ to∘from xs (f ∘ there) p

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

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

  ∷↔ : ∀ {n} (P : Pred A p) {x} {xs : Vec A n} → (P x ⊎ Any P xs) ↔ Any P (x ∷ xs)
  ∷↔ P {x} {xs} = ++↔ ∘↔ (singleton↔ ⊎-cong id↔)

------------------------------------------------------------------------
-- _>>=_

module _ {ℓ p} {A B : Set ℓ} {P : B → Set p} {m} {f : A → Vec B m} where

  >>=↔ : ∀ {n} {xs : Vec A n} → Any (Any P ∘ f) xs ↔ Any P (xs >>= f)
  >>=↔ = concat↔ ∘↔ map↔


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

open import Cubical.Core.Everything
open import Cubical.Foundations.HLevels

module Cubical.Algebra.Magma.Construct.Right {ℓ} (Aˢ : hSet ℓ) where

open import Cubical.Foundations.Prelude
open import Cubical.Algebra.Magma

private
  A = ⟨ Aˢ ⟩
  isSetA = Aˢ .snd

_▸_ : Op₂ A
x ▸ y = y

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

▸-identityˡ : ∀ x → LeftIdentity x _▸_
▸-identityˡ _ _ = refl

▸-zeroʳ : ∀ x → RightZero x _▸_
▸-zeroʳ _ _ = refl

------------------------------------------------------------------------
-- Magma definition

Right-isMagma : IsMagma A _▸_
Right-isMagma = record { is-set = isSetA }

RightMagma : Magma ℓ
RightMagma = record { isMagma = Right-isMagma }


text:
module Foundation.Equivalence where

open import Foundation.Primitive

record IsEquivalence {a} {A : Set a} {ℓ} (_≈_ : A → A → Set ℓ) : ℞ a ⊔ ℓ where
  field
    reflexivity : ∀ x → x ≈ x
    symmetry : ∀ x y → x ≈ y → y ≈ x
    transitivity : ∀ x y z → x ≈ y → y ≈ z → x ≈ z

open IsEquivalence ⦃ … ⦄ public

record Equivalence {a} (A : Set a) ℓ : ℞ a ⊔ ⟰ ℓ where
  infix 4 _≈_
  field
    _≈_ : A → A → Set ℓ
    instance ⦃ isEquivalence ⦄ : IsEquivalence _≈_

open Equivalence ⦃ … ⦄ public

open import Foundation.Bottom

infix 4 _≉_
_≉_ : ∀ {a} {A : Set a} {ℓ} ⦃ _ : Equivalence A ℓ ⦄ {b} ⦃ _ : Bottom b ℓ  ⦄ → A → A → Set (b ⊔ ℓ)
_≉_ {ℓ = ℓ} x y = ¬ (x ≈ y)


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

module Cubical.Categories.Morphism where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Categories.Category

private
  variable
    ℓ ℓ' : Level

module _ {C : Precategory ℓ ℓ'} where
  open Precategory C
  private
    variable
      x y z w : ob

  isMonic : (Hom[ x , y ]) → Type (ℓ-max ℓ ℓ')
  isMonic {x} {y} f = ∀ {z : ob} {a a' : Hom[ z , x ]}
    → (f ∘ a ≡ f ∘ a') → (a ≡ a')

  isEpic : (Hom[ x , y ]) → Type (ℓ-max ℓ ℓ')
  isEpic {x} {y} g = ∀ {z : ob} {b b' : Hom[ y , z ]}
    → (b ∘ g ≡ b' ∘ g) → (b ≡ b')

  -- A morphism is split monic if it has a *retraction*
  isSplitMon : (Hom[ x , y ]) → Type ℓ'
  isSplitMon {x} {y} f = ∃[ r ∈ Hom[ y , x ] ] r ∘ f ≡ id x

  -- A morphism is split epic if it has a *section*
  isSplitEpi : (Hom[ x , y ]) → Type ℓ'
  isSplitEpi {x} {y} g = ∃[ s ∈ Hom[ y , x ] ] g ∘ s ≡ id y

  record areInv (f : Hom[ x , y ]) (g : Hom[ y , x ]) : Type ℓ' where
    field
      sec : g ⋆ f ≡ id y
      ret : f ⋆ g ≡ id x

  open areInv

  symAreInv : ∀ {f : Hom[ x , y ]} {g : Hom[ y , x ]}
            → areInv f g
            → areInv g f
  symAreInv record { sec = sec ; ret = ret } = record { sec = ret ; ret = sec }

  -- equational reasoning with inverses
  invMoveR : ∀ {f : Hom[ x , y ]} {g : Hom[ y , x ]} {h : Hom[ z , x ]} {k : Hom[ z , y ]}
           → areInv f g
           → h ⋆ f ≡ k
           → h ≡ k ⋆ g
  invMoveR {f = f} {g} {h} {k} ai p
    = h
    ≡⟨ sym (⋆IdR _) ⟩
      (h ⋆ id _)
    ≡⟨ cong (h ⋆_) (sym (ai .ret)) ⟩
      (h ⋆ (f ⋆ g))
    ≡⟨ sym (⋆Assoc _ _ _) ⟩
      ((h ⋆ f) ⋆ g)
    ≡⟨ cong (_⋆ g) p ⟩
      k ⋆ g
    ∎

  invMoveL : ∀ {f : Hom[ x , y ]} {g : Hom[ y , x ]} {h : Hom[ y , z ]} {k : Hom[ x , z ]}
          → areInv f g
          → f ⋆ h ≡ k
          → h ≡ g ⋆ k
  invMoveL {f = f} {g} {h} {k} ai p
    = h
    ≡⟨ sym (⋆IdL _) ⟩
      id _ ⋆ h
    ≡⟨ cong (_⋆ h) (sym (ai .sec)) ⟩
      (g ⋆ f) ⋆ h
    ≡⟨ ⋆Assoc _ _ _ ⟩
      g ⋆ (f ⋆ h)
    ≡⟨ cong (g ⋆_) p ⟩
      (g ⋆ k)
    ∎

  record isIso (f : Hom[ x , y ]) : Type ℓ' where
    field
      inv : Hom[ y , x ]
      sec : inv ⋆ f ≡ id y
      ret : f ⋆ inv ≡ id x

  open isIso

  isIso→areInv : ∀ {f : Hom[ x , y ]}
               → (isI : isIso f)
               → areInv f (isI .inv)
  isIso→areInv record { inv = inv ; sec = sec ; ret = ret } = record { sec = sec ; ret = ret }

  open CatIso

  -- isIso agrees with CatIso
  isIso→CatIso : ∀ {f : C [ x , y ]}
               → isIso f
               → CatIso {C = C} x y
  isIso→CatIso {f = f} record { inv = f⁻¹ ; sec = sec ; ret = ret } = catiso f f⁻¹ sec ret

  CatIso→isIso : (cIso : CatIso {C = C} x y)
               → isIso (cIso .mor)
  CatIso→isIso (catiso mor inv sec ret) = record { inv = inv ; sec = sec ; ret = ret }

  CatIso→areInv : (cIso : CatIso {C = C} x y)
                → areInv (cIso .mor) (cIso .inv)
  CatIso→areInv cIso = isIso→areInv (CatIso→isIso cIso)

  -- reverse of an iso is also an iso
  symCatIso : ∀ {x y}
             → CatIso {C = C} x y
             → CatIso {C = C} y x
  symCatIso (catiso mor inv sec ret) = catiso inv mor ret sec

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Structure.Real where

import      Lvl
open import Data.Boolean
open import Data.Boolean.Proofs
import      Data.Either as Either
open import Functional
open import Logic
open import Logic.Classical
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Natural using (ℕ)
import      Numeral.Natural.Relation.Order as ℕ
open import Relator.Ordering
open import Structure.Setoid
open import Structure.Function.Ordering
open import Structure.Operator.Field
open import Structure.Operator.Monoid
open import Structure.Operator.Group
open import Structure.Operator.Proofs
open import Structure.Operator.Properties
open import Structure.Relator.Ordering
open        Structure.Relator.Ordering.Weak.Properties
open import Structure.Relator.Properties
open import Structure.OrderedField
import      Structure.OrderedField.AbsoluteValue
open import Syntax.Transitivity
open import Type

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

-- Theory defining the axioms of ℝ in classical logic.
-- The axioms are the following:
-- • An ordered field.
-- • Monotone convergence.
record RealTheory {R : Type{ℓ₁}} ⦃ equiv-R : Equiv{ℓₑ}(R) ⦄ (_+_ _⋅_ : R → R → R) (_≤_ : R → R → Stmt{ℓ₂}) ⦃ classical : ∀{ℓ}{P : Stmt{ℓ}} → Classical(P) ⦄ : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓₑ} where
  field
    ⦃ orderedField ⦄ : OrderedField(_+_)(_⋅_)(_≤_)

  open OrderedField(orderedField) public
  open Structure.OrderedField.AbsoluteValue(_+_)(_⋅_)(_≤_)

  field
    sup-fn : (f : ℕ → R) → ⦃ Increasing(ℕ._≤_)(_≤_)(f) ⦄ → ⦃ UpperBounded(ℕ._≤_)(_≤_)(f) ⦄ → R
    monotone-convergence : ∀{f} → ⦃ inc : Increasing(ℕ._≤_)(_≤_)(f) ⦄ → ⦃ bound : UpperBounded(ℕ._≤_)(_≤_)(f) ⦄ → ∃{Obj = R → ℕ}(N ↦ ∀{ε} → (ε > 𝟎) → ∀{n} → (n ℕ.> N(ε)) → (‖ f(n) − sup-fn (f) ⦃ inc ⦄ ⦃ bound ⦄ ‖ < ε))

  -- TODO: Consider adding something that relates addition and multiplication so that it conform to the axioms of arithmetic and their definitions of addition and multiplication. This is so that one should be able to prove (x + x ≡ 𝐒(𝐒(𝟎)) ⋅ x) or (2.5 ⋅ x = x + x + x/2) (when 𝐒, the successor function is defined as (1 +_)) for easier to write statements. In other words: add ((1 + x) ⋅ y = x + (x ⋅ y)) as an axiom. (20201210 Is this TODO outdated?)

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:
Id₁ Id₂ Id₃ : {A B : Set} → (A → B) → A → B
Id₁ F = F
Id₂ = Id₁
Id₃ = Id₁

syntax Id₁ (λ X → B) = ƛ X ⟶ B
syntax Id₂ (λ X → B) = X ↦ B
syntax Id₃ (λ X → B) = X ↦ B •

postulate
  A : Set
  a : A

module One where

  example₀ : (A → A) → A
  example₀ = ƛ _ ⟶ a

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

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

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

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

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

  example₆ : (A → A → A) → (A → A → A)
  example₆ = ƛ !_!_ ⟶ λ a b → ! a ! b

  example₇ : (A → A → A) → (A → A → A)
  example₇ = ƛ _!_! ⟶ λ a b → a ! b !

  example₈ : (A → A → A → A → A) → (A → A → A → A → A)
  example₈ = ƛ _!_!_!_ ⟶ λ a b c → a !_! b ! c

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

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

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

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

module Two where

  example₀ : (A → A) → A
  example₀ = _ ↦ a

  example₁ : A → A
  example₁ = !_! ↦ (!_!)

  example₂ : A → A
  example₂ = !_!_ ↦ (!_!_)

  example₃ : A → A
  example₃ = _!_! ↦ (_!_!)

  example₄ : A → A
  example₄ = _!_!_!_ ↦ (_!_!_!_)

  example₅ : (A → A) → (A → A)
  example₅ = !_! ↦ λ a → ! a !

  example₆ : (A → A → A) → (A → A → A)
  example₆ = !_!_ ↦ λ a b → ! a ! b

  example₇ : (A → A → A) → (A → A → A)
  example₇ = _!_! ↦ λ a b → a ! b !

  example₈ : (A → A → A → A → A) → (A → A → A → A → A)
  example₈ = _!_!_!_ ↦ λ a b c → a !_! b ! c

  example₉ : (A → A) → A
  example₉ = !_! ↦ (! a !)

  example₁₀ : (A → A → A) → A
  example₁₀ = !_!_ ↦ (! a ! a)

  example₁₁ : (A → A → A) → A
  example₁₁ = _!_! ↦ (a ! a !)

  example₁₂ : (A → A → A → A → A) → (A → A)
  example₁₂ = _!_!_!_ ↦ (a ! a !_! a)

module Three where

  example₀ : (A → A) → A
  example₀ = _ ↦ a •

  example₁ : A → A
  example₁ = !_! ↦ (!_!) •

  example₂ : A → A
  example₂ = !_!_ ↦ (!_!_) •

  example₃ : A → A
  example₃ = _!_! ↦ (_!_!) •

  example₄ : A → A
  example₄ = _!_!_!_ ↦ (_!_!_!_) •

  example₅ : (A → A) → (A → A)
  example₅ = !_! ↦ (λ a → ! a !) •

  example₆ : (A → A → A) → (A → A → A)
  example₆ = !_!_ ↦ (λ a b → ! a ! b) •

  example₇ : (A → A → A) → (A → A → A)
  example₇ = _!_! ↦ (λ a b → a ! b !) •

  example₈ : (A → A → A → A → A) → (A → A → A → A → A)
  example₈ = _!_!_!_ ↦ (λ a b c → a !_! b ! c) •

  example₉ : (A → A) → A
  example₉ = !_! ↦ (! a !) •

  example₁₀ : (A → A → A) → A
  example₁₀ = !_!_ ↦ (! a ! a) •

  example₁₁ : (A → A → A) → A
  example₁₁ = _!_! ↦ (a ! a !) •

  example₁₂ : (A → A → A → A → A) → (A → A)
  example₁₂ = _!_!_!_ ↦ (a ! a !_! a) •

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --universe-polymorphism #-}

-- Support stuff mostly stolen or adapted from the Agda standard library

module Support where

data Level : Set where
  zero : Level
  suc  : (i : Level) → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}

-- Maximum.

infixl 6 _⊔_
infixr 2 _×_

_⊔_ : Level → Level → Level
zero  ⊔ j     = j
suc i ⊔ zero  = suc i
suc i ⊔ suc j = suc (i ⊔ j)

{-# BUILTIN LEVELMAX _⊔_ #-}

infix 4 _≣_

data _≣_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
  ≣-refl : x ≣ x

{-# BUILTIN EQUALITY _≣_ #-}
{-# BUILTIN REFL ≣-refl #-}

≣-trans : ∀ {a} {A : Set a} → ∀ {x y z : A} → y ≣ z → x ≣ y → x ≣ z
≣-trans ≣-refl ≣-refl = ≣-refl

≣-sym : ∀ {a} {A : Set a} → ∀ {x y : A} → x ≣ y → y ≣ x
≣-sym ≣-refl = ≣-refl

≣-subst : ∀ {a p} {A : Set a} → (P : A → Set p) → ∀ {x y} → x ≣ y → P x → P y
≣-subst P ≣-refl x = x

≣-subst₂ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p)
           {x₁ x₂ y₁ y₂} → x₁ ≣ x₂ → y₁ ≣ y₂ → P x₁ y₁ → P x₂ y₂
≣-subst₂ P ≣-refl ≣-refl p = p

≣-cong : ∀ {a b} {A : Set a} {B : Set b}
         (f : A → B) {x y} → x ≣ y → f x ≣ f y
≣-cong f ≣-refl = ≣-refl

≣-cong₂ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
          (f : A → B → C) {x y u v} → x ≣ y → u ≣ v → f x u ≣ f y v
≣-cong₂ f ≣-refl ≣-refl = ≣-refl

infixr 4 _,_

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃ = Σ _

∃₂ : ∀ {a b c} {A : Set a} {B : A → Set b}
     (C : (x : A) → B x → Set c) → Set (a ⊔ b ⊔ c)
∃₂ C = ∃ λ a → ∃ λ b → C a b

record Σ′ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁′ : A
    .proj₂′ : B proj₁′

open Σ′ public

∃′ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃′ = Σ′ _

∃₂′ : ∀ {a b c} {A : Set a} {B : A → Set b}
     (C : (x : A) → B x → Set c) → Set (a ⊔ b ⊔ c)
∃₂′ C = ∃ λ a → ∃′ λ b → C a b

record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B

open _×_ public

⟨_,_⟩ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} → (A → B) → (C → D) → A × C → B × D
⟨ f , g ⟩ (x , y) = f x , g y

⟨_&_⟩ : ∀ {a b d} {A : Set a} {B : Set b} {D : Set d} → (A → B) → (A → D) → A → B × D
⟨ f & g ⟩ x = f x , g x

_∙_ : ∀ {a b c}
        {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f ∙ g = λ x → f (g x)

∙-assoc : ∀ {a b c d} {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} {D : {x : A} {y : B x} → C y → Set d} → (f : ∀ {x} {y : B x} (z : C y) → D z) → (g : ∀ {x} (y : B x) → C y) → (h : (x : A) → B x) → {x : A} → (f ∙ (g ∙ h)) x ≣ ((f ∙ g) ∙ h) x
∙-assoc f g h {x} = ≣-refl

_∙′_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
       (B → C) → (A → B) → (A → C)
f ∙′ g = _∙_ f g

_∙₂_ : ∀ {a b c d}
         {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c}
         {D : {x : A} {y : B x} → C y → Set d} →
      (∀ {x} {y : B x} (z : C y) → D z) → (g : (x : A) (y : B x) → C y) →
      ((x : A) (y : B x) → D (g x y))
f ∙₂ g = λ x y → f (g x y)

_∙₃_ : ∀ {a b c d e}
         {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c}
         {D : {x : A} {y : B x} → C y → Set d}
         {E : {x : A} {y : B x} {z : C y} → D z → Set e} →
      (∀ {x} {y : B x} {z : C y} (w : D z) → E w) →
      (g : (x : A) (y : B x) (z : C y) → D z) →
      ((x : A) (y : B x) (z : C y) → E (g x y z))
f ∙₃ g = λ x y z → f (g x y z)

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

_$↑_ : ∀ {a b c}
         {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
       (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
       ((x : A) → C (g x))
_$↑_ = _∙_

_$⇈_ : ∀ {ℓ a b}
          {T : Set ℓ} {A : T → Set a} {B : (i : T) → (x : A i) → Set b} →
       (f : (i : T) → ∀ (x : A i) → B i x) → (x : (i : T) → A i) →
       ((i : T) → B i (x i))
f $⇈ x = λ i → f i (x i)

{- John Major equality would be nice for stating this result ... -}
$⇈-obs : ∀ {ℓ a b}
           {T : Set ℓ} {A : T → Set a} {B : (i : T) → (x : A i) → Set b} →
         {f f′ : (i : T) → ∀ (x : A i) → B i x}
           (eq-f : ∀ {i} {x : A i} → f i x ≣ f′ i x) →
         {x x′ : (i : T) → A i} (eq-x : ∀ {i} → x i ≣ x′ i) →
         ∀ {i} → (≣-subst (B i) (eq-x {i}) ((f $⇈ x) i) ≣ (f′ $⇈ x′) i)
$⇈-obs eq-f {x} {x′} eq-x {i} rewrite eq-x {i} | eq-f {i} {x′ i} = ≣-refl

lift↑ : ∀ {ℓ a b}
          {T : Set ℓ} {A : T → Set a} {B : (i : T) → A i → Set b} →
        (f : ∀ {i} (x : A i) → B i x) → (x : (i : T) → A i) →
        ((i : T) → B i (x i))
lift↑ = _$↑_

lift↑₂ : ∀ {ℓ a b c}
           {T : Set ℓ} {A : T → Set a} {B : (i : T) → Set b}
           {C : (i : T) → A i → B i → Set c} →
         (f : ∀ {i} (x : A i) (y : B i) → C i x y) →
         (x : (i : T) → A i) (y : (i : T) → B i) →
         ((i : T) → C i (x i) (y i))
lift↑₂ = λ f x y → (lift↑ f x) $⇈ y

Rel : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
Rel A ℓ = A → A → Set ℓ

private
  _⇒_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} →
       Rel A ℓ₁ → Rel A ℓ₂ → Set _
  P ⇒ Q = ∀ {i j} → P i j → Q i j

_Respects_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → (A → Set ℓ₁) → Rel A ℓ₂ → Set _
P Respects _∼_ = ∀ {x y} → x ∼ y → P x → P y

_Respects₂_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
P Respects₂ _∼_ =
  (∀ {x} → P x      Respects _∼_) ×
  (∀ {y} → flip P y Respects _∼_)

record IsEquivalence {a ℓ} {A : Set a}
                     (_≈_ : Rel A ℓ) : Set (a ⊔ ℓ) where
  field
    refl  : ∀ {x} → x ≈ x
    sym   : ∀ {x y} → x ≈ y → y ≈ x
    trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z

  -- a helper to promote propositional equality to equivalence
  .prop : ∀ {x y} → x ≣ y → x ≈ y
  prop ≣-refl = refl

record IsPreorder {a ℓ₁ ℓ₂} {A : Set a}
                  (_≈_ : Rel A ℓ₁) -- The underlying equality.
                  (_∼_ : Rel A ℓ₂) -- The relation.
                  : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isEquivalence : IsEquivalence _≈_
    -- Reflexivity is expressed in terms of an underlying equality:
    reflexive     : _≈_ ⇒ _∼_
    trans         : ∀ {x y z} → x ∼ y → y ∼ z → x ∼ z

  module Eq = IsEquivalence isEquivalence

  refl : ∀ {x} → x ∼ x
  refl = reflexive Eq.refl

  ∼-resp-≈ : _∼_ Respects₂ _≈_
  ∼-resp-≈ = (λ x≈y z∼x → trans z∼x (reflexive x≈y))
           , (λ x≈y x∼z → trans (reflexive (Eq.sym x≈y)) x∼z)

record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _∼_
  field
    Carrier    : Set c
    _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
    _∼_        : Rel Carrier ℓ₂  -- The relation.
    isPreorder : IsPreorder _≈_ _∼_

  open IsPreorder isPreorder public

record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infix 4 _≈_
  field
    Carrier       : Set c
    _≈_           : Rel Carrier ℓ
    .isEquivalence : IsEquivalence _≈_

record SetoidFunction {c ℓ c′ ℓ′} (X : Setoid c ℓ) (Y : Setoid c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′ ⊔ ℓ′) where
  field
    F : Setoid.Carrier X → Setoid.Carrier Y
    .cong : ∀ {x y} → Setoid._≈_ X x y → Setoid._≈_ Y (F x) (F y)

module SetoidReasoning {s₁ s₂} (S : Setoid s₁ s₂) where
  open Setoid S

  infix  4 _IsRelatedTo_
  infix  2 _∎
  infixr 2 _≈⟨_⟩_
  infixr 2 _↓⟨_⟩_
  infixr 2 _↑⟨_⟩_
  infixr 2 _↓≣⟨_⟩_
  infixr 2 _↑≣⟨_⟩_
  infixr 2 _↕_
  infix  1 begin_

  -- This seemingly unnecessary type is used to make it possible to
  -- infer arguments even if the underlying equality evaluates.

  data _IsRelatedTo_ (x y : Carrier) : Set s₂ where
    relTo : (x∼y : x ≈ y) → x IsRelatedTo y

  .begin_ : ∀ {x y} → x IsRelatedTo y → x ≈ y
  begin relTo x∼y = x∼y

  ._↓⟨_⟩_ : ∀ x {y z} → x ≈ y → y IsRelatedTo z → x IsRelatedTo z
  _ ↓⟨ x∼y ⟩ relTo y∼z = relTo (trans x∼y y∼z)
    where open IsEquivalence isEquivalence

  ._↑⟨_⟩_ : ∀ x {y z} → y ≈ x → y IsRelatedTo z → x IsRelatedTo z
  _ ↑⟨ y∼x ⟩ relTo y∼z = relTo (trans (sym y∼x) y∼z)
    where open IsEquivalence isEquivalence

  -- the syntax of the ancients, for compatibility
  ._≈⟨_⟩_ : ∀ x {y z} → x ≈ y → y IsRelatedTo z → x IsRelatedTo z
  _≈⟨_⟩_ = _↓⟨_⟩_

  ._↓≣⟨_⟩_ : ∀ x {y z} → x ≣ y → y IsRelatedTo z → x IsRelatedTo z
  _ ↓≣⟨ ≣-refl ⟩ y∼z = y∼z

  ._↑≣⟨_⟩_ : ∀ x {y z} → y ≣ x → y IsRelatedTo z → x IsRelatedTo z
  _ ↑≣⟨ ≣-refl ⟩ y∼z = y∼z

  ._↕_ : ∀ x {z} → x IsRelatedTo z → x IsRelatedTo z
  _ ↕ x∼z = x∼z

  ._∎ : ∀ x → x IsRelatedTo x
  _∎ _ = relTo refl
    where open IsEquivalence isEquivalence

≣-is-equivalence : ∀ {ℓ} (A : Set ℓ) → IsEquivalence (_≣_ {A = A})
≣-is-equivalence A = record { refl = λ {x} → ≣-refl
                            ; sym = λ {x} {y} → ≣-sym
                            ; trans = λ {x} {y} {z} → flip ≣-trans }

SetAsSetoid : ∀ {ℓ} (A : Set ℓ) → Setoid ℓ ℓ
SetAsSetoid A = record { Carrier = A
                       ; _≈_ = _≣_
                       ; isEquivalence = ≣-is-equivalence A }

module ≣-reasoning {ℓ} (S : Set ℓ) where
  infix  4 _IsRelatedTo_
  infix  2 _∎
  infixr 2 _≈⟨_⟩_
  infixr 2 _↓⟨_⟩_
  infixr 2 _↑⟨_⟩_
  infixr 2 _↕_
  infix  1 begin_

  -- This seemingly unnecessary type is used to make it possible to
  -- infer arguments even if the underlying equality evaluates.

  data _IsRelatedTo_ (x y : S) : Set ℓ where
    relTo : (x∼y : x ≣ y) → x IsRelatedTo y

  begin_ : ∀ {x y} → x IsRelatedTo y → x ≣ y
  begin relTo x∼y = x∼y

  -- the syntax of the ancients, for compatibility
  _≈⟨_⟩_ : ∀ x {y z} → x ≣ y → y IsRelatedTo z → x IsRelatedTo z
  _ ≈⟨ x∼y ⟩ relTo y∼z = relTo (≣-trans y∼z x∼y)

  _↓⟨_⟩_ : ∀ x {y z} → x ≣ y → y IsRelatedTo z → x IsRelatedTo z
  _ ↓⟨ x∼y ⟩ relTo y∼z = relTo (≣-trans y∼z x∼y)

  _↑⟨_⟩_ : ∀ x {y z} → y ≣ x → y IsRelatedTo z → x IsRelatedTo z
  _ ↑⟨ y∼x ⟩ relTo y∼z = relTo (≣-trans y∼z (≣-sym y∼x))

  _↕_ : ∀ x {z} → x IsRelatedTo z → x IsRelatedTo z
  _ ↕ x∼z = x∼z

  _∎ : ∀ x → x IsRelatedTo x
  _∎ _ = relTo ≣-refl

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

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}

data Fin : ℕ → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

data ⊥ : Set where

¬_ : ∀ {a} (A : Set a) → Set a
¬ A = A → ⊥

record ⊤ {ℓ} : Set ℓ where
  constructor tt

type-signature : ∀ {a} (A : Set a) → A → A
type-signature A x = x

syntax type-signature A x = x ∶ A

data Either {l r : Level} (L : Set l) (R : Set r) : Set (l ⊔ r) where
  inl : L → Either L R
  inr : R → Either L R

either₀ : ∀ {l r ℓ : Level} {L : Set l} {R : Set r} {A : Set ℓ} (f : L → A) (g : R → A) (v : Either L R) → A
either₀ f _ (inl x) = f x
either₀ _ g (inr y) = g y

∙-dist-either₀ : ∀ {l r ℓ ℓ′} {L : Set l} {R : Set r} {A : Set ℓ} {A′ : Set ℓ′} (f : L → A) (g : R → A) (h : A → A′) {v : Either L R} → (h ∙ either₀ f g) v ≣ either₀ (h ∙ f) (h ∙ g) v
∙-dist-either₀ f g h {inl y} = ≣-refl
∙-dist-either₀ f g h {inr y} = ≣-refl

either₀-obsˡ : ∀ {l r ℓ : Level} {L : Set l} {R : Set r} {A : Set ℓ}
                 {f : L → A} {f′ : L → A}
               (eq : ∀ {x} → f x ≣ f′ x) (g : R → A) →
               ∀ {v} → (either₀ f g v ≣ either₀ f′ g v)
either₀-obsˡ eq g {inl y} = eq
either₀-obsˡ eq g {inr y} = ≣-refl

either₀-obsʳ : ∀ {l r ℓ : Level} {L : Set l} {R : Set r} {A : Set ℓ}
                 {g : R → A} {g′ : R → A}
               (f : L → A) (eq : ∀ {x} → g x ≣ g′ x) →
               ∀ {v} → (either₀ f g v ≣ either₀ f g′ v)
either₀-obsʳ f eq {inl y} = ≣-refl
either₀-obsʳ f eq {inr y} = eq

either₀-correlate : ∀ {l r ℓ ℓ′ : Level} {L : Set l} {R : Set r} {A : Set ℓ} {A′ : Set ℓ′ } (f : L → A′ → A) (g : R → A′ → A) (f′ : L → A′) (g′ : R → A′) (v : Either L R) → either₀ (either₀ f g v ∙ f′) (either₀ f g v ∙ g′) v ≣ either₀ (f $⇈ f′) (g $⇈ g′) v
either₀-correlate f g f′ g′ (inl v) = ≣-refl
either₀-correlate f g f′ g′ (inr v) = ≣-refl

either : ∀ {l r ℓ} {L : Set l} {R : Set r} {L′ : L → Set ℓ} {R′ : R → Set ℓ} (f : (x : L) → L′ x) (g : (y : R) → R′ y) (v : Either L R) → either₀ L′ R′ v
either f _ (inl x) = f x
either _ g (inr y) = g y

either′ : ∀ {l r ℓ} {L : Set l} {R : Set r} {A : Either L R → Set ℓ} (f : (x : L) → A (inl x)) (g : (y : R) → A (inr y)) (v : Either L R) → A v
either′ f _ (inl x) = f x
either′ _ g (inr y) = g y

left : ∀ {l l′ r} {L : Set l} {R : Set r} {L′ : Set l′} (f : L → L′) (v : Either L R) → Either L′ R
left f (inl x) = inl (f x)
left _ (inr y) = inr y

right : ∀ {l r r′} {L : Set l} {R : Set r} {R′ : Set r′} (g : R → R′) (v : Either L R) → Either L R′
right _ (inl x) = inl x
right g (inr y) = inr (g y)

_+++_ : ∀ {l l′} {L : Set l} {L′ : Set l′} (f : L → L′) {r r′} {R : Set r} {R′ : Set r′} (g : R → R′) (v : Either L R) → Either L′ R′
(f +++ _) (inl x) = inl (f x)
(_ +++ g) (inr y) = inr (g y)

uncurry₀ : ∀ {x y z} {X : Set x} {Y : Set y} {Z : Set z} (f : X → Y → Z) → X × Y → Z
uncurry₀ f (x , y) = f x y

∙-commute-uncurry₀ : ∀ {x y z z′} {X : Set x} {Y : Set y} {Z : Set z} {Z′ : Set z′} (g : Z → Z′) (f : X → Y → Z) → (g ∙ uncurry₀ f) ≣ uncurry₀ (g ∙₂ f)
∙-commute-uncurry₀ g f = ≣-refl

∙₂-commute-uncurry₀ : ∀ {x y z w w′} {X : Set x} {Y : Set y} {Z : Set z} {W : Set w} {W′ : Set w′} (g : W → W′) (f : X → Y → Z → W) → (g ∙₂ uncurry₀ f) ≣ uncurry₀ (g ∙₃ f)
∙₂-commute-uncurry₀ g f = ≣-refl

uncurry₀-obs : ∀ {x y z} {X : Set x} {Y : Set y} {Z : Set z} {f : X → Y → Z} → (f-obs : ∀ {x x′ y y′} → x ≣ x′ → y ≣ y′ → f x y ≣ f x′ y′) {x,y x,y′ : X × Y} (eq : x,y ≣ x,y′) → uncurry₀ f x,y ≣ uncurry₀ f x,y′
uncurry₀-obs f-obs eq rewrite f-obs (≣-cong fst eq) (≣-cong snd eq) = ≣-refl

uncurry₀-obs′₁ : ∀ {x y z w} {X : Set x} {Y : Set y} {Z : Set z} {W : Z → Set w} {f f′ : X → Y → (c : Z) → W c} → (∀ a b c → f a b c ≣ f′ a b c) → ∀ a,b c → uncurry₀ f a,b c ≣ uncurry₀ f′ a,b c
uncurry₀-obs′₁ f-obs a,b c rewrite f-obs (fst a,b) (snd a,b) c = ≣-refl

uncurry : ∀ {x y z} {X : Set x} {Y : Set y} {Z : X → Y → Set z} (f : (x : X) → (y : Y) → Z x y) → (x,y : X × Y) → uncurry₀ Z x,y
uncurry f (x , y) = f x y

prop→obs : ∀ {a b} {A : Set a} {B : A → Set b} {f : (x : A) → B x} {g : (x : A) → B x} (eq : f ≣ g) → ∀ {x} → f x ≣ g x
prop→obs ≣-refl {x} = ≣-refl

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

open import Algebra

module Data.FingerTree.Cons
  {r m}
  (ℳ : Monoid r m)
  where

open import Data.Product

open import Data.FingerTree.Measures ℳ
open import Data.FingerTree.Structures ℳ
open import Data.FingerTree.Reasoning ℳ

open σ ⦃ ... ⦄

open Monoid ℳ renaming (Carrier to 𝓡)

infixr 5 _◂_
infixl 5 _▸_

_◂_ : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → (x : Σ) → (xs : Tree Σ) → μ⟨ Tree Σ ⟩≈ (μ x ∙ μ xs)
a ◂ empty = single a ⇑[ ℳ ↯ ]
a ◂ single b = deep ⟪ D₁ a & empty & D₁ b ⇓⟫ ⇑[ ℳ ↯ ]
a ◂ deep (𝓂 ↤ D₁ b       & m & rs ⇑[ 𝓂≈ ]) = deep (μ a ∙ 𝓂 ↤ D₂ a b     & m & rs ⇑[ assoc _ _ _ ⍮ ∙≫ 𝓂≈ ]) ⇑
a ◂ deep (𝓂 ↤ D₂ b c     & m & rs ⇑[ 𝓂≈ ]) = deep (μ a ∙ 𝓂 ↤ D₃ a b c   & m & rs ⇑[ assoc _ _ _ ⍮ ∙≫ 𝓂≈ ]) ⇑
a ◂ deep (𝓂 ↤ D₃ b c d   & m & rs ⇑[ 𝓂≈ ]) = deep (μ a ∙ 𝓂 ↤ D₄ a b c d & m & rs ⇑[ assoc _ _ _ ⍮ ∙≫ 𝓂≈ ]) ⇑
a ◂ deep (𝓂 ↤ D₄ b c d e & m & rs ⇑[ 𝓂≈ ]) with ⟪ N₃ c d e ⇓⟫ ◂ m
... | m′ ⇑[ m′≈ ] = deep (μ a ∙ 𝓂 ↤ D₂ a b & m′ & rs ⇑[ ∙≫ ≪∙ m′≈ ] ≈[ ℳ ↯ ] ≈[ ∙≫ 𝓂≈ ]′) ⇑

_▸_ : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → (xs : Tree Σ) → (x : Σ) → μ⟨ Tree Σ ⟩≈ (μ xs ∙ μ x)
empty ▸ a = single a ⇑[ ℳ ↯ ]
single a ▸ b = deep ⟪ D₁ a & empty & D₁ b ⇓⟫ ⇑[ ℳ ↯ ]
deep (𝓂 ↤ ls & m & D₁ a       ⇑[ 𝓂≈ ]) ▸ b = deep (𝓂 ∙ μ b ↤ ls & m & D₂ a b     ⇑[ ℳ ↯ ⍮′ ≪∙ 𝓂≈ ]) ⇑
deep (𝓂 ↤ ls & m & D₂ a b     ⇑[ 𝓂≈ ]) ▸ c = deep (𝓂 ∙ μ c ↤ ls & m & D₃ a b c   ⇑[ ℳ ↯ ⍮′ ≪∙ 𝓂≈ ]) ⇑
deep (𝓂 ↤ ls & m & D₃ a b c   ⇑[ 𝓂≈ ]) ▸ d = deep (𝓂 ∙ μ d ↤ ls & m & D₄ a b c d ⇑[ ℳ ↯ ⍮′ ≪∙ 𝓂≈ ]) ⇑
deep (𝓂 ↤ ls & m & D₄ a b c d ⇑[ 𝓂≈ ]) ▸ e with m ▸ ⟪ N₃ a b c ⇓⟫
... | m′ ⇑[ m′≈ ] = deep (𝓂 ∙ μ e ↤ ls & m′ & D₂ d e ⇑[ ∙≫ ≪∙ m′≈ ] ≈[ ℳ ↯ ] ≈[ ≪∙ 𝓂≈ ]′) ⇑

open import Data.List as List using (List; _∷_; [])

listToTree : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → (xs : List Σ) → μ⟨ Tree Σ ⟩≈ (μ xs)
listToTree [] = empty ⇑
listToTree (x ∷ xs) = [ ℳ ↯ ]≈ do
  ys ← listToTree xs [ μ x ∙> s ⟿ s ]
  x ◂ ys

max_stars_repo_name: oisdk/agda-indexed-fingertree

max_issues_repo_name: oisdk/agda-indexed-fingertree

max_forks_repo_name: oisdk/agda-indexed-fingertree


text:
-- Check that we can solve level inequalities involving three variables.

module _ where

open import Agda.Primitive
open import Agda.Builtin.Equality

data Constraint : Set where
  mkConstraint : (a b : Level) → a ≡ b → Constraint

infix 0 _:=_
pattern _:=_ x y = mkConstraint x y refl

postulate l : Level

mutual-block : Set

a b c : Level
a = _
b = _
c = _

_ = a := a ⊔ b ⊔ c
_ = b := a ⊔ b ⊔ c
_ = c := a ⊔ b ⊔ c
_ = l := a ⊔ b ⊔ c   -- to actually solve it

mutual-block = Level


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Instance.Posets where

-- The category of partially ordered sets and order-preserving maps.

open import Level
open import Relation.Binary using (Poset; IsEquivalence; _Preserves_⟶_)
open import Relation.Binary.Morphism using (IsOrderHomomorphism)
open import Relation.Binary.Morphism.Bundles using (PosetHomomorphism)
import Relation.Binary.Morphism.Construct.Identity as Id
import Relation.Binary.Morphism.Construct.Composition as Comp

open import Categories.Category

open Poset renaming (_≈_ to ₍_₎_≈_; _≤_ to ₍_₎_≤_)
open PosetHomomorphism using (⟦_⟧; cong)

private
  variable
    a₁ a₂ a₃ b₁ b₂ b₃ : Level
    A B C : Poset a₁ a₂ a₃

module _ {A : Poset a₁ a₂ a₃} {B : Poset b₁ b₂ b₃} where

  infix 4 _≗_

  -- Pointwise equality (on order preserving maps).

  _≗_ : (f g : PosetHomomorphism A B) → Set (a₁ ⊔ b₂)
  f ≗ g = ∀ {x} → ₍ B ₎ ⟦ f ⟧ x ≈ ⟦ g ⟧ x

  ≗-isEquivalence : IsEquivalence _≗_
  ≗-isEquivalence = record
    { refl    = Eq.refl B
    ; sym     = λ f≈g → Eq.sym B f≈g
    ; trans   = λ f≈g g≈h → Eq.trans B f≈g g≈h
    }

  module ≗ = IsEquivalence ≗-isEquivalence

-- The category of posets and order-preserving maps.

Posets : ∀ c ℓ₁ ℓ₂ → Category (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) (c ⊔ ℓ₁ ⊔ ℓ₂) (c ⊔ ℓ₁)
Posets c ℓ₁ ℓ₂ = record
  { Obj       = Poset c ℓ₁ ℓ₂
  ; _⇒_       = PosetHomomorphism
  ; _≈_       = _≗_
  ; id        = λ {A} → Id.posetHomomorphism A
  ; _∘_       = λ f g → Comp.posetHomomorphism g f
  ; assoc     = λ {_ _ _ D} → Eq.refl D
  ; sym-assoc = λ {_ _ _ D} → Eq.refl D
  ; identityˡ = λ {_ B} → Eq.refl B
  ; identityʳ = λ {_ B} → Eq.refl B
  ; identity² = λ {A} → Eq.refl A
  ; equiv     = ≗-isEquivalence
  ; ∘-resp-≈  = λ {_ _ C _ h} f≈h g≈i → Eq.trans C f≈h (cong h g≈i)
  }


text:
{-# OPTIONS --without-K #-}
open import Type
open import Data.Zero
open import Data.Fin using (Fin; zero; suc; #_)
open import Relation.Binary.PropositionalEquality.NP using (_≡_; refl)
open import HoTT
open Equivalences

open import Explore.Core
open import Explore.Properties
open import Explore.Explorable
open import Explore.Universe.Type {𝟘}
open import Explore.Universe.Base

module Explore.Dice where

data Dice : ★₀ where
  ⚀ ⚁ ⚂ ⚃ ⚄ ⚅ : Dice

module ByHand where
    exploreDice : ∀ {m} → Explore m Dice
    exploreDice ε _∙_ f = f ⚀ ∙ (f ⚁ ∙ (f ⚂ ∙ (f ⚃ ∙ (f ⚄ ∙ f ⚅))))

    exploreDice-ind : ∀ {m p} → ExploreInd p (exploreDice {m})
    exploreDice-ind P ε _∙_ f = f ⚀ ∙ (f ⚁ ∙ (f ⚂ ∙ (f ⚃ ∙ (f ⚄ ∙ f ⚅))))

    open FromExploreInd exploreDice-ind public
      using ()
      renaming (sum to sumDice; product to productDice; reify to reifyDice; unfocus to unfocusDice)

Dice≃Fin6 : Dice ≃ Fin 6
Dice≃Fin6 = equiv (⇒) (⇐) ⇒⇐ ⇐⇒
  module Dice≃Fin6 where
    S = Dice
    T = Fin 6
    ⇒ : S → T
    ⇒ ⚀ = # 0
    ⇒ ⚁ = # 1
    ⇒ ⚂ = # 2
    ⇒ ⚃ = # 3
    ⇒ ⚄ = # 4
    ⇒ ⚅ = # 5
    ⇐ : T → S
    ⇐ zero = ⚀
    ⇐ (suc zero) = ⚁
    ⇐ (suc (suc zero)) = ⚂
    ⇐ (suc (suc (suc zero))) = ⚃
    ⇐ (suc (suc (suc (suc zero)))) = ⚄
    ⇐ (suc (suc (suc (suc (suc zero))))) = ⚅
    ⇐ (suc (suc (suc (suc (suc (suc ()))))))
    ⇐⇒ : ∀ x → ⇐ (⇒ x) ≡ x
    ⇐⇒ ⚀ = refl
    ⇐⇒ ⚁ = refl
    ⇐⇒ ⚂ = refl
    ⇐⇒ ⚃ = refl
    ⇐⇒ ⚄ = refl
    ⇐⇒ ⚅ = refl
    ⇒⇐ : ∀ x → ⇒ (⇐ x) ≡ x
    ⇒⇐ zero = refl
    ⇒⇐ (suc zero) = refl
    ⇒⇐ (suc (suc zero)) = refl
    ⇒⇐ (suc (suc (suc zero))) = refl
    ⇒⇐ (suc (suc (suc (suc zero)))) = refl
    ⇒⇐ (suc (suc (suc (suc (suc zero))))) = refl
    ⇒⇐ (suc (suc (suc (suc (suc (suc ()))))))

-- By using FinU' instead of FinU one get a special case for Fin 1 thus avoiding
-- a final ε in the exploration function.
module DiceE = Explore.Universe.Base (≃ᵁ (Finᵁ' 6) Dice (Finᵁ'≃Fin 6 ≃-∙ ≃-! Dice≃Fin6))

module _ {m} where
  open ByHand
  _≡ᵉ_ : (e₀ e₁ : Explore m Dice) → ★_ _
  _≡ᵉ_ = _≡_

  same-as-by-hand : exploreDice ≡ᵉ DiceE.explore
  same-as-by-hand = refl

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
------------------------------------------------------------------------------
-- First-order Peano arithmetic
------------------------------------------------------------------------------

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

module PA.README where

------------------------------------------------------------------------------
-- Description

-- Two formalizations of first-order Peano arithmetic using axioms and
-- inductive definitions.

------------------------------------------------------------------------------
-- Axiomatic PA
open import PA.Axiomatic.Standard.README

-- Inductive PA
open import PA.Inductive.README

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Issue3879 where

open import Issue3879.Fin    using (Fin ; zero ; suc)
open import Agda.Builtin.Nat using (Nat ; zero ; suc)

foo : Nat → Nat → Nat
foo zero m = {!!}
foo (suc n) m = {!!}

-- WAS: case-splitting on m produces Issue3879.Fin.0F patterns
-- WANT: unqualified 0F is not in scope: do not resugar!


text:
----------------------------------------------------------------------------
-- Well-founded induction on the natural numbers
----------------------------------------------------------------------------

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

module FOTC.Data.Nat.Induction.NonAcc.WF-I where

open import FOTC.Base
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesI
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------
-- Well-founded induction on the natural numbers.
-- Adapted from http://code.haskell.org/~dolio/agda-share/induction/.

module WFInd where
  <-wfind : (A : D → Set) →
            (∀ {n} → N n → (∀ {m} → N m → m < n → A m) → A n) →
            ∀ {n} → N n → A n
  <-wfind A h Nn = h Nn (helper Nn)
    where
    helper : ∀ {n m} → N n → N m → m < n → A m
    helper nzero     Nm    m<0  = ⊥-elim (x<0→⊥ Nm m<0)
    helper (nsucc _) nzero 0<Sn = h nzero (λ Nm' m'<0 → ⊥-elim (x<0→⊥ Nm' m'<0))

    helper (nsucc {n} Nn) (nsucc {m} Nm) Sm<Sn = h (nsucc Nm)
      (λ {m'} Nm' m'<Sm →
        let Sm'≤Sm : succ₁ m' ≤ succ₁ m
            Sm'≤Sm = x<y→Sx≤y Nm' (nsucc Nm) m'<Sm

            Sm≤n : succ₁ m ≤ n
            Sm≤n = Sx≤Sy→x≤y (x<y→Sx≤y (nsucc Nm) (nsucc Nn) Sm<Sn)

            Sm'≤n : succ₁ m' ≤ n
            Sm'≤n = ≤-trans (nsucc Nm') (nsucc Nm) Nn Sm'≤Sm Sm≤n

            m'<n : m' < n
            m'<n = Sx≤y→x<y Nm' Nn Sm'≤n

        in  helper Nn Nm' m'<n
      )

------------------------------------------------------------------------------
-- Well-founded induction on the natural numbers (using different
-- properties of inequalities).

module WFInd' where

  <-wfind : (A : D → Set) →
            (∀ {n} → N n → (∀ {m} → N m → m < n → A m) → A n) →
            ∀ {n} → N n → A n
  <-wfind A h Nn = h Nn (helper Nn)
    where
    helper : ∀ {n m} → N n → N m → m < n → A m
    helper nzero Nm m<0 = ⊥-elim (x<0→⊥ Nm m<0)
    helper (nsucc _) nzero 0<Sn = h nzero (λ Nm' m'<0 → ⊥-elim (x<0→⊥ Nm' m'<0))
    helper (nsucc {n} Nn) (nsucc {m} Nm) Sm<Sn = h (nsucc Nm)
      (λ {m'} Nm' m'<Sm →
         let m<n : m < n
             m<n = Sx<Sy→x<y Sm<Sn

             m'<n : m' < n
             m'<n = case (λ m'<m → <-trans Nm' Nm Nn m'<m m<n)
                         (λ m'≡m → x≡y→y<z→x<z m'≡m m<n)
                         (x<Sy→x<y∨x≡y Nm' Nm m'<Sm)

         in  helper Nn Nm' m'<n
      )


text:
module L.Base.Coproduct.Core where

open import Agda.Primitive

-- Introducing Coproduct types
data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inl : A → A + B
  inr : B → A + B

case : ∀{a b c} {A : Set a} {B : Set b}
       → (C : A + B → Set c)
       → ((x : A) → C (inl x)) → ((y : B) → C (inr y))
       → (e : A + B) → C e
case C c d (inl a) = c a
case C c d (inr b) = d b

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


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

module Generalize where

open import Agda.Primitive

-- Generalization in definitions

module Definitions where

  variable
    ℓ : Level
    A B C : Set ℓ
    A₀ B₀  : Set
    a b c : A

  -- Function signature

  id : A → A
  id x = x

  -- Module signature
  module M (a : A) where
    identity = a

  -- Data parameters and constructors

  data Eq (a : A) : A → Setω where
    refl  : Eq a a
    trans : Eq a b → Eq b c → Eq a c

  record R (a : A) : Set₁ where
    field
      fld : B₀

    open M a

    alias = fld

    K : B → C → B
    K x _ = x

    field
      fld₁ : B₀

-- Original content (postulates only)

data _≡_ {ℓ}{A : Set ℓ} (x : A) : A → Set ℓ where
  refl : x ≡ x

infix 4 _≡_

{-# BUILTIN REWRITE _≡_ #-}

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

postulate   Con     :                       Set
postulate   Ty      : (Γ : Con) →           Set
postulate   Tms     : (Γ Δ : Con) →         Set
postulate   Tm      : (Γ : Con)(A : Ty Γ) → Set

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

variable    {Γ Δ Θ} :              Con
postulate   •       :              Con       -- • is \bub
postulate   _▹_     : ∀ Γ → Ty Γ → Con       -- ▹ is \tw2
infixl 5    _▹_

variable    {A B C} :                  Ty _
postulate   _∘ᵀ_    : Ty Δ → Tms Γ Δ → Ty Γ
infixl 6    _∘ᵀ_

variable    {σ δ ν} :                                 Tms _ _
postulate   _∘_     : Tms Θ Δ → Tms Γ Θ →             Tms Γ Δ
infixr 7    _∘_
postulate   id      :                                 Tms Γ Γ
postulate   ε       :                                 Tms Γ •
postulate   _,_     : (σ : Tms Γ Δ) → Tm Γ (A ∘ᵀ σ) → Tms Γ (Δ ▹ A)
infixl 5    _,_
postulate   π₁      : Tms Γ (Δ ▹ A) →                 Tms Γ Δ

variable    {t u v} :                          Tm _ _
postulate   π₂      : (σ : Tms Γ (Δ ▹ A)) →    Tm Γ (A ∘ᵀ π₁ σ)
postulate   _∘ᵗ_    : Tm Δ A → (σ : Tms Γ Δ) → Tm Γ (A ∘ᵀ σ)
infixl 6    _∘ᵗ_

postulate   ass     :   (σ ∘ δ) ∘ ν ≡ σ ∘ δ ∘ ν
{-# REWRITE ass #-}
postulate   idl     :        id ∘ δ ≡ δ
{-# REWRITE idl #-}
postulate   idr     :        δ ∘ id ≡ δ
{-# REWRITE idr #-}
postulate   εη      :             δ ≡ ε  -- can't rewrite, so we specialize this in the next two cases
postulate   εηid    :            id ≡ ε
{-# REWRITE εηid #-}
postulate   εη∘     :         ε ∘ δ ≡ ε
{-# REWRITE εη∘ #-}
postulate   ,β₁     :    π₁ (δ , t) ≡ δ
{-# REWRITE ,β₁ #-}
postulate   ,β₂     :    π₂ (δ , t) ≡ t
{-# REWRITE ,β₂ #-}
postulate   ,η      : (π₁ δ , π₂ δ) ≡ δ
{-# REWRITE ,η #-}
postulate   [id]ᵀ   :       A ∘ᵀ id ≡ A
{-# REWRITE [id]ᵀ #-}
postulate   [∘]ᵀ    :   A ∘ᵀ δ ∘ᵀ σ ≡ A ∘ᵀ δ ∘ σ
{-# REWRITE [∘]ᵀ #-}
postulate   ,∘      :   (δ , t) ∘ σ ≡ δ ∘ σ , t ∘ᵗ σ
{-# REWRITE ,∘ #-}

postulate   [∘]ᵗ    :   t ∘ᵗ σ ∘ᵗ δ ≡ t ∘ᵗ σ ∘ δ
{-# REWRITE [∘]ᵗ #-}
postulate   π₁∘     :      π₁ δ ∘ σ ≡ π₁ (δ ∘ σ)
{-# REWRITE π₁∘ #-}
postulate   π₂∘     :     π₂ δ ∘ᵗ σ ≡ π₂ (δ ∘ σ)
{-# REWRITE π₂∘ #-}
postulate   ∘id     :       t ∘ᵗ id ≡ t
{-# REWRITE ∘id #-}

_↑_ : ∀ σ A → Tms (Γ ▹ A ∘ᵀ σ) (Δ ▹ A)
σ ↑ A = σ ∘ π₁ id , π₂ id

⟨_⟩ : Tm Γ A → Tms Γ (Γ ▹ A)
⟨ t ⟩ = id , t

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

postulate   U       : Ty Γ
variable    {a b c} : Tm _ U
postulate   El      : Tm Γ U → Ty Γ
postulate   U[]     : U ∘ᵀ σ ≡ U
{-# REWRITE U[] #-}
postulate   El[]    : El a ∘ᵀ σ ≡ El (a ∘ᵗ σ)
{-# REWRITE El[] #-}

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

postulate   Π       : (a : Tm Γ U) → Ty (Γ ▹ El a) → Ty Γ
postulate   Π[]     : Π a B ∘ᵀ σ ≡ Π (a ∘ᵗ σ) (B ∘ᵀ σ ↑ El a)
{-# REWRITE Π[] #-}
postulate   app     : Tm Γ (Π a B) → Tm (Γ ▹ El a) B
postulate   app[]   : app t ∘ᵗ (σ ↑ El a) ≡ app (t ∘ᵗ σ)
{-# REWRITE app[] #-}


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

import AssocFree.STLambdaC.Typ
import AssocFree.STLambdaC.Exp
import AssocFree.STLambdaC.NF

module AssocFree.STLambdaC.Redn
  (TConst : Set)
  (Const : AssocFree.STLambdaC.Typ.Typ TConst → Set) where

open module Typ = AssocFree.STLambdaC.Typ TConst using
  ( Typ ; Ctxt ; const ; _⇝_ ; [_] ; [] ; _∷_ ; _++_ ; case )

open module Exp = AssocFree.STLambdaC.Exp TConst Const using
  ( Exp ; const ; abs ; app ; var ; var₀
  ; substn ; weaken ; weaken* ; weaken+ ; weaken-comm ; weaken-substn ; weaken+-var₀ )

open module Redn = AssocFree.STLambdaC.NF TConst Const using
  ( NF ; Atom ; app ; abs )

-- Small-step reduction

data _⇒_ {Γ} : ∀ {T : Typ} → Exp Γ T → Exp Γ T → Set where
  beta : ∀ {T U} (M : Exp (T ∷ Γ) U) (N : Exp Γ T) →
    (app (abs {Γ} T M) N) ⇒ substn N M
  eta : ∀ {T U} (M : Exp Γ (T ⇝ U)) →
    (M ⇒ (abs {Γ} T (app (weaken T M) (var₀ {Γ}))))
  lhs : ∀ {T U} {L M : Exp Γ (T ⇝ U)} {N : Exp Γ T} →
    (L ⇒ M) → (app L N ⇒ app M N)
  rhs : ∀ {T U} {L : Exp Γ (T ⇝ U)} {M N : Exp Γ T} →
    (M ⇒ N) → (app L M ⇒ app L N)
  abs : ∀ T {U} {M N : Exp (T ∷ Γ) U} →
    (M ⇒ N) → (abs {Γ} T M ⇒ abs {Γ} T N)

-- Reduction to normal form

data _⇓ {Γ T} (M : Exp Γ T) : Set where
  nf : NF M → (M ⇓)
  redn : ∀ {N} → (M ⇒ N) → (N ⇓) → (M ⇓)

-- Reduction to atomic form

data _⇓′ {Γ T} (M : Exp Γ T) : Set where
  atom : Atom M → (M ⇓′)
  redn : ∀ {N} → (M ⇒ N) → (N ⇓′) → (M ⇓′)

-- Target of normalization

tgt : ∀ {Γ T} {M : Exp Γ T} → (M ⇓) → Exp Γ T
tgt {Γ} {T} {M} (nf M⇓) = M
tgt       (redn M⇒N N⇓) = tgt N⇓

-- Normalization is closed under abstraction and application

⇓abs : ∀ {Γ} T {U} {M : Exp (T ∷ Γ) U} → (M ⇓) → (abs {Γ} T M ⇓)
⇓abs {Γ} T (nf M)        = nf (abs {Γ} T M)
⇓abs {Γ} T (redn M⇒N N⇓) = redn (abs T M⇒N) (⇓abs {Γ} T N⇓)

⇓app : ∀ {Γ T U} {M : Exp Γ (T ⇝ U)} {N : Exp Γ T} → (M ⇓′) → (N ⇓) → (app M N ⇓′)
⇓app (atom M)      (nf N)        = atom (app M N)
⇓app (atom L)      (redn L⇒M M⇓) = redn (rhs L⇒M) (⇓app (atom L) M⇓)
⇓app (redn L⇒M M⇓) N⇓            = redn (lhs L⇒M) (⇓app M⇓ N⇓)

-- Weakening

rweaken+ : ∀ B Γ Δ {T} {M N : Exp (B ++ Δ) T} → (M ⇒ N) → (weaken+ B Γ Δ M ⇒ weaken+ B Γ Δ N)
rweaken+ B Γ Δ (beta {T} M N) =
  subst (λ X → weaken+ B Γ Δ (app (abs {B ++ Δ} T M) N) ⇒ X)
    (weaken-substn B Γ Δ N M)
    (beta (weaken+ (T ∷ B) Γ Δ M) (weaken+ B Γ Δ N))
rweaken+ B Γ Δ (eta {T} M) =
  subst₂ (λ X Y → weaken+ B Γ Δ M ⇒ abs T (app X Y))
    (weaken-comm T B Γ Δ M) (sym (weaken+-var₀ B Γ Δ))
    (eta (weaken+ B Γ Δ M))
rweaken+ B Γ Δ (lhs M⇒N)   = lhs (rweaken+ B Γ Δ M⇒N)
rweaken+ B Γ Δ (rhs M⇒N)   = rhs (rweaken+ B Γ Δ M⇒N)
rweaken+ B Γ Δ (abs T M⇒N) = abs T (rweaken+ (T ∷ B) Γ Δ M⇒N)

rweaken* : ∀ Γ {Δ T} {M N : Exp Δ T} → (M ⇒ N) → (weaken* Γ M ⇒ weaken* Γ N)
rweaken* Γ {Δ} = rweaken+ [] Γ Δ

rweaken : ∀ T {Δ U} {M N : Exp Δ U} → (M ⇒ N) → (weaken T M ⇒ weaken T N)
rweaken T = rweaken* [ T ]

max_stars_repo_name: agda/agda-assoc-free

max_issues_repo_name: agda/agda-assoc-free

max_forks_repo_name: agda/agda-assoc-free


text:
module ModuleDefinedInOtherFile where

import Imports.B


text:
module Issue530 where

data Unit : Set where
  unit : Unit

postulate
  A : Set
  a : A
  k : A → Unit

data P (a : A) : Unit → Set where
  p : P a (k a)

F : (u : Unit) → P a u → Set₁
F unit _ = Set

f : F (k a) p
f with k a
f | _ = ?

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Vehicle.Data.Tensor
open import Data.Product
open import Data.Integer as ℤ using (ℤ)
open import Data.Rational as ℚ using (ℚ)
open import Data.Fin as Fin using (Fin; #_)
open import Data.List

module windController-temp-output where

InputVector : Set
InputVector = Tensor ℚ (2 ∷ [])

currentSensor : ∀ {_x0 : Set} {{_x1 : HasNatLits _x0}} → _x0
currentSensor = 0

previousSensor : ∀ {_x4 : Set} {{_x5 : HasNatLits _x4}} → _x4
previousSensor = 1

postulate controller : InputVector → Tensor ℚ (1 ∷ [])

SafeInput : InputVector → Set
SafeInput x = ∀ (i : Fin 2) → ℚ.- (ℤ.+ 13 ℚ./ 4) ℚ.≤ x i × x i ℚ.≤ ℤ.+ 13 ℚ./ 4

SafeOutput : InputVector → Set
SafeOutput x = ℚ.- (ℤ.+ 5 ℚ./ 4) ℚ.< (controller x (# 0) ℚ.+ (ℤ.+ 2 ℚ./ 1) ℚ.* x currentSensor) ℚ.- x previousSensor × (controller x (# 0) ℚ.+ (ℤ.+ 2 ℚ./ 1) ℚ.* x currentSensor) ℚ.- x previousSensor ℚ.< ℤ.+ 5 ℚ./ 4

abstract
  safe : ∀ (x : Tensor ℚ (2 ∷ [])) → SafeInput x → SafeOutput x
  safe = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


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

module Issue765 where

infixr 1 _⊎_
infixr 4 _,_
infix 4 _≡_

data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

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

data _⊎_ (A : Set) (B : Set) : Set where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

[_,_]₁ : ∀ {A : Set} {B : Set} {C : A ⊎ B → Set₁} →
        ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
        ((x : A ⊎ B) → C x)
[ f , g ]₁ (inj₁ x) = f x
[ f , g ]₁ (inj₂ y) = g y

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

open Σ public

infix 5 _◃_
infixr 1 _⊎C_

record Container : Set₁ where
  constructor _◃_
  field
    Shape     : Set
    Position  : Shape → Set

open Container public

constC : Set → Container
constC X = X ◃ λ _ → ⊥

_⊎C_ : Container → Container → Container
S ◃ P ⊎C S′ ◃ P′ = (S ⊎ S′) ◃ [ P , P′ ]₁

data μ (C : Container) : Set where
  sup : (s : Shape C) (k : Position C s → μ C) → μ C

_⋆_ : Container → Set → Set
C ⋆ X = μ (constC X ⊎C C)

to : ∀ {C X} → C ⋆ X → C ⋆ (C ⋆ X)
to m = sup (inj₁ m) ⊥-elim

injective : ∀ {C X}{m n : C ⋆ X} → to m ≡ to n → m ≡ n
injective refl = refl


text:
------------------------------------------------------------------------------
-- The unary numbers are FOTC total natural numbers
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.UnaryNumbers.TotalityI where

open import FOTC.Base
open import FOTC.Data.Nat.Type
open import FOTC.Data.Nat.UnaryNumbers

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

0-N : N 0'
0-N = nzero

1-N : N 1'
1-N = nsucc 0-N

2-N : N 2'
2-N = nsucc 1-N


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

_^_ : Nat → Nat → Nat
x ^ zero = 1
x ^ suc y = x * (x ^ y)

data Enum : Set where
  makeEnum : (size : Nat) → (variants : Nat) →
             .{{ _ : (variants < size) ≡ true }} → Enum

five : Enum
five = makeEnum (2 ^ 32) 5

data Expr : (t : Enum) → Set where
  constant : (x : Nat) → Expr five

func : ∀ {t} → Expr t → Bool
func (constant x) = false


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

module Cubical.Categories.Functor where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Categories.Category

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

record Functor (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD') : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
  no-eta-equality
  open Precategory

  field
    F-ob : C .ob → D .ob
    F-hom : {x y : C .ob} → C [ x , y ] → D [(F-ob x) , (F-ob y)]
    F-id : {x : C .ob} → F-hom (C .id x) ≡ D .id (F-ob x)
    F-seq : {x y z : C .ob} (f : C [ x , y ]) (g : C [ y , z ]) → F-hom (f ⋆⟨ C ⟩ g) ≡ (F-hom f) ⋆⟨ D ⟩ (F-hom g)

  isFull = (x y : _) (F[f] : D [(F-ob x) , (F-ob y)]) → ∃ (C [ x , y ]) (λ f → F-hom f ≡ F[f])
  isFaithful = (x y : _) (f g : C [ x , y ]) → F-hom f ≡ F-hom g → f ≡ g

-- Functor results

module _ (C : Precategory ℓC ℓC') (D : Precategory ℓC ℓC') (F : Functor C D ) where
  open Precategory
  open Functor F

  open CatIso

  -- functors preserve isomorphisms
  preserveIsosF : ∀ {x y : C .ob} → CatIso {C = C} x y → CatIso {C = D} (F-ob x) (F-ob y)
  preserveIsosF {x} {y} (catiso f f⁻¹ sec' ret') =
    catiso
      g g⁻¹
      -- sec
      ( (g⁻¹ ⋆⟨ D ⟩ g)
      ≡⟨ sym (F-seq f⁻¹ f) ⟩
        F-hom (f⁻¹ ⋆⟨ C ⟩ f)
      ≡⟨ cong F-hom sec' ⟩
        F-hom (C .id y)
      ≡⟨ F-id ⟩
        D .id y'
      ∎ )
      -- ret
      ( (g ⋆⟨ D ⟩ g⁻¹)
        ≡⟨ sym (F-seq f f⁻¹) ⟩
      F-hom (f ⋆⟨ C ⟩ f⁻¹)
        ≡⟨ cong F-hom ret' ⟩
      F-hom (C .id x)
      ≡⟨ F-id ⟩
        D .id x'
      ∎ )

      where
        x' : D .ob
        x' = F-ob x
        y' : D .ob
        y' = F-ob y

        g : D [ x' , y' ]
        g = F-hom f
        g⁻¹ : D [ y' , x' ]
        g⁻¹ = F-hom f⁻¹


text:
open import Agda.Builtin.Nat

bar : Nat → Nat
bar n = let _!_ : Nat → Nat → Nat
            x ! y = 2 * x ! y  -- should give scope error in RHS
        in n ! n


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

{- Ad-hoc polymorphism -}
module AdHoc where

open import Data.Char as C
open import Data.String as S
open import Data.List as L
open import Data.Integer as I
open import Data.Nat as N
open import Data.Bool as B

open import Agda.Builtin.Nat renaming (_==_ to natEquals)

record Eq {l} (A : Set l) : Set l where
  field
    _===_ : A → A → Bool

open Eq ⦃ ... ⦄ public

_=/=_ : ∀ {l} {A : Set l} ⦃ _ : Eq A ⦄ → A → A → Bool
a =/= b = not (a === b)

instance
  eqInt : Eq ℤ
  _===_ ⦃ eqInt ⦄ (+ m) (+ n) = natEquals m n
  _===_ ⦃ eqInt ⦄ (-[1+ m ]) (-[1+ n ]) = natEquals m n
  _===_ ⦃ eqInt ⦄ _ _ = false

  eqNat : Eq ℕ
  _===_ ⦃ eqNat ⦄ = natEquals

  eqChar : Eq Char
  _===_ ⦃ eqChar ⦄ = C._==_

  eqBool : Eq Bool
  _===_ ⦃ eqBool ⦄ a b = not (a xor b)

  eqStr : Eq String
  _===_ ⦃ eqStr ⦄ = S._==_

  eqList : ∀ {l} {A : Set l} ⦃ _ : Eq A ⦄ → Eq (List A)
  _===_ ⦃ eqList ⦄ [] [] = true
  _===_ ⦃ eqList ⦄ (x ∷ xs) (y ∷ ys) = (x === y) ∧ (xs === ys)
  _===_ ⦃ eqList ⦄ _ _ = false

max_stars_repo_name: anqurvanillapy/fpl

max_issues_repo_name: anqurvanillapy/fpl

max_forks_repo_name: anqurvanillapy/fpl


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.AbGroup.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.Data.Unit

open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommMonoid
open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.DirProd

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open Iso

private
  variable
    ℓ ℓ' : Level

record IsAbGroup {G : Type ℓ}
                 (0g : G) (_+_ : G → G → G) (-_ : G → G) : Type ℓ where

  constructor isabgroup

  field
    isGroup : IsGroup 0g _+_ -_
    comm    : (x y : G) → x + y ≡ y + x

  open IsGroup isGroup public

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

  constructor abgroupstr

  field
    0g        : A
    _+_       : A → A → A
    -_        : A → A
    isAbGroup : IsAbGroup 0g _+_ -_

  infix  8 -_
  infixr 7 _+_

  open IsAbGroup isAbGroup public

AbGroup : ∀ ℓ → Type (ℓ-suc ℓ)
AbGroup ℓ = TypeWithStr ℓ AbGroupStr

makeIsAbGroup : {G : Type ℓ} {0g : G} {_+_ : G → G → G} { -_ : G → G}
              (is-setG : isSet G)
              (assoc   : (x y z : G) → x + (y + z) ≡ (x + y) + z)
              (rid     : (x : G) → x + 0g ≡ x)
              (rinv    : (x : G) → x + (- x) ≡ 0g)
              (comm    : (x y : G) → x + y ≡ y + x)
            → IsAbGroup 0g _+_ -_
makeIsAbGroup is-setG assoc rid rinv comm =
  isabgroup (makeIsGroup is-setG assoc rid (λ x → comm _ _ ∙ rid x) rinv (λ x → comm _ _ ∙ rinv x)) comm

makeAbGroup : {G : Type ℓ} (0g : G) (_+_ : G → G → G) (-_ : G → G)
            (is-setG : isSet G)
            (assoc : (x y z : G) → x + (y + z) ≡ (x + y) + z)
            (rid : (x : G) → x + 0g ≡ x)
            (rinv : (x : G) → x + (- x) ≡ 0g)
            (comm    : (x y : G) → x + y ≡ y + x)
          → AbGroup ℓ
makeAbGroup 0g _+_ -_ is-setG assoc rid rinv comm =
  _ , abgroupstr 0g _+_ -_ (makeIsAbGroup is-setG assoc rid rinv comm)

open GroupStr
open AbGroupStr
open IsAbGroup

AbGroupStr→GroupStr : {G : Type ℓ} → AbGroupStr G → GroupStr G
AbGroupStr→GroupStr A .1g = A .0g
AbGroupStr→GroupStr A ._·_ = A ._+_
AbGroupStr→GroupStr A .inv = A .-_
AbGroupStr→GroupStr A .isGroup = A .isAbGroup .isGroup

AbGroup→Group : AbGroup ℓ → Group ℓ
fst (AbGroup→Group A) = fst A
snd (AbGroup→Group A) = AbGroupStr→GroupStr (snd A)

Group→AbGroup : (G : Group ℓ) → ((x y : fst G) → _·_ (snd G) x y ≡ _·_ (snd G) y x) → AbGroup ℓ
fst (Group→AbGroup G comm) = fst G
AbGroupStr.0g (snd (Group→AbGroup G comm)) = 1g (snd G)
AbGroupStr._+_ (snd (Group→AbGroup G comm)) = _·_ (snd G)
AbGroupStr.- snd (Group→AbGroup G comm) = inv (snd G)
IsAbGroup.isGroup (AbGroupStr.isAbGroup (snd (Group→AbGroup G comm))) = isGroup (snd G)
IsAbGroup.comm (AbGroupStr.isAbGroup (snd (Group→AbGroup G comm))) = comm

AbGroup→CommMonoid : AbGroup ℓ → CommMonoid ℓ
AbGroup→CommMonoid (_ , abgroupstr  _ _ _ G) =
  _ , commmonoidstr _ _ (iscommmonoid (IsAbGroup.isMonoid G) (IsAbGroup.comm G))

isSetAbGroup : (A : AbGroup ℓ) → isSet ⟨ A ⟩
isSetAbGroup A = isSetGroup (AbGroup→Group A)

AbGroupHom : (G : AbGroup ℓ) (H : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
AbGroupHom G H = GroupHom (AbGroup→Group G) (AbGroup→Group H)

AbGroupIso : (G : AbGroup ℓ) (H : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
AbGroupIso G H = GroupIso (AbGroup→Group G) (AbGroup→Group H)

IsAbGroupEquiv : {A : Type ℓ} {B : Type ℓ'}
  (G : AbGroupStr A) (e : A ≃ B) (H : AbGroupStr B) → Type (ℓ-max ℓ ℓ')
IsAbGroupEquiv G e H = IsGroupHom (AbGroupStr→GroupStr G) (e .fst) (AbGroupStr→GroupStr H)

AbGroupEquiv : (G : AbGroup ℓ) (H : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
AbGroupEquiv G H = Σ[ e ∈ (G .fst ≃ H .fst) ] IsAbGroupEquiv (G .snd) e (H .snd)

isPropIsAbGroup : {G : Type ℓ} (0g : G) (_+_ : G → G → G) (- : G → G)
                → isProp (IsAbGroup 0g _+_ -)
isPropIsAbGroup 0g _+_ -_ (isabgroup GG GC) (isabgroup HG HC) =
  λ i → isabgroup (isPropIsGroup _ _ _ GG HG i) (isPropComm GC HC i)
  where
  isSetG : isSet _
  isSetG = GG .IsGroup.isMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

  isPropComm : isProp ((x y : _) → x + y ≡ y + x)
  isPropComm = isPropΠ2 λ _ _ → isSetG _ _

𝒮ᴰ-AbGroup : DUARel (𝒮-Univ ℓ) AbGroupStr ℓ
𝒮ᴰ-AbGroup =
  𝒮ᴰ-Record (𝒮-Univ _) IsAbGroupEquiv
    (fields:
      data[ _+_ ∣ autoDUARel _ _ ∣ pres· ]
      data[ 0g ∣ autoDUARel _ _ ∣ pres1 ]
      data[ -_ ∣ autoDUARel _ _ ∣ presinv ]
      prop[ isAbGroup ∣ (λ _ _ → isPropIsAbGroup _ _ _) ])
  where
  open AbGroupStr
  open IsGroupHom

-- Extract the characterization of equality of groups
AbGroupPath : (G H : AbGroup ℓ) → (AbGroupEquiv G H) ≃ (G ≡ H)
AbGroupPath = ∫ 𝒮ᴰ-AbGroup .UARel.ua

-- TODO: Induced structure results are temporarily inconvenient while we transition between algebra
-- representations
module _ (G : AbGroup ℓ) {A : Type ℓ} (m : A → A → A)
  (e : ⟨ G ⟩ ≃ A)
  (p· : ∀ x y → e .fst (G .snd ._+_ x y) ≡ m (e .fst x) (e .fst y))
  where

  private
    module G = AbGroupStr (G .snd)

    FamilyΣ : Σ[ B ∈ Type ℓ ] (B → B → B) → Type ℓ
    FamilyΣ (B , n) =
      Σ[ e ∈ B ]
      Σ[ i ∈ (B → B) ]
      IsAbGroup e n i

    inducedΣ : FamilyΣ (A , m)
    inducedΣ =
      subst FamilyΣ
        (UARel.≅→≡ (autoUARel (Σ[ B ∈ Type ℓ ] (B → B → B))) (e , p·))
        (G.0g , G.-_ , G.isAbGroup)

  InducedAbGroup : AbGroup ℓ
  InducedAbGroup .fst = A
  InducedAbGroup .snd ._+_ = m
  InducedAbGroup .snd .0g = inducedΣ .fst
  InducedAbGroup .snd .-_ = inducedΣ .snd .fst
  InducedAbGroup .snd .isAbGroup = inducedΣ .snd .snd

  InducedAbGroupPath : G ≡ InducedAbGroup
  InducedAbGroupPath = AbGroupPath _ _ .fst (e , makeIsGroupHom p·)

open IsMonoid
open IsSemigroup
open IsGroup

dirProdAb : AbGroup ℓ → AbGroup ℓ' → AbGroup (ℓ-max ℓ ℓ')
dirProdAb A B =
  Group→AbGroup (DirProd (AbGroup→Group A) (AbGroup→Group B))
                 λ p q → ΣPathP (comm (isAbGroup (snd A)) _ _
                                , comm (isAbGroup (snd B)) _ _)

trivialAbGroup : ∀ {ℓ} → AbGroup ℓ
fst trivialAbGroup = Unit*
0g (snd trivialAbGroup) = tt*
_+_ (snd trivialAbGroup) _ _ = tt*
(- snd trivialAbGroup) _ = tt*
is-set (isSemigroup (isMonoid (isGroup (isAbGroup (snd trivialAbGroup))))) =
  isProp→isSet isPropUnit*
assoc (isSemigroup (isMonoid (isGroup (isAbGroup (snd trivialAbGroup))))) _ _ _ = refl
identity (isMonoid (isGroup (isAbGroup (snd trivialAbGroup)))) _ = refl , refl
inverse (isGroup (isAbGroup (snd trivialAbGroup))) _ = refl , refl
comm (isAbGroup (snd trivialAbGroup)) _ _ = refl

-- useful lemma
move4 : ∀ {ℓ} {A : Type ℓ} (x y z w : A) (_+_ : A → A → A)
       → ((x y z : A) → x + (y + z) ≡ (x + y) + z)
       → ((x y : A) → x + y ≡ y + x)
      → (x + y) + (z + w) ≡ ((x + z) + (y + w))
move4 x y z w _+_ assoc comm =
     sym (assoc x y (z + w))
  ∙∙ cong (x +_) (assoc y z w ∙∙ cong (_+ w) (comm y z) ∙∙ sym (assoc z y w))
  ∙∙ assoc x z (y + w)

---- The type of homomorphisms A → B is an AbGroup if B is -----
module _ {ℓ ℓ' : Level} (AGr : Group ℓ) (BGr : AbGroup ℓ') where
  private
    strA = snd AGr
    strB = snd BGr

    _* = AbGroup→Group

    A = fst AGr
    B = fst BGr
    open IsGroupHom

    open AbGroupStr strB
      renaming (_+_ to _+B_ ; -_ to -B_ ; 0g to 0B
              ; rid to ridB ; lid to lidB
              ; assoc to assocB ; comm to commB
              ; invr to invrB ; invl to invlB)
    open GroupStr strA
      renaming (_·_ to _∙A_ ; inv to -A_
                ; 1g to 1A ; rid to ridA)

  trivGroupHom : GroupHom AGr (BGr *)
  fst trivGroupHom x = 0B
  snd trivGroupHom = makeIsGroupHom λ _ _ → sym (ridB 0B)

  compHom : GroupHom AGr (BGr *) → GroupHom AGr (BGr *) → GroupHom AGr (BGr *)
  fst (compHom f g) x = fst f x +B fst g x
  snd (compHom f g) =
      makeIsGroupHom λ x y
      → cong₂ _+B_ (pres· (snd f) x y) (pres· (snd g) x y)
      ∙ move4 (fst f x) (fst f y) (fst g x) (fst g y)
              _+B_ assocB commB

  invHom : GroupHom AGr (BGr *) → GroupHom AGr (BGr *)
  fst (invHom (f , p)) x = -B f x
  snd (invHom (f , p)) =
    makeIsGroupHom
      λ x y → cong -B_ (pres· p x y)
            ∙∙ GroupTheory.invDistr (BGr *) (f x) (f y)
            ∙∙ commB _ _

  open AbGroupStr
  open IsAbGroup
  open IsGroup
  open IsMonoid
  open IsSemigroup

  HomGroup : AbGroup (ℓ-max ℓ ℓ')
  fst HomGroup = GroupHom AGr (BGr *)
  0g (snd HomGroup) = trivGroupHom
  AbGroupStr._+_ (snd HomGroup) = compHom
  AbGroupStr.- snd HomGroup = invHom
  is-set (isSemigroup (isMonoid (isGroup (isAbGroup (snd HomGroup))))) =
    isSetGroupHom
  assoc (isSemigroup (isMonoid (isGroup (isAbGroup (snd HomGroup))))) (f , p) (g , q) (h , r) =
    Σ≡Prop (λ _ → isPropIsGroupHom _ _)
      (funExt λ x → assocB _ _ _)
  fst (identity (isMonoid (isGroup (isAbGroup (snd HomGroup)))) (f , p)) =
    Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ y → ridB _)
  snd (identity (isMonoid (isGroup (isAbGroup (snd HomGroup)))) (f , p)) =
    Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ x → lidB _)
  fst (inverse (isGroup (isAbGroup (snd HomGroup))) (f , p)) =
    Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ x → invrB (f x))
  snd (inverse (isGroup (isAbGroup (snd HomGroup))) (f , p)) =
    Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ x → invlB (f x))
  comm (isAbGroup (snd HomGroup)) (f , p) (g , q) =
    Σ≡Prop (λ _ → isPropIsGroupHom _ _)
      (funExt λ x → commB _ _)

max_stars_repo_name: gmagaf/cubical

max_issues_repo_name: gmagaf/cubical

max_forks_repo_name: gmagaf/cubical


text:
module _ where

data ⊤ : Set where tt : ⊤

pattern id x = x

postulate
  X : Set

loops : X
loops = tt


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Existential lifting of predicates over Vectors
------------------------------------------------------------------------

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

module Data.Vec.Functional.Relation.Unary.Any where

open import Data.Fin.Base
open import Data.Fin.Properties
open import Data.Nat.Base
open import Data.Product as Σ using (Σ; ∃; _×_; _,_; proj₁; proj₂)
open import Data.Vec.Functional as VF hiding (map)
open import Function
open import Level using (Level)
open import Relation.Unary

private
  variable
    a b p q ℓ : Level
    A : Set a
    B : Set b

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

Any : Pred A ℓ → ∀ {n} → Vector A n → Set ℓ
Any P xs = ∃ λ i → P (xs i)

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

module _ {P : Pred A p} where

  here : ∀ {x n} {v : Vector A n} → P x → Any P (x ∷ v)
  here px = zero , px

  there : ∀ {x n} {v : Vector A n} → Any P v → Any P (x ∷ v)
  there = Σ.map suc id

module _ {P : Pred A p} {Q : Pred A q} where

  map : P ⊆ Q → ∀ {n} → Any P {n = n} ⊆ Any Q
  map p⊆q = Σ.map id p⊆q

------------------------------------------------------------------------
-- Properties of predicates preserved by Any

module _ {P : Pred A p} where

  any : Decidable P → ∀ {n} → Decidable (Any P {n = n})
  any p? xs = any? λ i → p? (xs i)


text:
module cfg where

open import jarsec using (Parser ; run-parser ; partial-parse ; _>>=_ ; _>>_ ; _<*>_)

open import Data.Bool
open import Data.List hiding (lookup)
open import Data.Vec renaming ([_] to V[_] ; _++_ to _vv_) hiding (_>>=_)
open import Data.Fin hiding (_+_)
open import Data.Char
open import Agda.Builtin.Char renaming ( primCharEquality to charEq )
open import Data.Nat
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Data.Maybe
open import Data.Sum hiding (map)
open import Data.String hiding (length ; _++_) renaming (primStringToList to 𝕊→𝕃 ; primStringFromList to 𝕃→𝕊)
open import Data.Product hiding (map)
open import Agda.Builtin.Unit

postulate
  𝕃⇄𝕊 : ∀ (cs : List Char) → (𝕊→𝕃 (𝕃→𝕊 cs)) ≡ cs

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

A : Set
A = Char

data Cfg : ℕ → Set where
  emp : ∀ {n} → Cfg n
  eps : ∀ {n} → Cfg n
  lit : ∀ {n} → A → Cfg n
  var : ∀ {n} → Fin n → Cfg n
  seq : ∀ {n} → Cfg n → Cfg n → Cfg n
  alt : ∀ {n} → Cfg n → Cfg n → Cfg n
  many : ∀ {n} → Cfg n → Cfg n
  fix : ∀ {n} → Cfg (suc n) → Cfg n

Env : ℕ → Set
Env n = Vec (Cfg n) n

_⊖_ : ∀ (n : ℕ) → Fin n → ℕ
(suc n) ⊖ zero = n
(suc n) ⊖ suc i = suc (n ⊖ i)

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

introd-var : ∀ {n : ℕ} (i : Fin n) → Fin (n ⊖ i) → Fin n
introd-var zero x = suc x
introd-var (suc i) zero = zero

introd-var (suc i) (suc x) = suc (introd-var i x)

introd : ∀ {n : ℕ} (i : Fin n) → Cfg (n ⊖ i) → Cfg n
introd i emp = emp
introd i eps = eps
introd i (lit l) = lit l
introd i (var x) = var (introd-var i x)
introd i (seq e₁ e₂) = seq (introd i e₁) (introd i e₂)
introd i (alt e₁ e₂) = alt (introd i e₁) (introd i e₂)
introd i (many e) = many (introd i e)
introd i (fix e) = fix (introd (suc i) e)

-- used in subst
introd-var-N : ∀ {n : ℕ} (m : ℕ) → Fin n → Fin (m ⊕ n)
introd-var-N zero x = x
introd-var-N (suc m) x = introd-var-N m (introd-var zero x)

-- used in subst
intro : ∀ {n : ℕ} → Cfg n → Cfg (suc n)
intro = introd zero

subst-var : ∀ {n : ℕ} (m : ℕ) (x : Fin n) → Cfg (m ⊕ (n ⊖ x)) → Fin n → Cfg (m ⊕ (n ⊖ x))
subst-var m zero v zero = v
subst-var m zero v (suc y) = var (introd-var-N m y)
subst-var m (suc x) v zero = var (introd-var-N m zero)
subst-var m (suc x) v (suc y) = subst-var (suc m) x v y

subst : ∀ {n : ℕ} (x : Fin n) → Cfg (n ⊖ x) → Cfg n → Cfg (n ⊖ x)
subst y v emp = emp
subst y v eps = eps
subst y v (lit l) = lit l
subst y v (var x) = subst-var zero y v x
subst y v (seq e₁ e₂) = seq (subst y v e₁) (subst y v e₂)
subst y v (alt e₁ e₂) = alt (subst y v e₁) (subst y v e₂)
subst y v (many e) = many (subst y v e)
subst y v (fix e) = fix (subst (suc y) (intro v) e)

sub : ∀ {n : ℕ} → Cfg n → Cfg (suc n) → Cfg n
sub = subst zero

data _∈[_] : List A → Cfg 0 → Set where
  eps : [] ∈[ eps ]

  lit : ∀ (c : A) → [ c ] ∈[ lit c ]

  seq : ∀ {s₁ s₂ : List A} {cfg₁ cfg₂ : Cfg 0}
    → s₁ ∈[ cfg₁ ]
    → s₂ ∈[ cfg₂ ]
    → (s₁ ++ s₂) ∈[ seq cfg₁ cfg₂ ]

  alt₁ : {s : List A} {cfg₁ cfg₂ : Cfg 0}
    → s ∈[ cfg₁ ]
    → s ∈[ alt cfg₁ cfg₂ ]

  alt₂ : {s : List A} {cfg₁ cfg₂ : Cfg 0}
    → s ∈[ cfg₂ ]
    → s ∈[ alt cfg₁ cfg₂ ]

  many0 : {cfg : Cfg 0}
    → [] ∈[ many cfg ]

  many+ : {s₁ s₂ : List A} {cfg : Cfg 0}
    → s₁ ∈[ cfg ]
    → s₂ ∈[ many cfg ]
    → (s₁ ++ s₂) ∈[ many cfg ]

  unroll : {s : List A}
    → {cfg : Cfg 1}
    → s ∈[ sub (fix cfg) cfg ]
    → s ∈[ fix cfg ]

abstract
  instance
    block : ⊤
    block = tt
  unblock : block ≡ tt
  unblock = refl

delayed : ∀ {A : Set} → ⊤ → A  → A
delayed tt x = x

delay : ∀ {A : Set} → A → A
delay = delayed block

{-# TERMINATING #-}
interp : Cfg 0 → Parser (List A)
interp emp = Parser.mk-parser (λ _ → [])
interp eps = Parser.mk-parser (λ str → [ ([] , str) ])
interp (lit c) = do
  c′ ← jarsec.satisfy (charEq c)
  jarsec.unit [ c′ ]
interp (var ())
interp (seq cfg₁ cfg₂) = do
  x ← (interp cfg₁)
  y ← (interp cfg₂)
  jarsec.unit (x ++ y)
interp (alt cfg₁ cfg₂) = jarsec.combine (interp cfg₁) (interp cfg₂)
interp (many cfg) = interp (alt eps (seq cfg (delay (many cfg))))
interp (fix cfg) = interp (sub (fix cfg) cfg)

a : Fin 2
a = zero
b : Fin 2
b = (suc zero)

xX-or-ε : Cfg 0
xX-or-ε = fix (alt (seq (lit 'x') (var zero)) eps)

-- _ : interp xX-or-ε ≡ {!   !}
-- _ = refl

_ : (𝕊→𝕃 "xx") ∈[ fix {n = 0} (alt (seq (lit 'x') (var zero)) (eps)) ]
_ = unroll (alt₁ (seq (lit 'x') (unroll (alt₁ (seq (lit 'x') (unroll (alt₂ eps)))))))

_ : (𝕊→𝕃 "xx") ∈[ xX-or-ε ]
_ =
  unroll
  (alt₁ (seq (lit 'x') (
    unroll
    (alt₁ (seq (lit 'x') (
      unroll
      (alt₂ eps)))))))

_ : ( 'a' ∷ 'a' ∷ []) ∈[ many (lit 'a') ]
_ = many+ (lit 'a') (many+ (lit 'a') many0)

max_stars_repo_name: jaywunder/jarsec-verified

max_issues_repo_name: jaywunder/jarsec-verified

max_forks_repo_name: jaywunder/jarsec-verified


text:
-- 2010-09-06 Andreas

module IrrelevantVar where

-- type checker should fail and complain that x is irrelevant and cannot be used

f : {A : Set} -> .A -> A -> A
f x y = x