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

open import HoTT
open import lib.cubical.elims.CubeMove

module lib.cubical.elims.CofWedge where

cof-wedge-path-rec : ∀ {i j k l}
  {X : Ptd i} {Y : Ptd j} {C : Type k} {D : Type l}
  {f : X ∨ Y → C} {d₁ d₂ : D}
  → (p : d₁ == d₂)
  → (q : C → d₁ == d₂)
  → ((x : fst X) → p == q (f (winl x)))
  → ((y : fst Y) → p == q (f (winr y)))
  → ((κ : Cofiber f) → d₁ == d₂)
cof-wedge-path-rec {X = X} {Y = Y} {f = f} base* cod* winl* winr* =
  CofiberRec.f _
    base*
    cod*
    (WedgeElim.f
      winl*
      (λ y → (winl* (snd X) ∙ ap (cod* ∘ f) wglue)
             ∙ ! (winr* (snd Y)) ∙ winr* y)
      (↓-cst=app-from-square $ disc-to-square $ ! $
        ap (λ w → (winl* (snd X) ∙ ap (cod* ∘ f) wglue) ∙ w)
           (!-inv-l (winr* (snd Y)))
        ∙ ∙-unit-r _))

cof-wedge-path-elim : ∀ {i j k l}
  {X : Ptd i} {Y : Ptd j} {C : Type k} {D : Type l}
  {f : X ∨ Y → C} (g h : Cofiber f → D)
  → (p : g (cfbase _) == h (cfbase _))
  → (q : (c : C) → g (cfcod _ c) == h (cfcod _ c))
  → ((x : fst X) → Square p (ap g (cfglue _ (winl x)))
                            (ap h (cfglue _ (winl x))) (q (f (winl x))))
  → ((y : fst Y) → Square p (ap g (cfglue _ (winr y)))
                            (ap h (cfglue _ (winr y))) (q (f (winr y))))
  → ((κ : Cofiber f) → g κ == h κ)
cof-wedge-path-elim {X = X} {Y = Y} {f = f} g h base* cod* winl* winr* =
  Cofiber-elim _
    base*
    cod*
    (↓-='-from-square ∘ Wedge-elim
      winl*
      (λ y → fst fill ⊡h winr* y)
      (cube-to-↓-square $
        cube-right-from-front _ (winr* (snd Y)) (snd fill)))
  where
  fill : Σ (Square base* idp idp base*) (λ sq' →
    Cube (winl* (snd X)) sq'
      (natural-square (λ _ → base*) wglue)
      (square-push-rb _ _ (natural-square (ap g ∘ cfglue _) wglue))
      (square-push-rb _ _ (natural-square (ap h ∘ cfglue _) wglue))
      (natural-square (cod* ∘ f) wglue ⊡h' !□h (winr* (snd Y))))

  fill = fill-cube-right _ _ _ _ _

{- Note, only squares with constant endpoints. General case? -}
cof-wedge-square-elim : ∀ {i j k l}
  {X : Ptd i} {Y : Ptd j} {C : Type k} {D : Type l}
  {f : X ∨ Y → C} {d₀₀ d₀₁ d₁₀ d₁₁ : D}
  (p₀₋ : (κ : Cofiber f) → d₀₀ == d₀₁)
  (p₋₀ : (κ : Cofiber f) → d₀₀ == d₁₀)
  (p₋₁ : (κ : Cofiber f) → d₀₁ == d₁₁)
  (p₁₋ : (κ : Cofiber f) → d₁₀ == d₁₁)
  → (base* : Square (p₀₋ (cfbase _)) (p₋₀ (cfbase _))
                    (p₋₁ (cfbase _)) (p₁₋ (cfbase _)))
  → (cod* : (c : C) → Square (p₀₋ (cfcod _ c)) (p₋₀ (cfcod _ c))
                             (p₋₁ (cfcod _ c)) (p₁₋ (cfcod _ c)))
  → ((x : fst X) → Cube base* (cod* (f (winl x)))
                     (natural-square p₀₋ (cfglue _ (winl x)))
                     (natural-square p₋₀ (cfglue _ (winl x)))
                     (natural-square p₋₁ (cfglue _ (winl x)))
                     (natural-square p₁₋ (cfglue _ (winl x))))
  → ((y : fst Y) → Cube base* (cod* (f (winr y)))
                     (natural-square p₀₋ (cfglue _ (winr y)))
                     (natural-square p₋₀ (cfglue _ (winr y)))
                     (natural-square p₋₁ (cfglue _ (winr y)))
                     (natural-square p₁₋ (cfglue _ (winr y))))

  → ((κ : Cofiber f) → Square (p₀₋ κ) (p₋₀ κ) (p₋₁ κ) (p₁₋ κ))
cof-wedge-square-elim p₀₋ p₋₀ p₋₁ p₁₋ base* cod* winl* winr* =
  disc-to-square ∘ cof-wedge-path-elim _ _
    (square-to-disc base*)
    (square-to-disc ∘ cod*)
    (cube-to-disc-square ∘ winl*)
    (cube-to-disc-square ∘ winr*)

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Functor.Base where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Sigma

open import Cubical.Categories.Category

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

record Functor (C : Category ℓC ℓC') (D : Category ℓD ℓD') :
         Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
  no-eta-equality

  open Category

  field
    F-ob  : C .ob → D .ob
    F-hom : {x y : C .ob} → C [ x , y ] → D [ F-ob x , F-ob y ]
    F-id  : {x : C .ob} → F-hom (C .id) ≡ D .id {x = F-ob x}
    F-seq : {x y z : C .ob} (f : C [ x , y ]) (g : C [ y , z ])
          → F-hom (f ⋆⟨ C ⟩ g) ≡ (F-hom f) ⋆⟨ D ⟩ (F-hom g)

  isFull = (x y : _) (F[f] : D [ F-ob x , F-ob y ]) → ∃[ f ∈ C [ x , y ] ] F-hom f ≡ F[f]
  isFaithful = (x y : _) (f g : C [ x , y ]) → F-hom f ≡ F-hom g → f ≡ g
  isEssentiallySurj = (d : D .ob) → Σ[ c ∈ C .ob ] CatIso D (F-ob c) d

  F-square : {x y u v : C .ob}
             {f : C [ x , y ]} {g : C [ x , u ]}
             {h : C [ u , v ]} {k : C [ y , v ]}
           → f ⋆⟨ C ⟩ k ≡ g ⋆⟨ C ⟩ h
           → (F-hom f) ⋆⟨ D ⟩ (F-hom k) ≡ (F-hom g) ⋆⟨ D ⟩ (F-hom h)
  F-square Csquare = sym (F-seq _ _) ∙∙ cong F-hom Csquare ∙∙ F-seq _ _

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

open Category
open Functor

Functor≡ : {F G : Functor C D}
         → (h : ∀ (c : ob C) → F-ob F c ≡ F-ob G c)
         → (∀ {c c' : ob C} (f : C [ c , c' ]) → PathP (λ i → D [ h c i , h c' i ]) (F-hom F f) (F-hom G f))
         → F ≡ G
F-ob (Functor≡ hOb hHom i) c = hOb c i
F-hom (Functor≡ hOb hHom i) f = hHom f i
F-id (Functor≡ {C = C} {D = D} {F = F} {G = G} hOb hHom i) =
  isProp→PathP (λ j → isSetHom D (hHom (C .id) j) (D .id)) (F-id F) (F-id G) i
F-seq (Functor≡ {C = C} {D = D} {F = F} {G = G} hOb hHom i) f g =
  isProp→PathP (λ j → isSetHom D (hHom (f ⋆⟨ C ⟩ g) j) ((hHom f j) ⋆⟨ D ⟩ (hHom g j))) (F-seq F f g) (F-seq G f g) i

-- Helpful notation

-- action on objects
infix 30 _⟅_⟆
_⟅_⟆ : (F : Functor C D)
     → C .ob
     → D .ob
_⟅_⟆ = F-ob

-- action on morphisms
infix 30 _⟪_⟫ -- same infix level as on objects since these will never be used in the same context
_⟪_⟫ : (F : Functor C D)
     → ∀ {x y}
     → C [ x , y ]
     → D [(F ⟅ x ⟆) , (F ⟅ y ⟆)]
_⟪_⟫ = F-hom

-- Functor constructions

𝟙⟨_⟩ : ∀ (C : Category ℓ ℓ') → Functor C C
𝟙⟨ C ⟩ .F-ob x    = x
𝟙⟨ C ⟩ .F-hom f   = f
𝟙⟨ C ⟩ .F-id      = refl
𝟙⟨ C ⟩ .F-seq _ _ = refl

-- functor composition
funcComp : ∀ (G : Functor D E) (F : Functor C D) → Functor C E
(funcComp G F) .F-ob c    = G ⟅ F ⟅ c ⟆ ⟆
(funcComp G F) .F-hom f   = G ⟪ F ⟪ f ⟫ ⟫
(funcComp G F) .F-id      = cong (G ⟪_⟫) (F .F-id) ∙ G .F-id
(funcComp G F) .F-seq f g = cong (G ⟪_⟫) (F .F-seq _ _) ∙ G .F-seq _ _

infixr 30 funcComp
syntax funcComp G F = G ∘F F

_^opF : Functor C D → Functor (C ^op) (D ^op)
(F ^opF) .F-ob      = F .F-ob
(F ^opF) .F-hom     = F .F-hom
(F ^opF) .F-id      = F .F-id
(F ^opF) .F-seq f g = F .F-seq g f

ext: agda

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module STLC.Kovacs.PresheafRefinement where

open import STLC.Kovacs.Substitution public
open import STLC.Kovacs.Normalisation public
open import Category

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

-- (Tyᴺ-idₑ)
idacc : ∀ {A Γ} → (a : Γ ⊩ A)
                → acc idₑ a ≡ a
idacc {⎵}      M = idrenⁿᶠ M
idacc {A ⇒ B} f = fext¡ (fext! (λ η → f & lid○ η))

-- (Tyᴺ-∘ₑ)
acc○ : ∀ {A Γ Γ′ Γ″} → (η₁ : Γ″ ⊇ Γ′) (η₂ : Γ′ ⊇ Γ) (a : Γ ⊩ A)
                     → acc (η₂ ○ η₁) a ≡ (acc η₁ ∘ acc η₂) a
acc○ {⎵}      η₁ η₂ M = renⁿᶠ○ η₁ η₂ M
acc○ {A ⇒ B} η₁ η₂ f = fext¡ (fext! (λ η′ → f & assoc○ η′ η₁ η₂))

-- (Conᴺ-idₑ)
lid⬖ : ∀ {Γ Ξ} → (ρ : Γ ⊩⋆ Ξ)
               → ρ ⬖ idₑ ≡ ρ
lid⬖ ∅       = refl
lid⬖ (ρ , a) = _,_ & lid⬖ ρ
                   ⊗ idacc a

-- (Conᴺ-∘ₑ)
comp⬖○ : ∀ {Γ Γ′ Γ″ Ξ} → (η₁ : Γ″ ⊇ Γ′) (η₂ : Γ′ ⊇ Γ) (ρ : Γ ⊩⋆ Ξ)
                       → (ρ ⬖ η₂) ⬖ η₁ ≡ ρ ⬖ (η₂ ○ η₁)
comp⬖○ η₁ η₂ ∅       = refl
comp⬖○ η₁ η₂ (ρ , a) = _,_ & comp⬖○ η₁ η₂ ρ
                           ⊗ (acc○ η₁ η₂ a ⁻¹)

-- (∈ᴺ-nat)
get⬖ : ∀ {Γ Γ′ Ξ A} → (η : Γ′ ⊇ Γ) (ρ : Γ ⊩⋆ Ξ) (i : Ξ ∋ A)
                    → getᵥ (ρ ⬖ η) i ≡ (acc η ∘ getᵥ ρ) i
get⬖ η (ρ , a) zero    = refl
get⬖ η (ρ , a) (suc i) = get⬖ η ρ i

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

-- (Tyᴾ)
𝒰 : ∀ {A Γ} → Γ ⊩ A → Set

𝒰 {⎵}      {Γ} M = ⊤

𝒰 {A ⇒ B} {Γ} f = ∀ {Γ′} → (η : Γ′ ⊇ Γ) {a : Γ′ ⊩ A} (u : 𝒰 a)
                          → (∀ {Γ″} → (η′ : Γ″ ⊇ Γ′)
                                     → (f (η ○ η′) ∘ acc η′) a ≡
                                        (acc η′ ∘ f η) a)
                           × 𝒰 (f η a)

-- (Tyᴾₑ)
acc𝒰 : ∀ {A Γ Γ′} → {a : Γ ⊩ A}
                  → (η : Γ′ ⊇ Γ) → 𝒰 a
                  → 𝒰 (acc η a)
acc𝒰 {⎵}      {a = M} η tt = tt
acc𝒰 {A ⇒ B} {a = f} η u  = λ η′ {a} u′ →
                               let
                                 natf , u″ = u (η ○ η′) u′
                               in
                                 (λ η″ → (λ η‴ → (f η‴ ∘ acc η″) a)
                                          & (assoc○ η″ η′ η ⁻¹)
                                        ⦙ natf η″)
                               , u″

-- (Conᴾ ; ∙ ; _,_)
data 𝒰⋆ : ∀ {Γ Ξ} → Γ ⊩⋆ Ξ → Set where
  ∅   : ∀ {Γ} → 𝒰⋆ (∅ {Γ})

  _,_ : ∀ {Γ Ξ A} → {ρ : Γ ⊩⋆ Ξ} {a : Γ ⊩ A}
                  → (υ : 𝒰⋆ ρ) (u : 𝒰 a)
                  → 𝒰⋆ (ρ , a)

-- (Conᴾₑ)
-- NOTE _⬖𝒰_ = acc𝒰⋆
_⬖𝒰_ : ∀ {Γ Γ′ Ξ} → {ρ : Γ ⊩⋆ Ξ}
                  → 𝒰⋆ ρ → (η : Γ′ ⊇ Γ)
                  → 𝒰⋆ (ρ ⬖ η)
∅       ⬖𝒰 η = ∅
(υ , u) ⬖𝒰 η = υ ⬖𝒰 η , acc𝒰 η u

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

-- (∈ᴾ)
get𝒰 : ∀ {Γ Ξ A} → {ρ : Γ ⊩⋆ Ξ}
                 → 𝒰⋆ ρ → (i : Ξ ∋ A)
                 → 𝒰 (getᵥ ρ i)
get𝒰 (υ , u) zero    = u
get𝒰 (υ , u) (suc i) = get𝒰 υ i

mutual
  -- (Tmᴾ)
  eval𝒰 : ∀ {Γ Ξ A} → {ρ : Γ ⊩⋆ Ξ}
                    → 𝒰⋆ ρ → (M : Ξ ⊢ A)
                    → 𝒰 (eval ρ M)
  eval𝒰 {ρ = ρ} υ (𝓋 i)   = get𝒰 υ i
  eval𝒰 {ρ = ρ} υ (ƛ M)   = λ η {a} u →
                              (λ η′ → (λ ρ′ → eval (ρ′ , acc η′ a) M)
                                       & (comp⬖○ η′ η ρ ⁻¹)
                                     ⦙ eval⬖ η′ (υ ⬖𝒰 η , u) M)
                            , eval𝒰 (υ ⬖𝒰 η , u) M
  eval𝒰 {ρ = ρ} υ (M ∙ N) = proj₂ (eval𝒰 υ M idₑ (eval𝒰 υ N))

  -- (Tmᴺ-nat)
  eval⬖ : ∀ {Γ Γ′ Ξ A} → {ρ : Γ ⊩⋆ Ξ}
                       → (η : Γ′ ⊇ Γ) → 𝒰⋆ ρ → (M : Ξ ⊢ A)
                       → eval (ρ ⬖ η) M ≡ (acc η ∘ eval ρ) M
  eval⬖ {ρ = ρ} η υ (𝓋 i)   = get⬖ η ρ i
  eval⬖ {ρ = ρ} η υ (ƛ M)   = fext¡ (fext! (λ η′ → fext! (λ a →
                                (λ ρ′ → eval ρ′ M)
                                & ((_, a) & comp⬖○ η′ η ρ))))
  eval⬖ {ρ = ρ} η υ (M ∙ N) rewrite eval⬖ η υ M | eval⬖ η υ N
                            = (λ η′ → eval ρ M η′ (acc η (eval ρ N)))
                              & (rid○ η ⦙ lid○ η ⁻¹)
                            ⦙ proj₁ (eval𝒰 υ M idₑ (eval𝒰 υ N)) η

mutual
  -- (uᴾ)
  reflect𝒰 : ∀ {A Γ} → (M : Γ ⊢ⁿᵉ A)
                     → 𝒰 (reflect M)
  reflect𝒰 {⎵}      M = tt
  reflect𝒰 {A ⇒ B} M = λ η {a} u →
                          (λ η′ → (λ M′ N′ → reflect (M′ ∙ N′))
                                   & renⁿᵉ○ η′ η M
                                   ⊗ (natreify η′ a u)
                                 ⦙ natreflect η′ (renⁿᵉ η M ∙ reify a))
                        , reflect𝒰 (renⁿᵉ η M ∙ reify a)

  -- (qᴺ-nat)
  natreify : ∀ {A Γ Γ′} → (η : Γ′ ⊇ Γ) (a : Γ ⊩ A) → 𝒰 a
                        → (reify ∘ acc η) a ≡ (renⁿᶠ η ∘ reify) a
  natreify {⎵}      η M u = refl
  natreify {A ⇒ B} η f u =
    let
      natf , u′ = u (wkₑ idₑ) (reflect𝒰 0)
    in
      ƛ & ( reify & ( f & (wkₑ & ( rid○ η
                                 ⦙ lid○ η ⁻¹
                                 ))
                        ⊗ natreflect (liftₑ η) 0
                    ⦙ natf (liftₑ η)
                    )
          ⦙ natreify (liftₑ η) (f (wkₑ idₑ) (reflect 0)) u′
          )

  -- (uᴺ-nat)
  natreflect : ∀ {A Γ Γ′} → (η : Γ′ ⊇ Γ) (M : Γ ⊢ⁿᵉ A)
                          → (reflect ∘ renⁿᵉ η) M ≡ (acc η ∘ reflect) M
  natreflect {⎵}      η M = refl
  natreflect {A ⇒ B} η M = fext¡ (fext! (λ η′ → fext! (λ a →
                              (λ M′ → reflect (M′ ∙ reify a))
                              & (renⁿᵉ○ η′ η M ⁻¹))))

-- (uᶜᴾ)
id𝒰 : ∀ {Γ} → 𝒰⋆ (idᵥ {Γ})
id𝒰 {∅}     = ∅
id𝒰 {Γ , A} = id𝒰 ⬖𝒰 wkₑ idₑ , reflect𝒰 0

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

-- (OPEᴺ)
_⬗_ : ∀ {Γ Ξ Ξ′} → Ξ′ ⊇ Ξ → Γ ⊩⋆ Ξ′ → Γ ⊩⋆ Ξ
done    ⬗ ρ       = ρ
wkₑ η   ⬗ (ρ , a) = η ⬗ ρ
liftₑ η ⬗ (ρ , a) = η ⬗ ρ , a

-- (OPEᴺ-nat)
nat⬗ : ∀ {Γ Γ′ Ξ Ξ′} → (η₁ : Γ′ ⊇ Γ) (ρ : Γ ⊩⋆ Ξ′) (η₂ : Ξ′ ⊇ Ξ)
                     → η₂ ⬗ (ρ ⬖ η₁) ≡ (η₂ ⬗ ρ) ⬖ η₁
nat⬗ η₁ ρ       done       = refl
nat⬗ η₁ (ρ , a) (wkₑ η₂)   = nat⬗ η₁ ρ η₂
nat⬗ η₁ (ρ , a) (liftₑ η₂) = (_, acc η₁ a) & nat⬗ η₁ ρ η₂

-- (OPEᴺ-idₑ)
lid⬗ : ∀ {Γ Ξ} → (ρ : Γ ⊩⋆ Ξ)
               → idₑ ⬗ ρ ≡ ρ
lid⬗ ∅       = refl
lid⬗ (ρ , a) = (_, a) & lid⬗ ρ

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

-- (∈ₑᴺ)
get⬗ : ∀ {Γ Ξ Ξ′ A} → (ρ : Γ ⊩⋆ Ξ′) (η : Ξ′ ⊇ Ξ) (i : Ξ ∋ A)
                    → getᵥ (η ⬗ ρ) i ≡ (getᵥ ρ ∘ getₑ η) i
get⬗ ρ       done      i       = refl
get⬗ (ρ , a) (wkₑ η)   i       = get⬗ ρ η i
get⬗ (ρ , a) (liftₑ η) zero    = refl
get⬗ (ρ , a) (liftₑ η) (suc i) = get⬗ ρ η i

-- (Tmₑᴺ)
eval⬗ : ∀ {Γ Ξ Ξ′ A} → (ρ : Γ ⊩⋆ Ξ′) (η : Ξ′ ⊇ Ξ) (M : Ξ ⊢ A)
                     → eval (η ⬗ ρ) M ≡ (eval ρ ∘ ren η) M
eval⬗ ρ η (𝓋 i)   = get⬗ ρ η i
eval⬗ ρ η (ƛ M)   = fext¡ (fext! (λ η′ → fext! (λ a →
                      (λ ρ′ → eval (ρ′ , a) M) & nat⬗ η′ ρ η ⁻¹
                    ⦙ eval⬗ (ρ ⬖ η′ , a) (liftₑ η) M)))
eval⬗ ρ η (M ∙ N) rewrite eval⬗ ρ η M | eval⬗ ρ η N
                  = refl

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

-- (Subᴺ)
-- NOTE: _◆_ = eval⋆
_◆_ : ∀ {Γ Ξ Φ} → Ξ ⊢⋆ Φ → Γ ⊩⋆ Ξ → Γ ⊩⋆ Φ
∅       ◆ ρ = ∅
(σ , M) ◆ ρ = σ ◆ ρ , eval ρ M

-- (Subᴺ-nat)
comp◆⬖ : ∀ {Γ Γ′ Ξ Φ} → {ρ : Γ ⊩⋆ Ξ}
                      → (η : Γ′ ⊇ Γ) → 𝒰⋆ ρ → (σ : Ξ ⊢⋆ Φ)
                      → (σ ◆ ρ) ⬖ η ≡ σ ◆ (ρ ⬖ η)
comp◆⬖ η υ ∅       = refl
comp◆⬖ η υ (σ , M) = _,_ & comp◆⬖ η υ σ
                         ⊗ (eval⬖ η υ M ⁻¹)

-- (Subᴺ-ₛ∘ₑ)
comp◆⬗ : ∀ {Γ Ξ Ξ′ Φ} → (ρ : Γ ⊩⋆ Ξ′) (η : Ξ′ ⊇ Ξ) (σ : Ξ ⊢⋆ Φ)
                      → (σ ◐ η) ◆ ρ ≡ σ ◆ (η ⬗ ρ)
comp◆⬗ ρ η ∅       = refl
comp◆⬗ ρ η (σ , M) = _,_ & comp◆⬗ ρ η σ
                         ⊗ (eval⬗ ρ η M ⁻¹)

-- (∈ₛᴺ)
get◆ : ∀ {Γ Ξ Φ A} → (ρ : Γ ⊩⋆ Ξ) (σ : Ξ ⊢⋆ Φ) (i : Φ ∋ A)
                   → getᵥ (σ ◆ ρ) i ≡ (eval ρ ∘ getₛ σ) i
get◆ ρ (σ , M) zero    = refl
get◆ ρ (σ , M) (suc i) = get◆ ρ σ i

-- (Subᴺ-idₛ)
lid◆ : ∀ {Γ Ξ} → (ρ : Γ ⊩⋆ Ξ)
               → idₛ ◆ ρ ≡ ρ
lid◆ ∅       = refl
lid◆ (ρ , a) = (_, a) & ( comp◆⬗ (ρ , a) (wkₑ idₑ) idₛ
                        ⦙ lid◆ (idₑ ⬗ ρ)
                        ⦙ lid⬗ ρ
                        )

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

accPsh : 𝒯 → Presheaf₀ 𝗢𝗣𝗘
accPsh A =
  record
    { Fₓ  = _⊩ A
    ; F   = acc
    ; idF = fext! idacc
    ; F⋄  = λ η₁ η₂ → fext! (acc○ η₂ η₁)
    }

flip⬖Psh : 𝒞 → Presheaf₀ 𝗢𝗣𝗘
flip⬖Psh Ξ =
  record
    { Fₓ  = _⊩⋆ Ξ
    ; F   = flip _⬖_
    ; idF = fext! lid⬖
    ; F⋄  = λ η₁ η₂ → fext! (λ ρ → comp⬖○ η₂ η₁ ρ ⁻¹)
    }

getᵥNT : ∀ {Ξ A} → (i : Ξ ∋ A)
                 → NaturalTransformation (flip⬖Psh Ξ) (accPsh A)
getᵥNT i =
  record
    { N    = flip getᵥ i
    ; natN = λ η → fext! (λ ρ → get⬖ η ρ i)
    }

-- TODO
-- evalNT : ∀ {Ξ A} → (M : Ξ ⊢ A)
--                  → NaturalTransformation (flip⬖Psh Ξ) (accPsh A)
-- evalNT M =
--   record
--     { N    = flip eval M
--     ; natN = λ η → fext! (λ ρ → eval⬖ {ρ = ρ} η {!!} M)
--     }

-- TODO
-- reifyNT : ∀ {A} → NaturalTransformation (accPsh A) (renⁿᶠPsh A)
-- reifyNT =
--   record
--     { N    = reify
--     ; natN = λ η → fext! (λ a → natreify η a {!!})
--     }

reflectNT : ∀ {A} → NaturalTransformation (renⁿᵉPsh A) (accPsh A)
reflectNT =
  record
    { N    = reflect
    ; natN = λ η → fext! (λ M → natreflect η M)
    }

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
------------------------------------------------------------------------
-- A combinator for running two (independent) computations in sequence
------------------------------------------------------------------------

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

module Delay-monad.Sequential where

open import Equality.Propositional as Eq using (_≡_)
open import Prelude hiding (_+_)
open import Prelude.Size

open import Conat Eq.equality-with-J as Conat
  using (zero; suc; force; _+_)

open import Delay-monad
open import Delay-monad.Bisimilarity
open import Delay-monad.Bisimilarity.Kind
open import Delay-monad.Monad

private

  variable
    a               : Level
    A B C           : Type a
    i               : Size
    k               : Kind
    f₁ f₂           : Delay (A → B) ∞
    x x₁ x₂ y y₁ y₂ : Delay A ∞
    f′              : Delay′ (A → B) ∞
    x′              : Delay′ A ∞
    h               : A → B
    z               : A

------------------------------------------------------------------------
-- The _⊛_ operator

-- Sequential composition of computations.

infixl 6 _⊛_

_⊛_ : Delay (A → B) i → Delay A i → Delay B i
f ⊛ x = f >>=′ λ f → x >>=′ λ x → now (f x)

-- The number of later constructors in f ⊛ x is bisimilar to the sum
-- of the number of later constructors in f and the number of later
-- constructors in x.

steps-⊛∼steps-+-steps :
  (f : Delay (A → B) ∞) →
  Conat.[ i ] steps (f ⊛ x) ∼ steps f + steps x
steps-⊛∼steps-+-steps {x = now _}   (now _)   = zero
steps-⊛∼steps-+-steps {x = later _} (now _)   = suc λ { .force → steps-⊛∼steps-+-steps (now _)    }
steps-⊛∼steps-+-steps               (later f) = suc λ { .force → steps-⊛∼steps-+-steps (f .force) }

-- A rearrangement lemma for _⊛_.

later-⊛∼⊛-later :
  [ i ] later f′ ⊛ x′ .force ∼ f′ .force ⊛ later x′
later-⊛∼⊛-later = lemma _ Eq.refl
  where
  lemma :
    ∀ f → f′ .force ≡ f → [ i ] later f′ ⊛ x′ .force ∼ f ⊛ later x′
  lemma {f′ = f′} {x′ = x′} (now f) eq = later λ { .force →
    f′ .force ⊛ x′ .force  ≡⟨ Eq.cong (_⊛ x′ .force) eq ⟩
    now f ⊛ x′ .force      ∎ }
  lemma {f′ = f′} {x′ = x′} (later f) eq = later λ { .force →
    f′ .force ⊛ x′ .force  ≡⟨ Eq.cong (_⊛ x′ .force) eq ⟩
    later f ⊛ x′ .force    ∼⟨ later-⊛∼⊛-later ⟩∼
    f .force ⊛ later x′    ∎ }

-- The _⊛_ operator preserves strong and weak bisimilarity and
-- expansion.

infixl 6 _⊛-cong_

_⊛-cong_ :
  [ i ] f₁ ⟨ k ⟩ f₂ →
  [ i ] x₁ ⟨ k ⟩ x₂ →
  [ i ] f₁ ⊛ x₁ ⟨ k ⟩ f₂ ⊛ x₂
p ⊛-cong q = p >>=-cong λ _ → q >>=-cong λ _ → now

-- The _⊛_ operator is (kind of) commutative.

⊛-comm :
  (f : Delay (A → B) ∞) (x : Delay A ∞) →
  [ i ] f ⊛ x ∼ map′ (flip _$_) x ⊛ f
⊛-comm (now f)   (now x)   = reflexive _
⊛-comm (now f)   (later x) = later λ { .force → ⊛-comm (now f) (x .force) }
⊛-comm (later f) (now x)   = later λ { .force → ⊛-comm (f .force) (now x) }
⊛-comm (later f) (later x) = later λ { .force →
  f .force ⊛ later x                    ∼⟨ symmetric later-⊛∼⊛-later ⟩
  later f ⊛ x .force                    ∼⟨ ⊛-comm (later f) (x .force) ⟩∼
  map′ (flip _$_) (x .force) ⊛ later f  ∎ }

-- The function map′ can be expressed using _⊛_.

map∼now-⊛ : (x : Delay A ∞) → [ i ] map′ h x ∼ now h ⊛ x
map∼now-⊛ {h = h} x =
  map′ h x                           ∼⟨ map∼>>=-now _ ⟩
  (x >>=′ now ∘ h)                   ∼⟨⟩
  (now h >>=′ λ h → x >>=′ now ∘ h)  ∼⟨⟩
  now h ⊛ x                          ∎

-- The applicative functor laws hold up to strong bisimilarity.

now-id-⊛ : [ i ] now id ⊛ x ∼ x
now-id-⊛ {x = now x}   = now
now-id-⊛ {x = later x} = later λ { .force → now-id-⊛ }

now-∘-⊛-⊛-⊛ :
  (f : Delay (B → C) ∞) (g : Delay (A → B) ∞) (x : Delay A ∞) →
  [ i ] now (λ f → f ∘_) ⊛ f ⊛ g ⊛ x ∼ f ⊛ (g ⊛ x)
now-∘-⊛-⊛-⊛ (now _)   (now _)   (now _)   = now
now-∘-⊛-⊛-⊛ (now _)   (now _)   (later x) = later λ { .force → now-∘-⊛-⊛-⊛ (now _)    (now _)    (x .force) }
now-∘-⊛-⊛-⊛ (now _)   (later g) x         = later λ { .force → now-∘-⊛-⊛-⊛ (now _)    (g .force) x          }
now-∘-⊛-⊛-⊛ (later f) g         x         = later λ { .force → now-∘-⊛-⊛-⊛ (f .force) g          x          }

now-⊛-now : [ i ] now h ⊛ now z ∼ now (h z)
now-⊛-now = now

⊛-now :
  (f : Delay (A → B) ∞) →
  [ i ] f ⊛ now z ∼ now (λ f → f z) ⊛ f
⊛-now (now f)   = now
⊛-now (later f) = later λ { .force → ⊛-now (f .force) }

------------------------------------------------------------------------
-- The _∣_ operator

-- Sequential composition of computations.

infix 10 _∣_

_∣_ : Delay A i → Delay B i → Delay (A × B) i
x ∣ y = map′ _,_ x ⊛ y

-- The number of later constructors in x ∣ y is bisimilar to the sum
-- of the number of later constructors in x and the number of later
-- constructors in y.

steps-∣∼max-steps-steps :
  Conat.[ i ] steps (x ∣ y) ∼ steps x + steps y
steps-∣∼max-steps-steps {x = x} {y = y} =
  steps (x ∣ y)                 Conat.∼⟨ Conat.reflexive-∼ _ ⟩
  steps (map′ _,_ x ⊛ y)        Conat.∼⟨ steps-⊛∼steps-+-steps (map′ _,_ x) ⟩
  steps (map′ _,_ x) + steps y  Conat.∼⟨ steps-map′ x Conat.+-cong Conat.reflexive-∼ _ ⟩∎
  steps x + steps y             ∎∼

-- The _∣_ operator preserves strong and weak bisimilarity and
-- expansion.

infix 10 _∣-cong_

_∣-cong_ :
  [ i ] x₁ ⟨ k ⟩ x₂ →
  [ i ] y₁ ⟨ k ⟩ y₂ →
  [ i ] x₁ ∣ y₁ ⟨ k ⟩ x₂ ∣ y₂
p ∣-cong q = map-cong _,_ p ⊛-cong q

-- The _∣_ operator is commutative (up to swapping of results).

∣-comm : [ i ] x ∣ y ∼ map′ swap (y ∣ x)
∣-comm {x = x} {y = y} =
  x ∣ y                                                          ∼⟨⟩
  map′ _,_ x ⊛ y                                                 ∼⟨ ⊛-comm (map′ _,_ x) y ⟩
  map′ (flip _$_) y ⊛ map′ _,_ x                                 ∼⟨ map∼now-⊛ y ⊛-cong map∼now-⊛ x ⟩
  now (flip _$_) ⊛ y ⊛ (now _,_ ⊛ x)                             ∼⟨ symmetric (now-∘-⊛-⊛-⊛ (now _ ⊛ y) (now _) x) ⟩
  now (λ f → f ∘_) ⊛ (now (flip _$_) ⊛ y) ⊛ now _,_ ⊛ x          ∼⟨ symmetric (now-∘-⊛-⊛-⊛ (now _) (now _) y) ⊛-cong (now _ ∎) ⊛-cong (x ∎) ⟩
  now _∘_ ⊛ now (λ f → f ∘_) ⊛ now (flip _$_) ⊛ y ⊛ now _,_ ⊛ x  ∼⟨⟩
  now (λ x f y → f y x) ⊛ y ⊛ now _,_ ⊛ x                        ∼⟨ ⊛-now (now (λ x f y → f y x) ⊛ y) ⊛-cong (x ∎) ⟩
  now (_$ _,_) ⊛ (now (λ x f y → f y x) ⊛ y) ⊛ x                 ∼⟨ symmetric (now-∘-⊛-⊛-⊛ (now _) (now _) y) ⊛-cong (x ∎) ⟩
  now _∘_ ⊛ now (_$ _,_) ⊛ now (λ x f y → f y x) ⊛ y ⊛ x         ∼⟨⟩
  now (curry swap) ⊛ y ⊛ x                                       ∼⟨⟩
  now _∘_ ⊛ now (swap ∘_) ⊛ now _,_ ⊛ y ⊛ x                      ∼⟨ now-∘-⊛-⊛-⊛ (now _) (now _) y ⊛-cong (x ∎) ⟩
  now (swap ∘_) ⊛ (now _,_ ⊛ y) ⊛ x                              ∼⟨ (now _ ∎) ⊛-cong symmetric (map∼now-⊛ y) ⊛-cong (x ∎) ⟩
  now (swap ∘_) ⊛ map′ _,_ y ⊛ x                                 ∼⟨⟩
  now _∘_ ⊛ now swap ⊛ map′ _,_ y ⊛ x                            ∼⟨ now-∘-⊛-⊛-⊛ (now _) (map′ _,_ y) x ⟩
  now swap ⊛ (map′ _,_ y ⊛ x)                                    ∼⟨ symmetric (map∼now-⊛ _) ⟩
  map′ swap (map′ _,_ y ⊛ x)                                     ∼⟨⟩
  map′ swap (y ∣ x)                                              ∎

-- The _∣_ operator can be expressed using other functions.

∣-∼ : [ i ] x ∣ y ∼ (x >>=′ λ x → y >>=′ λ y → now (x , y))
∣-∼ {x = x} {y = y} =
  (map′ _,_ x >>=′ λ f → y >>=′ λ y → now (f y))                 ∼⟨ (map∼>>=-now x >>=-cong λ _ → _ ∎) ⟩
  ((x >>=′ λ x → now (x ,_)) >>=′ λ f → y >>=′ λ y → now (f y))  ∼⟨ symmetric $ associativity′ x (λ x → now (x ,_)) (λ f → y >>=′ λ y → now (f y)) ⟩
  (x >>=′ λ x → now (x ,_) >>=′ λ f → y >>=′ λ y → now (f y))    ∼⟨⟩
  (x >>=′ λ x → y >>=′ λ y → now (x , y))                        ∎

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
{-# OPTIONS --universe-polymorphism --guardedness #-}
-- {-# OPTIONS --verbose tc.constr.findInScope:15 #-}
-- {-# OPTIONS --verbose tc.meta.eta:20 #-}
-- {-# OPTIONS --verbose tc.conv.term:20 #-}
-- {-# OPTIONS --verbose tc.meta.assign:70 #-}
-- {-# OPTIONS --verbose tc.eta.rec:70 #-}
-- {-# OPTIONS --verbose tc.sig.inst:30 #-}

module InstanceArguments.11-monads where

open import Effect.Monad using (RawMonad; module RawMonad)
open import Effect.Monad.Indexed using (RawIMonad; module RawIMonad)
--open import Effect.Applicative.Indexed using ()
-- identityMonad often makes monadic code ambiguous.
--open import Effect.Monad.Identity using (IdentityMonad)
open import Effect.Monad.Partiality using (_⊥; now; isNow; never; run_for_steps) renaming (monad to partialityMonad)
open import Effect.Monad.State using (StateMonad)
open import Effect.Applicative.Indexed using (IFun)
open import Function using (_$_)
open import Function.Reasoning
open import Level using (zero; Level)
--open import Data.Unit hiding (_≟_)
open import Data.Bool using (if_then_else_)
open import Data.Nat using (ℕ; _≟_; _+_; suc; _*_)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Data.List using (List; _∷_; []; [_]; null)
open import Data.List.Effectful using () renaming (monad to listMonad)
--open import Data.Product

module RawMonadExt {li f} {I : Set li} {M : IFun I f} (m : RawIMonad M) where
  -- _>>=_ : ∀ {i j k A B} → M i j A → (A → M j k B) → M i k B
  -- _>>=_ {i} {j} {k} {A} {B} = RawIMonad._>>=_ {li} {f} {I} {M} m {i} {j} {k} {A} {B}

instance i⊥ = partialityMonad
         iList = listMonad

stateMonad = StateMonad ℕ

nToList : ℕ → List ℕ
nToList 0 = [ 0 ]
nToList (suc n) = n ∷ nToList n

test′ : ℕ → (List ℕ) ⊥
test′ k = let open RawMonad partialityMonad
          in do x ← return (k ∷ k + 1 ∷ [])
                return x

test2′ : ℕ → (List ℕ) ⊥
test2′ k =  let open RawMonad partialityMonad
                open RawMonad listMonad using () renaming (_>>=_ to _l>>=_)
            in do x ← return [ k ]
                  if ⌊ k ≟ 4 ⌋ then return (x l>>= nToList) else never

open RawMonad {{...}}
open RawMonadExt {{...}}

test1 : ℕ → ℕ ⊥
test1 k =  do x ← return k
              if ⌊ x ≟ 4 ⌋ then return 10 else never

test2 : ℕ → (List ℕ) ⊥
test2 k =  do x ← return [ k ]
              if ⌊ k ≟ 4 ⌋ then return ((x ∶ List ℕ) >>= nToList) else never
test' : ℕ → (List ℕ) ⊥
test' k = do x ← return (k ∷ k + 1 ∷ [])
             if null x then never else return (x >>= nToList)

test3 : List ℕ
test3 = do x ← 1 ∷ 2 ∷ 3 ∷ []
           return $ x + 1


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors defined in terms of Data.Star
------------------------------------------------------------------------

module Data.Star.Vec where

open import Data.Star
open import Data.Star.Nat
open import Data.Star.Fin using (Fin)
open import Data.Star.Decoration
open import Data.Star.Pointer as Pointer hiding (lookup)
open import Data.Star.List using (List)
open import Relation.Binary
open import Relation.Binary.Consequences
open import Function
open import Data.Unit

-- The vector type. Vectors are natural numbers decorated with extra
-- information (i.e. elements).

Vec : Set → ℕ → Set
Vec a = All (λ _ → a)

-- Nil and cons.

[] : ∀ {a} → Vec a zero
[] = ε

infixr 5 _∷_

_∷_ : ∀ {a n} → a → Vec a n → Vec a (suc n)
x ∷ xs = ↦ x ◅ xs

-- Projections.

head : ∀ {a n} → Vec a (1# + n) → a
head (↦ x ◅ _) = x

tail : ∀ {a n} → Vec a (1# + n) → Vec a n
tail (↦ _ ◅ xs) = xs

-- Append.

infixr 5 _++_

_++_ : ∀ {a m n} → Vec a m → Vec a n → Vec a (m + n)
_++_ = _◅◅◅_

-- Safe lookup.

lookup : ∀ {a n} → Fin n → Vec a n → a
lookup i xs with Pointer.lookup i xs
... | result _ x = x

------------------------------------------------------------------------
-- Conversions

fromList : ∀ {a} → (xs : List a) → Vec a (length xs)
fromList ε        = []
fromList (x ◅ xs) = x ∷ fromList xs

toList : ∀ {a n} → Vec a n → List a
toList = gmap (const tt) decoration


text:
module Nats.Add.Comm where

open import Equality
open import Nats
open import Function

------------------------------------------------------------------------
-- internal stuffs

private

  a+0=0+a : ∀ a → a + 0 ≡ a
  a+0=0+a  zero   = refl
  a+0=0+a (suc a) = cong suc $ a+0=0+a a

  ++a+b=a+b++ : ∀ a b → suc (a + b) ≡ a + suc b
  ++a+b=a+b++  zero   b = refl
  ++a+b=a+b++ (suc a) b = cong suc $ ++a+b=a+b++ a b

  a+b=b+a : ∀ a b → a + b ≡ b + a
  a+b=b+a zero b = sym (a+0=0+a b)
  a+b=b+a (suc a) b = suc (a + b) ≡⟨ cong suc (a+b=b+a a b) ⟩ ++a+b=a+b++ b a

------------------------------------------------------------------------
-- public aliases

nat-add-comm : ∀ a b → a + b ≡ b + a
nat-add-comm = a+b=b+a


text:
{-# OPTIONS --no-unicode #-}

module Issue2749 where

-- testing ascii only lambda and arrow
id : {A : Set} -> A -> A
id = {!!}

-- testing ascii only double braces
it : {A : Set} {{a : A}} → A → A
it = {!!}

data B : Set where
  mkB : B → B → B

-- testing ascii only suffixes
left : B → B
left b1 = {!!}

open import Agda.Builtin.Equality

-- testing ascii only forall
allq : (∀ m n → m ≡ n) ≡ {!!}
allq = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --copatterns --sized-types #-}

-- {-# OPTIONS -v tc.size:60 #-}
-- {-# OPTIONS -v term:20 -vterm.matrices:40 #-}

module SizedTypesMutual where

open import Common.Size

-- Syntax: Types, terms and contexts.

infixr 6 _⇒_
infixl 1 _,_

-- Types and contexts.

data Ty : Set where
  _⇒_ : (a b : Ty) → Ty

data Cxt : Set where
  _,_ : (Γ : Cxt) (a : Ty) → Cxt

-- Generic reversed Spines (last application available first).

data RSpine (V : Ty → Set) (a : Ty) : (c : Ty) → Set where
  _,_ : ∀ {b c} → RSpine V a (b ⇒ c) → V b → RSpine V a c

-- Functoriality for RSpine

mapRSp : ∀ {V W : Ty → Set} → (∀ {d} → V d → W d) → ∀ {a c} → RSpine V a c → RSpine W a c
mapRSp f (rs , r) = mapRSp f rs , f r

-- Values and environments

mutual
  data Env {i : Size} (Δ : Cxt) : Set where
    _,_ : ∀ {a} (ρ : Env {i = i} Δ) (v : Val {i = i} Δ a) → Env Δ

  data Val {i : Size} (Δ : Cxt) : (a : Ty) → Set where
    ne  : ∀ {j : Size< i}{a c} (vs : ValSpine {i = j} Δ a c) → Val Δ c
    lam : ∀ {a b}              (ρ : Env {i = i} Δ)           → Val Δ (a ⇒ b)

  ValSpine : {i : Size} (Δ : Cxt) (a c : Ty) → Set
  ValSpine {i = i} Δ = RSpine (Val {i = i} Δ)

-- Weakening

mutual
  weakEnv : ∀ {i Δ a} → Env {i = i} Δ → Env {i = i} (Δ , a)
  weakEnv {i = i} (ρ , v)  = weakEnv ρ , weakVal v

  weakVal : ∀ {i Δ a c} → Val {i = i} Δ c → Val {i = i} (Δ , a) c
  weakVal (ne {j = j} vs)  = ne (mapRSp (weakVal {i = j}) vs)
  weakVal (lam ρ)          = lam (weakEnv ρ)

-- This mutual block produces garbage size solutions
-- if solving is not done on a per-definition basis.

-- The reason is that the current solver assumes
-- that all size constraints live in (an extension of)
-- the same context (which is not true here).

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Issue402 where

record Unit : Set where
  constructor inn
  field
    out : Unit

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

test : (x y : Unit) -> x == y
test x y = refl

-- this used to cause an infinite loop in the conversion checker
-- now it fails, because no eta-laws are generated for the
-- unguarded recursive record Unit

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --safe #-}
module Generics.Reflection where

open import Function.Base
import Data.Unit    as ⊤
import Data.Product as Product
import Relation.Binary.PropositionalEquality as Eq
open import Data.Nat.Base hiding (_⊔_)
open import Data.List.Base   as List hiding (_++_)
import Data.Vec.Base as Vec
open import Data.String as S using (String; _++_)
open import Data.Bool.Base
open import Data.Maybe.Base using (Maybe; just; nothing; maybe)
open import Agda.Builtin.Reflection renaming ( primQNameEquality to _Name≈_
                                             )
open import Reflection.Abstraction using (unAbs)
open import Reflection.Argument    using (_⟨∷⟩_; _⟅∷⟆_)
open import Reflection.Term hiding (Telescope; var)
open import Relation.Nullary using (yes; no)

open import Category.Monad   as Monad

import Data.List.Categorical as List
import Data.Nat.Induction    as Nat
import Data.Char             as C

open import Reflection.TypeChecking.Monad.Instances using (tcMonad)
open import Reflection.Traversal hiding (_,_)

open import Generics.Prelude
open import Generics.Telescope
open import Generics.Desc renaming (_,_ to _,ω_)
import Generics.Accessibility as Accessibility
open import Generics.HasDesc
import Function.Identity.Categorical as Identity

open List.TraversableM ⦃...⦄
open Monad.RawMonad    ⦃...⦄

tErr : Term → TC ⊤
tErr = typeError ∘ [_] ∘ termErr

sErr : String → TC ⊤
sErr = typeError ∘ [_] ∘ strErr

open Actions

-- `liftN n f` maps numbers 0..(n-1) to themselves, and numbers
-- `n + k` to `n + (f k)`
liftN : ℕ → (ℕ → ℕ) → (ℕ → ℕ)
liftN zero    f k       = f k
liftN (suc n) f zero    = zero
liftN (suc n) f (suc k) = suc (liftN n f k)

mapVars : (ℕ → ℕ) → Term → Term
mapVars f = traverseTerm Identity.applicative actions (0 Reflection.Traversal., [])
  where
    actions : Actions Identity.applicative
    actions .onVar  ctx = liftN (ctx .Cxt.len) f
    actions .onMeta _   = id
    actions .onCon  _   = id
    actions .onDef  _   = id

prettyName : Name → String
prettyName f = maybe id "" (List.last (S.wordsBy ('.' C.≟_) (showName f)))

{-
When converting types to telescopes
variables are converted to context lookups:
Given K := [(oₒ : Oₒ) ⋯ (o₁ : O₁)] "forced" arguments (reversed)
      P := [A₁ ⋯ Aₙ] parameters
      I := [B₁ ⋯ Bₘ] indices,

we want to replace a term in context (Γ , O₁ , ⋯ , Oₒ , A₁ , ⋯ , Aₙ , B₁ , ⋯ , Bₘ , C₁ , ⋯ , Cₚ)
into a term in context               (Γ , Σ P I , C₁ , ⋯ , Cₚ)

 A term (var k) should be replaced by:
   - (var k)                                 if k < p

   - (proj₂ (proj₂ (var p)))                 if p         <= k < p + m      (inside I)
     (proj₂ (proj₁ (proj₂ (var p))))         ...
     (proj₂ (proj₁ (proj₁ (proj₂ (var p))))) ...

   - (proj₂ (proj₁ (var p))                  if p + m     <= k < p + m + n  (inside P)
   - (proj₂ (proj₁ (proj₁ (var p)))          ...
   - (proj₂ (proj₁ (proj₁ (proj₁ (var p))))  ...

   - K[k - (n + m + p)]                      if p + m + n <= k < p + m + n + o

   - var (k + 1 - n - m - o)                 if p + m + n + o <= k
-}

-- o: position of (PI : Σ P I) in the context
--    (i.e number of locally bound variables)
mkVar : (o k : ℕ) → Name → List (Arg Term) → Term
mkVar o k t args = def (quote proj₂) (aux o k ⟨∷⟩ args)
  where
    aux : (o k : ℕ) → Term
    aux o zero    = def t (var o [] ⟨∷⟩ [])
    aux o (suc k) = def (quote proj₁) (aux o k ⟨∷⟩ [])

mkPVar : (o k : ℕ) → List (Arg Term) → Term
mkPVar o k = mkVar o k (quote proj₁)

mkIVar : (o k : ℕ) → List (Arg Term) → Term
mkIVar o k = mkVar o k (quote proj₂)

-- TODO: telescopize should account for forced arguments

module _ (fargs : List Term) (nP nI : ℕ) where

    telescopize       : ℕ → Term → Term
    telescopizeSort   : ℕ → Sort → Sort
    telescopizeArgs   : ℕ → List (Arg Term) → List (Arg Term)
    telescopizeTel    : ℕ → List (String × Arg Type) → List (String × Arg Type)
    telescopizeClause : ℕ → List Clause → List Clause

    lookupForced : List Term → ℕ → ℕ → List (Arg Term) → Term
    lookupForced [] n o = var (suc (n + o))
    -- WARN: we ignore args, this should go alright
    --       ALSO, we might/should lift everything up, probably
    lookupForced (x ∷ xs) zero o = const (mapVars (λ n → n + suc o) x)
    lookupForced (x ∷ xs) (suc n) o = lookupForced xs n o

    telescopize o (var k args) =
      let args′ = telescopizeArgs o args in
           if k <ᵇ o           then var k args′
      else if k ∸ o <ᵇ nI      then mkIVar o (k ∸ o     ) args′
      else if k ∸ o <ᵇ nI + nP then mkPVar o (k ∸ o ∸ nI) args′
      else                          lookupForced fargs (k ∸ (nI + nP + o)) o args
  --  else                          var (k ∸ pred (nP + nI)) args′

    telescopize o (con c args) = con c (telescopizeArgs o args)
    telescopize o (def f args) = def f (telescopizeArgs o args)
    telescopize o (lam v (abs s t)) = lam v (abs s (telescopize (suc o) t))
    telescopize o (pat-lam cs args) = pat-lam (telescopizeClause o cs) (telescopizeArgs o args)
    telescopize o (Π[ s ∶ arg i a ] b) = Π[ s ∶ arg i (telescopize o a) ] telescopize (suc o) b
    telescopize o (sort s) = sort (telescopizeSort o s)
    telescopize o (lit l) = lit l
    telescopize o (meta x args) = meta x (telescopizeArgs o args)
    telescopize o unknown = unknown

    telescopizeSort o (set t)  = set  (telescopize o t)
    telescopizeSort o (prop t) = prop (telescopize o t)
    telescopizeSort o x = x

    telescopizeArgs o [] = []
    telescopizeArgs o (arg i x ∷ xs) = arg i (telescopize o x) ∷ telescopizeArgs o xs

    telescopizeTel o [] = []
    telescopizeTel o ((s , arg i t) ∷ xs) = (s , arg i (telescopize o t))
                                          ∷ telescopizeTel (suc o) xs

    telescopizeClause o [] = []
    telescopizeClause o (clause tel ps t ∷ xs)
      -- careful: telescopes bring (length tel) variables in scope
      = clause (telescopizeTel o tel) ps (telescopize (o + length tel) t)
      ∷ telescopizeClause o xs
    telescopizeClause o (absurd-clause tel ps ∷ xs) =
      absurd-clause (telescopizeTel o tel) ps ∷ telescopizeClause o xs

-- sanity check
private
  module TelescopizeTests where
    t : Term
    t = var 4 []

    -- locally bound variable
    t₁ : Term
    t₁ = telescopize [] 0 0 5 t

    t₁-ok : t₁ ≡ var 4 []
    t₁-ok = refl

    -- retrieving var in index telescope, 4 variable locally-bound
    t₂ : Term
    t₂ = telescopize [] 2 1 4 t

    t₂-ok : t₂ ≡ def (quote proj₂) (def (quote proj₂) (var 4 [] ⟨∷⟩ []) ⟨∷⟩ [])
    t₂-ok = refl

    -- retrieving var in parameter telescope, 2 variable locally-bound
    t₃ : Term
    t₃ = telescopize [] 1 2 2 t

    t₃-ok : t₃ ≡ def (quote proj₂) (def (quote proj₁) (var 2 [] ⟨∷⟩ []) ⟨∷⟩ [])
    t₃-ok = refl

    -- retrieving var outside parameter & index telescope
    t₄ : Term
    t₄ = telescopize [] 1 1 2 t

    t₄-ok : t₄ ≡ var 3 []
    t₄-ok = refl

    -- retrieving 4th var in index telescope
    t₅ : Term
    t₅ = telescopize [] 0 5 1 t

    t₅-ok : t₅ ≡ def (quote proj₂)
                   (def (quote proj₁)
                    (def (quote proj₁)
                     (def (quote proj₁) (def (quote proj₂) (var 1 [] ⟨∷⟩ []) ⟨∷⟩ []) ⟨∷⟩
                      [])
                     ⟨∷⟩ [])
                    ⟨∷⟩ [])
    t₅-ok = refl

-----------------------------
-- Deriving telescopes

getIndexTel : List Term → ℕ → Type → TC Term
getIndexTel fargs nP ty = aux ty 0 (con (quote ε) [])
  where aux : Type → ℕ → Term → TC Term
        aux (agda-sort s) n I = return I
        aux (Π[ s ∶ arg i a ] b) n I = do
          i′ ← quoteTC i >>= normalise
          aux b (suc n) (con (quote _⊢<_>_)
              (I ⟨∷⟩ con (quote Product._,_) (lit (string s) ⟨∷⟩ i′ ⟨∷⟩ [])
                 ⟨∷⟩ vLam "PI" (telescopize fargs nP n 0 a)
                 ⟨∷⟩ []))
        aux _ _ _ = typeError [ strErr "ill-formed type signature when deriving index telescope" ]

getTels : List Term → ℕ → Type → TC (Term × Term)
getTels fargs nP ty = aux nP ty 0 (quoteTerm (ε {A = ⊤}))
  where aux : ℕ → Type → ℕ → Term → TC (Term × Term)
        aux zero ty _ P = (P ,_) <$> getIndexTel fargs nP ty
        aux (suc nP) (Π[ s ∶ arg i a ] b) n P = do
          i′ ← quoteTC i >>= normalise
          aux nP b (suc n) (con (quote _⊢<_>_)
              (P ⟨∷⟩ con (quote Product._,_) (lit (string s) ⟨∷⟩ i′ ⟨∷⟩ [])
                 ⟨∷⟩ vLam "PI" (telescopize fargs 0 n 0 a)
                 ⟨∷⟩ []))
        aux _ _ _ _ = typeError [ strErr "ill-formed type signature when deriving parameter telescope" ]

-----------------------------
-- Deriving descriptions

-- we cannot unquote things in Setω directly
-- so we can't unquote Terms of type Telescope directly
-- instead we produce skeletons to ease code generation
data Skel : Set where
  Cκ   : Skel
  Cπ   : ArgInfo → Skel → Skel
  _C⊗_ : Skel → Skel → Skel

dropPis : ℕ → Type → Type
dropPis (suc n) (pi a (abs _ b)) = dropPis n b
dropPis _ t = t

module _ (fargs : List Term) (dt : Name) (nP : ℕ) where

  toIndex : ℕ → List (Arg Term) → Term
  toIndex nV xs = vLam "PV" $ foldl cons (quoteTerm ⊤.tt) (drop (nP + List.length fargs) xs)
    where cons : Term → Arg Term → Term
          cons x (arg _ y) =
            con (quote Product._,_) ( x
                          ⟨∷⟩ telescopize fargs nP nV 0 y
                          ⟨∷⟩ [])

  getRecDesc : ℕ → Type → TC (Maybe (Term × Skel))
  getRecDesc n (def nm args) = do
    if nm Name≈ dt
      then return (just (con (quote ConDesc.var) (toIndex n args ⟨∷⟩ []) , Cκ))
      else return nothing
  getRecDesc n (Π[ s ∶ arg i a ] b) = do
    getRecDesc (suc n) b >>= λ where
      (just (right , skright)) → do
        i′ ← quoteTC i >>= normalise
        return $ just ( con (quote ConDesc.π) (con (quote Product._,_) (lit (string s) ⟨∷⟩ i′ ⟨∷⟩ [])
                                          ⟨∷⟩ vLam "PV" (telescopize fargs nP n 0 a) ⟨∷⟩ right ⟨∷⟩ [])
                      , Cπ i skright
                      )
      nothing  → return nothing
  getRecDesc n ty = return nothing

  getDesc : (ℕ → ℕ) → ℕ → Type → TC (Term × Skel)
  getDesc f n (def nm args) =
    -- we're gonna assume nm == dt
    -- TODO: why does this work???
    --       surely args contain parameters
    return (con (quote ConDesc.var) (toIndex n (List.map (Arg.map (mapVars f)) args) ⟨∷⟩ []) , Cκ)
  getDesc f n (Π[ s ∶ arg i a ] b) =
    getRecDesc n (mapVars f a) >>= λ where
      -- (possibly higher order) inductive argument
      (just (left , skleft)) → do
        -- we cannot depend on inductive argument (for now)
        -- note: inductive arguments are relevant (for now)
        -- /!\ inductive arguments to not bind a variable, so we strengthen the term
        (right , skright) ← getDesc ((_- 1) ∘ f) n b
        return (con (quote ConDesc._⊗_) (left ⟨∷⟩ right ⟨∷⟩ []) , (skleft C⊗ skright))
      -- plain old argument
      nothing → do
        (right , skright) ← getDesc (liftN 1 f) (suc n) b
        i′    ← quoteTC i >>= normalise
        return ( con (quote ConDesc.π) (con (quote Product._,_) (lit (string s) ⟨∷⟩ i′ ⟨∷⟩ [])
                                    ⟨∷⟩ vLam "PV" (telescopize fargs nP n 0 a)
                                    ⟨∷⟩ right
                                    ⟨∷⟩ [])
               , Cπ i skright
               )
  getDesc _ _ _ = typeError [ strErr "ill-formed constructor type" ]

-- TODO: the reason we do this is that I've failed to make the PI arguments
--       implicit in the reflection code
record HD {P} {I : ExTele P} {ℓ} (A : Indexed P I ℓ) : Setω where
  constructor mkHD

  A′ : ⟦ P , I ⟧xtel → Set ℓ
  A′ = uncurry P I A

  field
    {n} : ℕ
    D : DataDesc P I n
    names : Vec String n
    constr : ∀ pi → ⟦ D ⟧Data A′ pi → A′ pi
    split  : ∀ pi → A′ pi → ⟦ D ⟧Data A′ pi
    split∘constr : ∀ pi → (x : ⟦ D ⟧Data A′ pi) → split pi (constr pi x) ≡ω x
    constr∘split : ∀ pi → (x : A′ pi          ) → constr pi (split pi x) ≡  x

  open Accessibility A D (λ {pi} → split pi)

  field wf : ∀ pi (x : A′ pi) → Acc x

badconvert : ∀ {P} {I : ExTele P} {ℓ} {A : Indexed P I ℓ}
           → HD {P} {I} {ℓ} A → HasDesc {P} {I} {ℓ} A
badconvert d = record
  { D            = HD.D d
  ; names        = HD.names d
  ; constr       = λ {PI} → HD.constr d PI
  ; split        = λ {PI} → HD.split d PI
  ; split∘constr = λ {PI} → HD.split∘constr d PI
  ; constr∘split = λ {PI} → HD.constr∘split d PI
  ; wf           = λ {PI} → HD.wf d PI
  }

withAI : ArgInfo → Term → Term
withAI i t with relevance i
... | relevant   = t
... | irrelevant = con (quote irrv) [ vArg t ]

patAI : ArgInfo → Pattern → Pattern
patAI i t with relevance i
... | relevant   = t
... | irrelevant = con (quote irrv) [ vArg t ]

deriveThings : (gargs : List (Arg Term)) (nP : ℕ)
               (qconstr qsplit qsplitconstr qconstrsplit qwf : Name)
               (cons : List (Name × Skel))
             → TC ⊤
deriveThings gargs nP qconstr qsplit qsplitconstr qconstrsplit  qwf cons = do
  let clauses = deriveDef cons
  -- TODO: use some n-ary magic
  let (constr_cls      , rest  ) = unzip clauses
  let (split_cls       , rest  ) = unzip rest
  let (splitconstr_cls , rest  ) = unzip rest
  let (constrsplit_cls , wf_cls) = unzip rest
  defineFun qconstr       constr_cls
  defineFun qsplit        split_cls
  defineFun qsplitconstr  splitconstr_cls
  defineFun qconstrsplit  constrsplit_cls
  defineFun qwf           wf_cls
  where
    deriveIndArg : Skel → ℕ × List (String × Arg Type) × List (Arg Pattern) × List (Arg Term)
    deriveIndArg Cκ = 0 , [] , [] , []
    deriveIndArg (Cπ ia C) =
      let (o , tel , pat , args) = deriveIndArg C
      in suc o
       , ("x" , vArg unknown) ∷ tel
       , arg ia (var o) ∷ pat
       , arg ia (var o []) ∷ args

    -- WARNING: intentionally wrong, never used when deriving descriptions
    deriveIndArg (A C⊗ B) = 0 , [] , [] , []

    deriveCon : Skel → ℕ × List (String × Arg Type) -- variable types
                         × Pattern            -- pattern for ⟦_⟧Data
                         × List (Arg Pattern) -- pattern for arguments of A′ cons
                         × List (Arg Term)    -- arguments for constructor
                         × Term               -- return value for split
                         × Term               -- body of wf
    deriveCon Cκ
      = 0 , [] -- we bind zero vars
      , con (quote Eq.refl) []
      , []
      , []
      , con (quote Eq.refl) []
      , def (quote ttω) []
    deriveCon (Cπ ia C) =
      let (o , vars , datapat , apat , cargs , sval , wfval) = deriveCon C
      in suc o
       , ("s" , arg ia unknown) ∷ vars -- TODO: unsure about ia here
       , con (quote Product._,_) (patAI ia (var o) ⟨∷⟩ datapat ⟨∷⟩ [])
       , arg ia (var o) ∷ apat
       , arg ia (var o []) ∷ cargs
       , con (quote Product._,_) (withAI ia (var o []) ⟨∷⟩ sval ⟨∷⟩ [])
       , wfval
    deriveCon (A C⊗ B) =
      let (ro , rtel , rpat , rargs)  = deriveIndArg A in
      let (o , vars , datapat , apat , cargs , sval , wfval) = deriveCon B
      in suc o
       , ("x" , vArg unknown) ∷ vars -- we only support visible relevant inductive args
       , con (quote Product._,_) (var o ⟨∷⟩ datapat ⟨∷⟩ [])
       , var o ⟨∷⟩ apat
       , var o [] ⟨∷⟩ cargs
       , con (quote Product._,_) (var o [] ⟨∷⟩ sval ⟨∷⟩ [])
       , def (quote _ω,ω_)
             (pat-lam [ clause rtel rpat
                          (def qwf (unknown  -- PI of inductive argument
                                     ⟨∷⟩ var (o + ro) rargs
                                     ⟨∷⟩ []))
                      ] []
             ⟨∷⟩ wfval ⟨∷⟩ []) -- TODOOOO
    deriveClause : Pattern → Term → Name × Skel
                 → Clause × Clause × Clause × Clause × Clause
    deriveClause kp kt (consname , shape) =
      let (o , vars , datapat , apat , cargs , sval , wfval) = deriveCon shape
      in clause (("pi" , vArg unknown) ∷ vars)
                (var o ⟨∷⟩ con (quote _,ω_) (kp ⟨∷⟩ datapat ⟨∷⟩ []) ⟨∷⟩ [])
                (con consname (nP ⋯⟅∷⟆ cargs)) -- TODO: maybe forced args go here
       , clause (("pi" , vArg unknown) ∷ vars)
                (var o ⟨∷⟩ con consname apat ⟨∷⟩ [])
                (con (quote _,ω_) (kt ⟨∷⟩ sval ⟨∷⟩ []))
       , clause (("pi" , vArg unknown) ∷ vars)
                (var o ⟨∷⟩ con (quote _,ω_) (kp ⟨∷⟩ datapat ⟨∷⟩ []) ⟨∷⟩ [])
                (def (quote reflω) [])
       , clause (("pi" , vArg unknown) ∷ vars)
                (var o ⟨∷⟩ con consname apat ⟨∷⟩ [])
                (con (quote Eq.refl) [])
       , clause (("pi" , vArg unknown) ∷ vars)
                (var o ⟨∷⟩ con consname apat ⟨∷⟩ [])
                (con (quote Accessibility.Acc.acc) (wfval ⟨∷⟩ []))

    deriveClauses : Pattern -- pattern for index of constructor
                  → Term    -- term for index constructor
                  → List (Name × Skel)
                  → List (Clause × Clause × Clause × Clause × Clause)
    deriveClauses _ _ [] = []
    deriveClauses kp kt (x ∷ xs)
      = deriveClause kp kt x
      ∷ deriveClauses (con (quote Fin.suc) (kp ⟨∷⟩ []))
                      (con (quote Fin.suc) (kt ⟨∷⟩ []))
                      xs

    deriveDef : List (Name × Skel) → List (Clause × Clause × Clause × Clause × Clause)
    deriveDef [] = [ cls , cls , cls , cls , cls ]
      where cls = absurd-clause (("PI" , hArg unknown) ∷ ("x" , vArg unknown) ∷ [])
                                (var 1 ⟨∷⟩ absurd 0 ⟨∷⟩ [] )
    deriveDef xs = deriveClauses (con (quote Fin.zero) [])
                                 (con (quote Fin.zero) [])
                                 xs

macro
  deriveDesc : Term → Term → TC ⊤
  deriveDesc t hole = do
    -- Arguments are used for enabling universe-polymorphic defintions
    -- these arguments should be prepended to every use of nm as a type
    def nm gargs ← return t
      where _ → typeError [ strErr "Expected name with arguments." ]

    let fargs = reverse (List.map Arg.unArg gargs)

    data-type nP cs ← getDefinition nm
      where _ → typeError [ strErr "Name given is not a datatype." ]

    let nCons = List.length cs
    let nArgs = List.length gargs

    names ← quoteTC (Vec.fromList (List.map prettyName cs))

    -- we get the type of the family, with the provided arguments removed
    ty ← getType nm >>= normalise <&> dropPis nArgs >>= normalise

    -- (nP - nArgs) is the amount of actual parameters we consider in our encoding
    -- the remaining Pi types are indices
    (P , I) ← getTels fargs (nP - nArgs) ty

    descs&skels ← forM cs λ cn → do
      -- get the type of current constructor, with explicit arguments and parameters stripped
      conTyp ← getType cn >>= normalise <&> dropPis nP
      (desc , skel) ← getDesc fargs nm (nP - nArgs) id 0 conTyp
      return $ (cn , skel) , desc

    let descs = List.map proj₂ descs&skels
    let skels = List.map proj₁ descs&skels

    let D = foldr (λ C D → con (quote DataDesc._∷_) (C ⟨∷⟩ D ⟨∷⟩ []))
                  (con (quote DataDesc.[]) [])
                  descs

    qconstr      ← freshName "constr"
    qsplit       ← freshName "split"
    qsplitconstr ← freshName "split∘constr"
    qconstrsplit ← freshName "constr∘split"
    qwf          ← freshName "wf"

    declareDef (vArg qconstr)
      (pi (vArg (def (quote ⟦_,_⟧xtel) (P ⟨∷⟩ I ⟨∷⟩ [])))
          (abs "PI" (pi (vArg unknown) (abs "x" unknown))))

    declareDef (vArg qsplit)
      (pi (vArg (def (quote ⟦_,_⟧xtel) (P ⟨∷⟩ I ⟨∷⟩ [])))
          (abs "PI" (pi (vArg unknown) (abs "x" unknown))))

    declareDef (vArg qconstrsplit)
      (pi (vArg (def (quote ⟦_,_⟧xtel) (P ⟨∷⟩ I ⟨∷⟩ [])))
          (abs "PI" (pi (vArg unknown) (abs "x" unknown))))

    declareDef (vArg qsplitconstr)
      (pi (vArg (def (quote ⟦_,_⟧xtel) (P ⟨∷⟩ I ⟨∷⟩ [])))
          (abs "PI" (pi (vArg unknown) (abs "x" unknown))))

    declareDef (vArg qwf)
      (pi (vArg (def (quote ⟦_,_⟧xtel) (P ⟨∷⟩ I ⟨∷⟩ [])))
          (abs "PI" (pi (vArg unknown) (abs "x" unknown))))

    deriveThings gargs (nP - nArgs) qconstr qsplit qsplitconstr qconstrsplit qwf skels

    unify hole (def (quote badconvert) ((con (quote mkHD)
      (   P                 -- P
      ⟅∷⟆ I                 -- I
      ⟅∷⟆ unknown           -- ℓ
      ⟅∷⟆ def nm gargs      -- A
      ⟅∷⟆ lit (nat nCons)   -- n
      ⟅∷⟆ D                 -- D
      ⟨∷⟩ names             -- names
      ⟨∷⟩ def qconstr      []
      ⟨∷⟩ def qsplit       []
      ⟨∷⟩ def qsplitconstr []
      ⟨∷⟩ def qconstrsplit []
      ⟨∷⟩ def qwf          []
      ⟨∷⟩ [])) ⟨∷⟩ []))

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


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

-- This module shows that D<: subtyping without transitivity, or equivalently, without
-- bad bounds, remains undecidable.
module DsubNoTrans where

open import Data.List as List
open import Data.List.All as All
open import Data.Nat as ℕ
open import Data.Maybe as Maybe
open import Data.Product
open import Data.Sum
open import Data.Empty renaming (⊥ to False)
open import Data.Vec as Vec renaming (_∷_ to _‼_ ; [] to nil) hiding (_++_)
open import Function

open import Data.Maybe.Properties as Maybeₚ
open import Data.Nat.Properties as ℕₚ
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as ≡
open import Induction.Nat

open import DsubDef
open import DsubReduced
open import FsubMinus
open import FsubMinus2
open import Utils

infix 4 _⊢_<:_
data _⊢_<:_ : Env → Typ → Typ → Set where
  <:⊤  : ∀ {Γ T} → Γ ⊢ T <: ⊤
  ⊥<:  : ∀ {Γ T} → Γ ⊢ ⊥ <: T
  refl : ∀ {Γ T} → Γ ⊢ T <: T
  bnd  : ∀ {Γ S U S′ U′} →
           Γ ⊢ S′ <: S →
           Γ ⊢ U <: U′ →
           Γ ⊢ ⟨A: S ⋯ U ⟩ <: ⟨A: S′ ⋯ U′ ⟩
  Π<:  : ∀ {Γ S U S′ U′} →
           Γ ⊢ S′ <: S →
           Γ ‣ S′ ! ⊢ U <: U′ →
           Γ ⊢ Π S ∙ U <: Π S′ ∙ U′
  sel₁ : ∀ {Γ n T S} →
           env-lookup Γ n ≡ just T →
           Γ ⊢ T <: ⟨A: S ⋯ ⊤ ⟩ →
           Γ ⊢ S <: n ∙A
  sel₂ : ∀ {Γ n T U} →
           env-lookup Γ n ≡ just T →
           Γ ⊢ T <: ⟨A: ⊥ ⋯ U ⟩ →
           Γ ⊢ n ∙A <: U

module Contravariant where
  open InvertibleProperties contraInvertible _⊢_<:_ public

  D⇒Dᵢ : ∀ {Γ S U} → Γ ⊢ S <: U → ContraEnv Γ → Γ ⊢ᵢ S <: U
  D⇒Dᵢ <:⊤ all                        = ditop
  D⇒Dᵢ ⊥<: all                        = dibot
  D⇒Dᵢ refl all                       = direfl
  D⇒Dᵢ (bnd S′<:S U<:U′) all          = dibnd (D⇒Dᵢ S′<:S all) (D⇒Dᵢ U<:U′ all)
  D⇒Dᵢ (Π<: S′<:S U<:U′) all          = diall (D⇒Dᵢ S′<:S all) U<:U′
  D⇒Dᵢ (sel₁ T∈Γ S<:U) all with lookupContraEnv T∈Γ all
  ... | ctt _ with ⟨A:⟩<:⟨A:⟩ (D⇒Dᵢ S<:U all) all
  ...            | S<:⊥ , _ with <:⊥ S<:⊥ all
  ...                          | refl = dibot
  D⇒Dᵢ (sel₂ T∈Γ S<:U) all with lookupContraEnv T∈Γ all
  ... | ctt _ with ⟨A:⟩<:⟨A:⟩ (D⇒Dᵢ S<:U all) all
  ...            | _ , U′<:U          = ditrans _ (disel T∈Γ) U′<:U

module Undecidability′ where
  open FsubMinusToDsubR
  open Contravariant hiding (Π<:)

  ⟨A:⊥⟩<:-lb : ∀ {Γ T S U} → Γ ⊢ ⟨A: ⊥ ⋯ T ⟩ <: ⟨A: S ⋯ U ⟩ → ContraEnv Γ → S ≡ ⊥
  ⟨A:⊥⟩<:-lb D cΓ with ⟨A:⟩<:⟨A:⟩ (D⇒Dᵢ D cΓ) cΓ
  ... | S<:⊥ , _  with <:⊥ S<:⊥ cΓ
  ...                | S≡⊥ = S≡⊥

  <:⇒<:ᵣ : ∀ {Γ S U} →
              Γ ⊢ S <: U →
              ContraEnv Γ → Covar S → Covar U →
              Γ ⊢ᵣ S <: U
  <:⇒<:ᵣ <:⊤ cΓ cS cU                                           = drtop cS
  <:⇒<:ᵣ ⊥<: cΓ () cU
  <:⇒<:ᵣ refl cΓ cS cU                                          = drrefl cU
  <:⇒<:ᵣ (bnd S′<:S U<:U′) cΓ cS ()
  <:⇒<:ᵣ (Π<: <:⊤ U<:U′) cΓ () cU
  <:⇒<:ᵣ (Π<: ⊥<: U<:U′) cΓ cS ()
  <:⇒<:ᵣ (Π<: refl U<:U′) cΓ (cvΠ cS cU) (cvΠ cS′ cU′)          = drall cS′ cU cS′ cU′
                                                                        (drrefl cS′)
                                                                        (<:⇒<:ᵣ U<:U′ (ctt cS′ ∷ cΓ) cU cU′)
  <:⇒<:ᵣ (Π<: (bnd _ S′<:S) U<:U′) cΓ (cvΠ cS cU) (cvΠ cS′ cU′) = drall cS cU cS′ cU′
                                                                        (<:⇒<:ᵣ S′<:S cΓ cS′ cS)
                                                                        (<:⇒<:ᵣ U<:U′ (ctt cS′ ∷ cΓ) cU cU′)
  <:⇒<:ᵣ (Π<: (Π<: S′<:S S′<:S₁) U<:U′) cΓ () cU
  <:⇒<:ᵣ (Π<: (sel₁ x S′<:S) U<:U′) cΓ () cU
  <:⇒<:ᵣ (Π<: (sel₂ x S′<:S) U<:U′) cΓ cS ()
  <:⇒<:ᵣ (sel₁ T∈Γ T<:B) cΓ cS cU
    with lookupContraEnv T∈Γ cΓ
  ... | ctt _  with ⟨A:⊥⟩<:-lb T<:B cΓ
  ...             | refl                                        = case cS of λ ()
  <:⇒<:ᵣ (sel₂ T∈Γ T<:B) cΓ cS cU
    with lookupContraEnv T∈Γ cΓ
  ... | ctt cT                                                  = drsel T∈Γ cT (aux T<:B cΓ cT cU)
    where aux : ∀ {Γ T S U} → Γ ⊢ ⟨A: ⊥ ⋯ T ⟩ <: ⟨A: S ⋯ U ⟩ → ContraEnv Γ → Covar T → Covar U → Γ ⊢ᵣ T <: U
          aux refl cΓ cT cU         = drrefl cU
          aux (bnd _ T<:U) cΓ cT cU = <:⇒<:ᵣ T<:U cΓ cT cU

  <:ᵣ⇒<: : ∀ {Γ S U} → Γ ⊢ᵣ S <: U → Γ ⊢ S <: U
  <:ᵣ⇒<: (drtop _)                   = <:⊤
  <:ᵣ⇒<: (drrefl _)                  = refl
  <:ᵣ⇒<: (drall _ _ _ _ S′<:S U<:U′) = Π<: (bnd ⊥<: (<:ᵣ⇒<: S′<:S)) (<:ᵣ⇒<: U<:U′)
  <:ᵣ⇒<: (drsel T∈Γ _ T<:B)          = sel₂ T∈Γ (bnd ⊥<: (<:ᵣ⇒<: T<:B))

  open FsubMinus.FsubMinus

  F<:⇒D<: : ∀ {Γ S U} → Γ ⊢F S <: U → ⟪ Γ ⟫ ⊢ ⟦ S ⟧ <: ⟦ U ⟧
  F<:⇒D<: = <:ᵣ⇒<: ∘ F<:⇒D<:ᵣ

  D<:⇒F<: : ∀ {Γ S U} → ⟪ Γ ⟫ ⊢ ⟦ S ⟧ <: ⟦ U ⟧ → Γ ⊢F S <: U
  D<:⇒F<: S<:U = D<:ᵣ⇒F<: (<:⇒<:ᵣ S<:U (⟪⟫-contraEnv _) (⟦⟧-covar _) (⟦⟧-covar _))
                          refl refl refl


text:
{-

This file contains:

- Properties of set truncations

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.SetTruncation.Properties where

open import Cubical.HITs.SetTruncation.Base

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ' : Level
    A B C D : Type ℓ

rec : isSet B → (A → B) → ∥ A ∥₂ → B
rec Bset f ∣ x ∣₂ = f x
rec Bset f (squash₂ x y p q i j) =
  Bset _ _ (cong (rec Bset f) p) (cong (rec Bset f) q) i j

rec2 : isSet C → (A → B → C) → ∥ A ∥₂ → ∥ B ∥₂ → C
rec2 Cset f ∣ x ∣₂ ∣ y ∣₂ = f x y
rec2 Cset f ∣ x ∣₂ (squash₂ y z p q i j) =
  Cset _ _ (cong (rec2 Cset f ∣ x ∣₂) p) (cong (rec2 Cset f ∣ x ∣₂) q) i j
rec2 Cset f (squash₂ x y p q i j) z =
  Cset _ _ (cong (λ a → rec2 Cset f a z) p) (cong (λ a → rec2 Cset f a z) q) i j

-- Old version:
-- rec2 Cset f = rec (isSetΠ λ _ → Cset) λ x → rec Cset (f x)

-- lemma 6.9.1 in HoTT book
elim : {B : ∥ A ∥₂ → Type ℓ}
       (Bset : (x : ∥ A ∥₂) → isSet (B x))
       (f : (a : A) → B (∣ a ∣₂))
       (x : ∥ A ∥₂) → B x
elim Bset f ∣ a ∣₂ = f a
elim Bset f (squash₂ x y p q i j) =
  isOfHLevel→isOfHLevelDep 2 Bset _ _
    (cong (elim Bset f) p) (cong (elim Bset f) q) (squash₂ x y p q) i j

elim2 : {C : ∥ A ∥₂ → ∥ B ∥₂ → Type ℓ}
        (Cset : ((x : ∥ A ∥₂) (y : ∥ B ∥₂) → isSet (C x y)))
        (f : (a : A) (b : B) → C ∣ a ∣₂ ∣ b ∣₂)
        (x : ∥ A ∥₂) (y : ∥ B ∥₂) → C x y
elim2 Cset f ∣ x ∣₂ ∣ y ∣₂ = f x y
elim2 Cset f ∣ x ∣₂ (squash₂ y z p q i j) =
  isOfHLevel→isOfHLevelDep 2 (λ a → Cset ∣ x ∣₂ a) _ _
     (cong (elim2 Cset f ∣ x ∣₂) p) (cong (elim2 Cset f ∣ x ∣₂) q) (squash₂ y z p q) i j
elim2 Cset f (squash₂ x y p q i j) z =
  isOfHLevel→isOfHLevelDep 2 (λ a → Cset a z) _ _
    (cong (λ a → elim2 Cset f a z) p) (cong (λ a → elim2 Cset f a z) q) (squash₂ x y p q) i j

-- Old version:
-- elim2 Cset f = elim (λ _ → isSetΠ (λ _ → Cset _ _))
--                     (λ a → elim (λ _ → Cset _ _) (f a))

-- TODO: generalize
elim3 : {B : (x y z : ∥ A ∥₂) → Type ℓ}
        (Bset : ((x y z : ∥ A ∥₂) → isSet (B x y z)))
        (g : (a b c : A) → B ∣ a ∣₂ ∣ b ∣₂ ∣ c ∣₂)
        (x y z : ∥ A ∥₂) → B x y z
elim3 Bset g = elim2 (λ _ _ → isSetΠ (λ _ → Bset _ _ _))
                     (λ a b → elim (λ _ → Bset _ _ _) (g a b))

map : (A → B) → ∥ A ∥₂ → ∥ B ∥₂
map f = rec squash₂ λ x → ∣ f x ∣₂

setTruncUniversal : isSet B → (∥ A ∥₂ → B) ≃ (A → B)
setTruncUniversal {B = B} Bset =
  isoToEquiv (iso (λ h x → h ∣ x ∣₂) (rec Bset) (λ _ → refl) rinv)
  where
  rinv : (f : ∥ A ∥₂ → B) → rec Bset (λ x → f ∣ x ∣₂) ≡ f
  rinv f i x =
    elim (λ x → isProp→isSet (Bset (rec Bset (λ x → f ∣ x ∣₂) x) (f x)))
         (λ _ → refl) x i

setTruncIsSet : isSet ∥ A ∥₂
setTruncIsSet a b p q = squash₂ a b p q

setTruncIdempotent≃ : isSet A → ∥ A ∥₂ ≃ A
setTruncIdempotent≃ {A = A} hA = isoToEquiv f
  where
  f : Iso ∥ A ∥₂ A
  Iso.fun f = rec hA (idfun A)
  Iso.inv f x = ∣ x ∣₂
  Iso.rightInv f _ = refl
  Iso.leftInv f = elim (λ _ → isSet→isGroupoid setTruncIsSet _ _) (λ _ → refl)

setTruncIdempotent : isSet A → ∥ A ∥₂ ≡ A
setTruncIdempotent hA = ua (setTruncIdempotent≃ hA)

isContr→isContrSetTrunc : isContr A → isContr (∥ A ∥₂)
isContr→isContrSetTrunc contr = ∣ fst contr ∣₂
                                , elim (λ _ → isOfHLevelPath 2 (setTruncIsSet) _ _)
                                       λ a → cong ∣_∣₂ (snd contr a)

setTruncIso : Iso A B → Iso ∥ A ∥₂ ∥ B ∥₂
Iso.fun (setTruncIso is) = rec setTruncIsSet (λ x → ∣ Iso.fun is x ∣₂)
Iso.inv (setTruncIso is) = rec setTruncIsSet (λ x → ∣ Iso.inv is x ∣₂)
Iso.rightInv (setTruncIso is) =
  elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        λ a → cong ∣_∣₂ (Iso.rightInv is a)
Iso.leftInv (setTruncIso is) =
  elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        λ a → cong ∣_∣₂ (Iso.leftInv is a)

setSigmaIso : {B : A → Type ℓ} → Iso ∥ Σ A B ∥₂ ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂
setSigmaIso {A = A} {B = B} = iso fun funinv sect retr
  where
  {- writing it out explicitly to avoid yellow highlighting -}
  fun : ∥ Σ A B ∥₂ → ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂
  fun = rec setTruncIsSet λ {(a , p) → ∣ a , ∣ p ∣₂ ∣₂}
  funinv : ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂ → ∥ Σ A B ∥₂
  funinv = rec setTruncIsSet (λ {(a , p) → rec setTruncIsSet (λ p → ∣ a , p ∣₂) p})
  sect : section fun funinv
  sect = elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
              λ { (a , p) → elim {B = λ p → fun (funinv ∣ a , p ∣₂) ≡ ∣ a , p ∣₂}
              (λ p → isOfHLevelPath 2 setTruncIsSet _ _) (λ _ → refl) p }
  retr : retract fun funinv
  retr = elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
              λ { _ → refl }

sigmaElim : {B : ∥ A ∥₂ → Type ℓ} {C : Σ ∥ A ∥₂ B  → Type ℓ'}
            (Bset : (x : Σ ∥ A ∥₂ B) → isSet (C x))
            (g : (a : A) (b : B ∣ a ∣₂) → C (∣ a ∣₂ , b))
            (x : Σ ∥ A ∥₂ B) → C x
sigmaElim {B = B} {C = C} set g (x , y) =
  elim {B = λ x → (y : B x) → C (x , y)} (λ _ → isSetΠ λ _ → set _) g x y

sigmaProdElim : {C : ∥ A ∥₂ × ∥ B ∥₂ → Type ℓ} {D : Σ (∥ A ∥₂ × ∥ B ∥₂) C  → Type ℓ'}
                (Bset : (x : Σ (∥ A ∥₂ × ∥ B ∥₂) C) → isSet (D x))
                (g : (a : A) (b : B) (c : C (∣ a ∣₂ , ∣ b ∣₂)) → D ((∣ a ∣₂ , ∣ b ∣₂) , c))
                (x : Σ (∥ A ∥₂ × ∥ B ∥₂) C) → D x
sigmaProdElim {B = B} {C = C} {D = D} set g ((x , y) , c) =
  elim {B = λ x → (y : ∥ B ∥₂) (c : C (x , y)) → D ((x , y) , c)}
       (λ _ → isSetΠ λ _ → isSetΠ λ _ → set _)
       (λ x → elim (λ _ → isSetΠ λ _ → set _) (g x))
       x y c

prodElim : {C : ∥ A ∥₂ × ∥ B ∥₂ → Type ℓ}
         → ((x : ∥ A ∥₂ × ∥ B ∥₂) → isSet (C x))
         → ((a : A) (b : B) → C (∣ a ∣₂ , ∣ b ∣₂))
         → (x : ∥ A ∥₂ × ∥ B ∥₂) → C x
prodElim setC f (a , b) = elim2 (λ x y → setC (x , y)) f a b

prodRec : {C : Type ℓ} → isSet C → (A → B → C) → ∥ A ∥₂ × ∥ B ∥₂ → C
prodRec setC f (a , b) = rec2 setC f a b

prodElim2 : {E : (∥ A ∥₂ × ∥ B ∥₂) → (∥ C ∥₂ × ∥ D ∥₂) → Type ℓ}
         → ((x : ∥ A ∥₂ × ∥ B ∥₂) (y : ∥ C ∥₂ × ∥ D ∥₂) → isSet (E x y))
         → ((a : A) (b : B) (c : C) (d : D) → E (∣ a ∣₂ , ∣ b ∣₂) (∣ c ∣₂ , ∣ d ∣₂))
         → ((x : ∥ A ∥₂ × ∥ B ∥₂) (y : ∥ C ∥₂ × ∥ D ∥₂) → (E x y))
prodElim2 isset f = prodElim (λ _ → isSetΠ λ _ → isset _ _)
                             λ a b → prodElim (λ _ → isset _ _)
                                     λ c d → f a b c d

setTruncOfProdIso :  Iso ∥ A × B ∥₂ (∥ A ∥₂ × ∥ B ∥₂)
Iso.fun setTruncOfProdIso = rec (isSet× setTruncIsSet setTruncIsSet) λ { (a , b) → ∣ a ∣₂ , ∣ b ∣₂ }
Iso.inv setTruncOfProdIso = prodRec setTruncIsSet λ a b → ∣ a , b ∣₂
Iso.rightInv setTruncOfProdIso =
  prodElim (λ _ → isOfHLevelPath 2 (isSet× setTruncIsSet setTruncIsSet) _ _) λ _ _ → refl
Iso.leftInv setTruncOfProdIso =
  elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _) λ {(a , b) → refl}

IsoSetTruncateSndΣ : {A : Type ℓ} {B : A → Type ℓ'} → Iso ∥ Σ A B ∥₂ ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂
Iso.fun IsoSetTruncateSndΣ = map λ a → (fst a) , ∣ snd a ∣₂
Iso.inv IsoSetTruncateSndΣ = rec setTruncIsSet (uncurry λ x → map λ b → x , b)
Iso.rightInv IsoSetTruncateSndΣ =
  elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        (uncurry λ a → elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        λ _ → refl)
Iso.leftInv IsoSetTruncateSndΣ =
  elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
         λ _ → refl

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
open import Relation.Binary using (Rel)
open import Algebra.Bundles using (CommutativeRing)

open import Normed

module Beside
  {r ℓr} {CR : CommutativeRing r ℓr}
  (open CommutativeRing CR using () renaming (Carrier to X))
  {rel} {_≤_ : Rel X rel}
  {ma ℓma} (MA : NormedModule CR _≤_ ma ℓma)
  {mb ℓmb} (MB : NormedModule CR _≤_ mb ℓmb)
  {mc ℓmc} (MC : NormedModule CR _≤_ mc ℓmc)
  {md ℓmd} (MD : NormedModule CR _≤_ md ℓmd)
  where

open import Data.Product using (_,_; map)
open import Function using (_∘_)

open CommutativeRing CR
open import Limit using (D[_,_][_,_])
open import Assume using (assume)

private
  MAC = directProduct MA MC
  MBD = directProduct MB MD

  module MA = NormedModule MA
  module MB = NormedModule MB
  module MC = NormedModule MC
  module MD = NormedModule MD
  module MAC = NormedModule MAC
  module MBD = NormedModule MBD

⊗-differentiable-at : ∀ {f g x y} → D[ MA , MB ][ f , x ] → D[ MC , MD ][ g , y ] → D[ MAC , MBD ][ map f g , (x , y) ]
⊗-differentiable-at (f' , _) (g' , _) = (λ (x , y) (dx , dy) → f' x dx , g' y dy) , assume

max_stars_repo_name: cspollard/diff

max_issues_repo_name: cspollard/diff

max_forks_repo_name: cspollard/diff


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by total orders
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Properties.TotalOrder
  {t₁ t₂ t₃} (T : TotalOrder t₁ t₂ t₃) where

open TotalOrder T

open import Data.Sum.Base using (inj₁; inj₂)
import Relation.Binary.Construct.Converse as Converse
import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
import Relation.Binary.Properties.Poset poset as PosetProperties
open import Relation.Binary.Consequences
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contradiction)

------------------------------------------------------------------------
-- Total orders are almost decidable total orders

decTotalOrder : Decidable _≈_ → DecTotalOrder _ _ _
decTotalOrder ≟ = record
  { isDecTotalOrder = record
    { isTotalOrder = isTotalOrder
    ; _≟_          = ≟
    ; _≤?_         = total+dec⟶dec reflexive antisym total ≟
    }
  }

------------------------------------------------------------------------
-- _≥_ - the flipped relation is also a total order

open PosetProperties public
  using
  ( _≥_
  ; ≥-refl
  ; ≥-reflexive
  ; ≥-trans
  ; ≥-antisym
  ; ≥-isPreorder
  ; ≥-isPartialOrder
  ; ≥-preorder
  ; ≥-poset
  )

≥-isTotalOrder : IsTotalOrder _≈_ _≥_
≥-isTotalOrder = Converse.isTotalOrder isTotalOrder

≥-totalOrder : TotalOrder _ _ _
≥-totalOrder = record
  { isTotalOrder = ≥-isTotalOrder
  }

open TotalOrder ≥-totalOrder public
  using () renaming (total to ≥-total)

------------------------------------------------------------------------
-- _<_ - the strict version is a strict partial order

-- Note that total orders can NOT be turned into strict total orders as
-- in order to distinguish between the _≤_ and _<_ cases we must have
-- decidable equality _≈_.

open PosetProperties public
  using
  ( _<_
  ; <-resp-≈
  ; <-respʳ-≈
  ; <-respˡ-≈
  ; <-irrefl
  ; <-asym
  ; <-trans
  ; <-isStrictPartialOrder
  ; <-strictPartialOrder
  ; <⇒≉
  ; ≤∧≉⇒<
  ; <⇒≱
  ; ≤⇒≯
  )

≰⇒> : ∀ {x y} → ¬ (x ≤ y) → y < x
≰⇒> = ToStrict.≰⇒> Eq.sym reflexive total


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

open import Fragment.Equational.Theory

module Fragment.Equational.FreeExtension (Θ : Theory) where

open import Fragment.Equational.FreeExtension.Base Θ public
open import Fragment.Equational.FreeExtension.Synthetic Θ using (SynFrex) public
open import Fragment.Equational.FreeExtension.Properties Θ public

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- The values of terms in Parametric.Change.Term.
------------------------------------------------------------------------

import Parametric.Syntax.Type as Type
import Parametric.Syntax.Term as Term
import Parametric.Denotation.Value as Value
import Parametric.Change.Type as ChangeType

module Parametric.Change.Value
    {Base : Type.Structure}
    (Const : Term.Structure Base)
    (⟦_⟧Base : Value.Structure Base)
    (ΔBase : ChangeType.Structure Base)
  where

open Type.Structure Base
open Term.Structure Base Const
open Value.Structure Base ⟦_⟧Base
open ChangeType.Structure Base ΔBase

open import Base.Denotation.Notation

-- Extension point 1: The value of ⊕ for base types.
ApplyStructure : Set
ApplyStructure = ∀ ι → ⟦ ι ⟧Base → ⟦ ΔBase ι ⟧Type → ⟦ ι ⟧Base

-- Extension point 2: The value of ⊝ for base types.
DiffStructure : Set
DiffStructure = ∀ ι → ⟦ ι ⟧Base → ⟦ ι ⟧Base → ⟦ ΔBase ι ⟧Type

NilStructure : Set
NilStructure = ∀ ι → ⟦ ι ⟧Base → ⟦ ΔBase ι ⟧Type

module Structure
    (⟦apply-base⟧ : ApplyStructure)
    (⟦diff-base⟧ : DiffStructure)
    (⟦nil-base⟧ : NilStructure)
  where

  -- We provide: The value of ⊕ and ⊝ for arbitrary types.
  ⟦apply⟧ : ∀ τ → ⟦ τ ⟧ → ⟦ ΔType τ ⟧ → ⟦ τ ⟧
  ⟦diff⟧ : ∀ τ → ⟦ τ ⟧ → ⟦ τ ⟧ → ⟦ ΔType τ ⟧
  ⟦nil₍_₎⟧ : ∀ τ → ⟦ τ ⟧ → ⟦ ΔType τ ⟧

  infixl 6 ⟦apply⟧ ⟦diff⟧
  syntax ⟦apply⟧ τ v dv = v ⟦⊕₍ τ ₎⟧ dv
  syntax ⟦diff⟧ τ u v = u ⟦⊝₍ τ ₎⟧ v

  v ⟦⊕₍ base ι ₎⟧ Δv = ⟦apply-base⟧ ι v Δv
  f ⟦⊕₍ σ ⇒ τ ₎⟧ Δf = λ v → f v ⟦⊕₍ τ ₎⟧ Δf v (⟦nil₍ σ ₎⟧ v)

  u ⟦⊝₍ base ι ₎⟧ v = ⟦diff-base⟧ ι u v
  g ⟦⊝₍ σ ⇒ τ ₎⟧ f = λ v Δv → (g (v ⟦⊕₍ σ ₎⟧ Δv)) ⟦⊝₍ τ ₎⟧ (f v)

  ⟦nil₍ base ι ₎⟧ v = ⟦nil-base⟧ ι v
  ⟦nil₍ σ ⇒ τ ₎⟧ f = f ⟦⊝₍ σ ⇒ τ ₎⟧ f

  _⟦⊕⟧_ : ∀ {τ} → ⟦ τ ⟧ → ⟦ ΔType τ ⟧ → ⟦ τ ⟧
  _⟦⊕⟧_ {τ} = ⟦apply⟧ τ

  _⟦⊝⟧_ : ∀ {τ} → ⟦ τ ⟧ → ⟦ τ ⟧ → ⟦ ΔType τ ⟧
  _⟦⊝⟧_ {τ} = ⟦diff⟧ τ

  ⟦nil⟧ : ∀ {τ} → ⟦ τ ⟧ → ⟦ ΔType τ ⟧
  ⟦nil⟧ {τ} = ⟦nil₍ τ ₎⟧

  alternate : ∀ {Γ} → ⟦ Γ ⟧ → ⟦ mapContext ΔType Γ ⟧ → ⟦ ΔContext Γ ⟧
  alternate {∅} ∅ ∅ = ∅
  alternate {τ • Γ} (v • ρ) (dv • dρ) = dv • v • alternate ρ dρ

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

-- Properties relating Initial and Terminal Objects,
-- and Product / Coproduct via op

module Categories.Object.Duality {o ℓ e} (C : Category o ℓ e) where

open Category C

open import Level

open import Categories.Morphism C
open import Categories.Object.Terminal op
open import Categories.Object.Initial C
open import Categories.Object.Product op
open import Categories.Object.Coproduct C

IsInitial⇒coIsTerminal : ∀ {X} → IsInitial X → IsTerminal X
IsInitial⇒coIsTerminal is⊥ = record
  { !        = !
  ; !-unique = !-unique
  }
  where open IsInitial is⊥

⊥⇒op⊤ : Initial → Terminal
⊥⇒op⊤ i = record
  { ⊤             = ⊥
  ; ⊤-is-terminal = IsInitial⇒coIsTerminal ⊥-is-initial
  }
  where open Initial i

coIsTerminal⇒IsInitial : ∀ {X} → IsTerminal X → IsInitial X
coIsTerminal⇒IsInitial is⊤ = record
  { !        = !
  ; !-unique = !-unique
  }
  where open IsTerminal is⊤

op⊤⇒⊥ : Terminal → Initial
op⊤⇒⊥ t = record
  { ⊥            = ⊤
  ; ⊥-is-initial = coIsTerminal⇒IsInitial ⊤-is-terminal
  }
  where open Terminal t

Coproduct⇒coProduct : ∀ {A B} → Coproduct A B → Product A B
Coproduct⇒coProduct A+B = record
  { A×B      = A+B.A+B
  ; π₁       = A+B.i₁
  ; π₂       = A+B.i₂
  ; ⟨_,_⟩    = A+B.[_,_]
  ; project₁ = A+B.inject₁
  ; project₂ = A+B.inject₂
  ; unique   = A+B.unique
  }
  where
  module A+B = Coproduct A+B

coProduct⇒Coproduct : ∀ {A B} → Product A B → Coproduct A B
coProduct⇒Coproduct A×B = record
  { A+B     = A×B.A×B
  ; i₁      = A×B.π₁
  ; i₂      = A×B.π₂
  ; [_,_]   = A×B.⟨_,_⟩
  ; inject₁ = A×B.project₁
  ; inject₂ = A×B.project₂
  ; unique  = A×B.unique
  }
  where
  module A×B = Product A×B


text:
{-# OPTIONS --termination-depth=2 #-}

module TerminationWithMerge where

data List (a : Set) : Set where
  []  : List a
  _∷_ : a -> List a -> List a

open import Agda.Builtin.Bool

postulate
  a : Set
  _≤?_ : a -> a -> Bool

merge : List a -> List a -> List a
merge xs           []           = xs
merge []           ys           = ys
merge (x ∷ xs) (y ∷ ys) with x ≤? y
... | true  = x ∷ merge xs  (y ∷ ys)
... | false = y ∷ merge (x ∷ xs) ys

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit

@0 m : Name → TC ⊤
m F = defineFun F
  (clause
     (( "A"
      , arg (arg-info visible (modality relevant quantity-0))
          (agda-sort (lit 0))) ∷
      [])
     (arg (arg-info visible (modality relevant quantity-0)) (var 0) ∷
      [])
     (var 0 []) ∷
   [])

F : @0 Set → Set
unquoteDef F = m F


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

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Function.Base using (_∋_; _$_)

open import MorePropAlgebra.Bundles
import Cubical.Algebra.Ring as Std

module MorePropAlgebra.Properties.Ring {ℓ} (assumptions : Ring {ℓ}) where
open Ring assumptions renaming (Carrier to R)

import MorePropAlgebra.Properties.AbGroup
module AbGroup'Properties = MorePropAlgebra.Properties.AbGroup   (record { Ring assumptions renaming (+-AbGroup to is-AbGroup) })
module AbGroup'           =                            AbGroup   (record { Ring assumptions renaming (+-AbGroup to is-AbGroup) })
(      AbGroup')          =                            AbGroup ∋ (record { Ring assumptions renaming (+-AbGroup to is-AbGroup) })

import MorePropAlgebra.Properties.Monoid
module Monoid'Properties = MorePropAlgebra.Properties.Monoid   (record { Ring assumptions renaming (·-Monoid to is-Monoid) })
module Monoid'           =                            Monoid   (record { Ring assumptions renaming (·-Monoid to is-Monoid) })
(      Monoid')          =                            Monoid ∋ (record { Ring assumptions renaming (·-Monoid to is-Monoid) })

stdIsRing : Std.IsRing 0r 1r _+_ _·_ (-_)
stdIsRing  .Std.IsRing.+-isAbGroup = AbGroup'Properties.stdIsAbGroup
stdIsRing  .Std.IsRing.·-isMonoid  = Monoid'Properties.stdIsMonoid
stdIsRing  .Std.IsRing.dist        = is-dist

stdRing : Std.Ring {ℓ}
stdRing = record { Ring assumptions ; isRing = stdIsRing }

module RingTheory' = Std.Theory stdRing

{-

-- NOTE: a few facts about rings that might be collected from elsewhere
a+b-b≡a : ∀ a b → a ≡ (a + b) - b
a+b-b≡a a b = let P = sym (fst (+-inv b))
                  Q = sym (fst (+-identity a))
                  R = transport (λ i → a ≡ a + P i) Q
                  S = transport (λ i → a ≡ (+-assoc a b (- b)) i ) R
              in S

-- NOTE: this is called `simplL` and `simplL` in `Cubical.Structures.Group.Properties.GroupLemmas`
+-preserves-≡ : ∀{a b} → ∀ c → a ≡ b → a + c ≡ b + c
+-preserves-≡ c a≡b i = a≡b i + c

+-preserves-≡-l : ∀{a b} → ∀ c → a ≡ b → c + a ≡ c + b
+-preserves-≡-l c a≡b i = c + a≡b i

a+b≡0→a≡-b : ∀{a b} → a + b ≡ 0r → a ≡ - b
a+b≡0→a≡-b {a} {b} a+b≡0 = transport
  (λ i →
    let RHS = snd (+-identity (- b))
        LHS₁ : a + (b + - b) ≡ a + 0r
        LHS₁ = +-preserves-≡-l a (fst (+-inv b))
        LHS₂ : (a + b) - b ≡ a
        LHS₂ = transport (λ j →  (+-assoc a b (- b)) j ≡ fst (+-identity a) j) LHS₁
        in  LHS₂ i ≡ RHS i
  ) (+-preserves-≡ (- b) a+b≡0)

-- NOTE: there is already
-- -commutesWithRight-· : (x y : R) →  x · (- y) ≡ - (x · y)

a·-b≡-a·b : ∀ a b → a · (- b) ≡ - (a · b)
a·-b≡-a·b a b =
  let P : a · 0r ≡ 0r
      P = 0-rightNullifies a
      Q : a · (- b + b) ≡ 0r
      Q = transport (λ i →  a · snd (+-inv b) (~ i) ≡ 0r) P
      R : a · (- b) + a · b ≡ 0r
      R = transport (λ i → ·-rdist-+ a (- b) b i ≡ 0r) Q
  in a+b≡0→a≡-b R

a·b-a·c≡a·[b-c] : ∀ a b c → a · b - (a · c) ≡ a · (b - c)
a·b-a·c≡a·[b-c] a b c =
  let P : a · b + a · (- c) ≡ a · (b + - c)
      P = sym (·-rdist-+ a b (- c))
      Q : a · b - a · c ≡ a · (b + - c)
      Q = transport (λ i →  a · b + a·-b≡-a·b a c i ≡ a · (b + - c) ) P
  in  Q

-}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
{- Type class for comonads. -}
module CategoryTheory.Comonad where

open import CategoryTheory.Categories
open import CategoryTheory.Functor
open import CategoryTheory.NatTrans

-- A comonad on a category
record Comonad {n} (ℂ : Category n) : Set (lsuc n) where
    open Category ℂ
    field
        -- Underlying endofunctor
        W : Endofunctor ℂ
    open Functor W

    field
        -- || Definitions
        -- Counit / extract
        ε : W ⟹ I
        -- Comultiplication / duplicate
        δ : W ⟹ (W ²)

    module ε = _⟹_ ε
    module δ = _⟹_ δ
    field
        -- || Laws
        -- Duplication is cancelled by extraction on both sides (counit)
        ε-unit1 : ∀ {A : obj} -> (ε.at (omap A)) ∘ (δ.at A) ≈ id
        ε-unit2 : ∀ {A : obj} -> (fmap (ε.at A)) ∘ (δ.at A) ≈ id

        -- Duplication can be performed on both sides (coassociativity)
        δ-assoc : ∀ {A : obj} -> (δ.at (omap A)) ∘ (δ.at A)
                               ≈ (fmap (δ.at A)) ∘ (δ.at A)

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


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

module LEM where
  open import Basics
  open import Flat
  open import Bool

  open import lib.Basics
  open import lib.types.Bool
  open import Bool
  open import lib.NType2

  open import Axiom.LEM public

  flat-set-has-dec-eq : {@♭ i : ULevel} (@♭ A : hSet i)
                        → has-dec-eq (♭ (∈ A))
  flat-set-has-dec-eq A  =
    λ {(x ^♭) (y ^♭) → LEM (_==ₚ_ {A = ♭ₙ A} (x ^♭) (y ^♭))}

  discrete-set-has-dec-eq : {@♭ i : ULevel} (@♭ A : hSet i)
                            → (@♭ _ : (∈ A) is-discrete) → has-dec-eq (∈ A)
  discrete-set-has-dec-eq A p = transport has-dec-eq (discrete-id p) (flat-set-has-dec-eq A)

  _=bool=ₚ_ : {@♭ i : ULevel} {@♭ A : hSet i} {@♭ p : (∈ A) is-discrete} (x y : ∈ A) → Bool
  _=bool=ₚ_ {A = A} {p = p} x y = _=bool=_ {_} {∈ A} {discrete-set-has-dec-eq A p} x y

  un¬¬-crisp : {@♭ i : ULevel} {@♭ P : PropT i} (nnp : ¬ (¬ (P holds))) → P holds
  un¬¬-crisp {P = P} nnp with (LEM P)
  ...                    |    (inl p)  = p
  ...                    |    (inr np) = quodlibet (nnp np)

  ♭PropT₀≃Bool : ♭ PropT₀ ≃ Bool
  ♭PropT₀≃Bool = equiv to fro to-fro fro-to
    where
      to : ♭ PropT₀ → Bool
      to (P ^♭) = Dec-Prop-to-Bool P (LEM P)

      fro : Bool → ♭ PropT₀
      fro = Bool-to-♭PropT₀

      to-fro : (b : Bool) → to (fro b) == b
      to-fro true = Dec-Prop-to-Bool-true-id True (LEM True) unit
      to-fro false = Dec-Prop-to-Bool-false-id False (LEM False) quodlibet

      fro-to : (P : ♭ PropT₀) → fro (to P) == P
      fro-to (P ^♭) = case P (LEM P)
        where
          case₀♭ : (@♭ P : PropT₀) → ♭ (P holds) → fro (to (P ^♭)) == (P ^♭)
          case₀♭ P (p ^♭) = fro (to (P ^♭))
                          =⟨ (ap fro (Dec-Prop-to-Bool-true-id P (LEM P) p)) ⟩
                            fro true -- Since P holds, it equals true
                          =⟨ ! (♭-ap _^♭ (P holds-by p implies-=-True)) ⟩
                            P ^♭
                          =∎

          case₁♭ : (@♭ P : PropT₀) → ♭ (¬ (P holds)) → fro (to (P ^♭)) == (P ^♭)
          case₁♭ P (np ^♭) = fro (to (P ^♭))
                           =⟨ (ap fro (Dec-Prop-to-Bool-false-id P (LEM P) np)) ⟩
                             fro false
                           =⟨ ! (♭-ap _^♭ (¬- P holds-by np implies-=-False)) ⟩
                             P ^♭
                           =∎

          case : (@♭ P : PropT₀) → (@♭ d : Dec (P holds)) → fro (to (P ^♭)) == (P ^♭)
          case P (inl p ) = case₀♭ P (p ^♭)
          case P (inr np) = case₁♭ P (np ^♭)

  {-
  -- We prove that this equivalence preserves the relevant logical structure.
  module ♭PropT₀≃Bool-properties where
    preserves-⇒ : {@♭ P Q : PropT₀} (p : (P ⇒ Q) holds)
                  → (((–> ♭PropT₀≃Bool) (P ^♭)) ≤b ((–> ♭PropT₀≃Bool) (Q ^♭))) holds
    preserves-⇒ {P} {Q} p = {!!}

  -- As a corollary, we find that the points of the upper naturals are the conaturals.
  module Points-Of-Upper-Naturals-Are-Conaturals where
    open import UpperNaturals
    open import Conaturals

    theorem : ℕ∞ ≃ ♭ ℕ↑
    theorem = {!!}

-}

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


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

module Definition.Conversion.Soundness where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Conversion
open import Definition.Conversion.Whnf
open import Definition.Typed.Consequences.InverseUniv
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.NeTypeEq

open import Tools.Product
import Tools.PropositionalEquality as PE

mutual
  -- Algorithmic equality of neutrals is well-formed.
  soundness~↑ : ∀ {k l A Γ} → Γ ⊢ k ~ l ↑ A → Γ ⊢ k ≡ l ∷ A
  soundness~↑ (var-refl x x≡y) = PE.subst (λ y → _ ⊢ _ ≡ var y ∷ _) x≡y (refl x)
  soundness~↑ (app-cong k~l x₁) = app-cong (soundness~↓ k~l) (soundnessConv↑Term x₁)
  soundness~↑ (fst-cong x) =
    let p≡ = soundness~↓ x
        ⊢ΣFG = proj₁ (syntacticEqTerm p≡)
        ⊢F , ⊢G = syntacticΣ ⊢ΣFG
    in  fst-cong ⊢F ⊢G p≡
  soundness~↑ (snd-cong x) =
    let p≡ = soundness~↓ x
        ⊢ΣFG = proj₁ (syntacticEqTerm p≡)
        ⊢F , ⊢G = syntacticΣ ⊢ΣFG
    in  snd-cong ⊢F ⊢G p≡
  soundness~↑ (natrec-cong x₁ x₂ x₃ k~l) =
    natrec-cong (soundnessConv↑ x₁) (soundnessConv↑Term x₂)
                (soundnessConv↑Term x₃) (soundness~↓ k~l)
  soundness~↑ (Emptyrec-cong x₁ k~l) =
    Emptyrec-cong (soundnessConv↑ x₁) (soundness~↓ k~l)

  -- Algorithmic equality of neutrals in WHNF is well-formed.
  soundness~↓ : ∀ {k l A Γ} → Γ ⊢ k ~ l ↓ A → Γ ⊢ k ≡ l ∷ A
  soundness~↓ ([~] A₁ D whnfA k~l) = conv (soundness~↑ k~l) (subset* D)

  -- Algorithmic equality of types is well-formed.
  soundnessConv↑ : ∀ {A B Γ} → Γ ⊢ A [conv↑] B → Γ ⊢ A ≡ B
  soundnessConv↑ ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′) =
    trans (subset* D) (trans (soundnessConv↓ A′<>B′) (sym (subset* D′)))

  -- Algorithmic equality of types in WHNF is well-formed.
  soundnessConv↓ : ∀ {A B Γ} → Γ ⊢ A [conv↓] B → Γ ⊢ A ≡ B
  soundnessConv↓ (U-refl ⊢Γ) = refl (Uⱼ ⊢Γ)
  soundnessConv↓ (ℕ-refl ⊢Γ) = refl (ℕⱼ ⊢Γ)
  soundnessConv↓ (Empty-refl ⊢Γ) = refl (Emptyⱼ ⊢Γ)
  soundnessConv↓ (Unit-refl ⊢Γ) = refl (Unitⱼ ⊢Γ)
  soundnessConv↓ (ne x) = univ (soundness~↓ x)
  soundnessConv↓ (Π-cong F c c₁) =
    Π-cong F (soundnessConv↑ c) (soundnessConv↑ c₁)
  soundnessConv↓ (Σ-cong F c c₁) =
    Σ-cong F (soundnessConv↑ c) (soundnessConv↑ c₁)

  -- Algorithmic equality of terms is well-formed.
  soundnessConv↑Term : ∀ {a b A Γ} → Γ ⊢ a [conv↑] b ∷ A → Γ ⊢ a ≡ b ∷ A
  soundnessConv↑Term ([↑]ₜ B t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u) =
    conv (trans (subset*Term d)
                (trans (soundnessConv↓Term t<>u)
                       (sym (subset*Term d′))))
         (sym (subset* D))

  -- Algorithmic equality of terms in WHNF is well-formed.
  soundnessConv↓Term : ∀ {a b A Γ} → Γ ⊢ a [conv↓] b ∷ A → Γ ⊢ a ≡ b ∷ A
  soundnessConv↓Term (ℕ-ins x) = soundness~↓ x
  soundnessConv↓Term (Empty-ins x) = soundness~↓ x
  soundnessConv↓Term (Unit-ins x) = soundness~↓ x
  soundnessConv↓Term (ne-ins t u x x₁) =
    let _ , neA , _ = ne~↓ x₁
        _ , t∷M , _ = syntacticEqTerm (soundness~↓ x₁)
        M≡A = neTypeEq neA t∷M t
    in  conv (soundness~↓ x₁) M≡A
  soundnessConv↓Term (univ x x₁ x₂) = inverseUnivEq x (soundnessConv↓ x₂)
  soundnessConv↓Term (zero-refl ⊢Γ) = refl (zeroⱼ ⊢Γ)
  soundnessConv↓Term (suc-cong c) = suc-cong (soundnessConv↑Term c)
  soundnessConv↓Term (η-eq x x₁ y y₁ c) =
    let ⊢ΠFG = syntacticTerm x
        ⊢F , _ = syntacticΠ ⊢ΠFG
    in  η-eq ⊢F x x₁ (soundnessConv↑Term c)
  soundnessConv↓Term (Σ-η ⊢p ⊢r pProd rProd fstConv sndConv) =
    let ⊢ΣFG = syntacticTerm ⊢p
        ⊢F , ⊢G = syntacticΣ ⊢ΣFG
        fst≡ = soundnessConv↑Term fstConv
        snd≡ = soundnessConv↑Term sndConv
    in  Σ-η ⊢F ⊢G ⊢p ⊢r fst≡ snd≡
  soundnessConv↓Term (η-unit [a] [b] aUnit bUnit) = η-unit [a] [b]


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

open import HoTT
open import cohomology.FunctionOver

{- Flipping the pushout diagram (switching left and right) gives the
 - same pushout. -}

module cohomology.FlipPushout where

{- Span-flipping functions -}
flip-span : ∀ {i j k} → Span {i} {j} {k} → Span {j} {i} {k}
flip-span (span A B C f g) = span B A C g f

flip-⊙span : ∀ {i j k} → ⊙Span {i} {j} {k} → ⊙Span {j} {i} {k}
flip-⊙span (⊙span X Y Z f g) = ⊙span Y X Z g f

{- Pushout-flipping function -}
module _ {i j k} {d : Span {i} {j} {k}} where

  module FlipPushout = PushoutRec
    (right {d = flip-span d})
    (left {d = flip-span d})
    (λ z → ! (glue {d = flip-span d} z))

  flip-pushout : Pushout d → Pushout (flip-span d)
  flip-pushout = FlipPushout.f

flip-pushout-involutive : ∀ {i j k} (d : Span {i} {j} {k})
  (s : Pushout d) → flip-pushout (flip-pushout s) == s
flip-pushout-involutive d = Pushout-elim
  (λ a → idp)
  (λ b → idp)
  (λ c → ↓-∘=idf-in flip-pushout flip-pushout $
     ap flip-pushout (ap flip-pushout (glue c))
       =⟨ ap (ap flip-pushout) (FlipPushout.glue-β c) ⟩
     ap flip-pushout (! (glue c))
       =⟨ ap-! flip-pushout (glue c) ⟩
     ! (ap flip-pushout (glue c))
       =⟨ ap ! (FlipPushout.glue-β c) ⟩
     ! (! (glue c))
       =⟨ !-! (glue c) ⟩
     glue c ∎)

{- Equivalence for spans with proofs that the equivalence swaps the
 - injections -}
module _ {i j k} (d : Span {i} {j} {k}) where

  open Span d

  flip-pushout-equiv : Pushout d ≃ Pushout (flip-span d)
  flip-pushout-equiv =
    equiv flip-pushout flip-pushout
      (flip-pushout-involutive (flip-span d))
      (flip-pushout-involutive d)

  flip-pushout-path : Pushout d == Pushout (flip-span d)
  flip-pushout-path = ua flip-pushout-equiv

  flip-left : left == right [ (λ D → (A → D)) ↓ flip-pushout-path ]
  flip-left = codomain-over-equiv _ _

  flip-right : right == left [ (λ D → (B → D)) ↓ flip-pushout-path ]
  flip-right = codomain-over-equiv _ _

{- Path for pointed spans with proofs that the path swaps the pointed
 - injections -}
module _ {i j k} (ps : ⊙Span {i} {j} {k}) where

  open ⊙Span ps

  private
    s = ⊙span-out ps

    preserves : –> (flip-pushout-equiv s) (left (snd X)) == left (snd Y)
    preserves = snd (⊙right (flip-⊙span ps))

  flip-⊙pushout : fst (⊙Pushout ps ⊙→ ⊙Pushout (flip-⊙span ps))
  flip-⊙pushout = (FlipPushout.f , preserves)

  flip-⊙pushout-path : ⊙Pushout ps == ⊙Pushout (flip-⊙span ps)
  flip-⊙pushout-path = ⊙ua (⊙≃-in (flip-pushout-equiv s) preserves)

  {- action of [flip-pushout] on [snd ⊙right] -}
  ap-flip-right : ap flip-pushout (snd (⊙right ps))
               == ! (snd (⊙right (flip-⊙span ps)))
  ap-flip-right = lemma f g
    where
    lemma : {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
        (f : fst (Z ⊙→ X)) (g : fst (Z ⊙→ Y))
      → ap (flip-pushout {d = ⊙span-out (⊙span X Y Z f g)})
          (ap right (! (snd g)) ∙ ! (glue (snd Z)) ∙' ap left (snd f))
        == ! (ap right (! (snd f)) ∙ ! (glue (snd Z)) ∙' ap left (snd g))
    lemma {Z = Z} (f , idp) (g , idp) =
      ap flip-pushout (! (glue (snd Z)))
        =⟨ ap-! flip-pushout (glue (snd Z)) ⟩
      ! (ap flip-pushout (glue (snd Z)))
        =⟨ FlipPushout.glue-β (snd Z) |in-ctx ! ⟩
      ! (! (glue (snd Z))) ∎

  flip-⊙left : ⊙left ps == ⊙right (flip-⊙span ps)
                  [ (λ W → fst (X ⊙→ W)) ↓ flip-⊙pushout-path ]
  flip-⊙left = codomain-over-⊙equiv _ _

  flip-⊙right : ⊙right ps == ⊙left (flip-⊙span ps)
                   [ (λ W → fst (Y ⊙→ W)) ↓ flip-⊙pushout-path ]
  flip-⊙right =
    codomain-over-⊙equiv _ _
    ▹ pair= idp (ap (λ w → w ∙ preserves) ap-flip-right ∙ !-inv-l preserves)

flip-⊙pushout-involutive : ∀ {i j k} (ps : ⊙Span {i} {j} {k})
  → flip-⊙pushout (flip-⊙span ps) ⊙∘ flip-⊙pushout ps == ⊙idf _
flip-⊙pushout-involutive ps =
  ⊙λ= (flip-pushout-involutive _) lemma
  where
  lemma :
    ap flip-pushout (snd (⊙right (flip-⊙span ps))) ∙ snd (⊙right ps)
    == idp
  lemma =
    ap flip-pushout (snd (⊙right (flip-⊙span ps))) ∙ snd (⊙right ps)
      =⟨ ap-flip-right (flip-⊙span ps)
         |in-ctx (λ w → w ∙ snd (⊙right ps)) ⟩
    ! (snd (⊙right ps)) ∙ snd (⊙right ps)
      =⟨ !-inv-l (snd (⊙right ps)) ⟩
    idp

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
open import x1-Base
open import x4-Nat
open import x3-PropositionalEquality using (_≡_; refl; cong; equivalence)
open import x2-Sort _≤?_ totalOrder

module x5-Test where

empty : OList ⊥ ⊤
empty = nil ⊥≤̂

l-9 : OList ⊥ ⊤
l-9 = insert 9 empty ⊥≤̂ ≤̂⊤

_ : l-9 ≡ cons 9 (nil ≤̂⊤) ⊥≤̂
_ = refl

l-5-9 : OList ⊥ ⊤
l-5-9 = insert 5 l-9 ⊥≤̂ ≤̂⊤

_ : l-5-9 ≡ cons 5
                 (cons 9
                       (nil ≤̂⊤)
                       (≤-lift (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))))
                 ⊥≤̂
_ = refl

l-1-5-9 : OList ⊥ ⊤
l-1-5-9 = insert 1 l-5-9 ⊥≤̂ ≤̂⊤

_ : l-1-5-9 ≡ cons 1
                   (cons 5
                         (cons 9
                               (nil ≤̂⊤)
                               (≤-lift (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))))
                         (≤-lift (s≤s z≤n))) -- NOTE CHANGE
                   ⊥≤̂
_ = refl

sl : List ℕ
sl = t-sort (12 ∷ 3 ∷ 7 ∷ 4 ∷ 40 ∷ 5 ∷ 0 ∷ [])

_ : sl ≡ (0 ∷ 3 ∷ 4 ∷ 5 ∷ 7 ∷ 12 ∷ 40 ∷ [])
_ = refl

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
module io-test where

open import io
open import string
open import unit

main : IO ⊤
main = (readFiniteFile "hello-world.txt") >>= λ x → writeFile "output.txt" x

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
module calculus where

open import utility

open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.Properties
open import Esterel.Lang.CanFunction
  using (Canθₛ ; Canθₛₕ ; [S]-env)
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; sig ; []env ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.Context
  using (EvaluationContext ; EvaluationContext1 ; _⟦_⟧e ; _≐_⟦_⟧e ;
         Context ; Context1 ; _⟦_⟧c ; _≐_⟦_⟧c)
open import Esterel.Variable.Signal as Signal
  using (Signal)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)
open import Esterel.Context.Properties

open import Relation.Nullary
  using (¬_)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl)
open import Data.Empty
  using (⊥ ; ⊥-elim)
import Data.FiniteMap
open import Data.List
  using (List ; _∷_ ; [] ; _++_)
open import Data.List.All as All
  using (All ; _∷_ ; [])
open import Data.Nat
  using (ℕ ; zero ; suc ; _+_) renaming (_⊔_ to _⊔ℕ_)
open import Data.Product
  using (Σ-syntax ; Σ ; _,_ ; proj₁ ; proj₂ ; _×_ ; _,′_)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Relation.Binary.PropositionalEquality

open import sn-calculus

open _≐_⟦_⟧e
open _≐_⟦_⟧c

open EvaluationContext1
open Context1

infix 4 _⟶₁_
infix 4 _⟶_
infix 4 _⟶*_

data _⟶₁_ : Term → Term → Set where
  [par-swap] : ∀{p q} →
    (p ∥ q) ⟶₁ (q ∥ p)

  [par-nothing] : ∀ {q} ->
    done q ->
    (nothin ∥ q) ⟶₁ q

  [par-1exit] : ∀ {q} -> ∀ n ->
    (pausedq : paused q) ->
    (exit n ∥ q) ⟶₁ exit n

  [par-2exit] : ∀ n m ->
    (exit n ∥ exit m) ⟶₁ exit (n ⊔ℕ m)

  [is-present] : ∀{θ r p q E A} → ∀ S ->
    (S∈ : (Env.isSig∈ S θ)) →
    (θ[S]≡present : Env.sig-stats{S} θ S∈ ≡ Signal.present) →
    (de : r ≐ E ⟦ present S ∣⇒ p ∣⇒ q ⟧e) →
    (ρ⟨ θ , A ⟩· r) ⟶₁ (ρ⟨ θ , A ⟩· E ⟦ p ⟧e)

  [is-absent] : ∀{θ r p q E A} → ∀ S ->
    (S∈ : (Env.isSig∈ S θ)) →
    (θ[S]≡absent : Env.sig-stats{S} θ S∈ ≡ Signal.absent) →
    (de : r ≐ E ⟦ present S ∣⇒ p ∣⇒ q ⟧e) →
    (ρ⟨ θ , A ⟩· r) ⟶₁ (ρ⟨ θ , A ⟩· E ⟦ q ⟧e)

  [emit] : ∀{θ r S E} →
    (S∈ : (Env.isSig∈ S θ)) →
    (¬S≡a : ¬ (Env.sig-stats{S} θ S∈) ≡ Signal.absent) →
    (de : r ≐ E ⟦ emit S ⟧e) →
    (ρ⟨ θ , GO ⟩· r) ⟶₁
    (ρ⟨ (Env.set-sig{S} θ S∈ Signal.present) , GO ⟩·
      E ⟦ nothin ⟧e)

  [loop-unroll] : ∀{p} →
    (loop p)
    ⟶₁
    (loopˢ p p)

  [seq-done] : ∀{q} →
    (nothin >> q) ⟶₁ q

  [seq-exit] : ∀{q n} →
    (exit n >> q) ⟶₁ (exit n)

  [loopˢ-exit] : ∀{q n} →
    (loopˢ (exit n) q) ⟶₁ (exit n)

  [suspend-done] : ∀{p S} →
    (haltedp : halted p) →
    (suspend p S) ⟶₁ p

  -- traps
  [trap-done] : ∀{p} →
    (haltedp : halted p) →
    (trap p) ⟶₁ (↓ haltedp)

  -- lifting signals
  [raise-signal] : ∀{p S} →
    (signl S p) ⟶₁
    (ρ⟨ (Θ SigMap.[ S ↦ Signal.unknown ] ShrMap.empty VarMap.empty) , WAIT ⟩·
      p)

  -- shared state
  [raise-shared] : ∀{θ r s e p E A} →
    (all-readyeθ : all-ready e θ) →
    (de : r ≐ E ⟦ shared s ≔ e in: p ⟧e) →
    (ρ⟨ θ , A ⟩· r) ⟶₁
    (ρ⟨ θ , A ⟩· E ⟦ (ρ⟨ [s,δe]-env s (δ all-readyeθ) , WAIT ⟩· p) ⟧e)

  [set-shared-value-old] : ∀{θ r s e E} →
    (e' : all-ready e θ) →
    (s∈ : (Env.isShr∈ s θ)) →
    (θ[s]≡old : Env.shr-stats{s} θ s∈ ≡ SharedVar.old) →
    (de : r ≐ E ⟦ s ⇐ e ⟧e) →
    (ρ⟨ θ , GO ⟩· r) ⟶₁
    (ρ⟨ (Env.set-shr{s} θ s∈ (SharedVar.new) (δ e')) , GO ⟩·
      E ⟦ nothin ⟧e)

  [set-shared-value-new] : ∀{θ r s e E} →
    (e' : all-ready e θ) →
    (s∈ : (Env.isShr∈ s θ)) →
    (θ[s]≡n : Env.shr-stats{s} θ s∈ ≡ SharedVar.new) →
    (de : r ≐ E ⟦ s ⇐ e ⟧e) →
    (ρ⟨ θ , GO ⟩· r) ⟶₁
    (ρ⟨ (Env.set-shr{s} θ s∈ (SharedVar.new) (Env.shr-vals{s} θ s∈ + δ e')) , GO ⟩·
      E ⟦ nothin ⟧e)

  -- unshared state
  [raise-var] : ∀{θ r x p e E A} →
    (all-readyeθ : all-ready e θ) →
    (de : r ≐ E ⟦ var x ≔ e in: p ⟧e) →
    (ρ⟨ θ , A ⟩· r) ⟶₁
    (ρ⟨ θ , A ⟩·
      E ⟦ (ρ⟨ [x,δe]-env x (δ all-readyeθ) , WAIT ⟩· p) ⟧e)

  [set-var] : ∀{θ r x e E A} →
    (x∈ : (Env.isVar∈ x θ)) →
    (all-readyeθ : all-ready e θ) →
    (de : r ≐ E ⟦ x ≔ e ⟧e) →
    (ρ⟨ θ , A ⟩· r) ⟶₁
    (ρ⟨ (Env.set-var{x} θ x∈ (δ all-readyeθ)) , A ⟩·
      E ⟦ nothin ⟧e)

  -- if
  [if-false] : ∀{θ r p q x E A} →
    (x∈ : (Env.isVar∈ x θ)) →
    (θ[x]≡z : Env.var-vals{x} θ x∈ ≡ zero) →
    (de : r ≐ E ⟦ if x ∣⇒ p ∣⇒ q ⟧e) →
    (ρ⟨ θ , A ⟩· r) ⟶₁ (ρ⟨ θ , A ⟩· E ⟦ q ⟧e)

  [if-true] : ∀{θ r p q x E n A} →
    (x∈ : (Env.isVar∈ x θ)) →
    (θ[x]≡s : Env.var-vals{x} θ x∈ ≡ suc n) →
    (de : r ≐ E ⟦ if x ∣⇒ p ∣⇒ q ⟧e) →
    (ρ⟨ θ , A ⟩· r) ⟶₁ (ρ⟨ θ , A ⟩· E ⟦ p ⟧e)

  -- progression
  [absence] : ∀{θ p A} -> ∀ S →
    (S∈ : (Env.isSig∈ S θ)) →
    (θ[S]≡unknown : Env.sig-stats{S} θ S∈ ≡ Signal.unknown) →
    (S∉Canθₛ : (Signal.unwrap S) ∉ Canθₛ (sig θ) 0 p []env) →
    (ρ⟨ θ , A ⟩· p) ⟶₁
    (ρ⟨ (Env.set-sig{S} θ S∈ (Signal.absent)) , A ⟩·
      p)

  [readyness] : ∀{θ p A} -> ∀ s →
    (s∈ : (Env.isShr∈ s θ)) →
    (θ[s]≡old⊎θ[s]≡new : (Env.shr-stats{s} θ s∈ ≡ SharedVar.old) ⊎
                         (Env.shr-stats{s} θ s∈ ≡ SharedVar.new)) →
    (s∉Canθₛₕ : (SharedVar.unwrap s) ∉ Canθₛₕ (sig θ) 0 p []env) →
    (ρ⟨ θ , A ⟩· p) ⟶₁
    (ρ⟨ (Env.set-shr{s} θ s∈ (SharedVar.ready) (Env.shr-vals{s} θ s∈)) , A ⟩·
      p)

  [merge] : ∀{θ₁ θ₂ r p E A₁ A₂} →
    (de : r ≐ E ⟦ ρ⟨ θ₂ , A₂ ⟩· p ⟧e) →
    (ρ⟨ θ₁ , A₁ ⟩· r) ⟶₁ (ρ⟨ (θ₁ ← θ₂) , (A-max A₁ A₂) ⟩· E ⟦ p ⟧e)

-- The compatible closure of _⟶₁_.
data _⟶_ : Term → Term → Set where
  [context] : ∀{r p p'} →
    (C : Context) →
    (dc : r ≐ C ⟦ p ⟧c) →
    (p⟶₁p' : p ⟶₁ p') →
    r ⟶ (C ⟦ p' ⟧c)

-- The reflexive transitive closure of ⟶
data _⟶*_ : Term → Term → Set where
  [refl] : ∀{p} → (p ⟶* p)
  [step] : ∀{p q r} → (p⟶q : p ⟶ q) → (q⟶*r : q ⟶* r) → (p ⟶* r)

data _≡ₑ_#_ : Term -> Term -> List Context1 -> Set where

  ≡ₑrefl : ∀ {p C} ->

    ------------
     p ≡ₑ p # C

  ≡ₑtran : ∀ {p r q C} ->

     (p≡ₑr#C : p ≡ₑ r # C) ->
     (r≡ₑq#C : r ≡ₑ q # C) ->
    -----------------------
      p ≡ₑ q # C

  ≡ₑsymm : ∀ {p q C BVq FVq} ->

     (CBq : CorrectBinding (C ⟦ q ⟧c) BVq FVq) ->
     (q≡ₑp : q ≡ₑ p # C) ->
    -------------------------------------------
      p ≡ₑ q # C

  ≡ₑctxt : ∀ {C C′ p q C′⟦p⟧ C′⟦q⟧ } ->

     (C′⟦p⟧≐C′⟦p⟧c : C′⟦p⟧ ≐ C′ ⟦ p ⟧c) ->
     (C′⟦q⟧≐C′⟦q⟧c : C′⟦q⟧ ≐ C′ ⟦ q ⟧c) ->
     (p≡ₑq : p ≡ₑ q # (C ++ C′)) ->
    -----------------------------------
     C′⟦p⟧ ≡ₑ C′⟦q⟧ # C

  ≡ₑstep : ∀ {C p q} ->

     (p⟶₁q : p ⟶₁ q) ->
    --------------------
     p ≡ₑ q # C

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
data I : Set where
  i : I

variable
  x : I

abstract

  data D : I → Set where
    d : D i

  accepted : {x : I} → D x → Set₁
  accepted {x = i} d = Set

  rejected : D x → Set₁
  rejected {x = i} d = Set


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

module Cham.Molecule where

open import Cham.Agent
open import Cham.Context
open import Cham.Label
open import Cham.Name
open import Data.List
open import Data.Product using (_×_)

data Molecule : Context → Set₁ where
  Reagent : ∀ {Γ} → Agent Γ → Molecule Γ

  _·ₘ_    : ∀ {Γ}
          → (Valence : Label)
          → Molecule Γ
          → Molecule (Γ ⊢ Valence)

  _∣ₘ_    : ∀ {Γ₁ Γ₂}
          → Molecule Γ₁
          → Molecule Γ₂
          → Molecule (Γ₁ , Γ₂)

  _/ₘ_    : ∀ {Γ}
          → (Ion : Name)
          → Molecule Γ
          → Molecule (Γ ⊢ Ion ⁻)

  ⟨_,_⟩   : ∀ {Γ₁ Γ₂}
          → Molecule Γ₁
          → Molecule Γ₂
          → Molecule (Γ₁ , Γ₂)

  l∶⟨_,_⟩  : ∀ {Γ₁ Γ₂}
          → Molecule (Γ₁ , Γ₂)
          → Molecule Γ₁

  r∶⟨_,_⟩  : ∀ {Γ₁ Γ₂}
          → Molecule (Γ₁ , Γ₂)
          → Molecule Γ₂

  -- molecular solutions
  Sol     : ∀ {Γ₁ Γ₂}
          → Molecule Γ₁
          → Molecule Γ₂
          → Molecule (permeate Γ₁ Γ₂)


text:
module Using where

module Dummy where
  data DummySet1 : Set where ds1 : DummySet1
  data DummySet2 : Set where ds2 : DummySet2

open Dummy
  using (DummySet1)

open Dummy -- checking that newline + comment is allowed before "using"
  using (DummySet2)

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
-- Testcase for #2028 by Ulf

record ⊤ : Set where
  constructor tt

data Either (A B : Set) : Set where
  inl : A → Either A B
  inr : B → Either A B

Subset : Set → Set₁
Subset X = X → Set

U : ∀ {X} → Subset X
U _ = {!⊤!}

_⊆_ : ∀ {X} → Subset X → Subset X → Set
A ⊆ B = ∀ {x} → A x → B x

_∪_ : ∀ {X} → Subset X → Subset X → Subset X
(A ∪ B) x = Either (A x) (B x)

∪-bound : ∀ {X} {A : Subset X} → (A ∪ U) ⊆ U
∪-bound {X} {A} = aux
  where
    aux : _ → _
    aux (inl _) = tt
    aux (inr tt) = tt