Valeria de Paiva vcvpaiva

## dial_2.v
Record Dial_2 :=
  {
  U : Type;
  X : Type;
  alpha : U -> X -> Prop
  }.

Record Mor (A B : Dial_2) :=
  {
  f : U A -> U B;

## Dialectica.lagda.md

      
        
          
            
              
              1 file
            
          
          
            
              
              1 fork
            
          
          
            
              
              1 comment
            
          
          
            
              
              1 star
            
          
        
        
          
              
          
          
            
                TOTBWF
                / Dialectica.lagda.md
            
            
              Last active
              June 14, 2024 14:55
            
              
                Dialectica Categories with Valeria
              
          
        
      
        
  
      
    
  
  
  description
  
  
  
  
  Dialectica categories, done representably.
June 4th, 2024 at the HIM trimester.
	Record Dial_2 :=
	{
	U : Type;
	X : Type;
	alpha : U -> X -> Prop
	}.

	Record Mor (A B : Dial_2) :=
	{
	f : U A -> U B;