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

open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Unit
open import Data.Empty
open import Function

-- some HoTT-inspired combinators

_&_ = cong
_⁻¹ = sym
_◾_ = trans

coe : {A B : Set} → A ≡ B → A → B
coe refl a = a

_⊗_ : ∀ {A B : Set}{f g : A → B}{a a'} → f ≡ g → a ≡ a' → f a ≡ g a'
refl ⊗ refl = refl

infix 6 _⁻¹
infixr 4 _◾_
infixl 9 _&_
infixl 8 _⊗_

-- Syntax
--------------------------------------------------------------------------------

infixr 4 _⇒_
infixr 4 _,_

data Ty : Set where
  ι   : Ty
  _⇒_ : Ty → Ty → Ty

data Con : Set where
  ∙   : Con
  _,_ : Con → Ty → Con

data _∈_ (A : Ty) : Con → Set where
  vz : ∀ {Γ} → A ∈ (Γ , A)
  vs : ∀ {B Γ} → A ∈ Γ → A ∈ (Γ , B)

data Tm Γ : Ty → Set where
  var : ∀ {A} → A ∈ Γ → Tm Γ A
  lam : ∀ {A B} → Tm (Γ , A) B → Tm Γ (A ⇒ B)
  app : ∀ {A B} → Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B

-- Embedding
--------------------------------------------------------------------------------

-- Order-preserving embedding
data OPE : Con → Con → Set where
  ∙    : OPE ∙ ∙
  drop : ∀ {A Γ Δ} → OPE Γ Δ → OPE (Γ , A) Δ
  keep : ∀ {A Γ Δ} → OPE Γ Δ → OPE (Γ , A) (Δ , A)

-- OPE is a category
idₑ : ∀ {Γ} → OPE Γ Γ
idₑ {∙}     = ∙
idₑ {Γ , A} = keep (idₑ {Γ})

wk : ∀ {A Γ} → OPE (Γ , A) Γ
wk = drop idₑ

_∘ₑ_ : ∀ {Γ Δ Σ} → OPE Δ Σ → OPE Γ Δ → OPE Γ Σ
σ      ∘ₑ ∙      = σ
σ      ∘ₑ drop δ = drop (σ ∘ₑ δ)
drop σ ∘ₑ keep δ = drop (σ ∘ₑ δ)
keep σ ∘ₑ keep δ = keep (σ ∘ₑ δ)

idlₑ : ∀ {Γ Δ}(σ : OPE Γ Δ) → idₑ ∘ₑ σ ≡ σ
idlₑ ∙        = refl
idlₑ (drop σ) = drop & idlₑ σ
idlₑ (keep σ) = keep & idlₑ σ

idrₑ : ∀ {Γ Δ}(σ : OPE Γ Δ) → σ ∘ₑ idₑ ≡ σ
idrₑ ∙        = refl
idrₑ (drop σ) = drop & idrₑ σ
idrₑ (keep σ) = keep & idrₑ σ

assₑ :
  ∀ {Γ Δ Σ Ξ}(σ : OPE Σ Ξ)(δ : OPE Δ Σ)(ν : OPE Γ Δ)
  → (σ ∘ₑ δ) ∘ₑ ν ≡ σ ∘ₑ (δ ∘ₑ ν)
assₑ σ        δ        ∙        = refl
assₑ σ        δ        (drop ν) = drop & assₑ σ δ ν
assₑ σ        (drop δ) (keep ν) = drop & assₑ σ δ ν
assₑ (drop σ) (keep δ) (keep ν) = drop & assₑ σ δ ν
assₑ (keep σ) (keep δ) (keep ν) = keep & assₑ σ δ ν

∈ₑ : ∀ {A Γ Δ} → OPE Γ Δ → A ∈ Δ → A ∈ Γ
∈ₑ ∙        v      = v
∈ₑ (drop σ) v      = vs (∈ₑ σ v)
∈ₑ (keep σ) vz     = vz
∈ₑ (keep σ) (vs v) = vs (∈ₑ σ v)

∈-idₑ : ∀ {A Γ}(v : A ∈ Γ) → ∈ₑ idₑ v ≡ v
∈-idₑ vz     = refl
∈-idₑ (vs v) = vs & ∈-idₑ v

∈-∘ₑ : ∀ {A Γ Δ Σ}(σ : OPE Δ Σ)(δ : OPE Γ Δ)(v : A ∈ Σ) → ∈ₑ (σ ∘ₑ δ) v ≡ ∈ₑ δ (∈ₑ σ v)
∈-∘ₑ ∙        ∙        v      = refl
∈-∘ₑ σ        (drop δ) v      = vs & ∈-∘ₑ σ δ v
∈-∘ₑ (drop σ) (keep δ) v      = vs & ∈-∘ₑ σ δ v
∈-∘ₑ (keep σ) (keep δ) vz     = refl
∈-∘ₑ (keep σ) (keep δ) (vs v) = vs & ∈-∘ₑ σ δ v

Tmₑ : ∀ {A Γ Δ} → OPE Γ Δ → Tm Δ A → Tm Γ A
Tmₑ σ (var v)   = var (∈ₑ σ v)
Tmₑ σ (lam t)   = lam (Tmₑ (keep σ) t)
Tmₑ σ (app f a) = app (Tmₑ σ f) (Tmₑ σ a)

Tm-idₑ : ∀ {A Γ}(t : Tm Γ A) → Tmₑ idₑ t ≡ t
Tm-idₑ (var v)   = var & ∈-idₑ v
Tm-idₑ (lam t)   = lam & Tm-idₑ t
Tm-idₑ (app f a) = app & Tm-idₑ f ⊗ Tm-idₑ a

Tm-∘ₑ : ∀ {A Γ Δ Σ}(σ : OPE Δ Σ)(δ : OPE Γ Δ)(t : Tm Σ A) → Tmₑ (σ ∘ₑ δ) t ≡ Tmₑ δ (Tmₑ σ t)
Tm-∘ₑ σ δ (var v)   = var & ∈-∘ₑ σ δ v
Tm-∘ₑ σ δ (lam t)   = lam & Tm-∘ₑ (keep σ) (keep δ) t
Tm-∘ₑ σ δ (app f a) = app & Tm-∘ₑ σ δ f ⊗ Tm-∘ₑ σ δ a

-- Theory of substitution & embedding
--------------------------------------------------------------------------------

infixr 6 _ₑ∘ₛ_ _ₛ∘ₑ_ _∘ₛ_

data Sub (Γ : Con) : Con → Set where
  ∙   : Sub Γ ∙
  _,_ : ∀ {A : Ty}{Δ : Con} → Sub Γ Δ → Tm Γ A → Sub Γ (Δ , A)

_ₛ∘ₑ_ : ∀ {Γ Δ Σ} → Sub Δ Σ → OPE Γ Δ → Sub Γ Σ
∙       ₛ∘ₑ δ = ∙
(σ , t) ₛ∘ₑ δ = σ ₛ∘ₑ δ , Tmₑ δ t

_ₑ∘ₛ_ : ∀ {Γ Δ Σ} → OPE Δ Σ → Sub Γ Δ → Sub Γ Σ
∙      ₑ∘ₛ δ       = δ
drop σ ₑ∘ₛ (δ , t) = σ ₑ∘ₛ δ
keep σ ₑ∘ₛ (δ , t) = σ ₑ∘ₛ δ , t

dropₛ : ∀ {A Γ Δ} → Sub Γ Δ → Sub (Γ , A) Δ
dropₛ σ = σ ₛ∘ₑ wk

keepₛ : ∀ {A Γ Δ} → Sub Γ Δ → Sub (Γ , A) (Δ , A)
keepₛ σ = dropₛ σ , var vz

⌜_⌝ᵒᵖᵉ : ∀ {Γ Δ} → OPE Γ Δ → Sub Γ Δ
⌜ ∙      ⌝ᵒᵖᵉ = ∙
⌜ drop σ ⌝ᵒᵖᵉ = dropₛ ⌜ σ ⌝ᵒᵖᵉ
⌜ keep σ ⌝ᵒᵖᵉ = keepₛ ⌜ σ ⌝ᵒᵖᵉ

∈ₛ : ∀ {A Γ Δ} → Sub Γ Δ → A ∈ Δ → Tm Γ A
∈ₛ (σ , t) vz     = t
∈ₛ (σ  , t)(vs v) = ∈ₛ σ v

Tmₛ : ∀ {A Γ Δ} → Sub Γ Δ → Tm Δ A → Tm Γ A
Tmₛ σ (var v)   = ∈ₛ σ v
Tmₛ σ (lam t)   = lam (Tmₛ (keepₛ σ) t)
Tmₛ σ (app f a) = app (Tmₛ σ f) (Tmₛ σ a)

idₛ : ∀ {Γ} → Sub Γ Γ
idₛ {∙}     = ∙
idₛ {Γ , A} = (idₛ {Γ} ₛ∘ₑ drop idₑ) , var vz

_∘ₛ_ : ∀ {Γ Δ Σ} → Sub Δ Σ → Sub Γ Δ → Sub Γ Σ
∙       ∘ₛ δ = ∙
(σ , t) ∘ₛ δ = σ ∘ₛ δ , Tmₛ δ t

assₛₑₑ :
  ∀ {Γ Δ Σ Ξ}(σ : Sub Σ Ξ)(δ : OPE Δ Σ)(ν : OPE Γ Δ)
  → (σ ₛ∘ₑ δ) ₛ∘ₑ ν ≡ σ ₛ∘ₑ (δ ∘ₑ ν)
assₛₑₑ ∙       δ ν = refl
assₛₑₑ (σ , t) δ ν = _,_ & assₛₑₑ σ δ ν ⊗ (Tm-∘ₑ δ ν t ⁻¹)

assₑₛₑ :
  ∀ {Γ Δ Σ Ξ}(σ : OPE Σ Ξ)(δ : Sub Δ Σ)(ν : OPE Γ Δ)
  → (σ ₑ∘ₛ δ) ₛ∘ₑ ν ≡ σ ₑ∘ₛ (δ ₛ∘ₑ ν)
assₑₛₑ ∙        δ       ν = refl
assₑₛₑ (drop σ) (δ , t) ν = assₑₛₑ σ δ ν
assₑₛₑ (keep σ) (δ , t) ν = (_, Tmₑ ν t) & assₑₛₑ σ δ ν

idlₑₛ : ∀ {Γ Δ}(σ : Sub Γ Δ) → idₑ ₑ∘ₛ σ ≡ σ
idlₑₛ ∙       = refl
idlₑₛ (σ , t) = (_, t) & idlₑₛ σ

idlₛₑ : ∀ {Γ Δ}(σ : OPE Γ Δ) → idₛ ₛ∘ₑ σ ≡ ⌜ σ ⌝ᵒᵖᵉ
idlₛₑ ∙        = refl
idlₛₑ (drop σ) =
      ((idₛ ₛ∘ₑ_) ∘ drop) & idrₑ σ ⁻¹
    ◾ assₛₑₑ idₛ σ wk ⁻¹
    ◾ dropₛ & idlₛₑ σ
idlₛₑ (keep σ) =
  (_, var vz) &
      (assₛₑₑ idₛ wk (keep σ)
    ◾ ((idₛ ₛ∘ₑ_) ∘ drop) & (idlₑ σ ◾ idrₑ σ ⁻¹)
    ◾ assₛₑₑ idₛ σ wk ⁻¹
    ◾ (_ₛ∘ₑ wk) & idlₛₑ σ )

idrₑₛ : ∀ {Γ Δ}(σ : OPE Γ Δ) → σ ₑ∘ₛ idₛ ≡ ⌜ σ ⌝ᵒᵖᵉ
idrₑₛ ∙        = refl
idrₑₛ (drop σ) = assₑₛₑ σ idₛ wk ⁻¹ ◾ dropₛ & idrₑₛ σ
idrₑₛ (keep σ) = (_, var vz) & (assₑₛₑ σ idₛ wk ⁻¹ ◾ (_ₛ∘ₑ wk) & idrₑₛ σ)

∈-ₑ∘ₛ : ∀ {A Γ Δ Σ}(σ : OPE Δ Σ)(δ : Sub Γ Δ)(v : A ∈ Σ) → ∈ₛ (σ ₑ∘ₛ δ) v ≡ ∈ₛ δ (∈ₑ σ v)
∈-ₑ∘ₛ ∙        δ       v      = refl
∈-ₑ∘ₛ (drop σ) (δ , t) v      = ∈-ₑ∘ₛ σ δ v
∈-ₑ∘ₛ (keep σ) (δ , t) vz     = refl
∈-ₑ∘ₛ (keep σ) (δ , t) (vs v) = ∈-ₑ∘ₛ σ δ v

Tm-ₑ∘ₛ : ∀ {A Γ Δ Σ}(σ : OPE Δ Σ)(δ : Sub Γ Δ)(t : Tm Σ A) → Tmₛ (σ ₑ∘ₛ δ) t ≡ Tmₛ δ (Tmₑ σ t)
Tm-ₑ∘ₛ σ δ (var v) = ∈-ₑ∘ₛ σ δ v
Tm-ₑ∘ₛ σ δ (lam t) =
  lam & ((λ x → Tmₛ (x , var vz) t) & assₑₛₑ σ δ wk ◾ Tm-ₑ∘ₛ (keep σ) (keepₛ δ) t)
Tm-ₑ∘ₛ σ δ (app f a) = app & Tm-ₑ∘ₛ σ δ f ⊗ Tm-ₑ∘ₛ σ δ a

∈-ₛ∘ₑ : ∀ {A Γ Δ Σ}(σ : Sub Δ Σ)(δ : OPE Γ Δ)(v : A ∈ Σ) → ∈ₛ (σ ₛ∘ₑ δ) v ≡ Tmₑ δ (∈ₛ σ v)
∈-ₛ∘ₑ (σ , _) δ vz     = refl
∈-ₛ∘ₑ (σ , _) δ (vs v) = ∈-ₛ∘ₑ σ δ v

Tm-ₛ∘ₑ : ∀ {A Γ Δ Σ}(σ : Sub Δ Σ)(δ : OPE Γ Δ)(t : Tm Σ A) → Tmₛ (σ ₛ∘ₑ δ) t ≡ Tmₑ δ (Tmₛ σ t)
Tm-ₛ∘ₑ σ δ (var v)   = ∈-ₛ∘ₑ σ δ v
Tm-ₛ∘ₑ σ δ (lam t)   =
  lam &
      ((λ x → Tmₛ (x , var vz) t) &
          (assₛₑₑ σ δ wk
        ◾ (σ ₛ∘ₑ_) & (drop & (idrₑ δ ◾ idlₑ δ ⁻¹))
        ◾ assₛₑₑ σ wk (keep δ) ⁻¹)
    ◾ Tm-ₛ∘ₑ (keepₛ σ) (keep δ) t)
Tm-ₛ∘ₑ σ δ (app f a) = app & Tm-ₛ∘ₑ σ δ f ⊗ Tm-ₛ∘ₑ σ δ a

assₛₑₛ :
  ∀ {Γ Δ Σ Ξ}(σ : Sub Σ Ξ)(δ : OPE Δ Σ)(ν : Sub Γ Δ)
  → (σ ₛ∘ₑ δ) ∘ₛ ν ≡ σ ∘ₛ (δ ₑ∘ₛ ν)
assₛₑₛ ∙       δ ν = refl
assₛₑₛ (σ , t) δ ν = _,_ & assₛₑₛ σ δ ν ⊗ (Tm-ₑ∘ₛ δ ν t ⁻¹)

assₛₛₑ :
  ∀ {Γ Δ Σ Ξ}(σ : Sub Σ Ξ)(δ : Sub Δ Σ)(ν : OPE Γ Δ)
  → (σ ∘ₛ δ) ₛ∘ₑ ν ≡ σ ∘ₛ (δ ₛ∘ₑ ν)
assₛₛₑ ∙       δ ν = refl
assₛₛₑ (σ , t) δ ν = _,_ & assₛₛₑ σ δ ν ⊗ (Tm-ₛ∘ₑ δ ν t ⁻¹)

∈-idₛ : ∀ {A Γ}(v : A ∈ Γ) → ∈ₛ idₛ v ≡ var v
∈-idₛ vz     = refl
∈-idₛ (vs v) = ∈-ₛ∘ₑ idₛ wk v ◾ Tmₑ wk & ∈-idₛ v ◾ (var ∘ vs) & ∈-idₑ v

∈-∘ₛ : ∀ {A Γ Δ Σ}(σ : Sub Δ Σ)(δ : Sub Γ Δ)(v : A ∈ Σ) → ∈ₛ (σ ∘ₛ δ) v ≡ Tmₛ δ (∈ₛ σ v)
∈-∘ₛ (σ , _) δ vz     = refl
∈-∘ₛ (σ , _) δ (vs v) = ∈-∘ₛ σ δ v

Tm-idₛ : ∀ {A Γ}(t : Tm Γ A) → Tmₛ idₛ t ≡ t
Tm-idₛ (var v)   = ∈-idₛ v
Tm-idₛ (lam t)   = lam & Tm-idₛ t
Tm-idₛ (app f a) = app & Tm-idₛ f ⊗ Tm-idₛ a

Tm-∘ₛ : ∀ {A Γ Δ Σ}(σ : Sub Δ Σ)(δ : Sub Γ Δ)(t : Tm Σ A) → Tmₛ (σ ∘ₛ δ) t ≡ Tmₛ δ (Tmₛ σ t)
Tm-∘ₛ σ δ (var v)   = ∈-∘ₛ σ δ v
Tm-∘ₛ σ δ (lam t)   =
  lam &
      ((λ x → Tmₛ (x , var vz) t) &
          (assₛₛₑ σ δ wk
        ◾ (σ ∘ₛ_) & (idlₑₛ  (dropₛ δ) ⁻¹) ◾ assₛₑₛ σ wk (keepₛ δ) ⁻¹)
    ◾ Tm-∘ₛ (keepₛ σ) (keepₛ δ) t)
Tm-∘ₛ σ δ (app f a) = app & Tm-∘ₛ σ δ f ⊗ Tm-∘ₛ σ δ a

idrₛ : ∀ {Γ Δ}(σ : Sub Γ Δ) → σ ∘ₛ idₛ ≡ σ
idrₛ ∙       = refl
idrₛ (σ , t) = _,_ & idrₛ σ ⊗ Tm-idₛ t

idlₛ : ∀ {Γ Δ}(σ : Sub Γ Δ) → idₛ ∘ₛ σ ≡ σ
idlₛ ∙       = refl
idlₛ (σ , t) = (_, t) & (assₛₑₛ idₛ wk (σ , t) ◾ (idₛ ∘ₛ_) & idlₑₛ σ ◾ idlₛ σ)

-- Reduction
--------------------------------------------------------------------------------

data _~>_ {Γ} : ∀ {A} → Tm Γ A → Tm Γ A → Set where
  β    : ∀ {A B}(t : Tm (Γ , A) B) t'  → app (lam t) t' ~> Tmₛ (idₛ , t') t
  lam  : ∀ {A B}{t t' : Tm (Γ , A) B}     → t ~> t' →  lam t   ~> lam t'
  app₁ : ∀ {A B}{f}{f' : Tm Γ (A ⇒ B)}{a} → f ~> f' →  app f a ~> app f' a
  app₂ : ∀ {A B}{f : Tm Γ (A ⇒ B)} {a a'} → a ~> a' →  app f a ~> app f  a'
infix 3 _~>_

~>ₛ : ∀ {Γ Δ A}{t t' : Tm Γ A}(σ : Sub Δ Γ) → t ~> t' → Tmₛ σ t ~> Tmₛ σ t'
~>ₛ σ (β t t') =
  coe ((app (lam (Tmₛ (keepₛ σ) t)) (Tmₛ σ t') ~>_) &
      (Tm-∘ₛ (keepₛ σ) (idₛ , Tmₛ σ t') t ⁻¹
    ◾ (λ x → Tmₛ (x , Tmₛ σ t') t) &
        (assₛₑₛ σ wk (idₛ , Tmₛ σ t')
      ◾ ((σ ∘ₛ_) & idlₑₛ idₛ ◾ idrₛ σ) ◾ idlₛ σ ⁻¹)
    ◾ Tm-∘ₛ (idₛ , t') σ t))
  (β (Tmₛ (keepₛ σ) t) (Tmₛ σ t'))
~>ₛ σ (lam  step) = lam  (~>ₛ (keepₛ σ) step)
~>ₛ σ (app₁ step) = app₁ (~>ₛ σ step)
~>ₛ σ (app₂ step) = app₂ (~>ₛ σ step)

~>ₑ : ∀ {Γ Δ A}{t t' : Tm Γ A}(σ : OPE Δ Γ) → t ~> t' → Tmₑ σ t ~> Tmₑ σ t'
~>ₑ σ (β t t')    =
  coe ((app (lam (Tmₑ (keep σ) t)) (Tmₑ σ t') ~>_)
      & (Tm-ₑ∘ₛ (keep σ) (idₛ , Tmₑ σ t') t ⁻¹
      ◾ (λ x → Tmₛ (x , Tmₑ σ t') t) & (idrₑₛ σ ◾ idlₛₑ σ ⁻¹)
      ◾ Tm-ₛ∘ₑ (idₛ , t') σ t))
  (β (Tmₑ (keep σ) t) (Tmₑ σ t'))
~>ₑ σ (lam step)  = lam (~>ₑ (keep σ) step)
~>ₑ σ (app₁ step) = app₁ (~>ₑ σ step)
~>ₑ σ (app₂ step) = app₂ (~>ₑ σ step)

Tmₑ~> :
  ∀ {Γ Δ A}{t : Tm Γ A}{σ : OPE Δ Γ}{t'}
  → Tmₑ σ t ~> t' → ∃ λ t'' → (t ~> t'') × (Tmₑ σ t'' ≡ t')
Tmₑ~> {t = var x} ()
Tmₑ~> {t = lam t} (lam step) with Tmₑ~> step
... | t'' , (p , refl) = lam t'' , lam p , refl
Tmₑ~> {t = app (var v) a} (app₁ ())
Tmₑ~> {t = app (var v) a} (app₂ step) with Tmₑ~> step
... | t'' , (p , refl) = app (var v) t'' , app₂ p , refl
Tmₑ~> {t = app (lam f) a} {σ} (β _ _) =
  Tmₛ (idₛ , a) f , β _ _ ,
      Tm-ₛ∘ₑ (idₛ , a) σ f ⁻¹
    ◾ (λ x →  Tmₛ (x , Tmₑ σ a) f) & (idlₛₑ σ ◾ idrₑₛ σ ⁻¹)
    ◾ Tm-ₑ∘ₛ (keep σ) (idₛ , Tmₑ σ a) f
Tmₑ~> {t = app (lam f) a}     (app₁ (lam step)) with Tmₑ~> step
... | t'' , (p , refl) = app (lam t'') a , app₁ (lam p) , refl
Tmₑ~> {t = app (lam f) a}     (app₂ step) with Tmₑ~> step
... | t'' , (p , refl) = app (lam f) t'' , app₂ p , refl
Tmₑ~> {t = app (app f a) a'}  (app₁ step) with Tmₑ~> step
... | t'' , (p , refl) = app t'' a' , app₁ p , refl
Tmₑ~> {t = app (app f a) a''} (app₂ step) with Tmₑ~> step
... | t'' , (p , refl) = app (app f a) t'' , app₂ p , refl

-- Strong normalization/neutrality definition
--------------------------------------------------------------------------------

data SN {Γ A} (t : Tm Γ A) : Set where
  sn : (∀ {t'} → t ~> t' → SN t') → SN t

SNₑ→ : ∀ {Γ Δ A}{t : Tm Γ A}(σ : OPE Δ Γ) → SN t → SN (Tmₑ σ t)
SNₑ→ σ (sn s) = sn λ {t'} step →
  let (t'' , (p , q)) = Tmₑ~> step in coe (SN & q) (SNₑ→ σ (s p))

SNₑ← : ∀ {Γ Δ A}{t : Tm Γ A}(σ : OPE Δ Γ) → SN (Tmₑ σ t) → SN t
SNₑ← σ (sn s) = sn λ step → SNₑ← σ (s (~>ₑ σ step))

SN-app₁ : ∀ {Γ A B}{f : Tm Γ (A ⇒ B)}{a} → SN (app f a) → SN f
SN-app₁ (sn s) = sn λ f~>f' → SN-app₁ (s (app₁ f~>f'))

neu : ∀ {Γ A} → Tm Γ A → Set
neu (lam _)   = ⊥
neu _         = ⊤

neuₑ : ∀ {Γ Δ A}(σ : OPE Δ Γ)(t : Tm Γ A) → neu t → neu (Tmₑ σ t)
neuₑ σ (lam t)   nt = nt
neuₑ σ (var v)   nt = tt
neuₑ σ (app f a) nt = tt

-- The actual proof, by Kripke logical predicate
--------------------------------------------------------------------------------

Tmᴾ : ∀ {Γ A} → Tm Γ A → Set
Tmᴾ {Γ}{ι}     t = SN t
Tmᴾ {Γ}{A ⇒ B} t = ∀ {Δ}(σ : OPE Δ Γ){a} → Tmᴾ a → Tmᴾ (app (Tmₑ σ t) a)

data Subᴾ {Γ} : ∀ {Δ} → Sub Γ Δ → Set where
  ∙   : Subᴾ ∙
  _,_ : ∀ {A Δ}{σ : Sub Γ Δ}{t : Tm Γ A}(σᴾ : Subᴾ σ)(tᴾ : Tmᴾ t) → Subᴾ (σ , t)

Tmᴾₑ : ∀ {Γ Δ A}{t : Tm Γ A}(σ : OPE Δ Γ) → Tmᴾ t → Tmᴾ (Tmₑ σ t)
Tmᴾₑ {A = ι}        σ tᴾ = SNₑ→ σ tᴾ
Tmᴾₑ {A = A ⇒ B}{t} σ tᴾ δ aᴾ rewrite Tm-∘ₑ σ δ t ⁻¹ = tᴾ (σ ∘ₑ δ) aᴾ

Subᴾₑ : ∀ {Γ Δ Σ}{σ : Sub Δ Σ}(δ : OPE Γ Δ) → Subᴾ σ → Subᴾ (σ ₛ∘ₑ δ)
Subᴾₑ σ ∙        = ∙
Subᴾₑ σ (δ , tᴾ) = Subᴾₑ σ δ , Tmᴾₑ σ tᴾ

~>ᴾ : ∀ {Γ A}{t t' : Tm Γ A} → t ~> t' → Tmᴾ t → Tmᴾ t'
~>ᴾ {A = ι}     t~>t' (sn tˢⁿ) = tˢⁿ t~>t'
~>ᴾ {A = A ⇒ B} t~>t' tᴾ       = λ σ aᴾ → ~>ᴾ (app₁ (~>ₑ σ t~>t')) (tᴾ σ aᴾ)

mutual
  -- quote
  qᴾ : ∀ {Γ A}{t : Tm Γ A} → Tmᴾ t → SN t
  qᴾ {A = ι}     tᴾ = tᴾ
  qᴾ {A = A ⇒ B} tᴾ = SNₑ← wk $ SN-app₁ (qᴾ $ tᴾ wk (uᴾ (var vz) (λ ())))

  -- unquote
  uᴾ : ∀ {Γ A}(t : Tm Γ A){nt : neu t} → (∀ {t'} → t ~> t' → Tmᴾ t') → Tmᴾ t
  uᴾ {Γ} {A = ι} t      f     = sn f
  uᴾ {Γ} {A ⇒ B} t {nt} f {Δ} σ {a} aᴾ =
    uᴾ (app (Tmₑ σ t) a) (go (Tmₑ σ t) (neuₑ σ t nt) f' a aᴾ (qᴾ aᴾ))
    where
      f' : ∀ {t'} → Tmₑ σ t ~> t' → Tmᴾ t'
      f' step δ aᴾ with Tmₑ~> step
      ... | t'' , step' , refl rewrite Tm-∘ₑ σ δ t'' ⁻¹ = f step' (σ ∘ₑ δ) aᴾ

      go :
        ∀ {Γ A B}(t : Tm Γ (A ⇒ B)) → neu t → (∀ {t'} → t ~> t' → Tmᴾ t')
        → ∀ a → Tmᴾ a → SN a → ∀ {t'} → app t a ~> t' → Tmᴾ t'
      go _ () _ _ _ _ (β _ _)
      go t nt f a aᴾ sna (app₁ {f' = f'} step) =
        coe ((λ x → Tmᴾ (app x a)) & Tm-idₑ f') (f step idₑ aᴾ)
      go t nt f a aᴾ (sn aˢⁿ) (app₂ {a' = a'} step) =
        uᴾ (app t a') (go t nt f a' (~>ᴾ step aᴾ) (aˢⁿ step))

fundThm-∈ : ∀ {Γ A}(v : A ∈ Γ) → ∀ {Δ}{σ : Sub Δ Γ} → Subᴾ σ → Tmᴾ (∈ₛ σ v)
fundThm-∈ vz     (σᴾ , tᴾ) = tᴾ
fundThm-∈ (vs v) (σᴾ , tᴾ) = fundThm-∈ v σᴾ

fundThm-lam :
  ∀ {Γ A B}
    (t : Tm (Γ , A) B)
  → SN t
  → (∀ {a} → Tmᴾ a → Tmᴾ (Tmₛ (idₛ , a) t))
  → ∀ a → SN a → Tmᴾ a → Tmᴾ (app (lam t) a)
fundThm-lam {Γ} t (sn tˢⁿ) hyp a (sn aˢⁿ) aᴾ = uᴾ (app (lam t) a)
  λ {(β _ _) → hyp aᴾ;
     (app₁ (lam {t' = t'} t~>t')) →
       fundThm-lam t' (tˢⁿ t~>t') (λ aᴾ → ~>ᴾ (~>ₛ _ t~>t') (hyp aᴾ)) a (sn aˢⁿ) aᴾ;
     (app₂ a~>a') →
       fundThm-lam t (sn tˢⁿ) hyp _ (aˢⁿ a~>a') (~>ᴾ a~>a' aᴾ)}

fundThm : ∀ {Γ A}(t : Tm Γ A) → ∀ {Δ}{σ : Sub Δ Γ} → Subᴾ σ → Tmᴾ (Tmₛ σ t)
fundThm (var v) σᴾ = fundThm-∈ v σᴾ
fundThm (lam {A} t) {σ = σ} σᴾ δ {a} aᴾ
  rewrite Tm-ₛ∘ₑ (keepₛ σ) (keep δ) t ⁻¹ | assₛₑₑ σ (wk {A}) (keep δ) | idlₑ δ
  = fundThm-lam
      (Tmₛ (σ ₛ∘ₑ drop δ , var vz) t)
      (qᴾ (fundThm t (Subᴾₑ (drop δ) σᴾ , uᴾ (var vz) (λ ()))))
      (λ aᴾ → coe (Tmᴾ & sub-sub-lem) (fundThm t (Subᴾₑ δ σᴾ , aᴾ)))
      a (qᴾ aᴾ) aᴾ
  where
    sub-sub-lem : ∀ {a} → Tmₛ (σ ₛ∘ₑ δ , a) t ≡ Tmₛ (idₛ , a) (Tmₛ (σ ₛ∘ₑ drop δ , var vz) t)
    sub-sub-lem {a} =
        (λ x → Tmₛ (x , a) t) &
          (idrₛ (σ ₛ∘ₑ δ) ⁻¹ ◾ assₛₑₛ σ δ idₛ ◾ assₛₑₛ σ (drop δ) (idₛ , a) ⁻¹)
      ◾ Tm-∘ₛ (σ ₛ∘ₑ drop δ , var vz) (idₛ , a) t
fundThm (app f a) {σ = σ} σᴾ
  rewrite Tm-idₑ (Tmₛ σ f) ⁻¹
  = fundThm f σᴾ idₑ (fundThm a σᴾ)

idₛᴾ : ∀ {Γ} → Subᴾ (idₛ {Γ})
idₛᴾ {∙}     = ∙
idₛᴾ {Γ , A} = Subᴾₑ wk idₛᴾ , uᴾ (var vz) (λ ())

strongNorm : ∀ {Γ A}(t : Tm Γ A) → SN t
strongNorm t = qᴾ (coe (Tmᴾ & Tm-idₛ t) (fundThm t idₛᴾ))


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

-- define a less-than-great equivalence on natural transformations
module Categories.NaturalTransformation.Equivalence where

open import Level
open import Relation.Binary using (Rel; IsEquivalence; Setoid)

open import Categories.Category
open import Categories.Functor
open import Categories.NaturalTransformation.Core

private
  variable
    o ℓ e o′ ℓ′ e′ : Level
    C D E : Category o ℓ e

-- This ad hoc equivalence for NaturalTransformation should really be 'modification'
--  (yep, tricategories!). What is below is only part of the definition of a 'modification'.  TODO
infix 4 _≃_

_≃_ : ∀ {F G : Functor C D} → Rel (NaturalTransformation F G) _
_≃_ {D = D} X Y = ∀ {x} → D [ NaturalTransformation.η X x ≈ NaturalTransformation.η Y x ]

≃-isEquivalence : ∀ {F G : Functor C D} → IsEquivalence (_≃_ {F = F} {G})
≃-isEquivalence {D = D} {F} {G} = record
  { refl  = refl
  ; sym   = λ f → sym f -- need to eta-expand to get things to line up properly
  ; trans = λ f g → trans f g
  }
  where open Category.Equiv D

≃-setoid : ∀ (F G : Functor C D) → Setoid _ _
≃-setoid F G = record
  { Carrier       = NaturalTransformation F G
  ; _≈_           = _≃_
  ; isEquivalence = ≃-isEquivalence
  }

ext: agda

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-

Computable stuff constructed from the Combinatorics of Finite Sets

-}
{-# OPTIONS --safe #-}

module Cubical.Experiments.Combinatorics where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.Data.Nat
open import Cubical.Data.Sum
open import Cubical.Data.Sigma

open import Cubical.Data.Fin
open import Cubical.Data.FinSet
open import Cubical.Data.FinSet.Constructors

open import Cubical.Functions.Embedding
open import Cubical.Functions.Surjection

-- some computable functions

-- this should be addtion
card+ : ℕ → ℕ → ℕ
card+ m n = card (Fin m ⊎ Fin n , isFinSet⊎ (Fin m , isFinSetFin) (Fin n , isFinSetFin))

-- this should be multiplication
card× : ℕ → ℕ → ℕ
card× m n = card (Fin m × Fin n , isFinSet× (Fin m , isFinSetFin) (Fin n , isFinSetFin))

-- this should be exponential
card→ : ℕ → ℕ → ℕ
card→ m n = card ((Fin m → Fin n) , isFinSet→ (Fin m , isFinSetFin) (Fin n , isFinSetFin))

-- this should be factorial or zero
card≃ : ℕ → ℕ → ℕ
card≃ m n = card ((Fin m ≃ Fin n) , isFinSet≃ (Fin m , isFinSetFin) (Fin n , isFinSetFin))

-- this should be binomial coeffient
card↪ : ℕ → ℕ → ℕ
card↪ m n = card ((Fin m ↪ Fin n) , isFinSet↪ (Fin m , isFinSetFin) (Fin n , isFinSetFin))

-- this should be something that I don't know the name
card↠ : ℕ → ℕ → ℕ
card↠ m n = card ((Fin m ↠ Fin n) , isFinSet↠ (Fin m , isFinSetFin) (Fin n , isFinSetFin))

-- explicit numbers

s2 : card≃ 2 2 ≡ 2
s2 = refl

s3 : card≃ 3 3 ≡ 6
s3 = refl

c3,2 : card↪ 2 3 ≡ 6
c3,2 = refl

max_stars_repo_name: FernandoLarrain/cubical


text:
module FFI.Data.Maybe where

open import Agda.Builtin.Equality using (_≡_; refl)

{-# FOREIGN GHC import qualified Data.Maybe #-}

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A → Maybe A
{-# COMPILE GHC Maybe = data Data.Maybe.Maybe (Data.Maybe.Nothing|Data.Maybe.Just) #-}

just-inv : ∀ {A} {x y : A} → (just x ≡ just y) → (x ≡ y)
just-inv refl = refl

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
module JVM.Syntax where

open import JVM.Syntax.Instructions public


text:
module DotPatternTermination where

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

-- A simple example.
module Test1 where
  data D : Nat -> Set where
    cz : D zero
    c1 : forall {n} -> D n -> D (suc n)
    c2 : forall {n} -> D n -> D n

  -- To see that this is terminating the termination checker has to look at the
  -- natural number index, which is in a dot pattern.
  f : forall {n} -> D n -> Nat
  f cz     = zero
  f (c1 d) = f (c2 d)
  f (c2 d) = f d

-- There was a bug with dot patterns having the wrong context which manifested
-- itself in the following example.
module Test2 where
  data P : Nat -> Nat -> Set where
    c  : forall {d r} -> P d r -> P (suc d) r
    c' : forall {d r} -> P d r -> P d r

  g : forall {d r} -> P d r -> Nat
  g .{suc d} {r} (c {d} .{r} x) = g (c' x)
  g (c' _) = zero

-- Another bug where the dot patterns weren't substituted properly.
module Test3 where

  data Parser : Nat -> Set where
    alt :  (d : Nat) -> Nat -> Parser d -> Parser (suc d)
    !   :  (d : Nat) -> Parser (suc d)
    pp  :  (d : Nat) -> Parser d

  parse₀ : (d : Nat) -> Parser d -> Nat
  parse₀ .(suc d) (alt d zero p) = parse₀ d p
  parse₀ .(suc d) (alt d _ p)    = parse₀ d p
  parse₀ ._       (! d)          = parse₀ d (pp d)
  parse₀ ._       (pp d)         = zero

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Characters
------------------------------------------------------------------------

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

module Data.Char where

------------------------------------------------------------------------
-- Re-export base definitions and decidability of equality

open import Data.Char.Base public
open import Data.Char.Properties using (_≟_; _==_) public


text:
-- All 256 ASCII characters

module LineEndings.LexASCII where

{- In Block comment:

Control characters 0-31

Rest of 7-bit ASCII

 !"#$%&'()*+,-./0123456789:;<=>?
@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_
`abcdefghijklmnopqrstuvwxyz{|}~

8-Bit ASCII

 ¡¢£¤¥¦§¨©ª«¬®¯°±²³´µ¶·¸¹º»¼½¾¿
ÀÁÂÃÄÅÆÇÈÉÊËÌÍÎÏÐÑÒÓÔÕÖ×ØÙÚÛÜÝÞß
àáâãäåæçèéêëìíîïðñòóôõö÷øùúûüýþÿ

-}

-- In line comments

--
--
--

--  !"#$%&'()*+,-./0123456789:;<=>?
-- @ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_
-- `abcdefghijklmnopqrstuvwxyz{|}~

--

-- Note: Agda translates the following character (decimal: 133 xd: x85)
-- into a new line, see function convertLineEndings.

--

--
--
--
--

--  ¡¢£¤¥¦§¨©ª«¬®¯°±²³´µ¶·¸¹º»¼½¾¿
-- ÀÁÂÃÄÅÆÇÈÉÊËÌÍÎÏÐÑÒÓÔÕÖ×ØÙÚÛÜÝÞß
-- àáâãäåæçèéêëìíîïðñòóôõö÷øùúûüýþÿ

-- -}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Esterel.Context where

open import Esterel.Lang
open import Esterel.Environment
  using (Env)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ) renaming (_≟ₛₜ_ to _≟ₛₜₛ_)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ) renaming (_≟ₛₜ_ to _≟ₛₜₛₕ_)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ)

open import Data.List
  using (List ; _∷_ ; [])

infix   7 _⟦_⟧e
infix   7 _⟦_⟧c
infix   4 _≐_⟦_⟧e
infix   4 _≐_⟦_⟧c

data EvaluationContext1 : Set where
  epar₁    : (q : Term)    → EvaluationContext1
  epar₂    : (p : Term)    → EvaluationContext1
  eseq     : (q : Term)    → EvaluationContext1
  eloopˢ   : (q : Term)    → EvaluationContext1
  esuspend : (S : Signal)  → EvaluationContext1
  etrap    :                 EvaluationContext1

EvaluationContext : Set
EvaluationContext = List EvaluationContext1

_⟦_⟧e : EvaluationContext → Term → Term
[]               ⟦ p ⟧e = p
(epar₁ q ∷ E)    ⟦ p ⟧e = (E ⟦ p ⟧e) ∥  q
(epar₂ p ∷ E)    ⟦ q ⟧e = p          ∥  (E ⟦ q ⟧e)
(eseq q ∷ E)     ⟦ p ⟧e = (E ⟦ p ⟧e) >> q
(eloopˢ q ∷ E)   ⟦ p ⟧e = loopˢ (E ⟦ p ⟧e) q
(esuspend S ∷ E) ⟦ p ⟧e = suspend (E ⟦ p ⟧e) S
(etrap ∷ E)      ⟦ p ⟧e = trap (E ⟦ p ⟧e)

data _≐_⟦_⟧e : Term → EvaluationContext → Term → Set where
  dehole    : ∀{p}                        → (p           ≐  []               ⟦ p ⟧e)
  depar₁    : ∀{p r q E} → (p ≐ E ⟦ r ⟧e) → (p ∥ q       ≐  (epar₁ q ∷ E)    ⟦ r ⟧e)
  depar₂    : ∀{p r q E} → (q ≐ E ⟦ r ⟧e) → (p ∥ q       ≐  (epar₂ p ∷ E)    ⟦ r ⟧e)
  deseq     : ∀{p r q E} → (p ≐ E ⟦ r ⟧e) → (p >> q      ≐  (eseq q ∷ E)     ⟦ r ⟧e)
  deloopˢ   : ∀{p r q E} → (p ≐ E ⟦ r ⟧e) → (loopˢ p q   ≐  (eloopˢ q ∷ E)   ⟦ r ⟧e)
  desuspend : ∀{p E r S} → (p ≐ E ⟦ r ⟧e) → (suspend p S ≐  (esuspend S ∷ E) ⟦ r ⟧e)
  detrap    : ∀{p E r}   → (p ≐ E ⟦ r ⟧e) → (trap p      ≐  (etrap ∷ E)      ⟦ r ⟧e)

-- Should we just not use inclusion from EvaluationContext?
data Context1 : Set where
  ceval     : (E1 : EvaluationContext1) → Context1
  csignl    : (S : Signal) → Context1
  cpresent₁ : (S : Signal) → (q : Term) → Context1
  cpresent₂ : (S : Signal) → (p : Term) → Context1
  cloop     : Context1
  cloopˢ₂   : (p : Term) → Context1
  cseq₂     : (p : Term) → Context1
  cshared   : (s : SharedVar) → (e : Expr) → Context1
  cvar      : (x : SeqVar) → (e : Expr) → Context1
  cif₁      : (x : SeqVar) → (q : Term) → Context1
  cif₂      : (x : SeqVar) → (p : Term) → Context1
  cenv      : (θ : Env) →  (A : Ctrl) → Context1

Context : Set
Context = List Context1

_⟦_⟧c : Context → Term → Term
[]                       ⟦ p ⟧c = p
(ceval (epar₁ q) ∷ C)    ⟦ p ⟧c = (C ⟦ p ⟧c) ∥ q
(ceval (epar₂ p) ∷ C)    ⟦ q ⟧c = p          ∥ (C ⟦ q ⟧c)
(ceval (eseq q) ∷ C)     ⟦ p ⟧c = (C ⟦ p ⟧c) >> q
(ceval (eloopˢ q) ∷ C)   ⟦ p ⟧c = loopˢ (C ⟦ p ⟧c) q
(cseq₂ p ∷ C)            ⟦ q ⟧c = p          >> (C ⟦ q ⟧c)
(ceval (esuspend S) ∷ C) ⟦ p ⟧c = suspend (C ⟦ p ⟧c) S
(ceval etrap ∷ C)        ⟦ p ⟧c = trap (C ⟦ p ⟧c)
(csignl S ∷ C)           ⟦ p ⟧c = signl S (C ⟦ p ⟧c)
(cpresent₁ S q ∷ C)      ⟦ p ⟧c = present S ∣⇒ (C ⟦ p ⟧c) ∣⇒ q
(cpresent₂ S p ∷ C)      ⟦ q ⟧c = present S ∣⇒ p          ∣⇒ (C ⟦ q ⟧c)
(cloop ∷ C)              ⟦ p ⟧c = loop (C ⟦ p ⟧c)
(cloopˢ₂ p ∷ C)          ⟦ q ⟧c = loopˢ p (C ⟦ q ⟧c)
(cshared s e ∷ C)        ⟦ p ⟧c = shared s ≔ e in: (C ⟦ p ⟧c)
(cvar x e ∷ C)           ⟦ p ⟧c = var x ≔ e in: (C ⟦ p ⟧c)
(cif₁ x q ∷ C)           ⟦ p ⟧c = if x ∣⇒ (C ⟦ p ⟧c) ∣⇒ q
(cif₂ x p ∷ C)           ⟦ q ⟧c = if x ∣⇒ p          ∣⇒ (C ⟦ q ⟧c)
(cenv θ A ∷ C)           ⟦ p ⟧c = ρ⟨ θ , A ⟩· (C ⟦ p ⟧c)

data _≐_⟦_⟧c : Term → Context → Term → Set where
  dchole     : ∀{p}                            → (p                    ≐  []                       ⟦ p ⟧c)
  dcpar₁     : ∀{p r q C}     → (p ≐ C ⟦ r ⟧c) → (p ∥ q                ≐  (ceval (epar₁ q) ∷ C)    ⟦ r ⟧c)
  dcpar₂     : ∀{p r q C}     → (q ≐ C ⟦ r ⟧c) → (p ∥ q                ≐  (ceval (epar₂ p) ∷ C)    ⟦ r ⟧c)
  dcseq₁     : ∀{p r q C}     → (p ≐ C ⟦ r ⟧c) → (p >> q               ≐  (ceval (eseq q) ∷ C)     ⟦ r ⟧c)
  dcseq₂     : ∀{p r q C}     → (q ≐ C ⟦ r ⟧c) → (p >> q               ≐  (cseq₂ p ∷ C)            ⟦ r ⟧c)
  dcsuspend  : ∀{p C r S}     → (p ≐ C ⟦ r ⟧c) → (suspend p S          ≐  (ceval (esuspend S) ∷ C) ⟦ r ⟧c)
  dctrap     : ∀{p C r}       → (p ≐ C ⟦ r ⟧c) → (trap p               ≐  (ceval etrap ∷ C)        ⟦ r ⟧c)
  dcsignl    : ∀{p C r S}     → (p ≐ C ⟦ r ⟧c) → (signl S p            ≐  (csignl S ∷ C)           ⟦ r ⟧c)
  dcpresent₁ : ∀{p r q C S}   → (p ≐ C ⟦ r ⟧c) → (present S ∣⇒ p ∣⇒ q   ≐  (cpresent₁ S q ∷ C)      ⟦ r ⟧c)
  dcpresent₂ : ∀{p r q C S}   → (q ≐ C ⟦ r ⟧c) → (present S ∣⇒ p ∣⇒ q   ≐  (cpresent₂ S p ∷ C)      ⟦ r ⟧c)
  dcloop     : ∀{p C r}       → (p ≐ C ⟦ r ⟧c) → (loop p               ≐  (cloop ∷ C)              ⟦ r ⟧c)
  dcloopˢ₁   : ∀{p q C r}     → (p ≐ C ⟦ r ⟧c) → (loopˢ p q            ≐  (ceval (eloopˢ q) ∷ C)   ⟦ r ⟧c)
  dcloopˢ₂   : ∀{p q C r}     → (q ≐ C ⟦ r ⟧c) → (loopˢ p q            ≐  (cloopˢ₂ p ∷ C)          ⟦ r ⟧c)
  dcshared   : ∀{p C r s e}   → (p ≐ C ⟦ r ⟧c) → (shared s ≔ e in: p   ≐  (cshared s e ∷ C)        ⟦ r ⟧c)
  dcvar      : ∀{p C r x e}   → (p ≐ C ⟦ r ⟧c) → (var x ≔ e in: p      ≐  (cvar x e ∷ C)           ⟦ r ⟧c)
  dcif₁      : ∀{p r q x C}   → (p ≐ C ⟦ r ⟧c) → (if x ∣⇒ p ∣⇒ q        ≐  (cif₁ x q ∷ C)           ⟦ r ⟧c)
  dcif₂      : ∀{p r q x C}   → (q ≐ C ⟦ r ⟧c) → (if x ∣⇒ p ∣⇒ q        ≐  (cif₂ x p ∷ C)           ⟦ r ⟧c)
  dcenv      : ∀{p C r θ A}     → (p ≐ C ⟦ r ⟧c) → (ρ⟨ θ , A ⟩· p       ≐  (cenv θ A ∷ C)             ⟦ r ⟧c)

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
module Cats.Category.Constructions.Terminal where

open import Data.Product using (proj₁ ; proj₂)
open import Level

open import Cats.Category.Base

import Cats.Category.Constructions.Iso as Iso
import Cats.Category.Constructions.Unique as Unique

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

  open Category Cat
  open Iso.Build Cat
  open Unique.Build Cat

  IsTerminal : Obj → Set (lo ⊔ la ⊔ l≈)
  IsTerminal One = ∀ X → ∃! X One

  terminal→id-unique : ∀ {A} → IsTerminal A → IsUnique (id {A})
  terminal→id-unique {A} term id′ with term A
  ... | ∃!-intro id″ _ id″-uniq = ≈.trans (≈.sym (id″-uniq _)) (id″-uniq _)

  terminal-unique : ∀ {A B} → IsTerminal A → IsTerminal B → A ≅ B
  terminal-unique {A} {B} A-term B-term = record
      { forth = ∃!′.arr (B-term A)
      ; back = ∃!′.arr (A-term B)
      ; back-forth = ≈.sym (terminal→id-unique A-term _)
      ; forth-back = ≈.sym (terminal→id-unique B-term _)
      }

  X⇒Terminal-unique : ∀ {One} → IsTerminal One → ∀ {X} {f g : X ⇒ One} → f ≈ g
  X⇒Terminal-unique term {X} {f} {g} with term X
  ... | ∃!-intro x _ x-uniq = ≈.trans (≈.sym (x-uniq _)) (x-uniq _)

record HasTerminal {lo la l≈} (Cat : Category lo la l≈)
  : Set (lo ⊔ la ⊔ l≈) where
  open Category Cat
  open Build Cat

  field
    One : Obj
    isTerminal : IsTerminal One

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:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax Combinatory | CL

type
  * : 0-ary

term
  app : *  *  ->  * | _$_ l20
  i   : *
  k   : *
  s   : *

theory
  (IA) x     |> app (i, x) = x
  (KA) x y   |> app (app(k, x), y) = x
  (SA) x y z |> app (app (app (s, x), y), z) = app (app(x, z), app(y, z))
-}

module Combinatory.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import Combinatory.Signature
open import Combinatory.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution CL:Syn
open import SOAS.Metatheory.SecondOrder.Equality CL:Syn

private
  variable
    α β γ τ : *T
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ CL) α Γ → (𝔐 ▷ CL) α Γ → Set where
  IA : ⁅ * ⁆̣             ▹ ∅ ⊢             I $ 𝔞 ≋ₐ 𝔞
  KA : ⁅ * ⁆ ⁅ * ⁆̣       ▹ ∅ ⊢       (K $ 𝔞) $ 𝔟 ≋ₐ 𝔞
  SA : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ ((S $ 𝔞) $ 𝔟) $ 𝔠 ≋ₐ (𝔞 $ 𝔠) $ (𝔟 $ 𝔠)

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
-- Andreas, 2019-06-25, issue #3855 reported by nad
-- Constraint solver needs to respect erasure.

module _
  (_≡_ : {A : Set₁} → A → A → Set)
  (refl : {A : Set₁} (x : A) → x ≡ x)
  where

-- rejected : (@0 A : Set) → A ≡ A
-- rejected A = refl A

should-also-be-rejected : (@0 A : Set) → A ≡ A
should-also-be-rejected A = refl _

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Agda is an /interactive/ language;
-- that's very important difference (compared to language-pts)
module J where

open import Level
open import Data.Bool using (Bool; true; false)

data ⊤ : Set where
  I : ⊤

data ⊥ : Set where

data Eq {ℓ : Level} (A : Set ℓ) : A → A → Set ℓ where
  refl : {x : A} → Eq A x x

J : ∀ {ℓ ℓ′} (A : Set ℓ)
  → (C : (x : A) → (y : A) → (p : Eq A x y) → Set ℓ′)
  → (r : (x : A) → C x x refl)
  → (u : A)
  → (v : A)
  → (p : Eq A u v)
  → C u v p
J A C r u .u refl = r u

Eq-sym : ∀ {ℓ} (A : Set ℓ) (x y : A) → Eq A x y → Eq A y x
Eq-sym A x .x refl = refl

Eq-sym-with-J : ∀ {ℓ} (A : Set ℓ) (x y : A) → Eq A x y → Eq A y x
Eq-sym-with-J A = J A (λ x y _ → Eq A y x) (λ x → refl)

Eq-trans-with-J : ∀ {ℓ} (A : Set ℓ) (x y z : A) → Eq A x y → Eq A y z → Eq A x z
Eq-trans-with-J A x y z p = J A (λ u v _ → Eq A v z → Eq A u z) (λ _ r → r) x y p

Bool-elim : ∀ {ℓ} (P : Bool → Set ℓ) → P true → P false  → (b : Bool) → P b
Bool-elim P t f false = f
Bool-elim P t f true  = t

if1 : (r : Set1) → Bool → r → r → r
if1 r b t f = Bool-elim (λ _ → r) t f b

lemma-motive : Bool → Bool → Set
lemma-motive u v = if1 Set u (if1 Set v ⊤ ⊥) ⊤

lemma : Eq Bool true false → ⊥
lemma p = J Bool
  (λ u v _ → lemma-motive u v)
  (λ b → Bool-elim (λ c → lemma-motive c c) I I b )
  true false p

max_stars_repo_name: phadej/language-pts

max_issues_repo_name: phadej/language-pts

max_forks_repo_name: phadej/language-pts


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Unsafe String operations and proofs
------------------------------------------------------------------------

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

module Data.String.Unsafe where

open import Data.String.Base

open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe)

------------------------------------------------------------------------
-- Properties of conversion functions

toList∘fromList : ∀ s → toList (fromList s) ≡ s
toList∘fromList s = trustMe

fromList∘toList : ∀ s → fromList (toList s) ≡ s
fromList∘toList s = trustMe


text:
------------------------------------------------------------------------
-- A coinductive definition of weak bisimilarity
------------------------------------------------------------------------

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

open import Labelled-transition-system

module Bisimilarity.Weak {ℓ} (lts : LTS ℓ) where

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

import Function-universe equality-with-J as F

import Bisimilarity
import Bisimilarity.Equational-reasoning-instances
import Bisimilarity.General
open import Equational-reasoning
import Expansion
import Expansion.Equational-reasoning-instances
open import Indexed-container using (Container; ν; ν′)
open import Relation
open import Up-to

open LTS lts
private
  open module SB = Bisimilarity lts
    using (_∼_; _∼′_; [_]_∼_; [_]_∼′_)
  open module E = Expansion lts
    using (_≳_; _≳′_; _≲_; [_]_≳_; [_]_≳′_)

private
  module General = Bisimilarity.General lts _[_]⇒̂_ _[_]⇒̂_ ⟶→⇒̂ ⟶→⇒̂

open General public
  using (module StepC; ⟨_,_⟩; left-to-right; right-to-left; force;
         [_]_≡_; [_]_≡′_; []≡↔; Extensionality; extensionality)
  renaming ( reflexive-∼ to reflexive-≈
           ; reflexive-∼′ to reflexive-≈′
           ; ≡⇒∼ to ≡⇒≈
           ; ∼:_ to ≈:_
           ; ∼′:_ to ≈′:_
           ; module Bisimilarity-of-∼ to Bisimilarity-of-≈
           )

-- StepC is given in the following way, rather than via open public,
-- to make hyperlinks to it more informative.

StepC : Container (Proc × Proc) (Proc × Proc)
StepC = General.StepC

-- The following definitions are given explicitly, to make the code
-- easier to follow for readers of the paper.

Weak-bisimilarity : Size → Rel₂ ℓ Proc
Weak-bisimilarity = ν StepC

Weak-bisimilarity′ : Size → Rel₂ ℓ Proc
Weak-bisimilarity′ = ν′ StepC

infix 4 [_]_≈_ [_]_≈′_ _≈_ _≈′_

[_]_≈_ : Size → Proc → Proc → Type ℓ
[ i ] p ≈ q = ν StepC i (p , q)

[_]_≈′_ : Size → Proc → Proc → Type ℓ
[ i ] p ≈′ q = ν′ StepC i (p , q)

_≈_ : Proc → Proc → Type ℓ
_≈_ = [ ∞ ]_≈_

_≈′_ : Proc → Proc → Type ℓ
_≈′_ = [ ∞ ]_≈′_

private

  -- However, these definitions are definitionally equivalent to
  -- corresponding definitions in General.

  indirect-Weak-bisimilarity :
    Weak-bisimilarity ≡ General.Bisimilarity
  indirect-Weak-bisimilarity = refl

  indirect-Weak-bisimilarity′ :
    Weak-bisimilarity′ ≡ General.Bisimilarity′
  indirect-Weak-bisimilarity′ = refl

  indirect-[]≈ : [_]_≈_ ≡ General.[_]_∼_
  indirect-[]≈ = refl

  indirect-[]≈′ : [_]_≈′_ ≡ General.[_]_∼′_
  indirect-[]≈′ = refl

  indirect-≈ : _≈_ ≡ General._∼_
  indirect-≈ = refl

  indirect-≈′ : _≈′_ ≡ General._∼′_
  indirect-≈′ = refl

-- Combinators that can perhaps make the code a bit nicer to read.

infix -3 lr-result rl-result

lr-result : ∀ {i p′ q q′} μ → [ i ] p′ ≈′ q′ → q [ μ ]⇒̂ q′ →
            ∃ λ q′ → q [ μ ]⇒̂ q′ × [ i ] p′ ≈′ q′
lr-result _ p′≈′q′ q⇒̂q′ = _ , q⇒̂q′ , p′≈′q′

rl-result : ∀ {i p p′ q′} μ → p [ μ ]⇒̂ p′ → [ i ] p′ ≈′ q′ →
            ∃ λ p′ → p [ μ ]⇒̂ p′ × [ i ] p′ ≈′ q′
rl-result _ p⇒̂p′ p′≈′q′ = _ , p⇒̂p′ , p′≈′q′

syntax lr-result μ p′≈′q′ q⇒̂q′ = p′≈′q′ ⇐̂[ μ ] q⇒̂q′
syntax rl-result μ p⇒̂p′ p′≈′q′ = p⇒̂p′ ⇒̂[ μ ] p′≈′q′

-- Processes that are related by the expansion ordering are weakly
-- bisimilar.

mutual

  ≳⇒≈ : ∀ {i p q} → [ i ] p ≳ q → [ i ] p ≈ q
  ≳⇒≈ {i} = λ p≳q → StepC.⟨ lr p≳q , rl p≳q ⟩
    where
    lr : ∀ {p p′ q μ} →
         [ i ] p ≳ q → p [ μ ]⟶ p′ →
         ∃ λ q′ → q [ μ ]⇒̂ q′ × [ i ] p′ ≈′ q′
    lr p≳q q⟶q′ =
      let p′ , p⟶̂p′ , p′≳′q′ = E.left-to-right p≳q q⟶q′
      in p′ , ⟶̂→⇒̂ p⟶̂p′ , ≳⇒≈′ p′≳′q′

    rl : ∀ {p q q′ μ} →
         [ i ] p ≳ q → q [ μ ]⟶ q′ →
         ∃ λ p′ → p [ μ ]⇒̂ p′ × [ i ] p′ ≈′ q′
    rl p≳q q⟶q′ =
      let p′ , p⇒p′ , p′≳′q′ = E.right-to-left p≳q q⟶q′
      in p′ , ⇒→⇒̂ p⇒p′ , ≳⇒≈′ p′≳′q′

  ≳⇒≈′ : ∀ {i p q} → [ i ] p ≳′ q → [ i ] p ≈′ q
  force (≳⇒≈′ p≳′q) = ≳⇒≈ (SB.force p≳′q)

-- Strongly bisimilar processes are weakly bisimilar.

∼⇒≈ : ∀ {i p q} → [ i ] p ∼ q → [ i ] p ≈ q
∼⇒≈ = ≳⇒≈ ∘ convert {a = ℓ}

∼⇒≈′ : ∀ {i p q} → [ i ] p ∼′ q → [ i ] p ≈′ q
∼⇒≈′ = ≳⇒≈′ ∘ convert {a = ℓ}

-- Weak bisimilarity is a weak simulation (of one kind).

weak-is-weak⇒ :
  ∀ {p p′ q} →
  p ≈ q → p ⇒ p′ →
  ∃ λ q′ → q ⇒ q′ × p′ ≈ q′
weak-is-weak⇒ = is-weak⇒ StepC.left-to-right (λ p≈′q → force p≈′q) ⇒̂→⇒

-- Weak bisimilarity is a weak simulation (of another kind).

weak-is-weak⇒̂ :
  ∀ {p p′ q μ} →
  p ≈ q → p [ μ ]⇒̂ p′ →
  ∃ λ q′ → q [ μ ]⇒̂ q′ × p′ ≈ q′
weak-is-weak⇒̂ =
  is-weak⇒̂ StepC.left-to-right (λ p≈′q → force p≈′q) ⇒̂→⇒ id

mutual

  -- Weak bisimilarity is symmetric.

  symmetric-≈ : ∀ {i p q} → [ i ] p ≈ q → [ i ] q ≈ p
  symmetric-≈ p≈q =
    StepC.⟨ Σ-map id (Σ-map id symmetric-≈′) ∘ StepC.right-to-left p≈q
          , Σ-map id (Σ-map id symmetric-≈′) ∘ StepC.left-to-right p≈q
          ⟩

  symmetric-≈′ : ∀ {i p q} → [ i ] p ≈′ q → [ i ] q ≈′ p
  force (symmetric-≈′ p≈q) = symmetric-≈ (force p≈q)

private

  -- An alternative proof of symmetry.

  alternative-proof-of-symmetry : ∀ {i p q} → [ i ] p ≈ q → [ i ] q ≈ p
  alternative-proof-of-symmetry {i} =
    uncurry [ i ]_≈_ ⁻¹  ⊆⟨ ν-symmetric _ _ swap refl F.id ⟩∎
    uncurry [ i ]_≈_     ∎

mutual

  -- Weak bisimilarity is transitive.
  --
  -- Note that the transitivity proof is not claimed to be
  -- size-preserving. For proofs showing that transitivity cannot, in
  -- general, be size-preserving in any of its arguments, see
  -- Bisimilarity.Weak.Delay-monad.size-preserving-transitivityʳ⇔uninhabited
  -- and size-preserving-transitivityˡ⇔uninhabited.

  transitive-≈ : ∀ {i p q r} → p ≈ q → q ≈ r → [ i ] p ≈ r
  transitive-≈ {i} = λ p≈q q≈r →
    StepC.⟨ lr p≈q q≈r
          , Σ-map id (Σ-map id symmetric-≈′) ∘
            lr (symmetric-≈ q≈r) (symmetric-≈ p≈q)
          ⟩
    where
    lr : ∀ {p p′ q r μ} →
         p ≈ q → q ≈ r → p [ μ ]⟶ p′ →
         ∃ λ r′ → r [ μ ]⇒̂ r′ × [ i ] p′ ≈′ r′
    lr p≈q q≈r p⟶p′ =
      let q′ , q⇒̂q′ , p′≈′q′ = StepC.left-to-right p≈q p⟶p′
          r′ , r⇒̂r′ , q′≈r′  = weak-is-weak⇒̂ q≈r q⇒̂q′
      in r′ , r⇒̂r′ , transitive-≈′ p′≈′q′ q′≈r′

  transitive-≈′ : ∀ {i p q r} → p ≈′ q → q ≈ r → [ i ] p ≈′ r
  force (transitive-≈′ p≈q q≈r) = transitive-≈ (force p≈q) q≈r

-- The following variants of transitivity are partially
-- size-preserving.
--
-- For proofs showing that they cannot, in general, be size-preserving
-- in the "other" argument, see the following lemmas in
-- Bisimilarity.Weak.Delay-monad:
-- size-preserving-transitivity-≳≈ˡ⇔uninhabited,
-- size-preserving-transitivity-≈≲ʳ⇔uninhabited and
-- size-preserving-transitivity-≈∼ʳ⇔uninhabited.

mutual

  transitive-≳≈ : ∀ {i p q r} →
                  p ≳ q → [ i ] q ≈ r → [ i ] p ≈ r
  transitive-≳≈ {i} {p} {r = r} p≳q q≈r = StepC.⟨ lr , rl ⟩
    where
    lr : ∀ {p′ μ} → p [ μ ]⟶ p′ →
         ∃ λ r′ → r [ μ ]⇒̂ r′ × [ i ] p′ ≈′ r′
    lr p⟶p′ with E.left-to-right p≳q p⟶p′
    ... | _  , done s , p≳′q′  =
      r , silent s done
        , transitive-≳≈′ p≳′q′ (record { force = λ { {_} → q≈r } })
    ... | q′ , step q⟶q′ , p′≳′q′ =
      let r′ , r⇒̂r′ , q′≈′r′ = StepC.left-to-right q≈r q⟶q′
      in r′ , r⇒̂r′ , transitive-≳≈′ p′≳′q′ q′≈′r′

    rl : ∀ {r′ μ} → r [ μ ]⟶ r′ →
         ∃ λ p′ → p [ μ ]⇒̂ p′ × [ i ] p′ ≈′ r′
    rl r⟶r′ =
      let q′ , q⇒̂q′ , q′≈′r′ = StepC.right-to-left q≈r r⟶r′
          p′ , p⇒̂p′ , p′≳q′  = E.converse-of-expansion-is-weak⇒̂ p≳q q⇒̂q′
      in p′ , p⇒̂p′ , transitive-≳≈′ (record { force = p′≳q′ }) q′≈′r′

  transitive-≳≈′ : ∀ {i p q r} →
                   p ≳′ q → [ i ] q ≈′ r → [ i ] p ≈′ r
  force (transitive-≳≈′ p≳′q q≈′r) =
    transitive-≳≈ (force p≳′q) (force q≈′r)

transitive-≈≲ : ∀ {i p q r} →
                [ i ] p ≈ q → q ≲ r → [ i ] p ≈ r
transitive-≈≲ p≈q q≲r =
  symmetric-≈ (transitive-≳≈ q≲r (symmetric-≈ p≈q))

transitive-≈∼ : ∀ {i p q r} →
                [ i ] p ≈ q → q ∼ r → [ i ] p ≈ r
transitive-≈∼ p≈q q∼r =
  symmetric-≈ $
    transitive-≳≈ (convert {a = ℓ} (symmetric q∼r)) (symmetric-≈ p≈q)

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
module Itse.Grammar where

open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Unary
open import Data.List
open import Data.Maybe
open import Data.String
open import Data.Empty

data ExprVari : Set
Prgm : Set
data Stmt : Set
data Expr : ExprVari → Set
data Name : ExprVari → Set

data ExprVari where
  s : ExprVari -- sort
  k : ExprVari -- kind
  p : ExprVari -- type
  t : ExprVari -- term

_≟-ExprVari_ : ∀ (e : ExprVari) (e′ : ExprVari) → Dec (e ≡ e′)

TypeOf : ExprVari → ExprVari
TypeOf s = s
TypeOf k = s
TypeOf p = k
TypeOf t = p

Kind : Set
Type : Set
Term : Set
Nameₚ : Set
Nameₜ : Set

Sort = Expr s
Kind = Expr k
Type = Expr p
Term = Expr t
Nameₚ = Name p
Nameₜ = Name t

Prgm = List Stmt

infixr 10 `defnₚ_⦂_≔_ `defnₚ_⦂_≔_
infixr 11 _`→_
infixr 12 `λₖₚ[_⦂_]_ `λₖₜ[_⦂_]_ `λₚₚ[_⦂_]_ `λₚₜ[_⦂_]_ `λₜₚ[_⦂_]_ `λₜₜ[_⦂_]_
infixr 13 _`∙ₚₚ_ _`∙ₚₜ_ _`∙ₜₚ_ _`∙ₜₜ_
infixr 14 `ₚ_ `ₜ_

data Stmt where
  `defnₚ_⦂_≔_ : Nameₚ → Kind → Type → Stmt
  `defnₜ_⦂_≔_ : Nameₜ → Type → Term → Stmt

data Expr where
  -- sort
  `□ₛ : Sort
  -- kind
  `●ₖ : Kind
  `λₖₚ[_⦂_]_ : Nameₚ → Kind → Kind → Kind
  `λₖₜ[_⦂_]_ : Nameₜ → Type → Kind → Kind
  -- p
  `ₚ_        : Nameₚ → Type
  `λₚₚ[_⦂_]_ : Nameₚ → Kind → Type → Type
  `λₚₜ[_⦂_]_ : Nameₜ → Type → Type → Type
  _`∙ₚₚ_     : Type → Type → Type
  _`∙ₚₜ_     : Type → Term → Type
  `ι[_]_     : Nameₜ → Type → Type
  -- t
  `ₜ_        : Nameₜ → Term
  `λₜₚ[_⦂_]_ : Nameₚ → Kind → Term → Term
  `λₜₜ[_⦂_]_ : Nameₜ → Type → Term → Term
  _`∙ₜₚ_     : Term → Type → Term
  _`∙ₜₜ_     : Term → Term → Term

data Name where
  nameₚ : Maybe String → Nameₚ
  nameₜ : Maybe String → Nameₜ

postulate
  _≟-Name_ : ∀ {e} (n : Name e) → (n′ : Name e) → Dec (n ≡ n′)

s ≟-ExprVari s = yes refl
s ≟-ExprVari k = no λ ()
s ≟-ExprVari p = no λ ()
s ≟-ExprVari t = no λ ()
k ≟-ExprVari s = no λ ()
k ≟-ExprVari k = yes refl
k ≟-ExprVari p = no λ ()
k ≟-ExprVari t = no λ ()
p ≟-ExprVari s = no λ ()
p ≟-ExprVari k = no λ ()
p ≟-ExprVari p = yes refl
p ≟-ExprVari t = no λ ()
t ≟-ExprVari s = no λ ()
t ≟-ExprVari k = no λ ()
t ≟-ExprVari p = no λ ()
t ≟-ExprVari t = yes refl

_`→_ : Type → Type → Type
α `→ β = `λₚₜ[ nameₜ nothing ⦂ α ] β


text:
-- Andreas, 2016-07-27, issue #2117 reported by Guillermo Calderon

-- {-# OPTIONS -v tc:10 #-}

record R : Set₁ where
  field
    A : Set

open R {{...}}

record S (r : R) : Set where
  instance i = r
  field f : A

-- ERROR WAS:
-- No instance of type R was found in scope.
-- when checking that the expression A has type Set

-- Should succeed!


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Order morphisms
------------------------------------------------------------------------

module Relation.Binary.OrderMorphism where

open import Relation.Binary
open Poset
import Function as F
open import Level

record _⇒-Poset_ {p₁ p₂ p₃ p₄ p₅ p₆}
                 (P₁ : Poset p₁ p₂ p₃)
                 (P₂ : Poset p₄ p₅ p₆) : Set (p₁ ⊔ p₃ ⊔ p₄ ⊔ p₆) where
  field
    fun      : Carrier P₁ → Carrier P₂
    monotone : _≤_ P₁ =[ fun ]⇒ _≤_ P₂

_⇒-DTO_ : ∀ {p₁ p₂ p₃ p₄ p₅ p₆} →
          DecTotalOrder p₁ p₂ p₃ →
          DecTotalOrder p₄ p₅ p₆ → Set _
DTO₁ ⇒-DTO DTO₂ = poset DTO₁ ⇒-Poset poset DTO₂
  where open DecTotalOrder

open _⇒-Poset_

id : ∀ {p₁ p₂ p₃} {P : Poset p₁ p₂ p₃} → P ⇒-Poset P
id = record
  { fun      = F.id
  ; monotone = F.id
  }

_∘_ : ∀ {p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉}
        {P₁ : Poset p₁ p₂ p₃}
        {P₂ : Poset p₄ p₅ p₆}
        {P₃ : Poset p₇ p₈ p₉} →
      P₂ ⇒-Poset P₃ → P₁ ⇒-Poset P₂ → P₁ ⇒-Poset P₃
f ∘ g = record
  { fun      = F._∘_ (fun f)      (fun g)
  ; monotone = F._∘_ (monotone f) (monotone g)
  }

const : ∀ {p₁ p₂ p₃ p₄ p₅ p₆}
          {P₁ : Poset p₁ p₂ p₃}
          {P₂ : Poset p₄ p₅ p₆} →
        Carrier P₂ → P₁ ⇒-Poset P₂
const {P₂ = P₂} x = record
  { fun      = F.const x
  ; monotone = F.const (refl P₂)
  }


text:
module MJSF.Examples.Integer where

open import Prelude
open import Data.Maybe
open import Data.Star
open import Data.Bool
open import Data.List
open import Data.Integer
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All as All hiding (lookup)
open import Data.Product hiding (Σ)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable

k : ℕ
k = 5

open import MJSF.Syntax k
open import ScopesFrames.ScopesFrames k Ty

{-
    class Integer {
      int x = 0;
      void set(Integer b) {
        this.x = b.get()
      }
    }
-}

classes : List Ty
classes = (cᵗ (# 0) (# 1) ∷ [])

intmethods intfields : List Ty
intfields =
  {- x -} vᵗ int
  ∷ []
intmethods =
  {- set -} mᵗ ((ref (# 1)) ∷ []) void
  ∷ []

Integer : Scope
Integer = # 1

g : Graph
-- root scope
g zero = classes , []
-- class scope of Integer class
g (suc zero)= (intmethods ++ intfields) , zero ∷ []
-- scope of Integer.set method
g (suc (suc zero)) = (vᵗ (ref (# 1)) ∷ []) , # 1 ∷ []
-- scopes of main
g (suc (suc (suc zero))) = vᵗ (ref Integer) ∷ [] , (# 0 ∷ [])
g (suc (suc (suc (suc zero)))) = vᵗ (ref Integer) ∷ [] , # 3 ∷ []
g (suc (suc (suc (suc (suc ())))))

open SyntaxG g
open UsesGraph g

IntegerImpl : Class (# 0) (# 1)
IntegerImpl = class0 {ms = intmethods}{intfields}{[]}
  (-- methods
    (#m' (meth (# 2) (body-void
    (set
      (this [] (here refl))
      (path [] (there (here refl)))
      (get (var (path [] (here refl))) (path [] (there (here refl))))
    ◅ ε)))) ∷ [])
  (-- fields
    (#v' tt) ∷ [])
  []

{-
  int main() {
    Integer x;
    Integer y;
    x = new Integer();
    y = new Integer();
    x.x = 9;
    y.x = 18;
    y.set(x);
    return y.x;
  }
-}
main : Body (# 0) int
main = body
    (
        loc (# 3) (ref Integer)
      ◅ loc (# 4) (ref Integer)
      ◅ asgn (path (here refl ∷ []) (here refl)) (new (path (here refl ∷ here refl ∷ []) (here refl)))
      ◅ asgn (path [] (here refl)) (new (path (here refl ∷ here refl ∷ []) (here refl)))
      ◅ set (var (path (here refl ∷ []) (here refl))) (path [] (there (here refl))) (num (+ 9))
      ◅ set (var (path [] (here refl))) (path [] (there (here refl))) (num (+ 18))
      ◅ run (call (var (path [] (here refl))) (path [] (here refl)) (var (path (here refl ∷ []) (here refl)) ∷ []))
      ◅ ε
    )
    (get (var (path [] (here refl))) (path [] (there (here refl))))

p : Program (# 0) int
p = program classes (#c' (IntegerImpl , # 1 , obj (# 1) ⦃ refl ⦄)  ∷ []) main

open import MJSF.Semantics
open Semantics _ g
open import MJSF.Values
open ValuesG _ g

test : p ⇓⟨ 100 ⟩ (λ v → v ≡ num (+ 9) )
test = refl


text:
{-# OPTIONS --universe-polymorphism #-}

module Categories.Groupoid.Coproduct where

open import Level
open import Data.Sum

open import Categories.Category
open import Categories.Groupoid
open import Categories.Morphisms
import Categories.Coproduct as CoproductC

Coproduct : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
          → Groupoid C → Groupoid D → Groupoid (CoproductC.Coproduct C D)
Coproduct C D = record
  { _⁻¹ = λ { {inj₁ _} {inj₁ _} → λ { {lift f} → lift (C._⁻¹ f) }
            ; {inj₁ _} {inj₂ _} (lift ())
            ; {inj₂ _} {inj₁ _} (lift ())
            ; {inj₂ _} {inj₂ _} → λ { {lift f} → lift (D._⁻¹ f) }
            }
  ; iso = λ { {inj₁ _} {inj₁ _} → record { isoˡ = lift (Iso.isoˡ C.iso)
                                         ; isoʳ = lift (Iso.isoʳ C.iso) }
            ; {inj₁ _} {inj₂ _} {lift ()}
            ; {inj₂ _} {inj₁ _} {lift ()}
            ; {inj₂ _} {inj₂ _} → record { isoˡ = lift (Iso.isoˡ D.iso)
                                         ; isoʳ = lift (Iso.isoʳ D.iso) }
            }
  }
  where
  module C = Groupoid C
  module D = Groupoid D

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: copumpkin/categories

max_forks_repo_name: copumpkin/categories


text:
module nat where

open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
open import Data.Empty
open import Relation.Nullary
open import  Relation.Binary.PropositionalEquality
open import  logic

nat-<> : { x y : Nat } → x < y → y < x → ⊥
nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x

nat-<≡ : { x : Nat } → x < x → ⊥
nat-<≡  (s≤s lt) = nat-<≡ lt

nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥
nat-≡< refl lt = nat-<≡ lt

¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
¬a≤a  (s≤s lt) = ¬a≤a  lt

a<sa : {la : Nat} → la < Suc la
a<sa {Zero} = s≤s z≤n
a<sa {Suc la} = s≤s a<sa

=→¬< : {x : Nat  } → ¬ ( x < x )
=→¬< {Zero} ()
=→¬< {Suc x} (s≤s lt) = =→¬< lt

>→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
>→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x

<-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) )
<-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl
<-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n)
<-∨ {Suc x} {Zero} (s≤s ())
<-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt
<-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
<-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)

max : (x y : Nat) → Nat
max Zero Zero = Zero
max Zero (Suc x) = (Suc x)
max (Suc x) Zero = (Suc x)
max (Suc x) (Suc y) = Suc ( max x y )

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- "Evaluating" a polynomial, using Horner's method.
------------------------------------------------------------------------

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

open import Tactic.RingSolver.Core.Polynomial.Parameters

module Tactic.RingSolver.Core.Polynomial.Semantics
  {r₁ r₂ r₃ r₄}
  (homo : Homomorphism r₁ r₂ r₃ r₄)
  where

open import Data.Nat     using (ℕ; suc; zero; _≤′_; ≤′-step; ≤′-refl)
open import Data.Vec     using (Vec; []; _∷_; uncons)
open import Data.List    using ([]; _∷_)
open import Data.Product using (_,_; _×_)
open import Data.List.Kleene using (_+; _*; ∹_; _&_; [])

open Homomorphism homo
open import Tactic.RingSolver.Core.Polynomial.Base from
open import Algebra.Operations.Ring rawRing

drop : ∀ {i n} → i ≤′ n → Vec Carrier n → Vec Carrier i
drop ≤′-refl         xs       = xs
drop (≤′-step i+1≤n) (_ ∷ xs) = drop i+1≤n xs

drop-1 : ∀ {i n} → suc i ≤′ n → Vec Carrier n → Carrier × Vec Carrier i
drop-1 si≤n xs = uncons (drop si≤n xs)
{-# INLINE drop-1 #-}

_*⟨_⟩^_ : Carrier → Carrier → ℕ → Carrier
x *⟨ ρ ⟩^ zero = x
x *⟨ ρ ⟩^ suc i = ρ ^ i +1 * x
{-# INLINE _*⟨_⟩^_ #-}

--------------------------------------------------------------------------------
-- Evaluation
--------------------------------------------------------------------------------
-- Why do we have three functions here? Why are they so weird looking?
--
-- These three functions are the main bottleneck for all of the proofs: as such,
-- slight changes can dramatically affect the length of proof code.

mutual

  _⟦∷⟧_ : ∀ {n} → Poly n × Coeff n * → Carrier × Vec Carrier n → Carrier
  (x , [])     ⟦∷⟧ (ρ , ρs) = ⟦ x ⟧ ρs
  (x , (∹ xs)) ⟦∷⟧ (ρ , ρs) = ρ * ⅀⟦ xs ⟧ (ρ , ρs) + ⟦ x ⟧ ρs

  ⅀⟦_⟧ : ∀ {n} → Coeff n + → (Carrier × Vec Carrier n) → Carrier
  ⅀⟦ x ≠0 Δ i & xs ⟧ (ρ , ρs) = ((x , xs) ⟦∷⟧ (ρ , ρs)) *⟨ ρ ⟩^ i
  {-# INLINE ⅀⟦_⟧ #-}

  ⟦_⟧ : ∀ {n} → Poly n → Vec Carrier n → Carrier
  ⟦ Κ x  ⊐ i≤n ⟧ _ = ⟦ x ⟧ᵣ
  ⟦ ⅀ xs ⊐ i≤n ⟧ Ρ = ⅀⟦ xs ⟧ (drop-1 i≤n Ρ)
  {-# INLINE ⟦_⟧ #-}

--------------------------------------------------------------------------------
-- Performance
--------------------------------------------------------------------------------
-- As you might imagine, the implementation of the functions above seriously
-- affect performance. What you might not realise, though, is that the most
-- important component is the *order of the arguments*. For instance, if
-- we change:
--
--   (x , xs) ⟦∷⟧ (ρ , ρs) = ρ * ⅀⟦ xs ⟧ (ρ , ρs) + ⟦ x ⟧ ρs
--
-- To:
--
--   (x , xs) ⟦∷⟧ (ρ , ρs) = ⟦ x ⟧ ρs +  ⅀⟦ xs ⟧ (ρ , ρs) * ρ
--
-- We get a function that's several orders of magnitude slower!


text:
-- Andreas, 2016-08-08, issue #2132 reported by effectfully
-- Pattern synonyms in lhss of display form definitions

-- {-# OPTIONS -v scope:50 -v tc.decl:10 #-}

open import Common.Equality

data D : Set where
  C c : D
  g : D → D

pattern C′ = C

{-# DISPLAY C′ = C′ #-}
{-# DISPLAY g C′ = c #-}

-- Since pattern synonyms are now expanded on lhs of DISPLAY,
-- this behaves as
-- {-# DISPLAY C = C′ #-}
-- {-# DISPLAY g C = c #-}

test : C ≡ g C
test = refl

-- Expected error:
-- C′ != c of type D
-- when checking that the expression refl has type C′ ≡ c


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

open import Examples.Sorting.Parallel.Comparable

module Examples.Sorting.Parallel.Core (M : Comparable) where

open import Calf.CostMonoid
open ParCostMonoid parCostMonoid
  hiding (costMonoid)
  renaming (
    _≤_ to _≤ₚ_;
    ≤-refl to ≤ₚ-refl;
    ≤-trans to ≤ₚ-trans;
    module ≤-Reasoning to ≤ₚ-Reasoning
  ) public

open import Examples.Sorting.Core costMonoid fromℕ M public

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some boring lemmas used by the ring solver
------------------------------------------------------------------------

-- Note that these proofs use all "almost commutative ring" properties.

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

open import Algebra
open import Algebra.Solver.Ring.AlmostCommutativeRing

module Algebra.Solver.Ring.Lemmas
  {r₁ r₂ r₃}
  (coeff : RawRing r₁)
  (r : AlmostCommutativeRing r₂ r₃)
  (morphism : coeff -Raw-AlmostCommutative⟶ r)
  where

private
  module C = RawRing coeff
open AlmostCommutativeRing r
open import Algebra.Morphism
open _-Raw-AlmostCommutative⟶_ morphism
open import Relation.Binary.Reasoning.Setoid setoid
open import Function

lemma₀ : ∀ a b c x →
         (a + b) * x + c ≈ a * x + (b * x + c)
lemma₀ a b c x = begin
  (a + b) * x + c      ≈⟨ distribʳ _ _ _ ⟨ +-cong ⟩ refl ⟩
  (a * x + b * x) + c  ≈⟨ +-assoc _ _ _ ⟩
  a * x + (b * x + c)  ∎

lemma₁ : ∀ a b c d x →
         (a + b) * x + (c + d) ≈ (a * x + c) + (b * x + d)
lemma₁ a b c d x = begin
  (a + b) * x + (c + d)      ≈⟨ lemma₀ _ _ _ _ ⟩
  a * x + (b * x + (c + d))  ≈⟨ refl ⟨ +-cong ⟩ sym (+-assoc _ _ _) ⟩
  a * x + ((b * x + c) + d)  ≈⟨ refl ⟨ +-cong ⟩ (+-comm _ _ ⟨ +-cong ⟩ refl) ⟩
  a * x + ((c + b * x) + d)  ≈⟨ refl ⟨ +-cong ⟩ +-assoc _ _ _ ⟩
  a * x + (c + (b * x + d))  ≈⟨ sym $ +-assoc _ _ _ ⟩
  (a * x + c) + (b * x + d)  ∎

lemma₂ : ∀ a b c x → a * c * x + b * c ≈ (a * x + b) * c
lemma₂ a b c x = begin
  a * c * x + b * c  ≈⟨ lem ⟨ +-cong ⟩ refl ⟩
  a * x * c + b * c  ≈⟨ sym $ distribʳ _ _ _ ⟩
  (a * x + b) * c    ∎
  where
  lem = begin
    a * c * x    ≈⟨ *-assoc _ _ _ ⟩
    a * (c * x)  ≈⟨ refl ⟨ *-cong ⟩ *-comm _ _ ⟩
    a * (x * c)  ≈⟨ sym $ *-assoc _ _ _ ⟩
    a * x * c    ∎

lemma₃ : ∀ a b c x → a * b * x + a * c ≈ a * (b * x + c)
lemma₃ a b c x = begin
  a * b * x + a * c    ≈⟨ *-assoc _ _ _ ⟨ +-cong ⟩ refl ⟩
  a * (b * x) + a * c  ≈⟨ sym $ distribˡ _ _ _ ⟩
  a * (b * x + c)      ∎

lemma₄ : ∀ a b c d x →
         (a * c * x + (a * d + b * c)) * x + b * d ≈
         (a * x + b) * (c * x + d)
lemma₄ a b c d x = begin
  (a * c * x + (a * d + b * c)) * x + b * d              ≈⟨ distribʳ _ _ _ ⟨ +-cong ⟩ refl ⟩
  (a * c * x * x + (a * d + b * c) * x) + b * d          ≈⟨ refl ⟨ +-cong ⟩ ((refl ⟨ +-cong ⟩ refl) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ refl ⟩
  (a * c * x * x + (a * d + b * c) * x) + b * d          ≈⟨ +-assoc _ _ _  ⟩
  a * c * x * x + ((a * d + b * c) * x + b * d)          ≈⟨ lem₁ ⟨ +-cong ⟩ (lem₂ ⟨ +-cong ⟩ refl) ⟩
  a * x * (c * x) + (a * x * d + b * (c * x) + b * d)    ≈⟨ refl ⟨ +-cong ⟩ +-assoc _ _ _ ⟩
  a * x * (c * x) + (a * x * d + (b * (c * x) + b * d))  ≈⟨ sym $ +-assoc _ _ _ ⟩
  a * x * (c * x) + a * x * d + (b * (c * x) + b * d)    ≈⟨ sym $ distribˡ _ _ _ ⟨ +-cong ⟩ distribˡ _ _ _ ⟩
  a * x * (c * x + d) + b * (c * x + d)                  ≈⟨ sym $ distribʳ _ _ _ ⟩
  (a * x + b) * (c * x + d)                              ∎
  where
  lem₁′ = begin
    a * c * x    ≈⟨ *-assoc _ _ _ ⟩
    a * (c * x)  ≈⟨ refl ⟨ *-cong ⟩ *-comm _ _ ⟩
    a * (x * c)  ≈⟨ sym $ *-assoc _ _ _ ⟩
    a * x * c    ∎

  lem₁ = begin
    a * c * x * x    ≈⟨ lem₁′ ⟨ *-cong ⟩ refl ⟩
    a * x * c * x    ≈⟨ *-assoc _ _ _ ⟩
    a * x * (c * x)  ∎

  lem₂ = begin
    (a * d + b * c) * x        ≈⟨ distribʳ _ _ _ ⟩
    a * d * x + b * c * x      ≈⟨ *-assoc _ _ _ ⟨ +-cong ⟩ *-assoc _ _ _ ⟩
    a * (d * x) + b * (c * x)  ≈⟨ (refl ⟨ *-cong ⟩ *-comm _ _) ⟨ +-cong ⟩ refl ⟩
    a * (x * d) + b * (c * x)  ≈⟨ sym $ *-assoc _ _ _ ⟨ +-cong ⟩ refl ⟩
    a * x * d + b * (c * x)    ∎

lemma₅ : ∀ x → (0# * x + 1#) * x + 0# ≈ x
lemma₅ x = begin
  (0# * x + 1#) * x + 0#   ≈⟨ ((zeroˡ _ ⟨ +-cong ⟩ refl) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ refl ⟩
  (0# + 1#) * x + 0#       ≈⟨ (+-identityˡ _ ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ refl ⟩
  1# * x + 0#              ≈⟨ +-identityʳ _ ⟩
  1# * x                   ≈⟨ *-identityˡ _ ⟩
  x                        ∎

lemma₆ : ∀ a x → 0# * x + a ≈ a
lemma₆ a x = begin
  0# * x + a    ≈⟨ zeroˡ _ ⟨ +-cong ⟩ refl ⟩
  0# + a        ≈⟨ +-identityˡ _ ⟩
  a             ∎

lemma₇ : ∀ x → - 1# * x ≈ - x
lemma₇ x = begin
  - 1# * x      ≈⟨ -‿*-distribˡ _ _ ⟩
  - (1# * x)    ≈⟨ -‿cong (*-identityˡ _) ⟩
  - x           ∎


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

module Data.Binary.Tests.Helpers where

open import Data.List as List using (List; _∷_; [])
open import Data.Product
open import Data.Nat as Nat using (ℕ; suc; zero)
open import Data.Binary.Definitions
open import Data.Binary.Operations.Semantics
open import Relation.Binary.PropositionalEquality

_≡⌈_⌉≡_ : (𝔹 → 𝔹) → ℕ → (ℕ → ℕ) → Set
fᵇ ≡⌈ n ⌉≡ fⁿ = let xs = List.upTo n in List.map (λ x → ⟦ fᵇ ⟦ x ⇑⟧ ⇓⟧ ) xs ≡ List.map fⁿ xs

prod : ∀ {a b} {A : Set a} {B : Set b} → List A → List B → List (A × B)
prod [] ys = []
prod (x ∷ xs) ys = List.foldr (λ y ys → (x , y) ∷ ys) (prod xs ys) ys

_≡⌈_⌉₂≡_ : (𝔹 → 𝔹 → 𝔹) → ℕ → (ℕ → ℕ → ℕ) → Set
fᵇ ≡⌈ n ⌉₂≡ fⁿ = List.map (λ { (x , y) → ⟦ fᵇ ⟦ x ⇑⟧ ⟦ y ⇑⟧ ⇓⟧ }) ys ≡ List.map (uncurry fⁿ) ys
  where
  xs : List ℕ
  xs = List.upTo n
  ys = prod xs xs

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
module Data.Tuple.Equivalence where

import      Lvl
open import Data using (Unit ; <>)
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Logic.Propositional
open import Structure.Setoid
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Type

private variable ℓₒ ℓₒ₁ ℓₒ₂ ℓₒ₃ ℓₒ₄ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₑ₄ : Lvl.Level

module _ {A : Type{ℓₒ₁}} ⦃ _ : Equiv{ℓₑ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₑ₂}(B) ⦄ where
  instance
    Tuple-equiv : Equiv(A ⨯ B)
    _≡_ ⦃ Tuple-equiv ⦄ (x₁ , y₁) (x₂ , y₂) = (x₁ ≡ x₂) ∧ (y₁ ≡ y₂)
    Equiv-equivalence ⦃ Tuple-equiv ⦄ = intro where
      instance
        [≡]-reflexivity : Reflexivity(_≡_ ⦃ Tuple-equiv ⦄)
        Reflexivity.proof([≡]-reflexivity) = [∧]-intro (reflexivity(_≡_)) (reflexivity(_≡_))

      instance
        [≡]-symmetry : Symmetry(_≡_ ⦃ Tuple-equiv ⦄)
        Symmetry.proof([≡]-symmetry) ([∧]-intro l r) = [∧]-intro (symmetry(_≡_) l) (symmetry(_≡_) r)

      instance
        [≡]-transitivity : Transitivity(_≡_ ⦃ Tuple-equiv ⦄)
        Transitivity.proof([≡]-transitivity) ([∧]-intro l1 r1) ([∧]-intro l2 r2) = [∧]-intro (transitivity(_≡_) l1 l2) (transitivity(_≡_) r1 r2)

  instance
    left-function : Function(Tuple.left)
    Function.congruence left-function = Tuple.left

  instance
    right-function : Function(Tuple.right)
    Function.congruence right-function = Tuple.right

  instance
    [,]-function : BinaryOperator(_,_)
    BinaryOperator.congruence [,]-function a b = (a , b)

module _ {A : Type{ℓₒ₁}} ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ where
  instance
    swap-function : Function ⦃ Tuple-equiv ⦃ equiv-A ⦄ ⦃ equiv-B ⦄ ⦄ ⦃ Tuple-equiv ⦄ (Tuple.swap)
    Function.congruence swap-function = Tuple.swap

module _ {A : Type{ℓₒ}} ⦃ equiv : Equiv{ℓₑ}(A) ⦄ where
  instance
    repeat-function : Function(Tuple.repeat{A = A})
    Function.congruence repeat-function = Tuple.repeat

module _
  {A₁ : Type{ℓₒ₁}} ⦃ equiv-A₁ : Equiv{ℓₑ₁}(A₁) ⦄
  {A₂ : Type{ℓₒ₂}} ⦃ equiv-A₂ : Equiv{ℓₑ₂}(A₂) ⦄
  {B₁ : Type{ℓₒ₃}} ⦃ equiv-B₁ : Equiv{ℓₑ₃}(B₁) ⦄
  {B₂ : Type{ℓₒ₄}} ⦃ equiv-B₂ : Equiv{ℓₑ₄}(B₂) ⦄
  {f : A₁ → A₂} ⦃ func-f : Function(f) ⦄
  {g : B₁ → B₂} ⦃ func-g : Function(g) ⦄
  where

  instance
    map-function : Function(Tuple.map f g)
    Function.congruence map-function = Tuple.map (congruence₁(f)) (congruence₁(g))

module _
  {A : Type{ℓₒ₁}} ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  {B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {C : Type{ℓₒ₃}} ⦃ equiv-C : Equiv{ℓₑ₃}(C) ⦄
  where

  instance
    associateLeft-function : Function(Tuple.associateLeft {A = A}{B = B}{C = C})
    Function.congruence associateLeft-function = Tuple.associateLeft

  instance
    associateRight-function : Function(Tuple.associateRight {A = A}{B = B}{C = C})
    Function.congruence associateRight-function = Tuple.associateRight

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.Groups.CP2 where

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv

open import Cubical.Relation.Nullary

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Unit
open import Cubical.Data.Nat renaming (_+_ to _+ℕ_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Int
open import Cubical.Data.Sigma

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Unit

open import Cubical.HITs.Pushout
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.Join
open import Cubical.HITs.SetTruncation as ST
open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.Truncation

open import Cubical.Homotopy.Hopf

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Groups.Connected
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.MayerVietorisUnreduced
open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Sn
open import Cubical.ZCohomology.RingStructure.CupProduct

open S¹Hopf
open IsGroupHom
open Iso

CP² : Type
CP² = Pushout {A = TotalHopf} fst λ _ → tt

characFunSpaceCP² : ∀ {ℓ} {A : Type ℓ}
  → Iso (CP² → A) (Σ[ x ∈ A ] Σ[ f ∈ (S₊ (suc (suc zero)) → A) ]
         ((y : TotalHopf) → f (fst y) ≡ x))
fun characFunSpaceCP² f = (f (inr tt)) , ((f ∘ inl ) , (λ a → cong f (push a)))
inv characFunSpaceCP² (a , f , p) (inl x) = f x
inv characFunSpaceCP² (a , f , p) (inr x) = a
inv characFunSpaceCP² (a , f , p) (push b i) = p b i
rightInv characFunSpaceCP² _ = refl
leftInv characFunSpaceCP² _ =
  funExt λ { (inl x) → refl
           ; (inr x) → refl
           ; (push a i) → refl}

H⁰CP²≅ℤ : GroupIso (coHomGr 0 CP²) ℤGroup
H⁰CP²≅ℤ =
  H⁰-connected (inr tt)
    (PushoutToProp (λ _ → squash₁)
      (sphereElim _ (λ _ → isOfHLevelSuc 1 squash₁)
        ∣ sym (push (north , base)) ∣₁)
    λ _ → ∣ refl ∣₁)

module M = MV (S₊ 2) Unit TotalHopf fst (λ _ → tt)

H²CP²≅ℤ : GroupIso (coHomGr 2 CP²) ℤGroup
H²CP²≅ℤ = compGroupIso (BijectionIso→GroupIso bij)
            (compGroupIso (invGroupIso trivIso) (Hⁿ-Sⁿ≅ℤ 1))
  where
  isContrH¹TotalHopf : isContr (coHom 1 TotalHopf)
  isContrH¹TotalHopf =
    isOfHLevelRetractFromIso 0 (setTruncIso (domIso (invIso (IsoS³TotalHopf))))
      (isOfHLevelRetractFromIso 0 ((fst (H¹-Sⁿ≅0 1))) isContrUnit)

  isContrH²TotalHopf : isContr (coHom 2 TotalHopf)
  isContrH²TotalHopf =
    isOfHLevelRetractFromIso 0 (setTruncIso (domIso (invIso (IsoS³TotalHopf))))
      ((isOfHLevelRetractFromIso 0
        (fst (Hⁿ-Sᵐ≅0 1 2 λ p → snotz (sym (cong predℕ p)))) isContrUnit))

  trivIso : GroupIso (coHomGr 2 (Susp S¹)) (×coHomGr 2 (Susp S¹) Unit)
  fun (fst trivIso) x = x , 0ₕ _
  inv (fst trivIso) = fst
  rightInv (fst trivIso) (x , p) =
    ΣPathP (refl , isContr→isProp (isContrHⁿ-Unit 1) _ _)
  leftInv (fst trivIso) x = refl
  snd trivIso = makeIsGroupHom λ _ _ → refl

  bij : BijectionIso (coHomGr 2 CP²) (×coHomGr 2 (Susp S¹) Unit)
  BijectionIso.fun bij = M.i 2
  BijectionIso.inj bij x p =
    PT.rec (squash₂ _ _)
      (uncurry (λ z q
        → sym q
        ∙∙ cong (fst (M.d 1)) (isContr→isProp isContrH¹TotalHopf z (0ₕ _))
        ∙∙ (M.d 1) .snd .pres1))
      (M.Ker-i⊂Im-d 1 x p)
    where
    help : isInIm (M.d 1) x
    help = M.Ker-i⊂Im-d 1 x p
  BijectionIso.surj bij y =
    M.Ker-Δ⊂Im-i 2 y (isContr→isProp isContrH²TotalHopf _ _)

H⁴CP²≅ℤ : GroupIso (coHomGr 4 CP²) ℤGroup
H⁴CP²≅ℤ = compGroupIso (invGroupIso (BijectionIso→GroupIso bij))
          (compGroupIso help (Hⁿ-Sⁿ≅ℤ 2))
  where
  help : GroupIso (coHomGr 3 TotalHopf) (coHomGr 3 (S₊ 3))
  help = isoType→isoCohom 3 (invIso IsoS³TotalHopf)

  bij : BijectionIso (coHomGr 3 TotalHopf) (coHomGr 4 CP²)
  BijectionIso.fun bij = M.d 3
  BijectionIso.inj bij x p =
    PT.rec (squash₂ _ _)
         (uncurry (λ z q →
             sym q
          ∙∙ cong (M.Δ 3 .fst)
                (isOfHLevelΣ 1 (isContr→isProp
                  (isOfHLevelRetractFromIso 0
                    (fst (Hⁿ-Sᵐ≅0 2 1 λ p → snotz (cong predℕ p))) isContrUnit))
                (λ _ → isContr→isProp (isContrHⁿ-Unit 2))
                z (0ₕ _ , 0ₕ _))
          ∙∙ M.Δ 3 .snd .pres1))
         (M.Ker-d⊂Im-Δ _ x p)
  BijectionIso.surj bij y =
    M.Ker-i⊂Im-d 3 y (isOfHLevelΣ 1
      (isContr→isProp (isOfHLevelRetractFromIso 0
        (fst (Hⁿ-Sᵐ≅0 3 1 λ p → snotz (cong predℕ p))) isContrUnit))
        (λ _ → isContr→isProp (isContrHⁿ-Unit _)) _ _)

-- Characterisations of the trivial groups

private
    elim-TotalHopf : (B : TotalHopf → Type)
      → ((x : _) → isOfHLevel 3 (B x)) → B (north , base)
      → (x : _) → B x
    elim-TotalHopf =
      transport (λ i → (B : isoToPath IsoS³TotalHopf i → Type)
        → ((x : _) → isOfHLevel 3 (B x))
          → B (transp (λ j → isoToPath IsoS³TotalHopf (i ∨ ~ j)) i (north , base)) → (x : _) → B x)
          λ B hLev elim-TotalHopf → sphereElim _ (λ _ → hLev _) elim-TotalHopf

H¹-CP²≅0 : GroupIso (coHomGr 1 CP²) UnitGroup₀
H¹-CP²≅0 =
  contrGroupIsoUnit
    (isOfHLevelRetractFromIso 0 (setTruncIso characFunSpaceCP²)
    (isOfHLevelRetractFromIso 0 lem₂ lem₃))
  where
  lem₁ : (f : (Susp S¹ → coHomK 1)) → ∥ (λ _ → 0ₖ _) ≡ f ∥₁
  lem₁ f = PT.map (λ p → p)
                (Iso.fun PathIdTrunc₀Iso (isOfHLevelRetractFromIso 1
                  (fst (Hⁿ-Sᵐ≅0 0 1 (λ p → snotz (sym p)))) isPropUnit (0ₕ _) ∣ f ∣₂))

  lem₂ : Iso ∥ (Σ[ x ∈ coHomK 1 ] ( Σ[ f ∈ (Susp S¹ → coHomK 1) ] ((y : TotalHopf) → f (fst y) ≡ x))) ∥₂
             ∥ (Σ[ f ∈ (Susp S¹ → coHomK 1) ] ((y : TotalHopf) → f (fst y) ≡ 0ₖ 1)) ∥₂
  fun lem₂ = ST.map (uncurry λ x → uncurry λ f p → (λ y → (-ₖ x) +ₖ f y) , λ y → cong ((-ₖ x) +ₖ_) (p y) ∙ lCancelₖ _ x)
  inv lem₂ = ST.map λ p → 0ₖ _ , p
  rightInv lem₂ =
    ST.elim (λ _ → isOfHLevelPath 2 squash₂ _ _)
          λ {(f , p) → cong ∣_∣₂ (ΣPathP ((funExt (λ x → lUnitₖ _ (f x)))
          , (funExt (λ y → sym (rUnit (λ i → (-ₖ 0ₖ 1) +ₖ p y i)))
           ◁ λ j y i → lUnitₖ _ (p y i) j)))}
  leftInv lem₂ =
    ST.elim (λ _ → isOfHLevelPath 2 squash₂ _ _)
      (uncurry (coHomK-elim _ (λ _ → isPropΠ (λ _ → squash₂ _ _))
       (uncurry λ f p → cong ∣_∣₂ (ΣPathP (refl , (ΣPathP ((funExt (λ x → lUnitₖ _ (f x)))
       , ((funExt (λ y → sym (rUnit (λ i → (-ₖ 0ₖ 1) +ₖ p y i)))
         ◁ λ j y i → lUnitₖ _ (p y i) j)))))))))

  lem₃ : isContr _
  fst lem₃ = ∣ (λ _ → 0ₖ 1) , (λ _ → refl) ∣₂
  snd lem₃ =
    ST.elim (λ _ → isOfHLevelPath 2 squash₂ _ _)
      (uncurry λ f → PT.rec (isPropΠ (λ _ → squash₂ _ _))
      (J (λ f _ → (y : (y₁ : TotalHopf) → f (fst y₁) ≡ 0ₖ 1) →
      ∣ (λ _ → 0ₖ 1) , (λ _ _ → 0ₖ 1) ∣₂ ≡ ∣ f , y ∣₂)
      (λ y → cong ∣_∣₂ (ΣPathP ((funExt (λ z → sym (y (north , base)))) , toPathP (s y)))))
      (lem₁ f))

    where
    s : (y : TotalHopf → 0ₖ 1 ≡ 0ₖ 1)
     → transport (λ i → (_ : TotalHopf) → y (north , base) (~ i) ≡ ∣ base ∣)
                  (λ _ _ → 0ₖ 1) ≡ y
    s y = funExt (elim-TotalHopf _ (λ _ → isOfHLevelPath 3 (isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _) _ _)
                 λ k → transp (λ i → y (north , base) (~ i ∧ ~ k) ≡ ∣ base ∣) k
                                λ j → y (north , base) (~ k ∨ j))

Hⁿ-CP²≅0-higher : (n : ℕ) → ¬ (n ≡ 1) → GroupIso (coHomGr (3 +ℕ n) CP²) UnitGroup₀
Hⁿ-CP²≅0-higher n p = contrGroupIsoUnit ((0ₕ _) , (λ x → sym (main x)))
  where
  h : GroupHom (coHomGr (2 +ℕ n) TotalHopf) (coHomGr (3 +ℕ n) CP²)
  h = M.d (2 +ℕ n)

  propᵣ : isProp (fst (×coHomGr (3 +ℕ n) (Susp S¹) Unit))
  propᵣ =
    isPropΣ
      (isOfHLevelRetractFromIso 1
         (fst (Hⁿ-Sᵐ≅0 (2 +ℕ n) 1 λ p → ⊥.rec (snotz (cong predℕ p)))) isPropUnit)
      λ _ → isContr→isProp (isContrHⁿ-Unit _)

  propₗ : isProp (coHom (2 +ℕ n) TotalHopf)
  propₗ = subst (λ x → isProp (coHom (2 +ℕ n) x)) (isoToPath IsoS³TotalHopf)
               (isOfHLevelRetractFromIso 1
                 (fst (Hⁿ-Sᵐ≅0 (suc n) 2 λ q → p (cong predℕ q))) isPropUnit)

  inIm : (x : coHom (3 +ℕ n) CP²) → isInIm h x
  inIm x = M.Ker-i⊂Im-d (2 +ℕ n) x (propᵣ _ _)

  main : (x : coHom (3 +ℕ n) CP²) → x ≡ 0ₕ _
  main x =
    PT.rec (squash₂ _ _)
      (uncurry (λ f p → sym p ∙∙ cong (h .fst) (propₗ f (0ₕ _)) ∙∙ pres1 (snd h)))
      (inIm x)

-- All trivial groups:
Hⁿ-CP²≅0 : (n : ℕ) → ¬ suc n ≡ 2 → ¬ suc n ≡ 4
       → GroupIso (coHomGr (suc n) CP²) UnitGroup₀
Hⁿ-CP²≅0 zero p q = H¹-CP²≅0
Hⁿ-CP²≅0 (suc zero) p q = ⊥.rec (p refl)
Hⁿ-CP²≅0 (suc (suc zero)) p q = Hⁿ-CP²≅0-higher 0 λ p → snotz (sym p)
Hⁿ-CP²≅0 (suc (suc (suc zero))) p q = ⊥.rec (q refl)
Hⁿ-CP²≅0 (suc (suc (suc (suc n)))) p q =
  Hⁿ-CP²≅0-higher (suc (suc n))
    λ p → snotz (cong predℕ p)

-- Another Brunerie number
ℤ→HⁿCP²→ℤ : ℤ → ℤ
ℤ→HⁿCP²→ℤ x =
  Iso.fun (fst H⁴CP²≅ℤ)
    (Iso.inv (fst H²CP²≅ℤ) x ⌣ Iso.inv (fst H²CP²≅ℤ) x)

brunerie2 : ℤ
brunerie2 = ℤ→HⁿCP²→ℤ 1

{-
|brunerie2|≡1 : abs (ℤ→HⁿCP²→ℤ 1) ≡ 1
|brunerie2|≡1 = refl
-}

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax FOL

type
  * : 0-ary
  N : 0-ary

term
  false : * | ⊥
  or    : *  *  ->  * | _∨_ l20
  true  : * | ⊤
  and   : *  *  ->  * | _∧_ l20
  not   : *  ->  * | ¬_ r50
  eq    : N  N  ->  * | _≟_ l20
  all   : N.*  ->  * | ∀′
  ex    : N.*  ->  * | ∃′

theory
  (⊥U∨ᴸ) a |> or (false, a) = a
  (⊥U∨ᴿ) a |> or (a, false) = a
  (∨A) a b c |> or (or(a, b), c) = or (a, or(b, c))
  (∨C) a b |> or(a, b) = or(b, a)
  (⊤U∧ᴸ) a |> and (true, a) = a
  (⊤U∧ᴿ) a |> and (a, true) = a
  (∧A) a b c |> and (and(a, b), c) = and (a, and(b, c))
  (∧D∨ᴸ) a b c |> and (a, or (b, c)) = or (and(a, b), and(a, c))
  (∧D∨ᴿ) a b c |> and (or (a, b), c) = or (and(a, c), and(b, c))
  (⊥X∧ᴸ) a |> and (false, a) = false
  (⊥X∧ᴿ) a |> and (a, false) = false
  (¬N∨ᴸ) a |> or (not (a), a) = false
  (¬N∨ᴿ) a |> or (a, not (a)) = false
  (∧C) a b |> and(a, b) = and(b, a)
  (∨I) a |> or(a, a) = a
  (∧I) a |> and(a, a) = a
  (¬²) a |> not(not (a)) = a
  (∨D∧ᴸ) a b c |> or (a, and (b, c)) = and (or(a, b), or(a, c))
  (∨D∧ᴿ) a b c |> or (and (a, b), c) = and (or(a, c), or(b, c))
  (∨B∧ᴸ) a b |> or (and (a, b), a) = a
  (∨B∧ᴿ) a b |> or (a, and (a, b)) = a
  (∧B∨ᴸ) a b |> and (or (a, b), a) = a
  (∧B∨ᴿ) a b |> and (a, or (a, b)) = a
  (⊤X∨ᴸ) a |> or (true, a) = true
  (⊤X∨ᴿ) a |> or (a, true) = true
  (¬N∧ᴸ) a |> and (not (a), a) = false
  (¬N∧ᴿ) a |> and (a, not (a)) = false
  (DM∧) a b |> not (and (a, b)) = or (not(a), not(b))
  (DM∨) a b |> not (or (a, b)) = and (not(a), not(b))
  (DM∀) p : N.* |> not (all (x. p[x])) = ex  (x. not(p[x]))
  (DM∃) p : N.* |> not (ex  (x. p[x])) = all (x. not(p[x]))
  (∀D∧) p q : N.* |> all (x. and(p[x], q[x])) = and (all(x.p[x]), all(x.q[x]))
  (∃D∨) p q : N.* |> ex (x. or(p[x], q[x])) = or (ex(x.p[x]), ex(x.q[x]))
  (∧P∀ᴸ) p : *  q : N.* |> and (p, all(x.q[x])) = all (x. and(p, q[x]))
  (∧P∃ᴸ) p : *  q : N.* |> and (p, ex (x.q[x])) = ex  (x. and(p, q[x]))
  (∨P∀ᴸ) p : *  q : N.* |> or  (p, all(x.q[x])) = all (x. or (p, q[x]))
  (∨P∃ᴸ) p : *  q : N.* |> or  (p, ex (x.q[x])) = ex  (x. or (p, q[x]))
  (∧P∀ᴿ) p : N.*  q : * |> and (all(x.p[x]), q) = all (x. and(p[x], q))
  (∧P∃ᴿ) p : N.*  q : * |> and (ex (x.p[x]), q) = ex  (x. and(p[x], q))
  (∨P∀ᴿ) p : N.*  q : * |> or  (all(x.p[x]), q) = all (x. or (p[x], q))
  (∨P∃ᴿ) p : N.*  q : * |> or  (ex (x.p[x]), q) = ex  (x. or (p[x], q))
  (∀Eᴸ) p : N.*  n : N |> all (x.p[x]) = and (p[n], all(x.p[x]))
  (∃Eᴸ) p : N.*  n : N |> ex  (x.p[x]) = or  (p[n], ex (x.p[x]))
  (∀Eᴿ) p : N.*  n : N |> all (x.p[x]) = and (all(x.p[x]), p[n])
  (∃Eᴿ) p : N.*  n : N |> ex  (x.p[x]) = or  (ex (x.p[x]), p[n])
  (∃⟹) p : N.*  q : * |> imp (ex (x.p[x]), q) = all (x. imp(p[x], q))
  (∀⟹) p : N.*  q : * |> imp (all(x.p[x]), q) = ex  (x. imp(p[x], q))
-}

module FOL.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import FOL.Signature
open import FOL.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution FOL:Syn
open import SOAS.Metatheory.SecondOrder.Equality FOL:Syn

private
  variable
    α β γ τ : FOLT
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ FOL) α Γ → (𝔐 ▷ FOL) α Γ → Set where
  ⊥U∨ᴸ : ⁅ * ⁆̣               ▹ ∅ ⊢                  ⊥ ∨ 𝔞 ≋ₐ 𝔞
  ∨A   : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣   ▹ ∅ ⊢            (𝔞 ∨ 𝔟) ∨ 𝔠 ≋ₐ 𝔞 ∨ (𝔟 ∨ 𝔠)
  ∨C   : ⁅ * ⁆ ⁅ * ⁆̣         ▹ ∅ ⊢                  𝔞 ∨ 𝔟 ≋ₐ 𝔟 ∨ 𝔞
  ⊤U∧ᴸ : ⁅ * ⁆̣               ▹ ∅ ⊢                  ⊤ ∧ 𝔞 ≋ₐ 𝔞
  ∧A   : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣   ▹ ∅ ⊢            (𝔞 ∧ 𝔟) ∧ 𝔠 ≋ₐ 𝔞 ∧ (𝔟 ∧ 𝔠)
  ∧D∨ᴸ : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣   ▹ ∅ ⊢            𝔞 ∧ (𝔟 ∨ 𝔠) ≋ₐ (𝔞 ∧ 𝔟) ∨ (𝔞 ∧ 𝔠)
  ⊥X∧ᴸ : ⁅ * ⁆̣               ▹ ∅ ⊢                  ⊥ ∧ 𝔞 ≋ₐ ⊥
  ¬N∨ᴸ : ⁅ * ⁆̣               ▹ ∅ ⊢              (¬ 𝔞) ∨ 𝔞 ≋ₐ ⊥
  ∧C   : ⁅ * ⁆ ⁅ * ⁆̣         ▹ ∅ ⊢                  𝔞 ∧ 𝔟 ≋ₐ 𝔟 ∧ 𝔞
  ∨I   : ⁅ * ⁆̣               ▹ ∅ ⊢                  𝔞 ∨ 𝔞 ≋ₐ 𝔞
  ∧I   : ⁅ * ⁆̣               ▹ ∅ ⊢                  𝔞 ∧ 𝔞 ≋ₐ 𝔞
  ¬²   : ⁅ * ⁆̣               ▹ ∅ ⊢                ¬ (¬ 𝔞) ≋ₐ 𝔞
  ∨D∧ᴸ : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣   ▹ ∅ ⊢            𝔞 ∨ (𝔟 ∧ 𝔠) ≋ₐ (𝔞 ∨ 𝔟) ∧ (𝔞 ∨ 𝔠)
  ∨B∧ᴸ : ⁅ * ⁆ ⁅ * ⁆̣         ▹ ∅ ⊢            (𝔞 ∧ 𝔟) ∨ 𝔞 ≋ₐ 𝔞
  ∧B∨ᴸ : ⁅ * ⁆ ⁅ * ⁆̣         ▹ ∅ ⊢            (𝔞 ∨ 𝔟) ∧ 𝔞 ≋ₐ 𝔞
  ⊤X∨ᴸ : ⁅ * ⁆̣               ▹ ∅ ⊢                  ⊤ ∨ 𝔞 ≋ₐ ⊤
  ¬N∧ᴸ : ⁅ * ⁆̣               ▹ ∅ ⊢              (¬ 𝔞) ∧ 𝔞 ≋ₐ ⊥
  DM∧  : ⁅ * ⁆ ⁅ * ⁆̣         ▹ ∅ ⊢              ¬ (𝔞 ∧ 𝔟) ≋ₐ (¬ 𝔞) ∨ (¬ 𝔟)
  DM∨  : ⁅ * ⁆ ⁅ * ⁆̣         ▹ ∅ ⊢              ¬ (𝔞 ∨ 𝔟) ≋ₐ (¬ 𝔞) ∧ (¬ 𝔟)
  DM∀  : ⁅ N ⊩ * ⁆̣           ▹ ∅ ⊢       ¬ (∀′ (𝔞⟨ x₀ ⟩)) ≋ₐ ∃′ (¬ 𝔞⟨ x₀ ⟩)
  DM∃  : ⁅ N ⊩ * ⁆̣           ▹ ∅ ⊢       ¬ (∃′ (𝔞⟨ x₀ ⟩)) ≋ₐ ∀′ (¬ 𝔞⟨ x₀ ⟩)
  ∀D∧  : ⁅ N ⊩ * ⁆ ⁅ N ⊩ * ⁆̣ ▹ ∅ ⊢ ∀′ (𝔞⟨ x₀ ⟩ ∧ 𝔟⟨ x₀ ⟩) ≋ₐ (∀′ (𝔞⟨ x₀ ⟩)) ∧ (∀′ (𝔟⟨ x₀ ⟩))
  ∃D∨  : ⁅ N ⊩ * ⁆ ⁅ N ⊩ * ⁆̣ ▹ ∅ ⊢ ∃′ (𝔞⟨ x₀ ⟩ ∨ 𝔟⟨ x₀ ⟩) ≋ₐ (∃′ (𝔞⟨ x₀ ⟩)) ∨ (∃′ (𝔟⟨ x₀ ⟩))
  ∧P∀ᴸ : ⁅ * ⁆ ⁅ N ⊩ * ⁆̣     ▹ ∅ ⊢     𝔞 ∧ (∀′ (𝔟⟨ x₀ ⟩)) ≋ₐ ∀′ (𝔞 ∧ 𝔟⟨ x₀ ⟩)
  ∧P∃ᴸ : ⁅ * ⁆ ⁅ N ⊩ * ⁆̣     ▹ ∅ ⊢     𝔞 ∧ (∃′ (𝔟⟨ x₀ ⟩)) ≋ₐ ∃′ (𝔞 ∧ 𝔟⟨ x₀ ⟩)
  ∨P∀ᴸ : ⁅ * ⁆ ⁅ N ⊩ * ⁆̣     ▹ ∅ ⊢     𝔞 ∨ (∀′ (𝔟⟨ x₀ ⟩)) ≋ₐ ∀′ (𝔞 ∨ 𝔟⟨ x₀ ⟩)
  ∨P∃ᴸ : ⁅ * ⁆ ⁅ N ⊩ * ⁆̣     ▹ ∅ ⊢     𝔞 ∨ (∃′ (𝔟⟨ x₀ ⟩)) ≋ₐ ∃′ (𝔞 ∨ 𝔟⟨ x₀ ⟩)
  ∀Eᴸ  : ⁅ N ⊩ * ⁆ ⁅ N ⁆̣     ▹ ∅ ⊢           ∀′ (𝔞⟨ x₀ ⟩) ≋ₐ 𝔞⟨ 𝔟 ⟩ ∧ (∀′ (𝔞⟨ x₀ ⟩))
  ∃Eᴸ  : ⁅ N ⊩ * ⁆ ⁅ N ⁆̣     ▹ ∅ ⊢           ∃′ (𝔞⟨ x₀ ⟩) ≋ₐ 𝔞⟨ 𝔟 ⟩ ∨ (∃′ (𝔞⟨ x₀ ⟩))

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

-- Derived equations
⊥U∨ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∨ ⊥ ≋ 𝔞
⊥U∨ᴿ = tr (ax ∨C with《 𝔞 ◃ ⊥ 》) (ax ⊥U∨ᴸ with《 𝔞 》)
⊤U∧ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∧ ⊤ ≋ 𝔞
⊤U∧ᴿ = tr (ax ∧C with《 𝔞 ◃ ⊤ 》) (ax ⊤U∧ᴸ with《 𝔞 》)
∧D∨ᴿ : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (𝔞 ∨ 𝔟) ∧ 𝔠 ≋ (𝔞 ∧ 𝔠) ∨ (𝔟 ∧ 𝔠)
∧D∨ᴿ = begin
  (𝔞 ∨ 𝔟) ∧ 𝔠       ≋⟨ ax ∧C with《 𝔞 ∨ 𝔟 ◃ 𝔠 》 ⟩
  𝔠 ∧ (𝔞 ∨ 𝔟)       ≋⟨ ax ∧D∨ᴸ with《 𝔠 ◃ 𝔞 ◃ 𝔟 》 ⟩
  (𝔠 ∧ 𝔞) ∨ (𝔠 ∧ 𝔟)  ≋⟨ cong₂[ ax ∧C with《 𝔠 ◃ 𝔞 》 ][ ax ∧C with《 𝔠 ◃ 𝔟 》 ]inside ◌ᵈ ∨ ◌ᵉ ⟩
  (𝔞 ∧ 𝔠) ∨ (𝔟 ∧ 𝔠)  ∎
⊥X∧ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∧ ⊥ ≋ ⊥
⊥X∧ᴿ = tr (ax ∧C with《 𝔞 ◃ ⊥ 》) (ax ⊥X∧ᴸ with《 𝔞 》)
¬N∨ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∨ (¬ 𝔞) ≋ ⊥
¬N∨ᴿ = tr (ax ∨C with《 𝔞 ◃ (¬ 𝔞) 》) (ax ¬N∨ᴸ with《 𝔞 》)
∨D∧ᴿ : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (𝔞 ∧ 𝔟) ∨ 𝔠 ≋ (𝔞 ∨ 𝔠) ∧ (𝔟 ∨ 𝔠)
∨D∧ᴿ = begin
  (𝔞 ∧ 𝔟) ∨ 𝔠       ≋⟨ ax ∨C with《 𝔞 ∧ 𝔟 ◃ 𝔠 》 ⟩
  𝔠 ∨ (𝔞 ∧ 𝔟)       ≋⟨ ax ∨D∧ᴸ with《 𝔠 ◃ 𝔞 ◃ 𝔟 》 ⟩
  (𝔠 ∨ 𝔞) ∧ (𝔠 ∨ 𝔟)  ≋⟨ cong₂[ ax ∨C with《 𝔠 ◃ 𝔞 》 ][ ax ∨C with《 𝔠 ◃ 𝔟 》 ]inside ◌ᵈ ∧ ◌ᵉ ⟩
  (𝔞 ∨ 𝔠) ∧ (𝔟 ∨ 𝔠)  ∎
⊤X∨ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∨ ⊤ ≋ ⊤
⊤X∨ᴿ = tr (ax ∨C with《 𝔞 ◃ ⊤ 》) (ax ⊤X∨ᴸ with《 𝔞 》)
¬N∧ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∧ (¬ 𝔞) ≋ ⊥
¬N∧ᴿ = tr (ax ∧C with《 𝔞 ◃ (¬ 𝔞) 》) (ax ¬N∧ᴸ with《 𝔞 》)
∧P∀ᴿ : ⁅ N ⊩ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (∀′ (𝔞⟨ x₀ ⟩)) ∧ 𝔟 ≋ ∀′ (𝔞⟨ x₀ ⟩ ∧ 𝔟)
∧P∀ᴿ = begin
  (∀′ (𝔞⟨ x₀ ⟩)) ∧ 𝔟   ≋⟨ ax ∧C with《 ∀′ (𝔞⟨ x₀ ⟩) ◃ 𝔟 》 ⟩
  𝔟 ∧ (∀′ (𝔞⟨ x₀ ⟩))   ≋⟨ ax ∧P∀ᴸ with《 𝔟 ◃ 𝔞⟨ x₀ ⟩ 》 ⟩
  ∀′ (𝔟 ∧ 𝔞⟨ x₀ ⟩)     ≋⟨ cong[ ax ∧C with《 𝔟 ◃ 𝔞⟨ x₀ ⟩ 》 ]inside ∀′ (◌ᶜ⟨ x₀ ⟩) ⟩
  ∀′ (𝔞⟨ x₀ ⟩ ∧ 𝔟)     ∎
∧P∃ᴿ : ⁅ N ⊩ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (∃′ (𝔞⟨ x₀ ⟩)) ∧ 𝔟 ≋ ∃′ (𝔞⟨ x₀ ⟩ ∧ 𝔟)
∧P∃ᴿ = begin
  (∃′ (𝔞⟨ x₀ ⟩)) ∧ 𝔟   ≋⟨ ax ∧C with《 ∃′ (𝔞⟨ x₀ ⟩) ◃ 𝔟 》 ⟩
  𝔟 ∧ (∃′ (𝔞⟨ x₀ ⟩))   ≋⟨ ax ∧P∃ᴸ with《 𝔟 ◃ 𝔞⟨ x₀ ⟩ 》 ⟩
  ∃′ (𝔟 ∧ 𝔞⟨ x₀ ⟩)     ≋⟨ cong[ ax ∧C with《 𝔟 ◃ 𝔞⟨ x₀ ⟩ 》 ]inside ∃′ (◌ᶜ⟨ x₀ ⟩) ⟩
  ∃′ (𝔞⟨ x₀ ⟩ ∧ 𝔟)     ∎
∨P∀ᴿ : ⁅ N ⊩ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (∀′ (𝔞⟨ x₀ ⟩)) ∨ 𝔟 ≋ ∀′ (𝔞⟨ x₀ ⟩ ∨ 𝔟)
∨P∀ᴿ = begin
  (∀′ (𝔞⟨ x₀ ⟩)) ∨ 𝔟   ≋⟨ ax ∨C with《 ∀′ (𝔞⟨ x₀ ⟩) ◃ 𝔟 》 ⟩
  𝔟 ∨ (∀′ (𝔞⟨ x₀ ⟩))   ≋⟨ ax ∨P∀ᴸ with《 𝔟 ◃ 𝔞⟨ x₀ ⟩ 》 ⟩
  ∀′ (𝔟 ∨ 𝔞⟨ x₀ ⟩)     ≋⟨ cong[ ax ∨C with《 𝔟 ◃ 𝔞⟨ x₀ ⟩ 》 ]inside ∀′ (◌ᶜ⟨ x₀ ⟩) ⟩
  ∀′ (𝔞⟨ x₀ ⟩ ∨ 𝔟)     ∎
∨P∃ᴿ : ⁅ N ⊩ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (∃′ (𝔞⟨ x₀ ⟩)) ∨ 𝔟 ≋ ∃′ (𝔞⟨ x₀ ⟩ ∨ 𝔟)
∨P∃ᴿ = begin
  (∃′ (𝔞⟨ x₀ ⟩)) ∨ 𝔟   ≋⟨ ax ∨C with《 ∃′ (𝔞⟨ x₀ ⟩) ◃ 𝔟 》 ⟩
  𝔟 ∨ (∃′ (𝔞⟨ x₀ ⟩))   ≋⟨ ax ∨P∃ᴸ with《 𝔟 ◃ 𝔞⟨ x₀ ⟩ 》 ⟩
  ∃′ (𝔟 ∨ 𝔞⟨ x₀ ⟩)     ≋⟨ cong[ ax ∨C with《 𝔟 ◃ 𝔞⟨ x₀ ⟩ 》 ]inside ∃′ (◌ᶜ⟨ x₀ ⟩) ⟩
  ∃′ (𝔞⟨ x₀ ⟩ ∨ 𝔟)     ∎
∀Eᴿ : ⁅ N ⊩ * ⁆ ⁅ N ⁆̣ ▹ ∅ ⊢ ∀′ (𝔞⟨ x₀ ⟩) ≋ (∀′ (𝔞⟨ x₀ ⟩)) ∧ 𝔞⟨ 𝔟 ⟩
∀Eᴿ = tr (ax ∀Eᴸ with《 𝔞⟨ x₀ ⟩ ◃ 𝔟 》) (ax ∧C with《  𝔞⟨ 𝔟 ⟩ ◃ ∀′ (𝔞⟨ x₀ ⟩) 》)
∃Eᴿ : ⁅ N ⊩ * ⁆ ⁅ N ⁆̣ ▹ ∅ ⊢ ∃′ (𝔞⟨ x₀ ⟩) ≋ (∃′ (𝔞⟨ x₀ ⟩)) ∨ 𝔞⟨ 𝔟 ⟩
∃Eᴿ = tr (ax ∃Eᴸ with《 𝔞⟨ x₀ ⟩ ◃ 𝔟 》) (ax ∨C with《  𝔞⟨ 𝔟 ⟩ ◃ ∃′ (𝔞⟨ x₀ ⟩) 》)
∃⟹ : ⁅ N ⊩ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (∃′ (𝔞⟨ x₀ ⟩)) ⟹ 𝔟 ≋ ∀′ (𝔞⟨ x₀ ⟩ ⟹ 𝔟)
∃⟹ = begin
  (∃′ (𝔞⟨ x₀ ⟩)) ⟹ 𝔟    ≡⟨⟩
  (¬ (∃′ (𝔞⟨ x₀ ⟩))) ∨ 𝔟 ≋⟨ cong[ ax DM∃ with《 𝔞⟨ x₀ ⟩ 》 ]inside (◌ᶜ ∨ 𝔟) ⟩
  (∀′ (¬ (𝔞⟨ x₀ ⟩))) ∨ 𝔟 ≋⟨ thm ∨P∀ᴿ with《 ¬ 𝔞⟨ x₀ ⟩ ◃ 𝔟 》 ⟩
  ∀′ (¬ (𝔞⟨ x₀ ⟩) ∨ 𝔟)   ≡⟨⟩
  ∀′ (𝔞⟨ x₀ ⟩ ⟹ 𝔟)      ∎
∀⟹ : ⁅ N ⊩ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (∀′ (𝔞⟨ x₀ ⟩)) ⟹ 𝔟 ≋ ∃′ (𝔞⟨ x₀ ⟩ ⟹ 𝔟)
∀⟹ = begin
  (∀′ (𝔞⟨ x₀ ⟩)) ⟹ 𝔟    ≡⟨⟩
  (¬ (∀′ (𝔞⟨ x₀ ⟩))) ∨ 𝔟 ≋⟨ cong[ ax DM∀ with《 𝔞⟨ x₀ ⟩ 》 ]inside (◌ᶜ ∨ 𝔟) ⟩
  (∃′ (¬ (𝔞⟨ x₀ ⟩))) ∨ 𝔟 ≋⟨ thm ∨P∃ᴿ with《 ¬ 𝔞⟨ x₀ ⟩ ◃ 𝔟 》 ⟩
  ∃′ (¬ (𝔞⟨ x₀ ⟩) ∨ 𝔟)   ≡⟨⟩
  ∃′ (𝔞⟨ x₀ ⟩ ⟹ 𝔟)      ∎


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

module Categories.Category.Instance.Properties.Setoids where

open import Level
open import Data.Product using (Σ; proj₁; proj₂; _,_; Σ-syntax; _×_; -,_)
open import Function.Equality using (Π)
open import Relation.Binary using (Setoid; Preorder; Rel)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
open import Relation.Binary.Indexed.Heterogeneous using (_=[_]⇒_)
open import Relation.Binary.Construct.Closure.SymmetricTransitive as ST using (Plus⇔; minimal)
open Plus⇔

open import Categories.Category using (Category; _[_,_])
open import Categories.Functor
open import Categories.Category.Instance.Setoids
open import Categories.Category.Complete
open import Categories.Category.Cocomplete

import Categories.Category.Construction.Cocones as Coc
import Categories.Category.Construction.Cones as Co
import Relation.Binary.Reasoning.Setoid as RS

open Π using (_⟨$⟩_)

module _ {o ℓ e} c ℓ′ {J : Category o ℓ e} (F : Functor J (Setoids (o ⊔ c) (o ⊔ ℓ ⊔ c ⊔ ℓ′))) where
  private
    module J    = Category J
    open Functor F
    module F₀ j = Setoid (F₀ j)
    open F₀ using () renaming (_≈_ to _[_≈_])

  vertex-carrier : Set (o ⊔ c)
  vertex-carrier = Σ J.Obj F₀.Carrier

  coc : Rel vertex-carrier (o ⊔ ℓ ⊔ c ⊔ ℓ′)
  coc (X , x) (Y , y) = Σ[ f ∈ J [ X , Y ] ] Y [ (F₁ f ⟨$⟩ x) ≈ y ]

  coc-preorder : Preorder (o ⊔ c) (o ⊔ c) (o ⊔ ℓ ⊔ c ⊔ ℓ′)
  coc-preorder = record
    { Carrier    = vertex-carrier
    ; _≈_        = _≡_
    ; _∼_        = coc
    ; isPreorder = record
      { isEquivalence = ≡.isEquivalence
      ; reflexive     = λ { {j , _} ≡.refl → J.id , (identity (F₀.refl j)) }
      ; trans         = λ { {a , Sa} {b , Sb} {c , Sc} (f , eq₁) (g , eq₂) →
        let open RS (F₀ c)
        in g J.∘ f , (begin
        F₁ (g J.∘ f) ⟨$⟩ Sa    ≈⟨ homomorphism (F₀.refl a) ⟩
        F₁ g ⟨$⟩ (F₁ f ⟨$⟩ Sa) ≈⟨ Π.cong (F₁ g) eq₁ ⟩
        F₁ g ⟨$⟩ Sb            ≈⟨ eq₂ ⟩
        Sc                     ∎) }
      }
    }

Setoids-Cocomplete : (o ℓ e c ℓ′ : Level) → Cocomplete o ℓ e (Setoids (o ⊔ c) (o ⊔ ℓ ⊔ c ⊔ ℓ′))
Setoids-Cocomplete o ℓ e c ℓ′ {J} F = record
  { initial =
    record
    { ⊥        = record
      { N      = ⇛-Setoid
      ; coapex = record
        { ψ       = λ j → record
          { _⟨$⟩_ = j ,_
          ; cong  = λ i≈k → forth (-, identity i≈k)
          }
        ; commute = λ {X} X⇒Y x≈y → back (-, Π.cong (F₁ X⇒Y) (F₀.sym X x≈y))
        }
      }
    ; !        = λ {K} →
      let module K = Cocone K
      in record
      { arr     = record
        { _⟨$⟩_ = to-coapex K
        ; cong  = minimal (coc c ℓ′ F) K.N (to-coapex K) (coapex-cong K)
        }
      ; commute = λ {X} x≈y → Π.cong (Coapex.ψ (Cocone.coapex K) X) x≈y
      }
    ; !-unique = λ { {K} f {a , Sa} {b , Sb} eq →
      let module K = Cocone K
          module f = Cocone⇒ f
          open RS K.N
      in begin
        K.ψ a ⟨$⟩ Sa       ≈˘⟨ f.commute (F₀.refl a) ⟩
        f.arr ⟨$⟩ (a , Sa) ≈⟨ Π.cong f.arr eq ⟩
        f.arr ⟨$⟩ (b , Sb) ∎ }
    }
  }
  where open Functor F
        open Coc F
        module J    = Category J
        module F₀ j = Setoid (F₀ j)
        open F₀ using () renaming (_≈_ to _[_≈_])

        -- this is essentially a symmetric transitive closure of coc
        ⇛-Setoid : Setoid (o ⊔ c) (o ⊔ ℓ ⊔ c ⊔ ℓ′)
        ⇛-Setoid = ST.setoid (coc c ℓ′ F) (Preorder.refl (coc-preorder c ℓ′ F))

        to-coapex : ∀ K → vertex-carrier c ℓ′ F → Setoid.Carrier (Cocone.N K)
        to-coapex K (j , Sj) = K.ψ j ⟨$⟩ Sj
          where module K = Cocone K
        coapex-cong : ∀ K → coc c ℓ′ F =[ to-coapex K ]⇒ (Setoid._≈_ (Cocone.N K))
        coapex-cong K {X , x} {Y , y} (f , fx≈y) = begin
          K.ψ X ⟨$⟩ x            ≈˘⟨ K.commute f (F₀.refl X) ⟩
          K.ψ Y ⟨$⟩ (F₁ f ⟨$⟩ x) ≈⟨ Π.cong (K.ψ Y) fx≈y ⟩
          K.ψ Y ⟨$⟩ y            ∎
          where module K = Cocone K
                open RS K.N

Setoids-Complete : (o ℓ e c ℓ′ : Level) → Complete o ℓ e (Setoids (c ⊔ ℓ ⊔ o ⊔ ℓ′) (o ⊔ ℓ′))
Setoids-Complete o ℓ e c ℓ′ {J} F =
  record
  { terminal = record
    { ⊤        = record
      { N     = record
        { Carrier       = Σ (∀ j → F₀.Carrier j)
                            (λ S → ∀ {X Y} (f : J [ X , Y ]) → [ F₀ Y ] F₁ f ⟨$⟩ S X ≈ S Y)
        ; _≈_           = λ { (S₁ , _) (S₂ , _) → ∀ j → [ F₀ j ] S₁ j ≈ S₂ j }
        ; isEquivalence = record
          { refl  = λ j → F₀.refl j
          ; sym   = λ a≈b j → F₀.sym j (a≈b j)
          ; trans = λ a≈b b≈c j → F₀.trans j (a≈b j) (b≈c j)
          }
        }
      ;  apex = record
        { ψ = λ j → record
          { _⟨$⟩_ = λ { (S , _) → S j }
          ; cong  = λ eq → eq j
          }
        ; commute = λ { {X} {Y} X⇒Y {_ , eq} {y} f≈g → F₀.trans Y (eq X⇒Y) (f≈g Y) }
        }
      }
    ; !        = λ {K} →
      let module K = Cone K
      in record
      { arr     = record
        { _⟨$⟩_ = λ x → (λ j → K.ψ j ⟨$⟩ x) , λ f → K.commute f (Setoid.refl K.N)
        ; cong  = λ a≈b j → Π.cong (K.ψ j) a≈b
        }
      ; commute = λ x≈y → Π.cong (K.ψ _) x≈y
      }
    ; !-unique = λ {K} f x≈y j →
      let module K = Cone K
      in F₀.sym j (Cone⇒.commute f (Setoid.sym K.N x≈y))
    }
  }
  where open Functor F
        open Co F
        module J    = Category J
        module F₀ j = Setoid (F₀ j)
        [_]_≈_ = Setoid._≈_

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
open import Agda.Primitive

variable
  ℓ : Level
  A : Set ℓ
  P : A → Set ℓ
  f : (x : A) → P x

postulate
  R : (a : Level) → Set (lsuc a)
  r : (a : Level) → R a

  Id : (a : Level) (A : Set a) → A → A → Set a
  cong₂ : (a b c : Level) (A : Set a) (B : Set b) (C : Set c) (x y : A) (u v : B)
          (f : A → B → C) → Id c C (f x u) (f y v)

  foo   : (x y u v : A) (g : A → A) →
          let a = _ in
          Id a (Id _ _ _ _)
               (cong₂ _ _ _ _ _ _ x y u v (λ x → f (g x)))
               (cong₂ _ _ _ _ _ _ (g x) (g y) u v f)

max_forks_repo_name: shlevy/agda


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

module Oscar.Class.Reflexivity.Function where

module _
  {a}
  where

  instance

    𝓡eflexivityFunction : Reflexivity.class Function⟦ a ⟧
    𝓡eflexivityFunction .⋆ = ¡


text:
-- https://github.com/idris-lang/Idris-dev/blob/4e704011fb805fcb861cc9a1bd68a2e727cefdde/libs/contrib/Data/Nat/Fib.idr

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

-- agda-stdlib
open import Algebra

module Math.NumberTheory.Fibonacci.Generic
  {c e} (CM : CommutativeMonoid c e)
  (v0 v1 : CommutativeMonoid.Carrier CM)
  where

-- agda-stdlib
open import Data.Nat
open import Function
import Relation.Binary.PropositionalEquality as ≡
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

open CommutativeMonoid CM
  renaming
  ( Carrier to A
  )

open SetoidReasoning setoid

fibRec : ℕ → A
fibRec 0             = v0
fibRec 1             = v1
fibRec (suc (suc n)) = fibRec (suc n) ∙ fibRec n

fibAcc : ℕ → A → A → A
fibAcc 0       a b = a
fibAcc (suc n) a b = fibAcc n b (a ∙ b)

fib : ℕ → A
fib n = fibAcc n v0 v1

lemma : ∀ m n o p → (m ∙ n) ∙ (o ∙ p) ≈ (m ∙ o) ∙ (n ∙ p)
lemma m n o p = begin
  (m ∙ n) ∙ (o ∙ p) ≈⟨ assoc m n (o ∙ p)  ⟩
  m ∙ (n ∙ (o ∙ p)) ≈⟨ sym $ ∙-congˡ $ assoc n o p ⟩
  m ∙ ((n ∙ o) ∙ p) ≈⟨ ∙-congˡ $ ∙-congʳ $ comm n o ⟩
  m ∙ ((o ∙ n) ∙ p) ≈⟨ ∙-congˡ $ assoc o n p ⟩
  m ∙ (o ∙ (n ∙ p)) ≈⟨ sym $ assoc m o (n ∙ p) ⟩
  (m ∙ o) ∙ (n ∙ p) ∎

fibAcc-cong : ∀ {m n o p q r} →
  m ≡.≡ n → o ≈ p → q ≈ r → fibAcc m o q ≈ fibAcc n p r
fibAcc-cong {zero}  {.0}       {o} {p} {q} {r} ≡.refl o≈p q≈r = o≈p
fibAcc-cong {suc m} {.(suc m)} {o} {p} {q} {r} ≡.refl o≈p q≈r =
  fibAcc-cong {m = m} ≡.refl q≈r (∙-cong o≈p q≈r)

fibAdd : ∀ m n o p q → fibAcc m n o ∙ fibAcc m p q ≈ fibAcc m (n ∙ p) (o ∙ q)
fibAdd 0             n o p q = refl
fibAdd 1             n o p q = refl
fibAdd (suc (suc m)) n o p q = begin
  fibAcc (2 + m) n o ∙ fibAcc (2 + m) p q                         ≡⟨⟩
  fibAcc (1 + m) o (n ∙ o) ∙ fibAcc (1 + m) q (p ∙ q)             ≡⟨⟩
  fibAcc m (n ∙ o) (o ∙ (n ∙ o)) ∙ fibAcc m (p ∙ q) (q ∙ (p ∙ q)) ≈⟨ fibAdd m (n ∙ o) (o ∙ (n ∙ o)) (p ∙ q) (q ∙ (p ∙ q)) ⟩
  fibAcc m ((n ∙ o) ∙ (p ∙ q)) ((o ∙ (n ∙ o)) ∙ (q ∙ (p ∙ q)))    ≈⟨ fibAcc-cong {m = m} ≡.refl (lemma n o p q) (lemma o (n ∙ o) q (p ∙ q)) ⟩
  fibAcc m ((n ∙ p) ∙ (o ∙ q)) ((o ∙ q) ∙ ((n ∙ o) ∙ (p ∙ q)))    ≈⟨ fibAcc-cong {m = m} ≡.refl refl (∙-congˡ $ lemma n o p q) ⟩
  fibAcc m ((n ∙ p) ∙ (o ∙ q)) ((o ∙ q) ∙ ((n ∙ p) ∙ (o ∙ q)))    ≡⟨⟩
  fibAcc (1 + m) (o ∙ q) ((n ∙ p) ∙ (o ∙ q))                      ≡⟨⟩
  fibAcc (2 + m) (n ∙ p) (o ∙ q)                                  ∎

fibRec≈fib : ∀ n → fibRec n ≈ fib n
fibRec≈fib 0             = refl
fibRec≈fib 1             = refl
fibRec≈fib (suc (suc n)) = begin
  fibRec (2 + n)                         ≡⟨⟩
  fibRec (1 + n) ∙ fibRec n              ≈⟨ ∙-cong (fibRec≈fib (suc n)) (fibRec≈fib n) ⟩
  fib (1 + n) ∙ fib n                    ≡⟨⟩
  fibAcc (1 + n) v0 v1 ∙ fibAcc n v0 v1  ≡⟨⟩
  fibAcc n v1 (v0 ∙ v1) ∙ fibAcc n v0 v1 ≈⟨ fibAdd n v1 (v0 ∙ v1) v0 v1 ⟩
  fibAcc n (v1 ∙ v0) ((v0 ∙ v1) ∙ v1)    ≈⟨ fibAcc-cong {m = n} ≡.refl (comm v1 v0) (trans (∙-congʳ (comm v0 v1)) (assoc v1 v0 v1)) ⟩
  fibAcc n (v0 ∙ v1) (v1 ∙ (v0 ∙ v1))    ≡⟨⟩
  fib (2 + n)                            ∎

fib[2+n]≈fib[1+n]∙fib[n] : ∀ n → fib (suc (suc n)) ≈ fib (suc n) ∙ fib n
fib[2+n]≈fib[1+n]∙fib[n] n =
  trans (sym $ fibRec≈fib (suc (suc n)))
        (∙-cong (fibRec≈fib (suc n)) (fibRec≈fib n))

fib[1+n]∙fib[n]≈fib[2+n] : ∀ n → fib (suc n) ∙ fib n ≈ fib (suc (suc n))
fib[1+n]∙fib[n]≈fib[2+n] n = sym $ fib[2+n]≈fib[1+n]∙fib[n] n

fib[n]∙fib[1+n]≈fib[2+n] : ∀ n → fib n ∙ fib (suc n) ≈ fib (suc (suc n))
fib[n]∙fib[1+n]≈fib[2+n] n = trans (comm (fib n) (fib (suc n))) (fib[1+n]∙fib[n]≈fib[2+n] n)


text:
module Lib.Maybe where

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A -> Maybe A

{-# COMPILE GHC Maybe = data Maybe (Nothing | Just) #-}


text:
module Subst where

open import Prelude
open import Lambda

infix 100 _[_] _[_:=_] _↑
infixl 100 _↑_ _↑ˢ_ _↑ˣ_ _↓ˣ_
infixl 60 _-_

{-
_-_ : {τ : Type}(Γ : Ctx) -> Var Γ τ -> Ctx
ε     - ()
Γ , τ - vz   = Γ
Γ , τ - vs x = (Γ - x) , τ

wkˣ : {Γ : Ctx}{σ τ : Type}
      (x : Var Γ σ) -> Var (Γ - x) τ -> Var Γ τ
wkˣ vz     y      = vs y
wkˣ (vs x) vz     = vz
wkˣ (vs x) (vs y) = vs (wkˣ x y)

wk : {Γ : Ctx}{σ τ : Type}
     (x : Var Γ σ) -> Term (Γ - x) τ -> Term Γ τ
wk x (var y) = var (wkˣ x y)
wk x (s • t) = wk x s • wk x t
wk x (ƛ t)   = ƛ wk (vs x) t

_↑ : {Γ : Ctx}{σ τ : Type} -> Term Γ τ -> Term (Γ , σ) τ
t ↑ = wk vz t

_↑_ : {Γ : Ctx}{τ : Type} -> Term Γ τ -> (Δ : Ctx) -> Term (Γ ++ Δ) τ
t ↑ ε       = t
t ↑ (Δ , σ) = (t ↑ Δ) ↑

data Cmpˣ {Γ : Ctx}{τ : Type}(x : Var Γ τ) :
          {σ : Type} -> Var Γ σ -> Set where
  same : Cmpˣ x x
  diff : {σ : Type}(y : Var (Γ - x) σ) -> Cmpˣ x (wkˣ x y)

_≟_ : {Γ : Ctx}{σ τ : Type}(x : Var Γ σ)(y : Var Γ τ) -> Cmpˣ x y
vz   ≟ vz   = same
vz   ≟ vs y = diff y
vs x ≟ vz   = diff vz
vs x ≟ vs y with x ≟ y
vs x ≟ vs .x         | same   = same
vs x ≟ vs .(wkˣ x y) | diff y = diff (vs y)

_[_:=_] : {Γ : Ctx}{σ τ : Type} ->
         Term Γ σ -> (x : Var Γ τ) -> Term (Γ - x) τ ->
         Term (Γ - x) σ
var y   [ x := u ] with x ≟ y
var .x         [ x := u ] | same = u
var .(wkˣ x y) [ x := u ] | diff y = var y
(s • t) [ x := u ] = s [ x := u ] • t [ x := u ]
(ƛ t)   [ x := u ] = ƛ t [ vs x := u ↑ ]
-}

infix 30 _─⟶_
infixl 90 _/_

_─⟶_ : Ctx -> Ctx -> Set
Γ ─⟶ Δ = Terms Γ Δ

idS : forall {Γ} -> Γ ─⟶ Γ
idS = tabulate var

infixr 80 _∘ˢ_

[_] : forall {Γ σ  } -> Term Γ σ -> Γ ─⟶ Γ , σ
[ t ] = idS ◄ t

wkS : forall {Γ Δ τ} -> Γ ─⟶ Δ -> Γ , τ ─⟶ Δ
wkS ∅       = ∅
wkS (θ ◄ t) = wkS θ ◄ wk t

_↑ : forall {Γ Δ τ} -> (Γ ─⟶ Δ) -> Γ , τ ─⟶ Δ , τ
θ ↑ = wkS θ ◄ vz

_/_ : forall {Γ Δ τ} -> Term Δ τ -> Γ ─⟶ Δ -> Term Γ τ
vz      / (θ ◄ u) = u
wk t    / (θ ◄ u) = t / θ
(s • t) / θ       = s / θ • t / θ
(ƛ t)   / θ       = ƛ t / θ ↑

_∘ˢ_ : forall {Γ Δ Θ} -> Δ ─⟶ Θ -> Γ ─⟶ Δ -> Γ ─⟶ Θ
∅       ∘ˢ θ = ∅
(δ ◄ t) ∘ˢ θ = δ ∘ˢ θ ◄ t / θ

inj : forall {Γ Δ τ} Θ -> Term Γ τ -> Γ ─⟶ Δ ++ Θ -> Γ ─⟶ Δ , τ ++ Θ
inj ε       t θ       = θ ◄ t
inj (Θ , σ) t (θ ◄ u) = inj Θ t θ ◄ u

[_⟵_] : forall {Γ τ} Δ -> Term (Γ ++ Δ) τ -> Γ ++ Δ ─⟶ Γ , τ ++ Δ
[ Δ ⟵ t ] = inj Δ t idS

_↑_ : forall {Γ σ} -> Term Γ σ -> (Δ : Ctx) -> Term (Γ ++ Δ) σ
t ↑ ε       = t
t ↑ (Δ , τ) = wk (t ↑ Δ)

_↑ˢ_ : forall {Γ Δ} -> Terms Γ Δ -> (Θ : Ctx) -> Terms (Γ ++ Θ) Δ
∅        ↑ˢ Θ = ∅
(ts ◄ t) ↑ˢ Θ = ts ↑ˢ Θ ◄ t ↑ Θ

_↑ˣ_ : forall {Γ τ} -> Var Γ τ -> (Δ : Ctx) -> Var (Γ ++ Δ) τ
x ↑ˣ ε       = x
x ↑ˣ (Δ , σ) = vsuc (x ↑ˣ Δ)

lem-var-↑ˣ : forall {Γ τ}(x : Var Γ τ)(Δ : Ctx) ->
             var (x ↑ˣ Δ) ≡ var x ↑ Δ
lem-var-↑ˣ x ε       = refl
lem-var-↑ˣ x (Δ , σ) = cong wk (lem-var-↑ˣ x Δ)

{- Not true!
lem-•-↑ : forall {Γ σ τ}(t : Term Γ (σ ⟶ τ))(u : Term Γ σ) Δ ->
          (t ↑ Δ) • (u ↑ Δ) ≡ (t • u) ↑ Δ
lem-•-↑ t u ε       = refl
lem-•-↑ t u (Δ , δ) = {! !}

lem-•ˢ-↑ : forall {Γ Θ τ}(t : Term Γ (Θ ⇒ τ))(ts : Terms Γ Θ) Δ ->
           (t ↑ Δ) •ˢ (ts ↑ˢ Δ) ≡ (t •ˢ ts) ↑ Δ
lem-•ˢ-↑ t ∅        Δ = refl
lem-•ˢ-↑ t (u ◄ us) Δ = {! !}
-}

{-
_[_] : {Γ : Ctx}{σ τ : Type} ->
       Term (Γ , τ) σ -> Term Γ τ -> Term Γ σ
t [ u ] = t / [ u ]
-}

{-
vz      [ u ] = u
wk t    [ u ] = {! !}
(s • t) [ u ] = {! !}
(ƛ_ {τ = ρ} t)   [ u ] = ƛ {! !}
-}

{-
_↓ˣ_ : {Γ : Ctx}{σ τ : Type}
       (y : Var Γ σ)(x : Var (Γ - y) τ) -> Var (Γ - wkˣ y x) σ
vz   ↓ˣ x    = vz
vs y ↓ˣ vz   = y
vs y ↓ˣ vs x = vs (y ↓ˣ x)

lem-commute-minus :
  {Γ : Ctx}{σ τ : Type}(y : Var Γ σ)(x : Var (Γ - y) τ) ->
  Γ - y - x ≡ Γ - wkˣ y x - (y ↓ˣ x)
lem-commute-minus vz     x      = refl
lem-commute-minus (vs y) vz     = refl
lem-commute-minus (vs {Γ} y) (vs x) with Γ - y - x | lem-commute-minus y x
... | ._ | refl = refl

Lem-wk-[] :
      {Γ : Ctx}{τ σ ρ : Type}
      (y : Var Γ τ)
      (x : Var (Γ - y) σ)
      (t : Term (Γ - wkˣ y x) ρ)
      (u : Term (Γ - y - x) τ) -> Set
Lem-wk-[] {Γ}{τ}{σ}{ρ} y x t u =
    wk (wkˣ y x) t [ y := wk x u ]
    ≡ wk x t[u']'
  where
    u' : Term (Γ - wkˣ y x - y ↓ˣ x) τ
    u' = subst (\Δ -> Term Δ τ) (sym (lem-commute-minus y x)) u

    t[u']' : Term (Γ - y - x) ρ
    t[u']' = subst (\Δ -> Term Δ ρ) (lem-commute-minus y x)
             (t [ y ↓ˣ x := u' ])

postulate
 lem-wk-[] : {Γ : Ctx}{σ τ ρ : Type}
             (y : Var Γ τ)(x : Var (Γ - y) σ)
             (t : Term (Γ - wkˣ y x) ρ){u : Term (Γ - y - x) τ} ->
             Lem-wk-[] y x t u
{-
lem-wk-[] y x (var z) = {! !}
lem-wk-[] y x (t • u) = {! !}
lem-wk-[] y x (ƛ t)   = {! !}
-}

lem-wk-[]' : {Γ : Ctx}{σ τ ρ : Type}
            (x : Var Γ σ)(t : Term (Γ - x , ρ) τ){u : Term (Γ - x) ρ} ->
            wk x (t [ vz := u ]) ≡ wk (vs x) t [ vz := wk x u ]
lem-wk-[]' x t = sym (lem-wk-[] vz x t)

-}

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda