{- Checking that nesting invertible functions works properly. In this example we should get El2 α = B {reduces to} El1 (embed α) = B {simplifies by invertibility to} embed α = b {simplifies by invertibility to} α = b -} module NestedInj where data A : Set where theA : A data B : Set where theB : B data U1 : Set where a : U1 b : U1 data U2 : Set where b : U2 El1 : U1 -> Set El1 a = A El1 b = B embed : U2 -> U1 embed b = b El2 : U2 -> Set El2 c = El1 (embed c) f1 : {c : U1} -> El1 c -> El1 c f1 {a} theA = theA f1 {b} theB = theB f2 : {c : U2} -> El2 c -> El2 c f2 x = f1 x test : B test = f2 theB