How do I determine the breakpoint of a functor?

In Haskell, I can define the endofunctor endpoint like so:

data Fix f = Fix (f (Fix f))

      

        
        
        
      

    

But in Agda it cannot:

data Fix (F : Id (Set → Set)) : Set where
    fix : (unId F) (Fix F) → Fix F

      

        
        
        
      

    

because it says, "The fix is ​​not strictly positive because it occurs in the argument of a bound variable in the type of the fix constructor in the Fix definition."

I tried using Coinduction.∞

from stdlib, in vain:

data Fix (F : Set → Set) : Set where
    fix : ∞ (F (Fix F)) → Fix F

      

        
        
        
      

    

or

data Fix (F : Set → Set) : Set where
    fix : F (∞ (Fix F)) → Fix F

      

        
        
        
      

    

does not work.

I found this document which defines polynomial functors Functor

and a function [_] : Functor → Set → Set

that works:

data Functor : Set₁ where
    Id : Functor
    Const : Set → Functor
    _⊕_ : Functor → Functor → Functor
    _⊗_ : Functor → Functor → Functor

[_] : Functor → Set → Set
[ Id ] B = B
[ Const C ] _ = C
[ F ⊕ G ] B = [ F ] B ⊎ [ G ] B
[ F ⊗ G ] B = [ F ] B × [ G ] B

data Fix (F : Functor) : Set where
    fix : [ F ] (Fix F) → Fix F

      

        
        
        
      

    

but I'm not sure why that would be, and it is not, since both have a Fix

bound variable as an argument F

.

Is it possible to define a common endpoint in Agda, and if so how?

EDIT: This has been noted as a possible duplicate of 14699334 , but the only answer there is related to the Agda tutorial (?), Which includes fixing the point of the type of a specific polynomial functor; I want to know if this can be defined more generally. Specifically, I want to define fixed points of types that may be structurally equal, but nominally unequal.