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

{-
  Ribbon is the explicit covering space construction.

  This construction is given by Daniel Grayson, Favonia (me)
  and Guillaume Brunerie together.
-}

open import Base
open import Homotopy.Pointed

-- A is the pointed base space.
-- Y is intended to be a (group-)set,
-- but can be an arbitrarily weird space.
module Homotopy.Cover.Ribbon {i} (A⋆ : pType i) {Y : Set i} where
  open pType A⋆ renaming (∣_∣ to A ; ⋆ to a)

  open import Homotopy.Truncation
  open import Homotopy.PathTruncation
  open import Homotopy.HomotopyGroups
  open import Algebra.GroupSets (fundamental-group A⋆)

  -- The HIT ribbon---reconstructed covering space
  private
    module Ribbon {act : action Y} where
      open action act

      private
        data #ribbon (a₂ : A) : Set i where
          #trace : Y →  a ≡₀ a₂ → #ribbon a₂

      ribbon : A → Set i
      ribbon = #ribbon

      -- A point in the fiber a₂.
      {-
        y is a point in the fiber a, and
        p is a path to transport y to fiber a₂.
      -}
      trace : ∀ {a₂} → Y → a ≡₀ a₂ → ribbon a₂
      trace = #trace

      {-
        A loop based at a can used as a group action
        or for concatination.  Both should be equivalent.

        And after pasting, make the type fiberwise a set.
      -}
      postulate -- HIT
        paste : ∀ {a₂} y loop (p : a ≡₀ a₂)
          → trace (y ∙ loop) p ≡ trace y (loop ∘₀ p)
        ribbon-is-set : ∀ a₂ → is-set (ribbon a₂)

      -- Standard dependent eliminator
      ribbon-rec : ∀ a₂ {j} (P : ribbon a₂ → Set j)
        ⦃ P-is-set : ∀ r → is-set (P r) ⦄
        (trace* : ∀ y p → P (trace y p))
        (paste* : ∀ y loop p → transport P (paste y loop p) (trace* (y ∙ loop) p)
                             ≡ trace* y (loop ∘₀ p))
        → (∀ r → P r)
      ribbon-rec a₂ P trace* paste* (#trace y p) = trace* y p

      -- Standard non-dependent eliminator
      ribbon-rec-nondep : ∀ a₂ {j} (P : Set j)
        ⦃ P-is-set : is-set P ⦄
        (trace* : ∀ (y : Y) (p : a ≡₀ a₂) → P)
        (paste* : ∀ y (loop : a ≡₀ a) p → trace* (y ∙ loop) p ≡ trace* y (loop ∘₀ p))
        → (ribbon a₂ → P)
      ribbon-rec-nondep a₂ P trace* paste* (#trace y p) = trace* y p

  open Ribbon public hiding (ribbon)

  module _ (act : action Y) where

    ribbon : A → Set i
    ribbon = Ribbon.ribbon {act}

    trans-trace : ∀ {a₁ a₂} (q : a₁ ≡ a₂) y p
      → transport ribbon q (trace y p) ≡ trace y (p ∘₀ proj q)
    trans-trace refl y p = ap (trace y) $ ! $ refl₀-right-unit p

max_stars_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------------
-- ABP Lemma 1
------------------------------------------------------------------------------

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

-- From Dybjer and Sander's paper: The first lemma states that given a
-- start state S of the ABP, we will arrive at a state S', where the
-- message has been received by the receiver, but where the
-- acknowledgement has not yet been received by the sender.

module FOT.FOTC.Program.ABP.Lemma1NoHelperATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.Loop
open import FOTC.Data.Bool
open import FOTC.Data.Bool.PropertiesATP using ( x≢not-x )
open import FOTC.Data.List
open import FOTC.Program.ABP.ABP
open import FOTC.Program.ABP.Fair.Type
open import FOTC.Program.ABP.Fair.PropertiesATP
open import FOTC.Program.ABP.Terms

------------------------------------------------------------------------------
-- 30 November 2013. If we don't have the following definitions
-- outside, the ATPs cannot prove the theorems.

as^ : ∀ b i' is' ds → D
as^ b i' is' ds = await b i' is' ds
{-# ATP definition as^ #-}

bs^ : D → D → D → D → D → D
bs^ b i' is' ds os₁^ = corrupt os₁^ · (as^ b i' is' ds)
{-# ATP definition bs^ #-}

cs^ : D → D → D → D → D → D
cs^ b i' is' ds os₁^ = ack b · (bs^ b i' is' ds os₁^)
{-# ATP definition cs^ #-}

ds^ : D → D → D → D → D → D → D
ds^ b i' is' ds os₁^ os₂^ = corrupt os₂^ · cs^ b i' is' ds os₁^
{-# ATP definition ds^ #-}

os₁^ : D → D → D
os₁^ os₁' ft₁^ = ft₁^ ++ os₁'
{-# ATP definition os₁^ #-}

os₂^ : D → D
os₂^ os₂ = tail₁ os₂
{-# ATP definition os₂^ #-}

------------------------------------------------------------------------------
-- From Dybjer and Sander's paper: From the assumption that os₁ ∈ Fair
-- and hence by unfolding Fair, we conclude that there are ft₁ :  F*T
-- and os₁' : Fair, such that os₁ = ft₁ ++ os₁'.
--
-- We proceed by induction on ft₁ : F*T using helper.

-- 26 January 2014. Pattern matching after a @with@ it is not accepted
-- by the termination checker. See Agda issue 59, comment 18.

{-# TERMINATING #-}
lemma₁ : ∀ b i' is' os₁ os₂ as bs cs ds js →
         Bit b →
         Fair os₁ →
         Fair os₂ →
         S b (i' ∷ is') os₁ os₂ as bs cs ds js →
         ∃[ os₁' ] ∃[ os₂' ] ∃[ as' ] ∃[ bs' ] ∃[ cs' ] ∃[ ds' ] ∃[ js' ]
           Fair os₁'
           ∧ Fair os₂'
           ∧ S' b i' is' os₁' os₂' as' bs' cs' ds' js'
           ∧ js ≡ i' ∷ js'
lemma₁ b i' is' os₁ os₂ as bs cs ds js Bb Fos₁ Fos₂ s with Fair-out Fos₁
... | .(true ∷ []) , os₁' , f*tnil , os₁≡ft₁++os₁' , Fos₁' = prf
  where
  postulate
    prf : ∃[ os₁' ] ∃[ os₂' ] ∃[ as' ] ∃[ bs' ] ∃[ cs' ] ∃[ ds' ] ∃[ js' ]
            Fair os₁'
            ∧ Fair os₂'
            ∧ (as' ≡ await b i' is' ds'
              ∧ bs' ≡ corrupt os₁' · as'
              ∧ cs' ≡ ack (not b) · bs'
              ∧ ds' ≡ corrupt os₂' · (b ∷ cs')
              ∧ js' ≡ out (not b) · bs')
            ∧ js ≡ i' ∷ js'
  {-# ATP prove prf #-}

... | .(F ∷ ft₁^) , os₁' , f*tcons {ft₁^} FTft₁ , os₁≡ft₁++os₁' , Fos₁' =
  lemma₁ b i' is'
         (ft₁^ ++ os₁')
         (tail₁ os₂)
         (await b i' is' ds)
         (corrupt (ft₁^ ++ os₁') · await b i' is' ds)
         (ack b · (corrupt (ft₁^ ++ os₁') · await b i' is' ds))
         (corrupt (tail₁ os₂) ·
           (ack b · (corrupt (ft₁^ ++ os₁') · await b i' is' ds)))
         js Bb (Fair-in (ft₁^ , os₁' , FTft₁ , refl , Fos₁')) (tail-Fair Fos₂) ihS
     where
     postulate os₁-eq-helper : os₁ ≡ F ∷ os₁^ os₁' ft₁^
     {-# ATP prove os₁-eq-helper #-}

     postulate as-eq : as ≡ < i' , b > ∷ (as^ b i' is' ds)
     {-# ATP prove as-eq #-}

     postulate bs-eq : bs ≡ error ∷ (bs^ b i' is' ds (os₁^ os₁' ft₁^))
     {-# ATP prove bs-eq os₁-eq-helper as-eq #-}

     postulate cs-eq : cs ≡ not b ∷ cs^ b i' is' ds (os₁^ os₁' ft₁^)
     {-# ATP prove cs-eq bs-eq #-}

     postulate ds-eq : ds ≡ ok (not b) ∷ ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂)
                  ∨ ds ≡ error ∷ ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂)
     {-# ATP prove ds-eq head-tail-Fair cs-eq #-}

     postulate
       as^-eq-helper₁ :
         ds ≡ ok (not b) ∷ ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂) →
         as^ b i' is' ds ≡
           send b · (i' ∷ is') · ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂)
     {-# ATP prove as^-eq-helper₁ x≢not-x #-}

     postulate
       as^-eq-helper₂ :
         ds ≡ error ∷ ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂) →
         as^ b i' is' ds ≡
           send b · (i' ∷ is') · ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂)
     {-# ATP prove as^-eq-helper₂ #-}

     as^-eq : as^ b i' is' ds ≡
              send b · (i' ∷ is') · ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂)
     as^-eq = case as^-eq-helper₁ as^-eq-helper₂ ds-eq

     postulate js-eq : js ≡ out b · bs^ b i' is' ds (os₁^ os₁' ft₁^)
     {-# ATP prove js-eq bs-eq #-}

     ihS : S b
             (i' ∷ is')
             (os₁^ os₁' ft₁^)
             (os₂^ os₂)
             (as^ b i' is' ds)
             (bs^ b i' is' ds (os₁^ os₁' ft₁^))
             (cs^ b i' is' ds (os₁^ os₁' ft₁^))
             (ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂))
             js
     ihS = as^-eq , refl , refl , refl , js-eq

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- A virtual machine
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --sized-types #-}

module Lambda.Partiality-monad.Inductive.Virtual-machine where

open import Prelude hiding (⊥)

open import Partiality-monad.Inductive

open import Lambda.Syntax
open import Lambda.Virtual-machine

open Closure Code

-- A functional semantics for the VM.
--
-- For an alternative definition, see the semantics in
-- Lambda.Simplified.Partiality-monad.Inductive.Virtual-machine, which
-- is defined using a fixpoint combinator.

steps : State → ℕ → Maybe Value ⊥
steps s n       with step s
steps s zero    | continue s′ = never
steps s (suc n) | continue s′ = steps s′ n
steps s n       | done v      = now (just v)
steps s n       | crash       = now nothing

steps-increasing : ∀ s n → steps s n ⊑ steps s (suc n)
steps-increasing s n       with step s
steps-increasing s zero    | continue s′ = never⊑ _
steps-increasing s (suc n) | continue s′ = steps-increasing s′ n
steps-increasing s n       | done v      = ⊑-refl _
steps-increasing s n       | crash       = ⊑-refl _

stepsˢ : State → Increasing-sequence (Maybe Value)
stepsˢ s = (steps s , steps-increasing s)

exec : State → Maybe Value ⊥
exec s = ⨆ (stepsˢ s)

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module Cats.Category.Constructions.Initial where

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

open import Cats.Category.Base

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

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

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

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

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

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

  Initial⇒X-unique : ∀ {Zero} → IsInitial Zero → ∀ {X} {f g : Zero ⇒ X} → f ≈ g
  Initial⇒X-unique init {X} {f} {g} with init X
  ... | ∃!-intro x _ x-uniq = ≈.trans (≈.sym (x-uniq _)) (x-uniq _)

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

  field
    Zero : Obj
    isInitial : IsInitial Zero

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Functor.Limits where

open import Level

open import Categories.Category
open import Categories.Functor
open import Categories.Functor.Properties
open import Categories.Object.Terminal
open import Categories.Object.Initial

open import Categories.Diagram.Limit
open import Categories.Diagram.Colimit
open import Categories.Diagram.Cone.Properties
open import Categories.Diagram.Cocone.Properties

open import Categories.Category.Construction.Cones
open import Categories.Category.Construction.Cocones

private
  variable
    o ℓ e : Level
    𝒞 𝒟 ℐ : Category o ℓ e

module _ (F : Functor 𝒞 𝒟) {J : Functor ℐ 𝒞} where

  PreservesLimit : (L : Limit J) → Set _
  PreservesLimit L = IsTerminal (Cones (F ∘F J)) (F-map-Coneˡ F limit)
    where open Limit L

  PreservesColimit : (L : Colimit J) → Set _
  PreservesColimit L = IsInitial (Cocones (F ∘F J)) (F-map-Coconeˡ F colimit)
    where open Colimit L

  ReflectsLimits : Set _
  ReflectsLimits = ∀ (K : Cone J) → IsTerminal (Cones (F ∘F J)) (F-map-Coneˡ F K) → IsTerminal (Cones J) K

  ReflectsColimits : Set _
  ReflectsColimits = ∀ (K : Cocone J) → IsInitial (Cocones (F ∘F J)) (F-map-Coconeˡ F K) → IsInitial (Cocones J) K

--   record CreatesLimits : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′ ⊔ o″ ⊔ ℓ″) where
--     field
--       preserves-limits : PreservesLimit
--       reflects-limits  : ReflectsLimits

--   record CreatesColimits : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′ ⊔ o″ ⊔ ℓ″) where
--     field
--       preserves-colimits : PreservesColimit
--       reflects-colimits  : ReflectsColimits

Continuous : ∀ o ℓ e → (F : Functor 𝒞 𝒟) → Set _
Continuous {𝒞 = 𝒞} o ℓ e F = ∀ {𝒥 : Category o ℓ e} {J : Functor 𝒥 𝒞} (L : Limit J) → PreservesLimit F L

Cocontinuous : ∀ o ℓ e → (F : Functor 𝒞 𝒟) → Set _
Cocontinuous {𝒞 = 𝒞} o ℓ e F = ∀ {𝒥 : Category o ℓ e} {J : Functor 𝒥 𝒞} (L : Colimit J) → PreservesColimit F L

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import LogicalFormulae
open import Maybe
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

open import Numbers.Naturals.Semiring

module KeyValue.KeyValue {a b : _} (keys : Set a) (values : Set b) where

record KeyValue {c : _} (maps : Set c) : Set (a ⊔ b ⊔ c) where
  field
    tryFind : maps → keys → Maybe values
    add : (map : maps) → keys → values → maps
    empty : maps
    count : maps → ℕ
    lookupAfterAdd : (map : maps) → (k : keys) → (v : values) → tryFind (add map k v) k ≡ yes v
    lookupAfterAdd' : (map : maps) → (k1 : keys) → (v : values) → (k2 : keys) → (k1 ≡ k2) || (tryFind (add map k1 v) k2 ≡ tryFind map k2)
    countAfterAdd' : (map : maps) → (k : keys) → (v : values) → (tryFind map k ≡ no) → count (add map k v) ≡ succ (count map)
    countAfterAdd : (map : maps) → (k : keys) → (v1 v2 : values) → (tryFind map k ≡ yes v2) → count (add map k v1) ≡ count map


text:
module TerminationArgumentSwapping where

-- subtyping simple types

data Bool : Set where
   true  : Bool
   false : Bool

_&&_ : Bool -> Bool -> Bool
true && a = a
false && a = false

data Ty : Set where
   bot : Ty
   top : Ty
   arr : Ty -> Ty -> Ty

subty : Ty -> Ty -> Bool
subty bot _ = true
subty _ top = true
subty (arr a b) (arr a' b') = subty a' a && subty b b'
subty _ _ = false

-- maximum with happy swapping

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

-- Maximum of 3 numbers

max3 : Nat -> Nat -> Nat -> Nat
max3 zero zero z = z
max3 zero y zero = y
max3 x zero zero = x
max3 (succ x) (succ y) zero = succ (max3 x y zero)
max3 (succ x) zero (succ z) = succ (max3 x z zero)
max3 zero (succ y) (succ z) = succ (max3 y z zero)
max3 (succ x) (succ y) (succ z) = succ (max3 z x y)

-- can also be done with sized types
-- max3 : Nat^i -> Nat^i -> Nat^i -> Nat^i

-- swapping with higher-order datatypes

data Ord : Set where
   ozero : Ord
   olim  : (Nat -> Ord) -> Ord

foo : Ord -> (Nat -> Ord) -> Ord
foo ozero    g = ozero
foo (olim f) g = olim (\n -> foo (g n) f)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Typed.LTLCRef where

open import Data.List.Relation.Ternary.Interleaving.Propositional
open import Relation.Unary hiding (_∈_)
open import Relation.Unary.PredicateTransformer using (Pt)
open import Function
open import Category.Monad

open import Relation.Ternary.Separation
open import Relation.Ternary.Separation.Allstar
open import Relation.Ternary.Separation.Morphisms
open import Relation.Ternary.Separation.Monad
open import Relation.Ternary.Separation.Monad.Reader

open import Prelude

data Ty : Set where
  unit : Ty
  ref  : Ty → Ty
  prod : Ty → Ty → Ty
  _⊸_  : (a b : Ty) → Ty

Ctx  = List Ty
CtxT = List Ty → List Ty

open import Relation.Ternary.Separation.Construct.List Ty
open import Relation.Ternary.Separation.Construct.Market
open import Relation.Ternary.Separation.Construct.Product

infixr 20 _◂_
_◂_ : Ty → CtxT → CtxT
(x ◂ f) Γ = x ∷ f Γ

variable a b c : Ty
variable ℓv  : Level
variable τ   : Set ℓv
variable Γ Γ₁ Γ₂ Γ₃ : List τ

data Exp : Ty → Ctx → Set where
  -- base type
  tt       : ε[ Exp unit ]
  letunit  : ∀[ Exp unit ✴ Exp a ⇒ Exp a ]

  -- linear λ calculus
  var      : ∀[ Just a ⇒ Exp a ]
  lam      : ∀[ (a ◂ id ⊢ Exp b) ⇒ Exp (a ⊸ b) ]
  ap       : ∀[ Exp (a ⊸ b) ✴ Exp a ⇒ Exp b ]

  -- products
  pair    : ∀[ Exp a ✴ Exp b ⇒ Exp (prod a b) ]
  letpair : ∀[ Exp (prod a b) ✴ (λ Γ → a ∷ b ∷ Γ) ⊢ Exp c ⇒ Exp c ]

  -- state
  ref     : ε[ Exp a ⇒ Exp (ref a) ]
  swaps   : ∀[ Exp (ref a) ✴ Exp b ⇒ Exp (prod a (ref b)) ]
  del     : ε[ Exp (ref unit) ⇒ Exp unit ]

-- store types
ST = List Ty

-- values
data Val : Ty → Pred ST 0ℓ where
  tt    : ε[ Val unit ]
  clos  : Exp b (a ∷ Γ) → ∀[ Allstar Val Γ ⇒ Val (a ⊸ b) ]
  ref   : ∀[ Just a ⇒ Val (ref a) ]
  pair  : ∀[ Val a ✴ Val b ⇒ Val (prod a b) ]

{- The 'give-it-to-me-straight' semantics -}

Store : ST → ST → Set
Store = Allstar Val

-- {- First attempt -- evaluation without a frame, seems simple enough... -}
-- eval₁ : ∀ {Ψ Γ} → Exp a Γ → Allstar Val Γ Φ₁ → Store Ψ Φ₂ → Φ₁ ⊎ Φ₂ ≣ Ψ →
--         ∃ λ Ψ' → ∃₂ λ Φ₃ Φ₄ → Store Ψ' Φ₃ × Val a Φ₄ × Φ₃ ⊎ Φ₄ ≣ Ψ'

-- eval₁ (num x) nil μ σ = -, -, -, μ , num x , ⊎-comm σ

-- eval₁ (lam e) env μ σ = -, -, -, μ , (clos e env) , ⊎-comm σ

-- eval₁ (ap (f ×⟨ σ ⟩ e)) env μ σ₂ =
--   let
--     env₁ ×⟨ σ₃ ⟩ env₂ = repartition σ env
--     _ , τ₁ , τ₂ = ⊎-assoc (⊎-comm σ₃) σ₂

--   {- Oops, store contains more stuff than used; i.e. we have a frame -}
--   in case eval₁ f env₁ μ {!τ₂!} of λ where
--     (_ , _ , _ , μ' , clos e env₃ , σ₄) → {!!}

-- eval₁ (var x) = {!!}

-- eval₁ (ref e) = {!!}

-- eval₁ (deref e) = {!!}

-- eval₁ (asgn x) = {!!}

-- {- First attempt -- evaluation *with* a frame. Are you sure want this? -}
-- eval₂ : ∀ {Ψ Γ Φf} → Exp a Γ → Allstar Val Γ Φ₁ → Store Ψ Φ₂ → Φ₁ ⊎ Φ₂ ≣ Φ → Φ ⊎ Φf ≣ Ψ →
--         ∃₂ λ Φ' Ψ' → ∃₂ λ Φ₃ Φ₄ → Store Ψ' Φ₃ × Val a Φ₄ × Φ₃ ⊎ Φ₄ ≣ Φ' × Φ' ⊎ Φf ≣ Ψ'
-- eval₂ (num x) nil μ σ₁ σ₂ =
--   case ⊎-id⁻ˡ σ₁ of λ where refl → -, -, -, -, μ , num x , ⊎-idʳ , σ₂
-- eval₂ (lam x) env μ σ₁ σ₂ = {!!}

-- eval₂ (pair (e₁ ×⟨ σ ⟩ e₂)) env μ σ₁ σ₂ =
--   let
--     env₁ ×⟨ σ₃ ⟩ env₂ = repartition σ env
--     _ , τ₁ , τ₂ = ⊎-assoc (⊎-comm σ₃) σ₁ -- separation between sub-env and store
--     _ , τ₃ , τ₄ = ⊎-assoc (⊎-comm τ₁) σ₂ -- compute the frame

--   in case eval₂ e₁ env₁ μ τ₂ τ₃ of λ where
--     (_ , _ , _ , _ , μ' , v₁ , σ₄ , σ₅) →
--        let v = eval₂ e₂ env₂ μ' {!τ₁!} {!!} in {!!}

-- eval₂ (var x) env μ σ₁ σ₂ = {!!}
-- eval₂ (ref e) env μ σ₁ σ₂ = {!!}
-- eval₂ (deref e) env μ σ₁ σ₂ = {!!}
-- eval₂ (asgn x) env μ σ₁ σ₂ = {!!}
-- eval₂ (ap (f ×⟨ σ ⟩ e)) env μ σ₁ σ₂ = {!!}

{- The monadic semantics -}

module _ {i : Size} where
  open import Relation.Ternary.Separation.Monad.Delay public
  open import Relation.Ternary.Separation.Monad.State
  open import Relation.Ternary.Separation.Monad.State.Heap Val

  open HeapOps (Delay i) {{ monad = delay-monad }}
    using (state-monad; newref; read; write; Cells)
    public

  open ReaderTransformer id-morph Val (StateT (Delay i) Cells)
    {{ monad = state-monad }}
    renaming (Reader to M'; reader-monad to monad)
    public

  open Monads.Monad monad public
  open Monads using (_&_; str; typed-str) public

M : Size → (Γ₁ Γ₂ : Ctx) → Pt ST 0ℓ
M i = M' {i}

mutual
  eval⊸ : ∀ {i Γ} → Exp (a ⊸ b) Γ → ∀[ Val a ⇒ M i Γ ε (Val b) ]
  eval⊸ e v = do
    clos e env ×⟨ σ₂ ⟩ v ← ►eval e & v
    empty                ← append (cons (v ×⟨ ⊎-comm σ₂ ⟩ env))
    ►eval e

  eval : ∀ {i Γ} → Exp a Γ → ε[ M i Γ ε (Val a) ]

  eval tt = do
    return tt

  eval (letunit (e₁ ×⟨ Γ≺ ⟩ e₂)) = do
    tt ← frame Γ≺ (►eval e₁)
    ►eval e₂

  eval (var refl) = do
    lookup

  eval (lam e) = do
    env ← ask
    return (clos e env)

  eval (pair (e₁ ×⟨ Γ≺ ⟩ e₂)) = do
    v₁    ← frame Γ≺ (►eval e₁)
    v₂✴v₁ ← ►eval e₂ & v₁
    return (pair (✴-swap v₂✴v₁))

  eval (letpair (e₁ ×⟨ Γ≺ ⟩ e₂)) = do
    pair (v₁ ×⟨ σ ⟩ v₂) ← frame Γ≺ (►eval e₁)
    empty               ← prepend (cons (v₁ ×⟨ σ ⟩ (singleton v₂)))
    ►eval e₂

  eval (ap (f ×⟨ Γ≺ ⟩ e)) = do
    v ← frame (⊎-comm Γ≺) (►eval e)
    eval⊸ f v

  eval (ref e) = do
    v ← ►eval e
    r ← liftM (newref v)
    return (ref r)

  eval (swaps (e₁ ×⟨ Γ≺ ⟩ e₂)) = do
    ref ra ← frame Γ≺ (►eval e₁)
    vb ×⟨ σ₁ ⟩ ra ← ►eval e₂ & ra
    rb ×⟨ σ₂ ⟩ va ← liftM (write (ra ×⟨ ⊎-comm σ₁ ⟩ vb))
    return (pair (va ×⟨ (⊎-comm σ₂) ⟩ (ref rb)))

  eval (del e) = do
    ref r ← ►eval e
    liftM (read r)

  ►eval : ∀ {i Γ} → Exp a Γ → ε[ M i Γ ε (Val a) ]
  app (app (►eval e) env σ) μ σ' = later (λ where .force → app (app (eval e) env σ) μ σ')


text:
{- 2010-09-28 Andreas, see issue 336 -}

module WhyWeNeedUntypedLambda where

IdT = ({A : Set} -> A -> A)

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

-- Untyped lambda succeeds, because checking \ x -> x : X is postponed,
-- then the solution X = IdT is found, and upon revisiting the tc problem
-- a hidden lambda \ {A} is inserted.
foo : ({X : Set1} -> X -> X == IdT -> Set) -> Set
foo k = k (\ x -> x) refl         -- succeeds

{-
-- Typed lambda fails, because \ (x : _) -> x has inferred type ?A -> ?A
-- but then unification with IdT fails.
foo' : ({X : Set1} -> X -> X == IdT -> Set) -> Set
foo' k = k (\ (x : _) -> x) refl  -- fails
-}

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
------------------------------------------------------------------------
-- The parser data type
------------------------------------------------------------------------

-- This hybrid variant is coinductive /and/ includes !_.

module RecursiveDescent.Hybrid.Type where

open import Data.Bool
open import Data.Product.Record

open import RecursiveDescent.Index

-- A type for parsers which can be implemented using recursive
-- descent. The types used ensure that the implemented backends are
-- structurally recursive.

-- The parsers are indexed on a type of nonterminals.

codata Parser (tok : Set) (nt : ParserType) : ParserType₁ where
  !_     :  forall {e c r}
         -> nt (e , c) r -> Parser tok nt (e , step c) r
  symbol :  Parser tok nt (false , leaf) tok
  return :  forall {r} -> r -> Parser tok nt (true , leaf) r
  fail   :  forall {r} -> Parser tok nt (false , leaf) r
  _?>>=_ :  forall {c₁ e₂ c₂ r₁ r₂}
         -> Parser tok nt (true , c₁) r₁
         -> (r₁ -> Parser tok nt (e₂ , c₂) r₂)
         -> Parser tok nt (e₂ , node c₁ c₂) r₂
  _!>>=_ :  forall {c₁ r₁ r₂} {i₂ : r₁ -> Index}
         -> Parser tok nt (false , c₁) r₁
         -> ((x : r₁) -> Parser tok nt (i₂ x) r₂)
         -> Parser tok nt (false , step c₁) r₂
  alt    :  forall e₁ e₂ {c₁ c₂ r}
         -> Parser tok nt (e₁      , c₁)         r
         -> Parser tok nt (e₂      , c₂)         r
         -> Parser tok nt (e₁ ∨ e₂ , node c₁ c₂) r

-- Grammars.

Grammar : Set -> ParserType -> Set1
Grammar tok nt = forall {i r} -> nt i r -> Parser tok nt i r

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------------
-- No theorem used by the shelltestrunner test
------------------------------------------------------------------------------

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

module NoTheorem where

postulate
  D   : Set
  _≡_ : D → D → Set
  a b : D

postulate foo : a ≡ b
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Categories.SubCategory where

open import Categories.Category
open import Data.Product

sub-category : ∀ {o ℓ e o′ ℓ′} -> (C : Category o ℓ e) -> let module C = Category C in
               {A : Set o′} (U : A -> C.Obj) (R : ∀ {a b} -> U a C.⇒ U b -> Set ℓ′) ->
               (∀ {a} -> R (C.id {U a})) -> (∀ {a b c} {f : U b C.⇒ U c} {g : U a C.⇒ U b} -> R f -> R g -> R (f C.∘ g)) →
               Category _ _ _
sub-category C {A} U R Rid R∘ = record
  { Obj = A
  ; _⇒_ = λ a b → Σ (U a C.⇒ U b) R
  ; _≡_ = λ f g → proj₁ f C.≡ proj₁ g
  ; id = C.id , Rid
  ; _∘_ = λ f g → (proj₁ f C.∘ proj₁ g) , R∘ (proj₂ f) (proj₂ g)
  ; assoc = C.assoc
  ; identityˡ = C.identityˡ
  ; identityʳ = C.identityʳ
  ; equiv = record
      { refl = C.Equiv.refl
      ; sym = C.Equiv.sym
      ; trans = C.Equiv.trans
      }
  ; ∘-resp-≡ = C.∘-resp-≡
  }
  where
    module C = Category C

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module EtaAndMetas where

record Functor : Set₁ where
  field
    F : Set → Set

eta : Functor → Functor
eta S = record { F = F }
  where open Functor S

postulate
  Π   : (To : Functor) → Set
  mkΠ : (B : Functor) → Π (eta B)
  To  : Functor

π : Π (eta To)
π = mkΠ _

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Integer12 where

open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥)
open import Data.Bool using (Bool; true; false)
open import Relation.Binary.PropositionalEquality
  as PropEq using (_≡_; refl; cong; cong₂; sym)

isTrue : Bool → Set
isTrue true = ⊤
isTrue false = ⊥

-- 整数のガチな定義
--（succ (succ (pred zero))などはもうできない）
mutual
  data ℤ : Set where
    zero : ℤ
    succ : (x : ℤ) → isTrue (zeroOrSucc x) → ℤ
    pred : (x : ℤ) → isTrue (zeroOrPred x) → ℤ

  zeroOrSucc : ℤ → Bool
  zeroOrSucc zero = true
  zeroOrSucc (succ x p) = true
  zeroOrSucc (pred x p) = false
  zeroOrPred : ℤ → Bool
  zeroOrPred zero = true
  zeroOrPred (succ x p) = false
  zeroOrPred (pred x p) = true
-- succ (succ zero tt) tt のように使う

postulate -- ここだけ
  ttxS : (x : ℤ) → (isTrue (zeroOrSucc x))
  ttxP : (x : ℤ) → (isTrue (zeroOrPred x))
  succPred :
    (x : ℤ)(px : isTrue (zeroOrPred x))(px2 : isTrue (zeroOrSucc (pred x px)))
      → succ (pred x px) px2 ≡ x
  predSucc :
    (x : ℤ)(px : isTrue (zeroOrSucc x))(px2 : isTrue (zeroOrPred (succ x px)))
      → pred (succ x px) px2 ≡ x
  pxToTtxS : (x : ℤ)(px : isTrue (zeroOrSucc x)) → px ≡ ttxS x
  pyToTtxP : (y : ℤ)(py : isTrue (zeroOrPred y)) → py ≡ ttxP y
  myCong₂S : {x y : ℤ}{u : ⊤}{v : ⊤}
    → x ≡ y → u ≡ v → succ x (ttxS x) ≡ succ y (ttxS y)
  myCong₂P : {x y : ℤ}{u : ⊤}{v : ⊤}
    → x ≡ y → u ≡ v → pred x (ttxP x) ≡ pred y (ttxP y)
  myCong₂ : {A : Set}(x y : A){B : Set}{C : Set}(f : A → B → C){u v : B} →
              x ≡ y → u ≡ v → f x u ≡ f y v

infixl 40 _+_
infixl 60 _*_

-- 加法
_+_ : ℤ → ℤ → ℤ
zero + y = y
succ x px + zero = succ x px
succ x px + succ y py
  = let z = succ x px + y in succ z (ttxS z)
succ x _ + pred y _ = x + y
pred x px + zero = pred x px
pred x _ + succ y _ = x + y
pred x px + pred y py
  = let z = pred x px + y in pred z (ttxP z)

-- 反数
opposite : ℤ → ℤ
opposite zero = zero
opposite (succ x px) = pred (opposite x) (ttxP (opposite x))
opposite (pred x px) = succ (opposite x) (ttxS (opposite x))

-- 乗法
_*_ : ℤ → ℤ → ℤ
x * zero = zero
x * succ y py = (x * y) + x
x * pred y py = (x * y) + (opposite x)

-- (-1) * (-1) = 1
-1*-1≡1 : pred zero tt * pred zero tt ≡ succ zero tt
-1*-1≡1 = refl
-- 2 * (-3) = (-6)
2*-3≡-6 :
  succ (succ zero tt) tt * pred (pred (pred zero tt) tt) tt
    ≡ pred (pred (pred (pred (pred (pred zero tt) tt) tt) tt) tt) tt
2*-3≡-6 = refl

-- 雑多な定理
-- 右から0を足しても変わらない
x+zero≡x : (x : ℤ) → x + zero ≡ x
x+zero≡x zero = refl
x+zero≡x (succ _ _) = refl
x+zero≡x (pred _ _) = refl

-- ユーティリティ
mutual
  succOut1 : (x y : ℤ)(px : isTrue (zeroOrSucc x))
    → succ x px + y ≡ succ (x + y) (ttxS (x + y))
  succOut1 x zero px rewrite x+zero≡x x | pxToTtxS x px = refl
  succOut1 x (succ y py) px rewrite succOut1 x y px | succOut2 x y py = refl
  succOut1 x (pred y py) _ rewrite predOut2 x y py
                                 | succPred (x + y) (ttxP (x + y))
      (ttxS (pred (x + y) (ttxP (x + y)))) = refl
  succOut2 : (x y : ℤ)(py : isTrue (zeroOrSucc y))
    → x + succ y py ≡ succ (x + y) (ttxS (x + y))
  succOut2 zero y py rewrite pxToTtxS y py = refl
  succOut2 (succ x px) y py = refl
  succOut2 (pred x px) y py rewrite predOut1 x y px
                                  | succPred (x + y) (ttxP (x + y))
      (ttxS (pred (x + y) (ttxP (x + y)))) = refl
  predOut1 : (x y : ℤ)(px : isTrue (zeroOrPred x))
    → pred x px + y ≡ pred (x + y) (ttxP (x + y))
  predOut1 x zero px rewrite x+zero≡x x | pyToTtxP x px = refl
  predOut1 x (succ y py) px rewrite succOut2 x y py
                                  | predSucc (x + y) (ttxS (x + y))
      (ttxP (succ (x + y) (ttxS (x + y)))) = refl
  predOut1 x (pred y py) px rewrite predOut1 x y px
                                  | predOut2 x y py = refl
  predOut2 : (x y : ℤ)(py : isTrue (zeroOrPred y))
    → x + pred y py ≡ pred (x + y) (ttxP (x + y))
  predOut2 zero y py rewrite pyToTtxP y py = refl
  predOut2 (succ x px) y py rewrite succOut1 x y px
                                  | predSucc (x + y) (ttxS (x + y))
      (ttxP (succ (x + y) (ttxS (x + y)))) = refl
  predOut2 (pred x px) y py = refl

-- 結合法則
ℤ+-assoc : (x y z : ℤ) → (x + y) + z ≡ x + (y + z)
ℤ+-assoc zero y z = refl
ℤ+-assoc (succ x px) y z rewrite succOut1 x y px
                               | succOut1 (x + y) z (ttxS (x + y))
                               | succOut1 x (y + z) px
                               = myCong₂S (ℤ+-assoc x y z) refl
ℤ+-assoc (pred x px) y z rewrite predOut1 x y px
                               | predOut1 (x + y) z (ttxP (x + y))
                               | predOut1 x (y + z) px
                               = myCong₂P (ℤ+-assoc x y z) refl

-- 左分配法則
ℤdistL : (x y z : ℤ) → x * (y + z) ≡ (x * y) + (x * z)
ℤdistL x y zero rewrite x+zero≡x y | x+zero≡x (x * y) = refl
ℤdistL x y (succ z pz) rewrite succOut2 y z pz
                             | ℤdistL x y z
                             = ℤ+-assoc (x * y) (x * z) x
ℤdistL x y (pred z pz) rewrite predOut2 y z pz
                             | ℤdistL x y z
                             = ℤ+-assoc (x * y) (x * z) (opposite x)

-- oppositeの線形性
oppoLinear : (x y : ℤ) → opposite x + opposite y ≡ opposite (x + y)
oppoLinear x zero rewrite x+zero≡x (opposite x)
                        | x+zero≡x x = refl
oppoLinear x (succ y py) rewrite predOut2 (opposite x) (opposite y) (ttxP (opposite y))
                               | succOut2 x y py
                               = myCong₂P (oppoLinear x y) refl
oppoLinear x (pred y py) rewrite succOut2 (opposite x) (opposite y) (ttxS (opposite y))
                               | predOut2 x y py
                               = myCong₂S (oppoLinear x y) refl


text:
open import SOAS.Common
open import SOAS.Families.Core
open import Categories.Object.Initial
open import SOAS.Coalgebraic.Strength
import SOAS.Metatheory.MetaAlgebra

-- Monoids with ⅀-algebra structure
module SOAS.Metatheory.Monoid {T : Set}
  (⅀F : Functor 𝔽amiliesₛ 𝔽amiliesₛ) (⅀:Str : Strength ⅀F)
  where

open import SOAS.Context
open import SOAS.Variable
open import SOAS.Construction.Structure as Structure
open import SOAS.Abstract.Hom

open import SOAS.Abstract.Monoid

open import SOAS.Coalgebraic.Map
open import SOAS.Coalgebraic.Monoid

open import SOAS.Metatheory.Algebra {T} ⅀F

open Strength ⅀:Str

private
  variable
    Γ Δ : Ctx
    α : T

-- Family with compatible monoid and ⅀-algebra structure
record ΣMon (ℳ : Familyₛ) : Set where
  field
    ᵐ : Mon ℳ
    𝑎𝑙𝑔 : ⅀ ℳ ⇾̣ ℳ

  open Mon ᵐ public

  field
    μ⟨𝑎𝑙𝑔⟩ : {σ : Γ ~[ ℳ ]↝ Δ}(t : ⅀ ℳ α Γ)
          → μ (𝑎𝑙𝑔 t) σ ≡ 𝑎𝑙𝑔 (str ᴮ ℳ (⅀₁ μ t) σ)

record ΣMon⇒ {ℳ 𝒩 : Familyₛ}(ℳᴹ : ΣMon ℳ)(𝒩ᴹ : ΣMon 𝒩)
             (f : ℳ ⇾̣ 𝒩) : Set where
  private module ℳ = ΣMon ℳᴹ
  private module 𝒩 = ΣMon 𝒩ᴹ
  field
    ᵐ⇒ : Mon⇒ ℳ.ᵐ 𝒩.ᵐ f
    ⟨𝑎𝑙𝑔⟩ : {t : ⅀ ℳ α Γ} → f (ℳ.𝑎𝑙𝑔 t) ≡ 𝒩.𝑎𝑙𝑔 (⅀₁ f t)

  open Mon⇒ ᵐ⇒ public

-- Category of Σ-monoids
module ΣMonoidStructure = Structure 𝔽amiliesₛ ΣMon

ΣMonoidCatProps : ΣMonoidStructure.CategoryProps
ΣMonoidCatProps = record
  { IsHomomorphism = ΣMon⇒
  ; id-hom = λ {ℳ}{ℳᴹ} → record
    { ᵐ⇒ = AsMonoid⇒.ᵐ⇒ 𝕄on.id
    ; ⟨𝑎𝑙𝑔⟩ = cong (ΣMon.𝑎𝑙𝑔 ℳᴹ) (sym ⅀.identity)
    }
  ; comp-hom = λ{ {𝐸ˢ = 𝒪ᴹ} g f record { ᵐ⇒ = gᵐ⇒ ; ⟨𝑎𝑙𝑔⟩ = g⟨𝑎𝑙𝑔⟩ }
                      record { ᵐ⇒ = fᵐ⇒ ; ⟨𝑎𝑙𝑔⟩ = f⟨𝑎𝑙𝑔⟩ } → record
    { ᵐ⇒ = AsMonoid⇒.ᵐ⇒ ((g ⋉ gᵐ⇒) 𝕄on.∘ (f ⋉ fᵐ⇒))
    ; ⟨𝑎𝑙𝑔⟩ = trans (cong g f⟨𝑎𝑙𝑔⟩) (trans g⟨𝑎𝑙𝑔⟩
                   (cong (ΣMon.𝑎𝑙𝑔 𝒪ᴹ) (sym ⅀.homomorphism))) } }
  }

Σ𝕄onoids : Category 1ℓ 0ℓ 0ℓ
Σ𝕄onoids = ΣMonoidStructure.StructCat ΣMonoidCatProps

module Σ𝕄on = Category Σ𝕄onoids

ΣMonoid : Set₁
ΣMonoid = Σ𝕄on.Obj

ΣMonoid⇒ : ΣMonoid → ΣMonoid → Set
ΣMonoid⇒ = Σ𝕄on._⇒_

module FreeΣMonoid = ΣMonoidStructure.Free ΣMonoidCatProps

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.GroupoidTruncation where

open import Cubical.HITs.GroupoidTruncation.Base public
open import Cubical.HITs.GroupoidTruncation.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Container where

open import Prelude

Container : (s p : Level) → Type (ℓsuc (s ℓ⊔ p))
Container s p = Σ[ Shape ⦂ Type s ] × (Shape → Type p)

⟦_⟧ : ∀ {s p ℓ} → Container s p → Set ℓ → Set (s ℓ⊔ p ℓ⊔ ℓ)
⟦ S , P ⟧ X = Σ[ s ⦂ S ] × (P s → X)

cmap : ∀ {s p} {C : Container s p} → (A → B) → ⟦ C ⟧ A → ⟦ C ⟧ B
cmap f xs = xs .fst , λ i → f (xs .snd i)
{-# INLINE cmap #-}

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- Properties satisfied by posets
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.Props.Poset (p : Poset) where

open Relation.Binary.Poset p hiding (trans)
import Relation.Binary.NonStrictToStrict as Conv
open Conv _≈_ _≤_

------------------------------------------------------------------------
-- Posets can be turned into strict partial orders

strictPartialOrder : StrictPartialOrder
strictPartialOrder = record
  { isStrictPartialOrder = record
    { isEquivalence = isEquivalence
    ; irrefl        = irrefl
    ; trans         = trans isPartialOrder
    ; <-resp-≈      = <-resp-≈ isEquivalence ≤-resp-≈
    }
  }

open StrictPartialOrder strictPartialOrder

max_issues_repo_name: larrytheliquid/Lemmachine


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

module container.fixpoint where

open import sum
open import level
open import container.core
open import function.core
open import function.isomorphism
open import function.overloading

record Fixpoint {li la lb}
                (c : Container li la lb)
                (lx : Level) : Set (li ⊔ la ⊔ lb ⊔ lsuc lx) where
  constructor fix

  open Container c
  field
    X : I → Set lx
    fixpoint : ∀ i → X i ≅ F X i

  head : ∀ {i} → X i → A i
  head {i} = proj₁ ∘ apply (fixpoint i)

  tail : ∀ {i}(u : X i)(b : B (head u)) → X (r b)
  tail {i} = proj₂ ∘' apply (fixpoint i)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


text:
module plfa.part2.Properties-peer where

open import Relation.Binary.PropositionalEquality
  using (_≡_; _≢_; refl; sym; cong; cong₂)
open import Data.String using (String; _≟_)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product
  using (_×_; proj₁; proj₂; ∃; ∃-syntax)
  renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Function using (_∘_)
open import plfa.part1.Isomorphism
open import plfa.part2.Lambda

V¬—→ : ∀ {M N}
  → Value M
    ----------
  → ¬ (M —→ N)
V¬—→ V-ƛ        ()
V¬—→ V-zero     ()
V¬—→ (V-suc VM) (ξ-suc M—→N) = V¬—→ VM M—→N

—→¬V : ∀ {M N}
  → M —→ N
    ---------
  → ¬ Value M
—→¬V M—→N VM  =  V¬—→ VM M—→N

infix  4 Canonical_⦂_

data Canonical_⦂_ : Term → Type → Set where

  C-ƛ : ∀ {x A N B}
    → ∅ , x ⦂ A ⊢ N ⦂ B
      -----------------------------
    → Canonical (ƛ x ⇒ N) ⦂ (A ⇒ B)

  C-zero :
      --------------------
      Canonical `zero ⦂ `ℕ

  C-suc : ∀ {V}
    → Canonical V ⦂ `ℕ
      ---------------------
    → Canonical `suc V ⦂ `ℕ

canonical : ∀ {V A}
  → ∅ ⊢ V ⦂ A
  → Value V
    -----------
  → Canonical V ⦂ A
canonical (⊢` ())          ()
canonical (⊢ƛ ⊢N)          V-ƛ         =  C-ƛ ⊢N
canonical (⊢L · ⊢M)        ()
canonical ⊢zero            V-zero      =  C-zero
canonical (⊢suc ⊢V)        (V-suc VV)  =  C-suc (canonical ⊢V VV)
canonical (⊢case ⊢L ⊢M ⊢N) ()
canonical (⊢μ ⊢M)          ()

value : ∀ {M A}
  → Canonical M ⦂ A
    ----------------
  → Value M
value (C-ƛ ⊢N)    =  V-ƛ
value C-zero      =  V-zero
value (C-suc CM)  =  V-suc (value CM)

typed : ∀ {M A}
  → Canonical M ⦂ A
    ---------------
  → ∅ ⊢ M ⦂ A
typed (C-ƛ ⊢N)    =  ⊢ƛ ⊢N
typed C-zero      =  ⊢zero
typed (C-suc CM)  =  ⊢suc (typed CM)

data Progress (M : Term) : Set where

  step : ∀ {N}
    → M —→ N
      ----------
    → Progress M

  done :
      Value M
      ----------
    → Progress M

progress : ∀ {M A}
  → ∅ ⊢ M ⦂ A
    ----------
  → Progress M
progress (⊢` ())
progress (⊢ƛ ⊢N)                            =  done V-ƛ
progress (⊢L · ⊢M) with progress ⊢L
... | step L—→L′                            =  step (ξ-·₁ L—→L′)
... | done VL with progress ⊢M
...   | step M—→M′                          =  step (ξ-·₂ VL M—→M′)
...   | done VM with canonical ⊢L VL
...     | C-ƛ _                             =  step (β-ƛ VM)
progress ⊢zero                              =  done V-zero
progress (⊢suc ⊢M) with progress ⊢M
...  | step M—→M′                           =  step (ξ-suc M—→M′)
...  | done VM                              =  done (V-suc VM)
progress (⊢case ⊢L ⊢M ⊢N) with progress ⊢L
... | step L—→L′                            =  step (ξ-case L—→L′)
... | done VL with canonical ⊢L VL
...   | C-zero                              =  step β-zero
...   | C-suc CL                            =  step (β-suc (value CL))
progress (⊢μ ⊢M)                            =  step β-μ

postulate
  progress′ : ∀ M {A} → ∅ ⊢ M ⦂ A → Value M ⊎ ∃[ N ](M —→ N)

ext : ∀ {Γ Δ}
  → (∀ {x A}     →         Γ ∋ x ⦂ A →         Δ ∋ x ⦂ A)
    -----------------------------------------------------
  → (∀ {x y A B} → Γ , y ⦂ B ∋ x ⦂ A → Δ , y ⦂ B ∋ x ⦂ A)
ext ρ Z           =  Z
ext ρ (S x≢y ∋x)  =  S x≢y (ρ ∋x)

rename : ∀ {Γ Δ}
  → (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A)
    ----------------------------------
  → (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
rename ρ (⊢` ∋w)           =  ⊢` (ρ ∋w)
rename ρ (⊢ƛ ⊢N)           =  ⊢ƛ (rename (ext ρ) ⊢N)
rename ρ (⊢L · ⊢M)         =  (rename ρ ⊢L) · (rename ρ ⊢M)
rename ρ ⊢zero             =  ⊢zero
rename ρ (⊢suc ⊢M)         =  ⊢suc (rename ρ ⊢M)
rename ρ (⊢case ⊢L ⊢M ⊢N)  =  ⊢case (rename ρ ⊢L) (rename ρ ⊢M) (rename (ext ρ) ⊢N)
rename ρ (⊢μ ⊢M)           =  ⊢μ (rename (ext ρ) ⊢M)

weaken : ∀ {Γ M A}
  → ∅ ⊢ M ⦂ A
    ----------
  → Γ ⊢ M ⦂ A
weaken {Γ} ⊢M = rename ρ ⊢M
  where
  ρ : ∀ {z C}
    → ∅ ∋ z ⦂ C
      ---------
    → Γ ∋ z ⦂ C
  ρ ()

drop : ∀ {Γ x M A B C}
  → Γ , x ⦂ A , x ⦂ B ⊢ M ⦂ C
    --------------------------
  → Γ , x ⦂ B ⊢ M ⦂ C
drop {Γ} {x} {M} {A} {B} {C} ⊢M = rename ρ ⊢M
  where
  ρ : ∀ {z C}
    → Γ , x ⦂ A , x ⦂ B ∋ z ⦂ C
      -------------------------
    → Γ , x ⦂ B ∋ z ⦂ C
  ρ Z                 =  Z
  ρ (S x≢x Z)         =  ⊥-elim (x≢x refl)
  ρ (S z≢x (S _ ∋z))  =  S z≢x ∋z

swap : ∀ {Γ x y M A B C}
  → x ≢ y
  → Γ , y ⦂ B , x ⦂ A ⊢ M ⦂ C
    --------------------------
  → Γ , x ⦂ A , y ⦂ B ⊢ M ⦂ C
swap {Γ} {x} {y} {M} {A} {B} {C} x≢y ⊢M = rename ρ ⊢M
  where
  ρ : ∀ {z C}
    → Γ , y ⦂ B , x ⦂ A ∋ z ⦂ C
      --------------------------
    → Γ , x ⦂ A , y ⦂ B ∋ z ⦂ C
  ρ Z                   =  S x≢y Z
  ρ (S z≢x Z)           =  Z
  ρ (S z≢x (S z≢y ∋z))  =  S z≢y (S z≢x ∋z)

subst : ∀ {Γ x N V A B}
  → ∅ ⊢ V ⦂ A
  → Γ , x ⦂ A ⊢ N ⦂ B
    --------------------
  → Γ ⊢ N [ x := V ] ⦂ B
subst {x = y} ⊢V (⊢` {x = x} Z) with x ≟ y
... | yes _           =  weaken ⊢V
... | no  x≢y         =  ⊥-elim (x≢y refl)
subst {x = y} ⊢V (⊢` {x = x} (S x≢y ∋x)) with x ≟ y
... | yes refl        =  ⊥-elim (x≢y refl)
... | no  _           =  ⊢` ∋x
subst {x = y} ⊢V (⊢ƛ {x = x} ⊢N) with x ≟ y
... | yes refl        =  ⊢ƛ (drop ⊢N)
... | no  x≢y         =  ⊢ƛ (subst ⊢V (swap x≢y ⊢N))
subst ⊢V (⊢L · ⊢M)    =  (subst ⊢V ⊢L) · (subst ⊢V ⊢M)
subst ⊢V ⊢zero        =  ⊢zero
subst ⊢V (⊢suc ⊢M)    =  ⊢suc (subst ⊢V ⊢M)
subst {x = y} ⊢V (⊢case {x = x} ⊢L ⊢M ⊢N) with x ≟ y
... | yes refl        =  ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (drop ⊢N)
... | no  x≢y         =  ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (subst ⊢V (swap x≢y ⊢N))
subst {x = y} ⊢V (⊢μ {x = x} ⊢M) with x ≟ y
... | yes refl        =  ⊢μ (drop ⊢M)
... | no  x≢y         =  ⊢μ (subst ⊢V (swap x≢y ⊢M))

preserve : ∀ {M N A}
  → ∅ ⊢ M ⦂ A
  → M —→ N
    ----------
  → ∅ ⊢ N ⦂ A
preserve (⊢` ())
preserve (⊢ƛ ⊢N)                 ()
preserve (⊢L · ⊢M)               (ξ-·₁ L—→L′)     =  (preserve ⊢L L—→L′) · ⊢M
preserve (⊢L · ⊢M)               (ξ-·₂ VL M—→M′)  =  ⊢L · (preserve ⊢M M—→M′)
preserve ((⊢ƛ ⊢N) · ⊢V)          (β-ƛ VV)         =  subst ⊢V ⊢N
preserve ⊢zero                   ()
preserve (⊢suc ⊢M)               (ξ-suc M—→M′)    =  ⊢suc (preserve ⊢M M—→M′)
preserve (⊢case ⊢L ⊢M ⊢N)        (ξ-case L—→L′)   =  ⊢case (preserve ⊢L L—→L′) ⊢M ⊢N
preserve (⊢case ⊢zero ⊢M ⊢N)     (β-zero)         =  ⊢M
preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) (β-suc VV)       =  subst ⊢V ⊢N
preserve (⊢μ ⊢M)                 (β-μ)            =  subst (⊢μ ⊢M) ⊢M

sucμ  =  μ "x" ⇒ `suc (` "x")

data Gas : Set where
  gas : ℕ → Gas

data Finished (N : Term) : Set where

  done :
      Value N
      ----------
    → Finished N

  out-of-gas :
      ----------
      Finished N

data Steps (L : Term) : Set where

  steps : ∀ {N}
    → L —↠ N
    → Finished N
      ----------
    → Steps L

{-# TERMINATING #-}
eval : ∀ {L A}
  → Gas
  → ∅ ⊢ L ⦂ A
    ---------
  → Steps L

eval {L} (gas zero)    ⊢L                             =  steps (L ∎) out-of-gas
eval {L} (gas (suc m)) ⊢L with progress ⊢L
... | done VL                                         =  steps (L ∎) (done VL)
... | step L—→M with eval (gas m) (preserve ⊢L L—→M)
...    | steps M—↠N fin                               =  steps (L —→⟨ L—→M ⟩ M—↠N) fin

⊢sucμ : ∅ ⊢ μ "x" ⇒ `suc ` "x" ⦂ `ℕ
⊢sucμ = ⊢μ (⊢suc (⊢` ∋x))
  where
  ∋x = Z

_ : eval (gas 3) ⊢sucμ ≡
  steps
   (μ "x" ⇒ `suc ` "x"
   —→⟨ β-μ ⟩
    `suc (μ "x" ⇒ `suc ` "x")
   —→⟨ ξ-suc β-μ ⟩
    `suc (`suc (μ "x" ⇒ `suc ` "x"))
   —→⟨ ξ-suc (ξ-suc β-μ) ⟩
    `suc (`suc (`suc (μ "x" ⇒ `suc ` "x")))
   ∎)
   out-of-gas
_ = refl

_ : eval (gas 100) (⊢twoᶜ · ⊢sucᶜ · ⊢zero) ≡
  steps
   ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
   · `zero
   —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
    (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
     `zero
   —→⟨ β-ƛ V-zero ⟩
    (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `zero)
   —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
    (ƛ "n" ⇒ `suc ` "n") · `suc `zero
   —→⟨ β-ƛ (V-suc V-zero) ⟩
    `suc (`suc `zero)
   ∎)
   (done (V-suc (V-suc V-zero)))
_ = refl

_ : eval (gas 100) ⊢2+2 ≡
  steps
   ((μ "+" ⇒
     (ƛ "m" ⇒
      (ƛ "n" ⇒
       case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
       ])))
    · `suc (`suc `zero)
    · `suc (`suc `zero)
   —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
    (ƛ "m" ⇒
     (ƛ "n" ⇒
      case ` "m" [zero⇒ ` "n" |suc "m" ⇒
      `suc
      ((μ "+" ⇒
        (ƛ "m" ⇒
         (ƛ "n" ⇒
          case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
          ])))
       · ` "m"
       · ` "n")
      ]))
    · `suc (`suc `zero)
    · `suc (`suc `zero)
   —→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
    (ƛ "n" ⇒
     case `suc (`suc `zero) [zero⇒ ` "n" |suc "m" ⇒
     `suc
     ((μ "+" ⇒
       (ƛ "m" ⇒
        (ƛ "n" ⇒
         case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
         ])))
      · ` "m"
      · ` "n")
     ])
    · `suc (`suc `zero)
   —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
    case `suc (`suc `zero) [zero⇒ `suc (`suc `zero) |suc "m" ⇒
    `suc
    ((μ "+" ⇒
      (ƛ "m" ⇒
       (ƛ "n" ⇒
        case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
        ])))
     · ` "m"
     · `suc (`suc `zero))
    ]
   —→⟨ β-suc (V-suc V-zero) ⟩
    `suc
    ((μ "+" ⇒
      (ƛ "m" ⇒
       (ƛ "n" ⇒
        case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
        ])))
     · `suc `zero
     · `suc (`suc `zero))
   —→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
    `suc
    ((ƛ "m" ⇒
      (ƛ "n" ⇒
       case ` "m" [zero⇒ ` "n" |suc "m" ⇒
       `suc
       ((μ "+" ⇒
         (ƛ "m" ⇒
          (ƛ "n" ⇒
           case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
           ])))
        · ` "m"
        · ` "n")
       ]))
     · `suc `zero
     · `suc (`suc `zero))
   —→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
    `suc
    ((ƛ "n" ⇒
      case `suc `zero [zero⇒ ` "n" |suc "m" ⇒
      `suc
      ((μ "+" ⇒
        (ƛ "m" ⇒
         (ƛ "n" ⇒
          case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
          ])))
       · ` "m"
       · ` "n")
      ])
     · `suc (`suc `zero))
   —→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
    `suc
    case `suc `zero [zero⇒ `suc (`suc `zero) |suc "m" ⇒
    `suc
    ((μ "+" ⇒
      (ƛ "m" ⇒
       (ƛ "n" ⇒
        case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
        ])))
     · ` "m"
     · `suc (`suc `zero))
    ]
   —→⟨ ξ-suc (β-suc V-zero) ⟩
    `suc
    (`suc
     ((μ "+" ⇒
       (ƛ "m" ⇒
        (ƛ "n" ⇒
         case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
         ])))
      · `zero
      · `suc (`suc `zero)))
   —→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
    `suc
    (`suc
     ((ƛ "m" ⇒
       (ƛ "n" ⇒
        case ` "m" [zero⇒ ` "n" |suc "m" ⇒
        `suc
        ((μ "+" ⇒
          (ƛ "m" ⇒
           (ƛ "n" ⇒
            case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
            ])))
         · ` "m"
         · ` "n")
        ]))
      · `zero
      · `suc (`suc `zero)))
   —→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
    `suc
    (`suc
     ((ƛ "n" ⇒
       case `zero [zero⇒ ` "n" |suc "m" ⇒
       `suc
       ((μ "+" ⇒
         (ƛ "m" ⇒
          (ƛ "n" ⇒
           case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
           ])))
        · ` "m"
        · ` "n")
       ])
      · `suc (`suc `zero)))
   —→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
    `suc
    (`suc
     case `zero [zero⇒ `suc (`suc `zero) |suc "m" ⇒
     `suc
     ((μ "+" ⇒
       (ƛ "m" ⇒
        (ƛ "n" ⇒
         case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
         ])))
      · ` "m"
      · `suc (`suc `zero))
     ])
   —→⟨ ξ-suc (ξ-suc β-zero) ⟩
    `suc (`suc (`suc (`suc `zero)))
   ∎)
   (done (V-suc (V-suc (V-suc (V-suc V-zero)))))
_ = refl

Normal : Term → Set
Normal M  =  ∀ {N} → ¬ (M —→ N)

Stuck : Term → Set
Stuck M  =  Normal M × ¬ Value M

-- Exercise Progress-≃ (practice)

Progress-≃ : ∀ {M} → Progress M ≃ Value M ⊎ ∃[ N ](M —→ N)
Progress-≃ {M} = record
  { to      = to
  ; from    = from
  ; from∘to = from∘to
  ; to∘from = to∘from }
  where
    to : ∀ { M } → Progress M  → Value M ⊎ ∃[ N ](M —→ N)
    to (done m) = inj₁ m
    to (step {N} M→N) = inj₂ ⟨ N , M→N ⟩
    from : ∀ { M } →  Value M ⊎ ∃[ N ](M —→ N) → Progress M
    from (inj₁ m) = done m
    from (inj₂ ⟨ N , M→N ⟩) = step M→N
    from∘to : ∀ { M } → (m : Progress M) → from (to m) ≡ m
    from∘to (done m) = refl
    from∘to (step M→N) = refl
    to∘from : ∀ { M } ( s : Value M ⊎ ∃[ N ](M —→ N)) → to (from s) ≡ s
    to∘from (inj₁ m) = refl
    to∘from (inj₂ ⟨ N , M→N ⟩) = refl

-- Exercise value? (practice)

value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M)
value? ⊢M with progress ⊢M
... | done m = yes m
... | step M→N = no (—→¬V M→N)

-- Exercise mul-eval (recommended)

mulᶜ : Term
mulᶜ = ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
         ` "m" · (` "n" · ` "s" ) · ` "z"

⊢mulᶜ : ∀ {Γ A} → Γ ⊢ mulᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A
⊢mulᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (⊢m · ⊢z))))
  where
    ⊢m = (⊢` (S  (λ()) (S  (λ()) (S  (λ()) Z))))
      · (⊢` (S  (λ()) (S  (λ()) Z))
      · (⊢` (S  (λ()) Z)))
    ⊢z = ⊢` Z

⊢2*2ᶜ : ∅ ⊢ mulᶜ · twoᶜ · twoᶜ · sucᶜ · `zero ⦂ `ℕ
⊢2*2ᶜ = ⊢mulᶜ · ⊢twoᶜ · ⊢twoᶜ · ⊢sucᶜ · ⊢zero

_ : eval (gas 100) (⊢2*2ᶜ) ≡
  steps
  ((ƛ "m" ⇒
    (ƛ "n" ⇒ (
      ƛ "s" ⇒ (ƛ "z" ⇒ ` "m" · (` "n" · ` "s") · ` "z"))))
   · (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")))
   · (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")))
   · (ƛ "n" ⇒ `suc ` "n")
   · `zero
  —→⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩
  (ƛ "n" ⇒
   (ƛ "s" ⇒
    (ƛ "z" ⇒
      (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (` "n" · ` "s") · ` "z")))
    · (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")))
    · (ƛ "n" ⇒ `suc ` "n")
    · `zero
 —→⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
  (ƛ "s" ⇒
   (ƛ "z" ⇒
    (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) ·
    ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · ` "s") · ` "z"))
   · (ƛ "n" ⇒ `suc ` "n")
   · `zero
 —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
  (ƛ "z" ⇒
   (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) ·
    ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) ·
     (ƛ "n" ⇒ `suc ` "n"))
   · ` "z")
   · `zero
 —→⟨ β-ƛ V-zero ⟩
  (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) ·
  ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) ·
    (ƛ "n" ⇒ `suc ` "n"))
    · `zero
 —→⟨ ξ-·₁ (ξ-·₂ V-ƛ (β-ƛ V-ƛ)) ⟩
   (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) ·
    (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z"))
    · `zero
 —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
  (ƛ "z" ⇒
   (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
   ((ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) · ` "z"))
   · `zero
 —→⟨ β-ƛ V-zero ⟩
  (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
   ((ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
   `zero)
 —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
  (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
   ((ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `zero))
 —→⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩
  (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
   ((ƛ "n" ⇒ `suc ` "n") · `suc `zero)
 —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
  (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
   `suc (`suc `zero)
 —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
  (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `suc (`suc `zero))
 —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc (V-suc V-zero))) ⟩
  (ƛ "n" ⇒ `suc ` "n") · `suc (`suc (`suc `zero)) —→⟨
   β-ƛ (V-suc (V-suc (V-suc V-zero))) ⟩
   `suc (`suc (`suc (`suc `zero))) ∎)
  (done (V-suc (V-suc (V-suc (V-suc V-zero)))))
_ = refl

-- Exercise: progress-preservation (practice)
-- progress: If there exists a term M ⦂ A, then M must either be a value, or there exists an N such that M —→ N
-- preservation: If term M ⦂ A and N can be reduced from M, then N ⦂ A.

-- Exercise subject_expansion (practice)

-- counter example with case expression
-- M = case `suc V [zero ⇒ N |suc x ⇒ T ], ∅ ⊢ N ⦂ A,  ∅ ⊢ T ⦂ B
-- In this example, M does not have a type, but M —→ A or M  —→ B.

-- counter example without case expression
-- M —→ N, ∅ ⊢ N ⦂ A → B → A and  N = λ a b. a

-- Exercise stuck (practice)

-- example: `zero · `suc `zero
-- The example above is an ill-typed term.

-- Exercise unstuck (recommended)

unstuck : ∀ {M A}
  → ∅ ⊢ M ⦂ A
  -----------
  → ¬ (Stuck M)
unstuck m ⟨ fst , snd ⟩ with progress m
... | done m₁ = ⊥-elim (snd m₁)
... | step m₁  = ⊥-elim (fst m₁)

preserves : ∀ {M N A}
  → ∅ ⊢ M ⦂ A
  → M —↠ N
  ---------
  → ∅ ⊢ N ⦂ A
preserves m (M _—↠_.∎) = m
preserves m (L —→⟨ LM ⟩ MN) = preserves (preserve m LM) MN

wttdgs : ∀ {M N A}
  → ∅ ⊢ M ⦂ A
  → M —↠ N
  -----------
  → ¬ (Stuck N)
wttdgs a n = unstuck (preserves a n)


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

module lib.two-semi-categories.TwoSemiCategories where

open import lib.two-semi-categories.FunCategory public
open import lib.two-semi-categories.Functor public
open import lib.two-semi-categories.FunctorInverse public
open import lib.two-semi-categories.FundamentalCategory public
open import lib.two-semi-categories.FunextFunctors public
open import lib.two-semi-categories.GroupToCategory public

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
open import Function                              using (_∘_)
open import Category.Monad                        using (module RawMonad)
open import Data.Fin                              using (Fin; suc; zero)
open import Data.Fin.Properties                   renaming (_≟_ to _≟-Fin_)
open import Data.List    as List                  using (List; _∷_; [])
open import Data.List.Properties                  renaming (∷-injective to ∷-inj)
open import Data.Maybe   as Maybe                 using (Maybe; just; nothing)
open import Data.Nat                              using (ℕ; suc; zero)
open import Data.Product as Prod                  using (∃; _×_; _,_; proj₁; proj₂)
open import Relation.Nullary                      using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)

module Unification
  (Name    : Set) (_≟-Name_    : (x y : Name)    → Dec (x ≡ y))
  (Literal : Set) (_≟-Literal_ : (x y : Literal) → Dec (x ≡ y))
  where

  open RawMonad {{...}} using (_<$>_; _>>=_; return)

  private
    instance
      MaybeMonad = Maybe.monad

  data Term (n : ℕ) : Set where
    var : (x : Fin n) → Term n
    con : (s : Name) (ts : List (Term n)) → Term n
    lit : (l : Literal) → Term n
--  ext : (x : Fin (suc n)) (t : Term (suc n)) → Term n

  var-inj : ∀ {n x₁ x₂} → var {n} x₁ ≡ var {n} x₂ → x₁ ≡ x₂
  var-inj refl = refl

  con-inj : ∀ {n s₁ s₂ ts₁ ts₂} → con {n} s₁ ts₁ ≡ con {n} s₂ ts₂ → s₁ ≡ s₂ × ts₁ ≡ ts₂
  con-inj refl = (refl , refl)

  lit-inj : ∀ {n x₁ x₂} → lit {n} x₁ ≡ lit {n} x₂ → x₁ ≡ x₂
  lit-inj refl = refl

  mutual
    _≟-Term_ : ∀ {n} → (t₁ t₂ : Term n) → Dec (t₁ ≡ t₂)
    _≟-Term_ (var _)  (lit _)   = no (λ ())
    _≟-Term_ (var _)  (con _ _) = no (λ ())
    _≟-Term_ (var x₁) (var x₂) with x₁ ≟-Fin x₂
    ... | yes x₁=x₂ = yes (cong var x₁=x₂)
    ... | no  x₁≠x₂ = no (x₁≠x₂ ∘ var-inj)
    _≟-Term_ (con _ _)    (var _)   = no (λ ())
    _≟-Term_ (con _ _)    (lit _)   = no (λ ())
    _≟-Term_ (con s₁ ts₁) (con s₂ ts₂) with s₁ ≟-Name s₂
    ... | no  s₁≠s₂ = no (s₁≠s₂ ∘ proj₁ ∘ con-inj)
    ... | yes s₁=s₂ rewrite s₁=s₂ with ts₁ ≟-Terms ts₂
    ... | no  ts₁≠ts₂ = no (ts₁≠ts₂ ∘ proj₂ ∘ con-inj)
    ... | yes ts₁=ts₂ = yes (cong (con s₂) ts₁=ts₂)
    _≟-Term_ (lit _)  (var _)   = no (λ ())
    _≟-Term_ (lit _)  (con _ _) = no (λ ())
    _≟-Term_ (lit x₁) (lit x₂) with x₁ ≟-Literal x₂
    ... | yes x₁=x₂ = yes (cong lit x₁=x₂)
    ... | no  x₁≠x₂ = no (x₁≠x₂ ∘ lit-inj)

    _≟-Terms_ : ∀ {n} (xs ys : List (Term n)) → Dec (xs ≡ ys)
    _≟-Terms_ [] [] = yes refl
    _≟-Terms_ [] (_  ∷ _) = no (λ ())
    _≟-Terms_ (_ ∷ _) [] = no (λ ())
    _≟-Terms_ (x ∷ xs) (y ∷ ys) with x ≟-Term y
    ... | no  x≠y = no (x≠y ∘ proj₁ ∘ ∷-inj)
    ... | yes x=y with xs ≟-Terms ys
    ... | no  xs≠ys = no (xs≠ys ∘ proj₂ ∘ ∷-inj)
    ... | yes xs=ys = yes (cong₂ _∷_ x=y xs=ys)

  -- defining thick and thin
  thin : {n : ℕ} → Fin (suc n) → Fin n → Fin (suc n)
  thin  zero    y      = suc y
  thin (suc x)  zero   = zero
  thin (suc x) (suc y) = suc (thin x y)

  thick : {n : ℕ} → (x y : Fin (suc n)) → Maybe (Fin n)
  thick          zero    zero   = nothing
  thick          zero   (suc y) = just y
  thick {zero}  (suc ()) _
  thick {suc n} (suc x)  zero   = just zero
  thick {suc n} (suc x) (suc y) = suc <$> thick x y

  -- defining replacement function (written _◂ in McBride, 2003)
  replace : ∀ {n m} → (Fin n → Term m) → Term n → Term m
  replace _ (lit l) = lit l
  replace f (var i) = f i
  replace f (con s ts) = con s (replaceChildren f ts)
    where
      replaceChildren : ∀ {n m} → (Fin n → Term m) → (List (Term n) → List (Term m))
      replaceChildren f []       = []
      replaceChildren f (x ∷ xs) = replace f x ∷ (replaceChildren f xs)

  -- defining replacement composition
  _◇_ : ∀ {m n l} (f : Fin m → Term n) (g : Fin l → Term m) → Fin l → Term n
  _◇_ f g = replace f ∘ g

  -- defining an occurs check (**check** in McBride, 2003)
  check : ∀ {n} (x : Fin (suc n)) (t : Term (suc n)) → Maybe (Term n)
  check _  (lit l)    = just (lit l)
  check x₁ (var x₂)   = var <$> thick x₁ x₂
  check x₁ (con s ts) = con s <$> checkChildren x₁ ts
    where
      checkChildren : ∀ {n} (x : Fin (suc n)) (ts : List (Term (suc n))) → Maybe (List (Term n))
      checkChildren x₁ [] = just []
      checkChildren x₁ (t ∷ ts) = check x₁ t >>= λ t' →
        checkChildren x₁ ts >>= λ ts' → return (t' ∷ ts')

  -- datatype for substitutions (AList in McBride, 2003)
  data Subst : ℕ → ℕ → Set where
    nil  : ∀ {n}   → Subst n n
    snoc : ∀ {m n} → (s : Subst m n) → (t : Term m) → (x : Fin (suc m)) → Subst (suc m) n

  -- substitutes t for x (**for** in McBride, 2003)
  _for_ : ∀ {n} (t : Term n) (x : Fin (suc n)) → Fin (suc n) → Term n
  _for_ t x y with thick x y
  _for_ t x y | just y' = var y'
  _for_ t x y | nothing = t

  -- substitution application (**sub** in McBride, 2003)
  sub : ∀ {m n} → Subst m n → Fin m → Term n
  sub nil = var
  sub (snoc s t x) = (sub s) ◇ (t for x)

  -- composes two substitutions
  _++_ : ∀ {l m n} → Subst m n → Subst l m → Subst l n
  s₁ ++ nil = s₁
  s₁ ++ (snoc s₂ t x) = snoc (s₁ ++ s₂) t x

  flexRigid : ∀ {n} → Fin n → Term n → Maybe (∃ (Subst n))
  flexRigid {zero} () t
  flexRigid {suc n} x t with check x t
  flexRigid {suc n} x t | nothing = nothing
  flexRigid {suc n} x t | just t' = just (n , snoc nil t' x)

  flexFlex : ∀ {n} → (x y : Fin n) → ∃ (Subst n)
  flexFlex {zero} () j
  flexFlex {suc n} x y with thick x y
  flexFlex {suc n} x y | nothing = (suc n , nil)
  flexFlex {suc n} x y | just  z = (n , snoc nil (var z) x)

  mutual
    unifyAcc : ∀ {m} → (t₁ t₂ : Term m) → ∃ (Subst m) → Maybe (∃ (Subst m))
    unifyAcc (lit x₁) (lit x₂) (n , nil) with x₁ ≟-Literal x₂
    ... | yes x₁=x₂ rewrite x₁=x₂ = just (n , nil)
    ... | no  x₁≠x₂ = nothing
    unifyAcc (con s ts) (lit x) (n , nil) = nothing
    unifyAcc (lit x) (con s ts) (n , nil) = nothing
    unifyAcc (con s₁ ts₁) (con  s₂ ts₂) acc with s₁ ≟-Name s₂
    ... | yes s₁=s₂ rewrite s₁=s₂ = unifyAccChildren ts₁ ts₂ acc
    ... | no  s₁≠s₂ = nothing
    unifyAcc (var x₁) (var x₂) (n , nil) = just (flexFlex x₁ x₂)
    unifyAcc t (var x) (n , nil) = flexRigid x t
    unifyAcc (var x) t (n , nil) = flexRigid x t
    unifyAcc t₁ t₂ (n , snoc s t′ x) =
      ( λ s → proj₁ s , snoc (proj₂ s) t′ x )
        <$> unifyAcc (replace (t′ for x) t₁) (replace (t′ for x) t₂) (n , s)

    unifyAccChildren : ∀ {n} → (ts₁ ts₂ : List (Term n)) → ∃ (Subst n) → Maybe (∃ (Subst n))
    unifyAccChildren []         []       acc = just acc
    unifyAccChildren []         _        _   = nothing
    unifyAccChildren _          []       _   = nothing
    unifyAccChildren (t₁ ∷ ts₁) (t₂ ∷ ts₂) acc = unifyAcc t₁ t₂ acc >>= unifyAccChildren ts₁ ts₂

  unify : ∀ {m} → (t₁ t₂ : Term m) → Maybe (∃ (Subst m))
  unify {m} t₁ t₂ = unifyAcc t₁ t₂ (m , nil)

max_stars_repo_name: wenkokke/AutoInAgda

max_issues_repo_name: wenkokke/AutoInAgda

max_forks_repo_name: wenkokke/AutoInAgda


text:
module Oscar.Data.Term.internal.SubstituteAndSubstitution1 {𝔣} (FunctionName : Set 𝔣) where

open import Oscar.Data.Equality
open import Oscar.Data.Equality.properties
open import Oscar.Data.Fin
open import Oscar.Data.Nat
open import Oscar.Data.Term FunctionName
open import Oscar.Data.Vec
open import Oscar.Function

infix 19 _◃_ _◃s_
mutual

  _◃_ : ∀ {m n} → (f : m ⊸ n) → Term m → Term n
  σ̇ ◃ i 𝑥 = σ̇ 𝑥
  _ ◃ leaf = leaf
  σ̇ ◃ (τl fork τr) = (σ̇ ◃ τl) fork (σ̇ ◃ τr)
  σ̇ ◃ (function fn τs) = function fn (σ̇ ◃s τs) where

  _◃s_ : ∀ {m n} → m ⊸ n → ∀ {N} → Vec (Term m) N → Vec (Term n) N
  f ◃s [] = []
  f ◃s (t ∷ ts) = f ◃ t ∷ f ◃s ts

_◇_ : ∀ {m n} → m ⊸ n → ∀ {l} → l ⊸ m → l ⊸ n
_◇_ f g = (f ◃_) ∘ g

mutual

  ◃-extensionality : ∀ {m n} {f g : m ⊸ n} → f ≡̇ g → f ◃_ ≡̇ g ◃_
  ◃-extensionality p (i x) = p x
  ◃-extensionality p leaf = refl
  ◃-extensionality p (s fork t) = cong₂ _fork_ (◃-extensionality p s) (◃-extensionality p t)
  ◃-extensionality p (function fn ts) = cong (function fn) (◃s-extensionality p ts)

  ◃s-extensionality : ∀ {m n} {f g : m ⊸ n} → f ≡̇ g → ∀ {N} → _◃s_ f {N} ≡̇ _◃s_ g
  ◃s-extensionality p [] = refl
  ◃s-extensionality p (t ∷ ts) = cong₂ _∷_ (◃-extensionality p t) (◃s-extensionality p ts)

mutual

  ◃-associativity : ∀ {l m} (f : l ⊸ m) {n} (g : m ⊸ n) → (g ◇ f) ◃_ ≡̇ (g ◃_) ∘ (f ◃_)
  ◃-associativity _ _ (i _) = refl
  ◃-associativity _ _ leaf = refl
  ◃-associativity _ _ (τ₁ fork τ₂) = cong₂ _fork_ (◃-associativity _ _ τ₁) (◃-associativity _ _ τ₂)
  ◃-associativity f g (function fn ts) = cong (function fn) (◃s-associativity f g ts)

  ◃s-associativity : ∀ {l m n} (f : l ⊸ m) (g : m ⊸ n) → ∀ {N} → (_◃s_ (g ◇ f) {N}) ≡̇ (g ◃s_) ∘ (f ◃s_)
  ◃s-associativity _ _ [] = refl
  ◃s-associativity _ _ (τ ∷ τs) = cong₂ _∷_ (◃-associativity _ _ τ) (◃s-associativity _ _ τs)

◇-associativity : ∀ {k l} (f : k ⊸ l) {m} (g : l ⊸ m) {n} (h : m ⊸ n) → (h ◇ g) ◇ f ≡̇ h ◇ (g ◇ f)
◇-associativity f g h x rewrite ◃-associativity g h (f x) = refl

◇-extensionality : ∀ {l m} {f₁ f₂ : l ⊸ m} → f₁ ≡̇ f₂ → ∀ {n} {g₁ g₂ : m ⊸ n} → g₁ ≡̇ g₂ → g₁ ◇ f₁ ≡̇ g₂ ◇ f₂
◇-extensionality {f₂ = f₂} f₁≡̇f₂ g₁≡̇g₂ x rewrite f₁≡̇f₂ x = ◃-extensionality g₁≡̇g₂ (f₂ x)

open import Oscar.Category.Semigroupoid

SemigroupoidSubstitution : Semigroupoid _ _ _
Semigroupoid.⋆ SemigroupoidSubstitution = _
Semigroupoid._⇒_ SemigroupoidSubstitution m n = Fin m ⇒ Term n
Semigroupoid._∙_ SemigroupoidSubstitution = _◇_
Semigroupoid.associativity SemigroupoidSubstitution = ◇-associativity
Semigroupoid.extensionality SemigroupoidSubstitution = ◇-extensionality

open import Oscar.Category.Semifunctor

SemifunctorSubstitution : Semifunctor _ _ _ _ _ _
Semifunctor.semigroupoid₁ SemifunctorSubstitution = SemigroupoidSubstitution
Semifunctor.semigroupoid₂ SemifunctorSubstitution = SemigroupoidFunction Term
Semifunctor.μ SemifunctorSubstitution = id
Semifunctor.𝔣 SemifunctorSubstitution = _◃_
Semifunctor.extensionality SemifunctorSubstitution = ◃-extensionality
Semifunctor.preservativity SemifunctorSubstitution = ◃-associativity

ε : ∀ {m} → m ⊸ m
ε = i

mutual

  ◃-identity : ∀ {m} (t : Term m) → ε ◃ t ≡ t
  ◃-identity (i x) = refl
  ◃-identity leaf = refl
  ◃-identity (s fork t) = cong₂ _fork_ (◃-identity s) (◃-identity t)
  ◃-identity (function fn ts) = cong (function fn) (◃s-identity ts)

  ◃s-identity : ∀ {N m} (t : Vec (Term m) N) → ε ◃s t ≡ t
  ◃s-identity [] = refl
  ◃s-identity (t ∷ ts) = cong₂ _∷_ (◃-identity t) (◃s-identity ts)

◇-left-identity : ∀ {m n} (f : m ⊸ n) → ε ◇ f ≡̇ f
◇-left-identity f = ◃-identity ∘ f

◇-right-identity : ∀ {m n} (f : m ⊸ n) → f ◇ ε ≡̇ f
◇-right-identity _ _ = refl

open import Oscar.Category.Category

CategorySubstitution : Category _ _ _
Category.semigroupoid CategorySubstitution = SemigroupoidSubstitution
Category.ε CategorySubstitution = ε
Category.left-identity CategorySubstitution = {!!}
Category.right-identity CategorySubstitution {x} {y} {f} x₁ = ◇-right-identity f x₁

test-right-id = {!Category.right-identity CategorySubstitution!}

-- open import Oscar.Property.Associativity
-- open import Oscar.Property.Equivalence
-- open import Oscar.Property.Extensionality₂

-- instance

--   AssociativitySubstitutionComposition : Associativity _◇_ _≡̇_
--   Associativity.associativity AssociativitySubstitutionComposition = ◇-associativity

--   ExtensionalityS◇ : ExtensionalitySemigroupoid _◇_ _≡̇_
--   ExtensionalitySemigroupoid.extensionalitySemigroupoid ExtensionalityS◇ g₁≡̇g₂ {_} {_} {f₂} f₁≡̇f₂ x rewrite f₁≡̇f₂ x = ◃-extensionality g₁≡̇g₂ (f₂ x)

-- -- instance

-- --   Extensionality₂≡̇◇⋆ : ∀ {x y z} → Extensionality₂⋆ _≡̇_ _≡̇_ (λ ‵ → _≡̇_ ‵) ((y ⊸ z → x ⊸ y → x ⊸ z) ∋ λ ` → _◇_ `) (λ ` → _◇_ `)
-- --   Extensionality₂⋆.extensionality* Extensionality₂≡̇◇⋆ g₁≡̇g₂ {_} {f₂} f₁≡̇f₂ x rewrite f₁≡̇f₂ x = ◃-extensionality g₁≡̇g₂ (f₂ x)

-- -- --  Extensionality₂≡̇◇ : ∀ {x y z} → Extensionality₂ _≡̇_ _≡̇_ (λ ‵ → _≡̇_ ‵) (λ {yz} → _◇_ {y} {z} yz {x}) (λ {_} {yz} → yz ◇_)
-- -- --  Extensionality₂.extensionality₂ Extensionality₂≡̇◇ {g₁} {g₂} g₁≡̇g₂ {f₁} {f₂} f₁≡̇f₂ x rewrite f₁≡̇f₂ x = ◃-extensionality g₁≡̇g₂ (f₂ x)

-- instance

--   SemigroupoidSubstitution : Semigroupoid _ _ _
--   Semigroupoid.⋆ SemigroupoidSubstitution = _
--   Semigroupoid._⇒_ SemigroupoidSubstitution = _⊸_
--   Semigroupoid._≋_ SemigroupoidSubstitution = _≡̇_
--   Semigroupoid._∙_ SemigroupoidSubstitution = _◇_

-- instance

--   Associativity-∘ : ∀ {𝔬} {⋆ : Set 𝔬} {f} {F : ⋆ → Set f} →
--                     Associativity (λ {y} {z} g {x} f₁ x₁ → g (f₁ x₁))
--                                   (λ {x} {y} f₁ g → (x₁ : F x) → f₁ x₁ ≡ g x₁)
--   Associativity.associativity Associativity-∘ _ _ _ _ = refl

--   ExtensionalityS∘ : ∀ {𝔬} {⋆ : Set 𝔬} {f} {F : ⋆ → Set f} → ExtensionalitySemigroupoid (λ g f → {!(λ {_} → g) ∘ f!}) (_≡̇_ {B = F})
--   ExtensionalityS∘ = {!!}

-- --   Extensionality₂-≡̇ : ∀ {𝔬} {⋆ : Set 𝔬} {f} {F : ⋆ → Set f} {x y z : ⋆} →
-- --      Extensionality₂ {_} {F _ → _} {_} {λ _ → F _ → _}
-- --      (λ f₁ g → (x₁ : F y) → _≡_ (f₁ x₁) (g x₁)) {_}
-- --      {λ {w} _ → F _ → _} {_} {λ {w} {x₁} _ → F x → F y} {f}
-- --      (λ {w} {x₁} f₁ g → (x₂ : F x) → _≡_ {f} {F y} (f₁ x₂) (g x₂)) {f}
-- --      {λ {w} {y₁} _ → F x → F z} {f} {λ {w} {x₁} {y₁} _ → F x → F z} {f}
-- --      (λ {w} {x₁} {y₁} ′ {z₁} g →
-- --         (x₂ : F x) → _≡_ (′ x₂) (g x₂))
-- --      (λ {yz} f₁ x₂ → yz (f₁ x₂))
-- --      (λ {_} {yz} f₁ x₁ → yz (f₁ x₁))
-- --   Extensionality₂.extensionality₂ Extensionality₂-≡̇ w≡̇x y≡̇z f rewrite y≡̇z f = w≡̇x _

-- SemigroupoidIndexedFunction : ∀ {𝔬} {⋆ : Set 𝔬} {f} (F : ⋆ → Set f) → Semigroupoid _ _ _
-- Semigroupoid.⋆ (SemigroupoidIndexedFunction F) = _
-- Semigroupoid._⇒_ (SemigroupoidIndexedFunction F) m n = F m → F n
-- Semigroupoid._≋_ (SemigroupoidIndexedFunction F) = _≡̇_
-- Semigroupoid._∙_ (SemigroupoidIndexedFunction F) g f = g ∘ f
-- Semigroupoid.′associativity (SemigroupoidIndexedFunction F) = it
-- Semigroupoid.′extensionality₂ (SemigroupoidIndexedFunction F) = {!!} -- Extensionality₂-≡̇ {F = F}

-- open import Oscar.Property.Extensionality

-- instance

--   ex : ∀ {x y} →
--        Extensionality (λ f g →
--                          (x₁ : Fin x) →
--                          _≡_ (f x₁) (g x₁))
--        (λ {x₁} ‵ {y₁} g →
--           (x₂ : Term x) →
--           _≡_ {𝔣} {Term y} (‵ x₂) (g x₂))
--        _◃_ _◃_
--   Extensionality.extensionality ex = ◃-extensionality

-- open import Oscar.Property.Preservativity

-- instance

--   pres : ∀ {x y z} →
--          Preservativity {𝔣}
--          {Fin y → Term z} {𝔣}
--          {λ _ → Fin x → Term y} {𝔣}
--          {λ x₁ _ → Fin x → Term z}
--          (λ ‵ g x₁ → _◃_ {y} {z} ‵ (g x₁)) {𝔣}
--          {Term y →
--           Term z}
--          {𝔣}
--          {λ _ →
--             Term x →
--             Term y}
--          {𝔣}
--          {λ x₁ _ →
--             Term x →
--             Term z}
--          (λ ‵ f x₁ → ‵ (f x₁)) {𝔣}
--          (λ {x₁} {y₁} f g →
--             (x₂ : Term x) →
--             _≡_ {𝔣} {Term z} (f x₂) (g x₂))
--          (_◃_ {y} {z}) (λ {x₁} → _◃_ {x} {y}) (λ {x₁} {y₁} → _◃_ {x} {z})
--   Preservativity.preservativity pres ρ₂ ρ₁ t = ◃-associativity' t ρ₁ ρ₂

-- semifunctor : Semifunctor _ _ _ _ _ _
-- Semifunctor.semigroupoid₁ semifunctor = SemigroupoidSubstitution
-- Semifunctor.semigroupoid₂ semifunctor = SemigroupoidIndexedFunction Term
-- Semifunctor.μ semifunctor = id
-- Semifunctor.𝔣 semifunctor = _◃_


text:
------------------------------------------------------------------------
-- A parser for PBM images; illustrates essential use of bind
------------------------------------------------------------------------

-- Note that I am using the simple "Plain PBM" format, and I try to
-- adhere to the following statement from the pbm man page:
--
--   "Programs that read this format should be as lenient as possible,
--   accepting anything that looks remotely like a bitmap."

-- The idea to write this particular parser was taken from "The Power
-- of Pi" by Oury and Swierstra.

module RecursiveDescent.Hybrid.PBM where

import Data.Vec as Vec
open Vec using (Vec; _++_; [_])
import Data.List as List
open import Data.Nat
import Data.String as String
open String using (String) renaming (_++_ to _<+>_)
import Data.Char as Char
open Char using (Char; _==_)
open import Data.Product.Record
open import Data.Function
open import Data.Bool
open import Data.Unit
open import Data.Maybe
import Data.Nat.Show as N
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import RecursiveDescent.Index
open import RecursiveDescent.Hybrid
open import RecursiveDescent.Hybrid.Lib
open Token Char.decSetoid
open import RecursiveDescent.Hybrid.Simple

------------------------------------------------------------------------
-- The PBM type

data Colour : Set where
  white : Colour
  black : Colour

Matrix : Set -> ℕ -> ℕ -> Set
Matrix a rows cols = Vec (Vec a cols) rows

record PBM : Set where
  field
    rows   : ℕ
    cols   : ℕ
    matrix : Matrix Colour rows cols

open PBM

makePBM : forall {rows cols} -> Matrix Colour rows cols -> PBM
makePBM m = record { rows = _; cols = _; matrix = m }

------------------------------------------------------------------------
-- Showing PBM images

showColour : Colour -> Char
showColour white = '0'
showColour black = '1'

show : PBM -> String
show i = "P1 # Generated using Agda.\n" <+>
         N.show (cols i) <+> " " <+> N.show (rows i) <+> "\n" <+>
         showMatrix (matrix i)
  where
  showMatrix = String.fromList ∘
               Vec.toList ∘
               Vec.concat ∘
               Vec.map ((\xs -> xs ++ [ '\n' ]) ∘ Vec.map showColour)

------------------------------------------------------------------------
-- Parsing PBM images

data NT : ParserType where
  comment : NT _ ⊤
  colour  : NT _ Colour
  pbm     : NT _ PBM

grammar : Grammar Char NT
grammar comment  = tt <$ sym '#' <⊛ sat' (not ∘ _==_ '\n') ⋆ <⊛ sym '\n'
grammar colour   = white <$ sym '0'
                 ∣ black <$ sym '1'
grammar pbm      =
  w∣c ⋆ ⊛>
  string (String.toVec "P1") ⊛>
  w∣c ⋆ ⊛>
  number !>>= \cols ->  -- _>>=_ works just as well.
  w∣c + ⊛>
  number >>=  \rows ->  -- _!>>=_ works just as well.
  w∣c ⊛>
  (makePBM <$> exactly rows (exactly cols (w∣c ⋆ ⊛> ! colour))) <⊛
  any ⋆
  where w∣c = whitespace ∣ ! comment

module Example where

  open Vec

  image = makePBM ((white ∷ black ∷ []) ∷
                   (black ∷ white ∷ []) ∷
                   (black ∷ black ∷ []) ∷ [])

  ex₁ : parse-complete (! pbm) grammar (String.toList (show image)) ≡
        List.[_] image
  ex₁ = refl


text:
{-# OPTIONS --no-qualified-instances #-}
module CF.Compile where

open import Data.Product
open import Data.List hiding (null; [_])
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Unary
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax
open import Relation.Ternary.Monad.Possibly
open import Relation.Ternary.Monad.Weakening
open import Relation.Ternary.Data.ReflexiveTransitive

open import CF.Syntax as Src
open import CF.Contexts.Lexical

open import CF.Transform.Hoist
open import CF.Transform.UnCo
open import CF.Transform.Compile.Expressions
open import CF.Transform.Compile.Statements
open import CF.Transform.Compile.ToJVM

open import JVM.Builtins
open import JVM.Types
open import JVM.Contexts
open import JVM.Syntax.Values
open import JVM.Syntax.Instructions
open import JVM.Transform.Noooops
open import JVM.Compiler

module _ {T : Set} where
  open import JVM.Model T public

compile : ∀ {r} → Src.Block r [] → ∃ λ Γ → ε[ ⟪ Γ ∣ [] ↝ [] ⟫ ]
compile bl₁                       with hoist bl₁
... | _ , Possibly.possibly (intros r refl) bl₂  -- The grading of the possibility modality
                                                 -- proves that only the lexical context has been extended
          with unco bl₂
... | bl₃ with execCompiler (compiler [] bl₃)
... | bl₄ with noooop bl₄
... | bl₅ = -, bl₅


text:
open import Agda.Primitive
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

record R {A : Set} {B : A → Set} (p) : Set where
  field
    prf : p ≡ p

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --without-K #-}
module level where

open import Agda.Primitive public
  using    (Level; _⊔_; lzero; lsuc)

record ↑ {a} ℓ (A : Set a) : Set (a ⊔ ℓ) where
  constructor lift
  field lower : A

open ↑ public


text:
{-

Type quotients:

-}

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

open import Cubical.HITs.TypeQuotients.Base

open import Cubical.Core.Everything

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.HITs.PropositionalTruncation as PropTrunc using (∥_∥ ; ∣_∣ ; squash)
open import Cubical.HITs.SetTruncation as SetTrunc using (∥_∥₂ ; ∣_∣₂ ; squash₂
                                                              ; setTruncIsSet)

private
  variable
    ℓ ℓ' ℓ'' : Level
    A : Type ℓ
    R : A → A → Type ℓ'
    B : A /ₜ R → Type ℓ''
    C : A /ₜ R → A /ₜ R → Type ℓ''

elim : (f : (a : A) → (B [ a ]))
     → ((a b : A) (r : R a b) → PathP (λ i → B (eq/ a b r i)) (f a) (f b))
    ------------------------------------------------------------------------
     → (x : A /ₜ R) → B x
elim f feq [ a ] = f a
elim f feq (eq/ a b r i) = feq a b r i

rec : {X : Type ℓ''}
    → (f : A → X)
    → (∀ (a b : A) → R a b → f a ≡ f b)
   -------------------------------------
    → A /ₜ R → X
rec f feq [ a ] = f a
rec f feq (eq/ a b r i) = feq a b r i

elimProp : ((x : A /ₜ R ) → isProp (B x))
         → ((a : A) → B ( [ a ]))
        ---------------------------------
         → (x : A /ₜ R) → B x
elimProp Bprop f [ a ] = f a
elimProp Bprop f (eq/ a b r i) = isOfHLevel→isOfHLevelDep 1 Bprop (f a) (f b) (eq/ a b r) i

elimProp2 : ((x y : A /ₜ R ) → isProp (C x y))
          → ((a b : A) → C [ a ] [ b ])
         --------------------------------------
          → (x y : A /ₜ R) → C x y
elimProp2 Cprop f = elimProp (λ x → isPropΠ (λ y → Cprop x y))
                             (λ x → elimProp (λ y → Cprop [ x ] y) (f x))

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module OldBasicILP.UntypedSyntax.Translation where

open import OldBasicILP.UntypedSyntax.Common public

import OldBasicILP.UntypedSyntax.ClosedHilbertSequential as CHS
import OldBasicILP.UntypedSyntax.ClosedHilbert as CH

-- Translation of types parametrised by a closed, untyped representation of syntax.

_↦ᵀ_ : ∀ {Rep Rep′} → (Rep → Rep′) → ClosedSyntax.Ty Rep → ClosedSyntax.Ty Rep′
f ↦ᵀ (ClosedSyntax.α P)   = ClosedSyntax.α P
f ↦ᵀ (A ClosedSyntax.▻ B) = f ↦ᵀ A ClosedSyntax.▻ f ↦ᵀ B
f ↦ᵀ (p ClosedSyntax.⦂ A) = f p ClosedSyntax.⦂ f ↦ᵀ A
f ↦ᵀ (A ClosedSyntax.∧ B) = f ↦ᵀ A ClosedSyntax.∧ f ↦ᵀ B
f ↦ᵀ ClosedSyntax.⊤      = ClosedSyntax.⊤

-- Translation from closed Hilbert-style sequential to closed Hilbert-style.

chsᴿ→chᴿ : ∀ {n} → CHS.Rep n → Fin n → CH.Rep
chsᴿ→chᴿ (CHS.MP i j r) zero    = CH.APP (chsᴿ→chᴿ r i) (chsᴿ→chᴿ r j)
chsᴿ→chᴿ (CHS.CI r)     zero    = CH.CI
chsᴿ→chᴿ (CHS.CK r)     zero    = CH.CK
chsᴿ→chᴿ (CHS.CS r)     zero    = CH.CS
chsᴿ→chᴿ (CHS.NEC `r r) zero    = CH.BOX (chsᴿ→chᴿ `r zero)
chsᴿ→chᴿ (CHS.CDIST r)  zero    = CH.CDIST
chsᴿ→chᴿ (CHS.CUP r)    zero    = CH.CUP
chsᴿ→chᴿ (CHS.CDOWN r)  zero    = CH.CDOWN
chsᴿ→chᴿ (CHS.CPAIR r)  zero    = CH.CPAIR
chsᴿ→chᴿ (CHS.CFST r)   zero    = CH.CFST
chsᴿ→chᴿ (CHS.CSND r)   zero    = CH.CSND
chsᴿ→chᴿ (CHS.UNIT r)   zero    = CH.UNIT
chsᴿ→chᴿ (CHS.MP i j r) (suc k) = chsᴿ→chᴿ r k
chsᴿ→chᴿ (CHS.CI r)     (suc k) = chsᴿ→chᴿ r k
chsᴿ→chᴿ (CHS.CK r)     (suc k) = chsᴿ→chᴿ r k
chsᴿ→chᴿ (CHS.CS r)     (suc k) = chsᴿ→chᴿ r k
chsᴿ→chᴿ (CHS.NEC `r r) (suc k) = chsᴿ→chᴿ r k
chsᴿ→chᴿ (CHS.CDIST r)  (suc k) = chsᴿ→chᴿ r k
chsᴿ→chᴿ (CHS.CUP r)    (suc k) = chsᴿ→chᴿ r k
chsᴿ→chᴿ (CHS.CDOWN r)  (suc k) = chsᴿ→chᴿ r k
chsᴿ→chᴿ (CHS.CPAIR r)  (suc k) = chsᴿ→chᴿ r k
chsᴿ→chᴿ (CHS.CFST r)   (suc k) = chsᴿ→chᴿ r k
chsᴿ→chᴿ (CHS.CSND r)   (suc k) = chsᴿ→chᴿ r k
chsᴿ→chᴿ (CHS.UNIT r)   (suc k) = chsᴿ→chᴿ r k

chsᴾ→chᴾ : CHS.Proof → CH.Proof
chsᴾ→chᴾ CHS.[ r ] = CH.[ chsᴿ→chᴿ r zero ]

chsᵀ→chᵀ : CHS.Ty → CH.Ty
chsᵀ→chᵀ = chsᴾ→chᴾ ↦ᵀ_

-- FIXME: What is going on here?
postulate
  ᴬlem₁ : ∀ {n₁ n₂} → (r₁ : CHS.Rep (suc n₁)) → (r₂ : CHS.Rep (suc n₂))
          → chsᴿ→chᴿ (CHS.APP r₁ r₂) zero ≡ CH.APP (chsᴿ→chᴿ r₁ zero) (chsᴿ→chᴿ r₂ zero)

mutual
  chsᴰ→ch : ∀ {Ξ A} → CHS.⊢ᴰ Ξ → A ∈ Ξ → CH.⊢ chsᵀ→chᵀ A
  chsᴰ→ch (CHS.mp i j d)               top     = CH.app (chsᴰ→ch d i) (chsᴰ→ch d j)
  chsᴰ→ch (CHS.ci d)                   top     = CH.ci
  chsᴰ→ch (CHS.ck d)                   top     = CH.ck
  chsᴰ→ch (CHS.cs d)                   top     = CH.cs
  chsᴰ→ch (CHS.nec `d d)               top     rewrite ᴬlem₂ `d top = CH.box (chsᴰ→ch `d top)
  chsᴰ→ch (CHS.cdist {r₁ = r₁} {r₂} d) top     rewrite ᴬlem₁ r₁ r₂  = CH.cdist
  chsᴰ→ch (CHS.cup d)                  top     = CH.cup
  chsᴰ→ch (CHS.cdown d)                top     = CH.cdown
  chsᴰ→ch (CHS.cpair d)                top     = CH.cpair
  chsᴰ→ch (CHS.cfst d)                 top     = CH.cfst
  chsᴰ→ch (CHS.csnd d)                 top     = CH.csnd
  chsᴰ→ch (CHS.unit d)                 top     = CH.unit
  chsᴰ→ch (CHS.mp i j d)               (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.ci d)                   (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.ck d)                   (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.cs d)                   (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.nec `d d)               (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.cdist d)                (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.cup d)                  (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.cdown d)                (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.cpair d)                (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.cfst d)                 (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.csnd d)                 (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.unit d)                 (pop k) = chsᴰ→ch d k

  ᴬlem₂ : ∀ {Ξ A} → (d : CHS.⊢ᴰ Ξ) → (k : A ∈ Ξ)
         → chsᴿ→chᴿ CHS.ᴿ⌊ d ⌋ ⁱ⌊ k ⌋ ≡ CH.ᴿ⌊ chsᴰ→ch d k ⌋
  ᴬlem₂ CHS.nil                      ()
  ᴬlem₂ (CHS.mp i j d)               top     = cong² CH.APP (ᴬlem₂ d i) (ᴬlem₂ d j)
  ᴬlem₂ (CHS.ci d)                   top     = refl
  ᴬlem₂ (CHS.ck d)                   top     = refl
  ᴬlem₂ (CHS.cs d)                   top     = refl
  ᴬlem₂ (CHS.nec `d d)               top     rewrite ᴬlem₂ `d top = cong CH.BOX refl
  ᴬlem₂ (CHS.cdist {r₁ = r₁} {r₂} d) top     rewrite ᴬlem₁ r₁ r₂ = refl
  ᴬlem₂ (CHS.cup d)                  top     = refl
  ᴬlem₂ (CHS.cdown d)                top     = refl
  ᴬlem₂ (CHS.cpair d)                top     = refl
  ᴬlem₂ (CHS.cfst d)                 top     = refl
  ᴬlem₂ (CHS.csnd d)                 top     = refl
  ᴬlem₂ (CHS.unit d)                 top     = refl
  ᴬlem₂ (CHS.mp i j d)               (pop k) = ᴬlem₂ d k
  ᴬlem₂ (CHS.ci d)                   (pop k) = ᴬlem₂ d k
  ᴬlem₂ (CHS.ck d)                   (pop k) = ᴬlem₂ d k
  ᴬlem₂ (CHS.cs d)                   (pop k) = ᴬlem₂ d k
  ᴬlem₂ (CHS.nec `d d)               (pop k) = ᴬlem₂ d k
  ᴬlem₂ (CHS.cdist d)                (pop k) = ᴬlem₂ d k
  ᴬlem₂ (CHS.cup d)                  (pop k) = ᴬlem₂ d k
  ᴬlem₂ (CHS.cdown d)                (pop k) = ᴬlem₂ d k
  ᴬlem₂ (CHS.cpair d)                (pop k) = ᴬlem₂ d k
  ᴬlem₂ (CHS.cfst d)                 (pop k) = ᴬlem₂ d k
  ᴬlem₂ (CHS.csnd d)                 (pop k) = ᴬlem₂ d k
  ᴬlem₂ (CHS.unit d)                 (pop k) = ᴬlem₂ d k

chs→ch : ∀ {A} → CHS.⊢ A → CH.⊢ chsᵀ→chᵀ A
chs→ch (Ξ , d) = chsᴰ→ch d top

-- Translation from closed Hilbert-style to closed Hilbert-style sequential.

chᴿ→chsᴿ : CH.Rep → ∃ (λ n → CHS.Rep (suc n))
chᴿ→chsᴿ (CH.APP r₁ r₂) with chᴿ→chsᴿ r₁ | chᴿ→chsᴿ r₂
chᴿ→chsᴿ (CH.APP r₁ r₂) | (n₁ , r₁′) | (n₂ , r₂′) = suc n₂ + suc n₁ , CHS.APP r₁′ r₂′
chᴿ→chsᴿ CH.CI          = zero , CHS.CI CHS.NIL
chᴿ→chsᴿ CH.CK          = zero , CHS.CK CHS.NIL
chᴿ→chsᴿ CH.CS          = zero , CHS.CS CHS.NIL
chᴿ→chsᴿ (CH.BOX r)     with chᴿ→chsᴿ r
chᴿ→chsᴿ (CH.BOX r)     | (n , r′) = zero , CHS.BOX r′
chᴿ→chsᴿ CH.CDIST       = zero , CHS.CDIST CHS.NIL
chᴿ→chsᴿ CH.CUP         = zero , CHS.CUP CHS.NIL
chᴿ→chsᴿ CH.CDOWN       = zero , CHS.CDOWN CHS.NIL
chᴿ→chsᴿ CH.CPAIR       = zero , CHS.CPAIR CHS.NIL
chᴿ→chsᴿ CH.CFST        = zero , CHS.CFST CHS.NIL
chᴿ→chsᴿ CH.CSND        = zero , CHS.CSND CHS.NIL
chᴿ→chsᴿ CH.UNIT        = zero , CHS.UNIT CHS.NIL

chᴾ→chsᴾ : CH.Proof → CHS.Proof
chᴾ→chsᴾ CH.[ r ] with chᴿ→chsᴿ r
chᴾ→chsᴾ CH.[ r ] | (n , r′) = CHS.[ r′ ]

chᵀ→chsᵀ : CH.Ty → CHS.Ty
chᵀ→chsᵀ = chᴾ→chsᴾ ↦ᵀ_

distᴺ⌊⌋+ : ∀ {U} → (Γ Γ′ : Cx U) → ᴺ⌊ Γ ⧺ Γ′ ⌋ ≡ ᴺ⌊ Γ ⌋ + ᴺ⌊ Γ′ ⌋
distᴺ⌊⌋+ Γ ∅        = refl
distᴺ⌊⌋+ Γ (Γ′ , A) = cong suc (distᴺ⌊⌋+ Γ Γ′)

mutual
  ch→chs : ∀ {A} → CH.⊢ A → CHS.⊢ chᵀ→chsᵀ A
  ch→chs (CH.app d₁ d₂) = CHS.app (ch→chs d₁) (ch→chs d₂)
  ch→chs CH.ci          = ∅ , CHS.ci CHS.nil
  ch→chs CH.ck          = ∅ , CHS.ck CHS.nil
  ch→chs CH.cs          = ∅ , CHS.cs CHS.nil
  ch→chs (CH.box d)     rewrite ᴮlem₁ d = CHS.box (ch→chs d)
  ch→chs CH.cdist       = ∅ , CHS.cdist CHS.nil
  ch→chs CH.cup         = ∅ , CHS.cup CHS.nil
  ch→chs CH.cdown       = ∅ , CHS.cdown CHS.nil
  ch→chs CH.cpair       = ∅ , CHS.cpair CHS.nil
  ch→chs CH.cfst        = ∅ , CHS.cfst CHS.nil
  ch→chs CH.csnd        = ∅ , CHS.csnd CHS.nil
  ch→chs CH.unit        = ∅ , CHS.unit CHS.nil

  -- FIXME: This should hold by ᴮlem₂.
  postulate
    ᴮlem₁ : ∀ {A} → (d : CH.⊢ A)
           → chᴿ→chsᴿ CH.ᴿ⌊ d ⌋ ≡ ᴺ⌊ π₁ (ch→chs d) ⌋ , CHS.ᴿ⌊ π₂ (ch→chs d) ⌋

  ᴮlem₂ : ∀ {A} → (d : CH.⊢ A)
         → ᴺ⌊ π₁ (ch→chs d) ⌋ ≡ π₁ (chᴿ→chsᴿ CH.ᴿ⌊ d ⌋)
  ᴮlem₂ (CH.app d₁ d₂) rewrite ᴮlem₂ d₂ | ᴮlem₃ d₁ d₂ = cong suc refl
  ᴮlem₂ CH.ci          = refl
  ᴮlem₂ CH.ck          = refl
  ᴮlem₂ CH.cs          = refl
  ᴮlem₂ (CH.box d)     rewrite ᴮlem₂ d | ᴮlem₁ d = refl
  ᴮlem₂ CH.cdist       = refl
  ᴮlem₂ CH.cup         = refl
  ᴮlem₂ CH.cdown       = refl
  ᴮlem₂ CH.cpair       = refl
  ᴮlem₂ CH.cfst        = refl
  ᴮlem₂ CH.csnd        = refl
  ᴮlem₂ CH.unit        = refl

  ᴮlem₃ : ∀ {A B} → (d₁ : CH.⊢ A CH.▻ B) → (d₂ : CH.⊢ A)
         → ᴺ⌊ (π₁ (ch→chs d₂) , chᵀ→chsᵀ A) ⧺ π₁ (ch→chs d₁) ⌋ ≡
            suc (π₁ (chᴿ→chsᴿ CH.ᴿ⌊ d₂ ⌋)) + π₁ (chᴿ→chsᴿ CH.ᴿ⌊ d₁ ⌋)
  ᴮlem₃ {A} d₁ d₂ rewrite distᴺ⌊⌋+ (π₁ (ch→chs d₂) , chᵀ→chsᵀ A) (π₁ (ch→chs d₁)) =
                  cong² _+_ (cong suc (ᴮlem₂ d₂)) (ᴮlem₂ d₁)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
open import Nat
open import Prelude
open import dynamics-core
open import contexts
open import typed-elaboration
open import lemmas-gcomplete
open import lemmas-complete
open import progress-checks
open import finality

module cast-inert where
  -- if a term is compelete and well typed, then the casts inside are all
  -- identity casts and there are no failed casts
  cast-inert : ∀{Δ Γ d τ} →
               d dcomplete →
               Δ , Γ ⊢ d :: τ →
               cast-id d
  cast-inert dc TANum = CINum
  cast-inert (DCPlus dc dc₁) (TAPlus wt wt₁) = CIPlus (cast-inert dc wt) (cast-inert dc₁ wt₁)
  cast-inert dc (TAVar x₁) = CIVar
  cast-inert (DCLam dc x₁) (TALam x₂ wt) = CILam (cast-inert dc wt)
  cast-inert (DCAp dc dc₁) (TAAp wt wt₁) = CIAp (cast-inert dc wt) (cast-inert dc₁ wt₁)
  cast-inert (DCInl x dc) (TAInl wt) = CIInl (cast-inert dc wt)
  cast-inert (DCInr x dc) (TAInr wt) = CIInr (cast-inert dc wt)
  cast-inert (DCCase dc dc₁ dc₂) (TACase wt x wt₁ x₁ wt₂) =
    CICase (cast-inert dc wt) (cast-inert dc₁ wt₁) (cast-inert dc₂ wt₂)
  cast-inert (DCPair dc dc₁) (TAPair wt wt₁) = CIPair (cast-inert dc wt) (cast-inert dc₁ wt₁)
  cast-inert (DCFst dc) (TAFst wt) = CIFst (cast-inert dc wt)
  cast-inert (DCSnd dc) (TASnd wt) = CISnd (cast-inert dc wt)
  cast-inert () (TAEHole x x₁)
  cast-inert () (TANEHole x wt x₁)
  cast-inert (DCCast dc x x₁) (TACast wt x₂)
    with complete-consistency x₂ x x₁
  ... | refl = CICast (cast-inert dc wt)
  cast-inert () (TAFailedCast wt x x₁ x₂)

  -- in a well typed complete internal expression, every cast is the
  -- identity cast.
  complete-casts : ∀{Γ Δ d τ1 τ2} →
                   Γ , Δ ⊢ d ⟨ τ1 ⇒ τ2 ⟩ :: τ2 →
                   d ⟨ τ1 ⇒ τ2 ⟩ dcomplete →
                   τ1 == τ2
  complete-casts wt comp with cast-inert comp wt
  complete-casts wt comp | CICast qq = refl

  -- relates expressions to the same thing with all identity casts
  -- removed. note that this is a syntactic rewrite and it goes under
  -- binders.
  data no-id-casts : ihexp → ihexp → Set where
    NICNum    : ∀{n} →
                no-id-casts (N n) (N n)
    NICPlus   : ∀{d1 d2 d1' d2'} →
                no-id-casts d1 d1' →
                no-id-casts d2 d2' →
                no-id-casts (d1 ·+ d2) (d1' ·+ d2')
    NICVar    : ∀{x} →
                no-id-casts (X x) (X x)
    NICLam    : ∀{x τ d d'} →
                no-id-casts d d' →
                no-id-casts (·λ x ·[ τ ] d) (·λ x ·[ τ ] d')
    NICAp     : ∀{d1 d2 d1' d2'} →
                no-id-casts d1 d1' →
                no-id-casts d2 d2' →
                no-id-casts (d1 ∘ d2) (d1' ∘ d2')
    NICInl    : ∀{d τ d'} →
                no-id-casts d d' →
                no-id-casts (inl τ d) (inl τ d')
    NICInr    : ∀{d τ d'} →
                no-id-casts d d' →
                no-id-casts (inr τ d) (inr τ d')
    NICCase   : ∀{d x d1 y d2 d' d1' d2'} →
                no-id-casts d d' →
                no-id-casts d1 d1' →
                no-id-casts d2 d2' →
                no-id-casts (case d x d1 y d2) (case d' x d1' y d2')
    NICPair   : ∀{d1 d2 d1' d2'} →
                no-id-casts d1 d1' →
                no-id-casts d2 d2' →
                no-id-casts ⟨ d1 , d2 ⟩ ⟨ d1' , d2' ⟩
    NICFst    : ∀{d d'} →
                no-id-casts d d' →
                no-id-casts (fst d) (fst d')
    NICSnd    : ∀{d d'} →
                no-id-casts d d' →
                no-id-casts (snd d) (snd d')
    NICHole   : ∀{u} →
                no-id-casts (⦇-⦈⟨ u ⟩) (⦇-⦈⟨ u ⟩)
    NICNEHole : ∀{d d' u} →
                no-id-casts d d' →
                no-id-casts (⦇⌜ d ⌟⦈⟨ u ⟩) (⦇⌜ d' ⌟⦈⟨ u ⟩)
    NICCast   : ∀{d d' τ} →
                no-id-casts d d' →
                no-id-casts (d ⟨ τ ⇒ τ ⟩) d'
    NICFailed : ∀{d d' τ1 τ2} →
                no-id-casts d d' →
                no-id-casts (d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩) (d' ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩)

  -- removing identity casts doesn't change the type
  no-id-casts-type : ∀{Γ Δ d τ d' } → Δ , Γ ⊢ d :: τ →
                                      no-id-casts d d' →
                                      Δ , Γ ⊢ d' :: τ
  no-id-casts-type TANum NICNum = TANum
  no-id-casts-type (TAPlus wt wt₁) (NICPlus nic nic₁) = TAPlus (no-id-casts-type wt nic) (no-id-casts-type wt₁ nic₁)
  no-id-casts-type (TAVar x₁) NICVar = TAVar x₁
  no-id-casts-type (TALam x₁ wt) (NICLam nic) = TALam x₁ (no-id-casts-type wt nic)
  no-id-casts-type (TAAp wt wt₁) (NICAp nic nic₁) = TAAp (no-id-casts-type wt nic) (no-id-casts-type wt₁ nic₁)
  no-id-casts-type (TAInl wt) (NICInl nic) = TAInl (no-id-casts-type wt nic)
  no-id-casts-type (TAInr wt) (NICInr nic) = TAInr (no-id-casts-type wt nic)
  no-id-casts-type (TACase wt x wt₁ x₁ wt₂) (NICCase nic nic₁ nic₂) = TACase (no-id-casts-type wt nic) x (no-id-casts-type wt₁ nic₁) x₁ (no-id-casts-type wt₂ nic₂)
  no-id-casts-type (TAPair wt wt₁) (NICPair nic nic₁) = TAPair (no-id-casts-type wt nic) (no-id-casts-type wt₁ nic₁)
  no-id-casts-type (TAFst wt) (NICFst nic) = TAFst (no-id-casts-type wt nic)
  no-id-casts-type (TASnd wt) (NICSnd nic) = TASnd (no-id-casts-type wt nic)
  no-id-casts-type (TAEHole x x₁) NICHole = TAEHole x x₁
  no-id-casts-type (TANEHole x wt x₁) (NICNEHole nic) = TANEHole x (no-id-casts-type wt nic) x₁
  no-id-casts-type (TACast wt x) (NICCast nic) = no-id-casts-type wt nic
  no-id-casts-type (TAFailedCast wt x x₁ x₂) (NICFailed nic) = TAFailedCast (no-id-casts-type wt nic) x x₁ x₂

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module PatternMatchingLambda where

data Bool : Set where
  true false : Bool

data Void : Set where

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

and : Bool -> Bool -> Bool
and = λ { true x → x ; false _ → false }

or : Bool -> Bool -> Bool
or x y = not (and (not x) (not y))
  where not : Bool -> Bool
        not = \ { true -> false ; false -> true }

iff : Bool -> Bool -> Bool -> Bool
iff = λ { true  x -> λ { true → true ; false → false } ;
          false x -> λ { true -> false ; false -> true }
        }

pattern-matching-lambdas-compute : (x : Bool) -> or true x ≡ true
pattern-matching-lambdas-compute x = refl

isTrue : Bool -> Set
isTrue = \ { true -> Bool ; false -> Void }

absurd : (x : Bool) -> isTrue x -> Bool
absurd = \ { true x -> x ; false () }

--carefully chosen without eta, so that pattern matching is needed
data Unit : Set where
  unit : Unit

isNotUnit : Unit -> Set
isNotUnit = \ { tt -> Void }

absurd-one-clause : (x : Unit) -> isNotUnit x -> Bool
absurd-one-clause = λ { tt ()}

data indexed-by-xor : (Bool -> Bool -> Bool) -> Set where
  c : (b : Bool) -> indexed-by-xor \ { true  true  -> false ;
                                       false false -> false ;
                                       _     _     -> true  }

-- won't work if the underscore is replaced with the actual value at the moment
f : (r : Bool -> Bool -> Bool) -> indexed-by-xor r -> Bool
f ._ (c b) = b

record Σ (A : Set)(B : A -> Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

fst : {A : Set}{B : A -> Set} -> (x : Σ A B) -> A
fst =  \ { (a , b) -> a }

snd : {A : Set}{B : A -> Set} -> (x : Σ A B) -> B (fst x)
snd = \ { (a , b) -> b }

record FamSet : Set1 where
  constructor _,_
  field
    A : Set
    B : A -> Set

ΣFAM : (A : Set)(B : A -> Set)(P : A -> Set)(Q : (x : A) -> B x -> P x -> Set) -> FamSet
ΣFAM A B P Q = (Σ A P , \ { (a , p) -> Σ (B a) (λ b → Q a b p) } )

--The syntax doesn't interfere with hidden lambdas etc:
postulate
  P : ({x : Bool} -> Bool) -> Set
  p : P (λ {x} → x)

--Issue 446: Absurd clauses can appear inside more complex expressions
data Box (A : Set) : Set where
  box : A → Box A

foo : {A : Set} → Box Void → A
foo = λ { (box ()) }

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


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

open import Generics.Prelude
open import Generics.Telescope
open import Generics.Desc
open import Generics.Mu
open import Generics.Mu.All

module Generics.Mu.Elim
  {P I n} {D : DataDesc P I n}
  {p c} (Pr : ∀ {i} → μ D (p , i) → Set c)
  (f : ∀ {i} (x : μ D (p , i)) → All D Pr x → Pr x) where

private
  variable
    V : ExTele P
    i : ⟦ I ⟧tel p
    v : ⟦ V ⟧tel p

private
  Pr′ : ∀{i} → μ D (p , i) → Setω
  Pr′ x = Liftω (Pr x)

all : (x : μ D (p , i)) → All D Pr x

allIndArg : (C : ConDesc P V I)
            (x : ⟦ C ⟧IndArgω (μ D) (p , v))
          → AllIndArgωω Pr′ C x
allIndArg (var _) x = liftω (f x (all x))
allIndArg (A ⊗ B) (xa , xb) = allIndArg A xa , allIndArg B xb
allIndArg (π _ _ C) x s = allIndArg C (x s)

allCon : (C : ConDesc P V I)
         (x : ⟦ C ⟧Conω (μ D) (p , v , i))
       → AllConωω Pr′ C x
allCon (var _) x = tt
allCon (A ⊗ B) (xa , xb) = allIndArg A xa , allCon B xb
allCon (π _ _ C) (_ , x) = allCon C x

all ⟨ k , x ⟩ = allCon (lookupCon D k) x

elim : (x : μ D (p , i)) → Pr x
elim x = f x (all x)

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
------------------------------------------------------------------------
-- The two big-step semantics given by Leroy and Grall in "Coinductive
-- big-step operational semantics"
------------------------------------------------------------------------

module Lambda.Substitution.TwoSemantics where

open import Codata.Musical.Notation

open import Lambda.Syntax
open WHNF
open import Lambda.Substitution

-- Big-step semantics for terminating computations.

infix 4 _⇓_

data _⇓_ {n} : Tm n → Value n → Set where
  val : ∀ {v} → ⌜ v ⌝ ⇓ v
  app : ∀ {t₁ t₂ t v v′}
        (t₁⇓   : t₁ ⇓ ƛ t)
        (t₂⇓   : t₂ ⇓ v)
        (t₁t₂⇓ : t / sub ⌜ v ⌝ ⇓ v′) →
        t₁ · t₂ ⇓ v′

-- Big-step semantics for non-terminating computations.

infix 4 _⇑

data _⇑ {n} : Tm n → Set where
  ·ˡ  : ∀ {t₁ t₂}
        (t₁⇑ : ∞ (t₁ ⇑)) →
        t₁ · t₂ ⇑
  ·ʳ  : ∀ {t₁ t₂ v}
        (t₁⇓ : t₁ ⇓ v)
        (t₂⇑ : ∞ (t₂ ⇑)) →
        t₁ · t₂ ⇑
  app : ∀ {t₁ t₂ t v}
        (t₁⇓   : t₁ ⇓ ƛ t)
        (t₂⇓   : t₂ ⇓ v)
        (t₁t₂⇓ : ∞ (t / sub ⌜ v ⌝ ⇑)) →
        t₁ · t₂ ⇑

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
------------------------------------------------------------------------
-- Inversion of canonical subtyping in Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Kinding.Canonical.Inversion where

open import Data.Product using (_,_; _×_; proj₁; proj₂)
open import Data.Vec using ([]; _∷_; foldl)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂)
open import Relation.Nullary using (¬_)

open import FOmegaInt.Syntax
open import FOmegaInt.Kinding.Canonical
open import FOmegaInt.Kinding.Canonical.Validity

open Syntax
open ElimCtx
open Kinding
open ContextNarrowing

------------------------------------------------------------------------
-- Inversion of canonical subtyping (in the empty context).

-- NOTE.  The lemmas in this module only hold in the empty context
-- because we can not invert instances of the interval projection
-- rules (<:-⟨| and (<:-|⟩) in arbitrary contexts.  This is because
-- instances of these rules can reflect arbitrary subtyping
-- assumptions into the subtyping relation.  Consider, e.g.
--
--     Γ, X :: ⊤..⊥ ctx    Γ(X) = ⊥..⊤
--     ------------------------------- (∈-var)
--     Γ, X :: ⊤..⊥ ⊢ X :: ⊤..⊥
--     -------------------------- (<:-⟨|, <:-|⟩)
--     Γ, X :: ⊤..⊥ ⊢ ⊤ <: X <: ⊥
--
-- Which allows us to prove that ⊤ <: ⊥ using (<:-trans) under the
-- assumption (X : ⊤..⊥).  On the other hand, it is impossible to give
-- a transitivity-free proof of ⊤ <: ⊥.  In general, it is therefore
-- impossible to invert subtyping statements in non-empty contexts,
-- i.e. one cannot prove lemmas like (<:-→-inv) or (<:-∀-inv) below
-- for arbitrary contexts.

infix 4 ⊢_<!_

-- Top-level transitivity-free canonical subtyping in the empty
-- context.
data ⊢_<!_ : Elim 0 → Elim 0 → Set where
  <!-⊥ : ∀ {a} → [] ⊢Nf a ⇉ a ⋯ a → ⊢ ⊥∙ <! a
  <!-⊤ : ∀ {a} → [] ⊢Nf a ⇉ a ⋯ a → ⊢ a  <! ⊤∙
  <!-∀ : ∀ {k₁ k₂ a₁ a₂} → [] ⊢ k₂ <∷ k₁ → kd k₂ ∷ [] ⊢ a₁ <: a₂ →
         [] ⊢Nf ∀∙ k₁ a₁ ⇉ ∀∙ k₁ a₁ ⋯ ∀∙ k₁ a₁ → ⊢ ∀∙ k₁ a₁ <! ∀∙ k₂ a₂
  <!-→ : ∀ {a₁ a₂ b₁ b₂} → [] ⊢ a₂ <: a₁ → [] ⊢ b₁ <: b₂ →
         ⊢ a₁ ⇒∙ b₁ <! a₂ ⇒∙ b₂

-- Soundness of <! with respect to <: in the empty context.
sound-<! : ∀ {a b : Elim 0} → ⊢ a <! b → [] ⊢ a <: b
sound-<! (<!-⊥ a⇉a⋯a)         = <:-⊥ a⇉a⋯a
sound-<! (<!-⊤ a⇉a⋯a)         = <:-⊤ a⇉a⋯a
sound-<! (<!-∀ k₂<∷k₁ a₁<:a₂ Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁) =
  <:-∀ k₂<∷k₁ a₁<:a₂ Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁
sound-<! (<!-→ a₂<:a₁ b₁<:b₂) = <:-→ a₂<:a₁ b₁<:b₂

-- The only proper (top-level) subtype of ⊥ is ⊥ itself.
⊥-<!-min : ∀ {a : Elim 0} → ⊢ a <! ⊥∙ → a ≡ ⊥∙
⊥-<!-min (<!-⊥ _) = refl

-- The only proper (top-level) supertype of ⊤ is ⊤ itself.
⊤-<!-max : ∀ {a : Elim 0} → ⊢ ⊤∙ <! a → a ≡ ⊤∙
⊤-<!-max (<!-⊤ _) = refl

-- Arrows are not (top-level) subtypes of universals and vice-versa.

⇒-≮!-Π : ∀ {a : Elim 0} {k b₁ b₂} → ¬ ⊢ a ⇒∙ b₁ <! ∀∙ k b₂
⇒-≮!-Π ()

Π-≮!-⇒ : ∀ {a : Elim 0} {k b₁ b₂} → ¬ ⊢ ∀∙ k b₁ <! a ⇒∙ b₂
Π-≮!-⇒ ()

-- Validity of <!
<!-valid : ∀ {a b} → ⊢ a <! b → [] ⊢Nf a ⇉ a ⋯ a × [] ⊢Nf b ⇉ b ⋯ b
<!-valid a<!b = <:-valid (sound-<! a<!b)

-- Top-level transitivity of canonical subtyping is admissible.
<!-trans : ∀ {a b c} → [] ⊢ a <: b → ⊢ b <! c → ⊢ a <! c
<!-trans (<:-trans a<:b b<:c) c<!d = <!-trans a<:b (<!-trans b<:c c<!d)
<!-trans (<:-⊥ a⇉a⋯a) a<!d     = <!-⊥ (proj₂ (<!-valid a<!d))
<!-trans (<:-⊤ a⇉a⋯a) (<!-⊤ _) = <!-⊤ a⇉a⋯a
<!-trans (<:-∀ k₂<∷k₁ a₁<:a₂ Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁) (<!-⊤ _) =
  <!-⊤ (proj₁ (<:-valid (<:-∀ k₂<∷k₁ a₁<:a₂ Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁)))
<!-trans (<:-∀ k₂<∷k₁ a₁<:a₂ Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁) (<!-∀ k₃<∷k₂ a₂<:a₃ _) =
  <!-∀ (<∷-trans k₃<∷k₂ k₂<∷k₁)
       (<:-trans (⇓-<: k₃-kd k₃<∷k₂ a₁<:a₂) a₂<:a₃) Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁
  where k₃-kd = wf-kd-inv (wf-∷₁ (<:-ctx a₂<:a₃))
<!-trans (<:-→ a₂<:a₁ b₁<:b₂) (<!-⊤ a₂⇒b₂⇉a₂⇒b₂⋯a₂⇒b₂) =
  <!-⊤ (proj₁ (<:-valid (<:-→ a₂<:a₁ b₁<:b₂)))
<!-trans (<:-→ a₂<:a₁ b₁<:b₂) (<!-→ a₃<:a₂ b₂<:b₃) =
  <!-→ (<:-trans a₃<:a₂ a₂<:a₁) (<:-trans b₁<:b₂ b₂<:b₃)
<!-trans (<:-∙ {()} _ _)        b<!c
<!-trans (<:-⟨| (∈-∙ {()} _ _)) b<!c
<!-trans (<:-|⟩ (∈-∙ {()} _ _)) b<!c

-- Completeness of <! with respect to <: in the empty context.
complete-<! : ∀ {a b : Elim 0} → [] ⊢ a <: b → ⊢ a <! b
complete-<! (<:-trans a<:b b<:c) = <!-trans a<:b (complete-<! b<:c)
complete-<! (<:-⊥ a⇉a⋯a)         = <!-⊥ a⇉a⋯a
complete-<! (<:-⊤ a⇉a⋯a)         = <!-⊤ a⇉a⋯a
complete-<! (<:-∀ k₂<∷k₁ a₁<:a₂ Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁) =
  <!-∀ k₂<∷k₁ a₁<:a₂ Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁
complete-<! (<:-→ a₂<:a₁ b₁<:b₂) = <!-→ a₂<:a₁ b₁<:b₂
complete-<! (<:-∙ {()} _ _)
complete-<! (<:-⟨| (∈-∙ {()} _ _))
complete-<! (<:-|⟩ (∈-∙ {()} _ _))

-- The only proper (top-level) subtype of ⊥ is ⊥ itself.
⊥-<:-min : ∀ {a : Elim 0} → [] ⊢ a <: ⊥∙ → a ≡ ⊥∙
⊥-<:-min a<:⊥ = ⊥-<!-min (complete-<! a<:⊥)

-- The only proper (top-level) supertype of ⊤ is ⊤ itself.
⊤-<:-max : ∀ {a : Elim 0} → [] ⊢ ⊤∙ <: a → a ≡ ⊤∙
⊤-<:-max ⊤<:a = ⊤-<!-max (complete-<! ⊤<:a)

-- Inversion of canonical subtyping for universals and arrow types.

<:-∀-inv : ∀ {k₁ k₂ : Kind Elim 0} {a₁ a₂} → [] ⊢ ∀∙ k₁ a₁ <: ∀∙ k₂ a₂ →
           [] ⊢ k₂ <∷ k₁ × kd k₂ ∷ [] ⊢ a₁ <: a₂
<:-∀-inv Πk₁a₁<:Πk₂a₂ with complete-<! Πk₁a₁<:Πk₂a₂
<:-∀-inv Πk₁a₁<:Πk₂a₂ | <!-∀ k₂<∷k₁ a₁<:a₂ _ = k₂<∷k₁ , a₁<:a₂

<:-→-inv : ∀ {a₁ a₂ : Elim 0} {b₁ b₂} → [] ⊢ a₁ ⇒∙ b₁ <: a₂ ⇒∙ b₂ →
           [] ⊢ a₂ <: a₁ × [] ⊢ b₁ <: b₂
<:-→-inv a₁⇒b₁<:a₂⇒b₂ with complete-<! a₁⇒b₁<:a₂⇒b₂
<:-→-inv a₁⇒b₁<:a₂⇒b₂ | <!-→ a₂<∷a₁ b₁<:b₂ = a₂<∷a₁ , b₁<:b₂

-- Arrows are not canonical subtypes of universals and vice-versa.

⇒-≮:-Π : ∀ {a : Elim 0} {k b₁ b₂} → ¬ [] ⊢ a ⇒∙ b₁ <: ∀∙ k b₂
⇒-≮:-Π = ⇒-≮!-Π ∘ complete-<!

Π-≮:-⇒ : ∀ {a : Elim 0} {k b₁ b₂} → ¬ [] ⊢ ∀∙ k b₁ <: a ⇒∙ b₂
Π-≮:-⇒ = Π-≮!-⇒ ∘ complete-<!

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda