remove unnecessary --safe

anshwad10 · anshwad10 · commit 7411b8e19508 · 2025-11-22T21:43:26.000+05:30
diff --git a/Cubical/Categories/Dagger/Functor.agda b/Cubical/Categories/Dagger/Functor.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --hidden-argument-puns #-}
+{-# OPTIONS --hidden-argument-puns #-}
 
 module Cubical.Categories.Dagger.Functor where
 
@@ -40,7 +40,7 @@ open Functor
 
 †FuncComp : †Functor C D → †Functor D E → †Functor C E
 †FuncComp F G .fst = G .fst ∘F F .fst
-†FuncComp {C = C} {D = D} {E = E} F G .snd .F-† f =
+†FuncComp {C} {D} {E} F G .snd .F-† f =
   G .fst ⟪ F .fst ⟪ f †[ C ] ⟫ ⟫ ≡⟨ cong (G .fst .F-hom) (F .snd .F-† f) ⟩
   G .fst ⟪ F .fst ⟪ f ⟫ †[ D ] ⟫ ≡⟨ G .snd .F-† (F .fst .F-hom f) ⟩
   G .fst ⟪ F .fst ⟪ f ⟫ ⟫ †[ E ] ∎
diff --git a/Cubical/Categories/Dagger/Instances/BinProduct.agda b/Cubical/Categories/Dagger/Instances/BinProduct.agda
@@ -1,5 +1,3 @@
-{-# OPTIONS --safe #-}
-
 module Cubical.Categories.Dagger.Instances.BinProduct where
 
 open import Cubical.Foundations.Prelude
diff --git a/Cubical/Categories/Dagger/Instances/Functors.agda b/Cubical/Categories/Dagger/Instances/Functors.agda
@@ -1,5 +1,3 @@
-{-# OPTIONS --safe #-}
-
 module Cubical.Categories.Dagger.Instances.Functors where
 
 open import Cubical.Foundations.Prelude
diff --git a/Cubical/Categories/Dagger/Properties.agda b/Cubical/Categories/Dagger/Properties.agda
@@ -1,5 +1,3 @@
-{-# OPTIONS --safe #-}
-
 module Cubical.Categories.Dagger.Properties where
 
 open import Cubical.Foundations.Prelude

Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,3 @@`
`1`		`-{-# OPTIONS --safe #-}`
`2`		`-`
`3`	`1`	`module Cubical.Categories.Dagger.Instances.BinProduct where`
`4`	`2`
`5`	`3`	`open import Cubical.Foundations.Prelude`
Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,3 @@`
`1`		`-{-# OPTIONS --safe #-}`
`2`		`-`
`3`	`1`	`module Cubical.Categories.Dagger.Properties where`
`4`	`2`
`5`	`3`	`open import Cubical.Foundations.Prelude`