text:
open import Relation.Binary.Core

module Bound.Lower.Order.Properties {A : Set}
                 (_≤_ : A → A → Set)
                 (trans≤ : Transitive _≤_)  where

open import Bound.Lower A
open import Bound.Lower.Order _≤_

transLeB : {a b c : Bound} → LeB a b → LeB b c → LeB a c
transLeB lebx _ = lebx
transLeB (lexy x≤y) (lexy y≤z) = lexy (trans≤ x≤y y≤z)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------------
-- The program to sort a list is correct
------------------------------------------------------------------------------

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

-- This module prove the correctness of a program which sorts a list
-- by converting it into an ordered tree and then back to a list
-- (Burstall 1969, p. 45).

module FOTC.Program.SortList.CorrectnessProofI where

open import FOTC.Base
open import FOTC.Data.Nat.List.Type
open import FOTC.Program.SortList.PropertiesI
open import FOTC.Program.SortList.Properties.Totality.TreeI
open import FOTC.Program.SortList.SortList

------------------------------------------------------------------------------
-- Main theorem: The sort program generates an ordered list.
sortCorrect : ∀ {is} → ListN is → OrdList (sort is)
sortCorrect {is} Lis =
  subst OrdList
        refl
        (flatten-OrdList (makeTree-Tree Lis) (makeTree-OrdTree Lis))

------------------------------------------------------------------------------
-- References
--
-- Burstall, R. M. (1969). Proving properties of programs by
-- structural induction. The Computer Journal 12.1, pp. 41–48.

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module plfa.working.Naturals where

    data ℕ : Set where
      zero : ℕ
      suc : ℕ → ℕ

    seven : ℕ
    seven = suc(suc(suc(suc(suc(suc(suc(zero)))))))

    {-# BUILTIN NATURAL ℕ #-}

    import Relation.Binary.PropositionalEquality as Eq
    open Eq using (_≡_; refl)
    open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

    _+_ : ℕ → ℕ → ℕ
    zero + n = n
    (suc m) + n = suc(m + n)

    _ : 2 + 3 ≡ 5
    _ =
      begin
        2 + 3
      ≡⟨⟩
        (suc (suc zero)) + (suc (suc (suc zero)))
      ≡⟨⟩
        suc( (suc zero) + (suc (suc (suc zero))))
      ≡⟨⟩
        (suc(suc (zero + (suc (suc (suc zero))))))
      ≡⟨⟩
        (suc (suc (suc (suc (suc zero)))))
      ≡⟨⟩
        5
      ∎

    _ : 2 + 3 ≡ 5
    _ =
      begin
        2 + 3
      ≡⟨⟩
        suc (1 + 3)
      ≡⟨⟩
        suc (suc (0 + 3))
      ≡⟨⟩
        suc (suc 3)
      ≡⟨⟩
        5
      ∎

    _ : 3 + 4 ≡ 7
    _ =
      begin
        3 + 4
      ≡⟨⟩
        suc (2 + 4)
      ≡⟨⟩
        suc (2 + (suc 3))
      ≡⟨⟩
        suc (suc (2 + 3))
      ≡⟨⟩
        suc (suc  5)
      ≡⟨⟩
        7
      ∎

    _*_ : ℕ → ℕ → ℕ
    zero * n = zero
    (suc m) * n = n + (n * m)

    _ : 3 * 4 ≡ 12
    _ =
      begin
        3 * 4
      ≡⟨⟩
        (suc 2) * 4
      ≡⟨⟩
        4 + (4 * 2)
      ≡⟨⟩
        4 + ((suc 3) * 2)
      ≡⟨⟩
        4 + (2 + (2 * 3))
      ≡⟨⟩
        4 + (2 + (suc 1 * 3))
      ≡⟨⟩
        4 + (2 + (3 + (3 * 1)))
      ≡⟨⟩
        4 + (2 + (3 + (suc 2 * 1)))
      ≡⟨⟩
        4 + (2 + (3 + (1 + (1 * 2))))
      ≡⟨⟩
        12
      ∎

    _^_ : ℕ → ℕ → ℕ
    n ^ zero = suc zero
    n ^ (suc m) = n * (n ^ m)

    _ : 3 ^ 4 ≡ 81
    _ =
      begin
        3 ^ 4
      ≡⟨⟩
        3 ^ (1 + 3)
      ≡⟨⟩
        3 * (3 ^ 3)
      ≡⟨⟩
        3 * (3 * (3 ^ 2))
      ≡⟨⟩
        3 * (3 * (3 * (3 ^ 1)))
      ≡⟨⟩
        3 * (3 * (3 * 3))
      ≡⟨⟩
        81
      ∎

    _∸_ : ℕ → ℕ → ℕ
    m ∸ zero = m
    zero ∸ suc n = zero
    suc m ∸ suc n = m ∸ n

    _ : 5 ∸ 3 ≡ 2
    _ =
      begin
        5 ∸ 3
      ≡⟨⟩
        (1 + 4) ∸ (1 + 2)
      ≡⟨⟩
        4 ∸ 2
      ≡⟨⟩
        3 ∸ 1
      ≡⟨⟩
        2 ∸ 0
      ≡⟨⟩
        2
      ∎

    _ : 2 ∸ 5 ≡ 0
    _ =
      begin
        2 ∸ 5
      ≡⟨⟩
        1 ∸ 4
      ≡⟨⟩
        0 ∸ 3
      ≡⟨⟩
        0
      ∎

    data Bin : Set where
      ⟨⟩ : Bin
      _O : Bin → Bin
      _I : Bin → Bin

    inc : Bin → Bin
    inc ⟨⟩ = ⟨⟩ I
    inc (p O) = p I
    inc (p I) = (inc p) O

    _ : inc (⟨⟩ O O O O) ≡ ⟨⟩ O O O I
    _ = refl

    _ : inc (⟨⟩ O O O I) ≡ ⟨⟩ O O I O
    _ = refl

    _ : inc (⟨⟩ O O I O) ≡ ⟨⟩ O O I I
    _ = refl

    _ : inc (⟨⟩ O O I I) ≡ ⟨⟩ O I O O
    _ = refl

    _ : inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O
    _ = refl

    to : ℕ → Bin
    to zero = ⟨⟩ O
    to (suc n) = inc (to n)

    from : Bin → ℕ
    from ⟨⟩ = zero
    from (p O) = from p * 2
    from (p I) = suc ((from p) * 2)

    _ : to 3 ≡ ⟨⟩ I I
    _ = refl

    _ : from (⟨⟩ I I) ≡ 3
    _ = refl


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

module Categories.Category.Construction.Graphs where

-- The "Underlying Graph" <-> "Free Category on a Graph" Adjunction.
-- Lots of surprises here, of various level of surprisingness
-- 1. The Free Category rises universe levels of arrows (and equivalences); the Underlying Graph does not
--   (due to the Transitive Closure "Star" construction)
-- 2. As a consequence of (1), the eventual Adjunction will be for all Levels being the same
-- 3. If you want a Functor Categories Graph, then the object/hom levels are straightforward,
--   but if you use "Categories" with NaturalIsomorphism, then the 2-point Groupoid is contractible
--   (thus equivalent to the 1-point Category), and yet those two Graphs shouldn't be considered to
--   be the same!  So _≡F_ must be used so that we have no wiggle room when mapping Graphs around.
--   Interestingly, this only shows up when trying to prove that the Underlying Functor respects
--   _≈_, which is not traditionally a requirement of a Functor! This requirement is usually left
--   implicit.  If we were to allow Functor to not respect _≈_, things would be fine. But of course
--   we couldn't do any reasonable equational reasoning anymore.  Of course, if _≈_ were the global
--   _≡_, this isn't an issue, but that is definitely not wanted here.
-- 4. A lot of weird little lemmas about _≡_ and subst/transport are needed, because we're in a mixed
--   reasoning situation with both ≡ and ≈ present.  These could probably be generalized and factored
--   into a separate module (or into the standard library).

open import Level
open import Function using (_$_; flip) renaming (id to idFun; _∘_ to _⊚_)
open import Relation.Binary hiding (_⇒_)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
import Relation.Binary.EqReasoning as EqR
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties hiding (trans)
open import Data.Product using (proj₁; proj₂; _,_)

open import Categories.Category
open import Categories.Functor using (Functor)
open import Categories.Functor.Equivalence
open import Categories.Category.Instance.StrictCats
open import Categories.Utils.EqReasoning
open import Categories.NaturalTransformation hiding (id)
open import Categories.NaturalTransformation.NaturalIsomorphism hiding (refl; sym; trans; isEquivalence)
open import Categories.Adjoint
import Categories.Morphism.HeterogeneousIdentity as HId

-- a graph has vertices Obj and edges _⇒_, where edges form a setoid over _≈_.
record Graph o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  infix 4 _≈_ _⇒_

  field
    Obj   : Set o
    _⇒_   : Rel Obj ℓ
    _≈_   : ∀ {A B} → Rel (A ⇒ B) e
    equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B})

  setoid : {A B : Obj} → Setoid _ _
  setoid {A} {B} = record
    { Carrier       = A ⇒ B
    ; _≈_           = _≈_
    ; isEquivalence = equiv
    }

  module Equiv {A} {B} = IsEquivalence (equiv {A} {B})
  module EdgeReasoning {A B : Obj} = EqR (setoid {A} {B})

private
  variable
    o o′ ℓ ℓ′ e e′ : Level

-- This doesn't belong here... but will do for now
module PathEquiv {o ℓ e : Level} {Obj : Set o} {_⇒_ : Obj → Obj → Set ℓ} (_≈_ : {A B : Obj} → Rel (A ⇒ B) e)
  (equiv : {A B : Obj} → IsEquivalence ( _≈_ {A} {B})) where

  private
    module E {A} {B} = IsEquivalence (equiv {A} {B})

  open E renaming (refl to ≈refl; sym to ≈sym; trans to ≈trans)

  infix 4 _≈*_
  data _≈*_ : {A B : Obj} (p q : Star _⇒_ A B) → Set (o ⊔ ℓ ⊔ e) where
      ε : {A : Obj} → _≈*_ {A} ε ε
      _◅_ : {A B C : Obj} {x y : A ⇒ B} {p q : Star _⇒_ B C} (x≈y : x ≈ y) (p≈q : p ≈* q) → x ◅ p ≈* y ◅ q

  refl : {A B : Obj} {p : Star _⇒_ A B} → p ≈* p
  refl {p = ε} = ε
  refl {p = x ◅ p} = ≈refl ◅ refl

  sym : {A B : Obj} {p q : Star _⇒_ A B} → p ≈* q → q ≈* p
  sym ε = ε
  sym (x≈y ◅ eq) = ≈sym x≈y ◅ sym eq

  ≡⇒≈* : {A B : Obj} {p q : Star _⇒_ A B} → p ≡ q → p ≈* q
  ≡⇒≈* ≡.refl = refl

  ≡⇒≈ : {A B : Obj} → {p q : A ⇒ B} → p ≡ q → p ≈ q
  ≡⇒≈ ≡.refl = ≈refl

  trans : {A B : Obj} {p q r : Star _⇒_ A B} → p ≈* q → q ≈* r → p ≈* r
  trans ε ε = ε
  trans (x≈y ◅ ss) (y≈z ◅ tt) = ≈trans x≈y y≈z ◅ trans ss tt

  isEquivalence : {A B : Obj} → IsEquivalence (λ (p q : Star _⇒_ A B) → p ≈* q)
  isEquivalence = record { refl = refl ; sym = sym ; trans = trans }

  setoid : Obj → Obj → Setoid (o ⊔ ℓ) (o ⊔ ℓ ⊔ e)
  setoid A B = record { _≈_ = _≈*_ ; isEquivalence = isEquivalence {A} {B} }

  -- convenient to define here
  --
  -- FIXME: this should go into the standard library at
  -- Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
  ◅◅-identityʳ : {A B : Obj} → (f : Star _⇒_ A B) → f ◅◅ ε ≈* f
  ◅◅-identityʳ ε = ε
  ◅◅-identityʳ (x ◅ f) = ≈refl ◅ ◅◅-identityʳ f

  module PathEqualityReasoning {A B} where
    open EqR (setoid A B) public

module _ (G : Graph o ℓ e) where
  open Graph G
  private module P = PathEquiv {o} {ℓ} {e} {Obj} {_⇒_} _≈_ equiv
  open P

  Free : Category o (o ⊔ ℓ) (o ⊔ ℓ ⊔ e)
  Free = record
    { Obj       = Obj
    ; _⇒_       = Star _⇒_
    ; _≈_       = _≈*_
    ; id        = ε
    ; _∘_       = _▻▻_
    ; assoc     = λ {_ _ _ _} {f g h} → sym $ ≡⇒≈* $ ◅◅-assoc f g h
    ; sym-assoc = λ {_ _ _ _} {f g h} → ≡⇒≈* $ ◅◅-assoc f g h
    ; identityˡ = λ {_ _ f} → ◅◅-identityʳ f
    ; identityʳ = refl
    ; identity² = refl
    ; equiv     = isEquivalence
    ; ∘-resp-≈  = resp
    }
    where resp : ∀ {A B C} {f h : Star _⇒_ B C} {g i : Star _⇒_ A B} →
                   f ≈* h → g ≈* i → (f ▻▻ g) ≈* (h ▻▻ i)
          resp eq ε = eq
          resp eq (eq₁ ◅ eq₂) = eq₁ ◅ (resp eq eq₂)

  open P public renaming (_≈*_ to [_]_≈*_)

record GraphMorphism (G : Graph o ℓ e) (G′ : Graph o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private
    module G  = Graph G
    module G′ = Graph G′

  field
    M₀       : G.Obj → G′.Obj
    M₁       : ∀ {A B} → A G.⇒ B → M₀ A G′.⇒ M₀ B
    M-resp-≈ : ∀ {A B} {f g : A G.⇒ B} → f G.≈ g → M₁ f G′.≈ M₁ g

idGHom : {G : Graph o ℓ e} → GraphMorphism G G
idGHom = record { M₀ = idFun ; M₁ = idFun ; M-resp-≈ = idFun }

_∘GM_ : {G₁ G₂ G₃ : Graph o ℓ e} (m₁ : GraphMorphism G₂ G₃) (m₂ : GraphMorphism G₁ G₂) → GraphMorphism G₁ G₃
m₁ ∘GM m₂ = record
  { M₀ = M₀ m₁ ⊚ M₀ m₂
  ; M₁ = M₁ m₁ ⊚ M₁ m₂
  ; M-resp-≈ = M-resp-≈ m₁ ⊚ M-resp-≈ m₂
  }
  where open GraphMorphism

module Trsp (G : Graph o ℓ e) where
  open Graph G

  -- Two shorthands that will be useful for the definition of morphism
  -- equality: transport the domain or codomain of an edge along an
  -- equality.

  infixr 9 _◂_
  infixl 9 _▸_

  _◂_ : ∀ {A B C} → A ≡ B → B ⇒ C → A ⇒ C
  p ◂ f = ≡.subst (_⇒ _) (≡.sym p) f

  _▸_ : ∀ {A B C} → A ⇒ B → B ≡ C → A ⇒ C
  f ▸ p = ≡.subst (_ ⇒_) p f

  -- Some simple properties of transports

  ◂-▸-comm : ∀ {A B C D} (p : A ≡ B) (f : B ⇒ C) (q : C ≡ D) →
             p ◂ (f ▸ q) ≡ (p ◂ f) ▸ q
  ◂-▸-comm ≡.refl f ≡.refl = ≡.refl

  ◂-trans : ∀ {A B C D} (p : A ≡ B) (q : B ≡ C) (f : C ⇒ D) →
            p ◂ q ◂ f ≡ (≡.trans p q) ◂ f
  ◂-trans ≡.refl ≡.refl f = ≡.refl

  ▸-trans : ∀ {A B C D} (f : A ⇒ B) (p : B ≡ C) (q : C ≡ D) →
            f ▸ p ▸ q ≡ f ▸ ≡.trans p q
  ▸-trans f ≡.refl ≡.refl = ≡.refl

  ◂-resp-≈ : ∀ {A B C} (p : A ≡ B) {f g : B ⇒ C} → f ≈ g → p ◂ f ≈ p ◂ g
  ◂-resp-≈ ≡.refl f≈g = f≈g

  ▸-resp-≈ : ∀ {A B C} {f g : A ⇒ B} → f ≈ g → (p : B ≡ C) → f ▸ p ≈ g ▸ p
  ▸-resp-≈ f≈g ≡.refl = f≈g

module TrspGM {G : Graph o ℓ e} {H : Graph o′ ℓ′ e′}
              (m : GraphMorphism G H) where
  module G = Graph G
  module H = Graph H
  open GraphMorphism m
  open Trsp G
  open Trsp H using () renaming (_◂_ to _◃_; _▸_ to _▹_)

  M-resp-▸ : ∀ {A B C} (f : A G.⇒ B) (p : B ≡ C) →
             M₁ (f ▸ p) ≡ M₁ f ▹ ≡.cong M₀ p
  M-resp-▸ f ≡.refl = ≡.refl

  M-resp-◂ : ∀ {A B C} (p : A ≡ B) (f : B G.⇒ C) →
             M₁ (p ◂ f) ≡ ≡.cong M₀ p ◃ M₁ f
  M-resp-◂ ≡.refl f = ≡.refl

record GraphMorphism≈ {G : Graph o ℓ e} {G′ : Graph o′ ℓ′ e′}
                      (M M′ : GraphMorphism G G′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private
    module G  = Graph G
    module G′ = Graph G′
    module M  = GraphMorphism M
    module M′ = GraphMorphism M′
  open Trsp G′

  -- Pick a presentation of equivalence for graph morphisms that works
  -- well with functor equality.

  field
    M₀≡ : ∀ {X} → M.M₀ X ≡ M′.M₀ X
    M₁≡ : ∀ {A B} {f : A G.⇒ B} → M.M₁ f ▸ M₀≡ G′.≈ M₀≡ ◂ M′.M₁ f

Graphs : ∀ o ℓ e → Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
Graphs o ℓ e = record
  { Obj       = Graph o ℓ e
  ; _⇒_       = GraphMorphism
  ; _≈_       = GraphMorphism≈
  ; id        = idGHom
  ; _∘_       = _∘GM_
  ; assoc     = λ {_ _ _ G} → record { M₀≡ = ≡.refl ; M₁≡ = Equiv.refl G }
  ; sym-assoc = λ {_ _ _ G} → record { M₀≡ = ≡.refl ; M₁≡ = Equiv.refl G }
  ; identityˡ = λ {_ G}     → record { M₀≡ = ≡.refl ; M₁≡ = Equiv.refl G }
  ; identityʳ = λ {_ G}     → record { M₀≡ = ≡.refl ; M₁≡ = Equiv.refl G }
  ; identity² = λ {G}       → record { M₀≡ = ≡.refl ; M₁≡ = Equiv.refl G }
  ; equiv     = λ {_ G} → record
    { refl  = record { M₀≡ = ≡.refl ; M₁≡ = Equiv.refl G }
    ; sym   = λ {i j} eq → record
      { M₀≡ = ≡.sym (M₀≡ eq)
      ; M₁≡ = λ {_ _ f} →
        let open EdgeReasoning G
            open Trsp G
        in begin
          M₁ j f ▸ ≡.sym (M₀≡ eq)
        ≡˘⟨ ≡.cong (_◂ (M₁ j f ▸ _)) (≡.trans-symˡ (M₀≡ eq)) ⟩
          ≡.trans (≡.sym $ M₀≡ eq) (M₀≡ eq) ◂ (M₁ j f ▸ ≡.sym (M₀≡ eq))
        ≡˘⟨ ◂-trans (≡.sym $ M₀≡ eq) (M₀≡ eq) _ ⟩
          ≡.sym (M₀≡ eq) ◂ M₀≡ eq ◂ (M₁ j f ▸ ≡.sym (M₀≡ eq))
        ≡⟨ ≡.cong (≡.sym (M₀≡ eq) ◂_)
                  (◂-▸-comm (M₀≡ eq) (M₁ j f) (≡.sym $ M₀≡ eq)) ⟩
          ≡.sym (M₀≡ eq) ◂ ((M₀≡ eq ◂ M₁ j f) ▸ ≡.sym (M₀≡ eq))
        ≈˘⟨ ◂-resp-≈ (≡.sym (M₀≡ eq)) (▸-resp-≈ (M₁≡ eq) (≡.sym (M₀≡ eq))) ⟩
          ≡.sym (M₀≡ eq) ◂ (M₁ i f ▸ M₀≡ eq ▸ ≡.sym (M₀≡ eq))
        ≡⟨ ≡.cong (≡.sym (M₀≡ eq) ◂_)
                  (▸-trans (M₁ i f) (M₀≡ eq) (≡.sym (M₀≡ eq))) ⟩
          ≡.sym (M₀≡ eq) ◂ (M₁ i f ▸ ≡.trans (M₀≡ eq) (≡.sym (M₀≡ eq)))
        ≡⟨ ≡.cong (λ p → ≡.sym (M₀≡ eq) ◂ (M₁ i f ▸ p)) (≡.trans-symʳ (M₀≡ eq)) ⟩
          ≡.sym (M₀≡ eq) ◂ M₁ i f
        ∎
      }
    ; trans = λ {i j k} eq eq′ → record
      { M₀≡ = ≡.trans (M₀≡ eq) (M₀≡ eq′)
      ; M₁≡ = λ {_ _ f} →
        let open EdgeReasoning G
            open Trsp G
        in begin
          M₁ i f ▸ ≡.trans (M₀≡ eq) (M₀≡ eq′)
        ≡˘⟨ ▸-trans (M₁ i f) (M₀≡ eq) (M₀≡ eq′) ⟩
          (M₁ i f ▸ M₀≡ eq) ▸ M₀≡ eq′
        ≈⟨ ▸-resp-≈ (M₁≡ eq) (M₀≡ eq′) ⟩
          (M₀≡ eq ◂ M₁ j f) ▸ M₀≡ eq′
        ≡˘⟨ ◂-▸-comm (M₀≡ eq) (M₁ j f) (M₀≡ eq′) ⟩
          M₀≡ eq ◂ (M₁ j f ▸ M₀≡ eq′)
        ≈⟨ ◂-resp-≈ (M₀≡ eq) (M₁≡ eq′) ⟩
          M₀≡ eq ◂ (M₀≡ eq′ ◂ M₁ k f)
        ≡⟨ ◂-trans (M₀≡ eq) (M₀≡ eq′) (M₁ k f) ⟩
          ≡.trans (M₀≡ eq) (M₀≡ eq′) ◂ M₁ k f
        ∎
      }
    }
  ; ∘-resp-≈  = λ {_ G H} {f g h i} eq eq′ → record
    { M₀≡ = ≡.trans (≡.cong (M₀ f) (M₀≡ eq′)) (M₀≡ eq)
    ; M₁≡ = λ {_ _ j} →
      let open EdgeReasoning H
          open Trsp H
          open Trsp G using () renaming (_▸_ to _▹_; _◂_ to _◃_)
          open TrspGM
      in begin
        M₁ (f ∘GM h) j ▸ ≡.trans (≡.cong (M₀ f) (M₀≡ eq′)) (M₀≡ eq)
      ≡˘⟨ ▸-trans (M₁ f (M₁ h j)) (≡.cong (M₀ f) (M₀≡ eq′)) (M₀≡ eq) ⟩
        M₁ f (M₁ h j) ▸ ≡.cong (M₀ f) (M₀≡ eq′) ▸ M₀≡ eq
      ≡˘⟨ ≡.cong (_▸ M₀≡ eq) (M-resp-▸ f (M₁ h j) (M₀≡ eq′)) ⟩
        M₁ f (M₁ h j ▹ M₀≡ eq′) ▸ M₀≡ eq
      ≈⟨ M₁≡ eq ⟩
        M₀≡ eq ◂ M₁ g (M₁ h j ▹ M₀≡ eq′)
      ≈⟨ ◂-resp-≈ (M₀≡ eq) (M-resp-≈ g (M₁≡ eq′)) ⟩
        M₀≡ eq ◂ M₁ g (M₀≡ eq′ ◃ M₁ i j)
      ≡⟨ ≡.cong (M₀≡ eq ◂_) (M-resp-◂ g (M₀≡ eq′) (M₁ i j)) ⟩
        M₀≡ eq ◂ ≡.cong (M₀ g) (M₀≡ eq′) ◂ M₁ g (M₁ i j)
      ≡⟨ ◂-trans (M₀≡ eq) (≡.cong (M₀ g) (M₀≡ eq′)) (M₁ g (M₁ i j)) ⟩
        ≡.trans (M₀≡ eq) (≡.cong (M₀ g) (M₀≡ eq′)) ◂ M₁ g (M₁ i j)
      ≡˘⟨ ≡.cong (_◂ M₁ g (M₁ i j)) (≡.naturality (λ _ → M₀≡ eq)) ⟩
        ≡.trans (≡.cong (M₀ f) (M₀≡ eq′)) (M₀≡ eq) ◂ M₁ g (M₁ i j)
      ∎
    }
  }
  where
    open Graph
    open GraphMorphism
    open GraphMorphism≈

open _≡F_

-- Put the rest of the Graph stuff here too:
Underlying₀ : Category o ℓ e → Graph o ℓ e
Underlying₀ C = record { Obj = C.Obj ; _⇒_ = C._⇒_ ; _≈_ = C._≈_ ; equiv = C.equiv }
  where module C = Category C

Underlying₁ : {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → Functor C D → GraphMorphism (Underlying₀ C) (Underlying₀ D)
Underlying₁ F = record { M₀ = F.F₀ ; M₁ = F.F₁ ; M-resp-≈ = F.F-resp-≈ }
  where module F = Functor F

Underlying : Functor (Cats o ℓ e) (Graphs o ℓ e)
Underlying = record
  { F₀ = Underlying₀
  ; F₁ = Underlying₁
  ; identity = λ {A} → record { M₀≡ = ≡.refl ; M₁≡ = Category.Equiv.refl A }
  ; homomorphism = λ where {Z = Z} → record { M₀≡ = ≡.refl ; M₁≡ = Category.Equiv.refl Z }
  ; F-resp-≈ = λ {A} {B} {F} {G} F≈G → record
    { M₀≡ = λ {X} → eq₀ F≈G X
    ; M₁≡ = λ {x} {y} {f} →
      let open Category B
          open HId B
          open Trsp (Underlying₀ B)
          open Functor
          open Graph.EdgeReasoning (Underlying₀ B)
      in begin
        F₁ F f ▸ eq₀ F≈G y         ≈⟨ hid-subst-cod (F₁ F f) (eq₀ F≈G y) ⟩
        hid (eq₀ F≈G y) ∘ F₁ F f   ≈⟨ eq₁ F≈G f ⟩
        F₁ G f ∘ hid (eq₀ F≈G x)   ≈˘⟨ hid-subst-dom (eq₀ F≈G x) (F₁ G f) ⟩
        eq₀ F≈G x ◂ F₁ G f         ∎
    }
  }
  where
  open NaturalTransformation
  open NaturalIsomorphism

-- Transports on paths

module TrspStar (G : Graph o ℓ e) where
  open Graph G
  open Trsp (Underlying₀ (Free G)) public using () renaming
    ( _◂_ to _◂*_
    ; _▸_ to _▸*_
    )
  open Trsp G

  -- Lemmas relating transports to path operations.

  ◂*-▸*-ε : ∀ {A B : Obj} (p : A ≡ B) → ε ▸* p ≡ p ◂* ε
  ◂*-▸*-ε ≡.refl = ≡.refl

  ◂*-◅ : ∀ {A B C D : Obj} (p : A ≡ B) (f : B ⇒ C) (fs : Star _⇒_ C D) →
         p ◂* (f ◅ fs) ≡ (p ◂ f) ◅ fs
  ◂*-◅ ≡.refl f fs = ≡.refl

  ◅-▸* : ∀ {A B C D : Obj} (f : A ⇒ B) (fs : Star _⇒_ B C) (p : C ≡ D) →
         (f ◅ fs) ▸* p ≡ f ◅ (fs ▸* p)
  ◅-▸* f fs ≡.refl = ≡.refl

  ◅-◂*-▸ : ∀ {A B C D : Obj} (f : A ⇒ B) (p : B ≡ C) (fs : Star _⇒_ C D) →
           _≡_ {_} {Star _⇒_ A D} (f ◅ (p ◂* fs)) ((f ▸ p) ◅ fs)
  ◅-◂*-▸ f ≡.refl fs = ≡.refl

-- define these ahead of time
module _ {G₁ G₂ : Graph o ℓ e} (G⇒ : GraphMorphism G₁ G₂) where
  open Graph G₁ renaming (_⇒_ to _⇒₁_; Obj to Obj₁)
  open Graph G₂ renaming (_⇒_ to _⇒₂_; Obj to Obj₂; module Equiv to Equiv₂)
  open GraphMorphism G⇒

  mapGraph : {A B : Obj₁} → Star _⇒₁_ A B → Star _⇒₂_ (M₀ A) (M₀ B)
  mapGraph ε = ε
  mapGraph (x ◅ y) = M₁ x ◅ mapGraph y

  map-hom : {X Y Z : Graph.Obj G₁} (f : Star _⇒₁_ X Y) {g : Star _⇒₁_ Y Z} →
      [ G₂ ] mapGraph (f ◅◅ g) ≈* (mapGraph f ◅◅ mapGraph g)
  map-hom ε {g} = refl G₂
  map-hom (x ◅ f) {g} = Equiv₂.refl ◅ map-hom f

  map-resp : {A B : Obj₁} (f : Star _⇒₁_ A B) {g : Star _⇒₁_ A B} →
      [ G₁ ] f ≈* g → [ G₂ ] mapGraph f ≈* mapGraph g
  map-resp ε ε = ε
  map-resp (x ◅ f) (f≈* ◅ eq) = M-resp-≈ f≈* ◅ map-resp f eq

-- don't want a single global GraphMorphism
module _ {G : Graph o ℓ e} where
  open Graph G

  map-id : {A B : Obj} (f : Star _⇒_ A B) → [ G ] mapGraph (idGHom {G = G}) f ≈* f
  map-id ε        = ε
  map-id (fs ◅ f) = Equiv.refl ◅ map-id f

module _ {X Y Z : Graph o ℓ e} {G₁ : GraphMorphism X Y} {G₂ : GraphMorphism Y Z} where
  open Graph X

  map-∘ : {A B : Obj} (f : Star _⇒_ A B) → [ Z ] (mapGraph (G₂ ∘GM G₁) f) ≈* mapGraph G₂ (mapGraph G₁ f)
  map-∘ ε        = ε
  map-∘ (fs ◅ f) = Graph.Equiv.refl Z ◅ map-∘ f

module _ {G H : Graph o ℓ e} {f g : GraphMorphism G H}
         (f≈g : GraphMorphism≈ f g) where
  open Graph G
  open GraphMorphism
  open GraphMorphism≈ f≈g
  open TrspStar H
  open Trsp H

  map-M₁≡ : {A B : Obj} (hs : Star _⇒_ A B) →
            [ H ] mapGraph f hs ▸* M₀≡ ≈* M₀≡ ◂* mapGraph g hs
  map-M₁≡ ε        = ≡⇒≈* H (◂*-▸*-ε M₀≡)
  map-M₁≡ (hs ◅ h) = begin
    (M₁ f hs ◅ mapGraph f h) ▸* M₀≡   ≡⟨ ◅-▸* (M₁ f hs) _ M₀≡ ⟩
    M₁ f hs ◅ (mapGraph f h ▸* M₀≡)   ≈⟨ Graph.Equiv.refl H ◅ map-M₁≡ h ⟩
    M₁ f hs ◅ (M₀≡ ◂* mapGraph g h)   ≡⟨ ◅-◂*-▸ (M₁ f hs) M₀≡ _ ⟩
    (M₁ f hs ▸ M₀≡) ◅ mapGraph g h    ≈⟨ M₁≡ ◅ (refl H) ⟩
    (M₀≡ ◂ M₁ g hs) ◅ mapGraph g h    ≡˘⟨ ◂*-◅ M₀≡ (M₁ g hs) _ ⟩
    M₀≡ ◂* (M₁ g hs ◅ mapGraph g h)   ∎
    where open PathEqualityReasoning H

module _ (C : Category o ℓ e) where
  open Category C
  open HomReasoning

  -- A helper that should probably go into Categories.Morphism.Reasoning...

  toSquare : ∀ {A B} {f g : A ⇒ B} → f ≈ g → CommutativeSquare f id id g
  toSquare {_} {_} {f} {g} f≈g = begin
        id ∘ f   ≈⟨ identityˡ ⟩
        f        ≈⟨ f≈g ⟩
        g        ≈˘⟨ identityʳ ⟩
        g ∘ id   ∎

CatF : Functor (Graphs o ℓ e) (Cats o (o ⊔ ℓ) (o ⊔ ℓ ⊔ e))
CatF = record
  { F₀ = Free
  ; F₁ = λ {G₁} {G₂} G⇒ → record
    { F₀ = M₀ G⇒
    ; F₁ = mapGraph G⇒
    ; identity = refl G₂
    ; homomorphism = λ {_} {_} {_} {f} → map-hom G⇒ f
    ; F-resp-≈ = λ { {f = f} → map-resp G⇒ f}
    }
  ; identity = λ {G} → record
    { eq₀ = λ _ → ≡.refl
    ; eq₁ = λ f → toSquare (Free G) (map-id f)
    }
  ; homomorphism = λ {_} {_} {G} → record
    { eq₀ = λ _ → ≡.refl
    ; eq₁ = λ h → toSquare (Free G) (map-∘ h)
    }
  ; F-resp-≈ = λ {_} {G} {f} {g} f≈g → record
    { eq₀ = λ _ → M₀≡ f≈g
    ; eq₁ = λ h →
      let open Category (Free G)
          open HId      (Free G)
          open TrspStar G
          open HomReasoning
      in begin
        mapGraph f h ◅◅ (hid $ M₀≡ f≈g)
      ≈˘⟨ hid-subst-cod (mapGraph f h) (M₀≡ f≈g) ⟩
        mapGraph f h ▸* M₀≡ f≈g
      ≈⟨ map-M₁≡ f≈g h ⟩
        M₀≡ f≈g ◂* mapGraph g h
      ≈⟨ hid-subst-dom (M₀≡ f≈g) (mapGraph g h) ⟩
        (hid $ M₀≡ f≈g) ◅◅ mapGraph g h
      ∎
    }
  }
  where
  open GraphMorphism
  open GraphMorphism≈

-- Because of the Level changes in CatF, sizes must all be same:
CatF-is-Free : (o : Level) → Adjoint (CatF {o} {o} {o}) (Underlying)
CatF-is-Free o = record
  { unit = ntHelper record
    { η = GM
    ; commute = λ {X} {Y} f → record { M₀≡ = ≡.refl ; M₁≡ = Graph.Equiv.refl Y ◅ ε }
    }
  ; counit = ntHelper record
    { η = λ X → record
      { F₀ = idFun
      ; F₁ = unwind X
      ; identity = Category.Equiv.refl X
      ; homomorphism = λ { {f = f} {g} → unwind-◅◅ X {f = f} {g} }
      ; F-resp-≈ = unwind-resp-≈ X
      }
    ; commute = λ {_} {Y} F → record
      { eq₀ = λ _ → ≡.refl
      ; eq₁ = λ f → toSquare Y (comm F f)
      }
    }
  ; zig = λ {G} → record
    { eq₀ = λ _ → ≡.refl
    ; eq₁ = λ f → toSquare (Free G) (zig′ G f)
    }
  ; zag = λ {B} → record { M₀≡ = ≡.refl ; M₁≡ = Category.identityˡ B  }
  }
  where
  GM : (X : Graph o o o) → GraphMorphism X (Underlying₀ (Free X))
  GM _ = record { M₀ = idFun ; M₁ = return ; M-resp-≈ = λ f≈g → f≈g ◅ ε }
  module _ (X : Category o o o) where
    open Category X
    open HomReasoning
    unwind : {A B : Obj} → Star _⇒_ A B → A ⇒ B
    unwind = fold _⇒_ (flip _∘_) id
    unwind-◅◅ : {A B C : Obj} {f : Star _⇒_ A B} {g : Star _⇒_ B C} →
                unwind (f ◅◅ g) ≈ (unwind g) ∘ (unwind f)
    unwind-◅◅ {f = ε} {g} = Equiv.sym identityʳ
    unwind-◅◅ {f = x ◅ f} {g} = ∘-resp-≈ˡ (unwind-◅◅ {f = f} {g}) ○ assoc
    unwind-resp-≈ : {A B : Obj} {f g : Star _⇒_ A B} → [ Underlying₀ X ] f ≈* g → unwind f ≈ unwind g
    unwind-resp-≈ ε = Equiv.refl
    unwind-resp-≈ (x ◅ eq) = ∘-resp-≈ (unwind-resp-≈ eq) x

  zig′ : (X : Graph o o o) → {A B : Graph.Obj X} → (f : Star (Graph._⇒_ X) A B) →
    let Y = Free X in [ X ] (unwind Y) (mapGraph (GM X) f) ≈* f
  zig′ A ε        = ε
  zig′ A (fs ◅ f) = Graph.Equiv.refl A ◅ zig′ A f

  module _ {X Y : Category o o o} (F : Functor X Y) where
    open Category X renaming (Obj to Obj₁; _⇒_ to _⇒₁_)
    open Category Y renaming (_≈_ to _≈₂_; module Equiv to EY)
    open Category.HomReasoning Y
    open Functor F
    comm : {A B : Obj₁} (f : Star _⇒₁_ A B) → unwind Y (mapGraph (Underlying₁ F) f) ≈₂ F₁ (unwind X f)
    comm ε = EY.sym identity
    comm (x ◅ f) = EY.sym (homomorphism ○ Category.∘-resp-≈ˡ Y (EY.sym (comm f)))

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
module bug where

data True : Set where
  tt : True

data Sigma (x : True) : Set where
 pair : True -> Sigma x

postulate
  p : True

T : True -> Sigma p -> Set
T tt (pair _) = True

postulate
  S : True -> Sigma p -> Set

z : Sigma p
z = pair p

postulate
  build : (q : Sigma p) -> T p q -> True
  pz    : T p z

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module conversion where

open import constants
open import cedille-types
open import ctxt
open import free-vars
open import rename
open import subst
open import syntax-util
open import general-util
open import type-util

record unfolding : Set where
  constructor unfold
  field
    unfold-all : 𝔹
    unfold-defs : 𝔹
    unfold-erase : 𝔹

unfold-all : unfolding
unfold-all = unfold tt tt tt

unfold-head : unfolding
unfold-head = unfold ff tt tt

unfold-head-elab : unfolding
unfold-head-elab = unfold ff tt ff

unfold-no-defs : unfolding
unfold-no-defs = unfold tt ff ff

unfold-head-no-defs : unfolding
unfold-head-no-defs = unfold ff ff ff

unfold-dampen : unfolding → unfolding
unfold-dampen (unfold a d e) = unfold a (a && d) e

conv-t : Set → Set
conv-t T = ctxt → T → T → 𝔹

{-# TERMINATING #-}

-- main entry point
-- does not assume erased
conv-term : conv-t term
conv-type : conv-t type
conv-kind : conv-t kind

-- assume erased
conv-terme : conv-t term
conv-argse : conv-t (𝕃 term)
conv-typee : conv-t type
conv-kinde : conv-t kind

-- call hnf, then the conv-X-norm functions
conv-term' : conv-t term
conv-type' : conv-t type

hnf : ∀ {ed : exprd} → ctxt → (u : unfolding) → ⟦ ed ⟧ → ⟦ ed ⟧

-- assume head normalized inputs
conv-term-norm : conv-t term
conv-type-norm : conv-t type
conv-kind-norm : conv-t kind

-- does not assume erased
conv-tpkd : conv-t tpkd
conv-tmtp : conv-t tmtp
conv-tmtp* : conv-t (𝕃 tmtp)

-- assume erased
conv-tpkde : conv-t tpkd
conv-tmtpe : conv-t tmtp
conv-tmtpe* : conv-t (𝕃 tmtp)

conv-ctr-ps : ctxt → var → var → maybe (ℕ × ℕ)
conv-ctr-args : conv-t (var × args)
conv-ctr : conv-t var

conv-term Γ t t' = conv-terme Γ (erase t) (erase t')

conv-terme Γ t t' with decompose-apps t | decompose-apps t'
conv-terme Γ t t' | Var x , args | Var x' , args' =
     ctxt-eq-rep Γ x x' && conv-argse Γ (erase-args args) (erase-args args')
  || conv-ctr-args Γ (x , args) (x' , args')
  || conv-term' Γ t t'
conv-terme Γ t t' | _ | _ = conv-term' Γ t t'

conv-argse Γ [] [] = tt
conv-argse Γ (a :: args) (a' :: args') = conv-terme Γ a a' && conv-argse Γ args args'
conv-argse Γ _ _ = ff

conv-type Γ t t' = conv-typee Γ (erase t) (erase t')

conv-typee Γ t t' with decompose-tpapps t | decompose-tpapps t'
conv-typee Γ t t' | TpVar x , args | TpVar x' , args' =
     ctxt-eq-rep Γ x x' && conv-tmtp* Γ args args'
  || conv-type' Γ t t'
conv-typee Γ t t' | _ | _ = conv-type' Γ t t'

conv-kind Γ k k' = conv-kinde Γ (erase k) (erase k')
conv-kinde Γ k k' = conv-kind-norm Γ (hnf Γ unfold-head k) (hnf Γ unfold-head k')

conv-term' Γ t t' = conv-term-norm Γ (hnf Γ unfold-head t) (hnf Γ unfold-head t')
conv-type' Γ t t' = conv-type-norm Γ (hnf Γ unfold-head t) (hnf Γ unfold-head t')

hnf {TERM} Γ u (AppE t T) = hnf Γ u t
hnf {TERM} Γ u (Beta _ t) = hnf Γ u t
hnf {TERM} Γ u (Delta b? T t) = id-term
hnf {TERM} Γ u (Hole pi) = Hole pi
hnf {TERM} Γ u (IotaPair t₁ t₂ x Tₓ) = hnf Γ u t₁
hnf {TERM} Γ u (IotaProj t n) = hnf Γ u t
hnf {TERM} Γ u (Lam tt x T t) = hnf Γ u t
hnf {TERM} Γ u (LetTp x k T t) = hnf Γ u t
hnf {TERM} Γ u (Phi tₑ t₁ t₂) = hnf Γ u t₂
hnf {TERM} Γ u (Rho tₑ x Tₓ t) = hnf Γ u t
hnf {TERM} Γ u (VarSigma t) = hnf Γ u t
hnf {TERM} Γ u (App t t') with hnf Γ u t
...| Lam ff x nothing t'' = hnf Γ u ([ Γ - t' / x ] t'')
...| t'' = App t'' (hnf Γ (unfold-dampen u) t')
hnf {TERM} Γ u (Lam ff x _ t) with hnf (ctxt-var-decl x Γ) u t
...| App t' (Var x') = if x' =string x && ~ is-free-in x t' then t' else Lam ff x nothing (App t' (Var x'))
...| t' = Lam ff x nothing t'
hnf {TERM} Γ u (LetTm me x T t t') = hnf Γ u ([ Γ - t / x ] t')
hnf {TERM} Γ u (Var x) with
   ifMaybe (unfolding.unfold-defs u) $ ctxt-lookup-term-var-def Γ x
...| nothing = Var x
...| just t = hnf Γ (unfold-dampen u) t
hnf {TERM} Γ u (Mu f tₒ _ t~ cs') =
  let t = hnf Γ u tₒ
      Γ' = ctxt-var-decl f Γ
      cs = erase-cases cs'
      t-else = λ t → Mu f t nothing t~ $ flip map cs λ where
                 (Case x cas t T) → Case x cas
                   (hnf (add-caseArgs-to-ctxt cas Γ') (unfold-dampen u) t) T
      case-matches : var → args → case → maybe (term × case-args × args)
      case-matches = λ {cₓ as (Case cₓ' cas t T) →
                          conv-ctr-ps Γ cₓ' cₓ ≫=maybe uncurry λ ps' ps →
                          ifMaybej (length as =ℕ length cas + ps) (t , cas , drop ps as)}
      matching-case = λ cₓ as → foldr (_||-maybe_ ∘ case-matches cₓ as) nothing cs
      sub-mu = let x = fresh-var Γ "x" in , Lam ff x nothing (t-else (Var x))
      sub = λ Γ → substs Γ (trie-insert (trie-single f sub-mu) (data-to/ f) (, id-term)) in
  maybe-else' (decompose-var-headed t ≫=maybe uncurry matching-case) (t-else t) λ where
    (tₓ , cas , as) → hnf Γ u (recompose-apps as (case-args-to-lams cas (sub (add-caseArgs-to-ctxt cas Γ') tₓ)))
hnf {TERM} Γ u (Sigma mt tₒ _ t~ cs') =
  let t = hnf Γ u tₒ
      cs = erase-cases cs'
      t-else = λ t → Sigma nothing t nothing t~ $ flip map cs λ where
                 (Case x cas t T) → Case x cas
                   (hnf (add-caseArgs-to-ctxt cas Γ) (unfold-dampen u) t) T
      case-matches : var → args → case → maybe (term × case-args × args)
      case-matches = λ {cₓ as (Case cₓ' cas t T) →
                          conv-ctr-ps Γ cₓ' cₓ ≫=maybe uncurry λ ps' ps →
                          ifMaybej (length as =ℕ length cas + ps) (t , cas , drop ps as)}
      matching-case = λ cₓ as → foldr (_||-maybe_ ∘ case-matches cₓ as) nothing cs
      sub = λ Γ → id {A = term} in
  maybe-else' (decompose-var-headed t ≫=maybe uncurry matching-case) (t-else t) λ where
    (tₓ , cas , as) → hnf Γ u (recompose-apps as (case-args-to-lams cas (sub (add-caseArgs-to-ctxt cas Γ) tₓ)))

hnf{TYPE} Γ u (TpAbs me x tk tp) = TpAbs me x (hnf Γ (unfold-dampen u) -tk tk) (hnf (ctxt-var-decl x Γ) (unfold-dampen u) tp)
hnf{TYPE} Γ u (TpIota x tp₁ tp₂) = TpIota x (hnf Γ (unfold-dampen u) tp₁) (hnf (ctxt-var-decl x Γ) (unfold-dampen u) tp₂)
hnf{TYPE} Γ u (TpAppTp tp tp') with hnf Γ u tp
...| TpLam x _ tp'' = hnf Γ u ([ Γ - tp' / x ] tp'')
...| tp'' = TpAppTp tp'' (hnf Γ (unfold-dampen u) tp')
hnf{TYPE} Γ u (TpAppTm tp tm) with hnf Γ u tp
...| TpLam x _ tp'' = hnf Γ u ([ Γ - tm / x ] tp'')
...| tp'' = TpAppTm tp''
              (if unfolding.unfold-erase u then hnf Γ (unfold-dampen u) tm else tm)
hnf{TYPE} Γ u (TpEq tm₁ tm₂) = TpEq (hnf Γ (unfold-dampen u) tm₁) (hnf Γ (unfold-dampen u) tm₂)
hnf{TYPE} Γ u (TpHole pi) = TpHole pi
hnf{TYPE} Γ u (TpLam x tk tp) = TpLam x (hnf Γ (unfold-dampen u) -tk tk) (hnf (ctxt-var-decl x Γ) (unfold-dampen u) tp)
hnf{TYPE} Γ u (TpVar x) with
   ifMaybe (unfolding.unfold-defs u) $ ctxt-lookup-type-var-def Γ x
...| nothing = TpVar x
...| just t = hnf Γ (unfold-dampen u) t

hnf{KIND} Γ u (KdAbs x tk kd) =
  KdAbs x (hnf Γ (unfold-dampen u) -tk tk) (hnf (ctxt-var-decl x Γ) u kd)
hnf{KIND} Γ u (KdHole pi) = KdHole pi
hnf{KIND} Γ u KdStar = KdStar

hanf : ctxt → (erase : 𝔹) → term → term
hanf Γ e t with erase-if e t
...| t' = maybe-else t' id
  (decompose-var-headed t' ≫=maybe uncurry λ x as →
   ctxt-lookup-term-var-def Γ x ≫=maybe λ t'' →
   just (recompose-apps as t''))

-- unfold across the term-type barrier
hnf-term-type : ctxt → (erase : 𝔹) → type → type
hnf-term-type Γ e (TpEq t₁ t₂) = TpEq (hanf Γ e t₁) (hanf Γ e t₂)
hnf-term-type Γ e (TpAppTm tp t) = hnf Γ (record unfold-head {unfold-erase = e}) (TpAppTm tp (hanf Γ e t))
hnf-term-type Γ e tp = hnf Γ unfold-head tp

conv-cases : conv-t cases
conv-cases Γ cs₁ cs₂ = isJust $ foldl (λ c₂ x → x ≫=maybe λ cs₁ → conv-cases' Γ cs₁ c₂) (just cs₁) cs₂ where
  conv-cases' : ctxt → cases → case → maybe cases
  conv-cases' Γ [] (Case x₂ as₂ t₂ T₂) = nothing
  conv-cases' Γ (c₁ @ (Case x₁ as₁ t₁ T₁) :: cs₁) c₂ @ (Case x₂ as₂ t₂ T₂) with conv-ctr Γ x₁ x₂
  ...| ff = conv-cases' Γ cs₁ c₂ ≫=maybe λ cs₁ → just (c₁ :: cs₁)
  ...| tt = ifMaybej (length as₂ =ℕ length as₁ && conv-term Γ (expand-case c₁) (expand-case (Case x₂ as₂ t₂ T₂))) cs₁

ctxt-term-udef : posinfo → defScope → opacity → var → term → ctxt → ctxt

conv-term-norm Γ (Var x) (Var x') = ctxt-eq-rep Γ x x' || conv-ctr Γ x x'
-- hnf implements erasure for terms, so we can ignore some subterms for App and Lam cases below
conv-term-norm Γ (App t1 t2) (App t1' t2') = conv-term-norm Γ t1 t1' && conv-term Γ t2 t2'
conv-term-norm Γ (Lam ff x _ t) (Lam ff x' _ t') = conv-term (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) t t'
conv-term-norm Γ (Hole _) _ = tt
conv-term-norm Γ _ (Hole _) = tt
conv-term-norm Γ (Mu x₁ t₁ _ _ cs₁) (Mu x₂ t₂ _ _ cs₂) =
  let Γ' = ctxt-rename x₁ x₂ $ ctxt-var-decl x₂ Γ in
  conv-term Γ t₁ t₂ && conv-cases Γ' cs₁ cs₂
conv-term-norm Γ (Sigma _ t₁ _ _ cs₁) (Sigma _ t₂ _ _ cs₂) = conv-term Γ t₁ t₂ && conv-cases Γ cs₁ cs₂
{- it can happen that a term is equal to a lambda abstraction in head-normal form,
   if that lambda-abstraction would eta-contract following some further beta-reductions.
   We implement this here by implicitly eta-expanding the variable and continuing
   the comparison.

   A simple example is

       λ v . t ((λ a . a) v) ≃ t
 -}
conv-term-norm Γ (Lam ff x _ t) t' =
  let x' = fresh-var Γ x in
  conv-term (ctxt-rename x x' Γ) t (App t' (Var x'))
conv-term-norm Γ t' (Lam ff x _ t) =
  let x' = fresh-var Γ x in
  conv-term (ctxt-rename x x' Γ) (App t' (Var x')) t
conv-term-norm Γ _ _ = ff

conv-type-norm Γ (TpVar x) (TpVar x') = ctxt-eq-rep Γ x x'
conv-type-norm Γ (TpApp t1 t2) (TpApp t1' t2') = conv-type-norm Γ t1 t1' && conv-tmtp Γ t2 t2'
conv-type-norm Γ (TpAbs me x tk tp) (TpAbs me' x' tk' tp') =
  (me iff me') && conv-tpkd Γ tk tk' && conv-type (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) tp tp'
conv-type-norm Γ (TpIota x m tp) (TpIota x' m' tp') =
  conv-type Γ m m' && conv-type (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) tp tp'
conv-type-norm Γ (TpEq t₁ t₂) (TpEq t₁' t₂') = conv-term Γ t₁ t₁' && conv-term Γ t₂ t₂'
conv-type-norm Γ (TpLam x tk tp) (TpLam x' tk' tp') =
  conv-tpkd Γ tk tk' && conv-type (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) tp tp'
conv-type-norm Γ _ _ = ff

{- even though hnf turns Pi-kinds where the variable is not free in the body into arrow kinds,
   we still need to check off-cases, because normalizing the body of a kind could cause the
   bound variable to be erased (hence allowing it to match an arrow kind). -}
conv-kind-norm Γ (KdAbs x tk k) (KdAbs x' tk' k'') =
    conv-tpkd Γ tk tk' && conv-kind (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) k k''
conv-kind-norm Γ KdStar KdStar = tt
conv-kind-norm Γ _ _ = ff

conv-tpkd Γ tk tk' = conv-tpkde Γ (erase -tk tk) (erase -tk tk')
conv-tmtp Γ tT tT' = conv-tmtpe Γ (erase -tT tT) (erase -tT tT')

conv-tpkde Γ (Tkk k) (Tkk k') = conv-kind Γ k k'
conv-tpkde Γ (Tkt t) (Tkt t') = conv-type Γ t t'
conv-tpkde Γ _ _ = ff

conv-tmtpe Γ (Ttm t) (Ttm t') = conv-term Γ t t'
conv-tmtpe Γ (Ttp T) (Ttp T') = conv-type Γ T T'
conv-tmtpe Γ _ _ = ff

conv-tmtp* = =𝕃 ∘ conv-tmtp

conv-tmtpe* = =𝕃 ∘ conv-tmtpe

conv-ctr Γ x₁ x₂ = conv-ctr-args Γ (x₁ , []) (x₂ , [])

conv-ctr-ps Γ x₁ x₂ with env-lookup Γ x₁ | env-lookup Γ x₂
...| just (ctr-def ps₁ T₁ n₁ i₁ a₁ , _) | just (ctr-def ps₂ T₂ n₂ i₂ a₂ , _) =
  ifMaybej (n₁ =ℕ n₂ && i₁ =ℕ i₂ && a₁ =ℕ a₂) (length (erase-params ps₁) , length (erase-params ps₂))
...| _ | _ = nothing

conv-ctr-args Γ (x₁ , as₁) (x₂ , as₂) =
  maybe-else' (conv-ctr-ps Γ x₁ x₂) ff $ uncurry λ ps₁ ps₂ →
  let as₁ = erase-args as₁; as₂ = erase-args as₂ in
  ps₁ ∸ length as₁ =ℕ ps₂ ∸ length as₂ &&
  conv-argse Γ (drop ps₁ as₁) (drop ps₂ as₂)

{-# TERMINATING #-}
inconv : ctxt → term → term → 𝔹
inconv Γ t₁ t₂ = inconv-lams empty-renamectxt empty-renamectxt
                   (hnf Γ unfold-all t₁) (hnf Γ unfold-all t₂)
  where
  fresh : var → renamectxt → renamectxt → var
  fresh x ρ₁ ρ₂ = fresh-h (λ x → ctxt-binds-var Γ x || renamectxt-in-field ρ₁ x || renamectxt-in-field ρ₂ x) x

  make-subst : renamectxt → renamectxt → 𝕃 var → 𝕃 var → term → term → (renamectxt × renamectxt × term × term)
  make-subst ρ₁ ρ₂ [] [] t₁ t₂ = ρ₁ , ρ₂ , t₁ , t₂
  make-subst ρ₁ ρ₂ (x₁ :: xs₁) [] t₁ t₂ =
    let x = fresh x₁ ρ₁ ρ₂ in
    make-subst (renamectxt-insert ρ₁ x₁ x) (renamectxt-insert ρ₂ x x) xs₁ [] t₁ (App t₂ $ Var x)
  make-subst ρ₁ ρ₂ [] (x₂ :: xs₂) t₁ t₂ =
    let x = fresh x₂ ρ₁ ρ₂ in
    make-subst (renamectxt-insert ρ₁ x x) (renamectxt-insert ρ₂ x₂ x) [] xs₂ (App t₁ $ Var x) t₂
  make-subst ρ₁ ρ₂ (x₁ :: xs₁) (x₂ :: xs₂) t₁ t₂ =
    let x = fresh x₁ ρ₁ ρ₂ in
    make-subst (renamectxt-insert ρ₁ x₁ x) (renamectxt-insert ρ₂ x₂ x) xs₁ xs₂ t₁ t₂

  inconv-lams : renamectxt → renamectxt → term → term → 𝔹
  inconv-apps : renamectxt → renamectxt → var → var → args → args → 𝔹
  inconv-ctrs : renamectxt → renamectxt → var → var → args → args → 𝔹
  inconv-mu : renamectxt → renamectxt → maybe (var × var) → cases → cases → 𝔹
  inconv-args : renamectxt → renamectxt → args → args → 𝔹

  inconv-args ρ₁ ρ₂ a₁ a₂ =
    let a₁ = erase-args a₁; a₂ = erase-args a₂ in
    ~  length a₁ =ℕ length a₂
    || list-any (uncurry $ inconv-lams ρ₁ ρ₂) (zip a₁ a₂)

  inconv-lams ρ₁ ρ₂ t₁ t₂ =
    elim-pair (decompose-lams t₁) λ l₁ b₁ →
    elim-pair (decompose-lams t₂) λ l₂ b₂ →
    elim-pair (make-subst ρ₁ ρ₂ l₁ l₂ b₁ b₂) λ ρ₁ ρ₂b₁₂ →
    elim-pair ρ₂b₁₂ λ ρ₂ b₁₂ →
    elim-pair b₁₂ λ b₁ b₂ →
    case (decompose-apps b₁ , decompose-apps b₂) of uncurry λ where
      (Var x₁ , a₁) (Var x₂ , a₂) →
        inconv-apps ρ₁ ρ₂ x₁ x₂ a₁ a₂ || inconv-ctrs ρ₁ ρ₂ x₁ x₂ a₁ a₂
      (Mu x₁ t₁ _ _ ms₁ , a₁) (Mu x₂ t₂ _ _ ms₂ , a₂) →
        inconv-mu ρ₁ ρ₂ (just $ x₁ , x₂) ms₁ ms₂ ||
        inconv-lams ρ₁ ρ₂ t₁ t₂ || inconv-args ρ₁ ρ₂ a₁ a₂
      (Sigma _ t₁ _ _ ms₁ , a₁) (Sigma _ t₂ _ _ ms₂ , a₂) →
        inconv-mu ρ₁ ρ₂ nothing ms₁ ms₂ ||
        inconv-lams ρ₁ ρ₂ t₁ t₂ || inconv-args ρ₁ ρ₂ a₁ a₂
      _ _ → ff

  inconv-apps ρ₁ ρ₂ x₁ x₂ a₁ a₂ =
    maybe-else' (renamectxt-lookup ρ₁ x₁) ff λ x₁ →
    maybe-else' (renamectxt-lookup ρ₂ x₂) ff λ x₂ →
    ~ x₁ =string x₂
    || inconv-args ρ₁ ρ₂ a₁ a₂

  inconv-ctrs ρ₁ ρ₂ x₁ x₂ as₁ as₂ with env-lookup Γ x₁ | env-lookup Γ x₂
  ...| just (ctr-def ps₁ _ n₁ i₁ a₁ , _) | just (ctr-def ps₂ _ n₂ i₂ a₂ , _) =
    let ps₁ = erase-params ps₁; ps₂ = erase-params ps₂
        as₁ = erase-args   as₁; as₂ = erase-args   as₂ in
    length as₁ ≤ length ps₁ + a₁ && -- Could use of "≤" here conflict with η-equality?
    length as₂ ≤ length ps₂ + a₂ &&
    (~ n₁ =ℕ n₂ ||
    ~ i₁ =ℕ i₂ ||
    ~ a₁ =ℕ a₂ ||
    ~ length as₁ + length ps₂ =ℕ length as₂ + length ps₁ ||
    -- ^ as₁ ∸ ps₁ ≠ as₂ ∸ ps₂, + ps₁ + ps₂ to both sides ^
    list-any (uncurry $ inconv-lams ρ₁ ρ₂)
      (zip (drop (length ps₁) as₁) (drop (length ps₂) as₂)))
  ...| _ | _ = ff

  inconv-mu ρ₁ ρ₂ xs? ms₁ ms₂ =
    ~ length ms₁ =ℕ length ms₂ ||
    maybe-else ff id
      (foldr {B = maybe 𝔹} (λ c b? → b? ≫=maybe λ b → inconv-case c ≫=maybe λ b' → just (b || b')) (just ff) ms₁)
    where
    matching-case : case → maybe (term × ℕ × ℕ)
    matching-case (Case x _ _ _) = foldl (λ where
      (Case xₘ cas tₘ _) m? → m? ||-maybe
        (conv-ctr-ps Γ xₘ x ≫=maybe uncurry λ psₘ ps →
         just (case-args-to-lams cas tₘ , length cas , ps)))
      nothing ms₂

    inconv-case : case → maybe 𝔹
    inconv-case c₁ @ (Case x cas₁ t₁ _) =
      matching-case c₁ ≫=maybe λ c₂ →
      just (inconv-lams ρ₁ ρ₂ (case-args-to-lams cas₁ t₁) (fst c₂))

ctxt-kind-def : posinfo → var → params → kind → ctxt → ctxt
ctxt-kind-def pi v ps2 k Γ =
  record Γ {
    qual = qualif-insert-params (ctxt.qual Γ) (ctxt.mn Γ # v) v (ctxt.ps Γ);
    syms = trie-insert-append2 (ctxt.syms Γ) (ctxt.fn Γ) (ctxt.mn Γ) v;
    i = trie-insert (ctxt.i Γ) (ctxt.mn Γ # v)
          (kind-def (ctxt.ps Γ ++ ps2) (hnf Γ unfold-head-elab k) , ctxt.fn Γ , pi)
  }

ctxt-datatype-decl : var → var → args → ctxt → ctxt
ctxt-datatype-decl vₒ vᵣ as Γ =
  record Γ {
    μ' = trie-insert (ctxt.μ' Γ) (mu-Type/ vᵣ) (vₒ , as);
    μ̲ = stringset-insert (ctxt.μ̲ Γ) (mu-Type/ vᵣ)
  }

ctxt-datatype-undef : var → ctxt → ctxt
ctxt-datatype-undef v Γ =
  record Γ {
    μ = trie-remove (ctxt.μ Γ) v;
    μ' = trie-remove (ctxt.μ' Γ) v;
    Is/μ = trie-remove (ctxt.Is/μ Γ) v;
    μ~ = trie-remove (ctxt.μ~ Γ) v;
    μ̲ = trie-remove (ctxt.μ̲ Γ) v
  }

ctxt-datatype-def : posinfo → var → params → kind → kind → ctrs → encoding-defs → ctxt → ctxt
ctxt-datatype-def pi D psᵢ kᵢ k cs eds Γ =
  let D' = ctxt.mn Γ # D
      ecds = record {
        Is/D = data-Is/ D';
        is/D = data-is/ D';
        to/D = data-to/ D';
        TypeF/D = data-TypeF/ D';
        fmap/D = data-fmap/ D';
        IndF/D = data-IndF/ D'} in
  record Γ {
    qual = qualif-insert-params (ctxt.qual Γ) D' D (ctxt.ps Γ);
    syms = trie-insert-append2 (ctxt.syms Γ) (ctxt.fn Γ) (ctxt.mn Γ) D;
    i = trie-insert (ctxt.i Γ) D' (type-def (just (ctxt.ps Γ)) tt nothing (abs-expand-kind psᵢ k) , ctxt.fn Γ , pi);
    μ = trie-insert (ctxt.μ Γ) D' (ctxt.ps Γ ++ psᵢ , kᵢ , k , cs , eds , ecds);
    Is/μ = trie-insert (ctxt.Is/μ Γ) (data-Is/ D') D';
    μ~ = trie-insert (ctxt.μ~ Γ) D' (foldl pull-defs [] (encoding-defs.ecs eds ++ encoding-defs.gcs eds));
    μᵤ = just eds;
    μ̲ = stringset-insert (ctxt.μ̲ Γ) D'
  }
  where
  pull-defs : cmd → 𝕃 (var × tmtp) → 𝕃 (var × tmtp)
  pull-defs (CmdDefTerm x t) μ~ = ((ctxt.mn Γ # x) , Ttm t) :: μ~
  pull-defs (CmdDefType x k T) μ~ = ((ctxt.mn Γ # x) , Ttp T) :: μ~
  pull-defs _ μ~ = μ~

ctxt-type-def : posinfo → defScope → opacity → var → maybe type → kind → ctxt → ctxt
ctxt-type-def _  _ _ ignored-var _ _  Γ = Γ
ctxt-type-def pi s op v t k Γ =
  let v' = if s iff localScope then pi % v else ctxt.mn Γ # v in
  record Γ {
    qual = qualif-insert-params (ctxt.qual Γ) v' v (if s iff localScope then [] else ctxt.ps Γ);
    i = trie-insert (ctxt.i Γ) v' (type-def (def-params s (ctxt.ps Γ)) op (hnf Γ unfold-head-elab <$> t) k , ctxt.fn Γ , pi)
  }

ctxt-ctr-def : posinfo → var → type → params → (ctrs-length ctr-index : ℕ) → ctxt → ctxt
ctxt-ctr-def pi c t ps' n i Γ =
  let c' = ctxt.mn Γ # c in
  record Γ {
    qual = qualif-insert-params (ctxt.qual Γ) c' c (ctxt.ps Γ);
    syms = trie-insert-append2 (ctxt.syms Γ) (ctxt.fn Γ) (ctxt.mn Γ) c;
    i = trie-insert (ctxt.i Γ) c' (ctr-def ps' t n i (unerased-arrows t) , ctxt.fn Γ , pi)
  }

ctxt-term-def : posinfo → defScope → opacity → var → maybe term → type → ctxt → ctxt
ctxt-term-def _  _ _  ignored-var _ _ Γ = Γ
ctxt-term-def pi s op v t tp Γ =
  let v' = if s iff localScope then pi % v else ctxt.mn Γ # v in
  record Γ {
    qual = qualif-insert-params (ctxt.qual Γ) v' v (if s iff localScope then [] else ctxt.ps Γ);
    syms = if s iff localScope then ctxt.syms Γ else trie-insert-append2 (ctxt.syms Γ) (ctxt.fn Γ) (ctxt.mn Γ) v;
    i = trie-insert (ctxt.i Γ) v' (term-def (def-params s (ctxt.ps Γ)) op (hnf Γ unfold-head <$> t) tp , ctxt.fn Γ , pi)
  }

ctxt-term-udef _ _ _ ignored-var _ Γ = Γ
ctxt-term-udef pi s op v t Γ =
  let v' = if s iff localScope then pi % v else ctxt.mn Γ # v in
  record Γ {
    qual = qualif-insert-params (ctxt.qual Γ) v' v (if s iff localScope then [] else ctxt.ps Γ);
    syms = if s iff localScope then ctxt.syms Γ else trie-insert-append2 (ctxt.syms Γ) (ctxt.fn Γ) (ctxt.mn Γ) v;
    i = trie-insert (ctxt.i Γ) v' (term-udef (def-params s (ctxt.ps Γ)) op (hnf Γ unfold-head t) , ctxt.fn Γ , pi)
  }


text:
module IrrelevantModuleParameter1 (A : Set) .(a : A) where

postulate
  P : A -> Set
  p : P a
-- cannot use a here, because it is irrelevant

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --cubical --no-positivity-check --no-termination-check --allow-unsolved-metas #-}

open import Prelude
open import Algebra
open import Algebra.Monus
open import Relation.Binary
open import Data.Maybe
open import Data.List using (List; _∷_; []; foldr)

module Control.Monad.HeapT.Sized
  {ℓ}
  (mon : CTMAPOM ℓ)
  (gmon : GradedMonad (CTMAPOM.monoid mon) ℓ ℓ)
  where

open CTMAPOM mon
open GradedMonad gmon

private
  variable
    w i j : 𝑆

infixr 5 _∷_
infixr 6 _⋊_

mutual
  data Root′ (A : Type ℓ) (i : 𝑆) : Type ℓ where
    _⋊_ : ∀ w → (w < i → 𝐹 w (Branch A (i ∸ w))) → Root′ A i

  data Node (A : Type ℓ) (i : 𝑆) : Type ℓ where
    ⌊_⌋ : A → Node A i
    ⌈_⌉ : Root′ A i → Node A i

  data Branch (A : Type ℓ) (i : 𝑆) : Type ℓ where
    []  : Branch A i
    _∷_ : Node A i → 𝐹 ε (Branch A i) → Branch A i

Heap : Type ℓ → Type ℓ
Heap A = ∀ {i} → 𝐹 ε (Branch A i)

infixr 5 _++_
_++_ : 𝐹 w (Branch A i) → 𝐹 ε (Branch A i) → 𝐹 w (Branch A i)
xs ++ ys =
  xs >>=ε λ  {  []       → ys
             ;  (x ∷ xs) → pure (x ∷ xs ++ ys) }

infixr 1 _>>=ᴺ_ _>>=ᴴ_
mutual
  _>>=ᴺ_ : Node A i → (A → Heap B) → 𝐹 ε (Branch B i)
  ⌊ x ⌋  >>=ᴺ f = f x
  ⌈ w ⋊ s ⌉  >>=ᴺ f = pure (⌈ w ⋊ (λ w<i → s w<i >>=ᴴ f) ⌉ ∷ pure [])

  _>>=ᴴ_ : 𝐹 w (Branch A i) → (A → Heap B) → 𝐹 w (Branch B i)
  xs >>=ᴴ f =
    xs >>=ε λ  {  []        → pure []
               ;  (x ∷ xs)  → (x >>=ᴺ f) ++ (xs >>=ᴴ f) }

pureᴴ : A → Heap A
pureᴴ x = pure (⌊ x ⌋ ∷ pure [])

liftᴴ : 𝐹 w A → Heap A
liftᴴ xs = pure (⌈ _ ⋊ const (map (λ x → ⌊ x ⌋ ∷ pure []) xs) ⌉ ∷ pure [])

flatten : 𝐹 w (Branch A i) → 𝐹 w (List A × List (Root′ A i))
flatten xs =
  xs >>=ε λ  {  []            → pure ([] , [])
             ;  (⌊ x ⌋ ∷ xs)  → map (map₁ (x ∷_)) (flatten xs)
             ;  (⌈ x ⌉ ∷ xs)  → map (map₂ (x ∷_)) (flatten xs) }

module PopMin
  (decomp : ∀ {A B w₁ w₂ w₃} → 𝐹 (w₁ ∙ w₂) A → 𝐹 (w₁ ∙ w₃) B → 𝐹 w₁ (𝐹 w₂ A × 𝐹 w₃ B))
  (choice : {w : 𝑆} → {A B : Type ℓ} → (A → 𝐹 w B) → 𝐹 w (A → B))
  where

  _∪_ : Root′ A i → Root′ A i → Root′ A i
  _∪_ {i = i} (wˣ ⋊ xs) (wʸ ⋊ ys) with wˣ ≤|≥ wʸ
  ... | inr (k , wˣ≡wʸ∙k) = {!!}
  ... | inl (k , wʸ≡wˣ∙k) = wˣ ⋊ λ wˣ<i → map (λ { (xs , ys) → ⌈ k ⋊ (λ k<i∸wˣ → subst (𝐹 _ ∘ Branch _) (cong (_ ∸_) wʸ≡wˣ∙k ; sym (∸‿assoc _ wˣ k)) (map (_$ subst (_< i) (sym wʸ≡wˣ∙k) {!!})  ys)) ⌉ ∷ xs }) (decomp (subst (flip 𝐹 _) (sym (∙ε _)) (xs wˣ<i)) (subst (flip 𝐹 _) wʸ≡wˣ∙k (choice ys)))
    where
    lemma : ∀ x y z → x < z → y < z ∸ x → x ∙ y < z
    lemma = {!!}

  -- ⋃⁺ : Root A → List (Root A) → Root A
  -- ⋃⁺ x₁ []             = x₁
  -- ⋃⁺ x₁ (x₂ ∷ [])      = x₁ ∪ x₂
  -- ⋃⁺ x₁ (x₂ ∷ x₃ ∷ xs) = (x₁ ∪ x₂) ∪ ⋃⁺ x₃ xs

  -- ⋃ : List (Root A) → Maybe (Root A)
  -- ⋃ []       = nothing
  -- ⋃ (x ∷ xs) = just (⋃⁺ x xs)

  -- popMin : 𝐹 w (Branch A) → 𝐹 w (List A × Maybe (Root A))
  -- popMin = map (map₂ ⋃) ∘ flatten

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

{-# OPTIONS --guardedness #-}

open import Data.Empty
open import Data.Product
open import Data.Sum
open import Data.List using ([]; _++_; _∷_; _∷ʳ_)

open import Relation.Nullary
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Unary using (_∈_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; subst)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (ε; _◅_; _◅◅_; return)

open import Common

module FairCompliance {ℙ : Set} (message : Message ℙ)
  where

open import Trace message
open import Session message
open import SessionType message
open import Transitions message
open import HasTrace message

fair-compliance-red* : ∀{S S'} -> FairComplianceS S -> Reductions S S' -> FairComplianceS S'
fair-compliance-red* comp reds reds' = comp (reds ◅◅ reds')

fair-compliance->may-succeed : ∀{S} -> FairComplianceS S -> MaySucceed S
fair-compliance->may-succeed fcomp = fcomp ε

fc-after-output :
  ∀{f g x} ->
  FairComplianceS (out f # inp g) ->
  x ∈ dom f ->
  FairComplianceS (f x .force # g x .force)
fc-after-output comp fx reds = comp (sync (out fx) inp ◅ reds)

fc-after-input :
  ∀{f g x} ->
  FairComplianceS (inp f # out g) ->
  x ∈ dom g ->
  FairComplianceS (f x .force # g x .force)
fc-after-input comp gx reds = comp (sync inp (out gx) ◅ reds)

fc-input : ∀{R f} -> FairComplianceS (R # inp f) ->
            Win R ⊎ ∃[ g ] (R ≡ out g × Witness g × (∀{x} (!x : x ∈ dom g) -> FairComplianceS (g x .force # f x .force)))
fc-input {nil} spec with spec ε
... | _ , ε , win#def () _
... | _ , sync () _ ◅ _ , _
fc-input {inp _} spec with spec ε
... | _ , ε , win#def () _
... | _ , sync () inp ◅ _ , _
fc-input {out g} spec with Empty? g
... | inj₁ U = inj₁ (out U)
... | inj₂ W = inj₂ (g , refl , W , λ !x -> fair-compliance-red* spec (return (sync (out !x) inp)))

fc-output : ∀{R f} -> FairComplianceS (R # out f) ->
            Win R ⊎ ∃[ g ] (R ≡ inp g × Witness f × (∀{x} (!x : x ∈ dom f) -> FairComplianceS (g x .force # f x .force)))
fc-output {nil} spec with spec ε
... | _ , ε , win#def () out
... | _ , sync () _ ◅ _ , _
fc-output {inp g} {f} spec with Empty? f
... | inj₂ W = inj₂ (g , refl , W , λ !x -> fair-compliance-red* spec (return (sync inp (out !x))))
... | inj₁ U with spec ε
... | _ , ε , win#def () _
... | _ , sync inp (out !x) ◅ _ , _ = ⊥-elim (U _ !x)
fc-output {out g} spec with Empty? g
... | inj₁ U = inj₁ (out U)
... | inj₂ (_ , !x) with spec ε
... | _ , ε , win#def (out U) out = ⊥-elim (U _ !x)
... | _ , sync () (out _) ◅ _ , _

fc-transitions :
  ∀{R R' T T' φ} ->
  Transitions R (co-trace φ) R' ->
  Transitions T φ T' ->
  FairComplianceS (R # T) ->
  FairComplianceS (R' # T')
fc-transitions rr tr comp = fair-compliance-red* comp (zip-red* rr tr)

fc-trace :
  ∀{R T φ} ->
  FairComplianceS (R # T) ->
  (rφ : R HasTrace (co-trace φ))
  (tφ : T HasTrace φ) ->
  FairComplianceS (after rφ # after tφ)
fc-trace comp (_ , _ , rr) (_ , _ , tr) = fc-transitions rr tr comp

fc-output-trace :
  ∀{R T x} ->
  FairComplianceS (R # T) ->
  T HasTrace (O x ∷ []) ->
  Win R ⊎ (R HasTrace (I x ∷ []))
fc-output-trace {nil} comp tφ with comp ε
... | _ , ε , win#def () _
... | _ , sync () _ ◅ _ , _
fc-output-trace {inp f} {_} {x} comp (_ , _ , step (out gx) refl) with x ∈? f
... | yes fx = inj₂ (_ , fx , step inp refl)
... | no nfx with comp (return (sync inp (out gx)))
... | _ , ε , win#def w _ = ⊥-elim (nfx (win->defined w))
... | _ , sync r _ ◅ _ , _ = ⊥-elim (contraposition transition->defined nfx r)
fc-output-trace {out f} comp (_ , _ , step (out _) refl) with comp ε
... | _ , ε , win#def w _ = inj₁ w
... | _ , sync () (out _) ◅ _ , _

has-trace-snoc :
  ∀{T φ α} -> T HasTrace (φ ∷ʳ α) ->
  ∃ λ (tφ : T HasTrace φ) -> after tφ HasTrace (α ∷ [])
has-trace-snoc {_} {[]} tα@(_ , _ , step inp refl) = (_ , inp , refl) , tα
has-trace-snoc {_} {[]} tα@(_ , _ , step (out _) refl) = (_ , out , refl) , tα
has-trace-snoc {_} {_ ∷ φ} (_ , def , step t tr) =
  let (_ , tdef , sr) , tφ/α = has-trace-snoc (_ , def , tr) in
  (_ , tdef , step t sr) , tφ/α

client-wins-or-accepts-prefix :
  ∀{R T φ x}
  (comp : FairComplianceS (R # T))
  (rφ : R HasTrace (co-trace φ))
  (tφ : T HasTrace (φ ∷ʳ O x)) ->
  Win (after rφ) ⊎ R HasTrace (co-trace (φ ∷ʳ O x))
client-wins-or-accepts-prefix {_} {_} {φ} comp rφ tφα with has-trace-snoc tφα
... | tφ , tφ/α with fc-trace comp rφ tφ
... | comp/φ with fc-output-trace comp/φ tφ/α
... | inj₁ w = inj₁ w
... | inj₂ rφ/α =
  let rφα = join-trace rφ rφ/α in
  inj₂ (subst (_ HasTrace_) (sym (co-trace-++ φ _)) rφα)

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module OscarPrelude where

open import Prelude public
  renaming (_==_ to _≟_) -- TODO ask Agda to rename Eq._==_ to Eq._≟_
  renaming (force to force!) -- needed by ∞Delay
  renaming (forceLemma to force!Lemma)

_≢_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
x ≢ y = ¬ (x ≡ y)

infix 0 _↔_
_↔_ : {ℓ¹ : Level} → Set ℓ¹ → {ℓ² : Level} → Set ℓ² → Set (ℓ¹ ⊔ ℓ²)
P ↔ Q = (P → Q) × (Q → P)

infix 0 _←⊗→_
_←⊗→_ : {ℓ¹ : Level} → Set ℓ¹ → {ℓ² : Level} → Set ℓ² → Set (ℓ¹ ⊔ ℓ²)
P ←⊗→ Q = (P → ¬ Q) × (Q → ¬ P)

∃ : ∀ {ℓᴬ ℓᴮ} {A : Set ℓᴬ} (B : A → Set ℓᴮ) → Set (ℓᴬ ⊔ ℓᴮ)
∃ = Σ _

∄ : ∀ {ℓᴬ ℓᴮ} {A : Set ℓᴬ} (B : A → Set ℓᴮ) → Set (ℓᴬ ⊔ ℓᴮ)
∄ = ¬_ ∘ ∃

infixl 4 _⊎_
_⊎_ = Either

{-# DISPLAY Either = _⊎_ #-}

--open import Agda.Builtin.Size public
open import Size public

open import Control.Monad.State public
open import Control.Monad.Identity public
open import Container.Traversable public
open import Container.List renaming (_∈_ to _∈Container_) public

sequence : ∀ {a b} {A : Set a} {F : Set a → Set b} ⦃ _ : Applicative F ⦄ → List (F A) → F ⊤′
sequence [] = pure tt
sequence (x ∷ xs) = x *> sequence xs

open import Tactic.Nat public

open import Tactic.Deriving.Eq public


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Semi-heterogeneous vector equality over setoids
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.Vec.Relation.Binary.Equality.Setoid
  {a ℓ} (S : Setoid a ℓ) where

open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.Vec
open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
  using (Pointwise)
open import Function
open import Level using (_⊔_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open Setoid S renaming (Carrier to A)

------------------------------------------------------------------------
-- Definition of equality

infix 4 _≋_

_≋_ : ∀ {m n} → REL (Vec A m) (Vec A n) (a ⊔ ℓ)
_≋_ = Pointwise _≈_

open Pointwise public using ([]; _∷_)
open PW public using (length-equal)

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

≋-refl : ∀ {n} → Reflexive (_≋_ {n})
≋-refl = PW.refl refl

≋-sym : ∀ {n m} → Sym _≋_ (_≋_ {m} {n})
≋-sym = PW.sym sym

≋-trans : ∀ {n m o} → Trans (_≋_ {m}) (_≋_ {n} {o}) (_≋_)
≋-trans = PW.trans trans

≋-isEquivalence : ∀ n → IsEquivalence (_≋_ {n})
≋-isEquivalence = PW.isEquivalence isEquivalence

≋-setoid : ℕ → Setoid a (a ⊔ ℓ)
≋-setoid = PW.setoid S

------------------------------------------------------------------------
-- map

open PW public using ( map⁺)

------------------------------------------------------------------------
-- ++

open PW public using (++⁺ ; ++⁻ ; ++ˡ⁻; ++ʳ⁻)

++-identityˡ : ∀ {n} (xs : Vec A n) → [] ++ xs ≋ xs
++-identityˡ _ = ≋-refl

++-identityʳ : ∀ {n} (xs : Vec A n) → xs ++ [] ≋ xs
++-identityʳ []       = []
++-identityʳ (x ∷ xs) = refl ∷ ++-identityʳ xs

map-++-commute : ∀ {b m n} {B : Set b}
                   (f : B → A) (xs : Vec B m) {ys : Vec B n} →
                   map f (xs ++ ys) ≋ map f xs ++ map f ys
map-++-commute f []       = ≋-refl
map-++-commute f (x ∷ xs) = refl ∷ map-++-commute f xs

------------------------------------------------------------------------
-- concat

open PW public using (concat⁺; concat⁻)

------------------------------------------------------------------------
-- replicate

replicate-shiftʳ : ∀ {m} n x (xs : Vec A m) →
                  replicate {n = n}     x ++ (x ∷ xs) ≋
                  replicate {n = 1 + n} x ++      xs
replicate-shiftʳ zero    x xs = ≋-refl
replicate-shiftʳ (suc n) x xs = refl ∷ (replicate-shiftʳ n x xs)


text:
module IIRD where

open import LF

-- A code for an IIRD (captures both general and restricted IIRDs)
-- I - index set
-- D - return type of the recursive component
-- E - generalised return type of the recursive component (including the index)
--     for restricted IIRD  E = D i   for an external i
--     and for general IIRD E = (i : I) × D i
--     The intuition is that restricted IIRD are parameterised over the index,
--     whereas general IIRD compute their indices.
data OP (I : Set)(D : I -> Set1)(E : Set1) : Set1 where

  -- Nullary constructor, contains the result of the recursive component
  ι : E -> OP I D E

  -- Non-recursive argument A, following arguments may depend on this argument.
  -- To code multi-constructor datatypes, the first argument is the name of the
  -- constructor and γ does the appropriate case-split on the name.
  σ : (A : Set)(γ : A -> OP I D E) -> OP I D E

  -- Recursive argument
  -- A - assumptions, for instance  lim : (Nat -> Ord) -> Ord, where A = Nat
  -- i - the index of the inductive occurrence
  -- γ - the rest of the arguments, may depend on the result of calling the
  --	 recursive function on the inductive argument
  δ : (A : Set)(i : A -> I)(γ : ((a : A) -> D (i a)) -> OP I D E) -> OP I D E

-- Helper function. The definition is simple, but the type is not.
_«_×_» : {A B : Set}{C : B -> Set}{D : B -> Set1}
         (f : (b : B) -> C b -> D b)
         (g : A -> B)(h : (a : A) -> C (g a)) ->
         (a : A) -> D (g a)
f « g × h » = \a -> f (g a) (h a)

-- The type of constructor arguments. Parameterised over
--  U - the inductive type
--  T - the recursive function
-- This is the F of the simple polynomial type μF
Ku : {I : Set}{D : I -> Set1}{E : Set1} -> OP I D E ->
     (U : I -> Set)(T : (i : I) -> U i -> D i) -> Set
Ku (ι e)     U T = One
Ku (σ A γ)   U T = A × \a -> Ku (γ a) U T
Ku (δ A i γ) U T = ((a : A) -> U (i a)) × \g -> Ku (γ (T « i × g »)) U T

-- The recursive function. As with Ku this is only the top-level structure.
-- To get the real function there is a recursive knot to be tied.
Kt : {I : Set}{D : I -> Set1}{E : Set1}
     (γ : OP I D E)(U : I -> Set)(T : (i : I) -> U i -> D i) ->
     Ku γ U T -> E
Kt (ι e)     U T ★         = e
Kt (σ A γ)   U T < a | b > = Kt (γ a) U T b
Kt (δ A i γ) U T < g | b > = Kt (γ (T « i × g »)) U T b

-- The assumptions of a particular inductive occurrence in a value.
KIArg : {I : Set}{D : I -> Set1}{E : Set1}
       (γ : OP I D E)(U : I -> Set)(T : (i : I) -> U i -> D i) ->
       Ku γ U T -> Set
KIArg (ι e)     U T ★         = Zero
KIArg (σ A γ)   U T < a | b > = KIArg (γ a) U T b
KIArg (δ A i γ) U T < g | b > = A + KIArg (γ (T « i × g »)) U T b

-- Given the assumptions of an inductive occurence in a value we can compute
-- its index.
KIArg→I : {I : Set}{D : I -> Set1}{E : Set1}
          (γ : OP I D E)(U : I -> Set)(T : (i : I) -> U i -> D i) ->
          (a : Ku γ U T) -> KIArg γ U T a -> I
KIArg→I (ι e)     U T ★ ()
KIArg→I (σ A γ)   U T < a | b > c       = KIArg→I (γ a) U T b c
KIArg→I (δ A i γ) U T < g | b > (inl a) = i a
KIArg→I (δ A i γ) U T < g | b > (inr a) = KIArg→I (γ (T « i × g »)) U T b a

-- Given the assumptions of an inductive occurrence in a value we can compute
-- its value.
KIArg→U : {I : Set}{D : I -> Set1}{E : Set1}
          (γ : OP I D E)(U : I -> Set)(T : (i : I) -> U i -> D i) ->
          (a : Ku γ U T)(v : KIArg γ U T a) -> U (KIArg→I γ U T a v)
KIArg→U (ι e)     U T ★ ()
KIArg→U (σ A γ)   U T < a | b > c       = KIArg→U (γ a) U T b c
KIArg→U (δ A i γ) U T < g | b > (inl a) = g a
KIArg→U (δ A i γ) U T < g | b > (inr a) = KIArg→U (γ (T « i × g »)) U T b a

-- The type of induction hypotheses. Basically
--  forall assumptions, the predicate holds for an inductive occurrence with
--  those assumptions
KIH : {I : Set}{D : I -> Set1}{E : Set1}
      (γ : OP I D E)(U : I -> Set)(T : (i : I) -> U i -> D i) ->
      (F : (i : I) -> U i -> Set1)(a : Ku γ U T) -> Set1
KIH γ U T F a = (v : KIArg γ U T a) -> F (KIArg→I γ U T a v) (KIArg→U γ U T a v)

-- If we can prove a predicate F for any values, we can construct the inductive
-- hypotheses for a given value.
-- Termination note: g will only be applied to values smaller than a
Kmap : {I : Set}{D : I -> Set1}{E : Set1}
       (γ : OP I D E)(U : I -> Set)(T : (i : I) -> U i -> D i) ->
       (F : (i : I) -> U i -> Set1)
       (g : (i : I)(u : U i) -> F i u)
       (a : Ku γ U T) -> KIH γ U T F a
Kmap γ U T F g a = \v -> g (KIArg→I γ U T a v) (KIArg→U γ U T a v)

-- Things needed for general IIRD

OPg : (I : Set)(D : I -> Set1) -> Set1
OPg I D = OP I D (I ×' D)

Gu : {I : Set}{D : I -> Set1}(γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i) -> Set
Gu γ U T = Ku γ U T

Gi : {I : Set}{D : I -> Set1}(γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
     (a : Gu γ U T) -> I
Gi γ U T a = π₀' (Kt γ U T a)

Gt : {I : Set}{D : I -> Set1}(γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
     (a : Gu γ U T) -> D (Gi γ U T a)
Gt γ U T a = π₁' (Kt γ U T a)

-- Things needed for restricted IIRD

OPr : (I : Set)(D : I -> Set1) -> Set1
OPr I D = (i : I) -> OP I D (D i)

Hu : {I : Set}{D : I -> Set1}
     (γ : OPr I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
     (i : I) -> Set
Hu γ U T i = Ku (γ i) U T

Ht : {I : Set}{D : I -> Set1}
     (γ : OPr I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
     (i : I)(a : Hu γ U T i) -> D i
Ht γ U T i a = Kt (γ i) U T a


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Conversion {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.RedSteps
open import Definition.Typed.Properties
import Definition.Typed.Weakening as Wk
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Conversion of syntactic reduction closures.
convRed:*: : ∀ {t u A B Γ} → Γ ⊢ t :⇒*: u ∷ A → Γ ⊢ A ≡ B → Γ ⊢ t :⇒*: u ∷ B
convRed:*: [ ⊢t , ⊢u , d ] A≡B = [ conv ⊢t  A≡B , conv ⊢u  A≡B , conv* d  A≡B ]

mutual
  -- Helper function for conversion of terms converting from left to right.
  convTermT₁ : ∀ {l l′ Γ A B t} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
             → ShapeView Γ l l′ A B [A] [B]
             → Γ ⊩⟨ l ⟩  A ≡ B / [A]
             → Γ ⊩⟨ l ⟩  t ∷ A / [A]
             → Γ ⊩⟨ l′ ⟩ t ∷ B / [B]
  convTermT₁ (ℕᵥ D D′) A≡B t = t
  convTermT₁ (Emptyᵥ D D′) A≡B t = t
  convTermT₁ (Unitᵥ D D′) A≡B t = t
  convTermT₁ (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
             (neₜ k d (neNfₜ neK₂ ⊢k k≡k)) =
    let K≡K₁ = PE.subst (λ x → _ ⊢ _ ≡ x)
                        (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                        (≅-eq (~-to-≅ K≡M))
    in  neₜ k (convRed:*: d K≡K₁)
            (neNfₜ neK₂ (conv ⊢k K≡K₁) (~-conv k≡k K≡K₁))
  convTermT₁ {Γ = Γ} (Bᵥ BΠ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                            (Bᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
             (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
             (Πₜ f d funcF f≡f [f] [f]₁) =
    let ΠF₁G₁≡ΠF′G′   = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
        F₁≡F′ , G₁≡G′ = B-PE-injectivity BΠ ΠF₁G₁≡ΠF′G′
        ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ▹ G ≡ x) (PE.sym ΠF₁G₁≡ΠF′G′)
                             (≅-eq A≡B)
    in  Πₜ f (convRed:*: d ΠFG≡ΠF₁G₁) funcF (≅-conv f≡f ΠFG≡ΠF₁G₁)
           (λ {ρ} [ρ] ⊢Δ [a] [b] [a≡b] →
              let [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                           ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                  [a]₁ = convTerm₂ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                  [b]₁ = convTerm₂ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [b]
                  [a≡b]₁ = convEqTerm₂ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a≡b]
                  [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                    (PE.sym G₁≡G′))
                                           ([G] [ρ] ⊢Δ [a]₁)
                                           ([G≡G′] [ρ] ⊢Δ [a]₁)
              in  convEqTerm₁ ([G] [ρ] ⊢Δ [a]₁) ([G]₁ [ρ] ⊢Δ [a]) [G≡G₁]
                              ([f] [ρ] ⊢Δ [a]₁ [b]₁ [a≡b]₁))
          (λ {ρ} [ρ] ⊢Δ [a] →
             let [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                          ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                 [a]₁ = convTerm₂ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                 [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                   (PE.sym G₁≡G′))
                                          ([G] [ρ] ⊢Δ [a]₁)
                                          ([G≡G′] [ρ] ⊢Δ [a]₁)
             in  convTerm₁ ([G] [ρ] ⊢Δ [a]₁) ([G]₁ [ρ] ⊢Δ [a]) [G≡G₁] ([f]₁ [ρ] ⊢Δ [a]₁))
  convTermT₁ {l} {l′} {Γ} (Bᵥ BΣ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                 (Bᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
             (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
             (Σₜ f d pProd f≡f [fst] [snd]) =
    let ΣF₁G₁≡ΣF′G′   = whrDet* (red D₁ , Σₙ) (D′ , Σₙ)
        F₁≡F′ , G₁≡G′ = B-PE-injectivity BΣ ΣF₁G₁≡ΣF′G′
        ΣFG≡ΣF₁G₁ = PE.subst (λ x → Γ ⊢ Σ F ▹ G ≡ x) (PE.sym ΣF₁G₁≡ΣF′G′)
                             (≅-eq A≡B)
        ⊢Γ = wf ⊢F
        F≡F₁ = PE.subst (λ x → Γ ⊩⟨ l ⟩ wk id F ≡ wk id x / [F] Wk.id ⊢Γ)
                        (PE.sym F₁≡F′)
                        ([F≡F′] Wk.id ⊢Γ)
        [fst]₁ = convTerm₁ ([F] Wk.id ⊢Γ) ([F]₁ Wk.id (wf ⊢F₁)) F≡F₁ [fst]
        G≡G₁ = PE.subst (λ x → Γ ⊩⟨ l ⟩ wk (lift id) G [ fst f ] ≡ wk (lift id) x [ fst f ] / [G] Wk.id ⊢Γ [fst])
                        (PE.sym G₁≡G′)
                        ([G≡G′] Wk.id ⊢Γ [fst])
        [snd]₁ = convTerm₁ ([G] Wk.id ⊢Γ [fst]) ([G]₁ Wk.id (wf ⊢F₁) [fst]₁) G≡G₁ [snd]
    in  Σₜ f (convRed:*: d ΣFG≡ΣF₁G₁) pProd (≅-conv f≡f ΣFG≡ΣF₁G₁)
          [fst]₁ [snd]₁
  convTermT₁ (Uᵥ (Uᵣ .⁰ 0<1 ⊢Γ) (Uᵣ .⁰ 0<1 ⊢Γ₁)) A≡B t = t
  convTermT₁ (emb⁰¹ x) A≡B t = convTermT₁ x A≡B t
  convTermT₁ (emb¹⁰ x) A≡B t = convTermT₁ x A≡B t

  -- Helper function for conversion of terms converting from right to left.
  convTermT₂ : ∀ {l l′ Γ A B t} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
           → ShapeView Γ l l′ A B [A] [B]
           → Γ ⊩⟨ l ⟩  A ≡ B / [A]
           → Γ ⊩⟨ l′ ⟩ t ∷ B / [B]
           → Γ ⊩⟨ l ⟩  t ∷ A / [A]
  convTermT₂ (ℕᵥ D D′) A≡B t = t
  convTermT₂ (Emptyᵥ D D′) A≡B t = t
  convTermT₂ (Unitᵥ D D′) A≡B t = t
  convTermT₂ (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
             (neₜ k d (neNfₜ neK₂ ⊢k k≡k)) =
    let K₁≡K = PE.subst (λ x → _ ⊢ x ≡ _)
                        (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                        (sym (≅-eq (~-to-≅ K≡M)))
    in  neₜ k (convRed:*: d K₁≡K)
            (neNfₜ neK₂ (conv ⊢k K₁≡K) (~-conv k≡k K₁≡K))
  convTermT₂ {Γ = Γ} (Bᵥ BΠ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                            (Bᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
             (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
             (Πₜ f d funcF f≡f [f] [f]₁) =
    let ΠF₁G₁≡ΠF′G′   = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
        F₁≡F′ , G₁≡G′ = B-PE-injectivity BΠ ΠF₁G₁≡ΠF′G′
        ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ▹ G ≡ x)
                             (PE.sym ΠF₁G₁≡ΠF′G′) (≅-eq A≡B)
    in  Πₜ f (convRed:*: d (sym ΠFG≡ΠF₁G₁)) funcF (≅-conv f≡f (sym ΠFG≡ΠF₁G₁))
           (λ {ρ} [ρ] ⊢Δ [a] [b] [a≡b] →
              let [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                           ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                  [a]₁ = convTerm₁ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                  [b]₁ = convTerm₁ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [b]
                  [a≡b]₁ = convEqTerm₁ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a≡b]
                  [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                    (PE.sym G₁≡G′))
                                           ([G] [ρ] ⊢Δ [a])
                                           ([G≡G′] [ρ] ⊢Δ [a])
              in  convEqTerm₂ ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁)
                              [G≡G₁] ([f] [ρ] ⊢Δ [a]₁ [b]₁ [a≡b]₁))
           (λ {ρ} [ρ] ⊢Δ [a] →
              let [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                           ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                  [a]₁ = convTerm₁ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                  [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                    (PE.sym G₁≡G′))
                                           ([G] [ρ] ⊢Δ [a])
                                           ([G≡G′] [ρ] ⊢Δ [a])
              in  convTerm₂ ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁)
                            [G≡G₁] ([f]₁ [ρ] ⊢Δ [a]₁))
  convTermT₂ {l} {l′} {Γ = Γ} (Bᵥ BΣ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                     (Bᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
             (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
             (Σₜ f d pProd f≡f [fst]₁ [snd]₁) =
    let ΣF₁G₁≡ΣF′G′   = whrDet* (red D₁ , Σₙ) (D′ , Σₙ)
        F₁≡F′ , G₁≡G′ = B-PE-injectivity BΣ ΣF₁G₁≡ΣF′G′
        ΣFG≡ΣF₁G₁ = PE.subst (λ x → Γ ⊢ Σ F ▹ G ≡ x)
                             (PE.sym ΣF₁G₁≡ΣF′G′) (≅-eq A≡B)
        ⊢Γ = wf ⊢F
        ⊢Γ₁ = wf ⊢F₁
        F≡F₁ = PE.subst (λ x → Γ ⊩⟨ l ⟩ wk id F ≡ wk id x / [F] Wk.id ⊢Γ)
                        (PE.sym F₁≡F′)
                        ([F≡F′] Wk.id ⊢Γ)
        [fst] = (convTerm₂ ([F] Wk.id ⊢Γ) ([F]₁ Wk.id ⊢Γ₁) F≡F₁ [fst]₁)
        G≡G₁ = PE.subst (λ x → Γ ⊩⟨ l ⟩ wk (lift id) G [ fst f ] ≡ wk (lift id) x [ fst f ] / [G] Wk.id ⊢Γ [fst])
                        (PE.sym G₁≡G′)
                        ([G≡G′] Wk.id ⊢Γ [fst])
        [snd] = (convTerm₂ ([G] Wk.id ⊢Γ [fst]) ([G]₁ Wk.id ⊢Γ₁ [fst]₁) G≡G₁ [snd]₁)
    in  Σₜ f (convRed:*: d (sym ΣFG≡ΣF₁G₁)) pProd (≅-conv f≡f (sym ΣFG≡ΣF₁G₁))
           [fst] [snd]
  convTermT₂ (Uᵥ (Uᵣ .⁰ 0<1 ⊢Γ) (Uᵣ .⁰ 0<1 ⊢Γ₁)) A≡B t = t
  convTermT₂ (emb⁰¹ x) A≡B t = convTermT₂ x A≡B t
  convTermT₂ (emb¹⁰ x) A≡B t = convTermT₂ x A≡B t

  -- Conversion of terms converting from left to right.
  convTerm₁ : ∀ {Γ A B t l l′} ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
            → Γ ⊩⟨ l ⟩  A ≡ B / [A]
            → Γ ⊩⟨ l ⟩  t ∷ A / [A]
            → Γ ⊩⟨ l′ ⟩ t ∷ B / [B]
  convTerm₁ [A] [B] A≡B t = convTermT₁ (goodCases [A] [B] A≡B) A≡B t

  -- Conversion of terms converting from right to left.
  convTerm₂ : ∀ {Γ A B t l l′} ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
          → Γ ⊩⟨ l ⟩  A ≡ B / [A]
          → Γ ⊩⟨ l′ ⟩ t ∷ B / [B]
          → Γ ⊩⟨ l ⟩  t ∷ A / [A]
  -- NOTE: this would be easier to define by mutual induction with symEq (which needs conversion),
  -- rather than by defining everything from scratch for both left-to-right and right-to-left,
  -- but with the mutual definition termination checking fails in Agda.
  convTerm₂ [A] [B] A≡B t = convTermT₂ (goodCases [A] [B] A≡B) A≡B t

  -- Conversion of terms converting from right to left
  -- with some propositionally equal types.
  convTerm₂′ : ∀ {Γ A B B′ t l l′} → B PE.≡ B′
          → ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
          → Γ ⊩⟨ l ⟩  A ≡ B′ / [A]
          → Γ ⊩⟨ l′ ⟩ t ∷ B / [B]
          → Γ ⊩⟨ l ⟩  t ∷ A / [A]
  convTerm₂′ PE.refl [A] [B] A≡B t = convTerm₂ [A] [B] A≡B t

  -- Helper function for conversion of term equality converting from left to right.
  convEqTermT₁ : ∀ {l l′ Γ A B t u} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
               → ShapeView Γ l l′ A B [A] [B]
               → Γ ⊩⟨ l ⟩  A ≡ B / [A]
               → Γ ⊩⟨ l ⟩  t ≡ u ∷ A / [A]
               → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B / [B]
  convEqTermT₁ (ℕᵥ D D′) A≡B t≡u = t≡u
  convEqTermT₁ (Emptyᵥ D D′) A≡B t≡u = t≡u
  convEqTermT₁ (Unitᵥ D D′) A≡B t≡u = t≡u
  convEqTermT₁ (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
               (neₜ₌ k m d d′ (neNfₜ₌ neK₂ neM₁ k≡m)) =
    let K≡K₁ = PE.subst (λ x → _ ⊢ _ ≡ x)
                        (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                        (≅-eq (~-to-≅ K≡M))
    in  neₜ₌ k m (convRed:*: d K≡K₁)
                 (convRed:*: d′ K≡K₁)
                 (neNfₜ₌ neK₂ neM₁ (~-conv k≡m K≡K₁))
  convEqTermT₁ {Γ = Γ} (Bᵥ BΠ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                              (Bᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
               (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
               (Πₜ₌ f g d d′ funcF funcG t≡u [t] [u] [t≡u]) =
    let [A] = Bᵣ′ BΠ F G D ⊢F ⊢G A≡A [F] [G] G-ext
        [B] = Bᵣ′ BΠ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁
        [A≡B] = B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
        ΠF₁G₁≡ΠF′G′ = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
        ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ▹ G ≡ x)
                             (PE.sym ΠF₁G₁≡ΠF′G′) (≅-eq A≡B)
    in  Πₜ₌ f g (convRed:*: d ΠFG≡ΠF₁G₁) (convRed:*: d′ ΠFG≡ΠF₁G₁)
            funcF funcG (≅-conv t≡u ΠFG≡ΠF₁G₁)
            (convTerm₁ [A] [B] [A≡B] [t]) (convTerm₁ [A] [B] [A≡B] [u])
            (λ {ρ} [ρ] ⊢Δ [a] →
               let F₁≡F′ , G₁≡G′ = B-PE-injectivity BΠ (whrDet* (red D₁ , Πₙ) (D′ , Πₙ))
                   [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                            ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                   [a]₁ = convTerm₂ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                   [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                     (PE.sym G₁≡G′))
                                            ([G] [ρ] ⊢Δ [a]₁)
                                            ([G≡G′] [ρ] ⊢Δ [a]₁)
               in  convEqTerm₁ ([G] [ρ] ⊢Δ [a]₁) ([G]₁ [ρ] ⊢Δ [a])
                               [G≡G₁] ([t≡u] [ρ] ⊢Δ [a]₁))
  convEqTermT₁ {Γ = Γ} (Bᵥ BΣ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                              (Bᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
               (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
               (Σₜ₌ p r d d′ pProd rProd p≅r [t] [u] [fstp] [fstr] [fst≡] [snd≡]) =
    let [A] = Bᵣ′ BΣ F G D ⊢F ⊢G A≡A [F] [G] G-ext
        [B] = Bᵣ′ BΣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁
        [A≡B] = B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
        ΣF₁G₁≡ΣF′G′ = whrDet* (red D₁ , Σₙ) (D′ , Σₙ)
        F₁≡F′ , G₁≡G′ = B-PE-injectivity BΣ ΣF₁G₁≡ΣF′G′
        ΣFG≡ΣF₁G₁ = PE.subst (λ x → Γ ⊢ Σ F ▹ G ≡ x)
                             (PE.sym ΣF₁G₁≡ΣF′G′) (≅-eq A≡B)
        ⊢Γ = wf ⊢F
        ⊢Γ₁ = wf ⊢F₁
        F≡F₁ = PE.subst (λ x → Γ ⊩⟨ _ ⟩ wk id F ≡ wk id x / [F] Wk.id ⊢Γ)
                        (PE.sym F₁≡F′)
                        ([F≡F′] Wk.id ⊢Γ)
        [fstp]₁ = convTerm₁ ([F] Wk.id ⊢Γ) ([F]₁ Wk.id ⊢Γ₁) F≡F₁ [fstp]
        [fstr]₁ = convTerm₁ ([F] Wk.id ⊢Γ) ([F]₁ Wk.id ⊢Γ₁) F≡F₁ [fstr]
        [fst≡]₁ = convEqTerm₁ ([F] Wk.id ⊢Γ) ([F]₁ Wk.id ⊢Γ₁) F≡F₁ [fst≡]
        G≡G₁ = PE.subst (λ x → Γ ⊩⟨ _ ⟩ wk (lift id) G [ fst p ] ≡ wk (lift id) x [ fst p ] / [G] Wk.id ⊢Γ [fstp])
                        (PE.sym G₁≡G′)
                        ([G≡G′] Wk.id ⊢Γ [fstp])
        [snd≡]₁ = convEqTerm₁ ([G] Wk.id ⊢Γ [fstp]) ([G]₁ Wk.id ⊢Γ₁ [fstp]₁) G≡G₁ [snd≡]
    in  Σₜ₌ p r (convRed:*: d ΣFG≡ΣF₁G₁) (convRed:*: d′ ΣFG≡ΣF₁G₁)
            pProd rProd (≅-conv p≅r ΣFG≡ΣF₁G₁)
            (convTerm₁ [A] [B] [A≡B] [t]) (convTerm₁ [A] [B] [A≡B] [u])
            [fstp]₁ [fstr]₁ [fst≡]₁ [snd≡]₁
  convEqTermT₁ (Uᵥ (Uᵣ .⁰ 0<1 ⊢Γ) (Uᵣ .⁰ 0<1 ⊢Γ₁)) A≡B t≡u = t≡u
  convEqTermT₁ (emb⁰¹ x) A≡B t≡u = convEqTermT₁ x A≡B t≡u
  convEqTermT₁ (emb¹⁰ x) A≡B t≡u = convEqTermT₁ x A≡B t≡u

  -- Helper function for conversion of term equality converting from right to left.
  convEqTermT₂ : ∀ {l l′ Γ A B t u} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
             → ShapeView Γ l l′ A B [A] [B]
             → Γ ⊩⟨ l ⟩  A ≡ B / [A]
             → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B / [B]
             → Γ ⊩⟨ l ⟩  t ≡ u ∷ A / [A]
  convEqTermT₂ (ℕᵥ D D′) A≡B t≡u = t≡u
  convEqTermT₂ (Emptyᵥ D D′) A≡B t≡u = t≡u
  convEqTermT₂ (Unitᵥ D D′) A≡B t≡u = t≡u
  convEqTermT₂ (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
               (neₜ₌ k m d d′ (neNfₜ₌ neK₂ neM₁ k≡m)) =
    let K₁≡K = PE.subst (λ x → _ ⊢ x ≡ _)
                        (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                        (sym (≅-eq (~-to-≅ K≡M)))
    in  neₜ₌ k m (convRed:*: d K₁≡K) (convRed:*: d′ K₁≡K)
                 (neNfₜ₌ neK₂ neM₁ (~-conv k≡m K₁≡K))
  convEqTermT₂ {Γ = Γ} (Bᵥ BΠ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                              (Bᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
               (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
               (Πₜ₌ f g d d′ funcF funcG t≡u [t] [u] [t≡u]) =
    let [A] = Bᵣ′ BΠ F G D ⊢F ⊢G A≡A [F] [G] G-ext
        [B] = Bᵣ′ BΠ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁
        [A≡B] = B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
        ΠF₁G₁≡ΠF′G′ = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
        ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ▹ G ≡ x)
                             (PE.sym ΠF₁G₁≡ΠF′G′) (≅-eq A≡B)
    in  Πₜ₌ f g (convRed:*: d (sym ΠFG≡ΠF₁G₁)) (convRed:*: d′ (sym ΠFG≡ΠF₁G₁))
            funcF funcG (≅-conv t≡u (sym ΠFG≡ΠF₁G₁))
            (convTerm₂ [A] [B] [A≡B] [t]) (convTerm₂ [A] [B] [A≡B] [u])
            (λ {ρ} [ρ] ⊢Δ [a] →
               let F₁≡F′ , G₁≡G′ = B-PE-injectivity BΠ (whrDet* (red D₁ , Πₙ) (D′ , Πₙ))
                   [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                            ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                   [a]₁ = convTerm₁ ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                   [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                     (PE.sym G₁≡G′))
                                            ([G] [ρ] ⊢Δ [a])
                                            ([G≡G′] [ρ] ⊢Δ [a])
               in  convEqTerm₂ ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁)
                               [G≡G₁] ([t≡u] [ρ] ⊢Δ [a]₁))
  convEqTermT₂ {Γ = Γ} (Bᵥ BΣ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                              (Bᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
               (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
               (Σₜ₌ p r d d′ funcF funcG t≡u [t] [u] [fstp]₁ [fstr]₁ [fst≡]₁ [snd≡]₁) =
    let [A] = Bᵣ′ BΣ F G D ⊢F ⊢G A≡A [F] [G] G-ext
        [B] = Bᵣ′ BΣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁
        [A≡B] = B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
        ΣF₁G₁≡ΣF′G′ = whrDet* (red D₁ , Σₙ) (D′ , Σₙ)
        F₁≡F′ , G₁≡G′ = B-PE-injectivity BΣ ΣF₁G₁≡ΣF′G′
        ΣFG≡ΣF₁G₁ = PE.subst (λ x → Γ ⊢ Σ F ▹ G ≡ x)
                             (PE.sym ΣF₁G₁≡ΣF′G′) (≅-eq A≡B)
        ⊢Γ = wf ⊢F
        ⊢Γ₁ = wf ⊢F₁
        F≡F₁ = PE.subst (λ x → Γ ⊩⟨ _ ⟩ wk id F ≡ wk id x / [F] Wk.id ⊢Γ)
                        (PE.sym F₁≡F′)
                        ([F≡F′] Wk.id ⊢Γ)
        [fstp] = convTerm₂ ([F] Wk.id ⊢Γ) ([F]₁ Wk.id ⊢Γ₁) F≡F₁ [fstp]₁
        [fstr] = convTerm₂ ([F] Wk.id ⊢Γ) ([F]₁ Wk.id ⊢Γ₁) F≡F₁ [fstr]₁
        [fst≡] = convEqTerm₂ ([F] Wk.id ⊢Γ) ([F]₁ Wk.id ⊢Γ₁) F≡F₁ [fst≡]₁
        G≡G₁ = PE.subst (λ x → Γ ⊩⟨ _ ⟩ wk (lift id) G [ fst p ] ≡ wk (lift id) x [ fst p ] / [G] Wk.id ⊢Γ [fstp])
                        (PE.sym G₁≡G′)
                        ([G≡G′] Wk.id ⊢Γ [fstp])
        [snd≡] = convEqTerm₂ ([G] Wk.id ⊢Γ [fstp]) ([G]₁ Wk.id ⊢Γ₁ [fstp]₁) G≡G₁ [snd≡]₁
    in  Σₜ₌ p r (convRed:*: d (sym ΣFG≡ΣF₁G₁)) (convRed:*: d′ (sym ΣFG≡ΣF₁G₁))
            funcF funcG (≅-conv t≡u (sym ΣFG≡ΣF₁G₁))
            (convTerm₂ [A] [B] [A≡B] [t]) (convTerm₂ [A] [B] [A≡B] [u])
            [fstp] [fstr] [fst≡] [snd≡]
  convEqTermT₂ (Uᵥ (Uᵣ .⁰ 0<1 ⊢Γ) (Uᵣ .⁰ 0<1 ⊢Γ₁)) A≡B t≡u = t≡u
  convEqTermT₂ (emb⁰¹ x) A≡B t≡u = convEqTermT₂ x A≡B t≡u
  convEqTermT₂ (emb¹⁰ x) A≡B t≡u = convEqTermT₂ x A≡B t≡u

  -- Conversion of term equality converting from left to right.
  convEqTerm₁ : ∀ {l l′ Γ A B t u} ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
              → Γ ⊩⟨ l ⟩  A ≡ B / [A]
              → Γ ⊩⟨ l ⟩  t ≡ u ∷ A / [A]
              → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B / [B]
  convEqTerm₁ [A] [B] A≡B t≡u = convEqTermT₁ (goodCases [A] [B] A≡B) A≡B t≡u

  -- Conversion of term equality converting from right to left.
  convEqTerm₂ : ∀ {l l′ Γ A B t u} ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
            → Γ ⊩⟨ l ⟩  A ≡ B / [A]
            → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B / [B]
            → Γ ⊩⟨ l ⟩  t ≡ u ∷ A / [A]
  convEqTerm₂ [A] [B] A≡B t≡u = convEqTermT₂ (goodCases [A] [B] A≡B) A≡B t≡u


text:
module Negative4 where

data Empty : Set where

data NSPos : Set where
   c : ((NSPos -> Empty) -> NSPos) -> NSPos


text:
module Implicits.Syntax.Type.Constructors where

open import Prelude
open import Implicits.Syntax.Type
open import Implicits.Substitutions
open TypeSubst

-- polymorphic identity
tid : ∀ {n} → Type n
tid = ∀' (simpl ((TVar zero) →' (TVar zero)))

-- type of bools encoding
tbool : Type 0
tbool = ∀' (simpl ((TVar zero) →' (simpl ((TVar zero) →' (TVar zero)))))

-- church numerals
tnat : Type 0
tnat = ∀' (simpl ((simpl ((TVar zero) →' (TVar zero))) →' (simpl ((TVar zero) →' (TVar zero)))))

-- existential quantification
∃' : ∀ {n} → (Type (suc n)) → Type n
∃' a = ∀' (∀' (simpl ((a tp/tp (wk ↑)) →' (simpl ((TVar (suc zero)) →' (TVar zero))))))

-- unit type
⊤' : ∀ {n} → Type n
⊤' = tid

-- zero type
⊥' : ∀ {n} → Type n
⊥' = ∀' (TVar zero)

-- n-ary function type
infixr 7 _→ⁿ_
_→ⁿ_ : ∀ {n k} → Vec (Type n) k → Type n → Type n
[]       →ⁿ z = z
(a ∷ as) →ⁿ z = as →ⁿ (simpl (a →' z))

-- Record/finite tuple
rec : ∀ {n k} → Vec (Type n) k → Type n
rec []       = ⊤'
rec (a ∷ as) = ∀' (simpl ((map tp-weaken (a ∷ as) →ⁿ TVar zero) →' TVar zero))

-- tuple
_×'_ : ∀ {n} → Type n → Type n → Type n
a ×' b = rec (a ∷ b ∷ [])


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

module Flat where
  open import lib.Basics
  open import Basics
  open import Bool

  open import lib.types.Bool
  open import lib.NType2
  open import lib.Equivalence2
  open import lib.types.Suspension
  open import lib.types.IteratedSuspension
  open import lib.types.Pushout as Pushout
  open import lib.types.Truncation

  -- The type of points of A, ♭ A, is inductively generated by the crisp elements of A
  data ♭ {@♭ l : ULevel} (@♭ A : Type l) : Type l where
    _^♭ : A ::→ ♭ A

  -- The deduced mapping principle of ♭ A: it represents crisp functions.
  ♭-elim : {c : ULevel} {@♭ l : ULevel}{@♭ A : Type l}
         → (C : ♭ A → Type c)
         → ((@♭ u : A) → C (u ^♭))
         → (x : ♭ A) → C x
  ♭-elim C f (x ^♭) = f x
  syntax ♭-elim C (λ u → t) a = let♭ u ^♭:= a in♭ t in-family C

   {- Mike's "let" notation (following Felix) -}
   -- An implicit version of ♭-elim
  let♭ : {@♭ i j : ULevel} {@♭ A : Type i} {B : ♭ A → Type j}
         (a : ♭ A) (f : (@♭ u : A) → B (u ^♭))
         → B a
  let♭ (u ^♭) f = f u
  syntax let♭ a (λ u → t) = let♭ u ^♭:= a in♭ t

  ♭-rec : {@♭ i : ULevel} {j : ULevel} {@♭ A : Type i} {B : Type j}
                → (A ::→ B) → (♭ A) → B
  ♭-rec f (a ^♭) = f a

  ♭-rec-eq : {@♭ i : ULevel} {j : ULevel} {@♭ A : Type i} {B : Type j}
                → (A ::→ B) ≃ (♭ A → B)
  ♭-rec-eq {A = A} {B = B} =
    equiv ♭-rec
      (λ f → λ (@♭ a : A) → f (a ^♭))  -- fro
      (λ f → λ= (λ { (a ^♭) → refl })) -- to-fro
      (λ f → refl)                     -- fro-to

  -- Crisp function types, but from A : ♭ Type
  _♭:→_ : {@♭ i : ULevel} {j : ULevel} (A : ♭ (Type i)) (B : Type j) → Type (lmax i j)
  (A ^♭) ♭:→ B = A ::→ B

  -- The inclusion of the points of A into A
  _↓♭ : {@♭ i : ULevel} {@♭ A : Type i} → (♭ A → A)
  _↓♭ (x ^♭) = x

  -- The (judgemental) computation rule for mapping out of points
  ♭-β : {@♭ i : ULevel} {@♭ A : Type i} (@♭ a : ♭  A)
        → ((a ↓♭) ^♭) == a
  ♭-β (a ^♭) = refl

  -- Application of crisp functions to crisp equalities
  -- Used mostly to apply _^♭.
  ♭-ap : {@♭ i j : ULevel} {@♭ A : Type i} {B : Type j}
         (f : (@♭ a : A) → B) {@♭ x y : A} (@♭ p : x == y)
         → (f x) == (f y)
  ♭-ap f refl = refl

  -- ♭ is a functor
  ♭→ : {@♭ i j : ULevel} {@♭ A : Type i} {@♭ B : Type j}
       → (@♭ f : A → B) → (♭ A → ♭ B)
  ♭→ f (x ^♭) = (f x) ^♭

  -- The naturality square of the inclusion of points (judgemental!)
  ♭→-nat : {@♭ i j : ULevel} {@♭ A : Type i} {@♭ B : Type j} (@♭ f : A → B)
           → (a : ♭ A) → (f ∘ _↓♭) a  == (_↓♭ ∘ (♭→ f)) a
  ♭→-nat f (a ^♭) = refl

  -- Proof of functoriality
  ♭→∘ : {@♭ i j k : ULevel} {@♭ A : Type i} {@♭ B : Type j} {@♭ C : Type k}
        {@♭ f : A → B} {@♭ g : B → C}
        → ♭→ (g ∘ f) == (♭→ g) ∘ (♭→ f)
  ♭→∘ {f = f} {g = g} =
    λ= (λ a → -- We test on elements, but
          let♭ u ^♭:= a in♭ -- might as well assume those elements are crisp
            refl -- where it follows by definition.
          in-family (λ a → (♭→ (g ∘ f)) a == ((♭→ g) ∘ (♭→ f)) a)  )

  -- ♭→ preserves crisp equivalences
  ♭→e : {@♭ i j : ULevel} {@♭ A : Type i} {@♭ B : Type j}
        → (@♭ e : A ≃ B) → (♭ A) ≃ (♭ B)
  ♭→e e =
    equiv (♭→ (–> e))
          (♭→ (<– e))
          (λ { (a ^♭) → ♭-ap _^♭ (<–-inv-r e a) })
          (λ { (a ^♭) → ♭-ap _^♭ (<–-inv-l e a) })

  -- A type is discrete if the inclusion of its point is an equivalence.
  _is-discrete : {@♭ l : ULevel} → (@♭ A : Type l) → Type l
  _is-discrete {l} A = is-equiv {l} {l} {♭ A} {A} _↓♭

  -- The equivalence between the points of a discrete type and itself
  discrete-eq : {@♭ l : ULevel} {@♭ A : Type l} → A is-discrete → (♭ A) ≃ A
  discrete-eq = _↓♭ ,_

  _is-discrete-is-a-prop : {@♭ l : ULevel} (@♭ A : Type l) → (A is-discrete) is-a-prop
  A is-discrete-is-a-prop = is-equiv-is-prop

  is-discrete-prop : {@♭ l : ULevel} → SubtypeProp (♭ (Type l)) l
  is-discrete-prop = (λ { (A ^♭) → A is-discrete }) , (λ { (A ^♭) → A is-discrete-is-a-prop })

  -- The subtype of discrete types
  Discrete : (@♭ l : ULevel) → Type (lsucc l)
  Discrete l = Subtype is-discrete-prop

  Discrete-_-Type_ : (@♭ n : ℕ₋₂) (@♭ i : ULevel) → Type (lsucc i)
  Discrete- n -Type i = Subtype prop
    where prop : SubtypeProp (♭ (n -Type i)) i
          prop = (λ { (A ^♭) → (fst A) is-discrete }) , (λ { (A ^♭) → (fst A) is-discrete-is-a-prop })

  DiscSet : (@♭ i : ULevel) → Type (lsucc i)
  DiscSet i = Discrete- ⟨ S (S O) ⟩₋₂ -Type i

  DiscSet₀ = DiscSet lzero

  ∈Disc : {@♭ i : ULevel} (A : DiscSet i) → Type i
  ∈Disc A = ((♭→ ∈) (fst A)) ↓♭

  DiscSet-to-Set : {@♭ i : ULevel} → DiscSet i → hSet i
  DiscSet-to-Set A = (fst A) ↓♭

  -- DiscSet_is-discrete : {@♭ i : ULevel} → (@♭ A : DiscSet i) → (∈Disc A) is-discrete
  -- DiscSet A is-discrete = {!(snd A)!}

  -- Just in case, we apply univalence to the discrete-eq
  discrete-id : {@♭ l : ULevel} {@♭ A : Type l} → A is-discrete → (♭ A) == A
  discrete-id p = ua (discrete-eq p)

  -- Obviously, the points of a type are discrete
  ♭-is-discrete : {@♭ l : ULevel} {@♭ A : Type l} → (♭ A) is-discrete
  ♭-is-discrete {_} {A} =
                        _↓♭ is-an-equivalence-because
                           fro is-inverse-by
                             to-fro
                             and
                             fro-to
                        where
                          fro : ♭ A → ♭ (♭ A)
                          fro (a ^♭) = (a ^♭) ^♭

                          to-fro : (a : ♭ A) → ((fro a) ↓♭) == a
                          to-fro (a ^♭) = refl

                          fro-to  : (a : ♭ (♭ A)) → fro (a ↓♭) == a
                          fro-to ((a ^♭) ^♭) = refl

  -- To prove the ♭i is an equivalence, it suffices to give a section of it.
  _is-discrete-because_is-section-by_ : {@♭ l : ULevel} (@♭ A : Type l)
                        (@♭ s : A → ♭ A) (@♭ p : (a : A) → ((s a) ↓♭)== a)
                        → A is-discrete
  A is-discrete-because s is-section-by p =
      _↓♭ is-an-equivalence-because s is-inverse-by p and
        (λ { (a ^♭) → ! (♭-β (s a)) ∙ (♭-ap _^♭ (p a))})

  -- ♭ commutes with identity types in the following sense
  module _ {@♭ i : ULevel} {@♭ A : Type i} where
    ♭-identity-eq : (@♭ x y : A) → ♭ (x == y) ≃ ((x ^♭) == (y ^♭))
    ♭-identity-eq _ _ = equiv to fro to-fro fro-to
      where
        to : {@♭ x y : A} → ♭ (x == y) → ((x ^♭) == (y ^♭))
        to (refl ^♭) = refl

        fro : {@♭ x y : A} → ((x ^♭) == (y ^♭)) → ♭ (x == y)
        fro refl = refl ^♭

        to-fro : {@♭ x y : A} → (p : (x ^♭) == (y ^♭)) → (to (fro p) == p)
        to-fro refl = refl

        fro-to : {@♭ x y : A} → (p : ♭ (x == y)) → fro (to p) == p
        fro-to (refl ^♭) = refl

        {- From Tslil:
                There once was a Bear in a Zoo
                Who didn't know quite what to do
                    It bored him so
                    To walk to and fro
                So he flipped it and walked fro and to
        -}

  -- ♭ preserves crisp level.
  ♭-preserves-level : {@♭ i : ULevel} {@♭ A : Type i}
                      {@♭ n : ℕ₋₂} (@♭ p : has-level n A)
                      → has-level n (♭ A)
  ♭-preserves-level {_}{A}{⟨-2⟩} p =
    has-level-in ((a ^♭) ,
      (λ {(y ^♭) → (–> (♭-identity-eq a y)) ((contr-path p y )^♭)}))
    where -- If A contracts onto a, then ♭ A contracts onto a ^♭
      a = contr-center p
  ♭-preserves-level {_}{A}{S n}  p =
    has-level-in (λ {(x ^♭) (y ^♭) →
      equiv-preserves-level
        (♭-identity-eq x y)
        {{♭-preserves-level {_}{(x == y)}{n} (has-level-apply p x y)}}})
       {-
         Because the equality types of ♭ A are themselves ♭ (x == y) for x y : A,
         and because we know that x == y has level n if A has level (S n), we can recurse
         to show that ♭ (x == y) has level n and therefore ♭ A has level (S n).
       -}

  -- A version of ♭ that acts on n-types.
  ♭ₙ : {@♭ i : ULevel} {@♭ n : ℕ₋₂}
       → (@♭ A : n -Type i) → (n -Type i)
  ♭ₙ A = (♭ (fst A)) , ♭-preserves-level (snd A)

  ♭-Trunc-map : {@♭ i : ULevel} {@♭ n : ℕ₋₂} (@♭ X : Type i)
             → (Trunc n (♭ X)) → ♭ (Trunc n X)
  ♭-Trunc-map X =
    Trunc-elim {{p = ♭-preserves-level Trunc-level}}
      (λ { (a ^♭) → [ a ] ^♭ })

  -- Until ♯ works we have to postulate this.
  ♭-Trunc-eq : {@♭ i : ULevel} {@♭ n : ℕ₋₂} (@♭ X : Type i)
             → (Trunc n (♭ X)) ≃ ♭ (Trunc n X)
  ♭-Trunc-eq X = (♭-Trunc-map X) , unproven
    where
      postulate unproven : (♭-Trunc-map X) is-an-equiv

  ⊤-is-discrete : ⊤ is-discrete
  ⊤-is-discrete = _↓♭ is-an-equivalence-because
                         (λ {unit → unit ^♭}) is-inverse-by
                           (λ {unit → refl})
                           and
                           (λ {(unit ^♭) → refl})

  -- ♭ commutes with coproducts.
  ♭-commutes-with-⊔ : {@♭ i j : ULevel} {@♭ A : Type i} {@♭ B : Type j}
                      → ♭ (A ⊔ B) ≃ (♭ A) ⊔ (♭ B)
  ♭-commutes-with-⊔ = to ,
    (to is-an-equivalence-because
      fro is-inverse-by
        (λ { (inl (a ^♭)) → refl ;
             (inr (b ^♭)) → refl })
        and
        (λ { ((inl a) ^♭) → refl ;
             ((inr b) ^♭) → refl }))
    where
      to : {@♭ i j : ULevel} {@♭ A : Type i} {@♭ B : Type j}
           → ♭ (A ⊔ B) → (♭ A) ⊔ (♭ B)
      to ((inl a) ^♭) = inl (a ^♭)
      to ((inr b) ^♭) = inr (b ^♭)

      fro : {@♭ i j : ULevel} {@♭ A : Type i} {@♭ B : Type j}
           → (♭ A) ⊔ (♭ B) → ♭ (A ⊔ B)
      fro (inl (a ^♭)) = (inl a) ^♭
      fro (inr (b ^♭)) = (inr b) ^♭

  -- ♭ commutes with Σ types for crisp families.
  module _ {@♭ i j : ULevel} {@♭ A : Type i} {@♭ B : A → Type j} where
    ♭-commutes-with-Σ : ♭ (Σ A B) ≃ Σ (♭ A) (λ a → let♭ u ^♭:= a in♭ ♭ (B u))
    ♭-commutes-with-Σ = equiv to fro ((λ { ((a ^♭) , (b ^♭)) → refl })) ((λ { ((a , b) ^♭) → refl }))
      where
        to : ♭ (Σ A B) → Σ (♭ A) (λ a → let♭ u ^♭:= a in♭ ♭ (B u))
        to ((a , b) ^♭) = ((a ^♭) , (b ^♭))

        fro : Σ (♭ A) (λ a → let♭ u ^♭:= a in♭ ♭ (B u)) → ♭ (Σ A B)
        fro ((a ^♭) , (b ^♭)) = (a , b) ^♭

  ℕ-is-discrete : ℕ is-discrete
  ℕ-is-discrete =
    ℕ is-discrete-because fro is-section-by to-fro
    where
      fro : ℕ → ♭ ℕ
      fro O = O ^♭
      fro (S n) = (♭→ S) (fro n)

      to-fro : (n : ℕ) → ((fro n) ↓♭) == n
      to-fro O = refl
      to-fro (S n) = (fro (S n)) ↓♭
                   =⟨ ! ((♭→-nat S) (fro n)) ⟩
                     (S ∘ _↓♭) (fro n)
                   =⟨ ap S (to-fro n) ⟩
                     S n
                   =∎
        {-
          When proving this equality by induction on n, the case of 0 presents no problem,
          but when we work with (S n), we have to deal with the fact that n is not crisp.
          However, as a constructor (and therefore defined in the empty context), S is crisp.
          Therefore, we can use the naturality sqaure of ♭ to commute it past fro, and then recurse.
        -}

  -- We copy the proof for ULevel (or would but we can't pattern match on lsucc?)
  {-
  ULevel-is-discrete : ULevel is-discrete
  ULevel-is-discrete =
    ULevel is-discrete-because fro is-section-by to-fro
    where
      fro : ULevel → ♭ ULevel
      fro lzero = lzero ^♭
      fro (lsucc n) = (♭→ lsucc) (fro n)

      to-fro : (n : ULevel) → ♭i (fro n) == n
      to-fro lzero = refl
      to-fro (lsucc n) = ♭i (fro (lsucc n))
                       =⟨ ! ((♭→-nat lsucc) (fro n)) ⟩
                         (lsucc ∘ ♭i) (fro n)
                       =⟨ ap lsucc (to-fro n) ⟩
                         lsucc n
                       =∎ -}

  Bool-is-discrete : Bool is-discrete
  Bool-is-discrete = Bool is-discrete-because fro is-section-by to-fro
    where
      fro : Bool → ♭ Bool
      fro true = true ^♭
      fro false = false ^♭

      to-fro : (b : Bool) → ((fro b) ↓♭)== b
      to-fro true = refl
      to-fro false = refl

  Bool-to-♭PropT₀ : Bool → ♭ PropT₀
  Bool-to-♭PropT₀ true = True ^♭
  Bool-to-♭PropT₀ false = False ^♭

  Bool-to-♭PropT₀∘↓♭=♭→Bool-to-PropT₀ : Bool-to-♭PropT₀ ∘ _↓♭ == (♭→ Bool-to-PropT₀)
  Bool-to-♭PropT₀∘↓♭=♭→Bool-to-PropT₀ = λ= (λ { (true ^♭) → refl ; (false ^♭) → refl })

{-
  _-Sphere-is-discrete : (@♭ n : ℕ) → (Sphere n) is-discrete
  n -Sphere-is-discrete = (Sphere n) is-discrete-because
    (fro n) is-section-by {!!}
    where
      ♭-north : {@♭ n : ℕ} → ♭ (Sphere n)
      ♭-north {O} = true ^♭
      ♭-north {S n} = {!north!}

      ♭-south : {@♭ n : ℕ} → ♭ (Sphere n)
      ♭-south = {!!}

      fro : (@♭ n : ℕ) → (Sphere n) → ♭ (Sphere n)
      fro O = λ { true → true ^♭ ; false →  false ^♭ }
      fro (S n) = {!Susp-rec {A = Sphere n} {C = ♭ (Sphere (S n))} ♭-north ♭-south!}

-}

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


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

open _×_
infixr 1 _,_

_∩_ : {I : Set} → (I → Set) → (I → Set) → I → Set
P ∩ Q = λ i → P i × Q i

record Preorder : Set₁ where
  no-eta-equality
  field I : Set

infix 4 _∈_

postulate
  Ty World Cxt : Set
  All : (P : Ty → Set) → Cxt → Set
  _∈_ : Ty → World → Set

module Monotone (pre : Preorder) where
  open Preorder pre

  postulate
    Monotone : (I → Set) → Set

  instance
    postulate
      all-monotone : {Γ : Cxt} {C : Ty → I → Set}
                     ⦃ w : ∀ {ty} → Monotone (C ty) ⦄ →
                     Monotone (λ W → All (λ ty → C ty W) Γ)

module Monad (pre : Preorder) (let open Preorder pre)
             (M : (I → Set) → I → Set) where
  postulate
    _>>=_ : ∀ {P Q W} → M P W → (∀ {W'} → P W' → M Q W') → M Q W

postulate
  M   : (World → Set) → World → Set
  Val : World → Set

preorder : Preorder
preorder .Preorder.I = World

module Inner (Dummy : Set) where -- Succeeds if no Dummy

  private
    -- Succeeds if type is given
    pre : _ -- Preorder
    pre = preorder

  open Monotone pre
  open Monad pre M

  postulate
    R : World → Set

    instance
      any-monotone : ∀ {ty} → Monotone (ty ∈_)

    local : ∀ Γ {W} → R W × All (_∈ W) Γ → M Val W
    ^     : ∀ {Q : World → Set} ⦃ m : Monotone Q ⦄ → ∀ {W} → Q W → M (R ∩ Q) W

  eval-method : ∀ Γ {W} → All (_∈ W) Γ → M Val W
  eval-method Γ args =
    ^ args >>= local _ -- Succeeds if giving Γ for _

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Prelude.Vec where

open import Prelude.Nat
open import Prelude.Fin
open import Prelude.Unit
open import Prelude.List using (List ; [] ; _::_)
infixr 40 _::_

data Vec (A : Set) :  Nat -> Set where
  _::_ : forall {n} -> A -> Vec A n -> Vec A (S n)
  []   : Vec A Z

infixr 30 _++_

_++_ : {A : Set}{m n : Nat} -> Vec A m -> Vec A n -> Vec A (m + n)
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

snoc : {A : Set}{n : Nat} -> Vec A n -> A -> Vec A (S n)
snoc []        e = e :: []
snoc (x :: xs) e = x :: snoc xs e

length : {A : Set}{n : Nat} -> Vec A n -> Nat
length [] = Z
length (x :: xs) = 1 + length xs

length' : {A : Set}{n : Nat} -> Vec A n -> Nat
length' {n = n} _ = n

zipWith3 : ∀ {A B C D n} -> (A -> B -> C -> D) -> Vec A n -> Vec B n -> Vec C n -> Vec D n
zipWith3 f []        []        []        = []
zipWith3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: zipWith3 f xs ys zs

zipWith : ∀ {A B C n} -> (A -> B -> C) -> Vec A n -> Vec B n -> {u : Unit} -> Vec C n
zipWith _ [] [] = []
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys {u = unit}

_!_ : ∀ {A n} -> Vec A n -> Fin n -> A
x :: xs ! fz = x
_ :: xs ! fs n = xs ! n
[] ! ()

_[_]=_ : {A : Set}{n : Nat} -> Vec A n -> Fin n -> A -> Vec A n
(a :: as) [ fz ]= e = e :: as
(a :: as) [ fs n ]= e = a :: (as [ n ]= e)
[] [ () ]= e

map : ∀ {A B n}(f : A -> B)(xs : Vec A n) -> Vec B n
map f []        = []
map f (x :: xs) = f x :: map f xs

forgetL : {A : Set}{n : Nat} -> Vec A n -> List A
forgetL [] = []
forgetL (x :: xs) = x :: forgetL xs

rem : {A : Set}(xs : List A) -> Vec A (Prelude.List.length xs)
rem [] = []
rem (x :: xs) = x :: rem xs

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda