text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.ConsensusTypes.Block      as Block
import      LibraBFT.Impl.Consensus.ConsensusTypes.BlockData  as BlockData
import      LibraBFT.Impl.Consensus.ConsensusTypes.QuorumCert as QuorumCert
import      LibraBFT.Impl.Types.BlockInfo                     as BlockInfo
import      LibraBFT.Impl.Types.ValidatorVerifier             as ValidatorVerifier
open import LibraBFT.Impl.OBM.Crypto hiding (verify)
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.PKCS                                         hiding (verify)
open import Util.Prelude
open import Util.Hash
------------------------------------------------------------------------------
open import Data.String                                       using (String)

module LibraBFT.Impl.Consensus.ConsensusTypes.BlockRetrieval where

verify : BlockRetrievalResponse → HashValue → U64 → ValidatorVerifier → Either ErrLog Unit
verify self blockId numBlocks sigVerifier =
  grd‖ self ^∙ brpStatus /= BRSSucceeded ≔
       Left fakeErr -- here ["/= BRSSucceeded"]
     ‖ length (self ^∙ brpBlocks) /= numBlocks ≔
       Left fakeErr -- here ["not enough blocks returned", show (self^.brpBlocks), show numBlocks]
     ‖ otherwise≔
       verifyBlocks (self ^∙ brpBlocks)
 where
  here' : List String → List String
  here' t = "BlockRetrieval" ∷ "verify" ∷ t

  verifyBlock : HashValue → Block → Either ErrLog HashValue

  verifyBlocks : List Block → Either ErrLog Unit
  verifyBlocks blks = foldM_ verifyBlock blockId blks

  verifyBlock expectedId block = do
    Block.validateSignature block sigVerifier
    Block.verifyWellFormed  block
    lcheck (block ^∙ bId == expectedId)
           (here' ("blocks do not form a chain" ∷ [])) -- lsHV (block^.bId), lsHV expectedId
    pure (block ^∙ bParentId)

ext: agda


text:
{-# OPTIONS --type-in-type #-}
open import Data.Unit
open import Data.Product hiding ( curry ; uncurry )
open import Data.List hiding ( concat )
open import Data.String
open import Relation.Binary.PropositionalEquality
open import Function
module Spire.Examples.CompLev where

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

Label : Set
Label = String

Enum : Set
Enum = List Label

data Tag : Enum → Set where
  here : ∀{l E} → Tag (l ∷ E)
  there : ∀{l E} → Tag E → Tag (l ∷ E)

Branches : (E : Enum) (P : Tag E → Set) → Set
Branches [] P = ⊤
Branches (l ∷ E) P = P here × Branches E (λ t → P (there t))

case : {E : Enum} (P : Tag E → Set) (cs : Branches E P) (t : Tag E) → P t
case P (c , cs) here = c
case P (c , cs) (there t) = case (λ t → P (there t)) cs t

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

data Tel : Set where
  End : Tel
  Arg : (A : Set) (B : A → Tel) → Tel

Elᵀ  : Tel → Set
Elᵀ End = ⊤
Elᵀ (Arg A B) = Σ A (λ a → Elᵀ (B a))

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

data Desc (I : Set) : Set where
  End : Desc I
  Rec : (i : I) (D : Desc I) → Desc I
  RecFun : (A : Set) (B : A → I) (D : Desc I) → Desc I
  Arg : (A : Set) (B : A → Desc I) → Desc I

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

ISet : Set → Set
ISet I = I → Set

Elᴰ : {I : Set} (D : Desc I) → ISet I → Set
Elᴰ End X = ⊤
Elᴰ (Rec j D) X = X j × Elᴰ D X
Elᴰ (RecFun A B D) X = ((a : A) → X (B a)) × Elᴰ D X
Elᴰ (Arg A B) X = Σ A (λ a → Elᴰ (B a) X)

Hyps : {I : Set} (D : Desc I) (X : ISet I) (P : (i : I) → X i → Set) (xs : Elᴰ D X) → Set
Hyps End X P tt = ⊤
Hyps (Rec i D) X P (x , xs) = P i x × Hyps D X P xs
Hyps (RecFun A B D) X P (f , xs) = ((a : A) → P (B a) (f a)) × Hyps D X P xs
Hyps (Arg A B) X P (a , xs) = Hyps (B a) X P xs

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

data μ {I : Set} (R : I → Desc I) (i : I) : Set where
  init : Elᴰ (R i) (μ R) → μ R i

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

ind : {I : Set} (R : I → Desc I)
  (M : (i : I) → μ R i → Set)
  (α : ∀ i (xs : Elᴰ (R i) (μ R)) (ihs : Hyps (R i) (μ R) M xs) → M i (init xs))
  (i : I)
  (x : μ R i)
  → M i x

prove : {I : Set} (D : Desc I) (R : I → Desc I)
  (M : (i : I) → μ R i → Set)
  (α : ∀ i (xs : Elᴰ (R i) (μ R)) (ihs : Hyps (R i) (μ R) M xs) → M i (init xs))
  (xs : Elᴰ D (μ R)) → Hyps D (μ R) M xs

ind R M α i (init xs) = α i xs (prove (R i) R M α xs)

prove End R M α tt = tt
prove (Rec j D) R M α (x , xs) = ind R M α j x , prove D R M α xs
prove (RecFun A B D) R M α (f , xs) = (λ a → ind R M α (B a) (f a)) , prove D R M α xs
prove (Arg A B) R M α (a , xs) = prove (B a) R M α xs

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

DescE : Enum
DescE = "End" ∷ "Rec" ∷ "Arg" ∷ []

DescT : Set
DescT = Tag DescE

-- EndT : DescT
pattern EndT = here

-- RecT : DescT
pattern RecT = there here

-- ArgT : DescT
pattern ArgT = there (there here)

DescR : Set → ⊤ → Desc ⊤
DescR I tt = Arg (Tag DescE)
  (case (λ _ → Desc ⊤) (
      (Arg I λ i → End)
    , (Arg I λ i → Rec tt End)
    , (Arg Set λ A → RecFun A (λ a → tt) End)
    , tt
  ))

`Desc : (I : Set) → Set
`Desc I = μ (DescR I) tt

-- `End : {I : Set} (i : I) → `Desc I
pattern `End i = init (EndT , i , tt)

-- `Rec : {I : Set} (i : I) (D : `Desc I) → `Desc I
pattern `Rec i D = init (RecT , i , D , tt)

-- `Arg : {I : Set} (A : Set) (B : A → `Desc I) → `Desc I
pattern `Arg A B = init (ArgT , A , B , tt)

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

FixI : (I : Set) → Set
FixI I = I × `Desc I

FixR' : (I : Set) (D : `Desc I) → I → `Desc I → Desc (FixI I)
FixR' I D i (`End j) = Arg (j ≡ i) λ q → End
FixR' I D i (`Rec j E) = Rec (j , D) (FixR' I D i E)
FixR' I D i (`Arg A B) = Arg A λ a → FixR' I D i (B a)
FixR' I D i (init (there (there (there ())) , xs))

FixR : (I : Set) (D : `Desc I) → FixI I → Desc (FixI I)
FixR I D E,i = FixR' I D (proj₁ E,i) (proj₂ E,i)

`Fix : (I : Set) (D : `Desc I) (i : I) → Set
`Fix I D i = μ (FixR I D) (i , D)

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

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


text:
module Issue87 where

data I : Set where

data D : I -> Set where
  d : forall {i} (x : D i) -> D i

bar : forall {i} -> D i -> D i -> D i
bar (d x) (d     y) with y
bar (d x) (d {i} y) | z = d {i} y

-- ERROR WAS:
-- Panic: unbound variable i
-- when checking that the expression i has type I

-- Andreas, 2016-06-02
-- This looks weird, but is accepted currently:
test : ∀ i → D i → D i → D i
test .i (d {i} x) (d {.i} y) with y
test .i (d {j} x) (d {i} y) | _ = d {i} y
-- Note the {j}!

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Agda.Builtin.Equality

_∘_ : ∀ {a b c}
        {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
        (f : ∀ {x} (y : B x) → C y) →
        (g : (x : A) → B x) →
        ((x : A) → C (g x))
f ∘ g = λ x → f (g x)

postulate
  A : Set
  B : A → Set
  C : {x : A} → B x → Set
  f : ∀ {x : A} (y : B x) → C y
  g : (x : A) → B x

test : (f ∘ g) ≡ (f ∘ g)
test = {!!}

-- WAS: goal displayed as ((λ {x} -> f) ∘ g) ≡ ((λ {x} -> f) ∘ g)
-- WANT: no spurious hidden lambda i.e. (f ∘ g) ≡ (f ∘ g)


text:
open import Data.Natural using ( Natural ; # ; _+_ )

module System.IO.Examples.Four where

four : Natural
four = # 2 + # 2

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


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

open import Sets.EquivalenceRelations
open import Setoids.Setoids
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Groups.Definition

module Groups.Homomorphisms.Definition where

record GroupHom {m n o p : _} {A : Set m} {S : Setoid {m} {o} A} {_·A_ : A → A → A} {B : Set n} {T : Setoid {n} {p} B} {_·B_ : B → B → B} (G : Group S _·A_) (H : Group T _·B_) (f : A → B) : Set (m ⊔ n ⊔ o ⊔ p) where
  open Group H
  open Setoid T
  field
    groupHom : {x y : A} → f (x ·A y) ∼ (f x) ·B (f y)
    wellDefined : {x y : A} → Setoid._∼_ S x y → f x ∼ f y
  groupHom' : {x y : A} → (f x) ·B (f y) ∼ f (x ·A y)
  groupHom' = Equivalence.symmetric eq groupHom

record InjectiveGroupHom {m n o p : _} {A : Set m} {S : Setoid {m} {o} A} {_·A_ : A → A → A} {B : Set n} {T : Setoid {n} {p} B} {_·B_ : B → B → B} {G : Group S _·A_} {H : Group T _·B_} {underf : A → B} (f : GroupHom G H underf) : Set (m ⊔ n ⊔ o ⊔ p) where
  open Setoid S renaming (_∼_ to _∼A_)
  open Setoid T renaming (_∼_ to _∼B_)
  field
    injective : SetoidInjection S T underf


text:
-- Andreas, 2017-02-14 issue #2455 reported by mechvel
-- Test case by Andrea

-- Seem that the fix for issue #44 was not complete.

-- When inserting module parameters for a definition,
-- we need to respect polarities!

-- {-# OPTIONS -v tc.decl:10 -v tc.polarity:70 -v tc.sig.inst:30 #-}

module Issue2455 where

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

data Unit : Set where
  unit : Unit

postulate
  A : Set
  P : A → Set
  p : ∀ {e} → P e

module M (e : A) (f : Unit) where

   aux : Unit → P e
   aux unit = p

   -- se does not depent on f
   -- se gets type (e : A) (f :{UnusedArg} Unit) -> A
   se = e

   -- aux' should not depend on f
   -- For this to work, the module parameters for se must be
   -- respecting UnusedArg.
   aux' : Unit → P se
   aux' unit = p

works : ∀ x y e → M.aux e x ≡ M.aux e y
works _ _ _ = refl

fails : ∀ x y e → M.aux' e x ≡ M.aux' e y
fails _ _ _ = refl

max_stars_repo_name: Blaisorblade/Agda

max_issues_repo_name: Blaisorblade/Agda

max_forks_repo_name: Blaisorblade/Agda


text:
module ShouldBeApplicationOf where

data One : Set where one : One
data Two : Set where two : Two

f : One -> Two
f two = two


text:
-- Andreas, bug found 2011-12-31

{-# OPTIONS --irrelevant-projections #-}

module Issue543 where

open import Common.Equality

data   ⊥ : Set where
record ⊤ : Set where
  constructor tt

data Bool : Set where
  true false : Bool

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

record Squash {ℓ}(A : Set ℓ) : Set ℓ where
  constructor squash
  field
    .unsquash : A
open Squash

-- ok:
sqT≡sqF : squash true ≡ squash false
sqT≡sqF = refl

-- this should not be provable!!
.irrT≡F : true ≡ false
irrT≡F = subst (λ s → unsquash (squash true) ≡ unsquash s) sqT≡sqF refl

-- the rest is easy
T≠F : true ≡ false → ⊥
T≠F p = subst T p tt

.irr⊥ : ⊥
irr⊥ = T≠F irrT≡F

rel⊥ : .⊥ → ⊥
rel⊥ ()

absurd : ⊥
absurd = rel⊥ irr⊥


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

module HoTT.Ident where

data Id (X : Set) : X → X → Set  where
 refl : (x : X) → Id X x x

_≡_ : {X : Set} → X → X → Set
x ≡ y = Id _ x y

𝕁 : {X : Set}
  → (A : (x y : X) → x ≡ y → Set)
  → ((x : X) → A x x (refl x))
  → (x y : X) → (p : x ≡ y) → A x y p
𝕁 A f x x (refl x) = f x

ℍ : {X : Set}
  → (x : X)
  → (B : (y : X) → x ≡ y → Set)
  → B x (refl x)
  → (y : X) → (p : x ≡ y) → B y p
ℍ x B b x (refl x) = b

-- Defining `𝕁` in terms of `ℍ`.

𝕁' : {X : Set}
  → (A : (x y : X) → x ≡ y → Set)
  → ((x : X) → A x x (refl x))
  → (x y : X) → (p : x ≡ y) → A x y p
𝕁' A f x = ℍ x (A x) (f x)

-- Defining `ℍ` in terms of `𝕁`.

transport : {X : Set} → (f : X → Set) → (x y : X) → (x ≡ y) → f x → f y
transport f = 𝕁 (λ x y p → f x → f y) (λ x y → y)

data Σ (A : Set) (p : A → Set) : Set  where
  _,_ : (x : A) → p x → Σ A p

curry : {A : Set} {B : A → Set} → ((x : A) → B x → Set) → Σ A B → Set
curry f (x , y) = f x y

-- This is just for the "Note" below.
singl : (A : Set) → A → Set
singl A x = Σ A (λ y → x ≡ y)

-- Note: `≡` in the conclusion is WRT `Id (singl X x)`.
-- Source: http://www.cse.chalmers.se/~coquand/singl.pdf
lemma : {X : Set} → (x y : X) → (p : x ≡ y) → (x , refl x) ≡ (y , p)
lemma = 𝕁 (λ x y p → (x , refl x) ≡ (y , p)) (λ x → refl (x , refl x))

ℍ' : {X : Set}
  → (x : X)
  → (B : (y : X) → x ≡ y → Set)
  → B x (refl x)
  → (y : X) → (p : x ≡ y) → B y p
ℍ' x B b y p = transport (curry B) (x , refl x) (y , p) (lemma x y p) b

max_stars_repo_name: izuk/agda-hott

max_issues_repo_name: izuk/agda-hott

max_forks_repo_name: izuk/agda-hott


text:
------------------------------------------------------------------------
-- Compiler correctness
------------------------------------------------------------------------

open import Prelude

import Lambda.Syntax

module Lambda.Compiler-correctness
  {Name : Type}
  (open Lambda.Syntax Name)
  (def : Name → Tm 1)
  where

import Equality.Propositional as E
import Tactic.By.Propositional as By
open import Prelude.Size

open import List E.equality-with-J using (_++_)
open import Monad E.equality-with-J using (return; _>>=_)
open import Vec.Data E.equality-with-J

open import Delay-monad.Bisimilarity

open import Lambda.Compiler def
open import Lambda.Delay-crash
open import Lambda.Interpreter def
open import Lambda.Virtual-machine.Instructions Name hiding (crash)
open import Lambda.Virtual-machine comp-name

private
  module C = Closure Code
  module T = Closure Tm

------------------------------------------------------------------------
-- A lemma

-- A rearrangement lemma for ⟦_⟧.

⟦⟧-· :
  ∀ {n} (t₁ t₂ : Tm n) {ρ} {k : T.Value → Delay-crash C.Value ∞} →
  ⟦ t₁ · t₂ ⟧ ρ >>= k ∼
  ⟦ t₁ ⟧ ρ >>= λ v₁ → ⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ ∙ v₂ >>= k
⟦⟧-· t₁ t₂ {ρ} {k} =
  ⟦ t₁ · t₂ ⟧ ρ >>= k      ∼⟨⟩

  (do v₁ ← ⟦ t₁ ⟧ ρ
      v₂ ← ⟦ t₂ ⟧ ρ
      v₁ ∙ v₂) >>= k       ∼⟨ symmetric (associativity (⟦ t₁ ⟧ _) _ _) ⟩

  (do v₁ ← ⟦ t₁ ⟧ ρ
      (do v₂ ← ⟦ t₂ ⟧ ρ
          v₁ ∙ v₂) >>= k)  ∼⟨ (⟦ t₁ ⟧ _ ∎) >>=-cong (λ _ → symmetric (associativity (⟦ t₂ ⟧ _) _ _)) ⟩

  (do v₁ ← ⟦ t₁ ⟧ ρ
      v₂ ← ⟦ t₂ ⟧ ρ
      v₁ ∙ v₂ >>= k)       ∎

------------------------------------------------------------------------
-- Well-formed continuations and stacks

-- A continuation is OK with respect to a certain state if the
-- following property is satisfied.

Cont-OK : Size → State → (T.Value → Delay-crash C.Value ∞) → Type
Cont-OK i ⟨ c , s , ρ ⟩ k =
  ∀ v → [ i ] exec ⟨ c , val (comp-val v) ∷ s , ρ ⟩ ≈ k v

-- If the In-tail-context parameter indicates that we are in a tail
-- context, then the stack must have a certain shape, and it must be
-- related to the continuation in a certain way.

data Stack-OK (i : Size) (k : T.Value → Delay-crash C.Value ∞) :
              In-tail-context → Stack → Type where
  unrestricted : ∀ {s} → Stack-OK i k false s
  restricted   : ∀ {s n} {c : Code n} {ρ : C.Env n} →
                 Cont-OK i ⟨ c , s , ρ ⟩ k →
                 Stack-OK i k true (ret c ρ ∷ s)

-- A lemma that can be used to show that certain stacks are OK.

ret-ok :
  ∀ {p i s n c} {ρ : C.Env n} {k} →
  Cont-OK i ⟨ c , s , ρ ⟩ k →
  Stack-OK i k p (ret c ρ ∷ s)
ret-ok {true}  c-ok = restricted c-ok
ret-ok {false} _    = unrestricted

------------------------------------------------------------------------
-- The semantics of the compiled program matches that of the source
-- code

mutual

  -- Some lemmas making up the main part of the compiler correctness
  -- result.

  ⟦⟧-correct :
    ∀ {i n} (t : Tm n) (ρ : T.Env n) {c s}
      {k : T.Value → Delay-crash C.Value ∞} {tc} →
    Stack-OK i k tc s →
    Cont-OK i ⟨ c , s , comp-env ρ ⟩ k →
    [ i ] exec ⟨ comp tc t c , s , comp-env ρ ⟩ ≈ ⟦ t ⟧ ρ >>= k

  ⟦⟧-correct (var x) ρ {c} {s} {k} _ c-ok =
    exec ⟨ var x ∷ c , s , comp-env ρ ⟩                            ≳⟨⟩
    exec ⟨ c , val By.⟨ index (comp-env ρ) x ⟩ ∷ s , comp-env ρ ⟩  ≡⟨ By.⟨by⟩ (comp-index ρ x) ⟩
    exec ⟨ c , val (comp-val (index ρ x)) ∷ s , comp-env ρ ⟩       ≈⟨ c-ok (index ρ x) ⟩∼
    k (index ρ x)                                                  ∼⟨⟩
    ⟦ var x ⟧ ρ >>= k                                              ∎

  ⟦⟧-correct (lam t) ρ {c} {s} {k} _ c-ok =
    exec ⟨ clo (comp-body t) ∷ c , s , comp-env ρ ⟩             ≳⟨⟩
    exec ⟨ c , val (comp-val (T.lam t ρ)) ∷ s , comp-env ρ ⟩    ≈⟨ c-ok (T.lam t ρ) ⟩∼
    k (T.lam t ρ)                                               ∼⟨⟩
    ⟦ lam t ⟧ ρ >>= k                                           ∎

  ⟦⟧-correct (t₁ · t₂) ρ {c} {s} {k} _ c-ok =
    exec ⟨ comp false t₁ (comp false t₂ (app ∷ c))
         , s
         , comp-env ρ
         ⟩                                                   ≈⟨ (⟦⟧-correct t₁ _ unrestricted λ v₁ →

      exec ⟨ comp false t₂ (app ∷ c)
           , val (comp-val v₁) ∷ s
           , comp-env ρ
           ⟩                                                       ≈⟨ (⟦⟧-correct t₂ _ unrestricted λ v₂ →

        exec ⟨ app ∷ c
             , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s
             , comp-env ρ
             ⟩                                                           ≈⟨ ∙-correct v₁ v₂ c-ok ⟩∼

        v₁ ∙ v₂ >>= k                                                    ∎) ⟩∼

      (⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ ∙ v₂ >>= k)                          ∎) ⟩∼

    (⟦ t₁ ⟧ ρ >>= λ v₁ → ⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ ∙ v₂ >>= k)  ∼⟨ symmetric (⟦⟧-· t₁ t₂) ⟩

    ⟦ t₁ · t₂ ⟧ ρ >>= k                                      ∎

  ⟦⟧-correct (call f t) ρ {c} {s} {k} unrestricted c-ok =
    exec ⟨ comp false (call f t) c , s , comp-env ρ ⟩         ∼⟨⟩

    exec ⟨ comp false t (cal f ∷ c) , s , comp-env ρ ⟩        ≈⟨ (⟦⟧-correct t _ unrestricted λ v →

      exec ⟨ cal f ∷ c , val (comp-val v) ∷ s , comp-env ρ ⟩        ≈⟨ (later λ { .force →

        exec ⟨ comp-name f
             , ret c (comp-env ρ) ∷ s
             , comp-val v ∷ []
             ⟩                                                            ≈⟨ body-lemma (def f) [] c-ok ⟩∼

        (⟦ def f ⟧ (v ∷ []) >>= k)                                        ∎ }) ⟩∼

      (T.lam (def f) [] ∙ v >>= k)                                  ∎) ⟩∼

    (⟦ t ⟧ ρ >>= λ v → T.lam (def f) [] ∙ v >>= k)            ∼⟨ associativity (⟦ t ⟧ ρ) _ _ ⟩

    (⟦ t ⟧ ρ >>= λ v → T.lam (def f) [] ∙ v) >>= k            ∼⟨⟩

    ⟦ call f t ⟧ ρ >>= k                                      ∎

  ⟦⟧-correct (call f t) ρ {c} {ret c′ ρ′ ∷ s} {k} (restricted c-ok) _ =
    exec ⟨ comp true (call f t) c , ret c′ ρ′ ∷ s , comp-env ρ ⟩    ∼⟨⟩

    exec ⟨ comp false t (tcl f ∷ c) , ret c′ ρ′ ∷ s , comp-env ρ ⟩  ≈⟨ (⟦⟧-correct t _ unrestricted λ v →

      exec ⟨ tcl f ∷ c
           , val (comp-val v) ∷ ret c′ ρ′ ∷ s
           , comp-env ρ
           ⟩                                                              ≈⟨ (later λ { .force →

        exec ⟨ comp-name f
             , ret c′ ρ′ ∷ s
             , comp-val v ∷ []
             ⟩                                                                  ≈⟨ body-lemma (def f) [] c-ok ⟩∼

        ⟦ def f ⟧ (v ∷ []) >>= k                                                ∎ }) ⟩∼

      T.lam (def f) [] ∙ v >>= k                                          ∎) ⟩∼

    (⟦ t ⟧ ρ >>= λ v → T.lam (def f) [] ∙ v >>= k)                  ∼⟨ associativity (⟦ t ⟧ ρ) _ _ ⟩

    (⟦ t ⟧ ρ >>= λ v → T.lam (def f) [] ∙ v) >>= k                  ∼⟨⟩

    ⟦ call f t ⟧ ρ >>= k                                            ∎

  ⟦⟧-correct (con b) ρ {c} {s} {k} _ c-ok =
    exec ⟨ con b ∷ c , s , comp-env ρ ⟩                     ≳⟨⟩
    exec ⟨ c , val (comp-val (T.con b)) ∷ s , comp-env ρ ⟩  ≈⟨ c-ok (T.con b) ⟩∼
    k (T.con b)                                             ∼⟨⟩
    ⟦ con b ⟧ ρ >>= k                                       ∎

  ⟦⟧-correct (if t₁ t₂ t₃) ρ {c} {s} {k} {tc} s-ok c-ok =
    exec ⟨ comp false t₁ (bra (comp tc t₂ []) (comp tc t₃ []) ∷ c)
         , s
         , comp-env ρ
         ⟩                                                          ≈⟨ (⟦⟧-correct t₁ _ unrestricted λ v₁ → ⟦if⟧-correct v₁ t₂ t₃ s-ok c-ok) ⟩∼

    (⟦ t₁ ⟧ ρ >>= λ v₁ → ⟦if⟧ v₁ t₂ t₃ ρ >>= k)                     ∼⟨ associativity (⟦ t₁ ⟧ ρ) _ _ ⟩

    (⟦ t₁ ⟧ ρ >>= λ v₁ → ⟦if⟧ v₁ t₂ t₃ ρ) >>= k                     ∼⟨⟩

    ⟦ if t₁ t₂ t₃ ⟧ ρ >>= k                                         ∎

  body-lemma :
    ∀ {i n n′} (t : Tm (1 + n)) ρ {ρ′ : C.Env n′} {c s v}
      {k : T.Value → Delay-crash C.Value ∞} →
    Cont-OK i ⟨ c , s , ρ′ ⟩ k →
    [ i ] exec ⟨ comp-body t
               , ret c ρ′ ∷ s
               , comp-val v ∷ comp-env ρ
               ⟩ ≈
          ⟦ t ⟧ (v ∷ ρ) >>= k
  body-lemma t ρ {ρ′} {c} {s} {v} {k} c-ok =
    exec ⟨ comp-body t , ret c ρ′ ∷ s , comp-val v ∷ comp-env ρ ⟩  ∼⟨⟩

    exec ⟨ comp-body t , ret c ρ′ ∷ s , comp-env (v ∷ ρ) ⟩         ≈⟨ (⟦⟧-correct t (_ ∷ _) (ret-ok c-ok) λ v′ →

      exec ⟨ ret ∷ []
           , val (comp-val v′) ∷ ret c ρ′ ∷ s
           , comp-env (v ∷ ρ)
           ⟩                                                             ≳⟨⟩

      exec ⟨ c , val (comp-val v′) ∷ s , ρ′ ⟩                            ≈⟨ c-ok v′ ⟩∼

      k v′                                                               ∎) ⟩∼

    ⟦ t ⟧ (v ∷ ρ) >>= k                                            ∎

  ∙-correct :
    ∀ {i n} v₁ v₂ {ρ : C.Env n} {c s}
      {k : T.Value → Delay-crash C.Value ∞} →
    Cont-OK i ⟨ c , s , ρ ⟩ k →
    [ i ] exec ⟨ app ∷ c
               , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s
               , ρ
               ⟩ ≈
          v₁ ∙ v₂ >>= k

  ∙-correct (T.lam t₁ ρ₁) v₂ {ρ} {c} {s} {k} c-ok =
    exec ⟨ app ∷ c
         , val (comp-val v₂) ∷ val (comp-val (T.lam t₁ ρ₁)) ∷ s
         , ρ
         ⟩                                                             ≈⟨ later (λ { .force →

      exec ⟨ comp-body t₁ , ret c ρ ∷ s , comp-val v₂ ∷ comp-env ρ₁ ⟩       ≈⟨ body-lemma t₁ _ c-ok ⟩∼

      ⟦ t₁ ⟧ (v₂ ∷ ρ₁) >>= k                                                ∎ }) ⟩∎

    T.lam t₁ ρ₁ ∙ v₂ >>= k                                             ∎

  ∙-correct (T.con b) v₂ {ρ} {c} {s} {k} _ =
    exec ⟨ app ∷ c
         , val (comp-val v₂) ∷ val (comp-val (T.con b)) ∷ s
         , ρ
         ⟩                                                   ≳⟨⟩

    crash                                                    ∼⟨⟩

    T.con b ∙ v₂ >>= k                                       ∎

  ⟦if⟧-correct :
    ∀ {i n} v₁ (t₂ t₃ : Tm n) {ρ : T.Env n} {c s}
      {k : T.Value → Delay-crash C.Value ∞} {tc} →
    Stack-OK i k tc s →
    Cont-OK i ⟨ c , s , comp-env ρ ⟩ k →
    [ i ] exec ⟨ bra (comp tc t₂ []) (comp tc t₃ []) ∷ c
               , val (comp-val v₁) ∷ s
               , comp-env ρ
               ⟩ ≈
          ⟦if⟧ v₁ t₂ t₃ ρ >>= k

  ⟦if⟧-correct (T.lam t₁ ρ₁) t₂ t₃ {ρ} {c} {s} {k} {tc} _ _ =
    exec ⟨ bra (comp tc t₂ []) (comp tc t₃ []) ∷ c
         , val (comp-val (T.lam t₁ ρ₁)) ∷ s
         , comp-env ρ
         ⟩                                          ≳⟨⟩

    crash                                           ∼⟨⟩

    ⟦if⟧ (T.lam t₁ ρ₁) t₂ t₃ ρ >>= k                ∎

  ⟦if⟧-correct (T.con true) t₂ t₃ {ρ} {c} {s} {k} {tc} s-ok c-ok =
    exec ⟨ bra (comp tc t₂ []) (comp tc t₃ []) ∷ c
         , val (comp-val (T.con true)) ∷ s
         , comp-env ρ
         ⟩                                          ≳⟨⟩

    exec ⟨ comp tc t₂ [] ++ c , s , comp-env ρ ⟩    ≡⟨ By.by (comp-++ _ t₂) ⟩

    exec ⟨ comp tc t₂ c , s , comp-env ρ ⟩          ≈⟨ ⟦⟧-correct t₂ _ s-ok c-ok ⟩∼

    ⟦ t₂ ⟧ ρ >>= k                                  ∼⟨⟩

    ⟦if⟧ (T.con true) t₂ t₃ ρ >>= k                 ∎

  ⟦if⟧-correct (T.con false) t₂ t₃ {ρ} {c} {s} {k} {tc} s-ok c-ok =
    exec ⟨ bra (comp tc t₂ []) (comp tc t₃ []) ∷ c
         , val (comp-val (T.con false)) ∷ s
         , comp-env ρ
         ⟩                                          ≳⟨⟩

    exec ⟨ comp tc t₃ [] ++ c , s , comp-env ρ ⟩    ≡⟨ By.by (comp-++ _ t₃) ⟩

    exec ⟨ comp tc t₃ c , s , comp-env ρ ⟩          ≈⟨ ⟦⟧-correct t₃ _ s-ok c-ok ⟩∼

    ⟦ t₃ ⟧ ρ >>= k                                  ∼⟨⟩

    ⟦if⟧ (T.con false) t₂ t₃ ρ >>= k                ∎

-- Compiler correctness. Note that the equality that is used here is
-- syntactic.

correct :
  (t : Tm 0) →
  exec ⟨ comp₀ t , [] , [] ⟩ ≈
  ⟦ t ⟧ [] >>= λ v → return (comp-val v)
correct t =
  exec ⟨ comp false t [] , [] , [] ⟩           ∼⟨⟩
  exec ⟨ comp false t [] , [] , comp-env [] ⟩  ≈⟨ ⟦⟧-correct t [] unrestricted (λ v → laterˡ (return (comp-val v) ∎)) ⟩
  (⟦ t ⟧ [] >>= λ v → return (comp-val v))     ∎

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


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

data Bool : Set where
  true  : Bool
  false : Bool

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc  : {n : ℕ} (i : Fin n) → Fin (suc n)

infixr 5 _∷_

data Vec {a} (A : Set a) : ℕ → Set a where
  []  : Vec A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

infix 4 _[_]=_

data _[_]=_ {a} {A : Set a} :
            {n : ℕ} → Vec A n → Fin n → A → Set a where
  here  : ∀ {n}     {x}   {xs : Vec A n} → x ∷ xs [ zero ]= x
  there : ∀ {n} {i} {x y} {xs : Vec A n}
          (xs[i]=x : xs [ i ]= x) → y ∷ xs [ suc i ]= x

Subset : ℕ → Set
Subset = Vec Bool

infix 4 _∈_

_∈_ : ∀ {n} → Fin n → Subset n → Set
x ∈ p = p [ x ]= true

drop-there : ∀ {s n x} {p : Subset n} → suc x ∈ s ∷ p → x ∈ p
drop-there (there x∈p) = x∈p

_∘_ : ∀ {a b c}
        {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
        (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
        ((x : A) → C (g x))
f ∘ g = λ x → f (g x)

data ⊥ : Set where

infix 3 ¬_

¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ P = P → ⊥

data Dec {p} (P : Set p) : Set p where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P

infix 4 _∈?_

_∈?_ : ∀ {n} x (p : Subset n) → Dec (x ∈ p)
zero  ∈? true  ∷ p = yes here
zero  ∈? false ∷ p = no  λ()
suc n ∈? s ∷ p       with n ∈? p
...                  | yes n∈p = yes (there n∈p)
...                  | no  n∉p = no  (n∉p ∘ drop-there)


text:
module STLC1.Kovacs.Soundness where

open import STLC1.Kovacs.Convertibility public
open import STLC1.Kovacs.PresheafRefinement public

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

infix 3 _≈_
_≈_ : ∀ {A Γ} → Γ ⊩ A → Γ ⊩ A → Set

_≈_ {⎵}      {Γ} M₁ M₂ = M₁ ≡ M₂

_≈_ {A ⇒ B} {Γ} f₁ f₂ = ∀ {Γ′} → (η : Γ′ ⊇ Γ) {a₁ a₂ : Γ′ ⊩ A}
                                → (p : a₁ ≈ a₂) (u₁ : 𝒰 a₁) (u₂ : 𝒰 a₂)
                                → f₁ η a₁ ≈ f₂ η a₂

_≈_ {A ⩕ B}  {Γ} s₁ s₂ = proj₁ s₁ ≈ proj₁ s₂ × proj₂ s₁ ≈ proj₂ s₂

_≈_ {⫪}     {Γ} s₁ s₂ = ⊤

-- (≈ᶜ ; ∙ ; _,_)
infix 3 _≈⋆_
data _≈⋆_ : ∀ {Γ Ξ} → Γ ⊩⋆ Ξ → Γ ⊩⋆ Ξ → Set
  where
    ∅   : ∀ {Γ} → ∅ {Γ} ≈⋆ ∅

    _,_ : ∀ {Γ Ξ A} → {ρ₁ ρ₂ : Γ ⊩⋆ Ξ} {M₁ M₂ : Γ ⊩ A}
                    → (χ : ρ₁ ≈⋆ ρ₂) (p : M₁ ≈ M₂)
                    → ρ₁ , M₁ ≈⋆ ρ₂ , M₂

-- (_≈⁻¹)
_⁻¹≈ : ∀ {A Γ} → {a₁ a₂ : Γ ⊩ A}
               → a₁ ≈ a₂
               → a₂ ≈ a₁
_⁻¹≈ {⎵}      p = p ⁻¹
_⁻¹≈ {A ⇒ B} F = λ η p u₁ u₂ →
                    F η (p ⁻¹≈) u₂ u₁ ⁻¹≈
_⁻¹≈ {A ⩕ B}  p = proj₁ p ⁻¹≈ , proj₂ p ⁻¹≈
_⁻¹≈ {⫪}     p = tt

-- (_≈ᶜ⁻¹)
_⁻¹≈⋆ : ∀ {Γ Ξ} → {ρ₁ ρ₂ : Γ ⊩⋆ Ξ}
                → ρ₁ ≈⋆ ρ₂
                → ρ₂ ≈⋆ ρ₁
∅       ⁻¹≈⋆ = ∅
(χ , p) ⁻¹≈⋆ = χ ⁻¹≈⋆ , p ⁻¹≈

-- (_≈◾_)
_⦙≈_ : ∀ {A Γ} → {a₁ a₂ a₃ : Γ ⊩ A}
               → a₁ ≈ a₂ → a₂ ≈ a₃
               → a₁ ≈ a₃
_⦙≈_ {⎵}      p q = p ⦙ q
_⦙≈_ {A ⇒ B} F G = λ η p u₁ u₂ →
                       F η (p ⦙≈ (p ⁻¹≈)) u₁ u₁
                    ⦙≈ G η p u₁ u₂
_⦙≈_ {A ⩕ B}  p q = proj₁ p ⦙≈ proj₁ q , proj₂ p ⦙≈ proj₂ q
_⦙≈_ {⫪}     p q = tt

-- (_≈ᶜ◾_)
_⦙≈⋆_ : ∀ {Γ Ξ} → {ρ₁ ρ₂ ρ₃ : Γ ⊩⋆ Ξ}
                → ρ₁ ≈⋆ ρ₂ → ρ₂ ≈⋆ ρ₃
                → ρ₁ ≈⋆ ρ₃
∅        ⦙≈⋆ ∅        = ∅
(χ₁ , p) ⦙≈⋆ (χ₂ , q) = χ₁ ⦙≈⋆ χ₂ , p ⦙≈ q

instance
  per≈ : ∀ {Γ A} → PER (Γ ⊩ A) _≈_
  per≈ =
    record
      { _⁻¹ = _⁻¹≈
      ; _⦙_ = _⦙≈_
      }

instance
  per≈⋆ : ∀ {Γ Ξ} → PER (Γ ⊩⋆ Ξ) _≈⋆_
  per≈⋆ =
    record
      { _⁻¹ = _⁻¹≈⋆
      ; _⦙_ = _⦙≈⋆_
      }

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

-- (≈ₑ)
acc≈ : ∀ {A Γ Γ′} → {a₁ a₂ : Γ ⊩ A}
                  → (η : Γ′ ⊇ Γ) → a₁ ≈ a₂
                  → acc η a₁ ≈ acc η a₂
acc≈ {⎵}      η p = renⁿᶠ η & p
acc≈ {A ⇒ B} η F = λ η′ → F (η ○ η′)
acc≈ {A ⩕ B}  η p = acc≈ η (proj₁ p) , acc≈ η (proj₂ p)
acc≈ {⫪}     η p = tt

-- (≈ᶜₑ)
_⬖≈_ : ∀ {Γ Γ′ Ξ} → {ρ₁ ρ₂ : Γ ⊩⋆ Ξ}
                  → ρ₁ ≈⋆ ρ₂ → (η : Γ′ ⊇ Γ)
                  → ρ₁ ⬖ η ≈⋆ ρ₂ ⬖ η
∅       ⬖≈ η = ∅
(χ , p) ⬖≈ η = χ ⬖≈ η , acc≈ η p

-- (∈≈)
get≈ : ∀ {Γ Ξ A} → {ρ₁ ρ₂ : Γ ⊩⋆ Ξ}
                 → ρ₁ ≈⋆ ρ₂ → (i : Ξ ∋ A)
                 → getᵥ ρ₁ i ≈ getᵥ ρ₂ i
get≈ (χ , p) zero    = p
get≈ (χ , p) (suc i) = get≈ χ i

-- (Tm≈)
eval≈ : ∀ {Γ Ξ A} → {ρ₁ ρ₂ : Γ ⊩⋆ Ξ}
                  → ρ₁ ≈⋆ ρ₂ → 𝒰⋆ ρ₁ → 𝒰⋆ ρ₂ → (M : Ξ ⊢ A)
                  → eval ρ₁ M ≈ eval ρ₂ M
eval≈ χ υ₁ υ₂ (𝓋 i)   = get≈ χ i
eval≈ χ υ₁ υ₂ (ƛ M)   = λ η p u₁ u₂ →
                          eval≈ (χ ⬖≈ η , p)
                                (υ₁ ⬖𝒰 η , u₁)
                                (υ₂ ⬖𝒰 η , u₂)
                                M
eval≈ χ υ₁ υ₂ (M ∙ N) = eval≈ χ υ₁ υ₂ M idₑ
                              (eval≈ χ υ₁ υ₂ N)
                              (eval𝒰 υ₁ N)
                              (eval𝒰 υ₂ N)
eval≈ χ υ₁ υ₂ (M , N) = eval≈ χ υ₁ υ₂ M , eval≈ χ υ₁ υ₂ N
eval≈ χ υ₁ υ₂ (π₁ M)  = proj₁ (eval≈ χ υ₁ υ₂ M)
eval≈ χ υ₁ υ₂ (π₂ M)  = proj₂ (eval≈ χ υ₁ υ₂ M)
eval≈ χ υ₁ υ₂ τ       = tt

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

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

-- (Subᴺ≈ᶜ)
-- NOTE: _◆≈_ = eval≈⋆
_◆≈_ : ∀ {Γ Ξ Φ} → {ρ₁ ρ₂ : Γ ⊩⋆ Ξ}
                 → (σ : Ξ ⊢⋆ Φ) → ρ₁ ≈⋆ ρ₂ → 𝒰⋆ ρ₁ → 𝒰⋆ ρ₂
                 → σ ◆ ρ₁ ≈⋆ σ ◆ ρ₂
(∅ ◆≈ χ)       υ₁ υ₂ = ∅
((σ , M) ◆≈ χ) υ₁ υ₂ = (σ ◆≈ χ) υ₁ υ₂ , eval≈ χ υ₁ υ₂ M

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

-- (Tmₛᴺ)
eval◆ : ∀ {Γ Ξ Φ A} → {ρ : Γ ⊩⋆ Ξ}
                    → ρ ≈⋆ ρ → 𝒰⋆ ρ → (σ : Ξ ⊢⋆ Φ) (M : Φ ⊢ A)
                    → eval ρ (sub σ M) ≈ eval (σ ◆ ρ) M

eval◆ {ρ = ρ} χ υ σ (𝓋 i)
  rewrite get◆ ρ σ i
  = eval≈ χ υ υ (getₛ σ i)

eval◆ {ρ = ρ} χ υ σ (ƛ M) η {a₁} {a₂} p u₁ u₂
  rewrite comp◆⬖ η υ σ
  = let
      υ′ = υ ⬖𝒰 η
    in
      eval◆ {ρ = ρ ⬖ η , a₁}
            ((χ ⬖≈ η) , (p ⦙ p ⁻¹))
            (υ ⬖𝒰 η , u₁)
            (liftₛ σ)
            M
    ⦙ coe ((λ ρ′ → eval (ρ′ , a₁) M ≈ _)
           & ( comp◆⬗ (ρ ⬖ η , a₁) (wkₑ idₑ) σ
             ⦙ (σ ◆_) & lid⬗ (ρ ⬖ η)
             ) ⁻¹)
          (eval≈ ((σ ◆≈ (χ ⬖≈ η)) υ′ υ′ , p)
                 (σ ◆𝒰 υ′ , u₁)
                 (σ ◆𝒰 υ′ , u₂)
                 M)

eval◆ {ρ = ρ} χ υ σ (M ∙ N)
  = eval◆ χ υ σ M
          idₑ
          (eval◆ χ υ σ N)
          (eval𝒰 υ (sub σ N))
          (eval𝒰 (σ ◆𝒰 υ) N)

eval◆ {ρ = ρ} χ υ σ (M , N) = eval◆ χ υ σ M , eval◆ χ υ σ N
eval◆ {ρ = ρ} χ υ σ (π₁ M)  = proj₁ (eval◆ χ υ σ M)
eval◆ {ρ = ρ} χ υ σ (π₂ M)  = proj₂ (eval◆ χ υ σ M)
eval◆ {ρ = ρ} χ υ σ τ       = tt

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

-- (~≈)
eval∼ : ∀ {Γ Ξ A} → {ρ₁ ρ₂ : Γ ⊩⋆ Ξ}
                  → ρ₁ ≈⋆ ρ₂ → 𝒰⋆ ρ₁ → 𝒰⋆ ρ₂
                  → {M₁ M₂ : Ξ ⊢ A}
                  → M₁ ∼ M₂
                  → eval ρ₁ M₁ ≈ eval ρ₂ M₂

eval∼ χ υ₁ υ₂ {M} refl∼ = eval≈ χ υ₁ υ₂ M
eval∼ χ υ₁ υ₂ (p ⁻¹∼)   = eval∼ (χ ⁻¹) υ₂ υ₁ p ⁻¹
eval∼ χ υ₁ υ₂ (p ⦙∼ q)  = eval∼ (χ ⦙ χ ⁻¹) υ₁ υ₁ p
                        ⦙ eval∼ χ υ₁ υ₂ q

eval∼ χ υ₁ υ₂ (ƛ∼ p)
  = λ η q u₁ u₂ →
      eval∼ (χ ⬖≈ η , q)
            (υ₁ ⬖𝒰 η , u₁)
            (υ₂ ⬖𝒰 η , u₂)
            p

eval∼ χ υ₁ υ₂ (_∙∼_ {N₁ = N₁} {N₂} p q)
  = eval∼ χ υ₁ υ₂ p
          idₑ
          (eval∼ χ υ₁ υ₂ q)
          (eval𝒰 υ₁ N₁)
          (eval𝒰 υ₂ N₂)

eval∼ χ υ₁ υ₂ (p ,∼ q) = eval∼ χ υ₁ υ₂ p , eval∼ χ υ₁ υ₂ q
eval∼ χ υ₁ υ₂ (π₁∼ p ) = proj₁ (eval∼ χ υ₁ υ₂ p)
eval∼ χ υ₁ υ₂ (π₂∼ p ) = proj₂ (eval∼ χ υ₁ υ₂ p)

eval∼ {ρ₁ = ρ₁} {ρ₂} χ υ₁ υ₂ (red⇒ M N)
  = coe ((λ ρ₁′ ρ₂′ → eval (ρ₁′ , eval ρ₁ N) M ≈ eval (ρ₂′ , eval ρ₂ N) M)
         & (lid⬖ ρ₁ ⁻¹)
         ⊗ (lid◆ ρ₂ ⁻¹))
        (eval≈ (χ , eval≈ χ υ₁ υ₂ N)
               (υ₁ , eval𝒰 υ₁ N)
               (υ₂ , eval𝒰 υ₂ N)
               M)
  ⦙ eval◆ (χ ⁻¹ ⦙ χ) υ₂ (idₛ , N) M ⁻¹

eval∼ χ υ₁ υ₂ (red⩕₁ M N) = eval≈ χ υ₁ υ₂ M
eval∼ χ υ₁ υ₂ (red⩕₂ M N) = eval≈ χ υ₁ υ₂ N

eval∼ {ρ₂ = ρ₂} χ υ₁ υ₂ (exp⇒ M) η {a₂ = a₂} p u₁ u₂
  rewrite eval⬗ (ρ₂ ⬖ η , a₂) (wkₑ idₑ) M ⁻¹
        | lid⬗ (ρ₂ ⬖ η)
        | eval⬖ η υ₂ M
        | rid○ η
  = eval≈ χ υ₁ υ₂ M η p u₁ u₂

eval∼ χ υ₁ υ₂ (exp⩕ M)  = eval≈ χ υ₁ υ₂ M
eval∼ χ υ₁ υ₂ (exp⫪ M) = tt

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

mutual
  -- (q≈)
  reify≈ : ∀ {A Γ} → {a₁ a₂ : Γ ⊩ A}
                   → a₁ ≈ a₂
                   → reify a₁ ≡ reify a₂
  reify≈ {⎵}      p = p
  reify≈ {A ⇒ B} F = ƛ & reify≈ (F (wkₑ {A = A} idₑ)
                                    (reflect≈ refl)
                                    (reflect𝒰 {A} 0)
                                    (reflect𝒰 {A} 0))
  reify≈ {A ⩕ B}  p = _,_ & reify≈ (proj₁ p)
                          ⊗ reify≈ (proj₂ p)
  reify≈ {⫪}     p = refl

  -- (u≈)
  reflect≈ : ∀ {A Γ} → {M₁ M₂ : Γ ⊢ⁿᵉ A}
                     → M₁ ≡ M₂
                     → reflect M₁ ≈ reflect M₂
  reflect≈ {⎵}      p = ne & p
  reflect≈ {A ⇒ B} p = λ η q u₁ u₂ →
                          reflect≈ (_∙_ & (renⁿᵉ η & p)
                                        ⊗ reify≈ q)
  reflect≈ {A ⩕ B}  p = reflect≈ (π₁ & p) , reflect≈ (π₂ & p)
  reflect≈ {⫪}     p = tt

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

sound : ∀ {Γ A} → {M₁ M₂ : Γ ⊢ A}
                → M₁ ∼ M₂
                → nf M₁ ≡ nf M₂
sound p = reify≈ (eval∼ id≈ id𝒰 id𝒰 p)

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Decision procedures for finite sets and subsets of finite sets
--
-- This module is DEPRECATED. Please use the Data.Fin.Properties
-- and Data.Fin.Subset.Properties directly.
------------------------------------------------------------------------

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

module Data.Fin.Dec where

open import Data.Fin.Properties public
  using (decFinSubset; any?; all?; ¬∀⟶∃¬-smallest; ¬∀⟶∃¬)

open import Data.Fin.Subset.Properties public
  using (_∈?_; _⊆?_; nonempty?; anySubset?)
  renaming (Lift? to decLift)


text:
module ial where

open import ial-datatypes public
open import logic public
open import thms public
open import termination public
open import error public
open import io public

max_stars_repo_name: mudathirmahgoub/cedille

max_issues_repo_name: mudathirmahgoub/cedille

max_forks_repo_name: mudathirmahgoub/cedille


text:
------------------------------------------------------------------------
-- Values
------------------------------------------------------------------------

open import Atom

module Values (atoms : χ-atoms) where

open import Equality.Propositional
open import Prelude hiding (const)

open import Chi atoms
open import Deterministic atoms

open χ-atoms atoms

-- Values.

mutual

  infixr 5 _∷_

  data Value : Exp → Type where
    lambda : ∀ x e → Value (lambda x e)
    const  : ∀ c {es} → Values es → Value (const c es)

  data Values : List Exp → Type where
    []  : Values []
    _∷_ : ∀ {e es} → Value e → Values es → Values (e ∷ es)

-- Constructor applications.

data Consts : Type where
  const : Const → List Consts → Consts

mutual

  data Constructor-application : Exp → Type where
    const : ∀ c {es} →
            Constructor-applications es →
            Constructor-application (const c es)

  data Constructor-applications : List Exp → Type where
    []  : Constructor-applications []
    _∷_ : ∀ {e es} →
          Constructor-application e → Constructor-applications es →
          Constructor-applications (e ∷ es)

-- Constructor applications are values.

mutual

  const→value : ∀ {e} → Constructor-application e → Value e
  const→value (const c cs) = const c (consts→values cs)

  consts→values : ∀ {es} → Constructor-applications es → Values es
  consts→values []       = []
  consts→values (c ∷ cs) = const→value c ∷ consts→values cs

-- The second argument of _⇓_ is always a Value.

mutual

  ⇓-Value : ∀ {e v} → e ⇓ v → Value v
  ⇓-Value (apply _ _ p)  = ⇓-Value p
  ⇓-Value (case _ _ _ p) = ⇓-Value p
  ⇓-Value (rec p)        = ⇓-Value p
  ⇓-Value lambda         = lambda _ _
  ⇓-Value (const ps)     = const _ (⇓⋆-Values ps)

  ⇓⋆-Values : ∀ {es vs} → es ⇓⋆ vs → Values vs
  ⇓⋆-Values []       = []
  ⇓⋆-Values (p ∷ ps) = ⇓-Value p ∷ ⇓⋆-Values ps

mutual

  values-compute-to-themselves : ∀ {v} → Value v → v ⇓ v
  values-compute-to-themselves (lambda _ _) = lambda
  values-compute-to-themselves (const _ ps) =
    const (values-compute-to-themselves⋆ ps)

  values-compute-to-themselves⋆ : ∀ {vs} → Values vs → vs ⇓⋆ vs
  values-compute-to-themselves⋆ []       = []
  values-compute-to-themselves⋆ (p ∷ ps) =
    values-compute-to-themselves p ∷ values-compute-to-themselves⋆ ps

values-only-compute-to-themselves :
  ∀ {v₁ v₂} → Value v₁ → v₁ ⇓ v₂ → v₁ ≡ v₂
values-only-compute-to-themselves p q =
  ⇓-deterministic (values-compute-to-themselves p) q

values-only-compute-to-themselves⋆ :
  ∀ {vs₁ vs₂} → Values vs₁ → vs₁ ⇓⋆ vs₂ → vs₁ ≡ vs₂
values-only-compute-to-themselves⋆ ps qs =
  ⇓⋆-deterministic (values-compute-to-themselves⋆ ps) qs

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Semigroup.Properties where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function using (_∘_; id)
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Logic using (_≡ₚ_)
open import Cubical.Functions.Embedding
open import Cubical.Data.Nat
open import Cubical.Data.NatPlusOne

open import Cubical.Algebra
open import Cubical.Algebra.Properties
open import Cubical.Algebra.Semigroup.Morphism
open import Cubical.Algebra.Magma.Properties using (isPropIsMagma)

open import Cubical.Relation.Binary
open import Cubical.Relation.Binary.Reasoning.Equality
open import Cubical.HITs.PropositionalTruncation

open import Cubical.Algebra.Semigroup.MorphismProperties public
  using (SemigroupPath; uaSemigroup; carac-uaSemigroup; Semigroup≡; caracSemigroup≡)

private
  variable
    ℓ ℓ′ : Level

isPropIsSemigroup : ∀ {S : Type ℓ} {_•_} → isProp (IsSemigroup S _•_)
isPropIsSemigroup {_} {_} {_•_} (issemigroup aMagma aAssoc) (issemigroup bMagma bAssoc) =
  cong₂ issemigroup (isPropIsMagma aMagma bMagma) (isPropAssociative (IsMagma.is-set aMagma) _•_ aAssoc bAssoc)

module SemigroupLemmas (S : Semigroup ℓ) where
  open Semigroup S

  ^-suc : ∀ x n → x ^ suc₊₁ n ≡ x ^ n • x
  ^-suc x one    = refl
  ^-suc x (2+ n) =
    x ^ suc₊₁ (2+ n)     ≡⟨⟩
    x ^ 1+ suc (suc n)   ≡⟨⟩
    x • (x • x ^ 1+ n)   ≡⟨⟩
    x • x ^ suc₊₁ (1+ n) ≡⟨ cong (x •_) (^-suc x (1+ n)) ⟩
    x • (x ^ 1+ n • x)   ≡˘⟨ assoc x (x ^ 1+ n) x ⟩
    x • x ^ 1+ n • x     ≡⟨⟩
    x ^ 2+ n • x         ∎

  ^-plus : ∀ x → Homomorphic₂ (x ^_) _+₊₁_ _•_
  ^-plus _ one _ = refl
  ^-plus x (2+ m) n =
    x ^ (1+ (suc m) +₊₁ n) ≡⟨⟩
    x • (x ^ (1+ m +₊₁ n)) ≡⟨ cong (x •_) (^-plus x (1+ m) n) ⟩
    x • (x ^ 1+ m • x ^ n) ≡˘⟨ assoc x (x ^ 1+ m) (x ^ n) ⟩
    x • x ^ 1+ m • x ^ n   ≡⟨⟩
    x ^ 2+ m • x ^ n       ∎

module Kernel {S : Semigroup ℓ} {T : Semigroup ℓ′} (hom : SemigroupHom S T) where
  private
    module S = Semigroup S
    module T = Semigroup T
  open SemigroupHom hom renaming (fun to f)

  Kernel′ : RawRel ⟨ S ⟩ ℓ′
  Kernel′ x y = f x ≡ f y

  isPropKernel : isPropValued Kernel′
  isPropKernel x y = T.is-set (f x) (f y)

  Kernel : Rel ⟨ S ⟩ ℓ′
  Kernel = fromRaw Kernel′ isPropKernel

  ker-reflexive : Reflexive Kernel
  ker-reflexive = refl

  ker-fromEq : FromEq Kernel
  ker-fromEq = rec (isPropKernel _ _) (cong f)

  ker-symmetric : Symmetric Kernel
  ker-symmetric = sym

  ker-transitive : Transitive Kernel
  ker-transitive = _∙_

  ker-isPreorder : IsPreorder Kernel
  ker-isPreorder = record
    { reflexive  = ker-reflexive
    ; transitive = ker-transitive
    }

  ker-isPartialEquivalence : IsPartialEquivalence Kernel
  ker-isPartialEquivalence = record
    { symmetric  = ker-symmetric
    ; transitive = ker-transitive
    }

  ker-isEquivalence : IsEquivalence Kernel
  ker-isEquivalence = record
    { isPartialEquivalence = ker-isPartialEquivalence
    ; reflexive            = ker-reflexive
    }

  ker⇒id→emb : Kernel ⇒ _≡ₚ_ → isEmbedding f
  ker⇒id→emb ker⇒id = injEmbedding S.is-set T.is-set (λ p → rec (S.is-set _ _) id (ker⇒id p))

  emb→ker⇒id : isEmbedding f → Kernel ⇒ _≡ₚ_
  emb→ker⇒id isemb {x} {y} = ∣_∣ ∘ invIsEq (isemb x y)


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

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

postulate
  funextP : {A : Prop} {B : A → Set} {f g : (a : A) → B a} (h : (x : A) → f x ≡ g x) → f ≡ g

test      : {A : Prop} {B : A → Set} {f g : (a : A) → B a} (h : (x : A) → f x ≡ g x) → f ≡ g
test h = funextP h

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------------
-- Parametrized preorder reasoning
------------------------------------------------------------------------------

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

module Common.Relation.Binary.PreorderReasoning
  {D     : Set}
  (_∼_   : D → D → Set)
  (refl  : ∀ {x} → x ∼ x)
  (trans : ∀ {x y z} → x ∼ y → y ∼ z → x ∼ z)
  where

infix  3 _∎
infixr 2 _∼⟨_⟩_

------------------------------------------------------------------------------
-- From (Mu, S.-C., Ko, H.-S. and Jansson, P. (2009)).
--
-- N.B. Unlike Ulf's thesis (and the Agda standard library 0.8.1) this
-- set of combinators do not use a wrapper data type.

_∼⟨_⟩_ : ∀ x {y z} → x ∼ y → y ∼ z → x ∼ z
_ ∼⟨ x∼y ⟩ y∼z = trans x∼y y∼z

_∎ : ∀ x → x ∼ x
_∎ _ = refl

------------------------------------------------------------------------------
-- References
--
-- Mu, S.-C., Ko, H.-S. and Jansson, P. (2009). Algebra of programming
-- in Agda: Dependent types for relational program derivation. Journal
-- of Functional Programming 19.5, pp. 545–579.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module SubstLemmas where

open import Level using (Level)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; subst; cong₂)
open import Data.Nat using (ℕ; _+_; _*_)

------------------------------------------------------------------------------
-- Lemmas about subst (and a couple about trans)

subst-dist :
  {a b : Level} {A : Set a} {B : A → Set b}
  (f : {x : A} → B x → B x → B x) →
  {x₁ x₂ : A} → (x₂≡x₁ : x₂ ≡ x₁) → (v₁ v₂ : B x₂) →
  subst B x₂≡x₁ (f v₁ v₂) ≡ f (subst B x₂≡x₁ v₁) (subst B x₂≡x₁ v₂)
subst-dist f refl v₁ v₂ = refl

subst-trans :
  {a b : Level} {A : Set a} {B : A → Set b} {x₁ x₂ x₃ : A} →
  (x₂≡x₁ : x₂ ≡ x₁) → (x₃≡x₂ : x₃ ≡ x₂) → (v : B x₃) →
  subst B x₂≡x₁ (subst B x₃≡x₂ v) ≡ subst B (trans x₃≡x₂ x₂≡x₁) v
subst-trans refl refl v = refl

subst₂+ : {b : Level} {B : ℕ → Set b} {x₁ x₂ x₃ x₄ : ℕ} →
  (x₂≡x₁ : x₂ ≡ x₁) → (x₄≡x₃ : x₄ ≡ x₃) → (v₁ : B x₂) → (v₂ : B x₄) →
  (f : {x₁ x₂ : ℕ} → B x₁ → B x₂ → B (x₁ + x₂)) →
  subst B (cong₂ _+_ x₂≡x₁ x₄≡x₃) (f v₁ v₂) ≡
  f (subst B x₂≡x₁ v₁) (subst B x₄≡x₃ v₂)
subst₂+ refl refl v₁ v₂ f = refl

subst₂* : {b : Level} {B : ℕ → Set b} {x₁ x₂ x₃ x₄ : ℕ} →
  (x₂≡x₁ : x₂ ≡ x₁) → (x₄≡x₃ : x₄ ≡ x₃) → (v₁ : B x₂) → (v₂ : B x₄) →
  (f : {x₁ x₂ : ℕ} → B x₁ → B x₂ → B (x₁ * x₂)) →
  subst B (cong₂ _*_ x₂≡x₁ x₄≡x₃) (f v₁ v₂) ≡
  f (subst B x₂≡x₁ v₁) (subst B x₄≡x₃ v₂)
subst₂* refl refl v₁ v₂ f = refl

trans-syml : {A : Set} {x y : A} → (p : x ≡ y) → trans (sym p) p ≡ refl
trans-syml refl = refl

trans-symr : {A : Set} {x y : A} → (p : x ≡ y) → trans p (sym p) ≡ refl
trans-symr refl = refl

subst-subst :
  {a b : Level} {A : Set a} {B : A → Set b}
  {x y : A} → (eq : x ≡ y) → (eq' : y ≡ x) → (irr : sym eq ≡ eq') → (v : B y) →
  subst B eq (subst B eq' v) ≡ v
subst-subst refl .refl refl v = refl

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
-- Andreas, 2015-12-29
-- with-clause stripping for record patterns

-- {-# OPTIONS -v tc.with.strip:60 #-}

record R : Set1 where
  field
    f : Set

test : R → Set1
test record{ f = a } with a
... | x = R

test1 : R → Set1
test1 record{ f = a } with a
test1 record{ f = a } | _ = R

test2 : R → Set1
test2 record{ f = a } with a
test2 record{ f = _ } | _ = R

-- Visible fields may be missing.
test3 : R → Set1
test3 record{ f = a } with a
test3 record{} | _ = R

-- With-clauses may specify more fields than the parent
test4 : R → Set1
test4 record{} with R
test4 record{ f = _ } | _ = R

-- all should pass


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

module TypeTheory.HoTT.Data.Sum.Properties where

-- agda-stdlib
open import Level
open import Data.Empty
open import Data.Product
open import Data.Sum
open import Function.Base
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

-- agda-misc
open import TypeTheory.HoTT.Base

private
  variable
    a b : Level
    A : Set a
    B : Set b

isProp-⊎ : ¬ (A × B) → isProp A → isProp B → isProp (A ⊎ B)
isProp-⊎ ¬[A×B] A-isP B-isP (inj₁ x₁) (inj₁ x₂) = cong inj₁ (A-isP x₁ x₂)
isProp-⊎ ¬[A×B] A-isP B-isP (inj₁ x₁) (inj₂ y₂) = ⊥-elim $ ¬[A×B] (x₁ , y₂)
isProp-⊎ ¬[A×B] A-isP B-isP (inj₂ y₁) (inj₁ x₂) = ⊥-elim $ ¬[A×B] (x₂ , y₁)
isProp-⊎ ¬[A×B] A-isP B-isP (inj₂ y₁) (inj₂ y₂) = cong inj₂ (B-isP y₁ y₂)


text:
module Proofs where

open import Agda.Builtin.Equality
open import Relation.Binary.PropositionalEquality.Core
open import Data.Nat

open ≡-Reasoning

open import Classes

data Vec : ℕ → Set → Set where
  Nil  : ∀ {a} → Vec 0 a
  Cons : ∀ {n A} → (a : A) → Vec n A → Vec (suc n) A

cons-cong : ∀ {n A} {a c : A} {b d : Vec n A} → a ≡ c → b ≡ d → Cons a b ≡ Cons c d
cons-cong {_} {_} {a} {c} {b} {d} p q = begin
  Cons a b ≡⟨ cong (λ x → Cons a x) q ⟩
  Cons a d ≡⟨ cong (λ x → Cons x d) p ⟩
  Cons c d ∎

instance
  VecF : {n : ℕ} → Functor (Vec n)
  VecF = record {
    fmap = fmap' ;
    F-id = id' ;
    F-∘ = comp' }
    where
      fmap' : ∀ {n A B} → (A → B) → Vec n A → Vec n B
      fmap' f Nil = Nil
      fmap' f (Cons a v) = Cons (f a) (fmap' f v)

      id' : ∀ {n A} → (a : Vec n A) → fmap' id a ≡ a
      id' Nil = refl
      id' (Cons a v) = cong (λ w → Cons a w) (id' v)

      comp' : ∀ {n A B C} → (g : B → C) (f : A → B) (a : Vec n A) → fmap' (g ∘ f) a ≡ (fmap' g ∘ fmap' f) a
      comp' g f Nil = refl
      comp' g f (Cons a v) = cons-cong refl (comp' g f v)

full : ∀ {A} → A → (n : ℕ) → Vec n A
full x zero = Nil
full x (suc n) = Cons x (full x n)

zipWith : ∀ {n A B C} → (A → B → C) → Vec n A → Vec n B → Vec n C
zipWith _ Nil Nil = Nil
zipWith f (Cons a v) (Cons b w) = Cons (f a b) (zipWith f v w)

instance
  VecA : {n : ℕ} → Applicative (Vec n)
  VecA {n} = record
           { pure = λ x → full x n
           ; _<*>_ = ap'
           ; A-id = id'
           ; A-∘ = comp'
           ; A-hom = hom'
           ; A-ic = ic'
           }
    where
      ap' : ∀ {n A B} (v : Vec n (A → B)) (w : Vec n A) → Vec n B
      ap' Nil Nil = Nil
      ap' (Cons a v) (Cons b w) = Cons (a b) (ap' v w)

      id' : ∀ {n A} (v : Vec n A) → ap' (full id n) v ≡ v
      id' Nil = refl
      id' (Cons a v) = cons-cong refl (id' v)

      comp' : ∀ {n A B C} → (u : Vec n (B → C)) (v : Vec n (A → B)) (w : Vec n A)
              → ap' (ap' (ap' (full _∘_ n) u) v) w ≡ ap' u (ap' v w)
      comp' Nil Nil Nil = refl
      comp' (Cons a u) (Cons b v) (Cons c w) = cons-cong refl (comp' u v w)

      hom' : ∀ {n A B} (f : A → B) (x : A) → ap' (full f n) (full x n) ≡ full (f x) n
      hom' {zero} f x = refl
      hom' {suc n} f x = cons-cong refl (hom' {n} f x)

      ic' : ∀ {n A B} (u : Vec n (A → B)) (y : A) → ap' u (full y n) ≡ ap' (full (_$ y) n) u
      ic' Nil y = refl
      ic' (Cons a u) y = cons-cong refl (ic' u y)

tail : ∀ {n A} → Vec (suc n) A → Vec n A
tail (Cons x v) = v

diag : ∀ {n A} → Vec n (Vec n A) → Vec n A
diag Nil = Nil
diag (Cons (Cons a w) v) = Cons a (diag (fmap tail v))

fmap-pure : ∀ {A B F} {{aF : Applicative F}} (f : A → B) (x : A)
            → fmap f (Applicative.pure aF x) ≡ Applicative.pure aF (f x)
fmap-pure f x = begin
  fmap f (pure x) ≡⟨ sym (appFun f (pure x)) ⟩
  pure f <*> pure x ≡⟨ A-hom f x ⟩
  pure (f x) ∎

diag-full : ∀ {A} (n : ℕ) (v : Vec n A) → diag (full v n) ≡ v
diag-full _ Nil = refl
diag-full (suc n) (Cons a v) = cons-cong refl (begin
  diag (fmap tail (full (Cons a v) n)) ≡⟨ cong diag (fmap-pure tail (Cons a v)) ⟩
  diag (full v n) ≡⟨ diag-full n v ⟩
  v ∎)

instance
  VecM : {n : ℕ} → Monad (Vec n)
  VecM = record { _>>=_ = bind' ;
                  left-1 = left' ;
                  right-1 = {!!} ;
                  assoc = {!!} }

    where
      bind' : ∀ {n A B} → Vec n A → (A → Vec n B) → Vec n B
      bind' v f = diag (fmap f v)

      left' : ∀ {n A B} (a : A) (k : A → Vec n B) → bind' (pure a) k ≡ k a
      left' {n} a k = begin
          diag (fmap k (full a n)) ≡⟨ cong diag (fmap-pure k a) ⟩
          diag (full (k a) n) ≡⟨ diag-full n (k a) ⟩
          k a ∎

      right' : ∀ {n A} (m : Vec n A) → bind' m pure ≡ m
      right' Nil = refl
      right' (Cons a m) = begin
        bind' (Cons a m) pure ≡⟨ refl ⟩
        diag (fmap pure (Cons a m)) ≡⟨ cons-cong refl {!!} ⟩ -- :(
        Cons a m ∎

max_stars_repo_name: samuelhklumpers/strong-vector

max_issues_repo_name: samuelhklumpers/strong-vector

max_forks_repo_name: samuelhklumpers/strong-vector


text:
{-# OPTIONS --without-K #-}
module Model.Term where

open import Cats.Category

open import Model.Size as MS using (_<_ ; ⟦_⟧Δ ; ⟦_⟧n ; ⟦_⟧σ)
open import Model.Type as MT
open import Util.HoTT.Equiv
open import Util.Prelude hiding (id ; _∘_ ; _×_)
open import Source.Size as SS using (v0 ; v1 ; ⋆)
open import Source.Size.Substitution.Theory
open import Source.Size.Substitution.Universe as SU using (Sub⊢ᵤ)
open import Source.Term

import Model.RGraph as RG
import Source.Type as ST

open Category._≅_
open MS.Size
open MS._<_
open MS._≤_
open RG._⇒_
open SS.Size
open SS.Ctx
open ST.Ctx

⟦_⟧x : ∀ {Δ Γ x T}
  → Δ , Γ ⊢ₓ x ∶ T
  → ⟦ Γ ⟧Γ ⇒ ⟦ T ⟧T
⟦_⟧x {Γ = Γ ∙ T} zero = π₂ ⟦ Γ ⟧Γ
⟦ suc {U = U} x ⟧x = ⟦ x ⟧x ∘ π₁ ⟦ U ⟧T

⟦abs⟧ : ∀ Δ (Γ : ST.Ctx Δ) T U
  → ⟦ Γ ∙ T ⟧Γ ⇒ ⟦ U ⟧T
  → ⟦ Γ ⟧Γ ⇒ ⟦ T ⟧T ↝ ⟦ U ⟧T
⟦abs⟧ Δ Γ T U t = curry ⟦ Γ ⟧Γ ⟦ T ⟧T ⟦ U ⟧T t

⟦app⟧ : ∀ Δ (Γ : ST.Ctx Δ) T U
  → ⟦ Γ ⟧Γ ⇒ ⟦ T ⟧T ↝ ⟦ U ⟧T
  → ⟦ Γ ⟧Γ ⇒ ⟦ T ⟧T
  → ⟦ Γ ⟧Γ ⇒ ⟦ U ⟧T
⟦app⟧ Δ Γ T U t u = eval ⟦ T ⟧T ⟦ U ⟧T ∘ ⟨ t , u ⟩

⟦absₛ⟧ : ∀ Δ n (Γ : ST.Ctx Δ) (T : ST.Type (Δ ∙ n))
  → ⟦ Γ [ SU.Wk ]ᵤ ⟧Γ ⇒ ⟦ T ⟧T
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Π n , T ⟧T
⟦absₛ⟧ Δ n Γ T t = MT.absₛ (t ∘ ⟦subΓ⟧ SU.Wk Γ .back)

⟦appₛ⟧ : ∀ Δ m n (Γ : ST.Ctx Δ) T
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Π n , T ⟧T
  → m SS.< n
  → ⟦ Γ ⟧Γ ⇒ ⟦ T [ SU.Sing m ]ᵤ ⟧T
⟦appₛ⟧ Δ m n Γ T t m<n = ⟦subT⟧ (SU.Sing m<n) T .back ∘ MT.appₛ m<n t

⟦zero⟧ : ∀ Δ (Γ : ST.Ctx Δ) n
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Nat n ⟧T
⟦zero⟧ Δ Γ n = record
  { fobj = λ {δ} γ → zero≤ (⟦ n ⟧n .fobj δ)
  ; feq = λ δ≈δ′ x≈y → refl
  }

⟦suc⟧ : ∀ Δ (Γ : ST.Ctx Δ) {m n}
  → m SS.< n
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Nat m ⟧T
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Nat n ⟧T
⟦suc⟧ Δ Γ m<n i = record
  { fobj = λ γ → suc≤ _ _ (MS.⟦<⟧ m<n) (i .fobj γ)
  ; feq = λ δ≈δ′ x≈y → cong suc (i .feq _ x≈y)
  }

⟦caseNat⟧ : ∀ Δ (Γ : ST.Ctx Δ) n T
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Nat n ⟧T
  → ⟦ Γ ⟧Γ ⇒ ⟦ T ⟧T
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Π n , ST.Nat v0 ST.⇒ T [ SU.Wk ]ᵤ ⟧T
  → ⟦ Γ ⟧Γ ⇒ ⟦ T ⟧T
⟦caseNat⟧ Δ Γ n T i z s = record
  { fobj = λ γ → caseℕ≤ (i .fobj γ) (z .fobj γ)
      λ m m<n i
        → ⟦subT⟧ SU.Wk T .forth .fobj
            (s .fobj γ .arr m m<n .fobj i)
  ; feq = λ {δ δ′} δ≈δ′ {γ γ′} γ≈γ′
      → caseℕ≤-pres (⟦ T ⟧T .eq δ≈δ′) (i .fobj γ) (i .fobj γ′)
          (z .fobj γ) (z .fobj γ′) _ _ (i .feq _ γ≈γ′)
          (z .feq _ γ≈γ′)
          λ m m<n m′ m′<n′ j j′ j≡j′
            → ⟦subT⟧ SU.Wk T .forth .feq _
                (s .feq _ γ≈γ′ m m<n m′ m′<n′ j≡j′)
  }

⟦cons⟧ : ∀ Δ (Γ : ST.Ctx Δ) n
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Nat ∞ ⟧T
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Π n , ST.Stream v0 ⟧T
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Stream n ⟧T
⟦cons⟧ Δ Γ n i is = record
  { fobj = λ γ → MT.cons (i .fobj γ .proj₁) (is .fobj γ .arr)
  ; feq = λ δ≈δ′ γ≈γ′ k k≤nδ k≤nδ′
      → cons-≡⁺ (i .feq _ γ≈γ′)
          (λ m m<n m<n′ k k≤m → is .feq _ γ≈γ′ m m<n m m<n′ k k≤m k≤m)
          k k≤nδ k≤nδ′
  }

⟦head⟧ : ∀ Δ (Γ : ST.Ctx Δ) n
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Stream n ⟧T
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Nat ∞ ⟧T
⟦head⟧ Δ Γ n is = record
  { fobj = λ γ → MT.head (is .fobj γ) , MS.<→≤ MS.zero<∞
  ; feq = λ δ≈δ′ γ≈γ′ → head-≡⁺ (is .feq _ γ≈γ′)
  }

⟦tail⟧ : ∀ Δ (Γ : ST.Ctx Δ) {m n}
  → m SS.< n
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Stream n ⟧T
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Stream m ⟧T
⟦tail⟧ Δ Γ m<n is = record
  { fobj = λ γ → MT.tail (is .fobj γ) _ (MS.⟦<⟧ m<n)
  ; feq = λ δ≈δ′ γ≈γ′ i i≤mδ i≤mδ′
      → tail-≡⁺ (is .feq _ γ≈γ′) _ _ (MS.⟦<⟧ m<n) (MS.⟦<⟧ m<n) i i≤mδ i≤mδ′
  }

⟦fix⟧ : ∀ Δ (Γ : ST.Ctx Δ) n T
  → n SS.< ⋆
  → ⟦ Γ ⟧Γ ⇒ ⟦ ST.Π ⋆ , (ST.Π v0 , T [ SU.Skip ]ᵤ) ST.⇒ T ⟧T
  → ⟦ Γ ⟧Γ ⇒ ⟦ T [ SU.Sing n ]ᵤ ⟧T
⟦fix⟧ Δ Γ n T n<⋆ t = ⟦subT⟧ (SU.Sing n<⋆) T .back ∘ term⇒
  module ⟦fix⟧ where
    go
      : Σ[ f ∈ (∀ n n<⋆ δ → ⟦ Γ ⟧Γ .Obj δ → ⟦ T ⟧T .Obj (δ , n , n<⋆)) ]
        Σ[ f-param ∈ (∀ n n′ n<⋆ n′<⋆ δ δ′ (γ : ⟦ Γ ⟧Γ .Obj δ) (γ′ : ⟦ Γ ⟧Γ .Obj δ′)
          → ⟦ Γ ⟧Γ .eq _ γ γ′ → ⟦ T ⟧T .eq _ (f n n<⋆ δ γ) (f n′ n′<⋆ δ′ γ′)) ]
          (∀ {n} → f n ≡ _)
    go = MS.<-indΣ′
      (λ n → ∀ n<⋆ δ (γ : ⟦ Γ ⟧Γ .Obj δ) → ⟦ T ⟧T .Obj (δ , n , n<⋆))
      (λ n m f g → ∀ n<⋆ m<⋆ δ δ′ γ γ′ (γ≈γ′ : ⟦ Γ ⟧Γ .eq _ γ γ′)
        → ⟦ T ⟧T .eq _ (f n<⋆ δ γ) (g m<⋆ δ′ γ′))
      (λ n rec rec-resp n<⋆ δ γ
        → t .fobj γ .arr n n<⋆ .fobj
            (⟦∀⟧′-resp-≈⟦Type⟧ (⟦subT⟧ SU.Skip T) .back record
              { arr = λ m m<n → rec m m<n (MS.<-trans m<n n<⋆) δ γ
              ; param = λ m m<n m′ m′<n
                  → rec-resp m m<n m′ m′<n _ _ δ δ γ γ (⟦ Γ ⟧Γ .eq-refl γ)
              }))
      λ n g g-resp m h h-resp g≈h n<⋆ m<⋆ δ δ′ γ γ′ γ≈γ′
        → t .feq _ γ≈γ′ n n<⋆ m m<⋆ λ k k<n k′ k′<m
            → ⟦subT⟧ SU.Skip T .back .feq _
                (g≈h k k<n k′ k′<m _ _ δ δ′ γ γ′ γ≈γ′)

    term : ∀ n n<⋆ δ → ⟦ Γ ⟧Γ .Obj δ → ⟦ T ⟧T .Obj (δ , n , n<⋆)
    term = go .proj₁

    term-param : ∀ n n′ n<⋆ n′<⋆ δ δ′ (γ : ⟦ Γ ⟧Γ .Obj δ) (γ′ : ⟦ Γ ⟧Γ .Obj δ′)
      → ⟦ Γ ⟧Γ .eq _ γ γ′
      → ⟦ T ⟧T .eq _ (term n n<⋆ δ γ) (term n′ n′<⋆ δ′ γ′)
    term-param = go .proj₂ .proj₁

    term⇒ : ⟦ Γ ⟧Γ ⇒ subT ⟦ SU.Sing n<⋆ ⟧σ ⟦ T ⟧T
    term⇒ = record
      { fobj = term _ _ _
      ; feq = λ δ≈δ′ → term-param _ _ _ _ _ _ _ _
      }

    term-unfold₀ : ∀ {n}
      → term n
      ≡ λ n<⋆ δ γ → t .fobj γ .arr n n<⋆ .fobj
            (⟦∀⟧′-resp-≈⟦Type⟧ (⟦subT⟧ SU.Skip T) .back record
              { arr = λ m m<n → term m (MS.<-trans m<n n<⋆) δ γ
              ; param = λ m m<n m′ m′<n
                  → term-param _ _ _ _ _ _ _ _ (⟦ Γ ⟧Γ .eq-refl γ)
              })
    term-unfold₀ = go .proj₂ .proj₂

    term-unfold : ∀ {n n<⋆ δ γ}
      → term n n<⋆ δ γ
      ≡ t .fobj γ .arr n n<⋆ .fobj
          (⟦∀⟧′-resp-≈⟦Type⟧ (⟦subT⟧ SU.Skip T) .back record
            { arr = λ m m<n → term m (MS.<-trans m<n n<⋆) δ γ
            ; param = λ m m<n m′ m′<n
                → term-param _ _ _ _ _ _ _ _ (⟦ Γ ⟧Γ .eq-refl γ)
            })
    term-unfold {n} {n<⋆} {δ} {γ} = cong (λ f → f n<⋆ δ γ) term-unfold₀

⟦_⟧t : ∀ {Δ Γ t T}
  → Δ , Γ ⊢ t ∶ T
  → ⟦ Γ ⟧Γ ⇒ ⟦ T ⟧T
⟦ var ⊢x ⟧t = ⟦ ⊢x ⟧x
⟦ abs {Δ = Δ} {Γ} {T} {t} {U} ⊢t ⟧t = ⟦abs⟧ Δ Γ T U ⟦ ⊢t ⟧t
⟦ app {Δ} {Γ} {T = T} {U = U} ⊢t ⊢u ⟧t = ⟦app⟧ Δ Γ T U ⟦ ⊢t ⟧t ⟦ ⊢u ⟧t
⟦ absₛ {Δ} {n} {T = T} ⊢t refl ⟧t = ⟦absₛ⟧ Δ n _ T ⟦ ⊢t ⟧t
⟦ appₛ {Δ} {m} {n} {Γ} {T = T} m<n ⊢t refl ⟧t = ⟦appₛ⟧ Δ m n Γ T ⟦ ⊢t ⟧t m<n
⟦ zero {Δ} {n} {Γ} n<⋆ ⟧t = ⟦zero⟧ Δ Γ n
⟦ suc {Δ} {Γ = Γ} n<⋆ m<n ⊢i ⟧t = ⟦suc⟧ Δ Γ m<n ⟦ ⊢i ⟧t
⟦ cons {Δ} {n} {Γ} n<⋆ ⊢i ⊢is ⟧t = ⟦cons⟧ Δ Γ n ⟦ ⊢i ⟧t ⟦ ⊢is ⟧t
⟦ head {Δ} {n} {Γ} n<⋆ ⊢is ⟧t = ⟦head⟧ Δ Γ n ⟦ ⊢is ⟧t
⟦ tail {Δ} {n} {m} {Γ} n<⋆ m<n ⊢is ⟧t = ⟦tail⟧ Δ Γ m<n ⟦ ⊢is ⟧t
⟦ caseNat {Δ} {n} {Γ} {T = T} n<⋆ ⊢i ⊢z ⊢s refl ⟧t
  = ⟦caseNat⟧ Δ Γ n T ⟦ ⊢i ⟧t ⟦ ⊢z ⟧t ⟦ ⊢s ⟧t
⟦ fix {Δ} {n} {Γ} {T = T} n<⋆ ⊢t refl refl ⟧t
  = ⟦fix⟧ Δ Γ n T n<⋆ ⟦ ⊢t ⟧t

⟦_⟧ν : ∀ {Δ} {Γ Ψ : ST.Ctx Δ} {ν} → ν ∶ Γ ⇛ Ψ → ⟦ Γ ⟧Γ ⇒ ⟦ Ψ ⟧Γ
⟦ [] ⟧ν = ! _
⟦ Snoc ⊢ν ⊢t ⟧ν = ⟨ ⟦ ⊢ν ⟧ν , ⟦ ⊢t ⟧t ⟩

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
------------------------------------------------------------------------------
-- Co-inductive natural numbers
------------------------------------------------------------------------------

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

module FOTC.Data.Conat where

open import FOTC.Base
open import FOTC.Data.Conat.Type public

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

postulate
  ∞    : D
  ∞-eq : ∞ ≡ succ₁ ∞
{-# ATP axiom ∞-eq #-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An equality postulate which evaluates
------------------------------------------------------------------------

module Relation.Binary.PropositionalEquality.TrustMe where

open import Relation.Binary.PropositionalEquality

private
 primitive
   primTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y

-- trustMe {x = x} {y = y} evaluates to refl if x and y are
-- definitionally equal.
--
-- For an example of the use of trustMe, see Data.String._≟_.

trustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
trustMe = primTrustMe


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Instances.Semilattice where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.Semilattice

open import Cubical.Categories.Category
open import Cubical.Categories.Instances.Poset

open Category

module _ {ℓ} (L : Semilattice ℓ) where
  -- more convenient than working with meet-semilattices
  -- as joins are limits
  open JoinSemilattice L

  SemilatticeCategory : Category ℓ ℓ
  SemilatticeCategory = PosetCategory IndPoset


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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Functions.Definition
open import Setoids.Setoids
open import Setoids.Subset
open import Graphs.Definition
open import Sets.FinSet.Definition
open import Sets.FinSet.Lemmas
open import Numbers.Naturals.Semiring
open import Sets.EquivalenceRelations

module Graphs.PathGraph where

nNotSucc : {n : ℕ} → (n ≡ succ n) → False
nNotSucc {zero} ()
nNotSucc {succ n} pr = nNotSucc (succInjective pr)

PathGraph : (n : ℕ) → Graph _ (reflSetoid (FinSet (succ n)))
Graph._<->_ (PathGraph n) x y = (toNat x ≡ succ (toNat y)) || (toNat y ≡ succ (toNat x))
Graph.noSelfRelation (PathGraph n) x (inl bad) = nNotSucc bad
Graph.noSelfRelation (PathGraph n) x (inr bad) = nNotSucc bad
Graph.symmetric (PathGraph n) (inl x) = inr x
Graph.symmetric (PathGraph n) (inr x) = inl x
Graph.wellDefined (PathGraph n) refl refl i = i


text:
-- Care needs to be taken to distinguish between instance solutions with and
-- without leftover constraints.
module _ where

_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → A → C
(f ∘ g) x = f (g x)

postulate
  Functor : (Set → Set) → Set₁
  fmap : ∀ {F} {{_ : Functor F}} {A B} → (A → B) → F A → F B
  List : Set → Set
  map : ∀ {A B} → (A → B) → List A → List B
  Term : Set
  Arg : Set → Set

  instance FunArg : Functor Arg

postulate
  SafeTerm  : Set
  safe-term : SafeTerm → Term
  DeBruijn : Set → Set₁
  weaken : ∀ {A} {{_ : DeBruijn A}} → A → A
  instance
    DBTerm : DeBruijn Term
    DBArg : ∀ {A} {{_ : DeBruijn A}} → DeBruijn (Arg A)

toArgs : List (Arg SafeTerm) → List (Arg Term)
toArgs = map (weaken ∘ fmap safe-term)


text:
-- There was a problem with reordering telescopes.
module Issue234 where

postulate
  A : Set
  P : A → Set

data List : Set where
  _∷ : A → List

data _≅_ {x : A}(p : P x) : ∀ {y} → P y → Set where
  refl : p ≅ p

data _≡_ (x : A) : A → Set where
  refl : x ≡ x

data Any (x : A) : Set where
  here : P x → Any x

it : ∀ {x : A} → Any x → A
it {x} (here _) = x

prf : ∀ {x : A}(p : Any x) → P (it p)
prf (here px) = px

foo : (x : A) (p : Any x) →
      (f : ∀ {y} → it p ≡ y → P y) →
      f refl ≅ prf p →
      Set₁
foo x (here ._) f refl = Set


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

open import HoTT

module lib.Quaternions where

data Sign : Type₀ where
  plus : Sign
  minus : Sign

opposite : Sign → Sign
opposite plus = minus
opposite minus = plus

_·_ : Sign → Sign → Sign
plus · x = x
minus · x = opposite x

·unitr : (x : Sign) → x · plus == x
·unitr plus = idp
·unitr minus = idp

·assoc : (x y z : Sign) → (x · y) · z == x · (y · z)
·assoc plus y z = idp
·assoc minus plus z = idp
·assoc minus minus plus = idp
·assoc minus minus minus = idp

·cohl : {x y : Sign} → x == y → (z : Sign) → x · z == y · z
·cohl idp z = idp

·cohr : (x : Sign) → {y z : Sign} → y == z → x · y == x · z
·cohr x idp = idp

·comm : (x y : Sign) → x · y == y · x
·comm plus plus = idp
·comm plus minus = idp
·comm minus plus = idp
·comm minus minus = idp

data Dir : Type₀ where
  i : Dir
  j : Dir
  k : Dir

shift : Dir → Dir
shift i = j
shift j = k
shift k = i

data QU : Type₀ where
  one : QU
  dir : Dir → QU

Q : Type₀
Q = Σ Sign λ _ → QU

multWithSign : Dir → Dir → Q
multWithSign i i = minus , one
multWithSign i j = plus , dir k
multWithSign i k = minus , dir j
multWithSign j i = minus , dir k
multWithSign j j = minus , one
multWithSign j k = plus , dir i
multWithSign k i = plus , dir j
multWithSign k j = minus , dir i
multWithSign k k = minus , one

_⊙_ : Q → Q → Q
(s , one) ⊙ (t , u) = s · t , u
(s , dir d) ⊙ (t , one) = s · t , dir d
(s , dir d) ⊙ (t , dir e) with multWithSign d e
... | (x , u) = (s · t) · x , u

inv : Q → Q
inv (x , one) = x , one
inv (x , dir d) = opposite x , dir d

unitl : (a : Q) → (plus , one) ⊙ a == a
unitl (x , u) = idp

unitr : (a : Q) → a ⊙ (plus , one) == a
unitr (x , one) = pair×= (·unitr x) idp
unitr (x , dir d) = pair×= (·unitr x) idp

assoc : (a b c : Q) → (a ⊙ b) ⊙ c == a ⊙ (b ⊙ c)
assoc (x , one) (y , one) (z , w) = pair×= (·assoc x y z) idp
assoc (x , one) (y , dir d) (z , one) = pair×= (·assoc x y z) idp
assoc (x , one) (y , dir d) (z , dir e) with multWithSign d e
... | (w , u) = pair×= lemma idp
  where
    lemma : ((x · y) · z) · w == x · ((y · z) · w)
    lemma = ((x · y) · z) · w     =⟨ ·assoc (x · y) z w ⟩
            (x · y) · (z · w)     =⟨ ·assoc x y (z · w) ⟩
            x · (y · (z · w))     =⟨ ·cohr x (! (·assoc y z w)) ⟩
            x · ((y · z) · w) ∎
assoc (x , dir d) (y , one) (z , one) = pair×= (·assoc x y z) idp
assoc (x , dir d) (y , one) (z , dir f) with multWithSign d f
... | (w , u) = pair×= lemma idp
  where
    lemma : ((x · y) · z) · w == (x · (y · z)) · w
    lemma = ((x · y) · z) · w     =⟨ ·cohl (·assoc x y z) w ⟩
            (x · (y · z)) · w ∎
assoc (x , dir d) (y , dir e) (z , one) with multWithSign d e
assoc (x , dir d) (y , dir e) (z , one) | (w , one) = pair×= lemma idp
  where
    lemma : ((x · y) · w) · z == (x · (y · z)) · w
    lemma = ((x · y) · w) · z     =⟨ ·assoc (x · y) w z ⟩
            (x · y) · (w · z)     =⟨ ·cohr (x · y) (·comm w z) ⟩
            (x · y) · (z · w)     =⟨ ! (·assoc (x · y) z w) ⟩
            ((x · y) · z) · w     =⟨ ·cohl (·assoc x y z) w ⟩
            (x · (y · z)) · w ∎
assoc (x , dir d) (y , dir e) (z , one) | (w , dir g) = pair×= lemma idp
  where
    lemma : ((x · y) · w) · z == (x · (y · z)) · w
    lemma = ((x · y) · w) · z     =⟨ ·assoc (x · y) w z ⟩
            (x · y) · (w · z)     =⟨ ·cohr (x · y) (·comm w z) ⟩
            (x · y) · (z · w)     =⟨ ! (·assoc (x · y) z w) ⟩
            ((x · y) · z) · w     =⟨ ·cohl (·assoc x y z) w ⟩
            (x · (y · z)) · w ∎
assoc (x , dir d) (y , dir e) (z , dir f) with multWithSign d e | multWithSign e f
assoc (x , dir d) (y , dir e) (z , dir f) | a , one | b , v = {!!}
assoc (x₁ , dir d) (y , dir e) (z , dir f) | a , dir x | b , v = {!!}

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: UlrikBuchholtz/HoTT-Agda

max_forks_repo_name: UlrikBuchholtz/HoTT-Agda


text:
open import SOAS.Metatheory.Syntax

-- Initial (⅀, 𝔛)-meta-algebra 𝕋 𝔛 is the free ⅀-monoid on 𝔛
module SOAS.Metatheory.FreeMonoid {T : Set} (Syn : Syntax {T}) where

open Syntax Syn

open import SOAS.Common
open import SOAS.Families.Core {T}
open import SOAS.Context {T}
open import SOAS.Variable {T}
open import SOAS.Construction.Structure as Structure
open import SOAS.Abstract.Hom {T}
import SOAS.Abstract.Coalgebra {T} as →□ ; open →□.Sorted
import SOAS.Abstract.Box {T} as □ ; open □.Sorted

open import Categories.Monad

open import SOAS.Abstract.Monoid

open import SOAS.Coalgebraic.Map
open import SOAS.Coalgebraic.Monoid
open import SOAS.Coalgebraic.Strength
open import SOAS.Metatheory Syn

private
  variable
    α β : T
    Γ Δ : Ctx

module _ (𝔛 : Familyₛ) where
  open Theory 𝔛

  -- 𝕋 is a Σ-monoid
  Σ𝕋ᵐ : ΣMon 𝕋
  Σ𝕋ᵐ =   record
    { ᵐ = 𝕋ᵐ
    ; 𝑎𝑙𝑔 = 𝕒𝕝𝕘
    ; μ⟨𝑎𝑙𝑔⟩ = λ{ {σ = σ} t → begin
          𝕤𝕦𝕓 (𝕒𝕝𝕘 t) σ
      ≡⟨ Substitution.𝕥⟨𝕒⟩ ⟩
          𝕒𝕝𝕘 (str 𝕋ᴮ 𝕋 (⅀₁ 𝕤𝕦𝕓 t) σ)
      ≡⟨ cong 𝕒𝕝𝕘 (CoalgMon.str-eq 𝕋ᴹ 𝕋 ⅀:Str (⅀₁ 𝕤𝕦𝕓 t) σ) ⟩
          𝕒𝕝𝕘 (str (Mon.ᴮ 𝕋ᵐ) 𝕋 (⅀₁ 𝕤𝕦𝕓 t) σ)
      ∎ }
    } where open ≡-Reasoning

  -- Given a ⅀-monoid ℳ and interpretation ω : 𝔛 ⇾̣ ℳ,
  -- there is a unique homomorphic extension 𝕋 𝔛 ⇾̣ ℳ
  module FΣM {ℳ : Familyₛ}(Σℳᵐ : ΣMon ℳ) (ω : 𝔛 ⇾̣ ℳ) where
    open ΣMon Σℳᵐ renaming (𝑎𝑙𝑔 to ℳ𝑎𝑙𝑔 ; ᴮ to ℳᴮ ; ᵐ to ℳᵐ) public
    private module ℳ = ΣMon Σℳᵐ

    -- Metavariable operator of ℳ using ω and monoid multiplication, making
    -- ℳ into a meta-algebra
    χ : 𝔛 ⇾̣ 〖 ℳ , ℳ 〗
    χ 𝔪 ε = μ (ω 𝔪) ε

    ℳᵃ : MetaAlg ℳ
    ℳᵃ = record { 𝑎𝑙𝑔 = ℳ.𝑎𝑙𝑔 ; 𝑣𝑎𝑟 = η ; 𝑚𝑣𝑎𝑟 = χ }

    open Semantics ℳᵃ public renaming (𝕤𝕖𝕞 to 𝕖𝕩𝕥)
    open MetaAlg ℳᵃ
    open Coalgebraic μᶜ

    -- Extension is pointed coalgebra hommorphism
    𝕖𝕩𝕥ᵇ⇒ : Coalg⇒ 𝕋ᵇ ℳ.ᵇ 𝕖𝕩𝕥
    𝕖𝕩𝕥ᵇ⇒ = 𝕤𝕖𝕞ᵇ⇒ ℳ.ᵇ ℳᵃ record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → dext (λ ρ → begin
            μ (𝑎𝑙𝑔 t) (η ∘ ρ)
        ≡⟨ μ⟨𝑎𝑙𝑔⟩ t ⟩
            𝑎𝑙𝑔 (str ℳ.ᴮ ℳ (⅀₁ μ t) (η ∘ ρ))
        ≡⟨ cong 𝑎𝑙𝑔 (str-nat₁ (ηᴮ⇒ ℳᴮ) (⅀₁ ℳ.μ t) ρ) ⟩
            𝑎𝑙𝑔 (str ℐᴮ ℳ (⅀.F₁ (λ { h ς → h (λ v → η (ς v)) }) (⅀₁ ℳ.μ t)) ρ)
        ≡˘⟨ congr ⅀.homomorphism (λ - → 𝑎𝑙𝑔 (str ℐᴮ ℳ - ρ)) ⟩
            𝑎𝑙𝑔 (str ℐᴮ ℳ (⅀.F₁ (λ{ t ρ → μ t (η ∘ ρ)}) t) ρ)
        ∎) }
      ; ⟨𝑣𝑎𝑟⟩ = dext′ ℳ.lunit
      ; ⟨𝑚𝑣𝑎𝑟⟩ = dext′ ℳ.assoc
      } where open ≡-Reasoning

    𝕖𝕩𝕥ᴮ⇒ : Coalgₚ⇒ 𝕋ᴮ ℳ.ᴮ 𝕖𝕩𝕥
    𝕖𝕩𝕥ᴮ⇒ = record { ᵇ⇒ = 𝕖𝕩𝕥ᵇ⇒ ; ⟨η⟩ = ⟨𝕧⟩ }

    -- Extension is monoid homomorphims
    μ∘𝕖𝕩𝕥 : MapEq₁ 𝕋ᴮ ℳ.𝑎𝑙𝑔 (λ t σ → 𝕖𝕩𝕥 (𝕤𝕦𝕓 t σ))
                           (λ t σ → μ (𝕖𝕩𝕥 t) (𝕖𝕩𝕥 ∘ σ))
    μ∘𝕖𝕩𝕥 = record
      { φ = 𝕖𝕩𝕥
      ; χ = χ
      ; f⟨𝑣⟩ = cong 𝕖𝕩𝕥 Substitution.𝕥⟨𝕧⟩
      ; f⟨𝑚⟩ = trans (cong 𝕖𝕩𝕥 Substitution.𝕥⟨𝕞⟩) ⟨𝕞⟩
      ; f⟨𝑎⟩ = λ{ {σ = σ}{t} → begin
            𝕖𝕩𝕥 (𝕤𝕦𝕓 (𝕒𝕝𝕘 t) σ)
        ≡⟨ cong 𝕖𝕩𝕥 Substitution.𝕥⟨𝕒⟩ ⟩
            𝕖𝕩𝕥 (𝕒𝕝𝕘 (str 𝕋ᴮ 𝕋 (⅀₁ 𝕤𝕦𝕓 t) σ))
        ≡⟨ ⟨𝕒⟩ ⟩
            𝑎𝑙𝑔 (⅀₁ 𝕖𝕩𝕥 (str 𝕋ᴮ 𝕋 (⅀₁ 𝕤𝕦𝕓 t) σ))
        ≡˘⟨ cong 𝑎𝑙𝑔 (str-nat₂ 𝕖𝕩𝕥 (⅀₁ 𝕤𝕦𝕓 t) σ) ⟩
            𝑎𝑙𝑔 (str 𝕋ᴮ ℳ (⅀.F₁ (λ { h ς → 𝕖𝕩𝕥 (h ς) }) (⅀₁ 𝕤𝕦𝕓 t)) σ)
        ≡˘⟨ congr ⅀.homomorphism (λ - → 𝑎𝑙𝑔 (str 𝕋ᴮ ℳ - σ))  ⟩
            𝑎𝑙𝑔 (str 𝕋ᴮ ℳ (⅀₁ (λ{ t σ → 𝕖𝕩𝕥 (𝕤𝕦𝕓 t σ)}) t) σ)
        ∎ }
      ; g⟨𝑣⟩ = trans (μ≈₁ ⟨𝕧⟩) (Mon.lunit ℳ.ᵐ)
      ; g⟨𝑚⟩ = trans (μ≈₁ ⟨𝕞⟩) (Mon.assoc ℳ.ᵐ)
      ; g⟨𝑎⟩ = λ{ {σ = σ}{t} → begin
            μ (𝕖𝕩𝕥 (𝕒𝕝𝕘 t)) (𝕖𝕩𝕥 ∘ σ)
        ≡⟨ μ≈₁ ⟨𝕒⟩ ⟩
            μ (𝑎𝑙𝑔 (⅀₁ 𝕖𝕩𝕥 t)) (𝕖𝕩𝕥 ∘ σ)
        ≡⟨ μ⟨𝑎𝑙𝑔⟩ _ ⟩
            𝑎𝑙𝑔 (str ℳᴮ ℳ (⅀₁ μ (⅀₁ 𝕖𝕩𝕥 t)) (𝕖𝕩𝕥 ∘ σ))
        ≡˘⟨ congr ⅀.homomorphism (λ - → 𝑎𝑙𝑔 (str ℳᴮ ℳ - (𝕖𝕩𝕥 ∘ σ))) ⟩
            𝑎𝑙𝑔 (str ℳᴮ ℳ (⅀₁ (μ ∘ 𝕖𝕩𝕥) t) (𝕖𝕩𝕥 ∘ σ))
        ≡⟨ cong 𝑎𝑙𝑔 (str-nat₁ 𝕖𝕩𝕥ᴮ⇒ ((⅀₁ (μ ∘ 𝕖𝕩𝕥) t)) σ) ⟩
            𝑎𝑙𝑔 (str 𝕋ᴮ ℳ (⅀.F₁ (λ { h′ ς → h′ (𝕖𝕩𝕥 ∘ ς) }) (⅀₁ (μ ∘ 𝕖𝕩𝕥) t)) σ)
        ≡˘⟨ congr ⅀.homomorphism (λ - → ℳ𝑎𝑙𝑔 (str 𝕋ᴮ ℳ - σ))  ⟩
            𝑎𝑙𝑔 (str 𝕋ᴮ ℳ (⅀₁ (λ{ t σ → μ (𝕖𝕩𝕥 t) (𝕖𝕩𝕥 ∘ σ)}) t) σ)
        ∎ }
      } where open ≡-Reasoning

    𝕖𝕩𝕥ᵐ⇒ : ΣMon⇒ Σ𝕋ᵐ Σℳᵐ 𝕖𝕩𝕥
    𝕖𝕩𝕥ᵐ⇒ = record { ᵐ⇒ = record
      { ⟨η⟩ = ⟨𝕧⟩
      ; ⟨μ⟩ = λ{ {t = t} → MapEq₁.≈ μ∘𝕖𝕩𝕥 t } }
      ; ⟨𝑎𝑙𝑔⟩ = ⟨𝕒⟩ }

    module 𝕖𝕩𝕥ᵐ⇒ = ΣMon⇒ 𝕖𝕩𝕥ᵐ⇒

    -- Interpretation map is equal to any homomorphism that factors through 𝔛 ⇾ ℳ
    module _ {g : 𝕋 ⇾̣ ℳ}
             (gᵐ⇒ : ΣMon⇒ Σ𝕋ᵐ Σℳᵐ g)
             (p : ∀{α Π}{𝔪 : 𝔛 α Π} → g (𝕞𝕧𝕒𝕣 𝔪 𝕧𝕒𝕣) ≡ ω 𝔪) where
      open ΣMon⇒ gᵐ⇒ renaming (⟨𝑎𝑙𝑔⟩ to g⟨𝑎𝑙𝑔⟩)

      gᵃ⇒ : MetaAlg⇒ 𝕋ᵃ ℳᵃ g
      gᵃ⇒ = record
        { ⟨𝑎𝑙𝑔⟩ = g⟨𝑎𝑙𝑔⟩
        ; ⟨𝑣𝑎𝑟⟩ = ⟨η⟩
        ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{ε} → begin
            g (𝕞𝕧𝕒𝕣 𝔪 ε)                     ≡˘⟨ cong g (cong (𝕞𝕧𝕒𝕣 𝔪) (dext′ Substitution.𝕥⟨𝕧⟩)) ⟩
            g (𝕞𝕧𝕒𝕣 𝔪 (λ v → 𝕤𝕦𝕓 (𝕧𝕒𝕣 v) ε))  ≡˘⟨ cong g Substitution.𝕥⟨𝕞⟩ ⟩
            g (𝕤𝕦𝕓 (𝕞𝕧𝕒𝕣 𝔪 𝕧𝕒𝕣) ε)            ≡⟨ ⟨μ⟩ ⟩
            μ (g (𝕞𝕧𝕒𝕣 𝔪 𝕧𝕒𝕣)) (g ∘ ε)        ≡⟨ μ≈₁ p ⟩
            μ (ω 𝔪) (λ x → g (ε x))          ∎  }
        } where open ≡-Reasoning

      𝕖𝕩𝕥ᵐ! : {α : T}{Γ : Ctx}(t : 𝕋 α Γ) → 𝕖𝕩𝕥 t ≡ g t
      𝕖𝕩𝕥ᵐ! = 𝕤𝕖𝕞! gᵃ⇒

-- Free Σ-monoid functor
Famₛ→ΣMon :  Familyₛ → ΣMonoid
Famₛ→ΣMon 𝔛 = Theory.𝕋 𝔛 ⋉ (Σ𝕋ᵐ 𝔛)

open ΣMonoidStructure.Free

Free-ΣMon-Mapping : FreeΣMonoid.FreeMapping Famₛ→ΣMon
Free-ΣMon-Mapping = record
  { embed = λ {𝔛} 𝔪 → let open Theory 𝔛 in 𝕞𝕧𝕒𝕣 𝔪 𝕧𝕒𝕣
  ; univ = λ{ 𝔛 (ℳ ⋉ Σℳᵐ) ω → let open FΣM 𝔛 Σℳᵐ ω in record
    { extend = 𝕖𝕩𝕥 ⋉ 𝕖𝕩𝕥ᵐ⇒
    ; factor = trans ⟨𝕞⟩ (trans (μ≈₂ ⟨𝕧⟩) runit)
    ; unique = λ{ (g ⋉ gᵐ⇒) p {x = t} → sym (𝕖𝕩𝕥ᵐ! gᵐ⇒ p t) } }}
  }

Free:𝔽amₛ⟶Σ𝕄on : Functor 𝔽amiliesₛ Σ𝕄onoids
Free:𝔽amₛ⟶Σ𝕄on = FreeΣMonoid.FreeMapping.Free Free-ΣMon-Mapping

-- Σ-monoid monad on families
ΣMon:Monad : Monad 𝔽amiliesₛ
ΣMon:Monad = FreeΣMonoid.FreeMapping.FreeMonad Free-ΣMon-Mapping

𝕋F : Functor 𝔽amiliesₛ 𝔽amiliesₛ
𝕋F = Monad.F ΣMon:Monad

open Theory
open Monad ΣMon:Monad

-- Functorial action of 𝕋
𝕋₁ : {𝔛 𝔜 : Familyₛ} → (𝔛 ⇾̣ 𝔜) → 𝕋 𝔛 ⇾̣ 𝕋 𝔜
𝕋₁ f t = Functor.₁ 𝕋F f t

-- Functorial action preserves variables
𝕋₁∘𝕧𝕒𝕣 : {𝔛 𝔜 : Familyₛ}(f : 𝔛 ⇾̣ 𝔜)(v : ℐ α Γ)
       → 𝕋₁ f (𝕧𝕒𝕣 𝔛 v) ≡ 𝕧𝕒𝕣 𝔜 v
𝕋₁∘𝕧𝕒𝕣 {𝔛 = 𝔛}{𝔜} f v = FΣM.⟨𝕧⟩ 𝔛 (Σ𝕋ᵐ 𝔜) (λ 𝔪 → 𝕞𝕧𝕒𝕣 𝔜 (f 𝔪) (𝕧𝕒𝕣 𝔜))

-- Functorial action preserves metavariables
𝕋₁∘𝕞𝕧𝕒𝕣 : {𝔛 𝔜 : Familyₛ}(f : 𝔛 ⇾̣ 𝔜)(𝔪 : 𝔛 α Γ)(ε : Γ ~[ 𝕋 𝔛 ]↝ Δ)
       → 𝕋₁ f (𝕞𝕧𝕒𝕣 𝔛 𝔪 ε) ≡ 𝕞𝕧𝕒𝕣 𝔜 (f 𝔪) (𝕋₁ f ∘ ε)
𝕋₁∘𝕞𝕧𝕒𝕣 {𝔛 = 𝔛}{𝔜} f 𝔪 ε = begin
      𝕋₁ f (𝕞𝕧𝕒𝕣 𝔛 𝔪 ε)
  ≡⟨⟩
      FΣM.𝕖𝕩𝕥 𝔛 (Σ𝕋ᵐ 𝔜) (λ 𝔪 → 𝕞𝕧𝕒𝕣 𝔜 (f 𝔪) (𝕧𝕒𝕣 𝔜)) (𝕞𝕧𝕒𝕣 𝔛 𝔪 ε)
  ≡⟨ FΣM.⟨𝕞⟩ 𝔛 (Σ𝕋ᵐ 𝔜) (λ 𝔪 → 𝕞𝕧𝕒𝕣 𝔜 (f 𝔪) (𝕧𝕒𝕣 𝔜)) ⟩
      𝕤𝕦𝕓 𝔜 (𝕞𝕧𝕒𝕣 𝔜 (f 𝔪) (𝕧𝕒𝕣 𝔜)) (𝕋₁ f ∘ ε)
  ≡⟨ Substitution.𝕥⟨𝕞⟩ 𝔜 ⟩
      𝕞𝕧𝕒𝕣 𝔜 (f 𝔪) (λ 𝔫 → 𝕤𝕦𝕓 𝔜 (𝕧𝕒𝕣 𝔜 𝔫) (𝕋₁ f ∘ ε))
  ≡⟨ cong (𝕞𝕧𝕒𝕣 𝔜 (f 𝔪)) (dext (λ 𝔫 → lunit 𝔜)) ⟩
      𝕞𝕧𝕒𝕣 𝔜 (f 𝔪) (𝕋₁ f ∘ ε)
  ∎ where open ≡-Reasoning

-- Corollary fo the above two
𝕋₁∘𝕞𝕧𝕒𝕣[𝕧𝕒𝕣] : {𝔛 𝔜 : Familyₛ}(f : 𝔛 ⇾̣ 𝔜)(𝔪 : 𝔛 α Γ)(ρ : Γ ↝ Δ)
       → 𝕋₁ f (𝕞𝕧𝕒𝕣 𝔛 𝔪 (𝕧𝕒𝕣 𝔛 ∘ ρ)) ≡ 𝕞𝕧𝕒𝕣 𝔜 (f 𝔪) (𝕧𝕒𝕣 𝔜 ∘ ρ)
𝕋₁∘𝕞𝕧𝕒𝕣[𝕧𝕒𝕣] {𝔛 = 𝔛}{𝔜} f 𝔪 ρ = begin
      𝕋₁ f (𝕞𝕧𝕒𝕣 𝔛 𝔪 (𝕧𝕒𝕣 𝔛 ∘ ρ))
  ≡⟨ 𝕋₁∘𝕞𝕧𝕒𝕣 f 𝔪 (𝕧𝕒𝕣 𝔛 ∘ ρ) ⟩
      𝕞𝕧𝕒𝕣 𝔜 (f 𝔪) (𝕋₁ f ∘ 𝕧𝕒𝕣 𝔛 ∘ ρ)
  ≡⟨ cong (𝕞𝕧𝕒𝕣 𝔜 (f 𝔪)) (dext λ v → 𝕋₁∘𝕧𝕒𝕣 f (ρ v)) ⟩
      𝕞𝕧𝕒𝕣 𝔜 (f 𝔪) (𝕧𝕒𝕣 𝔜 ∘ ρ)
  ∎ where open ≡-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
{- Name: Bowornmet (Ben) Hudson

--Type safety and meaning functions for L{⇒,+,×,unit}--

-}

open import Preliminaries
open import Preorder
open import Preorder-repackage

module L where

  -- => and + and × and unit
  data Typ : Set where
    _⇒_ : Typ → Typ → Typ
    _×'_ : Typ → Typ → Typ
    _+'_ : Typ → Typ → Typ
    unit : Typ

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

  -- represent a context as a list of types
  Ctx = List Typ

  -- de Bruijn indices (for free variables)
  data _∈_ : Typ → Ctx → Set where
    i0 : ∀ {Γ τ}
       → τ ∈ (τ :: Γ)
    iS : ∀ {Γ τ τ1}
       → τ ∈ Γ
       → τ ∈ (τ1 :: Γ)

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

  -- static semantics
  data _|-_ : Ctx → Typ → Set where
    var : ∀ {Γ τ}
        → (x : τ ∈ Γ) → Γ |- τ
    lam : ∀ {Γ τ ρ}
        → (x : (ρ :: Γ) |- τ)
        → Γ |- (ρ ⇒ τ)
    app : ∀ {Γ τ1 τ2}
       → (e1 : Γ |- (τ2 ⇒ τ1)) → (e2 : Γ |- τ2)
       → Γ |- τ1
    unit : ∀ {Γ}
         → Γ |- unit
    prod : ∀ {Γ τ1 τ2}
         → (e1 : Γ |- τ1) → (e2 : Γ |- τ2)
         → Γ |- (τ1 ×' τ2)
    l-proj : ∀ {Γ τ1 τ2}
           → (e : Γ |- (τ1 ×' τ2))
           → Γ |- τ1
    r-proj : ∀ {Γ τ1 τ2}
           → (e : Γ |- (τ1 ×' τ2))
           → Γ |- τ2
    inl : ∀ {Γ τ1 τ2}
        → (e : Γ |- τ1)
        → Γ |- (τ1 +' τ2)
    inr : ∀ {Γ τ1 τ2}
        → (e : Γ |- τ2)
        → Γ |- (τ1 +' τ2)
    case` : ∀ {Γ τ1 τ2 τ}
         → (e : Γ |- (τ1 +' τ2))
         → (e1 : (τ1 :: Γ) |- τ)
         → (e2 : (τ2 :: Γ) |- τ)
         → Γ |- τ

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

  -- renaming
  rctx : Ctx → Ctx → Set
  rctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → τ ∈ Γ

  -- re: transferring variables in contexts
  lem1 : ∀ {Γ Γ' τ} → rctx Γ Γ' → rctx (τ :: Γ) (τ :: Γ')
  lem1 d i0 = i0
  lem1 d (iS x) = iS (d x)

  -- renaming lemma
  ren : ∀ {Γ Γ' τ} → Γ' |- τ → rctx Γ Γ' → Γ |- τ
  ren (var x) d = var (d x)
  ren (lam e) d = lam (ren e (lem1 d))
  ren (app e1 e2) d = app (ren e1 d) (ren e2 d)
  ren unit d = unit
  ren (prod e1 e2) d = prod (ren e1 d) (ren e2 d)
  ren (l-proj e) d = l-proj (ren e d)
  ren (r-proj e) d = r-proj (ren e d)
  ren (inl x) d = inl (ren x d)
  ren (inr x) d = inr (ren x d)
  ren (case` e e1 e2) d = case` (ren e d) (ren e1 (lem1 d)) (ren e2 (lem1 d))

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

  -- substitution
  sctx : Ctx → Ctx → Set
  sctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → Γ |- τ

  -- weakening (didn't need this later on. Oh well)
  wkn : ∀ {Γ τ1 τ2} → Γ |- τ2 → (τ1 :: Γ) |- τ2
  wkn e = ren e iS

  -- lem2 (need a lemma for subst like we did for renaming)
  lem2 : ∀ {Γ Γ' τ} → sctx Γ Γ' → sctx (τ :: Γ) (τ :: Γ')
  lem2 d i0 = var i0
  lem2 d (iS i0) = ren (d i0) iS
  lem2 d (iS (iS i)) = ren (d (iS i)) iS

  -- another substitution lemma
  lem3 : ∀ {Γ τ} → Γ |- τ → sctx Γ (τ :: Γ)
  lem3 d i0 = d
  lem3 d (iS i) = var i

  -- one final lemma needed for the last stepping rule. Thank you Professor Licata!
  lem4 : ∀ {Γ τ1 τ2} → Γ |- τ1 → Γ |- τ2 → sctx Γ (τ1 :: (τ2 :: Γ))
  lem4 x y i0 = x
  lem4 x y (iS i0) = y
  lem4 x y (iS (iS i)) = var i

  -- the 'real' substitution lemma
  subst : ∀ {Γ Γ' τ} → sctx Γ Γ' → Γ' |- τ → Γ |- τ
  subst d (var x) = d x
  subst d (lam e) = lam (subst (lem2 d) e)
  subst d (app e1 e2) = app (subst d e1) (subst d e2)
  subst d unit = unit
  subst d (prod e1 e2) = prod (subst d e1) (subst d e2)
  subst d (l-proj e) = l-proj (subst d e)
  subst d (r-proj e) = r-proj (subst d e)
  subst d (inl x) = inl (subst d x)
  subst d (inr x) = inr (subst d x)
  subst d (case` e e1 e2) = case` (subst d e) (subst (lem2 d) e1) (subst (lem2 d) e2)

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

  -- closed values of L (when something is a value)
  -- recall that we use empty contexts when we work with dynamic semantics
  data val : ∀ {τ} → [] |- τ → Set where
    unit-isval : val unit
    lam-isval : ∀ {ρ τ} (e : (ρ :: []) |- τ)
              → val (lam e)
    prod-isval : ∀ {τ1 τ2}
               → (e1 : [] |- τ1) → (e2 : [] |- τ2)
               → val e1 → val e2
               → val (prod e1 e2)
    inl-isval : ∀ {τ1 τ2}
              → (e : [] |- τ1)
              → val e
              → val (inl {_} {_} {τ2} e)
    inr-isval : ∀ {τ1 τ2}
              → (e : [] |- τ2)
              → val e
              → val (inr {_} {τ1} {_} e)

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

  -- stepping rules (preservation is folded into this)
  -- Preservation: if e:τ and e=>e', then e':τ
  data _>>_ : ∀ {τ} → [] |- τ → [] |- τ → Set where
     app-steps : ∀ {τ1 τ2}
              → (e1 e1' : [] |- (τ2 ⇒ τ1)) → (e2 : [] |- τ2)
              → e1 >> e1'
              → (app e1 e2) >> (app e1' e2)
     app-steps-2 : ∀ {τ1 τ2}
                → (e1 : [] |- (τ2 ⇒ τ1)) → (e2 e2' : [] |- τ2)
                → val e1 → e2 >> e2'
                → (app e1 e2) >> (app e1 e2')
     app-steps-3 : ∀ {τ1 τ2}
                → (e1 : (τ1 :: []) |- τ2)
                → (e2 : [] |- τ1)
                → (app (lam e1) e2) >> subst (lem3 e2) e1
     prod-steps : ∀ {τ1 τ2}
                → (e1 e1' : [] |- τ1) → (e2 : [] |- τ2)
                → e1 >> e1'
                → (prod e1 e2) >> (prod e1' e2)
     prod-steps-2 : ∀ {τ1 τ2}
                  → (e1 : [] |- τ1) → (e2 e2' : [] |- τ2)
                  → val e1 → e2 >> e2'
                  → (prod e1 e2) >> (prod e1 e2')
     l-proj-steps : ∀ {τ1 τ2}
                  → (e e' : [] |- (τ1 ×' τ2))
                  → e >> e'
                  → (l-proj e) >> (l-proj e')
     l-proj-steps-2 : ∀ {τ1 τ2}
                    → (e1 : [] |- τ1) → (e2 : [] |- τ2)
                    → val e1 → val e2
                    → (l-proj (prod e1 e2)) >> e1
     r-proj-steps : ∀ {τ1 τ2}
                  → (e e' : [] |- (τ1 ×' τ2))
                  → e >> e'
                  → (r-proj e) >> (r-proj e')
     r-proj-steps-2 : ∀ {τ1 τ2}
                    → (e1 : [] |- τ1) → (e2 : [] |- τ2)
                    → val e1 → val e2
                    → (r-proj (prod e1 e2)) >> e2
     inl-steps : ∀ {τ1 τ2}
               → (e e' : [] |- τ1)
               → e >> e'
               → inl {_} {_} {τ2} e >> inl e'
     inr-steps : ∀ {τ1 τ2}
               → (e e' : [] |- τ2)
               → e >> e'
               → inr {_} {τ1} {_} e >> inr e'
     case`-steps : ∀ {τ1 τ2 τ}
                 → (e e' : [] |- (τ1 +' τ2))
                 → (e1 : (τ1 :: []) |- τ)
                 → (e2 : (τ2 :: []) |- τ)
                 → e >> e'
                 → (case` e e1 e2) >> (case` e' e1 e2)
     case`-steps-2 : ∀ {τ1 τ2 τ}
                   → (e : [] |- τ1)
                   → (e1 : (τ1 :: []) |- τ)
                   → (e2 : (τ2 :: []) |- τ)
                   → val e
                   → (case` (inl e) e1 e2) >> subst (lem3 e) e1
     case`-steps-3 : ∀ {τ1 τ2 τ}
                   → (e : [] |- τ2)
                   → (e1 : (τ1 :: []) |- τ)
                   → (e2 : (τ2 :: []) |- τ)
                   → val e
                   → (case` (inr e) e1 e2) >> subst (lem3 e) e2

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

  -- Proof of progress!
  -- Progress: if e:τ, then either e val or ∃e' such that e=>e'
  progress : ∀ {τ} (e : [] |- τ) → Either (val e) (Σ (λ e' → (e >> e')))
  progress (var ())
  progress (lam x) = Inl (lam-isval x)
  progress (app e1 e2) with progress e1
  progress (app .(lam e) e2) | Inl (lam-isval e) = Inr (_ , app-steps-3 e e2)
  progress (app e1 e2) | Inr (x , d) = Inr (_ , app-steps e1 x e2 d)
  progress unit = Inl unit-isval
  progress (prod e1 e2) with progress e1
  progress (prod e1 e2) | Inl d with progress e2
  progress (prod e1 e2) | Inl d | Inl x = Inl (prod-isval e1 e2 d x)
  progress (prod e1 e2) | Inl d | Inr (x , k) = Inr (_ , prod-steps-2 e1 e2 x d k)
  progress (prod e1 e2) | Inr (x , d) = Inr (_ , prod-steps e1 x e2 d)
  progress (l-proj e) with progress e
  progress (l-proj .(prod e1 e2)) | Inl (prod-isval e1 e2 d d₁) = Inr (_ , l-proj-steps-2 e1 e2 d d₁)
  progress (l-proj e) | Inr (x , d) = Inr (_ , l-proj-steps e x d)
  progress (r-proj e) with progress e
  progress (r-proj .(prod e1 e2)) | Inl (prod-isval e1 e2 d d₁) = Inr (_ , r-proj-steps-2 e1 e2 d d₁)
  progress (r-proj e) | Inr (x , d) = Inr (_ , r-proj-steps e x d)
  progress (inl e) with progress e
  progress (inl e) | Inl x = Inl (inl-isval e x)
  progress (inl e) | Inr (x , d) = Inr (_ , inl-steps e x d)
  progress (inr e) with progress e
  progress (inr e) | Inl x = Inl (inr-isval e x)
  progress (inr e) | Inr (x , d) = Inr (_ , inr-steps e x d)
  progress (case` e e1 e2) with progress e
  progress (case` .(inl e) e1 e2) | Inl (inl-isval e x) = Inr (_ , case`-steps-2 e e1 e2 x)
  progress (case` .(inr e) e1 e2) | Inl (inr-isval e x) = Inr (_ , case`-steps-3 e e1 e2 x)
  progress (case` e e1 e2) | Inr (x , d) = Inr (_ , case`-steps e x e1 e2 d)

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

  -- how to interpret types in L as preorders

  interp : Typ → PREORDER
  interp (A ⇒ B) = interp A ->p interp B
  interp (A ×' B) = interp A ×p interp B
  interp (A +' B) = interp A +p interp B
  interp unit = unit-p

  interpC : Ctx → PREORDER
  interpC [] = unit-p
  interpC (A :: Γ) = interpC Γ ×p interp A

  -- look up a variable in context
  lookup : ∀{Γ τ} → τ ∈ Γ → el (interpC Γ ->p interp τ)
  lookup (i0 {Γ} {τ}) = snd' {interpC (τ :: Γ)} {interpC Γ} {_} id
  lookup (iS {Γ} {τ} {τ1} x) = comp {interpC (τ1 :: Γ)} {_} {_} (fst' {interpC (τ1 :: Γ)} {_} {interp τ1} id) (lookup x)

  interpE : ∀{Γ τ} → Γ |- τ → el (interpC Γ ->p interp τ)
  interpE (var x) = lookup x
  interpE (lam e) = lam' (interpE e)
  interpE (app e1 e2) = app' (interpE e1) (interpE e2)
  interpE unit = monotone (λ _ → <>) (λ x y _ → <>)
  interpE (prod e1 e2) = pair' (interpE e1) (interpE e2)
  interpE (l-proj {Γ} {τ1} {τ2} e) = fst' {_} {_} {interp τ2} (interpE e)
  interpE (r-proj {Γ} {τ1} {τ2} e) = snd' {_} {interp τ1} {_} (interpE e)
  interpE (inl e) = inl' (interpE e)
  interpE (inr e) = inr' (interpE e)
  interpE (case` e e1 e2) = case' (interpE e1) (interpE e2) (interpE e)

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


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

module Data.Nat where

open import Data.Nat.Base public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
open import Common.Prelude
open import Common.Reflection
open import Common.Equality
open import Agda.Builtin.Sigma

magic₁ : ⊥ → Nat
magic₁ = λ ()

magic₂ : ⊥ → Nat
magic₂ = λ { () }

magic₃ : ⊥ → Nat
magic₃ ()

data Wrap (A : Set) : Set where
  wrap : A → Wrap A

magic₄ : Wrap ⊥ → Nat
magic₄ (wrap ())

data OK : Set where
  ok : OK

bad : String
bad = "not good"

macro
  checkDefinition : (Definition → Bool) → QName → Tactic
  checkDefinition isOk f hole =
    bindTC (getDefinition f) λ def →
    give (if isOk def then quoteTerm ok else quoteTerm bad) hole

pattern `Nat  = def (quote Nat) []
pattern _`→_ a b = pi (vArg a) (abs "_" b)
pattern `Wrap a = def (quote Wrap) (vArg a ∷ [])
pattern `⊥ = def (quote ⊥) []

pattern expected₄ = funDef
  (absurdClause (("()" , vArg `⊥) ∷ []) (vArg (con (quote wrap) (vArg absurd ∷ [])) ∷ [])
  ∷ [])

check₄ : OK
check₄ = checkDefinition (λ { expected₄ → true; _ → false }) magic₄

expected = extLam (absurdClause (("()" , vArg `⊥) ∷ []) (arg (argInfo visible relevant) absurd ∷ []) ∷ []) []

macro

  quoteTermNormalised : Term → Term → TC ⊤
  quoteTermNormalised t hole =
    bindTC (normalise t) λ t →
    bindTC (quoteTC t) λ t →
    unify hole t

check₁ : quoteTermNormalised magic₁ ≡ expected
check₁ = refl

check₂ : quoteTermNormalised magic₂ ≡ expected
check₂ = refl

pattern expectedDef =
  funDef (absurdClause (("()" , vArg `⊥) ∷ []) (vArg absurd ∷ []) ∷ [])

check₃ : OK
check₃ = checkDefinition (λ { expectedDef → true; _ → false }) magic₃

max_forks_repo_name: shlevy/agda


text:
import cedille-options
open import general-util

module untyped-spans (options : cedille-options.options) {F : Set → Set} {{monadF : monad F}} where

open import lib
open import ctxt
open import cedille-types
open import spans options {F}
open import syntax-util
open import to-string options

untyped-term-spans : term → spanM ⊤
untyped-type-spans : type → spanM ⊤
untyped-kind-spans : kind → spanM ⊤
untyped-tk-spans : tk → spanM ⊤
untyped-liftingType-spans : liftingType → spanM ⊤
untyped-optTerm-spans : optTerm → spanM (posinfo → posinfo)
untyped-optType-spans : optType → spanM ⊤
untyped-optGuide-spans : optGuide → spanM ⊤
untyped-lterms-spans : lterms → spanM ⊤
untyped-optClass-spans : optClass → spanM ⊤
untyped-defTermOrType-spans : defTermOrType → spanM (spanM ⊤ → spanM ⊤)
untyped-var-spans : posinfo → var → (ctxt → posinfo → var → checking-mode → 𝕃 tagged-val → err-m → span) → spanM ⊤ → spanM ⊤

untyped-var-spans pi x f m = get-ctxt λ Γ → with-ctxt (ctxt-var-decl-loc pi x Γ) (get-ctxt λ Γ → spanM-add (f Γ pi x untyped [] nothing) ≫span m)

untyped-term-spans (App t me t') = untyped-term-spans t ≫span untyped-term-spans t' ≫span spanM-add (App-span ff t t' untyped [] nothing)
untyped-term-spans (AppTp t T) = untyped-term-spans t ≫span untyped-type-spans T ≫span spanM-add (AppTp-span t T untyped [] nothing)
untyped-term-spans (Beta pi ot ot') = untyped-optTerm-spans ot ≫=span λ f → untyped-optTerm-spans ot' ≫=span λ f' → spanM-add (Beta-span pi (f' (f (posinfo-plus pi 1))) untyped [] nothing)
untyped-term-spans (Chi pi mT t) = untyped-optType-spans mT ≫span untyped-term-spans t ≫span get-ctxt λ Γ → spanM-add (Chi-span Γ pi mT t untyped [] nothing)
untyped-term-spans (Delta pi mT t) = untyped-optType-spans mT ≫span untyped-term-spans t ≫span get-ctxt λ Γ → spanM-add (Delta-span Γ pi mT t untyped [] nothing)
untyped-term-spans (Epsilon pi lr mm t) = untyped-term-spans t ≫span spanM-add (Epsilon-span pi lr mm t untyped [] nothing)
untyped-term-spans (Hole pi) = get-ctxt λ Γ → spanM-add (hole-span Γ pi nothing [])
untyped-term-spans (IotaPair pi t t' og pi') = untyped-term-spans t ≫span untyped-term-spans t' ≫span untyped-optGuide-spans og ≫span spanM-add (IotaPair-span pi pi' untyped [] nothing)
untyped-term-spans (IotaProj t n pi) = untyped-term-spans t ≫span spanM-add (IotaProj-span t pi untyped [] nothing)
untyped-term-spans (Lam pi l pi' x oc t) = untyped-optClass-spans oc ≫span get-ctxt λ Γ → spanM-add (Lam-span Γ untyped pi l x oc t [] nothing) ≫span untyped-var-spans pi' x Var-span (untyped-term-spans t)
untyped-term-spans (Let pi d t) = untyped-defTermOrType-spans d ≫=span λ f → f (untyped-term-spans t) ≫span get-ctxt λ Γ → spanM-add (Let-span Γ untyped pi d t [] nothing)
untyped-term-spans (Open pi x t) = untyped-term-spans t ≫span spanM-add (mk-span "Open" pi (term-end-pos t) [] nothing)
untyped-term-spans (Parens pi t pi') = untyped-term-spans t
untyped-term-spans (Phi pi t t' t'' pi') = untyped-term-spans t ≫span untyped-term-spans t' ≫span untyped-term-spans t'' ≫span spanM-add (Phi-span pi pi' untyped [] nothing)
untyped-term-spans (Rho pi op on t og t') = untyped-term-spans t ≫span untyped-term-spans t' ≫span spanM-add (mk-span "Rho" pi (term-end-pos t') (ll-data-term :: [ checking-data untyped ]) nothing)
untyped-term-spans (Sigma pi t) = untyped-term-spans t ≫span get-ctxt λ Γ → spanM-add (mk-span "Sigma" pi (term-end-pos t) (ll-data-term :: [ checking-data untyped ]) nothing)
untyped-term-spans (Theta pi θ t ls) = untyped-term-spans t ≫span untyped-lterms-spans ls ≫span get-ctxt λ Γ → spanM-add (Theta-span Γ pi θ t ls untyped [] nothing)
untyped-term-spans (Var pi x) = get-ctxt λ Γ →
  spanM-add (Var-span Γ pi x untyped [] (if ctxt-binds-var Γ x then nothing else just "This variable is not currently in scope."))
untyped-term-spans (Mu pi x t ot pi' cs pi'') = spanM-add (Mu-span t [] nothing)
untyped-term-spans (Mu' pi t ot pi' cs pi'')  = spanM-add (Mu-span t [] nothing)

untyped-type-spans (Abs pi b pi' x atk T) = untyped-tk-spans atk ≫span spanM-add (TpQuant-span (me-unerased b) pi x atk T untyped [] nothing) ≫span untyped-var-spans pi' x (if tk-is-type atk then Var-span else TpVar-span) (untyped-type-spans T)
untyped-type-spans (Iota pi pi' x T T') = untyped-type-spans T ≫span spanM-add (Iota-span pi T' untyped [] nothing) ≫span untyped-var-spans pi' x TpVar-span (untyped-type-spans T')
untyped-type-spans (Lft pi pi' x t lT) = untyped-liftingType-spans lT ≫span spanM-add (Lft-span pi x t untyped [] nothing) ≫span untyped-var-spans pi' x Var-span (untyped-term-spans t)
untyped-type-spans (NoSpans T pi) = spanMok
untyped-type-spans (TpApp T T') = untyped-type-spans T ≫span untyped-type-spans T' ≫span spanM-add (TpApp-span T T' untyped [] nothing)
untyped-type-spans (TpAppt T t) = untyped-type-spans T ≫span untyped-term-spans t ≫span spanM-add (TpAppt-span T t untyped [] nothing)
untyped-type-spans (TpArrow T a T') = untyped-type-spans T ≫span untyped-type-spans T' ≫span spanM-add (TpArrow-span T T' untyped [] nothing)
untyped-type-spans (TpEq pi t t' pi') = untyped-term-spans t ≫span untyped-term-spans t' ≫span spanM-add (TpEq-span pi t t' pi' untyped [] nothing)
untyped-type-spans (TpHole pi) = get-ctxt λ Γ → spanM-add (tp-hole-span Γ pi nothing [])
untyped-type-spans (TpLambda pi pi' x atk T) = untyped-tk-spans atk ≫span spanM-add (TpLambda-span pi pi' atk T untyped [] nothing) ≫span untyped-var-spans pi' x TpVar-span (untyped-type-spans T)
untyped-type-spans (TpParens pi T pi') = untyped-type-spans T
untyped-type-spans (TpVar pi x) = get-ctxt λ Γ →
  spanM-add (TpVar-span Γ pi x untyped [] (if ctxt-binds-var Γ x then nothing else just "This variable is not currently in scope."))
untyped-type-spans (TpLet pi d T) = untyped-defTermOrType-spans d ≫=span λ f → f (untyped-type-spans T) ≫span get-ctxt λ Γ → spanM-add (TpLet-span Γ untyped pi d T [] nothing)

untyped-kind-spans (KndArrow k k') = untyped-kind-spans k ≫span untyped-kind-spans k' ≫span spanM-add (KndArrow-span k k' untyped nothing)
untyped-kind-spans (KndParens pi k pi') = untyped-kind-spans k
untyped-kind-spans (KndPi pi pi' x atk k) = untyped-tk-spans atk ≫span spanM-add (KndPi-span pi x atk k untyped nothing) ≫span untyped-var-spans pi' x (if tk-is-type atk then Var-span else TpVar-span) (untyped-kind-spans k)
untyped-kind-spans (KndTpArrow T k) = untyped-type-spans T ≫span untyped-kind-spans k ≫span spanM-add (KndTpArrow-span T k untyped nothing)
untyped-kind-spans (KndVar pi x as) = get-ctxt λ Γ →
  spanM-add (KndVar-span Γ (pi , x) (kvar-end-pos pi x as) ParamsNil untyped [] (if ctxt-binds-var Γ x then nothing else just "This variable is not currently in scope."))
untyped-kind-spans (Star pi) = spanM-add (Star-span pi untyped nothing)

untyped-liftingType-spans lT = spanMok -- Unimplemented

untyped-tk-spans (Tkt T) = untyped-type-spans T
untyped-tk-spans (Tkk k) = untyped-kind-spans k

untyped-optTerm-spans NoTerm = spanMr λ pi → pi
untyped-optTerm-spans (SomeTerm t pi) = untyped-term-spans t ≫span spanMr λ _ → pi

untyped-optType-spans NoType = spanMok
untyped-optType-spans (SomeType T) = untyped-type-spans T

untyped-optGuide-spans NoGuide = spanMok
untyped-optGuide-spans (Guide pi x T) = untyped-var-spans pi x Var-span (untyped-type-spans T)

untyped-lterms-spans (LtermsNil pi) = spanMok
untyped-lterms-spans (LtermsCons me t ls) = untyped-term-spans t ≫span untyped-lterms-spans ls

untyped-optClass-spans NoClass = spanMok
untyped-optClass-spans (SomeClass atk) = untyped-tk-spans atk

untyped-defTermOrType-spans (DefTerm pi x NoType t) = untyped-term-spans t ≫span get-ctxt λ Γ → with-ctxt (ctxt-var-decl-loc pi x Γ) (spanMr λ x → x)
untyped-defTermOrType-spans (DefTerm pi x (SomeType T) t) = untyped-term-spans t ≫span untyped-type-spans T ≫span get-ctxt λ Γ → with-ctxt (ctxt-var-decl-loc pi x Γ) (spanMr λ x → x)
untyped-defTermOrType-spans (DefType pi x k T) = untyped-kind-spans k ≫span untyped-type-spans T ≫span get-ctxt λ Γ → with-ctxt (ctxt-var-decl-loc pi x Γ) (spanMr λ x → x)

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
data unit : Set where tt : unit

record Y (A : Set) : Set where field y : A
record Z (A : Set) : Set where field z : A

instance
  -- Y[unit] : Y unit
  -- Y.y Y[unit] = tt
  Z[unit] : Z unit
  Z.z Z[unit] = tt

foo : ∀ (A : Set) {{YA : Y A}} {{ZA : Z A}} → unit
foo A = tt

foo[unit] : unit
foo[unit] = foo unit -- {{ZA = Z[unit]}}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module L.Base.Empty where

-- Reexport definitions
open import L.Base.Empty.Core public

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


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

open import lib.Base
open import lib.Equivalence
open import lib.PathGroupoid
open import lib.NType
open import lib.Univalence
open import lib.path-seq.Concat
open import lib.path-seq.Split

module lib.path-seq.Reasoning where

infix 30 _=↯=_
_=↯=_ : ∀ {i} {A : Type i} {a a' : A} → a =-= a' → a =-= a' → Type i
_=↯=_ s t = (↯ s) == (↯ t)

module _ {i} {A : Type i} {a a' : A} where

  =-=ₛ-equiv : (s t : a =-= a') → (s =↯= t) ≃ (s =ₛ t)
  =-=ₛ-equiv s t = equiv =ₛ-in =ₛ-out (λ _ → idp) (λ _ → idp)

  =ₛ-level : {s t : a =-= a'} {n : ℕ₋₂}
    → has-level (S (S n)) A → has-level n (s =ₛ t)
  =ₛ-level {s} {t} {n} A-level =
    transport (has-level n) (ua (=-=ₛ-equiv s t)) $
    has-level-apply (has-level-apply A-level _ _) _ _

  !ₛ : {s t : a =-= a'} → s =ₛ t → t =ₛ s
  !ₛ (=ₛ-in p) = =ₛ-in (! p)

  _∙ₛ_ : {s t u : a =-= a'} → s =ₛ t → t =ₛ u → s =ₛ u
  _∙ₛ_ (=ₛ-in p) (=ₛ-in q) = =ₛ-in (p ∙ q)

  expand : (s : a =-= a') → ↯ s ◃∎ =ₛ s
  expand s = =ₛ-in idp

  contract : {s : a =-= a'} → s =ₛ ↯ s ◃∎
  contract = =ₛ-in idp

  abstract
    private
      infixr 10 _=↯=⟨_&_&_&_⟩_
      _=↯=⟨_&_&_&_⟩_ : {q : a == a'}
        → (s : a =-= a')
        → (n : ℕ) (m : ℕ)
        → (t : point-from-start n s =-= point-from-start m (drop n s))
        → take m (drop n s) =↯= t
        → ↯ (take n s ∙∙ t ∙∙ drop m (drop n s)) == q
        → ↯ s == q
      _=↯=⟨_&_&_&_⟩_ {q} s n m t p p' =
        ↯ s
          =⟨ =ₛ-out (take-drop-split n s) ⟩
        ↯ (take n s) ∙ ↯ (drop n s)
          =⟨ ap (↯ (take n s) ∙_) (=ₛ-out (take-drop-split m (drop n s))) ⟩
        ↯ (take n s) ∙ ↯ (take m (drop n s)) ∙ ↯ (drop m (drop n s))
          =⟨ ap (λ v → ↯ (take n s) ∙ v ∙ ↯ (drop m (drop n s))) p ⟩
        ↯ (take n s) ∙ ↯ t ∙ ↯ (drop m (drop n s))
          =⟨ ap (λ v → ↯ (take n s) ∙ v) (! (↯-∙∙ t (drop m (drop n s)))) ⟩
        ↯ (take n s) ∙ ↯ (t ∙∙ drop m (drop n s))
          =⟨ ! (↯-∙∙ (take n s) (t ∙∙ drop m (drop n s))) ⟩
        ↯ (take n s ∙∙ t ∙∙ drop m (drop n s))
          =⟨ p' ⟩
        q =∎

    {- For making proofs more readable by making
       definitional equalities visible. Example:

      p ◃∙ ap f idp ◃∙ q ◃∎
        =ₛ⟨id⟩
      p ◃∙ idp ◃∙ q ◃∎ ∎ₛ

    -}
    infixr 10 _=ₛ⟨id⟩_
    _=ₛ⟨id⟩_ : (s : a =-= a') {u : a =-= a'}
      → s =ₛ u
      → s =ₛ u
    _=ₛ⟨id⟩_ s e = e

    {- For rewriting everything using a [_=ₛ_] path. Example:

      ap f p ◃∙ h y ◃∎
        =ₛ⟨ homotopy-naturality f g h p ⟩
      h x ◃∙ ap g p ◃∎ ∎ₛ

    -}
    infixr 10 _=ₛ⟨_⟩_
    _=ₛ⟨_⟩_ : (s : a =-= a') {t u : a =-= a'}
      → s =ₛ t
      → t =ₛ u
      → s =ₛ u
    _=ₛ⟨_⟩_ _ p q = p ∙ₛ q

    {- For rewriting a segment using a [_=ₛ_] path. Example:

      p ◃∙ ! (q ∙ r) ◃∙ s ◃∎
        =ₛ⟨ 1 & 1 & !-∙-seq (q ◃∙ r ◃∎) ⟩
      p ◃∙ ! r ◃∙ ! q ◃∙ s ◃∎ ∎ₛ

    -}
    infixr 10 _=ₛ⟨_&_&_⟩_
    _=ₛ⟨_&_&_⟩_ : (s : a =-= a') {u : a =-= a'}
      → (m n : ℕ)
      → {r : point-from-start m s =-= point-from-start n (drop m s)}
      → take n (drop m s) =ₛ r
      → take m s ∙∙ r ∙∙ drop n (drop m s) =ₛ u
      → s =ₛ u
    _=ₛ⟨_&_&_⟩_ s m n {r} p p' = =ₛ-in (s =↯=⟨ m & n & r & =ₛ-out p ⟩ =ₛ-out p')

    {- For rewriting everything using a [_==_] path. Example:

      p ◃∙ idp ◃∎
        =ₛ₁⟨ ∙-unit-r p ⟩
      p ◃∎ ∎ₛ

    -}
    infixr 10 _=ₛ₁⟨_⟩_
    _=ₛ₁⟨_⟩_ : (s : a =-= a') {u : a =-= a'}
      → {r : a == a'}
      → ↯ s == r
      → r ◃∎ =ₛ u
      → s =ₛ u
    _=ₛ₁⟨_⟩_ s {r} p p' = =ₛ-in p ∙ₛ p'

    {- For rewriting a segment using a [_==_] path. Example:

      p ◃∙ ! (ap f q) ◃∙ r ◃∎
        =ₛ₁⟨ 1 & 1 & !-ap f q ⟩
      p ◃∙ ap f (! q) ◃∙ r ◃∎ ∎ₛ

    -}
    infixr 10 _=ₛ₁⟨_&_&_⟩_
    _=ₛ₁⟨_&_&_⟩_ : (s : a =-= a') {u : a =-= a'}
      → (m n : ℕ)
      → {r : point-from-start m s == point-from-start n (drop m s)}
      → ↯ (take n (drop m s)) == r
      → take m s ∙∙ r ◃∙ drop n (drop m s) =ₛ u
      → s =ₛ u
    _=ₛ₁⟨_&_&_⟩_ s m n {r} p p' = s =ₛ⟨ m & n & =ₛ-in {t = r ◃∎} p ⟩ p'

  infix 15 _∎ₛ
  _∎ₛ : (s : a =-= a') → s =ₛ s
  _∎ₛ _ = =ₛ-in idp

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda