IrrelevantFamilyIndex.agda

-- Andreas, 2011-04-07

module IrrelevantFamilyIndex where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

-- irrelevant index
data Fin : .Nat -> Set where
  zero : .(n : Nat) -> Fin (suc n)
  suc  : .(n : Nat) -> Fin n -> Fin (suc n)

t : Fin zero
t = zero zero

-- the following is ok, since Fin _ is really just Nat
toNat : Fin zero -> Nat
toNat (zero _)  = zero
toNat (suc _ i) = suc (toNat i)

data Pos : Nat -> Set where
  pos : (n : Nat) -> Pos (suc n)

f : (n : Nat) -> Fin n -> Pos n
f .(suc n) (zero n)  = pos n
f .(suc n) (suc n i) = pos n
-- cannot infer value of dot pattern

{-
f : (n : Nat) -> Fin n -> Pos n
f .(suc _) (zero _)  = pos _
f .(suc _) (suc _ _) = pos _

f' : (n : Nat) -> Fin n -> Pos n
f' _ (zero _)  = pos _
f' _ (suc _ _) = pos _
-}