data Vec A : ℕ → Set where
[] : Vec A zero
_∷_ : A → Vec A n → Vec A (suc n)
--vs--
record Vec A n : Set where
constructor tabulate
field
lookup : Fin n → A
--vs--
Vec : Set → ℕ → Set
Vec A zero = ⊤
Vec A (suc n) = A × Vec A n
Fight!
Conversation
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Where's that univalence axiom when you need it…