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

module Bundles where

open import Algebra.Core
open import Quasigroup.Structures
open import Relation.Binary
open import Level
open import Algebra.Bundles
open import Algebra.Structures
open import Structures

record InverseSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier            : Set c
    _≈_                : Rel Carrier ℓ
    _∙_                : Op₂ Carrier
    isInverseSemigroup : IsInverseSemigroup _≈_ _∙_

  open IsInverseSemigroup isInverseSemigroup public

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

  open Magma magma public
    using (_≉_; rawMagma)

record Rng c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    isRng  : IsRng _≈_ _+_ _*_ -_ 0#

  open IsRng isRng public

  +-abelianGroup : AbelianGroup _ _
  +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }

  *-semigroup : Semigroup _ _
  *-semigroup = record { isSemigroup = *-isSemigroup }

  open AbelianGroup +-abelianGroup public
    using () renaming (group to +-group; invertibleMagma to +-invertibleMagma; invertibleUnitalMagma to +-invertibleUnitalMagma)

  open Semigroup *-semigroup public
    using () renaming
    ( rawMagma to *-rawMagma
    ; magma    to *-magma
    )

record NonAssociativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier               : Set c
    _≈_                   : Rel Carrier ℓ
    _+_                   : Op₂ Carrier
    _*_                   : Op₂ Carrier
    -_                    : Op₁ Carrier
    0#                    : Carrier
    1#                    : Carrier
    isNonAssociativeRing  : IsNonAssociativeRing _≈_ _+_ _*_ -_ 0# 1#

  open IsNonAssociativeRing isNonAssociativeRing public

  +-abelianGroup : AbelianGroup _ _
  +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }

  *-unitalmagma : UnitalMagma _ _
  *-unitalmagma = record { isUnitalMagma = *-isUnitalMagma }

  open AbelianGroup +-abelianGroup public
    using () renaming (group to +-group; invertibleMagma to +-invertibleMagma; invertibleUnitalMagma to +-invertibleUnitalMagma)

  open UnitalMagma *-unitalmagma public
    using () renaming
    ( rawMagma to *-rawMagma
    ; magma    to *-magma
    )


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

-- From: Hancock (2008). (Ordinal-theoretic) proof theory.

module Ordinals where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

data Ω : Set where
  zero : Ω
  succ : Ω → Ω
  limN : (ℕ → Ω) → Ω

inj : ℕ → Ω
inj zero     = zero
inj (succ n) = succ (inj n)

ω : Ω
ω = limN (λ n → inj n)

ω+1 : Ω
ω+1 = succ ω

data Ω₂ : Set where
  zero : Ω₂
  succ : Ω₂ → Ω₂
  limN : (ℕ → Ω₂) → Ω₂
  limΩ : (Ω → Ω₂) → Ω₂

inj₁ : Ω → Ω₂
inj₁ zero     = zero
inj₁ (succ o) = succ (inj₁ o)
inj₁ (limN f) = limN (λ n → inj₁ (f n))

ω₁ : Ω₂
ω₁ = limΩ (λ o → inj₁ o)

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Andreas, 2019-11-12, issue #4168b
--
-- Meta variable solver should not use uncurrying
-- if the record type contains erased fields.

open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma
open import Common.IO

P : (A B : Set) → (A → B) → Set
P A B f = (y : B) → Σ A (λ x → f x ≡ y)

record R (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from-to : (x : A) → from (to x) ≡ x

p : (A B : Set) (r : R A B) → P A B (R.to r)
p _ _ r y = R.from r y , to-from y
  where
  postulate
    to-from : ∀ x → R.to r (R.from r x) ≡ x

record Box (A : Set) : Set where
  constructor box
  field
    @0 unbox : A

test : (A : Set) → P (Box A) (Box (Box A)) (box {A = Box A})
test A = p _ _ (record
  { to      = box {A = _}
  ; from    = λ { (box (box x)) → box {A = A} x }
      -- at first, a postponed type checking problem ?from
  ; from-to = λ x → refl {A = Box A} {x = _}
  })
-- from-to creates constraint
--
--   x : Box A |- ?from (box x) = x : Box A
--
-- This was changed to
--
--   y : Box (Box A) |- ?from y = unbox y : Box A
--
-- which is an invalid transformation since x is not
-- guaranteed to be in erased context.

-- As a consequence, compilation (GHC backend) failed.

-- A variant with a non-erased field.

record ⊤ : Set where

record Box' (A : Set) : Set where
  constructor box'
  field
    unit : ⊤
    @0 unbox' : A

test' : (A : Set) → P (Box' A) (Box' (Box' A)) (box' {A = Box' A} _)
test' A = p _ _ (record
  { to      = box' {A = _} _
  ; from    = λ { (box' _ (box' _ x)) → box' {A = A} _ x }
  ; from-to = λ x → refl {A = Box' A} {x = _}
  })

main : IO ⊤
main = return _

max_stars_repo_name: k-bx/agda

max_issues_repo_name: k-bx/agda

max_forks_repo_name: k-bx/agda


text:
open import Data.Product using ( _×_ ; _,_ ; proj₁ ; proj₂ )
open import Data.Sum using ( inj₁ ; inj₂ )
open import Data.Unit using ( tt )
open import Relation.Binary.PropositionalEquality using ( refl )
open import Relation.Unary using ( _∈_ ; _⊆_ )
open import Web.Semantic.DL.ABox using
  ( ABox ; Assertions ; ε ; _,_ ; _∼_ ; _∈₁_ ; _∈₂_ )
open import Web.Semantic.DL.ABox.Interp using
  ( Interp ; _,_ ; ⌊_⌋ ; ind ; _*_ )
open import Web.Semantic.DL.ABox.Interp.Morphism using
  ( _≲_ ; _,_ ; ≲⌊_⌋ ; ≲-resp-ind ; _≋_ )
open import Web.Semantic.DL.ABox.Model using
  ( _⟦_⟧₀ ; _⊨a_ ; Assertions✓ )
open import Web.Semantic.DL.Concept using
  ( ⟨_⟩ ; ¬⟨_⟩ ; ⊤ ; ⊥ ; _⊓_ ; _⊔_ ; ∀[_]_ ; ∃⟨_⟩_ ; ≤1 ; >1 )
open import Web.Semantic.DL.Concept.Model using ( _⟦_⟧₁ ; ⟦⟧₁-resp-≈ )
open import Web.Semantic.DL.Integrity using
  ( Unique ; Mediator ; Initial ; _>>_ ; _⊕_⊨_ ; _,_ )
open import Web.Semantic.DL.KB using ( KB ; tbox ; abox )
open import Web.Semantic.DL.KB.Model using ( _⊨_ )
open import Web.Semantic.DL.Role using ( ⟨_⟩ ; ⟨_⟩⁻¹ )
open import Web.Semantic.DL.Role.Model using ( _⟦_⟧₂ ; ⟦⟧₂-resp-≈ )
open import Web.Semantic.DL.Sequent using
  ( Γ ; γ ; _⊕_⊢_∼_ ; _⊕_⊢_∈₁_ ; _⊕_⊢_∈₂_
  ; ∼-assert ; ∼-import ;∼-refl ; ∼-sym ; ∼-trans ; ∼-≤1
  ; ∈₂-assert ; ∈₂-import ; ∈₂-resp-∼ ; ∈₂-subsum
  ; ∈₂-refl ; ∈₂-trans ; ∈₂-inv-I ; ∈₂-inv-E
  ; ∈₁-assert ; ∈₁-import ; ∈₁-resp-∼ ; ∈₁-subsum
  ; ∈₁-⊤-I ; ∈₁-⊓-I ; ∈₁-⊓-E₁ ; ∈₁-⊓-E₂
  ; ∈₁-⊔-I₁ ; ∈₁-⊔-I₂ ; ∈₁-∃-I ; ∈₁-∀-E )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using
  ( TBox ; Axioms ; ε ; _,_ ;_⊑₁_ ; _⊑₂_ ; Tra )
open import Web.Semantic.DL.TBox.Interp using
  ( interp ; Δ ; _⊨_≈_ ; ≈-refl ; ≈-sym ; ≈-trans ; con-≈ ; rol-≈ ) renaming
  ( Interp to Interp′ )
open import Web.Semantic.DL.TBox.Interp.Morphism using
  ( morph ; ≲-image ; ≲-resp-≈ ; ≲-resp-con ; ≲-resp-rol )
open import Web.Semantic.DL.TBox.Minimizable using
  ( LHS ; RHS ; μTBox
  ; ⟨_⟩ ; ⊤ ; ⊥ ; _⊓_ ; _⊔_ ; ∀[_]_ ; ∃⟨_⟩_ ; ≤1
  ; ε ; _,_ ;_⊑₁_ ; _⊑₂_ ; Ref ; Tra )
open import Web.Semantic.DL.TBox.Model using ( _⊨t_ ; Axioms✓ )
open import Web.Semantic.Util using
  ( Subset ; ⊆-refl ; id ; _∘_ ; _⊕_⊕_ ; _[⊕]_[⊕]_ ; inode ; bnode ; enode )

module Web.Semantic.DL.Sequent.Model {Σ : Signature} {W X Y : Set} where

infix 5 _⊞_

minimal′ : Interp Σ X → KB Σ (X ⊕ W ⊕ Y) → Interp′ Σ
minimal′ I KB =
  interp (Γ I KB) (λ x y → (I ⊕ KB ⊢ x ∼ y)) ∼-refl ∼-sym ∼-trans
    (λ c x → I ⊕ KB ⊢ x ∈₁ ⟨ c ⟩) (λ r xy → I ⊕ KB ⊢ xy ∈₂ ⟨ r ⟩)
    (λ c → ∈₁-resp-∼) (λ r → ∈₂-resp-∼)

minimal : Interp Σ X → KB Σ (X ⊕ W ⊕ Y) → Interp Σ (X ⊕ W ⊕ Y)
minimal I KB = (minimal′ I KB , γ I KB)

complete₂ : ∀ I KB R {xy} → (xy ∈ minimal′ I KB ⟦ R ⟧₂) → (I ⊕ KB ⊢ xy ∈₂ R)
complete₂ I KB ⟨ r ⟩   {(x , y)} xy∈⟦r⟧ = xy∈⟦r⟧
complete₂ I KB ⟨ r ⟩⁻¹ {(x , y)} yx∈⟦r⟧ = ∈₂-inv-I yx∈⟦r⟧

complete₁ : ∀ I KB {C x} → (C ∈ LHS) → (x ∈ minimal′ I KB ⟦ C ⟧₁) →
  (I ⊕ KB ⊢ x ∈₁ C)
complete₁ I KB ⟨ c ⟩ x∈⟦c⟧ =
  x∈⟦c⟧
complete₁ I KB ⊤ _ =
  ∈₁-⊤-I
complete₁ I KB (C ⊓ D) (x∈⟦C⟧ , x∈⟦D⟧) =
  ∈₁-⊓-I (complete₁ I KB C x∈⟦C⟧) (complete₁ I KB D x∈⟦D⟧)
complete₁ I KB (C ⊔ D) (inj₁ x∈⟦C⟧) =
  ∈₁-⊔-I₁ (complete₁ I KB C x∈⟦C⟧)
complete₁ I KB (C ⊔ D) (inj₂ x∈⟦D⟧) =
  ∈₁-⊔-I₂ (complete₁ I KB D x∈⟦D⟧)
complete₁ I KB (∃⟨ R ⟩ C) (y , xy∈⟦R⟧ , y∈⟦C⟧) =
  ∈₁-∃-I (complete₂ I KB R xy∈⟦R⟧) (complete₁ I KB C y∈⟦C⟧)
complete₁ I KB ⊥ ()

sound₂ : ∀ I KB R {xy} → (I ⊕ KB ⊢ xy ∈₂ R) → (xy ∈ minimal′ I KB ⟦ R ⟧₂)
sound₂ I KB ⟨ r ⟩   {(x , y)} ⊢xy∈r  = ⊢xy∈r
sound₂ I KB ⟨ r ⟩⁻¹ {(x , y)} ⊢xy∈r⁻ = ∈₂-inv-E ⊢xy∈r⁻

sound₁ : ∀ I KB {C x} → (C ∈ RHS) → (I ⊕ KB ⊢ x ∈₁ C) →
  (x ∈ minimal′ I KB ⟦ C ⟧₁)
sound₁ I KB ⟨ c ⟩ ⊢x∈c =
  ⊢x∈c
sound₁ I KB ⊤ ⊢x∈⊤ =
  tt
sound₁ I KB (C ⊓ D) ⊢x∈C⊓D =
  (sound₁ I KB C (∈₁-⊓-E₁ ⊢x∈C⊓D) , sound₁ I KB D (∈₁-⊓-E₂ ⊢x∈C⊓D))
sound₁ I KB (∀[ R ] C) ⊢x∈∀RC = λ y xy∈⟦R⟧ →
  sound₁ I KB C (∈₁-∀-E ⊢x∈∀RC (complete₂ I KB R xy∈⟦R⟧))
sound₁ I KB (≤1 R) ⊢x∈≤1R = λ y z xy∈⟦R⟧ xz∈⟦R⟧ →
  ∼-≤1 ⊢x∈≤1R (complete₂ I KB R xy∈⟦R⟧) (complete₂ I KB R xz∈⟦R⟧)

minimal-⊨ : ∀ I KB → (tbox KB ∈ μTBox) → (minimal I KB ⊨ KB)
minimal-⊨ I KB μT =
  ( minimal-tbox μT (⊆-refl (Axioms (tbox KB)))
  , minimal-abox (abox KB) (⊆-refl (Assertions (abox KB)))) where

  minimal-tbox : ∀ {T} → (T ∈ μTBox) → (Axioms T ⊆ Axioms (tbox KB)) →
    minimal′ I KB ⊨t T
  minimal-tbox ε ε⊆T =
    tt
  minimal-tbox (U , V) UV⊆T =
    ( minimal-tbox U (λ u → UV⊆T (inj₁ u))
    , minimal-tbox V (λ v → UV⊆T (inj₂ v)) )
  minimal-tbox (C ⊑₁ D) C⊑₁D∈T = λ x∈⟦C⟧ →
    sound₁ I KB D (∈₁-subsum (complete₁ I KB C x∈⟦C⟧) (C⊑₁D∈T refl))
  minimal-tbox (Q ⊑₂ R) Q⊑₁R∈T = λ xy∈⟦Q⟧ →
    sound₂ I KB R (∈₂-subsum (complete₂ I KB Q xy∈⟦Q⟧) (Q⊑₁R∈T refl))
  minimal-tbox (Ref R) RefR∈T = λ x →
    sound₂ I KB R (∈₂-refl x (RefR∈T refl))
  minimal-tbox (Tra R) TraR∈T = λ xy∈⟦R⟧ yz∈⟦R⟧ →
    sound₂ I KB R (∈₂-trans
      (complete₂ I KB R xy∈⟦R⟧) (complete₂ I KB R yz∈⟦R⟧) (TraR∈T refl))

  minimal-abox : ∀ A → (Assertions A ⊆ Assertions (abox KB)) →
    minimal I KB ⊨a A
  minimal-abox ε ε⊆A =
    tt
  minimal-abox (B , C) BC⊆A =
    ( minimal-abox B (λ b → BC⊆A (inj₁ b))
    , minimal-abox C (λ c → BC⊆A (inj₂ c)) )
  minimal-abox (x ∼ y) x∼y⊆A =
    ∼-assert (x∼y⊆A refl)
  minimal-abox (x ∈₁ c) x∈C⊆A =
    sound₁ I KB ⟨ c ⟩ (∈₁-assert (x∈C⊆A refl))
  minimal-abox ((x , y) ∈₂ r) xy∈R⊆A =
    sound₂ I KB ⟨ r ⟩ (∈₂-assert (xy∈R⊆A refl))

minimal-≳ : ∀ I KB → (I ≲ inode * minimal I KB)
minimal-≳ I KB = (morph inode ∼-import ∈₁-import ∈₂-import , λ x → ∼-refl)

minimal-≲ : ∀ I KB J → (I ≲ inode * J) → (J ⊨ KB) → (minimal I KB ≲ J)
minimal-≲ I KB J I≲J (J⊨T , J⊨A) =
  (morph f minimal-≈ minimal-con minimal-rol , fγ≈j) where

    f : Γ I KB → Δ ⌊ J ⌋
    f = (≲-image ≲⌊ I≲J ⌋) [⊕] (ind J ∘ bnode) [⊕] (ind J ∘ enode)

    fγ≈j : ∀ x → ⌊ J ⌋ ⊨ f (γ I KB x) ≈ ind J x
    fγ≈j (inode x) = ≲-resp-ind I≲J x
    fγ≈j (bnode v) = ≈-refl ⌊ J ⌋
    fγ≈j (enode y) = ≈-refl ⌊ J ⌋

    mutual

      minimal-≈ : ∀ {x y} → (I ⊕ KB ⊢ x ∼ y) → (⌊ J ⌋ ⊨ f x ≈ f y)
      minimal-≈ (∼-assert x∼y∈A) =
        ≈-trans ⌊ J ⌋ (fγ≈j _)
          (≈-trans ⌊ J ⌋ (Assertions✓ J (abox KB) x∼y∈A J⊨A)
            (≈-sym ⌊ J ⌋ (fγ≈j _)))
      minimal-≈ (∼-import x≈y) =
        ≲-resp-≈ ≲⌊ I≲J ⌋ x≈y
      minimal-≈ ∼-refl =
        ≈-refl ⌊ J ⌋
      minimal-≈ (∼-sym x∼y) =
        ≈-sym ⌊ J ⌋ (minimal-≈ x∼y)
      minimal-≈ (∼-trans x∼y y∼z) =
        ≈-trans ⌊ J ⌋ (minimal-≈ x∼y) (minimal-≈ y∼z)
      minimal-≈ (∼-≤1 x∈≤1R xy∈R xz∈R) =
        minimal-con x∈≤1R _ _ (minimal-rol xy∈R) (minimal-rol xz∈R)

      minimal-con : ∀ {x C} → (I ⊕ KB ⊢ x ∈₁ C) → (f x ∈ ⌊ J ⌋ ⟦ C ⟧₁)
      minimal-con (∈₁-assert x∈c∈A) =
        con-≈ ⌊ J ⌋ _ (Assertions✓ J (abox KB) x∈c∈A J⊨A)
          (≈-sym ⌊ J ⌋ (fγ≈j _))
      minimal-con (∈₁-import x∈⟦c⟧) =
        ≲-resp-con ≲⌊ I≲J ⌋ x∈⟦c⟧
      minimal-con {x} {C} (∈₁-resp-∼ x∈C x∼y) =
        ⟦⟧₁-resp-≈ ⌊ J ⌋ C (minimal-con x∈C) (minimal-≈ x∼y)
      minimal-con (∈₁-subsum x∈C C⊑D∈T) =
        Axioms✓ ⌊ J ⌋ (tbox KB) C⊑D∈T J⊨T (minimal-con x∈C)
      minimal-con ∈₁-⊤-I =
        tt
      minimal-con (∈₁-⊓-I x∈C x∈D) =
        (minimal-con x∈C , minimal-con x∈D)
      minimal-con (∈₁-⊓-E₁ x∈C⊓D) =
        proj₁ (minimal-con x∈C⊓D)
      minimal-con (∈₁-⊓-E₂ x∈C⊓D) =
        proj₂ (minimal-con x∈C⊓D)
      minimal-con (∈₁-⊔-I₁ x∈C) =
        inj₁ (minimal-con x∈C)
      minimal-con (∈₁-⊔-I₂ x∈D) =
        inj₂ (minimal-con x∈D)
      minimal-con (∈₁-∀-E x∈[R]C xy∈R) =
        minimal-con x∈[R]C _ (minimal-rol xy∈R)
      minimal-con (∈₁-∃-I xy∈R y∈C) =
        (_ , minimal-rol xy∈R , minimal-con y∈C)

      minimal-rol : ∀ {x y R} → (I ⊕ KB ⊢ (x , y) ∈₂ R) →
        ((f x , f y) ∈ ⌊ J ⌋ ⟦ R ⟧₂)
      minimal-rol (∈₂-assert xy∈r∈A) =
        rol-≈ ⌊ J ⌋ _ (fγ≈j _) (Assertions✓ J (abox KB) xy∈r∈A J⊨A)
          (≈-sym ⌊ J ⌋ (fγ≈j _))
      minimal-rol (∈₂-import xy∈⟦r⟧) =
        ≲-resp-rol ≲⌊ I≲J ⌋ xy∈⟦r⟧
      minimal-rol {x} {y} {R} (∈₂-resp-∼ w∼x xy∈R y∼z) =
        ⟦⟧₂-resp-≈ ⌊ J ⌋ R (minimal-≈ w∼x) (minimal-rol xy∈R) (minimal-≈ y∼z)
      minimal-rol (∈₂-subsum xy∈Q Q⊑R∈T) =
        Axioms✓ ⌊ J ⌋ (tbox KB) Q⊑R∈T J⊨T (minimal-rol xy∈Q)
      minimal-rol (∈₂-refl x RefR∈T) =
        Axioms✓ ⌊ J ⌋ (tbox KB) RefR∈T J⊨T _
      minimal-rol (∈₂-trans xy∈R yz∈R TraR∈T) =
        Axioms✓ ⌊ J ⌋ (tbox KB) TraR∈T J⊨T
          (minimal-rol xy∈R) (minimal-rol yz∈R)
      minimal-rol (∈₂-inv-I xy∈r) =
        minimal-rol xy∈r
      minimal-rol (∈₂-inv-E xy∈r⁻) =
        minimal-rol xy∈r⁻

minimal-≋ : ∀ I KB K I≲K K⊨KB →
  (I≲K ≋ minimal-≳ I KB >> minimal-≲ I KB K I≲K K⊨KB)
minimal-≋ I KB K I≲K (K⊨T , K⊨A) = λ x → ≈-refl ⌊ K ⌋

minimal-uniq : ∀ I KB K I≲K →
  Unique I (minimal I KB) K (minimal-≳ I KB) I≲K
minimal-uniq I KB K I≲K J≲₁K J≲₂K I≲K≋I≲J≲₁K I≲K≋I≲J≲₂K (inode x) =
  ≈-trans ⌊ K ⌋ (≈-sym ⌊ K ⌋ (I≲K≋I≲J≲₁K x)) (I≲K≋I≲J≲₂K x)
minimal-uniq I KB K I≲K J≲₁K J≲₂K I≲K≋I≲J≲₁K I≲K≋I≲J≲₂K (bnode v) =
  ≈-trans ⌊ K ⌋ (≲-resp-ind J≲₁K (bnode v))
    (≈-sym ⌊ K ⌋ (≲-resp-ind J≲₂K (bnode v)))
minimal-uniq I KB K I≲K J≲₁K J≲₂K I≲K≋I≲J≲₁K I≲K≋I≲J≲₂K (enode y) =
  ≈-trans ⌊ K ⌋ (≲-resp-ind J≲₁K (enode y))
    (≈-sym ⌊ K ⌋ (≲-resp-ind J≲₂K (enode y)))

minimal-med : ∀ I KB → Mediator I (minimal I KB) (minimal-≳ I KB) KB
minimal-med I KB K I≲K K⊨KB =
  ( minimal-≲ I KB K I≲K K⊨KB
  , minimal-≋ I KB K I≲K K⊨KB
  , minimal-uniq I KB K I≲K)

minimal-init : ∀ I KB → (tbox KB ∈ μTBox) → Initial I KB (minimal I KB)
minimal-init I KB μKB =
  (minimal-≳ I KB
  , minimal-⊨ I KB μKB
  , minimal-med I KB)

_⊞_ : Interp Σ X → KB Σ (X ⊕ W ⊕ Y) → Interp Σ Y
I ⊞ KB = enode * minimal I KB

⊞-sound : ∀ I KB₁ KB₂ → (tbox KB₁ ∈ μTBox) → (I ⊞ KB₁ ⊨ KB₂) → (I ⊕ KB₁ ⊨ KB₂)
⊞-sound I KB₁ KB₂ μKB₁ ⊨KB₂ = (minimal I KB₁ , minimal-init I KB₁ μKB₁ , ⊨KB₂)

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:
------------------------------------------------------------------------
-- A simplification of Hinze.Section2-4
------------------------------------------------------------------------

module Hinze.Simplified.Section2-4 where

open import Stream.Programs
open import Stream.Equality
open import Stream.Pointwise hiding (⟦_⟧)
open import Hinze.Lemmas

open import Codata.Musical.Notation hiding (∞)
open import Data.Nat renaming (suc to 1+)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
  renaming (module ≡-Reasoning to ER)
open import Algebra.Structures
import Data.Nat.Properties as Nat
private
  module CS = IsCommutativeSemiring Nat.+-*-isCommutativeSemiring
open import Data.Product

------------------------------------------------------------------------
-- Abbreviations

2* : ℕ → ℕ
2* n = 2 * n

1+2* : ℕ → ℕ
1+2* n = 1 + 2 * n

2+2* : ℕ → ℕ
2+2* n = 2 + 2 * n

------------------------------------------------------------------------
-- Definitions

nat : Prog ℕ
nat = 0 ≺ ♯ (1+ · nat)

fac : Prog ℕ
fac = 1 ≺ ♯ (1+ · nat ⟨ _*_ ⟩ fac)

fib : Prog ℕ
fib = 0 ≺ ♯ (fib ⟨ _+_ ⟩ (1 ≺ ♯ fib))

bin : Prog ℕ
bin = 0 ≺ ♯ (1+2* · bin ⋎ 2+2* · bin)

------------------------------------------------------------------------
-- Laws and properties

const-is-∞ : ∀ {A} {x : A} {xs} →
             xs ≊ x ≺♯ xs → xs ≊ x ∞
const-is-∞ {x = x} {xs} eq =
  xs
            ≊⟨ eq ⟩
  x ≺♯ xs
            ≊⟨ refl ≺ ♯ const-is-∞ eq ⟩
  x ≺♯ x ∞
            ≡⟨ refl ⟩
  x ∞
            ∎

nat-lemma₁ : 0 ≺♯ 1+2* · nat ⋎ 2+2* · nat ≊ 2* · nat ⋎ 1+2* · nat
nat-lemma₁ =
  0 ≺♯ 1+2* · nat ⋎ 2+2* · nat
                                   ≊⟨ refl ≺ ♯ ⋎-cong
                                        (1+2* · nat) (1+2* · nat) (1+2* · nat ∎)
                                        (2+2* · nat) (2* · 1+ · nat) (lemma 2 nat) ⟩
  0 ≺♯ 1+2* · nat ⋎ 2* · 1+ · nat
                                   ≡⟨ refl ⟩
  2* · nat ⋎ 1+2* · nat
                                   ∎
  where
  lemma : ∀ m s → (λ n → m + m * n) · s ≊ _*_ m · 1+ · s
  lemma m = pointwise 1 (λ s → (λ n → m + m * n) · s)
                        (λ s → _*_ m · 1+ · s)
                        (λ n → sym (ER.begin
                           m * (1 + n)
                                          ER.≡⟨ proj₁ CS.distrib m 1 n ⟩
                           m * 1 + m * n
                                          ER.≡⟨ cong (λ x → x + m * n)
                                                     (proj₂ CS.*-identity m) ⟩
                           m + m * n
                                          ER.∎))

nat-lemma₂ : nat ≊ 2* · nat ⋎ 1+2* · nat
nat-lemma₂ =
  nat
                                        ≡⟨ refl ⟩
  0 ≺♯ 1+ · nat
                                        ≊⟨ refl ≺ ♯ ·-cong 1+ nat (2* · nat ⋎ 1+2* · nat) nat-lemma₂ ⟩
  0 ≺♯ 1+ · (2* · nat ⋎ 1+2* · nat)
                                        ≊⟨ ≅-sym (refl ≺ ♯ ⋎-map 1+ (2* · nat) (1+2* · nat)) ⟩
  0 ≺♯ 1+ · 2* · nat ⋎ 1+ · 1+2* · nat
                                        ≊⟨ refl ≺ ♯ ⋎-cong (1+ ·   2* · nat) (1+2* · nat)
                                                           (map-fusion 1+   2* nat)
                                                           (1+ · 1+2* · nat) (2+2* · nat)
                                                           (map-fusion 1+ 1+2* nat) ⟩
  0 ≺♯ 1+2* · nat ⋎ 2+2* · nat
                                        ≊⟨ nat-lemma₁ ⟩
  2* · nat ⋎ 1+2* · nat
                                        ∎

nat≊bin : nat ≊ bin
nat≊bin =
  nat
                                  ≊⟨ nat-lemma₂ ⟩
  2* · nat ⋎ 1+2* · nat
                                  ≊⟨ ≅-sym nat-lemma₁ ⟩
  0 ≺♯ 1+2* · nat ⋎ 2+2* · nat
                                  ≊⟨ refl ≺ coih ⟩
  0 ≺♯ 1+2* · bin ⋎ 2+2* · bin
                                  ≡⟨ refl ⟩
  bin
                                  ∎
  where
  coih = ♯ ⋎-cong (1+2* · nat) (1+2* · bin)
                  (·-cong 1+2* nat bin nat≊bin)
                  (2+2* · nat) (2+2* · bin)
                  (·-cong 2+2* nat bin nat≊bin)

iterate-fusion
  : ∀ {A B} (h : A → B) (f₁ : A → A) (f₂ : B → B) →
    (∀ x → h (f₁ x) ≡ f₂ (h x)) →
    ∀ x → h · iterate f₁ x ≊ iterate f₂ (h x)
iterate-fusion h f₁ f₂ hyp x =
  h · iterate f₁ x
                                ≡⟨ refl ⟩
  h x ≺♯ h · iterate f₁ (f₁ x)
                                ≊⟨ refl ≺ ♯ iterate-fusion h f₁ f₂ hyp (f₁ x) ⟩
  h x ≺♯ iterate f₂ (h (f₁ x))
                                ≡⟨ cong (λ y → ⟦ h x ≺♯ iterate f₂ y ⟧) (hyp x) ⟩
  h x ≺♯ iterate f₂ (f₂ (h x))
                                ≡⟨ refl ⟩
  iterate f₂ (h x)
                                ∎

nat-iterate : nat ≊ iterate 1+ 0
nat-iterate =
  nat
                          ≡⟨ refl ⟩
  0 ≺ ♯ (1+ · nat)
                          ≊⟨ refl ≺ ♯ ·-cong 1+ nat (iterate 1+ 0) nat-iterate ⟩
  0 ≺♯ 1+ · iterate 1+ 0
                          ≊⟨ refl ≺ ♯ iterate-fusion 1+ 1+ 1+ (λ _ → refl) 0 ⟩
  0 ≺♯ iterate 1+ 1
                          ≡⟨ refl ⟩
  iterate 1+ 0
                          ∎

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of homogeneous binary relations
------------------------------------------------------------------------

-- This file contains some core definitions which are reexported by
-- Relation.Binary or Relation.Binary.PropositionalEquality.

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

module Relation.Binary.Core where

open import Agda.Builtin.Equality using (_≡_) renaming (refl to ≡-refl)

open import Data.Maybe.Base using (Maybe)
open import Data.Product using (_×_)
open import Data.Sum.Base using (_⊎_)
open import Function using (_on_; flip)
open import Level
open import Relation.Nullary using (Dec; ¬_)

------------------------------------------------------------------------
-- Binary relations

-- Heterogeneous binary relations

REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ suc ℓ)
REL A B ℓ = A → B → Set ℓ

-- Homogeneous binary relations

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

------------------------------------------------------------------------
-- Simple properties of binary relations

infixr 4 _⇒_ _=[_]⇒_

-- Implication/containment. Could also be written ⊆.

_⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
      REL A B ℓ₁ → REL A B ℓ₂ → Set _
P ⇒ Q = ∀ {i j} → P i j → Q i j

-- Generalised implication. If P ≡ Q it can be read as "f preserves P".

_=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
          Rel A ℓ₁ → (A → B) → Rel B ℓ₂ → Set _
P =[ f ]⇒ Q = P ⇒ (Q on f)

-- A synonym, along with a binary variant.

_Preserves_⟶_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
                (A → B) → Rel A ℓ₁ → Rel B ℓ₂ → Set _
f Preserves P ⟶ Q = P =[ f ]⇒ Q

_Preserves₂_⟶_⟶_ :
  ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
  (A → B → C) → Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Set _
_+_ Preserves₂ P ⟶ Q ⟶ R =
  ∀ {x y u v} → P x y → Q u v → R (x + u) (y + v)

-- Reflexivity of _∼_ can be expressed as _≈_ ⇒ _∼_, for some
-- underlying equality _≈_. However, the following variant is often
-- easier to use.

Reflexive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Reflexive _∼_ = ∀ {x} → x ∼ x

-- Irreflexivity is defined using an underlying equality.

Irreflexive : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
              REL A B ℓ₁ → REL A B ℓ₂ → Set _
Irreflexive _≈_ _<_ = ∀ {x y} → x ≈ y → ¬ (x < y)

-- Generalised symmetry.

Sym : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
      REL A B ℓ₁ → REL B A ℓ₂ → Set _
Sym P Q = P ⇒ flip Q

Symmetric : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Symmetric _∼_ = Sym _∼_ _∼_

-- Generalised transitivity.

Trans : ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
        REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k

-- A variant of Trans.

TransFlip : ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
            REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
TransFlip P Q R = ∀ {i j k} → Q j k → P i j → R i k

Transitive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Transitive _∼_ = Trans _∼_ _∼_ _∼_

-- Generalised antisymmetry

Antisym : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} →
          REL A B ℓ₁ → REL B A ℓ₂ → REL A B ℓ₃ → Set _
Antisym R S E = ∀ {i j} → R i j → S j i → E i j

Antisymmetric : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
Antisymmetric _≈_ _≤_ = Antisym _≤_ _≤_ _≈_

Asymmetric : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)

-- Generalised connex.

Conn : ∀ {a b p q} {A : Set a} {B : Set b} → REL A B p → REL B A q → Set _
Conn P Q = ∀ x y → P x y ⊎ Q y x

Total : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Total _∼_ = Conn _∼_ _∼_

data Tri {a b c} (A : Set a) (B : Set b) (C : Set c) :
         Set (a ⊔ b ⊔ c) where
  tri< : ( a :   A) (¬b : ¬ B) (¬c : ¬ C) → Tri A B C
  tri≈ : (¬a : ¬ A) ( b :   B) (¬c : ¬ C) → Tri A B C
  tri> : (¬a : ¬ A) (¬b : ¬ B) ( c :   C) → Tri A B C

Trichotomous : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
Trichotomous _≈_ _<_ = ∀ x y → Tri (x < y) (x ≈ y) (x > y)
  where _>_ = flip _<_

Max : ∀ {a ℓ} {A : Set a} {b} {B : Set b} → REL A B ℓ → B → Set _
Max _≤_ T = ∀ x → x ≤ T

Maximum : ∀ {a ℓ} {A : Set a} → Rel A ℓ → A → Set _
Maximum = Max

Min : ∀ {a ℓ} {A : Set a} {b} {B : Set b} → REL A B ℓ → A → Set _
Min R = Max (flip R)

Minimum : ∀ {a ℓ} {A : Set a} → Rel A ℓ → A → Set _
Minimum = Min

_⟶_Respects_ : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} →
               (A → Set ℓ₁) → (B → Set ℓ₂) → REL A B ℓ₃ → Set _
P ⟶ Q Respects _∼_ = ∀ {x y} → x ∼ y → P x → Q y

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

_Respectsʳ_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} → REL A B ℓ₁ → Rel B ℓ₂ → Set _
P Respectsʳ _∼_ = ∀ {x} → (P x) Respects _∼_

_Respectsˡ_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} → REL A B ℓ₁ → Rel A ℓ₂ → Set _
P Respectsˡ _∼_ = ∀ {y} → (flip P y) Respects _∼_

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

Substitutive : ∀ {a ℓ₁} {A : Set a} → Rel A ℓ₁ → (ℓ₂ : Level) → Set _
Substitutive {A = A} _∼_ p = (P : A → Set p) → P Respects _∼_

Decidable : ∀ {a b ℓ} {A : Set a} {B : Set b} → REL A B ℓ → Set _
Decidable _∼_ = ∀ x y → Dec (x ∼ y)

WeaklyDecidable : ∀ {a b ℓ} {A : Set a} {B : Set b} → REL A B ℓ → Set _
WeaklyDecidable _∼_ = ∀ x y → Maybe (x ∼ y)

Irrelevant : ∀ {a b ℓ} {A : Set a} {B : Set b} → REL A B ℓ → Set _
Irrelevant _∼_ = ∀ {x y} (a b : x ∼ y) → a ≡ b

record NonEmpty {a b ℓ} {A : Set a} {B : Set b}
                (T : REL A B ℓ) : Set (a ⊔ b ⊔ ℓ) where
  constructor nonEmpty
  field
    {x}   : A
    {y}   : B
    proof : T x y

------------------------------------------------------------------------
-- Equivalence relations

-- The preorders of this library are defined in terms of an underlying
-- equivalence relation, and hence equivalence relations are not
-- defined in terms of preorders.

record IsEquivalence {a ℓ} {A : Set a}
                     (_≈_ : Rel A ℓ) : Set (a ⊔ ℓ) where
  field
    refl  : Reflexive _≈_
    sym   : Symmetric _≈_
    trans : Transitive _≈_

  reflexive : _≡_ ⇒ _≈_
  reflexive ≡-refl = refl


text:
{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-}

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

module Number.Base where

private
  variable
    ℓ ℓ' ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)

open import Cubical.Data.Nat renaming (ℕ to Nat)
open import Cubical.Data.Unit.Base -- Unit
open import Cubical.Data.Empty -- ⊥

open import Number.Postulates
open import Number.Bundles

data NumberKind : Type where
  isNat     : NumberKind
  isInt     : NumberKind
  isRat     : NumberKind
  isReal    : NumberKind
  isComplex : NumberKind

-- NumberKindEnumeration
NLE : NumberKind → Nat
NLE isNat     = 0
NLE isInt     = 1
NLE isRat     = 2
NLE isReal    = 3
NLE isComplex = 4

-- inverse of NumberKindEnumeration
NLE⁻¹ : Nat → NumberKind
NLE⁻¹ 0 = isNat
NLE⁻¹ 1 = isInt
NLE⁻¹ 2 = isRat
NLE⁻¹ 3 = isReal
NLE⁻¹ 4 = isComplex
NLE⁻¹ x = isComplex -- doesn't matter

-- proof of inversity
NLE⁻¹-isRetraction : ∀ x → NLE⁻¹ (NLE x) ≡ x
NLE⁻¹-isRetraction isNat     = refl
NLE⁻¹-isRetraction isInt     = refl
NLE⁻¹-isRetraction isRat     = refl
NLE⁻¹-isRetraction isReal    = refl
NLE⁻¹-isRetraction isComplex = refl

-- order lifted from Nat
open import Enumeration NLE NLE⁻¹ NLE⁻¹-isRetraction using () renaming
  ( _≤'_ to _≤ₙₗ_
  ; min' to minₙₗ
  ; max' to maxₙₗ
  ; max-implies-≤' to max-implies-≤ₙₗ₂
  ) public

data PositivityKindOrderedRing : Type where
  anyPositivityᵒʳ : PositivityKindOrderedRing
  isNonzeroᵒʳ     : PositivityKindOrderedRing
  isNonnegativeᵒʳ : PositivityKindOrderedRing
  isPositiveᵒʳ    : PositivityKindOrderedRing
  isNegativeᵒʳ    : PositivityKindOrderedRing
  isNonpositiveᵒʳ : PositivityKindOrderedRing

data PositivityKindField : Type where
  anyPositivityᶠ : PositivityKindField
  isNonzeroᶠ     : PositivityKindField

PositivityKindType : NumberKind → Type
PositivityKindType isNat     = PositivityKindOrderedRing
PositivityKindType isInt     = PositivityKindOrderedRing
PositivityKindType isRat     = PositivityKindOrderedRing
PositivityKindType isReal    = PositivityKindOrderedRing
PositivityKindType isComplex = PositivityKindField

NumberProp = Σ NumberKind PositivityKindType

module PatternsType where
  -- ordered ring patterns
  pattern X   = anyPositivityᵒʳ
  pattern X⁺⁻ = isNonzeroᵒʳ
  pattern X₀⁺ = isNonnegativeᵒʳ
  pattern X⁺  = isPositiveᵒʳ
  pattern X⁻  = isNegativeᵒʳ
  pattern X₀⁻ = isNonpositiveᵒʳ
  -- field patterns (overlapping)
  pattern X   = anyPositivityᶠ
  pattern X⁺⁻ = isNonzeroᶠ

module PatternsProp where
  -- ordered ring patterns
  pattern ⁇x⁇ = anyPositivityᵒʳ
  pattern x#0 = isNonzeroᵒʳ
  pattern 0≤x = isNonnegativeᵒʳ
  pattern 0<x = isPositiveᵒʳ
  pattern x<0 = isNegativeᵒʳ
  pattern x≤0 = isNonpositiveᵒʳ
  -- field patterns (overlapping)
  pattern ⁇x⁇ = anyPositivityᶠ
  pattern x#0 = isNonzeroᶠ

open PatternsProp

coerce-PositivityKind-OR2F : PositivityKindOrderedRing → PositivityKindField
coerce-PositivityKind-OR2F ⁇x⁇ = ⁇x⁇
coerce-PositivityKind-OR2F x#0 = x#0
coerce-PositivityKind-OR2F 0≤x = ⁇x⁇
coerce-PositivityKind-OR2F 0<x = x#0
coerce-PositivityKind-OR2F x<0 = x#0
coerce-PositivityKind-OR2F x≤0 = ⁇x⁇

coerce-PositivityKind-F2OR : PositivityKindField → PositivityKindOrderedRing
coerce-PositivityKind-F2OR ⁇x⁇ = ⁇x⁇
coerce-PositivityKind-F2OR x#0 = x#0

coerce-PositivityKind-OR2 : PositivityKindOrderedRing → (to : NumberKind) → PositivityKindType to
coerce-PositivityKind-OR2 pl isNat     = pl
coerce-PositivityKind-OR2 pl isInt     = pl
coerce-PositivityKind-OR2 pl isRat     = pl
coerce-PositivityKind-OR2 pl isReal    = pl
coerce-PositivityKind-OR2 pl isComplex = coerce-PositivityKind-OR2F pl

coerce-PositivityKind-F2 : PositivityKindField → (to : NumberKind) → PositivityKindType to
coerce-PositivityKind-F2 pl isNat     = coerce-PositivityKind-F2OR pl
coerce-PositivityKind-F2 pl isInt     = coerce-PositivityKind-F2OR pl
coerce-PositivityKind-F2 pl isRat     = coerce-PositivityKind-F2OR pl
coerce-PositivityKind-F2 pl isReal    = coerce-PositivityKind-F2OR pl
coerce-PositivityKind-F2 pl isComplex = pl

coerce-PositivityKind : (from to : NumberKind) → PositivityKindType from → PositivityKindType to
coerce-PositivityKind isNat     to x = coerce-PositivityKind-OR2 x to
coerce-PositivityKind isInt     to x = coerce-PositivityKind-OR2 x to
coerce-PositivityKind isRat     to x = coerce-PositivityKind-OR2 x to
coerce-PositivityKind isReal    to x = coerce-PositivityKind-OR2 x to
coerce-PositivityKind isComplex to x = coerce-PositivityKind-F2  x to

-- NumberKind interpretation

NumberKindLevel : NumberKind → Level
NumberKindLevel isNat     = ℕℓ
NumberKindLevel isInt     = ℤℓ
NumberKindLevel isRat     = ℚℓ
NumberKindLevel isReal    = ℝℓ
NumberKindLevel isComplex = ℂℓ

NumberKindProplevel : NumberKind → Level
NumberKindProplevel isNat     = ℕℓ'
NumberKindProplevel isInt     = ℤℓ'
NumberKindProplevel isRat     = ℚℓ'
NumberKindProplevel isReal    = ℝℓ'
NumberKindProplevel isComplex = ℂℓ'

NumberKindInterpretation : (x : NumberKind) → Type (NumberKindLevel x)
NumberKindInterpretation isNat     = let open ℕ* in ℕ
NumberKindInterpretation isInt     = let open ℤ* in ℤ
NumberKindInterpretation isRat     = let open ℚ* in ℚ
NumberKindInterpretation isReal    = let open ℝ* in ℝ
NumberKindInterpretation isComplex = let open ℂ* in ℂ

-- PositivityKind interpretation

PositivityKindInterpretation : (nl : NumberKind) → PositivityKindType nl → (x : NumberKindInterpretation nl) → Type (NumberKindProplevel nl)
PositivityKindInterpretation isNat     ⁇x⁇ x =               Unit
PositivityKindInterpretation isNat     x#0 x = let open ℕ in  x # 0f
PositivityKindInterpretation isNat     0≤x x = let open ℕ in 0f ≤  x
PositivityKindInterpretation isNat     0<x x = let open ℕ in 0f <  x
PositivityKindInterpretation isNat     x≤0 x = let open ℕ in  x ≤ 0f
PositivityKindInterpretation isNat     x<0 x =               ⊥
PositivityKindInterpretation isInt     ⁇x⁇ x =               Lift Unit
PositivityKindInterpretation isInt     x#0 x = let open ℤ in  x # 0f
PositivityKindInterpretation isInt     0≤x x = let open ℤ in 0f ≤  x
PositivityKindInterpretation isInt     0<x x = let open ℤ in 0f <  x
PositivityKindInterpretation isInt     x≤0 x = let open ℤ in  x ≤ 0f
PositivityKindInterpretation isInt     x<0 x = let open ℤ in  x < 0f
PositivityKindInterpretation isRat     ⁇x⁇ x =               Lift Unit
PositivityKindInterpretation isRat     x#0 x = let open ℚ in  x # 0f
PositivityKindInterpretation isRat     0≤x x = let open ℚ in 0f ≤  x
PositivityKindInterpretation isRat     0<x x = let open ℚ in 0f <  x
PositivityKindInterpretation isRat     x≤0 x = let open ℚ in  x ≤ 0f
PositivityKindInterpretation isRat     x<0 x = let open ℚ in  x < 0f
PositivityKindInterpretation isReal    ⁇x⁇ x =               Lift Unit
PositivityKindInterpretation isReal    x#0 x = let open ℝ in  x # 0f
PositivityKindInterpretation isReal    0≤x x = let open ℝ in 0f ≤  x
PositivityKindInterpretation isReal    0<x x = let open ℝ in 0f <  x
PositivityKindInterpretation isReal    x≤0 x = let open ℝ in  x ≤ 0f
PositivityKindInterpretation isReal    x<0 x = let open ℝ in  x < 0f
PositivityKindInterpretation isComplex ⁇x⁇ x =               Lift Unit
PositivityKindInterpretation isComplex x#0 x = let open ℂ in  x # 0f

NumberLevel : NumberKind → Level
NumberLevel l = ℓ-max (NumberKindLevel l) (NumberKindProplevel l)

-- NumberProp interpretation
NumberInterpretation : ((l , p) : NumberProp) → Type (NumberLevel l)
NumberInterpretation (level , positivity) = Σ (NumberKindInterpretation level) (PositivityKindInterpretation level positivity)

-- generic number type
data Number (p : NumberProp) : Type (NumberLevel (fst p)) where
  _,,_ : (x :  NumberKindInterpretation (fst p))
       → (PositivityKindInterpretation (fst p) (snd p) x)
       → Number p

num : ∀{(l , p) : NumberProp} → Number (l , p) → NumberKindInterpretation l
num (p ,, q) = p

prp : ∀{pp@(l , p) : NumberProp} → (x : Number pp) → PositivityKindInterpretation l p (num x)
prp (p ,, q) = q

pop : ∀{p : NumberProp} → Number p → NumberInterpretation p
pop (x ,, p) = x , p

open PatternsType

{- NOTE: overlapping patterns makes this possible:

_ : NumberProp'
_ = isRat , X⁺⁻

_ : NumberProp'
_ = isComplex , X⁺⁻

-}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Operations on and properties of decidable relations
------------------------------------------------------------------------

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

module Relation.Nullary.Decidable where

open import Level using (Level)
open import Function.Base
open import Function.Equality    using (_⟨$⟩_; module Π)
open import Function.Equivalence using (_⇔_; equivalence; module Equivalence)
open import Function.Injection   using (Injection; module Injection)
open import Relation.Binary      using (Setoid; module Setoid; Decidable)
open import Relation.Nullary

private
  variable
    p q : Level
    P : Set p
    Q : Set q

------------------------------------------------------------------------
-- Re-exporting the core definitions

open import Relation.Nullary.Decidable.Core public

------------------------------------------------------------------------
-- Maps

map : P ⇔ Q → Dec P → Dec Q
map P⇔Q = map′ (to ⟨$⟩_) (from ⟨$⟩_)
  where open Equivalence P⇔Q

module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
         (inj : Injection A B)
  where

  open Injection inj
  open Setoid A using () renaming (_≈_ to _≈A_)
  open Setoid B using () renaming (_≈_ to _≈B_)

  -- If there is an injection from one setoid to another, and the
  -- latter's equivalence relation is decidable, then the former's
  -- equivalence relation is also decidable.

  via-injection : Decidable _≈B_ → Decidable _≈A_
  via-injection dec x y =
    map′ injective (Π.cong to) (dec (to ⟨$⟩ x) (to ⟨$⟩ y))


text:
module Impossible where

-- The only way to trigger an __IMPOSSIBLE__ that isn't a bug.
{-# IMPOSSIBLE #-}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module Web.Semantic.DL.Category.Properties.Composition where

open import Web.Semantic.DL.Category.Properties.Composition.RespectsEquiv
  public using ( compose-resp-≣ )

open import Web.Semantic.DL.Category.Properties.Composition.LeftUnit
  public using ( compose-unit₁ )

open import Web.Semantic.DL.Category.Properties.Composition.RightUnit
  public using ( compose-unit₂ )

open import Web.Semantic.DL.Category.Properties.Composition.Assoc
  public using ( compose-assoc )


text:
{-# OPTIONS -v scope.import:10 #-}

import Common.Level
import Common.Level

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition of the sublist relation. This is commonly
-- known as Order Preserving Embeddings (OPE).
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Sublist.Propositional
  {a} {A : Set a} where

open import Data.List.Relation.Binary.Equality.Propositional using (≋⇒≡)
import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist
open import Data.List.Relation.Unary.Any using (Any)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Unary using (Pred)

------------------------------------------------------------------------
-- Re-export definition and operations from setoid sublists

open SetoidSublist (setoid A) public
  hiding
  (lookup; ⊆-reflexive; ⊆-antisym
  ; ⊆-isPreorder; ⊆-isPartialOrder
  ; ⊆-preorder; ⊆-poset
  )

------------------------------------------------------------------------
-- Additional operations

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

  lookup : ∀ {xs ys} → xs ⊆ ys → Any P xs → Any P ys
  lookup = SetoidSublist.lookup (setoid A) (subst _)

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

⊆-reflexive : _≡_ ⇒ _⊆_
⊆-reflexive refl = ⊆-refl

⊆-antisym : Antisymmetric _≡_ _⊆_
⊆-antisym xs⊆ys ys⊆xs = ≋⇒≡ (SetoidSublist.⊆-antisym (setoid A) xs⊆ys ys⊆xs)

⊆-isPreorder : IsPreorder _≡_ _⊆_
⊆-isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = ⊆-reflexive
  ; trans         = ⊆-trans
  }

⊆-isPartialOrder : IsPartialOrder _≡_ _⊆_
⊆-isPartialOrder = record
  { isPreorder = ⊆-isPreorder
  ; antisym    = ⊆-antisym
  }

⊆-preorder : Preorder a a a
⊆-preorder = record
  { isPreorder = ⊆-isPreorder
  }

⊆-poset : Poset a a a
⊆-poset = record
  { isPartialOrder = ⊆-isPartialOrder
  }


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

module Function where

open import Level

infixr 9 _∘_ _∘′_
_∘_ : ∀ {A : Type a} {B : A → Type b} {C : {x : A} → B x → Type c} →
        (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
        ((x : A) → C (g x))
f ∘ g = λ x → f (g x)
{-# INLINE _∘_ #-}

_∘′_ : (B → C) → (A → B) → A → C
f ∘′ g = λ x → f (g x)
{-# INLINE _∘′_ #-}

flip : ∀ {A : Type a} {B : Type b} {C : A → B → Type c} →
        ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ y x → f x y
{-# INLINE flip #-}

id : ∀ {A : Type a} → A → A
id x = x
{-# INLINE id #-}

const : A → B → A
const x _ = x
{-# INLINE const #-}

infixr -1 _$_
_$_ : ∀ {A : Type a} {B : A → Type b}
      → (∀ (x : A) → B x)
      → (x : A)
      → B x
f $ x = f x
{-# INLINE _$_ #-}

infixl 0 _|>_
_|>_ : ∀ {A : Type a} {B : A → Type b}
      → (x : A)
      → (∀ (x : A) → B x)
      → B x
_|>_ = flip _$_
{-# INLINE _|>_ #-}

infixl 1 _⟨_⟩_
_⟨_⟩_ : A → (A → B → C) → B → C
x ⟨ f ⟩ y = f x y
{-# INLINE _⟨_⟩_ #-}

infixl 0 the
the : (A : Type a) → A → A
the _ x = x
{-# INLINE the #-}

syntax the A x = x ⦂ A

infix 0 case_of_
case_of_ : A → (A → B) → B
case x of f = f x
{-# INLINE case_of_ #-}

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module FileNotFound where

import A.B.WildGoose


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

open import HoTT
open import groups.KernelImage

module cohomology.ChainComplex where

  record ChainComplex i : Type (lsucc i) where
    field
      head : AbGroup i
      chain : ℕ → AbGroup i
      augment : AbGroup.grp (chain 0) →ᴳ AbGroup.grp head
      boundary : ∀ n → (AbGroup.grp (chain (S n)) →ᴳ AbGroup.grp (chain n))

  record CochainComplex i : Type (lsucc i) where
    field
      head : AbGroup i
      cochain : ℕ → AbGroup i
      augment : AbGroup.grp head →ᴳ AbGroup.grp (cochain 0)
      coboundary : ∀ n → (AbGroup.grp (cochain n) →ᴳ AbGroup.grp (cochain (S n)))

  homology-group : ∀ {i} → ChainComplex i
    → (n : ℤ) → Group i
  homology-group cc (pos 0) = Ker/Im cc.augment (cc.boundary 0) (snd (cc.chain 0))
    where module cc = ChainComplex cc
  homology-group cc (pos (S n)) = Ker/Im (cc.boundary n) (cc.boundary (S n)) (snd (cc.chain (S n)))
    where module cc = ChainComplex cc
  homology-group {i} cc (negsucc _) = Lift-group {j = i} Unit-group

  cohomology-group : ∀ {i} → CochainComplex i
    → (n : ℤ) → Group i
  cohomology-group cc (pos 0) = Ker/Im (cc.coboundary 0) cc.augment (snd (cc.cochain 0))
    where module cc = CochainComplex cc
  cohomology-group cc (pos (S n)) = Ker/Im (cc.coboundary (S n)) (cc.coboundary n) (snd (cc.cochain (S n)))
    where module cc = CochainComplex cc
  cohomology-group {i} cc (negsucc _) = Lift-group {j = i} Unit-group

  complex-dualize : ∀ {i j} → ChainComplex i → AbGroup j
    →  CochainComplex (lmax i j)
  complex-dualize {i} {j} cc G = record {M} where
    module cc = ChainComplex cc
    module M where
      head : AbGroup (lmax i j)
      head = hom-abgroup (AbGroup.grp cc.head) G

      cochain : ℕ → AbGroup (lmax i j)
      cochain n = hom-abgroup (AbGroup.grp (cc.chain n)) G

      augment : AbGroup.grp head →ᴳ AbGroup.grp (cochain 0)
      augment = pre∘ᴳ-hom G cc.augment

      coboundary : ∀ n → (AbGroup.grp (cochain n) →ᴳ AbGroup.grp (cochain (S n)))
      coboundary n = pre∘ᴳ-hom G (cc.boundary n)

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
{-# OPTIONS -v tc.lhs.shadow:30 #-}

{-# OPTIONS --copatterns #-}

module PatternShadowsConstructor4 where

module A where

  data B : Set where
    x : B

  data C : Set where
    c : B → C

open A using (C; c)

record R : Set where
  field
    fst : C → C
    snd : A.B
open R

r : R
fst r (c x) = x
snd r       = A.B.x

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Logic.WeaklyClassical where

import      Lvl
open import Functional
open import Logic.Names
open import Logic.Predicate
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Type

private variable ℓ : Lvl.Level
private variable T X Y : Type{ℓ}
private variable P : T → Type{ℓ}

-- TODO: What should (¬¬ P → P) for a P be called? DoubleNegation? Stable proposition?

[⊤]-doubleNegation : DoubleNegationOn(⊤)
[⊤]-doubleNegation = const [⊤]-intro

[⊥]-doubleNegation : DoubleNegationOn(⊥)
[⊥]-doubleNegation = apply id

[¬]-doubleNegation : DoubleNegationOn(¬ X)
[¬]-doubleNegation = _∘ apply

[∧]-doubleNegation : DoubleNegationOn(X) → DoubleNegationOn(Y) → DoubleNegationOn(X ∧ Y)
[∧]-doubleNegation nnxx nnyy nnxy = [∧]-intro (nnxx(nx ↦ nnxy(nx ∘ [∧]-elimₗ))) (nnyy(ny ↦ nnxy(ny ∘ [∧]-elimᵣ)))

[→]-doubleNegation : DoubleNegationOn(Y) → DoubleNegationOn(X → Y)
[→]-doubleNegation nnyy nnxy x = nnyy(ny ↦ nnxy(xy ↦ (ny ∘ xy) x))

[∀]-doubleNegation-distribute : (∀{x} → DoubleNegationOn(P(x))) → DoubleNegationOn(∀{x} → P(x))
[∀]-doubleNegation-distribute annp nnap = annp(npx ↦ nnap(npx $_))

doubleNegation-to-callCC : DoubleNegationOn(X) → DoubleNegationOn(Y) → (((X → Y) → X) → X)
doubleNegation-to-callCC dx dy xyx = dx(nx ↦ nx(xyx(dy ∘ const ∘ nx)))

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:
-- Solutions to ExerciseSession2
{-# OPTIONS --cubical #-}
module SolutionsSession2 where

open import Part1
open import Part2
open import ExerciseSession1

-- Exercise 1
JEq : {x : A} (P : (z : A) → x ≡ z → Type ℓ'')
      (d : P x refl) → J P d refl ≡ d
JEq P p d = transportRefl p d

-- Exercise 2
isContr→isProp : isContr A → isProp A
isContr→isProp (x , p) a b = sym (p a) ∙ p b

-- Exercise 3
isProp→isProp' : isProp A → isProp' A
isProp→isProp' p x y = p x y , isProp→isSet p _ _ (p x y)

-- Exercise 4
isContr→isContr≡ : isContr A → (x y : A) → isContr (x ≡ y)
isContr→isContr≡ h = isProp→isProp' (isContr→isProp h)

-- Exercise 5
fromPathP : {A : I → Type ℓ} {x : A i0} {y : A i1}
          → PathP A x y
          → transport (λ i → A i) x ≡ y
fromPathP {A = A} p i = transp (λ j → A (i ∨ j)) i (p i)

-- The converse is harder to prove so we give it:
toPathP : {A : I → Type ℓ} {x : A i0} {y : A i1}
        → transport (λ i → A i) x ≡ y
        → PathP A x y
toPathP {A = A} {x = x} p i =
  hcomp (λ j → λ { (i = i0) → x
                 ; (i = i1) → p j })
        (transp (λ j → A (i ∧ j)) (~ i) x)

-- Exercise 6
Σ≡Prop : {B : A → Type ℓ'} {u v : Σ A B} (h : (x : A) → isProp (B x))
       → (p : fst u ≡ fst v) → u ≡ v
Σ≡Prop {B = B} {u = u} {v = v} h p =
  ΣPathP (p , toPathP (h _ (transport (λ i → B (p i)) (snd u)) (snd v)))

-- Exercice 7 (thanks Loïc for the slick proof!)
isPropIsContr : isProp (isContr A)
isPropIsContr (c0 , h0) (c1 , h1) j =
  h0 c1 j , λ y i → hcomp (λ k → λ { (i = i0) → h0 (h0 c1 j) k;
                                     (i = i1) → h0 y k;
                                     (j = i0) → h0 (h0 y i) k;
                                     (j = i1) → h0 (h1 y i) k}) c0

-- Exercises about Part 3:

-- Exercise 8 (a bit longer, but very good):

open import Cubical.Data.Nat
open import Cubical.Data.Int hiding (addEq ; subEq)

-- Compose sucPathInt with itself n times. Transporting along this
-- will be addition, transporting with it backwards will be subtraction.

-- a) Define a path "addEq n" by composing sucPathInt with itself n
-- times.
addEq : ℕ → Int ≡ Int
addEq zero = refl
addEq (suc n) = (addEq n) ∙ sucPathInt

-- b) Define another path "subEq n" by composing "sym sucPathInt" with
-- itself n times.
subEq : ℕ → Int ≡ Int
subEq zero = refl
subEq (suc n) = (subEq n) ∙ sym sucPathInt

-- c) Define addition on integers by pattern-matching and transporting
-- along addEq/subEq appropriately.
_+Int_ : Int → Int → Int
m +Int pos n    = transport (addEq n) m
m +Int negsuc n = transport (subEq (suc n)) m

-- d) Do some concrete computations using _+Int_ (this would not work
-- in HoTT as the transport would be stuck!)

-- Exercise 9: prove that hSet is not an hSet

open import Cubical.Data.Bool renaming (notEq to notPath)
open import Cubical.Data.Empty

-- Just define hSets of level 0 for simplicity
hSet : Type₁
hSet = Σ[ A ∈ Type₀ ] isSet A

-- Bool is an hSet
BoolSet : hSet
BoolSet = Bool , isSetBool

notPath≢refl : (notPath ≡ refl) → ⊥
notPath≢refl e = true≢false (transport (λ i → transport (e i) true ≡ false) refl)

¬isSet-hSet : isSet hSet → ⊥
¬isSet-hSet h = notPath≢refl (cong (cong fst) (h BoolSet BoolSet p refl))
 where
 p : BoolSet ≡ BoolSet
 p = Σ≡Prop (λ A → isPropIsSet {A = A}) notPath

-- Exercise 10: squivalence between FinData and Fin

-- Thanks to Elies for the PR with the code. On the development
-- version of the library there is now:
--
-- open import Cubical.Data.Fin using (FinData≡Fin)


text:
open import x1-Base

module x2-Sort
         {X    : Set}
         {_≈_  : Rel X}
         {_≤_  : Rel X}
         (_≤?_ : Decidable _≤_)
         (ord  : TotalOrder _≈_ _≤_)
  where
open TotalOrder  ord         using (total; equivalence)
open Equivalence equivalence using (refl)

-- represent bounded lists, but want bounds to be open
-- so lift X in a type that contains a top and bottom elements
data ⊥X⊤ : Set where
  ⊤ ⊥ : ⊥X⊤
  ⟦_⟧ : X → ⊥X⊤

-- lift ordering to work with ⊥X⊤
data _≤̂_ : Rel ⊥X⊤ where
  ⊥≤̂     : ∀ {x} → ⊥ ≤̂ x
  ≤̂⊤     : ∀ {x} → x ≤̂ ⊤
  ≤-lift : ∀ {x y} → x ≤ y → ⟦ x ⟧ ≤̂ ⟦ y ⟧

-- bounded, ordered lists
-- elements ordered according to ≤ relation
data OList (l u : ⊥X⊤) : Set where
  -- nil works with any bounds l ≤ u
  nil  : l ≤̂ u
       → OList l u
  -- cons x to a list with x as a lower bound,
  -- return a list with lower bound l, l ≤̂ ⟦ x ⟧
  cons : ∀ x
         (xs : OList ⟦ x ⟧ u)
       → l ≤̂ ⟦ x ⟧
       → OList l u

toList : ∀ {l u} → OList l u → List X
toList (nil _)       = []
toList (cons x xs _) = x ∷ toList xs

insert : ∀ {l u} x
       → OList l           u
       →       l ≤̂ ⟦ x ⟧
       →           ⟦ x ⟧ ≤̂ u
       → OList l           u
insert x   (nil _)             l≤̂⟦x⟧ ⟦x⟧≤̂u =
  cons x  (nil ⟦x⟧≤̂u)
          l≤̂⟦x⟧

insert x L@(cons x' xs l≤̂⟦x'⟧) l≤̂⟦x⟧ ⟦x⟧≤̂u with x ≤? x'
... | left   x≤x'        =
  cons x  (cons   x' xs (≤-lift x≤x'))
          l≤̂⟦x⟧
... | (right x≤x'→Empty) =
  cons x' (insert x  xs ([ ≤-lift
                         , (λ y≤x → absurd (x≤x'→Empty y≤x)) ]
                         (total x' x))
                        ⟦x⟧≤̂u)
          l≤̂⟦x'⟧

-- Insertion sort uses OList ⊥ ⊤ to represent a sorted list with open bounds:
isort' : List X → OList ⊥ ⊤
isort' = foldr (λ x xs → insert x xs ⊥≤̂ ≤̂⊤) (nil ⊥≤̂)

isort : List X → List X
isort xs = toList (isort' xs)

------------------------------------------------------------------------------
-- Tree sort (more efficient)

-- bounded, ordered binary tree
data Tree (l u : ⊥X⊤) : Set where
  leaf : l ≤̂ u
       → Tree l       u
  node : (x : X)
       → Tree l ⟦ x ⟧
       → Tree   ⟦ x ⟧ u
       → Tree l       u

t-insert : ∀ {l u}
         → (x : X)
         → Tree l       u
         →      l   ≤̂ ⟦ x ⟧
         →    ⟦ x ⟧ ≤̂   u
         → Tree l       u
t-insert x (leaf _)       l≤x x≤u =
  node x    (leaf l≤x) (leaf x≤u)
t-insert x (node y ly yu) l≤x x≤u with x ≤? y
... | left x≤y  =
  node y    (t-insert x ly l≤x (≤-lift x≤y)) yu
... | right x>y =
  node y ly (t-insert x yu ([ (λ x≤y → absurd (x>y x≤y)) , ≤-lift ] (total x y)) x≤u)

t-fromList : List X → Tree ⊥ ⊤
t-fromList = foldr (λ x xs → t-insert x xs ⊥≤̂ ≤̂⊤) (leaf ⊥≤̂)

-- OList concatenation, including inserting a new element in the middle
_⇒_++_ : ∀ {l u} x
       → OList l ⟦ x ⟧
       → OList   ⟦ x ⟧ u
       → OList l      u
x ⇒ nil l≤u       ++ xu = cons x            xu  l≤u
x ⇒ cons y yx l≤y ++ xu = cons y (x ⇒ yx ++ xu) l≤y

t-flatten : ∀ {l u} → Tree l u → OList l u
t-flatten (leaf l≤u)     = (nil l≤u)
t-flatten (node x lx xu) = x ⇒ t-flatten lx ++ t-flatten xu

t-sort' : List X → OList ⊥ ⊤
t-sort' xs = t-flatten (foldr (λ x xs → t-insert x xs ⊥≤̂ ≤̂⊤) (leaf ⊥≤̂) xs)

t-sort : List X → List X
t-sort xs = toList (t-sort' xs)

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
{-# OPTIONS --prop --rewriting --confluence-check #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

postulate
  A : Prop
  a : A
  B : Set
  b : B
  f : A → B → Set₁
  g : B → Set₁

  rew₁ : ∀ y → f a y ≡ g y
  rew₂ : ∀ x → f x b ≡ Set
  rew₃ : ∀ y → g y ≡ Set

{-# REWRITE rew₁ rew₂ rew₃ #-}


text: test = forall (_Set_ : Set) → Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Functor.Instance.SetoidDiscrete where

-- Discrete Functor
--   from Setoids to Cats.

open import Categories.Category
open import Categories.Functor
open import Categories.Category.Instance.Setoids
open import Categories.Category.Instance.Cats
open import Categories.NaturalTransformation.NaturalIsomorphism
  hiding (refl)
import Categories.Category.SetoidDiscrete as D

open import Relation.Binary
open import Function renaming (id to idf; _∘_ to _●_)
open import Function.Equality renaming (id to id⟶)

Discrete : ∀ {o ℓ e} → Functor (Setoids o ℓ) (Cats o ℓ e)
Discrete {o} {ℓ} {e} = record
   { F₀ = D.Discrete
   ; F₁ = DiscreteFunctor
   ; identity = λ {A} → DiscreteId {A}
   ; homomorphism = λ {X} {Y} {Z} {g} {h} → PointwiseHom {X} {Y} {Z} {g} {h}
   ; F-resp-≈ = λ {A} {B} {f} {g} → ExtensionalityNI {A} {B} {f} {g}
   }
   where
     DiscreteFunctor : {A B : Setoid o ℓ} → (A ⟶ B) → Cats o ℓ e [ D.Discrete A , D.Discrete B ]
     DiscreteFunctor f = record
       { F₀ = f ⟨$⟩_
       ; F₁ = cong f
       ; identity = _
       ; homomorphism = _
       ; F-resp-≈ = _
       }
     DiscreteId : {A : Setoid o ℓ} → NaturalIsomorphism (DiscreteFunctor {A} id⟶) id
     DiscreteId {A} = record
       { F⇒G = record { η = λ _ → refl ; commute = _ }
       ; F⇐G = record { η = λ _ → refl ; commute = _ }
       } where open Setoid A
     PointwiseHom : {X Y Z : Setoid o ℓ} {g : X ⟶ Y} {h : Y ⟶ Z} →
       NaturalIsomorphism (DiscreteFunctor (h ∘ g)) (DiscreteFunctor h ∘F DiscreteFunctor g)
     PointwiseHom {_} {_} {Z} = record
       { F⇒G = record { η = λ _ → refl }
       ; F⇐G = record { η = λ _ → refl }
       }
       where open Setoid Z
     ExtensionalityNI : {A B : Setoid o ℓ} {f g : A ⟶ B} → let open Setoid A in
      ({x y : Carrier} → x ≈ y → Setoid._≈_ B (f ⟨$⟩ x) (g ⟨$⟩ y)) →
      NaturalIsomorphism (DiscreteFunctor f) (DiscreteFunctor g)
     ExtensionalityNI {A} {B} cong≈ = record
       { F⇒G = record { η = λ X → cong≈ A.refl }
       ; F⇐G = record { η = λ X → B.sym (cong≈ A.refl) }
       }
       where
       module A = Setoid A
       module B = Setoid B

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
module plfa.part1.Relations where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)

-- z≤n, s≤s       - constructor names (with no spaces)
-- zero ≤ n       - types (with spaces) indexed by
-- suc m ≤ suc n  - 2 naturals: m and n
-- "-----------"  - is just a comment (to make it look
--                  like math notation for inference rule)

data _≤_ : ℕ → ℕ → Set where

  -- base case
  z≤n : ∀ {n : ℕ}
        -------------
      → zero ≤ n

  -- inductive case
  s≤s : ∀ {m n : ℕ}
      → m ≤ n
        -------------
      → suc m ≤ suc n

-- Base case: for all naturals n, the constructor
-- z≤n produces evidence that zero ≤ n holds.

-- Inductive case: for all naturals m and n,
-- the constructor s≤s takes evidence that m ≤ n
-- holds into evidence that suc m ≤ suc n holds.

_ : 2 ≤ 4
_ = s≤s (s≤s z≤n)

--   z≤n -----
--       0 ≤ 2
--  s≤s -------
--       1 ≤ 3
-- s≤s ---------
--       2 ≤ 4

-- We can provide implicit arguments
-- explicitly by writing them inside curly braces

_ : 2 ≤ 4
_ = s≤s {1} {3} (s≤s {0} {2} (z≤n {2}))

--     2 ≤     4
-- suc m ≤ suc n
-- suc 1 ≤ suc 3

-- One may also identify implicit arugments by name

_ : 2 ≤ 4
_ = s≤s {n = 3} (s≤s {n = 2} z≤n)

-- Precedence

infix 4 _≤_

inv-s≤s : ∀ {m n : ℕ}
  → suc m ≤ suc n
    --------------
  → m ≤ n
inv-s≤s (s≤s m≤n) = m≤n

inv-z≤n : ∀ {m : ℕ}
  → m ≤ zero
    --------
  → m ≡ zero
inv-z≤n z≤n = refl
    --  z≤n : zero ≤ n
    --  z≤n : zero ≤ (n : ℕ)
    --               (zero : ℕ)
    --  z≤n : zero ≤ zero
    -- refl :    m ≡ m
    -- refl : zero ≡ zero

max_stars_repo_name: vyorkin/plfa

max_issues_repo_name: vyorkin/plfa

max_forks_repo_name: vyorkin/plfa


text:
module Type{ℓ} where

open import Agda.Primitive public
  using ()
  renaming (Set to TYPE ; Setω to Typeω)

Type : TYPE(_)
Type = TYPE(ℓ)
{-# INLINE Type #-}

module Type where
  -- Returns the type of a certain value
  of : ∀{T : Type} → T → Type
  of {T} _ = T
  {-# INLINE of #-}


text:
module _ where

open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

postulate
  A : Set

module _ (X : Set) where

  macro
    give : Name → Term → TC ⊤
    give x goal = unify (def x []) goal

  B : Set
  B = give A


text:
{-# OPTIONS --copatterns #-}
module Issue1290 where

record R : Set1 where
  constructor con
  field
    A : Set
open R

postulate
  X : Set

x : R
A x = X

exp : R -> R
A (exp x) = A x


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

-- The Category of "Families of Setoids"
-- This fits into this library much better than the Families of Sets

-- This particular formalization should be considered alpha, i.e. its
-- names will change once things settle.

open import Level
open import Relation.Binary
  using (Rel; Setoid; module Setoid; Reflexive; Symmetric; Transitive)
open import Function.Base renaming (id to idf; _∘_ to _⊚_)
open import Function.Equality
open import Function.Inverse using (_InverseOf_)
import Relation.Binary.Reasoning.Setoid as SetoidR

open import Categories.Category

module _ {a b c d : Level} where
  record Fam : Set (suc (a ⊔ b ⊔ c ⊔ d)) where
    constructor fam
    open Setoid using () renaming (Carrier to ∣_∣; _≈_ to _≈≈_)
    field
      U : Setoid a b
    open Setoid U hiding (Carrier)
    field
      T : ∣ U ∣ → Setoid c d
      reindex : {x y : ∣ U ∣} (P : x ≈ y) → T y ⟶ T x

      -- the following coherence laws are needed to make _≃_ below an equivalence
      reindex-refl : {x : ∣ U ∣} {bx : ∣ T x ∣} → _≈≈_ (T x) (reindex refl ⟨$⟩ bx) bx
      reindex-sym : {x y : ∣ U ∣} → (p : x ≈ y) → (reindex (sym p)) InverseOf (reindex p)
      reindex-trans : {x y z : ∣ U ∣} {b : ∣ T z ∣} → (p : x ≈ y) → (q : y ≈ z) →
        Setoid._≈_ (T x) (reindex (trans p q) ⟨$⟩ b)
                         (reindex p ∘ reindex q ⟨$⟩ b)
  open Fam

  record Hom (B B′ : Fam) : Set (a ⊔ b ⊔ c ⊔ d) where
    constructor fhom
    open Setoid (U B) using (_≈_)
    field
      map : U B ⟶ U B′
      transport : (x : Setoid.Carrier (U B)) → T B x ⟶ T B′ (map ⟨$⟩ x)
      transport-coh : {x y : Setoid.Carrier (U B)} → (p : x ≈ y) →
        Setoid._≈_ (T B y ⇨ T B′ (map ⟨$⟩ x))
          (transport x ∘ reindex B p)
          (reindex B′ (Π.cong map p) ∘ transport y)

  record _≈≈_ {X Y} (F F′ : (Hom X Y)) : Set (a ⊔ b ⊔ c ⊔ d) where
    constructor feq
    open Hom
    open Setoid (U X) renaming (Carrier to A) hiding (refl; _≈_)
    open Setoid (U Y)
    -- the order below is chosen to simplify some of the later reasoning
    field
      g≈f : {x : A} → map F ⟨$⟩ x ≈ map F′ ⟨$⟩ x
      φ≈γ : {x : A} → let C = T X x
                          D = T Y (map F ⟨$⟩ x) in
            {bx : Setoid.Carrier C} → Setoid._≈_ D ((reindex Y g≈f ∘ transport F′ x) ⟨$⟩ bx) (transport F x ⟨$⟩ bx)

  fam-id : {A : Fam} → Hom A A
  fam-id {A} = fhom id (λ _ → id) λ p x≈y → Π.cong (reindex A p) x≈y
  comp : {A B C : Fam} → Hom B C → Hom A B → Hom A C
  comp {B = B} {C} (fhom map₀ trans₀ coh₀) (fhom map₁ trans₁ coh₁) =
    fhom (map₀ ∘ map₁) (λ x → trans₀ (map₁ ⟨$⟩ x) ∘ (trans₁ x))
         λ {a} {b} p {x} {y} x≈y →
           let open Setoid (T C (map₀ ∘ map₁ ⟨$⟩ a)) renaming (trans to _⟨≈⟩_) in
           Π.cong (trans₀ (map₁ ⟨$⟩ a)) (coh₁ p x≈y) ⟨≈⟩
           coh₀ (Π.cong map₁ p) (Setoid.refl (T B (map₁ ⟨$⟩ b)))

  ≈≈-refl : ∀ {A B} → Reflexive (_≈≈_ {A} {B})
  ≈≈-refl {B = B} = feq refl (reindex-refl B)
    where open Setoid (U B)

  ≈≈-sym : ∀ {A B} → Symmetric (_≈≈_ {A} {B})
  ≈≈-sym {A} {B} {F} {G} (feq g≈f φ≈γ) = feq (sym g≈f)
    λ {x} {bx} → Setoid.trans ( T B (map G ⟨$⟩ x) )
      (Π.cong (reindex B (sym g≈f)) (Setoid.sym (T B (map F ⟨$⟩ x)) φ≈γ))
      (left-inverse-of (reindex-sym B g≈f) (transport G x ⟨$⟩ bx))
    where
    open Setoid (U B) using (sym; Carrier)
    open Hom
    open _InverseOf_

  ≈≈-trans : ∀ {A B} → Transitive (_≈≈_ {A} {B})
  ≈≈-trans {A} {B} {F} {G} {H}  (feq ≈₁ t₁) (feq ≈₂ t₂) =
    feq (trans ≈₁ ≈₂) (λ {x} {bx} →
      let open Setoid (T B (Hom.map F ⟨$⟩ x)) renaming (trans to _⟨≈⟩_) in
      reindex-trans B ≈₁ ≈₂ ⟨≈⟩ (Π.cong (reindex B ≈₁) t₂ ⟨≈⟩ t₁))
    where
    open Setoid (U B) using (trans)

  comp-resp-≈≈ : {A B C : Fam} {f h : Hom B C} {g i : Hom A B} →
      f ≈≈ h → g ≈≈ i → comp f g ≈≈ comp h i
  comp-resp-≈≈ {A} {B} {C} {f} {h} {g} {i} (feq f≈h t-f≈h) (feq g≈i t-g≈i) =
    feq (trans (Π.cong (map f) g≈i) f≈h)
        λ {x} → let open Setoid (T C (map (comp f g) ⟨$⟩ x)) renaming (trans to _⟨≈⟩_; sym to ≈sym) in
        reindex-trans C (cong (map f) g≈i) f≈h ⟨≈⟩
        (Π.cong (reindex C (cong (map f) g≈i)) t-f≈h ⟨≈⟩
        (≈sym (transport-coh {B} {C} f g≈i (Setoid.refl (T B (map i ⟨$⟩ x)))) ⟨≈⟩
        Π.cong (transport f (map g ⟨$⟩ x)) t-g≈i))
    where
    open _≈≈_
    open Setoid (U C)
    open Hom

  Cat : Category (suc (a ⊔ b ⊔ c ⊔ d)) (a ⊔ b ⊔ c ⊔ d) (a ⊔ b ⊔ c ⊔ d)
  Cat = record
    { Obj = Fam
    ; _⇒_ = Hom
    ; _≈_ = _≈≈_
    ; id = fam-id
    ; _∘_ = comp
    ; assoc     = λ {_} {_} {_} {_} {f} {g} {h} → assoc′ {f = f} {g} {h}
    ; sym-assoc = λ {_} {_} {_} {_} {f} {g} {h} → ≈≈-sym (assoc′ {f = f} {g} {h})
    ; identityˡ = λ {_} {B} → feq (Setoid.refl (U B)) (reindex-refl B)
    ; identityʳ = λ {_} {B} → feq (Setoid.refl (U B)) (reindex-refl B)
    ; identity² = λ {A} → feq (Setoid.refl (U A)) (reindex-refl A)
    ; equiv = λ {A} {B} → let open Setoid (U B) in record
      { refl = ≈≈-refl
      ; sym = ≈≈-sym
      ; trans = ≈≈-trans
      }
    ; ∘-resp-≈ = comp-resp-≈≈
    }
    where
    open _InverseOf_
    assoc′ : {A B C D : Fam} {f : Hom A B} {g : Hom B C} {h : Hom C D} →
      comp (comp h g) f ≈≈ comp h (comp g f)
    assoc′ {D = D} = feq (Setoid.refl (U D)) (reindex-refl D)

  open Category Cat public

FamilyOfSetoids : ∀ a b c d → Category (suc (a ⊔ b ⊔ c ⊔ d)) (a ⊔ b ⊔ c ⊔ d) (a ⊔ b ⊔ c ⊔ d)
FamilyOfSetoids a b c d = Cat {a} {b} {c} {d}

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- | In this module, we proof that the 2-category of endofunctors
-- inherits locally all colimits from underlying category.
-- More precisely, for a functor F : C → C, we compute in Endo(F, F)
-- colimits point-wise from those in C.
module UpToColim where

open import Level
open import Relation.Binary using (Rel; IsEquivalence)
open import Data.Product
open import Categories.Support.Equivalence
open import Categories.Category
open import Categories.2-Category
open import Categories.Functor
open import Categories.NaturalTransformation
  renaming (id to natId; _≡_ to _≡N_; setoid to natSetoid)
  hiding (_∘ˡ_; _∘ʳ_)
open import Categories.Support.EqReasoning
open import Categories.Colimit
open import Categories.Cocones
open import Categories.Cocone
open import Categories.Object.Initial
open import Categories.Functor.Constant

open import NaturalTransFacts
open import UpTo

-- _⇒_ = NaturalTransformation

EndoDiagram : (C : Cat₀) → (F : EndoFunctor C) → (I : Cat₀) → Set
EndoDiagram C F I = Functor I (EndoMor (C , F) (C , F))

PW-Diagram : {C : Cat₀} → {F : EndoFunctor C} → {I : Cat₀} →
             EndoDiagram C F I → (X : Category.Obj C) →
             Functor I C
PW-Diagram {C} {F} {I} D X =
  record
  { F₀ = λ i → Functor.F₀ (Endo⇒.T (D.F₀ i)) X
  ; F₁ = λ h → NaturalTransformation.η (UpTo⇒.γ (D.F₁ h)) X
  ; identity = ≡U-proof D.identity
  ; homomorphism = ≡U-proof D.homomorphism
  ; F-resp-≡ = λ x → ≡U-proof (D.F-resp-≡ x)
  }
  where
    module C = Category C
    module D = Functor D
    module I = Category I
    open _≡U_

EndoMor-inherit-colim : {C : Cat₀} → (F : EndoFunctor C) →
                        {I : Cat₀} → (D : EndoDiagram C F I) →
                        ((X : Category.Obj C) → Colimit (PW-Diagram D X)) →
                        Colimit D
EndoMor-inherit-colim {C} F {I} D c =
  record
  { initial = record
    { ⊥ = colim-D
    ; ! = out
    ; !-unique = out-unique
    }
  }
  where
    -- Notations

    module C = Category C
    module I = Category I
    module CC-D = Category (Cocones D)

    -- Components of F
    F₀ = Functor.F₀ F
    F₁ = Functor.F₁ F

    -- Components of the diagram D
    D₀ = Functor.F₀ D
    D₁ = Functor.F₁ D

    -- Tᵢ = π₁(D(i))
    T : (i : I.Obj) → Functor C C
    T i = Endo⇒.T (D₀ i)

    -- Components of T
    T₀ = λ i → Functor.F₀ (T i)
    T₁ = λ i {A} {B} → Functor.F₁ (T i) {A} {B}

    -- ρ‌ᵢA = π₂(D(i))
    ρ : (i : I.Obj) → (T i ∘ F) ⇒ (F ∘ T i)
    ρ i = Endo⇒.ρ (D₀ i)

    ρη : (i : I.Obj) → (A : C.Obj) → C [ T₀ i (F₀ A) , F₀ (T₀ i A) ]
    ρη i A = NaturalTransformation.η (ρ i) A

    -- The natural transformation (w/o proof) D(f) : D(i) ⇒ D(i)
    D₁η : ∀ {i j} → (f : I [ i , j ]) →
          (A : C.Obj) → C [ T₀ i A , T₀ j A ]
    D₁η f A = NaturalTransformation.η (UpTo⇒.γ (D₁ f)) A

    ----- Construction of the colimit -----
    -- It is given by the cocone (colim-T, ρ).

    -- Action of colim-T on objects
    colim-T₀ : C.Obj → C.Obj
    colim-T₀ A = CL.∃F
      where
        module CL = Colimit (c A)

    -- Injection into colim DX
    κ : (i : I.Obj) → (X : C.Obj) → C [ T₀ i X , Colimit.∃F (c X) ]
    κ i X = Colimit.Ic.ψ (c X) i

    -- Given a morphism u : A → B in C, we construct a cocone DA ⇒ colim DB,
    -- which will give us then T(u) by the universal property of colim DA.
    -- The components of the cocone are given by κBᵢ ∘ Tᵢ(u) : T₁(A) → colim DB,
    -- where we use that Tᵢ(A) = DA(i).
    cocone-T₁ : {A B : C.Obj} →
                C [ A , B ] → Category.Obj (Cocones (PW-Diagram D A))
    cocone-T₁ {A} {B} u = record
      { N = colim-T₀ B
      ; ψ = λ i → C [ κB i ∘ T₁ i u ]
      ; commute = comm
      }
      where
        module CA = Colimit (c A)
        module PW-Cocones-A = Category (Cocones (PW-Diagram D A))
        module CB = Colimit (c B)
        DA = PW-Diagram D A
        module DA = Functor DA
        DB = PW-Diagram D B
        module DB = Functor DB

        -- Injection into colim DB
        κB : (i : I.Obj) → C [ T₀ i B , CB.∃F ]
        κB i = NaturalTransformation.η CB.ι i

        .comm : {i j : I.Obj} (f : I [ i , j ]) →
                C [ κB i ∘ T₁ i u ] C.≡ C [ κB j ∘ T₁ j u ] C.∘ DA.F₁ f
        comm {i} {j} f =
          begin
            C [ κB i ∘ T₁ i u ]
          ↓⟨ C.∘-resp-≡ˡ (Colimit.Ic.commute (c B) f) ⟩
            (κB j C.∘ DB.F₁ f) C.∘ T₁ i u
          ↓⟨ C.assoc ⟩
            κB j C.∘ (DB.F₁ f C.∘ T₁ i u)
          ↓⟨ C.∘-resp-≡ʳ
             (NaturalTransformation.commute (UpTo⇒.γ (D₁ f)) u)
          ⟩
            κB j C.∘ (T₁ j u C.∘ DA.F₁ f)
          ↑⟨ C.assoc ⟩
            C [ κB j ∘ T₁ j u ] C.∘ DA.F₁ f
          ∎
          where
            open SetoidReasoning (C.hom-setoid {DA.F₀ i} {colim-T₀ B})

    -- Action of colim-T on morphisms
    colim-T₁ : {A B : C.Obj} → C [ A , B ] → C [ colim-T₀ A , colim-T₀ B ]
    colim-T₁ {A} {B} u = CoconeMorphism.f (CA.I.! {cocone-T₁ u})
      where
        module CA = Colimit (c A)

    -- Proof that T(id_A) = id_{T(A)}
    .colim-T-id : ∀ {A : C.Obj} →
                 C [ colim-T₁ (C.id {A}) ≡ C.id {colim-T₀ A} ]
    colim-T-id {A} = CA.I.⊥-id (record
        { f = colim-T₁ (C.id {A})
        ; commute = λ {i} →
          let open SetoidReasoning (C.hom-setoid {DA.F₀ i} {colim-T₀ A})
          in begin
            C [ colim-T₁ (C.id {A}) ∘ κ i A ]
          -- colimit property of T(id) = [κ i A ∘ id]_{i ∈ I}
          ↓⟨ CoconeMorphism.commute (CA.I.! {cocone-T₁ (C.id {A})}) ⟩
            C [ κ i A ∘ T₁ i (C.id {A}) ]
          -- Functoriality of Tᵢ
          ↓⟨ C.∘-resp-≡ʳ (Functor.identity (T i)) ⟩
            C [ κ i A ∘ C.id {T₀ i A} ]
          ↓⟨ C.identityʳ ⟩
            κ i A
          ∎
        })
      where
        module CA = Colimit (c A)
        module DA = Functor (PW-Diagram D A)

    -- Proof that T(g ∘ f) = Tg ∘ Tf
    .colim-T-hom : {X Y Z : C.Obj} {f : C [ X , Y ]} {g : C [ Y , Z ]} →
                   colim-T₁ (C [ g ∘ f ]) C.≡ C [ colim-T₁ g ∘ colim-T₁ f ]
    colim-T-hom {X} {Y} {Z} {f} {g} = CX.I.!-unique CX⇒TgTf
      where
        module CX = Colimit (c X)
        module CY = Colimit (c Y)
        module DX = Functor (PW-Diagram D X)
        module CC-DX = Category (Cocones (PW-Diagram D X))

        -- Show that Tg ∘ Tf is a cocone for T(g ∘ f), which implies that
        -- Tg ∘ Tf = T(g ∘ f).
        -- To achieve this, we need to show that for each i ∈ I, we have
        -- Tg ∘ Tf ∘ κ i X = κ i Z ∘ Tᵢ (g ∘ f).
        CX⇒TgTf : Colimit.I.⊥ (c X) CC-DX.⇒ cocone-T₁ (C [ g ∘ f ])
        CX⇒TgTf = record
          { f = C [ colim-T₁ g ∘ colim-T₁ f ]
          ; commute = λ {i : I.Obj} →
            let open SetoidReasoning (C.hom-setoid {DX.F₀ i} {colim-T₀ Z})
            in begin
               C [ colim-T₁ g ∘ colim-T₁ f ] C.∘ κ i X
            ↓⟨ C.assoc ⟩
                colim-T₁ g C.∘ (colim-T₁ f C.∘ κ i X)
            ↓⟨ C.∘-resp-≡ʳ
               (CoconeMorphism.commute (CX.I.! {cocone-T₁ f}))
            ⟩
                colim-T₁ g C.∘ (κ i Y C.∘ T₁ i f)
            ↑⟨ C.assoc ⟩
                (colim-T₁ g C.∘ κ i Y) C.∘ T₁ i f
            ↓⟨ C.∘-resp-≡ˡ
               (CoconeMorphism.commute (CY.I.! {cocone-T₁ g}))
            ⟩
                (κ i Z C.∘ T₁ i g) C.∘ T₁ i f
            ↓⟨ C.assoc ⟩
                κ i Z C.∘ (T₁ i g C.∘ T₁ i f)
            ↑⟨ C.∘-resp-≡ʳ (Functor.homomorphism (T i)) ⟩
              C [ κ i Z ∘ T₁ i (g C.∘ f) ]
            ∎
          }

    -- Proof that T respects the equality of C.
    .colim-T-resp-≡ : {A B : C.Obj} {f : C [ A , B ]} {g : C [ A , B ]} →
                      C [ f ≡ g ] → C [ colim-T₁ f ≡ colim-T₁ g ]
    colim-T-resp-≡ {A} {B} {f} {g} f≡g = CA.I.!-unique CA⇒Tg
      where
        module CA = Colimit (c A)
        module DA = Functor (PW-Diagram D A)
        module CC-DA = Category (Cocones (PW-Diagram D A))

        -- That T respects ≡ is inherited point-wise from the fact that
        -- each Tᵢ respects ≡.
        CA⇒Tg : Colimit.I.⊥ (c A) CC-DA.⇒ cocone-T₁ f
        CA⇒Tg = record
          { f = colim-T₁ g
          ; commute = λ {i} →
            let open SetoidReasoning (C.hom-setoid {DA.F₀ i} {colim-T₀ B})
            in begin
              C [ colim-T₁ g ∘ κ i A ]
            ↓⟨ CoconeMorphism.commute (CA.I.! {cocone-T₁ g}) ⟩
              C [ κ i B ∘ T₁ i g ]
            ↑⟨ C.∘-resp-≡ʳ (Functor.F-resp-≡ (T i) f≡g) ⟩
              C [ κ i B ∘ T₁ i f ]
            ∎
          }

    -- The colimiting up-to technique
    colim-T : Functor C C
    colim-T = record
        { F₀ = colim-T₀
        ; F₁ = colim-T₁
        ; identity = colim-T-id
        ; homomorphism = colim-T-hom
        ; F-resp-≡ = colim-T-resp-≡
        }

    -- Cocone to construct ρ = [F₁ (κᵢ A) ∘ ρᵢ A]_{i ∈ I}
    cocone-ρ : {A : C.Obj} →
               Category.Obj (Cocones (PW-Diagram D (F₀ A)))
    cocone-ρ {A} = record
      { N = F₀ (colim-T₀ A)
      ; ψ = λ i → C [ F₁ (κ i A) ∘ ρη i A ]
      ; commute = λ {i} {j} f →
        let open SetoidReasoning (C.hom-setoid {T₀ i (F₀ A)} {F₀ (colim-T₀ A)})
        in begin
          C [ F₁ (κ i A) ∘ ρη i A ]
        ↓⟨ C.∘-resp-≡ˡ (Functor.F-resp-≡ F (CA.Ic.commute f)) ⟩
          C [ F₁ ((κ j A) C.∘ (DA.F₁ f)) ∘ ρη i A ]
        ↓⟨ C.∘-resp-≡ˡ (Functor.homomorphism F) ⟩
          C [ C [ F₁ (κ j A) ∘ F₁ (DA.F₁ f) ] ∘ ρη i A ]
        ↓⟨ C.assoc ⟩
          C [ F₁ (κ j A) ∘ C [ F₁ (DA.F₁ f) ∘ ρη i A ] ]
        ↓⟨ C.∘-resp-≡ʳ (lemma f) ⟩
          C [ F₁ (κ j A) ∘ C [ ρη j A ∘ DFA.F₁ f ] ]
        ↑⟨ C.assoc ⟩
          C [ F₁ (κ j A) ∘ ρη j A ] C.∘ DFA.F₁ f
        ∎
      }
      where
        module CA = Colimit (c A)
        module DA = Functor (PW-Diagram D A)
        module DFA = Functor (PW-Diagram D (F₀ A))

        -- Lemma to turn the commuting square for ρ into the equation we need
        .lemma : {i j : I.Obj} → (f : I [ i , j ]) →
                 C [ F₁ (DA.F₁ f) ∘ ρη i A ] C.≡ C [ ρη j A ∘ DFA.F₁ f ]
        lemma {i} {j} f =
          begin
            C [ F₁ (DA.F₁ f) ∘ ρη i A ]
          ↑⟨ C.∘-resp-≡ˡ C.identityʳ ⟩
            C [ C [ F₁ (DA.F₁ f) ∘ C.id {F₀ (DA.F₀ i)} ] ∘ ρη i A ]
          ↑⟨ UpTo⇒.square (D₁ f) {A} ⟩
            C [ ρη j A ∘ C [ T₁ j (C.id {F₀ A}) ∘ (DFA.F₁ f) ] ]
          ↓⟨ C.∘-resp-≡ʳ (C.∘-resp-≡ˡ
             (Functor.identity (T j)))
          ⟩
            C [ ρη j A ∘ C [ C.id {T₀ j (F₀ A)} ∘ (DFA.F₁ f) ] ]
          ↓⟨ C.∘-resp-≡ʳ C.identityˡ ⟩
            C [ ρη j A ∘ DFA.F₁ f ]
          ∎
          where
            open SetoidReasoning (C.hom-setoid {T₀ i (F₀ A)} {F₀ (T₀ j A)})

    colim-ρ-η : (A : C.Obj) → C [ colim-T₀ (F₀ A) , F₀ (colim-T₀ A) ]
    colim-ρ-η A = CoconeMorphism.f (CFA.I.! {cocone-ρ})
      where
        module CFA = Colimit (c (F₀ A))

    -- Natural transformation to make colim-T indeed an up-to technique
    colim-ρ : (colim-T ∘ F) ⇒ (F ∘ colim-T)
    colim-ρ = record
      { η = colim-ρ-η
      ; commute = λ {A} {B} f →
        let open SetoidReasoning
                 (C.hom-setoid {colim-T₀ (F₀ A)} {F₀ (colim-T₀ B)})
        in begin
          C [ colim-ρ-η B ∘ colim-T₁ (F₁ f) ]
        ↓⟨ {!!} ⟩
          C [ F₁ (colim-T₁ f) ∘ colim-ρ-η A ]
        ∎
      }
      where

    colim-Endo : Endo⇒ C F C F
    colim-Endo = record
      { T = colim-T
      ; ρ = colim-ρ
      }

    colim-ψ : (i : I.Obj) → UpTo⇒ (D₀ i) colim-Endo
    colim-ψ i = record
      { γ = record
        { η = λ X → κ i X
        ; commute = {!!}
        }
      ; square = {!!}
      }

    colim-D : CC-D.Obj
    colim-D =
      record
      { N = colim-Endo
      ; ψ = colim-ψ
      ; commute = {!!}
      }

    out : ∀ {A : CC-D.Obj} → colim-D CC-D.⇒ A
    out = {!!}

    out-unique : {A : CC-D.Obj} (f : colim-D CC-D.⇒ A) → out CC-D.≡ f
    out-unique = {!!}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module _ where

open import Agda.Builtin.Equality

module MM1 (A : Set) where
  postulate a0 : A

  module M1 (a : A) where
    postulate
      x : A

  module M = M1 a0

module MM2 (A : Set) where

  open module MM1A = MM1 A

  check : M1.x ≡ (λ a → a)
  check = refl  -- used to be internal error

max_forks_repo_name: Agda-zh/agda


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

{- Remember to keep CodeAP.agda in sync. -}

open import HoTT
import homotopy.RelativelyConstantToSetExtendsViaSurjection as SurjExt

module homotopy.vankampen.CodeBP {i j k l}
  (span : Span {i} {j} {k})
  {D : Type l} (h : D → Span.C span) (h-is-surj : is-surj h) where

  open Span span

  data precodeBB (b₀ : B) : B → Type (lmax (lmax (lmax i j) k) l)
  data precodeBA (b₀ : B) (a₁ : A) : Type (lmax (lmax (lmax i j) k) l)

  data precodeBB b₀ where
    pc-b : ∀ {b₁} (pB : b₀ =₀ b₁) → precodeBB b₀ b₁
    pc-bab : ∀ d {b₁} (pc : precodeBA b₀ (f (h d))) (pB : g (h d) =₀ b₁) → precodeBB b₀ b₁

  infix 66 pc-b
  syntax pc-b p = ⟧b p
  infixl 65 pc-bab
  syntax pc-bab d pcBA pB = pcBA ba⟦ d ⟧b pB

  data precodeBA b₀ a₁ where
    pc-bba : ∀ d (pc : precodeBB b₀ (g (h d))) (pA : f (h d) =₀ a₁) → precodeBA b₀ a₁

  infixl 65 pc-bba
  syntax pc-bba d pcBB pA = pcBB bb⟦ d ⟧a pA

  data precodeBB-rel {b₀ : B} : {b₁ : B}
    → precodeBB b₀ b₁ → precodeBB b₀ b₁ → Type (lmax (lmax (lmax i j) k) l)
  data precodeBA-rel {b₀ : B} : {a₁ : A}
    → precodeBA b₀ a₁ → precodeBA b₀ a₁ → Type (lmax (lmax (lmax i j) k) l)
  data precodeBB-rel {b₀} where
    pcBBr-idp₀-idp₀ : ∀ {d} pcBB → precodeBB-rel (pcBB bb⟦ d ⟧a idp₀ ba⟦ d ⟧b idp₀) pcBB
    pcBBr-switch : ∀ {d₀ d₁ : D} pcBB (pC : h d₀ =₀ h d₁)
      → precodeBB-rel (pcBB bb⟦ d₀ ⟧a ap₀ f pC ba⟦ d₁ ⟧b idp₀) (pcBB bb⟦ d₀ ⟧a idp₀ ba⟦ d₀ ⟧b ap₀ g pC)
    pcBBr-cong : ∀ {d b₁ pcBA₁ pcBA₂} (r : precodeBA-rel pcBA₁ pcBA₂) (pB : g (h d) =₀ b₁)
      → precodeBB-rel (pcBA₁ ba⟦ d ⟧b pB) (pcBA₂ ba⟦ d ⟧b pB)
  data precodeBA-rel {b₀} where
    pcBAr-idp₀-idp₀ : ∀ {d} pcBA → precodeBA-rel (pcBA ba⟦ d ⟧b idp₀ bb⟦ d ⟧a idp₀) pcBA
    pcBAr-cong : ∀ {d a₁ pcBB₁ pcBB₂} (r : precodeBB-rel pcBB₁ pcBB₂) (pA : f (h d) =₀ a₁)
      → precodeBA-rel (pcBB₁ bb⟦ d ⟧a pA) (pcBB₂ bb⟦ d ⟧a pA)

  codeBB : B → B → Type (lmax (lmax (lmax i j) k) l)
  codeBB b₀ b₁ = SetQuot (precodeBB-rel {b₀} {b₁})

  codeBA : B → A → Type (lmax (lmax (lmax i j) k) l)
  codeBA b₀ a₁ = SetQuot (precodeBA-rel {b₀} {a₁})

  c-bba : ∀ {a₀} d {a₁} (pc : codeBB a₀ (g (h d))) (pA : f (h d) =₀ a₁) → codeBA a₀ a₁
  c-bba d {a₁} c pA = SetQuot-rec SetQuot-is-set
    (λ pc → q[ pc-bba d pc pA ])
    (λ r → quot-rel $ pcBAr-cong r pA) c

  c-bab : ∀ {a₀} d {b₁} (pc : codeBA a₀ (f (h d))) (pB : g (h d) =₀ b₁) → codeBB a₀ b₁
  c-bab d {a₁} c pB = SetQuot-rec SetQuot-is-set
    (λ pc → q[ pc-bab d pc pB ])
    (λ r → quot-rel $ pcBBr-cong r pB) c

-- codeBP

  abstract
    pcBB-idp₀-idp₀-head : ∀ {d₀ b} (pB : g (h d₀) =₀ b)
      → q[ ⟧b idp₀ bb⟦ d₀ ⟧a idp₀ ba⟦ d₀ ⟧b pB ] == q[ ⟧b pB ] :> codeBB _ b
    pcBB-idp₀-idp₀-head {d₀} = Trunc-elim (λ _ → =-preserves-set SetQuot-is-set) lemma where
      lemma : ∀ {b} (pB : g (h d₀) == b)
        → q[ ⟧b idp₀ bb⟦ d₀ ⟧a idp₀ ba⟦ d₀ ⟧b [ pB ] ] == q[ ⟧b [ pB ] ] :> codeBB _ b
      lemma idp = quot-rel $ pcBBr-idp₀-idp₀ (⟧b idp₀)

  pcBA-prepend : ∀ {b₀} d₁ {b₂} → b₀ =₀ g (h d₁) → precodeBA (g (h d₁)) b₂ → precodeBA b₀ b₂
  pcBB-prepend : ∀ {b₀} d₁ {a₂} → b₀ =₀ g (h d₁) → precodeBB (g (h d₁)) a₂ → precodeBB b₀ a₂
  pcBA-prepend d₁ pB (pc-bba d pc pA) = pc-bba d (pcBB-prepend d₁ pB pc) pA
  pcBB-prepend d₁ pB (pc-b pB₁) = pc-bab d₁ (pc-bba d₁ (pc-b pB) idp₀) pB₁
  pcBB-prepend d₁ pB (pc-bab d pc pB₁) = pc-bab d (pcBA-prepend d₁ pB pc) pB₁

  abstract
    pcBA-prepend-idp₀ : ∀ {d₀ b₁} (pcBA : precodeBA (g (h d₀)) b₁)
      → q[ pcBA-prepend d₀ idp₀ pcBA ] == q[ pcBA ] :> codeBA (g (h d₀)) b₁
    pcBB-prepend-idp₀ : ∀ {d₀ a₁} (pcBB : precodeBB (g (h d₀)) a₁)
      → q[ pcBB-prepend d₀ idp₀ pcBB ] == q[ pcBB ] :> codeBB (g (h d₀)) a₁
    pcBA-prepend-idp₀ (pc-bba d pc pB) = pcBB-prepend-idp₀ pc |in-ctx λ c → c-bba d c pB
    pcBB-prepend-idp₀ (pc-b pB) = pcBB-idp₀-idp₀-head pB
    pcBB-prepend-idp₀ (pc-bab d pc pB) = pcBA-prepend-idp₀ pc |in-ctx λ c → c-bab d c pB

    transp-cBA-l : ∀ d {b₀ a₁} (p : g (h d) == b₀) (pcBA : precodeBA (g (h d)) a₁)
      → transport (λ x → codeBA x a₁) p q[ pcBA ] == q[ pcBA-prepend d [ ! p ] pcBA ]
    transp-cBA-l d idp pcBA = ! $ pcBA-prepend-idp₀ pcBA

    transp-cBB-l : ∀ d {b₀ b₁} (p : g (h d) == b₀) (pcBB : precodeBB (g (h d)) b₁)
      → transport (λ x → codeBB x b₁) p q[ pcBB ] == q[ pcBB-prepend d [ ! p ] pcBB ]
    transp-cBB-l d idp pcBB = ! $ pcBB-prepend-idp₀ pcBB

    transp-cBA-r : ∀ d {b₀ a₁} (p : f (h d) == a₁) (pcBA : precodeBA b₀ (f (h d)))
      → transport (λ x → codeBA b₀ x) p q[ pcBA ] == q[ pcBA ba⟦ d ⟧b idp₀ bb⟦ d ⟧a [ p ] ]
    transp-cBA-r d idp pcBA = ! $ quot-rel $ pcBAr-idp₀-idp₀ pcBA

    transp-cBB-r : ∀ d {b₀ b₁} (p : g (h d) == b₁) (pcBB : precodeBB b₀ (g (h d)))
      → transport (λ x → codeBB b₀ x) p q[ pcBB ] == q[ pcBB bb⟦ d ⟧a idp₀ ba⟦ d ⟧b [ p ] ]
    transp-cBB-r d idp pcBB = ! $ quot-rel $ pcBBr-idp₀-idp₀ pcBB

  module CodeBAEquivCodeBB (b₀ : B) where

    eqv-on-image : (d : D) → codeBA b₀ (f (h d)) ≃ codeBB b₀ (g (h d))
    eqv-on-image d = equiv to from to-from from-to where
      to = λ c → c-bab d c idp₀
      from = λ c → c-bba d c idp₀

      abstract
        from-to : ∀ cBA → from (to cBA) == cBA
        from-to = SetQuot-elim
          (λ _ → =-preserves-set SetQuot-is-set)
          (λ pcBA → quot-rel (pcBAr-idp₀-idp₀ pcBA))
          (λ _ → prop-has-all-paths-↓ (SetQuot-is-set _ _))

        to-from : ∀ cBB → to (from cBB) == cBB
        to-from = SetQuot-elim
          (λ _ → =-preserves-set SetQuot-is-set)
          (λ pcBB → quot-rel (pcBBr-idp₀-idp₀ pcBB))
          (λ _ → prop-has-all-paths-↓ (SetQuot-is-set _ _))

    abstract
      eqv-is-const : ∀ d₁ d₂ (p : h d₁ == h d₂)
        → eqv-on-image d₁ == eqv-on-image d₂
        [ (λ c → codeBA b₀ (f c) ≃ codeBB b₀ (g c)) ↓ p ]
      eqv-is-const d₁ d₂ p = ↓-Subtype-in (λ d → is-equiv-prop) $
        ↓-→-from-transp $ λ= $
          SetQuot-elim (λ _ → =-preserves-set SetQuot-is-set)
            (λ pcBA →
              transport (λ c → codeBB b₀ (g c)) p q[ pcBA ba⟦ d₁ ⟧b idp₀ ]
                =⟨ ap-∘ (codeBB b₀) g p |in-ctx (λ p → coe p q[ pcBA ba⟦ d₁ ⟧b idp₀ ]) ⟩
              transport (codeBB b₀) (ap g p) q[ pcBA ba⟦ d₁ ⟧b idp₀ ]
                =⟨ transp-cBB-r d₁ (ap g p) (pcBA ba⟦ d₁ ⟧b idp₀) ⟩
              q[ pcBA ba⟦ d₁ ⟧b idp₀ bb⟦ d₁ ⟧a idp₀ ba⟦ d₁ ⟧b [ ap g p ] ]
                =⟨ ! $ quot-rel $ pcBBr-switch (pcBA ba⟦ d₁ ⟧b idp₀) [ p ] ⟩
              q[ pcBA ba⟦ d₁ ⟧b idp₀ bb⟦ d₁ ⟧a [ ap f p ] ba⟦ d₂ ⟧b idp₀ ]
                =⟨ ! $ transp-cBA-r d₁ (ap f p) pcBA |in-ctx (λ c → c-bab d₂ c idp₀) ⟩
              c-bab d₂ (transport (codeBA b₀) (ap f p) q[ pcBA ]) idp₀
                =⟨ ∘-ap (codeBA b₀) f p |in-ctx (λ p → coe p q[ pcBA ]) |in-ctx (λ c → c-bab d₂ c idp₀) ⟩
              c-bab d₂ (transport (λ c → codeBA b₀ (f c)) p q[ pcBA ]) idp₀
                =∎)
            (λ _ → prop-has-all-paths-↓ (SetQuot-is-set _ _))

    module SE = SurjExt
      (λ c → ≃-is-set SetQuot-is-set SetQuot-is-set)
      h h-is-surj
      eqv-on-image
      eqv-is-const

    abstract
      eqv : ∀ c → codeBA b₀ (f c) ≃ codeBB b₀ (g c)
      eqv = SE.ext

      eqv-β : ∀ d → eqv (h d) == eqv-on-image d
      eqv-β = SE.β

  module CodeBP (b₀ : B) = PushoutRec (codeBA b₀) (codeBB b₀)
    (ua ∘ CodeBAEquivCodeBB.eqv b₀)

  codeBP : B → Pushout span → Type (lmax (lmax (lmax i j) k) l)
  codeBP = CodeBP.f

  abstract
    codeBP-level : ∀ {a₀ p₁} → is-set (codeBP a₀ p₁)
    codeBP-level {a₀} {p₁} = Pushout-elim
      {P = λ p₁ → is-set (codeBP a₀ p₁)}
      (λ a₁ → SetQuot-is-set)
      (λ b₁ → SetQuot-is-set)
      (λ c₁ → prop-has-all-paths-↓ is-set-is-prop)
      p₁
  codeBP-is-set = codeBP-level

  abstract
    transp-cBP-glue : ∀ {b₀} d₁ (pcBA : precodeBA b₀ (f (h d₁)))
      → transport (codeBP b₀) (glue (h d₁)) q[ pcBA ] == q[ pcBA ba⟦ d₁ ⟧b idp₀ ]
    transp-cBP-glue {b₀} d₁ pcBA =
      transport (codeBP b₀) (glue (h d₁)) q[ pcBA ]
        =⟨ ap (λ e → coe e q[ pcBA ]) (CodeBP.glue-β b₀ (h d₁) ∙ ap ua (CodeBAEquivCodeBB.eqv-β b₀ d₁)) ⟩
      coe (ua (CodeBAEquivCodeBB.eqv-on-image b₀ d₁)) q[ pcBA ]
        =⟨ coe-β (CodeBAEquivCodeBB.eqv-on-image b₀ d₁) q[ pcBA ] ⟩
      q[ pcBA ba⟦ d₁ ⟧b idp₀ ]
        =∎

    transp-cBP-!glue : ∀ {b₀} d₁ (pcBB : precodeBB b₀ (g (h d₁)))
      → transport (codeBP b₀) (! (glue (h d₁))) q[ pcBB ] == q[ pcBB bb⟦ d₁ ⟧a idp₀ ]
    transp-cBP-!glue {b₀} d₁ pcBB =
      transport (codeBP b₀) (! (glue (h d₁))) q[ pcBB ]
        =⟨ ap (λ e → coe e q[ pcBB ]) (ap-! (codeBP b₀) (glue (h d₁)))
         ∙ coe-! (ap (codeBP b₀) (glue (h d₁))) q[ pcBB ] ⟩
      transport! (codeBP b₀) (glue (h d₁)) q[ pcBB ]
        =⟨ ap (λ e → coe! e q[ pcBB ]) (CodeBP.glue-β b₀ (h d₁) ∙ ap ua (CodeBAEquivCodeBB.eqv-β b₀ d₁)) ⟩
      coe! (ua (CodeBAEquivCodeBB.eqv-on-image b₀ d₁)) q[ pcBB ]
        =⟨ coe!-β (CodeBAEquivCodeBB.eqv-on-image b₀ d₁) q[ pcBB ] ⟩
      q[ pcBB bb⟦ d₁ ⟧a idp₀ ]
        =∎

  -- code to path
  pcBA-to-path : ∀ {b₀ a₁} → precodeBA b₀ a₁ → right b₀ =₀ left a₁ :> Pushout span
  pcBB-to-path : ∀ {b₀ b₁} → precodeBB b₀ b₁ → right b₀ =₀ right b₁ :> Pushout span
  pcBA-to-path (pc-bba d pc pA) = pcBB-to-path pc ∙₀' !₀ [ glue (h d) ] ∙₀' ap₀ left pA
  pcBB-to-path (pc-b pB) = ap₀ right pB
  pcBB-to-path (pc-bab d pc pB) = pcBA-to-path pc ∙₀' [ glue (h d) ] ∙₀' ap₀ right pB

  abstract
    pcBA-to-path-rel : ∀ {b₀ a₁} {pcBA₀ pcBA₁ : precodeBA b₀ a₁}
      → precodeBA-rel pcBA₀ pcBA₁ → pcBA-to-path pcBA₀ == pcBA-to-path pcBA₁
    pcBB-to-path-rel : ∀ {b₀ b₁} {pcBB₀ pcBB₁ : precodeBB b₀ b₁}
      → precodeBB-rel pcBB₀ pcBB₁ → pcBB-to-path pcBB₀ == pcBB-to-path pcBB₁
    pcBA-to-path-rel (pcBAr-idp₀-idp₀ pcBA) =
        ∙₀'-assoc (pcBA-to-path pcBA) [ glue (h _) ] [ ! (glue (h _)) ]
      ∙ ap (λ p → pcBA-to-path pcBA ∙₀' [ p ]) (!-inv'-r (glue (h _)))
      ∙ ∙₀'-unit-r (pcBA-to-path pcBA)
    pcBA-to-path-rel (pcBAr-cong pcBB pA) = pcBB-to-path-rel pcBB |in-ctx _∙₀' !₀ [ glue (h _) ] ∙₀' ap₀ left pA
    pcBB-to-path-rel (pcBBr-idp₀-idp₀ pcBB) =
        ∙₀'-assoc (pcBB-to-path pcBB) [ ! (glue (h _)) ] [ glue (h _) ]
      ∙ ap (λ p → pcBB-to-path pcBB ∙₀' [ p ]) (!-inv'-l (glue (h _)))
      ∙ ∙₀'-unit-r (pcBB-to-path pcBB)
    pcBB-to-path-rel (pcBBr-switch pcBB pC) =
        ap (_∙₀' [ glue (h _) ]) (! (∙₀'-assoc (pcBB-to-path pcBB) [ ! (glue (h _)) ] (ap₀ left (ap₀ f pC))))
      ∙ ∙₀'-assoc (pcBB-to-path pcBB ∙₀' [ ! (glue (h _)) ]) (ap₀ left (ap₀ f pC)) [ glue (h _) ]
      ∙ ap ((pcBB-to-path pcBB ∙₀' [ ! (glue (h _)) ]) ∙₀'_) (natural₀ pC)
      where
        natural : ∀ {c₀ c₁} (p : c₀ == c₁)
          → (ap left (ap f p) ∙' glue c₁) == (glue c₀ ∙' ap right (ap g p))
          :> (left (f c₀) == right (g c₁) :> Pushout span)
        natural idp = ∙'-unit-l (glue _)

        natural₀ : ∀ {c₀ c₁} (p : c₀ =₀ c₁)
          → (ap₀ left (ap₀ f p) ∙₀' [ glue c₁ ]) == ([ glue c₀ ] ∙₀' ap₀ right (ap₀ g p))
          :> (left (f c₀) =₀ right (g c₁) :> Pushout span)
        natural₀ = Trunc-elim (λ _ → =-preserves-set Trunc-level) (ap [_] ∘ natural)
    pcBB-to-path-rel (pcBBr-cong pcBA pB) = pcBA-to-path-rel pcBA |in-ctx _∙₀' [ glue (h _) ] ∙₀' ap₀ right pB

  decodeBA : ∀ {b₀ a₁} → codeBA b₀ a₁ → right b₀ =₀ left a₁ :> Pushout span
  decodeBB : ∀ {b₀ b₁} → codeBB b₀ b₁ → right b₀ =₀ right b₁ :> Pushout span
  decodeBA = SetQuot-rec Trunc-level pcBA-to-path pcBA-to-path-rel
  decodeBB = SetQuot-rec Trunc-level pcBB-to-path pcBB-to-path-rel

  abstract
    decodeBA-is-decodeBB : ∀ {b₀} c₁ →
      decodeBA {b₀} {f c₁} == decodeBB {b₀} {g c₁}
      [ (λ p₁ → codeBP b₀ p₁ → right b₀ =₀ p₁) ↓ glue c₁ ]
    decodeBA-is-decodeBB {b₀ = b₀} = SurjExt.ext
      (λ _ → ↓-preserves-level $ Π-is-set λ _ → Trunc-level) h h-is-surj
      (λ d₁ → ↓-→-from-transp $ λ= $ SetQuot-elim
        {P = λ cBA → transport (right b₀ =₀_) (glue (h d₁)) (decodeBA cBA)
                  == decodeBB (transport (codeBP b₀) (glue (h d₁)) cBA)}
        (λ _ → =-preserves-set Trunc-level)
        (λ pcBA →
          transport (right b₀ =₀_) (glue (h d₁)) (pcBA-to-path pcBA)
            =⟨ transp₀-cst=₀idf [ glue (h d₁) ] (pcBA-to-path pcBA) ⟩
          pcBA-to-path pcBA ∙₀' [ glue (h d₁) ]
            =⟨ ! $ ap (λ e → decodeBB (–> e q[ pcBA ])) (CodeBAEquivCodeBB.eqv-β b₀ d₁) ⟩
          decodeBB (–> (CodeBAEquivCodeBB.eqv b₀ (h d₁)) q[ pcBA ])
            =⟨ ! $ ap decodeBB (coe-β (CodeBAEquivCodeBB.eqv b₀ (h d₁)) q[ pcBA ]) ⟩
          decodeBB (coe (ua (CodeBAEquivCodeBB.eqv b₀ (h d₁))) q[ pcBA ])
            =⟨ ! $ ap (λ p → decodeBB (coe p q[ pcBA ])) (CodeBP.glue-β b₀ (h d₁)) ⟩
          decodeBB (transport (codeBP b₀) (glue (h d₁)) q[ pcBA ])
            =∎)
        (λ _ → prop-has-all-paths-↓ $ Trunc-level {n = 0} _ _))
      (λ _ _ _ → prop-has-all-paths-↓ $ ↓-level $ Π-is-set λ _ → Trunc-level)

  decodeBP : ∀ {b₀ p₁} → codeBP b₀ p₁ → right b₀ =₀ p₁
  decodeBP {p₁ = p₁} = Pushout-elim
    (λ a₁ → decodeBA) (λ b₁ → decodeBB)
    decodeBA-is-decodeBB
    p₁