———— All done; warnings encountered ———————————————————————— /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Bounded/Base.agda:138,1-140,70 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: it relies on higher-dimensional unification, which is not yet supported when checking the definition of drop /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Bounded/Base.agda:133,1-135,74 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: it relies on higher-dimensional unification, which is not yet supported when checking the definition of take /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:281,1-284,24 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor zero, which is not yet supported when checking the definition of initLast /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:281,1-284,24 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of initLast /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:254,1-25 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of uncons /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:242,1-246,22 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor zero, which is not yet supported when checking the definition of group /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:227,1-230,25 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of splitAt /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:192,1-39 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of foldl₁ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:181,1-182,50 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of foldr₁ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:152,1-153,38 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of _⊛_ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:152,1-153,38 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor zero, which is not yet supported when checking the definition of _⊛_ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:120,1-121,54 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of zipWith /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:120,1-121,54 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor zero, which is not yet supported when checking the definition of zipWith /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:71,1-72,52 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of updateAt /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:67,1-68,53 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of remove /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:63,1-64,47 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of insert /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:59,1-60,38 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of lookup /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:56,1-19 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of tail /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Vec/Base.agda:53,1-18 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of head /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:736,3-737,75 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of respects /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:736,3-737,75 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of respects /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:700,1-701,34 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of tails⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:687,1-690,61 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of inits⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:687,1-690,61 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of inits⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:677,1-25 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of replicate⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:666,1-667,40 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of fromMaybe⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:666,1-667,40 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of fromMaybe⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:640,3-646,85 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of deduplicate⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:640,3-646,85 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of deduplicate⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:629,3-637,73 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of derun⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:633,5-637,73 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of aux /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:633,5-637,73 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of aux /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:635,5-637,73 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1646 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:635,5-637,73 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1646 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:635,5-637,73 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1646 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:636,5-83 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1660 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:618,3-622,35 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of derun⁺ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:618,3-622,35 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of derun⁺ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:595,3-600,94 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of filter⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:597,3-600,94 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1468 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:597,3-600,94 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1468 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:597,3-600,94 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1468 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:574,1-575,42 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ─⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:570,1-571,36 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ─⁺ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:563,1-564,57 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of tabulate⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:563,1-564,57 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of tabulate⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:563,1-564,57 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: it relies on higher-dimensional unification, which is not yet supported when checking the definition of tabulate⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:533,1-535,39 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of applyUpTo⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:533,1-535,39 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of applyUpTo⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:533,1-535,39 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: it relies on higher-dimensional unification, which is not yet supported when checking the definition of applyUpTo⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:519,1-520,18 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1222 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:519,1-520,18 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1222 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:513,1-514,28 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1184 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:513,1-514,28 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1184 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:496,1-497,24 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1094 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:496,1-497,24 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1094 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:489,1-490,28 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1056 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:489,1-490,28 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-1056 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:449,1-450,68 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor just, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-912 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:449,1-450,68 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor nothing, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-912 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:428,1-429,67 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of concat⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:413,3-414,63 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ++⁺∘++⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:406,1-407,58 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ++⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:402,1-403,39 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ++⁻ʳ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:398,1-399,45 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ++⁻ˡ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:384,1-388,37 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of mapMaybe⁺ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:384,1-388,37 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of mapMaybe⁺ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:388,1-37 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor just, which is not yet supported when checking the definition of Data.List.Relation.Unary.All.Properties.with-742 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:371,1-372,41 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of map⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:371,1-372,41 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of map⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:361,1-362,51 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor just, which is not yet supported when checking the definition of uncons⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:361,1-362,51 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor nothing, which is not yet supported when checking the definition of uncons⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:333,1-26 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of singleton⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:333,1-26 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of singleton⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:324,1-325,77 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of map-updateAt /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:313,1-318,68 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of updateAt-commutes /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:295,1-296,100 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of updateAt-cong-relative /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:284,1-285,80 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of updateAt-compose /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:276,1-278,54 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of updateAt-compose-relative /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:262,1-263,93 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of updateAt-id-relative /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:218,1-223,64 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor there, which is not yet supported when checking the definition of updateAt-minimal /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:218,1-223,64 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor here, which is not yet supported when checking the definition of updateAt-minimal /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:218,1-223,64 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of updateAt-minimal /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:207,1-209,38 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor there, which is not yet supported when checking the definition of updateAt-updates /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:207,1-209,38 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor here, which is not yet supported when checking the definition of updateAt-updates /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:207,1-209,38 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of updateAt-updates /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:194,1-195,53 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of lookup-map /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:156,1-157,59 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of []=lookup /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:141,3-145,45 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of All-swap /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:121,33-124,6 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of .extendedlambda0 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:95,1-96,47 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of All¬⇒¬Any /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:82,1-83,66 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor there, which is not yet supported when checking the definition of []=-injective /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All/Properties.agda:82,1-83,66 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor here, which is not yet supported when checking the definition of []=-injective /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Maybe/Relation/Unary/All.agda:116,3-117,53 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor nothing, which is not yet supported when checking the definition of irrelevant /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Maybe/Relation/Unary/All.agda:116,3-117,53 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor just, which is not yet supported when checking the definition of irrelevant /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Maybe/Relation/Unary/All.agda:55,3-56,42 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor nothing, which is not yet supported when checking the definition of zipWith /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Maybe/Relation/Unary/All.agda:55,3-56,42 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor just, which is not yet supported when checking the definition of zipWith /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Maybe/Relation/Unary/All.agda:37,3-27 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor just, which is not yet supported when checking the definition of drop-just /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Induction/WellFounded.agda:237,5-239,46 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _,_, which is not yet supported when checking the definition of accessible′ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Membership/Propositional/Properties.agda:402,1-405,51 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of boolFilter-∈ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Membership/Propositional/Properties.agda:352,3-382,8 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of helper /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Membership/Propositional/Properties.agda:352,3-382,8 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of helper /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Membership/Propositional/Properties.agda:348,3-349,28 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of Data.List.Membership.Propositional.Properties.with-740 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Membership/Setoid/Properties.agda:387,3-390,64 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ∈-∷=⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Membership/Setoid/Properties.agda:381,3-384,88 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ∈-∷=⁺-untouched /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Membership/Setoid/Properties.agda:348,3-349,52 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of ∈-lookup /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Membership/Setoid/Properties.agda:304,3-305,60 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of Data.List.Membership.Setoid.Properties.with-1484 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Membership/Setoid/Properties.agda:293,3-298,34 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ∈-filter⁺ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Membership/Setoid/Properties.agda:77,3-84,33 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of unique⇒irrelevant /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:655,3-34 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of return⁺∘return⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:652,3-23 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of return⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:631,1-634,38 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of Data.List.Relation.Unary.Any.Properties.with-2012 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:623,1-626,78 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of reverseAcc⁺ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:615,5-617,46 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of to∘from /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:597,3-599,65 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of map-with-∈⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:579,3-580,91 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of deduplicate⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:569,5-573,63 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of derun⁻-aux /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:571,5-573,63 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of Data.List.Relation.Unary.Any.Properties.with-1780 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:560,3-565,67 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of deduplicate⁺ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:554,3-557,40 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of derun⁺ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:550,5-551,42 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.List.Relation.Unary.Any.Properties.with-1638 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:537,3-539,48 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of Data.List.Relation.Unary.Any.Properties.with-1576 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:528,3-533,26 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of filter⁺ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:529,3-530,41 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.List.Relation.Unary.Any.Properties.with-1538 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:519,1-520,65 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of tabulate⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:507,3-509,43 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of applyDownFrom⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:501,3-503,64 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of applyDownFrom⁺ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:502,3-503,64 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.List.Relation.Unary.Any.Properties.with-1430 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:502,3-503,64 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.List.Relation.Unary.Any.Properties.with-1430 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:491,1-493,40 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of applyUpTo⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:485,1-487,43 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of applyUpTo⁺ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:434,3-439,57 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of concat⁺∘concat⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:438,3-439,57 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of Data.List.Relation.Unary.Any.Properties.with-1178 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:416,3-420,28 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of concat⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:419,3-420,28 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of Data.List.Relation.Unary.Any.Properties.with-1084 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:385,3-397,53 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ++-comm∘++-comm /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:372,3-375,81 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ++⁻∘++⁺ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:364,3-368,39 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ++⁺∘++⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:359,3-361,55 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ++⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:341,3-343,60 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: it relies on higher-dimensional unification, which is not yet supported when checking the definition of Data.List.Relation.Unary.Any.Properties.with-770 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:341,3-343,60 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor just, which is not yet supported when checking the definition of Data.List.Relation.Unary.Any.Properties.with-770 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:341,3-343,60 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of Data.List.Relation.Unary.Any.Properties.with-770 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:320,3-321,65 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of map⁺∘map⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:316,3-317,48 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of map⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:304,1-26 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of singleton⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:76,1-28 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor there, which is not yet supported when checking the definition of there-injective /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:73,1-27 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor here, which is not yet supported when checking the definition of here-injective /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any/Properties.agda:69,1-70,76 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of lift-resp /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Maybe/Relation/Unary/Any.agda:73,3-75 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor just, which is not yet supported when checking the definition of irrelevant /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Maybe/Relation/Unary/Any.agda:50,3-53 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor just, which is not yet supported when checking the definition of zipWith /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Maybe/Relation/Unary/Any.agda:33,3-27 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor just, which is not yet supported when checking the definition of drop-just /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Function/Related/TypeIsomorphisms.agda:334,1-337,55 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of True↔ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Function/Setoid.agda:101,5-102,66 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₂, which is not yet supported when checking the definition of inj /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Function/Setoid.agda:101,5-102,66 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₁, which is not yet supported when checking the definition of inj /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Relation/Binary/Pointwise.agda:103,3-104,63 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₂, which is not yet supported when checking the definition of ⊎-respectsʳ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Relation/Binary/Pointwise.agda:103,3-104,63 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₁, which is not yet supported when checking the definition of ⊎-respectsʳ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Relation/Binary/Pointwise.agda:98,3-99,63 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₂, which is not yet supported when checking the definition of ⊎-respectsˡ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Relation/Binary/Pointwise.agda:98,3-99,63 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₁, which is not yet supported when checking the definition of ⊎-respectsˡ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Relation/Binary/Pointwise.agda:93,3-94,76 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₂, which is not yet supported when checking the definition of ⊎-antisymmetric /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Relation/Binary/Pointwise.agda:93,3-94,76 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₁, which is not yet supported when checking the definition of ⊎-antisymmetric /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Relation/Binary/Pointwise.agda:88,3-89,64 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₂, which is not yet supported when checking the definition of ⊎-irreflexive /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Relation/Binary/Pointwise.agda:88,3-89,64 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₁, which is not yet supported when checking the definition of ⊎-irreflexive /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Relation/Binary/Pointwise.agda:63,39-65 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₂, which is not yet supported when checking the definition of .extendedlambda1 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Relation/Binary/Pointwise.agda:62,39-65 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₁, which is not yet supported when checking the definition of .extendedlambda0 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Relation/Binary/Pointwise.agda:57,3-58,67 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₂, which is not yet supported when checking the definition of ⊎-transitive /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Relation/Binary/Pointwise.agda:57,3-58,67 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₁, which is not yet supported when checking the definition of ⊎-transitive /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Relation/Binary/Pointwise.agda:43,3-25 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₂, which is not yet supported when checking the definition of drop-inj₂ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Relation/Binary/Pointwise.agda:40,3-25 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₁, which is not yet supported when checking the definition of drop-inj₁ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Properties.agda:33,1-27 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₂, which is not yet supported when checking the definition of inj₂-injective /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Sum/Properties.agda:30,1-27 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor inj₁, which is not yet supported when checking the definition of inj₁-injective /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Product/Properties.agda:54,1-31 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _,_, which is not yet supported when checking the definition of ,-injective /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Product/Properties.agda:51,1-25 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _,_, which is not yet supported when checking the definition of ,-injectiveʳ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Product/Properties.agda:44,3-45,106 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor Agda.Builtin.Bool.Bool.true, which is not yet supported when checking the definition of Data.Product.Properties.with-84 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Product/Properties.agda:44,3-45,106 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor Agda.Builtin.Bool.Bool.false, which is not yet supported when checking the definition of Data.Product.Properties.with-84 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Product/Properties.agda:36,3-72 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _,_, which is not yet supported when checking the definition of ,-injectiveʳ-≡ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Product/Properties.agda:33,3-27 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _,_, which is not yet supported when checking the definition of ,-injectiveˡ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:253,1-254,47 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor ℕ.suc, which is not yet supported when checking the definition of lookup⁺ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:228,3-231,61 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.List.Relation.Binary.Pointwise.with-490 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:228,3-231,61 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.List.Relation.Binary.Pointwise.with-490 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:202,1-203,57 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of map⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:202,1-203,57 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of map⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:159,1-165,107 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ++-cancelʳ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:155,1-156,70 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ++-cancelˡ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:143,1-144,65 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor ℕ.suc, which is not yet supported when checking the definition of tabulate⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:143,1-144,65 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of tabulate⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:143,1-144,65 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: it relies on higher-dimensional unification, which is not yet supported when checking the definition of tabulate⁻ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:119,1-122,40 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of AllPairs-resp-Pointwise /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:119,1-122,40 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of AllPairs-resp-Pointwise /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:113,1-115,41 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of Any-resp-Pointwise /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:107,1-109,47 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of All-resp-Pointwise /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise.agda:107,1-109,47 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of All-resp-Pointwise /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/AllPairs.agda:77,1-79,68 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of irrelevant /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/AllPairs.agda:77,1-79,68 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of irrelevant /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/AllPairs.agda:53,3-54,84 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of zipWith /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/AllPairs.agda:53,3-54,84 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of zipWith /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/AllPairs.agda:39,1-22 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of tail /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/AllPairs.agda:36,1-21 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of head /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise/Properties.agda:76,1-78,49 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of irrelevant /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise/Properties.agda:76,1-78,49 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of irrelevant /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise/Properties.agda:62,1-63,79 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of respˡ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise/Properties.agda:62,1-63,79 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of respˡ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise/Properties.agda:58,1-59,79 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of respʳ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise/Properties.agda:58,1-59,79 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of respʳ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise/Properties.agda:53,1-55,54 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of antisymmetric /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise/Properties.agda:53,1-55,54 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of antisymmetric /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise/Properties.agda:47,1-49,47 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of transitive /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise/Properties.agda:47,1-49,47 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of transitive /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise/Base.agda:45,1-27 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of tail /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Binary/Pointwise/Base.agda:42,1-25 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of head /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:975,3-979,42 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ∷ʳ-injective /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:808,3-809,23 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.List.Properties.with-3952 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:808,3-809,23 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.List.Properties.with-3952 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:803,3-804,42 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.List.Properties.with-3914 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:803,3-804,42 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.List.Properties.with-3914 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:764,3-765,31 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.List.Properties.with-3768 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:759,3-760,46 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.List.Properties.with-3744 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:745,3-748,47 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of filter-none /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:745,3-748,47 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of filter-none /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:747,3-748,47 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.List.Properties.with-3682 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:737,3-742,32 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of filter-some /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:738,3-739,46 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.List.Properties.with-3630 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:729,3-734,43 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of filter-notAll /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:730,3-731,47 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.List.Properties.with-3580 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:723,3-726,55 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of filter-all /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:723,3-726,55 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of filter-all /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:725,3-726,55 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.List.Properties.with-3546 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:661,1-662,56 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of map-─ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:655,1-656,63 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of length-─ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:648,1-649,62 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of map-∷= /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:636,1-637,59 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of length-%= /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:583,3-584,66 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of lookup-applyDownFrom /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:570,1-571,68 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of lookup-applyUpTo /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:470,3-475,60 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of foldr-preservesᵒ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:66,3-27 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ∷-injectiveʳ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:63,3-27 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ∷-injectiveˡ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Properties.agda:60,3-35 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of ∷-injective /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All.agda:213,1-215,55 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of irrelevant /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All.agda:213,1-215,55 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of irrelevant /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All.agda:185,1-186,49 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of lookupAny /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All.agda:135,1-137,60 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of updateAt /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All.agda:102,1-103,70 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of zipWith /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All.agda:102,1-103,70 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor [], which is not yet supported when checking the definition of zipWith /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/All.agda:74,1-29 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of uncons /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any.agda:80,1-81,29 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of toSum /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any.agda:50,1-51,27 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of tail /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Relation/Unary/Any.agda:46,1-47,47 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor _∷_, which is not yet supported when checking the definition of head /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Base.agda:339,1-340,32 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of _─_ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Base.agda:332,1-333,44 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of _[_]%=_ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/List/Base.agda:219,1-220,38 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of lookup /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:282,1-288,47 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of compare /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:246,1-248,48 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of pinch /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:239,1-241,44 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of punchIn /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:231,1-234,72 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of punchOut /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:223,1-224,48 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of opposite /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:211,1-212,27 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of _ℕ-ℕ_ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:203,1-204,25 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of _ℕ-_ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:195,1-196,23 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of _-_ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:178,1-180,42 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of lift /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:171,1-173,46 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of fold′ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:152,1-153,54 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of combine /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:130,1-132,55 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of splitAt /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:116,1-118,65 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of lower₁ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:110,1-111,61 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: it relies on higher-dimensional unification, which is not yet supported when checking the definition of inject≤ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:98,1-99,59 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of inject! /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:94,1-95,44 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of inject /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:88,1-89,50 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of reduce≥ /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Fin/Base.agda:51,1-53,64 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of cast /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Nat/Properties.agda:1865,1-30 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor ≤′-step, which is not yet supported when checking the definition of ≤′-step-injective /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Nat/Properties.agda:1614,1-22 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of <⇒≤pred /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Nat/Properties.agda:1484,1-1486,54 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of +-∸-comm /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Nat/Properties.agda:1478,1-48 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of m>n⇒m∸n≢0 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Nat/Properties.agda:1478,1-48 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: it relies on higher-dimensional unification, which is not yet supported when checking the definition of m>n⇒m∸n≢0 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Nat/Properties.agda:1474,1-1475,58 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Data.Nat.Properties.with-3898 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Nat/Properties.agda:1474,1-1475,58 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Data.Nat.Properties.with-3898 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Data/Nat/Properties.agda:1469,1-1470,52 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of m-nonZero /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Relation/Nullary/Decidable/Core.agda:118,1-39 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of Relation.Nullary.Decidable.Core.with-130 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Relation/Nullary/Decidable/Core.agda:118,1-39 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: it relies on higher-dimensional unification, which is not yet supported when checking the definition of Relation.Nullary.Decidable.Core.with-130 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Relation/Nullary/Decidable/Core.agda:114,1-38 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of Relation.Nullary.Decidable.Core.with-112 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Relation/Nullary/Decidable/Core.agda:114,1-38 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: it relies on higher-dimensional unification, which is not yet supported when checking the definition of Relation.Nullary.Decidable.Core.with-112 /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Relation/Nullary.agda:63,1-64,36 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor true, which is not yet supported when checking the definition of recompute /build/agda-stdlib/src/agda-stdlib-1.7.2/src/Relation/Nullary.agda:63,1-64,36 This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor false, which is not yet supported when checking the definition of recompute