text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module Quicksort.Correctness.Order {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_)  where

open import Data.List
open import Function using (_∘_)
open import List.Sorted _≤_
open import Quicksort _≤_ tot≤
open import SBList _≤_
open import Size
open import SOList.Total _≤_
open import SOList.Total.Properties _≤_ trans≤

theorem-quickSort-sorted : (xs : List A) → Sorted (forget (quickSort (bound xs)))
theorem-quickSort-sorted = lemma-solist-sorted ∘ quickSort ∘ bound

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------
-- Adjunctions and monads (for 1-categories)
------------------------------------------------------------------------

-- The code is based on the presentation in the HoTT book (but might
-- not follow it exactly).

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

open import Equality

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

open import Prelude hiding (id)

open import Category eq
open Derived-definitions-and-properties eq
open import Functor eq

------------------------------------------------------------------------
-- Adjunctions

private

  -- Is-left-adjoint-of ext F G means that F is a left adjoint of G.
  -- This definition tries to follow the HoTT book closely.

  Is-left-adjoint-of :
    ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
      {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄} →
    Extensionality (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) →
    C ⇨ D → D ⇨ C → Type _
  Is-left-adjoint-of {ℓ₁} {ℓ₂} {C} {ℓ₃} {ℓ₄} {D} ext F G =
    ∃ λ (η : id⇨ ⇾ G ∙⇨ F) →
    ∃ λ (ε : F ∙⇨ G ⇾ id⇨) →
    subst ((F ∙⇨ G) ∙⇨ F ⇾_) (id⇨∙⇨ ext₁) (ε ⇾∙⇨ F) ∙⇾
      subst (_⇾ (F ∙⇨ G) ∙⇨ F) (∙⇨id⇨ ext₁)
        (subst (F ∙⇨ id⇨ ⇾_) (∙⇨-assoc ext₁ F G) (F ⇨∙⇾ η))
      ≡
    id⇾ F
      ×
    subst (G ∙⇨ F ∙⇨ G ⇾_) (∙⇨id⇨ ext₂) (G ⇨∙⇾ ε) ∙⇾
      subst (_⇾ G ∙⇨ F ∙⇨ G) (id⇨∙⇨ ext₂)
        (subst (id⇨ ∙⇨ G ⇾_) (sym $ ∙⇨-assoc ext₂ G F) (η ⇾∙⇨ G))
      ≡
    id⇾ G
    where
    ext₁ : Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄)
    ext₁ = lower-extensionality (ℓ₃ ⊔ ℓ₄) ℓ₃ ext

    ext₂ : Extensionality (ℓ₃ ⊔ ℓ₄) (ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
    ext₂ = lower-extensionality (ℓ₁ ⊔ ℓ₂) ℓ₁ ext

-- F ⊣ G means that F is a left adjoint of G.
--
-- This definition avoids the use of subst in the previous definition
-- by making use of the equality characterisation for natural
-- transformations (equality-characterisation⇾). I (NAD) took the idea
-- for this definition from the HoTT-Agda library
-- (https://github.com/HoTT/HoTT-Agda/blob/2871c6f6dbe90b47b3b2770e57abc4732cd1c295/theorems/homotopy/PtdAdjoint.agda).
--
-- TODO: Prove that the two definitions are equivalent.

_⊣_ :
  ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
    {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄} →
  C ⇨ D → D ⇨ C → Type _
_⊣_ {ℓ₁} {ℓ₂} {C} {ℓ₃} {ℓ₄} {D} F G =
  ∃ λ (η : id⇨ ⇾ G ∙⇨ F) →
  ∃ λ (ε : F ∙⇨ G ⇾ id⇨) →
  (∀ {X} → transformation ε D.∙ (F ⊙ transformation η {X = X}) ≡ D.id)
    ×
  (∀ {X} → (G ⊙ transformation ε {X = X}) C.∙ transformation η ≡ C.id)
  where
  open _⇾_
  module C = Precategory C
  module D = Precategory D

-- Adjunctions.

Adjunction :
  ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
  Precategory ℓ₁ ℓ₂ → Precategory ℓ₃ ℓ₄ → Type _
Adjunction C D = ∃ λ (F : C ⇨ D) → ∃ λ (G : D ⇨ C) → F ⊣ G

------------------------------------------------------------------------
-- Monads

-- A monad on a precategory.
--
-- This definition is taken from Wikipedia
-- (https://en.wikipedia.org/wiki/Monad_%28category_theory%29).

Monad : ∀ {ℓ₁ ℓ₂} (C : Precategory ℓ₁ ℓ₂) → Type (ℓ₁ ⊔ ℓ₂)
Monad C =
  ∃ λ (F : C ⇨ C) →
  ∃ λ (η : id⇨ ⇾ F) →
  ∃ λ (μ : F ∙⇨ F ⇾ F) →
  (∀ {X} → transformation μ ∙ (F ⊙ transformation μ {X = X})
             ≡
           transformation μ ∙ transformation μ {X = F ⊚ X})
    ×
  (∀ {X} → transformation μ ∙ (F ⊙ transformation η {X = X}) ≡ id)
    ×
  (∀ {X} → transformation μ ∙ transformation η {X = F ⊚ X} ≡ id)
  where
  open _⇾_
  open Precategory C

-- Adjunctions give rise to monads.
--
-- This definition is taken from Wikipedia
-- (https://en.wikipedia.org/wiki/Monad_%28category_theory%29).

adjunction→monad :
  ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
    {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄} →
  Adjunction C D → Monad C
adjunction→monad {C = C} {D = D} (F , G , η , ε , εFFη≡1 , GεηG≡1) =
    G ∙⇨ F
  , η
  , GεF
  , lemma₁
  , lemma₂
  , lemma₃
  where
  open _⇾_
  module C = Precategory C
  module D = Precategory D

  -- This natural transformation is defined directly, rather than by
  -- using composition, to avoid the use of casts.

  GεF : (G ∙⇨ F) ∙⇨ (G ∙⇨ F) ⇾ G ∙⇨ F
  natural-transformation GεF =
      G ⊙ transformation ε
    , nat
    where
    abstract
      nat :
        ∀ {X Y} {f : C.Hom X Y} →
        ((G ∙⇨ F) ⊙ f) C.∙ (G ⊙ transformation ε) ≡
        (G ⊙ transformation ε) C.∙ (((G ∙⇨ F) ∙⇨ (G ∙⇨ F)) ⊙ f)
      nat {f = f} =
        ((G ∙⇨ F) ⊙ f) C.∙ (G ⊙ transformation ε)                ≡⟨⟩
        (G ⊙ F ⊙ f) C.∙ (G ⊙ transformation ε)                   ≡⟨ sym (⊙-∙ G) ⟩
        G ⊙ ((F ⊙ f) D.∙ transformation ε)                       ≡⟨ cong (G ⊙_) (natural ε) ⟩
        G ⊙ (transformation ε D.∙ (F ⊙ G ⊙ F ⊙ f))               ≡⟨ ⊙-∙ G ⟩
        (G ⊙ transformation ε) C.∙ (G ⊙ F ⊙ G ⊙ F ⊙ f)           ≡⟨⟩
        (G ⊙ transformation ε) C.∙ (((G ∙⇨ F) ∙⇨ (G ∙⇨ F)) ⊙ f)  ∎

  abstract

    lemma₁ :
      ∀ {X} →
      transformation GεF {X = X} C.∙ ((G ∙⇨ F) ⊙ transformation GεF) ≡
      transformation GεF C.∙ transformation GεF
    lemma₁ =
      (G ⊙ transformation ε) C.∙ (G ⊙ F ⊙ G ⊙ transformation ε)  ≡⟨ sym (⊙-∙ G) ⟩
      G ⊙ (transformation ε D.∙ (F ⊙ G ⊙ transformation ε))      ≡⟨ cong (G ⊙_) (sym $ natural ε) ⟩
      G ⊙ (transformation ε D.∙ transformation ε)                ≡⟨ ⊙-∙ G ⟩∎
      (G ⊙ transformation ε) C.∙ (G ⊙ transformation ε)          ∎

    lemma₂ :
      ∀ {X} →
      transformation GεF {X = X} C.∙ ((G ∙⇨ F) ⊙ transformation η) ≡
      C.id
    lemma₂ =
      (G ⊙ transformation ε) C.∙ (G ⊙ F ⊙ transformation η)  ≡⟨ sym (⊙-∙ G) ⟩
      G ⊙ (transformation ε D.∙ (F ⊙ transformation η))      ≡⟨ cong (G ⊙_) εFFη≡1 ⟩
      G ⊙ D.id                                               ≡⟨ ⊙-id G ⟩∎
      C.id                                                   ∎

    lemma₃ :
      ∀ {X} →
      transformation GεF {X = X} C.∙ transformation η ≡ C.id
    lemma₃ =
      (G ⊙ transformation ε) C.∙ transformation η  ≡⟨ GεηG≡1 ⟩∎
      C.id                                         ∎

ext: agda

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Common.Equality

data Bool : Set where
  true false : Bool

data IsTrue : Bool → Set where
  itis : IsTrue true

module M (u : Bool) where
  foo bar : (p : IsTrue u) → Bool
  foo = \ { itis → true  }
  bar = \ { itis → false }

test : ∀ u → M.foo u ≡ M.bar u
test u = refl

-- Trigger printing of the extended lambdas.

-- Ideally, this would not show the internal names, like in
--
--   .Issue2047a.M..extendedlambda0 u p !=
--   .Issue2047a.M..extendedlambda1 u p of type Bool
--   when checking that the expression refl has type M.foo u ≡ M.bar u
--
-- but rather show
--
--   (\ { itis → true  }) .p != (\ { itis → false }) .p

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module MultipleFixityDecl where

infixl 40 _+_
infixr 60 _+_

_+_ : Set -> Set -> Set
A + B = A


text:
module Tactic.Reflection.Meta where

open import Prelude
open import Builtin.Reflection
open import Tactic.Reflection.DeBruijn

ensureNoMetas : Term → TC ⊤

noMetaArg : Arg Term → TC ⊤
noMetaArg (arg _ v) = ensureNoMetas v

noMetaArgs : List (Arg Term) → TC ⊤
noMetaArgs [] = pure _
noMetaArgs (v ∷ vs) = noMetaArg v *> noMetaArgs vs

noMetaClause : Clause → TC ⊤
noMetaClause (clause ps t) = ensureNoMetas t
noMetaClause (absurd-clause ps) = pure _

noMetaClauses : List Clause → TC ⊤
noMetaClauses [] = pure _
noMetaClauses (c ∷ cs) = noMetaClause c *> noMetaClauses cs

noMetaAbs : Abs Term → TC ⊤
noMetaAbs (abs _ v) = ensureNoMetas v

noMetaSort : Sort → TC ⊤
noMetaSort (set t) = ensureNoMetas t
noMetaSort (lit n) = pure _
noMetaSort unknown = pure _

ensureNoMetas (var x args) = noMetaArgs args
ensureNoMetas (con c args) = noMetaArgs args
ensureNoMetas (def f args) = noMetaArgs args
ensureNoMetas (lam v (abs _ t)) = ensureNoMetas t
ensureNoMetas (pat-lam cs args) = noMetaClauses cs *> noMetaArgs args
ensureNoMetas (pi a b) = noMetaArg a *> noMetaAbs b
ensureNoMetas (agda-sort s) = noMetaSort s
ensureNoMetas (lit l) = pure _
ensureNoMetas (meta x x₁) = blockOnMeta x
ensureNoMetas unknown = pure _

normaliseNoMetas : Term → TC Term
normaliseNoMetas a = do a ← normalise a
                        stripBoundNames a <$ ensureNoMetas a

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
--------------------------------------------------------------------------------
-- This file provides the generateCFG function that turns a list of strings of
-- the current syntax for grammars into a grammar as defined in Parser.agda
--------------------------------------------------------------------------------

{-# OPTIONS --type-in-type #-}

module Parse.Generate where

open import Class.Monad.Except
open import Data.Fin.Map
import Data.List.NonEmpty as NE
open NE using (List⁺; _∷_)
open import Data.String using (toList; fromChar; uncons) renaming (fromList to fromListS)
open import Data.Vec using (Vec; lookup; fromList; []; _∷_; _[_]%=_)
open import Data.Vec.Exts

open import Parse.LL1
open import Parse.MarkedString
open import Parse.MultiChar
open import Parse.Escape

open import Prelude
open import Prelude.Strings

-- Grammar with show functions for rules and non-terminals
Grammar = ∃[ n ]
  Σ[ G ∈ CFG (Fin (suc n)) MultiChar ] (CFG.Rule G → String) × (Fin (suc n) → String)

NonTerminal : Grammar → Set
NonTerminal (n , _) = Fin (suc n)

initNT : (G : Grammar) → NonTerminal G
initNT (_ , G , _) = CFG.S G

findNT : (G : Grammar) → String → Maybe (NonTerminal G)
findNT (n , _ , _ , showNT) NT = findIndex (NT ≟_) (Data.Vec.tabulate showNT)

checkRuleName : String → String × List MarkedString → Set
checkRuleName s r = s ≡ proj₁ r

checkRuleNameDec : ∀ s → Decidable (checkRuleName s)
checkRuleNameDec s (s' , _) = s ≟ s'

module _ {M} {{_ : Monad M}} {{_ : MonadExcept M String}} where

  -- Read until the closing marker
  bracketHelper : Marker → MarkedString → M (List⁺ String × MarkedString)
  bracketHelper m [] = throwError "Unexpected end of string! Expected a marker!"
  bracketHelper m (inj₁ x ∷ s) = do
    (head ∷ tail , rest) ← bracketHelper m s
    return (fromChar x + head ∷ tail , rest)
  bracketHelper m (inj₂ x ∷ s) =
    if x ≣ m
      then return (NE.[ "" ] , s)
      else
        if x ≣ WildcardSeparator
          then if (m ≣ WildcardBracket true) ∨ (m ≣ WildcardBracket false)
            then (do
              (res , rest) ← bracketHelper m s
              return ("" NE.∷⁺ res , rest))
            else throwError "Found a wildcard separator outside of a wildcard bracket!"
          else throwError "Found unexpected marker!"

  preParseCFG : List MarkedString → M (∃[ n ] Vec (String × List MarkedString) n)
  preParseCFG [] = return $ zero , []
  preParseCFG (x ∷ l) with break (_≟ inj₂ NameDivider) x
  ... | name , rule' = if null name
    then throwError $ "Parsing rule has no/empty name! Rule: " + markedStringToString x
    else do
      _ , rules ← preParseCFG l
      let rule = dropHeadIfAny rule'
      return $ case findIndex (checkRuleNameDec $ markedStringToString name) rules of λ
        { (just x) → -, rules [ x ]%= map₂ (rule ∷_)
        ; nothing → -, (markedStringToString name , [ rule ]) ∷ rules}

  {-# TERMINATING #-}
  generateCFG' : ∀ {n} → String → Vec (String × List MarkedString) (suc n) → M Grammar
  generateCFG' {n} start rules = do
    ruleTable ← parseRuleTable
    case findIndex (checkRuleNameDec start) rules of λ where
      (just i) →
        return $
          (-, record
            { S = i
            ; R = Fin ∘ numOfRules
            ; AllRules = allFin ∘ numOfRules
            ; Rstring'' = λ {v} → ruleTable v }
          , (λ where (NT , rule) → let (NT' , rules') = lookup rules NT
                                   in NT' + "$" + markedStringToString (lookup (fromList rules') rule))
          , proj₁ ∘ lookup rules)
      nothing → throwError $ "No non-terminal named " + start + " found!"
    where
      numOfRules : Fin (suc n) → ℕ
      numOfRules = length ∘ proj₂ ∘ lookup rules

      RuleTable : Set → Set
      RuleTable T = DepFinMap (suc n) (λ v → FinMap (numOfRules v) T)

      RuleString : Set
      RuleString = List ((Fin (suc n) × Bool) ⊎ MultiChar ⊎ String)

      sequenceRuleTable : ∀ {A} → RuleTable (M A) → M (RuleTable A)
      sequenceRuleTable f = sequenceDepFinMap (sequenceDepFinMap ∘ f)

      addCharToRuleString : Char → RuleString → RuleString
      addCharToRuleString c [] = [ inj₂ (inj₂ $ fromChar c) ]
      addCharToRuleString c s@(inj₁ _ ∷ _) = inj₂ (inj₂ $ fromChar c) ∷ s
      addCharToRuleString c s@(inj₂ (inj₁ _) ∷ _) = inj₂ (inj₂ $ fromChar c) ∷ s
      addCharToRuleString c (inj₂ (inj₂ y) ∷ s) = inj₂ (inj₂ (fromChar c + y)) ∷ s

      markedStringToRule : MarkedString → M RuleString
      markedStringToRule [] = return []
      markedStringToRule (inj₁ x ∷ s) = do
        res ← markedStringToRule s
        return (addCharToRuleString x res)
      -- this terminates because 'rest' is shorter than 's'
      markedStringToRule (inj₂ (NonTerminalBracket b) ∷ s) = do
        (nonTerm ∷ _ , rest) ← bracketHelper (NonTerminalBracket b) s
        res ← markedStringToRule rest
        nonTerm' ← maybeToError
          (findIndex (checkRuleNameDec nonTerm) rules)
          ("Couldn't find a non-terminal named '" + nonTerm + "'")
        return (inj₁ (nonTerm' , b) ∷ res)
      markedStringToRule (inj₂ NameDivider ∷ s) =
        throwError "The rule cannot contain a name divider!"
      markedStringToRule (inj₂ (WildcardBracket b) ∷ s) = do
        (multiChar , rest) ← bracketHelper (WildcardBracket b) s
        inj₂ (inj₁ $ parseMultiCharNE b multiChar) ∷_ <$> markedStringToRule rest
      markedStringToRule (inj₂ WildcardSeparator ∷ s) =
        throwError "Wildcard separator outside of a wildcard!"

      parseRuleTable : M (RuleTable RuleString)
      parseRuleTable = sequenceRuleTable
        λ v x → let y = lookup (fromList $ proj₂ (lookup rules v)) x in
          appendIfError (markedStringToRule y) (" In: " + show y)

  -- The first parameter describes the non-terminal the grammar should start with
  generateCFGNonEscaped : String → List String → M Grammar
  generateCFGNonEscaped start l = do
    (suc k , y) ← preParseCFG $ map convertToMarked l
      where _ → throwError "The grammar is empty!"
    generateCFG' start y

  -- The first parameter describes the non-terminal the grammar should start with
  generateCFG : String → List String → M Grammar
  generateCFG start l =
    maybe (generateCFGNonEscaped start)
      (throwError "Error while un-escaping parsing rules!")
      (sequence $ ((_<$>_ fromListS) ∘ translate ∘ toList) <$> l)

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
-- 2010-10-05 Andreas

module TerminationRecordPatternLie where

data Empty : Set where

record Unit : Set where

data Bool : Set where
  true false : Bool

T : Bool -> Set
T true = Unit
T false = Empty

-- Thorsten suggests on the Agda list  thread "Coinductive families"
-- to encode lists as records
record List (A : Set) : Set where
  inductive
  constructor list
  field
    isCons : Bool
    head   : T isCons -> A
    tail   : T isCons -> List A

open List public

-- However, we have to be careful to preserve termination
-- in the presence of a lie

postulate
  lie : {b : Bool} -> T b

-- this function is rejected
f : {A : Set} -> List A -> Empty
f (list b h t) = f (t lie)

-- since its internal representation is
g : {A : Set} -> List A -> Empty
g l = g (tail l lie)

-- however could record constructors still count as structural increase
-- if they cannot be translated away
-- should we accept this?
--   f (list true h t) = f (t _)

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic products of binary relations
------------------------------------------------------------------------

-- The definition of lexicographic product used here is suitable if
-- the left-hand relation is a (non-strict) partial order.

module Relation.Binary.Product.NonStrictLex where

open import Data.Product
open import Data.Sum
open import Level
open import Relation.Binary
open import Relation.Binary.Consequences
import Relation.Binary.NonStrictToStrict as Conv
open import Relation.Binary.Product.Pointwise as Pointwise
  using (_×-Rel_)
import Relation.Binary.Product.StrictLex as Strict

module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where

  ×-Lex : (_≈₁_ _≤₁_ : Rel A₁ ℓ₁) → (_≤₂_ : Rel A₂ ℓ₂) →
          Rel (A₁ × A₂) _
  ×-Lex _≈₁_ _≤₁_ _≤₂_ = Strict.×-Lex _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_

  -- Some properties which are preserved by ×-Lex (under certain
  -- assumptions).

  ×-reflexive : ∀ _≈₁_ _≤₁_ {_≈₂_} _≤₂_ →
                _≈₂_ ⇒ _≤₂_ → (_≈₁_ ×-Rel _≈₂_) ⇒ (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-reflexive _≈₁_ _≤₁_ _≤₂_ refl₂ {x} {y} =
    Strict.×-reflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_ refl₂ {x} {y}

  ×-transitive : ∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
                 ∀ {_≤₂_} → Transitive _≤₂_ →
                 Transitive (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-transitive {_≈₁_ = _≈₁_} {_≤₁_ = _≤₁_} po₁ {_≤₂_ = _≤₂_} trans₂
               {x} {y} {z} =
    Strict.×-transitive
      {_<₁_ = Conv._<_ _≈₁_ _≤₁_}
      isEquivalence (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
      (Conv.trans _ _ po₁)
      {_≤₂_ = _≤₂_} trans₂ {x} {y} {z}
    where open IsPartialOrder po₁

  ×-antisymmetric :
    ∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
    ∀ {_≈₂_ _≤₂_} → Antisymmetric _≈₂_ _≤₂_ →
    Antisymmetric (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-antisymmetric {_≈₁_ = _≈₁_} {_≤₁_ = _≤₁_}
                  po₁ {_≤₂_ = _≤₂_} antisym₂ {x} {y} =
    Strict.×-antisymmetric {_<₁_ = Conv._<_ _≈₁_ _≤₁_}
                           ≈-sym₁ irrefl₁ asym₁
                           {_≤₂_ = _≤₂_} antisym₂ {x} {y}
    where
    open IsPartialOrder po₁
    open Eq renaming (refl to ≈-refl₁; sym to ≈-sym₁)

    irrefl₁ : Irreflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_)
    irrefl₁ = Conv.irrefl _≈₁_ _≤₁_

    asym₁ : Asymmetric (Conv._<_ _≈₁_ _≤₁_)
    asym₁ = trans∧irr⟶asym {_≈_ = _≈₁_}
                           ≈-refl₁ (Conv.trans _ _ po₁) irrefl₁

  ×-≈-respects₂ :
    ∀ {_≈₁_ _≤₁_} → IsEquivalence _≈₁_ → _≤₁_ Respects₂ _≈₁_ →
    ∀ {_≈₂_ _≤₂_ : Rel A₂ ℓ₂} → _≤₂_ Respects₂ _≈₂_ →
    (×-Lex _≈₁_ _≤₁_ _≤₂_) Respects₂ (_≈₁_ ×-Rel _≈₂_)
  ×-≈-respects₂ eq₁ resp₁ resp₂ =
    Strict.×-≈-respects₂ eq₁ (Conv.<-resp-≈ _ _ eq₁ resp₁) resp₂

  ×-decidable : ∀ {_≈₁_ _≤₁_} → Decidable _≈₁_ → Decidable _≤₁_ →
                ∀ {_≤₂_} → Decidable _≤₂_ →
                Decidable (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-decidable dec-≈₁ dec-≤₁ dec-≤₂ =
    Strict.×-decidable dec-≈₁ (Conv.decidable _ _ dec-≈₁ dec-≤₁)
                       dec-≤₂

  ×-total : ∀ {_≈₁_ _≤₁_} → Symmetric _≈₁_ → Decidable _≈₁_ →
                            Antisymmetric _≈₁_ _≤₁_ → Total _≤₁_ →
            ∀ {_≤₂_} → Total _≤₂_ →
            Total (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-total {_≈₁_ = _≈₁_} {_≤₁_ = _≤₁_} sym₁ dec₁ antisym₁ total₁
                        {_≤₂_ = _≤₂_} total₂ = total
    where
    tri₁ : Trichotomous _≈₁_ (Conv._<_ _≈₁_ _≤₁_)
    tri₁ = Conv.trichotomous _ _ sym₁ dec₁ antisym₁ total₁

    total : Total (×-Lex _≈₁_ _≤₁_ _≤₂_)
    total x y with tri₁ (proj₁ x) (proj₁ y)
    ... | tri< x₁<y₁ x₁≉y₁ x₁≯y₁ = inj₁ (inj₁ x₁<y₁)
    ... | tri> x₁≮y₁ x₁≉y₁ x₁>y₁ = inj₂ (inj₁ x₁>y₁)
    ... | tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁ with total₂ (proj₂ x) (proj₂ y)
    ...   | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁ , x₂≤y₂))
    ...   | inj₂ x₂≥y₂ = inj₂ (inj₂ (sym₁ x₁≈y₁ , x₂≥y₂))

  -- Some collections of properties which are preserved by ×-Lex
  -- (under certain assumptions).

  _×-isPartialOrder_ :
    ∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
    ∀ {_≈₂_ _≤₂_} → IsPartialOrder _≈₂_ _≤₂_ →
    IsPartialOrder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
  _×-isPartialOrder_ {_≈₁_ = _≈₁_} {_≤₁_ = _≤₁_} po₁
                     {_≤₂_ = _≤₂_} po₂ = record
    { isPreorder = record
        { isEquivalence = Pointwise._×-isEquivalence_
                            (isEquivalence po₁)
                            (isEquivalence po₂)
        ; reflexive     = λ {x y} →
                          ×-reflexive _≈₁_ _≤₁_ _≤₂_ (reflexive po₂)
                                      {x} {y}
        ; trans         = λ {x y z} →
                          ×-transitive po₁ {_≤₂_ = _≤₂_} (trans po₂)
                                       {x} {y} {z}
        }
    ; antisym = λ {x y} →
                ×-antisymmetric {_≤₁_ = _≤₁_} po₁
                                {_≤₂_ = _≤₂_} (antisym po₂) {x} {y}
    }
    where open IsPartialOrder

  ×-isTotalOrder :
    ∀ {_≈₁_ _≤₁_} → Decidable _≈₁_ → IsTotalOrder _≈₁_ _≤₁_ →
    ∀ {_≈₂_ _≤₂_} → IsTotalOrder _≈₂_ _≤₂_ →
    IsTotalOrder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-isTotalOrder {_≤₁_ = _≤₁_} ≈₁-dec to₁ {_≤₂_ = _≤₂_} to₂ = record
    { isPartialOrder = isPartialOrder to₁ ×-isPartialOrder
                       isPartialOrder to₂
    ; total          = ×-total {_≤₁_ = _≤₁_} (Eq.sym to₁) ≈₁-dec
                                             (antisym to₁) (total to₁)
                               {_≤₂_ = _≤₂_} (total to₂)
    }
    where open IsTotalOrder

  _×-isDecTotalOrder_ :
    ∀ {_≈₁_ _≤₁_} → IsDecTotalOrder _≈₁_ _≤₁_ →
    ∀ {_≈₂_ _≤₂_} → IsDecTotalOrder _≈₂_ _≤₂_ →
    IsDecTotalOrder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
  _×-isDecTotalOrder_ {_≤₁_ = _≤₁_} to₁ {_≤₂_ = _≤₂_} to₂ = record
    { isTotalOrder = ×-isTotalOrder (_≟_ to₁)
                                    (isTotalOrder to₁)
                                    (isTotalOrder to₂)
    ; _≟_          = Pointwise._×-decidable_ (_≟_ to₁) (_≟_ to₂)
    ; _≤?_         = ×-decidable (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
    }
    where open IsDecTotalOrder

-- "Packages" (e.g. posets) can also be combined.

_×-poset_ :
  ∀ {p₁ p₂ p₃ p₄} → Poset p₁ p₂ _ → Poset p₃ p₄ _ → Poset _ _ _
p₁ ×-poset p₂ = record
  { isPartialOrder = isPartialOrder p₁ ×-isPartialOrder
                     isPartialOrder p₂
  } where open Poset

_×-totalOrder_ :
  ∀ {d₁ d₂ t₃ t₄} →
  DecTotalOrder d₁ d₂ _ → TotalOrder t₃ t₄ _ → TotalOrder _ _ _
t₁ ×-totalOrder t₂ = record
  { isTotalOrder = ×-isTotalOrder T₁._≟_ T₁.isTotalOrder T₂.isTotalOrder
  }
  where
  module T₁ = DecTotalOrder t₁
  module T₂ =    TotalOrder t₂

_×-decTotalOrder_ :
  ∀ {d₁ d₂ d₃ d₄} →
  DecTotalOrder d₁ d₂ _ → DecTotalOrder d₃ d₄ _ → DecTotalOrder _ _ _
t₁ ×-decTotalOrder t₂ = record
  { isDecTotalOrder = isDecTotalOrder t₁ ×-isDecTotalOrder
                      isDecTotalOrder t₂
  } where open DecTotalOrder


text:
{-

    Verified Koopa Troopa Movement
             Toon Nolten

-}

module koopa where
  open import Data.Nat
  open import Data.Fin renaming (_+_ to _F+_; _<_ to _F<_; suc to fsuc;
    zero to fzero)
  open import Data.Vec renaming (map to vmap; lookup to vlookup;
                                     replicate to vreplicate)
  open import Data.Unit
  open import Data.Empty

  module Matrix where
    data Matrix (A : Set) : ℕ → ℕ → Set where
      Mat : {w h : ℕ} → Vec (Vec A w) h → Matrix A w h

    lookup : ∀ {w h} {A : Set} → Fin h → Fin w → Matrix A w h → A
    lookup row column (Mat rows) = vlookup column (vlookup row rows)
  open Matrix

  data Color : Set where
    Green : Color
    Red : Color

  data KoopaTroopa : Color → Set where
    _KT : (c : Color) → KoopaTroopa c

  data Material : Set where
    gas    : Material
    -- liquid : Material
    solid  : Material

  data Clearance : Set where
    Low  : Clearance
    High : Clearance
    God  : Clearance

  record Position : Set where
    constructor pos
    field
      x   : ℕ
      y   : ℕ
      mat : Material
      clr : Clearance

  data _c>_ : Color → Clearance → Set where
    <red>   : ∀ {c} → c c> Low
    <green> : Green c> High

  data _follows_⟨_⟩ : Position → Position → Color → Set where
    stay  : ∀ {c x y} → pos x y gas Low follows pos x y gas Low ⟨ c ⟩
    next  : ∀ {c cl x y}{{_ : c c> cl}} →
            pos (suc x) y gas cl follows pos x y gas Low ⟨ c ⟩
    back  : ∀ {c cl x y}{{_ : c c> cl}} →
            pos x y gas cl follows pos (suc x) y gas Low ⟨ c ⟩
    -- jump  : ∀ {c x y} → pos x (suc y) gas High follows pos x y gas Low ⟨ c ⟩
    fall  : ∀ {c cl x y} → pos x y gas cl follows pos x (suc y) gas High ⟨ c ⟩

  infixr 5 _↠⟨_⟩_
  data Path {c : Color} (Koopa : KoopaTroopa c) :
       Position → Position → Set where
    []  : ∀ {p} → Path Koopa p p
    _↠⟨_⟩_ : {q r : Position} → (p : Position) → q follows p ⟨ c ⟩
                → (qs : Path Koopa q r) → Path Koopa p r

  ex_path : Path (Red KT) (pos 0 0 gas Low) (pos 0 0 gas Low)
  ex_path = pos 0 0 gas Low ↠⟨ next ⟩
            pos 1 0 gas Low ↠⟨ back ⟩
            pos 0 0 gas Low ↠⟨ stay ⟩ []

  matToPosVec : {n : ℕ} → Vec Material n → Vec Material n → ℕ → ℕ →
                   Vec Position n
  matToPosVec []           []        _ _ = []
  matToPosVec (mat ∷ mats) (under ∷ unders) x y =
    pos x y mat cl ∷ matToPosVec mats unders (x + 1) y
      where
        clearance : Material → Material → Clearance
        clearance gas   gas   = High
        clearance gas   solid = Low
        clearance solid _     = God
        cl = clearance mat under

  matToPosVecs : {w h : ℕ} → Vec (Vec Material w) h → Vec (Vec Position w) h
  matToPosVecs [] = []
  matToPosVecs (_∷_ {y} mats matss) =
    matToPosVec mats (unders matss gas) 0 y ∷ matToPosVecs matss
    where
      unders : ∀ {m n ℓ}{A : Set ℓ} → Vec (Vec A m) n → A → Vec A m
      unders [] fallback = vreplicate fallback
      unders (us ∷ _) _ = us

  matsToMat : {w h : ℕ} → Vec (Vec Material w) h → Matrix Position w h
  matsToMat matss = Mat (reverse (matToPosVecs matss))

  □ : Material
  □ = gas
  ■ : Material
  ■ = solid
  example_level : Matrix Position 10 7
  example_level = matsToMat (
    (□ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ []) ∷
    (□ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ ■ ∷ ■ ∷ ■ ∷ □ ∷ []) ∷
    (□ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ []) ∷
    (□ ∷ □ ∷ □ ∷ ■ ∷ ■ ∷ ■ ∷ □ ∷ □ ∷ □ ∷ □ ∷ []) ∷
    (□ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ []) ∷
    (■ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ ■ ∷ []) ∷
    (■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ □ ∷ □ ∷ ■ ∷ ■ ∷ ■ ∷ []) ∷ [])

  _<'_ : ℕ → ℕ → Set
  m <' zero = ⊥
  zero <' suc n = ⊤
  suc m <' suc n = m <' n

  fromNat : ∀ {n}(k : ℕ){_ : k <' n} → Fin n
  fromNat {zero} k {}
  fromNat {suc n} zero = fzero
  fromNat {suc n} (suc k) {p} = fsuc (fromNat k {p})

  f : ∀ {n}(k : ℕ){_ : k <' n} → Fin n
  f = fromNat

  p : (x : Fin 10) → (y : Fin 7) → Position
  p x y = lookup y x example_level

  red_path_one : Path (Red KT) (p (f 7) (f 6)) (p (f 8) (f 6))
  red_path_one = p (f 7) (f 6) ↠⟨ back ⟩
                 p (f 6) (f 6) ↠⟨ next ⟩
                 p (f 7) (f 6) ↠⟨ next ⟩
                 p (f 8) (f 6) ↠⟨ stay ⟩ []

  red_path_two : Path (Red KT) (p (f 2) (f 1)) (p (f 3) (f 1))
  red_path_two = p (f 2) (f 1) ↠⟨ back ⟩
                 p (f 1) (f 1) ↠⟨ next ⟩
                 p (f 2) (f 1) ↠⟨ next ⟩
                 p (f 3) (f 1) ↠⟨ next ⟩
                 p (f 4) (f 1) ↠⟨ back ⟩
                 p (f 3) (f 1) ↠⟨ stay ⟩
                 []

  -- -- Type error shows up 'late' because 'cons' is right associative
  -- red_nopath_one : Path (Red KT) (p (f 1) (f 1)) (p (f 0) (f 1))
  -- red_nopath_one = p (f 1) (f 1) ↠⟨ back ⟩
  --                  p (f 0) (f 1) ↠⟨ stay ⟩
  --                  []

  -- -- Red KoopaTroopa can't step into a wall
  -- red_nopath_two : Path (Red KT) (p (f 1) (f 1)) (p (f 0) (f 1))
  -- red_nopath_two = p (f 1) (f 1) ↠⟨ back ⟩ []

  -- -- Red KoopaTroopa can't step into air
  -- red_nopath_three : Path (Red KT) (p (f 4) (f 1)) (p (f 5) (f 1))
  -- red_nopath_three = p (f 4) (f 1) ↠⟨ next ⟩ []

  -- Any path that is valid for red KoopaTroopas, is also valid for green
  -- KoopaTroopas because we did not constrain KoopaTroopas to only turn
  -- When there is an obstacle
  green_path_one : Path (Green KT) (p (f 7) (f 6)) (p (f 8) (f 6))
  green_path_one = p (f 7) (f 6) ↠⟨ back ⟩
                   p (f 6) (f 6) ↠⟨ next ⟩
                   p (f 7) (f 6) ↠⟨ next ⟩
                   p (f 8) (f 6) ↠⟨ stay ⟩ []

  green_path_two : Path (Green KT) (p (f 7) (f 6)) (p (f 5) (f 0))
  green_path_two = p (f 7) (f 6) ↠⟨ back ⟩
                   p (f 6) (f 6) ↠⟨ back ⟩
                   p (f 5) (f 6) ↠⟨ fall ⟩
                   p (f 5) (f 5) ↠⟨ fall ⟩
                   p (f 5) (f 4) ↠⟨ back ⟩
                   p (f 4) (f 4) ↠⟨ back ⟩
                   p (f 3) (f 4) ↠⟨ back ⟩
                   p (f 2) (f 4) ↠⟨ fall ⟩
                   p (f 2) (f 3) ↠⟨ fall ⟩
                   p (f 2) (f 2) ↠⟨ fall ⟩
                   p (f 2) (f 1) ↠⟨ back ⟩
                   p (f 1) (f 1) ↠⟨ next ⟩
                   p (f 2) (f 1) ↠⟨ next ⟩
                   p (f 3) (f 1) ↠⟨ next ⟩
                   p (f 4) (f 1) ↠⟨ next ⟩
                   p (f 5) (f 1) ↠⟨ fall ⟩
                   []

  -- -- Green KoopaTroopa can't step into a wall
  -- green_nopath_one : Path (Green KT) (p (f 1) (f 1)) (p (f 0) (f 1))
  -- green_nopath_one = p (f 1) (f 1) ↠⟨ back ⟩ []

max_stars_repo_name: toonn/popartt

max_issues_repo_name: toonn/popartt

max_forks_repo_name: toonn/popartt


text:
module Equality where

open import Agda.Builtin.Equality public
open import Relation.Nullary

infix 4 _≅_ _≢_
infixr 2 _≡⟨_⟩_
infix  3 _QED

data _≅_ {ℓ} {A : Set ℓ} (x : A) : {B : Set ℓ} → B → Set ℓ where
   refl : x ≅ x

≡→≅ : ∀ {ℓ} {A : Set ℓ} {a b : A} → a ≡ b → a ≅ b
≡→≅ refl = refl

sym : ∀ {ℓ} {A : Set ℓ} {a b : A} → a ≡ b → b ≡ a
sym refl = refl

sym′ : ∀ {ℓ} {A B : Set ℓ} {a : A} {b : B} → a ≅ b → b ≅ a
sym′ refl = refl

subst₂ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p)
         {x₁ x₂ y₁ y₂} → x₁ ≡ x₂ → y₁ ≡ y₂ → P x₁ y₁ → P x₂ y₂
subst₂ P refl refl p = p

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

cong-app : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
           f ≡ g → (x : A) → f x ≡ g x
cong-app refl x = refl

cong₂ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
        (f : A → B → C) {x y u v} → x ≡ y → u ≡ v → f x u ≡ f y v
cong₂ f refl refl = refl

_≢_ : ∀ {a} {A : Set a} → A → A → Set a
x ≢ y = ¬ x ≡ y

_≡⟨_⟩_ : ∀ {A : Set} (x : A) {y z : A}
       → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ refl ⟩ refl = refl

_QED : ∀ {A : Set} (x : A) → x ≡ x
x QED = refl


text:
{-# OPTIONS --safe #-}
module JVM.Model {ℓ} (T : Set ℓ) where

open import Level hiding (Lift)
open import Data.Product
open import Data.Unit
open import Data.List

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Ternary.Core
open import Relation.Ternary.Structures

open import Relation.Ternary.Construct.Empty T public
open import Relation.Ternary.Construct.Duplicate T public

open import Data.List.Relation.Binary.Permutation.Propositional
  using ()
  renaming (_↭_ to _≈_)
open import Data.List.Relation.Binary.Permutation.Propositional.Properties
  using (++-isMonoid)

instance ++-monoid-instance = ++-isMonoid

module Disjoint where
  open import Relation.Ternary.Construct.Bag empty-rel tt public
  open IsPartialSemigroup bags-isSemigroup public
  open IsPartialMonoid bags-isMonoid public
  open IsCommutative bags-isCommutative public

module Overlap where
  open import Relation.Ternary.Construct.Bag duplicate tt public
  open IsPartialSemigroup bags-isSemigroup public
  open IsPartialMonoid bags-isMonoid public
  open IsCommutative bags-isCommutative  public
  open IsTotal bags-isTotal public

open Disjoint using (bag-emptiness) renaming
  ( empty-unique to empty-bag-unique
  ; singleton-unique to singleton-bag-unique)
  public

open Rel₃ Disjoint.bags using ()
  renaming (_∙_≣_ to _⊕_≣_; _✴_ to _⊕_; _─✴_ to _─⊕_; _∙⟨_⟩_ to _⊕⟨_⟩_) public
open Rel₃ Overlap.bags using ()
  renaming (_∙_≣_ to _⊗_≣_; _✴_ to _⊗_; _─✴_ to _─⊗_; _∙⟨_⟩_ to _⊗⟨_⟩_) public

open import Relation.Ternary.Construct.Bag.Properties
open import Data.List.Relation.Binary.Permutation.Propositional
open CrossSplittable {{div₁ = duplicate}} {{empty-rel}} (λ _ ())

abstract
  private
    m₁ : IsPartialMonoid _↭_ Disjoint.bags []
    m₁ = Disjoint.bags-isMonoid

    m₂ : IsPartialMonoid _↭_ Overlap.bags []
    m₂ = Overlap.bags-isMonoid

    p₁ : IsPositiveWithZero 0ℓ _↭_ Disjoint.bags []
    p₁ = Disjoint.bags-isPositive-w/0

    p₂ : IsPositiveWithZero 0ℓ _↭_ Overlap.bags []
    p₂ = Overlap.bags-isPositive-w/0

    c₁ : IsCommutative Disjoint.bags
    c₁ = Disjoint.bags-isCommutative

    c₂ : IsCommutative Overlap.bags
    c₂ = Overlap.bags-isCommutative

    x  : CrossSplit Overlap.bags Disjoint.bags
    x  = xsplit

    ux  : Uncross Disjoint.bags Overlap.bags
    ux = uncrossover (unxcross λ ())

  open import Relation.Ternary.Construct.Exchange
    {A = List T}
    {{m₁}} {{m₂}} {{p₁}} {{p₂}} {{empty-bag-unique}} {{c₁}} {{c₂}}
    {{Disjoint.bags-isTotal}}
    {{Overlap.bags-isTotal}}
    {{++-isMonoid}}
    x ux
    public
    renaming
      (Account to Intf
      ; _≈_ to _≈intf≈_
      ; exchange-rel to intf-rel
      ; exchange-emptiness to intf-emptiness
      ; exchange-isSemigroup to intf-isSemigroup
      ; exchange-isCommutative to intf-isCommutative
      ; exchange-isMonoid to intf-isMonoid
      ; exchange-isTotal to intf-isTotal)

  open DownIntuitive {{Overlap.bags-isContractive}} public

module Syntax where
  open Rel₃ intf-rel public
  open Emptiness          intf-emptiness     public
  open IsPartialSemigroup intf-isSemigroup   public
  open IsPartialMonoid    intf-isMonoid      public
  open IsCommutative      intf-isCommutative public
  open CommutativeSemigroupOps {{intf-isSemigroup}} {{intf-isCommutative}} public

  -- module _ {P} where
  --   open IsIntuitionistic (intf-isIntuitive {P}) w public

open Syntax


text:
open import OutsideIn.Prelude
open import OutsideIn.X
module OutsideIn.Environments(x : X) where
  open import Data.Vec hiding (map)
  import OutsideIn.TypeSchema as TS
  import OutsideIn.Expressions as E
  open TS(x)
  open E(x)
  open X(x)

  private
    module TS-f {x} = Functor(type-schema-is-functor {x})

  Environment : Set → Set → Set
  Environment ev tv = ∀ {x} → Name ev x → TypeSchema tv x

  ⟨_⟩,_ : ∀{ev}{tv} → TypeSchema tv Regular → (∀{x} → Name ev x → TypeSchema tv x)
        → ∀{x} → Name (Ⓢ ev) x → TypeSchema tv x
  (⟨ τ ⟩, Γ) (N zero) = τ
  (⟨ τ ⟩, Γ) (N (suc n)) = Γ (N n)
  (⟨ τ ⟩, Γ) (DC n) = Γ (DC n)

  _↑Γ : {ev tv : Set} → Environment ev tv → Environment ev (Ⓢ tv)
  Γ ↑Γ = TS-f.map suc ∘ Γ

  addAll : ∀{n}{ev}{tv} → Vec (Type tv) n → ( Environment ev tv) → Environment (ev ⨁ n) tv
  addAll [] Γ = Γ
  addAll (τ ∷ τs) Γ = addAll τs (⟨ ∀′ 0 · ε ⇒ τ ⟩, Γ )

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition of the sublist relation. This is commonly
-- known as Order Preserving Embeddings (OPE).
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Sublist.Propositional
  {a} {A : Set a} where

open import Data.List.Base using (List)
open import Data.List.Relation.Binary.Equality.Propositional using (≋⇒≡)
import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist
open import Data.List.Relation.Unary.Any using (Any)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Unary using (Pred)

------------------------------------------------------------------------
-- Re-export definition and operations from setoid sublists

open SetoidSublist (setoid A) public
  hiding
  (lookup; ⊆-reflexive; ⊆-antisym
  ; ⊆-isPreorder; ⊆-isPartialOrder
  ; ⊆-preorder; ⊆-poset
  )

------------------------------------------------------------------------
-- Additional operations

module _ {p} {P : Pred A p} where

  lookup : ∀ {xs ys} → xs ⊆ ys → Any P xs → Any P ys
  lookup = SetoidSublist.lookup (setoid A) (subst _)

------------------------------------------------------------------------
-- Relational properties

⊆-reflexive : _≡_ ⇒ _⊆_
⊆-reflexive refl = ⊆-refl

⊆-antisym : Antisymmetric _≡_ _⊆_
⊆-antisym xs⊆ys ys⊆xs = ≋⇒≡ (SetoidSublist.⊆-antisym (setoid A) xs⊆ys ys⊆xs)

⊆-isPreorder : IsPreorder _≡_ _⊆_
⊆-isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = ⊆-reflexive
  ; trans         = ⊆-trans
  }

⊆-isPartialOrder : IsPartialOrder _≡_ _⊆_
⊆-isPartialOrder = record
  { isPreorder = ⊆-isPreorder
  ; antisym    = ⊆-antisym
  }

⊆-preorder : Preorder a a a
⊆-preorder = record
  { isPreorder = ⊆-isPreorder
  }

⊆-poset : Poset a a a
⊆-poset = record
  { isPartialOrder = ⊆-isPartialOrder
  }

------------------------------------------------------------------------
-- Separating two sublists
--
-- Two possibly overlapping sublists τ : xs ⊆ zs and σ : ys ⊆ zs
-- can be turned into disjoint lists τρ : xs ⊆ zs and τρ : ys ⊆ zs′
-- by duplicating all entries of zs that occur both in xs and ys,
-- resulting in an extension ρ : zs ⊆ zs′ of zs.

record Separation {xs ys zs} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) : Set a where
  field
    {inflation} : List A
    separator₁  : zs ⊆ inflation
    separator₂  : zs ⊆ inflation
  separated₁ = ⊆-trans τ₁ separator₁
  separated₂ = ⊆-trans τ₂ separator₂
  field
    disjoint    : Disjoint separated₁ separated₂

infixr 5 _∷ₙ-Sep_ _∷ₗ-Sep_ _∷ᵣ-Sep_

-- Empty separation

[]-Sep : Separation [] []
[]-Sep = record { separator₁ = [] ; separator₂ = [] ; disjoint = [] }

-- Weaken a separation

_∷ₙ-Sep_ : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
           ∀ z → Separation τ₁ τ₂ → Separation (z ∷ʳ τ₁) (z ∷ʳ τ₂)
z ∷ₙ-Sep record{ separator₁ = ρ₁; separator₂ = ρ₂; disjoint = d } = record
  { separator₁ = refl ∷ ρ₁
  ; separator₂ = refl ∷ ρ₂
  ; disjoint   = z   ∷ₙ d
  }

-- Extend a separation by an element of the first sublist.
--
-- Note: this requires a category law from the underlying equality,
-- trans x=z refl = x=z, thus, separation is not available for Sublist.Setoid.

_∷ₗ-Sep_ : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
          ∀ {x z} (x≡z : x ≡ z) → Separation τ₁ τ₂ → Separation (x≡z ∷ τ₁) (z ∷ʳ τ₂)
refl ∷ₗ-Sep record{ separator₁ = ρ₁; separator₂ = ρ₂; disjoint = d } = record
  { separator₁ = refl ∷ ρ₁
  ; separator₂ = refl ∷ ρ₂
  ; disjoint   = refl ∷ₗ d
  }

-- Extend a separation by an element of the second sublist.

_∷ᵣ-Sep_ : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
          ∀ {y z} (y≡z : y ≡ z) → Separation τ₁ τ₂ → Separation (z ∷ʳ τ₁) (y≡z ∷ τ₂)
refl ∷ᵣ-Sep record{ separator₁ = ρ₁; separator₂ = ρ₂; disjoint = d } = record
  { separator₁ = refl ∷ ρ₁
  ; separator₂ = refl ∷ ρ₂
  ; disjoint   = refl ∷ᵣ d
  }

-- Extend a separation by a common element of both sublists.
--
-- Left-biased: the left separator gets the first copy
-- of the common element.

∷-Sepˡ : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
        ∀ {x y z} (x≡z : x ≡ z) (y≡z : y ≡ z) →
        Separation τ₁ τ₂ → Separation (x≡z ∷ τ₁) (y≡z ∷ τ₂)
∷-Sepˡ refl refl record{ separator₁ = ρ₁; separator₂ = ρ₂; disjoint = d } = record
  { separator₁ = _ ∷ʳ refl ∷ ρ₁
  ; separator₂ = refl ∷ _ ∷ʳ ρ₂
  ; disjoint   = refl ∷ᵣ (refl ∷ₗ d)
  }

-- Left-biased separation of two sublists.  Of common elements,
-- the first sublist receives the first copy.

separateˡ : ∀ {xs ys zs} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → Separation τ₁ τ₂
separateˡ [] [] = []-Sep
separateˡ (z  ∷ʳ τ₁) (z  ∷ʳ τ₂) = z   ∷ₙ-Sep separateˡ τ₁ τ₂
separateˡ (z  ∷ʳ τ₁) (y≡z ∷ τ₂) = y≡z ∷ᵣ-Sep separateˡ τ₁ τ₂
separateˡ (x≡z ∷ τ₁) (z  ∷ʳ τ₂) = x≡z ∷ₗ-Sep separateˡ τ₁ τ₂
separateˡ (x≡z ∷ τ₁) (y≡z ∷ τ₂) = ∷-Sepˡ x≡z y≡z (separateˡ τ₁ τ₂)


text:
module Verifier where

open import Definitions
open import DeMorgan using (deMorgan)

check : {A B : Set} → ¬ A ∧ ¬ B → ¬ (A ∨ B)
check = deMorgan

max_stars_repo_name: danr/agder

max_issues_repo_name: danr/agder

max_forks_repo_name: danr/agder


text:
-- Let's play with agda.
  -- Am i having fun doing this? @KMx404

module intro where --load the file with C-c - like that

data Bool: Set where
  true : Bool
  false : Bool

data Empty: Set Empty
  Empty : Empty -- I'm gonna leave this here. Moving to tests


text:
module Issue2858-nbe where

open import Agda.Builtin.List

data Ty : Set where
  α : Ty
  _↝_ : Ty → Ty → Ty

variable
  σ τ : Ty
  Γ Δ Θ : List Ty

Scoped : Set₁
Scoped = Ty → List Ty → Set

data Var : Scoped where
  z : Var σ (σ ∷ Γ)
  s : Var σ Γ → Var σ (τ ∷ Γ)

record Ren (Γ Δ : List Ty) : Set where
  field lookup : ∀ {σ} → Var σ Γ → Var σ Δ
open Ren public

bind : Ren Γ Δ → Ren (σ ∷ Γ) (σ ∷ Δ)
lookup (bind ρ) z     = z
lookup (bind ρ) (s v) = s (lookup ρ v)

refl : Ren Γ Γ
lookup refl v = v

step : Ren Γ (σ ∷ Γ)
lookup step v = s v

_∘_ : Ren Δ Θ → Ren Γ Δ → Ren Γ Θ
lookup (ρ′ ∘ ρ) v = lookup ρ′ (lookup ρ v)

interleaved mutual

  data Syn : Scoped
  data Chk : Scoped
  th^Syn : Ren Γ Δ → Syn σ Γ → Syn σ Δ
  th^Chk : Ren Γ Δ → Chk σ Γ → Chk σ Δ

  -- variable rule
  constructor
    var : Var σ Γ → Syn σ Γ
  th^Syn ρ (var v) = var (lookup ρ v)

  -- change of direction rules
  constructor
    emb : Syn σ Γ → Chk σ Γ
    cut : Chk σ Γ → Syn σ Γ
  th^Chk ρ (emb t) = emb (th^Syn ρ t)
  th^Syn ρ (cut c) = cut (th^Chk ρ c)

  -- function introduction and elimination
  constructor
    app : Syn (σ ↝ τ) Γ → Chk σ Γ → Syn τ Γ
    lam : Chk τ (σ ∷ Γ) → Chk (σ ↝ τ) Γ
  th^Syn ρ (app f t) = app (th^Syn ρ f) (th^Chk ρ t)
  th^Chk ρ (lam b) = lam (th^Chk (bind ρ) b)

-- Model construction

Val : Scoped
Val α       Γ = Syn α Γ
Val (σ ↝ τ) Γ = ∀ {Δ} → Ren Γ Δ → Val σ Δ → Val τ Δ

th^Val : Ren Γ Δ → Val σ Γ → Val σ Δ
th^Val {σ = α}     ρ t = th^Syn ρ t
th^Val {σ = σ ↝ τ} ρ t = λ ρ′ → t (ρ′ ∘ ρ)

interleaved mutual

  reify   : ∀ σ → Val σ Γ → Chk σ Γ
  reflect : ∀ σ → Syn σ Γ → Val σ Γ

  -- base case
  reify   α t = emb t
  reflect α t = t

  -- arrow case
  reify   (σ ↝ τ) t = lam (reify τ (t step (reflect σ (var z))))
  reflect (σ ↝ τ) t = λ ρ v → reflect τ (app (th^Syn ρ t) (reify σ v))

record Env (Γ Δ : List Ty) : Set where
  field lookup : ∀ {σ} → Var σ Γ → Val σ Δ
open Env public

th^Env : Ren Δ Θ → Env Γ Δ → Env Γ Θ
lookup (th^Env ρ vs) v = th^Val ρ (lookup vs v)

placeholders : Env Γ Γ
lookup placeholders v = reflect _ (var v)

extend : Env Γ Δ → Val σ Δ → Env (σ ∷ Γ) Δ
lookup (extend ρ t) z     = t
lookup (extend ρ t) (s v) = lookup ρ v

interleaved mutual

  eval^Syn : Env Γ Δ → Syn σ Γ → Val σ Δ
  eval^Chk : Env Γ Δ → Chk σ Γ → Val σ Δ

  -- variable
  eval^Syn vs (var v) = lookup vs v

  -- change of direction
  eval^Syn vs (cut t) = eval^Chk vs t
  eval^Chk vs (emb t) = eval^Syn vs t

  -- function introduction & elimination
  eval^Syn vs (app f t) = eval^Syn vs f refl (eval^Chk vs t)
  eval^Chk vs (lam b)   = λ ρ v → eval^Chk (extend (th^Env ρ vs) v) b

interleaved mutual

  norm^Syn : Syn σ Γ → Chk σ Γ
  norm^Chk : Chk σ Γ → Chk σ Γ

  norm^Syn t = norm^Chk (emb t)
  norm^Chk t = reify _ (eval^Chk placeholders t)

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --without-K #-}
-- Rending the Program Runner
-- A proof of Lӧb′s theorem: quoted interpreters are inconsistent
-- Jason Gross

{- Title and some comments inspired by and drawn heavily from
   "Scooping the Loop Sniffer: A proof that the Halting Problem is
   undecidable", by Geoffrey K. Pullum
   (http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html) -}

open import common

infixl 2 _▻_
infixl 3 _‘’_
infixr 1 _‘→’_

{- "Scooping the Loop Sniffer", with slight modifications for this
   code.

No general procedure for type-checking will do.
Now, I won’t just assert that, I’ll prove it to you.
I will prove that although you might work till you drop,
you cannot tell if computation will stop.

For imagine we have a procedure called P
that for specified input permits you to see
what specified source code, with all of its faults,
defines a routine that eventually halts.

You feed in your program, with suitable data,
and P gets to work, and a little while later
(in finite compute time) correctly infers
whether infinite looping behavior occurs.

If there will be no looping, then P prints out ‘Good.’
That means work on this input will halt, as it should.
But if it detects an unstoppable loop,
then P reports ‘Bad!’ — which means you’re in the soup.

Well, the truth is that P cannot possibly be,
because if you wrote it and gave it to me,
I could use it to set up a logical bind
that would shatter your reason and scramble your mind.

For a specified program, say ‶A″, one supplies,
the first step of this program called Q I devise
is to find out from P what’s the right thing to say
of the looping behavior of A run on ‶A″.

If P’s answer is ‘Bad!’, Q will suddenly stop.
But otherwise, Q will go back to the top,
and start off again, looping endlessly back,
till the universe dies and turns frozen and black.

And this program called Q wouldn’t stay on the shelf;
I would ask it to forecast its run on itself.
When it reads its own source code, just what will it do?
What’s the looping behavior of Q run on Q?

If P warns of infinite loops, Q will quit;
yet P is supposed to speak truly of it!
And if Q’s going to quit, then P should say ‘Good.’
Which makes Q start to loop! (P denied that it would.)

No matter how P might perform, Q will scoop it:
Q uses P’s output to make P look stupid.
Whatever P says, it cannot predict Q:
P is right when it’s wrong, and is false when it’s true!

I’ve created a paradox, neat as can be —
and simply by using your putative P.
When you posited P you stepped into a snare;
Your assumption has led you right into my lair.

So where can this argument possibly go?
I don’t have to tell you; I’m sure you must know.
A reductio: There cannot possibly be
a procedure that acts like the mythical P.

You can never find general mechanical means
for predicting the acts of computing machines;
it’s something that cannot be done. So we users
must find our own bugs. Our computers are losers! -}

{- Our program will act much like this Q, except that instead of saying that

  Q will go back to the top,
  and start off again, looping endlessly back,
  till the universe dies and turns frozen and black.

We would say something more like that

  Q will go back to the top,
  and ask for the output of A run on ‶A″,
  trusting P that execution will not run away.

Further more, we combine the type-checker and the interpreter; we show
there cannot be a well-typed quoted interpreter that interprets all
well-typed quoted terms directly, rather than having a separate phase
of type-checking.  Morally, they should be equivalent. -}

{- We start off by defining Contexts, Types, and Terms which are
well-typed by construction.

We will prove that assuming Lӧb′s theorem is consistent in a minimal
representation, and doesn′t require anything fancy to support it in a
model of the syntax.  Thus any reasonable syntax, which has a model,
will also have a model validating Lӧb′s theorem.

This last part is informal; it′s certainly conceivable that something
like internalized parametricity, which needs to do something special
with each constructor of the language, won't be able to do anything
with the quotation operator.

There's a much longer formalization of Lӧb′s theorem in this
repository which just assumes a quotation operator, and proves Lӧb′s
theorem by constructing it (though to build a quine, we end up needing
to decide equality of Contexts, which is fine); the quotation operator
is, in principle, definable, by stuffing the constructors of the
syntax into an initial context, and building up the quoted terms by
structural recursion.  This would be even more painful, though, unless
there′s a nice way to give specific quoted terms.

Now, down to business. -}

mutual
  -- Contexts are utterly standard
  data Context : Set where
    ε : Context
    _▻_ : (Γ : Context) → Type Γ → Context

  -- Types have standard substituition and non-dependent function
  -- types.
  data Type : Context → Set where
    _‘’_ : ∀ {Γ A} → Type (Γ ▻ A) → Term {Γ} A → Type Γ
    _‘→’_ : ∀ {Γ} → Type Γ → Type Γ → Type Γ
  -- We also require that there be a quotation of ‶Type ε″ (called
  -- ‘Typeε’), and a quotation of ‶Term ε″ (called ‘□’)
    ‘Typeε’ : Type ε
    ‘□’ : Type (ε ▻ ‘Typeε’)
  -- We don′t really need quoted versions of ⊤ and ⊥, but they are
  -- useful stating a few things after the proof of Lӧb′s theorem
    ‘⊤’ : ∀ {Γ} → Type Γ
    ‘⊥’ : ∀ {Γ} → Type Γ
  -- Note that you can add whatever other constructors to this data
  -- type you would like;

  data Term : {Γ : Context} → Type Γ → Set where
  -- We require the existence of a function (in the ambient language)
  -- that takes a type in the empty context, and returns the quotation
  -- of that type.
    ⌜_⌝ : Type ε → Term {ε} ‘Typeε’
  -- Finally, we assume Lӧb′s theorem; we will show that this syntax
  -- has a model.
    Lӧb : ∀ {X} → Term {ε} (‘□’ ‘’ ⌜ X ⌝ ‘→’ X) → Term {ε} X
  -- This is not strictly required, just useful for showing that some
  -- type is inhabited.
    ‘tt’ : ∀ {Γ} → Term {Γ} ‘⊤’

{- ‶□ T″ is read ‶T is provable″ or ‶T is inhabited″ or ‶the type of
syntactic terms of the syntactic type T″ or ‶the type of quoted terms
of the quoted type T″. -}

□ : Type ε → Set _
□ = Term {ε}

mutual
  {- Having an inhabitant of type ‶the interpretation of a given
  Context″ is having an inhabitant of the interpretation of every type
  in that Context.  If we wanted to represent more universes, we could
  sprinkle lifts and lowers, and it would not cause us trouble.  They
  are elided here for simplicity. -}
  Context⇓ : (Γ : Context) → Set
  Context⇓ ε = ⊤
  Context⇓ (Γ ▻ T) = Σ (Context⇓ Γ) (Type⇓ {Γ} T)

  -- Substitution and function types are interpreted standardly.
  Type⇓ : {Γ : Context} → Type Γ → Context⇓ Γ → Set
  Type⇓ (T ‘’ x) Γ⇓ = Type⇓ T (Γ⇓ , Term⇓ x Γ⇓)
  Type⇓ (A ‘→’ B) Γ⇓ = Type⇓ A Γ⇓ → Type⇓ B Γ⇓
  -- ‘Typeε’ is, unsurprisingly, interpreted as Type ε, the type of
  -- syntactic types in the empty context.
  Type⇓ ‘Typeε’ Γ⇓ = Type ε
  -- ‘□’ expects Term of Type ‘Typeε’ as the last element of the
  -- context, and represents the type of Terms of that Type.  We take
  -- the (already-interpreted) last element of the Context, and feed
  -- it to Term {ε}, to get the Set of Terms of that Type.
  Type⇓ ‘□’ Γ⇓ = Term {ε} (Σ.proj₂ Γ⇓)
  -- The rest of the interpreter, for types not formally needed in
  -- Lӧb′s theorem.
  Type⇓ ‘⊤’ Γ⇓ = ⊤
  Type⇓ ‘⊥’ Γ⇓ = ⊥

  Term⇓ : ∀ {Γ : Context} {T : Type Γ} → Term T → (Γ⇓ : Context⇓ Γ) → Type⇓ T Γ⇓
  -- Unsurprisingly, we interpret the quotation of a given source code
  -- as the source code itself.  (Defining the interpretation of
  -- quotation is really trivial.  Defining quotation itself is much
  -- tricker.)  Note that it is, I believe, essential, that every Type
  -- be quotable.  Otherwise Lӧb′s theorem cannot be internalized in
  -- our syntactic representation, and will require both being given
  -- both a type, and syntax which denotes to that type.
  Term⇓ ⌜ x ⌝ Γ⇓ = x
  -- Now, the interesting part.  Given an interpreter (P in the poem,
  -- □‘X’→X in this code), we validate Lӧb′s theorem (Q run on Q) by
  -- running the interpreter on ... Q run on Q!  It takes a bit of
  -- thinking to wrap your head around, but the types line up, and
  -- it′s beautifully simple.
  Term⇓ (Lӧb □‘X’→X) Γ⇓ = Term⇓ □‘X’→X Γ⇓ (Lӧb □‘X’→X)
  -- Inhabiting ⊤
  Term⇓ ‘tt’ Γ⇓ = tt

⌞_⌟ : Type ε → Set _
⌞ T ⌟ = Type⇓ T tt

‘¬’_ : ∀ {Γ} → Type Γ → Type Γ
‘¬’ T = T ‘→’ ‘⊥’

-- With our interpreter, we can chain Lӧb′s theorem with itself: if we
-- can prove that ‶proving ‘X’ is sufficient to make ‘X’ true″, then
-- we can already inhabit X.
lӧb : ∀ {‘X’} → □ (‘□’ ‘’ ⌜ ‘X’ ⌝ ‘→’ ‘X’) → ⌞ ‘X’ ⌟
lӧb f = Term⇓ (Lӧb f) tt

-- We can thus prove that it′s impossible to prove that contradictions
-- are unprovable.
incompleteness : ¬ □ (‘¬’ (‘□’ ‘’ ⌜ ‘⊥’ ⌝))
incompleteness = lӧb

-- We can also prove that contradictions are, in fact, unprovable.
soundness : ¬ □ ‘⊥’
soundness x = Term⇓ x tt

-- And we can prove that some things are provable, namely, ‘⊤’
non-emptyness : Σ (Type ε) (λ T → □ T)
non-emptyness = ‘⊤’ , ‘tt’

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
open import Data.Product using ( _,_ ; proj₁ ; proj₂ )
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ )
open import Relation.Binary.PropositionalEquality using ( refl )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.ABox using ( ABox ; _,_ ; ⟨ABox⟩ )
open import Web.Semantic.DL.ABox.Interp using ( Interp ; _,_ ; ⌊_⌋ ; ind ; _*_ )
open import Web.Semantic.DL.ABox.Interp.Morphism using
  ( _≲_ ; _,_ ; ≲⌊_⌋ ; ≲-resp-ind ; _**_ ; ≡³-impl-≈ ; ≡³-impl-≲ )
open import Web.Semantic.DL.ABox.Model using
  ( _⊨a_ ; _⊨b_ ; bnodes ; on-bnode ; _,_
  ; ⟨ABox⟩-resp-⊨ ; ⊨a-resp-≲ ; *-resp-⟨ABox⟩ )
open import Web.Semantic.DL.Category.Morphism using
  ( _⇒_ ; _⇒_w/_ ; _,_ ; BN ; impl ; impl✓ )
open import Web.Semantic.DL.Category.Object using
  ( Object ; _,_ ; IN ; fin ; iface )
open import Web.Semantic.DL.Integrity using
  ( _⊕_⊨_ ; Unique ; Mediated ; Mediator ; Initial
  ; _,_ ; extension ; ext-init ; ext-⊨ ; ext✓ ; init-≲ )
open import Web.Semantic.DL.KB using ( _,_ )
open import Web.Semantic.DL.KB.Model using ( _⊨_ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox ; _,_ )
open import Web.Semantic.DL.TBox.Interp using
  ( Δ ; _⊨_≈_ ; ≈-refl ; ≈-sym ; ≈-trans )
open import Web.Semantic.DL.TBox.Model using ( _⊨t_ )
open import Web.Semantic.DL.TBox.Interp.Morphism using
  ( ≲-image ; ≲-resp-≈ ; ≲-trans ) renaming ( _≲_ to _≲′_ )
open import Web.Semantic.Util using
  ( _∘_ ; Finite ; ⊎-resp-Fin ; _⊕_⊕_ ; inode ; bnode ; enode ; up ; down ; vmerge )

module Web.Semantic.DL.Category.Tensor {Σ : Signature} where

_&_ : ∀ {X₁ X₂} → ABox Σ X₁ → ABox Σ X₂ → ABox Σ (X₁ ⊎ X₂)
A₁ & A₂ = (⟨ABox⟩ inj₁ A₁ , ⟨ABox⟩ inj₂ A₂)

_⊗_ : ∀ {S T : TBox Σ} → Object S T → Object S T →  Object S T
A₁ ⊗ A₂ =
  ( (IN A₁ ⊎ IN A₂)
  , ⊎-resp-Fin (fin A₁) (fin A₂)
  , iface A₁ & iface A₂ )

_⟨&⟩_ : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} →
  ABox Σ (X₁ ⊕ V₁ ⊕ Y₁) → ABox Σ (X₂ ⊕ V₂ ⊕ Y₂) →
    ABox Σ ((X₁ ⊎ X₂) ⊕ (V₁ ⊎ V₂) ⊕ (Y₁ ⊎ Y₂))
F₁ ⟨&⟩ F₂ = (⟨ABox⟩ up F₁ , ⟨ABox⟩ down F₂)

⊨a-intro-⟨&⟩ : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} →
  (I : Interp Σ ((X₁ ⊎ X₂) ⊕ (V₁ ⊎ V₂) ⊕ (Y₁ ⊎ Y₂))) →
    (F₁ : ABox Σ (X₁ ⊕ V₁ ⊕ Y₁)) → (F₂ : ABox Σ (X₂ ⊕ V₂ ⊕ Y₂)) →
      (up * I ⊨a F₁) → (down * I ⊨a F₂) → (I ⊨a F₁ ⟨&⟩ F₂)
⊨a-intro-⟨&⟩ (I , i) F₁ F₂ I₁⊨F₁ I₂⊨F₂ =
  ( ⟨ABox⟩-resp-⊨ up (λ x → ≈-refl I) F₁ I₁⊨F₁
  , ⟨ABox⟩-resp-⊨ down (λ x → ≈-refl I) F₂ I₂⊨F₂ )

⊨b-intro-⟨&⟩ : ∀ {V₁ V₂ W₁ W₂ X₁ X₂ Y₁ Y₂} →
  (I : Interp Σ ((X₁ ⊎ X₂) ⊕ (W₁ ⊎ W₂) ⊕ (Y₁ ⊎ Y₂))) →
    (F₁ : ABox Σ (X₁ ⊕ V₁ ⊕ Y₁)) → (F₂ : ABox Σ (X₂ ⊕ V₂ ⊕ Y₂)) →
      (up * I ⊨b F₁) → (down * I ⊨b F₂) → (I ⊨b F₁ ⟨&⟩ F₂)
⊨b-intro-⟨&⟩ {V₁} {V₂} I F₁ F₂ (f₁ , I₁⊨F₁) (f₂ , I₂⊨F₂) =
  (f , I⊨F₁F₂) where

  f : (V₁ ⊎ V₂) → Δ ⌊ I ⌋
  f (inj₁ v) = f₁ v
  f (inj₂ v) = f₂ v

  I⊨F₁F₂ : bnodes I f ⊨a F₁ ⟨&⟩ F₂
  I⊨F₁F₂ =
    ( ⟨ABox⟩-resp-⊨ up
        (≡³-impl-≈ ⌊ I ⌋ (on-bnode f₁ (ind I ∘ up))
          (on-bnode f (ind I) ∘ up) refl)
        F₁ I₁⊨F₁
    , ⟨ABox⟩-resp-⊨ down
        (≡³-impl-≈ ⌊ I ⌋ (on-bnode f₂ (ind I ∘ down))
          (on-bnode f (ind I) ∘ down) refl)
        F₂ I₂⊨F₂ )

go₂ : ∀ {V₁ X₁ X₂ Y₁} → (I : Interp Σ (X₁ ⊎ X₂)) →
  (J₁ : Interp Σ (X₁ ⊕ V₁ ⊕ Y₁)) → (⌊ I ⌋ ≲′ ⌊ J₁ ⌋) →
    Interp Σ X₂
go₂ I J₁ I≲J = (⌊ J₁ ⌋ , ≲-image I≲J ∘ ind I ∘ inj₂)

go₂-≳ : ∀ {V₁ X₁ X₂ Y₁} → (I : Interp Σ (X₁ ⊎ X₂)) →
  (J₁ : Interp Σ (X₁ ⊕ V₁ ⊕ Y₁)) → (I≲J : ⌊ I ⌋ ≲′ ⌊ J₁ ⌋) →
    (inj₂ * I ≲ go₂ I J₁ I≲J)
go₂-≳ I (J , j₁) I≲J = (I≲J , λ x → ≈-refl J)

go₂-≲ : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} → (I : Interp Σ (X₁ ⊎ X₂)) →
  (J₁ : Interp Σ (X₁ ⊕ V₁ ⊕ Y₁)) →
    (L : Interp Σ ((X₁ ⊎ X₂) ⊕ (V₁ ⊎ V₂) ⊕ (Y₁ ⊎ Y₂))) →
      (I₁≲J₁ : inj₁ * I ≲ inode * J₁) → (I≲L : I ≲ inode * L) →
        (Mediated (inj₁ * I) J₁ (up * L) I₁≲J₁ (inj₁ ** I≲L)) →
          (go₂ I J₁ ≲⌊ I₁≲J₁ ⌋ ≲ inode * (down * L))
go₂-≲ (I , i) (J , j₁) (L , l) (I≲J , i₁≲j₁) (I≲L , i≲l)
  ((J≲L , j₁≲l₁) , I≲L≋I≲J≲L , J₁≲L₁-uniq) =
    (J≲L , λ x → ≈-trans L (≈-sym L (I≲L≋I≲J≲L (i (inj₂ x)))) (i≲l (inj₂ x)))

par : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} → (J₁ : Interp Σ (X₁ ⊕ V₁ ⊕ Y₁)) →
  (K₂ : Interp Σ (X₂ ⊕ V₂ ⊕ Y₂)) → (⌊ J₁ ⌋ ≲′ ⌊ K₂ ⌋) →
    Interp Σ ((X₁ ⊎ X₂) ⊕ (V₁ ⊎ V₂) ⊕ (Y₁ ⊎ Y₂))
par J₁ K₂ J≲K =
  (⌊ K₂ ⌋ , vmerge (≲-image J≲K ∘ ind J₁) (ind K₂))

par-inj₁ : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} → (J₁ : Interp Σ (X₁ ⊕ V₁ ⊕ Y₁)) →
  (K₂ : Interp Σ (X₂ ⊕ V₂ ⊕ Y₂)) → (J≲K : ⌊ J₁ ⌋ ≲′ ⌊ K₂ ⌋) →
    (J₁ ≲ up * par J₁ K₂ J≲K)
par-inj₁ (J , j₁) (K , k₂) J≲K =
  ( J≲K
  , ≡³-impl-≈ K
      (≲-image J≲K ∘ j₁)
      (vmerge (≲-image J≲K ∘ j₁) k₂ ∘ up)
      refl )

par-inj₂ : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} → (J₁ : Interp Σ (X₁ ⊕ V₁ ⊕ Y₁)) →
  (K₂ : Interp Σ (X₂ ⊕ V₂ ⊕ Y₂)) → (J≲K : ⌊ J₁ ⌋ ≲′ ⌊ K₂ ⌋) →
    (K₂ ≲ down * par J₁ K₂ J≲K)
par-inj₂ (J , j₁) (K , k₂) J≲K =
  ≡³-impl-≲ (K , k₂) (vmerge (≲-image J≲K ∘ j₁) k₂ ∘ down) refl

par-exp : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} → (J₁ : Interp Σ (X₁ ⊕ V₁ ⊕ Y₁)) →
  (K₂ : Interp Σ (X₂ ⊕ V₂ ⊕ Y₂)) → (J≲K : ⌊ J₁ ⌋ ≲′ ⌊ K₂ ⌋) →
    (T : TBox Σ) → (B₁ : ABox Σ Y₁) → (B₂ : ABox Σ Y₂) →
      (enode * J₁ ⊨ T , B₁) → (enode * K₂ ⊨ T , B₂) →
        (enode * (par J₁ K₂ J≲K) ⊨ T , (B₁ & B₂))
par-exp J₁ K₂ J≲K T B₁ B₂ (J⊨T , J₁⊨B₁) (K⊨T , K₂⊨B₂) =
  ( K⊨T
  , ⟨ABox⟩-resp-⊨ inj₁ (λ y → ≈-refl ⌊ K₂ ⌋) B₁
      (⊨a-resp-≲ (enode ** par-inj₁ J₁ K₂ J≲K) B₁ J₁⊨B₁)
  , ⟨ABox⟩-resp-⊨ inj₂ (λ y → ≈-refl ⌊ K₂ ⌋) B₂ K₂⊨B₂)

par-≳ : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} → (I : Interp Σ (X₁ ⊎ X₂)) →
  (J₁ : Interp Σ (X₁ ⊕ V₁ ⊕ Y₁)) → (K₂ : Interp Σ (X₂ ⊕ V₂ ⊕ Y₂)) →
    (I₁≲J₁ : inj₁ * I ≲ inode * J₁) →
      (J₂≲K₂ : go₂ I J₁ ≲⌊ I₁≲J₁ ⌋ ≲ inode * K₂) →
        (I ≲ inode * par J₁ K₂ ≲⌊ J₂≲K₂ ⌋)
par-≳ I J₁ K₂ (I≲J , i₁≲j₁) (J≲K , j₂≲k₂) =
  ( ≲-trans I≲J J≲K , lemma ) where

  lemma : ∀ x → ⌊ K₂ ⌋ ⊨
    ≲-image J≲K (≲-image I≲J (ind I x)) ≈
      vmerge (≲-image J≲K ∘ ind J₁) (ind K₂) (inode x)
  lemma (inj₁ x) = ≲-resp-≈ J≲K (i₁≲j₁ x)
  lemma (inj₂ x) = j₂≲k₂ x

par-impl : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} → (J₁ : Interp Σ (X₁ ⊕ V₁ ⊕ Y₁)) →
  (K₂ : Interp Σ (X₂ ⊕ V₂ ⊕ Y₂)) → (J≲K : ⌊ J₁ ⌋ ≲′ ⌊ K₂ ⌋) →
    (F₁ : ABox Σ (X₁ ⊕ V₁ ⊕ Y₁)) → (F₂ : ABox Σ (X₂ ⊕ V₂ ⊕ Y₂)) →
      (J₁ ⊨a F₁) → (K₂ ⊨a F₂) →
        (par J₁ K₂ J≲K ⊨a F₁ ⟨&⟩ F₂)
par-impl J₁ K₂ J≲K F₁ F₂ J₁⊨F₁ K₂⊨F₂ =
  ( ⟨ABox⟩-resp-⊨ up (λ x → ≈-refl ⌊ K₂ ⌋) F₁
      (⊨a-resp-≲ (par-inj₁ J₁ K₂ J≲K) F₁ J₁⊨F₁)
  , ⟨ABox⟩-resp-⊨ down (λ x → ≈-refl ⌊ K₂ ⌋) F₂
      (⊨a-resp-≲ (par-inj₂ J₁ K₂ J≲K) F₂ K₂⊨F₂) )

par-mediated : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} → (I : Interp Σ (X₁ ⊎ X₂)) →
  (J₁ : Interp Σ (X₁ ⊕ V₁ ⊕ Y₁)) → (K₂ : Interp Σ (X₂ ⊕ V₂ ⊕ Y₂)) →
    (L : Interp Σ ((X₁ ⊎ X₂) ⊕ (V₁ ⊎ V₂) ⊕ (Y₁ ⊎ Y₂))) →
      (I₁≲J₁ : inj₁ * I ≲ inode * J₁) → (I≲L : I ≲ inode * L) →
        (J₂≲K₂ : go₂ I J₁ ≲⌊ I₁≲J₁ ⌋ ≲ inode * K₂) →
          (m : Mediated (inj₁ * I) J₁ (up * L) I₁≲J₁ (inj₁ ** I≲L)) →
            (Mediated (go₂ I J₁ ≲⌊ I₁≲J₁ ⌋) K₂ (down * L) J₂≲K₂ (go₂-≲ I J₁ L I₁≲J₁ I≲L m)) →
              (Mediated I (par J₁ K₂ ≲⌊ J₂≲K₂ ⌋) L (par-≳ I J₁ K₂ I₁≲J₁ J₂≲K₂) I≲L)
par-mediated (I , i) (J , j₁) (K , k₂) (L , l) (I≲J , i₁≲j₁) (I≲L , i≲l) (J≲K , j₂≲k₂)
  ((J≲L , j₁≲l₁) , I≲L≋I≲J≲L , J₁≲L₁-uniq) ((K≲L , k₂≲l₂) , J≲L≋J≲K≲L , K₂≲L₂-uniq) =
    ((K≲L , k≲l) , I≲L≋I≲K≲L , K≲L-uniq) where

  k = vmerge (≲-image J≲K ∘ j₁) k₂

  I≲K : I ≲′ K
  I≲K = ≲-trans I≲J J≲K

  i≲k : ∀ x → K ⊨ ≲-image I≲K (i x) ≈ k (inode x)
  i≲k = ≲-resp-ind (par-≳ (I , i) (J , j₁) (K , k₂) (I≲J , i₁≲j₁) (J≲K , j₂≲k₂))

  k≲l : ∀ x → L ⊨ ≲-image K≲L (k x) ≈ l x
  k≲l (inode (inj₁ x)) = ≈-trans L (≈-sym L (J≲L≋J≲K≲L (j₁ (inode x)))) (j₁≲l₁ (inode x))
  k≲l (inode (inj₂ x)) = k₂≲l₂ (inode x)
  k≲l (bnode (inj₁ v)) = ≈-trans L (≈-sym L (J≲L≋J≲K≲L (j₁ (bnode v)))) (j₁≲l₁ (bnode v))
  k≲l (bnode (inj₂ v)) = k₂≲l₂ (bnode v)
  k≲l (enode (inj₁ y)) = ≈-trans L (≈-sym L (J≲L≋J≲K≲L (j₁ (enode y)))) (j₁≲l₁ (enode y))
  k≲l (enode (inj₂ y)) = k₂≲l₂ (enode y)

  I≲L≋I≲K≲L : ∀ x → L ⊨ ≲-image I≲L x ≈ ≲-image K≲L (≲-image I≲K x)
  I≲L≋I≲K≲L x = ≈-trans L (I≲L≋I≲J≲L x) (J≲L≋J≲K≲L (≲-image I≲J x))

  lemma₁ : ∀ (K≲L : (K , k) ≲ (L , l)) x → (L ⊨ ≲-image ≲⌊ K≲L ⌋ (≲-image J≲K (j₁ x)) ≈ l (up x))
  lemma₁ (K≲L' , k≲l) (inode x) = k≲l (inode (inj₁ x))
  lemma₁ (K≲L' , k≲l) (bnode v) = k≲l (bnode (inj₁ v))
  lemma₁ (K≲L' , k≲l) (enode y) = k≲l (enode (inj₁ y))

  lemma₂ : ∀ (K≲L : (K , k) ≲ (L , l)) x → (L ⊨ ≲-image ≲⌊ K≲L ⌋ (k₂ x) ≈ l (down x))
  lemma₂ (K≲L , k≲l) (inode x) = k≲l (inode (inj₂ x))
  lemma₂ (K≲L , k≲l) (bnode v) = k≲l (bnode (inj₂ v))
  lemma₂ (K≲L , k≲l) (enode y) = k≲l (enode (inj₂ y))

  K≲L-uniq : Unique (I , i) (K , k) (L , l) (I≲K , i≲k) (I≲L , i≲l)
  K≲L-uniq (K≲₁L , k≲₁l) (K≲₂L , k≲₂l) I≲L≋I≲K≲₁L I≲L≋I≲K≲₂L =
    K₂≲L₂-uniq (K≲₁L , lemma₂ (K≲₁L , k≲₁l)) (K≲₂L , lemma₂ (K≲₂L , k≲₂l))
      (J₁≲L₁-uniq (J≲L , j₁≲l₁) (≲-trans J≲K K≲₁L , lemma₁ (K≲₁L , k≲₁l)) I≲L≋I≲J≲L I≲L≋I≲K≲₁L)
      (J₁≲L₁-uniq (J≲L , j₁≲l₁) (≲-trans J≲K K≲₂L , lemma₁ (K≲₂L , k≲₂l)) I≲L≋I≲J≲L I≲L≋I≲K≲₂L)

par-mediator : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} → (I : Interp Σ (X₁ ⊎ X₂)) →
  (J₁ : Interp Σ (X₁ ⊕ V₁ ⊕ Y₁)) → (K₂ : Interp Σ (X₂ ⊕ V₂ ⊕ Y₂)) →
    (I₁≲J₁ : inj₁ * I ≲ inode * J₁) →
      (J₂≲K₂ : go₂ I J₁ ≲⌊ I₁≲J₁ ⌋ ≲ inode * K₂) → (S : TBox Σ) →
        (F₁ : ABox Σ (X₁ ⊕ V₁ ⊕ Y₁)) → (F₂ : ABox Σ (X₂ ⊕ V₂ ⊕ Y₂)) →
          (Mediator (inj₁ * I) J₁ I₁≲J₁ (S , F₁)) →
            (Mediator (go₂ I J₁ ≲⌊ I₁≲J₁ ⌋) K₂ J₂≲K₂ (S , F₂)) →
              (Mediator I (par J₁ K₂ ≲⌊ J₂≲K₂ ⌋)
                (par-≳ I J₁ K₂ I₁≲J₁ J₂≲K₂) (S , (F₁ ⟨&⟩ F₂)))
par-mediator I J₁ K₂ I₁≲J₁ J₂≲K₂ S F₁ F₂ J₁-med K₂-med L I≲L (L⊨S , L⊨F₁ , L⊨F₂) =
  par-mediated I J₁ K₂ L I₁≲J₁ I≲L J₂≲K₂ I₁≲J₁≲L₁-med J₂≲K₂≲L₂-med where

  I₁≲J₁≲L₁-med : Mediated (inj₁ * I) J₁ (up * L) I₁≲J₁ (inj₁ ** I≲L)
  I₁≲J₁≲L₁-med = J₁-med (up * L) (inj₁ ** I≲L) (L⊨S , *-resp-⟨ABox⟩ up L F₁ L⊨F₁)

  J₂≲K₂≲L₂-med : Mediated (go₂ I J₁ ≲⌊ I₁≲J₁ ⌋) K₂ (down * L) J₂≲K₂ (go₂-≲ I J₁ L I₁≲J₁ I≲L I₁≲J₁≲L₁-med)
  J₂≲K₂≲L₂-med = K₂-med (down * L) (go₂-≲ I J₁ L I₁≲J₁ I≲L I₁≲J₁≲L₁-med) (L⊨S , *-resp-⟨ABox⟩ down L F₂ L⊨F₂)

par-init : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} → (I : Interp Σ (X₁ ⊎ X₂)) →
  (J₁ : Interp Σ (X₁ ⊕ V₁ ⊕ Y₁)) → (K₂ : Interp Σ (X₂ ⊕ V₂ ⊕ Y₂)) →
    (S : TBox Σ) → (F₁ : ABox Σ (X₁ ⊕ V₁ ⊕ Y₁)) → (F₂ : ABox Σ (X₂ ⊕ V₂ ⊕ Y₂)) →
      (J₁-init : J₁ ∈ Initial (inj₁ * I) (S , F₁)) →
        (K₂-init : K₂ ∈ Initial (go₂ I J₁ ≲⌊ init-≲ J₁-init ⌋) (S , F₂)) →
          (par J₁ K₂ ≲⌊ init-≲ K₂-init ⌋ ∈
            Initial I (S , (F₁ ⟨&⟩ F₂)))
par-init I J₁ K₂ S F₁ F₂
  (I₁≲J₁ , (J⊨S , J₁⊨F₁) , J₁-med) (J₂≲K₂ , (K⊨S , K₂⊨F₂) , K₂-med) =
    ( par-≳ I J₁ K₂ I₁≲J₁ J₂≲K₂
    , (K⊨S , par-impl J₁ K₂ ≲⌊ J₂≲K₂ ⌋ F₁ F₂ J₁⊨F₁ K₂⊨F₂)
    , par-mediator I J₁ K₂ I₁≲J₁ J₂≲K₂ S F₁ F₂ J₁-med K₂-med )

tensor-⊨ : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} → (S T : TBox Σ) →
  (A₁ : ABox Σ X₁) → (A₂ : ABox Σ X₂) → (B₁ : ABox Σ Y₁) → (B₂ : ABox Σ Y₂) →
    (F₁ : ABox Σ (X₁ ⊕ V₁ ⊕ Y₁)) (F₂ : ABox Σ (X₂ ⊕ V₂ ⊕ Y₂)) →
      (∀ I → (I ⊨ (S , T) , A₁) → (I ⊕ S , F₁ ⊨ T , B₁)) →
        (∀ I → (I ⊨ (S , T) , A₂) → (I ⊕ S , F₂ ⊨ T , B₂)) →
          (∀ I → (I ⊨ (S , T) , (A₁ & A₂)) →
            (I ⊕ S , F₁ ⟨&⟩ F₂ ⊨ T , (B₁ & B₂)))
tensor-⊨ {V₁} {V₂} {X₁} {X₂} {Y₁} {Y₂}
  S T A₁ A₂ B₁ B₂ F₁ F₂ F₁✓ F₂✓ I (I⊨ST , (I⊨A₁ , I⊨A₂)) =
    ( par J₁ K₂ ≲⌊ J₂≲K₂ ⌋
    , par-init I J₁ K₂ S F₁ F₂ J₁-init K₂-init
    , par-exp J₁ K₂ ≲⌊ J₂≲K₂ ⌋ T B₁ B₂
        (ext-⊨ I₁⊕SF₁⊨TB₁) (ext-⊨ J₂⊕SF₂⊨TB₂) ) where

  I₁ : Interp Σ X₁
  I₁ = inj₁ * I

  I₂ : Interp Σ X₂
  I₂ = inj₂ * I

  I₁⊨A₁ : I₁ ⊨a A₁
  I₁⊨A₁ = *-resp-⟨ABox⟩ inj₁ I A₁ I⊨A₁

  I₂⊨A₂ : I₂ ⊨a A₂
  I₂⊨A₂ = *-resp-⟨ABox⟩ inj₂ I A₂ I⊨A₂

  I₁⊕SF₁⊨TB₁ : I₁ ⊕ S , F₁ ⊨ T , B₁
  I₁⊕SF₁⊨TB₁ = F₁✓ I₁ (I⊨ST , I₁⊨A₁)

  J₁ : Interp Σ (X₁ ⊕ V₁ ⊕ Y₁)
  J₁ = extension I₁⊕SF₁⊨TB₁

  J₁-init : J₁ ∈ Initial I₁ (S , F₁)
  J₁-init = ext-init I₁⊕SF₁⊨TB₁

  I₁≲J₁ : I₁ ≲ inode * J₁
  I₁≲J₁ = init-≲ J₁-init

  J₂ : Interp Σ X₂
  J₂ = go₂ I J₁ ≲⌊ I₁≲J₁ ⌋

  I₂≲J₂ : I₂ ≲ J₂
  I₂≲J₂ = go₂-≳ I J₁ ≲⌊ I₁≲J₁ ⌋

  J⊨ST : ⌊ J₂ ⌋ ⊨t (S , T)
  J⊨ST = proj₁ (ext✓ I₁⊕SF₁⊨TB₁)

  J₂⊨A₂ : J₂ ⊨a A₂
  J₂⊨A₂ = ⊨a-resp-≲ I₂≲J₂ A₂ I₂⊨A₂

  J₂⊕SF₂⊨TB₂ : J₂ ⊕ S , F₂ ⊨ T , B₂
  J₂⊕SF₂⊨TB₂ = F₂✓ J₂ (J⊨ST , J₂⊨A₂)

  K₂ : Interp Σ (X₂ ⊕ V₂ ⊕ Y₂)
  K₂ = extension J₂⊕SF₂⊨TB₂

  K₂-init : K₂ ∈ Initial J₂ (S , F₂)
  K₂-init = ext-init J₂⊕SF₂⊨TB₂

  J₂≲K₂ : J₂ ≲ inode * K₂
  J₂≲K₂ = init-≲ K₂-init

_⟨⊗⟩′_ : ∀ {S T : TBox Σ} {A₁ A₂ B₁ B₂ : Object S T} →
  (F₁ : A₁ ⇒ B₁) → (F₂ : A₂ ⇒ B₂) →
    ((A₁ ⊗ A₂) ⇒ (B₁ ⊗ B₂) w/ (BN F₁ ⊎ BN F₂))
_⟨⊗⟩′_ {S} {T} {X₁ , X₁∈Fin , A₁} {X₂ , X₂∈Fin , A₂} {Y₁ , Y₁∈Fin , B₁} {Y₂ , Y₂∈Fin , B₂}
  (V₁ , F₁ , F₁✓) (V₂ , F₂ , F₂✓) =
    (F₁ ⟨&⟩ F₂ , tensor-⊨ S T A₁ A₂ B₁ B₂ F₁ F₂ F₁✓ F₂✓)

_⟨⊗⟩_ : ∀ {S T : TBox Σ} {A₁ A₂ B₁ B₂ : Object S T} →
  (A₁ ⇒ B₁) → (A₂ ⇒ B₂) → ((A₁ ⊗ A₂) ⇒ (B₁ ⊗ B₂))
F₁ ⟨⊗⟩ F₂  = ( (BN F₁ ⊎ BN F₂) , F₁ ⟨⊗⟩′ F₂ )

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
open import Relation.Ternary.Separation

module Relation.Ternary.Separation.Monad.CompleteUpdate
  {a} {A : Set a} {{r : RawSep A}} {u} {{ s : IsUnitalSep r u }}
  where

open import Function
open import Level hiding (Lift)
open import Data.Product
open import Data.Unit using (⊤)

open import Relation.Unary
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Binary hiding (_⇒_)
open import Relation.Binary.PropositionalEquality as P

open import Relation.Ternary.Separation.Morphisms
open import Relation.Ternary.Separation.Monad
open import Relation.Ternary.Separation.Construct.Product
open import Relation.Ternary.Separation.Construct.Market

open Monads {{ bs = record { Carrier = A × A } }} (id-morph (A × A))
open ⟰_

module Update where
  private bind' : ∀ {p q} {P : Pred (A × A) p} {Q : Pred (A × A) q} → ∀[ (P ─✴ ⟰ Q) ⇒ (⟰ P ─✴ ⟰ Q) ]
  updater (app (bind' f) c σ) fr with ⊎-assoc (⊎-comm σ) fr
  ... | xs , σ₂ , σ₃ with updater c σ₂
  ... | ys , zs , σ₄ , px with ⊎-unassoc σ₄ σ₃
  ... | _ , σ₅ , σ₆ = updater (app f px (⊎-comm σ₅)) σ₆

  ⟰-monad : Monad ⊤ a (λ _ _ → ⟰_)
  updater (Monad.return ⟰-monad px) fr = -, -, fr , px
  Monad.bind ⟰-monad = bind'

{- updates with failure -}
module UpdateWithFailure where

  open import Relation.Ternary.Separation.Monad.Error
  open import Data.Sum

  ⟰? : Pt (A × A) a
  ⟰? P = ⟰ (Err P)

  instance ⟰?-monad : Monad ⊤ a (λ _ _ → ⟰?)
  Monad.return ⟰?-monad px = Monad.return Update.⟰-monad (return px)
  updater (app (Monad.bind ⟰?-monad f) m σ) fr with ⊎-assoc (⊎-comm σ) fr
  ... | _ , σ₂ , σ₃ with updater m σ₂
  ... | _ , _ , τ₁ , error  = -, -, fr , error
  ... | _ , _ , τ₁ , partial (inj₂ v) with ⊎-unassoc τ₁ σ₃
  ... | _ , τ₃ , τ₄ = updater (app f v (⊎-comm τ₃)) τ₄

  ⟰error : ∀ P → ∀[ ⟰? P ]
  updater (⟰error _) fr = -, -, fr , error


text:
--{-# OPTIONS --verbose 10 #-}
open import ExtractSac as ES using ()
open import Extract (ES.kompile-fun)

open import Data.Nat as N using (ℕ; zero; suc; _≤_; _≥_; _<_; s≤s; z≤n)
import      Data.Nat.DivMod as N
open import Data.Nat.Properties as N
open import Data.List as L using (List; []; _∷_)
open import Data.Vec as V using (Vec; []; _∷_)
import      Data.Vec.Properties as V
open import Data.Fin as F using (Fin; zero; suc; #_)
import      Data.Fin.Properties as F
open import Data.Product as Prod using (Σ; _,_; curry; uncurry) renaming (_×_ to _⊗_)

open import Relation.Binary.PropositionalEquality

open import Reflection

open import Structures
open import Function
open import ReflHelper

open import Array.Base
open import Array.Properties

open import APL2

open import Agda.Builtin.Float

-- Verbose facts about transitivity of <, ≤, and ≡
a≤b⇒b≡c⇒a≤c : ∀ {a b c} → a ≤ b → b ≡ c → a ≤ c
a≤b⇒b≡c⇒a≤c a≤b refl = a≤b

a≤b⇒a≡c⇒b≡d⇒c≤d : ∀ {a b c d} → a ≤ b → a ≡ c → b ≡ d → c ≤ d
a≤b⇒a≡c⇒b≡d⇒c≤d a≤b refl refl = a≤b

a<b⇒0<b : ∀ {a b} → a < b → zero < b
a<b⇒0<b {a} a<b = ≤-trans (s≤s z≤n) a<b

a<b⇒c≤a⇒c<b : ∀ {a b c} → a < b → c ≤ a → c < b
a<b⇒c≤a⇒c<b a<b z≤n = a<b⇒0<b a<b
a<b⇒c≤a⇒c<b (s≤s a<b) (s≤s c≤a) = s≤s (a<b⇒c≤a⇒c<b a<b c≤a)

a≤b⇒c≤a⇒c≤b : ∀ {a b c} → a ≤ b → c ≤ a → c ≤ b
a≤b⇒c≤a⇒c≤b {a} {b} {c} a≤b c≤a = ≤-trans c≤a a≤b

A<B⇒B≤C⇒A≤C : ∀ {n}{ix s s₁ : Ar ℕ 1 (n ∷ [])}
             → ix <a s → s₁ ≥a s → s₁ ≥a ix
A<B⇒B≤C⇒A≤C {ix = imap x} {imap x₁} {imap x₂} ix<s ix≤s₁ iv = ≤-trans (<⇒≤ $ ix<s iv) (ix≤s₁ iv)

A≥B⇒A≡C⇒C≥B : ∀ {d s}{A B C : Ar ℕ d s}
             → A ≥a B → A =a C → C ≥a B
A≥B⇒A≡C⇒C≥B {A = imap x} {imap x₁} {imap x₂} A≥B A≡C iv rewrite (sym $ A≡C iv) = A≥B iv

-- Something that could go in Stdlib.

a≤a*b : ∀ {a b} → a ≤ a N.* suc b
a≤a*b {a} {b = zero} rewrite (*-identityʳ a) = ≤-refl
a≤a*b {a} {b = suc b} = ≤-trans a≤a*b (*-monoʳ-≤ a (≤-step ≤-refl))

a-s[b]+1≡a-b : ∀ {a b} → b < a →  a N.∸ suc b N.+ 1 ≡ a N.∸ b
a-s[b]+1≡a-b {a} {b} pf = begin
                     a N.∸ suc (b) N.+ 1  ≡⟨ sym $ N.+-∸-comm 1 pf ⟩
                     a N.+ 1 N.∸ suc b    ≡⟨ cong₂ N._∸_ (N.+-comm a 1) (refl {x = suc b}) ⟩
                     a N.∸ b
                   ∎
                   where open ≡-Reasoning

conv-ix-inb : ∀ {n}{ix s s₁ : Ar ℕ 1 (n ∷ [])}
            → (ix<s : ix <a s)
            → (s₁≥s : s₁ ≥a s)
            → (s₁ - ix) {≥ = A<B⇒B≤C⇒A≤C {s₁ = s₁} ix<s s₁≥s}
               ≥a ((s₁ - s) {≥ = s₁≥s} + ( 1))
conv-ix-inb {ix = imap ix} {imap s} {imap s₁} ix<s s₁≥s iv =
       let
         s₁-[1+ix]≥s₁-s = ∸-monoʳ-≤ (s₁ iv) (ix<s iv)
         s₁-[1+ix]+1≥s₁-s+1 = +-monoˡ-≤ 1 s₁-[1+ix]≥s₁-s
       in a≤b⇒b≡c⇒a≤c s₁-[1+ix]+1≥s₁-s+1 (a-s[b]+1≡a-b {a = s₁ iv} {b = ix iv} (≤-trans (ix<s iv) (s₁≥s iv)))

undo-lkptab : ∀ {n s₁}{ix : Ar ℕ 1 (n ∷ [])} (iv : Ix 1 (n ∷ [])) →
      V.lookup s₁ (ix-lookup iv zero) N.∸ sel ix iv ≡
      V.lookup (V.tabulate (λ i → V.lookup s₁ i N.∸ sel ix (i ∷ [])))
      (ix-lookup iv zero)
undo-lkptab {s₁ = s₁}{ix} (i ∷ []) = sym (V.lookup∘tabulate _ i)

-- conv ← {a←⍵ ⋄ w←⍺ ⋄ ⊃+/,w×{(1+(⍴a)-⍴w)↑⍵↓a}¨⍳⍴w}
infixr 20 _conv_
_conv_ : ∀ {n wₛ aₛ}
      → Ar Float n wₛ
      → Ar Float n aₛ
      → {≥ : ▴ aₛ ≥a ▴ wₛ}
      → Ar Float n $ ▾ ((aₛ - wₛ){≥} + 1)
_conv_ {n = n} {wₛ = s} {aₛ = s₁} w a {s₁≥s} = let
               sr = (s₁ - s) {≥ = s₁≥s} + 1
               idxs = ι ρ w

               rots ix ix<s = let
                  ~ix≥ρa = A<B⇒B≤C⇒A≤C ix<s s₁≥s
                  ix↓a = (ix ↓ a) {pf = ~ix≥ρa}
                  ~ix-inb = conv-ix-inb {s₁ = s→a s₁} ix<s s₁≥s
                  ~ρix↓a≥sr = A≥B⇒A≡C⇒C≥B ~ix-inb (undo-lkptab {s₁ = s₁}{ix = ix})
                  in
                  (sr ↑ ix↓a) {pf = ~ρix↓a≥sr }

               r = (uncurry rots) ̈ idxs
               mul = w ̈⟨ _×ᵣ_ ⟩ (subst-ar (a→s∘s→a s) r)
               res = reduce-1d _+ᵣ_ (cst 0.0) (, mul)
              in res

--kconv : Prog
kconv = kompile _conv_ (quote _≥a_ ∷ quote reduce-1d ∷ quote _↑_ ∷ quote _↓_ ∷ []) [] -- (quote reduce-1d ∷ [])
--kconvr = frefl _conv_ (quote _≥a_ ∷ quote reduce-1d ∷ quote _↑_ ∷ quote _↓_ ∷ [])

--kconvr = frefl _conv_ (quote _≥a_ ∷ quote reduce-1d ∷ [])

--ktake : Term
--ktake = frefl _↑_ (quote _≥a_ ∷ quote reduce-1d ∷ [])

test-lw : ℕ → ℕ
test-lw n = case n of λ where
  1 → n N.+ 5
  _ → n N.+ 6

--ktest-lw = frefl test-lw []

n≤sn-i : ∀ {i n} → i N.≤ 1 → n N.≤ suc n N.∸ i
n≤sn-i z≤n       = <⇒≤ N.≤-refl
n≤sn-i (s≤s z≤n) = N.≤-refl

--test-take : ∀ {n} → Ix 1 V.[ 2 ] → Ar ℕ 1 V.[ 1 N.+ n ] → Ar ℕ 1 V.[ n ]
--test-take {n} ix@(i ∷ []) a =
--                 let ixₐ , ix<[2] = ix→a ix
--                     r' = (ixₐ   ↓ a)   {λ where jv@(zero ∷ []) → N.≤-trans (≤-pred $ ix<[2] jv) (s≤s z≤n)}
--                     r  = (cst n ↑ r')  {λ where jv@(zero ∷ []) → n≤sn-i (≤-pred $ F.toℕ<n i) }
--                 in r

test-take : ∀ {n} → Ix 1 V.[ 2 ] → Ar ℕ 1 V.[ 1 N.+ n ] → Ar ℕ 1 V.[ n ]
test-take {n} ix@(i ∷ []) a = r
  where
    ixₐ    = Prod.proj₁ $ ix→a ix
    ix<[2] = Prod.proj₂ $ ix→a ix
    r' = (ixₐ   ↓ a)   {λ where jv@(zero ∷ []) → N.≤-trans (≤-pred $ ix<[2] jv) (s≤s z≤n)}
    r  = (cst n ↑ r')  {λ where jv@(zero ∷ []) → n≤sn-i (≤-pred $ F.toℕ<n i) }

-- XXX These guys cause an impossible state.
--ktestr = frefl test-take []

--ktest : Prog
--ktest = kompile test-take (quote _≥a_ ∷ quote reduce-1d ∷ quote N._≟_ ∷ quote prod ∷ quote _↑_ ∷ quote _↓_ ∷ []) []

-- multiconv←{(a ws bs)←⍵⋄bs{⍺+⍵ conv a}⍤(0,(⍴⍴a))⊢ws}
multiconv : ∀ {n m s sw so} → (a : Ar Float n s)
          →  (ws : Ar (Ar Float n sw) m so)
          →  (bs : Ar Float m so)
          →  {≥ : ▴ s ≥a ▴ sw}
          →  Ar (Ar Float n $ ▾ ((s - sw){≥} + 1)) m so
multiconv a ws bs {≥} = bs ̈⟨ (λ α ω → α +ᵣ (ω conv a){≥}) ⟩ ws

--kmconv = kompile multiconv (quote _≥a_ ∷ quote reduce-1d ∷ quote _↑_ ∷ quote _↓_ ∷ []) [] -- (quote reduce-1d ∷ [])

{-

takeN : ∀ {n s}
      → (sh : Ar ℕ 1 (n ∷ []))
      → (a : Ar ℕ n s)
      → {pf : s→a s ≥a sh}
      → Ar ℕ n $ a→s sh
takeN sh a {pf} = (sh ↑ a){pf}

module _ where
  open import Relation.Nullary

  dec-test : ∀ {n} → (sh : Ar ℕ 1 V.[ n ]) → Ar ℕ n (▾ sh)
  dec-test a with (prod $ a→s a) N.≟ 0
  ... | yes p = mkempty _ p
  ... | no ¬p = cst 2

  open import Level as L
  bf : Names
  bf = (quote _≥a_ ∷ quote reduce-1d ∷ quote N._≟_ ∷ quote prod ∷ [])

  kdec-test = kompile dec-test bf ([])
  kdec-testR = frefl dec-test bf
  --kdec-testR2 = frefln dec-test bf ("Example-04._.with-350" ∷ [])

  ktakeN : Prog
  ktakeN = kompile takeN bf []

  ktakeNR = frefl takeN bf
  --ktakeNRW = ftyn takeN bf ("APL2.with-1366" ∷ [])

-}

{- --This moved into bug-nat-level--

poop : ∀ {d s} → Ar ℕ d s → Ix 1 V.[ prod s ] → ℕ
poop a ix = sel a (off→idx _ ix)

n≤sn-i : ∀ {i n} → i ≤ 1 → n ≤ suc n N.∸ i
n≤sn-i z≤n       = <⇒≤ ≤-refl
n≤sn-i (s≤s z≤n) = ≤-refl

test-take : ∀ {n} → Ix 1 V.[ 2 ] → Ar ℕ 1 V.[ 1 N.+ n ] → Ar ℕ 1 V.[ n ]
test-take {n} ix@(i ∷ []) a =
                 let ixₐ , ix<[2] = ix→a ix
                     r' = (ixₐ ↓ a){λ where jv@(zero ∷ []) → ≤-trans (≤-pred $ ix<[2] jv) (s≤s z≤n)}
                     r  = (cst n ↑ r'){ λ where jv@(zero ∷ []) → n≤sn-i (≤-pred $ F.toℕ<n i) }
                 in r

ktest = kompile test-take [] []

-}

max_stars_repo_name: ashinkarov/agda-extractor

max_issues_repo_name: ashinkarov/agda-extractor

max_forks_repo_name: ashinkarov/agda-extractor


text:
module New.Unused where

open import New.Changes

module _ {ℓ₁} {ℓ₂}
  {A : Set ℓ₁} {B : Set ℓ₂} {{CA : ChAlg A}} {{CB : ChAlg B}} where
  open ≡-Reasoning
  open import Postulate.Extensionality
  module _ (f : A → B) where
    nil-is-derivative : IsDerivative f (nil f)
    nil-is-derivative a da v =
      begin
        f (a ⊕ da)
      ≡⟨ sym (cong (λ □ → □ (_⊕_ a da)) (update-nil f)) ⟩
        (f ⊕ nil f) (a ⊕ da)
      ≡⟨ proj₂ (nil-valid f a da v) ⟩
        f a ⊕ (nil f a da)
      ∎

    derivative-is-nil : ∀ df → IsDerivative f df → f ⊕ df ≡ f
    derivative-is-nil df f-df =
      ext (λ v →
        begin
          f v ⊕ df v (nil v)
        ≡⟨ sym (f-df v (nil v) (nil-valid v)) ⟩
          f (v ⊕ nil v)
        ≡⟨ cong f (update-nil v) ⟩
          f v
        ∎)

    derivative-is-valid : ∀ df
      (IsDerivative-f-df : IsDerivative f df) →
      WellDefinedFunChange f df
    derivative-is-valid df IsDerivative-f-df a da ada
      rewrite sym (IsDerivative-f-df (a ⊕ da) (nil (a ⊕ da)) (nil-valid (a ⊕ da)))
      | update-nil (a ⊕ da)
      | IsDerivative-f-df a da ada
      = refl

    equal-future-expand-derivative : ∀ df → IsDerivative f df →
      ∀ v1 dv1 → valid v1 dv1 →
      ∀ v2 →
      v2 ≡ v1 ⊕ dv1 →
      f v2 ≡ f v1 ⊕ df v1 dv1
    equal-future-expand-derivative df is-derivative-f-df v1 dv1 v1dv1 v2 eq-fut =
      begin
        f v2
      ≡⟨ cong f eq-fut ⟩
        f (v1 ⊕ dv1)
      ≡⟨ is-derivative-f-df v1 dv1 v1dv1 ⟩
        f v1 ⊕ df v1 dv1
      ∎
    -- -- equal-future-expand-derivative df is-derivative-f-df v1 dv1 v1dv1 v2 dv2 v2dv2 eq-fut =
    -- --   begin
    -- --     (f ⊕ df) (v1 ⊕ dv1)
    -- --   ≡⟨ cong (f ⊕ df) eq-fut ⟩
    -- --     (f ⊕ df) (v2 ⊕ dv2)
    -- --   ≡⟨ well-defined-f-df v2 dv2 v2dv2 ⟩
    -- --     f v2 ⊕ df v2 dv2
    -- --   ∎
    --   -- equal-future-expand-base df (derivative-is-valid df is-derivative-f-df)

    equal-future-base : ∀ df → WellDefinedFunChange f df →
      ∀ v1 dv1 → valid v1 dv1 →
      ∀ v2 dv2 → valid v2 dv2 →
      v1 ⊕ dv1 ≡ v2 ⊕ dv2 →
      f v1 ⊕ df v1 dv1 ≡ f v2 ⊕ df v2 dv2
    equal-future-base df well-defined-f-df v1 dv1 v1dv1 v2 dv2 v2dv2 eq-fut =
      begin
        f v1 ⊕ df v1 dv1
      ≡⟨ sym (well-defined-f-df v1 dv1 v1dv1) ⟩
        (f ⊕ df) (v1 ⊕ dv1)
      ≡⟨ cong (f ⊕ df) eq-fut ⟩
        (f ⊕ df) (v2 ⊕ dv2)
      ≡⟨ well-defined-f-df v2 dv2 v2dv2 ⟩
        f v2 ⊕ df v2 dv2
      ∎

    equal-future-change : ∀ df → valid f df →
      ∀ v1 dv1 → valid v1 dv1 →
      ∀ v2 dv2 → valid v2 dv2 →
      v1 ⊕ dv1 ≡ v2 ⊕ dv2 →
      f v1 ⊕ df v1 dv1 ≡ f v2 ⊕ df v2 dv2
    equal-future-change df fdf =
      equal-future-base df
        (λ a da ada → proj₂ (fdf a da ada))

    equal-future-derivative : ∀ df → IsDerivative f df →
      ∀ v1 dv1 → valid v1 dv1 →
      ∀ v2 dv2 → valid v2 dv2 →
      v1 ⊕ dv1 ≡ v2 ⊕ dv2 →
      f v1 ⊕ df v1 dv1 ≡ f v2 ⊕ df v2 dv2
    equal-future-derivative df is-derivative-f-df =
      equal-future-base df (derivative-is-valid df is-derivative-f-df)

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

open import Relation.Binary.PropositionalEquality using (refl)
open import Relation.Nullary using (yes)

open import Data.Unit using (⊤; tt)
open import Data.Product using (_,_)
open import Data.Sum using (inj₁)

open import PiCalculus.LinearTypeSystem.Algebras

module PiCalculus.LinearTypeSystem.Algebras.Shared where

pattern ω = tt

Shared : Algebra ⊤
Algebra.0∙ Shared = ω
Algebra.1∙ Shared = ω
Algebra._≔_∙_ Shared _ _ _ = ⊤
Algebra.∙-computeʳ Shared _ _ = yes (ω , tt)
Algebra.∙-unique Shared _ _ = refl
Algebra.∙-uniqueˡ Shared _ _ = refl
Algebra.0∙-minˡ Shared _ = refl
Algebra.∙-idˡ Shared = tt
Algebra.∙-comm Shared _ = tt
Algebra.∙-assoc Shared _ _ = ω , tt , tt

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
{-# OPTIONS --without-K #-}
open import container.core

module container.w.fibration
  {li la lb}(c : Container li la lb) where

open import sum
open import equality
open import function
open import container.w.core
open import container.w.algebra c
open import hott.level

open Container c

AlgFib : ∀ ℓ → Set _
AlgFib ℓ = Σ ((i : I) → W c i → Set ℓ) λ P
         → (∀ i x → ((b : B (proj₁ x)) → P (r b) (proj₂ x b)) → P i (inW c i x))

AlgSection : ∀ {ℓ} (𝓟 : AlgFib ℓ) → Set _
AlgSection (P , θ) = Σ (∀ i x → P i x) λ f
                   → _≡_ {A = ∀ i x → P i (inW c i x)}
                     (λ i x → θ i x (λ b → f (r b) (proj₂ x b)))
                     (λ i x → f i (inW c i x))

alg-total : ∀ {ℓ} → AlgFib ℓ → Alg _
alg-total (P , θ) = X , ψ
  where
    X : I → Set _
    X i = Σ (W c i) (P i)

    ψ : F X →ⁱ X
    ψ i (a , u) = inW c i (a , λ b → proj₁ (u b))
                , θ i (a , λ b → proj₁ (u b)) (λ b → proj₂ (u b))

module _ {ℓ} (𝓟 : AlgFib ℓ) where
  private 𝓧 = alg-total 𝓟
  open Σ 𝓟 renaming (proj₁ to P ; proj₂ to θ)
  open Σ (alg-total 𝓟) renaming (proj₁ to X ; proj₂ to ψ)

  section : AlgSection 𝓟
  section = f₀ , refl
    where
      f₀ : ∀ i x → P i x
      f₀ i (sup a u) = θ i (a , u) (λ b → f₀ (r b) (u b))

  private
    split-lem : ∀ {ℓ'} (Y : I → Set ℓ')
              → (Y →ⁱ X)
              ≅ ( Σ (Y →ⁱ W c) λ g₀
                → ∀ i x → P i (g₀ i x) )
    split-lem Y
      = sym≅ (curry-iso (λ i _ → X i))
      ·≅ ΠΣ-swap-iso
      ·≅ Σ-ap-iso (curry-iso (λ i _ → W c i))
                  (λ g₀ → curry-iso (λ i x → P i (g₀ (i , x))))

  section-mor-iso : Mor 𝓦 𝓧 ≅ AlgSection 𝓟
  section-mor-iso = begin
      ( Σ (W c →ⁱ X) λ f → ψ ∘ⁱ imap f ≡ f ∘ⁱ inW c )
    ≅⟨ Σ-ap-iso (split-lem (W c)) (λ _ → refl≅) ⟩
      ( Σ (Σ (W c →ⁱ W c) λ f₀ → ∀ i → (w : W c i) → P i (f₀ i w)) λ { (f₀ , f₁)
        → _≡_ {A = ∀ i (x : F (W c) i) → X i}
          (λ i x → let x' = imap f₀ i x
                    in (inW c i x' , θ i x' (λ b → f₁ (r b) (proj₂ x b))))
          (λ i x → (f₀ i (inW c i x) , f₁ i (inW c i x))) } )
    ≅⟨ ( Σ-ap-iso refl≅ λ { (f₀ , f₁) → iso≡ (split-lem (F (W c)))
                                      ·≅ sym≅ Σ-split-iso } ) ⟩
      ( Σ (Σ (W c →ⁱ W c) λ f₀ → ∀ i → (w : W c i) → P i (f₀ i w)) λ { (f₀ , f₁)
      → Σ ( _≡_ {A = ∀ i (x : F (W c) i) → W c i}
            (λ i x → inW c i (imap f₀ i x))
            (λ i x → f₀ i (inW c i x)) ) λ eq
      → subst (λ g → ∀ i (x : F (W c) i) → P i (g i x)) eq
            (λ i x → θ i (imap f₀ i x) (λ b → f₁ (r b) (proj₂ x b)))
          ≡ (λ i x → f₁ i (inW c i x)) } )
    ≅⟨ record
          { to = λ { ((f₀ , f₁) , (α₀ , α₁)) → ((f₀ , α₀) , (f₁ , α₁)) }
          ; from = λ { ((f₀ , α₀) , (f₁ , α₁)) → ((f₀ , f₁) , (α₀ , α₁)) }
          ; iso₁ = λ { ((f₀ , f₁) , (α₀ , α₁)) → refl }
          ; iso₂ = λ { ((f₀ , α₀) , (f₁ , α₁)) → refl } } ⟩
      ( Σ ( Σ (∀ i → W c i → W c i) λ f₀
          → ( _≡_ {A = ∀ i (x : F (W c) i) → W c i}
              (λ i x → inW c i (imap f₀ i x))
              (λ i x → f₀ i (inW c i x)) ) ) λ { (f₀ , eq)
      → Σ (∀ i w → P i (f₀ i w)) λ f₁
      → subst (λ g → ∀ i (x : F (W c) i) → P i (g i x)) eq
            (λ i x → θ i (imap f₀ i x) (λ b → f₁ (r b) (proj₂ x b)))
          ≡ (λ i x → f₁ i (inW c i x)) } )
    ≅⟨ sym≅ ( Σ-ap-iso (sym≅ (contr-⊤-iso W-initial-W)) λ _ → refl≅ ) ·≅ ×-left-unit ⟩
      ( Σ (∀ i w → P i w) λ f₁
      → (λ i x → θ i x (λ b → f₁ (r b) (proj₂ x b)))
      ≡ (λ i x → f₁ i (inW c i x)) )
    ∎
    where
      open ≅-Reasoning

  W-section-contr : contr (AlgSection 𝓟)
  W-section-contr = iso-level section-mor-iso (W-initial 𝓧)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


text:
open import FRP.JS.String using ( _≟_ )
open import FRP.JS.Bool using ( Bool ; true ; false ; if_then_else_ ; _∧_ ; _∨_ ; not ; _xor_ )
open import FRP.JS.QUnit using ( TestSuite ; ok ; test ; _,_ )

module FRP.JS.Test.Bool where

tests : TestSuite
tests =
  ( test "true"
    ( ok "true" true )
  , test "false"
    ( ok "false" (not false) )
  , test "if"
    ( ok "if true" (if true then "a" else "b" ≟ "a")
    , ok "if false" (if false then "a" else "b" ≟ "b") )
  , test "∧"
    ( ok "true ∧ true" (true ∧ true)
    , ok "true ∧ false" (not (true ∧ false))
    , ok "false ∧ true" (not (false ∧ true))
    , ok "false ∧ false" (not (false ∧ false)) )
  , test "∨"
    ( ok "true ∨ true" (true ∨ true)
    , ok "true ∨ false" (true ∨ false)
    , ok "false ∨ true" (false ∨ true)
    , ok "false ∨ false" (not (false ∨ false)) )
  , test "xor"
    ( ok "true xor true" (not (true xor true))
    , ok "true xor false" (true xor false)
    , ok "false xor true" (false xor true)
    , ok "false xor false" (not (false xor false)) )
  )

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


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

import 05-identity-types
open 05-identity-types public

-- Inversion is uninteresting and comes from:
inversion-proof :
  {i : Level} {A : UU i} (x : A) → (y : A) → Id x y → Id y x
inversion-proof x y = ind-Id x (λ y' p' → Id y' x) refl y

lemma-2-2-2-i :
  {i j : Level} {A : UU i} {B : UU j} (x y z : A) (f : A → B) → (p : Id x y) → (q : Id y z)
  → Id (ap f (p ∙ q)) ((ap f p) ∙ (ap f q))
lemma-2-2-2-i x y z f refl q = refl
-- We apparently don't need a second induction on q..

lemma-2-2-2-ii :
  {i j : Level} {A : UU i} {B : UU j} (x y : A) (f : A → B) → (p : Id x y)
  → Id (ap f (inv p)) (inv (ap f p))
lemma-2-2-2-ii x y f refl = refl

lemma-2-2-2-iii :
  {i j k : Level} {A : UU i} {B : UU j} {C : UU k} (x y : A) (f : A → B) → (g : B → C) → (p : Id x y)
  → Id (ap g (ap f p)) (ap (g ∘ f) p)
lemma-2-2-2-iii x y f g refl = refl

lemma-2-2-2-iv :
  {i j k : Level} {A : UU i} {B : UU j} {C : UU k} (x y : A) → (p : Id x y)
  → Id (ap (λ x → x) p) p
lemma-2-2-2-iv x y refl = refl

-- Path lifting property
lemma-2-3-2 :
  {i j : Level} {A : UU i} {P : A → UU j} (x y : A) (u : P x) → (p : Id x y)
  → Id (pair x u) (pair y (tr P p u))
lemma-2-3-2 x y u refl = refl

lemma-2-3-9 :
  {i j : Level} {A : UU i} {P : A → UU j} (x y z : A) (u : P x) → (p : Id x y)
  → (q : Id y z) → Id (tr P q (tr P p u)) (tr P (p ∙ q) u)
lemma-2-3-9 x y z u refl q = refl

lemma-2-3-10 :
  {i j k : Level} {A : UU i} {B : UU j} {P : B → UU k} (x y : A) (f : A → B) (u : P (f x)) → (p : Id x y)
  → Id (tr (P ∘ f) p u) (tr P (ap f p) u)
lemma-2-3-10 x y f u refl = refl

lemma-2-3-11 :
  {i j k : Level} {A : UU i} {P : A → UU j} {Q : A → UU k}
  (x y : A) (f : (z : A) → P z → Q z) (u : P x) → (p : Id x y)
  → Id (tr Q p (f x u)) (f y (tr P p u))
lemma-2-3-11 x y f u refl = refl

-- Eckert-Hamilton

-- First, the loop
loop-type : {i : Level} {A : UU i} (x : A) → UU i
loop-type x = Id x x

order-2-star :
  {i : Level} {A : UU i} (a b c : A) → (p q : Id a b) → (r s : Id b c)
   → (alpha : Id p q) → (beta : Id r s) → Id (concat p c r) (concat q c s)
order-2-star a b c refl q refl s refl refl = refl

left-whisker :
  {i : Level} {A : UU i} (a b c : A) → (p q : Id a b) → (r : Id b c)
   → (alpha : Id p q) → Id (concat p c r) (concat q c r)
left-whisker a b c refl refl r refl = refl

right-whisker :
  {i : Level} {A : UU i} (a b c : A) → (p : Id a b) → (r s : Id b c)
   → (beta : Id r s) → Id (concat p c r) (concat p c s)
right-whisker a b c p refl refl refl = refl

-- TODO: Eckmann Hilton

-- 2.4: the equivalence of functions, quasi-inverses

-- `Sim-By` might be poorly set up since it basically takes the witness of what it
-- actually should just be. (../07- has the correct stuff.)
data Homotopic-Fn {i j : Level} (A : UU i) (B : UU j) (f g : A → B) : UU (i ⊔ j) where
  Sim-By : ((x : A) → (Id (f x) (g x))) → Homotopic-Fn A B f g

data Is-Equiv {i j : Level} {A : UU i} {B : UU j} (f : A → B) : UU (i ⊔ j) where
  With-Qinv : (g : B → A) → (Homotopic-Fn A A (g ∘ f) (λ x → x))
                          → (Homotopic-Fn B B (f ∘ g) (λ x → x))
                          → Is-Equiv f

-- Relying on the book's lemma 2.4.12, we're just using the above for type equivalence
data Equiv-Types {i j : Level} (A : UU i) (B : UU j) : UU (i ⊔ j) where
  Eq-By : (Σ (A → B) Is-Equiv)  → Equiv-Types A B

-- 2.6.1
product-functoriality :
  {i j : Level} {A : UU i} {B : UU j} (x y : prod A B) → (Id x y)
  → (prod (Id (pr1 x) (pr1 y)) (Id (pr2 x) (pr2 y)))
product-functoriality x y refl = pair refl refl

-- 2.6.2
pair= :
  {i j : Level} {A : UU i} {B : UU j} (a₁ a₂ : A) → (b₁ b₂ : B)
  → (prod (Id a₁ a₂) (Id b₁ b₂)) → (Id (pair a₁ b₁) (pair a₂ b₂))
pair= a₁ a₂ b₁ b₂ (pair refl refl) = refl

-- This is a bit of laziness to exhibit both bits of the proof with the same a₁ etc.
-- The point is to show that product-functoriality and pair= are quasi-inverses.
functoriality-is-equiv-to-2-6-2 :
  {i j : Level} {A : UU i} {B : UU j} {a₁ a₂ : A} {b₁ b₂ : B} →
  -- First two bindings give us shorthands for the proper invocations of the above
  -- functions (currying away aₙ and bₙ).
  let functorial = (product-functoriality (pair a₁ b₁) (pair a₂ b₂))
      2-6-2 = (pair= a₁ a₂ b₁ b₂)
      thm-after-funct = (Homotopic-Fn (prod (Id a₁ a₂) (Id b₁ b₂))
                                  (prod (Id a₁ a₂) (Id b₁ b₂))
                                  (λ x → x)
                                  (functorial ∘ 2-6-2))
      funct-after-thm = (Homotopic-Fn (Id (pair a₁ b₁) (pair a₂ b₂))
                                  (Id (pair a₁ b₁) (pair a₂ b₂))
                                  (2-6-2 ∘ functorial)
                                  (λ x → x))
  in (prod thm-after-funct funct-after-thm)
functoriality-is-equiv-to-2-6-2 = pair (Sim-By (λ {(pair refl refl) → refl})) (Sim-By (λ {refl → refl}))

-- 2.6.4
pair-transport :
  {i j k : Level} {Z : UU k} {A : Z → UU i} {B : Z → UU j} (z w : Z) → (p : Id z w) → (x : prod (A z) (B z))
  → (Id (tr (λ z → (prod (A z) (B z))) p x) (pair (tr A p (pr1 x)) (tr B p (pr2 x))))
pair-transport z w refl (pair az bz) = refl

-- 2.6.5
ap-functorial :
  {i j k l : Level} {A : UU i} {A' : UU j} {B : UU k} {B' : UU l} (g : A → A') → (h : B → B')
  → (x y : prod A B) → (p : Id (pr1 x) (pr1 y)) → (q : Id (pr2 x) (pr2 y)) →
  let pf= = (pair= (pr1 x) (pr1 y) (pr2 x) (pr2 y))
      pgh = (pair= (g (pr1 x)) (g (pr1 y)) (h (pr2 x)) (h (pr2 y)))
      f = (λ x → pair (g (pr1 x)) (h (pr2 x)))
  in Id (ap f (pf= (pair p q))) (pgh (pair (ap g p) (ap h q)))
ap-functorial g h (pair aₓ bₓ) (pair ay by) refl refl = refl

-- 2.9: Extensionality
happly : {i j : Level} {A : UU i} {B : A → UU j} (f g : (x : A) → B(x)) →
          (Id f g) → ((x : A) → (Id (f x) (g x)))
happly f g refl = λ x → refl

postulate fn-ext : Is-Equiv happly

dependent-fn-transport : {i j : Level} {X : UU i} (A : X → UU j) → (B : (x : X) → A x → UU (i ⊔ j))
                         (x₁ x₂ : X) → (Id x₁ x₂) →
                         (f : (a : A x₁) → (B x₁ a)) → (A x₂) → ((a : A x₂) → (B x₂ a))
dependent-fn-transport A B x₁ x₂ refl f a = tr (B-hat B) (pair= x₁ x₂ (tr A refl a) a
                                                              (pair refl refl))
                                                      (f (tr A refl a))
 where
   B-hat :  {i j : Level} {X : UU i} {A : X → UU j} (B : (x : X) → A x → UU (i ⊔ j)) → (Σ X (λ x → A x)) → UU (i ⊔ j)
   B-hat B w = B (pr1 w) (pr2 w)

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
module Semantics.Substitution where

open import Semantics.Substitution.Kits public
open import Semantics.Substitution.Traversal public
open import Semantics.Substitution.Instances public
open import Semantics.Substitution.Soundness public

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


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

module Verification.CorruptFormalisations where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.Loop
open import FOTC.Program.ABP.Terms

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

-- Corrupt as a constant.
module Constant where
  postulate
    corrupt   : D
    corrupt-T : ∀ os x xs →
                corrupt · (T ∷ os) · (x ∷ xs) ≡ ok x ∷ corrupt · os · xs
    corrupt-F : ∀ os x xs →
                corrupt · (F ∷ os) · (x ∷ xs) ≡ error ∷ corrupt · os · xs

-- Corrupt as a binary function.
module BinaryFunction where
  postulate
    corrupt   : D → D → D
    corrupt-T : ∀ os x xs →
                corrupt (T ∷ os) (x ∷ xs) ≡ ok x ∷ corrupt os xs
    corrupt-F : ∀ os x xs →
                corrupt (F ∷ os) (x ∷ xs) ≡ error ∷ corrupt os xs

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import lib.Basics
open import lib.types.Span
open import lib.types.Pointed
open import lib.types.Pushout
open import lib.types.PushoutFlattening
open import lib.types.Unit
open import lib.types.Paths
open import lib.cubical.Square

-- Suspension is defined as a particular case of pushout

module lib.types.Suspension where

module _ {i} (A : Type i) where

  suspension-span : Span
  suspension-span = span Unit Unit A (λ _ → tt) (λ _ → tt)

  Suspension : Type i
  Suspension = Pushout suspension-span

  north : Suspension
  north = left tt

  south : Suspension
  south = right tt

  merid : A → north == south
  merid x = glue x

  module SuspensionElim {j} {P : Suspension → Type j} (n : P north)
    (s : P south) (p : (x : A) → n == s [ P ↓ merid x ])
    = PushoutElim (λ _ → n) (λ _ → s) p

  open SuspensionElim public using () renaming (f to Suspension-elim)

  module SuspensionRec {j} {C : Type j} (n s : C) (p : A → n == s)
    = PushoutRec {d = suspension-span} (λ _ → n) (λ _ → s) p

  module SuspensionRecType {j} (n s : Type j) (p : A → n ≃ s)
    = PushoutRecType {d = suspension-span} (λ _ → n) (λ _ → s) p

suspension-⊙span : ∀ {i} → Ptd i → ⊙Span
suspension-⊙span X =
  ⊙span ⊙Unit ⊙Unit X (⊙cst {X = X}) (⊙cst {X = X})

⊙Susp : ∀ {i} → Ptd i → Ptd i
⊙Susp (A , _) = ⊙[ Suspension A , north A ]

σloop : ∀ {i} (X : Ptd i) → fst X → north (fst X) == north (fst X)
σloop (_ , x₀) x = merid _ x ∙ ! (merid _ x₀)

σloop-pt : ∀ {i} {X : Ptd i} → σloop X (snd X) == idp
σloop-pt {X = (_ , x₀)} = !-inv-r (merid _ x₀)

module FlipSusp {i} {A : Type i} = SuspensionRec A
  (south A) (north A) (! ∘ merid A)

flip-susp : ∀ {i} {A : Type i} → Suspension A → Suspension A
flip-susp = FlipSusp.f

⊙flip-susp : ∀ {i} (X : Ptd i) → fst (⊙Susp X ⊙→ ⊙Susp X)
⊙flip-susp X = (flip-susp , ! (merid _ (snd X)))

module _ {i j} where

  module SuspFmap {A : Type i} {B : Type j} (f : A → B) =
    SuspensionRec A (north B) (south B) (merid B ∘ f)

  susp-fmap : {A : Type i} {B : Type j} (f : A → B)
    → (Suspension A → Suspension B)
  susp-fmap = SuspFmap.f

  ⊙susp-fmap : {X : Ptd i} {Y : Ptd j} (f : fst (X ⊙→ Y))
    → fst (⊙Susp X ⊙→ ⊙Susp Y)
  ⊙susp-fmap (f , fpt) = (susp-fmap f , idp)

module _ {i} where

  susp-fmap-idf : (A : Type i) → ∀ a → susp-fmap (idf A) a == a
  susp-fmap-idf A = Suspension-elim _ idp idp $ λ a →
    ↓-='-in (ap-idf (merid _ a) ∙ ! (SuspFmap.glue-β (idf A) a))

  ⊙susp-fmap-idf : (X : Ptd i)
    → ⊙susp-fmap (⊙idf X) == ⊙idf (⊙Susp X)
  ⊙susp-fmap-idf X = ⊙λ= (susp-fmap-idf (fst X)) idp

module _ {i j} where

  susp-fmap-cst : {A : Type i} {B : Type j} (b : B)
    (a : Suspension A) → susp-fmap (cst b) a == north _
  susp-fmap-cst b = Suspension-elim _ idp (! (merid _ b)) $ (λ a →
    ↓-app=cst-from-square $ SuspFmap.glue-β (cst b) a ∙v⊡ tr-square _)

  ⊙susp-fmap-cst : {X : Ptd i} {Y : Ptd j}
    → ⊙susp-fmap (⊙cst {X = X} {Y = Y}) == ⊙cst
  ⊙susp-fmap-cst = ⊙λ= (susp-fmap-cst _) idp

module _ {i j k} where

  susp-fmap-∘ : {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → B)
    (σ : Suspension A) → susp-fmap (g ∘ f) σ == susp-fmap g (susp-fmap f σ)
  susp-fmap-∘ g f = Suspension-elim _
    idp
    idp
    (λ a → ↓-='-in $
      ap-∘ (susp-fmap g) (susp-fmap f) (merid _ a)
      ∙ ap (ap (susp-fmap g)) (SuspFmap.glue-β f a)
      ∙ SuspFmap.glue-β g (f a)
      ∙ ! (SuspFmap.glue-β (g ∘ f) a))

  ⊙susp-fmap-∘ : {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
    (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y))
    → ⊙susp-fmap (g ⊙∘ f) == ⊙susp-fmap g ⊙∘ ⊙susp-fmap f
  ⊙susp-fmap-∘ g f = ⊙λ= (susp-fmap-∘ (fst g) (fst f)) idp

{- Extract the 'glue component' of a pushout -}
module _ {i j k} {s : Span {i} {j} {k}} where

  module ExtGlue = PushoutRec {d = s} {D = Suspension (Span.C s)}
    (λ _ → north _) (λ _ → south _) (merid _)

  ext-glue = ExtGlue.f

module _ {i j k} {s : Span {i} {j} {k}} {x₀ : Span.A s} where

  ⊙ext-glue :
    fst ((Pushout s , left x₀) ⊙→ (Suspension (Span.C s) , north _))
  ⊙ext-glue = (ext-glue , idp)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda