sstucki

-- In response to https://lists.chalmers.se/pipermail/agda/2017/009872.html
module _ where

open import Data.Product using (proj₁; proj₂)
open import Level using (suc; _⊔_)
open import Relation.Binary


------------------------------------------------------------------------
-- Transitive relations that are not necessarily reflexive

sstucki

-- An attempt to implement implicit coercions via Agda's instance
-- argument resolution.  The basic principle works, but Agda's
-- instance resolution is a bit too weak to scale it to big examples
-- because it is hard to implement chains of coercions.

-- Doesn't help: {-# OPTIONS --overlapping-instances #-}

record Coercion {a} (x y : Set a) : Set a where
  constructor ⌞_⌟
  field coe : x → y