------------------------------------------------------------------------
-- Partiality algebra categories
------------------------------------------------------------------------

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

module Partiality-algebra.Category where

open import Equality.Propositional
open import Interval using (ext; ⟨ext⟩; bad-ext)
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as Bijection using (_↔_)
open import Category equality-with-J as Category
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J hiding (Type)
open import H-level.Closure equality-with-J
open import Structure-identity-principle equality-with-J
open import Univalence-axiom equality-with-J

open import Partiality-algebra as PA hiding (id; _∘_)

------------------------------------------------------------------------
-- Equality characterisation lemmas for Partiality-algebra-with

abstract

  -- An equality characterisation lemma for Partiality-algebra-with.

  equality-characterisation-Partiality-algebra-with₁ :
     {a p q} {A : Set a} {Type : Set p}
      {P₁ P₂ : Partiality-algebra-with Type q A} 
    let module P₁ = Partiality-algebra-with P₁
        module P₂ = Partiality-algebra-with P₂
    in
    ( λ (⊑≡⊑ :  x y  (x P₁.⊑ y)  (x P₂.⊑ y)) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s  P₂.⨆ (Σ-map id (≡⇒→ (⊑≡⊑ _ _) ∘_) s))
      
    P₁  P₂
  equality-characterisation-Partiality-algebra-with₁
    {q = q} {A} {Type} {P₁} {P₂} =

    ( λ (⊑≡⊑ :  x y  (x P₁.⊑ y)  (x P₂.⊑ y)) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s  P₂.⨆ (Σ-map id (≡⇒→ (⊑≡⊑ _ _) ∘_) s))              ↝⟨ ∃-cong  ⊑≡⊑  ∃-cong λ _  ∃-cong λ _  ∀-cong ext λ s 
                                                                              ≡⇒↝ _ $ cong  (p : {f :   Type}  _) 
                                                                                              P₁.⨆ s  P₂.⨆ (Σ-map id p s)) $
                                                                                _⇔_.to propositional⇔irrelevant
                                                                                  (implicit-Π-closure ext 1 λ _ 
                                                                                   Π-closure          ext 1 λ _ 
                                                                                   Π-closure          ext 1 λ _ 
                                                                                   P₂.⊑-propositional)
                                                                                  (≡⇒→ (⊑≡⊑ _ _) ∘_)
                                                                                   {f}  ≡⇒→ (cong  _⊑_   n  f n  f (suc n))
                                                                                                     (⟨ext⟩ (⟨ext⟩  ⊑≡⊑))))) 
    ( λ (⊑≡⊑ :  x y  (x P₁.⊑ y)  (x P₂.⊑ y)) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s 
             P₂.⨆ (Σ-map id
                          {f} 
                            ≡⇒→ (cong  _⊑_   n  f n  f (suc n))
                                      (⟨ext⟩ (⟨ext⟩  ⊑≡⊑))))
                         s))                                             ↝⟨ Σ-cong (∀-cong ext λ _ 
                                                                                    Eq.extensionality-isomorphism bad-ext)  _  F.id) 
    ( λ (⊑≡⊑ :  x  P₁._⊑_ x  P₂._⊑_ x) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s 
             P₂.⨆ (Σ-map id
                          {f} 
                            ≡⇒→ (cong  _⊑_   n  f n  f (suc n))
                                      (⟨ext⟩ ⊑≡⊑)))
                         s))                                             ↝⟨ Σ-cong (Eq.extensionality-isomorphism bad-ext)  _  F.id) 

    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s 
             P₂.⨆ (Σ-map id
                          {f} 
                            ≡⇒→ (cong  _⊑_   n  f n  f (suc n))
                                      ⊑≡⊑))
                         s))                                             ↔⟨⟩

    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s 
             P₂.⨆ ( proj₁ s
                  , ≡⇒→ (cong  _⊑_ 
                                  n  proj₁ s n  proj₁ s (suc n))
                              ⊑≡⊑)
                        (proj₂ s)
                  ))                                                     ↝⟨ ∃-cong  ⊑≡⊑  ∃-cong λ _  ∃-cong λ _  ∀-cong ext λ _ 
                                                                              ≡⇒↝ _ $ cong  eq  _  P₂.⨆ (_ , ≡⇒→ eq _)) $ sym $
                                                                                cong-∘ _ _ ⊑≡⊑) 
    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s 
             P₂.⨆ ( proj₁ s
                  , ≡⇒→ (cong (uncurry λ _⊑_ (f :   Type) 
                                          n  f n  f (suc n))
                              (cong (_, _) ⊑≡⊑))
                        (proj₂ s)
                  ))                                                     ↝⟨ ∃-cong  ⊑≡⊑  ∃-cong λ _  ∃-cong λ _  ∀-cong ext λ _ 
                                                                              ≡⇒↝ _ $ cong  inc  _  P₂.⨆ (_ , inc)) $ sym $
                                                                                subst-in-terms-of-≡⇒↝ equivalence (cong (_, _) ⊑≡⊑) _ _) 
    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s 
             P₂.⨆ ( proj₁ s
                  , subst (uncurry λ _⊑_ (f :   Type) 
                                      n  f n  f (suc n))
                          (cong (_, _) ⊑≡⊑)
                          (proj₂ s)
                  ))                                                     ↝⟨ ∃-cong  ⊑≡⊑  ∃-cong λ _  ∃-cong λ _  ∀-cong ext λ _ 
                                                                              ≡⇒↝ _ $ cong  eq  _ 
                                                                                                   P₂.⨆ (_ , subst (uncurry λ _⊑_ (f :   Type) 
                                                                                                                               n  f n  f (suc n))
                                                                                                                   eq _)) $ sym $
                                                                                Σ-≡,≡→≡-subst-const ⊑≡⊑ refl) 
    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s 
             P₂.⨆ ( proj₁ s
                  , subst (uncurry λ _⊑_ (f :   Type) 
                                      n  f n  f (suc n))
                          (Σ-≡,≡→≡ ⊑≡⊑ (subst-const ⊑≡⊑))
                          (proj₂ s)
                  ))                                                     ↝⟨ ∃-cong  ⊑≡⊑  ∃-cong λ _  ∃-cong λ _  ∀-cong ext λ _ 
                                                                              ≡⇒↝ _ $ cong  s  _  P₂.⨆ s) $ sym $
                                                                                push-subst-pair′ {y≡z = ⊑≡⊑} _ _ (subst-const ⊑≡⊑)) 
    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s 
             P₂.⨆ (subst  _⊑_   λ f   n  f n  f (suc n))
                         ⊑≡⊑ s))                                         ↝⟨ ∃-cong  ⊑≡⊑  ∃-cong λ _  ∃-cong λ _  ∀-cong ext λ _ 
                                                                              ≡⇒↝ _ $ cong  eq  _ 
                                                                                                   P₂.⨆ (subst  _⊑_   λ f   n 
                                                                                                                          f n  f (suc n)) eq _)) $
                                                                                sym $ sym-sym ⊑≡⊑) 
    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s 
             P₂.⨆ (subst  _⊑_   λ f   n  f n  f (suc n))
                         (sym (sym ⊑≡⊑)) s))                             ↝⟨ ∃-cong  ⊑≡⊑  ∃-cong λ _  ∃-cong λ _  ∀-cong ext λ _ 
                                                                              ≡⇒↝ _ $ cong  f  _  f _) $ sym $
                                                                                subst-→-domain _ (sym ⊑≡⊑)) 
    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s 
             subst  _⊑_    f   n  f n  f (suc n))  Type)
                   (sym ⊑≡⊑) P₂.⨆ s)                                     ↔⟨ ∃-cong  _  ∃-cong λ _ 
                                                                              Eq.extensionality-isomorphism ext
                                                                                ×-cong
                                                                              Eq.extensionality-isomorphism ext) 
    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       P₁.never  P₂.never
         ×
       P₁.now  P₂.now
         ×
       P₁.⨆  subst _ (sym ⊑≡⊑) P₂.⨆)                                    ↝⟨ ∃-cong  ⊑≡⊑  ∃-cong λ _  ∃-cong λ _ 
                                                                              ≡⇒↝ _ $ elim  ⊑≡⊑   {⨆₁ ⨆₂} 
                                                                                              (⨆₁  subst _ (sym ⊑≡⊑) ⨆₂) 
                                                                                              (subst _ ⊑≡⊑ ⨆₁  ⨆₂))
                                                                                            _  refl) ⊑≡⊑) 
    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       P₁.never  P₂.never
         ×
       P₁.now  P₂.now
         ×
       subst _ ⊑≡⊑ P₁.⨆  P₂.⨆)                                          ↝⟨ ∃-cong  ⊑≡⊑ 
                                                                              ≡⇒↝ _ (cong (_≡ _) $ sym $ subst-const ⊑≡⊑)
                                                                                ×-cong
                                                                              ≡⇒↝ _ (cong (_≡ _) $ sym $ subst-const ⊑≡⊑)
                                                                                ×-cong
                                                                              F.id) 
    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       subst _ ⊑≡⊑ P₁.never  P₂.never
         ×
       subst _ ⊑≡⊑ P₁.now  P₂.now
         ×
       subst _ ⊑≡⊑ P₁.⨆  P₂.⨆)                                          ↝⟨ ∃-cong  _  ∃-cong λ _  ≡×≡↔≡) 

    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       subst _ ⊑≡⊑ P₁.never  P₂.never
         ×
       (subst _ ⊑≡⊑ P₁.now , subst _ ⊑≡⊑ P₁.⨆) 
       (P₂.now , P₂.⨆))                                                  ↝⟨ ∃-cong  _  ≡×≡↔≡) 

    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       (subst _ ⊑≡⊑ P₁.never , subst _ ⊑≡⊑ P₁.now , subst _ ⊑≡⊑ P₁.⨆) 
       (P₂.never , P₂.now , P₂.⨆))                                       ↝⟨ ∃-cong  ⊑≡⊑  ≡⇒↝ _ $ cong  x  (subst _ ⊑≡⊑ P₁.never , x)  _) $
                                                                              sym $ push-subst-, {y≡z = ⊑≡⊑} _
                                                                                                  _⊑_  ( λ f   n  f n  f (suc n))  _)) 
    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       (subst _ ⊑≡⊑ P₁.never , subst _ ⊑≡⊑ (P₁.now , P₁.⨆)) 
       (P₂.never , P₂.now , P₂.⨆))                                       ↝⟨ ∃-cong  ⊑≡⊑  ≡⇒↝ _ $ cong (_≡ _) $ sym $
                                                                              push-subst-, {y≡z = ⊑≡⊑} _ _) 
    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       subst _ ⊑≡⊑ (P₁.never , P₁.now , P₁.⨆) 
       (P₂.never , P₂.now , P₂.⨆))                                       ↔⟨⟩

    ( λ (⊑≡⊑ : P₁._⊑_  P₂._⊑_) 
       subst _ ⊑≡⊑ (proj₂ (proj₁ (_↔_.to rearrange P₁))) 
       proj₂ (proj₁ (_↔_.to rearrange P₂)))                              ↝⟨ Bijection.Σ-≡,≡↔≡ 

    proj₁ (_↔_.to rearrange P₁)  proj₁ (_↔_.to rearrange P₂)            ↝⟨ ignore-propositional-component
                                                                              (×-closure 1 (implicit-Π-closure ext 1 λ _ 
                                                                                            implicit-Π-closure ext 1 λ _ 
                                                                                            Π-closure ext 1 λ _ 
                                                                                            Π-closure ext 1 λ _ 
                                                                                            P₂.Type-is-set _ _) $
                                                                               ×-closure 1 (UIP-propositional ext) $
                                                                               ×-closure 1 (Π-closure ext 1 λ _ 
                                                                                            P₂.⊑-propositional) $
                                                                               ×-closure 1 (implicit-Π-closure ext 1 λ _ 
                                                                                            implicit-Π-closure ext 1 λ _ 
                                                                                            implicit-Π-closure ext 1 λ _ 
                                                                                            Π-closure ext 1 λ _ 
                                                                                            Π-closure ext 1 λ _ 
                                                                                            P₂.⊑-propositional) $
                                                                               ×-closure 1 (Π-closure ext 1 λ _ 
                                                                                            P₂.⊑-propositional) $
                                                                               ×-closure 1 (Π-closure ext 1 λ _ 
                                                                                            Π-closure ext 1 λ _ 
                                                                                            P₂.⊑-propositional) $
                                                                               ×-closure 1 (Π-closure ext 1 λ _ 
                                                                                            Π-closure ext 1 λ _ 
                                                                                            Π-closure ext 1 λ _ 
                                                                                            P₂.⊑-propositional)
                                                                                           (implicit-Π-closure ext 1 λ _ 
                                                                                            implicit-Π-closure ext 1 λ _ 
                                                                                            Proof-irrelevant-propositional ext)) 
    _↔_.to rearrange P₁  _↔_.to rearrange P₂                            ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ rearrange) ⟩□

    P₁  P₂                                                              
    where
    module P₁ = Partiality-algebra-with P₁
    module P₂ = Partiality-algebra-with P₂

    rearrange :
      Partiality-algebra-with Type q A
        
       λ R 
        let _⊑_ : Type  Type  Set q
            _⊑_ = proj₁ R

            never : Type
            never = proj₁ (proj₂ R)

            now : A  Type
            now = proj₁ (proj₂ (proj₂ R))

             : ( λ (f :   Type)   n  f n  f (suc n))  Type
             = proj₂ (proj₂ (proj₂ R))
        in
        (∀ {x y}  x  y  y  x  x  y)
          ×
        Uniqueness-of-identity-proofs Type
          ×
        (∀ x  x  x)
          ×
        (∀ {x y z}  x  y  y  z  x  z)
          ×
        (∀ x  never  x)
          ×
        (∀ s   n  proj₁ s n   s)
          ×
        (∀ s ub  (∀ n  proj₁ s n  ub)   s  ub)
          ×
        (∀ {x y}  Proof-irrelevant (x  y))
    rearrange = record
      { surjection = record
        { logical-equivalence = record
          { to   = λ P  let open Partiality-algebra-with P in
                    ( _⊑_
                    , never
                    , now
                    , 
                    )
                  , antisymmetry
                  , Type-UIP-unused
                  , ⊑-refl
                  , ⊑-trans
                  , never⊑
                  , upper-bound
                  , least-upper-bound
                  , ⊑-proof-irrelevant
          ; from = λ where
              ((LE , ne , n , l) , a , u , r , t , le , ub , lub , p) 
                record
                  { _⊑_                = LE
                  ; never              = ne
                  ; now                = n
                  ;                   = l
                  ; antisymmetry       = a
                  ; Type-UIP-unused    = u
                  ; ⊑-refl             = r
                  ; ⊑-trans            = t
                  ; never⊑             = le
                  ; upper-bound        = ub
                  ; least-upper-bound  = lub
                  ; ⊑-proof-irrelevant = p
                  }
          }
        ; right-inverse-of = λ _  refl
        }
      ; left-inverse-of = λ _  refl
      }

  -- Another equality characterisation lemma for
  -- Partiality-algebra-with.

  equality-characterisation-Partiality-algebra-with₂ :
     {a p q} {A : Set a} {Type : Set p}
      {P₁ P₂ : Partiality-algebra-with Type q A} 

    Propositional-extensionality q 

    let module P₁ = Partiality-algebra-with P₁
        module P₂ = Partiality-algebra-with P₂
    in
    ( λ (⊑⇔⊑ :  x y  x P₁.⊑ y  x P₂.⊑ y) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s  P₂.⨆ (Σ-map id (_⇔_.to (⊑⇔⊑ _ _) ∘_) s))
      
    P₁  P₂
  equality-characterisation-Partiality-algebra-with₂
    {q = q} {A} {Type} {P₁} {P₂} prop-ext =

    ( λ (⊑⇔⊑ :  x y  x P₁.⊑ y  x P₂.⊑ y) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s  P₂.⨆ (Σ-map id (_⇔_.to (⊑⇔⊑ _ _) ∘_) s))  ↝⟨ Σ-cong (∀-cong ext λ _  ∀-cong ext λ _ 
                                                                             Eq.⇔↔≃ ext P₁.⊑-propositional P₂.⊑-propositional)
                                                                           _  F.id) 
    ( λ (⊑≃⊑ :  x y  (x P₁.⊑ y)  (x P₂.⊑ y)) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s  P₂.⨆ (Σ-map id (_≃_.to (⊑≃⊑ _ _) ∘_) s))  ↝⟨ inverse $ Σ-cong
                                                                     (∀-cong ext λ _  ∀-cong ext λ _ 
                                                                        ≡≃≃ (_≃_.to
                                                                               (Propositional-extensionality-is-univalence-for-propositions
                                                                                  ext)
                                                                               prop-ext
                                                                               P₁.⊑-propositional
                                                                               P₂.⊑-propositional))
                                                                      _  F.id) 
    ( λ (⊑≡⊑ :  x y  (x P₁.⊑ y)  (x P₂.⊑ y)) 
       P₁.never  P₂.never
         ×
       (∀ x  P₁.now x  P₂.now x)
         ×
        s  P₁.⨆ s  P₂.⨆ (Σ-map id (≡⇒→ (⊑≡⊑ _ _) ∘_) s))     ↝⟨ equality-characterisation-Partiality-algebra-with₁ ⟩□

    P₁  P₂                                                     
    where
    module P₁ = Partiality-algebra-with P₁
    module P₂ = Partiality-algebra-with P₂

------------------------------------------------------------------------
-- Partiality algebra categories

-- Partiality algebras (with fixed levels and types) form
-- precategories.

precategory :
   {a} p q (A : Set a)  Precategory (a  lsuc (p  q)) (a  p  q)
Precategory.precategory (precategory p q A) =
    Partiality-algebra p q A
  ,  P Q  Morphism P Q , Morphism-set)
  , PA.id
  , PA._∘_
  , _↔_.to equality-characterisation-Morphism refl
  , _↔_.to equality-characterisation-Morphism refl
  , _↔_.to equality-characterisation-Morphism refl

-- A "standard notion of structure" built using
-- Partiality-algebra-with (and propositional extensionality).

standard-notion-of-structure :
   {a} p {q} (A : Set a) 
  Propositional-extensionality q 
  Standard-notion-of-structure _ _ (precategory-Set p ext)
standard-notion-of-structure p {q} A prop-ext = record
  { P               = λ B  Partiality-algebra-with (proj₁ B) q A
  ; H               = Is-morphism-with
  ; H-prop          = λ { {p = P} {q = Q} _ 
                          Is-morphism-with-propositional P Q
                        }
  ; H-id            = λ { {p = P} 
                          proj₂ $
                            _↔_.to Morphism↔Morphism-as-Σ
                              (PA.id {P =  P })
                        }
  ; H-∘             = λ { {p = P} {q = Q} {r = R}
                          f-morphism g-morphism 
                          proj₂ $
                            _↔_.to Morphism↔Morphism-as-Σ
                              (_↔_.from
                                 (Morphism↔Morphism-as-Σ
                                    {P₁ =  Q } {P₂ =  R })
                                 (_ , g-morphism)
                                 PA.∘
                               _↔_.from
                                 (Morphism↔Morphism-as-Σ {P₁ =  P })
                                 (_ , f-morphism))
                        }
  ; H-antisymmetric = λ P Q id-morphism-P→Q id-morphism-Q→P 
      _↔_.to
        (equality-characterisation-Partiality-algebra-with₂ prop-ext)
        (  x y  record { to   = proj₁ id-morphism-P→Q
                          ; from = proj₁ id-morphism-Q→P
                          })
        , proj₁ (proj₂ id-morphism-P→Q)
        , proj₁ (proj₂ (proj₂ id-morphism-P→Q))
        , proj₂ (proj₂ (proj₂ id-morphism-P→Q))
        )
  }

abstract

  -- The precategory obtained from the standard notion of structure is
  -- equal to the direct definition above (assuming univalence).

  precategories-equal :
     {a p q} {A : Set a} 
    Univalence (a  lsuc (p  q)) 
    Univalence (a  p  q) 
    (prop-ext : Propositional-extensionality q) 
    Standard-notion-of-structure.Str
      (standard-notion-of-structure p A prop-ext)
      
    precategory p q A
  precategories-equal {p = p} {q} {A} univ₁ univ₂ prop-ext =
    _↔_.to (equality-characterisation-Precategory ext univ₁ univ₂)
      ( ≃Partiality-algebra
      ,  _ _  Eq.↔⇒≃ $ inverse $ Morphism↔Morphism-as-Σ)
      ,  _  refl)
      ,  _ _ _ _ _  refl)
      )
    where
    ≃Partiality-algebra :
      ( λ (Type : SET p)  Partiality-algebra-with (proj₁ Type) q A)
        
      Partiality-algebra p q A
    ≃Partiality-algebra =
      ( λ (Type : SET p)  Partiality-algebra-with (proj₁ Type) q A)  ↔⟨ inverse Σ-assoc 

      ( λ (Type : Set p) 
         Is-set Type × Partiality-algebra-with Type q A)               ↔⟨ ∃-cong  _  drop-⊤-left-× λ P  _⇔_.to contractible⇔↔⊤ $
                                                                            propositional⇒inhabited⇒contractible
                                                                              (H-level-propositional ext 2)
                                                                              (Partiality-algebra-with.Type-is-set P)) 
      ( λ (Type : Set p)  Partiality-algebra-with Type q A)          ↝⟨ Eq.↔⇒≃ record
                                                                            { surjection = record
                                                                              { logical-equivalence = record
                                                                                { to   = uncurry λ _ P   P 
                                                                                ; from = λ P  Type P , partiality-algebra-with P
                                                                                }
                                                                              ; right-inverse-of = λ _  refl
                                                                              }
                                                                            ; left-inverse-of = λ _  refl
                                                                            } ⟩□
      Partiality-algebra p q A                                         
      where
      open Partiality-algebra

-- Thus the precategory is a category (assuming univalence and
-- propositional extensionality).

category :
   {a p q} (A : Set a) 
  Univalence (a  lsuc (p  q)) 
  Univalence (a  p  q) 
  Univalence p 
  Propositional-extensionality q 
  Category (a  lsuc (p  q)) (a  p  q)
Category.category (category A univ₁ univ₂ univ₃ prop-ext) =
    precategory _ _ A
  , subst  C   {P Q}  Eq.Is-equivalence
                             (Precategory.≡→≅ C {P} {Q}))
          (precategories-equal univ₁ univ₂ prop-ext)
          (structure-identity-principle
             ext
             (category-Set _ ext  _ _  univ₃))
             (standard-notion-of-structure _ A prop-ext))

private

  precategory-category :
     {a p} {q} {A : Set a}
      {univ₁ : Univalence (a  lsuc (p  q))}
      {univ₂ : Univalence (a  p  q)}
      {univ₃ : Univalence p}
      {prop-ext : Propositional-extensionality q} 
    Category.precategory (category A univ₁ univ₂ univ₃ prop-ext) 
    precategory p q A
  precategory-category = refl