Theorem Struc_univalence (X Y:Struc) : X=Y ≃ X≅Y. Proof. simple refine (@remakeweq _ _ _ _ _). { intermediate_weq (X╝Y). { 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. exists (idpath _). split; apply isrefl_posetRelation. } try reflexivity. intro e. now induction e. Defined.