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

module Dodo.Binary.SplittableOrder where

-- Stdlib imports
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Level using (Level; _⊔_)
open import Function using (_∘_)
open import Data.Empty using (⊥-elim)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃-syntax)
open import Relation.Nullary using (¬_)
open import Relation.Unary using (Pred)
open import Relation.Binary using (Rel; REL; Transitive; Trichotomous; Tri; tri<; tri≈; tri>)
open import Relation.Binary.Construct.Closure.Transitive using (TransClosure; [_]; _∷_; _++_)
-- Local imports
open import Dodo.Unary.Equality
open import Dodo.Binary.Equality
open import Dodo.Binary.Immediate
open import Dodo.Binary.Trichotomous
open import Dodo.Binary.Transitive
open import Dodo.Binary.Domain
open import Dodo.Binary.Filter

open import Function using (flip)

-- # Definitions #

-- For any `R x y` there exists a /path/ from `x` to `y`.
SplittableOrder : {a ℓ : Level} {A : Set a} (R : Rel A ℓ) → Set (a ⊔ ℓ)
SplittableOrder R = R ⇔₂ TransClosure (immediate R)

-- # Properties #

module _ {a ℓ : Level} {A : Set a} {R : Rel A ℓ} where

  splittable-trans : SplittableOrder R → Transitive R
  splittable-trans splitR Rij Rjk =
    ⇔₂-apply-⊇₂ splitR (⇔₂-apply-⊆₂ splitR Rij ++ ⇔₂-apply-⊆₂ splitR Rjk)

  splittable-flip : SplittableOrder R → SplittableOrder (flip R)
  splittable-flip splitR = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : flip R ⊆₂' TransClosure (immediate (flip R))
    ⊆-proof _ _ = ⁺-map _ imm-flip ∘ ⁺-flip ∘ ⇔₂-apply-⊆₂ splitR

    ⊇-proof : TransClosure (immediate (flip R)) ⊆₂' flip R
    ⊇-proof _ _ = ⇔₂-apply-⊇₂ splitR ∘ ⁺-flip ∘ ⁺-map _ imm-flip

-- # Operations #

-- Split the left-most element from the ordered relation chain
splitˡ : ∀ {a ℓ : Level} {A : Set a} {R : Rel A ℓ}
  → SplittableOrder R
  → {x y : A}
  → R x y
    --------------------------------------------------
  → immediate R x y ⊎ ∃[ z ] (immediate R x z × R z y)
splitˡ splitR Rxy with ⇔₂-apply-⊆₂ splitR Rxy
... | [ immRxy ] = inj₁ immRxy
... | _∷_ {x} {z} {y} immRxz immR⁺zy = inj₂ (z , immRxz , ⇔₂-apply-⊇₂ splitR immR⁺zy)

-- Split the right-most element from the ordered relation chain
splitʳ : ∀ {a ℓ : Level} {A : Set a} {R : Rel A ℓ}
  → SplittableOrder R
  → {x y : A}
  → R x y
    --------------------------------------------------
  → immediate R x y ⊎ ∃[ z ] (R x z × immediate R z y)
splitʳ {A = A} {R = R} splitR Rxy = lemma (⇔₂-apply-⊆₂ splitR Rxy)
  where
  lemma : ∀ {x y : A} → TransClosure (immediate R) x y → immediate R x y ⊎ ∃[ z ] (R x z × immediate R z y)
  lemma [ immRxy ] = inj₁ immRxy
  lemma ( _∷_ {x} {z} {y} immRxz immR⁺zy ) with lemma immR⁺zy
  ... | inj₁ immRzy = inj₂ (z , proj₁ immRxz , immRzy)
  ... | inj₂ (w , Rzw , immRwy) = inj₂ (w , splittable-trans splitR (proj₁ immRxz) Rzw , immRwy)

-- Splits the given left-most element from the chain.
unsplitˡ : ∀ {a ℓ₁ ℓ₂ : Level} {A : Set a} {_≈_ : Rel A ℓ₁} {R : Rel A ℓ₂}
  → Trichotomous _≈_ R
  → SplittableOrder R
  → {x y z : A}
  → R x z
  → immediate R x y
  → y ≈ z ⊎ R y z
unsplitˡ triR splitR {x} {y} {z} Rxz immRxy with splitˡ splitR Rxz
unsplitˡ triR splitR {x} {y} {z} Rxz immRxy | inj₁ immRxz = inj₁ (tri-immʳ triR immRxy immRxz)
unsplitˡ triR splitR {x} {y} {z} Rxz immRxy | inj₂ (v , immRxv , Rvz) with triR y z
unsplitˡ triR splitR {x} {y} {z} Rxz immRxy | inj₂ (v , immRxv , Rvz) | tri<  Ryz y≢z ¬Rzy = inj₂ Ryz
unsplitˡ triR splitR {x} {y} {z} Rxz immRxy | inj₂ (v , immRxv , Rvz) | tri≈ ¬Ryz y≡z ¬Rzy = inj₁ y≡z
unsplitˡ triR splitR {x} {y} {z} Rxz immRxy | inj₂ (v , immRxv , Rvz) | tri> ¬Ryz y≢z  Rzy = ⊥-elim (proj₂ immRxy (z , Rxz , [ Rzy ]))

-- Splits the given right-most element from the chain.
unsplitʳ : ∀ {a ℓ₁ ℓ₂ : Level} {A : Set a} {_≈_ : Rel A ℓ₁} {R : Rel A ℓ₂}
  → Trichotomous _≈_ R
  → SplittableOrder R
  → {x y z : A}
  → R x z
  → immediate R y z
  → x ≈ y ⊎ R x y
unsplitʳ triR splitR {x} {y} {z} Rxz iRyz with splitʳ splitR Rxz
unsplitʳ triR splitR {x} {y} {z} Rxz iRyz | inj₁ iRxz = inj₁ (tri-immˡ triR iRxz iRyz)
unsplitʳ triR splitR {x} {y} {z} Rxz iRyz | inj₂ (v , Rxv , iRvz) with triR x y
unsplitʳ triR splitR {x} {y} {z} Rxz iRyz | inj₂ (v , Rxv , iRvz) | tri<  Rxy x≢y ¬Ryx = inj₂ Rxy
unsplitʳ triR splitR {x} {y} {z} Rxz iRyz | inj₂ (v , Rxv , iRvz) | tri≈ ¬Rxy x≡y ¬Ryx = inj₁ x≡y
unsplitʳ triR splitR {x} {y} {z} Rxz iRyz | inj₂ (v , Rxv , iRvz) | tri> ¬Rxy x≢y  Ryx = ⊥-elim (proj₂ iRyz (x , Ryx , [ Rxz ]))

splittable-imm-udr : ∀ {a ℓ : Level} {A : Set a} {R : Rel A ℓ}
  → SplittableOrder R
  → udr R ⇔₁ udr (immediate R)
splittable-imm-udr {R = R} splitR = ⇔: ⊆-proof ⊇-proof
  where
  ⊆-proof : udr R ⊆₁' udr (immediate R)
  ⊆-proof x (inj₁ (y , Rxy)) = inj₁ (⁺-dom (⇔₂-apply-⊆₂ splitR Rxy))
  ⊆-proof y (inj₂ (x , Rxy)) = inj₂ (⁺-codom (⇔₂-apply-⊆₂ splitR Rxy))

  ⊇-proof : udr (immediate R) ⊆₁' udr R
  ⊇-proof x (inj₁ (y , Rxy)) = inj₁ (y , proj₁ Rxy)
  ⊇-proof y (inj₂ (x , Rxy)) = inj₂ (x , proj₁ Rxy)

-- | If any value in the chain of R satisfies P, it remains splittable after lifting.
--
-- The chain is traversed /to the left/.
filter-splittableˡ : ∀ {a ℓ : Level} {A : Set a} {R : Rel A ℓ}
  → SplittableOrder R
  → (P : Pred A ℓ)
  → (∀ {x y : A} → P y → R x y → P x)
    ---------------------------------
  → SplittableOrder (filter-rel P R)
filter-splittableˡ {A = A} {R = R} splitR P f = ⇔: ⊆-proof ⊇-proof
  where
  lemma⊆-imm : ∀ {x y : A} → (Px : P x) → (Py : P y) → immediate R x y → immediate (filter-rel P R) (with-pred x Px) (with-pred y Py)
  lemma⊆-imm {x} {y} Px Py (Rxy , ¬∃z) = Rxy , ¬∃z'
    where
    ¬∃z' : ¬ (∃[ z ] filter-rel P R (with-pred x Px) z × TransClosure (filter-rel P R) z (with-pred y Py))
    ¬∃z' (with-pred z Pz , Rxz , R⁺zy) = ¬∃z (z , Rxz , ⁺-strip-filter R⁺zy)

  lemma⊆ : ∀ {x y : A} → (Px : P x) → (Py : P y) → TransClosure (immediate R) x y
    → TransClosure (immediate (filter-rel P R)) (with-pred x Px) (with-pred y Py)
  lemma⊆ Px Py [ iRxy ] = [ lemma⊆-imm Px Py iRxy ]
  lemma⊆ Px Py ( iRxz ∷ iR⁺zy ) =
    let Pz = ⁺-predˡ (λ Pz → f Pz ∘ proj₁) iR⁺zy Py
    in lemma⊆-imm Px Pz iRxz ∷ lemma⊆ Pz Py iR⁺zy

  ⊆-proof : filter-rel P R ⊆₂' TransClosure (immediate (filter-rel P R))
  ⊆-proof (with-pred x Px) (with-pred y Py) Rxy = lemma⊆ Px Py (⇔₂-apply-⊆₂ splitR Rxy)

  lemma⊇-imm : ∀ {x y : A} → (Px : P x) → (Py : P y) → immediate (filter-rel P R) (with-pred x Px) (with-pred y Py)
    → immediate R x y
  lemma⊇-imm {x} {y} Px Py (Rxy , ¬∃z) = (Rxy , ¬∃z')
    where
    ¬∃z' : ¬ (∃[ z ] R x z × TransClosure R z y)
    ¬∃z' (z , Rxz , R⁺zy) =
      let Pz = ⁺-predˡ f R⁺zy Py
      in ¬∃z (with-pred z Pz , Rxz , ⁺-filter-relˡ f Pz Py R⁺zy)

  lemma⊇ : ∀ {x y : A} → (Px : P x) → (Py : P y)
    → TransClosure (immediate (filter-rel P R)) (with-pred x Px) (with-pred y Py)
    → TransClosure (immediate R) x y
  lemma⊇ Px Py [ iRxy ] = [ lemma⊇-imm Px Py iRxy ]
  lemma⊇ Px Py ( _∷_ {_} {with-pred z Pz} iRxz iR⁺zy ) = lemma⊇-imm Px Pz iRxz ∷ lemma⊇ Pz Py iR⁺zy

  ⊇-proof : TransClosure (immediate (filter-rel P R)) ⊆₂' filter-rel P R
  ⊇-proof (with-pred x Px) (with-pred y Py) Rxy = ⇔₂-apply-⊇₂ splitR (lemma⊇ Px Py Rxy)

-- | If any value in the chain of R satisfies P, it remains splittable after lifting.
--
-- The chain is traversed /to the right/.
filter-splittableʳ : ∀ {a ℓ : Level} {A : Set a} {R : Rel A ℓ}
  → SplittableOrder R
  → (P : Pred A ℓ)
  → (∀ {x y : A} → P x → R x y → P y)
    ---------------------------------
  → SplittableOrder (filter-rel P R)
filter-splittableʳ {A = A} {R = R} splitR P f = ⇔: ⊆-proof ⊇-proof
  where
  lemma⊆-imm : ∀ {x y : A} → (Px : P x) → (Py : P y) → immediate R x y → immediate (filter-rel P R) (with-pred x Px) (with-pred y Py)
  lemma⊆-imm {x} {y} Px Py (Rxy , ¬∃z) = Rxy , ¬∃z'
    where
    ¬∃z' : ¬ (∃[ z ] filter-rel P R (with-pred x Px) z × TransClosure (filter-rel P R) z (with-pred y Py))
    ¬∃z' (with-pred z Pz , Rxz , R⁺zy) = ¬∃z (z , Rxz , ⁺-strip-filter R⁺zy)

  lemma⊆ : ∀ {x y : A} → (Px : P x) → (Py : P y) → TransClosure (immediate R) x y
    → TransClosure (immediate (filter-rel P R)) (with-pred x Px) (with-pred y Py)
  lemma⊆ Px Py [ iRxy ] = [ lemma⊆-imm Px Py iRxy ]
  lemma⊆ Px Py ( iRxz ∷ iR⁺zy ) =
    let Pz = f Px (proj₁ iRxz)
    in lemma⊆-imm Px Pz iRxz ∷ lemma⊆ Pz Py iR⁺zy

  ⊆-proof : filter-rel P R ⊆₂' TransClosure (immediate (filter-rel P R))
  ⊆-proof (with-pred x Px) (with-pred y Py) Rxy = lemma⊆ Px Py (⇔₂-apply-⊆₂ splitR Rxy)

  lemma⊇-imm : ∀ {x y : A} → (Px : P x) → (Py : P y) → immediate (filter-rel P R) (with-pred x Px) (with-pred y Py)
    → immediate R x y
  lemma⊇-imm {x} {y} Px Py (Rxy , ¬∃z) = Rxy , ¬∃z'
    where
    ¬∃z' : ¬ (∃[ z ] R x z × TransClosure R z y)
    ¬∃z' (z , Rxz , R⁺zy) =
      let Pz = f Px Rxz
      in ¬∃z (with-pred z Pz , Rxz , ⁺-filter-relʳ f Pz Py R⁺zy)

  lemma⊇ : ∀ {x y : A} → (Px : P x) → (Py : P y)
    → TransClosure (immediate (filter-rel P R)) (with-pred x Px) (with-pred y Py)
    → TransClosure (immediate R) x y
  lemma⊇ Px Py [ iRxy ] = [ lemma⊇-imm Px Py iRxy ]
  lemma⊇ Px Py ( _∷_ {_} {with-pred z Pz} iRxz iR⁺zy ) = lemma⊇-imm Px Pz iRxz ∷ lemma⊇ Pz Py iR⁺zy

  ⊇-proof : TransClosure (immediate (filter-rel P R)) ⊆₂' filter-rel P R
  ⊇-proof (with-pred x Px) (with-pred y Py) Rxy = ⇔₂-apply-⊇₂ splitR (lemma⊇ Px Py Rxy)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
{-# OPTIONS --without-K #-}
{- The main definitions are the following:

  * exploreΣ
  * exploreΣ-ind
  * adequate-sumΣ
-}

open import Level.NP
open import Type hiding (★)
open import Type.Identities
open import Function.NP
open import Function.Extensionality
open import Data.Two
open import Data.Product.NP
open import Data.Fin
open import Relation.Binary.Logical
open import Relation.Binary.PropositionalEquality.NP using (_≡_ ; module ≡-Reasoning; !_; _∙_; coe; tr; ap; ap₂; J-orig)
open import HoTT
open import Category.Monad.Continuation.Alias

open import Explore.Core
open import Explore.Properties
import Explore.Monad as EM
open import Explore.Explorable

module Explore.Product where

module _ {m a b} {A : ★ a} {B : A → ★ b} where
    exploreΣ : Explore m A → (∀ {x} → Explore m (B x)) → Explore m (Σ A B)
    exploreΣ exploreᴬ exploreᴮ ε _⊕_ = exploreᴬ ε _⊕_ ⟨,⟩ exploreᴮ ε _⊕_

    module _ {eᴬ : Explore m A} {eᴮ : ∀ {x} → Explore m (B x)} where

        exploreΣ-ind : ∀ {p} → ExploreInd p eᴬ → (∀ {x} → ExploreInd p (eᴮ {x})) → ExploreInd p (exploreΣ eᴬ eᴮ)
        exploreΣ-ind Peᴬ Peᴮ P Pε P⊕ Pf =
          Peᴬ (λ e → P (λ _ _ _ → e _ _ _)) Pε P⊕ (λ x → Peᴮ {x} (λ e → P (λ _ _ _ → e _ _ _)) Pε P⊕ (curry Pf x))

module _
    {ℓ₀ ℓ₁ ℓᵣ}
    {a₀ a₁ aᵣ} {A₀ : ★ a₀} {A₁ : ★ a₁} {Aᵣ : ⟦★⟧ aᵣ A₀ A₁}
    {b₀ b₁ bᵣ} {B₀ : A₀ → ★ b₀} {B₁ : A₁ → ★ b₁} {Bᵣ : (Aᵣ ⟦→⟧ ⟦★⟧ bᵣ) B₀ B₁}
    {eᴬ₀ : Explore ℓ₀ A₀} {eᴬ₁ : Explore ℓ₁ A₁}(eᴬᵣ : ⟦Explore⟧ ℓᵣ Aᵣ eᴬ₀ eᴬ₁)
    {eᴮ₀ : ∀ {x} → Explore ℓ₀ (B₀ x)} {eᴮ₁ : ∀ {x} → Explore ℓ₁ (B₁ x)}(eᴮᵣ : ∀ {x₀ x₁}(x : Aᵣ x₀ x₁) → ⟦Explore⟧ ℓᵣ (Bᵣ x) (eᴮ₀ {x₀}) (eᴮ₁ {x₁}))
    where
   ⟦exploreΣ⟧ : ⟦Explore⟧ ℓᵣ (⟦Σ⟧ Aᵣ Bᵣ) (exploreΣ eᴬ₀ (λ {x} → eᴮ₀ {x})) (exploreΣ eᴬ₁ (λ {x} → eᴮ₁ {x}))
   ⟦exploreΣ⟧ P Pε P⊕ Pf = eᴬᵣ P Pε P⊕ (λ {x₀} {x₁} x → eᴮᵣ x P Pε P⊕ (λ xᵣ → Pf (x ⟦,⟧ xᵣ)))

module _
    {ℓ₀ ℓ₁ ℓᵣ}
    {a} {A : ★ a}
    {b} {B : A → ★ b}
    {eᴬ₀ : Explore ℓ₀ A} {eᴬ₁ : Explore ℓ₁ A}(eᴬᵣ : ⟦Explore⟧ ℓᵣ _≡_ eᴬ₀ eᴬ₁)
    {eᴮ₀ : ∀ {x} → Explore ℓ₀ (B x)} {eᴮ₁ : ∀ {x} → Explore ℓ₁ (B x)}
    (eᴮᵣ : ∀ x → ⟦Explore⟧ ℓᵣ _≡_ (eᴮ₀ {x}) (eᴮ₁ {x}))
    where
   ⟦exploreΣ⟧≡ : ⟦Explore⟧ ℓᵣ _≡_ (exploreΣ eᴬ₀ (λ {x} → eᴮ₀ {x})) (exploreΣ eᴬ₁ (λ {x} → eᴮ₁ {x}))
   ⟦exploreΣ⟧≡ P Pε P⊕ Pf = eᴬᵣ P Pε P⊕ λ x → J-orig _ (λ y → eᴮᵣ y P Pε P⊕ (Pf ∘ ap (_,_ y))) x

module _
    {ℓ₀ ℓ₁ ℓᵣ}
    {a} {A : ★ a}
    {b} {B : A → ★ b}
    {eᴬ₀ : Explore ℓ₀ A} {eᴬ₁ : Explore ℓ₁ A}(eᴬᵣ : ⟦Explore⟧ ℓᵣ _≡_ eᴬ₀ eᴬ₁)
    {eᴮ₀ : ∀ {x} → Explore ℓ₀ (B x)} {eᴮ₁ : ∀ {x} → Explore ℓ₁ (B x)}
    (eᴮᵣ : ∀ {x₀ x₁} (x : x₀ ≡ x₁) → ⟦Explore⟧ ℓᵣ (λ b₀ b₁ → tr B x b₀ ≡ b₁) (eᴮ₀ {x₀}) (eᴮ₁ {x₁}))
    where
   ⟦exploreΣ⟧↑≡ : ⟦Explore⟧ ℓᵣ _≡_ (exploreΣ eᴬ₀ (λ {x} → eᴮ₀ {x})) (exploreΣ eᴬ₁ (λ {x} → eᴮ₁ {x}))
   ⟦exploreΣ⟧↑≡ P Pε P⊕ Pf = eᴬᵣ P Pε P⊕ (λ x → eᴮᵣ x P Pε P⊕ (Pf ∘ pair= x))

module _ {A : ★₀} {B : A → ★₀} {sumᴬ : Sum A} {sumᴮ : ∀ {x} → Sum (B x)}{{_ : FunExt}}{{_ : UA}} where
    open Adequacy _≡_
    private
        sumᴬᴮ : Sum (Σ A B)
        sumᴬᴮ = sumᴬ ⟨,⟩ (λ {x} → sumᴮ {x})

    adequate-sumΣ : Adequate-sum sumᴬ → (∀ {x} → Adequate-sum (sumᴮ {x})) → Adequate-sum sumᴬᴮ
    adequate-sumΣ asumᴬ asumᴮ f
      = Fin (sumᴬᴮ f)
      ≡⟨by-definition⟩
        Fin (sumᴬ (λ a → sumᴮ (λ b → f (a , b))))
      ≡⟨ asumᴬ _ ⟩
        Σ A (λ a → Fin (sumᴮ (λ b → f (a , b))))
      ≡⟨ Σ=′ _ (λ _ → asumᴮ _) ⟩
        Σ A (λ a → Σ (B a) (λ b → Fin (f (a , b))))
      ≡⟨ Σ-assoc ⟩
        Σ (Σ A B) (Fin ∘ f)
      ∎
      where open ≡-Reasoning

-- From now on, these are derived definitions for convenience and pedagogical reasons

explore× : ∀ {m a b} {A : ★ a} {B : ★ b} → Explore m A → Explore m B → Explore m (A × B)
explore× exploreᴬ exploreᴮ = exploreΣ exploreᴬ exploreᴮ

explore×-ind : ∀ {m p a b} {A : ★ a} {B : ★ b} {eᴬ : Explore m A} {eᴮ : Explore m B}
               → ExploreInd p eᴬ → ExploreInd p eᴮ
               → ExploreInd p (explore× eᴬ eᴮ)
explore×-ind Peᴬ Peᴮ = exploreΣ-ind Peᴬ Peᴮ

sumΣ : ∀ {a b} {A : ★ a} {B : A → ★ b} → Sum A → (∀ {x} → Sum (B x)) → Sum (Σ A B)
sumΣ = _⟨,⟩_

sum× : ∀ {a b} {A : ★ a} {B : ★ b} → Sum A → Sum B → Sum (A × B)
sum× = _⟨,⟩′_

module _ {ℓ₀ ℓ₁ ℓᵣ A₀ A₁ B₀ B₁}
         {Aᵣ  : ⟦★₀⟧ A₀ A₁}
         {Bᵣ  : ⟦★₀⟧ B₀ B₁}
         {eᴬ₀ : Explore ℓ₀ A₀} {eᴬ₁ : Explore ℓ₁ A₁}(eᴬᵣ : ⟦Explore⟧ ℓᵣ Aᵣ eᴬ₀ eᴬ₁)
         {eᴮ₀ : Explore ℓ₀ B₀} {eᴮ₁ : Explore ℓ₁ B₁}(eᴮᵣ : ⟦Explore⟧ ℓᵣ Bᵣ eᴮ₀ eᴮ₁)
    where
    ⟦explore×⟧ : ⟦Explore⟧ ℓᵣ (Aᵣ ⟦×⟧ Bᵣ) (explore× eᴬ₀ eᴮ₀) (explore× eᴬ₁ eᴮ₁)
    ⟦explore×⟧ P Pε P⊕ Pf = eᴬᵣ P Pε P⊕ (λ x → eᴮᵣ P Pε P⊕ (λ y → Pf (_⟦,⟧_ x y)))

module _ {ℓ₀ ℓ₁ ℓᵣ} {A B : ★₀}
         {eᴬ₀ : Explore ℓ₀ A} {eᴬ₁ : Explore ℓ₁ A}(eᴬᵣ : ⟦Explore⟧ ℓᵣ _≡_ eᴬ₀ eᴬ₁)
         {eᴮ₀ : Explore ℓ₀ B} {eᴮ₁ : Explore ℓ₁ B}(eᴮᵣ : ⟦Explore⟧ ℓᵣ _≡_ eᴮ₀ eᴮ₁)
    where
    ⟦explore×⟧≡ : ⟦Explore⟧ ℓᵣ _≡_ (explore× eᴬ₀ eᴮ₀) (explore× eᴬ₁ eᴮ₁)
    ⟦explore×⟧≡ P Pε P⊕ Pf = eᴬᵣ P Pε P⊕ (λ x → eᴮᵣ P Pε P⊕ (λ y → Pf (ap₂ _,_ x y)))

{-
μΣ : ∀ {A} {B : A → ★ _} → Explorable A → (∀ {x} → Explorable (B x)) → Explorable (Σ A B)
μΣ μA μB = mk _ (exploreΣ-ind (explore-ind μA) (explore-ind μB))
                (adequate-sumΣ (adequate-sum μA) (adequate-sum μB))

infixr 4 _×-μ_
_×-μ_ : ∀ {A B} → Explorable A → Explorable B → Explorable (A × B)
μA ×-μ μB = μΣ μA μB

_×-cmp_ : ∀ {A B : ★₀ } → Cmp A → Cmp B → Cmp (A × B)
(ca ×-cmp cb) (a , b) (a' , b') = ca a a' ∧ cb b b'

×-unique : ∀ {A B}(μA : Explorable A)(μB : Explorable B)(cA : Cmp A)(cB : Cmp B)
           → Unique cA (count μA) → Unique cB (count μB) → Unique (cA ×-cmp cB) (count (μA ×-μ μB))
×-unique μA μB cA cB uA uB (x , y) = count (μA ×-μ μB) ((cA ×-cmp cB) (x , y)) ≡⟨ explore-ext μA _ (λ x' → help (cA x x')) ⟩
                                     count μA (cA x) ≡⟨ uA x ⟩
                                     1 ∎
  where
    open ≡-Reasoning
    help : ∀ b → count μB (λ y' → b ∧ cB y y') ≡ (if b then 1 else 0)
    help = [0: sum-zero μB 1: uB y ]
-}

{-
module _ {A} {Aₚ : A → ★₀} {B : A → _} {eᴬ : Explore ₁ A} (eᴬₚ : [Explore] _ _ Aₚ eᴬ) (eᴬ-ind : ExploreInd (ₛ ₀) eᴬ) {eᴮ : ∀ {x} → Explore ₀ (B x)} where
  open import Explore.One
  --open import Explore.Product
  exploreΠᵉ : Explore ₀ (Πᵉ eᴬ B)
  exploreΠᵉ = eᴬ-ind (λ e → Explore ₀ (Πᵉ e B)) (λ ε _∙₁_ x → x _) explore× (λ x → eᴮ {x})

  exploreΠᵉ' : Explore ₀ (Πᵉ eᴬ B)
  exploreΠᵉ' = λ {M} ε _∙₁_ x → {!eᴬₚ (const (Lift M))!}

  exploreΠᵉ-ind : ExploreInd ₁ exploreΠᵉ
  exploreΠᵉ-ind = {!⟦Explore⟧ᵤ _ _ _ eᴬ!}
-}

module _ {ℓ a b} {A : ★ a} {B : A → ★ b} {eᴬ : Explore (ₛ ℓ) A} {eᴮ : ∀ {x} → Explore (ₛ ℓ) (B x)} where
  private
    eᴬᴮ = exploreΣ eᴬ λ {x} → eᴮ {x}

  focusΣ : Focus eᴬ → (∀ {x} → Focus (eᴮ {x})) → Focus eᴬᴮ
  focusΣ fᴬ fᴮ ((x , y) , z) = fᴬ (x , fᴮ (y , z))

  lookupΣ : Lookup eᴬ → (∀ {x} → Lookup (eᴮ {x})) → Lookup eᴬᴮ
  lookupΣ lookupᴬ lookupᴮ d = uncurry (lookupᴮ ∘ lookupᴬ d)

  -- can also be derived from explore-ind
  reifyΣ : Reify eᴬ → (∀ {x} → Reify (eᴮ {x})) → Reify eᴬᴮ
  reifyΣ reifyᴬ reifyᴮ f = reifyᴬ (reifyᴮ ∘ curry f)

module _ {ℓ} {A : ★₀} {B : A → ★₀}
         {eᴬ : Explore (ₛ ℓ) A} {eᴮ : ∀ {x} → Explore (ₛ ℓ) (B x)}
         {{_ : UA}}{{_ : FunExt}} where
  private
    eᴬᴮ = exploreΣ eᴬ λ {x} → eᴮ {x}

  ΣᵉΣ-ok : Adequate-Σ (Σᵉ eᴬ) → (∀ {x} → Adequate-Σ (Σᵉ (eᴮ {x}))) → Adequate-Σ (Σᵉ eᴬᴮ)
  ΣᵉΣ-ok eᴬ eᴮ f = eᴬ _ ∙ Σ=′ _ (λ _ → eᴮ _) ∙ Σ-assoc

  ΠᵉΣ-ok : Adequate-Π (Πᵉ eᴬ) → (∀ {x} → Adequate-Π (Πᵉ (eᴮ {x}))) → Adequate-Π (Πᵉ eᴬᴮ)
  ΠᵉΣ-ok eᴬ eᴮ f = eᴬ _ ∙ Π=′ _ (λ _ → eᴮ _) ∙ ! ΠΣ-curry

module _ {ℓ a b} {A : ★ a} {B : ★ b} {eᴬ : Explore (ₛ ℓ) A} {eᴮ : Explore (ₛ ℓ) B} where
  private
    eᴬᴮ = explore× eᴬ eᴮ

  focus× : Focus eᴬ → Focus eᴮ → Focus eᴬᴮ
  focus× fᴬ fᴮ = focusΣ {eᴬ = eᴬ} {eᴮ = eᴮ} fᴬ fᴮ

  lookup× : Lookup eᴬ → Lookup eᴮ → Lookup eᴬᴮ
  lookup× fᴬ fᴮ = lookupΣ {eᴬ = eᴬ} {eᴮ = eᴮ} fᴬ fᴮ

module _ {ℓ} {A B : ★₀} {eᴬ : Explore (ₛ ℓ) A} {eᴮ : Explore (ₛ ℓ) B} where
  private
    eᴬᴮ = explore× eᴬ eᴮ

  Σᵉ×-ok : {{_ : UA}}{{_ : FunExt}} → Adequate-Σ (Σᵉ eᴬ) → Adequate-Σ (Σᵉ eᴮ) → Adequate-Σ (Σᵉ eᴬᴮ)
  Σᵉ×-ok eᴬ eᴮ f = eᴬ _ ∙ Σ=′ _ (λ _ → eᴮ _) ∙ Σ-assoc

  Πᵉ×-ok : {{_ : UA}}{{_ : FunExt}} → Adequate-Π (Πᵉ eᴬ) → Adequate-Π (Πᵉ eᴮ) → Adequate-Π (Πᵉ eᴬᴮ)
  Πᵉ×-ok eᴬ eᴮ f = eᴬ _ ∙ Π=′ _ (λ _ → eᴮ _) ∙ ! ΠΣ-curry

module Operators where
    infixr 4 _×ᵉ_ _×ⁱ_ _×ˢ_
    _×ᵉ_ = explore×
    _×ⁱ_ = explore×-ind
    _×ᵃ_ = adequate-sumΣ
    _×ˢ_ = sum×
    _×ᶠ_ = focus×
    _×ˡ_ = lookup×

-- Those are here only for pedagogical use
private
    fst-explore : ∀ {m} {A : ★₀} {B : A → ★₀} → Explore m (Σ A B) → Explore m A
    fst-explore = EM.map _ fst

    snd-explore : ∀ {m} {A B : ★₀} → Explore m (A × B) → Explore m B
    snd-explore = EM.map _ snd

    sum'Σ : ∀ {A : ★₀} {B : A → ★₀} → Sum A → (∀ x → Sum (B x)) → Sum (Σ A B)
    sum'Σ sumᴬ sumᴮ f = sumᴬ (λ x₀ →
                          sumᴮ x₀ (λ x₁ →
                            f (x₀ , x₁)))

    explore×' : ∀ {A B : ★₀} → Explore₀ A → Explore _ B → Explore _ (A × B)
    explore×' exploreᴬ exploreᴮ ε _⊕_ f = exploreᴬ ε _⊕_ (λ x → exploreᴮ ε _⊕_ (curry f x))

    explore×-ind' : ∀ {A B} {eᴬ : Explore _ A} {eᴮ : Explore _ B}
                    → ExploreInd₀ eᴬ → ExploreInd₀ eᴮ → ExploreInd₀ (explore×' eᴬ eᴮ)
    explore×-ind' Peᴬ Peᴮ P Pε P⊕ Pf =
      Peᴬ (λ e → P (λ _ _ _ → e _ _ _)) Pε P⊕ (Peᴮ (λ e → P (λ _ _ _ → e _ _ _)) Pε P⊕ ∘ curry Pf)

    -- liftM2 _,_ in the continuation monad
    sum×' : ∀ {A B : ★₀} → Sum A → Sum B → Sum (A × B)
    sum×' sumᴬ sumᴮ f = sumᴬ λ x₀ →
                          sumᴮ λ x₁ →
                            f (x₀ , x₁)
-- -}
-- -}
-- -}

ext: agda

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
{-# OPTIONS --without-K #-}
module sets.vec.dependent where

open import sets.nat.core
open import sets.fin.core

-- syntactic sugar to create finite dependent functions

⟦⟧ : ∀ {i}{P : Fin 0 → Set i} → (i : Fin 0) → P i
⟦⟧ ()

_∷∷_ : ∀ {i n}{P : Fin (suc n) → Set i}
    → (x : P zero)(xs : (i : Fin n) → P (suc i))
    → (i : Fin (suc n)) → P i
_∷∷_ {P = P} x xs zero = x
_∷∷_ {P = P} x xs (suc i) = xs i

infixr 5 _∷∷_

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
open import Nat
open import Prelude
open import core
open import contexts

open import progress
open import preservation
open import elaborability
open import typed-elaboration

module continuity where
  -- we take the sensibilty theorem as a postulate; for a proof, refer to
  -- the POPL17 mechanization. we also postulate some glue that allows us
  -- to use our theorems here on the shape of results from that work.
  postulate
    action : Set
    zexp : Set
    _◆ : zexp → hexp
    _⊢_=>_~_~>_=>_ : (Γ : tctx) → (e1 : zexp) → (t1 : htyp)
                        → (α : action) → (e2 : zexp) → (t2 : htyp) → Set
    sensibility : {Γ : tctx} {e e' : zexp} {τ τ' : htyp} {α : action} →
                  Γ ⊢ (e ◆) => τ →
                  Γ ⊢ e => τ ~ α ~> e' => τ' →
                  Γ ⊢ (e' ◆) => τ'
    binders-unique-h : hexp → Set
    binders-unique-z : zexp → Set
    binders-unique-cursor1 : ∀{e} → binders-unique-z e → binders-unique-h (e ◆)
    binders-unique-cursor2 : ∀{e} → binders-unique-h (e ◆) → binders-unique-z e
    binders-unique-sensibility : {Γ : tctx} {e e' : zexp} {τ τ' : htyp} {α : action} →
                  binders-unique-z e →
                  Γ ⊢ e => τ ~ α ~> e' => τ' →
                  binders-unique-z e'
    expansion-unique : ∀{Γ e τ d Δ} →
                       binders-unique-h e →
                       Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                       binders-unique d

  continuity : ∀{ e τ α e' τ' }
             → binders-unique-z e
             → ∅ ⊢ (e ◆) => τ
             → ∅ ⊢ e => τ ~ α ~> e' => τ'
             → Σ[ Δ ∈ hctx ] Σ[ d ∈ ihexp ]
                (   ∅ ⊢ (e' ◆) ⇒ τ' ~> d ⊣ Δ
                  × Δ , ∅ ⊢ d :: τ'
                  × ( (Σ[ d' ∈ ihexp ]( d ↦ d' × Δ , ∅ ⊢ d' :: τ' ))
                     + d boxedval
                     + d indet
                    )
                )
  continuity bu wt action with sensibility wt action
  ... | sense with elaborability-synth sense
  ... | d , Δ , exp with typed-elaboration-synth exp
  ... | d::τ' with progress d::τ'
  ... | (S (d' , stp)) =  Δ , d , exp , d::τ' , Inl (d' , stp , preservation (expansion-unique (binders-unique-cursor1 (binders-unique-sensibility bu action)) exp) d::τ' stp)
  ... | (I ind) = Δ , d , exp , d::τ' , Inr (Inr ind)
  ... | (BV boxed) = Δ , d , exp , d::τ' , Inr (Inl boxed)

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
record R : Set₁ where
  X = Set Set   -- should get error here
  field A : Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Erased-cubical-Open-public.Erased (_ : Set₁) where

postulate
  A : Set

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

open import lib.Basics
open import lib.types.Coproduct
open import lib.types.Fin
open import lib.types.Int
open import lib.types.Nat
open import lib.types.Pi

module lib.types.Group where

-- 1-approximation of groups without higher coherence conditions.
record GroupStructure {i} (El : Type i) --(El-level : has-level 0 El)
  : Type i where
  constructor group-structure
  field
    ident  : El
    inv    : El → El
    comp   : El → El → El
    unit-l : ∀ a → comp ident a == a
    assoc  : ∀ a b c → comp (comp a b) c == comp a (comp b c)
    inv-l  : ∀ a → (comp (inv a) a) == ident

  ⊙El : Ptd i
  ⊙El = ⊙[ El , ident ]

  private
    infix 80 _⊙_
    _⊙_ = comp

  abstract
    inv-r  : ∀ g → g ⊙ inv g == ident
    inv-r g =
      g ⊙ inv g                           =⟨ ! $ unit-l (g ⊙ inv g) ⟩
      ident ⊙ (g ⊙ inv g)                 =⟨ ! $ inv-l (inv g) |in-ctx _⊙ (g ⊙ inv g) ⟩
      (inv (inv g) ⊙ inv g) ⊙ (g ⊙ inv g) =⟨ assoc (inv (inv g)) (inv g) (g ⊙ inv g) ⟩
      inv (inv g) ⊙ (inv g ⊙ (g ⊙ inv g)) =⟨ ! $ assoc (inv g) g (inv g) |in-ctx inv (inv g) ⊙_ ⟩
      inv (inv g) ⊙ ((inv g ⊙ g) ⊙ inv g) =⟨ inv-l g |in-ctx (λ h → inv (inv g) ⊙ (h ⊙ inv g)) ⟩
      inv (inv g) ⊙ (ident ⊙ inv g)       =⟨ unit-l (inv g) |in-ctx inv (inv g) ⊙_ ⟩
      inv (inv g) ⊙ inv g                 =⟨ inv-l (inv g) ⟩
      ident                               =∎

    unit-r : ∀ g → g ⊙ ident == g
    unit-r g =
      g ⊙ ident          =⟨ ! (inv-l g) |in-ctx g ⊙_ ⟩
      g ⊙ (inv g ⊙ g)    =⟨ ! $ assoc g (inv g) g ⟩
      (g ⊙ inv g) ⊙ g    =⟨ inv-r g |in-ctx _⊙ g ⟩
      ident ⊙ g          =⟨ unit-l g ⟩
      g                  =∎

    inv-unique-l : (g h : El) → (g ⊙ h == ident) → inv h == g
    inv-unique-l g h p =
      inv h              =⟨ ! (unit-l (inv h)) ⟩
      ident ⊙ inv h      =⟨ ! p |in-ctx (λ w → w ⊙ inv h) ⟩
      (g ⊙ h) ⊙ inv h    =⟨ assoc g h (inv h) ⟩
      g ⊙ (h ⊙ inv h)    =⟨ inv-r h |in-ctx (λ w → g ⊙ w) ⟩
      g ⊙ ident          =⟨ unit-r g ⟩
      g                  =∎

    inv-unique-r : (g h : El) → (g ⊙ h == ident) → inv g == h
    inv-unique-r g h p =
      inv g              =⟨ ! (unit-r (inv g)) ⟩
      inv g ⊙ ident      =⟨ ! p |in-ctx (λ w → inv g ⊙ w) ⟩
      inv g ⊙ (g ⊙ h)    =⟨ ! (assoc (inv g) g h) ⟩
      (inv g ⊙ g) ⊙ h    =⟨ inv-l g |in-ctx (λ w → w ⊙ h) ⟩
      ident ⊙ h          =⟨ unit-l h ⟩
      h                  =∎

    inv-ident : inv ident == ident
    inv-ident = inv-unique-l ident ident (unit-l ident)

    inv-comp : (g₁ g₂ : El) → inv (g₁ ⊙ g₂) == inv g₂ ⊙ inv g₁
    inv-comp g₁ g₂ =
      inv-unique-r (g₁ ⊙ g₂) (inv g₂ ⊙ inv g₁) $
        (g₁ ⊙ g₂) ⊙ (inv g₂ ⊙ inv g₁)
          =⟨ assoc g₁ g₂ (inv g₂ ⊙ inv g₁) ⟩
        g₁ ⊙ (g₂ ⊙ (inv g₂ ⊙ inv g₁))
          =⟨ ! (assoc g₂ (inv g₂) (inv g₁)) |in-ctx (λ w → g₁ ⊙ w) ⟩
        g₁ ⊙ ((g₂ ⊙ inv g₂) ⊙ inv g₁)
          =⟨ inv-r g₂ |in-ctx (λ w → g₁ ⊙ (w ⊙ inv g₁)) ⟩
        g₁ ⊙ (ident ⊙ inv g₁)
          =⟨ unit-l (inv g₁) |in-ctx (λ w → g₁ ⊙ w) ⟩
        g₁ ⊙ inv g₁
          =⟨ inv-r g₁ ⟩
        ident =∎

    inv-inv : (g : El) → inv (inv g) == g
    inv-inv g = inv-unique-r (inv g) g (inv-l g)

    inv-is-inj : is-inj inv
    inv-is-inj g₁ g₂ p = ! (inv-inv g₁) ∙ ap inv p ∙ inv-inv g₂

    cancel-l : (g : El) {h k : El} → g ⊙ h == g ⊙ k → h == k
    cancel-l g {h} {k} p =
      h                  =⟨ ! (unit-l h) ⟩
      ident ⊙ h          =⟨ ap (λ w → w ⊙ h) (! (inv-l g)) ⟩
      (inv g ⊙ g) ⊙ h    =⟨ assoc (inv g) g h ⟩
      inv g ⊙ (g ⊙ h)    =⟨ ap (λ w → inv g ⊙ w) p ⟩
      inv g ⊙ (g ⊙ k)    =⟨ ! (assoc (inv g) g k) ⟩
      (inv g ⊙ g) ⊙ k    =⟨ ap (λ w → w ⊙ k) (inv-l g) ⟩
      ident ⊙ k          =⟨ unit-l k ⟩
      k =∎

    cancel-r : (g : El) {h k : El} → h ⊙ g == k ⊙ g → h == k
    cancel-r g {h} {k} p =
      h                  =⟨ ! (unit-r h) ⟩
      h ⊙ ident          =⟨ ap (λ w → h ⊙ w) (! (inv-r g)) ⟩
      h ⊙ (g ⊙ inv g)    =⟨ ! (assoc h g (inv g)) ⟩
      (h ⊙ g) ⊙ inv g    =⟨ ap (λ w → w ⊙ inv g) p ⟩
      (k ⊙ g) ⊙ inv g    =⟨ assoc k g (inv g) ⟩
      k ⊙ (g ⊙ inv g)    =⟨ ap (λ w → k ⊙ w) (inv-r g) ⟩
      k ⊙ ident          =⟨ unit-r k ⟩
      k =∎

  conj : El → El → El
  conj g₁ g₂ = (g₁ ⊙ g₂) ⊙ inv g₁

  abstract
    conj-ident-r : ∀ g → conj g ident == ident
    conj-ident-r g = ap (_⊙ inv g) (unit-r _) ∙ inv-r g
  {- NOT USED
  abstract
    conj-unit-l : ∀ g → conj ident g == g
    conj-unit-l g = ap2 _⊙_ (unit-l _) inv-ident ∙ unit-r _

    conj-comp-l : ∀ g₁ g₂ g₃ → conj (g₁ ⊙ g₂) g₃ == conj g₁ (conj g₂ g₃)
    conj-comp-l g₁ g₂ g₃ =
      ((g₁ ⊙ g₂) ⊙ g₃) ⊙ inv (g₁ ⊙ g₂)
        =⟨ ap2 _⊙_ (assoc g₁ g₂ g₃) (inv-comp g₁ g₂) ⟩
      (g₁ ⊙ (g₂ ⊙ g₃)) ⊙ (inv g₂ ⊙ inv g₁)
        =⟨ ! $ assoc (g₁ ⊙ (g₂ ⊙ g₃)) (inv g₂) (inv g₁) ⟩
      ((g₁ ⊙ (g₂ ⊙ g₃)) ⊙ inv g₂) ⊙ inv g₁
        =⟨ assoc g₁ (g₂ ⊙ g₃) (inv g₂) |in-ctx _⊙ inv g₁ ⟩
      (g₁ ⊙ ((g₂ ⊙ g₃) ⊙ inv g₂)) ⊙ inv g₁
        =∎

    inv-conj : ∀ g₁ g₂ → inv (conj g₁ g₂) == conj g₁ (inv g₂)
    inv-conj g₁ g₂ = inv-comp (g₁ ⊙ g₂) (inv g₁)
                   ∙ ap2 _⊙_ (inv-inv g₁) (inv-comp g₁ g₂)
                   ∙ ! (assoc g₁ (inv g₂) (inv g₁))
  -}

  exp : El → ℤ → El
  exp g (pos 0) = ident
  exp g (pos 1) = g
  exp g (pos (S (S n))) = comp g (exp g (pos (S n)))
  exp g (negsucc 0) = inv g
  exp g (negsucc (S n)) = comp (inv g) (exp g (negsucc n))

  abstract
    exp-succ : ∀ g z → exp g (succ z) == comp g (exp g z)
    exp-succ g (pos 0) = ! (unit-r g)
    exp-succ g (pos 1) = idp
    exp-succ g (pos (S (S n))) = idp
    exp-succ g (negsucc 0) = ! (inv-r g)
    exp-succ g (negsucc (S n)) =
      ! (unit-l (exp g (negsucc n)))
      ∙ ap (λ h → comp h (exp g (negsucc n))) (! (inv-r g))
      ∙ assoc g (inv g) (exp g (negsucc n))

    exp-pred : ∀ g z → exp g (pred z) == comp (inv g) (exp g z)
    exp-pred g (pos 0) = ! (unit-r (inv g))
    exp-pred g (pos 1) = ! (inv-l g)
    exp-pred g (pos (S (S n))) =
      ! (unit-l (exp g (pos (S n))))
      ∙ ap (λ h → comp h (exp g (pos (S n)))) (! (inv-l g))
      ∙ assoc (inv g) g (exp g (pos (S n)))
    exp-pred g (negsucc 0) = idp
    exp-pred g (negsucc (S n)) = idp

    exp-+ : ∀ g z₁ z₂ → exp g (z₁ ℤ+ z₂) == comp (exp g z₁) (exp g z₂)
    exp-+ g (pos 0) z₂ = ! (unit-l _)
    exp-+ g (pos 1) z₂ = exp-succ g z₂
    exp-+ g (pos (S (S n))) z₂ =
      exp-succ g (pos (S n) ℤ+ z₂)
      ∙ ap (comp g) (exp-+ g (pos (S n)) z₂)
      ∙ ! (assoc g (exp g (pos (S n))) (exp g z₂))
    exp-+ g (negsucc 0) z₂ = exp-pred g z₂
    exp-+ g (negsucc (S n)) z₂ =
      exp-pred g (negsucc n ℤ+ z₂)
      ∙ ap (comp (inv g)) (exp-+ g (negsucc n) z₂)
      ∙ ! (assoc (inv g) (exp g (negsucc n)) (exp g z₂))

  exp-ident : ∀ z → exp ident z == ident
  exp-ident (pos 0) = idp
  exp-ident (pos 1) = idp
  exp-ident (pos (S (S n))) = unit-l _ ∙ exp-ident (pos (S n))
  exp-ident (negsucc 0) = inv-ident
  exp-ident (negsucc (S n)) = ap2 comp inv-ident (exp-ident (negsucc n)) ∙ unit-l _

  diff : El → El → El
  diff g h = g ⊙ inv h

  abstract
    zero-diff-same : (g h : El) → diff g h == ident → g == h
    zero-diff-same g h p = inv-is-inj g h $ inv-unique-r g (inv h) p

    inv-diff : (g h : El) → inv (diff g h) == diff h g
    inv-diff g h = inv-comp g (inv h) ∙ ap (_⊙ inv g) (inv-inv h)

  sum : ∀ {I : ℕ} → (Fin I → El) → El
  sum {I = O} f = ident
  sum {I = S n} f = comp (sum (f ∘ Fin-S)) (f (n , ltS))

  subsum-r : ∀ {j k} {I : ℕ} {A : Type j} {B : Type k}
    → (Fin I → Coprod A B) → (B → El) → El
  subsum-r p f = sum (λ x → ⊔-rec (λ _ → ident) f (p x))

record Group i : Type (lsucc i) where
  constructor group
  field
    El : Type i
    {{El-level}} : has-level 0 El
    group-struct : GroupStructure El
  open GroupStructure group-struct public

Group₀ : Type (lsucc lzero)
Group₀ = Group lzero

is-abelian : ∀ {i} → Group i → Type i
is-abelian G = (a b : Group.El G) → Group.comp G a b == Group.comp G b a

AbGroup : ∀ i → Type (lsucc i)
AbGroup i = Σ (Group i) is-abelian

AbGroup₀ : Type (lsucc lzero)
AbGroup₀ = AbGroup lzero

module AbGroup {i} (G : AbGroup i) where
  grp = fst G
  comm = snd G
  open Group grp public

  abstract
    interchange : (g₁ g₂ g₃ g₄ : El) →
        comp (comp g₁ g₂) (comp g₃ g₄)
        == comp (comp g₁ g₃) (comp g₂ g₄)
    interchange g₁ g₂ g₃ g₄ =
      comp (comp g₁ g₂) (comp g₃ g₄)
        =⟨ assoc g₁ g₂ (comp g₃ g₄) ⟩
      comp g₁ (comp g₂ (comp g₃ g₄))
        =⟨ comm g₃ g₄ |in-ctx (λ g → (comp g₁ (comp g₂ g))) ⟩
      comp g₁ (comp g₂ (comp g₄ g₃))
        =⟨ ! (assoc g₂ g₄ g₃) |in-ctx comp g₁ ⟩
      comp g₁ (comp (comp g₂ g₄) g₃)
        =⟨ comm (comp g₂ g₄) g₃ |in-ctx comp g₁ ⟩
      comp g₁ (comp g₃ (comp g₂ g₄))
        =⟨ ! (assoc g₁ g₃ (comp g₂ g₄)) ⟩
      comp (comp g₁ g₃) (comp g₂ g₄)
        =∎

    inv-comp' : ∀ g₁ g₂ → inv (comp g₁ g₂) == comp (inv g₁) (inv g₂)
    inv-comp' g₁ g₂ = inv-comp g₁ g₂ ∙ comm (inv g₂) (inv g₁)

    diff-comp : (g₁ g₂ g₃ g₄ : El) →
        diff (comp g₁ g₂) (comp g₃ g₄)
        == comp (diff g₁ g₃) (diff g₂ g₄)
    diff-comp g₁ g₂ g₃ g₄ =
        diff (comp g₁ g₂) (comp g₃ g₄)
          =⟨ ap (comp (comp g₁ g₂)) (inv-comp' g₃ g₄) ⟩
        comp (comp g₁ g₂) (comp (inv g₃) (inv g₄))
          =⟨ interchange g₁ g₂ (inv g₃) (inv g₄) ⟩
        comp (diff g₁ g₃) (diff g₂ g₄)
          =∎

    sum-comp : ∀ {I} (f g : Fin I → El)
      → sum (λ x → comp (f x) (g x)) == comp (sum f) (sum g)
    sum-comp {I = O} f g = ! (unit-l _)
    sum-comp {I = S I} f g =
        ap (λ x → comp x (comp (f (I , ltS)) (g (I , ltS)))) (sum-comp (f ∘ Fin-S) (g ∘ Fin-S))
      ∙ interchange (sum (f ∘ Fin-S)) (sum (g ∘ Fin-S)) (f (I , ltS)) (g (I , ltS))

    exp-comp : ∀ g₁ g₂ z → exp (comp g₁ g₂) z == comp (exp g₁ z) (exp g₂ z)
    exp-comp g₁ g₂ (pos O) = ! (unit-l _)
    exp-comp g₁ g₂ (pos (S O)) = idp
    exp-comp g₁ g₂ (pos (S (S n))) =
        ap (comp (comp g₁ g₂)) (exp-comp g₁ g₂ (pos (S n)))
      ∙ interchange g₁ g₂ (exp g₁ (pos (S n))) (exp g₂ (pos (S n)))
    exp-comp g₁ g₂ (negsucc O) = inv-comp' g₁ g₂
    exp-comp g₁ g₂ (negsucc (S n)) =
        ap2 comp (inv-comp' g₁ g₂) (exp-comp g₁ g₂ (negsucc n))
      ∙ interchange (inv g₁) (inv g₂) (exp g₁ (negsucc n)) (exp g₂ (negsucc n))

is-trivialᴳ : ∀ {i} (G : Group i) → Type i
is-trivialᴳ G = ∀ g → g == Group.ident G

contr-is-trivialᴳ : ∀ {i} (G : Group i)
  {{_ : is-contr (Group.El G)}} → is-trivialᴳ G
contr-is-trivialᴳ G g =
  contr-has-all-paths _ _

{- group-structure= -}

module _ where
  open GroupStructure

  abstract
    group-structure= : ∀ {i} {A : Type i} {{_ : is-set A}}
      {id₁ id₂ : A} {inv₁ inv₂ : A → A} {comp₁ comp₂ : A → A → A}
      → ∀ {unit-l₁ unit-l₂ assoc₁ assoc₂ inv-l₁ inv-l₂}
      → (id₁ == id₂) → (inv₁ == inv₂) → (comp₁ == comp₂)
      → Path {A = GroupStructure A}
          (group-structure id₁ inv₁ comp₁ unit-l₁ assoc₁ inv-l₁)
          (group-structure id₂ inv₂ comp₂ unit-l₂ assoc₂ inv-l₂)
    group-structure= {id₁ = id₁} {inv₁ = inv₁} {comp₁ = comp₁} idp idp idp =
      ap3 (group-structure id₁ inv₁ comp₁)
        (prop-has-all-paths _ _)
        (prop-has-all-paths _ _)
        (prop-has-all-paths _ _)

    ↓-group-structure= : ∀ {i} {A B : Type i}
      {{_ : has-level 0 A}}
      {GS : GroupStructure A} {HS : GroupStructure B} (p : A == B)
      → (ident GS == ident HS [ (λ C → C) ↓ p ])
      → (inv GS == inv HS [ (λ C → C → C) ↓ p ])
      → (comp GS == comp HS [ (λ C → C → C → C) ↓ p ])
      → GS == HS [ GroupStructure ↓ p ]
    ↓-group-structure= idp = group-structure=

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Cats.Category.Mon where

open import Data.Unit using (⊤)
open import Relation.Binary using (Setoid ; _Preserves₂_⟶_⟶_ ; IsEquivalence)
open import Level

open import Cats.Category
open import Cats.Category.Setoids using (Setoids)
open import Cats.Util.Conv

import Cats.Util.Function as Fun

record Monoid l l≈ : Set (suc (l ⊔ l≈)) where
  infixr 9 _⊕_

  field
    Universe : Setoid l l≈

  open Setoid Universe public

  field
    _⊕_ : Carrier → Carrier → Carrier
    unit : Carrier

    ⊕-resp : _⊕_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
    assoc : ∀ {a b c} → (a ⊕ b) ⊕ c ≈ a ⊕ (b ⊕ c)
    id-l : ∀ {a} → unit ⊕ a ≈ a
    id-r : ∀ {a} → a ⊕ unit ≈ a

  module ≈ = IsEquivalence isEquivalence

module _ (l l≈ : Level) where

  infixr 9 _∘_
  infixr 4 _≈_

  module Setoids = Category (Setoids l l≈)

  Obj : Set (suc (l ⊔ l≈))
  Obj = Monoid l l≈

  record _⇒_ (M N : Obj) : Set (l ⊔ l≈) where
    private
      module M = Monoid M
      module N = Monoid N

    field
      arr : M.Universe Setoids.⇒ N.Universe
      unit : (arr ⃗) M.unit N.≈ N.unit
      commute : ∀ {n m} → (arr ⃗) (n M.⊕ m) N.≈ (arr ⃗) n N.⊕ (arr ⃗) m

    open Cats.Category.Setoids._⇒_ arr public using (resp)

  open _⇒_ using (unit ; commute ; resp)

  instance
    HasArrow-⇒ : ∀ M N → HasArrow (M ⇒ N) _ _ _
    HasArrow-⇒ M N = record { Cat = Setoids l l≈ ; _⃗ = _⇒_.arr }

  id : ∀ {M} → M ⇒ M
  id {M} = record
      { arr = Setoids.id
      ; unit = refl
      ; commute = refl
      }
    where
      open Monoid M using (refl)

  _≈_ : ∀ {M N} (f g : M ⇒ N) → Set (l≈ ⊔ l)
  _≈_ = Setoids._≈_ Fun.on _⃗

  _∘_ : ∀ {M N O} → (N ⇒ O) → (M ⇒ N) → (M ⇒ O)
  _∘_ {M} {N} {O} f g = record
      { arr = f ⃗ Setoids.∘ g ⃗
      ; unit = trans (resp f (unit g)) (unit f)
      ; commute = trans (resp f (commute g)) (commute f)
      }
    where
      open Monoid O using (trans)

  Mon : Category (suc (l≈ ⊔ l)) (l≈ ⊔ l) (l≈ ⊔ l)
  Mon = record
      { Obj = Obj
      ; _⇒_ = _⇒_
      ; _≈_ = _≈_
      ; id = id
      ; _∘_ = _∘_
      ; equiv = Fun.on-isEquivalence _⃗ Setoids.equiv
      ; ∘-resp = Setoids.∘-resp
      ; id-r = Setoids.id-r
      ; id-l = Setoids.id-l
      ; assoc = λ { {f = f} {g} {h} → Setoids.assoc {f = f ⃗} {g ⃗} {h ⃗} }
      }

monoidAsCategory : ∀ {l l≈} → Monoid l l≈ → Category zero l l≈
monoidAsCategory M = record
    { Obj = ⊤
    ; _⇒_ = λ _ _ → M.Carrier
    ; _≈_ = M._≈_
    ; id = M.unit
    ; _∘_ = M._⊕_
    ; equiv = M.isEquivalence
    ; ∘-resp = M.⊕-resp
    ; id-r = M.id-r
    ; id-l = M.id-l
    ; assoc = M.assoc
    }
  where
    module M = Monoid M

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
module Prelude.Semiring where

open import Agda.Builtin.Nat using (Nat; zero; suc)
open import Prelude.Function

record Semiring {a} (A : Set a) : Set a where
  infixl 6 _+_
  infixl 7 _*_
  field zro one : A
        _+_ _*_ : A → A → A

open Semiring {{...}} public

{-# DISPLAY Semiring.zro _ = zro #-}
{-# DISPLAY Semiring.one _ = one #-}
{-# DISPLAY Semiring._+_ _ a b = a + b #-}
{-# DISPLAY Semiring._*_ _ a b = a * b #-}

infixr 8 _^_
_^_ : ∀ {a} {A : Set a} {{_ : Semiring A}} → A → Nat → A
n ^ zero  = one
n ^ suc m = n ^ m * n

record Subtractive {a} (A : Set a) : Set a where
  infixl 6 _-_
  field _-_    : A → A → A
        negate : A → A

open Subtractive {{...}} public

{-# DISPLAY Subtractive._-_ _ a b = a - b #-}
{-# DISPLAY Subtractive.negate _ = negate #-}

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
-- There are no level literals in the concrete syntax. This file tests
-- if type errors use level literals.

{-# OPTIONS --universe-polymorphism #-}

module LevelLiterals where

open import Imports.Level

data ⊥ : Set₁ where

DoubleNegated : ∀ {ℓ} → Set ℓ → Set
DoubleNegated A = (A → ⊥) → ⊥

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
------------------------------------------------------------------------------
-- All the FOTC modules
------------------------------------------------------------------------------

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

module FOTC.Everything where

open import FOTC.Base
open import FOTC.Base.Consistency.Axioms
open import FOTC.Base.Consistency.IfInjective
open import FOTC.Base.List
open import FOTC.Base.List.Consistency.Axioms
open import FOTC.Base.List.PropertiesATP
open import FOTC.Base.List.PropertiesI
open import FOTC.Base.Loop
open import FOTC.Base.PropertiesATP
open import FOTC.Base.PropertiesI

open import FOTC.Data.Bool
open import FOTC.Data.Bool.PropertiesATP
open import FOTC.Data.Bool.PropertiesI
open import FOTC.Data.Bool.Type

open import FOTC.Data.Colist
open import FOTC.Data.Colist.PropertiesATP
open import FOTC.Data.Colist.PropertiesI
open import FOTC.Data.Colist.Type
open import FOTC.Data.Colist.Type.Consistency.Axioms

open import FOTC.Data.Conat
open import FOTC.Data.Conat.Equality.Consistency.Axioms
open import FOTC.Data.Conat.Equality.PropertiesATP
open import FOTC.Data.Conat.Equality.PropertiesI
open import FOTC.Data.Conat.Equality.Type
open import FOTC.Data.Conat.PropertiesATP
open import FOTC.Data.Conat.PropertiesI
open import FOTC.Data.Conat.Type
open import FOTC.Data.Conat.Type.Consistency.Axioms

open import FOTC.Data.List
open import FOTC.Data.List.Consistency.Axioms
open import FOTC.Data.List.PropertiesATP
open import FOTC.Data.List.PropertiesByInductionI
open import FOTC.Data.List.PropertiesByInductionATP
open import FOTC.Data.List.PropertiesI
open import FOTC.Data.List.Type
open import FOTC.Data.List.WF-Relation.LT-Cons
open import FOTC.Data.List.WF-Relation.LT-Cons.Induction.Acc.WF-I
open import FOTC.Data.List.WF-Relation.LT-Cons.PropertiesI
open import FOTC.Data.List.WF-Relation.LT-Length
open import FOTC.Data.List.WF-Relation.LT-Length.Induction.Acc.WF-I
open import FOTC.Data.List.WF-Relation.LT-Length.PropertiesI

open import FOTC.Data.Nat
open import FOTC.Data.Nat.Consistency.Axioms
open import FOTC.Data.Nat.Divisibility.By0
open import FOTC.Data.Nat.Divisibility.By0.PropertiesATP
open import FOTC.Data.Nat.Divisibility.By0.PropertiesI
open import FOTC.Data.Nat.Divisibility.NotBy0
open import FOTC.Data.Nat.Divisibility.NotBy0.PropertiesATP
open import FOTC.Data.Nat.Divisibility.NotBy0.PropertiesI
open import FOTC.Data.Nat.Induction.Acc.WF-ATP
open import FOTC.Data.Nat.Induction.Acc.WF-I
open import FOTC.Data.Nat.Induction.NonAcc.LexicographicATP
open import FOTC.Data.Nat.Induction.NonAcc.LexicographicI
open import FOTC.Data.Nat.Induction.NonAcc.WF-ATP
open import FOTC.Data.Nat.Induction.NonAcc.WF-I
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.Consistency.Axioms
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesATP
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesI
open import FOTC.Data.Nat.Inequalities.PropertiesATP
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.List
open import FOTC.Data.Nat.List.PropertiesATP
open import FOTC.Data.Nat.List.PropertiesI
open import FOTC.Data.Nat.List.Type
open import FOTC.Data.Nat.PropertiesATP
open import FOTC.Data.Nat.PropertiesByInductionATP
open import FOTC.Data.Nat.PropertiesByInductionI
open import FOTC.Data.Nat.PropertiesI
open import FOTC.Data.Nat.Type
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Data.Nat.UnaryNumbers.Inequalities.PropertiesATP
open import FOTC.Data.Nat.UnaryNumbers.TotalityATP
open import FOTC.Data.Nat.UnaryNumbers.TotalityI

open import FOTC.Data.Stream
open import FOTC.Data.Stream.Equality.PropertiesATP
open import FOTC.Data.Stream.Equality.PropertiesI
open import FOTC.Data.Stream.PropertiesATP
open import FOTC.Data.Stream.PropertiesI
open import FOTC.Data.Stream.Type
open import FOTC.Data.Stream.Type.Consistency.Axioms

open import FOTC.Induction.WF

open import FOTC.Program.ABP.ABP
open import FOTC.Program.ABP.ABP.Consistency.Axioms
open import FOTC.Program.ABP.CorrectnessProofATP
open import FOTC.Program.ABP.CorrectnessProofI
open import FOTC.Program.ABP.Fair.Type
open import FOTC.Program.ABP.Fair.Consistency.Axioms
open import FOTC.Program.ABP.Fair.PropertiesATP
open import FOTC.Program.ABP.Fair.PropertiesI
open import FOTC.Program.ABP.Lemma1ATP
open import FOTC.Program.ABP.Lemma1I
open import FOTC.Program.ABP.Lemma2ATP
open import FOTC.Program.ABP.Lemma2I
open import FOTC.Program.ABP.PropertiesI
open import FOTC.Program.ABP.Terms

open import FOTC.Program.Collatz.Collatz
open import FOTC.Program.Collatz.Collatz.Consistency.Axioms
open import FOTC.Program.Collatz.Data.Nat
open import FOTC.Program.Collatz.Data.Nat.Consistency.Axioms
open import FOTC.Program.Collatz.Data.Nat.PropertiesATP
open import FOTC.Program.Collatz.Data.Nat.PropertiesI
open import FOTC.Program.Collatz.PropertiesI
open import FOTC.Program.Collatz.PropertiesATP

open import FOTC.Program.Division.ConversionRulesATP
open import FOTC.Program.Division.ConversionRulesI
open import FOTC.Program.Division.CorrectnessProofATP
open import FOTC.Program.Division.CorrectnessProofI
open import FOTC.Program.Division.Division
open import FOTC.Program.Division.ResultATP
open import FOTC.Program.Division.ResultI
open import FOTC.Program.Division.Specification
open import FOTC.Program.Division.TotalityATP
open import FOTC.Program.Division.TotalityI

open import FOTC.Program.GCD.Partial.CommonDivisorATP
open import FOTC.Program.GCD.Partial.CommonDivisorI
open import FOTC.Program.GCD.Partial.ConversionRulesATP
open import FOTC.Program.GCD.Partial.ConversionRulesI
open import FOTC.Program.GCD.Partial.CorrectnessProofATP
open import FOTC.Program.GCD.Partial.CorrectnessProofI
open import FOTC.Program.GCD.Partial.Definitions
open import FOTC.Program.GCD.Partial.DivisibleATP
open import FOTC.Program.GCD.Partial.DivisibleI
open import FOTC.Program.GCD.Partial.GCD
open import FOTC.Program.GCD.Partial.GCD.Consistency.Axioms
open import FOTC.Program.GCD.Partial.GreatestAnyCommonDivisor
open import FOTC.Program.GCD.Partial.TotalityATP
open import FOTC.Program.GCD.Partial.TotalityI

open import FOTC.Program.GCD.Total.CommonDivisorATP
open import FOTC.Program.GCD.Total.CommonDivisorI
open import FOTC.Program.GCD.Total.ConversionRulesATP
open import FOTC.Program.GCD.Total.ConversionRulesI
open import FOTC.Program.GCD.Total.CorrectnessProofATP
open import FOTC.Program.GCD.Total.CorrectnessProofI
open import FOTC.Program.GCD.Total.Definitions
open import FOTC.Program.GCD.Total.DivisibleATP
open import FOTC.Program.GCD.Total.DivisibleI
open import FOTC.Program.GCD.Total.GCD
open import FOTC.Program.GCD.Total.GCD.Consistency.Axioms
open import FOTC.Program.GCD.Total.TotalityATP
open import FOTC.Program.GCD.Total.TotalityI

open import FOTC.Program.Iter0.Iter0
open import FOTC.Program.Iter0.PropertiesATP
open import FOTC.Program.Iter0.PropertiesI

open import FOTC.Program.MapIterate.MapIterateATP
open import FOTC.Program.MapIterate.MapIterateI

open import FOTC.Program.McCarthy91.ArithmeticATP
open import FOTC.Program.McCarthy91.AuxiliaryPropertiesATP
open import FOTC.Program.McCarthy91.McCarthy91.Consistency.Axioms
open import FOTC.Program.McCarthy91.McCarthy91
open import FOTC.Program.McCarthy91.PropertiesATP
open import FOTC.Program.McCarthy91.WF-Relation
open import FOTC.Program.McCarthy91.WF-Relation.LT2WF-RelationATP
open import FOTC.Program.McCarthy91.WF-Relation.PropertiesATP
open import FOTC.Program.McCarthy91.WF-Relation.Induction.Acc.WF-ATP

open import FOTC.Program.Mirror.Example
open import FOTC.Program.Mirror.Forest.PropertiesATP
open import FOTC.Program.Mirror.Forest.PropertiesI
open import FOTC.Program.Mirror.Forest.TotalityATP
open import FOTC.Program.Mirror.Forest.TotalityI
open import FOTC.Program.Mirror.Mirror.Consistency.Axioms
open import FOTC.Program.Mirror.Mirror
open import FOTC.Program.Mirror.PropertiesATP
open import FOTC.Program.Mirror.PropertiesI
open import FOTC.Program.Mirror.Tree.TotalityATP
open import FOTC.Program.Mirror.Tree.TotalityI
open import FOTC.Program.Mirror.Type

open import FOTC.Program.Nest.Nest
open import FOTC.Program.Nest.Nest.Consistency.Axioms
open import FOTC.Program.Nest.PropertiesATP

open import FOTC.Program.SortList.CorrectnessProofATP
open import FOTC.Program.SortList.CorrectnessProofI
open import FOTC.Program.SortList.Properties.MiscellaneousATP
open import FOTC.Program.SortList.Properties.MiscellaneousI
open import FOTC.Program.SortList.Properties.Totality.BoolATP
open import FOTC.Program.SortList.Properties.Totality.BoolI
open import FOTC.Program.SortList.Properties.Totality.ListN-ATP
open import FOTC.Program.SortList.Properties.Totality.ListN-I
open import FOTC.Program.SortList.Properties.Totality.OrdList.FlattenI
open import FOTC.Program.SortList.Properties.Totality.OrdList.FlattenATP
open import FOTC.Program.SortList.Properties.Totality.OrdListATP
open import FOTC.Program.SortList.Properties.Totality.OrdListI
open import FOTC.Program.SortList.Properties.Totality.OrdTreeATP
open import FOTC.Program.SortList.Properties.Totality.OrdTreeI
open import FOTC.Program.SortList.Properties.Totality.TreeATP
open import FOTC.Program.SortList.Properties.Totality.TreeI
open import FOTC.Program.SortList.PropertiesI
open import FOTC.Program.SortList.PropertiesATP
open import FOTC.Program.SortList.SortList
open import FOTC.Program.SortList.SortList.Consistency.Axioms

open import FOTC.Relation.Binary.Bisimilarity.Bisimulation
open import FOTC.Relation.Binary.Bisimilarity.Consistency.Axioms
open import FOTC.Relation.Binary.Bisimilarity.PropertiesATP
open import FOTC.Relation.Binary.Bisimilarity.PropertiesI
open import FOTC.Relation.Binary.Bisimilarity.Type

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Data.Nat.AbsoluteDifference where

open import Data.Nat.Base
open import Path
open import Prelude
open import Algebra

∣_-_∣ : ℕ → ℕ → ℕ
∣ 0         - m     ∣ = m
∣ n@(suc _) - 0     ∣ = n
∣ suc n     - suc m ∣ = ∣ n - m ∣

_ : ∣ 5 - 3 ∣ ≡ 2
_ = refl

_ : ∣ 3 - 5 ∣ ≡ 2
_ = refl

∣-∣‿comm : Commutative ∣_-_∣
∣-∣‿comm zero    zero    = refl
∣-∣‿comm zero    (suc y) = refl
∣-∣‿comm (suc x) zero    = refl
∣-∣‿comm (suc x) (suc y) = ∣-∣‿comm x y

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
open import Agda.Primitive using (lzero; lsuc; _⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂; subst; setoid)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂; zip; map; <_,_>; swap)
import Function.Equality
open import Relation.Binary using (Setoid)
import Relation.Binary.Reasoning.Setoid as SetoidR

import SecondOrder.Arity
import SecondOrder.Signature
import SecondOrder.Metavariable
import SecondOrder.VRenaming
import SecondOrder.MRenaming
import SecondOrder.Term
import SecondOrder.Substitution
import SecondOrder.RelativeMonadMorphism
import SecondOrder.Instantiation
import SecondOrder.IndexedCategory
import SecondOrder.RelativeKleisli
import SecondOrder.Mslot
import SecondOrder.MRelativeMonad
import SecondOrder.VRelativeMonad

module SecondOrder.MRelMonMorphism
  {ℓ}
  {𝔸 : SecondOrder.Arity.Arity}
  (Σ : SecondOrder.Signature.Signature ℓ 𝔸)
  where

  open SecondOrder.Signature.Signature Σ
  open SecondOrder.Metavariable Σ
  open SecondOrder.Term Σ
  open SecondOrder.VRenaming Σ
  open SecondOrder.MRenaming Σ
  open SecondOrder.Mslot Σ
  open SecondOrder.Substitution Σ
  open SecondOrder.Instantiation Σ
  open SecondOrder.MRelativeMonad Σ
  open SecondOrder.VRelativeMonad Σ
  open SecondOrder.RelativeMonadMorphism

  module MRelMonMorph {Γ Γ′ : VContext} where
    open MTerm {Γ} renaming (MMonad to M_Γ)
    open MTerm {Γ′} renaming (MMonad to M_Γ′)

    Fᴹ : ∀ (ρ : Γ ⇒ᵛ Γ′) →  RMonadMorph (M_Γ) (M_Γ′)
    Fᴹ ρ = record
            { morph = λ Γᴹ Aᴹ →
                        record
                          { _⟨$⟩_ = [ ⇑ᵛ ρ ]ᵛ_
                          ; cong =  λ M≈N → []ᵛ-resp-≈ M≈N
                          }
            ; law-unit =  λ Γᴹ Aᴹ M≡N → ≈-≡
                                          (I-resp-≡
                                            {I = λ M → tm-meta M λ i → tm-var (var-inr i) }
                                            M≡N)
            ; law-extend = λ {Θ} {Ω} {k} Γᴹ Aᴹ {s} {t} s≈t →
                                       ≈-trans
                                           ([ᵛ∘ⁱ] s)
                                           (≈-trans
                                             ([]ⁱ-resp-≈
                                               (⇑ᵛ ρ ᵛ∘ⁱ ⇑ⁱ (λ {Λ} {B} →
                                                   Function.Equality._⟨$⟩_ (k Λ B)))
                                               ([]ᵛ-resp-≈ s≈t))
                                             ([]ⁱ-resp-≈ⁱ ([ (⇑ᵛ ρ) ]ᵛ t) λ M →
                                               (≈-trans
                                                 (≈-sym [∘ᵛ])
                                                 (≈-trans
                                                   ([]ᵛ-resp-≡ᵛ extend-aux)
                                                   [∘ᵛ]))))
            }

           where
             extend-aux : ∀ {Ξ Λ} → ⇑ᵛ {Ξ = Ξ} (⇑ᵛ {Ξ = Λ} ρ) ∘ᵛ (⇑ᵛ var-inl) ≡ᵛ ⇑ᵛ var-inl ∘ᵛ (⇑ᵛ ρ)
             extend-aux (var-inl x) = refl
             extend-aux (var-inr x) = refl

  -- Attempt with substitutions instead of renamings : not sure it works
    -- hat : (f : (Θ : MContext) → Θ ⊕ Γ ⇒ˢ Γ') → RMonadMorph M_Γ M_Γ'
    -- hat f =
    --   let open Function.Equality using (_⟨$⟩_) renaming (cong to func-cong) in
    --   record
    --   { morph = λ {Θ} Δ A → record { _⟨$⟩_ = λ t → [ ⇑ˢ (f Θ) ]ˢ t ; cong = []ˢ-resp-≈ (⇑ˢ (f Θ))}
    --   ; law-unit = λ Δ A {t} {s} t≡s → ≈-≡ (cong tm-meta-generic t≡s)
    --   ; law-extend = λ {Θ} {Ψ} {I} Δ A {t} {s} t≈s →
    --       let open SetoidR (Term-setoid Ψ (Γ' ,, Δ) A) in
    --       begin
    --       ([ ⇑ˢ (f Ψ) ]ˢ ([ ⇑ⁱ (λ {Λ} {B} M →  (I Λ B ⟨$⟩ M) ) ]ⁱ t) )
    --         ≈⟨ {!!} ⟩ -- this is the crucial step
    --       ([ ⇑ⁱ (λ {Λ} {B} M → [ ⇑ˢ (f Ψ) ]ˢ (I Λ B ⟨$⟩ M)) ]ⁱ ([ ⇑ˢ (f Θ) ]ˢ t))
    --         ≈⟨ []ⁱ-resp-≈ (⇑ⁱ (λ {Λ} {B} M → [ ⇑ˢ (f Ψ) ]ˢ (I Λ B ⟨$⟩ M))) ([]ˢ-resp-≈ (⇑ˢ (f Θ)) t≈s) ⟩
    --       ([ ⇑ⁱ (λ {Λ} {B} M → [ ⇑ˢ (f Ψ) ]ˢ (I Λ B ⟨$⟩ M)) ]ⁱ ([ ⇑ˢ (f Θ) ]ˢ s))
    --       ∎
    --   }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: cilinder/formaltt

max_forks_repo_name: cilinder/formaltt


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommRing.Instances.MultivariatePoly where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat renaming(_+_ to _+n_; _·_ to _·n_)

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Instances.Int

open import Cubical.Algebra.Polynomials.Multivariate.Base
open import Cubical.Algebra.Polynomials.Multivariate.Properties

private variable
  ℓ : Level

-----------------------------------------------------------------------------
-- General Nth polynome

module _
  (A : CommRing ℓ)
  (n : ℕ)
  where

  open CommRingStr
  open RingTheory (CommRing→Ring A)
  open Nth-Poly-structure A n

  PolyCommRing : CommRing ℓ
  fst PolyCommRing = Poly A n
  0r (snd PolyCommRing) = 0P
  1r (snd PolyCommRing) = 1P
  _+_ (snd PolyCommRing) = _poly+_
  _·_ (snd PolyCommRing) = _poly*_
  - snd PolyCommRing = polyInv
  isCommRing (snd PolyCommRing) = makeIsCommRing
                                  trunc
                                  poly+Assoc
                                  poly+IdR
                                  poly+InvR
                                  poly+Comm
                                  poly*Assoc
                                  poly*IdR
                                  poly*DistR
                                  poly*Comm

-----------------------------------------------------------------------------
-- Notation and syntax in the case 1,2,3 and ℤ

module _
  (Ar@(A , Astr) : CommRing ℓ)
  (n : ℕ)
  where

  A[X1,···,Xn] : CommRing ℓ
  A[X1,···,Xn] = PolyCommRing Ar n

  A[x1,···,xn] : Type ℓ
  A[x1,···,xn] = fst (A[X1,···,Xn])

max_stars_repo_name: guilhermehas/cubical

max_issues_repo_name: guilhermehas/cubical

max_forks_repo_name: guilhermehas/cubical


text:
-- 2013-02-18 reported by rotsor

module Issue796 where

data U : Set where
  a b : U

data A : Set where
data B : Set where

module Abs where
 abstract
  A' B' : Set

  A' = A
  B' = B

module Conc where

  open Abs

  -- Andreas, 2013-02-19
  -- this function should not be injective, since here
  -- it is not known whether A' and B' are actually different
  [_] : U → Set
  [_] a = A'
  [_] b = B'

  f : ∀ u → [ u ] → U
  f u _ = u

  postulate x : A'

  zzz = f _ x


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

module Cubical.Functions.Involution where

open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence

isInvolution : ∀{ℓ} {A : Type ℓ} → (A → A) → Type _
isInvolution f = ∀ x → f (f x) ≡ x

module _ {ℓ} {A : Type ℓ} {f : A → A} (invol : isInvolution f) where
  open Iso

  involIso : Iso A A
  involIso .fun = f
  involIso .inv = f
  involIso .rightInv = invol
  involIso .leftInv = invol

  involIsEquiv : isEquiv f
  involIsEquiv = isoToIsEquiv involIso

  involEquiv : A ≃ A
  involEquiv = f , involIsEquiv

  involPath : A ≡ A
  involPath = ua involEquiv

  involEquivComp : compEquiv involEquiv involEquiv ≡ idEquiv A
  involEquivComp
    = equivEq (λ i x → invol x i)

  involPathComp : involPath ∙ involPath ≡ refl
  involPathComp
    = sym (uaCompEquiv involEquiv involEquiv) ∙∙ cong ua involEquivComp ∙∙ uaIdEquiv

  involPath² : Square involPath refl refl involPath
  involPath²
    = subst (λ s → Square involPath s refl involPath)
        involPathComp (compPath-filler involPath involPath)

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:
open import Agda.Builtin.List

foldr : {A B : Set} → (A → B → B) → B → List A → B
foldr _⊕_ ε []       = ε
foldr _⊕_ ε (x ∷ xs) = x ⊕ foldr _⊕_ ε xs

infixr 5 _++_

_++_ : {A : Set} → List A → List A → List A
xs ++ ys = foldr _∷_ ys xs

record R (F : Set → Set) : Set₁ where
  field
    f : {A : Set} → A → F A → F A

open R ⦃ … ⦄ public

postulate
  D    : {A : Set} → List A → Set
  easy : {A : Set} {@0 xs : List A} → D xs

record Q (A : Set) : Set where
  field
    @0 index : List A
    d        : D index

g : {A : Set} → A → Q A → Q A
g x q .Q.index = q .Q.index ++ x ∷ []
g x q .Q.d     = easy

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

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A → Maybe A

postulate
  m₁ : {A : Set} {B : Maybe A → Set} →
       ((x : A) → B (just x)) → (x : Maybe A) → B x

m₂ : {A B : Set} → (A → Maybe B) → Maybe A → Maybe B
m₂ f x = m₁ f x

postulate
  P : {A : Set} → A → Set
  p : {A : Set} (x : A) → P x
  A : Set
  x : Maybe (A × Q A)

instance
  _ : R Q
  _ = record { f = g }

_ : P (m₂ (λ { (x , q) → just (f x q) }) x)
_ = p (m₁ (λ { (x , q) → just (f x q) }) x)


text:
{-# OPTIONS --without-K #-}
-- The core types behind exploration functions
module Explore.Core where

open import Level.NP
open import Algebra
open import Type hiding (★)
open import Function using (id; _∘_; _∘′_)
open import Data.Nat.NP using (ℕ)
open import Data.Two using (𝟚)
open import Data.Maybe.NP using (_→?_)
open import Relation.Unary.Logical
open import Relation.Binary.Logical

module _ {a} where
    BigOp : ∀ {ℓ} → ★ ℓ → ★ a → ★ (a ⊔ ℓ)
    BigOp M A = (A → M) → M

    Explore : ∀ ℓ → ★_ a → ★ (a ⊔ ₛ ℓ)
    Explore ℓ A = ∀ {M : ★ ℓ} (ε : M) (_∙_ : M → M → M) → BigOp M A

    BigOpMon : ∀ {c ℓ} → Monoid c ℓ → ★ a → ★ _
    BigOpMon M A = BigOp (Monoid.Carrier M) A

    ExploreMon : ∀ c ℓ → ★ a → ★ _
    ExploreMon c ℓ A = (M : Monoid c ℓ) → BigOpMon M A

    Explore₀ : ★ a → ★(a ⊔ ₁)
    Explore₀ = Explore ₀

    Explore₁ : ★ a → ★(a ⊔ ₂)
    Explore₁ = Explore ₁

    Sum : ★ a → ★ a
    Sum = BigOp ℕ

    Product : ★ a → ★ a
    Product = BigOp ℕ

    Count : ★ a → ★ a
    Count A = (A → 𝟚) → ℕ

    Find? : ∀ {b} → ★ a → ★(ₛ b ⊔ a)
    Find? {b} A = ∀ {B : ★ b} → (A →? B) →? B

    FindKey : ★ a → ★ a
    FindKey A = (A → 𝟚) →? A

-- These three basic combinators are defined here
-- since they are used to define ExploreInd
    module _ {ℓ} {A : ★ a} where
        merge-explore : Explore ℓ A → Explore ℓ A → Explore ℓ A
        merge-explore e₀ e₁ ε _∙_ f = e₀ ε _∙_ f ∙ e₁ ε _∙_ f

        empty-explore : Explore ℓ A
        empty-explore ε _ _ = ε

        point-explore : A → Explore ℓ A
        point-explore x _ _ f = f x

[Explore] : ∀ {a aₚ} → ([★₀] [→] [★] (ₛ (a ⊔ aₚ))) (Explore a)
[Explore] {a} {aₚ} Aₚ = ∀⟨ Mₚ ∶ [★] (a ⊔ aₚ)⟩[→] Mₚ [→] [Op₂] {_} {aₚ} Mₚ [→] (Aₚ [→] Mₚ) [→] Mₚ

module _ {ℓ₁ ℓ₂} ℓᵣ {a₁ a₂ aᵣ} where
    ⟦Explore⟧ : (⟦★⟧ {a₁} {a₂} aᵣ ⟦→⟧ ⟦★⟧ (a₁ ⊔ a₂ ⊔ aᵣ ⊔ ₛ (ℓ₁ ⊔ ℓ₂ ⊔ ℓᵣ))) (Explore ℓ₁) (Explore ℓ₂)
    ⟦Explore⟧ Aᵣ = ∀⟨ Mᵣ ∶ ⟦★⟧ (ℓ₁ ⊔ ℓ₂ ⊔ ℓᵣ) ⟩⟦→⟧ Mᵣ ⟦→⟧ ⟦Op₂⟧ {_} {_} {ℓᵣ} Mᵣ ⟦→⟧ (Aᵣ ⟦→⟧ Mᵣ) ⟦→⟧ Mᵣ

⟦Explore⟧₀ : (⟦★₀⟧ ⟦→⟧ ⟦★₁⟧) (Explore _) (Explore _)
⟦Explore⟧₀ = ⟦Explore⟧ _

-- -}
-- -}
-- -}
-- -}


text:
module L.Base.Nat.Core where

-- Introducing Nat type with constructors zero and succ
data Nat : Set where
  zero : Nat
  succ : Nat → Nat

-- Enabling the usage of numerals in code.
{-# BUILTIN NATURAL Nat #-}

ind : ∀{c} (C : Nat → Set c)
  → C zero → ((x : Nat) → C x → C (succ x))
  → (n : Nat) → C n
ind C cₒ cₛ  zero    = cₒ
ind C cₒ cₛ (succ n) = cₛ n (ind C cₒ cₛ n)

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
module Load where

data Bool : Set where
  tt : Bool
  ff : Bool


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Function using (_∘_)
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Functions.Embedding
open import Cubical.Data.Sigma

open import Cubical.Structures.Axioms
open import Cubical.Structures.Pointed
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphism

open import Cubical.Reflection.StrictEquiv

private
  variable
    ℓ ℓ' ℓ'' : Level

open Iso
open GroupStr
open GroupHom

isPropIsGroupHom : (G : Group {ℓ}) (H : Group {ℓ'}) {f : ⟨ G ⟩ → ⟨ H ⟩} → isProp (isGroupHom G H f)
isPropIsGroupHom G H {f} = isPropΠ2 λ a b → GroupStr.is-set (snd H) _ _

isSetGroupHom : {G : Group {ℓ}} {H : Group {ℓ'}} → isSet (GroupHom G H)
isSetGroupHom {G = G} {H = H} = isOfHLevelRespectEquiv 2 equiv (isSetΣ (isSetΠ λ _ → is-set (snd H)) λ _ → isProp→isSet (isPropIsGroupHom G H)) where
  equiv : (Σ[ g ∈ (⟨ G ⟩ → ⟨ H ⟩) ] (isGroupHom G H g)) ≃ (GroupHom G H)
  equiv =  isoToEquiv (iso (λ (g , m) → grouphom g m) (λ hom → fun hom , isHom hom) (λ _ → refl) λ _ → refl)

-- Morphism composition
isGroupHomComp : {F : Group {ℓ}} {G : Group {ℓ'}} {H : Group {ℓ''}} →
  (f : GroupHom F G) → (g : GroupHom G H) → isGroupHom F H (fun g ∘ fun f)
isGroupHomComp f g x y = cong (fun g) (isHom f _ _) ∙ isHom g _ _

compGroupHom : {F : Group {ℓ}} {G : Group {ℓ'}} {H : Group {ℓ''}} → GroupHom F G → GroupHom G H → GroupHom F H
fun (compGroupHom f g) = fun g ∘ fun f
isHom (compGroupHom f g) = isGroupHomComp f g

open GroupEquiv
compGroupEquiv : {F : Group {ℓ}} {G : Group {ℓ'}} {H : Group {ℓ''}} → GroupEquiv F G → GroupEquiv G H → GroupEquiv F H
eq (compGroupEquiv f g) = compEquiv (eq f) (eq g)
isHom (compGroupEquiv f g) = isHom (compGroupHom (hom f) (hom g))

idGroupEquiv : (G : Group {ℓ}) → GroupEquiv G G
eq (idGroupEquiv G) = idEquiv ⟨ G ⟩
isHom (idGroupEquiv G) = λ _ _ → refl

-- Isomorphism inversion
isGroupHomInv : {G : Group {ℓ}} {H : Group {ℓ'}} (f : GroupEquiv G H) → isGroupHom H G (invEq (GroupEquiv.eq f))
isGroupHomInv {G = G} {H = H}  f h h' = isInj-f _ _ (
  f' (g (h ⋆² h')) ≡⟨ retEq (eq f) _ ⟩
  (h ⋆² h') ≡⟨ sym (cong₂ _⋆²_ (retEq (eq f) h) (retEq (eq f) h')) ⟩
  (f' (g h) ⋆² f' (g h')) ≡⟨ sym (isHom (hom f) _ _) ⟩
  f' (g h ⋆¹ g h') ∎)
  where
  f' = fst (eq f)
  _⋆¹_ = _+_ (snd G)
  _⋆²_ = _+_ (snd H)
  g = invEq (eq f)

  isInj-f : (x y : ⟨ G ⟩) → f' x ≡ f' y → x ≡ y
  isInj-f x y = invEq (_ , isEquiv→isEmbedding (snd (eq f)) x y)

invGroupEquiv : {G : Group {ℓ}} {H : Group {ℓ'}} → GroupEquiv G H → GroupEquiv H G
eq (invGroupEquiv f) = invEquiv (eq f)
isHom (invGroupEquiv f) = isGroupHomInv f

dirProdEquiv : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Group {ℓ}} {B : Group {ℓ'}} {C : Group {ℓ''}} {D : Group {ℓ'''}}
           → GroupEquiv A C → GroupEquiv B D
           → GroupEquiv (dirProd A B) (dirProd C D)
eq (dirProdEquiv eq1 eq2) = ≃-× (eq eq1) (eq eq2)
isHom (dirProdEquiv eq1 eq2) = isHom (×hom (GroupEquiv.hom eq1) (GroupEquiv.hom eq2))

groupHomEq : {G : Group {ℓ}} {H : Group {ℓ'}} {f g : GroupHom G H} → (fun f ≡ fun g) → f ≡ g
fun (groupHomEq p i) = p i
isHom (groupHomEq {G = G} {H = H} {f = f} {g = g} p i) = p-hom i
  where
  p-hom : PathP (λ i → isGroupHom G H (p i)) (isHom f) (isHom g)
  p-hom = toPathP (isPropIsGroupHom G H _ _)

groupEquivEq : {G : Group {ℓ}} {H : Group {ℓ'}} {f g : GroupEquiv G H} → (eq f ≡ eq g) → f ≡ g
eq (groupEquivEq {G = G} {H = H} {f} {g} p i) = p i
isHom (groupEquivEq {G = G} {H = H} {f} {g} p i) = p-hom i
  where
  p-hom : PathP (λ i → isGroupHom G H (p i .fst)) (isHom f) (isHom g)
  p-hom = toPathP (isPropIsGroupHom G H _ _)

module GroupΣTheory {ℓ} where

  RawGroupStructure : Type ℓ → Type ℓ
  RawGroupStructure = SemigroupΣTheory.RawSemigroupStructure

  RawGroupEquivStr : StrEquiv RawGroupStructure _
  RawGroupEquivStr = SemigroupΣTheory.RawSemigroupEquivStr

  rawGroupUnivalentStr : UnivalentStr RawGroupStructure _
  rawGroupUnivalentStr = SemigroupΣTheory.rawSemigroupUnivalentStr

  -- The neutral element and the inverse function will be derived from the
  -- axioms, instead of being defined in the RawGroupStructure in order
  -- to have that group equivalences are equivalences that preserves
  -- multiplication (so we don't have to show that they also preserve inversion
  -- and neutral element, although they will preserve them).
  GroupAxioms : (G : Type ℓ) → RawGroupStructure G → Type ℓ
  GroupAxioms G _·_ =
      IsSemigroup _·_
    × (Σ[ e ∈ G ] ((x : G) → (x · e ≡ x) × (e · x ≡ x))
                × ((x : G) → Σ[ x' ∈ G ] (x · x' ≡ e) × (x' · x ≡ e)))

  GroupStructure : Type ℓ → Type ℓ
  GroupStructure = AxiomsStructure RawGroupStructure GroupAxioms

  GroupΣ : Type (ℓ-suc ℓ)
  GroupΣ = TypeWithStr ℓ GroupStructure

  -- Structured equivalences for groups are those for monoids (but different axioms)
  GroupEquivStr : StrEquiv GroupStructure ℓ
  GroupEquivStr = AxiomsEquivStr RawGroupEquivStr GroupAxioms

  open MonoidTheory

  isSetGroupΣ : (G : GroupΣ)
               → isSet _
  isSetGroupΣ (_ , _ , (isSemigroup-G , _ , _)) = IsSemigroup.is-set isSemigroup-G

  isPropGroupAxioms : (G : Type ℓ)
                      → (s : RawGroupStructure G)
                      → isProp (GroupAxioms G s)
  isPropGroupAxioms G _+_ = isPropΣ (isPropIsSemigroup _) γ
    where
    γ : (h : IsSemigroup _+_) →
        isProp (Σ[ e ∈ G ] ((x : G) → (x + e ≡ x) × (e + x ≡ x))
                         × ((x : G) → Σ[ x' ∈ G ] (x + x' ≡ e) × (x' + x ≡ e)))
    γ h (e , P , _) (e' , Q , _) =
      Σ≡Prop (λ x → isPropΣ (isPropΠ λ _ → isProp× ((IsSemigroup.is-set h) _ _) ((IsSemigroup.is-set h) _ _)) (β x))
             (sym (fst (Q e)) ∙ snd (P e'))
      where
      β : (e : G) → ((x : G) → (x + e ≡ x) × (e + x ≡ x))
        → isProp ((x : G) → Σ[ x' ∈ G ] (x + x' ≡ e) × (x' + x ≡ e))
      β e He =
        isPropΠ λ { x (x' , _ , P) (x'' , Q , _) →
                Σ≡Prop (λ _ → isProp× ((IsSemigroup.is-set h) _ _) ((IsSemigroup.is-set h) _ _))
                       (inv-lemma ℳ x x' x'' P Q) }
        where
        ℳ : Monoid
        ℳ = makeMonoid e _+_ (IsSemigroup.is-set h) (IsSemigroup.assoc h) (λ x → He x .fst) (λ x → He x .snd)

  Group→GroupΣ : Group → GroupΣ
  Group→GroupΣ (G , GS) = _ , _ , (isSemigroup GS , _ , identity GS , λ x → (- GS) x , inverse GS x)

  GroupΣ→Group : GroupΣ → Group
  GroupΣ→Group (G , _ , SG , _ , H0g , invertible ) =
     group _ _ _ (λ x → invertible x .fst) (isgroup (ismonoid SG H0g) λ x → invertible x .snd)

  GroupIsoGroupΣ : Iso Group GroupΣ
  GroupIsoGroupΣ = iso Group→GroupΣ GroupΣ→Group (λ _ → refl) (λ _ → refl)

  groupUnivalentStr : UnivalentStr GroupStructure GroupEquivStr
  groupUnivalentStr = axiomsUnivalentStr _ isPropGroupAxioms rawGroupUnivalentStr

  GroupΣPath : (G H : GroupΣ) → (G ≃[ GroupEquivStr ] H) ≃ (G ≡ H)
  GroupΣPath = SIP groupUnivalentStr

  GroupEquivΣ : (G H : Group) → Type ℓ
  GroupEquivΣ G H = Group→GroupΣ G ≃[ GroupEquivStr ] Group→GroupΣ H

  GroupIsoΣPath : {G H : Group} → Iso (GroupEquiv G H) (GroupEquivΣ G H)
  fun GroupIsoΣPath f       = (eq f) , isHom f
  inv GroupIsoΣPath (e , h) = groupequiv e h
  rightInv GroupIsoΣPath _  = refl
  leftInv GroupIsoΣPath _   = refl

  GroupPath : (G H : Group) → (GroupEquiv G H) ≃ (G ≡ H)
  GroupPath G H =
    GroupEquiv G H                  ≃⟨ strictIsoToEquiv GroupIsoΣPath ⟩
    GroupEquivΣ G H                 ≃⟨ GroupΣPath _ _ ⟩
    Group→GroupΣ G ≡ Group→GroupΣ H ≃⟨ isoToEquiv (invIso (congIso GroupIsoGroupΣ)) ⟩
    G ≡ H ■

  RawGroupΣ : Type (ℓ-suc ℓ)
  RawGroupΣ = TypeWithStr ℓ RawGroupStructure

  Group→RawGroupΣ : Group → RawGroupΣ
  Group→RawGroupΣ (G , GS) = G , _+_ GS

  InducedGroup : (G : Group) (H : RawGroupΣ) (e : ⟨ G ⟩ ≃ H .fst)
               → RawGroupEquivStr (Group→RawGroupΣ G) H e → Group
  InducedGroup G H e r =
    GroupΣ→Group (inducedStructure rawGroupUnivalentStr (Group→GroupΣ G) H (e , r))

  InducedGroupPath : (G : Group {ℓ}) (H : RawGroupΣ) (e : ⟨ G ⟩ ≃ H .fst)
                     (E : RawGroupEquivStr (Group→RawGroupΣ G) H e)
                   → G ≡ InducedGroup G H e E
  InducedGroupPath G H e E =
    GroupPath G (InducedGroup G H e E) .fst (groupequiv e E)

-- Extract the characterization of equality of groups
GroupPath : (G H : Group {ℓ}) → (GroupEquiv G H) ≃ (G ≡ H)
GroupPath = GroupΣTheory.GroupPath

InducedGroup : (G : Group {ℓ}) (H : GroupΣTheory.RawGroupΣ) (e : ⟨ G ⟩ ≃ H .fst)
             → GroupΣTheory.RawGroupEquivStr (GroupΣTheory.Group→RawGroupΣ G) H e
             → Group
InducedGroup = GroupΣTheory.InducedGroup

InducedGroupPath : (G : Group {ℓ}) (H : GroupΣTheory.RawGroupΣ) (e : ⟨ G ⟩ ≃ H .fst)
                   (E : GroupΣTheory.RawGroupEquivStr (GroupΣTheory.Group→RawGroupΣ G) H e)
                 → G ≡ InducedGroup G H e E
InducedGroupPath = GroupΣTheory.InducedGroupPath

uaGroup : {G H : Group {ℓ}} → GroupEquiv G H → G ≡ H
uaGroup {G = G} {H = H} = equivFun (GroupPath G H)

carac-uaGroup : {G H : Group {ℓ}} (f : GroupEquiv G H) → cong ⟨_⟩ (uaGroup f) ≡ ua (GroupEquiv.eq f)
carac-uaGroup f = ua (eq f) ∙ refl ≡⟨ sym (rUnit _)  ⟩
                  ua (eq f) ∎

-- Group-ua functoriality

Group≡ : (G H : Group {ℓ}) → (
  Σ[ p ∈ ⟨ G ⟩ ≡ ⟨ H ⟩ ]
  Σ[ q ∈ PathP (λ i → p i) (0g (snd G)) (0g (snd H)) ]
  Σ[ r ∈ PathP (λ i → p i → p i → p i) (_+_ (snd G)) (_+_ (snd H)) ]
  Σ[ s ∈ PathP (λ i → p i → p i) (- snd G) (- snd H) ]
  PathP (λ i → IsGroup (q i) (r i) (s i)) (isGroup (snd G)) (isGroup (snd H)))
  ≃ (G ≡ H)
Group≡ G H = isoToEquiv theIso
  where
  theIso : Iso _ _
  fun theIso (p , q , r , s , t) i = p i , groupstr (q i) (r i) (s i) (t i)
  inv theIso x = cong ⟨_⟩ x , cong (0g ∘ snd) x , cong (_+_ ∘ snd) x , cong (-_ ∘ snd) x , cong (isGroup ∘ snd) x
  rightInv theIso _ = refl
  leftInv theIso _ = refl

caracGroup≡ : {G H : Group {ℓ}} (p q : G ≡ H) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q
caracGroup≡ {G = G} {H = H} p q P = sym (transportTransport⁻ (ua (Group≡ G H)) p)
                                 ∙∙ cong (transport (ua (Group≡ G H))) helper
                                 ∙∙ transportTransport⁻ (ua (Group≡ G H)) q
  where
  helper : transport (sym (ua (Group≡ G H))) p ≡ transport (sym (ua (Group≡ G H))) q
  helper = Σ≡Prop
             (λ _ → isPropΣ
                       (isOfHLevelPathP' 1 (is-set (snd H)) _ _)
                       λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd H)) _ _)
                       λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ λ _ → is-set (snd H)) _ _)
                       λ _ → isOfHLevelPathP 1 (isPropIsGroup _ _ _) _ _)
             (transportRefl (cong ⟨_⟩ p) ∙ P ∙ sym (transportRefl (cong ⟨_⟩ q)))

uaGroupId : (G : Group {ℓ}) → uaGroup (idGroupEquiv G) ≡ refl
uaGroupId G = caracGroup≡ _ _ (carac-uaGroup (idGroupEquiv G) ∙ uaIdEquiv)

uaCompGroupEquiv : {F G H : Group {ℓ}} (f : GroupEquiv F G) (g : GroupEquiv G H) → uaGroup (compGroupEquiv f g) ≡ uaGroup f ∙ uaGroup g
uaCompGroupEquiv f g = caracGroup≡ _ _ (
  cong ⟨_⟩ (uaGroup (compGroupEquiv f g))
    ≡⟨ carac-uaGroup (compGroupEquiv f g) ⟩
  ua (eq (compGroupEquiv f g))
    ≡⟨ uaCompEquiv _ _ ⟩
  ua (eq f) ∙ ua (eq g)
    ≡⟨ cong (_∙ ua (eq g)) (sym (carac-uaGroup f)) ⟩
  cong ⟨_⟩ (uaGroup f) ∙ ua (eq g)
    ≡⟨ cong (cong ⟨_⟩ (uaGroup f) ∙_) (sym (carac-uaGroup g)) ⟩
  cong ⟨_⟩ (uaGroup f) ∙ cong ⟨_⟩ (uaGroup g)
    ≡⟨ sym (cong-∙ ⟨_⟩ (uaGroup f) (uaGroup g)) ⟩
  cong ⟨_⟩ (uaGroup f ∙ uaGroup g) ∎) where
  open GroupEquiv

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module WrongHidingInLHS where

f : Set -> Set
f {x} = x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Monads
------------------------------------------------------------------------

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

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

module Category.Monad where

open import Function
open import Category.Monad.Indexed
open import Data.Unit

RawMonad : ∀ {f} → (Set f → Set f) → Set _
RawMonad M = RawIMonad {I = ⊤} (λ _ _ → M)

RawMonadT : ∀ {f} (T : (Set f → Set f) → (Set f → Set f)) → Set _
RawMonadT T = RawIMonadT {I = ⊤} (λ M _ _ → T (M _ _))

RawMonadZero : ∀ {f} → (Set f → Set f) → Set _
RawMonadZero M = RawIMonadZero {I = ⊤} (λ _ _ → M)

RawMonadPlus : ∀ {f} → (Set f → Set f) → Set _
RawMonadPlus M = RawIMonadPlus {I = ⊤} (λ _ _ → M)

module RawMonad {f} {M : Set f → Set f}
                (Mon : RawMonad M) where
  open RawIMonad Mon public

module RawMonadZero {f} {M : Set f → Set f}
                    (Mon : RawMonadZero M) where
  open RawIMonadZero Mon public

module RawMonadPlus {f} {M : Set f → Set f}
                    (Mon : RawMonadPlus M) where
  open RawIMonadPlus Mon public


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

module Instance where

open import Level

it : ∀ {a} {A : Type a} → ⦃ _ : A ⦄ → A
it ⦃ x ⦄ = x

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
-- Example, ℤ is an Euclidean Domain. Here all the properties needed
-- are already proved in Data.Integer.Properties. However, we will
-- prove there is another divmod pair such that the rank estimation
-- is more precise, see EucDomain2.agda.

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

module Integer.EucDomain where

  -- imports from stdlib.
  open import Relation.Nullary using (¬_)
  open import Relation.Binary.PropositionalEquality using (refl ; _≡_)

  open import Data.Nat using (_<_)
  open import Data.Integer
    using (_+_ ; _*_ ; -_ ; ℤ ; 0ℤ ; 1ℤ ; ∣_∣ ; +[1+_] ; -[1+_] ; +_)
  open import Data.Integer.DivMod
    renaming (_div_ to _divℤ_; _mod_ to _modℤ_ ; n%d<d to euc-rankℤ; a≡a%n+[a/n]*n to euc-eqℤ)
  open import Data.Integer.Properties
    using (+-*-isCommutativeRing ; *-cancelˡ-≡)

  open import Algebra.Definitions (_≡_ {A = ℤ}) using (AlmostLeftCancellative)

  -- imports from local.
  import EuclideanDomain
  open EuclideanDomain.Structures (_≡_ {A = ℤ})
  open EuclideanDomain.Bundles

  -- You will notice the recurring pattern that I have to split on
  -- the divisor d, and use ¬ d ≡ 0ℤ to exclude the zero divisor
  -- case. And addtionally, I have to repeat similary codes
  -- twice. This is the price of the translation from ¬ a ≡ 0ℤ to
  -- NonZero a. I don't have a good way to avoid this. This become
  -- even more awkward when dealing with Gaussian integers since we
  -- have more constructor there (meaning more cases and more
  -- repeatitions).

  -- On the other hand, a translation from NonZero predicate to
  -- non-equaity ¬ d ≡ 0ℤ is quite easy. We will use this to define
  -- div and mod with instance predicate argument for 𝔾.

  -- I could use NonZero predicate in the definition of Euclidean
  -- Domain, but that will make the definition more complicated. Also
  -- the file "Algebra.Definition" using the same method as here to
  -- exclude zero, for example the definition of
  -- "AlmostLeftCancellative", so we also comply this convention.

  -- div with irrelevant instance argument replaced by non-equality
  -- argument.
  div : ∀ (n d : ℤ) -> ¬ d ≡ 0ℤ -> ℤ
  div n (+ 0) n0 with n0 refl
  ... | ()
  div n d@(+[1+ n₁ ]) n0 = n divℤ d
  div n d@(-[1+_] n₁) n0 = n divℤ d

  -- mod with irrelevant instance argument replaced by non-equality
  -- argument.
  mod : ∀ (n d : ℤ) -> ¬ d ≡ 0ℤ -> ℤ
  mod n (+ 0) n0 with n0 refl
  ... | ()
  mod n d@(+[1+ n₁ ]) n0 = + (n modℤ d)
  mod n d@(-[1+_] n₁) n0 = + (n modℤ d)

  -- Divident = reminder + quotient * divisor.
  euc-eq : ∀ (n d : ℤ) (n0 : ¬ d ≡ 0ℤ) ->
               let r = mod n d n0 in let q = div n d n0 in
               n ≡ r + q * d
  euc-eq n (+ 0) n0 with n0 refl
  ... | ()
  euc-eq n d@(+[1+ n₁ ]) n0 = euc-eqℤ n d
  euc-eq n d@(-[1+_] n₁) n0 = euc-eqℤ n d

  -- The rank of the reminder is strictly smaller than the rank of the
  -- divisor.
  euc-rank : ∀ (n d : ℤ) (n0 : ¬ d ≡ 0ℤ) ->
               let r = mod n d n0 in let q = div n d n0 in
               ∣ r ∣ < ∣ d ∣
  euc-rank n (+ 0) n0 with n0 refl
  ... | ()
  euc-rank n d@(+[1+ n₁ ]) n0 = euc-rankℤ n d
  euc-rank n d@(-[1+_] n₁) n0 = euc-rankℤ n d

  -- Multiplication is left cancellative.
  *-alc-ℤ : AlmostLeftCancellative 0ℤ _*_
  *-alc-ℤ {+ 0} j k n0 with n0 refl
  ... | ()
  *-alc-ℤ {i@(+[1+ n ])} j k n0 = *-cancelˡ-≡ i j k
  *-alc-ℤ { i@(-[1+ n ])} j k n0 = *-cancelˡ-≡ i j k

  -- ℤ is an Euclidean Domain.
  +-*-isEuclideanDomain : IsEuclideanDomain _+_ _*_ -_ 0ℤ 1ℤ
  +-*-isEuclideanDomain = record
                            { isCommutativeRing = +-*-isCommutativeRing
                            ; *-alc = *-alc-ℤ
                            ; div = div
                            ; mod = mod
                            ; rank = ∣_∣
                            ; euc-eq = euc-eq
                            ; euc-rank = euc-rank
                            }

  -- Bundle.
  +-*-euclideanDomain : EuclideanDomainBundle _ _
  +-*-euclideanDomain = record
    { isEuclideanDomain = +-*-isEuclideanDomain
    }

max_stars_repo_name: onestruggler/EucDomain

max_issues_repo_name: onestruggler/EucDomain

max_forks_repo_name: onestruggler/EucDomain


text:
------------------------------------------------------------------------------
-- The gcd program is correct
------------------------------------------------------------------------------

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

-- This module proves the correctness of the gcd program using
-- the Euclid's algorithm.

module LTC-PCF.Program.GCD.Partial.CorrectnessProof where

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat.Divisibility.NotBy0.Properties
  using ( 0∤x ; x∣S→x≤S )
open import LTC-PCF.Data.Nat.Type

open import LTC-PCF.Program.GCD.Partial.CommonDivisor using ( gcdCD )
open import LTC-PCF.Program.GCD.Partial.Definitions using ( x≢0≢y ; gcdSpec )
open import LTC-PCF.Program.GCD.Partial.Divisible using ( gcdDivisible )
open import LTC-PCF.Program.GCD.Partial.GCD using ( gcd )

import LTC-PCF.Program.GCD.Partial.GreatestAnyCommonDivisor
open module GreatestAnyCommonDivisor =
  LTC-PCF.Program.GCD.Partial.GreatestAnyCommonDivisor x∣S→x≤S 0∤x
  using ( gcdGACD )

open import LTC-PCF.Program.GCD.Partial.Totality using ( gcd-N )

------------------------------------------------------------------------------
-- The gcd is correct
gcdCorrect : ∀ {m n} → N m → N n → x≢0≢y m n → gcdSpec m n (gcd m n)
gcdCorrect Nm Nn m≢0≢n = gcdCD Nm Nn m≢0≢n
                         , gcdGACD (gcd-N Nm Nn m≢0≢n)
                                   (gcdCD Nm Nn m≢0≢n)
                                   (gcdDivisible Nm Nn m≢0≢n)


text:
module Structure.Operator.Monoid where

import      Lvl
open import Logic
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Operator.Properties hiding (associativity ; identityₗ ; identityᵣ)
open import Structure.Operator
open import Type

-- A type and a binary operator using this type is a monoid when:
-- • The operator is associative.
-- • The operator have an identity in both directions.
record Monoid {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    ⦃ binary-operator ⦄    : BinaryOperator(_▫_)
    ⦃ associativity ⦄      : Associativity(_▫_)
    ⦃ identity-existence ⦄ : ∃(Identity(_▫_))

  id = [∃]-witness identity-existence

  identity : Identity (_▫_) id
  identity = [∃]-proof identity-existence

  identityₗ : Identityₗ (_▫_) id
  identityₗ = Identity.left(identity)

  identityᵣ : Identityᵣ (_▫_) id
  identityᵣ = Identity.right(identity)

  identity-existenceₗ : ∃(Identityₗ(_▫_))
  identity-existenceₗ = [∃]-intro id ⦃ identityₗ ⦄

  identity-existenceᵣ : ∃(Identityᵣ(_▫_))
  identity-existenceᵣ = [∃]-intro id ⦃ identityᵣ ⦄

record MonoidObject {ℓ ℓₑ} : Stmt{Lvl.𝐒(ℓ Lvl.⊔ ℓₑ)} where
  constructor intro
  field
    {T} : Type{ℓ}
    ⦃ equiv ⦄ : Equiv{ℓₑ}(T)
    _▫_ : T → T → T
    ⦃ monoid ⦄ : Monoid(_▫_)
  open Monoid(monoid) public

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module _ where

open import Agda.Builtin.Equality

postulate
  A : Set
  P : A → Set

data Id (A : Set) : Set where
  id : A → Id A

data Flat (@♭ A : Set) : Set where
  con : (@♭ x : A) → Flat A

counit : {@♭ A : Set} → Flat A → A
counit (con x) = x

test2 : (@♭ x : Id A) → Flat A
test2 (id x) = con x

test3 : (@♭ x : A) (@♭ y : A) (@♭ p : x ≡ y) → P x → P y
test3 x y refl p = p

test4 : (@♭ x : A) (@♭ y : A) → Flat (x ≡ y) → P x → P y
test4 x y (con refl) p = p

test6 : (@♭ x y : A) → (eq : con x ≡ con y) → P x → P y
test6 x .x refl p = p

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- {-# OPTIONS -v 10 #-}
-- {-# OPTIONS -v auto:100 #-}

postulate A : Set

X : Set₂
X = (P : Set₁) → (A → P) → P

foo : X → X
foo x P f = {!!}

-- Invoke Agsy in the hole above. Result:
--
--   Set != Set₁
--   when checking that the expression A has type Set₁
--
-- The error message points to A in the definition of X.

-- x : (P : Set₁) → (A → P) → P
-- P : Set₁
-- f : A → P
-- ? : P

-- Agsy constructs  f (x A (λ z → z))  which is ill-typed
-- as A is in the wrong universe.
-- It should take universe levels into account.

-- Temporary fix: discard wrong solution, Agsy returns nothing.


text:
module sv20.assign2.Second where
-- The solution for the second task starts in line 53

open import Data.Unit using (⊤; tt)
open import Data.Product using (_×_ ; ∃) renaming (_,_ to ⟨_,_⟩)
open import Relation.Nullary using (¬_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_∘_)

-- For the second task. We took one common definition of Subset mentioned in
-- https://stackoverflow.com/q/34183349

-- Notice that this definition is equivalent to the definition presented in the
-- Standard Library where Subset is a "record".

Subset : (A : Set) -> Set _
Subset A = A → Set

-- Because, we are using a different definition from the standard library, we
-- need to define what it means to be included in a subset, what is a relation,
-- what is the range and domain of a relation, and so forth.

_∈_ : ∀ {A} → A → Subset A → Set
a ∈ P = P a

Relation : ∀ A B → Set₁
Relation A B = Subset (A × B)

Range : ∀ {A B} → Relation A B → Subset B
Range R b = ∃ (R ∘ ⟨_, b ⟩)  -- equivalent to ∃ \a → R ⟨ a , b ⟩

Dom : ∀ {A B} → Relation A B → Subset A
Dom R a = ∃ (R ∘ ⟨ a ,_⟩)  -- equivalent to ∃ \b → R ⟨ a , b ⟩

_⊆_ : ∀ {A} → Subset A → Subset A → Set
A ⊆ B = ∀ x → x ∈ A → x ∈ B

_∩_ : ∀ {A} → Subset A → Subset A → Subset A
A ∩ B = λ x → x ∈ A × x ∈ B

_∪_ : ∀ {A} → Subset A → Subset A → Subset A
A ∪ B = λ x → x ∈ A ⊎ x ∈ B

_/_ : ∀ {A} → Subset A → Subset A → Subset A
A / B = λ x → x ∈ A × ¬ (x ∈ B)

-- Practice theorem
∪-range-⊆ : ∀ {A B} {F G : Relation A B}
          → (Range F ∪ Range G) ⊆ Range (F ∪ G)
∪-range-⊆ _ (inj₁ ⟨ a , fab ⟩) = ⟨ a , inj₁ fab ⟩
∪-range-⊆ _ (inj₂ ⟨ a , gab ⟩) = ⟨ a , inj₂ gab ⟩

-- =========== SOLUTION TO TASK 2 STARTS HERE ===========

-- range-theorem-2
range-∩-⊆ : ∀ {A B} {F G : Relation A B}
          → Range (F ∩ G) ⊆ (Range F ∩ Range G)
range-∩-⊆ b b∈RangeF∩G =  -- Given "b ∈ Range (F ∩ G)", we need to prove that "b ∈ (Range F ∩ Range G)"
  let
    ⟨ a , a,b∈F∩G ⟩ = b∈RangeF∩G  -- (1) if "b ∈ Range (F ∩ G)" then there exists 'a' such that "(a,b) ∈ (F ∩ G)"
    ⟨ a,b∈F , a,b∈G ⟩ = a,b∈F∩G   -- (2) per definition of intersection, if "(a,b) ∈ (F ∩ G)" then "(a,b) ∈ F" and "(a,b) ∈ G"
    b∈RangeF = ⟨ a , a,b∈F ⟩      -- (3) from (1) we know there is an 'a' such that "(a,b) ∈ F" (2), so "b ∈ Range F", per definition of Range
    b∈RangeG = ⟨ a , a,b∈G ⟩      -- (4) as above, "b ∈ Range G" because of 'a' (1) and "(a,b) ∈ F" (2)
    b∈RangeF∩RangeG = ⟨ b∈RangeF , b∈RangeG ⟩ -- (5) given "b ∈ Range F" (3) and "b ∈ Range G" (4), and definition of ∩ "b ∈ Range F ∩ Range G". QED
  in b∈RangeF∩RangeG

-- dom-theorem-3
dom-/-⊆ : ∀ {A B} {F G : Relation A B}
        → (Dom F / Dom G) ⊆ Dom (F / G)
dom-/-⊆ a a∈DomF/DomG =  -- Given "a ∈ (Dom F / Dom G)", we need to prove that "a ∈ Dom (F / G)"
  let
    ⟨ a∈DomF , ¬a∈DomG ⟩ = a∈DomF/DomG  -- (1) per definition of '/', "a ∈ (Dom F / Dom G)" is the same as "a ∈ Dom F" and "¬ a ∈ Dom G"
    ⟨ b , a,b∈F ⟩ = a∈DomF              -- (2) per definition of 'Dom', if "a ∈ Dom F" then there exists 'b' such that "(a,b) ∈ F"
    ¬a,b∈G =                            -- (3) From "¬ a ∈ Dom G" we can prove that "¬ (a, b₁) ∈ G" for any 'b₁'
            λ{ a,b∈G →                     -- (a) By contradiction, suposse that "(a, b₁) ∈ G" for some 'b₁'
            let a∈DomG = ⟨ _ , a,b∈G ⟩     -- (b) per definition of 'Dom', "a ∈ Dom G"
            in ¬a∈DomG a∈DomG }            -- We know that "¬ a ∈ Dom G" (3) and "a ∈ Dom G" (b). Nonesense! So, "¬ (a, b₁) ∈ G" for all 'b₁'
    a,b∈F/G = ⟨ a,b∈F , ¬a,b∈G ⟩        -- (4) per definition of '/' and given (2) and (3), "(a, b) ∈ F/G"
    a∈DomF/G = ⟨ b , a,b∈F/G ⟩          -- (5) per definition of 'Dom' and given (4) and 'b', we have that "a ∈ Dom (F / G)". QED
  in a∈DomF/G

-- range-theorem-3
/-range-⊆ : ∀ {A B} {F G : Relation A B}
          → (Range F / Range G) ⊆ Range (F / G)
/-range-⊆ b b∈RangeF/RangeG = -- Given "b ∈ (Range F / Range G)", we need to prove that "b ∈ Range (F / G)"
  let
    ⟨ b∈RangeF , ¬b∈RangeG ⟩ = b∈RangeF/RangeG -- (1) per definition of '/', "b ∈ Range F" and "¬ b ∈ Range G"
    ⟨ a , a,b∈F ⟩ = b∈RangeF                   -- (2) per definition of 'Range', there exists 'a' such that "(a,b) ∈ F"
    ¬a,b∈G =                                   -- (3) by contradiction, we will prove that "¬ (a, b) ∈ G" given (1)
            λ{ a,b∈G →                           -- (a) suppose that there exists 'a₁' such that "(a₁, b) ∈ G"
            let b∈RangeG = ⟨ _ , a,b∈G ⟩         -- (b) per definition of Range and given (a), "b ∈ Range G"
            in ¬b∈RangeG b∈RangeG }              -- (c) we know from (1) that "¬ b ∈ Range G" but (b) says "b ∈ Range G". Nonesense!
    a,b∈F/G = ⟨ a,b∈F , ¬a,b∈G ⟩               -- (4) per definition of '/' and given (2) and (3), then "(a, b) ∈ F / G"
    b∈RangeF/G = ⟨ a , a,b∈F/G ⟩               -- (5) per definition of 'Range' and given 'a' and (4), we know that "b ∈ Range (F / G)". QED
  in b∈RangeF/G

-- Class exercise
-- This is not really an exercise at all because this is the definition of `⊆`!
exercise103a : ∀ {a} {A B : Subset a}
             → (∀ x → x ∈ A → x ∈ B)
             → A ⊆ B
exercise103a x→x∈A→x∈B = x→x∈A→x∈B

open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong)

exercise103id→ : ∀ {a} {A B : Subset a}
              → A ≡ B → A ⊆ B × B ⊆ A
exercise103id→ refl = ⟨ (λ{_ p → p}) , (λ{_ p → p}) ⟩

--exercise103id← : ∀ {a} {A B : Subset a}
--              → A ⊆ B × B ⊆ A → A ≡ B
--exercise103id← ⟨ A⊆B , B⊆A ⟩ = ? -- Probably impossible to prove without unification. Possibly, impossible to prove. Needs `postulate`

exercise108a : ∀ {a} {A B : Subset a} (z : a)
             → (z ∈ A) × (z ∈ B) → z ∈ (A ∩ B)
exercise108a _ ⟨ z∈A , z∈B ⟩ = ⟨ z∈A , z∈B ⟩ -- How to explain this?


text:
module NatTactic where

  module _ where
    open import Agda.Builtin.Nat
    open import Agda.Builtin.List

    -- n .. 1
    downFrom : Nat → List Nat
    downFrom zero    = []
    downFrom (suc n) = suc n ∷ downFrom n

  module AgdaPreludeTest where
    open import Prelude
    open import Tactic.Nat

-- All tactics know about addition, multiplication and subtraction
-- of natural numbers, and can prove equalities and inequalities (_<_).
-- The available tactics are:

{-
  auto

    Prove an equation or inequality.
-}

    auto-example₁ : (a b : Nat) → (a - b) * (a + b) ≡ a ^ 2 - b ^ 2
    auto-example₁ a b = auto

    auto-example₂ : (a b : Nat) → (a + b) ^ 2 ≥ a ^ 2 + b ^ 2
    auto-example₂ a b = auto

{-
  by eq

    Prove the goal using the given assumption. For equalities it simplifies
    the goal and the assumption and checks if they match any of the following
    forms (up to symmetry):

          a ≡ b → a ≡ b
      a + b ≡ 0 → a ≡ 0

    For inequalities, to prove a < b -> c < d, it simplifies the assumption and
    goal and then tries to prove c′ ≤ a′ and b′ ≤ d′.

    When proving that an inequality follows from an equality a ≡ b, the equality
    is weakened to a ≤ b before applying the above procedure.

    Proving an equality from an inequality works if the inequality simplifies to
    a ≤ 0 (or a < 0 in which case it's trivial). It then reduces that to a ≡ 0
    and tries to prove the goal from that.
-}

    by-example₁ : (xs ys : List Nat) → sum (xs ++ ys) ≡ sum ys + sum xs
    by-example₁ []       ys = auto
    by-example₁ (x ∷ xs) ys = by (by-example₁ xs ys)

    by-example₂ : (a b c : Nat) → a + c < b + c → a < b
    by-example₂ a b c lt = by lt

    by-example₃ : (a b : Nat) → a ≡ b * 2 → a + b < (b + 1) * 3
    by-example₃ a b eq = by eq

    by-example₄ : (a b c : Nat) → a + b + c ≤ b → 2 * c ≡ c
    by-example₄ a b c lt = by lt

    by-example₅ : (a b c : Nat) → a + b ≡ b + c → 2 + a ≡ 1 + c + 1
    by-example₅ a b c eq = by eq

{-
  refute eq

  Proves an arbitrary proposition given a false equation. Works for equations
  that simplify to 0 ≡ suc n (or symmetric) or n < 0, for some n.
-}

    refute-example₁ : {Anything : Set} (a : Nat) → a ≡ 2 * a + 1 → Anything
    refute-example₁ a eq = refute eq

    refute-example₂ : {Anything : Set} (a b : Nat) → a + b < a → Anything
    refute-example₂ a b lt = refute lt

{-
  simplify-goal ?

    Simplify the current goal and let you keep working on the new goal.
    In most cases 'by prf' works better than
    'simplify-goal => prf' since it will also simplify prf. The advantage
    of simplify-goal is that it allows holes in prf.
-}

    simplify-goal-example₁ : (a b : Nat) → a - b ≡ b - a → a ≡ b
    simplify-goal-example₁  zero    b      eq = by eq
    simplify-goal-example₁ (suc a)  zero   eq = refute eq
    simplify-goal-example₁ (suc a) (suc b) eq =
      simplify-goal (simplify-goal-example₁ a b eq)
      -- Old goal: suc a ≡ suc b
      -- New goal:     a ≡ b

    simplify-goal-example₂ : (a b : Nat) → a - b ≡ b - a → a < suc b
    simplify-goal-example₂  zero    b      eq = by eq
    simplify-goal-example₂ (suc a)  zero   eq = refute eq
    simplify-goal-example₂ (suc a) (suc b) eq =
      simplify-goal (simplify-goal-example₂ a b eq)
      -- Old goal: suc a ≤ suc b
      -- New goal:     a ≤ b

    simplify-goal-example₃ : (a b c : Nat) → a ≡ c → a + b ≡ b + c
    simplify-goal-example₃ a b c eq = simplify-goal eq

{-
  simplify eq λ x → ?

    Simplify the given equation (and the current goal) and bind the simplified
    equation to x in the new goal.
-}

    lemma₁ : (a b : Nat) → a + b ≡ 0 → a ≡ 0
    lemma₁ zero    b eq = refl
    lemma₁ (suc a) b eq = refute eq

    simplify-example₁ : ∀ a b → (a + 1) * (b + 1) ≡ a * b + 1 → a ≡ 0
    simplify-example₁ a b eq = simplify eq λ eq′ → lemma₁ a b eq′

    lemma₂ : (a b : Nat) → a + b ≡ 0 → a < suc 0
    lemma₂ zero    b eq = auto
    lemma₂ (suc a) b eq = refute eq

    simplify-example₂ : ∀ a b → (a + 1) * (b + 1) ≡ a * b + 1 → a < suc 0
    simplify-example₂ a b eq = simplify eq λ eq′ → by (lemma₂ a b eq′)

    simplify-example₃ : (a b c : Nat) → a + b ≡ b + c → 2 + a ≡ 1 + c + 1
    simplify-example₃ a b c eq = simplify eq λ eq′ → eq′

{-
  induction

    Prove a goal ∀ n → P n using induction. Applies 'auto' in the base case
    and 'by IH' in the step case.
-}

    induction-example₁ : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)
    induction-example₁ = induction

    induction-example₂ : ∀ n → sum (downFrom n) * 2 < suc (n * (n + 1))
    induction-example₂ = induction

  -- some equivalences needed to adapt Tactic.Nat to the standard library
  module EquivalenceOf≤ where
    open import Agda.Builtin.Equality
    open import Agda.Builtin.Nat

    open import Data.Nat using (less-than-or-equal) renaming (_≤_ to _≤s_)
    open import Data.Nat.Properties using (≤⇒≤″; ≤″⇒≤)
    open import Prelude using (diff; id) renaming (_≤_ to _≤p_)

    open import Tactic.Nat.Generic (quote _≤p_) (quote id) (quote id) using (by)

    ≤p→≤s : ∀ {a b} → a ≤p b → a ≤s b
    ≤p→≤s (diff k b₊₁≡k₊₁+a) = ≤″⇒≤ (less-than-or-equal {k = k} (by b₊₁≡k₊₁+a))

    ≤s→≤p : ∀ {a b} → a ≤s b → a ≤p b
    ≤s→≤p a≤sb with ≤⇒≤″ a≤sb
    ≤s→≤p _ | less-than-or-equal {k = k} a+k≡b = diff k (by a+k≡b)

  module StandardLibraryTest where
    open import Agda.Builtin.Equality
    open import Data.Nat
    open import Data.List hiding (downFrom)
    open import Function

    private
      infixr 8 _^_
      _^_ : ℕ → ℕ → ℕ
      n ^ zero  = 1
      n ^ suc m = n ^ m * n

    open EquivalenceOf≤
    open import Tactic.Nat.Generic (quote _≤_) (quote ≤s→≤p) (quote ≤p→≤s)

    auto-example₁ : (a b : ℕ) → (a ∸ b) * (a + b) ≡ a ^ 2 ∸ b ^ 2
    auto-example₁ a b = auto

    auto-example₂ : (a b : ℕ) → (a + b) ^ 2 ≥ a ^ 2 + b ^ 2
    auto-example₂ a b = auto

    by-example₁ : (xs ys : List ℕ) → sum (xs ++ ys) ≡ sum ys + sum xs
    by-example₁ []       ys = auto
    by-example₁ (x ∷ xs) ys = by (by-example₁ xs ys)

    by-example₂ : (a b c : ℕ) → a + c < b + c → a < b
    by-example₂ a b c lt = by lt

    by-example₃ : (a b : ℕ) → a ≡ b * 2 → a + b < (b + 1) * 3
    by-example₃ a b eq = by eq

    by-example₄ : (a b c : ℕ) → a + b + c ≤ b → 2 * c ≡ c
    by-example₄ a b c lt = by lt

    by-example₅ : (a b c : ℕ) → a + b ≡ b + c → 2 + a ≡ 1 + c + 1
    by-example₅ a b c eq = by eq

    refute-example₁ : {Anything : Set} (a : ℕ) → a ≡ 2 * a + 1 → Anything
    refute-example₁ a eq = refute eq

    refute-example₂ : {Anything : Set} (a b : ℕ) → a + b < a → Anything
    refute-example₂ a b lt = refute lt

    simplify-goal-example₁ : (a b : ℕ) → a ∸ b ≡ b ∸ a → a ≡ b
    simplify-goal-example₁  zero    b      eq = by eq
    simplify-goal-example₁ (suc a)  zero   eq = refute eq
    simplify-goal-example₁ (suc a) (suc b) eq =
      simplify-goal (simplify-goal-example₁ a b eq)

    simplify-goal-example₂ : (a b : ℕ) → a ∸ b ≡ b ∸ a → a < suc b
    simplify-goal-example₂  zero    b      eq = by eq
    simplify-goal-example₂ (suc a)  zero   eq = refute eq
    simplify-goal-example₂ (suc a) (suc b) eq =
      simplify-goal (by (simplify-goal-example₂ a b eq))

    simplify-goal-example₃ : (a b c : ℕ) → a ≡ c → a + b ≡ b + c
    simplify-goal-example₃ a b c eq = simplify-goal eq

    lemma₁ : (a b : ℕ) → a + b ≡ 0 → a ≡ 0
    lemma₁ zero    b eq = refl
    lemma₁ (suc a) b eq = refute eq

    simplify-example₁ : ∀ a b → (a + 1) * (b + 1) ≡ a * b + 1 → a ≡ 0
    simplify-example₁ a b eq = simplify eq λ eq′ → lemma₁ a b eq′

    lemma₂ : (a b : ℕ) → a + b ≡ 0 → a < suc 0
    lemma₂ zero    b eq = s≤s z≤n
    lemma₂ (suc a) b eq = refute eq

    simplify-example₂ : ∀ a b → (a + 1) * (b + 1) ≡ a * b + 1 → a < suc 0
    simplify-example₂ a b eq = simplify eq λ eq′ → by (lemma₂ a b eq′)

    simplify-example₃ : (a b c : ℕ) → a + b ≡ b + c → 2 + a ≡ 1 + c + 1
    simplify-example₃ a b c eq = simplify eq λ eq′ → eq′

    induction-example₁ : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)
    induction-example₁ = induction

    induction-example₂ : ∀ n → sum (downFrom n) * 2 < suc (n * (n + 1))
    induction-example₂ = induction

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
module Issue326 where

open import Common.Prelude
open import Common.MAlonzo using () -- see issue 561

postulate
  QName : Set
  printBool : Bool → IO Unit

{-# BUILTIN QNAME QName #-}
{-# COMPILED printBool print #-}

primitive primQNameEquality : QName → QName → Bool

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

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Categories.Category

-- we use duality to prove properties about coequalizer
module Categories.Diagram.Coequalizer.Properties {o ℓ e} (C : Category o ℓ e) where

open Category C

open import Categories.Diagram.Coequalizer C
open import Categories.Morphism C
open import Categories.Diagram.Equalizer op
open import Categories.Diagram.Duality C

private
  variable
    A B : Obj
    f g : A ⇒ B

module _ (coe : Coequalizer f g) where
  open Coequalizer coe

  private
    equalizer : Equalizer f g
    equalizer = Coequalizer⇒coEqualizer coe

  open Equalizer equalizer
    using (unique′; equality-∘; unique-diagram)
    renaming ( id-equalize      to id-coequalize
             ; equalize-resp-≈  to coequalize-resp-≈
             ; equalize-resp-≈′ to coequalize-resp-≈′
             )
    public

  Coequalizer⇒Epi : Epi arr
  Coequalizer⇒Epi = Equalizer⇒Mono equalizer

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories