Liang-Ting Chen L-TChen

## HIIRT.md

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              8 stars
            
          
                AndrasKovacs
                / HIIRT.md
            
            
              Last active
              March 25, 2024 08:20
            
              
                Higher induction-induction-recursion
              
          
    Inductive-Recursive Types, Generally

I write about inductive-recursive types here. "Generally" means "higher
inductive-inductive-recursive" or "quotient inductive-inductive-recursive".
This may sound quite gnarly, but fortunately the specification of signatures can
be given with just a few type formers in an appropriate framework.
In particular, we'll have a theory of signatures which includes Mike Shulman's
higher IR example.

  
## gist:4318441
# Replace REMOTE_NAME with your remote name (e.g. origin)

git branch -r | grep REMOTE_NAME/ | grep -v 'master$' | grep -v HEAD| cut -d/ -f2 | while read line; do git push REMOTE_NAME :$line; done;
	# Replace REMOTE_NAME with your remote name (e.g. origin)

	git branch -r \| grep REMOTE_NAME/ \| grep -v 'master$' \| grep -v HEAD\| cut -d/ -f2 \| while read line; do git push REMOTE_NAME :$line; done;