```------------------------------------------------------------------------
-- The Agda standard library
--
-- Homogeneously-indexed binary relations
------------------------------------------------------------------------

-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Homogeneous`.

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary.Indexed.Homogeneous.Core

module Relation.Binary.Indexed.Homogeneous.Structures
{i a ℓ} {I : Set i}
(A : I → Set a)   -- The underlying indexed sets
(_≈ᵢ_ : IRel A ℓ) -- The underlying indexed equality relation
where

open import Data.Product.Base using (_,_)
open import Function.Base using (_⟨_⟩_)
open import Level using (Level; _⊔_; suc)
open import Relation.Binary.Core using (_⇒_)
import Relation.Binary.Definitions as B
import Relation.Binary.Structures as B
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
open import Relation.Binary.Indexed.Homogeneous.Definitions

------------------------------------------------------------------------
-- Equivalences

-- Indexed structures are laid out in a similar manner as to those
-- in Relation.Binary. The main difference is each structure also
-- contains proofs for the lifted version of the relation.

record IsIndexedEquivalence : Set (i ⊔ a ⊔ ℓ) where
field
reflᵢ  : Reflexive  A _≈ᵢ_
symᵢ   : Symmetric  A _≈ᵢ_
transᵢ : Transitive A _≈ᵢ_

reflexiveᵢ : ∀ {i} → _≡_ ⟨ _⇒_ ⟩ _≈ᵢ_ {i}
reflexiveᵢ P.refl = reflᵢ

-- Lift properties

reflexive : _≡_ ⇒ (Lift A _≈ᵢ_)
reflexive P.refl i = reflᵢ

refl : B.Reflexive (Lift A _≈ᵢ_)
refl i = reflᵢ

sym : B.Symmetric (Lift A _≈ᵢ_)
sym x≈y i = symᵢ (x≈y i)

trans : B.Transitive (Lift A _≈ᵢ_)
trans x≈y y≈z i = transᵢ (x≈y i) (y≈z i)

isEquivalence : B.IsEquivalence (Lift A _≈ᵢ_)
isEquivalence = record
{ refl  = refl
; sym   = sym
; trans = trans
}

record IsIndexedDecEquivalence : Set (i ⊔ a ⊔ ℓ) where
infix 4 _≟ᵢ_
field
_≟ᵢ_           : Decidable A _≈ᵢ_
isEquivalenceᵢ : IsIndexedEquivalence

open IsIndexedEquivalence isEquivalenceᵢ public

------------------------------------------------------------------------
-- Preorders

record IsIndexedPreorder {ℓ₂} (_∼ᵢ_ : IRel A ℓ₂)
: Set (i ⊔ a ⊔ ℓ ⊔ ℓ₂) where
field
isEquivalenceᵢ : IsIndexedEquivalence
reflexiveᵢ     : _≈ᵢ_ ⇒[ A ] _∼ᵢ_
transᵢ         : Transitive A _∼ᵢ_

module Eq = IsIndexedEquivalence isEquivalenceᵢ

reflᵢ : Reflexive A _∼ᵢ_
reflᵢ = reflexiveᵢ Eq.reflᵢ

∼ᵢ-respˡ-≈ᵢ : Respectsˡ A _∼ᵢ_ _≈ᵢ_
∼ᵢ-respˡ-≈ᵢ x≈y x∼z = transᵢ (reflexiveᵢ (Eq.symᵢ x≈y)) x∼z

∼ᵢ-respʳ-≈ᵢ : Respectsʳ A _∼ᵢ_ _≈ᵢ_
∼ᵢ-respʳ-≈ᵢ x≈y z∼x = transᵢ z∼x (reflexiveᵢ x≈y)

∼ᵢ-resp-≈ᵢ : Respects₂ A _∼ᵢ_ _≈ᵢ_
∼ᵢ-resp-≈ᵢ = ∼ᵢ-respʳ-≈ᵢ , ∼ᵢ-respˡ-≈ᵢ

-- Lifted properties

reflexive : Lift A _≈ᵢ_ ⇒ Lift A _∼ᵢ_
reflexive x≈y i = reflexiveᵢ (x≈y i)

refl : B.Reflexive (Lift A _∼ᵢ_)
refl i = reflᵢ

trans : B.Transitive (Lift A _∼ᵢ_)
trans x≈y y≈z i = transᵢ (x≈y i) (y≈z i)

∼-respˡ-≈ : (Lift A _∼ᵢ_) B.Respectsˡ (Lift A _≈ᵢ_)
∼-respˡ-≈ x≈y x∼z i = ∼ᵢ-respˡ-≈ᵢ (x≈y i) (x∼z i)

∼-respʳ-≈ : (Lift A _∼ᵢ_) B.Respectsʳ (Lift A _≈ᵢ_)
∼-respʳ-≈ x≈y z∼x i = ∼ᵢ-respʳ-≈ᵢ (x≈y i) (z∼x i)

∼-resp-≈ : (Lift A _∼ᵢ_) B.Respects₂ (Lift A _≈ᵢ_)
∼-resp-≈ = ∼-respʳ-≈ , ∼-respˡ-≈

isPreorder : B.IsPreorder (Lift A _≈ᵢ_) (Lift A _∼ᵢ_)
isPreorder = record
{ isEquivalence = Eq.isEquivalence
; reflexive     = reflexive
; trans         = trans
}

------------------------------------------------------------------------
-- Partial orders

record IsIndexedPartialOrder {ℓ₂} (_≤ᵢ_ : IRel A ℓ₂)
: Set (i ⊔ a ⊔ ℓ ⊔ ℓ₂) where
field
isPreorderᵢ : IsIndexedPreorder _≤ᵢ_
antisymᵢ    : Antisymmetric A _≈ᵢ_ _≤ᵢ_

open IsIndexedPreorder isPreorderᵢ public
renaming
( ∼ᵢ-respˡ-≈ᵢ to ≤ᵢ-respˡ-≈ᵢ
; ∼ᵢ-respʳ-≈ᵢ to ≤ᵢ-respʳ-≈ᵢ
; ∼ᵢ-resp-≈ᵢ  to ≤ᵢ-resp-≈ᵢ
; ∼-respˡ-≈   to ≤-respˡ-≈
; ∼-respʳ-≈   to ≤-respʳ-≈
; ∼-resp-≈    to ≤-resp-≈
)

antisym : B.Antisymmetric (Lift A _≈ᵢ_) (Lift A _≤ᵢ_)
antisym x≤y y≤x i = antisymᵢ (x≤y i) (y≤x i)

isPartialOrder : B.IsPartialOrder (Lift A _≈ᵢ_) (Lift A _≤ᵢ_)
isPartialOrder = record
{ isPreorder = isPreorder
; antisym    = antisym
}
```