text:
module BBHeap {A : Set}(_≤_ : A → A → Set) where

open import BHeap _≤_ hiding (forget ; # ; flatten)
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import BTree {A} hiding (flatten)
open import Data.Nat
open import Data.List

mutual
  data BBHeap : Bound → Set where
    leaf : {b : Bound} → BBHeap b
    left : {b : Bound}{x : A}{l r : BBHeap (val x)}
                   → LeB b (val x)
                   → l ⋘ r
                   → BBHeap b
    right : {b : Bound}{x : A}{l r : BBHeap (val x)}
                   → LeB b (val x)
                   → l ⋙ r
                   → BBHeap b

  data _≃_ : {b b' : Bound} → BBHeap b → BBHeap b' → Set where
    ≃lf : {b b' : Bound} → leaf {b} ≃ leaf {b'}
    ≃nd : {b b' : Bound}{x x' : A}{l r : BBHeap (val x)}{l' r' : BBHeap (val x')}
                  → (b≤x : LeB b (val x))
                  → (b'≤x' : LeB b' (val x'))
                  → (l⋘r : l ⋘ r)
                  → (l'⋘r' : l' ⋘ r')
                  → l ≃ r
                  → l' ≃ r'
                  → l ≃ l'
                  → (left b≤x l⋘r) ≃ (left b'≤x' l'⋘r')

  data _⋘_ : {b b' : Bound} → BBHeap b → BBHeap b' → Set where
    lf⋘ : {b b' : Bound}
                  → leaf {b} ⋘ leaf {b'}
    ll⋘ : {b b' : Bound}{x x' : A}{l r : BBHeap (val x)}{l' r' : BBHeap (val x')}
                  → (b≤x : LeB b (val x))
                  → (b'≤x' : LeB b' (val x'))
                  → (l⋘r : l ⋘ r)
                  → (l'⋘r' : l' ⋘ r')
                  → (l'≃r' : l' ≃ r')
                  → r ≃ l'
                  → (left b≤x l⋘r) ⋘ (left b'≤x' l'⋘r')
    lr⋘ : {b b' : Bound}{x x' : A}{l r : BBHeap (val x)}{l' r' : BBHeap (val x')}
                  → (b≤x : LeB b (val x))
                  → (b'≤x' : LeB b' (val x'))
                  → (l⋙r : l ⋙ r)
                  → (l'⋘r' : l' ⋘ r')
                  → (l'≃r' : l' ≃ r')
                  → l ⋗ l'
                  → (right b≤x l⋙r) ⋘ (left b'≤x' l'⋘r')

  data _⋙_ : {b b' : Bound} → BBHeap b → BBHeap b' → Set where
    ⋙lf : {b b' : Bound}{x : A}
                  → (b≤x : LeB b (val x))
                  → (left b≤x lf⋘) ⋙ leaf {b'}
    ⋙rl : {b b' : Bound}{x x' : A}{l r : BBHeap (val x)}{l' r' : BBHeap (val x')}
                  → (b≤x : LeB b (val x))
                  → (b'≤x' : LeB b' (val x'))
                  → (l⋘r : l ⋘ r)
                  → (l≃r : l ≃ r)
                  → (l'⋘r' : l' ⋘ r')
                  → l ⋗ r'
                  → (left b≤x l⋘r) ⋙ (left b'≤x' l'⋘r')
    ⋙rr : {b b' : Bound}{x x' : A}{l r : BBHeap (val x)}{l' r' : BBHeap (val x')}
                  → (b≤x : LeB b (val x))
                  → (b'≤x' : LeB b' (val x'))
                  → (l⋘r : l ⋘ r)
                  → (l≃r : l ≃ r)
                  → (l'⋙r' : l' ⋙ r')
                  →  l ≃ l'
                  → (left b≤x l⋘r) ⋙ (right b'≤x' l'⋙r')

  data _⋗_ : {b b' : Bound} → BBHeap b → BBHeap b' → Set where
    ⋗lf : {b b' : Bound}{x : A}
                  → (b≤x : LeB b (val x))
                  → (left b≤x lf⋘) ⋗ (leaf {b'})
    ⋗nd : {b b' : Bound}{x x' : A}{l r : BBHeap (val x)}{l' r' : BBHeap (val x')}
                  → (b≤x : LeB b (val x))
                  → (b'≤x' : LeB b' (val x'))
                  → (l⋘r : l ⋘ r)
                  → (l'⋘r' : l' ⋘ r')
                  → l ≃ r
                  → l' ≃ r'
                  → l ⋗ l'
                  → (left b≤x l⋘r) ⋗ (left b'≤x' l'⋘r')

# : {b : Bound} → BBHeap b → ℕ
# leaf = zero
# (left {l = l} {r = r} _ _) = suc (# l + # r)
# (right {l = l} {r = r} _ _) = suc (# l + # r)

relax : {b : Bound}(h : BBHeap b) → BHeap b
relax leaf = lf
relax (left {l = l} {r = r} b≤x _) = nd b≤x (relax l) (relax r)
relax (right {l = l} {r = r} b≤x _) = nd b≤x (relax l) (relax r)

forget : {b : Bound}(h : BBHeap b) → BTree
forget leaf = leaf
forget (left {x = x} {l = l} {r = r} _ _) = node x (forget l) (forget r)
forget (right {x = x} {l = l} {r = r} _ _) = node x (forget l) (forget r)

flatten : {b : Bound} → BBHeap b → List A
flatten leaf = []
flatten (left {x = x} {l = l} {r = r} _ _) = x ∷ flatten l ++ flatten r
flatten (right {x = x} {l = l} {r = r} _ _) = x ∷ flatten l ++ flatten r

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- broken since the clocks are not supposed to be freely instantiable
open import guarded-recursion.prelude
  renaming (O to zero; S to suc)
open Coe
module guarded-recursion.clocks
    (Clk : Type)
    (▹ : ∀ {a} → Clk → Set a → Set a)

    (▹′ : ∀ {a} κ → ▹ κ (Set a) → Set a)
   --▹′ κ A = ▹ κ A

    (next : ∀ {κ a} {A : Set a} → A → ▹ κ A)

    (▹′-rule : ∀ {κ a} {A : Set a} → ▹′ κ (next A) ≡ ▹ κ A)
    -- (▹′-rule : ∀ {a} {A : Set a} → ▹′ ∘ next ≡ ▹_ {A})

    (fix      : ∀ {κ a} {A : Set a} → (▹ κ A → A) → A)
    (fix-rule : ∀ {κ a} {A : Set a} {f : ▹ κ A → A} → fix f ≡ f (next (fix f)))

    (_⊛_ : ∀ {κ a b} {A : Set a} {B : Set b} → ▹ κ (A → B) → ▹ κ A → ▹ κ B)

    (fix-uniq : ∀ {κ a} {A : Set a} (u : A) (f : ▹ κ A → A) → u ≡ f (next u) → u ≡ fix f)

    (next⊛next : ∀ {κ a b} {A : Set a} {B : Set b} (f : A → B) (x : A)
                 → next f ⊛ next x ≡ next {κ} (f x))

    where

    roll▹′ : ∀ {κ a} {A : Set a} → ▹ κ A → ▹′ κ (next A)
    roll▹′ = coe! ▹′-rule

    un▹′ : ∀ {κ a} {A : Set a} → ▹′ κ (next A) → ▹ κ A
    un▹′ = coe ▹′-rule

    ▹Fix : ∀ {a} → Clk → Set a → Set a
    ▹Fix κ X = (▹ κ X → X) → X

    ▹Endo : ∀ {a} → Clk → Set a → Set a
    ▹Endo κ X = ▹ κ X → X

    μ : ∀ {a} → Fix (Set a)
    μ F = ∀ {κ} → fix (F ∘ ▹′ κ)

    un : ∀ {κ a f} → fix {κ} {A = Set a} f → f (next (fix f))
    un = coe fix-rule

    {-
    unμ : ∀ {κ a} f → μ {a} f → f (▹ κ (μ f))
    unμ {κ} {a} f x rewrite sym (▹′-rule {κ} {A = μ f}) = {!un {κ} x!}
    -}

    roll : ∀ {κ a f} → f (next (fix f)) → fix {κ} {A = Set a} f
    roll = coe! fix-rule

    {-
    μ-rule : ∀ {κ a} f → μ {a} f ≡ f (▹ κ (μ f))
    μ-rule f = {!trans fix-rule (cong f (▹′-rule {A = μ f}))!}
    -}

    {-
    rollμ : ∀ {a} f → (∀ {κ} → f (▹ κ (μ f))) → μ {a} f
    rollμ f x {κ} = {!roll (x {κ})!}
    -- rollμ f = subst id (sym (μ-rule f))
    -}

    un₁ : ∀ {κ a b} {A : Set a} {f x} → fix {κ} {A = A → Set b} f x → f (next (fix f)) x
    un₁ = coe₁ fix-rule

    roll₁ : ∀ {κ a b} {A : Set a} {f x} → f (next (fix f)) x → fix {κ} {A = A → Set b} f x
    roll₁ = coe₁! fix-rule

    un₂ : ∀ {κ a b} {A : Set a} {B : Set b} {c f x y} → fix {κ} {A = A → B → Set c} f x y → f (next (fix f)) x y
    un₂ = coe₂ fix-rule

    roll₂ : ∀ {κ a b} {A : Set a} {B : Set b} {c f x y} → f (next (fix f)) x y → fix {κ} {A = A → B → Set c} f x y
    roll₂ = coe₂! fix-rule

    map▹ : ∀ {κ a b} {A : Set a} {B : Set b} → (A → B) → ▹ κ A → ▹ κ B
    map▹ f ▹x = next f ⊛ ▹x

    _⊛′_ : ∀ {κ a b} {A : Set a} {B : A → Set b} → ▹ κ ((x : A) → B x) → (x : A) → ▹ κ (B x)
    ▹f ⊛′ x = map▹ (λ f → f x) ▹f

    module SimpleStream where
      F : Type → Type → Type
      F A X = A × X

      S : Type → Type
      S A = μ (F A)

    {-
    data IsStream (s : S A) : Type where
      -- cons : ∀ x xs → IsStream xs → IsStream (cons x xs)
      cons : ∀ x xs → (▹ IsStream) ⊛ next xs → IsStream (cons x xs)
      cons : ∀ x xs → ▹ (IsStream xs) → IsStream (cons x xs)

      -}

    μ₁F' : ∀ {κ a} {A : Set a} → ((A → ▹ κ Type) → A → Type) → (▹ κ (A → Type) → A → Type)
    μ₁F' F self = F (λ x → (self ⊛ next x))

    μ₁F : ∀ {κ a} {A : Set a} → ((A → Type) → A → Type) → (▹ κ (A → Type) → A → Type)
    μ₁F F self = F (λ x → ▹′ _ (self ⊛ next x))

    -- μ₁ : Fix (Endo Type)
    μ₁ : ∀ {a} {A : Set a} → ((A → Type) → A → Type) → A → Type
    μ₁ F x = ∀ {κ} → fix (μ₁F {κ} F) x

    module μId where
        μid : Type
        μid = μ id

        {-
        μid-rule : μid ≡ (∀ {κ} → ▹ κ μid)
        μid-rule = {!trans fix-rule (▹′-rule {A = μ id})!}
        -}

        {-
        ω : μid
        ω = fix (rollμ id)
        -}

ext: agda

max_stars_repo_name: np/guarded-recursion

max_issues_repo_name: np/guarded-recursion

max_forks_repo_name: np/guarded-recursion


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

module Relation.Binary where

open import Level
open import Relation.Nullary
open import Path as ≡ hiding (sym; refl)
open import Data.Sum
open import Function
open import Data.Bool as Bool using (Bool; true; false; T; bool)
open import Relation.Nullary.Decidable
open import Relation.Nullary.Discrete

module _ (_~_ : A → A → Type b) where
  Reflexive : Type _
  Reflexive = ∀ {x} → x ~ x

  Transitive : Type _
  Transitive = ∀ {x y z} → x ~ y → y ~ z → x ~ z

  Symmetric : Type _
  Symmetric = ∀ {x y} → x ~ y → y ~ x

  Decidable : Type _
  Decidable = ∀ x y → Dec (x ~ y)

  Antisymmetric : Type _
  Antisymmetric = ∀ {x y} → x ~ y → y ~ x → x ≡ y

  Total : Type _
  Total = ∀ x y → (x ~ y) ⊎ (y ~ x)

data Tri {a r₁ r₂ r₃} {A : Type a} (R₁ : A → A → Type r₁) (R₂ : A → A → Type r₂) (R₃ : A → A → Type r₃) (x y : A) : Type (a ℓ⊔ r₁ ℓ⊔ r₂ ℓ⊔ r₃) where
  lt : (x<y : R₁ x y) → Tri R₁ R₂ R₃ x y
  eq : (x≡y : R₂ x y) → Tri R₁ R₂ R₃ x y
  gt : (x>y : R₃ x y) → Tri R₁ R₂ R₃ x y

record PartialOrder {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂) where
  infix 4 _≤_
  field
    _≤_ : 𝑆 → 𝑆 → Type ℓ₂
    refl : Reflexive _≤_
    antisym : Antisymmetric _≤_
    trans : Transitive _≤_

record TotalOrder {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂) where
  field
    partialOrder : PartialOrder 𝑆 ℓ₂
  open PartialOrder partialOrder public

  infix 4 _≤ᵇ_ _≤?_
  field
    _≤?_ : Total _≤_

  _≤ᵇ_ : 𝑆 → 𝑆 → Bool
  x ≤ᵇ y = is-l (x ≤? y)

  open import Data.Unit
  open import Data.Empty
  open import Data.Sigma

  total⇒discrete : Discrete 𝑆
  total⇒discrete x y with x ≤? y | inspect (x ≤?_) y | y ≤? x | inspect (y ≤?_) x
  total⇒discrete x y | inl x₁ | 〖 xy 〗 | inl x₂ | 〖 yx 〗 = yes (antisym x₁ x₂)
  total⇒discrete x y | inr x₁ | 〖 xy 〗 | inr x₂ | 〖 yx 〗 = yes (antisym x₂ x₁)
  total⇒discrete x y | inl x₁ | 〖 xy 〗 | inr x₂ | 〖 yx 〗 = no (λ p → subst (bool ⊥ ⊤) (cong is-l (≡.sym xy) ; cong₂ _≤ᵇ_ p (≡.sym p) ; cong is-l yx) tt)
  total⇒discrete x y | inr x₁ | 〖 xy 〗 | inl x₂ | 〖 yx 〗 = no (λ p → subst (bool ⊤ ⊥) (cong is-l (≡.sym xy) ; cong₂ _≤ᵇ_ p (≡.sym p) ; cong is-l yx) tt)

  infix 4 _<_
  _<_ : 𝑆 → 𝑆 → Type (ℓ₁ ℓ⊔ ℓ₂)
  x < y = (x ≢ y) × (x ≤ y)

  Ordering : 𝑆 → 𝑆 → Type (ℓ₁ ℓ⊔ ℓ₂)
  Ordering = Tri _<_ _≡_ (flip _<_)

  compare : ∀ x y → Ordering x y
  compare x y with x ≤? y | inspect (x ≤?_) y | y ≤? x | inspect (y ≤?_) x
  compare x y | inl x₁ | 〖 xy 〗 | inl x₂ | 〖 yx 〗 = eq (antisym x₁ x₂)
  compare x y | inr x₁ | 〖 xy 〗 | inr x₂ | 〖 yx 〗 = eq (antisym x₂ x₁)
  compare x y | inl x₁ | 〖 xy 〗 | inr x₂ | 〖 yx 〗 = lt ((λ p → subst (bool ⊥ ⊤) (cong is-l (≡.sym xy) ; cong₂ _≤ᵇ_ p (≡.sym p) ; cong is-l yx) tt) , x₁)
  compare x y | inr x₁ | 〖 xy 〗 | inl x₂ | 〖 yx 〗 = gt ((λ p → subst (bool ⊤ ⊥) (cong is-l (≡.sym xy) ; cong₂ _≤ᵇ_ (≡.sym p) p ; cong is-l yx) tt) , x₁)

record Equivalence {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂) where
  infix 4 _≋_
  field
    _≋_ : 𝑆 → 𝑆 → Type ℓ₂
    sym   : ∀ {x y} → x ≋ y → y ≋ x
    refl  : ∀ {x} → x ≋ x
    trans : ∀ {x y z} → x ≋ y → y ≋ z → x ≋ z

≡-equivalence : ∀ {a} {A : Set a} → Equivalence A a
≡-equivalence = record
  { _≋_ = _≡_
  ; sym = ≡.sym
  ; refl = ≡.refl
  ; trans = _;_
  }

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.FinData
open import Cubical.Data.Vec
open import Cubical.Data.Bool using (Bool; true; false; if_then_else_)

open import Cubical.Algebra.RingSolver.RawRing
open import Cubical.Algebra.RingSolver.AlmostRing renaming (⟨_⟩ to ⟨_⟩ᵣ)

private
  variable
    ℓ : Level

{-
  This defines the type of multivariate Polynomials over the RawRing R.
  The construction is based on the algebraic fact

    R[X₀][X₁]⋯[Xₙ] ≅ R[X₀,⋯,Xₙ]

  BUT: Contrary to algebraic convetions, we will give 'Xₙ' the lowest index
  in the definition of 'Variable' below. So if 'Variable n R k' is identified
  with 'Xₖ', then the RawRing we construct should rather be denoted with

    R[Xₙ][Xₙ₋₁]⋯[X₀]

  or, to be precise about the evaluation order:

    (⋯((R[Xₙ])[Xₙ₋₁])⋯)[X₀]

-}

data IteratedHornerForms (R : RawRing {ℓ}) : ℕ → Type ℓ where
  const : ⟨ R ⟩ → IteratedHornerForms R ℕ.zero
  0H : {n : ℕ} → IteratedHornerForms R (ℕ.suc n)
  _·X+_ : {n : ℕ} → IteratedHornerForms R (ℕ.suc n) → IteratedHornerForms R n
                  → IteratedHornerForms R (ℕ.suc n)

eval : {R : RawRing {ℓ}} (n : ℕ) (P : IteratedHornerForms R n)
             → Vec ⟨ R ⟩ n → ⟨ R ⟩
eval ℕ.zero (const r) [] = r
eval {R = R} .(ℕ.suc _) 0H (_ ∷ _) = RawRing.0r R
eval {R = R} (ℕ.suc n) (P ·X+ Q) (x ∷ xs) =
  let open RawRing R
  in (eval (ℕ.suc n) P (x ∷ xs)) · x + eval n Q xs

module IteratedHornerOperations (R : RawRing {ℓ}) where
  open RawRing R

  private
    1H' : (n : ℕ) → IteratedHornerForms R n
    1H' ℕ.zero = const 1r
    1H' (ℕ.suc n) = 0H ·X+ 1H' n

    0H' : (n : ℕ) → IteratedHornerForms R n
    0H' ℕ.zero = const 0r
    0H' (ℕ.suc n) = 0H

  1ₕ : {n : ℕ} → IteratedHornerForms R n
  1ₕ {n = n} = 1H' n

  0ₕ : {n : ℕ} → IteratedHornerForms R n
  0ₕ {n = n} = 0H' n

  X : (n : ℕ) (k : Fin n) → IteratedHornerForms R n
  X (ℕ.suc m) zero = 1ₕ ·X+ 0ₕ
  X (ℕ.suc m) (suc k) = 0ₕ ·X+ X m k

  _+ₕ_ : {n : ℕ} → IteratedHornerForms R n → IteratedHornerForms R n
               → IteratedHornerForms R n
  (const r) +ₕ (const s) = const (r + s)
  0H +ₕ Q = Q
  (P ·X+ r) +ₕ 0H = P ·X+ r
  (P ·X+ r) +ₕ (Q ·X+ s) = (P +ₕ Q) ·X+ (r +ₕ s)

  -ₕ : {n : ℕ} → IteratedHornerForms R n → IteratedHornerForms R n
  -ₕ (const x) = const (- x)
  -ₕ 0H = 0H
  -ₕ (P ·X+ Q) = (-ₕ P) ·X+ (-ₕ Q)

  isZero : {n : ℕ} → IteratedHornerForms R (ℕ.suc n)
                   → Bool
  isZero 0H = true
  isZero (P ·X+ P₁) = false

  _⋆_ : {n : ℕ} → IteratedHornerForms R n → IteratedHornerForms R (ℕ.suc n)
                → IteratedHornerForms R (ℕ.suc n)
  _·ₕ_ : {n : ℕ} → IteratedHornerForms R n → IteratedHornerForms R n
                → IteratedHornerForms R n
  r ⋆ 0H = 0H
  r ⋆ (P ·X+ Q) = (r ⋆ P) ·X+ (r ·ₕ Q)

  const x ·ₕ const y = const (x · y)
  0H ·ₕ Q = 0H
  (P ·X+ Q) ·ₕ S =
     let
        z = (P ·ₕ S)
     in if (isZero z)
        then (Q ⋆ S)
        else (z ·X+ 0ₕ) +ₕ (Q ⋆ S)

  asRawRing : (n : ℕ) → RawRing {ℓ}
  RawRing.Carrier (asRawRing n) = IteratedHornerForms R n
  RawRing.0r (asRawRing n) = 0ₕ
  RawRing.1r (asRawRing n) = 1ₕ
  RawRing._+_ (asRawRing n) = _+ₕ_
  RawRing._·_ (asRawRing n) = _·ₕ_
  RawRing.- (asRawRing n) =  -ₕ

Variable : (n : ℕ) (R : RawRing {ℓ}) (k : Fin n) → IteratedHornerForms R n
Variable n R k = IteratedHornerOperations.X R n k

Constant : (n : ℕ) (R : RawRing {ℓ}) (r : ⟨ R ⟩) → IteratedHornerForms R n
Constant ℕ.zero R r = const r
Constant (ℕ.suc n) R r = IteratedHornerOperations.0ₕ R ·X+ Constant n R r

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.Nat

postulate Pos : Set

data FVec : (n : Nat) → Set₁ where
  FNil  : FVec 0
  FCons : ∀ {n} → (Pos → Set) → FVec (suc n)

pre : ∀ {m n} → FVec m → FVec (suc n) → Pos → Set
pre FNil      (FCons x) = x
pre (FCons x) _         = x

data proofAG : ∀ {n} → FVec n → Set where
  []AG : proofAG FNil

postulate
  preAG : ∀ m n (v : FVec m) (v' : FVec (suc n)) →
            proofAG v → proofAG v' → ∀ p → pre v v' p
  m n : Nat
  v  : FVec m
  v' : FVec (suc n)
  p  : Pos

preAG₁ : pre v v' p
preAG₁ = preAG 0 n FNil _ []AG {!!} p
  -- Refine gives internal error instead of 'Cannot refine' or
  -- 'No introduction forms found'.

postulate Constrain : (A B : Set) → (A → B) → Set
syntax Constrain A B (λ x → y) = x ∈ A => y ∈ B

preAG₂ : (let X : FVec (suc n)
              X = _) →
         x ∈ pre FNil X p => x ∈ pre v v' p →
         proofAG X → Set
preAG₂ _ p = {!p!}
  -- Splitting on p causes the same internal error.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
open import Type hiding (★)
open import Function
open import Relation.Binary.PropositionalEquality

open import Explore.Core
open import Explore.Properties

-- Explore ℓ is not an endo functor because of universe levels
module Explore.Monad {a} ℓ where

M = Explore {a} ℓ

module _ {A : ★ a} where
    return : A → M A
    return = point-explore

    mzero : M A
    mzero = empty-explore

    mplus : M A → M A → M A
    mplus = merge-explore

    module _ {p} where
        return-ind : ∀ x → ExploreInd p (return x)
        return-ind = point-explore-ind

        mzero-ind : ExploreInd p mzero
        mzero-ind = empty-explore-ind

        mplus-ind : ∀ {e₀ e₁ : M A}
                    → ExploreInd p e₀ → ExploreInd p e₁
                    → ExploreInd p (merge-explore e₀ e₁)
        mplus-ind Pe₀ Pe₁ P Pε _P∙_ Pf = (Pe₀ P Pε _P∙_ Pf) P∙ (Pe₁ P Pε _P∙_ Pf)

module _ {A B : ★ a} where

    infixl 1 _>>=_ _>>=-ind_
    _>>=_ : M A → (A → M B) → M B
    (expᴬ >>= expᴮ) ε _∙_ f = expᴬ ε _∙_ λ x → expᴮ x ε _∙_ f

    _>>=-ind_ : ∀ {p}
                  {expᴬ : M A} → ExploreInd p expᴬ →
                  {expᴮ : A → M B} → (∀ x → ExploreInd p (expᴮ x))
               → ExploreInd p (expᴬ >>= expᴮ)
    _>>=-ind_ {expᴬ} Pᴬ {expᴮ} Pᴮ P Pz _P∙_ Pf
      = Pᴬ (λ e → P (e >>= expᴮ)) Pz _P∙_ λ x → Pᴮ x P Pz _P∙_ Pf

    map : (A → B) → M A → M B
    map f e = e >>= return ∘ f

    map-ind : ∀ {p} (f : A → B) {expᴬ : M A} → ExploreInd p expᴬ → ExploreInd p (map f expᴬ)
    map-ind f Pᴬ = Pᴬ >>=-ind return-ind ∘ f

    private
        {- This law is for free: map f e = e >>= return ∘ f -}
        map' : (A → B) → M A → M B
        map' f exp ε _∙_ g = exp ε _∙_ (g ∘ f)

        map'≡map : map' ≡ map
        map'≡map = refl

-- universe issues...
-- join : M (M A) → M A

module _ {A B C : ★ a} (m : M A) (f : A → M B) (g : B → M C) where
    infix 0 _≡e_
    _≡e_ = λ {A} → _≡_ {A = M A}

    left-identity : f ≡ (λ x → return x >>= f)
    left-identity = refl

    right-identity : m ≡e m >>= return
    right-identity = refl

    associativity : m >>= (λ x → f x >>= g) ≡e (m >>= f) >>= g
    associativity = refl

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
-- Occurs when different mixfix operators use similar names.
module Issue147a where

postulate
  X  : Set
  f  : X -> X
  f_ : X -> X

bad : X -> X
bad x = f x


text:
module ExtendedLambdaCase where

data Bool : Set where
  true false : Bool

data Void : Set where

foo : Bool -> Bool -> Bool -> Bool
foo = λ { x → λ { y z → {!!} } }

module parameterised {A : Set}(B : A -> Set) where

  data Bar : (Bool -> Bool) -> Set where
    baz : (t : Void) -> Bar λ { x → {!!} }

  -- with hidden argument
  data Bar' : (Bool -> Bool) -> Set where
    baz' : {t : Void} -> Bar' λ { x' → {!!} }

baz : Bool -> {w : Bool} -> Bool
baz = λ { z {w} → {!!} }

max_stars_repo_name: dagit/agda

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


text:
module Oscar.Data.Term.Substitution.Core {𝔣} (FunctionName : Set 𝔣) where

open import Oscar.Data.Term.Core FunctionName
open import Oscar.Data.Term.Substitution.Core.bootstrap FunctionName public hiding (_◃Term_; _◃VecTerm_)
open import Oscar.Data.Nat.Core
open import Oscar.Data.Fin.Core
open import Oscar.Data.Vec.Core
open import Oscar.Data.Equality.Core
open import Oscar.Data.Product.Core
open import Oscar.Function
open import Oscar.Level

⊸-Property : {ℓ : Level} → ℕ → Set (lsuc ℓ ⊔ 𝔣)
⊸-Property {ℓ} m = ∀ {n} → m ⊸ n → Set ℓ

_≐_ : {m n : ℕ} → m ⊸ n → m ⊸ n → Set 𝔣
f ≐ g = ∀ x → f x ≡ g x

⊸-Extensional : {ℓ : Level} {m : ℕ} → ⊸-Property {ℓ} m → Set (ℓ ⊔ 𝔣)
⊸-Extensional P = ∀ {m f g} → f ≐ g → P {m} f → P g

⊸-ExtentionalProperty : {ℓ : Level} → ℕ → Set (lsuc ℓ ⊔ 𝔣)
⊸-ExtentionalProperty {ℓ} m = Σ (⊸-Property {ℓ} m) ⊸-Extensional


text:
module Impure.LFRef.Readme where

open import Impure.LFRef.Syntax
open import Impure.LFRef.Welltyped
open import Impure.LFRef.Eval
open import Impure.LFRef.Properties.Soundness
open import Impure.LFRef.Properties.Confluence


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Union of two binary relations
------------------------------------------------------------------------

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

module Relation.Binary.Construct.Union where

open import Data.Product
open import Data.Sum.Base as Sum
open import Function using (_∘_)
open import Level using (Level; _⊔_)
open import Relation.Binary
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Sum using (_⊎-dec_)

private
  variable
    a b ℓ ℓ₁ ℓ₂ ℓ₃ : Level
    A : Set a
    B : Set b

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

_∪_ : ∀ {A : Set a} {B : Set b} →
      REL A B ℓ₁ → REL A B ℓ₂ → REL A B (ℓ₁ ⊔ ℓ₂)
L ∪ R = λ i j → L i j ⊎ R i j

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

module _ (L : Rel A ℓ) (R : Rel A ℓ) where

  reflexive : Reflexive L ⊎ Reflexive R → Reflexive (L ∪ R)
  reflexive (inj₁ L-refl) = inj₁ L-refl
  reflexive (inj₂ R-refl) = inj₂ R-refl

  total : Total L ⊎ Total R → Total (L ∪ R)
  total (inj₁ L-total) x y = [ inj₁ ∘ inj₁ , inj₂ ∘ inj₁ ] (L-total x y)
  total (inj₂ R-total) x y = [ inj₁ ∘ inj₂ , inj₂ ∘ inj₂ ] (R-total x y)

  min : ∀ {⊤} → Minimum L ⊤ ⊎ Minimum R ⊤ → Minimum (L ∪ R) ⊤
  min = [ inj₁ ∘_ , inj₂ ∘_ ]

  max : ∀ {⊥} → Maximum L ⊥ ⊎ Maximum R ⊥ → Maximum (L ∪ R) ⊥
  max = [ inj₁ ∘_ , inj₂ ∘_ ]

module _ {L : Rel A ℓ} {R : Rel A ℓ} where

  symmetric : Symmetric L → Symmetric R → Symmetric (L ∪ R)
  symmetric L-sym R-sym = [ inj₁ ∘ L-sym , inj₂ ∘ R-sym ]

  respects : ∀ {p} {P : A → Set p} →
             P Respects L → P Respects R → P Respects (L ∪ R)
  respects resp-L resp-R = [ resp-L , resp-R ]

module _ {≈ : Rel A ℓ₁} (L : REL A B ℓ₂) (R : REL A B ℓ₃) where

  respˡ : L Respectsˡ ≈ → R Respectsˡ ≈ → (L ∪ R) Respectsˡ ≈
  respˡ Lˡ Rˡ x≈y = Sum.map (Lˡ x≈y) (Rˡ x≈y)

module _ {≈ : Rel B ℓ₁} (L : REL A B ℓ₂) (R : REL A B ℓ₃) where

  respʳ : L Respectsʳ ≈ → R Respectsʳ ≈ → (L ∪ R) Respectsʳ ≈
  respʳ Lʳ Rʳ x≈y = Sum.map (Lʳ x≈y) (Rʳ x≈y)

module _ {≈ : Rel A ℓ₁} {L : Rel A ℓ₂} {R : Rel A ℓ₃} where

  resp₂ : L Respects₂ ≈ → R Respects₂ ≈ → (L ∪ R) Respects₂ ≈
  resp₂ (Lʳ , Lˡ) (Rʳ , Rˡ) = respʳ L R Lʳ Rʳ , respˡ L R Lˡ Rˡ

module _ (≈ : REL A B ℓ₁) (L : REL A B ℓ₂) (R : REL A B ℓ₃) where

  implies : (≈ ⇒ L) ⊎ (≈ ⇒ R) → ≈ ⇒ (L ∪ R)
  implies = [ inj₁ ∘_ , inj₂ ∘_ ]

  irreflexive : Irreflexive ≈ L → Irreflexive ≈ R → Irreflexive ≈ (L ∪ R)
  irreflexive L-irrefl R-irrefl x≈y = [ L-irrefl x≈y , R-irrefl x≈y ]

module _ {L : REL A B ℓ₁} {R : REL A B ℓ₂} where

  decidable : Decidable L → Decidable R → Decidable (L ∪ R)
  decidable L? R? x y = L? x y ⊎-dec R? x y


text:
-- We define the localisation of a commutative ring
-- at a multiplicatively closed subset and show that it
-- has a commutative ring structure.

{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommRing.Localisation.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.Transport
open import Cubical.Functions.FunExtEquiv

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Bool
open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_
                                      ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc
                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm)
open import Cubical.Data.Vec
open import Cubical.Data.Sigma.Base
open import Cubical.Data.Sigma.Properties
open import Cubical.Data.FinData
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.RingSolver.ReflectionSolving

open import Cubical.HITs.SetQuotients as SQ
open import Cubical.HITs.PropositionalTruncation as PT

open Iso

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

-- A multiplicatively closed subset is assumed to contain 1
record isMultClosedSubset (R' : CommRing ℓ) (S' : ℙ (fst R')) : Type ℓ where
 constructor
   multclosedsubset
 field
   containsOne : (R' .snd .CommRingStr.1r) ∈ S'
   multClosed : ∀ {s t} → s ∈ S' → t ∈ S' → ((snd R') .CommRingStr._·_ s t) ∈ S'

module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultClosedSubset R' S') where
 open isMultClosedSubset
 private R = fst R'
 open CommRingStr (snd R')
 open RingTheory (CommRing→Ring R')
 open CommRingTheory R'

 S = Σ[ s ∈ R ] (s ∈ S')

 -- We define the localisation of R by S by quotienting by the following relation:
 _≈_ : R × S → R × S → Type ℓ
 (r₁ , s₁) ≈ (r₂ , s₂) = Σ[ s ∈ S ] (fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁)

 S⁻¹R = (R × S) / _≈_

 -- now define addition for S⁻¹R
 open BinaryRelation

 locRefl : isRefl _≈_
 locRefl _ = (1r , SMultClosedSubset .containsOne) , refl

 locSym : isSym _≈_
 locSym (r , s , s∈S') (r' , s' , s'∈S') (u , p) = u , sym p

 locTrans : isTrans _≈_
 locTrans (r , s , s∈S') (r' , s' , s'∈S') (r'' , s'' , s''∈S') ((u , u∈S') , p) ((v , v∈S') , q) =
   ((u · v · s') , SMultClosedSubset .multClosed (SMultClosedSubset .multClosed u∈S' v∈S') s'∈S')
   , path
  where
  eq1 : (r s r' s' r'' s'' u v : R) → u · v · s' · r · s'' ≡ u · r · s' · v · s''
  eq1 = solve R'

  eq2 : (r s r' s' r'' s'' u v : R) → u · r' · s · v · s'' ≡ u · s · (v · r' · s'')
  eq2 = solve R'

  eq3 : (r s r' s' r'' s'' u v : R) → u · s · (v · r'' · s') ≡ u · v · s' · r'' · s
  eq3 = solve R'

  path : u · v · s' · r · s'' ≡ u · v · s' · r'' · s
  path = u · v · s' · r · s''   ≡⟨ eq1 r s r' s' r'' s'' u v ⟩ -- not just ≡⟨ solve R' ⟩
         u · r · s' · v · s''   ≡⟨ cong (λ x → x · v · s'') p ⟩
         u · r' · s · v · s''   ≡⟨ eq2 r s r' s' r'' s'' u v ⟩
         u · s · (v · r' · s'') ≡⟨ cong (u · s ·_) q ⟩
         u · s · (v · r'' · s') ≡⟨ eq3 r s r' s' r'' s'' u v ⟩
         u · v · s' · r'' · s   ∎

 locIsEquivRel : isEquivRel _≈_
 isEquivRel.reflexive locIsEquivRel = locRefl
 isEquivRel.symmetric locIsEquivRel = locSym
 isEquivRel.transitive locIsEquivRel = locTrans

 _+ₗ_ : S⁻¹R → S⁻¹R → S⁻¹R
 _+ₗ_ = setQuotSymmBinOp locRefl locTrans _+ₚ_
         (λ a b → subst (λ x → (a +ₚ b) ≈ x) (+ₚ-symm a b) (locRefl (a +ₚ b))) θ
  where
  _+ₚ_ : R × S → R × S → R × S
  (r₁ , s₁ , s₁∈S) +ₚ (r₂ , s₂ , s₂∈S) =
                      (r₁ · s₂ + r₂ · s₁) , (s₁ · s₂) , SMultClosedSubset .multClosed s₁∈S s₂∈S

  +ₚ-symm : (a b : R × S) → (a +ₚ b) ≡ (b +ₚ a)
  +ₚ-symm (r₁ , s₁ , s₁∈S) (r₂ , s₂ , s₂∈S) =
          ΣPathP (+Comm _ _ , Σ≡Prop (λ x → S' x .snd) (·-comm _ _))

  θ : (a a' b : R × S) → a ≈ a' → (a +ₚ b) ≈ (a' +ₚ b)
  θ (r₁ , s₁ , s₁∈S) (r'₁ , s'₁ , s'₁∈S) (r₂ , s₂ , s₂∈S) ((s , s∈S) , p) = (s , s∈S) , path
    where
    eq1 : (r₁ s₁ r'₁ s'₁ s'₁ r₂ s₂ s : R)
        → s · (r₁ · s₂ + r₂ · s₁) · (s'₁ · s₂) ≡ s · r₁ · s'₁ · s₂ · s₂ + s · r₂ · s₁ · s'₁ · s₂
    eq1 = solve R'

    eq2 : (r₁ s₁ r'₁ s'₁ s'₁ r₂ s₂ s : R)
        → s · r'₁ · s₁ · s₂ · s₂ + s · r₂ · s₁ · s'₁ · s₂ ≡ s · (r'₁ · s₂ + r₂ · s'₁) · (s₁ · s₂)
    eq2 = solve R'

    path : s · (r₁ · s₂ + r₂ · s₁) · (s'₁ · s₂) ≡ s · (r'₁ · s₂ + r₂ · s'₁) · (s₁ · s₂)
    path = s · (r₁ · s₂ + r₂ · s₁) · (s'₁ · s₂)

         ≡⟨ eq1 r₁ s₁ r'₁ s'₁ s'₁ r₂ s₂ s ⟩

           s · r₁ · s'₁ · s₂ · s₂ + s · r₂ · s₁ · s'₁ · s₂

         ≡⟨ cong (λ x → x · s₂ · s₂ + s · r₂ · s₁ · s'₁ · s₂) p ⟩

           s · r'₁ · s₁ · s₂ · s₂ + s · r₂ · s₁ · s'₁ · s₂

         ≡⟨ eq2 r₁ s₁ r'₁ s'₁ s'₁ r₂ s₂ s ⟩

           s · (r'₁ · s₂ + r₂ · s'₁) · (s₁ · s₂) ∎

 -- check group-laws for addition
 +ₗ-assoc : (x y z : S⁻¹R) → x +ₗ (y +ₗ z) ≡ (x +ₗ y) +ₗ z
 +ₗ-assoc = SQ.elimProp3 (λ _ _ _ → squash/ _ _) +ₗ-assoc[]
  where
  +ₗ-assoc[] : (a b c : R × S) → [ a ] +ₗ ([ b ] +ₗ [ c ]) ≡ ([ a ] +ₗ [ b ]) +ₗ [ c ]
  +ₗ-assoc[] (r , s , s∈S) (r' , s' , s'∈S) (r'' , s'' , s''∈S) =
     cong [_] (ΣPathP ((path r s r' s' r'' s'') , Σ≡Prop (λ x → ∈-isProp S' x) (·Assoc _ _ _)))
     where
     path : (r s r' s' r'' s'' : R)
          → r · (s' · s'') + (r' · s'' + r'' · s') · s ≡ (r · s' + r' · s) · s'' + r'' · (s · s')
     path = solve R'

 0ₗ : S⁻¹R
 0ₗ = [ 0r , 1r , SMultClosedSubset .containsOne ]

 +ₗ-rid : (x : S⁻¹R) → x +ₗ 0ₗ ≡ x
 +ₗ-rid = SQ.elimProp (λ _ → squash/ _ _) +ₗ-rid[]
  where
  +ₗ-rid[] : (a : R × S) → [ a ] +ₗ 0ₗ ≡ [ a ]
  +ₗ-rid[] (r , s , s∈S) = path
   where
   eq1 : (r s : R) → r · 1r + 0r · s ≡ r
   eq1 = solve R'

   path : [ r · 1r + 0r · s , s · 1r , SMultClosedSubset .multClosed s∈S
                                      (SMultClosedSubset .containsOne) ]
        ≡ [ r , s , s∈S ]
   path = cong [_] (ΣPathP (eq1 r s , Σ≡Prop (λ x → ∈-isProp S' x) (·Rid _)))

 -ₗ_ : S⁻¹R → S⁻¹R
 -ₗ_ = SQ.rec squash/ -ₗ[] -ₗWellDef
  where
  -ₗ[] : R × S → S⁻¹R
  -ₗ[] (r , s) = [ - r , s ]

  -ₗWellDef : (a b : R × S) → a ≈ b → -ₗ[] a ≡ -ₗ[] b
  -ₗWellDef (r , s , _) (r' , s' , _) ((u , u∈S) , p) = eq/ _ _ ((u , u∈S) , path)
   where
   eq1 : (u r s' : R) → u · - r · s' ≡ - (u · r · s')
   eq1 = solve R'

   eq2 : (u r' s : R) → - (u · r' · s) ≡ u · - r' · s
   eq2 = solve R'

   path : u · - r · s' ≡ u · - r' · s
   path = eq1 u r s' ∙∙ cong -_ p ∙∙ eq2 u r' s

 +ₗ-rinv : (x : S⁻¹R) → x +ₗ (-ₗ x) ≡ 0ₗ
 +ₗ-rinv = SQ.elimProp (λ _ → squash/ _ _) +ₗ-rinv[]
  where
  +ₗ-rinv[] : (a : R × S) → ([ a ] +ₗ (-ₗ [ a ])) ≡ 0ₗ
  +ₗ-rinv[] (r , s , s∈S) = eq/ _ _ ((1r , SMultClosedSubset .containsOne) , path r s)
   where
   path : (r s : R) → 1r · (r · s + - r · s) · 1r ≡ 1r · 0r · (s · s)
   path = solve R'

 +ₗ-comm : (x y : S⁻¹R) → x +ₗ y ≡ y +ₗ x
 +ₗ-comm = SQ.elimProp2 (λ _ _ → squash/ _ _) +ₗ-comm[]
  where
  +ₗ-comm[] : (a b : R × S) → ([ a ] +ₗ [ b ]) ≡ ([ b ] +ₗ [ a ])
  +ₗ-comm[] (r , s , s∈S) (r' , s' , s'∈S) =
            cong [_] (ΣPathP ((+Comm _ _) , Σ≡Prop (λ x → ∈-isProp S' x) (·-comm _ _)))

 -- Now for multiplication
 _·ₗ_ : S⁻¹R → S⁻¹R → S⁻¹R
 _·ₗ_ = setQuotSymmBinOp locRefl locTrans _·ₚ_
         (λ a b → subst (λ x → (a ·ₚ b) ≈ x) (·ₚ-symm a b) (locRefl (a ·ₚ b))) θ
  where
  _·ₚ_ : R × S → R × S → R × S
  (r₁ , s₁ , s₁∈S) ·ₚ (r₂ , s₂ , s₂∈S) =
                      (r₁ · r₂) , ((s₁ · s₂) , SMultClosedSubset .multClosed s₁∈S s₂∈S)

  ·ₚ-symm : (a b : R × S) → (a ·ₚ b) ≡ (b ·ₚ a)
  ·ₚ-symm (r₁ , s₁ , s₁∈S) (r₂ , s₂ , s₂∈S) =
          ΣPathP (·-comm _ _ , Σ≡Prop (λ x → S' x .snd) (·-comm _ _))

  θ : (a a' b : R × S) → a ≈ a' → (a ·ₚ b) ≈ (a' ·ₚ b)
  θ (r₁ , s₁ , s₁∈S) (r'₁ , s'₁ , s'₁∈S) (r₂ , s₂ , s₂∈S) ((s , s∈S) , p) = (s , s∈S) , path
   where
   eq1 : (r₁ s₁ r'₁ s'₁ r₂ s₂ s : R)
       → s · (r₁ · r₂) · (s'₁ · s₂) ≡ s · r₁ · s'₁ · r₂ · s₂
   eq1 = solve R'

   eq2 : (r₁ s₁ r'₁ s'₁ r₂ s₂ s : R)
       → s · r'₁ · s₁ · r₂ · s₂ ≡ s · (r'₁ · r₂) · (s₁ · s₂)
   eq2 = solve R'

   path : s · (r₁ · r₂) · (s'₁ · s₂) ≡ s · (r'₁ · r₂) · (s₁ · s₂)
   path = eq1 r₁ s₁ r'₁ s'₁ r₂ s₂ s ∙∙ cong (λ x → x · r₂ · s₂) p ∙∙ eq2 r₁ s₁ r'₁ s'₁ r₂ s₂ s

 -- checking laws for multiplication
 1ₗ : S⁻¹R
 1ₗ = [ 1r , 1r , SMultClosedSubset .containsOne ]

 ·ₗ-assoc : (x y z : S⁻¹R) → x ·ₗ (y ·ₗ z) ≡ (x ·ₗ y) ·ₗ z
 ·ₗ-assoc = SQ.elimProp3 (λ _ _ _ → squash/ _ _) ·ₗ-assoc[]
   where
   ·ₗ-assoc[] : (a b c : R × S) → [ a ] ·ₗ ([ b ] ·ₗ [ c ]) ≡ ([ a ] ·ₗ [ b ]) ·ₗ [ c ]
   ·ₗ-assoc[] (r , s , s∈S) (r' , s' , s'∈S) (r'' , s'' , s''∈S) =
              cong [_] (ΣPathP ((·Assoc _ _ _) , Σ≡Prop (λ x → ∈-isProp S' x) (·Assoc _ _ _)))

 ·ₗ-rid : (x : S⁻¹R) → x ·ₗ 1ₗ ≡ x
 ·ₗ-rid = SQ.elimProp (λ _ → squash/ _ _) ·ₗ-rid[]
   where
   ·ₗ-rid[] : (a : R × S) → ([ a ] ·ₗ 1ₗ) ≡ [ a ]
   ·ₗ-rid[] (r , s , s∈S) = cong [_] (ΣPathP ((·Rid _) , Σ≡Prop (λ x → ∈-isProp S' x) (·Rid _)))

 ·ₗ-rdist-+ₗ : (x y z : S⁻¹R) → x ·ₗ (y +ₗ z) ≡ (x ·ₗ y) +ₗ (x ·ₗ z)
 ·ₗ-rdist-+ₗ = SQ.elimProp3 (λ _ _ _ → squash/ _ _) ·ₗ-rdist-+ₗ[]
   where
   ·ₗ-rdist-+ₗ[] : (a b c : R × S) → [ a ] ·ₗ ([ b ] +ₗ [ c ]) ≡ ([ a ] ·ₗ [ b ]) +ₗ ([ a ] ·ₗ [ c ])
   ·ₗ-rdist-+ₗ[] (r , s , s∈S) (r' , s' , s'∈S) (r'' , s'' , s''∈S) =
      eq/ _ _ ((1r , (SMultClosedSubset .containsOne)) , path r s r' s' r'' s'')
      where
      -- could be shortened even further
      path : (r s r' s' r'' s'' : R)
           → 1r · (r · (r' · s'' + r'' · s')) · (s · s' · (s · s''))
           ≡ 1r · (r · r' · (s · s'') + r · r'' · (s · s')) · (s · (s' · s''))
      path = solve R'

 ·ₗ-comm : (x y : S⁻¹R) → x ·ₗ y ≡ y ·ₗ x
 ·ₗ-comm = SQ.elimProp2 (λ _ _ → squash/ _ _) ·ₗ-comm[]
   where
   ·ₗ-comm[] : (a b : R × S) → [ a ] ·ₗ [ b ] ≡ [ b ] ·ₗ [ a ]
   ·ₗ-comm[] (r , s , s∈S) (r' , s' , s'∈S) =
             cong [_] (ΣPathP ((·-comm _ _) , Σ≡Prop (λ x → ∈-isProp S' x) (·-comm _ _)))

 -- Commutative ring structure on S⁻¹R
 S⁻¹RAsCommRing : CommRing ℓ
 S⁻¹RAsCommRing = S⁻¹R , S⁻¹RCommRingStr
  where
  open CommRingStr
  S⁻¹RCommRingStr : CommRingStr S⁻¹R
  0r S⁻¹RCommRingStr = 0ₗ
  1r S⁻¹RCommRingStr = 1ₗ
  _+_ S⁻¹RCommRingStr = _+ₗ_
  _·_ S⁻¹RCommRingStr = _·ₗ_
  - S⁻¹RCommRingStr = -ₗ_
  isCommRing S⁻¹RCommRingStr = makeIsCommRing squash/ +ₗ-assoc +ₗ-rid +ₗ-rinv +ₗ-comm
                                                      ·ₗ-assoc ·ₗ-rid ·ₗ-rdist-+ₗ ·ₗ-comm

max_stars_repo_name: dolio/cubical

max_issues_repo_name: dolio/cubical

max_forks_repo_name: dolio/cubical


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Polynomials.UnivariateHIT.Base where

open import Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyHIT public

{-

The Univariate Functional Polynomials over a CommRing A is a CommRing.
The base type is define using an HIT.
This definition enables to defined a direct sum indexed by ℕ.
Thus base type and the AbGroup part of the CommRing is define an instance
of the more general Direct Sum one which can be found here :
-}

open import Cubical.Algebra.DirectSum.DirectSumHIT.Base

{-

On this definition of the Direct Sum, it is possible to raise a Graded Ring structure.
Then complete it to be a CommRing. Those version of the polynomials are hence
a instance of this graded ring structure.

see : for the details of the constructions

-}

open import Cubical.Algebra.GradedRing.DirectSumHIT

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2019-11-07, issue #4169 report and testcase by nad.
-- Extra coercions needed when erased versions of functions are used.

open import Agda.Builtin.Unit
open import Common.IO

data D : Set where
  c : D

F : D → Set → Set
F c A = A → A

f : (d : D) (A : Set) → F d A → A → A    -- 14
f c A g = g

f′ : (d : D) (A : Set) (P : Set → Set)   -- 30
     (g : (A : Set) → F d (P A))
   → P A → P A
f′ d A P g = f d (P A) (g A)

module _ (id : (A : Set) → (A → A) → A → A) (G : Set → Set) where

  postulate
    g : (A : Set) → G A → G A

  g′ : (A : Set) → G A → G A
  g′ A s = g A s

  g″ : (A : Set) → G A → G A
  g″ A = id (G A) (f′ c A G g′)

main : IO ⊤
main = return _

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- H-levels
------------------------------------------------------------------------

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

-- Partly based on Voevodsky's work on so-called univalent
-- foundations.

open import Equality

module H-level
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open Derived-definitions-and-properties eq
open import Logical-equivalence hiding (id; _∘_)
open import Nat eq
open import Prelude
open import Surjection eq hiding (id; _∘_)

private
  variable
    a ℓ : Level
    m n : ℕ
    A B : Type a

------------------------------------------------------------------------
-- H-levels

-- H-levels ("homotopy levels").

H-level : ℕ → Type ℓ → Type ℓ
H-level zero          A = Contractible A
H-level (suc zero)    A = Is-proposition A
H-level (suc (suc n)) A = {x y : A} → H-level (suc n) (x ≡ y)

private

  -- Note that H-level 2 is a synonym for Is-set.

  H-level-2≡Is-set : H-level 2 A ≡ Is-set A
  H-level-2≡Is-set = refl _

-- For-iterated-equality n P A means that P holds for (equalities
-- over)^n A.

For-iterated-equality : ℕ → (Type ℓ → Type ℓ) → (Type ℓ → Type ℓ)
For-iterated-equality zero    P A = P A
For-iterated-equality (suc n) P A =
  (x y : A) → For-iterated-equality n P (x ≡ y)

-- An alternative definition of h-levels.
--
-- In some cases this definition, with only two cases, is easier to
-- use. In other cases the definition above, which is less complicated
-- for positive h-levels, is easier to use.

H-level′ : ℕ → Type ℓ → Type ℓ
H-level′ = flip For-iterated-equality Contractible

-- Propositions are propositional types.

Proposition : (ℓ : Level) → Type (lsuc ℓ)
Proposition _ = ∃ Is-proposition

-- Types that are sets.

Set : (ℓ : Level) → Type (lsuc ℓ)
Set _ = ∃ Is-set

-- The underlying type.

⌞_⌟ : Set ℓ → Type ℓ
⌞ A ⌟ = proj₁ A

------------------------------------------------------------------------
-- General properties

-- H-level′ is upwards closed in its first argument.

mono₁′ : ∀ n → H-level′ n A → H-level′ (1 + n) A
mono₁′         (suc n) h x y = mono₁′ n (h x y)
mono₁′ {A = A} zero    h x y = trivial x y , irr
  where
  trivial : (x y : A) → x ≡ y
  trivial x y =
    x        ≡⟨ sym $ proj₂ h x ⟩
    proj₁ h  ≡⟨ proj₂ h y ⟩∎
    y        ∎

  irr : (x≡y : x ≡ y) → trivial x y ≡ x≡y
  irr = elim (λ {x y} x≡y → trivial x y ≡ x≡y)
             (λ x → trans-symˡ (proj₂ h x))

-- H-level and H-level′ are pointwise logically equivalent.

H-level⇔H-level′ : H-level n A ⇔ H-level′ n A
H-level⇔H-level′ = record { to = to _; from = from _ }
  where
  to : ∀ n → H-level n A → H-level′ n A
  to zero          h = h
  to (suc zero)    h = λ x → mono₁′ 0 (x , h x) x
  to (suc (suc n)) h = λ x y → to (suc n) h

  from : ∀ n → H-level′ n A → H-level n A
  from zero          h = h
  from (suc zero)    h x y = proj₁ (h x y)
  from (suc (suc n)) h {x = x} {y = y} = from (suc n) (h x y)

-- If A has h-level 1 + n, then the types of equality proofs between
-- elements of type A have h-level n.

+⇒≡ : {x y : A} → H-level (suc n) A → H-level n (x ≡ y)
+⇒≡ h = _⇔_.from H-level⇔H-level′ $ _⇔_.to H-level⇔H-level′ h _ _

-- H-level is upwards closed in its first argument.

mono₁ : ∀ n → H-level n A → H-level (1 + n) A
mono₁ n =
  _⇔_.from H-level⇔H-level′ ∘
  mono₁′ n ∘
  _⇔_.to H-level⇔H-level′

abstract

  mono : m ≤ n → H-level m A → H-level n A
  mono (≤-refl′ eq)     = subst (λ n → H-level n _) eq
  mono (≤-step′ m≤n eq) =
    subst (λ n → H-level n _) eq ∘
    mono₁ _ ∘
    mono m≤n

  -- If A has h-level n, then the types of equality proofs between
  -- elements of type A also have h-level n.

  ⇒≡ : {x y : A} → ∀ n → H-level n A → H-level n (x ≡ y)
  ⇒≡ _ = +⇒≡ ∘ mono₁ _

  -- If something is contractible given the assumption that it is
  -- inhabited, then it is propositional.

  [inhabited⇒contractible]⇒propositional :
    (A → Contractible A) → Is-proposition A
  [inhabited⇒contractible]⇒propositional h x = mono₁ 0 (h x) x

  -- If something has h-level (1 + n) given the assumption that it is
  -- inhabited, then it has h-level (1 + n).

  [inhabited⇒+]⇒+ : ∀ n → (A → H-level (1 + n) A) → H-level (1 + n) A
  [inhabited⇒+]⇒+ n h =
    _⇔_.from H-level⇔H-level′ λ x → _⇔_.to H-level⇔H-level′ (h x) x

  -- An alternative characterisation of sets and higher h-levels.
  --
  -- This is Theorem 7.2.7 from the HoTT book.

  2+⇔∀1+≡ :
    ∀ n → H-level (2 + n) A ⇔ ((x : A) → H-level (1 + n) (x ≡ x))
  2+⇔∀1+≡ n = record
    { to   = λ h _ → h
    ; from = λ h → [inhabited⇒+]⇒+ _
                     (elim (λ {x y} _ → H-level (1 + n) (x ≡ y)) h)
    }

-- If a propositional type is inhabited, then it is contractible.

propositional⇒inhabited⇒contractible :
  Is-proposition A → A → Contractible A
propositional⇒inhabited⇒contractible p x = (x , p x)

-- H-level′ n respects (split) surjections.

respects-surjection′ :
  A ↠ B → ∀ n → H-level′ n A → H-level′ n B
respects-surjection′ A↠B zero (x , irr) = (to x , irr′)
  where
  open _↠_ A↠B

  irr′ : ∀ y → to x ≡ y
  irr′ = λ y →
    to x         ≡⟨ cong to (irr (from y)) ⟩
    to (from y)  ≡⟨ right-inverse-of y ⟩∎
    y            ∎

respects-surjection′ A↠B (suc n) h = λ x y →
  respects-surjection′ (↠-≡ A↠B) n (h (from x) (from y))
  where open _↠_ A↠B

-- H-level n respects (split) surjections.

respects-surjection :
  A ↠ B → ∀ n → H-level n A → H-level n B
respects-surjection A↠B n =
  _⇔_.from H-level⇔H-level′ ∘
  respects-surjection′ A↠B n ∘
  _⇔_.to H-level⇔H-level′

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- define ⋁ and ⋀ as the bigOps of a Ring when interpreted
-- as an additive/multiplicative monoid

{-# OPTIONS --safe #-}
module Cubical.Algebra.DistLattice.BigOps where

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

open import Cubical.Data.Sigma
open import Cubical.Data.Nat using (ℕ ; zero ; suc)
open import Cubical.Data.FinData
open import Cubical.Data.Bool

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Macro
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Monoid.BigOp
open import Cubical.Algebra.CommMonoid
open import Cubical.Algebra.Semilattice
open import Cubical.Algebra.Lattice
open import Cubical.Algebra.DistLattice
open import Cubical.Relation.Binary.Poset

private
  variable
    ℓ : Level

module KroneckerDelta (L' : DistLattice ℓ) where
 private
  L = fst L'
 open DistLatticeStr (snd L')

 δ : {n : ℕ} (i j : Fin n) → L
 δ i j = if i == j then 1l else 0l

module Join (L' : DistLattice ℓ) where
 private
  L = fst L'
 open DistLatticeStr (snd L')
 open MonoidBigOp (Semilattice→Monoid (Lattice→JoinSemilattice (DistLattice→Lattice L')))
 -- extra DistLattice→JoinMonoid?
 open LatticeTheory (DistLattice→Lattice L')
 open KroneckerDelta L'

 ⋁ = bigOp
 ⋁Ext = bigOpExt
 ⋁0l = bigOpε
 ⋁Last = bigOpLast

 ⋁Split : ∀ {n} → (V W : FinVec L n) → ⋁ (λ i → V i ∨l W i) ≡ ⋁ V ∨l ⋁ W
 ⋁Split = bigOpSplit ∨lComm

 ⋁Meetrdist : ∀ {n} → (x : L) → (V : FinVec L n)
                → x ∧l ⋁ V ≡ ⋁ λ i → x ∧l V i
 ⋁Meetrdist {n = zero}  x _ = 0lRightAnnihilates∧l x
 ⋁Meetrdist {n = suc n} x V =
   x ∧l (V zero ∨l ⋁ (V ∘ suc))              ≡⟨ ∧lLdist∨l _ _ _ ⟩ --Ldist and Rdist wrong way around?
   (x ∧l V zero) ∨l (x ∧l ⋁ (V ∘ suc))       ≡⟨ (λ i → (x ∧l V zero) ∨l ⋁Meetrdist x (V ∘ suc) i) ⟩
   (x ∧l V zero) ∨l ⋁ (λ i → x ∧l V (suc i)) ∎

 ⋁Meetldist : ∀ {n} → (x : L) → (V : FinVec L n)
                → (⋁ V) ∧l x ≡ ⋁ λ i → V i ∧l x
 ⋁Meetldist {n = zero}  x _ = 0lLeftAnnihilates∧l x
 ⋁Meetldist {n = suc n} x V =
   (V zero ∨l ⋁ (V ∘ suc)) ∧l x              ≡⟨ ∧lRdist∨l _ _ _ ⟩
   (V zero ∧l x) ∨l ((⋁ (V ∘ suc)) ∧l x)     ≡⟨ (λ i → (V zero ∧l x) ∨l ⋁Meetldist x (V ∘ suc) i) ⟩
   (V zero ∧l x) ∨l ⋁ (λ i → V (suc i) ∧l x) ∎

 ⋁Meetr0 : ∀ {n} → (V : FinVec L n) → ⋁ (λ i → V i ∧l 0l) ≡ 0l
 ⋁Meetr0 V = sym (⋁Meetldist 0l V) ∙ 0lRightAnnihilates∧l _

 ⋁Meet0r : ∀ {n} → (V : FinVec L n) → ⋁ (λ i → 0l ∧l V i) ≡ 0l
 ⋁Meet0r V = sym (⋁Meetrdist 0l V) ∙ 0lLeftAnnihilates∧l _

 ⋁Meetr1 : (n : ℕ) (V : FinVec L n) → (j : Fin n) → ⋁ (λ i → V i ∧l δ i j) ≡ V j
 ⋁Meetr1 (suc n) V zero = (λ k → ∧lRid (V zero) k ∨l ⋁Meetr0 (V ∘ suc) k) ∙ ∨lRid (V zero)
 ⋁Meetr1 (suc n) V (suc j) =
    (λ i → 0lRightAnnihilates∧l (V zero) i ∨l ⋁ (λ x → V (suc x) ∧l δ x j))
    ∙∙ ∨lLid _ ∙∙ ⋁Meetr1 n (V ∘ suc) j

 ⋁Meet1r : (n : ℕ) (V : FinVec L n) → (j : Fin n) → ⋁ (λ i → (δ j i) ∧l V i) ≡ V j
 ⋁Meet1r (suc n) V zero = (λ k → ∧lLid (V zero) k ∨l ⋁Meet0r (V ∘ suc) k) ∙ ∨lRid (V zero)
 ⋁Meet1r (suc n) V (suc j) =
   (λ i → 0lLeftAnnihilates∧l (V zero) i ∨l ⋁ (λ i → (δ j i) ∧l V (suc i)))
   ∙∙ ∨lLid _ ∙∙ ⋁Meet1r n (V ∘ suc) j

 -- inequalities of big joins
 open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice L'))
 open PosetReasoning IndPoset
 open PosetStr (IndPoset .snd) hiding (_≤_)

 ⋁IsMax : {n : ℕ} (U : FinVec L n) (x : L) → (∀ i → U i ≤ x) → ⋁ U ≤ x
 ⋁IsMax {n = zero} _ _ _ = ∨lLid _
 ⋁IsMax {n = suc n} U x U≤x =
   ⋁ U                   ≤⟨ is-refl _ ⟩
   U zero ∨l ⋁ (U ∘ suc) ≤⟨ ≤-∨LPres _ _ _ (⋁IsMax _ _ (U≤x ∘ suc)) ⟩
   U zero ∨l x            ≤⟨ ∨lIsMax _ _ _ (U≤x zero) (is-refl x) ⟩
   x ◾

 ≤-⋁Ext : {n : ℕ} (U W : FinVec L n) → (∀ i → U i ≤ W i) → ⋁ U ≤ ⋁ W
 ≤-⋁Ext {n = zero} U W U≤W = is-refl 0l
 ≤-⋁Ext {n = suc n} U W U≤W =
   ⋁ U                   ≤⟨ is-refl _ ⟩
   U zero ∨l ⋁ (U ∘ suc) ≤⟨ ≤-∨Pres _ _ _ _ (U≤W zero) (≤-⋁Ext _ _ (U≤W ∘ suc)) ⟩
   W zero ∨l ⋁ (W ∘ suc) ≤⟨ is-refl _ ⟩
   ⋁ W ◾

module Meet (L' : DistLattice ℓ) where
 private
  L = fst L'
 open DistLatticeStr (snd L')
 open MonoidBigOp (Semilattice→Monoid (Lattice→MeetSemilattice (DistLattice→Lattice L')))
 -- extra DistLattice→MeetMonoid?
 open LatticeTheory (DistLattice→Lattice L')
 open KroneckerDelta L'

 ⋀ = bigOp
 ⋀Ext = bigOpExt
 ⋀1l = bigOpε
 ⋀Last = bigOpLast

 ⋀Split : ∀ {n} → (V W : FinVec L n) → ⋀ (λ i → V i ∧l W i) ≡ ⋀ V ∧l ⋀ W
 ⋀Split = bigOpSplit ∧lComm

 ⋀Joinrdist : ∀ {n} → (x : L) → (V : FinVec L n)
                → x ∨l ⋀ V ≡ ⋀ λ i → x ∨l V i
 ⋀Joinrdist {n = zero}  x _ = 1lRightAnnihilates∨l x
 ⋀Joinrdist {n = suc n} x V =
   x ∨l (V zero ∧l ⋀ (V ∘ suc))              ≡⟨ ∨lLdist∧l _ _ _ ⟩ --Ldist and Rdist wrong way around?
   (x ∨l V zero) ∧l (x ∨l ⋀ (V ∘ suc))       ≡⟨ (λ i → (x ∨l V zero) ∧l ⋀Joinrdist x (V ∘ suc) i) ⟩
   (x ∨l V zero) ∧l ⋀ (λ i → x ∨l V (suc i)) ∎

 ⋀Joinldist : ∀ {n} → (x : L) → (V : FinVec L n)
                → (⋀ V) ∨l x ≡ ⋀ λ i → V i ∨l x
 ⋀Joinldist {n = zero}  x _ = 1lLeftAnnihilates∨l x
 ⋀Joinldist {n = suc n} x V =
   (V zero ∧l ⋀ (V ∘ suc)) ∨l x              ≡⟨ ∨lRdist∧l _ _ _ ⟩
   (V zero ∨l x) ∧l ((⋀ (V ∘ suc)) ∨l x)     ≡⟨ (λ i → (V zero ∨l x) ∧l ⋀Joinldist x (V ∘ suc) i) ⟩
   (V zero ∨l x) ∧l ⋀ (λ i → V (suc i) ∨l x) ∎

 ⋀Joinr1 : ∀ {n} → (V : FinVec L n) → ⋀ (λ i → V i ∨l 1l) ≡ 1l
 ⋀Joinr1 V = sym (⋀Joinldist 1l V) ∙ 1lRightAnnihilates∨l _

 ⋀Join1r : ∀ {n} → (V : FinVec L n) → ⋀ (λ i → 1l ∨l V i) ≡ 1l
 ⋀Join1r V = sym (⋀Joinrdist 1l V) ∙ 1lLeftAnnihilates∨l _


text:
module examplesPaperJFP.IOExampleConsole where

open import examplesPaperJFP.BasicIO hiding (main)
open import examplesPaperJFP.Console hiding (main)
open import examplesPaperJFP.NativeIOSafe
open import examplesPaperJFP.CatTerm

main : NativeIO Unit
main = translateIOConsole cat

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

module Cubical.Categories.Additive where

open import Cubical.Categories.Additive.Base public
open import Cubical.Categories.Additive.Properties public
open import Cubical.Categories.Additive.Quotient public


text:
{-
This second-order term syntax was created from the following second-order syntax description:

syntax CTLC | ΛC

type
  N   : 0-ary
  _↣_ : 2-ary | r30
  ¬_  : 1-ary | r30

term
  app    : α ↣ β  α  ->  β | _$_ l20
  lam    : α.β  ->  α ↣ β | ƛ_ r10
  throw  : α  ¬ α  ->  β
  callcc : ¬ α.α  ->  α

theory
  (ƛβ) b : α.β  a : α |> app (lam(x.b[x]), a) = b[a]
  (ƛη) f : α ↣ β      |> lam (x. app(f, x))   = f
-}

module CTLC.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import CTLC.Signature

private
  variable
    Γ Δ Π : Ctx
    α β : ΛCT
    𝔛 : Familyₛ

-- Inductive term declaration
module ΛC:Terms (𝔛 : Familyₛ) where

  data ΛC : Familyₛ where
    var  : ℐ ⇾̣ ΛC
    mvar : 𝔛 α Π → Sub ΛC Π Γ → ΛC α Γ

    _$_    : ΛC (α ↣ β) Γ → ΛC α Γ → ΛC β Γ
    ƛ_     : ΛC β (α ∙ Γ) → ΛC (α ↣ β) Γ
    throw  : ΛC α Γ → ΛC (¬ α) Γ → ΛC β Γ
    callcc : ΛC α ((¬ α) ∙ Γ) → ΛC α Γ

  infixl 20 _$_
  infixr 10 ƛ_

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  ΛCᵃ : MetaAlg ΛC
  ΛCᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (appₒ    ⋮ a , b) → _$_    a b
      (lamₒ    ⋮ a)     → ƛ_     a
      (throwₒ  ⋮ a , b) → throw  a b
      (callccₒ ⋮ a)     → callcc a
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module ΛCᵃ = MetaAlg ΛCᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : ΛC ⇾̣ 𝒜
    𝕊 : Sub ΛC Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞 (_$_    a b) = 𝑎𝑙𝑔 (appₒ    ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (ƛ_     a)   = 𝑎𝑙𝑔 (lamₒ    ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (throw  a b) = 𝑎𝑙𝑔 (throwₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (callcc a)   = 𝑎𝑙𝑔 (callccₒ ⋮ 𝕤𝕖𝕞 a)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ ΛCᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ ΛC α Γ) → 𝕤𝕖𝕞 (ΛCᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (appₒ    ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (lamₒ    ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (throwₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (callccₒ ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ ΛC ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : ΛC ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ ΛCᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : ΛC α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub ΛC Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! (_$_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (ƛ_ a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (throw a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (callcc a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
ΛC:Syn : Syntax
ΛC:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = ΛC:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open ΛC:Terms 𝔛 in record
    { ⊥ = ΛC ⋉ ΛCᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax ΛC:Syn public
open ΛC:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands ΛCᵃ public
open import SOAS.Metatheory ΛC:Syn public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

open import Cubical.Foundations.Prelude

open import Cubical.Data.FinData
open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Vec.Base

open import Cubical.Algebra.RingSolver.AlmostRing
open import Cubical.Algebra.RingSolver.NatAsAlmostRing
open import Cubical.Algebra.RingSolver.RingExpression
open import Cubical.Algebra.RingSolver.RawRing renaming (⟨_⟩ to ⟨_⟩ᵣ)
open import Cubical.Algebra.RingSolver.HornerForms
open import Cubical.Algebra.RingSolver.Solver

private
  variable
    ℓ : Level

module MultivariateSolving where
  open AlmostRing ℕAsAlmostRing
  ℕAsRawRing = AlmostRing→RawRing ℕAsAlmostRing
  open EqualityToNormalform ℕAsAlmostRing
  ℕ[X₀,X₁] = IteratedHornerOperations.asRawRing ℕAsRawRing 2

  X₀ : ⟨ ℕ[X₀,X₁] ⟩ᵣ
  X₀ = Variable 2 ℕAsRawRing (Fin.zero)

  X₁ : ⟨ ℕ[X₀,X₁] ⟩ᵣ
  X₁ = Variable 2 ℕAsRawRing (suc Fin.zero)

  Two : ⟨ ℕ[X₀,X₁] ⟩ᵣ
  Two = Constant 2 ℕAsRawRing 2

  _ : eval 2 X₀ (1 ∷ 0 ∷ []) ≡ 1
  _ = refl

  _ : eval 2 X₁ (0 ∷ 1 ∷ []) ≡ 1
  _ = refl

  X : Expr ℕ 3
  X = ∣ Fin.zero

  Y : Expr ℕ 3
  Y = ∣ (suc Fin.zero)

  Z : Expr ℕ 3
  Z = ∣ (suc (suc Fin.zero))

  {-
     'normalize' maps an expression to its Horner Normalform.
     Two expressions evaluating to the same ring element
     have the same Horner Normal form.
     This means equality of the represented ring elements
     can be checked by agda's unification (so refl is a proof)

   -}
  _ : normalize 3 ((K 2) ⊗ X) ≡
      normalize 3 (X ⊕ X)
  _ = refl

  _ : normalize 3 ((K 2) ⊗ X) ≡ normalize 3 (X ⊕ X)
  _ = refl

  _ : normalize 3 (((K 2) ⊗ X) ⊗ Y) ≡ normalize 3 (Y ⊗ (X ⊕ X))
  _ = refl

  _ : normalize 3 (Z ⊗ (((K 2) ⊗ X) ⊗ Y)) ≡ normalize 3 (Z ⊗ (Y ⊗ (X ⊕ X)))
  _ = refl

  {-
    The solver needs to produce an equality between
    actual ring elements. So we need a proof that
    those actual ring elements are equal to a normal form:
  -}
  _ : (x y z : ℕ) →
      eval 3 (normalize 3 ((K 2) ⊗ X ⊗ Y)) (x ∷ y ∷ z ∷ [])
      ≡ 2 · x · y
  _ = λ x y z → isEqualToNormalform 3 ((K 2) ⊗ X ⊗ Y) (x ∷ y ∷ z ∷ [])

  {-
    Now two of these proofs can be plugged together
    to solve an equation:
  -}
  open Eval ℕAsRawRing
  _ : (x y z : ℕ) → 3 + x + y · y ≡ y · y + x + 1 + 2
  _ = let
        lhs = (K 3) ⊕ X ⊕ (Y ⊗ Y)
        rhs = Y ⊗ Y ⊕ X ⊕ (K 1) ⊕ (K 2)
      in (λ x y z →
          ⟦ lhs ⟧ (x ∷ y ∷ z ∷ [])
        ≡⟨ sym (isEqualToNormalform 3 lhs (x ∷ y ∷ z ∷ [])) ⟩
          eval 3 (normalize 3 lhs) (x ∷ y ∷ z ∷ [])
        ≡⟨ refl ⟩
          eval 3 (normalize 3 rhs) (x ∷ y ∷ z ∷ [])
        ≡⟨ isEqualToNormalform 3 rhs (x ∷ y ∷ z ∷ []) ⟩
          ⟦ rhs ⟧ (x ∷ y ∷ z ∷ []) ∎)

  {-
    Parts of that can be automated easily:
  -}
  _ : (x y z : ℕ) → (x + y) · (x + y) ≡ x · x + 2 · x · y + y · y
  _ = λ x y z → let
              lhs = (X ⊕ Y) ⊗ (X ⊕ Y)
              rhs = X ⊗ X ⊕ (K 2) ⊗ X ⊗ Y ⊕ Y ⊗ Y
             in solve lhs rhs (x ∷ y ∷ z ∷ []) refl

  {-
    A bigger example
  -}
  _ : (x y z : ℕ) → (x + y) · (x + y) · (x + y) · (x + y)
                ≡ x · x · x · x + 4 · x · x · x · y + 6 · x · x · y · y
                  +  4 · x · y · y · y + y · y · y · y
  _ = λ x y z → let
              lhs = (X ⊕ Y) ⊗ (X ⊕ Y) ⊗ (X ⊕ Y) ⊗ (X ⊕ Y)
              rhs = X ⊗ X ⊗ X ⊗ X
                  ⊕ (K 4) ⊗ X ⊗ X ⊗ X ⊗ Y
                  ⊕ (K 6) ⊗ X ⊗ X ⊗ Y ⊗ Y
                  ⊕ (K 4) ⊗ X ⊗ Y ⊗ Y ⊗ Y
                  ⊕ Y ⊗ Y ⊗ Y ⊗ Y
             in solve lhs rhs (x ∷ y ∷ z ∷ []) refl
  {-
    this one cannot work so far:

  _ : (x y z : ℕ) → (x + y) · (x - y) ≡ (x · x - (y · y))
  _ = λ x y z → let
                lhs = (X ⊕ Y) ⊗ (X ⊕ (⊝ Y))
                rhs = (X ⊗ X) ⊕ (⊝ (Y ⊗ Y))
              in solve lhs rhs (x ∷ y ∷ z ∷ []) {!!}
  -}

module ExamplesForArbitraryRings (R : AlmostRing {ℓ}) where
  open AlmostRing R
  open EqualityToNormalform R

  X : Expr ⟨ R ⟩ 4
  X = ∣ Fin.zero

  Y : Expr ⟨ R ⟩ 4
  Y = ∣ (suc Fin.zero)

  A : Expr ⟨ R ⟩ 4
  A = ∣ (suc (suc Fin.zero))

  B : Expr ⟨ R ⟩ 4
  B = ∣ (suc (suc (suc Fin.zero)))

  _ : (x y a b : ⟨ R ⟩) → (x + y) + (a + b) ≡ (y + b) + (x + a)
  _ = λ x y a b → let
                lhs = (X ⊕ Y) ⊕ (A ⊕ B)
                rhs = (Y ⊕ B) ⊕ (X ⊕ A)
              in solve lhs rhs (x ∷ y ∷ a ∷ b ∷ []) refl

  _ : (x y a b : ⟨ R ⟩) → (x + y) · (x + y) ≡ x · x + x · y + x · y + y · y
  _ = λ x y a b →
              let
                lhs = (X ⊕ Y) ⊗ (X ⊕ Y)
                rhs = (X ⊗ X) ⊕ (X ⊗ Y) ⊕ (X ⊗ Y) ⊕ (Y ⊗ Y)
              in solve lhs rhs (x ∷ y ∷ a ∷ b ∷ []) refl

  _ : (x y a b : ⟨ R ⟩) → x · a ≡ a · x
  _ = λ x y a b →
              let
                lhs = X ⊗ A
                rhs = A ⊗ X
              in solve lhs rhs (x ∷ y ∷ a ∷ b ∷ []) refl

{-
  this one should work, but doesn't:

  _ : (x y a b : ⟨ R ⟩) → x · (a + b) ≡ a · x + b · x
  _ = λ x y a b →
              let
                lhs = X ⊗ (A ⊕ B)
                rhs = (A ⊗ X) ⊕ (B ⊗ X)
              in solve lhs rhs (x ∷ y ∷ a ∷ b ∷ []) refl

  the reason ist, that lhs and rhs evaluate to definitionally different things:

(0r · x +
 (0r · y +
  ((0r · a + (0r · b + 1r · 1r)) · a +
   ((0r · b + 1r · 1r) · b + 1r · 0r))))
· x
+ 0r

(0r · x +
 (0r · y +
  ((0r · a + (0r · b + 1r · 1r)) · a +
   ((0r · b + 1r · 1r) · b + (0r + 0r · 1r)))))
· x
+ 0r
-}
{-
  '-' is problematic...

  _ : (x y a b : ⟨ R ⟩) → (x + y) · (x - y) ≡ (x · x - (y · y))
  _ = λ x y a b → let
                lhs = (X ⊕ Y) ⊗ (X ⊕ (⊝ Y))
                rhs = (X ⊗ X) ⊕ (⊝ (Y ⊗ Y))
              in solve lhs rhs (x ∷ y ∷ a ∷ b ∷ []) {!!}
-}


text:
{-

This file contains:
  - Eliminators of direct limit, especially an index-shifting version;
  - Connectivity of inclusion maps.

-}
{-# OPTIONS --safe #-}
module Cubical.HITs.SequentialColimit.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function

open import Cubical.Data.Nat hiding (elim)
open import Cubical.HITs.SequentialColimit.Base
open import Cubical.Homotopy.Connected

private
  variable
    ℓ ℓ' : Level

module _
  (X : Sequence ℓ) where

  open Sequence

  private
    inl∞ : (n : ℕ) → X .space n → Lim→ X
    inl∞ n = inl {n = n}

  record ElimData (P : Lim→ X → Type ℓ') : Type (ℓ-max ℓ ℓ') where
    field
      finl  : {k : ℕ}(x : X .space k) → P (inl x)
      fpush : {k : ℕ}(x : X .space k) → PathP (λ i → P (push x i)) (finl x) (finl (X .map x))

  record ElimShiftData (n : ℕ)(P : Lim→ X → Type ℓ') : Type (ℓ-max ℓ ℓ') where
    field
      finl  : {k : ℕ}(x : X .space (k + n)) → P (inl x)
      fpush : {k : ℕ}(x : X .space (k + n)) → PathP (λ i → P (push x i)) (finl x) (finl (X .map x))

  open ElimData
  open ElimShiftData

  ElimData→ElimShiftData : (n : ℕ)(P : Lim→ X → Type ℓ')
    → ElimData P → ElimShiftData n P
  ElimData→ElimShiftData n P datum .finl  = datum .finl
  ElimData→ElimShiftData n P datum .fpush = datum .fpush

  -- Preliminary lemmas
  -- The difficulty is mainly due to natural numbers having no strict +-commutativity

  private
    alg-path : (a b : ℕ) → a + (1 + b) ≡ 1 + (a + b)
    alg-path a b = +-assoc a 1 b ∙ (λ i → +-comm a 1 i + b)

  module _
    (P : Lim→ X → Type ℓ')
    (datum : ElimShiftData 0 P) where

    +-zero-0 : refl ≡ +-zero 0
    +-zero-0 i j = isSet→SquareP (λ i j → isSetℕ) refl refl refl (+-zero 0) j i

    finl'-filler : (k : ℕ) → (i : I) → (x : X .space (+-zero k i)) → P (inl x)
    finl'-filler k i = transport-filler (λ i → (x : X .space (+-zero k i)) → P (inl x)) (datum .finl) i

    finl' : (k : ℕ) → (x : X .space k) → P (inl x)
    finl' k = finl'-filler k i1

    finl'-0-eq : datum .finl ≡ finl' 0
    finl'-0-eq = sym (transportRefl _)
      ∙ (λ j → transport (λ i → (x : X .space (+-zero-0 j i)) → P (inl x)) (datum .finl {k = 0}))

    fpush' : (k : ℕ)
      → (x : X .space k)
      → PathP (λ i → P (push x i)) (finl' k x) (finl' (1 + k) (X .map x))
    fpush' k = transport
      (λ i → (x : X .space (+-zero k i)) →
        PathP (λ i → P (push x i)) (finl'-filler k i x) (finl'-filler (1 + k) i (X .map x))) (datum .fpush)

    ElimShiftData0→ElimData : ElimData P
    ElimShiftData0→ElimData .finl  = finl'  _
    ElimShiftData0→ElimData .fpush = fpush' _

  module _
    (n : ℕ)(P : Lim→ X → Type ℓ')
    (datum : ElimShiftData (1 + n) P) where

    alg-path-0 : (b : ℕ) → refl ≡ alg-path 0 b
    alg-path-0 b i j = isSet→SquareP (λ i j → isSetℕ) refl refl refl (alg-path 0 b) j i

    finl-n-filler : (k : ℕ) → (i : I) → ((x : X .space (alg-path k n i)) → P (inl x))
    finl-n-filler k i = transport-filler (λ i → (x : X .space (alg-path k n i)) → P (inl x)) (datum .finl) i

    finl-n : (k : ℕ) → (x : X .space ((1 + k) + n)) → P (inl x)
    finl-n k = finl-n-filler k i1

    fpush-n : (k : ℕ)
      → (x : X .space ((1 + k) + n))
      → PathP (λ i → P (push x i)) (finl-n k x) (finl-n (1 + k) (X .map x))
    fpush-n k =
      transport
        (λ i → (x : X .space (alg-path k n i)) →
          PathP (λ i → P (push x i)) (finl-n-filler k i x) (finl-n-filler (1 + k) i (X .map x))) (datum .fpush)

    finl-0-filler : (x : X .space n) → (i : I) → P (push x i)
    finl-0-filler x i = transport-filler (λ i → P (push x (~ i))) (datum .finl {k = 0} (X .map x)) (~ i)

    finl-0 : (x : X .space n) → P (inl x)
    finl-0 x = finl-0-filler x i0

    finl-0-eq : datum .finl {k = 0} ≡ finl-n 0
    finl-0-eq = sym (transportRefl _)
      ∙ (λ j → transport (λ i → (x : X .space (alg-path-0 n j i)) → P (inl x)) (datum .finl {k = 0}))

    fpush-0 :
        (x : X .space n)
      → PathP (λ i → P (push x i)) (finl-0 x) (finl-n 0 (X .map x))
    fpush-0 x i =
      hcomp (λ j → λ
          { (i = i0) → finl-0 x
          ; (i = i1) → finl-0-eq j (X .map x) })
        (finl-0-filler x i)

    elimShiftDataSuc : ElimShiftData n P
    elimShiftDataSuc .finl  {k = 0} = finl-0
    elimShiftDataSuc .finl  {k = suc k} = finl-n k
    elimShiftDataSuc .fpush {k = 0} = fpush-0
    elimShiftDataSuc .fpush {k = suc k} = fpush-n k

  -- The eliminators

  elim :
      (P : Lim→ X → Type ℓ')
    → ElimData P
    → (x : Lim→ X) → P x
  elim P datum (inl x) = datum .finl x
  elim P datum (push x i) = datum .fpush x i

  elimShift : (n : ℕ)
    → (P : Lim→ X → Type ℓ')
    → ElimShiftData n P
    → (x : Lim→ X) → P x
  elimShift 0 _ datum = elim _ (ElimShiftData0→ElimData _ datum)
  elimShift (suc n) _ datum = elimShift n _ (elimShiftDataSuc _ _ datum)

  elimShiftβ : (n : ℕ)(k : ℕ)
    → (P : Lim→ X → Type ℓ')
    → (datum : ElimShiftData n P)
    → elimShift _ _ datum ∘ inl∞ (k + n) ≡ datum .finl
  elimShiftβ 0 0 _ datum = sym (finl'-0-eq _ datum)
  elimShiftβ 0 (suc k) P datum =
    transport (λ i → elimShift _ _ datum ∘ inl∞ (+-zero (suc k) (~ i))
      ≡ finl'-filler P datum (suc k) (~ i)) refl
  elimShiftβ (suc n) 0 _ datum =
      elimShiftβ n _ _ (elimShiftDataSuc _ _ datum)
    ∙ sym (finl-0-eq _ _ datum)
  elimShiftβ (suc n) (suc k) P datum =
    transport (λ i → elimShift _ _ datum ∘ inl∞ (alg-path (suc k) n (~ i))
      ≡ finl-n-filler n P datum (suc k) (~ i))
      (elimShiftβ n (suc (suc k)) P (elimShiftDataSuc _ _ datum))

  -- Lemma to lift sections

  open Iso

  private
    transpSec :
      (n : ℕ)(Y : Lim→ X → Type ℓ')
      (sec : (x : X .space n) → Y (inl x))
      → (x : X .space n) → Y (inl (X .map x))
    transpSec n Y sec x = transport (λ i → Y (push x i)) (sec x)

    module _
      (d : ℕ)(n : ℕ)
      (conn : isConnectedFun d (X .map {n = n}))
      (Y : Lim→ X → TypeOfHLevel ℓ' d) where

      module _
        (sec : (x : X .space n) → Y (inl (X .map x)) .fst) where

        lift-iso = elim.isIsoPrecompose _ d (Y ∘ inl) conn

        liftSec' : (x : X .space (1 + n)) → Y (inl x) .fst
        liftSec' = lift-iso .inv sec

        liftSecPath' : (x : X .space n) → sec x ≡ liftSec' (X .map x)
        liftSecPath' x i = lift-iso .rightInv sec (~ i) x

      module _
        (sec : (x : X .space n) → Y (inl x) .fst) where

        liftSec : (x : X .space (1 + n)) → Y (inl x) .fst
        liftSec = liftSec' (transpSec n (λ x → Y x .fst) sec)

        liftSecPath :
          (x : X .space n)
          → PathP (λ i → Y (push x i) .fst) (sec x) (liftSec (X .map x))
        liftSecPath x i =
          hcomp (λ j → λ
            { (i = i0) → sec x
            ; (i = i1) → liftSecPath'
                (transpSec n (λ x → Y x .fst) sec) x j })
          (transport-filler (λ i → Y (push x i) .fst) (sec x) i)

  module _
    (d : ℕ)(n : ℕ)
    (conn : (k : ℕ) → isConnectedFun d (X .map {n = k + n})) where

    private
      module _
        (Y : Lim→ X → TypeOfHLevel ℓ' d) where

        lifting : (k : ℕ)(sec : (x : X .space n) → Y (inl x) .fst)
          → (x : X .space (k + n)) → Y (inl x) .fst
        lifting 0 sec = sec
        lifting (suc k) sec = liftSec d _ (conn _) Y (lifting k sec)

        liftingPath : (k : ℕ)(sec : (x : X .space n) → Y (inl x) .fst)
          → (x : X .space (k + n))
          → PathP (λ i → Y (push x i) .fst) (lifting k sec x) (lifting (1 + k) sec (X .map x))
        liftingPath k sec = liftSecPath d _ (conn _) Y (lifting k sec)

        liftingData : ((x : X .space n) → Y (inl x) .fst) → ElimShiftData n (λ x → Y x .fst)
        liftingData sec .finl  = lifting _ sec
        liftingData sec .fpush = liftingPath _ sec

        hasSectionInl∘ : hasSection (λ (sec : (x : Lim→ X) → Y x .fst) → sec ∘ inl {n = n})
        hasSectionInl∘ .fst sec = elimShift  _ _   (liftingData sec)
        hasSectionInl∘ .snd sec = elimShiftβ _ _ _ (liftingData sec)

    -- Connectivity of inclusion map

    isConnectedInl∞ : isConnectedFun d (inl∞ n)
    isConnectedInl∞ = elim.isConnectedPrecompose _ _ hasSectionInl∘