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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Irrelevance {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView

open import Tools.Embedding
open import Tools.Product
import Tools.PropositionalEquality as PE

-- Irrelevance for propositionally equal types
irrelevance′ : ∀ {A A′ Γ l}
             → A PE.≡ A′
             → Γ ⊩⟨ l ⟩ A
             → Γ ⊩⟨ l ⟩ A′
irrelevance′ PE.refl [A] = [A]

-- Irrelevance for propositionally equal types and contexts
irrelevanceΓ′ : ∀ {l A A′ Γ Γ′}
              → Γ PE.≡ Γ′
              → A PE.≡ A′
              → Γ  ⊩⟨ l ⟩ A
              → Γ′ ⊩⟨ l ⟩ A′
irrelevanceΓ′ PE.refl PE.refl [A] = [A]

mutual
  -- Irrelevance for type equality
  irrelevanceEq : ∀ {Γ A B l l′} (p : Γ ⊩⟨ l ⟩ A) (q : Γ ⊩⟨ l′ ⟩ A)
                → Γ ⊩⟨ l ⟩ A ≡ B / p → Γ ⊩⟨ l′ ⟩ A ≡ B / q
  irrelevanceEq p q A≡B = irrelevanceEqT (goodCasesRefl p q) A≡B

  -- Irrelevance for type equality with propositionally equal first types
  irrelevanceEq′ : ∀ {Γ A A′ B l l′} (eq : A PE.≡ A′)
                   (p : Γ ⊩⟨ l ⟩ A) (q : Γ ⊩⟨ l′ ⟩ A′)
                 → Γ ⊩⟨ l ⟩ A ≡ B / p → Γ ⊩⟨ l′ ⟩ A′ ≡ B / q
  irrelevanceEq′ PE.refl p q A≡B = irrelevanceEq p q A≡B

  -- Irrelevance for type equality with propositionally equal types
  irrelevanceEq″ : ∀ {Γ A A′ B B′ l l′} (eqA : A PE.≡ A′) (eqB : B PE.≡ B′)
                    (p : Γ ⊩⟨ l ⟩ A) (q : Γ ⊩⟨ l′ ⟩ A′)
                  → Γ ⊩⟨ l ⟩ A ≡ B / p → Γ ⊩⟨ l′ ⟩ A′ ≡ B′ / q
  irrelevanceEq″ PE.refl PE.refl p q A≡B = irrelevanceEq p q A≡B

  -- Irrelevance for type equality with propositionally equal second types
  irrelevanceEqR′ : ∀ {Γ A B B′ l} (eqB : B PE.≡ B′) (p : Γ ⊩⟨ l ⟩ A)
                  → Γ ⊩⟨ l ⟩ A ≡ B / p → Γ ⊩⟨ l ⟩ A ≡ B′ / p
  irrelevanceEqR′ PE.refl p A≡B = A≡B

  -- Irrelevance for type equality with propositionally equal types and
  -- a lifting of propositionally equal types
  irrelevanceEqLift″ : ∀ {Γ A A′ B B′ C C′ l l′}
                        (eqA : A PE.≡ A′) (eqB : B PE.≡ B′) (eqC : C PE.≡ C′)
                        (p : Γ ∙ C ⊩⟨ l ⟩ A) (q : Γ ∙ C′ ⊩⟨ l′ ⟩ A′)
                      → Γ ∙ C ⊩⟨ l ⟩ A ≡ B / p → Γ ∙ C′ ⊩⟨ l′ ⟩ A′ ≡ B′ / q
  irrelevanceEqLift″ PE.refl PE.refl PE.refl p q A≡B = irrelevanceEq p q A≡B

  -- Helper for irrelevance of type equality using shape view
  irrelevanceEqT : ∀ {Γ A B l l′} {p : Γ ⊩⟨ l ⟩ A} {q : Γ ⊩⟨ l′ ⟩ A}
                       → ShapeView Γ l l′ A A p q
                       → Γ ⊩⟨ l ⟩ A ≡ B / p → Γ ⊩⟨ l′ ⟩ A ≡ B / q
  irrelevanceEqT (ℕᵥ ℕA ℕB) (ιx (ℕ₌ x)) = ιx (ℕ₌ x)
  irrelevanceEqT (ne (ne K D neK _) (ne K₁ D₁ neK₁ K≡K₁)) (ιx (ne₌ M D′ neM K≡M))
                 rewrite whrDet* (red D , ne neK) (red D₁ , ne neK₁) =
    ιx (ne₌ M D′ neM K≡M)
  irrelevanceEqT {Γ} (Πᵥ (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                         (Πᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
                 (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
    let ΠFG≡ΠF₁G₁   = whrDet* (red D , Πₙ) (red D₁ , Πₙ)
        F≡F₁ , G≡G₁ = Π-PE-injectivity ΠFG≡ΠF₁G₁
    in  Π₌ F′ G′ D′ (PE.subst (λ x → Γ ⊢ x ≅ Π F′ ▹ G′) ΠFG≡ΠF₁G₁ A≡B)
           (λ {ρ} [ρ] ⊢Δ → irrelevanceEq′ (PE.cong (wk ρ) F≡F₁) ([F] [ρ] ⊢Δ)
                                    ([F]₁ [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ))
           (λ {ρ} [ρ] ⊢Δ [a]₁ →
              let [a] = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F≡F₁))
                                         ([F]₁ [ρ] ⊢Δ) ([F] [ρ] ⊢Δ) [a]₁
              in  irrelevanceEq′ (PE.cong (λ y → wk (lift ρ) y [ _ ]) G≡G₁)
                                 ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁) ([G≡G′] [ρ] ⊢Δ [a]))
  irrelevanceEqT (Uᵥ _ _ _ _ _ _) (U₌ B≡U) = U₌ B≡U
  irrelevanceEqT (emb⁰¹ PE.refl x) (ιx A≡B) = irrelevanceEqT x A≡B
  irrelevanceEqT {Γ} {A} {B} {l} {.¹} (emb¹⁰ PE.refl x) A≡B = ιx (irrelevanceEqT x A≡B)

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

  -- Irrelevance for terms
  irrelevanceTerm : ∀ {Γ A t l l′} (p : Γ ⊩⟨ l ⟩ A) (q : Γ ⊩⟨ l′ ⟩ A)
                  → Γ ⊩⟨ l ⟩ t ∷ A / p → Γ ⊩⟨ l′ ⟩ t ∷ A / q
  irrelevanceTerm p q t = irrelevanceTermT (goodCasesRefl p q) t

  -- Irrelevance for terms with propositionally equal types
  irrelevanceTerm′ : ∀ {Γ A A′ t l l′} (eq : A PE.≡ A′)
                     (p : Γ ⊩⟨ l ⟩ A) (q : Γ ⊩⟨ l′ ⟩ A′)
                   → Γ ⊩⟨ l ⟩ t ∷ A / p → Γ ⊩⟨ l′ ⟩ t ∷ A′ / q
  irrelevanceTerm′ PE.refl p q t = irrelevanceTerm p q t

  -- Irrelevance for terms with propositionally equal types and terms
  irrelevanceTerm″ : ∀ {Γ A A′ t t′ l l′}
                      (eqA : A PE.≡ A′) (eqt : t PE.≡ t′)
                      (p : Γ ⊩⟨ l ⟩ A) (q : Γ ⊩⟨ l′ ⟩ A′)
                    → Γ ⊩⟨ l ⟩ t ∷ A / p → Γ ⊩⟨ l′ ⟩ t′ ∷ A′ / q
  irrelevanceTerm″ PE.refl PE.refl p q t = irrelevanceTerm p q t

  -- Irrelevance for terms with propositionally equal types, terms and contexts
  irrelevanceTermΓ″ : ∀ {l l′ A A′ t t′ Γ Γ′}
                     → Γ PE.≡ Γ′
                     → A PE.≡ A′
                     → t PE.≡ t′
                     → ([A]  : Γ  ⊩⟨ l  ⟩ A)
                       ([A′] : Γ′ ⊩⟨ l′ ⟩ A′)
                     → Γ  ⊩⟨ l  ⟩ t ∷ A  / [A]
                     → Γ′ ⊩⟨ l′ ⟩ t′ ∷ A′ / [A′]
  irrelevanceTermΓ″ PE.refl PE.refl PE.refl [A] [A′] [t] = irrelevanceTerm [A] [A′] [t]

  -- Helper for irrelevance of terms using shape view
  irrelevanceTermT : ∀ {Γ A t l l′} {p : Γ ⊩⟨ l ⟩ A} {q : Γ ⊩⟨ l′ ⟩ A}
                         → ShapeView Γ l l′ A A p q
                         → Γ ⊩⟨ l ⟩ t ∷ A / p → Γ ⊩⟨ l′ ⟩ t ∷ A / q
  irrelevanceTermT (ℕᵥ D D′) (ιx (ℕₜ n d n≡n prop)) = ιx (ℕₜ n d n≡n prop)
  irrelevanceTermT (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ιx (neₜ k d nf))
                   with whrDet* (red D₁ , ne neK₁) (red D , ne neK)
  irrelevanceTermT (ne (ne K D neK K≡K) (ne .K D₁ neK₁ K≡K₁)) (ιx (neₜ k d nf))
    | PE.refl = ιx (neₜ k d nf)
  irrelevanceTermT {Γ} {t = t} (Πᵥ (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                   (Πᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
                   (Πₜ f d funcF f≡f [f] [f]₁) =
    let ΠFG≡ΠF₁G₁   = whrDet* (red D , Πₙ) (red D₁ , Πₙ)
        F≡F₁ , G≡G₁ = Π-PE-injectivity ΠFG≡ΠF₁G₁
    in  Πₜ f (PE.subst (λ x → Γ ⊢ t :⇒*: f ∷ x) ΠFG≡ΠF₁G₁ d) funcF
           (PE.subst (λ x → Γ ⊢ f ≅ f ∷ x) ΠFG≡ΠF₁G₁ f≡f)
           (λ {ρ} [ρ] ⊢Δ [a]₁ [b]₁ [a≡b]₁ →
              let [a]   = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F≡F₁))
                                           ([F]₁ [ρ] ⊢Δ) ([F] [ρ] ⊢Δ) [a]₁
                  [b]   = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F≡F₁))
                                           ([F]₁ [ρ] ⊢Δ) ([F] [ρ] ⊢Δ) [b]₁
                  [a≡b] = irrelevanceEqTerm′ (PE.cong (wk ρ) (PE.sym F≡F₁))
                                             ([F]₁ [ρ] ⊢Δ) ([F] [ρ] ⊢Δ) [a≡b]₁
              in  irrelevanceEqTerm′ (PE.cong (λ G → wk (lift ρ) G [ _ ]) G≡G₁)
                                     ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁)
                                     ([f] [ρ] ⊢Δ [a] [b] [a≡b]))
          (λ {ρ} [ρ] ⊢Δ [a]₁ →
             let [a] = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F≡F₁))
                                        ([F]₁ [ρ] ⊢Δ) ([F] [ρ] ⊢Δ) [a]₁
             in  irrelevanceTerm′ (PE.cong (λ G → wk (lift ρ) G [ _ ]) G≡G₁)
                                  ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁) ([f]₁ [ρ] ⊢Δ [a]))
  irrelevanceTermT (Uᵥ .⁰ 0<1 ⊢Γ .⁰ 0<1 _) t = t
  irrelevanceTermT (emb⁰¹ PE.refl x) (ιx t) = irrelevanceTermT x t
  irrelevanceTermT (emb¹⁰ PE.refl x) t = ιx (irrelevanceTermT x t)

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

  -- Irrelevance for term equality
  irrelevanceEqTerm : ∀ {Γ A t u l l′} (p : Γ ⊩⟨ l ⟩ A) (q : Γ ⊩⟨ l′ ⟩ A)
                    → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / p → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ A / q
  irrelevanceEqTerm p q t≡u = irrelevanceEqTermT (goodCasesRefl p q) t≡u

  -- Irrelevance for term equality with propositionally equal types
  irrelevanceEqTerm′ : ∀ {Γ A A′ t u l l′} (eq : A PE.≡ A′)
                       (p : Γ ⊩⟨ l ⟩ A) (q : Γ ⊩⟨ l′ ⟩ A′)
                     → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / p → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ A′ / q
  irrelevanceEqTerm′ PE.refl p q t≡u = irrelevanceEqTerm p q t≡u

  -- Irrelevance for term equality with propositionally equal types and terms
  irrelevanceEqTerm″ : ∀ {Γ A A′ t t′ u u′ l l′}
                        (eqt : t PE.≡ t′) (equ : u PE.≡ u′) (eqA : A PE.≡ A′)
                        (p : Γ ⊩⟨ l ⟩ A) (q : Γ ⊩⟨ l′ ⟩ A′)
                      → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / p → Γ ⊩⟨ l′ ⟩ t′ ≡ u′ ∷ A′ / q
  irrelevanceEqTerm″ PE.refl PE.refl PE.refl p q t≡u = irrelevanceEqTerm p q t≡u

  -- Helper for irrelevance of term equality using shape view
  irrelevanceEqTermT : ∀ {Γ A t u} {l l′} {p : Γ ⊩⟨ l ⟩ A} {q : Γ ⊩⟨ l′ ⟩ A}
                           → ShapeView Γ l l′ A A p q
                           → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / p → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ A / q
  irrelevanceEqTermT (ℕᵥ D D′) (ιx (ℕₜ₌ k k′ d d′ k≡k′ prop)) = ιx (ℕₜ₌ k k′ d d′ k≡k′ prop)
  irrelevanceEqTermT (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ιx (neₜ₌ k m d d′ nf))
                     with whrDet* (red D₁ , ne neK₁) (red D , ne neK)
  irrelevanceEqTermT (ne (ne K D neK K≡K) (ne .K D₁ neK₁ K≡K₁)) (ιx (neₜ₌ k m d d′ nf))
    | PE.refl = ιx (neₜ₌ k m d d′ nf)
  irrelevanceEqTermT {Γ} {t = t} {u = u}
                     (Πᵥ (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                         (Πᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
                     (Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g]) =
    let ΠFG≡ΠF₁G₁   = whrDet* (red D , Πₙ) (red D₁ , Πₙ)
        F≡F₁ , G≡G₁ = Π-PE-injectivity ΠFG≡ΠF₁G₁
        [A]         = Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext
        [A]₁        = Πᵣ′ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁
    in  Πₜ₌ f g (PE.subst (λ x → Γ ⊢ t :⇒*: f ∷ x) ΠFG≡ΠF₁G₁ d)
            (PE.subst (λ x → Γ ⊢ u :⇒*: g ∷ x) ΠFG≡ΠF₁G₁ d′) funcF funcG
            (PE.subst (λ x → Γ ⊢ f ≅ g ∷ x) ΠFG≡ΠF₁G₁ f≡g)
            (irrelevanceTerm [A] [A]₁ [f]) (irrelevanceTerm [A] [A]₁ [g])
            (λ {ρ} [ρ] ⊢Δ [a]₁ →
               let [a] = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F≡F₁))
                                          ([F]₁ [ρ] ⊢Δ) ([F] [ρ] ⊢Δ) [a]₁
               in  irrelevanceEqTerm′ (PE.cong (λ G → wk (lift ρ) G [ _ ]) G≡G₁)
                                     ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁) ([f≡g] [ρ] ⊢Δ [a]))
  irrelevanceEqTermT (Uᵥ .⁰ 0<1 ⊢Γ .⁰ 0<1 ⊢Γ₁) t≡u = t≡u
  irrelevanceEqTermT (emb⁰¹ PE.refl x) (ιx t≡u) = irrelevanceEqTermT x t≡u
  irrelevanceEqTermT (emb¹⁰ PE.refl x) t≡u = ιx (irrelevanceEqTermT x t≡u)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
{-# OPTIONS --copatterns #-}
{-# OPTIONS --allow-unsolved-metas #-}
-- {-# OPTIONS --show-implicit #-}

-- One-place functors (decorations) on Set

module Control.Decoration where

open import Data.Product using (_×_; _,_; proj₁; proj₂; uncurry)
open import Function using (id; _∘_; const)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Axiom.FunctionExtensionality
open import Control.Functor hiding (Id; Const) renaming (idIsFunctor to Id; compIsFunctor to _·_; constIsFunctor to Const)
open import Control.Functor.NaturalTransformation using (IsNatTrans; KKNat)
open import Control.Comonad

open IsFunctor

record IsDecoration (D : Set → Set) : Set₁ where
  field
    traverse    : ∀ {F} (F! : IsFunctor F) {A B} →

        (A → F B) → D A → F (D B)

    -- The free theorem for traverse:
    -- A natural transformation after a traversal can be combined with the traversal.

    traverse-free : ∀ {F} (F! : IsFunctor F) {G} (G! : IsFunctor G) →
      ∀ (η : ∀ {A} → F A → G A) (η! : IsNatTrans (functor F F!) (functor G G!) η) →
      ∀ {A B} (f : A → F B) →

        η ∘ traverse F! f ≡ traverse G! (η ∘ f)

    -- Identity traversal.

    traverse-id : ∀ {A} →

        traverse Id {A = A} id ≡ id

    -- Distributing a traversal.

    traverse-∘  :
      ∀ {F G} (F! : IsFunctor F) (G! : IsFunctor G) →
      ∀ {A B C} {f : A → F B} {g : B → G C} →

        traverse (F! · G!) ((map F! g) ∘ f) ≡ map F! (traverse G! g) ∘ traverse F! f

  isFunctor : IsFunctor D
  isFunctor = record
    { ops   = record { map    = traverse Id }
    ; laws  = record { map-id = traverse-id
                     ; map-∘  = traverse-∘ Id Id
                     }
    }

  open IsFunctor isFunctor using () renaming (map to dmap; map-∘ to dmap-∘)

  -- Lens operations.

  private

    gets : ∀ {A B} → (A → B) → D A → B
    gets {B = B} = traverse (Const B) {B = B}

    get : ∀ {A} → D A → A
    get = gets id

    modify : ∀ {A B} → (A → B) → D A → D B
    modify = dmap

    set : ∀ {A B} → B → D A → D B
    set b = dmap (const b)

  -- Comonad structure.

  isComonad : IsComonad D
  isComonad = record
    { extract  = extract
    ; extend   = extend
    ; extend-β = extend-β _
    ; extend-η = extend-η
    ; extend-∘ = {!!}
    }
    where
      extract : ∀ {A} → D A → A
      extract {A = A} = get

      extend : ∀ {A B} → (D A → B) → (D A → D B)
      extend {A = A}{B = B} f x = set (f x) x
--      extend {A = A}{B = B} f = uncurry set ∘ (λ x → f x , x)

      -- The get-set law.

      extend-β : ∀ {A B} (f : D A → B) → extract ∘ extend f ≡ f
      extend-β {A = A}{B = B} f = begin
        extract ∘ extend f                                     ≡⟨⟩
        get ∘ (λ x → set (f x) x)                              ≡⟨⟩
        traverse (Const B) id  ∘ (λ x → dmap (const (f x)) x)  ≡⟨⟩
        (λ x → traverse (Const B) id (dmap (const (f x)) x))   ≡⟨⟩
        (λ x → (traverse (Const B) id ∘ traverse Id (const (f x))) x)  ≡⟨ {! traverse-∘!} ⟩
        (λ x → traverse (Const B) (const (f x)) x)                     ≡⟨ {!gets=∘get!} ⟩
        (λ x → (const (f x) ∘ traverse (Const A) id) x)        ≡⟨⟩
        (λ x → f x)                                            ≡⟨⟩
        f                                                      ∎

      -- The set-get law.

      extend-η : ∀ {A} → extend {A = A} extract ≡ id
      extend-η = begin
         extend extract         ≡⟨⟩
         (λ x → set (get x) x)  ≡⟨ {!!} ⟩
         id ∎

      -- The set-set law.

   -- Lens structure.

  -- Law: gets in terms of get.
  gets=∘get : ∀ {A B} (f : A → B) →

      gets f ≡ f ∘ get

  gets=∘get {A = A}{B = B} f =
    begin
      gets f
        ≡⟨⟩
      traverse (Const B) {B = B} f
        ≡⟨ traverse-∘ (Const B) Id {g = f} ⟩
      traverse (Const B) {B = A} f
        ≡⟨ sym (traverse-free (Const A) (Const B) f (KKNat f) id) ⟩
      f ∘ traverse (Const A) {B = A} id
        ≡⟨⟩
      f ∘ get
    ∎

  -- Constant traversal.

  traverse-c :  ∀ {A B} (b : B) (l : D A) → B
  traverse-c {B = B} b = traverse (Const B) {B = B} (const b)

  -- Holds by parametricity (since type B is arbitrary and there is just one b : B given).

  traverse-const : ∀ {A B} {b : B} (l : D A) →

      traverse (Const B) (const b) l ≡ b

  traverse-const {A = A} {B = B} {b = b} l =
    begin
      traverse (Const B) (const b) l               ≡⟨ cong (λ z → z l) (gets=∘get (const b)) ⟩
      (const b ∘ traverse (Const A) {B = B} id) l  ≡⟨⟩
      b
    ∎

  -- Lens laws.

  -- 1. Get what you set.

  get-set : ∀ {A} {a : A} →

      get ∘ set {A = A} a ≡ const a

  get-set {A = A} {a = a} =
    begin
      get ∘ set a                                             ≡⟨⟩
      get ∘ dmap (const a)                                    ≡⟨⟩
      traverse (Const A) id ∘ traverse Id (const a)           ≡⟨⟩
      map Id (traverse (Const A) id) ∘ traverse Id (const a)  ≡⟨ sym (traverse-∘ Id (Const A)) ⟩
      traverse (Id · Const A) (map Id id ∘ const a)           ≡⟨⟩
      traverse (Const A) (const a)                            ≡⟨⟩
      gets (const a)                                          ≡⟨ gets=∘get (const a) ⟩
      const a ∘ get                                           ≡⟨⟩
      const a
    ∎

  -- 2. Set what you got.

  set-get : ∀ {A} (l : D A) →

      set (get l) l ≡ l

  set-get {A = A} l =
    begin

      set (get l) l               ≡⟨⟩
      dmap (λ _ → get l) l        ≡⟨⟩
      traverse Id (λ _ → get l) l ≡⟨ {!!} ⟩
      l
    ∎

  -- 3. Set twice is set once.

  set-set : ∀ {A} (a b : A) →

    set a ∘ set {A = A} b  ≡  set a

  set-set a b =
    begin
      set a ∘ set b                    ≡⟨⟩
      dmap (const a) ∘ dmap (const b)  ≡⟨ sym dmap-∘ ⟩
      dmap (const a ∘ const b)         ≡⟨⟩
      dmap (const a)                   ≡⟨⟩
      set a
    ∎

open IsDecoration

-- Identity decoration.

idIsDecoration : IsDecoration (λ A → A)
traverse      idIsDecoration F! f         = f
traverse-free idIsDecoration F! G! η η! f = refl
traverse-id   idIsDecoration              = refl
traverse-∘    idIsDecoration F! G!        = refl

-- Decoration composition.

_•_ : ∀ {D E} → IsDecoration D → IsDecoration E → IsDecoration (λ A → D (E A))

traverse    (d • e) F f = traverse d F (traverse e F f)

traverse-free (d • e) F G η η! f =
  begin
    η ∘ traverse (d • e) F f    ≡⟨⟩
    η ∘ traverse d F (traverse e F f)    ≡⟨  traverse-free d F G η η! _ ⟩
    traverse d G (η ∘ traverse e F f)    ≡⟨  cong (traverse d G) (traverse-free e F G η η! f) ⟩
    traverse d G (traverse e G (η ∘ f))  ≡⟨⟩
    traverse (d • e) G (η ∘ f)
  ∎

traverse-id (d • e) =
  begin
    traverse d Id (traverse e Id id)  ≡⟨ cong (traverse d Id) (traverse-id e) ⟩
    traverse d Id id                  ≡⟨ traverse-id d ⟩
    id
  ∎

traverse-∘ (d • e) F G {f = f} {g = g} =
  begin
    traverse (d • e) FG (map F g ∘ f)                                       ≡⟨⟩
    traverse d FG (traverse e FG (map F g ∘ f))                             ≡⟨ cong (traverse d FG) (traverse-∘ e F G) ⟩
    traverse d FG (map F (traverse e G g) ∘ traverse e F f)                 ≡⟨ traverse-∘ d F G ⟩
    map F (traverse d G (traverse e G g)) ∘ traverse d F (traverse e F f)   ≡⟨⟩
    map F (traverse (d • e) G g) ∘ traverse (d • e) F f
  ∎
  where FG = F · G

-- The instance.

decoration : ∀ {A} → IsDecoration (_×_ A)
-- traverse decoration F f (a , x) = map F (_,_ a) (f x)           -- FAILS BUG WITH record pattern trans!!
traverse      decoration F f ax              = map F (_,_ (proj₁ ax)) (f (proj₂ ax)) -- WORKS

traverse-free decoration F G η η! f          =  fun-ext λ ax → let (a , x) = ax in
  begin
    (η ∘ traverse decoration F f) (a , x)  ≡⟨⟩
    (η ∘ map F (_,_ a)) (f x)              ≡⟨  cong (λ z → z (f x)) (η! (_,_ a))  ⟩
    (map G (_,_ a) ∘ η) (f x)              ≡⟨⟩
    map G (_,_ a) (η (f x))                ≡⟨⟩
    traverse decoration G (η ∘ f) (a , x)
  ∎

traverse-id   decoration                     = refl

traverse-∘    decoration F G {f = f} {g = g} = fun-ext λ ax → let (a , x) = ax in
  begin
    traverse decoration FG (map F g ∘ f) (a , x)                        ≡⟨⟩
    map FG (_,_ a) (map F g (f x))                                      ≡⟨⟩
    map F (map G (_,_ a)) (map F g (f x))                               ≡⟨ cong (λ z → z _) (sym (map-∘ F))  ⟩
    map F (map G (_,_ a) ∘ g) (f x)                                     ≡⟨⟩
    map F (λ y → map G (_,_ a) (g y)) (f x)                             ≡⟨⟩
    map F (λ y → traverse decoration G g (a , y)) (f x)                 ≡⟨⟩
    map F (traverse decoration G g ∘ (_,_ a)) (f x)                     ≡⟨ cong (λ z → z _) (map-∘ F) ⟩
    map F (traverse decoration G g) (map F (_,_ a) (f x))               ≡⟨⟩
    map F (traverse decoration G g) (traverse decoration F f (a , x))   ≡⟨⟩
    (map F (traverse decoration G g) ∘ traverse decoration F f) (a , x)
  ∎
  where FG = F · G

ext: agda

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
open import Agda.Primitive using (_⊔_; lsuc; lzero)

import Categories.Category as Category
import Categories.Category.Cartesian as Cartesian

import MultiSorted.Model as Model
import MultiSorted.Interpretation as Interpretation
import MultiSorted.UniversalModel as UniversalModel
import MultiSorted.SyntacticCategory as SyntacticCategory
import MultiSorted.UniversalModel as UniversalModel

open import MultiSorted.AlgebraicTheory

module MultiSorted.Completeness
         {ℓt}
         {𝓈 ℴ}
         {Σ : Signature {𝓈} {ℴ}}
         (T : Theory ℓt Σ) where

  open Theory T
  open UniversalModel T

  -- An equation is semantically valid when it holds in all models
  valid : ∀ (ε : Equation Σ) → Set (lsuc (lsuc ℓt ⊔ lsuc 𝓈 ⊔ lsuc ℴ))
  valid ε = ∀ {𝒞 : Category.Category 𝓈 (lsuc ℴ) (lsuc (ℓt ⊔ 𝓈 ⊔ ℴ))}
              {cartesian-𝒞 : Cartesian.Cartesian 𝒞}
              {I : Interpretation.Interpretation Σ cartesian-𝒞}
              (M : Model.Model T I) → Interpretation.Interpretation.⊨_ I ε

  -- Completeness: semantic validity implies provability
  valid-⊢ : ∀ (ε : Equation Σ) → valid ε → ⊢ ε
  valid-⊢ ε v = universality ε (v 𝒰)

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
------------------------------------------------------------------------------
-- Totality properties respect to Bool
------------------------------------------------------------------------------

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

module FOTC.Program.SortList.Properties.Totality.BoolATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Bool.PropertiesATP
open import FOTC.Data.Bool.Type
open import FOTC.Data.Nat.List.Type
open import FOTC.Data.Nat.Type
open import FOTC.Program.SortList.SortList

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

le-ItemList-Bool : ∀ {item is} → N item → ListN is → Bool (le-ItemList item is)
le-ItemList-Bool {item} Nitem lnnil = prf
  where postulate prf : Bool (le-ItemList item [])
        {-# ATP prove prf #-}

le-ItemList-Bool {item} Nitem (lncons {i} {is} Ni Lis) =
  prf (le-ItemList-Bool Nitem Lis)
  where postulate prf : Bool (le-ItemList item is) →
                        Bool (le-ItemList item (i ∷ is))
        {-# ATP prove prf &&-Bool le-Bool #-}

le-Lists-Bool : ∀ {is js} → ListN is → ListN js → Bool (le-Lists is js)
le-Lists-Bool {js = js} lnnil LNjs = prf
  where postulate prf : Bool (le-Lists [] js)
        {-# ATP prove prf #-}
le-Lists-Bool {js = js} (lncons {i} {is} Ni LNis) LNjs =
  prf (le-Lists-Bool LNis LNjs)
  where postulate prf : Bool (le-Lists is js) → Bool (le-Lists (i ∷ is) js)
        {-# ATP prove prf &&-Bool le-ItemList-Bool #-}

ordList-Bool : ∀ {is} → ListN is → Bool (ordList is)
ordList-Bool lnnil = prf
  where postulate prf : Bool (ordList [])
        {-# ATP prove prf #-}

ordList-Bool (lncons {i} {is} Ni LNis) = prf (ordList-Bool LNis)
  where postulate prf : Bool (ordList is) → Bool (ordList (i ∷ is))
        {-# ATP prove prf &&-Bool le-ItemList-Bool #-}

le-ItemTree-Bool : ∀ {item t} → N item → Tree t → Bool (le-ItemTree item t)
le-ItemTree-Bool {item} Nt tnil = prf
  where postulate prf : Bool (le-ItemTree item nil)
        {-# ATP prove prf #-}
le-ItemTree-Bool {item} Nitem (ttip {i} Ni) = prf
  where postulate prf : Bool (le-ItemTree item (tip i))
        {-# ATP prove prf le-Bool #-}
le-ItemTree-Bool {item} Nitem  (tnode {t₁} {i} {t₂} Tt₁ Ni Tt₂) =
  prf (le-ItemTree-Bool Nitem Tt₁) (le-ItemTree-Bool Nitem Tt₂)
  where postulate prf : Bool (le-ItemTree item t₁) →
                        Bool (le-ItemTree item t₂) →
                        Bool (le-ItemTree item (node t₁ i t₂))
        {-# ATP prove prf &&-Bool #-}

le-TreeItem-Bool : ∀ {t item} → Tree t → N item → Bool (le-TreeItem t item)
le-TreeItem-Bool {item = item } tnil Nt = prf
  where postulate prf : Bool (le-TreeItem nil item)
        {-# ATP prove prf #-}
le-TreeItem-Bool {item = item} (ttip {i} Ni) Nitem = prf
  where postulate prf : Bool (le-TreeItem (tip i) item)
        {-# ATP prove prf le-Bool #-}
le-TreeItem-Bool {item = item} (tnode {t₁} {i} {t₂} Tt₁ Ni Tt₂) Nitem =
  prf (le-TreeItem-Bool Tt₁ Nitem) (le-TreeItem-Bool Tt₂ Nitem)
  where postulate prf : Bool (le-TreeItem t₁ item) →
                        Bool (le-TreeItem t₂ item) →
                        Bool (le-TreeItem (node t₁ i t₂) item)
        {-# ATP prove prf &&-Bool #-}

ordTree-Bool : ∀ {t} → Tree t → Bool (ordTree t)
ordTree-Bool tnil = prf
  where postulate prf : Bool (ordTree nil)
        {-# ATP prove prf #-}

ordTree-Bool (ttip {i} Ni) = prf
  where postulate prf : Bool (ordTree (tip i))
        {-# ATP prove prf #-}

ordTree-Bool (tnode {t₁} {i} {t₂} Tt₁ Ni Tt₂) =
  prf (ordTree-Bool Tt₁) (ordTree-Bool Tt₂)
  where postulate prf : Bool (ordTree t₁) →
                        Bool (ordTree t₂) →
                        Bool (ordTree (node t₁ i t₂))
        {-# ATP prove prf &&-Bool le-TreeItem-Bool le-ItemTree-Bool #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Universes
------------------------------------------------------------------------

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

module Universe where

open import Data.Product
open import Function
open import Level

-- Universes.

record Universe u e : Set (suc (u ⊔ e)) where
  field
    -- Codes.
    U : Set u

    -- Decoding function.
    El : U → Set e

-- Indexed universes.

record Indexed-universe i u e : Set (suc (i ⊔ u ⊔ e)) where
  field
    -- Index set.
    I : Set i

    -- Codes.
    U : I → Set u

    -- Decoding function.
    El : ∀ {i} → U i → Set e

  -- An indexed universe can be turned into an unindexed one.

  unindexed-universe : Universe (i ⊔ u) e
  unindexed-universe = record
    { U  = ∃ λ i → U i
    ; El = El ∘ proj₂
    }


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

module Relation.Nullary.Stable.Base where

open import Data.Empty
open import Level

Stable : Type a → Type a
Stable A = ¬ ¬ A → A

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Common.Reflection where

open import Agda.Builtin.Reflection public renaming
  ( arg-info      to argInfo
  ; function      to funDef
  ; data-type     to dataDef
  ; record-type   to recordDef
  ; agda-sort     to sort
  ; name          to qname
  ; absurd-clause to absurdClause
  ; pat-lam       to extLam
  ; proj          to projP
  ; instance′      to inst
  ; Visibility    to Hiding
  ; Name          to QName)
open import Common.Level
open import Common.Prelude hiding (_>>=_)

pattern vArg x = arg (argInfo visible relevant) x
pattern hArg x = arg (argInfo hidden  relevant) x
pattern iArg x = arg (argInfo inst    relevant) x

Args = List (Arg Term)

data FunDef : Set where
  funDef : Type → List Clause → FunDef

Tactic = Term → TC ⊤

give : Term → Tactic
give v = λ hole → unify hole v

define : Arg QName → FunDef → TC ⊤
define (arg i f) (funDef a cs) =
  bindTC (declareDef (arg i f) a) λ _ →
  defineFun f cs

newMeta : Type → TC Term
newMeta a = checkType unknown a

numberOfParameters : QName → TC Nat
numberOfParameters d =
  bindTC (getDefinition d) λ
  { (dataDef n _) → returnTC n
  ; _ → typeError (strErr "Cannot get parameters of non-data type" ∷ nameErr d ∷ [])
  }

getConstructors : QName → TC (List QName)
getConstructors d =
  bindTC (getDefinition d) λ
  { (dataDef _ cs)  → returnTC cs
  ; (recordDef c _) → returnTC (c ∷ [])
  ; _ → typeError (strErr "Cannot get constructors of non-data or record type" ∷ nameErr d ∷ [])
  }

infixl 1 _>>=_
_>>=_ = bindTC

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module gugugu where

open import Relation.Binary.PropositionalEquality
open import Data.List
open import Data.List.Properties
open import Agda.Builtin.Sigma
-- you can import other functions from the stdlib here

++-injectiveʳ : ∀ {ℓ} {A : Set ℓ} (a b c : List A) → a ++ b ≡ a ++ c → b ≡ c
++-injectiveʳ [] b c p = p
++-injectiveʳ (x ∷ a) b c p = ++-injectiveʳ a b c (snd (∷-injective p))

lemma : ∀ {ℓ} {A : Set ℓ} (x : A) (xs ys : List A) → xs ++ x ∷ ys ≡ (xs ++ x ∷ []) ++ ys
lemma x [] ys = refl
lemma x (x₁ ∷ xs) ys = cong (_∷_ x₁) (lemma x xs ys)

col : ∀ {ℓ} {A : Set ℓ} (x : A) (xs : List A) → xs ++ x ∷ [] ≡ (xs ∷ʳ x)
col x [] = refl
col x (x₁ ∷ xs) = refl

silly' : ∀ {ℓ} {A : Set ℓ} (x : A) (xs ys : List A) → xs ++ x ∷ [] ≡ ys ++ x ∷ [] → xs ∷ʳ x ≡ ys ∷ʳ x
silly' x xs ys = λ z → z

silly : ∀ {ℓ} {A : Set ℓ} (x : A) (xs ys : List A) → xs ++ x ∷ [] ≡ ys ++ x ∷ [] → xs ≡ ys
silly x xs ys p rewrite col x xs | col x ys = fst (∷ʳ-injective xs ys (silly' x xs ys p))

-- inductive can do this job too.
++-injectiveˡ : ∀ {ℓ} {A : Set ℓ} (a b c : List A) → a ++ c ≡ b ++ c → a ≡ b
++-injectiveˡ a b [] p rewrite ++-identityʳ a | ++-identityʳ b = p
++-injectiveˡ a b (x ∷ c) p rewrite lemma x a c | lemma x b c = silly x a b (++-injectiveˡ (a ++ x ∷ []) (b ++ x ∷ []) c p)

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


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

open import lib.Basics
open import lib.NType2
open import lib.types.Bool
open import lib.types.Empty
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Sigma

{-
This file contains various lemmas that rely on lib.types.Paths or
functional extensionality for pointed maps.
-}

module lib.types.Pointed where

{- Pointed maps -}

⊙app= : ∀ {i j} {X : Ptd i} {Y : Ptd j} {f g : X ⊙→ Y}
  → f == g → f ⊙∼ g
⊙app= {X = X} {Y = Y} p =
  app= (fst= p) , ↓-ap-in (_== pt Y) (λ u → u (pt X)) (snd= p)

-- function extensionality for pointed maps
⊙λ= : ∀ {i j} {X : Ptd i} {Y : Ptd j} {f g : X ⊙→ Y}
  → f ⊙∼ g → f == g
⊙λ= {g = g} (p , α) = pair= (λ= p)
  (↓-app=cst-in (↓-idf=cst-out α ∙ ap (_∙ snd g) (! (app=-β p _))))

⊙λ=' : ∀ {i j} {X : Ptd i} {Y : Ptd j} {f g : X ⊙→ Y}
  (p : fst f ∼ fst g)
  (α : snd f == snd g [ (λ y → y == pt Y) ↓ p (pt X) ])
  → f == g
⊙λ=' {g = g} = curry ⊙λ=

-- associativity of pointed maps
⊙∘-assoc-pt : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  {a₁ a₂ : A} (f : A → B) {b : B} (g : B → C) {c : C}
  (p : a₁ == a₂) (q : f a₂ == b) (r : g b == c)
  → ⊙∘-pt (g ∘ f) p (⊙∘-pt g q r) == ⊙∘-pt g (⊙∘-pt f p q) r
⊙∘-assoc-pt _ _ idp _ _ = idp

⊙∘-assoc : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (h : Z ⊙→ W) (g : Y ⊙→ Z) (f : X ⊙→ Y)
  → ((h ⊙∘ g) ⊙∘ f) ⊙∼ (h ⊙∘ (g ⊙∘ f))
⊙∘-assoc (h , hpt) (g , gpt) (f , fpt) = (λ _ → idp) , ⊙∘-assoc-pt g h fpt gpt hpt

⊙∘-cst-l : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → (f : X ⊙→ Y) → (⊙cst :> (Y ⊙→ Z)) ⊙∘ f ⊙∼ ⊙cst
⊙∘-cst-l {Z = Z} f = (λ _ → idp) , ap (_∙ idp) (ap-cst (pt Z) (snd f))

⊙∘-cst-r : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → (f : Y ⊙→ Z) → f ⊙∘ (⊙cst :> (X ⊙→ Y)) ⊙∼ ⊙cst
⊙∘-cst-r {X = X} f = (λ _ → snd f) , ↓-idf=cst-in' idp

{- Pointed equivalences -}

-- Extracting data from an pointed equivalence
module _ {i j} {X : Ptd i} {Y : Ptd j} (⊙e : X ⊙≃ Y) where

  ⊙≃-to-≃ : de⊙ X ≃ de⊙ Y
  ⊙≃-to-≃ = fst (fst ⊙e) , snd ⊙e

  ⊙–> : X ⊙→ Y
  ⊙–> = fst ⊙e

  ⊙–>-pt = snd ⊙–>

  ⊙<– : Y ⊙→ X
  ⊙<– = is-equiv.g (snd ⊙e) , lemma ⊙e where
    lemma : {Y : Ptd j} (⊙e : X ⊙≃ Y) → is-equiv.g (snd ⊙e) (pt Y) == pt X
    lemma ((f , idp) , f-ise) = is-equiv.g-f f-ise (pt X)

  ⊙<–-pt = snd ⊙<–

  infix 120 _⊙⁻¹
  _⊙⁻¹ : Y ⊙≃ X
  _⊙⁻¹ = ⊙<– , is-equiv-inverse (snd ⊙e)

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  ⊙<–-inv-l : (⊙e : X ⊙≃ Y) → ⊙<– ⊙e ⊙∘ ⊙–> ⊙e ⊙∼ ⊙idf _
  ⊙<–-inv-l ⊙e = <–-inv-l (⊙≃-to-≃ ⊙e) , ↓-idf=cst-in' (lemma ⊙e) where
    lemma : {Y : Ptd j} (⊙e : X ⊙≃ Y)
      → snd (⊙<– ⊙e ⊙∘ ⊙–> ⊙e) == is-equiv.g-f (snd ⊙e) (pt X)
    lemma ((f , idp) , f-ise) = idp

  ⊙<–-inv-r : (⊙e : X ⊙≃ Y) → ⊙–> ⊙e ⊙∘ ⊙<– ⊙e ⊙∼ ⊙idf _
  ⊙<–-inv-r ⊙e = <–-inv-r (⊙≃-to-≃ ⊙e) , ↓-idf=cst-in' (lemma ⊙e) where
    lemma : {Y : Ptd j} (⊙e : X ⊙≃ Y)
      → snd (⊙–> ⊙e ⊙∘ ⊙<– ⊙e) == is-equiv.f-g (snd ⊙e) (pt Y)
    lemma ((f , idp) , f-ise) = ∙-unit-r _ ∙ is-equiv.adj f-ise (pt X)

module _ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} (⊙e : X ⊙≃ Y) where

  post⊙∘-is-equiv : is-equiv (λ (k : Z ⊙→ X) → ⊙–> ⊙e ⊙∘ k)
  post⊙∘-is-equiv = is-eq (⊙–> ⊙e ⊙∘_) (⊙<– ⊙e ⊙∘_) (to-from ⊙e) (from-to ⊙e) where
    abstract
      to-from : ∀ {Y} (⊙e : X ⊙≃ Y) (k : Z ⊙→ Y) → ⊙–> ⊙e ⊙∘ (⊙<– ⊙e ⊙∘ k) == k
      to-from ((f , idp) , f-ise) (k , k-pt) = ⊙λ=' (f.f-g ∘ k) (↓-idf=cst-in' $ lemma k-pt)
        where
          module f = is-equiv f-ise
          lemma : ∀ {y₀} (k-pt : y₀ == f (pt X))
            → ⊙∘-pt f (⊙∘-pt f.g k-pt (f.g-f _)) idp == f.f-g y₀ ∙' k-pt
          lemma idp = ∙-unit-r _ ∙ f.adj _

      from-to : ∀ {Y} (⊙e : X ⊙≃ Y) (k : Z ⊙→ X) → ⊙<– ⊙e ⊙∘ (⊙–> ⊙e ⊙∘ k) == k
      from-to ((f , idp) , f-ise) (k , idp) = ⊙λ=' (f.g-f ∘ k) $ ↓-idf=cst-in' idp
        where module f = is-equiv f-ise

  post⊙∘-equiv : (Z ⊙→ X) ≃ (Z ⊙→ Y)
  post⊙∘-equiv = _ , post⊙∘-is-equiv

  pre⊙∘-is-equiv : is-equiv (λ (k : Y ⊙→ Z) → k ⊙∘ ⊙–> ⊙e)
  pre⊙∘-is-equiv = is-eq (_⊙∘ ⊙–> ⊙e) (_⊙∘ ⊙<– ⊙e) (to-from ⊙e) (from-to ⊙e) where
    abstract
      to-from : ∀ {Z} (⊙e : X ⊙≃ Y) (k : X ⊙→ Z) → (k ⊙∘ ⊙<– ⊙e) ⊙∘ ⊙–> ⊙e == k
      to-from ((f , idp) , f-ise) (k , idp) = ⊙λ=' (ap k ∘ f.g-f) $ ↓-idf=cst-in' $ ∙-unit-r _
        where module f = is-equiv f-ise

      from-to : ∀ {Z} (⊙e : X ⊙≃ Y) (k : Y ⊙→ Z) → (k ⊙∘ ⊙–> ⊙e) ⊙∘ ⊙<– ⊙e == k
      from-to ((f , idp) , f-ise) (k , idp) = ⊙λ=' (ap k ∘ f.f-g) $ ↓-idf=cst-in' $
        ∙-unit-r _ ∙ ap-∘ k f (f.g-f (pt X)) ∙ ap (ap k) (f.adj (pt X))
        where module f = is-equiv f-ise

  pre⊙∘-equiv : (Y ⊙→ Z) ≃ (X ⊙→ Z)
  pre⊙∘-equiv = _ , pre⊙∘-is-equiv

{- Pointed maps out of bool -}

-- intuition : [f true] is fixed and the only changable part is [f false].

⊙Bool→-to-idf : ∀ {i} {X : Ptd i}
  → ⊙Bool ⊙→ X → de⊙ X
⊙Bool→-to-idf (h , _) = h false

⊙Bool→-equiv-idf : ∀ {i} (X : Ptd i)
  → (⊙Bool ⊙→ X) ≃ de⊙ X
⊙Bool→-equiv-idf {i} X = equiv ⊙Bool→-to-idf g f-g g-f
  where
  g : de⊙ X → ⊙Bool ⊙→ X
  g x = Bool-rec (pt X) x , idp

  abstract
    f-g : ∀ x → ⊙Bool→-to-idf (g x) == x
    f-g x = idp

    g-f : ∀ H → g (⊙Bool→-to-idf H) == H
    g-f (h , hpt) = pair=
      (λ= lemma)
      (↓-app=cst-in $
        idp
          =⟨ ! (!-inv-l hpt) ⟩
        ! hpt ∙ hpt
          =⟨ ! (app=-β lemma true) |in-ctx (λ w → w ∙ hpt) ⟩
        app= (λ= lemma) true ∙ hpt
          =∎)
      where lemma : ∀ b → fst (g (h false)) b == h b
            lemma true = ! hpt
            lemma false = idp

⊙Bool→-equiv-idf-nat : ∀ {i j} {X : Ptd i} {Y : Ptd j} (F : X ⊙→ Y)
  → CommSquareEquiv
      (F ⊙∘_)
      (fst F)
      ⊙Bool→-to-idf
      ⊙Bool→-to-idf
⊙Bool→-equiv-idf-nat F = (comm-sqr λ _ → idp) ,
  snd (⊙Bool→-equiv-idf _) , snd (⊙Bool→-equiv-idf _)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- Some results/examples related to CCS, implemented using the
-- classical definition of bisimilarity
------------------------------------------------------------------------

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

open import Prelude

module Bisimilarity.CCS.Examples.Classical {ℓ} {Name : Type ℓ} where

open import Equality.Propositional
open import Prelude.Size

open import Bisimilarity.CCS.Classical
import Bisimilarity.Classical.Equational-reasoning-instances
open import Equational-reasoning
open import Labelled-transition-system.CCS Name
open import Relation

open import Bisimilarity.Classical CCS

------------------------------------------------------------------------
-- Exercise 6.2.4 from "Enhancements of the bisimulation proof method"
-- by Pous and Sangiorgi

6-2-4 : ∀ {a} → ! ! a ∙ ∼ ! a ∙
6-2-4 {a} = bisimulation-up-to-∼⊆∼ R-is base
  where
  data R : Rel₂ ℓ (Proc ∞) where
    base : R (! ! a ∙ , ! a ∙)

  impossible : ∀ {μ P q} {Q : Type q} →
               ! ! a ∙ [ μ ]⟶ P → μ ≡ τ → Q
  impossible {μ} !!a⟶P μ≡τ = ⊥-elim $ name≢τ
    (name a  ≡⟨ !-only (!-only ·-only) !!a⟶P ⟩
     μ       ≡⟨ μ≡τ ⟩∎
     τ       ∎)

  R-is : Bisimulation-up-to-bisimilarity R
  R-is = ⟪ lr , rl ⟫
    where
    lemma = λ {P : Proc ∞} P∼!a∣∅ →
      ! ! a ∙ ∣ P            ∼⟨ reflexive ∣-cong P∼!a∣∅ ⟩
      ! ! a ∙ ∣ (! a ∙ ∣ ∅)  ∼⟨ reflexive ∣-cong ∣-right-identity ⟩
      ! ! a ∙ ∣ ! a ∙        ∼⟨ 6-1-2 ⟩■
      ! ! a ∙

    lr : ∀ {P P′ Q μ} →
         R (P , Q) → P [ μ ]⟶ P′ →
         ∃ λ Q′ → Q [ μ ]⟶ Q′ ×
                  (Bisimilarity ⊙ R ⊙ Bisimilarity) (P′ , Q′)
    lr {P′ = P′} base !!a⟶P′ = case 6-1-3-2 !!a⟶P′ of λ where
      (inj₂ (μ≡τ , _)) → impossible !!a⟶P′ μ≡τ
      (inj₁ (P″ , !a⟶P″ , P′∼!!a∣P″)) → case 6-1-3-2 !a⟶P″ of λ where
        (inj₂ (μ≡τ , _)) → impossible !!a⟶P′ μ≡τ
        (inj₁ (.∅ , action , P″∼!a∣∅)) →
            _
          , (! a ∙      [ name a ]⟶⟨ replication (par-right action) ⟩
             ! a ∙ ∣ ∅)
          , _
          , (P′            ∼⟨ P′∼!!a∣P″ ⟩
             ! ! a ∙ ∣ P″  ∼⟨ ∼: lemma P″∼!a∣∅ ⟩■
             ! ! a ∙)
          , _
          , base
          , (! a ∙      ∼⟨ symmetric ∣-right-identity ⟩■
             ! a ∙ ∣ ∅)

    rl : ∀ {P Q Q′ μ} →
         R (P , Q) → Q [ μ ]⟶ Q′ →
         ∃ λ P′ → P [ μ ]⟶ P′ ×
                  (Bisimilarity ⊙ R ⊙ Bisimilarity) (P′ , Q′)
    rl {Q′ = Q′} base !a⟶Q′ = case 6-1-3-2 !a⟶Q′ of λ where
      (inj₂ (refl , .∅ , Q″ , .a , action , a⟶Q″ , _)) →
        ⊥-elim (names-are-not-inverted a⟶Q″)
      (inj₁ (.∅ , action , Q′∼!a∣∅)) →
          _
        , (! ! a ∙       [ name a ]⟶⟨ replication (par-right !a⟶Q′) ⟩
           ! ! a ∙ ∣ Q′)
        , _
        , (! ! a ∙ ∣ Q′  ∼⟨ lemma Q′∼!a∣∅ ⟩■
           ! ! a ∙)
        , _
        , base
        , (! a ∙      ∼⟨ symmetric ∣-right-identity ⟩
           ! a ∙ ∣ ∅  ∼⟨ symmetric Q′∼!a∣∅ ⟩■
           Q′)

------------------------------------------------------------------------
-- A result mentioned in "Enhancements of the bisimulation proof
-- method" by Pous and Sangiorgi

∙∣∙∼∙∙ : ∀ {a} → a ∙ ∣ a ∙ ∼ name a ∙ (a ∙)
∙∣∙∼∙∙ {a} = bisimulation-up-to-∪⊆∼ R-is base
  where
  data R : Rel₂ ℓ (Proc ∞) where
    base : R (a ∙ ∣ a ∙ , name a ∙ (a ∙))

  R-is : Bisimulation-up-to-∪ R
  R-is = ⟪ lr , rl ⟫
    where
    lr : ∀ {P P′ Q μ} →
         R (P , Q) → P [ μ ]⟶ P′ →
         ∃ λ Q′ → Q [ μ ]⟶ Q′ × (R ∪ Bisimilarity) (P′ , Q′)
    lr base (par-left action) =
        _
      , (name a ∙ (a ∙)  [ name a ]⟶⟨ action ⟩
         a ∙)
      , inj₂ (∅ ∣ a ∙  ∼⟨ ∣-left-identity ⟩■
              a ∙)

    lr base (par-right action) =
        _
      , (name a ∙ (a ∙)  [ name a ]⟶⟨ action ⟩
         a ∙)
      , inj₂ (a ∙ ∣ ∅  ∼⟨ ∣-right-identity ⟩■
              a ∙)

    lr base (par-τ action tr) = ⊥-elim (names-are-not-inverted tr)

    rl : ∀ {P Q Q′ μ} →
         R (P , Q) → Q [ μ ]⟶ Q′ →
         ∃ λ P′ → P [ μ ]⟶ P′ × (R ∪ Bisimilarity) (P′ , Q′)
    rl base action =
        _
      , (a ∙ ∣ a ∙  [ name a ]⟶⟨ par-right action ⟩
         a ∙ ∣ ∅)
      , inj₂ (a ∙ ∣ ∅  ∼⟨ ∣-right-identity ⟩■
              a ∙)

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


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

-- Bundled version of a Cocartesian Category
module Categories.Category.Cocartesian.Bundle where

open import Level

open import Categories.Category.Core using (Category)
open import Categories.Category.Cocartesian using (Cocartesian)
-- open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
-- open import Categories.Category.Monoidal using (MonoidalCategory)

record CocartesianCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    U           : Category o ℓ e  -- U for underlying
    cocartesian : Cocartesian U

  open Category U public
  open Cocartesian cocartesian public
{-
  monoidalCategory : MonoidalCategory o ℓ e
  monoidalCategory = record
    { U        = U
    ; monoidal = CocartesianMonoidal.monoidal cocartesian
    }
-}

max_stars_repo_name: sstucki/agda-categories

max_issues_repo_name: sstucki/agda-categories

max_forks_repo_name: sstucki/agda-categories


text:
module integer7 where

import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_; refl; cong; sym)
open import Data.Nat

-- Int
data Int : Set where
  O : Int
  I : ℕ → ℕ → Int
postulate
  zeroZ : (x : ℕ) → I x x ≡ O
-- plusInt
_++_ : Int → Int → Int
O ++ O = O
O ++ X = X
X ++ O = X
I x y ++ I z w = I (x + z) (y + w)
postulate
  ++Assoc : (X Y Z : Int) → (X ++ Y) ++ Z ≡ X ++ (Y ++ Z)
  ++Comm : (X Y : Int) → X ++ Y ≡ Y ++ X
-- productInt
_**_ : Int → Int → Int
O ** O = O
O ** _ = O
_ ** O = O
I x y ** I z w = I (x * z + y * w) (x * w + y * z)
postulate
  **Assoc : (X Y Z : Int) → (X ** Y) ** Z ≡ X ** (Y ** Z)
  **Dist : (X Y Z : Int) → X ** (Y ++ Z) ≡ (X ** Y) ++ (X ** Z)

-- (-1) ** (-1) = 1
minus1 : I 0 1 ** I 0 1 ≡ I 1 0
minus1 = refl
-1+1 : I 0 1 ++ I 1 0 ≡ I 1 1
-1+1 = refl
-1*1 : I 0 1 ** I 1 0 ≡ I 0 1
-1*1 = refl
minus2 : I 0 1 ** I 0 1 ≡ I 1 0
minus2 = begin
    I 0 1 ** I 0 1
  ≡⟨ refl ⟩
    (I 0 1 ** I 0 1) ++ O
  ≡⟨ sym (cong (\ x → (I 0 1 ** I 0 1) ++ x) (zeroZ 1)) ⟩
    (I 0 1 ** I 0 1) ++ (I 1 1)
  ≡⟨ sym (cong (\ x → (I 0 1 ** I 0 1) ++ x) -1+1) ⟩
    (I 0 1 ** I 0 1) ++ (I 0 1 ++ I 1 0)
  ≡⟨ sym (++Assoc O O (I (suc (suc zero)) (suc zero))) ⟩
    ((I 0 1 ** I 0 1) ++ I 0 1) ++ I 1 0
  ≡⟨ sym (cong (\ x → ((I 0 1 ** I 0 1) ++ x) ++ I 1 0) -1*1) ⟩
    ((I 0 1 ** I 0 1) ++ (I 0 1 ** I 1 0)) ++ I 1 0
  ≡⟨ sym (cong (\ x → x ++ I 1 0) (**Dist (I 0 1) (I 0 1) (I 1 0))) ⟩
    (I 0 1 ** (I 0 1 ++ I 1 0)) ++ I 1 0
  ≡⟨ refl ⟩
    (I 0 1 ** I 1 1) ++ I 1 0
  ≡⟨ cong (\ x → ((I 0 1 ** x) ++ I 1 0)) (zeroZ 1) ⟩
    (I 0 1 ** O) ++ I 1 0
  ≡⟨ refl ⟩
    O ++ I 1 0
  ≡⟨ refl ⟩
    I 1 0
  ∎
  where open PropEq.≡-Reasoning


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

open import Agda.Primitive
open import Prelude
import GSeTT.Syntax
import GSeTT.Rules
open import GSeTT.Typed-Syntax
import Globular-TT.Syntax

module Globular-TT.Rules {l} (index : Set l) (rule : index → GSeTT.Typed-Syntax.Ctx × (Globular-TT.Syntax.Pre-Ty index)) where
  open import Globular-TT.Syntax index

  {- Notational shortcuts : the context corresponding to an index -}
  Ci : index → Pre-Ctx
  Ci i = GPre-Ctx (fst (fst (rule i)))

  Ti : index → Pre-Ty
  Ti i = snd (rule i)

  data _⊢C : Pre-Ctx → Set (lsuc l)
  data _⊢T_ : Pre-Ctx → Pre-Ty → Set (lsuc l)
  data _⊢t_#_ : Pre-Ctx → Pre-Tm → Pre-Ty → Set (lsuc l)
  data _⊢S_>_ : Pre-Ctx → Pre-Sub → Pre-Ctx → Set (lsuc l)

  data _⊢C where
    ec : ⊘ ⊢C
    cc : ∀ {Γ A x} → Γ ⊢C → Γ ⊢T A → x == C-length Γ → (Γ ∙ x # A) ⊢C

  data _⊢T_ where
    ob : ∀ {Γ} → Γ ⊢C → Γ ⊢T ∗
    ar : ∀ {Γ A t u} → Γ ⊢T A → Γ ⊢t t # A → Γ ⊢t u # A → Γ ⊢T ⇒ A t u

  data _⊢t_#_ where
    var : ∀ {Γ x A} → Γ ⊢C → x # A ∈ Γ → Γ ⊢t (Var x) # A
    tm : ∀ {Δ γ A i} → Ci i ⊢T Ti i → Δ ⊢S γ > Ci i → (A == (Ti i [ γ ]Pre-Ty)) → Δ ⊢t Tm-constructor i γ # A

  data _⊢S_>_ where
    es : ∀ {Δ} → Δ ⊢C → Δ ⊢S <> > ⊘
    sc : ∀ {Δ Γ γ x y A t} → Δ ⊢S γ > Γ → (Γ ∙ x # A) ⊢C → (Δ ⊢t t # (A [ γ ]Pre-Ty)) → x == y → Δ ⊢S < γ , y ↦ t > > (Γ ∙ x # A)

  {- Derivability is preserved by the translation from GSeTT to our TT -}
  x∈GCtx : ∀ {x A Γ} → x GSeTT.Syntax.# A ∈ Γ → x # GPre-Ty A ∈ GPre-Ctx Γ
  x∈GCtx {Γ = Γ :: a} (inl x∈Γ) = inl (x∈GCtx x∈Γ)
  x∈GCtx {Γ = Γ :: (x,A)} (inr (idp , idp)) = inr (idp , idp)

  G-length : ∀ Γ → length Γ == C-length (GPre-Ctx Γ)
  G-length nil = idp
  G-length (Γ :: _) = S= (G-length Γ)

  GCtx : ∀ (Γ : GSeTT.Syntax.Pre-Ctx) → Γ GSeTT.Rules.⊢C → (GPre-Ctx Γ) ⊢C
  GTy : ∀ (Γ : GSeTT.Syntax.Pre-Ctx) (A : GSeTT.Syntax.Pre-Ty) → Γ GSeTT.Rules.⊢T A → (GPre-Ctx Γ) ⊢T (GPre-Ty A)
  GTm : ∀ (Γ : GSeTT.Syntax.Pre-Ctx) (A : GSeTT.Syntax.Pre-Ty) (t : GSeTT.Syntax.Pre-Tm) → Γ GSeTT.Rules.⊢t t # A  → (GPre-Ctx Γ) ⊢t (GPre-Tm t) # (GPre-Ty A)

  GCtx .nil GSeTT.Rules.ec = ec
  GCtx (Γ :: (.(length Γ) , A)) (GSeTT.Rules.cc Γ⊢ Γ⊢A idp) = coe (ap (λ n → (GPre-Ctx (Γ :: (n , A)) ⊢C)) (G-length Γ) ^) (cc (GCtx Γ Γ⊢) (GTy Γ A Γ⊢A) idp)
  GTy Γ .GSeTT.Syntax.∗ (GSeTT.Rules.ob Γ⊢) = ob (GCtx Γ Γ⊢)
  GTy Γ (GSeTT.Syntax.⇒ A t u) (GSeTT.Rules.ar Γ⊢t:A Γ⊢u:A) = ar (GTy Γ A (GSeTT.Rules.Γ⊢t:A→Γ⊢A Γ⊢t:A)) (GTm Γ A t Γ⊢t:A) (GTm Γ A u Γ⊢u:A)
  GTm Γ A (GSeTT.Syntax.Var x) (GSeTT.Rules.var Γ⊢ x∈Γ) = var (GCtx Γ Γ⊢) (x∈GCtx x∈Γ)

  {- Properties of the type theory -}
  {- weakening admissibility -}
  wkT : ∀ {Γ A y B} → Γ ⊢T A → (Γ ∙ y # B) ⊢C → (Γ ∙ y # B) ⊢T A
  wkt : ∀ {Γ A t y B} → Γ ⊢t t # A → (Γ ∙ y # B) ⊢C → (Γ ∙ y # B) ⊢t t # A
  wkS : ∀ {Δ Γ γ y B} → Δ ⊢S γ > Γ → (Δ ∙ y # B) ⊢C → (Δ ∙ y # B) ⊢S γ > Γ

  wkT (ob _) Γ,y:B⊢ = ob Γ,y:B⊢
  wkT (ar Γ⊢A Γ⊢t:A Γ⊢u:A) Γ,y:B⊢ = ar (wkT Γ⊢A Γ,y:B⊢) (wkt Γ⊢t:A Γ,y:B⊢) (wkt Γ⊢u:A Γ,y:B⊢)
  wkt (var Γ⊢C x∈Γ) Γ,y:B⊢ = var Γ,y:B⊢ (inl x∈Γ)
  wkt (tm Ci⊢Ti Γ⊢γ:Δ idp) Γ,y:B⊢ = tm Ci⊢Ti (wkS Γ⊢γ:Δ Γ,y:B⊢) idp
  wkS (es _) Δ,y:B⊢ = es Δ,y:B⊢
  wkS (sc Δ⊢γ:Γ Γ,x:A⊢ Δ⊢t:A[γ] idp) Δ,y:B⊢ = sc (wkS Δ⊢γ:Γ Δ,y:B⊢) Γ,x:A⊢ (wkt Δ⊢t:A[γ] Δ,y:B⊢) idp

  {- Consistency : all objects appearing in derivable judgments are derivable -}
  Γ⊢A→Γ⊢ : ∀ {Γ A} → Γ ⊢T A → Γ ⊢C
  Γ⊢t:A→Γ⊢ : ∀ {Γ A t} → Γ ⊢t t # A → Γ ⊢C
  Δ⊢γ:Γ→Δ⊢ : ∀ {Δ Γ γ} → Δ ⊢S γ > Γ → Δ ⊢C

  Γ⊢A→Γ⊢ (ob Γ⊢) = Γ⊢
  Γ⊢A→Γ⊢ (ar Γ⊢A Γ⊢t:A Γ⊢u:A) = Γ⊢t:A→Γ⊢ Γ⊢t:A
  Γ⊢t:A→Γ⊢ (var Γ⊢ _) = Γ⊢
  Γ⊢t:A→Γ⊢ (tm _ Γ⊢γ:Δ idp) = Δ⊢γ:Γ→Δ⊢ Γ⊢γ:Δ
  Δ⊢γ:Γ→Δ⊢ (es Δ⊢) = Δ⊢
  Δ⊢γ:Γ→Δ⊢ (sc Δ⊢γ:Γ Γ,x:A⊢ Δ⊢t:A[γ] idp) = Δ⊢γ:Γ→Δ⊢ Δ⊢γ:Γ

  Δ⊢γ:Γ→Γ⊢ : ∀ {Δ Γ γ} → Δ ⊢S γ > Γ → Γ ⊢C
  Δ⊢γ:Γ→Γ⊢ (es Δ⊢) = ec
  Δ⊢γ:Γ→Γ⊢ (sc Δ⊢γ:Γ Γ,x:A⊢ Δ⊢t:A[γ] idp) = Γ,x:A⊢

  Γ,x:A⊢→Γ,x:A⊢A : ∀ {Γ x A} → (Γ ∙ x # A) ⊢C → (Γ ∙ x # A) ⊢T A
  Γ,x:A⊢→Γ,x:A⊢A Γ,x:A⊢@(cc Γ⊢ Γ⊢A idp) = wkT Γ⊢A Γ,x:A⊢

  Γ,x:A⊢→Γ,x:A⊢x:A : ∀ {Γ x A} → (Γ ∙ x # A) ⊢C → (Γ ∙ x # A) ⊢t (Var x) # A
  Γ,x:A⊢→Γ,x:A⊢x:A Γ,x:A⊢ = var Γ,x:A⊢ (inr (idp , idp))

  Γ⊢src : ∀ {Γ A t u} → Γ ⊢T ⇒ A t u → Γ ⊢t t # A
  Γ⊢src (ar Γ⊢ Γ⊢t Γ⊢u) = Γ⊢t

  Γ⊢tgt : ∀ {Γ A t u} → Γ ⊢T ⇒ A t u → Γ ⊢t u # A
  Γ⊢tgt (ar Γ⊢ Γ⊢t Γ⊢u) = Γ⊢u

  -- The proposition Γ⊢t:A→Γ⊢A is slightly harder and is moved in CwF-Struture since it depends on lemmas there

  -- Type epressing that the rules are well-founded (useful to show that judgments are decidable)
  well-founded : Set (lsuc l)
  well-founded = ∀ (i : index) → Ci i ⊢T Ti i → dimC (Ci i) ≤ dim (Ti i)

  -- Derivation of a term constructed by a term constructor
  Γ⊢tm→Ci⊢Ti : ∀ {i Γ γ A} → Γ ⊢t (Tm-constructor i γ) # A → Ci i ⊢T Ti i
  Γ⊢tm→Ci⊢Ti (tm Ci⊢Ti _ idp) = Ci⊢Ti

  Γ⊢tm→Γ⊢γ : ∀ {i Γ γ A} → Γ ⊢t (Tm-constructor i γ) # A → Γ ⊢S γ > Ci i
  Γ⊢tm→Γ⊢γ (tm _ Γ⊢γ idp) = Γ⊢γ

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


text:
import      Lvl
open import Structure.Operator.Ring
open import Structure.Setoid
open import Type

module Structure.Operator.Ring.Characteristic {ℓ ℓₑ} {T : Type{ℓ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ (_+_ _⋅_  : T → T → T) ⦃ ring : Ring(_+_)(_⋅_) ⦄ where
open Ring(ring)

open import Function.Iteration
open import Numeral.Natural as ℕ using (ℕ)
import      Numeral.Natural.Relation.Order as ℕ
open import Relator.Equals using () renaming (_≡_ to _≡ₑ_)

CharacteristicMultiple : ℕ → Type
CharacteristicMultiple(n) = ∀{a} → (repeatᵣ(n)(_+_) a 𝟎 ≡ 𝟎)

data Characteristic : ℕ → Type{ℓ Lvl.⊔ ℓₑ} where
  none : (∀{n} → CharacteristicMultiple(n) → (n ≡ₑ ℕ.𝟎)) → Characteristic(ℕ.𝟎)
  pos  : ∀{n} → CharacteristicMultiple(ℕ.𝐒(n)) → (∀{m} → CharacteristicMultiple(ℕ.𝐒(m)) → (ℕ.𝐒(m) ℕ.≥ ℕ.𝐒(n))) → Characteristic(ℕ.𝐒(n))

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:
------------------------------------------------------------------------
-- The syntax of, and a type system for, the untyped λ-calculus with
-- constants
------------------------------------------------------------------------

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

module Lambda.Syntax where

open import Equality.Propositional
open import Prelude
open import Prelude.Size

open import Maybe equality-with-J
open import Vec.Function equality-with-J

------------------------------------------------------------------------
-- Terms

-- Variables are represented using de Bruijn indices.

infixl 9 _·_

data Tm (n : ℕ) : Type where
  con : (i : ℕ) → Tm n
  var : (x : Fin n) → Tm n
  ƛ   : Tm (suc n) → Tm n
  _·_ : Tm n → Tm n → Tm n

------------------------------------------------------------------------
-- Closure-based definition of values

-- Environments and values. Defined in a module parametrised by the
-- type of terms.

module Closure (Tm : ℕ → Type) where

  mutual

    -- Environments.

    Env : ℕ → Type
    Env n = Vec Value n

    -- Values. Lambdas are represented using closures, so values do
    -- not contain any free variables.

    data Value : Type where
      con : (i : ℕ) → Value
      ƛ   : ∀ {n} (t : Tm (suc n)) (ρ : Env n) → Value

------------------------------------------------------------------------
-- Type system

-- Recursive, simple types, defined coinductively.

infixr 8 _⇾_

mutual

  data Ty (i : Size) : Type where
    nat : Ty i
    _⇾_ : (σ τ : ∞Ty i) → Ty i

  record ∞Ty (i : Size) : Type where
    coinductive
    field
      force : {j : Size< i} → Ty j

open ∞Ty public

-- A conversion function.

[_] : Ty ∞ → ∞Ty ∞
[ σ ] .force = σ

-- Contexts.

Ctxt : ℕ → Type
Ctxt n = Vec (Ty ∞) n

-- Type system.

infix 4 _⊢_∈_

data _⊢_∈_ {n} (Γ : Ctxt n) : Tm n → Ty ∞ → Type where
  con : ∀ {i} → Γ ⊢ con i ∈ nat
  var : ∀ {x} → Γ ⊢ var x ∈ Γ x
  ƛ   : ∀ {t σ τ} →
        cons (force σ) Γ ⊢ t ∈ force τ → Γ ⊢ ƛ t ∈ σ ⇾ τ
  _·_ : ∀ {t₁ t₂ σ τ} →
        Γ ⊢ t₁ ∈ σ ⇾ τ → Γ ⊢ t₂ ∈ force σ →
        Γ ⊢ t₁ · t₂ ∈ force τ

------------------------------------------------------------------------
-- Some definitions used in several type soundness proofs

open Closure Tm

-- WF-Value, WF-Env and WF-MV specify when a
-- value/environment/potential value is well-formed with respect to a
-- given context (and type).

mutual

  data WF-Value : Ty ∞ → Value → Type where
    con : ∀ {i} → WF-Value nat (con i)
    ƛ   : ∀ {n Γ σ τ} {t : Tm (1 + n)} {ρ} →
          cons (force σ) Γ ⊢ t ∈ force τ →
          WF-Env Γ ρ →
          WF-Value (σ ⇾ τ) (ƛ t ρ)

  WF-Env : ∀ {n} → Ctxt n → Env n → Type
  WF-Env Γ ρ = ∀ x → WF-Value (Γ x) (ρ x)

WF-MV : Ty ∞ → Maybe Value → Type
WF-MV σ v = maybe (WF-Value σ) Prelude.⊥ v

-- Some "constructors" for WF-Env.

nil-wf : WF-Env nil nil
nil-wf ()

cons-wf : ∀ {n} {Γ : Ctxt n} {ρ σ v} →
          WF-Value σ v → WF-Env Γ ρ → WF-Env (cons σ Γ) (cons v ρ)
cons-wf v-wf ρ-wf fzero    = v-wf
cons-wf v-wf ρ-wf (fsuc x) = ρ-wf x

------------------------------------------------------------------------
-- Examples

-- A non-terminating term.

ω : Tm 0
ω = ƛ (var fzero · var fzero)

Ω : Tm 0
Ω = ω · ω

-- Ω is well-typed.

Ω-well-typed : (τ : Ty ∞) → nil ⊢ Ω ∈ τ
Ω-well-typed τ =
  _·_ {σ = σ} {τ = [ τ ]} (ƛ (var · var)) (ƛ (var · var))
  where
  σ : ∀ {i} → ∞Ty i
  σ .force = σ ⇾ [ τ ]

-- A call-by-value fixpoint combinator.

Z : Tm 0
Z = ƛ (t · t)
  where
  t = ƛ (var (fsuc fzero) ·
         ƛ (var (fsuc fzero) · var (fsuc fzero) · var fzero))

-- This combinator is also well-typed.

Z-well-typed :
  ∀ {σ τ} →
  nil ⊢ Z ∈ [ [ [ σ ] ⇾ [ τ ] ] ⇾ [ [ σ ] ⇾ [ τ ] ] ] ⇾
            [ [ σ ] ⇾ [ τ ] ]
Z-well-typed {σ = σ} {τ = τ} =
  ƛ (_·_ {σ = υ} {τ = [ _ ]}
         (ƛ (var · ƛ (var · var · var)))
         (ƛ (var · ƛ (var · var · var))))
  where
  υ : ∀ {i} → ∞Ty i
  force υ = υ ⇾ [ [ σ ] ⇾ [ τ ] ]

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module Plylet where

open import Data.String.Base
open import Data.Char.Base
open import Data.List.Base

data Type : Set where
  -- The type of the unit value
  TUnit : Type
  -- The type constructor for functions →
  TFunc : Type -> Type -> Type
  -- A type loaded from the prelude
  TBuiltin : String -> Type

data Term : Set where
  -- The value of unit
  VUnit : Term
  -- An well-typed application is a valid term
  VApp : Term → Term → Term
  -- A well-formed let expression is a valid term
  VLet : Char -> Term -> Term -> Term
  -- A function from the prelude
  VFunc : String -> Term

data Judgment : Set where
  -- A typing judgment
  TypeJ : Term → Type → Judgment
  -- A coercion validity judgment
  CoerceJ : Type → Type → Judgment

Gamma : Set
Gamma = List Judgment

baseEnv : Gamma
baseEnv =
  TypeJ VUnit TUnit
  ∷ []

max_stars_repo_name: Kazark/plylet

max_issues_repo_name: Kazark/plylet

max_forks_repo_name: Kazark/plylet


text:
------------------------------------------------------------------------------
--  Properties related with lists (using induction on the FOTC lists type)
------------------------------------------------------------------------------

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

module FOTC.Data.List.PropertiesByInductionATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.List
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------
-- Totality properties

-- See Issue https://github.com/asr/apia/issues/81 .
lengthList-NA : D → Set
lengthList-NA ds = N (length ds)
{-# ATP definition lengthList-NA #-}

lengthList-N : ∀ {xs} → List xs → N (length xs)
lengthList-N = List-ind lengthList-NA A[] h
  where
  postulate A[] : lengthList-NA []
  {-# ATP prove A[] #-}

  postulate h : ∀ a {as} → lengthList-NA as → lengthList-NA (a ∷ as)
  {-# ATP prove h #-}

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

-- See Issue https://github.com/asr/apia/issues/81 .
++-assocA : D → D → D → Set
++-assocA ys zs as = (as ++ ys) ++ zs ≡ as ++ ys ++ zs
{-# ATP definition ++-assocA #-}

++-assoc : ∀ {xs} → List xs → ∀ ys zs → (xs ++ ys) ++ zs ≡ xs ++ ys ++ zs
++-assoc Lxs ys zs = List-ind (++-assocA ys zs) A[] h Lxs
  where
  postulate A[] : ++-assocA ys zs []
  {-# ATP prove A[] #-}

  postulate h : ∀ a {as} → ++-assocA ys zs as → ++-assocA ys zs (a ∷ as)
  {-# ATP prove h #-}


text:
module Implicits.Resolution.Infinite.NormalFormEquiv where

open import Prelude

open import Implicits.Syntax
open import Implicits.Resolution.Infinite.Resolution
open import Implicits.Resolution.Embedding
open import Implicits.Resolution.Embedding.Lemmas

open import SystemF.Everything as F using ()
open import SystemF.NormalForm

open import Data.Vec hiding ([_])
open import Relation.Binary.HeterogeneousEquality as H using ()
open import Data.List.Any
open import Data.List.Properties
open import Data.Vec.Properties as VP using ()
open import Extensions.Vec
open import Function.Equivalence using (_⇔_; equivalence)

mutual

  from-⇓ : ∀ {ν n t a τ} {Γ : F.Ctx ν n} → Γ ⊢ t ⇓ a → ⟦ Γ ⟧ctx← ⊢ ⟦ a ⟧tp← ↓ τ →
           ∃ λ i → ⟦ Γ ⟧ctx← ⊢ ⟦ lookup i Γ ⟧tp← ↓ τ
  from-⇓ {Γ = Γ} (nvar i) ↓τ = i , ↓τ
  from-⇓ (napp p x) ↓τ = from-⇓ p (i-iabs (from-⇑ x) ↓τ)
  from-⇓ {Γ = Γ} (ntapp {a = a} b p) ↓τ = from-⇓ p
    (i-tabs ⟦ b ⟧tp← (subst (λ z → ⟦ Γ ⟧ctx← ⊢ z ↓ _) (⟦a/sub⟧tp← a b) ↓τ))

  from-⇑ : ∀ {ν n t a} {Γ : F.Ctx ν n} → Γ ⊢ t ⇑ a → ⟦ Γ ⟧ctx← ⊢ᵣ ⟦ a ⟧tp←
  from-⇑ (nbase b x) with ⟦base⟧tp← b
  from-⇑ (nbase b x) | τ , eq with from-⇓ x (subst (λ z → _ ⊢ z ↓ τ) (sym $ eq) (i-simp τ))
  from-⇑ (nbase b x) | τ , eq | i , lookup-i↓tc =
    subst (λ z → _ ⊢ᵣ z) (sym $ eq) (r-simp (lookup-∈ i _) lookup-i↓tc)
  from-⇑ (nabs p) = r-iabs (from-⇑ p)
  from-⇑ (ntabs p) = r-tabs (subst (λ z → z ⊢ᵣ _) (⟦weaken⟧ctx← _) (from-⇑ p))

  to-⇓ : ∀ {ν} {Δ : ICtx ν} {a τ t₁} → Δ ⊢ a ↓ τ → ⟦ Δ ⟧ctx→ ⊢ t₁ ⇓ ⟦ a ⟧tp→ →
        ∃ λ t₂ → ⟦ Δ ⟧ctx→ ⊢ t₂ ⇓ ⟦ simpl τ ⟧tp→
  to-⇓ (i-simp a) q = , q
  to-⇓ (i-iabs x p) q = to-⇓ p (napp q (proj₂ $ to-⇑ x))
  to-⇓ {Δ = Δ} (i-tabs {ρ = a} b p) q =
    to-⇓ p (subst (λ z → ⟦ Δ ⟧ctx→ ⊢ _ ⇓ z) (sym $ ⟦a/sub⟧tp→ a b) (ntapp ⟦ b ⟧tp→ q))

  to-⇑ : ∀ {ν} {Δ : ICtx ν} {a} → Δ ⊢ᵣ a → ∃ λ t → ⟦ Δ ⟧ctx→ ⊢ t ⇑ ⟦ a ⟧tp→
  to-⇑ {Δ = Δ} (r-simp {r = a} r r↓τ) = , nbase (⟦simpl⟧tp→ _) (proj₂ $ to-⇓ r↓τ var⇓a)
    where
      var⇓a : ⟦ Δ ⟧ctx→ ⊢ _ ⇓ ⟦ a ⟧tp→
      var⇓a = let (i , eq) = ∈⟶index (VP.List-∈⇒∈ r) in
        let i' = (subst Fin (sym $ length-map _ Δ) i) in
          subst (λ z → ⟦ Δ ⟧ctx→ ⊢ (F.var i') ⇓ z) (lookup⟦⟧ Δ i eq) (nvar i')
  to-⇑ (r-iabs p) =
    , nabs (proj₂ $ to-⇑ p)
  to-⇑ {Δ = Δ} (r-tabs {ρ = a} p) =
    , ntabs (⇑-subst-n (length-weaken-Δ Δ) (H.sym $ ⟦weaken⟧ctx→ Δ) (proj₂ (to-⇑ p)))

-- System F η-long-β-normal forms are isomorphic to infinite resolution derivations
equivalent : ∀ {ν} (Δ : ICtx ν) r → Δ ⊢ᵣ r ⇔ (∃ λ t → ⟦ Δ ⟧ctx→ ⊢ t ⇑ ⟦ r ⟧tp→)
equivalent Δ r = equivalence
  (λ x → to-⇑ x)
  (λ x → subst₂ (λ Δ' r' → Δ' ⊢ᵣ r') (ctx→← _) (tp→← r) (from-⇑ (proj₂ x)))

{-}
open import Function.Inverse
open import Function.Equality

-- from-⇑ : ∀ {ν n t a} {Γ : F.Ctx ν n} → Γ ⊢ t ⇑ a → ⟦ Γ ⟧ctx← ⊢ᵣ ⟦ a ⟧tp←
from-⇑' : ∀ {ν a} {Δ : ICtx ν} → (∃ λ t → ⟦ Δ ⟧ctx→ ⊢ t ⇑ ⟦ a ⟧tp→) → Δ ⊢ᵣ a
from-⇑' (_ , p) = subst₂ (λ Δ a → Δ ⊢ᵣ a) (ctx→← _) (tp→← _) (from-⇑ p)

-- from-⇓' : ∀ {ν a} {Δ : ICtx ν} {τ} → (∃ λ t → ⟦ Δ ⟧ctx→ ⊢ t ⇓ ⟦ a ⟧tp→) → Δ ⊢ Δ ⊢ a ↓ τ
-- from-⇓' {τ = τ} (_ , p) = subst₂ (λ Δ a → Δ ⊢ a ↓ τ) (ctx→← _) (tp→← _) (from-⇓ p)

-- from-to-⇓ : ∀ {ν a} {Δ : ICtx ν} {τ} → (p : Δ ⊢ a ↓ τ) → from-⇓' (to-⇓ p) ≡ p
-- from-to-⇓ p = ?

from-to-⇑ : ∀ {ν a} {Δ : ICtx ν} → (p : Δ ⊢ᵣ a) → from-⇑' (to-⇑ p) ≡ p
from-to-⇑ (r-simp x x₁) = {!!}
from-to-⇑ (r-iabs p) = begin
  from-⇑' (, (nabs (proj₂ (to-⇑ p))))
    ≡⟨ refl ⟩
  subst₂ (λ Δ a → Δ ⊢ᵣ a) (ctx→← _) (tp→← _) (from-⇑ (nabs (proj₂ (to-⇑ p))))
    ≡⟨ refl ⟩
  subst₂ (λ Δ a → Δ ⊢ᵣ a) (ctx→← _) (tp→← _) (r-iabs (from-⇑ (proj₂ (to-⇑ p))))
    ≡⟨ {!!} ⟩
  r-iabs (subst₂ (λ Δ a → Δ ⊢ᵣ a) (ctx→← _) (tp→← _) (from-⇑ (proj₂ (to-⇑ p))))
    ≡⟨ refl ⟩
  r-iabs (from-⇑' (to-⇑ p))
    ≡⟨ Prelude.cong r-iabs (from-to-⇑ p) ⟩
  r-iabs p ∎
from-to-⇑ (r-tabs p) with from-to-⇑ p
from-to-⇑ (r-tabs p) | x = {!x!}
  where
    lem : ∀ {ν a} {Δ : ICtx ν} →

to-from-⇑ : ∀ {ν a} {Δ : ICtx ν} → (p : ∃ λ t → ⟦ Δ ⟧ctx→ ⊢ t ⇑ ⟦ a ⟧tp→) → to-⇑ (from-⇑' p) ≡ p
to-from-⇑ p = {!!}

iso' : ∀ {ν a} {Δ : ICtx ν} → (→-to-⟶ (to-⇑ {Δ = Δ} {a = a})) InverseOf (→-to-⟶ from-⇑')
iso' = record { left-inverse-of = to-from-⇑; right-inverse-of = from-to-⇑ }
-}


text:
-- Solver for cartesian category
-- Normalisation is based on https://arxiv.org/abs/math/9911059

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

open import Categories.Category
open import Categories.Category.Cartesian

module Experiment.Categories.Solver.Category.Cartesian
  {o ℓ e} {𝒞 : Category o ℓ e} (cartesian : Cartesian 𝒞) where

open import Level
open import Relation.Binary using (Rel; REL)

import Categories.Morphism.Reasoning as MR

open Category 𝒞
open Cartesian cartesian
open HomReasoning
open MR 𝒞

private
  variable
    A B C D E F : Obj

infixr 9 _:∘_
infixr 7 _:×_
infix 11 :⟨_,_⟩

data Sig : Set o where
  ∥_∥  : Obj → Sig
  :⊤   : Sig
  _:×_ : Sig → Sig → Sig

⟦_⟧Sig : Sig → Obj
⟦ ∥ A ∥    ⟧Sig = A
⟦ :⊤       ⟧Sig = ⊤
⟦ S₁ :× S₂ ⟧Sig = ⟦ S₁ ⟧Sig × ⟦ S₂ ⟧Sig

private
  variable
    S T U V : Sig

-- Expression for cartesian category
data Expr : Rel Sig (o ⊔ ℓ) where
  :id    : Expr S S
  _:∘_   : Expr T U → Expr S T → Expr S U
  :π₁    : Expr (S :× T) S
  :π₂    : Expr (S :× T) T
  :⟨_,_⟩ : Expr U S → Expr U T → Expr U (S :× T)
  ∥_∥    : A ⇒ B → Expr ∥ A ∥ ∥ B ∥
  ∥_!∥   : A ⇒ ⊤ → Expr ∥ A ∥ :⊤

-- Atomised expression
data AExpr : REL Sig Obj (o ⊔ ℓ) where
  :π₁   : AExpr (∥ A ∥ :× T) A
  :π₂   : AExpr (S :× ∥ B ∥) B
  _:∘π₁ : AExpr S A → AExpr (S :× T) A
  _:∘π₂ : AExpr T A → AExpr (S :× T) A

-- Normalised expression
data NExpr : Rel Sig (o ⊔ ℓ) where
  :id    : NExpr ∥ A ∥ ∥ A ∥
  :!N    : NExpr S :⊤
  ⟪_⟫    : AExpr S A → NExpr S ∥ A ∥
  :⟨_,_⟩ : NExpr U S → NExpr U T → NExpr U (S :× T)
  ∥_∥∘_  : B ⇒ C → NExpr S ∥ B ∥ → NExpr S ∥ C ∥

-- Semantics
⟦_⟧ : Expr S T → ⟦ S ⟧Sig ⇒ ⟦ T ⟧Sig
⟦ :id          ⟧ = id
⟦ e₁ :∘ e₂     ⟧ = ⟦ e₁ ⟧ ∘ ⟦ e₂ ⟧
⟦ :π₁          ⟧ = π₁
⟦ :π₂          ⟧ = π₂
⟦ :⟨ e₁ , e₂ ⟩ ⟧ = ⟨ ⟦ e₁ ⟧ , ⟦ e₂ ⟧ ⟩
⟦ ∥ f ∥        ⟧ = f
⟦ ∥ g !∥       ⟧ = g

⟦_⟧A : AExpr S B → ⟦ S ⟧Sig ⇒ B
⟦ :π₁      ⟧A = π₁
⟦ :π₂      ⟧A = π₂
⟦ e :∘π₁   ⟧A = ⟦ e ⟧A ∘ π₁
⟦ e :∘π₂   ⟧A = ⟦ e ⟧A ∘ π₂

⟦_⟧N : NExpr S T → ⟦ S ⟧Sig ⇒ ⟦ T ⟧Sig
⟦ :id          ⟧N = id
⟦ :!N          ⟧N = !
⟦ ⟪ e ⟫        ⟧N = ⟦ e ⟧A
⟦ :⟨ e₁ , e₂ ⟩ ⟧N = ⟨ ⟦ e₁ ⟧N , ⟦ e₂ ⟧N ⟩
⟦ ∥ f ∥∘ e     ⟧N = f ∘ ⟦ e ⟧N

_∘AN_ : AExpr T A → NExpr S T → NExpr S ∥ A ∥
:π₁       ∘AN :⟨ e₂ , e₃ ⟩ = e₂
:π₂       ∘AN :⟨ e₂ , e₃ ⟩ = e₃
(e₁ :∘π₁) ∘AN :⟨ e₂ , e₃ ⟩ = e₁ ∘AN e₂
(e₁ :∘π₂) ∘AN :⟨ e₂ , e₃ ⟩ = e₁ ∘AN e₃

_∘π₁N : NExpr S U → NExpr (S :× T) U
:id          ∘π₁N = ⟪ :π₁ ⟫
:!N          ∘π₁N = :!N
⟪ e ⟫        ∘π₁N = ⟪ e :∘π₁ ⟫
:⟨ e₁ , e₂ ⟩ ∘π₁N = :⟨ e₁ ∘π₁N , e₂ ∘π₁N ⟩
(∥ f ∥∘ e)   ∘π₁N = ∥ f ∥∘ (e ∘π₁N)

_∘π₂N : NExpr T U → NExpr (S :× T) U
:id          ∘π₂N = ⟪ :π₂ ⟫
:!N          ∘π₂N = :!N
⟪ e ⟫        ∘π₂N = ⟪ e :∘π₂ ⟫
:⟨ e₁ , e₂ ⟩ ∘π₂N = :⟨ e₁ ∘π₂N , e₂ ∘π₂N ⟩
(∥ f ∥∘ e)   ∘π₂N = ∥ f ∥∘ (e ∘π₂N)

_∘N_ : NExpr T U → NExpr S T → NExpr S U
:id          ∘N e₂ = e₂
:!N          ∘N e₂ = :!N
⟪ e₁ ⟫       ∘N e₂ = e₁ ∘AN e₂
:⟨ e₁ , e₂ ⟩ ∘N e₃ = :⟨ e₁ ∘N e₃ , e₂ ∘N e₃ ⟩
(∥ f ∥∘ e₁)  ∘N e₂ = ∥ f ∥∘ (e₁ ∘N e₂)

π₁N : ∀ S T → NExpr (S :× T) S
π₂N : ∀ S T → NExpr (S :× T) T
π₁N ∥ _ ∥      T = ⟪ :π₁ ⟫
π₁N :⊤         T = :!N
π₁N (S₁ :× S₂) T = :⟨ (π₁N S₁ S₂) ∘π₁N , (π₂N S₁ S₂) ∘π₁N ⟩
π₂N S ∥ _ ∥      = ⟪ :π₂ ⟫
π₂N S :⊤         = :!N
π₂N S (T₁ :× T₂) = :⟨ (π₁N T₁ T₂) ∘π₂N , (π₂N T₁ T₂) ∘π₂N ⟩

idN : ∀ S → NExpr S S
idN ∥ _ ∥    = :id
idN :⊤       = :!N
idN (S :× T) = :⟨ π₁N S T , π₂N S T ⟩

-- expand id, π₁ and π₂
normalise : Expr S T → NExpr S T
normalise :id          = idN _
normalise (e₁ :∘ e₂)   = normalise e₁ ∘N normalise e₂
normalise :π₁          = π₁N _ _
normalise :π₂          = π₂N _ _
normalise :⟨ e₁ , e₂ ⟩ = :⟨ normalise e₁ , normalise e₂ ⟩
normalise ∥ f ∥        = ∥ f ∥∘ :id
normalise ∥ g !∥       = :!N

∘AN-homo : (e₁ : AExpr T A) (e₂ : NExpr S T) → ⟦ e₁ ∘AN e₂ ⟧N ≈ ⟦ e₁ ⟧A ∘ ⟦ e₂ ⟧N
∘AN-homo :π₁       :⟨ e₂ , e₃ ⟩ = ⟺ project₁
∘AN-homo :π₂       :⟨ e₂ , e₃ ⟩ = ⟺ project₂
∘AN-homo (e₁ :∘π₁) :⟨ e₂ , e₃ ⟩ = ∘AN-homo e₁ e₂ ○ pushʳ (⟺ project₁)
∘AN-homo (e₁ :∘π₂) :⟨ e₂ , e₃ ⟩ = ∘AN-homo e₁ e₃ ○ pushʳ (⟺ project₂)

∘N-homo : (e₁ : NExpr T U) (e₂ : NExpr S T) → ⟦ e₁ ∘N e₂ ⟧N ≈ ⟦ e₁ ⟧N ∘ ⟦ e₂ ⟧N
∘N-homo :id          e₂ = ⟺ identityˡ
∘N-homo :!N          e₂ = !-unique _
∘N-homo ⟪ e₁ ⟫       e₂ = ∘AN-homo e₁ e₂
∘N-homo :⟨ e₁ , e₂ ⟩ e₃ = ⟨⟩-cong₂ (∘N-homo e₁ e₃) (∘N-homo e₂ e₃) ○ ⟺ ⟨⟩∘
∘N-homo (∥ f ∥∘ e₁)  e₂ = pushʳ (∘N-homo e₁ e₂)

∘π₁N-homo : ∀ (e : NExpr S U) → ⟦ (_∘π₁N {T = T}) e ⟧N ≈ ⟦ e ⟧N ∘ π₁
∘π₁N-homo :id          = ⟺ identityˡ
∘π₁N-homo :!N          = !-unique _
∘π₁N-homo ⟪ e ⟫        = refl
∘π₁N-homo :⟨ e₁ , e₂ ⟩ = ⟨⟩-cong₂ (∘π₁N-homo e₁) (∘π₁N-homo e₂) ○ ⟺ ⟨⟩∘
∘π₁N-homo (∥ f ∥∘ e)   = pushʳ (∘π₁N-homo e)

∘π₂N-homo : ∀ (e : NExpr T U) → ⟦ (_∘π₂N {S = S}) e ⟧N ≈ ⟦ e ⟧N ∘ π₂
∘π₂N-homo :id          = ⟺ identityˡ
∘π₂N-homo :!N          = !-unique _
∘π₂N-homo ⟪ e ⟫        = refl
∘π₂N-homo :⟨ e₁ , e₂ ⟩ = ⟨⟩-cong₂ (∘π₂N-homo e₁) (∘π₂N-homo e₂) ○ ⟺ ⟨⟩∘
∘π₂N-homo (∥ f ∥∘ e)   = pushʳ (∘π₂N-homo e)

private
  ∘π₁N′ : ∀ S T → NExpr S U → NExpr (S :× T) U
  ∘π₁N′ _ _ = _∘π₁N
  ∘π₂N′ : ∀ S T → NExpr T U → NExpr (S :× T) U
  ∘π₂N′ _ _ = _∘π₂N

π₁N-homo : ∀ S T → ⟦ π₁N S T ⟧N ≈ π₁
π₂N-homo : ∀ S T → ⟦ π₂N S T ⟧N ≈ π₂
π₁N-homo ∥ A ∥      T = refl
π₁N-homo :⊤         T = !-unique _
π₁N-homo (S₁ :× S₂) T = begin
  ⟨ ⟦ ∘π₁N′ (S₁ :× S₂) T (π₁N S₁ S₂) ⟧N , ⟦ ∘π₁N′ (S₁ :× S₂) T (π₂N S₁ S₂) ⟧N ⟩
    ≈⟨ ⟨⟩-cong₂ (∘π₁N-homo (π₁N S₁ S₂)) (∘π₁N-homo (π₂N S₁ S₂)) ⟩
  ⟨ ⟦ π₁N S₁ S₂ ⟧N ∘ π₁ , ⟦ π₂N S₁ S₂ ⟧N ∘ π₁ ⟩
    ≈˘⟨ ⟨⟩∘ ⟩
  ⟨ ⟦ π₁N S₁ S₂ ⟧N , ⟦ π₂N S₁ S₂ ⟧N ⟩ ∘ π₁
    ≈⟨ ⟨⟩-cong₂ (π₁N-homo S₁ S₂) (π₂N-homo S₁ S₂) ⟩∘⟨refl ⟩
  ⟨ π₁ , π₂ ⟩ ∘ π₁
    ≈⟨ elimˡ η ⟩
  π₁
    ∎
π₂N-homo S ∥ A ∥      = refl
π₂N-homo S :⊤         = !-unique _
π₂N-homo S (T₁ :× T₂) = begin
  ⟨ ⟦ ∘π₂N′ S (T₁ :× T₂) (π₁N T₁ T₂) ⟧N , ⟦ ∘π₂N′ S (T₁ :× T₂) (π₂N T₁ T₂) ⟧N ⟩
    ≈⟨ ⟨⟩-cong₂ (∘π₂N-homo (π₁N T₁ T₂)) (∘π₂N-homo (π₂N T₁ T₂)) ⟩
  ⟨ ⟦ π₁N T₁ T₂ ⟧N ∘ π₂ , ⟦ π₂N T₁ T₂ ⟧N ∘ π₂ ⟩
    ≈˘⟨ ⟨⟩∘ ⟩
  ⟨ ⟦ π₁N T₁ T₂ ⟧N , ⟦ π₂N T₁ T₂ ⟧N ⟩ ∘ π₂
    ≈⟨ ⟨⟩-cong₂ (π₁N-homo T₁ T₂) (π₂N-homo T₁ T₂) ⟩∘⟨refl ⟩
  ⟨ π₁ , π₂ ⟩ ∘ π₂
    ≈⟨ elimˡ η ⟩
  π₂
    ∎

idN-homo : ∀ S → ⟦ idN S ⟧N ≈ id
idN-homo ∥ _ ∥      = refl
idN-homo :⊤         = !-unique id
idN-homo (S₁ :× S₂) = ⟨⟩-cong₂ (π₁N-homo S₁ S₂) (π₂N-homo S₁ S₂) ○ η

correct : ∀ (e : Expr S T) → ⟦ normalise e ⟧N ≈ ⟦ e ⟧
correct {S} :id          = idN-homo S
correct (e₁ :∘ e₂)       = begin
  ⟦ normalise e₁ ∘N normalise e₂ ⟧N     ≈⟨ ∘N-homo (normalise e₁) (normalise e₂) ⟩
  ⟦ normalise e₁ ⟧N ∘ ⟦ normalise e₂ ⟧N ≈⟨ correct e₁ ⟩∘⟨ correct e₂ ⟩
  ⟦ e₁ ⟧ ∘ ⟦ e₂ ⟧                       ∎
correct {S :× T} {S} :π₁ = π₁N-homo S T
correct {S :× T} {T} :π₂ = π₂N-homo S T
correct :⟨ e₁ , e₂ ⟩     = ⟨⟩-cong₂ (correct e₁) (correct e₂)
correct ∥ f ∥            = identityʳ
correct ∥ g !∥           = !-unique g

solve : (e₁ e₂ : Expr S T) →
        ⟦ normalise e₁ ⟧N ≈ ⟦ normalise e₂ ⟧N → ⟦ e₁ ⟧ ≈ ⟦ e₂ ⟧
solve e₁ e₂ eq = begin
  ⟦ e₁ ⟧            ≈˘⟨ correct e₁ ⟩
  ⟦ normalise e₁ ⟧N ≈⟨ eq ⟩
  ⟦ normalise e₂ ⟧N ≈⟨ correct e₂ ⟩
  ⟦ e₂ ⟧            ∎

-- Combinators

∥-∥ : ∀ {f : A ⇒ B} → Expr ∥ A ∥ ∥ B ∥
∥-∥ {f = f} = ∥ f ∥

:! : Expr ∥ A ∥ :⊤
:! = ∥ ! !∥

:swap : Expr (S :× T) (T :× S)
:swap = :⟨ :π₂ , :π₁ ⟩

:assocˡ : Expr ((S :× T) :× U) (S :× T :× U)
:assocˡ = :⟨ :π₁ :∘ :π₁ , :⟨ :π₂ :∘ :π₁ , :π₂ ⟩ ⟩

:assocʳ : Expr (S :× T :× U) ((S :× T) :× U)
:assocʳ = :⟨ :⟨ :π₁ , :π₁ :∘ :π₂ ⟩ , :π₂ :∘ :π₂ ⟩

infixr 8 _:⁂_

_:⁂_ : Expr S T → Expr U V → Expr (S :× U) (T :× V)
e₁ :⁂ e₂ = :⟨ e₁ :∘ :π₁ , e₂ :∘ :π₂ ⟩

:first : Expr S T → Expr (S :× U) (T :× U)
:first e = e :⁂ :id

:second : Expr T U → Expr (S :× T) (S :× U)
:second e = :id :⁂ e


text:
open import Oscar.Prelude

module Oscar.Class.[ExtensibleType] where

record [ExtensibleType]
    {𝔵} {𝔛 : Ø 𝔵}
    {𝔟} {𝔒₂ : 𝔛 → Ø 𝔟}
    {ℓ̇} (_↦_ : ∀ {x} → 𝔒₂ x → 𝔒₂ x → Ø ℓ̇)
    : Ø₀ where
  constructor ∁
  no-eta-equality


text:
open import Relation.Binary.Core

module TreeSort.Impl1.Correctness.Permutation  {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import BTree {A}
open import Data.List
open import Data.Sum
open import List.Permutation.Base A
open import List.Permutation.Base.Concatenation A
open import List.Permutation.Base.Equivalence A
open import TreeSort.Impl1 _≤_ tot≤

lemma-++∼ : {x : A}{xs ys : List A} → (x ∷ (xs ++ ys)) ∼ (xs ++ (x ∷ ys))
lemma-++∼ {xs = xs} = ∼x /head (lemma++/l {xs = xs} /head) refl∼

lemma-flatten∼ : (x : A) → (t : BTree) → (x ∷ flatten t) ∼ flatten (insert x t)
lemma-flatten∼ x leaf = ∼x /head /head ∼[]
lemma-flatten∼ x (node y l r)
    with tot≤ x y
... | inj₁ x≤y = lemma++∼r (lemma-flatten∼ x l)
... | inj₂ y≤x = trans∼ (lemma-++∼ {xs = flatten l}) (lemma++∼l {xs = flatten l} (∼x (/tail /head) /head (lemma-flatten∼ x r)))

theorem-treeSort∼ : (xs : List A) → xs ∼ (flatten (treeSort xs))
theorem-treeSort∼ [] = ∼[]
theorem-treeSort∼ (x ∷ xs) = trans∼ (∼x /head /head (theorem-treeSort∼ xs)) (lemma-flatten∼ x (treeSort xs))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic lemmas showing that various types are related (isomorphic or
-- equivalent or…)
------------------------------------------------------------------------

module Function.Related.TypeIsomorphisms where

open import Algebra
import Algebra.FunctionProperties as FP
import Algebra.Operations
import Algebra.RingSolver.Natural-coefficients
open import Algebra.Structures
open import Data.Empty
open import Data.Nat as Nat using (zero; suc)
open import Data.Product as Prod hiding (swap)
open import Data.Sum as Sum
open import Data.Unit
open import Level hiding (zero; suc)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Eq using (_⇔_; module Equivalence)
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Function.Related as Related
open import Relation.Binary
open import Relation.Binary.Product.Pointwise
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
open import Relation.Binary.Sum
open import Relation.Nullary
open import Relation.Nullary.Decidable as Dec using (True)

------------------------------------------------------------------------
-- Σ is "associative"

Σ-assoc : ∀ {a b c}
            {A : Set a} {B : A → Set b} {C : (a : A) → B a → Set c} →
          Σ (Σ A B) (uncurry C) ↔ Σ A (λ a → Σ (B a) (C a))
Σ-assoc = record
  { to         = P.→-to-⟶ λ p →
                   proj₁ (proj₁ p) , (proj₂ (proj₁ p) , proj₂ p)
  ; from       = P.→-to-⟶ _
  ; inverse-of = record
    { left-inverse-of  = λ _ → P.refl
    ; right-inverse-of = λ _ → P.refl
    }
  }

------------------------------------------------------------------------
-- ⊥, ⊤, _×_ and _⊎_ form a commutative semiring

×-CommutativeMonoid : Symmetric-kind → (ℓ : Level) →
                      CommutativeMonoid _ _
×-CommutativeMonoid k ℓ = record
  { Carrier             = Set ℓ
  ; _≈_                 = Related ⌊ k ⌋
  ; _∙_                 = _×_
  ; ε                   = Lift ⊤
  ; isCommutativeMonoid = record
    { isSemigroup   = record
      { isEquivalence = Setoid.isEquivalence $ Related.setoid k ℓ
      ; assoc         = λ _ _ _ → ↔⇒ Σ-assoc
      ; ∙-cong        = _×-cong_
      }
    ; identityˡ = λ A → ↔⇒ $ left-identity A
    ; comm      = λ A B → ↔⇒ $ comm A B
    }
  }
  where
  open FP _↔_

  left-identity : LeftIdentity (Lift {ℓ = ℓ} ⊤) _×_
  left-identity _ = record
    { to         = P.→-to-⟶ proj₂
    ; from       = P.→-to-⟶ λ y → _ , y
    ; inverse-of = record
      { left-inverse-of  = λ _ → P.refl
      ; right-inverse-of = λ _ → P.refl
      }
    }

  comm : Commutative _×_
  comm _ _ = record
    { to         = P.→-to-⟶ Prod.swap
    ; from       = P.→-to-⟶ Prod.swap
    ; inverse-of = record
      { left-inverse-of  = λ _ → P.refl
      ; right-inverse-of = λ _ → P.refl
      }
    }

⊎-CommutativeMonoid : Symmetric-kind → (ℓ : Level) →
                      CommutativeMonoid _ _
⊎-CommutativeMonoid k ℓ = record
  { Carrier             = Set ℓ
  ; _≈_                 = Related ⌊ k ⌋
  ; _∙_                 = _⊎_
  ; ε                   = Lift ⊥
  ; isCommutativeMonoid = record
    { isSemigroup   = record
      { isEquivalence = Setoid.isEquivalence $ Related.setoid k ℓ
      ; assoc         = λ A B C → ↔⇒ $ assoc A B C
      ; ∙-cong        = _⊎-cong_
      }
    ; identityˡ = λ A → ↔⇒ $ left-identity A
    ; comm      = λ A B → ↔⇒ $ comm A B
    }
  }
  where
  open FP _↔_

  left-identity : LeftIdentity (Lift ⊥) (_⊎_ {a = ℓ} {b = ℓ})
  left-identity A = record
    { to         = P.→-to-⟶ [ (λ ()) ∘′ lower , id ]
    ; from       = P.→-to-⟶ inj₂
    ; inverse-of = record
      { right-inverse-of = λ _ → P.refl
      ; left-inverse-of  = [ ⊥-elim ∘ lower , (λ _ → P.refl) ]
      }
    }

  assoc : Associative _⊎_
  assoc A B C = record
    { to         = P.→-to-⟶ [ [ inj₁ , inj₂ ∘ inj₁ ] , inj₂ ∘ inj₂ ]
    ; from       = P.→-to-⟶ [ inj₁ ∘ inj₁ , [ inj₁ ∘ inj₂ , inj₂ ] ]
    ; inverse-of = record
      { left-inverse-of  = [ [ (λ _ → P.refl) , (λ _ → P.refl) ] , (λ _ → P.refl) ]
      ; right-inverse-of = [ (λ _ → P.refl) , [ (λ _ → P.refl) , (λ _ → P.refl) ] ]
      }
    }

  comm : Commutative _⊎_
  comm _ _ = record
    { to         = P.→-to-⟶ swap
    ; from       = P.→-to-⟶ swap
    ; inverse-of = record
      { left-inverse-of  = inv
      ; right-inverse-of = inv
      }
    }
    where
    swap : {A B : Set ℓ} → A ⊎ B → B ⊎ A
    swap = [ inj₂ , inj₁ ]

    inv : ∀ {A B} → swap ∘ swap {A} {B} ≗ id
    inv = [ (λ _ → P.refl) , (λ _ → P.refl) ]

×⊎-CommutativeSemiring : Symmetric-kind → (ℓ : Level) →
                         CommutativeSemiring (Level.suc ℓ) ℓ
×⊎-CommutativeSemiring k ℓ = record
  { Carrier               = Set ℓ
  ; _≈_                   = Related ⌊ k ⌋
  ; _+_                   = _⊎_
  ; _*_                   = _×_
  ; 0#                    = Lift ⊥
  ; 1#                    = Lift ⊤
  ; isCommutativeSemiring = isCommutativeSemiring
  }
  where
  open CommutativeMonoid
  open FP _↔_

  left-zero : LeftZero (Lift ⊥) (_×_ {a = ℓ} {b = ℓ})
  left-zero A = record
    { to         = P.→-to-⟶ proj₁
    ; from       = P.→-to-⟶ (⊥-elim ∘′ lower)
    ; inverse-of = record
      { left-inverse-of  = λ p → ⊥-elim (lower $ proj₁ p)
      ; right-inverse-of = λ x → ⊥-elim (lower x)
      }
    }

  right-distrib : _×_ DistributesOverʳ _⊎_
  right-distrib A B C = record
    { to         = P.→-to-⟶ $ uncurry [ curry inj₁ , curry inj₂ ]
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { right-inverse-of = [ (λ _ → P.refl) , (λ _ → P.refl) ]
      ; left-inverse-of  =
          uncurry [ (λ _ _ → P.refl) , (λ _ _ → P.refl) ]
      }
    }
    where
    from : B × A ⊎ C × A → (B ⊎ C) × A
    from = [ Prod.map inj₁ id , Prod.map inj₂ id ]

  abstract

    -- If isCommutativeSemiring is made concrete, then it takes much
    -- more time to type-check coefficient-dec (at the time of
    -- writing, on a given system, using certain Agda options).

    isCommutativeSemiring :
      IsCommutativeSemiring
        {ℓ = ℓ} (Related ⌊ k ⌋) _⊎_ _×_ (Lift ⊥) (Lift ⊤)
    isCommutativeSemiring = record
      { +-isCommutativeMonoid = isCommutativeMonoid $
                                  ⊎-CommutativeMonoid k ℓ
      ; *-isCommutativeMonoid = isCommutativeMonoid $
                                  ×-CommutativeMonoid k ℓ
      ; distribʳ              = λ A B C → ↔⇒ $ right-distrib A B C
      ; zeroˡ                 = λ A → ↔⇒ $ left-zero A
      }

private

  -- A decision procedure used by the solver below.

  coefficient-dec :
    ∀ s ℓ →
    let open CommutativeSemiring (×⊎-CommutativeSemiring s ℓ)
        open Algebra.Operations semiring renaming (_×_ to Times)
    in

    ∀ m n → Dec (Times m 1# ∼[ ⌊ s ⌋ ] Times n 1#)

  coefficient-dec equivalence ℓ m n with m | n
  ... | zero  | zero  = yes (Eq.equivalence id id)
  ... | zero  | suc _ = no  (λ eq → lower (Equivalence.from eq ⟨$⟩ inj₁ _))
  ... | suc _ | zero  = no  (λ eq → lower (Equivalence.to   eq ⟨$⟩ inj₁ _))
  ... | suc _ | suc _ = yes (Eq.equivalence (λ _ → inj₁ _) (λ _ → inj₁ _))
  coefficient-dec bijection ℓ m n = Dec.map′ to (from m n) (Nat._≟_ m n)
    where
    open CommutativeSemiring (×⊎-CommutativeSemiring bijection ℓ)
      using (1#; semiring)
    open Algebra.Operations semiring renaming (_×_ to Times)

    to : ∀ {m n} → m ≡ n → Times m 1# ↔ Times n 1#
    to {m} P.refl = Times m 1# ∎
      where open Related.EquationalReasoning

    from : ∀ m n → Times m 1# ↔ Times n 1# → m ≡ n
    from zero    zero    _   = P.refl
    from zero    (suc n) 0↔+ = ⊥-elim $ lower $ Inverse.from 0↔+ ⟨$⟩ inj₁ _
    from (suc m) zero    +↔0 = ⊥-elim $ lower $ Inverse.to   +↔0 ⟨$⟩ inj₁ _
    from (suc m) (suc n) +↔+ = P.cong suc $ from m n (pred↔pred +↔+)
      where
      open P.≡-Reasoning

      ↑⊤ : Set ℓ
      ↑⊤ = Lift ⊤

      inj₁≢inj₂ : ∀ {A : Set ℓ} {x : ↑⊤ ⊎ A} {y} →
                  x ≡ inj₂ y → x ≡ inj₁ _ → ⊥
      inj₁≢inj₂ {x = x} {y} eq₁ eq₂ =
        P.subst [ const ⊥ , const ⊤ ] (begin
          inj₂ y  ≡⟨ P.sym eq₁ ⟩
          x       ≡⟨ eq₂ ⟩
          inj₁ _  ∎)
          _

      g′ : {A B : Set ℓ}
           (f : (↑⊤ ⊎ A) ↔ (↑⊤ ⊎ B)) (x : A) (y z : ↑⊤ ⊎ B) →
           Inverse.to f ⟨$⟩ inj₂ x ≡ y →
           Inverse.to f ⟨$⟩ inj₁ _ ≡ z →
           B
      g′ _ _ (inj₂ y)       _  _   _   = y
      g′ _ _ (inj₁ _) (inj₂ z) _   _   = z
      g′ f _ (inj₁ _) (inj₁ _) eq₁ eq₂ = ⊥-elim $
        inj₁≢inj₂ (Inverse.to-from f eq₁) (Inverse.to-from f eq₂)

      g : {A B : Set ℓ} → (↑⊤ ⊎ A) ↔ (↑⊤ ⊎ B) → A → B
      g f x = g′ f x _ _ P.refl P.refl

      g′∘g′ : ∀ {A B} (f : (↑⊤ ⊎ A) ↔ (↑⊤ ⊎ B))
              x y₁ z₁ y₂ z₂ eq₁₁ eq₂₁ eq₁₂ eq₂₂ →
              g′ (reverse f) (g′ f x y₁ z₁ eq₁₁ eq₂₁) y₂ z₂ eq₁₂ eq₂₂ ≡
              x
      g′∘g′ f x (inj₂ y₁) _ (inj₂ y₂) _ eq₁₁ _ eq₁₂ _ =
        P.cong [ const y₂ , id ] (begin
          inj₂ y₂                     ≡⟨ P.sym eq₁₂ ⟩
          Inverse.from f ⟨$⟩ inj₂ y₁  ≡⟨ Inverse.to-from f eq₁₁ ⟩
          inj₂ x                      ∎)
      g′∘g′ f x (inj₁ _) (inj₂ _) (inj₁ _) (inj₂ z₂) eq₁₁ _ _ eq₂₂ =
        P.cong [ const z₂ , id ] (begin
          inj₂ z₂                    ≡⟨ P.sym eq₂₂ ⟩
          Inverse.from f ⟨$⟩ inj₁ _  ≡⟨ Inverse.to-from f eq₁₁ ⟩
          inj₂ x                     ∎)
      g′∘g′ f _ (inj₂ y₁) _ (inj₁ _) _ eq₁₁ _ eq₁₂ _ =
        ⊥-elim $ inj₁≢inj₂ (Inverse.to-from f eq₁₁) eq₁₂
      g′∘g′ f _ (inj₁ _) (inj₂ z₁) (inj₂ y₂) _ _ eq₂₁ eq₁₂ _ =
        ⊥-elim $ inj₁≢inj₂ eq₁₂ (Inverse.to-from f eq₂₁)
      g′∘g′ f _ (inj₁ _) (inj₂ _) (inj₁ _) (inj₁ _) eq₁₁ _ _ eq₂₂ =
        ⊥-elim $ inj₁≢inj₂ (Inverse.to-from f eq₁₁) eq₂₂
      g′∘g′ f _ (inj₁ _) (inj₁ _) _ _ eq₁₁ eq₂₁ _ _ =
        ⊥-elim $ inj₁≢inj₂ (Inverse.to-from f eq₁₁)
                           (Inverse.to-from f eq₂₁)

      g∘g : ∀ {A B} (f : (↑⊤ ⊎ A) ↔ (↑⊤ ⊎ B)) x →
            g (reverse f) (g f x) ≡ x
      g∘g f x = g′∘g′ f x _ _ _ _ P.refl P.refl P.refl P.refl

      pred↔pred : {A B : Set ℓ} → (↑⊤ ⊎ A) ↔ (↑⊤ ⊎ B) → A ↔ B
      pred↔pred X⊎↔X⊎ = record
        { to         = P.→-to-⟶ $ g          X⊎↔X⊎
        ; from       = P.→-to-⟶ $ g (reverse X⊎↔X⊎)
        ; inverse-of = record
          { left-inverse-of  = g∘g          X⊎↔X⊎
          ; right-inverse-of = g∘g (reverse X⊎↔X⊎)
          }
        }

module Solver s {ℓ} =
  Algebra.RingSolver.Natural-coefficients
    (×⊎-CommutativeSemiring s ℓ)
    (coefficient-dec s ℓ)

private

  -- A test of the solver above.

  test : (A B C : Set) →
         (Lift ⊤ × A × (B ⊎ C)) ↔ (A × B ⊎ C × (Lift ⊥ ⊎ A))
  test = solve 3 (λ A B C → con 1 :* (A :* (B :+ C)) :=
                            A :* B :+ C :* (con 0 :+ A))
                 Inv.id
    where open Solver bijection

------------------------------------------------------------------------
-- Some reordering lemmas

ΠΠ↔ΠΠ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) →
        ((x : A) (y : B) → P x y) ↔ ((y : B) (x : A) → P x y)
ΠΠ↔ΠΠ _ = record
  { to         = P.→-to-⟶ λ f x y → f y x
  ; from       = P.→-to-⟶ λ f y x → f x y
  ; inverse-of = record
    { left-inverse-of  = λ _ → P.refl
    ; right-inverse-of = λ _ → P.refl
    }
  }

∃∃↔∃∃ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) →
        (∃₂ λ x y → P x y) ↔ (∃₂ λ y x → P x y)
∃∃↔∃∃ {a} {b} {p} _ = record
  { to         = P.→-to-⟶ λ p → (proj₁ (proj₂ p) , proj₁ p , proj₂ (proj₂ p))
  ; from       = P.→-to-⟶ λ p → (proj₁ (proj₂ p) , proj₁ p , proj₂ (proj₂ p))
  ; inverse-of = record
    { left-inverse-of  = λ _ → P.refl
    ; right-inverse-of = λ _ → P.refl
    }
  }

------------------------------------------------------------------------
-- Implicit and explicit function spaces are isomorphic

Π↔Π : ∀ {a b} {A : Set a} {B : A → Set b} →
      ((x : A) → B x) ↔ ({x : A} → B x)
Π↔Π = record
  { to         = P.→-to-⟶ λ f {x} → f x
  ; from       = P.→-to-⟶ λ f x → f {x}
  ; inverse-of = record
    { left-inverse-of  = λ _ → P.refl
    ; right-inverse-of = λ _ → P.refl
    }
  }

------------------------------------------------------------------------
-- _→_ preserves the symmetric relations

_→-cong-⇔_ :
  ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
  A ⇔ B → C ⇔ D → (A → C) ⇔ (B → D)
A⇔B →-cong-⇔ C⇔D = record
  { to   = P.→-to-⟶ λ f x →
             Equivalence.to   C⇔D ⟨$⟩ f (Equivalence.from A⇔B ⟨$⟩ x)
  ; from = P.→-to-⟶ λ f x →
             Equivalence.from C⇔D ⟨$⟩ f (Equivalence.to   A⇔B ⟨$⟩ x)
  }

→-cong :
  ∀ {a b c d} →
  P.Extensionality a c → P.Extensionality b d →
  ∀ {k} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
  A ∼[ ⌊ k ⌋ ] B → C ∼[ ⌊ k ⌋ ] D → (A → C) ∼[ ⌊ k ⌋ ] (B → D)
→-cong extAC extBD {equivalence} A⇔B C⇔D = A⇔B →-cong-⇔ C⇔D
→-cong extAC extBD {bijection}   A↔B C↔D = record
  { to         = Equivalence.to   A→C⇔B→D
  ; from       = Equivalence.from A→C⇔B→D
  ; inverse-of = record
    { left-inverse-of  = λ f → extAC λ x → begin
        Inverse.from C↔D ⟨$⟩ (Inverse.to C↔D ⟨$⟩
          f (Inverse.from A↔B ⟨$⟩ (Inverse.to A↔B ⟨$⟩ x)))  ≡⟨ Inverse.left-inverse-of C↔D _ ⟩
        f (Inverse.from A↔B ⟨$⟩ (Inverse.to A↔B ⟨$⟩ x))     ≡⟨ P.cong f $ Inverse.left-inverse-of A↔B x ⟩
        f x                                                 ∎
    ; right-inverse-of = λ f → extBD λ x → begin
        Inverse.to C↔D ⟨$⟩ (Inverse.from C↔D ⟨$⟩
          f (Inverse.to A↔B ⟨$⟩ (Inverse.from A↔B ⟨$⟩ x)))  ≡⟨ Inverse.right-inverse-of C↔D _ ⟩
        f (Inverse.to A↔B ⟨$⟩ (Inverse.from A↔B ⟨$⟩ x))     ≡⟨ P.cong f $ Inverse.right-inverse-of A↔B x ⟩
        f x                                                 ∎
    }
  }
  where
  open P.≡-Reasoning
  A→C⇔B→D = ↔⇒ A↔B →-cong-⇔ ↔⇒ C↔D

------------------------------------------------------------------------
-- ¬_ preserves the symmetric relations

¬-cong-⇔ : ∀ {a b} {A : Set a} {B : Set b} →
           A ⇔ B → (¬ A) ⇔ (¬ B)
¬-cong-⇔ A⇔B = A⇔B →-cong-⇔ (⊥ ∎)
  where open Related.EquationalReasoning

¬-cong : ∀ {a b} →
         P.Extensionality a Level.zero →
         P.Extensionality b Level.zero →
         ∀ {k} {A : Set a} {B : Set b} →
         A ∼[ ⌊ k ⌋ ] B → (¬ A) ∼[ ⌊ k ⌋ ] (¬ B)
¬-cong extA extB A≈B = →-cong extA extB A≈B (⊥ ∎)
  where open Related.EquationalReasoning

------------------------------------------------------------------------
-- _⇔_ preserves _⇔_

-- The type of the following proof is a bit more general.

Related-cong :
  ∀ {k a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
  A ∼[ ⌊ k ⌋ ] B → C ∼[ ⌊ k ⌋ ] D → (A ∼[ ⌊ k ⌋ ] C) ⇔ (B ∼[ ⌊ k ⌋ ] D)
Related-cong {A = A} {B} {C} {D} A≈B C≈D =
  Eq.equivalence (λ A≈C → B  ∼⟨ sym A≈B ⟩
                          A  ∼⟨ A≈C ⟩
                          C  ∼⟨ C≈D ⟩
                          D  ∎)
                 (λ B≈D → A  ∼⟨ A≈B ⟩
                          B  ∼⟨ B≈D ⟩
                          D  ∼⟨ sym C≈D ⟩
                          C  ∎)
  where open Related.EquationalReasoning

------------------------------------------------------------------------
-- A lemma relating True dec and P, where dec : Dec P

True↔ : ∀ {p} {P : Set p}
        (dec : Dec P) → ((p₁ p₂ : P) → p₁ ≡ p₂) → True dec ↔ P
True↔ (yes p) irr = record
  { to         = P.→-to-⟶ (λ _ → p)
  ; from       = P.→-to-⟶ (λ _ → _)
  ; inverse-of = record
    { left-inverse-of  = λ _ → P.refl
    ; right-inverse-of = irr p
    }
  }
True↔ (no ¬p) _ = record
  { to         = P.→-to-⟶ (λ ())
  ; from       = P.→-to-⟶ (λ p → ¬p p)
  ; inverse-of = record
    { left-inverse-of  = λ ()
    ; right-inverse-of = λ p → ⊥-elim (¬p p)
    }
  }

------------------------------------------------------------------------
-- Equality between pairs can be expressed as a pair of equalities

Σ-≡,≡↔≡ : ∀ {a b} {A : Set a} {B : A → Set b} {p₁ p₂ : Σ A B} →
          (∃ λ (p : proj₁ p₁ ≡ proj₁ p₂) →
             P.subst B p (proj₂ p₁) ≡ proj₂ p₂) ↔
          (p₁ ≡ p₂)
Σ-≡,≡↔≡ {A = A} {B} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = left-inverse-of
    ; right-inverse-of = right-inverse-of
    }
  }
  where
  to : {p₁ p₂ : Σ A B} →
       Σ (proj₁ p₁ ≡ proj₁ p₂)
         (λ p → P.subst B p (proj₂ p₁) ≡ proj₂ p₂) →
       p₁ ≡ p₂
  to (P.refl , P.refl) = P.refl

  from : {p₁ p₂ : Σ A B} →
         p₁ ≡ p₂ →
         Σ (proj₁ p₁ ≡ proj₁ p₂)
           (λ p → P.subst B p (proj₂ p₁) ≡ proj₂ p₂)
  from P.refl = P.refl , P.refl

  left-inverse-of : {p₁ p₂ : Σ A B}
                    (p : Σ (proj₁ p₁ ≡ proj₁ p₂)
                           (λ x → P.subst B x (proj₂ p₁) ≡ proj₂ p₂)) →
                    from (to p) ≡ p
  left-inverse-of (P.refl , P.refl) = P.refl

  right-inverse-of : {p₁ p₂ : Σ A B} (p : p₁ ≡ p₂) → to (from p) ≡ p
  right-inverse-of P.refl = P.refl

×-≡,≡↔≡ : ∀ {a b} {A : Set a} {B : Set b} {p₁ p₂ : A × B} →
          (proj₁ p₁ ≡ proj₁ p₂ × proj₂ p₁ ≡ proj₂ p₂) ↔
          p₁ ≡ p₂
×-≡,≡↔≡ {A = A} {B} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = left-inverse-of
    ; right-inverse-of = right-inverse-of
    }
  }
  where
  to : {p₁ p₂ : A × B} →
       (proj₁ p₁ ≡ proj₁ p₂) × (proj₂ p₁ ≡ proj₂ p₂) → p₁ ≡ p₂
  to (P.refl , P.refl) = P.refl

  from : {p₁ p₂ : A × B} → p₁ ≡ p₂ →
         (proj₁ p₁ ≡ proj₁ p₂) × (proj₂ p₁ ≡ proj₂ p₂)
  from P.refl = P.refl , P.refl

  left-inverse-of : {p₁ p₂ : A × B} →
                    (p : (proj₁ p₁ ≡ proj₁ p₂) × (proj₂ p₁ ≡ proj₂ p₂)) →
                    from (to p) ≡ p
  left-inverse-of (P.refl , P.refl) = P.refl

  right-inverse-of : {p₁ p₂ : A × B} (p : p₁ ≡ p₂) → to (from p) ≡ p
  right-inverse-of P.refl = P.refl


text:
-- Andreas, 2013-10-24 Bug reported to me by Christoph-Simon Senjak
module Issue924 where

open import Level

open import Data.Empty
open import Data.Product
open import Data.Sum

open import Data.Bool

open import Data.Maybe.Base

import Data.Nat as ℕ
open import Data.Nat using (ℕ)
import Data.Nat.Divisibility as ℕ
import Data.Nat.Properties as ℕ
open import Data.Nat.DivMod

import Data.Fin as F
open import Data.Fin using (Fin)
import Data.Fin.Properties as F

import Data.List as L
open import Data.List using (List)

open import Data.Vec

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Algebra
open import Algebra.Structures

Byte : Set
Byte = Fin 256

infixr 8 _^_

_^_ : ℕ → ℕ → ℕ
_ ^ 0 = 1
n ^ (ℕ.suc m) = n ℕ.* (n ^ m)

BitVecToNat : {n : ℕ} → Vec Bool n → ℕ
BitVecToNat [] = 0
BitVecToNat (true ∷ r) = ℕ.suc (2 ℕ.* (BitVecToNat r))
BitVecToNat (false ∷ r) = (2 ℕ.* (BitVecToNat r))

postulate ≤lem₁ : {a b : ℕ} → (a ℕ.< b) → (2 ℕ.* a) ℕ.< (2 ℕ.* b)

postulate ≤lem₂ : {a b : ℕ} → (a ℕ.< (ℕ.suc b)) → (ℕ.suc (2 ℕ.* a)) ℕ.< (2 ℕ.* (ℕ.suc b))
postulate ≤lem₃ : {a b c : ℕ} → (c ℕ.+ (a ℕ.* 2) ℕ.< (2 ℕ.* b)) → a ℕ.< b

¬0<b∧0≡b : {b : ℕ} → 0 ℕ.< b → 0 ≡ b → ⊥
¬0<b∧0≡b {0} () 0≡b
¬0<b∧0≡b {ℕ.suc n} 0<b ()

0<a∧0<b→0<ab : (a b : ℕ) → (0 ℕ.< a) → (0 ℕ.< b) → (0 ℕ.< (a ℕ.* b))
0<a∧0<b→0<ab a b 0<a 0<b with 1 ℕ.≤? (a ℕ.* b)
...                      | yes y = y
...                      | no n with (a ℕ.* b) | inspect (λ x → a ℕ.* x) b
...                             | ℕ.suc ns | _ = ⊥-elim (n (ℕ.s≤s (ℕ.z≤n {ns})))
...                             | 0 | [ eq ] with ℕ.m*n≡0⇒m≡0∨n≡0 a {b} eq
...                                          | inj₁ a≡0 = ⊥-elim (¬0<b∧0≡b 0<a (sym a≡0))
...                                          | inj₂ b≡0 = ⊥-elim (¬0<b∧0≡b 0<b (sym b≡0))

0<s^b : {a b : ℕ} → (0 ℕ.< ((ℕ.suc a) ^ b))
0<s^b {_} {0} = ℕ.s≤s ℕ.z≤n
0<s^b {m} {ℕ.suc n} = 0<a∧0<b→0<ab (ℕ.suc m) ((ℕ.suc m) ^ n) (ℕ.s≤s ℕ.z≤n) (0<s^b {m} {n})

<-lemma : (b : ℕ) → (0 ℕ.< b) → ∃ λ a → ℕ.suc a ≡ b
<-lemma (ℕ.suc b) (ℕ.s≤s (ℕ.z≤n {.b})) = ( b , refl )

2^lem₁ : (a : ℕ) → ∃ λ b → (ℕ.suc b) ≡ (2 ^ a)
2^lem₁ a = <-lemma (2 ^ a) (0<s^b {1} {a})

BitVecToNatLemma : {n : ℕ} → (s : Vec Bool n) → ((BitVecToNat s) ℕ.< (2 ^ n))
BitVecToNatLemma {0} [] = ℕ.s≤s ℕ.z≤n
BitVecToNatLemma {ℕ.suc n} (false ∷ r) = ≤lem₁ (BitVecToNatLemma r)
BitVecToNatLemma {ℕ.suc n} (true ∷ r) = ret₃ where
     q = 2^lem₁ n
     t = proj₁ q
     s : (ℕ.suc t) ≡ 2 ^ n
     s = proj₂ q
     ret₁ : (BitVecToNat r) ℕ.< (ℕ.suc t)
     ret₁ = subst (λ u → (BitVecToNat r) ℕ.< u) (sym s) (BitVecToNatLemma r)
     ret₂ : (ℕ.suc (2 ℕ.* (BitVecToNat r))) ℕ.< (2 ℕ.* (ℕ.suc t))
     ret₂ = ≤lem₂ ret₁
     ret₃ : (ℕ.suc (2 ℕ.* (BitVecToNat r))) ℕ.< (2 ^ (ℕ.suc n))
     ret₃ = subst (λ u → (ℕ.suc (2 ℕ.* (BitVecToNat r))) ℕ.< (2 ℕ.* u)) s ret₂

BitVecToFin : {n : ℕ} → Vec Bool n → Fin (2 ^ n)
BitVecToFin s = F.fromℕ< (BitVecToNatLemma s)

FinToBitVec : {n : ℕ} → (m : Fin (2 ^ n)) → ∃ λ (s : Vec Bool n) → (BitVecToFin s ≡ m)
FinToBitVec {0} F.zero = ( [] , refl )
FinToBitVec {0} (F.suc ())
FinToBitVec {ℕ.suc n} k = ( ret₁ , lem₇ ) where

  open CommutativeSemiring ℕ.+-*-commutativeSemiring using (*-comm)

  kn = F.toℕ k

  p2^n' = 2^lem₁ (ℕ.suc n)

  p2^n = proj₁ p2^n'

  p2^nl : ℕ.suc p2^n ≡ 2 ^ (ℕ.suc n)
  p2^nl = proj₂ p2^n'

  kn<2^n : kn ℕ.< 2 ^ (ℕ.suc n)
  kn<2^n = subst (λ d → kn ℕ.< d) p2^nl (subst (λ d → kn ℕ.< ℕ.suc (ℕ.pred d)) (sym p2^nl) (ℕ.s≤s (F.toℕ≤pred[n] k)))

  dm = kn divMod 2

  quot = DivMod.quotient dm

  rem = F.toℕ (DivMod.remainder dm)

  Fin2toBool : Fin 2 → Bool
  Fin2toBool F.zero = false
  Fin2toBool (F.suc F.zero) = true
  Fin2toBool (F.suc (F.suc ()))

  zl = 2^lem₁ n

  lem₀ : rem ℕ.+ quot ℕ.* 2 ℕ.< (2 ^ (ℕ.suc n))
  lem₀ = subst (λ d → d ℕ.< (2 ^ (ℕ.suc n))) (DivMod.property dm) kn<2^n

  lem₁ : (DivMod.quotient dm) ℕ.< (2 ^ n)
  lem₁ = ≤lem₃ {a = quot} {b = 2 ^ n} {c = rem} lem₀

  fQuot : Fin (2 ^ n)
  fQuot = F.fromℕ< lem₁

  -- the recursive call
  prevRet : ∃ λ (s : Vec Bool n) → (BitVecToFin s ≡ fQuot)
  prevRet = FinToBitVec (F.fromℕ< lem₁)

  prevRetEq : (BitVecToFin (proj₁ prevRet) ≡ fQuot)
  prevRetEq = proj₂ prevRet

  lem₉ : {n : ℕ} → (r : Vec Bool n) → F.toℕ (BitVecToFin r) ≡ (BitVecToNat r)
  lem₉ r = trans (cong F.toℕ refl) (F.toℕ-fromℕ< (BitVecToNatLemma r))

  prevRetEqℕ : quot ≡ BitVecToNat (proj₁ prevRet)
  prevRetEqℕ = trans (trans (sym (F.toℕ-fromℕ< lem₁)) (cong F.toℕ (sym prevRetEq))) (lem₉ (proj₁ prevRet))

  ret₁ = (Fin2toBool (DivMod.remainder dm)) ∷ (proj₁ prevRet)

  lem₃ : (r : Fin 2) → (BitVecToNat ((Fin2toBool r) ∷ (proj₁ prevRet))) ≡ (F.toℕ r) ℕ.+ (2 ℕ.* (BitVecToNat (proj₁ prevRet)))
  lem₃ F.zero = refl
  lem₃ (F.suc F.zero) = refl
  lem₃ (F.suc (F.suc ()))

  lem₅ : rem ℕ.+ (2 ℕ.* (BitVecToNat (proj₁ prevRet))) ≡ kn
  lem₅ = subst (λ d → rem ℕ.+ d ≡ kn) (*-comm (BitVecToNat (proj₁ prevRet)) 2)
         (subst (λ d → rem ℕ.+ d ℕ.* 2 ≡ kn) prevRetEqℕ (sym (DivMod.property dm)))

  lem₆ : (BitVecToNat ret₁) ≡ kn
  lem₆ =
    begin
      BitVecToNat ret₁
    ≡⟨ lem₃ (DivMod.remainder dm) ⟩
      rem ℕ.+ (2 ℕ.* (BitVecToNat (proj₁ prevRet)))
    ≡⟨ lem₅ ⟩
      kn
    ∎
  -- lem₆ = trans lem₄ lem₅

  lem₈ : kn ≡ F.toℕ (F.fromℕ< kn<2^n)
  lem₈ = sym (cong F.toℕ (F.fromℕ<-toℕ k kn<2^n))

  lem₇ : (BitVecToFin ret₁) ≡ k
  lem₇ = trans (F.toℕ-injective (trans (lem₉ ret₁) (trans lem₆ lem₈))) (F.fromℕ<-toℕ k kn<2^n)

record ByteStream : Set where
  constructor bs
  field
    cBit : Maybe (∃ λ (c : Fin 8) → Vec Bool (ℕ.suc (F.toℕ c)))
    str : List Byte
    property : (cBit ≡ nothing) → (str ≡ L.[])

byteStreamFromList : List Byte → ByteStream
byteStreamFromList L.[]      = bs nothing
                                  L.[]
                                  (λ _ → refl)
byteStreamFromList (a L.∷ x) = bs (just ((F.fromℕ 7) , (proj₁ (FinToBitVec a))))
                                  x
                                  (λ ())
-- Problem WAS:
-- Normalization in unifyConArgs went berserk when checking this
-- absurd lambda.  Fixed by more cautious normalization in unifier.


text:
module Cats.Category.Constructions.Exponential where

open import Level

open import Cats.Category.Base
open import Cats.Category.Constructions.Product as Product using
  (HasBinaryProducts)
open import Cats.Util.Conv

import Cats.Category.Constructions.Unique as Unique

module Build {lo la l≈}
  (Cat : Category lo la l≈)
  {{hasBinaryProducts : HasBinaryProducts Cat}}
  where

  open Category Cat
  open ≈-Reasoning
  open Unique.Build Cat
  open HasBinaryProducts hasBinaryProducts

  record Exp (B C : Obj) : Set (lo ⊔ la ⊔ l≈) where
    field
      Cᴮ : Obj
      eval : Cᴮ × B ⇒ C
      curry′ : ∀ {A} (f : A × B ⇒ C)
        → ∃![ f̃ ∈ A ⇒ Cᴮ ] (eval ∘ ⟨ f̃ × id ⟩ ≈ f)

    curry : ∀ {A} → A × B ⇒ C → A ⇒ Cᴮ
    curry f = curry′ f ⃗

    eval-curry : ∀ {A} {f : A × B ⇒ C}
      → eval ∘ ⟨ curry f × id ⟩ ≈ f
    eval-curry {f = f} = ∃!′.prop (curry′ f)

    curry-unique : ∀ {A} {f : A × B ⇒ C} {g}
      → eval ∘ ⟨ g × id ⟩ ≈ f
      → curry f ≈ g
    curry-unique {f = f} = ∃!′.unique (curry′ f)

    uncurry : ∀ {A} → A ⇒ Cᴮ → A × B ⇒ C
    uncurry f = eval ∘ ⟨ f × id ⟩

    curry∘uncurry : ∀ {A} {f : A ⇒ Cᴮ}
      → curry (uncurry f) ≈ f
    curry∘uncurry = curry-unique ≈.refl

    uncurry∘curry : ∀ {A} {f : A × B ⇒ C}
      → uncurry (curry f) ≈ f
    uncurry∘curry = eval-curry

  instance HasObj-Exp : ∀ {B C} → HasObj (Exp B C) lo la l≈
  HasObj-Exp = record { Cat = Cat ; _ᴼ = Exp.Cᴮ }

  open Exp public

  curry∘curry : ∀ {A B C Y Z} (Cᴮ : Exp B C) (Yᶻ : Exp Y Z)
    → {f : Cᴮ ᴼ × Y ⇒ Z} {g : A × B ⇒ C}
    → curry Yᶻ f ∘ curry Cᴮ g ≈ curry Yᶻ (f ∘ ⟨ curry Cᴮ g × id ⟩)
  curry∘curry Cᴮ Yᶻ {f} {g} = ≈.sym (curry-unique Yᶻ (
      begin
        eval Yᶻ ∘ ⟨ curry Yᶻ f ∘ curry Cᴮ g × id ⟩
      ≈⟨ ∘-resp-r (⟨×⟩-resp ≈.refl (≈.sym id-l)) ⟩
        eval Yᶻ ∘ ⟨ curry Yᶻ f ∘ curry Cᴮ g × id ∘ id ⟩
      ≈⟨ ∘-resp-r (≈.sym ⟨×⟩-∘) ⟩
        eval Yᶻ ∘ ⟨ curry Yᶻ f × id ⟩ ∘ ⟨ curry Cᴮ g × id ⟩
      ≈⟨ unassoc ⟩
        (eval Yᶻ ∘ ⟨ curry Yᶻ f × id ⟩) ∘ ⟨ curry Cᴮ g × id ⟩
      ≈⟨ ∘-resp-l (eval-curry Yᶻ) ⟩
        f ∘ ⟨ curry Cᴮ g × id ⟩
      ∎
    ))

record HasExponentials {lo la l≈}
  (Cat : Category lo la l≈)
  : Set (lo ⊔ la ⊔ l≈)
  where
  private open module Bld = Build Cat using (Exp)
  open Category Cat
  open Unique.Build Cat

  infixr 1 _↝′_ _↝_

  field
    {{hasBinaryProducts}} : HasBinaryProducts Cat
    _↝′_ : ∀ B C → Exp B C

  open HasBinaryProducts hasBinaryProducts

  _↝_ : Obj → Obj → Obj
  B ↝ C = (B ↝′ C) ᴼ

  eval : ∀ {B C} → (B ↝ C) × B ⇒ C
  eval {B} {C} = Bld.eval (B ↝′ C)

  curry : ∀ {A B C} → A × B ⇒ C → A ⇒ B ↝ C
  curry {B = B} {C} f = Bld.curry (B ↝′ C) f

  uncurry : ∀ {A B C} → A ⇒ B ↝ C → A × B ⇒ C
  uncurry {B = B} {C} = Bld.uncurry (B ↝′ C)

  eval-curry : ∀ {A B C} {f : A × B ⇒ C}
    → eval ∘ ⟨ curry f × id ⟩ ≈ f
  eval-curry {B = B} {C} = Bld.eval-curry (B ↝′ C)

  curry∘uncurry : ∀ {A B C} {f : A ⇒ B ↝ C}
    → curry (uncurry f) ≈ f
  curry∘uncurry {B = B} {C} = Bld.curry∘uncurry (B ↝′ C)

  uncurry∘curry : ∀ {A B C} {f : A × B ⇒ C}
    → uncurry (curry f) ≈ f
  uncurry∘curry {B = B} {C} = Bld.uncurry∘curry (B ↝′ C)

  curry∘curry : ∀ {A B C Y Z}
    → {f : (B ↝ C) × Y ⇒ Z} {g : A × B ⇒ C}
    → curry f ∘ curry g ≈ curry (f ∘ ⟨ curry g × id ⟩)
  curry∘curry {B = B} {C} {Y} {Z} = Bld.curry∘curry (B ↝′ C) (Y ↝′ Z)

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
open import Prelude

module Implicits.Resolution.Termination.SizeMeasures where

open import Induction.WellFounded
open import Induction.Nat
open import Data.Product hiding (map)
open import Data.Nat.Base using (_<′_)
open import Data.Fin hiding (_+_; _≤_; _<_; _≤?_)
open import Data.List hiding (map)
open import Data.List.All
open import Implicits.Syntax
open import Implicits.Syntax.Type.Unification
open import Data.Nat hiding (_<_)
open import Data.Nat.Properties

-- a strict sizemeasure for types
||_|| : ∀ {ν} → Type ν → ℕ
|| simpl (tc x) || = 1
|| simpl (tvar n) || = 1
|| simpl (a →' b) || = 1 + || a || + || b ||
|| a ⇒ b || = 1 + || a || + || b ||
|| ∀' a || = 1 + || a ||

-- size of the head of a type
h||_|| : ∀ {ν} → Type ν → ℕ
h|| a || = || proj₂ (a ◁) ||

-- type measure on metatypes
m||_|| : ∀ {m ν} → MetaType m ν → ℕ
m|| simpl (tc x) || = 1
m|| simpl (tvar n) || = 1
m|| simpl (mvar n) || = 1
m|| simpl (a →' b) || = suc (m|| a || + m|| b ||)
m|| a ⇒ b || = 1 + (m|| a || + m|| b ||)
m|| ∀' a || = 1 + m|| a ||

-- We package Type with it's deBruijn counter because
-- we need to express orderings such as a sρ< ∀' a
-- where the number of free variables varies.
-- We could express that as ∀ {ν μ} → Type ν → Type μ → Set,
-- but Well-founded _sρ<_ unifies ν and μ,
-- such that the well-founded proof would be too narrow
_hρ≤_ : (a b : ∃ Type) → Set
(_ , a) hρ≤ (_ , b) = h|| a || ≤ h|| b ||

_hρ<_ : (a b : ∃ Type) → Set
(_ , a) hρ< (_ , b) = h|| a || < h|| b ||

_hρ<?_ : ∀ {ν μ} → (a : Type ν) → (b : Type μ) → Dec ((ν , a) hρ< (μ , b))
a hρ<? b with h|| a || | h|| b ||
a hρ<? b | y | z = (suc y) ≤? z

_ρ<_ : ∃ Type → ∃ Type → Set
(_ , a) ρ< (_ , b) = || a || < || b ||

_ρ<?_ : (a b : ∃ Type) → Dec (a ρ< b)
(_ , a) ρ<? (_ , b) with || a || | || b ||
(_ , a) ρ<? (_ , b) | y | z = (suc y) ≤? z

_m<_ : ∃₂ MetaType → ∃₂ MetaType → Set
(_ , _ , a) m< (_ , _ , b) = m|| a || < m|| b ||

_occ[_]<_ : ∀ {ν μ} (a : Type ν) (x : ℕ) (b : Type μ) → Set
a occ[ x ]< b = (occ x (proj₂ (a ◁))) ≤ (occ x (proj₂ (b ◁)))

-- oliveira's termination condition on types
data ⊢term {ν} : (Type ν) → Set where
  term-simp : ∀ {τ} → ⊢term (simpl τ)
  term-tabs : ∀ {a} → ⊢term a → ⊢term (∀' a)
  term-iabs : ∀ {a b} → ⊢term a → ⊢term b → (, a) hρ< (, b) →
              All (λ x → a occ[ toℕ x ]< b) (fvars a ++ fvars b) →
              ⊢term (a ⇒ b)