module Uniform.Constructions.Coproduct
  (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

-- This file can take a while to type check

open import Data.Empty
open import Data.Unit
open import Data.Product as P
open import Data.Sum as S
open import Function
open import Data.Bool
open import Data.Nat

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Prelude.Equality

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

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

mutual
  plus : {Γ Δ : Ctxt} -> (γ : IR' Γ) -> (ψ : IR' Δ) -> same-shape γ ψ ->
         (q : same-ctxt-shape Γ Δ) -> IR' (Bool, Γ Δ q)
  plus {Γ} {Δ} (ι c) (ι d) p q = ι c|d
    where c|d : Env (Bool, Γ Δ q) -> C
          c|d = ((λ x → Bool-elim (λ z → Env (if z then Γ else Δ) -> C) c d (proj₁ x) (proj₂ x)) ∘′ EnvBool, Γ Δ q)
  plus {Γ} {Δ} (σ A γ) (σ B ψ) p q = σ A|B (plus γ ψ p q)
    where A|B : Env (Bool, Γ Δ q) -> Set
          A|B = (λ x → Bool-elim (λ z → Env (if z then Γ else Δ) → Set)
                                  A B (proj₁ x) (proj₂ x)) ∘′ EnvBool, Γ Δ q
  plus {Γ} {Δ} (δ A γ γ→) (δ B ψ ψ→) p q = δ A|B (plus γ ψ p q) (λ {e} {f} {g} η → plus-mor q q γ γ ψ ψ p p (rec-call e η))
    where A|B : Env (Bool, Γ Δ q) -> Set
          A|B = (λ x → Bool-elim (λ z → Env (if z then Γ else Δ) → Set)
                                  A B (proj₁ x) (proj₂ x)) ∘′ EnvBool, Γ Δ q
          rec-call : (e : Env (Bool, Γ Δ q)) -> {f g : A|B e -> C} ->
                (η : (a : A|B e) -> HomC (f a) (g a)) ->
                Hom' (proj₂ (EnvBool, (Γ ,δ A) (Δ ,δ B) q (e , f))) (proj₂ (EnvBool, (Γ ,δ A) (Δ ,δ B) q (e , g))) (Bool-elim (λ z → IR' (if z then Γ ,δ A else Δ ,δ B)) γ ψ (proj₁ (EnvBool, (Γ ,δ A) (Δ ,δ B) q (e , f)))) (Bool-elim (λ z → IR' (if z then Γ ,δ A else Δ ,δ B)) γ ψ (proj₁ (EnvBool, (Γ ,δ A) (Δ ,δ B) q (e , g))))
          rec-call e η with EnvBool, Γ Δ q e
          rec-call e η | true , w = γ→ η
          rec-call e η | false , w = ψ→ η
  plus (ι c) (σ B ψ) () q 
  plus (ι c) (δ B ψ ψ→) () q
  plus (σ A γ) (ι d) () q
  plus (σ A γ) (δ B ψ ψ→) () q
  plus (δ A γ γ→) (ι d) () q
  plus (δ A γ γ→) (σ B ψ) () q

  plus-mor : {Γ Γ' Δ Δ' : Ctxt} ->
             (q : same-ctxt-shape Γ Δ)(q' : same-ctxt-shape Γ' Δ')
             {e : Env (Bool, Γ Δ q)}{e' : Env (Bool, Γ' Δ' q')} ->
             (γ : IR' Γ )(γ' : IR' Γ') ->
             (ψ : IR' Δ)(ψ' : IR' Δ') ->
             (p : same-shape γ ψ)  -> 
             (p' : same-shape γ' ψ') ->  
             let funs : Env (Bool, Γ Δ q) × Env (Bool, Γ' Δ' q') -> Set1
                 funs = (λ (x : (Σ[ v ∈ Bool ] Env (if v then Γ else Δ)) × (Σ[ v ∈ Bool ] Env (if v then Γ' else Δ')))
                             → let
                                  xb = proj₁ (proj₁ x)
                                  xe = proj₂ (proj₁ x)
                                  yb = proj₁ (proj₂ x)
                                  ye = proj₂ (proj₂ x)
                                in Hom' {if xb then Γ else Δ} {if yb then Γ' else Δ'} xe ye (Bool-elim (λ z → IR' (if z then Γ else Δ)) γ ψ xb) (Bool-elim (λ z → IR' (if z then Γ' else Δ')) γ' ψ' yb)) ∘′ (P.map (EnvBool, Γ Δ q) (EnvBool, Γ' Δ' q'))
             in
             funs (e , e') ->
             Hom' e e' (plus γ ψ p q) (plus γ' ψ' p' q')

  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (ι c) (ι c') (ι d) (ι d') p p' f
    with EnvBool, Γ Δ q e | EnvBool, Γ' Δ' q' e'
       | inspect (EnvBool, Γ Δ q) e | inspect (EnvBool, Γ' Δ' q') e'    
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'} (ι c) (ι c') (ι d) (ι d') p p'
           (ι→ι f) | true , w | true , w' | [ eq ] | [ eq' ]
    = ι→ι (subst₂ (λ w q → HomC (Bool-elim (λ z → Env (if z then Γ else Δ) → C) c d (proj₁ w) (proj₂ w)) (Bool-elim (λ z → Env (if z then Γ' else Δ') → C) c' d' (proj₁ q) (proj₂ q))) (sym eq) (sym eq') f)
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'} (ι c) (ι c') (ι d) (ι d') p p'
           (ι→ι f) | true , w | false , w' | [ eq ] | [ eq' ]
    = ι→ι (subst₂ (λ w q → HomC (Bool-elim (λ z → Env (if z then Γ else Δ) → C) c d (proj₁ w) (proj₂ w)) (Bool-elim (λ z → Env (if z then Γ' else Δ') → C) c' d' (proj₁ q) (proj₂ q))) (sym eq) (sym eq') f)
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'} (ι c) (ι c') (ι d) (ι d') p p'
           (ι→ι f) | false , w | true , w' | [ eq ] | [ eq' ]
    = ι→ι (subst₂ (λ w q → HomC (Bool-elim (λ z → Env (if z then Γ else Δ) → C) c d (proj₁ w) (proj₂ w)) (Bool-elim (λ z → Env (if z then Γ' else Δ') → C) c' d' (proj₁ q) (proj₂ q))) (sym eq) (sym eq') f)
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'} (ι c) (ι c') (ι d) (ι d') p p'
           (ι→ι f) | false , w | false , w' | [ eq ] | [ eq' ]
    = ι→ι (subst₂ (λ w q → HomC (Bool-elim (λ z → Env (if z then Γ else Δ) → C) c d (proj₁ w) (proj₂ w)) (Bool-elim (λ z → Env (if z then Γ' else Δ') → C) c' d' (proj₁ q) (proj₂ q))) (sym eq) (sym eq') f)

  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (σ A γ) (σ A' γ') (σ B ψ) (σ B' ψ') p p' f
    with EnvBool, Γ Δ q e | EnvBool, Γ' Δ' q' e'
       | inspect (EnvBool, Γ Δ q) e | inspect (EnvBool, Γ' Δ' q') e'    
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (σ A γ) (σ A' γ') (σ B ψ) (σ B' ψ') p p'
           (σ→σ f g) | true , w | true , w' | [ eq ] | [ eq' ]
      = σ→σ (proj₁ f,plusmor∘g') (proj₂ f,plusmor∘g')
          where f,plusmor∘g' = auxσ-tt-tt f g (proj₁ (EnvBool, Γ Δ q e))
                                              (proj₂ (EnvBool, Γ Δ q e))
                                              refl
                                              (proj₁ (EnvBool, Γ' Δ' q' e'))
                                              (proj₂ (EnvBool, Γ' Δ' q' e'))
                                              refl
                                              (≡-fst eq) (≡-snd eq)
                                              (≡-fst eq') (≡-snd eq')
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (σ A γ) (σ A' γ') (σ B ψ) (σ B' ψ') p p'
           (σ→σ f g) | true , w | false , w' | [ eq ] | [ eq' ]
      = σ→σ (proj₁ f,plusmor∘g') (proj₂ f,plusmor∘g')
          where f,plusmor∘g' = auxσ-tt-ff f g (proj₁ (EnvBool, Γ Δ q e))
                                              (proj₂ (EnvBool, Γ Δ q e))
                                              refl
                                              (proj₁ (EnvBool, Γ' Δ' q' e'))
                                              (proj₂ (EnvBool, Γ' Δ' q' e'))
                                              refl
                                              (≡-fst eq) (≡-snd eq)
                                              (≡-fst eq') (≡-snd eq')
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (σ A γ) (σ A' γ') (σ B ψ) (σ B' ψ') p p'
           (σ→σ f g) | false , w | true , w' | [ eq ] | [ eq' ]
      = σ→σ (proj₁ f,plusmor∘g') (proj₂ f,plusmor∘g')
          where f,plusmor∘g' = auxσ-ff-tt f g (proj₁ (EnvBool, Γ Δ q e))
                                              (proj₂ (EnvBool, Γ Δ q e))
                                              refl
                                              (proj₁ (EnvBool, Γ' Δ' q' e'))
                                              (proj₂ (EnvBool, Γ' Δ' q' e'))
                                              refl
                                              (≡-fst eq) (≡-snd eq)
                                              (≡-fst eq') (≡-snd eq')
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (σ A γ) (σ A' γ') (σ B ψ) (σ B' ψ') p p'
           (σ→σ f g) | false , w | false , w' | [ eq ] | [ eq' ]
      = σ→σ (proj₁ f,plusmor∘g') (proj₂ f,plusmor∘g')
          where f,plusmor∘g' = auxσ-ff-ff f g (proj₁ (EnvBool, Γ Δ q e))
                                              (proj₂ (EnvBool, Γ Δ q e))
                                              refl
                                              (proj₁ (EnvBool, Γ' Δ' q' e'))
                                              (proj₂ (EnvBool, Γ' Δ' q' e'))
                                              refl
                                              (≡-fst eq) (≡-snd eq)
                                              (≡-fst eq') (≡-snd eq')

  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (δ A γ γ→) (δ A' γ' γ'→) (δ B ψ ψ→) (δ B' ψ' ψ'→) p p' f
    with EnvBool, Γ Δ q e | EnvBool, Γ' Δ' q' e'
       | inspect (EnvBool, Γ Δ q) e | inspect (EnvBool, Γ' Δ' q') e'
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (δ A γ γ→) (δ A' γ' γ'→) (δ B ψ ψ→) (δ B' ψ' ψ'→) p p'
           (δ→δ f g) | true , w | true , w' | [ eq ] | [ eq' ] 
      = δ→δ (proj₁ f,plusmor∘g') (proj₂ f,plusmor∘g')
          where f,plusmor∘g' = auxδ-tt-tt Γ Γ' Δ Δ' q q' w w' A A' B B' γ γ→ γ' γ'→ ψ ψ→ ψ' ψ'→ p p' f g (proj₁ (EnvBool, Γ Δ q e)) (proj₂ (EnvBool, Γ Δ q e)) refl  (proj₁ (EnvBool, Γ' Δ' q' e'))  (proj₂ (EnvBool, Γ' Δ' q' e')) refl (≡-fst eq) (≡-snd eq) (≡-fst eq') (≡-snd eq')
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (δ A γ γ→) (δ A' γ' γ'→) (δ B ψ ψ→) (δ B' ψ' ψ'→) p p'
           (δ→δ f g) | true , w | false , w' | [ eq ] | [ eq' ] 
      = δ→δ (proj₁ f,plusmor∘g') (proj₂ f,plusmor∘g')
          where f,plusmor∘g' = auxδ-tt-ff Γ Γ' Δ Δ' q q' w w' A A' B B' γ γ→ γ' γ'→ ψ ψ→ ψ' ψ'→ p p' f g (proj₁ (EnvBool, Γ Δ q e)) (proj₂ (EnvBool, Γ Δ q e)) refl  (proj₁ (EnvBool, Γ' Δ' q' e'))  (proj₂ (EnvBool, Γ' Δ' q' e')) refl (≡-fst eq) (≡-snd eq) (≡-fst eq') (≡-snd eq')
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (δ A γ γ→) (δ A' γ' γ'→) (δ B ψ ψ→) (δ B' ψ' ψ'→) p p'
           (δ→δ f g) | false , w | true , w' | [ eq ] | [ eq' ] 
      = δ→δ (proj₁ f,plusmor∘g') (proj₂ f,plusmor∘g')
          where f,plusmor∘g' = auxδ-ff-tt Γ Γ' Δ Δ' q q' w w' A A' B B' γ γ→ γ' γ'→ ψ ψ→ ψ' ψ'→ p p' f g (proj₁ (EnvBool, Γ Δ q e)) (proj₂ (EnvBool, Γ Δ q e)) refl  (proj₁ (EnvBool, Γ' Δ' q' e'))  (proj₂ (EnvBool, Γ' Δ' q' e')) refl (≡-fst eq) (≡-snd eq) (≡-fst eq') (≡-snd eq')
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (δ A γ γ→) (δ A' γ' γ'→) (δ B ψ ψ→) (δ B' ψ' ψ'→) p p'
           (δ→δ f g) | false , w | false , w' | [ eq ] | [ eq' ] 
      = δ→δ (proj₁ f,plusmor∘g') (proj₂ f,plusmor∘g')
          where f,plusmor∘g' = auxδ-ff-ff Γ Γ' Δ Δ' q q' w w' A A' B B' γ γ→ γ' γ'→ ψ ψ→ ψ' ψ'→ p p' f g (proj₁ (EnvBool, Γ Δ q e)) (proj₂ (EnvBool, Γ Δ q e)) refl  (proj₁ (EnvBool, Γ' Δ' q' e'))  (proj₂ (EnvBool, Γ' Δ' q' e')) refl (≡-fst eq) (≡-snd eq) (≡-fst eq') (≡-snd eq')

  -- rest are impossible cases
  plus-mor q q' (δ A γ γ→) (ι x) (δ B ψ ψ→) (σ A₁ ψ') p () f
  plus-mor q q' (δ A γ γ→) (ι x) (δ B ψ ψ→) (δ A₁ ψ' γ→₁) p () f
  plus-mor q q' (δ A γ γ→) (σ A₁ γ') (δ B ψ ψ→) (ι x) p () f
  plus-mor q q' (δ A γ γ→) (σ A₁ γ') (δ B ψ ψ→) (δ A₂ ψ' γ→₁) p () f
  plus-mor q q' (δ A γ γ→) (δ A₁ γ' γ→₁) (δ B ψ ψ→) (ι x) p () f
  plus-mor q q' (δ A γ γ→) (δ A₁ γ' γ→₁) (δ B ψ ψ→) (σ A₂ ψ') p () f
  plus-mor q q' (σ A γ) (ι x) (σ B ψ) (σ A₁ ψ') p () f
  plus-mor q q' (σ A γ) (ι x) (σ B ψ) (δ A₁ ψ' γ→) p () f
  plus-mor q q' (σ A γ) (σ A₁ γ') (σ B ψ) (ι x) p () f
  plus-mor q q' (σ A γ) (σ A₁ γ') (σ B ψ) (δ A₂ ψ' γ→) p () f
  plus-mor q q' (σ A γ) (δ A₁ γ' γ→) (σ B ψ) (ι x) p () f
  plus-mor q q' (σ A γ) (δ A₁ γ' γ→) (σ B ψ) (σ A₂ ψ') p () f
  plus-mor q q' (ι c) (ι x) (ι d) (σ A ψ') p () x₂
  plus-mor q q' (ι c) (ι x) (ι d) (δ A ψ' γ→) p () x₂
  plus-mor q q' (ι c) (σ A γ') (ι d) (ι x) p () x₂
  plus-mor q q' (ι c) (σ A γ') (ι d) (δ A₁ ψ' γ→) p () x₂
  plus-mor q q' (ι c) (δ A γ' γ→) (ι d) (ι x) p () x₂
  plus-mor q q' (ι c) (δ A γ' γ→) (ι d) (σ A₁ ψ') p () x₂
  plus-mor q q' (ι x) γ' (σ A ψ) ψ' () p' x₁
  plus-mor q q' (ι x) γ' (δ A ψ γ→) ψ' () p' x₁
  plus-mor q q' (σ A γ) γ' (ι x) ψ' () p' x₁
  plus-mor q q' (σ A γ) γ' (δ A₁ ψ γ→) ψ' () p' x
  plus-mor q q' (δ A γ γ→) γ' (ι x) ψ' () p' x₁
  plus-mor q q' (δ A γ γ→) γ' (σ A₁ ψ) ψ' () p' x
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (δ _ _ _) (σ _ _) (δ _ _ _) (σ _ _) p p' f
    with EnvBool, Γ Δ q e | EnvBool, Γ' Δ' q' e'
  plus-mor _ _ (δ _ _ _) (σ _ _) (δ _ _ _) (σ _ _) _ _ () | true , _ | true , _
  plus-mor _ _ (δ _ _ _) (σ _ _) (δ _ _ _) (σ _ _) _ _ () | true , _ | false , _
  plus-mor _ _ (δ _ _ _) (σ _ _) (δ _ _ _) (σ _ _) _ _ () | false , _ | true , _
  plus-mor _ _ (δ _ _ _) (σ _ _) (δ _ _ _) (σ _ _) _ _ () | false , _ | false , _
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (δ _ _ _) (ι _) (δ _ _ _) (ι _) _ _ f
    with EnvBool, Γ Δ q e | EnvBool, Γ' Δ' q' e'
  plus-mor _ _ (δ _ _ _) (ι _) (δ _ _ _) (ι _) p p' () | true , w | true , w'
  plus-mor _ _ (δ _ _ _) (ι _) (δ _ _ _) (ι _) p p' () | true , w | false , w'
  plus-mor _ _ (δ _ _ _) (ι _) (δ _ _ _) (ι _) p p' () | false , w | true , w'
  plus-mor _ _ (δ _ _ _) (ι _) (δ _ _ _) (ι _) p p' () | false , w | false , w'
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (ι _) (σ _ _) (ι _) (σ _ _) p p' f
    with EnvBool, Γ Δ q e | EnvBool, Γ' Δ' q' e'
  plus-mor _ _ (ι _) (σ _ _) (ι _) (σ _ _) p p' () | true , w | true , w'
  plus-mor _ _ (ι _) (σ _ _) (ι _) (σ _ _) p p' () | true , w | false , w'
  plus-mor _ _ (ι _) (σ _ _) (ι _) (σ _ _) p p' () | false , w | true , w'
  plus-mor _ _ (ι _) (σ _ _) (ι _) (σ _ _) p p' () | false , w | false , w'
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (ι _) (δ _ _ _) (ι _) (δ _ _ _) _ _ f
    with EnvBool, Γ Δ q e | EnvBool, Γ' Δ' q' e'
  plus-mor _ _ (ι _) (δ _ _ _) (ι _) (δ _ _ _) p p' () | true , w | true , w'
  plus-mor _ _ (ι _) (δ _ _ _) (ι _) (δ _ _ _) p p' () | true , w | false , w'
  plus-mor _ _ (ι _) (δ _ _ _) (ι _) (δ _ _ _) p p' () | false , w | true , w'
  plus-mor _ _ (ι _) (δ _ _ _) (ι _) (δ _ _ _) p p' () | false , w | false , w'
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (σ _ _) (δ _ _ _) (σ _ _) (δ _ _ _) _ _ f
    with EnvBool, Γ Δ q e | EnvBool, Γ' Δ' q' e'
  plus-mor _ _ (σ _ _) (δ _ _ _) (σ _ _) (δ _ _ _) _ _ () | true , _ | true , _
  plus-mor _ _ (σ _ _) (δ _ _ _) (σ _ _) (δ _ _ _) _ _ () | true , _ | false , _
  plus-mor _ _ (σ _ _) (δ _ _ _) (σ _ _) (δ _ _ _) _ _ () | false , _ | true , _
  plus-mor _ _ (σ _ _) (δ _ _ _) (σ _ _) (δ _ _ _) _ _ () | false , _ | false , _
  plus-mor {Γ} {Γ'} {Δ} {Δ'} q q' {e} {e'}
           (σ _ _) (ι _) (σ _ _) (ι _) _ _ f
    with EnvBool, Γ Δ q e | EnvBool, Γ' Δ' q' e'
  plus-mor _ _ (σ _ _) (ι _) (σ _ _) (ι _) _ _ () | true , _ | true , _
  plus-mor _ _ (σ _ _) (ι _) (σ _ _) (ι _) _ _ () | true , _ | false , _
  plus-mor _ _ (σ _ _) (ι _) (σ _ _) (ι _) _ _ () | false , _ | true , _
  plus-mor _ _ (σ _ _) (ι _) (σ _ _) (ι _) _ _ () | false , _ | false , _


  auxσ-tt-tt : {Γ Γ' Δ Δ' : Ctxt} ->
               {q  : same-ctxt-shape Γ Δ} ->
               {q' : same-ctxt-shape Γ' Δ'} ->
               {e  : Env (Bool, Γ Δ q)} ->
               {e' : Env (Bool, Γ' Δ' q')} ->
               {w  : Env (if true then Γ else Δ)} ->
               {w' : Env (if true then Γ' else Δ')} ->
               {A  : Env Γ → Set} ->
               {A' : Env Γ' → Set} ->
               {B  : Env Δ → Set} ->
               {B' : Env Δ' → Set} ->
               {γ  : IR' (Γ ,σ A)}
               {γ' : IR' (Γ' ,σ A')} ->
               {ψ  : IR' (Δ ,σ B)} ->
               {ψ' : IR' (Δ' ,σ B')}
               {p  : same-shape γ ψ} ->
               {p' : same-shape γ' ψ'} ->
               (f  : A w → A' w') ->
               (g  : (a : A w) → Hom' (w , a) (w' , (f a)) γ γ') ->
               (t  : Bool) ->
               (ww : Env (if t then Γ else Δ)) ->
               (eq : (t , ww) ≡ (EnvBool, Γ Δ q e)) ->
               (t' : Bool) ->
               (ww' : Env (if t' then Γ' else Δ')) ->
               (eq' : (t' , ww') ≡ (EnvBool, Γ' Δ' q' e')) ->
               (eqt : t ≡ true) ->
               (eqw : subst (λ z → Env (if z then Γ else Δ)) eqt ww ≡ w) ->
               (eqt' : t' ≡ true) ->
               (eqw' : subst (λ z → Env (if z then Γ' else Δ')) eqt' ww' ≡ w') ->
   Σ[ new-f ∈ (Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B t ww ->
              Bool-elim (λ z → Env (if z then Γ' else Δ') → Set) A' B' t' ww') ]
      ((a : Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B t ww) →
        Hom' (e , subst (λ r →  Bool-elim (λ z → Env (if z then Γ else Δ) → Set)
                        A B (proj₁ r) (proj₂ r)) eq a)
             (e' , subst (λ r →  Bool-elim
                                  (λ z → Env (if z then Γ' else Δ') → Set)
                                  A' B' (proj₁ r) (proj₂ r)) eq' (new-f a))
             (plus γ ψ p q)
             (plus γ' ψ' p' q'))
  auxσ-tt-tt {Γ} {Γ'} {Δ} {Δ'} {q} {q'} {e} {e'} {w} {w'}
             {A} {A'} {B} {B'} {γ} {γ'} {ψ} {ψ'} {p} {p'}
             f g .true .w eq .true .w' eq' refl refl refl refl
    = f , (plus-mor q q' γ γ' ψ ψ' p p' ∘ g')
      where g' : (a : A w) -> _
            g' a = subst₂ (λ (r : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ))
                             (s : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ)) →
                                Hom' {proj₁ r} {proj₁ s}
                                     (proj₁ (proj₂ r)) (proj₁ (proj₂ s))
                                     (proj₂ (proj₂ r)) (proj₂ (proj₂ s)))
                           (≡-pair fst (≡-pair-× snd thd))
                           (≡-pair fst' (≡-pair-× snd' thd'))
                    (g a)
                where fst  = proj₁        (EnvBool,-withσ-lemma-true eq   a)
                      snd  = proj₁ (proj₂ (EnvBool,-withσ-lemma-true eq   a))
                      thd  = proj₂ (proj₂ (EnvBool,-withσ-lemma-true eq   a))
                      fst' = proj₁        (EnvBool,-withσ-lemma-true eq' (f a))
                      snd' = proj₁ (proj₂ (EnvBool,-withσ-lemma-true eq' (f a)))
                      thd' = proj₂ (proj₂ (EnvBool,-withσ-lemma-true eq' (f a)))


  auxσ-tt-ff : {Γ Γ' Δ Δ' : Ctxt} ->
               {q  : same-ctxt-shape Γ Δ} ->
               {q' : same-ctxt-shape Γ' Δ'} ->
               {e  : Env (Bool, Γ Δ q)} ->
               {e' : Env (Bool, Γ' Δ' q')} ->
               {w  : Env (if true then Γ else Δ)} ->
               {w' : Env (if false then Γ' else Δ')} ->
               {A  : Env Γ → Set} ->
               {A' : Env Γ' → Set} ->
               {B  : Env Δ → Set} ->
               {B' : Env Δ' → Set} ->
               {γ  : IR' (Γ ,σ A)}
               {γ' : IR' (Γ' ,σ A')} ->
               {ψ  : IR' (Δ ,σ B)} ->
               {ψ' : IR' (Δ' ,σ B')}
               {p  : same-shape γ ψ} ->
               {p' : same-shape γ' ψ'} ->
               (f  : A w → B' w') ->
               (g  : (a : A w) → Hom' (w , a) (w' , (f a)) γ ψ') ->
               (t  : Bool) ->
               (ww : Env (if t then Γ else Δ)) ->
               (eq : (t , ww) ≡ (EnvBool, Γ Δ q e)) ->
               (t' : Bool) ->
               (ww' : Env (if t' then Γ' else Δ')) ->
               (eq' : (t' , ww') ≡ (EnvBool, Γ' Δ' q' e')) ->
               (eqt : t ≡ true) ->
               (eqw : subst (λ z → Env (if z then Γ else Δ)) eqt ww ≡ w) ->
               (eqt' : t' ≡ false) ->
               (eqw' : subst (λ z → Env (if z then Γ' else Δ')) eqt' ww' ≡ w') ->
   Σ[ new-f ∈ (Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B t ww ->
              Bool-elim (λ z → Env (if z then Γ' else Δ') → Set) A' B' t' ww') ]
      ((a : Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B t ww) →
        Hom' (e , subst (λ r →  Bool-elim (λ z → Env (if z then Γ else Δ) → Set)
                        A B (proj₁ r) (proj₂ r)) eq a)
             (e' , subst (λ r →  Bool-elim
                                  (λ z → Env (if z then Γ' else Δ') → Set)
                                  A' B' (proj₁ r) (proj₂ r)) eq' (new-f a))
             (plus γ ψ p q)
             (plus γ' ψ' p' q'))               
  auxσ-tt-ff {Γ} {Γ'} {Δ} {Δ'} {q} {q'} {e} {e'} {w} {w'}
             {A} {A'} {B} {B'} {γ} {γ'} {ψ} {ψ'} {p} {p'}
             f g .true .w eq .false .w' eq' refl refl refl refl
   = f , (plus-mor q q' γ γ' ψ ψ' p p' ∘ g')
      where g' : (a : A w) -> _
            g' a = (subst₂ (λ (r : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ)) (s : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ)) → Hom' {proj₁ r} {proj₁ s} (proj₁ (proj₂ r)) (proj₁ (proj₂ s)) (proj₂ (proj₂ r)) (proj₂ (proj₂ s))) (≡-pair fst (≡-pair-× snd thd)) (≡-pair fst' (≡-pair-× snd' thd')) (g a))
              where fst = proj₁ (EnvBool,-withσ-lemma-true eq a)
                    snd = proj₁ (proj₂ (EnvBool,-withσ-lemma-true eq a))
                    thd  = proj₂ (proj₂ (EnvBool,-withσ-lemma-true eq a))
                    fst' = proj₁ (EnvBool,-withσ-lemma-false eq' (f a))
                    snd' = proj₁ (proj₂ (EnvBool,-withσ-lemma-false eq' (f a)))
                    thd'  = proj₂ (proj₂ (EnvBool,-withσ-lemma-false eq' (f a)))


  auxσ-ff-tt : {Γ Γ' Δ Δ' : Ctxt} ->
               {q  : same-ctxt-shape Γ Δ} ->
               {q' : same-ctxt-shape Γ' Δ'} ->
               {e  : Env (Bool, Γ Δ q)} ->
               {e' : Env (Bool, Γ' Δ' q')} ->
               {w  : Env (if false then Γ else Δ)} ->
               {w' : Env (if true then Γ' else Δ')} ->
               {A  : Env Γ → Set} ->
               {A' : Env Γ' → Set} ->
               {B  : Env Δ → Set} ->
               {B' : Env Δ' → Set} ->
               {γ  : IR' (Γ ,σ A)}
               {γ' : IR' (Γ' ,σ A')} ->
               {ψ  : IR' (Δ ,σ B)} ->
               {ψ' : IR' (Δ' ,σ B')}
               {p  : same-shape γ ψ} ->
               {p' : same-shape γ' ψ'} ->
               (f  : B w → A' w') ->
               (g  : (a : B w) → Hom' (w , a) (w' , (f a)) ψ γ') ->
               (t  : Bool) ->
               (ww : Env (if t then Γ else Δ)) ->
               (eq : (t , ww) ≡ (EnvBool, Γ Δ q e)) ->
               (t' : Bool) ->
               (ww' : Env (if t' then Γ' else Δ')) ->
               (eq' : (t' , ww') ≡ (EnvBool, Γ' Δ' q' e')) ->
               (eqt : t ≡ false) ->
               (eqw : subst (λ z → Env (if z then Γ else Δ)) eqt ww ≡ w) ->
               (eqt' : t' ≡ true) ->
               (eqw' : subst (λ z → Env (if z then Γ' else Δ')) eqt' ww' ≡ w') ->
   Σ[ new-f ∈ (Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B t ww ->
              Bool-elim (λ z → Env (if z then Γ' else Δ') → Set) A' B' t' ww') ]
      ((a : Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B t ww) →
        Hom' (e , subst (λ r →  Bool-elim (λ z → Env (if z then Γ else Δ) → Set)
                        A B (proj₁ r) (proj₂ r)) eq a)
             (e' , subst (λ r →  Bool-elim
                                  (λ z → Env (if z then Γ' else Δ') → Set)
                                  A' B' (proj₁ r) (proj₂ r)) eq' (new-f a))
             (plus γ ψ p q)
             (plus γ' ψ' p' q'))
  auxσ-ff-tt {Γ} {Γ'} {Δ} {Δ'} {q} {q'} {e} {e'} {w} {w'}
             {A} {A'} {B} {B'} {γ} {γ'} {ψ} {ψ'} {p} {p'}
             f g .false .w eq .true .w' eq' refl refl refl refl
    = f , (plus-mor q q' γ γ' ψ ψ' p p' ∘ g')
      where g' : (a : B w) -> _
            g' a = (subst₂ (λ (r : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ))
                              (s : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ)) →
                               Hom' {proj₁ r} {proj₁ s} (proj₁ (proj₂ r))
                                                        (proj₁ (proj₂ s))
                                                        (proj₂ (proj₂ r))
                                                        (proj₂ (proj₂ s)))
                            (≡-pair fst (≡-pair-× snd thd))
                            (≡-pair fst' (≡-pair-× snd' thd'))
                    (g a))
              where fst  = proj₁        (EnvBool,-withσ-lemma-false eq   a)
                    snd  = proj₁ (proj₂ (EnvBool,-withσ-lemma-false eq   a))
                    thd  = proj₂ (proj₂ (EnvBool,-withσ-lemma-false eq   a))
                    fst' = proj₁        (EnvBool,-withσ-lemma-true  eq' (f a))
                    snd' = proj₁ (proj₂ (EnvBool,-withσ-lemma-true  eq' (f a)))
                    thd' = proj₂ (proj₂ (EnvBool,-withσ-lemma-true  eq' (f a)))


  auxσ-ff-ff : {Γ Γ' Δ Δ' : Ctxt} ->
               {q  : same-ctxt-shape Γ Δ} ->
               {q' : same-ctxt-shape Γ' Δ'} ->
               {e  : Env (Bool, Γ Δ q)} ->
               {e' : Env (Bool, Γ' Δ' q')} ->
               {w  : Env (if false then Γ else Δ)} ->
               {w' : Env (if false then Γ' else Δ')} ->
               {A  : Env Γ → Set} ->
               {A' : Env Γ' → Set} ->
               {B  : Env Δ → Set} ->
               {B' : Env Δ' → Set} ->
               {γ  : IR' (Γ ,σ A)}
               {γ' : IR' (Γ' ,σ A')} ->
               {ψ  : IR' (Δ ,σ B)} ->
               {ψ' : IR' (Δ' ,σ B')}
               {p  : same-shape γ ψ} ->
               {p' : same-shape γ' ψ'} ->
               (f  : B w → B' w') ->
               (g  : (a : B w) → Hom' (w , a) (w' , (f a)) ψ ψ') ->
               (t  : Bool) ->
               (ww : Env (if t then Γ else Δ)) ->
               (eq : (t , ww) ≡ (EnvBool, Γ Δ q e)) ->
               (t' : Bool) ->
               (ww' : Env (if t' then Γ' else Δ')) ->
               (eq' : (t' , ww') ≡ (EnvBool, Γ' Δ' q' e')) ->
               (eqt : t ≡ false) ->
               (eqw : subst (λ z → Env (if z then Γ else Δ)) eqt ww ≡ w) ->
               (eqt' : t' ≡ false) ->
               (eqw' : subst (λ z → Env (if z then Γ' else Δ')) eqt' ww' ≡ w') ->
   Σ[ new-f ∈ (Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B t ww ->
              Bool-elim (λ z → Env (if z then Γ' else Δ') → Set) A' B' t' ww') ]
      ((a : Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B t ww) →
        Hom' (e , subst (λ r →  Bool-elim (λ z → Env (if z then Γ else Δ) → Set)
                        A B (proj₁ r) (proj₂ r)) eq a)
             (e' , subst (λ r →  Bool-elim
                                  (λ z → Env (if z then Γ' else Δ') → Set)
                                  A' B' (proj₁ r) (proj₂ r)) eq' (new-f a))
             (plus γ ψ p q)
             (plus γ' ψ' p' q'))
  auxσ-ff-ff {Γ} {Γ'} {Δ} {Δ'} {q} {q'} {e} {e'} {w} {w'}
             {A} {A'} {B} {B'} {γ} {γ'} {ψ} {ψ'} {p} {p'}
             f g .false .w eq .false .w' eq' refl refl refl refl
    = f , (plus-mor q q' γ γ' ψ ψ' p p' ∘ g')
      where g' : (a : B w) -> _
            g' a = (subst₂ (λ (r : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ))
                              (s : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ)) →
                               Hom' {proj₁ r} {proj₁ s} (proj₁ (proj₂ r))
                                                        (proj₁ (proj₂ s))
                                                        (proj₂ (proj₂ r))
                                                        (proj₂ (proj₂ s)))
                            (≡-pair fst (≡-pair-× snd thd))
                            (≡-pair fst' (≡-pair-× snd' thd'))
                    (g a))
              where fst  = proj₁        (EnvBool,-withσ-lemma-false eq   a)
                    snd  = proj₁ (proj₂ (EnvBool,-withσ-lemma-false eq   a))
                    thd  = proj₂ (proj₂ (EnvBool,-withσ-lemma-false eq   a))
                    fst' = proj₁        (EnvBool,-withσ-lemma-false eq' (f a))
                    snd' = proj₁ (proj₂ (EnvBool,-withσ-lemma-false eq' (f a)))
                    thd' = proj₂ (proj₂ (EnvBool,-withσ-lemma-false eq' (f a)))

  auxδ-tt-tt :  (Γ Γ' Δ Δ' : Ctxt) ->
                (q    : same-ctxt-shape Γ Δ) ->
                (q'   : same-ctxt-shape Γ' Δ') ->
                {e    : Env (Bool, Γ Δ q)} ->
                {e'   : Env (Bool, Γ' Δ' q')} ->
                (w   : Env (if true then Γ else Δ)) ->
                (w'   : Env (if true then Γ' else Δ')) ->
                (A    : Env Γ → Set) ->
                (A'   : Env Γ' → Set) ->
                (B    : Env Δ → Set) ->
                (B'   : Env Δ' → Set) ->
                (γ    : IR' (Γ ,δ A))
                (γ→   : {e₁ : Env Γ} {f₁ : A e₁ → C} {g₁ : A e₁ → C} → ((a : A e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) γ γ) ->
                (γ'   : IR' (Γ' ,δ A')) ->
                (γ'→  : {e₁ : Env Γ'} {f₁ : A' e₁ → C} {g₁ : A' e₁ → C} → ((a : A' e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) γ' γ') ->
                (ψ    : IR' (Δ ,δ B)) ->
                (ψ→   : {e₁ : Env Δ} {f₁ : B e₁ → C} {g₁ : B e₁ → C} → ((a : B e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) ψ ψ) ->
                (ψ'   : IR' (Δ' ,δ B'))
                (ψ'→  : {e₁ : Env Δ'} {f₁ : B' e₁ → C} {g₁ : B' e₁ → C} → ((a : B' e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) ψ' ψ') ->
                (p    : same-shape γ ψ) ->
                (p'   : same-shape γ' ψ') ->
                (f    : A' w' → A w) ->
                (g    : (h : A w → C) → Hom' (w , h) (w' , (h ∘ f)) γ γ') ->
                (t : Bool) ->
                (ww    : Env (if t then Γ else Δ)) ->
                (eq : (t , ww) ≡ (EnvBool, Γ Δ q e)) ->
                (t' : Bool) ->
                (ww'    : Env (if t' then Γ' else Δ')) ->
                (eq' : (t' , ww') ≡ (EnvBool, Γ' Δ' q' e')) ->
                (eqt₀ : t ≡ true) ->
                (eqw : subst (λ z → Env (if z then Γ else Δ)) eqt₀ ww ≡ w) ->
                (eqt'₀ : t' ≡ true) ->
                (eqw' : subst (λ z → Env (if z then Γ' else Δ')) eqt'₀ ww' ≡ w') ->
                Σ[ new-f ∈ (Bool-elim (λ z → Env (if z then Γ' else Δ') → Set) A' B' t' ww' →
                        Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B      t ww) ] ((h : Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B t ww → C) →
                        Hom' (e , subst (λ r →  Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B (proj₁ r) (proj₂ r) → C) eq h) (e' , subst (λ r →  Bool-elim (λ z → Env (if z then Γ' else Δ') → Set) A' B' (proj₁ r) (proj₂ r) → C) eq' (h ∘ new-f)) (plus γ ψ p q) (plus γ' ψ' p' q'))
  auxδ-tt-tt Γ Γ' Δ Δ' q q' {e} {e'} w w' A A' B B' γ γ→ γ' γ'→ ψ ψ→ ψ' ψ'→ p p' f g .true .w eq .true .w' eq' refl refl refl refl  = f , (λ h → plus-mor q q' γ γ' ψ ψ' p p' (g' h))
    where g' : (h : A w -> C) -> _
          g' h = (subst₂ (λ (r : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ)) (s : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ)) → Hom' {proj₁ r} {proj₁ s} (proj₁ (proj₂ r)) (proj₁ (proj₂ s)) (proj₂ (proj₂ r)) (proj₂ (proj₂ s))) (≡-pair fst (≡-pair-× snd thd)) (≡-pair fst' (≡-pair-× snd' thd')) (g h))
            where fst = proj₁ (EnvBool,-withδ-lemma-true Γ A γ Δ B ψ q w e eq h)
                  snd = proj₁ (proj₂ (EnvBool,-withδ-lemma-true Γ A γ Δ B ψ q w e eq h))
                  thd  = proj₂ (proj₂ (EnvBool,-withδ-lemma-true Γ A γ Δ B ψ q w e eq h))
                  fst' = proj₁ (EnvBool,-withδ-lemma-true Γ' A' γ' Δ' B' ψ' q' w' e' eq' (h ∘ f))
                  snd' = proj₁ (proj₂ (EnvBool,-withδ-lemma-true Γ' A' γ' Δ' B' ψ' q' w' e' eq' (h ∘ f)))
                  thd'  = proj₂ (proj₂ (EnvBool,-withδ-lemma-true Γ' A' γ' Δ' B' ψ' q' w' e' eq' (h ∘ f)))

  auxδ-tt-ff :  (Γ Γ' Δ Δ' : Ctxt) ->
                (q    : same-ctxt-shape Γ Δ) ->
                (q'   : same-ctxt-shape Γ' Δ') ->
                {e    : Env (Bool, Γ Δ q)} ->
                {e'   : Env (Bool, Γ' Δ' q')} ->
                (w   : Env (if true then Γ else Δ)) ->
                (w'   : Env (if false then Γ' else Δ')) ->
                (A    : Env Γ → Set) ->
                (A'   : Env Γ' → Set) ->
                (B    : Env Δ → Set) ->
                (B'   : Env Δ' → Set) ->
                (γ    : IR' (Γ ,δ A))
                (γ→   : {e₁ : Env Γ} {f₁ : A e₁ → C} {g₁ : A e₁ → C} → ((a : A e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) γ γ) ->
                (γ'   : IR' (Γ' ,δ A')) ->
                (γ'→  : {e₁ : Env Γ'} {f₁ : A' e₁ → C} {g₁ : A' e₁ → C} → ((a : A' e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) γ' γ') ->
                (ψ    : IR' (Δ ,δ B)) ->
                (ψ→   : {e₁ : Env Δ} {f₁ : B e₁ → C} {g₁ : B e₁ → C} → ((a : B e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) ψ ψ) ->
                (ψ'   : IR' (Δ' ,δ B'))
                (ψ'→  : {e₁ : Env Δ'} {f₁ : B' e₁ → C} {g₁ : B' e₁ → C} → ((a : B' e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) ψ' ψ') ->
                (p    : same-shape γ ψ) ->
                (p'   : same-shape γ' ψ') ->
                (f    : B' w' → A w) ->
                (g    : (h : A w → C) → Hom' (w , h) (w' , (h ∘ f)) γ ψ') ->
                (t : Bool) ->
                (ww    : Env (if t then Γ else Δ)) ->
                (eq : (t , ww) ≡ (EnvBool, Γ Δ q e)) ->
                (t' : Bool) ->
                (ww'    : Env (if t' then Γ' else Δ')) ->
                (eq' : (t' , ww') ≡ (EnvBool, Γ' Δ' q' e')) ->
                (eqt₀ : t ≡ true) ->
                (eqw : subst (λ z → Env (if z then Γ else Δ)) eqt₀ ww ≡ w) ->
                (eqt'₀ : t' ≡ false) ->
                (eqw' : subst (λ z → Env (if z then Γ' else Δ')) eqt'₀ ww' ≡ w') ->
                Σ[ new-f ∈ (Bool-elim (λ z → Env (if z then Γ' else Δ') → Set) A' B' t' ww' →
                        Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B      t ww) ] ((h : Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B t ww → C) →
                        Hom' (e , subst (λ r →  Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B (proj₁ r) (proj₂ r) → C) eq h) (e' , subst (λ r →  Bool-elim (λ z → Env (if z then Γ' else Δ') → Set) A' B' (proj₁ r) (proj₂ r) → C) eq' (h ∘ new-f)) (plus γ ψ p q) (plus γ' ψ' p' q'))
  auxδ-tt-ff Γ Γ' Δ Δ' q q' {e} {e'} w w' A A' B B' γ γ→ γ' γ'→ ψ ψ→ ψ' ψ'→ p p' f g .true .w eq .false .w' eq' refl refl refl refl = f , (λ h → plus-mor q q' γ γ' ψ ψ' p p' (g' h))
        where g' : (h : A w -> C) -> _
              g' h = (subst₂ (λ (r : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ)) (s : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ)) → Hom' {proj₁ r} {proj₁ s} (proj₁ (proj₂ r)) (proj₁ (proj₂ s)) (proj₂ (proj₂ r)) (proj₂ (proj₂ s))) (≡-pair fst (≡-pair-× snd thd)) (≡-pair fst' (≡-pair-× snd' thd')) (g h))
                where fst = proj₁ (EnvBool,-withδ-lemma-true Γ A γ Δ B ψ q w e eq h)
                      snd = proj₁ (proj₂ (EnvBool,-withδ-lemma-true Γ A γ Δ B ψ q w e eq h))
                      thd  = proj₂ (proj₂ (EnvBool,-withδ-lemma-true Γ A γ Δ B ψ q w e eq h))
                      fst' = proj₁ (EnvBool,-withδ-lemma-false Γ' A' γ' Δ' B' ψ' q' w' e' eq' (h ∘ f))
                      snd' = proj₁ (proj₂ (EnvBool,-withδ-lemma-false Γ' A' γ' Δ' B' ψ' q' w' e' eq' (h ∘ f)))
                      thd'  = proj₂ (proj₂ (EnvBool,-withδ-lemma-false Γ' A' γ' Δ' B' ψ' q' w' e' eq' (h ∘ f)))



  auxδ-ff-tt :  (Γ Γ' Δ Δ' : Ctxt) ->
                (q    : same-ctxt-shape Γ Δ) ->
                (q'   : same-ctxt-shape Γ' Δ') ->
                {e    : Env (Bool, Γ Δ q)} ->
                {e'   : Env (Bool, Γ' Δ' q')} ->
                (w   : Env (if false then Γ else Δ)) ->
                (w'   : Env (if true then Γ' else Δ')) ->
                (A    : Env Γ → Set) ->
                (A'   : Env Γ' → Set) ->
                (B    : Env Δ → Set) ->
                (B'   : Env Δ' → Set) ->
                (γ    : IR' (Γ ,δ A))
                (γ→   : {e₁ : Env Γ} {f₁ : A e₁ → C} {g₁ : A e₁ → C} → ((a : A e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) γ γ) ->
                (γ'   : IR' (Γ' ,δ A')) ->
                (γ'→  : {e₁ : Env Γ'} {f₁ : A' e₁ → C} {g₁ : A' e₁ → C} → ((a : A' e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) γ' γ') ->
                (ψ    : IR' (Δ ,δ B)) ->
                (ψ→   : {e₁ : Env Δ} {f₁ : B e₁ → C} {g₁ : B e₁ → C} → ((a : B e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) ψ ψ) ->
                (ψ'   : IR' (Δ' ,δ B'))
                (ψ'→  : {e₁ : Env Δ'} {f₁ : B' e₁ → C} {g₁ : B' e₁ → C} → ((a : B' e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) ψ' ψ') ->
                (p    : same-shape γ ψ) ->
                (p'   : same-shape γ' ψ') ->
                (f    : A' w' → B w) ->
                (g    : (h : B w → C) → Hom' (w , h) (w' , (h ∘ f)) ψ γ') ->
                (t : Bool) ->
                (ww    : Env (if t then Γ else Δ)) ->
                (eq : (t , ww) ≡ (EnvBool, Γ Δ q e)) ->
                (t' : Bool) ->
                (ww'    : Env (if t' then Γ' else Δ')) ->
                (eq' : (t' , ww') ≡ (EnvBool, Γ' Δ' q' e')) ->
                (eqt₀ : t ≡ false) ->
                (eqw : subst (λ z → Env (if z then Γ else Δ)) eqt₀ ww ≡ w) ->
                (eqt'₀ : t' ≡ true) ->
                (eqw' : subst (λ z → Env (if z then Γ' else Δ')) eqt'₀ ww' ≡ w') ->
                Σ[ new-f ∈ (Bool-elim (λ z → Env (if z then Γ' else Δ') → Set) A' B' t' ww' →
                        Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B      t ww) ] ((h : Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B t ww → C) →
                        Hom' (e , subst (λ r →  Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B (proj₁ r) (proj₂ r) → C) eq h) (e' , subst (λ r →  Bool-elim (λ z → Env (if z then Γ' else Δ') → Set) A' B' (proj₁ r) (proj₂ r) → C) eq' (h ∘ new-f)) (plus γ ψ p q) (plus γ' ψ' p' q'))
  auxδ-ff-tt Γ Γ' Δ Δ' q q' {e} {e'} w w' A A' B B' γ γ→ γ' γ'→ ψ ψ→ ψ' ψ'→ p p' f g .false .w eq .true .w' eq' refl refl refl refl = f , (λ h → plus-mor q q' γ γ' ψ ψ' p p' (g' h))
        where g' : (h : B w -> C) -> _
              g' h = subst₂ (λ (r : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ)) (s : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ)) → Hom' {proj₁ r} {proj₁ s} (proj₁ (proj₂ r)) (proj₁ (proj₂ s)) (proj₂ (proj₂ r)) (proj₂ (proj₂ s))) (≡-pair fst (≡-pair-× snd thd)) (≡-pair fst' (≡-pair-× snd' thd')) (g h)
                where fst = proj₁ (EnvBool,-withδ-lemma-false Γ A γ Δ B ψ q w e eq h)
                      snd = proj₁ (proj₂ (EnvBool,-withδ-lemma-false Γ A γ Δ B ψ q w e eq h))
                      thd  = proj₂ (proj₂ (EnvBool,-withδ-lemma-false Γ A γ Δ B ψ q w e eq h))
                      fst' = proj₁ (EnvBool,-withδ-lemma-true Γ' A' γ' Δ' B' ψ' q' w' e' eq' (h ∘ f))
                      snd' = proj₁ (proj₂ (EnvBool,-withδ-lemma-true Γ' A' γ' Δ' B' ψ' q' w' e' eq' (h ∘ f)))
                      thd'  = proj₂ (proj₂ (EnvBool,-withδ-lemma-true Γ' A' γ' Δ' B' ψ' q' w' e' eq' (h ∘ f)))


  auxδ-ff-ff :  (Γ Γ' Δ Δ' : Ctxt) ->
                (q    : same-ctxt-shape Γ Δ) ->
                (q'   : same-ctxt-shape Γ' Δ') ->
                {e    : Env (Bool, Γ Δ q)} ->
                {e'   : Env (Bool, Γ' Δ' q')} ->
                (w   : Env (if false then Γ else Δ)) ->
                (w'   : Env (if false then Γ' else Δ')) ->
                (A    : Env Γ → Set) ->
                (A'   : Env Γ' → Set) ->
                (B    : Env Δ → Set) ->
                (B'   : Env Δ' → Set) ->
                (γ    : IR' (Γ ,δ A))
                (γ→   : {e₁ : Env Γ} {f₁ : A e₁ → C} {g₁ : A e₁ → C} → ((a : A e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) γ γ) ->
                (γ'   : IR' (Γ' ,δ A')) ->
                (γ'→  : {e₁ : Env Γ'} {f₁ : A' e₁ → C} {g₁ : A' e₁ → C} → ((a : A' e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) γ' γ') ->
                (ψ    : IR' (Δ ,δ B)) ->
                (ψ→   : {e₁ : Env Δ} {f₁ : B e₁ → C} {g₁ : B e₁ → C} → ((a : B e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) ψ ψ) ->
                (ψ'   : IR' (Δ' ,δ B'))
                (ψ'→  : {e₁ : Env Δ'} {f₁ : B' e₁ → C} {g₁ : B' e₁ → C} → ((a : B' e₁) → HomC (f₁ a) (g₁ a)) → Hom' (e₁ , f₁) (e₁ , g₁) ψ' ψ') ->
                (p    : same-shape γ ψ) ->
                (p'   : same-shape γ' ψ') ->
                (f    : B' w' → B w) ->
                (g    : (h : B w → C) → Hom' (w , h) (w' , (h ∘ f)) ψ ψ') ->
                (t : Bool) ->
                (ww    : Env (if t then Γ else Δ)) ->
                (eq : (t , ww) ≡ (EnvBool, Γ Δ q e)) ->
                (t' : Bool) ->
                (ww'    : Env (if t' then Γ' else Δ')) ->
                (eq' : (t' , ww') ≡ (EnvBool, Γ' Δ' q' e')) ->
                (eqt₀ : t ≡ false) ->
                (eqw : subst (λ z → Env (if z then Γ else Δ)) eqt₀ ww ≡ w) ->
                (eqt'₀ : t' ≡ false) ->
                (eqw' : subst (λ z → Env (if z then Γ' else Δ')) eqt'₀ ww' ≡ w') ->
                Σ[ new-f ∈ (Bool-elim (λ z → Env (if z then Γ' else Δ') → Set) A' B' t' ww' →
                        Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B      t ww) ] ((h : Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B t ww → C) →
                        Hom' (e , subst (λ r →  Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B (proj₁ r) (proj₂ r) → C) eq h) (e' , subst (λ r →  Bool-elim (λ z → Env (if z then Γ' else Δ') → Set) A' B' (proj₁ r) (proj₂ r) → C) eq' (h ∘ new-f)) (plus γ ψ p q) (plus γ' ψ' p' q'))
  auxδ-ff-ff Γ Γ' Δ Δ' q q' {e} {e'} w w' A A' B B' γ γ→ γ' γ'→ ψ ψ→ ψ' ψ'→ p p' f g .false .w eq .false .w' eq' refl refl refl refl = f , (λ h → plus-mor q q' γ γ' ψ ψ' p p' (g' h))
        where g' : (h : B w -> C) -> _
              g' h = subst₂ (λ (r : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ)) (s : Σ[ Γ ∈ Ctxt ] ((Env Γ) × IR' Γ)) → Hom' {proj₁ r} {proj₁ s} (proj₁ (proj₂ r)) (proj₁ (proj₂ s)) (proj₂ (proj₂ r)) (proj₂ (proj₂ s))) (≡-pair fst (≡-pair-× snd thd)) (≡-pair fst' (≡-pair-× snd' thd')) (g h)
                where fst = proj₁ (EnvBool,-withδ-lemma-false Γ A γ Δ B ψ q w e eq h)
                      snd = proj₁ (proj₂ (EnvBool,-withδ-lemma-false Γ A γ Δ B ψ q w e eq h))
                      thd  = proj₂ (proj₂ (EnvBool,-withδ-lemma-false Γ A γ Δ B ψ q w e eq h))
                      fst' = proj₁ (EnvBool,-withδ-lemma-false Γ' A' γ' Δ' B' ψ' q' w' e' eq' (h ∘ f))
                      snd' = proj₁ (proj₂ (EnvBool,-withδ-lemma-false Γ' A' γ' Δ' B' ψ' q' w' e' eq' (h ∘ f)))
                      thd'  = proj₂ (proj₂ (EnvBool,-withδ-lemma-false Γ' A' γ' Δ' B' ψ' q' w' e' eq' (h ∘ f)))

_+UIR_ : UIR+ -> UIR+ -> UIR+
γ +UIR ψ = σ (λ _ → Bool) (plus (pad₀ γ ψ)
                                (pad₁ γ ψ)
                                (padded-same-shape γ ψ)
                                tt)