1
$\begingroup$

I am confused with the context related to identity type in HoTT

In particular, for a family $C : (a =_A a) \to U$ dependent on a loop, we cannot apply path induction and consider only the case for $C(\text{refl}_a)$, and consequently, we cannot prove that all loops are reflexivity.

and

In other words, a path $p : x = x$ may be not equal to reflexivity as an element of $(x = x)$,

Then I try to verify the above sentences in agda, I have written following codes

open import Relation.Binary.PropositionalEquality

postulate
    x : Set
    y : Set

eq₁ : x ≡ x → Set
eq₁ refl = x

eq₂ : {z : Set} → x ≡ z → Set
eq₂ refl = x

eq₃ : x ≡ y → Set
eq₃ x=y = {!  !}

My problem is why we can just care the case $\text{refl}_x$ in eq₁, it seems to be contradictory to the second quote ? I can understand refl is just a instance constructor of identity type.

Then in eq₃, we can not use refl to substitute x=y. Can explain some details in these three eq?

$\endgroup$
3
  • 6
    $\begingroup$ Agda by default uses axiom K, which implies uniqueness of identity proofs and is therefore incompatible with HoTT. If you disable it with --without-K, then eq₁ won't be accepted any more (but eq₂ will be, because z is a "free" endpoint). $\endgroup$ Commented Apr 25, 2023 at 14:54
  • 1
    $\begingroup$ dl.acm.org/doi/10.1145/2628136.2628139 this paper explains pretty well $\endgroup$
    – ice1000
    Commented Apr 25, 2023 at 19:40
  • $\begingroup$ I wrote about this on my blog, see the elements of inductive types. $\endgroup$ Commented May 3, 2023 at 10:37

1 Answer 1

1
$\begingroup$

It looks like you have enough knowledge to work out what's going on with eq₁. It is accepted in standard Agda, but not with flags --without-K, --cubical, or --cubical-compatible.

As for eq₃, this pattern matching failure is more contingent on aspects traditionally thought of as “implementation details”. To start, in Agda, postulates are implemented essentially as (function) definitions without bodies. Therefore, whatever applies to postulates generally also applies to definitions. With that in mind, consider what happens when we replace the postulates x and y by these definitions:

data Bool : Set where true false : Bool

x : Bool → Bool
x _ = false

y : Bool → Bool
y true = false
y false = true

Then, if we have a variable q : x ≡ y and try to match it against refl, we have to unify x and y. The question is: Do we turn x into y or y into x? This matters, for example, when trying to work out the behaviour of the following function foo (where refl : {x : Bool → Bool} → x ≡ x, and thus z is bound to whatever common unifier is chosen between x and y).

foo : x ≡ y → Bool
foo (refl {x = z}) = z false

One could argue that x and y are unequal, and so they should anti-unify, allowing us to use the absurd pattern () rather than refl. However, their inequality is a matter of proof, and if you consider functions from the natural numbers instead of the Booleans, you can soon reach undecidability.

In contrast, in eq₂, we know that z is a bound variable, and thus cannot have a definition. The pattern refl unifies x and z using the substitution [z ↦ x].

$\endgroup$
3
  • $\begingroup$ What happends when x and z are both bound ? $\endgroup$
    – maplgebra
    Commented May 5, 2023 at 3:22
  • $\begingroup$ @maplgebra You mean x and y? They unify into a notionally fresh bound variable – like the z in my example. $\endgroup$
    – James Wood
    Commented May 5, 2023 at 7:37
  • $\begingroup$ I see, it finally makes sense. $\endgroup$
    – maplgebra
    Commented May 5, 2023 at 9:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.