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

module Cubical.Categories.Instances.Functors where

open import Cubical.Categories.Category
open import Cubical.Categories.Functor.Base
open import Cubical.Categories.NaturalTransformation.Base
open import Cubical.Categories.NaturalTransformation.Properties
open import Cubical.Categories.Morphism renaming (isIso to isIsoC)
open import Cubical.Foundations.Prelude

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

module _ (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD') ⦃ isCatD : isCategory D ⦄ where
  open Precategory
  open NatTrans
  open Functor

  FUNCTOR : Precategory (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) (ℓ-max (ℓ-max ℓC ℓC') ℓD')
  FUNCTOR .ob = Functor C D
  FUNCTOR .Hom[_,_] = NatTrans
  FUNCTOR .id = idTrans
  FUNCTOR ._⋆_ = seqTrans
  FUNCTOR .⋆IdL α = makeNatTransPath λ i x → D .⋆IdL (α .N-ob x) i
  FUNCTOR .⋆IdR α = makeNatTransPath λ i x → D .⋆IdR (α .N-ob x) i
  FUNCTOR .⋆Assoc α β γ = makeNatTransPath λ i x → D .⋆Assoc (α .N-ob x) (β .N-ob x) (γ .N-ob x) i

  isCatFUNCTOR : isCategory FUNCTOR
  isCatFUNCTOR .isSetHom = isSetNat

  open isIsoC renaming (inv to invC)
  -- component wise iso is an iso in Functor
  FUNCTORIso : ∀ {F G : Functor C D} (α : F ⇒ G)
             → (∀ (c : C .ob) → isIsoC {C = D} (α ⟦ c ⟧))
             → isIsoC {C = FUNCTOR} α
  FUNCTORIso α is .invC .N-ob c = (is c) .invC
  FUNCTORIso {F} {G} α is .invC .N-hom {c} {d} f
    = invMoveL areInv-αc
               ( α ⟦ c ⟧ ⋆⟨ D ⟩ (G ⟪ f ⟫ ⋆⟨ D ⟩ is d .invC)
               ≡⟨ sym (D .⋆Assoc _ _ _) ⟩
                 (α ⟦ c ⟧ ⋆⟨ D ⟩ G ⟪ f ⟫) ⋆⟨ D ⟩ is d .invC
               ≡⟨ sym (invMoveR areInv-αd (α .N-hom f)) ⟩
                 F ⟪ f ⟫
               ∎ )
    where
      areInv-αc : areInv (α ⟦ c ⟧) ((is c) .invC)
      areInv-αc = isIso→areInv (is c)

      areInv-αd : areInv (α ⟦ d ⟧) ((is d) .invC)
      areInv-αd = isIso→areInv (is d)
  FUNCTORIso α is .sec = makeNatTransPath (funExt (λ c → (is c) .sec))
  FUNCTORIso α is .ret = makeNatTransPath (funExt (λ c → (is c) .ret))

instance
  ⦃isCatFUNCTOR⦄ : {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} ⦃ isCatD : isCategory D ⦄
    → isCategory (FUNCTOR C D)
  ⦃isCatFUNCTOR⦄ {C = C} {D} = isCatFUNCTOR C D

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module Issue947 where

A : Set₁
A = Set
  where

B : Set₁
B = Set
  module _ where

C : Set₁
C = Set
  module M where

-- Andreas, 2020-04-25, #4623
-- These empty `where` blocks now generate warnings.

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
module Type.Isomorphism where

open import Functional
import      Lvl
open import Structure.Setoid
open import Structure.Function.Domain hiding (inverseₗ ; inverseᵣ)
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ ℓₑ₁ ℓₑ₂ : Lvl.Level

module _
  (A : Type{ℓ₁})
  (B : Type{ℓ₂})
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  where

  record _≅_ : Type{ℓ₁ Lvl.⊔ ℓₑ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓₑ₂} where
    field
      left  : A ← B
      right : A → B
      ⦃ inverseₗ ⦄ : Inverseₗ(right)(left)
      ⦃ inverseᵣ ⦄ : Inverseᵣ(right)(left)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import LogicalFormulae
open import Lists.Definition
open import Lists.Length
open import Numbers.Naturals.Semiring

module Lists.Concat where

appendEmptyList : {a : _} → {A : Set a} → (l : List A) → (l ++ [] ≡ l)
appendEmptyList [] = refl
appendEmptyList (x :: l) = applyEquality (_::_ x) (appendEmptyList l)

concatAssoc : {a : _} → {A : Set a} → (x : List A) → (y : List A) → (z : List A) → ((x ++ y) ++ z) ≡ x ++ (y ++ z)
concatAssoc [] m n = refl
concatAssoc (x :: l) m n = applyEquality (_::_ x) (concatAssoc l m n)

canMovePrepend : {a : _} → {A : Set a} → (l : A) → (x : List A) (y : List A) → ((l :: x) ++ y ≡ l :: (x ++ y))
canMovePrepend l [] n = refl
canMovePrepend l (x :: m) n = refl

lengthConcat : {a : _} {A : Set a} (l1 l2 : List A) → length (l1 ++ l2) ≡ length l1 +N length l2
lengthConcat [] l2 = refl
lengthConcat (x :: l1) l2 = applyEquality succ (lengthConcat l1 l2)


text:
-- Andreas, 2020-03-19, issue #4486
-- "did you mean?" now also for invalid imports

record Foo : Set₁ where
  field Θ : Set

open Foo using () renaming (θ to unwrap)

-- EXPECTED:
-- The module Foo doesn't export the following:
--   θ (did you mean 'Θ'?)

module M where
  private postulate S : Set

open M using (S)

-- EXPECTED:
-- The module M doesn't export the following:
--   S

module N where
  module O where
    record R : Set where
  open O public using (module R)

module N' where
  module O where
    record R : Set where
  open O public hiding (module R)

open N  using (R)
open N' using (module R)

-- EXPECTED:
-- The module N doesn't export the following:
--   R
-- The module N' doesn't export the following:
--   module R

module AB where
  record Ananas : Set where

open AB using (Bananas)

-- EXPECTED:
-- The module AB doesn't export the following:
--   Bananas (did you mean 'Ananas'?)

open AB using (module Bananas)

-- EXPECTED:
-- The module AB doesn't export the following:
--   module Bananas (did you mean 'Ananas'?)


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

module lists where

import 17-number-theory
open 17-number-theory public

unit-list :
  {l1 : Level} {A : UU l1} → A → list A
unit-list a = cons a nil

{- First we introduce the functoriality of the list operation, because it will
   come in handy when we try to define and prove more advanced things. -}

functor-list :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  list A → list B
functor-list f nil = nil
functor-list f (cons a x) = cons (f a) (functor-list f x)

identity-law-functor-list :
  {l1 : Level} {A : UU l1} →
  functor-list (id {A = A}) ~ id
identity-law-functor-list nil = refl
identity-law-functor-list (cons a x) =
  ap (cons a) (identity-law-functor-list x)

composition-law-functor-list :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} →
  (f : A → B) (g : B → C) →
  functor-list (g ∘ f) ~ (functor-list g ∘ functor-list f)
composition-law-functor-list f g nil = refl
composition-law-functor-list f g (cons a x) =
  ap (cons (g (f a))) (composition-law-functor-list f g x)

{- Concatenation of lists is an associative operation and nil is the unit for
   list concatenation. -}

assoc-concat-list :
  {l1 : Level} {A : UU l1} (x y z : list A) →
  Id (concat-list (concat-list x y) z) (concat-list x (concat-list y z))
assoc-concat-list nil y z = refl
assoc-concat-list (cons a x) y z = ap (cons a) (assoc-concat-list x y z)

left-unit-law-concat-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (concat-list nil x) x
left-unit-law-concat-list x = refl

right-unit-law-concat-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (concat-list x nil) x
right-unit-law-concat-list nil = refl
right-unit-law-concat-list (cons a x) =
  ap (cons a) (right-unit-law-concat-list x)

{- The length operation or course behaves well with respect to the other list
   operations. -}

length-nil :
  {l1 : Level} {A : UU l1} →
  Id (length-list {A = A} nil) zero-ℕ
length-nil = refl

length-concat-list :
  {l1 : Level} {A : UU l1} (x y : list A) →
  Id (length-list (concat-list x y)) (add-ℕ (length-list x) (length-list y))
length-concat-list nil y = inv (left-unit-law-add-ℕ (length-list y))
length-concat-list (cons a x) y =
  ( ap succ-ℕ (length-concat-list x y)) ∙
  ( inv (left-successor-law-add-ℕ (length-list x) (length-list y)))

{- We now prove the properties of flattening. -}

flatten-unit-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (flatten-list (unit-list x)) x
flatten-unit-list x = right-unit-law-concat-list x

length-flatten-list :
  {l1 : Level} {A : UU l1} (x : list (list A)) →
  Id ( length-list (flatten-list x))
     ( sum-list-ℕ (functor-list length-list x))
length-flatten-list nil = refl
length-flatten-list (cons a x) =
  ( length-concat-list a (flatten-list x)) ∙
  ( ap (add-ℕ (length-list a)) (length-flatten-list x))

flatten-concat-list :
  {l1 : Level} {A : UU l1} (x y : list (list A)) →
  Id ( flatten-list (concat-list x y))
     ( concat-list (flatten-list x) (flatten-list y))
flatten-concat-list nil y = refl
flatten-concat-list (cons a x) y =
  ( ap (concat-list a) (flatten-concat-list x y)) ∙
  ( inv (assoc-concat-list a (flatten-list x) (flatten-list y)))

flatten-flatten-list :
  {l1 : Level} {A : UU l1} (x : list (list (list A))) →
  Id ( flatten-list (flatten-list x))
     ( flatten-list (functor-list flatten-list x))
flatten-flatten-list nil = refl
flatten-flatten-list (cons a x) =
  ( flatten-concat-list a (flatten-list x)) ∙
  ( ap (concat-list (flatten-list a)) (flatten-flatten-list x))

{- Next, we prove the basic properties of list reversal. -}

reverse-unit-list :
  {l1 : Level} {A : UU l1} (a : A) →
  Id (reverse-list (unit-list a)) (unit-list a)
reverse-unit-list a = refl

length-reverse-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (length-list (reverse-list x)) (length-list x)
length-reverse-list nil = refl
length-reverse-list (cons a x) =
  ( length-concat-list (reverse-list x) (unit-list a)) ∙
  ( ap succ-ℕ (length-reverse-list x))

reverse-concat-list :
  {l1 : Level} {A : UU l1} (x y : list A) →
  Id ( reverse-list (concat-list x y))
     ( concat-list (reverse-list y) (reverse-list x))
reverse-concat-list nil y =
  inv (right-unit-law-concat-list (reverse-list y))
reverse-concat-list (cons a x) y =
  ( ap (λ t → concat-list t (unit-list a)) (reverse-concat-list x y)) ∙
  ( assoc-concat-list (reverse-list y) (reverse-list x) (unit-list a))

reverse-flatten-list :
  {l1 : Level} {A : UU l1} (x : list (list A)) →
  Id ( reverse-list (flatten-list x))
     ( flatten-list (reverse-list (functor-list reverse-list x)))
reverse-flatten-list nil = refl
reverse-flatten-list (cons a x) =
  ( reverse-concat-list a (flatten-list x)) ∙
  ( ( ap (λ t → concat-list t (reverse-list a)) (reverse-flatten-list x)) ∙
    ( ( ap
        ( concat-list
          ( flatten-list (reverse-list (functor-list reverse-list x))))
          ( inv (flatten-unit-list (reverse-list a)))) ∙
      ( inv
        ( flatten-concat-list
          ( reverse-list (functor-list reverse-list x))
          ( unit-list (reverse-list a))))))

reverse-reverse-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (reverse-list (reverse-list x)) x
reverse-reverse-list nil = refl
reverse-reverse-list (cons a x) =
  ( reverse-concat-list (reverse-list x) (unit-list a)) ∙
  ( ap (concat-list (unit-list a)) (reverse-reverse-list x))

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

{- Next we define the head and tail operations, and we define the operations
   of picking and removing the last element from a list. -}

head-list :
  {l1 : Level} {A : UU l1} → list A → list A
head-list nil = nil
head-list (cons a x) = unit-list a

tail-list :
  {l1 : Level} {A : UU l1} → list A → list A
tail-list nil = nil
tail-list (cons a x) = x

last-element-list :
  {l1 : Level} {A : UU l1} → list A → list A
last-element-list nil = nil
last-element-list (cons a nil) = unit-list a
last-element-list (cons a (cons b x)) = last-element-list (cons b x)

remove-last-element-list :
  {l1 : Level} {A : UU l1} → list A → list A
remove-last-element-list nil = nil
remove-last-element-list (cons a nil) = nil
remove-last-element-list (cons a (cons b x)) =
  cons a (remove-last-element-list (cons b x))

cons' :
  {l1 : Level} {A : UU l1} → list A → A → list A
cons' x a = concat-list x (unit-list a)

{- We prove the basic properties about heads and tails and their duals. -}

eta-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (concat-list (head-list x) (tail-list x)) x
eta-list nil = refl
eta-list (cons a x) = refl

eta-list' :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (concat-list (remove-last-element-list x) (last-element-list x)) x
eta-list' nil = refl
eta-list' (cons a nil) = refl
eta-list' (cons a (cons b x)) = ap (cons a) (eta-list' (cons b x))

last-element-cons' :
  {l1 : Level} {A : UU l1} (x : list A) (a : A) →
  Id (last-element-list (cons' x a)) (unit-list a)
last-element-cons' nil a = refl
last-element-cons' (cons b nil) a = refl
last-element-cons' (cons b (cons c x)) a =
  last-element-cons' (cons c x) a

head-concat-list :
  {l1 : Level} {A : UU l1} (x y : list A) →
  Id ( head-list (concat-list x y))
     ( head-list (concat-list (head-list x) (head-list y)))
head-concat-list nil nil = refl
head-concat-list nil (cons x y) = refl
head-concat-list (cons a x) y = refl

tail-concat-list :
  {l1 : Level} {A : UU l1} (x y : list A) →
  Id ( tail-list (concat-list x y))
     ( concat-list (tail-list x) (tail-list (concat-list (head-list x) y)))
tail-concat-list nil y = refl
tail-concat-list (cons a x) y = refl

last-element-concat-list :
  {l1 : Level} {A : UU l1} (x y : list A) →
  Id ( last-element-list (concat-list x y))
     ( last-element-list
       ( concat-list (last-element-list x) (last-element-list y)))
last-element-concat-list nil nil = refl
last-element-concat-list nil (cons b nil) = refl
last-element-concat-list nil (cons b (cons c y)) =
  last-element-concat-list nil (cons c y)
last-element-concat-list (cons a nil) nil = refl
last-element-concat-list (cons a nil) (cons b nil) = refl
last-element-concat-list (cons a nil) (cons b (cons c y)) =
  last-element-concat-list (cons a nil) (cons c y)
last-element-concat-list (cons a (cons b x)) y =
  last-element-concat-list (cons b x) y

remove-last-element-concat-list :
  {l1 : Level} {A : UU l1} (x y : list A) →
  Id ( remove-last-element-list (concat-list x y))
     ( concat-list
       ( remove-last-element-list (concat-list x (head-list y)))
       ( remove-last-element-list y))
remove-last-element-concat-list nil nil = refl
remove-last-element-concat-list nil (cons a nil) = refl
remove-last-element-concat-list nil (cons a (cons b y)) = refl
remove-last-element-concat-list (cons a nil) nil = refl
remove-last-element-concat-list (cons a nil) (cons b y) = refl
remove-last-element-concat-list (cons a (cons b x)) y =
  ap (cons a) (remove-last-element-concat-list (cons b x) y)

head-reverse-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (head-list (reverse-list x)) (last-element-list x)
head-reverse-list nil = refl
head-reverse-list (cons a nil) = refl
head-reverse-list (cons a (cons b x)) =
  ( ap head-list
    ( assoc-concat-list (reverse-list x) (unit-list b) (unit-list a))) ∙
  ( ( head-concat-list
      ( reverse-list x)
      ( concat-list (unit-list b) (unit-list a))) ∙
    ( ( inv (head-concat-list (reverse-list x) (unit-list b))) ∙
      ( head-reverse-list (cons b x))))

last-element-reverse-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (last-element-list (reverse-list x)) (head-list x)
last-element-reverse-list x =
  ( inv (head-reverse-list (reverse-list x))) ∙
  ( ap head-list (reverse-reverse-list x))

tail-concat-list' :
  {l1 : Level} {A : UU l1} (x y : list A) →
  Id ( tail-list (concat-list x y))
     ( concat-list
       ( tail-list x)
       ( tail-list (concat-list (last-element-list x) y)))
tail-concat-list' nil y = refl
tail-concat-list' (cons a nil) y = refl
tail-concat-list' (cons a (cons b x)) y =
  ap (cons b) (tail-concat-list' (cons b x) y)

tail-reverse-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (tail-list (reverse-list x)) (reverse-list (remove-last-element-list x))
tail-reverse-list nil = refl
tail-reverse-list (cons a nil) = refl
tail-reverse-list (cons a (cons b x)) =
  ( tail-concat-list' (reverse-list (cons b x)) (unit-list a)) ∙
  ( ( ap
      ( λ t → concat-list
        ( tail-list (reverse-list (cons b x)))
        ( tail-list (concat-list t (unit-list a))))
      ( last-element-cons' (reverse-list x) b)) ∙
    ( ap (λ t → concat-list t (unit-list a)) (tail-reverse-list (cons b x))))

remove-last-element-reverse-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (remove-last-element-list (reverse-list x)) (reverse-list (tail-list x))
remove-last-element-reverse-list x =
  ( inv (reverse-reverse-list (remove-last-element-list (reverse-list x)))) ∙
  ( ( inv (ap reverse-list (tail-reverse-list (reverse-list x)))) ∙
    ( ap (reverse-list ∘ tail-list) (reverse-reverse-list x)))

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

map-algebra-list :
  {l1 : Level} (A : UU l1) →
  coprod unit (A × list A) → list A
map-algebra-list A (inl star) = nil
map-algebra-list A (inr (pair a x)) = cons a x

inv-map-algebra-list :
  {l1 : Level} (A : UU l1) →
  list A → coprod unit (A × list A)
inv-map-algebra-list A nil = inl star
inv-map-algebra-list A (cons a x) = inr (pair a x)

issec-inv-map-algebra-list :
  {l1 : Level} (A : UU l1) →
  (map-algebra-list A ∘ inv-map-algebra-list A) ~ id
issec-inv-map-algebra-list A nil = refl
issec-inv-map-algebra-list A (cons a x) = refl

isretr-inv-map-algebra-list :
  {l1 : Level} (A : UU l1) →
  (inv-map-algebra-list A ∘ map-algebra-list A) ~ id
isretr-inv-map-algebra-list A (inl star) = refl
isretr-inv-map-algebra-list A (inr (pair a x)) = refl

is-equiv-map-algebra-list :
  {l1 : Level} (A : UU l1) → is-equiv (map-algebra-list A)
is-equiv-map-algebra-list A =
  is-equiv-has-inverse
    ( inv-map-algebra-list A)
    ( issec-inv-map-algebra-list A)
    ( isretr-inv-map-algebra-list A)

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

Eq-list :
  {l1 : Level} {A : UU l1} →
  list A → list A → UU l1
Eq-list nil nil = raise _ unit
Eq-list nil (cons x y) = raise _ empty
Eq-list (cons a x) nil = raise _ empty
Eq-list (cons a x) (cons b y) = (Id a b) × (Eq-list x y)

data Eq-list' {l1 : Level} {A : UU l1} : list A → list A → UU l1 where
  refl-nil : Eq-list' nil nil
  eq-cons :
    (x y : list A) (a b : A) →
    Eq-list' x y → Id a b → Eq-list' (cons a x) (cons b y)

refl-Eq-list :
  {l1 : Level} {A : UU l1} (x : list A) → Eq-list x x
refl-Eq-list nil = map-raise star
refl-Eq-list (cons a x) = pair refl (refl-Eq-list x)

contraction-total-Eq-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  (y : Σ (list A) (Eq-list x)) →
  Id (pair x (refl-Eq-list x)) y
contraction-total-Eq-list nil (pair nil (map-raise star)) = refl
contraction-total-Eq-list nil (pair (cons b y) (map-raise ()))
contraction-total-Eq-list (cons a x) (pair nil (map-raise ()))
contraction-total-Eq-list (cons a x) (pair (cons .a y) (pair refl e)) =
  {!!}

is-contr-total-Eq-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  is-contr (Σ (list A) (Eq-list x))
is-contr-total-Eq-list nil =
  pair
    ( pair nil (map-raise star))
    {!!}
is-contr-total-Eq-list (cons x x₁) = {!!}

max_stars_repo_name: tmoux/HoTT-Intro

max_issues_repo_name: tmoux/HoTT-Intro

max_forks_repo_name: tmoux/HoTT-Intro


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Reexport Data.List from the standard library.
--
-- Here we expose different names, for use in Contexts.
------------------------------------------------------------------------

module Base.Data.ContextList where

import Data.List as List
open List public
  using ()
  renaming
    ( [] to ∅ ; _∷_ to _•_
    ; map to mapContext
    )

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module PatternSynonyms where

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

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}

pattern z    = zero
pattern sz   = suc z
pattern ss x = suc (suc x)

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

test : z ≡ zero
test = refl

test′ : sz ≡ suc zero
test′ = refl

test″ : ss z ≡ suc (suc zero)
test″ = refl

test‴ : ss ≡ λ x → suc (suc x)
test‴ = refl

f : ℕ → ℕ
f z            = zero
f sz           = suc z
f (ss 0)       = 2
f (ss (suc n)) = n

test-f : f zero ≡ zero
test-f = refl

test-f′ : f (suc zero) ≡ suc zero
test-f′ = refl

test-f″ : f (suc (suc 0)) ≡ 2
test-f″ = refl

test-f‴ : ∀ {n} → f (suc (suc (suc n))) ≡ n
test-f‴ = refl

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

data L (A : Set) : Set where
  nil  : L A
  cons : A → L A → L A

pattern cc x y xs = cons x (cons y xs)

test-cc : ∀ {A} → cc ≡ λ (x : A) y xs → cons x (cons y xs)
test-cc = refl

crazyLength : ∀ {A} → L A → ℕ
crazyLength nil          = 0
crazyLength (cons x nil) = 1
crazyLength (cc x y xs)  = 9000

swap : ∀ {A} → L A → L A
swap nil          = nil
swap (cons x nil) = cons x nil
swap (cc x y xs)  = cc y x xs

test-swap : ∀ {xs} → swap (cons 1 (cons 2 xs)) ≡ cons 2 (cons 1 xs)
test-swap = refl

------------------------------------------------------------------------
-- refl and _

record ⊤ : Set where
  constructor tt

data _⊎_ (A B : Set) : Set where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

infixr 4 _,_
record Σ (A : Set)(B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ

_×_ : (A B : Set) → Set
A × B = Σ A λ _ → B

infixr 5 _+_
infixr 6 _*_

data Sig (O : Set) : Set₁ where
  ε ψ     : Sig O
  ρ       : (o : O) → Sig O
  ι       : (o : O) → Sig O
  _+_ _*_ : (Σ Σ′ : Sig O) → Sig O
  σ π     : (A : Set)(φ : A → Sig O) → Sig O

⟦_⟧ : ∀ {O} → Sig O → (Set → (O → Set) → (O → Set))
⟦ ε      ⟧ P R o = ⊤
⟦ ψ      ⟧ P R o = P
⟦ ρ o′   ⟧ P R o = R o′
⟦ ι o′   ⟧ P R o = o ≡ o′
⟦ Σ + Σ′ ⟧ P R o = ⟦ Σ ⟧ P R o ⊎ ⟦ Σ′ ⟧ P R o
⟦ Σ * Σ′ ⟧ P R o = ⟦ Σ ⟧ P R o × ⟦ Σ′ ⟧ P R o
⟦ σ A φ  ⟧ P R o = Σ A λ x → ⟦ φ x ⟧ P R o
⟦ π A φ  ⟧ P R o = (x : A) → ⟦ φ x ⟧ P R o

′List : Sig ⊤
′List = ε + ψ * ρ _

data μ {O}(Σ : Sig O)(P : Set)(o : O) : Set where
  ⟨_⟩ : ⟦ Σ ⟧ P (μ Σ P) o → μ Σ P o

List : Set → Set
List A = μ ′List A _

infixr 5 _∷_
pattern []       = ⟨ inj₁ _ ⟩
pattern _∷_ x xs = ⟨ inj₂ (x , xs) ⟩

length : ∀ {A} → List A → ℕ
length []       = zero
length (x ∷ xs) = suc (length xs)

test-list : List ℕ
test-list = 1 ∷ 2 ∷ []

test-length : length test-list ≡ 2
test-length = refl

′Vec : Sig ℕ
′Vec = ι 0
     + σ ℕ λ m → ψ * ρ m * ι (suc m)

Vec : Set → ℕ → Set
Vec A n = μ ′Vec A n

pattern []V     = ⟨ inj₁ refl ⟩
pattern _∷V_ x xs = ⟨ inj₂ (_ , x , xs , refl) ⟩

nilV : ∀ {A} → Vec A zero
nilV = []V

consV : ∀ {A n} → A → Vec A n → Vec A (suc n)
consV x xs = x ∷V xs

lengthV : ∀ {A n} → Vec A n → ℕ
lengthV []V       = 0
lengthV (x ∷V xs) = suc (lengthV xs)

test-lengthV : lengthV (consV 1 (consV 2 (consV 3 nilV))) ≡ 3
test-lengthV = refl

------------------------------------------------------------------------
-- .-patterns

pattern zr          = (.zero , refl)
pattern underscore² = _ , _

dot : (p : Σ ℕ λ n → n ≡ zero) → ⊤ × ⊤
dot zr = underscore²

------------------------------------------------------------------------
-- Implicit arguments

{-
pattern hiddenUnit = {_} -- XXX: We get lhs error msgs, can we refine
                         -- that?

imp : {p : ⊤} → ⊤
imp hiddenUnit = _
-}

data Box (A : Set) : Set where
  box : {x : A} → Box A

pattern [_] y = box {x = y}

b : Box ℕ
b = [ 1 ]

test-box : b ≡ box {x = 1}
test-box = refl

------------------------------------------------------------------------
-- Anonymous λs

g : ℕ → ℕ
g = λ { z → z
      ; sz → sz
      ; (ss n) → n
      }

test-g : g zero ≡ zero
test-g = refl

test-g′ : g sz ≡ suc zero
test-g′ = refl

test-g″ : ∀ {n} → g (suc (suc n)) ≡ n
test-g″ = refl

------------------------------------------------------------------------
-- λs

postulate
  X Y : Set
  h   : X → Y

p : (x : X)(y : Y) → h x ≡ y → ⊤
p x .((λ x → x) (h x)) refl = _

pattern app x = x , .((λ x → x) (h x))

p′ : (p : X × Y) → h (proj₁ p) ≡ proj₂ p → ⊤
p′ (app x) refl = _

------------------------------------------------------------------------
-- records

record Rec : Set where
  constructor rr
  field
    r : ℕ

rrr : (x : Rec) → x ≡ record { r = 0 } → ⊤
rrr .(record { r = 0}) refl = _

rrr′ : (x : Rec) → x ≡ record { r = 0 } → ⊤
rrr′ .(rr 0) refl = _

rrrr : (a : Rec × ℕ) → proj₁ a ≡ record { r = proj₂ a } → ⊤
rrrr (.(rr 0)       , 0)     refl = _
rrrr (.(rr (suc n)) , suc n) refl = _

pattern pair x = (.(record { r = x }) , x)

rrrr′ : (a : Rec × ℕ) → proj₁ a ≡ record { r = proj₂ a } → ⊤
rrrr′ (pair 0)       refl = _
rrrr′ (pair (suc n)) refl = _

------------------------------------------------------------------------
-- lets

pp : (x : X)(y : Y) → h x ≡ y → ⊤
pp x .(let i = (λ x → x) in i (h x)) refl = _

pattern llet x = x , .(let i = (λ x → x) in i (h x))

pp′ : (p : X × Y) → h (proj₁ p) ≡ proj₂ p → ⊤
pp′ (llet x) refl = _

------------------------------------------------------------------------
-- absurd patterns

pattern absurd = ()

data ⊥ : Set where

⊥-elim : ∀ {A : Set} → ⊥ → A
⊥-elim absurd

------------------------------------------------------------------------
-- ambiguous constructors

data ℕ2 : Set where
  zero : ℕ2
  suc  : ℕ2 -> ℕ2

-- This needs a type signature, because it is ambiguous:
amb : ℕ2
amb = suc (suc zero)

-- This isn't ambiguous, because the overloading is resolved when the
-- pattern synonym is scope-checked:
unamb = ss z

------------------------------------------------------------------------
-- underscore

pattern trivial = ._

trivf : (a : ⊤) -> a ≡ tt -> ⊤
trivf trivial refl = trivial

------------------------------------------------------------------------
-- let open

pattern nuts = .(let open Σ in z)

foo : (n : ℕ) -> n ≡ z -> ℕ
foo nuts refl = nuts

------------------------------------------------------------------------
-- pattern synonym inside unparamterised module

module M where
  pattern sss x = suc (suc (suc x))

  a : ℕ
  a = sss 2

mb : ℕ
mb = M.sss 0

mf : ℕ -> ℕ -> ℕ
mf (M.sss _) = M.sss
mf _         = \ _ -> 0

{-
module M (A : Set)(a : A) where
  pattern peep x = x , .a

  pop : (z : A × A) -> proj₂ z ≡ a -> ⊤
  pop (peep x) refl = _

  peep' = peep

pop' : (z : ⊤ × ⊤) -> proj₂ z ≡ tt -> ⊤
pop' (M.peep tt) refl = _

peep' = M.peep
-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
{-# OPTIONS --without-K --safe #-}
open import Algebra
open import Data.Bool.Base using (Bool; if_then_else_)
open import Function.Base using (_∘_)
open import Data.Integer.Base as ℤ
  using (ℤ; +_; +0; +[1+_]; -[1+_])
import Data.Integer.Properties as ℤP
open import Data.Integer.DivMod as ℤD
open import Data.Nat as ℕ using (ℕ; zero; suc)
open import Data.Nat.Properties as ℕP using (≤-step)
import Data.Nat.DivMod as ℕD
open import Level using (0ℓ)
open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Nullary.Decidable
open import Relation.Unary using (Pred)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong; sym; subst; trans; ≢-sym)
open import Relation.Binary
open import Data.Rational.Unnormalised as ℚ using (ℚᵘ; mkℚᵘ; _≢0; _/_; 0ℚᵘ; 1ℚᵘ; ↥_; ↧_; ↧ₙ_)
import Data.Rational.Unnormalised.Properties as ℚP
open import Algebra.Bundles
open import Algebra.Structures
open import Data.Empty
open import Data.Sum
open import Data.Maybe.Base
open import RealsRefactored
open import Data.List
open import Function.Structures {_} {_} {_} {_} {ℕ} _≡_ {ℕ} _≡_

{-
The solvers are used and renamed often enough to warrant them being opened up here
for the sake of consistency and cleanliness.
-}
open ℝ-Solver
open import NonReflectiveZ as ℤ-Solver using ()
  renaming
    ( solve to ℤsolve
    ; _⊕_   to _:+_
    ; _⊗_   to _:*_
    ; _⊖_   to _:-_
    ; ⊝_    to :-_
    ; _⊜_   to _:=_
    ; Κ     to ℤΚ
    )
open import NonReflectiveQ as ℚ-Solver using ()
  renaming
    ( solve to ℚsolve
    ; _⊕_   to _+:_
    ; _⊗_   to _*:_
    ; _⊖_   to _-:_
    ; ⊝_    to -:_
    ; _⊜_   to _=:_
    ; Κ     to ℚΚ
    )

open ℚᵘ
open ℝ

-- We use "Inequality" instead of "a≤x≤b" to avoid mixing up variable names in practice.
-- Intervals of the form (b,a) where a ≤ b will be nonempty of course.
record ⦅_,_⦆ (a b : ℝ) : Set where
  constructor mk⦅⦆
  field
    x          : ℝ
    inequality : a < x < b

record ⦅_,_⟧ (a b : ℝ) : Set where
  constructor mk⦅⟧
  field
    x          : ℝ
    inequality : a < x ≤ b

record ⟦_,_⦆ (a b : ℝ) : Set where
  constructor mk⟦⦆
  field
    x          : ℝ
    inequality : a ≤ x < b

record ⟦_,_⟧ (a b : ℝ) : Set where
  constructor mk⟦⟧
  field
    x          : ℝ
    inequality : a ≤ x ≤ b

record ⦅-∞,_⦆ (a : ℝ) : Set where
  constructor mk⦅-∞⦆
  field
    x          : ℝ
    inequality : x < a

record ⦅-∞,_⟧ (a : ℝ) : Set where
  constructor mk⦅-∞⟧
  field
    x          : ℝ
    inequality : x ≤ a

record ⦅_,∞⦆ (a : ℝ) : Set where
  constructor mk⦅∞⦆
  field
    x          : ℝ
    inequality : a < x

record ⟦_,∞⦆ (a : ℝ) : Set where
  constructor mk⟦∞⦆
  field
    x          : ℝ
    inequality : a ≤ x

_isNonvoid : {A : Set} -> (P : A -> Set) -> Set
_isNonvoid {A} P = ∃ λ (x : A) -> P x

Compact⟦_,_⟧ : ℝ -> ℝ -> Set
Compact⟦ a , b ⟧ = ∃ λ (x : ℝ) -> a ≤ x ≤ b

-- Too much bloat?
data _isUpperBoundOf_ (b : ℝ) (P : ℝ -> Set) : Set where
  upBound* : (∀ x -> P x -> x ≤ b) -> b isUpperBoundOf P

_isBoundedAbove : (P : ℝ -> Set) -> Set
P isBoundedAbove = ∃ λ (b : ℝ) -> b isUpperBoundOf P

_isSupremumOf_ : (s : ℝ) -> (P : ℝ -> Set) -> Set
s isSupremumOf P = s isUpperBoundOf P × (∀ ε -> ε > 0ℝ -> ∃ λ x -> P x × x > s - ε)

_hasSupremum : (ℝ -> Set) -> Set
P hasSupremum = ∃ λ s -> s isSupremumOf P

proposition-4-3-if : ∀ {P : ℝ -> Set} -> P isNonvoid -> P isBoundedAbove ->
                     (∀ {x y : ℝ} -> x < y -> y isUpperBoundOf P ⊎ ∃ λ a -> P a × x < a) ->
                     P hasSupremum
proposition-4-3-if {P} P≠Ø P≤U hyp = {!!}

proposition-4-3-onlyif : ∀ {P : ℝ -> Set} -> P isNonvoid -> P hasSupremum ->
                         ∀ {x y : ℝ} -> x < y -> y isUpperBoundOf P ⊎ ∃ λ a -> P a × x < a
proposition-4-3-onlyif {P} P≠Ø (s , upBound* P≤s , hyp) {x} {y} x<y = [ left , right ]′ (corollary-2-17 s x y x<y)
  where
    open ≤-Reasoning
    left : s < y -> y isUpperBoundOf P ⊎ ∃ λ a -> P a × x < a
    left s<y = inj₁ (upBound* (λ z Pz -> ≤-trans (P≤s z Pz) (<⇒≤ s<y)))

    right : s > x -> y isUpperBoundOf P ⊎ ∃ λ a -> P a × x < a
    right s>x = let aget = hyp (s - x) (x<y⇒0<y-x x s s>x); a = proj₁ aget in
                inj₂ (a , proj₁ (proj₂ aget) , (begin-strict
      x           ≈⟨ solve 2 (λ s x → x ⊜ s ⊖ (s ⊖ x)) ≃-refl s x ⟩
      s - (s - x) <⟨ proj₂ (proj₂ aget) ⟩
      a            ∎))

max_stars_repo_name: z-murray/AnalysisAgda

max_issues_repo_name: z-murray/AnalysisAgda

max_forks_repo_name: z-murray/AnalysisAgda


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

open import Cubical.Foundations.Prelude

open import Cubical.Data.FinData
open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Nat.Order using (zero-≤)
open import Cubical.Data.Vec.Base
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring
open import Cubical.Algebra.RingSolver.RawAlgebra renaming (⟨_⟩ to ⟨_⟩ᵣ)
open import Cubical.Algebra.RingSolver.AlgebraExpression public
open import Cubical.Algebra.RingSolver.CommRingHornerForms
open import Cubical.Algebra.RingSolver.CommRingEvalHom

private
  variable
    ℓ : Level

module EqualityToNormalform (R : CommRing {ℓ}) where
  νR = CommRing→RawℤAlgebra R
  open CommRingStr (snd R)
  open Theory (CommRing→Ring R)
  open Eval ℤAsRawRing νR
  open IteratedHornerOperations νR
  open HomomorphismProperties R

  ℤExpr : (n : ℕ) → Type _
  ℤExpr = Expr ℤAsRawRing (fst R)

  normalize : (n : ℕ) → ℤExpr n → IteratedHornerForms νR n
  normalize n (K r) = Constant n νR r
  normalize n (∣ k) = Variable n νR k
  normalize n (x +' y) =
    (normalize n x) +ₕ (normalize n y)
  normalize n (x ·' y) =
    (normalize n x) ·ₕ (normalize n y)
  normalize n (-' x) =  -ₕ (normalize n x)

  isEqualToNormalform :
            (n : ℕ)
            (e : ℤExpr n) (xs : Vec (fst R) n)
          → eval n (normalize n e) xs ≡ ⟦ e ⟧ xs
  isEqualToNormalform ℕ.zero (K r) [] = refl
  isEqualToNormalform (ℕ.suc n) (K r) (x ∷ xs) =
     eval (ℕ.suc n) (Constant (ℕ.suc n) νR r) (x ∷ xs)           ≡⟨ refl ⟩
     eval (ℕ.suc n) (0ₕ ·X+ Constant n νR r) (x ∷ xs)             ≡⟨ combineCasesEval 0ₕ (Constant n νR r) x xs ⟩
     eval (ℕ.suc n) 0ₕ (x ∷ xs) · x + eval n (Constant n νR r) xs
    ≡⟨ cong (λ u → u · x + eval n (Constant n νR r) xs) (Eval0H _ (x ∷ xs)) ⟩
     0r · x + eval n (Constant n νR r) xs
    ≡⟨ cong (λ u → u + eval n (Constant n νR r) xs) (0LeftAnnihilates _) ⟩
     0r + eval n (Constant n νR r) xs                             ≡⟨ +Lid _ ⟩
     eval n (Constant n νR r) xs                                  ≡⟨ isEqualToNormalform n (K r) xs ⟩
     _ ∎

  isEqualToNormalform (ℕ.suc n) (∣ zero) (x ∷ xs) =
    eval (ℕ.suc n) (1ₕ ·X+ 0ₕ) (x ∷ xs)           ≡⟨ refl ⟩
    eval (ℕ.suc n) 1ₕ (x ∷ xs) · x + eval n 0ₕ xs ≡⟨ cong (λ u → u · x + eval n 0ₕ xs)
                                                          (Eval1ₕ _ (x ∷ xs)) ⟩
    1r · x + eval n 0ₕ xs                         ≡⟨ cong (λ u → 1r · x + u ) (Eval0H _ xs) ⟩
    1r · x + 0r                                   ≡⟨ +Rid _ ⟩
    1r · x                                        ≡⟨ ·Lid _ ⟩
    x ∎
  isEqualToNormalform (ℕ.suc n) (∣ (suc k)) (x ∷ xs) =
      eval (ℕ.suc n) (0ₕ ·X+ Variable n νR k) (x ∷ xs)             ≡⟨ combineCasesEval 0ₕ (Variable n νR k) x xs ⟩
      eval (ℕ.suc n) 0ₕ (x ∷ xs) · x + eval n (Variable n νR k) xs
    ≡⟨ cong (λ u → u · x + eval n (Variable n νR k) xs) (Eval0H _ (x ∷ xs)) ⟩
      0r · x + eval n (Variable n νR k) xs
    ≡⟨ cong (λ u → u + eval n (Variable n νR k) xs) (0LeftAnnihilates _) ⟩
      0r + eval n (Variable n νR k) xs                             ≡⟨ +Lid _ ⟩
      eval n (Variable n νR k) xs
    ≡⟨ isEqualToNormalform n (∣ k) xs ⟩
      ⟦ ∣ (suc k) ⟧ (x ∷ xs) ∎

  isEqualToNormalform ℕ.zero (-' e) [] =
    eval ℕ.zero (-ₕ (normalize ℕ.zero e)) [] ≡⟨ -EvalDist ℕ.zero
                                                                  (normalize ℕ.zero e)
                                                                  [] ⟩
    - eval ℕ.zero (normalize ℕ.zero e) []    ≡⟨ cong -_
                                                          (isEqualToNormalform
                                                            ℕ.zero e [] ) ⟩
    - ⟦ e ⟧ [] ∎
  isEqualToNormalform (ℕ.suc n) (-' e) (x ∷ xs) =
    eval (ℕ.suc n) (-ₕ (normalize (ℕ.suc n) e)) (x ∷ xs) ≡⟨ -EvalDist (ℕ.suc n)
                                                                  (normalize
                                                                    (ℕ.suc n) e)
                                                                  (x ∷ xs) ⟩
    - eval (ℕ.suc n) (normalize (ℕ.suc n) e) (x ∷ xs)    ≡⟨ cong -_
                                                          (isEqualToNormalform
                                                            (ℕ.suc n) e (x ∷ xs) ) ⟩
    - ⟦ e ⟧ (x ∷ xs) ∎

  isEqualToNormalform ℕ.zero (e +' e₁) [] =
        eval ℕ.zero (normalize ℕ.zero e +ₕ normalize ℕ.zero e₁) []
      ≡⟨ +Homeval ℕ.zero (normalize ℕ.zero e) _ [] ⟩
        eval ℕ.zero (normalize ℕ.zero e) []
        + eval ℕ.zero (normalize ℕ.zero e₁) []
      ≡⟨ cong (λ u → u + eval ℕ.zero (normalize ℕ.zero e₁) [])
              (isEqualToNormalform ℕ.zero e []) ⟩
        ⟦ e ⟧ []
        + eval ℕ.zero (normalize ℕ.zero e₁) []
      ≡⟨ cong (λ u → ⟦ e ⟧ [] + u) (isEqualToNormalform ℕ.zero e₁ []) ⟩
        ⟦ e ⟧ [] + ⟦ e₁ ⟧ [] ∎
  isEqualToNormalform (ℕ.suc n) (e +' e₁) (x ∷ xs) =
        eval (ℕ.suc n) (normalize (ℕ.suc n) e
                         +ₕ normalize (ℕ.suc n) e₁) (x ∷ xs)
      ≡⟨ +Homeval (ℕ.suc n) (normalize (ℕ.suc n) e) _ (x ∷ xs) ⟩
        eval (ℕ.suc n) (normalize (ℕ.suc n) e) (x ∷ xs)
        + eval (ℕ.suc n) (normalize (ℕ.suc n) e₁) (x ∷ xs)
      ≡⟨ cong (λ u → u + eval (ℕ.suc n) (normalize (ℕ.suc n) e₁) (x ∷ xs))
              (isEqualToNormalform (ℕ.suc n) e (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs)
        + eval (ℕ.suc n) (normalize (ℕ.suc n) e₁) (x ∷ xs)
      ≡⟨ cong (λ u → ⟦ e ⟧ (x ∷ xs) + u)
              (isEqualToNormalform (ℕ.suc n) e₁ (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs) + ⟦ e₁ ⟧ (x ∷ xs) ∎

  isEqualToNormalform ℕ.zero (e ·' e₁) [] =
        eval ℕ.zero (normalize ℕ.zero e ·ₕ normalize ℕ.zero e₁) []
      ≡⟨ ·Homeval ℕ.zero (normalize ℕ.zero e) _ [] ⟩
        eval ℕ.zero (normalize ℕ.zero e) []
        · eval ℕ.zero (normalize ℕ.zero e₁) []
      ≡⟨ cong (λ u → u · eval ℕ.zero (normalize ℕ.zero e₁) [])
              (isEqualToNormalform ℕ.zero e []) ⟩
        ⟦ e ⟧ []
        · eval ℕ.zero (normalize ℕ.zero e₁) []
      ≡⟨ cong (λ u → ⟦ e ⟧ [] · u) (isEqualToNormalform ℕ.zero e₁ []) ⟩
        ⟦ e ⟧ [] · ⟦ e₁ ⟧ [] ∎

  isEqualToNormalform (ℕ.suc n) (e ·' e₁) (x ∷ xs) =
        eval (ℕ.suc n) (normalize (ℕ.suc n) e
                         ·ₕ normalize (ℕ.suc n) e₁) (x ∷ xs)
      ≡⟨ ·Homeval (ℕ.suc n) (normalize (ℕ.suc n) e) _ (x ∷ xs) ⟩
        eval (ℕ.suc n) (normalize (ℕ.suc n) e) (x ∷ xs)
        · eval (ℕ.suc n) (normalize (ℕ.suc n) e₁) (x ∷ xs)
      ≡⟨ cong (λ u → u · eval (ℕ.suc n) (normalize (ℕ.suc n) e₁) (x ∷ xs))
              (isEqualToNormalform (ℕ.suc n) e (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs)
        · eval (ℕ.suc n) (normalize (ℕ.suc n) e₁) (x ∷ xs)
      ≡⟨ cong (λ u → ⟦ e ⟧ (x ∷ xs) · u)
              (isEqualToNormalform (ℕ.suc n) e₁ (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs) · ⟦ e₁ ⟧ (x ∷ xs) ∎

  solve :
    {n : ℕ} (e₁ e₂ : ℤExpr n) (xs : Vec (fst R) n)
    (p : eval n (normalize n e₁) xs ≡ eval n (normalize n e₂) xs)
    → ⟦ e₁ ⟧ xs ≡ ⟦ e₂ ⟧ xs
  solve e₁ e₂ xs p =
    ⟦ e₁ ⟧ xs                  ≡⟨ sym (isEqualToNormalform _ e₁ xs) ⟩
    eval _ (normalize _ e₁) xs ≡⟨ p ⟩
    eval _ (normalize _ e₂) xs ≡⟨ isEqualToNormalform _ e₂ xs ⟩
    ⟦ e₂ ⟧ xs ∎

ℤExpr : (R : CommRing {ℓ}) (n : ℕ)
        → _
ℤExpr R n = EqualityToNormalform.ℤExpr R n

solve : (R : CommRing {ℓ})
        {n : ℕ} (e₁ e₂ : ℤExpr R n) (xs : Vec (fst R) n)
        (p : eval n (EqualityToNormalform.normalize R n e₁) xs ≡ eval n (EqualityToNormalform.normalize R n e₂) xs)
        → _
solve R = EqualityToNormalform.solve R

module VarNames3 (R : CommRing {ℓ}) where
  X1 : ℤExpr R 3
  X1 = ∣ Fin.zero

  X2 : ℤExpr R 3
  X2 = ∣ (suc Fin.zero)

  X3 : ℤExpr R 3
  X3 = ∣ (suc (suc Fin.zero))

module VarNames4 (R : CommRing {ℓ}) where
  X1 : ℤExpr R 4
  X1 = ∣ Fin.zero

  X2 : ℤExpr R 4
  X2 = ∣ (suc Fin.zero)

  X3 : ℤExpr R 4
  X3 = ∣ (suc (suc Fin.zero))

  X4 : ℤExpr R 4
  X4 = ∣ (suc (suc (suc Fin.zero)))

module VarNames5 (R : CommRing {ℓ}) where
  X1 : ℤExpr R 5
  X1 = ∣ Fin.zero

  X2 : ℤExpr R 5
  X2 = ∣ (suc Fin.zero)

  X3 : ℤExpr R 5
  X3 = ∣ (suc (suc Fin.zero))

  X4 : ℤExpr R 5
  X4 = ∣ (suc (suc (suc Fin.zero)))

  X5 : ℤExpr R 5
  X5 = ∣ (suc (suc (suc (suc Fin.zero))))

module VarNames6 (R : CommRing {ℓ}) where
  X1 : ℤExpr R 6
  X1 = ∣ Fin.zero

  X2 : ℤExpr R 6
  X2 = ∣ (suc Fin.zero)

  X3 : ℤExpr R 6
  X3 = ∣ (suc (suc Fin.zero))

  X4 : ℤExpr R 6
  X4 = ∣ (suc (suc (suc Fin.zero)))

  X5 : ℤExpr R 6
  X5 = ∣ (suc (suc (suc (suc Fin.zero))))

  X6 : ℤExpr R 6
  X6 = ∣ (suc (suc (suc (suc (suc Fin.zero)))))

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 --without-K --rewriting #-}

open import HoTT
open import cohomology.Theory
open import cohomology.PtdMapSequence
open import groups.ExactSequence
open import groups.Exactness
open import groups.HomSequence

open import cw.CW

module cw.cohomology.FirstCohomologyGroupOnDiag {i} (OT : OrdinaryTheory i)
  (⊙skel : ⊙Skeleton {i} 1) (ac : ⊙has-cells-with-choice 0 ⊙skel i) where

open OrdinaryTheory OT
open import cw.cohomology.TipCoboundary OT ⊙skel
open import cw.cohomology.TipGrid OT ⊙skel ac
open import cw.cohomology.WedgeOfCells OT

{-
    Coker ≃ C(X₁) = C(X)
              ^
              |
              |
           C(X₁/X₀)
             WoC

    WoC := Wedges of Cells
-}

open import groups.KernelImage {K = Lift-group {j = i} Unit-group} cst-hom cw-co∂-head CX₁/X₀-is-abelian
open import groups.KernelCstImage (Lift-group {j = i} Unit-group) cw-co∂-head CX₁/X₀-is-abelian

C-cw-iso-ker/im : C 1 ⊙⟦ ⊙skel ⟧ ≃ᴳ Ker/Im
C-cw-iso-ker/im = Ker-cst-quot-Im ⁻¹ᴳ ∘eᴳ Coker-cw-co∂-head ⁻¹ᴳ where

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
--------------------------------------------------------------------------------
-- This file provides functions for escaping
--------------------------------------------------------------------------------

module Parse.Escape where

open import Class.Map
open import Data.SimpleMap
open import Data.String using (fromList; toList)

open import Prelude
open import Prelude.Strings

private
  translationTable : SimpleMap String Char
  translationTable =
    ("newline" , '\n') ∷ ("space" , ' ') ∷ ("ast" , '*') ∷ ("sq" , '□') ∷
    ("lparen" , '(') ∷ ("rparen" , ')') ∷ ("lbrace" , '{') ∷ ("rbrace" , '}') ∷
    ("lsquare" , '[') ∷ ("rsquare" , ']') ∷ ("langle" , '<') ∷ ("rangle" , '>') ∷
    ("equal" , '=') ∷ ("dot" , '.') ∷ ("comma" , ',') ∷ ("colon" , ':') ∷ ("semicolon" , ';') ∷
    ("question" , '?') ∷ ("exclamation" , '!') ∷ ("at" , '@') ∷ ("doublequote" , '"') ∷
    ("ampersand" , '&') ∷ ("backslash" , '\\') ∷ ("slash" , '/') ∷ ("pipe" , '|') ∷ ("circumflex" , '^') ∷
    ("underscore" , '_') ∷ ("dollar" , '$') ∷ ("minus" , '-') ∷ ("forall" , '∀') ∷ ("exists" , '∃') ∷
    ("alpha" , 'α') ∷ ("beta" , 'β') ∷ ("gamma" , 'γ') ∷ ("delta" , 'δ') ∷ ("epsilon" , 'ε') ∷
    ("zeta" , 'ζ') ∷ ("eta" , 'η') ∷ ("theta" , 'θ') ∷ ("iota" , 'ι') ∷ ("kappa" , 'κ') ∷
    ("lambda" , 'λ') ∷ ("mu" , 'μ') ∷ ("nu" , 'ν') ∷ ("xi" , 'ξ') ∷ ("omicron" , 'ο') ∷ ("pi" , 'π') ∷
    ("rho" , 'ρ') ∷ ("varsigma" , 'ς') ∷ ("sigma" , 'σ') ∷ ("tau" , 'τ') ∷ ("upsilon" , 'υ') ∷
    ("phi" , 'φ') ∷ ("chi" , 'χ') ∷ ("psi" , 'ψ') ∷ ("omega" , 'ω') ∷
    ("Alpha" , 'Α') ∷ ("Beta" , 'Β') ∷ ("Gamma" , 'Γ') ∷ ("Delta" , 'Δ') ∷ ("Epsilon" , 'Ε') ∷
    ("Zeta" , 'Ζ') ∷ ("Eta" , 'Η') ∷ ("Theta" , 'Θ') ∷ ("Iota" , 'Ι') ∷ ("Kappa" , 'Κ') ∷
    ("Lambda" , 'Λ') ∷ ("Mu" , 'Μ') ∷ ("Nu" , 'Ν') ∷ ("Xi" , 'Ξ') ∷ ("Omicron" , 'Ο') ∷
    ("Pi" , 'Π') ∷ ("Rho" , 'Ρ') ∷ ("Varsigma" , 'Σ') ∷ ("Sigma" , 'Σ') ∷ ("Tau" , 'Τ') ∷
    ("Upsilon" , 'Υ') ∷ ("Phi" , 'Φ') ∷ ("Chi" , 'Χ') ∷ ("Psi" , 'Ψ') ∷ ("Omega" , 'Ω') ∷
    []

  escapeTable : SimpleMap Char String
  escapeTable = map swap translationTable

  isSpecialChar : Char → Bool
  isSpecialChar c = c ≣ '$' ∨ c ≣ '_' ∨ c ≣ '!' ∨ c ≣ '@' ∨ c ≣ '&' ∨ c ≣ '^'

-- accepts the head and tail of a string and returns the head of the full string without escape symbols
unescape : Char → String → Char
unescape c r = if ⌊ c ≟ '\\' ⌋ then (case strHead r of λ { nothing → c ; (just x) → x }) else c

groupEscaped : List Char → List (List Char)
groupEscaped = helper false
  where
    helper : Bool → List Char → List (List Char)
    helper b [] = []
    helper false (x ∷ l) = if ⌊ x ≟ '\\' ⌋ then helper true l else [ x ] ∷ helper false l
    helper true (x ∷ l) = ('\\' ∷ [ x ]) ∷ helper false l

translate : List Char → Maybe (List Char)
translate = helper ∘ splitMulti '='
  where
    helper : List (List Char) → Maybe (List Char)
    helper [] = just []
    helper (l ∷ []) = just l
    helper (l ∷ l₁ ∷ l₂) = do
      l' ← lookup (fromList l₁) translationTable
      l'' ← helper l₂
      return $ l + (if isSpecialChar l' then '\\' ∷ [ l' ] else [ l' ]) + l''

escapeChar : Char → List Char
escapeChar c = maybe (λ s → "=" ++ toList s ++ "=") [ c ] $ lookup c escapeTable

ruleToConstr : String → String
ruleToConstr = fromList ∘ concat ∘ helper ∘ groupEscaped ∘ toList
  where
    helper : List (List Char) → List (List Char)
    helper [] = []
    helper (l ∷ l₁) = (case l of λ where
      (c ∷ []) → if isSpecialChar c
        then [ c ]
        else escapeChar c
      ('\\' ∷ c ∷ []) → if isSpecialChar c
        then escapeChar c
        else l
      _ → l) ∷ (helper l₁)

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Indiscrete where

-- Category where all arrows are inhabited by a single element
open import Level
open import Data.Unit

open import Categories.Category

open import Relation.Binary.PropositionalEquality as ≡

Indiscrete : ∀ {o ℓ} (A : Set o) → Category o ℓ ℓ
Indiscrete {_} {ℓ} A = record
  { Obj       = A
  ; _⇒_       = λ _ _ → Lift ℓ ⊤
  ; _≈_       = _≡_
  ; id        = _
  ; _∘_       = _
  ; assoc     = refl
  ; sym-assoc = refl
  ; identityˡ = refl
  ; identityʳ = refl
  ; identity² = refl
  ; equiv     = isEquivalence
  ; ∘-resp-≈  = λ where
    refl refl → refl
  }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --copatterns #-}
-- {-# OPTIONS -v term:20 #-}
-- {-# OPTIONS --no-positivity-check #-}
-- {-# OPTIONS -v tc.def.fun:50  #-}
module CopatternNonterminating where

open import Common.Equality

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A
module S = Stream

illdefined : {A : Set} -> Stream A
S.head illdefined = S.head illdefined
S.tail illdefined = S.tail illdefined
-- should not termination-check

{-
illRepeat : {A : Set}(a : A) → Stream A
(       (S.head (illRepeat a))) = a
(S.head (S.tail (illRepeat a))) = a
(S.tail (S.tail (illRepeat a))) = S.tail (S.tail (illRepeat a))
-}

{-
-- deep copattern matches are not yet translated into something
-- that termination checks
illRepeat : {A : Set}(a : A) → Stream A
(       (S.head (illRepeat a))) = a
(S.head (S.tail (illRepeat a))) = a
(S.tail (S.tail (illRepeat a))) = (S.tail (illRepeat a))

record _≈_ {A : Set}(s t : Stream A) : Set where
  field
    head : S.head s ≡ S.head t
    tail : S.tail s ≈ S.tail t
module B = _≈_

repeat : {A : Set}(a : A) → Stream A
S.head (repeat a) = a
S.tail (repeat a) = repeat a

-- THIS SHOULD NOT TERMINATION CHECK WITH CURRENT TRANSLATION SEMANTICS
-- OF COPATTERNS
repeat′ : {A : Set}(a : A) → Stream A
(       (S.head (repeat′ a))) = a
(S.head (S.tail (repeat′ a))) = a
(S.tail (S.tail (repeat′ a))) = S.tail (repeat′ a) -- invalid projection

repeat≈repeat′ : {A : Set}(a : A) → repeat a ≈ repeat′ a
(       (B.head (repeat≈repeat′ a))) = refl
(B.head (B.tail (repeat≈repeat′ a))) = refl
(B.tail (B.tail (repeat≈repeat′ a))) = repeat≈repeat′ a
-}

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of functions, such as associativity and commutativity
------------------------------------------------------------------------

-- This file contains some core definitions which are reexported by
-- Algebra.FunctionProperties. They are placed here because
-- Algebra.FunctionProperties is a parameterised module, and some of
-- the parameters are irrelevant for these definitions.

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

module Algebra.FunctionProperties.Core where

open import Level

------------------------------------------------------------------------
-- Unary and binary operations

Op₁ : ∀ {ℓ} → Set ℓ → Set ℓ
Op₁ A = A → A

Op₂ : ∀ {ℓ} → Set ℓ → Set ℓ
Op₂ A = A → A → A


text:
------------------------------------------------------------------------
-- An alternative (non-standard) coinductive definition of weak
-- bisimilarity
------------------------------------------------------------------------

-- This definition is based on the function "wb" in Section 6.5.1 of
-- Pous and Sangiorgi's "Enhancements of the bisimulation proof
-- method".

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

open import Labelled-transition-system

module Bisimilarity.Weak.Alternative {ℓ} (lts : LTS ℓ) where

open import Prelude

import Bisimilarity
import Bisimilarity.Equational-reasoning-instances
open import Equational-reasoning

open LTS lts

-- We get weak bisimilarity by instantiating strong bisimilarity with
-- a different LTS.

private
  module WB = Bisimilarity (weak lts)

open WB public
  using ( ⟨_,_⟩
        ; [_]_≡_
        ; [_]_≡′_
        ; Extensionality
        ; force
        ; left-to-right
        ; right-to-left
        )
  renaming ( _∼_         to _≈_
           ; _∼′_        to _≈′_
           ; [_]_∼_      to [_]_≈_
           ; [_]_∼′_     to [_]_≈′_
           ; _⟶⟨_⟩ʳˡ_    to _⇒⟨_⟩ʳˡ_
           ; _[_]⟶⟨_⟩ʳˡ_ to _[_]⇒⟨_⟩ʳˡ_
           )

infix -3 lr-result-with-action lr-result-without-action

lr-result-without-action = WB.lr-result-without-action
lr-result-with-action    = WB.lr-result-with-action

syntax lr-result-without-action p′≈q′   q q⟶q′ = p′≈q′      ⇐⟨ q⟶q′ ⟩ q
syntax lr-result-with-action    p′≈q′ μ q q⟶q′ = p′≈q′ [ μ ]⇐⟨ q⟶q′ ⟩ q

-- Strongly bisimilar processes are weakly bisimilar.

private
  module SB = Bisimilarity lts

open SB using (_∼_; _∼′_; [_]_∼_; [_]_∼′_; force)

mutual

  ∼⇒≈ : ∀ {i p q} → p ∼ q → [ i ] p ≈ q
  ∼⇒≈ {i} = λ p∼q →
    ⟨ lr p∼q
    , Σ-map id (Σ-map id symmetric) ∘ lr (symmetric p∼q)
    ⟩
    where
    lr : ∀ {p p′ q μ} →
         p ∼ q → p [ μ ]⇒̂ p′ →
         ∃ λ q′ → q [ μ ]⇒̂ q′ × [ i ] p′ ≈′ q′
    lr p∼q p⇒̂p′ =
      Σ-map id (Σ-map id ∼⇒≈′) (SB.strong-is-weak⇒̂ p∼q p⇒̂p′)

  ∼⇒≈′ : ∀ {i p q} → p ∼ q → [ i ] p ≈′ q
  force (∼⇒≈′ p∼q) = ∼⇒≈ p∼q

∼⇒≈″ : ∀ {p q} → p ∼′ q → p ≈′ q
force (∼⇒≈″ p∼′q) = ∼⇒≈ (force p∼′q)

-- TODO: I suspect that the size isn't necessarily preserved: A weak
-- proof of a given size might require a strong proof which is much
-- larger, because a single weak transition might correspond to a
-- large number of strong transitions. I guess this has to be proved
-- for a particular LTS, or with certain assumptions about the LTS.

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
------------------------------------------------------------------------
-- A breadth-first backend which uses the derivative operator
------------------------------------------------------------------------

module TotalParserCombinators.BreadthFirst where

open import Data.List
open import Data.List.Membership.Propositional
open import Data.Product
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using (_↔_; module Inverse)
open import Relation.Binary.HeterogeneousEquality as H
  using () renaming (_≅_ to _≅H_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open import TotalParserCombinators.Congruence using (_≅P_; _∎)
import TotalParserCombinators.Congruence.Sound as CS
open import TotalParserCombinators.Derivative as D using (D)
import TotalParserCombinators.InitialBag as I
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics
open import TotalParserCombinators.Simplification as S using (simplify)

------------------------------------------------------------------------
-- A parametrised backend

-- The function f is applied before the derivative.

module Parse
  {Tok}
  (f : ∀ {R xs} → Parser Tok R xs → ∃ λ xs′ → Parser Tok R xs′)
  (f-correct : ∀ {R xs} (p : Parser Tok R xs) → proj₂ (f p) ≅P p)
  where

  -- The parsing function.

  parse : ∀ {R xs} → Parser Tok R xs → List Tok → List R
  parse {xs = xs} p []      = xs
  parse           p (t ∷ s) = parse (D t $ proj₂ $ f p) s

  -- A variant of f-correct.

  f-correct′ : ∀ {R xs} (p : Parser Tok R xs) → proj₂ (f p) ≅ p
  f-correct′ = CS.sound ∘ f-correct

  -- The backend is sound with respect to the semantics.

  sound : ∀ {R xs x} {p : Parser Tok R xs} (s : List Tok) →
          x ∈ parse p s → x ∈ p · s
  sound []      x∈p = I.sound _ x∈p
  sound (t ∷ s) x∈p =
    Inverse.to (f-correct′ _) ⟨$⟩ D.sound _ (sound s x∈p)

  -- The backend is complete with respect to the semantics.

  complete : ∀ {R xs x} {p : Parser Tok R xs} (s : List Tok) →
             x ∈ p · s → x ∈ parse p s
  complete []      x∈p = I.complete x∈p
  complete (t ∷ s) x∈p =
    complete s $ D.complete $ Inverse.from (f-correct′ _) ⟨$⟩ x∈p

  -- The backend does not introduce any unneeded ambiguity.
  --
  -- The proof complete is a left inverse of sound, so the (finite) type
  -- x ∈ parse p s contains at most as many proofs as x ∈ p · s. In
  -- other words, the output of parse p s can only contain n copies of x
  -- if there are at least n distinct parse trees in x ∈ p · s.

  complete∘sound : ∀ {R xs x} s
                   (p : Parser Tok R xs) (x∈p : x ∈ parse p s) →
                   complete s (sound s x∈p) ≡ x∈p
  complete∘sound []      p x∈p = I.complete∘sound p x∈p
  complete∘sound (t ∷ s) p x∈p
    rewrite Inverse.left-inverse-of (f-correct′ p)
              (D.sound (proj₂ (f p)) (sound s x∈p))
          | D.complete∘sound (proj₂ (f p)) (sound s x∈p) =
    complete∘sound s (D t $ proj₂ $ f p) x∈p

  -- The backend does not remove any ambiguity.
  --
  -- The proof complete is a right inverse of sound, which implies that
  -- the (finite) type x ∈ parse p s contains at least as many proofs as
  -- x ∈ p · s. In other words, if the output of parse p s contains n
  -- copies of x, then there are at most n distinct parse trees in
  -- x ∈ p · s.

  sound∘complete : ∀ {R xs x} {p : Parser Tok R xs}
                   (s : List Tok) (x∈p : x ∈ p · s) →
                   sound s (complete s x∈p) ≡ x∈p
  sound∘complete []      x∈p = I.sound∘complete x∈p
  sound∘complete (t ∷ s) x∈p
    rewrite sound∘complete s $
                  D.complete $ Inverse.from (f-correct′ _) ⟨$⟩ x∈p
          | D.sound∘complete $ Inverse.from (f-correct′ _) ⟨$⟩ x∈p
    = Inverse.right-inverse-of (f-correct′ _) x∈p

  -- The backend is correct.

  correct : ∀ {R xs x s} {p : Parser Tok R xs} →
            x ∈ p · s ↔ x ∈ parse p s
  correct {s = s} {p} = record
    { to         = P.→-to-⟶ $ complete s
    ; from       = P.→-to-⟶ $ sound s
    ; inverse-of = record
      { left-inverse-of  = sound∘complete s
      ; right-inverse-of = complete∘sound s p
      }
    }

------------------------------------------------------------------------
-- Specific instantiations

-- Parsing without simplification.

parse : ∀ {Tok R xs} → Parser Tok R xs → List Tok → List R
parse = Parse.parse -,_ _∎

parse-correct : ∀ {Tok R xs x s} {p : Parser Tok R xs} →
                x ∈ p · s ↔ x ∈ parse p s
parse-correct = Parse.correct -,_ _∎

-- Parsing with simplification.

parse-with-simplification :
  ∀ {Tok R xs} → Parser Tok R xs → List Tok → List R
parse-with-simplification = Parse.parse (λ p → -, simplify p) S.correct

parse-with-simplification-correct :
  ∀ {Tok R xs x s} {p : Parser Tok R xs} →
  x ∈ p · s ↔ x ∈ parse-with-simplification p s
parse-with-simplification-correct = Parse.correct _ S.correct

------------------------------------------------------------------------
-- An observation

-- The worst-case complexity of parse (without simplification) is /at
-- least/ exponential in the size of the input string. There is a
-- (finite) parser p whose derivative is p ∣ p (for any token). The
-- n-th derivative thus contains (at least) 2^n outermost occurrences
-- of _∣_, and these occurrences have to be traversed to compute the
-- initial bag of the n-th derivative.

parse-inefficient :
  ∀ {Tok R} → ∃ λ (p : Parser Tok R []) → ∀ t → D t p ≅H p ∣ p
parse-inefficient {R = R} =
  (fail {R = R} >>= (λ _ → fail) , λ t → H.refl)

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
-- Duplicate of #1984

postulate
  Path : {A : Set} → A → Set
  admit : {Z : Set} → Z
  X : Set
  Y : X → Set
  Y' : X → Set

record Square : Set₁ where
  field
    A : Set
    B : Set
    b : B
    coh : Path b

-- Spurious mutual block to trigger the problem
mut : Set

record Cocone : Set where
  field
    x : X

-- x : Cocone → X
-- x (mkCocone x) = x

postulate
  m n : Cocone
  fung : (c : Cocone) → Y' (Cocone.x c) → Path c

record CoconeDep (P : X → Set) : Set where
  inductive
  field
    x' : P (Cocone.x m)

s : Square
s .Square.A = CoconeDep Y
s .Square.B = Cocone
s .Square.b = n
s .Square.coh = fung _ (admit {Y' (Cocone.x (s .Square.b))})

mut = X

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- A type for values that should be erased at run-time
------------------------------------------------------------------------

-- The definitions in this module are reexported from Erased.

-- This module imports Equivalence.Erased.

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

open import Equality
open import Prelude hiding ([_,_])

module Erased.Level-2
  {c⁺} (eq-J : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq-J

open import Logical-equivalence using (_⇔_)

open import Bijection eq-J as Bijection using (_↔_; Has-quasi-inverse)
open import Embedding eq-J as Emb using (Embedding; Is-embedding)
open import Equivalence eq-J as Eq using (_≃_; Is-equivalence)
open import Equivalence.Erased eq-J as EEq
  using (_≃ᴱ_; Is-equivalenceᴱ)
open import Function-universe eq-J as F hiding (id; _∘_)
open import H-level eq-J as H-level
open import H-level.Closure eq-J
open import Injection eq-J using (_↣_; Injective)
open import Monad eq-J hiding (map; map-id; map-∘)
open import Preimage eq-J using (_⁻¹_)
open import Surjection eq-J using (_↠_; Split-surjective)

open import Erased.Level-1 eq-J as E₁
  hiding (module []-cong; module []-cong₂-⊔)

private

  variable
    a b c ℓ ℓ₁ ℓ₂ ℓ₃ : Level
    A B              : Type a
    eq k k′ p x y    : A
    P                : A → Type p
    f g              : A → B
    n                : ℕ

------------------------------------------------------------------------
-- Results that depend on an instantiation of the []-cong axioms (for
-- two universe levels as well as their maximum)

module []-cong₂-⊔
  (ax₁ : E₁.[]-cong-axiomatisation ℓ₁)
  (ax₂ : E₁.[]-cong-axiomatisation ℓ₂)
  (ax  : E₁.[]-cong-axiomatisation (ℓ₁ ⊔ ℓ₂))
  where

  open E₁.Erased-cong ax ax
  open E₁.[]-cong₁ ax₂
  open E₁.[]-cong₂ ax₁ ax₂
  open E₁.[]-cong₂-⊔ ax₁ ax₂ ax

  private

    module EEq′ = EEq.[]-cong₂-⊔ ax₁ ax₂ ax

  ----------------------------------------------------------------------
  -- Erased commutes with all kinds of functions (in some cases
  -- assuming extensionality)

  private

    -- A lemma used below.

    Erased-≃ᴱ↔≃ᴱ :
      {@0 A : Type ℓ₁} {@0 B : Type ℓ₂} →
      Erased (A ≃ᴱ B) ↝[ ℓ₁ ⊔ ℓ₂ ∣ ℓ₁ ⊔ ℓ₂ ]ᴱ (Erased A ≃ᴱ Erased B)
    Erased-≃ᴱ↔≃ᴱ {A = A} {B = B} ext =
      Erased (A ≃ᴱ B)                                                   ↔⟨ Erased-cong-≃ EEq.≃ᴱ-as-Σ ⟩
      Erased (∃ λ (f : A → B) → Is-equivalenceᴱ f)                      ↔⟨ Erased-Σ↔Σ ⟩
      (∃ λ (f : Erased (A → B)) → Erased (Is-equivalenceᴱ (erased f)))  ↝⟨ (Σ-cong Erased-Π↔Π-Erased λ _ →
                                                                            EEq′.Erased-Is-equivalenceᴱ↔Is-equivalenceᴱ ext) ⟩
      (∃ λ (f : Erased A → Erased B) → Is-equivalenceᴱ f)               ↔⟨ inverse EEq.≃ᴱ-as-Σ ⟩□
      Erased A ≃ᴱ Erased B                                              □

  -- Erased commutes with all kinds of functions (in some cases
  -- assuming extensionality).

  Erased-↝↝↝ :
    {@0 A : Type ℓ₁} {@0 B : Type ℓ₂} →
    Erased (A ↝[ k ] B) ↝[ ℓ₁ ⊔ ℓ₂ ∣ ℓ₁ ⊔ ℓ₂ ] (Erased A ↝[ k ] Erased B)
  Erased-↝↝↝ {k = implication} _ = from-isomorphism Erased-Π↔Π-Erased

  Erased-↝↝↝ {k = logical-equivalence} _ = from-isomorphism Erased-⇔↔⇔

  Erased-↝↝↝ {k = injection} {A = A} {B = B} ext =
    Erased (A ↣ B)                                              ↔⟨ Erased-cong-↔ ↣↔∃-Injective ⟩
    Erased (∃ λ (f : A → B) → Injective f)                      ↔⟨ Erased-Σ↔Σ ⟩
    (∃ λ (f : Erased (A → B)) → Erased (Injective (erased f)))  ↝⟨ Σ-cong Erased-Π↔Π-Erased (λ _ → Erased-Injective↔Injective ext) ⟩
    (∃ λ (f : Erased A → Erased B) → Injective f)               ↔⟨ inverse ↣↔∃-Injective ⟩□
    Erased A ↣ Erased B                                         □

  Erased-↝↝↝ {k = embedding} {A = A} {B = B} ext =
    Erased (Embedding A B)                                         ↔⟨ Erased-cong-↔ Emb.Embedding-as-Σ ⟩
    Erased (∃ λ (f : A → B) → Is-embedding f)                      ↔⟨ Erased-Σ↔Σ ⟩
    (∃ λ (f : Erased (A → B)) → Erased (Is-embedding (erased f)))  ↝⟨ Σ-cong Erased-Π↔Π-Erased (λ _ → Erased-Is-embedding↔Is-embedding ext) ⟩
    (∃ λ (f : Erased A → Erased B) → Is-embedding f)               ↔⟨ inverse Emb.Embedding-as-Σ ⟩□
    Embedding (Erased A) (Erased B)                                □

  Erased-↝↝↝ {k = surjection} {A = A} {B = B} {k = k′} ext =
    Erased (A ↠ B)                                                     ↔⟨ Erased-cong-↔ ↠↔∃-Split-surjective ⟩
    Erased (∃ λ (f : A → B) → Split-surjective f)                      ↔⟨ Erased-Σ↔Σ ⟩
    (∃ λ (f : Erased (A → B)) → Erased (Split-surjective (erased f)))  ↝⟨ Σ-cong Erased-Π↔Π-Erased (λ _ →
                                                                          Erased-Split-surjective↔Split-surjective
                                                                            (lower-extensionality? k′ ℓ₁ lzero ext)) ⟩
    (∃ λ (f : Erased A → Erased B) → Split-surjective f)               ↔⟨ inverse ↠↔∃-Split-surjective ⟩□
    Erased A ↠ Erased B                                                □

  Erased-↝↝↝ {k = bijection} {A = A} {B = B} ext =
    Erased (A ↔ B)                                                      ↔⟨ Erased-cong-↔ Bijection.↔-as-Σ ⟩
    Erased (∃ λ (f : A → B) → Has-quasi-inverse f)                      ↔⟨ Erased-Σ↔Σ ⟩
    (∃ λ (f : Erased (A → B)) → Erased (Has-quasi-inverse (erased f)))  ↝⟨ (Σ-cong Erased-Π↔Π-Erased λ _ →
                                                                            Erased-Has-quasi-inverse↔Has-quasi-inverse ext) ⟩
    (∃ λ (f : Erased A → Erased B) → Has-quasi-inverse f)               ↔⟨ inverse Bijection.↔-as-Σ ⟩□
    Erased A ↔ Erased B                                                 □

  Erased-↝↝↝ {k = equivalence} {A = A} {B = B} ext =
    Erased (A ≃ B)                                                   ↔⟨ Erased-cong-↔ Eq.≃-as-Σ ⟩
    Erased (∃ λ (f : A → B) → Is-equivalence f)                      ↔⟨ Erased-Σ↔Σ ⟩
    (∃ λ (f : Erased (A → B)) → Erased (Is-equivalence (erased f)))  ↝⟨ Σ-cong Erased-Π↔Π-Erased (λ _ → Erased-Is-equivalence↔Is-equivalence ext) ⟩
    (∃ λ (f : Erased A → Erased B) → Is-equivalence f)               ↔⟨ inverse Eq.≃-as-Σ ⟩□
    Erased A ≃ Erased B                                              □

  Erased-↝↝↝ {k = equivalenceᴱ} ext = Erased-≃ᴱ↔≃ᴱ ext

  -- Erased commutes with all kinds of functions (in some cases
  -- assuming extensionality).

  Erased-↝↔↝ :
    {@0 A : Type ℓ₁} {@0 B : Type ℓ₂} →
    Extensionality? k (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂) →
    Erased (A ↝[ k ] B) ↔ (Erased A ↝[ k ] Erased B)
  Erased-↝↔↝ {k = implication}         = λ _ → Erased-Π↔Π-Erased
  Erased-↝↔↝ {k = logical-equivalence} = λ _ → Erased-⇔↔⇔
  Erased-↝↔↝ {k = injection}           = Erased-↝↝↝
  Erased-↝↔↝ {k = embedding}           = Erased-↝↝↝
  Erased-↝↔↝ {k = surjection}          = Erased-↝↝↝
  Erased-↝↔↝ {k = bijection}           = Erased-↝↝↝
  Erased-↝↔↝ {k = equivalence}         = Erased-↝↝↝
  Erased-↝↔↝ {k = equivalenceᴱ}        = λ ([ ext ]) → Erased-≃ᴱ↔≃ᴱ ext

  -- Erased-↝↔↝ and Erased-↝↝↝ produce equal functions.

  to-Erased-↝↔↝≡to-Erased-↝↝↝ :
    {@0 A : Type ℓ₁} {@0 B : Type ℓ₂}
    (ext : Extensionality? k (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂))
    (ext′ : Extensionality? k′ (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂)) →
    _↔_.to (Erased-↝↔↝ {k = k} {A = A} {B = B} ext) ≡
    to-implication (Erased-↝↝↝ {k = k} {A = A} {B = B} {k = k′} ext′)
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = implication}         {k′ = implication}         _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = implication}         {k′ = logical-equivalence} _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = implication}         {k′ = injection}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = implication}         {k′ = embedding}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = implication}         {k′ = surjection}          _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = implication}         {k′ = bijection}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = implication}         {k′ = equivalence}         _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = implication}         {k′ = equivalenceᴱ}        _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = logical-equivalence} {k′ = implication}         _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = logical-equivalence} {k′ = logical-equivalence} _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = logical-equivalence} {k′ = injection}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = logical-equivalence} {k′ = embedding}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = logical-equivalence} {k′ = surjection}          _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = logical-equivalence} {k′ = bijection}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = logical-equivalence} {k′ = equivalence}         _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = logical-equivalence} {k′ = equivalenceᴱ}        _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = injection}           {k′ = implication}         _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = injection}           {k′ = logical-equivalence} _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = injection}           {k′ = injection}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = injection}           {k′ = embedding}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = injection}           {k′ = surjection}          _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = injection}           {k′ = bijection}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = injection}           {k′ = equivalence}         _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = injection}           {k′ = equivalenceᴱ}        _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = surjection}          {k′ = implication}         _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = surjection}          {k′ = logical-equivalence} _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = surjection}          {k′ = injection}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = surjection}          {k′ = embedding}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = surjection}          {k′ = surjection}          _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = surjection}          {k′ = bijection}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = surjection}          {k′ = equivalence}         _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = surjection}          {k′ = equivalenceᴱ}        _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = bijection}           {k′ = implication}         _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = bijection}           {k′ = logical-equivalence} _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = bijection}           {k′ = injection}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = bijection}           {k′ = embedding}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = bijection}           {k′ = surjection}          _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = bijection}           {k′ = bijection}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = bijection}           {k′ = equivalence}         _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = bijection}           {k′ = equivalenceᴱ}        _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalence}         {k′ = implication}         _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalence}         {k′ = logical-equivalence} _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalence}         {k′ = injection}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalence}         {k′ = embedding}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalence}         {k′ = surjection}          _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalence}         {k′ = bijection}           _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalence}         {k′ = equivalence}         _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalence}         {k′ = equivalenceᴱ}        _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalenceᴱ}        {k′ = implication}         _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalenceᴱ}        {k′ = logical-equivalence} _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalenceᴱ}        {k′ = injection}           _ ext = apply-ext ext λ _ → EEq′.to≡to→≡-Erased ext (refl _)
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalenceᴱ}        {k′ = embedding}           _ ext = apply-ext ext λ _ → EEq′.to≡to→≡-Erased ext (refl _)
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalenceᴱ}        {k′ = surjection}          _ ext = apply-ext ext λ _ → EEq′.to≡to→≡-Erased ext (refl _)
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalenceᴱ}        {k′ = bijection}           _ ext = apply-ext ext λ _ → EEq′.to≡to→≡-Erased ext (refl _)
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalenceᴱ}        {k′ = equivalence}         _ ext = apply-ext ext λ _ → EEq′.to≡to→≡-Erased ext (refl _)
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = equivalenceᴱ}        {k′ = equivalenceᴱ}        _ _   = refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = embedding} {k′ = implication}         ext _ = apply-ext ext λ _ → _↔_.to (Embedding-to-≡↔≡ ext) λ _ → refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = embedding} {k′ = logical-equivalence} ext _ = apply-ext ext λ _ → _↔_.to (Embedding-to-≡↔≡ ext) λ _ → refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = embedding} {k′ = injection}           ext _ = apply-ext ext λ _ → _↔_.to (Embedding-to-≡↔≡ ext) λ _ → refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = embedding} {k′ = embedding}           ext _ = apply-ext ext λ _ → _↔_.to (Embedding-to-≡↔≡ ext) λ _ → refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = embedding} {k′ = surjection}          ext _ = apply-ext ext λ _ → _↔_.to (Embedding-to-≡↔≡ ext) λ _ → refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = embedding} {k′ = bijection}           ext _ = apply-ext ext λ _ → _↔_.to (Embedding-to-≡↔≡ ext) λ _ → refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = embedding} {k′ = equivalence}         ext _ = apply-ext ext λ _ → _↔_.to (Embedding-to-≡↔≡ ext) λ _ → refl _
  to-Erased-↝↔↝≡to-Erased-↝↝↝ {k = embedding} {k′ = equivalenceᴱ}        ext _ = apply-ext ext λ _ → _↔_.to (Embedding-to-≡↔≡ ext) λ _ → refl _

  -- Erased preserves all kinds of functions.

  Erased-cong :
    {@0 A : Type ℓ₁} {@0 B : Type ℓ₂} →
    @0 A ↝[ k ] B → Erased A ↝[ k ] Erased B
  Erased-cong A↝B = Erased-↝↝↝ _ [ A↝B ]

  -- Dec-Erased preserves symmetric kinds of functions (in some cases
  -- assuming extensionality).

  Dec-Erased-cong :
    {@0 A : Type ℓ₁} {@0 B : Type ℓ₂} →
    @0 Extensionality? ⌊ k ⌋-sym (ℓ₁ ⊔ ℓ₂) lzero →
    @0 A ↝[ ⌊ k ⌋-sym ] B →
    Dec-Erased A ↝[ ⌊ k ⌋-sym ] Dec-Erased B
  Dec-Erased-cong ext A↝B =
    Erased-cong A↝B ⊎-cong Erased-cong (→-cong ext A↝B F.id)

------------------------------------------------------------------------
-- Results that depend on three instances of the axiomatisation of
-- []-cong, all for the same universe level

module []-cong₁₃
  (ax₁ : E₁.[]-cong-axiomatisation ℓ)
  (ax₂ : E₁.[]-cong-axiomatisation ℓ)
  (ax  : E₁.[]-cong-axiomatisation ℓ)
  where

  -- Note that []-cong₂-⊔, which contains Erased-cong, is instantiated
  -- with all of the module parameters.

  open []-cong₂-⊔ ax₁ ax₂ ax

  private
    module BC₁ = E₁.[]-cong₁ ax₁
    module BC₂ = E₁.[]-cong₁ ax₂

  ----------------------------------------------------------------------
  -- Erased-cong maps F.id to F.id for all kinds of functions (in some
  -- cases assuming extensionality)

  private

    -- Lemmas used in the implementation of Erased-cong-id.

    Erased-cong-≃-id :
      {@0 A : Type ℓ} →
      Extensionality ℓ ℓ →
      Erased-cong {k = equivalence} F.id ≡ F.id {A = Erased A}
    Erased-cong-≃-id ext = Eq.lift-equality ext (refl _)

    Erased-cong-≃ᴱ-id :
      {@0 A : Type ℓ} →
      Erased (Extensionality ℓ ℓ) →
      Erased-cong {k = equivalenceᴱ} F.id ≡ F.id {A = Erased A}
    Erased-cong-≃ᴱ-id [ ext ] =
      EEq.[]-cong₂-⊔.to≡to→≡-Erased ax₁ ax₂ ax ext (refl _)

    Erased-cong-Embedding-id :
      {@0 A : Type ℓ} →
      Extensionality ℓ ℓ →
      Erased-cong {k = embedding} F.id ≡ F.id {A = Erased A}
    Erased-cong-Embedding-id ext =
      _↔_.to (Embedding-to-≡↔≡ ext) λ _ → refl _

    Erased-cong-↠-id :
      {@0 A : Type ℓ} →
      Extensionality ℓ ℓ →
      Erased-cong {k = surjection} F.id ≡ F.id {A = Erased A}
    Erased-cong-↠-id ext =                              $⟨ lemma ⟩
      _↔_.to ↠↔∃-Split-surjective (Erased-cong F.id) ≡
      _↔_.to ↠↔∃-Split-surjective F.id                  ↝⟨ Eq.≃-≡ (from-isomorphism ↠↔∃-Split-surjective) ⟩□

      Erased-cong F.id ≡ F.id                           □
      where
      lemma :
        (map id , λ x → [ erased x ] , BC₂.[]-cong [ refl _ ]) ≡
        (id , λ x → x , refl _)
      lemma =
        cong (_ ,_) $ apply-ext ext λ _ → cong (_ ,_) BC₂.[]-cong-[refl]

    Erased-cong-↔-id :
      {@0 A : Type ℓ} →
      Extensionality ℓ ℓ →
      Erased-cong {k = bijection} F.id ≡ F.id {A = Erased A}
    Erased-cong-↔-id ext =                          $⟨ lemma ⟩
      _↔_.to Bijection.↔-as-Σ (Erased-cong F.id) ≡
      _↔_.to Bijection.↔-as-Σ F.id                  ↝⟨ Eq.≃-≡ (from-isomorphism Bijection.↔-as-Σ) ⟩□

      Erased-cong F.id ≡ F.id                       □
      where
      lemma :
        ( map id
        , map id
        , (λ { [ x ] → BC₂.[]-cong [ refl x ] })
        , (λ { [ x ] → BC₁.[]-cong [ refl x ] })
        ) ≡
        (id , id , refl , refl)
      lemma = cong (λ p → id , id , p) $ cong₂ _,_
        (apply-ext ext λ _ → BC₂.[]-cong-[refl])
        (apply-ext ext λ _ → BC₁.[]-cong-[refl])

    Erased-cong-↣-id :
      {@0 A : Type ℓ} →
      Extensionality ℓ ℓ →
      Erased-cong {k = injection} F.id ≡ F.id {A = Erased A}
    Erased-cong-↣-id ext =                       $⟨ lemma ⟩
      _↔_.to ↣↔∃-Injective (Erased-cong F.id) ≡
      _↔_.to ↣↔∃-Injective F.id                  ↝⟨ Eq.≃-≡ (from-isomorphism ↣↔∃-Injective) ⟩□

      Erased-cong F.id ≡ F.id                    □
      where
      lemma :
        ( map id
        , λ {_ _} → _↣_.injective (Erased-cong F.id)
        ) ≡
        (id , λ {_ _} → _↣_.injective F.id)
      lemma =
        cong (_ ,_) $
        implicit-extensionality ext λ _ →
        implicit-extensionality ext λ _ →
        apply-ext ext λ eq →
          BC₁.[]-cong (BC₂.[]-cong⁻¹ eq)  ≡⟨ []-cong-unique ax₁ ax₂ ⟩
          BC₂.[]-cong (BC₂.[]-cong⁻¹ eq)  ≡⟨ _↔_.right-inverse-of BC₂.Erased-≡↔[]≡[] _ ⟩∎
          eq                              ∎

  -- Erased-cong maps F.id to F.id for all kinds of functions (in some
  -- cases assuming extensionality).

  Erased-cong-id :
    {@0 A : Type ℓ} →
    Extensionality? k ℓ ℓ →
    Erased-cong F.id ≡ F.id {k = k} {A = Erased A}
  Erased-cong-id {k = implication}         = λ _ → map-id
  Erased-cong-id {k = logical-equivalence} = λ _ → Erased-cong-⇔-id
  Erased-cong-id {k = injection}           = Erased-cong-↣-id
  Erased-cong-id {k = embedding}           = Erased-cong-Embedding-id
  Erased-cong-id {k = surjection}          = Erased-cong-↠-id
  Erased-cong-id {k = bijection}           = Erased-cong-↔-id
  Erased-cong-id {k = equivalence}         = Erased-cong-≃-id
  Erased-cong-id {k = equivalenceᴱ}        = Erased-cong-≃ᴱ-id

------------------------------------------------------------------------
-- Results that depend on instances of the axiomatisation of []-cong
-- for three universe levels, as well as for the maximum of each pair
-- drawn from these three levels

module []-cong₃-⊔
  (ax₁  : []-cong-axiomatisation ℓ₁)
  (ax₂  : []-cong-axiomatisation ℓ₂)
  (ax₃  : []-cong-axiomatisation ℓ₃)
  (ax₁₂ : []-cong-axiomatisation (ℓ₁ ⊔ ℓ₂))
  (ax₁₃ : []-cong-axiomatisation (ℓ₁ ⊔ ℓ₃))
  (ax₂₃ : []-cong-axiomatisation (ℓ₂ ⊔ ℓ₃))
  where

  private
    module EC₁ = []-cong₂-⊔ ax₁ ax₃ ax₁₃
    module EC₂ = []-cong₂-⊔ ax₂ ax₃ ax₂₃
    module EC₃ = []-cong₂-⊔ ax₁ ax₂ ax₁₂

  ----------------------------------------------------------------------
  -- Erased-cong commutes with F._∘_ for all kinds of functions (in
  -- some cases assuming extensionality)

  private

    -- Lemmas used in the implementation of Erased-cong-∘.

    Erased-cong-≃-∘ :
      {@0 A : Type ℓ₁} {@0 B : Type ℓ₂} {@0 C : Type ℓ₃} →
      Extensionality (ℓ₁ ⊔ ℓ₃) (ℓ₁ ⊔ ℓ₃) →
      (@0 f : B ≃ C) (@0 g : A ≃ B) →
      EC₁.Erased-cong {k = equivalence} (f F.∘ g) ≡
      EC₂.Erased-cong f F.∘ EC₃.Erased-cong g
    Erased-cong-≃-∘ ext _ _ = Eq.lift-equality ext (refl _)

    Erased-cong-≃ᴱ-∘ :
      {@0 A : Type ℓ₁} {@0 B : Type ℓ₂} {@0 C : Type ℓ₃} →
      Erased (Extensionality (ℓ₁ ⊔ ℓ₃) (ℓ₁ ⊔ ℓ₃)) →
      (@0 f : B ≃ᴱ C) (@0 g : A ≃ᴱ B) →
      EC₁.Erased-cong {k = equivalenceᴱ} (f F.∘ g) ≡
      EC₂.Erased-cong f F.∘ EC₃.Erased-cong g
    Erased-cong-≃ᴱ-∘ [ ext ] _ _ =
      EEq.[]-cong₂-⊔.to≡to→≡-Erased ax₁ ax₃ ax₁₃ ext (refl _)

    Erased-cong-Embedding-∘ :
      {@0 A : Type ℓ₁} {@0 B : Type ℓ₂} {@0 C : Type ℓ₃} →
      Extensionality (ℓ₁ ⊔ ℓ₃) (ℓ₁ ⊔ ℓ₃) →
      (@0 f : Embedding B C) (@0 g : Embedding A B) →
      EC₁.Erased-cong {k = embedding} (f F.∘ g) ≡
      EC₂.Erased-cong f F.∘ EC₃.Erased-cong g
    Erased-cong-Embedding-∘ ext _ _ =
      _↔_.to (Embedding-to-≡↔≡ ext) λ _ → refl _

    right-inverse-of-cong-∘ :
      ∀ {ℓ₁ ℓ₂ ℓ₃}
      (ax₁  : []-cong-axiomatisation ℓ₁)
      (ax₂  : []-cong-axiomatisation ℓ₂)
      (ax₃  : []-cong-axiomatisation ℓ₃)
      (ax₁₂ : []-cong-axiomatisation (ℓ₁ ⊔ ℓ₂))
      (ax₁₃ : []-cong-axiomatisation (ℓ₁ ⊔ ℓ₃))
      (ax₂₃ : []-cong-axiomatisation (ℓ₂ ⊔ ℓ₃)) →
      let module EC₁′ = []-cong₂-⊔ ax₁ ax₃ ax₁₃
          module EC₂′ = []-cong₂-⊔ ax₂ ax₃ ax₂₃
          module EC₃′ = []-cong₂-⊔ ax₁ ax₂ ax₁₂
      in
      ∀ {@0 A : Type ℓ₁} {@0 B : Type ℓ₂} {@0 C : Type ℓ₃} {x} →
      (@0 f : B ↠ C) (@0 g : A ↠ B) →
      _↠_.right-inverse-of (EC₁′.Erased-cong (f F.∘ g)) x ≡
      _↠_.right-inverse-of (EC₂′.Erased-cong f F.∘ EC₃′.Erased-cong g) x
    right-inverse-of-cong-∘ ax₁ ax₂ ax₃ _ _ _ {x = [ x ]} f g =
      BC₃.[]-cong [ trans (cong (_↠_.to f)
                                  (_↠_.right-inverse-of g
                                     (_↠_.from f x)))
                               (_↠_.right-inverse-of f x)
                  ]                                         ≡⟨ E₁.[]-cong₁.[]-cong-trans ax₃ ⟩

      trans (BC₃.[]-cong [ cong (_↠_.to f)
                             (_↠_.right-inverse-of g
                                (_↠_.from f x)) ])
        (BC₃.[]-cong [ _↠_.right-inverse-of f x ])          ≡⟨ cong (λ p → trans p _) (E₁.[]-cong₂.[]-cong-cong ax₂ ax₃) ⟩∎

      trans (cong (map (_↠_.to f))
                     (BC₂.[]-cong [ _↠_.right-inverse-of g
                                      (_↠_.from f x) ]))
        (BC₃.[]-cong [ _↠_.right-inverse-of f x ])          ∎
      where
      module BC₂ = E₁.[]-cong₁ ax₂
      module BC₃ = E₁.[]-cong₁ ax₃

    Erased-cong-↠-∘ :
      {@0 A : Type ℓ₁} {@0 B : Type ℓ₂} {@0 C : Type ℓ₃} →
      Extensionality ℓ₃ (ℓ₁ ⊔ ℓ₃) →
      (@0 f : B ↠ C) (@0 g : A ↠ B) →
      EC₁.Erased-cong {k = surjection} (f F.∘ g) ≡
      EC₂.Erased-cong f F.∘ EC₃.Erased-cong g
    Erased-cong-↠-∘ ext f g =                                    $⟨ lemma ⟩
      _↔_.to ↠↔∃-Split-surjective (EC₁.Erased-cong (f F.∘ g)) ≡
      _↔_.to ↠↔∃-Split-surjective
        (EC₂.Erased-cong f F.∘ EC₃.Erased-cong g)                ↝⟨ Eq.≃-≡ (from-isomorphism ↠↔∃-Split-surjective) ⟩□

      EC₁.Erased-cong (f F.∘ g) ≡
      EC₂.Erased-cong f F.∘ EC₃.Erased-cong g                    □
      where
      lemma :
        ( map (_↠_.to f ∘ _↠_.to g)
        , (λ x →
               [ _↠_.from g (_↠_.from f (erased x)) ]
             , _↠_.right-inverse-of (EC₁.Erased-cong (f F.∘ g)) x)
        )
        ≡
        ( (λ x → [ _↠_.to f (_↠_.to g (erased x)) ])
        , (λ x →
               [ _↠_.from g (_↠_.from f (erased x)) ]
             , _↠_.right-inverse-of
                 (EC₂.Erased-cong f F.∘ EC₃.Erased-cong g) x)
        )
      lemma =
        cong (_ ,_) $ apply-ext ext λ ([ x ]) →
          cong ([ _↠_.from g (_↠_.from f x) ] ,_)
            (right-inverse-of-cong-∘ ax₁ ax₂ ax₃ ax₁₂ ax₁₃ ax₂₃ f g)

    Erased-cong-↔-∘ :
      {@0 A : Type ℓ₁} {@0 B : Type ℓ₂} {@0 C : Type ℓ₃} →
      Extensionality (ℓ₁ ⊔ ℓ₃) (ℓ₁ ⊔ ℓ₃) →
      (@0 f : B ↔ C) (@0 g : A ↔ B) →
      EC₁.Erased-cong {k = bijection} (f F.∘ g) ≡
      EC₂.Erased-cong f F.∘ EC₃.Erased-cong g
    Erased-cong-↔-∘ ext f g =                                            $⟨ lemma ⟩
      _↔_.to Bijection.↔-as-Σ (EC₁.Erased-cong (f F.∘ g)) ≡
      _↔_.to Bijection.↔-as-Σ (EC₂.Erased-cong f F.∘ EC₃.Erased-cong g)  ↝⟨ Eq.≃-≡ (from-isomorphism Bijection.↔-as-Σ) ⟩□

      EC₁.Erased-cong (f F.∘ g) ≡
      EC₂.Erased-cong f F.∘ EC₃.Erased-cong g                            □
      where
      lemma :
        ( map (_↔_.to f ∘ _↔_.to g)
        , map (_↔_.from g ∘ _↔_.from f)
        , _↔_.right-inverse-of (EC₁.Erased-cong (f F.∘ g))
        , _↔_.left-inverse-of (EC₁.Erased-cong (f F.∘ g))
        )
        ≡
        ( (λ x → [ _↔_.to f (_↔_.to g (erased x)) ])
        , (λ x → [ _↔_.from g (_↔_.from f (erased x)) ])
        , _↔_.right-inverse-of (EC₂.Erased-cong f F.∘ EC₃.Erased-cong g)
        , _↔_.left-inverse-of (EC₂.Erased-cong f F.∘ EC₃.Erased-cong g)
        )
      lemma =
        cong (λ p → map (_↔_.to f ∘ _↔_.to g)
                  , map (_↔_.from g ∘ _↔_.from f) , p) $
        cong₂ _,_
          (apply-ext (lower-extensionality ℓ₁ ℓ₁ ext) λ _ →
             right-inverse-of-cong-∘ ax₁ ax₂ ax₃ ax₁₂ ax₁₃ ax₂₃
               (_↔_.surjection f) (_↔_.surjection g))
          (apply-ext (lower-extensionality ℓ₃ ℓ₃ ext) λ _ →
           right-inverse-of-cong-∘ ax₃ ax₂ ax₁ ax₂₃ ax₁₃ ax₁₂
              (_↔_.surjection $ inverse g)
              (_↔_.surjection $ inverse f))

    Erased-cong-↣-∘ :
      {@0 A : Type ℓ₁} {@0 B : Type ℓ₂} {@0 C : Type ℓ₃} →
      Extensionality (ℓ₁ ⊔ ℓ₃) (ℓ₁ ⊔ ℓ₃) →
      (@0 f : B ↣ C) (@0 g : A ↣ B) →
      EC₁.Erased-cong {k = injection} (f F.∘ g) ≡
      EC₂.Erased-cong f F.∘ EC₃.Erased-cong g
    Erased-cong-↣-∘ ext f g =                                         $⟨ lemma ⟩
      _↔_.to ↣↔∃-Injective (EC₁.Erased-cong (f F.∘ g)) ≡
      _↔_.to ↣↔∃-Injective (EC₂.Erased-cong f F.∘ EC₃.Erased-cong g)  ↝⟨ Eq.≃-≡ (from-isomorphism ↣↔∃-Injective) ⟩□

      EC₁.Erased-cong (f F.∘ g) ≡
      EC₂.Erased-cong f F.∘ EC₃.Erased-cong g                         □
      where
      module BC₁ = E₁.[]-cong₁ ax₁
      module BC₂ = E₁.[]-cong₁ ax₂
      module BC₃ = E₁.[]-cong₁ ax₃

      lemma :
        ( map (_↣_.to f ∘ _↣_.to g)
        , λ {_ _} → _↣_.injective (EC₁.Erased-cong (f F.∘ g))
        )
        ≡
        ( (λ x → [ _↣_.to f (_↣_.to g (erased x)) ])
        , λ {_ _} →
            _↣_.injective (EC₂.Erased-cong f F.∘ EC₃.Erased-cong g)
        )
      lemma =
        cong (_ ,_) $
        implicit-extensionality
          (lower-extensionality ℓ₃ lzero ext) λ _ →
        implicit-extensionality
          (lower-extensionality ℓ₃ lzero ext) λ _ →
        apply-ext (lower-extensionality ℓ₁ ℓ₃ ext) λ eq →
          let eq′ = [ _↣_.injective f (erased (BC₃.[]-cong⁻¹ eq)) ]
          in
          BC₁.[]-cong [ _↣_.injective g (erased eq′) ]                  ≡⟨ cong BC₁.[]-cong $
                                                                           BC₁.[]-cong [ cong (_↣_.injective g ∘ erased) $ sym $
                                                                                _↔_.left-inverse-of BC₂.Erased-≡↔[]≡[] _ ] ⟩∎
          BC₁.[]-cong [ _↣_.injective g
                          (erased (BC₂.[]-cong⁻¹ (BC₂.[]-cong eq′))) ]  ∎

  -- Erased-cong commutes with F._∘_ for all kinds of functions (in
  -- some cases assuming extensionality).

  Erased-cong-∘ :
    {@0 A : Type ℓ₁} {@0 B : Type ℓ₂} {@0 C : Type ℓ₃} →
    Extensionality? k (ℓ₁ ⊔ ℓ₃) (ℓ₁ ⊔ ℓ₃) →
    (@0 f : B ↝[ k ] C) (@0 g : A  ↝[ k ] B) →
    EC₁.Erased-cong (f F.∘ g) ≡ EC₂.Erased-cong f F.∘ EC₃.Erased-cong g
  Erased-cong-∘ {k = implication}         = λ _ f → map-∘ f
  Erased-cong-∘ {k = logical-equivalence} = λ _ → Erased-cong-⇔-∘
  Erased-cong-∘ {k = injection}           = Erased-cong-↣-∘
  Erased-cong-∘ {k = embedding}           = λ ext f g →
                                              Erased-cong-Embedding-∘
                                                ext f g
  Erased-cong-∘ {k = surjection}          = λ ext →
                                              Erased-cong-↠-∘
                                                (lower-extensionality ℓ₁ lzero ext)
  Erased-cong-∘ {k = bijection}           = Erased-cong-↔-∘
  Erased-cong-∘ {k = equivalence}         = Erased-cong-≃-∘
  Erased-cong-∘ {k = equivalenceᴱ}        = λ ext f g →
                                              Erased-cong-≃ᴱ-∘ ext f g

------------------------------------------------------------------------
-- Results that depend on instances of the axiomatisation of []-cong
-- for all universe levels

module []-cong (ax : ∀ {ℓ} → []-cong-axiomatisation ℓ) where

  private
    open module BC₂ {ℓ₁ ℓ₂} = []-cong₂-⊔ (ax {ℓ = ℓ₁}) (ax {ℓ = ℓ₂}) ax
      public
    open module BC₁₃ {ℓ} = []-cong₁₃ (ax {ℓ = ℓ}) ax ax
      public
    open module BC₃ {ℓ₁ ℓ₂ ℓ₃} =
      []-cong₃-⊔ (ax {ℓ = ℓ₁}) (ax {ℓ = ℓ₂}) (ax {ℓ = ℓ₃}) ax ax ax
      public

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
agda --compile Ackermann.agda
./Ackermann

max_issues_repo_name: seanwallawalla-forks/RosettaCodeData

max_forks_repo_name: seanwallawalla-forks/RosettaCodeData


text:
{-# OPTIONS --warning ShadowingInTelescope --allow-unsolved-metas #-}

open import Agda.Primitive

-- warning here
data _~_ {a a : Level} {A : Set a} (a : A) : A -> Set where
  refl : a ~ a

module _ {a} {A : Set a} where

-- nothing: the repetition is in separate telescopes
  data Eq (a : A) : (a : A) → Set where
    refl : Eq a a

-- warning here
f : ∀ (a : Level) → ∀ {A : Set a} A ~ A → Set → Set
f a A ~ B = λ x → x

-- nothing here: the repetition is in separate telescopes
f' : ∀ a → Set a → Set a
f' a = g a where

  g : ∀ a → Set a → Set a
  g a z = z

-- nothing here: the variable {a} is not user-written
h : ∀ {a} → Set a → Set a
h = g _ where

  g : ∀ a → Set a → Set a
  g a z = z

i : (Set → Set → Set) → (∀ _ _ → _)
i f = f

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
open import Proc

module Interp (param : Param) where

import Hear
open import Basics

private
  open module P = Process param
  open module H = Hear param

open Tran

data Result {a : U}(p : Proc a) : Set where
  speak  : forall {w q} -> p -! w !-> q -> Result p
  refuse : Silent p -> Result p

upR : {a b : U}{p : Proc b}(φ : Tran a b) -> Result p -> Result (φ /| p)
upR φ (speak  s) = speak  (tx-/| s)
upR φ (refuse s) = refuse (silent-/| s)

Oracle : Set
Oracle = Nat -> LR

prophecy : Oracle -> LR
prophecy ol = ol zero

nextOracle : Oracle -> Oracle
nextOracle ol = ol % suc

anyOracle : Oracle
anyOracle _ = left

ocons : LR -> Oracle -> Oracle
ocons l or zero    = l
ocons l or (suc n) = or n

step : {a : U}{p : Proc a} -> Guard p -> Oracle -> Result p
step og           _  = refuse silent-o
step (>g _)       _  = refuse silent->
step (w !g p)     _  = speak tx-!
step (w ! p +g f) _  = speak tx-+
step (defg x g)   ol with step g ol
... | refuse s1 = refuse (silent-def s1)
... | speak  s1 = speak (tx-def s1)
step (g1 ||g g2)  ol with step g1 (nextOracle ol)
                        | step g2 (nextOracle ol)
                        | prophecy ol
... | refuse s1 | refuse s2 | _     = refuse (silent-|| s1 s2)
... | speak s1  | refuse s2 | _     = speak (tx-!| s1 (sound g2))
... | refuse s1 | speak s2  | _     = speak (tx-|! (sound g1) s2)
... | speak s1  | speak _   | left  = speak (tx-!| s1 (sound g2))
... | speak _   | speak s2  | right = speak (tx-|! (sound g1) s2)
step (φ /|g g)    ol = upR φ (step g ol)


text:
module Issue481PonderBase where

postulate
  List : Set
  as   : List


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

open import lib.Basics
open import lib.types.Coproduct
open import lib.types.Empty
open import lib.types.Pi

module lib.Relation2 where

module _ {i} {P : Type i} where

  Dec-level : ∀ {n} → has-level (S n) P → has-level (S n) (Dec P)
  Dec-level pP (inl p₁) (inl p₂) =
    equiv-preserves-level (inl=inl-equiv p₁ p₂ ⁻¹) (pP p₁ p₂)
  Dec-level pP (inl p) (inr ¬p) = ⊥-rec $ ¬p p
  Dec-level pP (inr ¬p) (inl p) = ⊥-rec $ ¬p p
  Dec-level {n} pP (inr ¬p₁) (inr ¬p₂) =
    equiv-preserves-level (inr=inr-equiv ¬p₁ ¬p₂ ⁻¹)
      (prop-has-level-S ¬-is-prop ¬p₁ ¬p₂)


text:
module Thesis.SIRelBigStep.IlcSILR where

open import Data.Unit.Base hiding (_≤_)
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Thesis.SIRelBigStep.Lang public
open import Thesis.SIRelBigStep.DLang public

open import Thesis.SIRelBigStep.ArithExtra public

rrelT3-skeleton :
  ∀ {τ Γ} →
  ((v1 : Val τ) → (dv : DVal τ) → (v2 : Val τ) → (k : ℕ) → Set) →
  (t1 : Term Γ τ) (dt : DTerm Γ τ) (t2 : Term Γ τ)
  (ρ1 : ⟦ Γ ⟧Context) (dρ : ChΔ Γ) (ρ2 : ⟦ Γ ⟧Context) →
  ℕ → Set
rrelT3-skeleton {τ} ternary-rel t1 dt t2 ρ1 dρ ρ2 k =
  (v1 v2 : Val τ) →
  ∀ j (j<k : j < k) →
  (ρ1⊢t1↓[j]v1 : ρ1 ⊢ t1 ↓[ i' j ] v1) →
  (ρ2⊢t2↓[n2]v2 : ρ2 ⊢ t2 ↓[ no ] v2) →
  Σ[ dv ∈ DVal τ ]
  ρ1 D dρ ⊢ dt ↓ dv ×
  ternary-rel v1 dv v2 (k ∸ j)

mutual
  rrelT3 : ∀ {τ Γ} (t1 : Term Γ τ) (dt : DTerm Γ τ) (t2 : Term Γ τ) (ρ1 : ⟦ Γ ⟧Context) (dρ : ChΔ Γ) (ρ2 : ⟦ Γ ⟧Context) → ℕ → Set
  rrelT3 {τ} = rrelT3-skeleton (rrelV3 τ)

  rrelV3 : ∀ τ (v1 : Val τ) (dv : DVal τ) (v2 : Val τ) → (n : ℕ) → Set
  -- Making this case first ensures rrelV3 splits on its second argument, hence
  -- that all its equations hold definitionally.
  rrelV3 τ v1 (bang v2) v2' n = v2 ≡ v2'
  rrelV3 nat (natV v1) (dnatV dv) (natV v2) n = dv + v1 ≡ v2
  rrelV3 (σ ⇒ τ) (closure {Γ1} t1 ρ1) (dclosure {ΔΓ} dt ρ dρ) (closure {Γ2} t2 ρ2) n =
      Σ ((Γ1 ≡ Γ2) × (Γ1 ≡ ΔΓ)) λ { (refl , refl) →
        ρ1 ≡ ρ ×
        ρ1 ⊕ρ dρ ≡ ρ2 ×
        t1 ≡ t2 ×
        dt ≡ derive-dterm t1 ×
        ∀ (k : ℕ) (k<n : k < n) v1 dv v2 →
        rrelV3 σ v1 dv v2 k →
        rrelT3
          t1
          dt
          t2
          (v1 • ρ1)
          (dv • dρ)
          (v2 • ρ2)
          k
      }
  rrelV3 (pair τ1 τ2) (pairV va1 vb1) (dpairV dva dvb) (pairV va2 vb2) n =
    rrelV3 τ1 va1 dva va2 n × rrelV3 τ2 vb1 dvb vb2 n

rrelV3→⊕ : ∀ {τ n} v1 dv v2 → rrelV3 τ v1 dv v2 n → v1 ⊕ dv ≡ v2
rrelV3→⊕ v1 (bang v2) v2' vv = vv
rrelV3→⊕ (closure {Γ} t ρ) (dclosure .(derive-dterm t) .ρ dρ) (closure .t .(ρ ⊕ρ dρ)) ((refl , refl) , refl , refl , refl , refl , dvv) with Γ ≟Ctx Γ | ≟Ctx-refl Γ
... | .(yes refl) | refl = refl
rrelV3→⊕ (natV n) (dnatV dn) (natV .(dn + n)) refl rewrite +-comm n dn = refl
rrelV3→⊕ (pairV va1 vb1) (dpairV dva dvb) (pairV va2 vb2) (vaa , vbb) rewrite rrelV3→⊕  va1 dva va2 vaa | rrelV3→⊕ vb1 dvb vb2 vbb = refl

rrelρ3 : ∀ Γ (ρ1 : ⟦ Γ ⟧Context) (dρ : ChΔ Γ) (ρ2 : ⟦ Γ ⟧Context) → ℕ → Set
rrelρ3 ∅ ∅ ∅ ∅ n = ⊤
rrelρ3 (τ • Γ) (v1 • ρ1) (dv • dρ) (v2 • ρ2) n = rrelV3 τ v1 dv v2 n × rrelρ3 Γ ρ1 dρ ρ2 n

rrelρ3→⊕ : ∀ {Γ n} ρ1 dρ ρ2 → rrelρ3 Γ ρ1 dρ ρ2 n → ρ1 ⊕ρ dρ ≡ ρ2
rrelρ3→⊕ ∅ ∅ ∅ tt = refl
rrelρ3→⊕ (v1 • ρ1) (dv • dρ) (v2 • ρ2) (vv , ρρ) rewrite rrelV3→⊕ v1 dv v2 vv | rrelρ3→⊕ ρ1 dρ ρ2 ρρ = refl

rrelV3-mono : ∀ m n → m ≤ n → ∀ τ v1 dv v2 → rrelV3 τ v1 dv v2 n → rrelV3 τ v1 dv v2 m
rrelV3-mono m n m≤n τ v1 (bang v2) v2′ vv = vv
rrelV3-mono m n m≤n (σ ⇒ τ) (closure t ρ) (dclosure dt ρ₁ dρ) (closure t₁ ρ₂)
  -- Validity
  ((refl , refl) , refl , refl , refl , refl , vv) =
  (refl  , refl) , refl , refl , refl , refl , λ k k<m → vv k (≤-trans k<m m≤n)
rrelV3-mono m n m≤n nat (natV n₁) (dnatV n₂) (natV n₃) vv = vv
rrelV3-mono m n m≤n (pair τ1 τ2) (pairV va1 vb1) (dpairV dva dvb) (pairV va2 vb2) (vaa , vbb) =
  rrelV3-mono m n m≤n τ1 va1 dva va2 vaa , rrelV3-mono m n m≤n τ2 vb1 dvb vb2 vbb

rrelρ3-mono : ∀ m n → m ≤ n → ∀ Γ ρ1 dρ ρ2 → rrelρ3 Γ ρ1 dρ ρ2 n → rrelρ3 Γ ρ1 dρ ρ2 m
rrelρ3-mono m n m≤n ∅ ∅ ∅ ∅ tt = tt
rrelρ3-mono m n m≤n (τ • Γ) (v1 • ρ1) (dv • dρ) (v2 • ρ2) (vv , ρρ) = rrelV3-mono m n m≤n _ v1 dv v2 vv , rrelρ3-mono m n m≤n Γ ρ1 dρ ρ2 ρρ

⟦_⟧RelVar3 : ∀ {Γ τ n} (x : Var Γ τ) {ρ1 dρ ρ2} →
  rrelρ3 Γ ρ1 dρ ρ2 n →
  rrelV3 τ (⟦ x ⟧Var ρ1) (D.⟦ x ⟧Var dρ) (⟦ x ⟧Var ρ2) n
⟦ this ⟧RelVar3   {v1 • ρ1} {dv • dρ} {v2 • ρ2} (vv , ρρ) = vv
⟦ that x ⟧RelVar3 {v1 • ρ1} {dv • dρ} {v2 • ρ2} (vv , ρρ) = ⟦ x ⟧RelVar3 ρρ

-- Direct analogue of rrelV3→⊕ for rrelT3: simply say that the resulting values
-- are related.
-- Alternatively, one could try internalizing ⊕ and giving some term equivalence, but it does not seem worthwhile.
rrelT3→⊕ : ∀ {τ Γ k}
  (t1 : Term Γ τ) (dt : DTerm Γ τ) (t2 : Term Γ τ) (ρ1 : ⟦ Γ ⟧Context) (dρ : ChΔ Γ) (ρ2 : ⟦ Γ ⟧Context) →
  rrelT3 {τ} t1 dt t2 ρ1 dρ ρ2 k →
  rrelT3-skeleton (λ v1 dv v2 _ → v1 ⊕ dv ≡ v2) t1 dt t2 ρ1 dρ ρ2 k
rrelT3→⊕ t1 dt t2 ρ1 dρ ρ2 ttrel v1 v2 j j<k ρ1⊢t1↓[j]v1 ρ2⊢t2↓[n2]v2 with ttrel v1 v2 j j<k ρ1⊢t1↓[j]v1 ρ2⊢t2↓[n2]v2
... | dv , ↓dv , vv = dv , ↓dv , rrelV3→⊕ v1 dv v2 vv