# Structural equality for GADTs

**URL:** <https://discuss.ocaml.org/t/structural-equality-for-gadts/9104>\
**Category:** Learning\
**Tags:** gadt\
**Created:** [January 5, 2022, 7:39am UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104 "2022-01-05T07:39:20Z")\
**Posts on this page:** 1\
**Showing post:** 17

<div class="post-metadata">

**Author:** ![kantian](https://avatars.discourse-cdn.com/v4/letter/k/4bbf92/32.png) [@kantian](https://discuss.ocaml.org/u/kantian)\
**Post date:** [January 5, 2022, 10:13pm UTC](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104/17 "2022-01-05T22:13:45Z")

</div>

For sure, take your definition:

```ocaml
type wrap = Wrap : 'a -> wrap

```

In the graph of Set category, the constructor `Wrap` is just the label of the arrow that maps any type to the terminal object `wrap`. Up to isomorphism, your type `wrap` could be replaced by `unit` and the arrow is just the polymorphic function `ignore`. The intuition is similar to the one I gave [here](https://discuss.ocaml.org/t/ad-hoc-polymorphism-and-usability/9059/17) with cone and co-cone for type base dynamic dispatch.

---

_[View the full topic](https://discuss.ocaml.org/t/structural-equality-for-gadts/9104)._