text:
{-# OPTIONS --allow-unsolved-metas --warning=error --without-K --guardedness #-}

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Setoids.Setoids
open import Rings.Definition
open import Rings.Lemmas
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Groups.Definition
open import Groups.Groups
open import Fields.Fields
open import Sets.EquivalenceRelations
open import Sequences
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order

module Fields.CauchyCompletion.Field {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

open Setoid S
open PartiallyOrderedRing pRing
open SetoidPartialOrder pOrder
open Equivalence eq
open SetoidTotalOrder (TotallyOrderedRing.total order)
open Field F
open Group (Ring.additiveGroup R)

open import Rings.Orders.Total.Cauchy order
open import Rings.Orders.Total.Lemmas order
open import Rings.Orders.Total.AbsoluteValue order
open import Fields.CauchyCompletion.Definition order F
open import Fields.CauchyCompletion.Multiplication order F
open import Fields.CauchyCompletion.Addition order F
open import Fields.CauchyCompletion.Setoid order F
open import Fields.CauchyCompletion.Group order F
open import Fields.CauchyCompletion.Ring order F
open import Fields.CauchyCompletion.Comparison order F

Cnontrivial : (pr : Setoid._∼_ cauchyCompletionSetoid (injection (Ring.0R R)) (injection (Ring.1R R))) → False
Cnontrivial pr with pr (Ring.1R R) (0<1 nontrivial)
Cnontrivial pr | N , b with b {succ N} (le 0 refl)
... | bl rewrite indexAndApply (constSequence 0G) (map inverse (constSequence (Ring.1R R))) _+_ {N} | indexAndConst 0G N | equalityCommutative (mapAndIndex (constSequence (Ring.1R R)) inverse N) | indexAndConst (Ring.1R R) N = irreflexive {Ring.1R R} (<WellDefined (Equivalence.transitive eq (absWellDefined _ _ identLeft) (Equivalence.transitive eq (Equivalence.symmetric eq (absNegation (Ring.1R R))) abs1Is1)) (Equivalence.reflexive eq) bl)

boundedMap : A → A
boundedMap a with totality 0G a
boundedMap a | inl (inl x) = underlying (allInvertible a λ pr → irreflexive (<WellDefined (Equivalence.reflexive eq) pr x))
boundedMap a | inl (inr x) = underlying (allInvertible a λ pr → irreflexive (<WellDefined pr (Equivalence.reflexive eq) x))
boundedMap a | inr x = Ring.1R R

-- TODO: make a real which is equivalent by approximating from above;
-- make a real which is equivalent by approximating from below.
-- Use not-zero to show that one of those sequences must pass 0 at some point.
aNonzeroImpliesBounded : (a : CauchyCompletion) → (Setoid._∼_ cauchyCompletionSetoid a (injection 0G) → False) → (a <Cr 0G) || 0G r<C a
aNonzeroImpliesBounded a a!=0 = {!!}

1/aConverges : (a : CauchyCompletion) → (Setoid._∼_ cauchyCompletionSetoid a (injection 0G) → False) → cauchy (map boundedMap (CauchyCompletion.elts a))
1/aConverges a a!=0 e 0<e = {!!}

1/a : (a : CauchyCompletion) → (Setoid._∼_ cauchyCompletionSetoid a (injection 0G) → False) → CauchyCompletion
1/a a a!=0 = record { elts = map boundedMap (CauchyCompletion.elts a) ; converges = 1/aConverges a a!=0 }

1/a*a=1 : (a : CauchyCompletion) (pr : Setoid._∼_ cauchyCompletionSetoid a (injection 0G) → False) → Setoid._∼_ cauchyCompletionSetoid ((1/a a pr) *C a) (injection (Ring.1R R))
1/a*a=1 a a!=0 e 0<e = {!!}

CField : Field CRing
Field.allInvertible CField a a!=0 = (1/a a a!=0) , 1/a*a=1 a a!=0
Field.nontrivial CField = Cnontrivial


text:
{-# OPTIONS --universe-polymorphism --allow-unsolved-metas --no-termination-check #-}

module Issue202 where

Foo : ∀ {A} → A → Set
Foo x = Foo x

-- Previously resulted in the following (cryptic) error:
-- Bug.agda:6,13-14
-- _5 !=< _5
-- when checking that the expression x has type _5

ext: agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- Operations and lemmas related to application of substitutions
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Substitution.Data.Application.Application1
  {i u e} {Uni : IndexedUniverse i u e} where

import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Data.Application.Application22
open import deBruijn.Substitution.Data.Basics
open import deBruijn.Substitution.Data.Map
open import deBruijn.Substitution.Data.Simple
open import Function using (_$_)
open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open P.≡-Reasoning

-- More operations and lemmas related to application. In this module
-- the application operator is assumed to be homogeneous, so some
-- previously proved lemmas can be stated in a less complicated way.

record Application₁ {t} (T : Term-like t) : Set (i ⊔ u ⊔ e ⊔ t) where

  open Term-like T

  field
    -- Simple substitutions.
    simple : Simple T

    -- The homogeneous variant is defined in terms of the
    -- heterogeneous one.
    application₂₂ : Application₂₂ simple simple ([id] {T = T})

  open Simple simple public
  open Application₂₂ application₂₂ public
    hiding ( ∘⋆; ∘⋆-cong; /∋-∘⋆
           ; trans-cong; id-∘; map-trans-wk-subst; map-trans-↑; wk-∘-↑
           )

  -- Composition of multiple substitutions.
  --
  -- Note that singleton sequences are handled specially, to avoid the
  -- introduction of unnecessary identity substitutions.

  ∘⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Subs T ρ̂ → Sub T ρ̂
  ∘⋆ ε        = id
  ∘⋆ (ε  ▻ ρ) = ρ
  ∘⋆ (ρs ▻ ρ) = ∘⋆ ρs ∘ ρ

  -- A congruence lemma.

  ∘⋆-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T ρ̂₁}
              {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T ρ̂₂} →
            ρs₁ ≅-⇨⋆ ρs₂ → ∘⋆ ρs₁ ≅-⇨ ∘⋆ ρs₂
  ∘⋆-cong P.refl = P.refl

  abstract

    -- Applying a composed substitution to a variable is equivalent to
    -- applying all the substitutions one after another.

    /∋-∘⋆ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ σ) (ρs : Subs T ρ̂) →
            x /∋ ∘⋆ ρs ≅-⊢ var · x /⊢⋆ ρs
    /∋-∘⋆ x ε = begin
      [ x /∋ id ]  ≡⟨ /∋-id x ⟩
      [ var · x ]  ∎
    /∋-∘⋆ x (ε ▻ ρ) = begin
      [ x /∋ ρ       ]  ≡⟨ P.sym $ var-/⊢ x ρ ⟩
      [ var · x /⊢ ρ ]  ∎
    /∋-∘⋆ x (ρs ▻ ρ₁ ▻ ρ₂) = begin
      [ x /∋ ∘⋆ (ρs ▻ ρ₁) ∘ ρ₂      ]  ≡⟨ /∋-∘ x (∘⋆ (ρs ▻ ρ₁)) ρ₂ ⟩
      [ x /∋ ∘⋆ (ρs ▻ ρ₁) /⊢ ρ₂     ]  ≡⟨ /⊢-cong (/∋-∘⋆ x (ρs ▻ ρ₁)) P.refl ⟩
      [ var · x /⊢⋆ (ρs ▻ ρ₁) /⊢ ρ₂ ]  ∎

    -- Yet another variant of var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆.

    ∘⋆-⇒-/⊢⋆ :
      ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρs₁ : Subs T ρ̂) (ρs₂ : Subs T ρ̂) →
      ∘⋆ ρs₁ ≅-⇨ ∘⋆ ρs₂ → ∀ {σ} (t : Γ ⊢ σ) → t /⊢⋆ ρs₁ ≅-⊢ t /⊢⋆ ρs₂
    ∘⋆-⇒-/⊢⋆ ρs₁ ρs₂ hyp = var-/⊢⋆-⇒-/⊢⋆ ρs₁ ρs₂ (λ x → begin
      [ var · x /⊢⋆ ρs₁ ]  ≡⟨ P.sym $ /∋-∘⋆ x ρs₁ ⟩
      [ x /∋ ∘⋆ ρs₁     ]  ≡⟨ /∋-cong (P.refl {x = [ x ]}) hyp ⟩
      [ x /∋ ∘⋆ ρs₂     ]  ≡⟨ /∋-∘⋆ x ρs₂ ⟩
      [ var · x /⊢⋆ ρs₂ ]  ∎)

    -- id is a left identity of _∘_.

    id-∘ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) → id ∘ ρ ≅-⇨ ρ
    id-∘ ρ = begin
      [ id ∘ ρ     ]  ≡⟨ Application₂₂.id-∘ application₂₂ ρ ⟩
      [ map [id] ρ ]  ≡⟨ map-[id] ρ ⟩
      [ ρ          ]  ∎

    -- The wk substitution commutes with any other (modulo lifting
    -- etc.).

    wk-∘-↑ : ∀ {Γ Δ} σ {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) →
             ρ ∘ wk {σ = σ / ρ} ≅-⇨ wk {σ = σ} ∘ ρ ↑
    wk-∘-↑ σ ρ = begin
      [ ρ ∘ wk           ]  ≡⟨ ∘-cong (P.sym $ map-[id] ρ) P.refl ⟩
      [ map [id] ρ ∘ wk  ]  ≡⟨ Application₂₂.wk-∘-↑ application₂₂ σ ρ ⟩
      [ wk {σ = σ} ∘ ρ ↑ ]  ∎

    -- Applying a composed substitution is equivalent to applying one
    -- substitution and then the other.

    /⊢-∘ : ∀ {Γ Δ Ε σ} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε}
           (t : Γ ⊢ σ) (ρ₁ : Sub T ρ̂₁) (ρ₂ : Sub T ρ̂₂) →
           t /⊢ ρ₁ ∘ ρ₂ ≅-⊢ t /⊢ ρ₁ /⊢ ρ₂
    /⊢-∘ t ρ₁ ρ₂ = ∘⋆-⇒-/⊢⋆ (ε ▻ ρ₁ ∘ ρ₂) (ε ▻ ρ₁ ▻ ρ₂) P.refl t

    -- _∘_ is associative.

    ∘-∘ : ∀ {Γ Δ Ε Ζ} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} {ρ̂₃ : Ε ⇨̂ Ζ}
          (ρ₁ : Sub T ρ̂₁) (ρ₂ : Sub T ρ̂₂) (ρ₃ : Sub T ρ̂₃) →
          ρ₁ ∘ (ρ₂ ∘ ρ₃) ≅-⇨ (ρ₁ ∘ ρ₂) ∘ ρ₃
    ∘-∘ ρ₁ ρ₂ ρ₃ = extensionality P.refl λ x → begin
      [ x /∋ ρ₁ ∘ (ρ₂ ∘ ρ₃) ]  ≡⟨ /∋-∘ x ρ₁ (ρ₂ ∘ ρ₃) ⟩
      [ x /∋ ρ₁ /⊢ ρ₂ ∘ ρ₃  ]  ≡⟨ /⊢-∘ (x /∋ ρ₁) ρ₂ ρ₃ ⟩
      [ x /∋ ρ₁ /⊢ ρ₂ /⊢ ρ₃ ]  ≡⟨ /⊢-cong (P.sym $ /∋-∘ x ρ₁ ρ₂) (P.refl {x = [ ρ₃ ]}) ⟩
      [ x /∋ ρ₁ ∘ ρ₂ /⊢ ρ₃  ]  ≡⟨ P.sym $ /∋-∘ x (ρ₁ ∘ ρ₂) ρ₃ ⟩
      [ x /∋ (ρ₁ ∘ ρ₂) ∘ ρ₃ ]  ∎

    -- If sub t is applied to variable zero then t is returned.

    zero-/⊢-sub : ∀ {Γ σ} (t : Γ ⊢ σ) → var · zero /⊢ sub t ≅-⊢ t
    zero-/⊢-sub t = begin
      [ var · zero /⊢ sub t ]  ≡⟨ var-/⊢ zero (sub t) ⟩
      [ zero /∋ sub t       ]  ≡⟨ P.refl ⟩
      [ t                   ]  ∎

    -- The sub substitution commutes with any other (modulo lifting
    -- etc.).

    ↑-∘-sub : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (t : Γ ⊢ σ) (ρ : Sub T ρ̂) →
              sub t ∘ ρ ≅-⇨ ρ ↑ σ ∘ sub (t /⊢ ρ)
    ↑-∘-sub t ρ =
      let lemma = begin
            [ id ∘ ρ                    ]  ≡⟨ id-∘ ρ ⟩
            [ ρ                         ]  ≡⟨ P.sym $ wk-subst-∘-sub ρ (t /⊢ ρ) ⟩
            [ wk-subst ρ ∘ sub (t /⊢ ρ) ]  ∎

      in begin
        [ sub t ∘ ρ                                              ]  ≡⟨ P.refl ⟩
        [ (id ▻ t) ∘ ρ                                           ]  ≡⟨ ▻-∘ id t ρ ⟩
        [ id ∘ ρ ▻ t /⊢ ρ                                        ]  ≡⟨ ▻⇨-cong P.refl lemma (P.sym $ zero-/⊢-sub (t /⊢ ρ)) ⟩
        [ wk-subst ρ ∘ sub (t /⊢ ρ) ▻ var · zero /⊢ sub (t /⊢ ρ) ]  ≡⟨ P.sym $ ▻-∘ (wk-subst ρ) (var · zero) (sub (t /⊢ ρ)) ⟩
        [ (wk-subst ρ ▻ var · zero) ∘ sub (t /⊢ ρ)               ]  ≡⟨ ∘-cong (P.sym $ unfold-↑ ρ) P.refl ⟩
        [ ρ ↑ ∘ sub (t /⊢ ρ)                                     ]  ∎

  -- wk-subst⁺ can be expressed using composition and wk⁺.

  ∘-wk⁺ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) (Δ⁺ : Ctxt⁺ Δ) →
          ρ ∘ wk⁺ Δ⁺ ≅-⇨ wk-subst⁺ Δ⁺ ρ
  ∘-wk⁺ ρ ε = begin
    [ ρ ∘ wk⁺ ε     ]  ≡⟨ P.refl ⟩
    [ ρ ∘ id        ]  ≡⟨ ∘-id ρ ⟩
    [ ρ             ]  ≡⟨ P.refl ⟩
    [ wk-subst⁺ ε ρ ]  ∎
  ∘-wk⁺ ρ (Δ⁺ ▻ σ) = begin
    [ ρ ∘ wk⁺ (Δ⁺ ▻ σ)          ]  ≡⟨ ∘-cong (P.refl {x = [ ρ ]}) (wk⁺-▻ Δ⁺) ⟩
    [ ρ ∘ (wk⁺ Δ⁺ ∘ wk)         ]  ≡⟨ ∘-∘ ρ (wk⁺ Δ⁺) wk ⟩
    [ (ρ ∘ wk⁺ Δ⁺) ∘ wk         ]  ≡⟨ ∘-cong (∘-wk⁺ ρ Δ⁺) P.refl ⟩
    [ wk-subst⁺ Δ⁺ ρ ∘ wk       ]  ≡⟨ ∘-wk (wk-subst⁺ Δ⁺ ρ) ⟩
    [ wk-subst (wk-subst⁺ Δ⁺ ρ) ]  ≡⟨ P.refl ⟩
    [ wk-subst⁺ (Δ⁺ ▻ σ) ρ      ]  ∎

  mutual

    -- wk-subst₊ can be expressed using composition and wk₊.

    ∘-wk₊ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) (Δ₊ : Ctxt₊ Δ) →
            ρ ∘ wk₊ Δ₊ ≅-⇨ wk-subst₊ Δ₊ ρ
    ∘-wk₊ ρ ε = begin
      [ ρ ∘ wk₊ ε     ]  ≡⟨ P.refl ⟩
      [ ρ ∘ id        ]  ≡⟨ ∘-id ρ ⟩
      [ ρ             ]  ≡⟨ P.refl ⟩
      [ wk-subst₊ ε ρ ]  ∎
    ∘-wk₊ ρ (σ ◅ Δ₊) = begin
      [ ρ ∘ wk₊ (σ ◅ Δ₊)          ]  ≡⟨ ∘-cong (P.refl {x = [ ρ ]}) (wk₊-◅ Δ₊) ⟩
      [ ρ ∘ (wk ∘ wk₊ Δ₊)         ]  ≡⟨ ∘-∘ ρ wk (wk₊ Δ₊) ⟩
      [ (ρ ∘ wk) ∘ wk₊ Δ₊         ]  ≡⟨ ∘-cong (∘-wk ρ) P.refl ⟩
      [ wk-subst ρ ∘ wk₊ Δ₊       ]  ≡⟨ ∘-wk₊ (wk-subst ρ) Δ₊ ⟩
      [ wk-subst₊ Δ₊ (wk-subst ρ) ]  ≡⟨ P.refl ⟩
      [ wk-subst₊ (σ ◅ Δ₊) ρ      ]  ∎

    -- Unfolding lemma for wk₊.

    wk₊-◅ : ∀ {Γ σ} (Γ₊ : Ctxt₊ (Γ ▻ σ)) →
            wk₊ (σ ◅ Γ₊) ≅-⇨ wk ∘ wk₊ Γ₊
    wk₊-◅ {σ = σ} Γ₊ = begin
      [ wk₊ (σ ◅ Γ₊)    ]  ≡⟨ P.refl ⟩
      [ wk-subst₊ Γ₊ wk ]  ≡⟨ P.sym $ ∘-wk₊ wk Γ₊ ⟩
      [ wk ∘ wk₊ Γ₊     ]  ∎

  -- A consequence of wk₊-◅.

  /∋-wk₊-◅ : ∀ {Γ τ σ} (x : Γ ∋ τ) (Γ₊ : Ctxt₊ (Γ ▻ σ)) →
             x /∋ wk₊ (σ ◅ Γ₊) ≅-⊢ suc x /∋ wk₊ Γ₊
  /∋-wk₊-◅ {σ = σ} x Γ₊ = begin
    [ x /∋ wk₊ (σ ◅ Γ₊)     ]  ≡⟨ /∋-cong (P.refl {x = [ x ]}) (wk₊-◅ Γ₊) ⟩
    [ x /∋ wk ∘ wk₊ Γ₊      ]  ≡⟨ /∋-∘ x wk (wk₊ Γ₊) ⟩
    [ x /∋ wk /⊢ wk₊ Γ₊     ]  ≡⟨ /⊢-cong (/∋-wk x) P.refl ⟩
    [ var · suc x /⊢ wk₊ Γ₊ ]  ≡⟨ var-/⊢ (suc x) (wk₊ Γ₊) ⟩
    [ suc x /∋ wk₊ Γ₊       ]  ∎

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointers into star-lists
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Star.Pointer {ℓ} {I : Set ℓ} where

open import Data.Maybe.Base using (Maybe; nothing; just)
open import Data.Star.Decoration
open import Data.Unit
open import Function
open import Level
open import Relation.Binary
open import Relation.Binary.Construct.Closure.ReflexiveTransitive

-- Pointers into star-lists. The edge pointed to is decorated with Q,
-- while other edges are decorated with P.

data Pointer {r p q} {T : Rel I r}
             (P : EdgePred p T) (Q : EdgePred q T)
             : Rel (Maybe (NonEmpty (Star T))) (p ⊔ q) where
  step : ∀ {i j k} {x : T i j} {xs : Star T j k}
         (p : P x) → Pointer P Q (just (nonEmpty (x ◅ xs)))
                                 (just (nonEmpty xs))
  done : ∀ {i j k} {x : T i j} {xs : Star T j k}
         (q : Q x) → Pointer P Q (just (nonEmpty (x ◅ xs))) nothing

-- Any P Q xs means that some edge in xs satisfies Q, while all
-- preceding edges satisfy P. A star-list of type Any Always Always xs
-- is basically a prefix of xs; the existence of such a prefix
-- guarantees that xs is non-empty.

Any : ∀ {r p q} {T : Rel I r} (P : EdgePred p T) (Q : EdgePred q T) →
      EdgePred (ℓ ⊔ (r ⊔ (p ⊔ q))) (Star T)
Any P Q xs = Star (Pointer P Q) (just (nonEmpty xs)) nothing

module _ {r p q} {T : Rel I r} {P : EdgePred p T} {Q : EdgePred q T} where

  this : ∀ {i j k} {x : T i j} {xs : Star T j k} →
         Q x → Any P Q (x ◅ xs)
  this q = done q ◅ ε

  that : ∀ {i j k} {x : T i j} {xs : Star T j k} →
         P x → Any P Q xs → Any P Q (x ◅ xs)
  that p = _◅_ (step p)

-- Safe lookup.

data Result {r p q} (T : Rel I r)
            (P : EdgePred p T) (Q : EdgePred q T) : Set (ℓ ⊔ r ⊔ p ⊔ q) where
  result : ∀ {i j} {x : T i j} (p : P x) (q : Q x) → Result T P Q

-- The first argument points out which edge to extract. The edge is
-- returned, together with proofs that it satisfies Q and R.

module _ {t p q} {T : Rel I t} {P : EdgePred p T} {Q : EdgePred q T} where

  lookup : ∀ {r} {R : EdgePred r T} {i j} {xs : Star T i j} →
           Any P Q xs → All R xs → Result T Q R
  lookup (done q ◅ ε)      (↦ r ◅ _)  = result q r
  lookup (step p ◅ ps)     (↦ r ◅ rs) = lookup ps rs
  lookup (done _ ◅ () ◅ _) _

-- We can define something resembling init.

  prefixIndex : ∀ {i j} {xs : Star T i j} → Any P Q xs → I
  prefixIndex (done {i = i} q ◅ _)  = i
  prefixIndex (step p         ◅ ps) = prefixIndex ps

  prefix : ∀ {i j} {xs : Star T i j} →
           (ps : Any P Q xs) → Star T i (prefixIndex ps)
  prefix (done q         ◅ _)  = ε
  prefix (step {x = x} p ◅ ps) = x ◅ prefix ps

-- Here we are taking the initial segment of ps (all elements but the
-- last, i.e. all edges satisfying P).

  init : ∀ {i j} {xs : Star T i j} →
        (ps : Any P Q xs) → All P (prefix ps)
  init (done q ◅ _)  = ε
  init (step p ◅ ps) = ↦ p ◅ init ps

-- One can simplify the implementation by not carrying around the
-- indices in the type:

  last : ∀ {i j} {xs : Star T i j} →
         Any P Q xs → NonEmptyEdgePred T Q
  last ps with lookup {r = p} ps (decorate (const (lift tt)) _)
  ... | result q _ = nonEmptyEdgePred q


text:
-- (Pre)additive categories
{-# OPTIONS --safe #-}

module Cubical.Categories.Additive.Base where

open import Cubical.Algebra.AbGroup.Base
open import Cubical.Categories.Category.Base
open import Cubical.Categories.Limits.Initial
open import Cubical.Categories.Limits.Terminal
open import Cubical.Foundations.Prelude

private
  variable
    ℓ ℓ' : Level

-- Preadditive categories
module _ (C : Category ℓ ℓ') where
  open Category C

  record PreaddCategoryStr : Type (ℓ-max ℓ (ℓ-suc ℓ')) where
    field
      homAbStr : (x y : ob) → AbGroupStr Hom[ x , y ]

    -- Polymorphic abelian group operations
    0h = λ {x} {y} → AbGroupStr.0g (homAbStr x y)
    -_ = λ {x} {y} → AbGroupStr.-_ (homAbStr x y)
    _+_ = λ {x} {y} → AbGroupStr._+_ (homAbStr x y)

    _-_ : ∀ {x y} (f g : Hom[ x , y ]) → Hom[ x , y ]
    f - g = f + (- g)

    infixr 7   _+_
    infixl 7.5 _-_
    infix  8    -_

    field
      ⋆distl+ : {x y z : ob} → (f : Hom[ x , y ]) → (g g' : Hom[ y , z ]) →
          f ⋆ (g + g') ≡ (f ⋆ g) + (f ⋆ g')

      ⋆distr+ : {x y z : ob} → (f f' : Hom[ x , y ]) → (g : Hom[ y , z ]) →
          (f + f') ⋆ g ≡ (f ⋆ g) + (f' ⋆ g)

record PreaddCategory (ℓ ℓ' : Level) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    cat : Category ℓ ℓ'
    preadd : PreaddCategoryStr cat

  open Category cat public
  open PreaddCategoryStr preadd public

-- Additive categories
module _ (C : PreaddCategory ℓ ℓ') where
  open PreaddCategory C

  -- Zero object
  record ZeroObject : Type (ℓ-max ℓ ℓ') where
    field
      z : ob
      zInit : isInitial cat z
      zTerm : isTerminal cat z

  -- Biproducts
  record IsBiproduct {x y x⊕y : ob}
      (i₁ : Hom[ x , x⊕y ]) (i₂ : Hom[ y , x⊕y ])
      (π₁ : Hom[ x⊕y , x ]) (π₂ : Hom[ x⊕y , y ])
          : Type (ℓ-max ℓ ℓ') where

    field
      i₁⋆π₁ : i₁ ⋆ π₁ ≡ id
      i₁⋆π₂ : i₁ ⋆ π₂ ≡ 0h
      i₂⋆π₁ : i₂ ⋆ π₁ ≡ 0h
      i₂⋆π₂ : i₂ ⋆ π₂ ≡ id
      ∑π⋆i : π₁ ⋆ i₁ + π₂ ⋆ i₂ ≡ id

  record Biproduct (x y : ob) : Type (ℓ-max ℓ ℓ') where
    field
      x⊕y : ob
      i₁ : Hom[ x , x⊕y ]
      i₂ : Hom[ y , x⊕y ]
      π₁ : Hom[ x⊕y , x ]
      π₂ : Hom[ x⊕y , y ]
      isBipr : IsBiproduct i₁ i₂ π₁ π₂

    open IsBiproduct isBipr public

  -- Additive categories
  record AdditiveCategoryStr : Type (ℓ-max ℓ (ℓ-suc ℓ')) where
    field
      zero : ZeroObject
      biprod : ∀ x y → Biproduct x y

    -- Biproduct notation
    open Biproduct
    _⊕_ = λ (x y : ob) → biprod x y .x⊕y
    infixr 6 _⊕_

record AdditiveCategory (ℓ ℓ' : Level) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    preaddcat : PreaddCategory ℓ ℓ'
    addit : AdditiveCategoryStr preaddcat

  open PreaddCategory preaddcat public
  open AdditiveCategoryStr addit public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2013-01-08, Reported by andres.sicard.ramirez, Jan 7
-- {-# OPTIONS -v term:10 -v term.matrices:40 #-}

-- The difference between @bar@ and @bar'@ is the position of the
-- hypothesis (n : ℕ). While @bar@ is accepted by the termination
-- checker, @bar'@ is rejected for it.

open import Common.Prelude renaming (Nat to ℕ)
open import Common.Product
open import Common.Coinduction
open import Common.Equality

data Foo : ℕ → Set where
  foo : (n : ℕ) → ∞ (Foo n) → Foo (suc n)

module NoWith where

  bar : (A : ℕ → Set) (n : ℕ) →
        ((m : ℕ) → A m → ∃ λ m' → m ≡ suc m' × A m') →
        A n → Foo n
  bar A n h An = subst Foo (sym (proj₁ (proj₂ (h n An))))
    (foo (proj₁ (h n An)) (♯ (bar A (proj₁ (h n An)) h (proj₂ (proj₂ (h n An))))))

module CorrectlyRejected where

  -- Proof rejected by the termination checker.
  --
  -- (If I do pattern matching on @n≡Sn'@, the proof is accepted.)
  bar' : (A : ℕ → Set) →
         ((m : ℕ) → A m → ∃ λ m' → m ≡ suc m' × A m') →
         (n : ℕ) → A n → Foo n
  bar' A h n An with h n An
  ... | (n' , n≡Sn' , An') = subst Foo (sym n≡Sn') (foo n' (♯ (bar' A h n' An')))

  postulate
    A : ℕ → Set
    h : (m : ℕ) → A m → ∃ λ m' → suc m' ≡ m × A m'

  -- Proof rejected by the termination checker.
  bar : (n : ℕ) → A n → Foo n
  bar n An with h n An
  ... | (n' , p , An') = subst Foo p (foo n' (♯ (bar n' An')))

module WasAccepted1 where

  -- Proof wrongly accepted by the termination checker.
  bar : (A : ℕ → Set) (n : ℕ) →
        ((m : ℕ) → A m → ∃ λ m' → m ≡ suc m' × A m') →
        A n → Foo n
  bar A n h An with h n An
  ... | (n' , n≡Sn' , An') = subst Foo (sym n≡Sn') (foo n' (♯ (bar A n' h An')))

-- Proof was wrongly accepted by the termination checker.

postulate
  A : ℕ → Set

H = (m : ℕ) → A m → ∃ λ m' → suc m' ≡ m × A m'

-- argument h was essential for faulty behavior

bar : (n : ℕ) → H → A n → Foo n
bar n h An with h n An
... | (n' , p , An') = subst Foo p (foo n' (♯ (bar n' h An')))

{- termination checking clause of bar
  lhs: 5 4 3 (_,_ 2 (_,_ 1 0))
  rhs: subst Foo p (foo n' (.Issue1014.♯-0 n h An n' p An'))
kept call from bar 5 4 3 (_,_ 2 (_,_ 1 0))
  to .Issue1014.♯-0 (n) (h) (An) (n') (p) (An')
  call matrix (with guardedness):
[[.,.,.,.,.]
,[.,0,.,.,.]
,[.,.,0,.,.]
,[.,.,.,0,.]
,[.,.,.,.,0]
,[.,.,.,.,0]
,[.,.,.,.,0]]
termination checking body of .Issue1014.♯-0
  : (n : ℕ)
    (h : (m : ℕ) → A m → Σ ℕ (λ m' → Σ (suc m' ≡ m) (λ x → A m')))
    (An : A n) (n' : ℕ) (p : suc n' ≡ n) (An' : A n') →
    ∞ (Foo n')
termination checking delayed clause of .Issue1014.♯-0
  lhs: 5 4 3 2 1 0
  rhs: ♯ bar n' h An'
kept call from .Issue1014.♯-0 5 4 3 2 1 0
  to bar (n') (h) (An')
  call matrix (with guardedness):
[[-1,.,.,.,.,.,.]
,[.,.,.,.,0,.,.]
,[.,.,0,.,.,.,.]
,[.,.,.,.,.,.,0]]
[Issue1014.bar] does termination check
-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Categories.Category
open import Categories.Diagram.Pullback

module Categories.Bicategory.Construction.Spans {o ℓ e} {𝒞 : Category o ℓ e}
                                                (_×ₚ_ : ∀ {X Y Z} → (f : 𝒞 [ X , Z ]) (g : 𝒞 [ Y , Z ]) → Pullback 𝒞 f g) where

open import Level
open import Function using (_$_)

open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; uncurry)

open import Categories.Bicategory
open import Categories.NaturalTransformation.NaturalIsomorphism hiding (refl; sym)

open import Categories.Category.Diagram.Span 𝒞
open import Categories.Category.Construction.Spans 𝒞 renaming (Spans to Spans₁)

open import Categories.Morphism
open import Categories.Morphism.Reasoning 𝒞

private
  module Spans₁ X Y = Category (Spans₁ X Y)

open Category 𝒞
open HomReasoning
open Equiv

open Span
open Span⇒
open Pullback

open Compositions _×ₚ_

private
  variable
    A B C D E : Obj

  --------------------------------------------------------------------------------
  -- Proofs about span compositions

⊚₁-identity : ∀ (f : Span B C) → (g : Span A B) → Spans₁ A C [ Spans₁.id B C {f} ⊚₁ Spans₁.id A B {g} ≈ Spans₁.id A C ]
⊚₁-identity f g = ⟺ (unique ((cod g) ×ₚ (dom f)) id-comm id-comm)

⊚₁-homomorphism : {f f′ f″ : Span B C} {g g′ g″ : Span A B}
                  → (α : Span⇒ f f′) → (α′ : Span⇒ f′ f″)
                  → (β : Span⇒ g g′) → (β′ : Span⇒ g′ g″)
                  → Spans₁ A C [ (Spans₁ B C [ α′ ∘ α ]) ⊚₁ (Spans₁ A B [ β′ ∘ β ]) ≈ Spans₁ A C [ α′ ⊚₁ β′ ∘ α ⊚₁ β ] ]
⊚₁-homomorphism {A} {B} {C} {f} {f′} {f″} {g} {g′} {g″} α α′ β β′ =
  let pullback  = (cod g) ×ₚ (dom f)
      pullback′ = (cod g′) ×ₚ(dom f′)
      pullback″ = (cod g″) ×ₚ (dom f″)
      α-chase = begin
        p₂ pullback″ ∘ universal pullback″ _ ∘ universal pullback′ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback″) ⟩
        (arr α′ ∘ p₂ pullback′) ∘ universal pullback′ _ ≈⟨ extendˡ (p₂∘universal≈h₂ pullback′) ⟩
        (arr α′ ∘ arr α) ∘ p₂ pullback ∎
      β-chase = begin
        p₁ pullback″ ∘ universal pullback″ _ ∘ universal pullback′ _            ≈⟨ pullˡ (p₁∘universal≈h₁ pullback″) ⟩
        (arr β′ ∘ p₁ pullback′) ∘ universal pullback′ _ ≈⟨ extendˡ (p₁∘universal≈h₁ pullback′) ⟩
        (arr β′ ∘ arr β) ∘ p₁ pullback                                          ∎
  in ⟺ (unique pullback″ β-chase α-chase)

--------------------------------------------------------------------------------
-- Associators

module _ (f : Span C D) (g : Span B C) (h : Span A B) where
  private
    pullback-fg    = (cod g) ×ₚ (dom f)
    pullback-gh    = (cod h) ×ₚ (dom g)
    pullback-⟨fg⟩h = (cod h) ×ₚ (dom (f ⊚₀ g))
    pullback-f⟨gh⟩ = (cod (g ⊚₀ h)) ×ₚ (dom f)

  ⊚-assoc : Span⇒ ((f ⊚₀ g) ⊚₀ h) (f ⊚₀ (g ⊚₀ h))
  ⊚-assoc = record
    { arr = universal pullback-f⟨gh⟩ {h₁ = universal pullback-gh (commute pullback-⟨fg⟩h ○ assoc)} $ begin
        (cod g ∘ p₂ pullback-gh) ∘ universal pullback-gh _ ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-gh) ⟩
        cod g ∘ p₁ pullback-fg ∘ p₂ pullback-⟨fg⟩h         ≈⟨ extendʳ (commute pullback-fg) ⟩
        dom f ∘ p₂ pullback-fg ∘ p₂ pullback-⟨fg⟩h         ∎
    ; commute-dom = begin
        ((dom h ∘ p₁ pullback-gh) ∘ p₁ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _ ≈⟨ pullʳ (p₁∘universal≈h₁ pullback-f⟨gh⟩) ⟩
        (dom h ∘ p₁ pullback-gh) ∘ universal pullback-gh _                          ≈⟨ pullʳ (p₁∘universal≈h₁ pullback-gh) ⟩
        dom h ∘ p₁ pullback-⟨fg⟩h                                                   ∎
    ; commute-cod = begin
        (cod f ∘ p₂ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _ ≈⟨ extendˡ (p₂∘universal≈h₂ pullback-f⟨gh⟩) ⟩
        (cod f ∘ p₂ pullback-fg) ∘ p₂ pullback-⟨fg⟩h             ∎
    }

  ⊚-assoc⁻¹ :  Span⇒ (f ⊚₀ (g ⊚₀ h)) ((f ⊚₀ g) ⊚₀ h)
  ⊚-assoc⁻¹ = record
    { arr = universal pullback-⟨fg⟩h {h₁ = p₁ pullback-gh ∘ p₁ pullback-f⟨gh⟩} {h₂ = universal pullback-fg (⟺ assoc ○ commute pullback-f⟨gh⟩)} $ begin
        cod h ∘ p₁ pullback-gh ∘ p₁ pullback-f⟨gh⟩         ≈⟨ extendʳ (commute pullback-gh) ⟩
        dom g ∘ p₂ pullback-gh ∘ p₁ pullback-f⟨gh⟩         ≈⟨ pushʳ (⟺ (p₁∘universal≈h₁ pullback-fg)) ⟩
        (dom g ∘ p₁ pullback-fg) ∘ universal pullback-fg _ ∎
      ; commute-dom = begin
        (dom h ∘ p₁ pullback-⟨fg⟩h) ∘ universal pullback-⟨fg⟩h _ ≈⟨ extendˡ (p₁∘universal≈h₁ pullback-⟨fg⟩h) ⟩
        (dom h ∘ p₁ pullback-gh) ∘ p₁ pullback-f⟨gh⟩             ∎
    ; commute-cod = begin
        ((cod f ∘ p₂ pullback-fg) ∘ p₂ pullback-⟨fg⟩h) ∘ universal pullback-⟨fg⟩h _ ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-⟨fg⟩h) ⟩
        (cod f ∘ p₂ pullback-fg) ∘ universal pullback-fg _                          ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-fg) ⟩
        cod f ∘ p₂ pullback-f⟨gh⟩                                                   ∎
    }

  ⊚-assoc-iso : Iso (Spans₁ A D) ⊚-assoc ⊚-assoc⁻¹
  ⊚-assoc-iso = record
    { isoˡ =
      let lemma-fgˡ = begin
            p₁ pullback-fg ∘ universal pullback-fg _ ∘ universal pullback-f⟨gh⟩ _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-fg) ⟩
            (p₂ pullback-gh ∘ p₁ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _     ≈⟨ pullʳ (p₁∘universal≈h₁ pullback-f⟨gh⟩) ⟩
            p₂ pullback-gh ∘ universal pullback-gh _                              ≈⟨ p₂∘universal≈h₂ pullback-gh ⟩
            p₁ pullback-fg ∘ p₂ pullback-⟨fg⟩h                                    ∎

          lemma-fgʳ = begin
            p₂ pullback-fg ∘ universal pullback-fg _ ∘ universal pullback-f⟨gh⟩ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-fg) ⟩
            p₂ pullback-f⟨gh⟩ ∘ universal pullback-f⟨gh⟩ _                        ≈⟨ p₂∘universal≈h₂ pullback-f⟨gh⟩ ⟩
            p₂ pullback-fg ∘ p₂ pullback-⟨fg⟩h                                    ∎

          lemmaˡ = begin
            p₁ pullback-⟨fg⟩h ∘ universal pullback-⟨fg⟩h _ ∘ universal pullback-f⟨gh⟩ _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-⟨fg⟩h) ⟩
            (p₁ pullback-gh ∘ p₁ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _           ≈⟨ pullʳ (p₁∘universal≈h₁ pullback-f⟨gh⟩) ⟩
            p₁ pullback-gh ∘ universal pullback-gh _                                    ≈⟨ p₁∘universal≈h₁ pullback-gh ⟩
            p₁ pullback-⟨fg⟩h                                                           ∎

          lemmaʳ = begin
            p₂ pullback-⟨fg⟩h ∘ universal pullback-⟨fg⟩h _ ∘ universal pullback-f⟨gh⟩ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-⟨fg⟩h) ⟩
            universal pullback-fg _ ∘ universal pullback-f⟨gh⟩ _                        ≈⟨ unique-diagram pullback-fg lemma-fgˡ lemma-fgʳ ⟩
            p₂ pullback-⟨fg⟩h                                                           ∎
      in unique pullback-⟨fg⟩h lemmaˡ lemmaʳ ○ ⟺ (Pullback.id-unique pullback-⟨fg⟩h)
    ; isoʳ =
      let lemma-ghˡ = begin
            p₁ pullback-gh ∘ universal pullback-gh _ ∘ universal pullback-⟨fg⟩h _ ≈⟨  pullˡ (p₁∘universal≈h₁ pullback-gh) ⟩
            p₁ pullback-⟨fg⟩h ∘ universal pullback-⟨fg⟩h _                        ≈⟨  p₁∘universal≈h₁ pullback-⟨fg⟩h ⟩
            p₁ pullback-gh ∘ p₁ pullback-f⟨gh⟩                                    ∎

          lemma-ghʳ = begin
            p₂ pullback-gh ∘ universal pullback-gh _ ∘ universal pullback-⟨fg⟩h _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-gh) ⟩
            (p₁ pullback-fg ∘ p₂ pullback-⟨fg⟩h) ∘ universal pullback-⟨fg⟩h _     ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-⟨fg⟩h) ⟩
            p₁ pullback-fg ∘ universal pullback-fg _                              ≈⟨ p₁∘universal≈h₁ pullback-fg ⟩
            p₂ pullback-gh ∘ p₁ pullback-f⟨gh⟩ ∎

          lemmaˡ = begin
            p₁ pullback-f⟨gh⟩ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-⟨fg⟩h _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-f⟨gh⟩) ⟩
            universal pullback-gh _ ∘ universal pullback-⟨fg⟩h _                        ≈⟨ unique-diagram pullback-gh lemma-ghˡ lemma-ghʳ ⟩
            p₁ pullback-f⟨gh⟩                                                           ∎
          lemmaʳ = begin
            p₂ pullback-f⟨gh⟩ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-⟨fg⟩h _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-f⟨gh⟩) ⟩
            (p₂ pullback-fg ∘ p₂ pullback-⟨fg⟩h) ∘ universal pullback-⟨fg⟩h _           ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-⟨fg⟩h) ⟩
            p₂ pullback-fg ∘ universal pullback-fg _                                    ≈⟨ p₂∘universal≈h₂ pullback-fg ⟩
            p₂ pullback-f⟨gh⟩                                                           ∎
      in unique pullback-f⟨gh⟩ lemmaˡ lemmaʳ ○ ⟺ (Pullback.id-unique pullback-f⟨gh⟩)
    }

⊚-assoc-commute : ∀ {f f′ : Span C D} {g g′ : Span B C} {h h′ : Span A B} → (α : Span⇒ f f′) → (β : Span⇒ g g′) → (γ : Span⇒ h h′)
            → Spans₁ A D [ Spans₁ A D [ ⊚-assoc f′ g′ h′ ∘ (α ⊚₁ β) ⊚₁ γ ] ≈ Spans₁ A D [ α ⊚₁ (β ⊚₁ γ) ∘ ⊚-assoc f g h ] ]
⊚-assoc-commute {f = f} {f′ = f′} {g = g} {g′ = g′} {h = h} {h′ = h′} α β γ =
  let pullback-fg     = (cod g) ×ₚ (dom f)
      pullback-fg′    = (cod g′) ×ₚ (dom f′)
      pullback-gh     = (cod h) ×ₚ (dom g)
      pullback-gh′    = (cod h′) ×ₚ (dom g′)
      pullback-f⟨gh⟩  = (cod (g ⊚₀ h)) ×ₚ (dom f)
      pullback-f⟨gh⟩′ = (cod (g′ ⊚₀ h′)) ×ₚ (dom f′)
      pullback-⟨fg⟩h  = (cod h) ×ₚ (dom (f ⊚₀ g))
      pullback-⟨fg⟩h′ = (cod h′) ×ₚ (dom (f′ ⊚₀ g′))

      lemma-ghˡ′ = begin
        p₁ pullback-gh′ ∘ universal pullback-gh′ _ ∘ universal pullback-⟨fg⟩h′ _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-gh′) ⟩
        p₁ pullback-⟨fg⟩h′ ∘ universal pullback-⟨fg⟩h′ _                         ≈⟨ p₁∘universal≈h₁ pullback-⟨fg⟩h′ ⟩
        arr γ ∘ p₁ pullback-⟨fg⟩h                                                ≈⟨ pushʳ (⟺ (p₁∘universal≈h₁ pullback-gh)) ⟩
        (arr γ ∘ p₁ pullback-gh) ∘ universal pullback-gh _                       ≈⟨ pushˡ (⟺ (p₁∘universal≈h₁ pullback-gh′)) ⟩
        p₁ pullback-gh′ ∘ universal pullback-gh′ _ ∘ universal pullback-gh _     ∎

      lemma-ghʳ′ = begin
        p₂ pullback-gh′ ∘ universal pullback-gh′ _ ∘ universal pullback-⟨fg⟩h′ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-gh′) ⟩
        (p₁ pullback-fg′ ∘ p₂ pullback-⟨fg⟩h′) ∘ universal pullback-⟨fg⟩h′ _     ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-⟨fg⟩h′) ⟩
        p₁ pullback-fg′ ∘ universal pullback-fg′ _ ∘ p₂ pullback-⟨fg⟩h           ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-fg′) ⟩
        (arr β ∘ p₁ pullback-fg) ∘ p₂ pullback-⟨fg⟩h                             ≈⟨ extendˡ (⟺ (p₂∘universal≈h₂ pullback-gh)) ⟩
        (arr β ∘ p₂ pullback-gh) ∘ universal pullback-gh _                       ≈⟨ pushˡ (⟺ (p₂∘universal≈h₂ pullback-gh′)) ⟩
        p₂ pullback-gh′ ∘ universal pullback-gh′ _ ∘ universal pullback-gh _     ∎

      lemmaˡ = begin
        p₁ pullback-f⟨gh⟩′ ∘ universal pullback-f⟨gh⟩′ _ ∘ universal pullback-⟨fg⟩h′ _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-f⟨gh⟩′) ⟩
        universal pullback-gh′ _ ∘ universal pullback-⟨fg⟩h′ _                         ≈⟨ unique-diagram pullback-gh′ lemma-ghˡ′ lemma-ghʳ′ ⟩
        universal pullback-gh′ _ ∘ universal pullback-gh _                             ≈⟨ pushʳ (⟺ (p₁∘universal≈h₁ pullback-f⟨gh⟩)) ⟩
        (universal pullback-gh′ _ ∘ p₁ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _    ≈⟨ pushˡ (⟺ (p₁∘universal≈h₁ pullback-f⟨gh⟩′)) ⟩
        p₁ pullback-f⟨gh⟩′ ∘ universal pullback-f⟨gh⟩′ _ ∘ universal pullback-f⟨gh⟩ _  ∎

      lemmaʳ = begin
        p₂ pullback-f⟨gh⟩′ ∘ universal pullback-f⟨gh⟩′ _ ∘ universal pullback-⟨fg⟩h′ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-f⟨gh⟩′) ⟩
        (p₂ pullback-fg′ ∘ p₂ pullback-⟨fg⟩h′) ∘ universal pullback-⟨fg⟩h′ _           ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-⟨fg⟩h′) ⟩
        p₂ pullback-fg′ ∘ universal pullback-fg′ _ ∘ p₂ pullback-⟨fg⟩h                 ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-fg′) ⟩
        (arr α ∘ p₂ pullback-fg) ∘ p₂ pullback-⟨fg⟩h                                   ≈⟨ extendˡ (⟺ (p₂∘universal≈h₂ pullback-f⟨gh⟩)) ⟩
        (arr α ∘ p₂ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _                       ≈⟨ pushˡ (⟺ (p₂∘universal≈h₂ pullback-f⟨gh⟩′)) ⟩
        p₂ pullback-f⟨gh⟩′ ∘ universal pullback-f⟨gh⟩′ _ ∘ universal pullback-f⟨gh⟩ _  ∎

  in unique-diagram pullback-f⟨gh⟩′ lemmaˡ lemmaʳ

--------------------------------------------------------------------------------
-- Unitors

module _ (f : Span A B) where
  private
    pullback-dom-f = id ×ₚ (dom f)
    pullback-cod-f = (cod f) ×ₚ id

  ⊚-unitˡ : Span⇒ (id-span ⊚₀ f) f
  ⊚-unitˡ = record
    { arr = p₁ pullback-cod-f
    ; commute-dom = refl
    ; commute-cod = commute pullback-cod-f
    }

  ⊚-unitˡ⁻¹ : Span⇒ f (id-span ⊚₀ f)
  ⊚-unitˡ⁻¹ = record
    { arr = universal pullback-cod-f id-comm
    ; commute-dom = cancelʳ (p₁∘universal≈h₁ pullback-cod-f)
    ; commute-cod = pullʳ (p₂∘universal≈h₂ pullback-cod-f) ○ identityˡ
    }

  ⊚-unitˡ-iso : Iso (Spans₁ A B) ⊚-unitˡ ⊚-unitˡ⁻¹
  ⊚-unitˡ-iso = record
    { isoˡ = unique-diagram pullback-cod-f (pullˡ (p₁∘universal≈h₁ pullback-cod-f) ○ id-comm-sym) (pullˡ (p₂∘universal≈h₂ pullback-cod-f) ○ commute pullback-cod-f ○ id-comm-sym)
    ; isoʳ = p₁∘universal≈h₁ pullback-cod-f
    }

  ⊚-unitʳ : Span⇒ (f ⊚₀ id-span) f
  ⊚-unitʳ = record
    { arr = p₂ pullback-dom-f
    ; commute-dom = ⟺ (commute pullback-dom-f)
    ; commute-cod = refl
    }

  ⊚-unitʳ⁻¹ : Span⇒ f (f ⊚₀ id-span)
  ⊚-unitʳ⁻¹ = record
    { arr = universal pullback-dom-f id-comm-sym
    ; commute-dom = pullʳ (p₁∘universal≈h₁ pullback-dom-f) ○ identityˡ
    ; commute-cod = pullʳ (p₂∘universal≈h₂ pullback-dom-f) ○ identityʳ
    }

  ⊚-unitʳ-iso : Iso (Spans₁ A B) ⊚-unitʳ ⊚-unitʳ⁻¹
  ⊚-unitʳ-iso = record
    { isoˡ = unique-diagram pullback-dom-f (pullˡ (p₁∘universal≈h₁ pullback-dom-f) ○ ⟺ (commute pullback-dom-f) ○ id-comm-sym) (pullˡ (p₂∘universal≈h₂ pullback-dom-f) ○ id-comm-sym)
    ; isoʳ = p₂∘universal≈h₂ pullback-dom-f
    }

⊚-unitˡ-commute : ∀ {f f′ : Span A B} → (α : Span⇒ f f′) → Spans₁ A B [ Spans₁ A B [ ⊚-unitˡ f′ ∘ Spans₁.id B B ⊚₁ α ] ≈ Spans₁ A B [ α ∘ ⊚-unitˡ f ] ]
⊚-unitˡ-commute {f′ = f′} α = p₁∘universal≈h₁ ((cod f′) ×ₚ id)

⊚-unitʳ-commute : ∀ {f f′ : Span A B} → (α : Span⇒ f f′) → Spans₁ A B [ Spans₁ A B [ ⊚-unitʳ f′ ∘ α ⊚₁ Spans₁.id A A ] ≈ Spans₁ A B [ α ∘ ⊚-unitʳ f ] ]
⊚-unitʳ-commute {f′ = f′} α = p₂∘universal≈h₂ (id ×ₚ (dom f′))

--------------------------------------------------------------------------------
-- Coherence Conditions

triangle : (f : Span A B) → (g : Span B C) → Spans₁ A C [ Spans₁ A C [ Spans₁.id B C {g} ⊚₁ ⊚-unitˡ f ∘ ⊚-assoc g id-span f ] ≈ ⊚-unitʳ g ⊚₁ Spans₁.id A B {f} ]
triangle f g =
  let pullback-dom-g = id ×ₚ (dom g)
      pullback-cod-f = (cod f) ×ₚ id
      pullback-fg    = (cod f) ×ₚ (dom g)
      pullback-id-fg = (cod (id-span ⊚₀ f)) ×ₚ (dom g)
      pullback-f-id-g = (cod f) ×ₚ (dom (id-span ⊚₀ g))
  in unique pullback-fg (pullˡ (p₁∘universal≈h₁ pullback-fg) ○ pullʳ (p₁∘universal≈h₁ pullback-id-fg) ○ p₁∘universal≈h₁ pullback-cod-f ○ ⟺ identityˡ)
                        (pullˡ (p₂∘universal≈h₂ pullback-fg) ○ pullʳ (p₂∘universal≈h₂ pullback-id-fg) ○ identityˡ)

pentagon : (f : Span A B) → (g : Span B C) → (h : Span C D) → (i : Span D E)
         →  Spans₁ A E [ Spans₁ A E [ (Spans₁.id D E {i}) ⊚₁ (⊚-assoc h g f) ∘ Spans₁ A E [ ⊚-assoc i (h ⊚₀ g) f ∘ ⊚-assoc i h g ⊚₁ Spans₁.id A B {f} ] ] ≈ Spans₁ A E [ ⊚-assoc i h (g ⊚₀ f) ∘ ⊚-assoc (i ⊚₀ h) g f ] ]
pentagon {A} {B} {C} {D} {E} f g h i =
  let pullback-fg       = (cod f) ×ₚ (dom g)
      pullback-gh       = (cod g) ×ₚ (dom h)
      pullback-hi       = (cod h) ×ₚ (dom i)
      pullback-f⟨gh⟩    = (cod f) ×ₚ (dom (h ⊚₀ g))
      pullback-⟨fg⟩h    = (cod (g ⊚₀ f)) ×ₚ (dom h)
      pullback-⟨gh⟩i    = (cod (h ⊚₀ g)) ×ₚ (dom i)
      pullback-g⟨hi⟩    = (cod g) ×ₚ (dom (i ⊚₀ h))
      pullback-⟨⟨fg⟩h⟩i = (cod (h ⊚₀ (g ⊚₀ f))) ×ₚ (dom i)
      pullback-⟨f⟨gh⟩⟩i = (cod ((h ⊚₀ g) ⊚₀ f)) ×ₚ (dom i)
      pullback-⟨fg⟩⟨hi⟩ = (cod (g ⊚₀ f)) ×ₚ (dom (i ⊚₀ h))
      pullback-f⟨⟨gh⟩i⟩ = (cod f) ×ₚ (dom (i ⊚₀ (h ⊚₀ g)))
      pullback-f⟨g⟨hi⟩⟩ = (cod f) ×ₚ (dom ((i ⊚₀ h) ⊚₀ g))

      lemma-fgˡ = begin
        p₁ pullback-fg ∘ universal pullback-fg _ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-fg) ⟩
        p₁ pullback-f⟨gh⟩ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _                        ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-f⟨gh⟩) ⟩
        p₁ pullback-f⟨⟨gh⟩i⟩ ∘ universal pullback-f⟨⟨gh⟩i⟩ _                                                  ≈⟨ p₁∘universal≈h₁ pullback-f⟨⟨gh⟩i⟩ ⟩
        id ∘ p₁ pullback-f⟨g⟨hi⟩⟩                                                                             ≈⟨ identityˡ ⟩
        p₁ pullback-f⟨g⟨hi⟩⟩                                                                                ≈˘⟨ p₁∘universal≈h₁ pullback-fg ⟩
        p₁ pullback-fg ∘ universal pullback-fg _                                                              ∎

      lemma-fgʳ = begin
        p₂ pullback-fg ∘ universal pullback-fg _ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-fg) ⟩
        (p₁ pullback-gh ∘ p₂ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _     ≈⟨ center (p₂∘universal≈h₂ pullback-f⟨gh⟩) ⟩
        p₁ pullback-gh ∘ (p₁ pullback-⟨gh⟩i ∘ p₂ pullback-f⟨⟨gh⟩i⟩) ∘ universal pullback-f⟨⟨gh⟩i⟩ _           ≈⟨ center⁻¹ refl (p₂∘universal≈h₂ pullback-f⟨⟨gh⟩i⟩) ⟩
        (p₁ pullback-gh ∘ p₁ pullback-⟨gh⟩i) ∘ universal pullback-⟨gh⟩i _ ∘ p₂ pullback-f⟨g⟨hi⟩⟩              ≈⟨ center (p₁∘universal≈h₁ pullback-⟨gh⟩i) ⟩
        p₁ pullback-gh ∘ universal pullback-gh _ ∘ p₂ pullback-f⟨g⟨hi⟩⟩                                       ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-gh) ⟩
        p₁ pullback-g⟨hi⟩ ∘ p₂ pullback-f⟨g⟨hi⟩⟩                                                              ≈˘⟨ p₂∘universal≈h₂ pullback-fg ⟩
        p₂ pullback-fg ∘ universal pullback-fg _                                                              ∎

      lemma-⟨fg⟩hˡ = begin
        p₁ pullback-⟨fg⟩h ∘ universal pullback-⟨fg⟩h _ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-⟨fg⟩h) ⟩
        universal pullback-fg _ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _                        ≈⟨ unique-diagram pullback-fg lemma-fgˡ lemma-fgʳ ⟩
        universal pullback-fg _                                                                                ≈˘⟨ p₁∘universal≈h₁ pullback-⟨fg⟩⟨hi⟩ ⟩
        p₁ pullback-⟨fg⟩⟨hi⟩ ∘ universal pullback-⟨fg⟩⟨hi⟩ _                                                        ≈⟨ pushˡ (⟺ (p₁∘universal≈h₁ pullback-⟨fg⟩h)) ⟩
        p₁ pullback-⟨fg⟩h ∘ universal pullback-⟨fg⟩h _ ∘ universal pullback-⟨fg⟩⟨hi⟩ _                              ∎

      lemma-⟨fg⟩hʳ = begin
        p₂ pullback-⟨fg⟩h ∘ universal pullback-⟨fg⟩h _ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-⟨fg⟩h) ⟩
        (p₂ pullback-gh ∘ p₂ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _           ≈⟨ center (p₂∘universal≈h₂ pullback-f⟨gh⟩) ⟩
        p₂ pullback-gh ∘ (p₁ pullback-⟨gh⟩i ∘ p₂ pullback-f⟨⟨gh⟩i⟩) ∘ universal pullback-f⟨⟨gh⟩i⟩ _                 ≈⟨ center⁻¹ refl (p₂∘universal≈h₂ pullback-f⟨⟨gh⟩i⟩) ⟩
        (p₂ pullback-gh ∘ p₁ pullback-⟨gh⟩i) ∘ universal pullback-⟨gh⟩i _ ∘ p₂ pullback-f⟨g⟨hi⟩⟩                    ≈⟨ center (p₁∘universal≈h₁ pullback-⟨gh⟩i) ⟩
        p₂ pullback-gh ∘ universal pullback-gh _ ∘ p₂ pullback-f⟨g⟨hi⟩⟩                                             ≈⟨ extendʳ (p₂∘universal≈h₂ pullback-gh) ⟩
        p₁ pullback-hi ∘ p₂ pullback-g⟨hi⟩ ∘ p₂ pullback-f⟨g⟨hi⟩⟩                                                   ≈⟨ pushʳ (⟺ (p₂∘universal≈h₂ pullback-⟨fg⟩⟨hi⟩)) ⟩
        (p₁ pullback-hi ∘ p₂ pullback-⟨fg⟩⟨hi⟩) ∘ universal pullback-⟨fg⟩⟨hi⟩ _                                     ≈⟨ pushˡ (⟺ (p₂∘universal≈h₂ pullback-⟨fg⟩h)) ⟩
        p₂ pullback-⟨fg⟩h ∘ universal pullback-⟨fg⟩h _ ∘ universal pullback-⟨fg⟩⟨hi⟩ _                              ∎

      lemmaˡ = begin
        p₁ pullback-⟨⟨fg⟩h⟩i ∘ universal pullback-⟨⟨fg⟩h⟩i _ ∘ universal pullback-⟨f⟨gh⟩⟩i _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-⟨⟨fg⟩h⟩i) ⟩
        (universal pullback-⟨fg⟩h _ ∘ p₁ pullback-⟨f⟨gh⟩⟩i) ∘ universal pullback-⟨f⟨gh⟩⟩i _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _  ≈⟨ center (p₁∘universal≈h₁ pullback-⟨f⟨gh⟩⟩i) ⟩
        universal pullback-⟨fg⟩h _ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _                              ≈⟨ unique-diagram pullback-⟨fg⟩h lemma-⟨fg⟩hˡ lemma-⟨fg⟩hʳ ⟩
        universal pullback-⟨fg⟩h _ ∘ universal pullback-⟨fg⟩⟨hi⟩ _                                                           ≈⟨ pushˡ (⟺ (p₁∘universal≈h₁ pullback-⟨⟨fg⟩h⟩i)) ⟩
        p₁ pullback-⟨⟨fg⟩h⟩i ∘ universal pullback-⟨⟨fg⟩h⟩i _ ∘ universal pullback-⟨fg⟩⟨hi⟩ _                                 ∎

      lemmaʳ = begin
        p₂ pullback-⟨⟨fg⟩h⟩i ∘ universal pullback-⟨⟨fg⟩h⟩i _ ∘ universal pullback-⟨f⟨gh⟩⟩i _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-⟨⟨fg⟩h⟩i) ⟩
        (id ∘ p₂ pullback-⟨f⟨gh⟩⟩i) ∘ universal pullback-⟨f⟨gh⟩⟩i _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _                          ≈⟨ center (p₂∘universal≈h₂ pullback-⟨f⟨gh⟩⟩i) ⟩
        id ∘ (p₂ pullback-⟨gh⟩i ∘ p₂ pullback-f⟨⟨gh⟩i⟩) ∘ universal pullback-f⟨⟨gh⟩i⟩ _                                      ≈⟨ center⁻¹ identityˡ (p₂∘universal≈h₂ pullback-f⟨⟨gh⟩i⟩) ⟩
        p₂ pullback-⟨gh⟩i ∘ universal pullback-⟨gh⟩i _ ∘ p₂ pullback-f⟨g⟨hi⟩⟩                                                ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-⟨gh⟩i) ⟩
        (p₂ pullback-hi ∘ p₂ pullback-g⟨hi⟩) ∘ p₂ pullback-f⟨g⟨hi⟩⟩                                                          ≈⟨ extendˡ (⟺ (p₂∘universal≈h₂ pullback-⟨fg⟩⟨hi⟩)) ⟩
        (p₂ pullback-hi ∘ p₂ pullback-⟨fg⟩⟨hi⟩) ∘ universal pullback-⟨fg⟩⟨hi⟩ _                                              ≈⟨ pushˡ (⟺ (p₂∘universal≈h₂ pullback-⟨⟨fg⟩h⟩i)) ⟩
        p₂ pullback-⟨⟨fg⟩h⟩i ∘ universal pullback-⟨⟨fg⟩h⟩i _ ∘ universal pullback-⟨fg⟩⟨hi⟩ _                                 ∎

  in unique-diagram pullback-⟨⟨fg⟩h⟩i lemmaˡ lemmaʳ

Spans : Bicategory (o ⊔ ℓ) (o ⊔ ℓ ⊔ e) e o
Spans = record
  { enriched = record
    { Obj = Obj
    ; hom = Spans₁
    ; id = λ {A} → record
      { F₀ = λ _ → id-span
      ; F₁ = λ _ → Spans₁.id A A
      ; identity = refl
      ; homomorphism = ⟺ identity²
      ; F-resp-≈ = λ _ → refl
      }
    ; ⊚ = record
      { F₀ = λ (f , g) → f ⊚₀ g
      ; F₁ = λ (α , β) → α ⊚₁ β
      ; identity = λ {(f , g)} → ⊚₁-identity f g
      ; homomorphism = λ {X} {Y} {Z} {(α , α′)} {(β , β′)} → ⊚₁-homomorphism α β α′ β′
      ; F-resp-≈ = λ {(f , g)} {(f′ , g′)} {_} {_} (α-eq , β-eq) → universal-resp-≈ ((cod g′) ×ₚ (dom f′)) (∘-resp-≈ˡ β-eq) (∘-resp-≈ˡ α-eq)
      }
    ; ⊚-assoc = niHelper record
      { η = λ ((f , g) , h) → ⊚-assoc f g h
      ; η⁻¹ = λ ((f , g) , h) → ⊚-assoc⁻¹ f g h
      ; commute = λ ((α , β) , γ) → ⊚-assoc-commute α β γ
      ; iso = λ ((f , g) , h) → ⊚-assoc-iso f g h
      }
    ; unitˡ = niHelper record
      { η = λ (_ , f) → ⊚-unitˡ f
      ; η⁻¹ = λ (_ , f) → ⊚-unitˡ⁻¹ f
      ; commute = λ (_ , α) → ⊚-unitˡ-commute α
      ; iso = λ (_ , f) → ⊚-unitˡ-iso f
      }
    ; unitʳ = niHelper record
      { η = λ (f , _) → ⊚-unitʳ f
      ; η⁻¹ = λ (f , _) → ⊚-unitʳ⁻¹ f
      ; commute = λ (α , _) → ⊚-unitʳ-commute α
      ; iso = λ (f , _) → ⊚-unitʳ-iso f
      }
    }
  ; triangle = λ {_} {_} {_} {f} {g} → triangle f g
  ; pentagon = λ {_} {_} {_} {_} {_} {f} {g} {h} {i} → pentagon f g h i
  }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

module Cubical.Categories.NaturalTransformation where

open import Cubical.Foundations.Prelude
open import Cubical.Categories.Category
open import Cubical.Categories.Functor

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

module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} where
  -- syntax for sequencing in category D
  _⋆ᴰ_ : ∀ {x y z} (f : D [ x , y ]) (g : D [ y , z ]) → D [ x , z ]
  f ⋆ᴰ g = f ⋆⟨ D ⟩ g

  record NatTrans (F G : Functor C D) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
    open Precategory
    open Functor

    field
      -- components of the natural transformation
      N-ob : (x : C .ob) → D [(F .F-ob x) , (G .F-ob x)]
      -- naturality condition
      N-hom : {x y : C .ob} (f : C [ x , y ]) → (F .F-hom f) ⋆ᴰ (N-ob y) ≡ (N-ob x) ⋆ᴰ (G .F-hom f)

  open Precategory
  open Functor
  open NatTrans

  idTrans : (F : Functor C D) → NatTrans F F
  idTrans F .N-ob x = D .id (F .F-ob x)
  idTrans F .N-hom f =
     (F .F-hom f) ⋆ᴰ (idTrans F .N-ob _)
       ≡⟨ D .⋆IdR _ ⟩
     F .F-hom f
       ≡⟨ sym (D .⋆IdL _) ⟩
     (D .id (F .F-ob _)) ⋆ᴰ (F .F-hom f)
       ∎

  seqTrans : {F G H : Functor C D} (α : NatTrans F G) (β : NatTrans G H) → NatTrans F H
  seqTrans α β .N-ob x = (α .N-ob x) ⋆ᴰ (β .N-ob x)
  seqTrans {F} {G} {H} α β .N-hom f =
    (F .F-hom f) ⋆ᴰ ((α .N-ob _) ⋆ᴰ (β .N-ob _))
      ≡⟨ sym (D .⋆Assoc _ _ _) ⟩
    ((F .F-hom f) ⋆ᴰ (α .N-ob _)) ⋆ᴰ (β .N-ob _)
      ≡[ i ]⟨ (α .N-hom f i) ⋆ᴰ (β .N-ob _) ⟩
    ((α .N-ob _) ⋆ᴰ (G .F-hom f)) ⋆ᴰ (β .N-ob _)
      ≡⟨ D .⋆Assoc _ _ _ ⟩
    (α .N-ob _) ⋆ᴰ ((G .F-hom f) ⋆ᴰ (β .N-ob _))
      ≡[ i ]⟨ (α .N-ob _) ⋆ᴰ (β .N-hom f i) ⟩
    (α .N-ob _) ⋆ᴰ ((β .N-ob _) ⋆ᴰ (H .F-hom f))
      ≡⟨ sym (D .⋆Assoc _ _ _) ⟩
    ((α .N-ob _) ⋆ᴰ (β .N-ob _)) ⋆ᴰ (H .F-hom f)
      ∎

  module _  ⦃ D-category : isCategory D ⦄ {F G : Functor C D} {α β : NatTrans F G} where
    open Precategory
    open Functor
    open NatTrans

    makeNatTransPath : α .N-ob ≡ β .N-ob → α ≡ β
    makeNatTransPath p i .N-ob = p i
    makeNatTransPath p i .N-hom f = rem i
      where
        rem : PathP (λ i → (F .F-hom f) ⋆ᴰ (p i _) ≡ (p i _) ⋆ᴰ (G .F-hom f)) (α .N-hom f) (β .N-hom f)
        rem = toPathP (D-category .isSetHom _ _ _ _)

module _ (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD') ⦃ _ : isCategory D ⦄ where
  open Precategory
  open NatTrans
  open Functor

  FUNCTOR : Precategory (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
  FUNCTOR .ob = Functor C D
  FUNCTOR .Hom[_,_] = NatTrans
  FUNCTOR .id = idTrans
  FUNCTOR ._⋆_ = seqTrans
  FUNCTOR .⋆IdL α = makeNatTransPath λ i x → D .⋆IdL (α .N-ob x) i
  FUNCTOR .⋆IdR α = makeNatTransPath λ i x → D .⋆IdR (α .N-ob x) i
  FUNCTOR .⋆Assoc α β γ = makeNatTransPath λ i x → D .⋆Assoc (α .N-ob x) (β .N-ob x) (γ .N-ob x) i


text:
{-

Part 3: Univalence and the SIP

- Univalence from ua and uaβ
- Transporting with ua (examples: ua not : Bool = Bool, ua suc : Z = Z, ...)
- Subst using ua
- The SIP as a consequence of ua
- Examples of using the SIP for math and programming (algebra, data
  structures, etc.)

-}

{-# OPTIONS --cubical #-}
module Part3 where

open import Cubical.Foundations.Prelude hiding (refl ; transport ; subst ; sym)
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Int

open import Part2 public

-- Another key concept in HoTT/UF is the Univalence Axiom. In Cubical
-- Agda this is provable, we hence refer to it as the Univalence
-- Theorem.

-- The univalence theorem: equivalences of types give paths of types
ua' : {A B : Type ℓ} → A ≃ B → A ≡ B
ua' = ua

-- Any isomorphism of types gives rise to an equivalence
isoToEquiv' : {A B : Type ℓ} → Iso A B → A ≃ B
isoToEquiv' = isoToEquiv

-- And hence to a path
isoToPath' : {A B : Type ℓ} → Iso A B → A ≡ B
isoToPath' e = ua' (isoToEquiv' e)

-- ua satisfies the following computation rule
-- This suffices to be able to prove the standard formulation of univalence.
uaβ' : {A B : Type ℓ} (e : A ≃ B) (x : A)
     → transport (ua' e) x ≡ fst e x
uaβ' e x = transportRefl (equivFun e x)

-- Time for an example!

-- Booleans
data Bool : Type₀ where
  false true : Bool

not : Bool → Bool
not false = true
not true  = false

notPath : Bool ≡ Bool
notPath = isoToPath' (iso not not rem rem)
  where
  rem : (b : Bool) → not (not b) ≡ b
  rem false = refl
  rem true  = refl

_ : transport notPath true ≡ false
_ = refl

-- Another example, integers:

sucPath : Int ≡ Int
sucPath = isoToPath' (iso sucInt predInt sucPred predSuc)

_ : transport sucPath (pos 0) ≡ pos 1
_ = refl

_ : transport (sucPath ∙ sucPath) (pos 0) ≡ pos 2
_ = refl

_ : transport (sym sucPath) (pos 0) ≡ negsuc 0
_ = refl

-------------------------------------------------------------------------
-- The structure identity principle

-- A more efficient version of finite multisets based on association lists
open import Cubical.HITs.AssocList.Base

-- data AssocList (A : Type) : Type where
--  ⟨⟩ : AssocList A
--  ⟨_,_⟩∷_ : (a : A) (n : ℕ) (xs : AssocList A) → AssocList A
--  per : (a b : A) (m n : ℕ) (xs : AssocList A)
--      → ⟨ a , m ⟩∷ ⟨ b , n ⟩∷ xs ≡ ⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs
--  agg : (a : A) (m n : ℕ) (xs : AssocList A)
--      → ⟨ a , m ⟩∷ ⟨ a , n ⟩∷ xs ≡ ⟨ a , m + n ⟩∷ xs
--  del : (a : A) (xs : AssocList A) → ⟨ a , 0 ⟩∷ xs ≡ xs
--  trunc : (xs ys : AssocList A) (p q : xs ≡ ys) → p ≡ q

-- Programming and proving is more complicated with AssocList compared
-- to FMSet. This kind of example occurs everywhere in programming and
-- mathematics: one representation is easier to work with, but not
-- efficient, while another is efficient but difficult to work with.

-- Solution: substitute using univalence
substIso : {A B : Type ℓ} (P : Type ℓ → Type ℓ') (e : Iso A B) → P A → P B
substIso P e = subst P (isoToPath e)

-- Can transport for example Monoid structure from FMSet to AssocList
-- this way, but the achieved Monoid structure is not very efficient
-- to work with. A better solution is to prove that FMSet and
-- AssocList are equal *as monoids*, but how to do this?

-- Solution: structure identity principle (SIP)
-- This is a very useful consequence of univalence
open import Cubical.Foundations.SIP

{-
sip' : {ℓ : Level} {S : Type ℓ → Type ℓ} {ι : StrEquiv S ℓ}
       (θ : UnivalentStr S ι) (A B : TypeWithStr ℓ S) → A ≃[ ι ] B → A ≡ B
sip' = sip
-}
-- The tricky thing is to prove that (S,ι) is a univalent structure.
-- Luckily we provide automation for this in the library, see for example:
-- open import Cubical.Algebra.Monoid.Base

-- Another cool application of the SIP: matrices represented as
-- functions out of pairs of Fin's and vectors are equal as abelian
-- groups:
open import Cubical.Algebra.Matrix


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

module Fin where

open import Cubical.Core.Everything using (_≡_; Level; Type; Σ; _,_; fst; snd; _≃_; ~_)

open import Cubical.Foundations.Prelude     using (refl; sym; _∙_; cong; transport; subst; funExt; transp; I; i0; i1)
open import Cubical.Foundations.Function    using (_∘_)
open import Cubical.Foundations.Isomorphism using (iso; Iso; isoToPath; section; retract)

open import Data.Fin   using (Fin; toℕ; fromℕ<; #_; _≟_) renaming (zero to fz; suc to fs)
open import Data.Nat   using (ℕ; zero; suc; _<_; _>_; z≤n; s≤s)

-- Alternate representation of Fin as a number and proof of its upper bound.
record Fin1 (n : ℕ) : Type where
  constructor fin1
  field
    r   : ℕ
    r<n : r < n

fin1suc : {n : ℕ} → Fin1 n → Fin1 (suc n)
fin1suc (fin1 r r<n) = fin1 (suc r) (s≤s r<n)

-- From Data.Fin.Properites
-- They need to be re-defined here since Cubical uses a different ≡

fromℕ<-toℕ : ∀ {m} (i : Fin m) (i<m : toℕ i < m) → fromℕ< i<m ≡ i
fromℕ<-toℕ fz     (s≤s z≤n)       = refl
fromℕ<-toℕ (fs i) (s≤s (s≤s m≤n)) = cong fs (fromℕ<-toℕ i (s≤s m≤n))

toℕ-fromℕ< : ∀ {m n} (m<n : m < n) → toℕ (fromℕ< m<n) ≡ m
toℕ-fromℕ< (s≤s z≤n)       = refl
toℕ-fromℕ< (s≤s (s≤s m<n)) = cong suc (toℕ-fromℕ< (s≤s m<n))

toℕ<n : ∀ {n} (i : Fin n) → toℕ i < n
toℕ<n fz     = s≤s z≤n
toℕ<n (fs i) = s≤s (toℕ<n i)

-------------------
-- Equivalence of Fin and Fin1

fin→fin1 : {n : ℕ} → Fin n → Fin1 n
fin→fin1 fz     = fin1 0 (s≤s z≤n)
fin→fin1 (fs x) = let fin1 r r<n = fin→fin1 x in fin1 (suc r) (s≤s r<n)

fin1→fin : {n : ℕ} → Fin1 n → Fin n
fin1→fin (fin1 _ r<n) = fromℕ< r<n

fin→fin1→fin : {n : ℕ} → (r : Fin n) → (fin1→fin ∘ fin→fin1) r ≡ r
fin→fin1→fin fz     = refl
fin→fin1→fin (fs r) = cong fs (fin→fin1→fin r)

fin1→fin→fin1 : {n : ℕ} → (r : Fin1 n) → (fin→fin1 ∘ fin1→fin) r ≡ r
fin1→fin→fin1 (fin1 zero    (s≤s z≤n))       = refl
fin1→fin→fin1 (fin1 (suc r) (s≤s (s≤s r<n))) = cong fin1suc (fin1→fin→fin1 (fin1 r (s≤s r<n)))

fin≃fin1 : {n : ℕ} → Iso (Fin n) (Fin1 n)
fin≃fin1 = iso fin→fin1 fin1→fin fin1→fin→fin1 fin→fin1→fin

fin≡fin1 : {n : ℕ} → Fin n ≡ Fin1 n
fin≡fin1 = isoToPath fin≃fin1

-- Equivalence of toℕ and Fin1.r

toℕ≡Fin1r1 : {n : ℕ} → (r : Fin n) → toℕ r ≡ Fin1.r (fin→fin1 r)
toℕ≡Fin1r1 fz     = refl
toℕ≡Fin1r1 (fs r) = cong suc (toℕ≡Fin1r1 r)

toℕ≡Fin1r : {n : ℕ} → toℕ {n} ≡ Fin1.r ∘ fin→fin1
toℕ≡Fin1r = funExt toℕ≡Fin1r1

Fin1r≡toℕ1 : {n : ℕ} → (r : Fin1 n) → toℕ (fin1→fin r) ≡ Fin1.r r
Fin1r≡toℕ1 (fin1 r r<n) = toℕ-fromℕ< r<n

Fin1r≡toℕ : {n : ℕ} → toℕ {n} ∘ fin1→fin ≡ Fin1.r
Fin1r≡toℕ = funExt Fin1r≡toℕ1

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
----------------------------------------------------------------------
-- Functional big-step evaluation of terms in the partiality monad
-- (alternative version not productivity checker workarounds)
----------------------------------------------------------------------

module SystemF.Eval.NoWorkarounds where

open import Codata.Musical.Notation using (∞; ♯_; ♭)
open import Category.Monad
open import Category.Monad.Partiality.All
open import Data.Fin using (Fin; zero; suc)
open import Data.Maybe as Maybe using (just; nothing)
open import Data.Maybe.Relation.Unary.Any as MaybeAny using (just)
open import Data.Nat using (_+_)
open import Data.Vec using ([])
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary

open import PartialityAndFailure as PF
open PF.Equality hiding (fail)
private
  open module M {f} = RawMonad (PF.monad {f}) using (return; _>>=_)

open import SystemF.Type
open import SystemF.Term
open import SystemF.WtTerm

open TypeSubst       using () renaming (_[/_]  to _[/tp_])
open TermTypeSubst   using () renaming (_[/_]  to _[/tmTp_])
open TermTermSubst   using () renaming (_[/_]  to _[/tmTm_])
open WtTermTypeSubst using () renaming (_[/_]′ to _[/⊢tmTp_])
open WtTermTermSubst using () renaming (_[/_]  to _[/⊢tmTm_])

open import SystemF.Eval as E
  using (Comp; _⊢comp_∈_; does-not-fail)

----------------------------------------------------------------------
-- Functional big-step semantics (alternative version)
--
-- The evaluation function _⇓ given below differs from that in
-- SystemF.Eval in that it evaluates terms directly in the
-- partiality-and-failure monad (rather than first evaluating them in
-- PartialityAndFailure.Workaround._?⊥P and subsequently interpreting
-- the result in PartialityAndFailure._?⊥).  This is achieved by
-- manually expanding and inlining every application of the monadic
-- bind operation.
--
-- We give a separate type soundness proof formulated with respect to
-- the alternative semantics, as well as a proof that the two
-- semantics are equivalent (i.e. the two evaluations of any given
-- term are bisimilar).
--
-- The definition of the alternative semantics is more verbose and
-- arguably less readable.  However the associated type soundness
-- proof is simpler in that it requires no additional compositionality
-- lemmas.

module _ where
  open M

  mutual

    infix 7 _⇓ _[_]⇓ _·⇓_

    -- Evaluation of untyped (open) terms.
    _⇓ : ∀ {m n} → Term m n → Comp m n
    var x ⇓      = fail
    Λ t ⇓        = return (Λ t)
    λ' a t ⇓     = return (λ' a t)
    μ a t ⇓      = later (♯ (t [/tmTm μ a t ] ⇓))
    (t [ a ]) ⇓  with t ⇓
    ... | c      = c [ a ]⇓
    (s · t) ⇓    with s ⇓ | t ⇓
    ... | f | c  = f ·⇓ c
    fold a t ⇓   with t ⇓
    ... | c      = fold⇓ a c
    unfold a t ⇓ with t ⇓
    ... | c      = unfold⇓ a c

    -- Evaluation of type application.
    _[_]⇓ : ∀ {m n} → Comp m n → Type n → Comp m n
    now (just (Λ t)) [ a ]⇓ = later (♯ (t [/tmTp a ] ⇓))
    now (just _)     [ _ ]⇓ = fail
    now nothing      [ _ ]⇓ = fail
    later c          [ a ]⇓ = later (♯ ((♭ c) [ a ]⇓))

    -- Evaluation of term application.
    _·⇓_ : ∀ {m n} → Comp m n → Comp m n → Comp m n
    now (just (λ' _ t)) ·⇓ now (just v) = later (♯ (t [/tmTm ⌜ v ⌝ ] ⇓))
    now (just _)        ·⇓ now _        = fail
    now nothing         ·⇓ _            = fail
    now f               ·⇓ later c      = later (♯ (now f ·⇓ (♭ c)))
    later f             ·⇓ c            = later (♯ ((♭ f) ·⇓ c))

    -- Evaluation of recursive type folding.
    fold⇓ : ∀ {m n} → Type (1 + n) → Comp m n → Comp m n
    fold⇓ a (now (just v)) = now (just (fold a v))
    fold⇓ _ (now nothing)  = fail
    fold⇓ a (later c)      = later (♯ fold⇓ a (♭ c))

    -- Evaluation of recursive type unfolding.
    unfold⇓ : ∀ {m n} → Type (1 + n) → Comp m n → Comp m n
    unfold⇓ _ (now (just (fold _ v))) = now (just v)
    unfold⇓ a (now (just _))          = fail
    unfold⇓ a (now nothing)           = fail
    unfold⇓ a (later c)               = later (♯ unfold⇓ a (♭ c))

----------------------------------------------------------------------
-- Type soundness wrt. to the alternative semantics

infix 4 ⊢comp_∈_

-- Short hand for closed well-typed computations.
⊢comp_∈_ : Comp 0 0 → Type 0 → Set
⊢comp c ∈ a = [] ⊢comp c ∈ a

mutual

  infix 7 ⊢_⇓ ⊢_[_]⇓ ⊢_·⇓_

  -- Evaluation of closed terms preserves well-typedness.
  ⊢_⇓ : ∀ {t a} → [] ⊢ t ∈ a → ⊢comp t ⇓ ∈ a
  ⊢ var ()      ⇓
  ⊢ Λ ⊢t        ⇓ = now (just (Λ ⊢t))
  ⊢ λ' a ⊢t     ⇓ = now (just (λ' a ⊢t))
  ⊢ μ a ⊢t      ⇓ = later (♯ ⊢ ⊢t [/⊢tmTm μ a ⊢t ] ⇓)
  ⊢ ⊢t [ a ]    ⇓ with ⊢ ⊢t ⇓
  ... | ⊢c        = ⊢ ⊢c [ a ]⇓
  ⊢ ⊢s · ⊢t     ⇓ with ⊢ ⊢s ⇓ | ⊢ ⊢t ⇓
  ... | ⊢f | ⊢c   = ⊢ ⊢f ·⇓ ⊢c
  ⊢ fold a ⊢t   ⇓ with ⊢ ⊢t ⇓
  ... | ⊢c        = ⊢fold⇓ a ⊢c
  ⊢ unfold a ⊢t ⇓ with ⊢ ⊢t ⇓
  ... | ⊢c        = ⊢unfold⇓ a ⊢c

  -- Evaluation of type application preserves well-typedness.
  ⊢_[_]⇓ : ∀ {c a} → ⊢comp c ∈ ∀' a → ∀ b → ⊢comp c [ b ]⇓ ∈ a [/tp b ]
  ⊢ now (just (Λ ⊢t)) [ a ]⇓ = later (♯ ⊢ ⊢t [/⊢tmTp a ] ⇓)
  ⊢ later ⊢c          [ a ]⇓ = later (♯ ⊢ (♭ ⊢c) [ a ]⇓)

  -- Evaluation of term application preserves well-typedness.
  ⊢_·⇓_ : ∀ {f c a b} → ⊢comp f ∈ a →' b → ⊢comp c ∈ a → ⊢comp f ·⇓ c ∈ b
  ⊢ now (just (λ' a ⊢t)) ·⇓ now (just ⊢v) =
    later (♯ (⊢ ⊢t [/⊢tmTm ⊢⌜ ⊢v ⌝ ] ⇓))
  ⊢ now (just (λ' a ⊢t)) ·⇓ later ⊢c =
    later (♯ (⊢ now (just (λ' a ⊢t)) ·⇓ ♭ ⊢c))
  ⊢ later ⊢f ·⇓ ⊢c = later (♯ (⊢ ♭ ⊢f ·⇓ ⊢c))

  -- Evaluation of recursive type folding preserves well-typedness.
  ⊢fold⇓ : ∀ {c} a → ⊢comp c ∈ a [/tp μ a ] → ⊢comp fold⇓ a c ∈ μ a
  ⊢fold⇓ a (now (just ⊢v)) = now (just (fold a ⊢v))
  ⊢fold⇓ a (later ⊢c)      = later (♯ ⊢fold⇓ a (♭ ⊢c))

  -- Evaluation of recursive type unfolding preserves well-typedness.
  ⊢unfold⇓ : ∀ {c} a → ⊢comp c ∈ μ a → ⊢comp unfold⇓ a c ∈ a [/tp μ a ]
  ⊢unfold⇓ _ (now (just (fold ._ ⊢v))) = now (just ⊢v)
  ⊢unfold⇓ a (later ⊢c)                = later (♯ ⊢unfold⇓ a (♭ ⊢c))

-- Type soundness: evaluation of well-typed terms does not fail.
type-soundness : ∀ {t a} → [] ⊢ t ∈ a → ¬ t ⇓ ≈ fail
type-soundness ⊢t = does-not-fail ⊢ ⊢t ⇓

----------------------------------------------------------------------
-- Equivalence (bisimilarity) of big-step semantics

open PF.Workaround using (⟦_⟧P)
open PF.Equivalence hiding (sym)
open PF.AlternativeEquality
  renaming (return to returnP; fail to failP; _>>=_ to _>>=P_)

-- Bind-expanded variants of the various helpers of of _⇓.

_[_]⇓′ : ∀ {m n} → Comp m n → Type n → Comp m n
c [ a ]⇓′ = c >>= λ v → (return v) [ a ]⇓

_·⇓′_ : ∀ {m n} → Comp m n → Comp m n → Comp m n
c ·⇓′ d = c >>= λ f → d >>= λ v → (return f) ·⇓ (return v)

fold⇓′ : ∀ {m n} → Type (1 + n) → Comp m n → Comp m n
fold⇓′ a c = c >>= λ v → fold⇓ a (return v)

unfold⇓′ : ∀ {m n} → Type (1 + n) → Comp m n → Comp m n
unfold⇓′ a c = c >>= λ v → unfold⇓ a (return v)

-- The two variants of _[_]⇓ are strongly bisimilar.
_[_]⇓≅ : ∀ {m n} (c : Comp m n) (a : Type n) → c [ a ]⇓ ≅ c [ a ]⇓′
now (just _) [ _ ]⇓≅ = refl P.refl
now nothing  [ _ ]⇓≅ = now P.refl
later c      [ a ]⇓≅ = later (♯ ((♭ c) [ a ]⇓≅))

-- The two variants of _·⇓_ are strongly bisimilar.
_·⇓≅_ : ∀ {m n} (c : Comp m n) (d : Comp m n) → c ·⇓ d ≅ c ·⇓′ d
now (just _)          ·⇓≅ now (just _) = refl P.refl
now (just (Λ t))      ·⇓≅ now nothing  = now P.refl
now (just (λ' a t))   ·⇓≅ now nothing  = now P.refl
now (just (fold a t)) ·⇓≅ now nothing  = now P.refl
now nothing           ·⇓≅ now v   = now P.refl
now (just (Λ t))      ·⇓≅ later d = later (♯ (now (just (Λ t))      ·⇓≅ ♭ d))
now (just (λ' a t))   ·⇓≅ later d = later (♯ (now (just (λ' a t))   ·⇓≅ ♭ d))
now (just (fold a t)) ·⇓≅ later d = later (♯ (now (just (fold a t)) ·⇓≅ ♭ d))
now nothing           ·⇓≅ later d = now P.refl
later c               ·⇓≅ d       = later (♯ ((♭ c) ·⇓≅ d))

-- The two variants of fold⇓ are strongly bisimilar.
fold⇓≅ : ∀ {m n} (a : Type (1 + n)) (c : Comp m n) → fold⇓ a c ≅ fold⇓′ a c
fold⇓≅ a (now (just v)) = now P.refl
fold⇓≅ a (now nothing)  = now P.refl
fold⇓≅ a (later c)      = later (♯ fold⇓≅ a (♭ c))

-- The two variants of unfold⇓ are strongly bisimilar.
unfold⇓≅ : ∀ {m n} (a : Type (1 + n)) (c : Comp m n) →
           unfold⇓ a c ≅ unfold⇓′ a c
unfold⇓≅ a (now (just v)) = refl P.refl
unfold⇓≅ a (now nothing)  = now P.refl
unfold⇓≅ a (later c)      = later (♯ unfold⇓≅ a (♭ c))

mutual

  -- Helper lemma relating the two semantics of type application.
  []-E⇓≅⇓′ : ∀ {m n} (v : Val m n) (a : Type n) →
             ⟦ v E.[ a ]′ ⟧P ≅P (return v) [ a ]⇓
  []-E⇓≅⇓′ (Λ t)      a = later (♯ E⇓≅⇓′ (t [/tmTp a ] ))
  []-E⇓≅⇓′ (λ' _ _)   _ = failP
  []-E⇓≅⇓′ (fold _ _) _ = failP

  -- Helper lemma relating the two semantics of term application.
  ·-E⇓≅⇓′ : ∀ {m n} (f : Val m n) (v : Val m n) →
            ⟦ f E.·′ v ⟧P ≅P (return f) ·⇓ (return v)
  ·-E⇓≅⇓′ (Λ _)      _ = failP
  ·-E⇓≅⇓′ (λ' a t)   v = later (♯ E⇓≅⇓′ (t [/tmTm ⌜ v ⌝ ]))
  ·-E⇓≅⇓′ (fold _ _) _ = failP

  -- Helper lemma relating the two semantics of recursive type
  -- unfolding.
  unfold-E⇓≅⇓′ : ∀ {m n} (a : Type (1 + n)) (v : Val m n) →
                 ⟦ E.unfold′ a v ⟧P ≅P unfold⇓ a (return v)
  unfold-E⇓≅⇓′ _ (Λ _)      = failP
  unfold-E⇓≅⇓′ _ (λ' _ _)   = failP
  unfold-E⇓≅⇓′ _ (fold _ _) = returnP P.refl

  -- The two semantics are ≅P-equivalent.
  E⇓≅⇓′ : ∀ {m n} (t : Term m n) → t E.⇓ ≅P t ⇓
  E⇓≅⇓′ (var x)           = failP
  E⇓≅⇓′ (Λ t)             = returnP P.refl
  E⇓≅⇓′ (λ' a t)          = returnP P.refl
  E⇓≅⇓′ (μ a t)           = later (♯ E⇓≅⇓′ (t [/tmTm μ a t ]))
  E⇓≅⇓′ (t [ a ])         =
    t [ a ] E.⇓           ≅⟨ complete (E.[]-comp t a) ⟩
    (t E.⇓) E.[ a ]⇓      ≅⟨ (E⇓≅⇓′ t >>=P λ v → []-E⇓≅⇓′ v a) ⟩
    (t ⇓) [ a ]⇓′         ≅⟨ sym (complete ((t ⇓) [ a ]⇓≅)) ⟩
    t [ a ] ⇓             ∎
  E⇓≅⇓′ (s · t)           =
    s · t E.⇓             ≅⟨ complete (E.·-comp s t) ⟩
    (s E.⇓) E.·⇓ (t E.⇓)  ≅⟨ (E⇓≅⇓′ s >>=P λ f → E⇓≅⇓′ t >>=P λ v →
                              ·-E⇓≅⇓′ f v) ⟩
    (s ⇓) ·⇓′ (t ⇓)       ≅⟨ sym (complete ((s ⇓) ·⇓≅ (t ⇓))) ⟩
    s · t ⇓               ∎
  E⇓≅⇓′ (fold a t)        =
    fold a t E.⇓          ≅⟨ complete (E.fold-comp a t) ⟩
    E.fold⇓ a (t E.⇓)     ≅⟨ (E⇓≅⇓′ t >>=P λ v → return (fold a v) ∎) ⟩
    fold⇓′ a (t ⇓)        ≅⟨ sym (complete (fold⇓≅ a (t ⇓))) ⟩
    fold a t ⇓            ∎
  E⇓≅⇓′ (unfold a t)      =
    unfold a t E.⇓        ≅⟨ complete (E.unfold-comp a t) ⟩
    E.unfold⇓ a (t E.⇓)   ≅⟨ (E⇓≅⇓′ t >>=P λ v → unfold-E⇓≅⇓′ a v) ⟩
    unfold⇓′ a (t ⇓)      ≅⟨ sym (complete (unfold⇓≅ a (t ⇓))) ⟩
    unfold a t ⇓          ∎

-- The two big-step semantics are strongly bisimliar.
E⇓≅⇓ : ∀ {m n} (t : Term m n) → t E.⇓ ≅ t ⇓
E⇓≅⇓ t = sound (E⇓≅⇓′ t)

max_stars_repo_name: sstucki/system-f-agda

max_issues_repo_name: sstucki/system-f-agda

max_forks_repo_name: sstucki/system-f-agda


text:
module Agda.Builtin.Int where

open import Agda.Builtin.Nat
open import Agda.Builtin.String

infix 8 pos  -- Standard library uses this as +_

data Int : Set where
  pos    : (n : Nat) → Int
  negsuc : (n : Nat) → Int

{-# BUILTIN INTEGER       Int    #-}
{-# BUILTIN INTEGERPOS    pos    #-}
{-# BUILTIN INTEGERNEGSUC negsuc #-}

primitive primShowInteger : Int → String


text:
module Stack where

open import Prelude public

-- Stacks, or snoc-lists.

data Stack (X : Set) : Set where
  ∅   : Stack X
  _,_ : Stack X → X → Stack X

-- Stack membership, or de Bruijn indices.

module _ {X : Set} where
  infix 3 _∈_
  data _∈_ (A : X) : Stack X → Set where
    top : ∀ {Γ}   → A ∈ Γ , A
    pop : ∀ {B Γ} → A ∈ Γ → A ∈ Γ , B

  i₀ : ∀ {A Γ} → A ∈ Γ , A
  i₀ = top

  i₁ : ∀ {A B Γ} → A ∈ Γ , A , B
  i₁ = pop i₀

  i₂ : ∀ {A B C Γ} → A ∈ Γ , A , B , C
  i₂ = pop i₁

-- Stack inclusion, or order-preserving embeddings.

module _ {X : Set} where
  infix 3 _⊆_
  data _⊆_ : Stack X → Stack X → Set where
    done : ∅ ⊆ ∅
    skip : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊆ Γ′ , A
    keep : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ , A ⊆ Γ′ , A

  bot⊆ : ∀ {Γ} → ∅ ⊆ Γ
  bot⊆ {∅}     = done
  bot⊆ {Γ , A} = skip bot⊆

  refl⊆ : ∀ {Γ} → Γ ⊆ Γ
  refl⊆ {∅}     = done
  refl⊆ {Γ , A} = keep refl⊆

  trans⊆ : ∀ {Γ Γ′ Γ″} → Γ ⊆ Γ′ → Γ′ ⊆ Γ″ → Γ ⊆ Γ″
  trans⊆ p        done      = p
  trans⊆ p        (skip p′) = skip (trans⊆ p p′)
  trans⊆ (skip p) (keep p′) = skip (trans⊆ p p′)
  trans⊆ (keep p) (keep p′) = keep (trans⊆ p p′)

  weak⊆ : ∀ {A Γ} → Γ ⊆ Γ , A
  weak⊆ = skip refl⊆

  idtrans⊆ : ∀ {Γ Γ′ } → (p : Γ ⊆ Γ′) → trans⊆ refl⊆ p ≡ p
  idtrans⊆ done     = refl
  idtrans⊆ (skip p) = cong skip (idtrans⊆ p)
  idtrans⊆ (keep p) = cong keep (idtrans⊆ p)

  idtrans⊆′ : ∀ {Γ Γ′} → (p : Γ ⊆ Γ′) → trans⊆ p refl⊆ ≡ p
  idtrans⊆′ done     = refl
  idtrans⊆′ (skip p) = cong skip (idtrans⊆′ p)
  idtrans⊆′ (keep p) = cong keep (idtrans⊆′ p)

  assoctrans⊆ : ∀ {Γ Γ′ Γ″ Γ‴} → (p : Γ ⊆ Γ′) (p′ : Γ′ ⊆ Γ″) (p″ : Γ″ ⊆ Γ‴) →
                trans⊆ (trans⊆ p p′) p″ ≡ trans⊆ p (trans⊆ p′ p″)
  assoctrans⊆ p        p′        done      = refl
  assoctrans⊆ p        p′        (skip p″) = cong skip (assoctrans⊆ p p′ p″)
  assoctrans⊆ p        (skip p′) (keep p″) = cong skip (assoctrans⊆ p p′ p″)
  assoctrans⊆ (skip p) (keep p′) (keep p″) = cong skip (assoctrans⊆ p p′ p″)
  assoctrans⊆ (keep p) (keep p′) (keep p″) = cong keep (assoctrans⊆ p p′ p″)

-- Monotonicity of stack membership with respect to stack inclusion.

module _ {X : Set} where
  mono∈ : ∀ {A : X} {Γ Γ′} → Γ ⊆ Γ′ → A ∈ Γ → A ∈ Γ′
  mono∈ done     ()
  mono∈ (skip p) i       = pop (mono∈ p i)
  mono∈ (keep p) top     = top
  mono∈ (keep p) (pop i) = pop (mono∈ p i)

  idmono∈ : ∀ {A : X} {Γ} → (i : A ∈ Γ) → mono∈ refl⊆ i ≡ i
  idmono∈ top     = refl
  idmono∈ (pop i) = cong pop (idmono∈ i)

-- Stack thinning.

module _ {X : Set} where
  _∖_ : ∀ {A} → (Γ : Stack X) → A ∈ Γ → Stack X
  ∅       ∖ ()
  (Γ , A) ∖ top   = Γ
  (Γ , B) ∖ pop i = Γ ∖ i , B

  thin⊆ : ∀ {A Γ} → (i : A ∈ Γ) → Γ ∖ i ⊆ Γ
  thin⊆ top     = weak⊆
  thin⊆ (pop i) = keep (thin⊆ i)

-- Decidable equality of stack membership.

module _ {X : Set} where
  data _=∈_ {A} {Γ : Stack X} (i : A ∈ Γ) : ∀ {B} → B ∈ Γ → Set where
    same : i =∈ i
    diff : ∀ {B} → (j : B ∈ Γ ∖ i) → i =∈ mono∈ (thin⊆ i) j

  _≟∈_ : ∀ {A B Γ} → (i : A ∈ Γ) (j : B ∈ Γ) → i =∈ j
  top   ≟∈ top    = same
  top   ≟∈ pop j  rewrite sym (idmono∈ j) = diff j
  pop i ≟∈ top    = diff top
  pop i ≟∈ pop j  with i ≟∈ j
  pop i ≟∈ pop .i | same   = same
  pop i ≟∈ pop ._ | diff j = diff (pop j)

max_stars_repo_name: mietek/nbe-correctness

max_issues_repo_name: mietek/nbe-correctness

max_forks_repo_name: mietek/nbe-correctness


text:
module examplesPaperJFP.loadAllOOAgdaPart2 where

-- This is a continuation of the file loadAllOOAgdaPart1
-- giving the code from the ooAgda paper
-- This file was split into two because of a builtin IO which
-- makes loading files from part1 and part2 incompatible.

-- Note that some files which are directly in the libary can be found
-- in loadAllOOAgdaFilesAsInLibrary

-- Sect 1 - 7 are in loadAllOOAgdaPart1.agda

-- 8. State-Dependent Objects and IO
-- 8.1 State-Dependent Interfaces

import examplesPaperJFP.StatefulObject

-- 8.2 State-Dependent Objects
-- 8.2.1. Example of Use of Safe Stack

import examplesPaperJFP.safeFibStackMachineObjectOriented

-- 8.3 Reasoning About Stateful Objects

import examplesPaperJFP.StackBisim

-- 8.3.1. Bisimilarity
-- 8.3.2. Verifying stack laws}
-- 8.3.3. Bisimilarity of different stack implementations

-- 8.4. State-Dependent IO

import examplesPaperJFP.StateDependentIO

-- 9. A Drawing Program in Agda

-- code as in paper adapted to new Agda
open import examplesPaperJFP.IOGraphicsLib
-- code as in library see loadAllOOAgdaFilesAsInLibrary.agda
-- open import SizedIO.IOGraphicsLib
open import examplesPaperJFP.ExampleDrawingProgram

-- 10. A Graphical User Interface using an Object
-- 10.1. wxHaskell
-- 10.2. A Library for Object-Based GUIs in Agda

open import examplesPaperJFP.VariableList
open import examplesPaperJFP.WxGraphicsLib
open import examplesPaperJFP.VariableListForDispatchOnly

-- 10.3 Example: A GUI controlling a Space Ship in Agda

open import examplesPaperJFP.SpaceShipSimpleVar
open import examplesPaperJFP.SpaceShipCell
open import examplesPaperJFP.SpaceShipAdvanced

-- 11. Related Work

open import examplesPaperJFP.agdaCodeBrady

-- 12. Conclusion
-- Bibliography

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
-- {-# OPTIONS -v tc.meta:20 #-}
-- Andreas, 2011-04-21
module PruneLHS where

data _≡_ {A : Set}(a : A) : A -> Set where
  refl : a ≡ a

data Bool : Set where true false : Bool

test : let X : Bool -> Bool -> Bool -> Bool
           X = _
       in (C : Set) ->
          (({x y : Bool} -> X x y x ≡ x) ->
           ({x y : Bool} -> X x x y ≡ x) -> C) -> C
test C k = k refl refl
-- by the first equation, X cannot depend its second argument
-- by the second equation, X cannot depend on its third argument


text:
{-

This file contains a diagonalization procedure simpler than Smith normalization.
For any matrix M, it provides two invertible matrices P, Q, one diagonal matrix D and an equality M = P·D·Q.
The only difference from Smith is, the numbers in D are allowed to be arbitrary, instead of being consecutively divisible.
But it is enough to establish important properties of finitely presented abelian groups.
Also, it can be computed much more efficiently (than Smith, only).

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.IntegerMatrix.Diagonalization where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat
  hiding   (_·_)
  renaming (_+_ to _+ℕ_ ; +-assoc to +Assocℕ)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Nat.Divisibility
  using    (m∣n→m≤n)
  renaming (∣-trans to ∣ℕ-trans ; ∣-refl to ∣-reflℕ)
open import Cubical.Data.Int
  hiding   (_+_ ; _·_ ; _-_ ; -_ ; addEq)
open import Cubical.Data.Int.Divisibility
open import Cubical.Data.FinData

open import Cubical.Data.Empty as Empty
open import Cubical.Data.Unit  as Unit
open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Data.List

open import Cubical.Algebra.Matrix
open import Cubical.Algebra.Matrix.CommRingCoefficient
open import Cubical.Algebra.Matrix.Elementaries
open import Cubical.Algebra.IntegerMatrix.Base
open import Cubical.Algebra.IntegerMatrix.Elementaries

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Instances.Int
  renaming (ℤ to ℤRing)

open import Cubical.Relation.Nullary
open import Cubical.Induction.WellFounded

private
  variable
    m n k : ℕ

open CommRingStr      (ℤRing .snd)

open Coefficient ℤRing
open Sim

open ElemTransformation ℤRing
open ElemTransformationℤ
open SwapPivot
open RowsImproved
open ColsImproved

-- Sequence of non-zero integers

isNonZero : List ℤ → Type
isNonZero [] = Unit
isNonZero (x ∷ xs) = (¬ x ≡ 0) × isNonZero xs

isPropIsNonZero : (xs : List ℤ) → isProp (isNonZero xs)
isPropIsNonZero [] = isPropUnit
isPropIsNonZero (x ∷ xs) = isProp× (isPropΠ (λ _ → isProp⊥)) (isPropIsNonZero xs)

NonZeroList : Type
NonZeroList = Σ[ xs ∈ List ℤ ] isNonZero xs

cons : (n : ℤ)(xs : NonZeroList) → ¬ n ≡ 0 → NonZeroList
cons n (xs , _) _ .fst = n ∷ xs
cons n ([] , _) p .snd = p , tt
cons n (x ∷ xs , q) p .snd = p , q

-- Smith normal matrix

_+length_ : NonZeroList → ℕ → ℕ
xs +length n = length (xs .fst) +ℕ n

diagMat : (xs : List ℤ)(m n : ℕ) → Mat (length xs +ℕ m) (length xs +ℕ n)
diagMat [] _ _ = 𝟘
diagMat (x ∷ xs) _ _ = x ⊕ diagMat xs _ _

diagMat⊕ :
    (a : ℤ)(xs : NonZeroList){m n : ℕ}
  → (p : ¬ a ≡ 0)
  → a ⊕ diagMat (xs .fst) m n ≡ diagMat (cons a xs p .fst) m n
diagMat⊕ _ _ _ = refl

-- Diagonal matrix with non-zero diagonal elements
-- Notice that we allow non-square matrices.

record isDiagonal (M : Mat m n) : Type where
  field
    divs : NonZeroList
    rowNull : ℕ
    colNull : ℕ

    rowEq : divs +length rowNull ≡ m
    colEq : divs +length colNull ≡ n
    matEq : PathP (λ t → Mat (rowEq t) (colEq t)) (diagMat (divs .fst) rowNull colNull) M

open isDiagonal

row col : {M : Mat m n} → isDiagonal M → ℕ
row isNorm = isNorm .divs +length isNorm .rowNull
col isNorm = isNorm .divs +length isNorm .colNull

isDiagonal𝟘 : isDiagonal (𝟘 {m = m} {n = n})
isDiagonal𝟘 .divs = [] , tt
isDiagonal𝟘 {m = m} .rowNull = m
isDiagonal𝟘 {n = n} .colNull = n
isDiagonal𝟘 .rowEq = refl
isDiagonal𝟘 .colEq = refl
isDiagonal𝟘 .matEq = refl

isDiagonalEmpty : (M : Mat 0 n) → isDiagonal M
isDiagonalEmpty _ .divs = [] , tt
isDiagonalEmpty _ .rowNull = 0
isDiagonalEmpty {n = n} _ .colNull = n
isDiagonalEmpty _ .rowEq = refl
isDiagonalEmpty _ .colEq = refl
isDiagonalEmpty _ .matEq = isContr→isProp isContrEmpty _ _

isDiagonalEmptyᵗ : (M : Mat m 0) → isDiagonal M
isDiagonalEmptyᵗ _ .divs = [] , tt
isDiagonalEmptyᵗ {m = m} _ .rowNull = m
isDiagonalEmptyᵗ _ .colNull = 0
isDiagonalEmptyᵗ _ .rowEq = refl
isDiagonalEmptyᵗ _ .colEq = refl
isDiagonalEmptyᵗ _ .matEq = isContr→isProp isContrEmptyᵗ _ _

-- Induction step towards diagonalization

data DivStatus (a : ℤ)(M : Mat (suc m) (suc n)) : Type where
  badCol  : (i : Fin m)(p : ¬ a ∣ M (suc i) zero) → DivStatus a M
  badRow  : (j : Fin n)(p : ¬ a ∣ M zero (suc j)) → DivStatus a M
  allDone : ((i : Fin m) → a ∣ M (suc i) zero)
          → ((j : Fin n) → a ∣ M zero (suc j)) → DivStatus a M

divStatus : (a : ℤ)(M : Mat (suc m) (suc n)) → DivStatus a M
divStatus a M =
  let  col? = ∀Dec (λ i → a ∣ M (suc i) zero) (λ _ → dec∣ _ _)
       row? = ∀Dec (λ j → a ∣ M zero (suc j)) (λ _ → dec∣ _ _) in
  case col?
  return (λ _ → DivStatus a M) of λ
  { (inr p) → badCol (p .fst) (p .snd)
  ; (inl p) →
      case row?
      return (λ _ → DivStatus a M) of λ
      { (inr q) → badRow (q .fst) (q .snd)
      ; (inl q) → allDone p q }}

record DiagStep (M : Mat (suc m) (suc n)) : Type where
  field
    sim : Sim M

    firstColClean : (i : Fin m) → sim .result (suc i) zero ≡ 0
    firstRowClean : (j : Fin n) → sim .result zero (suc j) ≡ 0

    nonZero : ¬ sim .result zero zero ≡ 0

open DiagStep

simDiagStep : {M : Mat (suc m) (suc n)}(sim : Sim M) → DiagStep (sim .result) → DiagStep M
simDiagStep simM diag .sim = compSim simM (diag .sim)
simDiagStep _    diag .firstColClean = diag .firstColClean
simDiagStep _    diag .firstRowClean = diag .firstRowClean
simDiagStep _    diag .nonZero = diag .nonZero

private
  diagStep-helper :
      (M : Mat (suc m) (suc n))
    → (p : ¬ M zero zero ≡ 0)(h : Norm (M zero zero))
    → (div? : DivStatus (M zero zero) M)
    → DiagStep M
  diagStep-helper M p (acc ind) (badCol i q) =
    let improved = improveRows M p
        normIneq =
          ind _ (stDivIneq p q (improved .div zero) (improved .div (suc i)))
    in  simDiagStep (improved .sim)
                    (diagStep-helper _ (improved .nonZero) normIneq (divStatus _ _))
  diagStep-helper M p (acc ind) (badRow j q) =
    let improved = improveCols M p
        normIneq =
          ind _ (stDivIneq p q (improved .div zero) (improved .div (suc j)))
    in  simDiagStep (improved .sim)
                    (diagStep-helper _ (improved .nonZero) normIneq (divStatus _ _))
  diagStep-helper M p (acc ind) (allDone div₁ div₂) =
    let improveColM = improveCols M p
        invCol = bézoutRows-inv _ p div₂
        divCol = (λ i → transport (λ t → invCol t zero ∣ invCol t (suc i)) (div₁ i))
        improveRowM = improveRows (improveColM .sim .result) (improveColM .nonZero)
        invCol = bézoutRows-inv _ (improveColM .nonZero) divCol
    in  record
        { sim = compSim (improveColM .sim) (improveRowM .sim)
        ; firstColClean = improveRowM .vanish
        ; firstRowClean = (λ j → (λ t → invCol (~ t) (suc j)) ∙ improveColM .vanish j)
        ; nonZero = improveRowM .nonZero }

  diagStep-getStart : (M : Mat (suc m) (suc n)) → NonZeroOrNot M → DiagStep M ⊎ (M ≡ 𝟘)
  diagStep-getStart _ (allZero p) = inr p
  diagStep-getStart M (hereIs i j p) =
    let swapM = swapPivot i j M
        swapNonZero = (λ r → p (swapM .swapEq ∙ r))
        diagM = diagStep-helper _ swapNonZero (<-wellfounded _) (divStatus _ _)
    in  inl (simDiagStep (swapM .sim) diagM)

diagStep : (M : Mat (suc m) (suc n)) → DiagStep M ⊎ (M ≡ 𝟘)
diagStep _ = diagStep-getStart _ (findNonZero _)

-- The diagonalization

record Diag (M : Mat m n) : Type where
  field
    sim : Sim M
    isdiag : isDiagonal (sim .result)

open Diag

simDiag : {M : Mat m n}(sim : Sim M) → Diag (sim .result) → Diag M
simDiag simM diag .sim = compSim simM (diag .sim)
simDiag _ diag .isdiag = diag .isdiag

diag𝟘 : Diag (𝟘 {m = m} {n = n})
diag𝟘 .sim    = idSim _
diag𝟘 .isdiag = isDiagonal𝟘

diagEmpty : (M : Mat 0 n) → Diag M
diagEmpty _ .sim    = idSim _
diagEmpty M .isdiag = isDiagonalEmpty M

diagEmptyᵗ : (M : Mat m 0) → Diag M
diagEmptyᵗ _ .sim    = idSim _
diagEmptyᵗ M .isdiag = isDiagonalEmptyᵗ M

decompDiagStep :
    (M : Mat (suc m) (suc n))(step : DiagStep M)
  → step .sim .result ≡ step .sim .result zero zero ⊕ sucMat (step .sim .result)
decompDiagStep M step t zero zero = step .sim .result zero zero
decompDiagStep M step t zero (suc j) = step .firstRowClean j t
decompDiagStep M step t (suc i) zero = step .firstColClean i t
decompDiagStep M step t (suc i) (suc j) = step .sim .result (suc i) (suc j)

consIsDiagonal :
    (a : ℤ)(M : Mat m n)
  → (p : ¬ a ≡ 0)
  → isDiagonal M → isDiagonal (a ⊕ M)
consIsDiagonal a _ p diag .divs = cons a (diag .divs) p
consIsDiagonal _ _ _ diag .rowNull = diag .rowNull
consIsDiagonal _ _ _ diag .colNull = diag .colNull
consIsDiagonal _ _ _ diag .rowEq = (λ t → suc (diag .rowEq t))
consIsDiagonal _ _ _ diag .colEq = (λ t → suc (diag .colEq t))
consIsDiagonal a _ _ diag .matEq = (λ t → a ⊕ diag .matEq t)

diagReduction :
    (a : ℤ)(M : Mat m n)
  → (p : ¬ a ≡ 0)
  → Diag M → Diag (a ⊕ M)
diagReduction a _ _ diag .sim = ⊕Sim a (diag .sim)
diagReduction a _ p diag .isdiag = consIsDiagonal a _ p (diag .isdiag)

-- The Existence of Diagonalization

diagonalize : (M : Mat m n) → Diag M
diagonalize {m = 0} = diagEmpty
diagonalize {m = suc m} {n = 0} = diagEmptyᵗ
diagonalize {m = suc m} {n = suc n} M = helper (diagStep _)
  where
  helper : DiagStep M ⊎ (M ≡ 𝟘) → Diag M
  helper (inr p) = subst Diag (sym p) diag𝟘
  helper (inl stepM) =
    let sucM = sucMat (stepM .sim .result)
        diagM = diagReduction _ _ (stepM .nonZero) (diagonalize sucM)
    in  simDiag (compSim (stepM .sim) (≡Sim (decompDiagStep _ stepM))) diagM

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module constants where

open import lib

cedille-extension : string
cedille-extension = "ced"

self-name : string
self-name = "self"

pattern ignored-var = "_"

pattern meta-var-pfx = '?'
pattern qual-local-chr = '@'
pattern qual-global-chr = '.'

meta-var-pfx-str = 𝕃char-to-string [ meta-var-pfx ]
qual-local-str = 𝕃char-to-string [ qual-local-chr ]
qual-global-str = 𝕃char-to-string [ qual-global-chr ]

options-file-name : string
options-file-name = "options"

global-error-string : string → string
global-error-string msg = "{\"error\":\"" ^ msg ^ "\"" ^ "}"

dot-cedille-directory : string → string
dot-cedille-directory dir = combineFileNames dir ".cedille"

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
open import Agda.Builtin.Char
open import Agda.Builtin.String
open import Agda.Builtin.Maybe
open import Agda.Builtin.Sigma
open import Common.IO

printTail : String → IO _
printTail str with primStringUncons str
... | just (_ , tl) = putStr tl
... | nothing       = putStr ""

main : _
main = printTail "/test/Compiler/simple/uncons.agda"

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness #-}

module Agda.Builtin.Char where

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

postulate Char : Set
{-# BUILTIN CHAR Char #-}

primitive
  primIsLower primIsDigit primIsAlpha primIsSpace primIsAscii
    primIsLatin1 primIsPrint primIsHexDigit : Char → Bool
  primToUpper primToLower : Char → Char
  primCharToNat : Char → Nat
  primNatToChar : Nat → Char
  primCharEquality : Char → Char → Bool
  primCharToNatInjective : ∀ a b → primCharToNat a ≡ primCharToNat b → a ≡ b

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
open import Oscar.Prelude

module Oscar.Class.Amgu where

record Amgu {𝔵} {X : Ø 𝔵} {𝔱} (T : X → Ø 𝔱) {𝔞} (A : X → Ø 𝔞) {𝔪} (M : Ø 𝔞 → Ø 𝔪) : Ø 𝔵 ∙̂ 𝔱 ∙̂ 𝔞 ∙̂ 𝔪 where
  field amgu : ∀ {x} → T x → T x → A x → M (A x)

open Amgu ⦃ … ⦄ public


text:
module FOLsequent where

open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import Data.String using (String)
open import Data.Sum
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≢_; refl; sym; cong; subst)
open import Relation.Nullary
open import Data.List.Base as List using (List; []; _∷_; [_]; _++_)
open import Data.List.Any as LAny
open LAny.Membership-≡

data Term : Set where
  $ : ℕ → Term
  Fun : String → List Term → Term

Const : String -> Term
Const n = Fun n []

data Formula : Set where
  _⟨_⟩ : String → List Term → Formula
  _∧_ : Formula → Formula → Formula
  _∨_ : Formula → Formula → Formula
  _⟶_ : Formula → Formula → Formula
  ~_ : Formula → Formula
  All : (Term → Formula) → Formula
  Ex : (Term → Formula) → Formula

-- data Structure : Set where
--   ∣_∣ : Formula → Structure
--   _,,_ : Structure → Structure → Structure
--   Ø : Structure

Structure = List Formula

mutual
  FVt : Term → List ℕ
  FVt ($ x) = [ x ]
  FVt (Fun _ args) = FVlst args

  FVlst : List Term -> List ℕ
  FVlst [] = []
  FVlst (x ∷ xs) = (FVt x) ++ (FVlst xs)

  FVf : Formula → List ℕ
  FVf (_ ⟨ lst ⟩) = FVlst lst
  FVf (f ∧ f₁) = FVf f ++ FVf f₁
  FVf (f ∨ f₁) = FVf f ++ FVf f₁
  FVf (f ⟶ f₁) = FVf f ++ FVf f₁
  FVf (~ f) = FVf f
  FVf (All x) = FVf (x (Const ""))
  FVf (Ex x) = FVf (x (Const ""))

FV : Structure → List ℕ
FV [] = []
FV (f ∷ l) = FVf f ++ FV l

_#_ : ℕ -> List ℕ -> Set
x # xs = x ∉ xs

∪ : List ℕ -> ℕ
∪ [] = 0
∪ (x ∷ xs) = x ⊔ (∪ xs)

∃# : List ℕ -> ℕ
∃# xs = suc (∪ xs)

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

ℕ-meet-dist : ∀ {x y z : ℕ} -> (x ≤ y) ⊎ (x ≤ z) -> x ≤ y ⊔ z
ℕ-meet-dist {zero} x≤y⊎x≤z = z≤n
ℕ-meet-dist {suc x} {zero} {zero} (inj₁ ())
ℕ-meet-dist {suc x} {zero} {zero} (inj₂ ())
ℕ-meet-dist {suc x} {zero} {suc z} (inj₁ ())
ℕ-meet-dist {suc x} {zero} {suc z} (inj₂ sx≤sz) = sx≤sz
ℕ-meet-dist {suc x} {suc y} {zero} (inj₁ sx≤sy) = sx≤sy
ℕ-meet-dist {suc x} {suc y} {zero} (inj₂ ())
ℕ-meet-dist {suc x} {suc y} {suc z} (inj₁ (s≤s x≤y)) = s≤s (ℕ-meet-dist (inj₁ x≤y))
ℕ-meet-dist {suc x} {suc y} {suc z} (inj₂ (s≤s y≤z)) =
  s≤s (ℕ-meet-dist {_} {y} {z} (inj₂ y≤z))
------------------------------------------------------------------------------------

≤-refl : ∀ {x : ℕ} -> x ≤ x
≤-refl {zero} = z≤n
≤-refl {suc x} = s≤s ≤-refl
------------------------------------------------------------------------------------

∈-cons : ∀ {L} {x y : ℕ} -> x ∈ (y ∷ L) -> ¬(x ≡ y) -> x ∈ L
∈-cons {[]} (here refl) ¬x≡y = ⊥-elim (¬x≡y refl)
∈-cons {[]} (there ()) ¬x≡y
∈-cons {y ∷ L} {x} (here refl) ¬x≡y = ⊥-elim (¬x≡y refl)
∈-cons {y ∷ L} {x} (there x∈L) ¬x≡y = x∈L
------------------------------------------------------------------------------------

∃#-lemma' : ∀ x L -> x ∈ L -> x ≤ ∪ L
∃#-lemma' x [] ()
∃#-lemma' x (y ∷ L) x∈y∷L with x ≟ y
∃#-lemma' x (.x ∷ L) x∈y∷L | yes refl = ℕ-meet-dist {x} {x} (inj₁ ≤-refl)
∃#-lemma' x (y ∷ L) x∈y∷L | no ¬x≡y =
  ℕ-meet-dist {x} {y} (inj₂ (∃#-lemma' x L (∈-cons x∈y∷L ¬x≡y)))
------------------------------------------------------------------------------------

∃#-lemma'' : ∀ x L -> x ∈ L -> ¬ (x ≡ ∃# L)
∃#-lemma'' .(suc (∪ L)) L x∈L refl =
  1+n≰n {∪ L} (∃#-lemma' (suc (∪ L)) L x∈L)
------------------------------------------------------------------------------------

∃#-lemma : ∀ L -> ∃# L ∉ L
∃#-lemma L ∃#L∈L = ∃#-lemma'' (∃# L) L ∃#L∈L refl

data _⊢_ : Structure → Structure → Set where
  I : ∀ {A} → [ A ] ⊢ [ A ]
  Cut : ∀ A {Γ Σ Δ Π} →
    Γ ⊢ (Δ ++ [ A ]) → ([ A ] ++ Σ) ⊢ Π →
    ------------------------------------
            (Γ ++ Σ) ⊢ (Δ ++ Π)
  ∧L₁ : ∀ {Γ Δ A B} → (Γ ++ [ A ]) ⊢ Δ → (Γ ++ [ A ∧ B ]) ⊢ Δ
  ∧L₂ : ∀ {Γ Δ A B} → (Γ ++ [ B ]) ⊢ Δ → (Γ ++ [ A ∧ B ]) ⊢ Δ
  ∧R : ∀ {Γ Σ Δ Π A B} →
    Γ ⊢ ([ A ] ++ Δ) → Σ ⊢ ([ B ] ++ Π) →
    -----------------------------------
    (Γ ++ Σ) ⊢ ([ A ∧ B ] ++ Δ ++ Π)
  ∨R₁ : ∀ {Γ Δ A B} → Γ ⊢ ([ A ] ++ Δ) → Γ ⊢ ([ A ∨ B ] ++ Δ)
  ∨R₂ : ∀ {Γ Δ A B} → Γ ⊢ ([ B ] ++ Δ) → Γ ⊢ ([ A ∨ B ] ++ Δ)
  ∨L :  ∀ {Γ Σ Δ Π A B} →
    (Γ ++ [ A ]) ⊢ Δ → (Σ ++ [ B ]) ⊢ Π →
    -----------------------------------
    (Γ ++ Σ ++ [ A ∨ B ]) ⊢ (Δ ++ Π)
  ⟶L : ∀ {Γ Σ Δ Π A B} →
    Γ ⊢ ([ A ] ++ Δ) → (Σ ++ [ B ]) ⊢ Π →
    ------------------------------------
    (Γ ++ Σ ++ [ A ⟶ B ]) ⊢ (Δ ++ Π)
  ⟶R : ∀ {Γ Δ A B} → (Γ ++ [ A ]) ⊢ ([ B ] ++ Δ) → Γ ⊢ ([ A ⟶ B ] ++ Δ)
  ~L : ∀ {Γ Δ A} → Γ ⊢ ([ A ] ++ Δ) → (Γ ++ [ ~ A ]) ⊢ Δ
  ~R : ∀ {Γ Δ A} → (Γ ++ [ A ]) ⊢ Δ → Γ ⊢ ([ ~ A ] ++ Δ)
  AllL : ∀ {Γ Δ A t} → (Γ ++ [ A t ]) ⊢ Δ → (Γ ++ [ All A ]) ⊢ Δ
  AllR : ∀ {Γ Δ A y} →
    Γ ⊢ ([ A ($ y) ] ++ Δ) → (y-fresh : y # FV (Γ ++ Δ)) →
    ----------------------
    Γ ⊢ ([ All A ] ++ Δ)
  ExL : ∀ {Γ Δ A y} →
    (Γ ++ [ A ($ y) ]) ⊢ Δ → (y-fresh : y # FV (Γ ++ Δ)) →
    ----------------------
    (Γ ++ [ Ex A ]) ⊢ Δ
  ExR : ∀ {Γ Δ A t} → Γ ⊢ ([ A t ] ++ Δ) → Γ ⊢ ([ Ex A ] ++ Δ)
  WL : ∀ {Γ Δ A} → Γ ⊢ Δ → (Γ ++ [ A ]) ⊢ Δ
  WR : ∀ {Γ Δ A} → Γ ⊢ Δ → Γ ⊢ ([ A ] ++ Δ)
  CL : ∀ {Γ Δ A} → (Γ ++ [ A ] ++ [ A ]) ⊢ Δ → (Γ ++ [ A ]) ⊢ Δ
  CR : ∀ {Γ Δ A} → Γ ⊢ ([ A ] ++ [ A ] ++ Δ) → Γ ⊢ ([ A ] ++ Δ)
  PL : ∀ {Γ₁ Γ₂ Δ A B} →
    (Γ₁ ++ [ A ] ++ [ B ] ++ Γ₂) ⊢ Δ →
    ------------------------------------
    (Γ₁ ++ [ B ] ++ [ A ] ++ Γ₂) ⊢ Δ
  PR : ∀ {Γ Δ₁ Δ₂ A B} →
    Γ ⊢ (Δ₁ ++ [ A ] ++ [ B ] ++ Δ₂) →
    ------------------------------------
    Γ ⊢ (Δ₁ ++ [ B ] ++ [ A ] ++ Δ₂)

PL' : ∀ {A B Δ} -> (A ∷ [ B ]) ⊢ Δ → (B ∷ [ A ]) ⊢ Δ
PL' {A} {B} A,B⊢Δ = PL {[]} {[]} {_} {A} {B} A,B⊢Δ

PR' : ∀ {A B Γ} -> Γ ⊢ (A ∷ [ B ]) → Γ ⊢ (B ∷ [ A ])
PR' {A} {B} Γ⊢A,B = PR {_} {[]} {[]} {A} {B} Γ⊢A,B

_>>_ : ∀ {A B : Set} -> (A → B) -> A -> B
A→B >> A = A→B A

open import Data.Product
_>>₂_ : ∀ {A B C : Set} -> (A → B → C) -> A × B -> C
A→B→C >>₂ (A , B) = A→B→C A B

infixr 4 _>>_
infixr 4 _>>₂_

lemma : ∀ {A B C} -> [] ⊢ [ (A ⟶ (B ∨ C)) ⟶ (((B ⟶ (~ A)) ∧ (~ C)) ⟶ (~ A)) ]
lemma {A} {B} {C} = ⟶R >> ⟶R >> PL' >> CR >> ⟶L {[]} {[ (B ⟶ (~ A)) ∧ (~ C) ]} {[ ~ A ]} {[ ~ A ]} >>₂
  (PR' >> ~R >> I) ,
  PL' >> CL {[ B ∨ C ]} {A = (B ⟶ (~ A)) ∧ (~ C)} >> ∧L₂ {(B ∨ C) ∷ [ (B ⟶ (~ A)) ∧ (~ C) ]}
    >> PL {[ B ∨ C ]} {[]} >> ∧L₁ {(B ∨ C) ∷ [ ~ C ]} >> ⟶L {(B ∨ C) ∷ [ ~ C ]} {[]} {[]} >>₂
      (~L {[ B ∨ C ]} >> PR' >> ∨L {[]} {[]} {[ B ]} >>₂ I , I) ,
      I

-- AllR {y = y} (AllL {[]} {t = $ y} I) y-fresh
--   where
--     y = ∃# (FV [ All (λ x → P ⟨ [ x ] ⟩) ])
--     y-fresh = ∃#-lemma (FV [ All (λ x → P ⟨ [ x ] ⟩) ])

AllR# : ∀ {Γ Δ A} → Γ ⊢ ([ A ($ (∃# (FV (Γ ++ Δ)))) ] ++ Δ) → Γ ⊢ ([ All A ] ++ Δ)
AllR# {Γ} {Δ} Γ⊢[y/x]A,Δ = AllR Γ⊢[y/x]A,Δ (∃#-lemma (FV (Γ ++ Δ)))

ExL# : ∀ {Γ Δ A} → (Γ ++ [ A ($ (∃# (FV (Γ ++ Δ)))) ]) ⊢ Δ → (Γ ++ [ Ex A ]) ⊢ Δ
ExL# {Γ} {Δ} Γ,[y/x]A⊢Δ = ExL {Γ} Γ,[y/x]A⊢Δ (∃#-lemma (FV (Γ ++ Δ)))

lemma₁ : ∀ {P} → [ All (λ x → P ⟨ [ x ] ⟩) ] ⊢ [ All (λ y → P ⟨ [ y ] ⟩) ]
lemma₁ {P} = AllR# (AllL {[]} I)

lemma₂ : ∀ {P} →
  [ Ex (λ y → All (λ x → P ⟨ x ∷ [ y ] ⟩)) ] ⊢ [ All (λ x → Ex (λ y → P ⟨ x ∷ [ y ] ⟩)) ]
lemma₂ {P} = AllR# >> ExL# {[]} >> ExR >> AllL {[]} >> I

max_stars_repo_name: goodlyrottenapple/FOLdisplay

max_issues_repo_name: goodlyrottenapple/FOLdisplay

max_forks_repo_name: goodlyrottenapple/FOLdisplay


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

data Maybe {a} (A : Set a) : Set a where
  just : A → Maybe A
  nothing : Maybe A

record RawRoutingAlgebra : Set₁ where
  field
    PathWeight : Set

module _ (A : RawRoutingAlgebra) where

  open RawRoutingAlgebra A

  PathWeight⁺ : Set
  PathWeight⁺ = Maybe (Σ PathWeight λ _ → Nat)

  data P : PathWeight⁺ → Set where
    [_] : ∀ {k} → snd k ≡ 0 → P (just k)

  badness : (r : PathWeight⁺) → P r → Set
  badness r [ refl ] = Nat

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module Data.Boolean where

import Lvl
open import Type

-- Boolean type
data Bool : Type{Lvl.𝟎} where
  𝑇 : Bool -- Represents truth
  𝐹 : Bool -- Represents falsity

{-# BUILTIN BOOL  Bool #-}
{-# BUILTIN TRUE  𝑇 #-}
{-# BUILTIN FALSE 𝐹 #-}

elim : ∀{ℓ}{T : Bool → Type{ℓ}} → T(𝑇) → T(𝐹) → ((b : Bool) → T(b))
elim t _ 𝑇 = t
elim _ f 𝐹 = f

not : Bool → Bool
not 𝑇 = 𝐹
not 𝐹 = 𝑇
{-# COMPILE GHC not = not #-}

-- Control-flow if-else expression
if_then_else_ : ∀{ℓ}{T : Type{ℓ}} → Bool → T → T → T
if b then t else f = elim t f b

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 --erased-cubical --safe #-}

module FarmCanon where

open import Data.List       using (List; _∷_; [])
open import Data.Nat        using (ℕ)
open import Data.Sign       renaming (+ to s+ ; - to s-)
open import Data.Vec        using (Vec; _∷_; []; map)

open import Canon           using (makeCanon2)
open import Instruments     using (pianos)
open import Interval
open import MakeTracks      using (makeTrackList)
open import MidiEvent
open import Note
open import Pitch

subject : List Note
subject =
  tone qtr  (c 5) ∷
  tone qtr  (d 5) ∷
  tone half (e 5) ∷
  tone 8th  (e 5) ∷
  tone 8th  (e 5) ∷
  tone 8th  (d 5) ∷
  tone 8th  (d 5) ∷
  tone half (e 5) ∷
  []

transpositions : Vec Opi 4
transpositions = map (makeSigned s-) (per1 ∷ per5 ∷ per8 ∷ per12 ∷ [])

repeats : ℕ
repeats = 3

delay : Duration
delay = half

canon : Vec (List Note) 4
canon = makeCanon2 subject delay transpositions

tempo : ℕ
tempo = 120

canonTracks : List MidiTrack
canonTracks = makeTrackList pianos tempo canon