text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Sublist-related properties
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Sublist.Propositional.Properties
  {a} {A : Set a} where

open import Data.List.Base using (List; []; _∷_;  map)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.Any.Properties
  using (here-injective; there-injective)
open import Data.List.Relation.Binary.Sublist.Propositional
  hiding (map)
import Data.List.Relation.Binary.Sublist.Setoid.Properties
  as SetoidProperties
open import Data.Product using (∃; _,_; proj₂)
open import Function.Base
open import Level using (Level)
open import Relation.Binary using (_Respects_)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary using (Pred)

private
  variable
    b ℓ : Level
    B : Set b

------------------------------------------------------------------------
-- Re-exporting setoid properties

open SetoidProperties (setoid A) public
  hiding (map⁺)

map⁺ : ∀ {as bs} (f : A → B) → as ⊆ bs → map f as ⊆ map f bs
map⁺ {B = B} f = SetoidProperties.map⁺ (setoid A) (setoid B) (cong f)

------------------------------------------------------------------------
-- Category laws for _⊆_

⊆-trans-idˡ : ∀ {xs ys : List A} {τ : xs ⊆ ys} →
              ⊆-trans ⊆-refl τ ≡ τ
⊆-trans-idˡ {_}     {τ = []    } = refl
⊆-trans-idˡ {_}     {τ = _ ∷  _} = cong (_ ∷_ ) ⊆-trans-idˡ
⊆-trans-idˡ {[]}    {τ = _ ∷ʳ _} = cong (_ ∷ʳ_) ⊆-trans-idˡ
⊆-trans-idˡ {_ ∷ _} {τ = _ ∷ʳ _} = cong (_ ∷ʳ_) ⊆-trans-idˡ

⊆-trans-idʳ : ∀ {xs ys : List A} {τ : xs ⊆ ys} →
              ⊆-trans τ ⊆-refl ≡ τ
⊆-trans-idʳ {τ = []      } = refl
⊆-trans-idʳ {τ = _ ∷ʳ _  } = cong (_  ∷ʳ_ ) ⊆-trans-idʳ
⊆-trans-idʳ {τ = refl ∷ _} = cong (refl ∷_) ⊆-trans-idʳ

-- Note: The associativity law is oriented such that rewriting with it
-- may trigger reductions of ⊆-trans, which matches first on its
-- second argument and then on its first argument.

⊆-trans-assoc : ∀ {ws xs ys zs : List A}
                {τ₁ : ws ⊆ xs} {τ₂ : xs ⊆ ys} {τ₃ : ys ⊆ zs} →
                ⊆-trans τ₁ (⊆-trans τ₂ τ₃) ≡ ⊆-trans (⊆-trans τ₁ τ₂) τ₃
⊆-trans-assoc {τ₁ = _}        {_}      {_ ∷ʳ _} = cong (_ ∷ʳ_) ⊆-trans-assoc
⊆-trans-assoc {τ₁ = _}        {_ ∷ʳ _} {_ ∷  _} = cong (_ ∷ʳ_) ⊆-trans-assoc
⊆-trans-assoc {τ₁ = _ ∷ʳ _  } {_ ∷  _} {_ ∷  _} = cong (_ ∷ʳ_) ⊆-trans-assoc
⊆-trans-assoc {τ₁ = refl ∷ _} {_ ∷  _} {_ ∷  _} = cong (_ ∷_ ) ⊆-trans-assoc
⊆-trans-assoc {τ₁ = []}       {[]}     {[]}     = refl

------------------------------------------------------------------------
-- Laws concerning ⊆-trans and ∷ˡ⁻

⊆-trans-∷ˡ⁻ᵣ : ∀ {y} {xs ys zs : List A} {τ : xs ⊆ ys} {σ : (y ∷ ys) ⊆ zs} →
               ⊆-trans τ (∷ˡ⁻ σ) ≡ ⊆-trans (y ∷ʳ τ) σ
⊆-trans-∷ˡ⁻ᵣ {σ = x ∷ σ} = refl
⊆-trans-∷ˡ⁻ᵣ {σ = y ∷ʳ σ} = cong (y ∷ʳ_) ⊆-trans-∷ˡ⁻ᵣ

⊆-trans-∷ˡ⁻ₗ : ∀ {x} {xs ys zs : List A} {τ : (x ∷ xs) ⊆ ys} {σ : ys ⊆ zs} →
              ⊆-trans (∷ˡ⁻ τ) σ ≡ ∷ˡ⁻ (⊆-trans τ σ)
⊆-trans-∷ˡ⁻ₗ                {σ = y   ∷ʳ σ} = cong (y ∷ʳ_) ⊆-trans-∷ˡ⁻ₗ
⊆-trans-∷ˡ⁻ₗ {τ = y   ∷ʳ τ} {σ = refl ∷ σ} = cong (y ∷ʳ_) ⊆-trans-∷ˡ⁻ₗ
⊆-trans-∷ˡ⁻ₗ {τ = refl ∷ τ} {σ = refl ∷ σ} = refl

⊆-∷ˡ⁻trans-∷ : ∀ {y} {xs ys zs : List A} {τ : xs ⊆ ys} {σ : (y ∷ ys) ⊆ zs} →
               ∷ˡ⁻ (⊆-trans (refl ∷ τ) σ) ≡ ⊆-trans (y ∷ʳ τ) σ
⊆-∷ˡ⁻trans-∷ {σ = y   ∷ʳ σ} = cong (y ∷ʳ_) ⊆-∷ˡ⁻trans-∷
⊆-∷ˡ⁻trans-∷ {σ = refl ∷ σ} = refl

------------------------------------------------------------------------
-- Relationships to other predicates

-- All P is a contravariant functor from _⊆_ to Set.

All-resp-⊆ : {P : Pred A ℓ} → (All P) Respects _⊇_
All-resp-⊆ []          []       = []
All-resp-⊆ (_    ∷ʳ p) (_ ∷ xs) = All-resp-⊆ p xs
All-resp-⊆ (refl ∷  p) (x ∷ xs) = x ∷ All-resp-⊆ p xs

-- Any P is a covariant functor from _⊆_ to Set.

Any-resp-⊆ : {P : Pred A ℓ} → (Any P) Respects _⊆_
Any-resp-⊆ = lookup

------------------------------------------------------------------------
-- Functor laws for All-resp-⊆

-- First functor law: identity.

All-resp-⊆-refl : ∀ {P : Pred A ℓ} {xs : List A} →
                  All-resp-⊆ ⊆-refl ≗ id {A = All P xs}
All-resp-⊆-refl []       = refl
All-resp-⊆-refl (p ∷ ps) = cong (p ∷_) (All-resp-⊆-refl ps)

-- Second functor law: composition.

All-resp-⊆-trans : ∀ {P : Pred A ℓ} {xs ys zs} {τ : xs ⊆ ys} (τ′ : ys ⊆ zs) →
                   All-resp-⊆ {P = P} (⊆-trans τ τ′) ≗ All-resp-⊆ τ ∘ All-resp-⊆ τ′
All-resp-⊆-trans                (_    ∷ʳ τ′) (p ∷ ps) = All-resp-⊆-trans τ′ ps
All-resp-⊆-trans {τ = _ ∷ʳ _  } (refl ∷  τ′) (p ∷ ps) = All-resp-⊆-trans τ′ ps
All-resp-⊆-trans {τ = refl ∷ _} (refl ∷  τ′) (p ∷ ps) = cong (p ∷_) (All-resp-⊆-trans τ′ ps)
All-resp-⊆-trans {τ = []      } ([]        ) []       = refl

------------------------------------------------------------------------
-- Functor laws for Any-resp-⊆ / lookup

-- First functor law: identity.

Any-resp-⊆-refl : ∀ {P : Pred A ℓ} {xs} →
                  Any-resp-⊆ ⊆-refl ≗ id {A = Any P xs}
Any-resp-⊆-refl (here p)  = refl
Any-resp-⊆-refl (there i) = cong there (Any-resp-⊆-refl i)

lookup-⊆-refl = Any-resp-⊆-refl

-- Second functor law: composition.

Any-resp-⊆-trans : ∀ {P : Pred A ℓ} {xs ys zs} {τ : xs ⊆ ys} (τ′ : ys ⊆ zs) →
                   Any-resp-⊆ {P = P} (⊆-trans τ τ′) ≗ Any-resp-⊆ τ′ ∘ Any-resp-⊆ τ
Any-resp-⊆-trans                (_ ∷ʳ τ′) i         = cong there (Any-resp-⊆-trans τ′ i)
Any-resp-⊆-trans {τ = _   ∷ʳ _} (_ ∷  τ′) i         = cong there (Any-resp-⊆-trans τ′ i)
Any-resp-⊆-trans {τ = _    ∷ _} (_ ∷  τ′) (there i) = cong there (Any-resp-⊆-trans τ′ i)
Any-resp-⊆-trans {τ = refl ∷ _} (_ ∷  τ′) (here _)  = refl
Any-resp-⊆-trans {τ = []      } []        ()

lookup-⊆-trans = Any-resp-⊆-trans

------------------------------------------------------------------------
-- The `lookup` function for `xs ⊆ ys` is injective.
--
-- Note: `lookup` can be seen as a strictly increasing reindexing function
-- for indices into `xs`, producing indices into `ys`.

lookup-injective : ∀ {P : Pred A ℓ} {xs ys} {τ : xs ⊆ ys} {i j : Any P xs} →
                   lookup τ i ≡ lookup τ j → i ≡ j
lookup-injective {τ = _  ∷ʳ _}                     = lookup-injective ∘′ there-injective
lookup-injective {τ = x≡y ∷ _} {here  _} {here  _} = cong here ∘′ subst-injective x≡y ∘′ here-injective
  -- Note: instead of using subst-injective, we could match x≡y against refl on the lhs.
  -- However, this turns the following clause into a non-strict match.
lookup-injective {τ = _   ∷ _} {there _} {there _} = cong there ∘′ lookup-injective ∘′ there-injective

-------------------------------------------------------------------------
-- from∈ ∘ to∈ turns a sublist morphism τ : x∷xs ⊆ ys into a morphism
-- [x] ⊆ ys.  The same morphism is obtained by pre-composing τ with
-- the canonial morphism [x] ⊆ x∷xs.
--
-- Note: This lemma does not hold for Sublist.Setoid, but could hold for
-- a hypothetical Sublist.Groupoid where trans refl = id.

from∈∘to∈ : ∀ {x : A} {xs ys} (τ : x ∷ xs ⊆ ys) →
            from∈ (to∈ τ) ≡ ⊆-trans (refl ∷ minimum xs) τ
from∈∘to∈ (x≡y ∷ τ) = cong (x≡y ∷_) ([]⊆-irrelevant _ _)
from∈∘to∈ (y  ∷ʳ τ) = cong (y  ∷ʳ_) (from∈∘to∈ τ)

from∈∘lookup : ∀{x : A} {xs ys} (τ : xs ⊆ ys) (i : x ∈ xs) →
               from∈ (lookup τ i) ≡ ⊆-trans (from∈ i) τ
from∈∘lookup (y   ∷ʳ τ)  i          = cong (y ∷ʳ_) (from∈∘lookup τ i)
from∈∘lookup (_    ∷ τ) (there i)   = cong (_ ∷ʳ_) (from∈∘lookup τ i)
from∈∘lookup (refl ∷ τ) (here refl) = cong (refl ∷_) ([]⊆-irrelevant _ _)

------------------------------------------------------------------------
-- Weak pushout (wpo)

-- A raw pushout is a weak pushout if the pushout square commutes.

IsWeakPushout : ∀{xs ys zs : List A} {τ : xs ⊆ ys} {σ : xs ⊆ zs} →
                RawPushout τ σ → Set a
IsWeakPushout {τ = τ} {σ = σ} rpo =
  ⊆-trans τ (RawPushout.leg₁ rpo) ≡
  ⊆-trans σ (RawPushout.leg₂ rpo)

-- Joining two list extensions with ⊆-pushout produces a weak pushout.

⊆-pushoutˡ-is-wpo : ∀{xs ys zs : List A} (τ : xs ⊆ ys) (σ : xs ⊆ zs) →
                    IsWeakPushout (⊆-pushoutˡ τ σ)
⊆-pushoutˡ-is-wpo [] σ
  rewrite ⊆-trans-idʳ {τ = σ}
        = ⊆-trans-idˡ {xs = []}
⊆-pushoutˡ-is-wpo (y   ∷ʳ τ) σ          = cong (y   ∷ʳ_) (⊆-pushoutˡ-is-wpo τ σ)
⊆-pushoutˡ-is-wpo (x≡y  ∷ τ) (z   ∷ʳ σ) = cong (z   ∷ʳ_) (⊆-pushoutˡ-is-wpo (x≡y ∷ τ) σ)
⊆-pushoutˡ-is-wpo (refl ∷ τ) (refl ∷ σ) = cong (refl ∷_) (⊆-pushoutˡ-is-wpo τ σ)

------------------------------------------------------------------------
-- Properties of disjointness

-- From τ₁ ⊎ τ₂ = τ, compute the injection ι₁ such that τ₁ = ⊆-trans ι₁ τ.

DisjointUnion-inj₁ : ∀ {xs ys zs xys : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : xys ⊆ zs} →
                      DisjointUnion τ₁ τ₂ τ → ∃ λ (ι₁ : xs ⊆ xys) → ⊆-trans ι₁ τ ≡ τ₁
DisjointUnion-inj₁ []         = []       , refl
DisjointUnion-inj₁ (y   ∷ₙ d) = _        , cong (y  ∷ʳ_) (proj₂ (DisjointUnion-inj₁ d))
DisjointUnion-inj₁ (x≈y ∷ₗ d) = refl ∷ _ , cong (x≈y ∷_) (proj₂ (DisjointUnion-inj₁ d))
DisjointUnion-inj₁ (x≈y ∷ᵣ d) = _ ∷ʳ _   , cong (_  ∷ʳ_) (proj₂ (DisjointUnion-inj₁ d))

-- From τ₁ ⊎ τ₂ = τ, compute the injection ι₂ such that τ₂ = ⊆-trans ι₂ τ.

DisjointUnion-inj₂ : ∀ {xs ys zs xys : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : xys ⊆ zs} →
                      DisjointUnion τ₁ τ₂ τ → ∃ λ (ι₂ : ys ⊆ xys) → ⊆-trans ι₂ τ ≡ τ₂
DisjointUnion-inj₂ []         = []       , refl
DisjointUnion-inj₂ (y   ∷ₙ d) = _        , cong (y  ∷ʳ_) (proj₂ (DisjointUnion-inj₂ d))
DisjointUnion-inj₂ (x≈y ∷ᵣ d) = refl ∷ _ , cong (x≈y ∷_) (proj₂ (DisjointUnion-inj₂ d))
DisjointUnion-inj₂ (x≈y ∷ₗ d) = _ ∷ʳ _   , cong (_  ∷ʳ_) (proj₂ (DisjointUnion-inj₂ d))

-- A sublist σ disjoint to both τ₁ and τ₂ is an equalizer
-- for the separators of τ₁ and τ₂.

equalize-separators : ∀ {us xs ys zs : List A}
  {σ : us ⊆ zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} (let s = separateˡ τ₁ τ₂) →
  Disjoint σ τ₁ → Disjoint σ τ₂ →
  ⊆-trans σ (Separation.separator₁ s) ≡
  ⊆-trans σ (Separation.separator₂ s)
equalize-separators [] [] = refl
equalize-separators (y    ∷ₙ d₁) (.y   ∷ₙ d₂) = cong (y ∷ʳ_) (equalize-separators d₁ d₂)
equalize-separators (y    ∷ₙ d₁) (refl ∷ᵣ d₂) = cong (y ∷ʳ_) (equalize-separators d₁ d₂)
equalize-separators (refl ∷ᵣ d₁) (y    ∷ₙ d₂) = cong (y ∷ʳ_) (equalize-separators d₁ d₂)
equalize-separators {τ₁ = refl ∷ _} {τ₂ = refl ∷ _}  -- match here to work around deficiency of Agda's forcing translation
                    (_    ∷ᵣ d₁) (_   ∷ᵣ d₂) = cong (_ ∷ʳ_) (cong (_ ∷ʳ_) (equalize-separators d₁ d₂))
equalize-separators (x≈y  ∷ₗ d₁) (.x≈y ∷ₗ d₂) = cong (trans x≈y refl ∷_) (equalize-separators d₁ d₂)


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

open import Numbers.ClassicalReals.RealField
open import LogicalFormulae
open import Setoids.Subset
open import Setoids.Setoids
open import Setoids.Orders.Partial.Definition
open import Sets.EquivalenceRelations
open import Rings.Orders.Partial.Definition
open import Rings.Definition
open import Fields.Fields
open import Groups.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Functions.Definition

module Numbers.Intervals.Arithmetic {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {_<_ : Rel {_} {c} A} {R : Ring S _+_ _*_} {pOrder : SetoidPartialOrder S _<_} (pRing : PartiallyOrderedRing R pOrder) where

open import Numbers.Intervals.Definition pRing
open import Rings.Orders.Partial.Lemmas pRing
open Ring R
open Group additiveGroup
open PartiallyOrderedRing pRing
open Setoid S
open Equivalence eq
open SetoidPartialOrder pOrder

intervalSum : OpenInterval → OpenInterval → OpenInterval
intervalSum record { minBound = a ; maxBound = b } record { minBound = c ; maxBound = d } = record { minBound = a + c ; maxBound = b + d }

intervalConstantSum : OpenInterval → A → OpenInterval
intervalConstantSum record { minBound = x ; maxBound = y } a = record { minBound = x + a ; maxBound = y + a }

intervalSumContains : {a b : A} → {i j : OpenInterval} → isInInterval a i → isInInterval b j → isInInterval (a + b) (intervalSum i j)
intervalSumContains (fst1 ,, snd1) (fst2 ,, snd2) = ringAddInequalities fst1 fst2 ,, ringAddInequalities snd1 snd2

intervalConstantProduct : OpenInterval → (a : A) → (0R < a) → OpenInterval
intervalConstantProduct record { minBound = minBound ; maxBound = maxBound } a 0<a = record { minBound = minBound * a ; maxBound = maxBound * a }

intervalInverse : OpenInterval → OpenInterval
intervalInverse record { minBound = b ; maxBound = c } = record { minBound = inverse c ; maxBound = inverse b }

intervalConstantSumContains : {a : A} {i : OpenInterval} (c : A) → isInInterval a i → isInInterval (a + c) (intervalConstantSum i c)
intervalConstantSumContains c (fst ,, snd) = orderRespectsAddition fst c ,, orderRespectsAddition snd c

intervalConstantProductContains : {a : A} {i : OpenInterval} {c : A} → (0<c : 0R < c) → isInInterval a i → isInInterval (a * c) (intervalConstantProduct i c 0<c)
intervalConstantProductContains {a} {i} 0<c ai = ringCanMultiplyByPositive 0<c (_&&_.fst ai) ,, ringCanMultiplyByPositive 0<c (_&&_.snd ai)

intervalInverseContains : {a : A} {i : OpenInterval} → isInInterval a i → isInInterval (inverse a) (intervalInverse i)
intervalInverseContains (less ,, greater) = ringSwapNegatives' greater ,, ringSwapNegatives' less

intervalEquality : OpenInterval → OpenInterval → Set b
intervalEquality record { minBound = minBound1 ; maxBound = maxBound1 } record { minBound = minBound ; maxBound = maxBound } = (minBound1 ∼ minBound) && (maxBound1 ∼ maxBound)

intervalWellDefined : {a : A} {i j : OpenInterval} → intervalEquality i j → isInInterval a i → isInInterval a j
intervalWellDefined (eq1 ,, eq2) (fst ,, snd) = <WellDefined eq1 reflexive fst ,, <WellDefined reflexive eq2 snd

intervalWellDefined' : {a b : A} {i : OpenInterval} → a ∼ b → isInInterval a i → isInInterval b i
intervalWellDefined' a=b (fst ,, snd) = <WellDefined reflexive a=b fst ,, <WellDefined a=b reflexive snd

increaseBoundAbove : {a minB maxB : A} → isInInterval a record { minBound = minB ; maxBound = maxB } → {bigger : A} → maxB < bigger → isInInterval a record { minBound = minB ; maxBound = bigger }
increaseBoundAbove (fst ,, snd) m<b = fst ,, <Transitive snd m<b

ext: agda


text:
module SystemF.BigStep.Extrinsic where

open import SystemF.BigStep.Types
open import SystemF.BigStep.Extrinsic.Terms
open import SystemF.BigStep.Extrinsic.Welltyped
open import SystemF.BigStep.Extrinsic.Semantics


text:
open import Nat
open import Prelude
open import contexts
open import core

open import canonical-value-forms

module canonical-boxed-forms where
  canonical-boxed-forms-b : ∀{Δ d} →
                            Δ , ∅ ⊢ d :: b →
                            d boxedval →
                            d == c
  canonical-boxed-forms-b (TAVar _) (BVVal ())
  canonical-boxed-forms-b wt (BVVal v) = canonical-value-forms-b wt v

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for boxed values at arrow type
  data cbf-arr : (Δ : hctx) (d : iexp) (τ1 τ2 : typ) → Set where
    CBFLam : ∀{Δ d τ1 τ2} →
      (Σ[ x ∈ Nat ] Σ[ d' ∈ iexp ]
         (d == (·λ x [ τ1 ] d') × Δ , ■ (x , τ1) ⊢ d' :: τ2))
      → cbf-arr Δ d τ1 τ2
    CBFCastArr : ∀{Δ d τ1 τ2} →
      (Σ[ d' ∈ iexp ] Σ[ τ1' ∈ typ ] Σ[ τ2' ∈ typ ]
         (d == (d' ⟨ τ1' ==> τ2' ⇒ τ1 ==> τ2 ⟩) ×
         (τ1' ==> τ2' ≠ τ1 ==> τ2) ×
         (Δ , ∅ ⊢ d' :: τ1' ==> τ2')))
      → cbf-arr Δ d τ1 τ2

  data cbf-prod : (Δ : hctx) (d : iexp) (τ1 τ2 : typ) → Set where
    CBFPairVal : ∀{Δ d τ1 τ2} →
              (Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ]
               (d == ⟨ d1 , d2 ⟩ ×
                Δ , ∅ ⊢ d1 :: τ1 ×
                Δ , ∅ ⊢ d2 :: τ2 ×
                d1 val ×
                d2 val))
              → cbf-prod Δ d τ1 τ2
    CBFPairBV : ∀{Δ d τ1 τ2} →
              (Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ]
               (d == ⟨ d1 , d2 ⟩ ×
                Δ , ∅ ⊢ d1 :: τ1 ×
                Δ , ∅ ⊢ d2 :: τ2 ×
                d1 boxedval ×
                d2 boxedval  ))
              → cbf-prod Δ d τ1 τ2
    CBFCastProd : ∀{Δ d τ1 τ2} →
                  (Σ[ d' ∈ iexp ] Σ[ τ1' ∈ typ ] Σ[ τ2' ∈ typ ]
                   (d == (d' ⟨ τ1' ⊗ τ2' ⇒ τ1 ⊗ τ2 ⟩) ×
                   (τ1' ⊗ τ2' ≠ τ1 ⊗ τ2) ×
                   (τ1' ⊗ τ2' ~ τ1 ⊗ τ2) ×
                   (d' boxedval) ×
                   (Δ , ∅ ⊢ d' :: τ1' ⊗ τ2')))
                  → cbf-prod Δ d τ1 τ2

  canonical-boxed-forms-arr : ∀{Δ d τ1 τ2 } →
                            Δ , ∅ ⊢ d :: (τ1 ==> τ2)  →
                            d boxedval →
                            cbf-arr Δ d τ1 τ2
  canonical-boxed-forms-arr (TAVar x₁) (BVVal ())
  canonical-boxed-forms-arr (TALam f wt) (BVVal v) = CBFLam (canonical-value-forms-arr (TALam f wt) v)
  canonical-boxed-forms-arr (TAAp wt wt₁) (BVVal ())
  canonical-boxed-forms-arr (TAEHole x x₁) (BVVal ())
  canonical-boxed-forms-arr (TANEHole x wt x₁) (BVVal ())
  canonical-boxed-forms-arr (TACast wt x) (BVVal ())
  canonical-boxed-forms-arr (TACast wt x) (BVArrCast x₁ bv) = CBFCastArr (_ , _ , _ , refl , x₁ , wt)
  canonical-boxed-forms-arr (TAFailedCast x x₁ x₂ x₃) (BVVal ())
  canonical-boxed-forms-arr (TAFst wt) (BVVal ())
  canonical-boxed-forms-arr (TASnd wt) (BVVal ())

  canonical-boxed-forms-hole : ∀{Δ d} →
                               Δ , ∅ ⊢ d :: ⦇·⦈ →
                               d boxedval →
                               Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
                                 ((d == d' ⟨ τ' ⇒ ⦇·⦈ ⟩) ×
                                  (τ' ground) ×
                                  (Δ , ∅ ⊢ d' :: τ'))
  canonical-boxed-forms-hole (TAVar x₁) (BVVal ())
  canonical-boxed-forms-hole (TAAp wt wt₁) (BVVal ())
  canonical-boxed-forms-hole (TAEHole x x₁) (BVVal ())
  canonical-boxed-forms-hole (TANEHole x wt x₁) (BVVal ())
  canonical-boxed-forms-hole (TACast wt x) (BVVal ())
  canonical-boxed-forms-hole (TACast wt x) (BVHoleCast x₁ bv) = _ , _ , refl , x₁ , wt
  canonical-boxed-forms-hole (TAFailedCast x x₁ x₂ x₃) (BVVal ())
  canonical-boxed-forms-hole (TAFst wt) (BVVal ())
  canonical-boxed-forms-hole (TASnd wt) (BVVal ())

  canonical-boxed-forms-prod : ∀{Δ d τ1 τ2 } →
                               Δ , ∅ ⊢ d :: (τ1 ⊗ τ2)  →
                               d boxedval →
                               cbf-prod Δ d τ1 τ2
  canonical-boxed-forms-prod (TAVar x₁) (BVVal ())
  canonical-boxed-forms-prod (TAAp wt wt₁) (BVVal ())
  canonical-boxed-forms-prod (TAEHole x x₁) (BVVal ())
  canonical-boxed-forms-prod (TANEHole x wt x₁) (BVVal ())
  canonical-boxed-forms-prod (TACast wt x) (BVVal ())
  canonical-boxed-forms-prod (TACast wt x) (BVProdCast x₁ bv) = CBFCastProd (_ , _ , _ , refl , x₁ , x , bv , wt)
  canonical-boxed-forms-prod (TAFailedCast wt x x₁ x₂) (BVVal ())
  canonical-boxed-forms-prod (TAFst wt) (BVVal ())
  canonical-boxed-forms-prod (TASnd wt) (BVVal ())
  canonical-boxed-forms-prod (TAPair wt wt₁) (BVVal (VPair x x₁)) = CBFPairVal (_ , _ , refl , wt , wt₁ , x , x₁)
  canonical-boxed-forms-prod (TAPair wt wt₁) (BVPair bv bv₁) = CBFPairBV (_ , _ , refl , wt , wt₁ , bv , bv₁)

  canonical-boxed-forms-coverage : ∀{Δ d τ} →
                                   Δ , ∅ ⊢ d :: τ →
                                   d boxedval →
                                   τ ≠ b →
                                   ((τ1 : typ) (τ2 : typ) → τ ≠ (τ1 ==> τ2)) →
                                   τ ≠ ⦇·⦈ →
                                   ((τ1 : typ) (τ2 : typ) → τ ≠ (τ1 ⊗ τ2)) →
                                   ⊥
  canonical-boxed-forms-coverage TAConst (BVVal x) nb na nh = λ _ → nb refl
  canonical-boxed-forms-coverage (TAVar x₁) (BVVal ()) nb na nh
  canonical-boxed-forms-coverage (TALam _ wt) (BVVal x₁) nb na nh = λ _ → na _ _ refl
  canonical-boxed-forms-coverage (TAAp wt wt₁) (BVVal ()) nb na nh
  canonical-boxed-forms-coverage (TAEHole x x₁) (BVVal ()) nb na nh
  canonical-boxed-forms-coverage (TANEHole x wt x₁) (BVVal ()) nb na nh
  canonical-boxed-forms-coverage (TACast wt x) (BVVal ()) nb na nh
  canonical-boxed-forms-coverage (TACast wt x) (BVArrCast x₁ bv) nb na nh = λ _ → na _ _ refl
  canonical-boxed-forms-coverage (TACast wt x) (BVHoleCast x₁ bv) nb na nh = λ _ → nh refl
  canonical-boxed-forms-coverage (TAFailedCast x x₁ x₂ x₃) (BVVal ())
  canonical-boxed-forms-coverage (TACast wt x) (BVProdCast x₁ bv) nb na nh = λ z → z _ _ refl
  canonical-boxed-forms-coverage (TAFst wt) (BVVal ()) nb na nh
  canonical-boxed-forms-coverage (TASnd wt) (BVVal ()) nb na nh
  canonical-boxed-forms-coverage (TAPair wt wt₁) (BVVal x) nb na nh = λ z → z _ _ refl
  canonical-boxed-forms-coverage (TAPair wt wt₁) (BVPair bv bv₁) nb na nh = λ z → z _ _ refl

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


text:
module Languages.FILL.Intermediate where

open import Utils.HaskellTypes
open import Languages.FILL.TypeSyntax

{-# IMPORT Languages.FILL.Intermediate #-}

data IPattern : Set where
  PTriv : IPattern
  PVar : String → IPattern
  PTensor : IPattern → IPattern → IPattern
  PPar : IPattern → IPattern → IPattern
{-# COMPILED_DATA IPattern Languages.FILL.Intermediate.IPattern
                           Languages.FILL.Intermediate.PTriv
                           Languages.FILL.Intermediate.PVar
                           Languages.FILL.Intermediate.PTensor
                           Languages.FILL.Intermediate.PPar #-}

data ITerm : Set where
  Var : String → ITerm
  Triv : ITerm
  Void : ITerm
  TTensor : ITerm → ITerm → ITerm
  TPar : ITerm → ITerm → ITerm
  Lam : String → Type → ITerm → ITerm
  Let : ITerm → Type → IPattern → ITerm → ITerm
  App : ITerm → ITerm → ITerm
{-# COMPILED_DATA ITerm Languages.FILL.Intermediate.ITerm
                        Languages.FILL.Intermediate.Var
                        Languages.FILL.Intermediate.Triv
                        Languages.FILL.Intermediate.Void
                        Languages.FILL.Intermediate.TTensor
                        Languages.FILL.Intermediate.TPar
                        Languages.FILL.Intermediate.Lam
                        Languages.FILL.Intermediate.Let
                        Languages.FILL.Intermediate.App #-}

max_stars_repo_name: heades/Agda-LLS

max_issues_repo_name: heades/Agda-LLS

max_forks_repo_name: heades/Agda-LLS


text:
module BTree.Complete.Alternative {A : Set} where

open import BTree {A}
open import BTree.Equality {A}

data _⋗_ : BTree → BTree → Set where
  ⋗lf : (x : A)
                → (node x leaf leaf) ⋗ leaf
  ⋗nd : {l r l' r' : BTree}
                → (x x' : A)
                → l ≃ r
                → l' ≃ r'
                → l ⋗ l'
                → (node x l r) ⋗ (node x' l' r')

mutual
  data _⋘_ : BTree → BTree → Set where
    lf⋘ : leaf ⋘ leaf
    ll⋘ : {l r l' r' : BTree}
                  → (x x' : A)
                  → (l⋘r : l ⋘ r)
                  → (l'≃r' : l' ≃ r')
                  → r ≃ l'
                  → (node x l r) ⋘ (node x' l' r')
    lr⋘ : {l r l' r' : BTree}
                  → (x x' : A)
                  → (l⋙r : l ⋙ r)
                  → (l'≃r' : l' ≃ r')
                  → l ⋗ l'
                  → (node x l r) ⋘ (node x' l' r')

  data _⋙_ : BTree → BTree → Set where
    ⋙lf : (x : A)
                  → (node x leaf leaf) ⋙ leaf
    ⋙rl : {l r l' r' : BTree}
                  → (x x' : A)
                  → (l≃r : l ≃ r)
                  → (l'⋘r' : l' ⋘ r')
                  → l ⋗ r'
                  → (node x l r) ⋙ (node x' l' r')
    ⋙rr : {l r l' r' : BTree}
                  → (x x' : A)
                  → (l≃r : l ≃ r)
                  → (l'⋙r' : l' ⋙ r')
                  →  l ≃ l'
                  → (node x l r) ⋙ (node x' l' r')

data Complete : BTree → Set where
  leaf : Complete leaf
  left : {l r : BTree}
                 (x : A)
                 → Complete l
                 → Complete r
                 → l ⋘ r
                 → Complete (node x l r)
  right : {l r : BTree}
                 (x : A)
                 → Complete l
                 → Complete r
                 → l ⋙ r
                 → Complete (node x l r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------------
-- The types used by the mirror function
------------------------------------------------------------------------------

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

module FOTC.Program.Mirror.Type where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.List

------------------------------------------------------------------------------
-- Tree terms.
postulate node : D → D → D

-- The mutually totality predicates

data Forest : D → Set  -- The list of rose trees (called forest).
data Tree   : D → Set  -- The rose tree type.

data Forest where
  fnil  : Forest []
  fcons : ∀ {t ts} → Tree t → Forest ts → Forest (t ∷ ts)
{-# ATP axioms fnil fcons #-}

data Tree where
  tree : ∀ d {ts} → Forest ts → Tree (node d ts)
{-# ATP axiom tree #-}

------------------------------------------------------------------------------
-- Mutual induction for Tree and Forest

-- Adapted from the mutual induction principles generate from Coq
-- 8.4pl4 using the command (see Coq'Art p. 401).
--
-- Scheme Tree_mutual_ind :=
--   Minimality for Tree Sort Prop
-- with Forest_mutual_ind :=
--   Minimality for Forest Sort Prop.

Tree-mutual-ind :
  {A B : D → Set} →
  (∀ d {ts} → Forest ts → B ts → A (node d ts)) →
  B [] →
  (∀ {t ts} → Tree t → A t → Forest ts → B ts → B (t ∷ ts)) →
  ∀ {t} → Tree t → A t

Forest-mutual-ind :
  {A B : D → Set} →
  (∀ d {ts} → Forest ts → B ts → A (node d ts)) →
  B [] →
  (∀ {t ts} → Tree t → A t → Forest ts → B ts → B (t ∷ ts)) →
  ∀ {ts} → Forest ts → B ts

Tree-mutual-ind hA B[] _ (tree d fnil) = hA d fnil B[]
Tree-mutual-ind hA B[] hB (tree d (fcons Tt Fts)) =
  hA d (fcons Tt Fts) (hB Tt (Tree-mutual-ind hA B[] hB Tt)
                          Fts (Forest-mutual-ind hA B[] hB Fts))

Forest-mutual-ind _  B[] _ fnil = B[]
Forest-mutual-ind hA B[] hB (fcons Tt Fts) =
  hB Tt (Tree-mutual-ind hA B[] hB Tt) Fts (Forest-mutual-ind hA B[] hB Fts)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Sometimes we can't infer a record type

module InferRecordTypes-1 where

bad = record { }

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Algebra.Structures.Bundles.Field

module Algebra.Linear.Construct.Matrix.Square
  {k ℓ} (K : Field k ℓ)
  where

open import Level using (_⊔_)
open import Data.Nat using (ℕ)
open import Data.Fin
open import Data.Product

open import Algebra.Structures.Field.Utils K
open import Algebra.Linear.Construct.Matrix K public

module F = Field K

private
  M : ℕ -> Set k
  M n = Matrix n n

  K' : Set k
  K' = F.Carrier

UpperTriangular : ℕ -> Set (k ⊔ ℓ)
UpperTriangular n = ∃ λ (A : M n) -> ∀ {i j} -> j ≤ i -> (A ⟪ i , j ⟫) F.≈ F.0#

LowerTriangular : ℕ -> Set (k ⊔ ℓ)
LowerTriangular n = ∃ λ (A : M n) -> ∀ {i j} -> i ≤ j -> (A ⟪ i , j ⟫) F.≈ F.0#

Invertible : ℕ -> Set (k ⊔ ℓ)
Invertible n = ∃₂ λ (A B : M n) -> (A * B) ≈ I n ×  (B * A) ≈ I n

trace : ∀ {n} -> M n n -> K'
trace A = vsum (V.tabulate λ i → A ⟪ i , i ⟫)

det : ∀ {n} -> M n -> K'
det A = {!!}

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
module Dave.Algebra.Naturals.Monus where
    open import Dave.Algebra.Naturals.Definition
    open import Dave.Algebra.Naturals.Addition

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

    infixl 6 _∸_

    ∸-zero : ∀ (n : ℕ) → 0 ∸ n ≡ 0
    ∸-zero zero = refl
    ∸-zero (suc n) = refl

    ∸-assoc-+ : ∀ (m n p : ℕ) → m ∸ n ∸ p ≡ m ∸ (n + p)
    ∸-assoc-+ m zero p = refl
    ∸-assoc-+ zero (suc n) p = ∸-zero p
    ∸-assoc-+ (suc m) (suc n) p = begin
        suc m ∸ suc n ∸ p ≡⟨⟩
        m ∸ n ∸ p ≡⟨ ∸-assoc-+ m n p ⟩
        m ∸ (n + p) ≡⟨⟩
        suc m ∸ suc (n + p) ≡⟨⟩
        suc m ∸ (suc n + p) ∎


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.CastPi {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening as T hiding (wk; wkTerm; wkEqTerm)
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Weakening
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Irrelevance as S
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Introductions.Sigma
open import Definition.LogicalRelation.Substitution.Introductions.Fst
open import Definition.LogicalRelation.Substitution.Introductions.Snd
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.Lambda
open import Definition.LogicalRelation.Substitution.Introductions.Application
open import Definition.LogicalRelation.Substitution.Introductions.Cast
open import Definition.LogicalRelation.Substitution.Introductions.Id
open import Definition.LogicalRelation.Substitution.Introductions.IdUPiPi
open import Definition.LogicalRelation.Substitution.Introductions.Transp
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
open import Definition.LogicalRelation.Substitution.MaybeEmbed
open import Definition.LogicalRelation.Substitution.Introductions.Universe
open import Definition.LogicalRelation.Substitution.Reduction
open import Definition.LogicalRelation.Substitution.Weakening
open import Definition.LogicalRelation.Substitution.Conversion
open import Definition.LogicalRelation.Substitution.ProofIrrelevance
open import Definition.LogicalRelation.Fundamental.Variable

open import Tools.Product
import Tools.PropositionalEquality as PE

wk2d : Term → Term
wk2d = U.wk (lift (lift (step id)))

wk1f-cast-subst : ∀ σ f A' A rA e →
  (wk1 (subst σ f) ∘ cast ⁰ (wk1 (subst σ A')) (wk1 (subst σ A)) (Idsym (Univ rA ⁰) (wk1 (subst σ A)) (wk1 (subst σ A')) (fst (wk1 (subst σ e)))) (var 0) ^ ⁰)
  PE.≡
  subst (repeat liftSubst (repeat liftSubst σ 1) 0) (wk1 f ∘ cast ⁰ (wk1 A') (wk1 A) (Idsym (Univ rA ⁰) (wk1 A) (wk1 A') (fst (wk1 e))) (var 0) ^ ⁰)
wk1f-cast-subst σ f A' A rA e = PE.cong₂ (λ X Y → X ∘ Y ^ ⁰) (PE.sym (Idsym-subst-lemma σ f))
  (PE.cong₃ (λ X Y Z → cast ⁰ X Y Z (var 0)) (PE.sym (Idsym-subst-lemma σ A')) (PE.sym (Idsym-subst-lemma σ A))
    (PE.trans (PE.cong₃ (λ X Y Z → Idsym (Univ rA ⁰) X Y Z) (PE.sym (Idsym-subst-lemma σ A)) (PE.sym (Idsym-subst-lemma σ A')) (PE.sym (Idsym-subst-lemma σ (fst e))))
      (PE.sym (subst-Idsym (liftSubst σ) (Univ rA ⁰) (wk1 A) (wk1 A') (fst (wk1 e))))))

B-cast-subst : ∀ σ A' A rA e B →
  subst (liftSubst σ) B [ cast ⁰ (wk1 (subst σ A')) (wk1 (subst σ A)) (Idsym (Univ rA ⁰) (wk1 (subst σ A)) (wk1 (subst σ A')) (fst (wk1 (subst σ e)))) (var 0) ]↑
  PE.≡
  subst (repeat liftSubst (repeat liftSubst σ 1) 0) (B [ cast ⁰ (wk1 A') (wk1 A) (Idsym (Univ rA ⁰) (wk1 A) (wk1 A') (fst (wk1 e))) (var 0) ]↑)
B-cast-subst σ A′ A rA e B = PE.trans (PE.cong (λ X → (subst (liftSubst σ) B) [ X ]↑)
  (PE.cong₃ (λ X Y Z → cast ⁰ X Y Z (var 0)) (PE.sym (Idsym-subst-lemma σ A′)) (PE.sym (Idsym-subst-lemma σ A))
      (PE.trans (PE.cong₃ (λ X Y Z → Idsym (Univ rA ⁰) X Y Z) (PE.sym (Idsym-subst-lemma σ A)) (PE.sym (Idsym-subst-lemma σ A′)) (PE.sym (Idsym-subst-lemma σ (fst e))))
      (PE.sym (subst-Idsym (liftSubst σ) (Univ rA ⁰) (wk1 A) (wk1 A′) (fst (wk1 e)))))))
  (PE.sym ((singleSubstLift↑ σ B _)))

wk2d11-111 : ∀ A → wk2d (wk1 (wk1 A)) PE.≡ wk1 (wk1 (wk1 A))
wk2d11-111 A = PE.trans (wk-comp (lift (lift (step id))) (step id) (wk1 A))
               (PE.trans (wk-comp (step (lift (step id))) (step id) A)
               (PE.trans (PE.sym (wk-comp (step (step id)) (step id) A)) (PE.sym (wk-comp (step id) (step id) (wk1 A)))))

wk2d1d-1d1d : ∀ A → wk2d (wk1d A) PE.≡ wk1d (wk1d A)
wk2d1d-1d1d A = PE.trans (wk-comp (lift (lift (step id))) (lift (step id)) A)
                (PE.trans PE.refl (PE.sym (wk-comp (lift (step id)) (lift (step id)) A)))

wk1∃-aux : ∀ A A' rA B B' →  wk1 (∃ Id (Univ rA ⁰) A A' ▹ (Π wk1 A' ^ rA ° ⁰ ▹
                             Id (U ⁰) (wk1d B [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A))
                                                                (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0) ]↑)
                                      (wk1d B') ° ¹ ° ¹))
                         PE.≡
                         ∃ Id (Univ rA ⁰) (wk1 A) (wk1 A') ▹ (Π wk1 (wk1 A') ^ rA ° ⁰ ▹
                           Id (U ⁰) (wk2d (wk1d B) [ cast ⁰ (wk2d (wk1 (wk1 A'))) (wk2d (wk1 (wk1 A)))
                                                                  (Idsym (Univ rA ⁰) (wk2d (wk1 (wk1 A))) (wk2d (wk1 (wk1 A'))) (var 1)) (var 0) ]↑)
                                    (wk1d (wk1d B')) ° ¹ ° ¹)
wk1∃-aux A A' rA B B' = PE.cong₃ (λ X Y Z → ∃ Id (Univ rA ⁰) (wk1 A) (wk1 A') ▹ Π X ^ rA ° ⁰ ▹ Id (U ⁰) Y Z ° ¹ ° ¹)
                             (PE.trans (wk-comp (lift (step id)) (step id) A') (PE.sym (wk-comp (step id) (step id) A')))
                             (PE.trans (wk-β↑ (wk1d B)) (PE.cong₃ (λ X Y Z → wk2d (wk1d B) [ cast ⁰ X Y Z (var 0) ]↑)
                             PE.refl PE.refl (wk-Idsym (lift (lift (step id))) (Univ rA ⁰) _ _ (var 1)) ))
                             (wk2d1d-1d1d B')

wk1∃ : ∀ A A' rA B B' → wk1 (∃ Id (Univ rA ⁰) A A' ▹ (Π wk1 A' ^ rA ° ⁰ ▹
                             Id (U ⁰) (wk1d B [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A))
                                                                (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0) ]↑)
                                      (wk1d B') ° ¹ ° ¹))
                         PE.≡
                         ∃ Id (Univ rA ⁰) (wk1 A) (wk1 A') ▹ (Π wk1 (wk1 A') ^ rA ° ⁰ ▹
                           Id (U ⁰) (wk1d (wk1d B) [ cast ⁰ (wk1 (wk1 (wk1 A'))) (wk1 (wk1 (wk1 A)))
                                                                  (Idsym (Univ rA ⁰) (wk1 (wk1 (wk1 A))) (wk1 (wk1 (wk1 A'))) (var 1)) (var 0) ]↑)
                                    (wk1d (wk1d B')) ° ¹ ° ¹)

wk1∃ A A' rA B B' = PE.trans (wk1∃-aux A A' rA B B') (PE.cong₃ (λ X Y Z → ∃ Id (Univ rA ⁰) (wk1 A) (wk1 A') ▹ Π (wk1 (wk1 A')) ^ rA ° ⁰ ▹ Id (U ⁰) (X [ Y ]↑) Z ° ¹ ° ¹)
                             (wk2d1d-1d1d B) (PE.cong₃ (λ X Y Z → cast ⁰ X Y Z (var 0)) (wk2d11-111 A') (wk2d11-111 A)
                                             (PE.cong₂ (λ X Y →   Idsym (Univ rA ⁰)  X Y (var 1)) (wk2d11-111 A) (wk2d11-111 A'))) PE.refl )

snd-cast-subst : ∀ A A' rA B B' e → Π wk1 (wk1 A') ^ rA ° ⁰ ▹
                                        Id (U ⁰) (wk1d (wk1d B) [ cast ⁰ (wk1 (wk1 (wk1 A'))) (wk1 (wk1 (wk1 A))) (Idsym (Univ rA ⁰) (wk1 (wk1 (wk1 A))) (wk1 (wk1 (wk1 A'))) (var 1)) (var 0) ]↑)
                                                 (wk1d (wk1d B')) ° ¹ ° ¹ [ fst (wk1 e) ]
                                    PE.≡
                                      Π (wk1 A') ^ rA ° ⁰ ▹
                                        Id (U ⁰) (wk1d B [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (fst (wk1 (wk1 e)))) (var 0) ]↑)
                                                 (wk1d B') ° ¹ ° ¹
snd-cast-subst A A' rA B B' e = PE.cong₃ (λ X Y Z → Π X ^ rA ° ⁰ ▹ Id (U ⁰) Y Z ° ¹ ° ¹)
  (wk1-singleSubst (wk1 A') _)
  (PE.trans (singleSubstLift↑ (sgSubst (fst (wk1 e))) (wk1d (wk1d B)) _)
    (PE.cong₂ (λ X Y → X [ Y ]↑) (wk1d-singleSubst (wk1d B) (fst (wk1 e)))
      (PE.cong₃ (λ X Y Z → cast ⁰ X Y Z (var 0)) (subst3wk A' (fst (wk1 e))) (subst3wk A (fst (wk1 e)))
        (PE.trans (subst-Idsym (liftSubst (sgSubst (fst (wk1 e)))) (Univ rA ⁰) (wk1 (wk1 (wk1 A))) (wk1 (wk1 (wk1 A'))) (var 1))
          (PE.cong₂ (λ X Y → Idsym (Univ rA ⁰) X Y (fst (wk1 (wk1 e)))) (subst3wk A (fst (wk1 e))) (subst3wk A' (fst (wk1 e))))))))
  (wk1d-singleSubst (wk1d B') (fst (wk1 e)))
  where
    subst3wk : ∀ t u → subst (liftSubst (sgSubst u)) (wk1 (wk1 (wk1 t))) PE.≡ wk1 (wk1 t)
    subst3wk t u = PE.trans (Idsym-subst-lemma (sgSubst u) (wk1 (wk1 t))) (PE.cong wk1 (wk1-singleSubst (wk1 t) u))

Id-cast-subst : ∀ A A' rA B B' e → Id (U ⁰) (wk1d B [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (fst (wk1 (wk1 e)))) (var 0) ]↑)
                                            (wk1d B')
                                      [ var 0 ]
                                   PE.≡
                                   Id (U ⁰) (B [ cast ⁰ (wk1 A') (wk1 A) (Idsym (Univ rA ⁰) (wk1 A) (wk1 A') (fst (wk1 e))) (var 0) ]↑)
                                                  B'
Id-cast-subst A A' rA B B' e = PE.cong₂ (Id (U ⁰))
  (PE.trans
    (PE.cong (λ X → X [ var 0 ]) (wk1d[]-[]↑ (wk1d B) _))
    (PE.trans aux (PE.sym (wk1d[]-[]↑ B _))) )
  (wkSingleSubstId B')
  where
    aux : (wk1d (wk1d B) [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (fst (wk1 (wk1 e)))) (var 0) ]) [ var 0 ]
      PE.≡ wk1d B [ cast ⁰ (wk1 A') (wk1 A) (Idsym (Univ rA ⁰) (wk1 A) (wk1 A') (fst (wk1 e))) (var 0) ]
    aux = PE.trans (singleSubstLift (wk1d (wk1d B)) _)
      (PE.cong₄ (λ X Y Z T → X [ cast ⁰ Y Z T (var 0) ])
        (wk1d-singleSubst (wk1d B) (var 0)) (wk1-singleSubst (wk1 A') (var 0)) (wk1-singleSubst (wk1 A) (var 0))
        (PE.trans (subst-Idsym _ (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (wk1 (wk1 (fst e))))
          (PE.cong₃ (λ X Y Z → Idsym (Univ rA ⁰) X Y Z) (wk1-singleSubst (wk1 A) (var 0)) (wk1-singleSubst (wk1 A') (var 0)) (wk1-singleSubst (wk1 (fst e)) (var 0)))))

cast-Πᵗᵛ-aux : ∀ {A B A' B' rA Γ e f} ([Γ] : ⊩ᵛ Γ) →
        let l    = ∞
            lΠ = ⁰
            [UA] = maybeEmbᵛ {A = Univ rA _} [Γ] (Uᵛ emb< [Γ])
            [UΠ] = maybeEmbᵛ {A = Univ ! _} [Γ] (Uᵛ emb< [Γ])
        in
           ([A] : Γ ⊩ᵛ⟨ l ⟩ A ^ [ rA , ι lΠ ] / [Γ])
           ([A'] : Γ ⊩ᵛ⟨ l ⟩ A' ^ [ rA , ι lΠ ] / [Γ])
           ([UB] : Γ ∙ A ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A])
           ([UB'] : Γ ∙ A' ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A'])
           ([A]ₜ : Γ ⊩ᵛ⟨ l ⟩ A ∷ Univ rA lΠ ^ [ ! , next lΠ ] / [Γ] / [UA])
           ([B]ₜ : Γ ∙ A ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ B ∷ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A] / (λ {Δ} {σ} → [UB] {Δ} {σ}))
           ([A']ₜ : Γ ⊩ᵛ⟨ l ⟩ A' ∷ Univ rA lΠ ^ [ ! , next lΠ ] / [Γ] / [UA])
           ([B']ₜ :  Γ ∙ A' ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ B' ∷ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A'] / (λ {Δ} {σ} → [UB'] {Δ} {σ}))
           ([Id] : Γ ⊩ᵛ⟨ l ⟩ Id (U lΠ) (Π A ^ rA ° lΠ ▹ B ° lΠ ° lΠ) (Π A' ^ rA ° lΠ  ▹ B' ° lΠ ° lΠ) ^ [ % , next lΠ ] / [Γ])
           ([e]ₜ : Γ ⊩ᵛ⟨ l ⟩ e ∷ Id (U lΠ) (Π A ^ rA ° lΠ ▹ B ° lΠ ° lΠ) (Π A' ^ rA ° lΠ  ▹ B' ° lΠ ° lΠ) ^ [ % , next lΠ ] / [Γ] / [Id])
           ([ΠAB] : Γ ⊩ᵛ⟨ l ⟩ Π A ^ rA ° lΠ ▹ B ° lΠ ° lΠ ^ [ ! , ι lΠ ] / [Γ])
           ([f]ₜ : Γ ⊩ᵛ⟨ l ⟩ f ∷ Π A ^ rA ° lΠ ▹ B ° lΠ ° lΠ ^ [ ! , ι lΠ ] / [Γ] / [ΠAB]) →
           ([Id-U-ΠΠ] : [ Γ ⊩ᵛ⟨ l ⟩ (Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° lΠ) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° lΠ))
                    ≡ ∃ (Id (Univ rA ⁰) A A') ▹
                      (Π (wk1 A') ^ rA ° ⁰ ▹ Id (U ⁰)
                        ((U.wk (lift (step id)) B) [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0) ]↑)
                        (U.wk (lift (step id)) B') ° ¹ ° ¹)
                  ∷ SProp ¹ ^ [ ! , next ¹ ] / [Γ] ] )
           →
           let [IdAA'] = Idᵛ {A = Univ rA ⁰} {t = A} {u = A'} [Γ] (λ {Δ} {σ} → [UA] {Δ} {σ}) [A]ₜ [A']ₜ
               [ΓId] = _∙_ {A = Id (Univ rA ⁰) A A'} [Γ] [IdAA']
               [wA'] = wk1ᵗᵛ {F = Id (Univ rA ⁰) A A'} {G = A'} {lG = ⁰} [Γ] [IdAA'] [A']ₜ
               [wA']' = wk1ᵛ {A = A'} {F = Id (Univ rA ⁰) A A'} [Γ] [IdAA'] [A']
               [wA]' = wk1ᵛ {A = A} {F = Id (Univ rA ⁰) A A'} [Γ] [IdAA'] [A]
               [wA] = wk1ᵗᵛ {F = Id (Univ rA ⁰) A A'} {G = A} {lG = ⁰} [Γ] [IdAA'] [A]ₜ
               [ΓIdA'] = _∙_ {A = wk1 A'} [ΓId] [wA']'
               [wwA']' = wk1ᵛ {A = wk1 A'} {F = wk1 A'}  [ΓId] [wA']' [wA']'
               [wwA'] = wk1ᵗᵛ {F = wk1 A'} {G = wk1 A'} {lG = ⁰} [ΓId] [wA']' [wA']
               [wwA] = wk1ᵗᵛ {F = wk1 A'} {G = wk1 A} {lG = ⁰} [ΓId] [wA']' [wA]
               [wwUA'] = λ {Δ} {σ} r → maybeEmbᵛ {A = Univ r _ } [ΓIdA'] (λ {Δ} {σ} → Uᵛ emb< [ΓIdA'] {Δ} {σ}) {Δ} {σ}
               [wwIdAA'] = Idᵛ {A = Univ rA ⁰} {t = wk1 (wk1 A)} {u = wk1 (wk1 A')} [ΓIdA'] (λ {Δ} {σ} → [wwUA'] {Δ} {σ} rA) [wwA] [wwA']
               [ΓA'] = (_∙_ {Γ} {A'} [Γ]  [A'])
               [w'A] = wk1ᵗᵛ {F = A'} {G = A} {lG = ⁰} [Γ] [A'] [A]ₜ
               [w'A'] = wk1ᵗᵛ {F = A'} {G = A'} {lG = ⁰} [Γ] [A'] [A']ₜ
               [w'A']' = wk1ᵛ {A = A'} {F = A'} [Γ] [A'] [A']
               [wUA] = maybeEmbᵛ {A = Univ rA _} [ΓA'] (λ {Δ} {σ} → Uᵛ emb< [ΓA'] {Δ} {σ})
               [wIdAA'] = Idᵛ {A = Univ rA ⁰} {t = wk1 A} {u = wk1 A'} [ΓA'] (λ {Δ} {σ} → [wUA] {Δ} {σ}) [w'A] [w'A']
               [ww'A']' = wk1ᵛ {A = wk1 A'} {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} [ΓA'] [wIdAA'] [w'A']'
               [ww'A'] = wk1ᵗᵛ {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} {G = wk1 A'} {lG = ⁰} [ΓA'] [wIdAA'] [w'A']
               [ΓA'Id] = _∙_ {A = Id (Univ rA ⁰) (wk1 A) (wk1 A')} [ΓA'] [wIdAA']
               [ΓA'IdA'] = _∙_ {A = wk1 (wk1 A')} [ΓA'Id] [ww'A']'
               [wwwUA'] = λ {Δ} {σ} r → maybeEmbᵛ {A = Univ r _ } [ΓA'IdA'] (λ {Δ} {σ} → Uᵛ emb< [ΓA'IdA'] {Δ} {σ}) {Δ} {σ}
               [www'A'] = wk1ᵗᵛ {F = wk1 (wk1 A')} {G = wk1 (wk1 A')} {lG = ⁰} [ΓA'Id] [ww'A']' [ww'A']
               [ww'A] = wk1ᵗᵛ {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} {G = wk1 A} {lG = ⁰} [ΓA'] [wIdAA'] [w'A]
               [www'A] = wk1ᵗᵛ {F = wk1 (wk1 A')} {G = wk1 (wk1 A)} {lG = ⁰} [ΓA'Id] [ww'A']' [ww'A]
               [wwwIdAA'] = Idᵛ {A = Univ rA ⁰} {t = wk1 (wk1 (wk1 A))} {u = wk1 (wk1 (wk1 A'))} [ΓA'IdA'] (λ {Δ} {σ} → [wwwUA'] {Δ} {σ} rA) [www'A] [www'A']
               [wwwU¹] = λ {Δ} {σ} r → Uᵛ {rU = r} ∞< [ΓA'Id] {Δ} {σ}
               Id-U-ΠΠ-res-end A A' B B' = Π (wk1 A') ^ rA ° ⁰ ▹ Id (U ⁰)
                                    ((wk1d B) [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0) ]↑)
                                    (wk1d B') ° ¹ ° ¹
           in
           ([Id-U-ΠΠ-res-end] : Γ ∙ A' ^ [ rA , ι ⁰ ] ∙ Id (Univ rA ⁰) (wk1 A) (wk1 A') ^ [ % , ι ¹ ] ⊩ᵛ⟨ ∞ ⟩
                        Id-U-ΠΠ-res-end (wk1 A) (wk1 A') (wk1d B) (wk1d B') ∷ SProp ¹ ^ [ ! , ∞ ] / [ΓA'Id] / (λ {Δ} {σ} → [wwwU¹] {Δ} {σ} %))
           ([var]ₜ : Γ ∙ A' ^ [ rA , ι ⁰ ] ⊩ᵛ⟨ ∞ ⟩ var 0 ∷ wk1 A' ^ [ rA , ι ⁰ ] / [ΓA'] / wk1ᵛ {A = A'} {F = A'} [Γ] [A'] [A'])
           ([var0']ₜ : Γ ∙ A' ^ [ rA , ι ⁰ ] ∙ Id (Univ rA ⁰) (wk1 A) (wk1 A') ^ [ % , ι ¹ ] ∙ wk1 (wk1 A') ^ [ rA , ι ⁰ ] ⊩ᵛ⟨ ∞ ⟩ var 0 ∷
                         wk1 (wk1 (wk1 A')) ^ [ rA , ι ⁰ ] / [ΓA'IdA'] / wk1ᵛ {A = wk1 (wk1 A')} {F = wk1 (wk1 A')} [ΓA'Id] [ww'A']' [ww'A']')
           ([var1']ₜ : Γ ∙ A' ^ [ rA , ι ⁰ ] ∙ Id (Univ rA ⁰) (wk1 A) (wk1 A') ^ [ % , ι ¹ ] ∙ wk1 (wk1 A') ^ [ rA , ι ⁰ ] ⊩ᵛ⟨ ∞ ⟩ var 1 ∷
                         Id (Univ rA ⁰) (wk1 (wk1 (wk1 A))) (wk1 (wk1 (wk1 A'))) ^ [ % , ι ¹ ] / [ΓA'IdA'] / [wwwIdAA'])
         → [ Γ ⊩ᵛ⟨ l ⟩ (cast lΠ (Π A ^ rA ° lΠ ▹ B ° lΠ ° lΠ) (Π A' ^ rA ° lΠ ▹ B' ° lΠ ° lΠ) e f) ≡
                       (lam A' ▹
                         (let a = cast lΠ (wk1 A') (wk1 A) (Idsym (Univ rA lΠ) (wk1 A) (wk1 A') (fst (wk1 e))) (var 0) in
                         cast lΠ (B [ a ]↑) B' ((snd (wk1 e)) ∘ (var 0) ^ ¹) ((wk1 f) ∘ a ^ lΠ)) ^ ⁰)
                       ∷ Π A' ^ rA ° lΠ ▹ B' ° lΠ ° lΠ ^ [ ! , ι lΠ ] / [Γ] ]

cast-Πᵗᵛ-aux {A} {B} {A'} {B'} {rA} {Γ} {e} {f}
        [Γ] [A] [A'] [UB] [UB'] [A]ₜ [B]ₜ [A']ₜ [B']ₜ [Id] [e]ₜ [ΠAB] [f]ₜ [Id-U-ΠΠ] [Id-U-ΠΠ-res-end] [var]ₜ [var0']ₜ [var1']ₜ =
  let l = ∞
      lΠ = ⁰
      [UA] = maybeEmbᵛ {A = Univ rA _} [Γ] (Uᵛ emb< [Γ])
      [UΠ] = maybeEmbᵛ {A = Univ ! _} [Γ] (Uᵛ emb< [Γ])
      ⊢AΔ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([UA] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([A]ₜ ⊢Δ [σ]))
      ⊢A'Δ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([UA] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([A']ₜ ⊢Δ [σ]))
      ⊢A = λ {Δ} {σ} ⊢Δ [σ] → escape (proj₁ ([A] {Δ} {σ} ⊢Δ [σ]))
      ⊢A' = λ {Δ} {σ} ⊢Δ [σ] → escape (proj₁ ([A'] {Δ} {σ} ⊢Δ [σ]))
      [ΓA]  = (_∙_ {Γ} {A} [Γ] [A])
      [ΓA'] = (_∙_ {Γ} {A'} [Γ]  [A'])
      ⊢BΔ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([UB] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([B]ₜ {Δ} {σ} ⊢Δ [σ]))
      [A]'  = univᵛ {A = A} [Γ] (≡is≤ PE.refl) (λ {Δ} {σ} → [UA] {Δ} {σ}) [A]ₜ
      [A']'  = univᵛ {A = A'} [Γ] (≡is≤ PE.refl) (λ {Δ} {σ} → [UA] {Δ} {σ}) [A']ₜ
      [B]'  = univᵛ {A = B} [ΓA] (≡is≤ PE.refl) (λ {Δ} {σ} → [UB] {Δ} {σ}) [B]ₜ
      [B]  = maybeEmbᵛ {A = B} [ΓA] [B]'
      [B']'  = univᵛ {A = B'} [ΓA'] (≡is≤ PE.refl) (λ {Δ} {σ} → [UB'] {Δ} {σ}) [B']ₜ
      [B']  = maybeEmbᵛ {A = B'} [ΓA'] [B']'
      ⊢B'Δ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([UB'] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([B']ₜ {Δ} {σ} ⊢Δ [σ]))
      [liftσ] = λ {Δ} {σ} ⊢Δ [σ] → liftSubstS {F = A} {σ = σ} {Δ = Δ} [Γ] ⊢Δ [A] [σ]
      [liftσ'] = λ {Δ} {σ} ⊢Δ [σ] → liftSubstS {F = A'} {σ = σ} {Δ = Δ} [Γ] ⊢Δ [A'] [σ]
      ⊢e = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([Id] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([e]ₜ {Δ} {σ} ⊢Δ [σ]))
      ⊢f = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([ΠAB] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([f]ₜ {Δ} {σ} ⊢Δ [σ]))
      [ΠAB'] = Πᵛ {A'} {B'} (≡is≤ PE.refl) (≡is≤ PE.refl) [Γ] [A'] [B']
      [ΓA'] = _∙_ {A = A'} [Γ]  [A']
      [wUA] = maybeEmbᵛ {A = Univ rA _} [ΓA'] (λ {Δ} {σ} → Uᵛ emb< [ΓA'] {Δ} {σ})
      [wUA]ᵗ = Uᵗᵛ [ΓA']
      [IdAA']ₜ = Idᵗᵛ {A = Univ rA ⁰} {t = A} {u = A'} [Γ] (λ {Δ} {σ} → [UA] {Δ} {σ}) [A]ₜ [A']ₜ (Uᵗᵛ [Γ])
      [IdAA'] = Idᵛ {A = Univ rA ⁰} {t = A} {u = A'} [Γ] (λ {Δ} {σ} → [UA] {Δ} {σ}) [A]ₜ [A']ₜ
      [ΓId] = _∙_ {A = Id (Univ rA ⁰) A A'} [Γ] [IdAA']
      [wA'] = wk1ᵗᵛ {F = Id (Univ rA ⁰) A A'} {G = A'} {lG = ⁰} [Γ] [IdAA'] [A']ₜ
      [wA']' = wk1ᵛ {A = A'} {F = Id (Univ rA ⁰) A A'} [Γ] [IdAA'] [A']
      [wA]' = wk1ᵛ {A = A} {F = Id (Univ rA ⁰) A A'} [Γ] [IdAA'] [A]
      [wA] = wk1ᵗᵛ {F = Id (Univ rA ⁰) A A'} {G = A} {lG = ⁰} [Γ] [IdAA'] [A]ₜ
      [ΓIdA'] = _∙_ {A = wk1 A'} [ΓId] [wA']'
      [wwU¹] = λ {Δ} {σ} r → Uᵛ {rU = r} ∞< [ΓIdA'] {Δ} {σ}
      [wwUA'] = λ {Δ} {σ} r → maybeEmbᵛ {A = Univ r _ } [ΓIdA'] (λ {Δ} {σ} → Uᵛ emb< [ΓIdA'] {Δ} {σ}) {Δ} {σ}
      [ΓIdA] = _∙_ {A = wk1 A} [ΓId] [wA]'
      [wwA'] = wk1ᵗᵛ {F = wk1 A'} {G = wk1 A'} {lG = ⁰} [ΓId] [wA']' [wA']
      [wwA] = wk1ᵗᵛ {F = wk1 A'} {G = wk1 A} {lG = ⁰} [ΓId] [wA']' [wA]
      [wwA']' = wk1ᵛ {A = wk1 A'} {F = wk1 A'}  [ΓId] [wA']' [wA']'
      [wwA]' = wk1ᵛ {A = wk1 A} {F = wk1 A'}  [ΓId] [wA']' [wA]'
      [wwU0A] = maybeEmbᵛ {A = Univ ! _ } [ΓIdA] (λ {Δ} {σ} → Uᵛ emb< [ΓIdA] {Δ} {σ})
      [wB'] = wk1dᵗᵛ {F = A'} {F' = Id (Univ rA ⁰) A A'} {G = B'} [Γ] [A'] [IdAA'] (λ {Δ} {σ} → [UB'] {Δ} {σ}) (λ {Δ} {σ} → [wwUA'] {Δ} {σ} !) [B']ₜ
      [wB] = wk1dᵗᵛ {F = A} {F' = Id (Univ rA ⁰) A A'} {G = B} [Γ] [A] [IdAA'] (λ {Δ} {σ} → [UB] {Δ} {σ}) (λ {Δ} {σ} → [wwU0A] {Δ} {σ}) [B]ₜ
      [wwIdAA'] = Idᵛ {A = Univ rA ⁰} {t = wk1 (wk1 A)} {u = wk1 (wk1 A')} [ΓIdA'] (λ {Δ} {σ} → [wwUA'] {Δ} {σ} rA) [wwA] [wwA']
      [wwIdA'A] = Idᵛ {A = Univ rA ⁰} {t = wk1 (wk1 A')} {u = wk1 (wk1 A)} [ΓIdA'] (λ {Δ} {σ} → [wwUA'] {Δ} {σ} rA) [wwA'] [wwA]
      Id-U-ΠΠ-res-end A A' B B' = Π (wk1 A') ^ rA ° ⁰ ▹ Id (U ⁰)
                                    ((wk1d B) [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0) ]↑)
                                    (wk1d B') ° ¹ ° ¹
      Id-U-ΠΠ-left = Id (U lΠ) (Π A ^ rA ° lΠ ▹ B ° lΠ ° lΠ) (Π A' ^ rA ° lΠ  ▹ B' ° lΠ ° lΠ)
      Id-U-ΠΠ-res A A' B B' = ∃ (Id (Univ rA ⁰) A A') ▹ Id-U-ΠΠ-res-end A A' B B'
      [wU¹] = λ {Δ} {σ} r → Uᵛ {rU = r} ∞< [ΓA'] {Δ} {σ}
      modelsTermEq [SProp] _ [Id-U-ΠΠ-res] [eq] = [Id-U-ΠΠ]
      [Id-U-ΠΠ-res]' = maybeEmbᵛ {A = Id-U-ΠΠ-res  A A' B B'}  [Γ] (univᵛ {A = Id-U-ΠΠ-res  A A' B B'} [Γ] (≡is≤ PE.refl) [SProp] [Id-U-ΠΠ-res])
      [conve]ₜ = convᵛ {t = e} {A = Id-U-ΠΠ-left} {B = Id-U-ΠΠ-res  A A' B B'}
                       [Γ] [Id] [Id-U-ΠΠ-res]'
                       (univEqᵛ {A = Id-U-ΠΠ-left} {B = Id-U-ΠΠ-res  A A' B B'} [Γ] [SProp] [Id] [eq]) [e]ₜ
      [we] = wk1Termᵛ {F = A'} {G = Id-U-ΠΠ-res A A' B B'} {t = e} [Γ] [A'] [Id-U-ΠΠ-res]' [conve]ₜ
      [w'A] = wk1ᵗᵛ {F = A'} {G = A} {lG = ⁰} [Γ] [A'] [A]ₜ
      [w'A]' = wk1ᵛ {A = A} {F = A'} [Γ] [A'] [A]
      [w'A]⁰ = wk1ᵛ {A = A} {F = A'} [Γ] [A'] [A]'
      [w'A'] = wk1ᵗᵛ {F = A'} {G = A'} {lG = ⁰} [Γ] [A'] [A']ₜ
      [w'A']' = wk1ᵛ {A = A'} {F = A'} [Γ] [A'] [A']
      [w'A']⁰ = wk1ᵛ {A = A'} {F = A'} [Γ] [A'] [A']'
      [wIdA'A] = Idᵛ {A = Univ rA ⁰} {t = wk1 A'} {u = wk1 A} [ΓA'] (λ {Δ} {σ} → [wUA] {Δ} {σ}) [w'A'] [w'A]
      [wIdAA'] = Idᵛ {A = Univ rA ⁰} {t = wk1 A} {u = wk1 A'} [ΓA'] (λ {Δ} {σ} → [wUA] {Δ} {σ}) [w'A] [w'A']
      [wIdAA']ᵗ = Idᵗᵛ {A = Univ rA ⁰} {t = wk1 A} {u = wk1 A'} [ΓA'] (λ {Δ} {σ} → [wUA] {Δ} {σ}) [w'A] [w'A'] (λ {Δ} {σ} → Uᵗᵛ [ΓA'] {Δ} {σ})
      [wIdAA']ₜ = Idᵗᵛ {A = Univ rA ⁰} {t = wk1 A} {u = wk1 A'} [ΓA'] (λ {Δ} {σ} → [wUA] {Δ} {σ}) [w'A] [w'A'] (λ {Δ} {σ} → Uᵗᵛ [ΓA'] {Δ} {σ})
      [ww'A']' = wk1ᵛ {A = wk1 A'} {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} [ΓA'] [wIdAA'] [w'A']'
      [ww'A'] = wk1ᵗᵛ {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} {G = wk1 A'} {lG = ⁰} [ΓA'] [wIdAA'] [w'A']
      [ww'A]' = wk1ᵛ {A = wk1 A} {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} [ΓA'] [wIdAA'] [w'A]'
      [ww'A] = wk1ᵗᵛ {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} {G = wk1 A} {lG = ⁰} [ΓA'] [wIdAA'] [w'A]
      [ΓA'A'] = _∙_ {A = wk1 A'} [ΓA'] [w'A']'
      [ww'UA'] = λ {Δ} {σ} r → maybeEmbᵛ {A = Univ r _ } [ΓA'A'] (λ {Δ} {σ} → Uᵛ emb< [ΓA'A'] {Δ} {σ}) {Δ} {σ}
      [ΓA'A] = _∙_ {A = wk1 A} [ΓA'] [w'A]'
      [ww'UA] = λ {Δ} {σ} r → maybeEmbᵛ {A = Univ r _ } [ΓA'A] (λ {Δ} {σ} → Uᵛ emb< [ΓA'A] {Δ} {σ}) {Δ} {σ}
      [ΓA'Id] = _∙_ {A = Id (Univ rA ⁰) (wk1 A) (wk1 A')} [ΓA'] [wIdAA']
      [ΓA'IdA'] = _∙_ {A = wk1 (wk1 A')} [ΓA'Id] [ww'A']'
      [www'UA'] = λ {Δ} {σ} r → maybeEmbᵛ {A = Univ r _ } [ΓA'IdA'] (λ {Δ} {σ} → Uᵛ emb< [ΓA'IdA'] {Δ} {σ}) {Δ} {σ}
      [ΓA'IdA] = _∙_ {A = wk1 (wk1 A)} [ΓA'Id] [ww'A]'
      [www'UA] = λ {Δ} {σ} r → maybeEmbᵛ {A = Univ r _ } [ΓA'IdA] (λ {Δ} {σ} → Uᵛ emb< [ΓA'IdA] {Δ} {σ}) {Δ} {σ}
      [w'B'] = wk1dᵗᵛ {F = A'} {F' = A'} {G = B'} [Γ] [A'] [A'] (λ {Δ} {σ} → [UB'] {Δ} {σ}) ((λ {Δ} {σ} → [ww'UA'] {Δ} {σ} !)) [B']ₜ
      [ww'B'] = wk1dᵗᵛ {F = wk1 A'} {F' = Id (Univ rA ⁰) (wk1 A) (wk1 A')} {G = wk1d B'} [ΓA'] [w'A']' [wIdAA'] (λ {Δ} {σ} → [ww'UA'] {Δ} {σ} !) (λ {Δ} {σ} → [www'UA'] {Δ} {σ} !) [w'B']
      [w'B] = wk1dᵗᵛ {F = A} {F' = A'} {G = B} [Γ] [A] [A'] (λ {Δ} {σ} → [UB] {Δ} {σ}) ((λ {Δ} {σ} → [ww'UA] {Δ} {σ} !)) [B]ₜ
      [ww'B] = wk1dᵗᵛ {F = wk1 A} {F' = Id (Univ rA ⁰) (wk1 A) (wk1 A')} {G = wk1d B} [ΓA'] [w'A]' [wIdAA'] (λ {Δ} {σ} → [ww'UA] {Δ} {σ} !) (λ {Δ} {σ} → [www'UA] {Δ} {σ} !) [w'B]
      [www'A']' = wk1ᵛ {A = wk1 (wk1 A')} {F = wk1 (wk1 A') } [ΓA'Id] [ww'A']' [ww'A']'
      [www'A'] = wk1ᵗᵛ {F = wk1 (wk1 A')} {G = wk1 (wk1 A')} {lG = ⁰} [ΓA'Id] [ww'A']' [ww'A']
      [www'A]' = wk1ᵛ {A = wk1 (wk1 A)} {F = wk1 (wk1 A')} [ΓA'Id] [ww'A']' [ww'A]'
      [www'A] = wk1ᵗᵛ {F = wk1 (wk1 A')} {G = wk1 (wk1 A)} {lG = ⁰} [ΓA'Id] [ww'A']' [ww'A]
      [wwU¹] = λ {Δ} {σ} r → Uᵛ {rU = r} ∞< [ΓA'A'] {Δ} {σ}
      [wwwU¹] = λ {Δ} {σ} r → Uᵛ {rU = r} ∞< [ΓA'Id] {Δ} {σ}
      Id-U-ΠΠ-res-end-wk1d = Id-U-ΠΠ-res-end (wk1 A) (wk1 A') (wk1d B) (wk1d B')
      Id-U-ΠΠ-res-wk1d = Id-U-ΠΠ-res (wk1 A) (wk1 A') (wk1d B) (wk1d B')
      [Id-U-ΠΠ-res-end]' = maybeEmbᵛ {A = Id-U-ΠΠ-res-end-wk1d} [ΓA'Id]
                                    (univᵛ {A = Id-U-ΠΠ-res-end-wk1d} [ΓA'Id] (≡is≤ PE.refl)
                                    (λ {Δ} {σ} → [wwwU¹] {Δ} {σ} %) [Id-U-ΠΠ-res-end])
      [we]' = S.irrelevanceTerm′ {A = wk1 (Id-U-ΠΠ-res A A' B B')} {A′ = Id-U-ΠΠ-res-wk1d} {t = wk1 e}
                                 (wk1∃ A A' rA B B')
                                 PE.refl [ΓA'] [ΓA'] (wk1ᵛ {A = Id-U-ΠΠ-res A A' B B'} {F = A'} [Γ] [A'] [Id-U-ΠΠ-res]')
                                 (∃ᵛ {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} {G = Id-U-ΠΠ-res-end-wk1d} [ΓA'] [wIdAA']
                                            [Id-U-ΠΠ-res-end]') [we]
      [fst] = fstᵛ {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} {G = Id-U-ΠΠ-res-end-wk1d} {tu = wk1 e}
                             [ΓA'] [wIdAA'] [Id-U-ΠΠ-res-end]'
                               (λ {Δ} {σ} → [wwwU¹] {Δ} {σ} %) [wIdAA']ᵗ [Id-U-ΠΠ-res-end]
                               [we]'
      [wfste] : Γ ∙ A' ^ [ rA , ι ⁰ ] ⊩ᵛ⟨ ∞ ⟩ Idsym (Univ rA ⁰) (wk1 A) (wk1 A') (fst (wk1 e)) ∷ Id (Univ rA ⁰) (wk1 A') (wk1 A) ^ [ % , ι ¹ ] / [ΓA'] / [wIdA'A]
      [wfste] = IdSymᵗᵛ {A = Univ rA ⁰} {t = wk1 A} {u = wk1 A'} {e = fst (wk1 e)} [ΓA'] (λ {Δ} {σ} → [wU¹] {Δ} {σ} !)
                       (λ {Δ} {σ} → [wUA]ᵗ {Δ} {σ}) (λ {Δ} {σ} → [wUA] {Δ} {σ})
                       [w'A] [w'A'] [wIdAA'] [wIdA'A] [fst]

      cast-Π-a A A' e = cast ⁰ (wk1 A') (wk1 A) (Idsym (Univ rA ⁰) (wk1 A) (wk1 A') (fst (wk1 e))) (var 0)
      [cast-Π-a] : Γ ∙ A' ^ [ rA , ι ⁰ ]  ⊩ᵛ⟨ ∞ ⟩ cast-Π-a A A' e ∷ wk1 A ^ [ rA , ι ⁰ ] / [ΓA'] / wk1ᵛ {A = A} {F = A'} [Γ] [A'] [A]
      [cast-Π-a] = castᵗᵛ {wk1 A'} {wk1 A} {t = var 0} {e = Idsym (Univ rA ⁰) (wk1 A) (wk1 A') (fst (wk1 e))} [ΓA']
                          (λ {Δ} {σ} → [wUA] {Δ} {σ}) [w'A'] [w'A]
                         (wk1ᵛ {A = A'} {F = A'} [Γ] [A'] [A'])   (wk1ᵛ {A = A} {F = A'} [Γ] [A'] [A])
                         [var]ₜ [wIdA'A] [wfste]
      B[cast-Π-a]↑ₜ = subst↑STerm {F = A'} {F' = A} {G = B} {t = cast-Π-a A A' e} [Γ] [A'] [A]
                                  (λ {Δ} {σ} → [UB'] {Δ} {σ}) (λ {Δ} {σ} → [UB] {Δ} {σ}) [B]ₜ [cast-Π-a]
      [f°cast-Π-a] = appᵛ↑ {F = A} {F' = A'} {G = B} {t = wk1 f} {u = cast-Π-a A A' e} (≡is≤ PE.refl) (≡is≤ PE.refl) [Γ] [A] [A'] [B] [ΠAB]
                          (wk1Termᵛ {F = A'} {G =  Π A ^ rA ° ⁰ ▹ B ° ⁰ ° lΠ} {t = f} [Γ] [A'] [ΠAB] [f]ₜ)
                          [cast-Π-a]
      [wIdBB'] : Γ ∙ A' ^ [ rA , ι ⁰ ] ⊩ᵛ⟨ ∞ ⟩ Id (Univ ! ⁰) (B [ cast-Π-a A A' e ]↑) B' ^ [ % , ι ¹ ] / [ΓA']
      [wIdBB'] = Idᵛ {A = Univ ! ⁰} {t = B [ cast-Π-a A A' e ]↑} {u = B'} [ΓA'] (λ {Δ} {σ} → [UB'] {Δ} {σ})
                     B[cast-Π-a]↑ₜ [B']ₜ
      [snd] = sndᵛ {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} {G = Id-U-ΠΠ-res-end-wk1d} {tu = wk1 e}
                             [ΓA'] [wIdAA'] [Id-U-ΠΠ-res-end]'
                               (λ {Δ} {σ} → [wwwU¹] {Δ} {σ} %) [wIdAA']ᵗ [Id-U-ΠΠ-res-end]
                               [we]'
      [sndType]' = S.irrelevance′ {A = Id-U-ΠΠ-res-end-wk1d [ fst (wk1 e) ]}
                                  {A′ = Π (wk1 A') ^ rA ° ⁰ ▹
                                        Id (U ⁰) ((wk1d B) [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (fst (wk1 (wk1 e)))) (var 0) ]↑)
                                                 (wk1d B') ° ¹ ° ¹}
                                  (snd-cast-subst A A' rA B B' e) [ΓA'] [ΓA']
                                  (substS {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} {G = Id-U-ΠΠ-res-end-wk1d} {fst (wk1 e)} [ΓA']
                                            [wIdAA'] [Id-U-ΠΠ-res-end]' [fst])
      [snd]' = S.irrelevanceTerm′ {A = Id-U-ΠΠ-res-end-wk1d [ fst (wk1 e) ]}
                                  {A′ = Π (wk1 A') ^ rA ° ⁰ ▹
                                        Id (U ⁰) ((wk1d B) [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (fst (wk1 (wk1 e)))) (var 0) ]↑)
                                                 (wk1d B') ° ¹ ° ¹}
                                  {t = snd (wk1 e)}
                                  (snd-cast-subst A A' rA B B' e) PE.refl [ΓA'] [ΓA']
                                  (substS {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} {G = Id-U-ΠΠ-res-end-wk1d} {fst (wk1 e)} [ΓA']
                                           [wIdAA'] [Id-U-ΠΠ-res-end]' [fst])
                                  [sndType]' [snd]
      [wsnde] : Γ ∙ A' ^ [ rA , ι ⁰ ] ⊩ᵛ⟨ ∞ ⟩ (snd (wk1 e)) ∘ (var 0) ^ ¹ ∷ Id (Univ ! ⁰) (B [ cast-Π-a A A' e ]↑) B' ^ [ % , ι ¹ ] / [ΓA'] / [wIdBB']
      [wsnde] = let X = appᵛ {F = wk1 A'}
                            {G = Id (U ⁰)
                                    ((wk1d B) [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (fst (wk1 (wk1 e)))) (var 0) ]↑)
                                    (wk1d B')}
                                    {t = snd (wk1 e)} {u = var 0} [ΓA'] [w'A']'
                                    [sndType]' [snd]' [var]ₜ
                 in S.irrelevanceTerm′ {A = (Id (U ⁰) ((wk1d B) [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (fst (wk1 (wk1 e)))) (var 0) ]↑)
                                                      (wk1d B'))  [ var 0 ]}
                                       {A′ = Id (Univ ! ⁰) (B [ cast-Π-a A A' e ]↑) B'}
                                       {t = (snd (wk1 e)) ∘ (var 0) ^ ¹}
                                       (Id-cast-subst A A' rA B B' e) PE.refl [ΓA'] [ΓA']
                                       (substSΠ {wk1 A'}
                                                {Id (U ⁰) (wk1d B [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (fst (wk1 (wk1 e)))) (var 0) ]↑)
                                                          (wk1d B')}
                                                {var 0} [ΓA'] [w'A']'
                                                [sndType]' [var]ₜ )
                                       [wIdBB'] X

      cast-Π-res A A' B B' e f =
                 cast ⁰ (B [ cast-Π-a A A' e ]↑) B' ((snd (wk1 e)) ∘ (var 0) ^ ¹) ((wk1 f) ∘ cast-Π-a A A' e ^ ⁰)
      [cast-Π-res] : Γ ⊩ᵛ⟨ ∞ ⟩ lam A' ▹ cast-Π-res A A' B B' e f ^ ⁰ ∷ Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ] / [Γ] / [ΠAB']
      [cast-Π-res] = lamᵛ {F = A'} {G = B'} {t = cast-Π-res A A' B B' e f} (≡is≤ PE.refl) (≡is≤ PE.refl) [Γ] [A'] [B']
                          (castᵗᵛ {B [ cast-Π-a A A' e ]↑} {B'} {t = (wk1 f) ∘ cast-Π-a A A' e ^ ⁰} {e = (snd (wk1 e)) ∘ (var 0) ^ ¹}
                                  [ΓA'] (λ {Δ} {σ} → [UB'] {Δ} {σ}) B[cast-Π-a]↑ₜ [B']ₜ (subst↑S {F = A'} {G = B} {F' = A} [Γ] [A'] [A] [B] [cast-Π-a]) [B']
                                  [f°cast-Π-a] [wIdBB'] [wsnde])
      [cast-Π] : Γ ⊩ᵛ cast ⁰ (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰) e f ⇒ lam A' ▹ cast-Π-res A A' B B' e f ^ ⁰ ∷ Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰ ^ ι ⁰ / [Γ]
      [cast-Π] = λ {Δ} {σ} ⊢Δ [σ] → let Aσ  = ⊢AΔ {Δ} {σ} ⊢Δ [σ]
                                        Bσ  = ⊢BΔ {Δ ∙ subst σ A ^ _} {liftSubst σ} (⊢Δ ∙ ⊢A {Δ} {σ} ⊢Δ [σ]) ([liftσ] {Δ} {σ} ⊢Δ [σ])
                                        A'σ = ⊢A'Δ {Δ} {σ} ⊢Δ [σ]
                                        B'σ = ⊢B'Δ {Δ ∙ subst σ A' ^ _} {liftSubst σ} (⊢Δ ∙ ⊢A' {Δ} {σ} ⊢Δ [σ]) ([liftσ'] {Δ} {σ} ⊢Δ [σ])
                                        eσ  = ⊢e {Δ} {σ} ⊢Δ [σ]
                                        fσ  = ⊢f {Δ} {σ} ⊢Δ [σ]
                                        X : Δ ⊢ (cast ⁰ (Π (subst σ A) ^ rA ° ⁰ ▹ (subst (liftSubst σ) B) ° ⁰ ° ⁰) (Π (subst σ A') ^ rA ° ⁰ ▹ (subst (liftSubst σ) B') ° ⁰ ° ⁰) (subst σ e) (subst σ f))
                                                  ⇒ lam (subst σ A') ▹ cast-Π-res (subst σ A) (subst σ A') (subst (liftSubst σ) B) (subst (liftSubst σ) B') (subst σ e) (subst σ f) ^ ⁰
                                                  ∷ Π (subst σ A') ^ rA ° ⁰ ▹ (subst (liftSubst σ) B') ° ⁰  ° ⁰ ^ ι ⁰
                                        X = cast-Π {Δ} {subst σ A} {subst σ A'} {rA} {subst (liftSubst σ) B} {subst (liftSubst σ) B'} {subst σ e} {subst σ f} Aσ Bσ A'σ B'σ eσ fσ
                                     in PE.subst (λ BB → Δ ⊢ subst σ (cast ⁰ (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰) e f) ⇒ lam subst σ A' ▹ BB ^ ⁰ ∷ subst σ (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰) ^ ι ⁰ )
                                                 (PE.cong₄ (cast ⁰)
                                                           (B-cast-subst  σ A' A rA e B)
                                                           PE.refl (PE.cong₂ (λ X Y → snd X ∘ Y ^ ¹) (PE.sym (Idsym-subst-lemma σ e)) PE.refl) (wk1f-cast-subst σ f A' A rA e)) X
      [id] , [eq] = redSubstTermᵛ {Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰} {cast ⁰ (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰) e f} {lam A' ▹ cast-Π-res A A' B B' e f ^ ⁰}
                                  [Γ] (λ {Δ} {σ} ⊢Δ [σ] → [cast-Π] {Δ} {σ} ⊢Δ [σ])
                                  [ΠAB'] [cast-Π-res]

   in modelsTermEq [ΠAB'] [id] [cast-Π-res] [eq]

cast-Πᵗᵛ : ∀ {A B A' B' rA Γ e f} ([Γ] : ⊩ᵛ Γ) →
        let l    = ∞
            lΠ = ⁰
            [UA] = maybeEmbᵛ {A = Univ rA _} [Γ] (Uᵛ emb< [Γ])
            [UΠ] = maybeEmbᵛ {A = Univ ! _} [Γ] (Uᵛ emb< [Γ])
        in
           ([A] : Γ ⊩ᵛ⟨ l ⟩ A ^ [ rA , ι lΠ ] / [Γ])
           ([A'] : Γ ⊩ᵛ⟨ l ⟩ A' ^ [ rA , ι lΠ ] / [Γ])
           ([UB] : Γ ∙ A ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A])
           ([UB'] : Γ ∙ A' ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A'])
           ([A]ₜ : Γ ⊩ᵛ⟨ l ⟩ A ∷ Univ rA lΠ ^ [ ! , next lΠ ] / [Γ] / [UA])
           ([B]ₜ : Γ ∙ A ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ B ∷ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A] / (λ {Δ} {σ} → [UB] {Δ} {σ}))
           ([A']ₜ : Γ ⊩ᵛ⟨ l ⟩ A' ∷ Univ rA lΠ ^ [ ! , next lΠ ] / [Γ] / [UA])
           ([B']ₜ :  Γ ∙ A' ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ B' ∷ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A'] / (λ {Δ} {σ} → [UB'] {Δ} {σ}))
           ([Id] : Γ ⊩ᵛ⟨ l ⟩ Id (U lΠ) (Π A ^ rA ° lΠ ▹ B ° lΠ ° lΠ) (Π A' ^ rA ° lΠ  ▹ B' ° lΠ ° lΠ) ^ [ % , next lΠ ] / [Γ])
           ([e]ₜ : Γ ⊩ᵛ⟨ l ⟩ e ∷ Id (U lΠ) (Π A ^ rA ° lΠ ▹ B ° lΠ ° lΠ) (Π A' ^ rA ° lΠ  ▹ B' ° lΠ ° lΠ) ^ [ % , next lΠ ] / [Γ] / [Id])
           ([ΠAB] : Γ ⊩ᵛ⟨ l ⟩ Π A ^ rA ° lΠ ▹ B ° lΠ ° lΠ ^ [ ! , ι lΠ ] / [Γ])
           ([f]ₜ : Γ ⊩ᵛ⟨ l ⟩ f ∷ Π A ^ rA ° lΠ ▹ B ° lΠ ° lΠ ^ [ ! , ι lΠ ] / [Γ] / [ΠAB]) →
           [ Γ ⊩ᵛ⟨ l ⟩ (cast lΠ (Π A ^ rA ° lΠ ▹ B ° lΠ ° lΠ) (Π A' ^ rA ° lΠ ▹ B' ° lΠ ° lΠ) e f) ≡
                       (lam A' ▹
                         (let a = cast lΠ (wk1 A') (wk1 A) (Idsym (Univ rA lΠ) (wk1 A) (wk1 A') (fst (wk1 e))) (var 0) in
                         cast lΠ (B [ a ]↑) B' ((snd (wk1 e)) ∘ (var 0) ^ ¹) ((wk1 f) ∘ a ^ ⁰)) ^ ⁰)
                       ∷ Π A' ^ rA ° lΠ ▹ B' ° lΠ ° lΠ ^ [ ! , ι lΠ ] / [Γ] ]

abstract

  cast-Πᵗᵛ {A} {B} {A'} {B'} {rA} {Γ} {e} {f}
           [Γ] [A] [A'] [UB] [UB'] [A]ₜ [B]ₜ [A']ₜ [B']ₜ [Id] [e]ₜ [ΠAB] [f]ₜ =
    let l = ∞
        lΠ = ⁰
        [UA] = maybeEmbᵛ {A = Univ rA _} [Γ] (Uᵛ emb< [Γ])
        [IdAA'] = Idᵛ {A = Univ rA ⁰} {t = A} {u = A'} [Γ] (λ {Δ} {σ} → [UA] {Δ} {σ}) [A]ₜ [A']ₜ
        [ΓId] = _∙_ {A = Id (Univ rA ⁰) A A'} [Γ] [IdAA']
        [wA'] = wk1ᵗᵛ {F = Id (Univ rA ⁰) A A'} {G = A'} {lG = ⁰} [Γ] [IdAA'] [A']ₜ
        [wA']' = wk1ᵛ {A = A'} {F = Id (Univ rA ⁰) A A'} [Γ] [IdAA'] [A']
        [wA]' = wk1ᵛ {A = A} {F = Id (Univ rA ⁰) A A'} [Γ] [IdAA'] [A]
        [wA] = wk1ᵗᵛ {F = Id (Univ rA ⁰) A A'} {G = A} {lG = ⁰} [Γ] [IdAA'] [A]ₜ
        [ΓIdA'] = _∙_ {A = wk1 A'} [ΓId] [wA']'
        [wwA']' = wk1ᵛ {A = wk1 A'} {F = wk1 A'}  [ΓId] [wA']' [wA']'
        [wwA'] = wk1ᵗᵛ {F = wk1 A'} {G = wk1 A'} {lG = ⁰} [ΓId] [wA']' [wA']
        [wwA] = wk1ᵗᵛ {F = wk1 A'} {G = wk1 A} {lG = ⁰} [ΓId] [wA']' [wA]
        [wwUA'] = λ {Δ} {σ} r → maybeEmbᵛ {A = Univ r _ } [ΓIdA'] (λ {Δ} {σ} → Uᵛ emb< [ΓIdA'] {Δ} {σ}) {Δ} {σ}
        [wwIdAA'] = Idᵛ {A = Univ rA ⁰} {t = wk1 (wk1 A)} {u = wk1 (wk1 A')} [ΓIdA'] (λ {Δ} {σ} → [wwUA'] {Δ} {σ} rA) [wwA] [wwA']
        [ΓA'] = (_∙_ {Γ} {A'} [Γ]  [A'])
        [w'A] = wk1ᵗᵛ {F = A'} {G = A} {lG = ⁰} [Γ] [A'] [A]ₜ
        [w'A'] = wk1ᵗᵛ {F = A'} {G = A'} {lG = ⁰} [Γ] [A'] [A']ₜ
        [w'A']' = wk1ᵛ {A = A'} {F = A'} [Γ] [A'] [A']
        [wUA] = maybeEmbᵛ {A = Univ rA _} [ΓA'] (λ {Δ} {σ} → Uᵛ emb< [ΓA'] {Δ} {σ})
        [wIdAA'] = Idᵛ {A = Univ rA ⁰} {t = wk1 A} {u = wk1 A'} [ΓA'] (λ {Δ} {σ} → [wUA] {Δ} {σ}) [w'A] [w'A']
        [ww'A']' = wk1ᵛ {A = wk1 A'} {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} [ΓA'] [wIdAA'] [w'A']'
        [ww'A'] = wk1ᵗᵛ {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} {G = wk1 A'} {lG = ⁰} [ΓA'] [wIdAA'] [w'A']
        [ΓA'Id] = _∙_ {A = Id (Univ rA ⁰) (wk1 A) (wk1 A')} [ΓA'] [wIdAA']
        [ΓA'IdA'] = _∙_ {A = wk1 (wk1 A')} [ΓA'Id] [ww'A']'
        [wwwUA'] = λ {Δ} {σ} r → maybeEmbᵛ {A = Univ r _ } [ΓA'IdA'] (λ {Δ} {σ} → Uᵛ emb< [ΓA'IdA'] {Δ} {σ}) {Δ} {σ}
        [www'A'] = wk1ᵗᵛ {F = wk1 (wk1 A')} {G = wk1 (wk1 A')} {lG = ⁰} [ΓA'Id] [ww'A']' [ww'A']
        [ww'A] = wk1ᵗᵛ {F = Id (Univ rA ⁰) (wk1 A) (wk1 A')} {G = wk1 A} {lG = ⁰} [ΓA'] [wIdAA'] [w'A]
        [www'A] = wk1ᵗᵛ {F = wk1 (wk1 A')} {G = wk1 (wk1 A)} {lG = ⁰} [ΓA'Id] [ww'A']' [ww'A]
        [wwwIdAA'] = Idᵛ {A = Univ rA ⁰} {t = wk1 (wk1 (wk1 A))} {u = wk1 (wk1 (wk1 A'))} [ΓA'IdA'] (λ {Δ} {σ} → [wwwUA'] {Δ} {σ} rA) [www'A] [www'A']
        [wA]ₜ = wk1ᵗᵛ {F = A'} {G = A} {lG = ⁰} [Γ] [A'] [A]ₜ
        [wA] = wk1ᵛ {A = A} {F = A'} [Γ] [A'] [A]
        [wA']ₜ = wk1ᵗᵛ {F = A'} {G = A'} {lG = ⁰} [Γ] [A'] [A']ₜ
        [wA'] = wk1ᵛ {A = A'} {F = A'} [Γ] [A'] [A']
        [wA']' = wk1ᵛ {A = A'} {F = A'} [Γ] [A'] [A']
        [wA]' = wk1ᵛ {A = A} {F = A'} [Γ] [A'] [A]
        [ΓA'A'] = _∙_ {A = wk1 A'} [ΓA'] [wA']'
        [ΓA'A] = _∙_ {A = wk1 A} [ΓA'] [wA]'
        [wwUA'] = λ {Δ} {σ} r → maybeEmbᵛ {A = Univ r _ } [ΓA'A'] (λ {Δ} {σ} → Uᵛ emb< [ΓA'A'] {Δ} {σ}) {Δ} {σ}
        [wwUA] = λ {Δ} {σ} r → maybeEmbᵛ {A = Univ r _ } [ΓA'A] (λ {Δ} {σ} → Uᵛ emb< [ΓA'A] {Δ} {σ}) {Δ} {σ}
        [wB']ₜ = wk1dᵗᵛ {F = A'} {F' = A'} {G = B'} [Γ] [A'] [A'] (λ {Δ} {σ} → [UB'] {Δ} {σ}) ((λ {Δ} {σ} → [wwUA'] {Δ} {σ} !)) [B']ₜ
        [wB]ₜ = wk1dᵗᵛ {F = A} {F' = A'} {G = B} [Γ] [A] [A'] (λ {Δ} {σ} → [UB] {Δ} {σ}) ((λ {Δ} {σ} → [wwUA] {Δ} {σ} !)) [B]ₜ
        [var]ₜ : Γ ∙ A' ^ [ rA , ι ⁰ ] ⊩ᵛ⟨ ∞ ⟩ var 0 ∷ wk1 A' ^ [ rA , ι ⁰ ] / [ΓA'] / wk1ᵛ {A = A'} {F = A'} [Γ] [A'] [A']
        [var]ₜ = proj₂ (fundamentalVar here [ΓA'])
        [var0']ₜ : Γ ∙ A' ^ [ rA , ι ⁰ ] ∙ Id (Univ rA ⁰) (wk1 A) (wk1 A') ^ [ % , ι ¹ ] ∙ wk1 (wk1 A') ^ [ rA , ι ⁰ ] ⊩ᵛ⟨ ∞ ⟩ var 0 ∷
                          wk1 (wk1 (wk1 A')) ^ [ rA , ι ⁰ ] / [ΓA'IdA'] / wk1ᵛ {A = wk1 (wk1 A')} {F = wk1 (wk1 A')} [ΓA'Id] [ww'A']' [ww'A']'
        [var0']ₜ = proj₂ (fundamentalVar here [ΓA'IdA'])
        [var1']ₜ : Γ ∙ A' ^ [ rA , ι ⁰ ] ∙ Id (Univ rA ⁰) (wk1 A) (wk1 A') ^ [ % , ι ¹ ] ∙ wk1 (wk1 A') ^ [ rA , ι ⁰ ] ⊩ᵛ⟨ ∞ ⟩ var 1 ∷
                          Id (Univ rA ⁰) (wk1 (wk1 (wk1 A))) (wk1 (wk1 (wk1 A'))) ^ [ % , ι ¹ ] / [ΓA'IdA'] / [wwwIdAA']
        [var1']ₜ = let X = fundamentalVar (there here) [ΓA'IdA'] in S.irrelevanceTerm {A = Id (Univ rA ⁰) (wk1 (wk1 (wk1 A))) (wk1 (wk1 (wk1 A')))} {t = var 1}
                                                                                [ΓA'IdA'] [ΓA'IdA'] (proj₁ X) [wwwIdAA'] (proj₂ X)
    in cast-Πᵗᵛ-aux {A} {B} {A'} {B'} {rA} {Γ} {e} {f}
                    [Γ] [A] [A'] (λ {Δ} {σ} → [UB] {Δ} {σ}) (λ {Δ} {σ} → [UB'] {Δ} {σ}) [A]ₜ [B]ₜ [A']ₜ [B']ₜ [Id] [e]ₜ [ΠAB] [f]ₜ
                    (Id-U-ΠΠᵗᵛ {A} {B} {A'} {B'} {rA} {Γ}
                               [Γ] [A] [A'] (λ {Δ} {σ} → [UB] {Δ} {σ}) (λ {Δ} {σ} → [UB'] {Δ} {σ}) [A]ₜ [B]ₜ [A']ₜ [B']ₜ)
                    (Id-U-ΠΠ-resᵗᵛ {wk1 A} {wk1d B} {wk1 A'} {wk1d B'}
                                   [ΓA'] [wA] [wA'] (λ {Δ} {σ} → [wwUA] {Δ} {σ} !) (λ {Δ} {σ} → [wwUA'] {Δ} {σ} !) [wA]ₜ [wB]ₜ [wA']ₜ [wB']ₜ [var0']ₜ [var1']ₜ)
                    [var]ₜ [var0']ₜ [var1']ₜ

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
-- Be afraid… Type as type Type
{-# OPTIONS --type-in-type #-}

{-
Be really afraid: this module is a hack to give definitional equalities
to ▹. This is done by introducing an 'evil' function called 'run' that
should not appear in user code. Is this safe to do? This remains to be
explored.

By the same token we give a definitional equalities to fix as well.
Beware of non-termination!
-}

open import guarded-recursion.prelude
  renaming (O to zero; S to suc)

module guarded-recursion.compute where

-- Same as in prelude but type-in-type
module Coe₀ where
    coe : {A B : Type} → A ≡ B → A → B
    coe = transport id

    coe! : {A B : Type} → A ≡ B → B → A
    coe! = transport id ∘ !

    module _ {A : Type} {P Q : A → Type} (p : P ≡ Q) {x} where
        coe₁ : P x → Q x
        coe₁ = transport (λ P → P x) p

        coe₁! : Q x → P x
        coe₁! = transport (λ P → P x) (! p)

    module _ {A : Type} {B : Type} {R S : A → B → Type} (p : R ≡ S) {x y} where
        coe₂ : R x y → S x y
        coe₂ = transport (λ R → R x y) p

        coe₂! : S x y → R x y
        coe₂! = transport (λ R → R x y) (! p)
open Coe₀

infixl 6 _⊛_

data ▹_ : Type → Type

private
  -- 'run' should not appear in user code
  run : ∀ {A} → ▹ A → A

-- User code should not pattern-match on ▹_...
data ▹_ where
  next : ∀ {A} → A → ▹ A
  _⊛_  : ∀ {A} {B : A → Type} → ▹ ((x : A) → B x) → (x : ▹ A) → ▹ (B (run x))

run (next x) = x
run (f  ⊛ x) = run f (run x)

▸ : ▹ Type → Type
▸ x = ▹ (run x)

▸F : ∀ {A} → (A → Type) → ▹ A → Type
▸F F x = ▸ (next F ⊛ x)

map▹ : ∀ {A} {B : A → Type} → ((x : A) → B x) → (x : ▹ A) → ▸F B x
map▹ f x = next f ⊛ x

private
  module Unused where
    by-computation : ∀ {A} {B : A → Type} {x} → ▸ (next B ⊛ x) ≡ ▹ (B (run x))
    by-computation = idp

    const⊛ : ∀ {A} {X : Type} {x : ▹ X} → ▸ (next (λ _ → A) ⊛ x) ≡ ▹ A
    const⊛ = idp

    -- useless: the dependent version is just as fine
    _⊛′_ : ∀ {A B} → ▹ (A → B) → ▹ A → ▹ B
    _⊛′_ = _⊛_

    -- useless: the dependent version is just as fine
    map▹′ : ∀ {A B} → (A → B) → ▹ A → ▹ B
    map▹′ = map▹

zip : ∀ {A} {B : A → Type} → Σ (▹ A) (▸F B) → ▹ Σ A B
zip (x , y) = map▹ _,_ x ⊛ y

unzip : ∀ {A} {B : A → Type} → ▹ Σ A B → Σ (▹ A) (▸F B)
unzip p = map▹ fst p , map▹ snd p

module M
   (fix      : ∀ {A} → (▹ A → A) → A)
   (fix-rule : ∀ {A} (f : ▹ A → A) → fix f ≡ f (next (fix f))) where

  -- Streams of 'A's
  S : Type → Type
  S A = fix (λ X → A × ▸ X)

  rollS : ∀ {A} → A × ▹ (S A) → S A
  rollS = coe! (fix-rule _)

  unS : ∀ {A} → S A → A × ▹ (S A)
  unS = coe (fix-rule _)

  hd : ∀ {A} → S A → A
  hd = fst ∘ unS

  tl : ∀ {A} → S A → ▹ S A
  tl = snd ∘ unS

  infixl 4 _∷_
  _∷_ : ∀ {A} → A → ▹ S A → S A
  x ∷ xs = rollS (x , xs)

  BF : ∀ {A} → ▹ (S A → S A → Type) → S A → S A → Type
  BF ▹B xs ys = (hd xs ≡ hd ys) × ▸ (▹B ⊛ tl xs ⊛ tl ys)

  B : ∀ {A} → S A → S A → Type
  B = fix BF

  rollB : ∀ {A} {xs ys : S A} → BF (next B) xs ys → B xs ys
  rollB = coe₂! (fix-rule BF)

  B-reflF : ∀ {A} → ▹((xs : S A) → B xs xs) → (xs : S A) → B xs xs
  B-reflF ▹BR xs = rollB (idp , ▹BR ⊛ tl xs)

  -- Reflexivity of the Bisimilarity relation
  -- Thanks to computation at the level of types this definition nicely
  -- goes through.
  B-refl : ∀ {A} (xs : S A) → B xs xs
  B-refl = fix B-reflF

  repeatS : ∀ {A} → A → S A
  repeatS x = fix (_∷_ x)

  zapSf : ∀ {A B} → ▹ (S (A → B) → S A → S B)
                  →    S (A → B) → S A → S B
  zapSf zapS fs xs = hd fs (hd xs) ∷ zapS ⊛ tl fs ⊛ tl xs

  zapS : ∀ {A B} → S (A → B) → S A → S B
  zapS = fix zapSf

  -- repeatS and zapS form an applicative functor

  iterateS : ∀ {A} → (A → A) → A → S A
  iterateS f = fix λ iterateS x → x ∷ iterateS ⊛ next (f x)

  mapSf : ∀ {A B} → (A → B) → ▹(S A → S B) → S A → S B
  mapSf f mapS xs = f (hd xs) ∷ mapS ⊛ tl xs

  mapS : ∀ {A B} → (A → B) → S A → S B
  mapS f = fix (mapSf f)

  nats : S ℕ
  nats = fix (λ nats → 0 ∷ map▹ (mapS suc) nats)

  ▹^ : ∀ ℕ → Type → Type
  ▹^ zero    A = A
  ▹^ (suc n) A = ▹ ▹^ n A

  next^ : ∀ {A} n → A → ▹^ n A
  next^ zero    x = x
  next^ (suc n) x = next (next^ n x)

  map▹^ : ∀ {A B} n → (A → B) → ▹^ n A → ▹^ n B
  map▹^ zero    f = f
  map▹^ (suc n) f = map▹ (map▹^ n f)

  run^ : ∀ {A} n → ▹^ n A → A
  run^ zero = id
  run^ (suc n) = run^ n ∘ run

  ‼ : ∀ {A} → (n : ℕ) → S A → ▹^ n A
  ‼ zero    = hd
  ‼ (suc n) = map▹ (‼ n) ∘ tl

  run‼ : ∀ {A} → ℕ → S A → A
  run‼ n = run^ n ∘ ‼ n

module HiddenFix {A} (f : ▹ A → A) where
    -- This definition is not intended to termination-check.
    -- Use with care it's really easy to make the type-checker loop.
    {-# TERMINATING #-}
    fix : Hidden A
    fix = hide f (next (reveal fix))

    fix-rule : reveal fix ≡ f (next (reveal fix))
    fix-rule = idp {_} {A} {reveal fix}

open HiddenFix
open M (reveal ∘ fix) fix-rule

  -- -}
  -- -}
  -- -}
  -- -}
  -- -}

max_stars_repo_name: np/guarded-recursion

max_issues_repo_name: np/guarded-recursion

max_forks_repo_name: np/guarded-recursion


text:
module Prelude.Char where

open import Prelude.Bool
open import Prelude.Nat
open import Prelude.Equality
open import Prelude.Equality.Unsafe
open import Prelude.Decidable
open import Prelude.Function
open import Prelude.Ord

open import Agda.Builtin.Char
open Agda.Builtin.Char public using (Char)

isLower    = primIsLower
isDigit    = primIsDigit
isSpace    = primIsSpace
isAscii    = primIsAscii
isLatin1   = primIsLatin1
isPrint    = primIsPrint
isHexDigit = primIsHexDigit
isAlpha    = primIsAlpha

toUpper    = primToUpper
toLower    = primToLower

isAlphaNum : Char → Bool
isAlphaNum c = isAlpha c || isDigit c

charToNat  = primCharToNat
natToChar  = primNatToChar

charToNat-inj : ∀ {x y} → charToNat x ≡ charToNat y → x ≡ y
charToNat-inj {x} p with charToNat x
charToNat-inj refl | ._ = unsafeEqual  -- need to be strict in the proof!

--- Equality --

eqChar : Char → Char → Bool
eqChar = eqNat on charToNat

instance
  EqChar : Eq Char
  _==_ {{EqChar}} x y with eqChar x y
  ... | false = no  unsafeNotEqual
  ... | true  = yes unsafeEqual

-- Missing primitive isUpper
isUpper : Char → Bool
isUpper c = isNo (toLower c == c)

--- Ord ---

instance
  OrdChar : Ord Char
  OrdChar = OrdBy charToNat-inj

  OrdLawsChar : Ord/Laws Char
  OrdLawsChar = OrdLawsBy charToNat-inj

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


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

module Definition.Typed where

open import Definition.Untyped hiding (_∷_)

open import Tools.Fin
open import Tools.Nat
open import Tools.Product

infixl 30 _∙_
infix 30 Πⱼ_▹_
infix 30 Σⱼ_▹_
infix 30 ⟦_⟧ⱼ_▹_

private
  variable
    n m : Nat
    Γ  : Con Term n
    A B F : Term n
    G : Term (1+ n)
    x : Fin n

-- Well-typed variables
data _∷_∈_ : (x : Fin n) (A : Term n) (Γ : Con Term n) → Set where
  here  :                       x0 ∷ wk1 A ∈ (Γ ∙ A)
  there : (h : x ∷ A ∈ Γ) → (x +1) ∷ wk1 A ∈ (Γ ∙ B)

mutual
  -- Well-formed context
  data ⊢_ : Con Term n → Set where
    ε   : ⊢ ε
    _∙_ : ⊢ Γ
        → Γ ⊢ A
        → ⊢ Γ ∙ A

  -- Well-formed type
  data _⊢_ (Γ : Con Term n) : Term n → Set where
    Uⱼ     : ⊢ Γ → Γ ⊢ U
    ℕⱼ     : ⊢ Γ → Γ ⊢ ℕ
    Emptyⱼ : ⊢ Γ → Γ ⊢ Empty
    Unitⱼ  : ⊢ Γ → Γ ⊢ Unit
    Πⱼ_▹_  : Γ     ⊢ F
           → Γ ∙ F ⊢ G
           → Γ     ⊢ Π F ▹ G
    Σⱼ_▹_  : Γ     ⊢ F
           → Γ ∙ F ⊢ G
           → Γ     ⊢ Σ F ▹ G
    univ   : Γ ⊢ A ∷ U
           → Γ ⊢ A

  -- Well-formed term of a type
  data _⊢_∷_ (Γ : Con Term n) : Term n → Term n → Set where
    Πⱼ_▹_     : ∀ {F G}
              → Γ     ⊢ F ∷ U
              → Γ ∙ F ⊢ G ∷ U
              → Γ     ⊢ Π F ▹ G ∷ U
    Σⱼ_▹_     : ∀ {F G}
              → Γ     ⊢ F ∷ U
              → Γ ∙ F ⊢ G ∷ U
              → Γ     ⊢ Σ F ▹ G ∷ U
    ℕⱼ        : ⊢ Γ → Γ ⊢ ℕ ∷ U
    Emptyⱼ    : ⊢ Γ → Γ ⊢ Empty ∷ U
    Unitⱼ     : ⊢ Γ → Γ ⊢ Unit ∷ U

    var       : ∀ {A x}
              → ⊢ Γ
              → x ∷ A ∈ Γ
              → Γ ⊢ var x ∷ A

    lamⱼ      : ∀ {F G t}
              → Γ     ⊢ F
              → Γ ∙ F ⊢ t ∷ G
              → Γ     ⊢ lam t ∷ Π F ▹ G
    _∘ⱼ_      : ∀ {g a F G}
              → Γ ⊢     g ∷ Π F ▹ G
              → Γ ⊢     a ∷ F
              → Γ ⊢ g ∘ a ∷ G [ a ]

    prodⱼ     : ∀ {F G t u}
              → Γ ⊢ F
              → Γ ∙ F ⊢ G
              → Γ ⊢ t ∷ F
              → Γ ⊢ u ∷ G [ t ]
              → Γ ⊢ prod t u ∷ Σ F ▹ G
    fstⱼ      : ∀ {F G t}
              → Γ ⊢ F
              → Γ ∙ F ⊢ G
              → Γ ⊢ t ∷ Σ F ▹ G
              → Γ ⊢ fst t ∷ F
    sndⱼ      : ∀ {F G t}
              → Γ ⊢ F
              → Γ ∙ F ⊢ G
              → Γ ⊢ t ∷ Σ F ▹ G
              → Γ ⊢ snd t ∷ G [ fst t ]

    zeroⱼ     : ⊢ Γ
              → Γ ⊢ zero ∷ ℕ
    sucⱼ      : ∀ {n}
              → Γ ⊢       n ∷ ℕ
              → Γ ⊢ suc n ∷ ℕ
    natrecⱼ   : ∀ {G s z n}
              → Γ ∙ ℕ ⊢ G
              → Γ       ⊢ z ∷ G [ zero ]
              → Γ       ⊢ s ∷ Π ℕ ▹ (G ▹▹ G [ suc (var x0) ]↑)
              → Γ       ⊢ n ∷ ℕ
              → Γ       ⊢ natrec G z s n ∷ G [ n ]

    Emptyrecⱼ : ∀ {A e}
              → Γ ⊢ A → Γ ⊢ e ∷ Empty → Γ ⊢ Emptyrec A e ∷ A

    starⱼ     : ⊢ Γ → Γ ⊢ star ∷ Unit

    conv      : ∀ {t A B}
              → Γ ⊢ t ∷ A
              → Γ ⊢ A ≡ B
              → Γ ⊢ t ∷ B

  -- Type equality
  data _⊢_≡_ (Γ : Con Term n) : Term n → Term n → Set where
    univ   : ∀ {A B}
           → Γ ⊢ A ≡ B ∷ U
           → Γ ⊢ A ≡ B
    refl   : ∀ {A}
           → Γ ⊢ A
           → Γ ⊢ A ≡ A
    sym    : ∀ {A B}
           → Γ ⊢ A ≡ B
           → Γ ⊢ B ≡ A
    trans  : ∀ {A B C}
           → Γ ⊢ A ≡ B
           → Γ ⊢ B ≡ C
           → Γ ⊢ A ≡ C
    Π-cong : ∀ {F H G E}
           → Γ     ⊢ F
           → Γ     ⊢ F ≡ H
           → Γ ∙ F ⊢ G ≡ E
           → Γ     ⊢ Π F ▹ G ≡ Π H ▹ E
    Σ-cong : ∀ {F H G E}
           → Γ     ⊢ F
           → Γ     ⊢ F ≡ H
           → Γ ∙ F ⊢ G ≡ E
           → Γ     ⊢ Σ F ▹ G ≡ Σ H ▹ E

  -- Term equality
  data _⊢_≡_∷_ (Γ : Con Term n) : Term n → Term n → Term n → Set where
    refl          : ∀ {t A}
                  → Γ ⊢ t ∷ A
                  → Γ ⊢ t ≡ t ∷ A
    sym           : ∀ {t u A}
                  → Γ ⊢ t ≡ u ∷ A
                  → Γ ⊢ u ≡ t ∷ A
    trans         : ∀ {t u r A}
                  → Γ ⊢ t ≡ u ∷ A
                  → Γ ⊢ u ≡ r ∷ A
                  → Γ ⊢ t ≡ r ∷ A
    conv          : ∀ {A B t u}
                  → Γ ⊢ t ≡ u ∷ A
                  → Γ ⊢ A ≡ B
                  → Γ ⊢ t ≡ u ∷ B
    Π-cong        : ∀ {E F G H}
                  → Γ     ⊢ F
                  → Γ     ⊢ F ≡ H       ∷ U
                  → Γ ∙ F ⊢ G ≡ E       ∷ U
                  → Γ     ⊢ Π F ▹ G ≡ Π H ▹ E ∷ U
    Σ-cong        : ∀ {E F G H}
                  → Γ     ⊢ F
                  → Γ     ⊢ F ≡ H       ∷ U
                  → Γ ∙ F ⊢ G ≡ E       ∷ U
                  → Γ     ⊢ Σ F ▹ G ≡ Σ H ▹ E ∷ U
    app-cong      : ∀ {a b f g F G}
                  → Γ ⊢ f ≡ g ∷ Π F ▹ G
                  → Γ ⊢ a ≡ b ∷ F
                  → Γ ⊢ f ∘ a ≡ g ∘ b ∷ G [ a ]
    β-red         : ∀ {a t F G}
                  → Γ     ⊢ F
                  → Γ ∙ F ⊢ t ∷ G
                  → Γ     ⊢ a ∷ F
                  → Γ     ⊢ (lam t) ∘ a ≡ t [ a ] ∷ G [ a ]
    η-eq          : ∀ {f g F G}
                  → Γ     ⊢ F
                  → Γ     ⊢ f ∷ Π F ▹ G
                  → Γ     ⊢ g ∷ Π F ▹ G
                  → Γ ∙ F ⊢ wk1 f ∘ var x0 ≡ wk1 g ∘ var x0 ∷ G
                  → Γ     ⊢ f ≡ g ∷ Π F ▹ G
    fst-cong      : ∀ {t t' F G}
                  → Γ ⊢ F
                  → Γ ∙ F ⊢ G
                  → Γ ⊢ t ≡ t' ∷ Σ F ▹ G
                  → Γ ⊢ fst t ≡ fst t' ∷ F
    snd-cong      : ∀ {t t' F G}
                  → Γ ⊢ F
                  → Γ ∙ F ⊢ G
                  → Γ ⊢ t ≡ t' ∷ Σ F ▹ G
                  → Γ ⊢ snd t ≡ snd t' ∷ G [ fst t ]
    Σ-β₁          : ∀ {F G t u}
                  → Γ ⊢ F
                  → Γ ∙ F ⊢ G
                  → Γ ⊢ t ∷ F
                  → Γ ⊢ u ∷ G [ t ]
                  → Γ ⊢ fst (prod t u) ≡ t ∷ F
    Σ-β₂          : ∀ {F G t u}
                  → Γ ⊢ F
                  → Γ ∙ F ⊢ G
                  → Γ ⊢ t ∷ F
                  → Γ ⊢ u ∷ G [ t ]
                  → Γ ⊢ snd (prod t u) ≡ u ∷ G [ fst (prod t u) ]
    Σ-η           : ∀ {p r F G}
                  → Γ ⊢ F
                  → Γ ∙ F ⊢ G
                  → Γ ⊢ p ∷ Σ F ▹ G
                  → Γ ⊢ r ∷ Σ F ▹ G
                  → Γ ⊢ fst p ≡ fst r ∷ F
                  → Γ ⊢ snd p ≡ snd r ∷ G [ fst p ]
                  → Γ ⊢ p ≡ r ∷ Σ F ▹ G
    suc-cong      : ∀ {m n}
                  → Γ ⊢ m ≡ n ∷ ℕ
                  → Γ ⊢ suc m ≡ suc n ∷ ℕ
    natrec-cong   : ∀ {z z′ s s′ n n′ F F′}
                  → Γ ∙ ℕ ⊢ F ≡ F′
                  → Γ     ⊢ z ≡ z′ ∷ F [ zero ]
                  → Γ     ⊢ s ≡ s′ ∷ Π ℕ ▹ (F ▹▹ F [ suc (var x0) ]↑)
                  → Γ     ⊢ n ≡ n′ ∷ ℕ
                  → Γ     ⊢ natrec F z s n ≡ natrec F′ z′ s′ n′ ∷ F [ n ]
    natrec-zero   : ∀ {z s F}
                  → Γ ∙ ℕ ⊢ F
                  → Γ     ⊢ z ∷ F [ zero ]
                  → Γ     ⊢ s ∷ Π ℕ ▹ (F ▹▹ F [ suc (var x0) ]↑)
                  → Γ     ⊢ natrec F z s zero ≡ z ∷ F [ zero ]
    natrec-suc    : ∀ {n z s F}
                  → Γ     ⊢ n ∷ ℕ
                  → Γ ∙ ℕ ⊢ F
                  → Γ     ⊢ z ∷ F [ zero ]
                  → Γ     ⊢ s ∷ Π ℕ ▹ (F ▹▹ F [ suc (var x0) ]↑)
                  → Γ     ⊢ natrec F z s (suc n) ≡ (s ∘ n) ∘ (natrec F z s n)
                          ∷ F [ suc n ]
    Emptyrec-cong : ∀ {A A' e e'}
                  → Γ ⊢ A ≡ A'
                  → Γ ⊢ e ≡ e' ∷ Empty
                  → Γ ⊢ Emptyrec A e ≡ Emptyrec A' e' ∷ A
    η-unit        : ∀ {e e'}
                  → Γ ⊢ e ∷ Unit
                  → Γ ⊢ e' ∷ Unit
                  → Γ ⊢ e ≡ e' ∷ Unit

-- Term reduction
data _⊢_⇒_∷_ (Γ : Con Term n) : Term n → Term n → Term n → Set where
  conv           : ∀ {A B t u}
                 → Γ ⊢ t ⇒ u ∷ A
                 → Γ ⊢ A ≡ B
                 → Γ ⊢ t ⇒ u ∷ B
  app-subst      : ∀ {A B t u a}
                 → Γ ⊢ t ⇒ u ∷ Π A ▹ B
                 → Γ ⊢ a ∷ A
                 → Γ ⊢ t ∘ a ⇒ u ∘ a ∷ B [ a ]
  β-red          : ∀ {A B a t}
                 → Γ     ⊢ A
                 → Γ ∙ A ⊢ t ∷ B
                 → Γ     ⊢ a ∷ A
                 → Γ     ⊢ (lam t) ∘ a ⇒ t [ a ] ∷ B [ a ]
  fst-subst      : ∀ {t t' F G}
                 → Γ ⊢ F
                 → Γ ∙ F ⊢ G
                 → Γ ⊢ t ⇒ t' ∷ Σ F ▹ G
                 → Γ ⊢ fst t ⇒ fst t' ∷ F
  snd-subst      : ∀ {t t' F G}
                 → Γ ⊢ F
                 → Γ ∙ F ⊢ G
                 → Γ ⊢ t ⇒ t' ∷ Σ F ▹ G
                 → Γ ⊢ snd t ⇒ snd t' ∷ G [ fst t ]
  Σ-β₁           : ∀ {F G t u}
                 → Γ ⊢ F
                 → Γ ∙ F ⊢ G
                 → Γ ⊢ t ∷ F
                 → Γ ⊢ u ∷ G [ t ]
                 → Γ ⊢ fst (prod t u) ⇒ t ∷ F
  Σ-β₂           : ∀ {F G t u}
                 → Γ ⊢ F
                 → Γ ∙ F ⊢ G
                 → Γ ⊢ t ∷ F
                 → Γ ⊢ u ∷ G [ t ]
                 -- TODO(WN): Prove that 𝔍 ∷ G [ t ] is admissible
                 → Γ ⊢ snd (prod t u) ⇒ u ∷ G [ fst (prod t u) ]
  natrec-subst   : ∀ {z s n n′ F}
                 → Γ ∙ ℕ ⊢ F
                 → Γ     ⊢ z ∷ F [ zero ]
                 → Γ     ⊢ s ∷ Π ℕ ▹ (F ▹▹ F [ suc (var x0) ]↑)
                 → Γ     ⊢ n ⇒ n′ ∷ ℕ
                 → Γ     ⊢ natrec F z s n ⇒ natrec F z s n′ ∷ F [ n ]
  natrec-zero    : ∀ {z s F}
                 → Γ ∙ ℕ ⊢ F
                 → Γ     ⊢ z ∷ F [ zero ]
                 → Γ     ⊢ s ∷ Π ℕ ▹ (F ▹▹ F [ suc (var x0) ]↑)
                 → Γ     ⊢ natrec F z s zero ⇒ z ∷ F [ zero ]
  natrec-suc     : ∀ {n z s F}
                 → Γ     ⊢ n ∷ ℕ
                 → Γ ∙ ℕ ⊢ F
                 → Γ     ⊢ z ∷ F [ zero ]
                 → Γ     ⊢ s ∷ Π ℕ ▹ (F ▹▹ F [ suc (var x0) ]↑)
                 → Γ     ⊢ natrec F z s (suc n) ⇒ (s ∘ n) ∘ (natrec F z s n) ∷ F [ suc n ]
  Emptyrec-subst : ∀ {n n′ A}
                 → Γ ⊢ A
                 → Γ     ⊢ n ⇒ n′ ∷ Empty
                 → Γ     ⊢ Emptyrec A n ⇒ Emptyrec A n′ ∷ A

-- Type reduction
data _⊢_⇒_ (Γ : Con Term n) : Term n → Term n → Set where
  univ : ∀ {A B}
       → Γ ⊢ A ⇒ B ∷ U
       → Γ ⊢ A ⇒ B

-- Term reduction closure
data _⊢_⇒*_∷_ (Γ : Con Term n) : Term n → Term n → Term n → Set where
  id  : ∀ {A t}
      → Γ ⊢ t ∷ A
      → Γ ⊢ t ⇒* t ∷ A
  _⇨_ : ∀ {A t t′ u}
      → Γ ⊢ t  ⇒  t′ ∷ A
      → Γ ⊢ t′ ⇒* u  ∷ A
      → Γ ⊢ t  ⇒* u  ∷ A

-- Type reduction closure
data _⊢_⇒*_ (Γ : Con Term n) : Term n → Term n → Set where
  id  : ∀ {A}
      → Γ ⊢ A
      → Γ ⊢ A ⇒* A
  _⇨_ : ∀ {A A′ B}
      → Γ ⊢ A  ⇒  A′
      → Γ ⊢ A′ ⇒* B
      → Γ ⊢ A  ⇒* B

-- Type reduction to whnf
_⊢_↘_ : (Γ : Con Term n) → Term n → Term n → Set
Γ ⊢ A ↘ B = Γ ⊢ A ⇒* B × Whnf B

-- Term reduction to whnf
_⊢_↘_∷_ : (Γ : Con Term n) → Term n → Term n → Term n → Set
Γ ⊢ t ↘ u ∷ A = Γ ⊢ t ⇒* u ∷ A × Whnf u

-- Type eqaulity with well-formed types
_⊢_:≡:_ : (Γ : Con Term n) → Term n → Term n → Set
Γ ⊢ A :≡: B = Γ ⊢ A × Γ ⊢ B × (Γ ⊢ A ≡ B)

-- Term equality with well-formed terms
_⊢_:≡:_∷_ : (Γ : Con Term n) → Term n → Term n → Term n → Set
Γ ⊢ t :≡: u ∷ A = (Γ ⊢ t ∷ A) × (Γ ⊢ u ∷ A) × (Γ ⊢ t ≡ u ∷ A)

-- Type reduction closure with well-formed types
record _⊢_:⇒*:_ (Γ : Con Term n) (A B : Term n) : Set where
  constructor [_,_,_]
  field
    ⊢A : Γ ⊢ A
    ⊢B : Γ ⊢ B
    D  : Γ ⊢ A ⇒* B

open _⊢_:⇒*:_ using () renaming (D to red; ⊢A to ⊢A-red; ⊢B to ⊢B-red) public

-- Term reduction closure with well-formed terms
record _⊢_:⇒*:_∷_ (Γ : Con Term n) (t u A : Term n) : Set where
  constructor [_,_,_]
  field
    ⊢t : Γ ⊢ t ∷ A
    ⊢u : Γ ⊢ u ∷ A
    d  : Γ ⊢ t ⇒* u ∷ A

open _⊢_:⇒*:_∷_ using () renaming (d to redₜ; ⊢t to ⊢t-redₜ; ⊢u to ⊢u-redₜ) public

-- Well-formed substitutions.
data _⊢ˢ_∷_ (Δ : Con Term m) : (σ : Subst m n) (Γ : Con Term n) → Set where
  id  : ∀ {σ} → Δ ⊢ˢ σ ∷ ε
  _,_ : ∀ {A σ}
      → Δ ⊢ˢ tail σ ∷ Γ
      → Δ ⊢  head σ ∷ subst (tail σ) A
      → Δ ⊢ˢ σ      ∷ Γ ∙ A

-- Conversion of well-formed substitutions.
data _⊢ˢ_≡_∷_ (Δ : Con Term m) : (σ σ′ : Subst m n) (Γ : Con Term n) → Set where
  id  : ∀ {σ σ′} → Δ ⊢ˢ σ ≡ σ′ ∷ ε
  _,_ : ∀ {A σ σ′}
      → Δ ⊢ˢ tail σ ≡ tail σ′ ∷ Γ
      → Δ ⊢  head σ ≡ head σ′ ∷ subst (tail σ) A
      → Δ ⊢ˢ      σ ≡ σ′      ∷ Γ ∙ A

-- Note that we cannot use the well-formed substitutions.
-- For that, we need to prove the fundamental theorem for substitutions.

⟦_⟧ⱼ_▹_ : (W : BindingType) → ∀ {F G}
     → Γ     ⊢ F
     → Γ ∙ F ⊢ G
     → Γ     ⊢ ⟦ W ⟧ F ▹ G
⟦ BΠ ⟧ⱼ ⊢F ▹ ⊢G = Πⱼ ⊢F ▹ ⊢G
⟦ BΣ ⟧ⱼ ⊢F ▹ ⊢G = Σⱼ ⊢F ▹ ⊢G

⟦_⟧ⱼᵤ_▹_ : (W : BindingType) → ∀ {F G}
     → Γ     ⊢ F ∷ U
     → Γ ∙ F ⊢ G ∷ U
     → Γ     ⊢ ⟦ W ⟧ F ▹ G ∷ U
⟦ BΠ ⟧ⱼᵤ ⊢F ▹ ⊢G = Πⱼ ⊢F ▹ ⊢G
⟦ BΣ ⟧ⱼᵤ ⊢F ▹ ⊢G = Σⱼ ⊢F ▹ ⊢G

max_stars_repo_name: fhlkfy/logrel-mltt

max_issues_repo_name: fhlkfy/logrel-mltt

max_forks_repo_name: fhlkfy/logrel-mltt


text:
-- Binary coproducts
{-# OPTIONS --safe #-}

module Cubical.Categories.Limits.BinCoproduct where

open import Cubical.Categories.Category.Base
open import Cubical.Data.Sigma.Base
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.HITs.PropositionalTruncation.Base

private
  variable
    ℓ ℓ' : Level

module _ (C : Category ℓ ℓ') where
  open Category C

  module _ {x y x+y : ob}
           (i₁ : Hom[ x , x+y ])
           (i₂ : Hom[ y , x+y ]) where

    isBinCoproduct : Type (ℓ-max ℓ ℓ')
    isBinCoproduct = ∀ {z : ob} (f₁ : Hom[ x , z ]) (f₂ : Hom[ y , z ]) →
        ∃![ f ∈ Hom[ x+y , z ] ] (i₁ ⋆ f ≡ f₁) × (i₂ ⋆ f ≡ f₂)

    isPropIsBinCoproduct : isProp (isBinCoproduct)
    isPropIsBinCoproduct = isPropImplicitΠ (λ _ → isPropΠ2 (λ _ _ → isPropIsContr))

  record BinCoproduct (x y : ob) : Type (ℓ-max ℓ ℓ') where
    field
      binCoprodOb : ob
      binCoprodInj₁ : Hom[ x , binCoprodOb ]
      binCoprodInj₂ : Hom[ y , binCoprodOb ]
      univProp : isBinCoproduct binCoprodInj₁ binCoprodInj₂

  BinCoproducts : Type (ℓ-max ℓ ℓ')
  BinCoproducts = (x y : ob) → BinCoproduct x y

  hasBinCoproducts : Type (ℓ-max ℓ ℓ')
  hasBinCoproducts = ∥ BinCoproducts ∥₁

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

-- Some properties of Restriction Categories

-- The first few lemmas are from Cocket & Lack, Lemma 2.1 and 2.2
module Categories.Category.Restriction.Properties where

open import Data.Product using (Σ; _,_)
open import Level using (Level; _⊔_)

open import Categories.Category.Core using (Category)
open import Categories.Category.Restriction using (Restriction)
open import Categories.Category.SubCategory
open import Categories.Morphism using (Mono)
open import Categories.Morphism.Idempotent using (Idempotent)
open import Categories.Morphism.Properties using (Mono-id)
import Categories.Morphism.Reasoning as MR

module _ {o ℓ e : Level} {𝒞 : Category o ℓ e} (R : Restriction 𝒞) where
  open Category 𝒞
  open Restriction R
  open HomReasoning
  open MR 𝒞 using (elimˡ; introʳ)

  private
    variable
      A B C : Obj
      f : A ⇒ B
      g : B ⇒ C

  ↓f-idempotent : (A ⇒ B) → Idempotent 𝒞 A
  ↓f-idempotent f = record { idem = f ↓ ; idempotent = ⟺ ↓-denestʳ ○ ↓-cong pidʳ }

  -- a special version of ↓ being a partial left identity
  ↓-pidˡ-gf : f ↓ ∘ (g ∘ f) ↓ ≈ (g ∘ f) ↓
  ↓-pidˡ-gf {f = f} {g = g} = begin
    f ↓ ∘ (g ∘ f) ↓   ≈⟨ ↓-comm ⟩
    (g ∘ f) ↓ ∘ f ↓   ≈˘⟨ ↓-denestʳ ⟩
    ((g ∘ f) ∘ f ↓) ↓ ≈⟨ ↓-cong assoc ⟩
    (g ∘ (f ∘ f ↓)) ↓ ≈⟨ ↓-cong (∘-resp-≈ʳ pidʳ) ⟩
    (g ∘ f) ↓ ∎

  -- left denesting looks different in its conclusion
  ↓-denestˡ : (g ↓ ∘ f) ↓ ≈ (g ∘ f) ↓
  ↓-denestˡ {g = g} {f = f} = begin
    (g ↓ ∘ f) ↓       ≈⟨ ↓-cong ↓-skew-comm ⟩
    (f ∘ (g ∘ f) ↓) ↓ ≈⟨ ↓-denestʳ ⟩
    f ↓ ∘ (g ∘ f) ↓   ≈⟨ ↓-pidˡ-gf ⟩
    (g ∘ f) ↓         ∎

  ↓-idempotent : f ↓ ↓ ≈ f ↓
  ↓-idempotent {f = f} = begin
    f ↓ ↓        ≈˘⟨ ↓-cong identityʳ ⟩
    (f ↓ ∘ id) ↓ ≈⟨ ↓-denestˡ ⟩
    (f ∘ id) ↓   ≈⟨ ↓-cong identityʳ ⟩
    f ↓ ∎

  ↓↓denest : (g ↓ ∘ f ↓) ↓ ≈ g ↓ ∘ f ↓
  ↓↓denest {g = g} {f = f} = begin
    (g ↓ ∘ f ↓) ↓ ≈⟨ ↓-denestʳ ⟩
    g ↓ ↓ ∘ f ↓   ≈⟨ (↓-idempotent ⟩∘⟨refl) ⟩
    g ↓ ∘ f ↓ ∎

  Mono⇒f↓≈id : Mono 𝒞 f → f ↓ ≈ id
  Mono⇒f↓≈id {f = f} mono = mono (f ↓) id (pidʳ ○ ⟺ identityʳ)

  -- if the domain of g is at least that of f, then the restriction coincides
  ↓⊃⇒≈ : f ∘ g ↓ ≈ f → f ↓ ≈ f ↓ ∘ g ↓
  ↓⊃⇒≈ {f = f} {g = g} fg↓≈f = ⟺ (↓-cong fg↓≈f) ○ ↓-denestʳ

  Mono⇒Total : Mono 𝒞 f → total f
  Mono⇒Total = Mono⇒f↓≈id

  ∘-pres-total : {A B C : Obj} {f : B ⇒ C} {g : A ⇒ B} → total f → total g → total (f ∘ g)
  ∘-pres-total {f = f} {g = g} tf tg = begin
    (f ∘ g) ↓   ≈˘⟨ ↓-denestˡ ⟩
    (f ↓ ∘ g) ↓ ≈⟨ ↓-cong (elimˡ tf) ⟩
    g ↓         ≈⟨ tg ⟩
    id ∎

  total-gf⇒total-f : total (g ∘ f) → total f
  total-gf⇒total-f {g = g} {f = f} tgf = begin
    f ↓             ≈⟨ introʳ tgf ⟩
    f ↓ ∘ (g ∘ f) ↓ ≈⟨ ↓-pidˡ-gf ⟩
    (g ∘ f) ↓       ≈⟨ tgf ⟩
    id              ∎

  total-SubCat : SubCat 𝒞 Obj
  total-SubCat = record
    { U = λ x → x
    ; R = total
    ; Rid = Mono⇒Total (Mono-id 𝒞)
    ; _∘R_ = ∘-pres-total
    }

  Total : Category o (ℓ ⊔ e) e
  Total = SubCategory 𝒞 total-SubCat

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories