anuyts

## category-theory-eq-in-eq-out.md

      
        
          
            
              
              1 file
            
          
          
            
              
              0 forks
            
          
          
            
              
              0 comments
            
          
          
            
              
              0 stars
            
          
        
        
          
              
          
          
            
                anuyts
                / category-theory-eq-in-eq-out.md
            
            
              Last active
              August 4, 2022 12:54
            
              
                Equality-in-equality-out category theory in cubical Agda
              
          
        
      
        
  
      
    Equality-in-equality-out category theory in cubical Agda

Now that equality has become computationally relevant but composition of equality remains cumbersome,
the statement of various equality laws in the cubical library feels "wrong".
Here I want to explore an alternative approach.
What I'm not proposing

To avoid confusion, I want to start by emphasizing what I'm not proposing.