open import Paths
open import Logic::HLevels

open data SetTrunc (A : Type)
| inj A
| trunc : isSet (SetTrunc A)

variable A B : Type

// TODO: improve the termination checker so that it unfolds unrecursive calls generate unfolded lambdas properly
def rec (A → B) (isSet B) (SetTrunc A) : B
| f, x, inj a ⇒ f a
| f, x, trunc a b p q i j ⇒
    x (rec f x a) (rec f x b) (\ k ⇒ rec f x (p k)) (\ k ⇒ rec f x (q k)) i j