# How does this dependently-typed boolean elimination function work?

In the companion code to A Tutorial Implementation of a Dependently Typed Lambda Calculus - prelude.lp - there is a rather intimidating definition of a boolElim function that's not described in the paper itself:

let boolElim =
( \ m mf mt -> finElim ( nat2Elim (\ n -> Fin n -> *)
(\ _ -> Unit) (\ _ -> Unit)
(\ x -> m x)
(\ _ _ _ -> Unit) )
( nat1Elim ( \ n -> nat1Elim (\ n -> Fin (Succ n) -> *)
(\ _ -> Unit)
(\ x -> m x)
(\ _ _ _ -> Unit)
n (FZero n))
U mf (\ _ _ -> U) )
( \ n f _ -> finElim ( \ n f -> nat1Elim (\ n -> Fin (Succ n) -> *)
(\ _ -> Unit)
(\ x -> m x)
(\ _ _ _ -> Unit)
n (FSucc n f) )
( natElim
( \ n -> natElim
(\ n -> Fin (Succ (Succ n)) -> *)
(\ x -> m x)
(\ _ _ _ -> Unit)
n (FSucc (Succ n) (FZero n)) )
mt (\ _ _ -> U) )
( \ n f _ -> finElim
(\ n f -> natElim
(\ n -> Fin (Succ (Succ n)) -> *)
(\ x -> m x)
(\ _ _ _ -> Unit)
n (FSucc (Succ n) (FSucc n f)))
(\ _ -> U)
(\ _ _ _ -> U)
n f )
n f )
2 )
:: forall (m :: Bool -> *) . m False -> m True -> forall (b :: Bool) . m b


The type indicates its behaviour (an if-else), but I can't make any headway with the definition. Can someone break it down for me?

• I think the code is a bit long to ask about in a stackexchange post. Is there a way to shorten the code to just the part you don't get? – 6005 May 14 '20 at 12:41
• @6005 I don't really get any of it – Matt R May 14 '20 at 15:53
• If I understand correctly this encodes Bool as Fin 2. I had a similar question a while ago, it might help: stackoverflow.com/questions/63728749/… – Labbekak Mar 31 at 14:18