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

module Definition.Typed where

open import Definition.Untyped

open import Tools.Nat using (Nat)
open import Tools.Product
import Tools.PropositionalEquality as PE

infixl 30 _∙_
infix 30 Πⱼ_▹_▹_▹_

-- Well-typed variables
data _∷_^_∈_ : (x : Nat) (A : Term) (r : TypeInfo) (Γ : Con Term) → Set where
  here  : ∀ {Γ A r}                     →         0 ∷ wk1 A ^ r ∈ (Γ ∙ A ^ r )
  there : ∀ {Γ A rA B rB x} (h : x ∷ A ^ rA ∈ Γ) → Nat.suc x ∷ wk1 A ^ rA ∈ (Γ ∙ B ^ rB)

mutual
  -- Well-formed context
  data ⊢_ : Con Term → Set where
    ε   : ⊢ ε
    _∙_ : ∀ {Γ A r}
        → ⊢ Γ
        → Γ ⊢ A ^ r
        → ⊢ Γ ∙ A ^ r

  -- Well-formed type
  data _⊢_^_ (Γ : Con Term) : Term → TypeInfo → Set where
    Uⱼ    : ∀ {r} → ⊢ Γ → Γ ⊢ Univ r ¹ ^ [ ! , ∞ ]
    univ : ∀ {A r l}
         → Γ ⊢ A ∷ Univ r l ^ [ ! , next l ]
         → Γ ⊢ A ^ [ r , ι l ]

  -- Well-formed term of a type
  data _⊢_∷_^_ (Γ : Con Term) : Term → Term → TypeInfo → Set where
    univ : ∀ {r l l'}
         → l < l'
         → ⊢ Γ
         → Γ ⊢ (Univ r l) ∷ (Univ ! l') ^ [ ! , next l' ]
    ℕⱼ      : ⊢ Γ → Γ ⊢ ℕ ∷ U ⁰ ^ [ ! , ι ¹ ]
    Emptyⱼ : ∀ {l} → ⊢ Γ → Γ ⊢ Empty l ∷ SProp l ^ [ ! , next l ]
    Πⱼ_▹_▹_▹_ : ∀ {F rF lF G lG r l}
           → lF ≤ l
           → lG ≤ l
           → Γ     ⊢ F ∷ (Univ rF lF) ^ [ ! , next lF ]
           → Γ ∙ F ^ [ rF , ι lF ] ⊢ G ∷ (Univ r lG) ^ [ ! , next lG ]
           → Γ     ⊢ Π F ^ rF ° lF ▹ G ° lG ° l ∷ (Univ r l) ^ [ ! , next l ]
    ∃ⱼ_▹_ : ∀ {F G l}
            → Γ ⊢ F ∷ SProp l ^ [ ! , next l ]
            → Γ ∙ F ^ [ % , ι l ] ⊢ G ∷ SProp l ^ [ ! , next l ]
            → Γ ⊢ ∃ F ▹ G ∷ SProp l ^ [ ! , next l ]
    var    : ∀ {A rl x}
           → ⊢ Γ
           → x ∷ A ^ rl ∈ Γ
           → Γ ⊢ var x ∷ A ^ rl
    lamⱼ    : ∀ {F r l rF lF G lG t}
           → lF ≤ l
           → lG ≤ l
           → Γ     ⊢ F ^ [ rF , ι lF ]
           → Γ ∙ F ^ [ rF , ι lF ] ⊢ t ∷ G ^ [ r , ι lG ]
           → Γ     ⊢ lam F ▹ t ^ l ∷ Π F ^ rF ° lF ▹ G ° lG ° l ^ [ r , ι l ]
    _∘ⱼ_    : ∀ {g a F rF lF G lG r lΠ}
           → Γ ⊢     g ∷ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ r , ι lΠ ]
           → Γ ⊢     a ∷ F ^ [ rF , ι lF ]
           → Γ ⊢ g ∘ a ^ lΠ ∷ G [ a ] ^ [ r , ι lG ]
    ⦅_,_,_,_⦆ⱼ : ∀ {l F G t u}
             → Γ ⊢ F ^ [ % , ι l ]
             → Γ ∙ F ^ [ % , ι l ] ⊢ G ^ [ % , ι l ]
             → Γ ⊢ t ∷ F ^ [ % , ι l ]
             → Γ ⊢ u ∷ G [ t ] ^ [ % , ι l ]
             → Γ ⊢ ⦅ G , t , u ⦆ ∷ ∃ F ▹ G ^ [ % , ι l ]
    fstⱼ : ∀ {F G t l}
           → Γ ⊢ F ∷ SProp l ^ [ ! , next l ]
           → Γ ∙ F ^ [ % , ι l ] ⊢ G ∷ SProp l ^ [ ! , next l ]
           → Γ ⊢ t ∷ ∃ F ▹ G ^ [ % , ι l ]
           → Γ ⊢ fst t ∷ F ^ [ % , ι l ]
    sndⱼ : ∀ {F G t l}
           → Γ ⊢ F ∷ SProp l ^ [ ! , next l ]
           → Γ ∙ F ^ [ % , ι l ] ⊢ G ∷ SProp l ^ [ ! , next l ]
           → Γ ⊢ t ∷ ∃ F ▹ G ^ [ % , ι l ]
           → Γ ⊢ snd t ∷ G [ fst t ] ^ [ % , ι l ]
    zeroⱼ   : ⊢ Γ
           → Γ ⊢ zero ∷ ℕ ^ [ ! ,  ι ⁰ ]
    sucⱼ    : ∀ {n}
           → Γ ⊢ n ∷ ℕ ^ [ ! ,  ι ⁰ ]
           → Γ ⊢ suc n ∷ ℕ ^ [ ! ,  ι ⁰ ]
    natrecⱼ : ∀ {G rG lG s z n}
           → Γ ∙ ℕ ^ [ ! ,  ι ⁰ ] ⊢ G ^ [ rG , ι lG ]
           → Γ       ⊢ z ∷ G [ zero ] ^ [ rG , ι lG ]
           → Γ       ⊢ s ∷ Π ℕ ^ ! ° ⁰ ▹ (G ^ rG ° lG ▹▹ G [ suc (var Nat.zero) ]↑ ° lG ° lG) ° lG ° lG ^ [ rG , ι lG ]
           → Γ       ⊢ n ∷ ℕ ^ [ ! ,  ι ⁰ ]
           → Γ       ⊢ natrec lG G z s n ∷ G [ n ] ^ [ rG , ι lG ]
    Emptyrecⱼ : ∀ {A l lA rA e}
           → Γ ⊢ A ^ [ rA , ι lA ] → Γ ⊢ e ∷ Empty l ^ [ % ,  ι l ] -> Γ ⊢ Emptyrec lA l A e ∷ A ^ [ rA , ι lA ]
    Idⱼ : ∀ {A l t u}
          → Γ ⊢ A ∷ U l ^ [ ! , next l ]
          → Γ ⊢ t ∷ A ^ [ ! , ι l ]
          → Γ ⊢ u ∷ A ^ [ ! , ι l ]
          → Γ ⊢ Id A t u ∷ SProp l ^ [ ! , next l ]
    Idreflⱼ : ∀ {A l t}
              → Γ ⊢ t ∷ A ^ [ ! , ι l ]
              → Γ ⊢ Idrefl A t ∷ (Id A t t) ^ [ % , ι l ]
    transpⱼ : ∀ {A l P t s u e}
              → Γ ⊢ A ^ [ ! , l ]
              → Γ ∙ A ^ [ ! , l ] ⊢ P ^ [ % , l ]
              → Γ ⊢ t ∷ A ^ [ ! , l ]
              → Γ ⊢ s ∷ P [ t ] ^ [ % , l ]
              → Γ ⊢ u ∷ A ^ [ ! , l ]
              → Γ ⊢ e ∷ (Id A t u) ^ [ % , l ]
              → Γ ⊢ transp A P t s u e ∷ P [ u ] ^ [ % , l ]
    castⱼ : ∀ {A B r e t}
            → Γ ⊢ A ∷ Univ r ⁰ ^ [ ! , next ⁰ ]
            → Γ ⊢ B ∷ Univ r ⁰ ^ [ ! , next ⁰ ]
            → Γ ⊢ e ∷ (Id (Univ r ⁰) A B) ^ [ % , next ⁰ ]
            → Γ ⊢ t ∷ A ^ [ r , ι ⁰ ]
            → Γ ⊢ cast ⁰ A B e t ∷ B ^ [ r , ι ⁰ ]
    castreflⱼ : ∀ {A t}
                 → Γ ⊢ A ∷ U ⁰ ^ [ ! , next ⁰ ]
                 → Γ ⊢ t ∷ A ^ [ ! , ι ⁰ ]
                 → Γ ⊢ castrefl A t ∷ (Id A t (cast ⁰ A A (Idrefl (U ⁰) A) t)) ^ [ % , ι ⁰ ]
    conv   : ∀ {t A B r}
           → Γ ⊢ t ∷ A ^ r
           → Γ ⊢ A ≡ B ^ r
           → Γ ⊢ t ∷ B ^ r

  -- Type equality
  data _⊢_≡_^_ (Γ : Con Term) : Term → Term → TypeInfo → Set where
    univ   : ∀ {A B r l}
           → Γ ⊢ A ≡ B ∷ (Univ r l) ^ [ ! , next l ]
           → Γ ⊢ A ≡ B ^ [ r , ι l ]
    refl   : ∀ {A r}
           → Γ ⊢ A ^ r
           → Γ ⊢ A ≡ A ^ r
    sym    : ∀ {A B r}
           → Γ ⊢ A ≡ B ^ r
           → Γ ⊢ B ≡ A ^ r
    trans  : ∀ {A B C r}
           → Γ ⊢ A ≡ B ^ r
           → Γ ⊢ B ≡ C ^ r
           → Γ ⊢ A ≡ C ^ r

  -- Term equality
  data _⊢_≡_∷_^_ (Γ : Con Term) : Term → Term → Term → TypeInfo → Set where
    refl        : ∀ {t A l}
                → Γ ⊢ t ∷ A ^ [ ! , l ]
                → Γ ⊢ t ≡ t ∷ A ^ [ ! , l ]
    sym         : ∀ {t u A l}
                → Γ ⊢ t ≡ u ∷ A ^ [ ! , l ]
                → Γ ⊢ u ≡ t ∷ A ^ [ ! , l ]
    trans       : ∀ {t u v A l}
                → Γ ⊢ t ≡ u ∷ A ^ [ ! , l ]
                → Γ ⊢ u ≡ v ∷ A ^ [ ! , l ]
                → Γ ⊢ t ≡ v ∷ A ^ [ ! , l ]
    conv        : ∀ {A B r t u}
                → Γ ⊢ t ≡ u ∷ A ^ r
                → Γ ⊢ A ≡ B ^ r
                → Γ ⊢ t ≡ u ∷ B ^ r
    Π-cong      : ∀ {E F G H rF lF rG lG l}
                → lF ≤ l
                → lG ≤ l
                → Γ     ⊢ F ^ [ rF , ι lF ]
                → Γ     ⊢ F ≡ H       ∷ (Univ rF lF) ^ [ ! , next lF ]
                → Γ ∙ F ^ [ rF , ι lF ] ⊢ G ≡ E       ∷ (Univ rG lG) ^ [ ! , next lG ]
                → Γ     ⊢ Π F ^ rF ° lF ▹ G ° lG ° l ≡ Π H ^ rF ° lF ▹ E ° lG ° l ∷ (Univ rG l) ^ [ ! , next l ]
    ∃-cong      : ∀ {E F G H l}
                → Γ     ⊢ F ^ [ % , ι l ]
                → Γ     ⊢ F ≡ H       ∷ SProp l ^ [ ! , next l ]
                → Γ ∙ F ^ [ % , ι l ] ⊢ G ≡ E       ∷ SProp l ^ [ ! , next l ]
                → Γ     ⊢ ∃ F ▹ G ≡ ∃ H ▹ E ∷ SProp l ^ [ ! , next l ]
    app-cong    : ∀ {a b f g F G rF lF lG l}
                → Γ ⊢ f ≡ g ∷ Π F ^ rF ° lF ▹ G ° lG ° l ^ [ ! , ι l ]
                → Γ ⊢ a ≡ b ∷ F ^ [ rF , ι lF ]
                → Γ ⊢ f ∘ a ^ l ≡ g ∘ b ^ l ∷ G [ a ] ^ [ ! , ι lG ]
    β-red       : ∀ {a t F rF lF G lG l}
                → lF ≤ l
                → lG ≤ l
                → Γ     ⊢ F ^ [ rF , ι lF ]
                → Γ ∙ F ^ [ rF , ι lF ] ⊢ t ∷ G ^ [ ! , ι lG ]
                → Γ     ⊢ a ∷ F ^ [ rF , ι lF ]
                → Γ     ⊢ (lam F ▹ t ^ l) ∘ a ^ l ≡ t [ a ] ∷ G [ a ] ^ [ ! , ι lG ]
    η-eq        : ∀ {f g F rF lF lG l G}
                → lF ≤ l
                → lG ≤ l
                → Γ     ⊢ F ^ [ rF , ι lF ]
                → Γ     ⊢ f ∷ Π F ^ rF ° lF ▹ G ° lG ° l ^ [ ! , ι l ]
                → Γ     ⊢ g ∷ Π F ^ rF ° lF ▹ G ° lG ° l ^ [ ! , ι l ]
                → Γ ∙ F ^ [ rF , ι lF ] ⊢ wk1 f ∘ var Nat.zero ^ l ≡ wk1 g ∘ var Nat.zero ^ l ∷ G ^ [ ! , ι lG ]
                → Γ     ⊢ f ≡ g ∷ Π F ^ rF ° lF ▹ G ° lG ° l ^ [ ! , ι l ]
    suc-cong    : ∀ {m n}
                → Γ ⊢ m ≡ n ∷ ℕ ^ [ ! ,  ι ⁰ ]
                → Γ ⊢ suc m ≡ suc n ∷ ℕ ^ [ ! ,  ι ⁰ ]
    natrec-cong : ∀ {z z′ s s′ n n′ F F′ l}
                → Γ ∙ ℕ ^ [ ! ,  ι ⁰ ] ⊢ F ≡ F′ ^ [ ! , ι l ]
                → Γ     ⊢ z ≡ z′ ∷ F [ zero ] ^ [ ! , ι l ]
                → Γ     ⊢ s ≡ s′ ∷ Π ℕ ^ ! ° ⁰ ▹ (F ^ ! ° l ▹▹ F [ suc (var Nat.zero) ]↑ ° l ° l) ° l ° l ^ [ ! , ι l  ]
                → Γ     ⊢ n ≡ n′ ∷ ℕ ^ [ ! ,  ι ⁰ ]
                → Γ     ⊢ natrec l F z s n ≡ natrec l F′ z′ s′ n′ ∷ F [ n ] ^ [ ! , ι l ]
    natrec-zero : ∀ {z s F l}
                → Γ ∙ ℕ ^ [ ! ,  ι ⁰ ] ⊢ F ^ [ ! , ι l ]
                → Γ     ⊢ z ∷ F [ zero ] ^ [ ! , ι l ]
                → Γ     ⊢ s ∷ Π ℕ ^ ! ° ⁰ ▹ (F ^ ! ° l ▹▹ F [ suc (var Nat.zero) ]↑ ° l ° l) ° l ° l ^ [ ! , ι l ]
                → Γ     ⊢ natrec l F z s zero ≡ z ∷ F [ zero ] ^ [ ! , ι l ]
    natrec-suc  : ∀ {n z s F l}
                → Γ     ⊢ n ∷ ℕ ^ [ ! ,  ι ⁰ ]
                → Γ ∙ ℕ ^ [ ! ,  ι ⁰ ] ⊢ F ^ [ ! , ι l ]
                → Γ     ⊢ z ∷ F [ zero ] ^ [ ! , ι l ]
                → Γ     ⊢ s ∷ Π ℕ ^ ! ° ⁰ ▹ (F ^ ! ° l ▹▹ F [ suc (var Nat.zero) ]↑ ° l ° l) ° l ° l ^ [ ! , ι l ]
                → Γ     ⊢ natrec l F z s (suc n) ≡ (s ∘ n ^ l) ∘ (natrec l F z s n) ^ l
                        ∷ F [ suc n ] ^ [ ! , ι l ]
    Emptyrec-cong : ∀ {A A' l lEmpty e e'}
                → Γ ⊢ A ≡ A' ^ [ ! , ι l ]
                → Γ ⊢ e ∷ Empty lEmpty ^ [ % , ι lEmpty ]
                → Γ ⊢ e' ∷ Empty lEmpty ^ [ % , ι lEmpty ]
                → Γ ⊢ Emptyrec l lEmpty  A e ≡ Emptyrec l lEmpty  A' e' ∷ A ^ [ ! , ι l ]
    proof-irrelevance : ∀ {t u A l}
                      → Γ ⊢ t ∷ A ^ [ % , l ]
                      → Γ ⊢ u ∷ A ^ [ % , l ]
                      → Γ ⊢ t ≡ u ∷ A ^ [ % , l ]
    Id-cong : ∀ {A A' l t t' u u'}
              → Γ ⊢ A ≡ A' ∷ Univ ! l ^ [ ! , next l ]
              → Γ ⊢ t ≡ t' ∷ A ^ [ ! , ι l ]
              → Γ ⊢ u ≡ u' ∷ A ^ [ ! , ι l ]
              → Γ ⊢ Id A t u ≡ Id A' t' u' ∷ SProp l ^ [ ! , next l ]
    Id-Π : ∀ {A rA lA lB l B t u}
           → lA ≤ l
           → lB ≤ l
           → Γ ⊢ A ∷ Univ rA lA ^ [ ! , next lA ]
           → Γ ∙ A ^ [ rA , ι lA ] ⊢ B ∷ Univ ! lB ^ [ ! , next lB ]
           → Γ ⊢ t ∷ (Π A ^ rA ° lA ▹ B ° lB ° l) ^ [ ! , ι l ]
           → Γ ⊢ u ∷ (Π A ^ rA ° lA ▹ B ° lB ° l) ^ [ ! , ι l ]
           → Γ ⊢ (Id (Π A ^ rA ° lA ▹ B ° lB ° l) t u)
                 ≡ Π A ^ rA ° lA ▹ (Id B ((wk1 t) ∘ (var 0) ^ l) ((wk1 u) ∘ (var 0) ^ l)) ° lB ° l
                 ∷ SProp l ^ [ ! , next l ]
    Id-ℕ-00 : ⊢ Γ
           → Γ ⊢ (Id ℕ zero zero)
                  ≡ Unit {⁰}
                  ∷ SProp ⁰ ^ [ ! , next ⁰ ]
    Id-ℕ-SS : ∀ {m n}
              → Γ ⊢ m ∷ ℕ ^ [ ! ,  ι ⁰ ]
              → Γ ⊢ n ∷ ℕ ^ [ ! ,  ι ⁰ ]
              → Γ ⊢ (Id ℕ (suc m) (suc n))
                    ≡ (Id ℕ m n)
                    ∷ SProp ⁰ ^ [ ! , next ⁰ ]
    Id-U-ΠΠ : ∀ {A A' rA B B'}
              → Γ ⊢ A ∷ (Univ rA ⁰) ^ [ ! , next ⁰ ]
              → Γ ∙ A ^ [ rA , ι ⁰ ] ⊢ B ∷ U ⁰ ^ [ ! , next ⁰ ]
              → Γ ⊢ A' ∷ (Univ rA ⁰) ^ [ ! , next ⁰ ]
              → Γ ∙ A' ^ [ rA , ι ⁰ ] ⊢ B' ∷ U ⁰ ^ [ ! , next ⁰ ]
              → Γ ⊢ (Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰))
                    ≡ ∃ (Id (Univ rA ⁰) A A') ▹
                      (Π (wk1 A') ^ rA ° ⁰ ▹ Id (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) ]↑)
                        (wk (lift (step id)) B') ° ¹ ° ¹)
                  ∷ SProp ¹ ^ [ ! , next ¹ ]
    Id-U-ℕℕ : ⊢ Γ
            → Γ ⊢ Id (U ⁰) ℕ ℕ
                  ≡ Unit {¹}
                  ∷ (SProp ¹) ^ [ ! , next ¹ ]
    Id-SProp : ∀ {A B}
               → Γ ⊢ A ∷ SProp ⁰ ^ [ ! , next ⁰ ]
               → Γ ⊢ B ∷ SProp ⁰ ^ [ ! , next ⁰ ]
               → Γ ⊢ Id (SProp ⁰) A B
                     ≡ (A ^ % ° ⁰ ▹▹ B ° ⁰ ° ¹) ×× (B ^ % ° ⁰ ▹▹ A ° ⁰ ° ¹)
                     ∷ SProp ¹ ^ [ ! , next ¹ ]
    Id-ℕ-0S : ∀ {t}
            → Γ ⊢ t ∷ ℕ ^ [ ! , ι ⁰ ]
            → Γ ⊢ Id ℕ zero (suc t) ≡ Empty ⁰ ∷ (SProp ⁰) ^ [ ! , next ⁰ ]
    Id-ℕ-S0 : ∀ {t}
            → Γ ⊢ t ∷ ℕ ^ [ ! , ι ⁰ ]
            → Γ ⊢ Id ℕ (suc t) zero ≡ Empty ⁰ ∷ (SProp ⁰) ^ [ ! , next ⁰ ]
    Id-U-ℕΠ : ∀ {A rA B}
            → Γ ⊢ A ∷ Univ rA ⁰ ^ [ ! , next ⁰ ]
            → Γ ∙ A ^ [ rA , ι ⁰ ] ⊢ B ∷ U ⁰ ^ [ ! , next ⁰ ]
            → Γ ⊢ Id (U ⁰) ℕ (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) ≡ Empty ¹ ∷ SProp ¹ ^ [ ! , next ¹ ]
    Id-U-Πℕ : ∀ {A rA B}
            → Γ ⊢ A ∷ Univ rA ⁰ ^ [ ! , next ⁰ ]
            → Γ ∙ A ^ [ rA , ι ⁰ ] ⊢ B ∷ U ⁰ ^ [ ! , next ⁰ ]
            → Γ ⊢ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) ℕ ≡ Empty ¹ ∷ SProp ¹ ^ [ ! , next ¹ ]
    Id-U-ΠΠ!% : ∀ {A rA B A' rA' B' }
            → rA PE.≢ rA'
            → Γ ⊢ A ∷ Univ rA ⁰ ^ [ ! , next ⁰ ]
            → Γ ∙ A ^ [ rA , ι ⁰ ] ⊢ B ∷ U ⁰ ^ [ ! , next ⁰ ]
            → Γ ⊢ A' ∷ Univ rA' ⁰ ^ [ ! , next ⁰ ]
            → Γ ∙ A' ^ [ rA' , ι ⁰ ] ⊢ B' ∷ U ⁰ ^ [ ! , next ⁰ ]
            → Γ ⊢ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) (Π A' ^ rA' ° ⁰ ▹ B' ° ⁰ ° ⁰) ≡ Empty ¹ ∷ SProp ¹ ^ [ ! , next ¹ ]
    cast-cong : ∀ {A A' B B' e e' t t'} → let l = ⁰ in
                  Γ ⊢ A ≡ A' ∷ U l ^ [ ! , next l ]
                → Γ ⊢ B ≡ B' ∷ U l ^ [ ! , next l ]
                → Γ ⊢ t ≡ t' ∷ A ^ [ ! , ι l ]
                → Γ ⊢ e ∷ (Id (U ⁰) A B) ^ [ % , next ⁰ ]
                → Γ ⊢ e' ∷ (Id (U ⁰) A' B') ^ [ % , next ⁰ ]
                → Γ ⊢ cast l A B e t ≡ cast l A' B' e' t' ∷ B ^ [ ! , ι l ]
    cast-Π : ∀ {A A' rA B B' e f} → let l = ⁰ in let lA = ⁰ in let lB = ⁰ in
               Γ ⊢ A ∷ (Univ rA lA) ^ [ ! , next lA ]
             → Γ ∙ A ^ [ rA , ι lA ] ⊢ B ∷ U lB ^ [ ! , next lB ]
             → Γ ⊢ A' ∷ (Univ rA lA) ^ [ ! , next lA ]
             → Γ ∙ A' ^ [ rA , ι lA ] ⊢ B' ∷ U lB ^ [ ! , next lB ]
             → Γ ⊢ e ∷ Id (U l) (Π A ^ rA ° lA ▹ B ° lB ° l) (Π A' ^ rA ° lA ▹ B' ° lB ° l) ^ [ % , next l ]
             → Γ ⊢ f ∷ (Π A ^ rA ° lA ▹ B ° lB ° l) ^ [ ! , ι l ]
             → Γ ⊢ (cast l (Π A ^ rA ° lA ▹ B ° lB ° l) (Π A' ^ rA ° lA ▹ B' ° lB ° 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))
                      ^ l)
                   ∷ Π A' ^ rA ° lA ▹ B' ° lB ° l ^ [ ! , ι l ]
    cast-ℕ-0 : ∀ {e}
               → Γ ⊢ e ∷ Id (U ⁰) ℕ ℕ ^ [ % , next ⁰ ]
               → Γ ⊢ cast ⁰ ℕ ℕ e zero
                   ≡ zero
                   ∷ ℕ ^ [ ! , ι ⁰ ]
    cast-ℕ-S : ∀ {e n}
               → Γ ⊢ e ∷ Id (U ⁰) ℕ ℕ ^ [ % , next ⁰ ]
               → Γ ⊢ n ∷ ℕ ^ [ ! , ι ⁰ ]
               → Γ ⊢ cast ⁰ ℕ ℕ e (suc n)
                   ≡ suc (cast ⁰ ℕ ℕ e n)
                   ∷ ℕ ^ [ ! , ι ⁰ ]

mutual
  data _⊢_⇒_∷_^_ (Γ : Con Term) : Term → Term → Term → TypeLevel → Set where
    conv         : ∀ {A B l t u}
                 → Γ ⊢ t ⇒ u ∷ A ^ l
                 → Γ ⊢ A ≡ B ^ [ ! , l ]
                 → Γ ⊢ t ⇒ u ∷ B ^ l
    app-subst    : ∀ {A B t u a rA lA lB l}
                 → Γ ⊢ t ⇒ u ∷ Π A ^ rA ° lA ▹ B ° lB ° l ^ ι l
                 → Γ ⊢ a ∷ A ^ [ rA , ι lA ]
                 → Γ ⊢ t ∘ a ^ l ⇒ u ∘ a ^ l  ∷ B [ a ] ^ ι lB
    β-red        : ∀ {A B lA lB a t rA l}
                 → lA ≤ l
                 → lB ≤ l
                 → Γ     ⊢ A ^ [ rA , ι lA ]
                 → Γ ∙ A ^ [ rA , ι lA ] ⊢ t ∷ B ^ [ ! , ι lB ]
                 → Γ     ⊢ a ∷ A ^ [ rA , ι lA ]
                 → Γ     ⊢ (lam A ▹ t ^ l) ∘ a ^ l ⇒ t [ a ] ∷ B [ a ] ^ ι lB
    natrec-subst : ∀ {z s n n′ F l}
                 → Γ ∙ ℕ ^ [ ! , ι ⁰ ] ⊢ F ^ [ ! , ι l ]
                 → Γ     ⊢ z ∷ F [ zero ] ^ [ ! , ι l ]
                 → Γ     ⊢ s ∷ Π ℕ ^ ! ° ⁰ ▹ (F ^ ! ° l ▹▹ F [ suc (var Nat.zero) ]↑ ° l ° l) ° l ° l ^ [ ! , ι l ]
                 → Γ     ⊢ n ⇒ n′ ∷ ℕ ^ ι ⁰
                 → Γ     ⊢ natrec l F z s n ⇒ natrec l F z s n′ ∷ F [ n ] ^ ι l
    natrec-zero  : ∀ {z s F l }
                 → Γ ∙ ℕ ^ [ ! , ι ⁰ ] ⊢ F ^ [ ! , ι l ]
                 → Γ     ⊢ z ∷ F [ zero ] ^ [ ! , ι l ]
                 → Γ     ⊢ s ∷ Π ℕ ^ ! ° ⁰ ▹ (F ^ ! ° l ▹▹ F [ suc (var Nat.zero) ]↑ ° l ° l ) ° l ° l ^ [ ! , ι l ]
                 → Γ     ⊢ natrec l F z s zero ⇒ z ∷ F [ zero ] ^ ι l
    natrec-suc   : ∀ {n z s F l}
                 → Γ     ⊢ n ∷ ℕ ^ [ ! , ι ⁰ ]
                 → Γ ∙ ℕ ^ [ ! , ι ⁰ ] ⊢ F ^ [ ! , ι l ]
                 → Γ     ⊢ z ∷ F [ zero ] ^ [ ! , ι l ]
                 → Γ     ⊢ s ∷ Π ℕ ^ ! ° ⁰ ▹ (F ^ ! ° l ▹▹ F [ suc (var Nat.zero) ]↑ ° l ° l) ° l ° l ^ [ ! , ι l ]
                 → Γ     ⊢ natrec l F z s (suc n) ⇒ (s ∘ n ^ l) ∘ (natrec l F z s n) ^ l
                         ∷ F [ suc n ] ^ ι l
    Id-subst : ∀ {A A' l t u}
              → Γ ⊢ A ⇒ A' ∷ Univ ! l ^ next l
              → Γ ⊢ t ∷ A ^ [ ! , ι l ]
              → Γ ⊢ u ∷ A ^ [ ! , ι l ]
              → Γ ⊢ Id A t u ⇒ Id A' t u ∷ SProp l ^ next l
    Id-ℕ-subst : ∀ {m m' n}
              → Γ ⊢ m ⇒ m' ∷ ℕ ^ ι ⁰
              → Γ ⊢ n ∷ ℕ ^ [ ! , ι ⁰ ]
              → Γ ⊢ Id ℕ m n ⇒ Id ℕ m' n ∷ SProp ⁰ ^ next ⁰
    Id-ℕ-0-subst : ∀ {n n'}
              → Γ ⊢ n ⇒ n' ∷ ℕ ^ ι ⁰
              → Γ ⊢ Id ℕ zero n ⇒ Id ℕ zero n' ∷ SProp ⁰ ^ next ⁰
    Id-ℕ-S-subst : ∀ {m n n'}
              → Γ ⊢ m ∷ ℕ ^ [ ! , ι ⁰ ]
              → Γ ⊢ n ⇒ n' ∷ ℕ ^ ι ⁰
              → Γ ⊢ Id ℕ (suc m) n ⇒ Id ℕ (suc m) n' ∷ SProp ⁰ ^ next ⁰
    Id-U-subst : ∀ {A A' B}
              → Γ ⊢ A ⇒ A' ∷ U ⁰  ^ next ⁰
              → Γ ⊢ B ∷ U ⁰  ^ [ ! , next ⁰  ]
              → Γ ⊢ Id (U ⁰ ) A B ⇒ Id (U ⁰) A' B ∷ SProp ¹ ^ next ¹
    Id-U-ℕ-subst : ∀ {B B'}
              → Γ ⊢ B ⇒ B' ∷ U ⁰ ^ next ⁰
              → Γ ⊢ Id (U ⁰) ℕ B ⇒ Id (U ⁰) ℕ B' ∷ SProp ¹ ^ next ¹
    Id-U-Π-subst : ∀ {A rA P B B'}
              → Γ ⊢ A ∷ (Univ rA ⁰) ^ [ ! , next ⁰ ]
              → Γ ∙ A ^ [ rA , ι ⁰ ] ⊢ P ∷ U ⁰ ^ [ ! , next ⁰ ]
              → Γ ⊢ B ⇒ B' ∷ U ⁰ ^ next ⁰
              → Γ ⊢ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰) B ⇒ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰) B' ∷ SProp ¹ ^ next ¹
    Id-Π : ∀ {A rA lA lB l B t u}
           → lA ≤ l
           → lB ≤ l
           → Γ ⊢ A ∷ Univ rA lA ^ [ ! , next lA ]
           → Γ ∙ A ^ [ rA , ι lA ] ⊢ B  ∷ Univ ! lB ^ [ ! , next lB ]
           → Γ ⊢ t ∷ (Π A ^ rA ° lA ▹ B ° lB ° l) ^ [ ! , ι l ]
           → Γ ⊢ u ∷ (Π A ^ rA ° lA ▹ B ° lB ° l) ^ [ ! , ι l ]
           → Γ ⊢ (Id (Π A ^ rA ° lA ▹ B ° lB ° l) t u)
                 ⇒ Π A ^ rA ° lA ▹ (Id B ((wk1 t) ∘ (var 0) ^ l) ((wk1 u) ∘ (var 0) ^ l)) ° lB ° l
                 ∷ SProp l ^ next l
    Id-ℕ-00 : ⊢ Γ
            → Γ ⊢ (Id ℕ zero zero)
                  ⇒ Unit {⁰}
                  ∷ SProp ⁰ ^ next ⁰
    Id-ℕ-SS : ∀ {m n}
              → Γ ⊢ m ∷ ℕ ^ [ ! , ι ⁰ ]
              → Γ ⊢ n ∷ ℕ ^ [ ! , ι ⁰ ]
              → Γ ⊢ (Id ℕ (suc m) (suc n))
                    ⇒ (Id ℕ m n)
                    ∷ SProp ⁰ ^ next ⁰
    Id-U-ΠΠ : ∀ {A A' rA B B'}
              → Γ ⊢ A ∷ (Univ rA ⁰) ^ [ ! , next ⁰ ]
              → Γ ∙ A ^ [ rA , ι ⁰ ] ⊢ B ∷ U ⁰ ^ [ ! , next ⁰ ]
              → Γ ⊢ A' ∷ (Univ rA ⁰) ^ [ ! , next ⁰ ]
              → Γ ∙ A' ^ [ rA , ι ⁰ ] ⊢ B' ∷ U ⁰ ^ [ ! , next ⁰ ]
              → Γ ⊢ (Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰))
                    ⇒ ∃ (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') ° ¹ ° ¹)
                    ∷ SProp ¹ ^ next ¹
    Id-U-ℕℕ : ⊢ Γ
            → Γ ⊢ (Id (U ⁰) ℕ ℕ)
                  ⇒ Unit {¹}
                  ∷ SProp ¹ ^ next ¹
    Id-SProp : ∀ {A B}
               → Γ ⊢ A ∷ SProp ⁰ ^ [ ! , next ⁰ ]
               → Γ ⊢ B ∷ SProp ⁰ ^ [ ! , next ⁰ ]
               → Γ ⊢ Id (SProp ⁰) A B
                     ⇒ (A ^ % ° ⁰ ▹▹ B ° ⁰ ° ¹) ×× (B ^ % ° ⁰  ▹▹ A ° ⁰ ° ¹)
                     ∷ SProp ¹ ^ next ¹
    Id-ℕ-0S : ∀ {t}
            → Γ ⊢ t ∷ ℕ ^ [ ! , ι ⁰ ]
            → Γ ⊢ Id ℕ zero (suc t) ⇒ Empty ⁰ ∷ SProp ⁰ ^ next ⁰
    Id-ℕ-S0 : ∀ {t}
            → Γ ⊢ t ∷ ℕ ^ [ ! , ι ⁰ ]
            → Γ ⊢ Id ℕ (suc t) zero ⇒ Empty ⁰ ∷ SProp ⁰ ^ next ⁰
    Id-U-ℕΠ : ∀ {A rA B}
            → Γ ⊢ A ∷ Univ rA ⁰ ^ [ ! , next ⁰ ]
            → Γ ∙ A ^ [ rA , ι ⁰ ] ⊢ B ∷ U ⁰ ^ [ ! , next ⁰ ]
            → Γ ⊢ Id (U ⁰) ℕ (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) ⇒ Empty ¹ ∷ SProp ¹ ^ next ¹
    Id-U-Πℕ : ∀ {A rA B}
            → Γ ⊢ A ∷ Univ rA ⁰ ^ [ ! , next ⁰ ]
            → Γ ∙ A ^ [ rA , ι ⁰ ] ⊢ B ∷ U ⁰ ^ [ ! , next ⁰ ]
            → Γ ⊢ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) ℕ ⇒ Empty ¹ ∷ SProp ¹ ^ next ¹
    Id-U-ΠΠ!% : ∀ {A rA B A' rA' B' }
            → rA PE.≢ rA'
            → Γ ⊢ A ∷ Univ rA ⁰ ^ [ ! , next ⁰ ]
            → Γ ∙ A ^ [ rA , ι ⁰ ] ⊢ B ∷ U ⁰ ^ [ ! , next ⁰ ]
            → Γ ⊢ A' ∷ Univ rA' ⁰ ^ [ ! , next ⁰ ]
            → Γ ∙ A' ^ [ rA' , ι ⁰ ] ⊢ B' ∷ U ⁰ ^ [ ! , next ⁰ ]
            → Γ ⊢ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) (Π A' ^ rA' ° ⁰ ▹ B' ° ⁰ ° ⁰) ⇒ Empty ¹ ∷ SProp ¹ ^ next ¹
    cast-subst : ∀ {A A' B e t} → let l = ⁰ in
                    Γ ⊢ A ⇒ A' ∷ U l ^ next l
                  → Γ ⊢ B ∷ U l ^ [ ! , next l ]
                  → Γ ⊢ e ∷ Id (U l) A B ^ [ % , next l ]
                  → Γ ⊢ t ∷ A ^ [ ! , ι l ]
                  → Γ ⊢ cast l A B e t ⇒ cast l A' B e t ∷ B ^ ι l
    cast-ℕ-subst : ∀ {B B' e t}
                  → Γ ⊢ B ⇒ B' ∷ U ⁰ ^ next ⁰
                  → Γ ⊢ e ∷ Id (U ⁰) ℕ B ^ [ % , next ⁰ ]
                  → Γ ⊢ t ∷ ℕ ^ [ ! , ι ⁰ ]
                  → Γ ⊢ cast ⁰ ℕ B e t ⇒ cast ⁰ ℕ B' e t ∷ B ^ ι ⁰
    cast-Π-subst : ∀ {A rA P B B' e t} → let l = ⁰ in let lA = ⁰ in let lP = ⁰ in
                    Γ ⊢ A ∷ (Univ rA lA) ^ [ ! , next lA ]
                  → Γ ∙ A ^ [ rA , ι lA ] ⊢ P ∷ U lP ^ [ ! , next lA ]
                  → Γ ⊢ B ⇒ B' ∷ U l ^ next l
                  → Γ ⊢ e ∷ Id (U l) (Π A ^ rA ° lA ▹ P ° lP ° l) B ^ [ % , next l ]
                  → Γ ⊢ t ∷ (Π A ^ rA ° lA ▹ P ° lP ° l) ^ [ ! , ι l ]
                  → Γ ⊢ cast l (Π A ^ rA ° lA ▹ P ° lP ° l) B e t ⇒ cast l (Π A ^ rA ° lA ▹ P ° lP ° l) B' e t ∷ B ^ ι l
    cast-Π : ∀ {A A' rA B B' e f} → let l = ⁰ in
               Γ ⊢ A ∷ (Univ rA l) ^ [ ! , next l ]
             → Γ ∙ A ^ [ rA , ι l ] ⊢ B ∷ U l ^ [ ! , next l ]
             → Γ ⊢ A' ∷ (Univ rA l) ^ [ ! , next l ]
             → Γ ∙ A' ^ [ rA , ι l ] ⊢ B' ∷ U l ^ [ ! , next l ]
             → Γ ⊢ e ∷ Id (U l) (Π A ^ rA ° l ▹ B ° l ° l) (Π A' ^ rA ° l  ▹ B' ° l ° l) ^ [ % , next l ]
             → Γ ⊢ f ∷ (Π A ^ rA ° l ▹ B ° l ° l) ^ [ ! , ι 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))
                       ^ l )
                   ∷ Π A' ^ rA ° l ▹ B' ° l ° l ^ ι l
    cast-ℕ-0 : ∀ {e}
               → Γ ⊢ e ∷ Id (U ⁰) ℕ ℕ ^ [ % , next ⁰ ]
               → Γ ⊢ cast ⁰ ℕ ℕ e zero
                   ⇒ zero
                   ∷ ℕ ^ ι ⁰
    cast-ℕ-S : ∀ {e n}
               → Γ ⊢ e ∷ Id (U ⁰) ℕ ℕ ^ [ % , next ⁰ ]
               → Γ ⊢ n ∷ ℕ ^ [ ! , ι ⁰ ]
               → Γ ⊢ cast ⁰ ℕ ℕ e (suc n)
                   ⇒ suc (cast ⁰ ℕ ℕ e n)
                   ∷ ℕ ^ ι ⁰

    cast-ℕ-cong : ∀ {e t u}
               → Γ ⊢ e ∷ Id (U ⁰) ℕ ℕ ^ [ % , next ⁰ ]
               → Γ ⊢ t ⇒ u ∷ ℕ ^ ι ⁰
               → Γ ⊢ cast ⁰ ℕ ℕ e t
                   ⇒ cast ⁰ ℕ ℕ e u
                   ∷ ℕ ^ ι ⁰

  -- Type reduction
  data _⊢_⇒_^_ (Γ : Con Term) : Term → Term → TypeInfo → Set where
    univ : ∀ {A B r l}
         → Γ ⊢ A ⇒ B ∷ (Univ r l) ^ next l
         → Γ ⊢ A ⇒ B ^ [ r , ι l ]

-- Term reduction closure
data _⊢_⇒*_∷_^_ (Γ : Con Term) : Term → Term → Term → TypeLevel → Set where
  id  : ∀ {A l t}
      → Γ ⊢ t ∷ A ^ [ ! , l ]
      → Γ ⊢ t ⇒* t ∷ A ^ l
  _⇨_ : ∀ {A l t t′ u}
      → Γ ⊢ t  ⇒  t′ ∷ A ^ l
      → Γ ⊢ t′ ⇒* u  ∷ A ^ l
      → Γ ⊢ t  ⇒* u  ∷ A ^ l

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

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

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

-- Type equality with well-formed types
_⊢_:≡:_^_ : (Γ : Con Term) → Term → Term → TypeInfo → Set
Γ ⊢ A :≡: B ^ r = Γ ⊢ A ^ r × Γ ⊢ B ^ r × (Γ ⊢ A ≡ B ^ r)

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

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

open _⊢_:⇒*:_^_ using () renaming (D to red) public

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

open _⊢_:⇒*:_∷_^_ using () renaming (d to redₜ) public

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

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

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

-- Some derivable rules
Unitⱼ : ∀ {Γ l} (⊢Γ : ⊢ Γ)
      → Γ ⊢ Unit ∷ SProp l ^ [ ! , next l ]
Unitⱼ ⊢Γ = Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ Emptyⱼ ⊢Γ ▹ Emptyⱼ (⊢Γ ∙ univ (Emptyⱼ ⊢Γ))

typeUnit : ∀ {l} →  Type (Unit {l})
typeUnit = Πₙ

Ugenⱼ : ∀ {r Γ l} → ⊢ Γ → Γ ⊢ Univ r l ^ [ ! , next l ]
Ugenⱼ {l = ⁰} ⊢Γ = univ (univ 0<1 ⊢Γ)
Ugenⱼ {l = ¹} ⊢Γ = Uⱼ ⊢Γ

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module BBHeap.Height.Convert {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import BBHeap _≤_
open import BBHeap.Properties _≤_
open import BBHeap.Height _≤_
open import BHeap _≤_ hiding (forget) renaming (height to heightₙ)
open import Data.List
open import Data.Nat renaming (_≤_ to _≤ₙ_)
open import Data.Nat.Properties
open import Data.Sum
open import Function using (_∘_)
open import OList _≤_
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding (trans)
open import SNat

open DecTotalOrder decTotalOrder hiding (refl)

data _⊳_ : {b b' : Bound} → BHeap b → BHeap b' → Set where
  ⊳leaf : {b b' : Bound}
                   → lf {b} ⊳ lf {b'}
  ⊳left : {b b' : Bound}{x : A}{l r : BHeap (val x)}{l' : BHeap b'}
                   (b≤x : LeB b (val x))
                   → l ⊳ r → l ⊳ l'
                   → (nd b≤x l r) ⊳ l'
  ⊳both : {b b' : Bound}{x x' : A}{l r : BHeap (val x)}{l' r' : BHeap (val x')}
                   (b≤x : LeB b (val x))
                   (b'≤x' : LeB b' (val x'))
                   → l ⊳ r
                   → l ⊳ l'
                   → l ⊳ r'
                   → (nd b≤x l r) ⊳ (nd b'≤x' l' r')

lemma-≃-⊳ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ≃ r → relax l ⊳ relax r
lemma-≃-⊳ ≃lf = ⊳leaf
lemma-≃-⊳ (≃nd b≤x b'≤x' _ _ l≃r l'≃r' l≃l') = ⊳both b≤x b'≤x' (lemma-≃-⊳ l≃r) (lemma-≃-⊳ l≃l') (lemma-≃-⊳ (trans≃ l≃l' l'≃r'))

lemma-⋗-⊳ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ⋗ r → relax l ⊳ relax r
lemma-⋗-⊳ (⋗lf b≤x) = ⊳left b≤x ⊳leaf ⊳leaf
lemma-⋗-⊳ (⋗nd b≤x b'≤x' _ _ l≃r l'≃r' l⋗l') = ⊳both b≤x b'≤x' (lemma-≃-⊳ l≃r) (lemma-⋗-⊳ l⋗l') (lemma-⋗-⊳ (lemma⋗≃ l⋗l' l'≃r'))

lemma-⋙-⊳ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ⋙ r → relax l ⊳ relax r
lemma-⋙-⊳ (⋙lf b≤x) = ⊳left b≤x ⊳leaf ⊳leaf
lemma-⋙-⊳ (⋙rl b≤x b'≤x' _ l≃r l'⋘r' l⋗r') = ⊳both b≤x b'≤x' (lemma-≃-⊳ l≃r) (lemma-⋙-⊳ (lemma-⋘-⋗ l'⋘r' l⋗r')) (lemma-⋗-⊳ l⋗r')
lemma-⋙-⊳ (⋙rr b≤x b'≤x' _ l≃r l'⋙r' l≃l') =  ⊳both b≤x b'≤x' (lemma-≃-⊳ l≃r) (lemma-≃-⊳ l≃l') (lemma-⋙-⊳ (lemma-≃-⋙ l≃l' l'⋙r'))

lemma-⋘-⊳ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ⋘ r → relax l ⊳ relax r
lemma-⋘-⊳ lf⋘ = ⊳leaf
lemma-⋘-⊳ (ll⋘ b≤x b'≤x' l⋘r _ l'≃r' r≃l') = ⊳both b≤x b'≤x' (lemma-⋘-⊳ l⋘r) (lemma-⋘-⊳ (lemma-⋘-≃ l⋘r r≃l')) (lemma-⋘-⊳ (lemma-⋘-≃ l⋘r (trans≃ r≃l' l'≃r')))
lemma-⋘-⊳ (lr⋘ b≤x b'≤x' l⋙r _ l'≃r' l⋗l') = ⊳both b≤x b'≤x' (lemma-⋙-⊳ l⋙r) (lemma-⋗-⊳ l⋗l') (lemma-⋗-⊳ (lemma⋗≃ l⋗l' l'≃r'))

lemma-⊳-heightₙ : {b b' : Bound}{l : BHeap b}{r : BHeap b'} → l ⊳ r → heightₙ r ≤ₙ heightₙ l
lemma-⊳-heightₙ ⊳leaf = z≤n
lemma-⊳-heightₙ (⊳left {l = l} {r = r} b≤x l⊳r l⊳l')
    with total (heightₙ l) (heightₙ r)
... | inj₁ hl≤hr rewrite antisym (lemma-⊳-heightₙ l⊳r) hl≤hr = ≤-step (lemma-⊳-heightₙ l⊳l')
... | inj₂ hr≤hl = trans (lemma-⊳-heightₙ l⊳l') (≤-step (reflexive refl))
lemma-⊳-heightₙ (⊳both {l = l} {r = r} {l' = l'} {r' = r'} b≤x b'≤x' l⊳r l⊳l' l⊳r')
    with total (heightₙ l) (heightₙ r) | total (heightₙ l') (heightₙ r')
... | inj₁ hl≤hr | inj₁ hl'≤hr' rewrite antisym (lemma-⊳-heightₙ l⊳r) hl≤hr = s≤s (lemma-⊳-heightₙ l⊳r')
... | inj₁ hl≤hr | inj₂ hr'≤hl' rewrite antisym (lemma-⊳-heightₙ l⊳r) hl≤hr = s≤s (lemma-⊳-heightₙ l⊳l')
... | inj₂ hr≤hl | inj₁ hl'≤hr' = s≤s (lemma-⊳-heightₙ l⊳r')
... | inj₂ hr≤hl | inj₂ hr'≤hl' = s≤s (lemma-⊳-heightₙ l⊳l')

theorem-height-relax : {b : Bound}(h : BBHeap b) → toNat (height h) ≡ heightₙ (relax h)
theorem-height-relax leaf = refl
theorem-height-relax (left {l = l} {r = r} _ l⋘r)
    with total (heightₙ (relax l)) (heightₙ (relax r))
... | inj₁ hl≤hr rewrite antisym (lemma-⊳-heightₙ (lemma-⋘-⊳ l⋘r)) hl≤hr | theorem-height-relax l = refl
... | inj₂ hr≤hl rewrite theorem-height-relax l = refl
theorem-height-relax (right {l = l} {r = r} _ l⋙r)
    with total (heightₙ (relax l)) (heightₙ (relax r))
... | inj₁ hl≤hr rewrite antisym (lemma-⊳-heightₙ (lemma-⋙-⊳ l⋙r)) hl≤hr | theorem-height-relax l = refl
... | inj₂ hr≤hl rewrite theorem-height-relax l = refl

ext: agda

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --type-in-type #-}

module FusionNotes where

{-
Idea: doing computation at compile time instead of at runtime

VTy : MTy   -- value types       (inductive data)
CTy : MTy   -- computation types (functions)
MTy : MTy   -- meta types        (meta TT types)

VTy ≤ CTy   (implicit cumulativity)

^_  : VTy → MTy        -- lifting
^_  : CTy → MTy
<_> : A → ^A           -- quote
~_  : ^A → A           -- splice

Nat  : VTy
^Nat  (has no elimination rule)

Solution: Church-encodings

- initial encoding:

  ^Nat ~ ((N : CTy) → (^N → ^N) → ^N → ^N)      βη

   List : VTy → VTy

  ^(List A) ~ ((L : CTy) → (^A → ^L → ^L) → ^L → ^L)
            ~ ((L : CTy) → (A → L → L) → L → L)

  A     : algebraic/inductive signature      e.g. (L : Set, cons : A → L → L, nil : L)
  A-Alg : MTy                                e.g. (List A)-Alg = (L : CTy) × (cons : A → L → L) × (nil : L)
  U : A-Alg → CTy  (underlying set functor)  e.g. U (L, cons, nil) = L

  - initial:  IChurch : Sig → MTy
              IChurch A = (α : A-Alg) → U α         IChurch ListSig = (α : ((L : CTy) × (cons : A → L → L) × (nil : L))) → U α
                                                                    = ((L : CTy) → (A → L → L) → L → L)

  - terminal: TChurch : CoSig → MTy
              TChurch A = (α : A-Alg) × U α

-- data List a = Nil | Cons a (List a)         ListSig   = (L : Set, cons : A → L → L, nil : L)
-- codata List a = Nil | Cons a (List a)       CoListSig = (L : Set, destruct : L → Maybe (A, L))

-- (more elegant: F-algebras, F-coalgebras)

CMaybe : MTy → MTy
CMaybe A = (M : MTy) → (A → M) → M → M                    -- Church Maybe

CoList : VTy → MTy
CoList A = (CL : VTy) × (next: CL → Maybe (A × CL)) × CL
         = (CL : VTy) × (next: CL → CMaybe (A × CL)) × CL

-- high-level: we want to optimize modulo positive η-rules
--  Bool : nf modulo η: exponential time
--  Boolᴺ → Bool

-- Compiler knows about *some* η-rules
--   e.g. GHC case-commutation

       runtime               meta             runtime
-- positive types  -->   IChurch rep   -->   residualize       (CPS transformations)
                   -->   TChurch rep   -->   residualize       (state machine transformation)

-- Initial Church encoding:
  + It works on all inductive types
  + It's relatively easy to efficiently compile
  - Only folding functions   (zip doesn't work for lists)

  "push" iterator, "internal" iterator

-- Terminal encoding:
  + More general for streams/dataflow stuff  (zip works fine)
  - In many cases doesn't make practical sense
    - For finite types it's just the same as initial encoding, but more complicated to use
  - Compiling state machines is pretty complicated

        (State : VTy) × (step : State → .....) × (seed : State)

                  step : (A + B + C + D + E) → (A + B + C + D + E + ⊤)

             --> turn it to tail-recursive loop
             -->   we have to turn lots of _+_ case splits into a *mutual* set of functions

             mutual
              f : A → B
              g : A → C

             fg : A + A → B + C
             fg (inj₁ a) = ... call either f or g recursively
             fg (inj₂ a) = ... call either f or g recursively

             -- job: do this transformation in reverse (not easy)

  "pull" stream, "external" iterator

-- Example:
   Rust iterator:
      - terminal encoding
      - *not* abstract (does not use sigma types) (internal state leaks to the outside)
          -- map : (A → B) → Stream S A → Stream S B
          --   easy to extend with typeclass magic

What I want:

  - constraints: only simple type theory at runtime, no closures

-}

--------------------------------------------------------------------------------

-- Comp/Val/Meta, 2LVLTT setting
-- fold fusion, stream fusion comparison
-- (external/internal, push/pull, initial/terminal, abstract/transparent)
-- closure-freedom
-- monadic bind
-- sigma-freedom
-- call-pattern spec
-- stream : skip-stream or CoList?
-- hybrid: affine stream + push lists + asymmetric zip
-- Robinson & Lippmeier : Machine Fusion (with split optimization!)
--
-- What are fusing functions?
--   - Finite positive types can be mechanically CPS'd into fusing defs
--               (but it is a lot weaker than full positive η!)
--   - Inifite types can't
--   - Auto-fusion for infinite types = supercompilation

--------------------------------------------------------------------------------

open import Data.List using (_∷_; [])
import Data.List as L

open import Data.Nat
open import Data.Product
  renaming (proj₁ to ₁; proj₂ to ₂) hiding (map; zip)
open import Function
import Data.Bool as B

--------------------------------------------------------------------------------

infix 3 _==_
_==_ : ℕ → ℕ → B.Bool
zero  == zero  = B.true
zero  == suc y = B.false
suc x == zero  = B.false
suc x == suc y = x == y

caseℕ : ∀ {A : Set} → ℕ → A → (ℕ → A) → A
caseℕ zero    z s = z
caseℕ (suc n) z s = s n

-- map (_+_ 3) ∘ countDown

-- λ x L c n →
--   fix
--   (λ go n₁ →
--      caseℕ n₁ (c 3 n) (λ n₂ → c (suc (suc (suc (suc n₂)))) (go n₂)))
--   x

module InitialList where
  -- Initial Church lists
  --------------------------------------------------------------------------------

  List : Set → Set
  List A = (L : Set) → (A → L → L) → L → L

  nil : ∀ {A} → List A
  nil L c n = n

  cons : ∀ {A} → A → List A → List A
  cons a as L c n = c a (as L c n)

  -- map : ∀ {A B} → (A → B) → List A → List B
  -- map f [] = []
  -- map f (a:as) = f a : map f as

  map : ∀ {A B} → (A → B) → List A → List B
  map f as L c n =
    as L (λ a bs → c (f a) bs) n
    -- foldr (λ a bs → c (f a) bs) n as

  -- {-# NON_TERMINATING #-}
  -- fix : ∀ {A B : Set} → ((A → B) → A → B) → A → B
  -- fix f a = f (fix f) a

  postulate
    fix : ∀ {A B : Set} → ((A → B) → A → B) → A → B

  -- countDown 5 = [5, 4, 3, 2, 1, 0]
  -- "push" iteration: start with a loop, inline stuff later inside
  countDown : ℕ → List ℕ
  countDown n = λ L cons nil →
    fix (λ go n → caseℕ n
          (cons zero nil)
          (λ n → cons (suc n) (go n)))
        n

  take : ∀ {A} → ℕ → List A → List A
  take n as L cons nil = as _
    (λ a k n → caseℕ n
        nil
        (λ n → cons a (k n)))
    (λ _ → nil)
    n

  reverse : ∀ {A} → List A → List A
  reverse as L c n = as _ (λ a k acc → k (c a acc)) (λ acc → acc) n

  -- optimized by "call pattern specialization" in GHC
  drop : ∀ {A} → ℕ → List A → List A
  drop n as L cons nil = as _
    (λ a k n → caseℕ n
      (cons a (k 0))        -- drop 0 recursive calls drop 0 until the list ends
      (λ n → k n))          -- recursive call drop (n - 1)
    (λ _ → nil)
    n

  filter : ∀ {A} → (A → B.Bool) → List A → List A
  filter f as L cons nil = as _
    (λ a as → B.if f a then cons a as else as)
    nil

  foldl : ∀ {A B} → (B → A → B) → B → List A → B
  foldl f b as = as _ (λ a k b → k (f b a)) (λ b → b) b

  sum : List ℕ → ℕ
  sum = foldl _+_ 0

  downList : ∀ {A} → List A → L.List A   -- CPS to usual list
  downList as = as _ L._∷_ L.[]

  upList : ∀ {A} → L.List A → List A     -- usual list to CPS
  upList as L cons nil = L.foldr cons nil as

  -- List is a monad
  bind : ∀ {A B} → List A → (A → List B) → List B
  bind as f L cons nil = as _
    (λ a bs → f a L cons bs)
    nil

  pure : ∀ {A} → A → List A
  pure a L cons nil = cons a nil

  module GenericListFun where

    -- (α : A-Alg) → U A
    -- CPS A := (α : A-Alg) → U A

    -- goal: define functions in (CPS A → CPS B)

    -- ((α : A-Alg) → U α) → ((β : B-Alg) → U β)

    -- input:  (f : A-Alg → B-Alg) × (∀ α. U (f α) = U α)
    -- output: ((β : B-Alg) → U β) → ((α : A-Alg) → U α)

    -- F-alg: (A : Set) × (F A → A)
    --    fusingFoldr : (∀ A. (F A → A) → G A → A) → (∀ A. (F A → A) → A) → (∀ A. (G A → A) → A)
    --

    fusibleFoldr : ∀ {A B} → (∀ {L} → (B → L → L) → L → (A → L → L) × L) → List A → List B
    fusibleFoldr f as L cons nil = as L (f cons nil .₁) (f cons nil .₂)

    map' : ∀ {A B} → (A → B) → List A → List B
    map' f = fusibleFoldr λ cons nil → (λ a bs → cons (f a) bs) , nil

    filter' : ∀ {A} → (A → B.Bool) → List A → List A
    filter' f = fusibleFoldr (λ c n → (λ a l → B.if f a then c a l else l) , n)

    -- what about returning in comp types?
    -- List A → B → List C
    -- (∀ L. (A → L → L) → L → L) → B → (∀ L. (C → L → L) → L → L)
    -- (∀ L. (A → L → L) → L → L) → (∀ L. B → (C → L → L) → L → L)
    -- (

    -- A → ((α : ListAlg) → U α)

    -- (∀ X. G X → F (A → X)) → CPS F → CPS G

    -- A → (∀ X. (F X → X) → X)
    -- ∀ X. A → (F X → X) → X

    -- fuse : (∀ X. (G X → X) → F X → X) → Fix F → Fix G
    -- fuse : (∀ X. (G X → X) → F (A → X) → (A → X)) → Fix F → A → Fix G

    -- -- fusing with +1 arg
    -- fusibleFoldr1 : ∀ {A B C : Set}
    --              → (∀ {L} → (C → L → L) → L → (A → (B → L) → (B → L)) × (B → L))
    --              → List A → B → List C
    -- fusibleFoldr1 {A} {B} {C} f as b L cons nil =
    --   as (B → L) (f cons nil .₁) (f cons nil .₂) b

    -- take' : ∀ {A} → ℕ → List A → List A
    -- take' n as = fusibleFoldr1 (λ cons nil → (λ a k n → caseℕ n nil λ n → cons a (k n)) , λ _ → nil) as n

    -- fusibleFoldr11 : ∀ {A B C : Set}
    --              → (∀ {L} → (C → L → L) → L → (A → (B → L) → (B → L)) × (B → L))
    --              → List A → B → List C
    -- fusibleFoldr11 {A} {B} {C} f as b L cons nil =
    --   as (B → L) (f cons nil .₁) (f cons nil .₂) b

      -- fusibleFoldr1 (λ n cons nil → (λ a l → caseℕ n nil λ n → {!cons!}) , nil) as n

    -- TODO: - look at fusibleUnfold
    --       - what if we have multiple indexed/mutual so5rts

-- Streams
--------------------------------------------------------------------------------

-- TODO here

-- data Step a s = Stop | Yield a s

Step : Set → Set → Set
Step A S = (Step : Set)(stop : Step)(yield : A → S → Step) → Step

record Stream (A : Set) : Set where
  constructor stream
  field
    State : Set
    next  : State → Step A State
    seed  : State
open Stream public

map : ∀ {A B} → (A → B) → Stream A → Stream B
State (map f as) =
  State as

next  (map f as) s M stop yield =
  next as s _
    stop
    λ a s → yield (f a) s

seed (map f as) =
  seed as

open import Data.Sum

append : ∀ {A} → Stream A → Stream A → Stream A
State (append as as') =
  State as ⊎ State as'       -- does not compute on meta level (state *must* be runtime represented)
                             -- 1. Let the compiler optimize by call pattern spec
                             -- 2. Do a deeply embedded rep of state machines, write an optimizer/compiler for it on meta level
                             --    (Robinson & Lippmeier : Machine Fusion (with split optimization!))
next (append as as') (inj₁ s ) Step stop yield =
  next as s _
    (next as' (seed as') _
      stop
      λ a s' → yield a (inj₂ s'))
    λ a s → yield a (inj₁ s)
next (append as as') (inj₂ s') Step stop yield =
  next as' s' _
    stop
    λ a s' → yield a (inj₂ s')
seed (append as as') =
  inj₁ (seed as)

zip : ∀ {A B} → Stream A → Stream B → Stream (A × B)
State (zip as bs) = State as × State bs
next  (zip as bs) = {!!}   -- try to make two steps
seed  (zip as bs) = seed as , seed bs

filter : ∀ {A} → (A → B.Bool) → Stream A → Stream A
State (filter f as) = State as
next  (filter f as) s Step stop yield =
  next as s _
    stop
    λ a s → B.if f a then yield a s
                     else {!skip s!}  -- scanning forward is *tail recursive*
                     -- where find = tailrec forward (fine, because fusible w/o loss of efficiency)
                     -- in general, skipping over stream elements can be done in a loop

          -- scan forward until the next output yield (recursively)
          -- Rust iterators: exactly this solution
          --    using recursion inside stepping functions

seed  (filter f as) = seed as

  --
  --   Haskell stream fusion: use Skip streams
  --   data Step s a = Stop | Yield a s | Skip s
  --   codata SkipStream a = Stop | Yield a (SkipStream a) | Skip (SkipStream a)
  --   Stream (Maybe a) ~ SkipStream a

  -- Skip is unnecessary if we have enough fusion guarantees (staging)

-- binding streams?
--------------------------------------------------------------------------------

-- not available in GHC
-- Another paper: "Staged Stream Fusion to Completeness"

-- bind can be implemented without closures if you have sigma types

open import Data.Maybe

bind : ∀ {A B} → Stream A → (A → Stream B) → Stream B
State (bind as f) = State as × Maybe (∃ (State ∘ f))    -- (s, nothing) : computing next outer index
                                                        -- (s, just s') : computing next inner index
next  (bind as f) = {!!}
seed  (bind as f) = seed as , nothing
-- we don't have Σ at runtime in my lang....

-- Proposal for stream fusion
--------------------------------------------------------------------------------

-- Inductive encoding for lists + coinductive encoding for "affine" streams

-- streams:    unfold, iterate over data structures, ranges, enumeration, filter, take, drop, zip
-- inductive:  full feature set

-- assymmetric zip:    ChurchList A → Stream B → ChurchList (A × B)
--                     Stream B → ChurchList A → ChurchList (A × B)

-- pull : Stream A → ChurchList A

-- do x ← pull $ range 0 100
--    y ← pull $ zip (enumFrom 0) (toStream xs)
--    return $ x + y

-- no closures, no compiler magic required

-- example for Lippmeier magic:
--     xs : Stream Int
--     zip (map (+10) xs) xs      -- nonlinear xs usage (machine is duplicated)
--     map (λ x → (x + 10, x)) xs

-- automatic fusion?

-- map : ∀ {A B} → (A → B) → List A → List B
-- map f []     = []
-- map f (a:as) = f a : map f as
--           length (map f as)
--           case map f as of [] -> _; _ -> ...

{-
map : ∀ {A B} → (A → B) → List A → List B
map f as L c n = as L (λ a bs → c (f a) bs) n
-}

-- syntactic translation from runtime TT to 2LTT
--   whenever A  : VTy
--            Aᴹ : (A-Alg : MTy) × (U : A-Alg → CTy)
--     t  : Tm Γ (A : VTy)
--     tᴹ : Tm Γᴹ ((α : A-Alg) → U α)

--  trueᴹ  := church true
--  falseᴹ := ...
--  ifᴹ    := ..

-- interesting: usual CPS translation: *everything* incl function is CPS'd
--              wrap everything in Chruch Id functor
--              CId A = (Id : Set) → (A → Id) → Id

-- only for finite types
--   try to do it anyway: supercompilation

-- restrict "foldr" to only the definitions which are fusable?

-- we can't eliminate recursive results of folding

-- How to define fusibleFoldr?

max_stars_repo_name: AndrasKovacs/staged

max_issues_repo_name: AndrasKovacs/staged

max_forks_repo_name: AndrasKovacs/staged


text:
module Sets.IterativeSet where

import      Lvl
open import Logic
open import Type

module _ where
  private variable {ℓ ℓ₁ ℓ₂} : Lvl.Level

  -- A model of constructive set theory (CZF) by using W-types (iterative sets).
  -- The interpretation of Iset being a type of sets comes from the idea that the image of `elem` is a set of elements.
  record Iset : Type{Lvl.𝐒(ℓ)} where
    constructor set
    inductive
    pattern
    field
      {Index} : Type{ℓ}
      elem : Index → Iset{ℓ}
  open Iset

  Iset-index-induction : ∀{P : Iset{ℓ₁} → Stmt{ℓ₂}} → (∀{A : Iset{ℓ₁}} → (∀{i : Index(A)} → P(elem(A)(i))) → P(A)) → (∀{A : Iset{ℓ₁}} → P(A))
  Iset-index-induction {P = P} proof {set elem} = proof{_} \{i} → Iset-index-induction{P = P} proof {elem(i)}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --universe-polymorphism #-}
open import Categories.Category

module Categories.Object.IndexedProduct {o ℓ e} (C : Category o ℓ e) where

-- An indexed product is similar to a limit, but the diagram is from a Set
--  (irrelevant Setoid here) rather than a category, so there are no subobjects
--  involved.

open Category C
open Equiv

open import Level
open import Relation.Binary as Bi using ()
open import Categories.Support.Equivalence
import Categories.Object.Indexed as IObj
import Categories.Morphism.Indexed as IArrow

-- Borrowed from Dan Doel's definition of products
record IndexedProduct {c q} (B : Setoid c q) (As : IObj.Dust C B) : Set (o ⊔ ℓ ⊔ e ⊔ c ⊔ q) where
  module B = Setoid B
  open B using (_≈_)
  open Heterogeneous C
  open IObj C B
  open IArrow C B

  Cone : Obj → _
  Cone apex = apex ⇒∗ As

  cone-setoid : Obj → Setoid _ _
  cone-setoid apex = fan-setoid apex As

  _≜_ : ∀ {apex} → Bi.Rel (Cone apex) _
  _≜_ {apex} = Setoid._≈_ (cone-setoid apex)

  field
    ∏ : Obj
    π : Cone ∏

  -- convenience!
  π[_] : (x : B.Carrier) → (∏ ⇒ (As ! x))
  π[_] x = π ‼ x
  -- ↑ XXX for some reason it won't parse as π[ x ]
  .π-cong : ∀ {x y} → x ≈ y → (π[ x ] ∼ π[ y ])
  π-cong x≈y = cong₁ π x≈y

  π▹_ : ∀ {X} (f : X ⇒ ∏) → Cone X
  π▹_ f = _▹_ {Zs = As} π f

  field
    uncurry : ∀ {V} → Cone V → V ⇒ ∏
    -- XXX fs should be implicit but call sites can't infer it
    --   because of eta-driven irrelevant-field dropping
    .commute∗ : ∀ {V} (fs : Cone V) → (π▹ uncurry fs) ≜ fs
    .universal : ∀ {V} (fs : Cone V) {i : V ⇒ ∏}
               → (∀ {x} → π[ x ] ∘ i ≡ fs ‼ x) → uncurry fs ≡ i

  -- convenience?
  .commute : ∀ {V} (fs : Cone V) {x} → (π[ x ] ∘ uncurry fs) ≡ fs ‼ x
  commute fs {x} = ∼⇒≡ (commute∗ fs B.refl)

  .universal∗ : ∀ {V} (fs : Cone V) {i : V ⇒ ∏}
              → ((π▹ i) ≜ fs) → uncurry fs ≡ i
  universal∗ fs pf = universal fs (∼⇒≡ (pf B.refl))

  .g-η : ∀ {C} {f : C ⇒ ∏} → (uncurry (π▹ f) ≡ f)
  g-η {f = f} = universal (π▹ f) Equiv.refl

  .η : uncurry π ≡ Category.id C
  η = universal π identityʳ

  .uncurry-cong : ∀ {V} {fs gs : Cone V} → (∀ {x} → fs ‼ x ≡ gs ‼ x) → uncurry fs ≡ uncurry gs
  uncurry-cong {fs = fs} {gs} eq =
    universal fs (Equiv.trans (commute gs) (Equiv.sym eq))

  .uncurry-cong∗ : ∀ {V} {fs gs : Cone V} → fs ≜ gs → uncurry fs ≡ uncurry gs
  uncurry-cong∗ {V} {fs} {gs} eq = universal∗ fs
      (≜-trans {π▹ uncurry gs} {gs} {fs} (commute∗ gs) (≜-sym {fs} {gs} eq))
    where
    open Setoid (cone-setoid V) using ()
                                renaming (trans to ≜-trans; sym to ≜-sym)

  .uncurry∘ : ∀ {V W} (fs : Cone V) {q : W ⇒ V} → (uncurry fs) ∘ q ≡ uncurry (_▹_ {Zs = As} fs q)
  uncurry∘ fs {q} = Equiv.sym (universal (_▹_ {Zs = As} fs q) (Equiv.trans (Equiv.sym assoc) (∘-resp-≡ˡ (commute fs))))

{-
open import Categories.Morphisms

Commutative : ∀ {A B} → (p₁ : Product A B) (p₂ : Product B A) → _≅_ C (Product.A×B p₁) (Product.A×B p₂)
Commutative p₁ p₂ = record
  { f = ⟨ π₂ , π₁ ⟩′
  ; g = ⟨ π′₂ , π′₁ ⟩
  ; iso = record
    { isoˡ = isoˡ
    ; isoʳ = isoʳ
    }
  }
  where
  module p₁ = Product p₁
  module p₂ = Product p₂
  open Product p₁
  open Product p₂ renaming (A×B to B×A; π₁ to π′₁; π₂ to π′₂; ⟨_,_⟩ to ⟨_,_⟩′)

  idˡ : A×B ⇒ A×B
  idˡ = ⟨ π′₂ , π′₁ ⟩ ∘ ⟨ π₂ , π₁ ⟩′

  idʳ : B×A ⇒ B×A
  idʳ = ⟨ π₂ , π₁ ⟩′ ∘ ⟨ π′₂ , π′₁ ⟩

  .idˡ-commutes₁ : π₁ ∘ idˡ ≡ π₁
  idˡ-commutes₁ = begin
                    π₁ ∘ idˡ
                  ↑⟨ assoc ⟩
                    (π₁ ∘ ⟨ π′₂ , π′₁ ⟩) ∘ ⟨ π₂ , π₁ ⟩′
                  ↓⟨ ∘-resp-≡ˡ p₁.commute₁ ⟩
                    π′₂ ∘ ⟨ π₂ , π₁ ⟩′
                  ↓⟨ p₂.commute₂ ⟩
                    π₁
                  ∎
    where
    open HomReasoning

  .idˡ-commutes₂ : π₂ ∘ idˡ ≡ π₂
  idˡ-commutes₂ = begin
                    π₂ ∘ idˡ
                  ↑⟨ assoc ⟩
                    (π₂ ∘ ⟨ π′₂ , π′₁ ⟩) ∘ ⟨ π₂ , π₁ ⟩′
                  ↓⟨ ∘-resp-≡ˡ p₁.commute₂ ⟩
                    π′₁ ∘ ⟨ π₂ , π₁ ⟩′
                  ↓⟨ p₂.commute₁ ⟩
                    π₂
                  ∎
    where
    open HomReasoning

  .isoˡ : idˡ ≡ id
  isoˡ = begin
           idˡ
         ↑⟨ p₁.universal idˡ-commutes₁ idˡ-commutes₂ ⟩
           ⟨ π₁ , π₂ ⟩
         ↓⟨ p₁.η ⟩
           id
         ∎
    where
    open HomReasoning

  .idʳ-commutes₁ : π′₁ ∘ idʳ ≡ π′₁
  idʳ-commutes₁ = begin
                    π′₁ ∘ idʳ
                  ↑⟨ assoc ⟩
                    (π′₁ ∘ ⟨ π₂ , π₁ ⟩′) ∘ ⟨ π′₂ , π′₁ ⟩
                  ↓⟨ ∘-resp-≡ˡ p₂.commute₁ ⟩
                    π₂ ∘ ⟨ π′₂ , π′₁ ⟩
                  ↓⟨ p₁.commute₂ ⟩
                    π′₁
                  ∎
    where
    open HomReasoning

  .idʳ-commutes₂ : π′₂ ∘ idʳ ≡ π′₂
  idʳ-commutes₂ = begin
                    π′₂ ∘ idʳ
                  ↑⟨ assoc ⟩
                    (π′₂ ∘ ⟨ π₂ , π₁ ⟩′) ∘ ⟨ π′₂ , π′₁ ⟩
                  ↓⟨ ∘-resp-≡ˡ p₂.commute₂ ⟩
                    π₁ ∘ ⟨ π′₂ , π′₁ ⟩
                  ↓⟨ p₁.commute₁ ⟩
                    π′₂
                  ∎
    where
    open HomReasoning

  .isoʳ : idʳ ≡ id
  isoʳ = begin
           idʳ
         ↑⟨ p₂.universal idʳ-commutes₁ idʳ-commutes₂ ⟩
           ⟨ π′₁ , π′₂ ⟩′
         ↓⟨ p₂.η ⟩
           id
         ∎
    where
    open HomReasoning

Associative : ∀ {X Y Z} (p₁ : Product X Y) (p₂ : Product Y Z) (p₃ : Product X (Product.A×B p₂)) (p₄ : Product (Product.A×B p₁) Z) → _≅_ C (Product.A×B p₃) (Product.A×B p₄)
Associative p₁ p₂ p₃ p₄ = record
  { f = f
  ; g = g
  ; iso = record
    { isoˡ = isoˡ
    ; isoʳ = isoʳ
    }
  }
  where
  module p₁ = Product p₁
  module p₂ = Product p₂
  module p₃ = Product p₃
  module p₄ = Product p₄
  open Product p₁ hiding (π₁; π₂) renaming (⟨_,_⟩ to ⟨_,_⟩p₁)
  open Product p₂ hiding (π₁; π₂) renaming (A×B to B×C; ⟨_,_⟩ to ⟨_,_⟩p₂)
  open Product p₃ renaming (A×B to A×[B×C])
  open Product p₄ renaming (A×B to [A×B]×C; π₁ to π′₁; π₂ to π′₂; ⟨_,_⟩ to ⟨_,_⟩′)

  f : A×[B×C] ⇒ [A×B]×C
  f = ⟨ ⟨ π₁ , p₂.π₁ ∘ π₂ ⟩p₁ , p₂.π₂ ∘ π₂ ⟩′

  g : [A×B]×C ⇒ A×[B×C]
  g = ⟨ p₁.π₁ ∘ π′₁ , ⟨ p₁.π₂ ∘ π′₁ , π′₂ ⟩p₂ ⟩

  idˡ : A×[B×C] ⇒ A×[B×C]
  idˡ = g ∘ f

  idʳ : [A×B]×C ⇒ [A×B]×C
  idʳ = f ∘ g

  .cmˡ₁ : π₁ ∘ idˡ ≡ π₁
  cmˡ₁ = begin
           π₁ ∘ idˡ
         ↑⟨ assoc ⟩
           (π₁ ∘ g) ∘ f
         ↓⟨ ∘-resp-≡ˡ p₃.commute₁ ⟩
           (p₁.π₁ ∘ π′₁) ∘ f
         ↓⟨ assoc ⟩
           p₁.π₁ ∘ (π′₁ ∘ f)
         ↓⟨ ∘-resp-≡ʳ p₄.commute₁ ⟩
           p₁.π₁ ∘ ⟨ p₃.π₁ , p₂.π₁ ∘ p₃.π₂ ⟩p₁
         ↓⟨ p₁.commute₁ ⟩
           p₃.π₁
         ∎
    where
    open HomReasoning

  .cmˡ₂₁ : p₂.π₁ ∘ (⟨ p₁.π₂ ∘ p₄.π₁ , p₄.π₂ ⟩p₂ ∘ f) ≡ p₂.π₁ ∘ p₃.π₂
  cmˡ₂₁ = begin
           p₂.π₁ ∘ (⟨ p₁.π₂ ∘ p₄.π₁ , p₄.π₂ ⟩p₂ ∘ f)
         ↑⟨ assoc ⟩
           (p₂.π₁ ∘ ⟨ p₁.π₂ ∘ p₄.π₁ , p₄.π₂ ⟩p₂) ∘ f
         ↓⟨ ∘-resp-≡ˡ p₂.commute₁ ⟩
           (p₁.π₂ ∘ p₄.π₁) ∘ f
         ↓⟨ assoc ⟩
           p₁.π₂ ∘ (p₄.π₁ ∘ f)
         ↓⟨ ∘-resp-≡ʳ p₄.commute₁ ⟩
           p₁.π₂ ∘ ⟨ p₃.π₁ , p₂.π₁ ∘ p₃.π₂ ⟩p₁
         ↓⟨ p₁.commute₂ ⟩
           p₂.π₁ ∘ p₃.π₂
         ∎
    where
      open HomReasoning

  .cmˡ₂₂ : p₂.π₂ ∘ (⟨ p₁.π₂ ∘ p₄.π₁ , p₄.π₂ ⟩p₂ ∘ f) ≡ p₂.π₂ ∘ p₃.π₂
  cmˡ₂₂ = begin
           p₂.π₂ ∘ (⟨ p₁.π₂ ∘ p₄.π₁ , p₄.π₂ ⟩p₂ ∘ f)
         ↑⟨ assoc ⟩
           (p₂.π₂ ∘ ⟨ p₁.π₂ ∘ p₄.π₁ , p₄.π₂ ⟩p₂) ∘ f
         ↓⟨ ∘-resp-≡ˡ p₂.commute₂ ⟩
           p₄.π₂ ∘ f
         ↓⟨ p₄.commute₂ ⟩
           p₂.π₂ ∘ p₃.π₂
         ∎
    where
      open HomReasoning

  .cmˡ₂ : π₂ ∘ idˡ ≡ π₂
  cmˡ₂ = begin
           π₂ ∘ idˡ
         ↑⟨ assoc ⟩
           (π₂ ∘ g) ∘ f
         ↓⟨ ∘-resp-≡ˡ p₃.commute₂ ⟩
           ⟨ p₁.π₂ ∘ p₄.π₁ , p₄.π₂ ⟩p₂ ∘ f
         ↑⟨ p₂.universal cmˡ₂₁ cmˡ₂₂ ⟩
           ⟨ p₂.π₁ ∘ p₃.π₂ , p₂.π₂ ∘ p₃.π₂ ⟩p₂
         ↓⟨ p₂.g-η ⟩
           p₃.π₂
         ∎
    where
    open HomReasoning

  .isoˡ : idˡ ≡ id
  isoˡ = begin
           idˡ
         ↑⟨ p₃.universal cmˡ₁ cmˡ₂ ⟩
           ⟨ π₁ , π₂ ⟩
         ↓⟨ p₃.η ⟩
           id
         ∎
    where
    open HomReasoning

  .cmʳ₁₁ : p₁.π₁ ∘ (⟨ p₃.π₁ , p₂.π₁ ∘ p₃.π₂ ⟩p₁ ∘ g) ≡ p₁.π₁ ∘ p₄.π₁
  cmʳ₁₁ = begin
            p₁.π₁ ∘ (⟨ p₃.π₁ , p₂.π₁ ∘ p₃.π₂ ⟩p₁ ∘ g)
          ↑⟨ assoc ⟩
            (p₁.π₁ ∘ ⟨ p₃.π₁ , p₂.π₁ ∘ p₃.π₂ ⟩p₁) ∘ g
          ↓⟨ ∘-resp-≡ˡ p₁.commute₁ ⟩
            p₃.π₁ ∘ g
          ↓⟨ p₃.commute₁ ⟩
            p₁.π₁ ∘ p₄.π₁
          ∎
    where
    open HomReasoning

  .cmʳ₁₂ : p₁.π₂ ∘ (⟨ p₃.π₁ , p₂.π₁ ∘ p₃.π₂ ⟩p₁ ∘ g) ≡ p₁.π₂ ∘ p₄.π₁
  cmʳ₁₂ = begin
            p₁.π₂ ∘ (⟨ p₃.π₁ , p₂.π₁ ∘ p₃.π₂ ⟩p₁ ∘ g)
          ↑⟨ assoc ⟩
            (p₁.π₂ ∘ ⟨ p₃.π₁ , p₂.π₁ ∘ p₃.π₂ ⟩p₁) ∘ g
          ↓⟨ ∘-resp-≡ˡ p₁.commute₂ ⟩
            (p₂.π₁ ∘ p₃.π₂) ∘ g
          ↓⟨ assoc ⟩
            p₂.π₁ ∘ (p₃.π₂ ∘ g)
          ↓⟨ ∘-resp-≡ʳ p₃.commute₂ ⟩
            p₂.π₁ ∘ ⟨ p₁.π₂ ∘ p₄.π₁ , p₄.π₂ ⟩p₂
          ↓⟨ p₂.commute₁ ⟩
            p₁.π₂ ∘ p₄.π₁
          ∎
    where
    open HomReasoning

  .cmʳ₁ : π′₁ ∘ idʳ ≡ π′₁
  cmʳ₁ = begin
           π′₁ ∘ idʳ
         ↑⟨ assoc ⟩
           (π′₁ ∘ f) ∘ g
         ↓⟨ ∘-resp-≡ˡ p₄.commute₁ ⟩
           ⟨ π₁ , p₂.π₁ ∘ p₃.π₂ ⟩p₁ ∘ g
         ↑⟨ p₁.universal cmʳ₁₁ cmʳ₁₂ ⟩
           ⟨ p₁.π₁ ∘ p₄.π₁ , p₁.π₂ ∘ p₄.π₁ ⟩p₁
         ↓⟨ p₁.g-η ⟩
           π′₁
         ∎
    where
    open HomReasoning

  .cmʳ₂ : π′₂ ∘ idʳ ≡ π′₂
  cmʳ₂ = begin
           π′₂ ∘ idʳ
         ↑⟨ assoc ⟩
           (π′₂ ∘ f) ∘ g
         ↓⟨ ∘-resp-≡ˡ p₄.commute₂ ⟩
           (p₂.π₂ ∘ p₃.π₂) ∘ g
         ↓⟨ assoc ⟩
           p₂.π₂ ∘ (p₃.π₂ ∘ g)
         ↓⟨ ∘-resp-≡ʳ p₃.commute₂ ⟩
           p₂.π₂ ∘ ⟨ p₁.π₂ ∘ p₄.π₁ , p₄.π₂ ⟩p₂
         ↓⟨ p₂.commute₂ ⟩
           p₄.π₂
         ∎
    where
    open HomReasoning

  .isoʳ : idʳ ≡ id
  isoʳ = begin
           idʳ
         ↑⟨ p₄.universal cmʳ₁ cmʳ₂ ⟩
           ⟨ π′₁ , π′₂ ⟩′
         ↓⟨ p₄.η ⟩
           id
         ∎
    where
    open HomReasoning
-}

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --allow-unsolved-metas #-}
module LiteralSequent where

open import Sequent
open import IsLiteralSequent

record LiteralSequent : Set
 where
  constructor ⟨_⟩
  field
    {sequent} : Sequent
    isLiteralSequent : IsLiteralSequent sequent

open LiteralSequent public

open import OscarPrelude

private
  module _ where

    pattern ⟪_,_⟫ h s = ⟨_⟩ {h} s
    pattern ⟪_⟫ h = (⟨_⟩ {h} _)

instance EqLiteralSequent : Eq LiteralSequent
Eq._==_ EqLiteralSequent ⟪ Φ₁ ⟫ ⟪ Φ₂ ⟫   with Φ₁ ≟ Φ₂
Eq._==_ EqLiteralSequent ⟨ !Φ₁ ⟩ ⟨ !Φ₂ ⟩ | yes refl with !Φ₁ ≟ !Φ₂
Eq._==_ EqLiteralSequent _ _             | yes refl | yes refl = yes refl
Eq._==_ EqLiteralSequent ⟨ Φ₁ ⟩ ⟨ Φ₂ ⟩   | yes refl | no !Φ₁≢!Φ₂ = no λ {refl → !Φ₁≢!Φ₂ refl}
Eq._==_ EqLiteralSequent ⟨ Φ₁ ⟩ ⟨ Φ₂ ⟩   | no Φ₁≢Φ₂ = no λ {refl → Φ₁≢Φ₂ refl}

module _ where

  open import HasNegation
  open import IsLiteralFormula

  instance HasNegationLiteralSequent : HasNegation LiteralSequent
  HasNegation.~ HasNegationLiteralSequent ⟨ atomic 𝑃 τs ╱ φˢs ⟩ = ⟨ logical 𝑃 τs ╱ φˢs ⟩
  HasNegation.~ HasNegationLiteralSequent ⟨ logical 𝑃 τs ╱ φˢs ⟩ = ⟨ atomic 𝑃 τs ╱ φˢs ⟩

open import 𝓐ssertion

instance 𝓐ssertionLiteralSequent : 𝓐ssertion LiteralSequent
𝓐ssertionLiteralSequent = record {}

open import HasSatisfaction

instance HasSatisfactionLiteralSequent : HasSatisfaction LiteralSequent
HasSatisfaction._⊨_ HasSatisfactionLiteralSequent I Φ = I ⊨ sequent Φ

open import HasDecidableValidation

instance HasDecidableValidationLiteralSequent : HasDecidableValidation LiteralSequent
HasDecidableValidationLiteralSequent = {!!}


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

module hott.truncation where

open import hott.truncation.core public
open import hott.truncation.const public
open import hott.truncation.equality public
open import hott.truncation.elim public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module Type.Size.Proofs where

import      Lvl
open import Data
open import Data.Proofs
open import Functional
open import Function.Equals
open import Function.Inverseᵣ
open import Function.Inverse
open import Function.Proofs
open import Logic
open import Logic.IntroInstances
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Function.Domain.Proofs
open import Structure.Relator.Equivalence
open import Structure.Relator.Ordering
open import Structure.Relator.Properties
open import Type
import      Type.Size

private variable ℓ ℓ₁ ℓ₂ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ : Lvl.Level
private variable T A B C : Type{ℓ}

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  open Type.Size

  [≼]-maximum : (_≼_ T (T → T) ⦃ [⊜]-equiv ⦄)
  [≼]-maximum = [∃]-intro(const) ⦃ intro(proof) ⦄ where
    proof : ∀{x y} → (const(x) ⊜ const(y)) → (x ≡ y)
    proof{x}{y} (intro fneq) = fneq{x}

  [≍]-reflexivity-raw : (T ≍ T)
  [≍]-reflexivity-raw = [∃]-intro(id) ⦃ id-bijective ⦄

  [≼]-reflexivity-raw : (T ≼ T)
  [≼]-reflexivity-raw = [∃]-intro(id) ⦃ id-injective ⦄

  [≽]-reflexivity-raw : (T ≽ T)
  [≽]-reflexivity-raw = [∃]-intro(id) ⦃ id-surjective ⦄

  [≼]-minimum-raw : ⦃ equiv-empty : Equiv{ℓₑ₁}(Empty{ℓ}) ⦄ → (_≼_ Empty ⦃ equiv-empty ⦄ T)
  [≼]-minimum-raw = [∃]-intro(empty) ⦃ empty-injective ⦄

    -- TODO: Impossible because there are no functions of type (T → ⊥)?
    -- instance
    --   [≽]-minimum : Weak.Properties.Maximum(_≽_ {ℓ})(Empty)
    --   Weak.Properties.Maximum.proof([≽]-minimum) {T} {}

module _ ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ where
  open Type.Size

  [≍]-to-[≼] : (A ≍ B) → (A ≼ B)
  [≍]-to-[≼] ([∃]-intro(f) ⦃ f-bijective ⦄) =
    ([∃]-intro(f) ⦃ bijective-to-injective(f) ⦃ f-bijective ⦄ ⦄)

  [≍]-to-[≽] : (A ≍ B) → (A ≽ B)
  [≍]-to-[≽] ([∃]-intro(f) ⦃ f-bijective ⦄) =
    ([∃]-intro(f) ⦃ bijective-to-surjective(f) ⦃ f-bijective ⦄ ⦄)

  [≽]-to-[≼] : (ab@([∃]-intro f) : (A ≽ B)) → ⦃ func : Function(f) ⦄ ⦃ inv-func : Function(invᵣ-surjective f) ⦄ → (B ≼ A)
  [≽]-to-[≼] ([∃]-intro(f) ⦃ f-surjective ⦄) ⦃ inv-func ⦄ = [∃]-intro(invᵣ f ⦃ surjective-to-invertibleᵣ ⦄) ⦃ inverseᵣ-injective{f = f} ⦃ [∧]-elimᵣ([∃]-proof surjective-to-invertibleᵣ) ⦄ ⦄

  {-[≼]-to-[≽] : (A ≼ B) → (B ≽ A)
  [≼]-to-[≽] ([∃]-intro(f) ⦃ f-injective ⦄) =
    {![∃]-intro()!}
  -}

  [≍]-symmetry-raw : (ab@([∃]-intro f) : (A ≍ B)) → ⦃ func : Function(f) ⦄ → (B ≍ A)
  [≍]-symmetry-raw ([∃]-intro(f) ⦃ f-bijective ⦄)
    = [∃]-intro(inv f ⦃ bijective-to-invertible ⦄) ⦃ inv-bijective{f = f} ⦃ inver = bijective-to-invertible ⦄ ⦄

module _ ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ ⦃ equiv-C : Equiv{ℓₑ₃}(C) ⦄ where
  open Type.Size

  [≍]-transitivity-raw : (ab@([∃]-intro f) : (A ≍ B)) ⦃ func-f : Function(f) ⦄ → (bc@([∃]-intro g) : (B ≍ C)) ⦃ func-g : Function(g) ⦄ → (A ≍ C)
  [≍]-transitivity-raw ([∃]-intro(f) ⦃ f-bijective ⦄) ([∃]-intro(g) ⦃ g-bijective ⦄)
    = [∃]-intro(g ∘ f) ⦃ [∘]-bijective {f = g} {g = f} ⦃ g-bijective ⦄ ⦃ f-bijective ⦄ ⦄

  [≼]-transitivity-raw : (A ≼ B) → (B ≼ C) → (A ≼ C)
  [≼]-transitivity-raw ([∃]-intro(f) ⦃ f-injective ⦄) ([∃]-intro(g) ⦃ g-injective ⦄)
    = [∃]-intro(g ∘ f) ⦃ [∘]-injective {f = g}{g = f} ⦃ g-injective ⦄ ⦃ f-injective ⦄ ⦄

  [≽]-transitivity-raw : (A ≽ B) → (([∃]-intro g) : (B ≽ C)) ⦃ func-g : Function(g) ⦄ → (A ≽ C)
  [≽]-transitivity-raw ([∃]-intro(f) ⦃ f-surjective ⦄) ([∃]-intro(g) ⦃ g-surjective ⦄)
    = [∃]-intro(g ∘ f) ⦃ [∘]-surjective {f = g} {g = f} ⦃ g-surjective ⦄ ⦃ f-surjective ⦄ ⦄

module _ where
  open import Relator.Equals renaming (_≡_ to _≡ₑ_)
  open import Relator.Equals.Proofs

  private
    _≍_ : ∀{ℓ₁ ℓ₂} → (A : Type{ℓ₁}) → (B : Type{ℓ₂}) → Stmt
    _≍_ A B = Type.Size._≍_ A B

    _≼_ : ∀{ℓ₁ ℓ₂} → (A : Type{ℓ₁}) → (B : Type{ℓ₂}) → Stmt
    _≼_ A B = Type.Size._≼_ A B

    _≽_ : ∀{ℓ₁ ℓ₂} → (A : Type{ℓ₁}) → (B : Type{ℓ₂}) → Stmt
    _≽_ A B = Type.Size._≽_ A B

    _≭_ : ∀{ℓ₁ ℓ₂} → (A : Type{ℓ₁}) → (B : Type{ℓ₂}) → Stmt
    _≭_ A B = Type.Size._≭_ A B

    _≺_ : ∀{ℓ₁ ℓ₂} → (A : Type{ℓ₁}) → (B : Type{ℓ₂}) → Stmt
    _≺_ A B = Type.Size._≺_ A B

    _≻_ : ∀{ℓ₁ ℓ₂} → (A : Type{ℓ₁}) → (B : Type{ℓ₂}) → Stmt
    _≻_ A B = Type.Size._≻_ A B

  module _ {ℓ} where
    instance
      [≍]-reflexivity : Reflexivity(_≍_ {ℓ})
      [≍]-reflexivity = intro [≍]-reflexivity-raw

    instance
      [≍]-symmetry : Symmetry(_≍_ {ℓ})
      [≍]-symmetry = intro(f ↦ [≍]-symmetry-raw f)

    instance
      [≍]-transitivity : Transitivity(_≍_ {ℓ})
      [≍]-transitivity = intro(f ↦ g ↦ [≍]-transitivity-raw f g)

    instance
      [≍]-equivalence : Equivalence(_≍_ {ℓ})
      [≍]-equivalence = intro

    instance
      [≼]-reflexivity : Reflexivity(_≼_ {ℓ})
      [≼]-reflexivity = intro [≼]-reflexivity-raw

    instance
      [≼]-transitivity : Transitivity(_≼_ {ℓ})
      [≼]-transitivity = intro [≼]-transitivity-raw

    instance
      [≽]-reflexivity : Reflexivity(_≽_ {ℓ})
      [≽]-reflexivity = intro [≽]-reflexivity-raw

    instance
      [≽]-transitivity : Transitivity(_≽_ {ℓ})
      [≽]-transitivity = intro(p ↦ q ↦ [≽]-transitivity-raw p q)

    instance
      [≼]-minimum : Weak.Properties.LE.Minimum(_≼_ {ℓ})(Empty)
      Weak.Properties.Extremumₗ.proof [≼]-minimum = [≼]-minimum-raw

    -- TODO: Impossible because there are no functions of type (T → ⊥)?
    -- instance
    --   [≽]-minimum : Weak.Properties.Maximum(_≽_ {ℓ})(Empty)
    --   Weak.Properties.Maximum.proof([≽]-minimum) {T} {}

  -- TODO: Remove this and the similar one in the other module. A more general variant is defined in Relator.Equals.Proofs
  module _ {A : Type{ℓ}} {B : Type{ℓ}} where
    [≡]-to-[≍] : (A ≡ₑ B) → (A ≍ B)
    [≡]-to-[≍] [≡]-intro = reflexivity(_≍_)


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

module common where
open import Agda.Primitive public
  using    (Level; _⊔_; lzero; lsuc)

infixl 1 _,_
infixl 1 _≡_
infixr 2 _∧_
infixr 2 _×_
infixl 2 _+_

data bool : Set where
  true : bool
  false : bool

_∧_ : bool → bool → bool
true ∧ true = true
true ∧ false = false
false ∧ true = false
false ∧ false = false

record Σ {ℓ ℓ′} (A : Set ℓ) (P : A → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : P proj₁

_×_ : ∀ {ℓ ℓ′} (A : Set ℓ) (B : Set ℓ′) → Set (ℓ ⊔ ℓ′)
A × B = Σ A (λ _ → B)

if_then_else_ : ∀ {ℓ} {A : Set ℓ} → (b : bool) → A → A → A
if true then t else f = t
if false then t else f = f

data Lifted {a b} (A : Set a) : Set (b ⊔ a) where
  lift : A → Lifted A

lower : ∀ {a b A} → Lifted {a} {b} A → A
lower (lift x) = x

data Maybe {ℓ : Level} (A : Set ℓ) : Set ℓ where
  just    : (x : A) → Maybe A
  nothing : Maybe A

Maybe-elim : ∀ {ℓ ℓ′} {A : Set ℓ} (P : Maybe A → Set ℓ′)
  → ((x : A) → P (just x))
  → P nothing
  → (x : Maybe A)
  → P x
Maybe-elim P Pjust Pnothing (just x) = Pjust x
Maybe-elim P Pjust Pnothing nothing = Pnothing

option-map : ∀ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′}
  → (A → B)
  → Maybe A → Maybe B
option-map f (just x) = just (f x)
option-map f nothing = nothing

option-bind : ∀ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′}
  → Maybe A
  → (A → Maybe B)
  → Maybe B
option-bind (just x) f = option-map (λ x₁ → x₁) (f x)
option-bind nothing f = nothing

data ⊥ {ℓ : Level} : Set ℓ where

⊥-elim : {ℓ ℓ′ : Level} → ⊥ {ℓ} → {A : Set ℓ′} → A
⊥-elim ()

¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ T = T → ⊥ {lzero}

record ⊤ {ℓ : Level} : Set ℓ where
  constructor tt

infixr 1 _⊎_

data _⊎_ (A : Set) (B : Set) : Set where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl : x ≡ x

_≢_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
x ≢ y = x ≡ y → ⊥ {lzero}

dec-eq-on : {A : Set} → (x : A) → (y : A) → Set
dec-eq-on x y = (x ≡ y) ⊎ (x ≢ y)

dec-eq : Set → Set
dec-eq A = (x : A) → (y : A) → dec-eq-on x y

sym : {A : Set} → {x : A} → {y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : {A : Set} → {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

transport : ∀ {A : Set} {x : A} {y : A} → (P : A → Set) → x ≡ y → P x → P y
transport P refl v = v

transport2 : ∀ {A : Set} {B : A → Set} {x x' : A} {y : B x} {y' : B x'} → (P : (x : A) → B x → Set) → (p : x ≡ x') → transport B p y ≡ y' → P x y → P x' y'
transport2 P refl = transport (P _)

transport3 : ∀ {A : Set} {B : A → Set} {C : (x : A) → (y : B x) → Set} {x x' : A} {y : B x} {y' : B x'} {z : C x y} {z' : C x' y'} → (P : (x : A) → (y : B x) → C x y → Set) → (p : x ≡ x') → (q : transport B p y ≡ y') → transport2 C p q z ≡ z' → P x y z → P x' y' z'
transport3 P refl = transport2 (P _)

transport4 : ∀ {A : Set} {B : A → Set} {C : (x : A) → (y : B x) → Set} {D : (x : A) → (y : B x) → (z : C x y) → Set} {x x' : A} {y : B x} {y' : B x'} {z : C x y} {z' : C x' y'} {w : D x y z} {w' : D x' y' z'} → (P : (x : A) → (y : B x) → (z : C x y) → D x y z → Set) → (p : x ≡ x') → (q : transport B p y ≡ y') → (r : transport2 C p q z ≡ z') → transport3 D p q r w ≡ w' → P x y z w → P x' y' z' w'
transport4 P refl = transport3 (P _)

Maybe-code : {A : Set} → Maybe A → Maybe A → Set
Maybe-code (just x) (just x₁) = x ≡ x₁
Maybe-code (just x) nothing = ⊥
Maybe-code nothing (just x) = ⊥
Maybe-code nothing nothing = ⊤

Maybe-encode : ∀ {A} {x y : Maybe A} → x ≡ y → Maybe-code x y
Maybe-encode {A} {just x} refl = refl
Maybe-encode {A} {nothing} refl = tt

Maybe-decode : ∀ {A} {x y : Maybe A} → Maybe-code x y → x ≡ y
Maybe-decode {A} {just .x₁} {just x₁} refl = refl
Maybe-decode {A} {just x} {nothing} ()
Maybe-decode {A} {nothing} {just x} ()
Maybe-decode {A} {nothing} {nothing} tt = refl

Maybe-deencode : ∀ {A} {x y : Maybe A} {p : x ≡ y} → Maybe-decode (Maybe-encode p) ≡ p
Maybe-deencode {A} {just x} {.(just x)} {refl} = refl
Maybe-deencode {A} {nothing} {.nothing} {refl} = refl

Maybe-endecode : ∀ {A} {x y : Maybe A} (p : Maybe-code x y) → Maybe-encode {A} {x} {y} (Maybe-decode p) ≡ p
Maybe-endecode {A} {just .x'} {just x'} refl = refl
Maybe-endecode {A} {just x} {nothing} ()
Maybe-endecode {A} {nothing} {just x} ()
Maybe-endecode {A} {nothing} {nothing} tt = refl

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ #-}

max : ℕ → ℕ → ℕ
max 0 y = y
max x 0 = x
max (suc x) (suc y) = suc (max x y)

_+_ : ℕ → ℕ → ℕ
0 + b = b
suc a + b = suc (a + b)

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


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

module TypeEquivEquiv where

open import Equiv
  using (refl∼; sym∼; trans∼; sym≃;
    _⊎≃_; id≃; _≃_; _●_; _×≃_; qinv; gg;
    β⊎₁; β⊎₂; β₁; β₂; cong∘l; cong∘r; cong₂∘; β×₁; β×₂)
open import TypeEquiv
  using (unite₊equiv; uniti₊equiv; unite₊′equiv; uniti₊′equiv;
    assocr₊equiv; assocl₊equiv; swap₊equiv;
    unite⋆equiv; uniti⋆equiv; unite⋆′equiv; uniti⋆′equiv;
    assocr⋆equiv; assocl⋆equiv; swap⋆equiv;
    distlequiv; factorlequiv; distequiv; factorequiv;
    distzrequiv; factorzrequiv; distzequiv; factorzequiv)
open import EquivEquiv

open import Data.Empty using (⊥)
open import Data.Unit using (⊤)
open import Data.Sum using (_⊎_)
open import Data.Product using (_,_; _×_; proj₁)
open import Function using (_∘_)

open import Data.Sum.Properties2
  using (id⊎id∼id; ⊎∘∼∘⊎; _⊎∼_;
    unite₊-coh; uniti₊-coh; unite₊′-coh; uniti₊′-coh;
    assocr₊-wf; assocl₊-wf;
    triangle⊎-left; triangle⊎-right;
    pentagon⊎-right; pentagon⊎-left;
    swap₊-coh; unite₊-swap-coh-left; unite₊-swap-coh-right;
    hexagon⊎-right; hexagon⊎-left)

open import Data.Product.Properties2
  using (id×id∼id; ×∘∼∘×; _×∼_;
    unite⋆-coh; uniti⋆-coh; unite⋆′-coh; uniti⋆′-coh;
    assocr⋆-wf; assocl⋆-wf;
    triangle×-left; triangle×-right;
    pentagon×-right; pentagon×-left;
    swap⋆-coh;  unite⋆-swap-coh-left; unite⋆-swap-coh-right;
    hexagon×-right; hexagon×-left)

open import Data.SumProd.Properties -- TODO: list them

-- some local abbreviations to make life nicer
infixr 10 _⊙_

private
  _⊙_ = trans∼
  !_ = sym∼

-- we define all the equivalences-between-equivalences that hold
-- between type equivalences.

-- TODO: quite possibly, everything here should be abstract, as
-- it shouldn't be useful to look into the structure of the proofs,
-- but just that they do, indeed exist.  That and the proofs are in
-- fact rather boring, consisting of explicit sequences of
-- unveil --> delegate to lower level -> veil
-- operations.
----
-- equivalences for the ⊎ structure

[id,id]≋id : ∀ {A B : Set} → id≃ {A = A} ⊎≃ id≃ {A = B} ≋ id≃
[id,id]≋id = eq (β⊎₁ ⊙ id⊎id∼id) (β⊎₂ ⊙ id⊎id∼id)

-- ● and ⊎≃ commute.

⊎●≋●⊎ : {A B C D E F : Set} →
  {f : A ≃ C} {g : B ≃ D} {h : C ≃ E} {i : D ≃ F} →
  (h ● f) ⊎≃ (i ● g) ≋ (h ⊎≃ i) ● (f ⊎≃ g)
⊎●≋●⊎ =
  eq (β⊎₁ ⊙ β₁ ⊎∼ β₁ ⊙ ⊎∘∼∘⊎ ⊙ ! cong₂∘ β⊎₁ β⊎₁ ⊙ ! β₁)
     (β⊎₂ ⊙ β₂ ⊎∼ β₂ ⊙ ⊎∘∼∘⊎ ⊙ ! cong₂∘ β⊎₂ β⊎₂ ⊙ ! β₂)

-- ≋ has, predictably, an additive structure as well

_⊎≋_ : {A B C D : Set} {f h : A ≃ B} {g i : C ≃ D} → f ≋ h → g ≋ i →
  f ⊎≃ g ≋ h ⊎≃ i
f≋h ⊎≋ g≋i =
  eq (β⊎₁ ⊙ (f≡ f≋h) ⊎∼ (f≡ g≋i) ⊙ ! β⊎₁)
     (β⊎₂ ⊙ (g≡ f≋h) ⊎∼ (g≡ g≋i) ⊙ ! β⊎₂)
  where open _≋_

-- strangely, this is not needed by Rig Category.  However, it
-- belongs to the structure of a Monoidal Groupoid (I think!  Should
-- be checked), and is quite useful on its own.

sym≃-distrib⊎ : ∀ {A B C D : Set} {f : A ≃ B} {g : C ≃ D} →
  sym≃ (f ⊎≃ g) ≋ sym≃ f ⊎≃ sym≃ g
sym≃-distrib⊎ = -- note how the proof mixes ₁ and ₂ !
  eq (β⊎₂ ⊙ ! β⊎₁) (β⊎₁ ⊙ ! β⊎₂)

-- Use '-nat' to signify that operation induces a
-- natural transformation, and that the induced operation
-- satisfies the naturality condition thus encoded

unite₊-nat : ∀ {A B} {f : A ≃ B} {g : ⊥ ≃ ⊥} →
  unite₊equiv ● (g ⊎≃ f) ≋ f ● unite₊equiv
unite₊-nat {g = g} =
  eq (β₁ ⊙ cong∘l (proj₁ unite₊equiv) β⊎₁ ⊙ unite₊-coh ⊙ ! β₁)
       (β₂ ⊙ cong∘r (gg unite₊equiv) β⊎₂ ⊙ uniti₊-coh {g = gg g} ⊙ ! β₂)

uniti₊-nat : ∀ {A B} {f : A ≃ B} {g : ⊥ ≃ ⊥} →
  uniti₊equiv ● f ≋ (g ⊎≃ f) ● uniti₊equiv
uniti₊-nat {g = g} =
  eq (β₁ ⊙ ! uniti₊-coh {g = proj₁ g} ⊙ ! cong∘r (proj₁ uniti₊equiv) β⊎₁ ⊙ ! β₁)
       (β₂ ⊙ ! unite₊-coh ⊙ ! cong∘l (gg uniti₊equiv) β⊎₂ ⊙ ! β₂)

unite₊′-nat : ∀ {A B} {f : A ≃ B} {g : ⊥ ≃ ⊥} →
  unite₊′equiv ● (f ⊎≃ g) ≋ f ● unite₊′equiv
unite₊′-nat {g = g} =
  eq (β₁ ⊙ cong∘l (proj₁ unite₊′equiv) β⊎₁ ⊙ unite₊′-coh ⊙ ! β₁)
     (β₂ ⊙ cong∘r (gg unite₊′equiv) β⊎₂ ⊙ uniti₊′-coh {g = gg g} ⊙ ! β₂)

uniti₊′-nat : ∀ {A B} {f : A ≃ B} {g : ⊥ ≃ ⊥} →
  uniti₊′equiv ● f ≋ (f ⊎≃ g) ● uniti₊′equiv
uniti₊′-nat {g = g} =
  eq (β₁ ⊙ ! uniti₊′-coh {g = proj₁ g} ⊙ ! cong∘r (proj₁ uniti₊′equiv) β⊎₁ ⊙ ! β₁)
       (β₂ ⊙ ! unite₊′-coh ⊙ ! cong∘l (gg uniti₊′equiv) β⊎₂ ⊙ ! β₂)

assocr₊-nat : ∀ {A B C D E F : Set} →
  {f₀ : A ≃ D} {f₁ : B ≃ E} {f₂ : C ≃ F} →
  assocr₊equiv ● ((f₀ ⊎≃ f₁) ⊎≃ f₂) ≋ (f₀ ⊎≃ (f₁ ⊎≃ f₂)) ● assocr₊equiv
assocr₊-nat {A} {B} {C} {D} {E} {F} {f₀} {f₁} {f₂} =
  let assocrDEF = proj₁ (assocr₊equiv {D} {E} {F}) in
  let assocrABC = proj₁ (assocr₊equiv {A} {B} {C}) in
  let assoclDEF = gg (assocr₊equiv {D} {E} {F}) in
  let assoclABC = gg (assocr₊equiv {A} {B} {C}) in
  eq (β₁ ⊙ cong∘l assocrDEF (β⊎₁ ⊙ (β⊎₁ ⊎∼ refl∼)) ⊙
           assocr₊-wf ⊙
           ! cong∘r assocrABC (refl∼ ⊎∼ β⊎₁) ⊙
           ! cong∘r assocrABC β⊎₁ ⊙ ! β₁)
     (β₂ ⊙ cong∘r assoclDEF (β⊎₂ {f = f₀ ⊎≃ f₁} {f₂}) ⊙
           cong∘r assoclDEF (β⊎₂ ⊎∼ refl∼) ⊙
           assocl₊-wf ⊙
          ! cong∘l assoclABC (refl∼ ⊎∼ β⊎₂) ⊙
          ! cong∘l assoclABC (β⊎₂ {f = f₀} {f₁ ⊎≃ f₂}) ⊙ ! β₂)

assocl₊-nat : ∀ {A B C D E F : Set} →
  {f₀ : A ≃ D} {f₁ : B ≃ E} {f₂ : C ≃ F} →
  assocl₊equiv ● (f₀ ⊎≃ (f₁ ⊎≃ f₂)) ≋ ((f₀ ⊎≃ f₁) ⊎≃ f₂) ● assocl₊equiv
assocl₊-nat {A} {B} {C} {D} {E} {F} {f₀} {f₁} {f₂} =
  let assoclDEF = proj₁ (assocl₊equiv {D} {E} {F}) in
  let assoclABC = proj₁ (assocl₊equiv {A} {B} {C}) in
  let assocrDEF = gg (assocl₊equiv {D} {E} {F}) in
  let assocrABC = gg (assocl₊equiv {A} {B} {C}) in
  eq (β₁ ⊙ cong∘l assoclDEF β⊎₁ ⊙
           cong∘l assoclDEF (refl∼ ⊎∼ β⊎₁) ⊙
           ! assocl₊-wf ⊙
           ! cong∘r assoclABC (β⊎₁ ⊎∼ refl∼) ⊙
           ! cong∘r assoclABC β⊎₁ ⊙ ! β₁)
     (β₂ ⊙ cong∘r assocrDEF (β⊎₂ {f = f₀} {f₁ ⊎≃ f₂}) ⊙
           cong∘r assocrDEF (refl∼ ⊎∼ β⊎₂) ⊙
           ! assocr₊-wf ⊙
           ! cong∘l assocrABC (β⊎₂ ⊎∼ refl∼) ⊙
           ! cong∘l assocrABC (β⊎₂ {f = f₀ ⊎≃ f₁} {f₂}) ⊙ ! β₂)

-- often called 'triangle'
unite-assocr₊-coh : ∀ {A B : Set} →
  unite₊′equiv ⊎≃ id≃ ≋ (id≃ ⊎≃ unite₊equiv) ● assocr₊equiv {A} {⊥} {B}
unite-assocr₊-coh = -- eq triangle⊎-right triangle⊎-left
  eq (β⊎₁ ⊙ triangle⊎-right ⊙ ! (β₁ ⊙ cong∘r (proj₁ assocr₊equiv) β⊎₁))
     (β⊎₂ ⊙ triangle⊎-left ⊙ ! (β₂ ⊙ cong∘l (gg assocr₊equiv) β⊎₂))

-- often called 'pentagon'
assocr₊-coh : ∀ {A B C D : Set} →
  assocr₊equiv {A} {B} {C ⊎ D} ● assocr₊equiv ≋
  (id≃ ⊎≃ assocr₊equiv) ● assocr₊equiv ● (assocr₊equiv ⊎≃ id≃)
assocr₊-coh = -- eq pentagon⊎-right pentagon⊎-left
 eq (β₁ ⊙ pentagon⊎-right ⊙
     ! (β₁ ⊙ cong₂∘ β⊎₁ β₁ ⊙
        cong∘l ((proj₁ id≃ ⊎→ proj₁ assocr₊equiv) ∘ proj₁ assocr₊equiv) β⊎₁))
    (β₂ ⊙ pentagon⊎-left ⊙
     ! (β₂ ⊙ cong₂∘ β₂ β⊎₂ ⊙
        cong∘r (gg assocr₊equiv ∘ (gg id≃ ⊎→ gg assocr₊equiv)) β⊎₂))

swap₊-nat : {A B C D : Set} {f : A ≃ C} {g : B ≃ D} →
  swap₊equiv ● (f ⊎≃ g) ≋ (g ⊎≃ f) ● swap₊equiv
swap₊-nat =
  eq (β₁ ⊙ cong∘l (proj₁ swap₊equiv) β⊎₁ ⊙ swap₊-coh ⊙
        ! (β₁ ⊙ cong∘r (proj₁ swap₊equiv) β⊎₁))
     (β₂ ⊙ cong∘r (gg swap₊equiv) β⊎₂ ⊙ sym∼ swap₊-coh ⊙
        ! (β₂ ⊙ cong∘l (gg swap₊equiv) β⊎₂))

-- also called 'triangle', but better to call it 'unit coherence'
unite₊l-coh : {A : Set} →
  unite₊equiv {A} ≋ unite₊′equiv ● swap₊equiv
unite₊l-coh =
  eq (unite₊-swap-coh-right ⊙ ! β₁) (unite₊-swap-coh-left ⊙ ! β₂)

-- often called 'hexagon'
assocr₊-swap₊-coh : ∀ {A B C : Set} →
  assocr₊equiv {B} {C} {A} ● swap₊equiv ● assocr₊equiv {A} {B} {C} ≋
  id≃ ⊎≃ swap₊equiv ● assocr₊equiv {B} {A} {C} ● swap₊equiv ⊎≃ id≃
assocr₊-swap₊-coh {A} {B} {C} = -- eq hexagon⊎-right hexagon⊎-left
  let assocrBCA = proj₁ (assocr₊equiv {B} {C} {A}) in
  let assocrABC = proj₁ (assocr₊equiv {A} {B} {C}) in
  let assocrBAC = proj₁ (assocr₊equiv {B} {A} {C}) in
  let swapAC = proj₁ id≃ ⊎→ proj₁ (swap₊equiv {A} {C}) in
  let assoclBCA = gg (assocr₊equiv {B} {C} {A}) in
  let assoclABC = gg (assocr₊equiv {A} {B} {C}) in
  let assoclBAC = gg (assocr₊equiv {B} {A} {C}) in
  let swapCA = gg id≃ ⊎→ gg (swap₊equiv {A} {C}) in
  eq (β₁ ⊙ cong∘l assocrBCA β₁ ⊙ hexagon⊎-right ⊙
      ! (β₁ ⊙ cong₂∘ β⊎₁ β₁ ⊙ cong∘l (swapAC ∘ assocrBAC) β⊎₁))
     (β₂ ⊙ cong∘r assoclBCA β₂ ⊙ hexagon⊎-left ⊙
      ! (β₂ ⊙ cong₂∘ β₂ β⊎₂ ⊙ cong∘r (assoclBAC ∘ swapCA) β⊎₂))

-- and in the opposite direction

assocl₊-swap₊-coh : ∀ {A B C : Set} →
  assocl₊equiv {A} {B} {C} ● swap₊equiv ● assocl₊equiv {B} {C} {A} ≋
  swap₊equiv ⊎≃ id≃ ● assocl₊equiv {B} {A} {C} ● id≃ ⊎≃ swap₊equiv
assocl₊-swap₊-coh {A} {B} {C} = -- eq hexagon⊎-left hexagon⊎-right
  let assoclBCA = proj₁ (assocl₊equiv {B} {C} {A}) in
  let assoclABC = proj₁ (assocl₊equiv {A} {B} {C}) in
  let assoclBAC = proj₁ (assocl₊equiv {B} {A} {C}) in
  let swapBA = proj₁ (swap₊equiv {B} {A}) ⊎→ proj₁ id≃ in
  let assocrBCA = gg (assocl₊equiv {B} {C} {A}) in
  let assocrABC = gg (assocl₊equiv {A} {B} {C}) in
  let assocrBAC = gg (assocl₊equiv {B} {A} {C}) in
  let swapAB = gg (swap₊equiv {B} {A}) ⊎→ proj₁ id≃ in
  eq (β₁ ⊙ (cong∘l assoclABC β₁ ⊙ hexagon⊎-left) ⊙
      ! (β₁ ⊙ cong₂∘ β⊎₁ β₁ ⊙ cong∘l (swapBA ∘ assoclBAC) β⊎₁))
     (β₂ ⊙ cong∘r assocrABC β₂ ⊙ hexagon⊎-right ⊙
      ! (β₂ ⊙ cong₂∘ β₂ β⊎₂ ⊙ cong∘r (assocrBAC ∘ swapAB) β⊎₂))

-- equivalences for the × structure

id×id≋id : ∀ {A B : Set} → id≃ {A = A} ×≃ id≃ {A = B} ≋ id≃
id×id≋id = eq (β×₁ ⊙ id×id∼id) (β×₂ ⊙ id×id∼id)

×●≋●× : {A B C D E F : Set} →
  {f : A ≃ C} {g : B ≃ D} {h : C ≃ E} {i : D ≃ F} →
  (h ● f) ×≃ (i ● g) ≋ (h ×≃ i) ● (f ×≃ g)
×●≋●× {f = f , qinv f⁻¹ _ _} {g , qinv g⁻¹ _ _} {h , qinv h⁻¹ _ _} {i , qinv i⁻¹ _ _} =
  eq (β×₁ ⊙ β₁ ×∼ β₁ ⊙ (×∘∼∘× {f = f} {g} {h} {i}) ⊙ ! cong₂∘ β×₁ β×₁ ⊙ ! β₁)
     (β×₂ ⊙ β₂ ×∼ β₂ ⊙ (×∘∼∘× {f = h⁻¹} {i⁻¹} {f⁻¹} {g⁻¹}) ⊙ ! cong₂∘ β×₂ β×₂ ⊙ ! β₂)

_×≋_ :  ∀ {A B C D : Set} {f g : A ≃ B} {h i : C ≃ D} →
  f ≋ g → h ≋ i → f ×≃ h ≋ g ×≃ i
e₁ ×≋ e₂ = eq (β×₁ ⊙ (f≡ e₁) ×∼ (f≡ e₂) ⊙ ! β×₁)
              (β×₂ ⊙ (g≡ e₁) ×∼ (g≡ e₂) ⊙ ! β×₂)
  where open _≋_

sym≃-distrib× : ∀ {A B C D : Set} {f : A ≃ B} {g : C ≃ D} →
  sym≃ (f ×≃ g) ≋ sym≃ f ×≃ sym≃ g
sym≃-distrib× = -- note how the proof mixes ₁ and ₂ !
  eq (β×₂ ⊙ ! β×₁) (β×₁ ⊙ ! β×₂)

unite⋆-nat : ∀ {A B} {f : A ≃ B} {g : ⊤ ≃ ⊤} →
  unite⋆equiv ● (g ×≃ f) ≋ f ● unite⋆equiv
unite⋆-nat = -- eq unite⋆-coh uniti⋆-coh
  eq (β₁ ⊙ cong∘l (proj₁ unite⋆equiv) β×₁ ⊙ unite⋆-coh ⊙ ! β₁)
     (β₂ ⊙ cong∘r (gg unite⋆equiv) β×₂ ⊙ uniti⋆-coh ⊙ ! β₂)

uniti⋆-nat : ∀ {A B} {f : A ≃ B} {g : ⊤ ≃ ⊤} →
  uniti⋆equiv ● f ≋ (g ×≃ f) ● uniti⋆equiv
uniti⋆-nat = -- flip-sym≋ unite⋆-nat
  eq (β₁ ⊙ ! uniti⋆-coh ⊙ ! cong∘r (proj₁ uniti⋆equiv) β×₁ ⊙ ! β₁)
     (β₂ ⊙ ! unite⋆-coh ⊙ ! cong∘l (gg uniti⋆equiv) β×₂ ⊙ ! β₂)

unite⋆′-nat : ∀ {A B} {f : A ≃ B} {g : ⊤ ≃ ⊤} →
  unite⋆′equiv ● (f ×≃ g) ≋ f ● unite⋆′equiv
unite⋆′-nat = -- eq unite⋆′-coh uniti⋆′-coh
  eq (β₁ ⊙ cong∘l (proj₁ unite⋆′equiv) β×₁ ⊙ unite⋆′-coh ⊙ ! β₁)
     (β₂ ⊙ cong∘r (gg unite⋆′equiv) β×₂ ⊙ uniti⋆′-coh ⊙ ! β₂)

uniti⋆′-nat : ∀ {A B} {f : A ≃ B} {g : ⊤ ≃ ⊤} →
  uniti⋆′equiv ● f ≋ (f ×≃ g) ● uniti⋆′equiv
uniti⋆′-nat = -- flip-sym≋ unite⋆′-nat
  eq (β₁ ⊙ ! uniti⋆′-coh ⊙ ! cong∘r (proj₁ uniti⋆′equiv) β×₁ ⊙ ! β₁)
     (β₂ ⊙ ! unite⋆′-coh ⊙ ! cong∘l (gg uniti⋆′equiv) β×₂ ⊙ ! β₂)

assocr⋆-nat : ∀ {A B C D E F : Set} →
  {f₀ : A ≃ D} {f₁ : B ≃ E} {f₂ : C ≃ F} →
  assocr⋆equiv ● ((f₀ ×≃ f₁) ×≃ f₂) ≋ (f₀ ×≃ (f₁ ×≃ f₂)) ● assocr⋆equiv
assocr⋆-nat {A} {B} {C} {D} {E} {F} {f₀} {f₁} {f₂} = -- eq assocr⋆-wf assocl⋆-wf
  let assocrDEF = proj₁ (assocr⋆equiv {D} {E} {F}) in
  let assocrABC = proj₁ (assocr⋆equiv {A} {B} {C}) in
  let assoclDEF = gg (assocr⋆equiv {D} {E} {F}) in
  let assoclABC = gg (assocr⋆equiv {A} {B} {C}) in
  eq (β₁ ⊙ cong∘l assocrDEF β×₁ ⊙
           cong∘l assocrDEF (β×₁ ×∼ refl∼) ⊙
           assocr⋆-wf ⊙
           ! cong∘r assocrABC (refl∼ ×∼ β×₁) ⊙
           ! cong∘r assocrABC β×₁ ⊙ ! β₁)
     (β₂ ⊙ cong∘r assoclDEF (β×₂ {f = f₀ ×≃ f₁} {f₂}) ⊙
           cong∘r assoclDEF (β×₂ ×∼ refl∼) ⊙
           assocl⋆-wf ⊙
          ! cong∘l assoclABC (refl∼ ×∼ β×₂) ⊙
          ! cong∘l assoclABC (β×₂ {f = f₀} {f₁ ×≃ f₂}) ⊙ ! β₂)
assocl⋆-nat : ∀ {A B C D E F : Set} →
  {f₀ : A ≃ D} {f₁ : B ≃ E} {f₂ : C ≃ F} →
  assocl⋆equiv ● (f₀ ×≃ (f₁ ×≃ f₂)) ≋ ((f₀ ×≃ f₁) ×≃ f₂) ● assocl⋆equiv
assocl⋆-nat {A} {B} {C} {D} {E} {F} {f₀} {f₁} {f₂}  = -- flip-sym≋ assocr⋆-nat
  let assoclDEF = proj₁ (assocl⋆equiv {D} {E} {F}) in
  let assoclABC = proj₁ (assocl⋆equiv {A} {B} {C}) in
  let assocrDEF = gg (assocl⋆equiv {D} {E} {F}) in
  let assocrABC = gg (assocl⋆equiv {A} {B} {C}) in
  eq (β₁ ⊙ cong∘l assoclDEF β×₁ ⊙
           cong∘l assoclDEF (refl∼ ×∼ β×₁) ⊙
           ! assocl⋆-wf ⊙
           ! cong∘r assoclABC (β×₁ ×∼ refl∼) ⊙
           ! cong∘r assoclABC β×₁ ⊙ ! β₁)
     (β₂ ⊙ cong∘r assocrDEF (β×₂ {f = f₀} {f₁ ×≃ f₂}) ⊙
           cong∘r assocrDEF (refl∼ ×∼ β×₂) ⊙
           ! assocr⋆-wf ⊙
           ! cong∘l assocrABC (β×₂ ×∼ refl∼) ⊙
           ! cong∘l assocrABC (β×₂ {f = f₀ ×≃ f₁} {f₂}) ⊙ ! β₂)

-- often called 'triangle'

unite-assocr⋆-coh : ∀ {A B : Set} →
  unite⋆′equiv ×≃ id≃ ≋ (id≃ ×≃ unite⋆equiv) ● assocr⋆equiv {A} {⊤} {B}
unite-assocr⋆-coh =
  eq (β×₁ ⊙ triangle×-right ⊙ ! (β₁ ⊙ cong∘r (proj₁ assocr⋆equiv) β×₁))
     (β×₂ ⊙ triangle×-left ⊙ ! (β₂ ⊙ cong∘l (gg assocr⋆equiv) β×₂))

-- often called 'pentagon'

assocr⋆-coh : ∀ {A B C D : Set} →
  assocr⋆equiv {A} {B} {C × D} ● assocr⋆equiv ≋
  (id≃ ×≃ assocr⋆equiv) ● assocr⋆equiv ● (assocr⋆equiv ×≃ id≃)
assocr⋆-coh =
 eq (β₁ ⊙ pentagon×-right ⊙
     ! (β₁ ⊙ cong₂∘ β×₁ β₁ ⊙
        cong∘l ((proj₁ id≃ ×→ proj₁ assocr⋆equiv) ∘ proj₁ assocr⋆equiv) β×₁))
    (β₂ ⊙ pentagon×-left ⊙
     ! (β₂ ⊙ cong₂∘ β₂ β×₂ ⊙
        cong∘r (gg assocr⋆equiv ∘ (gg id≃ ×→ gg assocr⋆equiv)) β×₂))

swap⋆-nat : {A B C D : Set} {f : A ≃ C} {g : B ≃ D} →
  swap⋆equiv ● (f ×≃ g) ≋ (g ×≃ f) ● swap⋆equiv
swap⋆-nat =
  eq (β₁ ⊙ cong∘l (proj₁ swap⋆equiv) β×₁ ⊙ swap⋆-coh ⊙
        ! (β₁ ⊙ cong∘r (proj₁ swap⋆equiv) β×₁))
     (β₂ ⊙ cong∘r (gg swap⋆equiv) β×₂ ⊙ sym∼ swap⋆-coh ⊙
        ! (β₂ ⊙ cong∘l (gg swap⋆equiv) β×₂))

-- also called 'triangle', but better to call it 'unit coherence'
unite⋆l-coh : {A : Set} →
  unite⋆equiv {A} ≋ unite⋆′equiv ● swap⋆equiv
unite⋆l-coh =
  eq (unite⋆-swap-coh-right ⊙ ! β₁) (unite⋆-swap-coh-left ⊙ ! β₂)

-- often called 'hexagon'

assocr⋆-swap⋆-coh : ∀ {A B C : Set} →
  assocr⋆equiv {B} {C} {A} ● swap⋆equiv ● assocr⋆equiv {A} {B} {C} ≋
  id≃ ×≃ swap⋆equiv ● assocr⋆equiv {B} {A} {C} ● swap⋆equiv ×≃ id≃
assocr⋆-swap⋆-coh {A} {B} {C} =
  let assocrBCA = proj₁ (assocr⋆equiv {B} {C} {A}) in
  let assocrABC = proj₁ (assocr⋆equiv {A} {B} {C}) in
  let assocrBAC = proj₁ (assocr⋆equiv {B} {A} {C}) in
  let swapAC = proj₁ id≃ ×→ proj₁ (swap⋆equiv {A} {C}) in
  let assoclBCA = gg (assocr⋆equiv {B} {C} {A}) in
  let assoclABC = gg (assocr⋆equiv {A} {B} {C}) in
  let assoclBAC = gg (assocr⋆equiv {B} {A} {C}) in
  let swapCA = gg id≃ ×→ gg (swap⋆equiv {A} {C}) in
  eq (β₁ ⊙ cong∘l assocrBCA β₁ ⊙ hexagon×-right ⊙
      ! (β₁ ⊙ cong₂∘ β×₁ β₁ ⊙ cong∘l (swapAC ∘ assocrBAC) β×₁))
     (β₂ ⊙ cong∘r assoclBCA β₂ ⊙ hexagon×-left ⊙
      ! (β₂ ⊙ cong₂∘ β₂ β×₂ ⊙ cong∘r (assoclBAC ∘ swapCA) β×₂))

-- and in the opposite direction

assocl⋆-swap⋆-coh : ∀ {A B C : Set} →
  assocl⋆equiv {A} {B} {C} ● swap⋆equiv ● assocl⋆equiv {B} {C} {A} ≋
  swap⋆equiv ×≃ id≃ ● assocl⋆equiv {B} {A} {C} ● id≃ ×≃ swap⋆equiv
assocl⋆-swap⋆-coh {A} {B} {C} =
  let assoclBCA = proj₁ (assocl⋆equiv {B} {C} {A}) in
  let assoclABC = proj₁ (assocl⋆equiv {A} {B} {C}) in
  let assoclBAC = proj₁ (assocl⋆equiv {B} {A} {C}) in
  let swapBA = proj₁ (swap⋆equiv {B} {A}) ×→ proj₁ id≃ in
  let assocrBCA = gg (assocl⋆equiv {B} {C} {A}) in
  let assocrABC = gg (assocl⋆equiv {A} {B} {C}) in
  let assocrBAC = gg (assocl⋆equiv {B} {A} {C}) in
  let swapAB = gg (swap⋆equiv {B} {A}) ×→ proj₁ id≃ in
  eq (β₁ ⊙ (cong∘l assoclABC β₁ ⊙ hexagon×-left) ⊙
      ! (β₁ ⊙ cong₂∘ β×₁ β₁ ⊙ cong∘l (swapBA ∘ assoclBAC) β×₁))
     (β₂ ⊙ cong∘r assocrABC β₂ ⊙ hexagon×-right ⊙
      ! (β₂ ⊙ cong₂∘ β₂ β×₂ ⊙ cong∘r (assocrBAC ∘ swapAB) β×₂))

-- distributivity

distl-nat : {A B C D E F : Set} →
  {f : A ≃ D} {g : B ≃ E} {h : C ≃ F} →
  distlequiv ● (f ×≃ (g ⊎≃ h)) ≋ ((f ×≃ g) ⊎≃ (f ×≃ h)) ● distlequiv
distl-nat {A} {B} {C} {D} {E} {F} {f} {g} {h} = -- eq distl-coh factorl-coh
  let distlDEF = proj₁ (distlequiv {D} {E} {F}) in
  let distlABC = proj₁ (distlequiv {A} {B} {C}) in
  let factorlDEF = gg (distlequiv {D} {E} {F}) in
  let factorlABC = gg (distlequiv {A} {B} {C}) in
  eq (β₁ ⊙ cong∘l distlDEF (β×₁ ⊙ (refl∼ ×∼ β⊎₁)) ⊙
      distl-coh ⊙
      ! (β₁ ⊙ cong∘r distlABC (β⊎₁ ⊙ (β×₁ ⊎∼ β×₁))))
      --
     (β₂ ⊙ cong∘r factorlDEF (β×₂ {f = f} {g ⊎≃ h} ⊙ (refl∼ ×∼ β⊎₂)) ⊙
      factorl-coh ⊙
      ! (β₂ ⊙ cong∘l factorlABC (β⊎₂ {f = f ×≃ g} {f ×≃ h} ⊙ (β×₂ ⊎∼ β×₂))))

factorl-nat : {A B C D E F : Set} →
  {f : A ≃ D} {g : B ≃ E} {h : C ≃ F} →
   factorlequiv ● ((f ×≃ g) ⊎≃ (f ×≃ h)) ≋ (f ×≃ (g ⊎≃ h)) ● factorlequiv
factorl-nat {A} {B} {C} {D} {E} {F} {f} {g} {h} = -- flip-sym≋ distl-nat
  let factorlDEF = proj₁ (factorlequiv {D} {E} {F}) in
  let factorlABC = proj₁ (factorlequiv {A} {B} {C}) in
  let distlDEF = gg (factorlequiv {D} {E} {F}) in
  let distlABC = gg (factorlequiv {A} {B} {C}) in
  eq (β₁ ⊙ cong∘l factorlDEF (β⊎₁ ⊙ (β×₁ ⊎∼ β×₁)) ⊙
      sym∼ factorl-coh ⊙
      ! (β₁ ⊙ cong∘r factorlABC (β×₁ ⊙ (refl∼ ×∼ β⊎₁)) ))
     --
     (β₂ ⊙ cong∘r distlDEF (β⊎₂ {f = f ×≃ g} {f ×≃ h} ⊙ (β×₂ ⊎∼ β×₂)) ⊙
     sym∼ distl-coh ⊙
     ! (β₂ ⊙ cong∘l distlABC (β×₂ {f = f} {g ⊎≃ h} ⊙ (refl∼ ×∼ β⊎₂))))

dist-nat : {A B C D E F : Set} →
  {f : A ≃ D} {g : B ≃ E} {h : C ≃ F} →
  distequiv ● ((f ⊎≃ g) ×≃ h) ≋ ((f ×≃ h) ⊎≃ (g ×≃ h)) ● distequiv
dist-nat {A} {B} {C} {D} {E} {F} {f} {g} {h} = -- eq dist-coh factor-coh
  let distDEF = proj₁ (distequiv {D} {E} {F}) in
  let distABC = proj₁ (distequiv {A} {B} {C}) in
  let factorDEF = gg (distequiv {D} {E} {F}) in
  let factorABC = gg (distequiv {A} {B} {C}) in
  eq (β₁ ⊙ cong∘l distDEF (β×₁ ⊙ (β⊎₁ ×∼ refl∼)) ⊙
      dist-coh ⊙
      ! (β₁ ⊙ cong∘r distABC (β⊎₁ ⊙ (β×₁ ⊎∼ β×₁))))
      --
     (β₂ ⊙ cong∘r factorDEF (β×₂ {f = f ⊎≃ g} {h} ⊙ (β⊎₂ ×∼ refl∼)) ⊙
      factor-coh ⊙
      ! (β₂ ⊙ cong∘l factorABC (β⊎₂ {f = f ×≃ h} {g ×≃ h} ⊙ (β×₂ ⊎∼ β×₂))))

factor-nat : {A B C D E F : Set} →
  {f : A ≃ D} {g : B ≃ E} {h : C ≃ F} →
  factorequiv ● ((f ×≃ h) ⊎≃ (g ×≃ h)) ≋ ((f ⊎≃ g) ×≃ h) ● factorequiv
factor-nat {A} {B} {C} {D} {E} {F} {f} {g} {h} = -- flip-sym≋ dist-nat
  let factorDEF = proj₁ (factorequiv {D} {E} {F}) in
  let factorABC = proj₁ (factorequiv {A} {B} {C}) in
  let distDEF = gg (factorequiv {D} {E} {F}) in
  let distABC = gg (factorequiv {A} {B} {C}) in
  eq (β₁ ⊙ cong∘l factorDEF (β⊎₁ ⊙ (β×₁ ⊎∼ β×₁)) ⊙
      sym∼ factor-coh ⊙
      ! (β₁ ⊙ cong∘r factorABC (β×₁ ⊙ (β⊎₁ ×∼ refl∼)) ))
     --
     (β₂ ⊙ cong∘r distDEF (β⊎₂ {f = f ×≃ h} {g ×≃ h} ⊙ (β×₂ ⊎∼ β×₂)) ⊙
     sym∼ dist-coh ⊙
     ! (β₂ ⊙ cong∘l distABC (β×₂ {f = f ⊎≃ g} {h} ⊙ (β⊎₂ ×∼ refl∼))))

-- note how we don't use id≃ but an arbitrary ⊥ ≃ ⊥.
-- because this law under-specifies f and g, we need to
-- be explicit in our calls

distzr-nat : {A B : Set} → {f : A ≃ B} → {g : ⊥ ≃ ⊥} →
  distzrequiv ● (f ×≃ g) ≋ g ● distzrequiv
distzr-nat {f = (f , qinv h _ _)} {(_ , qinv g _ _)} =
  -- eq (distzr-coh {f = f}) (factorzr-coh {f = h} {g})
  eq (β₁ ⊙ cong∘l (proj₁ distzrequiv) β×₁ ⊙ distzr-coh {f = f} ⊙ ! β₁)
     (β₂ ⊙ cong∘r (gg distzrequiv) β×₂ ⊙ factorzr-coh {f = h} {g} ⊙ ! β₂)

factorzr-nat : {A B : Set} → {f : A ≃ B} → {g : ⊥ ≃ ⊥} →
  factorzrequiv ● g ≋ (f ×≃ g) ● factorzrequiv
factorzr-nat {f = f , qinv f⁻¹ _ _} {g , _} = -- flip-sym≋ (distzr-nat {f = sym≃ f})
  eq (β₁ ⊙ sym∼ (factorzr-coh {f = f} {g}) ⊙
     ! (β₁ ⊙ cong∘r (proj₁ factorzrequiv) β×₁) )
     --
     (β₂ ⊙ sym∼ (distzr-coh {f = f⁻¹}) ⊙
     ! (β₂ ⊙ cong∘l (gg factorzrequiv) β×₂))

-- same comment as above

distz-nat : {A B : Set} → {f : A ≃ B} → {g : ⊥ ≃ ⊥} →
  distzequiv ● (g ×≃ f) ≋ g ● distzequiv
distz-nat {f = (f , qinv h _ _)} {(_ , qinv g _ _)} =
  eq (β₁ ⊙ cong∘l (proj₁ distzequiv) β×₁ ⊙ distz-coh {f = f} ⊙ ! β₁)
     (β₂ ⊙ cong∘r (gg distzequiv) β×₂ ⊙ factorz-coh {f = h} {g} ⊙ ! β₂)

factorz-nat : {A B : Set} → {f : A ≃ B} → {g : ⊥ ≃ ⊥} →
  factorzequiv ● g ≋ (g ×≃ f) ● factorzequiv
factorz-nat {f = (f , qinv f⁻¹ _ _)} {g , _} =
  eq (β₁ ⊙ (sym∼ (factorz-coh {f = f} {g})) ⊙
        ! (β₁ ⊙ cong∘r (proj₁ factorzequiv) β×₁))
     (β₂ ⊙ (sym∼ (distz-coh {f = f⁻¹})) ⊙ ! (β₂ ⊙ cong∘l (gg factorzequiv) β×₂))

-- some equivalences for which there are two 'obvious'
-- programs, but are in fact equivalent.  Named after
-- the types which are witnessed to be equivalent.

A×[B⊎C]≃[A×C]⊎[A×B] : {A B C : Set} →
  distlequiv ● (id≃ {A = A} ×≃ swap₊equiv {B} {C}) ≋ swap₊equiv ● distlequiv
A×[B⊎C]≃[A×C]⊎[A×B] = -- eq A×[B⊎C]→[A×C]⊎[A×B] [A×C]⊎[A×B]→A×[B⊎C]
  eq (β₁ ⊙ cong∘l (proj₁ distlequiv) β×₁ ⊙ A×[B⊎C]→[A×C]⊎[A×B] ⊙ ! β₁)
     (β₂ ⊙ cong∘r (gg distlequiv) β×₂ ⊙ [A×C]⊎[A×B]→A×[B⊎C] ⊙ ! β₂)

[A⊎B]×C≃[C×A]⊎[C×B] : {A B C : Set} →
  (swap⋆equiv ⊎≃ swap⋆equiv) ● distequiv ≋ distlequiv ● swap⋆equiv {A ⊎ B} {C}
[A⊎B]×C≃[C×A]⊎[C×B] = -- eq [A⊎B]×C→[C×A]⊎[C×B] [C×A]⊎[C×B]→[A⊎B]×C
  eq (β₁ ⊙ cong∘r (proj₁ distequiv) β⊎₁ ⊙ [A⊎B]×C→[C×A]⊎[C×B] ⊙ ! β₁)
     (β₂ ⊙ cong∘l (gg distequiv) β⊎₂ ⊙ [C×A]⊎[C×B]→[A⊎B]×C ⊙ ! β₂)

[A⊎B⊎C]×D≃[A×D⊎B×D]⊎C×D : {A B C D : Set} →
  (distequiv ⊎≃ id≃) ● distequiv ● (assocl₊equiv {A} {B} {C} ×≃ id≃ {A = D}) ≋
  assocl₊equiv ● (id≃ ⊎≃ distequiv) ● distequiv
[A⊎B⊎C]×D≃[A×D⊎B×D]⊎C×D = -- eq [A⊎B⊎C]×D→[A×D⊎B×D]⊎C×D [A×D⊎B×D]⊎C×D→[A⊎B⊎C]×D
  eq (β₁ ⊙ cong₂∘ β⊎₁ (β₁ ⊙ cong∘l (proj₁ distequiv) β×₁) ⊙
      [A⊎B⊎C]×D→[A×D⊎B×D]⊎C×D ⊙
      ! (β₁ ⊙ cong∘l (proj₁ assocl₊equiv) (β₁ ⊙ cong∘r (proj₁ distequiv) β⊎₁)))
      --
     (β₂ ⊙ cong₂∘ (β₂ ⊙ cong∘r (gg distequiv) β×₂) β⊎₂ ⊙
      [A×D⊎B×D]⊎C×D→[A⊎B⊎C]×D ⊙
      ! (β₂ ⊙ cong∘r (gg assocl₊equiv) (β₂ ⊙ cong∘l (gg distequiv) β⊎₂)))

A×B×[C⊎D]≃[A×B]×C⊎[A×B]×D : {A B C D : Set} →
  distlequiv ● assocl⋆equiv {A} {B} {C ⊎ D} ≋
  (assocl⋆equiv ⊎≃ assocl⋆equiv) ● distlequiv ● (id≃ ×≃ distlequiv)
A×B×[C⊎D]≃[A×B]×C⊎[A×B]×D =
  eq (β₁ ⊙ A×B×[C⊎D]→[A×B]×C⊎[A×B]×D ⊙
      ! (β₁ ⊙ cong₂∘ β⊎₁ (β₁ ⊙ cong∘l (proj₁ distlequiv) β×₁)))
     (β₂ ⊙ [A×B]×C⊎[A×B]×D→A×B×[C⊎D] ⊙
      ! (β₂ ⊙ cong₂∘ (β₂ ⊙ cong∘r (gg distlequiv) β×₂) β⊎₂))

0×0≃0 : distzequiv ≋ distzrequiv
0×0≃0 = eq 0×0→0 0→0×0

0×[A⊎B]≃0 : {A B : Set} →
  distzequiv ≋ unite₊equiv ● (distzequiv ⊎≃ distzequiv) ● distlequiv {⊥} {A} {B}
0×[A⊎B]≃0 =
  eq (0×[A⊎B]→0 ⊙
      ! (β₁ ⊙ cong∘l (proj₁ unite₊equiv) (β₁ ⊙ cong∘r (proj₁ distlequiv) β⊎₁)))
     (0→0×[A⊎B] ⊙
     ! (β₂ ⊙ cong∘r (gg unite₊equiv) (β₂ ⊙ cong∘l (gg distlequiv) β⊎₂)))

0×1≃0 : unite⋆′equiv  ≋ distzequiv
0×1≃0 = eq 0×1→0 0→0×1

A×0≃0 : {A : Set} → distzrequiv {A} ≋ distzequiv ● swap⋆equiv
A×0≃0 = eq (A×0→0 ⊙ ! β₁) (0→A×0 ⊙ ! β₂)

0×A×B≃0 : {A B : Set} →
  distzequiv ≋ distzequiv ● (distzequiv ×≃ id≃) ● assocl⋆equiv {⊥} {A} {B}
0×A×B≃0 =
  let distzB = proj₁ distzequiv in
  let factorzA = gg distzequiv in
  eq (0×A×B→0 ⊙
      ! (β₁ ⊙ cong∘l distzB (β₁ ⊙ cong∘r (proj₁ assocl⋆equiv) β×₁)))
     (0→0×A×B ⊙
       ! (β₂ ⊙ cong∘r factorzA (β₂ ⊙ cong∘l (gg assocl⋆equiv) β×₂)))

A×0×B≃0 : {A B : Set} →
  distzrequiv ● (id≃ ×≃ distzequiv)  ≋
  distzequiv ● (distzrequiv ×≃ id≃) ● assocl⋆equiv {A} {⊥} {B}
A×0×B≃0 =
  eq (β₁ ⊙ cong∘l (proj₁ distzrequiv) β×₁ ⊙ A×0×B→0 ⊙
      ! (β₁ ⊙ cong∘l (proj₁ distzequiv)
                     (β₁ ⊙ cong∘r (proj₁ assocl⋆equiv) β×₁)))
     (β₂ ⊙ cong∘r (gg distzrequiv) β×₂ ⊙  0→A×0×B ⊙
      ! (β₂ ⊙ cong∘r (gg distzequiv)
                      (β₂ ⊙ cong∘l (gg assocl⋆equiv) β×₂)))

A×[0+B]≃A×B : {A B : Set} →
  (id≃ {A = A} ×≃ unite₊equiv {B}) ≋ unite₊equiv ● (distzrequiv ⊎≃ id≃) ● distlequiv
A×[0+B]≃A×B =
  eq (β×₁ ⊙ A×[0+B]→A×B ⊙
      ! (β₁ ⊙ cong∘l (proj₁ unite₊equiv) (β₁ ⊙ cong∘r (proj₁ distlequiv) β⊎₁)))
     (β×₂ ⊙ A×B→A×[0+B] ⊙
      ! (β₂ ⊙ cong∘r (gg unite₊equiv) (β₂ ⊙ cong∘l (gg distlequiv) β⊎₂)))

1×[A⊎B]≃A⊎B : {A B : Set} →
  unite⋆equiv ≋ (unite⋆equiv ⊎≃ unite⋆equiv) ● distlequiv {⊤} {A} {B}
1×[A⊎B]≃A⊎B =
  eq (1×[A⊎B]→A⊎B ⊙ ! (β₁ ⊙ cong∘r (proj₁ distlequiv) β⊎₁))
     (A⊎B→1×[A⊎B] ⊙ ! (β₂ ⊙ cong∘l (gg distlequiv) β⊎₂))

[A⊎B]×[C⊎D]≃[[A×C⊎B×C]⊎A×D]⊎B×D : {A B C D : Set} →
  assocl₊equiv ● (distequiv ⊎≃ distequiv) ● distlequiv ≋
  (assocl₊equiv ⊎≃ id≃) ● ((id≃ ⊎≃ swap₊equiv) ⊎≃ id≃) ●
     (assocr₊equiv ⊎≃ id≃) ● assocl₊equiv ●
        (distlequiv ⊎≃ distlequiv) ● distequiv {A} {B} {C ⊎ D}
[A⊎B]×[C⊎D]≃[[A×C⊎B×C]⊎A×D]⊎B×D =
  eq (β₁ ⊙ cong∘l (proj₁ assocl₊equiv)
                  (β₁ ⊙ cong∘r (proj₁ distlequiv) β⊎₁) ⊙
      [A⊎B]×[C⊎D]→[[A×C⊎B×C]⊎A×D]⊎B×D ⊙
      ! (β₁ ⊙ cong₂∘ β⊎₁ (β₁ ⊙ cong₂∘ (β⊎₁ ⊙ (β⊎₁ ⊎∼ refl∼))
              (β₁ ⊙ cong₂∘ β⊎₁ (β₁ ⊙ cong∘l (proj₁ assocl₊equiv)
                    (β₁ ⊙ cong∘r (proj₁ distequiv) β⊎₁))))))
      --
     (β₂ ⊙ cong∘r (gg assocl₊equiv) (β₂ ⊙ cong∘l (gg distlequiv) β⊎₂) ⊙
      [[A×C⊎B×C]⊎A×D]⊎B×D→[A⊎B]×[C⊎D] ⊙
      ! (β₂ ⊙ cong₂∘
          (β₂ ⊙ cong₂∘
            (β₂ ⊙ cong₂∘
              (β₂ ⊙ cong∘r (gg assocl₊equiv) (β₂ ⊙ cong∘l (gg distequiv) β⊎₂))
              β⊎₂)
            (β⊎₂ {f = id≃ ⊎≃ swap₊equiv} ⊙ (β⊎₂ ⊎∼ refl∼)))
          β⊎₂))

------------------------------------------------------------------------------
-- also useful

[g+1]●[1+f]≋g+f : {A B C D : Set} {f : A ≃ B} {g : C ≃ D} →
  (g ⊎≃ id≃) ● (id≃ ⊎≃ f) ≋ g ⊎≃ f
[g+1]●[1+f]≋g+f {f = f} {g} = begin (
  (g ⊎≃ id≃) ● (id≃ ⊎≃ f)
    ≋⟨ sym≋ ⊎●≋●⊎ ⟩
  (g ● id≃) ⊎≃ (id≃ ● f)
    ≋⟨ rid≋ ⊎≋ lid≋ ⟩
  g ⊎≃ f ∎)
  where open ≋-Reasoning

-- same proof as above, just written compactly

[1+f]●[g+1]≋g+f : {A B C D : Set} {f : A ≃ B} {g : C ≃ D} →
  (id≃ ⊎≃ f) ● (g ⊎≃ id≃) ≋ g ⊎≃ f
[1+f]●[g+1]≋g+f = trans≋ (sym≋ ⊎●≋●⊎) (lid≋ ⊎≋ rid≋)

-- put then together

[g+1]●[1+f]≋[1+f]●[g+1] : {A B C D : Set} {f : A ≃ B} {g : C ≃ D} →
  (g ⊎≃ id≃) ● (id≃ ⊎≃ f) ≋ (id≃ ⊎≃ f) ● (g ⊎≃ id≃)
[g+1]●[1+f]≋[1+f]●[g+1] = trans≋ [g+1]●[1+f]≋g+f (sym≋ [1+f]●[g+1]≋g+f)

--

[g*1]●[1*f]≋g*f : {A B C D : Set} {f : A ≃ B} {g : C ≃ D} →
  (g ×≃ id≃) ● (id≃ ×≃ f) ≋ g ×≃ f
[g*1]●[1*f]≋g*f {f = f} {g} = begin (
  (g ×≃ id≃) ● (id≃ ×≃ f)
    ≋⟨ sym≋ ×●≋●× ⟩
  (g ● id≃) ×≃ (id≃ ● f)
    ≋⟨ rid≋ ×≋ lid≋ ⟩
  g ×≃ f ∎)
  where open ≋-Reasoning

[1*f]●[g*1]≋g*f : {A B C D : Set} {f : A ≃ B} {g : C ≃ D} →
  (id≃ ×≃ f) ● (g ×≃ id≃) ≋ g ×≃ f
[1*f]●[g*1]≋g*f = trans≋ (sym≋ ×●≋●×) (lid≋ ×≋ rid≋)

[g*1]●[1*f]≋[1*f]●[g*1] : {A B C D : Set} {f : A ≃ B} {g : C ≃ D} →
  (g ×≃ id≃) ● (id≃ ×≃ f) ≋ (id≃ ×≃ f) ● (g ×≃ id≃)
[g*1]●[1*f]≋[1*f]●[g*1] = trans≋ [g*1]●[1*f]≋g*f (sym≋ [1*f]●[g*1]≋g*f)

------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- ω-continuous functions
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

module Partiality-algebra.Omega-continuous where

open import Equality.Propositional.Cubical
open import Prelude

open import Bijection equality-with-J using (_↔_)
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J
open import H-level.Closure equality-with-J

open import Partiality-algebra as PA
open import Partiality-algebra.Monotone

-- Definition of ω-continuous functions.

record [_⟶_]
         {a₁ p₁ q₁} {A₁ : Type a₁} (P₁ : Partiality-algebra p₁ q₁ A₁)
         {a₂ p₂ q₂} {A₂ : Type a₂} (P₂ : Partiality-algebra p₂ q₂ A₂) :
         Type (p₁ ⊔ p₂ ⊔ q₁ ⊔ q₂) where
  private
    module P₁ = Partiality-algebra P₁
    module P₂ = Partiality-algebra P₂

  field
    monotone-function : [ P₁ ⟶ P₂ ]⊑

  open [_⟶_]⊑ monotone-function public

  field
    ω-continuous :
      ∀ s → function (P₁.⨆ s) ≡ P₂.⨆ [ monotone-function $ s ]-inc

open [_⟶_]

-- Identity.

idω : ∀ {a p q} {A : Type a} {P : Partiality-algebra p q A} →
      [ P ⟶ P ]
monotone-function idω   = id⊑
ω-continuous      idω _ = refl

-- Composition.

infixr 40 _∘ω_

_∘ω_ :
  ∀ {a₁ p₁ q₁} {A₁ : Type a₁} {P₁ : Partiality-algebra p₁ q₁ A₁}
    {a₂ p₂ q₂} {A₂ : Type a₂} {P₂ : Partiality-algebra p₂ q₂ A₂}
    {a₃ p₃ q₃} {A₃ : Type a₃} {P₃ : Partiality-algebra p₃ q₃ A₃} →
  [ P₂ ⟶ P₃ ] → [ P₁ ⟶ P₂ ] → [ P₁ ⟶ P₃ ]
monotone-function (f ∘ω g) = monotone-function f ∘⊑ monotone-function g

ω-continuous (_∘ω_ {P₁ = P₁} {P₂ = P₂} {P₃ = P₃} f g) s =
  function f (function g (P₁.⨆ s))                             ≡⟨ cong (function f) (ω-continuous g s) ⟩
  function f (P₂.⨆ [ monotone-function g $ s ]-inc)            ≡⟨ ω-continuous f _ ⟩∎
  P₃.⨆ [ monotone-function f ∘⊑ monotone-function g $ s ]-inc  ∎
  where
  module P₁ = Partiality-algebra P₁
  module P₂ = Partiality-algebra P₂
  module P₃ = Partiality-algebra P₃

-- Equality characterisation lemma for ω-continuous functions.

equality-characterisation-continuous :
  ∀ {a₁ p₁ q₁} {A₁ : Type a₁} {P₁ : Partiality-algebra p₁ q₁ A₁}
    {a₂ p₂ q₂} {A₂ : Type a₂} {P₂ : Partiality-algebra p₂ q₂ A₂}
    {f g : [ P₁ ⟶ P₂ ]} →
  (∀ x → function f x ≡ function g x) ↔ f ≡ g
equality-characterisation-continuous {P₁ = P₁} {P₂ = P₂} {f} {g} =
  (∀ x → function f x ≡ function g x)        ↝⟨ equality-characterisation-monotone ⟩
  monotone-function f ≡ monotone-function g  ↝⟨ ignore-propositional-component
                                                  (Π-closure ext 1 λ _ →
                                                   P₂.T-is-set) ⟩
  _↔_.to rearrange f ≡ _↔_.to rearrange g    ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ rearrange) ⟩□
  f ≡ g                                      □
  where
  module P₁ = Partiality-algebra P₁
  module P₂ = Partiality-algebra P₂

  rearrange :
    [ P₁ ⟶ P₂ ]
      ↔
    ∃ λ (h : [ P₁ ⟶ P₂ ]⊑) →
      ∀ s → [_⟶_]⊑.function h (P₁.⨆ s) ≡ P₂.⨆ [ h $ s ]-inc
  rearrange = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ f → monotone-function f , ω-continuous f
        ; from = uncurry λ f c → record { monotone-function = f
                                        ; ω-continuous      = c
                                        }
        }
      ; right-inverse-of = λ _ → refl
      }
    ; left-inverse-of = λ _ → refl
    }
    where
    open Partiality-algebra

-- Composition is associative.

∘ω-assoc :
  ∀ {a₁ p₁ q₁} {A₁ : Type a₁} {P₁ : Partiality-algebra p₁ q₁ A₁}
    {a₂ p₂ q₂} {A₂ : Type a₂} {P₂ : Partiality-algebra p₂ q₂ A₂}
    {a₃ p₃ q₃} {A₃ : Type a₃} {P₃ : Partiality-algebra p₃ q₃ A₃}
    {a₄ p₄ q₄} {A₄ : Type a₄} {P₄ : Partiality-algebra p₄ q₄ A₄}
  (f : [ P₃ ⟶ P₄ ]) (g : [ P₂ ⟶ P₃ ]) (h : [ P₁ ⟶ P₂ ]) →
  f ∘ω (g ∘ω h) ≡ (f ∘ω g) ∘ω h
∘ω-assoc _ _ _ =
  _↔_.to equality-characterisation-continuous λ _ → refl

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Table.Relation.Binary.Equality directly.
------------------------------------------------------------------------

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

module Data.Table.Relation.Equality where

open import Data.Table.Relation.Binary.Equality public