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

open import Base

module Integers where

succ : ℤ → ℤ
succ O = pos O
succ (pos n) = pos (S n)
succ (neg O) = O
succ (neg (S n)) = neg n

pred : ℤ → ℤ
pred O = neg O
pred (pos O) = O
pred (pos (S n)) = pos n
pred (neg n) = neg (S n)

abstract
  succ-pred : (n : ℤ) → succ (pred n) ≡ n
  succ-pred O = refl
  succ-pred (pos O) = refl
  succ-pred (pos (S n)) = refl
  succ-pred (neg n) = refl

  pred-succ : (n : ℤ) → pred (succ n) ≡ n
  pred-succ O = refl
  pred-succ (pos n) = refl
  pred-succ (neg O) = refl
  pred-succ (neg (S n)) = refl

succ-is-equiv : is-equiv succ
succ-is-equiv = iso-is-eq succ pred succ-pred pred-succ

succ-equiv : ℤ ≃ ℤ
succ-equiv = (succ , succ-is-equiv)

-- Equality on ℕ and ℤ is decidable and both are sets

private
  ℕ-get-S : ℕ → ℕ
  ℕ-get-S 0 = 42
  ℕ-get-S (S n) = n

  S-injective : (n m : ℕ) (p : S n ≡ S m) → n ≡ m
  S-injective n m p = ap ℕ-get-S p

  ℕ-S≢O-type : ℕ → Set
  ℕ-S≢O-type O = ⊥
  ℕ-S≢O-type (S n) = unit

-- Technical note: You need to write "0" and not "O" in the following types
-- because S and O are both overloaded so Agda is confused by [S n ≢ O]
abstract
  ℕ-S≢O : (n : ℕ) → S n ≢ 0
  ℕ-S≢O n p = transport ℕ-S≢O-type p tt

  ℕ-S≢O#instance : {n : ℕ} → (S n ≢ 0)
  ℕ-S≢O#instance {n} = ℕ-S≢O n

  ℕ-O≢S : (n : ℕ) → (0 ≢ S n)
  ℕ-O≢S n p = ℕ-S≢O n (! p)

  ℕ-has-dec-eq : has-dec-eq ℕ
  ℕ-has-dec-eq O O = inl refl
  ℕ-has-dec-eq O (S n) = inr (ℕ-O≢S n)
  ℕ-has-dec-eq (S n) O = inr (ℕ-S≢O n)
  ℕ-has-dec-eq (S n) (S m) with ℕ-has-dec-eq n m
  ℕ-has-dec-eq (S n) (S m) | inl p = inl (ap S p)
  ℕ-has-dec-eq (S n) (S m) | inr p⊥ = inr (λ p → p⊥ (S-injective n m p))

  ℕ-is-set : is-set ℕ
  ℕ-is-set = dec-eq-is-set ℕ-has-dec-eq

data _<_ : ℕ → ℕ → Set where
  <n : {n : ℕ} → n < S n
  <S : {n m : ℕ} → (n < m) → (n < S m)

_+_ : ℕ → ℕ → ℕ
0 + m = m
S n + m = S (n + m)

+S-is-S+ : (n m : ℕ) → n + S m ≡ S n + m
+S-is-S+ O m = refl
+S-is-S+ (S n) m = ap S (+S-is-S+ n m)

+0-is-id : (n : ℕ) → n + 0 ≡ n
+0-is-id O = refl
+0-is-id (S n) = ap S (+0-is-id n)

private
  ℤ-get-pos : ℤ → ℕ
  ℤ-get-pos O = 0
  ℤ-get-pos (pos n) = n
  ℤ-get-pos (neg n) = 0

  pos-injective : (n m : ℕ) (p : pos n ≡ pos m) → n ≡ m
  pos-injective n m p = ap ℤ-get-pos p

  ℤ-get-neg : ℤ → ℕ
  ℤ-get-neg O = 0
  ℤ-get-neg (pos n) = 0
  ℤ-get-neg (neg n) = n

  neg-injective : (n m : ℕ) (p : neg n ≡ neg m) → n ≡ m
  neg-injective n m p = ap ℤ-get-neg p

  ℤ-neg≢O≢pos-type : ℤ → Set
  ℤ-neg≢O≢pos-type O = unit
  ℤ-neg≢O≢pos-type (pos n) = ⊥
  ℤ-neg≢O≢pos-type (neg n) = ⊥

  ℤ-neg≢pos-type : ℤ → Set
  ℤ-neg≢pos-type O = unit
  ℤ-neg≢pos-type (pos n) = ⊥
  ℤ-neg≢pos-type (neg n) = unit

abstract
  ℤ-O≢pos : (n : ℕ) → O ≢ pos n
  ℤ-O≢pos n p = transport ℤ-neg≢O≢pos-type p tt

  ℤ-pos≢O : (n : ℕ) → pos n ≢ O
  ℤ-pos≢O n p = transport ℤ-neg≢O≢pos-type (! p) tt

  ℤ-O≢neg : (n : ℕ) → O ≢ neg n
  ℤ-O≢neg n p = transport ℤ-neg≢O≢pos-type p tt

  ℤ-neg≢O : (n : ℕ) → neg n ≢ O
  ℤ-neg≢O n p = transport ℤ-neg≢O≢pos-type (! p) tt

  ℤ-neg≢pos : (n m : ℕ) → neg n ≢ pos m
  ℤ-neg≢pos n m p = transport ℤ-neg≢pos-type p tt

  ℤ-pos≢neg : (n m : ℕ) → pos n ≢ neg m
  ℤ-pos≢neg n m p = transport ℤ-neg≢pos-type (! p) tt

  ℤ-has-dec-eq : has-dec-eq ℤ
  ℤ-has-dec-eq O O = inl refl
  ℤ-has-dec-eq O (pos n) = inr (ℤ-O≢pos n)
  ℤ-has-dec-eq O (neg n) = inr (ℤ-O≢neg n)
  ℤ-has-dec-eq (pos n) O = inr (ℤ-pos≢O n)
  ℤ-has-dec-eq (pos n) (pos m) with ℕ-has-dec-eq n m
  ℤ-has-dec-eq (pos n) (pos m) | inl p = inl (ap pos p)
  ℤ-has-dec-eq (pos n) (pos m) | inr p⊥ = inr (λ p → p⊥ (pos-injective n m p))
  ℤ-has-dec-eq (pos n) (neg m) = inr (ℤ-pos≢neg n m)
  ℤ-has-dec-eq (neg n) O = inr (ℤ-neg≢O n)
  ℤ-has-dec-eq (neg n) (pos m) = inr (ℤ-neg≢pos n m)
  ℤ-has-dec-eq (neg n) (neg m) with ℕ-has-dec-eq n m
  ℤ-has-dec-eq (neg n) (neg m) | inl p = inl (ap neg p)
  ℤ-has-dec-eq (neg n) (neg m) | inr p⊥ = inr (λ p → p⊥ (neg-injective n m p))

  ℤ-is-set : is-set ℤ
  ℤ-is-set = dec-eq-is-set ℤ-has-dec-eq

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
data Tm : Set where
  tzero : Tm
  tsucc : Tm → Tm
  tdiff : Tm → Tm → Tm

variable
  m n n' : Tm

data NotZero : Tm → Set where
  nzsucc : NotZero (tsucc n)
  nzdiff : NotZero (tdiff m n)

data Equal : Tm → Tm → Set where
  esucc : NotZero n → Equal (tsucc (tdiff tzero n)) n
  ediff : Equal n n' → Equal (tdiff m n) (tdiff m n')

data Foo : Tm → Set where
  fleft : Foo m → Foo (tdiff m n)
  frght : Foo n → Foo (tdiff m (tsucc n))

foo : Foo n → Equal n n' → Foo n'
foo (fleft f) e = {!!}
foo (frght (frght f)) (ediff (esucc nz)) = {!nz!} -- case-split on nz replaces nz with nzsucc

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.QuadTree.Implementation.ValidTypes where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Lens.Lens
open import Data.Logic
open import Data.QuadTree.Implementation.Definition

{-# FOREIGN AGDA2HS
{-# LANGUAGE Safe #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Rank2Types #-}
import Data.Nat
import Data.Lens.Lens
import Data.Logic

import Data.QuadTree.Implementation.Definition
#-}

---- Valid types

-- Calculates the depth of a quadrant
depth : {t : Set} -> Quadrant t -> Nat
depth (Leaf x) = 0
depth (Node a b c d) = 1 + max4 (depth a) (depth b) (depth c) (depth d)
{-# COMPILE AGDA2HS depth #-}

-- Calculates the maximum legal depth of a quadtree
maxDepth : {t : Set} -> QuadTree t -> Nat
maxDepth (Wrapper (w , h) _) = log2up (max w h)
{-# COMPILE AGDA2HS maxDepth #-}

-- Converts a tree to its root quadrant
treeToQuadrant : {t : Set} -> QuadTree t -> Quadrant t
treeToQuadrant (Wrapper _ qd) = qd
{-# COMPILE AGDA2HS treeToQuadrant #-}

-- Checks whether a quadrant is compressed
isCompressed : {t : Set} -> {{eqT : Eq t}} -> Quadrant t -> Bool
isCompressed (Leaf _) = true
isCompressed (Node (Leaf a) (Leaf b) (Leaf c) (Leaf d)) = not (a == b && b == c && c == d)
isCompressed (Node a b c d) = isCompressed a && isCompressed b && isCompressed c && isCompressed d
{-# COMPILE AGDA2HS isCompressed #-}

-- Checks whether the invariants of a quadrant hold
isValid : {t : Set} -> {{eqT : Eq t}} -> (dep : Nat) -> Quadrant t -> Bool
isValid dep qd = depth qd <= dep && isCompressed qd
{-# COMPILE AGDA2HS isValid #-}

-- A type that represents a valid quadrant
data VQuadrant (t : Set) {{eqT : Eq t}} {dep : Nat} : Set where
  CVQuadrant : (qd : Quadrant t) -> {.(IsTrue (isValid dep qd))} -> VQuadrant t {dep}
{-# FOREIGN AGDA2HS
newtype VQuadrant t = CVQuadrant (Quadrant t)
#-}

-- A type that represents a valid quadtree
data VQuadTree (t : Set) {{eqT : Eq t}} {dep : Nat} : Set where
  CVQuadTree : (qt : QuadTree t) -> {.(IsTrue (isValid dep (treeToQuadrant qt)))} -> {.(IsTrue (dep == maxDepth qt))} -> VQuadTree t {dep}
{-# FOREIGN AGDA2HS
newtype VQuadTree t = CVQuadTree (QuadTree t)
#-}

qtToSafe : {t : Set} {{eqT : Eq t}} {dep : Nat}
  -> (qt : QuadTree t) -> {.(IsTrue (isValid dep (treeToQuadrant qt)))} -> {.(IsTrue (dep == maxDepth qt))}
  -> VQuadTree t {maxDepth qt}
qtToSafe {dep = dep} qt {p} {q} = CVQuadTree qt {useEq (cong (λ g -> isValid g (treeToQuadrant qt)) (eqToEquiv dep (maxDepth qt) q)) p} {eqReflexivity (maxDepth qt)}
{-# COMPILE AGDA2HS qtToSafe #-}

qtFromSafe : {t : Set} {{eqT : Eq t}} -> {dep : Nat} -> VQuadTree t {dep} -> QuadTree t
qtFromSafe (CVQuadTree qt) = qt
{-# COMPILE AGDA2HS qtFromSafe #-}

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
------------------------------------------------------------------------
-- Breadth-first labelling of trees
------------------------------------------------------------------------

module BreadthFirst where

open import Codata.Musical.Notation
open import Codata.Musical.Colist using ([]; _∷_; concat)
open import Function
open import Data.Unit
open import Data.List.NonEmpty using (_⁺++⁺_)
open import Relation.Binary.PropositionalEquality as PropEq
  using () renaming (refl to ≡-refl)

open import BreadthFirst.Universe
open import BreadthFirst.Programs
open import BreadthFirst.Lemmas
open import Tree using (Tree; leaf; node; map)
open import Stream using (Stream; _≺_)

------------------------------------------------------------------------
-- Breadth-first labelling

label′ : ∀ {A B} → Tree A → Stream B →
         ElP (tree ⌈ B ⌉ ⊗ stream ⌈ Stream B ⌉)
label′ t ls = lab t (↓ (⌈ ls ⌉ ≺ ♯ snd (label′ t ls)))

label : ∀ {A B} → Tree A → Stream B → Tree B
label t ls = ⟦ fst (label′ t ls) ⟧

------------------------------------------------------------------------
-- Breadth-first labelling preserves the shape of the tree

shape-preserved′ : ∀ {A B} (t : Tree A)
                   (lss : ElP (stream ⌈ Stream B ⌉)) →
                   Eq (tree ⌈ ⊤ ⌉) (map (const tt) ⟦ fst (lab t lss) ⟧)
                                   (map (const tt) t)
shape-preserved′ leaf         lss = leaf
shape-preserved′ (node l _ r) lss with whnf lss
... | ⌈ x ≺ ls ⌉ ≺ lss′ =
  node (♯ shape-preserved′ (♭ l) (♭ lss′)) ⌈ ≡-refl ⌉
       (♯ shape-preserved′ (♭ r) (snd (lab (♭ l) (♭ lss′))))

shape-preserved : ∀ {A B} (t : Tree A) (ls : Stream B) →
                  Eq (tree ⌈ ⊤ ⌉) (map (const tt) (label t ls))
                                  (map (const tt) t)
shape-preserved t ls = shape-preserved′ t (↓ (⌈ ls ⌉ ≺ _))

------------------------------------------------------------------------
-- Breadth-first labelling uses the right labels

invariant : ∀ {A B} (t : Tree A) lss →
            EqP (stream (stream ⌈ B ⌉))
                ⟦ lss ⟧
                (zipWith _⁺++∞_ ⟦ flatten ⟦ fst (lab t lss) ⟧ ⟧
                                ⟦ snd (lab t lss) ⟧)
invariant leaf         lss = ⟦ lss ⟧ ∎
invariant (node l _ r) lss with whnf lss
... | ⌈ x ≺ ls ⌉ ≺ lss′ =
  (⌈ ≡-refl ⌉ ≺ ♯ refl (♭ ls)) ≺ ♯ (
    ⟦ ♭ lss′ ⟧                                     ≊⟨ invariant (♭ l) (♭ lss′) ⟩
    zipWith _⁺++∞_ ⟦ flatten ⟦ fst l′ ⟧ ⟧
                   ⟦ snd l′ ⟧                      ≊⟨ zipWith-cong ⁺++∞-cong
                                                        (⟦ flatten ⟦ fst l′ ⟧ ⟧ ∎)
                                                        (invariant (♭ r) (snd l′)) ⟩
    zipWith _⁺++∞_
      ⟦ flatten ⟦ fst l′ ⟧ ⟧
      (zipWith _⁺++∞_ ⟦ flatten ⟦ fst r′ ⟧ ⟧
                      ⟦ snd r′ ⟧)                  ≈⟨ zip-++-assoc (flatten ⟦ fst l′ ⟧)
                                                                   (flatten ⟦ fst r′ ⟧)
                                                                   ⟦ snd r′ ⟧ ⟩
    zipWith _⁺++∞_
      ⟦ longZipWith _⁺++⁺_ (flatten ⟦ fst l′ ⟧)
                           (flatten ⟦ fst r′ ⟧) ⟧
      ⟦ snd r′ ⟧                                   ∎)
  where
  l′ = lab (♭ l) (♭ lss′)
  r′ = lab (♭ r) (snd l′)

prefix-lemma : ∀ {a} xs xss yss →
               Eq (stream (stream a))
                  (xs ≺ ♯ xss) (zipWith _⁺++∞_ yss xss) →
               PrefixOfP a (concat yss) xs
prefix-lemma xs xss         []         _            = []
prefix-lemma xs (xs′ ≺ xss) (ys ∷ yss) (xs≈ ≺ xss≈) =
  concat (ys ∷ yss)      ≋⟨ concat-lemma ys yss ⟩
  ys ⁺++ concat (♭ yss)  ⊑⟨ ⁺++-mono ys (♯ prefix-lemma xs′ (♭ xss) (♭ yss) ⟦ lemma ⟧≈) ⟩
  ys ⁺++∞ xs′            ≈⟨ sym xs≈ ⟩
  xs                     ∎
  where
  lemma =
    xs′ ≺ _ {- ♯ ♭ xss -}           ≈⟨ refl xs′ ≺ ♯ refl (♭ xss) ⟩
    xs′ ≺ xss                       ≈⟨ ♭ xss≈ ⟩
    zipWith _⁺++∞_ (♭ yss) (♭ xss)  ∎

is-prefix : ∀ {A B} (t : Tree A) (ls : Stream B) →
            PrefixOf ⌈ B ⌉ (concat ⟦ flatten (label t ls) ⟧) ls
is-prefix {B = B} t ls =
  ⟦ prefix-lemma ls ⟦ snd l ⟧ ⟦ flatten ⟦ fst l ⟧ ⟧
      ⟦ ls ≺ _ {- ♯ ⟦ snd l ⟧ -}                        ≈⟨ refl ls ≺ ♯ refl ⟦ snd l ⟧ ⟩
        ⟦ ↓ (⌈ ls ⌉ ≺ _) ⟧                              ≊⟨ invariant t (↓ ⌈ ls ⌉ ≺ _) ⟩
        zipWith _⁺++∞_ ⟦ flatten ⟦ fst l ⟧ ⟧ ⟦ snd l ⟧  ∎ ⟧≈ ⟧⊑
  where l = label′ t ls

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
module Compilation.Term where

open import Context
open import Type.Core
open import Type.NbE
import Term.Core as Core
open import Compilation.Data
open import Compilation.Encode.Core

open import Function
open import Data.Empty
open import Data.Sum.Base
open import Data.List.Base as List

infix 3 _⊢_

data Recursivity : Set where
  NonRec Rec : Recursivity

caseRec : ∀ {ρ} {R : Set ρ} -> Recursivity -> R -> R -> R
caseRec NonRec x y = x
caseRec Rec    x y = y

data _⊢_ {Θ} Γ : Star Θ -> Set where
  letType : ∀ {σ β} -> (α : Θ ⊢ᵗ σ) -> shiftᶜ Γ ⊢ β -> Γ ⊢ β [ α ]ᵗ
  letTerm : ∀ {α} Δ rec -> Seq (caseRec rec Γ (Γ ▻▻ Δ) ⊢_) Δ -> Γ ▻▻ Δ ⊢ α -> Γ ⊢ α
  var  : ∀ {α}   -> α ∈ Γ -> Γ ⊢ α
  Λ_   : ∀ {σ α} -> shiftᶜ Γ ⊢ α -> Γ ⊢ π σ α
  _[_] : ∀ {σ β} -> Γ ⊢ π σ β -> (α : Θ ⊢ᵗ σ) -> Γ ⊢ β [ α ]ᵗ
  ƛ_   : ∀ {α β} -> Γ ▻ α ⊢ β -> Γ ⊢ α ⇒ β
  _·_  : ∀ {α β} -> Γ ⊢ α ⇒ β -> Γ ⊢ α -> Γ ⊢ β
  iwrap  : ∀ {κ ψ} {α : Θ ⊢ᵗ κ} -> Γ ⊢ Core.unfold ψ α -> Γ ⊢ μ ψ α
  unwrap : ∀ {κ ψ} {α : Θ ⊢ᵗ κ} -> Γ ⊢ μ ψ α -> Γ ⊢ Core.unfold ψ α

mutual
  compile : ∀ {Θ} {Γ : Con (Star Θ)} {α} -> Γ ⊢ α -> Γ Core.⊢ α
  compile (letType α term)         = (Core.Λ (compile term)) Core.[ α ]
  compile (letTerm Δ rec env term) with rec
  ... | NonRec = Core.instNonRec (map-compile env) (compile term)
  ... | Rec    = Core.instRec    (map-compile env) (compile term)
  compile (var v)                  = Core.var v
  compile (Λ body)                 = Core.Λ (compile body)
  compile (fun [ α ])              = compile fun Core.[ α ]
  compile (ƛ body)                 = Core.ƛ (compile body)
  compile (fun · arg)              = compile fun Core.· compile arg
  compile (iwrap  term)            = Core.iwrap (compile term)
  compile (unwrap term)            = Core.unwrap (compile term)

  -- This is just `mapˢ compile` inlined to convince Agda there are no termination problems.
  map-compile : ∀ {Θ} {Γ Δ : Con (Star Θ)} -> Seq (Γ ⊢_) Δ -> Seq (Γ Core.⊢_) Δ
  map-compile  ø           = ø
  map-compile (seq ▶ term) = map-compile seq ▶ compile term

max_stars_repo_name: AriFordsham/plutus

max_issues_repo_name: AriFordsham/plutus

max_forks_repo_name: AriFordsham/plutus


text:
------------------------------------------------------------------------
-- Descending lists
--
-- We present some simple examples to demonstrate
--
-- 1. the concatenation operation on sorted lists obtained by
--    transporting the one on finite multisets, and
--
-- 2. "sorting" finite multisets by converting into sorted lists.
------------------------------------------------------------------------

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

module Cubical.Data.DescendingList.Examples where

open import Cubical.Foundations.Everything

open import Cubical.Data.Empty
open import Cubical.Data.Nat

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq

open import Cubical.HITs.FiniteMultiset

------------------------------------------------------------------------
-- The ordering relation on natural numbers
--
-- we work with the definition from the standard library.

infix 4 _≤_ _≥_

data _≤_ : ℕ → ℕ → Set where
 z≤n : ∀ {n}                 → zero  ≤ n
 s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

_≥_ : ℕ → ℕ → Set
m ≥ n = n ≤ m

≤pred : {n m : ℕ} → suc n ≤ suc m → n ≤ m
≤pred (s≤s r) = r

≥isPropValued : {n m : ℕ} → isProp (n ≥ m)
≥isPropValued z≤n z≤n = refl
≥isPropValued (s≤s p) (s≤s q) = cong s≤s (≥isPropValued p q)

≥dec : (x y : ℕ) → Dec (x ≥ y)
≥dec zero zero = yes z≤n
≥dec zero (suc y) = no (λ ())
≥dec (suc x) zero = yes z≤n
≥dec (suc x) (suc y) with ≥dec x y
≥dec (suc x) (suc y) | yes p = yes (s≤s p)
≥dec (suc x) (suc y) | no ¬p = no (λ r → ¬p (≤pred r))

≰→≥ : {x y : ℕ} → ¬ (x ≥ y) → y ≥ x
≰→≥ {zero} {y} f = z≤n
≰→≥ {suc x} {zero} f = ⊥-elim (f z≤n)
≰→≥ {suc x} {suc y} f = s≤s (≰→≥ λ g → f (s≤s g))

≥trans : {x y z : ℕ} → x ≥ y → y ≥ z → x ≥ z
≥trans z≤n z≤n = z≤n
≥trans (s≤s r) z≤n = z≤n
≥trans (s≤s r) (s≤s s) = s≤s (≥trans r s)

≤≥→≡ : {x y : ℕ} → x ≥ y → y ≥ x → x ≡ y
≤≥→≡ z≤n z≤n = refl
≤≥→≡ (s≤s r) (s≤s s) = cong suc (≤≥→≡ r s)

open import Cubical.Data.DescendingList.Base ℕ _≥_
open import Cubical.Data.DescendingList.Properties ℕ _≥_
open isSetDL ≥isPropValued discreteℕ
open IsoToFMSet discreteℕ ≥dec ≥isPropValued ≥trans ≰→≥ ≤≥→≡

------------------------------------------------------------------------
-- A simple example of concatenating sorted lists

l1 : DL
l1 = cons 4 (cons 3 (cons 2 [] ≥ᴴ[]) (≥ᴴcons (s≤s (s≤s z≤n)))) (≥ᴴcons (s≤s (s≤s (s≤s z≤n))))

l2 : DL
l2 = cons 2 (cons 0 [] ≥ᴴ[]) (≥ᴴcons z≤n)

l3 : DL
l3 = l1 ++ᴰᴸ l2

ValueOfl3 : l3 ≡ cons 4 (cons 3 (cons 2 (cons 2 (cons 0 _ _) _) _) _) _
ValueOfl3 = refl

l3=l2++l1 : l3 ≡ l2 ++ᴰᴸ l1
l3=l2++l1 = refl

LongerExample :   l1 ++ᴰᴸ l2 ++ᴰᴸ l1 ++ᴰᴸ l1 ++ᴰᴸ l2
                ≡ l2 ++ᴰᴸ l1 ++ᴰᴸ l2 ++ᴰᴸ l1 ++ᴰᴸ l1
LongerExample = refl

------------------------------------------------------------------------
-- A simple example of sorting finite multisets

m1 : FMSet ℕ
m1 = 13 ∷ 9 ∷ 78 ∷ 31 ∷ 86 ∷ 3 ∷ 0 ∷ 99 ∷ []

m2 : FMSet ℕ
m2 = 3 ∷ 1 ∷ 4 ∷ 1 ∷ 5 ∷ 9 ∷ []

m3 : FMSet ℕ
m3 = toFMSet (toDL (m1 ++ m2))

ValueOfm3 :
        m3 ≡ 99 ∷ 86 ∷ 78 ∷ 31 ∷ 13 ∷ 9 ∷ 9 ∷ 5 ∷ 4 ∷ 3 ∷ 3 ∷ 1 ∷ 1 ∷ 0 ∷ []
ValueOfm3 = refl

ValueOfm1++m2 :
  m1 ++ m2 ≡ 13 ∷ 9 ∷ 78 ∷ 31 ∷ 86 ∷ 3 ∷ 0 ∷ 99 ∷ 3 ∷ 1 ∷ 4 ∷ 1 ∷ 5 ∷ 9 ∷ []
ValueOfm1++m2 = refl

m3=m1++m2 : m3 ≡ m1 ++ m2
m3=m1++m2 = toFMSet∘toDL≡id (m1 ++ m2)

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module UniDB where

open import UniDB.Morph.Depth public
open import UniDB.Morph.Pair public
open import UniDB.Morph.Reg public
open import UniDB.Morph.Shift public
open import UniDB.Morph.Shifts public
open import UniDB.Morph.ShiftsPrime public
open import UniDB.Morph.Sim public
open import UniDB.Morph.Star public
open import UniDB.Morph.StarPrime public
open import UniDB.Morph.Sub public
open import UniDB.Morph.Subs public
open import UniDB.Morph.Sum public
open import UniDB.Morph.Unit public
open import UniDB.Morph.Weaken public
open import UniDB.Morph.WeakenOne public
open import UniDB.Morph.WeakenPrime public
open import UniDB.Spec public
open import UniDB.Subst public
open import UniDB.Subst.Inst public
open import UniDB.Subst.Pair public
open import UniDB.Subst.Reg public
open import UniDB.Subst.Shifts public
open import UniDB.Subst.Star public
open import UniDB.Subst.StarPrime public
open import UniDB.Subst.Subs public
open import UniDB.Subst.Sum public

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


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

module CombiningProofs.Eta where

infix 7 _≡_
infix 5 ∃

postulate
  D   : Set
  ∃   : (A : D → Set) → Set
  _≡_ : D → D → Set

syntax ∃ (λ x → e) = ∃[ x ] e

postulate
  t₁ : ∀ d → ∃[ e ] d ≡ e
  t₂ : ∀ d → ∃ (_≡_ d)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module WrongDotPattern where

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

data NonZero : Nat -> Set where
  nonZ : (n : Nat) -> NonZero (suc n)

f : (n : Nat) -> NonZero n -> Nat
f .zero (nonZ n) = n


text:
-- {-# OPTIONS -v tc.polarity:15 #-}
module Issue166 where

open import Common.Size
open import Common.Prelude

module M (A : Set) where

  data SizedNat : {i : Size} → Set where
    zero : {i : Size} → SizedNat {↑ i}
    suc  : {i : Size} → SizedNat {i} → SizedNat {↑ i}

module M′ = M ⊥

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Prelude hiding (⊥)

module Implicits.Resolution.Infinite.Algorithm where

open import Data.Bool
open import Data.Unit.Base
open import Data.Maybe using (is-just; functor)
open import Coinduction
open import Data.Fin.Substitution
open import Data.Vec hiding (_>>=_)
open import Data.List hiding (monad)
open import Data.List.Any hiding (tail)
open import Data.Maybe hiding (monad; module Eq)

open import Implicits.Syntax
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Implicits.Syntax.Type.Unification
open import Implicits.Resolution.Termination

open import Category.Monad
open import Category.Functor
open import Category.Monad.Partiality as P
open import Category.Monad.Partiality.All
private module M {f} = RawMonad (monad {f})
private module MaybeFunctor {f} = RawFunctor (functor {f})
open import Induction.WellFounded
open import Induction.Nat

module _ where
  open P.Workaround

  m<-Acc : ∀ {m ν} → MetaType m ν → Set
  m<-Acc {m} {ν} r = Acc _m<_ (m , ν , r)

  mutual

    map-bool' : ∀ {A : Set} → A → Bool → Maybe A ⊥P
    map-bool' u true = now (just u)
    map-bool' u false = now nothing

    delayed-resolve' : ∀ {ν} (Δ : ICtx ν) a → Bool ⊥P
    delayed-resolve' Δ a = (later (♯ (resolve' Δ a)))

    resolve-context' : ∀ {ν m} (Δ : ICtx ν) a → (Maybe (Sub (flip MetaType ν) m zero)) →
                      (Maybe (Sub (flip MetaType ν) m zero)) ⊥P
    resolve-context' Δ a (just u) =
      (delayed-resolve' Δ (from-meta (MetaTypeMetaSubst._/_ a u)))
        >>= (map-bool' u)
    resolve-context' Δ a nothing = now nothing

    -- match' uses MetaType m ν instead of Type ν to be able to distinguish unification variables
    -- from other, non-unifiable tvars.
    -- The difference is subtle but the gist is that we can only unify variables that we open
    -- during matching. Any variables that are already open in the context are fixed.
    match-u' : ∀ {ν m} (Δ : ICtx ν) → (τ : SimpleType ν) → (r : MetaType m ν) →
               m<-Acc r →
              (Maybe (Sub (flip MetaType ν) m zero)) ⊥P
    -- For rule types we first check if b matches our query τ.
    -- If this is the case, we use the unifier to instantiate the unification vars in a and
    -- recursively try to resolve the result.
    match-u' {ν} {m} Δ τ (a ⇒ b) (acc f) =
      (match-u' Δ τ b (f _ (b-m<-a⇒b a b))) >>= (resolve-context' Δ a)

    -- On type vars we simply open it up, adding the tvar to the set of unification variables.
    -- and recursively try to match.
    match-u' Δ τ (∀' a) (acc f) = (match-u' Δ τ (open-meta a) (f _ (open-meta-a-m<-∀'a a))) >>=
      (now ∘ (MaybeFunctor._<$>_ tail))

    -- The only thing left to do is to try and unify τ and x.
    match-u' Δ τ (simpl x) _ = now (mgu (simpl x) τ)

    match' : ∀ {ν} (Δ : ICtx ν) → (τ : SimpleType ν) → Type ν → Bool ⊥P
    match' {ν} Δ τ r = match-u' Δ τ (to-meta {zero} r) (m<-well-founded _) >>= (now ∘ is-just)

    match1st-recover' : ∀ {ν} (Δ ρs : ICtx ν) → (τ : SimpleType ν) → Bool → Bool ⊥P
    match1st-recover' _ _ _ true = now true
    match1st-recover' Δ ρs τ false = match1st' Δ ρs τ

    match1st' : ∀ {ν} (Δ : ICtx ν) → (ρs : ICtx ν) → (τ : SimpleType ν) → Bool ⊥P
    match1st' Δ List.[] _ = now false
    match1st' Δ (x List.∷ ρs) τ = match' Δ τ x >>= (match1st-recover' Δ ρs τ)

    -- resolution in ResP
    resolve' : ∀ {ν} (Δ : ICtx ν) (a : Type ν) → Bool ⊥P
    resolve' Δ (simpl x) = match1st' Δ Δ x
    resolve' Δ (a ⇒ b) = resolve' (a List.∷ Δ) b
    resolve' Δ (∀' a) = resolve' (ictx-weaken Δ) a

module _ where
  open P.Workaround using (⟦_⟧P)
  open P.Workaround.Correct
  open M

  module Eq {l} {A : Set l} where
    open import Relation.Binary.PropositionalEquality as PEq using (_≡_) public
    open module Eq = P.Equality  {A = A} _≡_ public
    open module R  = P.Reasoning (PEq.isEquivalence {A = A}) public

  map-bool : ∀ {A : Set} → A → Bool → (Maybe A) ⊥
  map-bool x b = ⟦ map-bool' x b ⟧P

  delayed-resolve : ∀ {ν} (Δ : ICtx ν) a → Bool ⊥
  delayed-resolve Δ a = ⟦ delayed-resolve' Δ a ⟧P

  resolve-context : ∀ {ν m} (Δ : ICtx ν) a → (Maybe (Sub (flip MetaType ν) m zero)) →
                      (Maybe (Sub (flip MetaType ν) m zero)) ⊥
  resolve-context Δ a p = ⟦ resolve-context' Δ a p ⟧P

  match-u : ∀ {ν m} (Δ : ICtx ν) → SimpleType ν → (r : MetaType m ν) → m<-Acc r →
            (Maybe (Sub (flip MetaType ν) m zero)) ⊥
  match-u Δ τ r f = ⟦ match-u' Δ τ r f ⟧P

  match : ∀ {ν} (Δ : ICtx ν) → (τ : SimpleType ν) → (r : Type ν) → Bool ⊥
  match Δ τ r = ⟦ match' Δ τ r ⟧P

  match1st-recover : ∀ {ν} (Δ : ICtx ν) → (ρs : ICtx ν) → (τ : SimpleType ν) → Bool → Bool ⊥
  match1st-recover Δ ρs τ b = ⟦ match1st-recover' Δ ρs τ b ⟧P

  match1st : ∀ {ν} (Δ : ICtx ν) → (ρs : ICtx ν) → (τ : SimpleType ν) → Bool ⊥
  match1st Δ ρs τ = ⟦ match1st' Δ ρs τ ⟧P

  resolve : ∀ {ν} (Δ : ICtx ν) (r : Type ν) → Bool ⊥
  resolve Δ r = ⟦ resolve' Δ r ⟧P

  --
  -- compositionality of resolution functions
  --

  resolve-context-comp : ∀ {m ν} (Δ : ICtx ν) a u →
                        (resolve-context {ν} {m} Δ a (just u))
                          Eq.≅
                        (delayed-resolve Δ (from-meta (MetaTypeMetaSubst._/_ a u))
                          >>= (map-bool u))
  resolve-context-comp {m} {ν} Δ a u =
    (resolve-context {ν} {m} Δ a (just u))
      Eq.≅⟨ >>=-hom (delayed-resolve' Δ (from-meta (MetaTypeMetaSubst._/_ a u))) _ ⟩
    (delayed-resolve Δ (from-meta (MetaTypeMetaSubst._/_ a u)) >>= (map-bool u)) Eq.∎

  match-u-iabs-comp : ∀ {m ν} (Δ : ICtx ν) τ (a b : MetaType m ν) f →
                      (match-u Δ τ (a ⇒ b) (acc f))
                        Eq.≅
                      ((match-u Δ τ b (f _ (b-m<-a⇒b a b))) >>= (resolve-context Δ a))
  match-u-iabs-comp Δ τ a b f =
    (match-u Δ τ (a ⇒ b) (acc f))
      Eq.≅⟨ >>=-hom (match-u' Δ τ b (f _ (b-m<-a⇒b a b))) _ ⟩
    ((match-u Δ τ b (f _ (b-m<-a⇒b a b))) >>= (resolve-context Δ a)) Eq.∎

  match-u-tabs-comp : ∀ {m ν} (Δ : ICtx ν) τ (r : MetaType m (suc ν)) f →
                                  (match-u Δ τ (∀' r) (acc f))
                                    Eq.≅
                                  ((match-u Δ τ (open-meta r) (f _ (open-meta-a-m<-∀'a r))) >>=
                                    (now ∘ (MaybeFunctor._<$>_ tail)))
  match-u-tabs-comp Δ τ r f =
    match-u Δ τ (∀' r) (acc f)
      Eq.≅⟨ >>=-hom (match-u' Δ τ (open-meta r) (f _ (open-meta-a-m<-∀'a r))) _ ⟩
    ((match-u Δ τ (open-meta r) (f _ (open-meta-a-m<-∀'a r))) >>= (now ∘ (MaybeFunctor._<$>_ tail))) Eq.∎

  match-comp : ∀ {ν} (Δ : ICtx ν) τ r →
               match Δ τ r
                 Eq.≅
               ((match-u Δ τ (to-meta {zero} r) (m<-well-founded _)) >>= (now ∘ is-just))
  match-comp Δ τ r =
    match Δ τ r
      Eq.≅⟨ >>=-hom (match-u' Δ τ (to-meta {zero} r) (m<-well-founded _)) _ ⟩
    _>>=_ (match-u Δ τ (to-meta {zero} r) (m<-well-founded _)) (now ∘ is-just) Eq.∎

  match1st-comp : ∀ {ν} (Δ : ICtx ν) x ρs τ → match1st Δ (x List.∷ ρs) τ Eq.≅ ((match Δ τ x) >>=
                    (match1st-recover Δ ρs τ))
  match1st-comp Δ x ρs τ =
    match1st Δ (x List.∷ ρs) τ
      Eq.≅⟨ >>=-hom (match' Δ τ x) _ ⟩
    ((match Δ τ x) >>= (match1st-recover Δ ρs τ)) Eq.∎


text:
module RAdjunctions where

open import Library
open import Categories
open import Functors

open Cat
open Fun

record RAdj {a b c d e f}{C : Cat {a}{b}}{D : Cat {c}{d}}
            (J : Fun C D)(E : Cat {e}{f}) : Set (a ⊔ b ⊔ c ⊔ d ⊔ e ⊔ f) where
  constructor radjunction
  field L        : Fun C E
        R        : Fun E D
        left     : {X : Obj C}{Y : Obj E} →
                    Hom E (OMap L X) Y → Hom D (OMap J X) (OMap R Y)
        right    : {X : Obj C}{Y : Obj E} →
                   Hom D (OMap J X) (OMap R Y) → Hom E (OMap L X) Y
        lawa     : {X : Obj C}{Y : Obj E}(f : Hom E (OMap L X) Y) →
                   right (left f) ≅ f
        lawb     : {X : Obj C}{Y : Obj E}(f : Hom D (OMap J X) (OMap R Y)) →
                    left (right f) ≅ f
        natleft  : {X X' : Obj C}{Y Y' : Obj E}
                   (f : Hom C X' X)(g : Hom E Y Y')
                   (h : Hom E (OMap L X) Y) →
                   comp D (HMap R g) (comp D (left h) (HMap J f))
                   ≅
                   left (comp E g (comp E h (HMap L f)))
        natright : {X X' : Obj C}{Y Y' : Obj E}
                   (f : Hom C X' X)(g : Hom E Y Y')
                   (h : Hom D (OMap J X) (OMap R Y)) →
                   right (comp D (HMap R g) (comp D h (HMap J f)))
                   ≅
                   comp E g (comp E (right h) (HMap L f))

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
------------------------------------------------------------------------
-- Some negative results related to weak bisimilarity and expansion
------------------------------------------------------------------------

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

open import Prelude
open import Prelude.Size

module Delay-monad.Sized.Bisimilarity.Negative
  {a} {A : Size → Type a} where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)

open import Function-universe equality-with-J hiding (id; _∘_)

open import Delay-monad.Sized
open import Delay-monad.Sized.Bisimilarity
open import Delay-monad.Sized.Termination

------------------------------------------------------------------------
-- Lemmas stating that functions of certain types cannot be defined if
-- ∀ i → A i is inhabited

-- An abbreviation. (Note that, because pattern-matching lambdas like
-- the one in this definition are—at least at the time of
-- writing—compared by "name", Agda rejects the code that one gets if
-- this abbreviation is inlined below.)

later-now : (∀ i → A i) → ∀ {i} → Delay A i
later-now x = later λ { .force {j} → now (x j) }

-- If now (x ∞) is an expansion of later-now x for every
-- x : ∀ i → A i, then ∀ i → A i is uninhabited.

Now≳later-now = (x : ∀ i → A i) → now (x ∞) ≳ later-now x

now≳later-now→uninhabited : Now≳later-now → ¬ (∀ i → A i)
now≳later-now→uninhabited =
  Now≳later-now  ↝⟨ (λ hyp x → case hyp x of λ ()) ⟩□
  ¬ (∀ i → A i)  □

-- If a variant of laterˡ⁻¹ for (fully defined) expansion can be
-- defined, then ∀ i → A i is uninhabited.

Laterˡ⁻¹-≳ = ∀ {x} {y : Delay A ∞} → later x ≳ y → force x ≳ y

laterˡ⁻¹-≳→uninhabited : Laterˡ⁻¹-≳ → ¬ (∀ i → A i)
laterˡ⁻¹-≳→uninhabited =
  Laterˡ⁻¹-≳     ↝⟨ (λ hyp _ → hyp (reflexive _)) ⟩
  Now≳later-now  ↝⟨ now≳later-now→uninhabited ⟩□
  ¬ (∀ i → A i)  □

-- If the following variants of transitivity can be proved, then
-- ∀ i → A i is uninhabited.

Transitivity-≈≳≳ = {x y z : Delay A ∞} → x ≈ y → y ≳ z → x ≳ z
Transitivity-≳≈≳ = {x y z : Delay A ∞} → x ≳ y → y ≈ z → x ≳ z

transitive-≈≳≳→uninhabited : Transitivity-≈≳≳ → ¬ (∀ i → A i)
transitive-≈≳≳→uninhabited =
  Transitivity-≈≳≳  ↝⟨ (λ trans → trans (laterʳ (reflexive _))) ⟩
  Laterˡ⁻¹-≳        ↝⟨ laterˡ⁻¹-≳→uninhabited ⟩□
  ¬ (∀ i → A i)     □

transitive-≳≈≳→uninhabited : Transitivity-≳≈≳ → ¬ (∀ i → A i)
transitive-≳≈≳→uninhabited =
  Transitivity-≳≈≳  ↝⟨ (λ trans x → later⁻¹ {y = λ { .force → later-now x }}
                                            (trans (reflexive _) (laterʳ (reflexive _)))) ⟩
  Now≳later-now     ↝⟨ now≳later-now→uninhabited ⟩□
  ¬ (∀ i → A i)     □

------------------------------------------------------------------------
-- Lemmas stating that certain size-preserving functions cannot be
-- defined if ∀ i → A i is inhabited, and related results

-- If a variant of laterˡ⁻¹ in which one occurrence of weak
-- bisimilarity is replaced by strong bisimilarity, and both arguments
-- are specialised, can be made size-preserving, then ∀ i → A i is
-- uninhabited.
--
-- This lemma is used to prove all other similar results below
-- (directly or indirectly).

Laterˡ⁻¹-∼≈ = ∀ {i} (x : ∀ i → A i) →
              [ i ] later (λ { .force {j = j} → now (x j) }) ∼ never →
              [ i ] now {A = A} (x ∞)                        ≈ never

size-preserving-laterˡ⁻¹-∼≈→uninhabited :
  Laterˡ⁻¹-∼≈ → ¬ (∀ i → A i)
size-preserving-laterˡ⁻¹-∼≈→uninhabited laterˡ⁻¹-∼≈ x =
  contradiction ∞
  where

  mutual

    now≈never : ∀ {i} → [ i ] now (x ∞) ≈ never
    now≈never = laterˡ⁻¹-∼≈ x (later now∼never)

    now∼never : ∀ {i} → [ i ] now (x ∞) ∼′ never
    force now∼never {j = j} = ⊥-elim (contradiction j)

    contradiction : Size → ⊥
    contradiction i = now≉never (now≈never {i = i})

-- A logically equivalent variant of Laterˡ⁻¹-∼≈ which it is sometimes
-- easier to work with.

Laterˡ⁻¹-∼≈′ = ∀ {i} (x : ∀ i → A i) →
               [ i ] later (record { force = λ {j} → now (x j) }) ∼ never →
               [ i ] now {A = A} (x ∞)                            ≈ never

size-preserving-laterˡ⁻¹-∼≈⇔size-preserving-laterˡ⁻¹-∼≈′ :
  Laterˡ⁻¹-∼≈ ⇔ Laterˡ⁻¹-∼≈′
size-preserving-laterˡ⁻¹-∼≈⇔size-preserving-laterˡ⁻¹-∼≈′ = record
  { to   = λ laterˡ⁻¹ x → laterˡ⁻¹ x ∘ transitive-∼ˡ (later λ { .force → now })
  ; from = λ laterˡ⁻¹ x → laterˡ⁻¹ x ∘ transitive-∼ˡ (later λ { .force → now })
  }

-- The type Laterˡ⁻¹-∼≈′ is logically equivalent to the similar type
-- Laterʳ⁻¹-∼≈′.

Laterʳ⁻¹-∼≈′ = ∀ {i} (x : ∀ i → A i) →
               [ i ] never ∼ later (record { force = λ {j} → now (x j) }) →
               [ i ] never ≈ now {A = A} (x ∞)

size-preserving-laterˡ⁻¹-∼≈′⇔size-preserving-laterʳ⁻¹-∼≈′ :
  Laterˡ⁻¹-∼≈′ ⇔ Laterʳ⁻¹-∼≈′
size-preserving-laterˡ⁻¹-∼≈′⇔size-preserving-laterʳ⁻¹-∼≈′ =
  record { to   = λ laterˡ⁻¹ {_} _ → symmetric ∘ laterˡ⁻¹ _ ∘ symmetric
         ; from = λ laterʳ⁻¹ {_} _ → symmetric ∘ laterʳ⁻¹ _ ∘ symmetric
         }

-- The type Laterʳ⁻¹-∼≈′ is logically equivalent to the similar type
-- Laterʳ⁻¹-∼≳′.

Laterʳ⁻¹-∼≳′ = ∀ {i} (x : ∀ i → A i) →
               [ i ] never ∼ later (record { force = λ {j} → now (x j) }) →
               [ i ] never ≳ now {A = A} (x ∞)

size-preserving-laterʳ⁻¹-∼≈′⇔size-preserving-laterʳ⁻¹-∼≳′ :
  Laterʳ⁻¹-∼≈′ ⇔ Laterʳ⁻¹-∼≳′
size-preserving-laterʳ⁻¹-∼≈′⇔size-preserving-laterʳ⁻¹-∼≳′ =
  record { to   = λ laterʳ⁻¹ {_} _ → ≈→-now ∘ laterʳ⁻¹ _
         ; from = λ laterʳ⁻¹ {_} _ → ≳→     ∘ laterʳ⁻¹ _
         }

-- If Laterʳ⁻¹-∼≳′ is inhabited, then ∀ i → A i is uninhabited.

size-preserving-laterʳ⁻¹-∼≳′→uninhabited : Laterʳ⁻¹-∼≳′ → ¬ (∀ i → A i)
size-preserving-laterʳ⁻¹-∼≳′→uninhabited =
  Laterʳ⁻¹-∼≳′   ↝⟨ _⇔_.from size-preserving-laterʳ⁻¹-∼≈′⇔size-preserving-laterʳ⁻¹-∼≳′ ⟩
  Laterʳ⁻¹-∼≈′   ↝⟨ _⇔_.from size-preserving-laterˡ⁻¹-∼≈′⇔size-preserving-laterʳ⁻¹-∼≈′ ⟩
  Laterˡ⁻¹-∼≈′   ↝⟨ _⇔_.from size-preserving-laterˡ⁻¹-∼≈⇔size-preserving-laterˡ⁻¹-∼≈′ ⟩
  Laterˡ⁻¹-∼≈    ↝⟨ size-preserving-laterˡ⁻¹-∼≈→uninhabited ⟩□
  ¬ (∀ i → A i)  □

-- Having a size-preserving variant of laterˡ⁻¹ is logically
-- equivalent to having a size-preserving variant of laterʳ⁻¹ (for
-- weak bisimilarity).

Laterˡ⁻¹-≈ = ∀ {i x} {y : Delay A ∞} →
             [ i ] later x ≈ y →
             [ i ] force x ≈ y

Laterʳ⁻¹-≈ = ∀ {i} {x : Delay A ∞} {y} →
             [ i ] x ≈ later y →
             [ i ] x ≈ force y

size-preserving-laterˡ⁻¹-≈⇔size-preserving-laterʳ⁻¹-≈ :
  Laterˡ⁻¹-≈ ⇔ Laterʳ⁻¹-≈
size-preserving-laterˡ⁻¹-≈⇔size-preserving-laterʳ⁻¹-≈ = record
  { to   = λ laterʳ⁻¹ → symmetric ∘ laterʳ⁻¹ ∘ symmetric
  ; from = λ laterˡ⁻¹ → symmetric ∘ laterˡ⁻¹ ∘ symmetric
  }

-- If laterˡ⁻¹ can be made size-preserving, then ∀ i → A i is
-- uninhabited.

size-preserving-laterˡ⁻¹-≈→uninhabited : Laterˡ⁻¹-≈ → ¬ (∀ i → A i)
size-preserving-laterˡ⁻¹-≈→uninhabited =
  Laterˡ⁻¹-≈     ↝⟨ (λ laterˡ⁻¹ _ → laterˡ⁻¹ ∘ ∼→) ⟩
  Laterˡ⁻¹-∼≈    ↝⟨ size-preserving-laterˡ⁻¹-∼≈→uninhabited ⟩□
  ¬ (∀ i → A i)  □

-- If laterʳ⁻¹ can be made size-preserving for expansion, then
-- ∀ i → A i is uninhabited.

Laterʳ⁻¹-≳ = ∀ {i} {x : Delay A ∞} {y} →
             [ i ] x ≳ later y →
             [ i ] x ≳ force y

size-preserving-laterʳ⁻¹-≳→uninhabited : Laterʳ⁻¹-≳ → ¬ (∀ i → A i)
size-preserving-laterʳ⁻¹-≳→uninhabited =
  Laterʳ⁻¹-≳     ↝⟨ (λ laterʳ⁻¹ {_} _ p → laterʳ⁻¹ (∼→ p)) ⟩
  Laterʳ⁻¹-∼≳′   ↝⟨ size-preserving-laterʳ⁻¹-∼≳′→uninhabited ⟩□
  ¬ (∀ i → A i)  □

-- If a variant of ⇓-respects-≈ in which _≈_ is replaced by _∼_ can be
-- made size-preserving in the second argument, then ∀ i → A i is
-- uninhabited.

⇓-Respects-∼ʳ = ∀ {i} {x y : Delay A ∞} {z} →
                x ⇓ z → [ i ] x ∼ y → Terminates i y z

size-preserving-⇓-respects-∼ʳ→uninhabited :
  ⇓-Respects-∼ʳ → ¬ (∀ i → A i)
size-preserving-⇓-respects-∼ʳ→uninhabited =
  ⇓-Respects-∼ʳ  ↝⟨ (λ resp _ → resp (laterʳ now)) ⟩
  Laterˡ⁻¹-∼≈    ↝⟨ size-preserving-laterˡ⁻¹-∼≈→uninhabited ⟩□
  ¬ (∀ i → A i)  □

-- If ⇓-respects-≈ can be made size-preserving in the second argument,
-- then ∀ i → A i is uninhabited.

⇓-Respects-≈ʳ = ∀ {i} {x y : Delay A ∞} {z} →
                x ⇓ z → [ i ] x ≈ y → Terminates i y z

size-preserving-⇓-respects-≈ʳ→uninhabited :
  ⇓-Respects-≈ʳ → ¬ (∀ i → A i)
size-preserving-⇓-respects-≈ʳ→uninhabited =
  ⇓-Respects-≈ʳ  ↝⟨ (λ trans x⇓z → trans x⇓z ∘ ∼→) ⟩
  ⇓-Respects-∼ʳ  ↝⟨ size-preserving-⇓-respects-∼ʳ→uninhabited ⟩□
  ¬ (∀ i → A i)  □

-- Having a transitivity-like proof, taking weak bisimilarity and
-- strong bisimilarity to weak bisimilarity, that preserves the size
-- of the second argument, is logically equivalent to having a
-- transitivity-like proof, taking strong bisimilarity and weak
-- bisimilarity to weak bisimilarity, that preserves the size of the
-- first argument.

Transitivity-≈∼ʳ = ∀ {i} {x y z : Delay A ∞} →
                   x ≈ y → [ i ] y ∼ z → [ i ] x ≈ z

Transitivity-∼≈ˡ = ∀ {i} {x y z : Delay A ∞} →
                   [ i ] x ∼ y → y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-≈∼ʳ⇔size-preserving-transitivity-∼≈ˡ :
  Transitivity-≈∼ʳ ⇔ Transitivity-∼≈ˡ
size-preserving-transitivity-≈∼ʳ⇔size-preserving-transitivity-∼≈ˡ =
  record
    { to   = λ trans p q → symmetric (trans (symmetric q) (symmetric p))
    ; from = λ trans p q → symmetric (trans (symmetric q) (symmetric p))
    }

-- If there is a transitivity-like proof, taking weak bisimilarity and
-- strong bisimilarity to weak bisimilarity, that preserves the size
-- of the second argument, then ∀ i → A i is uninhabited.

size-preserving-transitivity-≈∼ʳ→uninhabited :
  Transitivity-≈∼ʳ → ¬ (∀ i → A i)
size-preserving-transitivity-≈∼ʳ→uninhabited =
  Transitivity-≈∼ʳ  ↝⟨ (λ trans → trans) ⟩
  ⇓-Respects-∼ʳ     ↝⟨ size-preserving-⇓-respects-∼ʳ→uninhabited ⟩
  ¬ (∀ i → A i)     □

-- If there is a transitivity-like proof, taking strong bisimilarity
-- and expansion to expansion, that preserves the size of the first
-- argument, then ∀ i → A i is uninhabited.

Transitivity-∼≳ˡ = ∀ {i} {x y z : Delay A ∞} →
                   [ i ] x ∼ y → y ≳ z → [ i ] x ≳ z

size-preserving-transitivity-∼≳ˡ→uninhabited :
  Transitivity-∼≳ˡ → ¬ (∀ i → A i)
size-preserving-transitivity-∼≳ˡ→uninhabited =
  Transitivity-∼≳ˡ  ↝⟨ (λ trans _ p → trans p (laterˡ now)) ⟩
  Laterʳ⁻¹-∼≳′      ↝⟨ size-preserving-laterʳ⁻¹-∼≳′→uninhabited ⟩
  ¬ (∀ i → A i)     □

-- Having a transitivity proof for weak bisimilarity that preserves
-- the size of the first argument is logically equivalent to having
-- one that preserves the size of the second argument.

Transitivity-≈ˡ = ∀ {i} {x y z : Delay A ∞} →
                  [ i ] x ≈ y → y ≈ z → [ i ] x ≈ z

Transitivity-≈ʳ = ∀ {i} {x y z : Delay A ∞} →
                x ≈ y → [ i ] y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-≈ˡ⇔size-preserving-transitivity-≈ʳ :
  Transitivity-≈ˡ ⇔ Transitivity-≈ʳ
size-preserving-transitivity-≈ˡ⇔size-preserving-transitivity-≈ʳ = record
  { to   = λ trans p q → symmetric (trans (symmetric q) (symmetric p))
  ; from = λ trans p q → symmetric (trans (symmetric q) (symmetric p))
  }

-- If there is a transitivity proof for weak bisimilarity that
-- preserves the size of the second argument, then ∀ i → A i is
-- uninhabited.

size-preserving-transitivity-≈ʳ→uninhabited :
  Transitivity-≈ʳ → ¬ (∀ i → A i)
size-preserving-transitivity-≈ʳ→uninhabited =
  Transitivity-≈ʳ  ↝⟨ (λ trans → trans) ⟩
  ⇓-Respects-≈ʳ    ↝⟨ size-preserving-⇓-respects-≈ʳ→uninhabited ⟩□
  ¬ (∀ i → A i)    □

-- If there is a transitivity proof for expansion that preserves the
-- size of the first argument, then ∀ i → A i is uninhabited.

Transitivity-≳ˡ = ∀ {i} {x y z : Delay A ∞} →
                  [ i ] x ≳ y → y ≳ z → [ i ] x ≳ z

size-preserving-transitivity-≳ˡ→uninhabited :
  Transitivity-≳ˡ → ¬ (∀ i → A i)
size-preserving-transitivity-≳ˡ→uninhabited =
  Transitivity-≳ˡ   ↝⟨ (λ trans → trans ∘ ∼→) ⟩
  Transitivity-∼≳ˡ  ↝⟨ size-preserving-transitivity-∼≳ˡ→uninhabited ⟩□
  ¬ (∀ i → A i)     □

-- If there is a fully size-preserving transitivity proof for weak
-- bisimilarity, then ∀ i → A i is uninhabited.

Transitivity-≈ = ∀ {i} {x y z : Delay A ∞} →
                 [ i ] x ≈ y → [ i ] y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-≈→uninhabited :
  Transitivity-≈ → ¬ (∀ i → A i)
size-preserving-transitivity-≈→uninhabited =
  Transitivity-≈   ↝⟨ (λ trans → trans) ⟩
  Transitivity-≈ʳ  ↝⟨ size-preserving-transitivity-≈ʳ→uninhabited ⟩□
  ¬ (∀ i → A i)    □

-- If there is a fully size-preserving transitivity proof for
-- expansion, then ∀ i → A i is uninhabited.

Transitivity-≳ = ∀ {i} {x y z : Delay A ∞} →
                 [ i ] x ≳ y → [ i ] y ≳ z → [ i ] x ≳ z

size-preserving-transitivity-≳→uninhabited :
  Transitivity-≳ → ¬ (∀ i → A i)
size-preserving-transitivity-≳→uninhabited =
  Transitivity-≳   ↝⟨ (λ trans → trans) ⟩
  Transitivity-≳ˡ  ↝⟨ size-preserving-transitivity-≳ˡ→uninhabited ⟩□
  ¬ (∀ i → A i)    □

-- There is a transitivity-like proof, taking expansion and weak
-- bisimilarity to weak bisimilarity, that preserves the size of the
-- first argument, iff there is a transitivity-like proof, taking weak
-- bisimilarity and the converse of expansion to weak bisimilarity,
-- that preserves the size of the second argument.

Transitivity-≳≈ˡ = ∀ {i} {x y z : Delay A ∞} →
                   [ i ] x ≳ y → y ≈ z → [ i ] x ≈ z

Transitivity-≈≲ʳ = ∀ {i} {x y z : Delay A ∞} →
                   x ≈ y → [ i ] y ≲ z → [ i ] x ≈ z

size-preserving-transitivity-≳≈ˡ⇔size-preserving-transitivity-≈≲ʳ :
  Transitivity-≳≈ˡ ⇔ Transitivity-≈≲ʳ
size-preserving-transitivity-≳≈ˡ⇔size-preserving-transitivity-≈≲ʳ =
  record
    { to   = λ trans x≈y y≲z → symmetric (trans y≲z (symmetric x≈y))
    ; from = λ trans x≳y y≈z → symmetric (trans (symmetric y≈z) x≳y)
    }

-- If there is a transitivity-like proof, taking expansion and weak
-- bisimilarity to weak bisimilarity, that preserves the size of the
-- first argument, then ∀ i → A i is uninhabited.

size-preserving-transitivity-≳≈ˡ→uninhabited :
  Transitivity-≳≈ˡ → ¬ (∀ i → A i)
size-preserving-transitivity-≳≈ˡ→uninhabited =
  Transitivity-≳≈ˡ  ↝⟨ _∘ ∼→ ⟩
  Transitivity-∼≈ˡ  ↝⟨ _⇔_.from size-preserving-transitivity-≈∼ʳ⇔size-preserving-transitivity-∼≈ˡ ⟩
  Transitivity-≈∼ʳ  ↝⟨ size-preserving-transitivity-≈∼ʳ→uninhabited ⟩□
  ¬ (∀ i → A i)     □

-- There is a transitivity-like proof, taking expansion and weak
-- bisimilarity to weak bisimilarity, that preserves the size of both
-- arguments, iff there is a transitivity-like proof, taking weak
-- bisimilarity and the converse of expansion to weak bisimilarity,
-- that also preserves the size of both arguments.

Transitivity-≳≈ = ∀ {i} {x y z : Delay A ∞} →
                  [ i ] x ≳ y → [ i ] y ≈ z → [ i ] x ≈ z

Transitivity-≈≲ = ∀ {i} {x y z : Delay A ∞} →
                  [ i ] x ≈ y → [ i ] y ≲ z → [ i ] x ≈ z

size-preserving-transitivity-≳≈⇔size-preserving-transitivity-≈≲ :
  Transitivity-≳≈ ⇔ Transitivity-≈≲
size-preserving-transitivity-≳≈⇔size-preserving-transitivity-≈≲ =
  record
    { to   = λ trans x≈y y≲z → symmetric (trans y≲z (symmetric x≈y))
    ; from = λ trans x≳y y≈z → symmetric (trans (symmetric y≈z) x≳y)
    }

-- If there is a transitivity-like proof, taking expansion and weak
-- bisimilarity to weak bisimilarity, that preserves the size of both
-- arguments, then ∀ i → A i is uninhabited.

size-preserving-transitivity-≳≈→uninhabited :
  Transitivity-≳≈ → ¬ (∀ i → A i)
size-preserving-transitivity-≳≈→uninhabited =
  Transitivity-≳≈   ↝⟨ (λ trans → trans) ⟩
  Transitivity-≳≈ˡ  ↝⟨ size-preserving-transitivity-≳≈ˡ→uninhabited ⟩□
  ¬ (∀ i → A i)     □

-- If there is a transitivity-like proof, taking weak bisimilarity and
-- expansion to weak bisimilarity, that preserves the size of the
-- first argument, then ∀ i → A i is uninhabited.

Transitivity-≈≳ˡ = ∀ {i} {x y z : Delay A ∞} →
                   [ i ] x ≈ y → y ≳ z → [ i ] x ≈ z

size-preserving-transitivity-≈≳ˡ→uninhabited :
  Transitivity-≈≳ˡ → ¬ (∀ i → A i)
size-preserving-transitivity-≈≳ˡ→uninhabited =
  Transitivity-≈≳ˡ  ↝⟨ (λ trans {_ _ _} x≈ly → trans x≈ly (laterˡ (reflexive _))) ⟩
  Laterʳ⁻¹-≈        ↝⟨ _⇔_.from size-preserving-laterˡ⁻¹-≈⇔size-preserving-laterʳ⁻¹-≈ ⟩
  Laterˡ⁻¹-≈        ↝⟨ size-preserving-laterˡ⁻¹-≈→uninhabited ⟩
  ¬ (∀ i → A i)     □

------------------------------------------------------------------------
-- Lemmas stating that certain types are inhabited if A ∞ is
-- uninhabited

-- If A ∞ is uninhabited, then Now≳later-now is inhabited.

uninhabited→now≳later-now : ¬ A ∞ → Now≳later-now
uninhabited→now≳later-now =
  ¬ A ∞            ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≳ y)  ↝⟨ (λ trivial _ → trivial _ _) ⟩□
  Now≳later-now    □

-- If A ∞ is uninhabited, then a variant of laterˡ⁻¹ for (fully
-- defined) expansion can be defined.

uninhabited→laterˡ⁻¹-≳ : ¬ A ∞ → Laterˡ⁻¹-≳
uninhabited→laterˡ⁻¹-≳ =
  ¬ A ∞            ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≳ y)  ↝⟨ (λ trivial {_ _} _ → trivial _ _) ⟩□
  Laterˡ⁻¹-≳       □

-- If A ∞ is uninhabited, then a transitivity-like proof taking weak
-- bisimilarity and expansion to expansion can be defined.

uninhabited→transitivity-≈≳≳ : ¬ A ∞ → Transitivity-≈≳≳
uninhabited→transitivity-≈≳≳ =
  ¬ A ∞             ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≳ y)   ↝⟨ (λ trivial {_ _ _} _ _ → trivial _ _) ⟩□
  Transitivity-≈≳≳  □

-- If A ∞ is uninhabited, then a transitivity-like proof taking
-- expansion and weak bisimilarity to expansion can be defined.

uninhabited→transitivity-≳≈≳ : ¬ A ∞ → Transitivity-≳≈≳
uninhabited→transitivity-≳≈≳ =
  ¬ A ∞             ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≳ y)   ↝⟨ (λ trivial {_ _ _} _ _ → trivial _ _) ⟩□
  Transitivity-≳≈≳  □

-- If A ∞ is uninhabited, then Laterˡ⁻¹-∼≈ is inhabited.

uninhabited→size-preserving-laterˡ⁻¹-∼≈ : ¬ A ∞ → Laterˡ⁻¹-∼≈
uninhabited→size-preserving-laterˡ⁻¹-∼≈ =
  ¬ A ∞            ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_} _ _ → trivial _ _) ⟩□
  Laterˡ⁻¹-∼≈      □

-- If A ∞ is uninhabited, then laterˡ⁻¹ can be made size-preserving.

uninhabited→size-preserving-laterˡ⁻¹ : ¬ A ∞ → Laterˡ⁻¹-≈
uninhabited→size-preserving-laterˡ⁻¹ =
  ¬ A ∞            ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _} _ → trivial _ _) ⟩□
  Laterˡ⁻¹-≈       □

-- If A ∞ is uninhabited, then a variant of ⇓-respects-≈ in which _≈_
-- is replaced by _∼_ can be made size-preserving in the second
-- argument.

uninhabited→size-preserving-⇓-respects-∼ʳ : ¬ A ∞ → ⇓-Respects-∼ʳ
uninhabited→size-preserving-⇓-respects-∼ʳ =
  ¬ A ∞            ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
  ⇓-Respects-∼ʳ    □

-- If A ∞ is uninhabited, then ⇓-respects-≈ can be made
-- size-preserving in the second argument.

uninhabited→size-preserving-⇓-respects-≈ʳ : ¬ A ∞ → ⇓-Respects-≈ʳ
uninhabited→size-preserving-⇓-respects-≈ʳ =
  ¬ A ∞            ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
  ⇓-Respects-≈ʳ    □

-- If A ∞ is uninhabited, then there is a transitivity-like proof,
-- taking weak bisimilarity and strong bisimilarity to weak
-- bisimilarity, that preserves the size of the second argument.

uninhabited→size-preserving-transitivity-≈∼ʳ : ¬ A ∞ → Transitivity-≈∼ʳ
uninhabited→size-preserving-transitivity-≈∼ʳ =
  ¬ A ∞             ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≈ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
  Transitivity-≈∼ʳ  □

-- If A ∞ is uninhabited, then there is a transitivity-like proof,
-- taking strong bisimilarity and expansion to expansion, that
-- preserves the size of the first argument.

uninhabited→size-preserving-transitivity-∼≳ˡ : ¬ A ∞ → Transitivity-∼≳ˡ
uninhabited→size-preserving-transitivity-∼≳ˡ =
  ¬ A ∞             ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≳ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
  Transitivity-∼≳ˡ  □

-- If A ∞ is uninhabited, then there is a transitivity proof for weak
-- bisimilarity that preserves the size of the second argument.

uninhabited→size-preserving-transitivity-≈ʳ : ¬ A ∞ → Transitivity-≈ʳ
uninhabited→size-preserving-transitivity-≈ʳ =
  ¬ A ∞            ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
  Transitivity-≈ʳ  □

-- If A ∞ is uninhabited, then there is a transitivity proof for
-- expansion that preserves the size of the first argument.

uninhabited→size-preserving-transitivity-≳ˡ : ¬ A ∞ → Transitivity-≳ˡ
uninhabited→size-preserving-transitivity-≳ˡ =
  ¬ A ∞            ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≳ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
  Transitivity-≳ˡ  □

-- If A ∞ is uninhabited, then there is a fully size-preserving
-- transitivity proof for weak bisimilarity.

uninhabited→size-preserving-transitivity-≈ : ¬ A ∞ → Transitivity-≈
uninhabited→size-preserving-transitivity-≈ =
  ¬ A ∞            ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
  Transitivity-≈   □

-- If A ∞ is uninhabited, then there is a fully size-preserving
-- transitivity proof for expansion.

uninhabited→size-preserving-transitivity-≳ : ¬ A ∞ → Transitivity-≳
uninhabited→size-preserving-transitivity-≳ =
  ¬ A ∞            ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≳ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
  Transitivity-≳   □

-- If A ∞ is uninhabited, then there is a transitivity-like proof,
-- taking expansion and weak bisimilarity to weak bisimilarity, that
-- preserves the size of the first argument.

uninhabited→size-preserving-transitivity-≳≈ˡ : ¬ A ∞ → Transitivity-≳≈ˡ
uninhabited→size-preserving-transitivity-≳≈ˡ =
  ¬ A ∞             ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≈ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
  Transitivity-≳≈ˡ  □

-- If A ∞ is uninhabited, then there is a transitivity-like proof,
-- taking expansion and weak bisimilarity to weak bisimilarity, that
-- preserves the size of both arguments.

uninhabited→size-preserving-transitivity-≳≈ : ¬ A ∞ → Transitivity-≳≈
uninhabited→size-preserving-transitivity-≳≈ =
  ¬ A ∞            ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
  Transitivity-≳≈  □

-- If A ∞ is uninhabited, then there is a transitivity-like proof,
-- taking weak bisimilarity and expansion to weak bisimilarity, that
-- preserves the size of the first argument.

uninhabited→size-preserving-transitivity-≈≳ˡ : ¬ A ∞ → Transitivity-≈≳ˡ
uninhabited→size-preserving-transitivity-≈≳ˡ =
  ¬ A ∞             ↝⟨ uninhabited→trivial ⟩
  (∀ x y → x ≈ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
  Transitivity-≈≳ˡ  □

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


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

-- These examples should now go through with no unsolved metavariables.
-- They work since the conversion checker is a little less prone to
-- abort checking when there are constraints. In particular if the
-- constraints only affect the sorts of the things compared, then it keeps
-- going.
module Issue211 where

open import Common.Level

infixr 4 _,_
infixr 3 _×_

data _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  _,_ : A → B → A × B

data D₀ : Set₀ where
data D₁ : Set₁ where

-- Works:
ex₁ : (D₁ → D₁) × (D₁ → D₁)
ex₁ = ((λ d → d) , (λ d → d))

-- Works:

ex₂ : (D₀ → D₀) × (D₀ → D₀) × (D₀ → D₀)
ex₂ = ((λ d → d) , (λ d → d) , (λ d → d))

-- Works:

ex₃ : (D₁ → D₁) × (D₁ → D₁) × (D₁ → D₁)
ex₃ = ((λ d → d) , (λ (d : D₁) → d) , (λ (d : D₁) → d))

-- Does not work:

ex₄ : Level × (D₁ → D₁) × (D₁ → D₁)
ex₄ = lzero , (λ d → d) , (λ d → d)

ex₅ : (D₁ → D₁) × (D₁ → D₁) × (D₁ → D₁)
ex₅ = (λ (d : _) → d) , (λ (d : _) → d) , (λ (d : _) → d)

-- Does not work:

ex₆ : (D₁ → D₁) × (D₁ → D₁) × (D₁ → D₁)
ex₆ = (λ d → d) , (λ d → d) , (λ d → d)

-- As far as I can tell there is an easily found unique solution for
-- the unsolved meta-variables above. Why does not the unification
-- machinery find it? Are the meta-variables solved in the wrong
-- order?


text:
------------------------------------------------------------------------
-- This file contains the definition the category of functors indexed --
-- by two categories.                                                 --
------------------------------------------------------------------------
module Category.CatFunc where

open import Level

open import Category.NatTrans public

CatFunc : {l₁ l₂ : Level} → Cat {l₁} → Cat {l₂} → Cat {l₁ ⊔ l₂}
CatFunc ℂ₁ ℂ₂ = record
                  { Obj = Functor ℂ₁ ℂ₂
                  ; Hom = λ F G → record { el = NatTrans F G ; eq = λ α₁ α₂ → {!!} ; eqRpf = {!!} }
                  ; comp = {!!}
                  ; id = {!!}
                  ; assocPf = {!!}
                  ; idPfCom = {!!}
                  ; idPf = {!!}
                  }

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
open import FRP.LTL.Time using ( Time ; _≤_ ; _<_ )

module FRP.LTL.RSet.Core where

-- Reactive types

RSet : Set₁
RSet = Time → Set

⟨_⟩ : Set → RSet
⟨ A ⟩ t = A

⟦_⟧ : RSet → Set
⟦ A ⟧ = ∀ {t} → (A t)

-- Reactive sets over an interval

_[_,_] : RSet → Time → Time → Set
A [ s , u ] = ∀ {t} → s ≤ t → t ≤ u → A t

_[_,_⟩ : RSet → Time → Time → Set
A [ s , u ⟩ = ∀ {t} → s ≤ t → t < u → A t

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
module Progress where

open import Prelude
open import T

---- progress

module Progress where
  -- Define a datatype representing that a term satisfies progress
  data TProgress : ∀{A} → TCExp A → Set where
    prog-val : ∀{A} {e : TCExp A} → (D : TVal e) → TProgress e
    prog-step : ∀{A} {e e' : TCExp A} → (D : e ~> e') → TProgress e

  -- prove that all terms satisfy progress
  progress : ∀{A} (e : TCExp A) → TProgress e
  progress (var ())
  progress (Λ e) = prog-val val-lam
  progress (e₁ $ e₂) with progress e₁
  progress (e₁ $ e₂) | prog-step D = prog-step (step-app-l D)
  progress (.(Λ e) $ e₂) | prog-val (val-lam {_} {_} {e}) = prog-step step-beta
  progress zero = prog-val val-zero
  progress (suc e) with progress e
  ... | prog-val D = prog-val (val-suc D)
  ... | prog-step D' = prog-step (step-suc D')
  progress (rec e e₀ es) with progress e
  progress (rec .zero e₀ es) | prog-val val-zero = prog-step step-rec-z
  progress (rec .(suc _) e₀ es) | prog-val (val-suc  y) = prog-step (step-rec-s y)
  ... | prog-step D = prog-step (step-rec D)

open Progress public

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text:
module _ where

postulate
  I : Set

data P (i : I) : Set where
  p : P i → P i

data Q (i : I) : P i → Set where
  q : (x : P i) → Q i (p x)

module _ (i : I) (x : P i)  where
  g : Q _ x → Set₁
  g (q y) = Set


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}
{-# OPTIONS --allow-unsolved-metas #-}

module Light.Implementation.Data.Product where

open import Light.Library.Data.Product using (Library ; Dependencies)
open import Light.Variable.Levels
open import Light.Level using (_⊔_)
open import Light.Library.Relation.Binary.Equality.Decidable using (DecidableEquality)
open import Light.Variable.Sets
open import Light.Library.Relation.Binary.Equality using (wrap)

instance dependencies : Dependencies
dependencies = record {}

instance library : Library dependencies
library = record { Implementation }
      where
      module Implementation where
            record Σ (𝕒 : Set aℓ) (𝕓 : 𝕒 → Set bℓ) : Set (aℓ ⊔ bℓ) where
                  constructor both
                  field first : 𝕒
                  field second : 𝕓 first
            open Σ public

            equals :
                  ∀ ⦃ a‐c‐equals : DecidableEquality 𝕒 𝕔 ⦄ ⦃ b‐d‐equals : DecidableEquality 𝕓 𝕕 ⦄
                  → DecidableEquality (Σ 𝕒 (λ _ → 𝕓)) (Σ 𝕔 (λ _ → 𝕕))
            equals = {!!}

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


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

open import Level using (Level)
open import FLA.Algebra.Structures
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

module FLA.Algebra.Properties.Field {ℓ : Level } {A : Set ℓ} ⦃ F : Field A ⦄ where

open Field F

0ᶠ+0ᶠ≡0ᶠ : 0ᶠ + 0ᶠ ≡ 0ᶠ
0ᶠ+0ᶠ≡0ᶠ = +0ᶠ 0ᶠ

0ᶠ+ : (a : A) → 0ᶠ + a ≡ a
0ᶠ+ a rewrite +-comm 0ᶠ a = +0ᶠ a

a*0ᶠ≡0ᶠ : (a : A) → a * 0ᶠ ≡ 0ᶠ
a*0ᶠ≡0ᶠ a = begin
  a * 0ᶠ                  ≡˘⟨ 0ᶠ+ (a * 0ᶠ) ⟩
  0ᶠ + a * 0ᶠ             ≡⟨ cong (_+ a * 0ᶠ) (sym (+-inv a)) ⟩
  - a + a + a * 0ᶠ        ≡⟨ cong (λ x → - a + x + a * 0ᶠ) (sym (*1ᶠ a)) ⟩
  - a + a * 1ᶠ + a * 0ᶠ   ≡˘⟨ +-assoc (- a) (a * 1ᶠ) (a * 0ᶠ) ⟩
  - a + (a * 1ᶠ + a * 0ᶠ) ≡⟨ cong (- a +_) (sym (*-distr-+ a 1ᶠ 0ᶠ)) ⟩
  - a + (a * (1ᶠ + 0ᶠ))   ≡⟨ cong (λ x → - a + (a * x)) (+0ᶠ 1ᶠ) ⟩
  - a + (a * 1ᶠ)          ≡⟨ cong (- a +_) (*1ᶠ a) ⟩
  - a + a                 ≡⟨ +-inv a ⟩
  0ᶠ                      ∎

0ᶠ*a≡0ᶠ : (a : A) → 0ᶠ * a ≡ 0ᶠ
0ᶠ*a≡0ᶠ a = trans (*-comm 0ᶠ a) (a*0ᶠ≡0ᶠ a)

-a≡-1ᶠ*a : (a : A) → - a ≡ - 1ᶠ * a
-a≡-1ᶠ*a a = begin
  - a                        ≡˘⟨ +0ᶠ (- a) ⟩
  - a + 0ᶠ                   ≡⟨ cong (- a +_) (sym (a*0ᶠ≡0ᶠ a)) ⟩
  - a + (a * 0ᶠ)             ≡⟨ cong (λ x → - a + (a * x)) (sym (+-inv 1ᶠ)) ⟩
  - a + (a * (- 1ᶠ + 1ᶠ))    ≡⟨ cong (- a +_) (*-distr-+ a (- 1ᶠ) 1ᶠ) ⟩
  - a + (a * - 1ᶠ + a * 1ᶠ)  ≡⟨ cong (- a +_) (+-comm (a * - 1ᶠ) (a * 1ᶠ)) ⟩
  - a + (a * 1ᶠ + a * - 1ᶠ ) ≡⟨ +-assoc (- a) (a * 1ᶠ) (a * - 1ᶠ) ⟩
  - a + a * 1ᶠ + a * - 1ᶠ    ≡⟨ cong (λ x → - a + x + a * - 1ᶠ) (*1ᶠ a) ⟩
  - a + a + a * - 1ᶠ         ≡⟨ cong (_+ a * - 1ᶠ) (+-inv a) ⟩
  0ᶠ + a * - 1ᶠ              ≡⟨ 0ᶠ+ (a * - 1ᶠ) ⟩
  a * - 1ᶠ                   ≡⟨ *-comm a (- 1ᶠ) ⟩
  - 1ᶠ * a                   ∎

-a*b≡-[a*b] : (a b : A) → - a * b ≡ - (a * b)
-a*b≡-[a*b] a b = begin
  - a * b        ≡⟨ cong (_* b) (-a≡-1ᶠ*a a) ⟩
  (- 1ᶠ * a) * b ≡˘⟨ *-assoc (- 1ᶠ) a b ⟩
  - 1ᶠ * (a * b) ≡˘⟨ -a≡-1ᶠ*a ((a * b)) ⟩
  - (a * b)      ∎

a*-b≡-[a*b] : (a b : A) → a * - b ≡ - (a * b)
a*-b≡-[a*b] a b = begin
  a * - b   ≡⟨ *-comm a (- b) ⟩
  - b * a   ≡⟨ -a*b≡-[a*b] b a ⟩
  - (b * a) ≡⟨ cong -_ (*-comm b a) ⟩
  - (a * b) ∎

max_stars_repo_name: turion/functional-linear-algebra

max_issues_repo_name: turion/functional-linear-algebra

max_forks_repo_name: turion/functional-linear-algebra


text:
------------------------------------------------------------------------
-- Collection of most needed import from standard library
------------------------------------------------------------------------

module Library where

open import Data.Empty public
open import Data.Unit hiding (_≟_; _≤_; _≤?_; decSetoid; decTotalOrder; setoid) public
open import Data.Sum public hiding (map)
open import Data.Bool hiding (_≟_) public
open import Data.Nat hiding (_⊔_) public
open import Data.Product hiding (map ; swap) public
open import Data.Vec using ([]; _∷_; Vec) public
open import Level renaming (zero to ℓ₀; suc to ℓ⁺) public
open import Function public
open import Size public
open import Relation.Binary.PropositionalEquality hiding (decSetoid; preorder; setoid) public

open import ContainerMonkeyPatched as Container renaming (map to fmap) public

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


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

module Issue1719.Pushouts where

open import Issue1719.Common
open import Issue1719.Spans

postulate
  Pushout : (d : Span) → Set
  left : {d : Span} → (Span.A d) → Pushout d
  right : {d : Span} → (Span.B d) → Pushout d
  glue : {d : Span} → (c : Span.C d) → left (Span.f d c) == right (Span.g d c) :> Pushout d

module _ {d : Span} {l} {P : Pushout d → Set l}
  (left* : (a : Span.A d) → P (left a))
  (right* : (b : Span.B d) → P (right b))
  (glue* : (c : Span.C d) → left* (Span.f d c) == right* (Span.g d c) [ P ↓ glue c ]) where

  postulate
    Pushout-elim : (x : Pushout d) → P x
    Pushout-left-β : (a : Span.A d) → Pushout-elim (left a) ↦ left* a
    {-# REWRITE Pushout-left-β #-}
    Pushout-right-β : (b : Span.B d) → Pushout-elim (right b) ↦ right* b
    {-# REWRITE Pushout-right-β #-}
    Pushout-glue-β : (c : Span.C d) → ap Pushout-elim (glue c) ↦ glue* c
    {-# REWRITE Pushout-glue-β #-}


text:
module examplesPaperJFP.Colists where

-- open import Function

-- Case expressions (to be used with pattern-matching lambdas, see
-- README.Case).

infix 0 case_return_of_ case_of_

case_return_of_ :
  ∀ {a b} {A : Set a}
  (x : A) (B : A → Set b) → ((x : A) → B x) → B x
case x return B of f = f x

case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = case x return _ of f

data ListF A S : Set where
  nil   :  ListF A S
  cons  :  (a : A) (s : S) → ListF A S

record Colist A : Set where
  coinductive
  field force : ListF A (Colist A)

open Colist using (force)

mapF : ∀{A S S′} (f : S → S′) → (ListF A S → ListF A S′)
mapF f nil         =  nil
mapF f (cons a s)  =  cons a (f s)

-- As an example, we define mapping over potentially infinite lists using
-- copattern matching:

map : ∀{A B} (f : A → B) (l : Colist A) → Colist B
force (map f l) with force l
... | nil        =  nil
... | cons x xs  =  cons (f x) (map f xs)

unfold              :  ∀{A S} (t : S → ListF A S) → (S → Colist A)
force (unfold t s)  with t s
... | nil           =  nil
... | cons a s′     =  cons a (unfold t s′)

fmap : ∀{A B} (f : A → B) (l : Colist A) → Colist B
fmap f = unfold λ l → case force l of λ
  { nil → nil
  ; (cons a s) → cons (f a) s
  }

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst

postulate
  P : {X : Set} → X → Set
  H : Set
  R : H → Set
  x : H
  y : R x
  help : (f : H) (p : R f) → P {X = Σ H R} (f , p)

record Category : Set₁ where
  field
    Hom : Set
    id : Hom
    comp : Hom → Hom
    neut-l : P (comp id)
    neut-r : Hom

slice : Category
slice = λ where
  .Category.Hom → Σ H R
  .Category.id → (x , y)
  .Category.comp (f , p) → (f , p)
  .Category.neut-l → help x _
  .Category.neut-r → {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module _ where

module A where

  infix 2 _↑
  infix 1 c

  data D : Set where
    ●  : D
    _↑ : D → D
    c  : {x y : D} → D

  syntax c {x = x} {y = y} = x ↓ y

module B where

  infix 3 c

  data D : Set where
    c : {y x : D} → D

  syntax c {y = y} {x = x} = y ↓ x

open A
open B

accepted : A.D → A.D
accepted (● ↑ ↓ x) = ● ↑ ↓ x
accepted _         = ● ↑ ↓ ●


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

module Agda.Builtin.Unit where

record ⊤ : Set where
  instance constructor tt

{-# BUILTIN UNIT ⊤ #-}
{-# COMPILE GHC ⊤ = data () (()) #-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

module Properties.ResolveOverloads where

open import FFI.Data.Either using (Left; Right)
open import Luau.ResolveOverloads using (Resolved; src; srcⁿ; resolve; resolveⁿ; resolveᶠ; resolveˢ; target; yes; no)
open import Luau.Subtyping using (_<:_; _≮:_; Language; ¬Language; witness; scalar; unknown; never; function; function-ok; function-err; function-tgt; function-scalar; function-ok₁; function-ok₂; scalar-scalar; scalar-function; scalar-function-ok; scalar-function-err; scalar-function-tgt; _,_; left; right)
open import Luau.Type using (Type ; Scalar; _⇒_; _∩_; _∪_; nil; boolean; number; string; unknown; never)
open import Luau.TypeSaturation using (saturate)
open import Luau.TypeNormalization using (normalize)
open import Properties.Contradiction using (CONTRADICTION)
open import Properties.DecSubtyping using (dec-subtyping; dec-subtypingⁿ; <:-impl-<:ᵒ)
open import Properties.Functions using (_∘_)
open import Properties.Subtyping using (<:-refl; <:-trans; <:-trans-≮:; ≮:-trans-<:; <:-∩-left; <:-∩-right; <:-∩-glb; <:-impl-¬≮:; <:-unknown; <:-function; function-≮:-never; <:-never; unknown-≮:-function; scalar-≮:-function; ≮:-∪-right; scalar-≮:-never; <:-∪-left; <:-∪-right; <:-impl-⊇; language-comp)
open import Properties.TypeNormalization using (Normal; FunType; normal; _⇒_; _∩_; _∪_; never; unknown; <:-normalize; normalize-<:; fun-≮:-never; unknown-≮:-fun; scalar-≮:-fun)
open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; _<:ᵒ_; normal-saturate; saturated; <:-saturate; saturate-<:; defn; here; left; right)

-- Properties of src
function-err-srcⁿ : ∀ {T t} → (FunType T) → (¬Language (srcⁿ T) t) → Language T (function-err t)
function-err-srcⁿ (S ⇒ T) p = function-err p
function-err-srcⁿ (S ∩ T) (p₁ , p₂) = (function-err-srcⁿ S p₁ , function-err-srcⁿ T p₂)

¬function-err-srcᶠ : ∀ {T t} → (FunType T) → (Language (srcⁿ T) t) → ¬Language T (function-err t)
¬function-err-srcᶠ (S ⇒ T) p = function-err p
¬function-err-srcᶠ (S ∩ T) (left p) = left (¬function-err-srcᶠ S p)
¬function-err-srcᶠ (S ∩ T) (right p) = right (¬function-err-srcᶠ T p)

¬function-err-srcⁿ : ∀ {T t} → (Normal T) → (Language (srcⁿ T) t) → ¬Language T (function-err t)
¬function-err-srcⁿ never p = never
¬function-err-srcⁿ unknown (scalar ())
¬function-err-srcⁿ (S ⇒ T) p = function-err p
¬function-err-srcⁿ (S ∩ T) (left p) = left (¬function-err-srcᶠ S p)
¬function-err-srcⁿ (S ∩ T) (right p) = right (¬function-err-srcᶠ T p)
¬function-err-srcⁿ (S ∪ T) (scalar ())

¬function-err-src : ∀ {T t} → (Language (src T) t) → ¬Language T (function-err t)
¬function-err-src {T = S ⇒ T} p = function-err p
¬function-err-src {T = nil} p = scalar-function-err nil
¬function-err-src {T = never} p = never
¬function-err-src {T = unknown} (scalar ())
¬function-err-src {T = boolean} p = scalar-function-err boolean
¬function-err-src {T = number} p = scalar-function-err number
¬function-err-src {T = string} p = scalar-function-err string
¬function-err-src {T = S ∪ T} p = <:-impl-⊇ (<:-normalize (S ∪ T)) _ (¬function-err-srcⁿ (normal (S ∪ T)) p)
¬function-err-src {T = S ∩ T} p = <:-impl-⊇ (<:-normalize (S ∩ T)) _ (¬function-err-srcⁿ (normal (S ∩ T)) p)

src-¬function-errᶠ : ∀ {T t} → (FunType T) → Language T (function-err t) → (¬Language (srcⁿ T) t)
src-¬function-errᶠ (S ⇒ T) (function-err p) = p
src-¬function-errᶠ (S ∩ T) (p₁ , p₂) = (src-¬function-errᶠ S p₁ , src-¬function-errᶠ T p₂)

src-¬function-errⁿ : ∀ {T t} → (Normal T) → Language T (function-err t) → (¬Language (srcⁿ T) t)
src-¬function-errⁿ unknown p = never
src-¬function-errⁿ (S ⇒ T) (function-err p) = p
src-¬function-errⁿ (S ∩ T) (p₁ , p₂) = (src-¬function-errᶠ S p₁ , src-¬function-errᶠ T p₂)
src-¬function-errⁿ (S ∪ T) p = never

src-¬function-err : ∀ {T t} → Language T (function-err t) → (¬Language (src T) t)
src-¬function-err {T = S ⇒ T} (function-err p) = p
src-¬function-err {T = unknown} p = never
src-¬function-err {T = S ∪ T} p = src-¬function-errⁿ (normal (S ∪ T)) (<:-normalize (S ∪ T) _ p)
src-¬function-err {T = S ∩ T} p = src-¬function-errⁿ (normal (S ∩ T)) (<:-normalize (S ∩ T) _ p)

fun-¬scalar : ∀ {S T} (s : Scalar S) → FunType T → ¬Language T (scalar s)
fun-¬scalar s (S ⇒ T) = function-scalar s
fun-¬scalar s (S ∩ T) = left (fun-¬scalar s S)

¬fun-scalar : ∀ {S T t} (s : Scalar S) → FunType T → Language T t → ¬Language S t
¬fun-scalar s (S ⇒ T) function = scalar-function s
¬fun-scalar s (S ⇒ T) (function-ok₁ p) = scalar-function-ok s
¬fun-scalar s (S ⇒ T) (function-ok₂ p) = scalar-function-ok s
¬fun-scalar s (S ⇒ T) (function-err p) = scalar-function-err s
¬fun-scalar s (S ⇒ T) (function-tgt p) = scalar-function-tgt s
¬fun-scalar s (S ∩ T) (p₁ , p₂) = ¬fun-scalar s T p₂

fun-function : ∀ {T} → FunType T → Language T function
fun-function (S ⇒ T) = function
fun-function (S ∩ T) = (fun-function S , fun-function T)

srcⁿ-¬scalar : ∀ {S T t} (s : Scalar S) → Normal T → Language T (scalar s) → (¬Language (srcⁿ T) t)
srcⁿ-¬scalar s never (scalar ())
srcⁿ-¬scalar s unknown p = never
srcⁿ-¬scalar s (S ⇒ T) (scalar ())
srcⁿ-¬scalar s (S ∩ T) (p₁ , p₂) = CONTRADICTION (language-comp (scalar s) (fun-¬scalar s S) p₁)
srcⁿ-¬scalar s (S ∪ T) p = never

src-¬scalar : ∀ {S T t} (s : Scalar S) → Language T (scalar s) → (¬Language (src T) t)
src-¬scalar {T = nil} s p = never
src-¬scalar {T = T ⇒ U} s (scalar ())
src-¬scalar {T = never} s (scalar ())
src-¬scalar {T = unknown} s p = never
src-¬scalar {T = boolean} s p = never
src-¬scalar {T = number} s p = never
src-¬scalar {T = string} s p = never
src-¬scalar {T = T ∪ U} s p = srcⁿ-¬scalar s (normal (T ∪ U)) (<:-normalize (T ∪ U) (scalar s) p)
src-¬scalar {T = T ∩ U} s p = srcⁿ-¬scalar s (normal (T ∩ U)) (<:-normalize (T ∩ U) (scalar s) p)

srcⁿ-unknown-≮: : ∀ {T U} → (Normal U) → (T ≮: srcⁿ U) → (U ≮: (T ⇒ unknown))
srcⁿ-unknown-≮: never (witness t p q) = CONTRADICTION (language-comp t q unknown)
srcⁿ-unknown-≮: unknown (witness t p q) = witness (function-err t) unknown (function-err p)
srcⁿ-unknown-≮: (U ⇒ V) (witness t p q) = witness (function-err t) (function-err q) (function-err p)
srcⁿ-unknown-≮: (U ∩ V) (witness t p q) = witness (function-err t) (function-err-srcⁿ (U ∩ V) q) (function-err p)
srcⁿ-unknown-≮: (U ∪ V) (witness t p q) = witness (scalar V) (right (scalar V)) (function-scalar V)

src-unknown-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ unknown))
src-unknown-≮: {U = nil} (witness t p q) = witness (scalar nil) (scalar nil) (function-scalar nil)
src-unknown-≮: {U = T ⇒ U} (witness t p q) = witness (function-err t) (function-err q) (function-err p)
src-unknown-≮: {U = never} (witness t p q) = CONTRADICTION (language-comp t q unknown)
src-unknown-≮: {U = unknown} (witness t p q) = witness (function-err t) unknown (function-err p)
src-unknown-≮: {U = boolean} (witness t p q) = witness (scalar boolean) (scalar boolean) (function-scalar boolean)
src-unknown-≮: {U = number} (witness t p q) = witness (scalar number) (scalar number) (function-scalar number)
src-unknown-≮: {U = string} (witness t p q) = witness (scalar string) (scalar string) (function-scalar string)
src-unknown-≮: {U = T ∪ U} p = <:-trans-≮: (normalize-<: (T ∪ U)) (srcⁿ-unknown-≮: (normal (T ∪ U)) p)
src-unknown-≮: {U = T ∩ U} p = <:-trans-≮: (normalize-<: (T ∩ U)) (srcⁿ-unknown-≮: (normal (T ∩ U)) p)

unknown-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ unknown)) → (U ≮: src T)
unknown-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p)
unknown-src-≮: r (witness (function-ok s .(scalar s₁)) p (function-ok x (scalar-scalar s₁ () x₂)))
unknown-src-≮: r (witness (function-ok s .function) p (function-ok x (scalar-function ())))
unknown-src-≮: r (witness (function-ok s .(function-ok _ _)) p (function-ok x (scalar-function-ok ())))
unknown-src-≮: r (witness (function-ok s .(function-err _)) p (function-ok x (scalar-function-err ())))
unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p)
unknown-src-≮: r (witness (function-tgt t) p (function-tgt (scalar-function-tgt ())))

-- Properties of resolve
resolveˢ-<:-⇒ : ∀ {F V U} → (FunType F) → (Saturated F) → (FunType (V ⇒ U)) → (r : Resolved F V) → (F <: (V ⇒ U)) → (target r <: U)
resolveˢ-<:-⇒ Fᶠ Fˢ V⇒Uᶠ r F<:V⇒U with <:-impl-<:ᵒ Fᶠ Fˢ V⇒Uᶠ F<:V⇒U here
resolveˢ-<:-⇒ Fᶠ Fˢ V⇒Uᶠ (yes Sʳ Tʳ oʳ V<:Sʳ tgtʳ) F<:V⇒U | defn o o₁ o₂ = <:-trans (tgtʳ o o₁) o₂
resolveˢ-<:-⇒ Fᶠ Fˢ V⇒Uᶠ (no tgtʳ) F<:V⇒U | defn o o₁ o₂ = CONTRADICTION (<:-impl-¬≮: o₁ (tgtʳ o))

resolveⁿ-<:-⇒ : ∀ {F V U} → (Fⁿ : Normal F) → (Vⁿ : Normal V) → (Uⁿ : Normal U) → (F <: (V ⇒ U)) → (resolveⁿ Fⁿ Vⁿ <: U)
resolveⁿ-<:-⇒ (Sⁿ ⇒ Tⁿ) Vⁿ Uⁿ F<:V⇒U = resolveˢ-<:-⇒ (normal-saturate (Sⁿ ⇒ Tⁿ)) (saturated (Sⁿ ⇒ Tⁿ)) (Vⁿ ⇒ Uⁿ) (resolveˢ (normal-saturate (Sⁿ ⇒ Tⁿ)) (saturated (Sⁿ ⇒ Tⁿ)) Vⁿ (λ o → o)) F<:V⇒U
resolveⁿ-<:-⇒ (Fⁿ ∩ Gⁿ) Vⁿ Uⁿ F<:V⇒U = resolveˢ-<:-⇒ (normal-saturate (Fⁿ ∩ Gⁿ)) (saturated (Fⁿ ∩ Gⁿ)) (Vⁿ ⇒ Uⁿ) (resolveˢ (normal-saturate (Fⁿ ∩ Gⁿ)) (saturated (Fⁿ ∩ Gⁿ)) Vⁿ (λ o → o)) (<:-trans (saturate-<: (Fⁿ ∩ Gⁿ)) F<:V⇒U)
resolveⁿ-<:-⇒ (Sⁿ ∪ Tˢ) Vⁿ Uⁿ F<:V⇒U = CONTRADICTION (<:-impl-¬≮: F<:V⇒U (<:-trans-≮: <:-∪-right (scalar-≮:-function Tˢ)))
resolveⁿ-<:-⇒ never Vⁿ Uⁿ F<:V⇒U = <:-never
resolveⁿ-<:-⇒ unknown Vⁿ Uⁿ F<:V⇒U = CONTRADICTION (<:-impl-¬≮: F<:V⇒U unknown-≮:-function)

resolve-<:-⇒ : ∀ {F V U} → (F <: (V ⇒ U)) → (resolve F V <: U)
resolve-<:-⇒ {F} {V} {U} F<:V⇒U = <:-trans (resolveⁿ-<:-⇒ (normal F) (normal V) (normal U) (<:-trans (normalize-<: F) (<:-trans F<:V⇒U (<:-normalize (V ⇒ U))))) (normalize-<: U)

resolve-≮:-⇒ : ∀ {F V U} → (resolve F V ≮: U) → (F ≮: (V ⇒ U))
resolve-≮:-⇒ {F} {V} {U} FV≮:U with dec-subtyping F (V ⇒ U)
resolve-≮:-⇒ {F} {V} {U} FV≮:U | Left F≮:V⇒U = F≮:V⇒U
resolve-≮:-⇒ {F} {V} {U} FV≮:U | Right F<:V⇒U = CONTRADICTION (<:-impl-¬≮: (resolve-<:-⇒ F<:V⇒U) FV≮:U)

<:-resolveˢ-⇒ : ∀ {S T V} → (r : Resolved (S ⇒ T) V) → (V <: S) → T <: target r
<:-resolveˢ-⇒ (yes S T here _ _) V<:S = <:-refl
<:-resolveˢ-⇒ (no _) V<:S = <:-unknown

<:-resolveⁿ-⇒ : ∀ {S T V} → (Sⁿ : Normal S) → (Tⁿ : Normal T) → (Vⁿ : Normal V) → (V <: S) → T <: resolveⁿ (Sⁿ ⇒ Tⁿ) Vⁿ
<:-resolveⁿ-⇒ Sⁿ Tⁿ Vⁿ V<:S = <:-resolveˢ-⇒ (resolveˢ (Sⁿ ⇒ Tⁿ) (saturated (Sⁿ ⇒ Tⁿ)) Vⁿ (λ o → o)) V<:S

<:-resolve-⇒ : ∀ {S T V} → (V <: S) → T <: resolve (S ⇒ T) V
<:-resolve-⇒ {S} {T} {V} V<:S = <:-trans (<:-normalize T) (<:-resolveⁿ-⇒ (normal S) (normal T) (normal V) (<:-trans (normalize-<: V) (<:-trans V<:S (<:-normalize S))))

<:-resolveˢ : ∀ {F G V W} → (r : Resolved F V) → (s : Resolved G W) → (F <:ᵒ G) → (V <: W) → target r <: target s
<:-resolveˢ (yes Sʳ Tʳ oʳ V<:Sʳ tgtʳ) (yes Sˢ Tˢ oˢ  W<:Sˢ tgtˢ) F<:G V<:W with F<:G oˢ
<:-resolveˢ (yes Sʳ Tʳ oʳ V<:Sʳ tgtʳ) (yes Sˢ Tˢ oˢ W<:Sˢ tgtˢ) F<:G V<:W | defn o o₁ o₂ = <:-trans (tgtʳ o (<:-trans (<:-trans V<:W W<:Sˢ) o₁)) o₂
<:-resolveˢ (no r) (yes Sˢ Tˢ oˢ  W<:Sˢ tgtˢ) F<:G V<:W with F<:G oˢ
<:-resolveˢ (no r) (yes Sˢ Tˢ oˢ  W<:Sˢ tgtˢ) F<:G V<:W | defn o o₁ o₂ = CONTRADICTION (<:-impl-¬≮: (<:-trans V<:W (<:-trans W<:Sˢ o₁)) (r o))
<:-resolveˢ r (no s) F<:G V<:W = <:-unknown

<:-resolveᶠ : ∀ {F G V W} → (Fᶠ : FunType F) → (Gᶠ : FunType G) → (Vⁿ : Normal V) → (Wⁿ : Normal W) → (F <: G) → (V <: W) → resolveᶠ Fᶠ Vⁿ <: resolveᶠ Gᶠ Wⁿ
<:-resolveᶠ Fᶠ Gᶠ Vⁿ Wⁿ F<:G V<:W = <:-resolveˢ
  (resolveˢ (normal-saturate Fᶠ) (saturated Fᶠ) Vⁿ (λ o → o))
  (resolveˢ (normal-saturate Gᶠ) (saturated Gᶠ) Wⁿ (λ o → o))
  (<:-impl-<:ᵒ (normal-saturate Fᶠ) (saturated Fᶠ) (normal-saturate Gᶠ) (<:-trans (saturate-<: Fᶠ) (<:-trans F<:G (<:-saturate Gᶠ))))
  V<:W

<:-resolveⁿ : ∀ {F G V W} → (Fⁿ : Normal F) → (Gⁿ : Normal G) → (Vⁿ : Normal V) → (Wⁿ : Normal W) → (F <: G) → (V <: W) → resolveⁿ Fⁿ Vⁿ <: resolveⁿ Gⁿ Wⁿ
<:-resolveⁿ (Rⁿ ⇒ Sⁿ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W = <:-resolveᶠ (Rⁿ ⇒ Sⁿ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W
<:-resolveⁿ (Rⁿ ⇒ Sⁿ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W = <:-resolveᶠ (Rⁿ ⇒ Sⁿ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W
<:-resolveⁿ (Eⁿ ∩ Fⁿ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W = <:-resolveᶠ (Eⁿ ∩ Fⁿ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W
<:-resolveⁿ (Eⁿ ∩ Fⁿ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W = <:-resolveᶠ (Eⁿ ∩ Fⁿ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W
<:-resolveⁿ (Fⁿ ∪ Sˢ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (≮:-∪-right (scalar-≮:-function Sˢ)))
<:-resolveⁿ unknown (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G unknown-≮:-function)
<:-resolveⁿ (Fⁿ ∪ Sˢ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (≮:-∪-right (scalar-≮:-fun (Gⁿ ∩ Hⁿ) Sˢ)))
<:-resolveⁿ unknown (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (unknown-≮:-fun (Gⁿ ∩ Hⁿ)))
<:-resolveⁿ (Rⁿ ⇒ Sⁿ) never Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (fun-≮:-never (Rⁿ ⇒ Sⁿ)))
<:-resolveⁿ (Eⁿ ∩ Fⁿ) never Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (fun-≮:-never (Eⁿ ∩ Fⁿ)))
<:-resolveⁿ (Fⁿ ∪ Sˢ) never Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (≮:-∪-right (scalar-≮:-never Sˢ)))
<:-resolveⁿ unknown never Vⁿ Wⁿ F<:G V<:W = F<:G
<:-resolveⁿ never Gⁿ Vⁿ Wⁿ F<:G V<:W = <:-never
<:-resolveⁿ Fⁿ (Gⁿ ∪ Uˢ) Vⁿ Wⁿ F<:G V<:W = <:-unknown
<:-resolveⁿ Fⁿ unknown Vⁿ Wⁿ F<:G V<:W = <:-unknown

<:-resolve : ∀ {F G V W} → (F <: G) → (V <: W) → resolve F V <: resolve G W
<:-resolve {F} {G} {V} {W} F<:G V<:W = <:-resolveⁿ (normal F) (normal G) (normal V) (normal W)
  (<:-trans (normalize-<: F) (<:-trans F<:G (<:-normalize G)))
  (<:-trans (normalize-<: V) (<:-trans V<:W (<:-normalize W)))

max_stars_repo_name: Libertus-Lab/luau

max_issues_repo_name: sthagen/Roblox-luau

max_forks_repo_name: sthagen/Roblox-luau


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

open import Cubical.HITs.Rationals.QuoQ.Base public

open import Cubical.HITs.Rationals.QuoQ.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.Lattice

open import Cubical.Categories.Category
open import Cubical.Categories.Instances.Semilattice

open Category

LatticeCategory : ∀ {ℓ} (L : Lattice ℓ) → Category ℓ ℓ
LatticeCategory L = SemilatticeCategory (Lattice→JoinSemilattice L)


text:
module plfa-code.Bin where

-- I collect code about Bin there. other definitions I use the std-lib version

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym; trans)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
open import Data.Nat.Properties using (+-comm; +-suc; +-mono-≤)

infixr 2 _≡⟨_⟩_

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

data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

inc : Bin → Bin
inc nil    = x1 nil
inc (x0 t) = x1 t
inc (x1 t) = x0 (inc t)

to : ℕ → Bin
to zero    = x0 nil
to (suc n) = inc (to n)

from : Bin → ℕ
from nil      = 0
from (x0 t)   = 2 * (from t)
from (x1 t)   = suc (2 * (from t))

+1≡suc : ∀ {n : ℕ} → n + 1 ≡ suc n
+1≡suc {zero}   = refl
+1≡suc {suc n}  = cong suc +1≡suc

suc-from-inc : ∀ (x : Bin) → from (inc x) ≡ suc (from x)
suc-from-inc nil                                        = refl
suc-from-inc (x0 x) rewrite +1≡suc {from x * 2}         = refl
suc-from-inc (x1 x) rewrite suc-from-inc x
                          | +-suc (from x) (from x + 0) = refl

-- t4 is ⊥ , because `to (from nil) ≡ x0 nil ≢ nil`
-- t4 : ∀ (x : Bin) → to (from x) ≡ x

from-to-const : ∀ (n : ℕ) → from (to n) ≡ n
from-to-const zero                               =  refl
from-to-const (suc n) rewrite suc-from-inc (to n)
                            | from-to-const n    =  refl

data Can : Bin → Set
data One : Bin → Set

data One where
  one  : One (x1 nil)
  x0_ : ∀ {b : Bin} → One b → One(x0 b)
  x1_ : ∀ {b : Bin} → One b → One(x1 b)

data Can where
  zero     : Can (x0 nil)
  can-one  : ∀ {b : Bin} → One b → Can b

one-inc : ∀ {x : Bin} → One x → One (inc x)
one-inc one = x0 one
one-inc (x0 x) = x1 x
one-inc (x1 x) = x0 (one-inc x)

can-inc : ∀ {x : Bin} → Can x → Can (inc x)
can-inc zero        =  can-one one
can-inc (can-one x) =  can-one (one-inc x)

one-to-n : ∀ (n : ℕ) → One (to (suc n))
one-to-n zero = one
one-to-n (suc n) = one-inc (one-to-n n)

can-to-n : ∀ (n : ℕ) → Can (to n)
can-to-n zero = zero
can-to-n (suc n) = can-one (one-to-n n)

open Data.Nat.Properties using (+-identityʳ; +-suc)

l0 : ∀ (n) → to (suc n) ≡ inc (to n)
l0 zero    = refl
l0 (suc n) = refl

2n-eq-x0 : ∀ (n) → 1 ≤ n → to (n + n) ≡ x0 (to n)
2n-eq-x0 zero ()
2n-eq-x0 (suc zero) (s≤s z≤n) = refl
2n-eq-x0 (suc (suc n)) (s≤s z≤n) =
  begin to (suc (suc n) + suc (suc n))
  ≡⟨ cong (λ x → to x) (+-suc (suc (suc n)) (suc n)) ⟩  to (suc (suc (suc n + suc n)))
  ≡⟨⟩  inc (inc (to (suc n + suc n)))
  ≡⟨ cong (λ x → (inc (inc x))) (2n-eq-x0 (suc n) (s≤s z≤n)) ⟩  inc (inc (x0 (to (suc n))))
  ≡⟨⟩  x0 (inc (to (suc n)))
  ≡⟨⟩  x0 (to (suc (suc n)))
  ∎

one-b-iff-1≤b : ∀ (b) → One b → 1 ≤ from b
one-b-iff-1≤b (x0 b) (x0 ob)
              rewrite +-identityʳ (from b) = +-mono-≤ (one-b-iff-1≤b b ob) z≤n
              where n = from b
one-b-iff-1≤b (x1 .nil) one     = s≤s z≤n
one-b-iff-1≤b (x1 b)    (x1 ob) = s≤s z≤n

one-tf-eq : ∀ {b} → One b → to (from b) ≡ b
one-tf-eq {_}    one    = refl
one-tf-eq {x0 b} (x0 x) =
  begin
    to (from (x0 b))
  ≡⟨⟩
    to (from b + (from b + zero))
  ≡⟨ cong (λ n → to (from b + n)) (+-identityʳ (from b)) ⟩
    to (from b + from b)
  ≡⟨ 2n-eq-x0 (from b) (one-b-iff-1≤b b x) ⟩
    x0 (to (from b))
  ≡⟨ cong x0_ (one-tf-eq x) ⟩
    x0 b
  ∎
one-tf-eq {x1 b} (x1 x) =
  begin
    to (from (x1 b))
  ≡⟨⟩
    inc (to (from b + (from b + zero)))
  ≡⟨ cong (λ n → inc (to (from b + n))) (+-identityʳ (from b)) ⟩
    inc (to (from b + from b))
  ≡⟨ cong inc (2n-eq-x0 (from b) (one-b-iff-1≤b b x)) ⟩
    inc (x0 (to (from b)))
  ≡⟨⟩
    x1 (to (from b))
  ≡⟨ cong x1_ (one-tf-eq x) ⟩
    x1 b
  ∎

can-tf-eq : ∀ {x} → Can x → to (from x) ≡ x
can-tf-eq {_}  zero        = refl
can-tf-eq {b}  (can-one x) = one-tf-eq x

open import Function.LeftInverse using (_↞_)

ℕ-embedding-Bin : ℕ ↞ Bin
ℕ-embedding-Bin =
  record
  { to              = record { _⟨$⟩_ = to   ; cong = cong to }
  ; from            = record { _⟨$⟩_ = from ; cong = cong from }
  ; left-inverse-of = from-to-const
  }

open import Function.Inverse using (_↔_)
open import Data.Product
  using (Σ; ∃; Σ-syntax; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Function using (_∘_)

one-assim : ∀ {b : Bin} → (x : One b) → (y : One b) → x ≡ y
one-assim one one = refl
one-assim (x0 x) (x0 y) = sym (cong x0_ (one-assim y x))
one-assim (x1 x) (x1 y) = sym (cong x1_ (one-assim y x))

can-assim : ∀ {b : Bin} → (x : Can b) → (y : Can b) → x ≡ y
can-assim zero zero = refl
can-assim zero (can-one (x0 ()))
can-assim (can-one (x0 ())) zero
can-assim (can-one one) (can-one one) = refl
can-assim (can-one (x0 x)) (can-one (x0 y)) = cong (can-one ∘ x0_) (one-assim x y)
can-assim (can-one (x1 x)) (can-one (x1 y)) = cong (can-one ∘ x1_) (one-assim x y)

∃-proj₁ : {A : Set} {B : A → Set} → ∃[ x ] B x → A
∃-proj₁ ⟨ x , _ ⟩ = x

∃≡ : ∀ {A : Set} {B : A → Set} (p₁ : ∃[ x ](B x)) (p₂ : ∃[ y ](B y))
  → ∃-proj₁ p₁ ≡ ∃-proj₁ p₂ → (∀ (x) → (b₁ : B x) → (b₂ : B x) → b₁ ≡ b₂)
  → p₁ ≡ p₂
∃≡ ⟨ x , bx ⟩ ⟨ .x , by ⟩ refl f = sym (cong (⟨_,_⟩ x) (f x by bx))

Bin-isomorphism : ℕ ↔ ∃[ x ](Can x)
Bin-isomorphism =
  record
  { to         = record { _⟨$⟩_ = to′; cong = cong to′}
  ; from       = record { _⟨$⟩_ = from′; cong = cong from′}
  ; inverse-of = record
                 { left-inverse-of = from-to-const
                 ; right-inverse-of = to∘from′
                 }
  }
  where
  to′ : ℕ → ∃[ x ](Can x)
  to′ n = ⟨ to n , can-to-n n ⟩
  from′ : ∃[ x ](Can x) → ℕ
  from′ ⟨ b , can-b ⟩ = from b
  to∘from′ : ∀ y → to′ (from′ y) ≡ y
  to∘from′ ⟨ b , can-b ⟩  = ∃≡ ⟨ to (from b) , can-to-n (from b) ⟩ ⟨ b , can-b ⟩ (can-tf-eq can-b) (λ x → can-assim {x})

max_stars_repo_name: chirsz-ever/plfa-code

max_issues_repo_name: chirsz-ever/plfa-code

max_forks_repo_name: chirsz-ever/plfa-code


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

open import Algebra
open import Relation.Binary
open import Algebra.Monus

module Data.MonoidalHeap.Monad {s} (monus : TMAPOM s) where

open TMAPOM monus

open import Prelude
open import Data.List using (List; _∷_; []; foldr; _++_)
import Data.Nat as ℕ
import Data.Nat.Properties as ℕ

𝒮 : Type s
𝒮 = 𝑆 → 𝑆

⟦_⇑⟧ : 𝑆 → 𝒮
⟦_⇑⟧ = _∙_

⟦_⇓⟧ : 𝒮 → 𝑆
⟦ x ⇓⟧ = x ε

infixl 10 _⊙_
_⊙_ : (𝑆 → A) → 𝑆 → 𝑆 → A
f ⊙ x = λ y → f (x ∙ y)

mutual
  data Node (V : 𝑆 → Type a) : Type (a ℓ⊔ s) where
    leaf : V ε → Node V
    _⋊_ : (w : 𝑆) → Heap (V ⊙ w) → Node V

  Heap : (𝑆 → Type a) → Type (a ℓ⊔ s)
  Heap V = List (Node V)

private
  variable
    v : Level
    V : 𝑆 → Type v

Root : (𝑆 → Type v) → Type _
Root V = ∃ w × Heap (V ⊙ w)

partition : Heap V → List (V ε) × List (Root V)
partition = foldr f ([] , [])
  where
    f : Node V → List (V ε) × List (∃ w × Heap (V ⊙ w)) → List (V ε) × List (∃ w × Heap (V ⊙ w))
    f (leaf x) (ls , hs) = (x ∷ ls) , hs
    f (w ⋊ x)  (ls , hs) = ls , ((w , x) ∷ hs)

module _ {V : 𝑆 → Type v} where
  ⊙-assoc : ∀ x y k → x ≡ y ∙ k → V ⊙ x ≡ V ⊙ y ⊙ k
  ⊙-assoc x y k x≡y∙k i z = V ((cong (_∙ z) x≡y∙k ; assoc y k z) i)

  ⊙ε : V ⊙ ε ≡ V
  ⊙ε i x = V (ε∙ x i)

  ⊙-rassoc : ∀ x y → V ⊙ (x ∙ y) ≡ V ⊙ x ⊙ y
  ⊙-rassoc x y i z = V (assoc x y z i)

  merge : Root V → Root V → Root V
  merge (x , xs) (y , ys) with x ≤|≥ y
  ... | inl (k , y≡x∙k) = x , (k ⋊ subst Heap (⊙-assoc y x k y≡x∙k) ys) ∷ xs
  ... | inr (k , x≡y∙k) = y , (k ⋊ subst Heap (⊙-assoc x y k x≡y∙k) xs) ∷ ys

  merges⁺ : Root V → List (Root V) → Root V
  merges⁺ x [] = x
  merges⁺ x₁ (x₂ ∷ []) = merge x₁ x₂
  merges⁺ x₁ (x₂ ∷ x₃ ∷ xs) = merge (merge x₁ x₂) (merges⁺ x₃ xs)

  merges : List (Root V) → Maybe (Root V)
  merges [] = nothing
  merges (x ∷ xs) = just (merges⁺ x xs)

  popMin : Heap V → List (V ε) × Maybe (Root V)
  popMin = map₂ merges ∘ partition

  return : V ε → Heap V
  return x = leaf x ∷ []

  weight : ∃ x × V x → Heap V
  weight (w , x) = (w ⋊ (leaf (subst V (sym (∙ε w)) x) ∷ [])) ∷ []

_>>=_ : Heap V → (∀ {x} → V x → Heap (V ⊙ x)) → Heap V
_>>=_ []             k = []
_>>=_ (leaf x ∷ xs)  k = subst Heap ⊙ε (k x) ++ (xs >>= k)
_>>=_ {V = V} ((w ⋊ x) ∷ xs) k = (w ⋊ (x >>= (subst Heap (⊙-rassoc {V = V} w _) ∘ k))) ∷ (xs >>= k)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Integers modulo N
module Numeric.Nat.Modulo where

open import Prelude
open import Numeric.Nat.DivMod
open import Tactic.Nat

data IntMod (n : Nat) : Set where
  modn : ∀ k → k < n → IntMod n

{-# DISPLAY modn k (LessNat.diff _ refl) = k #-}

negIntMod : ∀ {n} → IntMod n → IntMod n
negIntMod (modn 0 lt) = modn 0 lt
negIntMod (modn (suc k) (diff j eq)) = modn (suc j) (by (sym eq))

{-# DISPLAY negIntMod a = negate a #-}

instance
  NumberIntMod : ∀ {n} → Number (IntMod (suc n))
  Number.Constraint NumberIntMod _ = ⊤
  fromNat {{NumberIntMod {n}}} k with k divmod suc n
  ... | qr _ r lt _ = modn r lt

  NegativeIntMod : ∀ {n} → Negative (IntMod (suc n))
  Negative.Constraint NegativeIntMod _ = ⊤
  fromNeg {{NegativeIntMod}} k = negIntMod (fromNat k)

addIntMod : ∀ {n} → IntMod (suc n) → IntMod (suc n) → IntMod (suc n)
addIntMod {n} (modn a _) (modn b _) = force (a + b) λ a+b → fromNat a+b ofType IntMod (suc n)

mulIntMod : ∀ {n} → IntMod (suc n) → IntMod (suc n) → IntMod (suc n)
mulIntMod {n} (modn a _) (modn b _) = force (a * b) λ a*b → fromNat a*b ofType IntMod (suc n)

subIntMod : ∀ {n} → IntMod (suc n) → IntMod (suc n) → IntMod (suc n)
subIntMod a b = addIntMod a (negIntMod b)

{-# DISPLAY addIntMod a b = a + b #-}
{-# DISPLAY mulIntMod a b = a * b #-}
{-# DISPLAY subIntMod a b = a - b #-}

instance
  SemiringIntMod : ∀ {n} → Semiring (IntMod (suc n))
  zro {{SemiringIntMod}} = 0
  one {{SemiringIntMod}} = 1
  _+_ {{SemiringIntMod}} = addIntMod
  _*_ {{SemiringIntMod}} = mulIntMod

  SubtractiveIntMod : ∀ {n} → Subtractive (IntMod (suc n))
  _-_    {{SubtractiveIntMod}} = subIntMod
  negate {{SubtractiveIntMod}} = negIntMod

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
module Languages.FILL.TypeSyntax where

open import Utils.HaskellTypes

{-# IMPORT Languages.FILL.TypeSyntax #-}

data Type : Set where
  TVar : String → Type
  Top : Type
  Bottom : Type
  Imp : Type → Type → Type
  Tensor : Type → Type → Type
  Par : Type → Type → Type

{-# COMPILED_DATA Type Languages.FILL.TypeSyntax.Type
                       Languages.FILL.TypeSyntax.TVar
                       Languages.FILL.TypeSyntax.Top
                       Languages.FILL.TypeSyntax.Bottom
                       Languages.FILL.TypeSyntax.Imp
                       Languages.FILL.TypeSyntax.Tensor
                       Languages.FILL.TypeSyntax.Par #-}

max_stars_repo_name: heades/Agda-LLS

max_issues_repo_name: heades/Agda-LLS

max_forks_repo_name: heades/Agda-LLS


text:
open import Agda.Primitive

variable
  a : Level
  A : Set a
  P : A → Set a
  x : A

open import Agda.Builtin.Equality

data Box (A : Set a) : Set a where
  [_] : A → Box A

postulate
  _ : P (λ (_ : x ≡ x) → [ x ])

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Internal monoid in a strict monoidal category
{-# OPTIONS --safe #-}

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Monoidal.Base
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Path
open import Cubical.Categories.Functor.Base
open import Cubical.Reflection.RecordEquiv hiding (unit)

module Cubical.Categories.Monoidal.Strict.Monoid {ℓ ℓ' : Level} (C : StrictMonCategory ℓ ℓ') where

module _ where
    open StrictMonCategory C

    record Monoid : Type (ℓ-max ℓ ℓ') where
      constructor monoid
      field
        carrier : ob
        η : Hom[ unit , carrier ]
        μ : Hom[ carrier ⊗ carrier , carrier ]
        assoc-μ : PathP (λ i → Hom[ assoc carrier carrier carrier i , carrier ]) (μ ∘ (id ⊗ₕ μ)) (μ ∘ (μ ⊗ₕ id))
        idl-μ : PathP (λ i → Hom[ idl carrier i , carrier ]) (μ ∘ (η ⊗ₕ id)) id
        idr-μ : PathP (λ i → Hom[ idr carrier i , carrier ]) (μ ∘ (id ⊗ₕ η)) id

    open Monoid

    record Monoid[_,_] (monA monB : Monoid) : Type ℓ' where
      constructor monoidHom
      field
        carrierHom : Hom[ carrier monA , carrier monB ]
        nat-η : carrierHom ∘ η monA ≡ η monB
        nat-μ : carrierHom ∘ μ monA ≡ μ monB ∘ (carrierHom ⊗ₕ carrierHom)

    open Monoid[_,_]

    monoidHomExt : {monA monB : Monoid} (f g : Monoid[ monA , monB ]) → carrierHom f ≡ carrierHom g → f ≡ g
    carrierHom (monoidHomExt f g p i) = p i
    nat-η (monoidHomExt {monA} {monB} f g p i) = lemma i
      where lemma : PathP (λ i₁ → p i₁ ∘ η monA ≡ η monB) (nat-η f) (nat-η g)
            lemma = toPathP (isSetHom _ _ _ _)
    nat-μ (monoidHomExt {monA} {monB} f g p i) = lemma i
      where lemma : PathP (λ i₁ → p i₁ ∘ μ monA ≡ μ monB ∘ (p i₁ ⊗ₕ p i₁)) (nat-μ f) (nat-μ g)
            lemma = toPathP (isSetHom _ _ _ _)

module C = StrictMonCategory C
open Category
open Monoid
open Monoid[_,_]
open Functor

monoidCategory : Category (ℓ-max ℓ ℓ') ℓ'
ob monoidCategory = Monoid
Hom[_,_] monoidCategory = Monoid[_,_]
carrierHom (id monoidCategory) = C.id
nat-η (id monoidCategory {monA}) = C.⋆IdR (η monA)
nat-μ (id monoidCategory {monA}) =
  C.id C.∘ μ monA
    ≡⟨ C.⋆IdR (μ monA) ⟩
  μ monA
    ≡⟨ sym (C.⋆IdL (μ monA)) ⟩
  μ monA C.∘ id C.C
    ≡⟨ cong (μ monA C.∘_) (sym (F-id C.─⊗─)) ⟩
  μ monA C.∘ (C.id C.⊗ₕ C.id) ∎
carrierHom (_⋆_ monoidCategory f g) = carrierHom g C.∘ carrierHom f
nat-η (_⋆_ monoidCategory {monA} {monB} {monC} f g) =
  (carrierHom g C.∘ carrierHom f) C.∘ η monA
    ≡⟨ sym (C.⋆Assoc (η monA) (carrierHom f) (carrierHom g)) ⟩
  carrierHom g C.∘ (carrierHom f C.∘ η monA)
    ≡⟨ cong (carrierHom g C.∘_) (nat-η f) ⟩
  carrierHom g C.∘ η monB
    ≡⟨ nat-η g ⟩
  η monC ∎
nat-μ (_⋆_ monoidCategory {monA} {monB} {monC} f g) =
  (carrierHom g C.∘ carrierHom f) C.∘ μ monA
    ≡⟨ sym (C.⋆Assoc (μ monA) (carrierHom f) (carrierHom g)) ⟩
  carrierHom g C.∘ (carrierHom f C.∘ μ monA)
    ≡⟨ cong (carrierHom g C.∘_) (nat-μ f) ⟩
  carrierHom g C.∘ (μ monB C.∘ (carrierHom f C.⊗ₕ carrierHom f))
    ≡⟨ C.⋆Assoc (carrierHom f C.⊗ₕ carrierHom f) (μ monB) (carrierHom g) ⟩
  (carrierHom g C.∘ μ monB) C.∘ (carrierHom f C.⊗ₕ carrierHom f)
    ≡⟨ cong (C._∘ (carrierHom f C.⊗ₕ carrierHom f)) (nat-μ g) ⟩
  (μ monC C.∘ (carrierHom g C.⊗ₕ carrierHom g)) C.∘ (carrierHom f C.⊗ₕ carrierHom f)
    ≡⟨ sym (C.⋆Assoc (carrierHom f C.⊗ₕ carrierHom f) (carrierHom g C.⊗ₕ carrierHom g) (μ monC)) ⟩
  μ monC C.∘ ((carrierHom g C.⊗ₕ carrierHom g) C.∘ (carrierHom f C.⊗ₕ carrierHom f))
    ≡⟨ cong (μ monC C.∘_) (sym (F-seq C.─⊗─ (carrierHom f , carrierHom f) (carrierHom g , carrierHom g))) ⟩
  μ monC C.∘ ((carrierHom g C.∘ carrierHom f) C.⊗ₕ (carrierHom g C.∘ carrierHom f)) ∎
⋆IdL monoidCategory {monA} f = monoidHomExt _ _ (C.⋆IdL (carrierHom f))
⋆IdR monoidCategory {monA} f = monoidHomExt _ _ (C.⋆IdR (carrierHom f))
⋆Assoc monoidCategory {monA} {monB} {monC} {monD} f g h =
  monoidHomExt _ _ (C.⋆Assoc (carrierHom f) (carrierHom g) (carrierHom h))
isSetHom monoidCategory {monA} {monB} =
  isOfHLevelRetractFromIso 2 isoToΣ
    (isSetΣ C.isSetHom λ _ → isProp→isSet (isProp× (C.isSetHom _ _) (C.isSetHom _ _)))
  where
  unquoteDecl isoToΣ = declareRecordIsoΣ isoToΣ (quote Monoid[_,_])

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------
-- Lifting of weak equality to canonical equality
------------------------------------------------------------------------

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

module FOmegaInt.Kinding.Canonical.WeakEquality where

open import Data.Product as Prod using (∃; _×_; _,_)
open import Relation.Binary.PropositionalEquality using (_≡_; subst; sym; trans)

open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.HereditarySubstitution
open import FOmegaInt.Syntax.Normalization
open import FOmegaInt.Syntax.WeakEquality
open import FOmegaInt.Kinding.Canonical
open import FOmegaInt.Kinding.Canonical.HereditarySubstitution

------------------------------------------------------------------------
-- Lifting of weak kind/type equality into canonical equality.
--
-- The lemmas below state that a variant of reflexivity is admissible
-- in canonical subkinding, subtyping as well as kind and type
-- equality, which uses weak equality (instead of syntactic equality)
-- along with proofs of canonical well-formedness
-- resp. well-kindedness of *both* the kinds resp. types being
-- related.

open Syntax
open ElimCtx
open Kinding
open ContextNarrowing

-- Lifting of weak kind/type equality into canonical
-- subkinding/subtyping and type/kind equality.

mutual

  ≋-<∷ : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j kd → Γ ⊢ k kd → j ≋ k → Γ ⊢ j <∷ k
  ≋-<∷ (kd-⋯ a₁⇉a₁⋯a₁ b₁⇉b₁⋯b₁) (kd-⋯ a₂⇉a₂⋯a₂ b₂⇉b₂⋯b₂) (≋-⋯ a₁≈a₂ b₁≈b₂) =
    <∷-⋯ (≈-<: a₂⇉a₂⋯a₂ a₁⇉a₁⋯a₁ (≈-sym a₁≈a₂)) (≈-<: b₁⇉b₁⋯b₁ b₂⇉b₂⋯b₂ b₁≈b₂)
  ≋-<∷ (kd-Π j₁-kd k₁-kd) (kd-Π j₂-kd k₂-kd) (≋-Π j₁≋j₂ k₁≋k₂) =
    let j₂<∷j₁ = ≋-<∷ j₂-kd j₁-kd (≋-sym j₁≋j₂)
    in <∷-Π j₂<∷j₁ (≋-<∷ (⇓-kd j₂-kd j₂<∷j₁ k₁-kd) k₂-kd k₁≋k₂)
            (kd-Π j₁-kd k₁-kd)

  ≈-<: : ∀ {n} {Γ : Ctx n} {a a₁ a₂ b b₁ b₂} →
         Γ ⊢Nf a ⇉ a₁ ⋯ a₂ → Γ ⊢Nf b ⇉ b₁ ⋯ b₂ → a ≈ b → Γ ⊢ a <: b
  ≈-<: (⇉-⊥-f Γ-ctx) (⇉-⊥-f _)  (≈-∙ ≈-⊥ ≈-[]) = <:-⊥ (⇉-⊥-f Γ-ctx)
  ≈-<: (⇉-⊥-f _)     (⇉-s-i ()) (≈-∙ ≈-⊥ ≈-[])
  ≈-<: (⇉-⊤-f Γ-ctx) (⇉-⊤-f _)  (≈-∙ ≈-⊤ ≈-[]) = <:-⊤ (⇉-⊤-f Γ-ctx)
  ≈-<: (⇉-⊤-f _)     (⇉-s-i ()) (≈-∙ ≈-⊤ ≈-[])
  ≈-<: (⇉-∀-f k₁-kd a₁⇉a₁⋯a₁) (⇉-∀-f k₂-kd a₂⇉a₂⋯a₂)
       (≈-∙ (≈-∀ k₁≋k₂ a₁≈a₂) ≈-[]) =
    let k₂<∷k₁ = ≋-<∷ k₂-kd k₁-kd (≋-sym k₁≋k₂)
    in <:-∀ k₂<∷k₁ (≈-<: (⇓-Nf⇉ k₂-kd k₂<∷k₁ a₁⇉a₁⋯a₁) a₂⇉a₂⋯a₂ a₁≈a₂)
            (⇉-∀-f k₁-kd a₁⇉a₁⋯a₁)
  ≈-<: (⇉-∀-f _ _) (⇉-s-i ()) (≈-∙ (≈-∀ _ _) ≈-[])
  ≈-<: (⇉-→-f a₁⇉a₁⋯a₁ b₁⇉b₁⋯b₁) (⇉-→-f a₂⇉a₂⋯a₂ b₂⇉b₂⋯b₂)
       (≈-∙ (≈-→ a₁≈a₂ b₁≈b₂) ≈-[]) =
    <:-→ (≈-<: a₂⇉a₂⋯a₂ a₁⇉a₁⋯a₁ (≈-sym a₁≈a₂)) (≈-<: b₁⇉b₁⋯b₁ b₂⇉b₂⋯b₂ b₁≈b₂)
  ≈-<: (⇉-→-f _ _) (⇉-s-i ()) (≈-∙ (≈-→ _ _) ≈-[])
  ≈-<: (⇉-s-i (∈-∙ x∈j₁ j₁⇉as₁⇉k₁)) (⇉-s-i (∈-∙ x∈j₂ j₂⇉as₂⇉k₂))
       (≈-∙ (≈-var x) as₁≈as₂) =
    let j  , Γ[x]≡kd-j  , j<∷j₁  , j-kd , _ = Var∈-inv x∈j₁
        j′ , Γ[x]≡kd-j′ , j′<∷j₂ , _    , _ = Var∈-inv x∈j₂
        j′≡j  = kd-inj (trans (sym Γ[x]≡kd-j′) Γ[x]≡kd-j)
        j<∷j₂ = subst (_ ⊢_<∷ _) j′≡j j′<∷j₂
        c , d , j⇉as₁≃as₂⇉c⋯d = ≈Sp-Sp≃ j-kd j<∷j₁ j<∷j₂
                                        j₁⇉as₁⇉k₁ j₂⇉as₂⇉k₂ as₁≈as₂
    in <:-∙ (⇉-var x (Var∈-ctx x∈j₁) Γ[x]≡kd-j) j⇉as₁≃as₂⇉c⋯d

  ≈-<:⇇ : ∀ {n} {Γ : Ctx n} {a b j} →
          Γ ⊢ j kd → Γ ⊢Nf a ⇇ j → Γ ⊢Nf b ⇇ j → a ≈ b → Γ ⊢ a <: b ⇇ j
  ≈-<:⇇ b⋯c-kd
        (⇇-⇑ a₁⇉b₁⋯c₁ (<∷-⋯ b<:b₁ c₁<:c))
        (⇇-⇑ a₂⇉b₂⋯c₂ (<∷-⋯ b<:b₂ c₂<:c)) a₁≈a₂ =
    <:-⇇ (⇇-⇑ a₁⇉b₁⋯c₁ (<∷-⋯ b<:b₁ c₁<:c)) (⇇-⇑ a₂⇉b₂⋯c₂ (<∷-⋯ b<:b₂ c₂<:c))
         (≈-<: (Nf⇉-s-i a₁⇉b₁⋯c₁) (Nf⇉-s-i a₂⇉b₂⋯c₂) a₁≈a₂)
  ≈-<:⇇ (kd-Π j-kd k-kd)
        (⇇-⇑ (⇉-Π-i j₁-kd a₁⇉k₁) (<∷-Π j<∷j₁ k₁<∷k Πj₁k₁-kd))
        (⇇-⇑ (⇉-Π-i j₂-kd a₂⇉k₂) (<∷-Π j<∷j₂ k₂<∷k Πj₂k₂-kd))
        (≈-∙ (≈-Λ ⌊k₁⌋≡⌊k₂⌋ a₁≈a₂) ≈-[]) =
    let a₁⇇k = ⇇-⇑ (⇓-Nf⇉ j-kd j<∷j₁ a₁⇉k₁) k₁<∷k
        a₂⇇k = ⇇-⇑ (⇓-Nf⇉ j-kd j<∷j₂ a₂⇉k₂) k₂<∷k
        a₁<:a₂⇇k = ≈-<:⇇ k-kd a₁⇇k a₂⇇k a₁≈a₂
    in <:-λ a₁<:a₂⇇k
            (⇇-⇑ (⇉-Π-i j₁-kd a₁⇉k₁) (<∷-Π j<∷j₁ k₁<∷k Πj₁k₁-kd))
            (⇇-⇑ (⇉-Π-i j₂-kd a₂⇉k₂) (<∷-Π j<∷j₂ k₂<∷k Πj₂k₂-kd))

  ≈Sp-Sp≃ : ∀ {n} {Γ : Ctx n} {as₁ as₂ j j₁ j₂ b₁ b₂ c₁ c₂} →
            Γ ⊢ j kd → Γ ⊢ j <∷ j₁ → Γ ⊢ j <∷ j₂ →
            Γ ⊢ j₁ ⇉∙ as₁ ⇉ b₁ ⋯ c₁ → Γ ⊢ j₂ ⇉∙ as₂ ⇉ b₂ ⋯ c₂ → as₁ ≈Sp as₂ →
            ∃ λ b → ∃ λ c → Γ ⊢ j ⇉∙ as₁ ≃ as₂ ⇉ b ⋯ c
  ≈Sp-Sp≃ j-kd (<∷-⋯ b₁<:b c<:c₁) j<∷b₂⋯c₂ ⇉-[] ⇉-[] ≈-[] = _ , _ , ≃-[]
  ≈Sp-Sp≃ (kd-Π j-kd k-kd)
          (<∷-Π j₁<∷j k<∷k₁ Πj₁k₁-kd) (<∷-Π j₂<∷j k<∷k₂ Πj₂k₂-kd)
          (⇉-∷ a₁⇇j₁ j₁-kd k₁[a₁]⇉bs₁⇉c₁⋯d₁)
          (⇉-∷ a₂⇇j₂ j₂-kd k₂[a₂]⇉bs₂⇉c₂⋯d₂) (≈-∷ a₁≈a₂ bs₁≈bs₂) =
    let a₁⇇j     = Nf⇇-⇑ a₁⇇j₁ j₁<∷j
        k[a₁]-kd = TK.kd-/⟨⟩ k-kd (⇇-hsub a₁⇇j j-kd (⌊⌋-⌊⌋≡ _))
        a₁≃a₂⇇j  = ≈-≃ j-kd a₁⇇j (Nf⇇-⇑ a₂⇇j₂ j₂<∷j) a₁≈a₂
        k[a₁]<∷k₁[a₁] = subst (λ l → _ ⊢ _ Kind[ _ ∈ l ] <∷ _) (<∷-⌊⌋ j₁<∷j)
                              (TK.<∷-/⟨⟩≃ k<∷k₁ (⇇-hsub a₁⇇j₁ j₁-kd (⌊⌋-⌊⌋≡ _)))
        k[a₂]<∷k₂[a₂] = subst (λ l → _ ⊢ _ Kind[ _ ∈ l ] <∷ _) (<∷-⌊⌋ j₂<∷j)
                              (TK.<∷-/⟨⟩≃ k<∷k₂ (⇇-hsub a₂⇇j₂ j₂-kd (⌊⌋-⌊⌋≡ _)))
        k[a₁]<∷k[a₂]  = TK.kd-/⟨⟩≃-<∷ k-kd (≃-hsub a₁≃a₂⇇j (⌊⌋-⌊⌋≡ _))
        k[a₁]<∷k₂[a₂] = <∷-trans k[a₁]<∷k[a₂] k[a₂]<∷k₂[a₂]
        c , d , k[a₁]⇉bs₁≃bs₂⇉c⋯d = ≈Sp-Sp≃ k[a₁]-kd k[a₁]<∷k₁[a₁] k[a₁]<∷k₂[a₂]
                                            k₁[a₁]⇉bs₁⇉c₁⋯d₁ k₂[a₂]⇉bs₂⇉c₂⋯d₂
                                            bs₁≈bs₂
    in c , d , ≃-∷ a₁≃a₂⇇j k[a₁]⇉bs₁≃bs₂⇉c⋯d
    where
      module TK = TrackSimpleKindsSubst

  ≈-≃ : ∀ {n} {Γ : Ctx n} {a b j} →
        Γ ⊢ j kd → Γ ⊢Nf a ⇇ j → Γ ⊢Nf b ⇇ j → a ≈ b → Γ ⊢ a ≃ b ⇇ j
  ≈-≃ j-kd a⇇j b⇇j a≈b =
    <:-antisym j-kd (≈-<:⇇ j-kd a⇇j b⇇j a≈b) (≈-<:⇇ j-kd b⇇j a⇇j (≈-sym a≈b))

  ≋-≅ : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j kd → Γ ⊢ k kd → j ≋ k → Γ ⊢ j ≅ k
  ≋-≅ j-kd k-kd j≋k =
    <∷-antisym j-kd k-kd (≋-<∷ j-kd k-kd j≋k) (≋-<∷ k-kd j-kd (≋-sym j≋k))

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
{-# OPTIONS --safe #-}
module Cubical.Data.Int.MoreInts.DeltaInt where

open import Cubical.Data.Int.MoreInts.DeltaInt.Base public

open import Cubical.Data.Int.MoreInts.DeltaInt.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical