text:
------------------------------------------------------------------------
-- Weakening for the NBE values
------------------------------------------------------------------------

import Axiom.Extensionality.Propositional as E
import Level
open import Data.Universe

-- The code makes use of the assumption that propositional equality of
-- functions is extensional.

module README.DependentlyTyped.NBE.Weakening
  (Uni₀ : Universe Level.zero Level.zero)
  (ext : E.Extensionality Level.zero Level.zero)
  where

open import Data.Product renaming (curry to c)
open import deBruijn.Substitution.Data
open import Function.Base hiding (_∋_)
import README.DependentlyTyped.NBE.Value as Value
open Value Uni₀ renaming ([_] to [̌_])
import README.DependentlyTyped.NormalForm as NF
open NF Uni₀ renaming ([_] to [_]n)
import README.DependentlyTyped.NormalForm.Substitution as NFS
open NFS Uni₀
import README.DependentlyTyped.Term as Term; open Term Uni₀
import Relation.Binary.PropositionalEquality as P

open P.≡-Reasoning

mutual

  -- Weakening.

  w̌k[_] : ∀ {Γ} σ τ → V̌alue Γ τ → V̌alue (Γ ▻ σ) (τ /̂ ŵk)
  w̌k[ _ ] (⋆     , τ) t       =   t /⊢n Renaming.wk
  w̌k[ _ ] (el    , τ) [ t ]el = [ t /⊢n Renaming.wk ]el
  w̌k[ σ ] (π _ _ , τ) f       =
    (λ Γ₊ → proj₁ f (σ ◅ Γ₊)) , w̌k-π-well-behaved τ f

  w̌k : ∀ {Γ σ} τ → V̌alue Γ τ → V̌alue (Γ ▻ σ) (τ /̂ ŵk)
  w̌k τ v = w̌k[ _ ] τ v

  abstract

    -- The Π case of weakening is well-behaved.

    w̌k-π-well-behaved :
      ∀ {Γ σ sp₁ sp₂} τ (f : V̌alue Γ (π sp₁ sp₂ , τ)) →
      W̌ell-behaved sp₁ sp₂ (τ /̂I ŵk) (λ Γ₊ → proj₁ f (σ ◅ Γ₊))
    w̌k-π-well-behaved {σ = σ} τ f Γ₊ v =
      let lemma = begin
            [ ⟦̌ τ /̂I ŵk ∣ (λ Γ₊ → proj₁ f (σ ◅ Γ₊)) ⟧-π /̂Val ŵk₊ Γ₊ ]  ≡⟨ /̂Val-cong (P.sym $ w̌eaken-corresponds-π τ f) P.refl ⟩
            [ ⟦̌_⟧ {σ = τ} f /̂Val ŵk[ σ ] /̂Val ŵk₊ Γ₊                ]  ≡⟨ P.refl ⟩
            [ ⟦̌ τ ∣ proj₁ f ⟧-π /̂Val ŵk₊ (σ ◅ Γ₊)                   ]  ∎

      in begin
      [ (⟦̌ τ /̂I ŵk ∣ (λ Γ₊ → proj₁ f (σ ◅ Γ₊)) ⟧-π /̂Val ŵk₊      Γ₊ ) ˢ ⟦̌ v ⟧ ]  ≡⟨ ˢ-cong lemma P.refl ⟩
      [ (⟦̌ τ       ∣         proj₁ f           ⟧-π /̂Val ŵk₊ (σ ◅ Γ₊)) ˢ ⟦̌ v ⟧ ]  ≡⟨ proj₂ f (σ ◅ Γ₊) v ⟩
      [ ⟦̌ proj₁ f (σ ◅ Γ₊) v ⟧                                                ]  ∎

    -- The Π case of weakening weakens.

    w̌eaken-corresponds-π :
      ∀ {Γ σ sp₁ sp₂} τ (f : V̌alue Γ (π sp₁ sp₂ , τ)) →
        ⟦̌_⟧ {σ = τ} f /̂Val ŵk[ σ ] ≅-Value
        ⟦̌ τ /̂I ŵk ∣ (λ Γ₊ → proj₁ f (σ ◅ Γ₊)) ⟧-π
    w̌eaken-corresponds-π {σ = σ} τ f =
      let f̌ = ⟦̌_⟧ {σ = τ} f

      in begin
      [ f̌ /̂Val ŵk[ σ ]                                            ]  ≡⟨ P.refl ⟩
      [ c ((f̌ /̂Val ŵk₊ (σ ◅ fst τ /̂ ŵk ◅ ε)) ˢ lookup zero)       ]  ≡⟨ curry-cong $
                                                                          ˢ-cong (P.refl {x = [ f̌ /̂Val ŵk₊ (σ ◅ fst τ /̂ ŵk ◅ ε) ]})
                                                                                (P.sym $ ňeutral-to-normal-identity _ _) ⟩
      [ c ((f̌ /̂Val ŵk₊ (σ ◅ fst τ /̂ ŵk ◅ ε)) ˢ ⟦ žero _ _ ⟧n)     ]  ≡⟨ curry-cong $ proj₂ f (σ ◅ fst τ /̂ ŵk ◅ ε) _ ⟩
      [ c ⟦̌ proj₁ f (σ ◅ fst τ /̂ ŵk ◅ ε) (řeflect _ (var zero)) ⟧ ]  ≡⟨ P.sym $ unfold-⟦̌∣⟧-π (τ /̂I ŵk) (λ Γ₊ → proj₁ f (σ ◅ Γ₊)) ⟩
      [ ⟦̌ τ /̂I ŵk ∣ (λ Γ₊ → proj₁ f (σ ◅ Γ₊)) ⟧-π                 ]  ∎

-- Weakening.

w̌eaken : ∀ {Γ} {σ : Type Γ} → [ V̌al ⟶ V̌al ] ŵk[ σ ]
w̌eaken = record
  { function    = w̌k
  ; corresponds = corr
  }
  where
  abstract

    -- Weakening weakens.

    corr : ∀ {Γ σ} τ (v : V̌alue Γ τ) →
           ⟦̌ v ⟧ /̂Val ŵk[ σ ] ≅-Value ⟦̌ w̌k[ σ ] τ v ⟧
    corr (⋆         , τ) t       = t /⊢n-lemma Renaming.wk
    corr (el        , τ) [ t ]el = t /⊢n-lemma Renaming.wk
    corr (π sp₁ sp₂ , τ) f       = w̌eaken-corresponds-π τ f

-- Variables can be turned into values.

v̌ar : [ Var ⟶⁼ V̌al ]
v̌ar = record
  { function    = λ _ x → řeflect _ (var x)
  ; corresponds = λ _ x → P.sym $ ňeutral-to-normal-identity _ (var x)
  }

-- Values can be turned into terms.
--
-- This definition uses the assumption that propositional equality of
-- functions is extensional. I don't know how much work is required to
-- avoid this assumption, or if it is even possible to do so.

V̌al↦Tm : V̌al ↦ Tm
V̌al↦Tm = record
  { trans = record
    { function    = λ _ v → ⌊ řeify _ v ⌋
    ; corresponds = λ _ _ → P.refl
    }
  ; simple = record
    { weaken     = w̌eaken
    ; var        = v̌ar
    ; weaken-var = w̌eaken-v̌ar _
    }
  }
  where
  open Renaming hiding (var)

  abstract
    w̌eaken-v̌ar : ∀ {Γ σ} τ (x : Γ ∋ τ) →
                 w̌k[ σ ] τ (v̌ar ⊙ x) ≅-V̌alue v̌ar ⊙ suc[ σ ] x
    w̌eaken-v̌ar (⋆ , τ) x = begin
      [̌ var (x /∋ wk) ]  ≡⟨ ≅-⊢n-⇒-≅-Value-⋆ $ var-n-cong $ ≅-⊢-⇒-≅-∋ $ /∋-wk x ⟩
      [̌ var (suc x)   ]  ∎
    w̌eaken-v̌ar (el , τ) x =  begin
      [̌ [ var (x /∋ wk) ]el ]  ≡⟨ ≅-⊢n-⇒-≅-Value-el $ var-n-cong $ ≅-⊢-⇒-≅-∋ $ /∋-wk x ⟩
      [̌ [ var (suc x)   ]el ]  ∎
    w̌eaken-v̌ar {σ = σ} (π _ _ , τ) x = ,-cong ext λ Γ₊ v → begin
      [̌ řeflect _ ((var x /⊢n wk₊ (σ ◅ Γ₊)) · řeify _ v) ]  ≡⟨ řeflect-cong $
                                                                 ·n-cong (var-n-cong $ ≅-⊢-⇒-≅-∋ $ /∋-wk₊-◅ x Γ₊)
                                                                         (P.refl {x = [ řeify _ v ]n}) ⟩
      [̌ řeflect _ ((var (suc x) /⊢n wk₊ Γ₊) · řeify _ v) ]  ∎

module V̌al-subst = _↦_ V̌al↦Tm

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Construction.Grothendieck where

-- The construction of a 1-Category from a (contravariant)
-- pseudofunctor into Cats (as a bicategory)

open import Level
open import Data.Product using (Σ; _,_)
open import Function using (_$_)
open import Relation.Binary using (IsEquivalence)

open import Categories.Category
open import Categories.Bicategory using (Bicategory)
open import Categories.Bicategory.Instance.Cats
open import Categories.Bicategory.Construction.1-Category
open import Categories.Functor renaming (id to idF)
open import Categories.Morphism using (Iso)
open import Categories.Pseudofunctor
open import Categories.NaturalTransformation hiding (id)

private
  variable
    o ℓ e o′ ℓ′ e′ : Level

module _ {C : Category o ℓ e} {b}
         (P : Pseudofunctor (1-Category b (Category.op C)) (Cats o′ ℓ′ e′)) where

  open Pseudofunctor P renaming (P₁ to PF; assoc to P-assoc)
  open Functor using () renaming (F₀ to _$₀_; F₁ to _$₁_)
  open NaturalTransformation

  private
    infix  4 _≈_ _⇒_
    infixr 9 _∘_

    module B = Bicategory (1-Category b (Category.op C))
    module C = Category C
    module _ {x y} where
      open Functor (PF {x} {y}) public
        renaming (F₀ to P₁; F₁ to P₂; F-resp-≈ to P-resp-≈)

    open Functor

    module _ {x y : C.Obj} where
      open Category (P₀ x)
      open HomReasoning

      -- A helper lemma.

      P-resp-Iso : ∀ {f g : C [ x , y ]} (eq : C [ f ≈ g ]) {a} →
                   Iso (P₀ x) (η (P₂ eq) a) (η (P₂ $ C.Equiv.sym eq) a)
      P-resp-Iso eq {a} = record
        { isoˡ = begin
            η (P₂ $ C.Equiv.sym eq) a ∘ η (P₂ eq) a       ≈˘⟨ homomorphism PF ⟩
            η (P₂ $ C.Equiv.trans eq (C.Equiv.sym eq)) a  ≈⟨ P-resp-≈ _ ⟩
            η (P₂ C.Equiv.refl) a                         ≈⟨ identity PF ⟩
            id                                            ∎
        ; isoʳ = begin
            η (P₂ eq) a ∘ η (P₂ $ C.Equiv.sym eq) a       ≈˘⟨ homomorphism PF ⟩
            η (P₂ $ C.Equiv.trans (C.Equiv.sym eq) eq) a  ≈⟨ P-resp-≈ _ ⟩
            η (P₂ C.Equiv.refl) a                         ≈⟨ identity PF ⟩
            id                                            ∎
        }

    -- Objects and morphism

    Obj : Set (o ⊔ o′)
    Obj = Σ C.Obj (λ x → Category.Obj $ P₀ x)

    _⇒_ : Obj → Obj → Set (ℓ ⊔ ℓ′)
    (x₁ , a₁) ⇒ (x₂ , a₂) = Σ (x₁ C.⇒ x₂) λ f → P₀ x₁ [ a₁ , P₁ f $₀ a₂ ]

    -- Pairwise equivalence
    --
    -- The second components of equal morphisms don't live in the same
    -- homset because their domains don't agree 'on the nose'.  Hence
    -- the second components are equal only up to coherent iso.  This
    -- substantially complicates the proofs of associativity, the unit
    -- laws and functionality of composition.

    _≈_ : ∀ {A B} (f₁ f₂ : A ⇒ B) → Set (e ⊔ e′)
    _≈_ {x₁ , a₁} {x₂ , a₂} (f₁ , g₁) (f₂ , g₂) =
      Σ (f₁ C.≈ f₂) λ eq → η (P₂ $ eq) a₂ D.∘ g₁ D.≈ g₂
      where module D = Category (P₀ x₁)

    -- Identity and composition

    id : ∀ {A} → A ⇒ A
    id {_ , a} = C.id , η (unitˡ.η _) a

    _∘_ : ∀ {A B C} → B ⇒ C → A ⇒ B → A ⇒ C
    _∘_ {x₁ , a₁} {_ , a₂} {_ , a₃} (f₁ , g₁) (f₂ , g₂) =
      f₁ C.∘ f₂ , (η (Hom.η (f₂ , f₁)) a₃ D.∘ P₁ f₂ $₁ g₁) D.∘ g₂
      where module D = Category (P₀ x₁)

    -- Associativity and unit laws.
    --
    -- Because the second component of equality only holds up to
    -- coherent iso, we need to invoke the coherence conditions
    -- associated with the pseudofunctor P to establish associativity.
    --
    -- Once we realize this, the proofs are not particularly hard, but
    -- long and tedious (especially that of associativity), mostly
    -- because they involve re-arranging lots of parentheses via
    -- manual application of the underlying associativity laws.

    assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} →
            (h ∘ g) ∘ f ≈ h ∘ (g ∘ f)
    assoc {x₁ , _} {x₂ , _} {x₃ , a₃} {_ , a₄} {f₁ , g₁} {f₂ , g₂} {f₃ , g₃} =
      C.assoc ,
      (begin
        η (P₂ C.assoc) a₄ ∙
        (η (Hom.η (f₁ , f₃ C.∘ f₂)) a₄ ∙
         P₁ f₁ $₁ ((η (Hom.η (f₂ , f₃)) a₄ E.∘ P₁ f₂ $₁ g₃) E.∘ g₂)) ∙ g₁
      ≈⟨ ∘-resp-≈ʳ $ ∘-resp-≈ˡ $ ∘-resp-≈ʳ $ F-resp-≈ (P₁ f₁) E.assoc  ⟩
        η (P₂ C.assoc) a₄ ∙
        (η (Hom.η (f₁ , f₃ C.∘ f₂)) a₄ ∙
         P₁ f₁ $₁ (η (Hom.η (f₂ , f₃)) a₄ E.∘ P₁ f₂ $₁ g₃ E.∘ g₂)) ∙ g₁
      ≈⟨ ∘-resp-≈ʳ $ ∘-resp-≈ˡ $ ∘-resp-≈ʳ $ homomorphism (P₁ f₁) ⟩
        η (P₂ C.assoc) a₄ ∙
        (η (Hom.η (f₁ , f₃ C.∘ f₂)) a₄ ∙
         P₁ f₁ $₁ η (Hom.η (f₂ , f₃)) a₄ ∙
         P₁ f₁ $₁ (P₁ f₂ $₁ g₃ E.∘ g₂)) ∙ g₁
      ≈˘⟨ D.assoc                          then
          D.Equiv.sym $ ∘-resp-≈ʳ D.assoc  then
          ∘-resp-≈ʳ $ ∘-resp-≈ˡ $ D.assoc  ⟩
        (η (P₂ C.assoc) a₄ ∙
         η (Hom.η (f₁ , f₃ C.∘ f₂)) a₄ ∙
         P₁ f₁ $₁ η (Hom.η (f₂ , f₃)) a₄) ∙
        P₁ f₁ $₁ (P₁ f₂ $₁ g₃ E.∘ g₂) ∙ g₁
      ≈˘⟨ ∘-resp-≈ˡ $ ∘-resp-≈ʳ $ ∘-resp-≈ʳ (D.identityʳ then D.identityʳ) ⟩
        (η (P₂ C.assoc) a₄ ∙
         η (Hom.η (f₁ , f₃ C.∘ f₂)) a₄ ∙
         (P₁ f₁ $₁ η (Hom.η (f₂ , f₃)) a₄ ∙ D.id) ∙ D.id) ∙
        P₁ f₁ $₁ ((P₁ f₂ $₁ g₃) E.∘ g₂) ∙ g₁
      ≈˘⟨ ∘-resp-≈ˡ $ ∘-resp-≈ʳ P-assoc ⟩
        (η (P₂ C.assoc) a₄ ∙
         η (P₂ C.sym-assoc) a₄ ∙
         η (Hom.η (f₂ C.∘ f₁ , f₃)) a₄ ∙ P₁ (f₂ C.∘ f₁) $₁ F.id ∙
         η (Hom.η (f₁ , f₂)) (P₁ f₃ $₀ a₄)) ∙
        P₁ f₁ $₁ ((P₁ f₂ $₁ g₃) E.∘ g₂) ∙ g₁
      ≈˘⟨ ∘-resp-≈ˡ D.assoc ⟩
        ((η (P₂ C.assoc) a₄ ∙ η (P₂ C.sym-assoc) a₄) ∙
         η (Hom.η (f₂ C.∘ f₁ , f₃)) a₄ ∙ P₁ (f₂ C.∘ f₁) $₁ F.id ∙
         η (Hom.η (f₁ , f₂)) (P₁ f₃ $₀ a₄)) ∙
        P₁ f₁ $₁ ((P₁ f₂ $₁ g₃) E.∘ g₂) ∙ g₁
      ≈⟨ ∘-resp-≈ˡ $ ∘-resp-≈ˡ $
         (sym (homomorphism PF) then P-resp-≈ _ then identity PF) ⟩
        (D.id ∙
         η (Hom.η (f₂ C.∘ f₁ , f₃)) a₄ ∙ P₁ (f₂ C.∘ f₁) $₁ F.id ∙
         η (Hom.η (f₁ , f₂)) (P₁ f₃ $₀ a₄)) ∙
        P₁ f₁ $₁ ((P₁ f₂ $₁ g₃) E.∘ g₂) ∙ g₁
      ≈⟨ ∘-resp-≈ D.identityˡ (∘-resp-≈ˡ $ homomorphism (P₁ f₁) ) ⟩
        (η (Hom.η (f₂ C.∘ f₁ , f₃)) a₄ ∙ P₁ (f₂ C.∘ f₁) $₁ F.id ∙
         η (Hom.η (f₁ , f₂)) (P₁ f₃ $₀ a₄)) ∙
        (P₁ f₁ $₁ (P₁ f₂ $₁ g₃) ∙ P₁ f₁ $₁ g₂) ∙ g₁
      ≈⟨ ∘-resp-≈ (D.Equiv.sym D.assoc) D.assoc  then
         D.assoc                                 then
         ∘-resp-≈ʳ (D.Equiv.sym D.assoc)         ⟩
        (η (Hom.η (f₂ C.∘ f₁ , f₃)) a₄ ∙ P₁ (f₂ C.∘ f₁) $₁ F.id) ∙
        (η (Hom.η (f₁ , f₂)) (P₁ f₃ $₀ a₄) ∙ P₁ f₁ $₁ (P₁ f₂ $₁ g₃)) ∙
        P₁ f₁ $₁ g₂ ∙ g₁
      ≈⟨ ∘-resp-≈ʳ $ ∘-resp-≈ˡ (commute (Hom.η (f₁ , f₂)) g₃) ⟩
        (η (Hom.η (f₂ C.∘ f₁ , f₃)) a₄ ∙ P₁ (f₂ C.∘ f₁) $₁ F.id) ∙
        (P₁ (f₂ C.∘ f₁) $₁ g₃ ∙ η (Hom.η (f₁ , f₂)) a₃) ∙
        P₁ f₁ $₁ g₂ ∙ g₁
      ≈⟨ ∘-resp-≈ˡ (∘-resp-≈ʳ (identity (P₁ (f₂ C.∘ f₁))) then D.identityʳ) ⟩
        η (Hom.η (f₂ C.∘ f₁ , f₃)) a₄ ∙
        (P₁ (f₂ C.∘ f₁) $₁ g₃ ∙ η (Hom.η (f₁ , f₂)) a₃) ∙
        P₁ f₁ $₁ g₂ ∙ g₁
      ≈⟨ ∘-resp-≈ʳ D.assoc                then
         D.Equiv.sym D.assoc              then
         ∘-resp-≈ʳ (D.Equiv.sym D.assoc)  ⟩
        (η (Hom.η (f₂ C.∘ f₁ , f₃)) a₄ ∙ (P₁ (f₂ C.∘ f₁) $₁ g₃)) ∙
        (η (Hom.η (f₁ , f₂)) a₃ ∙ (P₁ f₁ $₁ g₂)) ∙ g₁
      ∎)
      where
        module D = Category (P₀ x₁)
        module E = Category (P₀ x₂)
        module F = Category (P₀ x₃)
        open D renaming (_∘_ to _∙_)
        infixl -5 _then_
        _then_ = Equiv.trans
        open HomReasoning

    identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
    identityˡ {x₁ , _} {_ , a₂} {f , g} =
      C.identityˡ ,
      (begin
        η (P₂ C.identityˡ) a₂ ∙
        ((η (Hom.η (f , C.id)) a₂ ∙ P₁ f $₁ η (unitˡ.η _) a₂) ∙ g)
      ≈˘⟨ D.assoc ⟩
        (η (P₂ C.identityˡ) a₂ ∙
         (η (Hom.η (f , C.id)) a₂ ∙ P₁ f $₁ η (unitˡ.η _) a₂)) ∙ g
      ≈˘⟨ ∘-resp-≈ˡ (∘-resp-≈ʳ (∘-resp-≈ʳ D.identityʳ)) ⟩
        (η (P₂ C.identityˡ) a₂ ∙
         (η (Hom.η (f , C.id)) a₂ ∙ (P₁ f $₁ η (unitˡ.η _) a₂ ∙ D.id))) ∙ g
      ≈⟨ ∘-resp-≈ˡ unitaryʳ ⟩
        D.id ∙ g
      ≈⟨ D.identityˡ ⟩
        g
      ∎)
      where
        module D = Category (P₀ x₁)
        open D renaming (_∘_ to _∙_)
        open HomReasoning

    identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f
    identityʳ {x₁ , a₁} {_ , a₂} {f , g} =
      C.identityʳ ,
      (begin
        η (P₂ C.identityʳ) a₂ ∙
        ((η (Hom.η (C.id , f)) a₂ ∙ P₁ C.id $₁ g) ∙ η (unitˡ.η _) a₁)
      ≈⟨ ∘-resp-≈ʳ D.assoc ⟩
        η (P₂ C.identityʳ) a₂ ∙
        (η (Hom.η (C.id , f)) a₂ ∙ (P₁ C.id $₁ g ∙ η (unitˡ.η _) a₁))
      ≈˘⟨ ∘-resp-≈ʳ $ ∘-resp-≈ʳ $ commute (unitˡ.η _) g ⟩
        η (P₂ C.identityʳ) a₂ ∙
        (η (Hom.η (C.id , f)) a₂ ∙ (η (unitˡ.η _) (P₁ f $₀ a₂) ∙ g))
      ≈˘⟨ ∘-resp-≈ʳ D.assoc ⟩
        η (P₂ C.identityʳ) a₂ ∙
        ((η (Hom.η (C.id , f)) a₂ ∙ η (unitˡ.η _) (P₁ f $₀ a₂)) ∙ g)
      ≈˘⟨ D.assoc ⟩
        (η (P₂ C.identityʳ) a₂ ∙
         (η (Hom.η (C.id , f)) a₂ ∙ η (unitˡ.η _) (P₁ f $₀ a₂))) ∙ g
      ≈˘⟨ ∘-resp-≈ˡ $ ∘-resp-≈ʳ $ ∘-resp-≈ʳ D.identityˡ ⟩
        (η (P₂ C.identityʳ) a₂ ∙
         (η (Hom.η (C.id , f)) a₂ ∙ (D.id ∙ η (unitˡ.η _) (P₁ f $₀ a₂)))) ∙ g
      ≈˘⟨ ∘-resp-≈ˡ $ ∘-resp-≈ʳ $ ∘-resp-≈ʳ $
          ∘-resp-≈ˡ $ identity (P₁ C.id) ⟩
        (η (P₂ C.identityʳ) a₂ ∙
         (η (Hom.η (C.id , f)) a₂ ∙
          ((P₁ C.id $₁ D.id) ∙ η (unitˡ.η _) (P₁ f $₀ a₂)))) ∙ g
      ≈⟨ ∘-resp-≈ˡ unitaryˡ ⟩
        D.id ∙ g
      ≈⟨ D.identityˡ ⟩
        g
      ∎)
      where
        module D = Category (P₀ x₁)
        open D renaming (_∘_ to _∙_)
        open HomReasoning

    -- Pair-wise equality is an equivalence

    refl : ∀ {A B} {f : A ⇒ B} → f ≈ f
    refl {x , _} =
      C.Equiv.refl , D.Equiv.trans (D.∘-resp-≈ˡ (identity PF)) D.identityˡ
      where module D = Category (P₀ x)

    sym : ∀ {A B} {f g : A ⇒ B} → f ≈ g → g ≈ f
    sym {x₁ , _} {_ , a₂} {_ , g₁} {_ , g₂} (f₁≈f₂ , g₁≈g₂) =
      C.Equiv.sym f₁≈f₂ ,
      (begin
         η (P₂ $ C.Equiv.sym f₁≈f₂) a₂ ∙ g₂
       ≈˘⟨ ∘-resp-≈ʳ g₁≈g₂ ⟩
         η (P₂ $ C.Equiv.sym f₁≈f₂) a₂ ∙ η (P₂ f₁≈f₂) a₂ ∙ g₁
       ≈˘⟨ D.assoc ⟩
         (η (P₂ $ C.Equiv.sym f₁≈f₂) a₂ ∙ η (P₂ f₁≈f₂) a₂) ∙ g₁
       ≈⟨ ∘-resp-≈ˡ $ Iso.isoˡ $ P-resp-Iso f₁≈f₂ ⟩
         D.id ∙ g₁
       ≈⟨ D.identityˡ ⟩
         g₁
       ∎)
      where
        module D = Category (P₀ x₁)
        open D renaming (_∘_ to _∙_)
        open HomReasoning

    trans : ∀ {A B} {f g h : A ⇒ B} → f ≈ g → g ≈ h → f ≈ h
    trans {x₁ , _} {_ , a₂} {_ , g₁} {_ , g₂} {_ , g₃}
          (f₁≈f₂ , g₁≈g₂) (f₂≈f₃ , g₂≈g₃) =
      C.Equiv.trans f₁≈f₂ f₂≈f₃ ,
      (begin
         η (P₂ $ C.Equiv.trans f₁≈f₂ f₂≈f₃) a₂ ∙ g₁
       ≈⟨ ∘-resp-≈ˡ $ homomorphism PF ⟩
         (η (P₂ f₂≈f₃) a₂ ∙ η (P₂ f₁≈f₂) a₂) ∙ g₁
       ≈⟨ D.assoc ⟩
         η (P₂ f₂≈f₃) a₂ ∙ η (P₂ f₁≈f₂) a₂ ∙ g₁
       ≈⟨ ∘-resp-≈ʳ g₁≈g₂ ⟩
         η (F₁ PF f₂≈f₃) a₂ ∙ g₂
       ≈⟨ g₂≈g₃ ⟩
         g₃
       ∎)
      where
        module D = Category (P₀ x₁)
        open D renaming (_∘_ to _∙_)
        open HomReasoning

    ≈-equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
    ≈-equiv = record
      { refl  = refl
      ; sym   = sym
      ; trans = trans
      }

    -- Functionality of composition
    --
    -- The key here is to use naturality of P-homomorphism to relate
    -- functionality of composition (∘) in C to functoriality of
    -- composition (⊚) in (P₀ x₁).

    ∘-resp-≈ : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} →
               f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i
    ∘-resp-≈ {x₁ , _} {x₂ , a₂} {_ , a₃}
             {f₁ , g₁} {f₂ , g₂} {f₃ , g₃} {f₄ , g₄}
             (f₁≈f₂ , g₁≈g₂) (f₃≈f₄ , g₃≈g₄) =
             C.∘-resp-≈ f₁≈f₂ f₃≈f₄ ,
             (begin
                η (P₂ $ C.∘-resp-≈ f₁≈f₂ f₃≈f₄) a₃ ∙
                (η (Hom.η (f₃ , f₁)) a₃ ∙ P₁ f₃ $₁ g₁) ∙ g₃
              ≈⟨ ∘-resp-≈ʳ D.assoc  then  D.Equiv.sym D.assoc ⟩
                (η (P₂ $ C.∘-resp-≈ f₁≈f₂ f₃≈f₄) a₃ ∙ η (Hom.η (f₃ , f₁)) a₃) ∙
                P₁ f₃ $₁ g₁ ∙ g₃
              ≈˘⟨ ∘-resp-≈ˡ $ Hom.commute (f₃≈f₄ , f₁≈f₂) ⟩
                (η (Hom.η (f₄ , f₂)) a₃ ∙
                 P₁ f₄ $₁ (η (P₂ f₁≈f₂) a₃) ∙ η (P₂ f₃≈f₄) (P₁ f₁ $₀ a₃)) ∙
                P₁ f₃ $₁ g₁ ∙ g₃
              ≈⟨ D.assoc                                   then
                 ∘-resp-≈ʳ D.assoc                         then
                 ∘-resp-≈ʳ $ ∘-resp-≈ʳ $ Equiv.sym D.assoc ⟩
                η (Hom.η (f₄ , f₂)) a₃ ∙
                P₁ f₄ $₁ (η (P₂ f₁≈f₂) a₃) ∙
                (η (P₂ f₃≈f₄) (P₁ f₁ $₀ a₃) ∙ P₁ f₃ $₁ g₁) ∙ g₃
              ≈⟨ ∘-resp-≈ʳ $ ∘-resp-≈ʳ $ ∘-resp-≈ˡ (commute (P₂ f₃≈f₄) g₁) ⟩
                η (Hom.η (f₄ , f₂)) a₃ ∙
                P₁ f₄ $₁ (η (P₂ f₁≈f₂) a₃) ∙
                (P₁ f₄ $₁ g₁ ∙ η (P₂ f₃≈f₄) a₂) ∙ g₃
              ≈⟨ ∘-resp-≈ʳ $ ∘-resp-≈ʳ D.assoc    then
                 Equiv.sym $ ∘-resp-≈ʳ $ D.assoc  then
                 Equiv.sym $ D.assoc              ⟩
                (η (Hom.η (f₄ , f₂)) a₃ ∙
                 P₁ f₄ $₁ (η (P₂ f₁≈f₂) a₃) ∙ P₁ f₄ $₁ g₁) ∙
                η (P₂ f₃≈f₄) a₂ ∙ g₃
              ≈˘⟨ ∘-resp-≈ˡ $ ∘-resp-≈ʳ $ homomorphism (P₁ f₄) ⟩
                (η (Hom.η (f₄ , f₂)) a₃ ∙
                 P₁ f₄ $₁ (η (P₂ f₁≈f₂) a₃ E.∘ g₁)) ∙
                η (P₂ f₃≈f₄) a₂ ∙ g₃
              ≈⟨ D.∘-resp-≈ (∘-resp-≈ʳ (F-resp-≈ (P₁ f₄) g₁≈g₂)) g₃≈g₄ ⟩
                (η (Hom.η (f₄ , f₂)) a₃ ∙ P₁ f₄ $₁ g₂) ∙ g₄
              ∎)
      where
        module D = Category (P₀ x₁)
        module E = Category (P₀ x₂)
        open D renaming (_∘_ to _∙_)
        infixl -5 _then_
        _then_ = Equiv.trans
        open HomReasoning

  Grothendieck : Category (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
  Grothendieck = record
    { Obj       = Obj
    ; _⇒_       = _⇒_
    ; _≈_       = _≈_
    ; id        = id
    ; _∘_       = _∘_
    ; assoc     = assoc
    ; sym-assoc = sym assoc
    ; identityˡ = identityˡ
    ; identityʳ = identityʳ
    ; identity² = identityˡ
    ; equiv     = ≈-equiv
    ; ∘-resp-≈  = ∘-resp-≈
    }

ext: agda

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
------------------------------------------------------------------------
-- Embeddings
------------------------------------------------------------------------

-- Partially following the HoTT book.

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

open import Equality

module Embedding
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)

open import Bijection eq using (_↔_)
open Derived-definitions-and-properties eq
open import Equivalence eq as Eq hiding (id; _∘_)
import Equivalence.Half-adjoint eq as HA
open import Excluded-middle eq
open import H-level eq
open import H-level.Closure eq
open import Injection eq as Injection using (Injective; _↣_)
open import Preimage eq using (_⁻¹_)
open import Surjection eq using (_↠_)

private
  variable
    a b t : Level
    A B C : Type a
    f x y : A

------------------------------------------------------------------------
-- Embeddings

-- The property of being an embedding.

Is-embedding : {A : Type a} {B : Type b} → (A → B) → Type (a ⊔ b)
Is-embedding f = ∀ x y → Is-equivalence (cong {x = x} {y = y} f)

-- Is-embedding is propositional (assuming extensionality).

Is-embedding-propositional :
  {A : Type a} {B : Type b} {f : A → B} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  Is-proposition (Is-embedding f)
Is-embedding-propositional {b = b} ext =
  Π-closure (lower-extensionality b lzero ext) 1 λ _ →
  Π-closure (lower-extensionality b lzero ext) 1 λ _ →
  Eq.propositional ext _

-- Embeddings.

record Embedding (From : Type f) (To : Type t) : Type (f ⊔ t) where
  field
    to           : From → To
    is-embedding : Is-embedding to

  equivalence : (x ≡ y) ≃ (to x ≡ to y)
  equivalence = ⟨ _ , is-embedding _ _ ⟩

-- The type family above could have been defined using Σ.

Embedding-as-Σ : Embedding A B ↔ ∃ λ (f : A → B) → Is-embedding f
Embedding-as-Σ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ emb → Embedding.to emb , Embedding.is-embedding emb
      ; from = λ { (f , is) → record { to = f; is-embedding = is } }
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- Equivalences are embeddings.

Is-equivalence→Is-embedding :
  Is-equivalence f → Is-embedding f
Is-equivalence→Is-embedding is-equiv _ _ =
  _≃_.is-equivalence (Eq.inverse (Eq.≃-≡ Eq.⟨ _ , is-equiv ⟩))

-- Equivalences can be converted to embeddings.

≃→Embedding :
  A ≃ B → Embedding A B
≃→Embedding A≃B = record
  { to           = _≃_.to A≃B
  ; is-embedding =
      Is-equivalence→Is-embedding (_≃_.is-equivalence A≃B)
  }

------------------------------------------------------------------------
-- Preorder

-- Embedding is a preorder.

id : Embedding A A
id {A = A} = record
  { to           = P.id
  ; is-embedding = λ x y →
      Eq.respects-extensional-equality
        cong-id
        HA.id-equivalence
  }

infixr 9 _∘_

_∘_ : Embedding B C → Embedding A B → Embedding A C
f ∘ g = record
  { to           = to f ⊚ to g
  ; is-embedding = λ _ _ →
      Eq.respects-extensional-equality
        (cong-∘ (to f) (to g))
        (HA.composition-equivalence
           (is-embedding f _ _)
           (is-embedding g _ _))
  }
  where
  open Embedding

------------------------------------------------------------------------
-- Preimages

-- If f is an embedding, then f ⁻¹ y is propositional.
--
-- This result is taken (perhaps with some changes) from the proof of
-- Theorem 4.6.3 in the HoTT book (first edition).

embedding→⁻¹-propositional :
  Is-embedding f →
  ∀ y → Is-proposition (f ⁻¹ y)
embedding→⁻¹-propositional {f = f} is-emb y (x₁ , eq₁) (x₂ , eq₂) =
  let
    equiv : (x₁ ≡ x₂) ≃ (f x₁ ≡ f x₂)
    equiv = ⟨ _ , is-emb _ _ ⟩

    x₁≡x₂ : x₁ ≡ x₂
    x₁≡x₂ = _≃_.from equiv
      (f x₁  ≡⟨ eq₁ ⟩
       y     ≡⟨ sym eq₂ ⟩∎
       f x₂  ∎)
  in
  Σ-≡,≡→≡
    x₁≡x₂
    (subst (λ z → f z ≡ y) x₁≡x₂ eq₁              ≡⟨ subst-∘ (_≡ y) f x₁≡x₂ ⟩
     subst (_≡ y) (cong f x₁≡x₂) eq₁              ≡⟨ cong (λ eq → subst (_≡ y) eq eq₁) $ sym $ sym-sym (cong f x₁≡x₂) ⟩
     subst (_≡ y) (sym $ sym $ cong f x₁≡x₂) eq₁  ≡⟨ subst-trans (sym $ cong f x₁≡x₂) ⟩
     trans (sym $ cong f x₁≡x₂) eq₁               ≡⟨ cong (λ eq → trans (sym eq) eq₁) $ _≃_.right-inverse-of equiv _ ⟩
     trans (sym $ trans eq₁ (sym eq₂)) eq₁        ≡⟨ cong (flip trans eq₁) $ sym-trans eq₁ (sym eq₂) ⟩
     trans (trans (sym (sym eq₂)) (sym eq₁)) eq₁  ≡⟨ trans-[trans-sym]- _ eq₁ ⟩
     sym (sym eq₂)                                ≡⟨ sym-sym _ ⟩∎
     eq₂                                          ∎)

------------------------------------------------------------------------
-- Injections

-- Functions that are embeddings are injective.

injective : Is-embedding f → Injective f
injective is-emb = _≃_.from ⟨ _ , is-emb _ _ ⟩

-- Embeddings are injections.

injection : Embedding A B → A ↣ B
injection f = record
  { to        = Embedding.to f
  ; injective = injective (Embedding.is-embedding f)
  }

private

  -- If the domain of f is a set, then Injective f is propositional
  -- (assuming extensionality).

  Injective-propositional :
    {A : Type a} {B : Type b} {f : A → B} →
    Extensionality (a ⊔ b) (a ⊔ b) →
    Is-set A → Is-proposition (Injective f)
  Injective-propositional {a = a} {b = b} ext A-set =
    implicit-Π-closure (lower-extensionality b lzero ext) 1 λ _ →
    implicit-Π-closure (lower-extensionality b lzero ext) 1 λ _ →
    Π-closure (lower-extensionality a b ext)              1 λ _ →
    A-set

-- For functions between sets the property of being injective is
-- logically equivalent to the property of being an embedding.

Injective⇔Is-embedding :
  Is-set A → Is-set B →
  (f : A → B) → Injective f ⇔ Is-embedding f
Injective⇔Is-embedding A-set B-set f = record
  { to   = λ cong-f⁻¹ _ _ →
               _≃_.is-equivalence $
               _↠_.from (≃↠⇔ A-set B-set)
                        (record { from = cong-f⁻¹ })
  ; from = injective
  }

-- For functions between sets the property of being injective is
-- equivalent to the property of being an embedding (assuming
-- extensionality).

Injective≃Is-embedding :
  {A : Type a} {B : Type b} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  Is-set A → Is-set B →
  (f : A → B) → Injective f ≃ Is-embedding f
Injective≃Is-embedding ext A-set B-set f =
  _↔_.to
    (⇔↔≃ ext
         (Injective-propositional ext A-set)
         (Is-embedding-propositional ext))
    (Injective⇔Is-embedding A-set B-set f)

-- If A and B are sets, then the type of injections from A to B is
-- isomorphic to the type of embeddings from A to B (assuming
-- extensionality).

↣↔Embedding :
  {A : Type a} {B : Type b} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  Is-set A → Is-set B →
  (A ↣ B) ↔ Embedding A B
↣↔Embedding {A = A} {B = B} ext A-set B-set = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ f → record
                 { to           = _↣_.to f
                 ; is-embedding =
                     _≃_.to (Injective≃Is-embedding ext A-set B-set _)
                            (_↣_.injective f)
                 }
      ; from = injection
      }
    ; right-inverse-of = λ f →
        cong (uncurry λ to (emb : Is-embedding to) →
                        record { to = to; is-embedding = emb })
             (Σ-≡,≡→≡ (refl _)
                      (Is-embedding-propositional ext _ _))
    }
  ; left-inverse-of = λ f →
      cong (uncurry λ to (inj : Injective to) →
                      record { to = to; injective = inj })
           (Σ-≡,≡→≡ (refl _)
                    (Injective-propositional ext A-set _ _))
  }

------------------------------------------------------------------------
-- Surjections

-- If excluded middle holds, then an embedding from an inhabited type
-- can be turned into a (split) surjection in the other direction.

Embedding→↠ :
  {A : Type a} {B : Type b} →
  Excluded-middle (a ⊔ b) →
  A → Embedding A B → B ↠ A
Embedding→↠ {A = A} {B = B} em a A↣B = record
  { logical-equivalence = record
    { to   = from
    ; from = to
    }
  ; right-inverse-of = from-to
  }
  where
  open Embedding A↣B

  prop : ∀ b → Is-proposition (to ⁻¹ b)
  prop = embedding→⁻¹-propositional is-embedding

  from : B → A
  from b = case em (prop b) of λ where
    (yes (a , _)) → a
    (no _)        → a

  from-to : ∀ a → from (to a) ≡ a
  from-to a with em (prop (to a))
  ... | (yes (a′ , to-a′≡to-a)) = injective is-embedding to-a′≡to-a
  ... | (no  hyp)               = ⊥-elim (hyp (a , refl _))

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Relation.Binary.Core

module Heapsort.Impl1 {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import BBHeap _≤_ hiding (flatten)
open import BBHeap.Heapify _≤_ tot≤ trans≤
open import BHeap _≤_ hiding (flatten)
open import BHeap.Order _≤_
open import BHeap.Order.Properties _≤_
open import BHeap.Properties _≤_
open import Bound.Lower A
open import Data.List
open import OList _≤_

flatten : {b : Bound}(h : BHeap b) → Acc h → OList b
flatten lf _ = onil
flatten (nd {x = x} b≤x l r) (acc rs) = :< b≤x (flatten (merge tot≤ l r) (rs (merge tot≤ l r) (lemma-merge≤′ tot≤ b≤x l r)))

heapsort : List A → OList bot
heapsort xs = flatten (relax (heapify xs)) (≺-wf (relax (heapify xs)))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module jarsec where

open import Algebra
open import Data.Bool
open import Data.Char
-- open import Data.Empty
-- open import Data.Fin
open import Data.List
open import Data.Maybe hiding (map)
open import Data.Nat
open import Data.Nat.Base
open import Data.Nat.Show
-- open import Data.Integer
open import Data.Product hiding (map)
open import Data.Sum hiding (map)
open import Data.String hiding (length)
open import Function
-- open import Data.Sum
-- open import Data.Unit
-- open import Data.Vec
open import Category.Functor
open import Relation.Binary
open import Data.Char.Base
open import Agda.Builtin.Char
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

record Parser (A : Set) : Set where
  constructor mk-parser
  field
    parse : List Char → (List (A × (List Char)))
open Parser public

item : Parser Char
item = mk-parser λ where
  [] → []
  (c ∷ cs) → (c , cs) ∷ []

bind : ∀ { A B : Set } → Parser A → (A → Parser B) → Parser B
bind {A} p f = mk-parser $ λ cs →
  let rs : List (A × List Char)
      rs = parse p cs
  in concatMap (λ x → parse (f (proj₁ x)) (proj₂ x)) rs
  -- in concatMap (λ where (x , cs′) → parse (f x) cs′) rs

_>>=_ : ∀ { A B : Set } → Parser A → (A → Parser B) → Parser B
p >>= f = bind p f

_>>_ : ∀ { A B : Set } → Parser A → Parser B → Parser B
pA >> pB = pA >>= λ _ → pB

unit : ∀ { A : Set } → A → Parser A
unit a = mk-parser (λ str → ( a , str ) ∷ [])

unit* : ∀ { A : Set } → List A → Parser A
unit* xs = mk-parser (λ str → foldl (λ sum x → (x , str) ∷ sum) [] xs)

fmap : ∀ { A B : Set } → (A → B) → Parser A → Parser B
fmap f p = do
  a ← p
  unit (f a)

_<$>_ : ∀ { A B : Set } → (A → B) → Parser A → Parser B
f <$> p = fmap f p

_<*>_ : ∀ {A B : Set } → Parser A → Parser B → Parser ( A × B )
aP <*> bP = do
  a ← aP
  b ← bP
  unit (a , b)

combine : { A : Set } → Parser A → Parser A → Parser A
combine p q = mk-parser (λ cs → (parse p cs) Data.List.++ (parse q cs))

failure : { A : Set } → Parser A
failure = mk-parser (λ cs → [])

option : { A : Set } → Parser A → Parser A → Parser A
option p q = mk-parser $ λ where
  cs → case (parse p cs) of λ where
    [] → parse q cs
    result → result

{-# TERMINATING #-}
mutual
  many* : { A : Set } → Parser A → Parser (List A)
  many* v = option (many+ v) (unit [])

  many+ : { A : Set } → Parser A → Parser (List A)
  many+ v = fmap (λ { (a , list) → a ∷ list }) (v <*> (many* v))

satisfy : (Char -> Bool) -> Parser Char
satisfy f = do
  c ← item
  case (f c) of λ where
    true → unit c
    false → failure

oneOf : List Char → Parser Char
oneOf options = satisfy (flip elem options)
  where
  elem : Char → List Char → Bool
  elem a [] = false
  elem a (x ∷ xs) = case primCharEquality a x of λ where
    true → true
    false → elem a xs

module _ { A : Set } where
  {-# TERMINATING #-}
  chainl1 : Parser A → Parser (A → A → A) → Parser A
  chainl1 p op = do
    a ← p
    rest a
    where
      rest : A → Parser A
      rest a = option (do
        f ← op
        b ← p
        rest (f a b)) (unit a)

chainl : { A : Set } → Parser A → Parser (A → A → A) → A → Parser A
chainl p op a = option (chainl1 p op) (unit a)

char : Char → Parser Char
char c = satisfy (primCharEquality c)

digit : Parser Char
digit = satisfy isDigit

-- TODO: Remove
∣_-_∣ : ℕ → ℕ → ℕ
∣ zero  - y     ∣ = y
∣ x     - zero  ∣ = x
∣ suc x - suc y ∣ = ∣ x - y ∣

natural : Parser ℕ
natural = natFromList <$> ((map primCharToNat) <$> (many+ digit))
  where
  natFromList : List ℕ → ℕ
  natFromList [] = zero
  natFromList (n ∷ ns) =
    let len = length ns
    in (∣ n - 48 ∣ + (10 * len)) + (natFromList ns)

string : String → Parser String
string str = primStringFromList <$> (string-chars (primStringToList str))
  where
  string-chars : List Char → Parser (List Char)
  string-chars [] = unit []
  string-chars (c ∷ cs) = do
    char c
    string-chars cs
    unit (c ∷ cs)

spaces : Parser String
spaces = fmap primStringFromList (many* (oneOf (primStringToList " \n\r")))

token : { A : Set } → Parser A → Parser A
token p = do
  a ← p
  spaces
  unit a

reserved : String → Parser String
reserved str = token (string str)

parens : { A : Set } → Parser A → Parser A
parens m = do
  (reserved "(")
  n ← m
  (reserved ")")
  unit n

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

data Expr : Set where
  Invalid : Expr
  -- Var     : Char → Expr
  Lit : ℕ → Expr
  Add : Expr → Expr → Expr
  Mul : Expr → Expr → Expr
  -- Add Sub : Expr → Expr → Expr
  -- Mul Div : Expr → Expr → Expr

eval : Expr → ℕ
eval Invalid = 0
eval (Lit n) = n
eval (Add a b) = eval a + eval b
eval (Mul a b) = eval a * eval b

eval′ : Maybe Expr → ℕ
eval′ (just x) = eval x
eval′ nothing = 0

module _ where
  {-# TERMINATING #-}
  expr : Parser Expr
  {-# TERMINATING #-}
  term : Parser Expr
  {-# TERMINATING #-}
  factor : Parser Expr

  infixOp : {A : Set} → String → (A → A → A) → Parser (A → A → A)
  mulop : Parser (Expr → Expr → Expr)
  addop : Parser (Expr → Expr → Expr)

  number : Parser Expr

  expr = chainl1 term addop

  term = chainl1 factor mulop

  factor = option number (parens expr)

  infixOp x f = reserved x >> unit f

  mulop = infixOp "*" Mul

  addop = infixOp "+" Add

  number = do
    n ← natural
    unit (Lit n)

runParser : { A : Set } → Parser A → String → Maybe A
runParser p str = case (parse p (primStringToList str)) of λ where
  [] → nothing
  (res ∷ xs) → just (proj₁ res)

run : String → Maybe Expr
run = runParser expr

do-everything : String → ℕ
do-everything str = eval′ $ run str

partial-parse :  { A : Set } → Parser A → String → Maybe (List (A × List Char))
partial-parse p str with parse p (primStringToList str)
partial-parse p str | [] = nothing
partial-parse p str | xs = just xs

run-parser : { A : Set } → Parser A → List Char → Maybe (List (A × List Char))
run-parser p str = case (parse p str) of λ where
  [] → nothing
  xs → just xs

max_stars_repo_name: jaywunder/jarsec-verified

max_issues_repo_name: jaywunder/jarsec-verified

max_forks_repo_name: jaywunder/jarsec-verified


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

module HoTT.Identity.Pi where

open variables
private variable f g h : Π A P

module _ {f g : Π A P} where
  -- Axiom 2.9.3 - function extensionality
  postulate
    happly-isequiv : isequiv (happly {f = f} {g})

  module _ where
    open qinv (isequiv→qinv happly-isequiv) renaming (g to happly⁻¹)
    abstract
      funext : f ~ g → f == g
      funext = happly⁻¹
      =Π-η : funext ∘ happly ~ id
      =Π-η = η
      =Π-β : happly ∘ funext ~ id
      =Π-β = ε

=Π-equiv : f == g ≃ f ~ g
=Π-equiv = happly , happly-isequiv

funext-∙ₕ : (α : f ~ g) (β : g ~ h) → funext (α ∙ₕ β) == funext α ∙ funext β
funext-∙ₕ α β = ap funext (funext λ x → (happly (=Π-β α) x ⋆ happly (=Π-β β) x) ⁻¹) ∙ p
  where
  p : funext (happly (funext α) ∙ₕ happly (funext β)) == funext α ∙ funext β
  p rewrite funext α rewrite funext β = =Π-η refl

funext-ap : {P : A → 𝒰 i} {Q : A → 𝒰 j} {g h : Π A P}
            (f : {a : A} → P a → Q a) (α : g ~ h) →
            funext (ap f ∘ α) == ap (f ∘_) (funext α)
funext-ap f α = ap (λ α → funext (ap f ∘ α)) (=Π-β α) ⁻¹ ∙ p
  where
  p : funext (ap f ∘ happly (funext α)) == ap (f ∘_) (funext α)
  p rewrite funext α = =Π-η refl

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
open import MJ.Types
import MJ.Classtable.Core as Core

module MJ.Syntax.Untyped {c}(Ct : Core.Classtable c) where

open import Prelude
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Data.Maybe.All as MayAll
open import Data.Vec as Vec hiding (_∈_)
open import Data.Star
open import Data.List.Most
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Data.String

import Data.Vec.All as Vec∀

open Core c
open Classtable Ct
open import MJ.Classtable.Membership Ct
open import MJ.LexicalScope Ct

NativeBinOp = ℕ → ℕ → ℕ

data Expr (n : ℕ) : Set where
  new      : Cid c → List (Expr n) → Expr n
  unit     : Expr n
  null     : Expr n
  num      : ℕ → Expr n
  iop      : NativeBinOp → (l r : Expr n) → Expr n
  call     : Expr n → String → List (Expr n) → Expr n
  var      : Fin n → Expr n
  get      : Expr n → String → Expr n

mutual
  data Stmt (i : ℕ) : ℕ → Set where
    loc        : Ty c → Stmt i (suc i)
    asgn       : Fin i → Expr i → Stmt i i
    set        : Expr i → String → Expr i → Stmt i i
    do         : Expr i → Stmt i i
    ret        : Expr i → Stmt i i
    raise      : Stmt i i
    try_catch_ : ∀ {o o'} → Stmt i o → Stmt i o' → Stmt i i
    while_do_  : ∀ {o} → Expr i → Stmt i o → Stmt i i
    block      : ∀ {o} → Stmts i o → Stmt i i

  Stmts : ℕ → ℕ → Set
  Stmts = Star Stmt

data Body (i : ℕ) : Set where
  body : ∀ {o} → Stmts i o → Expr o → Body i

-- let n be the number of formal method arguments
data Method (n : ℕ) : Set where
  super⟨_⟩then_ : List (Expr (suc n)) → Body (suc (suc n)) → Method n
  body          : Body (suc n) → Method n

-- let n be the number of formal constructor arguments
data Constructor (n : ℕ) : Set where
  super_then_ : List (Expr (suc n)) → Body (suc n) → Constructor n
  body        : Body (suc n) → Constructor n

record Implementation (cid : _): Set where
  constructor implementation
  open Class (Σ cid) public
  field
    construct : Constructor (length constr)
    mbodies   : All (λ{ (name , (as , b)) → Method (length as) }) (decls METHOD)

Classes = ∀ cid → Implementation cid

Prog : Set
Prog = Classes × (Body 0)


text:
module DefinitionalEquality where

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

subst : {A : Set}(P : A -> Set){x y : A} -> x == y -> P y -> P x
subst {A} P refl p = p

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

-- This formulation of the associativity law guarantees that for closed n, but
-- possibly open m and p the law holds definitionally.

assoc : (n : Nat) -> (\m p -> n + (m + p)) == (\m p -> (n + m) + p)
assoc zero    = refl
assoc (suc n) = subst (\ ∙ -> f ∙ == f (\m p -> ((n + m) + p)))
                      (assoc n) refl
  where
    f = \(g : Nat -> Nat -> Nat)(m p : Nat) -> suc (g m p)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Agda program using the Iowa Agda library

open import bool

module PROOF-odddoublecoin
  (Choice : Set)
  (choose : Choice → 𝔹)
  (lchoice : Choice → Choice)
  (rchoice : Choice → Choice)
  where

open import eq
open import nat
open import list
open import maybe

---------------------------------------------------------------------------
-- Translated Curry operations:

add : ℕ → ℕ → ℕ
add zero x = x
add (suc y) z = suc (add y z)

-- Forward declaration:
odd : ℕ → 𝔹

even : ℕ → 𝔹
even zero = tt
even (suc x) = odd x

coin : Choice → ℕ → ℕ
coin c1 x = if choose c1 then x else suc x

double : ℕ → ℕ
double x = add x x

odd zero = ff
odd (suc x) = even x

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

add-suc : ∀ (x y : ℕ) → add x (suc y) ≡ suc (add x y)
add-suc zero y = refl
add-suc (suc x) y rewrite add-suc x y = refl

-- auxiliary property for x+x instead of double:
odd-add-x-x : ∀ (x : ℕ) → odd (add x x) ≡ ff
odd-add-x-x zero = refl
odd-add-x-x (suc x) rewrite add-suc x x | odd-add-x-x x = refl

odddoublecoin : (c1 : Choice) → (x : ℕ) → (odd (double (coin c1 x))) ≡ ff
odddoublecoin c1 x rewrite odd-add-x-x (coin c1 x) = refl

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

max_stars_repo_name: phlummox/curry-tools

max_issues_repo_name: phlummox/curry-tools

max_forks_repo_name: phlummox/curry-tools


text:
{-# OPTIONS -v treeless:20 #-}
module _ where

open import Common.Prelude

f : List Nat → List Nat → Nat
f _        []       = 0
f []       (y ∷ ys) = y
f (x ∷ xs) _        = x

main : IO Unit
main = printNat (f [] [])
    ,, printNat (f (1 ∷ []) [])
    ,, printNat (f [] (2 ∷ []))
    ,, printNat (f (3 ∷ []) (4 ∷ []))


text:
module Cats.Category.Product.Binary where

open import Level using (_⊔_)
open import Relation.Binary using (Rel ; IsEquivalence ; _Preserves₂_⟶_⟶_)
open import Relation.Binary.Product.Pointwise using (×-isEquivalence ; Pointwise)

open import Cats.Category.Base
open import Cats.Util.Logic.Constructive using (_∧_ ; _,_)

module Build {lo la l≈ lo′ la′ l≈′}
  (C : Category lo la l≈)
  (D : Category lo′ la′ l≈′)
  where

  infixr 9 _∘_
  infixr 4 _≈_

  private
    module C = Category C
    module D = Category D

  Obj : Set (lo ⊔ lo′)
  Obj = C.Obj ∧ D.Obj

  _⇒_ : Obj → Obj → Set (la ⊔ la′)
  (A , A′) ⇒ (B , B′) = (A C.⇒ B) ∧ (A′ D.⇒ B′)

  _≈_ : ∀ {A B} → Rel (A ⇒ B) (l≈ ⊔ l≈′)
  _≈_ = Pointwise C._≈_ D._≈_

  id : {A : Obj} → A ⇒ A
  id = C.id , D.id

  _∘_ : ∀ {A B C} → B ⇒ C → A ⇒ B → A ⇒ C
  (f , f′) ∘ (g , g′) = f C.∘ g , f′ D.∘ g′

  equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
  equiv = ×-isEquivalence C.equiv D.equiv

  ∘-resp : ∀ {A B C} → _∘_ {A} {B} {C} Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
  ∘-resp (eq₁ , eq₁′) (eq₂ , eq₂′) = C.∘-resp eq₁ eq₂ , D.∘-resp eq₁′ eq₂′

  id-r : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f
  id-r = C.id-r , D.id-r

  id-l : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
  id-l = C.id-l , D.id-l

  assoc : ∀ {A B C D} {f : C ⇒ D} {g : B ⇒ C} {h : A ⇒ B}
    → (f ∘ g) ∘ h ≈ f ∘ (g ∘ h)
  assoc = C.assoc , D.assoc

  _×_ : Category (lo ⊔ lo′) (la ⊔ la′) (l≈ ⊔ l≈′)
  _×_ = record
      { Obj = Obj
      ; _⇒_ = _⇒_
      ; _≈_ = _≈_
      ; id = id
      ; _∘_ = _∘_
      ; equiv = equiv
      ; ∘-resp = ∘-resp
      ; id-r = id-r
      ; id-l = id-l
      ; assoc = assoc
      }

open Build public using (_×_)

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:
module Substitution where

open import Library
open import Terms

-- VarTm n specifies whether the substitution produces variables or terms.
-- The index is used to impose an order on the constructors
-- and so pass termination checking in lift/subst.

data VarTm : ℕ → Set where
  `Var : VarTm 0
  `Tm  : VarTm 1

max01 : ℕ → ℕ → ℕ
max01 0 m = m
max01 n m = n

_∙VT_ : ∀ {m n} → VarTm m → VarTm n → VarTm (max01 m n)
`Var ∙VT vt = vt
`Tm  ∙VT vt = `Tm

VT : ∀ {m} → VarTm m → Cxt → Ty → Set
VT `Var Γ a = Var Γ a
VT `Tm  Γ a = Tm Γ a

vt2tm : ∀ {Γ a m} vt → VT {m} vt Γ a → Tm Γ a
vt2tm `Var x = var x
vt2tm `Tm  t = t

RenSub : ∀ {m} → VarTm m → Cxt → Cxt → Set
RenSub vt Γ Δ = ∀ {a} → Var Γ a → VT vt Δ a

mutual

  -- Lifiting a substitution

  lifts : ∀ {m vt Γ Δ a} → RenSub {m} vt Γ Δ → RenSub vt (a ∷ Γ) (a ∷ Δ)
  lifts {vt = `Var} σ (zero)    = zero
  lifts {vt = `Var} σ (suc x) = suc (σ x)
  lifts {vt = `Tm}  σ (zero)    = var (zero)
  lifts {vt = `Tm}  σ (suc x) = subst {vt = `Var} suc (σ x)

  -- Performing a substitution

  subst : ∀ {m vt Γ Δ τ} → RenSub {m} vt Γ Δ → Tm Γ τ → Tm Δ τ

  subst σ (abs t)     = abs (subst (lifts σ) t)
  subst σ (app t u)   = app (subst σ t) (subst σ u)
  subst σ (var x)     = vt2tm _ (σ x)

-- Performing substitution, inductive specification

data IndSubst {m vt Γ Δ} (σ : RenSub {m} vt Γ Δ) : ∀ {τ} → Tm Γ τ → Tm Δ τ → Set where

  var  : ∀{a t} (x : Var Γ a)
       → vt2tm _ (σ x) ≡ t
       → IndSubst σ (var x) t

  abs  : ∀{a b} {t : Tm (a ∷ Γ) b} {t'}
       → IndSubst (lifts σ) t t'
       → IndSubst σ (abs t) (abs t')

  app  : ∀{a b} {t : Tm Γ (a →̂ b)} {u t' u'}
       → IndSubst σ t t'
       → IndSubst σ u u'
       → IndSubst σ (app t u) (app t' u')

-- Performing renaming, inductive specification

data IndRen {Γ Δ} (σ : RenSub `Var Γ Δ) : ∀ {τ} → Tm Γ τ → Tm Δ τ → Set where

  var  : ∀{a y} (x : Var Γ a)
       → (σ x) ≡ y
       → IndRen σ (var x) (var y)

  abs  : ∀{a b} {t : Tm (a ∷ Γ) b} {t'}
       → IndRen (lifts σ) t t'
       → IndRen σ (abs t) (abs t')

  app  : ∀{a b} {t : Tm Γ (a →̂ b)} {u t' u'}
       → IndRen σ t t'
       → IndRen σ u u'
       → IndRen σ (app t u) (app t' u')

-- Logical equivalence between inductive and algorithmic substitution

IndS→prop : ∀ {m vt Γ Δ} (σ : RenSub {m} vt Γ Δ) {τ} {t : Tm Γ τ} {t' : Tm Δ τ} → IndSubst σ t t' → subst σ t ≡ t'
IndS→prop σ (var x ≡.refl) = ≡.refl
IndS→prop σ (abs t)     = ≡.cong abs (IndS→prop (lifts σ) t)
IndS→prop σ (app t t₁)  = ≡.cong₂ app (IndS→prop σ t) (IndS→prop σ t₁)

prop→IndS' : ∀ {m vt Γ Δ} (σ : RenSub {m} vt Γ Δ) {τ} (t : Tm Γ τ) → IndSubst σ t (subst σ t)
prop→IndS' σ (var x) = var x ≡.refl
prop→IndS' σ (abs t)     = abs (prop→IndS' (lifts σ) t)
prop→IndS' σ (app t u)   = app (prop→IndS' σ t) (prop→IndS' σ u)

prop→IndS : ∀ {m vt Γ Δ} (σ : RenSub {m} vt Γ Δ) {τ} {t : Tm Γ τ} {t' : Tm Δ τ} → subst σ t ≡ t' → IndSubst σ t t'
prop→IndS _ ≡.refl = prop→IndS' _ _

-- Logical equivalence between inductive and algorithmic renaming

Ind→prop : ∀ {Γ Δ} (σ : RenSub `Var Γ Δ) {τ} {t : Tm Γ τ} {t' : Tm Δ τ} → IndRen σ t t' → subst σ t ≡ t'
Ind→prop σ (var x ≡.refl) = ≡.refl
Ind→prop σ (abs t)     = ≡.cong abs (Ind→prop (lifts σ) t)
Ind→prop σ (app t t₁)  = ≡.cong₂ app (Ind→prop σ t) (Ind→prop σ t₁)

prop→Ind' : ∀ {Γ Δ} (σ : RenSub `Var Γ Δ) {τ} (t : Tm Γ τ) → IndRen σ t (subst σ t)
prop→Ind' σ (var x) = var x ≡.refl
prop→Ind' σ (abs t)     = abs (prop→Ind' (lifts σ) t)
prop→Ind' σ (app t u)   = app (prop→Ind' σ t) (prop→Ind' σ u)

prop→Ind : ∀ {Γ Δ} (σ : RenSub `Var Γ Δ) {τ} {t : Tm Γ τ} {t' : Tm Δ τ} → subst σ t ≡ t' → IndRen σ t t'
prop→Ind _ ≡.refl = prop→Ind' _ _

-- Identity substitution

ids : ∀ {i vt Γ} → RenSub {i} vt Γ Γ
ids {vt = `Var} x = x
ids {vt = `Tm } x = var x

-- substitution composition

_•s_ : ∀ {Γ₀ Γ₁ Γ₂}
         {n}{vt2 : VarTm n}(τ : RenSub vt2 Γ₁ Γ₂)
         {m}{vt1 : VarTm m}(σ : RenSub vt1 Γ₀ Γ₁) → RenSub (vt1 ∙VT vt2) Γ₀ Γ₂
_•s_ τ {vt1 = `Var} σ x = τ (σ x)
_•s_ τ {vt1 = `Tm } σ x = subst τ (σ x)

-- Term substitution

Subst : Cxt → Cxt → Set
Subst Γ Δ = ∀ {a : Ty} → Var Γ a → Tm Δ a

-- Extending a substitution

_∷s_ : ∀ {Γ Δ a} → Tm Γ a → Subst Δ Γ → Subst (a ∷ Δ) Γ
(t ∷s σ) (zero) = t
(t ∷s σ) (suc x) = σ x

-- Substitution for 0th variable

sgs : ∀ {Γ a} → Tm Γ a → Subst (a ∷ Γ) Γ
sgs t = t ∷s ids

-- Substituting for the 0th variable [u/0]t

subst0 : ∀ {Γ a b} → Tm Γ a → Tm (a ∷ Γ) b → Tm Γ b
subst0 u = subst (sgs u)

-- Renamings

Ren : (Γ Δ : Cxt) → Set
Ren = RenSub `Var

_≤_  : (Γ Δ : Cxt) → Set
_≤_ Γ Δ = RenSub `Var Δ Γ

rename : ∀ {Γ Δ : Cxt} {a : Ty} (η : Γ ≤ Δ) (x : Tm Δ a) → Tm Γ a
rename = subst

-- Weakening renaming

weak : ∀{Γ a} → (a ∷ Γ) ≤ Γ
weak = suc

-- Weakening substitution

weaks : ∀{n}{vt : VarTm n}{a Γ Δ} (σ : RenSub vt Γ Δ) → RenSub vt (Γ) (a ∷ Δ)
weaks {vt = `Var} σ x = suc (σ x)
weaks {vt = `Tm} σ x = rename suc (σ x)

-- Properties

_≡s_ : ∀ {Γ Δ} {m n vt1 vt2} → (f : RenSub {m} vt1 Γ Δ)(g : RenSub {n} vt2 Γ Δ) → Set
f ≡s g = (∀ {a} x → vt2tm _ (f {a} x) ≡ vt2tm _ (g x))

mutual
  subst-ext : ∀ {Γ Δ} {m n vt1 vt2} {f : RenSub {m} vt1 Γ Δ}{g : RenSub {n} vt2 Γ Δ} → f ≡s g → ∀ {a} (t : Tm Γ a) → subst f t ≡ subst g t
  subst-ext f≐g (var v) = (f≐g v)
  subst-ext {f = f} {g = g} f≐g (abs t)     = ≡.cong abs (subst-ext (lifts-ext {f = f} {g = g} f≐g) t)
  subst-ext f≐g (app t t₁)  = ≡.cong₂ app (subst-ext f≐g t) (subst-ext f≐g t₁)

  lifts-ext : ∀ {Γ Δ b} {m n vt1 vt2} {f : RenSub {m} vt1 Γ Δ}{g : RenSub {n} vt2 Γ Δ} → f ≡s g → lifts {a = b} f ≡s lifts g
  lifts-ext {vt1 = `Var} {`Var} f≐g (zero) = ≡.refl
  lifts-ext {vt1 = `Var} {`Var} {f} {g} f≐g (suc x) with f x | g x | f≐g x
  lifts-ext {Γ} {Δ} {b} {._} {._} {`Var} {`Var} f≐g (suc x) | z | .z | ≡.refl = ≡.refl
  lifts-ext {vt1 = `Var} {`Tm} f≐g (zero) = ≡.refl
  lifts-ext {vt1 = `Var} {`Tm} f≐g (suc x) rewrite ≡.sym (f≐g x) = ≡.refl
  lifts-ext {vt1 = `Tm} {`Var} f≐g (zero) = ≡.refl
  lifts-ext {vt1 = `Tm} {`Var} f≐g (suc x) rewrite (f≐g x) = ≡.refl
  lifts-ext {vt1 = `Tm} {`Tm} f≐g (zero) = ≡.refl
  lifts-ext {vt1 = `Tm} {`Tm} f≐g (suc x) = ≡.cong (subst suc) (f≐g x)

mutual
  subst-∙ : ∀ {Γ₀ Γ₁ Γ₂}
           {n}{vt2 : VarTm n}(τ : RenSub vt2 Γ₁ Γ₂)
           {m}{vt1 : VarTm m}(σ : RenSub vt1 Γ₀ Γ₁) → ∀ {a} (t : Tm Γ₀ a) → subst (τ •s σ) t ≡ subst τ (subst σ t)
  subst-∙ τ {vt1 = `Var} σ (var x) = ≡.refl
  subst-∙ τ {vt1 = `Tm} σ (var x) = ≡.refl
  subst-∙ τ σ (abs t)     = ≡.cong abs (≡.trans (subst-ext (lifts-∙ τ σ) t) (subst-∙ (lifts τ) (lifts σ) t))
  subst-∙ τ σ (app t t₁)  = ≡.cong₂ app (subst-∙ τ σ t) (subst-∙ τ σ t₁)

  lifts-∙ : ∀ {Γ₀ Γ₁ Γ₂}
         {n}{vt2 : VarTm n}(τ : RenSub vt2 Γ₁ Γ₂)
         {m}{vt1 : VarTm m}(σ : RenSub vt1 Γ₀ Γ₁) → ∀ {a} → lifts {a = a} (τ •s σ) ≡s (lifts τ •s lifts σ)
  lifts-∙ {vt2 = `Var} τ {vt1 = `Var} σ (zero)    = ≡.refl
  lifts-∙ {vt2 = `Tm}  τ {vt1 = `Var} σ (zero)    = ≡.refl
  lifts-∙ {vt2 = `Var} τ {vt1 = `Var} σ (suc x) = ≡.refl
  lifts-∙ {vt2 = `Tm}  τ {vt1 = `Var} σ (suc x) = ≡.refl
  lifts-∙ {vt2 = `Var} τ {vt1 = `Tm}  σ (zero)    = ≡.refl
  lifts-∙ {vt2 = `Tm}  τ {vt1 = `Tm}  σ (zero)    = ≡.refl
  lifts-∙ {vt2 = `Var} τ {vt1 = `Tm}  σ (suc x) = ≡.trans (≡.sym (subst-∙ suc τ (σ x))) (subst-∙ (lifts τ) suc (σ x))
  lifts-∙ {vt2 = `Tm}  τ {vt1 = `Tm}  σ (suc x) = ≡.trans (≡.sym (subst-∙ suc τ (σ x))) (subst-∙ (lifts τ) suc (σ x))

mutual
  subst-id : ∀ {m vt Γ a} → (t : Tm Γ a) → subst (ids {m} {vt}) t ≡ t
  subst-id {vt = `Var} (var v) = ≡.refl
  subst-id {vt = `Tm}  (var v) = ≡.refl
  subst-id {m} {vt} {Γ} (abs t)     = ≡.cong abs (≡.trans (subst-ext {n = m} {vt2 = vt} (lifts-id {m} {vt}) t) (subst-id t))
  subst-id (app t t₁)  = ≡.cong₂ app (subst-id t) (subst-id t₁)

  lifts-id : ∀ {m vt Γ b} → lifts {a = b} (ids {m} {vt} {Γ = Γ}) ≡s ids {m} {vt} {Γ = b ∷ Γ}
  lifts-id {vt = `Var} (zero)    = ≡.refl
  lifts-id {vt = `Var} (suc x) = ≡.refl
  lifts-id {vt = `Tm}  (zero)    = ≡.refl
  lifts-id {vt = `Tm}  (suc x) = ≡.refl

sgs-lifts : ∀ {m vt Γ Δ a} {σ : RenSub {m} vt Γ Δ} {u : Tm Γ a} → (sgs (subst σ u) •s lifts σ) ≡s (σ •s sgs u)
sgs-lifts {vt = `Var} = (λ { (zero) → ≡.refl ; (suc x) → ≡.refl })
sgs-lifts {vt = `Tm} {σ = σ} {u} = (λ { (zero) → ≡.refl ; (suc x) → ≡.sym (≡.trans (≡.sym (subst-id (σ x)))
                                                                               (subst-∙ (sgs (subst σ u)) {vt1 = `Var} suc (σ x))) })
sgs-lifts-term : ∀ {m vt Γ Δ a b} {σ : RenSub {m} vt Γ Δ} {u : Tm Γ a}{t : Tm (a ∷ Γ) b}
                 → subst (sgs (subst σ u)) (subst (lifts σ) t) ≡ subst σ (subst (sgs u) t)
sgs-lifts-term {σ = σ} {u} {t} = (≡.trans (≡.sym (subst-∙ (sgs (subst σ u)) (lifts σ) t))
                                 (≡.trans (subst-ext sgs-lifts t)
                                          (subst-∙ σ (sgs u) t)))

renId : ∀ {Γ a}{t : Tm Γ a} → rename id t ≡ t
renId = subst-id _

contract : ∀ {a Γ} → RenSub `Var (a ∷ a ∷ Γ) (a ∷ Γ)
contract (zero)    = zero
contract (suc x) = x

contract-sgs : ∀ {a Γ} → contract {a} {Γ} ≡s sgs (var zero)
contract-sgs (zero)  = ≡.refl
contract-sgs (suc x) = ≡.refl

sgs-weak₀ : ∀ {Γ a} {u : Tm Γ a} {b} (x : Var Γ b) → sgs u (suc x) ≡ var x
sgs-weak₀ x = ≡.refl

sgs-weak₁ : ∀ {Γ a} {u : Tm Γ a} → (sgs u ∘ suc) ≡s (ids {vt = `Tm})
sgs-weak₁ x = ≡.refl

sgs-weak : ∀ {Γ a} {u : Tm Γ a} → (sgs u •s weak) ≡s (ids {vt = `Tm})
sgs-weak x = ≡.refl

cons-to-sgs :  ∀ {Γ Δ a} (u : Tm Δ a) (σ : Subst Γ Δ)
               → (u ∷s σ) ≡s (sgs u •s lifts σ)
cons-to-sgs u σ (zero) = ≡.refl
cons-to-sgs u σ (suc x) = begin
    σ x                               ≡⟨ ≡.sym (subst-id (σ x)) ⟩
    subst (ids {vt = `Tm}) (σ x)      ≡⟨ subst-ext (λ _ → ≡.refl) (σ x) ⟩
    subst (sgs u •s weak) (σ x)       ≡⟨ subst-∙ (sgs u) weak (σ x) ⟩
    subst (sgs u) (subst suc (σ x))
  ∎
  where open ≡-Reasoning
-- -}

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


text:
-- Andreas, 2014-09-23, later changed by someone else
-- Issue 1194, reported by marco.vax91, 2014-06-13

module _ where

module A where

  data D₁ : Set where
    b : D₁
    c : D₁ → D₁

  infix 19 c

  syntax c x = ! x

module B where

  data D₂ : Set where
    _+_ : D₂ → D₂ → D₂
    c   : A.D₁ → D₂

  infix 10 _+_
  infix 20 c

  syntax c x = ! x

open A
open B

test : D₂
test = ! b + ! b


text:
-- Andreas, 2017-11-01, issue #2831

-- The following pragma should trigger a warning, since the mutual block
-- does not contain anything the pragma could apply to.

{-# NO_POSITIVITY_CHECK #-}
mutual
  postulate
    A : Set

-- EXPECTED WARNING:
-- No positivity checking pragmas can only precede a data/record
-- definition or a mutual block (that contains a data/record
-- definition).

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Agda.Builtin.Unit

module Imports.Issue5583 (_ : ⊤) where

it : ∀ {A : Set} → ⦃ A ⦄ → A
it ⦃ x ⦄ = x

data X : Set where
  instance x : X


text:
module Issue1760d where

-- Skipping a new-style mutual block: Anywhere before the declaration or
-- the definition of a data/record in the block (case: record).
{-# NO_POSITIVITY_CHECK #-}
record U₁ : Set
data D₁   : Set

record U₁ where
  field ap : U₁ → U₁

data D₁ where
  lam : (D₁ → D₁) → D₁

-- Skipping a new-style mutual block: Anywhere before the declaration or
-- the definition of a data/record in the block (case: data).
record U₂ : Set
data D₂   : Set

record U₂ where
  field ap : U₂ → U₂

{-# NO_POSITIVITY_CHECK #-}
data D₂ where
  lam : (D₂ → D₂) → D₂


text:
module IPC.Metatheory.Gentzen-BasicTarski where

open import IPC.Syntax.Gentzen public
open import IPC.Semantics.BasicTarski public

-- Soundness with respect to all models, or evaluation.

eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
eval (var i)      γ = lookup i γ
eval (lam t)      γ = λ a → eval t (γ , a)
eval (app t u)    γ = eval t γ $ eval u γ
eval (pair t u)   γ = eval t γ , eval u γ
eval (fst t)      γ = π₁ (eval t γ)
eval (snd t)      γ = π₂ (eval t γ)
eval unit         γ = ∙
eval (boom t)     γ = elim𝟘 (eval t γ)
eval (inl t)      γ = ι₁ (eval t γ)
eval (inr t)      γ = ι₂ (eval t γ)
eval (case t u v) γ = elim⊎ (eval t γ)
                        (λ a → eval u (γ , a))
                        (λ b → eval v (γ , b))

-- Correctness of evaluation with respect to conversion.

-- FIXME: How to show this?
postulate
  oops₁ : ∀ {{_ : Model}} {A B Γ} {t : Γ , A ⊢ B} {u : Γ ⊢ A}
          → eval ([ top ≔ u ] t) ≡ (λ γ → eval t (γ , eval u γ))
  oops₂ : ∀ {{_ : Model}} {A B Γ} {t : Γ ⊢ A ▻ B}
          → eval t ≡ (λ γ a → eval (mono⊢ (weak⊆ {A = A}) t) (γ , a) a)
  oops₃ : ∀ {{_ : Model}} {A B C Γ} {t : Γ ⊢ A} {u : Γ , A ⊢ C} {v : Γ , B ⊢ C}
          → eval ([ top ≔ t ] u) ≡ (λ γ → eval u (γ , eval t γ))
  oops₄ : ∀ {{_ : Model}} {A B C Γ} {t : Γ ⊢ B} {u : Γ , A ⊢ C} {v : Γ , B ⊢ C}
          → eval ([ top ≔ t ] v) ≡ (λ γ → eval v (γ , eval t γ))
  oops₅ : ∀ {{_ : Model}} {A B Γ} {t : Γ ⊢ A ∨ B}
          → eval t ≡ (λ γ → elim⊎ (eval t γ) (λ a → ι₁ a) (λ b → ι₂ b))

eval✓ : ∀ {{_ : Model}} {A Γ} {t t′ : Γ ⊢ A} → t ⋙ t′ → eval t ≡ eval t′
eval✓ refl⋙                             = refl
eval✓ (trans⋙ p q)                      = trans (eval✓ p) (eval✓ q)
eval✓ (sym⋙ p)                          = sym (eval✓ p)
eval✓ (conglam⋙ {A} {B} p)              = cong (⟦λ⟧ {A} {B}) (eval✓ p)
eval✓ (congapp⋙ {A} {B} p q)            = cong² (_⟦$⟧_ {A} {B}) (eval✓ p) (eval✓ q)
eval✓ (congpair⋙ {A} {B} p q)           = cong² (_⟦,⟧_ {A} {B}) (eval✓ p) (eval✓ q)
eval✓ (congfst⋙ {A} {B} p)              = cong (⟦π₁⟧ {A} {B}) (eval✓ p)
eval✓ (congsnd⋙ {A} {B} p)              = cong (⟦π₂⟧ {A} {B}) (eval✓ p)
eval✓ (congboom⋙ {C} p)                 = cong (⟦elim𝟘⟧ {C}) (eval✓ p)
eval✓ (conginl⋙ {A} {B} p)              = cong (⟦ι₁⟧ {A} {B}) (eval✓ p)
eval✓ (conginr⋙ {A} {B} p)              = cong (⟦ι₂⟧ {A} {B}) (eval✓ p)
eval✓ (congcase⋙ {A} {B} {C} p q r)     = cong³ (⟦elim⊎⟧ {A} {B} {C}) (eval✓ p) (eval✓ q) (eval✓ r)
eval✓ (beta▻⋙ {A} {B} {t} {u})          = sym (oops₁ {A} {B} {_} {t} {u})
eval✓ (eta▻⋙ {A} {B} {t})               = oops₂ {A} {B} {_} {t}
eval✓ beta∧₁⋙                           = refl
eval✓ beta∧₂⋙                           = refl
eval✓ eta∧⋙                             = refl
eval✓ eta⊤⋙                            = refl
eval✓ (beta∨₁⋙ {A} {B} {C} {t} {u} {v}) = sym (oops₃ {A} {B} {C} {_} {t} {u} {v})
eval✓ (beta∨₂⋙ {A} {B} {C} {t} {u} {v}) = sym (oops₄ {A} {B} {C} {_} {t} {u} {v})
eval✓ (eta∨⋙ {A} {B} {t})               = oops₅ {A} {B} {_} {t}

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Correctness proofs for container combinators
------------------------------------------------------------------------

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

module Data.Container.Combinator.Properties where

open import Axiom.Extensionality.Propositional using (Extensionality)
open import Data.Container.Core
open import Data.Container.Combinator
open import Data.Container.Relation.Unary.Any
open import Data.Empty using (⊥-elim)
open import Data.Product as Prod using (∃; _,_; proj₁; proj₂; <_,_>; uncurry; curry)
open import Data.Sum as S using (inj₁; inj₂; [_,_]′; [_,_])
open import Function as F using (_∘′_)
open import Function.Inverse as Inv using (_↔_; inverse; module Inverse)
open import Level using (_⊔_; lower)
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)

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

module Identity where

  correct : ∀ {s p x} {X : Set x} → ⟦ id {s} {p} ⟧ X ↔ F.id X
  correct {X = X} = inverse to from (λ _ → P.refl) (λ _ → P.refl)
    where
    to : ⟦ id ⟧ X → F.id X
    to xs = proj₂ xs _

    from : F.id X → ⟦ id ⟧ X
    from x = (_ , λ _ → x)

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

  correct : ∀ {x p y} (X : Set x) {Y : Set y} → ⟦ const {x} {p ⊔ y} X ⟧ Y ↔ F.const X Y
  correct {x} {y} X {Y} = inverse proj₁ from from∘to λ _ → P.refl

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

    from∘to : (x : ⟦ const X ⟧ Y) → from (proj₁ x) ≡ x
    from∘to xs = P.cong (proj₁ xs ,_) (ext (λ x → ⊥-elim (lower x)))

module Composition {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) where

  correct : ∀ {x} {X : Set x} → ⟦ C₁ ∘ C₂ ⟧ X ↔ (⟦ C₁ ⟧ F.∘ ⟦ C₂ ⟧) X
  correct {X = X} = inverse to from (λ _ → P.refl) (λ _ → P.refl)
    where
    to : ⟦ C₁ ∘ C₂ ⟧ X → ⟦ C₁ ⟧ (⟦ C₂ ⟧ X)
    to ((s , f) , g) = (s , < f , curry (g ∘′ any) >)

    from : ⟦ C₁ ⟧ (⟦ C₂ ⟧ X) → ⟦ C₁ ∘ C₂ ⟧ X
    from (s , f) = ((s , proj₁ F.∘ f) , uncurry (proj₂ F.∘ f) ∘′ ◇.proof)

module Product (ext : ∀ {ℓ ℓ′} → Extensionality ℓ ℓ′)
       {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) where

  correct : ∀ {x} {X : Set x} →  ⟦ C₁ × C₂ ⟧ X ↔ (⟦ C₁ ⟧ X Prod.× ⟦ C₂ ⟧ X)
  correct {X = X} = inverse to from from∘to (λ _ → P.refl)
    where
    to : ⟦ C₁ × C₂ ⟧ X → ⟦ C₁ ⟧ X Prod.× ⟦ C₂ ⟧ X
    to ((s₁ , s₂) , f) = ((s₁ , f F.∘ inj₁) , (s₂ , f F.∘ inj₂))

    from : ⟦ C₁ ⟧ X Prod.× ⟦ C₂ ⟧ X → ⟦ C₁ × C₂ ⟧ X
    from ((s₁ , f₁) , (s₂ , f₂)) = ((s₁ , s₂) , [ f₁ , f₂ ]′)

    from∘to : from F.∘ to ≗ F.id
    from∘to (s , f) =
      P.cong (s ,_) (ext [ (λ _ → P.refl) , (λ _ → P.refl) ])

module IndexedProduct {i s p} {I : Set i} (Cᵢ : I → Container s p) where

  correct : ∀ {x} {X : Set x} → ⟦ Π I Cᵢ ⟧ X ↔ (∀ i → ⟦ Cᵢ i ⟧ X)
  correct {X = X} = inverse to from (λ _ → P.refl) (λ _ → P.refl)
    where
    to : ⟦ Π I Cᵢ ⟧ X → ∀ i → ⟦ Cᵢ i ⟧ X
    to (s , f) = λ i → (s i , λ p → f (i , p))

    from : (∀ i → ⟦ Cᵢ i ⟧ X) → ⟦ Π I Cᵢ ⟧ X
    from f = (proj₁ F.∘ f , uncurry (proj₂ F.∘ f))

module Sum {s₁ s₂ p} (C₁ : Container s₁ p) (C₂ : Container s₂ p) where

  correct : ∀ {x} {X : Set x} → ⟦ C₁ ⊎ C₂ ⟧ X ↔ (⟦ C₁ ⟧ X S.⊎ ⟦ C₂ ⟧ X)
  correct {X = X} = inverse to from from∘to to∘from
    where
    to : ⟦ C₁ ⊎ C₂ ⟧ X → ⟦ C₁ ⟧ X S.⊎ ⟦ C₂ ⟧ X
    to (inj₁ s₁ , f) = inj₁ (s₁ , f)
    to (inj₂ s₂ , f) = inj₂ (s₂ , f)

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

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

    to∘from : to F.∘ from ≗ F.id
    to∘from = [ (λ _ → P.refl) , (λ _ → P.refl) ]

module IndexedSum {i s p} {I : Set i} (C : I → Container s p) where

  correct : ∀ {x} {X : Set x} → ⟦ Σ I C ⟧ X ↔ (∃ λ i → ⟦ C i ⟧ X)
  correct {X = X} = inverse to from (λ _ → P.refl) (λ _ → P.refl)
    where
    to : ⟦ Σ I C ⟧ X → ∃ λ i → ⟦ C i ⟧ X
    to ((i , s) , f) = (i , (s , f))

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

module ConstantExponentiation {i s p} {I : Set i} (C : Container s p) where

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


text:
-- Occurs there are several ways to parse a left-hand side.
module AmbiguousParseForLHS where

data X : Set where
  if_then_else_ : X -> X -> X -> X
  if_then_      : X -> X -> X
  x             : X

bad : X -> X
bad (if x then if x then x else x) = x
bad _                              = if x then x

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import lib.Basics
open import lib.types.Truncation

module lib.Function2 where

is-surj : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) → Type (lmax i j)
is-surj {A = A} f = ∀ b → Trunc -1 (hfiber f b)

module _ {i j k} {A : Type i} {B : Type j} {C : Type k}
  {f : A → B} {g : B → C} where
  abstract
    ∘-is-surj : is-surj g → is-surj f → is-surj (g ∘ f)
    ∘-is-surj g-is-surj f-is-surj c =
      Trunc-rec Trunc-level
        (λ{(b , gb=c) →
          Trunc-rec Trunc-level
          (λ{(a , fa=b) → [ a , ap g fa=b ∙ gb=c ]})
          (f-is-surj b)})
        (g-is-surj c)

module _ {i j} {A : Type i} {B : Type j} {f : A → B} where
  abstract
    equiv-is-surj : is-equiv f → is-surj f
    equiv-is-surj f-is-equiv b = [ g b , f-g b ]
      where open is-equiv f-is-equiv

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
-- Not using any Floats so shouldn't need ieee754 installed.
-- .flags file contains
--    -c --ghc-flag="-hide-package ieee754"

module _ where

open import Agda.Builtin.IO
open import Agda.Builtin.Unit

postulate
  return : {A : Set} → A → IO A

{-# COMPILE GHC return = \ _ -> return #-}

main : IO ⊤
main = return _


text:
module Impure.STLCRef.Eval where

open import Prelude

open import Data.Product
open import Data.List
open import Data.List.Reverse
open import Data.Nat
open import Data.Fin hiding (_<_)
open import Extensions.List as L

open import Impure.STLCRef.Syntax
open import Impure.STLCRef.Welltyped

_!!_ : ∀ {n i} → (μ : Store n) → i < length μ → ∃ (Val {n})
_!!_ {i = i} [] ()
_!!_ {i = zero} (x ∷ μ) (s≤s p) = x
_!!_ {i = suc i} (x ∷ μ) (s≤s p) = μ !! p

Config : (n : ℕ) → Set
Config n = Exp n × Store n

infixl 1 _≻_
data _≻_ : ∀ {n} → Config n → Config n → Set where

  ---------------------------------------
  -- Reduction rules
  ---------------------------------------

  -- β
  AppAbs : ∀ {n} {A x} {e : Exp (suc n)} {μ : Store n} →
           ---------------------------------
           (ƛ A e) · x , μ ≻ e / (sub x) , μ

  -- new
  RefVal : ∀ {n e} {μ : Store n} →
           (v : Val e) →
           --------------------------------------------
           (ref e , μ) ≻ (loc (length μ) , μ ∷ʳ (, v))

  -- load
  DerefLoc : ∀ {n i} {μ : Store n} →
             (p : i < length μ) →
             ---------------------------------------------------
             (! (loc i) , μ) ≻ (proj₁ (μ !! p) , μ)

  -- store
  Assign : ∀ {i n e} {μ : Store n} →
           (p : i < length μ) →
           (v : Val e) →
           ----------------------------------------------
           loc i ≔ e , μ ≻ unit , (μ L.[ fromℕ≤ p ]≔ (, v))

  ---------------------------------------
  -- contextual closure
  ---------------------------------------

  Ref : ∀ {n e'} {e : Exp n} {μ μ'} →
        (e , μ) ≻ (e' , μ') →
        ---------------------------------------
        (ref e) , μ ≻ (ref e') , μ'

  Appₗ : ∀ {n f' e} {f : Exp n} {μ μ'} →
         (f , μ) ≻ (f' , μ') →
         ---------------------------------------
         (f · e) , μ ≻ (f' · e) , μ'

  Appᵣ : ∀ {n e' e} {f : Exp n} {μ μ'} →
         (e , μ) ≻ (e' , μ') →
         ---------------------------------------
         (f · e) , μ ≻ (f · e') , μ'

  Deref : ∀ {n} {e : Exp n} {e'} {μ μ'} →
          e , μ ≻ e' , μ' →
          ---------------------------------------
          ! e , μ ≻ ! e' , μ'

  Assign₁ : ∀ {n} {e₁ : Exp n} {e₁' e₂} {μ μ'} →
            e₁ , μ ≻ e₁' , μ' →
            ---------------------------------------
            e₁ ≔ e₂ , μ ≻ e₁' ≔ e₂ , μ'

  Assign₂ : ∀ {n} {e₁ : Exp n} {e₂' e₂} {μ μ'} →
            e₂ , μ ≻ e₂' , μ' →
            ---------------------------------------
            e₁ ≔ e₂ , μ ≻ e₁ ≔ e₂' , μ'

------------------------------------------------
-- Reflexive-transitive closure of step relation
------------------------------------------------

open import Data.Star

infixl 1 _≻*_
_≻*_ : ∀ {n} → Config n → Config n → Set
c ≻* c' = Star _≻_ c c'


text:
module STLC.Kovacs.NormalForm where

open import STLC.Kovacs.Embedding public
open import Category

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

mutual
  -- (Nfₑ)
  renⁿᶠ : ∀ {Γ Γ′ A} → Γ′ ⊇ Γ → Γ ⊢ⁿᶠ A → Γ′ ⊢ⁿᶠ A
  renⁿᶠ η (ƛ M)  = ƛ (renⁿᶠ (liftₑ η) M)
  renⁿᶠ η (ne M) = ne (renⁿᵉ η M)

  -- (Neₑ)
  renⁿᵉ : ∀ {Γ Γ′ A} → Γ′ ⊇ Γ → Γ ⊢ⁿᵉ A → Γ′ ⊢ⁿᵉ A
  renⁿᵉ η (𝓋 i)   = 𝓋 (getₑ η i)
  renⁿᵉ η (M ∙ N) = renⁿᵉ η M ∙ renⁿᶠ η N

mutual
  -- (Nf-idₑ)
  idrenⁿᶠ : ∀ {Γ A} → (M : Γ ⊢ⁿᶠ A)
                    → renⁿᶠ idₑ M ≡ M
  idrenⁿᶠ (ƛ M)  = ƛ & idrenⁿᶠ M
  idrenⁿᶠ (ne M) = ne & idrenⁿᵉ M

  -- (Ne-idₑ)
  idrenⁿᵉ : ∀ {Γ A} → (M : Γ ⊢ⁿᵉ A)
                    → renⁿᵉ idₑ M ≡ M
  idrenⁿᵉ (𝓋 i)   = 𝓋 & idgetₑ i
  idrenⁿᵉ (M ∙ N) = _∙_ & idrenⁿᵉ M
                        ⊗ idrenⁿᶠ N

mutual
  -- (Nf-∘ₑ)
  renⁿᶠ○ : ∀ {Γ Γ′ Γ″ A} → (η₁ : Γ″ ⊇ Γ′) (η₂ : Γ′ ⊇ Γ) (M : Γ ⊢ⁿᶠ A)
                         → renⁿᶠ (η₂ ○ η₁) M ≡ (renⁿᶠ η₁ ∘ renⁿᶠ η₂) M
  renⁿᶠ○ η₁ η₂ (ƛ M)  = ƛ & renⁿᶠ○ (liftₑ η₁) (liftₑ η₂) M
  renⁿᶠ○ η₁ η₂ (ne M) = ne & renⁿᵉ○ η₁ η₂ M

  -- (Ne-∘ₑ)
  renⁿᵉ○ : ∀ {Γ Γ′ Γ″ A} → (η₁ : Γ″ ⊇ Γ′) (η₂ : Γ′ ⊇ Γ) (M : Γ ⊢ⁿᵉ A)
                         → renⁿᵉ (η₂ ○ η₁) M ≡ (renⁿᵉ η₁ ∘ renⁿᵉ η₂) M
  renⁿᵉ○ η₁ η₂ (𝓋 i)   = 𝓋 & get○ η₁ η₂ i
  renⁿᵉ○ η₁ η₂ (M ∙ N) = _∙_ & renⁿᵉ○ η₁ η₂ M
                             ⊗ renⁿᶠ○ η₁ η₂ N

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

mutual
  -- (⌜_⌝Nf)
  embⁿᶠ : ∀ {Γ A} → Γ ⊢ⁿᶠ A → Γ ⊢ A
  embⁿᶠ (ƛ M)  = ƛ (embⁿᶠ M)
  embⁿᶠ (ne M) = embⁿᵉ M

  -- (⌜_⌝Ne)
  embⁿᵉ : ∀ {Γ A} → Γ ⊢ⁿᵉ A → Γ ⊢ A
  embⁿᵉ (𝓋 i)   = 𝓋 i
  embⁿᵉ (M ∙ N) = embⁿᵉ M ∙ embⁿᶠ N

mutual
  -- (⌜⌝Nf-nat)
  natembⁿᶠ : ∀ {A Γ Γ′} → (η : Γ′ ⊇ Γ) (M : Γ ⊢ⁿᶠ A)
                        → (embⁿᶠ ∘ renⁿᶠ η) M ≡ (ren η ∘ embⁿᶠ) M
  natembⁿᶠ η (ƛ M)  = ƛ & natembⁿᶠ (liftₑ η) M
  natembⁿᶠ η (ne M) = natembⁿᵉ η M

  -- (⌜⌝Ne-nat)
  natembⁿᵉ : ∀ {A Γ Γ′} → (η : Γ′ ⊇ Γ) (M : Γ ⊢ⁿᵉ A)
                        → (embⁿᵉ ∘ renⁿᵉ η) M ≡ (ren η ∘ embⁿᵉ) M
  natembⁿᵉ η (𝓋 i)   = refl
  natembⁿᵉ η (M ∙ N) = _∙_ & natembⁿᵉ η M
                           ⊗ natembⁿᶠ η N

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

renⁿᶠPsh : 𝒯 → Presheaf₀ 𝗢𝗣𝗘
renⁿᶠPsh A =
  record
    { Fₓ  = _⊢ⁿᶠ A
    ; F   = renⁿᶠ
    ; idF = fext! idrenⁿᶠ
    ; F⋄  = λ η₁ η₂ → fext! (renⁿᶠ○ η₂ η₁)
    }

renⁿᵉPsh : 𝒯 → Presheaf₀ 𝗢𝗣𝗘
renⁿᵉPsh A =
  record
    { Fₓ  = _⊢ⁿᵉ A
    ; F   = renⁿᵉ
    ; idF = fext! idrenⁿᵉ
    ; F⋄  = λ η₁ η₂ → fext! (renⁿᵉ○ η₂ η₁)
    }

embⁿᶠNT : ∀ {A} → NaturalTransformation (renⁿᶠPsh A) (renPsh A)
embⁿᶠNT =
  record
    { N    = embⁿᶠ
    ; natN = λ η → fext! (λ M → natembⁿᶠ η M)
    }

embⁿᵉNT : ∀ {A} → NaturalTransformation (renⁿᵉPsh A) (renPsh A)
embⁿᵉNT =
  record
    { N    = embⁿᵉ
    ; natN = λ η → fext! (λ M → natembⁿᵉ η M)
    }

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
------------------------------------------------------------------------------
-- Properties related with the group commutator
------------------------------------------------------------------------------

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

module GroupTheory.Commutator.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import GroupTheory.Base
open import GroupTheory.Commutator
open import GroupTheory.PropertiesI

------------------------------------------------------------------------------
-- Kurosh (1960), p. 99.
commutatorInverse : ∀ a b → [ a , b ] · [ b , a ] ≡ ε
commutatorInverse a b =
  a ⁻¹ · b ⁻¹ · a · b · (b ⁻¹ · a ⁻¹ · b · a)
    ≡⟨ assoc (a ⁻¹ · b ⁻¹ · a) b (b ⁻¹ · a ⁻¹ · b · a) ⟩
  a ⁻¹ · b ⁻¹ · a · (b · (b ⁻¹ · a ⁻¹ · b · a))
    ≡⟨ ·-rightCong (·-rightCong (assoc (b ⁻¹ · a ⁻¹) b a)) ⟩
  a ⁻¹ · b ⁻¹ · a · (b · (b ⁻¹ · a ⁻¹ · (b · a)))
    ≡⟨ ·-rightCong (·-rightCong (assoc (b ⁻¹) (a ⁻¹) (b · a))) ⟩
  a ⁻¹ · b ⁻¹ · a · (b · (b ⁻¹ · (a ⁻¹ · (b · a))))
    ≡⟨ ·-rightCong (sym (assoc b (b ⁻¹) (a ⁻¹ · (b · a)))) ⟩
  a ⁻¹ · b ⁻¹ · a · (b · b ⁻¹ · (a ⁻¹ · (b · a)))
    ≡⟨ ·-rightCong (·-leftCong (rightInverse b)) ⟩
  a ⁻¹ · b ⁻¹ · a · (ε · (a ⁻¹ · (b · a)))
    ≡⟨ ·-rightCong (leftIdentity (a ⁻¹ · (b · a))) ⟩
  a ⁻¹ · b ⁻¹ · a · (a ⁻¹ · (b · a))
    ≡⟨ assoc (a ⁻¹ · b ⁻¹) a (a ⁻¹ · (b · a)) ⟩
  a ⁻¹ · b ⁻¹ · (a · (a ⁻¹ · (b · a)))
    ≡⟨ ·-rightCong (sym (assoc a (a ⁻¹) (b · a))) ⟩
  a ⁻¹ · b ⁻¹ · (a · a ⁻¹ · (b · a))
    ≡⟨ ·-rightCong (·-leftCong (rightInverse a)) ⟩
  a ⁻¹ · b ⁻¹ · (ε · (b · a))
    ≡⟨ ·-rightCong (leftIdentity (b · a)) ⟩
  a ⁻¹ · b ⁻¹ · (b · a)
    ≡⟨ assoc (a ⁻¹) (b ⁻¹) (b · a) ⟩
  a ⁻¹ · (b ⁻¹ · (b · a))
     ≡⟨ ·-rightCong (sym (assoc (b ⁻¹) b a)) ⟩
  a ⁻¹ · ((b ⁻¹ · b) · a)
     ≡⟨ ·-rightCong (·-leftCong (leftInverse b)) ⟩
  a ⁻¹ · (ε · a)
     ≡⟨ ·-rightCong (leftIdentity a) ⟩
  a ⁻¹ · a
     ≡⟨ leftInverse a ⟩
  ε ∎

------------------------------------------------------------------------------
-- References
--
-- Kurosh, A. G. (1960). The Theory of Groups. 2nd
-- ed. Vol. 1. Translated and edited by K. A. Hirsch. Chelsea
-- Publising Company.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc