# Structure identity

## abstract the proof of Poset_rect for use in multiple situations

See Section 9.8 of the HoTT book, on "The structure identity principle".

Open Scope poset.

Context {Base : UU}
(Data : Base Poset).
Definition Struc := b, Data b.
for example: Base = hSet, Data = PartialOrder, Struc = Poset

Local Definition DataEquiv (b:Base) (d d':Data b) := d d' d' d.

Local Definition StrucEquiv (X Y:Struc)
:= (p: pr1 X = pr1 Y), DataEquiv _ (transportf Data p (pr2 X)) (pr2 Y).

Notation "X ≅ Y" := (StrucEquiv X Y).

Theorem Struc_univalence (X Y:Struc) : X=Y XY.
Proof.
simple refine (@remakeweq _ _ _ _ _).
{ intermediate_weq (XY).
{ apply total2_paths_equiv'. }
{ use weqfibtototal; intro p. apply weqimplimpl.
{ intros q. split; induction q; apply isrefl_posetRelation. }
{ intros e. apply isantisymm_posetRelation.
- exact (pr1 e).
- exact (pr2 e). }
{ apply (setproperty (Data _)). }
{ apply (propproperty (DataEquiv _ _ _)). } } }
{ intros e. induction e. (idpath _). split; apply isrefl_posetRelation. }
try reflexivity.     intro e. now induction e.
Defined.

Theorem Equiv_rect (X Y : Struc) (P : X Y UU) :
( e : X = Y, P (Struc_univalence _ _ e)) f, P f.
Proof.
intros ih f.
set (p := ih (invmap (Struc_univalence _ _) f)).
set (h := homotweqinvweq (Struc_univalence _ _) f).
exact (transportf P h p).
Defined.

End StructureIdentity.