Definition istrans2 {X:hSet} (le lt:hrel X) := ∑ transltle: ∏ x y z, lt x y -> le y z -> lt x z, ∑ translelt: ∏ x y z, le x y -> lt y z -> lt x z, unit.
Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.OrderTheory.Posets.Examples.StandardFiniteSet.