Library UniMath.CategoryTheory.DisplayedCats.SIP


The Structure Identity Principle

A short proof of the SIP (HoTT book, chapter 9.8)

Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Univalence.
Local Open Scope cat.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.

Local Open Scope mor_disp_scope.

The Structure Identity Principle


Section SIP.

The data and properties according to HoTT book, chapter 9.8


Variable C : category.
Variable univC : is_univalent C.
Variable P : ob C -> UU.
Variable Pisset : ∏ x, isaset (P x).
Variable H : ∏ (x y : C), P x → P y → C⟦x,y⟧ → UU.
Arguments H {_ _} _ _ _ .
Variable Hisprop : ∏ x y a b (f : C⟦x,y⟧), isaprop (H a b f).
Variable Hid : ∏ (x : C) (a : P x), H a a (identity _ ).
Variable Hcomp : ∏ (x y z : C) a b c (f : C⟦x,y⟧) (g : C⟦y,z⟧),
                 H a b f → H b c g → H a c (f · g).
Variable Hstandard : ∏ (x : C) (a a' : P x),
                     H a a' (identity _ ) → H a' a (identity _ ) → a = a'.

A displayed precategory from the data


Definition disp_cat_from_SIP_data : disp_cat C
  := disp_struct C P (@H) Hisprop Hid Hcomp.

Displayed category from SIP data is univalent


Lemma is_univalent_disp_from_SIP_data : is_univalent_disp disp_cat_from_SIP_data.
Show proof.
  apply is_univalent_disp_from_fibers.
  intros x a b.
  apply isweqimplimpl.
  - intro i. apply Hstandard.
    * apply i.
    * apply (inv_mor_disp_from_z_iso i).
  - apply Pisset.
  - apply isofhleveltotal2.
    + apply Hisprop.
    + intro. apply (@isaprop_is_z_iso_disp _ disp_cat_from_SIP_data).

The conclusion of SIP: total category is univalent


Definition SIP : is_univalent (total_category disp_cat_from_SIP_data).
Show proof.
  apply is_univalent_total_category.
  - apply univC.
  - apply is_univalent_disp_from_SIP_data.

End SIP.

TODO: add some examples