open import Cat.Displayed.Diagram.Total.Exponential
open import Cat.Displayed.Diagram.Total.Terminal
open import Cat.Displayed.Diagram.Total.Product
open import Cat.CartesianClosed.Free.Signature
open import Cat.Monoidal.Instances.Cartesian
open import Cat.Displayed.Instances.Slice
open import Cat.Diagram.Exponential
open import Cat.Displayed.Section
open import Cat.Functor.Kan.Nerve
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Instances.Slice
open import Cat.Displayed.Base
open import Cat.Monoidal.Base
open import Cat.Functor.Base
open import Cat.Functor.Hom
open import Cat.Cartesian
open import Cat.Morphism
open import Cat.Prelude

open import Data.Dec.Base

open import Meta.Invariant

import Cat.Instances.Presheaf.Exponentials as Pe
import Cat.Displayed.Instances.Gluing
import Cat.Instances.Presheaf.Limits as Pl
import Cat.Displayed.Reasoning
import Cat.Functor.Bifunctor as Bifunctor

open Slice-hom
open Functor
open _=>_

module Cat.CartesianClosed.Free {ℓ} (S : λ-Signature ℓ) where

Free cartesian closed categories🔗

open λ-Signature S renaming (Ob to Node ; Hom to Edge)

data Mor : Ty → Ty → Type ℓ

private variable
  τ σ ρ : Ty
  f g h : Mor τ σ

infixr  _`∘_
infixr  _`,_

We can define the free Cartesian closed category on a $\lambda$-signature $\Sigma =(T,H)$ directly as a higher inductive type. The objects of this category will be the simple types over $T\text{,}$¹ and the morphisms are generated by exactly the operations and equations which go into our definition of Cartesian closed category.

data Mor where
  `_    : ∀ {x y} → Edge x y → Mor x (` y)

  `id   : Mor σ σ
  _`∘_  : Mor σ ρ → Mor τ σ → Mor τ ρ

  `idr   : f `∘ `id ≡ f
  `idl   : `id `∘ f ≡ f
  `assoc : f `∘ (g `∘ h) ≡ (f `∘ g) `∘ h

  `!    : Mor τ `⊤
  `!-η  : (h : Mor τ `⊤) → `! ≡ h

  `π₁   : Mor (τ `× σ) τ
  `π₂   : Mor (τ `× σ) σ
  _`,_  : Mor τ σ → Mor τ ρ → Mor τ (σ `× ρ)

  `π₁β  : `π₁ `∘ (f `, g) ≡ f
  `π₂β  : `π₂ `∘ (f `, g) ≡ g
  `πη   : f ≡ (`π₁ `∘ f `, `π₂ `∘ f)

  `ev  : Mor ((τ `⇒ σ) `× τ) σ
  `ƛ   : Mor (τ `× σ) ρ → Mor τ (σ `⇒ ρ)

  `ƛβ : `ev `∘ (`ƛ f `∘ `π₁ `, `id `∘ `π₂) ≡ f
  `ƛη : f ≡ `ƛ (`ev `∘ (f `∘ `π₁ `, `id `∘ `π₂))

  squash : is-set (Mor τ σ)

instance
  H-Level-Mor : ∀ {x y n} → H-Level (Mor x y) ( + n)
  H-Level-Mor = basic-instance  squash

module _ where
  open Precategory

  Free-ccc : Precategory ℓ ℓ
  Free-ccc .Ob          = Ty
  Free-ccc .Hom         = Mor
  Free-ccc .Hom-set _ _ = squash
  Free-ccc .id          = `id
  Free-ccc ._∘_         = _`∘_
  Free-ccc .idr   _     = `idr
  Free-ccc .idl   _     = `idl
  Free-ccc .assoc _ _ _ = `assoc

  open Cartesian-closed
  open is-exponential
  open Exponential
  open is-product
  open Terminal
  open Product

  Free-products : has-products Free-ccc
  Free-products a b .apex = a `× b
  Free-products a b .π₁ = `π₁
  Free-products a b .π₂ = `π₂
  Free-products a b .has-is-product .⟨_,_⟩ f g = f `, g
  Free-products a b .has-is-product .π₁∘⟨⟩ = `π₁β
  Free-products a b .has-is-product .π₂∘⟨⟩ = `π₂β
  Free-products a b .has-is-product .unique p q = `πη ∙ ap₂ _`,_ p q

  Free-terminal : Terminal Free-ccc
  Free-terminal .top    = `⊤
  Free-terminal .has⊤ x = contr `! `!-η

  open Cartesian-category using (products ; terminal)
  Free-cartesian : Cartesian-category Free-ccc
  Free-cartesian .products = Free-products
  Free-cartesian .terminal = Free-terminal

  Free-closed : Cartesian-closed Free-ccc Free-cartesian
  Free-closed .has-exp A B .B^A = A `⇒ B
  Free-closed .has-exp A B .ev = `ev
  Free-closed .has-exp A B .has-is-exp .ƛ = `ƛ
  Free-closed .has-exp A B .has-is-exp .commutes m = `ƛβ
  Free-closed .has-exp A B .has-is-exp .unique m' x = `ƛη ∙ ap `ƛ x

private
  module Syn = Cartesian-category Free-cartesian
  module Synᵐ = Monoidal-category (Cartesian-monoidal Free-cartesian)

Instead of phrasing the universal property as a form of initiality, we’ll state induction instead. While we could derive induction from initiality, stating the “traditional” universal property for a free CCC, this has a couple of issues when it comes to working in a homotopical proof assistant.

Firstly, the categories we’re using for the normalisation proof are not strict, so we do not have a proper 1-category of models within which we could say that Free-ccc is initial. Even then, it is slightly unreasonable to expect Cartesian closed functors to preserve the structure up to identity.

We could set up a bicategory of Cartesian closed categories, functors, and natural transformations between them, but this would result in a significantly more annoying normalisation result, saying that every Morphism is isomorphic to the inclusion of a normal form.

Conversely, if we did require all the categories involved to be strict (which would require exchanging the presheaf category for something like a material set-valued presheaf category), having normal forms that live in types identical to the inputs is still not good enough, because now we either end up with a normal form that is only related to the input over a PathP, or we introduce a subst that would not compute in a useful way.

Stating an induction principle for Ty and Mor is simply a much more sensible thing to do: we do not impose a strictness condition on the categories we’re eliminating into by requiring models to live in a 1-category, and now the types guarantee that the results are definitionally talking about the input types. However, since Mor has quite a few constructors, the inputs to this induction principle are… quite gnarly. We package them up using the language of displayed categories.

First, we require a displayed category $\mathcal{D}{\mathbf{Syn}}_{\Sigma }\text{,}$ which gives us not only the motives for elimination, i.e. the types of the conclusions, but also the methods (including the equational methods) for `id and _`∘_.

module
  elim {o' ℓ'} {D : Displayed Free-ccc o' ℓ'}

Next, $\mathcal{D}$ must have total products over the Cartesian structure of ${\mathbf{Syn}}_{\Sigma }\text{.}$ In non-displayed language, this says that the total category $\int \mathcal{D}$ has products and the projection functor preserves them. But in displayed language, it says precisely that we can put together product diagrams in $\mathcal{D}$ which are displayed over product diagrams in ${\mathbf{Syn}}_{\Sigma }\text{.}$ We also ask for a total terminal object in $\mathcal{D}\text{.}$

    (cart : Cartesian-over D Free-cartesian)

This makes $\mathcal{D}$ into a Cartesian category over ${\mathbf{Syn}}_{\Sigma }\text{,}$ which in turn enables us to talk about total exponential objects in $\mathcal{D}\text{.}$ Of course, these also provide methods we’re lacking, so we must also ask for these, making $\mathcal{D}$ into a category Cartesian closed over ${\mathbf{Syn}}_{\Sigma }\text{.}$ Finally, we can ask for an interpretation $f$ of the base types in $\mathcal{D}\text{.}$

    (cco  : Cartesian-closed-over D cart Free-closed)
    (f : (x : Node) → D ʻ (` x))
  where

  open Cartesian-closed-over D cart {Free-closed} cco
  open Cat.Displayed.Reasoning D
  open Cartesian-over cart

This lets us construct a section of the objects of $\mathcal{D}\text{,}$ i.e. a method that turns any type $\tau$ into an object $S(\tau )\tau \text{.}$

  Ty-elim : (x : Ty) → D ʻ x
  Ty-elim `⊤       = top'
  Ty-elim (` x)    = f x
  Ty-elim (τ `× σ) = Ty-elim τ ⊗₀' Ty-elim σ
  Ty-elim (τ `⇒ σ) = [ Ty-elim τ , Ty-elim σ ]'

  base-method : Type _
  base-method = ∀ {x y} (e : Edge x y) → Hom[ ` e ] (Ty-elim x) (f y)

  private module _ (h : base-method) where
    go : ∀ {x y} (m : Mor x y) → Hom[ m ] (Ty-elim x) (Ty-elim y)

    go (` x)    = h x
    go `id      = id'
    go (f `∘ g) = go f ∘' go g

    go (`idr {f = f} i) = idr' (go f) i
    go (`idl {f = f} i) = idl' (go f) i
    go (`assoc {f = f} {g = g} {h = h} i) = assoc' (go f) (go g) (go h) i

    go `!         = !'
    go (`!-η e i) = !'-unique₂ {h = !'} {h' = go e} {p = `!-η e} i

    go `π₁        = π₁'
    go `π₂        = π₂'
    go (f `, g)   = ⟨ go f , go g ⟩'

    go (`π₁β {f = f} {g = g} i) = π₁∘⟨⟩' {f' = go f} {g' = go g} i
    go (`π₂β {f = f} {g = g} i) = π₂∘⟨⟩' {f' = go f} {g' = go g} i
    go `ev     = ev'
    go (`ƛ  e) = ƛ' (go e)

    go (`πη {f = f} i) = want i where
      have : PathP (λ i → Hom[ Syn.⟨⟩-unique refl refl i ] _ _) (go f) ⟨ π₁' ∘' go f , π₂' ∘' go f ⟩'
      have = ⟨⟩'-unique {other' = go f} refl refl

      want : PathP (λ i → Hom[ `πη i ] _ _) (go f) ⟨ π₁' ∘' go f , π₂' ∘' go f ⟩'
      want = cast[] have
    go (`ƛβ {f = f} i) = want i where
      want : PathP (λ i → Hom[ `ƛβ {f = f} i ] _ _) (ev' ∘' ⟨ ƛ' (go f) ∘' π₁' , id' ∘' π₂' ⟩') (go f)
      want = cast[] (commutes' (go f))
    go (`ƛη {f = f} i) = want i where
      want : PathP (λ i → Hom[ `ƛη {f = f} i ] _ _) (go f) (ƛ' (ev' ∘' ⟨ go f ∘' π₁' , id' ∘' π₂' ⟩'))
      want = cast[] (ƛ'-unique {p = refl} (go f) refl)

    go (squash x y p q i j) = is-set→squarep (λ i j → Hom[ squash x y p q i j ]-set (Ty-elim _) (Ty-elim _)) (λ i → go x) (λ i → go (p i)) (λ i → go (q i)) (λ i → go y) i j

  open Section

Induction for Free-ccc says that, if we have such a “displayed Cartesian closed category” $\mathcal{D}{\mathbf{Syn}}_{\Sigma }$ and interpretations of the base types and base terms, then $\mathcal{D}$ has a section.

  Free-ccc-elim : base-method → Section D
  Free-ccc-elim h .S₀      = Ty-elim
  Free-ccc-elim h .S₁      = go h
  Free-ccc-elim h .S-id    = refl
  Free-ccc-elim h .S-∘ f g = refl

We can recover a more traditional initiality result for Free-ccc by following the general pattern for deriving initiality from induction. Specifically, if $\mathcal{C}$ is a (non-displayed) Cartesian closed category, then the chaotic bifibration $\mathcal{C}{\mathbf{Syn}}_{\Sigma }$ provides the “generic” inputs to our induction principle, and supposing we additionally have a model of $\Sigma$ in $\mathcal{C}\text{,}$ the resulting section is exactly a Cartesian closed functor $[[-]]:{\mathbf{Syn}}_{\Sigma }\to \mathcal{C}\text{.}$ This proves weak initiality.

To prove uniqueness, supposing we have some other Cartesian closed functor $F:{\mathbf{Syn}}_{\Sigma }\to \mathcal{C}\text{,}$ we would define a category over ${\mathbf{Syn}}_{\Sigma }$ where the objects over $x$ are isomorphisms $I(x):[[x]]\cong F(x)\text{,}$ and the “morphism” over $h:{\mathbf{Syn}}_{\Sigma }(\tau ,\sigma )$ is the naturality square $I(\sigma )\circ [[h]]=F(h)\circ I(\tau )\text{.}$ Cartesian closure of $F$ would provide the data necessary for the displayed Cartesian closed structure. Then, assuming $F$ agrees with $[[-]]$ on base types and terms (i.e., it picks out the same $\Sigma \text{-model}$ in $\mathcal{C}\text{),}$ the section of $I(-)$ over objects is then a family of isomorphisms $[[x]]\cong F(x)\text{,}$ and the section over morphisms is exactly naturality for this family.

As mentioned above, without an additional assumption that $\mathcal{C}$ is also a strict category, and that $F$ preserves the Cartesian closed structure up to identity, this “pseudo”, or bicategorical initiality is the best we can do.

Intensional syntax🔗

Our objective is to prove that, if both the base types and base terms in the lambda-signature $\Sigma$ have decidable equality, then so do the objects and morphisms in ${\mathbf{Syn}}_{\Sigma }\text{.}$ As Mor is a complicated higher-inductive type, this is essentially infeasible to do ‘by hand’ by a case bash, which works for ordinary indexed inductive types because those have all disjoint constructors.

The strategy will instead be to show that Mor is equivalent to some type that we can write a case bash for. That is, we’ll write a sound normalisation procedure for Mor, which (by construction) factors through some type that has decidable equality.² Note that since Mor is a quotient, and our normalisation procedure is a function, completeness is automatic.

Factoring the construction through some intermediate type of normal forms is also necessary to actually state normalisation to begin with: soundness and completeness together imply that, if normalisation were just an endofunction on Mor, it would be the identity.

Our notion of normal form is that of the simply-typed lambda calculus. Note that despite Mor working over types, we will introduce a notion of context to be used during the proof of normalisation. The normal form of a map $m:{\mathbf{Syn}}_{\Sigma }(\tau ,\sigma )$ will then live in $x:\tau {⊢}_{\mathrm{nf}}e:\sigma \text{,}$ i.e. it will inhabit the context with a single variable typed the domain of $e\text{.}$ This is because normalisation for function types will involve renamings, and implementing this correctly is easier if binders are separate from products. Since we’re working with simple types, contexts are just lists of types. We also have the usual definition of variable as a pointer into a nonempty context.

data Cx : Type ℓ where
  ∅   : Cx
  _,_ : Cx → Ty → Cx

private variable Γ Δ Θ : Cx

data Var : Cx → Ty → Type ℓ where
  stop : Var (Γ , τ) τ
  pop  : Var Γ τ → Var (Γ , σ) τ

The type of normal forms has a unique constructor for each type,³ and the arguments are essentially unsurprising in each case: There’s nothing to a normal form of the unit type, and a normal pair is a pair of normal forms. For function types, we shift the domain into the context. At base types, the normal forms are given by neutral terms.

data Nf : Cx → Ty → Type ℓ
data Ne : Cx → Ty → Type ℓ

data Nf where
  lam  : Nf (Γ , τ) σ       → Nf Γ (τ `⇒ σ)
  pair : Nf Γ τ → Nf Γ σ    → Nf Γ (τ `× σ)
  unit :                      Nf Γ `⊤
  ne   : ∀ {x} → Ne Γ (` x) → Nf Γ (` x)

A neutral term is a variable, or an elimination form applied to another neutral. The “elimination form” for a base term is also application to a normal form in the domain. For example, we can build a neutral of type $\tau$ by projecting the first component from a neutral of type $\tau \times \sigma \text{.}$

data Ne where
  var  : Var Γ τ                     → Ne Γ τ
  app  : Ne Γ (τ `⇒ σ)      → Nf Γ τ → Ne Γ σ
  hom  : ∀ {a b} → Edge a b → Nf Γ a → Ne Γ (` b)
  fstₙ : Ne Γ (τ `× σ)               → Ne Γ τ
  sndₙ : Ne Γ (τ `× σ)               → Ne Γ σ

We summarize neutrals and normals with a selection of some of our finest “gammas and turnstiles”, eliding the translation⁴ from named variables in the context (i.e. the judgement $x:\tau \in \Gamma \text{)}$ to de Bruijn indices.

Normalisation and presheaves🔗

The key idea behind our normalisation algorithm, following Čubrić et. al. (1998), is to work in a category of presheaves over the syntax ${\mathbf{Syn}}_{\Sigma }\text{,}$ which are a model of the same $\lambda \text{-theory}$ $\Sigma \text{,}$ with the interpretation of base types (and terms) given by the Yoneda embedding $よ:{\mathbf{Syn}}_{\Sigma }\to \mathrm{PSh}({\mathbf{Syn}}_{\Sigma })\text{.}$ We thus have a (Cartesian closed) functor $[よ]:{\mathbf{Syn}}_{\Sigma }\to \mathrm{PSh}({\mathbf{Syn}}_{\Sigma })\text{,}$ arising from initiality, which is defined in terms of the Cartesian closed structure of $\mathrm{PSh}({\mathbf{Syn}}_{\Sigma })\text{,}$ i.e. we have the following (definitional) computation rules.

The elements of $[よ](\tau )$ thus do not correspond directly to morphisms in the base, but are instead a sort of $\eta \text{-long}$ interaction representation of $\lambda \text{-terms.}$ Now since the Yoneda embedding is a Cartesian closed functor, the universal property of ${\mathbf{Syn}}_{\Sigma }$ gives a natural isomorphism $よ\cong [よ]\text{.}$ Intensionally, round-tripping through this isomorphism has the effect of replacing a map by its normal form, which can be noticed because (e.g.) the elements of $[よ](\tau \times \sigma )$ are actual pairs. However, we can not observe this happening mathematically because, as mentioned above, a map and its normal form in $\mathbf{Syn}$ are identical.

We would like to factor this isomorphism through Nf above, but Nf is not readily made into a presheaf on the entire syntax. We instead pass to presheaves on a subcategory of the syntax where we can easily internalise Nf and Ne: the renamings, the smallest subcategory of ${\mathbf{Syn}}_{\Sigma }$ which is closed under precomposition by ${\pi }_1:\Gamma ,\tau \to \Gamma$ and under the functorial action $$(-\times \mathrm{id}):{\mathbf{Syn}}_{\Sigma }(\Gamma ,\Delta )\to {\mathbf{Syn}}_{\Sigma }(\Gamma \times \tau ,\Delta \times \tau )\text{,}$$ which is of course best defined as the inductive type Ren, which we use as the type of morphisms for the category Rens.

data Ren : Cx → Cx → Type ℓ where
  stop : Ren Γ Γ
  drop : Ren Γ Δ → Ren (Γ , τ) Δ
  keep : Ren Γ Δ → Ren (Γ , τ) (Δ , τ)

There is an evident embedding of ${\mathbf{Ren}}_{\Sigma }$ back into ${\mathbf{Syn}}_{\Sigma }\text{,}$ written out below, by interpreting the constructors as the aforementioned categorical constructions (and contexts by products). Moreover, this embedding is a Cartesian functor.

⟦_⟧ᶜ : Cx → Ty
⟦ ∅     ⟧ᶜ = `⊤
⟦ Γ , x ⟧ᶜ = ⟦ Γ ⟧ᶜ `× x

⟦_⟧ʳ : Ren Γ Δ → Mor ⟦ Γ ⟧ᶜ ⟦ Δ ⟧ᶜ
⟦ stop   ⟧ʳ = `id
⟦ drop r ⟧ʳ = ⟦ r ⟧ʳ `∘ `π₁
⟦ keep r ⟧ʳ = ⟦ r ⟧ʳ `∘ `π₁ `, `π₂

private
  same-cx : Cx → Cx → Prop ℓ
  same-cx ∅       ∅ = el! (Lift _ ⊤)
  same-cx ∅       _ = el! (Lift _ ⊥)
  same-cx (Γ , τ) (Δ , σ) = el! (⌞ same-cx Γ Δ ⌟ × ⌞ same-ty τ σ ⌟)
  same-cx (Γ , τ) _       = el! (Lift _ ⊥)

  from-same-cx : ∀ Γ Γ' → ⌞ same-cx Γ Γ' ⌟ → Γ ≡ Γ'
  from-same-cx ∅       ∅        p = refl
  from-same-cx (Γ , x) (Γ' , y) p = ap₂ _,_ (from-same-cx Γ Γ' (p .fst)) (from-same-ty x y (p .snd))

  refl-same-cx : ∀ Γ → ⌞ same-cx Γ Γ ⌟
  refl-same-cx ∅       = lift tt
  refl-same-cx (Γ , x) = (refl-same-cx Γ) , (refl-same-ty x)

instance
  H-Level-Cx : ∀ {n} → H-Level Cx ( + n)
  H-Level-Cx = basic-instance  $
    set-identity-system→hlevel
      (λ x y → ⌞ same-cx x y ⌟) refl-same-cx
      (λ x y → hlevel ) from-same-cx

private
  same-ren
    : ∀ {Γ' Δ'} (p : ⌞ same-cx Γ Γ' ⌟) (q : ⌞ same-cx Δ Δ' ⌟)
    → Ren Γ Δ → Ren Γ' Δ' → Prop ℓ

  same-ren p q stop stop         = el! (Lift _ ⊤)
  same-ren p q (drop x) (drop y) = same-ren (p .fst) q x y
  same-ren p q (keep x) (keep y) = same-ren (p .fst) (q .fst) x y

  same-ren p q stop (drop y)     = el! (Lift _ ⊥)
  same-ren p q stop (keep y)     = el! (Lift _ ⊥)
  same-ren p q (drop x) stop     = el! (Lift _ ⊥)
  same-ren p q (drop x) (keep y) = el! (Lift _ ⊥)
  same-ren p q (keep x) stop     = el! (Lift _ ⊥)
  same-ren p q (keep x) (drop y) = el! (Lift _ ⊥)

  from-same-ren
    : ∀ {Γ Δ Γ' Δ'} (p : ⌞ same-cx Γ Γ' ⌟) (q : ⌞ same-cx Δ Δ' ⌟) x y
    → ⌞ same-ren p q x y ⌟
    → PathP (λ i → Ren (from-same-cx Γ Γ' p i) (from-same-cx Δ Δ' q i)) x y
  from-same-ren {Γ = Γ} {Γ' = Γ'} p q stop stop α =
    is-set→cast-pathp {x = Γ , Γ} {y = Γ' , Γ'} {from-same-cx _ _ p ,ₚ _} {_ ,ₚ _}
      (uncurry Ren) (hlevel ) λ i → stop
  from-same-ren p q (drop x) (drop y) α = λ i → drop (from-same-ren _ _ x y α i)
  from-same-ren {Γ , τ} {Δ , τ} {Γ' , τ'} {Δ' , τ'} p q (keep x) (keep y) α =
    is-set→cast-pathp {x = _} {y = _} {from-same-cx _ _ (p .fst , q .snd) ,ₚ from-same-cx (Δ , τ) (Δ' , τ') q} {_ ,ₚ _}
      (uncurry Ren) (hlevel ) λ i → keep (from-same-ren _ _ x y α i)

  refl-same-ren : ∀ {Γ Δ} (x : Ren Γ Δ) → ⌞ same-ren (refl-same-cx Γ) (refl-same-cx Δ) x x ⌟
  refl-same-ren stop     = lift tt
  refl-same-ren (drop x) = refl-same-ren x
  refl-same-ren (keep x) = refl-same-ren x

  same-var : ∀ {Γ' τ'} → ⌞ same-cx Γ Γ' ⌟ → ⌞ same-ty τ τ' ⌟ → Var Γ τ → Var Γ' τ' → Prop ℓ
  same-var q p stop    stop    = el! (Lift _ ⊤)
  same-var q p stop    _       = el! (Lift _ ⊥)
  same-var q p (pop x) (pop y) = same-var (q .fst) p x y
  same-var q p (pop x) _       = el! (Lift _ ⊥)

  from-same-var
    : ∀ {Γ' τ'} (p : ⌞ same-cx Γ Γ' ⌟) (q : ⌞ same-ty τ τ' ⌟) x y
    → ⌞ same-var p q x y ⌟
    → PathP (λ i → Var (from-same-cx Γ Γ' p i) (from-same-ty τ τ' q i)) x y
  from-same-var {Γ = Γ , τ} {τ = τ} {Γ' , τ'} {τ'} p q stop    stop    α =
    subst (λ e → PathP (λ i → Var (from-same-cx Γ Γ' (p .fst) i , from-same-ty τ τ' (p .snd) i) (from-same-ty τ τ' e i)) stop stop)
      {x = p .snd} {y = q} prop!
      λ i → stop
  from-same-var p q (pop x) (pop y) α = λ i → Var.pop (from-same-var (p .fst) q x y α i)

  same-ne  : ∀ {Γ' τ'} → ⌞ same-cx Γ Γ' ⌟ → ⌞ same-ty τ τ' ⌟ → Ne  Γ τ → Ne  Γ' τ' → Prop ℓ
  same-nf  : ∀ {Γ' τ'} → ⌞ same-cx Γ Γ' ⌟ → ⌞ same-ty τ τ' ⌟ → Nf  Γ τ → Nf  Γ' τ' → Prop ℓ

  same-nf q p unit       unit       = el! (Lift _ ⊤)
  same-nf q p unit       _          = el! (Lift _ ⊥)
  same-nf q p (lam x)    (lam y)    = same-nf (q , p .fst) (p .snd) x y
  same-nf q p (lam x)    _          = el! (Lift _ ⊥)
  same-nf q p (pair a b) (pair x y) = el! (⌞ same-nf q (p .fst) a x ⌟ × ⌞ same-nf q (p .snd) b y ⌟)
  same-nf q p (pair a b) _          = el! (Lift _ ⊥)
  same-nf q p (ne x)     (ne y)     = same-ne q p x y
  same-nf q p (ne x)     _          = el! (Lift _ ⊥)

  same-ne {Γ = Γ} {τ = τ} {Γ'} {τ'} q p (var x) (var y) = same-var q p x y
  same-ne _ _ (var x)   _         = el! (Lift _ ⊥)

  same-ne {Γ = Γ} q p (app {τ = τ} f x) (app {τ = σ} g y) = el! (
    Σ[ r ∈ same-ty τ σ ] (⌞ same-ne q (r , p) f g ⌟ × ⌞ same-nf q r x y ⌟))
  same-ne _ _ (app f x) _         = el! (Lift _ ⊥)

  same-ne q p (fstₙ {σ = τ} x) (fstₙ {σ = σ} y) = el! (
    Σ[ r ∈ same-ty τ σ ] ⌞ same-ne q (p , r) x y ⌟)
  same-ne _ _ (fstₙ x)  _         = el! (Lift _ ⊥)

  same-ne q p (sndₙ {τ = τ} x) (sndₙ {τ = σ} y) = el! (
    Σ[ r ∈ same-ty τ σ ] ⌞ same-ne q (r , p) x y ⌟)
  same-ne _ _ (sndₙ x)  _         = el! (Lift _ ⊥)

  same-ne q p (hom {a = τ} x a) (hom {a = σ} y b) = el! (
    Σ[ r ∈ same-ty τ σ ]
      ( PathP (λ i → Edge (from-same-ty τ σ r i) (p i)) x y
      × ⌞ same-nf q r a b ⌟
      ))
  same-ne _ _ (hom x a) _         = el! (Lift _ ⊥)

  from-same-ne
    : ∀ {Γ' τ'} (p : ⌞ same-cx Γ Γ' ⌟) (q : ⌞ same-ty τ τ' ⌟) x y
    → ⌞ same-ne p q x y ⌟
    → PathP (λ i → Ne (from-same-cx Γ Γ' p i) (from-same-ty τ τ' q i)) x y
  from-same-nf
    : ∀ {Γ' τ'} (p : ⌞ same-cx Γ Γ' ⌟) (q : ⌞ same-ty τ τ' ⌟) x y
    → ⌞ same-nf p q x y ⌟
    → PathP (λ i → Nf (from-same-cx Γ Γ' p i) (from-same-ty τ τ' q i)) x y

  from-same-ne p q (var x)   (var y)   α = λ i → var (from-same-var _ _ x y α i)
  from-same-ne p q (app f x) (app g y) α = λ i → app (from-same-ne _ _ f g (α .snd .fst) i) (from-same-nf _ _ x y (α .snd .snd) i)
  from-same-ne p q (fstₙ x)  (fstₙ y)  α = λ i → fstₙ (from-same-ne _ _ x y (α .snd) i)
  from-same-ne p q (sndₙ x)  (sndₙ y)  α = λ i → sndₙ (from-same-ne _ _ x y (α .snd) i)
  from-same-ne p q (hom f x) (hom g y) α = λ i → hom (α .snd .fst i) (from-same-nf _ _ x y (α .snd .snd) i)

  from-same-nf p q (lam x)    (lam y)    α = λ i → lam (from-same-nf _ _ x y α i)
  from-same-nf p q (pair a b) (pair x y) α = λ i → pair (from-same-nf _ _ a x (α .fst) i) (from-same-nf _ _ b y (α .snd) i)
  from-same-nf p q unit       unit       α = λ i → unit
  from-same-nf p q (ne x)     (ne y)     α = λ i → ne (from-same-ne p q x y α i)

  refl-same-var : (v : Var Γ τ) → ⌞ same-var (refl-same-cx Γ) (refl-same-ty τ) v v ⌟
  refl-same-var stop    = lift tt
  refl-same-var (pop v) = refl-same-var v

  refl-same-ne : (v : Ne Γ τ) → ⌞ same-ne (refl-same-cx Γ) (refl-same-ty τ) v v ⌟
  refl-same-nf : (v : Nf Γ τ) → ⌞ same-nf (refl-same-cx Γ) (refl-same-ty τ) v v ⌟
  refl-same-ne (var x)            = refl-same-var x
  refl-same-ne (app  {τ = τ} v x) = refl-same-ty τ , refl-same-ne v , refl-same-nf x
  refl-same-ne (fstₙ {σ = σ} v)   = refl-same-ty σ , refl-same-ne v
  refl-same-ne (sndₙ {τ = τ} v)   = refl-same-ty τ , refl-same-ne v
  refl-same-ne (hom  {a = τ} x v) =
      refl-same-ty τ
    , is-set→cast-pathp {p = refl} {q = from-same-ty τ τ (refl-same-ty τ)} (λ e → Edge e _) (hlevel )
        refl
    , refl-same-nf v

  refl-same-nf (lam x)    = refl-same-nf x
  refl-same-nf (pair a b) = refl-same-nf a , refl-same-nf b
  refl-same-nf unit       = lift tt
  refl-same-nf (ne x)     = refl-same-ne x

  from-same-var'
    : (x y : Var Γ τ)
    → ⌞ same-var (refl-same-cx Γ) (refl-same-ty τ) x y ⌟
    → x ≡ y
  from-same-var' {Γ} {τ} x y p = is-set→cast-pathp
    {x = Γ , τ} {y = Γ , τ} {_ ,ₚ _} {refl} (uncurry Var) (hlevel )
    (from-same-var (refl-same-cx Γ) (refl-same-ty τ) x y p)

  from-same-nf'
    : (x y : Nf Γ τ)
    → ⌞ same-nf (refl-same-cx Γ) (refl-same-ty τ) x y ⌟
    → x ≡ y
  from-same-nf' {Γ} {τ} x y p = is-set→cast-pathp
    {x = Γ , τ} {y = Γ , τ} {_ ,ₚ _} {refl} (uncurry Nf) (hlevel )
    (from-same-nf (refl-same-cx Γ) (refl-same-ty τ) x y p)

  from-same-ne'
    : (x y : Ne Γ τ)
    → ⌞ same-ne (refl-same-cx Γ) (refl-same-ty τ) x y ⌟
    → x ≡ y
  from-same-ne' {Γ} {τ} x y p = is-set→cast-pathp
    {x = Γ , τ} {y = Γ , τ} {_ ,ₚ _} {refl} (uncurry Ne) (hlevel )
    (from-same-ne (refl-same-cx Γ) (refl-same-ty τ) x y p)

instance
  H-Level-Ren : ∀ {n} → H-Level (Ren Γ Δ) ( + n)
  H-Level-Ren {Γ} {Δ} = basic-instance  $
    set-identity-system→hlevel
      (λ x y → ⌞ same-ren (refl-same-cx Γ) (refl-same-cx Δ) x y ⌟)
      refl-same-ren
      (λ x y → hlevel )
      (λ x y p → is-set→cast-pathp {x = Γ , Δ} {y = Γ , Δ} {_ ,ₚ _} {refl} (uncurry Ren) (hlevel )
        (from-same-ren (refl-same-cx Γ) (refl-same-cx Δ) x y p))

  H-Level-Var : ∀ {n} → H-Level (Var Γ τ) ( + n)
  H-Level-Var {Γ} {τ} = basic-instance  $ set-identity-system→hlevel
    (λ x y → ⌞ same-var (refl-same-cx Γ) (refl-same-ty τ) x y ⌟)
    refl-same-var (λ x y → hlevel ) from-same-var'

  H-Level-Nf : ∀ {n} → H-Level (Nf Γ τ) ( + n)
  H-Level-Nf {Γ} {τ} = basic-instance  $ set-identity-system→hlevel
    (λ x y → ⌞ same-nf (refl-same-cx Γ) (refl-same-ty τ) x y ⌟)
    refl-same-nf (λ x y → hlevel ) from-same-nf'

  H-Level-Ne : ∀ {n} → H-Level (Ne Γ τ) ( + n)
  H-Level-Ne {Γ} {τ} = basic-instance  $ set-identity-system→hlevel
    (λ x y → ⌞ same-ne (refl-same-cx Γ) (refl-same-ty τ) x y ⌟)
    refl-same-ne (λ x y → hlevel ) from-same-ne'

module _ ⦃ _ : Discrete Node ⦄ ⦃ _ : ∀ {x y} → Discrete (Edge x y) ⦄ where
  private
    dec-same-ty : ∀ τ σ → Dec ⌞ same-ty τ σ ⌟
    dec-same-ty `⊤ σ with σ
    ... | `⊤      = yes (lift tt)
    ... | ` x     = no λ ()
    ... | x `× y  = no λ ()
    ... | x `⇒ y  = no λ ()
    dec-same-ty (` x) σ with σ
    ... | ` y     = auto
    ... | `⊤      = no λ ()
    ... | x `× y  = no λ ()
    ... | x `⇒ y  = no λ ()
    dec-same-ty (a `× b) σ with σ
    ... | x `× y  = Dec-× ⦃ dec-same-ty a x ⦄ ⦃ dec-same-ty b y ⦄
    ... | `⊤      = no λ ()
    ... | ` y     = no λ ()
    ... | x `⇒ y  = no λ ()
    dec-same-ty (a `⇒ b) σ with σ
    ... | x `⇒ y  = Dec-× ⦃ dec-same-ty a x ⦄ ⦃ dec-same-ty b y ⦄
    ... | `⊤      = no λ ()
    ... | ` y     = no λ ()
    ... | x `× y  = no λ ()

    dec-same-var
      : ∀ {Γ τ Γ' τ'}
      → (α : ⌞ same-cx Γ Γ' ⌟)
      → (β : ⌞ same-ty τ τ' ⌟)
      → (x : Var Γ τ) (y : Var Γ' τ') → Dec ⌞ same-var α β x y ⌟
    dec-same-var α β stop y with y
    ... | stop  = yes (lift tt)
    ... | pop _ = no λ ()
    dec-same-var α β (pop x) y with y
    ... | pop y = dec-same-var (α .fst) β x y
    ... | stop  = no λ ()

    dec-same-ne
      : ∀ {Γ τ Γ' τ'}
      → (α : ⌞ same-cx Γ Γ' ⌟)
      → (β : ⌞ same-ty τ τ' ⌟)
      → (x : Ne Γ τ) (y : Ne Γ' τ') → Dec ⌞ same-ne α β x y ⌟

    dec-same-nf
      : ∀ {Γ τ Γ' τ'}
      → (α : ⌞ same-cx Γ Γ' ⌟)
      → (β : ⌞ same-ty τ τ' ⌟)
      → (x : Nf Γ τ) (y : Nf Γ' τ') → Dec ⌞ same-nf α β x y ⌟

    dec-same-nf α β (lam x)    (lam y)    = dec-same-nf (α , β .fst) (β .snd) x y
    dec-same-nf α β (pair a b) (pair x y) = Dec-× ⦃ dec-same-nf α (β .fst) a x ⦄ ⦃ dec-same-nf α (β .snd) b y ⦄
    dec-same-nf α β unit       unit       = yes (lift tt)
    dec-same-nf α β (ne x)     (ne y)     = dec-same-ne α β x y

    dec-same-ne α β (var x) y with y
    ... | var y   = dec-same-var α β x y
    ... | app _ _ = no λ ()
    ... | fstₙ _  = no λ ()
    ... | sndₙ _  = no λ ()
    ... | hom _ _ = no λ ()
    dec-same-ne α β (app {τ = τ} f x) y with y
    ... | app {τ = σ} g y = Dec-Σ (hlevel ) (dec-same-ty τ σ) λ γ → Dec-× ⦃ dec-same-ne α (γ , β) f g ⦄ ⦃ dec-same-nf α γ x y ⦄
    ... | var _   = no λ ()
    ... | fstₙ _  = no λ ()
    ... | sndₙ _  = no λ ()
    ... | hom _ _ = no λ ()
    dec-same-ne α β (hom {a = a} f x) y with y
    ... | hom {a = b} g y = Dec-Σ (hlevel ) (dec-same-ty a b) λ γ → Dec-× ⦃ invmap to-pathp from-pathp auto ⦄ ⦃ dec-same-nf α γ x y ⦄
    ... | var _   = no λ ()
    ... | app _ _ = no λ ()
    ... | fstₙ _  = no λ ()
    ... | sndₙ _  = no λ ()
    dec-same-ne α β (fstₙ {σ = τ} x) y with y
    ... | fstₙ {σ = σ} y = Dec-Σ (hlevel ) (dec-same-ty τ σ) λ γ → dec-same-ne α (β , γ) x y
    ... | var _   = no λ ()
    ... | app _ _ = no λ ()
    ... | sndₙ _  = no λ ()
    ... | hom _ _ = no λ ()
    dec-same-ne α β (sndₙ {τ = τ} x) y with y
    ... | sndₙ {τ = σ} y = Dec-Σ (hlevel ) (dec-same-ty τ σ) λ γ → dec-same-ne α (γ , β) x y
    ... | var _   = no λ ()
    ... | app _ _ = no λ ()
    ... | fstₙ _  = no λ ()
    ... | hom _ _ = no λ ()

  instance
    Discrete-Ty : Discrete Ty
    Discrete-Ty .decide x y = invmap
      (from-same-ty x y) (λ p → subst (λ e → ⌞ same-ty x e ⌟) p (refl-same-ty x))
      (dec-same-ty x y)

    Discrete-Var : ∀ {Γ τ} → Discrete (Var Γ τ)
    Discrete-Var {Γ} {τ} .decide x y = invmap
      (from-same-var' x y)
      (λ p → subst (λ e → ⌞ same-var (refl-same-cx Γ) (refl-same-ty τ) x e ⌟) p (refl-same-var x))
      (dec-same-var (refl-same-cx Γ) (refl-same-ty τ) x y)

    Discrete-Ne  : ∀ {Γ τ} → Discrete (Ne  Γ τ)
    Discrete-Ne {Γ} {τ} .decide x y = invmap
      (from-same-ne' x y)
      (λ p → subst (λ e → ⌞ same-ne (refl-same-cx Γ) (refl-same-ty τ) x e ⌟) p (refl-same-ne x))
      (dec-same-ne (refl-same-cx Γ) (refl-same-ty τ) x y)

    Discrete-Nf  : ∀ {Γ τ} → Discrete (Nf  Γ τ)
    Discrete-Nf {Γ} {τ} .decide x y = invmap
      (from-same-nf' x y)
      (λ p → subst (λ e → ⌞ same-nf (refl-same-cx Γ) (refl-same-ty τ) x e ⌟) p (refl-same-nf x))
      (dec-same-nf (refl-same-cx Γ) (refl-same-ty τ) x y)

⟦_⟧ⁿ : Var Γ τ → Mor ⟦ Γ ⟧ᶜ τ
⟦_⟧ₙ : Nf  Γ τ → Mor ⟦ Γ ⟧ᶜ τ
⟦_⟧ₛ : Ne  Γ τ → Mor ⟦ Γ ⟧ᶜ τ

⟦ stop  ⟧ⁿ = `π₂
⟦ pop x ⟧ⁿ = ⟦ x ⟧ⁿ `∘ `π₁

⟦ lam h    ⟧ₙ = `ƛ ⟦ h ⟧ₙ
⟦ pair a b ⟧ₙ = ⟦ a ⟧ₙ `, ⟦ b ⟧ₙ
⟦ ne x     ⟧ₙ = ⟦ x ⟧ₛ
⟦ unit     ⟧ₙ = `!

⟦ var x   ⟧ₛ = ⟦ x ⟧ⁿ
⟦ app f x ⟧ₛ = `ev `∘ (⟦ f ⟧ₛ `, ⟦ x ⟧ₙ)
⟦ fstₙ h  ⟧ₛ = `π₁ `∘ ⟦ h ⟧ₛ
⟦ sndₙ h  ⟧ₛ = `π₂ `∘ ⟦ h ⟧ₛ
⟦ hom s h ⟧ₛ = (` s) `∘ ⟦ h ⟧ₙ

_∘ʳ_    : ∀ {Γ Δ Θ} → Ren Γ Δ → Ren Δ Θ → Ren Γ Θ
ren-var : ∀ {Γ Δ τ} → Ren Γ Δ → Var Δ τ → Var Γ τ
ren-ne  : ∀ {Γ Δ τ} → Ren Δ Γ → Ne  Γ τ → Ne  Δ τ
ren-nf  : ∀ {Γ Δ τ} → Ren Δ Γ → Nf  Γ τ → Nf  Δ τ

stop   ∘ʳ ρ      = ρ
drop σ ∘ʳ ρ      = drop (σ ∘ʳ ρ)
keep σ ∘ʳ stop   = keep σ
keep σ ∘ʳ drop ρ = drop (σ ∘ʳ ρ)
keep σ ∘ʳ keep ρ = keep (σ ∘ʳ ρ)

ren-var stop     v       = v
ren-var (drop σ) v       = pop (ren-var σ v)
ren-var (keep σ) stop    = stop
ren-var (keep σ) (pop v) = pop (ren-var σ v)

ren-ne σ (var v)   = var  (ren-var σ v)
ren-ne σ (app f a) = app  (ren-ne σ f) (ren-nf σ a)
ren-ne σ (fstₙ a)  = fstₙ (ren-ne σ a)
ren-ne σ (sndₙ a)  = sndₙ (ren-ne σ a)
ren-ne σ (hom s a) = hom s (ren-nf σ a)

ren-nf σ (lam n)    = lam  (ren-nf (keep σ) n)
ren-nf σ (pair a b) = pair (ren-nf σ a) (ren-nf σ b)
ren-nf σ (ne x)     = ne   (ren-ne σ x)
ren-nf σ unit       = unit

∘ʳ-idr : (ρ : Ren Δ Θ) → ρ ∘ʳ stop ≡ ρ
∘ʳ-idr stop     = refl
∘ʳ-idr (drop ρ) = ap drop (∘ʳ-idr ρ)
∘ʳ-idr (keep ρ) = refl

∘ʳ-assoc
  : ∀ {w x y z} (f : Ren y z) (g : Ren x y) (h : Ren w x)
  → ((h ∘ʳ g) ∘ʳ f) ≡ (h ∘ʳ (g ∘ʳ f))
∘ʳ-assoc f        g        stop     = refl
∘ʳ-assoc f        g        (drop h) = ap drop (∘ʳ-assoc f g h)
∘ʳ-assoc f        stop     (keep h) = refl
∘ʳ-assoc f        (drop g) (keep h) = ap drop (∘ʳ-assoc f g h)
∘ʳ-assoc stop     (keep g) (keep h) = refl
∘ʳ-assoc (drop f) (keep g) (keep h) = ap drop (∘ʳ-assoc f g h)
∘ʳ-assoc (keep f) (keep g) (keep h) = ap keep (∘ʳ-assoc f g h)

ren-⟦⟧ⁿ : (ρ : Ren Δ Γ) (v : Var Γ τ) → ⟦ ren-var ρ v ⟧ⁿ ≡ ⟦ v ⟧ⁿ `∘ ⟦ ρ ⟧ʳ
ren-⟦⟧ₛ : (ρ : Ren Δ Γ) (t : Ne Γ τ)  → ⟦ ren-ne ρ t  ⟧ₛ ≡ ⟦ t ⟧ₛ `∘ ⟦ ρ ⟧ʳ
ren-⟦⟧ₙ : (ρ : Ren Δ Γ) (t : Nf Γ τ)  → ⟦ ren-nf ρ t  ⟧ₙ ≡ ⟦ t ⟧ₙ `∘ ⟦ ρ ⟧ʳ

ren-⟦⟧ⁿ stop v           = Syn.intror refl
ren-⟦⟧ⁿ (drop ρ) v       = Syn.pushl (ren-⟦⟧ⁿ ρ v)
ren-⟦⟧ⁿ (keep ρ) stop    = sym (Syn.π₂∘⟨⟩) -- sym (Syn.π₂∘⟨⟩ ∙ Syn.idl _)
ren-⟦⟧ⁿ (keep ρ) (pop v) = Syn.pushl (ren-⟦⟧ⁿ ρ v) ∙ sym (Syn.pullr Syn.π₁∘⟨⟩)

ren-⟦⟧ₛ ρ (var x) = ren-⟦⟧ⁿ ρ x
ren-⟦⟧ₛ ρ (app f x) = ap₂ _`∘_ refl
  (ap₂ _`,_ (ren-⟦⟧ₛ ρ f) (ren-⟦⟧ₙ ρ x) ∙ sym (Syn.⟨⟩∘ _))
  ∙ Syn.pulll refl
ren-⟦⟧ₛ ρ (fstₙ t)  = Syn.pushr (ren-⟦⟧ₛ ρ t)
ren-⟦⟧ₛ ρ (sndₙ t)  = Syn.pushr (ren-⟦⟧ₛ ρ t)
ren-⟦⟧ₛ ρ (hom x a) = Syn.pushr (ren-⟦⟧ₙ ρ a)

ren-⟦⟧ₙ ρ (lam t) =
    ap `ƛ (ren-⟦⟧ₙ (keep ρ) t)
  ∙ sym (Cartesian-closed.unique Free-closed _ (ap₂ _`∘_ refl rem₁ ∙ Syn.pulll `ƛβ ∙ ap₂ _`∘_ refl (ap₂ _`,_ refl `idl)))
  where
  rem₁ : (⟦ lam t ⟧ₙ `∘ ⟦ ρ ⟧ʳ) Syn.⊗₁ `id ≡ (⟦ lam t ⟧ₙ Syn.⊗₁ `id) `∘ ⟦ ρ ⟧ʳ Syn.⊗₁ `id
  rem₁ = Bifunctor.first∘first Syn.×-functor

ren-⟦⟧ₙ ρ (pair a b) = ap₂ _`,_ (ren-⟦⟧ₙ ρ a) (ren-⟦⟧ₙ ρ b) ∙ sym (Syn.⟨⟩∘ _)
ren-⟦⟧ₙ ρ (ne x) = ren-⟦⟧ₛ ρ x
ren-⟦⟧ₙ ρ unit   = `!-η _

ren-⟦⟧ʳ : ∀ {Γ Δ Θ} (f : Ren Γ Δ) (g : Ren Δ Θ) → ⟦ f ∘ʳ g ⟧ʳ ≡ ⟦ g ⟧ʳ `∘ ⟦ f ⟧ʳ
ren-⟦⟧ʳ stop     g        = sym `idr
ren-⟦⟧ʳ (drop f) g        = Syn.pushl (ren-⟦⟧ʳ f g)
ren-⟦⟧ʳ (keep f) stop     = sym `idl
ren-⟦⟧ʳ (keep f) (drop g) = Syn.pushl (ren-⟦⟧ʳ f g) ∙ sym (Syn.pullr `π₁β)
ren-⟦⟧ʳ (keep f) (keep g) = sym (Syn.⟨⟩-unique (Syn.pulll `π₁β ∙ Syn.pullr `π₁β ∙ Syn.pulll (sym (ren-⟦⟧ʳ f g))) (Syn.pulll `π₂β ∙ `π₂β))


ren-var-∘ʳ : ∀ {Γ Δ Θ} (ρ : Ren Γ Δ) (σ : Ren Δ Θ) (x : Var Θ τ) → ren-var (ρ ∘ʳ σ) x ≡ ren-var ρ (ren-var σ x)
ren-var-∘ʳ ρ        stop     x       = ap (λ e → ren-var e x) (∘ʳ-idr ρ)
ren-var-∘ʳ stop     (drop σ) x       = refl
ren-var-∘ʳ (drop ρ) (drop σ) x       = ap pop (ren-var-∘ʳ ρ (drop σ) x)
ren-var-∘ʳ (keep ρ) (drop σ) x       = ap pop (ren-var-∘ʳ ρ σ x)
ren-var-∘ʳ stop     (keep σ) x       = refl
ren-var-∘ʳ (drop ρ) (keep σ) x       = ap pop (ren-var-∘ʳ ρ (keep σ) x)
ren-var-∘ʳ (keep ρ) (keep σ) stop    = refl
ren-var-∘ʳ (keep ρ) (keep σ) (pop x) = ap pop (ren-var-∘ʳ ρ σ x)

ren-nf-∘ʳ : ∀ {Γ Δ Θ} (ρ : Ren Γ Δ) (σ : Ren Δ Θ) (x : Nf Θ τ) → ren-nf (ρ ∘ʳ σ) x ≡ ren-nf ρ (ren-nf σ x)
ren-ne-∘ʳ : ∀ {Γ Δ Θ} (ρ : Ren Γ Δ) (σ : Ren Δ Θ) (x : Ne Θ τ) → ren-ne (ρ ∘ʳ σ) x ≡ ren-ne ρ (ren-ne σ x)

ren-nf-∘ʳ ρ σ (lam x)    = ap lam (ren-nf-∘ʳ (keep ρ) (keep σ) x)
ren-nf-∘ʳ ρ σ (pair a b) = ap₂ pair (ren-nf-∘ʳ ρ σ a) (ren-nf-∘ʳ ρ σ b)
ren-nf-∘ʳ ρ σ unit       = refl
ren-nf-∘ʳ ρ σ (ne x)     = ap ne (ren-ne-∘ʳ ρ σ x)
ren-ne-∘ʳ ρ σ (var x)    = ap var (ren-var-∘ʳ ρ σ x)
ren-ne-∘ʳ ρ σ (app f x)  = ap₂ app (ren-ne-∘ʳ ρ σ f) (ren-nf-∘ʳ ρ σ x)
ren-ne-∘ʳ ρ σ (fstₙ x)   = ap fstₙ (ren-ne-∘ʳ ρ σ x)
ren-ne-∘ʳ ρ σ (sndₙ x)   = ap sndₙ (ren-ne-∘ʳ ρ σ x)
ren-ne-∘ʳ ρ σ (hom n x)  = ap (hom n) (ren-nf-∘ʳ ρ σ x)

data Keep : Cx → Cx → Type ℓ where
  stop : Keep Γ Γ
  keep : Keep Γ Δ → Keep (Γ , τ) (Δ , τ)

keep→ren : Keep Γ Δ → Ren Γ Δ
keep→ren stop     = stop
keep→ren (keep x) = keep (keep→ren x)

keep→ctx : Keep Γ Δ → Δ ≡ Γ
keep→ctx stop     = refl
keep→ctx (keep x) = ap₂ Cx._,_ (keep→ctx x) refl

ren-var-stop : (ρ : Keep Γ Δ) (x : Var Δ τ) → PathP (λ i → Var (keep→ctx ρ (~ i)) τ) (ren-var (keep→ren ρ) x) x
ren-var-stop stop     x       = refl
ren-var-stop (keep ρ) stop    i = stop
ren-var-stop (keep ρ) (pop x) i = pop (ren-var-stop ρ x i)

ren-nf-stop  : (ρ : Keep Γ Γ) (x : Nf Γ τ) → ren-nf (keep→ren ρ) x ≡ x
ren-ne-stop  : (ρ : Keep Γ Γ) (x : Ne Γ τ) → ren-ne (keep→ren ρ) x ≡ x

ren-nf-stop ρ (lam x)    = ap lam (ren-nf-stop (keep ρ) x)
ren-nf-stop ρ (pair a b) = ap₂ pair (ren-nf-stop ρ a) (ren-nf-stop ρ b)
ren-nf-stop ρ unit       = refl
ren-nf-stop ρ (ne x)     = ap ne (ren-ne-stop ρ x)

ren-ne-stop {τ = τ} ρ (var x)    = ap var
  ( from-pathp⁻ (ren-var-stop ρ x)
  ∙∙ ap (λ e → subst (λ x → Var x τ) e x) {x = keep→ctx ρ} {y = refl} prop!
  ∙∙ transport-refl _
  )

ren-ne-stop ρ (app f x)  = ap₂ app (ren-ne-stop ρ f) (ren-nf-stop ρ x)
ren-ne-stop ρ (fstₙ x)   = ap fstₙ (ren-ne-stop ρ x)
ren-ne-stop ρ (sndₙ x)   = ap sndₙ (ren-ne-stop ρ x)
ren-ne-stop ρ (hom x n)  = ap (hom x) (ren-nf-stop ρ n)