Update Properties.agda

oisdk · Feb 1, 2024 · 7b4f1ba · 7b4f1ba
1 parent 863d155
commit 7b4f1ba
Showing 1 changed file with 5 additions and 4 deletions.
diff --git a/Data/List/Properties.agda b/Data/List/Properties.agda
@@ -99,10 +99,11 @@ foldr-reverse f b = foldl-fusion (foldr f b) [] (λ _ _ → refl)
 module _ {A : Type a} where
   reverse-reverse : (xs : List A) → reverse (reverse xs) ≡ xs
   reverse-reverse xs = foldl-is-foldr (flip _∷_) [] (reverse xs)
-                     ; cong (_$ []) (foldr-reverse (foldl-by-r-cons _∷_) id xs)
-                     ; cong (_$ []) (foldl-is-foldr (flip (foldl-by-r-cons _∷_)) id xs)
-                     ; cong (λ k → k id [] ) (sym (foldr-universal (λ xs k a → k (foldr _∷_ a xs)) (foldl-by-r-cons (foldl-by-r-cons _∷_)) id refl (λ x xs → funExt λ k → funExt λ a → refl) xs))
-                     -- ; cong (λ k → k id [] ) (sym (foldr-fusion {!!}  {_⊗_ = (foldl-by-r-cons (foldl-by-r-cons _∷_))} {!!} {!!} xs))
+                     ; cong (_$ [])
+                       ( foldr-reverse (foldl-by-r-cons _∷_) id xs
+                       ; foldl-is-foldr (flip (foldl-by-r-cons _∷_)) id xs
+                       ; cong′ (_$ id) (sym (foldr-universal (λ xs k a → k (foldr _∷_ a xs)) (foldl-by-r-cons (foldl-by-r-cons _∷_)) id refl (λ x xs → refl) xs))
+                       )
                      ; sym (foldr-id xs)
 
 ++-assoc : (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)