Agda-2.3.2.2: examples/AIM6/Path/Fin.agda

module Fin where

open import Prelude
open import Star
open import Modal
open import Nat

Fin : Nat -> Set
Fin = Any (\_ -> True)

fzero : {n : Nat} -> Fin (suc n)
fzero = done _ • ε

fsuc : {n : Nat} -> Fin n -> Fin (suc n)
fsuc i = step • i