min.agda

{-# OPTIONS --without-K --exact-split --safe #-}

Rel : Set -> Set1
Rel A = A -> A -> Set

-- Some properties
record Reflexive {A : Set} (R : Rel A) : Set where
    field refl : (a : A) -> (R a a)

record Symmetric {A : Set} (R : Rel A) : Set where
    field sym : (a b : A) -> (R a b) -> (R b a)

record Transitive {A : Set} (R : Rel A) : Set where
    field trans : (a b c : A) -> (R a b) -> (R b c) -> (R a c)

record Equivalent {A : Set} (R : Rel A) : Set where
    field
        {{refl}} : Reflexive {A} R
        {{sym}} : Symmetric {A} R
        {{trans}} : Transitive {A} R
open Equivalent {{...}}

data I {A : Set} : Rel A where
    I-refl : (a : A) -> I a a

_==_ : {A : Set} -> A -> A -> Set
x == y = I x y

J : {A : Set} -> {a b : A} -> (C : (a b : A) -> I a b -> Set) -> (c : I a b) -> C a a (I-refl a) -> C a b c
J _ (I-refl a) d = d

I-sym : {A : Set} -> (a b : A) -> (a == b) -> (b == a)
I-sym a b p = J C p (I-refl a)
    where C = \a b r -> I b a

I-trans : {A : Set} -> (a b c : A) -> (I a b) -> (I b c) -> (I a c)
I-trans a b c p q = J C q p
    where C = \b c r -> I a c

instance
    I-reflexivity : {A : Set} -> Reflexive {A} I
    I-reflexivity = record {refl = I-refl}
    
    I-symmetry : {A : Set} -> Symmetric {A} I
    I-symmetry = record {sym = I-sym}
    
    I-transitivity : {A : Set} -> Transitive {A} I
    I-transitivity = record {trans = I-trans}
    
    I-equivalence : {A : Set} -> Equivalent {A} I
    refl {{I-equivalence}} = I-refl
    sym {{I-equivalence}} = I-sym
    trans {{I-equivalence}} = I-trans