text:
------------------------------------------------------------------------
-- Definitions of combinatorial functions
------------------------------------------------------------------------

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

module Math.Combinatorics.Function where

-- agda-stdlib
import Algebra.Operations.CommutativeMonoid as CommutativeMonoidOperations
open import Data.Fin using (toℕ)
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.Properties using (+-0-commutativeMonoid)
open import Data.List
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Unit using (tt)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (yes; no; ¬_)
open import Relation.Nullary.Decidable using (False; fromWitnessFalse)

-- agda-misc
open import Math.NumberTheory.Summation.Nat

open CommutativeMonoidOperations +-0-commutativeMonoid

infix 10 _! _!!

------------------------------------------------------------------------
-- Factorial
-- n ! = n * (n - 1) * ... * 2 * 1
-- A000142

_! : ℕ → ℕ
0       ! = 1
(suc n) ! = suc n * n !

------------------------------------------------------------------------
-- Permutation, Falling factorial
-- P n k = (n)ₖ = n * (n - 1) * ... * (n - k + 1)  (k terms)

P : ℕ → ℕ → ℕ
P n       0       = 1
P 0       (suc k) = 0
P (suc n) (suc k) = suc n * P n k

------------------------------------------------------------------------
-- Combination, Binomial coefficient
-- C n k = P n k / k !

C : ℕ → ℕ → ℕ
C n       0       = 1
C 0       (suc k) = 0
C (suc n) (suc k) = (C n k * suc n) / suc k

-- recursive definition
CRec : ℕ → ℕ → ℕ
CRec n       0       = 1
CRec 0       (suc k) = 0
CRec (suc n) (suc k) = CRec n k + CRec n (suc k)

------------------------------------------------------------------------
-- Double factorial
-- A006882

_!! : ℕ → ℕ
0           !! = 1
1           !! = 1
suc (suc n) !! = suc (suc n) * n !!

------------------------------------------------------------------------
-- unsigned Stirling numbers of the first kind

S1 : ℕ → ℕ → ℕ
S1 0       0       = 1
S1 0       (suc k) = 0
S1 (suc n) 0       = 0
S1 (suc n) (suc k) = n * S1 n (suc k) + S1 n k

------------------------------------------------------------------------
-- Stirling numbers of the second kind

S2 : ℕ → ℕ → ℕ
S2 0       0       = 1
S2 0       (suc k) = 0
S2 (suc n) 0       = 0
S2 (suc n) (suc k) = suc k * S2 n (suc k) + S2 n k

------------------------------------------------------------------------
-- Lah number

L : ℕ → ℕ → ℕ
L n               0             = 0
L 0               (suc k)       = 0
L 1               1             = 1
L 1               (suc (suc k)) = 0
L (suc n@(suc _)) (suc k)       = (n + suc k) * L n (suc k) + L n k

------------------------------------------------------------------------
-- Bell number
-- A000110

B : ℕ → ℕ
B n = Σ[ i ≤ n ] S2 n i

------------------------------------------------------------------------
-- Pochhammer symbol, Rising factorial
-- Poch n k = x^(n) = n * (n + 1) * ... * (n + k - 1) (k terms)

Poch : ℕ → ℕ → ℕ
Poch n 0       = 1
Poch n (suc k) = n * Poch (suc n) k

------------------------------------------------------------------------
-- Central binomial coefficient
-- A000984

CB : ℕ → ℕ
CB n = C (2 * n) n

------------------------------------------------------------------------
-- Catalan number
-- A000108

Catalan : ℕ → ℕ
Catalan n = CB n / suc n

------------------------------------------------------------------------
-- Eulerian number

A : ℕ → ℕ → ℕ
A 0       0       = 1
A 0       (suc m) = 0
A (suc n) 0       = 1
A (suc n) (suc m) = (n ∸ m) * A n m + suc (suc m) * A n (suc m)

------------------------------------------------------------------------
-- Eulerian numbers of the second kind

E2 : ℕ → ℕ → ℕ
E2 0       0       = 1
E2 0       (suc m) = 0
E2 (suc n) 0       = 1
E2 (suc n) (suc m) =
  (2 * suc n ∸ suc m ∸ 1) * E2 n m + suc (suc m) * E2 n (suc m)

------------------------------------------------------------------------
-- Multinomial coefficient
-- Multinomial xs = (sum xs) ! / product (map _! xs)

Multinomial : List ℕ → ℕ
Multinomial []           = 1
Multinomial xxs@(x ∷ xs) = C (sum xxs) x * Multinomial xs

------------------------------------------------------------------------
-- Pascal's triangle

gpascal : ∀ {a} {A : Set a} → (A → A → A) → A → A → ℕ → List A
gpascal f v0 v1 0       = v1 ∷ []
gpascal f v0 v1 (suc n) =
  let ps = gpascal f v0 v1 n in zipWith f (v0 ∷ ps) (ps ∷ʳ v0)

pascal : ℕ → List ℕ
pascal = gpascal _+_ 0 1


text:
{-# OPTIONS --without-K --safe #-}
module Source.Size.Substitution.Canonical where

open import Source.Size
open import Util.Prelude

infix  0 Sub⊢
infixl 5 _>>_

data Sub (Δ : Ctx) : (Ω : Ctx) → Set where
  [] : Sub Δ []
  Snoc : (σ : Sub Δ Ω) (n : Size Δ) → Sub Δ (Ω ∙ m)

variable
  σ τ σ′ τ′ ι ι′ : Sub Δ Ω

subV : Sub Δ Ω → Var Ω → Size Δ
subV (Snoc σ n) zero = n
subV (Snoc σ n) (suc x) = subV σ x

sub : Sub Δ Ω → Size Ω → Size Δ
sub σ (var x) = subV σ x
sub σ ∞ = ∞
sub σ zero = zero
sub σ (suc n) = suc (sub σ n)

data Sub⊢ Δ : ∀ Ω (σ : Sub Δ Ω) → Set where
  [] : Sub⊢ Δ [] []
  Snoc : (⊢σ : Sub⊢ Δ Ω σ) (n<m : n < sub σ m) → Sub⊢ Δ (Ω ∙ m) (Snoc σ n)

syntax Sub⊢ Δ Ω σ = σ ∶ Δ ⇒ Ω

abstract
  sub-Snoc : ∀ (σ : Sub Δ Ω) n o
    → sub (Snoc {m = m} σ n) (wk o) ≡ sub σ o
  sub-Snoc σ n (var x) = refl
  sub-Snoc σ n ∞ = refl
  sub-Snoc σ n zero = refl
  sub-Snoc σ n (suc o) = cong suc (sub-Snoc σ n o)

  mutual
    subV-resp-< : σ ∶ Δ ⇒ Ω → var x < n → subV σ x < sub σ n
    subV-resp-< {x = zero} (Snoc {σ = σ} {n} {m} ⊢σ n<m) (var refl)
      = subst (n <_) (sym (sub-Snoc σ n m)) n<m
    subV-resp-< {x = suc x} (Snoc {σ = σ} {n} {m} ⊢σ n<m) (var refl)
      = subst (subV σ x <_) (sym (sub-Snoc σ n (bound x)))
          (subV-resp-< ⊢σ (var refl))
    subV-resp-< ⊢σ <suc = <suc
    subV-resp-< ⊢σ (<-trans x<m m<n)
      = <-trans (subV-resp-< ⊢σ x<m) (sub-resp-< ⊢σ m<n)

    sub-resp-< : σ ∶ Δ ⇒ Ω → n < m → sub σ n < sub σ m
    sub-resp-< ⊢σ (var p) = subV-resp-< ⊢σ (var p)
    sub-resp-< ⊢σ zero<suc = zero<suc
    sub-resp-< ⊢σ zero<∞ = zero<∞
    sub-resp-< ⊢σ (suc<suc n<m) = suc<suc (sub-resp-< ⊢σ n<m)
    sub-resp-< ⊢σ (suc<∞ n<∞) = suc<∞ (sub-resp-< ⊢σ n<∞)
    sub-resp-< ⊢σ (<-trans n<o o<m)
      = <-trans (sub-resp-< ⊢σ n<o) (sub-resp-< ⊢σ o<m)
    sub-resp-< ⊢σ <suc = <suc

Weaken : Sub Δ Ω → Sub (Δ ∙ n) Ω
Weaken [] = []
Weaken (Snoc σ m) = Snoc (Weaken σ) (wk m)

abstract
  subV-Weaken : ∀ (σ : Sub Δ Ω) x → subV (Weaken {n = o} σ) x ≡ wk (subV σ x)
  subV-Weaken (Snoc σ n) zero = refl
  subV-Weaken (Snoc σ n) (suc x) = subV-Weaken σ x

  sub-Weaken : ∀ (σ : Sub Δ Ω) n → sub (Weaken {n = o} σ) n ≡ wk (sub σ n)
  sub-Weaken σ (var x) = subV-Weaken σ x
  sub-Weaken σ ∞ = refl
  sub-Weaken σ zero = refl
  sub-Weaken σ (suc n) = cong suc (sub-Weaken σ n)

  Weaken⊢ : σ ∶ Δ ⇒ Ω → Weaken σ ∶ Δ ∙ n ⇒ Ω
  Weaken⊢ [] = []
  Weaken⊢ (Snoc {σ = σ} {n} {m} ⊢σ n<m)
    = Snoc (Weaken⊢ ⊢σ)
        (subst (wk n <_) (sym (sub-Weaken σ m)) (wk-resp-< n<m))

Lift : (σ : Sub Δ Ω) → Sub (Δ ∙ m) (Ω ∙ n)
Lift σ = Snoc (Weaken σ) (var zero)

abstract
  Lift⊢ : σ ∶ Δ ⇒ Ω → m ≡ sub σ n → Lift σ ∶ Δ ∙ m ⇒ Ω ∙ n
  Lift⊢ {Δ} {σ = σ} {n = n} ⊢σ refl
    = Snoc (Weaken⊢ ⊢σ) (var (sub-Weaken σ n))

mutual
  Id : Sub Δ Δ
  Id {[]} = []
  Id {Δ ∙ n} = Lift Id

  abstract
    subV-Id : ∀ x → subV (Id {Δ}) x ≡ var x
    subV-Id zero = refl
    subV-Id (suc x) = trans (subV-Weaken Id x) (cong wk (subV-Id x))

    sub-Id : ∀ n → σ ≡ Id → sub σ n ≡ n
    sub-Id (var x) refl  = subV-Id x
    sub-Id ∞ _ = refl
    sub-Id zero _ = refl
    sub-Id (suc n) p = cong suc (sub-Id n p)

abstract
  Id⊢ : Id ∶ Δ ⇒ Δ
  Id⊢ {[]} = []
  Id⊢ {Δ ∙ n} = Lift⊢ Id⊢ (sym (sub-Id _ refl))

Wk : Sub (Δ ∙ n) Δ
Wk = Weaken Id

abstract
  sub-Wk : ∀ n → sub (Wk {Δ} {o}) n ≡ wk n
  sub-Wk n = trans (sub-Weaken Id n) (cong wk (sub-Id _ refl))

  Wk⊢ : Wk ∶ Δ ∙ n ⇒ Δ
  Wk⊢ = Weaken⊢ Id⊢

Sing : Size Δ → Sub Δ (Δ ∙ m)
Sing n = Snoc Id n

abstract
  Sing⊢ : n < m → Sing n ∶ Δ ⇒ Δ ∙ m
  Sing⊢ {n = n} n<m
    = Snoc Id⊢ (subst (n <_) (sym (sub-Id _ refl)) n<m)

_>>_ : Sub Δ Δ′ → Sub Δ′ Δ″ → Sub Δ Δ″
σ >> [] = []
σ >> Snoc τ n = Snoc (σ >> τ) (sub σ n)

abstract
  subV->> : ∀ (σ : Sub Δ Δ′) (τ : Sub Δ′ Δ″) x
    → subV (σ >> τ) x ≡ sub σ (subV τ x)
  subV->> σ (Snoc τ n) zero = refl
  subV->> σ (Snoc τ n) (suc x) = subV->> σ τ x

  sub->> : ∀ n → ι ≡ σ >> τ
    → sub ι n ≡ sub σ (sub τ n)
  sub->> {σ = σ} {τ} (var x) refl = subV->> σ τ x
  sub->> ∞ _ = refl
  sub->> zero _ = refl
  sub->> (suc n) p = cong suc (sub->> n p)

  sub->>′ : σ >> τ ≡ σ′ >> τ′ → sub σ (sub τ n) ≡ sub σ′ (sub τ′ n)
  sub->>′ {σ = σ} {τ = τ} {σ′ = σ′} {τ′} {n} eq
    = trans (sym (sub->> n refl))
        (trans (cong (λ σ → sub σ n) eq) (sub->> n refl))

  >>⊢ : σ ∶ Δ ⇒ Δ′ → τ ∶ Δ′ ⇒ Δ″ → σ >> τ ∶ Δ ⇒ Δ″
  >>⊢ ⊢σ [] = []
  >>⊢ {σ = σ} ⊢σ (Snoc {σ = τ} {n} {m} ⊢τ n<m)
    = Snoc (>>⊢ ⊢σ ⊢τ)
        (subst (sub σ n <_) (sym (sub->> m refl)) (sub-resp-< ⊢σ n<m))

Skip : Sub (Δ ∙ n ∙ v0) (Δ ∙ n)
Skip = Snoc (Weaken Wk) (var zero)

abstract
  Skip⊢ : Skip ∶ Δ ∙ n ∙ v0 ⇒ Δ ∙ n
  Skip⊢ {n = n}
    = Snoc (Weaken⊢ Wk⊢)
        (<-trans (var refl)
          (var (trans (sub-Weaken Wk n) (cong wk (sub-Wk n)))))

  Weaken>> : Weaken σ >> τ ≡ Weaken {n = n} (σ >> τ)
  Weaken>> {τ = []} = refl
  Weaken>> {σ = σ} {τ = Snoc τ n} = cong₂ Snoc Weaken>>  (sub-Weaken σ n)

  Snoc>>Weaken : Snoc {m = m} σ n >> Weaken τ ≡ σ >> τ
  Snoc>>Weaken {τ = []} = refl
  Snoc>>Weaken {σ = σ} {n = n} {τ = Snoc τ k}
    = cong₂ Snoc Snoc>>Weaken (sub-Snoc σ n k)

  id-l : Id >> σ ≡ σ
  id-l {σ = []} = refl
  id-l {σ = Snoc σ n} = cong₂ Snoc id-l (sub-Id n refl)

  id-r : {σ : Sub Δ Ω} → σ >> Id ≡ σ
  id-r {σ = []} = refl
  id-r {σ = Snoc σ n} = cong₂ Snoc (trans Snoc>>Weaken id-r) refl

  >>-assoc : σ >> (τ >> ι) ≡ σ >> τ >> ι
  >>-assoc {ι = []} = refl
  >>-assoc {σ = σ} {τ = τ} {ι = Snoc ι n}
    = cong₂ Snoc >>-assoc (sym (sub->> n refl))

  Wk>> : Wk >> σ ≡ Weaken {n = n} σ
  Wk>> = trans Weaken>> (cong Weaken id-l)

  Snoc>>Wk : Snoc {m = m} σ n >> Wk ≡ σ
  Snoc>>Wk = trans Snoc>>Weaken id-r

  Lift>>Weaken : Lift {m = m} {n} σ >> Weaken τ ≡ Weaken (σ >> τ)
  Lift>>Weaken = trans Snoc>>Weaken Weaken>>

  Lift>>Wk : Lift {m = m} {n} σ >> Wk ≡ Wk >> σ
  Lift>>Wk = trans Lift>>Weaken (trans (sym Wk>>) (cong (Wk >>_) id-r))

  Sing>>Weaken : Sing {m = m} n >> Weaken σ ≡ σ
  Sing>>Weaken = trans Snoc>>Weaken id-l

  Sing>>Wk : Sing {m = m} n >> Wk ≡ Id
  Sing>>Wk = trans Snoc>>Weaken id-r

  Sing>>Lift : ∀ n → Sing (sub σ n) >> Lift {m = m} {o} σ ≡ σ >> Sing n
  Sing>>Lift n = cong₂ Snoc (trans Sing>>Weaken (sym id-r)) refl

  Lift>>Lift : Lift {m = m} {n} σ >> Lift {n = o} τ ≡ Lift (σ >> τ)
  Lift>>Lift = cong₂ Snoc Lift>>Weaken refl

  Skip>>Weaken : Skip {n = n} >> Weaken σ ≡ Weaken (Weaken σ)
  Skip>>Weaken = trans Snoc>>Weaken (trans Weaken>> (cong Weaken Wk>>))

  Skip>>Lift : Skip >> Lift {m = m} {n} σ ≡ Lift (Lift σ) >> Skip
  Skip>>Lift
    = cong₂ Snoc
        (trans Skip>>Weaken
          (sym (trans Lift>>Weaken (cong Weaken (trans Snoc>>Weaken id-r)))))
      refl

  Lift-Id : Lift {m = m} Id ≡ Id
  Lift-Id = refl

  LiftSing>>Wk>>Wk : Lift {m = o} {m} (Sing n) >> (Wk >> Wk) ≡ Wk
  LiftSing>>Wk>>Wk {n = n} = let open ≡-Reasoning in
    begin
      Lift (Sing n) >> (Wk >> Wk)
    ≡⟨ cong (Lift (Sing n) >>_) Wk>> ⟩
      Lift (Sing n) >> (Weaken Wk)
    ≡⟨ Lift>>Weaken ⟩
      Weaken (Sing n >> Weaken Id)
    ≡⟨ cong Weaken Sing>>Weaken ⟩
      Wk
    ∎

  LiftSing>>Skip
    : Lift {m = m} (Sing {m = m} n) >> Skip ≡ Sing {m = o} (var zero) >> Lift Wk
  LiftSing>>Skip {n = n} = cong₂ Snoc go refl
    where
      go : Lift (Sing n) >> Weaken Wk ≡ Sing (var zero) >> Weaken Wk
      go = let open ≡-Reasoning in
        begin
          Lift (Sing n) >> Weaken Wk
        ≡⟨ Lift>>Weaken ⟩
          Weaken (Sing n >> Weaken Id)
        ≡⟨ cong Weaken Sing>>Wk ⟩
          Wk
        ≡⟨ sym Sing>>Weaken ⟩
          Sing (var zero) >> Weaken Wk
        ∎

  LiftLift>>Skip : Lift (Lift {m = m} {n} σ) >> Skip ≡ Skip >> Lift σ
  LiftLift>>Skip
    = cong₂ Snoc (trans Lift>>Weaken
        (sym (trans Skip>>Weaken (cong Weaken (sym Snoc>>Wk))))) refl

ext: agda

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module Algebra.Module.Normed where

open import Assume using (assume)
open import Algebra.Bundles using (CommutativeRing)
open import Algebra.Module.Bundles using (Module)
open import Level using (_⊔_; suc)
open import Relation.Nullary using (¬_)
open import Relation.Binary using (Rel)
open import Function.Metric using (IsGeneralMetric)

module _
  {r ℓr} {CR : CommutativeRing r ℓr}
  {m ℓm} (M : Module CR m ℓm)
  where

  private
    module CR = CommutativeRing CR
    module M = Module M

  module _
    {rel} (_≤_ : Rel CR.Carrier rel)
    (∥_∥ : M.Carrierᴹ → CR.Carrier)
    where

    record IsNormedModule : Set (r ⊔ ℓr ⊔ m ⊔ ℓm ⊔ rel) where
      open CommutativeRing CR public
      open M public

      field
        triangle-norm : ∀ x y → (∥ x +ᴹ y ∥) ≤ (∥ x ∥ + ∥ y ∥)
        homogeneity : ∀ s x → ∥ s *ₗ x ∥ ≈ s * ∥ x ∥
        positive-definite : ∀ x → ∥ x ∥ ≈ 0# → x ≈ᴹ 0ᴹ

      infixl 6 _-ᴹ_
      _-ᴹ_ : Carrierᴹ → Carrierᴹ → Carrierᴹ
      x -ᴹ y = x +ᴹ (-ᴹ y)

      ⟨_,_⟩ : Carrierᴹ → Carrierᴹ → Carrier
      ⟨ x , y ⟩ = ∥ x -ᴹ y ∥

      isGeneralMetric : IsGeneralMetric _≈ᴹ_ _≈_ _≤_ 0# _+_ ⟨_,_⟩
      isGeneralMetric = assume

      open IsGeneralMetric isGeneralMetric public hiding (refl; reflexive)

module _
  {r ℓr} (CR : CommutativeRing r ℓr)
  (open CommutativeRing CR using () renaming (Carrier to X))
  {rel} (_≤_ : Rel X rel)
  m ℓm
  where

  record NormedModule : Set (suc (r ⊔ ℓr ⊔ m ⊔ ℓm ⊔ rel)) where
    module CR = CommutativeRing CR
    field
      M : Module CR m ℓm

    module M = Module M

    field
      ∥_∥ : M.Carrierᴹ → CR.Carrier
      isNormedModule : IsNormedModule M _≤_ ∥_∥

    open IsNormedModule isNormedModule public

module _
  {r ℓr} {CR : CommutativeRing r ℓr}
  (open CommutativeRing CR using () renaming (Carrier to X))
  {rel} {_≤_ : Rel X rel}
  {ma ℓma} (MA : NormedModule CR _≤_ ma ℓma)
  {mb ℓmb} (MB : NormedModule CR _≤_ mb ℓmb)
  where

  private
    module CR = CommutativeRing CR
    module MA = NormedModule MA
    module MB = NormedModule MB

  directProduct : NormedModule CR _≤_ (ma ⊔ mb) (ℓma ⊔ ℓmb)
  directProduct =
    record
    { M = ⟨module⟩ MA.M MB.M
    ; ∥_∥ = (uncurry CR._+_) ∘ (map MA.∥_∥ MB.∥_∥)
    ; isNormedModule = assume
    }
    where
      open import Algebra.Module.Construct.DirectProduct
      open import Function using (_∘_)
      open import Data.Product using (uncurry; map)

module _
  {r ℓr} {CR : CommutativeRing r ℓr}
  (open CommutativeRing CR using () renaming (Carrier to X))
  {rel} {_≤_ : Rel X rel}
  (∥_∥ : X → X)
  where

  tensorUnit : NormedModule CR _≤_ r ℓr
  tensorUnit =
    record
    { M = ⟨module⟩
    ; ∥_∥ = ∥_∥
    ; isNormedModule = assume
    }
    where open import Algebra.Module.Construct.TensorUnit

module _
  {r ℓr} {CR : CommutativeRing r ℓr}
  (open CommutativeRing CR using () renaming (Carrier to X))
  {rel} {_≤_ : Rel X rel}
  where

  null : ∀ {c l} → NormedModule CR _≤_ c l
  null =
    record
    { M = ⟨module⟩
    ; ∥_∥ = λ _ → 0#
    ; isNormedModule = assume
    }
    where
      open import Algebra.Module.Construct.Zero
      open CommutativeRing CR

-- TODO
-- →NormedModule

max_stars_repo_name: cspollard/reals

max_issues_repo_name: cspollard/reals

max_forks_repo_name: cspollard/reals


text:
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Cubical.Data.NatPlusOne.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Nat
open import Cubical.Data.NatPlusOne.Base

1+Path : ℕ ≡ ℕ₊₁
1+Path = isoToPath (iso 1+_ -1+_ (λ _ → refl) (λ _ → refl))


text:
module Common where

open import Level using (Level)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; sym; refl)
open import Relation.Nullary.Decidable using (False; toWitnessFalse)
open import Data.Nat using (ℕ)
open import Data.Fin using (Fin; _≟_)

private
  variable
    n : ℕ
    l : Level
    A : Set l
    x x′ y : A

Label : Set
Label = ℕ

data Action (n : ℕ) : Set where
  action : (p q : Fin n) -> p ≢ q -> Label -> Action n

action′ : (p q : Fin n) -> {False (p ≟ q)} -> Label -> Action n
action′ p q {p≢q} l = action p q (toWitnessFalse p≢q) l

¬≡-flip : x ≢ y -> y ≢ x
¬≡-flip x≢y = λ y≡x → x≢y (sym y≡x)

≢-subst-left : x ≢ y -> x ≡ x′ -> x′ ≢ y
≢-subst-left x≢y refl = x≢y

≢-subst-right : y ≢ x -> x ≡ x′ -> y ≢ x′
≢-subst-right y≢x refl = y≢x

max_stars_repo_name: fangyi-zhou/mpst-in-agda

max_issues_repo_name: fangyi-zhou/mpst-in-agda

max_forks_repo_name: fangyi-zhou/mpst-in-agda


text:
module BTA3 where

open import Data.Nat
open import Data.Bool
open import Data.List

-- Binding times
data BT : Set where
  S : BT
  D : BT

-- defining a data type [BT],where two members are
-- [S] standing for "static" and [D] standing for dynamic.

-- ``subsumption'' binding times; static can be treated as dynamic,
-- but not vice versa
_≼_ : BT → BT → Bool
_≼_ D S  = false
_≼_ _ _  = true

-- note that the above function can also be specified as follows,
-- _≼_ : BT → BT → Bool
-- D ≼ S = false
-- _ ≼ _ = true

-- note that the function [≼] specifies that a "static",S, can be treated
-- as a "dynamic",D, and not the other way round
-- since in Agda, pattern matching is conducted in a sequencial fashion,
-- the above specification makes sure that it returns [false] when the
-- first argument is [D] and the second [S] and returns [true] in all
-- the other three cases.

-- BEGIN: stuff that is also in the standard library

-- Standard propositional equality, see also Relation.Binary.PropositionalEquality
data _==_ {A : Set} (x : A) : A → Set where
  refl : x == x
-- [_==_] defines an equality proposition
-- it takes two identical elements of one type as arguments and gives one
-- evidence,[refl],for the proposition

-- subst lemma
subst : {A B : Set}{x x' : A} {C : A → B} → x == x' → C x == C x'
subst{A}{B}{x}{.x} refl = refl

-- or being defined in the following manner...
-- my_subst : {A B : Set}{x x' : A}{C : A → B} →  x == x' → C x == C x'
-- my_subst refl = refl

-- the above function further helps to construct evidence for equality
-- proposition
-- it says that if two elements are identical then two new elements obtained
-- by applying the former to a function  should also be identical

record True : Set where
data False : Set where

-- note that the above is regarding two simple proposition [True] and [False]
-- regarding [True],
-- it is defined as empty record with a single element of type [True],[record{}]
-- the trick here is that the type checker knows this and fills in any implicit
-- arguments of [True] with this element
-- another way of defining [True] as follows,
-- record True : Set where
-- trivial : True
-- trivial = _

-- regarding [False],
-- it is defined as a proposition without any evidence corresponding well to
-- what a [False] proposition really means

isTrue : Bool → Set
isTrue true  = True
isTrue false = False
-- note the isTrue b,given b as boolean, is the type of proof that b is equal to
-- true since if it is the case, [isTrue b] returns type [True] where its
-- evidence is automatically filled in by the type checker while if it is not
-- the case there is no way to supply for the evidence due to the way how
-- [false] is constructed

-- END standard library

----------------------
-- Sublists
----------------------
data _cx-≤_ {A : Set} : List A → List A → Set where
  cxle-eq : (l : List A) → l cx-≤ l
  cxle-lt : ∀ {l₁ l₂} x → l₁ cx-≤ l₂ → l₁ cx-≤ (x ∷ l₂)

lem-cx-≤-trans : {A : Set} → {l₁ : List A} {l₂ : List A} {l₃ : List A} →
                 l₁ cx-≤ l₂ → l₂ cx-≤ l₃ → l₁ cx-≤ l₃
lem-cx-≤-trans le1  (cxle-eq l) = le1
lem-cx-≤-trans (cxle-eq l) (cxle-lt x e) = cxle-lt x e
lem-cx-≤-trans (cxle-lt x e) (cxle-lt x' e') = cxle-lt x' (lem-cx-≤-trans (cxle-lt x e) e')

_cxle-∷_ : {A : Set} (x : A) (l : List A) → l cx-≤ (x ∷ l)
x cxle-∷ l = cxle-lt x (cxle-eq l)

data _⊆_ {A : Set} : List A → List A → Set where
  refl-⊆ : ∀ {l} → l ⊆ l
  step-⊆ : ∀ {l} x l₁ l₂ → l ⊆ (l₁ ++ l₂) → l ⊆ (l₁ ++ (x ∷ l₂))

lem-⊆-trans : {A : Set} → {l₁ : List A} {l₂ : List A} {l₃ : List A} →
                 l₁ ⊆ l₂ → l₂ ⊆ l₃ → l₁ ⊆ l₃
lem-⊆-trans e (refl-⊆ {l}) = e
lem-⊆-trans (refl-⊆ {l}) (step-⊆ x l₁ l₂ e) = step-⊆ x l₁ l₂ e
lem-⊆-trans (step-⊆ x l₁ l₂ e) (step-⊆ x' l₁' l₂' e') = step-⊆ x' l₁' l₂' (lem-⊆-trans (step-⊆ x l₁ l₂ e) e')

-- data _≤1_ {A : Set} : List A → List A → Set where
--   cxle1-eq : (l : List A) → l ≤1 l
--   cxle1-lt : ∀ x (l : List A) → l ≤1 (x ∷ l)

-- data _?∷_ {A : Set} (x : A): List A → Set where
--   yes∷ : (l : List A) → x ?∷ (x ∷ l)
--   no∷ : (l : List A) → x ?∷ l

-- getList : ∀ {A} {x : A} {l : List A} → x ?∷ l → List A
-- getList {x = x} (yes∷ l) = x ∷ l
-- getList {_} {_} {l} (no∷ .l) = l

-- end sublists

-- some lemmas about BT subsumption
lem-bt≼S : {bt : BT} → isTrue (bt ≼ S) → bt == S
lem-bt≼S {S} bt≼S = refl
lem-bt≼S {D} ()

-- which can also be defined as follows,
-- my_lem-bt≼S : {bt : BT} → isTrue (bt ≼ S) → bt == S
-- my_lem-bt≼S {S} _ = refl
-- my_lem-bt≼S {D} ()

lem-D≼bt : {bt : BT} → isTrue (D ≼ bt) → bt == D
lem-D≼bt {S} ()
lem-D≼bt {D} D≼bt = refl

-- Types of the calculus
mutual
  -- s ^ BT
  data AType : Set where
    Ann : BT → SType → AType

  -- int | t -> t
  data SType : Set where
    SInt  : SType
    SFun  : AType → AType → SType

-- aux definitions
ATInt : BT → AType
ATInt bt = Ann bt SInt
ATFun  : BT → AType → AType → AType
ATFun  bt at1 at2 = Ann bt (SFun at1 at2)

-- note that the above function labels a ground type with annotations [S] or
-- [D],sort of a labelling function

-- projection: get the BT from a type
btof : AType → BT
btof (Ann bt _) = bt

-- a related function which takes an annotated type as argument and returns
-- the annotation of that type

-- "constraint on types: functions have to be at least as dynamic as their component" should be corrected as follows,
-- arguments of function should be as dynamic as the function

data wft : AType → Set where
  wf-int  : ∀ {bt} → wft (Ann bt SInt)
  wf-fun  : ∀ {bt at1 at2} → wft at1 → wft at2
          → isTrue (bt ≼ btof at1) → isTrue (bt ≼ btof at2) → wft (Ann bt (SFun at1 at2))

-- the above proposition specifies a set of well-formed [AType]s,
-- any annotated [SInt]s are well-formed, wft (Ann bt SInt) forall bt ∈ BT
-- in case of functional type with annotation, the following two criteria have
-- to be satisfied to be a well form,
-- a. each of its arguments is well-formed
-- b. the annotation of the function and the annotations of its arguments must
--    satisfy [_≼_] relation
--    for instance, the functional type defined above is well-formed while
--    the following is not,
--    Ann D (
--            SFun (Ann S SInt) (Ann D SInt)
--          )
--    in conclusion,for functional type with annotation to be well-formed,
--    each of its arguments annotations has to be [D] when that of the function
--    is [D] while there is no constraint upon the annotations of its arguments
--    when that of the function is [S]

lem-force-bt : ∀ {bt at} → isTrue (bt ≼ btof at) → D == bt → D == btof at
lem-force-bt {S} bt≼at ()
lem-force-bt {D} {Ann S y'} () D=bt
lem-force-bt {D} {Ann D y'} bt≼at D=bt = refl

-- note the above function takes an element[bt] of type [BT] and a type with
-- annotation,
-- if both
-- a. the type is at least as dynamic as [bt]
-- b. [bt == D]
-- then we know that the annotation of the type must be [D] as well
-- and the function in that case returns evidence for that

-- Low-level types; types wihtout binding information
data Type : Set where
  TInt : Type
  TFun : Type → Type → Type

-- translation from ATypes to low-level types
mutual
  strip : AType → Type
  strip (Ann _ σ) = strip' σ

  strip' : SType → Type
  strip' SInt = TInt
  strip' (SFun y y') = TFun (strip y) (strip y')

-- note that the above function [strip] converts a type with annotation [AType]
-- to a low-level type [Type],
-- for instance,
-- strip (Ann D SInt)
-- = strip' SInt
-- = TInt
-- strip (Ann S
--         SFun (Ann S SInt) (Ann D SInt)
--       )
-- = strip' (SFun (Ann S SInt) (Ann D SInt))
-- = TFun (strip (Ann S SInt)) (strip (Ann D SInt))
-- = TFun (strip' SInt) (strip' SInt)
-- = TFun TInt TInt^

-- More general purpose definitions (should also be in standard library)
-- list membership
infix 4 _∈_
data _∈_ {A : Set} : A → List A → Set where
  hd : ∀ {x xs} → x ∈ (x ∷ xs)
  tl : ∀ {x y xs} → x ∈ xs → x ∈ (y ∷ xs)

-- note the above proposition gives us two constructors for getting
-- evidences for an element being a member of one list

-- end general purpose definitions

-- Typing context
Ctx = List Type

--data Exp' (Γ Γ' : Ctx) : Type → Set where
--  EVar' :

-- Typed expression
data Exp (Γ : Ctx) : Type → Set where
  -- [EVar] corresponds to the bounded variables in [AExp]
  EVar : ∀ {τ} → τ ∈ Γ → Exp Γ τ
  EInt : ℕ → Exp Γ TInt
  EFun : ∀ {τ₁ τ₂} → Exp (τ₂ ∷ Γ) τ₁ → Exp Γ (TFun τ₂ τ₁)
  EApp : ∀ {τ₁ τ₂} → Exp Γ (TFun τ₂ τ₁) → Exp Γ τ₂ → Exp Γ τ₁
-- one additional term,
count_tl : ∀ {A  Γ Γ'} {τ : A } → τ ∈ Γ → Γ cx-≤ Γ' → τ ∈ Γ'
count_tl  x (cxle-eq Γ) = x
count_tl x  (cxle-lt T e) = tl (count_tl x e)

data _cx=≤_ {A : Set} : List A → List A → Set where
  cxle-peq : ∀ {l₁ l₂} { x } → l₁ cx-≤ l₂ → (x ∷ l₁) cx=≤ (x ∷ l₂)
  cxle-plt : ∀ {l₁ l₂} { x } → l₁ cx=≤ l₂ → (x ∷ l₁) cx=≤ (x ∷ l₂)

count_tl' : ∀ {A  Γ Γ'} {τ : A } → τ ∈ Γ → Γ cx=≤ Γ' → τ ∈ Γ'
count_tl' hd (cxle-plt e) = hd
count_tl' hd (cxle-peq e) = hd
count_tl' (tl xid) (cxle-plt e) = tl (count_tl' xid  e)
count_tl' (tl xid) (cxle-peq e) = tl (count_tl xid e)

lem-Exp-weakening' : ∀ {τ₂ τ₁ Γ Γ'} → Exp (τ₂ ∷ Γ) τ₁ → (τ₂ ∷ Γ) cx=≤ (τ₂ ∷ Γ') → Exp (τ₂ ∷ Γ') τ₁
lem-Exp-weakening' (EVar x) e = EVar (count_tl' x  e)
lem-Exp-weakening'  (EInt n) e = EInt n
lem-Exp-weakening'  (EFun t) e = EFun (lem-Exp-weakening' t (cxle-plt e))
lem-Exp-weakening'  (EApp t1 t2) e = EApp (lem-Exp-weakening' t1 e) (lem-Exp-weakening' t2 e)

lem-Exp-weakening : ∀ {τ Γ Γ'} → Exp Γ τ → Γ cx-≤ Γ' → Exp Γ' τ
lem-Exp-weakening t (cxle-eq Γ) = t
lem-Exp-weakening (EInt n) e = EInt n
lem-Exp-weakening (EVar x) e  = EVar (count_tl x e)
lem-Exp-weakening (EFun t) (cxle-lt T e) = EFun (lem-Exp-weakening' t (cxle-peq (cxle-lt T e)))
lem-Exp-weakening (EApp t1 t2) e = EApp (lem-Exp-weakening t1 e) (lem-Exp-weakening t2 e)

-- typed annotated expressions
ACtx = List AType

data AExp (Δ : ACtx) : AType → Set where
  AVar : ∀ {α} → α ∈ Δ → AExp Δ α
  AInt : (bt : BT) → ℕ → AExp Δ (ATInt bt)
  AFun : ∀ {α₁ α₂} (bt : BT) → wft (ATFun bt α₂ α₁) → AExp (α₂ ∷ Δ) α₁ → AExp Δ (ATFun bt α₂ α₁)
  AApp : ∀ {α₁ α₂} (bt : BT) → wft (ATFun bt α₂ α₁) → AExp Δ (ATFun bt α₂ α₁) → AExp Δ α₂ → AExp Δ α₁

-- stripping of contexts
residual : ACtx → Ctx
residual [] = []
residual (Ann S _ ∷ xs) = residual xs
residual (Ann D σ ∷ xs) = strip' σ ∷ residual xs

-- ``semantic domain'' for partially evaluated AExp-terms:
--   - AExp-terms of dynamic type evaluate to Exp-terms
--   - AExp-terms of static type evaluate to agda terms, where SFun
--     are functions and SInt are natural numbers
mutual
  impTA : Ctx → AType → Set
  impTA Γ (Ann S σ) = impTA' Γ σ
  impTA Γ (Ann D σ) = Exp Γ (strip' σ)

  impTA' : Ctx → SType → Set
  impTA' Γ SInt = ℕ
  -- impTA' Γ (SFun y y') = impTA Γ y → impTA Γ y'
  impTA' Γ (SFun y y') = ∀ {Γ'} → Γ cx-≤ Γ' → impTA Γ' y → impTA Γ' y'

lem-impTA-weakening : ∀ {α Γ Γ'} →
                      impTA Γ α →
                      Γ cx-≤ Γ' →
                      impTA Γ' α
lem-impTA-weakening {Ann S SInt} v _ = v
lem-impTA-weakening {Ann S (SFun x x₁)} f prf = λ prf' → f (lem-cx-≤-trans prf prf')
lem-impTA-weakening {Ann D x₁} v prf = lem-Exp-weakening v prf

-- mutual
--   impTA-try : Ctx → AType → Set
--   impTA-try Γ (Ann S σ) = impTA-try' Γ σ
--   impTA-try Γ (Ann D σ) = Exp Γ (strip' σ)

--   impTA-try' : Ctx → SType → Set
--   impTA-try' Γ SInt = ℕ
--   impTA-try' Γ (SFun y y') = impTA-try Γ y → impTA-try Γ y'

-- lem-impTA-try-weakening : ∀ {α Γ Γ'} →
--                       impTA-try Γ α →
--                       Γ cx-≤ Γ' →
--                       impTA-try Γ' α
-- lem-impTA-try-weakening {Ann S SInt} v _ = v
-- lem-impTA-try-weakening {Ann S (SFun α x₁)} {Γ} {Γ'} f prf = {! λ (v : impTA-try Γ' α) → f v!}
-- lem-impTA-try-weakening {Ann D x₁} v prf = lem-Exp-weakening v prf

data AEnv : Ctx → ACtx → Set where
  env[] :  ∀ {Γ} → AEnv Γ []
  envS:: : ∀ {Γ Δ} {α} →
           impTA Γ α →
           AEnv Γ Δ →
           AEnv Γ (α ∷ Δ)
  envD:: : ∀ {Γ Δ} →
           (σ : SType) →
           impTA (strip' σ ∷ Γ) (Ann D σ) →
           AEnv Γ Δ →
           AEnv (strip' σ ∷ Γ) (Ann D σ ∷ Δ)

lem-AEnv-weakening : ∀ {Γ Γ' Δ} → AEnv Γ Δ → Γ cx-≤ Γ' → AEnv Γ' Δ
lem-AEnv-weakening env[] prf = env[]
lem-AEnv-weakening (envS:: {α = α} x env) prf = envS:: (lem-impTA-weakening {α} x prf) (lem-AEnv-weakening env prf)
lem-AEnv-weakening (envD:: {Γ} σ x env) prf = envS:: (lem-impTA-weakening {Ann D σ} x prf) (lem-AEnv-weakening env (lem-cx-≤-trans (cxle-lt (strip' σ) (cxle-eq Γ)) prf))  -- non-primitive recursion... this should be fixable by extending Γ in the middle, rather than in the end

lookup : ∀ {Γ Δ α} → AEnv Γ Δ → (o : α ∈ Δ ) → impTA Γ α
lookup env[] ()
lookup (envS:: x env) hd = x
lookup (envS:: x env) (tl idx) = lookup env idx
lookup (envD:: σ x env) hd = x
lookup {α = α} (envD:: {Γ} σ x env) (tl idx) = lem-impTA-weakening {α} (lookup env idx) (strip' σ cxle-∷ Γ)

data IsDynamic : AType → Set where
  is-dyn : ∀ σ → IsDynamic (Ann D σ)

lem-IsDynamic-by-wf : ∀ α → isTrue (D ≼ btof α) → IsDynamic α
lem-IsDynamic-by-wf (Ann S σ) ()
lem-IsDynamic-by-wf (Ann D σ) _ = is-dyn σ

-- TODO: Do we need additional assurance in the type signature (or as
-- an aux. lemma) that Γ is the residue of Δ?
pe : ∀ {Δ Γ α} → AEnv Γ Δ → AExp Δ α → impTA Γ α
pe env (AVar idx) = lookup env idx
pe env (AInt S i) = i
pe env (AInt D i) = EInt i
pe {Γ = Γ} env (AFun {α₁} {α₂} S prf exp) = λ {Γ'} (prf₁ : Γ cx-≤ Γ') (v : impTA Γ' α₂) →
                                                     pe (envS:: v (lem-AEnv-weakening env prf₁)) exp
pe env (AFun {α₁} {α₂} D (wf-fun _ _ prf-2 prf-1) e)
  with lem-IsDynamic-by-wf α₁ prf-1 | lem-IsDynamic-by-wf α₂ prf-2
pe {Γ = Γ} env (AFun {.(Ann D σ₁)} {.(Ann D σ₂)} D (wf-fun _ _ prf-1 prf-2) e)
  | is-dyn σ₁ | is-dyn σ₂ =
  EFun (pe (envD:: σ₂ (EVar hd) env) e)
pe {Γ = Γ} env (AApp S _ f e) = (pe env f (cxle-eq Γ)) (pe env e)
pe env (AApp {α₁} {α₂} D (wf-fun _ _ prf-2 prf-1) f e)
  with lem-IsDynamic-by-wf α₁ prf-1 | lem-IsDynamic-by-wf α₂ prf-2
pe env (AApp {.(Ann D σ₁)}{.(Ann D σ₂)} D (wf-fun _ _ prf-2 prf-1) f e)
 | is-dyn σ₁ | is-dyn σ₂ =
 EApp (pe env f) (pe env e) -- construct an Exp-application using the proof that argument and results are dynamic and thus pe yields Exp-terms for them

max_stars_repo_name: luminousfennell/polybta

max_issues_repo_name: luminousfennell/polybta

max_forks_repo_name: luminousfennell/polybta


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Module where

open import Cubical.Algebra.Module.Base public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
module RMonads.CatofRMonads where

open import Categories
open import Functors
open import RMonads
open import RMonads.RMonadMorphs

CatofRMonads : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}(J : Fun C D) → Cat
CatofRMonads J = record
                 { Obj  = RMonad J
                 ; Hom  = RMonadMorph
                 ; iden = IdRMonadMorph _
                 ; comp = CompRMonadMorph
                 ; idl  = idl _
                 ; idr  = idr _
                 ; ass  = λ{_ _ _ _ f g h} → ass f g h
                 }

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
-- Andreas, 2014-10-09, issue reported by jesper.cockx

open import Common.Product

pattern foo x = x , x
-- Should complain about non-linearity.

test : {A : Set} → A × A → A
test (foo x) = x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Cubical.HITs.FreeComMonoids.Properties where

open import Cubical.Foundations.Everything hiding (assoc; ⟨_⟩)

open import Cubical.Data.Nat hiding (_·_ ; _^_)

open import Cubical.HITs.FreeComMonoids.Base as FCM
open import Cubical.HITs.AssocList as AL

private variable
  ℓ : Level
  A : Type ℓ

multi-· : A → ℕ → FreeComMonoid A → FreeComMonoid A
multi-· x zero xs = xs
multi-· x (suc n) xs = ⟦ x ⟧ · multi-· x n xs

_^_ : A → ℕ → FreeComMonoid A
x ^ n = multi-· x n ε

^+≡ : ∀ (p : A) m n → ((p ^ m) · (p ^ n)) ≡ (p ^ (m + n))
^+≡ p zero n = identityₗ _
^+≡ p (suc m) n = sym (assoc _ _ _) ∙ cong (_ ·_) (^+≡ _ _ _)

AL→FCM : AssocList A → FreeComMonoid A
AL→FCM = AL.Rec.f trunc ε (λ a n p → (a ^ n) · p)
  per* agg* (const identityₗ)
  where
  per* : ∀ x y (mon : FreeComMonoid A) →
    ((⟦ x ⟧ · ε) · ((⟦ y ⟧ · ε) · mon)) ≡
    ((⟦ y ⟧ · ε) · ((⟦ x ⟧ · ε) · mon))
  per* x y mon =
    (⟦ x ⟧ · ε) · ((⟦ y ⟧ · ε) · mon)
    ≡⟨ assoc _ _ _ ⟩
    ((⟦ x ⟧ · ε) · (⟦ y ⟧ · ε)) · mon
    ≡⟨ cong (_· mon) (comm _ _) ⟩
    (((⟦ y ⟧ · ε) · (⟦ x ⟧ · ε)) · mon)
    ≡⟨ sym (assoc _ _ _) ⟩
    ((⟦ y ⟧ · ε) · ((⟦ x ⟧ · ε) · mon)) ∎

  agg* : ∀ a m n mon →
      ((a ^ m) · ((a ^ n) · mon)) ≡ ((a ^ (m + n)) · mon)
  agg* a m n mon =
    ((a ^ m) · ((a ^ n) · mon))
    ≡⟨ assoc _ _ _ ⟩
    (((a ^ m) · (a ^ n)) · mon)
    ≡⟨ cong (_· _) (^+≡ _ _ _) ⟩
    ((a ^ (m + n)) · mon) ∎

FCM→AL : FreeComMonoid A → AssocList A
FCM→AL = FCM.Rec.f trunc ⟨_⟩ ⟨⟩ _++_ comm-++ unitr-++ (λ _ → refl) assoc-++

^-id : (x : A) (m : ℕ) (u : FreeComMonoid A)
  → FCM→AL ((x ^ m) · u) ≡ ⟨ x , m ⟩∷ FCM→AL u
^-id x zero u = cong FCM→AL (identityₗ u) ∙ sym (del _ _)
^-id x (suc m) u =
  FCM→AL ((⟦ x ⟧ · (x ^ m)) · u)
  ≡⟨ cong ⟨ x , 1 ⟩∷_ (^-id x m u) ⟩
  ⟨ x , 1 ⟩∷ ⟨ x , m ⟩∷ FCM→AL u
  ≡⟨ agg _ _ _ _ ⟩
  ⟨ x , suc m ⟩∷ FCM→AL u ∎

++-· : (x y : AssocList A)
  → AL→FCM (x ++ y) ≡ AL→FCM x · AL→FCM y
++-· = AL.ElimProp.f
  (isPropΠ (λ _ → trunc _ _))
  (λ _ → sym (identityₗ _))
  λ x n {xs} p ys →
  AL→FCM (((⟨ x , n ⟩∷ ⟨⟩) ++ xs) ++ ys)
  ≡⟨ cong AL→FCM (cong (_++ ys) (comm-++ (⟨ x , n ⟩∷ ⟨⟩) xs) ∙ sym (assoc-++ xs _ ys)) ⟩
  AL→FCM (xs ++ (⟨ x , n ⟩∷ ys))
  ≡⟨ p _ ⟩
  (AL→FCM xs · ((x ^ n) · AL→FCM ys))
  ≡⟨ assoc (AL→FCM xs) _ _ ⟩
  ((AL→FCM xs · (x ^ n)) · AL→FCM ys)
  ≡⟨ cong (_· AL→FCM ys) (comm _ _) ⟩
  ((x ^ n) · AL→FCM xs) · AL→FCM ys ∎

AL→FCM∘FCM→AL≡id : section {A = AssocList A} AL→FCM FCM→AL
AL→FCM∘FCM→AL≡id = FCM.ElimProp.f (trunc _ _) (λ x → identityᵣ _ ∙ identityᵣ _) refl
  λ {x y} p q → ++-· (FCM→AL x) (FCM→AL y) ∙ cong₂ _·_ p q

FCM→AL∘AL→FCM≡id : retract {A = AssocList A} AL→FCM FCM→AL
FCM→AL∘AL→FCM≡id = AL.ElimProp.f (trunc _ _) refl
  λ x n {xs} p → ^-id x n (AL→FCM xs) ∙ cong (⟨ _ , _ ⟩∷_) p

AssocList≃FreeComMonoid : AssocList A ≃ FreeComMonoid A
AssocList≃FreeComMonoid = isoToEquiv (iso AL→FCM FCM→AL AL→FCM∘FCM→AL≡id FCM→AL∘AL→FCM≡id)

AssocList≡FreeComMonoid : AssocList A ≡ FreeComMonoid A
AssocList≡FreeComMonoid = ua AssocList≃FreeComMonoid

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module CoInf where

open import Coinduction

-- Check that ∞ can be used as an "expression".
test : Set → Set
test = ∞

max_stars_repo_name: andreasabel/agda-with-old-branches

max_issues_repo_name: andersk/agda

max_forks_repo_name: andersk/agda


text:
module Structure.Operator.Monoid.Proofs where

import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Operator.Monoid
open import Structure.Operator.Properties
open import Structure.Operator.Proofs
open import Type

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:
{-# OPTIONS --without-K --safe #-}

module Categories.Bicategory.Extras where

open import Data.Product using (_,_)

open import Categories.Bicategory using (Bicategory)
open import Categories.Functor using (Functor)
open import Categories.Functor.Bifunctor using (appʳ; appˡ)
open import Categories.Functor.Bifunctor.Properties using ([_]-commute)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)

import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR

module Extras {o ℓ e t} (Bicat : Bicategory o ℓ e t) where
  open Bicategory Bicat
  private
    variable
      A B C D : Obj
      f g h i : A ⇒₁ B
      α β γ : f ⇒₂ g

  module ⊚ {A B C}          = Functor (⊚ {A} {B} {C})
  module ⊚-assoc {A B C D}  = NaturalIsomorphism (⊚-assoc {A} {B} {C} {D})
  module unitˡ {A B}        = NaturalIsomorphism (unitˡ {A} {B})
  module unitʳ {A B}        = NaturalIsomorphism (unitʳ {A} {B})
  module id {A}             = Functor (id {A})

  unitorˡ : {A B : Obj} {f : A ⇒₁ B} → Mor._≅_ (hom A B) (id₁ ∘ₕ f) f
  unitorˡ {_} {_} {f} = record
    { from = unitˡ.⇒.η (_ , f)
    ; to   = unitˡ.⇐.η (_ , f)
    ; iso  = unitˡ.iso (_ , f)
    }

  module unitorˡ {A B f} = Mor._≅_ (unitorˡ {A} {B} {f})

  unitorʳ : {A B : Obj} {f : A ⇒₁ B} → Mor._≅_ (hom A B) (f ∘ₕ id₁) f
  unitorʳ {_} {_} {f} = record
    { from = unitʳ.⇒.η (f , _)
    ; to   = unitʳ.⇐.η (f , _)
    ; iso  = unitʳ.iso (f , _)
    }

  module unitorʳ {A B f} = Mor._≅_ (unitorʳ {A} {B} {f})

  associator : {A B C D : Obj} {f : D ⇒₁ B} {g : C ⇒₁ D} {h : A ⇒₁ C} →  Mor._≅_ (hom A B) ((f ∘ₕ g) ∘ₕ h) (f ∘ₕ g ∘ₕ h)
  associator {_} {_} {_} {_} {f} {g} {h} = record
    { from = ⊚-assoc.⇒.η ((f , g) , h)
    ; to   = ⊚-assoc.⇐.η ((f , g) , h)
    ; iso  = ⊚-assoc.iso ((f , g) , h)
    }

  module associator {A B C D} {f : C ⇒₁ B} {g : D ⇒₁ C} {h} = Mor._≅_ (associator {A = A} {B = B} {f = f} {g = g} {h = h})

  -⊚_ : C ⇒₁ A → Functor (hom A B) (hom C B)
  -⊚_ = appʳ ⊚

  _⊚- : B ⇒₁ C → Functor (hom A B) (hom A C)
  _⊚- = appˡ ⊚

  identity₂ˡ : id₂ ∘ᵥ α ≈ α
  identity₂ˡ = hom.identityˡ

  identity₂ʳ : α ∘ᵥ id₂ ≈ α
  identity₂ʳ = hom.identityʳ

  assoc₂ : (α ∘ᵥ β) ∘ᵥ γ ≈ α ∘ᵥ β ∘ᵥ γ
  assoc₂ = hom.assoc

  id₂◁ : id₂ {f = g} ◁ f ≈ id₂
  id₂◁ = ⊚.identity

  ▷id₂ : f ▷ id₂ {f = g} ≈ id₂
  ▷id₂ = ⊚.identity

  open hom.HomReasoning
  open hom.Equiv
  private
    module MR′ {A} {B} where
      open MR (hom A B) using (conjugate-to) public
      open Mor (hom A B) using (module ≅) public
    open MR′

  ∘ᵥ-distr-◁ : (α ◁ f) ∘ᵥ (β ◁ f) ≈ (α ∘ᵥ β) ◁ f
  ∘ᵥ-distr-◁ {f = f} = ⟺ (Functor.homomorphism (-⊚ f))

  ∘ᵥ-distr-▷ : (f ▷ α) ∘ᵥ (f ▷ β) ≈ f ▷ (α ∘ᵥ β)
  ∘ᵥ-distr-▷ {f = f} = ⟺ (Functor.homomorphism (f ⊚-))

  ρ-∘ᵥ-▷ : unitorˡ.from ∘ᵥ (id₁ ▷ α) ≈ α ∘ᵥ unitorˡ.from
  ρ-∘ᵥ-▷ {α = α} = begin
    unitorˡ.from ∘ᵥ (id₁ ▷ α)    ≈˘⟨ hom.∘-resp-≈ʳ (⊚.F-resp-≈ (id.identity , refl)) ⟩
    unitorˡ.from ∘ᵥ id.F₁ _ ⊚₁ α ≈⟨ unitˡ.⇒.commute (_ , α) ⟩
    α ∘ᵥ unitorˡ.from            ∎

  ▷-∘ᵥ-ρ⁻¹ : (id₁ ▷ α) ∘ᵥ unitorˡ.to ≈ unitorˡ.to ∘ᵥ α
  ▷-∘ᵥ-ρ⁻¹ = conjugate-to (≅.sym unitorˡ) (≅.sym unitorˡ) ρ-∘ᵥ-▷

  λ-∘ᵥ-◁ : unitorʳ.from ∘ᵥ (α ◁ id₁) ≈ α ∘ᵥ unitorʳ.from
  λ-∘ᵥ-◁ {α = α} = begin
    unitorʳ.from ∘ᵥ (α ◁ id₁)      ≈˘⟨ hom.∘-resp-≈ʳ (⊚.F-resp-≈ (refl , id.identity)) ⟩
    unitorʳ.from ∘ᵥ (α ⊚₁ id.F₁ _) ≈⟨ unitʳ.⇒.commute (α , _) ⟩
    α ∘ᵥ unitorʳ.from              ∎

  ◁-∘ᵥ-λ⁻¹ : (α ◁ id₁) ∘ᵥ unitorʳ.to ≈ unitorʳ.to ∘ᵥ α
  ◁-∘ᵥ-λ⁻¹ = conjugate-to (≅.sym unitorʳ) (≅.sym unitorʳ) λ-∘ᵥ-◁

  assoc⁻¹-◁-∘ₕ : associator.to ∘ᵥ (α ◁ (g ∘ₕ f)) ≈ ((α ◁ g) ◁ f) ∘ᵥ associator.to
  assoc⁻¹-◁-∘ₕ {α = α} {g = g} {f = f} = begin
    associator.to ∘ᵥ (α ◁ (g ∘ₕ f))    ≈˘⟨ hom.∘-resp-≈ʳ (⊚.F-resp-≈ (refl , ⊚.identity)) ⟩
    associator.to ∘ᵥ (α ⊚₁ id₂ ⊚₁ id₂) ≈⟨ ⊚-assoc.⇐.commute ((α , id₂) , id₂) ⟩
    ((α ◁ g) ◁ f) ∘ᵥ associator.to     ∎

  assoc⁻¹-▷-◁ : associator.to ∘ᵥ (f ▷ (α ◁ g)) ≈ ((f ▷ α) ◁ g) ∘ᵥ associator.to
  assoc⁻¹-▷-◁ {f = f} {α = α} {g = g} = ⊚-assoc.⇐.commute ((id₂ , α) , id₂)

  assoc⁻¹-▷-∘ₕ : associator.to ∘ᵥ (g ▷ (f ▷ α)) ≈ ((g ∘ₕ f) ▷ α) ∘ᵥ associator.to
  assoc⁻¹-▷-∘ₕ {g = g} {f = f} {α = α} = begin
    associator.to ∘ᵥ (g ▷ (f ▷ α))       ≈⟨ ⊚-assoc.⇐.commute ((id₂ , id₂) , α) ⟩
    ((id₂ ⊚₁ id₂) ⊚₁ α) ∘ᵥ associator.to ≈⟨ hom.∘-resp-≈ˡ (⊚.F-resp-≈ (⊚.identity , refl)) ⟩
    ((g ∘ₕ f) ▷ α) ∘ᵥ associator.to      ∎

  ◁-▷-exchg : ∀ {α : f ⇒₂ g} {β : h ⇒₂ i} → (i ▷ α) ∘ᵥ (β ◁ f) ≈ (β ◁ g) ∘ᵥ (h ▷ α)
  ◁-▷-exchg = [ ⊚ ]-commute

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
open import Relation.Binary.PropositionalEquality using ( refl )
open import Web.Semantic.DL.Category.Object using ( Object )
open import Web.Semantic.DL.Category.Morphism using ( _≣_ )
open import Web.Semantic.DL.Category.Composition using ( _∙_ )
open import Web.Semantic.DL.Category.Tensor using ( _⊗_ ; _⟨⊗⟩_ )
open import Web.Semantic.DL.Category.Unit using ( I )
open import Web.Semantic.DL.Category.Wiring using
  ( identity ; symm ; assoc ; assoc⁻¹ ; unit₁ ; unit₁⁻¹ ; unit₂ ; unit₂⁻¹ )
open import Web.Semantic.DL.Category.Properties.Wiring using
  ( rewriting ; rewrite-compose ; rewrite-tensor
  ; rewrite-identity ; rewrite-symm ; rewrite-assoc ; rewrite-assoc⁻¹
  ; rewrite-unit₁ ; rewrite-unit₁⁻¹ ; rewrite-unit₂ ; rewrite-unit₂⁻¹ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.Util using ( _≡⊎≡_ )

module Web.Semantic.DL.Category.Properties.Tensor.Coherence
  {Σ : Signature} {S T : TBox Σ} where

assoc-unit : ∀ (A₁ A₂ : Object S T) →
  (assoc A₁ I A₂ ∙ (identity A₁ ⟨⊗⟩ unit₁ A₂) ≣ unit₂ A₁ ⟨⊗⟩ identity A₂)
assoc-unit A₁ A₂ = rewriting
  (rewrite-compose (rewrite-assoc A₁ I A₂)
    (rewrite-tensor (rewrite-identity A₁) (rewrite-unit₁ A₂)))
  ((λ x → refl) ≡⊎≡ (λ x → refl))
  (rewrite-tensor (rewrite-unit₂ A₁) (rewrite-identity A₂))

assoc-assoc : ∀ (A₁ A₂ A₃ A₄ : Object S T) →
  (assoc (A₁ ⊗ A₂) A₃ A₄ ∙ assoc A₁ A₂ (A₃ ⊗ A₄) ≣
    (assoc A₁ A₂ A₃ ⟨⊗⟩ identity A₄) ∙ assoc A₁ (A₂ ⊗ A₃) A₄ ∙ (identity A₁ ⟨⊗⟩ assoc A₂ A₃ A₄))
assoc-assoc A₁ A₂ A₃ A₄ = rewriting
  (rewrite-compose (rewrite-assoc (A₁ ⊗ A₂) A₃ A₄) (rewrite-assoc A₁ A₂ (A₃ ⊗ A₄)))
  ((λ x → refl) ≡⊎≡ ((λ x → refl) ≡⊎≡ ((λ x → refl) ≡⊎≡ (λ x → refl))))
  (rewrite-compose (rewrite-tensor (rewrite-assoc A₁ A₂ A₃) (rewrite-identity A₄))
    (rewrite-compose (rewrite-assoc A₁ (A₂ ⊗ A₃) A₄)
      (rewrite-tensor (rewrite-identity A₁) (rewrite-assoc A₂ A₃ A₄))))

assoc-symm : ∀ (A₁ A₂ A₃ : Object S T) →
  (symm (A₁ ⊗ A₂) A₃ ∙ assoc⁻¹ A₃ A₁ A₂ ≣
    assoc A₁ A₂ A₃ ∙ (identity A₁ ⟨⊗⟩ symm A₂ A₃) ∙ assoc⁻¹ A₁ A₃ A₂ ∙ (symm A₁ A₃ ⟨⊗⟩ identity A₂))
assoc-symm A₁ A₂ A₃ = rewriting
  (rewrite-compose (rewrite-symm (A₁ ⊗ A₂) A₃) (rewrite-assoc⁻¹ A₃ A₁ A₂))
  (((λ x → refl) ≡⊎≡ (λ x → refl)) ≡⊎≡ (λ x → refl))
  (rewrite-compose (rewrite-assoc A₁ A₂ A₃)
    (rewrite-compose (rewrite-tensor (rewrite-identity A₁) (rewrite-symm A₂ A₃))
      (rewrite-compose (rewrite-assoc⁻¹ A₁ A₃ A₂)
        (rewrite-tensor (rewrite-symm A₁ A₃) (rewrite-identity A₂)))))

symm-unit : ∀ (A : Object S T) →
  (symm A I ∙ unit₁ A ≣ unit₂ A)
symm-unit A = rewriting
  (rewrite-compose (rewrite-symm A I) (rewrite-unit₁ A))
  (λ x → refl)
  (rewrite-unit₂ A)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
module Tactic.Reflection.Substitute where

open import Prelude hiding (abs)
open import Builtin.Reflection
open import Tactic.Reflection.DeBruijn

patternArgsVars : List (Arg Pattern) → Nat

patternVars : Pattern → Nat
patternVars (con _ ps) = patternArgsVars ps
patternVars dot = 1
patternVars (var _) = 1
patternVars (lit x) = 0
patternVars (proj _) = 0
patternVars absurd = 0

patternArgsVars [] = 0
patternArgsVars (arg _ p ∷ ps) = patternVars p + patternArgsVars ps

IsSafe : Term → Set
IsSafe (lam _ _) = ⊥
IsSafe _ = ⊤

data SafeTerm : Set where
  safe : (v : Term) (p : IsSafe v) → SafeTerm

maybeSafe : Term → Maybe SafeTerm
maybeSafe (var x args) = just (safe (var x args) _)
maybeSafe (con c args) = just (safe (con c args) _)
maybeSafe (def f args) = just (safe (def f args) _)
maybeSafe (meta x args) = just (safe (meta x args) _)
maybeSafe (lam v t) = nothing
maybeSafe (pat-lam cs args) = just (safe (pat-lam cs args) _)
maybeSafe (pi a b) = just (safe (pi a b) _)
maybeSafe (agda-sort s) = just (safe (agda-sort s) _)
maybeSafe (lit l) = just (safe (lit l) _)
maybeSafe unknown = just (safe unknown _)

instance
  DeBruijnSafeTerm : DeBruijn SafeTerm
  strengthenFrom {{DeBruijnSafeTerm}} k n (safe v _) = do
    -- Strengthening or weakening safe terms always results in safe terms,
    -- but proving that is a bit of a bother, thus maybeSafe.
    v₁ ← strengthenFrom k n v
    maybeSafe v₁
  weakenFrom {{DeBruijnSafeTerm}} k n (safe v p) =
    maybe (safe unknown _) id (maybeSafe (weakenFrom k n v))

safe-term : SafeTerm → Term
safe-term (safe v _) = v

applyTerm : SafeTerm → List (Arg Term) → Term
applyTerm v [] = safe-term v
applyTerm (safe (var x args) _) args₁ = var x (args ++ args₁)
applyTerm (safe (con c args) _) args₁ = con c (args ++ args₁)
applyTerm (safe (def f args) _) args₁ = def f (args ++ args₁)
applyTerm (safe (meta x args) _) args₁ = meta x (args ++ args₁)
applyTerm (safe (lam v t) ()) args
applyTerm (safe (pat-lam cs args) _) args₁ = pat-lam cs (args ++ args₁)
applyTerm (safe (pi a b) _) _ = pi a b
applyTerm (safe (agda-sort s) _) _ = agda-sort s
applyTerm (safe (lit l) _)  _ = lit l
applyTerm (safe unknown _) _ = unknown

Subst : Set → Set
Subst A = List SafeTerm → A → A

substTerm : Subst Term
substArgs : Subst (List (Arg Term))
substArg : Subst (Arg Term)
substAbs : Subst (Abs Term)
substSort : Subst Sort
substClauses : Subst (List Clause)
substClause : Subst Clause

substTerm σ (var x args) =
  case index σ x of λ
  { nothing  → var (x - length σ) (substArgs σ args)
  ; (just v) → applyTerm v (substArgs σ args) }
substTerm σ (con c args) = con c (substArgs σ args)
substTerm σ (def f args) = def f (substArgs σ args)
substTerm σ (meta x args) = meta x (substArgs σ args)
substTerm σ (lam v b) = lam v (substAbs σ b)
substTerm σ (pat-lam cs args) = pat-lam (substClauses σ cs) (substArgs σ args)
substTerm σ (pi a b) = pi (substArg σ a) (substAbs σ b)
substTerm σ (agda-sort s) = agda-sort (substSort σ s)
substTerm σ (lit l) = lit l
substTerm σ unknown = unknown

substSort σ (set t) = set (substTerm σ t)
substSort σ (lit n) = lit n
substSort σ unknown = unknown

substClauses σ [] = []
substClauses σ (c ∷ cs) = substClause σ c ∷ substClauses σ cs

substClause σ (clause ps b) =
  case patternArgsVars ps of λ
  { zero    → clause ps (substTerm σ b)
  ; (suc n) → clause ps (substTerm (reverse (map (λ i → safe (var i []) _) (from 0 to n)) ++ weaken (suc n) σ) b)
  }
substClause σ (absurd-clause ps) = absurd-clause ps

substArgs σ [] = []
substArgs σ (x ∷ args) = substArg σ x ∷ substArgs σ args
substArg σ (arg i x) = arg i (substTerm σ x)
substAbs σ (abs x v) = abs x $ substTerm (safe (var 0 []) _ ∷ weaken 1 σ) v

private
  toArgs : Nat → List (Arg SafeTerm) → List (Arg Term)
  toArgs k = map (λ x → weaken k (fmap safe-term x))

  SafeApplyType : Set → Set
  SafeApplyType A = List SafeTerm → Nat → A → List (Arg SafeTerm) → A

  safeApplyAbs : SafeApplyType (Abs Term)
  safeApplyArg : SafeApplyType (Arg Term)
  safeApplySort : SafeApplyType Sort

  -- safeApply′ env |Θ| v args = v′
  --   where Γ, Δ, Θ ⊢ v
  --         Γ ⊢ env : Δ
  --         Γ ⊢ args
  --         Γ, Θ ⊢ v′
  safeApply′ : List SafeTerm → Nat → Term → List (Arg SafeTerm) → Term
  safeApply′ env k (var x args) args₁ =
    if x <? k then var x (args ++ toArgs k args₁)
              else case index env (x - k) of λ
                   { nothing  → var (x - length env) (args ++ toArgs k args₁)
                   ; (just v) → applyTerm v (args ++ toArgs k args₁) }
  safeApply′ env k (con c args)      args₁      = con c (args ++ toArgs k args₁)
  safeApply′ env k (def f args)      args₁      = def f (args ++ toArgs k args₁)
  safeApply′ env k (lam v t)        (a ∷ args₁) = safeApply′ (unArg a ∷ env) k (unAbs t) args₁
  safeApply′ env k (lam v b)         []         = lam v $ safeApplyAbs env k b []
  safeApply′ env k (pat-lam cs args) args₁      = pat-lam cs (args ++ toArgs k args₁)
                                                  -- not right if applying to constructors
  safeApply′ env k (pi a b)          _          = pi (safeApplyArg env k a []) (safeApplyAbs env k b [])
  safeApply′ env k (agda-sort s)     args₁      = agda-sort (safeApplySort env k s [])
  safeApply′ env k (lit l)           args₁      = lit l
  safeApply′ env k (meta x args)     args₁      = meta x (args ++ toArgs k args₁)
  safeApply′ env k unknown           args₁      = unknown

  safeApplyAbs env k (abs x b) _ = abs x (safeApply′ env (suc k) b [])
  safeApplyArg env k (arg i v) args₁ = arg i (safeApply′ env k v args₁)

  safeApplySort env k (set t) _ = set (safeApply′ env k t [])
  safeApplySort env k (lit n) _ = lit n
  safeApplySort env k unknown _ = unknown

safeApply : Term → List (Arg SafeTerm) → Term
safeApply v args = safeApply′ [] 0 v args

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module _ where

{-# BUILTIN INTERVAL I #-}


text:
import Oscar.Class.Reflexivity.Function
import Oscar.Class.Transextensionality.Proposequality -- FIXME why not use the instance here?
open import Oscar.Class
open import Oscar.Class.Category
open import Oscar.Class.HasEquivalence
open import Oscar.Class.IsCategory
open import Oscar.Class.IsPrecategory
open import Oscar.Class.Precategory
open import Oscar.Class.Reflexivity
open import Oscar.Class.Transassociativity
open import Oscar.Class.Transextensionality
open import Oscar.Class.Transitivity
open import Oscar.Class.Transleftidentity
open import Oscar.Class.Transrightidentity
open import Oscar.Class.[IsExtensionB]
open import Oscar.Data.Proposequality
open import Oscar.Prelude
open import Oscar.Property.Category.Function
open import Oscar.Property.Setoid.Proposextensequality

module Oscar.Property.Category.ExtensionProposextensequality where

module _
  {a} {A : Ø a} {b} {B : A → Ø b}
  where

  instance

    𝓣ransassociativityExtensionProposextensequality : Transassociativity.class (Extension B) Proposextensequality transitivity
    𝓣ransassociativityExtensionProposextensequality .⋆ _ _ _ _ = !

module _
  {a} {A : Ø a} {b} {B : A → Ø b}
  where

  instance

    𝓣ransextensionalityExtensionProposextensequality : Transextensionality.class (Extension B) Proposextensequality transitivity
    𝓣ransextensionalityExtensionProposextensequality .⋆ = 𝓣ransextensionalityFunctionProposextensequality .⋆
    -- 𝓣ransextensionalityExtensionProposextensequality .⋆ {f₂ = f₂} f₁≡̇f₂ g₁≡̇g₂ x rewrite f₁≡̇f₂ x = g₁≡̇g₂ (f₂ x) -- FIXME using this causes problems in Test.Functor

module _
  {a} {A : Ø a} {b} {B : A → Ø b}
  where

  instance

    𝓣ransleftidentityExtensionProposextensequality : Transleftidentity.class (Extension B) Proposextensequality ε transitivity
    𝓣ransleftidentityExtensionProposextensequality .⋆ _ = !

module _
  {a} {A : Ø a} {b} {B : A → Ø b}
  where

  instance

    𝓣ransrightidentityExtensionProposextensequality : Transrightidentity.class (Extension B) Proposextensequality ε transitivity
    𝓣ransrightidentityExtensionProposextensequality .⋆ _ = !

module _
  {a} {A : Ø a} {b} {B : A → Ø b}
  where

  instance

    HasEquivalenceExtension : ∀ {x y : A} ⦃ _ : [IsExtensionB] B ⦄ → HasEquivalence (Extension B x y) _
    HasEquivalenceExtension = ∁ Proposextensequality

module _
  {a} {A : Ø a} {b} {B : A → Ø b}
  where

  instance

    IsPrecategoryExtension : IsPrecategory (Extension B) Proposextensequality transitivity
    IsPrecategoryExtension = ∁

    IsCategoryExtension : IsCategory (Extension B) Proposextensequality ε transitivity
    IsCategoryExtension = ∁

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

  PrecategoryExtension : Precategory _ _ _
  PrecategoryExtension = ∁ (Extension B) Proposextensequality transitivity

  CategoryExtension : Category _ _ _
  CategoryExtension = ∁ (Extension B) Proposextensequality ε transitivity


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

open import lib.Basics
open import lib.NType2
open import lib.Equivalences2
open import lib.NConnected
open import lib.types.Nat
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.TLevel
open import lib.types.Truncation
open import lib.types.Group
open import lib.types.Pointed
open import lib.types.LoopSpace
open import lib.groups.Homomorphisms
open import lib.groups.HomotopyGroup

module lib.types.EilenbergMacLane1 where

module EM₁ {i} (G : Group i) where

  module G = Group G

  private
    data #EM₁-aux : Type i where
      #embase : #EM₁-aux

    data #EM₁ : Type i where
      #em₁ : #EM₁-aux → (Unit → Unit) → #EM₁

  EM₁ : Type i
  EM₁ = #EM₁

  embase : EM₁
  embase = #em₁ #embase _

  ⊙EM₁ : Ptd i
  ⊙EM₁ = ⊙[ EM₁ , embase ]

  postulate  -- HIT
    emlevel : has-level ⟨ 1 ⟩ EM₁
    emloop : G.El → embase == embase
    emloop-ident : emloop G.ident == idp
    emloop-comp : ∀ g₁ g₂ → emloop (G.comp g₁ g₂) == emloop g₁ ∙ emloop g₂

  module EM₁Rec {j} {C : Type j}
    (C-level : has-level ⟨ 1 ⟩ C)
    (embase* : C)
    (hom* : G →ᴳ (Ω^S-group 0 (C , embase*) C-level)) where

    f : EM₁ → C
    f (#em₁ #embase _) = embase*

    postulate  -- HIT
      emloop-β : (g : G.El) → ap f (emloop g) == GroupHom.f hom* g

  open EM₁Rec public using () renaming (f to EM₁-rec)

  module EM₁Elim {j} {P : EM₁ → Type j}
    (P-level : (x : EM₁) → has-level ⟨ 1 ⟩ (P x))
    (embase* : P embase)
    (emloop* : (g : G.El) → embase* == embase* [ P ↓ emloop g ])
    (preserves-ident : emloop* G.ident == idp
       [ (λ p → embase* == embase* [ P ↓ p ]) ↓ emloop-ident ])
    (preserves-comp : (g₁ g₂ : G.El) →
       emloop* (G.comp g₁ g₂) == emloop* g₁ ∙ᵈ emloop* g₂
       [ (λ p → embase* == embase* [ P ↓ p ]) ↓ emloop-comp g₁ g₂ ])
    where

    f : Π EM₁ P
    f (#em₁ #embase _) = embase*

    postulate  -- HIT
      emloop-β : (g : G.El) → apd f (emloop g) == emloop* g

  open EM₁Elim public using () renaming (f to EM₁-elim)

  emloop-inv : ∀ g → emloop (G.inv g) == ! (emloop g)
  emloop-inv g = cancels-inverse _ _ lemma
    where
      cancels-inverse : ∀ {i} {A : Type i} {x y : A}
        (p : x == y) (q : y == x) → p ∙ q == idp → p == ! q
      cancels-inverse p idp r = ! (∙-unit-r p) ∙ r

      lemma : emloop (G.inv g) ∙ emloop g  == idp
      lemma = ! (emloop-comp (G.inv g) g) ∙ ap emloop (G.invl g) ∙ emloop-ident

  module π₁ where

    comp-equiv : ∀ g → G.El ≃ G.El
    comp-equiv g = equiv
      (λ x → G.comp x g)
      (λ x → G.comp x (G.inv g))
      (λ x → G.assoc x (G.inv g) g ∙ ap (G.comp x) (G.invl g) ∙ G.unitr x)
      (λ x → G.assoc x g (G.inv g) ∙ ap (G.comp x) (G.invr g) ∙ G.unitr x)

    comp-equiv-id : comp-equiv G.ident == ide G.El
    comp-equiv-id =
      pair= (λ= G.unitr)
            (prop-has-all-paths-↓ {B = is-equiv} (is-equiv-is-prop $ idf G.El))

    comp-equiv-comp : (g₁ g₂ : G.El) → comp-equiv (G.comp g₁ g₂)
                      == (comp-equiv g₂ ∘e comp-equiv g₁)
    comp-equiv-comp g₁ g₂ =
      pair= (λ= (λ x → ! (G.assoc x g₁ g₂)))
            (prop-has-all-paths-↓ {B = is-equiv} (is-equiv-is-prop _))

    Ω-group : Group (lsucc i)
    Ω-group = group (G.El == G.El) (universe-=-level G.El-level G.El-level)
                    (Ω^S-group-structure 0 (Type i , G.El))

    0-group : Group (lsucc i)
    0-group = Ω^S-group 0
      ((0 -Type i) , (G.El , G.El-level)) (0 -Type-level i)

    Codes-hom₁ : G →ᴳ Ω-group
    Codes-hom₁ = record {
      f = ua ∘ comp-equiv;

      pres-comp = λ g₁ g₂ →
        ua (comp-equiv (G.comp g₁ g₂))
          =⟨ ap ua (comp-equiv-comp g₁ g₂) ⟩
        ua (comp-equiv g₂ ∘e comp-equiv g₁)
          =⟨ ua-∘e (comp-equiv g₁) (comp-equiv g₂) ⟩
        ua (comp-equiv g₁) ∙ ua (comp-equiv g₂) ∎}

    Codes-hom₂ : Ω-group →ᴳ 0-group
    Codes-hom₂ = record {
      f = λ p → pair= p (phap p);

      pres-comp = λ p₁ p₂ →
        pair= (p₁ ∙ p₂) (phap (p₁ ∙ p₂))
          =⟨ prop-has-all-paths (↓-level (λ _ →
                                   raise-level _ has-level-is-prop)) _ _
              |in-ctx (λ w → pair= (p₁ ∙ p₂)  w) ⟩
        pair= (p₁ ∙ p₂) (phap p₁ ∙ᵈ phap p₂)
          =⟨ ! (Σ-∙ (phap p₁) (phap p₂)) ⟩
        pair= p₁ (phap p₁) ∙ pair= p₂ (phap p₂) ∎}

      where
      -- saving some space
      phap : (p : G.El == G.El)
        → G.El-level == G.El-level [ has-level 0 ↓ p ]
      phap p = prop-has-all-paths-↓ has-level-is-prop

    Codes-hom : G →ᴳ 0-group
    Codes-hom = Codes-hom₂ ∘ᴳ Codes-hom₁

    Codes : EM₁ → 0 -Type i
    Codes = EM₁-rec {C = 0 -Type i} (0 -Type-level i)
                    (G.El , G.El-level)
                    Codes-hom

    abstract
      ↓-Codes-loop : ∀ g g' → g' == G.comp g' g [ fst ∘ Codes ↓ emloop g ]
      ↓-Codes-loop g g' =
        ↓-ap-out fst Codes (emloop g) $
        ↓-ap-out (idf _) fst (ap Codes (emloop g)) $
        transport (λ w → g' == G.comp g' g [ idf _ ↓ ap fst w ])
                  (! (EM₁Rec.emloop-β (0 -Type-level i)
                                     (G.El , G.El-level) Codes-hom g)) $
        transport (λ w → g' == G.comp g' g [ idf _ ↓ w ])
                  (! (fst=-β (ua $ comp-equiv g) _)) $
        ↓-idf-ua-in (comp-equiv g) idp

    encode : {x : EM₁} → embase == x → fst (Codes x)
    encode α = transport (fst ∘ Codes) α G.ident

    encode-emloop : ∀ g → encode (emloop g) == g
    encode-emloop g = to-transp $
      transport (λ x → G.ident == x [ fst ∘ Codes ↓ emloop g ])
                 (G.unitl g) (↓-Codes-loop g G.ident)

    decode : {x : EM₁} → fst (Codes x) → embase == x
    decode {x} =
      EM₁-elim {P = λ x' → fst (Codes x') → embase == x'}
        (λ _ → Π-level (λ _ → =-preserves-level _ emlevel))
        emloop
        loop'
        (prop-has-all-paths-↓ (Π-level (λ _ → emlevel _ _) _ _))
        (λ _ _ → prop-has-all-paths-↓ (↓-level (λ _ → Π-level (λ _ → emlevel _ _))))
        x
      where
      loop' : (g : G.El)
        → emloop == emloop [ (λ x' → fst (Codes x') → embase == x') ↓ emloop g ]
      loop' g = ↓-→-from-transp $ λ= $ λ y →
        transport (λ z → embase == z) (emloop g) (emloop y)
          =⟨ trans-pathfrom (emloop g) (emloop y) ⟩
        emloop y ∙ emloop g
          =⟨ ! (emloop-comp y g) ⟩
        emloop (G.comp y g)
          =⟨ ap emloop (! (to-transp (↓-Codes-loop g y))) ⟩
        emloop (transport (λ z → fst (Codes z)) (emloop g) y) ∎

    decode-encode : ∀ {x} (α : embase == x) → decode (encode α) == α
    decode-encode idp = emloop-ident

    abstract
      Ω¹-equiv : (embase == embase) ≃ G.El
      Ω¹-equiv = equiv encode emloop encode-emloop decode-encode

    abstract
      Ω¹-path : (embase == embase) == G.El
      Ω¹-path = ua Ω¹-equiv

    abstract
      π₁-path : Trunc 0 (embase == embase) == G.El
      π₁-path = ap (Trunc 0) Ω¹-path ∙ ua (unTrunc-equiv G.El G.El-level)

    abstract
      π₁-iso : πS 0 (EM₁ , embase) == G
      π₁-iso = ! $ group-ua
        (record { f = [_] ∘ emloop;
                  pres-comp = λ g₁ g₂ → ap [_] (emloop-comp g₁ g₂) } ,
         snd ((unTrunc-equiv (embase == embase) (emlevel _ _))⁻¹
              ∘e (Ω¹-equiv ⁻¹)))

  {- EM₁ is 0-connected -}
  abstract
    EM₁-conn : is-connected 0 EM₁
    EM₁-conn = ([ embase ] , Trunc-elim (λ _ → =-preserves-level _ Trunc-level)
      (EM₁-elim
        {P = λ x → [ embase ] == [ x ]}
        (λ _ → raise-level _ (=-preserves-level _ Trunc-level))
        idp
        (λ _ → prop-has-all-paths-↓ (Trunc-level {n = 0} _ _))
        (set-↓-has-all-paths-↓ (=-preserves-level _ Trunc-level))
        (λ _ _ → set-↓-has-all-paths-↓ (=-preserves-level _ Trunc-level))))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module Issue1362 where

open import Common.Prelude
open import Common.Equality
open import Common.Reflection

module M₁ (A₁ : Set) where

  data D (B : Set) : Set where

  type₁ : TC Type
  type₁ = getType (quote D)

module M₂ (A₂ : Set) where

  open M₁ A₂

  type₂ : TC Type
  type₂ = getType (quote D)

open M₁ Nat
open M₂ Nat

foo : type₁ ≡ type₂
foo = cong getType {quote D} {quote D} ?

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 HoTT
open import cohomology.Exactness
open import cohomology.FunctionOver

module cohomology.ProductRepr where

{- Given the following commutative diagram of homomorphisms,

       H₁  i₁  i₂  H₂
          ↘     ↙
    id ↓     G     ↓ id
           ↙   ↘
       H₁ j₁   j₂  H₂

 - there exists an isomorphism G == H₁ × H₂ such that i₁,i₂ correspond
 - to the natural injections and j₁,j₂ correspond to the natural
 - projections. -}

module ProductRepr {i j}
  {G : Group (lmax i j)} {H₁ : Group i} {H₂ : Group j}
  (i₁ : H₁ →ᴳ G) (i₂ : H₂ →ᴳ G) (j₁ : G →ᴳ H₁) (j₂ : G →ᴳ H₂)
  (p₁ : ∀ h₁ → GroupHom.f j₁ (GroupHom.f i₁ h₁) == h₁)
  (p₂ : ∀ h₂ → GroupHom.f j₂ (GroupHom.f i₂ h₂) == h₂)
  (ex₁ : is-exact (GroupHom.⊙f i₁) (GroupHom.⊙f j₂))
  (ex₂ : is-exact (GroupHom.⊙f i₂) (GroupHom.⊙f j₁))
  where

  zero-ker : (g : Group.El G)
    → GroupHom.f (×ᴳ-hom-in j₁ j₂) g == Group.ident (H₁ ×ᴳ H₂)
    → g == Group.ident G
  zero-ker g q = Trunc-rec (Group.El-level G _ _)
      (lemma g (fst×= q))
      (ktoi ex₁ g (snd×= q))
    where
    lemma : (g : Group.El G) (r : GroupHom.f j₁ g == Group.ident H₁)
      → Σ (Group.El H₁) (λ h → GroupHom.f i₁ h == g)
      → g == Group.ident G
    lemma ._ r (h , idp) =
      ap (GroupHom.f i₁) (! (p₁ h) ∙ r) ∙ GroupHom.pres-ident i₁

  β₁ : (h₁ : Group.El H₁) (h₂ : Group.El H₂)
    → GroupHom.f j₁ (Group.comp G (GroupHom.f i₁ h₁) (GroupHom.f i₂ h₂)) == h₁
  β₁ h₁ h₂ =
    GroupHom.pres-comp j₁ (GroupHom.f i₁ h₁) (GroupHom.f i₂ h₂)
    ∙ ap2 (Group.comp H₁) (p₁ h₁) (itok ex₂ _ [ h₂ , idp ])
    ∙ Group.unitr H₁ h₁

  β₂ : (h₁ : Group.El H₁) (h₂ : Group.El H₂)
    → GroupHom.f j₂ (Group.comp G (GroupHom.f i₁ h₁) (GroupHom.f i₂ h₂)) == h₂
  β₂ h₁ h₂ =
    GroupHom.pres-comp j₂ (GroupHom.f i₁ h₁) (GroupHom.f i₂ h₂)
    ∙ ap2 (Group.comp H₂) (itok ex₁ _ [ h₁ , idp ]) (p₂ h₂)
    ∙ Group.unitl H₂ h₂

  iso : G == H₁ ×ᴳ H₂
  iso = surj-inj-= (×ᴳ-hom-in j₁ j₂)
    (zero-kernel-injective (×ᴳ-hom-in j₁ j₂) zero-ker)
    (λ {(h₁ , h₂) → [ Group.comp G (GroupHom.f i₁ h₁) (GroupHom.f i₂ h₂) ,
                      pair×= (β₁ h₁ h₂) (β₂ h₁ h₂) ]})

  fst-over : j₁ == ×ᴳ-fst [ (λ U → U →ᴳ H₁) ↓ iso ]
  fst-over = domain-over-iso _ _ _ _ $ domain-over-equiv fst _

  snd-over : j₂ == ×ᴳ-snd {G = H₁} [ (λ U → U →ᴳ H₂) ↓ iso ]
  snd-over = domain-over-iso _ _ _ _ $ domain-over-equiv snd _

  inl-over : i₁ == ×ᴳ-inl [ (λ V → H₁ →ᴳ V) ↓ iso ]
  inl-over = codomain-over-iso _ _ _ _ $
    codomain-over-equiv (GroupHom.f i₁) _
    ▹ λ= (λ h₁ → pair×= (p₁ h₁) (itok ex₁ _ [ h₁ , idp ]))

  inr-over : i₂ == ×ᴳ-inr {G = H₁} [ (λ V → H₂ →ᴳ V) ↓ iso ]
  inr-over = codomain-over-iso _ _ _ _ $
    codomain-over-equiv (GroupHom.f i₂) _
    ▹ λ= (λ h₂ → pair×= (itok ex₂ _ [ h₂ , idp ]) (p₂ h₂))

  {- Given additionally maps

            i₀    j₀
         K –––→ G ––→ L

   - such that j₀∘i₀ = 0, we have j₀(i₁(j₁(i₀ k)))⁻¹ = j₀(i₂(j₂(i₀ k))).
   - (This is called the hexagon lemma in Eilenberg & Steenrod's book.
   - The hexagon is not visible in this presentation.)
   -}

  module HexagonLemma {k l}
    {K : Group k} {L : Group l}
    (i₀ : K →ᴳ G) (j₀ : G →ᴳ L)
    (ex₀ : ∀ g → GroupHom.f j₀ (GroupHom.f i₀ g) == Group.ident L)
    where

    decomp : ∀ g → Group.comp G (GroupHom.f i₁ (GroupHom.f j₁ g))
                                (GroupHom.f i₂ (GroupHom.f j₂ g))
                   == g
    decomp = transport
      (λ {(G' , i₁' , i₂' , j₁' , j₂') → ∀ g →
         Group.comp G' (GroupHom.f i₁' (GroupHom.f j₁' g))
                       (GroupHom.f i₂' (GroupHom.f j₂' g))
         == g})
      (! (pair= iso (↓-×-in inl-over (↓-×-in inr-over
                                             (↓-×-in fst-over snd-over)))))
      (λ {(h₁ , h₂) → pair×= (Group.unitr H₁ h₁) (Group.unitl H₂ h₂)})

    cancel : ∀ k →
      Group.comp L (GroupHom.f (j₀ ∘ᴳ i₁ ∘ᴳ j₁ ∘ᴳ i₀) k)
                   (GroupHom.f (j₀ ∘ᴳ i₂ ∘ᴳ j₂ ∘ᴳ i₀) k)
      == Group.ident L
    cancel k = ! (GroupHom.pres-comp j₀ _ _)
             ∙ ap (GroupHom.f j₀) (decomp (GroupHom.f i₀ k))
             ∙ ex₀ k

    inv₁ : ∀ k → Group.inv L (GroupHom.f (j₀ ∘ᴳ i₁ ∘ᴳ j₁ ∘ᴳ i₀) k)
              == GroupHom.f (j₀ ∘ᴳ i₂ ∘ᴳ j₂ ∘ᴳ i₀) k
    inv₁ k = group-inv-unique-r L _ _ (cancel k)

    inv₂ : ∀ k → Group.inv L (GroupHom.f (j₀ ∘ᴳ i₂ ∘ᴳ j₂ ∘ᴳ i₀) k)
              == GroupHom.f (j₀ ∘ᴳ i₁ ∘ᴳ j₁ ∘ᴳ i₀) k
    inv₂ k = group-inv-unique-l L _ _ (cancel k)

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The unit type and the total relation on unit
------------------------------------------------------------------------

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

open import Agda.Builtin.Equality using (_≡_)

module Data.Unit.Base where

------------------------------------------------------------------------
-- A unit type defined as a record type

-- Note that by default the unit type is not universe polymorphic as it
-- often results in unsolved metas. See `Data.Unit.Polymorphic` for a
-- universe polymorphic variant.

-- Note also that the name of this type is "\top", not T.

open import Agda.Builtin.Unit public
  using (⊤; tt)

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

-- Version 1.2

record _≤_ (x y : ⊤) : Set where
{-# WARNING_ON_USAGE _≤_
"Warning: _≤_ was deprecated in v1.2.
Please use _≡_ from Relation.Binary.PropositionalEquality instead."
#-}


text:
module _ where

import Imports.Issue1913-M as M

module _ where

  import Imports.Issue1913-I as I

  accepted₁ : M.D
  accepted₁ = I.x

! : ⦃ _ : M.D ⦄ → M.D
! ⦃ x ⦄ = x

accepted₂ : M.D
accepted₂ = !

-- rejected : M.D
-- rejected = I.x


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

open import Types
open import Functions
open import Paths
open import HLevel
open import Equivalences

module FiberEquivalences {i j k} {A : Set i} {P : A → Set k} {Q : A → Set j}
  (f : (x : A) → (P x → Q x)) where

-- We want to prove that if [f] induces an equivalence on the total spaces,
-- then [f] induces an equivalence fiberwise

total-map : Σ A P → Σ A Q
total-map (x , y) = (x , f x y)

module TotalMapEquiv (e : is-equiv total-map) where

  total-equiv : Σ A P ≃ Σ A Q
  total-equiv = (total-map , e)

  -- The inverse is propositionally fiberwise
  base-path-inverse : (x : A) (y : Q x) → π₁ ((total-equiv ⁻¹) ☆ (x , y)) ≡ x
  base-path-inverse x y = base-path (inverse-right-inverse total-equiv (x , y))

  -- And the action of [total-map] on paths is correct on the base path
  total-map-fiberwise-on-paths : {u v : Σ A P} (p : u ≡ v)
    → base-path (ap total-map p) ≡ base-path p
  total-map-fiberwise-on-paths {u} {.u} refl = refl

  -- Here is the fiberwise inverse, we use the inverse of the total map and
  -- transform it into a fiberwise map using [base-path-inverse]
  inv : ((x : A) → (Q x → P x))
  inv x y = transport P (base-path-inverse x y)
                        (π₂ ((total-equiv ⁻¹) ☆ (x , y)))

  -- We prove that [inv] is a right and left inverse to [f]

  inv-right-inverse : (x : A) (y : Q x) → f x (inv x y) ≡ y
  inv-right-inverse x y =
    app-trans _ _ f (base-path (inverse-right-inverse total-equiv (x , y)))
              (π₂ (inverse (_ , e) (x , y)))
    ∘ fiber-path (inverse-right-inverse total-equiv (x , y))

  inv-left-inverse : (x : A) (y : P x) → inv x (f x y) ≡ y
  inv-left-inverse x y =
    ap (λ u → transport P (base-path (inverse-right-inverse total-equiv
                                                             (x , f x y))) u)
        (lemma2 x y)
    ∘ (! (trans-concat P (base-path (inverse-right-inverse total-equiv
                                                                 (x , f x y)))
                               (! (base-path-inverse x (f x y))) y)
    ∘ ap (λ p → transport P p y)
          (opposite-left-inverse (ap π₁
            (inverse-right-inverse total-equiv (x , f x y))))) where

    lemma1 : (x : A) (y : P x)
      → base-path-inverse x (f x y)
        ≡ base-path (inverse-left-inverse total-equiv (x , y))
    lemma1 x y = ap base-path (inverse-triangle total-equiv (x , y))
                 ∘ total-map-fiberwise-on-paths _

    lemma2 : (x : A) (y : P x)
      → π₂ ((total-equiv ⁻¹) ☆ (x , f x y))
        ≡ transport P (! (base-path-inverse x (f x y))) y
    lemma2 x y = ! (fiber-path (! (inverse-left-inverse total-equiv (x , y))))
      ∘ ap (λ p → transport P p y)
            (ap-opposite π₁ (inverse-left-inverse total-equiv (x , y))
            ∘ ! (ap ! (lemma1 x y)))

  fiberwise-is-equiv : ((x : A) → is-equiv (f x))
  fiberwise-is-equiv x = iso-is-eq (f x) (inv x) (inv-right-inverse x)
                                              (inv-left-inverse x)

fiberwise-is-equiv : is-equiv total-map → ((x : A) → is-equiv (f x))
fiberwise-is-equiv = TotalMapEquiv.fiberwise-is-equiv

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Syntax definitions.
------------------------------------------------------------------------------

open import Data.Nat using ( ℕ )

module Data.PropFormula.Syntax ( n : ℕ ) where

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

open import Data.Bool
  renaming ( _∧_ to _&&_; _∨_ to _||_ )
  using    ( Bool; true; false; not )

open import Data.Fin  using ( Fin; #_ )
open import Data.List using ( List ; [] ; _∷_ ; _++_ ; [_] )
open import Relation.Binary.PropositionalEquality
  using ( _≡_; refl; cong; trans; sym; subst)

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

-- Proposition data type.

data PropFormula : Set where
  Var              : Fin n → PropFormula
  ⊤                : PropFormula
  ⊥                : PropFormula
  _∧_ _∨_ _⊃_ _⇔_  : (φ ψ : PropFormula) → PropFormula
  ¬_               : (φ : PropFormula)   → PropFormula

infix  11 ¬_
infixl 8 _∧_ _∨_
infixr 7 _⊃_ _⇔_

-- Context is a list (set) of hypotesis and axioms.

Ctxt : Set
Ctxt = List PropFormula

infixl 5 _,_
_,_ : Ctxt → PropFormula → Ctxt
Γ , φ = Γ ++ [ φ ]

∅ : Ctxt
∅ = []

infix 30 _⨆_
_⨆_ : Ctxt → Ctxt → Ctxt
Γ ⨆ Δ = Γ ++ Δ

infix 4 _∈_
data _∈_ (φ : PropFormula) : Ctxt → Set where
  here   : ∀ {Γ} → φ ∈ Γ , φ
  there  : ∀ {Γ} → (ψ : PropFormula) → φ ∈ Γ → φ ∈ Γ , ψ
  ⨆-ext  : ∀ {Γ} → (Δ : Ctxt) → φ ∈ Γ → φ ∈ Γ ⨆ Δ

_⊆_ : Ctxt → Ctxt → Set
Γ ⊆ Η = ∀ {φ} → φ ∈ Γ → φ ∈ Η

------------------------------------------------------------------------
-- Theorem data type.

infix 3 _⊢_

data _⊢_ : Ctxt → PropFormula → Set where

-- Hyp.

  assume   : ∀ {Γ} → (φ : PropFormula)      → Γ , φ ⊢ φ

  axiom    : ∀ {Γ} → (φ : PropFormula)      → φ ∈ Γ
                                            → Γ ⊢ φ

  weaken   : ∀ {Γ} {φ} → (ψ : PropFormula)  → Γ ⊢ φ
                                            → Γ , ψ ⊢ φ

  weaken₂   : ∀ {Γ} {φ} → (ψ : PropFormula) → Γ ⊢ φ
                                            → ψ ∷ Γ ⊢ φ
-- Top and Bottom.

  ⊤-intro  : ∀ {Γ}                          → Γ ⊢ ⊤

  ⊥-elim   : ∀ {Γ} → (φ : PropFormula)      → Γ ⊢ ⊥
                                            → Γ ⊢ φ
-- Negation.

  ¬-intro  : ∀ {Γ} {φ}                      → Γ , φ ⊢ ⊥
                                            → Γ ⊢ ¬ φ

  ¬-elim   : ∀ {Γ} {φ}                      → Γ ⊢ ¬ φ → Γ ⊢ φ
                                            → Γ ⊢ ⊥
-- Conjunction.

  ∧-intro  : ∀ {Γ} {φ ψ}                    → Γ ⊢ φ → Γ ⊢ ψ
                                            → Γ ⊢ φ ∧ ψ

  ∧-proj₁  : ∀ {Γ} {φ ψ}                    → Γ ⊢ φ ∧ ψ
                                            → Γ ⊢ φ

  ∧-proj₂  : ∀ {Γ} {φ ψ}                    → Γ ⊢ φ ∧ ψ
                                            → Γ ⊢ ψ
-- Disjunction.

  ∨-intro₁ : ∀ {Γ} {φ} → (ψ : PropFormula)  → Γ ⊢ φ
                                            → Γ ⊢ φ ∨ ψ

  ∨-intro₂ : ∀ {Γ} {ψ} → (φ : PropFormula)  → Γ ⊢ ψ
                                            → Γ ⊢ φ ∨ ψ

  ∨-elim  : ∀ {Γ} {φ ψ χ}                   → Γ , φ ⊢ χ
                                            → Γ , ψ ⊢ χ
                                            → Γ , φ ∨ ψ ⊢ χ
-- Implication.

  ⊃-intro  : ∀ {Γ} {φ ψ}                    → Γ , φ ⊢ ψ
                                            → Γ ⊢ φ ⊃ ψ

  ⊃-elim   : ∀ {Γ} {φ ψ}                    → Γ ⊢ φ ⊃ ψ → Γ ⊢ φ
                                            → Γ ⊢ ψ
-- Biconditional.

  ⇔-intro  : ∀ {Γ} {φ ψ}                    → Γ , φ ⊢ ψ
                                            → Γ , ψ ⊢ φ
                                            → Γ ⊢ φ ⇔ ψ

  ⇔-elim₁ : ∀ {Γ} {φ ψ}                     → Γ ⊢ φ → Γ ⊢ φ ⇔ ψ
                                            → Γ ⊢ ψ

  ⇔-elim₂ : ∀ {Γ} {φ ψ}                     → Γ ⊢ ψ → Γ ⊢ φ ⇔ ψ
                                            → Γ ⊢ φ
------------------------------------------------------------------------

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
{-# OPTIONS --safe #-} -- implies --no-sized-types

module Issue3517.M where

open import Issue3517.S

f : (i : Size) (j : Size< i) → Size< j → Size< i
f i j k = k


text:
module Models where

open import Data.Nat
open import Terms

-- The (complete) Herbrand universe for Σ
U' : {n m : ℕ} → (Signature n m) → Set
U' Σ = GTerm Σ

-- The (complete) μ-Herbrand base for Σ

B'μ : {n m : ℕ} → (Signature n m) → Set
B'μ Σ = GAtom Σ μ

B'ν : {n m : ℕ} → (Signature n m) → Set
B'ν Σ = GAtom Σ ν

open import Relation.Unary as U
open import Level

-- a (complete) Herbrand interpretation
record Interp {n m : ℕ} (Σ : Signature n m) : Set₁ where
  field
    Carrier-μ : Pred (B'μ Σ) Level.zero
    Carrier-ν : Pred (B'ν Σ) Level.zero
open Interp

_∩ᵢ_ : {n m : ℕ} → {Σ : Signature n m} → Interp Σ → Interp Σ
  → Interp Σ
i₁ ∩ᵢ i₂ = record
  { Carrier-μ = Carrier-μ i₁ ∩ Carrier-μ i₂
  ; Carrier-ν = Carrier-ν i₁ ∩ Carrier-ν i₂
  }

_∪ᵢ_ : {n m : ℕ} → {Σ : Signature n m} → Interp Σ → Interp Σ
  → Interp Σ
i₁ ∪ᵢ i₂ = record
  { Carrier-μ = Carrier-μ i₁ ∪ Carrier-μ i₂
  ; Carrier-ν = Carrier-ν i₁ ∪ Carrier-ν i₂
  }

open import Data.List as L
open import Data.List.All as LAl
open import Data.List.Any as LAn
open import Relation.Binary.Core

open Program

-- | Inductive model
record IsIModel {n m : ℕ} {Σ : Signature n m} {var : Set}
       (i : Interp Σ) (P : Program Σ var) : Set₂ where
  field
    forwClosed :
      (bs'μ : List (GAtom Σ μ))
      → All (λ b → b ∈ Carrier-μ i) bs'μ
      → (bs'ν : List (GAtom Σ ν))
      → All (λ b → b ∈ Carrier-ν i) bs'ν
      → (σ : GSubst Σ var)
      → (a : Atom Σ var μ)
      → (bsμ : List (Atom Σ var μ))
      → (bsν : List (Atom Σ var ν))
      → Any (λ cl → cl ≡ (a :- bsμ , bsν)) (prg-μ P)
      → (L.map (appA σ) bsμ) ≡ bs'μ
      → (L.map (appA σ) bsν) ≡ bs'ν
      → (appA σ a ∈ Carrier-μ i)
open IsIModel
open import Data.Product

hA : {A : Set} {B : Set₁}  → A × B → A
hA = proj₁

hBsμ : {A B : Set} {C : Set₁} → A × B × C → B
hBsμ (_ , a , _) = a

hBsν : {A B C : Set} {D : Set₁} → A × B × C × D → C
hBsν (_ , _ , a , _) = a

hσ : {A B C : Set} {D : Set₁} → A × B × C × D → D
hσ (_ , _ , _ , a) = a
open import Data.List.All.Properties -- using (All-map)

-- | model intersection property for a pair of models
prop_model_intersection_pair : {n m : ℕ} → {Σ : Signature n m} {var : Set} →
  (P : Program Σ var)
  → (m₁ : Interp Σ)
  → (m₂ : Interp Σ)
  → Carrier-ν m₁ ≡ Carrier-ν m₂
  → (mp₁ : IsIModel m₁ P)
  → (mp₂ : IsIModel m₂ P)
  → IsIModel (m₁ ∩ᵢ m₂) P
prop_model_intersection_pair P m₁ m₂ eq mp₁ mp₂ =
  record { forwClosed = λ bs'μ x bs'ν y σ a bsμ bsν pcls pμ pν →
    ( forwClosed mp₁ bs'μ (LAl.map proj₁ x) bs'ν
                 (LAl.map proj₁ y) σ a bsμ bsν pcls pμ pν
    , forwClosed mp₂ bs'μ (LAl.map proj₂ x) bs'ν
                 (LAl.map proj₂ y) σ a bsμ bsν pcls pμ pν
    )}

-- | Coinductive model
record IsCModel {n m : ℕ} {Σ : Signature n m} {var : Set}
       (i : Interp Σ) (P : Program Σ var) : Set₁ where
  field
    backClosed :
      --→
      (a' : GAtom Σ ν)
      → a' ∈ Carrier-ν i
      → ∃ (λ ( w : (Atom Σ var ν) -- a
          × (List (Atom Σ var μ)) -- bs-μ
          × (List (Atom Σ var ν)) -- bs-ν
          × GSubst Σ var) →            -- σ

          (Any (λ c → (hA w) :- (hBsμ w) , (hBsν w) ≡ c) (prg-ν P))
          × appA (hσ w) (hA w) ≡ a'
          × All (λ c → c ∈ Carrier-μ i) (L.map (appA (hσ w)) (hBsμ w))
          × All (λ c → c ∈ Carrier-ν i) (L.map (appA (hσ w)) (hBsν w))
     )
open IsCModel

open import Data.Sum
open import Data.Product as DP
open Interp

open import Relation.Binary.PropositionalEquality

-- | model union property for a pair of models
prop_model_union_pair : {n m : ℕ} → {Σ : Signature n m} → {var : Set}
  (P : Program Σ var)
  → (m₁ : Interp Σ)
  → (m₂ : Interp Σ)
  → Carrier-μ m₁ ≡ Carrier-μ m₂
  → (mp₁ : IsCModel m₁ P)
  → (mp₂ : IsCModel m₂ P)
  → IsCModel (m₁ ∪ᵢ m₂) P
prop_model_union_pair P m₁ m₂ eq mp₁ mp₂ {-with (sym eq) -- | (Carrier-μ m₁)
... | eq' {-| dm₁-}-} = record { backClosed = λ
  { a' (inj₁ x) → DP.map
       (λ atm → atm)
       (DP.map
         (λ any → any)
         (λ w → DP.map (λ eq₁ → eq₁) (λ x₃
           → LAl.map inj₁ (proj₁ (proj₂ w))
           , LAl.map inj₁ (proj₂ (proj₂ w))) w))
       (backClosed mp₁ a' x)
  ; a' (inj₂ y) → DP.map
       (λ atm → atm)
       (DP.map
         (λ any → any)
         (λ w → DP.map (λ eq → eq) (λ x₁
           → LAl.map inj₂ (proj₁ (proj₂ w))
           , LAl.map inj₂ (proj₂ (proj₂ w))) w))
       (backClosed mp₂ a' y)
  } }

max_stars_repo_name: frantisekfarka/lp-mod

max_issues_repo_name: frantisekfarka/lp-mod

max_forks_repo_name: frantisekfarka/lp-mod


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Primitive IO: simple bindings to Haskell types and functions
------------------------------------------------------------------------

module IO.Primitive where

open import Data.Char
open import Data.String
open import Foreign.Haskell

------------------------------------------------------------------------
-- The IO monad

postulate
  IO : ∀ {ℓ} → Set ℓ → Set ℓ

{-# IMPORT IO.FFI #-}
{-# COMPILED_TYPE IO IO.FFI.AgdaIO #-}
{-# BUILTIN IO IO #-}

infixl 1 _>>=_

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

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

------------------------------------------------------------------------
-- Simple lazy IO

-- Note that the functions below produce commands which, when
-- executed, may raise exceptions.

-- Note also that the semantics of these functions depends on the
-- version of the Haskell base library. If the version is 4.2.0.0 (or
-- later?), then the functions use the character encoding specified by
-- the locale. For older versions of the library (going back to at
-- least version 3) the functions use ISO-8859-1.

postulate
  getContents : IO Costring
  readFile    : String → IO Costring
  writeFile   : String → Costring → IO Unit
  appendFile  : String → Costring → IO Unit
  putStr      : Costring → IO Unit
  putStrLn    : Costring → IO Unit

  -- Reads a finite file. Raises an exception if the file path refers
  -- to a non-physical file (like "/dev/zero").

  readFiniteFile : String → IO String

{-# COMPILED getContents    getContents           #-}
{-# COMPILED readFile       readFile              #-}
{-# COMPILED writeFile      writeFile             #-}
{-# COMPILED appendFile     appendFile            #-}
{-# COMPILED putStr         putStr                #-}
{-# COMPILED putStrLn       putStrLn              #-}
{-# COMPILED readFiniteFile IO.FFI.readFiniteFile #-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Dependent product combinators for propositional equality
-- preserving functions
------------------------------------------------------------------------

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

module Data.Product.Function.Dependent.Propositional where

open import Data.Product
open import Data.Product.Function.NonDependent.Setoid
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Relation.Binary
open import Function
open import Function.Equality using (_⟶_; _⟨$⟩_)
open import Function.Equivalence as Equiv using (_⇔_; module Equivalence)
open import Function.HalfAdjointEquivalence using (↔→≃; _≃_)
open import Function.Injection as Inj
  using (Injective; _↣_; module Injection)
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Function.LeftInverse as LeftInv
  using (_↞_; _LeftInverseOf_; module LeftInverse)
open import Function.Related
open import Function.Related.TypeIsomorphisms
open import Function.Surjection as Surj using (_↠_; module Surjection)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- Combinators for various function types

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

  ⇔ : (A₁⇔A₂ : A₁ ⇔ A₂) →
      (∀ {x} → B₁ x → B₂ (Equivalence.to   A₁⇔A₂ ⟨$⟩ x)) →
      (∀ {y} → B₂ y → B₁ (Equivalence.from A₁⇔A₂ ⟨$⟩ y)) →
      Σ A₁ B₁ ⇔ Σ A₂ B₂
  ⇔ A₁⇔A₂ B-to B-from = Equiv.equivalence
    (map (Equivalence.to   A₁⇔A₂ ⟨$⟩_) B-to)
    (map (Equivalence.from A₁⇔A₂ ⟨$⟩_) B-from)

  ⇔-↠ : ∀ (A₁↠A₂ : A₁ ↠ A₂) →
        (∀ {x} → _⇔_ (B₁ x) (B₂ (Surjection.to A₁↠A₂ ⟨$⟩ x))) →
        _⇔_ (Σ A₁ B₁) (Σ A₂ B₂)
  ⇔-↠ A₁↠A₂ B₁⇔B₂ = Equiv.equivalence
    (map (Surjection.to   A₁↠A₂ ⟨$⟩_) (Equivalence.to B₁⇔B₂ ⟨$⟩_))
    (map (Surjection.from A₁↠A₂ ⟨$⟩_)
       ((Equivalence.from B₁⇔B₂ ⟨$⟩_) ∘
        P.subst B₂ (P.sym $ Surjection.right-inverse-of A₁↠A₂ _)))

  -- See also Data.Product.Relation.Binary.Pointwise.Dependent.WithK.↣.

  ↣ : ∀ (A₁↔A₂ : A₁ ↔ A₂) →
      (∀ {x} → B₁ x ↣ B₂ (Inverse.to A₁↔A₂ ⟨$⟩ x)) →
      Σ A₁ B₁ ↣ Σ A₂ B₂
  ↣ A₁↔A₂ B₁↣B₂ = Inj.injection to to-injective
    where
    open P.≡-Reasoning

    A₁≃A₂ = ↔→≃ A₁↔A₂

    subst-application′ :
      let open _≃_ A₁≃A₂ in
      {x₁ x₂ : A₁} {y : B₁ (from (to x₁))}
      (g : ∀ x → B₁ (from (to x)) → B₂ (to x)) (eq : to x₁ ≡ to x₂) →
      P.subst B₂ eq (g x₁ y) ≡ g x₂ (P.subst B₁ (P.cong from eq) y)
    subst-application′ {x₁} {x₂} {y} g eq =
      P.subst B₂ eq (g x₁ y)                      ≡⟨ P.cong (P.subst B₂ eq) (P.sym (g′-lemma _ _)) ⟩
      P.subst B₂ eq (g′ (to x₁) y)                ≡⟨ P.subst-application B₁ g′ eq ⟩
      g′ (to x₂) (P.subst B₁ (P.cong from eq) y)  ≡⟨ g′-lemma _ _ ⟩
      g x₂ (P.subst B₁ (P.cong from eq) y)        ∎
      where
      open _≃_ A₁≃A₂

      g′ : ∀ x → B₁ (from x) → B₂ x
      g′ x =
        P.subst B₂ (right-inverse-of x) ∘
        g (from x) ∘
        P.subst B₁ (P.sym (P.cong from (right-inverse-of x)))

      g′-lemma : ∀ x y → g′ (to x) y ≡ g x y
      g′-lemma x y =
        P.subst B₂ (right-inverse-of (to x))
          (g (from (to x)) $
           P.subst B₁ (P.sym (P.cong from (right-inverse-of (to x)))) y)  ≡⟨ P.cong (λ p → P.subst B₂ p (g (from (to x))
                                                                                (P.subst B₁ (P.sym (P.cong from p)) y)))
                                                                               (P.sym (left-right x)) ⟩
        P.subst B₂ (P.cong to (left-inverse-of x))
          (g (from (to x)) $
           P.subst B₁
             (P.sym (P.cong from (P.cong to (left-inverse-of x))))
             y)                                                           ≡⟨ lemma _ ⟩

        g x y                                                             ∎
        where
        lemma :
          ∀ {x′} eq {y : B₁ (from (to x′))} →
          P.subst B₂ (P.cong to eq)
            (g (from (to x))
               (P.subst B₁ (P.sym (P.cong from (P.cong to eq))) y)) ≡
          g x′ y
        lemma P.refl = P.refl

    to = map (_≃_.to A₁≃A₂) (Injection.to B₁↣B₂ ⟨$⟩_)

    to-injective : Injective (P.→-to-⟶ {B = P.setoid _} to)
    to-injective {(x₁ , x₂)} {(y₁ , y₂)} =
      (Inverse.to Σ-≡,≡↔≡ ⟨$⟩_) ∘′

      map (_≃_.injective A₁≃A₂) (λ {eq₁} eq₂ →

        let lemma =

              Injection.to B₁↣B₂ ⟨$⟩
              P.subst B₁ (_≃_.injective A₁≃A₂ eq₁) x₂                     ≡⟨⟩

              Injection.to B₁↣B₂ ⟨$⟩
              P.subst B₁
                (P.trans (P.sym (_≃_.left-inverse-of A₁≃A₂ x₁))
                   (P.trans (P.cong (_≃_.from A₁≃A₂) eq₁)
                      (P.trans (_≃_.left-inverse-of A₁≃A₂ y₁)
                         P.refl)))
                x₂                                                        ≡⟨ P.cong (λ p → Injection.to B₁↣B₂ ⟨$⟩
                                                                                P.subst B₁
                                                                                (P.trans (P.sym (_≃_.left-inverse-of A₁≃A₂ _))
                                                                                (P.trans (P.cong (_≃_.from A₁≃A₂) eq₁) p))
                                                                                x₂)
                                                                               (P.trans-reflʳ _) ⟩
              Injection.to B₁↣B₂ ⟨$⟩
              P.subst B₁
                (P.trans (P.sym (_≃_.left-inverse-of A₁≃A₂ x₁))
                   (P.trans (P.cong (_≃_.from A₁≃A₂) eq₁)
                      (_≃_.left-inverse-of A₁≃A₂ y₁)))
                x₂                                                        ≡⟨ P.cong (Injection.to B₁↣B₂ ⟨$⟩_)
                                                                               (P.sym (P.subst-subst (P.sym (_≃_.left-inverse-of A₁≃A₂ _)))) ⟩
              Injection.to B₁↣B₂ ⟨$⟩
              (P.subst B₁ (P.trans (P.cong (_≃_.from A₁≃A₂) eq₁)
                             (_≃_.left-inverse-of A₁≃A₂ y₁)) $
               P.subst B₁ (P.sym (_≃_.left-inverse-of A₁≃A₂ x₁)) x₂)      ≡⟨ P.cong (Injection.to B₁↣B₂ ⟨$⟩_)
                                                                               (P.sym (P.subst-subst (P.cong (_≃_.from A₁≃A₂) eq₁))) ⟩
              Injection.to B₁↣B₂ ⟨$⟩
              (P.subst B₁ (_≃_.left-inverse-of A₁≃A₂ y₁) $
               P.subst B₁ (P.cong (_≃_.from A₁≃A₂) eq₁) $
               P.subst B₁ (P.sym (_≃_.left-inverse-of A₁≃A₂ x₁)) x₂)      ≡⟨ P.sym (subst-application′
                                                                                (λ x y → Injection.to B₁↣B₂ ⟨$⟩
                                                                                P.subst B₁ (_≃_.left-inverse-of A₁≃A₂ x) y)
                                                                                eq₁) ⟩
              P.subst B₂ eq₁
                (Injection.to B₁↣B₂ ⟨$⟩
                 (P.subst B₁ (_≃_.left-inverse-of A₁≃A₂ x₁) $
                  P.subst B₁ (P.sym (_≃_.left-inverse-of A₁≃A₂ x₁)) x₂))  ≡⟨ P.cong (P.subst B₂ eq₁ ∘ (Injection.to B₁↣B₂ ⟨$⟩_))
                                                                               (P.subst-subst (P.sym (_≃_.left-inverse-of A₁≃A₂ _))) ⟩
              P.subst B₂ eq₁
                (Injection.to B₁↣B₂ ⟨$⟩
                 P.subst B₁
                   (P.trans (P.sym (_≃_.left-inverse-of A₁≃A₂ x₁))
                      (_≃_.left-inverse-of A₁≃A₂ x₁))
                   x₂)                                                    ≡⟨ P.cong (λ p → P.subst B₂ eq₁
                                                                                (Injection.to B₁↣B₂ ⟨$⟩ P.subst B₁ p x₂))
                                                                               (P.trans-symˡ (_≃_.left-inverse-of A₁≃A₂ _)) ⟩
              P.subst B₂ eq₁
                (Injection.to B₁↣B₂ ⟨$⟩ P.subst B₁ P.refl x₂)             ≡⟨⟩

              P.subst B₂ eq₁ (Injection.to B₁↣B₂ ⟨$⟩ x₂)                  ≡⟨ eq₂ ⟩

              Injection.to B₁↣B₂ ⟨$⟩ y₂                                   ∎

        in

        P.subst B₁ (_≃_.injective A₁≃A₂ eq₁) x₂  ≡⟨ Injection.injective B₁↣B₂ lemma ⟩
        y₂                                       ∎) ∘

      (Inverse.from Σ-≡,≡↔≡ ⟨$⟩_)

  ↞ : (A₁↞A₂ : A₁ ↞ A₂) →
      (∀ {x} → B₁ (LeftInverse.from A₁↞A₂ ⟨$⟩ x) ↞ B₂ x) →
      Σ A₁ B₁ ↞ Σ A₂ B₂
  ↞ A₁↞A₂ B₁↞B₂ = record
    { to              = P.→-to-⟶ to
    ; from            = P.→-to-⟶ from
    ; left-inverse-of = left-inverse-of
    }
    where
    open P.≡-Reasoning

    from = map (LeftInverse.from A₁↞A₂ ⟨$⟩_) (LeftInverse.from B₁↞B₂ ⟨$⟩_)

    to   = map
      (LeftInverse.to A₁↞A₂ ⟨$⟩_)
      (λ {x} y →
         LeftInverse.to B₁↞B₂ ⟨$⟩
           P.subst B₁ (P.sym (LeftInverse.left-inverse-of A₁↞A₂ x)) y)

    left-inverse-of : ∀ p → from (to p) ≡ p
    left-inverse-of (x , y) = Inverse.to Σ-≡,≡↔≡ ⟨$⟩
      ( LeftInverse.left-inverse-of A₁↞A₂ x
      , (P.subst B₁ (LeftInverse.left-inverse-of A₁↞A₂ x)
           (LeftInverse.from B₁↞B₂ ⟨$⟩ (LeftInverse.to B₁↞B₂ ⟨$⟩
              (P.subst B₁ (P.sym (LeftInverse.left-inverse-of A₁↞A₂ x))
                 y)))                                                    ≡⟨ P.cong (P.subst B₁ _) (LeftInverse.left-inverse-of B₁↞B₂ _) ⟩

         P.subst B₁ (LeftInverse.left-inverse-of A₁↞A₂ x)
           (P.subst B₁ (P.sym (LeftInverse.left-inverse-of A₁↞A₂ x))
              y)                                                         ≡⟨ P.subst-subst-sym (LeftInverse.left-inverse-of A₁↞A₂ x) ⟩

         y                                                               ∎)
      )

  ↠ : (A₁↠A₂ : A₁ ↠ A₂) →
      (∀ {x} → B₁ x ↠ B₂ (Surjection.to A₁↠A₂ ⟨$⟩ x)) →
      Σ A₁ B₁ ↠ Σ A₂ B₂
  ↠ A₁↠A₂ B₁↠B₂ = record
    { to         = P.→-to-⟶ to
    ; surjective = record
      { from             = P.→-to-⟶ from
      ; right-inverse-of = right-inverse-of
      }
    }
    where
    open P.≡-Reasoning

    to   = map (Surjection.to A₁↠A₂ ⟨$⟩_)
                    (Surjection.to B₁↠B₂ ⟨$⟩_)
    from = map
      (Surjection.from A₁↠A₂ ⟨$⟩_)
      (λ {x} y →
         Surjection.from B₁↠B₂ ⟨$⟩
           P.subst B₂ (P.sym (Surjection.right-inverse-of A₁↠A₂ x)) y)

    right-inverse-of : ∀ p → to (from p) ≡ p
    right-inverse-of (x , y) = Inverse.to Σ-≡,≡↔≡ ⟨$⟩
      ( Surjection.right-inverse-of A₁↠A₂ x
      , (P.subst B₂ (Surjection.right-inverse-of A₁↠A₂ x)
           (Surjection.to B₁↠B₂ ⟨$⟩ (Surjection.from B₁↠B₂ ⟨$⟩
              (P.subst B₂ (P.sym (Surjection.right-inverse-of A₁↠A₂ x))
                 y)))                                                    ≡⟨ P.cong (P.subst B₂ _) (Surjection.right-inverse-of B₁↠B₂ _) ⟩

         P.subst B₂ (Surjection.right-inverse-of A₁↠A₂ x)
           (P.subst B₂ (P.sym (Surjection.right-inverse-of A₁↠A₂ x))
              y)                                                         ≡⟨ P.subst-subst-sym (Surjection.right-inverse-of A₁↠A₂ x) ⟩

         y                                                               ∎)
      )

  ↔ : (A₁↔A₂ : A₁ ↔ A₂) →
      (∀ {x} → B₁ x ↔ B₂ (Inverse.to A₁↔A₂ ⟨$⟩ x)) →
      Σ A₁ B₁ ↔ Σ A₂ B₂
  ↔ A₁↔A₂ B₁↔B₂ = Inv.inverse
    (Surjection.to   surjection′ ⟨$⟩_)
    (Surjection.from surjection′ ⟨$⟩_)
    left-inverse-of
    (Surjection.right-inverse-of surjection′)
    where
    open P.≡-Reasoning

    A₁≃A₂ = ↔→≃ A₁↔A₂

    surjection′ : _↠_ (Σ A₁ B₁) (Σ A₂ B₂)
    surjection′ =
      ↠ (Inverse.surjection (_≃_.inverse A₁≃A₂))
        (Inverse.surjection B₁↔B₂)

    left-inverse-of :
      ∀ p → Surjection.from surjection′ ⟨$⟩
              (Surjection.to surjection′ ⟨$⟩ p) ≡ p
    left-inverse-of (x , y) = Inverse.to Σ-≡,≡↔≡ ⟨$⟩
      ( _≃_.left-inverse-of A₁≃A₂ x
      , (P.subst B₁ (_≃_.left-inverse-of A₁≃A₂ x)
           (Inverse.from B₁↔B₂ ⟨$⟩
              (P.subst B₂ (P.sym (_≃_.right-inverse-of A₁≃A₂
                                    (_≃_.to A₁≃A₂ x)))
                 (Inverse.to B₁↔B₂ ⟨$⟩ y)))                   ≡⟨ P.subst-application B₂ (λ _ → Inverse.from B₁↔B₂ ⟨$⟩_) _ ⟩

         Inverse.from B₁↔B₂ ⟨$⟩
           (P.subst B₂ (P.cong (_≃_.to A₁≃A₂)
                          (_≃_.left-inverse-of A₁≃A₂ x))
              (P.subst B₂ (P.sym (_≃_.right-inverse-of A₁≃A₂
                                    (_≃_.to A₁≃A₂ x)))
                 (Inverse.to B₁↔B₂ ⟨$⟩ y)))                   ≡⟨ P.cong (λ eq → Inverse.from B₁↔B₂ ⟨$⟩ P.subst B₂ eq
                                                                                (P.subst B₂ (P.sym (_≃_.right-inverse-of A₁≃A₂ _)) _))
                                                                   (_≃_.left-right A₁≃A₂ _) ⟩
         Inverse.from B₁↔B₂ ⟨$⟩
           (P.subst B₂ (_≃_.right-inverse-of A₁≃A₂
                          (_≃_.to A₁≃A₂ x))
              (P.subst B₂ (P.sym (_≃_.right-inverse-of A₁≃A₂
                                    (_≃_.to A₁≃A₂ x)))
                 (Inverse.to B₁↔B₂ ⟨$⟩ y)))                   ≡⟨ P.cong (Inverse.from B₁↔B₂ ⟨$⟩_)
                                                                   (P.subst-subst-sym (_≃_.right-inverse-of A₁≃A₂ _)) ⟩

         Inverse.from B₁↔B₂ ⟨$⟩ (Inverse.to B₁↔B₂ ⟨$⟩ y)      ≡⟨ Inverse.left-inverse-of B₁↔B₂ _ ⟩

         y                                                    ∎)
      )

private

  swap-coercions : ∀ {k a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
    {B₁ : A₁ → Set b₁} (B₂ : A₂ → Set b₂)
    (A₁↔A₂ : _↔_ A₁ A₂) →
    (∀ {x} → B₁ x ∼[ k ] B₂ (Inverse.to A₁↔A₂ ⟨$⟩ x)) →
    ∀ {x} → B₁ (Inverse.from A₁↔A₂ ⟨$⟩ x) ∼[ k ] B₂ x
  swap-coercions {k} {B₁ = B₁} B₂ A₁↔A₂ eq {x} =
    B₁ (Inverse.from A₁↔A₂ ⟨$⟩ x)
      ∼⟨ eq ⟩
    B₂ (Inverse.to A₁↔A₂ ⟨$⟩ (Inverse.from A₁↔A₂ ⟨$⟩ x))
      ↔⟨ K-reflexive
         (P.cong B₂ $ Inverse.right-inverse-of A₁↔A₂ x) ⟩
    B₂ x
      ∎
    where open EquationalReasoning

cong : ∀ {k a₁ a₂ b₁ b₂}
         {A₁ : Set a₁} {A₂ : Set a₂}
         {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂}
       (A₁↔A₂ : _↔_ A₁ A₂) →
       (∀ {x} → B₁ x ∼[ k ] B₂ (Inverse.to A₁↔A₂ ⟨$⟩ x)) →
       Σ A₁ B₁ ∼[ k ] Σ A₂ B₂
cong {implication}                   =
  λ A₁↔A₂ → map (_⟨$⟩_ (Inverse.to A₁↔A₂))
cong {reverse-implication} {B₂ = B₂} =
  λ A₁↔A₂ B₁←B₂ → lam (map (_⟨$⟩_ (Inverse.from A₁↔A₂))
    (app-← (swap-coercions B₂ A₁↔A₂ B₁←B₂)))
cong {equivalence}                   = ⇔-↠ ∘ Inverse.surjection
cong {injection}                     = ↣
cong {reverse-injection}   {B₂ = B₂} =
  λ A₁↔A₂ B₁↢B₂ → lam (↣ (Inv.sym A₁↔A₂)
    (app-↢ (swap-coercions B₂ A₁↔A₂ B₁↢B₂)))
cong {left-inverse}                  =
  λ A₁↔A₂ → ↞ (Inverse.left-inverse A₁↔A₂) ∘ swap-coercions _ A₁↔A₂
cong {surjection}                    = ↠ ∘ Inverse.surjection
cong {bijection}                     = ↔


text:
-- Andreas, 2018-07-22, issue #3136
-- WAS: Internal error when printing termination errors

{-# OPTIONS --postfix-projections #-}

module Issue3136 (A : Set) where

-- postulate A : Set
postulate
  any : {X : Set} → X
  x : A
  P : A → Set

record C : Set where
  field
    a : A
    b : P a

c : C
c = λ where
  .C.a → x
  .C.b → λ where
    → any

-- Should report a termination error but not crash

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


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

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

single : {m n : Nat} → suc m ≡ suc n → n ≡ m
single p with refl ← p = refl

double : {m n p : Nat} → suc m ≡ n → suc n ≡ 2 + p → m ≡ p
double p q with refl ← p | refl ← q = refl

_∋_ : (A : Set) → A → A
A ∋ a = a

-- The second equality proof is only well-typed
-- after the first one has been used

tele : {m n : Nat} → suc m ≡ suc n → m ≡ n
tele {m} {n} p
  with refl ← p
  with refl ← (n ≡ m) ∋ refl
       = refl

tele' : {m n : Nat} → m ≡ n → m ≡ n
tele' {m} {n} p with refl ← p with (n ≡ m) ∋ refl
... | q = refl

-- Further splitting after a using & with

tele'' : {m n : Nat} → m ≡ n → Nat → Nat
tele'' {m} {n} p r with refl ← p | (n ≡ m) ∋ refl
tele'' {m} {m} p zero    | q = m
tele'' {m} {m} p (suc r) | q = r

data Vec {a} (A : Set a) : Nat → Set a where
  []  : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

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

  head : Vec A (suc n) → A
  head xs with (x ∷ _) ← xs = x

  tail : Vec A (suc n) → Vec A n
  tail xs with (_ ∷ xs) ← xs = xs -- pattern shadows variable with'd on

castVec : ∀ {m n} → m ≡ n → Vec Nat m → Vec Nat n
castVec eq ms with refl ← eq = ms

data All (P : Nat → Set) : ∀ {n} → Vec Nat n → Set where
  []  : All P []
  _∷_ : ∀ {n x xs} → P x → All P {n} xs → All P (x ∷ xs)

open import Agda.Builtin.Sigma

castAll : ∀ {P m n xs ys} → Σ (m ≡ n) (λ eq → castVec eq xs ≡ ys) →
          All P xs → All P ys
castAll (refl , refl) all = all

-- faking rewrite with the dependent irrefutable with
postulate +-comm : ∀ m n → m + n ≡ n + m

rew : ∀ m n p q → m + (p + q) + n ≡ m + (q + p) + n
rew m n p q with p+q ← p + q | refl ← +-comm p q {- : p + q ≡ q + p -} = refl

-- Note that the following does not work because
-- p+q is not abstracted over in `+-comm p q` which means
-- Agda gets stuck trying to unify `p + q` and `q + p`

-- Cf. test/Fail/UsingEq.agda

-- rew' : ∀ m n p q → m + (p + q) + n ≡ m + (q + p) + n
-- rew' m n p q with p+q ← p + q with refl ← +-comm p q = refl