# \#cic

**URL:** https://discourse.rocq-prover.org/tag/cic/5.md

[Latest](https://discourse.rocq-prover.org/latest.md) · [Categories](https://discourse.rocq-prover.org/categories.md) · [Tags](https://discourse.rocq-prover.org/tags.md)

---

## [Comparing Coq (pCUIC) with HoTT and CubicalTT for common verification tasks](https://discourse.rocq-prover.org/t/comparing-coq-pcuic-with-hott-and-cubicaltt-for-common-verification-tasks/598)

<div class="topic-metadata">

**Author:** [@palmskog](https://discourse.rocq-prover.org/u/palmskog)\
**Replies:** 4\
**Last updated:** [February 12, 2020, 3:37pm UTC](https://discourse.rocq-prover.org/t/comparing-coq-pcuic-with-hott-and-cubicaltt-for-common-verification-tasks/598 "2020-02-12T15:37:04Z")

</div>

Homotopy type theory (HoTT) and Cubical type theory (CubicalTT) have been used to formalize foundations of mathematics, and have inspired extensions to Coq such as SProp. However, demonstrated applications of HoTT and C…

---

## [Why is η-reduction illegal?](https://discourse.rocq-prover.org/t/why-is-reduction-illegal/345)

<div class="topic-metadata">

**Author:** [@neshkeev](https://discourse.rocq-prover.org/u/neshkeev)\
**Replies:** 2\
**Last updated:** [August 1, 2019, 2:33am UTC](https://discourse.rocq-prover.org/t/why-is-reduction-illegal/345 "2019-08-01T02:33:51Z")

</div>

Hi, I am trying to wrap my head around calculus of inductive constructions, but I stuck at η-reduction, I don’t understand why it is illegal. Here is my train of thought: If there is a term (as I interpret it: a functi…