Skip to content

Commit b98c453

Browse files
authored
Imported _$_
1 parent a48ba5c commit b98c453

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

Cubical/Algebra/SymmetricGroup.agda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ module Cubical.Algebra.SymmetricGroup where
44
open import Cubical.Foundations.Prelude
55
open import Cubical.Foundations.Equiv
66
open import Cubical.Foundations.HLevels
7+
open import Cubical.Foundations.Function
78
open import Cubical.Data.Sigma
89
open import Cubical.Data.Nat
910
open import Cubical.Data.SumFin

0 commit comments

Comments
 (0)