# Towards a general proof type

**URL:** <https://forum.anoma.net/t/towards-a-general-proof-type/732>\
**Category:** Protocol Design\
**Created:** [August 19, 2024, 1:06pm UTC](https://forum.anoma.net/t/towards-a-general-proof-type/732 "2024-08-19T13:06:32Z")\
**Posts on this page:** 1\
**Showing post:** 21

<div class="post-metadata">

**Author:** ![terence](https://avatars.discourse-cdn.com/v4/letter/t/aca169/32.png) [@terence](https://forum.anoma.net/u/terence)\
**Post date:** [August 27, 2024, 4:58pm UTC](https://forum.anoma.net/t/towards-a-general-proof-type/732/21 "2024-08-27T16:58:18Z")

</div>

I do not know enough about ZK proofs to say what it takes to represent them, but using (co)equality types (i.e. pushouts and pullbacks rather than just coproducts and products) as our basic types as described in [Data & function encoding - #18 by terence](https://forum.anoma.net/t/data-function-encoding/719/18) would allow some examples of the above. In particular, for example, global elements (morphisms from the terminal object) into equalizers correspond to:

> “trivial proofs” where verifying the proof requires simply computing the function

---

_[View the full topic](https://forum.anoma.net/t/towards-a-general-proof-type/732)._