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

open import Cubical.Foundations.Prelude

open import Cubical.Data.FinData
open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Nat.Order using (zero-≤)
open import Cubical.Data.Vec.Base
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRingSolver.RawAlgebra renaming (⟨_⟩ to ⟨_⟩ᵣ)
open import Cubical.Algebra.CommRingSolver.AlgebraExpression
open import Cubical.Algebra.CommRingSolver.IntAsRawRing
open import Cubical.Algebra.CommRingSolver.HornerForms
open import Cubical.Algebra.CommRingSolver.EvalHom
open import Cubical.Algebra.CommRingSolver.HornerEval

private
  variable
    ℓ : Level

module EqualityToNormalform (R : CommRing ℓ) where
  νR = CommRing→RawℤAlgebra R
  open CommRingStr (snd R)
  open RingTheory (CommRing→Ring R)
  open Eval ℤAsRawRing νR
  open IteratedHornerOperations νR
  open HomomorphismProperties R

  ℤExpr : (n : ℕ) → Type _
  ℤExpr = Expr ℤAsRawRing (fst R)

  normalize : {n : ℕ} → ℤExpr n → IteratedHornerForms νR n
  normalize {n = n} (K r) = Constant n νR r
  normalize {n = n} (∣ k) = Variable n νR k
  normalize (x +' y) =
    (normalize x) +ₕ (normalize y)
  normalize (x ·' y) =
    (normalize x) ·ₕ (normalize y)
  normalize (-' x) =  -ₕ (normalize x)

  isEqualToNormalform :
       {n : ℕ} (e : ℤExpr n) (xs : Vec (fst R) n)
     → eval (normalize e) xs ≡ ⟦ e ⟧ xs
  isEqualToNormalform (K r) [] = refl
  isEqualToNormalform {n = ℕ.suc n} (K r) (x ∷ xs) =
     eval (Constant (ℕ.suc n) νR r) (x ∷ xs)         ≡⟨ refl ⟩
     eval (0ₕ ·X+ Constant n νR r) (x ∷ xs)           ≡⟨ combineCasesEval R 0ₕ (Constant n νR r) x xs ⟩
     eval 0ₕ (x ∷ xs) · x + eval (Constant n νR r) xs ≡⟨ cong (λ u → u · x + eval (Constant n νR r) xs)
                                                             (Eval0H (x ∷ xs)) ⟩
     0r · x + eval (Constant n νR r) xs               ≡⟨ cong
                                                          (λ u → u + eval (Constant n νR r) xs)
                                                          (0LeftAnnihilates _) ⟩
     0r + eval (Constant n νR r) xs                   ≡⟨ +IdL _ ⟩
     eval (Constant n νR r) xs                        ≡⟨ isEqualToNormalform (K r) xs ⟩
     _ ∎

  isEqualToNormalform (∣ zero) (x ∷ xs) =
    eval (1ₕ ·X+ 0ₕ) (x ∷ xs)           ≡⟨ combineCasesEval R 1ₕ 0ₕ x xs ⟩
    eval 1ₕ (x ∷ xs) · x + eval 0ₕ xs   ≡⟨ cong (λ u → u · x + eval 0ₕ xs)
                                              (Eval1ₕ (x ∷ xs)) ⟩
    1r · x + eval 0ₕ xs                 ≡⟨ cong (λ u → 1r · x + u ) (Eval0H xs) ⟩
    1r · x + 0r                        ≡⟨ +IdR _ ⟩
    1r · x                             ≡⟨ ·IdL _ ⟩
    x ∎
  isEqualToNormalform {n = ℕ.suc n} (∣ (suc k)) (x ∷ xs) =
      eval (0ₕ ·X+ Variable n νR k) (x ∷ xs)           ≡⟨ combineCasesEval R 0ₕ (Variable n νR k) x xs ⟩
      eval 0ₕ (x ∷ xs) · x + eval (Variable n νR k) xs ≡⟨ cong (λ u → u · x + eval (Variable n νR k) xs)
                                                              (Eval0H (x ∷ xs)) ⟩
      0r · x + eval (Variable n νR k) xs              ≡⟨ cong (λ u → u + eval (Variable n νR k) xs)
                                                              (0LeftAnnihilates _) ⟩
      0r + eval (Variable n νR k) xs                  ≡⟨ +IdL _ ⟩
      eval (Variable n νR k) xs                       ≡⟨ isEqualToNormalform (∣ k) xs ⟩
      ⟦ ∣ (suc k) ⟧ (x ∷ xs) ∎

  isEqualToNormalform (-' e) [] =
    eval (-ₕ (normalize e)) []  ≡⟨ -EvalDist (normalize e) [] ⟩
    - eval (normalize e) []    ≡⟨ cong -_ (isEqualToNormalform e [] ) ⟩
    - ⟦ e ⟧ [] ∎
  isEqualToNormalform (-' e) (x ∷ xs) =
    eval (-ₕ (normalize e)) (x ∷ xs) ≡⟨ -EvalDist (normalize e) (x ∷ xs) ⟩
    - eval (normalize e) (x ∷ xs)    ≡⟨ cong -_ (isEqualToNormalform e (x ∷ xs) ) ⟩
    - ⟦ e ⟧ (x ∷ xs) ∎

  isEqualToNormalform (e +' e₁) [] =
        eval (normalize e +ₕ normalize e₁) []
      ≡⟨ +Homeval (normalize e) _ [] ⟩
        eval (normalize e) []
        + eval (normalize e₁) []
      ≡⟨ cong (λ u → u + eval (normalize e₁) [])
              (isEqualToNormalform e []) ⟩
        ⟦ e ⟧ []
        + eval (normalize e₁) []
      ≡⟨ cong (λ u → ⟦ e ⟧ [] + u) (isEqualToNormalform e₁ []) ⟩
        ⟦ e ⟧ [] + ⟦ e₁ ⟧ [] ∎
  isEqualToNormalform (e +' e₁) (x ∷ xs) =
        eval (normalize e +ₕ normalize e₁) (x ∷ xs)
      ≡⟨ +Homeval (normalize e) _ (x ∷ xs) ⟩
        eval (normalize e) (x ∷ xs) + eval (normalize e₁) (x ∷ xs)
      ≡⟨ cong (λ u → u + eval (normalize e₁) (x ∷ xs))
              (isEqualToNormalform e (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs) + eval (normalize e₁) (x ∷ xs)
      ≡⟨ cong (λ u → ⟦ e ⟧ (x ∷ xs) + u) (isEqualToNormalform e₁ (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs) + ⟦ e₁ ⟧ (x ∷ xs) ∎

  isEqualToNormalform (e ·' e₁) [] =
        eval (normalize e ·ₕ normalize e₁) []
      ≡⟨ ·Homeval (normalize e) _ [] ⟩
        eval (normalize e) [] · eval (normalize e₁) []
      ≡⟨ cong (λ u → u · eval (normalize e₁) [])
              (isEqualToNormalform e []) ⟩
        ⟦ e ⟧ [] · eval (normalize e₁) []
      ≡⟨ cong (λ u → ⟦ e ⟧ [] · u) (isEqualToNormalform e₁ []) ⟩
        ⟦ e ⟧ [] · ⟦ e₁ ⟧ [] ∎

  isEqualToNormalform (e ·' e₁) (x ∷ xs) =
        eval (normalize e ·ₕ normalize e₁) (x ∷ xs)
      ≡⟨ ·Homeval (normalize e) _ (x ∷ xs) ⟩
        eval (normalize e) (x ∷ xs) · eval (normalize e₁) (x ∷ xs)
      ≡⟨ cong (λ u → u · eval (normalize e₁) (x ∷ xs))
              (isEqualToNormalform e (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs) · eval (normalize e₁) (x ∷ xs)
      ≡⟨ cong (λ u → ⟦ e ⟧ (x ∷ xs) · u) (isEqualToNormalform e₁ (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs) · ⟦ e₁ ⟧ (x ∷ xs) ∎

  solve :
    {n : ℕ} (e₁ e₂ : ℤExpr n) (xs : Vec (fst R) n)
    (p : eval (normalize e₁) xs ≡ eval (normalize e₂) xs)
    → ⟦ e₁ ⟧ xs ≡ ⟦ e₂ ⟧ xs
  solve e₁ e₂ xs p =
    ⟦ e₁ ⟧ xs                  ≡⟨ sym (isEqualToNormalform e₁ xs) ⟩
    eval (normalize e₁) xs ≡⟨ p ⟩
    eval (normalize e₂) xs ≡⟨ isEqualToNormalform e₂ xs ⟩
    ⟦ e₂ ⟧ xs ∎

ℤExpr : (R : CommRing ℓ) (n : ℕ)
        → _
ℤExpr R n = EqualityToNormalform.ℤExpr R n

solve : (R : CommRing ℓ)
        {n : ℕ} (e₁ e₂ : ℤExpr R n) (xs : Vec (fst R) n)
        (p : eval (EqualityToNormalform.normalize R e₁) xs ≡ eval (EqualityToNormalform.normalize R e₂) xs)
        → _
solve R = EqualityToNormalform.solve R

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

module Categories.Diagram.Pullback {o ℓ e} (C : Category o ℓ e) where

open Category C
open HomReasoning

open import Level
open import Data.Product using (_,_; ∃)
open import Function using (flip; _$_) renaming (_∘_ to _●_)
open import Categories.Morphism C
open import Categories.Object.Product C
open import Categories.Diagram.Equalizer C
open import Categories.Morphism.Reasoning C as Square
  renaming (glue to glue-square) hiding (id-unique)

private
  variable
    A B X Y Z : Obj
    f g h h₁ h₂ i i₁ i₂ j : A ⇒ B

-- Pullback of two arrows with a common codomain
record Pullback (f : X ⇒ Z) (g : Y ⇒ Z) : Set (o ⊔ ℓ ⊔ e) where
  field
    {P} : Obj
    p₁  : P ⇒ X
    p₂  : P ⇒ Y

  field
    commute   : f ∘ p₁ ≈ g ∘ p₂
    universal : ∀ {h₁ : A ⇒ X} {h₂ : A ⇒ Y} → f ∘ h₁ ≈ g ∘ h₂ → A ⇒ P
    unique    : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} →
                  p₁ ∘ i ≈ h₁ → p₂ ∘ i ≈ h₂ →
                  i ≈ universal eq

    p₁∘universal≈h₁  : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} →
                         p₁ ∘ universal eq ≈ h₁
    p₂∘universal≈h₂  : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} →
                         p₂ ∘ universal eq ≈ h₂

  unique′ : (eq eq′ : f ∘ h₁ ≈ g ∘ h₂) → universal eq ≈ universal eq′
  unique′ eq eq′ = unique p₁∘universal≈h₁ p₂∘universal≈h₂

  id-unique : id ≈ universal commute
  id-unique = unique identityʳ identityʳ

  unique-diagram : p₁ ∘ h ≈ p₁ ∘ i →
                   p₂ ∘ h ≈ p₂ ∘ i →
                   h ≈ i
  unique-diagram {h = h} {i = i} eq₁ eq₂ = begin
    h            ≈⟨ unique eq₁ eq₂ ⟩
    universal eq ≈˘⟨ unique refl refl ⟩
    i            ∎
    where eq = extendʳ commute

swap : Pullback f g → Pullback g f
swap p = record
  { p₁              = p₂
  ; p₂              = p₁
  ; commute        = ⟺ commute
  ; universal       = universal ● ⟺
  ; unique          = flip unique
  ; p₁∘universal≈h₁ = p₂∘universal≈h₂
  ; p₂∘universal≈h₂ = p₁∘universal≈h₁
  }
  where open Pullback p

glue : (p : Pullback f g) → Pullback h (Pullback.p₁ p) → Pullback (f ∘ h) g
glue {h = h} p q = record
  { p₁              = q.p₁
  ; p₂              = p.p₂ ∘ q.p₂
  ; commute        = glue-square p.commute q.commute
  ; universal       = λ eq → q.universal (⟺ (p.p₁∘universal≈h₁ {eq = ⟺ assoc ○ eq}))
  ; unique          = λ {_ h₁ h₂ i} eq eq′ →
    q.unique eq (p.unique (begin
      p.p₁ ∘ q.p₂ ∘ i ≈˘⟨ extendʳ q.commute ⟩
      h ∘ q.p₁ ∘ i    ≈⟨ refl⟩∘⟨ eq ⟩
      h ∘ h₁          ∎)
                          (⟺ assoc ○ eq′))
  ; p₁∘universal≈h₁ = q.p₁∘universal≈h₁
  ; p₂∘universal≈h₂ = assoc ○ ∘-resp-≈ʳ q.p₂∘universal≈h₂ ○ p.p₂∘universal≈h₂
  }
  where module p = Pullback p
        module q = Pullback q

unglue : (p : Pullback f g) → Pullback (f ∘ h) g → Pullback h (Pullback.p₁ p)
unglue {f = f} {g = g} {h = h} p q = record
  { p₁              = q.p₁
  ; p₂              = p₂′
  ; commute        = ⟺ p.p₁∘universal≈h₁
  ; universal       = λ {_ h₁ h₂} eq → q.universal $ begin
    (f ∘ h) ∘ h₁      ≈⟨ pullʳ eq ⟩
    f ∘ p.p₁ ∘ h₂     ≈⟨ extendʳ p.commute ⟩
    g ∘ p.p₂ ∘ h₂     ∎
  ; unique          = λ {_ h₁ h₂ i} eq eq′ → q.unique eq $ begin
  q.p₂ ∘ i            ≈⟨ pushˡ (⟺ p.p₂∘universal≈h₂) ⟩
  p.p₂ ∘ p₂′ ∘ i      ≈⟨ refl⟩∘⟨ eq′ ⟩
  p.p₂ ∘ h₂           ∎
  ; p₁∘universal≈h₁ = q.p₁∘universal≈h₁
  ; p₂∘universal≈h₂ = λ {_ _ _ eq} →
    p.unique-diagram ((pullˡ p.p₁∘universal≈h₁) ○ pullʳ q.p₁∘universal≈h₁ ○ eq)
                     (pullˡ p.p₂∘universal≈h₂ ○ q.p₂∘universal≈h₂)
  }
  where module p = Pullback p
        module q = Pullback q
        p₂′ = p.universal (⟺ assoc ○ q.commute) -- used twice above

Product×Equalizer⇒Pullback :
  (p : Product A B) → Equalizer (f ∘ Product.π₁ p) (g ∘ Product.π₂ p) →
  Pullback f g
Product×Equalizer⇒Pullback {f = f} {g = g} p e = record
  { p₁              = π₁ ∘ arr
  ; p₂              = π₂ ∘ arr
  ; commute        = ⟺ assoc ○ equality ○ assoc
  ; universal       = λ {_ h₁ h₂} eq → equalize $ begin
    (f ∘ π₁) ∘ ⟨ h₁ , h₂ ⟩ ≈⟨ pullʳ project₁ ⟩
    f ∘ h₁                ≈⟨ eq ⟩
    g ∘ h₂                ≈˘⟨ pullʳ project₂ ⟩
    (g ∘ π₂) ∘ ⟨ h₁ , h₂ ⟩ ∎
  ; unique          = λ eq eq′ → e.unique (p.unique (⟺ assoc ○ eq) (⟺ assoc ○ eq′))
  ; p₁∘universal≈h₁ = pullʳ (⟺ e.universal) ○ project₁
  ; p₂∘universal≈h₂ = pullʳ (⟺ e.universal) ○ project₂
  }
  where module p = Product p
        module e = Equalizer e
        open p
        open e

Product×Pullback⇒Equalizer : (p : Product A B) → Pullback f g →
  Equalizer (f ∘ Product.π₁ p) (g ∘ Product.π₂ p)
Product×Pullback⇒Equalizer {f = f} {g = g} p pu = record
  { arr       = ⟨ p₁ , p₂ ⟩
  ; equality  = begin
    (f ∘ π₁) ∘ ⟨ p₁ , p₂ ⟩ ≈⟨ pullʳ project₁ ⟩
    f ∘ p₁                 ≈⟨ commute ⟩
    g ∘ p₂                 ≈˘⟨ pullʳ project₂ ⟩
    (g ∘ π₂) ∘ ⟨ p₁ , p₂ ⟩ ∎
  ; equalize  = λ eq → pu.universal (⟺ assoc ○ eq ○ assoc)
  ; universal = λ {_ h} → begin
    h                      ≈˘⟨ p.unique (⟺ p₁∘universal≈h₁) (⟺ p₂∘universal≈h₂) ⟩
    ⟨ p₁ ∘ _ , p₂ ∘ _ ⟩    ≈⟨ p.unique (pullˡ project₁) (pullˡ project₂) ⟩
    ⟨ p₁ , p₂ ⟩ ∘ _        ∎
  ; unique    = λ eq → pu.unique (pushˡ (⟺ project₁) ○ ⟺ (∘-resp-≈ʳ eq))
                                 (pushˡ (⟺ project₂) ○ ⟺ (∘-resp-≈ʳ eq))
  }
  where module p = Product p
        module pu = Pullback pu
        open p
        open pu

module _ (p : Pullback f g) where
  open Pullback p

  Pullback-resp-≈ : h ≈ f → i ≈ g → Pullback h i
  Pullback-resp-≈ eq eq′ = record
    { p₁              = p₁
    ; p₂              = p₂
    ; commute         = ∘-resp-≈ˡ eq ○ commute ○ ⟺ (∘-resp-≈ˡ eq′)
    ; universal       = λ eq″ → universal (∘-resp-≈ˡ (⟺ eq) ○ eq″ ○ ∘-resp-≈ˡ eq′)
    ; unique          = unique
    ; p₁∘universal≈h₁ = p₁∘universal≈h₁
    ; p₂∘universal≈h₂ = p₂∘universal≈h₂
    }

  Pullback-resp-Mono : Mono g → Mono p₁
  Pullback-resp-Mono mg h i eq = unique-diagram eq (mg _ _ eq′)
    where eq′ : g ∘ p₂ ∘ h ≈ g ∘ p₂ ∘ i
          eq′ = begin
            g ∘ p₂ ∘ h ≈⟨ extendʳ (sym commute) ⟩
            f ∘ p₁ ∘ h ≈⟨ refl⟩∘⟨ eq ⟩
            f ∘ p₁ ∘ i ≈⟨ extendʳ commute ⟩
            g ∘ p₂ ∘ i ∎

  Pullback-resp-Iso : Iso g h → ∃ λ i → Iso p₁ i
  Pullback-resp-Iso {h = h} iso = universal eq
                                , record
                                { isoˡ = unique-diagram eq₁ eq₂
                                ; isoʳ = p₁∘universal≈h₁
                                }
    where open Iso iso
          eq = begin
            f ∘ id                 ≈⟨ introˡ refl ⟩
            id ∘ f ∘ id            ≈⟨ pushˡ (⟺ isoʳ) ⟩
            g ∘ h ∘ f ∘ id         ∎
          eq₁ = begin
            p₁ ∘ universal eq ∘ p₁ ≈⟨ cancelˡ p₁∘universal≈h₁ ⟩
            p₁                     ≈˘⟨ identityʳ ⟩
            p₁ ∘ id                ∎
          eq₂ = begin
            p₂ ∘ universal eq ∘ p₁ ≈⟨ extendʳ p₂∘universal≈h₂ ⟩
            h ∘ (f ∘ id) ∘ p₁      ≈⟨ refl ⟩∘⟨ identityʳ ⟩∘⟨ refl ⟩
            h ∘ f ∘ p₁             ≈⟨ refl ⟩∘⟨ commute ⟩
            h ∘ g ∘ p₂             ≈⟨ cancelˡ isoˡ ⟩
            p₂                     ≈˘⟨ identityʳ ⟩
            p₂ ∘ id                ∎

ext: agda

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
-- Environment model of the STLC
module STLC.Model where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive
open import SOAS.Abstract.Monoid
open import SOAS.Coalgebraic.Lift

open import STLC.Signature
open import STLC.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution Λ:Syn
open import SOAS.Metatheory.SecondOrder.Equality Λ:Syn
open import SOAS.Metatheory.FreeMonoid Λ:Syn
open import SOAS.Syntax.Arguments

open import Data.Nat

private
  variable
    α β γ τ : ΛT
    Γ Δ Π : Ctx
    𝔛 : Familyₛ
Λᴳ : Familyₛ
Λᴳ = Λ Ø

-- Interpretation of types and contexts
⟦_⟧ : ΛT → Set
⟦ N ⟧ = ℕ
⟦ α ↣ β ⟧ = ⟦ α ⟧ → ⟦ β ⟧

⟦_⟧ᶜ : Ctx → Set
⟦ Γ ⟧ᶜ = {α : ΛT} → ℐ α Γ → ⟦ α ⟧

_⁺_ : ⟦ α ⟧ → ⟦ Γ ⟧ᶜ → ⟦ α ∙ Γ ⟧ᶜ
_⁺_ x γ new = x
_⁺_ x γ (old v) = γ v
infixr 10 _⁺_

-- Environment model
Env : Familyₛ
Env α Γ = ⟦ Γ ⟧ᶜ → ⟦ α ⟧

ΣEnvᴹ : ΣMon Env
ΣEnvᴹ = record
  { ᵐ = record
    { η = λ v γ → γ v ; μ = λ t σ δ → t (λ v → σ v δ)
    ; lunit = refl ; runit = refl ; assoc = refl }
  ; 𝑎𝑙𝑔 = λ{ (appₒ ⋮ f , a) γ → f γ (a γ)
          ; (lamₒ ⋮ b) γ → λ a → b (a ⁺ γ) }
  ; μ⟨𝑎𝑙𝑔⟩ = λ{ (appₒ ⋮ _) → refl
             ; (lamₒ ⋮ b) → ext² λ δ a → cong b (dext
                (λ { new → refl ; (old y) → refl })) } }

module Env = FΣM Ø ΣEnvᴹ (λ ())

eval : Λ Ø ⇾̣ Env
eval = Env.𝕖𝕩𝕥
evalᶜ : Λ Ø α ∅ → ⟦ α ⟧
evalᶜ t = eval t (λ ())

_ : evalᶜ {N ↣ N ↣ N} (ƛ ƛ x₁) ≡ λ x y → x
_ = refl

open Theory Ø

-- Operational semantics of the STLC
data Value : Λᴳ α Γ → Set where
  lamⱽ  : {b : Λᴳ β (α ∙ Γ)} →
          Value (ƛ b)

data _⟿_ : Λᴳ α Γ → Λᴳ α Γ → Set where
  ζ-$₁  : {f g : Λᴳ (α ↣ β) Γ}{a : Λᴳ α Γ} →
          f ⟿ g → f $ a ⟿ g $ a
  ζ-$₂  : {f : Λᴳ (α ↣ β) Γ}{a b : Λᴳ α Γ} →
          Value f → a ⟿ b → f $ a ⟿ f $ b
  β-ƛ   : {b : Λᴳ β (α ∙ Γ)}{t : Λᴳ α Γ} →
          Value t → ((ƛ b) $ t) ⟿ [ t /] b

infix 2 _⟿_

-- Evaluation preserves the meaning of terms
sound : {t s : Λᴳ α Γ} → t ⟿ s → (γ : ⟦ Γ ⟧ᶜ) →  eval t γ ≡ eval s γ
sound (ζ-$₁ r) γ rewrite sound r γ = refl
sound (ζ-$₂ _ r) γ rewrite sound r γ = refl
sound (β-ƛ {b = b}{t} x) γ rewrite Env.𝕖𝕩𝕥ᵐ⇒.sub-lemma t b =
  cong (eval b) (dext λ{ new → refl ; (old v) → refl })


text:
-- Andreas, 2016-12-12, issue #2046, reported by Nad
-- Parameter refinement broke the size solver.

-- {-# OPTIONS -v tc.size.solve:100 #-}
-- {-# OPTIONS -v tc.constr.cast:100 #-}
-- -- {-# OPTIONS -v tc.sig.param:60 #-}
-- -- {-# OPTIONS -v tc.check.internal:100 #-}
-- -- {-# OPTIONS -v interaction.give:100 #-}

open import Agda.Builtin.Size using (Size; Size<_)

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

record Always {A : Set} (P : A → Set) : Set where
  field
    always : ∀ x → P x

postulate
  A : Set

module M (P : A → Set) where

  record R₁ (i : Size) (x : A) : Set where
    coinductive
    field
      force : {j : Size< i} → R₁ j x

  record R₂ (i : Size) (x : A) : Set where
    inductive
    constructor ⟨_,_⟩
    field
      f₁ : P x
      f₂ : P x → R₁ i x

data P : A → Set where
  c : (y : A) → P y → P y

postulate
  p : (x : A) → P x
  a : (i : Size) → Always (M.R₁ P i)

module _ (Unused : Set) where

  open M P

  rejected : ∀ i z → R₂ i z
  rejected i z =
    ⟨ p z
    , (λ { (c y q) →  Always.always (a _) z   })
    ⟩

-- Should succeed

{-
Solving constraints (DontDefaultToInfty)
i =< _i_31 Unused i z : Size
_i_31 Unused i z =< _i_35 z Unused i q : Size
converting size constraint i =< _i_31 Unused i z : Size
converting size constraint
_i_31 Unused i z =< _i_35 z Unused i q : Size
Solving constraint cluster
[Unused, i, z] i ≤ _i_31 Unused i z
[z, Unused, i, q] _i_31 Unused i z ≤ _i_35 z Unused i q
Size hypotheses
Canonicalized constraints
[z, Unused, i, q] Unused ≤ _i_31 z Unused i
[z, Unused, i, q] _i_31 Unused i z ≤ _i_35 z Unused i q
solution  _i_31 z Unused i  :=  Unused
  xs = [3,2,1]
  u  = Var 2 []
solution  _i_35 z Unused i q  :=  Unused
  xs = [3,2,1,0]
  u  = Var 2 []
-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-

Matrix with coefficients in integers

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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function hiding (const)
open import Cubical.Foundations.Powerset

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)
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.Algebra.Matrix
open import Cubical.Algebra.Matrix.CommRingCoefficient
open import Cubical.Algebra.Ring.BigOps
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 Sum         (CommRing→Ring ℤRing)

-- Using well-foundedness to do induction

Norm : ℤ → Type
Norm n = Acc _<_ (abs n)

-- Divisibility of matrix elements

∣-sum :
    (a : ℤ)(V : FinVec ℤ n)
  → ((i : Fin n) → a ∣ V i)
  → a ∣ ∑ V
∣-sum {n = 0} _ _ _ = ∣-zeroʳ
∣-sum {n = suc n} _ _ p = ∣-+ (p zero) (∣-sum _ _ (p ∘ suc))

∣-left⋆ :
    (a : ℤ)(M : Mat m n)(N : Mat n k)
  → ((i : Fin m)(j : Fin n) → a ∣ M i j)
  →  (i : Fin m)(j : Fin k) → a ∣ (M ⋆ N) i j
∣-left⋆ a M N div i j =
  ∣-sum a (λ l → M i l · N l j) (λ l → ∣-left· (div i l))

∣-right⋆ :
    (a : ℤ)(M : Mat m n)(N : Mat n k)
  → ((i : Fin n)(j : Fin k) → a ∣ N i j)
  →  (i : Fin m)(j : Fin k) → a ∣ (M ⋆ N) i j
∣-right⋆ a M N div i j =
  ∣-sum a (λ l → M i l · N l j) (λ l → ∣-right· {n = M i l} (div l j))

open SimRel
open Sim

sim∣ :
    (a : ℤ)(M : Mat m n)
  → (sim : Sim M)
  → ((i : Fin m)(j : Fin n) → a ∣ M i j)
  →  (i : Fin m)(j : Fin n) → a ∣ sim .result i j
sim∣ a M sim div i j =
  subst (a ∣_) (λ t → sim .simrel .transEq (~ t) i j)
    (∣-left⋆ _ _ (sim .simrel .transMatR)
    (∣-right⋆ _ (sim .simrel .transMatL) _ div) i j)

-- Find a pivot to begin reduction

data PivotOrNot (a : ℤ)(M : Mat (suc m) (suc n)) : Type where
  pivot   : (i : Fin (suc m))(j : Fin (suc n))(p : ¬ a ∣ M i j) → PivotOrNot a M
  noPivot : ((i : Fin (suc m))(j : Fin (suc n)) → a ∣ M i j) → PivotOrNot a M

findPivot : (a : ℤ)(M : Mat (suc m) (suc n)) → PivotOrNot a M
findPivot a M =
  let  pivot? = ∀Dec2 (λ i j → a ∣ M i j) (λ _ _ → dec∣ _ _) in
  case pivot?
  return (λ _ → PivotOrNot a M) of λ
  { (inl p) → noPivot p
  ; (inr p) → pivot  (p .fst) (p .snd .fst) (p . snd .snd) }

-- Find an non-zero element

data NonZeroOrNot (M : Mat (suc m) (suc n)) : Type where
  hereIs  : (i : Fin (suc m))(j : Fin (suc n))(p : ¬ M i j ≡ 0) → NonZeroOrNot M
  allZero : M ≡ 𝟘 → NonZeroOrNot M

findNonZero : (M : Mat (suc m) (suc n)) → NonZeroOrNot M
findNonZero M =
  let  nonZero? = ∀Dec2 (λ i j → M i j ≡ 0) (λ _ _ → discreteℤ _ 0) in
  case nonZero?
  return (λ _ → NonZeroOrNot M) of λ
  { (inl p) → allZero (λ t i j → p i j t)
  ; (inr p) → hereIs  (p .fst) (p .snd .fst) (p . snd .snd) }

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{-# OPTIONS --exact-split #-}

-- The --exact-split flag causes Agda to raise an error whenever
-- a clause in a definition by pattern matching cannot be made to
-- hold definitionally (i.e. as a reduction rule). Specific clauses
-- can be excluded from this check by means of the {-# CATCHALL #-}
-- pragma.

module ExactSplit where

data Bool : Set where
  true false : Bool

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero    + n    = zero
(suc m) + n    = suc (m + n)

eq : ℕ → ℕ → Bool
eq zero    zero    = true
eq (suc m) (suc n) = eq m n
{-# CATCHALL #-}
eq _       _       = false

-- See also fail/ExactSplitMin.agda
min : ℕ → ℕ → ℕ
min zero    y       = zero
{-# CATCHALL #-}
min x       zero    = zero
min (suc x) (suc y) = suc (min x y)

-- See also fail/ExactSplitBerry.agda
maj : Bool → Bool → Bool → Bool
maj true  true  true  = true
{-# CATCHALL #-}
maj x     true  false = x
{-# CATCHALL #-}
maj false y     true  = y
maj true  false z     = z
maj false false false = false

-- See also fail/ExactSplitParity.agda
parity : ℕ → ℕ → Bool
parity zero          zero          = true
parity zero          (suc zero)    = false
parity zero          (suc (suc n)) = parity zero n
parity (suc zero)    zero          = false
parity (suc (suc m)) zero          = parity m zero
{-# CATCHALL #-}
parity (suc m)       (suc n)       = parity m n

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Numeral.Finite.Conversions where

import      Lvl
open import Data using (Empty ; Unit ; <>)
open import Data.Boolean using (Bool ; 𝐹 ; 𝑇)
open import Data.Tuple using (_,_)
open import Logic.Propositional using (_↔_)
open import Numeral.Finite
open import Numeral.Natural
open import Syntax.Number

private variable ℓ : Lvl.Level

empty : 𝕟(0) ↔ Empty{ℓ}
empty = (\()) , (\())

unit : 𝕟(1) ↔ Unit{ℓ}
unit = (\{<> → 0}) , (\{𝟎 → <>})

bool : 𝕟(2) ↔ Bool
bool = (\{𝐹 → 0 ; 𝑇 → 1}) , (\{𝟎 → 𝐹 ; (𝐒(𝟎)) → 𝑇})

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Equivalence

module HoTT.Equivalence.Lift where

open variables

Lift-equiv : Lift {i} A ≃ A
Lift-equiv = iso→eqv λ{.f → lower ; .g → lift ; .η _ → refl ; .ε _ → refl}
  where open Iso

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
module prelude where

open import level public
open import product public
open import product-thms public
open import sum public
open import empty public
open import unit public
open import functions renaming (id to id-set) public
open import eq public
open import list public
open import list-thms public
open import bool public
open import nat public
open import nat-thms public

-- Extensionality will be used when proving equivalences of morphisms.
postulate ext-set : ∀{l1 l2 : level} → extensionality {l1} {l2}
-- These are isomorphisms, but Agda has no way to prove these as
-- equivalences.  They are consistent to adopt as equivalences by
-- univalence:
postulate ∧-unit : ∀{ℓ}{A : Set ℓ} → A ≡ (⊤ {ℓ} ∧ A)
postulate ∧-assoc : ∀{ℓ}{A B C : Set ℓ} →  (A ∧ (B ∧ C)) ≡ ((A ∧ B) ∧ C)
postulate ∧-twist : ∀{ℓ}{A B : Set ℓ} →  (A ∧ B) ≡ (B ∧ A)
-- Provable from the above axioms:
postulate assoc-twist₁ : {A B C D : Set} → ((A × C) × (B × D)) ≡ ((A × B) × (C × D))

-- The following defines a commutative monoid as lists:
_* = 𝕃

postulate *-comm : ∀{A : Set}{l₁ l₂ : A *} → l₁ ++ l₂ ≡ l₂ ++ l₁

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Transitivity

module Oscar.Class.Transitivity.Function where

module _
  {a}
  where

  instance

    𝓣ransitivityFunction : Transitivity.class Function⟦ a ⟧
    𝓣ransitivityFunction .⋆ f g = g ∘ f


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Definition
open import Sets.FinSet.Definition

module Sets.Cardinality.Infinite.Definition where

InfiniteSet : {a : _} (A : Set a) → Set a
InfiniteSet A = (n : ℕ) → (f : FinSet n → A) → (Bijection f) → False

record DedekindInfiniteSet {a : _} (A : Set a) : Set a where
  field
    inj : ℕ → A
    isInjection : Injection inj


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

pathological : (e : 9999999999 ≡ 9999999999) → Set
pathological refl = Nat


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Container combinators
------------------------------------------------------------------------

module Data.Container.Combinator where

open import Data.Container
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_)
open import Data.Sum renaming (_⊎_ to _⟨⊎⟩_)
open import Data.Unit using (⊤)
open import Function as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_)
open import Function.Inverse using (_↔_)
open import Level
open import Relation.Binary.PropositionalEquality as P
  using (_≗_; refl)

------------------------------------------------------------------------
-- Combinators

-- Identity.

id : ∀ {c} → Container c
id = Lift ⊤ ▷ F.const (Lift ⊤)

-- Constant.

const : ∀ {c} → Set c → Container c
const X = X ▷ F.const (Lift ⊥)

-- Composition.

infixr 9 _∘_

_∘_ : ∀ {c} → Container c → Container c → Container c
C₁ ∘ C₂ = ⟦ C₁ ⟧ (Shape C₂) ▷ ◇ (Position C₂)

-- Product. (Note that, up to isomorphism, this is a special case of
-- indexed product.)

infixr 2 _×_

_×_ : ∀ {c} → Container c → Container c → Container c
C₁ × C₂ =
  (Shape C₁ ⟨×⟩ Shape C₂) ▷
  uncurry (λ s₁ s₂ → Position C₁ s₁ ⟨⊎⟩ Position C₂ s₂)

-- Indexed product.

Π : ∀ {c} {I : Set c} → (I → Container c) → Container c
Π C = (∀ i → Shape (C i)) ▷ λ s → ∃ λ i → Position (C i) (s i)

-- Sum. (Note that, up to isomorphism, this is a special case of
-- indexed sum.)

infixr 1 _⊎_

_⊎_ : ∀ {c} → Container c → Container c → Container c
C₁ ⊎ C₂ = (Shape C₁ ⟨⊎⟩ Shape C₂) ▷ [ Position C₁ , Position C₂ ]

-- Indexed sum.

Σ : ∀ {c} {I : Set c} → (I → Container c) → Container c
Σ C = (∃ λ i → Shape (C i)) ▷ λ s → Position (C (proj₁ s)) (proj₂ s)

-- Constant exponentiation. (Note that this is a special case of
-- indexed product.)

infix 0 const[_]⟶_

const[_]⟶_ : ∀ {c} → Set c → Container c → Container c
const[ X ]⟶ C = Π {I = X} (F.const C)

------------------------------------------------------------------------
-- Correctness proofs

-- I have proved some of the correctness statements under the
-- assumption of functional extensionality. I could have reformulated
-- the statements using suitable setoids, but I could not be bothered.

module Identity where

  correct : ∀ {c} {X : Set c} → ⟦ id ⟧ X ↔ F.id X
  correct {c} = record
    { to         = P.→-to-⟶ {a  = c} λ xs → proj₂ xs _
    ; from       = P.→-to-⟶ {b₁ = c} λ x → (_ , λ _ → x)
    ; inverse-of = record
      { left-inverse-of  = λ _ → refl
      ; right-inverse-of = λ _ → refl
      }
    }

module Constant (ext : ∀ {ℓ} → P.Extensionality ℓ ℓ) where

  correct : ∀ {ℓ} (X : Set ℓ) {Y} → ⟦ const X ⟧ Y ↔ F.const X Y
  correct X {Y} = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { right-inverse-of = λ _ → refl
      ; left-inverse-of  =
          λ xs → P.cong (_,_ (proj₁ xs)) (ext (λ x → ⊥-elim (lower x)))
      }
    }
    where
    to : ⟦ const X ⟧ Y → X
    to = proj₁

    from : X → ⟦ const X ⟧ Y
    from = < F.id , F.const (⊥-elim ∘′ lower) >

module Composition where

  correct : ∀ {c} (C₁ C₂ : Container c) {X : Set c} →
            ⟦ C₁ ∘ C₂ ⟧ X ↔ (⟦ C₁ ⟧ ⟨∘⟩ ⟦ C₂ ⟧) X
  correct C₁ C₂ {X} = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { left-inverse-of  = λ _ → refl
      ; right-inverse-of = λ _ → refl
      }
    }
    where
    to : ⟦ C₁ ∘ C₂ ⟧ X → ⟦ C₁ ⟧ (⟦ C₂ ⟧ X)
    to ((s , f) , g) = (s , < f , curry g >)

    from : ⟦ C₁ ⟧ (⟦ C₂ ⟧ X) → ⟦ C₁ ∘ C₂ ⟧ X
    from (s , f) = ((s , proj₁ ⟨∘⟩ f) , uncurry (proj₂ ⟨∘⟩ f))

module Product (ext : ∀ {ℓ} → P.Extensionality ℓ ℓ) where

  correct : ∀ {c} (C₁ C₂ : Container c) {X : Set c} →
            ⟦ C₁ × C₂ ⟧ X ↔ (⟦ C₁ ⟧ X ⟨×⟩ ⟦ C₂ ⟧ X)
  correct {c} C₁ C₂ {X} = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { left-inverse-of  = from∘to
      ; right-inverse-of = λ _ → refl
      }
    }
    where
    to : ⟦ C₁ × C₂ ⟧ X → ⟦ C₁ ⟧ X ⟨×⟩ ⟦ C₂ ⟧ X
    to ((s₁ , s₂) , f) = ((s₁ , f ⟨∘⟩ inj₁) , (s₂ , f ⟨∘⟩ inj₂))

    from : ⟦ C₁ ⟧ X ⟨×⟩ ⟦ C₂ ⟧ X → ⟦ C₁ × C₂ ⟧ X
    from ((s₁ , f₁) , (s₂ , f₂)) = ((s₁ , s₂) , [ f₁ , f₂ ])

    from∘to : from ⟨∘⟩ to ≗ F.id
    from∘to (s , f) =
      P.cong (_,_ s) (ext {ℓ = c} [ (λ _ → refl) , (λ _ → refl) ])

module IndexedProduct where

  correct : ∀ {c I} (C : I → Container c) {X : Set c} →
            ⟦ Π C ⟧ X ↔ (∀ i → ⟦ C i ⟧ X)
  correct {I = I} C {X} = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { left-inverse-of  = λ _ → refl
      ; right-inverse-of = λ _ → refl
      }
    }
    where
    to : ⟦ Π C ⟧ X → ∀ i → ⟦ C i ⟧ X
    to (s , f) = λ i → (s i , λ p → f (i , p))

    from : (∀ i → ⟦ C i ⟧ X) → ⟦ Π C ⟧ X
    from f = (proj₁ ⟨∘⟩ f , uncurry (proj₂ ⟨∘⟩ f))

module Sum where

  correct : ∀ {c} (C₁ C₂ : Container c) {X : Set c} →
            ⟦ C₁ ⊎ C₂ ⟧ X ↔ (⟦ C₁ ⟧ X ⟨⊎⟩ ⟦ C₂ ⟧ X)
  correct C₁ C₂ {X} = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { left-inverse-of  = from∘to
      ; right-inverse-of = [ (λ _ → refl) , (λ _ → refl) ]
      }
    }
    where
    to : ⟦ C₁ ⊎ C₂ ⟧ X → ⟦ C₁ ⟧ X ⟨⊎⟩ ⟦ C₂ ⟧ X
    to (inj₁ s₁ , f) = inj₁ (s₁ , f)
    to (inj₂ s₂ , f) = inj₂ (s₂ , f)

    from : ⟦ C₁ ⟧ X ⟨⊎⟩ ⟦ C₂ ⟧ X → ⟦ C₁ ⊎ C₂ ⟧ X
    from = [ Prod.map inj₁ F.id , Prod.map inj₂ F.id ]

    from∘to : from ⟨∘⟩ to ≗ F.id
    from∘to (inj₁ s₁ , f) = refl
    from∘to (inj₂ s₂ , f) = refl

module IndexedSum where

  correct : ∀ {c I} (C : I → Container c) {X : Set c} →
            ⟦ Σ C ⟧ X ↔ (∃ λ i → ⟦ C i ⟧ X)
  correct {I = I} C {X} = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { left-inverse-of  = λ _ → refl
      ; right-inverse-of = λ _ → refl
      }
    }
    where
    to : ⟦ Σ C ⟧ X → ∃ λ i → ⟦ C i ⟧ X
    to ((i , s) , f) = (i , (s , f))

    from : (∃ λ i → ⟦ C i ⟧ X) → ⟦ Σ C ⟧ X
    from (i , (s , f)) = ((i , s) , f)

module ConstantExponentiation where

  correct : ∀ {c X} (C : Container c) {Y : Set c} →
            ⟦ const[ X ]⟶ C ⟧ Y ↔ (X → ⟦ C ⟧ Y)
  correct C = IndexedProduct.correct (F.const C)


text:
test : Set → Set
test A with A
test | B = B


text:
module Sec4 where
-- open import Sec2

Prop : Set₁
Prop = Set

Value : Set₁
Value = Set

-- XXX: The true type
data ⊤ : Prop where
  ⋆ : ⊤

-- XXX: The false type
data ⊥ : Prop where

-- XXX: Conjunction of Propositions
data _∧_ (A B : Prop) : Prop where
  and : A → B → (A ∧ B)

-- XXX: The disjuction of propositions
data _∨_ (A B : Prop) : Prop where
  ora : A → A ∨ B
  orb : B → A ∨ B

-- XXX: implication
data _⇒_ (A B : Prop) : Prop where
  impl : (f : A → B) → A ⇒ B

infixr 2 _⇒_

-- XXX: equivalence
data _⇔_ (A B : Prop) : Prop where
  eq : (f₁ : A ⇒ B) → (f₂ : B ⇒ A) → A ⇔ B

-- XXX: Negation as a function
data ¬_ (A : Prop) : Prop where
  neg : A ⇒ ⊥ → (¬ A)

-- XXX: Elimination rules as functions

-- XXX: Eliminating ≡>
elim-⇒ : {A B : Prop} → (f₁ : A ⇒ B) → A → B
elim-⇒ (impl f) x = f x

elim1-⇔ : {A B : Prop} → (A ⇔ B) → A → B
elim1-⇔ (eq (impl f) _) x = f x
elim2-⇔ : {A B : Prop} → (A ⇔ B) → B → A
elim2-⇔ (eq _ (impl f₁)) x = f₁ x

-- XXX: Eliminating disjunction
elim-∨ : {A B C : Prop} → (A ∨ B) → (A → C) → (B → C) → C
elim-∨ (ora x) f₁ _ = f₁ x
elim-∨ (orb x) _ f₂ = f₂ x

-- XXX: Eliminating conjuction
elim1-∧ : {A B : Prop} → (A ∧ B) → A
elim1-∧ (and x x₁) = x
elim2-∧ : {A B : Prop} → (A ∧ B) → B
elim2-∧ (and x x₁) = x₁

-- TODO: Example of proofs of tautology
-- XXX: Easy one
ex1 : {A B : Prop} → ((A ⇒ B) ∧ (B ⇒ A)) ⇔ (A ⇔ B)
ex1 {A} {B} =
        eq
        (impl (λ x →
          let x1 = elim1-∧ x
              x2 = elim2-∧ x
          in
          eq (impl (λ x₁ → elim-⇒ x1 x₁))
             (impl (λ x₁ → elim-⇒ x2 x₁))))

        (impl (λ x →
                   let x1 = elim1-⇔ x
                       x2 = elim2-⇔ x
                   in
                   and
                   (impl (λ x₁ → x1 x₁))
                   (impl (λ x₁ → x2 x₁))))

-- XXX: Transitivity
ex2 : {A B C : Prop} → ((A ⇒ B) ∧ (B ⇒ C)) ⇒ (A ⇒ C)
ex2 = impl (λ x →
           impl (λ x₁ → elim-⇒ (elim2-∧ x) (elim-⇒ (elim1-∧ x) x₁)))

-- XXX: Transitivity in the function space of Agda itself. Equivalent to
-- the above one.
trans : {A B C : Set} → ((A → B) ∧ (B → C)) → (A → C)
trans (and x1 x2) z = let t = x1 z
                          t1 = x2 t
                      in t1
-- (elim-⇒ x x₂)
transitivity : {A B C : Prop} → (A ⇒ B) ⇒ (B ⇒ C) ⇒ (A ⇒ C)
transitivity = impl (λ x →
                    impl
                      (λ x₁ → impl
                              (λ x₂ →
                                elim-⇒ x₁ (elim-⇒ x x₂))))

-- XXX: Moving ∧ into Agda's space. Equivalent to transitivity and trans
-- above.
trans' : {A B C : Set} → (A → B) → (B → C) → (A → C)
trans' x y = λ z → y (x z)

-- XXX: absorption law
absorption : {P Q : Prop} → (P ∨ (P ∧ Q)) ⇔ P
absorption {p} {q} =
               eq
               (impl (λ x → let x1 = elim-∨ x (λ p → p) (λ y → elim1-∧ y) in x1))
               (impl (λ x → ora x))

-- XXX: commutativity
commute : {P Q : Prop} → (P ∧ Q) ⇔ (Q ∧ P)
commute = eq (impl (λ x → and (elim2-∧ x) (elim1-∧ x)))
             (impl (λ x → and (elim2-∧ x) (elim1-∧ x)))

-- XXX: associativity
associative : {P Q R : Prop} → ((P ∧ Q) ∧ R) ⇔ (P ∧ (Q ∧ R))
associative  = eq
               (impl (λ x →
                        and (elim1-∧ (elim1-∧ x))
                            (and (elim2-∧ (elim1-∧ x)) (elim2-∧ x))))
               (impl (λ x →
                        and (and (elim1-∧ x) (elim1-∧ (elim2-∧ x)))
                            (elim2-∧ (elim2-∧ x))))

elim-neg : {A : Prop} → A → (¬ A) → ⊥
elim-neg y (neg x) = elim-⇒ x y

eet : {A B : Prop} → ((¬ A) ∧ (¬ B)) ⇒ (¬ (A ∧ B))
eet = impl (λ x → neg (impl (λ x₁ → elim-neg (elim1-∧ x₁) (elim1-∧ x))))

-- tt : {A : Prop} → (A ∨ (¬ A)) → (¬ (¬ A)) → A
-- tt (ora x) (neg y) = x
-- tt {A} (orb x) (neg y) =
--                        let
--                          z = elim-⇒ y x
--                          t = elim-neg {!!} x
--                        in
--                        {!!}

-- XXX: A ⇒ ¬¬ A
f : {A : Prop} → A ⇒ (¬ (¬ A))
f = impl (λ x → neg (impl (λ x₁ → elim-neg x x₁)))

-- A⇔¬¬A : {A : Prop} → A ⇔ (¬ (¬ A))
-- A⇔¬¬A = eq (impl (λ x → neg (impl (λ x₁ → elim-neg x x₁))))
--            (impl (λ x → {!!}))

-- A⇔A⇒⊥⇒⊥ : {A : Prop} → (A ⇔ ((A ⇒ ⊥) ⇒ ⊥))
-- A⇔A⇒⊥⇒⊥ = eq (impl (λ x → impl (λ x₁ → elim-⇒ x₁ x)))
--          (impl (λ x → {!!}))

-- AC⇒Contra : {A : Prop} → (A ∨ (¬ A)) ⇒ ((¬ (¬ A)) ⇒ A)
-- AC⇒Contra = impl (λ x → impl (λ x₁ → {!!}))

-- XXX: Axiom of choice one way
C-⇒ : {P : Prop} → (P ∨ (¬ P)) ⇒ ⊤
C-⇒ = impl (λ _ → ⋆)

-- XXX: Axiom of choice
-- C-⇔ : {P : Prop} → (P ∨ (¬ P)) ⇔ ⊤
-- C-⇔ = eq
--       (impl (λ _ → ⋆))
--       -- XXX: The following proof is impossible todo
--       -- Goal: .P ∨ (¬ .P)
--       -- ————————————————————————————————————————————————————————————
--       -- x  : ⊤
--       -- .P : Prop
--       (impl (λ x → {!!})) -- XXX: We do not have any proof object of P
--                           -- on the right hand side. This is the
--                           -- difference between constructive logic, and
--                           -- classical logic.

-- distributive : {p q r : Prop} → (p ∧ (q ∨ r)) ⇔ ((p ∧ q) ∨ (p ∧ r))
-- distributive =
--                eq
--                (impl (λ x →
--                         let p = elim1-∧ x
--                             x2 = elim2-∧ x
--                             x3 = elim-∨ x2 (λ q → q) (λ x₁ → {!!})
--                         in
--                         ora (and p x3)))
--                (impl (λ x →
--                         let x1 = elim-∨ x (λ l → elim1-∧ l) (λ r → elim1-∧ r)
--                             x2 = elim-∨ x (λ x₁ → {!!}) (λ r → elim2-∧ r)
--                         in
--                         and x1 (orb x2)))

and-⇒ : {A B : Prop} → (A ∧ B) ⇒ (A ⇒ B)
and-⇒ = impl (λ x → impl (λ x₁ → elim2-∧ x))

tii : {A B C : Prop} → ((A ∧ B) ⇒ C) ⇒ (A ⇒ (B ⇒ C))
tii  = impl (λ x → impl (λ x₁ → impl (λ x₂ → elim-⇒ x (and x₁ x₂))))

-- tii2 : {A B : Prop} → (((¬ A) ∨ B) ∧ A) ⇒ B
-- tii2 = impl (λ x →
--             let
--               x₁ = elim1-∧ x
--               x₂ = elim2-∧ x
--             in
--             {!!})

-- contradiction : {A : Prop} → (¬ (¬ A)) ⇒ A
-- contradiction = impl (λ x → {!!})

-- XXX: Predicate logic
-- XXX: For all introduction
data ForAll (A : Set) (B : A → Prop) : Prop where
  dfun : (∀ (x : A) → (B x)) → (ForAll A B)

elim-ForAll : {A : Set} → (x : A) → {B : A → Prop} → (ForAll A B) → (B x)
elim-ForAll x (dfun x₁) = x₁ x

-- XXX: Exists
data Exists (A : Set) (B : A → Prop) : Prop where
  [_,_] : (x : A) → (B x) → Exists A B

elim1-exists : {A : Prop} → {B : A → Prop} → (Exists A B) → A
elim1-exists [ x , _ ] = x

elim2-exists : {A : Prop} → {B : A → Prop} → (p : Exists A B) → (B (elim1-exists p))
elim2-exists [ _ , x ] = x

-- TODO: Proofs in predicate logic

-- XXX: model-checking depends on this theorem
mthm : {V : Value} → {P : V → Prop} → (Exists V (λ (x : V) → (¬ P x)))
                                   ⇒ (¬ ForAll V P)
mthm = impl (λ x →
            neg (impl (λ x₁ →
                      elim-neg (elim-ForAll (elim1-exists x) x₁) (elim2-exists x))))

pex0 : {X : Set} → {P : X → Prop} → (¬ (Exists X P)) ⇒ (ForAll X (λ x → (¬ P x)))
pex0  = impl (λ x →
             dfun (λ x₁ →
                  neg (impl (λ x₂ →
                            let x1 = elim-neg [ x₁ , x₂ ] x
                            in
                            x1))))

pex0' : {X : Set} → {P : X → Prop} →  (ForAll X (λ x → (¬ P x))) ⇒ (¬ (Exists X P))
pex0' = impl (λ x →
             neg (impl
                 (λ x₁ →
                 let x1 = elim1-exists x₁
                     x1' = elim2-exists x₁
                     x2 = elim-ForAll x1 x
                 in
                 elim-neg x1' x2)))

pex2 : {X Y : Set} → {P : X → Y → Prop} → (Exists Y (λ (y : Y) → (ForAll X (λ (x : X) → P x y))))
                                        ⇒ (ForAll X (λ (x : X) → (Exists Y (λ (y : Y) → P x y))))
pex2 = impl (λ x →
            dfun (λ x₁ →
                 let x1 = elim1-exists x
                     x2 = elim2-exists x
                     x3 = elim-ForAll x₁ x2
                 in
                 [ x1 , x3 ]))

-- TODO: Tautology in first order predicate logic
ptau : {V B : Value} → {A : V → Prop} → (x : V)
                     → (ForAll V (λ _ → (A x) ⇒ B))
                     ⇔ (Exists V (λ _ → (A x) ⇒ B))
ptau a = eq
       (impl (λ x →
             [ a , (impl (λ x₁ →
                            elim-⇒ (elim-ForAll a x) x₁)) ]))
       (impl (λ x → dfun (λ x₁ → impl (λ x₂ →
                                      elim-⇒ (elim2-exists x) x₂))))


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Cocone where

open import Level

open import Categories.Category
open import Categories.Functor hiding (_≡_; _∘_)

record Cocone {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′) where
  module J = Category J
  open Category C
  open Functor F
  field
    N : Obj
    ψ : ∀ X → ((F₀ X) ⇒ N)
    .commute : ∀ {X Y} (f : J [ X , Y ]) → ψ X ≡ ψ Y ∘ F₁ f

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
------------------------------------------------------------------------
-- Up-to techniques, compatibility, size-preserving functions, and the
-- companion
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

-- The definitions below are parametrised by an indexed container.

open import Prelude

open import Indexed-container

module Up-to {ℓ} {I : Type ℓ} (C : Container I I) where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Bijection equality-with-J using (_↔_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import Function-universe.Size equality-with-J

open import Indexed-container.Combinators
  hiding (id; const) renaming (_∘_ to _⊚_)
open import Relation

------------------------------------------------------------------------
-- Up-to techniques

-- This definition of soundness is based on the definition of
-- "b-soundness" given by Pous and Sangiorgi in "Enhancements of the
-- bisimulation proof method", with the following differences:
--
-- * The property is stated for an indexed container rather than a
--   monotone function on a (particular) complete lattice.
--
-- * The extension ⟦ C ⟧ of the container C takes the place of b.
--
-- * The type-theoretic greatest fixpoint ν takes the place of a
--   set-theoretic greatest fixpoint.

Sound : Container I I → Type ℓ
Sound F = ν (C ⊚ F) ∞ ⊆ ν C ∞

-- A relation transformer F is a (sound) up-to technique if every
-- relation R that is contained in ⟦ C ⟧ (F R) is contained in ν C ∞.

Up-to-technique : Trans ℓ I → Type (lsuc ℓ)
Up-to-technique F = ∀ {R} → R ⊆ ⟦ C ⟧ (F R) → R ⊆ ν C ∞

-- The two definitions above are pointwise logically equivalent, if
-- the second one is restricted to containers (in a certain way).

Sound⇔ : ∀ F → Sound F ⇔ Up-to-technique ⟦ F ⟧
Sound⇔ F = record
  { to = λ sound {R} →

      R ⊆ ⟦ C ⟧ (⟦ F ⟧ R)  ↝⟨ ⊆-congʳ _ (_⇔_.from $ ⟦∘⟧↔ _ C) ⟩

      R ⊆ ⟦ C ⊚ F ⟧ R      ↝⟨ unfold (C ⊚ F) ⟩

      R ⊆ ν (C ⊚ F) ∞      ↝⟨ ⊆-congʳ _ sound ⟩□

      R ⊆ ν C ∞            □

  ; from = λ up-to → up-to (

      ν (C ⊚ F) ∞                  ⊆⟨ ν-out _ ⟩

      ⟦ C ⊚ F ⟧ (ν (C ⊚ F) ∞)      ⊆⟨ ⟦∘⟧↔ _ C ⟩∎

      ⟦ C ⟧ (⟦ F ⟧ (ν (C ⊚ F) ∞))  ∎)

  }

------------------------------------------------------------------------
-- Compatibility

-- Compatibility.
--
-- This definition corresponds to Pous and Sangiorgi's definition of
-- b-compatibility.

Compatible : Trans ℓ I → Type (lsuc ℓ)
Compatible F = ∀ {R} → F (⟦ C ⟧ R) ⊆ ⟦ C ⟧ (F R)

-- If F is monotone and compatible, and R is contained in ⟦ C ⟧ (F R),
-- then F ^ω R is a post-fixpoint of ⟦ C ⟧.
--
-- The proof of Pous and Sangiorgi's Theorem 6.3.9 contains a similar
-- result.

compatible→^ω-post-fixpoint :
  ∀ {F} →
  Monotone F → Compatible F →
  ∀ {R} → R ⊆ ⟦ C ⟧ (F R) → F ^ω R ⊆ ⟦ C ⟧ (F ^ω R)
compatible→^ω-post-fixpoint {F} mono comp {R = R} R⊆ = uncurry λ n →
  F ^[ n ] R              ⊆⟨ Fⁿ⊆∘F¹⁺ⁿ n ⟩
  ⟦ C ⟧ (F ^[ 1 + n ] R)  ⊆⟨ map C (1 + n ,_) ⟩∎
  ⟦ C ⟧ (F ^ω R)          ∎
  where
  Fⁿ⊆∘F¹⁺ⁿ : ∀ n → F ^[ n ] R ⊆ ⟦ C ⟧ (F ^[ suc n ] R)
  Fⁿ⊆∘F¹⁺ⁿ zero =
    R            ⊆⟨ R⊆ ⟩∎
    ⟦ C ⟧ (F R)  ∎
  Fⁿ⊆∘F¹⁺ⁿ (suc n) =
    F ^[ 1 + n ] R              ⊆⟨⟩
    F (F ^[ n ] R)              ⊆⟨ mono (Fⁿ⊆∘F¹⁺ⁿ n) ⟩
    F (⟦ C ⟧ (F ^[ 1 + n ] R))  ⊆⟨ comp ⟩∎
    ⟦ C ⟧ (F ^[ 2 + n ] R)      ∎

-- Monotone compatible functions are up-to techniques.
--
-- This is basically Pous and Sangiorgi's Theorem 6.3.9.

monotone→compatible→up-to :
  ∀ {F} → Monotone F → Compatible F → Up-to-technique F
monotone→compatible→up-to {F} mono comp {R = R} R⊆ =
  R       ⊆⟨ 0 ,_ ⟩
  F ^ω R  ⊆⟨ unfold C (compatible→^ω-post-fixpoint mono comp R⊆) ⟩∎
  ν C ∞   ∎

------------------------------------------------------------------------
-- Size-preserving functions (using sized types)

-- F is size-preserving if, for any relation R, if R is contained in
-- ν C i, then F R is contained in ν C i.

Size-preserving : Trans ℓ I → Type (lsuc ℓ)
Size-preserving F = ∀ {R i} → R ⊆ ν C i → F R ⊆ ν C i

-- If a transformer is size-preserving, then it satisfies the
-- corresponding property for ν′, and vice versa.
--
-- Note that this proof uses the size successor function.

size-preserving⇔size-preserving′ :
  ∀ {F} → Size-preserving F ⇔ (∀ {R i} → R ⊆ ν′ C i → F R ⊆ ν′ C i)
force (_⇔_.to size-preserving⇔size-preserving′ pres R⊆ν′Ci x) =
  pres (λ y → force (R⊆ν′Ci y)) x
_⇔_.from size-preserving⇔size-preserving′ pres′ {i = i} R⊆ν′Ci x =
  force (pres′ {i = ssuc i} (λ x → λ { .force → R⊆ν′Ci x }) x)

-- If the relation transformer F is size-preserving, then F is an
-- up-to technique.
--
-- On the other hand, up-to techniques are not necessarily
-- size-preserving, not even for monotone and extensive transformers,
-- see
-- Bisimilarity.Up-to.Counterexamples.∃monotone×extensive×up-to×¬size-preserving.
-- Thus the property of being size-preserving is less general than
-- that of being an up-to technique. However, the latter property is
-- not closed under composition (not even for monotone and extensive
-- transformers, see Bisimilarity.Up-to.Counterexamples.¬-∘-closure),
-- whereas the former property is (see ∘-closure below).

size-preserving→up-to : ∀ {F} → Size-preserving F → Up-to-technique F
size-preserving→up-to {F} pres {R = R} R⊆CFR = helper
  where
  helper : ∀ {i} → R ⊆ ⟦ C ⟧ (ν′ C i)
  helper =
    map C (_⇔_.to size-preserving⇔size-preserving′
             pres (λ x → λ { .force → helper x })) ∘
    R⊆CFR

  -- An alternative implementation of helper which might be a bit
  -- easier to follow.

  helper′ : ∀ {i} → R ⊆ ν C i
  helper′ {i} =
    R               ⊆⟨ R⊆CFR ⟩
    ⟦ C ⟧ (F R)     ⊆⟨ map C (_⇔_.to size-preserving⇔size-preserving′
                                pres (λ x → λ { .force → helper′ x })) ⟩
    ⟦ C ⟧ (ν′ C i)  ⊆⟨ id ⟩∎
    ν C i           ∎

-- If F is monotone, then Size-preserving F is logically equivalent to
-- a special case stating that, for any size i, ν C i should be a
-- pre-fixpoint of F.
--
-- Note that size-preserving relation transformers are not necessarily
-- monotone (or extensive), see
-- Bisimilarity.Up-to.Counterexamples.∃size-preserving×¬[monotone⊎extensive].
--
-- Furthermore there is a container C such that transformers F that
-- satisfy the property ∀ {i} → F (ν C i) ⊆ ν C i are not necessarily
-- up-to techniques for C, see
-- Bisimilarity.Up-to.Counterexamples.∃special-case-of-size-preserving×¬up-to.

monotone→⇔ :
  ∀ {F} →
  Monotone F →
  Size-preserving F ⇔ (∀ {i} → F (ν C i) ⊆ ν C i)
monotone→⇔ mono = record
  { to   = λ pres       → pres id
  ; from = λ pres R⊆νCi → pres ∘ mono R⊆νCi
  }

-- A special case of compatibility.

Compatible′ : Trans ℓ I → Type ℓ
Compatible′ F = ∀ {i} → F (⟦ C ⟧ (ν′ C i)) ⊆ ⟦ C ⟧ (F (ν′ C i))

-- Monotone transformers that satisfy the special case of
-- compatibility are size-preserving.

monotone→compatible′→size-preserving :
  ∀ {F} → Monotone F → Compatible′ F → Size-preserving F
monotone→compatible′→size-preserving {F = F} mono comp =
  _⇔_.from (monotone→⇔ mono) helper
  where

  mutual

    helper : ∀ {i} → F (⟦ C ⟧ (ν′ C i)) ⊆ ⟦ C ⟧ (ν′ C i)
    helper = map C helper′ ∘ comp

    helper′ : ∀ {i} → F (ν′ C i) ⊆ ν′ C i
    force (helper′ x) = helper (mono (λ y → force y) x)

  -- A variant of helper that is perhaps a bit easier to follow.

  helper″ : ∀ {i} → F (ν C i) ⊆ ν C i
  helper″ {i} =
    F (ν C i)           ⊆⟨⟩
    F (⟦ C ⟧ (ν′ C i))  ⊆⟨ comp ⟩
    ⟦ C ⟧ (F (ν′ C i))  ⊆⟨ map C helper′ ⟩
    ⟦ C ⟧ (ν′ C i)      ⊆⟨ id ⟩∎
    ν C i               ∎

  -- This definition is definitionally equal to helper.

  helper″≡helper : (λ {i x} → helper″ {i = i} {x = x}) ≡ helper
  helper″≡helper = refl

-- Monotone, compatible transformers are size-preserving.

monotone→compatible→size-preserving :
  ∀ {F} → Monotone F → Compatible F → Size-preserving F
monotone→compatible→size-preserving mono comp =
  monotone→compatible′→size-preserving mono comp

-- Extensive, size-preserving transformers satisfy the special case of
-- compatibility.

extensive→size-preserving→compatible′ :
  ∀ {F} →
  Extensive F → Size-preserving F → Compatible′ F
extensive→size-preserving→compatible′ {F} extensive pres {i} =
  F (⟦ C ⟧ (ν′ C i))  ⊆⟨⟩
  F (ν C i)           ⊆⟨ pres id ⟩
  ν C i               ⊆⟨⟩
  ⟦ C ⟧ (ν′ C i)      ⊆⟨ map C (extensive _) ⟩∎
  ⟦ C ⟧ (F (ν′ C i))  ∎

-- For monotone and extensive transformers the special case of
-- compatibility is logically equivalent to being size-preserving.
--
-- However, size-preserving transformers are not necessarily
-- compatible, not even if they are monotone and extensive, see
-- Bisimilarity.Up-to.Counterexamples.∃monotone×extensive×size-preserving×¬compatible.
-- Thus the property of being size-preserving is more general than the
-- property of being compatible. However, it is more well-behaved than
-- Up-to-technique, because it is closed under composition (see
-- ∘-closure below).

monotone→extensive→size-preserving⇔compatible′ :
  ∀ {F} →
  Monotone F → Extensive F →
  Size-preserving F ⇔ Compatible′ F
monotone→extensive→size-preserving⇔compatible′ mono extensive = record
  { to   = extensive→size-preserving→compatible′ extensive
  ; from = monotone→compatible′→size-preserving mono
  }

-- The following four lemmas correspond to Pous and Sangiorgi's
-- Proposition 6.3.11.

-- The identity function is size-preserving.

id-size-preserving :
  Size-preserving id
id-size-preserving = id

-- If R is contained in ν C ∞, then const R is size-preserving.

const-size-preserving :
  {R : Rel ℓ I} →
  R ⊆ ν C ∞ →
  Size-preserving (const R)
const-size-preserving R⊆∼ _ = R⊆∼

-- If F and G are both size-preserving, then F ∘ G is also
-- size-preserving.

∘-closure :
  ∀ {F G} →
  Size-preserving F → Size-preserving G → Size-preserving (F ∘ G)
∘-closure F-pres G-pres = F-pres ∘ G-pres

private

  -- An alternative implementation of ∘-closure which might be a bit
  -- easier to follow.

  ∘-closure′ :
    ∀ {F G} →
    Size-preserving F → Size-preserving G → Size-preserving (F ∘ G)
  ∘-closure′ {F} {G} F-pres G-pres {R = R} {i = i} =
   R ⊆ ν C i        ↝⟨ G-pres ⟩
   G R ⊆ ν C i      ↝⟨ F-pres ⟩□
   F (G R) ⊆ ν C i  □

-- If F is a family of size-preserving transformers, then ⋃ lzero F is
-- also size-preserving.

⋃-closure :
  {A : Type ℓ} {F : A → Trans ℓ I} →
  (∀ a → Size-preserving (F a)) →
  Size-preserving (⋃ lzero F)
⋃-closure {F = F} pres {R = R} {i = i} =
  R ⊆ ν C i                        ↝⟨ (λ R⊆∼ {_} → uncurry λ a →

      F a R                              ⊆⟨ pres a (λ {_} → R⊆∼ {_}) ⟩∎
      ν C i                              ∎) ⟩□

  (λ b → ∃ λ a → F a R b) ⊆ ν C i  □

-- If F and G are both size-preserving, then
-- λ R → F R ∪ G R is also size-preserving.

∪-closure :
  {F G : Trans ℓ I} →
  Size-preserving F →
  Size-preserving G →
  Size-preserving (λ R → F R ∪ G R)
∪-closure {F} {G} F-pres G-pres {R = R} {i = i} =
  R ⊆ ν C i          ↝⟨ (λ R⊆∼ {_} → [ F-pres (R⊆∼ {_}) , G-pres (R⊆∼ {_}) ]) ⟩□
  F R ∪ G R ⊆ ν C i  □

------------------------------------------------------------------------
-- The companion

-- The companion.
--
-- The name comes from "Coinduction All the Way Up" by Pous, but this
-- definition is based on the one presented by Parrow and Weber in
-- "The Largest Respectful Function".

Companion : Trans ℓ I
Companion R x = ∀ {i} → R ⊆ ν C i → ν C i x

-- Another conservative approximation of "up-to technique": being
-- below the companion. This notion was presented by Pous in
-- "Coinduction All the Way Up".

Below-the-companion : Trans ℓ I → Type (lsuc ℓ)
Below-the-companion F = ∀ {R} → F R ⊆ Companion R

-- A transformer is below the companion iff it is size-preserving.
--
-- This is a generalisation of the following result, which is based on
-- a proposition due to Pous and Rot.

below-the-companion⇔size-preserving :
  ∀ {F} → Below-the-companion F ⇔ Size-preserving F
below-the-companion⇔size-preserving {F} = record
  { to   = λ below R⊆νCi x → below x R⊆νCi
  ; from = λ pres x R⊆νCi  → pres R⊆νCi x
  }

-- A monotone transformer F is below the companion iff, for all
-- sizes i, ν C i is a pre-fixpoint of F.
--
-- This corresponds roughly to Proposition 5.2 in "Companions,
-- Codensity and Causality" by Pous and Rot.

monotone→below-the-companion⇔size-preserving :
  ∀ {F} →
  Monotone F →
  Below-the-companion F ⇔ (∀ {i} → F (ν C i) ⊆ ν C i)
monotone→below-the-companion⇔size-preserving {F} mono =
  Below-the-companion F        ↝⟨ below-the-companion⇔size-preserving ⟩
  Size-preserving F            ↝⟨ monotone→⇔ mono ⟩□
  (∀ {i} → F (ν C i) ⊆ ν C i)  □

-- The companion is size-preserving.

companion-size-preserving : Size-preserving Companion
companion-size-preserving =
  _⇔_.to below-the-companion⇔size-preserving id

-- The companion is monotone.
--
-- This result corresponds to Lemma 2.13 in "The Largest Respectful
-- Function".

companion-monotone : Monotone Companion
companion-monotone R⊆S f S⊆νCi = f (S⊆νCi ∘ R⊆S)

-- A preservation lemma.

companion-cong :
  ∀ {k R S} →
  Extensionality? ⌊ k ⌋-sym ℓ ℓ →
  (∀ {x} → R x ↝[ ⌊ k ⌋-sym ] S x) →
  (∀ {x} → Companion R x ↝[ ⌊ k ⌋-sym ] Companion S x)
companion-cong {k} {R} {S} ext R↝S {x} =
  (∀ {i} → R ⊆ ν C i → ν C i x)  ↝⟨ implicit-∀-size-cong (lower-extensionality? ⌊ k ⌋-sym _ lzero ext) (→-cong ext (⊆-cong ext R↝S F.id) F.id) ⟩□
  (∀ {i} → S ⊆ ν C i → ν C i x)  □

-- The companion is an up-to technique.

companion-up-to : Up-to-technique Companion
companion-up-to = size-preserving→up-to companion-size-preserving

-- The following four lemmas correspond to parts of Lemma 3.2 from
-- "Coinduction All the Way Up".

-- The identity function is below the companion.

id-below : Below-the-companion id
id-below x f = f x

private

  -- An alternative implementation that might be a bit easier to
  -- follow.

  id-below′ : Below-the-companion id
  id-below′ {R = R} {x = x} Rx {i} =
    R ⊆ ν C i  ↝⟨ (λ f → f Rx) ⟩□
    ν C i x    □

-- ⟦ C ⟧ is below the companion.

⟦⟧-below : Below-the-companion ⟦ C ⟧
⟦⟧-below x = ν-in C ∘ (λ f → f x) ∘ map C

private

  -- An alternative implementation that might be a bit easier to
  -- follow.

  ⟦⟧-below′ : Below-the-companion ⟦ C ⟧
  ⟦⟧-below′ {R = R} {x = x} CR {i} =
    R ⊆ ν C i                ↝⟨ map C ⟩
    ⟦ C ⟧ R ⊆ ⟦ C ⟧ (ν C i)  ↝⟨ (λ f → f CR) ⟩
    ⟦ C ⟧ (ν C i) x          ↝⟨ ν-in C ⟩□
    ν C i x                  □

-- The companion composed with itself is below the companion.

companion∘companion-below : Below-the-companion (Companion ∘ Companion)
companion∘companion-below =
  _⇔_.from below-the-companion⇔size-preserving
    (∘-closure companion-size-preserving companion-size-preserving)

-- The companion is idempotent (in a certain sense).

companion-idempotent :
  ∀ R {x} → Companion (Companion R) x ⇔ Companion R x
companion-idempotent R = record
  { to   = companion∘companion-below
  ; from = Companion R              ⊆⟨ companion-monotone id-below ⟩∎
           Companion (Companion R)  ∎
  }

-- An example illustrating how some of the lemmas above can be used:
-- If F is below the companion, then ⟦ C ⟧ ∘ F is below
-- Companion ∘ Companion, which is below the companion.

below-the-companion-example :
  ∀ {F} → Below-the-companion F → Below-the-companion (⟦ C ⟧ ∘ F)
below-the-companion-example {F} =
  F Below Companion                          ↝⟨ ∘-cong₂ companion-monotone ⟦⟧-below ⟩
  (⟦ C ⟧ ∘ F) Below (Companion ∘ Companion)  ↝⟨ (λ below {_ _} → companion∘companion-below ∘ below {_}) ⟩□
  (⟦ C ⟧ ∘ F) Below Companion                □
  where
  _Below_ : Trans ℓ I → Trans ℓ I → Type (lsuc ℓ)
  F Below G = ∀ {R} → F R ⊆ G R

  ∘-cong₂ : ∀ {F₁ F₂ G₁ G₂ : Trans ℓ I} →
            Monotone F₂ →
            F₁ Below F₂ → G₁ Below G₂ → (F₁ ∘ G₁) Below (F₂ ∘ G₂)
  ∘-cong₂ {F₁} {F₂} {G₁} {G₂} F₂-mono F₁⊆F₂ G₁⊆G₂ {R} =
    F₁ (G₁ R)  ⊆⟨ F₁⊆F₂ ⟩
    F₂ (G₁ R)  ⊆⟨ F₂-mono G₁⊆G₂ ⟩∎
    F₂ (G₂ R)  ∎

-- The greatest fixpoint ν C ∞ is pointwise logically equivalent to
-- the companion applied to an empty relation.
--
-- This corresponds to Theorem 3.3 from "Coinduction All the Way Up".

ν⇔companion-⊥ : ∀ {x} → ν C ∞ x ⇔ Companion (λ _ → ⊥) x
ν⇔companion-⊥ {x} = record
  { to   = λ x _ → x
  ; from = λ f → f (λ ())
  }

-- Every "partial" fixpoint ν C i is a pre-fixpoint of the companion.

companion-ν⊆ν : ∀ {i} → Companion (ν C i) ⊆ ν C i
companion-ν⊆ν {i} =
  (∀ {j} → ν C i ⊆ ν C j → ν C j _)  ↝⟨ (λ hyp → hyp id) ⟩□
  ν C i _                            □

-- Every "partial" fixpoint ν′ C i is a pre-fixpoint of the companion.

companion-ν′⊆ν′ : ∀ {i} → Companion (ν′ C i) ⊆ ν′ C i
force (companion-ν′⊆ν′ hyp) =
  companion-ν⊆ν (companion-monotone (λ x → force x) hyp)

-- The companion applied to the greatest fixpoint ν C ∞ is pointwise
-- logically equivalent to the greatest fixpoint.
--
-- This corresponds to Corollary 3.4 from "Coinduction All the Way
-- Up".

companion-ν⇔ν : ∀ {x} → Companion (ν C ∞) x ⇔ ν C ∞ x
companion-ν⇔ν {x} = record
  { to   = companion-ν⊆ν
  ; from = ν C ∞                ⊆⟨ _⇔_.to ν⇔companion-⊥ ⟩
           Companion (λ _ → ⊥)  ⊆⟨ companion-monotone (λ ()) ⟩∎
           Companion (ν C ∞)    ∎
  }

-- If "one half of f-symmetry" holds for R, for some involution f,
-- then the other half also holds.
--
-- (Pous mentions something similar in "Coinduction All the Way Up".)

other-half-of-symmetry :
  {f : I → I} →
  f ∘ f ≡ id →
  (R : Rel ℓ I) → R ∘ f ⊆ R → R ⊆ R ∘ f
other-half-of-symmetry {f} f-involution R R∘f⊆R =
  R          ⊆⟨ (λ {x} → subst (λ g → R (g x)) (sym f-involution)) ⟩
  R ∘ f ∘ f  ⊆⟨ R∘f⊆R ⟩∎
  R ∘ f      ∎

-- The results in the following module are based on Proposition 7.1 in
-- "Coinduction All the Way Up".

module _
  (D : Container I I)
  (f : I → I)
  (f-involution : f ∘ f ≡ id)
  (C⇔⟷D : ∀ {R : Rel ℓ I} {x} → ⟦ C ⟧ R x ⇔ ⟦ D ⊗ reindex f D ⟧ R x)
  where

  mutual

    ν-symmetric : ∀ {i} → ν C i ∘ f ⊆ ν C i
    ν-symmetric {i} =
      ν C i ∘ f                                          ⊆⟨⟩
      ⟦ C ⟧ (ν′ C i) ∘ f                                 ⊆⟨ _⇔_.to C⇔⟷D ⟩
      ⟦ D ⊗ reindex f D ⟧ (ν′ C i) ∘ f                   ⊆⟨ ⟦⊗⟧↔ _ D (reindex f D) ⟩
      ⟦ D ⟧ (ν′ C i) ∘ f ∩ ⟦ reindex f D ⟧ (ν′ C i) ∘ f  ⊆⟨ Σ-map id (⟦reindex⟧↔ _ D) ⟩
      ⟦ D ⟧ (ν′ C i) ∘ f ∩ ⟦ D ⟧ (ν′ C i ∘ f) ∘ f ∘ f    ⊆⟨ (λ {x} → Σ-map id (subst (λ g → ⟦ D ⟧ (ν′ C i ∘ f) (g x)) f-involution)) ⟩
      ⟦ D ⟧ (ν′ C i) ∘ f ∩ ⟦ D ⟧ (ν′ C i ∘ f)            ⊆⟨ Σ-map (map D (other-half-of-symmetry f-involution (ν′ C i) ν′-symmetric))
                                                                  (map D ν′-symmetric) ⟩
      ⟦ D ⟧ (ν′ C i ∘ f) ∘ f ∩ ⟦ D ⟧ (ν′ C i)            ⊆⟨ swap ⟩
      ⟦ D ⟧ (ν′ C i) ∩ ⟦ D ⟧ (ν′ C i ∘ f) ∘ f            ⊆⟨ Σ-map id (_⇔_.from (⟦reindex⟧↔ _ D)) ⟩
      ⟦ D ⟧ (ν′ C i) ∩ ⟦ reindex f D ⟧ (ν′ C i)          ⊆⟨ _⇔_.from (⟦⊗⟧↔ _ D (reindex f D)) ⟩
      ⟦ D ⊗ reindex f D ⟧ (ν′ C i)                       ⊆⟨ _⇔_.from C⇔⟷D ⟩
      ⟦ C ⟧ (ν′ C i)                                     ⊆⟨ id ⟩∎
      ν C i                                              ∎

    ν′-symmetric : ∀ {i} → ν′ C i ∘ f ⊆ ν′ C i
    force (ν′-symmetric x) = ν-symmetric (force x)

  companion-symmetric : ∀ {R} → Companion R ∘ f ⊆ Companion R
  companion-symmetric {R} {x} =
    Companion R (f x)                  ↔⟨⟩
    (∀ {i} → R ⊆ ν C i → ν C i (f x))  ↝⟨ (λ hyp R⊆ν → ν-symmetric (hyp R⊆ν)) ⦂ (_ → (∀ {i} → R ⊆ ν C i → ν C i x)) ⟩
    (∀ {i} → R ⊆ ν C i → ν C i x)      ↔⟨⟩
    Companion R x                      □

  symmetry-lemma :
    {R S : Rel ℓ I} →
    R ∘ f ⊆ R →
    R ⊆ ⟦ C ⟧ (Companion S) ⇔ R ⊆ ⟦ D ⟧ (Companion S)
  symmetry-lemma {R} {S} R-sym = record { to = to; from = from }
    where
    lemma = λ {x} →
      ⟦ C ⟧ (Companion S) x                                    ↝⟨ C⇔⟷D ⟩
      ⟦ D ⊗ reindex f D ⟧ (Companion S) x                      ↝⟨ ⟦⊗⟧↔ _ D (reindex f D) ⟩
      ⟦ D ⟧ (Companion S) x × ⟦ reindex f D ⟧ (Companion S) x  ↝⟨ ∃-cong (λ _ → ⟦reindex⟧↔ _ D) ⟩□
      ⟦ D ⟧ (Companion S) x × ⟦ D ⟧ (Companion S ∘ f) (f x)    □

    to : R ⊆ ⟦ C ⟧ (Companion S) → R ⊆ ⟦ D ⟧ (Companion S)
    to R⊆CCS =
      R                                                  ⊆⟨ R⊆CCS ⟩
      ⟦ C ⟧ (Companion S)                                ⊆⟨ _⇔_.to lemma ⟩
      ⟦ D ⟧ (Companion S) ∩ ⟦ D ⟧ (Companion S ∘ f) ∘ f  ⊆⟨ proj₁ ⟩∎
      ⟦ D ⟧ (Companion S)                                ∎

    from : R ⊆ ⟦ D ⟧ (Companion S) → R ⊆ ⟦ C ⟧ (Companion S)
    from R⊆DCS =
      R                                                  ⊆⟨ (λ x → x , x) ⟩
      R ∩ R                                              ⊆⟨ Σ-map id (other-half-of-symmetry f-involution R R-sym) ⟩
      R ∩ R ∘ f                                          ⊆⟨ Σ-map R⊆DCS R⊆DCS ⟩
      ⟦ D ⟧ (Companion S) ∩ ⟦ D ⟧ (Companion S) ∘ f      ⊆⟨ Σ-map id (map D (other-half-of-symmetry f-involution
                                                                               (Companion S) companion-symmetric)) ⟩
      ⟦ D ⟧ (Companion S) ∩ ⟦ D ⟧ (Companion S ∘ f) ∘ f  ⊆⟨ _⇔_.from lemma ⟩∎
      ⟦ C ⟧ (Companion S)                                ∎

-- Pous defines the companion in roughly the following way in
-- "Coinduction All the Way Up".
--
-- Note that this definition is large.

Companion₁ : Rel ℓ I → Rel (lsuc ℓ) I
Companion₁ R x = ∃ λ (F : Trans ℓ I) → Monotone F × Compatible F × F R x

-- Pous' variant of the companion is compatible (modulo size issues).
--
-- This corresponds to Lemma 3.2 from "Coinduction All the Way Up".

companion₁-compatible :
  ∀ R → Companion₁ (⟦ C ⟧ R) ⊆ ⟦ C ⟧ (Companion₁ R)
companion₁-compatible R {x} (F , mono , comp , FCR) =
                          $⟨ FCR ⟩
  F (⟦ C ⟧ R) x           ↝⟨ comp ⟩
  ⟦ C ⟧ (F R) x           ↝⟨ map C (λ FR → F , (λ {_ _} → mono) , (λ {_ _} → comp) , FR) ⟩□
  ⟦ C ⟧ (Companion₁ R) x  □

-- Pous' variant of the companion is monotone.

companion₁-monotone : ∀ {R S} → R ⊆ S → Companion₁ R ⊆ Companion₁ S
companion₁-monotone R⊆S =
  ∃-cong λ _ → ∃-cong λ mono → ∃-cong λ _ → mono R⊆S

-- Pous' variant of the companion is contained in Companion.

companion₁⊆companion : ∀ {R} → Companion₁ R ⊆ Companion R
companion₁⊆companion (F , mono , comp , x) =
  _⇔_.from below-the-companion⇔size-preserving
    (monotone→compatible→size-preserving mono comp) x

-- The other direction holds iff Companion is compatible.
--
-- However, I don't know if Companion is provably compatible (in
-- predicative, constructive type theory).

companion-compatible⇔companion⊆companion₁ :
  Compatible Companion ⇔ (∀ {R} → Companion R ⊆ Companion₁ R)
companion-compatible⇔companion⊆companion₁ = record
  { to   = λ comp f → (Companion , companion-monotone , comp , f)
  ; from = λ below f →
             let (F , mono , comp , FCR) = below f
             in map C ((λ FR → companion₁⊆companion (F , mono , comp , FR)) ⦂
                       (_ → Companion _ _))
                      (comp FCR)
  }
  where
  -- An alternative implementation of the from component which might
  -- be a bit easier to follow.

  from′ : (∀ {R} → Companion R ⊆ Companion₁ R) → Compatible Companion
  from′ below {R = R} =
    Companion (⟦ C ⟧ R)      ⊆⟨ below ⟩

    Companion₁ (⟦ C ⟧ R)     ⊆⟨ (λ { (F , mono , comp , x) → (_$ x) (

        F (⟦ C ⟧ R)               ⊆⟨ comp ⟩

        ⟦ C ⟧ (F R)               ⊆⟨ map C (

            F R                        ⊆⟨ (λ y → F , (λ {_ _} → mono) , (λ {_ _} → comp) , y) ⟩
            Companion₁ R               ⊆⟨ companion₁⊆companion ⟩∎
            Companion R                ∎) ⟩∎

        ⟦ C ⟧ (Companion R)        ∎) }) ⟩∎

    ⟦ C ⟧ (Companion R)      ∎

-- Assumptions used by companion-compatible below.

record Companion-compatible-assumptions : Type (lsuc ℓ) where
  field
    -- A strong form of excluded middle, not compatible with
    -- univalence.

    excluded-middle : (P : Type ℓ) → Dec P

  -- The type i < j means that i is a smaller size than j, i ≣ j means
  -- that i is equal to j, and i ≤ j means that i is smaller than or
  -- equal to j.

  infix 4 _<_ _≣_ _≤_

  _<_ : Size → Size → Type
  _<_ = λ i j → Σ (Size< j in-type) λ { k → record { size = i } ≡ k }

  _≣_ : Size → Size → Type
  _≣_ = λ i j →
    _≡_ {A = Size in-type} (record { size = i }) (record { size = j })

  _≤_ : Size → Size → Type
  _≤_ = λ i j → i < j ⊎ i ≣ j

  -- Successor sizes: Sizes i for which there is a size j < i such
  -- that every size k < i satisfies k ≤ j.

  Successor : Size → Type
  Successor i = ∃ λ (j : Size< i in-type) → (k : Size< i) → k ≤ size j

  field
    -- If i is not smaller than or equal to j, then j is smaller
    -- than i.

    ≰→> : ∀ {i j} → ¬ i ≤ j → j < i

    -- If a predicate from a certain class of predicates is satisfied
    -- for all sizes smaller than i, but not for i itself, then i is a
    -- successor size.

    is-successor :
      {R : Rel ℓ I} →
      let P = λ i → R ⊆ ν C i in
      ∀ i →
      ((j : Size< i) → P j) →
      ¬ P i →
      Successor i

    -- Size elimination. A very similar elimination principle can at
    -- the time of writing be implemented in Agda, but Andreas Abel
    -- has suggested that this implementation should not be allowed.

    size-elim :
      (P : Size → Type ℓ) →
      (∀ i → ((j : Size< i) → P j) → P i) →
      ∀ i → P i

  -- A variant of excluded-middle.

  excluded-middle₀ : (P : Type) → Dec P
  excluded-middle₀ P =
    ⊎-map lower (_∘ lift) $ excluded-middle (↑ ℓ P)

  -- "Not for all" implies "exists not".

  ¬∀→∃¬ : {A : Type} {P : A → Type ℓ} →
          ¬ (∀ x → P x) → ∃ λ x → ¬ P x
  ¬∀→∃¬ {P = P} ¬∀ = case excluded-middle (∃ λ x → ¬ P x) of λ where
    (inj₁ ∃¬P)  → ∃¬P
    (inj₂ ¬∃¬P) → ⊥-elim (¬∀ λ x → case excluded-middle (P x) of λ where
      (inj₁ Px)  → Px
      (inj₂ ¬Px) → ⊥-elim (¬∃¬P (x , ¬Px)))

  -- Given the assumptions above every pair of sizes must be related
  -- by either _<_, _≡_, or flip _<_. However, note that all three
  -- relations hold for ∞ and ∞, so we do not get a law of trichotomy.

  compare : ∀ i j → i < j ⊎ i ≣ j ⊎ j < i
  compare i j = case excluded-middle₀ (i < j) of λ where
    (inj₁ i<j) → inj₁ i<j
    (inj₂ i≮j) → case excluded-middle₀ (i ≣ j) of λ where
      (inj₁ i≡j) → inj₂ (inj₁ i≡j)
      (inj₂ i≢j) → inj₂ (inj₂ (≰→> [ i≮j , i≢j ]))

-- Given certain assumptions one can prove that the companion is
-- compatible. (The proof is based on that of Theorem 2.14 in Parrow
-- and Weber's "The Largest Respectful Function".) However, I don't
-- know if these assumptions are consistent with the variant of Agda
-- that is used in this development. I discussed the assumptions with
-- Andreas Abel and Andrea Vezzosi. Some potential problems came up in
-- the discussion:
--
-- * The fact that ∞ : Size< ∞ could perhaps lead to some kind of
--   problem.
--
-- * The assumptions make it possible to define functions that give
--   completely different results for different sizes (assuming that
--   there is more than one size).

companion-compatible :
  Companion-compatible-assumptions → Compatible Companion
companion-compatible assumptions {R} = case lemma R of λ where

    (inj₁ R⊆νC) →
      Companion (⟦ C ⟧ R)  ⊆⟨ _$ map C (λ Rx → λ { .force → R⊆νC Rx }) ⟩
      ν C ∞                ⊆⟨ map C ((λ ν′C∞x _ → force ν′C∞x) ⦂ (_ → Companion _ _)) ⟩∎
      ⟦ C ⟧ (Companion R)  ∎

    (inj₂ (1+i , (i , <1+i→≤i) , <1+i→R⊆νC , R⊈νC[1+i])) →

      let CR⊆νC[1+i] =
            ⟦ C ⟧ R               ⊆⟨ map C (<1+i→R⊆νC (size i)) ⟩
            ⟦ C ⟧ (ν C (size i))  ⊆⟨ map C (λ x → λ { .force {j} → cast (<1+i→≤i j) x }) ⟩∎
            ν C (size 1+i)        ∎

          νCi⊆CompanionR =
            ν C (size i)                                              ⊆⟨ (λ hyp → λ { j≤i → cast j≤i hyp }) ⟩
            (λ x → ∀ {j} → j ≤ size i → ν C j x)                      ⊆⟨ (λ hyp → λ { (j , refl) → hyp (<1+i→≤i (size j)) }) ⟩
            (λ x → ∀ {j} → j < size 1+i → ν C j x)                    ⊆⟨ (λ hyp → λ { j<1+i _ → hyp j<1+i }) ⟩
            (λ x → ∀ {j} → j < size 1+i → R ⊆ ν C j → ν C j x)        ⊆⟨ (λ hyp → λ { 1+i≰j → hyp (≰→> 1+i≰j) }) ⟩
            (λ x → ∀ {j} → ¬ size 1+i ≤ j → R ⊆ ν C j → ν C j x)      ⊆⟨ (λ hyp → λ { {j} → [ (λ 1+i≤j R⊆νCj →
                                                                                ⊥-elim $ R⊈νC[1+i] (
                R                                                                                ⊆⟨ (λ {x} → R⊆νCj {x}) ⟩
                ν C j                                                                              ⊆⟨ cast 1+i≤j ⟩∎
                ν C (size 1+i)                                                                     ∎))
                                                                                , hyp
                                                                                ] }) ⟩
            (λ x → ∀ {j} → Dec (size 1+i ≤ j) → R ⊆ ν C j → ν C j x)  ⊆⟨ (λ hyp → λ { {_} → hyp (excluded-middle₀ _) }) ⟩
            (λ x → ∀ {j} → R ⊆ ν C j → ν C j x)                       ⊆⟨ id ⟩∎
            Companion R                                               ∎

          ν′C[1+i]⊆νCi : ν′ C (size 1+i) ⊆ ν C (size i)
          ν′C[1+i]⊆νCi {x} y =
            let y′ : (j : Size< (size 1+i)) → ν C j x
                y′ = λ { j → y .force {j = j} }
            in y′ (size i)
      in
      Companion (⟦ C ⟧ R)      ⊆⟨ (λ c → c {i = size 1+i} CR⊆νC[1+i]) ⟩
      ν C (size 1+i)           ⊆⟨⟩
      ⟦ C ⟧ (ν′ C (size 1+i))  ⊆⟨ map C ν′C[1+i]⊆νCi ⟩
      ⟦ C ⟧ (ν C (size i))     ⊆⟨ map C νCi⊆CompanionR ⟩∎
      ⟦ C ⟧ (Companion R)      ∎

  where
  open Companion-compatible-assumptions assumptions

  cast : ∀ {j k} → j ≤ k → ν C k ⊆ ν C j
  cast (inj₁ (_ , refl)) x = x
  cast (inj₂ refl)       x = x

  lemma :
    ∀ R → (∀ {i} → R ⊆ ν C i)
            ⊎
          ∃ λ i → Successor (size i) ×
                  ((j : Size< (size i)) → R ⊆ ν C j) ×
                  ¬ R ⊆ ν C (size i)
  lemma R =
    case excluded-middle (∀ {i} → R ⊆ ν C i) of
      ⊎-map id
        (¬ (∀ {i} → R ⊆ ν C i)                          ↝⟨ (λ hyp₁ hyp₂ → hyp₁ λ { {i} → hyp₂ {i = record { size = i }} }) ⟩

         ¬ (∀ {i} → R ⊆ ν C (size i))                   ↝⟨ (λ hyp → ¬∀→∃¬ {P = λ _ → _ ⊆ _} (λ ∀iR⊆νCi → hyp λ {i} → ∀iR⊆νCi i)) ⟩

         (∃ λ i → ¬ R ⊆ ν C (size i))                   ↝⟨ (λ (i , R⊈νCi) →
                                                              size-elim
                                                                (λ i → ¬ R ⊆ ν C i → _)
                                                                (λ i ind-hyp R⊈νCi → case excluded-middle
                                                                                ((j : Size< i in-type) → R ⊆ ν C (size j))
                                                                                of λ where
                                                                     (inj₁ ∀<R⊆νC)  → record { size = i }
                                                                                , (λ { j → ∀<R⊆νC (record { size = j }) })
                                                                                , R⊈νCi
                                                                     (inj₂ ¬∀<R⊆νC) → let j , R⊈νCj = ¬∀→∃¬ ¬∀<R⊆νC
                                                                                in ind-hyp (size j) R⊈νCj)
                                                                (size i) R⊈νCi) ⟩
         (∃ λ i → ((j : Size< (size i)) → R ⊆ ν C j) ×
                  ¬ R ⊆ ν C (size i))                   ↝⟨ (λ { (i , hyp) → (i , uncurry (is-successor (size i)) hyp , hyp) }) ⟩□

         (∃ λ i → Successor (size i) ×
                  ((j : Size< (size i)) → R ⊆ ν C j) ×
                  ¬ R ⊆ ν C (size i))                   □)

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
module Homogenous.Reflexivity where
import Homogenous.Base
import Homogenous.Equality
open Homogenous.Base     using(Arity; Sig; Fa; Fa1; F; F1; T; It; FIHa; FIH; R)
open Homogenous.Equality using(equal; eq_step; eq_step'; eq_step_ar)

import PolyDepPrelude
open PolyDepPrelude using(Bool; true; false; True;
                   pair; fst; snd;
                   zero; suc;
                   left; right;
                   _::_; nil;
                   unit)
import Tools
open Tools       using(liftAnd)
import Reflexivity
open Reflexivity using(lref; Refl; refl)

-- -----------------------------
-- Reflexivity

-- Short-hand notation for mapping a rel. over Fa resp. F

Fa1rel : (n : Arity)-> (X : Set) -> (X -> X -> Bool) ->
         Fa n X -> Fa n (X -> Bool)
Fa1rel n X r = Fa1 n (\x -> (\y -> r x y) )

F1rel  : (fi : Sig)(X : Set) -> (X -> X -> Bool) -> F fi X -> F fi (X -> Bool)
F1rel fi X r = F1 fi (\x -> (\y -> r x y) )

-- Now the real reflexivity lemmas start

ref_eq_step_ar : (n : Arity) (Y : Set) (e : Y -> Y -> Bool) (x : Fa n Y)
                 (ih : FIHa n (lref e) x)
  -> True (eq_step_ar n (Fa1rel n Y e x) x)
ref_eq_step_ar (zero)  Y e (unit)      (unit)      = unit
ref_eq_step_ar (suc m) Y e (pair y ys) (pair r rs) with e y y | r
ref_eq_step_ar (suc m) Y e (pair y ys) (pair r rs) | false | ()
ref_eq_step_ar (suc m) Y e (pair y ys) (pair r rs) | true  | unit =
  ref_eq_step_ar m Y e ys rs

-- Reflexivity for matching constructors is trivial
ref_eq_step' : (fi : Sig)(X : Set)(e : X -> X -> Bool)(x : F fi X)
  -> FIH fi (lref e) x -> True (eq_step' fi (F1rel fi X e x) x)
ref_eq_step' (nil)   X e () -- empty
ref_eq_step' (n :: ns) X e (left  x') = ref_eq_step_ar n X e x'
ref_eq_step' (n :: ns) X e (right y)  = ref_eq_step'  ns X e y

ref_eq' : (fi : Sig) -> (x : T fi) -> lref (equal fi) x
ref_eq' fi =      R fi (ref_eq_step' fi (T fi) (equal fi))

ref_eq : (fi : Sig) -> Refl (equal fi)
ref_eq fi = refl (R fi (ref_eq_step' fi (T fi) (equal fi)))


text:
open import Agda.Builtin.Bool

test : (true : Bool) → Set
test = {!!}  -- C-c C-c


text:
{-# OPTIONS --without-K #-}
module sets.nat.ordering.leq.core where

open import decidable
open import equality.core
open import function.core
open import sets.nat.core
open import sets.empty

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n} → zero ≤ n
  s≤s : ∀ {m n} (p : m ≤ n) → suc m ≤ suc n

ap-pred-≤ : ∀ {n m} → suc n ≤ suc m → n ≤ m
ap-pred-≤ (s≤s p) = p

refl≤ : {n : ℕ} → n ≤ n
refl≤ {0} = z≤n
refl≤ {suc n} = s≤s refl≤

≡⇒≤ : {n m : ℕ} → n ≡ m → n ≤ m
≡⇒≤ refl = refl≤

suc≤ : ∀ {n} → n ≤ suc n
suc≤ {0} = z≤n
suc≤ {suc n} = s≤s suc≤

suc≰ : ∀ {n} → ¬ (suc n ≤ n)
suc≰ {zero} ()
suc≰ {suc n} p = suc≰ (ap-pred-≤ p)

trans≤ : ∀ {n m p} → n ≤ m → m ≤ p → n ≤ p
trans≤ z≤n q = z≤n
trans≤ (s≤s p) (s≤s q) = s≤s (trans≤ p q)

antisym≤ : ∀ {n m} → n ≤ m → m ≤ n → n ≡ m
antisym≤ z≤n z≤n = refl
antisym≤ (s≤s p) (s≤s q) = ap suc (antisym≤ p q)

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
-- You can't define the same module twice.
module ClashingModule where

module A where
module A where

open A


text:
module Nat where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ → ℕ → ℕ
zero    + n  =  n
(suc m) + n  =  suc (m + n)

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩
    suc (1 + 3)
  ≡⟨⟩
    suc (suc (0 + 3))
  ≡⟨⟩
    suc (suc 3)
  ≡⟨⟩
    5
  ∎


text:
{- This example goes through now that we allow instantiation of
   blocked terms #-}
module Issue439 where

record Σ (A : Set) (B : A → Set) : Set where
 constructor _,_
 field
   p₁ : A
   p₂ : B p₁

open Σ

record ⊤ : Set where

data Tree : Set where
 leaf : Tree
 node : Tree → Tree → Tree

mutual

 U : Tree → Set
 U leaf           = ⊤
 U (node tr₁ tr₂) = Σ (U tr₁) λ a → El a → U tr₂

 El : ∀ {tr} → U tr → Set
 El {leaf}         _       = ⊤
 El {node tr₁ tr₂} (a , b) = (x : El a) → El (b x)

mutual

 data C : Set where
   c : (Γ : C) → T Γ → C

 T : C → Set
 T Γ = Σ Tree (λ tr → E Γ → U tr)

 E : C → Set
 E (c Γ σ) = Σ (E Γ) λ γ → El (p₂ σ γ)

postulate
 e : C
 M : (Γ : C) → T Γ → Set
 z : ∀ {Γ σ} → M (c Γ σ) (p₁ σ , λ γ → p₂ σ (p₁ γ))
 l : ∀ {Γ} σ {τ} → M (c Γ σ) τ →
     M Γ (_ , λ γ → p₂ σ γ , λ v → p₂ τ (γ , v))
 a : ∀ {Γ tr₁ tr₂ σ} →
     M Γ (node tr₁ tr₂ , σ) → M Γ (tr₁ , λ γ → p₁ (σ γ)) →
     M Γ (leaf , _)
 s : ∀ {Γ} → M Γ (leaf , _)

t : ∀ {Γ σ} → M Γ σ → T Γ
t {σ = σ} _ = σ

foo : M (c e (leaf , _)) (leaf , _)
foo = a (l (t s) z) z


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

module Data.Quiver.Paths where

-- Paths in a Quiver.
--
-- This is almost the same as the 'paths' in a relation, as defined in
-- Relation.Binary.Construct.Closure.ReflexiveTransitive
-- but here the relation is typed, and that has to be respected. So this
-- is somewhat duplicated

open import Level
open import Data.Quiver
open import Relation.Binary using (Rel; IsEquivalence; Setoid)
import Relation.Binary.Reasoning.Setoid as EqR
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

module Paths {o ℓ e : Level} (Q : Quiver o ℓ e) where
  open Quiver Q hiding (setoid)

  private
    variable
      A B : Obj

  infix 4 _≈*_
  data _≈*_ : (p q : Star _⇒_ A B) → Set (o ⊔ ℓ ⊔ e) where
    ε : {A : Obj} → _≈*_ {A} ε ε
    _◅_ : {A B C : Obj} {x y : A ⇒ B} {p q : Star _⇒_ B C} (x≈y : x ≈ y) (p≈q : p ≈* q) → x ◅ p ≈* y ◅ q

  refl : {p : Star _⇒_ A B} → p ≈* p
  refl {p = ε} = ε
  refl {p = x ◅ p} = Equiv.refl ◅ refl

  sym : {p q : Star _⇒_ A B} → p ≈* q → q ≈* p
  sym ε = ε
  sym (x≈y ◅ eq) = Equiv.sym x≈y ◅ sym eq

  ≡⇒≈* : {p q : Star _⇒_ A B} → p ≡ q → p ≈* q
  ≡⇒≈* ≡.refl = refl

  ≡⇒≈ : {p q : A ⇒ B} → p ≡ q → p ≈ q
  ≡⇒≈ ≡.refl = Equiv.refl

  trans : {p q r : Star _⇒_ A B} → p ≈* q → q ≈* r → p ≈* r
  trans ε ε = ε
  trans (x≈y ◅ ss) (y≈z ◅ tt) = Equiv.trans x≈y y≈z ◅ trans ss tt

  isEquivalence : IsEquivalence (λ (p q : Star _⇒_ A B) → p ≈* q)
  isEquivalence = record { refl = refl ; sym = sym ; trans = trans }

  setoid : Obj → Obj → Setoid (o ⊔ ℓ) (o ⊔ ℓ ⊔ e)
  setoid A B = record { _≈_ = _≈*_ ; isEquivalence = isEquivalence {A} {B} }

  -- convenient to define here
  --
  -- FIXME: this should go into the standard library at
  -- Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
  ◅◅-identityʳ : (f : Star _⇒_ A B) → f ◅◅ ε ≈* f
  ◅◅-identityʳ ε = ε
  ◅◅-identityʳ (x ◅ f) = Equiv.refl ◅ ◅◅-identityʳ f

  module PathEqualityReasoning {A B} where
    open EqR (setoid A B) public

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Base definitions for the right-biased universe-sensitive functor
-- and monad instances for the Product type.
--
-- To minimize the universe level of the RawFunctor, we require that
-- elements of B are "lifted" to a copy of B at a higher universe level
-- (a ⊔ b). See the Data.Product.Categorical.Examples for how this is
-- done.
------------------------------------------------------------------------

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

open import Level

module Data.Product.Categorical.Right.Base
  {b} (B : Set b) (a : Level) where

open import Data.Product using (_×_; map₁; proj₁; proj₂; <_,_>)
open import Category.Functor using (RawFunctor)
open import Category.Comonad using (RawComonad)

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

Productᵣ : Set (a ⊔ b) → Set (a ⊔ b)
Productᵣ A = A × B

functor : RawFunctor Productᵣ
functor = record { _<$>_ = map₁ }

comonad : RawComonad Productᵣ
comonad = record
  { extract = proj₁
  ; extend  = <_, proj₂ >
  }