```module Uniform.Shape
(C : Set1)
(HomC : C -> C -> Set)
(idC : (c : C) -> HomC c c)
(_∘C_ : {a b c : C} -> HomC b c -> HomC a b -> HomC a c)
where

-- Definitions and lemmas relating the shape of a uniform code

open import Data.Unit
open import Data.Empty
open import Function

import Uniform.posIR
open Uniform.posIR C HomC idC _∘C_

same-shape : {Γ Δ : Ctxt} -> IR' Γ -> IR' Δ -> Set
same-shape (ι c) (ι d) = ⊤
same-shape (ι c) (σ B ψ) = ⊥
same-shape (ι c) (δ B ψ ψ→) = ⊥
same-shape (σ A γ) (ι d) = ⊥
same-shape (σ A γ) (σ B ψ) = same-shape γ ψ
same-shape (σ A γ) (δ B ψ ψ→) = ⊥
same-shape (δ A γ γ→) (ι d) = ⊥
same-shape (δ A γ γ→) (σ B ψ) = ⊥
same-shape (δ A γ γ→) (δ B ψ ψ→) = same-shape γ ψ

refl-shape : {Γ : Ctxt} -> (γ : IR' Γ) -> same-shape γ γ
refl-shape (ι c) = _
refl-shape (σ A γ) = refl-shape γ
refl-shape (δ A γ γ→) = refl-shape γ

trans-shape : {Γ Γ' Γ'' : Ctxt} -> {γ : IR' Γ}{γ' : IR' Γ'}{γ'' : IR' Γ''} ->
same-shape γ γ' -> same-shape γ' γ'' -> same-shape γ γ''
trans-shape {γ = ι c} {ι d} {ι e} _ _ = tt
trans-shape {γ = ι c} {ι d} {σ C γ''} p ()
trans-shape {γ = ι c} {ι d} {δ V γ'' γ''→} p ()
trans-shape {γ = ι c} {σ B γ'} () q
trans-shape {γ = ι c} {δ B γ' γ'→} () q
trans-shape {γ = σ A γ} {ι d} () q
trans-shape {γ = σ A γ} {σ B γ'} {ι e} p ()
trans-shape {γ = σ A γ} {σ B γ'} {σ C γ''} p q = trans-shape {γ = γ} p q
trans-shape {γ = σ A γ} {σ B γ'} {δ C γ'' γ''→} p ()
trans-shape {γ = σ A γ} {δ B γ' γ'→} () q
trans-shape {γ = δ A γ γ→} {ι d} () q
trans-shape {γ = δ A γ γ→} {σ B γ'} () q
trans-shape {γ = δ A γ γ→} {δ B γ' γ'→} {ι e} p ()
trans-shape {γ = δ A γ γ→} {δ B γ' γ'→} {σ C γ''} p ()
trans-shape {γ = δ A γ γ→} {δ B γ' γ'→} {δ C γ'' γ''→} p q
= trans-shape {γ = γ} p q

sym-shape : {Γ Δ : Ctxt} -> {γ : IR' Γ}{ψ : IR' Δ} ->
same-shape γ ψ -> same-shape ψ γ
sym-shape {γ = ι c} {ι d} _ = tt
sym-shape {γ = ι c} {σ B ψ} ()
sym-shape {γ = ι c} {δ B ψ ψ→} ()
sym-shape {γ = σ A γ} {ι d} ()
sym-shape {γ = σ A γ} {σ B ψ} p = sym-shape {γ = γ} p
sym-shape {γ = σ A γ} {δ B ψ ψ→} ()
sym-shape {γ = δ A γ γ→} {ι d} ()
sym-shape {γ = δ A γ γ→} {σ B ψ} ()
sym-shape {γ = δ A γ γ→} {δ B ψ ψ→} p = sym-shape {γ = γ} p

IRcMor-preserves-shape : ∀ {Γ Δ Γ' Δ'} ->
{f : Env Γ -> Env Δ}{f' : Env Γ' -> Env Δ'} ->
(γ : IR' Δ) -> (γ' : IR' Δ') ->
same-shape γ γ' ->
same-shape {Γ} {Γ'} (IRcMor f γ) (IRcMor f' γ')
IRcMor-preserves-shape (ι c) (ι d) p = p
IRcMor-preserves-shape (ι c) (σ B ψ) ()
IRcMor-preserves-shape (ι c) (δ B ψ ψ→) ()
IRcMor-preserves-shape (σ A γ) (ι d) ()
IRcMor-preserves-shape (σ A γ) (σ B ψ) p = IRcMor-preserves-shape γ ψ p
IRcMor-preserves-shape (σ A γ) (δ B ψ ψ→) ()
IRcMor-preserves-shape (δ A γ γ→) (ι d) ()
IRcMor-preserves-shape (δ A γ γ→) (σ B ψ) ()
IRcMor-preserves-shape (δ A γ γ→) (δ B ψ ψ→) p = IRcMor-preserves-shape γ ψ p

IRcMor-same-shape : ∀ {Γ Δ} ->
{f : Env Γ -> Env Δ}
(γ : IR' Δ) ->
same-shape {Δ} {Γ} γ (IRcMor f γ)
IRcMor-same-shape (ι c) = tt
IRcMor-same-shape (σ A γ) = IRcMor-same-shape γ
IRcMor-same-shape (δ A γ γ→) = IRcMor-same-shape γ

mutual
pad₀ : {Γ Δ : Ctxt} -> IR' Γ -> IR' Δ -> IR' Γ
pad₀ (ι c) (ι d) = ι c
pad₀ (ι c) (σ B ψ) = σ (λ _ → ⊤) (pad₀ (IRwkσ (ι c)) ψ)
pad₀ (ι c) (δ B ψ ψ→)
= δ (λ _ → ⊥) (pad₀ (IRwkδ (ι c)) ψ)
(λ _ → pad₀-mor  {ψ = ψ} (ι→ι (idC _)))
pad₀ {Γ} {Δ} (σ A γ) (ι d) = σ A (pad₀ {Γ ,σ A} {Δ} γ (ι d))
pad₀ (σ A γ) (σ B ψ) = σ A (pad₀ γ ψ)
pad₀ (σ A γ) (δ B ψ ψ→) = σ A  (pad₀ γ (δ B ψ ψ→))
pad₀ {Γ} {Δ} (δ A γ γ→) (ι d)
= δ A (pad₀ {Γ ,δ A} {Δ} γ (ι d)) (pad₀-mor ∘ γ→)
pad₀ (δ A γ γ→) (σ B ψ) = δ A (pad₀ γ (σ B ψ)) (pad₀-mor ∘ γ→)
pad₀ (δ A γ γ→) (δ B ψ ψ→) = δ A (pad₀ γ ψ) (pad₀-mor ∘ γ→)

pad₀-mor : {Γ Γ' Δ : Ctxt} ->
{γ : IR' Γ}{γ' : IR' Γ'}{ψ : IR' Δ}
{e : Env Γ}{e' : Env Γ'} ->
Hom' e e' γ γ' ->
pad₀-mor {ψ = ι c'} (ι→ι f) = ι→ι f
pad₀-mor {ψ = ι c'} (σ→σ f g) = σ→σ f (pad₀-mor ∘ g)
pad₀-mor {ψ = ι c'} (δ→δ f g) = δ→δ f (pad₀-mor ∘ g)
pad₀-mor {ψ = σ B ψ} (ι→ι f) = σ→σ id (λ _ → pad₀-mor {ψ = ψ} (ι→ι f))
pad₀-mor {ψ = σ B ψ} (σ→σ f g) = σ→σ f (pad₀-mor ∘ g)
pad₀-mor {ψ = σ B ψ} (δ→δ f g) = δ→δ f (pad₀-mor ∘ g)
pad₀-mor {ψ = δ B ψ ψ→} (ι→ι f) = δ→δ id (λ _ → pad₀-mor {ψ = ψ} (ι→ι f))
pad₀-mor {ψ = δ B ψ ψ→} (σ→σ f g) = σ→σ f (pad₀-mor ∘ g)
pad₀-mor {ψ = δ B ψ ψ→} (δ→δ f g) = δ→δ f (pad₀-mor ∘ g)

mutual

pad₁ : {Γ Δ : Ctxt} -> IR' Γ -> IR' Δ -> IR' Δ
pad₁ (ι c) (ι d) = ι d
pad₁ {Γ} {Δ} (ι c) (σ B ψ) = σ B (pad₁ {Γ} (ι c) ψ)
pad₁ {Γ} {Δ} (ι c) (δ B ψ ψ→)
= δ B (pad₁ {Γ} {Δ ,δ B} (ι c) ψ) (pad₁-mor {γ = ι c} ∘ ψ→)
pad₁ (σ A γ) (ι d) = σ (λ _ → ⊤) (pad₁ γ (IRwkσ (ι d)))
pad₁ (σ A γ) (σ B ψ) = σ B (pad₁ γ ψ)
pad₁ (σ A γ) (δ B ψ ψ→) = σ (λ _ → ⊤) (pad₁ γ (IRwkσ (δ B ψ ψ→)))
pad₁ (δ A γ γ→) (ι d)
= δ (λ _ → ⊥) (pad₁ γ (IRwkδ (ι d)))
(λ _ → pad₁-mor {γ = γ} (ι→ι (idC _)))
pad₁ (δ A γ γ→) (σ B ψ)
= δ (λ _ → ⊥) (pad₁ γ (IRwkδ (σ B ψ)))
(λ _ → pad₁-mor {γ = γ} (HomcMor _ _ (idIR' (σ B ψ))))
pad₁ (δ A γ γ→) (δ B ψ ψ→) = δ B (pad₁ γ ψ) (pad₁-mor {γ = γ} ∘ ψ→)

pad₁-mor : {Γ Δ Δ' : Ctxt} ->
{γ : IR' Γ}{ψ : IR' Δ}{ψ' : IR' Δ'}
{e : Env Δ}{e' : Env Δ'} ->
Hom' e e' ψ ψ' ->
pad₁-mor {γ = ι c} (ι→ι f) = ι→ι f
pad₁-mor {γ = ι c} (σ→σ f g) = σ→σ f (pad₁-mor {γ = ι c} ∘ g)
pad₁-mor {γ = ι c} (δ→δ f g) = δ→δ f (pad₁-mor {γ = ι c} ∘ g)
pad₁-mor {γ = σ A γ} (ι→ι f) = σ→σ id (λ _ → pad₁-mor {γ = γ} (ι→ι f))
pad₁-mor {γ = σ A γ} (σ→σ f g) = σ→σ f (pad₁-mor {γ = γ} ∘ g)
pad₁-mor {γ = σ A γ} (δ→δ f g)
= σ→σ id (λ _ → pad₁-mor {γ = γ} (δ→δ f (HomcMor _ _ ∘ g)))
pad₁-mor {γ = δ A γ γ→} (ι→ι f) = δ→δ id (λ _ → pad₁-mor {γ = γ} (ι→ι f))
pad₁-mor {γ = δ A γ γ→} (σ→σ f g)
= δ→δ id (λ _ → pad₁-mor {γ = γ} (HomcMor _ _ (σ→σ f g)))
pad₁-mor {γ = δ A γ γ→} (δ→δ f g) = δ→δ f (pad₁-mor {γ = γ} ∘ g)

pad₀-preserves-shape :  {Γ Γ' Δ : Ctxt} ->
(γ : IR' Γ) -> (γ' : IR' Γ') -> (ψ : IR' Δ) ->
pad₀-preserves-shape (ι c) (ι d) (ι e) _ = tt
pad₀-preserves-shape (ι c) (ι d) (σ C ψ) _
= pad₀-preserves-shape (IRwkσ (ι c)) (IRwkσ (ι d)) ψ tt
pad₀-preserves-shape (ι c) (ι d) (δ C ψ ψ→) _
=  pad₀-preserves-shape (IRwkδ (ι c)) (IRwkδ (ι d)) ψ tt
pad₀-preserves-shape (ι c) (σ B γ') ψ ()
pad₀-preserves-shape (ι c) (δ B γ' γ'→) ψ ()
pad₀-preserves-shape (σ A γ) (ι d) ψ ()
pad₀-preserves-shape (σ A γ) (σ B γ') (ι e) p = pad₀-preserves-shape γ γ' _ p
pad₀-preserves-shape (σ A γ) (σ B γ') (σ C ψ) p = pad₀-preserves-shape γ γ' _ p
pad₀-preserves-shape (σ A γ) (σ B γ') (δ C ψ ψ→) p
= pad₀-preserves-shape γ γ' _ p
pad₀-preserves-shape (σ A γ) (δ B γ' γ'→) ψ ()
pad₀-preserves-shape (δ A γ γ→) (ι d) ψ ()
pad₀-preserves-shape (δ A γ γ→) (σ B γ') ψ ()
pad₀-preserves-shape (δ A γ γ→) (δ B γ' γ'→) (ι e) p
= pad₀-preserves-shape γ γ' _ p
pad₀-preserves-shape (δ A γ γ→) (δ B γ' γ'→) (σ C ψ) p
= pad₀-preserves-shape γ γ' _ p
pad₀-preserves-shape (δ A γ γ→) (δ B γ' γ'→) (δ C ψ ψ→) p
= pad₀-preserves-shape γ γ' _ p

pad₁-preserves-shape :  {Γ Δ Δ' : Ctxt} ->
(γ : IR' Γ) -> (ψ : IR' Δ) -> (ψ' : IR' Δ') ->
pad₁-preserves-shape (ι c) (ι d) (ι e) _ = tt
pad₁-preserves-shape (σ A γ) (ι d) (ι e) p = pad₁-preserves-shape γ _ _ p
pad₁-preserves-shape (δ A γ γ→) (ι d) (ι e) p = pad₁-preserves-shape γ _ _ p
pad₁-preserves-shape γ (ι d) (σ C ψ') ()
pad₁-preserves-shape γ (ι d) (δ C ψ' ψ'→) ()
pad₁-preserves-shape γ (σ B ψ) (ι e) ()
pad₁-preserves-shape (ι c) (σ B ψ) (σ C ψ') p
= pad₁-preserves-shape (ι c) ψ ψ' p
pad₁-preserves-shape (σ A γ) (σ B ψ) (σ C ψ') p = pad₁-preserves-shape γ ψ ψ' p
pad₁-preserves-shape (δ A γ γ→) (σ B ψ) (σ C ψ') p
= pad₁-preserves-shape γ _ _ (IRcMor-preserves-shape ψ ψ' p)
pad₁-preserves-shape γ (σ B ψ) (δ C ψ' ψ'→) ()
pad₁-preserves-shape γ (δ B ψ ψ→) (ι e) ()
pad₁-preserves-shape γ (δ B ψ ψ→) (σ C ψ') ()
pad₁-preserves-shape (ι c) (δ B ψ ψ→) (δ C₁ ψ' ψ'→) p
= pad₁-preserves-shape (ι c) ψ ψ' p
pad₁-preserves-shape (σ A γ) (δ B ψ ψ→) (δ C₁ ψ' ψ'→) p
= pad₁-preserves-shape γ _ _ (IRcMor-preserves-shape ψ ψ' p)
pad₁-preserves-shape (δ A γ γ→) (δ B ψ ψ→) (δ C₁ ψ' ψ'→) p
= pad₁-preserves-shape γ ψ ψ' p

padded-same-shape : {Γ Δ : Ctxt} -> (γ : IR' Γ) -> (ψ : IR' Δ) ->
padded-same-shape (ι c) (ι d) = tt
padded-same-shape (ι c) (σ B ψ)
= trans-shape {γ = pad₀ (IRwkσ (ι c)) ψ}
(pad₀-preserves-shape (IRwkσ (ι c)) (ι c) ψ tt)
padded-same-shape (ι c) (δ B ψ ψ→)
= trans-shape {γ = pad₀ (IRwkδ (ι c)) ψ}
(pad₀-preserves-shape (IRwkδ (ι c)) (ι c) ψ tt)
padded-same-shape (σ A γ) (ι d)
= trans-shape {γ = pad₀ γ (ι d)}
(pad₁-preserves-shape γ (ι d) (IRwkσ (ι d)) tt)
padded-same-shape (σ A γ) (δ B ψ ψ→)
= trans-shape {γ = pad₀ γ (δ B ψ ψ→)}
(padded-same-shape γ (δ B ψ ψ→))
(pad₁-preserves-shape γ (δ B ψ ψ→) (IRwkσ (δ B ψ ψ→))
(IRcMor-same-shape ψ))
padded-same-shape (δ A γ γ→) (ι d)
= trans-shape {γ = pad₀ γ (ι d)}
(pad₁-preserves-shape γ (ι d) (IRwkδ (ι d)) tt)
padded-same-shape (δ A γ γ→) (σ B ψ)
= trans-shape {γ = pad₀ γ (σ B ψ)}
(pad₁-preserves-shape γ _ _ (IRcMor-same-shape ψ))
padded-same-shape (δ A γ γ→) (δ B ψ ψ→) = padded-same-shape γ ψ

same-ctxt-shape : Ctxt -> Ctxt -> Set
same-ctxt-shape [] [] = ⊤
same-ctxt-shape [] (Δ ,σ B) = ⊥
same-ctxt-shape [] (Δ ,δ B) = ⊥
same-ctxt-shape (Γ ,σ A) [] = ⊥
same-ctxt-shape (Γ ,σ A) (Δ ,σ B) = same-ctxt-shape Γ Δ
same-ctxt-shape (Γ ,σ A) (Δ ,δ B) = ⊥
same-ctxt-shape (Γ ,δ A) [] = ⊥
same-ctxt-shape (Γ ,δ A) (Δ ,σ B) = ⊥
same-ctxt-shape (Γ ,δ A) (Δ ,δ B) = same-ctxt-shape Γ Δ

```