CODEWITHSUNDEEP
typesrecordagdatype-theory
user5775230
user5775230

Reputation:

How does one understand Data vs Record capabilities in agda?

Why doesn't a custom unit type allow us to prove this basic left unit law? I see the only difference between my implementation and that of the standard library is the use of Record vs Data inductive inductive type former. I don't understand why the Data won't allow me to prove this basic left identity lemma, which should be true definitionally. Does it have to do with Record's automatic eta inheritance? If so, why is this the case? Is it possible to prove this without the builtin (e.g. Record) Unit type? In general, is this a limitation of Data, or is it possible to do everything in agda modulo records?


data _≡_ {A : Set} : A → A → Set where
  refl : (a : A) → a ≡ a

--from builtin
lunitm : (f : ⊤ → ⊤) → (λ x → f tt) ≡ f
lunitm f = refl (λ x → tt)

data ⊤2 : Set where
  tt2 : ⊤2

lunitm2 : (f : ⊤2 → ⊤2) → (λ x → f tt2) ≡ f
lunitm2 f = ? --refl ? --can't instantiate

Upvotes: 2

Views: 651

Answers (1)

effectfully
effectfully

Reputation: 12715

This is indeed due to ⊤2 being a data rather than record.

Agda implements eta-rules for negative types.

Records are negative and so have eta-rules associated with them. The eta-rule of

record Unit : Set where
  constructor unit

is

_ : (u : Unit) -> u ≡ unit
_ = λ u -> refl

Supporting eta-equality for positive types is possible in theory, but Agda does not implement that.

Upvotes: 2

Related Questions